Quelle  PreFormulas.thy

(*  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.
\<close>

lemma pre_id_unch: assumes h: "  F"
 shows "|~ F ∧ Unchanged id ⟶ ◯F"
  (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)
 

  pre_ex_unch:
 assumes h: "stutinv F"
 shows "∃(v::'a::world ==> 'a). ( |~ F ∧ Unchanged v ⟶ ◯F)"
  pre_id_unch[OF h] by blast

  unch_pair: "|~ Unchanged (x,y) = (Unchanged x ∧ Unchanged y)"
 by (auto simp: unch_def before_def after_def nexts_def)

  unch_eq1 = unch_pair[THEN pref_eq]
  unch_eq2 = unch_pair[THEN prefeq_reflection]

  angle_actrans_sem: "|~ ⟨F⟩_v = (F ∧ v$ ≠ $v)"
 by (auto simp: angle_actrans_def actrans_def unch_def)

  angle_actrans_sem_eq = angle_actrans_sem[THEN pref_eq]

  "Lemmas about ‹after›"

  after_const: "|~ (#c)` = #c"
 by (auto simp: nexts_def before_def after_def)

  after_fun1: "|~ fx` = f<x`>"
 by (auto simp: nexts_def before_def after_def)

  after_fun2: "|~ f<x,y>` = f <x`,y`>"
 by (auto simp: nexts_def before_def after_def)

  after_fun3: "|~ f<x,y,z>` = f <x`,y`,z`>"
 by (auto simp: nexts_def before_def after_def)

  after_fun4: "|~ f<x,y,z,zz>` = f <x`,y`,z`,zz`>"
 by (auto simp: nexts_def before_def after_def)

  after_forall: "|~ (∀ x. P x)` = (∀ x. (P x)`)"
 by (auto simp: nexts_def before_def after_def)

  after_exists: "|~ (∃ x. P x)` = (∃ x. (P x)`)"
 by (auto simp: nexts_def before_def after_def)

  after_exists1: "|~ (∃! x. P x)` = (∃! x. (P x)`)"
 by (auto simp: nexts_def before_def after_def)

  all_after = after_const after_fun1 after_fun2 after_fun3 after_fun4
 after_forall after_exists after_exists1

  all_after_unl = all_after[THEN prefD]
  all_after_eq = all_after[THEN prefeq_reflection]

  "Lemmas about ‹before›"

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

  before_fun1: "⊨ $(fx) = f <$x>"
 by (auto simp: before_def)

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

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

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

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

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

  before_exists1: "⊨ $(∃! x. P x) = (∃! x. $(P x))"
 by (auto simp: before_def)


  all_before = before_const before_fun1 before_fun2 before_fun3 before_fun4
 before_forall before_exists before_exists1

  all_before_unl = all_before[THEN intD]
  all_before_eq = all_before[THEN inteq_reflection]

  "Some general properties"

  angle_actrans_conj: "|~ (⟨F ∧ G⟩_v) = (⟨F⟩_v ∧ ⟨G⟩_v)"
 by (auto simp: angle_actrans_def actrans_def unch_def)

  angle_actrans_disj: "|~ (⟨F ∨ G⟩_v) = (⟨F⟩_v ∨ ⟨G⟩_v)"
 by (auto simp: angle_actrans_def actrans_def unch_def)

  int_eq_true: "⊨ P ==> ⊨ P = #True"
 by auto

  pref_eq_true: "|~ P ==> |~ P = #True"
 by auto

  "Unlifting attributes and methods"

  ‹Attribute which unlifts an intensional formula or preformula›
  ‹
  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;
 ›
  unlifted = ‹
 Scan.succeed (Thm.rule_attribute [] (unl_rewr o Context.proof_of))
 › "unlift intensional formulas"

  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"


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

  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