Theory Uniform_Renaming

theory "Uniform_Renaming" 
imports
  Ordinary_Differential_Equations.ODE_Analysis
  "Ids"
  "Lib"
  "Syntax"
  "Denotational_Semantics"
  "Frechet_Correctness"
  "Static_Semantics"
  "Coincidence"
  "Bound_Effect"
begin context ids begin

section ‹Uniform and Bound Renaming›
text ‹Definitions and soundness proofs for the renaming rules Uniform Renaming and Bound Renaming.
Renaming in dL swaps the names of two variables x and y, as in the swap operator of Nominal Logic.
›
fun swap ::"'sz ⇒ 'sz ⇒ 'sz ⇒ 'sz"
where "swap x y z = (if z = x then  y else if z = y then x else z)"
 
subsection ‹Uniform Renaming Definitions›

primrec TUrename :: "'sz ⇒ 'sz ⇒ ('sf, 'sz) trm ⇒ ('sf, 'sz) trm"
where 
  "TUrename x y (Var z) = Var (swap x y z)"
| "TUrename x y (DiffVar z) = DiffVar (swap x y z)"
| "TUrename x y (Const r) = (Const r)"
| "TUrename x y (Function f args) = Function f (λi. TUrename x y (args i))"
| "TUrename x y (Plus θ1 θ2) = Plus (TUrename x y θ1) (TUrename x y θ2)"
| "TUrename x y (Times θ1 θ2) = Times (TUrename x y θ1) (TUrename x y θ2)"
| "TUrename x y (Differential θ) = Differential (TUrename x y θ)"
  
primrec OUrename :: "'sz ⇒ 'sz ⇒ ('sf, 'sz) ODE ⇒ ('sf, 'sz) ODE"
where
  "OUrename x y (OVar c) = undefined"
| "OUrename x y (OSing z θ) = OSing (swap x y z) (TUrename x y θ)"
| "OUrename x y (OProd ODE1 ODE2) = OProd (OUrename x y ODE1) (OUrename x y ODE2)"
  
inductive ORadmit :: "('sf, 'sz) ODE ⇒ bool"
where
  ORadmit_Sing:"ORadmit (OSing x θ)"
| ORadmit_Prod:"ORadmit ODE1 ⟹ ORadmit ODE2 ⟹ ORadmit (OProd ODE1 ODE2)"
  
primrec PUrename :: "'sz ⇒ 'sz ⇒ ('sf, 'sc, 'sz) hp ⇒ ('sf, 'sc, 'sz) hp"
  and   FUrename :: "'sz ⇒ 'sz ⇒ ('sf, 'sc, 'sz) formula ⇒ ('sf, 'sc, 'sz) formula"
where
  "PUrename x y (Pvar a) = undefined"
| "PUrename x y (Assign z θ) = Assign (swap x y z) (TUrename x y θ)"
| "PUrename x y (DiffAssign z θ) = DiffAssign (swap x y z) (TUrename x y θ)"
| "PUrename x y (Test φ) = Test (FUrename x y φ)"
| "PUrename x y (EvolveODE ODE φ) = EvolveODE (OUrename x y ODE) (FUrename x y φ)"
| "PUrename x y (Choice a b) = Choice (PUrename x y a) (PUrename x y b)"
| "PUrename x y (Sequence a b) = Sequence (PUrename x y a) (PUrename x y b)"
| "PUrename x y (Loop a) = Loop (PUrename x y a)"

| "FUrename x y (Geq θ1 θ2) = Geq (TUrename x y θ1) (TUrename x y θ2)"
| "FUrename x y (Prop p args) = Prop p (λi. TUrename x y (args i))"
| "FUrename x y (Not φ) = Not (FUrename x y φ)"
| "FUrename x y (And φ ψ) = And (FUrename x y φ) (FUrename x y ψ)"
| "FUrename x y (Exists z φ) = Exists (swap x y z) (FUrename x y φ)"
| "FUrename x y (Diamond α φ) = Diamond (PUrename x y α) (FUrename x y φ)"
| "FUrename x y (InContext C φ) = undefined"

subsection ‹Uniform Renaming Admissibility›

inductive PRadmit :: "('sf, 'sc, 'sz) hp ⇒ bool"
  and     FRadmit ::"('sf, 'sc, 'sz) formula ⇒ bool"
where
  PRadmit_Assign:"PRadmit (Assign x θ)"
| PRadmit_DiffAssign:"PRadmit (DiffAssign x θ)"
| PRadmit_Test:"FRadmit φ ⟹ PRadmit (Test φ)"
| PRadmit_EvolveODE:"ORadmit ODE ⟹ FRadmit φ ⟹ PRadmit (EvolveODE ODE φ)"
| PRadmit_Choice:"PRadmit a ⟹ PRadmit b ⟹ PRadmit (Choice a b)"
| PRadmit_Sequence:"PRadmit a ⟹ PRadmit b ⟹ PRadmit (Sequence a b)"
| PRadmit_Loop:"PRadmit a ⟹ PRadmit (Loop a)"

| FRadmit_Geq:"FRadmit (Geq θ1 θ2)"
| FRadmit_Prop:"FRadmit (Prop p args)"
| FRadmit_Not:"FRadmit φ ⟹ FRadmit (Not φ)"
| FRadmit_And:"FRadmit φ ⟹ FRadmit ψ ⟹ FRadmit (And φ ψ)"
| FRadmit_Exists:"FRadmit φ ⟹ FRadmit (Exists x φ)"
| FRadmit_Diamond:"PRadmit α ⟹ FRadmit φ ⟹ FRadmit (Diamond α φ)"

inductive_simps
    FRadmit_box_simps[simp]: "FRadmit (Box a f)"
and PRadmit_box_simps[simp]: "PRadmit (Assign x e)"

definition RSadj :: "'sz ⇒ 'sz ⇒ 'sz simple_state ⇒ 'sz simple_state"
where "RSadj x y ν = (χ z. ν $ (swap x y z))" 

definition Radj :: "'sz ⇒ 'sz ⇒ 'sz state ⇒ 'sz state"
where "Radj x y ν = (RSadj x y (fst ν), RSadj x y (snd ν))" 

lemma SUren: "sterm_sem I (TUrename x y θ) ν = sterm_sem I θ (RSadj x y ν)"
  by (induction θ, auto simp add: RSadj_def)

lemma ren_preserves_dfree:"dfree θ ⟹ dfree (TUrename x y θ)"
  by(induction rule: dfree.induct, auto intro: dfree.intros)

subsection ‹Uniform Renaming Soundness Proof and Lemmas›

lemma TUren_frechet:
  assumes good_interp:"is_interp I"
  shows "dfree θ ⟹ frechet I (TUrename x y θ) ν ν' = frechet I θ (RSadj x y ν) (RSadj x y ν')"
proof (induction rule: dfree.induct)
  ― ‹There's got to be a more elegant proof of this...›
  case (dfree_Var i)
  then show ?case 
    unfolding RSadj_def apply auto 
       subgoal by (metis vec_lambda_eta)
      subgoal
      proof (auto simp add: axis_def)
        assume yx:"y ≠ x"
        have a:"(χ z. ν' $ (if z = x then y else if z = y then x else z)) $ y = ν' $ x"
         by simp
       show "ν' ∙ (χ i. if i = x then 1 else 0) 
                 = (χ z. ν' $ (if z = x then y else if z = y then x else z)) ∙ (χ i. if i = y then 1 else 0)"
         by (metis (no_types) a axis_def inner_axis)
      qed
     subgoal
     proof -
       have "⋀v s. v ∙ (χ sa. if sa = (s::'sz) then 1 else 0) = v $ s"
         subgoal for v s
           using inner_axis[of v s 1]
           by (auto simp add: axis_def)
         done
       then show ?thesis
         by (auto simp add: axis_def)
     qed
    subgoal
    proof -
      assume a1: "i ≠ y"
      assume a2: "i ≠ x"
      have "⋀v s. v ∙ (χ sa. if sa = (s::'sz) then 1 else 0) = v $ s"
        by (metis (no_types) inner_axis axis_def inner_prod_eq)
      then show ?thesis
        using a2 a1 by (auto simp add: axis_def)
    qed
    done 
qed (auto simp add: SUren good_interp is_interp_def)

lemma RSadj_fst:"RSadj x y (fst ν) = fst (Radj x y ν)"
  unfolding RSadj_def Radj_def by auto

lemma RSadj_snd:"RSadj x y (snd ν) = snd (Radj x y ν)"
  unfolding RSadj_def Radj_def by auto

lemma TUren:
  assumes good_interp:"is_interp I"
  shows "dsafe θ ⟹ dterm_sem I (TUrename x y θ) ν = dterm_sem I θ (Radj x y ν)"
proof (induction rule: dsafe.induct)
  case (dsafe_Diff θ)
  assume free:"dfree θ"
  show ?case 
    apply (auto simp add: directional_derivative_def)
    using TUren_frechet[OF good_interp free, of x y "fst ν" "snd ν"]
     by (auto simp add: RSadj_fst RSadj_snd)
qed (auto simp add: Radj_def RSadj_def)

lemma adj_sum:"RSadj x y (ν1 + ν2) = (RSadj x y ν1) + (RSadj x y ν2)"
  unfolding RSadj_def apply auto apply (rule vec_extensionality)
  subgoal for i
    apply (cases "i = x")
     apply (cases "i = y")
      by auto
  done

lemma OUren: "ORadmit ODE ⟹ ODE_sem I (OUrename x y ODE) ν = RSadj x y (ODE_sem I ODE (RSadj x y ν))"
proof (induction rule: ORadmit.induct)
  case (ORadmit_Prod ODE1 ODE2)
  then show ?case 
    using adj_sum by auto
next
  case (ORadmit_Sing z θ)
  then show ?case 
    by (rule vec_extensionality | auto simp add: SUren RSadj_def)+   
qed

lemma state_eq: 
  fixes ν ν' :: "'sz state"
  shows "(⋀i. (fst ν) $ i = (fst ν') $ i) ⟹ (⋀i. (snd ν) $ i = (snd ν') $ i) ⟹ ν  = ν'"
  apply (cases "ν", cases "ν'", auto)
   by(rule vec_extensionality, auto)+
  
lemma Radj_repv1:
  fixes x y z ::"'sz" 
  shows "(Radj x y (repv ν y r)) = repv (Radj x y ν) x r"
  apply(rule state_eq)
   subgoal for i
     apply(cases "i = x") apply (cases "i = y") 
       unfolding Radj_def RSadj_def by auto
  subgoal for i
    apply(cases "i = x") apply (cases "i = y") 
      unfolding Radj_def RSadj_def by auto
  done

lemma Radj_repv2:
  fixes x y z ::"'sz" 
  shows "(Radj x y (repv ν x r)) = repv (Radj x y ν) y r"
  apply(rule state_eq)
   subgoal for i
     apply(cases "i = x") apply (cases "i = y") 
       unfolding Radj_def RSadj_def by auto
  subgoal for i
    apply(cases "i = x") apply (cases "i = y") 
      unfolding Radj_def RSadj_def by auto
  done

lemma Radj_repv3:
  fixes x y z ::"'sz" 
  assumes zx:"z ≠ x" and zy:"z ≠ y"
  shows "(Radj x y (repv ν z r)) = repv (Radj x y ν) z r"
  apply(rule state_eq)
   subgoal for i
     apply(cases "i = x") apply (cases "i = y") 
       using zx zy unfolding Radj_def RSadj_def by auto
  subgoal for i
    apply(cases "i = x") apply (cases "i = y") 
      using zx zy unfolding Radj_def RSadj_def by auto
  done

lemma Radj_repd1:
  fixes x y z ::"'sz" 
  shows "(Radj x y (repd ν y r)) = repd (Radj x y ν) x r"
  apply(rule state_eq)
   subgoal for i
     apply(cases "i = x") apply (cases "i = y") 
       unfolding Radj_def RSadj_def by auto
  subgoal for i
    apply(cases "i = x") apply (cases "i = y") 
      unfolding Radj_def RSadj_def by auto
  done

lemma Radj_repd2:
  fixes x y z ::"'sz" 
  shows "(Radj x y (repd ν x r)) = repd (Radj x y ν) y r"
  apply(rule state_eq)
   subgoal for i
     apply(cases "i = x") apply (cases "i = y") 
       unfolding Radj_def RSadj_def by auto
  subgoal for i
    apply(cases "i = x") apply (cases "i = y") 
      unfolding Radj_def RSadj_def by auto
  done

lemma Radj_repd3:
  fixes x y z ::"'sz" 
  assumes zx:"z ≠ x" and zy:"z ≠ y"
  shows "(Radj x y (repd ν z r)) = repd (Radj x y ν) z r"
  apply(rule state_eq)
   subgoal for i
     apply(cases "i = x") apply (cases "i = y")
     using zx zy unfolding Radj_def RSadj_def by auto
  subgoal for i
    apply(cases "i = x") apply (cases "i = y") 
    using zx zy unfolding Radj_def RSadj_def by auto
  done

― ‹i.e. shows ‹Radj x y› is a bijection for all ‹x y››
lemma Radj_eq_iff:"(a = b) = ((Radj x y a) = (Radj x y b))"
  unfolding Radj_def RSadj_def apply auto
  apply (rule state_eq)
   apply (smt (verit))+
  done

lemma RSadj_cancel:"RSadj x y (RSadj x y ν) = ν"
  unfolding RSadj_def apply auto
  apply(rule vec_extensionality)
  by(auto)

lemma Radj_cancel:"Radj x y (Radj x y ν) = ν"
  unfolding Radj_def RSadj_def apply auto
  apply(rule state_eq)
   subgoal for i by(cases "i = x", cases "i = y", auto)
  subgoal for i by(cases "i = x", cases "i = y", auto)
  done

lemma OUrename_preserves_ODE_vars:"ORadmit ODE ⟹ {z. (swap x y z) ∈ ODE_vars I ODE} = ODE_vars I (OUrename x y ODE)"
  apply(induction rule: ORadmit.induct)
   subgoal for xa θ by auto
  subgoal for ODE1 ODE2
  proof -
    assume IH1:"{z. swap x y z ∈ ODE_vars I ODE1} = ODE_vars I (OUrename x y ODE1)"
    assume IH2:"{z. swap x y z ∈ ODE_vars I ODE2} = ODE_vars I (OUrename x y ODE2)"
    have "{z. swap x y z ∈ ODE_vars I (OProd ODE1 ODE2)} =
          {z. swap x y z ∈ (ODE_vars I ODE1 ∪ ODE_vars I ODE2)}" by auto
    moreover have "... = {z. swap x y z ∈ (ODE_vars I ODE1)} ∪ {z. swap x y z ∈ (ODE_vars I ODE2)}" by auto
    moreover have "... = ODE_vars I (OUrename x y ODE1) ∪ ODE_vars I (OUrename x y ODE2)" using IH1 IH2 by auto
    moreover have "... = ODE_vars I (OUrename x y (OProd ODE1 ODE2))" by auto
    ultimately show "{z. swap x y z ∈ ODE_vars I (OProd ODE1 ODE2)} = ODE_vars I (OUrename x y (OProd ODE1 ODE2))"
      by blast
  qed
  done

lemma ren_proj:"(RSadj x y a) $ z = a $ (swap x y z)"
  unfolding RSadj_def by simp

lemma swap_cancel:"swap x y (swap x y z) = z"
  by auto

lemma mkv_lemma:
  assumes ORA:"ORadmit ODE"
  shows "Radj x y (mk_v I (OUrename x y ODE) (a, b) c) = mk_v I ODE (RSadj x y a, RSadj x y b) (RSadj x y c)"
proof -
  have inner1:"(mk_v I (OUrename x y ODE) (a, b) c) = ((χ i. (if i ∈ ODE_vars I (OUrename x y ODE) then c else a) $ i), (χ i. (if i ∈ ODE_vars I (OUrename x y ODE) then ODE_sem I (OUrename x y ODE) c else b) $ i))"
    using mk_v_concrete[of I "OUrename x y ODE" "(a,b)" c] by auto
  have inner2:"(((χ i. (if i ∈ ODE_vars I (OUrename x y ODE) then c else a) $ i), (χ i. (if i ∈ ODE_vars I (OUrename x y ODE) then ODE_sem I (OUrename x y ODE) c else b) $ i))) 
            = (((χ i. (if (swap x y i) ∈ ODE_vars I ODE then c else a) $ i), (χ i. (if (swap x y i) ∈ ODE_vars I ODE then ODE_sem I (OUrename x y ODE) c else b) $ i)))"
    by (force simp: OUrename_preserves_ODE_vars[OF ORA, symmetric])
  have "Radj x y (mk_v I (OUrename x y ODE) (a, b) c) = 
        Radj x y (((χ i. (if i ∈ ODE_vars I (OUrename x y ODE) then c else a) $ i), (χ i. (if i ∈ ODE_vars I (OUrename x y ODE) then ODE_sem I (OUrename x y ODE) c else b) $ i)))"
    using inner1 by auto
  moreover have "... = Radj x y (((χ i. (if (swap x y i) ∈ ODE_vars I ODE then c else a) $ i), 
                              (χ i. (if (swap x y i) ∈ ODE_vars I ODE then ODE_sem I (OUrename x y ODE) c else b) $ i)))"
    using inner2 by auto
  moreover have "... = (((χ i. (if (swap x y (swap x y i)) ∈ ODE_vars I ODE then c else a) $ (swap x y i))),
                         (χ i. (if (swap x y (swap x y i)) ∈ ODE_vars I ODE then ODE_sem I (OUrename x y ODE) c else b) $ (swap x y i)))"
    unfolding Radj_def RSadj_def by auto
  moreover have "... = (((χ i. (if i ∈ ODE_vars I ODE then c else a) $ (swap x y i))),
                         (χ i. (if i ∈ ODE_vars I ODE then ODE_sem I (OUrename x y ODE) c else b) $ (swap x y i)))"
    using swap_cancel by auto
  moreover have "... = (((χ i. (if i ∈ ODE_vars I ODE then RSadj x y c else RSadj x y a) $ i)),
                         (χ i. (if i ∈ ODE_vars I ODE then RSadj x y (ODE_sem I (OUrename x y ODE) c) else RSadj x y b) $ i))"
     by(auto simp add: ren_proj)
  moreover have "... = (((χ i. (if i ∈ ODE_vars I ODE then RSadj x y c else RSadj x y a) $ i)),
                         (χ i. (if i ∈ ODE_vars I ODE then RSadj x y (RSadj x y (ODE_sem I ODE (RSadj x y c))) else RSadj x y b) $ i))"
    using OUren[OF ORA, of I x y c] by auto
  moreover have "... = (((χ i. (if i ∈ ODE_vars I ODE then RSadj x y c else RSadj x y a) $ i)),
                         (χ i. (if i ∈ ODE_vars I ODE then (ODE_sem I ODE (RSadj x y c)) else RSadj x y b) $ i))"
    by(auto simp add: RSadj_cancel)
  moreover have "... = mk_v I ODE (RSadj x y a, RSadj x y b) (RSadj x y c)"
    using mk_v_concrete[of I "ODE" "(RSadj x y a, RSadj x y b)" "RSadj x y c"]
    by auto
  ultimately show ?thesis by auto
qed

lemma sol_lemma:
  assumes ORA:"ORadmit ODE"
  assumes t:"0 ≤ t"
  assumes fml:"⋀ν. (ν ∈ fml_sem I (FUrename x y φ)) = (Radj x y ν ∈ fml_sem I φ)"
  assumes sol:"(sol solves_ode (λa. ODE_sem I (OUrename x y ODE))) {0..t} {xa. mk_v I (OUrename x y ODE) (sol 0, b) xa ∈ fml_sem I (FUrename x y φ)}"
  shows "((λt. RSadj x y (sol t)) solves_ode (λa. ODE_sem I ODE)) {0..t} {xa. mk_v I ODE (RSadj x y (sol 0), RSadj x y b) xa ∈ fml_sem I φ}"
  apply(unfold solves_ode_def)
  apply(rule conjI)
   defer
   subgoal 
     apply auto
   proof -
     fix s
     assume t:"0 ≤ s" "s ≤ t"
     have ivl:"s ∈ {0..t}" using t by auto
     have "mk_v I (OUrename x y ODE) (sol 0,b) (sol s) ∈ fml_sem I (FUrename x y φ)"
       using solves_odeD(2)[OF sol ivl] by auto
     then have "Radj x y (mk_v I (OUrename x y ODE) (sol 0, b) (sol s)) ∈ fml_sem I φ"
       using fml[of "mk_v I (OUrename x y ODE) (sol 0, b) (sol s)"] by auto
     then show "mk_v I ODE (RSadj x y (sol 0), RSadj x y b) (RSadj x y (sol s)) ∈ fml_sem I φ"
         using mkv_lemma[OF ORA, of x y I "sol 0" b "sol s"] by auto
   qed
   apply (unfold has_vderiv_on_def has_vector_derivative_def)
   proof -
     have "⋀s. s∈{0..t} ⟹  ((λt. RSadj x y (sol t)) has_derivative (λxb. xb *⇩R ODE_sem I ODE (RSadj x y (sol s)))) (at s within {0..t})"
     proof -
       fix s
       assume s:"s ∈{0..t}"
       let ?g = "RSadj x y"
       let ?g' = "RSadj x y"
       let ?f = "sol"
       let ?f' = "(λt'. t' *⇩R ODE_sem I (OUrename x y ODE) (sol s))"
       let ?h = "?g ∘ ?f"
       
       have fun_eq:"(λt'. t' *⇩R ODE_sem I (OUrename x y ODE) (sol s)) = (λt'. t' *⇩R (RSadj x y (ODE_sem I ODE (RSadj x y (sol s)))))"
         apply(rule ext)
         using OUren[OF ORA, of I x y] by simp
       have fun_eq1:"(λν. (χ i. RSadj x y ν $ i)) = RSadj x y"
         by(rule ext, rule vec_extensionality, simp)
       have "s ∈ {0..t} ⟹ (sol has_derivative (λt'. t' *⇩R ODE_sem I (OUrename x y ODE) (sol s))) (at s within {0..t})"
         using solves_odeD(1)[OF sol] unfolding has_vderiv_on_def has_vector_derivative_def by auto
       then have fderiv:"s ∈ {0..t} ⟹ (?f has_derivative ?f') (at s within {0..t})"
         using fun_eq by auto
       have "((λν. (χ i. RSadj x y ν $ i)) has_derivative (λν'. (χ i . RSadj x y ν' $ i))) (at (?f s) within ?f ` {0..t})"
         apply(rule has_derivative_vec)
         apply(auto simp add: RSadj_def intro:derivative_eq_intros)
           by (simp add: has_derivative_at_withinI has_derivative_proj')+
       then have gderiv:"(RSadj x y has_derivative (RSadj x y)) (at (?f s) within ?f ` {0..t})"
         using fun_eq1 by auto
       have hderiv:"(?h has_derivative (?g' ∘ ?f')) (at s within {0..t})"
         by (rule diff_chain_within[OF fderiv gderiv], rule s)
       have heq:"(λt. RSadj x y (sol t)) = ?h"
         unfolding comp_def by simp
       have RSadj_scale:"⋀c a. RSadj x y (c *⇩R RSadj x y a) = c *⇩R a"
         subgoal for c a
           unfolding RSadj_def
           apply auto
           apply(rule vec_extensionality)
           by(auto)
         done
       have heq':"(λxb. xb *⇩R ODE_sem I ODE (RSadj x y (sol s))) = (?g' ∘ ?f')"
         unfolding comp_def apply(rule ext) using OUren[OF ORA, of I x y "sol s"]
         apply auto
         subgoal for c
           using RSadj_scale[of c "ODE_sem I ODE (RSadj x y (sol s))"] by auto            
         done
       show "((λt. RSadj x y (sol t)) has_derivative (λxb. xb *⇩R ODE_sem I ODE (RSadj x y (sol s)))) (at s within {0..t})"
         using heq heq' hderiv by auto 
       qed
    then show "∀xa∈{0..t}. ((λt. RSadj x y (sol t)) has_derivative (λxb. xb *⇩R ODE_sem I ODE (RSadj x y (sol xa)))) (at xa within {0..t})"
      by auto
    qed

lemma sol_lemma2:
  assumes ORA:"ORadmit ODE"
  assumes t:"0 ≤ t"
  assumes fml:"⋀ν. (ν ∈ fml_sem I (FUrename x y φ)) = (Radj x y ν ∈ fml_sem I φ)"
  assumes sol:"(sol solves_ode (λa. ODE_sem I ODE)) {0..t} {x. mk_v I ODE (sol 0, b) x ∈ fml_sem I φ}"
  shows "((λt. RSadj x y (sol t)) solves_ode (λa. ODE_sem I (OUrename x y ODE))) {0..t} 
          {xa. mk_v I (OUrename x y ODE) (RSadj x y (sol 0), RSadj x y b) xa ∈ fml_sem I (FUrename x y φ)}"
  apply(unfold solves_ode_def)
  apply(rule conjI)
   defer
   subgoal 
     apply auto
   proof -
     fix s
     assume t:"0 ≤ s" "s ≤ t"
     have ivl:"s ∈ {0..t}" using t by auto
     have "mk_v I ODE (sol 0,b) (sol s) ∈ fml_sem I φ"
       using solves_odeD(2)[OF sol ivl] by auto
     then have "Radj x y (mk_v I ODE (sol 0, b) (sol s)) ∈ fml_sem I (FUrename x y φ)"
       using Radj_cancel[of x y "(mk_v I ODE (sol 0, b) (sol s))"]
       by (simp add: fml)
     then show " mk_v I (OUrename x y ODE) (RSadj x y (sol 0), RSadj x y b) (RSadj x y (sol s)) ∈ fml_sem I (FUrename x y φ)"
         using mkv_lemma[OF ORA, of x y I "RSadj x y (sol 0)" "RSadj x y b" "RSadj x y (sol s)"]
         by (simp add: RSadj_cancel ‹mk_v I ODE (sol 0, b) (sol s) ∈ fml_sem I φ› fml)
   qed
   apply (unfold has_vderiv_on_def has_vector_derivative_def)
 proof -
   have "⋀s. s∈{0..t} ⟹  ((λt. RSadj x y (sol t)) has_derivative (λxb. xb *⇩R ODE_sem I (OUrename x y ODE) (RSadj x y (sol s)))) (at s within {0..t})"
   proof -
     fix s
     assume s:"s ∈{0..t}"
     let ?g = "RSadj x y"
     let ?g' = "RSadj x y"
     let ?f = "sol"
     let ?f' = "(λxb. xb *⇩R RSadj x y (ODE_sem I (OUrename x y ODE) (RSadj x y (sol s))))"
     let ?h = "?g ∘ ?f"
     have fun_eq:"(λt'. t' *⇩R ODE_sem I ODE (sol s)) = (λxb. xb *⇩R RSadj x y (ODE_sem I (OUrename x y ODE) (RSadj x y (sol s))))"
       apply(rule ext)
       using OUren[OF ORA, of I x y, of "RSadj x y (sol s)"] RSadj_cancel by simp
     have fun_eq1:"(λν. (χ i. RSadj x y ν $ i)) = RSadj x y"
       by(rule ext, rule vec_extensionality, simp)
     have "s ∈ {0..t} ⟹ (sol has_derivative (λt'. t' *⇩R ODE_sem I ODE (sol s))) (at s within {0..t})"
       using solves_odeD(1)[OF sol] unfolding has_vderiv_on_def has_vector_derivative_def by auto
     then have fderiv:"s ∈ {0..t} ⟹ (?f has_derivative ?f') (at s within {0..t})"
       using fun_eq by auto
     have "((λν. (χ i. RSadj x y ν $ i)) has_derivative (λν'. (χ i . RSadj x y ν' $ i))) (at (?f s) within ?f ` {0..t})"
       apply(rule has_derivative_vec)
       apply(auto simp add: RSadj_def intro:derivative_eq_intros)
         by (simp add: has_derivative_at_withinI has_derivative_proj')+
     then have gderiv:"(RSadj x y has_derivative (RSadj x y)) (at (?f s) within ?f ` {0..t})"
       using fun_eq1 by auto
     have hderiv:"(?h has_derivative (?g' ∘ ?f')) (at s within {0..t})"
       by (rule diff_chain_within[OF fderiv gderiv], rule s)
     have heq:"(λt. RSadj x y (sol t)) = ?h"
       unfolding comp_def by simp
     have RSadj_scale:"⋀c a. RSadj x y (c *⇩R RSadj x y a) = c *⇩R a"
       subgoal for c a
         unfolding RSadj_def
         apply auto
         apply(rule vec_extensionality)
         by(auto)
       done
     have heq':"(λxb. xb *⇩R ODE_sem I (OUrename x y ODE) (RSadj x y (sol s))) = (?g' ∘ ?f')"
       unfolding comp_def apply(rule ext) using OUren[OF ORA, of I x y "RSadj x y (sol s)"]
       apply auto
       subgoal for c
         using RSadj_scale[of c "ODE_sem I (OUrename x y ODE) (RSadj x y (sol s))"] RSadj_cancel[of x y "sol s"]
             RSadj_cancel[of x y "ODE_sem I ODE (sol s)"] by auto
       done
     show "((λt. RSadj x y (sol t)) has_derivative (λxb. xb *⇩R ODE_sem I (OUrename x y ODE) (RSadj x y (sol s)))) (at s within {0..t})"
       using heq heq' hderiv by auto 
       qed
  then show "∀xa∈{0..t}. ((λt. RSadj x y (sol t)) has_derivative (λxb. xb *⇩R ODE_sem I (OUrename x y ODE) (RSadj x y (sol xa)))) (at xa within {0..t})"
  by blast
qed
    
lemma PUren_FUren:
  assumes good_interp:"is_interp I"
  shows
    "(PRadmit α ⟶ hpsafe α ⟶ (∀ ν ω. (ν, ω) ∈ prog_sem I (PUrename x y α) ⟷ (Radj x y ν, Radj x y ω) ∈ prog_sem I α))
    ∧ (FRadmit φ ⟶ fsafe φ ⟶ (∀ ν. ν ∈ fml_sem I (FUrename x y φ) ⟷ (Radj x y ν) ∈ fml_sem I φ))"
proof(induction rule: PRadmit_FRadmit.induct)
  case (FRadmit_Geq θ1 θ2)
  then show ?case using TUren[OF good_interp] by auto
next
  case (FRadmit_Exists φ z) then have
    FRA:"FRadmit φ"
    and IH:"fsafe φ ⟹  (⋀ν. (ν ∈ fml_sem I (FUrename x y φ)) = (Radj x y ν ∈ fml_sem I φ))"
    by auto
  have "fsafe (Exists z φ) ⟹  (⋀ν. (ν ∈ fml_sem I (FUrename x y (Exists z φ))) = (Radj x y ν ∈ fml_sem I (Exists z φ)))"
    apply (cases "z = x")
     subgoal for ν
     proof -
       assume fsafe:"fsafe (Exists z φ)"
       assume zx:"z = x"
       from fsafe have fsafe':"fsafe φ" by auto
       have IH':"(⋀ν. (ν ∈ fml_sem I (FUrename x y φ)) = (Radj x y ν ∈ fml_sem I φ))"
         by (rule IH[OF fsafe'])
       have "(ν ∈ fml_sem I (FUrename x y (Exists z φ))) = (ν ∈ fml_sem I (Exists y (FUrename x y φ)))" using zx by auto
       moreover have "... = (∃r. (repv ν y r) ∈ fml_sem I (FUrename x y φ))" by auto
       moreover have "... = (∃r. (Radj x y (repv ν y r)) ∈ fml_sem I φ)" using IH' by auto
       moreover have "... = (∃r. (repv (Radj x y ν) x r) ∈ fml_sem I φ)" using Radj_repv1[of x y ν] by auto
       moreover have "... = (Radj x y ν ∈ fml_sem I (Exists z φ))" using zx by auto
       ultimately 
       show "(ν ∈ fml_sem I (FUrename x y (Exists z φ))) = (Radj x y ν ∈ fml_sem I (Exists z φ))"
         by auto
     qed
    apply (cases "z = y")
     subgoal for ν
     proof -
       assume fsafe:"fsafe (Exists z φ)"
       assume zx:"z = y"
       from fsafe have fsafe':"fsafe φ" by auto
       have IH':"(⋀ν. (ν ∈ fml_sem I (FUrename x y φ)) = (Radj x y ν ∈ fml_sem I φ))"
         by (rule IH[OF fsafe'])
       have "(ν ∈ fml_sem I (FUrename x y (Exists z φ))) = (ν ∈ fml_sem I (Exists x (FUrename x y φ)))" using zx by auto
       moreover have "... = (∃r. (repv ν x r) ∈ fml_sem I (FUrename x y φ))" by auto
       moreover have "... = (∃r. (Radj x y (repv ν x r)) ∈ fml_sem I φ)" using IH' by auto
       moreover have "... = (∃r. (repv (Radj x y ν) y r) ∈ fml_sem I φ)" using Radj_repv2[of x y ν] by auto
       moreover have "... = (Radj x y ν ∈ fml_sem I (Exists z φ))" using zx by auto
       ultimately 
       show "(ν ∈ fml_sem I (FUrename x y (Exists z φ))) = (Radj x y ν ∈ fml_sem I (Exists z φ))"
         by auto
     qed
    subgoal for ν
    proof -
      assume fsafe:"fsafe (Exists z φ)"
      assume zx:"z ≠ x" and zy:"z ≠ y"
      from fsafe have fsafe':"fsafe φ" by auto
      have IH':"(⋀ν. (ν ∈ fml_sem I (FUrename x y φ)) = (Radj x y ν ∈ fml_sem I φ))"
        by (rule IH[OF fsafe'])
      have "(ν ∈ fml_sem I (FUrename x y (Exists z φ))) = (ν ∈ fml_sem I (Exists z (FUrename x y φ)))" using zx zy by auto
      moreover have "... = (∃r. (repv ν z r) ∈ fml_sem I (FUrename x y φ))" by auto
      moreover have "... = (∃r. (Radj x y (repv ν z r)) ∈ fml_sem I φ)" using IH' by auto
      moreover have "... = (∃r. (repv (Radj x y ν) z r) ∈ fml_sem I φ)" using Radj_repv3[of z x y ν, OF zx zy] by auto
      moreover have "... = (Radj x y ν ∈ fml_sem I (Exists z φ))" using zx by auto
      ultimately 
      show "(ν ∈ fml_sem I (FUrename x y (Exists z φ))) = (Radj x y ν ∈ fml_sem I (Exists z φ))"
        by auto
    qed
    done
  then show ?case by auto 
next
  case (PRadmit_Assign z θ)
  have "hpsafe (Assign z θ) ⟹  (⋀ν ω. ((ν, ω)  ∈ prog_sem I (PUrename x y (Assign z θ))) = ((Radj x y ν, Radj x y ω) ∈ prog_sem I (Assign z θ)))"
    apply (cases "z = x")
     subgoal for ν ω
     proof -
       assume fsafe:"hpsafe (Assign z θ)"
       assume zx:"z = x"
       from fsafe have dsafe:"dsafe θ" by auto
       have IH':"(⋀ν. dterm_sem I (TUrename x y θ) ν = dterm_sem I θ (Radj x y ν))"
         subgoal for ν using TUren[OF good_interp dsafe , of x y ν] by auto done
       have "((ν, ω) ∈ prog_sem I (PUrename x y (Assign z θ))) = ((ν, ω) ∈ prog_sem I (Assign y (TUrename x y θ)))"  using zx by auto
       moreover have "... = (ω = repv ν y (dterm_sem I (TUrename x y θ) ν))" by auto
       moreover have "... = (ω = repv ν y (dterm_sem I θ (Radj x y ν)))" using IH' by auto
       moreover have "... = (Radj x y ω = Radj x y (repv ν y (dterm_sem I θ (Radj x y ν))))" using Radj_eq_iff by auto
       moreover have "... = (Radj x y ω = repv (Radj x y ν) x (dterm_sem I θ (Radj x y ν)))" using Radj_repv1 by auto
       moreover have "... = (Radj x y ω = repv (Radj x y ν) z (dterm_sem I θ (Radj x y ν)))" using zx by auto
       moreover have "... = ((Radj x y ν, Radj x y ω) ∈ prog_sem  I (Assign z θ))" by auto        
       ultimately 
       show "((ν, ω) ∈ prog_sem I (PUrename x y (Assign z θ))) = ((Radj x y ν, Radj x y ω) ∈ prog_sem  I (Assign z θ))"
         by auto
     qed
    apply (cases "z = y")
     subgoal for ν ω
     proof -
       assume fsafe:"hpsafe (Assign z θ)"
       assume zy:"z = y"
       from fsafe have dsafe:"dsafe θ" by auto
       have IH':"(⋀ν. dterm_sem I (TUrename x y θ) ν = dterm_sem I θ (Radj x y ν))"
         subgoal for ν using TUren[OF good_interp dsafe , of x y ν] by auto done
       have "((ν, ω) ∈ prog_sem I (PUrename x y (Assign z θ))) = ((ν, ω) ∈ prog_sem I (Assign x (TUrename x y θ)))"  using zy by auto
       moreover have "... = (ω = repv ν x (dterm_sem I (TUrename x y θ) ν))" by auto
       moreover have "... = (ω = repv ν x (dterm_sem I θ (Radj x y ν)))" using IH' by auto
       moreover have "... = (Radj x y ω = Radj x y (repv ν x (dterm_sem I θ (Radj x y ν))))" using Radj_eq_iff by auto
       moreover have "... = (Radj x y ω = repv (Radj x y ν) y (dterm_sem I θ (Radj x y ν)))" using Radj_repv2 by auto
       moreover have "... = (Radj x y ω = repv (Radj x y ν) z (dterm_sem I θ (Radj x y ν)))" using zy by auto
       moreover have "... = ((Radj x y ν, Radj x y ω) ∈ prog_sem  I (Assign z θ))" by auto        
       ultimately 
       show "((ν, ω) ∈ prog_sem I (PUrename x y (Assign z θ))) = ((Radj x y ν, Radj x y ω) ∈ prog_sem  I (Assign z θ))"
         by auto
     qed
    subgoal for ν ω
    proof -
      assume fsafe:"hpsafe (Assign z θ)"
      assume zx:"z ≠ x" and zy:"z ≠ y"
      from fsafe have dsafe:"dsafe θ" by auto
      have IH':"(⋀ν. dterm_sem I (TUrename x y θ) ν = dterm_sem I θ (Radj x y ν))"
        subgoal for ν using TUren[OF good_interp dsafe , of x y ν] by auto done
      have "((ν, ω) ∈ prog_sem I (PUrename x y (Assign z θ))) = ((ν, ω) ∈ prog_sem I (Assign z (TUrename x y θ)))"  using zx zy by auto
      moreover have "... = (ω = repv ν z (dterm_sem I (TUrename x y θ) ν))" by auto
      moreover have "... = (ω = repv ν z (dterm_sem I θ (Radj x y ν)))" using IH' by auto
      moreover have "... = (Radj x y ω = Radj x y (repv ν z (dterm_sem I θ (Radj x y ν))))" using Radj_eq_iff by auto
      moreover have "... = (Radj x y ω = repv (Radj x y ν) z (dterm_sem I θ (Radj x y ν)))" using Radj_repv3[OF zx zy] by auto
      moreover have "... = ((Radj x y ν, Radj x y ω) ∈ prog_sem  I (Assign z θ))" by auto        
      ultimately 
      show "((ν, ω) ∈ prog_sem I (PUrename x y (Assign z θ))) = ((Radj x y ν, Radj x y ω) ∈ prog_sem  I (Assign z θ))"
        by auto
    qed
    done
  then show ?case by auto
next
  case (PRadmit_DiffAssign z θ)
  have "hpsafe (DiffAssign z θ) ⟹  (⋀ν ω. ((ν, ω)  ∈ prog_sem I (PUrename x y (DiffAssign z θ))) = ((Radj x y ν, Radj x y ω) ∈ prog_sem I (DiffAssign z θ)))"
    apply (cases "z = x")
     subgoal for ν ω
     proof -
       assume fsafe:"hpsafe (DiffAssign z θ)"
       assume zx:"z = x"
       from fsafe have dsafe:"dsafe θ" by auto
       have IH':"(⋀ν. dterm_sem I (TUrename x y θ) ν = dterm_sem I θ (Radj x y ν))"
         subgoal for ν using TUren[OF good_interp dsafe , of x y ν] by auto done
       have "((ν, ω) ∈ prog_sem I (PUrename x y (DiffAssign z θ))) = ((ν, ω) ∈ prog_sem I (DiffAssign y (TUrename x y θ)))"  using zx by auto
       moreover have "... = (ω = repd ν y (dterm_sem I (TUrename x y θ) ν))" by auto
       moreover have "... = (ω = repd ν y (dterm_sem I θ (Radj x y ν)))" using IH' by auto
       moreover have "... = (Radj x y ω = Radj x y (repd ν y (dterm_sem I θ (Radj x y ν))))" using Radj_eq_iff by auto
       moreover have "... = (Radj x y ω = repd (Radj x y ν) x (dterm_sem I θ (Radj x y ν)))" using Radj_repd1 by auto
       moreover have "... = (Radj x y ω = repd (Radj x y ν) z (dterm_sem I θ (Radj x y ν)))" using zx by auto
       moreover have "... = ((Radj x y ν, Radj x y ω) ∈ prog_sem  I (DiffAssign z θ))" by auto        
       ultimately 
       show "((ν, ω) ∈ prog_sem I (PUrename x y (DiffAssign z θ))) = ((Radj x y ν, Radj x y ω) ∈ prog_sem  I (DiffAssign z θ))"
         by auto
     qed
    apply (cases "z = y")
     subgoal for ν ω
     proof -
       assume fsafe:"hpsafe (DiffAssign z θ)"
       assume zy:"z = y"
       from fsafe have dsafe:"dsafe θ" by auto
       have IH':"(⋀ν. dterm_sem I (TUrename x y θ) ν = dterm_sem I θ (Radj x y ν))"
         subgoal for ν using TUren[OF good_interp dsafe , of x y ν] by auto done
       have "((ν, ω) ∈ prog_sem I (PUrename x y (DiffAssign z θ))) = ((ν, ω) ∈ prog_sem I (DiffAssign x (TUrename x y θ)))"  using zy by auto
       moreover have "... = (ω = repd ν x (dterm_sem I (TUrename x y θ) ν))" by auto
       moreover have "... = (ω = repd ν x (dterm_sem I θ (Radj x y ν)))" using IH' by auto
       moreover have "... = (Radj x y ω = Radj x y (repd ν x (dterm_sem I θ (Radj x y ν))))" using Radj_eq_iff by auto
       moreover have "... = (Radj x y ω = repd (Radj x y ν) y (dterm_sem I θ (Radj x y ν)))" using Radj_repd2 by auto
       moreover have "... = (Radj x y ω = repd (Radj x y ν) z (dterm_sem I θ (Radj x y ν)))" using zy by auto
       moreover have "... = ((Radj x y ν, Radj x y ω) ∈ prog_sem  I (DiffAssign z θ))" by auto        
       ultimately 
        show "((ν, ω) ∈ prog_sem I (PUrename x y (DiffAssign z θ))) = ((Radj x y ν, Radj x y ω) ∈ prog_sem  I (DiffAssign z θ))"
         by auto
     qed
    subgoal for ν ω
  proof -
    assume fsafe:"hpsafe (DiffAssign z θ)"
    assume zx:"z ≠ x" and zy:"z ≠ y"
    from fsafe have dsafe:"dsafe θ" by auto
    have IH':"(⋀ν. dterm_sem I (TUrename x y θ) ν = dterm_sem I θ (Radj x y ν))"
      subgoal for ν using TUren[OF good_interp dsafe , of x y ν] by auto done
    have "((ν, ω) ∈ prog_sem I (PUrename x y (DiffAssign z θ))) = ((ν, ω) ∈ prog_sem I (DiffAssign z (TUrename x y θ)))"  using zx zy by auto
    moreover have "... = (ω = repd ν z (dterm_sem I (TUrename x y θ) ν))" by auto
    moreover have "... = (ω = repd ν z (dterm_sem I θ (Radj x y ν)))" using IH' by auto
    moreover have "... = (Radj x y ω = Radj x y (repd ν z (dterm_sem I θ (Radj x y ν))))" using Radj_eq_iff by auto
    moreover have "... = (Radj x y ω = repd (Radj x y ν) z (dterm_sem I θ (Radj x y ν)))" using Radj_repd3[OF zx zy] by auto
    moreover have "... = ((Radj x y ν, Radj x y ω) ∈ prog_sem  I (DiffAssign z θ))" by auto        
    ultimately 
    show "((ν, ω) ∈ prog_sem I (PUrename x y (DiffAssign z θ))) = ((Radj x y ν, Radj x y ω) ∈ prog_sem  I (DiffAssign z θ))"
      by auto
  qed
  done
  then show ?case by auto
next
  case (PRadmit_Test φ) then
  have FRA:"FRadmit φ"
  and IH:"fsafe φ ⟹ (⋀ν. (ν ∈ fml_sem I (FUrename x y φ)) = (Radj x y ν ∈ fml_sem I φ))"
    by auto
  have "hpsafe (? φ) ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (PUrename x y (? φ))) = ((Radj x y ν, Radj x y ω) ∈ prog_sem I (? φ)))"
    proof -
      assume hpsafe:"hpsafe (? φ)"
      fix ν ω
      from hpsafe have fsafe:"fsafe φ" by auto
      have IH':"⋀ν. (ν ∈ fml_sem I (FUrename x y φ)) = (Radj x y ν ∈ fml_sem I φ)" 
        by (rule IH[OF fsafe])
      have "((ν, ω) ∈ prog_sem I (PUrename x y (? φ))) = (ν = ω ∧ (ω ∈ fml_sem I (FUrename x y φ)))" by (cases ω, auto)
      moreover have "... = (ν = ω ∧ (Radj x y ω) ∈ fml_sem I φ)" using IH' by auto
      moreover have "... = (Radj x y ν = Radj x y ω ∧ (Radj x y ω) ∈ fml_sem I φ)" using Radj_eq_iff by auto
      moreover have "... = ((Radj x y ν, Radj x y ω) ∈ prog_sem I (? φ))" by (cases "Radj x y ω", auto)
      ultimately show "?thesis ν ω" by auto
    qed
  then show ?case by auto
next
  case (FRadmit_Prop p args) then
  have "fsafe (Prop p args) ⟹ (⋀ν. (ν ∈ fml_sem I (FUrename x y (Prop p args))) = ((Radj x y ν) ∈ fml_sem I (Prop p args)))"
  proof -
    assume fsafe:"fsafe (Prop p args)"
    fix ν
    from fsafe have dsafes:"⋀i. dsafe (args i)" using dfree_is_dsafe by auto
    have IH:"⋀i ν. dterm_sem I (TUrename x y (args i)) ν = dterm_sem I (args i) (Radj x y ν)"
      using TUren[OF good_interp dsafes] by auto
    have "(ν ∈ fml_sem I (FUrename x y (Prop p args))) = (ν ∈ fml_sem I (Prop p (λi . TUrename x y (args i))))" by auto
    moreover have "... = (Predicates I p (χ i. dterm_sem I (TUrename x y (args i)) ν))" by auto
    moreover have "... = (Predicates I p (χ i. dterm_sem I (args i) (Radj x y ν)))" using IH by auto
    moreover have "... = ((Radj x y ν) ∈ fml_sem I (Prop p args))" by auto
    ultimately show "?thesis ν" by blast
  qed 
  then show ?case by auto
next
  case (PRadmit_Sequence a b) then 
  have IH1:"hpsafe a ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (PUrename x y a)) = ((Radj x y ν, Radj x y ω) ∈ prog_sem I a))"
    and  IH2:"hpsafe b ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (PUrename x y b)) = ((Radj x y ν, Radj x y ω) ∈ prog_sem I b))"
    by auto
  have "hpsafe (a ;; b) ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (PUrename x y (a ;;b))) = ((Radj x y ν, Radj x y ω) ∈ prog_sem I (a ;; b)))"
  proof -
    assume hpsafe:"hpsafe (a ;; b)"
    fix ν ω
    from hpsafe have safe1:"hpsafe a" and safe2:"hpsafe b" by auto
    have IH1:"(⋀μ. ((ν, μ) ∈ prog_sem I (PUrename x y a)) = ((Radj x y ν, Radj x y μ) ∈ prog_sem I a))"
      using IH1[OF safe1] by auto
    have IH2:"(⋀μ. ((μ, ω) ∈ prog_sem I (PUrename x y b)) = ((Radj x y μ, Radj x y ω) ∈ prog_sem I b))"
      using IH2[OF safe2] by auto
    have "((ν, ω) ∈ prog_sem I (PUrename x y (a ;;b))) = ((ν, ω) ∈ prog_sem I ((PUrename x y a) ;;(PUrename x y b)))" by auto
    moreover have "... = (∃μ. (ν, μ) ∈ prog_sem I (PUrename x y a) ∧ (μ, ω) ∈ prog_sem I (PUrename x y b))" by auto
    moreover have "... = (∃μ. (Radj x y ν, Radj x y μ) ∈ prog_sem I a ∧ (Radj x y μ, Radj x y ω) ∈ prog_sem I b)" using IH1 IH2 by auto
    moreover have "... = (∃μ. (Radj x y ν, μ) ∈ prog_sem I a ∧ (μ, Radj x y ω) ∈ prog_sem I b)" 
      apply auto
       subgoal for aa ba
         apply(rule exI[where x="fst(Radj x y (aa,ba))"])
         apply(rule exI[where x="snd(Radj x y (aa,ba))"])
         by auto
      subgoal for aa ba
        apply(rule exI[where x="fst(Radj x y (aa,ba))"])
        apply(rule exI[where x="snd(Radj x y (aa,ba))"])
        using Radj_cancel by auto
      done
    moreover have "... = ((Radj x y ν, Radj x y ω) ∈ prog_sem I (a ;;b))" by (auto,blast)
    ultimately show "?thesis ν ω" by auto
  qed
  then show ?case by auto
next
  case (FRadmit_Diamond α φ) then
  have IH1:"hpsafe α ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (PUrename x y α)) = ((Radj x y ν, Radj x y ω) ∈ prog_sem I α))"
  and IH2:"fsafe φ ⟹ (⋀ν. (ν ∈ fml_sem I (FUrename x y φ)) = (Radj x y ν ∈ fml_sem I φ))"
    by auto
  have "fsafe (⟨α⟩φ) ⟹ (⋀ν. (ν ∈ fml_sem I (FUrename x y (⟨α⟩φ))) = (Radj x y ν ∈ fml_sem I (⟨α⟩φ)))"
  proof -
    assume safe:"fsafe (⟨α⟩φ)"
    fix ν
    from safe have safe1:"hpsafe α" and safe2:"fsafe φ" by auto
    have IH1:"⋀ω. ((ν, ω) ∈ prog_sem I (PUrename x y α)) = ((Radj x y ν, Radj x y ω) ∈ prog_sem I α)"
      using IH1[OF safe1] by auto
    have IH2:"⋀ν. (ν ∈ fml_sem I (FUrename x y φ)) = (Radj x y ν ∈ fml_sem I φ)"
      by (rule IH2[OF safe2])
    have "(ν ∈ fml_sem I (FUrename x y (⟨α⟩φ))) = (ν ∈ fml_sem I (⟨PUrename x y α⟩FUrename x y φ))" by auto
    moreover have "... = (∃ ω. (ν, ω) ∈ prog_sem I (PUrename x y α) ∧ ω ∈ fml_sem I (FUrename x y φ))" by auto
    moreover have "... = (∃ ω. (Radj x y ν, Radj x y ω) ∈ prog_sem I α ∧ (Radj x y ω) ∈ fml_sem I φ)" 
      using IH1 IH2 by auto
    moreover have "... = (∃ ω. (Radj x y ν, ω) ∈ prog_sem I α ∧ ω ∈ fml_sem I φ)"
      apply auto
       subgoal for aa ba
         apply(rule exI[where x="fst(Radj x y (aa,ba))"])
         apply(rule exI[where x="snd(Radj x y (aa,ba))"])
         by auto
      subgoal for aa ba
        apply(rule exI[where x="fst(Radj x y (aa,ba))"])
        apply(rule exI[where x="snd(Radj x y (aa,ba))"])
        using Radj_cancel by auto
      done
    moreover have "... = (Radj x y ν ∈ fml_sem I (⟨α⟩φ))" by auto
    ultimately show "?thesis ν" by auto
  qed
  then show ?case by auto
next
  case (PRadmit_Loop a) then
  have IH:" hpsafe a ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (PUrename x y a)) = ((Radj x y ν, Radj x y ω) ∈ prog_sem I a))"
    by auto
  have "hpsafe (a** ) ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (PUrename x y (a** ))) = ((Radj x y ν, Radj x y ω) ∈ prog_sem I (a** )))"
  proof -
    assume safe:"hpsafe (a** )"
    fix ν ω
    from safe have safe:"hpsafe a" by auto
    have IH1:"(⋀ν ω. ((ν, ω) ∈ prog_sem I (PUrename x y a)) = ((Radj x y ν, Radj x y ω) ∈ prog_sem I a))"
      by (rule IH[OF safe])
    have relpow_iff:"⋀ν ω R n. ((ν, ω) ∈ R ^^ Suc n) = (∃μ. (ν, μ) ∈ R ∧ (μ, ω) ∈ R ^^ n)"
      apply auto
       subgoal for R n x y z by (auto simp add: relpow_Suc_D2')
      subgoal for ν ω R n μ using relpow_Suc_I2 by fastforce
      done
    have rtrancl_iff_relpow:"⋀ν ω R. ((ν, ω) ∈ R⇧*) = (∃n. (ν, ω) ∈ R ^^ n)"
      using rtrancl_imp_relpow relpow_imp_rtrancl by blast
    have lem:"⋀n. (∀ ν ω.  ((ν, ω) ∈ prog_sem I (PUrename x y a)^^n) = ((Radj x y ν, Radj x y ω) ∈ prog_sem I a^^n))"
      subgoal for n
      proof(induction n)
        case 0
        then show ?case using Radj_eq_iff by auto
      next
        case (Suc n) then
        have IH2:"⋀ν ω. ((ν, ω) ∈ prog_sem I (PUrename x y a) ^^ n) = ((Radj x y ν, Radj x y ω) ∈ prog_sem I a ^^ n)"
          by auto
        have "⋀ν ω. ((ν, ω) ∈ prog_sem I (PUrename x y a) ^^ Suc n) = ((Radj x y ν, Radj x y ω) ∈ prog_sem I a ^^ Suc n)"
        proof -
          fix ν ω
          have "((ν, ω) ∈ prog_sem I (PUrename x y a) ^^ Suc n) 
            = (∃ μ. (ν, μ) ∈ prog_sem I (PUrename x y a) ∧ (μ, ω) ∈ prog_sem I (PUrename x y a) ^^ n)"
            using relpow_iff[of ν ω n "prog_sem I (PUrename x y a)"] by auto
          moreover have "... = (∃ μ. (Radj x y ν, Radj x y μ) ∈ prog_sem I a ∧ (Radj x y μ, Radj x y ω) ∈ prog_sem I a ^^ n)"
            using IH1 IH2 by blast
          moreover have "... = (∃ μ. (Radj x y ν, μ) ∈ prog_sem I a ∧ (μ, Radj x y ω) ∈ prog_sem I a ^^ n)"
            apply auto
             subgoal for aa ba
               apply(rule exI[where x="fst(Radj x y (aa,ba))"])
               apply(rule exI[where x="snd(Radj x y (aa,ba))"])
               by auto
            subgoal for aa ba
              apply(rule exI[where x="fst(Radj x y (aa,ba))"])
              apply(rule exI[where x="snd(Radj x y (aa,ba))"])
              using Radj_cancel by auto
            done
          moreover have "... = ((Radj x y ν, Radj x y ω) ∈ prog_sem I a ^^ Suc n)"
            using relpow_iff[of "Radj x y ν" "Radj x y ω"  n "prog_sem I a"] by auto
          ultimately show "?thesis ν ω" by auto 
        qed
        then show ?case by auto
      qed
      done
    have "((ν, ω) ∈ prog_sem I (PUrename x y (a** ))) = ((ν, ω) ∈ (prog_sem I (PUrename x y a))⇧*)" by auto
    moreover have "... = (∃n. (ν, ω) ∈ (prog_sem I (PUrename x y a)) ^^ n)"
      using rtrancl_iff_relpow[of ν ω "prog_sem I (PUrename x y a)"] by auto
    moreover have "... = (∃n. (Radj x y ν, Radj x y ω) ∈ (prog_sem I a) ^^ n)"
      using lem by blast
    moreover have "... = ((Radj x y ν, Radj x y ω) ∈ (prog_sem I a)⇧*)"
      using rtrancl_iff_relpow[of "Radj x y ν" "Radj x y ω" "prog_sem I a"] by auto
    moreover have "... = ((Radj x y ν, Radj x y ω) ∈ prog_sem I (a** ))" by auto
    ultimately show "?thesis ν ω" by blast
  qed
  then show ?case by auto
next
  case (PRadmit_EvolveODE ODE φ) then
  have ORA:"ORadmit ODE"
    and IH:"fsafe φ ⟹ (⋀ν. (ν ∈ fml_sem I (FUrename x y φ)) = (Radj x y ν ∈ fml_sem I φ))"
    by auto
  have "hpsafe (EvolveODE ODE φ) ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (PUrename x y (EvolveODE ODE φ))) = ((Radj x y ν, Radj x y ω) ∈ prog_sem I (EvolveODE ODE φ)))"
  proof -
    assume safe:"hpsafe (EvolveODE ODE φ)"
    fix ν ω
    from safe have osafe:"osafe ODE" and fsafe:"fsafe φ" by auto
    have IH1:"⋀ν. (ν ∈ fml_sem I (FUrename x y φ) = (Radj x y ν ∈ fml_sem I φ))" by (rule IH[OF fsafe])
    have IH2:"⋀ν. ODE_sem I (OUrename x y ODE) ν = RSadj x y (ODE_sem I ODE (RSadj x y ν))"
      using OUren[OF ORA] by auto
    have RSadj_Radj:"⋀a b. (RSadj x y a, RSadj x y b) = Radj x y (a,b)"
      unfolding RSadj_def Radj_def by auto
    have Radj_swap:"⋀a b. Radj x y a = b ⟹ a = Radj x y b"
      using Radj_cancel Radj_eq_iff by metis
    have mkv:"⋀t sol b. Radj x y (mk_v I (OUrename x y ODE) (sol 0, b) (sol t)) = mk_v I ODE (RSadj x y (sol 0), RSadj x y b) (RSadj x y (sol t))"
      using mkv_lemma[OF ORA] by blast
    have mkv2:"⋀t sol b.  Radj x y ω = mk_v I ODE (sol 0, b) (sol t) ⟹
      ω = mk_v I (OUrename x y ODE) (RSadj x y (sol 0), RSadj x y b) (RSadj x y (sol t))"
      using mkv_lemma[OF ORA] by (metis RSadj_cancel Radj_cancel)
    have sol:"⋀t sol b. 0 ≤ t ⟹
      (sol solves_ode (λa. ODE_sem I (OUrename x y ODE))) {0..t} {xa. mk_v I (OUrename x y ODE) (sol 0, b) xa ∈ fml_sem I (FUrename x y φ)} ⟹
      ((λt. RSadj x y (sol t)) solves_ode (λa. ODE_sem I ODE)) {0..t} {xa. mk_v I ODE (RSadj x y (sol 0), RSadj x y b) xa ∈ fml_sem I φ}"
      using sol_lemma IH1 IH2 ORA by blast
    have sol2:"⋀t sol b. 0 ≤ t ⟹
(sol solves_ode (λa. ODE_sem I ODE)) {0..t} {x. mk_v I ODE (sol 0, b) x ∈ fml_sem I φ} ⟹
((λt. RSadj x y (sol t)) solves_ode (λa. ODE_sem I (OUrename x y ODE))) {0..t}
 {xa. mk_v I (OUrename x y ODE) (RSadj x y (sol 0), RSadj x y b) xa ∈ fml_sem I (FUrename x y φ)}"
      using sol_lemma2 IH1 IH2 ORA by blast
    show "?thesis ν ω"
      apply auto
       subgoal for b sol t
         apply(rule exI[where x= "RSadj x y b"])
         apply(rule exI[where x= "(λt. RSadj x y (sol t))"])
         apply(rule conjI)
          subgoal using RSadj_Radj[of "sol 0" "b"] by auto
         apply(rule exI[where x =t])
         apply(rule conjI)
          subgoal by (rule mkv)
         apply(rule conjI)
          subgoal by assumption
         by (rule sol)
      subgoal for b sol t
        apply(rule exI[where x= "RSadj x y b"])
        apply(rule exI[where x= "(λt. RSadj x y (sol t))"])
        apply(rule conjI)
         subgoal using RSadj_Radj[of "sol 0" "b"] Radj_swap[of ν "(sol 0,b)"] by auto
        apply(rule exI[where x =t])
        apply(rule conjI)
         subgoal by (rule mkv2)
        apply(rule conjI)
         subgoal by assumption
        by (rule sol2)
      done
    qed
  then show ?case by auto
qed (auto simp add: Radj_def)

lemma FUren:"is_interp I ⟹ FRadmit φ ⟹ fsafe φ ⟹ (⋀ν. (ν ∈ fml_sem I (FUrename x y φ)) = (Radj x y ν ∈ fml_sem I φ))"
  using PUren_FUren by blast

subsection ‹Uniform Renaming Rule Soundness›
lemma URename_sound:"FRadmit φ ⟹ fsafe φ ⟹ valid φ ⟹ valid (FUrename x y φ)"
  unfolding valid_def using FUren by blast

subsection ‹Bound Renaming Rule Soundness›
lemma BRename_sound:
  assumes FRA:"FRadmit([[Assign x θ]]φ)"
  assumes fsafe:"fsafe ([[Assign x θ]]φ)"
  assumes valid:"valid ([[Assign x θ]]φ)"
  assumes FVF:"{Inl y, Inr y, Inr x} ∩ FVF φ = {}"
  shows "valid([[Assign y θ]]FUrename x y φ)"
proof -
  have FRA':"FRadmit φ" using FRA 
    by (metis (no_types, lifting) Box_def FRadmit.cases formula.distinct(15) formula.distinct(21) formula.distinct(27) formula.distinct(29) formula.distinct(3) formula.distinct(31) formula.distinct formula.distinct(9) formula.inject(3) formula.inject(6))
  have fsafe':"fsafe φ" using fsafe  by (simp add: Box_def)
  have dsafe:"dsafe θ" using fsafe by (simp add: Box_def)
  have "⋀I ν. is_interp I ⟹ ν ∈ fml_sem I ([[y := θ]]FUrename x y φ)"
  proof -
    fix I::"('sf,'sc,'sz) interp" and ν::"'sz state"
    assume good_interp:"is_interp I"
    from FVF have sub:"FVF φ ⊆ -{Inl y, Inr y, Inr x}" by auto
    have "Vagree (repv (Radj x y ν) x (dterm_sem I θ ν)) (repv ν x (dterm_sem I θ ν)) (-{Inl y, Inr y, Inr x})"
      unfolding Vagree_def using FVF unfolding Radj_def RSadj_def by auto
    then have agree:"Vagree (repv (Radj x y ν) x (dterm_sem I θ ν)) (repv ν x (dterm_sem I θ ν)) (FVF φ)"
      using agree_sub[OF sub] by auto
    have fml_sem_eq:"(repv (Radj x y ν) x (dterm_sem I θ ν) ∈ fml_sem I φ) = (repv ν x (dterm_sem I θ ν) ∈ fml_sem I φ)"
      using coincidence_formula[OF fsafe' Iagree_refl agree] by auto
    have "(ν ∈ fml_sem I ([[y := θ]]FUrename x y φ)) = (repv ν y (dterm_sem I θ ν) ∈ fml_sem I (FUrename x y φ))"
      by auto
    moreover have "... = (Radj x y (repv ν y (dterm_sem I θ ν)) ∈ fml_sem I φ)"
      using FUren[OF good_interp FRA' fsafe'] by auto
    moreover have "... = (repv (Radj x y ν) x (dterm_sem I θ ν) ∈ fml_sem I φ)"
      using Radj_repv1 by auto
    moreover have "... = (ν ∈ fml_sem I ([[x := θ]]φ))"
      using fml_sem_eq by auto
    moreover have "... = True"
      using valid unfolding valid_def using good_interp by blast
    ultimately
    show "ν ∈ fml_sem I ([[y := θ]]FUrename x y φ)"
      by blast
  qed
  then
  show ?thesis unfolding valid_def by auto
qed
  


end end