diff r f6335d319e9f r db63752140c7 src/HOL/TLA/Intensional.thy
 a/src/HOL/TLA/Intensional.thy Mon Feb 08 13:02:42 1999 +0100
+++ b/src/HOL/TLA/Intensional.thy Mon Feb 08 13:02:56 1999 +0100
@@ 1,7 +1,7 @@
(*
File: TLA/Intensional.thy
Author: Stephan Merz
 Copyright: 1997 University of Munich
+ Copyright: 1998 University of Munich
Theory Name: Intensional
Logic Image: HOL
@@ 10,95 +10,168 @@
on top of HOL, with lifting of constants and functions.
*)
Intensional = Prod +
+Intensional = Main +
classes
 world < logic (* Type class of "possible worlds". Concrete types
 will be provided by children theories. *)
+axclass
+ world < term
+
+(** abstract syntax **)
types
 ('a,'w) term = "'w => 'a" (* Intention: 'w::world *)
 'w form = "'w => bool"
+ ('w,'a) expr = 'w => 'a (* intention: 'w::world, 'a::term *)
+ 'w form = ('w, bool) expr
consts
 TrueInt :: "('w::world form) => prop" ("(_)" 5)

 (* Holds at *)
 holdsAt :: "['w::world, 'w form] => bool" ("(_ = _)" [100,9] 8)

 (* Lifting base functions to "intensional" level *)
 con :: "'a => ('w::world => 'a)" ("(#_)" [100] 99)
 lift :: "['a => 'b, 'w::world => 'a] => ('w => 'b)" ("(_[_])")
 lift2 :: "['a => ('b => 'c), 'w::world => 'a, 'w => 'b] => ('w => 'c)" ("(_[_,/ _])")
 lift3 :: "['a => 'b => 'c => 'd, 'w::world => 'a, 'w => 'b, 'w => 'c] => ('w => 'd)" ("(_[_,/ _,/ _])")
+ 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
 (* Lifted infix functions *)
 IntEqu :: "['w::world => 'a, 'w => 'a] => 'w form" ("(_ .=/ _)" [50,51] 50)
 IntNeq :: "['w::world => 'a, 'w => 'a] => 'w form" ("(_ .~=/ _)" [50,51] 50)
 NotInt :: "('w::world) form => 'w form" ("(.~ _)" [40] 40)
 AndInt :: "[('w::world) form, 'w form] => 'w form" ("(_ .&/ _)" [36,35] 35)
 OrInt :: "[('w::world) form, 'w form] => 'w form" ("(_ ./ _)" [31,30] 30)
 ImpInt :: "[('w::world) form, 'w form] => 'w form" ("(_ .>/ _)" [26,25] 25)
 IfInt :: "[('w::world) form, ('a,'w) term, ('a,'w) term] => ('a,'w) term" ("(.if (_)/ .then (_)/ .else (_))" 10)
 PlusInt :: "[('w::world) => ('a::plus), 'w => 'a] => ('w => 'a)" ("(_ .+/ _)" [66,65] 65)
 MinusInt :: "[('w::world) => ('a::minus), 'w => 'a] => ('w => 'a)" ("(_ ./ _)" [66,65] 65)
 TimesInt :: "[('w::world) => ('a::times), 'w => 'a] => ('w => 'a)" ("(_ .*/ _)" [71,70] 70)
+ (* "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)
 LessInt :: "['w::world => 'a::ord, 'w => 'a] => 'w form" ("(_/ .< _)" [50, 51] 50)
 LeqInt :: "['w::world => 'a::ord, 'w => 'a] => 'w form" ("(_/ .<= _)" [50, 51] 50)
+(** concrete syntax **)
 (* lifted set membership *)
 memInt :: "[('a,'w::world) term, ('a set,'w) term] => 'w form" ("(_/ .: _)" [50, 51] 50)

 (* "Rigid" quantification *)
 RAll :: "('a => 'w::world form) => 'w form" (binder "RALL " 10)
 REx :: "('a => 'w::world form) => 'w form" (binder "REX " 10)
+nonterminals
+ lift
+ liftargs
syntax
 "@tupleInt" :: "args => ('a * 'b, 'w) term" ("(1{[_]})")
+ "" :: 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)
+ "_ARAll" :: [idts, lift] => lift ("(3ALL _./ _)" [0, 10] 10)
+ "_AREx" :: [idts, lift] => lift ("(3EX _./ _)" [0, 10] 10)
+ "_AREx1" :: [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"
 "{[x,y,z]}" == "{[x, {[y,z]} ]}"
 "{[x,y]}" == "Pair [x, y]"
 "{[x]}" => "x"
+ "w = A" => "A w"
+ "LIFT A" => "A::_=>_"
 "u .= v" == "op =[u,v]"
 "u .~= v" == ".~(u .= v)"
 ".~ A" == "Not[A]"
 "A .& B" == "op &[A,B]"
 "A . B" == "op [A,B]"
 "A .> B" == "op >[A,B]"
 ".if A .then u .else v" == "If[A,u,v]"
 "u .+ v" == "op +[u,v]"
 "u . v" == "op [u,v]"
 "u .* v" == "op *[u,v]"
+ "_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 (op #)"
+ "_liftApp" == "lift2 (op @)"
+ "_liftList (_liftargs x xs)" == "_liftCons x (_liftList xs)"
+ "_liftList x" == "_liftCons x (_const [])"
 "a .< b" == "op < [a,b]"
 "a .<= b" == "op <= [a,b]"
 "a .: A" == "op :[a,A]"
+
 "holdsAt w (lift f x)" == "lift f x w"
 "holdsAt w (lift2 f x y)" == "lift2 f x y w"
 "holdsAt w (lift3 f x y z)" == "lift3 f x y z w"

 "w = A" => "A(w)"
+ "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 (symbols)
 holdsAt :: "['w::world, 'w form] => bool" ("(_ \\ _)" [100,9] 8)

+ "_Valid" :: lift => bool ("(\\ _)" 5)
+ "_holdsAt" :: ['a, lift] => bool ("(_ \\ _)" [100,10] 10)
+ "_liftNeq" :: [lift, lift] => lift (infixl "\\" 50)
+ "_liftNot" :: lift => lift ("\\ _" [40] 40)
+ "_liftAnd" :: [lift, lift] => lift (infixr "\\" 35)
+ "_liftOr" :: [lift, lift] => lift (infixr "\\" 30)
+ "_liftImp" :: [lift, lift] => lift (infixr "\\\\" 25)
+ "_RAll" :: [idts, lift] => lift ("(3\\_./ _)" [0, 10] 10)
+ "_REx" :: [idts, lift] => lift ("(3\\_./ _)" [0, 10] 10)
+ "_REx1" :: [idts, lift] => lift ("(3\\!_./ _)" [0, 10] 10)
+ "_liftLeq" :: [lift, lift] => lift ("(_/ \\ _)" [50, 51] 50)
+ "_liftMem" :: [lift, lift] => lift ("(_/ \\ _)" [50, 51] 50)
+ "_liftNotMem" :: [lift, lift] => lift ("(_/ \\ _)" [50, 51] 50)
rules
 inteq_reflection "(x .= y) ==> (x == y)"
+ Valid_def " A == ALL w. w = A"
 int_valid "TrueInt(A) == (!! w. w = A)"
+ unl_con "LIFT #c w == c"
+ unl_lift "LIFT f w == f (x w)"
+ unl_lift2 "LIFT f w == f (x w) (y w)"
+ unl_lift3 "LIFT f w == f (x w) (y w) (z w)"
 unl_con "(#c) w == c" (* constants *)
 unl_lift "(f[x]) w == f(x w)"
 unl_lift2 "(f[x,y]) w == f (x w) (y w)"
 unl_lift3 "(f[x, y, z]) w == f (x w) (y w) (z w)"
+ unl_Rall "w = ! x. A x == ! x. (w = A x)"
+ unl_Rex "w = ? x. A x == ? x. (w = A x)"
+ unl_Rex1 "w = ?! x. A x == ?! x. (w = A x)"
+end
 unl_Rall "(RALL x. A(x)) w == ALL x. (w = A(x))"
 unl_Rex "(REX x. A(x)) w == EX x. (w = A(x))"

end
+ML