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 assigneq_valid: "valid assigneq_axiom"
unfolding assigneq_axiom_def by (auto simp add: valid_equiv)
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"
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