Theory Axioms
theory "Axioms"
imports
Ordinary_Differential_Equations.ODE_Analysis
"Ids"
"Lib"
"Syntax"
"Denotational_Semantics"
begin context ids begin
section ‹Axioms›
text ‹
The uniform substitution calculus is based on a finite list of concrete
axioms, which are defined and proved valid (as in sound) in this section. When axioms apply
to arbitrary programs or formulas, they mention concrete program or formula
variables, which are then instantiated by uniform substitution, as opposed
metavariables.
This section contains axioms and rules for propositional connectives and programs other than
ODE's. Differential axioms are handled separately because the proofs are significantly more involved.
›
named_theorems axiom_defs "Axiom definitions"
definition assign_axiom :: "('sf, 'sc, 'sz) formula"
where [axiom_defs]:"assign_axiom ≡
([[vid1 := ($f fid1 empty)]] (Prop vid1 (singleton (Var vid1))))
↔ Prop vid1 (singleton ($f fid1 empty))"
definition diff_assign_axiom :: "('sf, 'sc, 'sz) formula"
where [axiom_defs]:"diff_assign_axiom ≡
([[DiffAssign vid1 ($f fid1 empty)]] (Prop vid1 (singleton (DiffVar vid1))))
↔ Prop vid1 (singleton ($f fid1 empty))"
definition loop_iterate_axiom :: "('sf, 'sc, 'sz) formula"
where [axiom_defs]:"loop_iterate_axiom ≡ ([[$α vid1**]]Predicational pid1)
↔ ((Predicational pid1) && ([[$α vid1]][[$α vid1**]]Predicational pid1))"
definition test_axiom :: "('sf, 'sc, 'sz) formula"
where [axiom_defs]:"test_axiom ≡
([[?($φ vid2 empty)]]$φ vid1 empty) ↔ (($φ vid2 empty) → ($φ vid1 empty))"
definition box_axiom :: "('sf, 'sc, 'sz) formula"
where [axiom_defs]:"box_axiom ≡ (⟨$α vid1⟩Predicational pid1) ↔ !([[$α vid1]]!(Predicational pid1))"
definition choice_axiom :: "('sf, 'sc, 'sz) formula"
where [axiom_defs]:"choice_axiom ≡ ([[$α vid1 ∪∪ $α vid2]]Predicational pid1)
↔ (([[$α vid1]]Predicational pid1) && ([[$α vid2]]Predicational pid1))"
definition compose_axiom :: "('sf, 'sc, 'sz) formula"
where [axiom_defs]:"compose_axiom ≡ ([[$α vid1 ;; $α vid2]]Predicational pid1) ↔
([[$α vid1]][[ $α vid2]]Predicational pid1)"
definition Kaxiom :: "('sf, 'sc, 'sz) formula"
where [axiom_defs]:"Kaxiom ≡ ([[$α vid1]]((Predicational pid1) → (Predicational pid2)))
→ ([[$α vid1]]Predicational pid1) → ([[$α vid1]]Predicational pid2)"
definition Iaxiom :: "('sf, 'sc, 'sz) formula"
where [axiom_defs]:"Iaxiom ≡
([[($α vid1)**]](Predicational pid1 → ([[$α vid1]]Predicational pid1)))
→((Predicational pid1 → ([[($α vid1)**]]Predicational pid1)))"
definition Vaxiom :: "('sf, 'sc, 'sz) formula"
where [axiom_defs]:"Vaxiom ≡ ($φ vid1 empty) → ([[$α vid1]]($φ vid1 empty))"
subsection ‹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›
theorem test_valid: "valid test_axiom"
by (auto simp add: valid_def test_axiom_def)
lemma assign_lem1:
"dterm_sem I (if i = vid1 then Var vid1 else (Const 0))
(vec_lambda (λy. if vid1 = y then Functions I fid1
(vec_lambda (λi. dterm_sem I (empty i) ν)) else vec_nth (fst ν) y), snd ν)
=
dterm_sem I (if i = vid1 then $f fid1 empty else (Const 0)) ν"
by (cases "i = vid1") (auto simp: proj_sing1)
lemma diff_assign_lem1:
"dterm_sem I (if i = vid1 then DiffVar vid1 else (Const 0))
(fst ν, vec_lambda (λy. if vid1 = y then Functions I fid1 (vec_lambda (λi. dterm_sem I (empty i) ν)) else vec_nth (snd ν) y))
=
dterm_sem I (if i = vid1 then $f fid1 empty else (Const 0)) ν
"
by (cases "i = vid1") (auto simp: proj_sing1)
theorem assign_valid: "valid assign_axiom"
unfolding valid_def assign_axiom_def
by (simp add: assign_lem1)
theorem diff_assign_valid: "valid diff_assign_axiom"
unfolding valid_def diff_assign_axiom_def
by (simp add: diff_assign_lem1)
lemma mem_to_nonempty: "ω ∈ S ⟹ (S ≠ {})"
by (auto)
lemma loop_forward: "ν ∈ fml_sem I ([[$α id1**]]Predicational pid1)
⟶ ν ∈ fml_sem I (Predicational pid1&&[[$α id1]][[$α id1**]]Predicational pid1)"
by (cases ν) (auto intro: converse_rtrancl_into_rtrancl simp add: box_sem)
lemma loop_backward:
"ν ∈ fml_sem I (Predicational pid1 && [[$α id1]][[$α id1**]]Predicational pid1)
⟶ ν ∈ fml_sem I ([[$α id1**]]Predicational pid1)"
by (auto elim: converse_rtranclE simp add: box_sem)
theorem loop_valid: "valid loop_iterate_axiom"
apply(simp only: valid_def loop_iterate_axiom_def)
apply(simp only: iff_sem)
apply(simp only: HOL.iff_conv_conj_imp)
apply(rule allI | rule impI)+
apply(rule conjI)
apply(rule loop_forward)
apply(rule loop_backward)
done
theorem box_valid: "valid box_axiom"
unfolding valid_def box_axiom_def by(auto)
theorem choice_valid: "valid choice_axiom"
unfolding valid_def choice_axiom_def by (auto)
theorem compose_valid: "valid compose_axiom"
unfolding valid_def compose_axiom_def by (auto)
theorem K_valid: "valid Kaxiom"
unfolding valid_def Kaxiom_def by (auto)
lemma I_axiom_lemma:
fixes I::"('sf,'sc,'sz) interp" and ν
assumes "is_interp I"
assumes IS:"ν ∈ fml_sem I ([[$α vid1**]](Predicational pid1 →
[[$α vid1]]Predicational pid1))"
assumes BC:"ν ∈ fml_sem I (Predicational pid1)"
shows "ν ∈ fml_sem I ([[$α vid1**]](Predicational pid1))"
proof -
have IS':"⋀ν2. (ν, ν2) ∈ (prog_sem I ($α vid1))⇧* ⟹ ν2 ∈ fml_sem I (Predicational pid1 → [[$α vid1]](Predicational pid1))"
using IS by (auto simp add: box_sem)
have res:"⋀ν3. ((ν, ν3) ∈ (prog_sem I ($α vid1))⇧*) ⟹ ν3 ∈ fml_sem I (Predicational pid1)"
proof -
fix ν3
show "((ν, ν3) ∈ (prog_sem I ($α vid1))⇧*) ⟹ ν3 ∈ fml_sem I (Predicational pid1)"
apply(induction rule:rtrancl_induct)
apply(rule BC)
proof -
fix y z
assume vy:"(ν, y) ∈ (prog_sem I ($α vid1))⇧*"
assume yz:"(y, z) ∈ prog_sem I ($α vid1)"
assume yPP:"y ∈ fml_sem I (Predicational pid1)"
have imp3:"y ∈ fml_sem I (Predicational pid1 → [[$α vid1 ]](Predicational pid1))"
using IS' vy by (simp)
have imp4:"y ∈ fml_sem I (Predicational pid1) ⟹ y ∈ fml_sem I ([[$α vid1]](Predicational pid1))"
using imp3 impl_sem by (auto)
have yaPP:"y ∈ fml_sem I ([[$α vid1]]Predicational pid1)" using imp4 yPP by auto
have zPP:"z ∈ fml_sem I (Predicational pid1)" using yaPP box_sem yz mem_Collect_eq by blast
show "
(ν, y) ∈ (prog_sem I ($α vid1))⇧* ⟹
(y, z) ∈ prog_sem I ($α vid1) ⟹
y ∈ fml_sem I (Predicational pid1) ⟹
z ∈ fml_sem I (Predicational pid1)" using zPP by simp
qed
qed
show "ν ∈ fml_sem I ([[$α vid1**]]Predicational pid1)"
using res by (simp add: mem_Collect_eq box_sem loop_sem)
qed
theorem I_valid: "valid Iaxiom"
apply(unfold Iaxiom_def valid_def)
apply(rule impI | rule allI)+
apply(simp only: impl_sem)
using I_axiom_lemma by blast
theorem V_valid: "valid Vaxiom"
apply(simp only: valid_def Vaxiom_def impl_sem box_sem)
apply(rule allI | rule impI)+
apply(auto simp add: empty_def)
done
definition G_holds :: "('sf, 'sc, 'sz) formula ⇒ ('sf, 'sc, 'sz) hp ⇒ bool"
where "G_holds φ α ≡ valid φ ⟶ valid ([[α]]φ)"
definition Skolem_holds :: "('sf, 'sc, 'sz) formula ⇒ 'sz ⇒ bool"
where "Skolem_holds φ var ≡ valid φ ⟶ valid (Forall var φ)"
definition MP_holds :: "('sf, 'sc, 'sz) formula ⇒ ('sf, 'sc, 'sz) formula ⇒ bool"
where "MP_holds φ ψ ≡ valid (φ → ψ) ⟶ valid φ ⟶ valid ψ"
definition CT_holds :: "'sf ⇒ ('sf, 'sz) trm ⇒ ('sf, 'sz) trm ⇒ bool"
where "CT_holds g θ θ' ≡ valid (Equals θ θ')
⟶ valid (Equals (Function g (singleton θ)) (Function g (singleton θ')))"
definition CQ_holds :: "'sz ⇒ ('sf, 'sz) trm ⇒ ('sf, 'sz) trm ⇒ bool"
where "CQ_holds p θ θ' ≡ valid (Equals θ θ')
⟶ valid ((Prop p (singleton θ)) ↔ (Prop p (singleton θ')))"
definition CE_holds :: "'sc ⇒ ('sf, 'sc, 'sz) formula ⇒ ('sf, 'sc, 'sz) formula ⇒ bool"
where "CE_holds var φ ψ ≡ valid (φ ↔ ψ)
⟶ valid (InContext var φ ↔ InContext var ψ)"
subsection ‹Soundness proofs for rules›
theorem G_sound: "G_holds φ α"
by (simp add: G_holds_def valid_def box_sem)
theorem Skolem_sound: "Skolem_holds φ var"
by (simp add: Skolem_holds_def valid_def)
theorem MP_sound: "MP_holds φ ψ"
by (auto simp add: MP_holds_def valid_def)
lemma CT_lemma:"⋀I::('sf::finite, 'sc::finite, 'sz::{finite,linorder}) interp. ⋀ a::(real, 'sz) vec. ⋀ b::(real, 'sz) vec. ∀I::('sf,'sc,'sz) interp. is_interp I ⟶ (∀a b. dterm_sem I θ (a, b) = dterm_sem I θ' (a, b)) ⟹
is_interp I ⟹
Functions I var (vec_lambda (λi. dterm_sem I (if i = vid1 then θ else (Const 0)) (a, b))) =
Functions I var (vec_lambda (λi. dterm_sem I (if i = vid1 then θ' else (Const 0)) (a, b)))"
proof -
fix I :: "('sf::finite, 'sc::finite, 'sz::{finite,linorder}) interp" and a :: "(real, 'sz) vec" and b :: "(real, 'sz) vec"
assume a1: "is_interp I"
assume "∀I::('sf,'sc,'sz) interp. is_interp I ⟶ (∀a b. dterm_sem I θ (a, b) = dterm_sem I θ' (a, b))"
then have "∀i. dterm_sem I (if i = vid1 then θ' else (Const 0)) (a, b) = dterm_sem I (if i = vid1 then θ else (Const 0)) (a, b)"
using a1 by presburger
then show "Functions I var (vec_lambda (λi. dterm_sem I (if i = vid1 then θ else (Const 0)) (a, b)))
= Functions I var (vec_lambda (λi. dterm_sem I (if i = vid1 then θ' else (Const 0)) (a, b)))"
by presburger
qed
theorem CT_sound: "CT_holds var θ θ'"
apply(simp only: CT_holds_def valid_def equals_sem vec_extensionality vec_eq_iff)
apply(simp)
apply(rule allI | rule impI)+
apply(simp add: CT_lemma)
done
theorem CQ_sound: "CQ_holds var θ θ'"
proof (auto simp only: CQ_holds_def valid_def equals_sem vec_extensionality vec_eq_iff singleton.simps mem_Collect_eq)
fix I :: "('sf,'sc,'sz) interp" and a b
assume sem:"∀I::('sf,'sc,'sz) interp. ∀ ν. is_interp I ⟶ dterm_sem I θ ν = dterm_sem I θ' ν"
assume good:"is_interp I"
have sem_eq:"dterm_sem I θ (a,b) = dterm_sem I θ' (a,b)"
using sem good by auto
have feq:"(χ i. dterm_sem I (if i = vid1 then θ else Const 0) (a, b)) = (χ i. dterm_sem I (if i = vid1 then θ' else Const 0) (a, b))"
apply(rule vec_extensionality)
using sem_eq by auto
then show "(a, b) ∈ fml_sem I ($φ var (singleton θ) ↔ $φ var (singleton θ'))"
by auto
qed
theorem CE_sound: "CE_holds var φ ψ"
apply(simp only: CE_holds_def valid_def iff_sem)
apply(rule allI | rule impI)+
apply(simp)
apply(metis subsetI subset_antisym surj_pair)
done
end end