Theory Frechet_Correctness

theory "Frechet_Correctness"
imports
  Ordinary_Differential_Equations.ODE_Analysis
  "Lib"
  "Syntax"
  "Denotational_Semantics"
  "Ids"
begin
context ids begin
section ‹Characterization of Term Derivatives›
text ‹
 This section builds up to a proof that in well-formed interpretations, all
 terms have derivatives, and those derivatives agree with the expected rules
 of derivatives. In particular, we show the [frechet] function given in the
 denotational semantics is the true Frechet derivative of a term. From this
 theorem we can recover all the standard derivative identities as corollaries.
›

lemma inner_prod_eq:
  fixes i::"'a::finite"
  shows "(λ(v::'a Rvec). v ∙ axis i 1) = (λ(v::'a Rvec). v $ i)"
  unfolding cart_eq_inner_axis axis_def by (simp add: eq_commute)

theorem svar_deriv:
  fixes x:: "'sv::finite" and ν:: "'sv Rvec" and F::"real filter"
  shows "((λv. v $ x) has_derivative (λv'. v' ∙ (χ i. if i = x then 1 else 0))) (at ν)"
proof -
  let ?f = "(λv. v)"
  let ?f' = "(λv'. v')"
  let ?g = "(λv. axis x 1)"
  let ?g' = "(λv. 0)"
  have id_deriv: "(?f has_derivative ?f') (at ν) "
    by (rule has_derivative_ident)
  have const_deriv: "(?g has_derivative ?g') (at ν)"
    by (rule has_derivative_const)
  have inner_deriv:"((λx. inner (?f x) (?g x)) has_derivative
                     (λh. inner (?f ν) (?g' h) + inner (?f' h) (?g ν))) (at ν)"
    by (intro has_derivative_inner [OF id_deriv const_deriv])
  from inner_prod_eq
  have left_eq: "(λx. inner (?f x) (?g x)) = (λv. vec_nth v x)"
    by (auto)
  from inner_deriv and inner_prod_eq
  have better_deriv:"((λv. vec_nth v x) has_derivative
                     (λh. inner (?f ν) (?g' h) + inner (?f' h) (?g ν))) (at ν)"
    by (metis (no_types, lifting) UNIV_I has_derivative_transform)
  have vec_eq:"(χ i. if i = x then 1 else 0) = (χ i. if x = i then 1 else 0)"
    by(rule vec_extensionality, auto)
  have deriv_eq:"(λh. ν ∙ 0 + h ∙ axis x 1) = (λv'. v' ∙ (χ i. if i = x then 1 else 0))"
    by(rule ext, auto simp add: axis_def vec_eq)
  show ?thesis 
    apply(rule has_derivative_eq_rhs[where f'= "(λh. ν ∙ 0 + h ∙ axis x 1)"])
    using better_deriv deriv_eq  by auto
qed

lemma function_case_inner:
  assumes good_interp:
    "(∀x i. (Functions I i has_derivative FunctionFrechet I i x) (at x))"
  assumes IH:"((λv. χ i. sterm_sem I (args i) v)
             has_derivative (λ v. (χ i. frechet I (args i) ν v))) (at ν)"
  shows  "((λv. Functions I f (χ i. sterm_sem I (args i) v))
            has_derivative (λv. frechet I ($f f args) ν v)) (at ν)"
proof -
  let ?h = "(λv. Functions I f (χ i. sterm_sem I (args i) v))"
  let ?h' = "frechet I ($f f args) ν"
  let ?g = "(λv. χ i. sterm_sem I (args i) v)"
  let ?g' = "(λv. χ i. frechet I (args i) ν v)"
  let ?f = "(λy. Functions I f y)"
  let ?f' = "FunctionFrechet I f (?g ν)"
  have hEqFG:  "?h  = ?f  o ?g" by (auto)
  have hEqFG': "?h' = ?f' o ?g'"
  proof -
    have frechet_def:"frechet I (Function f args) ν
        = (λv'. FunctionFrechet I f (?g ν) (χ i. frechet I (args i) ν v'))"
      by (auto)
    have composition:
      "(λv'. FunctionFrechet I f (?g ν) (χ i. frechet I (args i) ν v'))
       = (FunctionFrechet I f (?g ν)) o (λ v'. χ i. frechet I (args i) ν v')"
      by (auto)
    from frechet_def and composition show ?thesis by (auto)
  qed
  have fDeriv: "(?f has_derivative ?f') (at (?g ν))"
    using good_interp is_interp_def by blast
  from IH have gDeriv: "(?g has_derivative ?g') (at ν)" by (auto)
  from fDeriv and gDeriv
  have composeDeriv: "((?f o ?g) has_derivative (?f' o ?g')) (at ν)"
    using diff_chain_at good_interp by blast
  from hEqFG hEqFG' composeDeriv show ?thesis by (auto)
qed

lemma func_lemma2:"(∀x i. (Functions I i has_derivative (THE f'. ∀x. (Functions I i has_derivative f' x) (at x)) x) (at x) ∧
          continuous_on UNIV (λx. Blinfun ((THE f'. ∀x. (Functions I i has_derivative f' x) (at x)) x))) ⟹
    (⋀θ. θ ∈ range args ⟹ (sterm_sem I θ has_derivative frechet I θ ν) (at ν)) ⟹
    ((λv. Functions I f (vec_lambda(λi. sterm_sem I (args i) v))) has_derivative (λv'. (THE f'. ∀x. (Functions I f has_derivative f' x) (at x)) (χ i. sterm_sem I (args i) ν) (χ i. frechet I (args i) ν v'))) (at ν)"
proof -
  assume a1: "∀x i. (Functions I i has_derivative (THE f'. ∀x. (Functions I i has_derivative f' x) (at x)) x) (at x) ∧
          continuous_on UNIV (λx. Blinfun ((THE f'. ∀x. (Functions I i has_derivative f' x) (at x)) x))"
  then have a1':"∀x i. (Functions I i has_derivative (THE f'. ∀x. (Functions I i has_derivative f' x) (at x)) x) (at x)" by auto
  assume a2: "⋀θ. θ ∈ range args ⟹ (sterm_sem I θ has_derivative frechet I θ ν) (at ν)"
  have "∀f fa v. (∃fb. ¬ (f (fb::'a) has_derivative fa fb (v::(real, 'a) vec)) (at v)) ∨ ((λv. (χ fa. (f fa v::real))) has_derivative (λva. (χ f. fa f v va))) (at v)"
    using has_derivative_vec by force
  then have "((λv. χ f. sterm_sem I (args f) v) has_derivative (λv. χ f. frechet I (args f) ν v)) (at ν)"
    by (auto simp add: a2 has_derivative_vec)
  then show "((λv. Functions I f (vec_lambda(λf. sterm_sem I (args f) v))) has_derivative (λv'. (THE f'. ∀x. (Functions I f has_derivative f' x) (at x)) (χ i. sterm_sem I (args i) ν) (χ i. frechet I (args i) ν v'))) (at ν)"
    using a1' function_case_inner by auto
qed

lemma func_lemma:
  "is_interp I ⟹
  (⋀θ :: ('a::finite, 'c::finite) trm. θ ∈ range args ⟹ (sterm_sem I θ has_derivative frechet I θ ν) (at ν)) ⟹
  (sterm_sem I ($f f args) has_derivative frechet I ($f f args) ν) (at ν)"
  apply(auto simp add: sfunction_case is_interp_def function_case_inner)
  apply(erule func_lemma2)
  apply(auto)  
  done

text ‹ The syntactic definition of term derivatives agrees with the semantic definition.
  Since the syntactic definition of derivative is total, this gives us that derivatives are "decidable" for
  terms (modulo computations on reals) and that they obey all the expected identities, which gives
  us the axioms we want for differential terms essentially for free.
 ›
lemma frechet_correctness:
  fixes I :: "('a::finite, 'b::finite, 'c::finite) interp" and ν
  assumes good_interp: "is_interp I"
  shows "dfree θ ⟹ FDERIV (sterm_sem I θ) ν :> (frechet I θ ν)"
proof (induct rule: dfree.induct)
  case (dfree_Var i) then show ?case
    by (auto simp add: svar_case svar_deriv axis_def)
next
  case (dfree_Fun args i) with good_interp show ?case
    by (intro func_lemma) auto
qed auto

text ‹If terms are semantically equivalent in all states, so are their derivatives›
lemma sterm_determines_frechet:
  fixes I ::"('a1::finite, 'b1::finite, 'c::finite) interp"
    and J ::"('a2::finite, 'b2::finite, 'c::finite) interp"
    and θ1 :: "('a1::finite, 'c::finite) trm"
    and θ2 :: "('a2::finite, 'c::finite) trm"
    and ν 
  assumes good_interp1:"is_interp I"
  assumes good_interp2:"is_interp J"
  assumes free1:"dfree θ1"
  assumes free2:"dfree θ2"
  assumes sem:"sterm_sem I θ1 = sterm_sem J θ2"
  shows "frechet I θ1 (fst ν) (snd ν) = frechet J θ2 (fst ν) (snd ν)"
proof -
  have d1:"(sterm_sem I θ1 has_derivative (frechet I θ1 (fst ν))) (at (fst ν))"
    using frechet_correctness[OF good_interp1 free1] by auto
  have d2:"(sterm_sem J θ2 has_derivative (frechet J θ2 (fst ν))) (at (fst ν))"
    using frechet_correctness[OF good_interp2 free2] by auto
  then have d1':"(sterm_sem I θ1 has_derivative (frechet J θ2 (fst ν))) (at (fst ν))"
    using sem by auto
  thus "?thesis" using has_derivative_unique d1 d1' by metis 
qed

lemma the_deriv:
  assumes deriv:"(f has_derivative F) (at x)"
  shows "(THE G. (f has_derivative G) (at x)) = F"
  apply(rule the_equality)
   subgoal by (rule deriv)
  subgoal for G by (auto simp add: deriv has_derivative_unique)
  done
   
lemma the_all_deriv:
  assumes deriv:"∀x. (f has_derivative F x) (at x)"
  shows "(THE G. ∀ x. (f has_derivative G x) (at x)) = F"
    apply(rule the_equality)
     subgoal by (rule deriv)
    subgoal for G 
      apply(rule ext)
      subgoal for x
        apply(erule allE[where x=x])
        by (auto simp add: deriv has_derivative_unique)
      done
    done
  
typedef ('a, 'c) strm = "{θ:: ('a,'c) trm. dfree θ}"
  morphisms raw_term simple_term
  by(rule exI[where x= "Const 0"], auto simp add: dfree_Const)
  
typedef ('a, 'b, 'c) good_interp = "{I::('a::finite,'b::finite,'c::finite) interp. is_interp I}"
  morphisms raw_interp good_interp
  apply(rule exI[where x="⦇ Functions = (λf x. 0), Predicates = (λp x. True), Contexts = (λC S. S), Programs = (λa. {}), ODEs = (λc v. (χ i. 0)), ODEBV = λc. {}⦈"])
  apply(auto simp add: is_interp_def)
proof -
  fix x ::real
  have eq:"(THE f'. ∀x. ((λx. 0) has_derivative f' x) (at x)) = (λ_ _. 0)"
    by(rule the_all_deriv, auto)
  have eq':"(THE f'. ∀x. ((λx. 0) has_derivative f' x) (at x)) x = (λ_. 0)"
    by (simp add: eq)
  have deriv:"((λx.0) has_derivative (λx. 0)) (at x)"
    by auto
  then show "⋀x. ((λx. 0) has_derivative (THE f'. ∀x. ((λx. 0) has_derivative f' x) (at x)) x) (at x)" 
    by (auto simp add: eq eq' deriv)
next
  have eq:"(THE f'. ∀x. ((λx. 0) has_derivative f' x) (at x)) = (λ_ _. 0)"
    by(rule the_all_deriv, auto)
  have eq':"∀x. (THE f'. ∀x. ((λx. 0) has_derivative f' x) (at x)) x = (λ_. 0)"
    by (simp add: eq)
  have deriv:"⋀x. ((λx.0) has_derivative (λx. 0)) (at x)"
    by auto
  have blin:"⋀x. bounded_linear ((THE f'. ∀x. ((λx. 0) has_derivative f' x) (at x)) x)"
    by (simp add: eq')
  show " continuous_on UNIV (λx. Blinfun ((THE f'. ∀x. ((λx. 0) has_derivative f' x) (at x)) x))"
    apply(clarsimp simp add: continuous_on_topological[of UNIV "(λx. Blinfun ((THE f'. ∀x. ((λx. 0) has_derivative f' x) (at x)) x))"])
    apply(rule exI[where x = UNIV])
    by(auto simp add: eq' blin)
 qed

lemma frechet_linear: 
  assumes good_interp:"is_interp I"
  fixes v θ
  shows " dfree θ ⟹ bounded_linear (frechet I θ v)"
proof(induction rule: dfree.induct)
  case (dfree_Var i)
  then show ?case by(auto)
next
  case (dfree_Const r)
  then show ?case by auto
next
  case (dfree_Fun args i)
  have blin1:"⋀x. bounded_linear(FunctionFrechet I i x)"
    using good_interp unfolding is_interp_def using has_derivative_bounded_linear
    by blast
  have blin2:"bounded_linear (λ a. (χ i. frechet I (args i) v a))"
    using dfree_Fun.IH by(rule bounded_linear_vec)
  then show ?case
    using bounded_linear_compose[of "FunctionFrechet I i (χ i. sterm_sem I (args i) v)" "(λa. (χ i. frechet I (args i) v a))", OF blin1 blin2]
    by auto
next
  case (dfree_Plus θ⇩1 θ⇩2)
  then show ?case 
    apply auto
    using bounded_linear_add by (blast)
next
  case (dfree_Times θ⇩1 θ⇩2)
  then show ?case
    by (auto simp add: bounded_linear_add bounded_linear_const_mult bounded_linear_mult_const)
qed

setup_lifting type_definition_good_interp

setup_lifting type_definition_strm

lift_definition blin_frechet::"('sf, 'sc, 'sz) good_interp ⇒ ('sf,'sz) strm ⇒ (real, 'sz) vec  ⇒ (real, 'sz) vec ⇒⇩L real" is "frechet"
  using frechet_linear by auto

lemmas [simp] = blin_frechet.rep_eq

lemma frechet_blin:"is_interp I ⟹ dfree θ ⟹ (λv. Blinfun (λv'. frechet I θ v v')) = blin_frechet (good_interp I) (simple_term θ)"
  apply(rule ext)
  apply(rule blinfun_eqI)
  by (simp add: bounded_linear_Blinfun_apply frechet_linear good_interp_inverse simple_term_inverse)

lemma sterm_continuous:
  assumes good_interp:"is_interp I"
  shows "dfree θ ⟹ continuous_on UNIV (sterm_sem I θ)"
proof(induction rule: dfree.induct)
  case (dfree_Fun args i)
  assume IH:"⋀i. continuous_on UNIV (sterm_sem I (args i))"
  have con1:"continuous_on UNIV (Functions I i)"
    using good_interp unfolding is_interp_def
    using continuous_on_eq_continuous_within has_derivative_continuous by blast
  have con2:"continuous_on UNIV (λ x. (χ i. sterm_sem I (args i) x))"
    apply(rule continuous_on_vec_lambda)
    using IH by auto
  have con:"continuous_on UNIV ((Functions I i) ∘ (λx.  (χ i. sterm_sem I (args i) x)))"
    apply(rule continuous_on_compose)
     using con1 con2 apply auto
    using continuous_on_subset by blast
  show ?case 
    using con comp_def by(simp)
qed (auto intro: continuous_intros)

lemma sterm_continuous':
  assumes good_interp:"is_interp I"
  shows "dfree θ ⟹ continuous_on S (sterm_sem I θ)"
  using sterm_continuous continuous_on_subset good_interp by blast

lemma frechet_continuous:
  fixes I :: "('sf, 'sc, 'sz) interp"
  assumes good_interp:"is_interp I"
  shows "dfree θ ⟹ continuous_on UNIV (blin_frechet (good_interp I) (simple_term θ))"    
proof (induction rule: dfree.induct)
  case (dfree_Var i)
  have free:"dfree (Var i)" by (rule dfree_Var)
  have bounded_linear:"bounded_linear (λ ν'. ν' ∙ axis i 1)"
    by (auto simp add: bounded_linear_vec_nth)
  have cont:"continuous_on UNIV (λν. Blinfun(λ ν'. ν' ∙ axis i 1))"
    using continuous_on_const by blast
  have eq:"⋀ν ν'. (λν. Blinfun(λ ν'. ν' ∙ axis i 1)) ν ν' = (blin_frechet (good_interp I) (simple_term (Var i))) ν ν'"
    unfolding axis_def apply(auto)
    by (metis (no_types) axis_def blinfun_inner_left.abs_eq blinfun_inner_left.rep_eq dfree_Var_simps frechet.simps(1) mem_Collect_eq simple_term_inverse)
  have eq':"(λν. Blinfun(λ ν'. ν' ∙ axis i 1)) = (blin_frechet (good_interp I) (simple_term (Var i)))"
    apply(rule ext)
    apply(rule blinfun_eqI)
    using eq by auto
  then show ?case by (metis cont)
next
  case (dfree_Const r)
  have free:"dfree (Const r)" by (rule dfree_Const)
  have bounded_linear:"bounded_linear (λ ν'. 0)" by (simp)
  have cont:"continuous_on UNIV (λν. Blinfun(λ ν'. 0))"
    using continuous_on_const by blast
  have eq':"(λν. Blinfun(λ ν'. 0)) = (blin_frechet (good_interp I) (simple_term (Const r)))"
    apply(rule ext)
    apply(rule blinfun_eqI)
    apply auto
    using zero_blinfun.abs_eq zero_blinfun.rep_eq free
    by (metis frechet.simps(5) mem_Collect_eq simple_term_inverse)
  then show ?case by (metis cont)
next
  case (dfree_Fun args f)
  assume IH:"⋀i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args i)))"
  assume frees:"(⋀i. dfree (args i))"
  then have free:"dfree ($f f args)" by (auto)
  have great_interp:"⋀f. continuous_on UNIV (λx. Blinfun (FunctionFrechet I f x))" using good_interp unfolding is_interp_def by auto
  have cont1:"⋀v. continuous_on UNIV (λv'. (χ i. frechet I (args i) v v'))"
    apply(rule continuous_on_vec_lambda)
    using IH by (simp add: frechet_linear frees good_interp linear_continuous_on)
  have eq:"(λv. Blinfun(λv'. FunctionFrechet I f (χ i. sterm_sem I (args i) v) (χ i. frechet I (args i) v v'))) 
    = (blin_frechet (good_interp I) (simple_term (Function f args)))"
    using frechet_blin[OF good_interp free] by auto
  have bounded_linears:"⋀x. bounded_linear (FunctionFrechet I f x)" using good_interp unfolding is_interp_def by blast
  let ?blin_ff ="(λx. Blinfun (FunctionFrechet I f x))" 
  have some_eq:"(λx. Blinfun (FunctionFrechet I f (χ i. sterm_sem I (args i) x))) = 
                ((?blin_ff) ∘ (λx. (χ i. sterm_sem I (args i) x)))"
    apply(rule ext)
    apply(rule blinfun_eqI)
    unfolding comp_def by blast
  have sub_cont:"continuous_on UNIV ((?blin_ff) ∘ (λx. (χ i. sterm_sem I (args i) x)))"
    apply(rule continuous_intros)+
     apply (simp add: frees good_interp sterm_continuous')
    using continuous_on_subset great_interp by blast
  have blin_frech_vec:"⋀x. bounded_linear (λv'. χ i. frechet I (args i) x v')" 
    by (simp add: bounded_linear_vec frechet_linear frees good_interp)
  have frech_vec_eq:"(λx. Blinfun (λv'. χ i. frechet I (args i) x v')) = (λx. blinfun_vec (λ i. blin_frechet (good_interp I) (simple_term (args i)) x))"
    apply(rule ext)
    apply(rule blinfun_eqI)
    apply(rule vec_extensionality)
    subgoal for x i j
      using blin_frech_vec[of x]
      apply auto
      by (metis (no_types, lifting) blin_frechet.rep_eq bounded_linear_Blinfun_apply frechet_blin frechet_linear frees good_interp vec_lambda_beta)
    done
  have cont_frech_vec:"continuous_on UNIV (λx. blinfun_vec (λ i. blin_frechet (good_interp I) (simple_term (args i)) x))"
    apply(rule continuous_blinfun_vec')
    using IH by blast
  have cont_intro:"⋀ s f g. continuous_on s f ⟹ continuous_on s g ⟹ continuous_on s (λx. f x o⇩L g x)"
    by (auto intro: continuous_intros)
  have cont:"continuous_on UNIV (λv. blinfun_compose (Blinfun (FunctionFrechet I f (χ i. sterm_sem I (args i) v))) (Blinfun(λv'.  (χ i. frechet I (args i) v v'))))"
    apply(rule cont_intro)
     subgoal using  sub_cont by simp
    using frech_vec_eq cont_frech_vec by presburger
  have best_eq:"(blin_frechet (good_interp I) (simple_term ($f f args))) = (λv. blinfun_compose (Blinfun (FunctionFrechet I f (χ i. sterm_sem I (args i) v))) (Blinfun(λv'.  (χ i. frechet I (args i) v v')))) "
    apply(rule ext)
    apply(rule blinfun_eqI)
  proof -
    fix v :: "(real, 'sz) vec" and i :: "(real, 'sz) vec"
    have "frechet I ($f f args) v i = blinfun_apply (blin_frechet (good_interp I) (simple_term ($f f args)) v) i"
      by (metis (no_types) bounded_linear_Blinfun_apply dfree_Fun_simps frechet_blin frechet_linear frees good_interp)
    then have "FunctionFrechet I f (χ s. sterm_sem I (args s) v) (blinfun_apply (Blinfun (λva. χ s. frechet I (args s) v va)) i) = blinfun_apply (blin_frechet (good_interp I) (simple_term ($f f args)) v) i"
      by (simp add: blin_frech_vec bounded_linear_Blinfun_apply)
    then show "blinfun_apply (blin_frechet (good_interp I) (simple_term ($f f args)) v) i = blinfun_apply (Blinfun (FunctionFrechet I f (χ s. sterm_sem I (args s) v)) o⇩L Blinfun (λva. χ s. frechet I (args s) v va)) i"
      by (metis (no_types) blinfun_apply_blinfun_compose bounded_linear_Blinfun_apply bounded_linears)
  qed
  then show ?case using cont best_eq by auto
next
  case (dfree_Plus θ⇩1 θ⇩2)
  assume IH1:"continuous_on UNIV (blin_frechet (good_interp I) (simple_term θ⇩1))"
  assume IH2:"continuous_on UNIV (blin_frechet (good_interp I) (simple_term θ⇩2))"
  assume free1:"dfree θ⇩1"
  assume free2:"dfree θ⇩2"
  have free:"dfree (Plus θ⇩1 θ⇩2)" using free1 free2 by auto 
  have bounded_linear:"⋀v. bounded_linear (λv'. frechet I θ⇩1 v v' + frechet I θ⇩2 v v')" 
    subgoal for v
      using frechet_linear[OF good_interp free] by auto
    done
  have eq2:"(λv. blin_frechet (good_interp I) (simple_term θ⇩1) v + blin_frechet (good_interp I) (simple_term θ⇩2) v) = blin_frechet (good_interp I) (simple_term (Plus θ⇩1 θ⇩2))"
    apply(rule ext)
    apply(rule blinfun_eqI)
    by (simp add: blinfun.add_left free1 free2 simple_term_inverse) 
  have cont:"continuous_on UNIV (λv. blin_frechet (good_interp I) (simple_term θ⇩1) v + blin_frechet (good_interp I) (simple_term θ⇩2) v)"
    using continuous_on_add dfree_Plus.IH(1) dfree_Plus.IH(2) by blast 
  then show ?case using cont eq2 by metis 
next
  case (dfree_Times θ⇩1 θ⇩2)
  assume IH1:"continuous_on UNIV (blin_frechet (good_interp I) (simple_term θ⇩1))"
  assume IH2:"continuous_on UNIV (blin_frechet (good_interp I) (simple_term θ⇩2))"
  assume free1:"dfree θ⇩1"
  assume free2:"dfree θ⇩2"
  have free:"dfree (Times θ⇩1 θ⇩2)" using free1 free2 by auto 
  have bounded_linear:"⋀v. bounded_linear (λv'. sterm_sem I θ⇩1 v * frechet I θ⇩2 v v' + frechet I θ⇩1 v v' * sterm_sem I θ⇩2 v)"
    apply(rule bounded_linear_add)
    apply(rule bounded_linear_const_mult)
    using frechet_linear[OF good_interp free2] apply auto
    apply(rule bounded_linear_mult_const)
    using frechet_linear[OF good_interp free1] by auto
  then have blin':"⋀v. (λv'. sterm_sem I θ⇩1 v * frechet I θ⇩2 v v' + frechet I θ⇩1 v v' * sterm_sem I θ⇩2 v) ∈ {f. bounded_linear f}" by auto
  have blinfun_eq:"⋀v. Blinfun (λv'. sterm_sem I θ⇩1 v * frechet I θ⇩2 v v' + frechet I θ⇩1 v v' * sterm_sem I θ⇩2 v) 
    =  scaleR (sterm_sem I θ⇩1 v) (blin_frechet (good_interp I) (simple_term θ⇩2) v) + scaleR (sterm_sem I θ⇩2 v) (blin_frechet (good_interp I) (simple_term θ⇩1) v)"
    apply(rule blinfun_eqI)
    subgoal for v i
      using Blinfun_inverse[OF blin', of v] apply auto
      using blinfun.add_left[of "sterm_sem I θ⇩1 v *⇩R blin_frechet (good_interp I) (simple_term θ⇩2) v" "sterm_sem I θ⇩2 v *⇩R blin_frechet (good_interp I) (simple_term θ⇩1) v"]
        blinfun.scaleR_left[of "sterm_sem I θ⇩1 v" "blin_frechet (good_interp I) (simple_term θ⇩2) v"]
        blinfun.scaleR_left[of "sterm_sem I θ⇩2 v" "blin_frechet (good_interp I) (simple_term θ⇩1) v"]
        bounded_linear_Blinfun_apply
        frechet_blin[OF good_interp free1]
        frechet_blin[OF good_interp free2]
        frechet_linear[OF good_interp free1]
        frechet_linear[OF good_interp free2]
        mult.commute 
        real_scaleR_def
    proof -
      have f1: "⋀v. blinfun_apply (blin_frechet (good_interp I) (simple_term θ⇩1) v) = frechet I θ⇩1 v"
        by (metis (no_types) ‹(λv. Blinfun (frechet I θ⇩1 v)) = blin_frechet (good_interp I) (simple_term θ⇩1)› ‹⋀v. bounded_linear (frechet I θ⇩1 v)› bounded_linear_Blinfun_apply)
      have "⋀v. blinfun_apply (blin_frechet (good_interp I) (simple_term θ⇩2) v) = frechet I θ⇩2 v"
      by (metis (no_types) ‹(λv. Blinfun (frechet I θ⇩2 v)) = blin_frechet (good_interp I) (simple_term θ⇩2)› ‹⋀v. bounded_linear (frechet I θ⇩2 v)› bounded_linear_Blinfun_apply)
      then show "sterm_sem I θ⇩1 v * frechet I θ⇩2 v i + frechet I θ⇩1 v i * sterm_sem I θ⇩2 v = blinfun_apply (sterm_sem I θ⇩1 v *⇩R blin_frechet (good_interp I) (simple_term θ⇩2) v + sterm_sem I θ⇩2 v *⇩R blin_frechet (good_interp I) (simple_term θ⇩1) v) i"
        using f1 by (simp add: ‹⋀b. blinfun_apply (sterm_sem I θ⇩1 v *⇩R blin_frechet (good_interp I) (simple_term θ⇩2) v + sterm_sem I θ⇩2 v *⇩R blin_frechet (good_interp I) (simple_term θ⇩1) v) b = blinfun_apply (sterm_sem I θ⇩1 v *⇩R blin_frechet (good_interp I) (simple_term θ⇩2) v) b + blinfun_apply (sterm_sem I θ⇩2 v *⇩R blin_frechet (good_interp I) (simple_term θ⇩1) v) b› ‹⋀b. blinfun_apply (sterm_sem I θ⇩1 v *⇩R blin_frechet (good_interp I) (simple_term θ⇩2) v) b = sterm_sem I θ⇩1 v *⇩R blinfun_apply (blin_frechet (good_interp I) (simple_term θ⇩2) v) b› ‹⋀b. blinfun_apply (sterm_sem I θ⇩2 v *⇩R blin_frechet (good_interp I) (simple_term θ⇩1) v) b = sterm_sem I θ⇩2 v *⇩R blinfun_apply (blin_frechet (good_interp I) (simple_term θ⇩1) v) b›)
    qed        
    done
  have cont':"continuous_on UNIV 
    (λv. scaleR (sterm_sem I θ⇩1 v) (blin_frechet (good_interp I) (simple_term θ⇩2) v) 
       + scaleR (sterm_sem I θ⇩2 v) (blin_frechet (good_interp I) (simple_term θ⇩1) v))"
    apply(rule continuous_on_add)
     apply(rule continuous_on_scaleR)
      apply(rule sterm_continuous[OF good_interp free1])
     apply(rule IH2)
    apply(rule continuous_on_scaleR)
     apply(rule sterm_continuous[OF good_interp free2])
    by(rule IH1)
  have cont:"continuous_on UNIV (λv. Blinfun (λv'. sterm_sem I θ⇩1 v * frechet I θ⇩2 v v' + frechet I θ⇩1 v v' * sterm_sem I θ⇩2 v))"
    using cont' blinfun_eq by auto
  have eq:"(λv. Blinfun (λv'. sterm_sem I θ⇩1 v * frechet I θ⇩2 v v' + frechet I θ⇩1 v v' * sterm_sem I θ⇩2 v)) = blin_frechet (good_interp I) (simple_term (Times θ⇩1 θ⇩2))"
    using frechet_blin[OF good_interp free]
    by auto
  then show ?case by (metis cont)
qed
end end