src/HOL/Hoare_Parallel/OG_Hoare.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (20 months ago)
changeset 67022 49309fe530fd
parent 62390 842917225d56
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 OG_Hoare imports OG_Tran begin
     4 
     5 primrec assertions :: "'a ann_com \<Rightarrow> ('a assn) set" where
     6   "assertions (AnnBasic r f) = {r}"
     7 | "assertions (AnnSeq c1 c2) = assertions c1 \<union> assertions c2"
     8 | "assertions (AnnCond1 r b c1 c2) = {r} \<union> assertions c1 \<union> assertions c2"
     9 | "assertions (AnnCond2 r b c) = {r} \<union> assertions c"
    10 | "assertions (AnnWhile r b i c) = {r, i} \<union> assertions c"
    11 | "assertions (AnnAwait r b c) = {r}"
    12 
    13 primrec atomics :: "'a ann_com \<Rightarrow> ('a assn \<times> 'a com) set" where
    14   "atomics (AnnBasic r f) = {(r, Basic f)}"
    15 | "atomics (AnnSeq c1 c2) = atomics c1 \<union> atomics c2"
    16 | "atomics (AnnCond1 r b c1 c2) = atomics c1 \<union> atomics c2"
    17 | "atomics (AnnCond2 r b c) = atomics c"
    18 | "atomics (AnnWhile r b i c) = atomics c"
    19 | "atomics (AnnAwait r b c) = {(r \<inter> b, c)}"
    20 
    21 primrec com :: "'a ann_triple_op \<Rightarrow> 'a ann_com_op" where
    22   "com (c, q) = c"
    23 
    24 primrec post :: "'a ann_triple_op \<Rightarrow> 'a assn" where
    25   "post (c, q) = q"
    26 
    27 definition interfree_aux :: "('a ann_com_op \<times> 'a assn \<times> 'a ann_com_op) \<Rightarrow> bool" where
    28   "interfree_aux \<equiv> \<lambda>(co, q, co'). co'= None \<or>
    29                     (\<forall>(r,a) \<in> atomics (the co'). \<parallel>= (q \<inter> r) a q \<and>
    30                     (co = None \<or> (\<forall>p \<in> assertions (the co). \<parallel>= (p \<inter> r) a p)))"
    31 
    32 definition interfree :: "(('a ann_triple_op) list) \<Rightarrow> bool" where
    33   "interfree Ts \<equiv> \<forall>i j. i < length Ts \<and> j < length Ts \<and> i \<noteq> j \<longrightarrow>
    34                          interfree_aux (com (Ts!i), post (Ts!i), com (Ts!j)) "
    35 
    36 inductive
    37   oghoare :: "'a assn \<Rightarrow> 'a com \<Rightarrow> 'a assn \<Rightarrow> bool"  ("(3\<parallel>- _//_//_)" [90,55,90] 50)
    38   and ann_hoare :: "'a ann_com \<Rightarrow> 'a assn \<Rightarrow> bool"  ("(2\<turnstile> _// _)" [60,90] 45)
    39 where
    40   AnnBasic: "r \<subseteq> {s. f s \<in> q} \<Longrightarrow> \<turnstile> (AnnBasic r f) q"
    41 
    42 | AnnSeq:   "\<lbrakk> \<turnstile> c0 pre c1; \<turnstile> c1 q \<rbrakk> \<Longrightarrow> \<turnstile> (AnnSeq c0 c1) q"
    43 
    44 | AnnCond1: "\<lbrakk> r \<inter> b \<subseteq> pre c1; \<turnstile> c1 q; r \<inter> -b \<subseteq> pre c2; \<turnstile> c2 q\<rbrakk>
    45               \<Longrightarrow> \<turnstile> (AnnCond1 r b c1 c2) q"
    46 | AnnCond2: "\<lbrakk> r \<inter> b \<subseteq> pre c; \<turnstile> c q; r \<inter> -b \<subseteq> q \<rbrakk> \<Longrightarrow> \<turnstile> (AnnCond2 r b c) q"
    47 
    48 | AnnWhile: "\<lbrakk> r \<subseteq> i; i \<inter> b \<subseteq> pre c; \<turnstile> c i; i \<inter> -b \<subseteq> q \<rbrakk>
    49               \<Longrightarrow> \<turnstile> (AnnWhile r b i c) q"
    50 
    51 | AnnAwait:  "\<lbrakk> atom_com c; \<parallel>- (r \<inter> b) c q \<rbrakk> \<Longrightarrow> \<turnstile> (AnnAwait r b c) q"
    52 
    53 | AnnConseq: "\<lbrakk>\<turnstile> c q; q \<subseteq> q' \<rbrakk> \<Longrightarrow> \<turnstile> c q'"
    54 
    55 
    56 | Parallel: "\<lbrakk> \<forall>i<length Ts. \<exists>c q. Ts!i = (Some c, q) \<and> \<turnstile> c q; interfree Ts \<rbrakk>
    57            \<Longrightarrow> \<parallel>- (\<Inter>i\<in>{i. i<length Ts}. pre(the(com(Ts!i))))
    58                      Parallel Ts
    59                   (\<Inter>i\<in>{i. i<length Ts}. post(Ts!i))"
    60 
    61 | Basic:   "\<parallel>- {s. f s \<in>q} (Basic f) q"
    62 
    63 | Seq:    "\<lbrakk> \<parallel>- p c1 r; \<parallel>- r c2 q \<rbrakk> \<Longrightarrow> \<parallel>- p (Seq c1 c2) q "
    64 
    65 | Cond:   "\<lbrakk> \<parallel>- (p \<inter> b) c1 q; \<parallel>- (p \<inter> -b) c2 q \<rbrakk> \<Longrightarrow> \<parallel>- p (Cond b c1 c2) q"
    66 
    67 | While:  "\<lbrakk> \<parallel>- (p \<inter> b) c p \<rbrakk> \<Longrightarrow> \<parallel>- p (While b i c) (p \<inter> -b)"
    68 
    69 | Conseq: "\<lbrakk> p' \<subseteq> p; \<parallel>- p c q ; q \<subseteq> q' \<rbrakk> \<Longrightarrow> \<parallel>- p' c q'"
    70 
    71 section \<open>Soundness\<close>
    72 (* In the version Isabelle-10-Sep-1999: HOL: The THEN and ELSE
    73 parts of conditional expressions (if P then x else y) are no longer
    74 simplified.  (This allows the simplifier to unfold recursive
    75 functional programs.)  To restore the old behaviour, we declare
    76 @{text "lemmas [cong del] = if_weak_cong"}. *)
    77 
    78 lemmas [cong del] = if_weak_cong
    79 
    80 lemmas ann_hoare_induct = oghoare_ann_hoare.induct [THEN conjunct2]
    81 lemmas oghoare_induct = oghoare_ann_hoare.induct [THEN conjunct1]
    82 
    83 lemmas AnnBasic = oghoare_ann_hoare.AnnBasic
    84 lemmas AnnSeq = oghoare_ann_hoare.AnnSeq
    85 lemmas AnnCond1 = oghoare_ann_hoare.AnnCond1
    86 lemmas AnnCond2 = oghoare_ann_hoare.AnnCond2
    87 lemmas AnnWhile = oghoare_ann_hoare.AnnWhile
    88 lemmas AnnAwait = oghoare_ann_hoare.AnnAwait
    89 lemmas AnnConseq = oghoare_ann_hoare.AnnConseq
    90 
    91 lemmas Parallel = oghoare_ann_hoare.Parallel
    92 lemmas Basic = oghoare_ann_hoare.Basic
    93 lemmas Seq = oghoare_ann_hoare.Seq
    94 lemmas Cond = oghoare_ann_hoare.Cond
    95 lemmas While = oghoare_ann_hoare.While
    96 lemmas Conseq = oghoare_ann_hoare.Conseq
    97 
    98 subsection \<open>Soundness of the System for Atomic Programs\<close>
    99 
   100 lemma Basic_ntran [rule_format]:
   101  "(Basic f, s) -Pn\<rightarrow> (Parallel Ts, t) \<longrightarrow> All_None Ts \<longrightarrow> t = f s"
   102 apply(induct "n")
   103  apply(simp (no_asm))
   104 apply(fast dest: relpow_Suc_D2 Parallel_empty_lemma elim: transition_cases)
   105 done
   106 
   107 lemma SEM_fwhile: "SEM S (p \<inter> b) \<subseteq> p \<Longrightarrow> SEM (fwhile b S k) p \<subseteq> (p \<inter> -b)"
   108 apply (induct "k")
   109  apply(simp (no_asm) add: L3_5v_lemma3)
   110 apply(simp (no_asm) add: L3_5iv L3_5ii Parallel_empty)
   111 apply(rule conjI)
   112  apply (blast dest: L3_5i)
   113 apply(simp add: SEM_def sem_def id_def)
   114 apply (auto dest: Basic_ntran rtrancl_imp_UN_relpow)
   115 apply blast
   116 done
   117 
   118 lemma atom_hoare_sound [rule_format]:
   119  " \<parallel>- p c q \<longrightarrow> atom_com(c) \<longrightarrow> \<parallel>= p c q"
   120 apply (unfold com_validity_def)
   121 apply(rule oghoare_induct)
   122 apply simp_all
   123 \<comment>\<open>Basic\<close>
   124     apply(simp add: SEM_def sem_def)
   125     apply(fast dest: rtrancl_imp_UN_relpow Basic_ntran)
   126 \<comment>\<open>Seq\<close>
   127    apply(rule impI)
   128    apply(rule subset_trans)
   129     prefer 2 apply simp
   130    apply(simp add: L3_5ii L3_5i)
   131 \<comment>\<open>Cond\<close>
   132   apply(simp add: L3_5iv)
   133 \<comment>\<open>While\<close>
   134  apply (force simp add: L3_5v dest: SEM_fwhile)
   135 \<comment>\<open>Conseq\<close>
   136 apply(force simp add: SEM_def sem_def)
   137 done
   138 
   139 subsection \<open>Soundness of the System for Component Programs\<close>
   140 
   141 inductive_cases ann_transition_cases:
   142     "(None,s) -1\<rightarrow> (c', s')"
   143     "(Some (AnnBasic r f),s) -1\<rightarrow> (c', s')"
   144     "(Some (AnnSeq c1 c2), s) -1\<rightarrow> (c', s')"
   145     "(Some (AnnCond1 r b c1 c2), s) -1\<rightarrow> (c', s')"
   146     "(Some (AnnCond2 r b c), s) -1\<rightarrow> (c', s')"
   147     "(Some (AnnWhile r b I c), s) -1\<rightarrow> (c', s')"
   148     "(Some (AnnAwait r b c),s) -1\<rightarrow> (c', s')"
   149 
   150 text \<open>Strong Soundness for Component Programs:\<close>
   151 
   152 lemma ann_hoare_case_analysis [rule_format]: "\<turnstile> C q' \<longrightarrow>
   153   ((\<forall>r f. C = AnnBasic r f \<longrightarrow> (\<exists>q. r \<subseteq> {s. f s \<in> q} \<and> q \<subseteq> q')) \<and>
   154   (\<forall>c0 c1. C = AnnSeq c0 c1 \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and> \<turnstile> c0 pre c1 \<and> \<turnstile> c1 q)) \<and>
   155   (\<forall>r b c1 c2. C = AnnCond1 r b c1 c2 \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and>
   156   r \<inter> b \<subseteq> pre c1 \<and> \<turnstile> c1 q \<and> r \<inter> -b \<subseteq> pre c2 \<and> \<turnstile> c2 q)) \<and>
   157   (\<forall>r b c. C = AnnCond2 r b c \<longrightarrow>
   158   (\<exists>q. q \<subseteq> q' \<and> r \<inter> b \<subseteq> pre c  \<and> \<turnstile> c q \<and> r \<inter> -b \<subseteq> q)) \<and>
   159   (\<forall>r i b c. C = AnnWhile r b i c \<longrightarrow>
   160   (\<exists>q. q \<subseteq> q' \<and> r \<subseteq> i \<and> i \<inter> b \<subseteq> pre c \<and> \<turnstile> c i \<and> i \<inter> -b \<subseteq> q)) \<and>
   161   (\<forall>r b c. C = AnnAwait r b c \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and> \<parallel>- (r \<inter> b) c q)))"
   162 apply(rule ann_hoare_induct)
   163 apply simp_all
   164  apply(rule_tac x=q in exI,simp)+
   165 apply(rule conjI,clarify,simp,clarify,rule_tac x=qa in exI,fast)+
   166 apply(clarify,simp,clarify,rule_tac x=qa in exI,fast)
   167 done
   168 
   169 lemma Help: "(transition \<inter> {(x,y). True}) = (transition)"
   170 apply force
   171 done
   172 
   173 lemma Strong_Soundness_aux_aux [rule_format]:
   174  "(co, s) -1\<rightarrow> (co', t) \<longrightarrow> (\<forall>c. co = Some c \<longrightarrow> s\<in> pre c \<longrightarrow>
   175  (\<forall>q. \<turnstile> c q \<longrightarrow> (if co' = None then t\<in>q else t \<in> pre(the co') \<and> \<turnstile> (the co') q )))"
   176 apply(rule ann_transition_transition.induct [THEN conjunct1])
   177 apply simp_all
   178 \<comment>\<open>Basic\<close>
   179          apply clarify
   180          apply(frule ann_hoare_case_analysis)
   181          apply force
   182 \<comment>\<open>Seq\<close>
   183         apply clarify
   184         apply(frule ann_hoare_case_analysis,simp)
   185         apply(fast intro: AnnConseq)
   186        apply clarify
   187        apply(frule ann_hoare_case_analysis,simp)
   188        apply clarify
   189        apply(rule conjI)
   190         apply force
   191        apply(rule AnnSeq,simp)
   192        apply(fast intro: AnnConseq)
   193 \<comment>\<open>Cond1\<close>
   194       apply clarify
   195       apply(frule ann_hoare_case_analysis,simp)
   196       apply(fast intro: AnnConseq)
   197      apply clarify
   198      apply(frule ann_hoare_case_analysis,simp)
   199      apply(fast intro: AnnConseq)
   200 \<comment>\<open>Cond2\<close>
   201     apply clarify
   202     apply(frule ann_hoare_case_analysis,simp)
   203     apply(fast intro: AnnConseq)
   204    apply clarify
   205    apply(frule ann_hoare_case_analysis,simp)
   206    apply(fast intro: AnnConseq)
   207 \<comment>\<open>While\<close>
   208   apply clarify
   209   apply(frule ann_hoare_case_analysis,simp)
   210   apply force
   211  apply clarify
   212  apply(frule ann_hoare_case_analysis,simp)
   213  apply auto
   214  apply(rule AnnSeq)
   215   apply simp
   216  apply(rule AnnWhile)
   217   apply simp_all
   218 \<comment>\<open>Await\<close>
   219 apply(frule ann_hoare_case_analysis,simp)
   220 apply clarify
   221 apply(drule atom_hoare_sound)
   222  apply simp
   223 apply(simp add: com_validity_def SEM_def sem_def)
   224 apply(simp add: Help All_None_def)
   225 apply force
   226 done
   227 
   228 lemma Strong_Soundness_aux: "\<lbrakk> (Some c, s) -*\<rightarrow> (co, t); s \<in> pre c; \<turnstile> c q \<rbrakk>
   229   \<Longrightarrow> if co = None then t \<in> q else t \<in> pre (the co) \<and> \<turnstile> (the co) q"
   230 apply(erule rtrancl_induct2)
   231  apply simp
   232 apply(case_tac "a")
   233  apply(fast elim: ann_transition_cases)
   234 apply(erule Strong_Soundness_aux_aux)
   235  apply simp
   236 apply simp_all
   237 done
   238 
   239 lemma Strong_Soundness: "\<lbrakk> (Some c, s)-*\<rightarrow>(co, t); s \<in> pre c; \<turnstile> c q \<rbrakk>
   240   \<Longrightarrow> if co = None then t\<in>q else t \<in> pre (the co)"
   241 apply(force dest:Strong_Soundness_aux)
   242 done
   243 
   244 lemma ann_hoare_sound: "\<turnstile> c q  \<Longrightarrow> \<Turnstile> c q"
   245 apply (unfold ann_com_validity_def ann_SEM_def ann_sem_def)
   246 apply clarify
   247 apply(drule Strong_Soundness)
   248 apply simp_all
   249 done
   250 
   251 subsection \<open>Soundness of the System for Parallel Programs\<close>
   252 
   253 lemma Parallel_length_post_P1: "(Parallel Ts,s) -P1\<rightarrow> (R', t) \<Longrightarrow>
   254   (\<exists>Rs. R' = (Parallel Rs) \<and> (length Rs) = (length Ts) \<and>
   255   (\<forall>i. i<length Ts \<longrightarrow> post(Rs ! i) = post(Ts ! i)))"
   256 apply(erule transition_cases)
   257 apply simp
   258 apply clarify
   259 apply(case_tac "i=ia")
   260 apply simp+
   261 done
   262 
   263 lemma Parallel_length_post_PStar: "(Parallel Ts,s) -P*\<rightarrow> (R',t) \<Longrightarrow>
   264   (\<exists>Rs. R' = (Parallel Rs) \<and> (length Rs) = (length Ts) \<and>
   265   (\<forall>i. i<length Ts \<longrightarrow> post(Ts ! i) = post(Rs ! i)))"
   266 apply(erule rtrancl_induct2)
   267  apply(simp_all)
   268 apply clarify
   269 apply simp
   270 apply(drule Parallel_length_post_P1)
   271 apply auto
   272 done
   273 
   274 lemma assertions_lemma: "pre c \<in> assertions c"
   275 apply(rule ann_com_com.induct [THEN conjunct1])
   276 apply auto
   277 done
   278 
   279 lemma interfree_aux1 [rule_format]:
   280   "(c,s) -1\<rightarrow> (r,t)  \<longrightarrow> (interfree_aux(c1, q1, c) \<longrightarrow> interfree_aux(c1, q1, r))"
   281 apply (rule ann_transition_transition.induct [THEN conjunct1])
   282 apply(safe)
   283 prefer 13
   284 apply (rule TrueI)
   285 apply (simp_all add:interfree_aux_def)
   286 apply force+
   287 done
   288 
   289 lemma interfree_aux2 [rule_format]:
   290   "(c,s) -1\<rightarrow> (r,t) \<longrightarrow> (interfree_aux(c, q, a)  \<longrightarrow> interfree_aux(r, q, a) )"
   291 apply (rule ann_transition_transition.induct [THEN conjunct1])
   292 apply(force simp add:interfree_aux_def)+
   293 done
   294 
   295 lemma interfree_lemma: "\<lbrakk> (Some c, s) -1\<rightarrow> (r, t);interfree Ts ; i<length Ts;
   296            Ts!i = (Some c, q) \<rbrakk> \<Longrightarrow> interfree (Ts[i:= (r, q)])"
   297 apply(simp add: interfree_def)
   298 apply clarify
   299 apply(case_tac "i=j")
   300  apply(drule_tac t = "ia" in not_sym)
   301  apply simp_all
   302 apply(force elim: interfree_aux1)
   303 apply(force elim: interfree_aux2 simp add:nth_list_update)
   304 done
   305 
   306 text \<open>Strong Soundness Theorem for Parallel Programs:\<close>
   307 
   308 lemma Parallel_Strong_Soundness_Seq_aux:
   309   "\<lbrakk>interfree Ts; i<length Ts; com(Ts ! i) = Some(AnnSeq c0 c1) \<rbrakk>
   310   \<Longrightarrow>  interfree (Ts[i:=(Some c0, pre c1)])"
   311 apply(simp add: interfree_def)
   312 apply clarify
   313 apply(case_tac "i=j")
   314  apply(force simp add: nth_list_update interfree_aux_def)
   315 apply(case_tac "i=ia")
   316  apply(erule_tac x=ia in allE)
   317  apply(force simp add:interfree_aux_def assertions_lemma)
   318 apply simp
   319 done
   320 
   321 lemma Parallel_Strong_Soundness_Seq [rule_format (no_asm)]:
   322  "\<lbrakk> \<forall>i<length Ts. (if com(Ts!i) = None then b \<in> post(Ts!i)
   323   else b \<in> pre(the(com(Ts!i))) \<and> \<turnstile> the(com(Ts!i)) post(Ts!i));
   324   com(Ts ! i) = Some(AnnSeq c0 c1); i<length Ts; interfree Ts \<rbrakk> \<Longrightarrow>
   325  (\<forall>ia<length Ts. (if com(Ts[i:=(Some c0, pre c1)]! ia) = None
   326   then b \<in> post(Ts[i:=(Some c0, pre c1)]! ia)
   327  else b \<in> pre(the(com(Ts[i:=(Some c0, pre c1)]! ia))) \<and>
   328  \<turnstile> the(com(Ts[i:=(Some c0, pre c1)]! ia)) post(Ts[i:=(Some c0, pre c1)]! ia)))
   329   \<and> interfree (Ts[i:= (Some c0, pre c1)])"
   330 apply(rule conjI)
   331  apply safe
   332  apply(case_tac "i=ia")
   333   apply simp
   334   apply(force dest: ann_hoare_case_analysis)
   335  apply simp
   336 apply(fast elim: Parallel_Strong_Soundness_Seq_aux)
   337 done
   338 
   339 lemma Parallel_Strong_Soundness_aux_aux [rule_format]:
   340  "(Some c, b) -1\<rightarrow> (co, t) \<longrightarrow>
   341   (\<forall>Ts. i<length Ts \<longrightarrow> com(Ts ! i) = Some c \<longrightarrow>
   342   (\<forall>i<length Ts. (if com(Ts ! i) = None then b\<in>post(Ts!i)
   343   else b\<in>pre(the(com(Ts!i))) \<and> \<turnstile> the(com(Ts!i)) post(Ts!i))) \<longrightarrow>
   344  interfree Ts \<longrightarrow>
   345   (\<forall>j. j<length Ts \<and> i\<noteq>j \<longrightarrow> (if com(Ts!j) = None then t\<in>post(Ts!j)
   346   else t\<in>pre(the(com(Ts!j))) \<and> \<turnstile> the(com(Ts!j)) post(Ts!j))) )"
   347 apply(rule ann_transition_transition.induct [THEN conjunct1])
   348 apply safe
   349 prefer 11
   350 apply(rule TrueI)
   351 apply simp_all
   352 \<comment>\<open>Basic\<close>
   353    apply(erule_tac x = "i" in all_dupE, erule (1) notE impE)
   354    apply(erule_tac x = "j" in allE , erule (1) notE impE)
   355    apply(simp add: interfree_def)
   356    apply(erule_tac x = "j" in allE,simp)
   357    apply(erule_tac x = "i" in allE,simp)
   358    apply(drule_tac t = "i" in not_sym)
   359    apply(case_tac "com(Ts ! j)=None")
   360     apply(force intro: converse_rtrancl_into_rtrancl
   361           simp add: interfree_aux_def com_validity_def SEM_def sem_def All_None_def)
   362    apply(simp add:interfree_aux_def)
   363    apply clarify
   364    apply simp
   365    apply(erule_tac x="pre y" in ballE)
   366     apply(force intro: converse_rtrancl_into_rtrancl
   367           simp add: com_validity_def SEM_def sem_def All_None_def)
   368    apply(simp add:assertions_lemma)
   369 \<comment>\<open>Seqs\<close>
   370   apply(erule_tac x = "Ts[i:=(Some c0, pre c1)]" in allE)
   371   apply(drule  Parallel_Strong_Soundness_Seq,simp+)
   372  apply(erule_tac x = "Ts[i:=(Some c0, pre c1)]" in allE)
   373  apply(drule  Parallel_Strong_Soundness_Seq,simp+)
   374 \<comment>\<open>Await\<close>
   375 apply(rule_tac x = "i" in allE , assumption , erule (1) notE impE)
   376 apply(erule_tac x = "j" in allE , erule (1) notE impE)
   377 apply(simp add: interfree_def)
   378 apply(erule_tac x = "j" in allE,simp)
   379 apply(erule_tac x = "i" in allE,simp)
   380 apply(drule_tac t = "i" in not_sym)
   381 apply(case_tac "com(Ts ! j)=None")
   382  apply(force intro: converse_rtrancl_into_rtrancl simp add: interfree_aux_def
   383         com_validity_def SEM_def sem_def All_None_def Help)
   384 apply(simp add:interfree_aux_def)
   385 apply clarify
   386 apply simp
   387 apply(erule_tac x="pre y" in ballE)
   388  apply(force intro: converse_rtrancl_into_rtrancl
   389        simp add: com_validity_def SEM_def sem_def All_None_def Help)
   390 apply(simp add:assertions_lemma)
   391 done
   392 
   393 lemma Parallel_Strong_Soundness_aux [rule_format]:
   394  "\<lbrakk>(Ts',s) -P*\<rightarrow> (Rs',t);  Ts' = (Parallel Ts); interfree Ts;
   395  \<forall>i. i<length Ts \<longrightarrow> (\<exists>c q. (Ts ! i) = (Some c, q) \<and> s\<in>(pre c) \<and> \<turnstile> c q ) \<rbrakk> \<Longrightarrow>
   396   \<forall>Rs. Rs' = (Parallel Rs) \<longrightarrow> (\<forall>j. j<length Rs \<longrightarrow>
   397   (if com(Rs ! j) = None then t\<in>post(Ts ! j)
   398   else t\<in>pre(the(com(Rs ! j))) \<and> \<turnstile> the(com(Rs ! j)) post(Ts ! j))) \<and> interfree Rs"
   399 apply(erule rtrancl_induct2)
   400  apply clarify
   401 \<comment>\<open>Base\<close>
   402  apply force
   403 \<comment>\<open>Induction step\<close>
   404 apply clarify
   405 apply(drule Parallel_length_post_PStar)
   406 apply clarify
   407 apply (ind_cases "(Parallel Ts, s) -P1\<rightarrow> (Parallel Rs, t)" for Ts s Rs t)
   408 apply(rule conjI)
   409  apply clarify
   410  apply(case_tac "i=j")
   411   apply(simp split del:if_split)
   412   apply(erule Strong_Soundness_aux_aux,simp+)
   413    apply force
   414   apply force
   415  apply(simp split del: if_split)
   416  apply(erule Parallel_Strong_Soundness_aux_aux)
   417  apply(simp_all add: split del:if_split)
   418  apply force
   419 apply(rule interfree_lemma)
   420 apply simp_all
   421 done
   422 
   423 lemma Parallel_Strong_Soundness:
   424  "\<lbrakk>(Parallel Ts, s) -P*\<rightarrow> (Parallel Rs, t); interfree Ts; j<length Rs;
   425   \<forall>i. i<length Ts \<longrightarrow> (\<exists>c q. Ts ! i = (Some c, q) \<and> s\<in>pre c \<and> \<turnstile> c q) \<rbrakk> \<Longrightarrow>
   426   if com(Rs ! j) = None then t\<in>post(Ts ! j) else t\<in>pre (the(com(Rs ! j)))"
   427 apply(drule  Parallel_Strong_Soundness_aux)
   428 apply simp+
   429 done
   430 
   431 lemma oghoare_sound [rule_format]: "\<parallel>- p c q \<longrightarrow> \<parallel>= p c q"
   432 apply (unfold com_validity_def)
   433 apply(rule oghoare_induct)
   434 apply(rule TrueI)+
   435 \<comment>\<open>Parallel\<close>
   436       apply(simp add: SEM_def sem_def)
   437       apply(clarify, rename_tac x y i Ts')
   438       apply(frule Parallel_length_post_PStar)
   439       apply clarify
   440       apply(drule_tac j=i in Parallel_Strong_Soundness)
   441          apply clarify
   442         apply simp
   443        apply force
   444       apply simp
   445       apply(erule_tac V = "\<forall>i. P i" for P in thin_rl)
   446       apply(drule_tac s = "length Rs" in sym)
   447       apply(erule allE, erule impE, assumption)
   448       apply(force dest: nth_mem simp add: All_None_def)
   449 \<comment>\<open>Basic\<close>
   450     apply(simp add: SEM_def sem_def)
   451     apply(force dest: rtrancl_imp_UN_relpow Basic_ntran)
   452 \<comment>\<open>Seq\<close>
   453    apply(rule subset_trans)
   454     prefer 2 apply assumption
   455    apply(simp add: L3_5ii L3_5i)
   456 \<comment>\<open>Cond\<close>
   457   apply(simp add: L3_5iv)
   458 \<comment>\<open>While\<close>
   459  apply(simp add: L3_5v)
   460  apply (blast dest: SEM_fwhile)
   461 \<comment>\<open>Conseq\<close>
   462 apply(auto simp add: SEM_def sem_def)
   463 done
   464 
   465 end