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]: 
"Γ, Θ ⊢⇘/F⇙ P 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]: 
"Γ, Θ ⊢⇘/F⇙ P 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]: 
"Γ, Θ ⊢⇘/F⇙ P 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]: 
"Γ, Θ ⊢⇘/F⇙ P 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]: 
"Γ, Θ ⊢⇘/F⇙ P c Q,A ⟹ c = (DynCom c') ⟶ 
 (∃r ad. P = (AnnRec r ad) ∧ r ⊆ pre ad ∧ (∀s∈r. Γ, Θ ⊢⇘/F⇙ ad (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]: 
"Γ,Θ⊢⇘/F⇙ P c Q,A ⟹ c = Guard f g d ⟶ 
 (∃P' r . P = AnnRec r P' ∧ 
   Γ,Θ⊢⇘/F⇙ P' 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]: 
"Γ, Θ⊢⇘/F⇙ P 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]: 
"Γ, Θ ⊢⇘/F⇙ P x Q,A ⟹ ∀p1 p2. x = Seq p1 p2 ⟶
 (∃ P⇩1 P⇩2 P' Q' A'. P = AnnComp P⇩1 P⇩2 ∧ Γ, Θ ⊢⇘/F⇙ P⇩1 p1 P', A' ∧ P' ⊆ pre P⇩2 ∧
         Γ, Θ ⊢⇘/F⇙ P⇩2 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]: 
"Γ, Θ ⊢⇘/F⇙ P x Q,A ⟹ ∀p1 p2. x = Catch p1 p2 ⟶
 (∃ P⇩1 P⇩2 P' Q' A'. P = AnnComp P⇩1 P⇩2 ∧ Γ, Θ ⊢⇘/F⇙ P⇩1 p1 Q', P' ∧ P' ⊆ pre P⇩2 ∧
         Γ, Θ ⊢⇘/F⇙ P⇩2 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]: 
 "Γ, Θ ⊢⇘/F⇙ P x Q,A ⟹
∀c⇩1 c⇩2 b. x = (Cond b c⇩1 c⇩2) ⟶
(∃P' P⇩1 P⇩2 Q' A'. P = (AnnBin P' P⇩1 P⇩2) ∧
  P' ⊆ {s. (s∈b ⟶ s∈pre P⇩1) ∧ (s∉b ⟶ s∈pre P⇩2)} ∧
    Γ, Θ ⊢⇘/F⇙ P⇩1 c⇩1 Q',A' ∧
    Γ, Θ ⊢⇘/F⇙ P⇩2 c⇩2 Q',A' ∧ Q' ⊆ Q ∧ A' ⊆ A)"
  apply (induct rule: oghoare_induct, simp_all)
   apply (rule conjI)
    apply fastforce
   apply (rename_tac  Q A P⇩2 c⇩2 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]:
  "Γ, Θ ⊢⇘/F⇙ P x Q,A ⟹
    ∀ b c. x = While b c ⟶
    (∃ r i P' A' Q'. P = AnnWhile r i P' ∧
     Γ, Θ⊢⇘/F⇙ P' 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:
 "Γ,Θ⊢⇘/F⇙ P 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 ∧
 Γ,Θ ⊢⇘/F⇙ P' 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]: 
"Γ, Θ⊢⇘/F⇙ P 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:
 " Γ,Θ⊩⇘/F⇙ P 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:
 " Γ,Θ⊢⇘/F⇙ a 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. (s∈b ⟶ s∈pre P⇩1) ∧ (s∉b ⟶ s∈pre P⇩2)};
    Γ, Θ ⊢⇘/F⇙ P⇩1 c⇩1 Q,A; 
    Γ, Θ ⊢⇘/F⇙ P⇩2 c⇩2 Q,A  ⟧ 
  ⟹ Γ, Θ ⊢⇘/F⇙ (AnnBin P P⇩1 P⇩2) (Cond b c⇩1 c⇩2) Q,A"
  by (auto intro: Cond)

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

lemma AwaitRule:
 "⟦atom_com c ; Γ, Θ ⊩⇘/F⇙P 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:
 " Γ⊨⇘/F⇙ P c⇩1 R,A ⟹
   Γ⊨⇘/F⇙ R c⇩2 Q,A ⟹
   Γ⊨⇘/F⇙ P Seq c⇩1 c⇩2 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:
 "Γ⊨⇘/F⇙ P⇩1 c⇩1 Q,A ⟹
  Γ⊨⇘/F⇙ P⇩2 c⇩2 Q,A ⟹
  r ∩ b ⊆ P⇩1 ⟹ r ∩ - b ⊆ P⇩2 ⟹
  Γ⊨⇘/F⇙ r Cond b c⇩1 c⇩2 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=c⇩1])
  apply (fastforce simp: valid_def[where c=c⇩2])
 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 .
       Γ⊨⇘/F⇙ P 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:
 "Γ⊨⇘/F⇙ P c Q,A ⟹
  P' ⊆ P ⟹ Γ⊨⇘/F⇙ P' c Q,A"
 by (fastforce simp: valid_def)

lemma valid_strengthen_post:
 "Γ⊨⇘/F⇙ P c Q,A ⟹
  Q ⊆ Q' ⟹ Γ⊨⇘/F⇙ P c Q',A"
 by (fastforce simp: valid_def)

lemma valid_strengthen_abr:
 "Γ⊨⇘/F⇙ P c Q,A ⟹
  A ⊆ A' ⟹ Γ⊨⇘/F⇙ P c Q,A'"
 by (fastforce simp: valid_def)

lemma oghoare_while_valid:
 "Γ⊨⇘/F⇙ P c i,A ⟹
  i ∩ b ⊆ P ⟹
  i ∩ - b ⊆ Q ⟹
  Γ⊨⇘/F⇙ i 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:
 "Γ⊨⇘/F⇙ P⇩1 c⇩1 Q,P⇩2 ⟹
  Γ⊨⇘/F⇙ P⇩2 c⇩2 Q,A ⟹
    Γ⊨⇘/F⇙ P⇩1 Catch c⇩1 c⇩2 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="c⇩1"])
     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="c⇩1"])
    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=c⇩1] 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=c⇩1] 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:
  "Γ, Θ ⊩⇘/F⇙P a c Q,A ⟹ atom_com c ⟹ Γ ⊨⇘/F⇙ P 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 P⇩1 c⇩1 P⇩2 A c⇩2 Q) show ?case
     using SeqSeq
     by (fold valid_def) 
        (fastforce intro: oghoare_seq_valid simp: valid_weaken_pre)
   next 
    case (SeqCatch Γ Θ F P⇩1 c⇩1 Q P⇩2 c⇩2 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) ⟹
  Γ,Θ⊢⇘/F ⇙a c Q,A ⟹
 s ∈ pre a ⟹
∃a'. Γ,Θ⊢⇘/F ⇙a' 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="(⋃x∈set 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 "Γ,Θ ⊢⇘/F ⇙a' 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 "∀a∈set 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 "∀a∈set 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 c⇩1 s c⇩1' s' c⇩2 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' P⇩2" 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 c⇩2 s c c' sa a t Q A) thus ?case
   apply clarsimp
   apply (drule oghoare_Seq)
    apply clarsimp
    apply (rename_tac P⇩1 P⇩2 P' Q' A')
    apply (rule_tac x=P⇩2 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 c⇩2 s c c' sa a t Q A) thus ?case
   apply clarsimp
   apply (drule oghoare_Seq)
   apply clarsimp
   apply (rename_tac P⇩1 P⇩2 P' Q' A')
   apply (rule_tac x=P⇩1 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 c⇩1 c⇩2 c sa c' s' ann) thus ?case
   apply (clarsimp)
   apply (drule oghoare_Cond)
   apply clarsimp
   apply (rename_tac P' P⇩1 P⇩2 Q' A')
   apply (rule_tac x= P⇩1 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 c⇩1 c⇩2 c sa c' s' ann) thus ?case
   apply (clarsimp)
   apply (drule oghoare_Cond)
   apply clarsimp
   apply (rename_tac P' P⇩1 P⇩2 Q' A')
   apply (rule_tac x= P⇩2 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 c⇩1 s c⇩1' s' c⇩2 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 P⇩1 P⇩2 P' Q' A' a')
    apply (rule_tac x="AnnComp a' P⇩2" 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 c⇩2 s c c' sa a t Q A) thus ?case
   apply clarsimp
   apply (drule oghoare_Catch, clarsimp)
   apply (rename_tac P⇩1 P⇩2 P' Q' A')
   apply (rule_tac x=P⇩1 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 c⇩2 s c c' sa a t Q A) thus ?case
  apply clarsimp
  apply (drule oghoare_Catch, clarsimp)
  apply (rename_tac P⇩1 P⇩2 P' Q' A')
  apply (rule_tac x=P⇩2 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 (⋂x∈set 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="(⋃x∈set 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) ⟹
  Γ,Θ⊢⇘/F ⇙a c Q,A ⟹
 s ∈ pre a ⟹
∃a'. Γ,Θ⊢⇘/F ⇙a' 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 ⟶
      Γ,Θ⊢⇘/F ⇙P 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="(⋂x∈set as. postcond x)" and A ="(⋃x∈set 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="(⋂x∈set as. postcond x)" in exI)
      apply (rule_tac x="(⋃x∈set 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="(⋃x∈set 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 ⟹
   Γ,Θ⊢⇘/F ⇙P 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 ⟹
   Γ,Θ⊢⇘/F ⇙P 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 ⟹
   Γ,Θ⊢⇘/F ⇙P 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 ⟹
   Γ,Θ⊢⇘/F ⇙P 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 ⟶
      Γ,Θ⊢⇘/F ⇙P 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="(⋂x∈set as. postcond x)" and A="(⋃x∈set 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="(⋂x∈set as. postcond x)" in exI)
        apply (rule_tac x="(⋃x∈set 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:
  "(Γ, Θ ⊢⇘/F⇙ P c Q,A ⟶ Γ ⊨⇘/F⇙ (pre P) c Q, A) ∧
   (Γ, Θ ⊩⇘/F⇙P' P c Q,A ⟶ Γ ⊨⇘/F⇙ P' 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 P⇩1 c⇩1 P⇩2 A c⇩2 Q) show ?case
     using SeqSeq
     by (fold valid_def) 
        (fastforce intro: oghoare_seq_valid simp: valid_weaken_pre)
  next 
    case (SeqCatch Γ Θ F P⇩1 c⇩1 Q P⇩2 c⇩2 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 P⇩1 c⇩1 P⇩2 A c⇩2 Q) show ?case
     using Seq
     by (fold valid_def) 
        (fastforce intro: oghoare_seq_valid simp: valid_weaken_pre)
   next 
    case (Cond Γ Θ F P⇩1 c⇩1 Q A P⇩2 c⇩2 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 P⇩1 c⇩1 Q P⇩2 c⇩2 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