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