# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1395925587 0
# Node ID 457240e429724fbc82c38f1668a15e7ad6ba3eb1
# Parent  f8b2bf858caf4fc5a5b18e6169ee876ada13547a
some minor changes

diff -r f8b2bf858caf -r 457240e42972 thys/Hoare_gen.thy
--- a/thys/Hoare_gen.thy	Thu Mar 27 11:50:37 2014 +0000
+++ b/thys/Hoare_gen.thy	Thu Mar 27 13:06:27 2014 +0000
@@ -30,20 +30,26 @@
 
 lemmas sep_conj_cond = sep_conj_cond1 sep_conj_cond2 sep_conj_cond3
 
-lemma cond_true_eq[simp]: "<True> = \<box>"
+lemma cond_true_eq [simp]: 
+  "<True> = \<box>"
   by(unfold sep_empty_def pasrt_def, auto)
 
-lemma cond_true_eq1: "(<True> \<and>* p) = p"
-  by(simp)
+lemma cond_true_eq1: 
+  "(<True> \<and>* p) = p"
+  by (simp)
 
-lemma false_simp [simp]: "<False> = sep_false" (* move *)
+lemma cond_true_eq2: 
+  "(p \<and>* <True>) = p"
+  by simp
+
+lemma false_simp [simp]: 
+  "<False> = sep_false" (* move *)
   by (simp add:pasrt_def)
 
-lemma cond_true_eq2: "(p \<and>* <True>) = p"
-  by simp
-
-lemma condD: "(<b> \<and>* r) s \<Longrightarrow> b \<and> r s" 
-by (unfold sep_conj_def pasrt_def, auto)
+lemma condD: 
+  "(<b> \<and>* r) s \<Longrightarrow> b \<and> r s" 
+unfolding sep_conj_def pasrt_def
+by auto
 
 locale sep_exec = 
    fixes step :: "'conf \<Rightarrow> 'conf"
@@ -189,8 +195,8 @@
 
 lemma hoare_sep_false: 
   "\<lbrace>sep_false\<rbrace> c \<lbrace>q\<rbrace>" 
-  by(unfold Hoare_gen_def, clarify, simp)
-
+unfolding Hoare_gen_def
+by auto
 
 lemma pred_exI: 
   assumes "(P(x) \<and>* r) s"
diff -r f8b2bf858caf -r 457240e42972 thys/Hoare_tm.thy
--- a/thys/Hoare_tm.thy	Thu Mar 27 11:50:37 2014 +0000
+++ b/thys/Hoare_tm.thy	Thu Mar 27 13:06:27 2014 +0000
@@ -25,7 +25,6 @@
 *}
 
 setup {* StepRules.setup *}
-
 setup {* FwdRules.setup *}
 
 method_setup prune = 
@@ -128,18 +127,22 @@
 
 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)
-  where "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace> == sep_exec.Hoare_gen tstep trset_of p c q"
+abbreviation 
+  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"
@@ -165,8 +168,10 @@
 
 lemmas tasmp = tassemble_to.simps (2, 3, 4)
 
-abbreviation tasmb_to :: "nat \<Rightarrow> tpg \<Rightarrow> nat \<Rightarrow> tassert" ("_ :[ _ ]: _" [60, 60, 60] 60)
-  where "i :[ tpg ]: j \<equiv> tassemble_to tpg i j"
+abbreviation 
+  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"
@@ -202,7 +207,8 @@
 
 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: 
@@ -352,24 +358,23 @@
 
 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 
-    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 ** r) (trset_of (ft, prog, i', pos, mem))
-       \<Longrightarrow> i' = i"
+  by (metis Diff_Int Diff_cancel Diff_empty Un_Diff sup.cobounded1 sup_bot.left_neutral sup_commute)
+  
+lemma stD: 
+  "(st i \<and>* 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
@@ -377,8 +382,8 @@
     by (unfold tpn_set_def, auto)
 qed
 
-lemma psD: "(ps p ** r) (trset_of (ft, prog, i', pos, mem))
-       \<Longrightarrow> pos = p"
+lemma psD: 
+  "(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]
@@ -408,45 +413,37 @@
 qed
 
 lemma t_hoare_seq: 
-  "\<lbrakk>\<And> i j. \<lbrace>st i ** p\<rbrace> i:[c1]:j \<lbrace>st j ** 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>"
-proof -
-  assume h: "\<And> i j. \<lbrace>st i ** p\<rbrace> i:[c1]:j \<lbrace>st j ** q\<rbrace>" 
-            "\<And> j k. \<lbrace>st j ** q\<rbrace> j:[c2]:k \<lbrace>st k ** r\<rbrace>"
-  show "\<lbrace>st i ** p\<rbrace> i:[(c1 ; c2)]:k \<lbrace>st k ** r\<rbrace>"
-  proof(subst tassemble_to.simps, rule tm.code_exI)
-    fix j'
-    show "\<lbrace>st i \<and>* p\<rbrace>  i :[ c1 ]: j' \<and>* j' :[ c2 ]: k \<lbrace>st k \<and>* r\<rbrace>"
-    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
+  assumes a1: "\<And> i j. \<lbrace>st i \<and>* p\<rbrace> i:[c1]:j \<lbrace>st j \<and>* q\<rbrace>"
+  and     a2: "\<And> j k. \<lbrace>st j ** q\<rbrace> j:[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(subst tassemble_to.simps, rule tm.code_exI)
+  fix j'
+  show "\<lbrace>st i \<and>* p\<rbrace>  i:[ c1 ]:j' \<and>* j':[ c2 ]:k \<lbrace>st k \<and>* r\<rbrace>"
+  proof(rule tm.composition)
+    from a1 show "\<lbrace>st i \<and>* p\<rbrace>  i:[ c1 ]:j' \<lbrace>st j' \<and>* q\<rbrace>" by auto
+  next
+    from a2 show "\<lbrace>st j' \<and>* q\<rbrace>  j':[ c2 ]:k \<lbrace>st k \<and>* r\<rbrace>" by auto
   qed
 qed
 
+
 lemma t_hoare_seq1:
-   "\<lbrakk>\<And>j'. \<lbrace>st i ** p\<rbrace> i:[c1]:j' \<lbrace>st j' ** q\<rbrace>;
-    \<And>j'. \<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>"
-proof -
-  assume h: "\<And>j'. \<lbrace>st i \<and>* p\<rbrace>  i :[ c1 ]: j' \<lbrace>st j' \<and>* q\<rbrace>" 
-            "\<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 ; c2) ]: k \<lbrace>st k' \<and>* r\<rbrace>"
-  proof(subst tassemble_to.simps, rule tm.code_exI)
-    fix j'
-    show "\<lbrace>st i \<and>* p\<rbrace>  i :[ c1 ]: j' \<and>* j' :[ c2 ]: k \<lbrace>st k' \<and>* r\<rbrace>"
-    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
+  assumes a1: "\<And>j'. \<lbrace>st i \<and>* p\<rbrace> i:[c1]:j' \<lbrace>st j' \<and>* q\<rbrace>"
+  assumes a2: "\<And>j'. \<lbrace>st j' \<and>* q\<rbrace> j':[c2]:k \<lbrace>st k' \<and>* r\<rbrace>"
+  shows "\<lbrace>st i \<and>* p\<rbrace> i:[(c1 ; c2)]:k \<lbrace>st k' \<and>* r\<rbrace>"
+proof(subst tassemble_to.simps, rule tm.code_exI)
+  fix j'
+  show "\<lbrace>st i \<and>* p\<rbrace>  i:[ c1 ]:j' \<and>* j':[ c2 ]:k \<lbrace>st k' \<and>* r\<rbrace>"
+  proof(rule tm.composition)
+    from a1 show "\<lbrace>st i \<and>* p\<rbrace>  i:[ c1 ]:j' \<lbrace>st j' \<and>* q\<rbrace>" by auto
+  next
+    from a2 show " \<lbrace>st j' \<and>* q\<rbrace>  j':[ c2 ]:k \<lbrace>st k' \<and>* r\<rbrace>" by auto
   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>"
+  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)
 
@@ -456,10 +453,9 @@
   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>
-             \<lbrace>st i \<and>* p \<rbrace> 
-               i:[(TLabel l; c l)]:j
-             \<lbrace>st k \<and>* q\<rbrace>"
+  assumes "\<And>l. l = i \<Longrightarrow> \<lbrace>st l \<and>* p\<rbrace>  l:[ c l ]:j \<lbrace>st k \<and>* q\<rbrace>"
+  shows "\<lbrace>st i \<and>* p\<rbrace> i:[(TLabel l; c l)]:j \<lbrace>st k \<and>* q\<rbrace>"
+using assms
 by (unfold tassemble_to.simps, intro tm.code_exI tm.code_condI, clarify, auto)
 
 primrec t_split_cmd :: "tpg \<Rightarrow> (tpg \<times> tpg option)"
@@ -470,15 +466,15 @@
                                       (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)"
@@ -486,7 +482,7 @@
 
 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)
@@ -505,7 +501,6 @@
 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>"
@@ -514,7 +509,6 @@
     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>"