Theory USubst_Lemma

theory "USubst_Lemma"
imports
  Ordinary_Differential_Equations.ODE_Analysis
  "Ids"
  "Lib"
  "Syntax"
  "Denotational_Semantics"
  "Frechet_Correctness"
  "Static_Semantics"
  "Coincidence"
  "Bound_Effect"
  "USubst"
begin context ids begin
section ‹Soundness proof for uniform substitution rule›
lemma interp_eq:
  "f = f'  p = p'  c = c'  PP = PP'  ode = ode'  odebv = odebv' 
   Functions = f, Predicates = p, Contexts = c, Programs = PP, ODEs = ode, ODEBV = odebv =
   Functions = f', Predicates = p', Contexts = c', Programs = PP', ODEs = ode', ODEBV = odebv'"
  by auto

subsection ‹Lemmas about well-formedness of (adjoint) interpretations.›

text ‹When adding a function to an interpretation with {\tt extendf}, we need to show it's C1 continuous.
  We do this by explicitly constructing the derivative {\tt extendf\_deriv} and showing it's continuous.›
primrec extendf_deriv :: "('sf,'sc,'sz) interp  'sf  ('sf + 'sz,'sz) trm  'sz state  'sz Rvec  ('sz Rvec  real)"
where
  "extendf_deriv I _ (Var i) ν x = (λ_. 0)"
| "extendf_deriv I _ (Const r) ν x = (λ_. 0)"
| "extendf_deriv I g (Function f args) ν x =
  (case f of 
    Inl ff  (THE f'. y. (Functions I ff has_derivative f' y) (at y))
              (χ i. dterm_sem
                     Functions = case_sum (Functions I) (λf' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
                        ODEs = ODEs I, ODEBV = ODEBV I
                     (args i) ν) 
             (λν'. χ ia. extendf_deriv I g (args ia) ν x ν')
  | Inr ff  (λ ν'. ν' $ ff))"
| "extendf_deriv I g (Plus t1 t2) ν x = (λν'. (extendf_deriv I g t1 ν x ν') + (extendf_deriv I g t2 ν x ν'))"
| "extendf_deriv I g (Times t1 t2) ν x = 
   (λν'. ((dterm_sem (extendf I x) t1 ν * (extendf_deriv I g t2 ν x ν'))) 
       + (extendf_deriv I g t1 ν x ν') * (dterm_sem (extendf I x) t2 ν))"
| "extendf_deriv I g ($' _) ν = undefined"
| "extendf_deriv I g (Differential _) ν = undefined"

lemma extendf_dterm_sem_continuous:
  fixes f'::"('sf + 'sz,'sz) trm" and I::"('sf,'sc,'sz) interp"
  assumes free:"dfree f'"
  assumes good_interp:"is_interp I"
  shows "continuous_on UNIV (λx. dterm_sem (extendf I x) f' ν)"
proof(induction rule: dfree.induct[OF free])
  case (3 args f)
  then show ?case 
    apply(cases f)
     apply (auto simp add: continuous_intros)
    subgoal for a
      apply(rule continuous_on_compose2[of UNIV "Functions I a" UNIV "(λ x. (χ i. dterm_sem
                       Functions = case_sum (Functions I) (λf' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I,
                          Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I
                       (args i) ν))"])
      subgoal
        using is_interpD[OF good_interp]
        using has_derivative_continuous_on[of UNIV "(Functions I a)" "(THE f'. x. (Functions I a has_derivative f' x) (at x))"] 
        by auto
      apply(rule continuous_on_vec_lambda) by auto
    done
qed (auto simp add: continuous_intros)

lemma extendf_deriv_bounded:
  fixes f'::"('sf + 'sz,'sz) trm" and I::"('sf,'sc,'sz) interp"
  assumes free:"dfree f'"
  assumes good_interp:"is_interp I"
  shows "bounded_linear (extendf_deriv I i f' ν x)"
proof(induction rule: dfree.induct[OF free])
  case (1 i)
  then show ?case by auto
next
  case (2 r)
  then show ?case by auto
next
  case (3 args f)
  then show ?case apply auto
    apply(cases f)
     apply auto
    subgoal for a
      apply(rule bounded_linear_compose[of "(THE f'. y. (Functions I a has_derivative f' y) (at y))
           (χ i. dterm_sem
                  Functions = case_sum (Functions I) (λf' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
                     ODEs = ODEs I, ODEBV = ODEBV I
                  (args i) ν)"])
       subgoal using good_interp unfolding is_interp_def  using has_derivative_bounded_linear  by fastforce
      apply(rule bounded_linear_vec)
      by auto
    done
next
  case (4 θ1 θ2)
  then show ?case apply auto
    using bounded_linear_add by blast
next
  case (5 θ1 θ2)
  then show ?case apply auto
    apply(rule bounded_linear_add)
     apply(rule bounded_linear_const_mult)
     subgoal by auto
    apply(rule bounded_linear_mult_const)
    subgoal by auto
    done
qed

lemma extendf_deriv_continuous:
  fixes f'::"('sf + 'sz,'sz) trm" and I::"('sf,'sc,'sz) interp"
  assumes free:"dfree f'"
  assumes good_interp:"is_interp I"
  shows "continuous_on UNIV (λx. Blinfun (extendf_deriv I i f' ν x))"
proof (induction rule: dfree.induct[OF free])
  case (3 args f)
  assume dfrees:"i. dfree (args i)"
  assume const:"j. continuous_on UNIV (λx. Blinfun (extendf_deriv I i (args j) ν x))"
  then show ?case 
    unfolding extendf_deriv.simps
    apply(cases f)
    subgoal for a 
      apply simp
      proof -
        have boundedF:"x. bounded_linear (((THE f'. y. (Functions I a has_derivative f' y) (at y))
                          (χ i. dterm_sem (extendf I x) (args i) ν) ))"
          using blinfun.bounded_linear_right using good_interp unfolding is_interp_def 
          by auto
        have boundedG:"x. bounded_linear (λ b. (χ ia. extendf_deriv I i (args ia) ν x b))"
          by (simp add: bounded_linear_vec dfrees extendf_deriv_bounded good_interp)
        have boundedH:"x. bounded_linear (λb. (THE f'. y. (Functions I a has_derivative f' y) (at y))
                          (χ i. dterm_sem
                          (extendf I x)
                                 
                                 (args i) ν)
                          (χ ia. extendf_deriv I i (args ia) ν x b))"
          using bounded_linear_compose  boundedG boundedF by blast
        have eq:"(λx. Blinfun (λb. (THE f'. y. (Functions I a has_derivative f' y) (at y))
                          (χ i. dterm_sem
                                 (extendf I x)
                                 (args i) ν)
                          (χ ia. extendf_deriv I i (args ia) ν x b)))
                          = 
                (λx. blinfun_compose(Blinfun((THE f'. y. (Functions I a has_derivative f' y) (at y))
                          (χ i. dterm_sem
                                 (extendf I x)
                                 (args i) ν) )) (Blinfun(λ b. (χ ia. extendf_deriv I i (args ia) ν x b))))"
          apply(rule ext)
          apply(rule blinfun_eqI)
          subgoal for x ia
            using boundedG[of x]  blinfun_apply_blinfun_compose bounded_linear_Blinfun_apply
          proof -
            have f1: "bounded_linear (λv. FunctionFrechet I a (χ s. dterm_sem (extendf I x) (args s) ν) (χ s. extendf_deriv I i (args s) ν x v))"
              using FunctionFrechet.simps bounded_linear (λb. (THE f'. y. (Functions I a has_derivative f' y) (at y)) (χ i. dterm_sem (extendf I x) (args i) ν) (χ ia. extendf_deriv I i (args ia) ν x b))
              by fastforce          
            have "bounded_linear (FunctionFrechet I a (χ s. dterm_sem (extendf I x) (args s) ν))"
              using good_interp is_interp_def by blast
            then have "blinfun_apply (Blinfun (FunctionFrechet I a (χ s. dterm_sem (extendf I x) (args s) ν))) (χ s. extendf_deriv I i (args s) ν x ia) = blinfun_apply (Blinfun (λv. FunctionFrechet I a (χ s. dterm_sem (extendf I x) (args s) ν) (χ s. extendf_deriv I i (args s) ν x v))) ia"
              using f1 by (simp add: bounded_linear_Blinfun_apply)
            then have "blinfun_apply (Blinfun (FunctionFrechet I a (χ s. dterm_sem (extendf I x) (args s) ν))) (χ s. extendf_deriv I i (args s) ν x ia) = blinfun_apply (Blinfun (λv. FunctionFrechet I a (χ s. dterm_sem (extendf I x) (args s) ν) (χ s. extendf_deriv I i (args s) ν x v))) ia  bounded_linear (λv. χ s. extendf_deriv I i (args s) ν x v)"
              by (metis bounded_linear (λb. χ ia. extendf_deriv I i (args ia) ν x b)) (* failed *)
            then show ?thesis
              by (simp add: bounded_linear_Blinfun_apply)
          qed
        done
        have bounds:"ia x. bounded_linear (extendf_deriv I i (args ia) ν x)" 
          by (simp add: dfrees extendf_deriv_bounded good_interp)
        have vec_bound:"x. bounded_linear (λb. χ ia. extendf_deriv I i (args ia) ν x b)" 
          by (simp add: boundedG)
        have blinfun_vec:"(λx. Blinfun (λb. χ ia. extendf_deriv I i (args ia) ν x b)) = (λx. blinfun_vec (λ ia.  Blinfun(λb. extendf_deriv I i (args ia) ν x b)))"
          apply(rule ext)
          apply(rule blinfun_eqI)
          apply(rule vec_extensionality)
          subgoal for x y ia
          proof -
            have "(χ s. extendf_deriv I i (args s) ν x y) $ ia = blinfun_apply (blinfun_vec (λs. Blinfun (extendf_deriv I i (args s) ν x))) y $ ia"
              by (simp add: bounded_linear_Blinfun_apply bounds)
            then have "(χ s. extendf_deriv I i (args s) ν x y) $ ia = blinfun_apply (blinfun_vec (λs. Blinfun (extendf_deriv I i (args s) ν x))) y $ ia  bounded_linear (λv. χ s. extendf_deriv I i (args s) ν x v)"
              by (metis bounded_linear (λb. χ ia. extendf_deriv I i (args ia) ν x b))
            then show ?thesis
              by (simp add: bounded_linear_Blinfun_apply)
          qed
          done
        have vec_cont:"continuous_on UNIV (λx. blinfun_vec (λ ia.  Blinfun(λb. extendf_deriv I i (args ia) ν x b)))"
          apply(rule continuous_blinfun_vec')
          using "3.IH" by blast
        have cont_intro:" f g s. continuous_on s f  continuous_on s g  continuous_on s (λx. f x  oL  g x)"
          by(auto intro: continuous_intros)
        have cont:"continuous_on UNIV (λx. blinfun_compose(Blinfun((THE f'. y. (Functions I a has_derivative f' y) (at y))
                          (χ i. dterm_sem
                                 Functions = case_sum (Functions I) (λf' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I,
                                    Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I
                                 (args i) ν) )) (Blinfun(λ b. (χ ia. extendf_deriv I i (args ia) ν x b))))"
          apply(rule cont_intro)
           defer
           subgoal using blinfun_vec vec_cont by presburger
          apply(rule continuous_on_compose2[of UNIV "(λx. Blinfun ((THE f'. y. (Functions I a has_derivative f' y) (at y)) x))"])
            subgoal using good_interp unfolding is_interp_def by simp
           apply(rule continuous_on_vec_lambda)
           subgoal for i using extendf_dterm_sem_continuous[OF dfrees[of i] good_interp] by auto
          by auto
        then show " continuous_on UNIV
       (λx. Blinfun (λb. (THE f'. y. (Functions I a has_derivative f' y) (at y))
                          (χ i. dterm_sem
                                 Functions = case_sum (Functions I) (λf' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I,
                                    Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I
                                 (args i) ν)
                          (χ ia. extendf_deriv I i (args ia) ν x b)))"
          using eq apply simp by presburger
        qed
    by simp
next
  case (4 θ1 θ2)
  assume free1:"dfree θ1"
  assume free2:"dfree θ2"
  assume IH1:"continuous_on UNIV (λx. Blinfun (extendf_deriv I i θ1 ν x))"
  assume IH2:"continuous_on UNIV (λx. Blinfun (extendf_deriv I i θ2 ν x))"
  have bound:"x. bounded_linear  (λa. extendf_deriv I i θ1 ν x a + extendf_deriv I i θ2 ν x a)"
    using extendf_deriv_bounded[OF free1 good_interp] extendf_deriv_bounded[OF free2 good_interp]
    by (simp add: bounded_linear_add)
  have eq:"(λx. Blinfun (λa. extendf_deriv I i θ1 ν x a + extendf_deriv I i θ2 ν x a)) = (λx. Blinfun (λa. extendf_deriv I i θ1 ν x a) + Blinfun (λa. extendf_deriv I i θ2 ν x a))"
    apply(rule ext)
    apply(rule blinfun_eqI)
    subgoal for x j
      using bound[of x] extendf_deriv_bounded[OF free1 good_interp] 
      extendf_deriv_bounded[OF free2 good_interp] 
      blinfun.add_left[of "Blinfun (extendf_deriv I i θ1 ν x)" "Blinfun (extendf_deriv I i θ2 ν x)"]
      bounded_linear_Blinfun_apply[of "(extendf_deriv I i θ1 ν x)"]
      bounded_linear_Blinfun_apply[of "(extendf_deriv I i θ2 ν x)"]
      by (simp add: bounded_linear_Blinfun_apply)
    done
  have "continuous_on UNIV (λx. Blinfun (λa. extendf_deriv I i θ1 ν x a) + Blinfun (λa. extendf_deriv I i θ2 ν x a))"
    apply(rule continuous_intros)
    using IH1 IH2 by auto
  then show ?case
    apply simp
    using eq by presburger
next
  case (5 θ1 θ2)
  assume free1:"dfree θ1"
  assume free2:"dfree θ2"
  assume IH1:"continuous_on UNIV (λx. Blinfun (extendf_deriv I i θ1 ν x))"
  assume IH2:"continuous_on UNIV (λx. Blinfun (extendf_deriv I i θ2 ν x))"
  have bounded:"x. bounded_linear (λa. dterm_sem (extendf I x) θ1 ν * extendf_deriv I i θ2 ν x a +
                       extendf_deriv I i θ1 ν x a * dterm_sem (extendf I x) θ2 ν)"
    using extendf_deriv_bounded[OF free1 good_interp] extendf_deriv_bounded[OF free2 good_interp]
    by (simp add: bounded_linear_add bounded_linear_const_mult bounded_linear_mult_const)
  have eq:"(λx. Blinfun (λa. dterm_sem (extendf I x) θ1 ν * extendf_deriv I i θ2 ν x a +
                       extendf_deriv I i θ1 ν x a * dterm_sem (extendf I x) θ2 ν)) = 
           (λx. dterm_sem (extendf I x) θ1 ν *R Blinfun (λa. extendf_deriv I i θ2 ν x a) +
           dterm_sem (extendf I x) θ2 ν *R Blinfun (λa. extendf_deriv I i θ1 ν x a))"
    apply(rule ext)
    apply(rule blinfun_eqI)
    subgoal for x j
      using extendf_deriv_bounded[OF free1 good_interp] extendf_deriv_bounded[OF free2 good_interp] bounded[of x]
      blinfun.scaleR_left 
      bounded_linear_Blinfun_apply[of "Blinfun (extendf_deriv I i θ2 ν x)"]
      bounded_linear_Blinfun_apply[of "Blinfun (extendf_deriv I i θ1 ν x)"]
      mult.commute 
      plus_blinfun.rep_eq[of "dterm_sem (extendf I x) θ1 ν *R Blinfun (extendf_deriv I i θ2 ν x)" "dterm_sem (extendf I x) θ2 ν *R Blinfun (extendf_deriv I i θ1 ν x)"]
      real_scaleR_def
      by (simp add: blinfun.scaleR_left bounded_linear_Blinfun_apply)
    done
  have "continuous_on UNIV (λx. dterm_sem (extendf I x) θ1 ν *R Blinfun (λa. extendf_deriv I i θ2 ν x a) +
           dterm_sem (extendf I x) θ2 ν *R Blinfun (λa. extendf_deriv I i θ1 ν x a))"
    apply(rule continuous_intros)+
      apply(rule extendf_dterm_sem_continuous[OF free1 good_interp])
     apply(rule IH2)
    apply(rule continuous_intros)+
     apply(rule extendf_dterm_sem_continuous[OF free2 good_interp])
    by(rule IH1)
  then show ?case
    unfolding extendf_deriv.simps
    using eq by presburger
qed (auto intro: continuous_intros)
  
lemma extendf_deriv:
  fixes f'::"('sf + 'sz,'sz) trm" and I::"('sf,'sc,'sz) interp"
  assumes free:"dfree f'"
  assumes good_interp:"is_interp I"
  shows "f''. x. ((λR. dterm_sem (extendf I R) f' ν) has_derivative (extendf_deriv I i_f f' ν x)) (at x)"
  using free apply (induction rule: dfree.induct)
  apply(auto)+
   defer
   subgoal for θ1 θ2 x
     apply(rule has_derivative_mult)
      by auto
   subgoal for args i x
     apply(cases "i")
      defer
      apply auto
      subgoal for b using has_derivative_proj' by blast
     subgoal for a
   proof -
     assume dfrees:"(i. dfree (args i))"
     assume IH1:"(ia. x. ((λR. dterm_sem
                      Functions = case_sum (Functions I) (λf' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
                         ODEs = ODEs I, ODEBV = ODEBV I
                      (args ia) ν) has_derivative
                extendf_deriv I i_f (args ia) ν x)
                (at x))"
     then have IH1':"(ia. x. ((λR. dterm_sem
                      Functions = case_sum (Functions I) (λf' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
                         ODEs = ODEs I, ODEBV = ODEBV I
                      (args ia) ν) has_derivative
                extendf_deriv I i_f (args ia) ν x)
                (at x))"
       by auto
     assume a:"i = Inl a"
     have chain:"f f' x s g g'. (f has_derivative f') (at x within s) 
      (g has_derivative g') (at (f x) within f ` s)  (g  f has_derivative g'  f') (at x within s)"
       by (auto intro: derivative_intros)
     let ?f = "(λx. Functions I a x)"
     let ?g = "(λ R. (χ i. dterm_sem
                       Functions = case_sum (Functions I) (λf' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I,
                          Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I
                       (args i) ν))"
     let ?myf' = "(λx. (THE f'. y. (Functions I a has_derivative f' y) (at y)) (?g x))"
     let ?myg' = "(λx. (λν'. χ ia. extendf_deriv I i_f (args ia) ν x ν'))"
     have fg_eq:"(λR. Functions I a
           (χ i. dterm_sem
                  Functions = case_sum (Functions I) (λf' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
                     ODEs = ODEs I, ODEBV = ODEBV I
                  (args i) ν)) = (?f  ?g)"
       by auto
     have "x. ((?f o ?g) has_derivative (?myf' x  ?myg' x)) (at x)"
       apply (rule allI)
       apply (rule diff_chain_at)
       subgoal for xa
         apply (rule has_derivative_vec)
         subgoal for i using IH1'[of i xa] by auto
         done
       subgoal for xa 
       proof -
         have deriv:"x. (Functions I a has_derivative FunctionFrechet I a x) (at x)"
         and cont:"continuous_on UNIV (λx. Blinfun (FunctionFrechet I a x))"
           using good_interp[unfolded is_interp_def] by auto
         show ?thesis
           apply(rule has_derivative_at_withinI)
           using deriv by auto
       qed
      done
    then have "((?f o ?g) has_derivative (?myf' x  ?myg' x)) (at x)" by auto
    then show "((λR. Functions I a
           (χ i. dterm_sem
                  Functions = case_sum (Functions I) (λf' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
                     ODEs = ODEs I, ODEBV = ODEBV I
                  (args i) ν)) has_derivative
              (THE f'. y. (Functions I a has_derivative f' y) (at y))
      (χ i. dterm_sem
             Functions = case_sum (Functions I) (λf' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
                ODEs = ODEs I, ODEBV = ODEBV I
             (args i) ν) 
     (λν'. χ ia. extendf_deriv I i_f (args ia) ν x ν'))
     (at x) "
      using fg_eq by auto
  qed
  done
done

lemma adjoint_safe:
  assumes good_interp:"is_interp I"
  assumes good_subst:"(i f'. SFunctions σ i = Some f'  dfree f') "    
  shows "is_interp (adjoint I σ ν)"
  apply(unfold adjoint_def)
  apply(unfold is_interp_def)
  apply(auto simp del: extendf.simps extendc.simps FunctionFrechet.simps)
   subgoal for x i
     apply(cases "SFunctions σ i = None")
      subgoal
        apply(auto simp del: extendf.simps extendc.simps)
        using good_interp unfolding is_interp_def by simp
      apply(auto  simp del: extendf.simps extendc.simps)
      subgoal for f'
        using good_subst[of i f'] apply (auto  simp del: extendf.simps extendc.simps)
      proof -
        assume some:"SFunctions σ i = Some f'"
        assume free:"dfree f'"
        let ?f = "(λR. dterm_sem (extendf I R) f' ν)"
        let ?Pred = "(λfd. (x. (?f has_derivative (fd x)) (at x)))"
        let ?f''="extendf_deriv I i f' ν"
        have Pf:"?Pred ?f''"
          using extendf_deriv[OF good_subst[of i f'] good_interp, of ν i, OF some]
          by auto
        have "(THE G. (?f has_derivative G) (at x)) = ?f'' x"
          apply(rule the_deriv)
          using Pf by auto
        then have the_eq:"(THE G.  x. (?f has_derivative G x) (at x)) = ?f''"
          using Pf the_all_deriv by auto
        show "((λR. dterm_sem (extendf I R) f' ν) has_derivative (THE f'a. x. ((λR. dterm_sem (extendf I R) f' ν) has_derivative f'a x) (at x)) x) (at x)"
          using the_eq Pf by simp
      qed
      done
    subgoal for i
      apply(cases "SFunctions σ i = None")
       subgoal
         apply(auto  simp del: extendf.simps extendc.simps)
         using good_interp unfolding is_interp_def by simp
      apply(auto  simp del: extendf.simps extendc.simps)
      subgoal for f'
        using good_subst[of i f'] apply (auto  simp del: extendf.simps extendc.simps)
      proof -
        assume some:"SFunctions σ i = Some f'"
        assume free:"dfree f'"
        let ?f = "(λR. dterm_sem (extendf I R) f' ν)"
        let ?Pred = "(λfd. (x. (?f has_derivative (fd x)) (at x)))"
        let ?f''="extendf_deriv I i f' ν"
        have Pf:"?Pred ?f''"
          using extendf_deriv[OF good_subst[of i f'] good_interp, of ν i, OF some]
          by auto
        have "x. (THE G. (?f has_derivative G) (at x)) = ?f'' x"
          apply(rule the_deriv)
          using Pf by auto
        then have the_eq:"(THE G.  x. (?f has_derivative G x) (at x)) = ?f''"
          using Pf the_all_deriv by auto
        have "continuous_on UNIV (λx. Blinfun (?f'' x))"
          by(rule extendf_deriv_continuous[OF free good_interp])
        show "continuous_on UNIV (λx. Blinfun ((THE f'a. x. ((λR. dterm_sem (extendf I R) f' ν) has_derivative f'a x) (at x)) x))"
          using the_eq Pf 
          by (simp add: continuous_on UNIV (λx. Blinfun (extendf_deriv I i f' ν x)))
      qed
    done
  done

lemma adjointFO_safe:
  assumes good_interp:"is_interp I"
  assumes good_subst:"(i. dsafe (σ i))"
  shows "is_interp (adjointFO I σ ν)"
  apply(unfold adjointFO_def)
  apply(unfold is_interp_def)
  apply(auto simp del: extendf.simps extendc.simps FunctionFrechet.simps)
   subgoal for x i
     apply(cases "i")
      subgoal
        apply(auto  simp del: extendf.simps extendc.simps)
        using good_interp unfolding is_interp_def by simp
     apply(auto  simp del: extendf.simps extendc.simps)
     subgoal for f'
     proof -
       assume some:"i = Inr f'"
       have free:"dsafe (σ f')" using good_subst by auto
       let ?f = "(λ_. dterm_sem I (σ f') ν)"
       let ?Pred = "(λfd. (x. (?f has_derivative (fd x)) (at x)))"
       let ?f''="(λ_ _. 0)"
       have Pf:"?Pred ?f''"
       proof (induction "σ f'")
       qed (auto)
       have "(THE G. (?f has_derivative G) (at x)) = ?f'' x"
         apply(rule the_deriv)
         using Pf by auto
       then have the_eq:"(THE G.  x. (?f has_derivative G x) (at x)) = ?f''"
         using Pf the_all_deriv[of ?f ?f''] by auto
       have another_eq:"(THE f'a. x. ((λ_. dterm_sem I (σ f') ν) has_derivative f'a x) (at x)) x = (λ _. 0)"
         using Pf by (simp add: the_eq) 
       then show "((λ_. dterm_sem I (σ f') ν) has_derivative (THE f'a. x. ((λ_. dterm_sem I (σ f') ν) has_derivative f'a x) (at x)) x) (at x)"
         using the_eq Pf by simp
       qed
    done
  subgoal for i
    apply(cases i)
     subgoal
       apply(auto  simp del: extendf.simps extendc.simps)
       using good_interp unfolding is_interp_def by simp
    apply(auto  simp del: extendf.simps extendc.simps)
    subgoal for f'
      using good_subst[of f'] 
    proof -
      assume some:"i = Inr f'"
      have free:"dsafe (σ f')" using good_subst by auto
      let ?f = "(λR. dterm_sem I (σ f') ν)"
      let ?Pred = "(λfd. (x. (?f has_derivative (fd x)) (at x)))"
      let ?f''="(λ_ _. 0)" (* *)
      have Pf:"?Pred ?f''" by simp
      have "x. (THE G. (?f has_derivative G) (at x)) = ?f'' x"
        apply(rule the_deriv)
        using Pf by auto
      then have the_eq:"(THE G.  x. (?f has_derivative G x) (at x)) = ?f''"
        using Pf the_all_deriv[of "(λR. dterm_sem I (σ f') ν)" "(λ_ _. 0)"]
        by blast
      then have blin_cont:"continuous_on UNIV (λx. Blinfun (?f'' x))"
        by (simp add: continuous_on_const)
      have truth:"(λx. Blinfun ((THE f'a. x. ((λ_. dterm_sem I (σ f') ν) has_derivative f'a x) (at x)) x))
        = (λx. Blinfun (λ _. 0))"
        apply(rule ext)
        apply(rule blinfun_eqI)
        by (simp add: local.the_eq)
      then show "continuous_on UNIV (λx. Blinfun ((THE f'a. x. ((λ_. dterm_sem I (σ f') ν) has_derivative f'a x) (at x)) x))"
        using truth 
        by (metis (mono_tags, lifting) blin_cont continuous_on_eq)
      qed
    done
  done

subsection ‹Lemmas about adjoint interpretations›
lemma adjoint_consequence:"(f f'. SFunctions σ f = Some f'  dsafe f')  (f f'. SPredicates σ f = Some f'  fsafe f')  Vagree ν ω (FVS σ)  adjoint I σ ν = adjoint I σ ω"
  apply(unfold FVS_def)
  apply(auto)
  apply(unfold adjoint_def)
  apply(rule interp_eq)
       apply(auto simp add: fun_eq_iff)
    subgoal for xa xaa 
      apply(cases "SFunctions σ xa")
       apply(auto)
      subgoal for a 
      proof -
        assume safes:"(f f'. SFunctions σ f = Some f'  dsafe f')"
        assume agrees:"Vagree ν ω (x. SFV σ x)"
        assume some:"SFunctions σ xa = Some a"
        from safes some have safe:"dsafe a" by auto
        have sub:"SFV σ (Inl xa)  (x. SFV σ x)"
          by blast
        from agrees 
        have "Vagree ν ω (SFV σ (Inl xa))"
          using agree_sub[OF sub agrees] by auto
        then have agree:"Vagree ν ω (FVT a)"
          using some by auto
        show "?thesis"
          using coincidence_dterm[of a, OF safes[of xa a, OF some] agree] by auto
      qed
    done
   subgoal for xa xaa 
    apply(cases "SPredicates σ xa")
     apply(auto)
    subgoal for a 
    proof -
      assume safes:"(f f'. SPredicates σ f = Some f'  fsafe f')"
      assume agrees:"Vagree ν ω (x. SFV σ x)"
      assume some:"SPredicates σ xa = Some a"
      assume sem:"ν  fml_sem Functions = case_sum (Functions I) (λf' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
                  ODEs = ODEs I, ODEBV = ODEBV I
        a"
      from safes some have safe:"fsafe a" by auto
      have sub:"SFV σ (Inr (Inr xa))  (x. SFV σ x)"
        by blast
      from agrees 
      have "Vagree ν ω (SFV σ (Inr (Inr xa)))"
        using agree_sub[OF sub agrees] by auto
      then have agree:"Vagree ν ω (FVF a)"
        using some by auto
      let ?I' = "Functions = case_sum (Functions I) (λf' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
                  ODEs = ODEs I, ODEBV = ODEBV I"
      have IA:"S. Iagree ?I' ?I' (SIGF a)" using Iagree_refl by auto
      show "?thesis"
        using coincidence_formula[of a, OF safes[of xa a, OF some] IA agree] sem by auto
    qed
    done
   subgoal for xa xaa 
    apply(cases "SPredicates σ xa")
     apply(auto)
    subgoal for a 
    proof -
      assume safes:"(f f'. SPredicates σ f = Some f'  fsafe f')"
      assume agrees:"Vagree ν ω (x. SFV σ x)"
      assume some:"SPredicates σ xa = Some a"
      assume sem:"ω  fml_sem Functions = case_sum (Functions I) (λf' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
                  ODEs = ODEs I, ODEBV = ODEBV I
        a"
      from safes some have safe:"fsafe a" by auto
      have sub:"SFV σ (Inr (Inr xa))  (x. SFV σ x)"
        by blast
      from agrees 
      have "Vagree ν ω (SFV σ (Inr (Inr xa)))"
        using agree_sub[OF sub agrees] by auto
      then have agree:"Vagree ν ω (FVF a)"
        using some by auto
      let ?I' = "Functions = case_sum (Functions I) (λf' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
                  ODEs = ODEs I, ODEBV = ODEBV I"
      have IA:"S. Iagree ?I' ?I' (SIGF a)" using Iagree_refl by auto
      show "?thesis"
        using coincidence_formula[of a, OF safes[of xa a, OF some] IA agree] sem by auto
    qed
  done    
done

lemma SIGT_plus1:"Vagree ν ω (iSIGT (Plus t1 t2). case SFunctions σ i of Some x  FVT x | None  {}) 
   Vagree ν ω (iSIGT t1. case SFunctions σ i of Some x  FVT x | None  {})"
  unfolding Vagree_def by auto

lemma SIGT_plus2:"Vagree ν ω (iSIGT (Plus t1 t2). case SFunctions σ i of Some x  FVT x | None  {}) 
   Vagree ν ω (iSIGT t2. case SFunctions σ i of Some x  FVT x | None  {})"
  unfolding Vagree_def by auto

lemma SIGT_times1:"Vagree ν ω (iSIGT (Times t1 t2). case SFunctions σ i of Some x  FVT x | None  {}) 
   Vagree ν ω (iSIGT t1. case SFunctions σ i of Some x  FVT x | None  {})"
  unfolding Vagree_def by auto

lemma SIGT_times2:"Vagree ν ω (iSIGT (Times t1 t2). case SFunctions σ i of Some x  FVT x | None  {}) 
   Vagree ν ω (iSIGT t2. case SFunctions σ i of Some x  FVT x | None  {})"
  unfolding Vagree_def by auto

lemma uadmit_sterm_adjoint':
  assumes dsafe:"f f'. SFunctions σ f = Some f'  dsafe f'"
  assumes fsafe:"f f'. SPredicates σ f = Some f'  fsafe f'"
  shows  "Vagree ν ω (iSIGT θ. case SFunctions σ i of Some x  FVT x | None  {})  sterm_sem (adjoint I σ ν) θ = sterm_sem (adjoint I σ ω) θ"
proof (induct "θ")
  case (Plus θ1 θ2)
  assume IH1:"Vagree ν ω (iSIGT θ1. case SFunctions σ i of Some a  FVT a | None  {})  sterm_sem (local.adjoint I σ ν) θ1 = sterm_sem (local.adjoint I σ ω) θ1"
  assume IH2:"Vagree ν ω (iSIGT θ2. case SFunctions σ i of Some a  FVT a | None  {})  sterm_sem (local.adjoint I σ ν) θ2 = sterm_sem (local.adjoint I σ ω) θ2"
  assume VA:"Vagree ν ω (iSIGT (Plus θ1 θ2). case SFunctions σ i of Some a  FVT a | None  {})"
  then show ?case
    using IH1[OF SIGT_plus1[OF VA]] IH2[OF SIGT_plus2[OF VA]] by auto
next
  case (Times θ1 θ2)
  assume IH1:"Vagree ν ω (iSIGT θ1. case SFunctions σ i of Some a  FVT a | None  {})  sterm_sem (local.adjoint I σ ν) θ1 = sterm_sem (local.adjoint I σ ω) θ1"
  assume IH2:"Vagree ν ω (iSIGT θ2. case SFunctions σ i of Some a  FVT a | None  {})  sterm_sem (local.adjoint I σ ν) θ2 = sterm_sem (local.adjoint I σ ω) θ2"
  assume VA:"Vagree ν ω (iSIGT (Times θ1 θ2). case SFunctions σ i of Some a  FVT a | None  {})"    
  then show ?case
    using IH1[OF SIGT_times1[OF VA]] IH2[OF SIGT_times2[OF VA]] by auto
next
  case (Function x1a x2a)
  assume IH:"x. x  range x2a  Vagree ν ω (iSIGT x. case SFunctions σ i of Some a  FVT a | None  {}) 
    sterm_sem (local.adjoint I σ ν) x = sterm_sem (local.adjoint I σ ω) x"
  from IH have IH':"j. Vagree ν ω (iSIGT (x2a j). case SFunctions σ i of Some a  FVT a | None  {}) 
    sterm_sem (local.adjoint I σ ν) (x2a j) = sterm_sem (local.adjoint I σ ω) (x2a j)"
    using rangeI by auto
  assume VA:"Vagree ν ω (iSIGT ($f x1a x2a). case SFunctions σ i of Some a  FVT a | None  {})"
  from VA have VAs:"j. Vagree ν ω (iSIGT (x2a j). case SFunctions σ i of Some a  FVT a | None  {})"
    unfolding Vagree_def SIGT.simps using rangeI by blast
  have SIGT:"x1a  SIGT ($f x1a x2a)" by auto
  have VAsub:"a. SFunctions σ x1a = Some a  (FVT a)  (iSIGT ($f x1a x2a). case SFunctions σ i of Some a  FVT a | None  {})"
    using SIGT by auto
  have VAf:"a. SFunctions σ x1a = Some a  Vagree ν ω (FVT a)"
    using agree_sub[OF VAsub VA] by auto
  then show ?case 
    using IH'[OF VAs] apply (auto simp add: fun_eq_iff)
    apply(cases "SFunctions σ x1a")
     defer
     subgoal for x a
     proof -
       assume VA:"(a. SFunctions σ x1a = Some a  Vagree ν ω (FVT a))"
       assume sems:"(j. x. sterm_sem (local.adjoint I σ ν) (x2a j) x = sterm_sem (local.adjoint I σ ω) (x2a j) x)"
       assume some:"SFunctions σ x1a = Some a"
       note FVT = VAf[OF some]
       have dsem:"R . dterm_sem (extendf I R) a ν = dterm_sem (extendf I R) a ω"
         using coincidence_dterm[OF dsafe[OF some] FVT] by auto
       have "R. Functions (local.adjoint I σ ν) x1a R = Functions (local.adjoint I σ ω) x1a R"
         using dsem some unfolding adjoint_def by auto
       then show "Functions (local.adjoint I σ ν) x1a (χ i. sterm_sem (local.adjoint I σ ω) (x2a i) x) =
                 Functions (local.adjoint I σ ω) x1a (χ i. sterm_sem (local.adjoint I σ ω) (x2a i) x)"
         by auto
     qed
    unfolding adjoint_def apply auto    
    done
qed (auto)  
  
― ‹Not used, but good practice for dterm› adjoint›
lemma uadmit_sterm_adjoint:
  assumes TUA:"TUadmit σ θ U"
  assumes VA:"Vagree ν ω (-U)"
  assumes dsafe:"f f'. SFunctions σ f = Some f'  dsafe f'"
  assumes fsafe:"f f'. SPredicates σ f = Some f'  fsafe f'"
  shows  "sterm_sem (adjoint I σ ν) θ = sterm_sem (adjoint I σ ω) θ"
proof -
  have duh:"A B. A  B = {}  A  -B"
    by auto
  have "x. x  (iSIGT θ. case SFunctions σ i of Some x  FVT x | None  {})  x  (-U)"
    using TUA unfolding TUadmit_def by auto
  then have sub1:"(iSIGT θ. case SFunctions σ i of Some x  FVT x | None  {})  -U"
    by auto
  then have VA':"Vagree ν ω (iSIGT θ. case SFunctions σ i of Some x  FVT x | None  {})"
    using agree_sub[OF sub1 VA] by auto
  then show "?thesis" using uadmit_sterm_adjoint'[OF dsafe fsafe VA'] by auto
qed

lemma uadmit_sterm_ntadjoint':
  assumes dsafe:"i. dsafe (σ i)"
  shows  "Vagree ν ω (( i{i. Inr i  SIGT θ}. FVT (σ i)))  sterm_sem (adjointFO I σ ν) θ = sterm_sem (adjointFO I σ ω) θ"
proof (induct "θ")
  case (Plus θ1 θ2)
  assume IH1:"Vagree ν ω ( i{i. Inr i  SIGT θ1}. FVT (σ i))  sterm_sem (adjointFO I σ ν) θ1 = sterm_sem (adjointFO I σ ω) θ1"
  assume IH2:"Vagree ν ω ( i{i. Inr i  SIGT θ2}. FVT (σ i))  sterm_sem (adjointFO I σ ν) θ2 = sterm_sem (adjointFO I σ ω) θ2"
  assume VA:"Vagree ν ω (( i{i. Inr i  SIGT (Plus θ1 θ2)}. FVT (σ i)))"
  from VA 
    have VA1:"Vagree ν ω ( i{i. Inr i  SIGT θ1}. FVT (σ i))"
    and  VA2:"Vagree ν ω ( i{i. Inr i  SIGT θ2}. FVT (σ i))" unfolding Vagree_def by auto
  then show ?case
    using IH1[OF VA1] IH2[OF VA2] by auto
next
  case (Times θ1 θ2)
  assume IH1:"Vagree ν ω ( i{i. Inr i  SIGT θ1}. FVT (σ i))  sterm_sem (adjointFO I σ ν) θ1 = sterm_sem (adjointFO I σ ω) θ1"
  assume IH2:"Vagree ν ω ( i{i. Inr i  SIGT θ2}. FVT (σ i))  sterm_sem (adjointFO I σ ν) θ2 = sterm_sem (adjointFO I σ ω) θ2"
  assume VA:"Vagree ν ω (( i{i. Inr i  SIGT (Times θ1 θ2)}. FVT (σ i)))"
  from VA 
  have VA1:"Vagree ν ω ( i{i. Inr i  SIGT θ1}. FVT (σ i))"
  and  VA2:"Vagree ν ω ( i{i. Inr i  SIGT θ2}. FVT (σ i))" unfolding Vagree_def by auto
  then show ?case
    using IH1[OF VA1] IH2[OF VA2] by auto
next
  case (Function x1a x2a) 
  assume IH:"x. x  range x2a  Vagree ν ω ( i{i. Inr i  SIGT x}. FVT (σ i)) 
    sterm_sem (adjointFO I σ ν) x = sterm_sem (adjointFO I σ ω) x"
  from IH have IH':"j. Vagree ν ω ( i{i. Inr i  SIGT (x2a j)}. FVT (σ i)) 
    sterm_sem (adjointFO I σ ν) (x2a j) = sterm_sem (adjointFO I σ ω) (x2a j)"
    using rangeI by auto
  assume VA:"Vagree ν ω ( i{i. Inr i  SIGT ($f x1a x2a)}. FVT (σ i)) "
  from VA have VAs:"j. Vagree ν ω ( i{i. Inr i  SIGT (x2a j)}. FVT (σ i))"
    unfolding Vagree_def SIGT.simps using rangeI by blast
  have SIGT:"x1a  SIGT ($f x1a x2a)" by auto
  have VAsub:"a. x1a = Inr a  (FVT (σ a))  ( i{i. Inr i  SIGT ($f x1a x2a)}. FVT (σ i))"
    using SIGT by auto
  have VAf:"a. x1a = Inr a Vagree ν ω (FVT (σ a))"
    using agree_sub[OF VAsub VA] by auto
  then show ?case 
    using IH'[OF VAs] apply (auto simp add: fun_eq_iff)
    apply(cases "x1a")
     defer
     subgoal for x a
     proof -
       assume VA:"(a.  x1a = Inr a  Vagree ν ω (FVT (σ a)))"
       assume sems:"(j. x. sterm_sem (adjointFO I σ ν) (x2a j) x = sterm_sem (adjointFO I σ ω) (x2a j) x)"
       assume some:"x1a = Inr a"
       note FVT = VAf[OF some]
       from dsafe have dsafer:"i. dsafe (σ i)" using dfree_is_dsafe by auto
       have dsem:"dterm_sem I (σ a) ν = dterm_sem I (σ a) ω"
         using coincidence_dterm[OF dsafer FVT] some by auto
       then have "R. Functions (adjointFO I σ ν) x1a R = Functions (adjointFO I σ ω) x1a R"
         using some unfolding adjoint_def unfolding adjointFO_def by auto
       then show "Functions (adjointFO I σ ν) x1a (χ i. sterm_sem (adjointFO I σ ω) (x2a i) x) =
                  Functions (adjointFO I σ ω) x1a (χ i. sterm_sem (adjointFO I σ ω) (x2a i) x)"
         by auto
     qed
    unfolding adjointFO_def by auto
qed (auto) 
  
lemma uadmit_sterm_ntadjoint:
  assumes TUA:"NTUadmit σ θ U"
  assumes VA:"Vagree ν ω (-U)"
  assumes dsafe:"i . dsafe (σ i)"
  assumes good_interp:"is_interp I"
  shows  "sterm_sem (adjointFO I σ ν) θ = sterm_sem (adjointFO I σ ω) θ"
proof -
  have duh:"A B. A  B = {}  A  -B"
    by auto
  have "x. x  (( i{i. Inr i  SIGT θ}. FVT (σ i)))  x  (-U)"
    using TUA unfolding NTUadmit_def by auto
  then have sub1:"(i{i. Inr i  SIGT θ}. FVT (σ i))  -U"
    by auto
  then have VA':"Vagree ν ω (i{i. Inr i  SIGT θ}. FVT (σ i))"
    using agree_sub[OF sub1 VA] by auto
  then show "?thesis" using uadmit_sterm_ntadjoint'[OF  dsafe VA'] by auto
qed

lemma uadmit_dterm_adjoint':
  assumes dfree:"f f'. SFunctions σ f = Some f'  dfree f'"
  assumes fsafe:"f f'. SPredicates σ f = Some f'  fsafe f'"
  assumes good_interp:"is_interp I"
  shows  "ν ω. Vagree ν ω (iSIGT θ. case SFunctions σ i of Some x  FVT x | None  {})  dsafe θ  dterm_sem (adjoint I σ ν) θ = dterm_sem (adjoint I σ ω) θ"
proof (induct "θ")
  case (Plus θ1 θ2)
  assume IH1:"ν ω. Vagree ν ω (iSIGT θ1. case SFunctions σ i of Some a  FVT a | None  {})  dsafe θ1  dterm_sem (local.adjoint I σ ν) θ1 = dterm_sem (local.adjoint I σ ω) θ1"
  assume IH2:"ν ω. Vagree ν ω (iSIGT θ2. case SFunctions σ i of Some a  FVT a | None  {})  dsafe θ2  dterm_sem (local.adjoint I σ ν) θ2 = dterm_sem (local.adjoint I σ ω) θ2"
  assume VA:"Vagree ν ω (iSIGT (Plus θ1 θ2). case SFunctions σ i of Some a  FVT a | None  {})"
  assume safe:"dsafe (Plus θ1 θ2)"
  then show ?case
    using IH1[OF SIGT_plus1[OF VA]] IH2[OF SIGT_plus2[OF VA]] by auto
next
  case (Times θ1 θ2)
  assume IH1:"ν ω. Vagree ν ω (iSIGT θ1. case SFunctions σ i of Some a  FVT a | None  {})  dsafe θ1  dterm_sem (local.adjoint I σ ν) θ1 = dterm_sem (local.adjoint I σ ω) θ1"
  assume IH2:"ν ω. Vagree ν ω (iSIGT θ2. case SFunctions σ i of Some a  FVT a | None  {})  dsafe θ2  dterm_sem (local.adjoint I σ ν) θ2 = dterm_sem (local.adjoint I σ ω) θ2"
  assume VA:"Vagree ν ω (iSIGT (Times θ1 θ2). case SFunctions σ i of Some a  FVT a | None  {})"
  assume safe:"dsafe (Times θ1 θ2)"
  then show ?case
    using IH1[OF SIGT_times1[OF VA]] IH2[OF SIGT_times2[OF VA]] by auto
next
  case (Function x1a x2a)
  assume IH:"x. ν ω. x  range x2a  Vagree ν ω (iSIGT x. case SFunctions σ i of Some a  FVT a | None  {}) 
    dsafe x  dterm_sem (local.adjoint I σ ν) x = dterm_sem (local.adjoint I σ ω) x"
  assume safe:"dsafe (Function x1a x2a)"
  from safe have safes:"j. dsafe (x2a j)" by auto
  from IH have IH':"j. Vagree ν ω (iSIGT (x2a j). case SFunctions σ i of Some a  FVT a | None  {}) 
    dterm_sem (local.adjoint I σ ν) (x2a j) = dterm_sem (local.adjoint I σ ω) (x2a j)"
    using rangeI safes by auto
  assume VA:"Vagree ν ω (iSIGT ($f x1a x2a). case SFunctions σ i of Some a  FVT a | None  {})"
  from VA have VAs:"j. Vagree ν ω (iSIGT (x2a j). case SFunctions σ i of Some a  FVT a | None  {})"
    unfolding Vagree_def SIGT.simps using rangeI by blast
  have SIGT:"x1a  SIGT ($f x1a x2a)" by auto
  have VAsub:"a. SFunctions σ x1a = Some a  (FVT a)  (iSIGT ($f x1a x2a). case SFunctions σ i of Some a  FVT a | None  {})"
    using SIGT by auto
  have VAf:"a. SFunctions σ x1a = Some a  Vagree ν ω (FVT a)"
    using agree_sub[OF VAsub VA] by auto
  then show ?case 
    using IH'[OF VAs] apply (auto simp add: fun_eq_iff)
    apply(cases "SFunctions σ x1a")
     defer
     subgoal for x1 x2 a
     proof -
       assume VA:"(a. SFunctions σ x1a = Some a  Vagree ν ω (FVT a))"
       assume sems:"(j. x1 x2. dterm_sem (local.adjoint I σ ν) (x2a j) (x1,x2) = dterm_sem (local.adjoint I σ ω) (x2a j) (x1,x2))"
       assume some:"SFunctions σ x1a = Some a"
       note FVT = VAf[OF some]
       have dsafe:"f f'. SFunctions σ f = Some f'  dsafe f'"
         using dfree dfree_is_dsafe by auto
       have dsem:"R . dterm_sem (extendf I R) a ν = dterm_sem (extendf I R) a ω"
         using coincidence_dterm[OF dsafe[OF some] FVT] by auto
       have "R. Functions (local.adjoint I σ ν) x1a R = Functions (local.adjoint I σ ω) x1a R"
         using dsem some unfolding adjoint_def by auto
       then show "Functions (local.adjoint I σ ν) x1a (χ i. dterm_sem (local.adjoint I σ ω) (x2a i) (x1,x2)) =
                  Functions (local.adjoint I σ ω) x1a (χ i. dterm_sem (local.adjoint I σ ω) (x2a i) (x1,x2))"
         by auto
      qed
  unfolding adjoint_def apply auto    
  done
next
  case (Differential θ)
  assume IH:"ν ω. Vagree ν ω (iSIGT θ. case SFunctions σ i of Some a  FVT a | None  {})  dsafe θ  dterm_sem (local.adjoint I σ ν) θ = dterm_sem (local.adjoint I σ ω) θ"
  assume VA:"Vagree ν ω (iSIGT (Differential θ). case SFunctions σ i of Some a  FVT a | None  {})"
  assume safe:"dsafe (Differential θ)"
  then have free:"dfree θ" by (auto dest: dsafe.cases)
  from VA have VA':"Vagree ν ω (iSIGT θ. case SFunctions σ i of Some a  FVT a | None  {})"
    by auto
  have dsafe:"f f'. SFunctions σ f = Some f'  dsafe f'"
    using dfree dfree_is_dsafe by auto
  have sem:"sterm_sem (local.adjoint I σ ν) θ = sterm_sem (local.adjoint I σ ω) θ"
    using uadmit_sterm_adjoint'[OF dsafe fsafe VA', of "λ x y. x" "λ x y. x" I] by auto
  have good1:"is_interp (adjoint I σ ν)" using adjoint_safe[OF good_interp dfree] by auto
  have good2:"is_interp (adjoint I σ ω)" using adjoint_safe[OF good_interp dfree] by auto
  have frech:"frechet (local.adjoint I σ ν) θ = frechet (local.adjoint I σ ω) θ"
    apply (auto simp add: fun_eq_iff)
    subgoal for a b
      using sterm_determines_frechet [OF good1 good2 free free sem, of "(a,b)"] by auto
    done
  then show "dterm_sem (local.adjoint I σ ν) (Differential θ) = dterm_sem (local.adjoint I σ ω) (Differential θ)"
    by (auto simp add: directional_derivative_def)
qed (auto)  

lemma uadmit_dterm_adjoint:
  assumes TUA:"TUadmit σ θ U"
  assumes VA:"Vagree ν ω (-U)"
  assumes dfree:"f f'. SFunctions σ f = Some f'  dfree f'"
  assumes fsafe:"f f'. SPredicates σ f = Some f'   fsafe f'"
  assumes dsafe:"dsafe θ"
  assumes good_interp:"is_interp I"
  shows  "dterm_sem (adjoint I σ ν) θ = dterm_sem (adjoint I σ ω) θ"
proof -
  have duh:"A B. A  B = {}  A  -B"
    by auto
  have "x. x  (iSIGT θ. case SFunctions σ i of Some x  FVT x | None  {})  x  (-U)"
    using TUA unfolding TUadmit_def by auto
  then have sub1:"(iSIGT θ. case SFunctions σ i of Some x  FVT x | None  {})  -U"
    by auto
  then have VA':"Vagree ν ω (iSIGT θ. case SFunctions σ i of Some x  FVT x | None  {})"
    using agree_sub[OF sub1 VA] by auto
  then show "?thesis" using uadmit_dterm_adjoint'[OF dfree fsafe good_interp VA' dsafe] 
    by auto
qed

lemma uadmit_dterm_ntadjoint':
  assumes dfree:"i. dsafe (σ i)"
  assumes good_interp:"is_interp I"
  shows  "ν ω. Vagree ν ω ( i{i. Inr i  SIGT θ}. FVT (σ i))  dsafe θ  dterm_sem (adjointFO I σ ν) θ = dterm_sem (adjointFO I σ ω) θ"
proof (induct "θ")
  case (Plus θ1 θ2 ν ω)
  assume IH1:"ν ω. Vagree ν ω ( i{i. Inr i  SIGT θ1}. FVT (σ i))  dsafe θ1  dterm_sem (adjointFO I σ ν) θ1 = dterm_sem (adjointFO I σ ω) θ1"
  assume IH2:"ν ω. Vagree ν ω ( i{i. Inr i  SIGT θ2}. FVT (σ i))  dsafe θ2  dterm_sem (adjointFO I σ ν) θ2 = dterm_sem (adjointFO I σ ω) θ2"
  assume VA:"Vagree ν ω ( i{i. Inr i  SIGT (Plus θ1 θ2)}. FVT (σ i))"
  then have VA1:"Vagree ν ω ( i{i. Inr i  SIGT θ1}. FVT (σ i))"
    and VA2:"Vagree ν ω ( i{i. Inr i  SIGT θ2}. FVT (σ i))"
    unfolding Vagree_def by auto
  assume safe:"dsafe (Plus θ1 θ2)"
  show ?case 
    using IH1[OF VA1] IH2[OF VA2] safe by auto
next
  case (Times θ1 θ2 ν ω)
  assume IH1:"ν ω. Vagree ν ω ( i{i. Inr i  SIGT θ1}. FVT (σ i))  dsafe θ1  dterm_sem (adjointFO I σ ν) θ1 = dterm_sem (adjointFO I σ ω) θ1"
  assume IH2:"ν ω. Vagree ν ω ( i{i. Inr i  SIGT θ2}. FVT (σ i))  dsafe θ2  dterm_sem (adjointFO I σ ν) θ2 = dterm_sem (adjointFO I σ ω) θ2"
  assume VA:"Vagree ν ω ( i{i. Inr i  SIGT (Times θ1 θ2)}. FVT (σ i))"
  then have VA1:"Vagree ν ω ( i{i. Inr i  SIGT θ1}. FVT (σ i))"
    and VA2:"Vagree ν ω ( i{i. Inr i  SIGT θ2}. FVT (σ i))"
    unfolding Vagree_def by auto
  assume safe:"dsafe (Times θ1 θ2)"
  show ?case 
    using IH1[OF VA1] IH2[OF VA2] safe by auto
next
  case (Function x1a x2a)
    assume IH:"x. ν ω. x  range x2a  Vagree ν ω ( i{i. Inr i  SIGT x}. FVT (σ i)) 
      dsafe x  dterm_sem (adjointFO I σ ν) x = dterm_sem (adjointFO I σ ω) x"
    assume safe:"dsafe (Function x1a x2a)"
    from safe have safes:"j. dsafe (x2a j)" by auto
    from IH have IH':"j. Vagree ν ω ( i{i. Inr i  SIGT (x2a j)}. FVT (σ i)) 
      dterm_sem (adjointFO I σ ν) (x2a j) = dterm_sem (adjointFO I σ ω) (x2a j)"
      using rangeI safes by auto
    assume VA:"Vagree ν ω ( i{i. Inr i  SIGT ($f x1a x2a)}. FVT (σ i))"
    from VA have VAs:"j. Vagree ν ω ( i{i. Inr i  SIGT (x2a j)}. FVT (σ i))"
      unfolding Vagree_def SIGT.simps using rangeI by blast
    have SIGT:"x1a  SIGT ($f x1a x2a)" by auto
    have VAsub:"a. x1a = Inr a (FVT (σ a))  ( i{i. Inr i  SIGT ($f x1a x2a)}. FVT (σ i))"
      using SIGT by auto
    have VAf:"a. x1a = Inr a  Vagree ν ω (FVT (σ a))"
      using agree_sub[OF VAsub VA] by auto
  then show ?case 
    using IH'[OF VAs] apply (auto simp add: fun_eq_iff)
    apply(cases "x1a")
     defer
     subgoal for x1 x2 a
     proof -
       assume VA:"(a. x1a = Inr a  Vagree ν ω (FVT (σ a)))"
       assume sems:"(j. x1 x2. dterm_sem (adjointFO I σ ν) (x2a j) (x1,x2) = dterm_sem (adjointFO I σ ω) (x2a j) (x1,x2))"
       assume some:"x1a = Inr a"
       note FVT = VAf[OF some]
       have dsafe:"i. dsafe (σ i)"
         using dfree dfree_is_dsafe by auto
       have dsem:"R . dterm_sem I (σ a) ν = dterm_sem I (σ a) ω"
         using coincidence_dterm[OF dsafe FVT] by auto
       have "R. Functions (adjointFO I σ ν) x1a R = Functions (adjointFO I σ ω) x1a R"
         using dsem some unfolding adjointFO_def by auto
       then show "Functions (adjointFO I σ ν) x1a (χ i. dterm_sem (adjointFO I σ ω) (x2a i) (x1,x2)) =
                  Functions (adjointFO I σ ω) x1a (χ i. dterm_sem (adjointFO I σ ω) (x2a i) (x1,x2))"
         by auto
     qed
    unfolding adjointFO_def apply auto    
    done
next
  case (Differential θ)
  assume IH:"ν ω. Vagree ν ω ( i{i. Inr i  SIGT θ}. FVT (σ i))  dsafe θ  dterm_sem (adjointFO I σ ν) θ = dterm_sem (adjointFO I σ ω) θ"
  assume VA:"Vagree ν ω ( i{i. Inr i  SIGT (Differential θ)}. FVT (σ i))"
  assume safe:"dsafe (Differential θ)"
  then have free:"dfree θ" by (auto dest: dsafe.cases)
  from VA have VA':"Vagree ν ω ( i{i. Inr i  SIGT θ}. FVT (σ i))"
    by auto
  have dsafe:"i. dsafe (σ i)"
    using dfree dfree_is_dsafe by auto
  have sem:"sterm_sem (adjointFO I σ ν) θ = sterm_sem (adjointFO I σ ω) θ"
    using uadmit_sterm_ntadjoint'[OF dsafe  VA'] by auto
  have good1:"is_interp (adjointFO I σ ν)" using adjointFO_safe[OF good_interp dsafe, of "λi. i"] by auto
  have good2:"is_interp (adjointFO I σ ω)" using adjointFO_safe[OF good_interp dsafe, of "λi. i"] by auto
  have frech:"frechet (adjointFO I σ ν) θ = frechet (adjointFO I σ ω) θ"
    apply (auto simp add: fun_eq_iff)
    subgoal for a b
      using sterm_determines_frechet [OF good1 good2 free free sem, of "(a,b)"] by auto
    done
  then show "dterm_sem (adjointFO I σ ν) (Differential θ) = dterm_sem (adjointFO I σ ω) (Differential θ)"
    by (auto simp add: directional_derivative_def)
qed (auto)  

lemma uadmit_dterm_ntadjoint:
  assumes TUA:"NTUadmit σ θ U"
  assumes VA:"Vagree ν ω (-U)"
  assumes dfree:"i . dsafe (σ i)"
  assumes dsafe:"dsafe θ"
  assumes good_interp:"is_interp I"
  shows  "dterm_sem (adjointFO I σ ν) θ = dterm_sem (adjointFO I σ ω) θ"
proof -
  have duh:"A B. A  B = {}  A  -B"
    by auto
  have duh:"A B. A  B = {}  A  -B"
    by auto
  have "x. x  ( i{i. Inr i  SIGT θ}. FVT (σ i))  x  (-U)"
    using TUA unfolding NTUadmit_def by auto
  then have sub1:"( i{i. Inr i  SIGT θ}. FVT (σ i))  -U"
    by auto
  then have VA':"Vagree ν ω ( i{i. Inr i  SIGT θ}. FVT (σ i))"
    using agree_sub[OF sub1 VA] by auto
  then show "?thesis" using uadmit_dterm_ntadjoint'[OF dfree good_interp VA' dsafe] 
    by auto
qed

definition ssafe ::"('sf, 'sc, 'sz) subst  bool"
where "ssafe σ 
  ( i f'. SFunctions σ i = Some f'  dfree f')  
  ( f f'. SPredicates σ f = Some f'   fsafe f') 
  ( f f'. SPrograms σ f = Some f'   hpsafe f') 
  ( f f'. SODEs σ f = Some f'   osafe f') 
  ( C C'. SContexts σ C = Some C'   fsafe C')"

lemma uadmit_dterm_adjointS:
  assumes ssafe:"ssafe σ"
  assumes good_interp:"is_interp I"
  fixes ν ω
  assumes VA:"Vagree ν ω (iSIGT θ. case SFunctions σ i of Some x  FVT x | None  {})"
  assumes dsafe:"dsafe θ"
  shows  "dterm_sem (adjoint I σ ν) θ = dterm_sem (adjoint I σ ω) θ"
proof -
  show "?thesis" 
    apply(rule uadmit_dterm_adjoint')
    using good_interp ssafe VA dsafe unfolding ssafe_def by auto 
qed

lemma adj_sub_assign_fact:"i j e. iSIGT e  j  (case SFunctions σ i of Some x  FVT x | None  {})  Inl i ({Inl x |x. x  dom (SFunctions σ)}  {Inr (Inl x) |x. x  dom (SContexts σ)}  {Inr (Inr x) |x. x  dom (SPredicates σ)} 
         {Inr (Inr x) |x. x  dom (SPrograms σ)}) 
        {Inl x |x. x  SIGT e}"
  unfolding SDom_def apply auto
  subgoal for i j
    apply (cases "SFunctions σ i")
     by auto
  done

lemma adj_sub_geq1_fact:"i j x1 x2. iSIGT x1  j  (case SFunctions σ i of Some x  FVT x | None  {})  Inl i ({Inl x |x. x  dom (SFunctions σ)}  {Inr (Inl x) |x. x  dom (SContexts σ)}  {Inr (Inr x) |x. x  dom (SPredicates σ)} 
         {Inr (Inr x) |x. x  dom (SPrograms σ)}) 
        {Inl x |x. x  SIGT x1  x  SIGT x2}"
  unfolding SDom_def apply auto
  subgoal for i j
    apply (cases "SFunctions σ i")
     by auto
  done

lemma adj_sub_geq2_fact:"i j x1 x2. iSIGT x2  j  (case SFunctions σ i of Some x  FVT x | None  {})  Inl i ({Inl x |x. x  dom (SFunctions σ)}  {Inr (Inl x) |x. x  dom (SContexts σ)}  {Inr (Inr x) |x. x  dom (SPredicates σ)} 
         {Inr (Inr x) |x. x  dom (SPrograms σ)}) 
        {Inl x |x. x  SIGT x1  x  SIGT x2}"
  unfolding SDom_def apply auto
  subgoal for i j
    apply (cases "SFunctions σ i")
     by auto
  done
lemma adj_sub_prop_fact:"i j x1 x2 k. iSIGT (x2 k)  j  (case SFunctions σ i of Some x  FVT x | None  {})  Inl i ({Inl x |x. x  dom (SFunctions σ)}  {Inr (Inl x) |x. x  dom (SContexts σ)}  {Inr (Inr x) |x. x  dom (SPredicates σ)} 
         {Inr (Inr x) |x. x  dom (SPrograms σ)}) 
         insert (Inr (Inr x1)) {Inl x |x. xa. x  SIGT (x2 xa)}"
  unfolding SDom_def apply auto
  subgoal for i j
    apply (cases "SFunctions σ i")
     by auto
  done

lemma adj_sub_ode_fact:"i j x1 x2. Inl i  SIGO x1  j  (case SFunctions σ i of Some x  FVT x | None  {})  Inl i ({Inl x |x. x  dom (SFunctions σ)}  {Inr (Inl x) |x. x  dom (SContexts σ)}  {Inr (Inr x) |x. x  dom (SPredicates σ)} 
         {Inr (Inr x) |x. x  dom (SPrograms σ)}) 
         (SIGF x2  {Inl x |x. Inl x  SIGO x1}  {Inr (Inr x) |x. Inr x  SIGO x1})"
  unfolding SDom_def apply auto
  subgoal for i j
    apply (cases "SFunctions σ i")
     by auto
  done

lemma adj_sub_assign:"e σ x. (iSIGT e. case SFunctions σ i of Some x  FVT x | None  {})  (aSDom σ  SIGP (x := e). SFV σ a)"
subgoal for e σ x
 unfolding SDom_def apply auto
  subgoal for i j
    apply (cases "SFunctions σ j")
     apply auto
    subgoal for a
      using adj_sub_assign_fact[of j e i]
      by (metis (mono_tags, lifting) SFV.simps(1) option.simps(5))
    done
  done
done

lemma adj_sub_diff_assign:"e σ x. (iSIGT e. case SFunctions σ i of Some x  FVT x | None  {})  (aSDom σ  SIGP (DiffAssign x e). SFV σ a)"
  subgoal for e σ x
    unfolding SDom_def apply auto
    subgoal for i j
      apply (cases "SFunctions σ j")
       apply auto
      subgoal for a
        using adj_sub_assign_fact[of j e i]
        by (metis (mono_tags, lifting) SFV.simps(1) option.simps(5))
      done
    done
  done
   
lemma adj_sub_geq1:"σ x1 x2. (iSIGT x1. case SFunctions σ i of Some x  FVT x | None  {})  (aSDom σ  SIGF (Geq x1 x2). SFV σ a)"
  subgoal for σ x1 x2
    unfolding SDom_def apply auto
    subgoal for x i
      apply (cases "SFunctions σ i")
       apply auto
      subgoal for a
        using adj_sub_geq1_fact[of i x1 x σ] 
        by (metis (mono_tags, lifting) SFV.simps(1) option.simps(5))
      done
    done
  done

lemma adj_sub_geq2:"σ x1 x2. (iSIGT x2. case SFunctions σ i of Some x  FVT x | None  {})  (aSDom σ  SIGF (Geq x1 x2). SFV σ a)"
  subgoal for σ x1 x2
    unfolding SDom_def apply auto
    subgoal for x i
      apply (cases "SFunctions σ i")
       apply auto
      subgoal for a
        using adj_sub_geq2_fact[of i x2 x σ] 
        by (metis (mono_tags, lifting) SFV.simps(1) option.simps(5))
      done
    done
  done

lemma adj_sub_prop:"σ x1 x2 j . (iSIGT (x2 j). case SFunctions σ i of Some x  FVT x | None  {})  (aSDom σ  SIGF ( x1 x2). SFV σ a)"
  subgoal for σ x1 x2 j
    unfolding SDom_def apply auto
    subgoal for x i
      apply (cases "SFunctions σ i")
       apply auto
      subgoal for a
        using adj_sub_prop_fact[of i x2 j x σ x1] 
        by (metis (mono_tags, lifting) SFV.simps(1) option.simps(5))     
      done
    done
  done

lemma adj_sub_ode:"σ x1 x2. (i{i |i. Inl i  SIGO x1}. case SFunctions σ i of None  {} | Some x  FVT x)  (aSDom σ  SIGP (EvolveODE x1 x2). SFV σ a)"
  subgoal for σ x1 x2
    unfolding SDom_def apply auto
    subgoal for x i
      apply (cases "SFunctions σ i")
       apply auto
      subgoal for a
        using adj_sub_ode_fact[of i x1 x σ x2]
        by (metis (mono_tags, lifting) SFV.simps(1) option.simps(5)) 
     done
   done
  done

lemma uadmit_ode_adjoint':
  fixes σ I
  assumes ssafe:"ssafe σ"
  assumes good_interp:"is_interp I"
  shows"ν ω. Vagree ν ω (i{i |i. Inl i  SIGO ODE}. case SFunctions σ i of None  {} | Some x  FVT x) osafe ODE  ODE_sem (adjoint I σ ν) ODE = ODE_sem (adjoint I σ ω) ODE"
proof (induction ODE)
  case (OVar x)
  then show ?case unfolding adjoint_def by auto
next
  case (OSing x1a x2)
    assume VA:"Vagree ν ω (i{i |i. Inl i  SIGO (OSing x1a x2)}. case SFunctions σ i of None  {} | Some a  FVT a)"
    assume osafe:"osafe (OSing x1a x2)"
    then have dfree:"dfree x2" by (auto dest: osafe.cases)
    have safes:"(f f'. SFunctions σ f = Some f'  dsafe f')"
      "(f f'. SPredicates σ f = Some f'  fsafe f')"
      using ssafe unfolding ssafe_def using dfree_is_dsafe by auto
    have sem:"sterm_sem (local.adjoint I σ ν) x2 = sterm_sem (local.adjoint I σ ω) x2"
       using uadmit_sterm_adjoint'[of σ ν ω x2 I, OF safes, of "(λ x y. x)" "(λ x y. x)"] VA
       by auto
    show ?case 
      apply auto
      apply (rule ext)
      subgoal for x
        apply (rule vec_extensionality)
        using sem by auto
      done
next
  case (OProd ODE1 ODE2)
    assume IH1:"ν ω. Vagree ν ω (i{i |i. Inl i  SIGO ODE1}. case SFunctions σ i of None  {} | Some a  FVT a) 
      osafe ODE1  ODE_sem (local.adjoint I σ ν) ODE1 = ODE_sem (local.adjoint I σ ω) ODE1"
    assume IH2:"ν ω. Vagree ν ω (i{i |i. Inl i  SIGO ODE2}. case SFunctions σ i of None  {} | Some a  FVT a) 
    osafe ODE2  ODE_sem (local.adjoint I σ ν) ODE2 = ODE_sem (local.adjoint I σ ω) ODE2"
    assume VA:"Vagree ν ω (i{i |i. Inl i  SIGO (OProd ODE1 ODE2)}. case SFunctions σ i of None  {} | Some a  FVT a)"
    assume safe:"osafe (OProd ODE1 ODE2)"
    from safe have safe1:"osafe ODE1" and safe2:"osafe ODE2" by (auto dest: osafe.cases) 
    have sub1:"(i{i |i. Inl i  SIGO ODE1}. case SFunctions σ i of None  {} | Some a  FVT a)  (i{i |i. Inl i  SIGO (OProd ODE1 ODE2)}. case SFunctions σ i of None  {} | Some a  FVT a)"
      by auto
    have sub2:"(i{i |i. Inl i  SIGO ODE2}. case SFunctions σ i of None  {} | Some a  FVT a)  (i{i |i. Inl i  SIGO (OProd ODE1 ODE2)}. case SFunctions σ i of None  {} | Some a  FVT a)"
      by auto
  then show ?case using IH1[OF agree_sub[OF sub1 VA] safe1] IH2[OF agree_sub[OF sub2 VA] safe2] by auto
qed

lemma uadmit_ode_ntadjoint':
  fixes σ I
  assumes ssafe:"i. dsafe (σ i)"
  assumes good_interp:"is_interp I"
  shows"ν ω. Vagree ν ω (y{y. Inl (Inr y)  SIGO ODE}. FVT (σ y))  osafe ODE  ODE_sem (adjointFO I σ ν) ODE = ODE_sem (adjointFO I σ ω) ODE"
proof (induction ODE)
  case (OVar x)
  then show ?case unfolding adjointFO_def by auto
next
  case (OSing x1a x2)
  assume VA:"Vagree ν ω (y{y. Inl (Inr y)  SIGO (OSing x1a x2)}. FVT (σ y))"
  assume osafe:"osafe (OSing x1a x2)"
  then have dfree:"dfree x2" by (auto dest: osafe.cases)
  have sem:"sterm_sem (adjointFO I σ ν) x2 = sterm_sem (adjointFO I σ ω) x2"
     using uadmit_sterm_ntadjoint'[of σ ν ω x2 I, OF ssafe] VA
     by auto
  show ?case 
    apply auto
    apply (rule ext)
    subgoal for x
      apply (rule vec_extensionality)
      using sem by auto
    done
next
  case (OProd ODE1 ODE2)
  assume IH1:"ν ω. Vagree ν ω (y{y. Inl (Inr y)  SIGO ODE1}. FVT (σ y)) 
    osafe ODE1  ODE_sem (adjointFO I σ ν) ODE1 = ODE_sem (adjointFO I σ ω) ODE1"
  assume IH2:"ν ω. Vagree ν ω (y{y. Inl (Inr y)  SIGO ODE2}. FVT (σ y)) 
    osafe ODE2  ODE_sem (adjointFO I σ ν) ODE2 = ODE_sem (adjointFO I σ ω) ODE2"
  assume VA:"Vagree ν ω (y{y. Inl (Inr y)  SIGO (OProd ODE1 ODE2)}. FVT (σ y))"
  assume safe:"osafe (OProd ODE1 ODE2)"
  from safe have safe1:"osafe ODE1" and safe2:"osafe ODE2" by (auto dest: osafe.cases) 
  have sub1:"(y{y. Inl (Inr y)  SIGO ODE1}. FVT (σ y))  (y{y. Inl (Inr y)  SIGO (OProd ODE1 ODE2)}. FVT (σ y))"
    by auto
  have sub2:"(y{y. Inl (Inr y)  SIGO ODE2}. FVT (σ y))  (y{y. Inl (Inr y)  SIGO (OProd ODE1 ODE2)}. FVT (σ y))"
    by auto
  then show ?case using IH1[OF agree_sub[OF sub1 VA] safe1] IH2[OF agree_sub[OF sub2 VA] safe2] by auto
qed

lemma adjoint_ode_vars:
  shows "ODE_vars (local.adjoint I σ ν) ODE = ODE_vars (local.adjoint I σ ω) ODE"
  apply(induction ODE)
  unfolding adjoint_def by auto

lemma uadmit_mkv_adjoint:
  assumes ssafe:"ssafe σ"
  assumes good_interp:"is_interp I"
  assumes VA:"Vagree ν ω (i  {i | i. (Inl iSIGO ODE)}. case SFunctions σ i of Some x  FVT x | None  {})"
  assumes osafe:"osafe ODE"
  shows "mk_v (adjoint I σ ν) ODE = mk_v (adjoint I σ ω) ODE"
  apply(rule ext)
  subgoal for R
    apply(rule ext)
    subgoal for solt
      apply(rule agree_UNIV_eq)
      using mk_v_agree[of "(adjoint I σ ν)" ODE "R" solt]
      using mk_v_agree[of "(adjoint I σ ω)" ODE "R" solt]
      using uadmit_ode_adjoint'[OF ssafe good_interp VA osafe]
      unfolding Vagree_def
      apply auto
       subgoal for i
         apply (cases "Inl i  Inl ` ODE_vars (adjoint I σ ω) ODE")
       proof -
         assume sem_eq:"ODE_sem (local.adjoint I σ ν) ODE = ODE_sem (local.adjoint I σ ω) ODE"
         have vars_eq:"ODE_vars (local.adjoint I σ ν) ODE = ODE_vars (local.adjoint I σ ω) ODE"
           apply(induction ODE)
           unfolding adjoint_def by auto
         assume thing1:" 
           i. (Inl i  Inl ` ODE_vars (local.adjoint I σ ν) ODE  fst (mk_v (local.adjoint I σ ν) ODE R solt) $ i = solt $ i) 
             (Inl i  Inr ` ODE_vars (local.adjoint I σ ν) ODE  fst (mk_v (local.adjoint I σ ν) ODE R solt) $ i = solt $ i)"
         assume thing2:" 
           i. (Inl i  Inl ` ODE_vars (local.adjoint I σ ω) ODE  fst (mk_v (local.adjoint I σ ω) ODE R solt) $ i = solt $ i) 
             (Inl i  Inr ` ODE_vars (local.adjoint I σ ω) ODE  fst (mk_v (local.adjoint I σ ω) ODE R solt) $ i = solt $ i)"
         assume inl:"Inl i  Inl ` ODE_vars (local.adjoint I σ ω) ODE"
          from thing1 and inl have eq1: "fst (mk_v (local.adjoint I σ ν) ODE R solt) $ i = solt $ i"
            using vars_eq by auto
          from thing2 and inl have eq2: "fst (mk_v (local.adjoint I σ ω) ODE R solt) $ i = solt $ i"
            using vars_eq by auto
         show "fst (mk_v (local.adjoint I σ ν) ODE R solt) $ i = fst (mk_v (local.adjoint I σ ω) ODE R solt) $ i"
           using eq1 eq2 by auto
       next
         assume sem_eq:"ODE_sem (local.adjoint I σ ν) ODE = ODE_sem (local.adjoint I σ ω) ODE"
         assume thing1:"i. Inl i  Inl ` ODE_vars (local.adjoint I σ ν) ODE  Inl i  Inr ` ODE_vars (local.adjoint I σ ν) ODE 
        fst (mk_v (local.adjoint I σ ν) ODE R solt) $ i = fst R $ i"
         assume thing2:"i. Inl i  Inl ` ODE_vars (local.adjoint I σ ω) ODE  Inl i  Inr ` ODE_vars (local.adjoint I σ ω) ODE 
        fst (mk_v (local.adjoint I σ ω) ODE R solt) $ i = fst R $ i"
         assume inl:"Inl i  Inl ` ODE_vars (local.adjoint I σ ω) ODE"
         have vars_eq:"ODE_vars (local.adjoint I σ ν) ODE = ODE_vars (local.adjoint I σ ω) ODE"
           apply(induction ODE)
             unfolding adjoint_def by auto
         from thing1 and inl have eq1: "fst (mk_v (local.adjoint I σ ν) ODE R solt) $ i = fst R $ i"
           using vars_eq by auto
         from thing2 and inl have eq2: "fst (mk_v (local.adjoint I σ ω) ODE R solt) $ i = fst R $ i"
           using vars_eq by auto
         show "fst (mk_v (local.adjoint I σ ν) ODE R solt) $ i = fst (mk_v (local.adjoint I σ ω) ODE R solt) $ i"
           using eq1 eq2 by auto
       qed
      subgoal for i
        apply (cases "Inr i  Inr ` ODE_vars (adjoint I σ ω) ODE")
       proof -
         assume sem_eq:"ODE_sem (local.adjoint I σ ν) ODE = ODE_sem (local.adjoint I σ ω) ODE"
         assume thing1:"i. (Inr i  Inl ` ODE_vars (local.adjoint I σ ν) ODE 
             snd (mk_v (local.adjoint I σ ν) ODE R solt) $ i = ODE_sem (local.adjoint I σ ω) ODE solt $ i) 
            (Inr i  Inr ` ODE_vars (local.adjoint I σ ν) ODE 
              snd (mk_v (local.adjoint I σ ν) ODE R solt) $ i = ODE_sem (local.adjoint I σ ω) ODE solt $ i)"
         assume thing2:"i. (Inr i  Inl ` ODE_vars (local.adjoint I σ ω) ODE 
              snd (mk_v (local.adjoint I σ ω) ODE R solt) $ i = ODE_sem (local.adjoint I σ ω) ODE solt $ i) 
             (Inr i  Inr ` ODE_vars (local.adjoint I σ ω) ODE 
          snd (mk_v (local.adjoint I σ ω) ODE R solt) $ i = ODE_sem (local.adjoint I σ ω) ODE solt $ i)"
         assume inr:"Inr i  Inr ` ODE_vars (local.adjoint I σ ω) ODE"
         have vars_eq:"ODE_vars (local.adjoint I σ ν) ODE = ODE_vars (local.adjoint I σ ω) ODE"
          apply(induction ODE)
            unfolding adjoint_def by auto
         show "snd (mk_v (local.adjoint I σ ν) ODE R solt) $ i = snd (mk_v (local.adjoint I σ ω) ODE R solt) $ i"
           using thing1 thing2 vars_eq inr by auto
       next
         assume sem_eq:"ODE_sem (local.adjoint I σ ν) ODE = ODE_sem (local.adjoint I σ ω) ODE"
         assume thing1:"i. Inr i  Inl ` ODE_vars (local.adjoint I σ ν) ODE  Inr i  Inr ` ODE_vars (local.adjoint I σ ν) ODE 
             snd (mk_v (local.adjoint I σ ν) ODE R solt) $ i = snd R $ i"
         assume thing2:"i. Inr i  Inl ` ODE_vars (local.adjoint I σ ω) ODE  Inr i  Inr ` ODE_vars (local.adjoint I σ ω) ODE 
             snd (mk_v (local.adjoint I σ ω) ODE R solt) $ i = snd R $ i"
         assume inr:"Inr i  Inr ` ODE_vars (local.adjoint I σ ω) ODE"
         have vars_eq:"ODE_vars (local.adjoint I σ ν) ODE = ODE_vars (local.adjoint I σ ω) ODE"
          apply(induction ODE)
            unfolding adjoint_def by auto
         have eq1:"snd (mk_v (local.adjoint I σ ν) ODE R solt) $ i = snd R $ i"
           using thing1 sem_eq vars_eq inr by auto
         have eq2:"snd (mk_v (local.adjoint I σ ω) ODE R solt) $ i = snd R $ i"
           using thing2 sem_eq vars_eq inr by auto
         show "snd (mk_v (local.adjoint I σ ν) ODE R solt) $ i = snd (mk_v (local.adjoint I σ ω) ODE R solt) $ i"
           using eq1 eq2 by auto
       qed
      done
    done
  done

lemma adjointFO_ode_vars:
  shows "ODE_vars (adjointFO I σ ν) ODE = ODE_vars (adjointFO I σ ω) ODE"
  apply(induction ODE)
    unfolding adjointFO_def by auto

lemma uadmit_mkv_ntadjoint:
  assumes ssafe:"i. dsafe (σ i)"
  assumes good_interp:"is_interp I"
  assumes VA:"Vagree ν ω (y{y. Inl (Inr y)  SIGO ODE}. FVT (σ y))"
  assumes osafe:"osafe ODE"
  shows "mk_v (adjointFO I σ ν) ODE = mk_v (adjointFO I σ ω) ODE"
  apply(rule ext)
  subgoal for R
    apply(rule ext)
    subgoal for solt
      apply(rule agree_UNIV_eq)
      using mk_v_agree[of "(adjointFO I σ ν)" ODE "R" solt]
      using mk_v_agree[of "(adjointFO I σ ω)" ODE "R" solt]
      using uadmit_ode_ntadjoint'[OF ssafe good_interp VA osafe]
      unfolding Vagree_def
      apply auto
      using adjointFO_ode_vars by metis+
    done
  done
    
lemma uadmit_prog_fml_adjoint':
  fixes σ I
  assumes ssafe:"ssafe σ"
  assumes good_interp:"is_interp I"
  shows "ν ω. Vagree ν ω (xSDom σ  SIGP α. SFV σ x)  hpsafe α  prog_sem (adjoint I σ ν) α = prog_sem (adjoint I σ ω) α"
  and "ν ω. Vagree ν ω (xSDom σ  SIGF φ. SFV σ x)  fsafe φ  fml_sem (adjoint I σ ν) φ = fml_sem (adjoint I σ ω) φ"
proof (induct "α" and "φ")
  case (Pvar x)
  then show ?case unfolding adjoint_def by auto
next
  case (Assign x e)
  assume VA:"Vagree ν ω (aSDom σ  SIGP (x := e). SFV σ a)"
  assume safe:"hpsafe (x := e)"
  from safe have dsafe:"dsafe e" by (auto dest: hpsafe.cases)
  have sub:"(iSIGT e. case SFunctions σ i of Some x  FVT x | None  {})  (aSDom σ  SIGP (x := e). SFV σ a)"
    using adj_sub_assign[of σ e x] by auto
  have "dterm_sem (local.adjoint I σ ν) e = dterm_sem (local.adjoint I σ ω) e"
    by (rule uadmit_dterm_adjointS[OF ssafe good_interp agree_sub[OF sub VA] dsafe])
  then show ?case by (auto simp add: vec_eq_iff)
next
  case (DiffAssign x e)
  assume VA:"Vagree ν ω (aSDom σ  SIGP (DiffAssign x e). SFV σ a)"
  assume safe:"hpsafe (DiffAssign x e)"
  from safe have dsafe:"dsafe e" by (auto dest: hpsafe.cases)
  have sub:"(iSIGT e. case SFunctions σ i of Some x  FVT x | None  {})  (aSDom σ  SIGP (DiffAssign x e). SFV σ a)"
    using adj_sub_diff_assign[of σ e] by auto
  have "dterm_sem (local.adjoint I σ ν) e = dterm_sem (local.adjoint I σ ω) e"
    by (rule uadmit_dterm_adjointS[OF ssafe good_interp agree_sub[OF sub VA] dsafe])
  then show ?case by (auto simp add: vec_eq_iff)
next
  case (Test x)
  assume IH:"ν ω. Vagree ν ω (aSDom σ  SIGF x. SFV σ a)  fsafe x  fml_sem (adjoint I σ ν) x = fml_sem (adjoint I σ ω) x"
  assume VA:"Vagree ν ω (aSDom σ  SIGP (? x). SFV σ a)"
  assume hpsafe:"hpsafe (? x)"
  then have fsafe:"fsafe x" by (auto dest: hpsafe.cases)
  have sub:"(aSDom σ  SIGF x. SFV σ a)  (aSDom σ  SIGP (? x). SFV σ a)"
    by auto
  have "fml_sem (adjoint I σ ν) x = fml_sem (adjoint I σ ω) x"
    using IH[OF agree_sub[OF sub VA] fsafe] by auto
  then show ?case by auto
next
  case (EvolveODE x1 x2)
  assume IH:"ν ω. Vagree ν ω (aSDom σ  SIGF x2. SFV σ a)  fsafe x2  fml_sem (local.adjoint I σ ν) x2 = fml_sem (local.adjoint I σ ω) x2"
  assume VA:"Vagree ν ω (aSDom σ  SIGP (EvolveODE x1 x2). SFV σ a)"
  assume safe:"hpsafe (EvolveODE x1 x2)"
  then have osafe:"osafe x1" and fsafe:"fsafe x2" by (auto dest: hpsafe.cases)
  have sub1:"(aSDom σ  SIGF x2. SFV σ a)  (aSDom σ  SIGP (EvolveODE x1 x2). SFV σ a)"
    by auto
  then have VAF:"Vagree ν ω (aSDom σ  SIGF x2. SFV σ a)"
    using agree_sub[OF sub1 VA] by auto 
  note IH' = IH[OF VAF fsafe]
  have sub:"(i{i |i. Inl i  SIGO x1}. case SFunctions σ i of None  {} | Some x  FVT x)  (aSDom σ  SIGP (EvolveODE x1 x2). SFV σ a)"
    using adj_sub_ode[of σ x1 x2] by auto
  moreover have IH2:"ODE_sem (local.adjoint I σ ν) x1 = ODE_sem (local.adjoint I σ ω) x1"
    apply (rule uadmit_ode_adjoint')
       subgoal by (rule ssafe)
      subgoal by (rule good_interp)
     subgoal using agree_sub[OF sub VA] by auto
    subgoal by (rule osafe)
    done
  have mkv:"mk_v (adjoint I σ ν) x1 = mk_v (adjoint I σ ω) x1"
    apply (rule uadmit_mkv_adjoint)
       using ssafe good_interp osafe agree_sub[OF sub VA] by auto
  show ?case 
    apply auto
     subgoal for aa ba bb sol t
       apply(rule exI[where x = sol])
       apply(rule conjI)
        subgoal by auto
       apply(rule exI[where x=t])
       apply(rule conjI)
        subgoal using mkv by auto
       apply(rule conjI)
        subgoal by auto using IH2 mkv IH' by auto
    subgoal for aa ba bb sol t
      apply(rule exI[where x = sol])
      apply(rule conjI)
       subgoal by auto
      apply(rule exI[where x=t])
      apply(rule conjI)
       subgoal using mkv by auto
      apply(rule conjI)
       subgoal by auto using IH2 mkv IH' by auto
    done
next
  case (Choice x1 x2)
  assume IH1:"ν ω. Vagree ν ω (aSDom σ  SIGP x1. SFV σ a)  hpsafe x1  prog_sem (local.adjoint I σ ν) x1 = prog_sem (local.adjoint I σ ω) x1"
  assume IH2:"ν ω. Vagree ν ω (aSDom σ  SIGP x2. SFV σ a)  hpsafe x2  prog_sem (local.adjoint I σ ν) x2 = prog_sem (local.adjoint I σ ω) x2"
  assume VA:"Vagree ν ω (aSDom σ  SIGP (x1 ∪∪ x2). SFV σ a)"
  assume safe:"hpsafe (x1 ∪∪ x2)"
  from safe have
    safe1:"hpsafe x1"
    and safe2:"hpsafe x2"
    by (auto dest: hpsafe.cases)
  have sub1:"(aSDom σ  SIGP x1. SFV σ a)  (aSDom σ  SIGP (x1 ∪∪ x2). SFV σ a)"
    by auto
  have sub2:"(aSDom σ  SIGP x2. SFV σ a)  (aSDom σ  SIGP (x1 ∪∪ x2). SFV σ a)"
    by auto
  then show ?case using IH1[OF agree_sub[OF sub1 VA] safe1] IH2[OF agree_sub[OF sub2 VA] safe2] by auto
next
  case (Sequence x1 x2)
  assume IH1:"ν ω. Vagree ν ω (aSDom σ  SIGP x1. SFV σ a)  hpsafe x1  prog_sem (local.adjoint I σ ν) x1 = prog_sem (local.adjoint I σ ω) x1"
  assume IH2:"ν ω. Vagree ν ω (aSDom σ  SIGP x2. SFV σ a)  hpsafe x2  prog_sem (local.adjoint I σ ν) x2 = prog_sem (local.adjoint I σ ω) x2"
  assume VA:"Vagree ν ω (aSDom σ  SIGP (x1 ;; x2). SFV σ a)"
  assume safe:"hpsafe (x1 ;; x2)"
  from safe have
    safe1:"hpsafe x1"
    and safe2:"hpsafe x2"
    by (auto dest: hpsafe.cases)
  have sub1:"(aSDom σ  SIGP x1. SFV σ a)  (aSDom σ  SIGP (x1 ;; x2). SFV σ a)"
    by auto
  have sub2:"(aSDom σ  SIGP x2. SFV σ a)  (aSDom σ  SIGP (x1 ;; x2). SFV σ a)"
    by auto
  then show ?case using IH1[OF agree_sub[OF sub1 VA] safe1] IH2[OF agree_sub[OF sub2 VA] safe2] by auto
next
  case (Loop x)
  assume IH:"ν ω. Vagree ν ω (aSDom σ  SIGP x. SFV σ a)  hpsafe x  prog_sem (local.adjoint I σ ν) x = prog_sem (local.adjoint I σ ω) x"
  assume VA:"Vagree ν ω (aSDom σ  SIGP (x**). SFV σ a)"
  assume safe:"hpsafe (x**)"
  from safe have
    safe:"hpsafe x"
    by (auto dest: hpsafe.cases)
  have sub:"(aSDom σ  SIGP x. SFV σ a)  (aSDom σ  SIGP (x**). SFV σ a)"
    by auto
  show ?case using IH[OF agree_sub[OF sub VA] safe] by auto
next
  case (Geq x1 x2)
  assume VA:"Vagree ν ω (aSDom σ  SIGF (Geq x1 x2). SFV σ a)"
  assume safe:"fsafe (Geq x1 x2)"
  then have dsafe1:"dsafe x1" and dsafe2:"dsafe x2" by (auto dest: fsafe.cases)
  have sub1:"(iSIGT x1. case SFunctions σ i of Some x  FVT x | None  {})  (aSDom σ  SIGF (Geq x1 x2). SFV σ a)"
    using adj_sub_geq1[of σ x1 x2] by auto
  have sub2:"(iSIGT x2. case SFunctions σ i of Some x  FVT x | None  {})  (aSDom σ  SIGF (Geq x1 x2). SFV σ a)"
    using adj_sub_geq2[of σ x2 x1] by auto
  have "dterm_sem (local.adjoint I σ ν) x1 = dterm_sem (local.adjoint I σ ω) x1"
    by (rule uadmit_dterm_adjointS[OF ssafe good_interp agree_sub[OF sub1 VA] dsafe1])
  moreover have "dterm_sem (local.adjoint I σ ν) x2 = dterm_sem (local.adjoint I σ ω) x2"
    by (rule uadmit_dterm_adjointS[OF ssafe good_interp agree_sub[OF sub2 VA] dsafe2])
  ultimately show ?case by auto
next
  case (Prop x1 x2 ν ω)
  assume VA:"Vagree ν ω (aSDom σ  SIGF ( x1 x2). SFV σ a)"
  assume safe:"fsafe ( x1 x2)"
  then have safes:"i. dsafe (x2 i)" using dfree_is_dsafe by auto
  have subs:"j. (iSIGT (x2 j). case SFunctions σ i of Some x  FVT x | None  {})  (aSDom σ  SIGF ( x1 x2). SFV σ a)"
    subgoal for j using adj_sub_prop[of σ x2 j x1] by auto
    done
  have "i. dterm_sem (local.adjoint I σ ν) (x2 i) = dterm_sem (local.adjoint I σ ω) (x2 i)"
    by (rule uadmit_dterm_adjointS[OF ssafe good_interp agree_sub[OF subs VA] safes])
  then have vec_eq:"R. (χ i. dterm_sem (local.adjoint I σ ν) (x2 i) R) = (χ i. dterm_sem (local.adjoint I σ ω) (x2 i) R)"
    by (auto simp add: vec_eq_iff)
  from VA have VAs:"j. Vagree ν ω (iSIGT (x2 j). case SFunctions σ i of Some a  FVT a | None  {})"
    unfolding Vagree_def SIGT.simps using rangeI 
    by (metis (no_types, lifting) subsetD subs)
  have SIGF:"a. SPredicates σ x1 = Some a  Inr (Inr x1)  SDom σ  SIGF ( x1 x2)" unfolding SDom_def
    by auto
  have VAsub:"a. SPredicates σ x1 = Some a  (FVF a)  (iSDom σ  SIGF ( x1 x2). SFV σ i)"
    using SIGF by auto
  have VAf:"a. SPredicates σ x1 = Some a  Vagree ν ω (FVF a)"
    using agree_sub[OF VAsub VA] by auto
  then show ?case 
    apply(cases "SPredicates σ x1")
    defer
    subgoal for a
    proof -
      assume some:"SPredicates σ x1 = Some a"
      note FVF = VAf[OF some]
      have dsafe:"f f'. SFunctions σ f = Some f'  dsafe f'"
        using ssafe dfree_is_dsafe unfolding ssafe_def by auto
      have dsem:"R . (ν  fml_sem (extendf I R) a) = (ω  fml_sem (extendf I R) a)"
        subgoal for R
          apply (rule coincidence_formula)
            subgoal using ssafe unfolding ssafe_def using some by auto
           subgoal unfolding Iagree_def by auto
          subgoal by (rule FVF)
        done
      done
      have pred_eq:"R. Predicates (local.adjoint I σ ν) x1 R = Predicates (local.adjoint I σ ω) x1 R"
        using dsem some unfolding adjoint_def by auto
      show "fml_sem (local.adjoint I σ ν) ( x1 x2) = fml_sem (local.adjoint I σ ω) ( x1 x2)"
        apply auto
         subgoal for a b using pred_eq[of "(χ i. dterm_sem (local.adjoint I σ ν) (x2 i) (a, b))"] vec_eq by auto
        subgoal for a b using pred_eq[of "(χ i. dterm_sem (local.adjoint I σ ν) (x2 i) (a, b))"] vec_eq by auto
        done
    qed
    unfolding adjoint_def using local.adjoint_def local.vec_eq apply auto
    done
next
  case (Not x)
  assume IH:"ν ω. Vagree ν ω (aSDom σ  SIGF x. SFV σ a)  fsafe x  fml_sem (local.adjoint I σ ν) x = fml_sem (local.adjoint I σ ω) x"
  assume VA:"Vagree ν ω (aSDom σ  SIGF (Not x). SFV σ a)"
  assume safe:"fsafe (Not x)"
  from safe have
    safe:"fsafe x"
    by (auto dest: fsafe.cases)
  have sub:"(aSDom σ  SIGF x. SFV σ a)  (aSDom σ  SIGF (Not x). SFV σ a)"
    by auto
  show ?case using IH[OF agree_sub[OF sub VA] safe] by auto
next
  case (And x1 x2)
  assume IH1:"ν ω. Vagree ν ω (aSDom σ  SIGF x1. SFV σ a)  fsafe x1  fml_sem (local.adjoint I σ ν) x1 = fml_sem (local.adjoint I σ ω) x1"
  assume IH2:"ν ω. Vagree ν ω (aSDom σ  SIGF x2. SFV σ a)  fsafe x2  fml_sem (local.adjoint I σ ν) x2 = fml_sem (local.adjoint I σ ω) x2"
  assume VA:"Vagree ν ω (aSDom σ  SIGF (And x1 x2). SFV σ a)"
  assume safe:"fsafe (And x1 x2)"
  from safe have
    safe1:"fsafe x1"
    and safe2:"fsafe x2"
    by (auto dest: fsafe.cases)
  have sub1:"(aSDom σ  SIGF x1. SFV σ a)  (aSDom σ  SIGF (And x1 x2). SFV σ a)"
    by auto
  have sub2:"(aSDom σ  SIGF x2. SFV σ a)  (aSDom σ  SIGF (And x1 x2). SFV σ a)"
    by auto
  show ?case using IH1[OF agree_sub[OF sub1 VA] safe1] IH2[OF agree_sub[OF sub2 VA] safe2] by auto
next
  case (Exists x1 x2)
  assume IH1:"ν ω. Vagree ν ω (aSDom σ  SIGF x2. SFV σ a)  fsafe x2  fml_sem (local.adjoint I σ ν) x2 = fml_sem (local.adjoint I σ ω) x2"
  assume VA:"Vagree ν ω (aSDom σ  SIGF (Exists x1 x2). SFV σ a)"
  assume safe:"fsafe (Exists x1 x2)"
  from safe have safe1:"fsafe x2"
    by (auto dest: fsafe.cases)
  have sub1:"(aSDom σ  SIGF x2. SFV σ a)  (aSDom σ  SIGF (Exists x1 x2). SFV σ a)"
    by auto
  show ?case using IH1[OF agree_sub[OF sub1 VA] safe1] by auto
next
  case (Diamond x1 x2)
  assume IH1:"ν ω. Vagree ν ω (aSDom σ  SIGP x1. SFV σ a)  hpsafe x1  prog_sem (local.adjoint I σ ν) x1 = prog_sem (local.adjoint I σ ω) x1"
  assume IH2:"ν ω. Vagree ν ω (aSDom σ  SIGF x2. SFV σ a)  fsafe x2  fml_sem (local.adjoint I σ ν) x2 = fml_sem (local.adjoint I σ ω) x2"
  assume VA:"Vagree ν ω (aSDom σ  SIGF (Diamond x1 x2). SFV σ a)"
  assume safe:"fsafe (Diamond x1 x2)"
  from safe have
    safe1:"hpsafe x1"
    and safe2:"fsafe x2"
    by (auto dest: fsafe.cases)
  have sub1:"(aSDom σ  SIGP x1. SFV σ a)  (aSDom σ  SIGF (Diamond x1 x2). SFV σ a)"
    by auto
  have sub2:"(aSDom σ  SIGF x2. SFV σ a)  (aSDom σ  SIGF (Diamond x1 x2). SFV σ a)"
    by auto
  show ?case using IH1[OF agree_sub[OF sub1 VA] safe1] IH2[OF agree_sub[OF sub2 VA] safe2] by auto
next
  case (InContext x1 x2)
  assume IH1:"ν ω. Vagree ν ω (aSDom σ  SIGF x2. SFV σ a)  fsafe x2  fml_sem (local.adjoint I σ ν) x2 = fml_sem (local.adjoint I σ ω) x2"
  assume VA:"Vagree ν ω (aSDom σ  SIGF (InContext x1 x2). SFV σ a)"
  assume safe:"fsafe (InContext x1 x2)"
  from safe have  safe1:"fsafe x2"
    by (auto dest: fsafe.cases)
  have sub:"(aSDom σ  SIGF x2. SFV σ a)  (aSDom σ  SIGF (InContext x1 x2). SFV σ a)"
    by auto
  show ?case using IH1[OF agree_sub[OF sub VA] safe1]  
    unfolding adjoint_def by auto
qed
 
lemma uadmit_prog_adjoint:
  assumes PUA:"PUadmit σ a U"
  assumes VA:"Vagree ν ω (-U)"
  assumes hpsafe:"hpsafe a"
  assumes ssafe:"ssafe σ"
  assumes good_interp:"is_interp I"
  shows "prog_sem (adjoint I σ ν) a = prog_sem (adjoint I σ ω) a"
proof -
  have sub:"(xSDom σ  SIGP a. SFV σ x)  -U" using PUA unfolding PUadmit_def by auto
  have VA':"Vagree ν ω (xSDom σ  SIGP a. SFV σ x)" using agree_sub[OF sub VA] by auto
  show ?thesis 
    apply(rule uadmit_prog_fml_adjoint'[OF ssafe good_interp])
     subgoal by (rule VA')
    subgoal by (rule hpsafe)
    done
qed

lemma uadmit_fml_adjoint:
  assumes FUA:"FUadmit σ φ U"
  assumes VA:"Vagree ν ω (-U)"
  assumes fsafe:"fsafe φ"
  assumes ssafe:"ssafe σ"
  assumes good_interp:"is_interp I"
  shows "fml_sem (adjoint I σ ν) φ = fml_sem (adjoint I σ ω) φ"
proof -
  have sub:"(xSDom σ  SIGF φ. SFV σ x)  -U" using FUA unfolding FUadmit_def by auto
  have VA':"Vagree ν ω (xSDom σ  SIGF φ. SFV σ x)" using agree_sub[OF sub VA] by auto
  show ?thesis 
    apply(rule uadmit_prog_fml_adjoint'[OF ssafe good_interp])
     subgoal by (rule VA')
    subgoal by (rule fsafe)
    done
qed

lemma ntadj_sub_assign:"e σ x. (y{y. Inr y  SIGT e}. FVT (σ y))  (y{y. Inl (Inr y)  SIGP (Assign x e)}. FVT (σ y))"
  by auto

lemma ntadj_sub_diff_assign:"e σ x. (y{y. Inl y  SIGT e}. FVT (σ y))  (y{y. Inl (Inl y)  SIGP (DiffAssign x e)}. FVT (σ y))"
  by auto
   
lemma ntadj_sub_geq1:"σ x1 x2. (y{y. Inl y  SIGT x1}. FVT (σ y))  (y{y. Inl (Inl y)  SIGF (Geq x1 x2)}. FVT (σ y))"
  by auto

lemma ntadj_sub_geq2:"σ x1 x2. (y{y. Inl y  SIGT x2}. FVT (σ y))  (y{y. Inl (Inl y)  SIGF (Geq x1 x2)}. FVT (σ y))"
  by auto

lemma ntadj_sub_prop:"σ x1 x2 j. (y{y. Inl y  SIGT (x2 j)}. FVT (σ y))  (y{y. Inl (Inl y)  SIGF ( x1 x2)}.FVT (σ y))"
  by auto

lemma ntadj_sub_ode:"σ x1 x2. (y{y. Inl (Inl y)  SIGO x1}. FVT (σ y))  (y{y. Inl (Inl y)  SIGP (EvolveODE x1 x2)}. FVT (σ y))"
  by auto

lemma uadmit_prog_fml_ntadjoint':
  fixes σ I
  assumes ssafe:"i. dsafe (σ i)"
  assumes good_interp:"is_interp I"
  shows "ν ω. Vagree ν ω (x{x. Inl (Inr x)  SIGP α}. FVT (σ x))  hpsafe α  prog_sem (adjointFO I σ ν) α = prog_sem (adjointFO I σ ω) α"
  and "ν ω. Vagree ν ω (x{x. Inl (Inr x)  SIGF φ}. FVT (σ x))  fsafe φ  fml_sem (adjointFO I σ ν) φ = fml_sem (adjointFO I σ ω) φ"
proof (induct "α" and "φ")
  case (Pvar x)
  then show ?case unfolding adjointFO_def by auto
next
  case (Assign x e)
  assume VA:"Vagree ν ω (y{y. Inl (Inr y)  SIGP (Assign x e)}. FVT (σ y))"
  assume safe:"hpsafe (x := e)"
  from safe have dsafe:"dsafe e" by (auto dest: hpsafe.cases)
  have sub:"(y{y. Inr y  SIGT e}. FVT (σ y))  (y{y. Inl (Inr y)  SIGP (Assign x e)}. FVT (σ y))"
    using ntadj_sub_assign[of σ e x] by auto
  have VA':"(Vagree ν ω (i{i. Inr i  SIGT e}. FVT (σ i)))"
    using agree_sub[OF sub VA] by auto
  have "dterm_sem (adjointFO I σ ν) e = dterm_sem (adjointFO I σ ω) e"
    using uadmit_dterm_ntadjoint'[of σ I ν ω e] ssafe good_interp agree_sub[OF sub VA] dsafe by auto
  then show ?case by (auto simp add: vec_eq_iff)
next
  case (DiffAssign x e)
  assume VA:"Vagree ν ω (y{y. Inl (Inr y)  SIGP (DiffAssign x e)}. FVT (σ y))"
  assume safe:"hpsafe (DiffAssign x e)"
  from safe have dsafe:"dsafe e" by (auto dest: hpsafe.cases)
  have sub:"(y{y. Inr y  SIGT e}. FVT (σ y))  (y{y. Inl (Inr y)  SIGP (DiffAssign x e)}. FVT (σ y))"
    using ntadj_sub_assign[of σ e x] by auto
  have VA':"(Vagree ν ω (i{i. Inr i  SIGT e}. FVT (σ i)))"
    using agree_sub[OF sub VA] by auto
  have "dterm_sem (adjointFO I σ ν) e = dterm_sem (adjointFO I σ ω) e"
    using uadmit_dterm_ntadjoint'[of σ I ν ω e] ssafe good_interp agree_sub[OF sub VA] dsafe by auto
  then show ?case by (auto simp add: vec_eq_iff)
next
  case (Test x)
  assume IH:"ν ω. Vagree ν ω (y{y. Inl (Inr y)  SIGF x}. FVT (σ y))  fsafe x  fml_sem (adjointFO I σ ν) x = fml_sem (adjointFO I σ ω) x"
  assume VA:"Vagree ν ω (y{y. Inl (Inr y)  SIGP (? x)}. FVT (σ y))"
  assume hpsafe:"hpsafe (? x)"
  then have fsafe:"fsafe x" by (auto dest: hpsafe.cases)
  have sub:"(y{y. Inl (Inr y)  SIGF x}. FVT (σ y))  (y{y. Inl (Inr y)  SIGP (? x)}. FVT (σ y))"
    by auto
  have "fml_sem (adjointFO I σ ν) x = fml_sem (adjointFO I σ ω) x"
    using IH[OF agree_sub[OF sub VA] fsafe] by auto
  then show ?case by auto
next
  case (EvolveODE x1 x2)
  assume IH:"ν ω. Vagree ν ω (y{y. Inl (Inr y)  SIGF x2}. FVT (σ y))  fsafe x2  fml_sem (adjointFO I σ ν) x2 = fml_sem (adjointFO I σ ω) x2"
  assume VA:"Vagree ν ω (y{y. Inl (Inr y)  SIGP (EvolveODE x1 x2)}. FVT (σ y))"
  assume safe:"hpsafe (EvolveODE x1 x2)"
  then have osafe:"osafe x1" and fsafe:"fsafe x2" by (auto dest: hpsafe.cases)
  have sub1:"(y{y. Inl (Inr y)  SIGF x2}. FVT (σ y))  (y{y. Inl (Inr y)  SIGP (EvolveODE x1 x2)}. FVT (σ y))"
    by auto
  then have VAF:"Vagree ν ω (y{y. Inl (Inr y)  SIGF x2}. FVT (σ y))"
    using agree_sub[OF sub1 VA] by auto 
  note IH' = IH[OF VAF fsafe]
  have sub:"(y{y. Inl (Inr y)  SIGO x1}. FVT (σ y))  (y{y. Inl (Inr y)  SIGP (EvolveODE x1 x2)}. FVT (σ y))"
    by auto
  moreover have IH2:"ODE_sem (adjointFO I σ ν) x1 = ODE_sem (adjointFO I σ ω) x1"
    apply (rule uadmit_ode_ntadjoint')
       subgoal by (rule ssafe)
      subgoal by (rule good_interp)
     defer subgoal by (rule osafe)
    using agree_sub[OF sub VA] by auto
  have mkv:"mk_v (adjointFO I σ ν) x1 = mk_v (adjointFO I σ ω) x1"
    apply (rule uadmit_mkv_ntadjoint)
       using ssafe good_interp osafe agree_sub[OF sub VA] by auto
  show ?case 
    apply auto
    subgoal for aa ba bb sol t
      apply(rule exI[where x = sol])
      apply(rule conjI)
       subgoal by auto
      apply(rule exI[where x=t])
      apply(rule conjI)
       subgoal using mkv by auto
      apply(rule conjI)
       subgoal by auto using IH2 mkv IH' by auto
    subgoal for aa ba bb sol t
      apply(rule exI[where x = sol])
      apply(rule conjI)
       subgoal by auto
      apply(rule exI[where x=t])
      apply(rule conjI)
       subgoal using mkv by auto
      apply(rule conjI)
       subgoal by auto using IH2 mkv IH' by auto
    done
next
  case (Choice x1 x2)
  assume IH1:"ν ω. Vagree ν ω (y{y. Inl (Inr y)  SIGP x1}. FVT (σ y))  hpsafe x1  prog_sem (adjointFO I σ ν) x1 = prog_sem (adjointFO I σ ω) x1"
  assume IH2:"ν ω. Vagree ν ω (y{y. Inl (Inr y)  SIGP x2}. FVT (σ y))  hpsafe x2  prog_sem (adjointFO I σ ν) x2 = prog_sem (adjointFO I σ ω) x2"
  assume VA:"Vagree ν ω (y{y. Inl (Inr y)  SIGP (x1 ∪∪ x2)}. FVT (σ y))"
  assume safe:"hpsafe (x1 ∪∪ x2)"
  from safe have
    safe1:"hpsafe x1"
    and safe2:"hpsafe x2"
    by (auto dest: hpsafe.cases)
  have sub1:"(y{y. Inl (Inr y)  SIGP (x1)}. FVT (σ y))  (y{y. Inl (Inr y)  SIGP (x1 ∪∪ x2)}. FVT (σ y))"
    by auto
  have sub2:"(y{y. Inl (Inr y)  SIGP (x2)}. FVT (σ y))  (y{y. Inl (Inr y)  SIGP (x1 ∪∪ x2)}. FVT (σ y))"
    by auto
  then show ?case using IH1[OF agree_sub[OF sub1 VA] safe1] IH2[OF agree_sub[OF sub2 VA] safe2] by auto
next
  case (Sequence x1 x2)
  assume IH1:"ν ω. Vagree ν ω (y{y. Inl (Inr y)  SIGP x1}. FVT (σ y))  hpsafe x1  prog_sem (adjointFO I σ ν) x1 = prog_sem (adjointFO I σ ω) x1"
  assume IH2:"ν ω. Vagree ν ω (y{y. Inl (Inr y)  SIGP x2}. FVT (σ y))  hpsafe x2  prog_sem (adjointFO I σ ν) x2 = prog_sem (adjointFO I σ ω) x2"
  assume VA:"Vagree ν ω (y{y. Inl (Inr y)  SIGP (x1 ;; x2)}. FVT (σ y))"
  assume safe:"hpsafe (x1 ;; x2)"
  from safe have
    safe1:"hpsafe x1"
    and safe2:"hpsafe x2"
    by (auto dest: hpsafe.cases)
  have sub1:"(y{y. Inl (Inr y)  SIGP x1}. FVT (σ y))  (y{y. Inl (Inr y)  SIGP (x1 ;; x2)}. FVT (σ y))"
    by auto
  have sub2:"(y{y. Inl (Inr y)  SIGP x2}. FVT (σ y))  (y{y. Inl (Inr y)  SIGP (x1 ;; x2)}. FVT (σ y))"
    by auto
  then show ?case using IH1[OF agree_sub[OF sub1 VA] safe1] IH2[OF agree_sub[OF sub2 VA] safe2] by auto
next
  case (Loop x)
  assume IH:"ν ω. Vagree ν ω (y{y. Inl (Inr y)  SIGP x}. FVT (σ y))  hpsafe x  prog_sem (adjointFO I σ ν) x = prog_sem (adjointFO I σ ω) x"
  assume VA:"Vagree ν ω (y{y. Inl (Inr y)  SIGP (x** )}. FVT (σ y))"
  assume safe:"hpsafe (x** )"
  from safe have
    safe:"hpsafe x"
    by (auto dest: hpsafe.cases)
  have sub:"(y{y. Inl (Inr y)  SIGP (x )}. FVT (σ y))  (y{y. Inl (Inr y)  SIGP (x** )}. FVT (σ y))"
    by auto
  show ?case using IH[OF agree_sub[OF sub VA] safe] by auto
next
  case (Geq x1 x2)
  assume VA:"Vagree ν ω (y{y. Inl (Inr y)  SIGF (Geq x1 x2)}. FVT (σ y))"
  assume safe:"fsafe (Geq x1 x2)"
  then have dsafe1:"dsafe x1" and dsafe2:"dsafe x2" by (auto dest: fsafe.cases)
  have sub1:"(y{y. Inr y  SIGT x1}. FVT (σ y))  (y{y. Inl (Inr y)  SIGF (Geq x1 x2)}. FVT (σ y))"
    by auto
  have sub2:"(y{y. Inr y  SIGT x2}. FVT (σ y))  (y{y. Inl (Inr y)  SIGF (Geq x1 x2)}. FVT (σ y))"
    by auto
  have "dterm_sem (adjointFO I σ ν) x1 = dterm_sem (adjointFO I σ ω) x1"
    by (rule uadmit_dterm_ntadjoint'[OF ssafe good_interp agree_sub[OF sub1 VA] dsafe1])
  moreover have "dterm_sem (adjointFO I σ ν) x2 = dterm_sem (adjointFO I σ ω) x2"
    by (rule uadmit_dterm_ntadjoint'[OF ssafe good_interp agree_sub[OF sub2 VA] dsafe2])
  ultimately show ?case by auto
next
  case (Prop x1 x2 ν ω)
  assume VA:"Vagree ν ω (y{y. Inl (Inr y)  SIGF ( x1 x2)}. FVT (σ y))"
  assume safe:"fsafe ( x1 x2)"
  then have safes:"i. dsafe (x2 i)" using dfree_is_dsafe by auto
  have subs:"j. (y{y. Inr y  SIGT (x2 j)}. FVT (σ y))  (y{y. Inl (Inr y)  SIGF ( x1 x2)}. FVT (σ y))"
    subgoal for j  by auto
    done
  have "i. dterm_sem (adjointFO I σ ν) (x2 i) = dterm_sem (adjointFO I σ ω) (x2 i)"
    by (rule uadmit_dterm_ntadjoint'[OF ssafe good_interp agree_sub[OF subs VA] safes])
  then have vec_eq:"R. (χ i. dterm_sem (adjointFO I σ ν) (x2 i) R) = (χ i. dterm_sem (adjointFO I σ ω) (x2 i) R)"
    by (auto simp add: vec_eq_iff)
  from VA have VAs:"j. Vagree ν ω (y{y. Inr y  SIGT (x2 j)}. FVT (σ y))"
    subgoal for j 
      using agree_sub[OF subs[of j] VA] by auto
    done
  then show ?case 
    using vec_eq by (auto simp add: adjointFO_def)
next
  case (Not x)
  assume IH:"ν ω. Vagree ν ω (y{y. Inl (Inr y)  SIGF x}. FVT (σ y))  fsafe x  fml_sem (adjointFO I σ ν) x = fml_sem (adjointFO I σ ω) x"
  assume VA:"Vagree ν ω (y{y. Inl (Inr y)  SIGF (Not x)}. FVT (σ y))"
  assume safe:"fsafe (Not x)"
  from safe have
    safe:"fsafe x"
    by (auto dest: fsafe.cases)
  have sub:"(y{y. Inl (Inr y)  SIGF x}. FVT (σ y))  (y{y. Inl (Inr y)  SIGF (Not x)}. FVT (σ y))"
    by auto
  show ?case using IH[OF agree_sub[OF sub VA] safe] by auto
next
  case (And x1 x2)
  assume IH1:"ν ω. Vagree ν ω (y{y. Inl (Inr y)  SIGF x1}. FVT (σ y))  fsafe x1  fml_sem (adjointFO I σ ν) x1 = fml_sem (adjointFO I σ ω) x1"
  assume IH2:"ν ω. Vagree ν ω (y{y. Inl (Inr y)  SIGF x2}. FVT (σ y))  fsafe x2  fml_sem (adjointFO I σ ν) x2 = fml_sem (adjointFO I σ ω) x2"
  assume VA:"Vagree ν ω (y{y. Inl (Inr y)  SIGF (And x1 x2)}. FVT (σ y))"
  assume safe:"fsafe (And x1 x2)"
  from safe have
    safe1:"fsafe x1"
and safe2:"fsafe x2"
    by (auto dest: fsafe.cases)
  have sub1:"(y{y. Inl (Inr y)  SIGF x1}. FVT (σ y))   (y{y. Inl (Inr y)  SIGF (And x1 x2)}. FVT (σ y))"
    by auto
  have sub2:"(y{y. Inl (Inr y)  SIGF x2}. FVT (σ y))   (y{y. Inl (Inr y)  SIGF (And x1 x2)}. FVT (σ y))"
    by auto
  show ?case using IH1[OF agree_sub[OF sub1 VA] safe1] IH2[OF agree_sub[OF sub2 VA] safe2] by auto
next
  case (Exists x1 x2)
  assume IH1:"ν ω. Vagree ν ω (y{y. Inl (Inr y)  SIGF x2}. FVT (σ y))  fsafe x2  fml_sem (adjointFO I σ ν) x2 = fml_sem (adjointFO I σ ω) x2"
  assume VA:"Vagree ν ω (y{y. Inl (Inr y)  SIGF (Exists x1 x2)}. FVT (σ y))"
  assume safe:"fsafe (Exists x1 x2)"
  from safe have safe1:"fsafe x2"
    by (auto dest: fsafe.cases)
  have sub1:"(y{y. Inl (Inr y)  SIGF x2}. FVT (σ y))  (y{y. Inl (Inr y)  SIGF (Exists x1 x2)}. FVT (σ y))"
    by auto
  show ?case using IH1[OF agree_sub[OF sub1 VA] safe1] by auto
next
  case (Diamond x1 x2)
  assume IH1:"ν ω. Vagree ν ω (y{y. Inl (Inr y)  SIGP x1}. FVT (σ y))  hpsafe x1  prog_sem (adjointFO I σ ν) x1 = prog_sem (adjointFO I σ ω) x1"
  assume IH2:"ν ω. Vagree ν ω (y{y. Inl (Inr y)  SIGF x2}. FVT (σ y))  fsafe x2  fml_sem (adjointFO I σ ν) x2 = fml_sem (adjointFO I σ ω) x2"
  assume VA:"Vagree ν ω (y{y. Inl (Inr y)  SIGF (Diamond x1 x2)}. FVT (σ y))"
  assume safe:"fsafe (Diamond x1 x2)"
  from safe have
    safe1:"hpsafe x1"
and safe2:"fsafe x2"
    by (auto dest: fsafe.cases)
  have sub1:"(y{y. Inl (Inr y)  SIGP x1}. FVT (σ y))  (y{y. Inl (Inr y)  SIGF (Diamond x1 x2)}. FVT (σ y))"
    by auto
  have sub2:"(y{y. Inl (Inr y)  SIGF x2}. FVT (σ y))  (y{y. Inl (Inr y)  SIGF (Diamond x1 x2)}. FVT (σ y))"
    by auto
  show ?case using IH1[OF agree_sub[OF sub1 VA] safe1] IH2[OF agree_sub[OF sub2 VA] safe2] by auto
next
  case (InContext x1 x2)
  assume IH1:"ν ω. Vagree ν ω (y{y. Inl (Inr y)  SIGF x2}. FVT (σ y))  fsafe x2  fml_sem (adjointFO I σ ν) x2 = fml_sem (adjointFO I σ ω) x2"
  assume VA:"Vagree ν ω (y{y. Inl (Inr y)  SIGF (InContext x1 x2)}. FVT (σ y))"
  assume safe:"fsafe (InContext x1 x2)"
  from safe have  safe1:"fsafe x2"
    by (auto dest: fsafe.cases)
  have sub:"(y{y. Inl (Inr y)  SIGF x2}. FVT (σ y))  (y{y. Inl (Inr y)  SIGF (InContext x1 x2)}. FVT (σ y))"
    by auto
  show ?case using IH1[OF agree_sub[OF sub VA] safe1]  
    unfolding adjointFO_def by auto
qed

lemma uadmit_prog_ntadjoint:
  assumes TUA:"PUadmitFO σ α U"
  assumes VA:"Vagree ν ω (-U)"
  assumes dfree:"i . dsafe (σ i)"
  assumes hpsafe:"hpsafe α"
  assumes good_interp:"is_interp I"
  shows  "prog_sem (adjointFO I σ ν) α = prog_sem (adjointFO I σ ω) α"
proof -
  have sub:"(x{x. Inl (Inr x)  SIGP α}. FVT (σ x))  -U" using TUA unfolding PUadmitFO_def by auto
  have VA':"Vagree ν ω (x{x. Inl (Inr x)  SIGP α}. FVT (σ x))" using agree_sub[OF sub VA] by auto
  show ?thesis 
    apply(rule uadmit_prog_fml_ntadjoint'[OF dfree good_interp])
     subgoal by (rule VA')
    subgoal by (rule hpsafe)
    done
qed

lemma uadmit_fml_ntadjoint:
  assumes TUA:"FUadmitFO σ φ U"
  assumes VA:"Vagree ν ω (-U)"
  assumes dfree:"i . dsafe (σ i)"
  assumes fsafe:"fsafe φ"
  assumes good_interp:"is_interp I"
  shows  "fml_sem (adjointFO I σ ν) φ = fml_sem (adjointFO I σ ω) φ"
proof -
  have sub:"(x{x. Inl (Inr x)  SIGF φ}. FVT (σ x))  -U" using TUA unfolding FUadmitFO_def by auto
  have VA':"Vagree ν ω (x{x. Inl (Inr x)  SIGF φ}. FVT (σ x))" using agree_sub[OF sub VA] by auto
  show ?thesis 
    apply(rule uadmit_prog_fml_ntadjoint'[OF dfree good_interp])
     subgoal by (rule VA')
    subgoal by (rule fsafe)
    done
qed

subsection‹Substitution theorems for terms›
lemma nsubst_sterm:
  fixes I::"('sf, 'sc, 'sz) interp"
  fixes ν::"'sz state"
  shows "TadmitFFO σ θ   (i. dsafe (σ i))  sterm_sem I (TsubstFO θ σ) (fst ν) = sterm_sem (adjointFO I σ ν) θ (fst ν)"
proof (induction rule: TadmitFFO.induct)
  case (TadmitFFO_Fun1 σ args f)
  then show ?case by(auto simp add:  adjointFO_def)
next
  case (TadmitFFO_Fun2 σ args f)
  then show ?case
    apply(auto simp add: adjointFO_def) 
    by (simp add: dsem_to_ssem)
qed (auto)

lemma nsubst_sterm':
  fixes I::"('sf, 'sc, 'sz) interp"
  fixes a b::"'sz simple_state"
  shows "TadmitFFO σ θ  (i. dsafe (σ i))  sterm_sem I (TsubstFO θ σ) a = sterm_sem (adjointFO I σ (a,b)) θ a"
  using nsubst_sterm by (metis fst_conv)

lemma ntsubst_preserves_free:
"dfree θ  (i. dfree (σ i))  dfree(TsubstFO θ σ)"
proof (induction rule: dfree.induct) 
  case (dfree_Fun args i) then show "?case"
    by (cases "i") (auto intro:dfree.intros)
qed (auto intro: dfree.intros)

lemma tsubst_preserves_free:
"dfree θ   (i f'. SFunctions σ i = Some f'  dfree f')  dfree(Tsubst θ σ)"
proof (induction rule: dfree.induct) 
  case (dfree_Fun args i) then show "?case" 
    by (cases "SFunctions σ i") (auto intro:dfree.intros ntsubst_preserves_free)
qed (auto intro: dfree.intros)

lemma subst_sterm:
  fixes I::"('sf, 'sc, 'sz) interp"
  fixes ν::"'sz state"
  shows "
    TadmitF σ θ  
    (i f'. SFunctions σ i = Some f'  dfree f')  
     sterm_sem I (Tsubst θ σ) (fst ν) = sterm_sem (adjoint I σ ν) θ (fst ν)"
proof (induction rule: TadmitF.induct)
  case (TadmitF_Fun1  σ args f f') then
    have subFree:" TadmitFFO (λi. Tsubst (args i) σ) f'" 
      and frees:"i. dfree (Tsubst (args i) σ)" 
      and TFA:"i. TadmitF σ (args i)"
      and NTFA:"TadmitFFO (λi. Tsubst (args i) σ) f'"
      and theIH:"i. sterm_sem I (Tsubst (args i) σ) (fst ν) = sterm_sem (local.adjoint I σ ν) (args i) (fst ν)"
        by auto
      from frees have safes:"i. dsafe (Tsubst (args i) σ)"
        by (simp add: dfree_is_dsafe) 
  assume subFreeer:"(i f'. SFunctions σ i = Some f'  dfree f')"
  note admit = TadmitF_Fun1.hyps(1) and sfree = TadmitF_Fun1.prems(1)
  have IH:"(i. sterm_sem I (Tsubst (args i) σ) (fst ν) = sterm_sem (adjoint I σ ν) (args i) (fst ν))" 
    using  admit TadmitF_Fun1.prems TadmitF_Fun1.IH by auto
  have vec_eq:"(χ i. sterm_sem (local.adjoint I σ ν) (args i) (fst ν)) = (χ i. sterm_sem I (Tsubst (args i) σ) (fst ν))"
    apply(rule vec_extensionality)
    using IH by auto
  assume some:"SFunctions σ f = Some f'" 
  let ?sub = "(λ i. Tsubst (args i) σ)"
  have IH2:"sterm_sem I (TsubstFO f' ?sub) (fst ν) = sterm_sem (adjointFO I ?sub ν) f' (fst ν)"
    apply(rule nsubst_sterm)
     apply(rule subFree)
    by (rule safes)
  show "?case"
    apply (simp add: some)
    unfolding vec_eq IH2
    by (auto simp add: some adjoint_free[OF subFreeer, of σ "(λ x y. x)" I ν] adjointFO_free[OF frees])      
next
  case (TadmitF_Fun2  σ args f) 
  assume none:"SFunctions σ f = None" 
  note admit = TadmitF_Fun2.hyps(1) and sfree = TadmitF_Fun2.prems(1)
  have IH:"(i. TadmitF σ (args i) 
      sterm_sem I (Tsubst (args i) σ) (fst ν) = sterm_sem (adjoint I σ ν) (args i) (fst ν))" 
    using  TadmitF_Fun2.prems TadmitF_Fun2.IH by auto
  have eqs:"i. sterm_sem I (Tsubst (args i) σ) (fst ν) = sterm_sem (adjoint I σ ν) (args i) (fst ν)"
    by (auto simp add: IH admit)
  show "?case" 
    by(auto simp add: none IH adjoint_def vec_extensionality eqs)
  qed auto

lemma nsubst_dterm':
  fixes I::"('sf, 'sc, 'sz) interp"
  fixes ν::"'sz state"
  assumes good_interp:"is_interp I"    
  shows "TadmitFO σ θ  dfree θ  (i. dsafe (σ i))  dterm_sem I (TsubstFO θ σ) ν = dterm_sem (adjointFO I σ ν) θ ν"
proof (induction rule: TadmitFO.induct)
  case (TadmitFO_Fun σ args f)
  assume admit:"i. TadmitFO σ (args i)"
  assume IH:"i. dfree (args i)  (i. dsafe (σ i))  dterm_sem I (TsubstFO (args i) σ) ν = dterm_sem (adjointFO I σ ν) (args i) ν"
  assume free:"dfree ($f f args)"
  assume safe:"i. dsafe (σ i)"
  from free have frees: "i. dfree (args i)" by (auto dest: dfree.cases)
  have sem:"i. dterm_sem I (TsubstFO (args i) σ) ν = dterm_sem (adjointFO I σ ν) (args i) ν"
    using IH[OF frees safe] by auto
  have vecEq:" (χ i. dterm_sem (adjointFO I σ ν) (args i) ν) =
   (χ i. dterm_sem
          Functions = case_sum (Functions I) (λf' _. dterm_sem I (σ f') ν), Predicates = Predicates I, Contexts = Contexts I,
             Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I
          (args i) ν) "
    apply(rule vec_extensionality)
    by (auto simp add: adjointFO_def)
  show " dterm_sem I (TsubstFO ($f f args) σ) ν = dterm_sem (adjointFO I σ ν) ($f f args) ν"
    apply (cases "f") 
     apply (auto simp add: vec_extensionality  adjointFO_def)
    using sem apply auto
    subgoal for a using vecEq by auto
    done
next
  case (TadmitFO_Diff σ θ) 
  hence admit:"TadmitFFO σ θ"
    and admitU:"NTUadmit σ θ UNIV"
    (*and IH : "dfree θ ⟹
          (⋀i. dfree (σ i)) ⟹ dterm_sem I (TsubstFO θ σ) ν = dterm_sem (adjointFO I σ ν) θ ν"*)
    and safe: "dfree (Differential θ)" 
    and freeSub:"i. dsafe (σ i)"
    by auto
  from safe have "False" by (auto dest: dfree.cases)
  then show "dterm_sem I (TsubstFO (Differential θ) σ) ν = dterm_sem (adjointFO I σ ν) (Differential θ) ν"
    by auto
qed (auto simp add: TadmitFO.cases)

lemma ntsubst_free_to_safe:
  "dfree θ  (i. dsafe (σ i))  dsafe (TsubstFO θ σ)"
proof (induction rule: dfree.induct) 
  case (dfree_Fun args i) then show "?case"
    by (cases "i") (auto intro:dsafe.intros ntsubst_preserves_free)
qed (auto intro: dsafe.intros)

lemma ntsubst_preserves_safe:
"dsafe θ  (i. dfree (σ i))  dsafe (TsubstFO θ σ)"
proof (induction rule: dsafe.induct) 
  case (dsafe_Fun args i) then show "?case"
    by (cases "i") (auto intro:dsafe.intros ntsubst_preserves_free dfree_is_dsafe)
next
  case (dsafe_Diff θ) then show "?case"
    by  (auto intro:dsafe.intros ntsubst_preserves_free)
qed (auto simp add: ntsubst_preserves_free intro: dsafe.intros)

lemma tsubst_preserves_safe:
"dsafe θ   (i f'. SFunctions σ i = Some f'  dfree f')  dsafe(Tsubst θ σ)"
proof (induction rule: dsafe.induct) 
  case (dsafe_Fun args i) 
  assume dsafes:"i. dsafe (args i)"
  assume IH:"j. (i f'. SFunctions σ i = Some f'  dfree f')  dsafe (Tsubst (args j) σ)"
  assume frees:"i f. SFunctions σ i = Some f  dfree f"
  have IH':"i. dsafe (Tsubst (args i) σ)"
    using frees IH by auto
  then show "?case" 
    apply auto
    apply(cases "SFunctions σ i")
     subgoal using IH frees by auto
    subgoal for a using frees[of i a] ntsubst_free_to_safe[of a] IH' by auto
    done 
qed (auto intro: dsafe.intros tsubst_preserves_free)

lemma subst_dterm:
  fixes I::"('sf, 'sc, 'sz) interp"
  assumes good_interp:"is_interp I"
  shows "
    Tadmit σ θ 
    dsafe θ 
    (i f'. SFunctions σ i = Some f'  dfree f')  
    (f f'. SPredicates σ f = Some f'   fsafe f') 
    (ν. dterm_sem I (Tsubst θ σ) ν = dterm_sem (adjoint I σ ν) θ ν)"
proof (induction rule: Tadmit.induct)
  case (Tadmit_Fun1 σ args f f' ν) 
  note safe = Tadmit_Fun1.prems(1) and sfree = Tadmit_Fun1.prems(2) and TA = Tadmit_Fun1.hyps(1)
    and some = Tadmit_Fun1.hyps(2) and NTA = Tadmit_Fun1.hyps(3)
  hence safes:"i. dsafe (args i)" by auto
  have IH:"(ν'. i. dsafe (args i) 
      dterm_sem I (Tsubst (args i) σ) ν = dterm_sem (adjoint I σ ν) (args i) ν)" 
    using  Tadmit_Fun1.prems Tadmit_Fun1.IH by auto
  have eqs:"i ν'. dterm_sem I (Tsubst (args i) σ) ν = dterm_sem (adjoint I σ ν) (args i) ν"
    by (auto simp add: IH safes)
  let ?sub = "(λ i. Tsubst (args i) σ)"
  have subSafe:"(i. dsafe (?sub i))"
    using tsubst_preserves_safe[OF safes sfree]
    by (simp add: safes sfree tsubst_preserves_safe)
  have freef:"dfree f'" using sfree some by auto 
  have IH2:"dterm_sem I (TsubstFO f' ?sub) ν = dterm_sem (adjointFO I ?sub ν) f' ν"
    by (simp add: nsubst_dterm'[OF good_interp NTA freef subSafe])
  have vec:"(χ i. dterm_sem I (Tsubst (args i) σ) ν) = (χ i. dterm_sem (local.adjoint I σ ν) (args i) ν)"
    apply(auto simp add: vec_eq_iff)
    subgoal for i
      using IH[of i, OF safes[of i]] 
      by auto
    done
  show "?case" 
    using IH safes eqs apply (auto simp add:  IH2  some good_interp)
    using some unfolding adjoint_def adjointFO_def by auto
next
  case (Tadmit_Fun2 σ args f ν) 
  note safe = Tadmit_Fun2.prems(1) and sfree = Tadmit_Fun2.prems(2) and TA = Tadmit_Fun2.hyps(1)
  and none = Tadmit_Fun2.hyps(2) 
  hence safes:"i. dsafe (args i)" by auto
  have IH:"(ν'. i. dsafe (args i) 
      dterm_sem I (Tsubst (args i) σ) ν = dterm_sem (adjoint I σ ν) (args i) ν)" 
  using  Tadmit_Fun2.prems Tadmit_Fun2.IH by auto
  have Ieq:"Functions I f = Functions (adjoint I σ ν) f"
    using none unfolding adjoint_def by auto
  have vec:"(χ i. dterm_sem I (Tsubst (args i) σ) ν) = (χ i. dterm_sem (adjoint I σ ν) (args i) ν)"
    apply(auto simp add: vec_eq_iff)
    subgoal for i using IH[of i, OF safes[of i]] by auto
    done
  show "?case" using none IH Ieq vec by auto
next
  case (Tadmit_Diff σ θ)  then
  have TA:"Tadmit σ θ"
    and TUA:"TUadmit σ θ UNIV"
    and IH:"dsafe θ  (i f'. SFunctions σ i = Some f'  dfree f')  (ν. dterm_sem I (Tsubst θ σ) ν = dterm_sem (local.adjoint I σ ν) θ ν)"
    and safe:"dsafe (Differential θ)"
    and sfree:"i f'1. SFunctions σ i = Some f'1  dfree f'1"
    and spsafe:"f f'. SPredicates σ f = Some f'   fsafe f'"
      by auto
  from sfree have sdsafe:"f f'. SFunctions σ f = Some f'  dsafe f'"
    using dfree_is_dsafe by auto  
  have VA:"ν ω. Vagree ν ω (-UNIV)" unfolding Vagree_def by auto
  from safe have free:"dfree θ" by (auto dest: dsafe.cases intro: dfree.intros)
  from free have tsafe:"dsafe θ" using dfree_is_dsafe by auto
  have freeSubst:"dfree (Tsubst θ σ)" 
    using tsubst_preserves_free[OF free sfree]
    using Tadmit_Diff.prems(2) free tsubst_preserves_free by blast 
  have IH':"ν. dterm_sem I (Tsubst θ σ) ν = dterm_sem (local.adjoint I σ ν) θ ν"
    using IH[OF tsafe sfree] by auto
  have sem_eq:"ν'. dsafe θ  is_interp I  dterm_sem (local.adjoint I σ ν) θ = dterm_sem (local.adjoint I σ ν') θ"
    subgoal for ν'
      using uadmit_dterm_adjoint[OF TUA VA sfree spsafe, of "(λ x y. x)" "(λ x y. x)" I ν ν']
      by auto
    done
  have IH'':"ν'. dterm_sem I (Tsubst θ σ) ν' = dterm_sem (local.adjoint I σ ν) θ ν'"
    subgoal for ν'
      using sem_eq[OF tsafe good_interp, of ν'] IH'[of ν'] by auto
    done
  have sem_eq:"sterm_sem I (Tsubst θ σ) = sterm_sem (local.adjoint I σ ν) θ" 
    apply (auto simp add: fun_eq_iff)
    subgoal for ν'
      apply (cases "ν'")
      subgoal for ν''
        apply auto
        using dsem_to_ssem[OF free, of "(local.adjoint I σ ν)" "(ν',ν')"] dsem_to_ssem[OF freeSubst, of I "(ν',ν')"] IH'[of "(ν)"]
        apply auto
        using IH'' by auto
      done
    done
  show "?case"
    apply (auto simp add: directional_derivative_def fun_eq_iff)
    using sterm_determines_frechet[OF 
        good_interp 
        adjoint_safe[OF good_interp sfree] 
        tsubst_preserves_free[OF free sfree] 
        free sem_eq]
    by auto
qed auto  

subsection‹Substitution theorems for ODEs›
lemma osubst_preserves_safe:
  assumes ssafe:"ssafe σ"
  shows "(osafe ODE  Oadmit σ ODE U  osafe (Osubst ODE σ))"
proof (induction rule: osafe.induct)
  case (osafe_Var c)
  then show ?case using ssafe unfolding ssafe_def by (cases "SODEs σ c", auto intro: osafe.intros)
next
  case (osafe_Sing θ x)
  then show ?case 
    using tsubst_preserves_free ssafe unfolding ssafe_def by (auto intro: osafe.intros)
next
  case (osafe_Prod ODE1 ODE2)
  moreover have "Oadmit σ ODE1 U" "Oadmit σ ODE2 U" "ODE_dom (Osubst ODE1 σ)   ODE_dom (Osubst ODE2 σ) = {}"
    using osafe_Prod.prems by (auto dest: Oadmit.cases) 
  ultimately show ?case by (auto intro: osafe.intros)
qed

lemma nosubst_preserves_safe:
  assumes sfree:"i. dfree (σ i)"
  fixes α ::"('a + 'd, 'b, 'c) hp" and φ ::"('a + 'd, 'b, 'c) formula"
  shows "(osafe ODE  OUadmitFO σ ODE U  osafe (OsubstFO ODE σ))"
proof (induction rule: osafe.induct)
  case (osafe_Var c)
  then show ?case by (auto intro: osafe.intros)
next
  case (osafe_Sing θ x)
  then show ?case using sfree ntsubst_preserves_free[of θ σ] unfolding OUadmitFO_def by (auto intro: osafe.intros)
next
  case (osafe_Prod ODE1 ODE2)
  assume safe1:"osafe ODE1"
    and safe2:"osafe ODE2"
    and disj:"ODE_dom ODE1  ODE_dom ODE2 = {}"
    and IH1:"OUadmitFO σ ODE1 U  osafe (OsubstFO ODE1 σ)"
    and IH2:"OUadmitFO σ ODE2 U  osafe (OsubstFO ODE2 σ)"
    and NOUA:"OUadmitFO σ (OProd ODE1 ODE2) U"    
  have nosubst_preserves_ODE_dom:"ODE. ODE_dom (OsubstFO ODE σ) = ODE_dom ODE"
    subgoal for ODE
      apply(induction "ODE")
        by auto
    done
  have disj':"ODE_dom (OsubstFO ODE1 σ)  ODE_dom (OsubstFO ODE2 σ) = {}"
    using disj nosubst_preserves_ODE_dom by auto
  from NOUA have NOUA1:"OUadmitFO σ ODE1 U" and NOUA2:"OUadmitFO σ  ODE2 U"  unfolding OUadmitFO_def by auto
  then show ?case using IH1[OF NOUA1] IH2[OF NOUA2] disj' by (auto intro: osafe.intros)
qed

lemma nsubst_dterm:
  fixes I::"('sf, 'sc, 'sz) interp"
  fixes ν::"'sz state"
  fixes ν'::"'sz state"
  assumes good_interp:"is_interp I"    
  shows "TadmitFO σ θ  dsafe θ  (i. dsafe (σ i))  dterm_sem I (TsubstFO θ σ) ν = dterm_sem (adjointFO I σ ν) θ ν"
proof (induction rule: TadmitFO.induct)
  case (TadmitFO_Diff σ θ) then
  have subFree:"(i. dsafe (σ i))"
    and  NTFA:"TadmitFFO σ θ"
    and substFree:"dfree (TsubstFO θ σ)"
    and dsafe:"dsafe (Differential θ)"
    and subSafe:"i. dsafe (σ i)"
    and  NTU:"NTUadmit σ θ UNIV"  
    by auto   
  have dfree:"dfree θ" using dsafe by auto
  then show ?case
    apply auto
    apply (unfold directional_derivative_def) 
    apply (rule sterm_determines_frechet)
    subgoal using good_interp by auto
       subgoal using adjointFO_safe[OF good_interp, of σ] subSafe by auto
      subgoal  using substFree by auto
     subgoal using dfree by auto
    subgoal
      apply(rule ext)
      subgoal for x
        using nsubst_sterm'[of  σ θ I "(fst ν)" "(snd ν)", OF NTFA subSafe] apply auto
      proof -
        assume sem:"sterm_sem I (TsubstFO θ σ) (fst ν) = sterm_sem (adjointFO I σ ν) θ (fst ν)"
        have VA:"ν ω. Vagree ν (x,snd ν) (-UNIV)" unfolding Vagree_def by auto
        show "sterm_sem I (TsubstFO θ σ) x = sterm_sem (adjointFO I σ ν) θ x"
          using uadmit_sterm_ntadjoint[OF NTU VA subSafe, OF  good_interp, of "(x, snd ν)"]
            nsubst_sterm[OF NTFA subSafe, of I ν ] 
          apply auto
          using NTU VA dfree_is_dsafe  dsafe subSafe substFree good_interp uadmit_sterm_ntadjoint
          by (metis NTFA fst_eqD nsubst_sterm)
      qed
    done
  done
next
  case (TadmitFO_Fun σ args f)
  then show ?case apply auto apply(cases f) unfolding adjointFO_def by auto
qed (auto)
  
lemma nsubst_ode:
  fixes I::"('sf, 'sc, 'sz) interp"
  fixes ν::"'sz state"
  fixes ν'::"'sz state"
  assumes good_interp:"is_interp I"    
  shows "osafe ODE  OadmitFO σ ODE U  (i. dsafe (σ i))  ODE_sem I (OsubstFO ODE σ) (fst ν)= ODE_sem (adjointFO I σ ν) ODE (fst ν)"
proof (induction rule: osafe.induct)
  case (osafe_Var c)
  then show ?case unfolding OUadmitFO_def adjointFO_def by auto
next
  case (osafe_Sing θ x)
  then show ?case apply auto
    using nsubst_sterm' [of  σ θ I "(fst ν)" "(snd ν)"] by auto
next
  case (osafe_Prod ODE1 ODE2) then
  have NO1:"OadmitFO σ ODE1 U" and NO2:"OadmitFO σ ODE2 U" 
    unfolding OUadmitFO_def by auto
  have "ODE_sem I (OsubstFO ODE1 σ) (fst ν) = ODE_sem (adjointFO I σ ν) ODE1 (fst ν)"
    "ODE_sem I (OsubstFO ODE2 σ) (fst ν) = ODE_sem (adjointFO I σ ν) ODE2 (fst ν)" using osafe_Prod.IH osafe_Prod.prems osafe_Prod.hyps
    using NO1 NO2 by auto
  then show ?case by auto
qed
    
lemma osubst_preserves_BVO:
  shows "BVO (OsubstFO ODE σ) = BVO ODE"
proof (induction "ODE")
qed (auto)

lemma osubst_preserves_ODE_vars:
  shows "ODE_vars I (OsubstFO ODE σ) = ODE_vars (adjointFO I σ ν) ODE"
proof (induction "ODE")
qed (auto simp add: adjointFO_def)

lemma osubst_preserves_semBV:
  shows "semBV I (OsubstFO ODE σ) = semBV (adjointFO I σ ν) ODE"
proof (induction "ODE")
qed (auto simp add: adjointFO_def)

lemma nsubst_mkv:
  fixes I::"('sf, 'sc, 'sz) interp"
  fixes ν::"'sz state"
  fixes ν'::"'sz state"
  assumes good_interp:"is_interp I"  
  assumes NOU:"OadmitFO σ ODE U"
  assumes osafe:"osafe ODE "
  assumes frees:"(i. dsafe (σ i))"
  shows "(mk_v I (OsubstFO ODE σ) ν (fst ν')) 
    = (mk_v (adjointFO I σ ν') ODE ν (fst ν'))"
  apply(rule agree_UNIV_eq)
  using mk_v_agree[of "adjointFO I σ ν'" "ODE" ν "fst ν'"]
  using mk_v_agree[of "I" "OsubstFO ODE σ" ν "fst ν'"] 
  unfolding Vagree_def 
  using nsubst_ode[OF good_interp osafe NOU frees, of ν']
  apply auto
   subgoal for i
     apply(erule allE[where x=i])+
     apply(cases "Inl i  semBV I (OsubstFO ODE σ)")
      using  osubst_preserves_ODE_vars
      by (metis (full_types))+
  subgoal for i
    apply(erule allE[where x=i])+
    apply(cases "Inr i  BVO ODE")
     using  osubst_preserves_ODE_vars
     by (metis (full_types))+
  done

lemma ODE_unbound_zero:
  fixes i
  shows "Inl i  BVO ODE  ODE_sem I ODE x $ i = 0"
proof (induction ODE)
qed (auto)

lemma ODE_bound_effect:
  fixes s t sol ODE X b
  assumes s:"s  {0..t}"
  assumes sol:"(sol solves_ode (λ_. ODE_sem I ODE)) {0..t}  X"
  shows "Vagree (sol 0,b) (sol s, b) (-(BVO ODE))"
proof -
  have "i. Inl i  BVO ODE   ( s. s  {0..t}  sol s $ i = sol 0 $ i)"
    apply auto
    apply (rule constant_when_zero)
         using s sol apply auto
    using ODE_unbound_zero solves_ode_subset 
    by fastforce+
  then show "Vagree (sol 0, b) (sol s, b) (- BVO ODE)"
    unfolding Vagree_def 
    using s  by (metis Compl_iff fst_conv  snd_conv)
qed

lemma NO_sub:"OadmitFO σ ODE A  B  A  OadmitFO σ ODE B"
  by(induction ODE, auto simp add: OUadmitFO_def)

lemma NO_to_NOU:"OadmitFO σ ODE S  OUadmitFO σ ODE S"
  by(induction ODE, auto simp add: OUadmitFO_def)
  
subsection‹Substitution theorems for formulas and programs›
lemma nsubst_hp_fml:
  fixes I::"('sf, 'sc, 'sz) interp"
  assumes good_interp:"is_interp I"    
  shows " (NPadmit σ α  (hpsafe α  (i. dsafe (σ i))  ( ν ω. ((ν, ω)  prog_sem I (PsubstFO α σ)) = ((ν, ω)  prog_sem (adjointFO I σ ν) α)))) 
    (NFadmit σ φ  (fsafe φ  (i. dsafe (σ i))  ( ν. (ν  fml_sem I (FsubstFO φ σ)) = (ν  fml_sem (adjointFO I σ ν) φ))))"
proof (induction rule: NPadmit_NFadmit.induct)
  case (NPadmit_Pvar σ a)
  then show ?case unfolding adjointFO_def by auto
next
  case (NPadmit_ODE σ ODE φ) then
  have  NOU:"OadmitFO σ ODE (BVO ODE)"
    and NFA:"NFadmit σ φ"
    and NFU:"FUadmitFO σ φ (BVO ODE)"
    and fsafe:"fsafe (FsubstFO φ σ)"
    and IH:"fsafe φ  (i. dsafe (σ i))  (ν. (ν  fml_sem I (FsubstFO φ σ)) = (ν  fml_sem (adjointFO I σ ν) φ))"
    and osafe':"osafe (OsubstFO ODE σ)"
      by auto
  have "hpsafe (EvolveODE ODE φ)   (i. dsafe (σ i))  (ν ω. ((ν, ω)  prog_sem I (PsubstFO (EvolveODE ODE φ) σ)) = ((ν, ω)  prog_sem (adjointFO I σ ν) (EvolveODE ODE φ)))"
  proof -
    assume safe:"hpsafe (EvolveODE ODE φ)"
    then have osafe:"osafe ODE" and fsafe:"fsafe φ" by auto
    assume frees:"(i. dsafe (σ i))"
    fix ν ω
    show "((ν, ω)  prog_sem I (PsubstFO (EvolveODE ODE φ) σ)) = ((ν, ω)  prog_sem (adjointFO I σ ν) (EvolveODE ODE φ))"
    proof (auto)
      fix b 
        and sol :: "real (real, 'sz) vec" 
        and t :: real
      assume eq1:"ν = (sol 0, b)"
      assume eq2:"ω = mk_v I (OsubstFO ODE σ) (sol 0, b) (sol t)"
      assume t:"0  t"
      assume sol:"(sol solves_ode (λa. ODE_sem I (OsubstFO ODE σ))) {0..t} 
         {x. mk_v I (OsubstFO ODE σ) (sol 0, b) x  fml_sem I (FsubstFO φ σ)}"
      have agree_sem:"t. Vagree (mk_v I (OsubstFO ODE σ) (sol 0, b) (sol t)) (sol 0, b) (- (Inl ` ODE_vars I (OsubstFO ODE σ)  Inr ` ODE_vars I (OsubstFO ODE σ)))"
        subgoal for t
          using mk_v_agree[of I "OsubstFO ODE σ" "(sol 0, b)" "sol t"] unfolding Vagree_def apply auto
          done
        done
      have bv_sub:"(-BVO ODE)  - (Inl ` ODE_vars I (OsubstFO ODE σ)  Inr ` ODE_vars I (OsubstFO ODE σ))"
        by(induction ODE, auto) 
      have agree:"t. Vagree (mk_v I (OsubstFO ODE σ) (sol 0, b) (sol t)) (sol 0, b) (- BVO ODE)"
        using agree_sub[OF bv_sub agree_sem] by auto
      ― ‹Necessary›
      have mkv:"t. mk_v I (OsubstFO ODE σ) (sol 0, b) (sol t) = mk_v (adjointFO I σ (sol t, b)) ODE (sol 0, b) (sol t)"
        using nsubst_mkv[OF good_interp NOU osafe frees]
        by auto
      have hmm:"s. s  {0..t}  Vagree (sol 0,b) (sol s, b) (-(BVO ODE))"
        using ODE_bound_effect sol
        by (metis osubst_preserves_BVO)
      have FVT_sub:"(y{y. Inl (Inr y)  SIGO ODE}. FVT (σ y))  (-(BVO ODE))"
        using NOU NO_to_NOU OUadmitFO_def 
        by fastforce
      have agrees:"s. s  {0..t}  Vagree (sol 0,b) (sol s, b) (y{y. Inl (Inr y)  SIGO ODE}. FVT (σ y))" 
        subgoal for s using agree_sub[OF FVT_sub hmm[of s]] by auto done
      have "s. s  {0..t}  mk_v (adjointFO I σ (sol s, b)) ODE  = mk_v (adjointFO I σ (sol 0, b)) ODE"
        subgoal for s
          apply (rule uadmit_mkv_ntadjoint)
             prefer 3
             using NOU hmm[of s] NO_to_NOU unfolding OUadmitFO_def Vagree_def
             apply fastforce   
            using frees good_interp osafe by auto
        done
      then have mkva:"s. s  {0..t}  mk_v (adjointFO I σ (sol s, b)) ODE (sol 0, b) (sol s) = mk_v (adjointFO I σ (sol 0, b)) ODE (sol 0, b) (sol s)"
        by presburger
      have main_eq:"s. s  {0..t}   mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s) = mk_v (adjointFO I σ (sol 0, b)) ODE (sol 0, b) (sol s) "
        using mkv mkva by auto
      note mkvt = main_eq[of t]
      have fml_eq1:"s. s  {0..t}  
          (mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s)  fml_sem I (FsubstFO φ σ)) 
        = (mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s)  fml_sem (adjointFO I σ (mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s))) φ)"
        using IH[OF fsafe frees] by auto
      have fml_eq2:"s. s  {0..t}  
        ((mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s)  fml_sem (adjointFO I σ (mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s))) φ)
        =(mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s)  fml_sem (adjointFO I σ (sol 0, b)) φ))"
        subgoal for s
          using NFU frees fsafe good_interp mk_v_agree osubst_preserves_ODE_vars uadmit_fml_ntadjoint
          using agree by blast
        done
      have fml_eq3:"s. s  {0..t} 
        (mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s)  fml_sem (adjointFO I σ (sol 0, b)) φ) = (mk_v (adjointFO I σ (sol 0,b)) ODE (sol 0, b) (sol s)  fml_sem (adjointFO I σ (sol 0, b)) φ) "
        using main_eq by auto
      have fml_eq: "s. s  {0..t} 
         (mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s)  fml_sem I (FsubstFO φ σ)) 
          =  (mk_v (adjointFO I σ (sol 0,b)) ODE (sol 0, b) (sol s)  fml_sem (adjointFO I σ (sol 0, b)) φ)"
        using fml_eq1 fml_eq2 fml_eq3 by meson
      have sem_eq:"t. ODE_sem I (OsubstFO ODE σ) (sol t) = ODE_sem (adjointFO I σ (sol t, b)) ODE (sol t)"
        subgoal for t
          using nsubst_ode[OF good_interp osafe NOU frees, of "(sol t,b)"] by auto
        done
      have sem_fact:"s. s  {0..t}  ODE_sem I (OsubstFO ODE σ) (sol s) = ODE_sem (adjointFO I σ (sol 0, b)) ODE (sol s)"
        subgoal for s
          using nsubst_ode[OF good_interp osafe NOU frees, of "(sol s, b)"]
          uadmit_ode_ntadjoint'[OF frees good_interp agrees[of s] osafe]
          by auto
        done
      have sol':"(sol solves_ode (λ_. ODE_sem (adjointFO I σ (sol 0, b)) ODE)) {0..t}
         {x. mk_v I (OsubstFO ODE σ) (sol 0, b) x  fml_sem I (FsubstFO φ σ)}"
        apply (rule solves_ode_congI)
            apply (rule sol)
           subgoal for ta by auto
          subgoal for ta by (rule sem_fact[of ta])
         subgoal by (rule refl)
        subgoal by (rule refl)
        done
      have sub:"s. s  {0..t} 
               sol s  {x. (mk_v (adjointFO I σ (sol 0,b)) ODE (sol 0, b) x  fml_sem (adjointFO I σ (sol 0, b)) φ)}"
        using fml_eq rangeI t sol solves_ode_domainD by fastforce
      have sol'':"(sol solves_ode (λc. ODE_sem (adjointFO I σ (sol 0, b)) ODE)) {0..t}
 {x. mk_v (adjointFO I σ (sol 0, b)) ODE (sol 0, b) x  fml_sem (adjointFO I σ (sol 0, b)) φ}"
        apply (rule solves_odeI)
         subgoal using sol' solves_ode_vderivD by blast
        using sub by auto
      show "sola. sol 0 = sola 0 
          (ta. mk_v I (OsubstFO ODE σ) (sol 0, b) (sol t) = mk_v (adjointFO I σ (sol 0, b)) ODE (sola 0, b) (sola ta) 
                0  ta 
                (sola solves_ode (λa. ODE_sem (adjointFO I σ (sol 0, b)) ODE)) {0..ta}
                 {x. mk_v (adjointFO I σ (sol 0, b)) ODE (sola 0, b) x  fml_sem (adjointFO I σ (sol 0, b)) φ})"
        apply(rule exI[where x=sol])
        apply(rule conjI)
         subgoal by (rule refl)
        apply(rule exI[where x=t])
        apply(rule conjI)
         subgoal using  mkvt t by auto
        apply(rule conjI)
         subgoal by (rule t)
        subgoal by (rule sol'') 
        done
  next
    fix b 
      and sol::"real  (real, 'sz) vec" 
      and t::real
    assume eq1:"ν = (sol 0, b)"
    assume eq2:"ω = mk_v (adjointFO I σ (sol 0, b)) ODE (sol 0, b) (sol t)"
    assume t:"0  t"
    assume sol:"(sol solves_ode (λa. ODE_sem (adjointFO I σ (sol 0, b)) ODE)) {0..t}
     {x. mk_v (adjointFO I σ (sol 0, b)) ODE (sol 0, b) x  fml_sem (adjointFO I σ (sol 0, b)) φ}"
    have agree_sem:"t. Vagree (mk_v I (OsubstFO ODE σ) (sol 0, b) (sol t)) (sol 0, b) (- (Inl ` ODE_vars I (OsubstFO ODE σ)  Inr ` ODE_vars I (OsubstFO ODE σ)))"
      subgoal for t
        using mk_v_agree[of I "OsubstFO ODE σ" "(sol 0, b)" "sol t"] unfolding Vagree_def apply auto
        done
      done
    have bv_sub:"(-BVO ODE)  - (Inl ` ODE_vars I (OsubstFO ODE σ)  Inr ` ODE_vars I (OsubstFO ODE σ))"
      by(induction ODE, auto) 
    have agree:"t. Vagree (mk_v I (OsubstFO ODE σ) (sol 0, b) (sol t)) (sol 0, b) (- BVO ODE)"
      using agree_sub[OF bv_sub agree_sem] by auto
    ― ‹Necessary›
    have mkv:"t. mk_v I (OsubstFO ODE σ) (sol 0, b) (sol t) = mk_v (adjointFO I σ (sol t, b)) ODE (sol 0, b) (sol t)"
      using nsubst_mkv[OF good_interp NOU osafe frees]
      by auto
    have hmm:"s. s  {0..t}  Vagree (sol 0,b) (sol s, b) (-(BVO ODE))"
      using ODE_bound_effect sol
      by (metis osubst_preserves_ODE_vars)
    have FVT_sub:"(y{y. Inl (Inr y)  SIGO ODE}. FVT (σ y))  (-(BVO ODE))"
      using NOU NO_to_NOU unfolding OUadmitFO_def by fastforce
    have agrees:"s. s  {0..t}  Vagree (sol 0,b) (sol s, b) (y{y. Inl (Inr y)  SIGO ODE}. FVT (σ y))" 
      subgoal for s using agree_sub[OF FVT_sub hmm[of s]] by auto done
    have "s. s  {0..t}  mk_v (adjointFO I σ (sol s, b)) ODE  = mk_v (adjointFO I σ (sol 0, b)) ODE"
      subgoal for s
        apply (rule uadmit_mkv_ntadjoint)
           prefer 3
           using NOU hmm[of s] NO_to_NOU unfolding OUadmitFO_def Vagree_def
           apply fastforce   
          using frees good_interp osafe by auto
        done
    then have mkva:"s. s  {0..t}  mk_v (adjointFO I σ (sol s, b)) ODE (sol 0, b) (sol s) = mk_v (adjointFO I σ (sol 0, b)) ODE (sol 0, b) (sol s)"
      by presburger
    have main_eq:"s. s  {0..t}   mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s) = mk_v (adjointFO I σ (sol 0, b)) ODE (sol 0, b) (sol s) "
      using mkv mkva by auto
    note mkvt = main_eq[of t]
    have fml_eq1:"s. s  {0..t}  
        (mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s)  fml_sem I (FsubstFO φ σ)) 
      = (mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s)  fml_sem (adjointFO I σ (mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s))) φ)"
      using IH[OF fsafe frees] by auto
    have fml_eq2:"s. s  {0..t}  
      ((mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s)  fml_sem (adjointFO I σ (mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s))) φ)
      =(mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s)  fml_sem (adjointFO I σ (sol 0, b)) φ))"
        using  NFU frees fsafe good_interp mk_v_agree osubst_preserves_ODE_vars uadmit_fml_ntadjoint agree by blast
      
    have fml_eq3:"s. s  {0..t} 
     (mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s)  fml_sem (adjointFO I σ (sol 0, b)) φ) = (mk_v (adjointFO I σ (sol 0,b)) ODE (sol 0, b) (sol s)  fml_sem (adjointFO I σ (sol 0, b)) φ) "
     using main_eq by auto
    have fml_eq: "s. s  {0..t} 
      (mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s)  fml_sem I (FsubstFO φ σ)) 
       =  (mk_v (adjointFO I σ (sol 0,b)) ODE (sol 0, b) (sol s)  fml_sem (adjointFO I σ (sol 0, b)) φ)"
      using fml_eq1 fml_eq2 fml_eq3 by meson
     have sem_eq:"t. ODE_sem I (OsubstFO ODE σ) (sol t) = ODE_sem (adjointFO I σ (sol t, b)) ODE (sol t)"
       subgoal for t
         using nsubst_ode[OF good_interp osafe NOU frees, of "(sol t,b)"] by auto
       done
    have sem_fact:"s. s  {0..t}  ODE_sem I (OsubstFO ODE σ) (sol s) = ODE_sem (adjointFO I σ (sol 0, b)) ODE (sol s)"
      subgoal for s
        using nsubst_ode[OF good_interp osafe NOU frees, of "(sol s, b)"]
        uadmit_ode_ntadjoint'[OF frees good_interp agrees[of s] osafe]
        by auto
      done
    have sol':"
      (sol solves_ode (λa. ODE_sem I (OsubstFO ODE σ))) {0..t}  {x. mk_v (adjointFO I σ (sol 0, b)) ODE (sol 0, b) x  fml_sem (adjointFO I σ (sol 0, b)) φ}"
      apply (rule solves_ode_congI)
          apply (rule sol)
         subgoal for ta by auto
        subgoal for ta using sem_fact[of ta] by auto
       subgoal by (rule refl)
      subgoal by (rule refl)
      done
    have sub:"s. s  {0..t} 
             sol s  {x. (mk_v (adjointFO I σ (sol 0,b)) ODE (sol 0, b) x  fml_sem (adjointFO I σ (sol 0, b)) φ)}"
      using fml_eq rangeI t sol solves_ode_domainD by fastforce
    have sol'':"(sol solves_ode (λa. ODE_sem I (OsubstFO ODE σ))) {0..t} {x. mk_v I (OsubstFO ODE σ) (sol 0, b) x  fml_sem I (FsubstFO φ σ)}"
      apply (rule solves_odeI)
       subgoal using sol' solves_ode_vderivD by blast
      using sub fml_eq by blast
    show "sola. sol 0 = sola 0 
          (ta. mk_v (adjointFO I σ (sol 0, b)) ODE (sol 0, b) (sol t) = mk_v I (OsubstFO ODE σ) (sola 0, b) (sola ta) 
                0  ta 
                (sola solves_ode (λa. ODE_sem I (OsubstFO ODE σ))) {0..ta} {x. mk_v I (OsubstFO ODE σ) (sola 0, b) x  fml_sem I (FsubstFO φ σ)})"
      apply(rule exI[where x=sol])
      apply(rule conjI)
       subgoal by (rule refl)
      apply(rule exI[where x=t])
      apply(rule conjI)
       subgoal using t mkvt by auto
      apply(rule conjI)
       subgoal by (rule t)
      subgoal by (rule sol'')
      done
    qed
  qed
  then show ?case by auto 
next
  case (NPadmit_Assign σ θ x)
  then show ?case using nsubst_dterm[OF good_interp, of σ θ] by auto
next
  case (NPadmit_DiffAssign σ θ x)
  then show ?case using nsubst_dterm[OF good_interp, of σ θ] by auto
next
  case (NFadmit_Geq σ θ1 θ2)
  then show ?case 
    using nsubst_dterm[OF good_interp, of σ θ1] 
    using nsubst_dterm[OF good_interp, of σ θ2] by auto
next
  case (NFadmit_Prop σ args f)
  assume NTA:"i. TadmitFO σ (args i)"
  have "ν.  fsafe ( f args)   (i. dsafe (σ i))  (ν  fml_sem I (FsubstFO ( f args) σ)) = (ν  fml_sem (adjointFO I σ ν) ( f args))"
  proof -
    fix ν
    assume safe:"fsafe ( f args)"
    from safe have safes:"i. dsafe (args i)" using dfree_is_dsafe by auto
    assume subFree:"(i. dsafe (σ i))"
    have vec_eq:"(χ i. dterm_sem (adjointFO I σ ν) (args i) ν) = (χ i. dterm_sem I (TsubstFO (args i) σ) ν)"
      apply(rule vec_extensionality)
      using nsubst_dterm[OF good_interp NTA safes subFree] by auto
    then show "?thesis ν" unfolding adjointFO_def by auto
  qed
  then show ?case by auto 
next
  case (NPadmit_Sequence σ a b) then 
  have PUA:"PUadmitFO σ b (BVP (PsubstFO a σ))"
    and PA:"NPadmit σ a"
    and IH1:"hpsafe a  (i. dsafe (σ i))  (ν ω. ((ν, ω)  prog_sem I (PsubstFO a σ)) = ((ν, ω)  prog_sem (adjointFO I σ ν) a))"
    and IH2:"hpsafe b  (i. dsafe (σ i))  (ν ω. ((ν, ω)  prog_sem I (PsubstFO b σ)) = ((ν, ω)  prog_sem (adjointFO I σ ν) b))"
    and hpsafeS:"hpsafe (PsubstFO a σ)"
     by auto
  have "hpsafe (a ;; b)  (i. dsafe (σ i))  (ν ω. ((ν, ω)  prog_sem I (PsubstFO (a ;; b) σ)) = ((ν, ω)  prog_sem (adjointFO I σ ν) (a ;; b)))"
  proof -
    assume hpsafe:"hpsafe (a ;; b)"
    assume ssafe:"(i. dsafe (σ i))"
    from hpsafe have safe1:"hpsafe a" and safe2:"hpsafe b" by (auto dest: hpsafe.cases)
    fix ν ω
    have agree:"μ. (ν, μ)  prog_sem I (PsubstFO a σ)  Vagree ν μ (-BVP(PsubstFO a σ))"
      subgoal for μ
        using bound_effect[OF good_interp, of "(PsubstFO a σ)" ν , OF hpsafeS] by auto
      done
    have sem_eq:"μ. (ν, μ)  prog_sem I (PsubstFO a σ)  
        ((μ, ω)  prog_sem (adjointFO I σ ν) b) =
        ((μ, ω)  prog_sem (adjointFO I σ μ) b)"
      subgoal for μ
      proof -
        assume assm:"(ν, μ)  prog_sem I (PsubstFO a σ)"
        show "((μ, ω)  prog_sem (adjointFO I σ ν) b) = ((μ, ω)  prog_sem (adjointFO I σ μ) b)"
          using uadmit_prog_ntadjoint [OF PUA agree[OF assm] ssafe safe2 good_interp] 
          by auto
      qed
      done      
    have "((ν, ω)  prog_sem I (PsubstFO (a ;; b) σ)) = ( μ. (ν, μ)  prog_sem I (PsubstFO a σ)  (μ, ω)  prog_sem I (PsubstFO b σ))"
      by auto
    moreover have "... = ( μ. (ν, μ)  prog_sem I (PsubstFO a σ)  (μ, ω)  prog_sem (adjointFO I σ μ) b)"
      using IH2[OF safe2 ssafe] by auto
    moreover have "... = ( μ. (ν, μ)  prog_sem I (PsubstFO a σ)  (μ, ω)  prog_sem (adjointFO I σ ν) b)"
      using sem_eq by auto
    moreover have "... = ( μ. (ν, μ)  prog_sem (adjointFO I σ ν) a  (μ, ω)  prog_sem (adjointFO I σ ν) b)"
      using IH1[OF safe1 ssafe] by auto
    ultimately
    show "((ν, ω)  prog_sem I (PsubstFO (a ;; b) σ)) = ((ν, ω)  prog_sem (adjointFO I σ ν) (a ;; b))"
      by auto
  qed
  then show ?case by auto
next
  case (NPadmit_Loop σ a) then 
  have PA:"NPadmit σ a"
    and PUA:"PUadmitFO σ a (BVP (PsubstFO a σ))"
    and IH:"hpsafe a  (i. dsafe (σ i))  (ν ω. ((ν, ω)  prog_sem I (PsubstFO a σ)) = ((ν, ω)  prog_sem (adjointFO I σ ν) a))"
    and hpsafeS:"hpsafe (PsubstFO a σ)"
      by auto
  have "hpsafe (a**)  (i. dsafe (σ i))  (ν ω. ((ν, ω)  prog_sem I (PsubstFO (a**) σ)) = ((ν, ω)  prog_sem (adjointFO I σ ν) (a**)))"
  proof -
    assume "hpsafe (a**)"
    then have hpsafe:"hpsafe a" by (auto dest: hpsafe.cases)
    assume ssafe:"(i. dsafe (σ i))"
    have agree:"ν μ. (ν, μ)  prog_sem I (PsubstFO a σ)  Vagree ν μ (-BVP(PsubstFO a σ))"
      subgoal for ν μ
        using bound_effect[OF good_interp, of "(PsubstFO a σ)" ν, OF hpsafeS] 
        by auto
      done
    have sem_eq:"ν μ ω. (ν, μ)  prog_sem I (PsubstFO a σ)  
        ((μ, ω)  prog_sem (adjointFO I σ ν) a) =
        ((μ, ω)  prog_sem (adjointFO I σ μ) a)"
      subgoal for ν μ ω 
        proof -
          assume assm:"(ν, μ)  prog_sem I (PsubstFO a σ)"
          show "((μ, ω)  prog_sem (adjointFO I σ ν) a) = ((μ, ω)  prog_sem (adjointFO I σ μ) a)"
            using uadmit_prog_ntadjoint[OF PUA agree[OF assm] ssafe hpsafe  good_interp] by auto
        qed
      done 
    fix ν ω
    have UN_rule:" a S S'. (n b. (a,b)  S n  (a,b)  S' n)  (b. (a,b)  (n. S n)  (a,b)  (n. S' n))"
      by auto
    have eqL:"((ν, ω)  prog_sem I (PsubstFO (a**) σ)) = ((ν, ω)  (n. (prog_sem I (PsubstFO a σ)) ^^ n))"
      using rtrancl_is_UN_relpow by auto
    moreover have eachEq:"n. ((ν ω. ((ν, ω)  (prog_sem I (PsubstFO a σ)) ^^ n) = ((ν, ω)  (prog_sem (adjointFO I σ ν) a)^^ n)))"
    proof -
      fix n
      show "((ν ω. ((ν, ω)  (prog_sem I (PsubstFO a σ)) ^^ n) = ((ν, ω)  (prog_sem (adjointFO I σ ν) a)^^ n)))"
      proof (induct n)
        case 0
        then show ?case by auto
      next
        case (Suc n) then
        have IH2:"ν ω. ((ν, ω)  prog_sem I (PsubstFO a σ) ^^ n) = ((ν, ω)  prog_sem (adjointFO I σ ν) a ^^ n)"
          by auto
        have relpow:"R n. R ^^ Suc n = R O R ^^ n"
          using relpow.simps(2) relpow_commute by metis
        show ?case 
          apply (simp only: relpow[of n "prog_sem I (PsubstFO a σ)"] relpow[of n "prog_sem (adjointFO I σ ν) a"])
          apply(unfold relcomp_unfold)
          apply auto
           subgoal for ab b
             apply(rule exI[where x=ab])
             apply(rule exI[where x=b])
             using IH2 IH[OF hpsafe ssafe] sem_eq[of ν "(ab,b)" ω] apply auto
              using uadmit_prog_ntadjoint[OF PUA agree ssafe hpsafe good_interp] IH[OF hpsafe ssafe]
              apply (metis (no_types, lifting)) 
             using uadmit_prog_ntadjoint[OF PUA agree ssafe hpsafe good_interp] IH[OF hpsafe ssafe]
             apply (metis (no_types, lifting)) 
           done
          subgoal for ab b
            apply(rule exI[where x=ab])
            apply(rule exI[where x=b])
            using IH2 IH[OF hpsafe ssafe] sem_eq[of ν "(ab,b)" ω] apply auto
             using uadmit_prog_ntadjoint[OF PUA agree ssafe hpsafe good_interp] IH[OF hpsafe ssafe]
             apply (metis (no_types, lifting))
            using uadmit_prog_ntadjoint[OF PUA agree ssafe hpsafe good_interp] IH[OF hpsafe ssafe]
            apply (metis (no_types, lifting))
          done
        done
      qed
      qed
    moreover have "((ν, ω)  (n. (prog_sem I (PsubstFO a σ)) ^^ n)) = ((ν, ω)  ( n.(prog_sem (adjointFO I σ ν) a)^^ n))"
      apply(rule UN_rule)
      using eachEq by auto
    moreover have eqR:"((ν, ω)  prog_sem (adjointFO I σ ν) (a**)) = ((ν, ω)  (n. (prog_sem (adjointFO I σ ν) a) ^^ n))"
       using rtrancl_is_UN_relpow by auto
    ultimately show "((ν, ω)  prog_sem I (PsubstFO (a**) σ)) = ((ν, ω)  prog_sem (adjointFO I σ ν) (a**))"
      by auto
  qed
  then show ?case by auto
next
  case (NFadmit_Exists σ φ x)
  then have IH:"fsafe φ  (i. dsafe (σ i))  (ν. (ν  fml_sem I (FsubstFO φ σ)) = (ν  fml_sem (adjointFO I σ ν) φ))"
    and FUA:"FUadmitFO σ φ {Inl x}"
    by blast+
  have fsafe:"fsafe (Exists x φ)  fsafe φ"
    by (auto dest: fsafe.cases)
  have eq:"fsafe (Exists x φ)  (i. dsafe (σ i))  (ν. (ν  fml_sem I (FsubstFO (Exists x φ) σ)) = (ν  fml_sem (adjointFO I σ ν)  (Exists x φ)))"
  proof -
    assume fsafe:"fsafe (Exists x φ)"
    from fsafe have fsafe':"fsafe φ" by (auto dest: fsafe.cases)
    assume ssafe:"(i. dsafe (σ i))"
    fix ν
    have agree:"r. Vagree ν (repv ν x r) (- {Inl x})"
      unfolding Vagree_def by auto
    have sem_eq:"r. ((repv ν x r)  fml_sem (adjointFO I σ (repv ν x r)) φ) =
                      ((repv ν x r)  fml_sem (adjointFO I σ ν) φ)"
      using uadmit_fml_ntadjoint[OF FUA agree ssafe fsafe' good_interp] by auto
    have "(ν  fml_sem I (FsubstFO  (Exists x φ) σ)) = (r. (repv ν x r)  fml_sem I (FsubstFO φ σ))"
      by auto
    moreover have "... = (r. (repv ν x r)  fml_sem (adjointFO I σ (repv ν x r)) φ)"
      using IH[OF fsafe' ssafe] by auto
    moreover have "... = (r. (repv ν x r)  fml_sem (adjointFO I σ ν) φ)"
      using sem_eq by auto
    moreover have "... = (ν  fml_sem (adjointFO I σ ν) (Exists x φ))"
      by auto
    ultimately show "(ν  fml_sem I (FsubstFO  (Exists x φ) σ)) = (ν  fml_sem (adjointFO I σ ν) (Exists x φ))"
      by auto
  qed
  then show ?case by auto
next
  case (NFadmit_Diamond σ φ a) then 
  have PA:"NPadmit σ a" 
    and FUA:"FUadmitFO σ φ (BVP (PsubstFO a σ))"
    and IH1:"fsafe φ  (i. dsafe (σ i))  (ν. (ν  fml_sem I (FsubstFO φ σ)) = (ν  fml_sem (adjointFO I σ ν) φ))"
    and IH2:"hpsafe a  (i. dsafe (σ i))  (ν ω. ((ν, ω)  prog_sem I (PsubstFO a σ)) = ((ν, ω)  prog_sem (adjointFO I σ ν) a))"
    and hpsafeF:"hpsafe (PsubstFO a σ)"
      by auto
  have "fsafe ( a  φ)  (i. dsafe (σ i))  (ν. (ν  fml_sem I (FsubstFO ( a  φ) σ)) = (ν  fml_sem (adjointFO I σ ν) ( a  φ)))"
  proof -
    assume fsafe:"fsafe ( a  φ)"
    assume ssafe:"(i. dsafe (σ i))"
    from fsafe have fsafe':"fsafe φ" and hpsafe:"hpsafe a" by (auto dest: fsafe.cases)
    fix ν
    have agree:"ω. (ν, ω)  prog_sem I (PsubstFO a σ)  Vagree ν ω (-BVP(PsubstFO a σ))"
      using bound_effect[OF good_interp, of "(PsubstFO a σ)" ν, OF hpsafeF] by auto
    have sem_eq:"ω. (ν, ω)  prog_sem I (PsubstFO a σ)  
        (ω  fml_sem (adjointFO I σ ν) φ) =
        (ω  fml_sem (adjointFO I σ ω) φ)"
      using uadmit_fml_ntadjoint [OF FUA agree ssafe fsafe' good_interp] by auto
    have "(ν  fml_sem I (FsubstFO ( a  φ) σ)) = ( ω. (ν, ω)  prog_sem I (PsubstFO a σ)  ω  fml_sem I (FsubstFO φ σ))"
      by auto
    moreover have "... = ( ω. (ν, ω)  prog_sem (adjointFO I σ ν) a  ω  fml_sem (adjointFO I σ ω) φ)"
      using IH1[OF fsafe' ssafe] IH2[OF hpsafe ssafe, of ν] by auto
    moreover have "... = ( ω. (ν, ω)  prog_sem (adjointFO I σ ν) a  ω  fml_sem (adjointFO I σ ν) φ)"
      using sem_eq IH2 hpsafe ssafe by blast
    moreover have "... = (ν  fml_sem (adjointFO I σ ν) ( a  φ))"
      by auto
    ultimately show "?thesis ν" by auto
  qed
  then show ?case by auto
next
  case (NFadmit_Context σ φ C) then
  have FA:"NFadmit σ φ"
    and FUA:"FUadmitFO σ φ UNIV"
    and IH:"fsafe φ  (i. dsafe (σ i))  (ν. (ν  fml_sem I (FsubstFO φ σ)) = (ν  fml_sem (adjointFO I σ ν) φ))"
      by auto
  have "fsafe (InContext C φ) 
           (i. dsafe (σ i)) (ν. (ν  fml_sem I (FsubstFO (InContext C φ) σ)) = (ν  fml_sem (adjointFO I σ ν) (InContext C φ)))"
  proof -
    assume safe:"fsafe (InContext C φ)"
    then have fsafe:"fsafe φ" by (auto dest: fsafe.cases)
    assume ssafe:"i. dsafe (σ i)"
    fix ν
    have Ieq:" Contexts (adjointFO I σ ν) C = Contexts I C"
      unfolding adjointFO_def by auto
    have IH':"ν. (ν  fml_sem I (FsubstFO φ σ)) = (ν  fml_sem (adjointFO I σ ν) φ)"
      using IH[OF fsafe ssafe] by auto
    have agree:"ω. Vagree ν ω (-UNIV)" unfolding Vagree_def by auto
    have adj_eq:"ω. fml_sem (adjointFO I σ ν) φ = fml_sem (adjointFO I σ ω) φ"
      using uadmit_fml_ntadjoint[OF FUA agree ssafe fsafe good_interp] by auto
    then have sem:"fml_sem I (FsubstFO φ σ) =  fml_sem (adjointFO I σ ν) φ"
      using IH' agree adj_eq by auto
    show "?thesis ν"  using Ieq sem by auto
  qed
  then show ?case by auto
qed (auto)

lemma nsubst_fml:
  fixes I::"('sf, 'sc, 'sz) interp"
  fixes ν::"'sz state"
  assumes good_interp:"is_interp I"
  assumes NFA:"NFadmit σ φ"
  assumes fsafe:"fsafe φ"
  assumes frees:"(i. dsafe (σ i))"
  shows "(ν  fml_sem I (FsubstFO φ σ)) = (ν  fml_sem (adjointFO I σ ν) φ)"
  using good_interp NFA fsafe frees 
  by (auto simp add: nsubst_hp_fml)

lemma nsubst_hp:
  fixes I::"('sf, 'sc, 'sz) interp"
  fixes ν::"'sz state"
  assumes good_interp:"is_interp I"    
  assumes NPA:"NPadmit σ α"
  assumes hpsafe:"hpsafe α"
  assumes frees:"i. dsafe (σ i)"
  shows "((ν, ω)  prog_sem I (PsubstFO α σ)) = ((ν, ω)   prog_sem (adjointFO I σ ν) α)"
 using good_interp NPA hpsafe frees nsubst_hp_fml by blast

lemma psubst_sterm:
  fixes I::"('sf, 'sc, 'sz) interp"
  assumes good_interp:"is_interp I"    
  shows "(sterm_sem I θ = sterm_sem (PFadjoint I σ) θ)"
proof (induction θ)
qed (auto simp add: PFadjoint_def)

lemma psubst_dterm:
  fixes I::"('sf, 'sc, 'sz) interp"
  assumes good_interp:"is_interp I"    
  shows "(dsafe θ  dterm_sem I θ = dterm_sem (PFadjoint I σ) θ)"
proof (induction θ)
  case (Differential θ)
  assume safe:"dsafe (Differential θ)"
  from safe have free:"dfree θ" by auto
  assume sem:"dsafe θ  dterm_sem I θ = dterm_sem (PFadjoint I σ) θ"
  have "ν. frechet I θ (fst ν) (snd ν) = frechet (PFadjoint I σ) θ (fst ν) (snd ν)"
    apply(rule sterm_determines_frechet)
        using good_interp free apply auto
     subgoal unfolding is_interp_def PFadjoint_def by auto
    using psubst_sterm[of I θ] by auto
  then show "?case"
    by (auto simp add: directional_derivative_def)
 qed (auto simp add: PFadjoint_def)
    
lemma psubst_ode:
assumes good_interp:"is_interp I"
shows "ODE_sem I ODE = ODE_sem (PFadjoint I σ) ODE"
proof (induction "ODE")
  case (OVar x)
  then show ?case unfolding PFadjoint_def by auto
next
  case (OSing x1a x2)
  then show ?case apply auto apply (rule ext) apply (rule vec_extensionality) using psubst_sterm[OF good_interp, of x2 σ]  by auto 
next
  case (OProd ODE1 ODE2)
  then show ?case by auto
qed
  
lemma psubst_fml:
fixes I::"('sf, 'sc, 'sz) interp"
assumes good_interp:"is_interp I"    
shows "(PPadmit σ α   hpsafe α  (i. fsafe (σ i))  ( ν ω. (ν,ω)  prog_sem I (PPsubst α σ) = ((ν,ω)  prog_sem (PFadjoint I σ) α)))  
  (PFadmit σ φ  fsafe φ  (i. fsafe (σ i))  ( ν. ν  fml_sem I (PFsubst φ σ) = (ν  fml_sem (PFadjoint I σ) φ)))"
proof (induction rule: PPadmit_PFadmit.induct)
  case (PPadmit_ODE σ φ ODE)
  assume PF:"PFadmit σ φ"
  assume PFU:"PFUadmit σ φ (BVO ODE)"
  assume IH:"fsafe φ  (i. fsafe (σ i))  (ν. (ν  fml_sem I (PFsubst φ σ)) = (ν  fml_sem (PFadjoint I σ) φ))"
  have "hpsafe (EvolveODE ODE φ) 
  (i. fsafe (σ i))  (ν ω. ((ν, ω)  prog_sem I (PPsubst (EvolveODE ODE φ) σ)) = ((ν, ω)  prog_sem (PFadjoint I σ) (EvolveODE ODE φ)))"
  proof -
    assume safe:"hpsafe (EvolveODE ODE φ)"
    from safe have fsafe:"fsafe φ" by auto
    assume ssafe:"(i. fsafe (σ i))"
    have fml_eq:"ν. (ν  fml_sem I (PFsubst φ σ)) = (ν  fml_sem (PFadjoint I σ) φ)"
      using IH ssafe fsafe by auto
    fix ν ω
    show "((ν, ω)  prog_sem I (PPsubst (EvolveODE ODE φ) σ)) = ((ν, ω)  prog_sem (PFadjoint I σ) (EvolveODE ODE φ))"
      apply auto
    proof -
      fix b sol t
      assume eq1:"ν = (sol 0, b)"
        and eq2:"ω = mk_v I ODE (sol 0, b) (sol t)"
        and t:"0  t"
        and sol:"(sol solves_ode (λa. ODE_sem I ODE)) {0..t} {x. mk_v I ODE (sol 0, b) x  fml_sem I (PFsubst φ σ)}"
      have var:"ODE_vars I ODE =  ODE_vars (PFadjoint I σ) ODE"
        by(induction ODE, auto simp add: PFadjoint_def)
      have mkv_eq:"s. s  {0..t}  mk_v I ODE (sol 0, b) (sol s) = mk_v (PFadjoint I σ) ODE (sol 0, b) (sol s)"
        apply(rule agree_UNIV_eq)
        unfolding Vagree_def apply auto
         subgoal for s i
           using mk_v_agree[of I ODE "(sol 0, b)" "sol s"] mk_v_agree[of "PFadjoint I σ" ODE "(sol 0, b)" "sol s"]
           unfolding Vagree_def var 
           apply (cases "Inl i  Inl ` ODE_vars I ODE", auto simp add: var)
            by force
        subgoal for s i
          using mk_v_agree[of I ODE "(sol 0, b)" "sol s"] mk_v_agree[of "PFadjoint I σ" ODE "(sol 0, b)" "sol s"]
          unfolding Vagree_def var 
          apply (cases "Inr i  Inr ` ODE_vars I ODE", auto simp add: var psubst_ode)
           using psubst_ode[OF good_interp, of ODE σ] apply auto
          using psubst_ode[OF good_interp, of ODE σ] by force
        done
      have sol':"(sol solves_ode (λ_. ODE_sem (PFadjoint I σ) ODE)) {0..t}
       {x. mk_v I ODE (sol 0, b) x  fml_sem I (PFsubst φ σ)}"
        apply (rule solves_ode_congI)
            apply (rule sol)
           subgoal for ta by auto
          subgoal for ta using psubst_ode[OF good_interp, of ODE σ] by auto
         subgoal by (rule refl)
        subgoal by (rule refl)
        done
      have sub:"s. s  {0..t} 
               sol s  {x. (mk_v (PFadjoint I σ ) ODE (sol 0, b) x  fml_sem (PFadjoint I σ ) φ)}"
        subgoal for s
          using solves_ode_domainD[OF sol, of s] mkv_eq[of s] fml_eq[of "mk_v (PFadjoint I σ ) ODE (sol 0, b) (sol s)"]
          by auto
        done
      have sol'':"(sol solves_ode (λc. ODE_sem (PFadjoint I σ ) ODE)) {0..t}
        {x. mk_v (PFadjoint I σ) ODE (sol 0, b) x  fml_sem (PFadjoint I σ ) φ}"
        apply (rule solves_odeI)
         subgoal using sol' solves_ode_vderivD by blast
        using sub by auto          
      show"sola. sol 0 = sola 0 
          (ta. mk_v I ODE (sol 0, b) (sol t) = mk_v (PFadjoint I σ) ODE (sola 0, b) (sola ta) 
                0  ta 
                (sola solves_ode (λa. ODE_sem (PFadjoint I σ) ODE)) {0..ta}
               {x. mk_v (PFadjoint I σ) ODE (sola 0, b) x  fml_sem (PFadjoint I σ) φ})"
        apply(rule exI[where x=sol])
        apply(rule conjI)
         apply(rule refl)
        apply(rule exI[where x=t])
        apply(rule conjI)
         subgoal using mkv_eq t by auto
        apply(rule conjI)
         apply(rule t)
        apply(rule sol'') 
        done
    next
      fix b sol t
      assume eq1:"ν = (sol 0, b)"
        and eq2:"ω = mk_v (PFadjoint I σ) ODE (sol 0, b) (sol t)"
        and t:"0  t"
        and sol:"(sol solves_ode (λa. ODE_sem (PFadjoint I σ) ODE)) {0..t} {x. mk_v (PFadjoint I σ) ODE (sol 0, b) x  fml_sem (PFadjoint I σ) φ}"
      have var:"ODE_vars I ODE =  ODE_vars (PFadjoint I σ) ODE"
        by(induction ODE, auto simp add: PFadjoint_def)
      have mkv_eq:"s. s  {0..t}  mk_v I ODE (sol 0, b) (sol s) = mk_v (PFadjoint I σ) ODE (sol 0, b) (sol s)"
        apply(rule agree_UNIV_eq)
        unfolding Vagree_def apply auto
         subgoal for s i
           using mk_v_agree[of I ODE "(sol 0, b)" "sol s"] mk_v_agree[of "PFadjoint I σ" ODE "(sol 0, b)" "sol s"]
           unfolding Vagree_def var 
           apply (cases "Inl i  Inl ` ODE_vars I ODE", auto simp add: var)
            by force
        subgoal for s i
          using mk_v_agree[of I ODE "(sol 0, b)" "sol s"] mk_v_agree[of "PFadjoint I σ" ODE "(sol 0, b)" "sol s"]
          unfolding Vagree_def var 
          apply (cases "Inr i  Inr ` ODE_vars I ODE", auto simp add: var psubst_ode)
           using psubst_ode[OF good_interp, of ODE σ] apply auto
          using psubst_ode[OF good_interp, of ODE σ] by force
        done
      have sol':"(sol solves_ode (λ_. ODE_sem I ODE)) {0..t}
         {x. mk_v (PFadjoint I σ) ODE (sol 0, b) x  fml_sem (PFadjoint I σ) φ}"
        apply (rule solves_ode_congI)
            apply (rule sol)
           subgoal for ta by auto
          subgoal for ta using psubst_ode[OF good_interp, of ODE σ] by auto
         subgoal by (rule refl)
        subgoal by (rule refl)
        done
      have sub:"s. s  {0..t} 
               sol s  {x. (mk_v  I ODE (sol 0, b) x  fml_sem I (PFsubst φ σ))}"
        subgoal for s
          using solves_ode_domainD[OF sol, of s] mkv_eq[of s] fml_eq[of "mk_v (PFadjoint I σ ) ODE (sol 0, b) (sol s)"]
          by auto
        done
      have sol'':"(sol solves_ode (λc. ODE_sem I ODE)) {0..t}
        {x. mk_v I ODE (sol 0, b) x  fml_sem I (PFsubst φ σ)}"
        apply (rule solves_odeI)
         subgoal using sol' solves_ode_vderivD by blast
        using sub by auto
      show "sola. sol 0 = sola 0 
          (ta. mk_v (PFadjoint I σ) ODE (sol 0, b) (sol t) = mk_v I ODE (sola 0, b) (sola ta) 
                0  ta  (sola solves_ode (λa. ODE_sem I ODE)) {0..ta} {x. mk_v I ODE (sola 0, b) x  fml_sem I (PFsubst φ σ)})"
        apply(rule exI[where x=sol])
        by (metis dual_order.refl intervalE mkv_eq sol'' t)
    qed
  qed
  then show ?case
    by auto
next
  case (PPadmit_Assign σ x θ)
  have "hpsafe (x := θ)  (i. fsafe (σ i))  ( ν ω. ((ν, ω)  prog_sem I (PPsubst (x := θ) σ)) = ((ν, ω)  prog_sem (PFadjoint I σ) (x := θ)))"
  proof -
    assume safe:"hpsafe (x := θ)"
    then have dsafe:"dsafe θ" by auto
    assume safes:"(i. fsafe (σ i))"
    show "?thesis"
      using psubst_dterm[OF good_interp dsafe, of σ] by auto
  qed
  then show "?case" by auto 
next
  case (PPadmit_DiffAssign σ x θ)
  have "hpsafe (DiffAssign x θ)  (i. fsafe (σ i))  ( ν ω. ((ν, ω)  prog_sem I (PPsubst (DiffAssign x θ) σ)) = (((ν, ω)  prog_sem (PFadjoint I σ) (DiffAssign x θ))))"
  proof -
    assume safe:"hpsafe (DiffAssign x θ)"
    then have dsafe:"dsafe θ" by auto
    assume safes:"(i. fsafe (σ i))"
    show "?thesis"
      using psubst_dterm[OF good_interp dsafe, of σ] by auto
   qed
  then show ?case by auto
next
  case (PFadmit_Geq σ θ1 θ2) then 
  have "fsafe (Geq θ1 θ2)  (i. fsafe (σ i))  ( ν. (ν  fml_sem I (PFsubst (Geq θ1 θ2) σ)) = (ν  fml_sem (PFadjoint I σ) (Geq θ1 θ2)))"
  proof -
    assume safe:"fsafe (Geq θ1 θ2)"
    then have safe1:"dsafe θ1" 
      and safe2:"dsafe θ2" by auto
    assume safes:"(i. fsafe (σ i))"
    show "?thesis"
      using psubst_dterm[OF good_interp safe1, of σ] psubst_dterm[OF good_interp safe2, of σ] by  auto
  qed
  then show ?case by auto
next
  case (PFadmit_Prop σ p args) then
  have "fsafe (Prop p args)  (i. fsafe (σ i))  (ν.(ν  fml_sem I (PFsubst ( p args) σ)) = (ν  fml_sem (PFadjoint I σ) ( p args)))"
  proof -
    assume safe:"fsafe (Prop p args)" and ssafe:" (i. fsafe (σ i))"
    fix ν
    from safe have safes:"i. dsafe (args i)" using dfree_is_dsafe by auto
    have Ieq:"Predicates I p = Predicates (PFadjoint I σ) p"
      unfolding PFadjoint_def by auto
    have vec:"(χ i. dterm_sem I (args i) ν) = (χ i. dterm_sem (PFadjoint I σ) (args i) ν)"
      apply(auto simp add: vec_eq_iff)
      subgoal for i using safes[of i] 
        by (metis good_interp psubst_dterm)
      done
    show "?thesis ν" using  Ieq vec by auto
  qed
  then show "?case" by auto
next
  case (PPadmit_Sequence σ a b) then 
  have PUA:"PPUadmit σ b (BVP (PPsubst a σ))"
    and PA:"PPadmit σ a"
    and IH1:"hpsafe a  (i. fsafe (σ i))  ( ν ω. ((ν, ω)  prog_sem I (PPsubst a σ)) = ((ν, ω)  prog_sem (PFadjoint I σ) a))"
    and IH2:"hpsafe b  (i. fsafe (σ i))  ( ν ω. ((ν, ω)  prog_sem I (PPsubst b σ)) = ((ν, ω)  prog_sem (PFadjoint I σ) b))"
    and substSafe:"hpsafe (PPsubst a σ)"
    by auto
  have "hpsafe (a ;; b)  (i. fsafe (σ i))  ( ν ω. ((ν, ω)  prog_sem I (PPsubst (a ;; b) σ)) = ((ν, ω)  prog_sem (PFadjoint I σ) (a ;; b)))"
  proof -
    assume hpsafe:"hpsafe (a ;; b)"
    assume ssafe:"(i. fsafe (σ i))"
    from hpsafe have safe1:"hpsafe a" and safe2:"hpsafe b" by (auto dest: hpsafe.cases)
    fix ν ω
    have agree:"μ. (ν, μ)  prog_sem I (PPsubst a σ)  Vagree ν μ (-BVP(PPsubst a σ))"
      subgoal for μ
        using bound_effect[OF good_interp, of "(PPsubst a σ)" ν, OF substSafe] by auto
      done
    have sem_eq:"μ. (ν, μ)  prog_sem I (PPsubst a σ)  
        ((μ, ω)  prog_sem (PFadjoint I σ) b) =
        ((μ, ω)  prog_sem (PFadjoint I σ) b)"
      subgoal for μ
      proof -
        assume assm:"(ν, μ)  prog_sem I (PPsubst a σ)"
        show "((μ, ω)  prog_sem (PFadjoint I σ) b) = ((μ, ω)  prog_sem (PFadjoint I σ) b)"
          using PUA agree[OF assm] safe2 ssafe good_interp by auto
      qed
      done      
    have "((ν, ω)  prog_sem I (PPsubst (a ;; b) σ)) = ( μ. (ν, μ)  prog_sem I (PPsubst a σ)  (μ, ω)  prog_sem I (PPsubst b σ))"
      by auto
    moreover have "... = ( μ. (ν, μ)  prog_sem I (PPsubst a σ)  (μ, ω)  prog_sem (PFadjoint I σ) b)"
      using IH2[OF safe2 ssafe] by blast 
    moreover have "... = ( μ. (ν, μ)  prog_sem (PFadjoint I σ) a  (μ, ω)  prog_sem (PFadjoint I σ) b)"
      using IH1[OF safe1 ssafe] sem_eq by blast
    ultimately
    show "((ν, ω)  prog_sem I (PPsubst (a ;; b) σ)) = ((ν, ω)  prog_sem (PFadjoint I σ) (a ;; b))"
      by auto
  qed
  then show ?case by auto
next
  case (PPadmit_Loop σ a) then 
  have PA:"PPadmit σ a"
  and PUA:"PPUadmit σ a (BVP (PPsubst a σ))"
  and IH:"hpsafe a  (i. fsafe (σ i))  (ν ω. ((ν, ω)  prog_sem I (PPsubst a σ)) = ((ν, ω)  prog_sem (PFadjoint I σ) a))"
  and substSafe:"hpsafe (PPsubst a σ)"   
    by auto
  have "hpsafe (a**)  (i. fsafe (σ i))  (ν ω. ((ν, ω)  prog_sem I (PPsubst (a**) σ)) = ((ν, ω)  prog_sem (PFadjoint I σ) (a**)))"
  proof -
    assume "hpsafe (a**)"
    then have hpsafe:"hpsafe a" by (auto dest: hpsafe.cases)
    assume ssafe:"i. fsafe (σ i)"
    have agree:"ν μ. (ν, μ)  prog_sem I (PPsubst a σ)  Vagree ν μ (-BVP(PPsubst a σ))"
      subgoal for ν μ
        using bound_effect[OF good_interp, of "(PPsubst a σ)" ν, OF substSafe] by auto
      done
    fix ν ω
    have UN_rule:" a S S'. (n b. (a,b)  S n  (a,b)  S' n)  (b. (a,b)  (n. S n)  (a,b)  (n. S' n))"
      by auto
    have eqL:"((ν, ω)  prog_sem I (PPsubst (a**) σ)) = ((ν, ω)  (n. (prog_sem I (PPsubst a σ)) ^^ n))"
      using rtrancl_is_UN_relpow by auto
    moreover have eachEq:"n. ((ν ω. ((ν, ω)  (prog_sem I (PPsubst a σ)) ^^ n) = ((ν, ω)  (prog_sem (PFadjoint I σ) a)^^ n)))"
    proof -
      fix n
      show "((ν ω. ((ν, ω)  (prog_sem I (PPsubst a σ)) ^^ n) = ((ν, ω)  (prog_sem (PFadjoint I σ) a)^^ n)))"
      proof (induct n)
        case 0
        then show ?case by auto
      next
        case (Suc n) then
        have IH2:"ν ω. ((ν, ω)  prog_sem I (PPsubst a σ) ^^ n) = ((ν, ω)  prog_sem (PFadjoint I σ) a ^^ n)"
          by auto
        have relpow:"R n. R ^^ Suc n = R O R ^^ n"
          using relpow.simps(2) relpow_commute by metis
        show ?case 
          apply (simp only: relpow[of n "prog_sem I (PPsubst a σ)"] relpow[of n "prog_sem (PFadjoint I σ) a"])
          apply(unfold relcomp_unfold)
          apply auto
           subgoal for ab b
              apply(rule exI[where x=ab])
              apply(rule exI[where x=b])
              using IH2 IH[OF hpsafe ssafe]  by auto
          subgoal for ab b
            apply(rule exI[where x=ab])
            apply(rule exI[where x=b])
            using IH2 IH[OF hpsafe ssafe] by auto
        done
      qed
    qed
    moreover have "((ν, ω)  (n. (prog_sem I (PPsubst a σ)) ^^ n)) = ((ν, ω)  ( n.(prog_sem (PFadjoint I σ) a)^^ n))"
      apply(rule UN_rule)
      using eachEq by auto
    moreover have eqR:"((ν, ω)  prog_sem (PFadjoint I σ) (a**)) = ((ν, ω)  (n. (prog_sem (PFadjoint I σ) a) ^^ n))"
       using rtrancl_is_UN_relpow by auto
    ultimately show "((ν, ω)  prog_sem I (PPsubst (a**) σ)) = ((ν, ω)  prog_sem (PFadjoint I σ) (a**))"
      by auto
  qed
  then show ?case by auto
next
next
  case (PFadmit_Context σ φ C) then
  have FA:"PFadmit σ φ"
    and FUA:"PFUadmit σ φ UNIV"
    and IH:"fsafe φ  (i. fsafe (σ i))  (ν. (ν  fml_sem I (PFsubst φ σ)) = (ν  fml_sem (PFadjoint I σ) φ))"
    by auto
  have "fsafe (InContext C φ) 
           (i. fsafe (σ i))  (ν. (ν  fml_sem I (PFsubst (InContext C φ) σ)) = (ν  fml_sem (PFadjoint I σ) (InContext C φ)))"
  proof -
    assume safe:"fsafe (InContext C φ)"
    then have fsafe:"fsafe φ" by (auto dest: fsafe.cases)
    assume ssafe:"(i. fsafe (σ i))"
    fix ν :: "(real, 'sz) vec × (real, 'sz) vec"
    have IH':"ν. (ν  fml_sem I (PFsubst φ σ)) = (ν  fml_sem (PFadjoint I σ) φ)"
      using IH[OF fsafe ssafe] by auto
    have agree:"ω. Vagree ν ω (-UNIV)" unfolding Vagree_def by auto
    then have sem:"fml_sem I (PFsubst φ σ) =  fml_sem (PFadjoint I σ) φ"
      using IH' agree  by auto
    show "?thesis ν"  using sem 
      apply auto
      apply(cases C)
        unfolding PFadjoint_def apply auto
      apply(cases C)
       by auto
  qed
  then show ?case by auto
qed (auto simp add: PFadjoint_def)

lemma subst_ode:
  fixes I:: "('sf, 'sc, 'sz) interp" and ν :: "'sz state"
  assumes good_interp:"is_interp I"
  shows "osafe ODE  
         ssafe σ  
         Oadmit σ ODE (BVO ODE) 
         ODE_sem I (Osubst ODE σ) (fst ν) = ODE_sem (adjoint I σ ν) ODE (fst ν)"
proof (induction rule: osafe.induct)
  case (osafe_Var c)
  then show ?case unfolding adjoint_def by (cases "SODEs σ c", auto)
next
  case (osafe_Sing θ x)
  then show ?case 
    using subst_sterm [of  σ θ I "ν"]
    unfolding ssafe_def by auto
next
  case (osafe_Prod ODE1 ODE2) then
  have NOU1:"Oadmit σ ODE1  (BVO (OProd ODE1 ODE2))" and NOU2:"Oadmit σ ODE2  (BVO (OProd ODE1 ODE2))" 
    by auto
  have TUA_sub:"σ θ A B. TUadmit σ θ B  A  B  TUadmit σ θ A"
    unfolding TUadmit_def by auto
  have OA_sub:"ODE A B. Oadmit σ ODE B  A  B  Oadmit σ ODE A"
    subgoal for ODE A B
    proof (induction rule: Oadmit.induct)
      case (Oadmit_Var σ c U)
      then show ?case by auto
    next
      case (Oadmit_Sing σ θ U x)
      then show ?case using TUA_sub[of σ θ U A] by auto
    next
      case (Oadmit_Prod σ ODE1 U ODE2)
      then show ?case by auto
    qed
    done
  have sub1:"(BVO ODE1)  (BVO (OProd ODE1 ODE2))"
    by auto
  have sub2: "(BVO ODE2)  (BVO (OProd ODE1 ODE2))"
    by auto
  have "ODE_sem I (Osubst ODE1 σ) (fst ν) = ODE_sem (adjoint I σ ν) ODE1 (fst ν)"
    "ODE_sem I (Osubst ODE2 σ) (fst ν) = ODE_sem (adjoint I σ ν) ODE2 (fst ν)" using osafe_Prod.IH osafe_Prod.prems osafe_Prod.hyps
    using OA_sub[OF NOU1 sub1] OA_sub[OF NOU2 sub2] by auto
  then show ?case by auto
qed

lemma osubst_eq_ODE_vars: "ODE_vars I (Osubst ODE σ) = ODE_vars (adjoint I σ ν) ODE"
proof (induction ODE)
  case (OVar x)
  then show ?case by (cases "SODEs σ x", auto simp add: adjoint_def)
qed (auto)

lemma subst_semBV:"semBV (adjoint I σ ν') ODE = (semBV I (Osubst ODE σ))"
proof (induction ODE)
  case (OVar x)
  then show ?case by (cases "SODEs σ x", auto simp add: adjoint_def)
qed (auto)

lemma subst_mkv:
  fixes I::"('sf, 'sc, 'sz) interp"
  fixes ν::"'sz state"
  fixes ν'::"'sz state"
  assumes good_interp:"is_interp I"  
  assumes NOU:"Oadmit σ ODE (BVO ODE)"
  assumes osafe:"osafe ODE "
  assumes frees:"ssafe σ"
  shows "(mk_v I (Osubst ODE σ) ν (fst ν')) 
    = (mk_v (adjoint I σ ν') ODE ν (fst ν'))"
  apply(rule agree_UNIV_eq)
  using mk_v_agree[of "adjoint I σ ν'" "ODE" ν "fst ν'"]
  using mk_v_agree[of "I" "Osubst ODE σ" ν "fst ν'"] 
  unfolding Vagree_def 
  using subst_ode[OF good_interp osafe  frees NOU, of ν'] 
  apply auto
   subgoal for i
     apply(erule allE[where x=i])+
     apply(cases "Inl i  Inl ` ODE_vars (adjoint I σ ν') ODE")
      using osubst_eq_ODE_vars[of I ODE σ ν']
      apply force
   proof -
     assume "ODE_sem I (Osubst ODE σ) (fst ν') = ODE_sem (local.adjoint I σ ν') ODE (fst ν')"
       "Inl i  Inl ` ODE_vars (local.adjoint I σ ν') ODE  Inl i  Inr ` ODE_vars (local.adjoint I σ ν') ODE 
       fst (mk_v (local.adjoint I σ ν') ODE ν (fst ν')) $ i = fst ν $ i"
       "Inl i  Inl ` ODE_vars I (Osubst ODE σ)  Inl i  Inr ` ODE_vars I (Osubst ODE σ) 
       fst (mk_v I (Osubst ODE σ) ν (fst ν')) $ i = fst ν $ i"
       "Inl i  Inl ` ODE_vars (local.adjoint I σ ν') ODE"
     then show
        "fst (mk_v I (Osubst ODE σ) ν (fst ν')) $ i = fst (mk_v (local.adjoint I σ ν') ODE ν (fst ν')) $ i"
         using osubst_eq_ODE_vars[of I ODE σ ν'] by force
   qed
  subgoal for i
    apply(erule allE[where x=i])+
    apply(cases "Inr i  Inr ` ODE_vars (adjoint I σ ν') ODE")
     using osubst_eq_ODE_vars[of I ODE σ ν']
     apply force
  proof -
    assume "ODE_sem I (Osubst ODE σ) (fst ν') = ODE_sem (local.adjoint I σ ν') ODE (fst ν')"
      "Inr i  Inl ` ODE_vars (local.adjoint I σ ν') ODE  Inr i  Inr ` ODE_vars (local.adjoint I σ ν') ODE 
      snd (mk_v (local.adjoint I σ ν') ODE ν (fst ν')) $ i = snd ν $ i"
      "Inr i  Inl ` ODE_vars I (Osubst ODE σ)  Inr i  Inr ` ODE_vars I (Osubst ODE σ) 
      snd (mk_v I (Osubst ODE σ) ν (fst ν')) $ i = snd ν $ i"
      "Inr i  Inr ` ODE_vars (local.adjoint I σ ν') ODE"
    then show "snd (mk_v I (Osubst ODE σ) ν (fst ν')) $ i = snd (mk_v (local.adjoint I σ ν') ODE ν (fst ν')) $ i"
      using osubst_eq_ODE_vars[of I ODE σ ν'] by force
  qed
done 
  
lemma subst_fml_hp:
  fixes I::"('sf, 'sc, 'sz) interp"
  assumes good_interp:"is_interp I"
  shows 
  "(Padmit σ α 
    (hpsafe α 
     ssafe σ 
    ( ν ω. ((ν, ω)  prog_sem I (Psubst α σ)) = ((ν, ω)  prog_sem (adjoint I σ ν) α))))
    
    (Fadmit σ φ 
    (fsafe φ 
    ssafe σ 
    ( ν. (ν  fml_sem I (Fsubst φ σ)) = (ν  fml_sem (adjoint I σ ν) φ))))"
proof (induction rule: Padmit_Fadmit.induct)
  case (Padmit_Pvar σ a) then
  have "hpsafe ( a)  ssafe σ  (ν ω. ((ν, ω)  prog_sem I (Psubst ( a) σ)) = ((ν, ω)  prog_sem (local.adjoint I σ ν) ( a)))"
    apply (cases "SPrograms σ a")
     unfolding adjoint_def by auto
  then show ?case by auto
next
  case (Padmit_Sequence σ a b) then 
  have PUA:"PUadmit σ b (BVP (Psubst a σ))"
    and PA:"Padmit σ a"
    and IH1:"hpsafe a  ssafe σ  (ν ω. ((ν, ω)  prog_sem I (Psubst a σ)) = ((ν, ω)  prog_sem (local.adjoint I σ ν) a))"
    and IH2:"hpsafe b  ssafe σ  (ν ω. ((ν, ω)  prog_sem I (Psubst b σ)) = ((ν, ω)  prog_sem (local.adjoint I σ ν) b))"
    and substSafe:"hpsafe (Psubst a σ)"
    by auto
  have "hpsafe (a ;; b)  ssafe σ  (ν ω. ((ν, ω)  prog_sem I (Psubst (a ;; b) σ)) = ((ν, ω)  prog_sem (local.adjoint I σ ν) (a ;; b)))"
  proof -
    assume hpsafe:"hpsafe (a ;; b)"
    assume ssafe:"ssafe σ"
    from hpsafe have safe1:"hpsafe a" and safe2:"hpsafe b" by (auto dest: hpsafe.cases)
    fix ν ω
    have agree:"μ. (ν, μ)  prog_sem I (Psubst a σ)  Vagree ν μ (-BVP(Psubst a σ))"
      subgoal for μ
        using bound_effect[OF good_interp, of "(Psubst a σ)" ν, OF substSafe] by auto
      done
    have sem_eq:"μ. (ν, μ)  prog_sem I (Psubst a σ)  
        ((μ, ω)  prog_sem (local.adjoint I σ ν) b) =
        ((μ, ω)  prog_sem (local.adjoint I σ μ) b)"
      subgoal for μ
      proof -
        assume assm:"(ν, μ)  prog_sem I (Psubst a σ)"
        show "((μ, ω)  prog_sem (local.adjoint I σ ν) b) = ((μ, ω)  prog_sem (local.adjoint I σ μ) b)"
          using uadmit_prog_adjoint[OF PUA agree[OF assm] safe2 ssafe good_interp] by auto
      qed
      done      
    have "((ν, ω)  prog_sem I (Psubst (a ;; b) σ)) = ( μ. (ν, μ)  prog_sem I (Psubst a σ)  (μ, ω)  prog_sem I (Psubst b σ))"
      by auto
    moreover have "... = ( μ. (ν, μ)  prog_sem I (Psubst a σ)  (μ, ω)  prog_sem (adjoint I σ μ) b)"
      using IH2[OF safe2 ssafe] by auto
    moreover have "... = ( μ. (ν, μ)  prog_sem I (Psubst a σ)  (μ, ω)  prog_sem (adjoint I σ ν) b)"
      using sem_eq by auto
    moreover have "... = ( μ. (ν, μ)  prog_sem (adjoint I σ ν) a  (μ, ω)  prog_sem (adjoint I σ ν) b)"
      using IH1[OF safe1 ssafe] by auto
    ultimately
    show "((ν, ω)  prog_sem I (Psubst (a ;; b) σ)) = ((ν, ω)  prog_sem (local.adjoint I σ ν) (a ;; b))"
      by auto
  qed
  then show ?case by auto
next
  case (Padmit_Loop σ a) then 
  have PA:"Padmit σ a"
    and PUA:"PUadmit σ a (BVP (Psubst a σ))"
    and IH:"hpsafe a  ssafe σ  (ν ω. ((ν, ω)  prog_sem I (Psubst a σ)) = ((ν, ω)  prog_sem (local.adjoint I σ ν) a))"
    and substSafe:"hpsafe (Psubst a σ)"
    by auto
  have "hpsafe (a**)  ssafe σ  (ν ω. ((ν, ω)  prog_sem I (Psubst (a**) σ)) = ((ν, ω)  prog_sem (local.adjoint I σ ν) (a**)))"
  proof -
    assume "hpsafe (a**)"
    then have hpsafe:"hpsafe a" by (auto dest: hpsafe.cases)
    assume ssafe:"ssafe σ"
    have agree:"ν μ. (ν, μ)  prog_sem I (Psubst a σ)  Vagree ν μ (-BVP(Psubst a σ))"
    subgoal for ν μ
      using bound_effect[OF good_interp, of "(Psubst a σ)" ν, OF substSafe] by auto
    done
  have sem_eq:"ν μ ω. (ν, μ)  prog_sem I (Psubst a σ)  
      ((μ, ω)  prog_sem (local.adjoint I σ ν) a) =
      ((μ, ω)  prog_sem (local.adjoint I σ μ) a)"
    subgoal for ν μ ω 
    proof -
      assume assm:"(ν, μ)  prog_sem I (Psubst a σ)"
      show "((μ, ω)  prog_sem (local.adjoint I σ ν) a) = ((μ, ω)  prog_sem (local.adjoint I σ μ) a)"
        using uadmit_prog_adjoint[OF PUA agree[OF assm] hpsafe ssafe good_interp] by auto
    qed
    done 
  fix ν ω
  have UN_rule:" a S S'. (n b. (a,b)  S n  (a,b)  S' n)  (b. (a,b)  (n. S n)  (a,b)  (n. S' n))"
    by auto
  have eqL:"((ν, ω)  prog_sem I (Psubst (a**) σ)) = ((ν, ω)  (n. (prog_sem I (Psubst a σ)) ^^ n))"
    using rtrancl_is_UN_relpow by auto
  moreover have eachEq:"n. ((ν ω. ((ν, ω)  (prog_sem I (Psubst a σ)) ^^ n) = ((ν, ω)  (prog_sem (adjoint I σ ν) a)^^ n)))"
  proof -
    fix n
    show "((ν ω. ((ν, ω)  (prog_sem I (Psubst a σ)) ^^ n) = ((ν, ω)  (prog_sem (adjoint I σ ν) a)^^ n)))"
    proof (induct n)
      case 0
      then show ?case by auto
    next
      case (Suc n) then
      have IH2:"ν ω. ((ν, ω)  prog_sem I (Psubst a σ) ^^ n) = ((ν, ω)  prog_sem (local.adjoint I σ ν) a ^^ n)"
        by auto
      have relpow:"R n. R ^^ Suc n = R O R ^^ n"
        using relpow.simps(2) relpow_commute by metis
      show ?case 
        apply (simp only: relpow[of n "prog_sem I (Psubst a σ)"] relpow[of n "prog_sem (adjoint I σ ν) a"])
        apply(unfold relcomp_unfold)
        apply auto
         subgoal for ab b
            apply(rule exI[where x=ab])
            apply(rule exI[where x=b])
            using IH2 IH[OF hpsafe ssafe] sem_eq[of ν "(ab,b)" ω] apply auto
             using uadmit_prog_adjoint[OF PUA agree hpsafe ssafe good_interp] IH[OF hpsafe ssafe]
             apply (metis (no_types, lifting)) 
            using uadmit_prog_adjoint[OF PUA agree hpsafe ssafe good_interp] IH[OF hpsafe ssafe]
            apply (metis (no_types, lifting)) 
          done
        subgoal for ab b
          apply(rule exI[where x=ab])
          apply(rule exI[where x=b])
          using IH2 IH[OF hpsafe ssafe] sem_eq[of ν "(ab,b)" ω] apply auto
           using uadmit_prog_adjoint[OF PUA agree hpsafe ssafe good_interp] IH[OF hpsafe ssafe]
           apply (metis (no_types, lifting))
          using uadmit_prog_adjoint[OF PUA agree hpsafe ssafe good_interp] IH[OF hpsafe ssafe]
          apply (metis (no_types, lifting))
        done
      done
    qed
  qed
  moreover have "((ν, ω)  (n. (prog_sem I (Psubst a σ)) ^^ n)) = ((ν, ω)  ( n.(prog_sem (adjoint I σ ν) a)^^ n))"
    apply(rule UN_rule)
    using eachEq by auto
  moreover have eqR:"((ν, ω)  prog_sem (adjoint I σ ν) (a**)) = ((ν, ω)  (n. (prog_sem (adjoint I σ ν) a) ^^ n))"
     using rtrancl_is_UN_relpow by auto
  ultimately show "((ν, ω)  prog_sem I (Psubst (a**) σ)) = ((ν, ω)  prog_sem (local.adjoint I σ ν) (a**))"
    by auto
   qed
  then show ?case by auto
next
  case (Padmit_ODE σ ODE φ) then
  have OA:"Oadmit σ ODE (BVO ODE)"
    and FA:"Fadmit σ φ"
    and FUA:"FUadmit σ φ (BVO ODE)"
    and IH:"fsafe φ  ssafe σ  (ν. (ν  fml_sem I (Fsubst φ σ)) = (ν  fml_sem (local.adjoint I σ ν) φ))"
      by auto
  have "hpsafe (EvolveODE ODE φ) 
     ssafe σ  (ν ω. ((ν, ω)  prog_sem I (Psubst (EvolveODE ODE φ) σ)) = ((ν, ω)  prog_sem (local.adjoint I σ ν) (EvolveODE ODE φ)))"
  proof (auto)
    fix aa ba bb
      and sol :: "real (real, 'sz) vec" 
      and t :: real
    assume ssafe:"ssafe σ"
    assume osafe:"osafe ODE"
    assume fsafe:"fsafe φ"
    assume t:"0  t"
    assume eq:"(aa,ba) = mk_v I (Osubst ODE σ) (sol 0, bb) (sol t)"
    assume sol:"(sol solves_ode (λa. ODE_sem I (Osubst ODE σ))) {0..t} 
      {x. mk_v I (Osubst ODE σ) (sol 0, bb) x  fml_sem I (Fsubst φ σ)}"
    have silly:"
      t. mk_v I (Osubst ODE σ) (sol 0, bb) (sol t) = mk_v (local.adjoint I σ (sol t, bb)) ODE (sol 0, bb) (sol t)"
      subgoal for t using subst_mkv[OF good_interp OA osafe ssafe, of "(sol 0, bb)" "(sol t, bb)"] by auto done
    have hmmsubst:"s. s  {0..t}  Vagree (sol 0,bb) (sol s, bb) (-(BVO (Osubst ODE σ)))"
      subgoal for s
        apply (rule ODE_bound_effect[of s])
         apply auto[1]
        by (rule sol)
      done
    have sub:"(-(BVO ODE))  (-(BVO (Osubst ODE σ)))"
      by(induction ODE, auto)
    have hmm:"s. s  {0..t}  Vagree (sol 0,bb) (sol s, bb) (-(BVO ODE))"
      subgoal for s
        using agree_sub[OF sub hmmsubst[of s]] by auto
      done
    from hmm have hmm':"s. s  {0..t}  VSagree (sol 0) (sol s) {x. Inl x  (-(BVO ODE))}"
      unfolding VSagree_def Vagree_def by auto
    note hmmm = hmmsubst
    from hmmm have hmmm':"s. s  {0..t}  VSagree (sol 0) (sol s) {x. Inl x  (-(BVO (Osubst ODE σ)))}"
      unfolding VSagree_def Vagree_def by auto
    have Vagree_of_VSagree:"ν1 ν2 ω1 ω2 S. VSagree ν1 ν2 {x. Inl x  S}  VSagree ω1 ω2 {x. Inr x  S}  Vagree (ν1, ω1) (ν2, ω2) S"
      unfolding VSagree_def Vagree_def by auto
    have mkv:"s. s  {0..t}  mk_v I (Osubst ODE σ) (sol 0, bb) (sol s) = mk_v (adjoint I σ (sol s, bb)) ODE (sol 0, bb) (sol s)"
      subgoal for s by (rule silly[of s])
      done
    have lem:"ODE. Oadmit σ ODE (BVO ODE)  (i{i |i. Inl i  SIGO ODE}. case SFunctions σ i of None  {} | Some x  FVT x)  (-(BVO ODE))"
      subgoal for ODE
        apply(induction rule: Oadmit.induct)
          apply auto
        subgoal for σ θ U x xa
          apply (cases "SFunctions σ xa")
           apply auto
          unfolding TUadmit_def
        proof -
          fix a
          assume un:"(iSIGT θ. case SFunctions σ i of None  {} | Some x  FVT x)  U = {}"
          assume sig:"xa  SIGT θ"
          assume some:"SFunctions σ xa = Some a"
          assume fvt:"x  FVT a"
          assume xU:"x  U"
          from un sig have "(case SFunctions σ xa of None  {} | Some x  FVT x)  U = {}"
            by auto 
          then have "(FVT a)  U = {}"
           using some by auto
          then show "False" using fvt xU by auto
        qed
        done
      done
    have FVT_sub:"(i{i |i. Inl i  SIGO ODE}. case SFunctions σ i of None  {} | Some x  FVT x)  (-(BVO ODE))"
      using lem[OF OA] by auto
    have agrees: "s. s  {0..t}  Vagree (sol 0,bb) (sol s, bb) (i{i |i. Inl i  SIGO ODE}. case SFunctions σ i of None  {} | Some x  FVT x)"
       subgoal for s using agree_sub[OF FVT_sub hmm[of s]] by auto done
    have "s. s  {0..t}  mk_v (adjoint I σ (sol 0, bb)) ODE = mk_v (adjoint I σ (sol s, bb)) ODE"
      subgoal for s         
        apply (rule uadmit_mkv_adjoint)
           prefer 3
          subgoal using agrees by auto
         using OA hmm[of s] unfolding  Vagree_def
        using ssafe good_interp osafe by auto
      done
    then have mkva:"s. s  {0..t}  mk_v (adjoint I σ (sol s, bb)) ODE (sol 0, bb) (sol s) = mk_v (adjoint I σ (sol 0, bb)) ODE (sol 0, bb) (sol s)"
      by presburger
    have main_eq:"s. s  {0..t}   mk_v I (Osubst ODE σ) (sol 0, bb) (sol s) = mk_v (adjoint I σ (sol 0, bb)) ODE (sol 0, bb) (sol s) "
      using mkv mkva by auto
    note mkvt = main_eq[of t]
    have fml_eq1:"s. s  {0..t}  
        (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s)  fml_sem I (Fsubst φ σ)) 
      = (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s)  fml_sem (adjoint I σ (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s))) φ)"
      using IH[OF fsafe ssafe] by auto
    have fml_vagree:"s. s  {0..t}  Vagree (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s)) (sol 0, bb) (- semBV I (Osubst ODE σ))"
      subgoal for s
        using mk_v_agree[of I "Osubst ODE σ" "(sol 0,bb)" "sol s"] osubst_eq_ODE_vars[of I ODE σ]
        unfolding Vagree_def
        by auto
      done
    have sembv_eq:"semBV I (Osubst ODE σ) = semBV (adjoint I σ (sol 0, bb)) ODE"
      using subst_semBV by auto
    have fml_vagree':"s. s  {0..t}  Vagree (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s)) (sol 0, bb) (- semBV (adjoint I σ (sol 0,bb)) ODE)"
      using sembv_eq fml_vagree by auto
    have mysub:"-BVO ODE  -(semBV I (Osubst ODE σ))"
      by(induction ODE,auto)
    have fml_vagree:"s. s  {0..t}  Vagree (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s)) (sol 0, bb) (- BVO ODE)"
      subgoal for s using agree_sub[OF mysub fml_vagree[of s]] by auto done
    have fml_sem_eq:"s. s  {0..t}  fml_sem (adjoint I σ (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s))) φ = fml_sem (adjoint I σ (sol 0, bb)) φ"
      apply (rule uadmit_fml_adjoint)
          using FUA fsafe ssafe  good_interp fml_vagree by auto
    have fml_eq2:"s. s  {0..t}  
      ((mk_v I (Osubst ODE σ) (sol 0, bb) (sol s)  fml_sem (adjoint I σ (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s))) φ)
      =(mk_v I (Osubst ODE σ) (sol 0, bb) (sol s)  fml_sem (adjoint I σ (sol 0, bb)) φ))"
      using fml_sem_eq by auto
    have fml_eq3:"s. s  {0..t} 
      (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s)  fml_sem (adjoint I σ (sol 0, bb)) φ) = (mk_v (adjoint I σ (sol 0,bb)) ODE (sol 0, bb) (sol s)  fml_sem (adjoint I σ (sol 0, bb)) φ) "
      using main_eq by auto
    have fml_eq: "s. s  {0..t} 
      (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s)  fml_sem I (Fsubst φ σ)) 
       =  (mk_v (adjoint I σ (sol 0, bb)) ODE (sol 0, bb) (sol s)  fml_sem (adjoint I σ (sol 0, bb)) φ)"
      using fml_eq1 fml_eq2 fml_eq3 by meson
    have sem_eq:"t. ODE_sem I (Osubst ODE σ) (sol t) = ODE_sem (adjoint I σ (sol t, bb)) ODE (sol t)"
      subgoal for t
        using subst_ode[OF good_interp osafe ssafe OA, of "(sol t,bb)"] by auto
      done
    have sem_fact:"s. s  {0..t}  ODE_sem I (Osubst ODE σ) (sol s) = ODE_sem (adjoint I σ (sol 0, bb)) ODE (sol s)"
      subgoal for s
        using subst_ode[OF good_interp osafe ssafe OA, of "(sol s, bb)"]
        uadmit_ode_adjoint'[OF ssafe good_interp agrees[of s] osafe] 
        by auto
      done
    have sol':"(sol solves_ode (λ_. ODE_sem (adjoint I σ (sol 0, bb)) ODE)) {0..t}
       {x. mk_v I (Osubst ODE σ) (sol 0, bb) x  fml_sem I (Fsubst φ σ)}"
      apply (rule solves_ode_congI)
          apply (rule sol)
         subgoal for ta by auto
        subgoal for ta by (rule sem_fact[of ta])
       subgoal by (rule refl)
      subgoal by (rule refl)
      done
    have sub:"s. s  {0..t} 
             sol s  {x. (mk_v (adjoint I σ (sol 0,bb)) ODE (sol 0, bb) x  fml_sem (adjoint I σ (sol 0, bb)) φ)}"
      using fml_eq rangeI t sol solves_ode_domainD by fastforce
    have sol'':"(sol solves_ode (λc. ODE_sem (adjoint I σ (sol 0, bb)) ODE)) {0..t}
{x. mk_v (adjoint I σ (sol 0, bb)) ODE (sol 0, bb) x  fml_sem (adjoint I σ (sol 0, bb)) φ}"
      apply (rule solves_odeI)
       subgoal using sol' solves_ode_vderivD by blast
      using sub by auto
    show "sola. sol 0 = sola 0 
      (ta. mk_v I (Osubst ODE σ) (sol 0, bb) (sol t) = mk_v (local.adjoint I σ (sol 0, bb)) ODE (sola 0, bb) (sola ta) 
            0  ta 
            (sola solves_ode (λa. ODE_sem (local.adjoint I σ (sol 0, bb)) ODE)) {0..ta}
             {x. mk_v (local.adjoint I σ (sol 0, bb)) ODE (sola 0, bb) x  fml_sem (local.adjoint I σ (sol 0, bb)) φ})"
    apply(rule exI[where x=sol])
    apply(rule conjI)
     subgoal by (rule refl)
    apply(rule exI[where x=t])
    apply(rule conjI)
     subgoal using  mkvt t by auto
    apply(rule conjI)
     subgoal by (rule t)
    subgoal by (rule sol'') 
    done
  next
    fix aa ba bb 
      and sol::"real  (real, 'sz) vec" 
      and t::real
    assume ssafe:"ssafe σ"
    assume osafe:"osafe ODE"
    assume fsafe:"fsafe φ"
      
    assume eq:"(aa,ba) = mk_v (adjoint I σ (sol 0, bb)) ODE (sol 0, bb) (sol t)"
    assume t:"0  t"
    assume sol:"(sol solves_ode (λa. ODE_sem (adjoint I σ (sol 0, bb)) ODE)) {0..t}
    {x. mk_v (adjoint I σ (sol 0, bb)) ODE (sol 0, bb) x  fml_sem (adjoint I σ (sol 0, bb)) φ}"
    have silly:"
      t. mk_v I (Osubst ODE σ) (sol 0, bb) (sol t) = mk_v (local.adjoint I σ (sol t, bb)) ODE (sol 0, bb) (sol t)"
      subgoal for t using subst_mkv[OF good_interp OA osafe ssafe, of "(sol 0, bb)" "(sol t, bb)"] by auto done
    have hmm:"s. s  {0..t}  Vagree (sol 0,bb) (sol s, bb) (-(BVO ODE))"
      subgoal for s
        apply (rule ODE_bound_effect[of s])
         apply auto[1]
        by (rule sol)
      done
    from hmm have hmm':"s. s  {0..t}  VSagree (sol 0) (sol s) {x. Inl x  (-(BVO ODE))}"
      unfolding VSagree_def Vagree_def by auto
    have Vagree_of_VSagree:"ν1 ν2 ω1 ω2 S. VSagree ν1 ν2 {x. Inl x  S}  VSagree ω1 ω2 {x. Inr x  S}  Vagree (ν1, ω1) (ν2, ω2) S"
      unfolding VSagree_def Vagree_def by auto
    have mkv:"s. s  {0..t}  mk_v I (Osubst ODE σ) (sol 0, bb) (sol s) = mk_v (adjoint I σ (sol s, bb)) ODE (sol 0, bb) (sol s)"
      subgoal for s by (rule silly[of s])
      done
    have lem:"ODE. Oadmit σ ODE (BVO ODE)  (i{i |i. Inl i  SIGO ODE}. case SFunctions σ i of None  {} | Some x  FVT x)  (-(BVO ODE))"
      subgoal for ODE
        apply(induction rule: Oadmit.induct)
        apply auto
        subgoal for σ θ U x xa
        apply (cases "SFunctions σ xa")
         apply auto
        unfolding TUadmit_def
     proof -
       fix a
       assume un:"(iSIGT θ. case SFunctions σ i of None  {} | Some x  FVT x)  U = {}"
       assume sig:"xa  SIGT θ"
       assume some:"SFunctions σ xa = Some a"
       assume fvt:"x  FVT a"
       assume xU:"x  U"
       from un sig have "(case SFunctions σ xa of None  {} | Some x  FVT x)  U = {}"
         by auto 
       then have "(FVT a)  U = {}"
        using some by auto
       then show "False" using fvt xU by auto
     qed
       done
     done
    have FVT_sub:"(i{i |i. Inl i  SIGO ODE}. case SFunctions σ i of None  {} | Some x  FVT x)  (-(BVO ODE))"
      using lem[OF OA] by auto
    have agrees: "s. s  {0..t}  Vagree (sol 0,bb) (sol s, bb) (i{i |i. Inl i  SIGO ODE}. case SFunctions σ i of None  {} | Some x  FVT x)"
       subgoal for s using agree_sub[OF FVT_sub hmm[of s]] by auto done
    have "s. s  {0..t}  mk_v (adjoint I σ (sol 0, bb)) ODE = mk_v (adjoint I σ (sol s, bb)) ODE"
      subgoal for s         
        apply (rule uadmit_mkv_adjoint)
           prefer 3
          subgoal using agrees by auto
         using OA hmm[of s] unfolding  Vagree_def
        using ssafe good_interp osafe by auto
      done
    then have mkva:"s. s  {0..t}  mk_v (adjoint I σ (sol s, bb)) ODE (sol 0, bb) (sol s) = mk_v (adjoint I σ (sol 0, bb)) ODE (sol 0, bb) (sol s)"
      by presburger
    have main_eq:"s. s  {0..t}   mk_v I (Osubst ODE σ) (sol 0, bb) (sol s) = mk_v (adjoint I σ (sol 0, bb)) ODE (sol 0, bb) (sol s) "
      using mkv mkva by auto
    note mkvt = main_eq[of t]
    have fml_eq1:"s. s  {0..t}  
        (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s)  fml_sem I (Fsubst φ σ)) 
      = (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s)  fml_sem (adjoint I σ (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s))) φ)"
      using IH[OF fsafe ssafe] by auto
    have fml_vagree:"s. s  {0..t}  Vagree (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s)) (sol 0, bb) (- semBV I (Osubst ODE σ))"
      subgoal for s
        using mk_v_agree[of I "Osubst ODE σ" "(sol 0,bb)" "sol s"] osubst_eq_ODE_vars[of I ODE σ]
        unfolding Vagree_def
        by auto
      done
    have sembv_eq:"semBV I (Osubst ODE σ) = semBV (adjoint I σ (sol 0, bb)) ODE"
      using subst_semBV by auto
    have fml_vagree':"s. s  {0..t}  Vagree (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s)) (sol 0, bb) (- semBV (adjoint I σ (sol 0,bb)) ODE)"
      using sembv_eq fml_vagree by auto
    have mysub:"-BVO ODE  -(semBV I (Osubst ODE σ))"
      by(induction ODE,auto)
    have fml_vagree:"s. s  {0..t}  Vagree (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s)) (sol 0, bb) (- BVO ODE)"
      subgoal for s using agree_sub[OF mysub fml_vagree[of s]] by auto done
    have fml_sem_eq:"s. s  {0..t}  fml_sem (adjoint I σ (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s))) φ = fml_sem (adjoint I σ (sol 0, bb)) φ"
      apply (rule uadmit_fml_adjoint)
      using FUA fsafe ssafe  good_interp fml_vagree by auto
    have fml_eq2:"s. s  {0..t}  
      ((mk_v I (Osubst ODE σ) (sol 0, bb) (sol s)  fml_sem (adjoint I σ (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s))) φ)
      =(mk_v I (Osubst ODE σ) (sol 0, bb) (sol s)  fml_sem (adjoint I σ (sol 0, bb)) φ))"
      using fml_sem_eq by auto
    have fml_eq3:"s. s  {0..t} 
        (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s)  fml_sem (adjoint I σ (sol 0, bb)) φ) = (mk_v (adjoint I σ (sol 0,bb)) ODE (sol 0, bb) (sol s)  fml_sem (adjoint I σ (sol 0, bb)) φ) "
      using main_eq by auto
    have fml_eq: "s. s  {0..t} 
         (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s)  fml_sem I (Fsubst φ σ)) 
          =  (mk_v (adjoint I σ (sol 0, bb)) ODE (sol 0, bb) (sol s)  fml_sem (adjoint I σ (sol 0, bb)) φ)"
         using fml_eq1 fml_eq2 fml_eq3 by meson
    have sem_eq:"t. ODE_sem I (Osubst ODE σ) (sol t) = ODE_sem (adjoint I σ (sol t, bb)) ODE (sol t)"
      subgoal for t
        using subst_ode[OF good_interp osafe ssafe OA, of "(sol t,bb)"] by auto
      done
    have sem_fact:"s. s  {0..t}  ODE_sem I (Osubst ODE σ) (sol s) = ODE_sem (adjoint I σ (sol 0, bb)) ODE (sol s)"
      subgoal for s
        using subst_ode[OF good_interp osafe ssafe OA, of "(sol s, bb)"]
        uadmit_ode_adjoint'[OF ssafe good_interp agrees[of s] osafe] 
        by auto
      done
    have sub:"s. s  {0..t} 
             sol s  {x. mk_v I (Osubst ODE σ) (sol 0, bb) (sol s)  fml_sem I (Fsubst φ σ)}"
      using fml_eq rangeI t sol solves_ode_domainD by fastforce
    have sol':"(sol solves_ode (λa. ODE_sem I (Osubst ODE σ))) {0..t} {x. mk_v (adjoint I σ (sol 0, bb)) ODE (sol 0, bb) x  fml_sem (adjoint I σ (sol 0, bb)) φ}"
      apply (rule solves_ode_congI)
          apply (rule sol)
         subgoal for ta by auto
        subgoal for ta using sem_fact[of ta] by auto
       subgoal by (rule refl)
      subgoal by (rule refl)
      done
    have sol'':"(sol solves_ode (λa. ODE_sem I (Osubst ODE σ))) {0..t} {x. mk_v I (Osubst ODE σ) (sol 0, bb) x  fml_sem I (Fsubst φ σ)}"
      apply (rule solves_odeI)
       subgoal using sol' solves_ode_vderivD by blast
      subgoal for ta using sub[of ta] apply auto 
        by (meson empty_iff)
      done
  show "sola. sol 0 = sola 0 
        (ta. mk_v (adjoint I σ (sol 0, bb)) ODE (sol 0, bb) (sol t) = mk_v I (Osubst ODE σ) (sola 0, bb) (sola ta) 
              0  ta 
              (sola solves_ode (λa. ODE_sem I (Osubst ODE σ))) {0..ta} {x. mk_v I (Osubst ODE σ) (sola 0, bb) x  fml_sem I (Fsubst φ σ)})"
    apply(rule exI[where x=sol])
    apply(rule conjI)
     subgoal by (rule refl)
    apply(rule exI[where x=t])
    apply(rule conjI)
     subgoal using  mkvt t by auto
    apply(rule conjI)
     subgoal by (rule t)
    subgoal using sol'' by auto 
    done
  qed
  then show "?case" by auto 
next
  case (Padmit_Choice σ a b) then 
  have IH1:"hpsafe a  ssafe σ  (ν ω. ((ν, ω)  prog_sem I (Psubst a σ)) = ((ν, ω)  prog_sem (local.adjoint I σ ν) a))"
    and IH2:"hpsafe b  ssafe σ  (ν ω. ((ν, ω)  prog_sem I (Psubst b σ)) = ((ν, ω)  prog_sem (local.adjoint I σ ν) b))"
    by blast+
  have hpsafe1:"hpsafe (a ∪∪ b)  hpsafe a" 
    and hpsafe2:"hpsafe (a ∪∪ b)  hpsafe b" 
    by (auto dest: hpsafe.cases)
  show ?case using IH1[OF hpsafe1] IH2[OF hpsafe2] by auto
next
  case (Padmit_Assign σ θ x) then
  have TA:"Tadmit σ θ" by auto
  have "hpsafe (Assign x θ)  ssafe σ   (ν ω. ((ν, ω)  prog_sem I (Psubst (Assign x θ) σ)) = ((ν, ω)  prog_sem (adjoint I σ ν) (Assign x θ)))"
  proof -
    assume hpsafe:"hpsafe (Assign x θ)"
    assume ssafe:"ssafe σ"
    from ssafe have ssafes:"(i f'. SFunctions σ i = Some f'  dfree f')"
        "(f f'. SPredicates σ f = Some f'  fsafe f')"
        unfolding ssafe_def by auto
    from hpsafe have dsafe:"dsafe θ" by (auto elim: hpsafe.cases)
    fix ν ω
    show "?thesis ν ω"
      using subst_dterm[OF good_interp TA dsafe ssafes]
      by auto
  qed
  then show ?case by auto
next
  case (Padmit_DiffAssign σ θ x) then
  have TA:"Tadmit σ θ" by auto
  have "hpsafe (DiffAssign x θ)  ssafe σ   (ν ω. ((ν, ω)  prog_sem I (Psubst (DiffAssign x θ) σ)) = ((ν, ω)  prog_sem (adjoint I σ ν) (DiffAssign x θ)))"
  proof -
    assume hpsafe:"hpsafe (DiffAssign x θ)"
    assume ssafe:"ssafe σ"
    from ssafe have ssafes:"(i f'. SFunctions σ i = Some f'  dfree f')"
        "(f f'. SPredicates σ f = Some f'  fsafe f')"
        unfolding ssafe_def by auto
    from hpsafe have dsafe:"dsafe θ" by (auto elim: hpsafe.cases)
    fix ν ω
    show "?thesis ν ω"
      using subst_dterm[OF good_interp TA dsafe ssafes]
      by auto
  qed
  then show ?case by auto
next
  case (Padmit_Test σ φ) then
  have IH:"fsafe φ  ssafe σ  (ν. (ν  fml_sem I (Fsubst φ σ)) = (ν  fml_sem (local.adjoint I σ ν) φ))"
    by auto
  have "hpsafe (? φ)  ssafe σ  (ν ω. ((ν, ω)  prog_sem I (Psubst (? φ) σ)) = ((ν, ω)  prog_sem (local.adjoint I σ ν) (? φ)))"
  proof -
    assume hpsafe:"hpsafe (? φ)"
    from hpsafe have fsafe:"fsafe φ" by (auto dest: hpsafe.cases)
    assume ssafe:"ssafe σ"
    fix ν ω
    show "?thesis ν ω" using IH[OF fsafe ssafe] by auto
  qed
  then show ?case by auto
next
  case (Fadmit_Geq σ θ1 θ2) then 
  have TA1:"Tadmit σ θ1" and TA2:"Tadmit σ θ2"
    by auto
  have "fsafe (Geq θ1 θ2)  ssafe σ  (ν. (ν  fml_sem I (Fsubst (Geq θ1 θ2) σ)) = (ν  fml_sem (local.adjoint I σ ν) (Geq θ1 θ2)))"
  proof -
    assume fsafe:"fsafe (Geq θ1 θ2)"
    assume ssafe:"ssafe σ"
    from fsafe have dsafe1:"dsafe θ1" and dsafe2:"dsafe θ2"
      by (auto dest: fsafe.cases)
    from ssafe have ssafes:"(i f'. SFunctions σ i = Some f'  dfree f')"
      "(f f'. SPredicates σ f = Some f'  fsafe f')"
      unfolding ssafe_def by auto
    fix ν
    show "?thesis ν" using 
      subst_dterm[OF good_interp TA1 dsafe1 ssafes]
      subst_dterm[OF good_interp TA2 dsafe2 ssafes]
      by auto 
  qed
  then show ?case by auto 
next 
  case (Fadmit_Prop1 σ args p p') then
    have TA:"i. Tadmit σ (args i)"
    and some:"SPredicates σ p = Some p'"
    and NFA:"NFadmit (λi. Tsubst (args i) σ) p'"
    and substSafes:"i. dsafe (Tsubst (args i) σ)"
      by auto
    have "fsafe ( p args) 
         ssafe σ  (ν. (ν  fml_sem I (Fsubst ( p args) σ)) = (ν  fml_sem (local.adjoint I σ ν) ( p args)))"
    proof -
      assume fsafe:"fsafe ( p args)"
      assume ssafe:"ssafe σ"
      from ssafe have ssafes:"(i f'. SFunctions σ i = Some f'  dfree f')"
      "(f f'. SPredicates σ f = Some f'  fsafe f')"
      unfolding ssafe_def by auto
      fix ν
      from fsafe have safes:"i. dsafe (args i)" using dfree_is_dsafe by auto
      have IH:"(ν'. i. dsafe (args i) 
          dterm_sem I (Tsubst (args i) σ) ν = dterm_sem (adjoint I σ ν) (args i) ν)" 
        using  subst_dterm[OF good_interp TA safes ssafes] by auto
      have eqs:"i ν'. dterm_sem I (Tsubst (args i) σ) ν = dterm_sem (adjoint I σ ν) (args i) ν"
        by (auto simp add: IH safes)
      let ?sub = "(λ i. Tsubst (args i) σ)"
      have freef:"fsafe p'" using ssafe some unfolding ssafe_def by auto 
      have IH2:"(ν  fml_sem I (FsubstFO p' ?sub)) = (ν  fml_sem (adjointFO I ?sub ν) p')"
        using nsubst_fml good_interp NFA freef substSafes
        by blast
      have vec:"(χ i. dterm_sem I (Tsubst (args i) σ) ν) = (χ i. dterm_sem (local.adjoint I σ ν) (args i) ν)"
        apply(auto simp add: vec_eq_iff)
        subgoal for i
          using IH[of i, OF safes[of i]] 
          by auto
        done
      show "?thesis ν" 
        using IH safes eqs apply (auto simp add:  IH2  some good_interp)
        using some unfolding adjoint_def adjointFO_def by auto
    qed
  then show "?case" by auto
next
  case (Fadmit_Prop2 σ args p) 
  note TA = Fadmit_Prop2.hyps(1)
    and none = Fadmit_Prop2.hyps(2)
  have "fsafe (Prop p args)  ssafe σ  (ν.(ν  fml_sem I (Fsubst ( p args) σ)) = (ν  fml_sem (local.adjoint I σ ν) ( p args)))"
  proof -
    assume safe:"fsafe (Prop p args)" and ssafe:"ssafe σ"
    from ssafe have ssafes:"(i f'. SFunctions σ i = Some f'  dfree f')"
        "(f f'. SPredicates σ f = Some f'  fsafe f')"
        unfolding ssafe_def by auto
    fix ν
    from safe have  safes:"i. dsafe (args i)" using dfree_is_dsafe by auto
    have IH:"(ν'. i. dsafe (args i) 
        dterm_sem I (Tsubst (args i) σ) ν = dterm_sem (adjoint I σ ν) (args i) ν)" 
    using  subst_dterm[OF good_interp TA safes ssafes] by auto
    have Ieq:"Predicates I p = Predicates (adjoint I σ ν) p"
      using none unfolding adjoint_def by auto
    have vec:"(χ i. dterm_sem I (Tsubst (args i) σ) ν) = (χ i. dterm_sem (adjoint I σ ν) (args i) ν)"
      apply(auto simp add: vec_eq_iff)
      subgoal for i using IH[of i, OF safes[of i]] by auto
      done
    show "?thesis ν" using none IH Ieq vec by auto
  qed
  then show "?case" by auto
next
  case (Fadmit_Not σ φ) then 
  have IH:"fsafe φ  ssafe σ  (ν. (ν  fml_sem I (Fsubst φ σ)) = (ν  fml_sem (local.adjoint I σ ν) φ))"
    by blast
  have fsafe:"fsafe (Not φ)  fsafe φ"
    by (auto dest: fsafe.cases)
  show ?case using IH[OF fsafe] by auto
next
  case (Fadmit_And σ φ ψ) then
    have IH1:"fsafe φ  ssafe σ  (ν. (ν  fml_sem I (Fsubst φ σ)) = (ν  fml_sem (local.adjoint I σ ν) φ))"
      and IH2:"fsafe ψ  ssafe σ  (ν. (ν  fml_sem I (Fsubst ψ σ)) = (ν  fml_sem (local.adjoint I σ ν) ψ))"
      by (blast)+
    have fsafe1:"fsafe (φ && ψ)  fsafe φ" and fsafe2:"fsafe (φ && ψ)  fsafe ψ" 
      by (auto dest: fsafe.cases)
    show ?case using IH1[OF fsafe1] IH2[OF fsafe2] by auto
next
  case (Fadmit_Exists σ φ x)
  then have IH:"fsafe φ  ssafe σ  (ν. (ν  fml_sem I (Fsubst φ σ)) = (ν  fml_sem (local.adjoint I σ ν) φ))"
    and FUA:"FUadmit σ φ {Inl x}"
    by blast+
  have fsafe:"fsafe (Exists x φ)  fsafe φ"
    by (auto dest: fsafe.cases)
  have eq:"fsafe (Exists x φ)  ssafe σ  (ν. (ν  fml_sem I (Fsubst  (Exists x φ) σ)) = (ν  fml_sem (local.adjoint I σ ν)  (Exists x φ)))"
  proof -
    assume fsafe:"fsafe (Exists x φ)"
    from fsafe have fsafe':"fsafe φ" by (auto dest: fsafe.cases)
    assume ssafe:"ssafe σ"
    fix ν
    have agree:"r. Vagree ν (repv ν x r) (- {Inl x})"
      unfolding Vagree_def by auto
    have sem_eq:"r. ((repv ν x r)  fml_sem (local.adjoint I σ (repv ν x r)) φ) =
                      ((repv ν x r)  fml_sem (local.adjoint I σ ν) φ)"
      using uadmit_fml_adjoint[OF FUA agree fsafe' ssafe good_interp] by auto
    have "(ν  fml_sem I (Fsubst  (Exists x φ) σ)) = (r. (repv ν x r)  fml_sem I (Fsubst φ σ))"
      by auto
    moreover have "... = (r. (repv ν x r)  fml_sem (local.adjoint I σ (repv ν x r)) φ)"
      using IH[OF fsafe' ssafe] by auto
    moreover have "... = (r. (repv ν x r)  fml_sem (local.adjoint I σ ν) φ)"
      using sem_eq by auto
    moreover have "... = (ν  fml_sem (adjoint I σ ν) (Exists x φ))"
      by auto
    ultimately show "(ν  fml_sem I (Fsubst  (Exists x φ) σ)) = (ν  fml_sem (local.adjoint I σ ν)  (Exists x φ))"
      by auto
    qed
  then show ?case by auto
next
  case (Fadmit_Diamond σ φ a) then 
    have PA:"Padmit σ a" 
      and FUA:"FUadmit σ φ (BVP (Psubst a σ))"
      and IH1:"fsafe φ  ssafe σ  (ν. (ν  fml_sem I (Fsubst φ σ)) = (ν  fml_sem (adjoint I σ ν) φ))"
      and IH2:"hpsafe a  ssafe σ  (ν ω. ((ν, ω)  prog_sem I (Psubst a σ)) = ((ν, ω)  prog_sem (adjoint I σ ν) a))"
      and substSafe:"hpsafe (Psubst a σ)"
      by auto
    have "fsafe ( a  φ)  ssafe σ  (ν. (ν  fml_sem I (Fsubst ( a  φ) σ)) = (ν  fml_sem (local.adjoint I σ ν) ( a  φ)))"
    proof -
      assume fsafe:"fsafe ( a  φ)"
      assume ssafe:"ssafe σ"
      from fsafe have fsafe':"fsafe φ" and hpsafe:"hpsafe a" by (auto dest: fsafe.cases)
      fix ν
      have agree:"ω. (ν, ω)  prog_sem I (Psubst a σ)  Vagree ν ω (-BVP(Psubst a σ))"
        using bound_effect[OF good_interp, of "(Psubst a σ)" ν, OF substSafe] by auto
      have sem_eq:"ω. (ν, ω)  prog_sem I (Psubst a σ)  
          (ω  fml_sem (local.adjoint I σ ν) φ) =
          (ω  fml_sem (local.adjoint I σ ω) φ)"
        using uadmit_fml_adjoint[OF FUA agree fsafe' ssafe good_interp] by auto
      have "(ν  fml_sem I (Fsubst ( a  φ) σ)) = ( ω. (ν, ω)  prog_sem I (Psubst a σ)  ω  fml_sem I (Fsubst φ σ))"
        by auto
      moreover have "... = ( ω. (ν, ω)  prog_sem (adjoint I σ ν) a  ω  fml_sem (adjoint I σ ω) φ)"
        using IH1[OF fsafe' ssafe] IH2[OF hpsafe ssafe, of ν] by auto
      moreover have "... = ( ω. (ν, ω)  prog_sem (adjoint I σ ν) a  ω  fml_sem (adjoint I σ ν) φ)"
        using sem_eq IH2 hpsafe ssafe by blast
      moreover have "... = (ν  fml_sem (adjoint I σ ν) ( a  φ))"
        by auto
      ultimately show "?thesis ν" by auto
    qed
  then show ?case by auto
next
   case (Fadmit_Prop1 σ args p p') 
   have "fsafe(Prop p args)  ssafe σ  (ν.(ν  fml_sem I (Fsubst ( p args) σ)) = (ν  fml_sem (local.adjoint I σ ν) ( p args)))"
   proof -
     assume fsafe:"fsafe (Prop p args)"
       and ssafe:"ssafe σ"
     from ssafe have ssafes:"(i f'. SFunctions σ i = Some f'  dfree f')"
       "(f f'. SPredicates σ f = Some f'  fsafe f')"
       unfolding ssafe_def by auto
     fix ν
     note TA = Fadmit_Prop1.hyps(1)
       and some = Fadmit_Prop1.hyps(2) and NFA = Fadmit_Prop1.hyps(3)
     from fsafe have safes:"i. dsafe (args i)" using dfree_is_dsafe by auto
     have IH:"(ν'. i. dsafe (args i) 
         dterm_sem I (Tsubst (args i) σ) ν = dterm_sem (adjoint I σ ν) (args i) ν)" 
       using  subst_dterm[OF good_interp TA safes ssafes] by auto
     have eqs:"i ν'. dterm_sem I (Tsubst (args i) σ) ν = dterm_sem (adjoint I σ ν) (args i) ν"
       by (auto simp add: IH safes)
     let ?sub = "(λ i. Tsubst (args i) σ)"
     have subSafe:"( i. dsafe (?sub i))"
       by (simp add: safes ssafes tsubst_preserves_safe)
     have freef:"fsafe p'" using ssafe some unfolding ssafe_def by auto 
     have IH2:"(ν  fml_sem I (FsubstFO p' ?sub)) = (ν  fml_sem (adjointFO I ?sub ν) p')"
       by (simp add: nsubst_fml [OF good_interp NFA freef subSafe])
     have vec:"(χ i. dterm_sem I (Tsubst (args i) σ) ν) = (χ i. dterm_sem (local.adjoint I σ ν) (args i) ν)"
       apply(auto simp add: vec_eq_iff)
       subgoal for i
         using IH[of i, OF safes[of i]] 
         by auto
       done
     show "?thesis ν" 
       using IH safes eqs apply (auto simp add:  IH2  some good_interp)
       using some unfolding adjoint_def adjointFO_def by auto
   qed    
next
  case (Fadmit_Context1 σ φ C C') then
  have FA:"Fadmit σ φ"
    and FUA:"FUadmit σ φ UNIV"
    and some:"SContexts σ C = Some C'"
    and PFA:"PFadmit (λ_. Fsubst φ σ) C'"
    and IH:"fsafe φ  ssafe σ  (ν. (ν  fml_sem I (Fsubst φ σ)) = (ν  fml_sem (local.adjoint I σ ν) φ))"
    and substSafe:"fsafe(Fsubst φ σ)"
    by auto
  have "fsafe (InContext C φ)  ssafe σ  (ν. (ν  fml_sem I (Fsubst (InContext C φ) σ)) = (ν  fml_sem (local.adjoint I σ ν) (InContext C φ)))"
  proof -
    assume safe:"fsafe (InContext C φ)"
    from safe have fsafe:"fsafe φ" by (auto dest: fsafe.cases)
    assume ssafe:"ssafe σ"
    fix ν :: "'sz state"
    have agree:"ω. Vagree ν ω (-UNIV)" unfolding Vagree_def by auto
    have adj_eq:"ω. fml_sem (adjoint I σ ν) φ = fml_sem (adjoint I σ ω) φ"
      using uadmit_fml_adjoint[OF FUA agree fsafe ssafe good_interp] by auto
    have eq:"(ν  fml_sem I (Fsubst φ σ)) = (ν  fml_sem (local.adjoint I σ ν) φ)"
      using adj_eq IH[OF fsafe ssafe] by auto
    let ?sub = "(λ_. Fsubst φ σ)"
    let ?R1 = "fml_sem I (Fsubst φ σ)"
    let ?R2 = "fml_sem (adjoint I σ ν) φ"
    have eq':"?R1 = ?R2"
      using adj_eq IH[OF fsafe ssafe] by auto
    have freef:"fsafe C'" using ssafe some unfolding ssafe_def by auto 
    have IH2:"(ν  fml_sem I (PFsubst C' ?sub)) = (ν  fml_sem (PFadjoint I ?sub) C')"
      using psubst_fml good_interp PFA fsafe substSafe freef by blast 
    have IH':"(ν. (ν  fml_sem I (Fsubst φ σ)) = (ν  fml_sem (adjoint I σ ν) φ))"
      using IH[OF fsafe ssafe] by auto
    then have IH:"fml_sem I (Fsubst φ σ) = fml_sem (adjoint I σ ν) φ"
      using eq' by blast
    have duh:" (λf' _. fml_sem I (case () of ()  Fsubst φ σ)) = (λ x (). fml_sem (local.adjoint I σ ν) φ)"
      by (simp add: case_unit_Unity eq' ext)
    have extend_PF:"(PFadjoint I ?sub) = (extendc I ?R2)"
      unfolding PFadjoint_def using IH apply (simp)
      by (metis old.unit.case old.unit.exhaust)
    have "(ν  fml_sem I (Fsubst (InContext C φ) σ)) = (ν  fml_sem I (PFsubst C' (λ_. Fsubst φ σ)))"
      using some by simp
    moreover have "... = (ν  fml_sem (PFadjoint I ?sub) C')"
      using IH2 by auto
    moreover have "... = (ν  fml_sem (extendc I ?R2) C')"
      using extend_PF by simp
    moreover have "... = (ν  fml_sem (extendc I ?R1) C')"
      using eq' by auto
    moreover have "... = (ν  Contexts (adjoint I σ ν) C (fml_sem (adjoint I σ ν) φ))"
      using some unfolding adjoint_def apply auto
      apply (simp add: eq' local.adjoint_def)
      by (simp add: eq' local.adjoint_def)
    moreover have "... = (ν  fml_sem (adjoint I σ ν) (InContext C φ))"
      by auto
    ultimately
    show "(ν  fml_sem I (Fsubst (InContext C φ) σ)) = (ν  fml_sem (local.adjoint I σ ν) (InContext C φ))"
      by blast
  qed
  then show ?case by auto
next
  case (Fadmit_Context2 σ φ C) then
  have FA:"Fadmit σ φ"
  and FUA:"FUadmit σ φ UNIV"
  and none:"SContexts σ C = None"
  and IH:"fsafe φ  ssafe σ  (ν. (ν  fml_sem I (Fsubst φ σ)) = (ν  fml_sem (local.adjoint I σ ν) φ))"
    by auto
  have "fsafe (InContext C φ) 
           ssafe σ  (ν. (ν  fml_sem I (Fsubst (InContext C φ) σ)) = (ν  fml_sem (local.adjoint I σ ν) (InContext C φ)))"
  proof -
    assume safe:"fsafe (InContext C φ)"
    then have fsafe:"fsafe φ" by (auto dest: fsafe.cases)
    assume ssafe:"ssafe σ"
    fix ν
    have Ieq:" Contexts (local.adjoint I σ ν) C = Contexts I C"
      using none unfolding adjoint_def by auto
    have IH':"ν. (ν  fml_sem I (Fsubst φ σ)) = (ν  fml_sem (local.adjoint I σ ν) φ)"
      using IH[OF fsafe ssafe] by auto
    have agree:"ω. Vagree ν ω (-UNIV)" unfolding Vagree_def by auto
    have adj_eq:"ω. fml_sem (adjoint I σ ν) φ = fml_sem (adjoint I σ ω) φ"
      using uadmit_fml_adjoint[OF FUA agree fsafe ssafe good_interp] by auto
    then have sem:"fml_sem I (Fsubst φ σ) =  fml_sem (local.adjoint I σ ν) φ"
      using IH' agree adj_eq by auto
    show "?thesis ν"  using none Ieq sem by auto
  qed
  then show ?case by auto
qed

lemma subst_fml:
  fixes I::"('sf, 'sc, 'sz) interp" and ν::"'sz state"
  assumes good_interp:"is_interp I"
  assumes Fadmit:"Fadmit σ φ"
  assumes fsafe:"fsafe φ"
  assumes ssafe:"ssafe σ"
  shows "(ν  fml_sem I (Fsubst φ σ)) = (ν  fml_sem (adjoint I σ ν) φ)"
      using subst_fml_hp[OF good_interp] Fadmit fsafe ssafe by blast
    
lemma subst_fml_valid:
  fixes I::"('sf, 'sc, 'sz) interp" and ν::"'sz state"
  assumes Fadmit:"Fadmit σ φ"
  assumes fsafe:"fsafe φ"
  assumes ssafe:"ssafe σ"
  assumes valid:"valid φ"
  shows "valid (Fsubst φ σ)"
proof -
  have sub_sem:"I ν. is_interp I  ν  fml_sem I (Fsubst φ σ)"
  proof -
    fix I::"('sf,'sc,'sz) interp" and ν::"'sz state"
    assume good_interp:"is_interp I"
    have good_adj:"is_interp (adjoint I σ ν)"
      apply(rule adjoint_safe[OF good_interp])
      using ssafe unfolding ssafe_def by auto
    have φsem:"ν  fml_sem (adjoint I σ ν) φ" using valid using good_adj unfolding valid_def by blast
    then show "?thesis I ν"
      using subst_fml[OF good_interp Fadmit fsafe ssafe]
      by auto
  qed
  then show ?thesis unfolding valid_def by blast 
qed
  

lemma subst_sequent:
  fixes I::"('sf, 'sc, 'sz) interp" and ν::"'sz state"
  assumes good_interp:"is_interp I"
  assumes Sadmit:"Sadmit σ (Γ,Δ)"
  assumes Ssafe:"Ssafe (Γ,Δ)"
  assumes ssafe:"ssafe σ"
  shows "(ν  seq_sem I (Ssubst (Γ,Δ) σ)) = (ν  seq_sem (adjoint I σ ν) (Γ,Δ))"
proof -
  let ?f = "(seq2fml (Γ, Δ))"
  have subst_eqG:"Fsubst (foldr (&&) Γ TT) σ = foldr (&&) (map (λφ. Fsubst φ σ) Γ) TT"
    by(induction Γ, auto simp add: TT_def)
  have subst_eqD:"Fsubst (foldr (||) Δ FF) σ = foldr (||) (map (λφ. Fsubst φ σ) Δ) FF"
    by(induction Δ, auto simp add: FF_def Or_def)
  have subst_eq:"Fsubst ?f σ = (seq2fml (Ssubst (Γ, Δ) σ))"
    using subst_eqG subst_eqD 
    by (auto simp add: Implies_def Or_def)
  have fsafeG:"fsafe (foldr (&&) Γ TT)" 
    using Ssafe apply(induction Γ, auto simp add: Ssafe_def TT_def)
    by fastforce
  have fsafeD:"fsafe (foldr (||) Δ FF)" 
    using Ssafe Or_def apply(induction Δ, auto simp add: Ssafe_def FF_def Or_def)
    by fastforce
  have fsafe:"fsafe ?f" 
    using fsafeD fsafeG by (auto simp add: Implies_def Or_def)
  have FadmitG:"Fadmit σ (foldr (&&) Γ TT)"
    using Sadmit Or_def apply(induction Γ, auto simp add: Sadmit_def TT_def Or_def)
    by fastforce
  have FadmitD:"Fadmit σ (foldr (||) Δ FF)"
    using Sadmit Or_def apply(induction Δ, auto simp add: Sadmit_def FF_def Or_def)
    by fastforce
  have Fadmit:"Fadmit σ ?f" 
    using FadmitG FadmitD unfolding Implies_def
    by (simp add: Implies_def Or_def)
  have "(ν  fml_sem I (Fsubst ?f σ)) 
       =(ν  fml_sem (adjoint I σ ν) (seq2fml (Γ, Δ)))"
    using subst_fml[OF good_interp Fadmit fsafe ssafe]
    by auto
  then show ?thesis
    using subst_eq by auto
  qed

subsection ‹Soundness of substitution rule›
theorem subst_rule:
  assumes sound:"sound R"
  assumes Radmit:"Radmit σ R"
  assumes FVS:"FVS σ = {}"
  assumes Rsafe:"Rsafe R"
  assumes ssafe:"ssafe σ"
  shows "sound (Rsubst R σ)"
proof -
  obtain SG and C where Rdef:"R = (SG,C)" by (cases R, auto)
  obtain SG' and C' where Rdef':"Rsubst R σ = (SG',C')" by (cases R, auto)
  obtain ΓC and ΔC where Cdef:"C = (ΓC, ΔC)" by (cases C, auto)
  obtain ΓC' and ΔC' where C'def:"C' = (ΓC', ΔC')" by (cases C', auto)
  have CC':"(Ssubst (ΓC, ΔC) σ) = (ΓC', ΔC')"
    using Rdef Rdef' Cdef C'def by auto
  have "I ν. is_interp I  (Γ Δ ω  . List.member SG' (Γ, Δ)  ω  seq_sem I (Γ, Δ))  ν  seq_sem I C'"
  proof -
    fix I::"('sf,'sc,'sz) interp" and ν::"'sz state"
    assume good_interp:"is_interp I"
    assume prems:"(Γ Δ ω. List.member SG' (Γ, Δ)  ω  seq_sem I (Γ, Δ))"
    have good_interp':"ω. is_interp (adjoint I σ ω)"
      using adjoint_safe[OF good_interp ] ssafe[unfolded ssafe_def] by auto
    have sound:"ω. (φ ν . List.member SG φ  ν  seq_sem (adjoint I σ ω) φ)  ω  seq_sem (adjoint I σ ω) (ΓC, ΔC)"
      using soundD_memv[of SG C] sound good_interp' Rdef Cdef by auto
    have SadmitC:"Sadmit σ (ΓC, ΔC)" 
      using Radmit unfolding Radmit_def Rdef Cdef by auto
    have SsafeC:"Ssafe (ΓC, ΔC)" 
      using Rsafe unfolding Rsafe_def Rdef Cdef by auto
    have seq_sem:"ν  seq_sem (adjoint I σ ν) (ΓC, ΔC)"
    proof(rule sound)
      fix S :: "('sf,'sc,'sz) sequent" and ν'
      assume mem:"List.member SG S"
      obtain ΓS ΔS where Sdef:"S = (ΓS, ΔS)" by (cases S, auto)
      from mem obtain di where di:"di < length SG  SG ! di = S"
      by (meson in_set_conv_nth in_set_member)
      have SadmitS:"Sadmit σ (ΓS, ΔS)"
        using Rdef Sdef di Radmit Radmit_def by auto
      have SsafeS:"Ssafe (ΓS, ΔS)"
        using Rsafe unfolding Rsafe_def Rdef Cdef using Sdef mem di by auto
      have map_mem:"f L x. List.member L x  List.member (map f L) (f x)"
        subgoal for f L x 
          by (induction L, auto simp add: member_rec)
        done
      let ?S' = "(Ssubst (ΓS, ΔS) σ)"
      have eq:"Ssubst S σ = (map (λφ. Fsubst φ σ) ΓS, map (λφ. Fsubst φ σ) ΔS)" 
        using Sdef by auto
      from Sdef have mem':"List.member SG' (fst ?S', snd ?S')"
        using mem Rdef Rdef' eq map_mem[of SG S "(λx. Ssubst x σ)"] by auto
      have "ν'  seq_sem I (fst ?S', snd ?S')" by (rule prems[OF mem', of ν'])
      then have "ν'  seq_sem (adjoint I σ ν') S"
        using subst_sequent[OF good_interp SadmitS SsafeS ssafe, of ν']
        Sdef by auto
      have VA:"Vagree ν ν' (FVS σ)" using FVS unfolding Vagree_def by auto
      show "ν'  seq_sem (local.adjoint I σ ν) S"
        using adjoint_consequence VA ssafe[unfolded ssafe_def]
        by (metis ν'  seq_sem (local.adjoint I σ ν') S dfree_is_dsafe)
      qed
    have "ν  seq_sem I (ΓC', ΔC')"
      using subst_sequent[OF good_interp SadmitC SsafeC ssafe, of ν] seq_sem Cdef C'def CC'
      by auto
    then show  "ν  seq_sem I C'" using C'def by auto
    qed
  then show ?thesis
    apply(rule soundI_memv')
      using Rdef' by auto
qed

end end