Theory USubst

theory "USubst"
imports
  Ordinary_Differential_Equations.ODE_Analysis
  "Ids"
  "Lib"
  "Syntax"
  "Denotational_Semantics"
  "Static_Semantics"
begin 
section ‹Uniform Substitution Definitions›
text‹This section defines substitutions and implements the substitution operation.
  Every part of substitution comes in two flavors. The "Nsubst" variant of each function
  returns a term/formula/ode/program which (as encoded in the type system) has less symbols
  that the input. We use this operation when substitution into functions and function-like
  constructs to make it easy to distinguish identifiers that stand for arguments to functions
  from other identifiers. In order to expose a simpler interface, we also have a "subst" variant
  which does not delete variables.
  
  Naive substitution without side conditions would not always be sound. The various admissibility 
  predicates *admit describe conditions under which the various substitution operations are sound.
  ›

text‹ 
Explicit data structure for substitutions.

The RHS of a function or predicate substitution is a term or formula
with extra variables, which are used to refer to arguments. ›
record ('a, 'b, 'c) subst =
  SFunctions       :: "'a ⇀ ('a + 'c, 'c) trm"
  SPredicates      :: "'c ⇀ ('a + 'c, 'b, 'c) formula"
  SContexts        :: "'b ⇀ ('a, 'b + unit, 'c) formula"
  SPrograms        :: "'c ⇀ ('a, 'b, 'c) hp"
  SODEs            :: "'c ⇀ ('a, 'c) ODE"

context ids begin
definition NTUadmit :: "('d ⇒ ('a, 'c) trm) ⇒ ('a + 'd, 'c) trm ⇒ ('c + 'c) set ⇒ bool"
where "NTUadmit σ θ U ⟷ ((⋃ i ∈ {i. Inr i ∈ SIGT θ}. FVT (σ i)) ∩ U) = {}"

inductive TadmitFFO :: "('d ⇒ ('a, 'c) trm) ⇒ ('a + 'd, 'c) trm ⇒ bool"
where 
  TadmitFFO_Diff:"TadmitFFO σ θ ⟹ NTUadmit σ θ UNIV ⟹ TadmitFFO σ (Differential θ)"
| TadmitFFO_Fun1:"(⋀i. TadmitFFO σ (args i)) ⟹ TadmitFFO σ (Function (Inl f) args)"
| TadmitFFO_Fun2:"(⋀i. TadmitFFO σ (args i)) ⟹ dfree (σ f) ⟹ TadmitFFO σ (Function (Inr f) args)"
| TadmitFFO_Plus:"TadmitFFO σ θ1 ⟹ TadmitFFO σ θ2 ⟹ TadmitFFO σ (Plus θ1 θ2)"
| TadmitFFO_Times:"TadmitFFO σ θ1 ⟹ TadmitFFO σ θ2 ⟹ TadmitFFO σ (Times θ1 θ2)"
| TadmitFFO_Var:"TadmitFFO σ (Var x)"
| TadmitFFO_Const:"TadmitFFO σ (Const r)"

inductive_simps
  TadmitFFO_Diff_simps[simp]: "TadmitFFO σ (Differential θ)"
and TadmitFFO_Fun_simps[simp]: "TadmitFFO σ (Function f args)"
and TadmitFFO_Plus_simps[simp]: "TadmitFFO σ (Plus t1 t2)"
and TadmitFFO_Times_simps[simp]: "TadmitFFO σ (Times t1 t2)"
and TadmitFFO_Var_simps[simp]: "TadmitFFO σ (Var x)"
and TadmitFFO_Const_simps[simp]: "TadmitFFO σ (Const r)"
  
primrec TsubstFO::"('a + 'b, 'c) trm ⇒ ('b ⇒ ('a, 'c) trm) ⇒ ('a, 'c) trm"
where
  "TsubstFO (Var v) σ = Var v"
| "TsubstFO (DiffVar v) σ = DiffVar v"
| "TsubstFO (Const r) σ = Const r"  
| "TsubstFO (Function f args) σ =
    (case f of 
      Inl f' ⇒ Function f' (λ i. TsubstFO (args i) σ) 
    | Inr f' ⇒ σ f')"  
| "TsubstFO (Plus θ1 θ2) σ = Plus (TsubstFO θ1 σ) (TsubstFO θ2 σ)"  
| "TsubstFO (Times θ1 θ2) σ = Times (TsubstFO θ1 σ) (TsubstFO θ2 σ)"  
| "TsubstFO (Differential θ) σ = Differential (TsubstFO θ σ)"

inductive TadmitFO :: "('d ⇒ ('a, 'c) trm) ⇒ ('a + 'd, 'c) trm ⇒ bool"
where 
  TadmitFO_Diff:"TadmitFFO σ θ ⟹ NTUadmit σ θ UNIV ⟹ dfree (TsubstFO θ σ) ⟹ TadmitFO σ (Differential θ)"
| TadmitFO_Fun:"(⋀i. TadmitFO σ (args i)) ⟹ TadmitFO σ (Function f args)"
| TadmitFO_Plus:"TadmitFO σ θ1 ⟹ TadmitFO σ θ2 ⟹ TadmitFO σ (Plus θ1 θ2)"
| TadmitFO_Times:"TadmitFO σ θ1 ⟹ TadmitFO σ θ2 ⟹ TadmitFO σ (Times θ1 θ2)"
| TadmitFO_DiffVar:"TadmitFO σ (DiffVar x)"
| TadmitFO_Var:"TadmitFO σ (Var x)"
| TadmitFO_Const:"TadmitFO σ (Const r)"

inductive_simps
      TadmitFO_Plus_simps[simp]: "TadmitFO σ (Plus a b)"
  and TadmitFO_Times_simps[simp]: "TadmitFO σ (Times a b)"
  and TadmitFO_Var_simps[simp]: "TadmitFO σ (Var x)"
  and TadmitFO_DiffVar_simps[simp]: "TadmitFO σ (DiffVar x)"
  and TadmitFO_Differential_simps[simp]: "TadmitFO σ (Differential θ)"
  and TadmitFO_Const_simps[simp]: "TadmitFO σ (Const r)"
  and TadmitFO_Fun_simps[simp]: "TadmitFO σ (Function i args)"

primrec Tsubst::"('a, 'c) trm ⇒ ('a, 'b, 'c) subst ⇒ ('a, 'c) trm"
where
  "Tsubst (Var x) σ = Var x"
| "Tsubst (DiffVar x) σ = DiffVar x"  
| "Tsubst (Const r) σ = Const r"  
| "Tsubst (Function f args) σ = (case SFunctions σ f of Some f' ⇒ TsubstFO f' | None ⇒ Function f) (λ i. Tsubst (args i) σ)"  
| "Tsubst (Plus θ1 θ2) σ = Plus (Tsubst θ1 σ) (Tsubst θ2 σ)"  
| "Tsubst (Times θ1 θ2) σ = Times (Tsubst θ1 σ) (Tsubst θ2 σ)"  
| "Tsubst (Differential θ) σ = Differential (Tsubst θ σ)"
  
primrec OsubstFO::"('a + 'b, 'c) ODE ⇒ ('b ⇒ ('a, 'c) trm) ⇒ ('a, 'c) ODE"
where
  "OsubstFO (OVar c) σ = OVar c"
| "OsubstFO (OSing x θ) σ = OSing x (TsubstFO θ σ)"
| "OsubstFO (OProd ODE1 ODE2) σ = OProd (OsubstFO ODE1 σ) (OsubstFO ODE2 σ)"

primrec Osubst::"('a, 'c) ODE ⇒ ('a, 'b, 'c) subst ⇒ ('a, 'c) ODE"
where
  "Osubst (OVar c) σ = (case SODEs σ c of Some c' ⇒ c' | None ⇒ OVar c)"
| "Osubst (OSing x θ) σ = OSing x (Tsubst θ σ)"
| "Osubst (OProd ODE1 ODE2) σ = OProd (Osubst ODE1 σ) (Osubst ODE2 σ)"
  
fun PsubstFO::"('a + 'd, 'b, 'c) hp ⇒ ('d ⇒ ('a, 'c) trm) ⇒ ('a, 'b, 'c) hp"
and FsubstFO::"('a + 'd, 'b, 'c) formula ⇒ ('d ⇒ ('a, 'c) trm) ⇒ ('a, 'b, 'c) formula"
where
  "PsubstFO (Pvar a) σ = Pvar a"
| "PsubstFO (Assign x θ) σ = Assign x (TsubstFO θ σ)"
| "PsubstFO (DiffAssign x θ) σ = DiffAssign x (TsubstFO θ σ)"
| "PsubstFO (Test φ) σ = Test (FsubstFO φ σ)"
| "PsubstFO (EvolveODE ODE φ) σ = EvolveODE (OsubstFO ODE σ) (FsubstFO φ σ)"
| "PsubstFO (Choice α β) σ = Choice (PsubstFO α σ) (PsubstFO β σ)"
| "PsubstFO (Sequence α β) σ = Sequence (PsubstFO α σ) (PsubstFO β σ)"
| "PsubstFO (Loop α) σ = Loop (PsubstFO α σ)"

| "FsubstFO (Geq θ1 θ2) σ = Geq (TsubstFO θ1 σ) (TsubstFO θ2 σ)"
| "FsubstFO (Prop p args) σ = Prop p (λi. TsubstFO (args i) σ)"
| "FsubstFO (Not φ) σ = Not (FsubstFO φ σ)"
| "FsubstFO (And φ ψ) σ = And (FsubstFO φ σ) (FsubstFO ψ σ)"
| "FsubstFO (Exists x φ) σ = Exists x (FsubstFO φ σ)"
| "FsubstFO (Diamond α φ) σ = Diamond (PsubstFO α σ) (FsubstFO φ σ)"
| "FsubstFO (InContext C φ) σ = InContext C (FsubstFO φ σ)"
  
fun PPsubst::"('a, 'b + 'd, 'c) hp ⇒ ('d ⇒ ('a, 'b, 'c) formula) ⇒ ('a, 'b, 'c) hp"
and PFsubst::"('a, 'b + 'd, 'c) formula ⇒ ('d ⇒ ('a, 'b, 'c) formula) ⇒ ('a, 'b, 'c) formula"
where
  "PPsubst (Pvar a) σ = Pvar a"
| "PPsubst (Assign x θ) σ = Assign x θ"
| "PPsubst (DiffAssign x θ) σ = DiffAssign x θ"
| "PPsubst (Test φ) σ = Test (PFsubst φ σ)"
| "PPsubst (EvolveODE ODE φ) σ = EvolveODE ODE (PFsubst φ σ)"
| "PPsubst (Choice α β) σ = Choice (PPsubst α σ) (PPsubst β σ)"
| "PPsubst (Sequence α β) σ = Sequence (PPsubst α σ) (PPsubst β σ)"
| "PPsubst (Loop α) σ = Loop (PPsubst α σ)"

| "PFsubst (Geq θ1 θ2) σ = (Geq θ1 θ2)"
| "PFsubst (Prop p args) σ = Prop p args"
| "PFsubst (Not φ) σ = Not (PFsubst φ σ)"
| "PFsubst (And φ ψ) σ = And (PFsubst φ σ) (PFsubst ψ σ)"
| "PFsubst (Exists x φ) σ = Exists x (PFsubst φ σ)"
| "PFsubst (Diamond α φ) σ = Diamond (PPsubst α σ) (PFsubst φ σ)"
| "PFsubst (InContext C φ) σ = (case C of Inl C' ⇒ InContext C' (PFsubst φ σ) | Inr p' ⇒ σ p')"

  
fun Psubst::"('a, 'b, 'c) hp ⇒ ('a, 'b, 'c) subst ⇒ ('a, 'b, 'c) hp"
and Fsubst::"('a, 'b, 'c) formula ⇒ ('a, 'b, 'c) subst ⇒ ('a, 'b, 'c) formula"
where
  "Psubst (Pvar a) σ = (case SPrograms σ a of Some a' ⇒ a' | None ⇒ Pvar a)"
| "Psubst (Assign x θ) σ = Assign x (Tsubst θ σ)"
| "Psubst (DiffAssign x θ) σ = DiffAssign x (Tsubst θ σ)"
| "Psubst (Test φ) σ = Test (Fsubst φ σ)"
| "Psubst (EvolveODE ODE φ) σ = EvolveODE (Osubst ODE σ) (Fsubst φ σ)"
| "Psubst (Choice α β) σ = Choice (Psubst α σ) (Psubst β σ)"
| "Psubst (Sequence α β) σ = Sequence (Psubst α σ) (Psubst β σ)"
| "Psubst (Loop α) σ = Loop (Psubst α σ)"

| "Fsubst (Geq θ1 θ2) σ = Geq (Tsubst θ1 σ) (Tsubst θ2 σ)"
| "Fsubst (Prop p args) σ = (case SPredicates σ p of Some p' ⇒ FsubstFO p' (λi. Tsubst (args i) σ) | None ⇒ Prop p (λi. Tsubst (args i) σ))"
| "Fsubst (Not φ) σ = Not (Fsubst φ σ)"
| "Fsubst (And φ ψ) σ = And (Fsubst φ σ) (Fsubst ψ σ)"
| "Fsubst (Exists x φ) σ = Exists x (Fsubst φ σ)"
| "Fsubst (Diamond α φ) σ = Diamond (Psubst α σ) (Fsubst φ σ)"
| "Fsubst (InContext C φ) σ = (case SContexts σ C of Some C' ⇒ PFsubst C' (λ _. (Fsubst φ σ)) | None ⇒  InContext C (Fsubst φ σ))"

definition FVA :: "('a ⇒ ('a, 'c) trm) ⇒ ('c + 'c) set"
where "FVA args = (⋃ i. FVT (args i))"

fun SFV :: "('a, 'b, 'c) subst ⇒ ('a + 'b + 'c) ⇒ ('c + 'c) set"
where "SFV σ (Inl i) = (case SFunctions σ i of Some f' ⇒ FVT f' | None ⇒ {})"
| "SFV σ (Inr (Inl i)) = {}"
| "SFV σ (Inr (Inr i)) = (case SPredicates σ i of Some p' ⇒ FVF p' | None ⇒ {})"

definition FVS :: "('a, 'b, 'c) subst ⇒ ('c + 'c) set"
where "FVS σ = (⋃i. SFV σ i)"

definition SDom :: "('a, 'b, 'c) subst ⇒ ('a + 'b + 'c) set"
where "SDom σ = 
 {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 σ)}"

definition TUadmit :: "('a, 'b, 'c) subst ⇒ ('a, 'c) trm ⇒ ('c + 'c) set ⇒ bool"
where "TUadmit σ θ U ⟷ ((⋃ i ∈ SIGT θ. (case SFunctions σ i of Some f' ⇒ FVT f'  | None ⇒ {})) ∩ U) = {}"

inductive Tadmit :: "('a, 'b, 'c) subst ⇒ ('a, 'c) trm ⇒ bool"
where 
  Tadmit_Diff:"Tadmit σ θ ⟹ TUadmit σ θ UNIV ⟹ Tadmit σ (Differential θ)"
| Tadmit_Fun1:"(⋀i. Tadmit σ (args i)) ⟹ SFunctions σ f = Some f' ⟹ TadmitFO (λ i. Tsubst (args i) σ) f' ⟹ Tadmit σ (Function f args)"
| Tadmit_Fun2:"(⋀i. Tadmit σ (args i)) ⟹ SFunctions σ f = None ⟹ Tadmit σ (Function f args)"
| Tadmit_Plus:"Tadmit σ θ1 ⟹ Tadmit σ θ2 ⟹ Tadmit σ (Plus θ1 θ2)"
| Tadmit_Times:"Tadmit σ θ1 ⟹ Tadmit σ θ2 ⟹ Tadmit σ (Times θ1 θ2)"
| Tadmit_DiffVar:"Tadmit σ (DiffVar x)"
| Tadmit_Var:"Tadmit σ (Var x)"
| Tadmit_Const:"Tadmit σ (Const r)"

inductive_simps
      Tadmit_Plus_simps[simp]: "Tadmit σ (Plus a b)"
  and Tadmit_Times_simps[simp]: "Tadmit σ (Times a b)"
  and Tadmit_Var_simps[simp]: "Tadmit σ (Var x)"
  and Tadmit_DiffVar_simps[simp]: "Tadmit σ (DiffVar x)"
  and Tadmit_Differential_simps[simp]: "Tadmit σ (Differential θ)"
  and Tadmit_Const_simps[simp]: "Tadmit σ (Const r)"
  and Tadmit_Fun_simps[simp]: "Tadmit σ (Function i args)"

inductive TadmitF :: "('a, 'b, 'c) subst ⇒ ('a, 'c) trm ⇒ bool"
where 
  TadmitF_Diff:"TadmitF σ θ ⟹ TUadmit σ θ UNIV ⟹ TadmitF σ (Differential θ)"
| TadmitF_Fun1:"(⋀i. TadmitF σ (args i)) ⟹ SFunctions σ f = Some f' ⟹ (⋀i. dfree (Tsubst (args i) σ)) ⟹ TadmitFFO (λ i. Tsubst (args i) σ) f' ⟹ TadmitF σ (Function f args)"
| TadmitF_Fun2:"(⋀i. TadmitF σ (args i)) ⟹ SFunctions σ f = None ⟹ TadmitF σ (Function f args)"
| TadmitF_Plus:"TadmitF σ θ1 ⟹ TadmitF σ θ2 ⟹ TadmitF σ (Plus θ1 θ2)"
| TadmitF_Times:"TadmitF σ θ1 ⟹ TadmitF σ θ2 ⟹ TadmitF σ (Times θ1 θ2)"
| TadmitF_DiffVar:"TadmitF σ (DiffVar x)"
| TadmitF_Var:"TadmitF σ (Var x)"
| TadmitF_Const:"TadmitF σ (Const r)"

inductive_simps
      TadmitF_Plus_simps[simp]: "TadmitF σ (Plus a b)"
  and TadmitF_Times_simps[simp]: "TadmitF σ (Times a b)"
  and TadmitF_Var_simps[simp]: "TadmitF σ (Var x)"
  and TadmitF_DiffVar_simps[simp]: "TadmitF σ (DiffVar x)"
  and TadmitF_Differential_simps[simp]: "TadmitF σ (Differential θ)"
  and TadmitF_Const_simps[simp]: "TadmitF σ (Const r)"
  and TadmitF_Fun_simps[simp]: "TadmitF σ (Function i args)"

inductive Oadmit:: "('a, 'b, 'c) subst ⇒ ('a, 'c) ODE ⇒ ('c + 'c) set ⇒ bool"
where 
  Oadmit_Var:"Oadmit σ (OVar c) U"
| Oadmit_Sing:"TUadmit σ θ U ⟹ TadmitF σ θ ⟹ Oadmit σ (OSing x θ) U"
| Oadmit_Prod:"Oadmit σ ODE1 U ⟹ Oadmit σ ODE2 U ⟹ ODE_dom (Osubst ODE1 σ) ∩ ODE_dom (Osubst ODE2 σ) = {} ⟹ Oadmit σ (OProd ODE1 ODE2) U"

inductive_simps
      Oadmit_Var_simps[simp]: "Oadmit σ (OVar c) U"
  and Oadmit_Sing_simps[simp]: "Oadmit σ (OSing x e) U"
  and Oadmit_Prod_simps[simp]: "Oadmit σ (OProd ODE1 ODE2) U"

definition PUadmit :: "('a, 'b, 'c) subst ⇒ ('a, 'b, 'c) hp ⇒ ('c + 'c) set ⇒ bool"
where "PUadmit σ θ U ⟷ ((⋃ i ∈ (SDom σ ∩ SIGP θ).  SFV σ i) ∩ U) = {}"

definition FUadmit :: "('a, 'b, 'c) subst ⇒ ('a, 'b, 'c) formula ⇒ ('c + 'c) set ⇒ bool"
where "FUadmit σ θ U ⟷ ((⋃ i ∈ (SDom σ ∩ SIGF θ).  SFV σ i) ∩ U) = {}"

definition OUadmitFO :: "('d ⇒ ('a, 'c) trm) ⇒ ('a + 'd,  'c) ODE ⇒ ('c + 'c) set ⇒ bool"
where "OUadmitFO σ θ U ⟷ ((⋃ i ∈ {i. Inl (Inr i) ∈ SIGO θ}. FVT (σ i)) ∩ U) = {}"
 
inductive OadmitFO :: "('d ⇒ ('a, 'c) trm) ⇒ ('a + 'd,  'c) ODE ⇒ ('c + 'c) set ⇒ bool"
where 
  OadmitFO_OVar:"OUadmitFO σ (OVar c) U ⟹ OadmitFO σ (OVar c) U"
| OadmitFO_OSing:"OUadmitFO σ (OSing x θ) U ⟹ TadmitFFO σ θ ⟹ OadmitFO σ (OSing x θ) U"
| OadmitFO_OProd:"OadmitFO σ ODE1 U ⟹ OadmitFO σ ODE2 U ⟹ OadmitFO σ (OProd ODE1 ODE2) U"

inductive_simps
      OadmitFO_OVar_simps[simp]: "OadmitFO σ (OVar a) U"
  and OadmitFO_OProd_simps[simp]: "OadmitFO σ (OProd ODE1 ODE2) U"
  and OadmitFO_OSing_simps[simp]: "OadmitFO σ (OSing x e) U"
  
definition FUadmitFO :: "('d ⇒ ('a, 'c) trm) ⇒ ('a + 'd, 'b, 'c) formula ⇒ ('c + 'c) set ⇒ bool"
where "FUadmitFO σ θ U ⟷ ((⋃ i ∈ {i. Inl (Inr i) ∈ SIGF θ}. FVT (σ i)) ∩ U) = {}"

definition PUadmitFO :: "('d ⇒ ('a, 'c) trm) ⇒ ('a + 'd, 'b, 'c) hp ⇒ ('c + 'c) set ⇒ bool"
where "PUadmitFO σ θ U ⟷ ((⋃ i  ∈ {i. Inl (Inr i) ∈ SIGP θ}. FVT (σ i)) ∩ U) = {}"

inductive NPadmit :: "('d ⇒ ('a, 'c) trm) ⇒ ('a + 'd, 'b, 'c) hp ⇒ bool" 
and NFadmit :: "('d ⇒ ('a, 'c) trm) ⇒ ('a + 'd, 'b, 'c) formula ⇒ bool"
where
  NPadmit_Pvar:"NPadmit σ (Pvar a)"
| NPadmit_Sequence:"NPadmit σ a ⟹ NPadmit σ b ⟹ PUadmitFO σ b (BVP (PsubstFO a σ))⟹ hpsafe (PsubstFO a σ) ⟹ NPadmit σ (Sequence a b)"  
| NPadmit_Loop:"NPadmit σ a ⟹ PUadmitFO σ a (BVP (PsubstFO a σ)) ⟹ hpsafe (PsubstFO a σ) ⟹ NPadmit σ (Loop a)"        
| NPadmit_ODE:"OadmitFO σ ODE (BVO ODE) ⟹ NFadmit σ φ ⟹ FUadmitFO σ φ (BVO ODE) ⟹ fsafe (FsubstFO φ σ) ⟹ osafe (OsubstFO ODE σ) ⟹ NPadmit σ (EvolveODE ODE φ)"
| NPadmit_Choice:"NPadmit σ a ⟹ NPadmit σ b ⟹ NPadmit σ (Choice a b)"            
| NPadmit_Assign:"TadmitFO σ θ ⟹ NPadmit σ (Assign x θ)"  
| NPadmit_DiffAssign:"TadmitFO σ θ ⟹ NPadmit σ (DiffAssign x θ)"  
| NPadmit_Test:"NFadmit σ φ ⟹ NPadmit σ (Test φ)"

| NFadmit_Geq:"TadmitFO σ θ1 ⟹ TadmitFO σ θ2 ⟹ NFadmit σ (Geq θ1 θ2)"
| NFadmit_Prop:"(⋀i. TadmitFO σ (args i)) ⟹ NFadmit σ (Prop f args)"
| NFadmit_Not:"NFadmit σ φ ⟹ NFadmit σ (Not φ)"
| NFadmit_And:"NFadmit σ φ ⟹ NFadmit σ ψ ⟹ NFadmit σ (And φ ψ)"
| NFadmit_Exists:"NFadmit σ φ ⟹ FUadmitFO σ φ {Inl x} ⟹ NFadmit σ (Exists x φ)"
| NFadmit_Diamond:"NFadmit σ φ ⟹ NPadmit σ a ⟹ FUadmitFO σ φ (BVP (PsubstFO a σ)) ⟹ hpsafe (PsubstFO a σ) ⟹ NFadmit σ (Diamond a φ)"
| NFadmit_Context:"NFadmit σ φ ⟹ FUadmitFO σ φ UNIV ⟹ NFadmit σ (InContext C φ)"

inductive_simps
      NPadmit_Pvar_simps[simp]: "NPadmit σ (Pvar a)"
  and NPadmit_Sequence_simps[simp]: "NPadmit σ (a ;; b)"
  and NPadmit_Loop_simps[simp]: "NPadmit σ (a**)"
  and NPadmit_ODE_simps[simp]: "NPadmit σ (EvolveODE ODE p)"
  and NPadmit_Choice_simps[simp]: "NPadmit σ (a ∪∪ b)"
  and NPadmit_Assign_simps[simp]: "NPadmit σ (Assign x e)"
  and NPadmit_DiffAssign_simps[simp]: "NPadmit σ (DiffAssign x e)"
  and NPadmit_Test_simps[simp]: "NPadmit σ (? p)"
  
  and NFadmit_Geq_simps[simp]: "NFadmit σ (Geq t1 t2)"
  and NFadmit_Prop_simps[simp]: "NFadmit σ (Prop p args)"
  and NFadmit_Not_simps[simp]: "NFadmit σ (Not p)"
  and NFadmit_And_simps[simp]: "NFadmit σ (And p q)"
  and NFadmit_Exists_simps[simp]: "NFadmit σ (Exists x p)"
  and NFadmit_Diamond_simps[simp]: "NFadmit σ (Diamond a p)"
  and NFadmit_Context_simps[simp]: "NFadmit σ (InContext C p)"

definition PFUadmit :: "('d ⇒ ('a, 'b, 'c) formula) ⇒ ('a, 'b + 'd, 'c) formula ⇒ ('c + 'c) set ⇒ bool"
where "PFUadmit σ θ U ⟷ True"

definition PPUadmit :: "('d ⇒ ('a, 'b, 'c) formula) ⇒ ('a, 'b + 'd, 'c) hp ⇒ ('c + 'c) set ⇒ bool"
where "PPUadmit σ θ U ⟷ ((⋃ i. FVF (σ i)) ∩ U) = {}"
  
inductive PPadmit:: "('d ⇒ ('a, 'b, 'c) formula) ⇒ ('a, 'b + 'd, 'c) hp ⇒ bool"
and PFadmit:: "('d ⇒ ('a, 'b, 'c) formula) ⇒ ('a, 'b + 'd, 'c) formula ⇒ bool"
where 
  PPadmit_Pvar:"PPadmit σ (Pvar a)"
| PPadmit_Sequence:"PPadmit σ a ⟹ PPadmit σ b ⟹ PPUadmit σ b (BVP (PPsubst a σ))⟹ hpsafe (PPsubst a σ) ⟹ PPadmit σ (Sequence a b)"  
| PPadmit_Loop:"PPadmit σ a ⟹ PPUadmit σ a (BVP (PPsubst a σ)) ⟹ hpsafe (PPsubst a σ) ⟹ PPadmit σ (Loop a)"        
| PPadmit_ODE:"PFadmit σ φ ⟹ PFUadmit σ φ (BVO ODE) ⟹ PPadmit σ (EvolveODE ODE φ)"
| PPadmit_Choice:"PPadmit σ a ⟹ PPadmit σ b ⟹ PPadmit σ (Choice a b)"            
| PPadmit_Assign:"PPadmit σ (Assign x θ)"  
| PPadmit_DiffAssign:"PPadmit σ (DiffAssign x θ)"  
| PPadmit_Test:"PFadmit σ φ ⟹ PPadmit σ (Test φ)"

| PFadmit_Geq:"PFadmit σ (Geq θ1 θ2)"
| PFadmit_Prop:"PFadmit σ (Prop f args)"
| PFadmit_Not:"PFadmit σ φ ⟹ PFadmit σ (Not φ)"
| PFadmit_And:"PFadmit σ φ ⟹ PFadmit σ ψ ⟹ PFadmit σ (And φ ψ)"
| PFadmit_Exists:"PFadmit σ φ ⟹ PFUadmit σ φ {Inl x} ⟹ PFadmit σ (Exists x φ)"
| PFadmit_Diamond:"PFadmit σ φ ⟹ PPadmit σ a ⟹ PFUadmit σ φ (BVP (PPsubst a σ)) ⟹ PFadmit σ (Diamond a φ)"
| PFadmit_Context:"PFadmit σ φ ⟹ PFUadmit σ φ UNIV ⟹ PFadmit σ (InContext C φ)"

inductive_simps
      PPadmit_Pvar_simps[simp]: "PPadmit σ (Pvar a)"
  and PPadmit_Sequence_simps[simp]: "PPadmit σ (a ;; b)"
  and PPadmit_Loop_simps[simp]: "PPadmit σ (a**)"
  and PPadmit_ODE_simps[simp]: "PPadmit σ (EvolveODE ODE p)"
  and PPadmit_Choice_simps[simp]: "PPadmit σ (a ∪∪ b)"
  and PPadmit_Assign_simps[simp]: "PPadmit σ (Assign x e)"
  and PPadmit_DiffAssign_simps[simp]: "PPadmit σ (DiffAssign x e)"
  and PPadmit_Test_simps[simp]: "PPadmit σ (? p)"
  
  and PFadmit_Geq_simps[simp]: "PFadmit σ (Geq t1 t2)"
  and PFadmit_Prop_simps[simp]: "PFadmit σ (Prop p args)"
  and PFadmit_Not_simps[simp]: "PFadmit σ (Not p)"
  and PFadmit_And_simps[simp]: "PFadmit σ (And p q)"
  and PFadmit_Exists_simps[simp]: "PFadmit σ (Exists x p)"
  and PFadmit_Diamond_simps[simp]: "PFadmit σ (Diamond a p)"
  and PFadmit_Context_simps[simp]: "PFadmit σ (InContext C p)"
  
inductive Padmit:: "('a, 'b, 'c) subst ⇒ ('a, 'b, 'c) hp ⇒ bool"
and Fadmit:: "('a, 'b, 'c) subst ⇒ ('a, 'b, 'c) formula ⇒ bool"
where
  Padmit_Pvar:"Padmit σ (Pvar a)"
| Padmit_Sequence:"Padmit σ a ⟹ Padmit σ b ⟹ PUadmit σ b (BVP (Psubst a σ))⟹ hpsafe (Psubst a σ) ⟹ Padmit σ (Sequence a b)"  
| Padmit_Loop:"Padmit σ a ⟹ PUadmit σ a (BVP (Psubst a σ)) ⟹ hpsafe (Psubst a σ) ⟹ Padmit σ (Loop a)"        
| Padmit_ODE:"Oadmit σ ODE (BVO ODE) ⟹ Fadmit σ φ ⟹ FUadmit σ φ (BVO ODE) ⟹ Padmit σ (EvolveODE ODE φ)"
| Padmit_Choice:"Padmit σ a ⟹ Padmit σ b ⟹ Padmit σ (Choice a b)"            
| Padmit_Assign:"Tadmit σ θ ⟹ Padmit σ (Assign x θ)"  
| Padmit_DiffAssign:"Tadmit σ θ ⟹ Padmit σ (DiffAssign x θ)"  
| Padmit_Test:"Fadmit σ φ ⟹ Padmit σ (Test φ)"

| Fadmit_Geq:"Tadmit σ θ1 ⟹ Tadmit σ θ2 ⟹ Fadmit σ (Geq θ1 θ2)"
| Fadmit_Prop1:"(⋀i. Tadmit σ (args i)) ⟹ SPredicates σ p = Some p' ⟹ NFadmit (λ i. Tsubst (args i) σ) p' ⟹ (⋀i. dsafe (Tsubst (args i) σ))⟹ Fadmit σ (Prop p args)"
| Fadmit_Prop2:"(⋀i. Tadmit σ (args i)) ⟹ SPredicates σ p = None ⟹ Fadmit σ (Prop p args)"
| Fadmit_Not:"Fadmit σ φ ⟹ Fadmit σ (Not φ)"
| Fadmit_And:"Fadmit σ φ ⟹ Fadmit σ ψ ⟹ Fadmit σ (And φ ψ)"
| Fadmit_Exists:"Fadmit σ φ ⟹ FUadmit σ φ {Inl x} ⟹ Fadmit σ (Exists x φ)"
| Fadmit_Diamond:"Fadmit σ φ ⟹ Padmit σ a ⟹ FUadmit σ φ (BVP (Psubst a σ)) ⟹ hpsafe (Psubst a σ) ⟹ Fadmit σ (Diamond a φ)"
| Fadmit_Context1:"Fadmit σ φ ⟹ FUadmit σ φ UNIV ⟹ SContexts σ C = Some C' ⟹ PFadmit (λ _. Fsubst φ σ) C' ⟹ fsafe(Fsubst φ σ) ⟹ Fadmit σ (InContext C φ)"
| Fadmit_Context2:"Fadmit σ φ ⟹ FUadmit σ φ UNIV ⟹ SContexts σ C = None ⟹ Fadmit σ (InContext C φ)"
  
inductive_simps
      Padmit_Pvar_simps[simp]: "Padmit σ (Pvar a)"
  and Padmit_Sequence_simps[simp]: "Padmit σ (a ;; b)"
  and Padmit_Loop_simps[simp]: "Padmit σ (a**)"
  and Padmit_ODE_simps[simp]: "Padmit σ (EvolveODE ODE p)"
  and Padmit_Choice_simps[simp]: "Padmit σ (a ∪∪ b)"
  and Padmit_Assign_simps[simp]: "Padmit σ (Assign x e)"
  and Padmit_DiffAssign_simps[simp]: "Padmit σ (DiffAssign x e)"
  and Padmit_Test_simps[simp]: "Padmit σ (? p)"
  
  and Fadmit_Geq_simps[simp]: "Fadmit σ (Geq t1 t2)"
  and Fadmit_Prop_simps[simp]: "Fadmit σ (Prop p args)"
  and Fadmit_Not_simps[simp]: "Fadmit σ (Not p)"
  and Fadmit_And_simps[simp]: "Fadmit σ (And p q)"
  and Fadmit_Exists_simps[simp]: "Fadmit σ (Exists x p)"
  and Fadmit_Diamond_simps[simp]: "Fadmit σ (Diamond a p)"
  and Fadmit_Context_simps[simp]: "Fadmit σ (InContext C p)"
    
fun extendf :: "('sf, 'sc, 'sz) interp ⇒ 'sz Rvec ⇒ ('sf + 'sz, 'sc, 'sz) interp"
where "extendf I R =
⦇Functions = (λf. case f of Inl f' ⇒ Functions I f' | Inr f' ⇒ (λ_. R $ f')),
 Predicates = Predicates I,
 Contexts = Contexts I,
 Programs = Programs I,
 ODEs = ODEs I,
 ODEBV = ODEBV I
 ⦈"

fun extendc :: "('sf, 'sc, 'sz) interp ⇒ 'sz state set ⇒ ('sf, 'sc + unit, 'sz) interp"
where "extendc I R =
⦇Functions =  Functions I,
 Predicates = Predicates I,
 Contexts = (λC. case C of Inl C' ⇒ Contexts I C' | Inr () ⇒ (λ_.  R)),
 Programs = Programs I,
 ODEs = ODEs I,
 ODEBV = ODEBV I⦈"

definition adjoint :: "('sf, 'sc, 'sz) interp ⇒ ('sf, 'sc, 'sz) subst ⇒ 'sz state ⇒ ('sf, 'sc, 'sz) interp" 
where "adjoint I σ ν =
⦇Functions =   (λf. case SFunctions σ f of Some f' ⇒ (λR. dterm_sem (extendf I R) f' ν) | None ⇒ Functions I f),
 Predicates = (λp. case SPredicates σ p of Some p' ⇒ (λR. ν ∈ fml_sem (extendf I R) p') | None ⇒ Predicates I p),
 Contexts =   (λc. case SContexts σ c of Some c' ⇒ (λR. fml_sem (extendc I R) c') | None ⇒ Contexts I c),
 Programs =   (λa. case SPrograms σ a of Some a' ⇒ prog_sem I a' | None ⇒ Programs I a),
 ODEs =     (λode. case SODEs σ ode of Some ode' ⇒ ODE_sem I ode' | None ⇒ ODEs I ode),
 ODEBV = (λode. case SODEs σ ode of Some ode' ⇒ ODE_vars I ode' | None ⇒ ODEBV I ode)
 ⦈"

lemma dsem_to_ssem:"dfree θ ⟹ dterm_sem I θ ν = sterm_sem I θ (fst ν)"
  by (induct rule: dfree.induct) (auto)

definition adjointFO::"('sf, 'sc, 'sz) interp ⇒ ('d::finite ⇒ ('sf, 'sz) trm) ⇒ 'sz state ⇒ ('sf + 'd, 'sc, 'sz) interp" 
where "adjointFO I σ ν =
⦇Functions =   (λf. case f of Inl f' ⇒ Functions I f' | Inr f' ⇒ (λ_. dterm_sem I (σ f') ν)),
 Predicates = Predicates I,
 Contexts = Contexts I,
 Programs = Programs I,
 ODEs = ODEs I,
 ODEBV = ODEBV I
 ⦈"

lemma adjoint_free:
  assumes sfree:"(⋀i f'. SFunctions σ i = Some f' ⟹ dfree f')"
  shows "adjoint I σ ν =
  ⦇Functions =  (λf. case SFunctions σ f of Some f' ⇒ (λR. sterm_sem (extendf I R) f' (fst ν)) | None ⇒ Functions I f),
   Predicates = (λp. case SPredicates σ p of Some p' ⇒ (λR. ν ∈ fml_sem (extendf I R) p') | None ⇒ Predicates I p),
   Contexts =   (λc. case SContexts σ c of Some c' ⇒ (λR. fml_sem (extendc I R) c') | None ⇒ Contexts I c),
   Programs =   (λa. case SPrograms σ a of Some a' ⇒ prog_sem I a' | None ⇒ Programs I a),
   ODEs =     (λode. case SODEs σ ode of Some ode' ⇒ ODE_sem I ode' | None ⇒ ODEs I ode),
   ODEBV = (λode. case SODEs σ ode of Some ode' ⇒ ODE_vars I ode' | None ⇒ ODEBV I ode)⦈"
  using dsem_to_ssem[OF sfree] 
  by (cases ν) (auto simp add: adjoint_def fun_eq_iff split: option.split)

lemma adjointFO_free:"(⋀i. dfree (σ i)) ⟹ (adjointFO I σ ν =
⦇Functions =   (λf. case f of Inl f' ⇒ Functions I f' | Inr f' ⇒ (λ_. sterm_sem I (σ f') (fst ν))),
 Predicates = Predicates I,
 Contexts = Contexts I,
 Programs = Programs I,
 ODEs = ODEs I,
 ODEBV = ODEBV I⦈)" 
  by (auto simp add: dsem_to_ssem adjointFO_def)

definition PFadjoint::"('sf, 'sc, 'sz) interp ⇒ ('d::finite ⇒ ('sf, 'sc, 'sz) formula) ⇒ ('sf, 'sc  + 'd, 'sz) interp" 
where "PFadjoint I σ =
⦇Functions =  Functions I,
 Predicates = Predicates I,
 Contexts = (λf. case f of Inl f' ⇒ Contexts I f' | Inr f' ⇒ (λ_. fml_sem I (σ f'))),
 Programs = Programs I,
 ODEs = ODEs I,
 ODEBV = ODEBV I⦈"


fun Ssubst::"('sf, 'sc, 'sz) sequent ⇒ ('sf,'sc,'sz) subst ⇒ ('sf,'sc,'sz) sequent"
where "Ssubst (Γ,Δ) σ = (map (λ φ. Fsubst φ σ) Γ, map (λ φ. Fsubst φ σ) Δ)"
  
fun Rsubst::"('sf, 'sc, 'sz) rule ⇒ ('sf,'sc,'sz) subst ⇒ ('sf,'sc,'sz) rule"
where "Rsubst (SG,C) σ = (map (λ φ. Ssubst φ σ) SG, Ssubst C σ)"

definition Sadmit::"('sf,'sc,'sz) subst ⇒ ('sf,'sc,'sz) sequent ⇒ bool"
where "Sadmit σ S ⟷ ((∀i. i ≥ 0 ⟶ i < length (fst S) ⟶ Fadmit σ (nth (fst S) i))
                      ∧(∀i. i ≥ 0 ⟶ i < length (snd S) ⟶ Fadmit σ (nth (snd S) i)))"
  
definition Radmit::"('sf,'sc,'sz) subst ⇒ ('sf,'sc,'sz) rule ⇒ bool"
where "Radmit σ R ⟷ (((∀i. i ≥ 0 ⟶ i < length (fst R) ⟶ Sadmit σ (nth (fst R) i)) 
                   ∧ Sadmit σ (snd R)))"

end end