Theory SeqCatch_decomp

(*
 * 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⇩1 →⇧* cfg⇩2 ⟹ ∀p' t. cfg⇩2 = (p', Normal t) ⟶
 (∃p s. cfg⇩1 = (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⇩2. p = Seq Skip p⇩2 ⟶ s' = s ∧ p' = p⇩2"
  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⇩2 z. s = Normal z ⟶ p = Seq Throw p⇩2 ⟶ 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⇩1 →⇧* cfg⇩2 ⟹ ∀s. cfg⇩1 = (Throw, Normal s) ⟶
  cfg⇩2 = cfg⇩1"
  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⇩1 p⇩2. p = Seq p⇩1 p⇩2 ⟶ p⇩1 ≠ Skip ⟶ p⇩1 ≠ Throw ⟶
  (∃p⇩1'. Γ ⊢ (p⇩1, s) → (p⇩1', s') ∧ p' = Seq p⇩1' p⇩2)"
  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⇩1 p⇩2, Normal s) →⇧nn (p', Normal s') ⟹
 final (p', Normal s') ⟹
 (∃n1<n. Γ ⊢ (p⇩1, Normal s) →⇧nn1 (Throw, Normal s')) ∧ p'=Throw ∨
 (∃t n1 n2. Γ ⊢ (p⇩1, Normal s) →⇧nn1 (Skip, Normal t) ∧ n1 < n ∧ n2 < n ∧ Γ ⊢ (p⇩2, Normal t) →⇧nn2 (p', Normal s'))"
  apply (induct n arbitrary: p⇩1 p⇩2 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⇩1 p⇩2 s p' s' a b)
  apply(case_tac "p⇩1 = 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⇩1 p⇩2 s p' s' a b)
  apply(case_tac "p⇩1 = 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⇩1 p⇩2 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⇩1 p⇩2, Normal s) →⇧* (p', Normal s') ⟹ final (p', Normal s') ⟹
 Γ ⊢ (p⇩1, Normal s) →⇧* (Throw, Normal s') ∧ p'=Throw ∨
 (∃t. Γ ⊢ (p⇩1, Normal s) →⇧* (Skip, Normal t) ∧ Γ ⊢ (p⇩2, 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⇩1 p⇩2, Normal s) →⇧nn (Skip, Fault f) ⟹
 (∃n1. Γ ⊢ (p⇩1, Normal s) →⇧nn1 (Skip, Fault f)) ∨
 (∃t n1 n2. Γ ⊢ (p⇩1, Normal s) →⇧nn1 (Skip, Normal t) ∧ n1 < n ∧ n2 < n  ∧ Γ ⊢ (p⇩2, Normal t) →⇧nn2 (Skip, Fault f))"
  apply (induct n arbitrary: s p⇩1)
   apply (clarsimp simp: final_def)
  apply (simp only: relpowp.simps)
  apply (subst (asm) relpowp_commute[symmetric])
  apply clarsimp
  apply (rename_tac n s p⇩1 a b)
  apply (case_tac "p⇩1 = 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⇩1 = 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⇩1 →⇧* cfg⇩2 ⟹ ∀p s p' f. cfg⇩1 = (p, Normal s) ⟶ cfg⇩2 = (Skip, Fault f) ⟶ 
 (∀p⇩1 p⇩2. p = Seq p⇩1 p⇩2 ⟶ 
 (Γ ⊢ (p⇩1, Normal s) →⇧* (Skip, Fault f))
 ∨ (∃s'. (Γ ⊢ (p⇩1,  Normal s) →⇧* (Skip, Normal s')) ∧ Γ ⊢ (p⇩2, Normal s') →⇧* (Skip, Fault f)))"
  apply(erule converse_rtranclp_induct)
   apply clarsimp
  apply clarsimp
  apply (rename_tac c s' s f p⇩1 p⇩2)
  apply (case_tac "p⇩1 = Skip")
   apply simp
   apply (drule Seq_decomp_Skip)
   apply simp
  apply (case_tac "p⇩1 = 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⇩1' 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⇩1 p⇩2, Normal s) →⇧nn (Skip, Stuck) ⟹
 (∃n1. Γ ⊢ (p⇩1, Normal s) →⇧nn1 (Skip, Stuck)) ∨
 (∃t n1 n2. Γ ⊢ (p⇩1, Normal s) →⇧nn1 (Skip, Normal t) ∧ n1 < n ∧ n2 < n  ∧ Γ ⊢ (p⇩2, Normal t) →⇧nn2 (Skip, Stuck))"
  apply (induct n arbitrary: s p⇩1)
   apply (clarsimp simp: final_def)
  apply (simp only: relpowp.simps)
  apply (subst (asm) relpowp_commute[symmetric])
  apply clarsimp
  apply (rename_tac n s p⇩1 a b)
  apply (case_tac "p⇩1 = 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⇩1 = 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⇩1 →⇧* (Skip, Stuck) ⟹ ∀p s p'. cfg⇩1 = (p, Normal s) ⟶ 
 (∀p⇩1 p⇩2. p = Seq p⇩1 p⇩2 ⟶ 
 (Γ ⊢ (p⇩1, Normal s) →⇧* (Skip, Stuck))
 ∨ (∃s'. (Γ ⊢ (p⇩1,  Normal s) →⇧* (Skip, Normal s')) ∧ Γ ⊢ (p⇩2, Normal s') →⇧* (Skip, Stuck)))"
  apply(erule converse_rtranclp_induct)
   apply clarsimp
  apply clarsimp
  apply (rename_tac c s' s p⇩1 p⇩2)
  apply (case_tac "p⇩1 = Skip")
   apply simp
   apply (drule Seq_decomp_Skip)
   apply simp
  apply (case_tac "p⇩1 = Throw")
   apply simp
   apply (drule Seq_decomp_Throw)
   apply simp
  apply (drule Seq_decomp)
    apply simp+
  apply clarsimp
  apply (rename_tac s' s p⇩1 p⇩2 p⇩1')
  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⇩1' 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⇩1 →⇧* cfg⇩2 ⟹
    ∀p s p' s'.
       cfg⇩1 = (p, Normal s) ⟶
       cfg⇩2 = (p', Normal s') ⟶
       final (p', Normal s') ⟶
       (∀p⇩1 p⇩2.
           p = Catch p⇩1 p⇩2 ⟶
           (∃t. Γ ⊢ (p⇩1, Normal s) →⇧* (Throw, Normal t) ∧ Γ ⊢ (p⇩2, Normal t) →⇧* (p', Normal s')) ∨
           (Γ ⊢ (p⇩1, 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⇩1 p⇩2)
  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⇩2)
     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⇩2. p = Catch Skip p⇩2 ⟶ 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⇩1 p⇩2. p = Catch p⇩1 p⇩2 ⟶ p⇩1 ≠ Skip ⟶ p⇩1 ≠ Throw ⟶
  (∃p⇩1'. Γ ⊢ (p⇩1, s) → (p⇩1', s') ∧ p' = Catch p⇩1' p⇩2)"
  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⇩1 →⇧* cfg⇩2 ⟹ ∀p s f. cfg⇩1 = (p, Normal s) ⟶ cfg⇩2 = (Skip, Fault f) ⟶ 
 (∀p⇩1 p⇩2. p = Catch p⇩1 p⇩2 ⟶ 
 (Γ ⊢ (p⇩1, Normal s) →⇧* (Skip, Fault f)) 
 ∨ (∃s'. (Γ ⊢ (p⇩1,  Normal s) →⇧* (Throw, Normal s')) ∧ Γ ⊢ (p⇩2, Normal s') →⇧* (Skip, Fault f)))"
  apply(erule converse_rtranclp_induct)
   apply clarsimp
  apply clarsimp
  apply (rename_tac c s' s f p⇩1 p⇩2)
  apply (case_tac "p⇩1 = Skip")
   apply (fastforce dest: Catch_decomp_Skip)
  apply (case_tac "p⇩1 = 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⇩1' 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⇩1')
  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⇩1' 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⇩1 →⇧* cfg⇩2 ⟹ ∀p s. cfg⇩1 = (p, Normal s) ⟶ cfg⇩2 = (Skip, Stuck) ⟶ 
 (∀p⇩1 p⇩2. p = Catch p⇩1 p⇩2 ⟶ 
 (Γ ⊢ (p⇩1, Normal s) →⇧* (Skip, Stuck)) 
 ∨ (∃s'. (Γ ⊢ (p⇩1,  Normal s) →⇧* (Throw, Normal s')) ∧ Γ ⊢ (p⇩2, Normal s') →⇧* (Skip, Stuck)))"
  apply(erule converse_rtranclp_induct)
   apply clarsimp
  apply clarsimp
  apply (rename_tac c s' s p⇩1 p⇩2)
  apply (case_tac "p⇩1 = Skip")
   apply (fastforce dest: Catch_decomp_Skip)
  apply (case_tac "p⇩1 = 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⇩1') 
    apply (cut_tac c=c⇩1' 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⇩1' in steps_Stuck[where Γ=Γ])
   apply (fastforce)

  apply (drule (2) Catch_decomp)
  apply clarsimp
  apply (rename_tac p⇩1')
  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⇩1' in steps_Stuck[where Γ=Γ])
  apply fastforce
 done

end