Added store_thmss_atts to signature again.
(*
File: TLA/Intensional.thy
ID: $Id$
Author: Stephan Merz
Copyright: 1998 University of Munich
Theory Name: Intensional
Logic Image: HOL
Define a framework for "intensional" (possible-world based) logics
on top of HOL, with lifting of constants and functions.
*)
theory Intensional
imports Main
begin
axclass
world < type
(** abstract syntax **)
types
('w,'a) expr = "'w => 'a" (* intention: 'w::world, 'a::type *)
'w form = "('w, bool) expr"
consts
Valid :: "('w::world) form => bool"
const :: "'a => ('w::world, 'a) expr"
lift :: "['a => 'b, ('w::world, 'a) expr] => ('w,'b) expr"
lift2 :: "['a => 'b => 'c, ('w::world,'a) expr, ('w,'b) expr] => ('w,'c) expr"
lift3 :: "['a => 'b => 'c => 'd, ('w::world,'a) expr, ('w,'b) expr, ('w,'c) expr] => ('w,'d) expr"
(* "Rigid" quantification (logic level) *)
RAll :: "('a => ('w::world) form) => 'w form" (binder "Rall " 10)
REx :: "('a => ('w::world) form) => 'w form" (binder "Rex " 10)
REx1 :: "('a => ('w::world) form) => 'w form" (binder "Rex! " 10)
(** concrete syntax **)
nonterminals
lift
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) *)
"_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" ("(3ALL _./ _)" [0, 10] 10)
"_REx" :: "[idts, lift] => lift" ("(3EX _./ _)" [0, 10] 10)
"_REx1" :: "[idts, lift] => lift" ("(3EX! _./ _)" [0, 10] 10)
translations
"_const" == "const"
"_lift" == "lift"
"_lift2" == "lift2"
"_lift3" == "lift3"
"_Valid" == "Valid"
"_RAll x A" == "Rall x. A"
"_REx x A" == "Rex x. A"
"_REx1 x A" == "Rex! x. A"
"_ARAll" => "_RAll"
"_AREx" => "_REx"
"_AREx1" => "_REx1"
"w |= A" => "A w"
"LIFT A" => "A::_=>_"
"_liftEqu" == "_lift2 (op =)"
"_liftNeq u v" == "_liftNot (_liftEqu u v)"
"_liftNot" == "_lift Not"
"_liftAnd" == "_lift2 (op &)"
"_liftOr" == "_lift2 (op | )"
"_liftImp" == "_lift2 (op -->)"
"_liftIf" == "_lift3 If"
"_liftPlus" == "_lift2 (op +)"
"_liftMinus" == "_lift2 (op -)"
"_liftTimes" == "_lift2 (op *)"
"_liftDiv" == "_lift2 (op div)"
"_liftMod" == "_lift2 (op mod)"
"_liftLess" == "_lift2 (op <)"
"_liftLeq" == "_lift2 (op <=)"
"_liftMem" == "_lift2 (op :)"
"_liftNotMem x xs" == "_liftNot (_liftMem x xs)"
"_liftFinset (_liftargs x xs)" == "_lift2 insert x (_liftFinset xs)"
"_liftFinset x" == "_lift2 insert x (_const {})"
"_liftPair x (_liftargs y z)" == "_liftPair x (_liftPair y z)"
"_liftPair" == "_lift2 Pair"
"_liftCons" == "lift2 Cons"
"_liftApp" == "lift2 (op @)"
"_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 |= ALL x. A" <= "_RAll x A w"
"w |= EX x. A" <= "_REx x A w"
"w |= EX! x. A" <= "_REx1 x A w"
syntax (xsymbols)
"_Valid" :: "lift => bool" ("(\<turnstile> _)" 5)
"_holdsAt" :: "['a, lift] => bool" ("(_ \<Turnstile> _)" [100,10] 10)
"_liftNeq" :: "[lift, lift] => lift" (infixl "\<noteq>" 50)
"_liftNot" :: "lift => lift" ("\<not> _" [40] 40)
"_liftAnd" :: "[lift, lift] => lift" (infixr "\<and>" 35)
"_liftOr" :: "[lift, lift] => lift" (infixr "\<or>" 30)
"_liftImp" :: "[lift, lift] => lift" (infixr "\<longrightarrow>" 25)
"_RAll" :: "[idts, lift] => lift" ("(3\<forall>_./ _)" [0, 10] 10)
"_REx" :: "[idts, lift] => lift" ("(3\<exists>_./ _)" [0, 10] 10)
"_REx1" :: "[idts, lift] => lift" ("(3\<exists>!_./ _)" [0, 10] 10)
"_liftLeq" :: "[lift, lift] => lift" ("(_/ \<le> _)" [50, 51] 50)
"_liftMem" :: "[lift, lift] => lift" ("(_/ \<in> _)" [50, 51] 50)
"_liftNotMem" :: "[lift, lift] => lift" ("(_/ \<notin> _)" [50, 51] 50)
syntax (HTML output)
"_liftNeq" :: "[lift, lift] => lift" (infixl "\<noteq>" 50)
"_liftNot" :: "lift => lift" ("\<not> _" [40] 40)
"_liftAnd" :: "[lift, lift] => lift" (infixr "\<and>" 35)
"_liftOr" :: "[lift, lift] => lift" (infixr "\<or>" 30)
"_RAll" :: "[idts, lift] => lift" ("(3\<forall>_./ _)" [0, 10] 10)
"_REx" :: "[idts, lift] => lift" ("(3\<exists>_./ _)" [0, 10] 10)
"_REx1" :: "[idts, lift] => lift" ("(3\<exists>!_./ _)" [0, 10] 10)
"_liftLeq" :: "[lift, lift] => lift" ("(_/ \<le> _)" [50, 51] 50)
"_liftMem" :: "[lift, lift] => lift" ("(_/ \<in> _)" [50, 51] 50)
"_liftNotMem" :: "[lift, lift] => lift" ("(_/ \<notin> _)" [50, 51] 50)
axioms
Valid_def: "|- A == ALL w. w |= A"
unl_con: "LIFT #c w == c"
unl_lift: "LIFT f<x> w == f (x w)"
unl_lift2: "LIFT f<x, y> w == f (x w) (y w)"
unl_lift3: "LIFT f<x, y, z> w == f (x w) (y w) (z w)"
unl_Rall: "w |= ALL x. A x == ALL x. (w |= A x)"
unl_Rex: "w |= EX x. A x == EX x. (w |= A x)"
unl_Rex1: "w |= EX! x. A x == EX! x. (w |= A x)"
ML {* use_legacy_bindings (the_context ()) *}
end