Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: rdf.scala Sprache: Isabelle

Original von: Isabelle^©

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

section \<open>A framework for "intensional" (possible-world based) logics
  on top of HOL, with lifting of constants and functions\<close>

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 \<turnstile> 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 \<open>Lemmas and tactics for "intensional" logics.\<close>

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 \<open>
(* Basic unlifting introduces a parameter "w" and applies basic rewrites, e.g.
   \<turnstile> F = G    becomes   F w = G w
   \<turnstile> F \<longrightarrow> G  becomes   F w \<longrightarrow> G w
*)

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

(* Turn  \<turnstile> 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 "\<longrightarrow>" into "\<Longrightarrow>" and eliminates conjunctions in the
   antecedent. For example,

         P & Q \<longrightarrow> (R | S \<longrightarrow> T)    becomes   \<lbrakk> P; Q; R | S \<rbrakk> \<Longrightarrow> 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>\<open>HOL.implies\<close>, _) $ _ $ _) => 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>\<open>Valid\<close>, _) $ _) =>
              (flatten (int_unlift ctxt th) handle THM _ => th)
    | _ => th
\<close>

attribute_setup int_unlift =
  \<open>Scan.succeed (Thm.rule_attribute [] (int_unlift o Context.proof_of))\<close>
attribute_setup int_rewrite =
  \<open>Scan.succeed (Thm.rule_attribute [] (int_rewrite o Context.proof_of))\<close>
attribute_setup flatten =
  \<open>Scan.succeed (Thm.rule_attribute [] (K flatten))\<close>
attribute_setup int_use =
  \<open>Scan.succeed (Thm.rule_attribute [] (int_use o Context.proof_of))\<close>

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

¤ Dauer der Verarbeitung: 0.29 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.