Theory Intensional

(*  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 ‹Representing Intensional Logic›

theory Intensional 
imports Main
begin

text‹
  In higher-order logic, every proof rule has a corresponding tautology, i.e.
  the \emph{deduction theorem} holds. Isabelle/HOL implements this since object-level
  implication ($\longrightarrow$) and meta-level entailment ($\Longrightarrow$) 
  commute, viz. the proof rule ‹impI:› @{thm impI}. 
  However, the deduction theorem does not hold for 
  most modal and temporal logics \<^cite>‹‹page 95› in "Lamport02"›\<^cite>‹"Merz98"›.
  For example $A \vdash \Box A$ holds, meaning that if $A$ holds in any world, then
  it always holds. However, $\vdash A \longrightarrow \Box A$, stating that 
  $A$ always holds if it initially holds, is not valid.

  Merz  \<^cite>‹"Merz98"› overcame this problem by creating an
  @{term Intensional} logic. It exploits Isabelle's 
  axiomatic type class feature  \<^cite>‹"Wenzel00b"› by creating a type
  class @{term world}, which provides Skolem constants to associate formulas
  with the world they hold in. The class is trivial, not requiring any axioms.
›

class world 
text ‹
  @{term world} is a type class of possible worlds. It is a subclass
  of all HOL types @{term type}. No axioms are provided, since its only
  purpose is to avoid silly use of the @{term Intensional} syntax.
›

subsection‹Abstract Syntax and Definitions›


type_synonym ('w,'a) expr = "'w ⇒ 'a"         
type_synonym  'w form = "('w, bool) expr"

text ‹The intention is that @{typ 'a} will be used for unlifted
types (class @{term type}), while @{typ 'w} is lifted (class @{term world}). 
›


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

definition const :: "'a ⇒ ('w::world, 'a) expr"
  where unl_con: "const c w ≡ c"

definition lift :: "['a ⇒ 'b, ('w::world, 'a) expr] ⇒ ('w,'b) expr"
  where unl_lift: "lift f x w ≡ f (x w)"

definition lift2 :: "['a ⇒ 'b ⇒ 'c, ('w::world,'a) expr, ('w,'b) expr] ⇒ ('w,'c) expr"
  where unl_lift2: "lift2 f x y w ≡ f (x w) (y w)"

definition lift3 :: "['a ⇒ 'b => 'c ⇒ 'd, ('w::world,'a) expr, ('w,'b) expr, ('w,'c) expr] ⇒ ('w,'d) expr"
  where unl_lift3: "lift3 f x y z w ≡ f (x w) (y w) (z w)"

definition lift4 :: "['a ⇒ 'b => 'c ⇒ 'd ⇒ 'e, ('w::world,'a) expr, ('w,'b) expr, ('w,'c) expr,('w,'d) expr] ⇒ ('w,'e) expr"
  where unl_lift4: "lift4 f x y z zz w ≡ f (x w) (y w) (z w) (zz w)"

text ‹
  @{term "Valid F"} asserts that the lifted formula @{term F} holds everywhere.
  @{term const} allows lifting of a constant, while @{term lift} through
  @{term lift4} allow functions with arity 1--4 to be lifted. (Note that there
  is no way to define a generic lifting operator for functions of arbitrary arity.)
›

definition RAll :: "('a ⇒ ('w::world) form) ⇒ 'w form"  (binder ‹Rall › 10)
  where unl_Rall: "(Rall x. A x) w ≡ ∀x. A x w"

definition REx :: "('a ⇒ ('w::world) form) ⇒ 'w form"  (binder ‹Rex › 10)
  where unl_Rex: "(Rex x. A x) w ≡ ∃x. A x w"

definition REx1 :: "('a ⇒ ('w::world) form) ⇒ 'w form"  (binder ‹Rex! › 10)
  where unl_Rex1: "(Rex! x. A x) w ≡ ∃!x. A x w"

text ‹
  @{term RAll}, @{term REx} and @{term REx1} introduces ``rigid'' quantification
  over values (of non-world types) within ``intensional'' formulas. @{term RAll}
  is universal quantification, @{term REx} is existential quantifcation.
  @{term REx1} requires unique existence.
›

text ‹
  We declare the ``unlifting rules'' as rewrite rules that will be applied
  automatically.
›

lemmas intensional_rews[simp] = 
  unl_con unl_lift unl_lift2 unl_lift3 unl_lift4 
  unl_Rall unl_Rex unl_Rex1



subsection‹Concrete Syntax›

nonterminal
  lift and liftargs

text‹
  The non-terminal @{term lift} represents lifted expressions. The idea is to use 
  Isabelle's macro mechanism to convert between the concrete and abstract syntax.
›

syntax
  ""            :: "id ⇒ lift"                          (‹_›)
  ""            :: "longid ⇒ lift"                      (‹_›)
  ""            :: "var ⇒ lift"                         (‹_›)
  "_applC"      :: "[lift, cargs] ⇒ lift"               (‹(1_/ _)› [1000, 1000] 999)
  ""            :: "lift ⇒ lift"                        (‹'(_')›)
  "_lambda"     :: "[idts, 'a] ⇒ lift"                  (‹(3%_./ _)› [0, 3] 3)
  "_constrain"  :: "[lift, type] ⇒ lift"                (‹(_::_)› [4, 0] 3)
  ""            :: "lift ⇒ liftargs"                    (‹_›)
  "_liftargs"   :: "[lift, liftargs] ⇒ liftargs"        (‹_,/ _›)
  "_Valid"      :: "lift ⇒ bool"                        (‹(⊢ _)› 5)
  "_holdsAt"    :: "['a, lift] ⇒ bool"                  (‹(_ ⊨ _)› [100,10] 10)

  (* Syntax for lifted expressions outside the scope of ⊢ or ⊨.*)
  "LIFT"        :: "lift ⇒ 'a"                          (‹LIFT _›)

  (* generic syntax for lifted constants and functions *)
  "_const"      :: "'a ⇒ lift"                          (‹(#_)› [1000] 999)
  "_lift"       :: "['a, lift] ⇒ lift"                  (‹(_<_>)› [1000] 999)
  "_lift2"      :: "['a, lift, lift] ⇒ lift"            (‹(_<_,/ _>)› [1000] 999)
  "_lift3"      :: "['a, lift, lift, lift] ⇒ lift"      (‹(_<_,/ _,/ _>)› [1000] 999)
  "_lift4"      :: "['a, lift, lift, lift,lift] ⇒ lift"      (‹(_<_,/ _,/ _,/ _>)› [1000] 999)

  (* concrete syntax for common infix functions: reuse same symbol *)
  "_liftEqu"    :: "[lift, lift] ⇒ lift"                (‹(_ =/ _)› [50,51] 50)
  "_liftNeq"    :: "[lift, lift] ⇒ lift"                (infixl ‹≠› 50)
  "_liftNot"    :: "lift ⇒ lift"                        (‹¬ _› [90] 90)
  "_liftAnd"    :: "[lift, lift] ⇒ lift"                (infixr ‹∧› 35)
  "_liftOr"     :: "[lift, lift] ⇒ lift"                (infixr ‹∨› 30)
  "_liftImp"    :: "[lift, lift] ⇒ lift"                (infixr ‹⟶› 25)
  "_liftIf"     :: "[lift, lift, lift] ⇒ lift"          (‹(if (_)/ then (_)/ else (_))› 10)
  "_liftPlus"   :: "[lift, lift] ⇒ lift"                (‹(_ +/ _)› [66,65] 65)
  "_liftMinus"  :: "[lift, lift] ⇒ lift"                (‹(_ -/ _)› [66,65] 65)
  "_liftTimes"  :: "[lift, lift] ⇒ lift"                (‹(_ */ _)› [71,70] 70)
  "_liftDiv"    :: "[lift, lift] ⇒ lift"                (‹(_ div _)› [71,70] 70)
  "_liftMod"    :: "[lift, lift] ⇒ lift"                (‹(_ mod _)› [71,70] 70)
  "_liftLess"   :: "[lift, lift] ⇒ lift"                (‹(_/ < _)›  [50, 51] 50)
  "_liftLeq"    :: "[lift, lift] ⇒ lift"                (‹(_/ ≤ _)› [50, 51] 50)
  "_liftMem"    :: "[lift, lift] ⇒ lift"                (‹(_/ ∈ _)› [50, 51] 50)
  "_liftNotMem" :: "[lift, lift] ⇒ lift"                (‹(_/ ∉ _)› [50, 51] 50)
  "_liftFinset" :: "liftargs => lift"                    (‹{(_)}›)
  (** TODO: syntax for lifted collection / comprehension **)
  "_liftPair"   :: "[lift,liftargs] ⇒ lift"                   (‹(1'(_,/ _'))›)
  (* infix syntax for list operations *)
  "_liftCons" :: "[lift, lift] ⇒ lift"                  (‹(_ #/ _)› [65,66] 65)
  "_liftApp"  :: "[lift, lift] ⇒ lift"                  (‹(_ @/ _)› [65,66] 65)
  "_liftList" :: "liftargs ⇒ lift"                      (‹[(_)]›)

  (* Rigid quantification (syntax level) *)
  "_ARAll"  :: "[idts, lift] ⇒ lift"                    (‹(3! _./ _)› [0, 10] 10)
  "_AREx"   :: "[idts, lift] ⇒ lift"                    (‹(3? _./ _)› [0, 10] 10)
  "_AREx1"  :: "[idts, lift] ⇒ lift"                    (‹(3?! _./ _)› [0, 10] 10)
  "_RAll"       :: "[idts, lift] ⇒ lift"                (‹(3∀_./ _)› [0, 10] 10)
  "_REx"        :: "[idts, lift] ⇒ lift"                (‹(3∃_./ _)› [0, 10] 10)
  "_REx1"       :: "[idts, lift] ⇒ lift"                (‹(3∃!_./ _)› [0, 10] 10)

translations
  "_const"        ⇌  "CONST const"

translations
  "_lift"         ⇌ "CONST lift"
  "_lift2"        ⇌ "CONST lift2"
  "_lift3"        ⇌ "CONST lift3"
  "_lift4"        ⇌ "CONST lift4"
  "_Valid"        ⇌ "CONST Valid"

translations
  "_RAll x A"     ⇌ "Rall x. A"
  "_REx x A"      ⇌ "Rex x. A"
  "_REx1 x A"     ⇌ "Rex! x. A"

translations
  "_ARAll"        ⇀  "_RAll"
  "_AREx"         ⇀ "_REx"
  "_AREx1"        ⇀ "_REx1"

  "w ⊨ A"        ⇀ "A w"
  "LIFT A"        ⇀ "A::_⇒_"

translations
  "_liftEqu"      ⇌ "_lift2 (=)"
  "_liftNeq u v"  ⇌ "_liftNot (_liftEqu u v)"
  "_liftNot"      ⇌ "_lift (CONST Not)"
  "_liftAnd"      ⇌ "_lift2 (&)"
  "_liftOr"       ⇌ "_lift2 ((|) )"
  "_liftImp"      ⇌ "_lift2 (-->)"
  "_liftIf"       ⇌ "_lift3 (CONST If)"
  "_liftPlus"     ⇌ "_lift2 (+)"
  "_liftMinus"    ⇌ "_lift2 (-)"
  "_liftTimes"    ⇌ "_lift2 (*)"
  "_liftDiv"      ⇌ "_lift2 (div)"
 "_liftMod"      ⇌ "_lift2 (mod)"
  "_liftLess"     ⇌ "_lift2 (<)"
  "_liftLeq"      ⇌ "_lift2 (<=)"
  "_liftMem"      ⇌ "_lift2 (:)"
  "_liftNotMem x xs"             ⇌ "_liftNot (_liftMem x xs)"

translations
  "_liftFinset (_liftargs x xs)" ⇌ "_lift2 (CONST insert) x (_liftFinset xs)"
  "_liftFinset x"                ⇌ "_lift2 (CONST insert) x (_const (CONST Set.empty))"
  "_liftPair x (_liftargs y z)"  ⇌ "_liftPair x (_liftPair y z)"
  "_liftPair"                    ⇌ "_lift2 (CONST Pair)"
  "_liftCons"                    ⇌ "_lift2 (CONST Cons)"
  "_liftApp"                     ⇌ "_lift2 (@)"
  "_liftList (_liftargs x xs)"   ⇌ "_liftCons x (_liftList xs)"
  "_liftList x"                  ⇌ "_liftCons x (_const [])"

  "w ⊨ ¬ A" ↽ "_liftNot A w"
  "w ⊨ A ∧ B" ↽ "_liftAnd A B w"
  "w ⊨ A ∨ B" ↽ "_liftOr A B w"
  "w ⊨ A ⟶ B" ↽ "_liftImp A B w"
  "w ⊨ u = v" ↽ "_liftEqu u v w"
  "w ⊨ ∀x. A" ↽ "_RAll x A w"
  "w ⊨ ∃x. A" ↽ "_REx x A w"
  "w ⊨ ∃!x. A" ↽ "_REx1 x A w"

syntax (ASCII)
  "_Valid"      :: "lift ⇒ bool"                        (‹(|- _)› 5)
  "_holdsAt"    :: "['a, lift] ⇒ bool"                  (‹(_ |= _)› [100,10] 10)
  "_liftNeq"    :: "[lift, lift] ⇒ lift"                (‹(_ ~=/ _)› [50,51] 50)
  "_liftNot"    :: "lift ⇒ lift"                        (‹(~ _)› [90] 90)
  "_liftAnd"    :: "[lift, lift] ⇒ lift"                (‹(_ &/ _)› [36,35] 35)
  "_liftOr"     :: "[lift, lift] ⇒ lift"                (‹(_ |/ _)› [31,30] 30)
  "_liftImp"    :: "[lift, lift] ⇒ lift"                (‹(_ -->/ _)› [26,25] 25)
  "_liftLeq"    :: "[lift, lift] ⇒ lift"                (‹(_/ <= _)› [50, 51] 50)
  "_liftMem"    :: "[lift, lift] ⇒ lift"                (‹(_/ : _)› [50, 51] 50)
  "_liftNotMem" :: "[lift, lift] ⇒ lift"                (‹(_/ ~: _)› [50, 51] 50)
  "_RAll" :: "[idts, lift] ⇒ lift"                      (‹(3ALL _./ _)› [0, 10] 10)
  "_REx"  :: "[idts, lift] ⇒ lift"                      (‹(3EX _./ _)› [0, 10] 10)
  "_REx1" :: "[idts, lift] ⇒ lift"                      (‹(3EX! _./ _)› [0, 10] 10)


subsection ‹Lemmas and Tactics›

lemma intD[dest]: "⊢ A ⟹ w ⊨ A"
proof -
  assume a:"⊢ A"
  from a have "∀w. w ⊨ A" by (auto simp add: Valid_def)
  thus ?thesis ..
qed

lemma intI [intro!]: assumes P1:"(⋀ w. w ⊨ A)" shows "⊢ A"
  using assms by (auto simp: Valid_def)

text‹
  Basic unlifting introduces a parameter @{term w} and applies basic rewrites, e.g 
  @{term "⊢ F = G"} becomes @{term "F w = G w"} and @{term "⊢ F ⟶ G"} becomes   
  @{term "F w ⟶ G w"}.
›

method_setup int_unlift = ‹
  Scan.succeed (fn ctxt => SIMPLE_METHOD'
    (resolve_tac ctxt @{thms intI} THEN' rewrite_goal_tac ctxt @{thms intensional_rews}))
› "method to unlift and followed by intensional rewrites"

lemma inteq_reflection: assumes P1: "⊢ x=y" shows  "(x ≡ y)"
proof -
  from P1 have P2: "∀w. x w = y w" by (unfold Valid_def unl_lift2)
  hence P3:"x=y" by blast
  thus "x ≡ y" by (rule "eq_reflection")
qed

lemma int_simps:
  "⊢ (x=x) = #True"
  "⊢ (¬ #True) = #False"
  "⊢ (¬ #False) = #True"
  "⊢ (¬¬ P) = P"
  "⊢ ((¬ P) = P) = #False"
  "⊢ (P = (¬P)) = #False"
  "⊢ (P ≠ Q) = (P = (¬ Q))"
  "⊢ (#True=P) = P"
  "⊢ (P=#True) = P"
  "⊢ (#True ⟶ P) = P"
  "⊢ (#False ⟶ P) = #True"
  "⊢ (P ⟶ #True) = #True"
  "⊢ (P ⟶ P) = #True"
  "⊢ (P ⟶ #False) = (¬P)"
  "⊢ (P ⟶ ~P) = (¬P)"
  "⊢ (P ∧ #True) = P"
  "⊢ (#True ∧ P) = P"
  "⊢ (P ∧ #False) = #False"
  "⊢ (#False ∧ P) = #False"
  "⊢ (P ∧ P) = P"
  "⊢ (P ∧ ~P) = #False"
  "⊢ (¬P ∧ P) = #False"
  "⊢ (P ∨ #True) = #True"
  "⊢ (#True ∨ P) = #True"
  "⊢ (P ∨ #False) = P"
  "⊢ (#False ∨ P) = P"
  "⊢ (P ∨ P) = P"
  "⊢ (P ∨ ¬P) = #True"
  "⊢ (¬P ∨ P) = #True"
  "⊢ (∀ x. P) = P"
  "⊢ (∃ x. P) = P"
  by auto

lemmas intensional_simps[simp] = int_simps[THEN inteq_reflection]

method_setup int_rewrite = ‹
  Scan.succeed (fn ctxt => SIMPLE_METHOD' (rewrite_goal_tac ctxt @{thms intensional_simps}))
› "rewrite method at intensional level"

lemma Not_Rall: "⊢ (¬(∀ x. F x)) = (∃ x. ¬F x)"
  by auto

lemma Not_Rex: "⊢ (¬(∃ x. F x)) = (∀ x. ¬F x)"
  by auto

lemma TrueW [simp]: "⊢ #True"
  by auto

lemma int_eq: "⊢ X = Y ⟹ X = Y"
  by (auto simp: inteq_reflection)

lemma int_iffI: 
  assumes "⊢ F ⟶ G" and "⊢ G ⟶ F"
  shows "⊢ F = G"
  using assms by force

lemma int_iffD1: assumes h: "⊢ F = G" shows "⊢ F ⟶ G"
  using h by auto

lemma int_iffD2: assumes h: "⊢ F = G" shows "⊢ G ⟶ F"
  using h by auto

lemma lift_imp_trans: 
  assumes "⊢ A ⟶ B" and "⊢ B ⟶ C"
  shows "⊢ A ⟶ C"
  using assms by force

lemma lift_imp_neg: assumes "⊢ A ⟶ B" shows "⊢ ¬B ⟶ ¬A"
  using assms by auto

lemma lift_and_com:  "⊢ (A ∧ B) = (B ∧ A)"
  by auto

end