src/HOL/Hoare_Parallel/RG_Hoare.thy
 author blanchet Tue Nov 07 15:16:42 2017 +0100 (20 months ago) changeset 67022 49309fe530fd parent 62343 24106dc44def child 67443 3abf6a722518 permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
```     1 section \<open>The Proof System\<close>
```
```     2
```
```     3 theory RG_Hoare imports RG_Tran begin
```
```     4
```
```     5 subsection \<open>Proof System for Component Programs\<close>
```
```     6
```
```     7 declare Un_subset_iff [simp del] sup.bounded_iff [simp del]
```
```     8
```
```     9 definition stable :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" where
```
```    10   "stable \<equiv> \<lambda>f g. (\<forall>x y. x \<in> f \<longrightarrow> (x, y) \<in> g \<longrightarrow> y \<in> f)"
```
```    11
```
```    12 inductive
```
```    13   rghoare :: "['a com, 'a set, ('a \<times> 'a) set, ('a \<times> 'a) set, 'a set] \<Rightarrow> bool"
```
```    14     ("\<turnstile> _ sat [_, _, _, _]" [60,0,0,0,0] 45)
```
```    15 where
```
```    16   Basic: "\<lbrakk> pre \<subseteq> {s. f s \<in> post}; {(s,t). s \<in> pre \<and> (t=f s \<or> t=s)} \<subseteq> guar;
```
```    17             stable pre rely; stable post rely \<rbrakk>
```
```    18            \<Longrightarrow> \<turnstile> Basic f sat [pre, rely, guar, post]"
```
```    19
```
```    20 | Seq: "\<lbrakk> \<turnstile> P sat [pre, rely, guar, mid]; \<turnstile> Q sat [mid, rely, guar, post] \<rbrakk>
```
```    21            \<Longrightarrow> \<turnstile> Seq P Q sat [pre, rely, guar, post]"
```
```    22
```
```    23 | Cond: "\<lbrakk> stable pre rely; \<turnstile> P1 sat [pre \<inter> b, rely, guar, post];
```
```    24            \<turnstile> P2 sat [pre \<inter> -b, rely, guar, post]; \<forall>s. (s,s)\<in>guar \<rbrakk>
```
```    25           \<Longrightarrow> \<turnstile> Cond b P1 P2 sat [pre, rely, guar, post]"
```
```    26
```
```    27 | While: "\<lbrakk> stable pre rely; (pre \<inter> -b) \<subseteq> post; stable post rely;
```
```    28             \<turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s,s)\<in>guar \<rbrakk>
```
```    29           \<Longrightarrow> \<turnstile> While b P sat [pre, rely, guar, post]"
```
```    30
```
```    31 | Await: "\<lbrakk> stable pre rely; stable post rely;
```
```    32             \<forall>V. \<turnstile> P sat [pre \<inter> b \<inter> {V}, {(s, t). s = t},
```
```    33                 UNIV, {s. (V, s) \<in> guar} \<inter> post] \<rbrakk>
```
```    34            \<Longrightarrow> \<turnstile> Await b P sat [pre, rely, guar, post]"
```
```    35
```
```    36 | Conseq: "\<lbrakk> pre \<subseteq> pre'; rely \<subseteq> rely'; guar' \<subseteq> guar; post' \<subseteq> post;
```
```    37              \<turnstile> P sat [pre', rely', guar', post'] \<rbrakk>
```
```    38             \<Longrightarrow> \<turnstile> P sat [pre, rely, guar, post]"
```
```    39
```
```    40 definition Pre :: "'a rgformula \<Rightarrow> 'a set" where
```
```    41   "Pre x \<equiv> fst(snd x)"
```
```    42
```
```    43 definition Post :: "'a rgformula \<Rightarrow> 'a set" where
```
```    44   "Post x \<equiv> snd(snd(snd(snd x)))"
```
```    45
```
```    46 definition Rely :: "'a rgformula \<Rightarrow> ('a \<times> 'a) set" where
```
```    47   "Rely x \<equiv> fst(snd(snd x))"
```
```    48
```
```    49 definition Guar :: "'a rgformula \<Rightarrow> ('a \<times> 'a) set" where
```
```    50   "Guar x \<equiv> fst(snd(snd(snd x)))"
```
```    51
```
```    52 definition Com :: "'a rgformula \<Rightarrow> 'a com" where
```
```    53   "Com x \<equiv> fst x"
```
```    54
```
```    55 subsection \<open>Proof System for Parallel Programs\<close>
```
```    56
```
```    57 type_synonym 'a par_rgformula =
```
```    58   "('a rgformula) list \<times> 'a set \<times> ('a \<times> 'a) set \<times> ('a \<times> 'a) set \<times> 'a set"
```
```    59
```
```    60 inductive
```
```    61   par_rghoare :: "('a rgformula) list \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set \<Rightarrow> bool"
```
```    62     ("\<turnstile> _ SAT [_, _, _, _]" [60,0,0,0,0] 45)
```
```    63 where
```
```    64   Parallel:
```
```    65   "\<lbrakk> \<forall>i<length xs. rely \<union> (\<Union>j\<in>{j. j<length xs \<and> j\<noteq>i}. Guar(xs!j)) \<subseteq> Rely(xs!i);
```
```    66     (\<Union>j\<in>{j. j<length xs}. Guar(xs!j)) \<subseteq> guar;
```
```    67      pre \<subseteq> (\<Inter>i\<in>{i. i<length xs}. Pre(xs!i));
```
```    68     (\<Inter>i\<in>{i. i<length xs}. Post(xs!i)) \<subseteq> post;
```
```    69     \<forall>i<length xs. \<turnstile> Com(xs!i) sat [Pre(xs!i),Rely(xs!i),Guar(xs!i),Post(xs!i)] \<rbrakk>
```
```    70    \<Longrightarrow>  \<turnstile> xs SAT [pre, rely, guar, post]"
```
```    71
```
```    72 section \<open>Soundness\<close>
```
```    73
```
```    74 subsubsection \<open>Some previous lemmas\<close>
```
```    75
```
```    76 lemma tl_of_assum_in_assum:
```
```    77   "(P, s) # (P, t) # xs \<in> assum (pre, rely) \<Longrightarrow> stable pre rely
```
```    78   \<Longrightarrow> (P, t) # xs \<in> assum (pre, rely)"
```
```    79 apply(simp add:assum_def)
```
```    80 apply clarify
```
```    81 apply(rule conjI)
```
```    82  apply(erule_tac x=0 in allE)
```
```    83  apply(simp (no_asm_use)only:stable_def)
```
```    84  apply(erule allE,erule allE,erule impE,assumption,erule mp)
```
```    85  apply(simp add:Env)
```
```    86 apply clarify
```
```    87 apply(erule_tac x="Suc i" in allE)
```
```    88 apply simp
```
```    89 done
```
```    90
```
```    91 lemma etran_in_comm:
```
```    92   "(P, t) # xs \<in> comm(guar, post) \<Longrightarrow> (P, s) # (P, t) # xs \<in> comm(guar, post)"
```
```    93 apply(simp add:comm_def)
```
```    94 apply clarify
```
```    95 apply(case_tac i,simp+)
```
```    96 done
```
```    97
```
```    98 lemma ctran_in_comm:
```
```    99   "\<lbrakk>(s, s) \<in> guar; (Q, s) # xs \<in> comm(guar, post)\<rbrakk>
```
```   100   \<Longrightarrow> (P, s) # (Q, s) # xs \<in> comm(guar, post)"
```
```   101 apply(simp add:comm_def)
```
```   102 apply clarify
```
```   103 apply(case_tac i,simp+)
```
```   104 done
```
```   105
```
```   106 lemma takecptn_is_cptn [rule_format, elim!]:
```
```   107   "\<forall>j. c \<in> cptn \<longrightarrow> take (Suc j) c \<in> cptn"
```
```   108 apply(induct "c")
```
```   109  apply(force elim: cptn.cases)
```
```   110 apply clarify
```
```   111 apply(case_tac j)
```
```   112  apply simp
```
```   113  apply(rule CptnOne)
```
```   114 apply simp
```
```   115 apply(force intro:cptn.intros elim:cptn.cases)
```
```   116 done
```
```   117
```
```   118 lemma dropcptn_is_cptn [rule_format,elim!]:
```
```   119   "\<forall>j<length c. c \<in> cptn \<longrightarrow> drop j c \<in> cptn"
```
```   120 apply(induct "c")
```
```   121  apply(force elim: cptn.cases)
```
```   122 apply clarify
```
```   123 apply(case_tac j,simp+)
```
```   124 apply(erule cptn.cases)
```
```   125   apply simp
```
```   126  apply force
```
```   127 apply force
```
```   128 done
```
```   129
```
```   130 lemma takepar_cptn_is_par_cptn [rule_format,elim]:
```
```   131   "\<forall>j. c \<in> par_cptn \<longrightarrow> take (Suc j) c \<in> par_cptn"
```
```   132 apply(induct "c")
```
```   133  apply(force elim: cptn.cases)
```
```   134 apply clarify
```
```   135 apply(case_tac j,simp)
```
```   136  apply(rule ParCptnOne)
```
```   137 apply(force intro:par_cptn.intros elim:par_cptn.cases)
```
```   138 done
```
```   139
```
```   140 lemma droppar_cptn_is_par_cptn [rule_format]:
```
```   141   "\<forall>j<length c. c \<in> par_cptn \<longrightarrow> drop j c \<in> par_cptn"
```
```   142 apply(induct "c")
```
```   143  apply(force elim: par_cptn.cases)
```
```   144 apply clarify
```
```   145 apply(case_tac j,simp+)
```
```   146 apply(erule par_cptn.cases)
```
```   147   apply simp
```
```   148  apply force
```
```   149 apply force
```
```   150 done
```
```   151
```
```   152 lemma tl_of_cptn_is_cptn: "\<lbrakk>x # xs \<in> cptn; xs \<noteq> []\<rbrakk> \<Longrightarrow> xs  \<in> cptn"
```
```   153 apply(subgoal_tac "1 < length (x # xs)")
```
```   154  apply(drule dropcptn_is_cptn,simp+)
```
```   155 done
```
```   156
```
```   157 lemma not_ctran_None [rule_format]:
```
```   158   "\<forall>s. (None, s)#xs \<in> cptn \<longrightarrow> (\<forall>i<length xs. ((None, s)#xs)!i -e\<rightarrow> xs!i)"
```
```   159 apply(induct xs,simp+)
```
```   160 apply clarify
```
```   161 apply(erule cptn.cases,simp)
```
```   162  apply simp
```
```   163  apply(case_tac i,simp)
```
```   164   apply(rule Env)
```
```   165  apply simp
```
```   166 apply(force elim:ctran.cases)
```
```   167 done
```
```   168
```
```   169 lemma cptn_not_empty [simp]:"[] \<notin> cptn"
```
```   170 apply(force elim:cptn.cases)
```
```   171 done
```
```   172
```
```   173 lemma etran_or_ctran [rule_format]:
```
```   174   "\<forall>m i. x\<in>cptn \<longrightarrow> m \<le> length x
```
```   175    \<longrightarrow> (\<forall>i. Suc i < m \<longrightarrow> \<not> x!i -c\<rightarrow> x!Suc i) \<longrightarrow> Suc i < m
```
```   176    \<longrightarrow> x!i -e\<rightarrow> x!Suc i"
```
```   177 apply(induct x,simp)
```
```   178 apply clarify
```
```   179 apply(erule cptn.cases,simp)
```
```   180  apply(case_tac i,simp)
```
```   181   apply(rule Env)
```
```   182  apply simp
```
```   183  apply(erule_tac x="m - 1" in allE)
```
```   184  apply(case_tac m,simp,simp)
```
```   185  apply(subgoal_tac "(\<forall>i. Suc i < nata \<longrightarrow> (((P, t) # xs) ! i, xs ! i) \<notin> ctran)")
```
```   186   apply force
```
```   187  apply clarify
```
```   188  apply(erule_tac x="Suc ia" in allE,simp)
```
```   189 apply(erule_tac x="0" and P="\<lambda>j. H j \<longrightarrow> (J j) \<notin> ctran" for H J in allE,simp)
```
```   190 done
```
```   191
```
```   192 lemma etran_or_ctran2 [rule_format]:
```
```   193   "\<forall>i. Suc i<length x \<longrightarrow> x\<in>cptn \<longrightarrow> (x!i -c\<rightarrow> x!Suc i \<longrightarrow> \<not> x!i -e\<rightarrow> x!Suc i)
```
```   194   \<or> (x!i -e\<rightarrow> x!Suc i \<longrightarrow> \<not> x!i -c\<rightarrow> x!Suc i)"
```
```   195 apply(induct x)
```
```   196  apply simp
```
```   197 apply clarify
```
```   198 apply(erule cptn.cases,simp)
```
```   199  apply(case_tac i,simp+)
```
```   200 apply(case_tac i,simp)
```
```   201  apply(force elim:etran.cases)
```
```   202 apply simp
```
```   203 done
```
```   204
```
```   205 lemma etran_or_ctran2_disjI1:
```
```   206   "\<lbrakk> x\<in>cptn; Suc i<length x; x!i -c\<rightarrow> x!Suc i\<rbrakk> \<Longrightarrow> \<not> x!i -e\<rightarrow> x!Suc i"
```
```   207 by(drule etran_or_ctran2,simp_all)
```
```   208
```
```   209 lemma etran_or_ctran2_disjI2:
```
```   210   "\<lbrakk> x\<in>cptn; Suc i<length x; x!i -e\<rightarrow> x!Suc i\<rbrakk> \<Longrightarrow> \<not> x!i -c\<rightarrow> x!Suc i"
```
```   211 by(drule etran_or_ctran2,simp_all)
```
```   212
```
```   213 lemma not_ctran_None2 [rule_format]:
```
```   214   "\<lbrakk> (None, s) # xs \<in>cptn; i<length xs\<rbrakk> \<Longrightarrow> \<not> ((None, s) # xs) ! i -c\<rightarrow> xs ! i"
```
```   215 apply(frule not_ctran_None,simp)
```
```   216 apply(case_tac i,simp)
```
```   217  apply(force elim:etranE)
```
```   218 apply simp
```
```   219 apply(rule etran_or_ctran2_disjI2,simp_all)
```
```   220 apply(force intro:tl_of_cptn_is_cptn)
```
```   221 done
```
```   222
```
```   223 lemma Ex_first_occurrence [rule_format]: "P (n::nat) \<longrightarrow> (\<exists>m. P m \<and> (\<forall>i<m. \<not> P i))"
```
```   224 apply(rule nat_less_induct)
```
```   225 apply clarify
```
```   226 apply(case_tac "\<forall>m. m<n \<longrightarrow> \<not> P m")
```
```   227 apply auto
```
```   228 done
```
```   229
```
```   230 lemma stability [rule_format]:
```
```   231   "\<forall>j k. x \<in> cptn \<longrightarrow> stable p rely \<longrightarrow> j\<le>k \<longrightarrow> k<length x \<longrightarrow> snd(x!j)\<in>p  \<longrightarrow>
```
```   232   (\<forall>i. (Suc i)<length x \<longrightarrow>
```
```   233           (x!i -e\<rightarrow> x!(Suc i)) \<longrightarrow> (snd(x!i), snd(x!(Suc i))) \<in> rely) \<longrightarrow>
```
```   234   (\<forall>i. j\<le>i \<and> i<k \<longrightarrow> x!i -e\<rightarrow> x!Suc i) \<longrightarrow> snd(x!k)\<in>p \<and> fst(x!j)=fst(x!k)"
```
```   235 apply(induct x)
```
```   236  apply clarify
```
```   237  apply(force elim:cptn.cases)
```
```   238 apply clarify
```
```   239 apply(erule cptn.cases,simp)
```
```   240  apply simp
```
```   241  apply(case_tac k,simp,simp)
```
```   242  apply(case_tac j,simp)
```
```   243   apply(erule_tac x=0 in allE)
```
```   244   apply(erule_tac x="nat" and P="\<lambda>j. (0\<le>j) \<longrightarrow> (J j)" for J in allE,simp)
```
```   245   apply(subgoal_tac "t\<in>p")
```
```   246    apply(subgoal_tac "(\<forall>i. i < length xs \<longrightarrow> ((P, t) # xs) ! i -e\<rightarrow> xs ! i \<longrightarrow> (snd (((P, t) # xs) ! i), snd (xs ! i)) \<in> rely)")
```
```   247     apply clarify
```
```   248     apply(erule_tac x="Suc i" and P="\<lambda>j. (H j) \<longrightarrow> (J j)\<in>etran" for H J in allE,simp)
```
```   249    apply clarify
```
```   250    apply(erule_tac x="Suc i" and P="\<lambda>j. (H j) \<longrightarrow> (J j) \<longrightarrow> (T j)\<in>rely" for H J T in allE,simp)
```
```   251   apply(erule_tac x=0 and P="\<lambda>j. (H j) \<longrightarrow> (J j)\<in>etran \<longrightarrow> T j" for H J T in allE,simp)
```
```   252   apply(simp(no_asm_use) only:stable_def)
```
```   253   apply(erule_tac x=s in allE)
```
```   254   apply(erule_tac x=t in allE)
```
```   255   apply simp
```
```   256   apply(erule mp)
```
```   257   apply(erule mp)
```
```   258   apply(rule Env)
```
```   259  apply simp
```
```   260  apply(erule_tac x="nata" in allE)
```
```   261  apply(erule_tac x="nat" and P="\<lambda>j. (s\<le>j) \<longrightarrow> (J j)" for s J in allE,simp)
```
```   262  apply(subgoal_tac "(\<forall>i. i < length xs \<longrightarrow> ((P, t) # xs) ! i -e\<rightarrow> xs ! i \<longrightarrow> (snd (((P, t) # xs) ! i), snd (xs ! i)) \<in> rely)")
```
```   263   apply clarify
```
```   264   apply(erule_tac x="Suc i" and P="\<lambda>j. (H j) \<longrightarrow> (J j)\<in>etran" for H J in allE,simp)
```
```   265  apply clarify
```
```   266  apply(erule_tac x="Suc i" and P="\<lambda>j. (H j) \<longrightarrow> (J j) \<longrightarrow> (T j)\<in>rely" for H J T in allE,simp)
```
```   267 apply(case_tac k,simp,simp)
```
```   268 apply(case_tac j)
```
```   269  apply(erule_tac x=0 and P="\<lambda>j. (H j) \<longrightarrow> (J j)\<in>etran" for H J in allE,simp)
```
```   270  apply(erule etran.cases,simp)
```
```   271 apply(erule_tac x="nata" in allE)
```
```   272 apply(erule_tac x="nat" and P="\<lambda>j. (s\<le>j) \<longrightarrow> (J j)" for s J in allE,simp)
```
```   273 apply(subgoal_tac "(\<forall>i. i < length xs \<longrightarrow> ((Q, t) # xs) ! i -e\<rightarrow> xs ! i \<longrightarrow> (snd (((Q, t) # xs) ! i), snd (xs ! i)) \<in> rely)")
```
```   274  apply clarify
```
```   275  apply(erule_tac x="Suc i" and P="\<lambda>j. (H j) \<longrightarrow> (J j)\<in>etran" for H J in allE,simp)
```
```   276 apply clarify
```
```   277 apply(erule_tac x="Suc i" and P="\<lambda>j. (H j) \<longrightarrow> (J j) \<longrightarrow> (T j)\<in>rely" for H J T in allE,simp)
```
```   278 done
```
```   279
```
```   280 subsection \<open>Soundness of the System for Component Programs\<close>
```
```   281
```
```   282 subsubsection \<open>Soundness of the Basic rule\<close>
```
```   283
```
```   284 lemma unique_ctran_Basic [rule_format]:
```
```   285   "\<forall>s i. x \<in> cptn \<longrightarrow> x ! 0 = (Some (Basic f), s) \<longrightarrow>
```
```   286   Suc i<length x \<longrightarrow> x!i -c\<rightarrow> x!Suc i \<longrightarrow>
```
```   287   (\<forall>j. Suc j<length x \<longrightarrow> i\<noteq>j \<longrightarrow> x!j -e\<rightarrow> x!Suc j)"
```
```   288 apply(induct x,simp)
```
```   289 apply simp
```
```   290 apply clarify
```
```   291 apply(erule cptn.cases,simp)
```
```   292  apply(case_tac i,simp+)
```
```   293  apply clarify
```
```   294  apply(case_tac j,simp)
```
```   295   apply(rule Env)
```
```   296  apply simp
```
```   297 apply clarify
```
```   298 apply simp
```
```   299 apply(case_tac i)
```
```   300  apply(case_tac j,simp,simp)
```
```   301  apply(erule ctran.cases,simp_all)
```
```   302  apply(force elim: not_ctran_None)
```
```   303 apply(ind_cases "((Some (Basic f), sa), Q, t) \<in> ctran" for sa Q t)
```
```   304 apply simp
```
```   305 apply(drule_tac i=nat in not_ctran_None,simp)
```
```   306 apply(erule etranE,simp)
```
```   307 done
```
```   308
```
```   309 lemma exists_ctran_Basic_None [rule_format]:
```
```   310   "\<forall>s i. x \<in> cptn \<longrightarrow> x ! 0 = (Some (Basic f), s)
```
```   311   \<longrightarrow> i<length x \<longrightarrow> fst(x!i)=None \<longrightarrow> (\<exists>j<i. x!j -c\<rightarrow> x!Suc j)"
```
```   312 apply(induct x,simp)
```
```   313 apply simp
```
```   314 apply clarify
```
```   315 apply(erule cptn.cases,simp)
```
```   316  apply(case_tac i,simp,simp)
```
```   317  apply(erule_tac x=nat in allE,simp)
```
```   318  apply clarify
```
```   319  apply(rule_tac x="Suc j" in exI,simp,simp)
```
```   320 apply clarify
```
```   321 apply(case_tac i,simp,simp)
```
```   322 apply(rule_tac x=0 in exI,simp)
```
```   323 done
```
```   324
```
```   325 lemma Basic_sound:
```
```   326   " \<lbrakk>pre \<subseteq> {s. f s \<in> post}; {(s, t). s \<in> pre \<and> t = f s} \<subseteq> guar;
```
```   327   stable pre rely; stable post rely\<rbrakk>
```
```   328   \<Longrightarrow> \<Turnstile> Basic f sat [pre, rely, guar, post]"
```
```   329 apply(unfold com_validity_def)
```
```   330 apply clarify
```
```   331 apply(simp add:comm_def)
```
```   332 apply(rule conjI)
```
```   333  apply clarify
```
```   334  apply(simp add:cp_def assum_def)
```
```   335  apply clarify
```
```   336  apply(frule_tac j=0 and k=i and p=pre in stability)
```
```   337        apply simp_all
```
```   338    apply(erule_tac x=ia in allE,simp)
```
```   339   apply(erule_tac i=i and f=f in unique_ctran_Basic,simp_all)
```
```   340  apply(erule subsetD,simp)
```
```   341  apply(case_tac "x!i")
```
```   342  apply clarify
```
```   343  apply(drule_tac s="Some (Basic f)" in sym,simp)
```
```   344  apply(thin_tac "\<forall>j. H j" for H)
```
```   345  apply(force elim:ctran.cases)
```
```   346 apply clarify
```
```   347 apply(simp add:cp_def)
```
```   348 apply clarify
```
```   349 apply(frule_tac i="length x - 1" and f=f in exists_ctran_Basic_None,simp+)
```
```   350   apply(case_tac x,simp+)
```
```   351   apply(rule last_fst_esp,simp add:last_length)
```
```   352  apply (case_tac x,simp+)
```
```   353 apply(simp add:assum_def)
```
```   354 apply clarify
```
```   355 apply(frule_tac j=0 and k="j" and p=pre in stability)
```
```   356       apply simp_all
```
```   357   apply(erule_tac x=i in allE,simp)
```
```   358  apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all)
```
```   359 apply(case_tac "x!j")
```
```   360 apply clarify
```
```   361 apply simp
```
```   362 apply(drule_tac s="Some (Basic f)" in sym,simp)
```
```   363 apply(case_tac "x!Suc j",simp)
```
```   364 apply(rule ctran.cases,simp)
```
```   365 apply(simp_all)
```
```   366 apply(drule_tac c=sa in subsetD,simp)
```
```   367 apply clarify
```
```   368 apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all)
```
```   369  apply(case_tac x,simp+)
```
```   370  apply(erule_tac x=i in allE)
```
```   371 apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all)
```
```   372   apply arith+
```
```   373 apply(case_tac x)
```
```   374 apply(simp add:last_length)+
```
```   375 done
```
```   376
```
```   377 subsubsection\<open>Soundness of the Await rule\<close>
```
```   378
```
```   379 lemma unique_ctran_Await [rule_format]:
```
```   380   "\<forall>s i. x \<in> cptn \<longrightarrow> x ! 0 = (Some (Await b c), s) \<longrightarrow>
```
```   381   Suc i<length x \<longrightarrow> x!i -c\<rightarrow> x!Suc i \<longrightarrow>
```
```   382   (\<forall>j. Suc j<length x \<longrightarrow> i\<noteq>j \<longrightarrow> x!j -e\<rightarrow> x!Suc j)"
```
```   383 apply(induct x,simp+)
```
```   384 apply clarify
```
```   385 apply(erule cptn.cases,simp)
```
```   386  apply(case_tac i,simp+)
```
```   387  apply clarify
```
```   388  apply(case_tac j,simp)
```
```   389   apply(rule Env)
```
```   390  apply simp
```
```   391 apply clarify
```
```   392 apply simp
```
```   393 apply(case_tac i)
```
```   394  apply(case_tac j,simp,simp)
```
```   395  apply(erule ctran.cases,simp_all)
```
```   396  apply(force elim: not_ctran_None)
```
```   397 apply(ind_cases "((Some (Await b c), sa), Q, t) \<in> ctran" for sa Q t,simp)
```
```   398 apply(drule_tac i=nat in not_ctran_None,simp)
```
```   399 apply(erule etranE,simp)
```
```   400 done
```
```   401
```
```   402 lemma exists_ctran_Await_None [rule_format]:
```
```   403   "\<forall>s i.  x \<in> cptn \<longrightarrow> x ! 0 = (Some (Await b c), s)
```
```   404   \<longrightarrow> i<length x \<longrightarrow> fst(x!i)=None \<longrightarrow> (\<exists>j<i. x!j -c\<rightarrow> x!Suc j)"
```
```   405 apply(induct x,simp+)
```
```   406 apply clarify
```
```   407 apply(erule cptn.cases,simp)
```
```   408  apply(case_tac i,simp+)
```
```   409  apply(erule_tac x=nat in allE,simp)
```
```   410  apply clarify
```
```   411  apply(rule_tac x="Suc j" in exI,simp,simp)
```
```   412 apply clarify
```
```   413 apply(case_tac i,simp,simp)
```
```   414 apply(rule_tac x=0 in exI,simp)
```
```   415 done
```
```   416
```
```   417 lemma Star_imp_cptn:
```
```   418   "(P, s) -c*\<rightarrow> (R, t) \<Longrightarrow> \<exists>l \<in> cp P s. (last l)=(R, t)
```
```   419   \<and> (\<forall>i. Suc i<length l \<longrightarrow> l!i -c\<rightarrow> l!Suc i)"
```
```   420 apply (erule converse_rtrancl_induct2)
```
```   421  apply(rule_tac x="[(R,t)]" in bexI)
```
```   422   apply simp
```
```   423  apply(simp add:cp_def)
```
```   424  apply(rule CptnOne)
```
```   425 apply clarify
```
```   426 apply(rule_tac x="(a, b)#l" in bexI)
```
```   427  apply (rule conjI)
```
```   428   apply(case_tac l,simp add:cp_def)
```
```   429   apply(simp add:last_length)
```
```   430  apply clarify
```
```   431 apply(case_tac i,simp)
```
```   432 apply(simp add:cp_def)
```
```   433 apply force
```
```   434 apply(simp add:cp_def)
```
```   435  apply(case_tac l)
```
```   436  apply(force elim:cptn.cases)
```
```   437 apply simp
```
```   438 apply(erule CptnComp)
```
```   439 apply clarify
```
```   440 done
```
```   441
```
```   442 lemma Await_sound:
```
```   443   "\<lbrakk>stable pre rely; stable post rely;
```
```   444   \<forall>V. \<turnstile> P sat [pre \<inter> b \<inter> {s. s = V}, {(s, t). s = t},
```
```   445                  UNIV, {s. (V, s) \<in> guar} \<inter> post] \<and>
```
```   446   \<Turnstile> P sat [pre \<inter> b \<inter> {s. s = V}, {(s, t). s = t},
```
```   447                  UNIV, {s. (V, s) \<in> guar} \<inter> post] \<rbrakk>
```
```   448   \<Longrightarrow> \<Turnstile> Await b P sat [pre, rely, guar, post]"
```
```   449 apply(unfold com_validity_def)
```
```   450 apply clarify
```
```   451 apply(simp add:comm_def)
```
```   452 apply(rule conjI)
```
```   453  apply clarify
```
```   454  apply(simp add:cp_def assum_def)
```
```   455  apply clarify
```
```   456  apply(frule_tac j=0 and k=i and p=pre in stability,simp_all)
```
```   457    apply(erule_tac x=ia in allE,simp)
```
```   458   apply(subgoal_tac "x\<in> cp (Some(Await b P)) s")
```
```   459   apply(erule_tac i=i in unique_ctran_Await,force,simp_all)
```
```   460   apply(simp add:cp_def)
```
```   461 \<comment>\<open>here starts the different part.\<close>
```
```   462  apply(erule ctran.cases,simp_all)
```
```   463  apply(drule Star_imp_cptn)
```
```   464  apply clarify
```
```   465  apply(erule_tac x=sa in allE)
```
```   466  apply clarify
```
```   467  apply(erule_tac x=sa in allE)
```
```   468  apply(drule_tac c=l in subsetD)
```
```   469   apply (simp add:cp_def)
```
```   470   apply clarify
```
```   471   apply(erule_tac x=ia and P="\<lambda>i. H i \<longrightarrow> (J i, I i)\<in>ctran" for H J I in allE,simp)
```
```   472   apply(erule etranE,simp)
```
```   473  apply simp
```
```   474 apply clarify
```
```   475 apply(simp add:cp_def)
```
```   476 apply clarify
```
```   477 apply(frule_tac i="length x - 1" in exists_ctran_Await_None,force)
```
```   478   apply (case_tac x,simp+)
```
```   479  apply(rule last_fst_esp,simp add:last_length)
```
```   480  apply(case_tac x, simp+)
```
```   481 apply clarify
```
```   482 apply(simp add:assum_def)
```
```   483 apply clarify
```
```   484 apply(frule_tac j=0 and k="j" and p=pre in stability,simp_all)
```
```   485   apply(erule_tac x=i in allE,simp)
```
```   486  apply(erule_tac i=j in unique_ctran_Await,force,simp_all)
```
```   487 apply(case_tac "x!j")
```
```   488 apply clarify
```
```   489 apply simp
```
```   490 apply(drule_tac s="Some (Await b P)" in sym,simp)
```
```   491 apply(case_tac "x!Suc j",simp)
```
```   492 apply(rule ctran.cases,simp)
```
```   493 apply(simp_all)
```
```   494 apply(drule Star_imp_cptn)
```
```   495 apply clarify
```
```   496 apply(erule_tac x=sa in allE)
```
```   497 apply clarify
```
```   498 apply(erule_tac x=sa in allE)
```
```   499 apply(drule_tac c=l in subsetD)
```
```   500  apply (simp add:cp_def)
```
```   501  apply clarify
```
```   502  apply(erule_tac x=i and P="\<lambda>i. H i \<longrightarrow> (J i, I i)\<in>ctran" for H J I in allE,simp)
```
```   503  apply(erule etranE,simp)
```
```   504 apply simp
```
```   505 apply clarify
```
```   506 apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all)
```
```   507  apply(case_tac x,simp+)
```
```   508  apply(erule_tac x=i in allE)
```
```   509 apply(erule_tac i=j in unique_ctran_Await,force,simp_all)
```
```   510  apply arith+
```
```   511 apply(case_tac x)
```
```   512 apply(simp add:last_length)+
```
```   513 done
```
```   514
```
```   515 subsubsection\<open>Soundness of the Conditional rule\<close>
```
```   516
```
```   517 lemma Cond_sound:
```
```   518   "\<lbrakk> stable pre rely; \<Turnstile> P1 sat [pre \<inter> b, rely, guar, post];
```
```   519   \<Turnstile> P2 sat [pre \<inter> - b, rely, guar, post]; \<forall>s. (s,s)\<in>guar\<rbrakk>
```
```   520   \<Longrightarrow> \<Turnstile> (Cond b P1 P2) sat [pre, rely, guar, post]"
```
```   521 apply(unfold com_validity_def)
```
```   522 apply clarify
```
```   523 apply(simp add:cp_def comm_def)
```
```   524 apply(case_tac "\<exists>i. Suc i<length x \<and> x!i -c\<rightarrow> x!Suc i")
```
```   525  prefer 2
```
```   526  apply simp
```
```   527  apply clarify
```
```   528  apply(frule_tac j="0" and k="length x - 1" and p=pre in stability,simp+)
```
```   529      apply(case_tac x,simp+)
```
```   530     apply(simp add:assum_def)
```
```   531    apply(simp add:assum_def)
```
```   532   apply(erule_tac m="length x" in etran_or_ctran,simp+)
```
```   533  apply(case_tac x, (simp add:last_length)+)
```
```   534 apply(erule exE)
```
```   535 apply(drule_tac n=i and P="\<lambda>i. H i \<and> (J i, I i) \<in> ctran" for H J I in Ex_first_occurrence)
```
```   536 apply clarify
```
```   537 apply (simp add:assum_def)
```
```   538 apply(frule_tac j=0 and k="m" and p=pre in stability,simp+)
```
```   539  apply(erule_tac m="Suc m" in etran_or_ctran,simp+)
```
```   540 apply(erule ctran.cases,simp_all)
```
```   541  apply(erule_tac x="sa" in allE)
```
```   542  apply(drule_tac c="drop (Suc m) x" in subsetD)
```
```   543   apply simp
```
```   544   apply clarify
```
```   545  apply simp
```
```   546  apply clarify
```
```   547  apply(case_tac "i\<le>m")
```
```   548   apply(drule le_imp_less_or_eq)
```
```   549   apply(erule disjE)
```
```   550    apply(erule_tac x=i in allE, erule impE, assumption)
```
```   551    apply simp+
```
```   552  apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. H j \<longrightarrow> J j \<longrightarrow> (I j)\<in>guar" for H J I in allE)
```
```   553  apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
```
```   554   apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
```
```   555    apply(rotate_tac -2)
```
```   556    apply simp
```
```   557   apply arith
```
```   558  apply arith
```
```   559 apply(case_tac "length (drop (Suc m) x)",simp)
```
```   560 apply(erule_tac x="sa" in allE)
```
```   561 back
```
```   562 apply(drule_tac c="drop (Suc m) x" in subsetD,simp)
```
```   563  apply clarify
```
```   564 apply simp
```
```   565 apply clarify
```
```   566 apply(case_tac "i\<le>m")
```
```   567  apply(drule le_imp_less_or_eq)
```
```   568  apply(erule disjE)
```
```   569   apply(erule_tac x=i in allE, erule impE, assumption)
```
```   570   apply simp
```
```   571  apply simp
```
```   572 apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. H j \<longrightarrow> J j \<longrightarrow> (I j)\<in>guar" for H J I in allE)
```
```   573 apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
```
```   574  apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
```
```   575   apply(rotate_tac -2)
```
```   576   apply simp
```
```   577  apply arith
```
```   578 apply arith
```
```   579 done
```
```   580
```
```   581 subsubsection\<open>Soundness of the Sequential rule\<close>
```
```   582
```
```   583 inductive_cases Seq_cases [elim!]: "(Some (Seq P Q), s) -c\<rightarrow> t"
```
```   584
```
```   585 lemma last_lift_not_None: "fst ((lift Q) ((x#xs)!(length xs))) \<noteq> None"
```
```   586 apply(subgoal_tac "length xs<length (x # xs)")
```
```   587  apply(drule_tac Q=Q in  lift_nth)
```
```   588  apply(erule ssubst)
```
```   589  apply (simp add:lift_def)
```
```   590  apply(case_tac "(x # xs) ! length xs",simp)
```
```   591 apply simp
```
```   592 done
```
```   593
```
```   594 lemma Seq_sound1 [rule_format]:
```
```   595   "x\<in> cptn_mod \<Longrightarrow> \<forall>s P. x !0=(Some (Seq P Q), s) \<longrightarrow>
```
```   596   (\<forall>i<length x. fst(x!i)\<noteq>Some Q) \<longrightarrow>
```
```   597   (\<exists>xs\<in> cp (Some P) s. x=map (lift Q) xs)"
```
```   598 apply(erule cptn_mod.induct)
```
```   599 apply(unfold cp_def)
```
```   600 apply safe
```
```   601 apply simp_all
```
```   602     apply(simp add:lift_def)
```
```   603     apply(rule_tac x="[(Some Pa, sa)]" in exI,simp add:CptnOne)
```
```   604    apply(subgoal_tac "(\<forall>i < Suc (length xs). fst (((Some (Seq Pa Q), t) # xs) ! i) \<noteq> Some Q)")
```
```   605     apply clarify
```
```   606     apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # zs" in exI,simp)
```
```   607     apply(rule conjI,erule CptnEnv)
```
```   608     apply(simp (no_asm_use) add:lift_def)
```
```   609    apply clarify
```
```   610    apply(erule_tac x="Suc i" in allE, simp)
```
```   611   apply(ind_cases "((Some (Seq Pa Q), sa), None, t) \<in> ctran" for Pa sa t)
```
```   612  apply(rule_tac x="(Some P, sa) # xs" in exI, simp add:cptn_iff_cptn_mod lift_def)
```
```   613 apply(erule_tac x="length xs" in allE, simp)
```
```   614 apply(simp only:Cons_lift_append)
```
```   615 apply(subgoal_tac "length xs < length ((Some P, sa) # xs)")
```
```   616  apply(simp only :nth_append length_map last_length nth_map)
```
```   617  apply(case_tac "last((Some P, sa) # xs)")
```
```   618  apply(simp add:lift_def)
```
```   619 apply simp
```
```   620 done
```
```   621
```
```   622 lemma Seq_sound2 [rule_format]:
```
```   623   "x \<in> cptn \<Longrightarrow> \<forall>s P i. x!0=(Some (Seq P Q), s) \<longrightarrow> i<length x
```
```   624   \<longrightarrow> fst(x!i)=Some Q \<longrightarrow>
```
```   625   (\<forall>j<i. fst(x!j)\<noteq>(Some Q)) \<longrightarrow>
```
```   626   (\<exists>xs ys. xs \<in> cp (Some P) s \<and> length xs=Suc i
```
```   627    \<and> ys \<in> cp (Some Q) (snd(xs !i)) \<and> x=(map (lift Q) xs)@tl ys)"
```
```   628 apply(erule cptn.induct)
```
```   629 apply(unfold cp_def)
```
```   630 apply safe
```
```   631 apply simp_all
```
```   632  apply(case_tac i,simp+)
```
```   633  apply(erule allE,erule impE,assumption,simp)
```
```   634  apply clarify
```
```   635  apply(subgoal_tac "(\<forall>j < nat. fst (((Some (Seq Pa Q), t) # xs) ! j) \<noteq> Some Q)",clarify)
```
```   636   prefer 2
```
```   637   apply force
```
```   638  apply(case_tac xsa,simp,simp)
```
```   639  apply(rename_tac list)
```
```   640  apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # list" in exI,simp)
```
```   641  apply(rule conjI,erule CptnEnv)
```
```   642  apply(simp (no_asm_use) add:lift_def)
```
```   643  apply(rule_tac x=ys in exI,simp)
```
```   644 apply(ind_cases "((Some (Seq Pa Q), sa), t) \<in> ctran" for Pa sa t)
```
```   645  apply simp
```
```   646  apply(rule_tac x="(Some Pa, sa)#[(None, ta)]" in exI,simp)
```
```   647  apply(rule conjI)
```
```   648   apply(drule_tac xs="[]" in CptnComp,force simp add:CptnOne,simp)
```
```   649  apply(case_tac i, simp+)
```
```   650  apply(case_tac nat,simp+)
```
```   651  apply(rule_tac x="(Some Q,ta)#xs" in exI,simp add:lift_def)
```
```   652  apply(case_tac nat,simp+)
```
```   653  apply(force)
```
```   654 apply(case_tac i, simp+)
```
```   655 apply(case_tac nat,simp+)
```
```   656 apply(erule_tac x="Suc nata" in allE,simp)
```
```   657 apply clarify
```
```   658 apply(subgoal_tac "(\<forall>j<Suc nata. fst (((Some (Seq P2 Q), ta) # xs) ! j) \<noteq> Some Q)",clarify)
```
```   659  prefer 2
```
```   660  apply clarify
```
```   661  apply force
```
```   662 apply(rule_tac x="(Some Pa, sa)#(Some P2, ta)#(tl xsa)" in exI,simp)
```
```   663 apply(rule conjI,erule CptnComp)
```
```   664 apply(rule nth_tl_if,force,simp+)
```
```   665 apply(rule_tac x=ys in exI,simp)
```
```   666 apply(rule conjI)
```
```   667 apply(rule nth_tl_if,force,simp+)
```
```   668  apply(rule tl_zero,simp+)
```
```   669  apply force
```
```   670 apply(rule conjI,simp add:lift_def)
```
```   671 apply(subgoal_tac "lift Q (Some P2, ta) =(Some (Seq P2 Q), ta)")
```
```   672  apply(simp add:Cons_lift del:list.map)
```
```   673  apply(rule nth_tl_if)
```
```   674    apply force
```
```   675   apply simp+
```
```   676 apply(simp add:lift_def)
```
```   677 done
```
```   678 (*
```
```   679 lemma last_lift_not_None3: "fst (last (map (lift Q) (x#xs))) \<noteq> None"
```
```   680 apply(simp only:last_length [THEN sym])
```
```   681 apply(subgoal_tac "length xs<length (x # xs)")
```
```   682  apply(drule_tac Q=Q in  lift_nth)
```
```   683  apply(erule ssubst)
```
```   684  apply (simp add:lift_def)
```
```   685  apply(case_tac "(x # xs) ! length xs",simp)
```
```   686 apply simp
```
```   687 done
```
```   688 *)
```
```   689
```
```   690 lemma last_lift_not_None2: "fst ((lift Q) (last (x#xs))) \<noteq> None"
```
```   691 apply(simp only:last_length [THEN sym])
```
```   692 apply(subgoal_tac "length xs<length (x # xs)")
```
```   693  apply(drule_tac Q=Q in  lift_nth)
```
```   694  apply(erule ssubst)
```
```   695  apply (simp add:lift_def)
```
```   696  apply(case_tac "(x # xs) ! length xs",simp)
```
```   697 apply simp
```
```   698 done
```
```   699
```
```   700 lemma Seq_sound:
```
```   701   "\<lbrakk>\<Turnstile> P sat [pre, rely, guar, mid]; \<Turnstile> Q sat [mid, rely, guar, post]\<rbrakk>
```
```   702   \<Longrightarrow> \<Turnstile> Seq P Q sat [pre, rely, guar, post]"
```
```   703 apply(unfold com_validity_def)
```
```   704 apply clarify
```
```   705 apply(case_tac "\<exists>i<length x. fst(x!i)=Some Q")
```
```   706  prefer 2
```
```   707  apply (simp add:cp_def cptn_iff_cptn_mod)
```
```   708  apply clarify
```
```   709  apply(frule_tac Seq_sound1,force)
```
```   710   apply force
```
```   711  apply clarify
```
```   712  apply(erule_tac x=s in allE,simp)
```
```   713  apply(drule_tac c=xs in subsetD,simp add:cp_def cptn_iff_cptn_mod)
```
```   714   apply(simp add:assum_def)
```
```   715   apply clarify
```
```   716   apply(erule_tac P="\<lambda>j. H j \<longrightarrow> J j \<longrightarrow> I j" for H J I in allE,erule impE, assumption)
```
```   717   apply(simp add:snd_lift)
```
```   718   apply(erule mp)
```
```   719   apply(force elim:etranE intro:Env simp add:lift_def)
```
```   720  apply(simp add:comm_def)
```
```   721  apply(rule conjI)
```
```   722   apply clarify
```
```   723   apply(erule_tac P="\<lambda>j. H j \<longrightarrow> J j \<longrightarrow> I j" for H J I in allE,erule impE, assumption)
```
```   724   apply(simp add:snd_lift)
```
```   725   apply(erule mp)
```
```   726   apply(case_tac "(xs!i)")
```
```   727   apply(case_tac "(xs! Suc i)")
```
```   728   apply(case_tac "fst(xs!i)")
```
```   729    apply(erule_tac x=i in allE, simp add:lift_def)
```
```   730   apply(case_tac "fst(xs!Suc i)")
```
```   731    apply(force simp add:lift_def)
```
```   732   apply(force simp add:lift_def)
```
```   733  apply clarify
```
```   734  apply(case_tac xs,simp add:cp_def)
```
```   735  apply clarify
```
```   736  apply (simp del:list.map)
```
```   737  apply (rename_tac list)
```
```   738  apply(subgoal_tac "(map (lift Q) ((a, b) # list))\<noteq>[]")
```
```   739   apply(drule last_conv_nth)
```
```   740   apply (simp del:list.map)
```
```   741   apply(simp only:last_lift_not_None)
```
```   742  apply simp
```
```   743 \<comment>\<open>\<open>\<exists>i<length x. fst (x ! i) = Some Q\<close>\<close>
```
```   744 apply(erule exE)
```
```   745 apply(drule_tac n=i and P="\<lambda>i. i < length x \<and> fst (x ! i) = Some Q" in Ex_first_occurrence)
```
```   746 apply clarify
```
```   747 apply (simp add:cp_def)
```
```   748  apply clarify
```
```   749  apply(frule_tac i=m in Seq_sound2,force)
```
```   750   apply simp+
```
```   751 apply clarify
```
```   752 apply(simp add:comm_def)
```
```   753 apply(erule_tac x=s in allE)
```
```   754 apply(drule_tac c=xs in subsetD,simp)
```
```   755  apply(case_tac "xs=[]",simp)
```
```   756  apply(simp add:cp_def assum_def nth_append)
```
```   757  apply clarify
```
```   758  apply(erule_tac x=i in allE)
```
```   759   back
```
```   760  apply(simp add:snd_lift)
```
```   761  apply(erule mp)
```
```   762  apply(force elim:etranE intro:Env simp add:lift_def)
```
```   763 apply simp
```
```   764 apply clarify
```
```   765 apply(erule_tac x="snd(xs!m)" in allE)
```
```   766 apply(drule_tac c=ys in subsetD,simp add:cp_def assum_def)
```
```   767  apply(case_tac "xs\<noteq>[]")
```
```   768  apply(drule last_conv_nth,simp)
```
```   769  apply(rule conjI)
```
```   770   apply(erule mp)
```
```   771   apply(case_tac "xs!m")
```
```   772   apply(case_tac "fst(xs!m)",simp)
```
```   773   apply(simp add:lift_def nth_append)
```
```   774  apply clarify
```
```   775  apply(erule_tac x="m+i" in allE)
```
```   776  back
```
```   777  back
```
```   778  apply(case_tac ys,(simp add:nth_append)+)
```
```   779  apply (case_tac i, (simp add:snd_lift)+)
```
```   780   apply(erule mp)
```
```   781   apply(case_tac "xs!m")
```
```   782   apply(force elim:etran.cases intro:Env simp add:lift_def)
```
```   783  apply simp
```
```   784 apply simp
```
```   785 apply clarify
```
```   786 apply(rule conjI,clarify)
```
```   787  apply(case_tac "i<m",simp add:nth_append)
```
```   788   apply(simp add:snd_lift)
```
```   789   apply(erule allE, erule impE, assumption, erule mp)
```
```   790   apply(case_tac "(xs ! i)")
```
```   791   apply(case_tac "(xs ! Suc i)")
```
```   792   apply(case_tac "fst(xs ! i)",force simp add:lift_def)
```
```   793   apply(case_tac "fst(xs ! Suc i)")
```
```   794    apply (force simp add:lift_def)
```
```   795   apply (force simp add:lift_def)
```
```   796  apply(erule_tac x="i-m" in allE)
```
```   797  back
```
```   798  back
```
```   799  apply(subgoal_tac "Suc (i - m) < length ys",simp)
```
```   800   prefer 2
```
```   801   apply arith
```
```   802  apply(simp add:nth_append snd_lift)
```
```   803  apply(rule conjI,clarify)
```
```   804   apply(subgoal_tac "i=m")
```
```   805    prefer 2
```
```   806    apply arith
```
```   807   apply clarify
```
```   808   apply(simp add:cp_def)
```
```   809   apply(rule tl_zero)
```
```   810     apply(erule mp)
```
```   811     apply(case_tac "lift Q (xs!m)",simp add:snd_lift)
```
```   812     apply(case_tac "xs!m",case_tac "fst(xs!m)",simp add:lift_def snd_lift)
```
```   813      apply(case_tac ys,simp+)
```
```   814     apply(simp add:lift_def)
```
```   815    apply simp
```
```   816   apply force
```
```   817  apply clarify
```
```   818  apply(rule tl_zero)
```
```   819    apply(rule tl_zero)
```
```   820      apply (subgoal_tac "i-m=Suc(i-Suc m)")
```
```   821       apply simp
```
```   822       apply(erule mp)
```
```   823       apply(case_tac ys,simp+)
```
```   824    apply force
```
```   825   apply arith
```
```   826  apply force
```
```   827 apply clarify
```
```   828 apply(case_tac "(map (lift Q) xs @ tl ys)\<noteq>[]")
```
```   829  apply(drule last_conv_nth)
```
```   830  apply(simp add: snd_lift nth_append)
```
```   831  apply(rule conjI,clarify)
```
```   832   apply(case_tac ys,simp+)
```
```   833  apply clarify
```
```   834  apply(case_tac ys,simp+)
```
```   835 done
```
```   836
```
```   837 subsubsection\<open>Soundness of the While rule\<close>
```
```   838
```
```   839 lemma last_append[rule_format]:
```
```   840   "\<forall>xs. ys\<noteq>[] \<longrightarrow> ((xs@ys)!(length (xs@ys) - (Suc 0)))=(ys!(length ys - (Suc 0)))"
```
```   841 apply(induct ys)
```
```   842  apply simp
```
```   843 apply clarify
```
```   844 apply (simp add:nth_append)
```
```   845 done
```
```   846
```
```   847 lemma assum_after_body:
```
```   848   "\<lbrakk> \<Turnstile> P sat [pre \<inter> b, rely, guar, pre];
```
```   849   (Some P, s) # xs \<in> cptn_mod; fst (last ((Some P, s) # xs)) = None; s \<in> b;
```
```   850   (Some (While b P), s) # (Some (Seq P (While b P)), s) #
```
```   851    map (lift (While b P)) xs @ ys \<in> assum (pre, rely)\<rbrakk>
```
```   852   \<Longrightarrow> (Some (While b P), snd (last ((Some P, s) # xs))) # ys \<in> assum (pre, rely)"
```
```   853 apply(simp add:assum_def com_validity_def cp_def cptn_iff_cptn_mod)
```
```   854 apply clarify
```
```   855 apply(erule_tac x=s in allE)
```
```   856 apply(drule_tac c="(Some P, s) # xs" in subsetD,simp)
```
```   857  apply clarify
```
```   858  apply(erule_tac x="Suc i" in allE)
```
```   859  apply simp
```
```   860  apply(simp add:Cons_lift_append nth_append snd_lift del:list.map)
```
```   861  apply(erule mp)
```
```   862  apply(erule etranE,simp)
```
```   863  apply(case_tac "fst(((Some P, s) # xs) ! i)")
```
```   864   apply(force intro:Env simp add:lift_def)
```
```   865  apply(force intro:Env simp add:lift_def)
```
```   866 apply(rule conjI)
```
```   867  apply clarify
```
```   868  apply(simp add:comm_def last_length)
```
```   869 apply clarify
```
```   870 apply(rule conjI)
```
```   871  apply(simp add:comm_def)
```
```   872 apply clarify
```
```   873 apply(erule_tac x="Suc(length xs + i)" in allE,simp)
```
```   874 apply(case_tac i, simp add:nth_append Cons_lift_append snd_lift last_conv_nth lift_def split_def)
```
```   875 apply(simp add:Cons_lift_append nth_append snd_lift)
```
```   876 done
```
```   877
```
```   878 lemma While_sound_aux [rule_format]:
```
```   879   "\<lbrakk> pre \<inter> - b \<subseteq> post; \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s, s) \<in> guar;
```
```   880    stable pre rely;  stable post rely; x \<in> cptn_mod \<rbrakk>
```
```   881   \<Longrightarrow>  \<forall>s xs. x=(Some(While b P),s)#xs \<longrightarrow> x\<in>assum(pre, rely) \<longrightarrow> x \<in> comm (guar, post)"
```
```   882 apply(erule cptn_mod.induct)
```
```   883 apply safe
```
```   884 apply (simp_all del:last.simps)
```
```   885 \<comment>\<open>5 subgoals left\<close>
```
```   886 apply(simp add:comm_def)
```
```   887 \<comment>\<open>4 subgoals left\<close>
```
```   888 apply(rule etran_in_comm)
```
```   889 apply(erule mp)
```
```   890 apply(erule tl_of_assum_in_assum,simp)
```
```   891 \<comment>\<open>While-None\<close>
```
```   892 apply(ind_cases "((Some (While b P), s), None, t) \<in> ctran" for s t)
```
```   893 apply(simp add:comm_def)
```
```   894 apply(simp add:cptn_iff_cptn_mod [THEN sym])
```
```   895 apply(rule conjI,clarify)
```
```   896  apply(force simp add:assum_def)
```
```   897 apply clarify
```
```   898 apply(rule conjI, clarify)
```
```   899  apply(case_tac i,simp,simp)
```
```   900  apply(force simp add:not_ctran_None2)
```
```   901 apply(subgoal_tac "\<forall>i. Suc i < length ((None, t) # xs) \<longrightarrow> (((None, t) # xs) ! i, ((None, t) # xs) ! Suc i)\<in> etran")
```
```   902  prefer 2
```
```   903  apply clarify
```
```   904  apply(rule_tac m="length ((None, s) # xs)" in etran_or_ctran,simp+)
```
```   905  apply(erule not_ctran_None2,simp)
```
```   906  apply simp+
```
```   907 apply(frule_tac j="0" and k="length ((None, s) # xs) - 1" and p=post in stability,simp+)
```
```   908    apply(force simp add:assum_def subsetD)
```
```   909   apply(simp add:assum_def)
```
```   910   apply clarify
```
```   911   apply(erule_tac x="i" in allE,simp)
```
```   912   apply(erule_tac x="Suc i" in allE,simp)
```
```   913  apply simp
```
```   914 apply clarify
```
```   915 apply (simp add:last_length)
```
```   916 \<comment>\<open>WhileOne\<close>
```
```   917 apply(thin_tac "P = While b P \<longrightarrow> Q" for Q)
```
```   918 apply(rule ctran_in_comm,simp)
```
```   919 apply(simp add:Cons_lift del:list.map)
```
```   920 apply(simp add:comm_def del:list.map)
```
```   921 apply(rule conjI)
```
```   922  apply clarify
```
```   923  apply(case_tac "fst(((Some P, sa) # xs) ! i)")
```
```   924   apply(case_tac "((Some P, sa) # xs) ! i")
```
```   925   apply (simp add:lift_def)
```
```   926   apply(ind_cases "(Some (While b P), ba) -c\<rightarrow> t" for ba t)
```
```   927    apply simp
```
```   928   apply simp
```
```   929  apply(simp add:snd_lift del:list.map)
```
```   930  apply(simp only:com_validity_def cp_def cptn_iff_cptn_mod)
```
```   931  apply(erule_tac x=sa in allE)
```
```   932  apply(drule_tac c="(Some P, sa) # xs" in subsetD)
```
```   933   apply (simp add:assum_def del:list.map)
```
```   934   apply clarify
```
```   935   apply(erule_tac x="Suc ia" in allE,simp add:snd_lift del:list.map)
```
```   936   apply(erule mp)
```
```   937   apply(case_tac "fst(((Some P, sa) # xs) ! ia)")
```
```   938    apply(erule etranE,simp add:lift_def)
```
```   939    apply(rule Env)
```
```   940   apply(erule etranE,simp add:lift_def)
```
```   941   apply(rule Env)
```
```   942  apply (simp add:comm_def del:list.map)
```
```   943  apply clarify
```
```   944  apply(erule allE,erule impE,assumption)
```
```   945  apply(erule mp)
```
```   946  apply(case_tac "((Some P, sa) # xs) ! i")
```
```   947  apply(case_tac "xs!i")
```
```   948  apply(simp add:lift_def)
```
```   949  apply(case_tac "fst(xs!i)")
```
```   950   apply force
```
```   951  apply force
```
```   952 \<comment>\<open>last=None\<close>
```
```   953 apply clarify
```
```   954 apply(subgoal_tac "(map (lift (While b P)) ((Some P, sa) # xs))\<noteq>[]")
```
```   955  apply(drule last_conv_nth)
```
```   956  apply (simp del:list.map)
```
```   957  apply(simp only:last_lift_not_None)
```
```   958 apply simp
```
```   959 \<comment>\<open>WhileMore\<close>
```
```   960 apply(thin_tac "P = While b P \<longrightarrow> Q" for Q)
```
```   961 apply(rule ctran_in_comm,simp del:last.simps)
```
```   962 \<comment>\<open>metiendo la hipotesis antes de dividir la conclusion.\<close>
```
```   963 apply(subgoal_tac "(Some (While b P), snd (last ((Some P, sa) # xs))) # ys \<in> assum (pre, rely)")
```
```   964  apply (simp del:last.simps)
```
```   965  prefer 2
```
```   966  apply(erule assum_after_body)
```
```   967   apply (simp del:last.simps)+
```
```   968 \<comment>\<open>lo de antes.\<close>
```
```   969 apply(simp add:comm_def del:list.map last.simps)
```
```   970 apply(rule conjI)
```
```   971  apply clarify
```
```   972  apply(simp only:Cons_lift_append)
```
```   973  apply(case_tac "i<length xs")
```
```   974   apply(simp add:nth_append del:list.map last.simps)
```
```   975   apply(case_tac "fst(((Some P, sa) # xs) ! i)")
```
```   976    apply(case_tac "((Some P, sa) # xs) ! i")
```
```   977    apply (simp add:lift_def del:last.simps)
```
```   978    apply(ind_cases "(Some (While b P), ba) -c\<rightarrow> t" for ba t)
```
```   979     apply simp
```
```   980    apply simp
```
```   981   apply(simp add:snd_lift del:list.map last.simps)
```
```   982   apply(thin_tac " \<forall>i. i < length ys \<longrightarrow> P i" for P)
```
```   983   apply(simp only:com_validity_def cp_def cptn_iff_cptn_mod)
```
```   984   apply(erule_tac x=sa in allE)
```
```   985   apply(drule_tac c="(Some P, sa) # xs" in subsetD)
```
```   986    apply (simp add:assum_def del:list.map last.simps)
```
```   987    apply clarify
```
```   988    apply(erule_tac x="Suc ia" in allE,simp add:nth_append snd_lift del:list.map last.simps, erule mp)
```
```   989    apply(case_tac "fst(((Some P, sa) # xs) ! ia)")
```
```   990     apply(erule etranE,simp add:lift_def)
```
```   991     apply(rule Env)
```
```   992    apply(erule etranE,simp add:lift_def)
```
```   993    apply(rule Env)
```
```   994   apply (simp add:comm_def del:list.map)
```
```   995   apply clarify
```
```   996   apply(erule allE,erule impE,assumption)
```
```   997   apply(erule mp)
```
```   998   apply(case_tac "((Some P, sa) # xs) ! i")
```
```   999   apply(case_tac "xs!i")
```
```  1000   apply(simp add:lift_def)
```
```  1001   apply(case_tac "fst(xs!i)")
```
```  1002    apply force
```
```  1003  apply force
```
```  1004 \<comment>\<open>\<open>i \<ge> length xs\<close>\<close>
```
```  1005 apply(subgoal_tac "i-length xs <length ys")
```
```  1006  prefer 2
```
```  1007  apply arith
```
```  1008 apply(erule_tac x="i-length xs" in allE,clarify)
```
```  1009 apply(case_tac "i=length xs")
```
```  1010  apply (simp add:nth_append snd_lift del:list.map last.simps)
```
```  1011  apply(simp add:last_length del:last.simps)
```
```  1012  apply(erule mp)
```
```  1013  apply(case_tac "last((Some P, sa) # xs)")
```
```  1014  apply(simp add:lift_def del:last.simps)
```
```  1015 \<comment>\<open>\<open>i>length xs\<close>\<close>
```
```  1016 apply(case_tac "i-length xs")
```
```  1017  apply arith
```
```  1018 apply(simp add:nth_append del:list.map last.simps)
```
```  1019 apply(rotate_tac -3)
```
```  1020 apply(subgoal_tac "i- Suc (length xs)=nat")
```
```  1021  prefer 2
```
```  1022  apply arith
```
```  1023 apply simp
```
```  1024 \<comment>\<open>last=None\<close>
```
```  1025 apply clarify
```
```  1026 apply(case_tac ys)
```
```  1027  apply(simp add:Cons_lift del:list.map last.simps)
```
```  1028  apply(subgoal_tac "(map (lift (While b P)) ((Some P, sa) # xs))\<noteq>[]")
```
```  1029   apply(drule last_conv_nth)
```
```  1030   apply (simp del:list.map)
```
```  1031   apply(simp only:last_lift_not_None)
```
```  1032  apply simp
```
```  1033 apply(subgoal_tac "((Some (Seq P (While b P)), sa) # map (lift (While b P)) xs @ ys)\<noteq>[]")
```
```  1034  apply(drule last_conv_nth)
```
```  1035  apply (simp del:list.map last.simps)
```
```  1036  apply(simp add:nth_append del:last.simps)
```
```  1037  apply(rename_tac a list)
```
```  1038  apply(subgoal_tac "((Some (While b P), snd (last ((Some P, sa) # xs))) # a # list)\<noteq>[]")
```
```  1039   apply(drule last_conv_nth)
```
```  1040   apply (simp del:list.map last.simps)
```
```  1041  apply simp
```
```  1042 apply simp
```
```  1043 done
```
```  1044
```
```  1045 lemma While_sound:
```
```  1046   "\<lbrakk>stable pre rely; pre \<inter> - b \<subseteq> post; stable post rely;
```
```  1047     \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s,s)\<in>guar\<rbrakk>
```
```  1048   \<Longrightarrow> \<Turnstile> While b P sat [pre, rely, guar, post]"
```
```  1049 apply(unfold com_validity_def)
```
```  1050 apply clarify
```
```  1051 apply(erule_tac xs="tl x" in While_sound_aux)
```
```  1052  apply(simp add:com_validity_def)
```
```  1053  apply force
```
```  1054  apply simp_all
```
```  1055 apply(simp add:cptn_iff_cptn_mod cp_def)
```
```  1056 apply(simp add:cp_def)
```
```  1057 apply clarify
```
```  1058 apply(rule nth_equalityI)
```
```  1059  apply simp_all
```
```  1060  apply(case_tac x,simp+)
```
```  1061 apply clarify
```
```  1062 apply(case_tac i,simp+)
```
```  1063 apply(case_tac x,simp+)
```
```  1064 done
```
```  1065
```
```  1066 subsubsection\<open>Soundness of the Rule of Consequence\<close>
```
```  1067
```
```  1068 lemma Conseq_sound:
```
```  1069   "\<lbrakk>pre \<subseteq> pre'; rely \<subseteq> rely'; guar' \<subseteq> guar; post' \<subseteq> post;
```
```  1070   \<Turnstile> P sat [pre', rely', guar', post']\<rbrakk>
```
```  1071   \<Longrightarrow> \<Turnstile> P sat [pre, rely, guar, post]"
```
```  1072 apply(simp add:com_validity_def assum_def comm_def)
```
```  1073 apply clarify
```
```  1074 apply(erule_tac x=s in allE)
```
```  1075 apply(drule_tac c=x in subsetD)
```
```  1076  apply force
```
```  1077 apply force
```
```  1078 done
```
```  1079
```
```  1080 subsubsection \<open>Soundness of the system for sequential component programs\<close>
```
```  1081
```
```  1082 theorem rgsound:
```
```  1083   "\<turnstile> P sat [pre, rely, guar, post] \<Longrightarrow> \<Turnstile> P sat [pre, rely, guar, post]"
```
```  1084 apply(erule rghoare.induct)
```
```  1085  apply(force elim:Basic_sound)
```
```  1086  apply(force elim:Seq_sound)
```
```  1087  apply(force elim:Cond_sound)
```
```  1088  apply(force elim:While_sound)
```
```  1089  apply(force elim:Await_sound)
```
```  1090 apply(erule Conseq_sound,simp+)
```
```  1091 done
```
```  1092
```
```  1093 subsection \<open>Soundness of the System for Parallel Programs\<close>
```
```  1094
```
```  1095 definition ParallelCom :: "('a rgformula) list \<Rightarrow> 'a par_com" where
```
```  1096   "ParallelCom Ps \<equiv> map (Some \<circ> fst) Ps"
```
```  1097
```
```  1098 lemma two:
```
```  1099   "\<lbrakk> \<forall>i<length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j))
```
```  1100      \<subseteq> Rely (xs ! i);
```
```  1101    pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i));
```
```  1102    \<forall>i<length xs.
```
```  1103    \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
```
```  1104    length xs=length clist; x \<in> par_cp (ParallelCom xs) s; x\<in>par_assum(pre, rely);
```
```  1105   \<forall>i<length clist. clist!i\<in>cp (Some(Com(xs!i))) s; x \<propto> clist \<rbrakk>
```
```  1106   \<Longrightarrow> \<forall>j i. i<length clist \<and> Suc j<length x \<longrightarrow> (clist!i!j) -c\<rightarrow> (clist!i!Suc j)
```
```  1107   \<longrightarrow> (snd(clist!i!j), snd(clist!i!Suc j)) \<in> Guar(xs!i)"
```
```  1108 apply(unfold par_cp_def)
```
```  1109 apply (rule ccontr)
```
```  1110 \<comment>\<open>By contradiction:\<close>
```
```  1111 apply simp
```
```  1112 apply(erule exE)
```
```  1113 \<comment>\<open>the first c-tran that does not satisfy the guarantee-condition is from \<open>\<sigma>_i\<close> at step \<open>m\<close>.\<close>
```
```  1114 apply(drule_tac n=j and P="\<lambda>j. \<exists>i. H i j" for H in Ex_first_occurrence)
```
```  1115 apply(erule exE)
```
```  1116 apply clarify
```
```  1117 \<comment>\<open>\<open>\<sigma>_i \<in> A(pre, rely_1)\<close>\<close>
```
```  1118 apply(subgoal_tac "take (Suc (Suc m)) (clist!i) \<in> assum(Pre(xs!i), Rely(xs!i))")
```
```  1119 \<comment>\<open>but this contradicts \<open>\<Turnstile> \<sigma>_i sat [pre_i,rely_i,guar_i,post_i]\<close>\<close>
```
```  1120  apply(erule_tac x=i and P="\<lambda>i. H i \<longrightarrow> \<Turnstile> (J i) sat [I i,K i,M i,N i]" for H J I K M N in allE,erule impE,assumption)
```
```  1121  apply(simp add:com_validity_def)
```
```  1122  apply(erule_tac x=s in allE)
```
```  1123  apply(simp add:cp_def comm_def)
```
```  1124  apply(drule_tac c="take (Suc (Suc m)) (clist ! i)" in subsetD)
```
```  1125   apply simp
```
```  1126   apply (blast intro: takecptn_is_cptn)
```
```  1127  apply simp
```
```  1128  apply clarify
```
```  1129  apply(erule_tac x=m and P="\<lambda>j. I j \<and> J j \<longrightarrow> H j" for I J H in allE)
```
```  1130  apply (simp add:conjoin_def same_length_def)
```
```  1131 apply(simp add:assum_def)
```
```  1132 apply(rule conjI)
```
```  1133  apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> I j \<in>cp (K j) (J j)" for H I K J in allE)
```
```  1134  apply(simp add:cp_def par_assum_def)
```
```  1135  apply(drule_tac c="s" in subsetD,simp)
```
```  1136  apply simp
```
```  1137 apply clarify
```
```  1138 apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> M \<union> UNION (S j) (T j) \<subseteq> (L j)" for H M S T L in allE)
```
```  1139 apply simp
```
```  1140 apply(erule subsetD)
```
```  1141 apply simp
```
```  1142 apply(simp add:conjoin_def compat_label_def)
```
```  1143 apply clarify
```
```  1144 apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> (P j) \<or> Q j" for H P Q in allE,simp)
```
```  1145 \<comment>\<open>each etran in \<open>\<sigma>_1[0\<dots>m]\<close> corresponds to\<close>
```
```  1146 apply(erule disjE)
```
```  1147 \<comment>\<open>a c-tran in some \<open>\<sigma>_{ib}\<close>\<close>
```
```  1148  apply clarify
```
```  1149  apply(case_tac "i=ib",simp)
```
```  1150   apply(erule etranE,simp)
```
```  1151  apply(erule_tac x="ib" and P="\<lambda>i. H i \<longrightarrow> (I i) \<or> (J i)" for H I J in allE)
```
```  1152  apply (erule etranE)
```
```  1153  apply(case_tac "ia=m",simp)
```
```  1154  apply simp
```
```  1155  apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> (\<forall>i. P i j)" for H P in allE)
```
```  1156  apply(subgoal_tac "ia<m",simp)
```
```  1157   prefer 2
```
```  1158   apply arith
```
```  1159  apply(erule_tac x=ib and P="\<lambda>j. (I j, H j) \<in> ctran \<longrightarrow> P i j" for I H P in allE,simp)
```
```  1160  apply(simp add:same_state_def)
```
```  1161  apply(erule_tac x=i and P="\<lambda>j. (T j) \<longrightarrow> (\<forall>i. (H j i) \<longrightarrow> (snd (d j i))=(snd (e j i)))" for T H d e in all_dupE)
```
```  1162  apply(erule_tac x=ib and P="\<lambda>j. (T j) \<longrightarrow> (\<forall>i. (H j i) \<longrightarrow> (snd (d j i))=(snd (e j i)))" for T H d e in allE,simp)
```
```  1163 \<comment>\<open>or an e-tran in \<open>\<sigma>\<close>,
```
```  1164 therefore it satisfies \<open>rely \<or> guar_{ib}\<close>\<close>
```
```  1165 apply (force simp add:par_assum_def same_state_def)
```
```  1166 done
```
```  1167
```
```  1168
```
```  1169 lemma three [rule_format]:
```
```  1170   "\<lbrakk> xs\<noteq>[]; \<forall>i<length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j))
```
```  1171    \<subseteq> Rely (xs ! i);
```
```  1172    pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i));
```
```  1173    \<forall>i<length xs.
```
```  1174     \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
```
```  1175    length xs=length clist; x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum(pre, rely);
```
```  1176   \<forall>i<length clist. clist!i\<in>cp (Some(Com(xs!i))) s; x \<propto> clist \<rbrakk>
```
```  1177   \<Longrightarrow> \<forall>j i. i<length clist \<and> Suc j<length x \<longrightarrow> (clist!i!j) -e\<rightarrow> (clist!i!Suc j)
```
```  1178   \<longrightarrow> (snd(clist!i!j), snd(clist!i!Suc j)) \<in> rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j))"
```
```  1179 apply(drule two)
```
```  1180  apply simp_all
```
```  1181 apply clarify
```
```  1182 apply(simp add:conjoin_def compat_label_def)
```
```  1183 apply clarify
```
```  1184 apply(erule_tac x=j and P="\<lambda>j. H j \<longrightarrow> (J j \<and> (\<exists>i. P i j)) \<or> I j" for H J P I in allE,simp)
```
```  1185 apply(erule disjE)
```
```  1186  prefer 2
```
```  1187  apply(force simp add:same_state_def par_assum_def)
```
```  1188 apply clarify
```
```  1189 apply(case_tac "i=ia",simp)
```
```  1190  apply(erule etranE,simp)
```
```  1191 apply(erule_tac x="ia" and P="\<lambda>i. H i \<longrightarrow> (I i) \<or> (J i)" for H I J in allE,simp)
```
```  1192 apply(erule_tac x=j and P="\<lambda>j. \<forall>i. S j i \<longrightarrow> (I j i, H j i) \<in> ctran \<longrightarrow> P i j" for S I H P in allE)
```
```  1193 apply(erule_tac x=ia and P="\<lambda>j. S j \<longrightarrow> (I j, H j) \<in> ctran \<longrightarrow> P j" for S I H P in allE)
```
```  1194 apply(simp add:same_state_def)
```
```  1195 apply(erule_tac x=i and P="\<lambda>j. T j \<longrightarrow> (\<forall>i. H j i \<longrightarrow> (snd (d j i))=(snd (e j i)))" for T H d e in all_dupE)
```
```  1196 apply(erule_tac x=ia and P="\<lambda>j. T j \<longrightarrow> (\<forall>i. H j i \<longrightarrow> (snd (d j i))=(snd (e j i)))" for T H d e in allE,simp)
```
```  1197 done
```
```  1198
```
```  1199 lemma four:
```
```  1200   "\<lbrakk>xs\<noteq>[]; \<forall>i < length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j))
```
```  1201     \<subseteq> Rely (xs ! i);
```
```  1202    (\<Union>j\<in>{j. j < length xs}. Guar (xs ! j)) \<subseteq> guar;
```
```  1203    pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i));
```
```  1204    \<forall>i < length xs.
```
```  1205     \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
```
```  1206    x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum (pre, rely); Suc i < length x;
```
```  1207    x ! i -pc\<rightarrow> x ! Suc i\<rbrakk>
```
```  1208   \<Longrightarrow> (snd (x ! i), snd (x ! Suc i)) \<in> guar"
```
```  1209 apply(simp add: ParallelCom_def)
```
```  1210 apply(subgoal_tac "(map (Some \<circ> fst) xs)\<noteq>[]")
```
```  1211  prefer 2
```
```  1212  apply simp
```
```  1213 apply(frule rev_subsetD)
```
```  1214  apply(erule one [THEN equalityD1])
```
```  1215 apply(erule subsetD)
```
```  1216 apply simp
```
```  1217 apply clarify
```
```  1218 apply(drule_tac pre=pre and rely=rely and  x=x and s=s and xs=xs and clist=clist in two)
```
```  1219 apply(assumption+)
```
```  1220      apply(erule sym)
```
```  1221     apply(simp add:ParallelCom_def)
```
```  1222    apply assumption
```
```  1223   apply(simp add:Com_def)
```
```  1224  apply assumption
```
```  1225 apply(simp add:conjoin_def same_program_def)
```
```  1226 apply clarify
```
```  1227 apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> fst(I j)=(J j)" for H I J in all_dupE)
```
```  1228 apply(erule_tac x="Suc i" and P="\<lambda>j. H j \<longrightarrow> fst(I j)=(J j)" for H I J in allE)
```
```  1229 apply(erule par_ctranE,simp)
```
```  1230 apply(erule_tac x=i and P="\<lambda>j. \<forall>i. S j i \<longrightarrow> (I j i, H j i) \<in> ctran \<longrightarrow> P i j" for S I H P in allE)
```
```  1231 apply(erule_tac x=ia and P="\<lambda>j. S j \<longrightarrow> (I j, H j) \<in> ctran \<longrightarrow> P j" for S I H P in allE)
```
```  1232 apply(rule_tac x=ia in exI)
```
```  1233 apply(simp add:same_state_def)
```
```  1234 apply(erule_tac x=ia and P="\<lambda>j. T j \<longrightarrow> (\<forall>i. H j i \<longrightarrow> (snd (d j i))=(snd (e j i)))" for T H d e in all_dupE,simp)
```
```  1235 apply(erule_tac x=ia and P="\<lambda>j. T j \<longrightarrow> (\<forall>i. H j i \<longrightarrow> (snd (d j i))=(snd (e j i)))" for T H d e in allE,simp)
```
```  1236 apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in all_dupE)
```
```  1237 apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in all_dupE,simp)
```
```  1238 apply(erule_tac x="Suc i" and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE,simp)
```
```  1239 apply(erule mp)
```
```  1240 apply(subgoal_tac "r=fst(clist ! ia ! Suc i)",simp)
```
```  1241 apply(drule_tac i=ia in list_eq_if)
```
```  1242 back
```
```  1243 apply simp_all
```
```  1244 done
```
```  1245
```
```  1246 lemma parcptn_not_empty [simp]:"[] \<notin> par_cptn"
```
```  1247 apply(force elim:par_cptn.cases)
```
```  1248 done
```
```  1249
```
```  1250 lemma five:
```
```  1251   "\<lbrakk>xs\<noteq>[]; \<forall>i<length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j))
```
```  1252    \<subseteq> Rely (xs ! i);
```
```  1253    pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i));
```
```  1254    (\<Inter>i\<in>{i. i < length xs}. Post (xs ! i)) \<subseteq> post;
```
```  1255    \<forall>i < length xs.
```
```  1256     \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
```
```  1257     x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum (pre, rely);
```
```  1258    All_None (fst (last x)) \<rbrakk> \<Longrightarrow> snd (last x) \<in> post"
```
```  1259 apply(simp add: ParallelCom_def)
```
```  1260 apply(subgoal_tac "(map (Some \<circ> fst) xs)\<noteq>[]")
```
```  1261  prefer 2
```
```  1262  apply simp
```
```  1263 apply(frule rev_subsetD)
```
```  1264  apply(erule one [THEN equalityD1])
```
```  1265 apply(erule subsetD)
```
```  1266 apply simp
```
```  1267 apply clarify
```
```  1268 apply(subgoal_tac "\<forall>i<length clist. clist!i\<in>assum(Pre(xs!i), Rely(xs!i))")
```
```  1269  apply(erule_tac x=xa and P="\<lambda>i. H i \<longrightarrow> \<Turnstile> (J i) sat [I i,K i,M i,N i]" for H J I K M N in allE,erule impE,assumption)
```
```  1270  apply(simp add:com_validity_def)
```
```  1271  apply(erule_tac x=s in allE)
```
```  1272  apply(erule_tac x=xa and P="\<lambda>j. H j \<longrightarrow> (I j) \<in> cp (J j) s" for H I J in allE,simp)
```
```  1273  apply(drule_tac c="clist!xa" in subsetD)
```
```  1274   apply (force simp add:Com_def)
```
```  1275  apply(simp add:comm_def conjoin_def same_program_def del:last.simps)
```
```  1276  apply clarify
```
```  1277  apply(erule_tac x="length x - 1" and P="\<lambda>j. H j \<longrightarrow> fst(I j)=(J j)" for H I J in allE)
```
```  1278  apply (simp add:All_None_def same_length_def)
```
```  1279  apply(erule_tac x=xa and P="\<lambda>j. H j \<longrightarrow> length(J j)=(K j)" for H J K in allE)
```
```  1280  apply(subgoal_tac "length x - 1 < length x",simp)
```
```  1281   apply(case_tac "x\<noteq>[]")
```
```  1282    apply(simp add: last_conv_nth)
```
```  1283    apply(erule_tac x="clist!xa" in ballE)
```
```  1284     apply(simp add:same_state_def)
```
```  1285     apply(subgoal_tac "clist!xa\<noteq>[]")
```
```  1286      apply(simp add: last_conv_nth)
```
```  1287     apply(case_tac x)
```
```  1288      apply (force simp add:par_cp_def)
```
```  1289     apply (force simp add:par_cp_def)
```
```  1290    apply force
```
```  1291   apply (force simp add:par_cp_def)
```
```  1292  apply(case_tac x)
```
```  1293   apply (force simp add:par_cp_def)
```
```  1294  apply (force simp add:par_cp_def)
```
```  1295 apply clarify
```
```  1296 apply(simp add:assum_def)
```
```  1297 apply(rule conjI)
```
```  1298  apply(simp add:conjoin_def same_state_def par_cp_def)
```
```  1299  apply clarify
```
```  1300  apply(erule_tac x=i and P="\<lambda>j. T j \<longrightarrow> (\<forall>i. H j i \<longrightarrow> (snd (d j i))=(snd (e j i)))" for T H d e in allE,simp)
```
```  1301  apply(erule_tac x=0 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE)
```
```  1302  apply(case_tac x,simp+)
```
```  1303  apply (simp add:par_assum_def)
```
```  1304  apply clarify
```
```  1305  apply(drule_tac c="snd (clist ! i ! 0)" in subsetD)
```
```  1306  apply assumption
```
```  1307  apply simp
```
```  1308 apply clarify
```
```  1309 apply(erule_tac x=i in all_dupE)
```
```  1310 apply(rule subsetD, erule mp, assumption)
```
```  1311 apply(erule_tac pre=pre and rely=rely and x=x and s=s in  three)
```
```  1312  apply(erule_tac x=ib in allE,erule mp)
```
```  1313  apply simp_all
```
```  1314  apply(simp add:ParallelCom_def)
```
```  1315  apply(force simp add:Com_def)
```
```  1316 apply(simp add:conjoin_def same_length_def)
```
```  1317 done
```
```  1318
```
```  1319 lemma ParallelEmpty [rule_format]:
```
```  1320   "\<forall>i s. x \<in> par_cp (ParallelCom []) s \<longrightarrow>
```
```  1321   Suc i < length x \<longrightarrow> (x ! i, x ! Suc i) \<notin> par_ctran"
```
```  1322 apply(induct_tac x)
```
```  1323  apply(simp add:par_cp_def ParallelCom_def)
```
```  1324 apply clarify
```
```  1325 apply(case_tac list,simp,simp)
```
```  1326 apply(case_tac i)
```
```  1327  apply(simp add:par_cp_def ParallelCom_def)
```
```  1328  apply(erule par_ctranE,simp)
```
```  1329 apply(simp add:par_cp_def ParallelCom_def)
```
```  1330 apply clarify
```
```  1331 apply(erule par_cptn.cases,simp)
```
```  1332  apply simp
```
```  1333 apply(erule par_ctranE)
```
```  1334 back
```
```  1335 apply simp
```
```  1336 done
```
```  1337
```
```  1338 theorem par_rgsound:
```
```  1339   "\<turnstile> c SAT [pre, rely, guar, post] \<Longrightarrow>
```
```  1340    \<Turnstile> (ParallelCom c) SAT [pre, rely, guar, post]"
```
```  1341 apply(erule par_rghoare.induct)
```
```  1342 apply(case_tac xs,simp)
```
```  1343  apply(simp add:par_com_validity_def par_comm_def)
```
```  1344  apply clarify
```
```  1345  apply(case_tac "post=UNIV",simp)
```
```  1346   apply clarify
```
```  1347   apply(drule ParallelEmpty)
```
```  1348    apply assumption
```
```  1349   apply simp
```
```  1350  apply clarify
```
```  1351  apply simp
```
```  1352 apply(subgoal_tac "xs\<noteq>[]")
```
```  1353  prefer 2
```
```  1354  apply simp
```
```  1355 apply(rename_tac a list)
```
```  1356 apply(thin_tac "xs = a # list")
```
```  1357 apply(simp add:par_com_validity_def par_comm_def)
```
```  1358 apply clarify
```
```  1359 apply(rule conjI)
```
```  1360  apply clarify
```
```  1361  apply(erule_tac pre=pre and rely=rely and guar=guar and x=x and s=s and xs=xs in four)
```
```  1362         apply(assumption+)
```
```  1363      apply clarify
```
```  1364      apply (erule allE, erule impE, assumption,erule rgsound)
```
```  1365     apply(assumption+)
```
```  1366 apply clarify
```
```  1367 apply(erule_tac pre=pre and rely=rely and post=post and x=x and s=s and xs=xs in five)
```
```  1368       apply(assumption+)
```
```  1369    apply clarify
```
```  1370    apply (erule allE, erule impE, assumption,erule rgsound)
```
```  1371   apply(assumption+)
```
```  1372 done
```
```  1373
```
```  1374 end
```