Theory Axioms

theory "Axioms" 
imports
  "Syntax"
  "Denotational_Semantics"
  "Ids"
begin

section ‹Axioms and Axiomatic Proof Rules of Differential Game Logic›

subsection ‹Axioms›

abbreviation pusall:: "fml"
  where "pusall ≡ ⟨Game hgidc⟩TT"

abbreviation nothing:: "trm"
  where "nothing ≡ Number 0"

  
named_theorems axiom_defs "Axiom definitions"

definition box_axiom :: "fml"
  where [axiom_defs]:
"box_axiom ≡ (Box (Game hgid1) pusall) ↔ Not(Diamond (Game hgid1) (Not(pusall)))"

definition assigneq_axiom :: "fml"
  where [axiom_defs]:
"assigneq_axiom ≡ (Diamond (Assign xid1 (Const fid1)) pusall) ↔ Exists xid1 (Equals (Var xid1) (Const fid1) && pusall)"

definition stutterd_axiom :: "fml"
  where [axiom_defs]:
"stutterd_axiom ≡ (Diamond (Assign xid1 (Var xid1)) pusall) ↔ pusall"

definition test_axiom :: "fml"
  where [axiom_defs]:
"test_axiom ≡ Diamond (Test (Pred pid2 nothing)) (Pred pid1 nothing) ↔ (Pred pid2 nothing && Pred pid1 nothing)"

definition choice_axiom :: "fml"
  where [axiom_defs]:
"choice_axiom ≡ Diamond (Choice (Game hgid1) (Game hgid2)) pusall ↔ (Diamond (Game hgid1) pusall || Diamond (Game hgid2) pusall)"

definition compose_axiom :: "fml"
  where [axiom_defs]:
"compose_axiom ≡ Diamond (Compose (Game hgid1) (Game hgid2)) pusall ↔ Diamond (Game hgid1) (Diamond (Game hgid2) pusall)"

definition iterate_axiom :: "fml"
  where [axiom_defs]:
"iterate_axiom ≡ Diamond (Loop (Game hgid1)) pusall ↔ (pusall || Diamond (Game hgid1) (Diamond (Loop (Game hgid1)) pusall))"

definition dual_axiom :: "fml"
  where [axiom_defs]:
"dual_axiom ≡ Diamond (Dual (Game hgid1)) pusall ↔ !(Diamond (Game hgid1) (!pusall))"


subsection ‹Axiomatic Rules›

named_theorems rule_defs "Rule definitions"

definition mon_rule :: "inference"
  where [rule_defs]:
"mon_rule ≡ ([(⟨Game hgidc⟩TT) → (⟨Game hgidd⟩TT)], (⟨Game hgid1⟩(⟨Game hgidc⟩TT)) → (⟨Game hgid1⟩(⟨Game hgidd⟩TT)))"

definition FP_rule :: "inference"
  where [rule_defs]:
"FP_rule ≡ ([((⟨Game hgidc⟩TT) || ⟨Game hgid1⟩⟨Game hgidd⟩TT) → ⟨Game hgidd⟩TT], (⟨Loop (Game hgid1)⟩⟨Game hgidc⟩TT) → (⟨Game hgidd⟩TT))"

definition MP_rule :: "inference"
  where [rule_defs]:
"MP_rule ≡ ([Pred pid1 nothing , Pred pid1 nothing → Pred pid2 nothing], Pred pid2 nothing)"

definition gena_rule :: "inference"
  where [rule_defs]:
"gena_rule ≡ ([pusall], Exists xid1 pusall)"


subsection ‹Soundness / Validity Proofs for Axioms›

text ‹Because an axiom in a uniform substitution calculus is an individual formula, 
  proving the validity of that formula suffices to prove soundness›

lemma box_valid: "valid box_axiom"
  unfolding box_axiom_def Box_def Or_def by simp

(*lemma assign_equal: "game_sem I (Assign x (Const f)) (fml_sem I φ) = fml_sem I (Exists x (Equals (Var x) (Const f) && φ))"
  by simp*)

lemma assigneq_valid: "valid assigneq_axiom"
  unfolding assigneq_axiom_def by (auto simp add: valid_equiv)
  
(*lemma game_sem_stutter: "game_sem I (Assign x (Var x)) X = X"
  by (auto simp add: repv_self)*)

lemma stutterd_valid: "valid stutterd_axiom"
  unfolding stutterd_axiom_def by (auto simp add: valid_equiv)

lemma test_valid: "valid test_axiom"
  unfolding test_axiom_def Or_def using valid_equiv by fastforce

lemma choice_valid: "valid choice_axiom"
  unfolding choice_axiom_def Or_def by (auto simp add: valid_equiv)

lemma compose_valid: "valid compose_axiom"
  unfolding compose_axiom_def Or_def by (simp add: valid_equiv)

lemma dual_valid: "valid dual_axiom"
unfolding dual_axiom_def using valid_equiv fml_sem_not using fml_sem.simps(6) game_sem.simps(7) by presburger

lemma iterate_valid: "valid iterate_axiom"
(*unfolding iterate_axiom_def using valid_equiv fml_sem.simps(6) game_equiv_subst[OF loop_iterate_equiv]*)
proof-
  have "∀I. fml_sem I (Diamond (Loop (Game hgid1)) pusall) = fml_sem I (pusall || Diamond (Game hgid1) (Diamond (Loop (Game hgid1)) pusall))"
  proof
  fix I
    have "fml_sem I (Diamond (Loop (Game hgid1)) pusall) = game_sem I (Loop (Game hgid1)) (fml_sem I pusall)" by (rule fml_sem.simps(6))
    also have "... = game_sem I (Choice Skip (Compose (Game hgid1) (Loop (Game hgid1)))) (fml_sem I pusall)"
    using game_equiv_subst[where I=I and X=‹fml_sem I pusall›, OF loop_iterate_equiv[where α=‹Game hgid1›]] by blast
    also have "... = fml_sem I (Diamond (Choice Skip (Compose (Game hgid1) (Loop (Game hgid1)))) pusall)" by simp
    also have "... = fml_sem I (Diamond Skip pusall || Diamond (Compose (Game hgid1) (Loop (Game hgid1))) pusall)" by simp
    also have "... = fml_sem I (pusall || Diamond (Compose (Game hgid1) (Loop (Game hgid1))) pusall)" by simp
    also have "... = fml_sem I (pusall || Diamond (Game hgid1) (Diamond (Loop (Game hgid1)) pusall))" by simp
    finally show "fml_sem I (Diamond (Loop (Game hgid1)) pusall) = fml_sem I (pusall || Diamond (Game hgid1) (Diamond (Loop (Game hgid1)) pusall))" .
  qed
  then have "valid ((Diamond (Loop (Game hgid1)) pusall) ↔ (pusall || Diamond (Game hgid1) (Diamond (Loop (Game hgid1)) pusall)))" using valid_equiv by (rule rev_iffD2)
  then show "valid iterate_axiom" unfolding iterate_axiom_def by auto
qed


subsection ‹Local Soundness Proofs for Axiomatic Rules›

lemma mon_locsound: "locally_sound mon_rule"
  unfolding mon_rule_def locally_sound_def using valid_in_impl monotone by simp

lemma FP_locsound: "locally_sound FP_rule"
  unfolding FP_rule_def locally_sound_def using valid_in_impl game_sem_loop by auto

lemma MP_locsound: "locally_sound MP_rule"
  unfolding MP_rule_def locally_sound_def valid_in_def using fml_sem_implies less_Suc_eq by auto 

lemma gena_locsound: "locally_sound gena_rule"
  unfolding gena_rule_def locally_sound_def valid_in_def using fml_sem_implies less_Suc_eq by auto 

end