Theory Static_Semantics

theory "Static_Semantics"
imports
  Ordinary_Differential_Equations.ODE_Analysis
  "Ids"
  "Lib"
  "Syntax"
  "Denotational_Semantics"
  "Frechet_Correctness"
begin
section ‹Static Semantics›
text ‹This section introduces functions for computing properties of the static semantics, specifically
 the following dependencies:
  \begin{itemize}
    \item Signatures: Symbols (from the interpretation) which influence the result of a term, ode, formula, program
    \item Free variables: Variables (from the state) which influence the result of a term, ode, formula, program
    \item Bound variables: Variables (from the state) that *might* be influenced by a program
    \item Must-bound variables: Variables (from the state) that are *always* influenced by a program (i.e.
  will never depend on anything other than the free variables of that program)
  \end{itemize}
   
  We also prove basic lemmas about these definitions, but their overall correctness is proved elsewhere
  in the Bound Effect and Coincidence theorems.
  ›

subsection ‹Signature Definitions›
primrec SIGT :: "('a, 'c) trm ⇒ 'a set"
where
  "SIGT (Var var) = {}"
| "SIGT (Const r) = {}"
| "SIGT (Function var f) = {var} ∪ (⋃i. SIGT (f i))"
| "SIGT (Plus t1 t2) = SIGT t1 ∪ SIGT t2"
| "SIGT (Times t1 t2) = SIGT t1 ∪ SIGT t2"
| "SIGT (DiffVar x) = {}"
| "SIGT (Differential t) = SIGT t"

primrec SIGO   :: "('a, 'c) ODE ⇒ ('a + 'c) set"
where
  "SIGO (OVar c) = {Inr c}"
| "SIGO (OSing x θ) =  {Inl x| x. x ∈ SIGT θ}"
| "SIGO (OProd ODE1 ODE2) = SIGO ODE1 ∪ SIGO ODE2"
  
primrec SIGP   :: "('a, 'b, 'c) hp      ⇒ ('a + 'b + 'c) set"
and     SIGF   :: "('a, 'b, 'c) formula ⇒ ('a + 'b + 'c) set"
where
  "SIGP (Pvar var) = {Inr (Inr var)}"
| "SIGP (Assign var t) = {Inl x | x. x ∈ SIGT t}"
| "SIGP (DiffAssign var t) = {Inl x | x. x ∈ SIGT t}"
| "SIGP (Test p) = SIGF p"
| "SIGP (EvolveODE ODE p) = SIGF p ∪ {Inl x | x. Inl x ∈ SIGO ODE} ∪ {Inr (Inr x) | x. Inr x ∈ SIGO ODE}"
| "SIGP (Choice a b) = SIGP a ∪ SIGP b"
| "SIGP (Sequence a b) = SIGP a ∪ SIGP b"
| "SIGP (Loop a) = SIGP a"
| "SIGF (Geq t1 t2) = {Inl x | x. x ∈ SIGT t1 ∪ SIGT t2}"
| "SIGF (Prop var args) = {Inr (Inr var)} ∪ {Inl x | x. x ∈ (⋃i. SIGT (args i))}"
| "SIGF (Not p) = SIGF p"
| "SIGF (And p1 p2) = SIGF p1 ∪ SIGF p2"
| "SIGF (Exists var p) = SIGF p"
| "SIGF (Diamond a p) = SIGP a ∪ SIGF p"
| "SIGF (InContext var p) = {Inr (Inl var)} ∪ SIGF p"

fun primify :: "('a + 'a) ⇒ ('a + 'a) set"
where
  "primify (Inl x) = {Inl x, Inr x}"
| "primify (Inr x) = {Inl x, Inr x}"
  
subsection ‹Variable Binding Definitions›
text‹
  We represent the (free or bound or must-bound) variables of a term as an (id + id) set,
  where all the (Inl x) elements are unprimed variables x and all the (Inr x) elements are
  primed variables x'.
  ›
text‹Free variables of a term ›
primrec FVT :: "('a, 'c) trm ⇒ ('c + 'c) set"
where
  "FVT (Var x) = {Inl x}"
| "FVT (Const x) = {}"
| "FVT (Function f args) = (⋃i. FVT (args i))"
| "FVT (Plus f g) = FVT f ∪ FVT g"
| "FVT (Times f g) = FVT f ∪ FVT g"
| "FVT (Differential f) = (⋃x ∈ (FVT f). primify x)"
| "FVT (DiffVar x) = {Inr x}"

fun FVDiff :: "('a, 'c) trm ⇒ ('c + 'c) set"
where "FVDiff f = (⋃x ∈ (FVT f). primify x)"

text‹ Free variables of an ODE includes both the bound variables and the terms ›
fun FVO :: "('a, 'c) ODE ⇒ 'c set"
where
  "FVO (OVar c) = UNIV"
| "FVO (OSing x θ) = {x} ∪ {x . Inl x ∈ FVT θ}"
| "FVO (OProd ODE1 ODE2) = FVO ODE1 ∪ FVO ODE2"

text‹ Bound variables of ODEs, formulas, programs ›
fun BVO :: "('a, 'c) ODE ⇒ ('c + 'c) set"
where 
  "BVO (OVar c) = UNIV"
| "BVO (OSing x θ) = {Inl x, Inr x}"
| "BVO (OProd ODE1 ODE2) = BVO ODE1 ∪ BVO ODE2"
  
fun BVF :: "('a, 'b, 'c) formula ⇒ ('c + 'c) set"
and BVP :: "('a, 'b, 'c) hp ⇒ ('c + 'c) set"
where
  "BVF (Geq f g) = {}"
| "BVF (Prop p dfun_args) = {}"
| "BVF (Not p) = BVF p"
| "BVF (And p q) = BVF p ∪ BVF q"
| "BVF (Exists x p) = {Inl x} ∪ BVF p"
| "BVF (Diamond α p) = BVP α ∪ BVF p"
| "BVF (InContext C p) = UNIV"

| "BVP (Pvar a) = UNIV"
| "BVP (Assign x θ) = {Inl x}"
| "BVP (DiffAssign x θ) = {Inr x}"
| "BVP (Test φ) = {}"
| "BVP (EvolveODE ODE φ) = BVO ODE"
| "BVP (Choice α β) = BVP α ∪ BVP β"
| "BVP (Sequence α β) = BVP α ∪ BVP β"
| "BVP (Loop α) = BVP α"

text‹ Must-bound variables (of a program)›
fun MBV :: "('a, 'b, 'c) hp ⇒ ('c + 'c) set"
where
  "MBV (Pvar a) = {}"
| "MBV (Choice α β) = MBV α ∩ MBV β"
| "MBV (Sequence α β) = MBV α ∪ MBV β"
| "MBV (Loop α) = {}"
| "MBV (EvolveODE ODE _) = (Inl ` (ODE_dom ODE)) ∪ (Inr ` (ODE_dom ODE))"
| "MBV α = BVP α"

text‹Free variables of a formula,
 free variables of a program ›
fun FVF :: "('a, 'b, 'c) formula ⇒ ('c + 'c) set"
and FVP :: "('a, 'b, 'c) hp ⇒ ('c + 'c) set"
where
  "FVF (Geq f g) = FVT f ∪ FVT g"
| "FVF (Prop p args) = (⋃i. FVT (args i))"
| "FVF (Not p) = FVF p"
| "FVF (And p q) = FVF p ∪ FVF q"
| "FVF (Exists x p) = FVF p - {Inl x}"
| "FVF (Diamond α p) =   FVP α ∪ (FVF p - MBV α)"
| "FVF (InContext C p) = UNIV"
| "FVP (Pvar a) = UNIV"
| "FVP (Assign x θ) = FVT θ"
| "FVP (DiffAssign x θ) = FVT θ"
| "FVP (Test φ) = FVF φ"
| "FVP (EvolveODE ODE φ) = BVO ODE ∪ (Inl ` FVO ODE) ∪ FVF φ"
| "FVP (Choice α β) = FVP α ∪ FVP β"
| "FVP (Sequence α β) = FVP α ∪ (FVP β - MBV α)"
| "FVP (Loop α) = FVP α"

subsection ‹Lemmas for reasoning about static semantics› 

lemma primify_contains:"x ∈ primify x"
  by (cases "x") auto

lemma FVDiff_sub:"FVT f ⊆ FVDiff f"
  by (auto simp add:  primify_contains)

lemma fvdiff_plus1:"FVDiff (Plus t1 t2) = FVDiff t1 ∪ FVDiff t2"
  by (auto)

lemma agree_func_fvt:"Vagree ν ν' (FVT (Function f args)) ⟹ Vagree ν ν' (FVT (args i))"
  by (auto simp add: Set.Un_upper1 agree_supset Vagree_def)

lemma agree_plus1:"Vagree ν ν' (FVDiff (Plus t1 t2)) ⟹ Vagree ν ν' (FVDiff t1)"
proof -
  assume agree:"Vagree ν ν' (FVDiff (Plus t1 t2))"
  have agree':"Vagree ν ν' ((⋃i∈FVT t1. primify i) ∪ (⋃i∈FVT t2. primify i))"
    using fvdiff_plus1 FVDiff.simps agree by (auto)
  have agreeL:"Vagree ν ν' ((⋃i∈FVT t1. primify i))"
    using agree' agree_supset Set.Un_upper1 by (blast)
  show "Vagree ν ν' (FVDiff t1)" using agreeL by (auto)
qed

lemma agree_plus2:"Vagree ν ν' (FVDiff (Plus t1 t2)) ⟹ Vagree ν ν' (FVDiff t2)"
proof -
  assume agree:"Vagree ν ν' (FVDiff (Plus t1 t2))"
  have agree':"Vagree ν ν' ((⋃i∈FVT t1. primify i) ∪ (⋃i∈FVT t2. primify i))"
    using fvdiff_plus1 FVDiff.simps agree by (auto)
  have agreeR:"Vagree ν ν' ((⋃i∈FVT t2. primify i))"
    using agree' agree_supset Set.Un_upper1 by (blast)
  show "Vagree ν ν' (FVDiff t2)" using agreeR by (auto)
qed

lemma agree_times1:"Vagree ν ν' (FVDiff (Times t1 t2)) ⟹ Vagree ν ν' (FVDiff t1)"
proof -
  assume agree:"Vagree ν ν' (FVDiff (Times t1 t2))"
  have agree':"Vagree ν ν' ((⋃i∈FVT t1. primify i) ∪ (⋃i∈FVT t2. primify i))"
    using fvdiff_plus1 FVDiff.simps agree by (auto)
  have agreeL:"Vagree ν ν' ((⋃i∈FVT t1. primify i))"
    using agree' agree_supset Set.Un_upper1 by (blast)
  show "Vagree ν ν' (FVDiff t1)" using agreeL by (auto)
qed

lemma agree_times2:"Vagree ν ν' (FVDiff (Times t1 t2)) ⟹ Vagree ν ν' (FVDiff t2)"
proof -
  assume agree:"Vagree ν ν' (FVDiff (Times t1 t2))"
  have agree':"Vagree ν ν' ((⋃i∈FVT t1. primify i) ∪ (⋃i∈FVT t2. primify i))"
    using fvdiff_plus1 FVDiff.simps agree by (auto)
  have agreeR:"Vagree ν ν' ((⋃i∈FVT t2. primify i))"
    using agree' agree_supset Set.Un_upper1 by (blast)
  show "Vagree ν ν' (FVDiff t2)" using agreeR by (auto)
qed

lemma agree_func:"Vagree ν ν' (FVDiff ($f var args)) ⟹ (⋀i. Vagree ν ν' (FVDiff (args i)))"
proof -
  assume agree:"Vagree ν ν' (FVDiff ($f var args))"
  have agree':"Vagree ν ν' ((⋃i. (⋃j ∈(FVT (args i)). primify j)))"
    using fvdiff_plus1 FVDiff.simps agree by (auto)
  fix i :: 'a
  have "⋀S. ¬ S ⊆ (⋃f. ⋃ (primify ` FVT (args f))) ∨ Vagree ν ν' S"
    using agree' agree_supset by blast
  then have "⋀f. f ∉ UNIV ∨ Vagree ν ν' (⋃ (primify ` FVT (args f)))"
    by blast
  then show "Vagree ν ν' (FVDiff (args i))"
    by simp
qed
  
end