src/HOL/Hoare_Parallel/RG_Hoare.thy
author wenzelm
Thu May 24 17:25:53 2012 +0200 (2012-05-24)
changeset 47988 e4b69e10b990
parent 42174 d0be2722ce9f
child 52597 a8a81453833d
permissions -rw-r--r--
tuned proofs;
     1 header {* \section{The Proof System} *}
     2 
     3 theory RG_Hoare imports RG_Tran begin
     4 
     5 subsection {* Proof System for Component Programs *}
     6 
     7 declare Un_subset_iff [simp del] le_sup_iff [simp del]
     8 declare Cons_eq_map_conv [iff]
     9 
    10 definition stable :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" where  
    11   "stable \<equiv> \<lambda>f g. (\<forall>x y. x \<in> f \<longrightarrow> (x, y) \<in> g \<longrightarrow> y \<in> f)" 
    12 
    13 inductive
    14   rghoare :: "['a com, 'a set, ('a \<times> 'a) set, ('a \<times> 'a) set, 'a set] \<Rightarrow> bool"  
    15     ("\<turnstile> _ sat [_, _, _, _]" [60,0,0,0,0] 45)
    16 where
    17   Basic: "\<lbrakk> pre \<subseteq> {s. f s \<in> post}; {(s,t). s \<in> pre \<and> (t=f s \<or> t=s)} \<subseteq> guar; 
    18             stable pre rely; stable post rely \<rbrakk> 
    19            \<Longrightarrow> \<turnstile> Basic f sat [pre, rely, guar, post]"
    20 
    21 | Seq: "\<lbrakk> \<turnstile> P sat [pre, rely, guar, mid]; \<turnstile> Q sat [mid, rely, guar, post] \<rbrakk> 
    22            \<Longrightarrow> \<turnstile> Seq P Q sat [pre, rely, guar, post]"
    23 
    24 | Cond: "\<lbrakk> stable pre rely; \<turnstile> P1 sat [pre \<inter> b, rely, guar, post];
    25            \<turnstile> P2 sat [pre \<inter> -b, rely, guar, post]; \<forall>s. (s,s)\<in>guar \<rbrakk>
    26           \<Longrightarrow> \<turnstile> Cond b P1 P2 sat [pre, rely, guar, post]"
    27 
    28 | While: "\<lbrakk> stable pre rely; (pre \<inter> -b) \<subseteq> post; stable post rely;
    29             \<turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s,s)\<in>guar \<rbrakk>
    30           \<Longrightarrow> \<turnstile> While b P sat [pre, rely, guar, post]"
    31 
    32 | Await: "\<lbrakk> stable pre rely; stable post rely; 
    33             \<forall>V. \<turnstile> P sat [pre \<inter> b \<inter> {V}, {(s, t). s = t}, 
    34                 UNIV, {s. (V, s) \<in> guar} \<inter> post] \<rbrakk>
    35            \<Longrightarrow> \<turnstile> Await b P sat [pre, rely, guar, post]"
    36   
    37 | Conseq: "\<lbrakk> pre \<subseteq> pre'; rely \<subseteq> rely'; guar' \<subseteq> guar; post' \<subseteq> post;
    38              \<turnstile> P sat [pre', rely', guar', post'] \<rbrakk>
    39             \<Longrightarrow> \<turnstile> P sat [pre, rely, guar, post]"
    40 
    41 definition Pre :: "'a rgformula \<Rightarrow> 'a set" where
    42   "Pre x \<equiv> fst(snd x)"
    43 
    44 definition Post :: "'a rgformula \<Rightarrow> 'a set" where
    45   "Post x \<equiv> snd(snd(snd(snd x)))"
    46 
    47 definition Rely :: "'a rgformula \<Rightarrow> ('a \<times> 'a) set" where
    48   "Rely x \<equiv> fst(snd(snd x))"
    49 
    50 definition Guar :: "'a rgformula \<Rightarrow> ('a \<times> 'a) set" where
    51   "Guar x \<equiv> fst(snd(snd(snd x)))"
    52 
    53 definition Com :: "'a rgformula \<Rightarrow> 'a com" where
    54   "Com x \<equiv> fst x"
    55 
    56 subsection {* Proof System for Parallel Programs *}
    57 
    58 type_synonym 'a par_rgformula =
    59   "('a rgformula) list \<times> 'a set \<times> ('a \<times> 'a) set \<times> ('a \<times> 'a) set \<times> 'a set"
    60 
    61 inductive
    62   par_rghoare :: "('a rgformula) list \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set \<Rightarrow> bool"
    63     ("\<turnstile> _ SAT [_, _, _, _]" [60,0,0,0,0] 45)
    64 where
    65   Parallel: 
    66   "\<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);
    67     (\<Union>j\<in>{j. j<length xs}. Guar(xs!j)) \<subseteq> guar;
    68      pre \<subseteq> (\<Inter>i\<in>{i. i<length xs}. Pre(xs!i)); 
    69     (\<Inter>i\<in>{i. i<length xs}. Post(xs!i)) \<subseteq> post;
    70     \<forall>i<length xs. \<turnstile> Com(xs!i) sat [Pre(xs!i),Rely(xs!i),Guar(xs!i),Post(xs!i)] \<rbrakk>
    71    \<Longrightarrow>  \<turnstile> xs SAT [pre, rely, guar, post]"
    72 
    73 section {* Soundness*}
    74 
    75 subsubsection {* Some previous lemmas *}
    76 
    77 lemma tl_of_assum_in_assum: 
    78   "(P, s) # (P, t) # xs \<in> assum (pre, rely) \<Longrightarrow> stable pre rely 
    79   \<Longrightarrow> (P, t) # xs \<in> assum (pre, rely)"
    80 apply(simp add:assum_def)
    81 apply clarify
    82 apply(rule conjI)
    83  apply(erule_tac x=0 in allE)
    84  apply(simp (no_asm_use)only:stable_def)
    85  apply(erule allE,erule allE,erule impE,assumption,erule mp)
    86  apply(simp add:Env)
    87 apply clarify
    88 apply(erule_tac x="Suc i" in allE)
    89 apply simp
    90 done
    91 
    92 lemma etran_in_comm: 
    93   "(P, t) # xs \<in> comm(guar, post) \<Longrightarrow> (P, s) # (P, t) # xs \<in> comm(guar, post)"
    94 apply(simp add:comm_def)
    95 apply clarify
    96 apply(case_tac i,simp+)
    97 done
    98 
    99 lemma ctran_in_comm: 
   100   "\<lbrakk>(s, s) \<in> guar; (Q, s) # xs \<in> comm(guar, post)\<rbrakk> 
   101   \<Longrightarrow> (P, s) # (Q, s) # xs \<in> comm(guar, post)"
   102 apply(simp add:comm_def)
   103 apply clarify
   104 apply(case_tac i,simp+)
   105 done
   106 
   107 lemma takecptn_is_cptn [rule_format, elim!]: 
   108   "\<forall>j. c \<in> cptn \<longrightarrow> take (Suc j) c \<in> cptn"
   109 apply(induct "c")
   110  apply(force elim: cptn.cases)
   111 apply clarify
   112 apply(case_tac j) 
   113  apply simp
   114  apply(rule CptnOne)
   115 apply simp
   116 apply(force intro:cptn.intros elim:cptn.cases)
   117 done
   118 
   119 lemma dropcptn_is_cptn [rule_format,elim!]: 
   120   "\<forall>j<length c. c \<in> cptn \<longrightarrow> drop j c \<in> cptn"
   121 apply(induct "c")
   122  apply(force elim: cptn.cases)
   123 apply clarify
   124 apply(case_tac j,simp+) 
   125 apply(erule cptn.cases)
   126   apply simp
   127  apply force
   128 apply force
   129 done
   130 
   131 lemma takepar_cptn_is_par_cptn [rule_format,elim]: 
   132   "\<forall>j. c \<in> par_cptn \<longrightarrow> take (Suc j) c \<in> par_cptn"
   133 apply(induct "c")
   134  apply(force elim: cptn.cases)
   135 apply clarify
   136 apply(case_tac j,simp) 
   137  apply(rule ParCptnOne)
   138 apply(force intro:par_cptn.intros elim:par_cptn.cases)
   139 done
   140 
   141 lemma droppar_cptn_is_par_cptn [rule_format]:
   142   "\<forall>j<length c. c \<in> par_cptn \<longrightarrow> drop j c \<in> par_cptn"
   143 apply(induct "c")
   144  apply(force elim: par_cptn.cases)
   145 apply clarify
   146 apply(case_tac j,simp+) 
   147 apply(erule par_cptn.cases)
   148   apply simp
   149  apply force
   150 apply force
   151 done
   152 
   153 lemma tl_of_cptn_is_cptn: "\<lbrakk>x # xs \<in> cptn; xs \<noteq> []\<rbrakk> \<Longrightarrow> xs  \<in> cptn"
   154 apply(subgoal_tac "1 < length (x # xs)") 
   155  apply(drule dropcptn_is_cptn,simp+)
   156 done
   157 
   158 lemma not_ctran_None [rule_format]: 
   159   "\<forall>s. (None, s)#xs \<in> cptn \<longrightarrow> (\<forall>i<length xs. ((None, s)#xs)!i -e\<rightarrow> xs!i)"
   160 apply(induct xs,simp+)
   161 apply clarify
   162 apply(erule cptn.cases,simp)
   163  apply simp
   164  apply(case_tac i,simp)
   165   apply(rule Env)
   166  apply simp
   167 apply(force elim:ctran.cases)
   168 done
   169 
   170 lemma cptn_not_empty [simp]:"[] \<notin> cptn"
   171 apply(force elim:cptn.cases)
   172 done
   173 
   174 lemma etran_or_ctran [rule_format]: 
   175   "\<forall>m i. x\<in>cptn \<longrightarrow> m \<le> length x 
   176    \<longrightarrow> (\<forall>i. Suc i < m \<longrightarrow> \<not> x!i -c\<rightarrow> x!Suc i) \<longrightarrow> Suc i < m 
   177    \<longrightarrow> x!i -e\<rightarrow> x!Suc i"
   178 apply(induct x,simp)
   179 apply clarify
   180 apply(erule cptn.cases,simp)
   181  apply(case_tac i,simp)
   182   apply(rule Env)
   183  apply simp
   184  apply(erule_tac x="m - 1" in allE)
   185  apply(case_tac m,simp,simp)
   186  apply(subgoal_tac "(\<forall>i. Suc i < nata \<longrightarrow> (((P, t) # xs) ! i, xs ! i) \<notin> ctran)")
   187   apply force
   188  apply clarify
   189  apply(erule_tac x="Suc ia" in allE,simp)
   190 apply(erule_tac x="0" and P="\<lambda>j. ?H j \<longrightarrow> (?J j) \<notin> ctran" in allE,simp)
   191 done
   192 
   193 lemma etran_or_ctran2 [rule_format]: 
   194   "\<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)
   195   \<or> (x!i -e\<rightarrow> x!Suc i \<longrightarrow> \<not> x!i -c\<rightarrow> x!Suc i)"
   196 apply(induct x)
   197  apply simp
   198 apply clarify
   199 apply(erule cptn.cases,simp)
   200  apply(case_tac i,simp+)
   201 apply(case_tac i,simp)
   202  apply(force elim:etran.cases)
   203 apply simp
   204 done
   205 
   206 lemma etran_or_ctran2_disjI1: 
   207   "\<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"
   208 by(drule etran_or_ctran2,simp_all)
   209 
   210 lemma etran_or_ctran2_disjI2: 
   211   "\<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"
   212 by(drule etran_or_ctran2,simp_all)
   213 
   214 lemma not_ctran_None2 [rule_format]: 
   215   "\<lbrakk> (None, s) # xs \<in>cptn; i<length xs\<rbrakk> \<Longrightarrow> \<not> ((None, s) # xs) ! i -c\<rightarrow> xs ! i"
   216 apply(frule not_ctran_None,simp)
   217 apply(case_tac i,simp)
   218  apply(force elim:etranE)
   219 apply simp
   220 apply(rule etran_or_ctran2_disjI2,simp_all)
   221 apply(force intro:tl_of_cptn_is_cptn)
   222 done
   223 
   224 lemma Ex_first_occurrence [rule_format]: "P (n::nat) \<longrightarrow> (\<exists>m. P m \<and> (\<forall>i<m. \<not> P i))";
   225 apply(rule nat_less_induct)
   226 apply clarify
   227 apply(case_tac "\<forall>m. m<n \<longrightarrow> \<not> P m")
   228 apply auto
   229 done
   230  
   231 lemma stability [rule_format]: 
   232   "\<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>
   233   (\<forall>i. (Suc i)<length x \<longrightarrow> 
   234           (x!i -e\<rightarrow> x!(Suc i)) \<longrightarrow> (snd(x!i), snd(x!(Suc i))) \<in> rely) \<longrightarrow> 
   235   (\<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)"
   236 apply(induct x)
   237  apply clarify
   238  apply(force elim:cptn.cases)
   239 apply clarify
   240 apply(erule cptn.cases,simp)
   241  apply simp
   242  apply(case_tac k,simp,simp)
   243  apply(case_tac j,simp) 
   244   apply(erule_tac x=0 in allE)
   245   apply(erule_tac x="nat" and P="\<lambda>j. (0\<le>j) \<longrightarrow> (?J j)" in allE,simp)
   246   apply(subgoal_tac "t\<in>p")
   247    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)")
   248     apply clarify
   249     apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran" in allE,simp)
   250    apply clarify
   251    apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j) \<longrightarrow> (?T j)\<in>rely" in allE,simp)
   252   apply(erule_tac x=0 and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran \<longrightarrow> ?T j" in allE,simp)
   253   apply(simp(no_asm_use) only:stable_def)
   254   apply(erule_tac x=s in allE)
   255   apply(erule_tac x=t in allE)
   256   apply simp 
   257   apply(erule mp)
   258   apply(erule mp)
   259   apply(rule Env)
   260  apply simp
   261  apply(erule_tac x="nata" in allE)
   262  apply(erule_tac x="nat" and P="\<lambda>j. (?s\<le>j) \<longrightarrow> (?J j)" in allE,simp)
   263  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)")
   264   apply clarify
   265   apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran" in allE,simp)
   266  apply clarify
   267  apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j) \<longrightarrow> (?T j)\<in>rely" in allE,simp)
   268 apply(case_tac k,simp,simp)
   269 apply(case_tac j)
   270  apply(erule_tac x=0 and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran" in allE,simp)
   271  apply(erule etran.cases,simp)
   272 apply(erule_tac x="nata" in allE)
   273 apply(erule_tac x="nat" and P="\<lambda>j. (?s\<le>j) \<longrightarrow> (?J j)" in allE,simp)
   274 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)")
   275  apply clarify
   276  apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran" in allE,simp)
   277 apply clarify
   278 apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j) \<longrightarrow> (?T j)\<in>rely" in allE,simp)
   279 done
   280 
   281 subsection {* Soundness of the System for Component Programs *}
   282 
   283 subsubsection {* Soundness of the Basic rule *}
   284 
   285 lemma unique_ctran_Basic [rule_format]: 
   286   "\<forall>s i. x \<in> cptn \<longrightarrow> x ! 0 = (Some (Basic f), s) \<longrightarrow> 
   287   Suc i<length x \<longrightarrow> x!i -c\<rightarrow> x!Suc i \<longrightarrow> 
   288   (\<forall>j. Suc j<length x \<longrightarrow> i\<noteq>j \<longrightarrow> x!j -e\<rightarrow> x!Suc j)"
   289 apply(induct x,simp)
   290 apply simp
   291 apply clarify
   292 apply(erule cptn.cases,simp)
   293  apply(case_tac i,simp+)
   294  apply clarify
   295  apply(case_tac j,simp)
   296   apply(rule Env)
   297  apply simp
   298 apply clarify
   299 apply simp
   300 apply(case_tac i)
   301  apply(case_tac j,simp,simp)
   302  apply(erule ctran.cases,simp_all)
   303  apply(force elim: not_ctran_None)
   304 apply(ind_cases "((Some (Basic f), sa), Q, t) \<in> ctran" for sa Q t)
   305 apply simp
   306 apply(drule_tac i=nat in not_ctran_None,simp)
   307 apply(erule etranE,simp)
   308 done
   309 
   310 lemma exists_ctran_Basic_None [rule_format]: 
   311   "\<forall>s i. x \<in> cptn \<longrightarrow> x ! 0 = (Some (Basic f), s) 
   312   \<longrightarrow> i<length x \<longrightarrow> fst(x!i)=None \<longrightarrow> (\<exists>j<i. x!j -c\<rightarrow> x!Suc j)"
   313 apply(induct x,simp)
   314 apply simp
   315 apply clarify
   316 apply(erule cptn.cases,simp)
   317  apply(case_tac i,simp,simp)
   318  apply(erule_tac x=nat in allE,simp)
   319  apply clarify
   320  apply(rule_tac x="Suc j" in exI,simp,simp)
   321 apply clarify
   322 apply(case_tac i,simp,simp)
   323 apply(rule_tac x=0 in exI,simp)
   324 done
   325 
   326 lemma Basic_sound: 
   327   " \<lbrakk>pre \<subseteq> {s. f s \<in> post}; {(s, t). s \<in> pre \<and> t = f s} \<subseteq> guar; 
   328   stable pre rely; stable post rely\<rbrakk>
   329   \<Longrightarrow> \<Turnstile> Basic f sat [pre, rely, guar, post]"
   330 apply(unfold com_validity_def)
   331 apply clarify
   332 apply(simp add:comm_def)
   333 apply(rule conjI)
   334  apply clarify
   335  apply(simp add:cp_def assum_def)
   336  apply clarify
   337  apply(frule_tac j=0 and k=i and p=pre in stability)
   338        apply simp_all
   339    apply(erule_tac x=ia in allE,simp)
   340   apply(erule_tac i=i and f=f in unique_ctran_Basic,simp_all)
   341  apply(erule subsetD,simp)
   342  apply(case_tac "x!i")
   343  apply clarify
   344  apply(drule_tac s="Some (Basic f)" in sym,simp)
   345  apply(thin_tac "\<forall>j. ?H j")
   346  apply(force elim:ctran.cases)
   347 apply clarify
   348 apply(simp add:cp_def)
   349 apply clarify
   350 apply(frule_tac i="length x - 1" and f=f in exists_ctran_Basic_None,simp+)
   351   apply(case_tac x,simp+)
   352   apply(rule last_fst_esp,simp add:last_length)
   353  apply (case_tac x,simp+)
   354 apply(simp add:assum_def)
   355 apply clarify
   356 apply(frule_tac j=0 and k="j" and p=pre in stability)
   357       apply simp_all
   358   apply(erule_tac x=i in allE,simp)
   359  apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all)
   360 apply(case_tac "x!j")
   361 apply clarify
   362 apply simp
   363 apply(drule_tac s="Some (Basic f)" in sym,simp)
   364 apply(case_tac "x!Suc j",simp)
   365 apply(rule ctran.cases,simp)
   366 apply(simp_all)
   367 apply(drule_tac c=sa in subsetD,simp)
   368 apply clarify
   369 apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all)
   370  apply(case_tac x,simp+)
   371  apply(erule_tac x=i in allE)
   372 apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all)
   373   apply arith+
   374 apply(case_tac x)
   375 apply(simp add:last_length)+
   376 done
   377 
   378 subsubsection{* Soundness of the Await rule *}
   379 
   380 lemma unique_ctran_Await [rule_format]: 
   381   "\<forall>s i. x \<in> cptn \<longrightarrow> x ! 0 = (Some (Await b c), s) \<longrightarrow> 
   382   Suc i<length x \<longrightarrow> x!i -c\<rightarrow> x!Suc i \<longrightarrow> 
   383   (\<forall>j. Suc j<length x \<longrightarrow> i\<noteq>j \<longrightarrow> x!j -e\<rightarrow> x!Suc j)"
   384 apply(induct x,simp+)
   385 apply clarify
   386 apply(erule cptn.cases,simp)
   387  apply(case_tac i,simp+)
   388  apply clarify
   389  apply(case_tac j,simp)
   390   apply(rule Env)
   391  apply simp
   392 apply clarify
   393 apply simp
   394 apply(case_tac i)
   395  apply(case_tac j,simp,simp)
   396  apply(erule ctran.cases,simp_all)
   397  apply(force elim: not_ctran_None)
   398 apply(ind_cases "((Some (Await b c), sa), Q, t) \<in> ctran" for sa Q t,simp)
   399 apply(drule_tac i=nat in not_ctran_None,simp)
   400 apply(erule etranE,simp)
   401 done
   402 
   403 lemma exists_ctran_Await_None [rule_format]: 
   404   "\<forall>s i.  x \<in> cptn \<longrightarrow> x ! 0 = (Some (Await b c), s) 
   405   \<longrightarrow> i<length x \<longrightarrow> fst(x!i)=None \<longrightarrow> (\<exists>j<i. x!j -c\<rightarrow> x!Suc j)"
   406 apply(induct x,simp+)
   407 apply clarify
   408 apply(erule cptn.cases,simp)
   409  apply(case_tac i,simp+)
   410  apply(erule_tac x=nat in allE,simp)
   411  apply clarify
   412  apply(rule_tac x="Suc j" in exI,simp,simp)
   413 apply clarify
   414 apply(case_tac i,simp,simp)
   415 apply(rule_tac x=0 in exI,simp)
   416 done
   417 
   418 lemma Star_imp_cptn: 
   419   "(P, s) -c*\<rightarrow> (R, t) \<Longrightarrow> \<exists>l \<in> cp P s. (last l)=(R, t)
   420   \<and> (\<forall>i. Suc i<length l \<longrightarrow> l!i -c\<rightarrow> l!Suc i)"
   421 apply (erule converse_rtrancl_induct2)
   422  apply(rule_tac x="[(R,t)]" in bexI)
   423   apply simp
   424  apply(simp add:cp_def)
   425  apply(rule CptnOne)
   426 apply clarify
   427 apply(rule_tac x="(a, b)#l" in bexI)
   428  apply (rule conjI)
   429   apply(case_tac l,simp add:cp_def)
   430   apply(simp add:last_length)
   431  apply clarify
   432 apply(case_tac i,simp)
   433 apply(simp add:cp_def)
   434 apply force
   435 apply(simp add:cp_def)
   436  apply(case_tac l)
   437  apply(force elim:cptn.cases)
   438 apply simp
   439 apply(erule CptnComp)
   440 apply clarify
   441 done
   442  
   443 lemma Await_sound: 
   444   "\<lbrakk>stable pre rely; stable post rely;
   445   \<forall>V. \<turnstile> P sat [pre \<inter> b \<inter> {s. s = V}, {(s, t). s = t}, 
   446                  UNIV, {s. (V, s) \<in> guar} \<inter> post] \<and>
   447   \<Turnstile> P sat [pre \<inter> b \<inter> {s. s = V}, {(s, t). s = t}, 
   448                  UNIV, {s. (V, s) \<in> guar} \<inter> post] \<rbrakk>
   449   \<Longrightarrow> \<Turnstile> Await b P sat [pre, rely, guar, post]"
   450 apply(unfold com_validity_def)
   451 apply clarify
   452 apply(simp add:comm_def)
   453 apply(rule conjI)
   454  apply clarify
   455  apply(simp add:cp_def assum_def)
   456  apply clarify
   457  apply(frule_tac j=0 and k=i and p=pre in stability,simp_all)
   458    apply(erule_tac x=ia in allE,simp)
   459   apply(subgoal_tac "x\<in> cp (Some(Await b P)) s")
   460   apply(erule_tac i=i in unique_ctran_Await,force,simp_all)
   461   apply(simp add:cp_def)
   462 --{* here starts the different part. *}
   463  apply(erule ctran.cases,simp_all)
   464  apply(drule Star_imp_cptn) 
   465  apply clarify
   466  apply(erule_tac x=sa in allE)
   467  apply clarify
   468  apply(erule_tac x=sa in allE)
   469  apply(drule_tac c=l in subsetD)
   470   apply (simp add:cp_def)
   471   apply clarify
   472   apply(erule_tac x=ia and P="\<lambda>i. ?H i \<longrightarrow> (?J i,?I i)\<in>ctran" in allE,simp)
   473   apply(erule etranE,simp)
   474  apply simp
   475 apply clarify
   476 apply(simp add:cp_def)
   477 apply clarify
   478 apply(frule_tac i="length x - 1" in exists_ctran_Await_None,force)
   479   apply (case_tac x,simp+)
   480  apply(rule last_fst_esp,simp add:last_length)
   481  apply(case_tac x, (simp add:cptn_not_empty)+)
   482 apply clarify
   483 apply(simp add:assum_def)
   484 apply clarify
   485 apply(frule_tac j=0 and k="j" and p=pre in stability,simp_all)
   486   apply(erule_tac x=i in allE,simp)
   487  apply(erule_tac i=j in unique_ctran_Await,force,simp_all)
   488 apply(case_tac "x!j")
   489 apply clarify
   490 apply simp
   491 apply(drule_tac s="Some (Await b P)" in sym,simp)
   492 apply(case_tac "x!Suc j",simp)
   493 apply(rule ctran.cases,simp)
   494 apply(simp_all)
   495 apply(drule Star_imp_cptn) 
   496 apply clarify
   497 apply(erule_tac x=sa in allE)
   498 apply clarify
   499 apply(erule_tac x=sa in allE)
   500 apply(drule_tac c=l in subsetD)
   501  apply (simp add:cp_def)
   502  apply clarify
   503  apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> (?J i,?I i)\<in>ctran" in allE,simp)
   504  apply(erule etranE,simp)
   505 apply simp
   506 apply clarify
   507 apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all)
   508  apply(case_tac x,simp+)
   509  apply(erule_tac x=i in allE)
   510 apply(erule_tac i=j in unique_ctran_Await,force,simp_all)
   511  apply arith+
   512 apply(case_tac x)
   513 apply(simp add:last_length)+
   514 done
   515 
   516 subsubsection{* Soundness of the Conditional rule *}
   517 
   518 lemma Cond_sound: 
   519   "\<lbrakk> stable pre rely; \<Turnstile> P1 sat [pre \<inter> b, rely, guar, post]; 
   520   \<Turnstile> P2 sat [pre \<inter> - b, rely, guar, post]; \<forall>s. (s,s)\<in>guar\<rbrakk>
   521   \<Longrightarrow> \<Turnstile> (Cond b P1 P2) sat [pre, rely, guar, post]"
   522 apply(unfold com_validity_def)
   523 apply clarify
   524 apply(simp add:cp_def comm_def)
   525 apply(case_tac "\<exists>i. Suc i<length x \<and> x!i -c\<rightarrow> x!Suc i")
   526  prefer 2
   527  apply simp
   528  apply clarify
   529  apply(frule_tac j="0" and k="length x - 1" and p=pre in stability,simp+)
   530      apply(case_tac x,simp+)
   531     apply(simp add:assum_def)
   532    apply(simp add:assum_def)
   533   apply(erule_tac m="length x" in etran_or_ctran,simp+)
   534  apply(case_tac x, (simp add:last_length)+)
   535 apply(erule exE)
   536 apply(drule_tac n=i and P="\<lambda>i. ?H i \<and> (?J i,?I i)\<in> ctran" in Ex_first_occurrence)
   537 apply clarify
   538 apply (simp add:assum_def)
   539 apply(frule_tac j=0 and k="m" and p=pre in stability,simp+)
   540  apply(erule_tac m="Suc m" in etran_or_ctran,simp+)
   541 apply(erule ctran.cases,simp_all)
   542  apply(erule_tac x="sa" in allE)
   543  apply(drule_tac c="drop (Suc m) x" in subsetD)
   544   apply simp
   545   apply clarify
   546  apply simp
   547  apply clarify
   548  apply(case_tac "i\<le>m")
   549   apply(drule le_imp_less_or_eq)
   550   apply(erule disjE)
   551    apply(erule_tac x=i in allE, erule impE, assumption)
   552    apply simp+
   553  apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
   554  apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
   555   apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
   556    apply(rotate_tac -2)
   557    apply simp
   558   apply arith
   559  apply arith
   560 apply(case_tac "length (drop (Suc m) x)",simp)
   561 apply(erule_tac x="sa" in allE)
   562 back
   563 apply(drule_tac c="drop (Suc m) x" in subsetD,simp)
   564  apply clarify
   565 apply simp
   566 apply clarify
   567 apply(case_tac "i\<le>m")
   568  apply(drule le_imp_less_or_eq)
   569  apply(erule disjE)
   570   apply(erule_tac x=i in allE, erule impE, assumption)
   571   apply simp
   572  apply simp
   573 apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
   574 apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
   575  apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
   576   apply(rotate_tac -2)
   577   apply simp
   578  apply arith
   579 apply arith
   580 done
   581 
   582 subsubsection{* Soundness of the Sequential rule *}
   583 
   584 inductive_cases Seq_cases [elim!]: "(Some (Seq P Q), s) -c\<rightarrow> t"
   585 
   586 lemma last_lift_not_None: "fst ((lift Q) ((x#xs)!(length xs))) \<noteq> None"
   587 apply(subgoal_tac "length xs<length (x # xs)")
   588  apply(drule_tac Q=Q in  lift_nth)
   589  apply(erule ssubst)
   590  apply (simp add:lift_def)
   591  apply(case_tac "(x # xs) ! length xs",simp)
   592 apply simp
   593 done
   594 
   595 declare map_eq_Cons_conv [simp del] Cons_eq_map_conv [simp del]
   596 lemma Seq_sound1 [rule_format]: 
   597   "x\<in> cptn_mod \<Longrightarrow> \<forall>s P. x !0=(Some (Seq P Q), s) \<longrightarrow> 
   598   (\<forall>i<length x. fst(x!i)\<noteq>Some Q) \<longrightarrow> 
   599   (\<exists>xs\<in> cp (Some P) s. x=map (lift Q) xs)"
   600 apply(erule cptn_mod.induct)
   601 apply(unfold cp_def)
   602 apply safe
   603 apply simp_all
   604     apply(simp add:lift_def)
   605     apply(rule_tac x="[(Some Pa, sa)]" in exI,simp add:CptnOne)
   606    apply(subgoal_tac "(\<forall>i < Suc (length xs). fst (((Some (Seq Pa Q), t) # xs) ! i) \<noteq> Some Q)")
   607     apply clarify
   608     apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # zs" in exI,simp)
   609     apply(rule conjI,erule CptnEnv)
   610     apply(simp (no_asm_use) add:lift_def)
   611    apply clarify
   612    apply(erule_tac x="Suc i" in allE, simp)
   613   apply(ind_cases "((Some (Seq Pa Q), sa), None, t) \<in> ctran" for Pa sa t)
   614  apply(rule_tac x="(Some P, sa) # xs" in exI, simp add:cptn_iff_cptn_mod lift_def)
   615 apply(erule_tac x="length xs" in allE, simp)
   616 apply(simp only:Cons_lift_append)
   617 apply(subgoal_tac "length xs < length ((Some P, sa) # xs)")
   618  apply(simp only :nth_append length_map last_length nth_map)
   619  apply(case_tac "last((Some P, sa) # xs)")
   620  apply(simp add:lift_def)
   621 apply simp
   622 done
   623 declare map_eq_Cons_conv [simp del] Cons_eq_map_conv [simp del]
   624 
   625 lemma Seq_sound2 [rule_format]: 
   626   "x \<in> cptn \<Longrightarrow> \<forall>s P i. x!0=(Some (Seq P Q), s) \<longrightarrow> i<length x 
   627   \<longrightarrow> fst(x!i)=Some Q \<longrightarrow>
   628   (\<forall>j<i. fst(x!j)\<noteq>(Some Q)) \<longrightarrow>
   629   (\<exists>xs ys. xs \<in> cp (Some P) s \<and> length xs=Suc i 
   630    \<and> ys \<in> cp (Some Q) (snd(xs !i)) \<and> x=(map (lift Q) xs)@tl ys)"
   631 apply(erule cptn.induct)
   632 apply(unfold cp_def)
   633 apply safe
   634 apply simp_all
   635  apply(case_tac i,simp+)
   636  apply(erule allE,erule impE,assumption,simp)
   637  apply clarify
   638  apply(subgoal_tac "(\<forall>j < nat. fst (((Some (Seq Pa Q), t) # xs) ! j) \<noteq> Some Q)",clarify)
   639   prefer 2
   640   apply force
   641  apply(case_tac xsa,simp,simp)
   642  apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # list" in exI,simp)
   643  apply(rule conjI,erule CptnEnv)
   644  apply(simp (no_asm_use) add:lift_def)
   645  apply(rule_tac x=ys in exI,simp)
   646 apply(ind_cases "((Some (Seq Pa Q), sa), t) \<in> ctran" for Pa sa t)
   647  apply simp
   648  apply(rule_tac x="(Some Pa, sa)#[(None, ta)]" in exI,simp)
   649  apply(rule conjI)
   650   apply(drule_tac xs="[]" in CptnComp,force simp add:CptnOne,simp)
   651  apply(case_tac i, simp+)
   652  apply(case_tac nat,simp+)
   653  apply(rule_tac x="(Some Q,ta)#xs" in exI,simp add:lift_def)
   654  apply(case_tac nat,simp+)
   655  apply(force)
   656 apply(case_tac i, simp+)
   657 apply(case_tac nat,simp+)
   658 apply(erule_tac x="Suc nata" in allE,simp)
   659 apply clarify
   660 apply(subgoal_tac "(\<forall>j<Suc nata. fst (((Some (Seq P2 Q), ta) # xs) ! j) \<noteq> Some Q)",clarify)
   661  prefer 2
   662  apply clarify
   663  apply force
   664 apply(rule_tac x="(Some Pa, sa)#(Some P2, ta)#(tl xsa)" in exI,simp)
   665 apply(rule conjI,erule CptnComp)
   666 apply(rule nth_tl_if,force,simp+)
   667 apply(rule_tac x=ys in exI,simp)
   668 apply(rule conjI)
   669 apply(rule nth_tl_if,force,simp+)
   670  apply(rule tl_zero,simp+)
   671  apply force
   672 apply(rule conjI,simp add:lift_def)
   673 apply(subgoal_tac "lift Q (Some P2, ta) =(Some (Seq P2 Q), ta)") 
   674  apply(simp add:Cons_lift del:map.simps)
   675  apply(rule nth_tl_if)
   676    apply force
   677   apply simp+
   678 apply(simp add:lift_def)
   679 done
   680 (*
   681 lemma last_lift_not_None3: "fst (last (map (lift Q) (x#xs))) \<noteq> None"
   682 apply(simp only:last_length [THEN sym])
   683 apply(subgoal_tac "length xs<length (x # xs)")
   684  apply(drule_tac Q=Q in  lift_nth)
   685  apply(erule ssubst)
   686  apply (simp add:lift_def)
   687  apply(case_tac "(x # xs) ! length xs",simp)
   688 apply simp
   689 done
   690 *)
   691 
   692 lemma last_lift_not_None2: "fst ((lift Q) (last (x#xs))) \<noteq> None"
   693 apply(simp only:last_length [THEN sym])
   694 apply(subgoal_tac "length xs<length (x # xs)")
   695  apply(drule_tac Q=Q in  lift_nth)
   696  apply(erule ssubst)
   697  apply (simp add:lift_def)
   698  apply(case_tac "(x # xs) ! length xs",simp)
   699 apply simp
   700 done
   701 
   702 lemma Seq_sound: 
   703   "\<lbrakk>\<Turnstile> P sat [pre, rely, guar, mid]; \<Turnstile> Q sat [mid, rely, guar, post]\<rbrakk>
   704   \<Longrightarrow> \<Turnstile> Seq P Q sat [pre, rely, guar, post]"
   705 apply(unfold com_validity_def)
   706 apply clarify
   707 apply(case_tac "\<exists>i<length x. fst(x!i)=Some Q")
   708  prefer 2
   709  apply (simp add:cp_def cptn_iff_cptn_mod)
   710  apply clarify
   711  apply(frule_tac Seq_sound1,force)
   712   apply force
   713  apply clarify
   714  apply(erule_tac x=s in allE,simp)
   715  apply(drule_tac c=xs in subsetD,simp add:cp_def cptn_iff_cptn_mod)
   716   apply(simp add:assum_def)
   717   apply clarify
   718   apply(erule_tac P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE,erule impE, assumption)
   719   apply(simp add:snd_lift)
   720   apply(erule mp)
   721   apply(force elim:etranE intro:Env simp add:lift_def)
   722  apply(simp add:comm_def)
   723  apply(rule conjI)
   724   apply clarify
   725   apply(erule_tac P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE,erule impE, assumption)
   726   apply(simp add:snd_lift)
   727   apply(erule mp)
   728   apply(case_tac "(xs!i)")
   729   apply(case_tac "(xs! Suc i)")
   730   apply(case_tac "fst(xs!i)")
   731    apply(erule_tac x=i in allE, simp add:lift_def)
   732   apply(case_tac "fst(xs!Suc i)")
   733    apply(force simp add:lift_def)
   734   apply(force simp add:lift_def)
   735  apply clarify
   736  apply(case_tac xs,simp add:cp_def)
   737  apply clarify
   738  apply (simp del:map.simps)
   739  apply(subgoal_tac "(map (lift Q) ((a, b) # list))\<noteq>[]")
   740   apply(drule last_conv_nth)
   741   apply (simp del:map.simps)
   742   apply(simp only:last_lift_not_None)
   743  apply simp
   744 --{* @{text "\<exists>i<length x. fst (x ! i) = Some Q"} *}
   745 apply(erule exE)
   746 apply(drule_tac n=i and P="\<lambda>i. i < length x \<and> fst (x ! i) = Some Q" in Ex_first_occurrence)
   747 apply clarify
   748 apply (simp add:cp_def)
   749  apply clarify
   750  apply(frule_tac i=m in Seq_sound2,force)
   751   apply simp+
   752 apply clarify
   753 apply(simp add:comm_def)
   754 apply(erule_tac x=s in allE)
   755 apply(drule_tac c=xs in subsetD,simp)
   756  apply(case_tac "xs=[]",simp)
   757  apply(simp add:cp_def assum_def nth_append)
   758  apply clarify
   759  apply(erule_tac x=i in allE)
   760   back 
   761  apply(simp add:snd_lift)
   762  apply(erule mp)
   763  apply(force elim:etranE intro:Env simp add:lift_def)
   764 apply simp
   765 apply clarify
   766 apply(erule_tac x="snd(xs!m)" in allE)
   767 apply(drule_tac c=ys in subsetD,simp add:cp_def assum_def)
   768  apply(case_tac "xs\<noteq>[]")
   769  apply(drule last_conv_nth,simp)
   770  apply(rule conjI)
   771   apply(erule mp)
   772   apply(case_tac "xs!m")
   773   apply(case_tac "fst(xs!m)",simp)
   774   apply(simp add:lift_def nth_append)
   775  apply clarify
   776  apply(erule_tac x="m+i" in allE)
   777  back
   778  back
   779  apply(case_tac ys,(simp add:nth_append)+)
   780  apply (case_tac i, (simp add:snd_lift)+)
   781   apply(erule mp)
   782   apply(case_tac "xs!m")
   783   apply(force elim:etran.cases intro:Env simp add:lift_def)
   784  apply simp 
   785 apply simp
   786 apply clarify
   787 apply(rule conjI,clarify)
   788  apply(case_tac "i<m",simp add:nth_append)
   789   apply(simp add:snd_lift)
   790   apply(erule allE, erule impE, assumption, erule mp)
   791   apply(case_tac "(xs ! i)")
   792   apply(case_tac "(xs ! Suc i)")   
   793   apply(case_tac "fst(xs ! i)",force simp add:lift_def)   
   794   apply(case_tac "fst(xs ! Suc i)")
   795    apply (force simp add:lift_def)
   796   apply (force simp add:lift_def)
   797  apply(erule_tac x="i-m" in allE) 
   798  back
   799  back
   800  apply(subgoal_tac "Suc (i - m) < length ys",simp)
   801   prefer 2
   802   apply arith
   803  apply(simp add:nth_append snd_lift)
   804  apply(rule conjI,clarify)
   805   apply(subgoal_tac "i=m")
   806    prefer 2
   807    apply arith
   808   apply clarify
   809   apply(simp add:cp_def)
   810   apply(rule tl_zero)
   811     apply(erule mp)
   812     apply(case_tac "lift Q (xs!m)",simp add:snd_lift)
   813     apply(case_tac "xs!m",case_tac "fst(xs!m)",simp add:lift_def snd_lift)
   814      apply(case_tac ys,simp+)
   815     apply(simp add:lift_def)
   816    apply simp 
   817   apply force
   818  apply clarify
   819  apply(rule tl_zero)
   820    apply(rule tl_zero)
   821      apply (subgoal_tac "i-m=Suc(i-Suc m)")
   822       apply simp
   823       apply(erule mp)
   824       apply(case_tac ys,simp+)
   825    apply force
   826   apply arith
   827  apply force
   828 apply clarify
   829 apply(case_tac "(map (lift Q) xs @ tl ys)\<noteq>[]")
   830  apply(drule last_conv_nth)
   831  apply(simp add: snd_lift nth_append)
   832  apply(rule conjI,clarify)
   833   apply(case_tac ys,simp+)
   834  apply clarify
   835  apply(case_tac ys,simp+)
   836 done
   837 
   838 subsubsection{* Soundness of the While rule *}
   839 
   840 lemma last_append[rule_format]:
   841   "\<forall>xs. ys\<noteq>[] \<longrightarrow> ((xs@ys)!(length (xs@ys) - (Suc 0)))=(ys!(length ys - (Suc 0)))"
   842 apply(induct ys)
   843  apply simp
   844 apply clarify
   845 apply (simp add:nth_append length_append)
   846 done
   847 
   848 lemma assum_after_body: 
   849   "\<lbrakk> \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; 
   850   (Some P, s) # xs \<in> cptn_mod; fst (last ((Some P, s) # xs)) = None; s \<in> b;
   851   (Some (While b P), s) # (Some (Seq P (While b P)), s) # 
   852    map (lift (While b P)) xs @ ys \<in> assum (pre, rely)\<rbrakk>
   853   \<Longrightarrow> (Some (While b P), snd (last ((Some P, s) # xs))) # ys \<in> assum (pre, rely)"
   854 apply(simp add:assum_def com_validity_def cp_def cptn_iff_cptn_mod)
   855 apply clarify
   856 apply(erule_tac x=s in allE)
   857 apply(drule_tac c="(Some P, s) # xs" in subsetD,simp)
   858  apply clarify
   859  apply(erule_tac x="Suc i" in allE)
   860  apply simp
   861  apply(simp add:Cons_lift_append nth_append snd_lift del:map.simps)
   862  apply(erule mp)
   863  apply(erule etranE,simp)
   864  apply(case_tac "fst(((Some P, s) # xs) ! i)")
   865   apply(force intro:Env simp add:lift_def)
   866  apply(force intro:Env simp add:lift_def)
   867 apply(rule conjI)
   868  apply clarify
   869  apply(simp add:comm_def last_length)
   870 apply clarify
   871 apply(rule conjI)
   872  apply(simp add:comm_def)
   873 apply clarify
   874 apply(erule_tac x="Suc(length xs + i)" in allE,simp)
   875 apply(case_tac i, simp add:nth_append Cons_lift_append snd_lift last_conv_nth lift_def split_def)
   876 apply(simp add:Cons_lift_append nth_append snd_lift)
   877 done
   878 
   879 lemma While_sound_aux [rule_format]: 
   880   "\<lbrakk> pre \<inter> - b \<subseteq> post; \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s, s) \<in> guar;
   881    stable pre rely;  stable post rely; x \<in> cptn_mod \<rbrakk> 
   882   \<Longrightarrow>  \<forall>s xs. x=(Some(While b P),s)#xs \<longrightarrow> x\<in>assum(pre, rely) \<longrightarrow> x \<in> comm (guar, post)"
   883 apply(erule cptn_mod.induct)
   884 apply safe
   885 apply (simp_all del:last.simps)
   886 --{* 5 subgoals left *}
   887 apply(simp add:comm_def)
   888 --{* 4 subgoals left *}
   889 apply(rule etran_in_comm)
   890 apply(erule mp)
   891 apply(erule tl_of_assum_in_assum,simp)
   892 --{* While-None *}
   893 apply(ind_cases "((Some (While b P), s), None, t) \<in> ctran" for s t)
   894 apply(simp add:comm_def)
   895 apply(simp add:cptn_iff_cptn_mod [THEN sym])
   896 apply(rule conjI,clarify)
   897  apply(force simp add:assum_def)
   898 apply clarify
   899 apply(rule conjI, clarify)
   900  apply(case_tac i,simp,simp)
   901  apply(force simp add:not_ctran_None2)
   902 apply(subgoal_tac "\<forall>i. Suc i < length ((None, t) # xs) \<longrightarrow> (((None, t) # xs) ! i, ((None, t) # xs) ! Suc i)\<in> etran")
   903  prefer 2
   904  apply clarify
   905  apply(rule_tac m="length ((None, s) # xs)" in etran_or_ctran,simp+)
   906  apply(erule not_ctran_None2,simp)
   907  apply simp+
   908 apply(frule_tac j="0" and k="length ((None, s) # xs) - 1" and p=post in stability,simp+)
   909    apply(force simp add:assum_def subsetD)
   910   apply(simp add:assum_def)
   911   apply clarify
   912   apply(erule_tac x="i" in allE,simp) 
   913   apply(erule_tac x="Suc i" in allE,simp) 
   914  apply simp
   915 apply clarify
   916 apply (simp add:last_length)
   917 --{* WhileOne *}
   918 apply(thin_tac "P = While b P \<longrightarrow> ?Q")
   919 apply(rule ctran_in_comm,simp)
   920 apply(simp add:Cons_lift del:map.simps)
   921 apply(simp add:comm_def del:map.simps)
   922 apply(rule conjI)
   923  apply clarify
   924  apply(case_tac "fst(((Some P, sa) # xs) ! i)")
   925   apply(case_tac "((Some P, sa) # xs) ! i")
   926   apply (simp add:lift_def)
   927   apply(ind_cases "(Some (While b P), ba) -c\<rightarrow> t" for ba t)
   928    apply simp
   929   apply simp
   930  apply(simp add:snd_lift del:map.simps)
   931  apply(simp only:com_validity_def cp_def cptn_iff_cptn_mod)
   932  apply(erule_tac x=sa in allE)
   933  apply(drule_tac c="(Some P, sa) # xs" in subsetD)
   934   apply (simp add:assum_def del:map.simps)
   935   apply clarify
   936   apply(erule_tac x="Suc ia" in allE,simp add:snd_lift del:map.simps)
   937   apply(erule mp)
   938   apply(case_tac "fst(((Some P, sa) # xs) ! ia)")
   939    apply(erule etranE,simp add:lift_def)
   940    apply(rule Env)
   941   apply(erule etranE,simp add:lift_def)
   942   apply(rule Env)
   943  apply (simp add:comm_def del:map.simps)
   944  apply clarify
   945  apply(erule allE,erule impE,assumption)
   946  apply(erule mp)
   947  apply(case_tac "((Some P, sa) # xs) ! i")
   948  apply(case_tac "xs!i")
   949  apply(simp add:lift_def)
   950  apply(case_tac "fst(xs!i)")
   951   apply force
   952  apply force
   953 --{* last=None *}
   954 apply clarify
   955 apply(subgoal_tac "(map (lift (While b P)) ((Some P, sa) # xs))\<noteq>[]")
   956  apply(drule last_conv_nth)
   957  apply (simp del:map.simps)
   958  apply(simp only:last_lift_not_None)
   959 apply simp
   960 --{* WhileMore *}
   961 apply(thin_tac "P = While b P \<longrightarrow> ?Q")
   962 apply(rule ctran_in_comm,simp del:last.simps)
   963 --{* metiendo la hipotesis antes de dividir la conclusion. *}
   964 apply(subgoal_tac "(Some (While b P), snd (last ((Some P, sa) # xs))) # ys \<in> assum (pre, rely)")
   965  apply (simp del:last.simps)
   966  prefer 2
   967  apply(erule assum_after_body)
   968   apply (simp del:last.simps)+
   969 --{* lo de antes. *}
   970 apply(simp add:comm_def del:map.simps last.simps)
   971 apply(rule conjI)
   972  apply clarify
   973  apply(simp only:Cons_lift_append)
   974  apply(case_tac "i<length xs")
   975   apply(simp add:nth_append del:map.simps last.simps)
   976   apply(case_tac "fst(((Some P, sa) # xs) ! i)")
   977    apply(case_tac "((Some P, sa) # xs) ! i")
   978    apply (simp add:lift_def del:last.simps)
   979    apply(ind_cases "(Some (While b P), ba) -c\<rightarrow> t" for ba t)
   980     apply simp
   981    apply simp
   982   apply(simp add:snd_lift del:map.simps last.simps)
   983   apply(thin_tac " \<forall>i. i < length ys \<longrightarrow> ?P i")
   984   apply(simp only:com_validity_def cp_def cptn_iff_cptn_mod)
   985   apply(erule_tac x=sa in allE)
   986   apply(drule_tac c="(Some P, sa) # xs" in subsetD)
   987    apply (simp add:assum_def del:map.simps last.simps)
   988    apply clarify
   989    apply(erule_tac x="Suc ia" in allE,simp add:nth_append snd_lift del:map.simps last.simps, erule mp)
   990    apply(case_tac "fst(((Some P, sa) # xs) ! ia)")
   991     apply(erule etranE,simp add:lift_def)
   992     apply(rule Env)
   993    apply(erule etranE,simp add:lift_def)
   994    apply(rule Env)
   995   apply (simp add:comm_def del:map.simps)
   996   apply clarify
   997   apply(erule allE,erule impE,assumption)
   998   apply(erule mp)
   999   apply(case_tac "((Some P, sa) # xs) ! i")
  1000   apply(case_tac "xs!i")
  1001   apply(simp add:lift_def)
  1002   apply(case_tac "fst(xs!i)")
  1003    apply force
  1004  apply force
  1005 --{*  @{text "i \<ge> length xs"} *}
  1006 apply(subgoal_tac "i-length xs <length ys") 
  1007  prefer 2
  1008  apply arith
  1009 apply(erule_tac x="i-length xs" in allE,clarify)
  1010 apply(case_tac "i=length xs")
  1011  apply (simp add:nth_append snd_lift del:map.simps last.simps)
  1012  apply(simp add:last_length del:last.simps)
  1013  apply(erule mp)
  1014  apply(case_tac "last((Some P, sa) # xs)")
  1015  apply(simp add:lift_def del:last.simps)
  1016 --{* @{text "i>length xs"} *} 
  1017 apply(case_tac "i-length xs")
  1018  apply arith
  1019 apply(simp add:nth_append del:map.simps last.simps)
  1020 apply(rotate_tac -3)
  1021 apply(subgoal_tac "i- Suc (length xs)=nat")
  1022  prefer 2
  1023  apply arith
  1024 apply simp
  1025 --{* last=None *}
  1026 apply clarify
  1027 apply(case_tac ys)
  1028  apply(simp add:Cons_lift del:map.simps last.simps)
  1029  apply(subgoal_tac "(map (lift (While b P)) ((Some P, sa) # xs))\<noteq>[]")
  1030   apply(drule last_conv_nth)
  1031   apply (simp del:map.simps)
  1032   apply(simp only:last_lift_not_None)
  1033  apply simp
  1034 apply(subgoal_tac "((Some (Seq P (While b P)), sa) # map (lift (While b P)) xs @ ys)\<noteq>[]")
  1035  apply(drule last_conv_nth)
  1036  apply (simp del:map.simps last.simps)
  1037  apply(simp add:nth_append del:last.simps)
  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:map.simps 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{* Soundness of the Rule of Consequence *}
  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 {* Soundness of the system for sequential component programs *}
  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 {* Soundness of the System for Parallel Programs *}
  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 --{* By contradiction: *}
  1111 apply (simp del: Un_subset_iff)
  1112 apply(erule exE)
  1113 --{* the first c-tran that does not satisfy the guarantee-condition is from @{text "\<sigma>_i"} at step @{text "m"}. *}
  1114 apply(drule_tac n=j and P="\<lambda>j. \<exists>i. ?H i j" in Ex_first_occurrence)
  1115 apply(erule exE)
  1116 apply clarify
  1117 --{* @{text "\<sigma>_i \<in> A(pre, rely_1)"} *}
  1118 apply(subgoal_tac "take (Suc (Suc m)) (clist!i) \<in> assum(Pre(xs!i), Rely(xs!i))")
  1119 --{* but this contradicts @{text "\<Turnstile> \<sigma>_i sat [pre_i,rely_i,guar_i,post_i]"} *}
  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]" 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" in allE)
  1130  apply (simp add:conjoin_def same_length_def)
  1131 apply(simp add:assum_def del: Un_subset_iff)
  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)" 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)" in allE)
  1139 apply(simp del: Un_subset_iff)
  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" in allE,simp)
  1145 --{* each etran in @{text "\<sigma>_1[0\<dots>m]"} corresponds to  *}
  1146 apply(erule disjE)
  1147 --{* a c-tran in some @{text "\<sigma>_{ib}"}  *}
  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)" 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)" 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)" 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)))" 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)))" in allE,simp)
  1163 --{* or an e-tran in @{text "\<sigma>"}, 
  1164 therefore it satisfies @{text "rely \<or> guar_{ib}"} *}
  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" 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)" 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)" in allE)
  1193 apply(erule_tac x=ia and P="\<lambda>j. ?S j \<longrightarrow> (?I j, ?H j)\<in> ctran \<longrightarrow> (?P j)" 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)))" 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)))" 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 del: Un_subset_iff)
  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 del: Un_subset_iff)
  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)" in all_dupE)
  1228 apply(erule_tac x="Suc i" and P="\<lambda>j. ?H j \<longrightarrow> fst(?I j)=(?J 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)" in allE)
  1231 apply(erule_tac x=ia and P="\<lambda>j. ?S j \<longrightarrow> (?I j, ?H j)\<in> ctran \<longrightarrow> (?P j)" 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)))" 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)))" in allE,simp)
  1236 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in all_dupE)
  1237 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in all_dupE,simp)
  1238 apply(erule_tac x="Suc i" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" 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 del: Un_subset_iff)
  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 del: Un_subset_iff)
  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=i and P="\<lambda>i. ?H i \<longrightarrow> \<Turnstile> (?J i) sat [?I i,?K i,?M i,?N i]" 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=i and P="\<lambda>j. ?H j \<longrightarrow> (?I j) \<in> cp (?J j) s" in allE,simp)
  1273  apply(drule_tac c="clist!i" 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)" in allE)
  1278  apply (simp add:All_None_def same_length_def)
  1279  apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> length(?J j)=(?K j)" 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!i" in ballE)
  1284     apply(simp add:same_state_def)
  1285     apply(subgoal_tac "clist!i\<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=ia and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in allE,simp)
  1301  apply(erule_tac x=0 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" 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 ! ia ! 0)" in subsetD)
  1306  apply assumption
  1307  apply simp
  1308 apply clarify
  1309 apply(erule_tac x=ia 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=ic 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(thin_tac "xs = a # list")
  1356 apply(simp add:par_com_validity_def par_comm_def)
  1357 apply clarify
  1358 apply(rule conjI)
  1359  apply clarify
  1360  apply(erule_tac pre=pre and rely=rely and guar=guar and x=x and s=s and xs=xs in four)
  1361         apply(assumption+)
  1362      apply clarify
  1363      apply (erule allE, erule impE, assumption,erule rgsound)
  1364     apply(assumption+)
  1365 apply clarify
  1366 apply(erule_tac pre=pre and rely=rely and post=post and x=x and s=s and xs=xs in five)
  1367       apply(assumption+)
  1368    apply clarify
  1369    apply (erule allE, erule impE, assumption,erule rgsound)
  1370   apply(assumption+) 
  1371 done
  1372 
  1373 end