Theory Intensional

(*  Title:      HOL/TLA/Intensional.thy
    Author:     Stephan Merz
    Copyright:  1998 University of Munich
*)

section ‹A framework for "intensional" (possible-world based) logics
  on top of HOL, with lifting of constants and functions›

theory Intensional
imports Main
begin

class world

(** abstract syntax **)

type_synonym ('w,'a) expr = "'w ⇒ 'a"   (* intention: 'w::world, 'a::type *)
type_synonym 'w form = "('w, bool) expr"

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)"

(* "Rigid" quantification (logic level) *)
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"


(** concrete syntax **)

nonterminal lift and liftargs

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)

  (* concrete syntax for common infix functions: reuse same symbol *)
  "_liftEqu"    :: "[lift, lift] ⇒ lift"                ("(_ =/ _)" [50,51] 50)
  "_liftNeq"    :: "[lift, lift] ⇒ lift"                ("(_ ≠/ _)" [50,51] 50)
  "_liftNot"    :: "lift ⇒ lift"                        ("(¬ _)" [40] 40)
  "_liftAnd"    :: "[lift, lift] ⇒ lift"                ("(_ ∧/ _)" [36,35] 35)
  "_liftOr"     :: "[lift, lift] ⇒ lift"                ("(_ ∨/ _)" [31,30] 30)
  "_liftImp"    :: "[lift, lift] ⇒ lift"                ("(_ ⟶/ _)" [26,25] 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) *)
  "_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"
  "_lift"         == "CONST lift"
  "_lift2"        == "CONST lift2"
  "_lift3"        == "CONST lift3"
  "_Valid"        == "CONST Valid"
  "_RAll x A"     == "Rall x. A"
  "_REx x  A"     == "Rex x. A"
  "_REx1 x  A"    == "Rex! x. A"

  "w ⊨ A"        => "A w"
  "LIFT A"        => "A::_⇒_"

  "_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)"
  "_liftFinset (_liftargs x xs)"  == "_lift2 (CONST insert) x (_liftFinset xs)"
  "_liftFinset x" == "_lift2 (CONST insert) x (_const {})"
  "_liftPair x (_liftargs y z)"       == "_liftPair x (_liftPair y z)"
  "_liftPair"     == "_lift2 (CONST Pair)"
  "_liftCons"     == "CONST lift2 (CONST Cons)"
  "_liftApp"      == "CONST 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"


subsection ‹Lemmas and tactics for "intensional" logics.›

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

lemma inteq_reflection: "⊢ x=y  ⟹  (x==y)"
  apply (unfold Valid_def unl_lift2)
  apply (rule eq_reflection)
  apply (rule ext)
  apply (erule spec)
  done

lemma intI [intro!]: "(⋀w. w ⊨ A) ⟹ ⊢ A"
  apply (unfold Valid_def)
  apply (rule allI)
  apply (erule meta_spec)
  done

lemma intD [dest]: "⊢ A ⟹ w ⊨ A"
  apply (unfold Valid_def)
  apply (erule spec)
  done

(** Lift usual HOL simplifications to "intensional" level. **)

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"
  "⊢ (¬Q ⟶ ¬P) = (P ⟶ Q)"
  "⊢ (P∨Q ⟶ R) = ((P⟶R)∧(Q⟶R))"
  apply (unfold Valid_def intensional_rews)
  apply blast+
  done

declare int_simps [THEN inteq_reflection, simp]

lemma TrueW [simp]: "⊢ #True"
  by (simp add: Valid_def unl_con)



(* ======== Functions to "unlift" intensional implications into HOL rules ====== *)

ML ‹
(* Basic unlifting introduces a parameter "w" and applies basic rewrites, e.g.
   ⊢ F = G    becomes   F w = G w
   ⊢ F ⟶ G  becomes   F w ⟶ G w
*)

fun int_unlift ctxt th =
  rewrite_rule ctxt @{thms intensional_rews} (th RS @{thm intD} handle THM _ => th);

(* Turn  ⊢ F = G  into meta-level rewrite rule  F == G *)
fun int_rewrite ctxt th =
  zero_var_indexes (rewrite_rule ctxt @{thms intensional_rews} (th RS @{thm inteq_reflection}))

(* flattening turns "⟶" into "⟹" and eliminates conjunctions in the
   antecedent. For example,

         P & Q ⟶ (R | S ⟶ T)    becomes   ⟦ P; Q; R | S ⟧ ⟹ T

   Flattening can be useful with "intensional" lemmas (after unlifting).
   Naive resolution with mp and conjI may run away because of higher-order
   unification, therefore the code is a little awkward.
*)
fun flatten t =
  let
    (* analogous to RS, but using matching instead of resolution *)
    fun matchres tha i thb =
      case Seq.chop 2 (Thm.biresolution NONE true [(false,tha)] i thb) of
          ([th],_) => th
        | ([],_)   => raise THM("matchres: no match", i, [tha,thb])
        |      _   => raise THM("matchres: multiple unifiers", i, [tha,thb])

    (* match tha with some premise of thb *)
    fun matchsome tha thb =
      let fun hmatch 0 = raise THM("matchsome: no match", 0, [tha,thb])
            | hmatch n = matchres tha n thb handle THM _ => hmatch (n-1)
      in hmatch (Thm.nprems_of thb) end

    fun hflatten t =
      case Thm.concl_of t of
        Const _ $ (Const (\<^const_name>‹HOL.implies›, _) $ _ $ _) => hflatten (t RS mp)
      | _ => (hflatten (matchsome conjI t)) handle THM _ => zero_var_indexes t
  in
    hflatten t
  end

fun int_use ctxt th =
    case Thm.concl_of th of
      Const _ $ (Const (\<^const_name>‹Valid›, _) $ _) =>
              (flatten (int_unlift ctxt th) handle THM _ => th)
    | _ => th
›

attribute_setup int_unlift =
  ‹Scan.succeed (Thm.rule_attribute [] (int_unlift o Context.proof_of))›
attribute_setup int_rewrite =
  ‹Scan.succeed (Thm.rule_attribute [] (int_rewrite o Context.proof_of))›
attribute_setup flatten =
  ‹Scan.succeed (Thm.rule_attribute [] (K flatten))›
attribute_setup int_use =
  ‹Scan.succeed (Thm.rule_attribute [] (int_use o Context.proof_of))›

lemma Not_Rall: "⊢ (¬(∀x. F x)) = (∃x. ¬F x)"
  by (simp add: Valid_def)

lemma Not_Rex: "⊢ (¬ (∃x. F x)) = (∀x. ¬ F x)"
  by (simp add: Valid_def)

end