Theory Compose

(*
    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 ‹
We develop some theory to support state-space modular development of programs.
These experiments aim at the representation of state-spaces with records.
If 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⇩1 c⇩2)  =
  (Seq (lift⇩c prj inject c⇩1) (lift⇩c prj inject c⇩2))" |
"lift⇩c prj inject (Cond b c⇩1 c⇩2) =
  Cond (lift⇩s prj b) (lift⇩c prj inject c⇩1) (lift⇩c prj inject c⇩2)" |
"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⇩1 c⇩2) =
  Catch (lift⇩c prj inject c⇩1) (lift⇩c prj inject c⇩2)"



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⇩1 lc⇩2) =
     (∃ c⇩1 c⇩2. c = Seq c⇩1 c⇩2 ∧
               lc⇩1 = lift⇩c prj inject c⇩1 ∧ lc⇩2 = lift⇩c prj inject c⇩2 )"
    by (cases c) auto

lemma lift⇩c_Cond:
  "(lift⇩c prj inject c = Cond lb lc⇩1 lc⇩2) =
     (∃b c⇩1 c⇩2. c = Cond b c⇩1 c⇩2 ∧ lb = lift⇩s prj b ∧
                lc⇩1 = lift⇩c prj inject c⇩1 ∧ lc⇩2 = lift⇩c prj inject c⇩2 )"
  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⇩1 lc⇩2) =
     (∃ c⇩1 c⇩2. c = Catch c⇩1 c⇩2 ∧
               lc⇩1 = lift⇩c prj inject c⇩1 ∧ lc⇩2 = lift⇩c prj inject c⇩2 )"
    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⇩f_simp  = Compose.lift⇩f_def
 [of project "inject", folded lift⇩f_def]
lemmas (in lift_state_space) lift⇩s_simp  = Compose.lift⇩s_def
 [of project, folded lift⇩s_def]
lemmas (in lift_state_space) lift⇩r_simp  = Compose.lift⇩r_def
 [of project "inject", folded lift⇩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⇩1 c⇩2)  =
  (Seq (lift⇩c c⇩1) (lift⇩c c⇩2))"
  by (simp add: lift⇩c_def)
lemma (in lift_state_space) lift⇩c_Cond_simp [simp]:
"lift⇩c (Cond b c⇩1 c⇩2) =
  Cond (lift⇩s b) (lift⇩c c⇩1) (lift⇩c c⇩2)"
  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⇩1 c⇩2) =
  Catch (lift⇩c c⇩1) (lift⇩c c⇩2)"
  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 ‹
The problem is that @{term "(lift⇩c project inject ∘ Γ)"} is quite
a strong premise. The problem is that @{term "Γ"} is a function here.
A map would be better. We only have to lift those procedures in the domain
of @{term "Γ"}:
‹Γ p = Some bdy ⟶ Γ' p = Some lift⇩c project inject bdy›.
We then can com up with theorems that allow us to extend the domains
of @{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⇩1 s t c⇩2 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⇩s A"
  proof -
    from lexec
    have "Γ⊢ ⟨c,project⇩x (Normal s)⟩ ⇒ (project⇩x t)"
      by (rule lift_exec) (simp_all)
    moreover
    from lP have "project s ∈ P"
      by (simp add: lift⇩s_def Compose.lift⇩s_def project⇩x_def)
    ultimately
    have "project⇩x 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: "Γ⊨⇩t⇘/F⇙ P c Q,A"
  shows "(lift⇩e Γ)⊨⇩t⇘/F⇙ (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: "Γ,{}⊢⇩t⇘/F⇙ P c Q,A"
  shows
   "(lift⇩e Γ),{}⊢⇩t⇘/F⇙ (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"


(* ∃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⇩c_Guard lift⇩c_def)
next
  case GuardFault thus ?case
    by simp
next
  case FaultProp thus ?case by simp
next
  case Basic thus ?case
    by (clarsimp simp add: lift⇩f_def Compose.lift⇩f_def
        proj_inj_commute lift⇩c_Basic lift⇩c_def)
next
  case (Spec r) thus ?case
    by (clarsimp simp add: Compose.lift⇩r_def lift⇩c_Spec lift⇩c_def)
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⇩c c = While lb lc'" by fact
  then obtain b c' where
    c: "c = While b c'" and
    lb: "lb = lift⇩s b" and
    lc: "lc' = lift⇩c c'"
    by (auto simp add: lift⇩c_While lift⇩s_def lift⇩c_def)
  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⇩c_While inj_proj_commute)
next
  case Call thus ?case
    by (clarsimp simp add: inject_last lift⇩c_Call lift⇩e_def lift⇩c_def)
next
  case CallUndefined thus ?case by simp
next
  case StuckProp thus ?case by simp
next
  case DynCom
  thus ?case
    by (clarsimp simp add: lift⇩c_DynCom lift⇩c_def)
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⇩e Γ⊨⇘/F⇙ {σ} lift⇩c c
                {t. t=inject σ (project t)}, {t. t=inject σ (project t)}"
proof (rule validI)
  fix s t
  assume exec: "lift⇩e Γ⊢⟨lift⇩c 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⇩s (ModifAbr (project S)).
                  t = inject S (project t)}"
  proof -
    from lift_exec [OF exec]
    have "Γ⊢ ⟨c,project⇩x (Normal s)⟩ ⇒ project⇩x t"
      by auto
    moreover
    from noFault have "project⇩x 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⇩s (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⇩1 c⇩2)  = (Seq (rename N c⇩1) (rename N c⇩2))" |
"rename N (Cond b c⇩1 c⇩2) = Cond b (rename N c⇩1) (rename N c⇩2)" |
"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⇩1 c⇩2) = Catch (rename N c⇩1) (rename N c⇩2)"

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⇩1 rc⇩2) =
     (∃ c⇩1 c⇩2. c = Seq c⇩1 c⇩2 ∧
               rc⇩1 = rename h c⇩1 ∧ rc⇩2 = rename h c⇩2 )"
    by (cases c) auto

lemma rename_Cond:
  "(rename h c = Cond b rc⇩1 rc⇩2) =
     (∃c⇩1 c⇩2. c = Cond b c⇩1 c⇩2  ∧ rc⇩1 = rename h c⇩1 ∧ rc⇩2 = rename h c⇩2 )"
  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⇩1 rc⇩2) =
     (∃c⇩1 c⇩2. c = Catch c⇩1 c⇩2 ∧ rc⇩1 = rename h c⇩1 ∧ rc⇩2 = rename h c⇩2 )"
    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: "Γ⊨⇩t⇘/F⇙ P c Q,A"
  shows "Γ'⊨⇩t⇘/F⇙ 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: "Γ,{}⊢⇩t⇘/F⇙ P c Q,A"
  shows "Γ',{}⊢⇩t⇘/F⇙ 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. Γ,{}⊢⇩t⇘/F⇙ (P Z) c (Q Z),(A Z)"
  shows "∀Z. Γ',{}⊢⇩t⇘/F⇙ (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⇩c_block [simp]: "lift⇩c prj inject (block init bdy return c) =
  block (lift⇩f prj inject init) (lift⇩c prj inject bdy)
        (λs t. inject s (return (prj s) (prj t)))
        (λs t. lift⇩c prj inject (c (prj s) (prj t)))"
  apply (simp add: block_def)
  apply (simp add: lift⇩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