Theory OG_Soundness

(*
 * Copyright 2016, Data61, CSIRO
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(DATA61_BSD)
 *)
section ‹Soundness proof of Owicki-Gries w.r.t.
           COMPLX small-step semantics›

theory OG_Soundness
imports
  OG_Hoare
  SeqCatch_decomp  
begin

lemma pre_weaken_pre:
 " x  pre P   x  pre (weaken_pre P P')"
 by (induct P, clarsimp+)

lemma oghoare_Skip[rule_format, OF _ refl]: 
"Γ, Θ ⊢⇘/FP c Q,A  c = Skip  
 (P'. P = AnnExpr P'  P'  Q)"
  apply (induct rule: oghoare_induct, simp_all)
  apply clarsimp
  apply (rename_tac Γ Θ F P Q A P' Q' A' P'')
  apply(case_tac P, simp_all)
  by force

lemma oghoare_Throw[rule_format, OF _ refl]: 
"Γ, Θ ⊢⇘/FP c Q,A  c = Throw  
 (P'. P = AnnExpr P'  P'  A)"
  apply (induct rule: oghoare_induct, simp_all)
  apply clarsimp
  apply (rename_tac Γ Θ F P Q A P' Q' A' P'')
  apply(case_tac P, simp_all)
  by force

lemma oghoare_Basic[rule_format, OF _ refl]: 
"Γ, Θ ⊢⇘/FP c Q,A  c = Basic f  
 (P'. P = AnnExpr P'  P'  {x. f x  Q})"
  apply (induct rule: oghoare_induct, simp_all)
   apply clarsimp
  apply (rename_tac Γ Θ F P Q A P' Q' A' P'')
  apply(case_tac P, simp_all)
  by force

lemma oghoare_Spec[rule_format, OF _ refl]: 
"Γ, Θ ⊢⇘/FP c Q,A  c = Spec r  
 (P'. P = AnnExpr P'  P'  {s. (t. (s, t)  r  t  Q)  (t. (s, t)  r)})"
  apply (induct rule: oghoare_induct, simp_all)
  apply clarsimp
  apply (rename_tac Γ Θ F P Q A P' Q' A' P'')
  apply(case_tac P, simp_all)
  by force

lemma oghoare_DynCom[rule_format, OF _ refl]: 
"Γ, Θ ⊢⇘/FP c Q,A  c = (DynCom c')  
 (r ad. P = (AnnRec r ad)  r  pre ad  (sr. Γ, Θ ⊢⇘/Fad (c' s) Q,A))"
  apply (induct rule: oghoare_induct, simp_all)
   apply clarsimp
  apply clarsimp
  apply (rename_tac Γ Θ F P Q A P' Q' A' P'' x)
  apply(case_tac P, simp_all)
  apply clarsimp
  apply (rename_tac P s)
  apply (drule_tac x=s in bspec, simp)
  apply (rule Conseq)
  apply (rule_tac x="{}" in exI)
  apply (fastforce)
 done

lemma oghoare_Guard[rule_format, OF _ refl]: 
"Γ,Θ⊢⇘/FP c Q,A  c = Guard f g d  
 (P' r . P = AnnRec r P'  
   Γ,Θ⊢⇘/FP' d Q,A 
   r  g  pre P' 
   (r  -g  {}  f  F))"
  apply (induct rule: oghoare_induct, simp_all)
   apply force
  apply clarsimp
  apply (rename_tac Γ Θ F P Q A P' Q' A' P'' r)
  apply (case_tac P, simp_all)
  apply clarsimp
  apply (rename_tac r)
  apply(rule conjI)
   apply (rule Conseq)
   apply (rule_tac x="{}" in exI)
   apply (rule_tac x="Q'" in exI)
   apply (rule_tac x="A'" in exI)
   apply (clarsimp)
  apply (case_tac "(r  P')  g  {}")
   apply fast
  apply clarsimp
  apply(drule equalityD1, force)
 done

lemma oghoare_Await[rule_format, OF _ refl]: 
"Γ, Θ⊢⇘/FP x Q,A  b c. x = Await b c 
 (r P' Q' A'. P = AnnRec r P'  Γ, Θ⊩⇘/F(r  b) P' c Q',A'  atom_com c 
                  Q'  Q  A'  A)"
  supply [[simproc del: defined_all]]
  apply (induct rule: oghoare_induct, simp_all)
    apply (rename_tac Γ Θ F r P Q A)
   apply (rule_tac x=Q in exI)
   apply (rule_tac x=A in exI)
   apply clarsimp
  apply (rename_tac Γ Θ F P c Q A)
  apply clarsimp

  apply(case_tac P, simp_all)
  apply (rename_tac P'' Q'' A'' x y)
  apply (rule_tac x=Q'' in exI)
  apply (rule_tac x=A'' in exI)
  apply clarsimp
  apply (rule conjI[rotated])
   apply blast
  apply (erule SeqConseq[rotated])
    apply simp
   apply simp
  apply blast
 done

lemma oghoare_Seq[rule_format, OF _ refl]: 
"Γ, Θ ⊢⇘/FP x Q,A  p1 p2. x = Seq p1 p2 
 ( P1 P2 P' Q' A'. P = AnnComp P1 P2  Γ, Θ ⊢⇘/FP1 p1 P', A'  P'  pre P2 
         Γ, Θ ⊢⇘/FP2 p2 Q',A' 
          Q'  Q  A'  A)"
  apply (induct rule: oghoare_induct, simp_all)
   apply blast
  apply (rename_tac Γ Θ F P c Q A)
  apply clarsimp
  apply (rename_tac P'' Q'' A'')
  apply(case_tac P, simp_all)
  apply clarsimp
  apply (rule_tac x="P''" in exI)
  apply (rule_tac x="Q''" in exI)
  apply (rule_tac x="A''" in exI)
  apply clarsimp
  apply (rule conjI)
   apply (rule Conseq)
   apply (rule_tac x="P'" in exI)
   apply (rule_tac x="P''" in exI)
   apply (rule_tac x="A''" in exI)
   apply simp
  apply fastforce
 done

lemma oghoare_Catch[rule_format, OF _ refl]: 
"Γ, Θ ⊢⇘/FP x Q,A  p1 p2. x = Catch p1 p2 
 ( P1 P2 P' Q' A'. P = AnnComp P1 P2  Γ, Θ ⊢⇘/FP1 p1 Q', P'  P'  pre P2 
         Γ, Θ ⊢⇘/FP2 p2 Q',A' 
          Q'  Q  A'  A)"
  apply (induct rule: oghoare_induct, simp_all)
   apply blast
  apply (rename_tac Γ Θ F P c Q A)
  apply clarsimp
  apply(case_tac P, simp_all)
  apply clarsimp
  apply (rename_tac P'' Q'' A'' x)
  apply (rule_tac x="P''" in exI)
  apply (rule_tac x="Q''" in exI)
  apply clarsimp
   apply (rule conjI)
   apply (rule Conseq)
   apply (rule_tac x=P' in exI)
   apply fastforce
  apply (rule_tac x="A''" in exI)
  apply clarsimp
  apply fastforce
 done

lemma oghoare_Cond[rule_format, OF _ refl]: 
 "Γ, Θ ⊢⇘/FP x Q,A 
c1 c2 b. x = (Cond b c1 c2) 
(P' P1 P2 Q' A'. P = (AnnBin P' P1 P2) 
  P'  {s. (sb  spre P1)  (sb  spre P2)} 
    Γ, Θ ⊢⇘/FP1 c1 Q',A' 
    Γ, Θ ⊢⇘/FP2 c2 Q',A'  Q'  Q  A'  A)"
  apply (induct rule: oghoare_induct, simp_all)
   apply (rule conjI)
    apply fastforce
   apply (rename_tac  Q A P2 c2 r b)
   apply (rule_tac x=Q in exI)
   apply (rule_tac x=A in exI)
   apply fastforce
  apply (rename_tac Γ Θ F P c Q A)
  apply clarsimp
  apply (case_tac P, simp_all)
  apply fastforce
done

lemma oghoare_While[rule_format, OF _ refl]:
  "Γ, Θ ⊢⇘/FP x Q,A 
     b c. x = While b c 
    ( r i P' A' Q'. P = AnnWhile r i P' 
     Γ, Θ⊢⇘/FP' c i,A' 
     r  i 
     i  b  pre P' 
     i  -b  Q' 
      Q'  Q  A'  A)"
  apply (induct rule: oghoare_induct, simp_all)
   apply blast
  apply (rename_tac Γ Θ F P c Q A)
  apply clarsimp
  apply (rename_tac P' Q' A' b ca r i P'' A'' Q'')
  apply (case_tac P; simp)
  apply (rule_tac x= A'' in exI)
  apply (rule conjI)
   apply blast
  apply clarsimp
  apply (rule_tac x= "Q'" in exI)
  by fast


lemma oghoare_Call:
 "Γ,Θ⊢⇘/FP x Q,A 
  p. x = Call p 
 (r n.
 P = (AnnCall r n) 
 (as P' f b.
 Θ p = Some as 
 (as ! n) = P' 
 r  pre P' 
 Γ p = Some b 
 n < length as 
 Γ,Θ ⊢⇘/FP' b Q,A))"
  apply (induct rule: oghoare_induct, simp_all)
  apply (rename_tac Γ Θ F P c Q A)
  apply clarsimp
  apply (case_tac P, simp_all)
  apply clarsimp
  apply (rule Conseq)
  apply (rule_tac x="{}" in exI)
  apply force
 done

lemma oghoare_Parallel[rule_format, OF _ refl]: 
"Γ, Θ⊢⇘/FP x Q,A  cs. x = Parallel cs 
 (as. P = AnnPar as  
   length as = length cs 
   (set (map postcond as))  Q 
   (set (map abrcond as))  A 
   (i<length cs. Q' A'. Γ,Θ⊢⇘/F(pres (as!i)) (cs!i) Q', A' 
            Q'  postcond (as!i)  A'  abrcond (as!i)) 
  interfree Γ Θ F as cs)"
  apply (induct rule: oghoare_induct, simp_all)
   apply clarsimp
   apply (drule_tac x=i in spec)
   apply fastforce
  apply clarsimp
  apply (case_tac P, simp_all)
  apply blast
 done

lemma  ann_matches_weaken[OF _ refl]:
" ann_matches Γ Θ X c  X = (weaken_pre P P')  ann_matches Γ Θ P c"
  apply (induct arbitrary: P P' rule: ann_matches.induct)
   apply (case_tac P, simp_all, fastforce simp add: ann_matches.intros)+
done


lemma oghoare_seq_imp_ann_matches:
 " Γ,Θ⊩⇘/FP a c Q,A  ann_matches Γ Θ a c"
  apply (induct rule: oghoare_seq_induct, simp_all add: ann_matches.intros)
  apply (clarsimp, erule ann_matches_weaken)+
 done

lemma oghoare_imp_ann_matches:
 " Γ,Θ⊢⇘/Fa c Q,A  ann_matches Γ Θ a c"
  apply (induct rule: oghoare_induct, simp_all add: ann_matches.intros oghoare_seq_imp_ann_matches)
  apply (clarsimp, erule ann_matches_weaken)+
 done

(* intros *)

lemma SkipRule: "P  Q  Γ, Θ ⊢⇘/F(AnnExpr P) Skip Q, A"
  apply (rule Conseq, simp)
  apply (rule exI, rule exI, rule exI)
  apply (rule conjI, rule Skip, auto)
done

lemma ThrowRule: "P  A  Γ, Θ ⊢⇘/F(AnnExpr P) Throw Q, A"
  apply (rule Conseq, simp)
  apply (rule exI, rule exI, rule exI)
  apply (rule conjI, rule Throw, auto)
done

lemma BasicRule: "P  {s. (f s)  Q}  Γ, Θ ⊢⇘/F(AnnExpr P) (Basic f) Q, A"
  apply (rule Conseq, simp, rule exI[where x="{s. (f s)  Q}"])
  apply (rule exI[where x=Q], rule exI[where x=A])
  apply simp
  apply (subgoal_tac "(P  {s. f s  Q}) = {s. f s  Q}")
  apply (auto intro: Basic)
done

lemma SpecRule:
  "P  {s. (t. (s, t)  r  t  Q)  (t. (s, t)  r)}
     Γ, Θ ⊢⇘/F(AnnExpr P) (Spec r) Q, A"
  apply (rule Conseq, simp, rule exI[where x="{s. (t. (s, t)  r  t  Q)  (t. (s, t)  r) }"])
  apply (rule exI[where x=Q], rule exI[where x=A])
  apply simp
  apply (subgoal_tac "(P  {s. (t. (s, t)  r  t  Q)  (t. (s, t)  r)}) = {s. (t. (s, t)  r  t  Q)  (t. (s, t)  r)}")
   apply (auto intro: Spec)
done

lemma CondRule: 
 " P  {s. (sb  spre P1)  (sb  spre P2)};
    Γ, Θ ⊢⇘/FP1 c1 Q,A; 
    Γ, Θ ⊢⇘/FP2 c2 Q,A   
   Γ, Θ ⊢⇘/F(AnnBin P P1 P2) (Cond b c1 c2) Q,A"
  by (auto intro: Cond)

lemma WhileRule: " r  I; I  b  pre P; (I  -b)  Q;
                    Γ, Θ ⊢⇘/FP c I,A   
         Γ, Θ ⊢⇘/F(AnnWhile r I P) (While b c) Q,A"
  by (simp add: While)

lemma AwaitRule:
 "atom_com c ; Γ, Θ ⊩⇘/FP a c Q,A ; (r  b)  P 
  Γ, Θ ⊢⇘/F(AnnRec r a) (Await b c) Q,A"
  apply (erule Await[rotated])
  apply (erule (1) SeqConseq, simp+)
 done

lemma rtranclp_1n_induct [consumes 1, case_names base step]:
  "r** a b; P a; y z. r y z; r** z b; P y  P z  P b" 
 by (induct rule: rtranclp.induct) 
    (simp add: rtranclp.rtrancl_into_rtrancl)+

lemmas rtranclp_1n_induct2[consumes 1, case_names base step] = 
  rtranclp_1n_induct[of _ "(ax,ay)" "(bx,by)", split_rule]

lemma oghoare_seq_valid:
 " Γ⊨⇘/FP c1 R,A 
   Γ⊨⇘/FR c2 Q,A 
   Γ⊨⇘/FP Seq c1 c2 Q,A"
  apply (clarsimp simp add: valid_def)
  apply (rename_tac t c' s)
  apply (case_tac t)
    apply simp
    apply (drule (1) Seq_decomp_star)
    apply (erule disjE)
     apply fastforce
    apply clarsimp
    apply (rename_tac s1 t')
    apply (drule_tac x="Normal s" and y="Normal t'" in spec2)
    apply (erule_tac x="Skip" in allE)
    apply (fastforce simp: final_def)
   apply (clarsimp simp add: final_def)
   apply (drule Seq_decomp_star_Fault)
   apply (erule disjE)
    apply (rename_tac s2)
    apply (drule_tac x="Normal s" and y="Fault s2" in spec2)
    apply (erule_tac x="Skip" in allE)
    apply fastforce
   apply clarsimp
   apply (rename_tac s s2 s')
   apply (drule_tac x="Normal s" and y="Normal s'" in spec2)
   apply (erule_tac x="Skip" in allE)
   apply clarsimp
   apply (drule_tac x="Normal s'" and y="Fault s2" in spec2)
   apply (erule_tac x="Skip" in allE)
   apply clarsimp
  apply clarsimp
  apply (simp add: final_def)
  apply (drule Seq_decomp_star_Stuck)
  apply (erule disjE)
   apply fastforce
  apply clarsimp
  apply fastforce
 done

lemma oghoare_if_valid:
 "Γ⊨⇘/FP1 c1 Q,A 
  Γ⊨⇘/FP2 c2 Q,A 
  r  b  P1  r  - b  P2 
  Γ⊨⇘/Fr Cond b c1 c2 Q,A"
  apply (simp (no_asm) add: valid_def)
  apply (clarsimp)
  apply (erule converse_rtranclpE) 
   apply (clarsimp simp: final_def)
  apply (erule step_Normal_elim_cases)
   apply (fastforce simp: valid_def[where c=c1])
  apply (fastforce simp: valid_def[where c=c2])
 done

lemma Skip_normal_steps_end:
"Γ  (Skip, Normal s) * (c, s')  c = Skip  s' = Normal s"
  apply  (erule converse_rtranclpE)
   apply simp
  apply (erule step_Normal_elim_cases)
 done

lemma Throw_normal_steps_end:
"Γ  (Throw, Normal s) * (c, s')  c = Throw  s' = Normal s"
  apply  (erule converse_rtranclpE)
   apply simp
  apply (erule step_Normal_elim_cases)
 done

lemma while_relpower_induct:
 "t c' x .
       Γ⊨⇘/FP c i,A 
       i  b  P 
       i  - b  Q 
       final (c', t) 
       x  i 
       t  Fault ` F 
       c' = Throw  t  Normal ` A 
       (step Γ ^^ n) (While b c, Normal x) (c', t)  c' = Skip  t  Normal ` Q"
  apply (induct n rule:less_induct)
  apply (rename_tac n t c' x)
  apply (case_tac n)
   apply (clarsimp simp: final_def)
  apply clarify
  apply (simp only: relpowp.simps)
  apply (subst (asm) relpowp_commute[symmetric])
  apply clarsimp
  apply (erule step_Normal_elim_cases)
   apply clarsimp
   apply (rename_tac t c' x v)
   apply(case_tac "t")
    apply clarsimp
    apply(drule Seq_decomp_relpow)
     apply(simp add: final_def)
     apply(erule disjE, erule conjE)
      apply clarify
      apply(drule relpowp_imp_rtranclp)
      apply (simp add: valid_def)
      apply (rename_tac x n t' n1)
      apply (drule_tac x="Normal x" in spec)
      apply (drule_tac x="Normal t'" in spec)
      apply (drule spec[where x=Throw])
      apply (fastforce simp add: final_def)
     apply clarsimp
     apply (rename_tac c' x n t' t n1 n2)
     apply (drule_tac x=n2 and y="Normal t'" in meta_spec2)
     apply (drule_tac x=c' and y="t" in meta_spec2)
     apply (erule meta_impE, fastforce)
     apply (erule meta_impE, fastforce)
     apply (erule meta_impE)
      apply(drule relpowp_imp_rtranclp)
      apply (simp add: valid_def)
      apply (drule_tac x="Normal x" and y="Normal t" in spec2)
      apply (drule spec[where x=Skip])
      apply (fastforce simp add: final_def)
     apply assumption
    apply clarsimp
    apply (rename_tac c' s n f)
    apply (subgoal_tac "c' = Skip", simp)
     prefer 2
     apply (case_tac c'; fastforce simp: final_def)
    apply (drule Seq_decomp_relpowp_Fault)
    apply (erule disjE)
     apply (clarsimp simp: valid_def)
     apply (drule_tac x="Normal s" and y="Fault f" in spec2)
     apply (drule spec[where x=Skip])
     apply(drule relpowp_imp_rtranclp)
     apply (fastforce simp: final_def)
    apply clarsimp
    apply (rename_tac t n1 n2)
    apply (subgoal_tac "t  i")
     prefer 2
     apply (fastforce dest:relpowp_imp_rtranclp simp: final_def valid_def)
    apply (drule_tac x=n2 in meta_spec)
    apply (drule_tac x="Fault f" in meta_spec)
    apply (drule meta_spec[where x=Skip])
    apply (drule_tac x=t in meta_spec)
    apply (fastforce simp: final_def)
   apply clarsimp
   apply (rename_tac c' s n)
   apply (subgoal_tac "c' = Skip", simp)
    prefer 2
    apply (case_tac c'; fastforce simp: final_def)
    apply (drule Seq_decomp_relpowp_Stuck)
    apply clarsimp
    apply (erule disjE)
     apply (simp add:valid_def)
     apply (drule_tac x="Normal s" and y="Stuck" in spec2)
     apply clarsimp
     apply (drule spec[where x=Skip])
     apply(drule relpowp_imp_rtranclp)
     apply (fastforce)
    apply clarsimp
   apply (rename_tac t n1 n2)
   apply (subgoal_tac "t  i")
    prefer 2
    apply (fastforce dest:relpowp_imp_rtranclp simp: final_def valid_def)
   apply (drule_tac x=n2 in meta_spec)
   apply (drule meta_spec[where x=Stuck])
   apply (drule meta_spec[where x=Skip])
   apply (drule_tac x=t in meta_spec)
   apply (fastforce simp: final_def)
  apply clarsimp
  apply (drule relpowp_imp_rtranclp)
  apply (drule Skip_normal_steps_end)
  apply fastforce
done

lemma valid_weaken_pre:
 "Γ⊨⇘/FP c Q,A 
  P'  P  Γ⊨⇘/FP' c Q,A"
 by (fastforce simp: valid_def)

lemma valid_strengthen_post:
 "Γ⊨⇘/FP c Q,A 
  Q  Q'  Γ⊨⇘/FP c Q',A"
 by (fastforce simp: valid_def)

lemma valid_strengthen_abr:
 "Γ⊨⇘/FP c Q,A 
  A  A'  Γ⊨⇘/FP c Q,A'"
 by (fastforce simp: valid_def)

lemma oghoare_while_valid:
 "Γ⊨⇘/FP c i,A 
  i  b  P 
  i  - b  Q 
  Γ⊨⇘/Fi While b c Q,A"
  apply (simp (no_asm) add: valid_def)
  apply (clarsimp simp add: )
  apply (drule rtranclp_imp_relpowp)
  apply (clarsimp)
  by (erule while_relpower_induct)

lemma oghoare_catch_valid:
 "Γ⊨⇘/FP1 c1 Q,P2 
  Γ⊨⇘/FP2 c2 Q,A 
    Γ⊨⇘/FP1 Catch c1 c2 Q,A"
  apply (clarsimp simp add: valid_def[where c="Catch _ _"])
  apply (rename_tac t c' s)
  apply (case_tac t)
    apply simp            
    apply (drule Catch_decomp_star)
     apply (fastforce simp: final_def)
    apply clarsimp
    apply (erule disjE)
     apply (clarsimp simp add: valid_def[where c="c1"])
     apply (rename_tac s x t)
     apply (drule_tac x="Normal s" in spec) 
     apply (drule_tac x="Normal t" in spec)
     apply (drule_tac x=Throw in spec)
     apply (fastforce simp: final_def valid_def)
    apply (clarsimp simp add: valid_def[where c="c1"])
    apply (rename_tac s t)
    apply (drule_tac x="Normal s" in spec)
    apply (drule_tac x="Normal t" in spec)
    apply (drule_tac x=Skip in spec)
    apply (fastforce simp: final_def)
   apply (rename_tac c' s t)
   apply (simp add: final_def)
   apply (drule Catch_decomp_star_Fault)
   apply clarsimp
   apply (erule disjE)
    apply (clarsimp simp: valid_def[where c=c1] final_def)
   apply (fastforce simp: valid_def final_def)
  apply (simp add: final_def)
  apply (drule Catch_decomp_star_Stuck)
  apply clarsimp
  apply (erule disjE)
   apply (clarsimp simp: valid_def[where c=c1] final_def)
  apply (fastforce simp: valid_def final_def)
 done

lemma ann_matches_imp_assertionsR:
  "ann_matches Γ Θ a c  ¬ pre_par a 
    assertionsR Γ Θ Q A a c (pre a)"
  by (induct arbitrary: Q A  rule: ann_matches.induct , (fastforce intro:  assertionsR.intros )+)

lemma ann_matches_imp_assertionsR':
  "ann_matches Γ Θ a c  a'  pre_set a 
    assertionsR Γ Θ Q A a c a'"
 apply (induct arbitrary: Q A  rule: ann_matches.induct)
  apply ((fastforce intro:  assertionsR.intros )+)[12]
  apply simp
  apply (erule bexE)
  apply (simp only: in_set_conv_nth)
  apply (erule exE)
  apply (drule_tac x=i in spec)
  apply clarsimp
  apply (erule AsParallelExprs)
  apply simp
done

lemma rtranclp_conjD:
  "(λx1 x2. r1 x1 x2  r2 x1 x2)** x1 x2 
  r1** x1 x2  r2** x1 x2"
by (metis (no_types, lifting) rtrancl_mono_proof)

lemma rtranclp_mono' :
"r** a b  r  s  s** a b"
by (metis rtrancl_mono_proof sup.orderE sup2CI)

lemma state_upd_in_atomicsR[rule_format, OF _ refl refl]:
 "Γ cf  cf' 
   cf = (c, Normal s) 
   cf' = (c', Normal t) 
       s  t  
       ann_matches Γ Θ a c 
       s  pre a 
       (p cm x. atomicsR Γ Θ a c (p, cm)  s  p 
       Γ  (cm, Normal s)  (x, Normal t)  final (x, Normal t))"
supply [[simproc del: defined_all]]
  apply (induct arbitrary: c c' s t a rule: step.induct, simp_all)
       apply clarsimp
       apply (erule  ann_matches.cases, simp_all)
       apply (rule exI)+
       apply (rule conjI)
        apply (rule atomicsR.intros)
        apply clarsimp
        apply (rule_tac x="Skip" in exI)
        apply (simp add: final_def)
        apply (rule step.Basic)
       apply clarsimp
       apply (erule  ann_matches.cases, simp_all)
       apply (rule exI)+
       apply (rule conjI)
        apply (rule atomicsR.intros)
        apply clarsimp
        apply (rule_tac x="Skip" in exI)
        apply (simp add: final_def)
        apply (erule step.Spec)
      apply clarsimp
      apply (erule  ann_matches.cases, simp_all)
      apply clarsimp        
      apply (drule meta_spec)+
      apply (erule meta_impE, rule conjI, (rule refl)+)+
      apply clarsimp
      apply (erule (1) meta_impE)
      apply (erule meta_impE, fastforce)
      apply clarsimp
      apply (rule exI)+
      apply (rule conjI)
      apply (erule AtSeqExpr1)
     apply fastforce
    apply clarsimp
    apply (erule  ann_matches.cases, simp_all)
    apply clarsimp        
    apply (drule meta_spec)+
    apply (erule meta_impE, rule conjI, (rule refl)+)+
    apply clarsimp
    apply (erule (1) meta_impE)
    apply (erule meta_impE, fastforce)
    apply clarsimp
    apply (rule exI)+
    apply (rule conjI)
    apply (erule AtCatchExpr1)
    apply fastforce
    apply (erule  ann_matches.cases, simp_all)
    apply clarsimp
    apply (drule meta_spec)+
    apply (erule meta_impE, rule conjI, (rule refl)+)+
    apply clarsimp
    apply (erule meta_impE)
     apply fastforce
    apply (erule meta_impE)
     apply (case_tac "i=0"; fastforce)
    apply clarsimp
    apply (rule exI)+
    apply (rule conjI)
     apply (erule AtParallelExprs)
    apply fastforce
   apply (drule_tac x=i in spec)
   apply clarsimp
   apply fastforce
  apply (erule ann_matches.cases, simp_all)
  apply clarsimp
  apply (rule exI)+
  apply (rule conjI)
   apply (rule AtAwait)
   apply clarsimp
   apply (rename_tac c' sa t aa e r ba)
   apply (rule_tac x=c' in exI)
   apply (rule conjI)
    apply (erule step.Await)
   apply (erule rtranclp_mono')
   apply clarsimp
   apply assumption+
   apply (simp add: final_def)
 done

lemma oghoare_atom_com_sound:
  "Γ, Θ ⊩⇘/FP a c Q,A  atom_com c  Γ ⊨⇘/FP c Q, A"
 unfolding valid_def 
  proof (induct rule: oghoare_seq_induct)
    case SeqSkip thus ?case 
      by (fastforce 
            elim: converse_rtranclpE step_Normal_elim_cases(1))
  next
    case SeqThrow thus ?case
    by (fastforce 
            elim: converse_rtranclpE step_Normal_elim_cases)
  next 
    case SeqBasic thus ?case 
      by (fastforce 
            elim: converse_rtranclpE step_Normal_elim_cases 
            simp: final_def)
  next 
    case (SeqSpec Γ Θ F r Q A) thus ?case
    apply clarsimp
    apply (erule converse_rtranclpE) 
     apply (clarsimp simp: final_def)
    apply (erule step_Normal_elim_cases)
     apply (fastforce elim!: converse_rtranclpE step_Normal_elim_cases)
    by clarsimp
  next
    case (SeqSeq Γ Θ F P1 c1 P2 A c2 Q) show ?case
     using SeqSeq
     by (fold valid_def) 
        (fastforce intro: oghoare_seq_valid simp: valid_weaken_pre)
   next 
    case (SeqCatch Γ Θ F P1 c1 Q P2 c2 A) thus ?case
    apply (fold valid_def)
    apply simp
    apply (fastforce elim:  oghoare_catch_valid)+
    done
   next 
    case (SeqCond Γ Θ F P b c1 Q A c2) thus ?case
     by (fold valid_def)
        (fastforce intro:oghoare_if_valid)
   next 
    case (SeqWhile Γ Θ F P c A b) thus ?case
     by (fold valid_def)
        (fastforce elim: valid_weaken_pre[rotated] oghoare_while_valid)
   next
    case (SeqGuard Γ Θ F P c Q A r g f) thus ?case
    apply (fold valid_def)
    apply (simp (no_asm) add: valid_def)
    apply clarsimp
    apply (erule converse_rtranclpE)
     apply (fastforce simp: final_def)
    apply clarsimp
    apply (erule step_Normal_elim_cases)
     apply (case_tac "r  - g  {}")
      apply clarsimp
      apply (fastforce simp: valid_def)
     apply clarsimp
     apply (fastforce simp: valid_def)
    apply clarsimp
     apply (case_tac "r  - g  {}")
      apply (fastforce dest: no_steps_final simp:final_def)
     apply (fastforce dest: no_steps_final simp:final_def)
   done
   next
    case (SeqCall Γ p f Θ F P Q A) thus ?case
     by simp
   next

    case (SeqDynCom r fa Γ Θ F P c Q A) thus ?case
    apply -
    apply clarsimp
    apply (erule converse_rtranclpE)
     apply (clarsimp simp: final_def)
    apply clarsimp
    apply (erule step_Normal_elim_cases)
    apply clarsimp
    apply (rename_tac t c' x)

    apply (drule_tac x=x in spec)
    apply (drule_tac x=x in bspec, fastforce)
    apply clarsimp
    apply (drule_tac x="Normal x" in spec)
    apply (drule_tac x="t" in spec)
    apply (drule_tac x="c'" in spec)
    apply fastforce+
   done
   next 
    case (SeqConseq Γ Θ F P c Q A) thus ?case 
     apply (clarsimp)
     apply (rename_tac t c' x)
     apply (erule_tac x="Normal x" in allE)
     apply (erule_tac x="t" in allE)
     apply (erule_tac x="c'" in allE)
     apply (clarsimp simp: pre_weaken_pre)
     apply force
    done
qed simp_all

lemma ParallelRuleAnn:
" length as = length cs 
  i<length cs. Γ,Θ ⊢⇘/F(pres (as ! i)) (cs ! i) (postcond (as ! i)),(abrcond (as ! i)) 
  interfree Γ Θ F as cs 
  (set (map postcond as))  Q 
  (set (map abrcond as))  A  Γ,Θ ⊢⇘/F(AnnPar as) (Parallel cs) Q,A"
 apply (erule (3) Parallel)
 apply auto
done

lemma oghoare_step[rule_format, OF _ refl refl]:
shows
 "Γ  cf  cf'  cf = (c, Normal s)  cf' = (c', Normal t) 
  Γ,Θ⊢⇘/Fa c Q,A 
 s  pre a 
a'. Γ,Θ⊢⇘/Fa' c' Q,A  t  pre a' 
        (as. assertionsR Γ Θ Q A a' c' as  assertionsR Γ Θ Q A a c as) 
        (pm cm. atomicsR Γ Θ a' c' (pm, cm)  atomicsR Γ Θ  a c (pm, cm))"
 proof (induct arbitrary:c c' s a t Q A rule: step.induct)
   case (Parallel i cs s c' s' ca c'a sa a t Q A) thus ?case
     supply [[simproc del: defined_all]]
     apply (clarsimp simp:)
     apply (drule oghoare_Parallel)
     apply clarsimp
     apply (rename_tac as)
     apply (frule_tac x=i in spec, erule (1) impE)
     apply (elim exE conjE)


     apply (drule meta_spec)+
     apply (erule meta_impE, rule conjI, (rule refl)+)+
     apply (erule meta_impE)
      apply (rule_tac P="(pres (as ! i))" in Conseq)
      apply (rule exI[where x="{}"])
      apply (rule_tac x="Q'" in exI)
      apply (rule_tac x="A'" in exI)
      apply (simp)
     apply (erule meta_impE, simp)
     apply clarsimp
     apply (rule_tac x="AnnPar (as[i:=(a',postcond(as!i), abrcond(as!i))])" in exI)
     apply (rule conjI)
      apply (rule ParallelRuleAnn, simp)
          apply clarsimp
          apply (rename_tac j)
          apply (drule_tac x=j in spec)
          apply clarsimp
          apply (case_tac "i = j")
           apply (clarsimp simp: )
           apply (rule Conseq)
           apply (rule exI[where x="{}"])
           apply (fastforce)
          apply simp
          apply (clarsimp simp: interfree_def)
          apply (rename_tac i' j')
          apply (drule_tac x=i' and y=j' in spec2)
          apply clarsimp
          apply (case_tac "i = i'")
           apply clarsimp
           apply (simp add: interfree_aux_def prod.case_eq_if )
          apply clarsimp
          apply (case_tac "j' = i")
           apply (clarsimp)
           apply (simp add: interfree_aux_def prod.case_eq_if)
           apply clarsimp
          apply (clarsimp)
         apply (erule subsetD)
         apply (clarsimp simp: in_set_conv_nth)
         apply (rename_tac a' x a b c i')
         apply (case_tac "i' = i")
          apply clarsimp
          apply (drule_tac x="(a', b, c)" in bspec, simp)
           apply (fastforce simp add: in_set_conv_nth)
          apply fastforce
         apply (drule_tac x="(a, b, c)" in bspec, simp)
          apply (simp add: in_set_conv_nth)
          apply (rule_tac x=i' in exI)
          apply clarsimp
         apply fastforce
     apply clarsimp
     apply (erule_tac A="(xset as. abrcond x) " in  subsetD)
     apply (clarsimp simp: in_set_conv_nth)
     apply (rename_tac a b c j)
     apply (case_tac "j = i")
      apply clarsimp
      apply (rule_tac x="as!i" in bexI)
       apply simp
     apply clarsimp
    apply clarsimp
    apply (rule_tac x="(a,b,c)" in bexI)
     apply simp
    apply (clarsimp simp:in_set_conv_nth)
    apply (rule_tac x=j in exI)
    apply fastforce
   apply (rule conjI)
    apply (case_tac "s = Normal t")
     apply clarsimp
     apply (clarsimp simp: in_set_conv_nth)
     apply (rename_tac a b c j)
     apply (case_tac "j = i")
      apply clarsimp
     apply clarsimp
     apply (drule_tac x="as!j" in bspec)
      apply (clarsimp simp add: in_set_conv_nth)
      apply (rule_tac x=j in exI)
      apply fastforce
     apply clarsimp
    apply (frule state_upd_in_atomicsR, simp)
      apply (erule oghoare_imp_ann_matches)
     apply (clarsimp simp: in_set_conv_nth)
     apply fastforce
    apply (clarsimp simp: in_set_conv_nth)
    apply (rename_tac j)
    apply (case_tac "j = i")
     apply clarsimp
    apply clarsimp
    apply (thin_tac "Γ,Θ ⊢⇘/Fa' c'  (postcond (as ! i)),(abrcond (as ! i))")
    apply (simp add: interfree_def interfree_aux_def)
    apply (drule_tac x="j" and y=i in spec2)
    apply (simp add: prod.case_eq_if)
    apply (drule spec2, drule (1) mp)
    apply clarsimp
    apply (case_tac "pre_par a")
     apply (subst pre_set)
     apply clarsimp
     apply (drule_tac x="as!j" in bspec) 
      apply (clarsimp simp: in_set_conv_nth)
      apply (rule_tac x=j in exI)
      apply fastforce
     apply clarsimp
     apply (frule (1) pre_imp_pre_set)
     apply (rename_tac as Q' A' a' a b c p cm x j X)
     apply (drule_tac x="X" in spec, erule_tac P="assertionsR Γ Θ b c a (cs ! j) X" in impE)
      apply (rule ann_matches_imp_assertionsR')
       apply (drule_tac x=j in spec, clarsimp)
       apply (erule (1) oghoare_imp_ann_matches)
     apply (rename_tac a b c p cm x j X )
     apply (thin_tac "Γ⊨⇘/F(b  p) cm b,b")
     apply (thin_tac " Γ⊨⇘/F(c  p) cm c,c")
     apply (simp add: valid_def)
     apply (drule_tac x="Normal sa" in spec)
     apply (drule_tac x="Normal t" in spec)
     apply (drule_tac x=x in spec)
     apply (erule impE, fastforce)
     apply force

   apply (drule_tac x=j in spec)
   apply clarsimp
   apply (rename_tac a b c p cm x j Q'' A'')
   apply (drule_tac x="pre a" in spec,erule impE, rule ann_matches_imp_assertionsR)
     apply (erule (1) oghoare_imp_ann_matches)
     apply (thin_tac " Γ⊨⇘/F(b  p) cm b,b")
     apply (thin_tac " Γ⊨⇘/F(c  p) cm c,c")
    apply (simp add: valid_def)
    apply (drule_tac x="Normal sa" in spec)
    apply (drule_tac x="Normal t" in spec)
    apply (drule_tac x=x in spec)
    apply (erule impE, fastforce)
    apply clarsimp
    apply (drule_tac x="as ! j" in bspec)
     apply (clarsimp simp: in_set_conv_nth)
     apply (rule_tac x=j in exI, fastforce)
    apply clarsimp
    apply fastforce
  apply (rule conjI)
    apply (clarsimp simp: )
    apply (erule assertionsR.cases ; simp)
      apply (clarsimp simp: )
      apply (rename_tac j a)
      apply (case_tac "j = i")
       apply clarsimp
       apply (drule_tac x=a in spec, erule (1) impE) 
       apply (erule (1)  AsParallelExprs)
      apply (subst (asm) nth_list_update_neq, simp)
      apply (erule_tac i=j in  AsParallelExprs)
      apply fastforce
     apply clarsimp
    apply (rule  AsParallelSkips)
    apply (clarsimp simp:)
    apply (rule equalityI)
     apply (clarsimp simp: in_set_conv_nth)
     apply (rename_tac a' x a b c j)
     apply (case_tac "j = i")
      apply (thin_tac "aset as. sa  precond a")
      apply clarsimp
      apply (drule_tac x="(a', b, c)" in bspec)
      apply (clarsimp simp: in_set_conv_nth)
      apply (rule_tac x="i" in exI)
      apply fastforce
     apply fastforce
    apply (drule_tac x="as ! j" in bspec)
     apply (clarsimp simp: in_set_conv_nth)
     apply (rule_tac x=j in exI)
     apply fastforce
   apply clarsimp
   apply (drule_tac x=" as ! j" in bspec)
    apply (clarsimp simp: in_set_conv_nth)
    apply (rule_tac x=j in exI, fastforce)
    apply fastforce
   apply (clarsimp simp: in_set_conv_nth)
   apply (rename_tac x a b c j)
   apply (thin_tac "aset as. sa  precond a")
   apply (case_tac "j = i")
    apply clarsimp
    apply (drule_tac x="as!i" in bspec, fastforce)
    apply fastforce
   apply clarsimp
   apply (drule_tac x="as!j" in bspec)
   apply (clarsimp simp: in_set_conv_nth)
   apply (rule_tac x=j in exI, fastforce)
   apply fastforce
  apply clarsimp
  apply (erule atomicsR.cases ; simp)
  apply clarsimp
  apply (rename_tac j atc atp)
  apply (case_tac "j = i")
   apply clarsimp
   apply (drule_tac x=atc and y=atp in spec2, erule impE)
    apply (clarsimp)
   apply (erule (1)  AtParallelExprs)
  apply (subst (asm) nth_list_update_neq, simp)
  apply (erule_tac i=j in  AtParallelExprs)
  apply (clarsimp)
 done
next
 case (Basic f s c c' sa a t Q A) thus ?case
  apply clarsimp
  apply (drule oghoare_Basic)
  apply clarsimp
  apply (rule_tac x="AnnExpr Q" in exI)
  apply clarsimp
  apply (rule conjI)
   apply (rule SkipRule)
   apply fastforce
  apply (rule conjI)
   apply fastforce
  apply clarsimp
  apply (drule assertionsR.cases, simp_all)
  apply (rule assertionsR.AsBasicSkip)
 done
next
  case (Spec s t r c c' sa a ta Q A) thus ?case
  apply clarsimp
  apply (drule oghoare_Spec)
  apply clarsimp
  apply (rule_tac x="AnnExpr Q" in exI)
  apply clarsimp
  apply (rule conjI)
   apply (rule SkipRule)
   apply fastforce
  apply (rule conjI)
   apply force
  apply clarsimp
  apply (erule assertionsR.cases, simp_all)
  apply clarsimp
  apply (rule assertionsR.AsSpecSkip)
 done
next
  case (Guard s g f c ca c' sa a t Q A) thus ?case
  apply -
  apply clarsimp
  apply (drule oghoare_Guard)
  apply clarsimp
  apply (rule exI, rule conjI, assumption)
   by (fastforce dest: oghoare_Guard
                 intro:assertionsR.intros atomicsR.intros)
next
  case (GuardFault s g f c ca c' sa a t Q A) thus ?case
   by (fastforce dest: oghoare_Guard
                 intro:assertionsR.intros atomicsR.intros)
next
  case (Seq c1 s c1' s' c2 c c' sa a t A Q) thus ?case
    supply [[simproc del: defined_all]]
    apply (clarsimp simp:)
    apply (drule oghoare_Seq)
    apply clarsimp
    apply (drule meta_spec)+
    apply (erule meta_impE, rule conjI, (rule refl)+)+
    apply (erule meta_impE)
     apply (rule Conseq)
     apply (rule exI[where x="{}"])
     apply (rule exI)+
     apply (rule conjI)
      apply (simp)
     apply (erule (1) conjI)
    apply clarsimp
    apply (rule_tac x="AnnComp a' P2" in exI, rule conjI)
     apply (rule oghoare_oghoare_seq.Seq)
      apply (rule Conseq)
      apply (rule_tac x="{}" in exI)
      apply (fastforce)
     apply (rule Conseq)
     apply (rule_tac x="{}" in exI)
     apply (fastforce)
    apply clarsimp
    apply (rule conjI)
     apply clarsimp
     apply (erule assertionsR.cases, simp_all)
      apply clarsimp
      apply (drule_tac x=a in spec, simp)
      apply (erule AsSeqExpr1)
      apply clarsimp
     apply (erule AsSeqExpr2)
    apply clarsimp
    apply (erule atomicsR.cases, simp_all)
      apply clarsimp
      apply (drule_tac x="a" and y=b in spec2, simp)
      apply (erule AtSeqExpr1)
      apply clarsimp
     apply (erule AtSeqExpr2)
   done
next
  case (SeqSkip c2 s c c' sa a t Q A) thus ?case
   apply clarsimp
   apply (drule oghoare_Seq)
    apply clarsimp
    apply (rename_tac P1 P2 P' Q' A')
    apply (rule_tac x=P2 in exI)
    apply (rule conjI, rule Conseq)
     apply (rule_tac x="{}" in exI)
     apply (fastforce)
    apply (rule conjI)
     apply (drule oghoare_Skip)
     apply fastforce
    apply (rule conjI)
     apply clarsimp
    apply (erule assertionsR.AsSeqExpr2)
   apply clarsimp
   apply (fastforce intro: atomicsR.intros)
  done
next
  case (SeqThrow c2 s c c' sa a t Q A) thus ?case
   apply clarsimp
   apply (drule oghoare_Seq)
   apply clarsimp
   apply (rename_tac P1 P2 P' Q' A')
   apply (rule_tac x=P1 in exI)
   apply (drule oghoare_Throw)
   apply clarsimp
   apply (rename_tac P'')
   apply (rule conjI, rule Conseq)
    apply (rule_tac x="{}" in exI)
    apply (rule_tac x="Q'" in exI)
    apply (rule_tac x="P''" in exI)
    apply (fastforce intro: Throw)
   apply clarsimp
   apply (erule assertionsR.cases, simp_all)
   apply clarsimp
   apply (rule AsSeqExpr1)
   apply (rule AsThrow)
  done
next
  case (CondTrue s b c1 c2 c sa c' s' ann) thus ?case
   apply (clarsimp)
   apply (drule oghoare_Cond)
   apply clarsimp
   apply (rename_tac P' P1 P2 Q' A')
   apply (rule_tac x= P1 in exI)
   apply (rule conjI) 
    apply (rule Conseq, rule_tac x="{}" in exI, fastforce)
   apply (rule conjI, fastforce)
   apply (rule conjI)
    apply (fastforce elim: assertionsR.cases intro: AsCondExpr1)
   apply (fastforce elim: atomicsR.cases intro: AtCondExpr1)
  done
next
  case (CondFalse s b c1 c2 c sa c' s' ann) thus ?case
   apply (clarsimp)
   apply (drule oghoare_Cond)
   apply clarsimp
   apply (rename_tac P' P1 P2 Q' A')
   apply (rule_tac x= P2 in exI)
   apply (rule conjI) 
    apply (rule Conseq, rule_tac x="{}" in exI, fastforce)
   apply (rule conjI, fastforce)
   apply (rule conjI)
    apply (fastforce elim: assertionsR.cases intro: AsCondExpr2)
   apply (fastforce elim: atomicsR.cases intro: AtCondExpr2)
  done
next
  case (WhileTrue s b c ca sa c' s' ann) thus ?case
  apply clarsimp
  apply (frule oghoare_While)
  apply clarsimp
  apply (rename_tac r i P' A' Q')
  apply (rule_tac x="AnnComp P' (AnnWhile i i P')" in exI)
  apply (rule conjI)
   apply (rule Seq)
     apply (rule Conseq) 
     apply (rule_tac x="{}" in exI)
     apply (rule_tac x="i" in exI)
     apply (rule_tac x="A'" in exI)
     apply (subst weaken_pre_empty)
     apply clarsimp
    apply (rule While)
       apply (rule Conseq) 
       apply (rule_tac x="{}" in exI)
       apply (rule_tac x="i" in exI)
       apply (rule_tac x="A'" in exI)
       apply (subst weaken_pre_empty)
       apply clarsimp
      apply clarsimp
     apply force
    apply simp
   apply simp
  apply (rule conjI)
   apply blast
  apply (rule conjI)
   apply clarsimp
   apply (erule assertionsR.cases, simp_all)
    apply clarsimp
    apply (rule AsWhileExpr)
   apply clarsimp
   apply (erule assertionsR.cases,simp_all)
      apply clarsimp
      apply (erule AsWhileExpr)
     apply clarsimp
     apply (rule AsWhileInv)
    apply clarsimp
    apply (rule AsWhileInv)
   apply clarsimp
   apply (rule AsWhileSkip)
  apply clarsimp
  apply (erule atomicsR.cases, simp_all)
   apply clarsimp
   apply (rule AtWhileExpr)
  apply clarsimp+
  apply (erule atomicsR.cases, simp_all)
   apply clarsimp
  apply (erule AtWhileExpr)
  done
next
  case (WhileFalse s b c ca sa c' ann s' Q A) thus ?case
   apply clarsimp
   apply (drule oghoare_While)
   apply clarsimp
   apply (rule_tac x="AnnExpr Q" in exI)
   apply (rule conjI)
    apply (rule SkipRule)
    apply blast
   apply (rule conjI)
    apply fastforce
   apply clarsimp
   apply (erule assertionsR.cases, simp_all)
   apply (drule sym, simp, rule AsWhileSkip)
  done
next
  case (Call p bs s c c' sa a t Q A) thus ?case
  apply clarsimp
  apply (drule oghoare_Call)
  apply clarsimp
  apply (rename_tac n as)
  apply (rule_tac x="as ! n" in exI)
  apply clarsimp
  apply (rule conjI, fastforce)
  apply (rule conjI)
   apply clarsimp
   apply (erule (2) AsCallExpr)
   apply fastforce
  apply clarsimp
  apply (erule (2) AtCallExpr)
  apply simp
 done
next
  case (DynCom c s ca c' sa a t Q A) thus ?case
  apply -
  apply clarsimp
  apply (drule oghoare_DynCom)
  apply clarsimp
  apply (drule_tac x=t in bspec, assumption)
  apply (rule exI)
  apply (erule conjI)
  apply (rule conjI, fastforce)
  apply (rule conjI)
   apply clarsimp
   apply (erule (1) AsDynComExpr)
  apply (clarsimp)
  apply (erule (1) AtDynCom)
  done
next
  case (Catch c1 s c1' s' c2 c c' sa a t Q A) thus ?case
    supply [[simproc del: defined_all]]
    apply (clarsimp simp:)
    apply (drule oghoare_Catch)
    apply clarsimp
    apply (drule meta_spec)+
    apply (erule meta_impE, rule conjI, (rule refl)+)+
    apply (erule meta_impE)
     apply (rule Conseq)
     apply (rule exI[where x="{}"])
     apply (rule exI)+
     apply (rule conjI)
      apply (simp)
     apply (erule (1) conjI)
    apply clarsimp
    apply (rename_tac P1 P2 P' Q' A' a')
    apply (rule_tac x="AnnComp a' P2" in exI, rule conjI)
     apply (rule oghoare_oghoare_seq.Catch)
      apply (rule Conseq)
      apply (rule_tac x="{}" in exI)
      apply (fastforce)
     apply (rule Conseq)
     apply (rule_tac x="{}" in exI)
     apply (fastforce)
    apply clarsimp
   apply (rule conjI)
    apply clarsimp
     apply (erule assertionsR.cases, simp_all)
      apply clarsimp
      apply (rename_tac a)
      apply (drule_tac x=a in spec, simp)
      apply (erule AsCatchExpr1)
     apply clarsimp
     apply (erule AsCatchExpr2)
    apply clarsimp
    apply (erule atomicsR.cases, simp_all)
      apply clarsimp
      apply (rename_tac a b a2)
      apply (drule_tac x="a" and y=b in spec2, simp)
      apply (erule AtCatchExpr1)
      apply clarsimp
     apply (erule AtCatchExpr2)
   done
next
  case (CatchSkip c2 s c c' sa a t Q A) thus ?case
   apply clarsimp
   apply (drule oghoare_Catch, clarsimp)
   apply (rename_tac P1 P2 P' Q' A')
   apply (rule_tac x=P1 in exI)
   apply clarsimp
   apply (rule conjI)
    apply (rule Conseq)
    apply (rule_tac x="{}" in exI)
    apply (drule oghoare_Skip)
    apply clarsimp
    apply (rule_tac x=Q' in exI)
    apply (rule_tac x=A' in exI)
    apply (rule conjI, erule SkipRule)
    apply clarsimp
   apply clarsimp
   apply (rule AsCatchExpr1)
   apply (erule assertionsR.cases, simp_all)
   apply (rule assertionsR.AsSkip)
  done
next
  case (CatchThrow c2 s c c' sa a t Q A) thus ?case
  apply clarsimp
  apply (drule oghoare_Catch, clarsimp)
  apply (rename_tac P1 P2 P' Q' A')
  apply (rule_tac x=P2 in exI)
  apply (rule conjI)
   apply (rule Conseq)
   apply (rule_tac x="{}" in exI)
   apply (fastforce )
  apply (rule conjI)
   apply (drule oghoare_Throw)
   apply clarsimp
   apply fastforce
  apply (rule conjI)
   apply (clarsimp)
   apply (erule AsCatchExpr2)
  apply clarsimp
  apply (erule AtCatchExpr2)
 done
next
 case (ParSkip cs s c c' sa a t Q A) thus ?case
  apply clarsimp
  apply (drule oghoare_Parallel)
  apply clarsimp
  apply (rename_tac as)
    
  apply (rule_tac x="AnnExpr (xset as. postcond x)" in exI)
  apply (rule conjI, rule SkipRule)
   apply blast
  apply (rule conjI)
   apply simp
    apply clarsimp
    apply (simp only: in_set_conv_nth)
    apply clarsimp
    apply (drule_tac x="i" in spec)
    apply clarsimp
    apply (drule_tac x="cs!i" in bspec)
     apply clarsimp
    apply clarsimp
    apply (drule oghoare_Skip)
    apply clarsimp
    apply (drule_tac x="as!i" in bspec)
     apply (clarsimp simp: in_set_conv_nth)
     apply (rule_tac x=i in exI, fastforce)
     apply clarsimp
     apply blast
  apply clarsimp
  apply (erule assertionsR.cases; simp)
  apply clarsimp
  apply (rule AsParallelSkips; clarsimp)
 done
next
 case (ParThrow cs s c c' sa a t Q A) thus ?case
  apply clarsimp
  apply (drule oghoare_Parallel)
  apply (clarsimp simp: in_set_conv_nth)  
  apply (drule_tac x=i in spec)
  apply clarsimp
  apply (drule oghoare_Throw)
  apply clarsimp
  apply (rename_tac i as Q' A' P')
  apply (rule_tac x="AnnExpr P'" in exI)
  apply (rule conjI)
   apply (rule ThrowRule)
   apply clarsimp
   apply (erule_tac A="(xset as. abrcond x)" in subsetD[where B=A], force)
  apply (rule conjI)
   apply (drule_tac x="as!i" in bspec)
    apply (clarsimp simp: in_set_conv_nth)
    apply (rule_tac x=i in exI, fastforce)
   apply (fastforce)
  apply clarsimp
  apply (erule AsParallelExprs)
  apply clarsimp
  apply (erule assertionsR.cases, simp_all)
  apply (rule AsThrow)
 done
next
 case (Await x b c c' x' c'' c''' x'' a x''' Q A) thus ?case
   apply (clarsimp)
   apply (drule oghoare_Await)
   apply clarsimp

   apply (drule rtranclp_conjD)
   apply clarsimp
   apply (erule disjE)
    apply clarsimp
    apply (rename_tac P' Q' A')
    apply (rule_tac x="AnnExpr Q" in exI)
    apply clarsimp
    apply (rule conjI)
     apply (rule Skip)
    apply (rule conjI)
     apply (drule (1) oghoare_atom_com_sound)
     apply (fastforce simp: final_def valid_def)
    apply clarsimp
    apply (erule assertionsR.cases, simp_all)
    apply clarsimp
    apply (rule AsAwaitSkip)

   apply (rule_tac x="AnnExpr A" in exI)
   apply clarsimp
   apply (rule conjI)
    apply (rule Throw)
    apply (rule conjI)
     apply (drule (1) oghoare_atom_com_sound)
     apply (fastforce simp: final_def valid_def)
    apply clarsimp
    apply (erule assertionsR.cases, simp_all)
    apply clarsimp
    apply (rule AsAwaitThrow)
  done
qed simp_all

lemma oghoare_steps[rule_format, OF _ refl refl]:
 "Γ  cf * cf'  cf = (c, Normal s)  cf' = (c', Normal t) 
  Γ,Θ⊢⇘/Fa c Q,A 
 s  pre a 
a'. Γ,Θ⊢⇘/Fa' c' Q,A  t  pre a' 
        (as. assertionsR Γ Θ Q A a' c' as  assertionsR Γ Θ Q A a c as) 
        (pm cm. atomicsR Γ Θ a' c' (pm, cm)  atomicsR Γ Θ a c (pm, cm))"
  apply (induct arbitrary: a c s c' t rule: converse_rtranclp_induct)
   supply [[simproc del: defined_all]]
   apply fastforce
  apply clarsimp
  apply (frule Normal_pre_star)
  apply clarsimp
  apply (drule (2) oghoare_step)
  apply clarsimp
  apply ((drule meta_spec)+, (erule meta_impE, rule conjI, (rule refl)+)+)
  apply (erule (1) meta_impE)+
  apply clarsimp
  apply (rule exI)
  apply (rule conjI, fastforce)+
  apply force
 done

lemma oghoare_sound_Parallel_Normal_case[rule_format, OF _ refl refl]:
 "Γ  (c, s) * (c', t) 
   P x y cs. c = Parallel cs   s = Normal x 
      t = Normal y 
      Γ,Θ⊢⇘/FP c Q,A  final (c', t) 
       x  pre P  t  Fault ` F  (c' = Throw  t  Normal ` A)  (c' = Skip  t  Normal ` Q)"
  apply(erule converse_rtranclp_induct2)
   apply (clarsimp simp: final_def)
  apply(erule step.cases, simp_all)
― ‹Parallel›
    apply clarsimp
    apply (frule Normal_pre_star)
    apply (drule oghoare_Parallel)
    apply clarsimp
    apply (rename_tac i cs c1' x y  s' as)
    apply (subgoal_tac "Γ (Parallel cs, Normal x)  (Parallel (cs[i := c1']), Normal s')")
     apply (frule_tac c="Parallel cs" and
                      a="AnnPar as"  and
                      Q="(xset as. postcond x)" and A ="(xset as. abrcond x)"
                   in oghoare_step[where Θ=Θ and F=F])
       apply(rule Parallel, simp)
          apply clarsimp
          apply (rule Conseq, rule exI[where x="{}"], fastforce)
         apply clarsimp
        apply force
       apply force
      apply clarsimp
     apply clarsimp
     apply (rename_tac a')
     apply (drule_tac x=a' in spec)
     apply (drule mp, rule Conseq)
      apply (rule_tac x="{}" in exI)
      apply (rule_tac x="(xset as. postcond x)" in exI)
      apply (rule_tac x="(xset as. abrcond x)" in exI)
      apply (simp)
     apply clarsimp
    apply(erule (1) step.Parallel)
― ‹ParSkip›
   apply (frule no_steps_final, simp add: final_def)
   apply clarsimp
   apply (drule oghoare_Parallel)
   apply clarsimp
   apply (rule imageI)
   apply (erule subsetD)
   apply clarsimp
   apply (clarsimp simp: in_set_conv_nth)
   apply (rename_tac i)
   apply (frule_tac x="i" in spec)
   apply clarsimp
   apply (frule_tac x="cs!i" in bspec)
    apply (clarsimp simp: in_set_conv_nth)
    apply (rule_tac x="i" in exI)
    apply clarsimp
   apply clarsimp
   apply (drule_tac x="as ! i" in bspec)
    apply (clarsimp simp: in_set_conv_nth)
    apply fastforce
   apply (drule oghoare_Skip)
   apply fastforce
― ‹ParThrow›
  apply clarsimp
  apply (frule no_steps_final, simp add: final_def)
  apply clarsimp
  apply (drule oghoare_Parallel)
  apply (clarsimp simp: in_set_conv_nth)
  apply (drule_tac x=i in spec)
  apply clarsimp
  apply (drule oghoare_Throw)
  apply clarsimp
  apply (rename_tac i as Q' A' P')
  apply (drule_tac x="as ! i" in bspec)
   apply (clarsimp simp: in_set_conv_nth)
   apply (rule_tac x=i in exI, fastforce)
  apply clarsimp
  apply (rule imageI)
  apply (erule_tac  A="(xset as. abrcond x)" in subsetD)
  apply clarsimp
  apply (rule_tac x="as!i" in bexI)
   apply blast
  apply clarsimp
  done

lemma oghoare_step_Fault[rule_format, OF _ refl refl]:
 "Γ cf  cf' 
   cf = (c, Normal x) 
   cf' = (c', Fault f) 
   x  pre P 
   Γ,Θ⊢⇘/FP c Q,A  f  F"
  supply [[simproc del: defined_all]]
  apply (induct arbitrary: x c c' P Q A f rule: step.induct, simp_all)
       apply clarsimp
       apply (drule oghoare_Guard)
       apply clarsimp
       apply blast
      apply clarsimp
      apply (drule oghoare_Seq)
      apply clarsimp
     apply clarsimp
     apply (drule oghoare_Catch)
     apply clarsimp
    apply clarsimp
    apply (rename_tac i cs c' x P Q A f)
    apply (drule oghoare_Parallel)
    apply clarsimp
    apply (rename_tac i cs c' x Q A f as)
    apply (drule_tac x="i" in spec)
    apply clarsimp
    apply (drule meta_spec)+
    apply (erule meta_impE, rule conjI, (rule refl)+)+
    apply (drule_tac x="as!i" in bspec)
    apply (clarsimp simp: in_set_conv_nth)
    apply (rule_tac x="i" in exI, fastforce)
   apply (erule (1) meta_impE)
   apply (erule (2) meta_impE)
  apply clarsimp
  apply (drule rtranclp_conjD[THEN conjunct1])
  apply (drule oghoare_Await)
  apply clarsimp
  apply (rename_tac b c c' x Q A f r P' Q' A')
  apply (drule (1) oghoare_atom_com_sound)
  apply (simp add: valid_def)
  apply (drule_tac x="Normal x" in spec)
  apply (drule_tac x="Fault f" in spec)
  apply (drule_tac x=Skip in spec)
  apply clarsimp
  apply (erule impE)
   apply (cut_tac f=f and c=c' in  steps_Fault[where Γ=Γ])
   apply fastforce
   apply (fastforce simp: final_def steps_Fault)
 done

lemma oghoare_step_Stuck[rule_format, OF _ refl refl]:
 "Γ cf  cf' 
   cf = (c, Normal x) 
   cf' = (c', Stuck) 
   x  pre P 
   Γ,Θ⊢⇘/FP c Q,A  P'"
  apply (induct arbitrary: x c c' P Q A  rule: step.induct, simp_all)
         apply clarsimp
         apply (drule oghoare_Spec)
         apply force
        apply clarsimp
       apply (drule oghoare_Seq)
       apply clarsimp
      apply clarsimp
      apply (drule oghoare_Call)
      apply clarsimp
     apply clarsimp
     apply (drule oghoare_Catch)
     apply clarsimp
    apply clarsimp
    apply (drule oghoare_Parallel)
    apply clarsimp
    apply (rename_tac i cs c' x Q A as)
    apply (drule_tac x="i" in spec)
    apply clarsimp
    apply (drule meta_spec)+
    apply (drule_tac x="as!i" in bspec)
    apply (clarsimp simp: in_set_conv_nth)
    apply (rule_tac x="i" in exI, fastforce)
    apply (erule  meta_impE[OF _ refl])
    apply (erule (1) meta_impE)
    apply (erule (2) meta_impE)
   apply clarsimp
   apply (drule rtranclp_conjD[THEN conjunct1])
   apply (drule oghoare_Await)
   apply clarsimp
   apply (rename_tac b c c' x Q A  r P'' Q' A')
  apply (drule (1) oghoare_atom_com_sound)
  apply (simp add: valid_def)
  apply (drule_tac x="Normal x" in spec)
  apply (drule_tac x=Stuck in spec)
  apply (drule_tac x=Skip in spec)
  apply clarsimp
  apply (erule impE)
   apply (cut_tac c=c' in  steps_Stuck[where Γ=Γ])
   apply fastforce
   apply (fastforce simp: final_def steps_Fault)
  apply clarsimp
  apply (drule oghoare_Await)
  apply clarsimp
 done

lemma oghoare_steps_Fault[rule_format, OF _ refl refl]:
 "Γ cf * cf' 
   cf = (c, Normal x) 
   cf' = (c', Fault f) 
   x  pre P 
   Γ,Θ⊢⇘/FP c Q,A  f  F"
  apply (induct arbitrary: x c c' f rule: rtranclp_induct)
   supply [[simproc del: defined_all]]
   apply fastforce
  apply clarsimp
  apply (rename_tac b x c c' f)
  apply (case_tac b)
    apply clarsimp
    apply (drule (2) oghoare_steps)
    apply clarsimp
    apply (drule (3) oghoare_step_Fault)
   apply clarsimp
   apply (drule meta_spec)+
   apply (erule meta_impE, (rule conjI, (rule refl)+))+
    apply simp
   apply (drule step_Fault_prop ; simp)
   apply simp
  apply clarsimp
  apply (drule step_Stuck_prop ; simp)
 done

lemma oghoare_steps_Stuck[rule_format, OF _ refl refl]:
 "Γ cf * cf' 
   cf = (c, Normal x) 
   cf' = (c', Stuck) 
   x  pre P 
   Γ,Θ⊢⇘/FP c Q,A  P'"
  apply (induct arbitrary: x c c' rule: rtranclp_induct)
   apply fastforce
  apply clarsimp
  apply (rename_tac b x c c')
  apply (case_tac b)
    apply clarsimp
    apply (drule (2) oghoare_steps)
    apply clarsimp
    apply (drule (3) oghoare_step_Stuck)
   apply clarsimp
   apply (drule step_Fault_prop ; simp)
   apply simp
 done

lemma oghoare_sound_Parallel_Fault_case[rule_format, OF _ refl refl]:
 "Γ  (c, s) * (c', t) 
   P x f cs. c = Parallel cs   s = Normal x 
      x  pre P  t = Fault f 
      Γ,Θ⊢⇘/FP c Q,A  final (c', t) 
      f  F"
  apply(erule converse_rtranclp_induct2)
   apply (clarsimp simp: final_def)
  apply clarsimp

  apply (rename_tac c s P x f cs)
  apply (case_tac s)
    apply clarsimp

    apply(erule step.cases, simp_all)
         apply (clarsimp simp: final_def)
         apply (drule oghoare_Parallel)
         apply clarsimp
         apply (rename_tac x f s' i cs c1' as)
         apply (subgoal_tac "Γ (Parallel cs, Normal x)  (Parallel (cs[i := c1']), Normal s')")
         apply (frule_tac c="Parallel cs" and a="AnnPar as"  and
                      Q="(xset as. postcond x)" and A="(xset as. abrcond x)" 
                      in oghoare_step[where Θ=Θ and F=F])
          apply(rule Parallel)
               apply simp
              apply clarsimp
              apply (rule Conseq, rule exI[where x="{}"], fastforce)
             apply assumption
            apply clarsimp
           apply clarsimp
          apply simp
         apply clarsimp
        apply (rename_tac a')
        apply (drule_tac x=a' in spec)
        apply clarsimp
        apply (erule notE[where P="oghoare _ _ _ _ _ _ _"])
        apply (rule Conseq, rule exI[where x="{}"])
        apply (clarsimp)
        apply (rule_tac x="(xset as. postcond x)" in exI)
        apply (rule_tac x="(xset as. abrcond x)" in exI ; simp)
       apply(erule (1) step.Parallel)
      apply clarsimp
      apply (fastforce dest: no_steps_final simp: final_def)+
   apply (clarsimp simp: final_def)
   apply (drule oghoare_Parallel)
   apply (erule step_Normal_elim_cases, simp_all)
    apply clarsimp
    apply (rename_tac f cs f' i c1' as)
   apply (drule_tac x="i" in spec)
   apply (erule  impE, fastforce)
   apply clarsimp
   apply (drule_tac x="as!i" in bspec)
    apply (clarsimp simp: in_set_conv_nth)
    apply (rule_tac x="i" in exI, fastforce)
   apply (drule_tac P="pres (as ! i)" in  oghoare_step_Fault[where Θ=Θ and F=F])
     apply assumption+
   apply (drule steps_Fault_prop ; simp)
   apply simp
  apply (drule steps_Stuck_prop ;simp)
 done

lemma oghoare_soundness:
  "(Γ, Θ ⊢⇘/FP c Q,A  Γ ⊨⇘/F(pre P) c Q, A) 
   (Γ, Θ ⊩⇘/FP' P c Q,A  Γ ⊨⇘/FP' c Q, A)"
  unfolding valid_def
  proof (induct rule: oghoare_oghoare_seq.induct)
    case SeqSkip thus ?case 
      by (fastforce 
            elim: converse_rtranclpE step_Normal_elim_cases(1))
  next
    case SeqThrow thus ?case
    by (fastforce 
            elim: converse_rtranclpE step_Normal_elim_cases)
  next 
    case SeqBasic thus ?case 
      by (fastforce 
            elim: converse_rtranclpE step_Normal_elim_cases 
            simp: final_def)
  next 
    case (SeqSpec Γ Θ F r Q A) thus ?case
    apply clarsimp
    apply (erule converse_rtranclpE) 
     apply (clarsimp simp: final_def)
    apply (erule step_Normal_elim_cases)
     apply (fastforce elim!: converse_rtranclpE step_Normal_elim_cases)
    by clarsimp
  next
    case (SeqSeq Γ Θ F P1 c1 P2 A c2 Q) show ?case
     using SeqSeq
     by (fold valid_def) 
        (fastforce intro: oghoare_seq_valid simp: valid_weaken_pre)
  next 
    case (SeqCatch Γ Θ F P1 c1 Q P2 c2 A) thus ?case
    by (fold valid_def)
       (fastforce elim:  oghoare_catch_valid)+
  next 
    case (SeqCond Γ Θ F P b c1 Q A c2) thus ?case
     by (fold valid_def)
        (fastforce intro:oghoare_if_valid)
  next 
    case (SeqWhile Γ Θ F P c A b) thus ?case
     by (fold valid_def)
        (fastforce elim: valid_weaken_pre[rotated] oghoare_while_valid)
  next
    case (SeqGuard Γ Θ F P c Q A r g f) thus ?case
    apply (fold valid_def)
    apply (simp (no_asm) add: valid_def)
    apply clarsimp
    apply (erule converse_rtranclpE)
     apply (fastforce simp: final_def)
    apply clarsimp
    apply (erule step_Normal_elim_cases)
     apply (case_tac "r  - g  {}")
      apply clarsimp
      apply (fastforce simp: valid_def)
     apply clarsimp
     apply (fastforce simp: valid_def)
    apply clarsimp
     apply (case_tac "r  - g  {}")
      apply (fastforce dest: no_steps_final simp:final_def)
     apply (fastforce dest: no_steps_final simp:final_def)
   done
  next
    case (SeqCall Γ p f Θ F P Q A) thus ?case
    apply clarsimp
    apply (erule converse_rtranclpE)
     apply (clarsimp simp add: final_def)
    apply (erule step_Normal_elim_cases)
     apply (clarsimp simp: final_def)
     apply fastforce
    apply fastforce
   done
  next
    case (SeqDynCom r P fa Γ Θ F c Q A) thus ?case
    apply -
    apply clarsimp
    apply (erule converse_rtranclpE)
     apply (clarsimp simp: final_def)
    apply clarsimp
    apply (erule step_Normal_elim_cases)
    apply clarsimp
    apply (rename_tac t c' x)
    apply (drule_tac x=x in bspec, fastforce)
    apply clarsimp
    apply (drule_tac x="Normal x" in spec)
    apply (drule_tac x="t" in spec)
    apply (drule_tac x="c'" in spec)
    apply fastforce+
   done
   next 
    case (SeqConseq Γ Θ F P c Q A) thus ?case 
     apply (clarsimp)
     apply (rename_tac t c' x)
     apply (erule_tac x="Normal x" in allE)
     apply (erule_tac x="t" in allE)
     apply (erule_tac x="c'" in allE)
     apply (clarsimp simp: pre_weaken_pre)
     apply force
    done
  next
    case (SeqParallel as P Γ Θ F cs Q A) thus ?case
    by (fold valid_def)
       (erule (1) valid_weaken_pre)
  next
    case (Call Θ p as n P Q A r Γ f F) thus ?case
    apply clarsimp
    apply (erule converse_rtranclpE)
     apply (clarsimp simp add: final_def)
    apply (erule step_Normal_elim_cases)
    apply (clarsimp simp: final_def)
     apply (erule disjE)
     apply clarsimp
      apply fastforce
     apply fastforce
    apply fastforce
   done
   next 
    case (Await Γ Θ F P c Q A r b) thus ?case
    apply clarsimp
    apply (erule converse_rtranclpE)
     apply (clarsimp simp add: final_def)
    apply (erule step_Normal_elim_cases)
       apply (erule converse_rtranclpE)
        apply (fastforce simp add: final_def )
       apply (force dest!:no_step_final simp: final_def)
      apply clarsimp
      apply (rename_tac x c'')
      apply (drule_tac x="Normal x" in spec)
      apply (drule_tac x="Stuck" in spec)
      apply (drule_tac x="Skip" in spec)
      apply (clarsimp simp: final_def)
      apply (erule impE[where P="rtranclp _ _ _"])
       apply (cut_tac c="c''" in  steps_Stuck[where Γ=Γ])
       apply fastforce
      apply fastforce
     apply clarsimp
     apply (rename_tac x c'' f)
     apply (drule_tac x="Normal x" in spec)
     apply (drule_tac x="Fault f" in spec)
     apply (drule_tac x="Skip" in spec)
     apply (erule impE[where P="rtranclp _ _ _"])
      apply (cut_tac c="c''" and f=f in  steps_Fault[where Γ=Γ])
      apply fastforce
     apply clarsimp
     apply (erule converse_rtranclpE)
       apply fastforce
     apply (erule step_elim_cases)
    apply (fastforce)
   done
   next 
    case (Parallel as cs Γ Θ F Q A ) thus ?case
    apply (fold valid_def)
    apply (simp only:pre.simps)
    apply (simp (no_asm) only: valid_def)
    apply clarsimp
    apply (rename_tac t c' x')
    apply (case_tac t)
      apply clarsimp
      apply (drule oghoare_sound_Parallel_Normal_case[where Θ=Θ and Q=Q and A=A and F=F and P="AnnPar as", OF _ refl])
          apply (rule oghoare_oghoare_seq.Parallel)
              apply simp
             apply clarsimp
            apply assumption
           apply (clarsimp)
          apply clarsimp
         apply (clarsimp simp: final_def)
        apply (clarsimp )
       apply clarsimp
      apply clarsimp
     apply (drule oghoare_sound_Parallel_Fault_case[where Θ=Θ and Q=Q and A=A and F=F and P="AnnPar as", OF _ ])
         apply clarsimp
        apply assumption
        apply (rule oghoare_oghoare_seq.Parallel)
            apply simp
           apply clarsimp
          apply assumption
         apply clarsimp
        apply clarsimp
       apply (simp add: final_def)
      apply (fastforce simp add: final_def)
     apply (clarsimp simp: final_def)
     apply (erule  oghoare_steps_Stuck[where Θ=Θ and F=F and Q=Q and A=A and P="AnnPar as"])
      apply simp
     apply (rule  oghoare_oghoare_seq.Parallel)
         apply simp
        apply simp
       apply simp
      apply clarsimp
     apply clarsimp
    done
  next
    case Skip thus ?case
      by (fastforce 
            elim: converse_rtranclpE step_Normal_elim_cases(1))
  next 
    case Basic thus ?case 
      by (fastforce 
            elim: converse_rtranclpE step_Normal_elim_cases 
            simp: final_def)
  next 
    case (Spec Γ Θ F r Q A) thus ?case
    apply clarsimp
    apply (erule converse_rtranclpE) 
     apply (clarsimp simp: final_def)
    apply (erule step_Normal_elim_cases)
     apply (fastforce elim!: converse_rtranclpE step_Normal_elim_cases)
    by clarsimp
  next
    case (Seq Γ Θ F P1 c1 P2 A c2 Q) show ?case
     using Seq
     by (fold valid_def) 
        (fastforce intro: oghoare_seq_valid simp: valid_weaken_pre)
   next 
    case (Cond Γ Θ F P1 c1 Q A P2 c2 r b) thus ?case
     by (fold valid_def)
        (fastforce intro:oghoare_if_valid)
   next 
    case (While Γ Θ F P c i A b Q r) thus ?case
     by (fold valid_def)
        (fastforce elim: valid_weaken_pre[rotated] oghoare_while_valid)
   next 
    case Throw thus ?case
    by (fastforce 
            elim: converse_rtranclpE step_Normal_elim_cases)
   next 
    case (Catch Γ Θ F P1 c1 Q P2 c2 A) thus ?case
    apply (fold valid_def)
    apply (fastforce elim: oghoare_catch_valid)+
    done
   next 
    case (Guard Γ Θ F P c Q A r g f) thus ?case
    apply (fold valid_def)
    apply (simp)
    apply (frule (1) valid_weaken_pre[rotated])
    apply (simp (no_asm) add: valid_def)
    apply clarsimp
    apply (erule converse_rtranclpE)
     apply (fastforce simp: final_def)
    apply clarsimp
    apply (erule step_Normal_elim_cases)
     apply (case_tac "r  - g  {}")
      apply clarsimp
      apply (fastforce simp: valid_def)
     apply clarsimp
     apply (fastforce simp: valid_def)
    apply clarsimp
     apply (case_tac "r  - g  {}")
      apply clarsimp
      apply (fastforce dest: no_steps_final simp:final_def)
     apply (clarsimp simp: ex_in_conv[symmetric])
    done
   next 
    case (DynCom r Γ Θ F P c Q A) thus ?case
   
    apply clarsimp
    apply (erule converse_rtranclpE)
     apply (clarsimp simp: final_def)
    apply clarsimp
    apply (erule step_Normal_elim_cases)
    apply clarsimp
    apply (rename_tac t c' x)
    apply (erule_tac x=x in ballE)
    apply clarsimp
    apply (drule_tac x="Normal x" in spec)
    apply (drule_tac x="t" in spec)
    apply (drule_tac x="c'" in spec)
    
    apply fastforce+
   done
   next 
    case (Conseq Γ Θ F P c Q A) thus ?case 
     apply (clarsimp)
     apply (rename_tac P' Q' A' t c' x)
     apply (erule_tac x="Normal x" in allE)
     apply (erule_tac x="t" in allE)
     apply (erule_tac x="c'" in allE)
     apply (clarsimp simp: pre_weaken_pre)
     apply force
    done   
qed

lemmas oghoare_sound = oghoare_soundness[THEN conjunct1, rule_format]
lemmas oghoare_seq_sound = oghoare_soundness[THEN conjunct2, rule_format]

end