Theory Denotational_Semantics

theory "Denotational_Semantics" 
imports
  "HOL-Analysis.Derivative"
  "Syntax"         
begin
section ‹Denotational Semantics›

text ‹Defines the denotational semantics of Differential Game Logic. 🌐‹https://doi.org/10.1145/2817824› 🌐‹https://doi.org/10.1007/978-3-319-94205-6_15››

subsection ‹States›

text ‹Vector of reals over ident›
type_synonym Rvec = "variable ⇒ real"
type_synonym state = "Rvec"


text ‹the set of all worlds›
definition worlds:: "state set"
  where "worlds = {ν. True}"

text ‹the set of all variables›
abbreviation allvars:: "variable set"
  where "allvars ≡ {x::variable. True}"

text ‹the set of all real variables›
abbreviation allrvars:: "variable set"
  where "allrvars ≡ {RVar x | x. True}"

text ‹the set of all differential variables›
abbreviation alldvars:: "variable set"
  where "alldvars ≡ {DVar x | x. True}"

  
lemma ident_finite: "finite({x::ident. True})"
  by auto

lemma allvar_cases: "allvars = allrvars ∪ alldvars"
  using variable.exhaust by blast 

lemma rvar_finite: "finite allrvars"
  using finite_imageI[OF ident_finite, where h=‹λx. RVar x›] by (simp add: full_SetCompr_eq) 

lemma dvar_finite: "finite alldvars"
  using finite_imageI[OF ident_finite, where h=‹λx. DVar x›] by (simp add: full_SetCompr_eq) 

lemma allvars_finite [simp]: "finite(allvars)"
  using allvar_cases dvar_finite rvar_finite by (metis finite_Un) 
  
  
definition Vagree :: "state ⇒ state ⇒ variable set ⇒ bool"
  where "Vagree ν ν' V ≡ (∀i. i∈V ⟶ ν(i) = ν'(i))"

definition Uvariation :: "state ⇒ state ⇒ variable set ⇒ bool"
  where "Uvariation ν ν' U ≡ (∀i. ~(i∈U) ⟶ ν(i) = ν'(i))"

lemma Uvariation_Vagree [simp]: "Uvariation ν ν' (-V) = Vagree ν ν' V"
  unfolding Vagree_def Uvariation_def by simp

  
lemma Vagree_refl [simp]: "Vagree ν ν V"
  by (auto simp add: Vagree_def)

lemma Vagree_sym: "Vagree ν ν' V = Vagree ν' ν V"
  by (auto simp add: Vagree_def)

lemma Vagree_sym_rel [sym]: "Vagree ν ν' V ⟹ Vagree ν' ν V"
  using Vagree_sym by auto

lemma Vagree_union [trans]: "Vagree ν ν' V ⟹ Vagree ν ν' W ⟹ Vagree ν ν' (V∪W)"
  by (auto simp add: Vagree_def)

lemma Vagree_trans [trans]: "Vagree ν ν' V ⟹ Vagree  ν' ν'' W ⟹ Vagree ν ν'' (V∩W)"
  by (auto simp add: Vagree_def)

lemma Vagree_antimon [simp]: "Vagree ν ν' V ∧ W⊆V ⟶ Vagree ν ν' W"
  by (auto simp add: Vagree_def)

lemma Vagree_empty [simp]: "Vagree ν ν' {}"
  by (auto simp add: Vagree_def)

lemma Uvariation_empty [simp]: "Uvariation ν ν' {} = (ν=ν')"
  by (auto simp add: Uvariation_def)

lemma Vagree_univ [simp]: "Vagree ν ν' allvars = (ν=ν')"
  by (auto simp add: Vagree_def)

lemma Uvariation_univ [simp]: "Uvariation ν ν' allvars"
  by (auto simp add: Uvariation_def)

lemma Vagree_and [simp]: "Vagree ν ν' V ∧ Vagree ν ν' W ⟷ Vagree ν ν' (V∪W)"
  by (auto simp add: Vagree_def)

lemma Vagree_or: "Vagree ν ν' V ∨ Vagree ν ν' W ⟶ Vagree ν ν' (V∩W)"
  by (auto simp add: Vagree_def)

lemma Uvariation_refl [simp]: "Uvariation ν ν V"
  by (auto simp add: Uvariation_def)

lemma Uvariation_sym: "Uvariation ω ν U = Uvariation ν ω U"
  unfolding Uvariation_def by auto

lemma Uvariation_sym_rel [sym]: "Uvariation ω ν U ⟹ Uvariation ν ω U"
  using Uvariation_sym by auto

lemma Uvariation_trans [trans]: "Uvariation ω ν U ⟹ Uvariation ν μ V ⟹ Uvariation ω μ (U∪V)"
  unfolding Uvariation_def by simp

lemma Uvariation_mon [simp]: "V ⊇ U ⟹ Uvariation ω ν U ⟹ Uvariation ω ν V"
  unfolding Uvariation_def by auto


  
subsection Interpretations

lemma mon_mono: "mono r = ((∀X Y. (X⊆Y ⟶ r(X)⊆r(Y))))"
  unfolding mono_def by simp
 
text ‹interpretations of symbols in ident›
type_synonym interp_rep =
 "(ident ⇒ real) × (ident ⇒ (real ⇒ real)) × (ident ⇒ (real ⇒ bool)) × (ident ⇒ (state set ⇒ state set))"

definition is_interp :: "interp_rep ⇒ bool"
 where "is_interp I ≡ case I of (_, _, _, G) ⇒ (∀a. mono (G a))"

typedef interp = "{I:: interp_rep. is_interp I}"
  morphisms raw_interp well_interp
proof
 show "(λf. 0, λf x. 0, λp x. True, λa. λX. X) ∈ {I. is_interp I}" unfolding is_interp_def mono_def by simp
qed

setup_lifting type_definition_interp

lift_definition Consts::"interp ⇒ ident ⇒ (real)" is "λ(F0, _, _, _). F0" .
lift_definition Funcs:: "interp ⇒ ident ⇒ (real ⇒ real)" is "λ(_, F, _, _). F" .
lift_definition Preds:: "interp ⇒ ident ⇒ (real ⇒ bool)" is "λ(_, _, P, _). P" .
lift_definition Games:: "interp ⇒ ident ⇒ (state set ⇒ state set)" is "λ(_, _, _, G). G" .

text ‹make interpretations›
lift_definition mkinterp:: "(ident ⇒ real) × (ident ⇒ (real ⇒ real)) × (ident ⇒ (real ⇒ bool)) × (ident ⇒ (state set ⇒ state set))
⇒ interp" 
  is "λ(C, F, P, G). if ∀a. mono (G a) then (C, F, P, G) else (C, F, P, λ_ _. {})"
  by (auto split: prod.splits simp: mono_def is_interp_def)

lemma Consts_mkinterp [simp]: "Consts (mkinterp(C,F,P,G)) = C"
  apply (transfer fixing: C F P G)
  apply (auto simp add: is_interp_def mono_def)
  done

lemma Funcs_mkinterp [simp]: "Funcs (mkinterp(C,F,P,G)) = F"
  apply (transfer fixing: C F P G)
  apply (auto simp add: is_interp_def mono_def)
  done
  
lemma Preds_mkinterp [simp]: "Preds (mkinterp(C,F,P,G)) = P"
  apply (transfer fixing: C F P G)
  apply (auto simp add: is_interp_def mono_def)
  done

lemma Games_mkinterp [simp]: "(⋀a. mono (G a) ) ⟹ Games (mkinterp(C,F,P,G)) = G"
  apply (transfer fixing: C F P G)
  apply (auto simp add: is_interp_def mono_def)
  done

lemma mkinterp_eq [iff]: "(Consts I = Consts J ∧ Funcs I = Funcs J ∧ Preds I = Preds J ∧ Games I = Games J) = (I=J)"
  apply (transfer fixing: C F P G)
  apply (auto simp add: is_interp_def mono_def)
  done
  
lemma [simp]: "X⊆Y ⟹ (Games I a)(X)⊆(Games I a)(Y)"
  apply (transfer fixing: a X Y)
  apply (auto simp add: is_interp_def mono_def)
  apply (blast)
  done

lifting_update interp.lifting
lifting_forget interp.lifting


subsection Semantics

text ‹Semantic modification ‹repv ω x r› replaces the value of variable ‹x› in the state ‹ω› with r›
definition repv :: "state ⇒ variable ⇒ real ⇒ state"
  where "repv ω x r = fun_upd ω x r"

lemma repv_def_correct: "repv ω x r = (λy. if x = y then r else ω(y))"
  unfolding repv_def by auto 

lemma repv_access [simp]: "(repv ω x r)(y) = (if (x=y) then r else ω(y))"
  unfolding repv_def by simp

lemma repv_self [simp]: "repv ω x (ω(x)) = ω"
  unfolding repv_def by auto

lemma Vagree_repv: "Vagree ω (repv ω x d) (-{x})"
  unfolding repv_def Vagree_def by simp

lemma Vagree_repv_self: "Vagree ω (repv ω x d) {x} = (d=ω(x))"
  unfolding repv_def Vagree_def by auto

lemma Uvariation_repv: "Uvariation ω (repv ω x d) {x}"
  unfolding repv_def Uvariation_def by simp

paragraph ‹Semantics of Terms›

fun term_sem :: "interp ⇒ trm ⇒ (state ⇒ real)"
where
  "term_sem I (Var x) = (λω. ω(x))"
| "term_sem I (Number r) = (λω. r)"
| "term_sem I (Const f) = (λω. (Consts I f))"
| "term_sem I (Func f θ) = (λω. (Funcs I f)(term_sem I θ ω))"
| "term_sem I (Plus θ η) = (λω. term_sem I θ ω + term_sem I η ω)"
| "term_sem I (Times θ η) = (λω. term_sem I θ ω * term_sem I η ω)"
| "term_sem I (Differential θ) = (λω. sum(λx. ω(DVar x)*deriv(λX. term_sem I θ (repv ω (RVar x) X))(ω(RVar x)))(allidents))"
  
paragraph ‹Solutions of Differential Equations›

(*@note For simplicity, solutions are not limited to a smaller interval of existence*)
type_synonym solution = "real ⇒ state"

definition solves_ODE :: "interp ⇒ solution ⇒ ident ⇒ trm ⇒ bool"
where "solves_ODE I F x θ ≡ (∀ζ::real.
     Vagree (F(0)) (F(ζ)) (-{RVar x, DVar x})
   ∧ F(ζ)(DVar x) = deriv(λt. F(t)(RVar x))(ζ)
   ∧ F(ζ)(DVar x) = term_sem I θ (F(ζ)))"

paragraph ‹Semantics of Formulas and Games›
  
fun fml_sem :: "interp ⇒ fml ⇒ (state set)" and
   game_sem :: "interp ⇒ game ⇒ (state set ⇒ state set)"
where
  "fml_sem I (Pred p θ) = {ω. (Preds I p)(term_sem I θ ω)}"
| "fml_sem I (Geq θ η) = {ω. term_sem I θ ω ≥ term_sem I η ω}"
| "fml_sem I (Not φ) = {ω. ω ∉ fml_sem I φ}"
| "fml_sem I (And φ ψ) = fml_sem I φ ∩ fml_sem I ψ"
| "fml_sem I (Exists x φ) = {ω. ∃r. (repv ω x r) ∈ fml_sem I φ}"
| "fml_sem I (Diamond α φ) = game_sem I α (fml_sem I φ)"

| "game_sem I (Game a) = (λX. (Games I a)(X))"
| "game_sem I (Assign x θ) = (λX. {ω. (repv ω x (term_sem I θ ω)) ∈ X})"
| "game_sem I (Test φ) = (λX. fml_sem I φ ∩ X)"
| "game_sem I (Choice α β) = (λX. game_sem I α X ∪ game_sem I β X)"
| "game_sem I (Compose α β) = (λX. game_sem I α (game_sem I β X))"
| "game_sem I (Loop α) = (λX. ⋂{Z. X ∪ game_sem I α Z ⊆ Z})"
| "game_sem I (Dual α) = (λX. -(game_sem I α (-X)))"
| "game_sem I (ODE x θ) = (λX. {ω. ∃F T. Vagree ω (F(0)) (-{DVar x}) ∧ F(T) ∈ X ∧ solves_ODE I F x θ})"


text ‹Validity›

definition valid_in :: "interp ⇒ fml ⇒ bool"
where "valid_in I φ ≡ (∀ω. ω ∈ fml_sem I φ)"

definition valid :: "fml ⇒ bool"
  where "valid φ ≡ (∀I.∀ω. ω ∈ fml_sem I φ)"

lemma valid_is_valid_in_all: "valid φ = (∀I. valid_in I φ)"
  unfolding valid_def valid_in_def by auto

definition locally_sound :: "inference ⇒ bool"
  where "locally_sound R ≡
  (∀I. (∀k. 0≤k ⟶ k<length (fst R) ⟶ valid_in I (nth (fst R) k)) ⟶ valid_in I (snd R))"

definition sound :: "inference ⇒ bool"
  where "sound R ≡
  (∀k. 0≤k ⟶ k<length (fst R) ⟶ valid (nth (fst R) k)) ⟶ valid (snd R)"

lemma locally_sound_is_sound: "locally_sound R ⟹ sound R"
  unfolding locally_sound_def sound_def using valid_is_valid_in_all by auto


subsection ‹Monotone Semantics›

lemma monotone_Test [simp]: "X⊆Y ⟹ game_sem I (Test φ) X ⊆ game_sem I (Test φ) Y"
  by auto

lemma monotone [simp]: "X⊆Y ⟹ game_sem I α X ⊆ game_sem I α Y"
proof (induction α arbitrary: X Y rule: game_induct)
  case (Game a)
  then show ?case by simp
next
  case (Assign x θ)
  then show ?case by auto
next
  case (Test φ)
  then show ?case by auto
next
  case (Choice α1 α2)
  then show ?case by (metis Un_mono game_sem.simps(4))
next
  case (Compose α1 α2)
  then show ?case by auto
next
  case (Loop α)
  then show ?case by auto
next
  case (Dual α)
  then show ?case by auto
next
  case (ODE x θ)
  then show ?case by auto
qed

corollary game_sem_mono [simp]: "mono (λX. game_sem I α X)"
  by (simp add: mon_mono)

corollary game_union: "game_sem I α (X∪Y) ⊇ game_sem I α X ∪ game_sem I α Y"
  by simp

lemmas game_sem_union = game_union


subsection ‹Fixpoint Semantics Alternative for Loops›

lemma game_sem_loop_fixpoint_mono: "mono (λZ. X ∪ game_sem I α Z)"
  using game_sem_mono by (metis Un_mono mon_mono order_refl) 

text ‹Consequence of Knaster-Tarski Theorem 3.5 of 🌐‹https://doi.org/10.1145/2817824››

lemma game_sem_loop: "game_sem I (Loop α) = (λX. lfp(λZ. X ∪ game_sem I α Z))"
proof-
  have "⋂{Z. X ∪ game_sem I α Z ⊆ Z} = lfp(λZ. X ∪ game_sem I α Z)" by (simp add: lfp_def)
  then show ?thesis by (simp add: lfp_def)
qed

corollary game_sem_loop_back: "(λX. lfp(λZ. X ∪ game_sem I α Z)) = game_sem I (Loop α)"
  using game_sem_loop by simp

corollary game_sem_loop_iterate: "game_sem I (Loop α) = (λX. X ∪ game_sem I α (game_sem I (Loop α) X))"
  by (metis (no_types) game_sem_loop game_sem_loop_fixpoint_mono lfp_fixpoint)

corollary game_sem_loop_unwind: "game_sem I (Loop α) = (λX. X ∪ game_sem I (Compose α (Loop α)) X)"
using game_sem_loop_iterate by (metis game_sem.simps(5))

corollary game_sem_loop_unwind_reduce: "(λX. X ∪ game_sem I (Compose α (Loop α)) X) = game_sem I (Loop α)"
  using game_sem_loop_unwind by (rule sym)

lemmas lfp_ordinal_induct_set_cases = lfp_ordinal_induct_set [case_names mono step union]

(* Read off a fixpoint induction scheme from the fact that loops have a least fixpoint semantics *)
lemma game_loop_induct [case_names step union]: 
  "(⋀Z. Z ⊆ game_sem I (Loop α) X ⟹ P(Z) ⟹ P(X ∪ game_sem I α Z))
  ⟹ (⋀M. (∀Z∈M. P(Z)) ⟹ P(Sup M))
  ⟹ P(game_sem I (Loop α) X)"
proof-
  assume loopstep: "⋀Z. Z ⊆ game_sem I (Loop α) X ⟹ P(Z) ⟹  P(X ∪ game_sem I α Z)"
  assume loopsup: "⋀M. (∀Z∈M. P(Z)) ⟹ P(Sup M)"
  have "P(lfp(λZ. X ∪ game_sem I α Z))"
  proof (induction rule: lfp_ordinal_induct[where f=‹λZ. X ∪ game_sem I α Z›])
    case mono
    then show ?case using game_sem_loop_fixpoint_mono by simp
  next
    case (step S)
    then show ?case using loopstep[where Z=S] game_sem_loop[where I=I and α=α] by (simp add: loopstep)
  next
    case (union M)
    then show ?case using loopsup game_sem_loop by auto
  qed
  then show "P(game_sem I (Loop α) X)" using game_sem_loop by simp
  (*proof (induction rule: lfp_ordinal_induct_set_cases[where f=‹λZ. X ∪ game_sem I α Z›])
    case mono
    then show ?case using game_sem_loop_fixpoint_mono by simp
  next
    case (step S)
    then show ?case using loopstep by auto
  next
    case (union M)
    then show ?case using loopsup game_sem_loop by auto
  qed*)
qed


subsection ‹Some Simple Obvious Observations›

lemma fml_sem_not [simp]: "fml_sem I (Not φ) = -fml_sem I φ"
  by auto

lemma fml_sem_not_not [simp]: "fml_sem I (Not (Not φ)) = fml_sem I φ"
  by simp

lemma fml_sem_or [simp]: "fml_sem I (Or φ ψ) = fml_sem I φ ∪ fml_sem I ψ"
  unfolding Or_def by auto

lemma fml_sem_implies [simp]: "fml_sem I (Implies φ ψ) = (-fml_sem I φ) ∪ fml_sem I ψ"
  unfolding Implies_def by auto

lemma TT_valid [simp]: "valid TT"
  unfolding valid_def TT_def by simp

paragraph ‹Semantic equivalence of formulas›

definition fml_equiv:: "fml => fml => bool"
  where "fml_equiv φ ψ ≡ (∀I. fml_sem I φ = fml_sem I ψ)"

text ‹Substitutionality for Equivalent Formulas›

lemma fml_equiv_subst: "fml_equiv φ ψ ⟹ P (fml_sem I φ) ⟹ P (fml_sem I ψ)"
proof-
  assume a1: "fml_equiv φ ψ"
  assume a2: "P (fml_sem I φ)"
  from a1 have "fml_sem I φ = fml_sem I ψ" using fml_equiv_def by blast
  then show ?thesis using forw_subst a2 by simp
qed
  
lemma valid_fml_equiv: "valid (φ ↔ ψ) = fml_equiv φ ψ"
  unfolding valid_def Equiv_def Or_def fml_equiv_def by auto

lemma valid_in_equiv: "valid_in I (φ ↔ ψ) = ((fml_sem I φ) = (fml_sem I ψ))"
  using valid_in_def Equiv_def Or_def by auto

lemma valid_in_impl: "valid_in I (φ → ψ) = ((fml_sem I φ) ⊆ (fml_sem I ψ))"
  unfolding valid_in_def Implies_def Or_def by auto

lemma valid_equiv: "valid (φ ↔ ψ) = (∀I. fml_sem I φ = fml_sem I ψ)"
  using valid_fml_equiv fml_equiv_def by auto

lemma valid_impl: "valid (φ → ψ) = (∀I. (fml_sem I φ) ⊆ (fml_sem I ψ))"
  unfolding valid_def Implies_def Or_def by auto

lemma fml_sem_equals [simp]: "(ω ∈ fml_sem I (Equals θ η)) = (term_sem I θ ω = term_sem I η ω)"
  unfolding valid_def Equals_def Or_def by auto

lemma equiv_refl_valid [simp]: "valid (φ ↔ φ)"
  unfolding valid_def Equiv_def Or_def by simp

lemma equal_refl_valid [simp]: "valid (Equals θ θ)"
  unfolding valid_def Equals_def Or_def by simp

lemma solves_ODE_alt : "solves_ODE I F x θ ≡ (∀ζ::real.
     Vagree (F(0)) (F(ζ)) (-{RVar x, DVar x})
   ∧ F(ζ)(DVar x) = deriv(λt. F(t)(RVar x))(ζ)
   ∧ F(ζ) ∈ fml_sem I (Equals (Var (DVar x)) θ))"
   unfolding solves_ODE_def using fml_sem_equals by simp

paragraph ‹Semantic equivalence of games›

definition game_equiv:: "game => game => bool"
  where "game_equiv α β ≡ (∀I X. game_sem I α X = game_sem I β X)"


text ‹Substitutionality for Equivalent Games›
  
lemma game_equiv_subst: "game_equiv α β ⟹ P (game_sem I α X) ⟹ P (game_sem I β X)"
proof-
  assume a1: "game_equiv α β"
  assume a2: "P (game_sem I α X)"
  from a1 have "game_sem I α X = game_sem I β X" using game_equiv_def by blast
  then show ?thesis using forw_subst a2 by simp
qed

lemma game_equiv_subst_eq: "game_equiv α β ⟹ P (game_sem I α X) == P (game_sem I β X)"
  by (simp add: game_equiv_def)

lemma skip_id [simp]: "game_sem I Skip X = X"
  unfolding Skip_def TT_def by auto

lemma loop_iterate_equiv: "game_equiv (Loop α) (Choice Skip (Compose α (Loop α)))"
unfolding game_equiv_def  
proof (clarify)
  fix I X
  from game_sem_loop_unwind_reduce have "X ∪ game_sem I (Compose α (Loop α)) X = game_sem I (Loop α) X" by metis
  then show "game_sem I (Loop α) X = game_sem I (Choice Skip (Compose α (Loop α))) X" using skip_id by auto
qed


lemma fml_equiv_valid: "fml_equiv φ ψ ⟹ valid φ = valid ψ"
  unfolding valid_def using fml_equiv_subst by blast

lemma solves_Vagree: "solves_ODE I F x θ ⟹ (⋀ζ. Vagree (F(ζ)) (F(0)) (-{RVar x,DVar x}))"
  using solves_ODE_def Vagree_sym_rel by blast 

lemma solves_Vagree_trans: "Uvariation (F(0)) ω U ⟹ solves_ODE I F x θ ⟹ Uvariation (F(ζ)) ω (U∪{RVar x,DVar x})"
  using solves_Vagree Uvariation_Vagree solves_ODE_def
  by (metis Uvariation_sym_rel Uvariation_trans double_complement)  

end