header "Reasoning about PreFormulas"
theory PreFormulas
imports Semantics
begin
text{*
Semantic separation of formulas and pre-formulas requires a deep embedding.
We introduce a syntactically distinct notion of validity, written @{text "|~ A"},
for pre-formulas. Although it is semantically identical to @{text "\<turnstile> A"}, it
helps users distinguish pre-formulas from formulas in \tlastar{} proofs.
*}
definition PreValid :: "('w::world) form => bool"
where "PreValid A ≡ ∀ w. w \<Turnstile> A"
syntax
"_PreValid" :: "lift => bool" ("(|~ _)" 5)
translations
"_PreValid" \<rightleftharpoons> "CONST PreValid"
lemma prefD[dest]: "|~ A ==> w \<Turnstile> A"
by (simp add: PreValid_def)
lemma prefI[intro!]: "(!! w. w \<Turnstile> A) ==> |~ A"
by (simp add: PreValid_def)
method_setup pref_unlift = {* Scan.succeed
(K (SIMPLE_METHOD ((rtac @{thm prefI} THEN' rewrite_goal_tac @{thms intensional_rews}) 1))) *}
"int_unlift for PreFormulas"
lemma prefeq_reflection: assumes P1: "|~ x=y" shows "(x ≡ y)"
using P1 by (intro eq_reflection) force
lemma pref_True[simp]: "|~ #True"
by auto
lemma pref_eq: "|~ X = Y ==> X = Y"
by (auto simp: prefeq_reflection)
lemma pref_iffI:
assumes "|~ F --> G" and "|~ G --> F"
shows "|~ F = G"
using assms by force
lemma pref_iffD1: assumes "|~ F = G" shows "|~ F --> G"
using assms by auto
lemma pref_iffD2: assumes "|~ F = G" shows "|~ G --> F"
using assms by auto
lemma unl_pref_imp:
assumes "|~ F --> G" shows "!! w. w \<Turnstile> F ==> w \<Turnstile> G"
using assms by auto
lemma pref_imp_trans:
assumes "|~ F --> G" and "|~ G --> H"
shows "|~ F --> H"
using assms by force
subsection "Lemmas about @{text Unchanged}"
text {*
Many of the \tlastar{} axioms only require a state function witness
which leaves the state space unchanged. An obvious witness is the
@{term id} function. The lemmas require that the given formula is
invariant under stuttering.
*}
lemma pre_id_unch: assumes h: "stutinv F"
shows "|~ F ∧ Unchanged id --> oF"
proof (pref_unlift, clarify)
fix s
assume a1: "s \<Turnstile> F" and a2: "s \<Turnstile> Unchanged id"
from a2 have "(id (second s) = id (first s))" by (simp add: unch_defs)
hence "s ≈ (tail s)" by (simp add: addfirststut)
with h a1 have "(tail s) \<Turnstile> F" by (simp add: stutinv_def)
thus "s \<Turnstile> oF" by (unfold nexts_def)
qed
lemma pre_ex_unch:
assumes h: "stutinv F"
shows "∃(v::'a::world => 'a). ( |~ F ∧ Unchanged v --> oF)"
using pre_id_unch[OF h] by blast
lemma unch_pair: "|~ Unchanged (x,y) = (Unchanged x ∧ Unchanged y)"
by (auto simp: unch_def before_def after_def nexts_def)
lemmas unch_eq1 = unch_pair[THEN pref_eq]
lemmas unch_eq2 = unch_pair[THEN prefeq_reflection]
lemma angle_actrans_sem: "|~ ⟨F⟩_v = (F ∧ v$ ≠ $v)"
by (auto simp: angle_actrans_def actrans_def unch_def)
lemmas angle_actrans_sem_eq = angle_actrans_sem[THEN pref_eq]
subsection "Lemmas about @{text after}"
lemma after_const: "|~ (#c)` = #c"
by (auto simp: nexts_def before_def after_def)
lemma after_fun1: "|~ f<x>` = f<x`>"
by (auto simp: nexts_def before_def after_def)
lemma after_fun2: "|~ f<x,y>` = f <x`,y`>"
by (auto simp: nexts_def before_def after_def)
lemma after_fun3: "|~ f<x,y,z>` = f <x`,y`,z`>"
by (auto simp: nexts_def before_def after_def)
lemma after_fun4: "|~ f<x,y,z,zz>` = f <x`,y`,z`,zz`>"
by (auto simp: nexts_def before_def after_def)
lemma after_forall: "|~ (∀ x. P x)` = (∀ x. (P x)`)"
by (auto simp: nexts_def before_def after_def)
lemma after_exists: "|~ (∃ x. P x)` = (∃ x. (P x)`)"
by (auto simp: nexts_def before_def after_def)
lemma after_exists1: "|~ (∃! x. P x)` = (∃! x. (P x)`)"
by (auto simp: nexts_def before_def after_def)
lemmas all_after = after_const after_fun1 after_fun2 after_fun3 after_fun4
after_forall after_exists after_exists1
lemmas all_after_unl = all_after[THEN prefD]
lemmas all_after_eq = all_after[THEN prefeq_reflection]
subsection "Lemmas about @{text before}"
lemma before_const: "\<turnstile> $(#c) = #c"
by (auto simp: before_def)
lemma before_fun1: "\<turnstile> $(f<x>) = f <$x>"
by (auto simp: before_def)
lemma before_fun2: "\<turnstile> $(f<x,y>) = f <$x,$y>"
by (auto simp: before_def)
lemma before_fun3: "\<turnstile> $(f<x,y,z>) = f <$x,$y,$z>"
by (auto simp: before_def)
lemma before_fun4: "\<turnstile> $(f<x,y,z,zz>) = f <$x,$y,$z,$zz>"
by (auto simp: before_def)
lemma before_forall: "\<turnstile> $(∀ x. P x) = (∀ x. $(P x))"
by (auto simp: before_def)
lemma before_exists: "\<turnstile> $(∃ x. P x) = (∃ x. $(P x))"
by (auto simp: before_def)
lemma before_exists1: "\<turnstile> $(∃! x. P x) = (∃! x. $(P x))"
by (auto simp: before_def)
lemmas all_before = before_const before_fun1 before_fun2 before_fun3 before_fun4
before_forall before_exists before_exists1
lemmas all_before_unl = all_before[THEN intD]
lemmas all_before_eq = all_before[THEN inteq_reflection]
subsection "Some general properties"
lemma angle_actrans_conj: "|~ (⟨F ∧ G⟩_v) = (⟨F⟩_v ∧ ⟨G⟩_v)"
by (auto simp: angle_actrans_def actrans_def unch_def)
lemma angle_actrans_disj: "|~ (⟨F ∨ G⟩_v) = (⟨F⟩_v ∨ ⟨G⟩_v)"
by (auto simp: angle_actrans_def actrans_def unch_def)
lemma int_eq_true: "\<turnstile> P ==> \<turnstile> P = #True"
by auto
lemma pref_eq_true: "|~ P ==> |~ P = #True"
by auto
subsection "Unlifting attributes and methods"
text {* Attribute which unlifts an intensional formula or preformula *}
ML {*
fun unl_rewr thm =
let
val unl = (thm RS @{thm intD}) handle THM _ => (thm RS @{thm prefD})
handle THM _ => thm
val rewr = rewrite_rule @{thms intensional_rews}
in
unl |> rewr
end;
val att_unl_tac = Thm.rule_attribute (fn _ => unl_rewr);
val att_unl_rule_tac = Thm.rule_attribute (fn _ => Object_Logic.rulify o unl_rewr);
*}
attribute_setup unlifted = {* Scan.succeed att_unl_tac *}
"attribute to unlift intensional formulas"
attribute_setup unlift_rule = {* Scan.succeed att_unl_rule_tac *}
"attribute to unlift and rulify intensional formulas"
text {*
Attribute which turns an intensional formula or preformula into a rewrite rule.
Formulas @{text F} that are not equalities are turned into @{text "F ≡ #True"}.
*}
ML {*
fun int_rewr thm =
(thm RS @{thm inteq_reflection})
handle THM _ => (thm RS @{thm prefeq_reflection})
handle THM _ => ((thm RS @{thm int_eq_true}) RS @{thm inteq_reflection})
handle THM _ => ((thm RS @{thm pref_eq_true}) RS @{thm prefeq_reflection});
val att_int_rew_tac =
Thm.rule_attribute (fn _ => int_rewr)
val add_intensional_simp = Thm.declaration_attribute (fn th => Simplifier.map_ss (Simplifier.add_simp (int_rewr th)));
fun empty_attribute _ = (NONE, NONE);
*}
attribute_setup simp_unl = {* Attrib.add_del add_intensional_simp empty_attribute *}
"adds thm unlifted from rewrites from intensional formulas or preformulas"
attribute_setup int_rewrite = {* Scan.succeed att_int_rew_tac *}
"attribute to produce rewrites from intensional formulas or preformulas"
end