Quelle  Compose.thy

(*
    Author:      Norbert Schirmer
    Maintainer:  Norbert Schirmer, norbert.schirmer at web de

Copyright (C) 2006-2008 Norbert Schirmer
Copyright (c) 2022 Apple Inc. All rights reserved.

*)

section "Experiments on State Composition"


theory Compose imports "../HoareTotalProps" begin

text ‹
  develop some theory to support state-space modular development of programs.
  experiments aim at the representation of state-spaces with records.
  we use ‹statespaces› instead we get this kind of compositionality for free.
 ›


subsection ‹Changing the State-Space›

(* Lift a command on statespace 'b to work on statespace 'a *)

definition lift_f:: "('S ==> 's) ==> ('S ==> 's ==> 'S) ==> ('s ==> 's) ==> ('S ==> 'S)"
  where "lift_f prj inject f = (λS. inject S (f (prj S)))"

definition lift_s:: "('S ==> 's) ==> 's set ==> 'S set"
  where "lift_s prj A = {S. prj S ∈ A}"

definition lift_r:: "('S ==> 's) ==> ('S ==> 's ==> 'S) ==> ('s × 's) set
                       ==> ('S × 'S) set"
where
"lift_r prj inject R = {(S,T). (prj S,prj T) ∈ R ∧ T=inject S (prj T)}"


primrec lift_c:: "('S ==> 's) ==> ('S ==> 's ==> 'S) ==> ('s,'p,'f) com ==> ('S,'p,'f) com"
where
"lift_c prj inject Skip = Skip" |
"lift_c prj inject (Basic f) = Basic (lift_f prj inject f)" |
"lift_c prj inject (Spec r) = Spec (lift_r prj inject r)" |
"lift_c prj inject (Seq c₁ c₂) =
  (Seq (lift_c prj inject c₁) (lift_c prj inject c₂))" |
"lift_c prj inject (Cond b c₁ c₂) =
  Cond (lift_s prj b) (lift_c prj inject c₁) (lift_c prj inject c₂)" |
"lift_c prj inject (While b c) =
  While (lift_s prj b) (lift_c prj inject c)" |
"lift_c prj inject (Call p) = Call p" |
"lift_c prj inject (DynCom c) = DynCom (λs. lift_c prj inject (c (prj s)))" |
"lift_c prj inject (Guard f g c) = Guard f (lift_s prj g) (lift_c prj inject c)" |
"lift_c prj inject Throw = Throw" |
"lift_c prj inject (Catch c₁ c₂) =
  Catch (lift_c prj inject c₁) (lift_c prj inject c₂)"



lemma lift_{c_Skip}: "(lift_c prj inject c = Skip) = (c = Skip)"
  by (cases c) auto

lemma lift_{c_Basic}:
  "(lift_c prj inject c = Basic lf) = (∃f. c = Basic f ∧ lf = lift_f prj inject f)"
  by (cases c) auto

lemma lift_{c_Spec}:
  "(lift_c prj inject c = Spec lr) = (∃r. c = Spec r ∧ lr = lift_r prj inject r)"
  by (cases c) auto

lemma lift_{c_Seq}:
  "(lift_c prj inject c = Seq lc₁ lc₂) =
     (∃ c₁ c₂. c = Seq c₁ c₂ ∧
               lc₁ = lift_c prj inject c₁ ∧ lc₂ = lift_c prj inject c₂ )"
    by (cases c) auto

lemma lift_{c_Cond}:
  "(lift_c prj inject c = Cond lb lc₁ lc₂) =
     (∃b c₁ c₂. c = Cond b c₁ c₂ ∧ lb = lift_s prj b ∧
                lc₁ = lift_c prj inject c₁ ∧ lc₂ = lift_c prj inject c₂ )"
  by (cases c) auto

lemma lift_{c_While}:
  "(lift_c prj inject c = While lb lc') =
     (∃b c'. c = While b c' ∧ lb = lift_s prj b ∧
               lc' = lift_c prj inject c')"
  by (cases c) auto

lemma lift_{c_Call}:
  "(lift_c prj inject c = Call p) = (c = Call p)"
  by (cases c) auto

lemma lift_{c_DynCom}:
  "(lift_c prj inject c = DynCom lc) =
     (∃C. c=DynCom C ∧ lc = (λs. lift_c prj inject (C (prj s))))"
  by (cases c) auto

lemma lift_{c_Guard}:
  "(lift_c prj inject c = Guard f lg lc') =
     (∃g c'. c = Guard f g c' ∧ lg = lift_s prj g ∧
             lc' = lift_c prj inject c')"
   by (cases c) auto

lemma lift_{c_Throw}:
  "(lift_c prj inject c = Throw) = (c = Throw)"
  by (cases c) auto

lemma lift_{c_Catch}:
  "(lift_c prj inject c = Catch lc₁ lc₂) =
     (∃ c₁ c₂. c = Catch c₁ c₂ ∧
               lc₁ = lift_c prj inject c₁ ∧ lc₂ = lift_c prj inject c₂ )"
    by (cases c) auto



definition xstate_map:: "('S ==> 's) ==> ('S,'f) xstate ==> ('s,'f) xstate"
where
"xstate_map g x = (case x of
                      Normal s ==> Normal (g s)
                    | Abrupt s ==> Abrupt (g s)
                    | Fault f ==> Fault f
                    | Stuck ==> Stuck)"

lemma xstate_map_simps [simp]:
"xstate_map g (Normal s) = Normal (g s)"
"xstate_map g (Abrupt s) = Abrupt (g s)"
"xstate_map g (Fault f) = (Fault f)"
"xstate_map g Stuck = Stuck"
  by (auto simp add: xstate_map_def)

lemma xstate_map_Normal_conv:
  "xstate_map g S = Normal s = (∃s'. S=Normal s' ∧ s = g s')"
  by (cases S) auto

lemma xstate_map_Abrupt_conv:
  "xstate_map g S = Abrupt s = (∃s'. S=Abrupt s' ∧ s = g s')"
  by (cases S) auto

lemma xstate_map_Fault_conv:
  "xstate_map g S = Fault f = (S=Fault f)"
  by (cases S) auto

lemma xstate_map_Stuck_conv:
  "xstate_map g S = Stuck = (S=Stuck)"
  by (cases S) auto

lemmas xstate_map_convs = xstate_map_Normal_conv xstate_map_Abrupt_conv
 xstate_map_Fault_conv xstate_map_Stuck_conv

definition state:: "('s,'f) xstate ==> 's"
where
"state x = (case x of
               Normal s ==> s
             | Abrupt s ==> s
             | Fault g ==> undefined
             | Stuck ==> undefined)"

lemma state_simps [simp]:
"state (Normal s) = s"
"state (Abrupt s) = s"
  by (auto simp add: state_def )


locale lift_state_space =
  fixes project::"'S ==> 's"
  fixes "inject"::"'S ==> 's ==> 'S"
  fixes "project_x"::"('S,'f) xstate ==> ('s,'f) xstate"
  fixes "lift_e"::"('s,'p,'f) body ==> ('S,'p,'f) body"
  fixes lift_c:: "('s,'p,'f) com ==> ('S,'p,'f) com"
  fixes lift_f:: "('s ==> 's) ==> ('S ==> 'S)"
  fixes lift_s:: "'s set ==> 'S set"
  fixes lift_r:: "('s × 's) set ==> ('S × 'S) set"
  assumes proj_inj_commute: "∧S s. project (inject S s) = s"
  defines "lift_c ≡ Compose.lift_c project inject"
  defines "project_x ≡ xstate_map project"
  defines "lift_e ≡ (λΓ p. map_option lift_c (Γ p))"
  defines "lift_f ≡ Compose.lift_f project inject"
  defines "lift_s ≡ Compose.lift_s project"
  defines "lift_r ≡ Compose.lift_r project inject"


lemma (in lift_state_space) lift_{f_simp}:
 "lift_f f ≡ λS. inject S (f (project S))"
  by (simp add: lift_{f_def} Compose.lift_{f_def})

lemma (in lift_state_space) lift_{s_simp}:
  "lift_s A ≡ {S. project S ∈ A}"
  by  (simp add: lift_{s_def} Compose.lift_{s_def})

lemma (in lift_state_space) lift_{r_simp}:
"lift_r R ≡ {(S,T). (project S,project T) ∈ R ∧ T=inject S (project T)}"
  by  (simp add: lift_{r_def} Compose.lift_{r_def})

(* Causes loop when instantiating locale
lemmas (in lift_state_space) lift\<^sub>f_simp  = Compose.lift\<^sub>f_def
 [of project "inject", folded lift\<^sub>f_def]
lemmas (in lift_state_space) lift\<^sub>s_simp  = Compose.lift\<^sub>s_def
 [of project, folded lift\<^sub>s_def]
lemmas (in lift_state_space) lift\<^sub>r_simp  = Compose.lift\<^sub>r_def
 [of project "inject", folded lift\<^sub>r_def]
*)
lemma (in lift_state_space) lift_{c_Skip_simp} [simp]:
 "lift_c Skip = Skip"
  by (simp add: lift_{c_def})
lemma (in lift_state_space) lift_{c_Basic_simp} [simp]:
"lift_c (Basic f) = Basic (lift_f f)"
  by (simp add: lift_{c_def} lift_{f_def})
lemma (in lift_state_space) lift_{c_Spec_simp} [simp]:
"lift_c (Spec r) = Spec (lift_r r)"
  by (simp add: lift_{c_def} lift_{r_def})
lemma (in lift_state_space) lift_{c_Seq_simp} [simp]:
"lift_c (Seq c₁ c₂) =
  (Seq (lift_c c₁) (lift_c c₂))"
  by (simp add: lift_{c_def})
lemma (in lift_state_space) lift_{c_Cond_simp} [simp]:
"lift_c (Cond b c₁ c₂) =
  Cond (lift_s b) (lift_c c₁) (lift_c c₂)"
  by (simp add: lift_{c_def} lift_{s_def})
lemma (in lift_state_space) lift_{c_While_simp} [simp]:
"lift_c (While b c) =
  While (lift_s b) (lift_c c)"
  by (simp add: lift_{c_def} lift_{s_def})
lemma (in lift_state_space) lift_{c_Call_simp} [simp]:
"lift_c (Call p) = Call p"
  by (simp add: lift_{c_def})
lemma (in lift_state_space) lift_{c_DynCom_simp} [simp]:
"lift_c (DynCom c) = DynCom (λs. lift_c (c (project s)))"
  by (simp add: lift_{c_def})
lemma (in lift_state_space) lift_{c_Guard_simp} [simp]:
"lift_c (Guard f g c) = Guard f (lift_s g) (lift_c c)"
  by (simp add: lift_{c_def} lift_{s_def})
lemma (in lift_state_space) lift_{c_Throw_simp} [simp]:
"lift_c Throw = Throw"
  by (simp add: lift_{c_def})
lemma (in lift_state_space) lift_{c_Catch_simp} [simp]:
"lift_c (Catch c₁ c₂) =
  Catch (lift_c c₁) (lift_c c₂)"
  by (simp add: lift_{c_def})

lemma (in lift_state_space) project_{x_def}':
"project_x s ≡ (case s of
                 Normal s ==> Normal (project s)
                | Abrupt s ==> Abrupt (project s)
                | Fault f ==> Fault f
                | Stuck ==> Stuck)"
  by (simp add: xstate_map_def project_{x_def})

lemma (in lift_state_space) lift_{e_def}':
  "lift_e Γ p ≡ (case Γ p of Some bdy ==> Some (lift_c bdy) | None ==> None)"
  by (simp add: lift_{e_def} map_option_case)




text ‹
  problem is that @{term "(lift_c project inject ∘ Γ)"} is quite
  strong premise. The problem is that @{term "Γ"} is a function here.
  map would be better. We only have to lift those procedures in the domain
  @{term "Γ"}:
 ‹Γ p = Some bdy ⟶ Γ' p = Some lift_c project inject bdy›.
  then can com up with theorems that allow us to extend the domains
  @{term Γ} and preserve validity.
 ›


lemma (in lift_state_space)
"{(S,T). ∃t. (project S,t) ∈ r ∧ T=inject S t}
 ⊆ {(S,T). (project S,project T) ∈ r ∧ T=inject S (project T)}"
  apply clarsimp
  apply (rename_tac S t)
  apply (simp add: proj_inj_commute)
  done

lemma (in lift_state_space)
"{(S,T). (project S,project T) ∈ r ∧ T=inject S (project T)}
 ⊆ {(S,T). ∃t. (project S,t) ∈ r ∧ T=inject S t}"
  apply clarsimp
  apply (rename_tac S T)
  apply (rule_tac x="project T" in exI)
  apply simp
  done


lemma (in lift_state_space) lift_exec:
assumes exec_lc: "(lift_e Γ)⊨⟨lc,s⟩ ==> t"
shows "∧c. [ lift_c c = lc] ==>
              Γ⊨⟨c,project_x s⟩ ==> project_x t"
using exec_lc
proof (induct)
  case Skip thus ?case
    by (auto simp add: project_{x_def} lift_{c_Skip} lift_{c_def} intro: exec.Skip)
next
  case Guard thus ?case
    by (auto simp add: project_{x_def} lift_{s_def} Compose.lift_{s_def} lift_{c_Guard} lift_{c_def}
      intro: exec.Guard)
next
  case GuardFault thus ?case
    by (auto simp add: project_{x_def} lift_{s_def} Compose.lift_{s_def} lift_{c_Guard} lift_{c_def}
      intro: exec.GuardFault)
next
  case FaultProp thus ?case
    by (fastforce simp add: project_{x_def})
next
  case Basic
  thus ?case
    by (fastforce simp add: project_{x_def} lift_{c_Basic} lift_{f_def} Compose.lift_{f_def}
      lift_{c_def}
        proj_inj_commute
        intro: exec.Basic)
next
  case Spec
  thus ?case
    by (fastforce simp add: project_{x_def} lift_{c_Spec} lift_{f_def} Compose.lift_{f_def}
        lift_{r_def} Compose.lift_{r_def} lift_{c_def}
        proj_inj_commute
        intro: exec.Spec)
next
  case (SpecStuck s r)
  thus ?case
    apply (simp add: project_{x_def})
    apply (clarsimp simp add: lift_{c_Spec} lift_{c_def})
    apply (unfold lift_{r_def} Compose.lift_{r_def})
    apply (rule exec.SpecStuck)
    apply (rule allI)
    apply (erule_tac x="inject s t" in allE)
    apply clarsimp
    apply (simp add: proj_inj_commute)
    done
next
  case Seq
  thus ?case
    by (fastforce simp add: project_{x_def} lift_{c_Seq} lift_{c_def} intro: exec.intros)
next
  case CondTrue
  thus ?case
     by (auto simp add: project_{x_def} lift_{s_def} Compose.lift_{s_def} lift_{c_Cond} lift_{c_def}
         intro: exec.CondTrue)
next
  case CondFalse
  thus ?case
     by (auto simp add: project_{x_def} lift_{s_def} Compose.lift_{s_def} lift_{c_Cond} lift_{c_def}
         intro: exec.CondFalse)
next
  case WhileTrue
  thus ?case
     by (fastforce simp add: project_{x_def} lift_{s_def} Compose.lift_{s_def}
         lift_{c_While} lift_{c_def}
         intro: exec.WhileTrue)
next
  case WhileFalse
  thus ?case
     by (fastforce simp add: project_{x_def} lift_{s_def} Compose.lift_{s_def}
         lift_{c_While} lift_{c_def}
         intro: exec.WhileFalse)
next
  case Call
  thus ?case
    by (fastforce simp add:
               project_{x_def} lift_{c_Call} lift_{f_def} Compose.lift_{f_def} lift_{c_def}
               lift_{e_def}
          intro: exec.Call)
next
  case CallUndefined
  thus ?case
    by (fastforce simp add:
               project_{x_def} lift_{c_Call} lift_{f_def} Compose.lift_{f_def} lift_{c_def}
               lift_{e_def}
          intro: exec.CallUndefined)
next
  case StuckProp thus ?case
    by (fastforce simp add: project_{x_def})
next
  case DynCom
  thus ?case
    by (fastforce simp add:
               project_{x_def} lift_{c_DynCom} lift_{f_def} Compose.lift_{f_def} lift_{c_def}
          intro: exec.DynCom)
next
  case Throw thus ?case
    by (fastforce simp add: project_{x_def} lift_{c_Throw} lift_{c_def} intro: exec.Throw)
next
  case AbruptProp thus ?case
    by (fastforce simp add: project_{x_def})
next
  case CatchMatch
  thus ?case
    by (fastforce simp add: project_{x_def} lift_{c_Catch} lift_{c_def} intro: exec.CatchMatch)
next
  case (CatchMiss c₁ s t c₂ c)
  thus ?case
    by (cases t)
       (fastforce simp add: project_{x_def} lift_{c_Catch} lift_{c_def} intro: exec.CatchMiss)+
qed

lemma (in lift_state_space) lift_exec':
assumes exec_lc: "(lift_e Γ)⊨⟨lift_c c,s⟩ ==> t"
shows "Γ⊨⟨c,project_x s⟩ ==> project_x t"
  using lift_exec [OF exec_lc]
  by simp



lemma (in lift_state_space) lift_valid:
  assumes valid: "Γ⊨_F P c Q,A"
  shows
   "(lift_e Γ)⊨_F (lift_s P) (lift_c c) (lift_s Q),(lift_s A)"
proof (rule validI)
  fix s t
  assume lexec:
    "(lift_e Γ)⊨⟨lift_c c,Normal s⟩ ==> t"
  assume lP: "s ∈ lift_s P"
  assume noFault: "t ∉ Fault ` F"
  show "t ∈ Normal ` lift_s Q ∪ Abrupt ` lift<sub>s</sub> A"
  proof -
    from lexec
    have "Γ⊨ ⟨c,project<sub>x</sub> (Normal s)⟩ ==> (project<sub>x</sub> t)"
      by (rule lift_exec) (simp_all)
    moreover
    from lP have "project s ∈ P"
      by (simp add: lift<sub>s_def</sub> Compose.lift<sub>s_def</sub> project<sub>x_def</sub>)
    ultimately
    have "project<sub>x</sub> t ∈ Normal ` Q ∪ Abrupt ` A"
      using valid noFault
      apply (clarsimp simp add: valid_def project_{x_def})
      apply (cases t)
      apply auto
      done
    thus ?thesis
      apply (simp add: lift_{s_def} Compose.lift_{s_def})
      apply (cases t)
      apply (auto simp add: project_{x_def})
      done
  qed
qed

lemma (in lift_state_space) lift_hoarep:
  assumes deriv: "Γ,{}⊨_F P c Q,A"
  shows
   "(lift_e Γ),{}⊨_F (lift_s P) (lift_c c) (lift_s Q),(lift_s A)"
apply (rule hoare_complete)
apply (insert hoare_sound [OF deriv])
apply (rule lift_valid)
apply (simp add: cvalid_def)
done

lemma (in lift_state_space) lift_hoarep':
  "∀Z. Γ,{}⊨_F (P Z) c (Q Z),(A Z) ==>
    ∀Z. (lift_e Γ),{}⊨_F (lift_s (P Z)) (lift_c c)
                                  (lift_s (Q Z)),(lift_s (A Z))"
apply (iprover intro: lift_hoarep)
done



lemma (in lift_state_space) lift_termination:
assumes termi: "Γ⊨c↓s"
shows "∧S. project_x S = s ==>
  lift_e Γ ⊨(lift_c c)↓S"
  using termi
proof (induct)
  case Skip thus ?case
    by (clarsimp simp add: terminates.Skip project_{x_def} xstate_map_convs)
next
  case Basic thus ?case
    by (fastforce simp add: project_{x_def} xstate_map_convs intro: terminates.intros)
next
  case Spec thus ?case
    by (fastforce simp add: project_{x_def} xstate_map_convs intro: terminates.intros)
next
  case Guard thus ?case
    by (auto simp add: project_{x_def} xstate_map_convs intro: terminates.intros)
next
  case GuardFault thus ?case
    by (auto simp add: project_{x_def} xstate_map_convs lift_{s_def} Compose.lift_{s_def}
           intro: terminates.intros)
next
  case Fault thus ?case by (clarsimp simp add: project_{x_def} xstate_map_convs)
next
  case (Seq c1 s c2)
  have "project_x S = Normal s" by fact
  then obtain s' where S: "S=Normal s'" and s: "s = project s'"
    by (auto simp add: project_{x_def} xstate_map_convs)
  from Seq have "lift_e Γ⊨lift_c c1 ↓ S"
    by simp
  moreover
  {
    fix w
    assume exec_lc1: "lift_e Γ⊨⟨lift_c c1,Normal s'⟩ ==> w"
    have "lift_e Γ⊨lift_c c2 ↓ w"
    proof (cases w)
      case (Normal w')
      with lift_exec [where c=c1, OF exec_lc1] s
      have "Γ⊨⟨c1,Normal s⟩ ==> Normal (project w')"
        by (simp add: project_{x_def})
      from Seq.hyps (3) [rule_format, OF this] Normal
      show "lift_e Γ⊨lift_c c2 ↓ w"
        by (auto simp add: project_{x_def} xstate_map_convs)
    qed (auto)
  }
  ultimately show ?case
    using S s
    by (auto intro: terminates.intros)
next
  case CondTrue thus ?case
    by (fastforce simp add: project_{x_def} lift_{s_def} Compose.lift_{s_def} xstate_map_convs
      intro: terminates.intros)
next
  case CondFalse thus ?case
    by (fastforce simp add: project_{x_def} lift_{s_def} Compose.lift_{s_def} xstate_map_convs
      intro: terminates.intros)
next
  case (WhileTrue s b c)
  have "project_x S = Normal s" by fact
  then obtain s' where S: "S=Normal s'" and s: "s = project s'"
    by (auto simp add: project_{x_def} xstate_map_convs)
  from WhileTrue have "lift_e Γ⊨lift_c c ↓ S"
    by simp
  moreover
  {
    fix w
    assume exec_lc: "lift_e Γ⊨⟨lift_c c,Normal s'⟩ ==> w"
    have "lift_e Γ⊨lift_c (While b c) ↓ w"
    proof (cases w)
      case (Normal w')
      with lift_exec [where c=c, OF exec_lc] s
      have "Γ⊨⟨c,Normal s⟩ ==> Normal (project w')"
        by (simp add: project_{x_def})
      from WhileTrue.hyps (4) [rule_format, OF this] Normal
      show "lift_e Γ⊨lift_c (While b c) ↓ w"
        by (auto simp add: project_{x_def} xstate_map_convs)
    qed (auto)
  }
  ultimately show ?case
    using S s
    by (auto intro: terminates.intros)
next
  case WhileFalse thus ?case
    by (fastforce simp add: project_{x_def} lift_{s_def} Compose.lift_{s_def} xstate_map_convs
      intro: terminates.intros)
next
  case Call thus ?case
    by (fastforce simp add: project_{x_def} xstate_map_convs lift_{e_def}
      intro: terminates.intros)
next
  case CallUndefined thus ?case
    by (fastforce simp add: project_{x_def} xstate_map_convs lift_{e_def}
      intro: terminates.intros)
next
  case Stuck thus ?case
    by (fastforce simp add: project_{x_def} xstate_map_convs)
next
  case DynCom thus ?case
    by (fastforce simp add: project_{x_def} xstate_map_convs
      intro: terminates.intros)
next
  case Throw thus ?case
    by (fastforce simp add: project_{x_def} xstate_map_convs
      intro: terminates.intros)
next
  case Abrupt thus ?case
    by (fastforce simp add: project_{x_def} xstate_map_convs
      intro: terminates.intros)
next
  case (Catch c1 s c2)
  have "project_x S = Normal s" by fact
  then obtain s' where S: "S=Normal s'" and s: "s = project s'"
    by (auto simp add: project_{x_def} xstate_map_convs)
  from Catch have "lift_e Γ⊨lift_c c1 ↓ S"
    by simp
  moreover
  {
    fix w
    assume exec_lc1: "lift_e Γ⊨⟨lift_c c1,Normal s'⟩ ==> Abrupt w"
    have "lift_e Γ⊨lift_c c2 ↓ Normal w"
    proof -
      from lift_exec [where c=c1, OF exec_lc1] s
      have "Γ⊨⟨c1,Normal s⟩ ==> Abrupt (project w)"
        by (simp add: project_{x_def})
      from Catch.hyps (3) [rule_format, OF this]
      show "lift_e Γ⊨lift_c c2 ↓ Normal w"
        by (auto simp add: project_{x_def} xstate_map_convs)
    qed
  }
  ultimately show ?case
    using S s
    by (auto intro: terminates.intros)
qed

lemma (in lift_state_space) lift_termination':
assumes termi: "Γ⊨c↓project_x S"
shows "lift_e Γ ⊨(lift_c c)↓S"
  using lift_termination [OF termi]
  by iprover


lemma (in lift_state_space) lift_validt:
  assumes valid: "Γ⊨_tF P c Q,A"
  shows "(lift_e Γ)⊨_tF (lift_s P) (lift_c c) (lift_s Q),(lift_s A)"
proof -
  from valid
  have "(lift_e Γ)⊨_F (lift_s P) (lift_c c) (lift_s Q),(lift_s A)"
    by (auto intro: lift_valid simp add: validt_def)
  moreover
  {
    fix S
    assume "S ∈ lift_s P"
    hence "project S ∈ P"
      by (simp add: lift_{s_def} Compose.lift_{s_def})
    with valid have "Γ⊨c ↓ project_x (Normal S)"
      by (simp add: validt_def project_{x_def})
    hence "lift_e Γ⊨lift_c c ↓ Normal S"
      by (rule lift_termination')
  }
  ultimately show ?thesis
    by (simp add: validt_def)
qed

lemma (in lift_state_space) lift_hoaret:
  assumes deriv: "Γ,{}⊨_tF P c Q,A"
  shows
   "(lift_e Γ),{}⊨_tF (lift_s P) (lift_c c) (lift_s Q),(lift_s A)"
apply (rule hoaret_complete)
apply (insert hoaret_sound [OF deriv])
apply (rule lift_validt)
apply (simp add: cvalidt_def)
done


locale lift_state_space_ext = lift_state_space +
  assumes inj_proj_commute: "∧S. inject S (project S) = S"
  assumes inject_last: "∧S s t. inject (inject S s) t = inject S t"


(* \<exists>x. state t = inject (state s) x *)
lemma (in lift_state_space_ext) lift_exec_inject_same:
assumes exec_lc: "(lift_e Γ)⊨⟨lc,s⟩ ==> t"
shows "∧c. [lift_c c = lc; t ∉ (Fault ` UNIV) ∪ {Stuck}] ==>
              state t = inject (state s) (project (state t))"
using exec_lc
proof (induct)
  case Skip thus ?case
    by (clarsimp simp add: inj_proj_commute)
next
  case Guard thus ?case
    by (clarsimp simp add: lift<sub>c_Guard</sub> lift<sub>c_def</sub>)
next
  case GuardFault thus ?case
    by simp
next
  case FaultProp thus ?case by simp
next
  case Basic thus ?case
    by (clarsimp simp add: lift<sub>f_def</sub> Compose.lift<sub>f_def</sub>
        proj_inj_commute lift<sub>c_Basic</sub> lift<sub>c_def</sub>)
next
  case (Spec r) thus ?case
    by (clarsimp simp add: Compose.lift<sub>r_def</sub> lift<sub>c_Spec</sub> lift<sub>c_def</sub>)
next
  case SpecStuck
  thus ?case by simp
next
  case (Seq lc1 s s' lc2 t c)
  have t: "t ∉ Fault ` UNIV ∪ {Stuck}" by fact
  have "lift_c c = Seq lc1 lc2" by fact
  then obtain c1 c2 where
    c: "c = Seq c1 c2" and
    lc1: "lc1 = lift_c c1" and
    lc2: "lc2 = lift_c c2"
    by (auto simp add: lift_{c_Seq} lift_{c_def})
  show ?case
  proof (cases s')
    case (Normal s'')
    from Seq.hyps (2) [OF lc1 [symmetric]] this
    have "s'' = inject s (project s'')"
      by auto
    moreover from Seq.hyps (4) [OF lc2 [symmetric]] Normal t
    have "state t = inject s'' (project (state t))"
      by auto
    ultimately have "state t = inject (inject s (project s'')) (project (state t))"
      by simp
    then show ?thesis
      by (simp add: inject_last)
  next
    case (Abrupt s'')
    from Seq.hyps (2) [OF lc1 [symmetric]] this
    have "s'' = inject s (project s'')"
      by auto
    moreover from Seq.hyps (4) [OF lc2 [symmetric]] Abrupt t
    have "state t = inject s'' (project (state t))"
      by auto
    ultimately have "state t = inject (inject s (project s'')) (project (state t))"
      by simp
    then show ?thesis
      by (simp add: inject_last)
  next
    case (Fault f)
    with Seq
    have "t = Fault f"
      by (auto dest: Fault_end)
    with t have False by simp
    thus ?thesis ..
  next
    case Stuck
    with Seq
    have "t = Stuck"
      by (auto dest: Stuck_end)
    with t have False by simp
    thus ?thesis ..
  qed
next
  case CondTrue thus ?case
    by (clarsimp simp add: lift_{c_Cond} lift_{c_def})
next
  case CondFalse thus ?case
    by (clarsimp simp add: lift_{c_Cond} lift_{c_def})
next
  case (WhileTrue s lb lc' s' t c)
  have t: "t ∉ Fault ` UNIV ∪ {Stuck}" by fact
  have lw: "lift<sub>c</sub> c = While lb lc'" by fact
  then obtain b c' where
    c: "c = While b c'" and
    lb: "lb = lift<sub>s</sub> b" and
    lc: "lc' = lift<sub>c</sub> c'"
    by (auto simp add: lift<sub>c_While</sub> lift<sub>s_def</sub> lift<sub>c_def</sub>)
  show ?case
  proof (cases s')
    case (Normal s'')
    from WhileTrue.hyps (3) [OF lc [symmetric]] this
    have "s'' = inject s (project s'')"
      by auto
    moreover from WhileTrue.hyps (5) [OF lw] Normal t
    have "state t = inject s'' (project (state t))"
      by auto
    ultimately have "state t = inject (inject s (project s'')) (project (state t))"
      by simp
    then show ?thesis
      by (simp add: inject_last)
  next
    case (Abrupt s'')
    from WhileTrue.hyps (3) [OF lc [symmetric]] this
    have "s'' = inject s (project s'')"
      by auto
    moreover from WhileTrue.hyps (5) [OF lw] Abrupt t
    have "state t = inject s'' (project (state t))"
      by auto
    ultimately have "state t = inject (inject s (project s'')) (project (state t))"
      by simp
    then show ?thesis
      by (simp add: inject_last)
  next
    case (Fault f)
    with WhileTrue
    have "t = Fault f"
      by (auto dest: Fault_end)
    with t have False by simp
    thus ?thesis ..
  next
    case Stuck
    with WhileTrue
    have "t = Stuck"
      by (auto dest: Stuck_end)
    with t have False by simp
    thus ?thesis ..
  qed
next
  case WhileFalse thus ?case
    by (clarsimp simp add: lift<sub>c_While</sub> inj_proj_commute)
next
  case Call thus ?case
    by (clarsimp simp add: inject_last lift<sub>c_Call</sub> lift<sub>e_def</sub> lift<sub>c_def</sub>)
next
  case CallUndefined thus ?case by simp
next
  case StuckProp thus ?case by simp
next
  case DynCom
  thus ?case
    by (clarsimp simp add: lift<sub>c_DynCom</sub> lift<sub>c_def</sub>)
next
  case Throw thus ?case
    by (simp add: inj_proj_commute)
next
  case AbruptProp thus ?case by (simp add: inj_proj_commute)
next
  case (CatchMatch lc1 s s' lc2 t c)
  have t: "t ∉ Fault ` UNIV ∪ {Stuck}" by fact
  have "lift_c c = Catch lc1 lc2" by fact
  then obtain c1 c2 where
    c: "c = Catch c1 c2" and
    lc1: "lc1 = lift_c c1" and
    lc2: "lc2 = lift_c c2"
    by (auto simp add: lift_{c_Catch} lift_{c_def})
  from CatchMatch.hyps (2) [OF lc1 [symmetric]] this
  have "s' = inject s (project s')"
    by auto
  moreover
  from CatchMatch.hyps (4) [OF lc2 [symmetric]] t
  have "state t = inject s' (project (state t))"
    by auto
  ultimately have "state t = inject (inject s (project s')) (project (state t))"
    by simp
  then show ?case
    by (simp add: inject_last)
next
  case CatchMiss
  thus ?case
    by (clarsimp simp add: lift_{c_Catch} lift_{c_def})
qed

lemma (in lift_state_space_ext) valid_inject_project:
 assumes noFaultStuck:
  "Γ⊨⟨c,Normal (project σ)⟩ ==>∉(Fault ` UNIV ∪ {Stuck})"
 shows "lift<sub>e</sub> Γ⊨<sub>F</sub> {σ} lift<sub>c</sub> c
                {t. t=inject σ (project t)}, {t. t=inject σ (project t)}"
proof (rule validI)
  fix s t
  assume exec: "lift<sub>e</sub> Γ⊨⟨lift<sub>c</sub> c,Normal s⟩ ==> t"
  assume P: "s ∈ {σ}"
  assume noFault: "t ∉ Fault ` F"
  show "t ∈ Normal ` {t. t = inject σ (project t)} ∪
        Abrupt ` {t. t = inject σ (project t)}"
  proof -
    from lift_exec [OF exec]
    have "Γ⊨⟨c,project_x (Normal s)⟩ ==> project_x t"
      by simp
    with noFaultStuck P have t: "t ∉ Fault ` UNIV ∪ {Stuck}"
      by (auto simp add: final_notin_def project_{x_def})
    from lift_exec_inject_same [OF exec refl this] P
    have "state t = inject σ (project (state t))"
      by simp
    with t show ?thesis
      by (cases t) auto
  qed
qed

lemma (in lift_state_space_ext) lift_exec_inject_same':
assumes exec_lc: "(lift_e Γ)⊨⟨lift_c c,S⟩ ==> T"
shows "∧c. [T ∉ (Fault ` UNIV) ∪ {Stuck}] ==>
              state T = inject (state S) (project (state T))"
  using lift_exec_inject_same [OF exec_lc]
  by simp

lemma (in lift_state_space_ext) valid_lift_modifies:
  assumes valid: "∀s. Γ⊨_F {s} c (Modif s),(ModifAbr s)"
  shows "(lift_e Γ)⊨_F {S} (lift_c c)
           {T. T ∈ lift_s (Modif (project S)) ∧ T=inject S (project T)},
           {T. T ∈ lift_s (ModifAbr (project S)) ∧ T=inject S (project T)}"
proof (rule validI)
  fix s t
  assume exec: "lift_e Γ⊨⟨lift_c c,Normal s⟩ ==> t"
  assume P: "s ∈ {S}"
  assume noFault: "t ∉ Fault ` F"
  show "t ∈ Normal `
                 {t ∈ lift_s (Modif (project S)).
                  t = inject S (project t)} ∪
                 Abrupt `
                 {t ∈ lift<sub>s</sub> (ModifAbr (project S)).
                  t = inject S (project t)}"
  proof -
    from lift_exec [OF exec]
    have "Γ⊨ ⟨c,project<sub>x</sub> (Normal s)⟩ ==> project<sub>x</sub> t"
      by auto
    moreover
    from noFault have "project<sub>x</sub> t ∉ Fault ` F"
      by (cases "t") (auto simp add: project_{x_def})
    ultimately
    have "project_x t ∈
            Normal ` (Modif (project s)) ∪ Abrupt ` (ModifAbr (project s))"
      using valid [rule_format, of "(project s)"]
      by (auto simp add: valid_def project_{x_def})
    hence t: "t ∈ Normal ` lift<sub>s</sub> (Modif (project s)) ∪
               Abrupt ` lift_s (ModifAbr (project s))"
      by (cases t) (auto simp add: project_{x_def} lift_{s_def} Compose.lift_{s_def})
    then have "t ∉ Fault ` UNIV ∪ {Stuck}"
      by (cases t) auto
    from lift_exec_inject_same [OF exec _ this]
    have "state t = inject (state (Normal s)) (project (state t))"
      by simp
    with t show ?thesis
      using P by auto
  qed
qed

lemma (in lift_state_space_ext) hoare_lift_modifies:
  assumes deriv: "∀σ. Γ,{}⊨_F {σ} c (Modif σ),(ModifAbr σ)"
  shows "∀σ. (lift_e Γ),{}⊨_F {σ} (lift_c c)
           {T. T ∈ lift_s (Modif (project σ)) ∧ T=inject σ (project T)},
           {T. T ∈ lift_s (ModifAbr (project σ)) ∧ T=inject σ (project T)}"
apply (rule allI)
apply (rule hoare_complete)
apply (rule valid_lift_modifies)
apply (rule allI)
apply (insert hoare_sound [OF deriv [rule_format]])
apply (simp add: cvalid_def)
done

lemma (in lift_state_space_ext) hoare_lift_modifies':
  assumes deriv: "∀σ. Γ,{}⊨_F {σ} c (Modif σ),(ModifAbr σ)"
  shows "∀σ. (lift_e Γ),{}⊨_F {σ} (lift_c c)
           {T. T ∈ lift_s (Modif (project σ)) ∧
                   (∃T'. T=inject σ T')},
           {T. T ∈ lift_s (ModifAbr (project σ)) ∧
                   (∃T'. T=inject σ T')}"
apply (rule allI)
apply (rule HoarePartialDef.conseq [OF hoare_lift_modifies [OF deriv]])
apply blast
done

subsection ‹Renaming Procedures›

primrec rename:: "('p ==> 'q) ==> ('s,'p,'f) com ==> ('s,'q,'f) com"
where
"rename N Skip = Skip" |
"rename N (Basic f) = Basic f" |
"rename N (Spec r) = Spec r" |
"rename N (Seq c₁ c₂) = (Seq (rename N c₁) (rename N c₂))" |
"rename N (Cond b c₁ c₂) = Cond b (rename N c₁) (rename N c₂)" |
"rename N (While b c) = While b (rename N c)" |
"rename N (Call p) = Call (N p)" |
"rename N (DynCom c) = DynCom (λs. rename N (c s))" |
"rename N (Guard f g c) = Guard f g (rename N c)" |
"rename N Throw = Throw" |
"rename N (Catch c₁ c₂) = Catch (rename N c₁) (rename N c₂)"

lemma rename_Skip: "rename h c = Skip = (c=Skip)"
  by (cases c) auto

lemma rename_Basic:
  "(rename h c = Basic f) = (c=Basic f)"
  by (cases c) auto

lemma rename_Spec:
  "(rename h c = Spec r) = (c=Spec r)"
  by (cases c) auto

lemma rename_Seq:
  "(rename h c = Seq rc₁ rc₂) =
     (∃ c₁ c₂. c = Seq c₁ c₂ ∧
               rc₁ = rename h c₁ ∧ rc₂ = rename h c₂ )"
    by (cases c) auto

lemma rename_Cond:
  "(rename h c = Cond b rc₁ rc₂) =
     (∃c₁ c₂. c = Cond b c₁ c₂ ∧ rc₁ = rename h c₁ ∧ rc₂ = rename h c₂ )"
  by (cases c) auto

lemma rename_While:
  "(rename h c = While b rc') = (∃c'. c = While b c' ∧ rc' = rename h c')"
  by (cases c) auto

lemma rename_Call:
  "(rename h c = Call q) = (∃p. c = Call p ∧ q=h p)"
  by (cases c) auto

lemma rename_DynCom:
  "(rename h c = DynCom rc) = (∃C. c=DynCom C ∧ rc = (λs. rename h (C s)))"
  by (cases c) auto

lemma rename_Guard:
  "(rename h c = Guard f g rc') =
     (∃c'. c = Guard f g c' ∧ rc' = rename h c')"
   by (cases c) auto

lemma rename_Throw:
  "(rename h c = Throw) = (c = Throw)"
  by (cases c) auto

lemma rename_Catch:
  "(rename h c = Catch rc₁ rc₂) =
     (∃c₁ c₂. c = Catch c₁ c₂ ∧ rc₁ = rename h c₁ ∧ rc₂ = rename h c₂ )"
    by (cases c) auto

lemma exec_rename_to_exec:
  assumes Γ: "∀p bdy. Γ p = Some bdy ⟶ Γ' (h p) = Some (rename h bdy)"
  assumes exec: "Γ'⊨⟨rc,s⟩ ==> t"
  shows "∧c. rename h c = rc==> ∃t'. Γ⊨⟨c,s⟩ ==> t' ∧ (t'=Stuck ∨ t'=t)"
using exec
proof (induct)
  case Skip thus ?case by (fastforce intro: exec.intros simp add: rename_Skip)
next
  case Guard thus ?case by (fastforce intro: exec.intros simp add: rename_Guard)
next
  case GuardFault thus ?case by (fastforce intro: exec.intros simp add: rename_Guard)
next
  case FaultProp thus ?case by (fastforce intro: exec.intros)
next
  case Basic thus ?case by (fastforce intro: exec.intros simp add: rename_Basic)
next
  case Spec thus ?case by (fastforce intro: exec.intros simp add: rename_Spec)
next
  case SpecStuck thus ?case by (fastforce intro: exec.intros simp add: rename_Spec)
next
  case Seq thus ?case by (fastforce intro: exec.intros simp add: rename_Seq)
next
  case CondTrue thus ?case by (fastforce intro: exec.intros simp add: rename_Cond)
next
  case CondFalse thus ?case by (fastforce intro: exec.intros simp add: rename_Cond)
next
  case WhileTrue thus ?case by (fastforce intro: exec.intros simp add: rename_While)
next
  case WhileFalse thus ?case by (fastforce intro: exec.intros simp add: rename_While)
next
  case (Call p rbdy s t)
  have rbdy: "Γ' p = Some rbdy" by fact
  have "rename h c = Call p" by fact
  then obtain q where c: "c=Call q" and p: "p=h q"
    by (auto simp add: rename_Call)
  show ?case
  proof (cases "Γ q")
    case None
    with c show ?thesis by (auto intro: exec.CallUndefined)
  next
    case (Some bdy)
    from Γ [rule_format, OF this] p rbdy
    have "rename h bdy = rbdy" by simp
    with Call.hyps c Some
    show ?thesis
      by (fastforce intro: exec.intros)
  qed
next
  case (CallUndefined p s)
  have undef: "Γ' p = None" by fact
  have "rename h c = Call p" by fact
  then obtain q where c: "c=Call q" and p: "p=h q"
    by (auto simp add: rename_Call)
  from undef p Γ have "Γ q = None"
    by (cases "Γ q") auto
  with p c show ?case
    by (auto intro: exec.intros)
next
  case StuckProp thus ?case by (fastforce intro: exec.intros)
next
  case DynCom thus ?case by (fastforce intro: exec.intros simp add: rename_DynCom)
next
  case Throw thus ?case by (fastforce intro: exec.intros simp add: rename_Throw)
next
  case AbruptProp thus ?case by (fastforce intro: exec.intros)
next
  case CatchMatch thus ?case by (fastforce intro: exec.intros simp add: rename_Catch)
next
  case CatchMiss thus ?case by (fastforce intro: exec.intros simp add: rename_Catch)
qed



lemma exec_rename_to_exec':
  assumes Γ: "∀p bdy. Γ p = Some bdy ⟶ Γ' (N p) = Some (rename N bdy)"
  assumes exec: "Γ'⊨⟨rename N c,s⟩ ==> t"
  shows "∃t'. Γ⊨⟨c,s⟩ ==> t' ∧ (t'=Stuck ∨ t'=t)"
  using exec_rename_to_exec [OF Γ exec]
  by  auto



lemma valid_to_valid_rename:
  assumes Γ: "∀p bdy. Γ p = Some bdy ⟶ Γ' (N p) = Some (rename N bdy)"
  assumes valid: "Γ⊨_F P c Q,A"
  shows "Γ'⊨_F P (rename N c) Q,A"
proof (rule validI)
  fix s t
  assume execr: "Γ'⊨ ⟨rename N c,Normal s⟩ ==> t"
  assume P: "s ∈ P"
  assume noFault: "t ∉ Fault ` F"
  show "t ∈ Normal ` Q ∪ Abrupt ` A"
  proof -
    from exec_rename_to_exec [OF Γ execr]
    obtain t' where
      exec: "Γ⊨ ⟨c,Normal s⟩ ==> t'"  and t': "(t' = Stuck ∨ t' = t)"
      by auto
    with valid noFault P show ?thesis
      by (auto simp add: valid_def)
  qed
qed

lemma hoare_to_hoare_rename:
  assumes Γ: "∀p bdy. Γ p = Some bdy ⟶ Γ' (N p) = Some (rename N bdy)"
  assumes deriv: "Γ,{}⊨_F P c Q,A"
  shows "Γ',{}⊨_F P (rename N c) Q,A"
apply (rule hoare_complete)
apply (insert hoare_sound [OF deriv])
apply (rule valid_to_valid_rename)
apply  (rule Γ)
apply (simp add: cvalid_def)
done

lemma hoare_to_hoare_rename':
  assumes Γ: "∀p bdy. Γ p = Some bdy ⟶ Γ' (N p) = Some (rename N bdy)"
  assumes deriv: "∀Z. Γ,{}⊨_F (P Z) c (Q Z),(A Z)"
  shows "∀Z. Γ',{}⊨_F (P Z) (rename N c) (Q Z),(A Z)"
apply rule
apply (rule hoare_to_hoare_rename [OF Γ])
apply (rule deriv[rule_format])
done

lemma terminates_to_terminates_rename:
  assumes Γ: "∀p bdy. Γ p = Some bdy ⟶ Γ' (N p) = Some (rename N bdy)"
  assumes termi: "Γ⊨ c ↓ s"
  assumes noStuck: "Γ⊨ ⟨c,s⟩ ==>∉{Stuck}"
  shows "Γ'⊨ rename N c ↓ s"
using termi noStuck
proof (induct)
  case Skip thus ?case by (fastforce intro: terminates.intros)
next
  case Basic thus ?case by (fastforce intro: terminates.intros)
next
  case Spec thus ?case by (fastforce intro: terminates.intros)
next
  case Guard thus ?case by (fastforce intro: terminates.intros
    simp add: final_notin_def exec.intros)
next
  case GuardFault thus ?case by (fastforce intro: terminates.intros)
next
  case Fault thus ?case by (fastforce intro: terminates.intros)
next
  case Seq
  thus ?case
    by (force intro!: terminates.intros exec.intros dest: exec_rename_to_exec [OF Γ]
         simp add: final_notin_def)
next
  case CondTrue thus ?case by (fastforce intro: terminates.intros
    simp add: final_notin_def exec.intros)
next
  case CondFalse thus ?case by (fastforce intro: terminates.intros
    simp add: final_notin_def exec.intros)
next
  case (WhileTrue s b c)
  have s_in_b: "s ∈ b" by fact
  have noStuck: "Γ⊨ ⟨While b c,Normal s⟩ ==>∉{Stuck}" by fact
  with s_in_b have "Γ⊨ ⟨c,Normal s⟩ ==>∉{Stuck}"
    by (auto simp add: final_notin_def intro: exec.intros)
  with WhileTrue.hyps have "Γ'⊨rename N c ↓ Normal s"
    by simp
  moreover
  {
    fix t
    assume exec_rc: "Γ'⊨ ⟨rename N c,Normal s⟩ ==> t"
    have "Γ'⊨ While b (rename N c) ↓ t"
    proof -
      from exec_rename_to_exec [OF Γ exec_rc] obtain t'
        where exec_c: "Γ⊨ ⟨c,Normal s⟩ ==> t'" and t': "(t' = Stuck ∨ t' = t)"
        by auto
      with s_in_b noStuck obtain "t'=t" and "Γ⊨ ⟨While b c,t⟩ ==>∉{Stuck}"
        by (auto simp add: final_notin_def intro: exec.intros)
      with exec_c WhileTrue.hyps
      show ?thesis
        by auto
    qed
  }
  ultimately show ?case
    using s_in_b
    by (auto intro: terminates.intros)
next
  case WhileFalse thus ?case by (fastforce intro: terminates.intros)
next
  case (Call p bdy s)
  have "Γ p = Some bdy" by fact
  from Γ [rule_format, OF this]
  have bdy': "Γ' (N p) = Some (rename N bdy)".
  from Call have "Γ'⊨rename N bdy ↓ Normal s"
    by (auto simp add: final_notin_def intro: exec.intros)
  with bdy' have "Γ'⊨Call (N p) ↓ Normal s"
    by (auto intro: terminates.intros)
  thus ?case by simp
next
  case (CallUndefined p s)
  have "Γ p = None" "Γ⊨ ⟨Call p,Normal s⟩ ==>∉{Stuck}" by fact+
  hence False by (auto simp add: final_notin_def intro: exec.intros)
  thus ?case ..
next
  case Stuck thus ?case by (fastforce intro: terminates.intros)
next
  case DynCom thus ?case by (fastforce intro: terminates.intros
    simp add: final_notin_def exec.intros)
next
  case Throw thus ?case by (fastforce intro: terminates.intros)
next
  case Abrupt thus ?case by (fastforce intro: terminates.intros)
next
  case (Catch c1 s c2)
  have noStuck: "Γ⊨ ⟨Catch c1 c2,Normal s⟩ ==>∉{Stuck}" by fact
  hence "Γ⊨ ⟨c1,Normal s⟩ ==>∉{Stuck}"
    by (fastforce simp add: final_notin_def intro: exec.intros)
  with Catch.hyps have "Γ'⊨rename N c1 ↓ Normal s"
    by auto
  moreover
  {
    fix t
    assume exec_rc1:"Γ'⊨ ⟨rename N c1,Normal s⟩ ==> Abrupt t"
    have "Γ'⊨rename N c2 ↓ Normal t"
    proof -
      from exec_rename_to_exec [OF Γ exec_rc1] obtain t'
        where exec_c: "Γ⊨ ⟨c1,Normal s⟩ ==> t'" and "(t' = Stuck ∨ t' = Abrupt t)"
        by auto
      with noStuck have t': "t'=Abrupt t"
        by (fastforce simp add: final_notin_def intro: exec.intros)
      with exec_c noStuck have "Γ⊨ ⟨c2,Normal t⟩ ==>∉{Stuck}"
        by (auto simp add: final_notin_def intro: exec.intros)
      with exec_c t' Catch.hyps
      show ?thesis
        by auto
    qed
  }
  ultimately show ?case
    by (auto intro: terminates.intros)
qed

lemma validt_to_validt_rename:
  assumes Γ: "∀p bdy. Γ p = Some bdy ⟶ Γ' (N p) = Some (rename N bdy)"
  assumes valid: "Γ⊨_tF P c Q,A"
  shows "Γ'⊨_tF P (rename N c) Q,A"
proof -
  from valid
  have "Γ'⊨_F P (rename N c) Q,A"
    by (auto intro: valid_to_valid_rename [OF Γ] simp add: validt_def)
  moreover
  {
    fix s
    assume "s ∈ P"
    with valid obtain "Γ⊨c ↓ (Normal s)" "Γ⊨ ⟨c,Normal s⟩ ==>∉{Stuck}"
      by (auto simp add: validt_def valid_def final_notin_def)
    from terminates_to_terminates_rename [OF Γ this]
    have "Γ'⊨rename N c ↓ Normal s"
      .
  }
  ultimately show ?thesis
    by (simp add: validt_def)
qed

lemma hoaret_to_hoaret_rename:
  assumes Γ: "∀p bdy. Γ p = Some bdy ⟶ Γ' (N p) = Some (rename N bdy)"
  assumes deriv: "Γ,{}⊨_tF P c Q,A"
  shows "Γ',{}⊨_tF P (rename N c) Q,A"
apply (rule hoaret_complete)
apply (insert hoaret_sound [OF deriv])
apply (rule validt_to_validt_rename)
apply  (rule Γ)
apply (simp add: cvalidt_def)
done

lemma hoaret_to_hoaret_rename':
  assumes Γ: "∀p bdy. Γ p = Some bdy ⟶ Γ' (N p) = Some (rename N bdy)"
  assumes deriv: "∀Z. Γ,{}⊨_tF (P Z) c (Q Z),(A Z)"
  shows "∀Z. Γ',{}⊨_tF (P Z) (rename N c) (Q Z),(A Z)"
apply rule
apply (rule hoaret_to_hoaret_rename [OF Γ])
apply (rule deriv[rule_format])
done

lemma lift_{c_whileAnno} [simp]: "lift_c prj inject (whileAnno b I V c) =
    whileAnno (lift_s prj b)
              (lift_s prj I) (lift_r prj inject V) (lift_c prj inject c)"
  by (simp add: whileAnno_def)

lemma lift_{c_block} [simp]: "lift_c prj inject (block init bdy return c) =
  block (lift_f prj inject init) (lift_c prj inject bdy)
        (λs. (lift_f prj inject (return (prj s))))
        (λs t. lift_c prj inject (c (prj s) (prj t)))"
  by (simp add: block_def block_exn_def)

(*
lemma lift\<^sub>c_block [simp]: "lift\<^sub>c prj inject (block init bdy return c) =
  block (lift\<^sub>f prj inject init) (lift\<^sub>c prj inject bdy)
        (\<lambda>s t. inject s (return (prj s) (prj t)))
        (\<lambda>s t. lift\<^sub>c prj inject (c (prj s) (prj t)))"
  apply (simp add: block_def)
  apply (simp add: lift\<^sub>f_def)
*)
lemma lift_{c_call} [simp]: "lift_c prj inject (call init p return c) =
  call (lift_f prj inject init) p
        (λs. (lift_f prj inject (return (prj s))))
        (λs t. lift_c prj inject (c (prj s) (prj t)))"
  by (simp add: call_def lift_{c_block})

lemma rename_whileAnno [simp]: "rename h (whileAnno b I V c) =
   whileAnno b I V (rename h c)"
  by (simp add: whileAnno_def)

lemma rename_block [simp]: "rename h (block init bdy return c) =
  block init (rename h bdy) return (λs t. rename h (c s t))"
  by (simp add: block_def block_exn_def)

lemma rename_call [simp]: "rename h (call init p return c) =
  call init (h p) return (λs t. rename h (c s t))"
  by (simp add: call_def)


end