Theory PreFormulas

(*  Title:       A Definitional Encoding of TLA in Isabelle/HOL
    Authors:     Gudmund Grov <ggrov at inf.ed.ac.uk>
                 Stephan Merz <Stephan.Merz at loria.fr>
    Year:        2011
    Maintainer:  Gudmund Grov <ggrov at inf.ed.ac.uk>
*)

section "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 ‹|~ A›,
  for pre-formulas. Although it is semantically identical to ‹⊢ A›, it
  helps users distinguish pre-formulas from formulas in \tlastar{} proofs.
›

definition PreValid :: "('w::world) form ⇒ bool"
where "PreValid A ≡ ∀ w. w ⊨ A"

syntax
  "_PreValid"      :: "lift ⇒ bool"     ("(|~ _)" 5)

translations
  "_PreValid"  ⇌ "CONST PreValid"

lemma prefD[dest]: "|~ A ⟹ w ⊨ A"
  by (simp add: PreValid_def)

lemma prefI[intro!]: "(⋀ w. w ⊨ A) ⟹ |~ A"
  by (simp add: PreValid_def)

method_setup pref_unlift = ‹
  Scan.succeed (fn ctxt => SIMPLE_METHOD'
    (resolve_tac ctxt @{thms prefI} THEN' rewrite_goal_tac ctxt @{thms intensional_rews}))
› "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 ⊨ F ⟹ w ⊨ 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 ‹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 ⟶ ○F"
proof (pref_unlift, clarify)
  fix s
  assume a1: "s ⊨ F" and  a2: "s ⊨ 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) ⊨ F" by (simp add: stutinv_def)
  thus "s ⊨ ○F" by (unfold nexts_def)
qed

lemma pre_ex_unch: 
  assumes h: "stutinv F"
  shows "∃(v::'a::world ⇒ 'a). ( |~ F ∧ Unchanged v ⟶ ○F)"
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 ‹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 ‹before›"

lemma before_const: "⊢ $(#c) = #c"
  by (auto simp: before_def)

lemma before_fun1: "⊢ $(f<x>) = f <$x>"
  by (auto simp: before_def)

lemma before_fun2: "⊢ $(f<x,y>) = f <$x,$y>"
  by (auto simp: before_def)

lemma before_fun3: "⊢ $(f<x,y,z>) = f <$x,$y,$z>"
  by (auto simp: before_def)

lemma before_fun4: "⊢ $(f<x,y,z,zz>) = f <$x,$y,$z,$zz>"
  by (auto simp: before_def)

lemma before_forall: "⊢ $(∀ x. P x) = (∀ x. $(P x))"
  by (auto simp: before_def)

lemma before_exists: "⊢ $(∃ x. P x) = (∃ x. $(P x))"
  by (auto simp: before_def)

lemma before_exists1: "⊢ $(∃! 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: "⊢ P ⟹ ⊢ 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 ctxt thm = 
    let
       val unl = (thm RS @{thm intD}) handle THM _ => (thm RS @{thm prefD})
                                      handle THM _ => thm
       val rewr = rewrite_rule ctxt @{thms intensional_rews} 
     in
       unl |> rewr
     end;
›
attribute_setup unlifted = ‹
  Scan.succeed (Thm.rule_attribute [] (unl_rewr o Context.proof_of))
› "unlift intensional formulas"

attribute_setup unlift_rule = ‹
  Scan.succeed
    (Thm.rule_attribute []
      (Context.proof_of #> (fn ctxt => Object_Logic.rulify ctxt o unl_rewr ctxt)))
› "unlift and rulify intensional formulas"


text ‹
  Attribute which turns an intensional formula or preformula into a rewrite rule.
  Formulas ‹F› that are not equalities are turned into ‹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});
›

attribute_setup simp_unl = ‹
    Attrib.add_del
      (Thm.declaration_attribute
        (fn th => Simplifier.map_ss (Simplifier.add_simp (int_rewr th))))
      (K (NONE, NONE))  (* note only adding -- removing is ignored *)
› "add thm unlifted from rewrites from intensional formulas or preformulas"

attribute_setup int_rewrite = ‹Scan.succeed (Thm.rule_attribute [] (fn _ => int_rewr))›
  "produce rewrites from intensional formulas or preformulas"

end