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