author | wenzelm |
Fri, 09 Nov 2001 00:09:47 +0100 | |
changeset 12114 | a8e860c86252 |
parent 9517 | f58863b1406a |
child 12338 | de0f4a63baa5 |
permissions | -rw-r--r-- |
3807 | 1 |
(* |
2 |
File: TLA/Intensional.thy |
|
3 |
Author: Stephan Merz |
|
6255 | 4 |
Copyright: 1998 University of Munich |
3807 | 5 |
|
6 |
Theory Name: Intensional |
|
7 |
Logic Image: HOL |
|
8 |
||
9 |
Define a framework for "intensional" (possible-world based) logics |
|
10 |
on top of HOL, with lifting of constants and functions. |
|
11 |
*) |
|
12 |
||
6255 | 13 |
Intensional = Main + |
3807 | 14 |
|
6255 | 15 |
axclass |
16 |
world < term |
|
17 |
||
18 |
(** abstract syntax **) |
|
3807 | 19 |
|
20 |
types |
|
6255 | 21 |
('w,'a) expr = 'w => 'a (* intention: 'w::world, 'a::term *) |
22 |
'w form = ('w, bool) expr |
|
3807 | 23 |
|
24 |
consts |
|
6255 | 25 |
Valid :: ('w::world) form => bool |
26 |
const :: 'a => ('w::world, 'a) expr |
|
27 |
lift :: ['a => 'b, ('w::world, 'a) expr] => ('w,'b) expr |
|
28 |
lift2 :: ['a => 'b => 'c, ('w::world,'a) expr, ('w,'b) expr] => ('w,'c) expr |
|
29 |
lift3 :: ['a => 'b => 'c => 'd, ('w::world,'a) expr, ('w,'b) expr, ('w,'c) expr] => ('w,'d) expr |
|
3807 | 30 |
|
6255 | 31 |
(* "Rigid" quantification (logic level) *) |
32 |
RAll :: "('a => ('w::world) form) => 'w form" (binder "Rall " 10) |
|
33 |
REx :: "('a => ('w::world) form) => 'w form" (binder "Rex " 10) |
|
34 |
REx1 :: "('a => ('w::world) form) => 'w form" (binder "Rex! " 10) |
|
3807 | 35 |
|
6255 | 36 |
(** concrete syntax **) |
3807 | 37 |
|
6255 | 38 |
nonterminals |
39 |
lift |
|
40 |
liftargs |
|
3807 | 41 |
|
42 |
syntax |
|
6255 | 43 |
"" :: id => lift ("_") |
44 |
"" :: longid => lift ("_") |
|
45 |
"" :: var => lift ("_") |
|
46 |
"_applC" :: [lift, cargs] => lift ("(1_/ _)" [1000, 1000] 999) |
|
47 |
"" :: lift => lift ("'(_')") |
|
48 |
"_lambda" :: [idts, 'a] => lift ("(3%_./ _)" [0, 3] 3) |
|
49 |
"_constrain" :: [lift, type] => lift ("(_::_)" [4, 0] 3) |
|
50 |
"" :: lift => liftargs ("_") |
|
51 |
"_liftargs" :: [lift, liftargs] => liftargs ("_,/ _") |
|
52 |
"_Valid" :: lift => bool ("(|- _)" 5) |
|
53 |
"_holdsAt" :: ['a, lift] => bool ("(_ |= _)" [100,10] 10) |
|
54 |
||
55 |
(* Syntax for lifted expressions outside the scope of |- or |= *) |
|
56 |
"LIFT" :: lift => 'a ("LIFT _") |
|
57 |
||
58 |
(* generic syntax for lifted constants and functions *) |
|
59 |
"_const" :: 'a => lift ("(#_)" [1000] 999) |
|
60 |
"_lift" :: ['a, lift] => lift ("(_<_>)" [1000] 999) |
|
61 |
"_lift2" :: ['a, lift, lift] => lift ("(_<_,/ _>)" [1000] 999) |
|
62 |
"_lift3" :: ['a, lift, lift, lift] => lift ("(_<_,/ _,/ _>)" [1000] 999) |
|
63 |
||
64 |
(* concrete syntax for common infix functions: reuse same symbol *) |
|
65 |
"_liftEqu" :: [lift, lift] => lift ("(_ =/ _)" [50,51] 50) |
|
66 |
"_liftNeq" :: [lift, lift] => lift ("(_ ~=/ _)" [50,51] 50) |
|
67 |
"_liftNot" :: lift => lift ("(~ _)" [40] 40) |
|
68 |
"_liftAnd" :: [lift, lift] => lift ("(_ &/ _)" [36,35] 35) |
|
69 |
"_liftOr" :: [lift, lift] => lift ("(_ |/ _)" [31,30] 30) |
|
70 |
"_liftImp" :: [lift, lift] => lift ("(_ -->/ _)" [26,25] 25) |
|
71 |
"_liftIf" :: [lift, lift, lift] => lift ("(if (_)/ then (_)/ else (_))" 10) |
|
72 |
"_liftPlus" :: [lift, lift] => lift ("(_ +/ _)" [66,65] 65) |
|
73 |
"_liftMinus" :: [lift, lift] => lift ("(_ -/ _)" [66,65] 65) |
|
74 |
"_liftTimes" :: [lift, lift] => lift ("(_ */ _)" [71,70] 70) |
|
75 |
"_liftDiv" :: [lift, lift] => lift ("(_ div _)" [71,70] 70) |
|
76 |
"_liftMod" :: [lift, lift] => lift ("(_ mod _)" [71,70] 70) |
|
77 |
"_liftLess" :: [lift, lift] => lift ("(_/ < _)" [50, 51] 50) |
|
78 |
"_liftLeq" :: [lift, lift] => lift ("(_/ <= _)" [50, 51] 50) |
|
79 |
"_liftMem" :: [lift, lift] => lift ("(_/ : _)" [50, 51] 50) |
|
80 |
"_liftNotMem" :: [lift, lift] => lift ("(_/ ~: _)" [50, 51] 50) |
|
81 |
"_liftFinset" :: liftargs => lift ("{(_)}") |
|
82 |
(** TODO: syntax for lifted collection / comprehension **) |
|
83 |
"_liftPair" :: [lift,liftargs] => lift ("(1'(_,/ _'))") |
|
84 |
(* infix syntax for list operations *) |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7224
diff
changeset
|
85 |
"_liftCons" :: [lift, lift] => lift ("(_ #/ _)" [65,66] 65) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7224
diff
changeset
|
86 |
"_liftApp" :: [lift, lift] => lift ("(_ @/ _)" [65,66] 65) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7224
diff
changeset
|
87 |
"_liftList" :: liftargs => lift ("[(_)]") |
6255 | 88 |
|
89 |
(* Rigid quantification (syntax level) *) |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7224
diff
changeset
|
90 |
"_ARAll" :: [idts, lift] => lift ("(3! _./ _)" [0, 10] 10) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7224
diff
changeset
|
91 |
"_AREx" :: [idts, lift] => lift ("(3? _./ _)" [0, 10] 10) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7224
diff
changeset
|
92 |
"_AREx1" :: [idts, lift] => lift ("(3?! _./ _)" [0, 10] 10) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7224
diff
changeset
|
93 |
"_RAll" :: [idts, lift] => lift ("(3ALL _./ _)" [0, 10] 10) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7224
diff
changeset
|
94 |
"_REx" :: [idts, lift] => lift ("(3EX _./ _)" [0, 10] 10) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7224
diff
changeset
|
95 |
"_REx1" :: [idts, lift] => lift ("(3EX! _./ _)" [0, 10] 10) |
3807 | 96 |
|
97 |
translations |
|
6255 | 98 |
"_const" == "const" |
99 |
"_lift" == "lift" |
|
100 |
"_lift2" == "lift2" |
|
101 |
"_lift3" == "lift3" |
|
102 |
"_Valid" == "Valid" |
|
103 |
"_RAll x A" == "Rall x. A" |
|
104 |
"_REx x A" == "Rex x. A" |
|
105 |
"_REx1 x A" == "Rex! x. A" |
|
106 |
"_ARAll" => "_RAll" |
|
107 |
"_AREx" => "_REx" |
|
108 |
"_AREx1" => "_REx1" |
|
3807 | 109 |
|
6255 | 110 |
"w |= A" => "A w" |
111 |
"LIFT A" => "A::_=>_" |
|
3807 | 112 |
|
6255 | 113 |
"_liftEqu" == "_lift2 (op =)" |
114 |
"_liftNeq u v" == "_liftNot (_liftEqu u v)" |
|
115 |
"_liftNot" == "_lift Not" |
|
116 |
"_liftAnd" == "_lift2 (op &)" |
|
117 |
"_liftOr" == "_lift2 (op | )" |
|
118 |
"_liftImp" == "_lift2 (op -->)" |
|
119 |
"_liftIf" == "_lift3 If" |
|
120 |
"_liftPlus" == "_lift2 (op +)" |
|
121 |
"_liftMinus" == "_lift2 (op -)" |
|
122 |
"_liftTimes" == "_lift2 (op *)" |
|
123 |
"_liftDiv" == "_lift2 (op div)" |
|
124 |
"_liftMod" == "_lift2 (op mod)" |
|
125 |
"_liftLess" == "_lift2 (op <)" |
|
126 |
"_liftLeq" == "_lift2 (op <=)" |
|
127 |
"_liftMem" == "_lift2 (op :)" |
|
128 |
"_liftNotMem x xs" == "_liftNot (_liftMem x xs)" |
|
129 |
"_liftFinset (_liftargs x xs)" == "_lift2 insert x (_liftFinset xs)" |
|
130 |
"_liftFinset x" == "_lift2 insert x (_const {})" |
|
131 |
"_liftPair x (_liftargs y z)" == "_liftPair x (_liftPair y z)" |
|
132 |
"_liftPair" == "_lift2 Pair" |
|
7224 | 133 |
"_liftCons" == "lift2 Cons" |
6255 | 134 |
"_liftApp" == "lift2 (op @)" |
135 |
"_liftList (_liftargs x xs)" == "_liftCons x (_liftList xs)" |
|
136 |
"_liftList x" == "_liftCons x (_const [])" |
|
3807 | 137 |
|
6255 | 138 |
|
3807 | 139 |
|
6255 | 140 |
"w |= ~A" <= "_liftNot A w" |
141 |
"w |= A & B" <= "_liftAnd A B w" |
|
142 |
"w |= A | B" <= "_liftOr A B w" |
|
143 |
"w |= A --> B" <= "_liftImp A B w" |
|
144 |
"w |= u = v" <= "_liftEqu u v w" |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7224
diff
changeset
|
145 |
"w |= ALL x. A" <= "_RAll x A w" |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7224
diff
changeset
|
146 |
"w |= EX x. A" <= "_REx x A w" |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7224
diff
changeset
|
147 |
"w |= EX! x. A" <= "_REx1 x A w" |
3807 | 148 |
|
12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
9517
diff
changeset
|
149 |
syntax (xsymbols) |
6255 | 150 |
"_Valid" :: lift => bool ("(\\<turnstile> _)" 5) |
151 |
"_holdsAt" :: ['a, lift] => bool ("(_ \\<Turnstile> _)" [100,10] 10) |
|
152 |
"_liftNeq" :: [lift, lift] => lift (infixl "\\<noteq>" 50) |
|
153 |
"_liftNot" :: lift => lift ("\\<not> _" [40] 40) |
|
154 |
"_liftAnd" :: [lift, lift] => lift (infixr "\\<and>" 35) |
|
155 |
"_liftOr" :: [lift, lift] => lift (infixr "\\<or>" 30) |
|
12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
9517
diff
changeset
|
156 |
"_liftImp" :: [lift, lift] => lift (infixr "\\<longrightarrow>" 25) |
6255 | 157 |
"_RAll" :: [idts, lift] => lift ("(3\\<forall>_./ _)" [0, 10] 10) |
158 |
"_REx" :: [idts, lift] => lift ("(3\\<exists>_./ _)" [0, 10] 10) |
|
159 |
"_REx1" :: [idts, lift] => lift ("(3\\<exists>!_./ _)" [0, 10] 10) |
|
160 |
"_liftLeq" :: [lift, lift] => lift ("(_/ \\<le> _)" [50, 51] 50) |
|
161 |
"_liftMem" :: [lift, lift] => lift ("(_/ \\<in> _)" [50, 51] 50) |
|
162 |
"_liftNotMem" :: [lift, lift] => lift ("(_/ \\<notin> _)" [50, 51] 50) |
|
3808 | 163 |
|
6340 | 164 |
syntax (HTML output) |
165 |
"_liftNot" :: lift => lift ("\\<not> _" [40] 40) |
|
166 |
||
3807 | 167 |
rules |
6255 | 168 |
Valid_def "|- A == ALL w. w |= A" |
3807 | 169 |
|
6255 | 170 |
unl_con "LIFT #c w == c" |
171 |
unl_lift "LIFT f<x> w == f (x w)" |
|
172 |
unl_lift2 "LIFT f<x, y> w == f (x w) (y w)" |
|
173 |
unl_lift3 "LIFT f<x, y, z> w == f (x w) (y w) (z w)" |
|
3807 | 174 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7224
diff
changeset
|
175 |
unl_Rall "w |= ALL x. A x == ALL x. (w |= A x)" |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7224
diff
changeset
|
176 |
unl_Rex "w |= EX x. A x == EX x. (w |= A x)" |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7224
diff
changeset
|
177 |
unl_Rex1 "w |= EX! x. A x == EX! x. (w |= A x)" |
6255 | 178 |
end |