Quelle  SeqCatch_decomp.thy

(*
 * 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)
 *)
text ‹Helper lemmas for sequential reasoning about Seq and Catch›
theory SeqCatch_decomp 
imports SmallStep
begin

lemma redex_size[rule_format] :
"∀r. redex c = r ⟶ size r ≤ size c"
  by(induct_tac c, simp_all)

lemma Normal_pre[rule_format, OF _ refl] :
"Γ ⊨ (p, s) → (p', s') ==>
 ∀u. s' = Normal u ⟶ (∃v. s = Normal v)"
  by(erule step_induct, simp_all)


lemma Normal_pre_star[rule_format, OF _ refl] :
"Γ ⊨ cfg₁ →^* cfg₂ ==> ∀p' t. cfg₂ = (p', Normal t) ⟶
 (∃p s. cfg₁ = (p, Normal s))"
  apply(erule converse_rtranclp_induct)
   apply simp
  apply clarsimp
  apply(drule Normal_pre)
  by force



lemma Seq_decomp_Skip[rule_format, OF _ refl] :
"Γ ⊨ (p, s) → (p', s') ==>
 ∀p₂. p = Seq Skip p₂ ⟶ s' = s ∧ p' = p₂"
  apply(erule step_induct, simp_all)
    apply clarsimp
    apply(erule step.cases, simp_all)
   apply clarsimp+
 done

lemma Seq_decomp_Throw[rule_format, OF _ refl, OF _ refl] :
"Γ ⊨ (p, s) → (p', s') ==>
 ∀p₂ z. s = Normal z ⟶ p = Seq Throw p₂ ⟶ s' = s ∧ p' = Throw"
  apply(erule step_induct, simp_all)
  apply clarsimp
  apply(erule step.cases, simp_all)
 done

lemma Throw_star[rule_format, OF _ refl] :
"Γ ⊨ cfg₁ →^* cfg₂ ==> ∀s. cfg₁ = (Throw, Normal s) ⟶
  cfg₂ = cfg₁"
  apply(erule converse_rtranclp_induct)
   apply simp
  apply clarsimp
  apply(erule step.cases, simp_all)
 done

lemma Seq_decomp[rule_format, OF _ refl] :
"Γ ⊨ (p, s) → (p', s') ==>
 ∀p₁ p₂. p = Seq p₁ p₂ ⟶ p₁ ≠ Skip ⟶ p₁ ≠ Throw ⟶
  (∃p₁'. Γ ⊨ (p₁, s) → (p₁', s') ∧ p' = Seq p₁' p₂)"
  apply(erule step_induct, simp_all)
   apply clarsimp
   apply(drule redex_size)
   apply simp
  apply clarsimp
  apply(drule redex_size)
  apply simp
 done

lemma Seq_decomp_relpow:
"Γ ⊨ (Seq p₁ p₂, Normal s) →ⁿⁿ (p', Normal s') ==>
 final (p', Normal s') ==>
 (∃n1<n. Γ ⊨ (p₁, Normal s) →ⁿⁿ¹ (Throw, Normal s')) ∧ p'=Throw ∨
 (∃t n1 n2. Γ ⊨ (p₁, Normal s) →ⁿⁿ¹ (Skip, Normal t) ∧ n1 < n ∧ n2 < n ∧ Γ ⊨ (p₂, Normal t) →ⁿⁿ² (p', Normal s'))"
  apply (induct n arbitrary: p₁ p₂ s p' s')
   apply (clarsimp simp: final_def)
  apply (simp only: relpowp.simps)
  apply (subst (asm) relpowp_commute[symmetric])
  apply clarsimp
  apply (rename_tac n p₁ p₂ s p' s' a b)
  apply(case_tac "p₁ = Skip")
   apply clarsimp
   apply(drule Seq_decomp_Skip)
   apply clarsimp
   apply(drule_tac x=s in spec)
   apply(drule_tac x=0 in spec)
   apply simp
  apply (rename_tac n p₁ p₂ s p' s' a b)
  apply(case_tac "p₁ = Throw")
   apply clarsimp
   apply(drule Seq_decomp_Throw)
   apply clarsimp
   apply(frule relpowp_imp_rtranclp)
   apply(drule Throw_star)
   apply clarsimp
   apply(rule_tac x=n in exI, simp)
  apply(drule Seq_decomp)
    apply assumption+
  apply (rename_tac n p₁ p₂ s p' s' a b)
  apply clarsimp
  apply(frule relpowp_imp_rtranclp)
  apply(drule Normal_pre_star) 
  apply clarsimp
  apply(drule meta_spec, drule meta_spec, drule meta_spec, drule meta_spec, drule meta_spec, drule meta_mp, assumption)
  apply(drule meta_mp, assumption)
  apply(erule disjE, clarsimp)
   apply (rename_tac n1)
   apply(rule_tac x="Suc n1" in exI, simp)
   apply (subst relpowp_commute[symmetric])
   apply(rule_tac relcomppI, assumption+)
  apply clarsimp
  apply (rename_tac t n1 n2)
  apply(drule_tac x=t in spec)
  apply(drule_tac x="Suc n1" in spec)
  apply simp
  apply(drule mp)
  apply (subst relpowp_commute[symmetric])
  apply(rule_tac relcomppI, assumption+)
  apply simp
 done

lemma Seq_decomp_star:
"Γ ⊨ (Seq p₁ p₂, Normal s) →^* (p', Normal s') ==> final (p', Normal s') ==>
 Γ ⊨ (p₁, Normal s) →^* (Throw, Normal s') ∧ p'=Throw ∨
 (∃t. Γ ⊨ (p₁, Normal s) →^* (Skip, Normal t) ∧ Γ ⊨ (p₂, Normal t) →^* (p', Normal s'))"
  apply (drule rtranclp_imp_relpowp)
  apply clarsimp
  apply (drule (1) Seq_decomp_relpow)
  apply (erule disjE)
   apply clarsimp
   apply (drule (1) relpowp_imp_rtranclp)
  apply clarsimp
  apply (drule  relpowp_imp_rtranclp)+
  apply clarsimp
 done

lemma Seq_decomp_relpowp_Fault:
"Γ ⊨ (Seq p₁ p₂, Normal s) →ⁿⁿ (Skip, Fault f) ==>
 (∃n1. Γ ⊨ (p₁, Normal s) →ⁿⁿ¹ (Skip, Fault f)) ∨
 (∃t n1 n2. Γ ⊨ (p₁, Normal s) →ⁿⁿ¹ (Skip, Normal t) ∧ n1 < n ∧ n2 < n ∧ Γ ⊨ (p₂, Normal t) →ⁿⁿ² (Skip, Fault f))"
  apply (induct n arbitrary: s p₁)
   apply (clarsimp simp: final_def)
  apply (simp only: relpowp.simps)
  apply (subst (asm) relpowp_commute[symmetric])
  apply clarsimp
  apply (rename_tac n s p₁ a b)
  apply (case_tac "p₁ = Skip")
   apply simp
   apply (drule Seq_decomp_Skip)
   apply clarify
   apply (drule_tac x=s in spec)
   apply (drule spec[where x=0])
   apply simp
  apply (case_tac "p₁ = Throw")
   apply simp
   apply (drule Seq_decomp_Throw)
   apply fastforce
  apply (frule Seq_decomp )
    apply simp+
  apply clarsimp
  apply (rename_tac s p1 t p1')  
  apply (case_tac "∃v. Normal v = t")
   apply clarsimp
   apply (rename_tac v)
   apply (drule_tac x=v in meta_spec)
   apply (drule_tac x=p1' in meta_spec)
   apply clarsimp
   apply (erule disjE)
    apply clarsimp
    apply (rename_tac n1)
    apply (rule_tac x="n1+1" in exI)
    apply (drule (1) relpowp_Suc_I2, fastforce)
   apply clarsimp
   apply (rename_tac t n1 n2)
   apply (drule_tac x=t in spec)
   apply (drule_tac x="n1+1" in spec)
   apply simp
   apply (subst (asm) relpowp_commute[symmetric])
   apply (drule mp)
   apply (erule relcomppI, assumption)
   apply clarsimp
  apply (case_tac "t = Stuck")
   apply clarsimp
   apply (drule relpowp_imp_rtranclp)
   apply (fastforce dest: steps_Stuck_prop)
  apply (case_tac t, simp_all)
  apply (rename_tac f')
  apply (frule steps_Fault_prop[where s'="Fault f", OF relpowp_imp_rtranclp, THEN sym], rule refl)
  apply clarify
  apply (cut_tac c=p1' in steps_Fault[where Γ=Γ and f=f])
  apply (drule rtranclp_imp_relpowp)
  apply clarsimp
  apply (rename_tac n')
  apply (rule_tac x="n'+1" in exI)
  apply simp
  apply (subst relpowp_commute[symmetric])
  apply (erule relcomppI, assumption)
 done

lemma Seq_decomp_star_Fault[rule_format, OF _ refl, OF _ refl, OF _ refl] :
"Γ ⊨ cfg₁ →^* cfg₂ ==> ∀p s p' f. cfg₁ = (p, Normal s) ⟶ cfg₂ = (Skip, Fault f) ⟶
 (∀p₁ p₂. p = Seq p₁ p₂ ⟶
 (Γ ⊨ (p₁, Normal s) →^* (Skip, Fault f))
 ∨ (∃s'. (Γ ⊨ (p₁, Normal s) →^* (Skip, Normal s')) ∧ Γ ⊨ (p₂, Normal s') →^* (Skip, Fault f)))"
  apply(erule converse_rtranclp_induct)
   apply clarsimp
  apply clarsimp
  apply (rename_tac c s' s f p₁ p₂)
  apply (case_tac "p₁ = Skip")
   apply simp
   apply (drule Seq_decomp_Skip)
   apply simp
  apply (case_tac "p₁ = Throw")
   apply simp
   apply (drule Seq_decomp_Throw)
   apply simp
  apply (drule Seq_decomp)
    apply simp+
  apply clarsimp
  apply (case_tac s')
    apply simp
    apply (erule disjE)
     apply (erule (1) converse_rtranclp_into_rtranclp)
    apply clarsimp
    apply (rename_tac s')
    apply (erule_tac x="s'" in allE)
    apply (drule (1) converse_rtranclp_into_rtranclp, fastforce)
   apply simp
   apply (frule steps_Fault_prop[THEN sym], rule refl)
   apply simp
   apply (cut_tac c=p₁' and f=f in steps_Fault[where Γ=Γ])
   apply (drule (2)  converse_rtranclp_into_rtranclp)
  apply clarsimp
  apply (frule steps_Stuck_prop[THEN sym], rule refl)
  apply simp
 done


lemma Seq_decomp_relpowp_Stuck:
"Γ ⊨ (Seq p₁ p₂, Normal s) →ⁿⁿ (Skip, Stuck) ==>
 (∃n1. Γ ⊨ (p₁, Normal s) →ⁿⁿ¹ (Skip, Stuck)) ∨
 (∃t n1 n2. Γ ⊨ (p₁, Normal s) →ⁿⁿ¹ (Skip, Normal t) ∧ n1 < n ∧ n2 < n ∧ Γ ⊨ (p₂, Normal t) →ⁿⁿ² (Skip, Stuck))"
  apply (induct n arbitrary: s p₁)
   apply (clarsimp simp: final_def)
  apply (simp only: relpowp.simps)
  apply (subst (asm) relpowp_commute[symmetric])
  apply clarsimp
  apply (rename_tac n s p₁ a b)
  apply (case_tac "p₁ = Skip")
   apply simp
   apply (drule Seq_decomp_Skip)
   apply clarify
   apply (drule_tac x=s in spec)
   apply (drule spec[where x=0])
   apply simp
  apply (case_tac "p₁ = Throw")
   apply simp
   apply (drule Seq_decomp_Throw)
   apply fastforce
  apply (frule Seq_decomp )
    apply simp+
  apply clarsimp
  apply (rename_tac s p1 t p1')  
  apply (case_tac "∃v. Normal v = t")
   apply clarsimp
   apply (rename_tac v)
   apply (drule_tac x=v in meta_spec)
   apply (drule_tac x=p1' in meta_spec)
   apply clarsimp
   apply (erule disjE)
    apply clarsimp
    apply (rename_tac n1)
    apply (rule_tac x="n1+1" in exI)
    apply (drule (1) relpowp_Suc_I2, fastforce)
   apply clarsimp
   apply (rename_tac t n1 n2)
   apply (drule_tac x=t in spec)
   apply (drule_tac x="n1+1" in spec)
   apply simp
   apply (subst (asm) relpowp_commute[symmetric])
   apply (drule mp)
   apply (erule relcomppI, assumption)
   apply clarsimp
  apply (case_tac "∃v. t = Fault v")
   apply clarsimp
   apply (drule relpowp_imp_rtranclp)
   apply (fastforce dest: steps_Fault_prop)
  apply (case_tac t, simp_all)
  apply (rename_tac p1')
  apply clarify
  apply (cut_tac c=p1' in steps_Stuck[where Γ=Γ])
  apply (drule rtranclp_imp_relpowp)
  apply clarsimp
  apply (rename_tac n')
  apply (rule_tac x="n'+1" in exI)
  apply simp
  apply (subst relpowp_commute[symmetric])
  apply (erule relcomppI, assumption)
 done

lemma Seq_decomp_star_Stuck[rule_format, OF _ refl, OF _ refl] :
"Γ ⊨ cfg₁ →^* (Skip, Stuck) ==> ∀p s p'. cfg₁ = (p, Normal s) ⟶
 (∀p₁ p₂. p = Seq p₁ p₂ ⟶
 (Γ ⊨ (p₁, Normal s) →^* (Skip, Stuck))
 ∨ (∃s'. (Γ ⊨ (p₁, Normal s) →^* (Skip, Normal s')) ∧ Γ ⊨ (p₂, Normal s') →^* (Skip, Stuck)))"
  apply(erule converse_rtranclp_induct)
   apply clarsimp
  apply clarsimp
  apply (rename_tac c s' s p₁ p₂)
  apply (case_tac "p₁ = Skip")
   apply simp
   apply (drule Seq_decomp_Skip)
   apply simp
  apply (case_tac "p₁ = Throw")
   apply simp
   apply (drule Seq_decomp_Throw)
   apply simp
  apply (drule Seq_decomp)
    apply simp+
  apply clarsimp
  apply (rename_tac s' s p₁ p₂ p₁')
  apply (case_tac s')
    apply simp
    apply (erule disjE)
     apply (erule (1) converse_rtranclp_into_rtranclp)
    apply clarsimp
    apply (rename_tac s')
    apply (erule_tac x="s'" in allE)
    apply (drule (1) converse_rtranclp_into_rtranclp, fastforce)
   apply simp
   apply (drule steps_Fault_prop, rule refl, fastforce)
   apply simp
   apply (cut_tac c=p₁' in steps_Stuck[where Γ=Γ])
  apply (frule steps_Stuck_prop[THEN sym], rule refl)
  apply simp
 done


lemma Catch_decomp_star[rule_format, OF _ refl, OF _ refl, OF _ _ refl]:
" Γ ⊨ cfg₁ →^* cfg₂ ==>
    ∀p s p' s'.
       cfg₁ = (p, Normal s) ⟶
       cfg₂ = (p', Normal s') ⟶
       final (p', Normal s') ⟶
       (∀p₁ p₂.
           p = Catch p₁ p₂ ⟶
           (∃t. Γ ⊨ (p₁, Normal s) →^* (Throw, Normal t) ∧ Γ ⊨ (p₂, Normal t) →^* (p', Normal s')) ∨
           (Γ ⊨ (p₁, Normal s) →^* (Skip, Normal s') ∧ p' = Skip))"
  apply (erule converse_rtranclp_induct)
   apply (clarsimp simp: final_def)
  apply clarsimp
  apply (rename_tac a b s p' s' p₁ p₂)
  apply (case_tac b)
    apply clarsimp
    apply (rename_tac x)
    apply (erule step_Normal_elim_cases)
      apply clarsimp
      apply (erule disjE)
       apply clarsimp
       apply (rename_tac t)
       apply (rule_tac x=t in exI)
       apply fastforce
      apply (erule impE)
       apply fastforce
      apply fastforce
     apply clarsimp
     apply (clarsimp simp: final_def)
     apply (erule disjE)
      apply fastforce
     apply clarsimp
     apply (fastforce dest: no_steps_final simp: final_def)
    apply (clarsimp simp: final_def)
    apply (erule disjE)
     apply clarsimp
     apply (rename_tac s s' p₂)
     apply (rule_tac x=s in exI)
     apply fastforce
    apply fastforce
   apply (fastforce dest: steps_Fault_prop)
  apply (fastforce dest: steps_Stuck_prop)
 done

lemma Catch_decomp_Skip[rule_format, OF _ refl] :
"Γ ⊨ (p, s) → (p', s') ==>
 ∀p₂. p = Catch Skip p₂ ⟶ s' = s ∧ p' = Skip"
  apply(erule step_induct, simp_all)
  apply clarsimp
  apply(erule step.cases, simp_all)
 done

lemma Catch_decomp[rule_format, OF _ refl] :
"Γ ⊨ (p, s) → (p', s') ==>
 ∀p₁ p₂. p = Catch p₁ p₂ ⟶ p₁ ≠ Skip ⟶ p₁ ≠ Throw ⟶
  (∃p₁'. Γ ⊨ (p₁, s) → (p₁', s') ∧ p' = Catch p₁' p₂)"
  apply(erule step_induct, simp_all)
   apply clarsimp
  apply(drule redex_size)
  apply simp
  apply clarsimp
  apply(drule redex_size)
  apply simp
 done

lemma Catch_decomp_star_Fault[rule_format, OF _ refl, OF _ refl, OF _ refl] :
"Γ ⊨ cfg₁ →^* cfg₂ ==> ∀p s f. cfg₁ = (p, Normal s) ⟶ cfg₂ = (Skip, Fault f) ⟶
 (∀p₁ p₂. p = Catch p₁ p₂ ⟶
 (Γ ⊨ (p₁, Normal s) →^* (Skip, Fault f))
 ∨ (∃s'. (Γ ⊨ (p₁, Normal s) →^* (Throw, Normal s')) ∧ Γ ⊨ (p₂, Normal s') →^* (Skip, Fault f)))"
  apply(erule converse_rtranclp_induct)
   apply clarsimp
  apply clarsimp
  apply (rename_tac c s' s f p₁ p₂)
  apply (case_tac "p₁ = Skip")
   apply (fastforce dest: Catch_decomp_Skip)
  apply (case_tac "p₁ = Throw")
   apply simp
   apply (case_tac s')
     apply clarsimp
     apply (erule step_Normal_elim_cases)
       apply clarsimp
       apply (erule disjE)
        apply fastforce
       apply (fastforce elim: no_step_final simp:final_def)
      apply fastforce
     apply fastforce
    apply clarsimp
    apply (drule_tac x=s in spec)
    apply clarsimp
    apply (erule step_elim_cases, simp_all)
    apply clarsimp
    apply (cut_tac c=c₁' and f=f in steps_Fault[where Γ=Γ])
    apply (drule steps_Fault_prop, rule refl)
    apply fastforce
   apply (fastforce dest: steps_Stuck_prop)
  apply (drule (2) Catch_decomp)
  apply clarsimp
  apply (rename_tac p₁')
  apply (case_tac s')
    apply simp
    apply (erule disjE)
     apply (erule (1) converse_rtranclp_into_rtranclp)
    apply clarsimp
    apply (rename_tac s')
    apply (erule_tac x="s'" in allE)
    apply (drule (1) converse_rtranclp_into_rtranclp, fastforce)
   apply simp
   apply (frule steps_Fault_prop[THEN sym], rule refl)
   apply simp
   apply (cut_tac c=p₁' and f=f in steps_Fault[where Γ=Γ])
   apply (drule (2)  converse_rtranclp_into_rtranclp)
  apply (fastforce dest: steps_Stuck_prop)
 done

lemma Catch_decomp_star_Stuck[rule_format, OF _ refl, OF _ refl, OF _ refl] :
"Γ ⊨ cfg₁ →^* cfg₂ ==> ∀p s. cfg₁ = (p, Normal s) ⟶ cfg₂ = (Skip, Stuck) ⟶
 (∀p₁ p₂. p = Catch p₁ p₂ ⟶
 (Γ ⊨ (p₁, Normal s) →^* (Skip, Stuck))
 ∨ (∃s'. (Γ ⊨ (p₁, Normal s) →^* (Throw, Normal s')) ∧ Γ ⊨ (p₂, Normal s') →^* (Skip, Stuck)))"
  apply(erule converse_rtranclp_induct)
   apply clarsimp
  apply clarsimp
  apply (rename_tac c s' s p₁ p₂)
  apply (case_tac "p₁ = Skip")
   apply (fastforce dest: Catch_decomp_Skip)
  apply (case_tac "p₁ = Throw")
   apply simp
   apply (case_tac s')
     apply clarsimp
     apply (erule step_Normal_elim_cases)
       apply clarsimp
       apply (erule disjE)
        apply fastforce
       apply (fastforce elim: no_step_final simp:final_def)
      apply fastforce
     apply fastforce
    apply clarsimp
    apply (drule_tac x=s in spec)
    apply clarsimp
    apply (erule step_elim_cases, simp_all)
    apply clarsimp
    apply (rename_tac c₁') 
    apply (cut_tac c=c₁' in steps_Fault[where Γ=Γ])
    apply (drule steps_Fault_prop, rule refl)
    apply fastforce

   apply (drule_tac x=s in spec)
   apply clarsimp
   apply (erule step_elim_cases, simp_all)
   apply clarsimp
   apply (cut_tac c=c₁' in steps_Stuck[where Γ=Γ])
   apply (fastforce)

  apply (drule (2) Catch_decomp)
  apply clarsimp
  apply (rename_tac p₁')
  apply (case_tac s')
    apply simp
    apply (erule disjE)
     apply (erule (1) converse_rtranclp_into_rtranclp)
    apply clarsimp
    apply (rename_tac s')
    apply (erule_tac x="s'" in allE)
    apply (drule (1) converse_rtranclp_into_rtranclp, fastforce)
   apply simp
   apply (frule steps_Fault_prop[THEN sym], rule refl)
   apply fastforce
  apply (cut_tac c=p₁' in steps_Stuck[where Γ=Γ])
  apply fastforce
 done

end