Quelle  Intensional.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 ‹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
  (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 \<turnstile> or \<Turnstile>.*)
  "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