tm2: comparison thys/Hoare

equal deleted inserted replaced

-:f8b2bf858caf
+:457240e42972
 (val name = @{binding "fwd"}
 val description = "Theorems for fwd derivation of seperation implication")
 *}
 setup {* StepRules.setup *}
 setup {* FwdRules.setup *}
 method_setup prune =
 {* Scan.succeed (SIMPLE_METHOD' o (K (K prune_params_tac))) *}
 "pruning parameters"
 | TSeq tpg tpg
 | TLocal "nat \<Rightarrow> tpg"
 notation TLocal (binder "TL " 10)
-abbreviation tprog_instr :: "tm_inst \<Rightarrow> tpg" ("\<guillemotright> _" [61] 61)
+abbreviation
+tprog_instr :: "tm_inst \<Rightarrow> tpg" ("\<guillemotright> _" [61] 61)
 where "\<guillemotright> i \<equiv> TInstr i"
-abbreviation tprog_seq :: "tpg \<Rightarrow> tpg \<Rightarrow> tpg" (infixr ";" 52)
+abbreviation tprog_seq ::
+"tpg \<Rightarrow> tpg \<Rightarrow> tpg" (infixr ";" 52)
 where "c1 ; c2 \<equiv> TSeq c1 c2"
-definition "sg e = (\<lambda> s. s = e)"
+definition "sg e = (\<lambda>s. s = e)"
 type_synonym tassert = "tresource set \<Rightarrow> bool"
-abbreviation t_hoare :: "tassert \<Rightarrow> tassert  \<Rightarrow> tassert \<Rightarrow> bool" ("(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50)
+abbreviation
-where "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace> == sep_exec.Hoare_gen tstep trset_of p c q"
+t_hoare :: "tassert \<Rightarrow> tassert  \<Rightarrow> tassert \<Rightarrow> bool" ("(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50)
+where
+"\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace> == sep_exec.Hoare_gen tstep trset_of p c q"
 abbreviation it_hoare ::
 "('a::sep_algebra \<Rightarrow> tresource set \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> (tresource set \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
 ("(1_).(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50)
 where "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace> == sep_exec.IHoare tstep trset_of I P c Q"
 declare tassemble_to.simps [simp del]
 lemmas tasmp = tassemble_to.simps (2, 3, 4)
-abbreviation tasmb_to :: "nat \<Rightarrow> tpg \<Rightarrow> nat \<Rightarrow> tassert" ("_ :[ _ ]: _" [60, 60, 60] 60)
+abbreviation
-where "i :[ tpg ]: j \<equiv> tassemble_to tpg i j"
+tasmb_to :: "nat \<Rightarrow> tpg \<Rightarrow> nat \<Rightarrow> tassert" ("_ :[ _ ]: _" [60, 60, 60] 60)
+where
+"i :[ tpg ]: j \<equiv> tassemble_to tpg i j"
 lemma EXS_intro:
 assumes h: "(P x) s"
 shows "(EXS x. P(x)) s"
 by (smt h pred_ex_def sep_conj_impl)
 qed
 qed
 definition "tpg_fold tpgs = foldr TSeq (butlast tpgs) (last tpgs)"
-lemma tpg_fold_sg: "tpg_fold [tpg] = tpg"
+lemma tpg_fold_sg:
+"tpg_fold [tpg] = tpg"
 by (simp add:tpg_fold_def)
 lemma tpg_fold_cons:
 assumes h: "tpgs \<noteq> []"
 shows "tpg_fold (tpg#tpgs) = (tpg; (tpg_fold tpgs))"
 subsection {* Assertions and program logic for this assembly language *}
 definition "st l = sg (tpc_set l)"
 definition "ps p = sg (tpos_set p)"
-definition "tm a v =sg ({TM a v})"
+definition "tm a v = sg ({TM a v})"
 definition "one i = tm i Oc"
 definition "zero i= tm i Bk"
 definition "any i = (EXS v. tm i v)"
 declare trset_of.simps[simp del]
-lemma stimes_sgD: "(sg x ** q) s \<Longrightarrow> q (s - x) \<and> x \<subseteq> s"
+lemma stimes_sgD:
+"(sg x \<and>* q) s \<Longrightarrow> q (s - x) \<and> x \<subseteq> s"
 apply(erule_tac sep_conjE)
 apply(unfold set_ins_def sg_def)
-by (metis Diff_Int2 Diff_Int_distrib2 Diff_Un Diff_cancel
+by (metis Diff_Int Diff_cancel Diff_empty Un_Diff sup.cobounded1 sup_bot.left_neutral sup_commute)
-Diff_empty Diff_idemp Diff_triv Int_Diff Un_Diff
-Un_Diff_cancel inf_commute inf_idem sup_bot_right sup_commute sup_ge2)
+lemma stD:
+"(st i \<and>* r) (trset_of (ft, prog, i', pos, mem)) \<Longrightarrow> i' = i"
-lemma stD: "(st i ** r) (trset_of (ft, prog, i', pos, mem))
-\<Longrightarrow> i' = i"
 proof -
-assume "(st i ** r) (trset_of (ft, prog, i', pos, mem))"
+assume "(st i \<and>* r) (trset_of (ft, prog, i', pos, mem))"
 from stimes_sgD [OF this[unfolded st_def], unfolded trset_of.simps]
 have "tpc_set i \<subseteq> tprog_set prog \<union> tpc_set i' \<union> tpos_set pos \<union>
 tmem_set mem \<union> tfaults_set ft" by auto
 thus ?thesis
 by (unfold tpn_set_def, auto)
 qed
-lemma psD: "(ps p ** r) (trset_of (ft, prog, i', pos, mem))
+lemma psD:
-\<Longrightarrow> pos = p"
+"(ps p \<and>* r) (trset_of (ft, prog, i', pos, mem)) \<Longrightarrow> pos = p"
 proof -
 assume "(ps p ** r) (trset_of (ft, prog, i', pos, mem))"
 from stimes_sgD [OF this[unfolded ps_def], unfolded trset_of.simps]
 have "tpos_set p \<subseteq> tprog_set prog \<union> tpc_set i' \<union>
 tpos_set pos \<union> tmem_set mem \<union> tfaults_set ft"
 {TPos pos} \<union> {TM i n |i n. mem i = Some n} \<union> {TFaults ft}" by simp
 thus ?thesis by auto
 qed
 lemma t_hoare_seq:
-"\<lbrakk>\<And> i j. \<lbrace>st i ** p\<rbrace> i:[c1]:j \<lbrace>st j ** q\<rbrace>;
+assumes a1: "\<And> i j. \<lbrace>st i \<and>* p\<rbrace> i:[c1]:j \<lbrace>st j \<and>* q\<rbrace>"
-\<And> j k. \<lbrace>st j ** q\<rbrace> j:[c2]:k \<lbrace>st k ** r\<rbrace>\<rbrakk> \<Longrightarrow>  \<lbrace>st i ** p\<rbrace> i:[(c1 ; c2)]:k \<lbrace>st k ** r\<rbrace>"
+and     a2: "\<And> j k. \<lbrace>st j ** q\<rbrace> j:[c2]:k \<lbrace>st k ** r\<rbrace>"
-proof -
+shows "\<lbrace>st i \<and>* p\<rbrace> i:[(c1 ; c2)]:k \<lbrace>st k \<and>* r\<rbrace>"
-assume h: "\<And> i j. \<lbrace>st i ** p\<rbrace> i:[c1]:j \<lbrace>st j ** q\<rbrace>"
+proof(subst tassemble_to.simps, rule tm.code_exI)
-"\<And> j k. \<lbrace>st j ** q\<rbrace> j:[c2]:k \<lbrace>st k ** r\<rbrace>"
+fix j'
-show "\<lbrace>st i ** p\<rbrace> i:[(c1 ; c2)]:k \<lbrace>st k ** r\<rbrace>"
+show "\<lbrace>st i \<and>* p\<rbrace>  i:[ c1 ]:j' \<and>* j':[ c2 ]:k \<lbrace>st k \<and>* r\<rbrace>"
-proof(subst tassemble_to.simps, rule tm.code_exI)
+proof(rule tm.composition)
-fix j'
+from a1 show "\<lbrace>st i \<and>* p\<rbrace>  i:[ c1 ]:j' \<lbrace>st j' \<and>* q\<rbrace>" by auto
-show "\<lbrace>st i \<and>* p\<rbrace>  i :[ c1 ]: j' \<and>* j' :[ c2 ]: k \<lbrace>st k \<and>* r\<rbrace>"
+next
-proof(rule tm.composition)
+from a2 show "\<lbrace>st j' \<and>* q\<rbrace>  j':[ c2 ]:k \<lbrace>st k \<and>* r\<rbrace>" by auto
-from h(1) show "\<lbrace>st i \<and>* p\<rbrace>  i :[ c1 ]: j' \<lbrace> st j' \<and>* q \<rbrace>" by auto
-next
-from h(2) show "\<lbrace>st j' \<and>* q\<rbrace>  j' :[ c2 ]: k \<lbrace>st k \<and>* r\<rbrace>" by auto
-qed
 qed
 qed
 lemma t_hoare_seq1:
-"\<lbrakk>\<And>j'. \<lbrace>st i ** p\<rbrace> i:[c1]:j' \<lbrace>st j' ** q\<rbrace>;
+assumes a1: "\<And>j'. \<lbrace>st i \<and>* p\<rbrace> i:[c1]:j' \<lbrace>st j' \<and>* q\<rbrace>"
-\<And>j'. \<lbrace>st j' ** q\<rbrace> j':[c2]:k \<lbrace>st k' ** r\<rbrace>\<rbrakk> \<Longrightarrow>
+assumes a2: "\<And>j'. \<lbrace>st j' \<and>* q\<rbrace> j':[c2]:k \<lbrace>st k' \<and>* r\<rbrace>"
-\<lbrace>st i ** p\<rbrace> i:[(c1 ; c2)]:k \<lbrace>st k' ** r\<rbrace>"
+shows "\<lbrace>st i \<and>* p\<rbrace> i:[(c1 ; c2)]:k \<lbrace>st k' \<and>* r\<rbrace>"
-proof -
+proof(subst tassemble_to.simps, rule tm.code_exI)
-assume h: "\<And>j'. \<lbrace>st i \<and>* p\<rbrace>  i :[ c1 ]: j' \<lbrace>st j' \<and>* q\<rbrace>"
+fix j'
-"\<And>j'. \<lbrace>st j' \<and>* q\<rbrace>  j' :[ c2 ]: k \<lbrace>st k' \<and>* r\<rbrace>"
+show "\<lbrace>st i \<and>* p\<rbrace>  i:[ c1 ]:j' \<and>* j':[ c2 ]:k \<lbrace>st k' \<and>* r\<rbrace>"
-show "\<lbrace>st i \<and>* p\<rbrace>  i :[ (c1 ; c2) ]: k \<lbrace>st k' \<and>* r\<rbrace>"
+proof(rule tm.composition)
-proof(subst tassemble_to.simps, rule tm.code_exI)
+from a1 show "\<lbrace>st i \<and>* p\<rbrace>  i:[ c1 ]:j' \<lbrace>st j' \<and>* q\<rbrace>" by auto
-fix j'
+next
-show "\<lbrace>st i \<and>* p\<rbrace>  i :[ c1 ]: j' \<and>* j' :[ c2 ]: k \<lbrace>st k' \<and>* r\<rbrace>"
+from a2 show " \<lbrace>st j' \<and>* q\<rbrace>  j':[ c2 ]:k \<lbrace>st k' \<and>* r\<rbrace>" by auto
-proof(rule tm.composition)
-from h(1) show "\<lbrace>st i \<and>* p\<rbrace>  i :[ c1 ]: j' \<lbrace> st j' \<and>* q \<rbrace>" by auto
-next
-from h(2) show " \<lbrace>st j' \<and>* q\<rbrace>  j' :[ c2 ]: k \<lbrace>st k' \<and>* r\<rbrace>" by auto
-qed
 qed
 qed
 lemma t_hoare_seq2:
 assumes h: "\<And>j. \<lbrace>st i ** p\<rbrace> i:[c1]:j \<lbrace>st k' \<and>* r\<rbrace>"
 shows "\<lbrace>st i ** p\<rbrace> i:[(c1 ; c2)]:j \<lbrace>st k' ** r\<rbrace>"
 apply (unfold tassemble_to.simps, rule tm.code_exI)
 by (rule tm.code_extension, rule h)
 lemma t_hoare_local:
 assumes h: "(\<And>l. \<lbrace>st i \<and>* p\<rbrace>  i :[ c l ]: j \<lbrace>st k \<and>* q\<rbrace>)"
 shows "\<lbrace>st i ** p\<rbrace> i:[TLocal c]:j \<lbrace>st k ** q\<rbrace>" using h
 by (unfold tassemble_to.simps, intro tm.code_exI, simp)
 lemma t_hoare_label:
-"(\<And>l. l = i \<Longrightarrow> \<lbrace>st l \<and>* p\<rbrace>  l :[ c l ]: j \<lbrace>st k \<and>* q\<rbrace>) \<Longrightarrow>
+assumes "\<And>l. l = i \<Longrightarrow> \<lbrace>st l \<and>* p\<rbrace>  l:[ c l ]:j \<lbrace>st k \<and>* q\<rbrace>"
-\<lbrace>st i \<and>* p \<rbrace>
+shows "\<lbrace>st i \<and>* p\<rbrace> i:[(TLabel l; c l)]:j \<lbrace>st k \<and>* q\<rbrace>"
-i:[(TLabel l; c l)]:j
+using assms
-\<lbrace>st k \<and>* q\<rbrace>"
 by (unfold tassemble_to.simps, intro tm.code_exI tm.code_condI, clarify, auto)
 primrec t_split_cmd :: "tpg \<Rightarrow> (tpg \<times> tpg option)"
 where "t_split_cmd (\<guillemotright>inst) = (\<guillemotright>inst, None)" |
 "t_split_cmd (TLabel l) = (TLabel l, None)" |
 "t_split_cmd (TSeq c1 c2) = (case (t_split_cmd c2) of
 (c21, Some c22) \<Rightarrow> (TSeq c1 c21, Some c22) |
 (c21, None) \<Rightarrow> (c1, Some c21))" |
 "t_split_cmd (TLocal c) = (TLocal c, None)"
-definition "t_last_cmd tpg = (snd (t_split_cmd tpg))"
+definition "t_last_cmd tpg = snd (t_split_cmd tpg)"
 declare t_last_cmd_def [simp]
-definition "t_blast_cmd tpg = (fst (t_split_cmd tpg))"
+definition "t_blast_cmd tpg = fst (t_split_cmd tpg)"
 declare t_blast_cmd_def [simp]
-lemma "t_last_cmd (c1; c2; (TLabel l)) = (Some (TLabel l))"
+lemma "t_last_cmd (c1; c2; TLabel l) = Some (TLabel l)"
 by simp
 lemma "t_blast_cmd (c1; c2; TLabel l) = (c1; c2)"
 by simp
 lemma t_split_cmd_eq:
 assumes "t_split_cmd c = (c1, Some c2)"
-shows "(i:[c]:j) = (i:[(c1; c2)]:j)"
+shows "i:[c]:j = i:[(c1; c2)]:j"
 using assms
 proof(induct c arbitrary: c1 c2 i j)
 case (TSeq cx cy)
 from `t_split_cmd (cx ; cy) = (c1, Some c2)`
 show ?case
 by (simp add:pred_ex_def, default, auto)
 qed
 qed auto
 lemma t_hoare_label_last_pre:
-fixes l
 assumes h1: "t_split_cmd c = (c', Some (TLabel l))"
 and h2: "l = j \<Longrightarrow> \<lbrace>p\<rbrace> i:[c']:j \<lbrace>q\<rbrace>"
 shows "\<lbrace>p\<rbrace> i:[c]:j \<lbrace>q\<rbrace>"
 by (unfold t_split_cmd_eq[OF h1],
 simp only:tassemble_to.simps sep_conj_cond,
 intro tm.code_exI tm.code_condI, insert h2, auto)
 lemma t_hoare_label_last:
-fixes l
 assumes h1: "t_last_cmd c = Some (TLabel l)"
 and h2: "l = j \<Longrightarrow> \<lbrace>p\<rbrace> i:[t_blast_cmd c]:j \<lbrace>q\<rbrace>"
 shows "\<lbrace>p\<rbrace> i:[c]:j \<lbrace>q\<rbrace>"
 proof -
 have "t_split_cmd c = (t_blast_cmd c, t_last_cmd c)"

changeset 12	457240e42972
parent 11	f8b2bf858caf
child 13	e6e412406a2d