imports Permanent_Interpretation Complete_Lattice_ix ACom_ITP

theory Collecting_ITP imports "~~/src/Tools/Permanent_Interpretation" Complete_Lattice_ix "ACom_ITP" begin subsection "Collecting Semantics of Commands" subsubsection "Annotated commands as a complete lattice" (* Orderings could also be lifted generically (thus subsuming the instantiation for preord and order), but then less_eq_acom would need to become a definition, eg less_eq_acom = lift2 less_eq, and then proofs would need to unfold this defn first. *) instantiation acom :: (order) order begin fun less_eq_acom :: "('a::order)acom => 'a acom => bool" where "(SKIP {S}) ≤ (SKIP {S'}) = (S ≤ S')" | "(x ::= e {S}) ≤ (x' ::= e' {S'}) = (x=x' ∧ e=e' ∧ S ≤ S')" | "(c1;;c2) ≤ (c1';;c2') = (c1 ≤ c1' ∧ c2 ≤ c2')" | "(IF b THEN c1 ELSE c2 {S}) ≤ (IF b' THEN c1' ELSE c2' {S'}) = (b=b' ∧ c1 ≤ c1' ∧ c2 ≤ c2' ∧ S ≤ S')" | "({Inv} WHILE b DO c {P}) ≤ ({Inv'} WHILE b' DO c' {P'}) = (b=b' ∧ c ≤ c' ∧ Inv ≤ Inv' ∧ P ≤ P')" | "less_eq_acom _ _ = False" lemma SKIP_le: "SKIP {S} ≤ c <-> (∃S'. c = SKIP {S'} ∧ S ≤ S')" by (cases c) auto lemma Assign_le: "x ::= e {S} ≤ c <-> (∃S'. c = x ::= e {S'} ∧ S ≤ S')" by (cases c) auto lemma Seq_le: "c1;;c2 ≤ c <-> (∃c1' c2'. c = c1';;c2' ∧ c1 ≤ c1' ∧ c2 ≤ c2')" by (cases c) auto lemma If_le: "IF b THEN c1 ELSE c2 {S} ≤ c <-> (∃c1' c2' S'. c= IF b THEN c1' ELSE c2' {S'} ∧ c1 ≤ c1' ∧ c2 ≤ c2' ∧ S ≤ S')" by (cases c) auto lemma While_le: "{Inv} WHILE b DO c {P} ≤ w <-> (∃Inv' c' P'. w = {Inv'} WHILE b DO c' {P'} ∧ c ≤ c' ∧ Inv ≤ Inv' ∧ P ≤ P')" by (cases w) auto definition less_acom :: "'a acom => 'a acom => bool" where "less_acom x y = (x ≤ y ∧ ¬ y ≤ x)" instance proof case goal1 show ?case by(simp add: less_acom_def) next case goal2 thus ?case by (induct x) auto next case goal3 thus ?case apply(induct x y arbitrary: z rule: less_eq_acom.induct) apply (auto intro: le_trans simp: SKIP_le Assign_le Seq_le If_le While_le) done next case goal4 thus ?case apply(induct x y rule: less_eq_acom.induct) apply (auto intro: le_antisym) done qed end fun sub⇩_{1}:: "'a acom => 'a acom" where "sub⇩_{1}(c1;;c2) = c1" | "sub⇩_{1}(IF b THEN c1 ELSE c2 {S}) = c1" | "sub⇩_{1}({I} WHILE b DO c {P}) = c" fun sub⇩_{2}:: "'a acom => 'a acom" where "sub⇩_{2}(c1;;c2) = c2" | "sub⇩_{2}(IF b THEN c1 ELSE c2 {S}) = c2" fun invar :: "'a acom => 'a" where "invar({I} WHILE b DO c {P}) = I" fun lift :: "('a set => 'b) => com => 'a acom set => 'b acom" where "lift F com.SKIP M = (SKIP {F (post ` M)})" | "lift F (x ::= a) M = (x ::= a {F (post ` M)})" | "lift F (c1;;c2) M = lift F c1 (sub⇩_{1}` M);; lift F c2 (sub⇩_{2}` M)" | "lift F (IF b THEN c1 ELSE c2) M = IF b THEN lift F c1 (sub⇩_{1}` M) ELSE lift F c2 (sub⇩_{2}` M) {F (post ` M)}" | "lift F (WHILE b DO c) M = {F (invar ` M)} WHILE b DO lift F c (sub⇩_{1}` M) {F (post ` M)}" permanent_interpretation Complete_Lattice_ix "%c. {c'. strip c' = c}" "lift Inter" proof case goal1 have "a:A ==> lift Inter (strip a) A ≤ a" proof(induction a arbitrary: A) case Seq from Seq.prems show ?case by(force intro!: Seq.IH) next case If from If.prems show ?case by(force intro!: If.IH) next case While from While.prems show ?case by(force intro!: While.IH) qed force+ with goal1 show ?case by auto next case goal2 thus ?case proof(induction b arbitrary: i A) case SKIP thus ?case by (force simp:SKIP_le) next case Assign thus ?case by (force simp:Assign_le) next case Seq from Seq.prems show ?case by (force intro!: Seq.IH simp:Seq_le) next case If from If.prems show ?case by (force simp: If_le intro!: If.IH) next case While from While.prems show ?case by(fastforce simp: While_le intro: While.IH) qed next case goal3 have "strip(lift Inter i A) = i" proof(induction i arbitrary: A) case Seq from Seq.prems show ?case by (fastforce simp: strip_eq_Seq subset_iff intro!: Seq.IH) next case If from If.prems show ?case by (fastforce intro!: If.IH simp: strip_eq_If) next case While from While.prems show ?case by(fastforce intro: While.IH simp: strip_eq_While) qed auto thus ?case by auto qed lemma le_post: "c ≤ d ==> post c ≤ post d" by(induction c d rule: less_eq_acom.induct) auto subsubsection "Collecting semantics" fun step :: "state set => state set acom => state set acom" where "step S (SKIP {P}) = (SKIP {S})" | "step S (x ::= e {P}) = (x ::= e {{s'. EX s:S. s' = s(x := aval e s)}})" | "step S (c1;; c2) = step S c1;; step (post c1) c2" | "step S (IF b THEN c1 ELSE c2 {P}) = IF b THEN step {s:S. bval b s} c1 ELSE step {s:S. ¬ bval b s} c2 {post c1 ∪ post c2}" | "step S ({Inv} WHILE b DO c {P}) = {S ∪ post c} WHILE b DO (step {s:Inv. bval b s} c) {{s:Inv. ¬ bval b s}}" definition CS :: "com => state set acom" where "CS c = lfp (step UNIV) c" lemma mono2_step: "c1 ≤ c2 ==> S1 ⊆ S2 ==> step S1 c1 ≤ step S2 c2" proof(induction c1 c2 arbitrary: S1 S2 rule: less_eq_acom.induct) case 2 thus ?case by fastforce next case 3 thus ?case by(simp add: le_post) next case 4 thus ?case by(simp add: subset_iff)(metis le_post set_mp)+ next case 5 thus ?case by(simp add: subset_iff) (metis le_post set_mp) qed auto lemma mono_step: "mono (step S)" by(blast intro: monoI mono2_step) lemma strip_step: "strip(step S c) = strip c" by (induction c arbitrary: S) auto lemma lfp_cs_unfold: "lfp (step S) c = step S (lfp (step S) c)" apply(rule lfp_unfold[OF _ mono_step]) apply(simp add: strip_step) done lemma CS_unfold: "CS c = step UNIV (CS c)" by (metis CS_def lfp_cs_unfold) lemma strip_CS[simp]: "strip(CS c) = c" by(simp add: CS_def index_lfp[simplified]) end