3807
|
1 |
(*
|
|
2 |
File: TLA/Intensional.thy
|
|
3 |
Author: Stephan Merz
|
|
4 |
Copyright: 1997 University of Munich
|
|
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 |
|
|
13 |
Intensional = Prod +
|
|
14 |
|
|
15 |
classes
|
|
16 |
world < logic (* Type class of "possible worlds". Concrete types
|
|
17 |
will be provided by children theories. *)
|
|
18 |
|
|
19 |
types
|
|
20 |
('a,'w) term = "'w => 'a" (* Intention: 'w::world *)
|
|
21 |
'w form = "'w => bool"
|
|
22 |
|
|
23 |
consts
|
|
24 |
TrueInt :: "('w::world form) => prop" ("(_)" 5)
|
|
25 |
|
|
26 |
(* Holds at *)
|
|
27 |
holdsAt :: "['w::world, 'w form] => bool" ("(_ |= _)" [100,9] 8)
|
|
28 |
|
|
29 |
(* Lifting base functions to "intensional" level *)
|
|
30 |
con :: "'a => ('w::world => 'a)" ("(#_)" [100] 99)
|
|
31 |
lift :: "['a => 'b, 'w::world => 'a] => ('w => 'b)" ("(_[_])")
|
|
32 |
lift2 :: "['a => ('b => 'c), 'w::world => 'a, 'w => 'b] => ('w => 'c)" ("(_[_,/ _])")
|
|
33 |
lift3 :: "['a => 'b => 'c => 'd, 'w::world => 'a, 'w => 'b, 'w => 'c] => ('w => 'd)" ("(_[_,/ _,/ _])")
|
|
34 |
|
|
35 |
(* Lifted infix functions *)
|
|
36 |
IntEqu :: "['w::world => 'a, 'w => 'a] => 'w form" ("(_ .=/ _)" [50,51] 50)
|
|
37 |
IntNeq :: "['w::world => 'a, 'w => 'a] => 'w form" ("(_ .~=/ _)" [50,51] 50)
|
|
38 |
NotInt :: "('w::world) form => 'w form" ("(.~ _)" [40] 40)
|
|
39 |
AndInt :: "[('w::world) form, 'w form] => 'w form" ("(_ .&/ _)" [36,35] 35)
|
|
40 |
OrInt :: "[('w::world) form, 'w form] => 'w form" ("(_ .|/ _)" [31,30] 30)
|
|
41 |
ImpInt :: "[('w::world) form, 'w form] => 'w form" ("(_ .->/ _)" [26,25] 25)
|
|
42 |
IfInt :: "[('w::world) form, ('a,'w) term, ('a,'w) term] => ('a,'w) term" ("(.if (_)/ .then (_)/ .else (_))" 10)
|
|
43 |
PlusInt :: "[('w::world) => ('a::plus), 'w => 'a] => ('w => 'a)" ("(_ .+/ _)" [66,65] 65)
|
|
44 |
MinusInt :: "[('w::world) => ('a::minus), 'w => 'a] => ('w => 'a)" ("(_ .-/ _)" [66,65] 65)
|
|
45 |
TimesInt :: "[('w::world) => ('a::times), 'w => 'a] => ('w => 'a)" ("(_ .*/ _)" [71,70] 70)
|
|
46 |
|
|
47 |
LessInt :: "['w::world => 'a::ord, 'w => 'a] => 'w form" ("(_/ .< _)" [50, 51] 50)
|
|
48 |
LeqInt :: "['w::world => 'a::ord, 'w => 'a] => 'w form" ("(_/ .<= _)" [50, 51] 50)
|
|
49 |
|
|
50 |
(* lifted set membership *)
|
|
51 |
memInt :: "[('a,'w::world) term, ('a set,'w) term] => 'w form" ("(_/ .: _)" [50, 51] 50)
|
|
52 |
|
|
53 |
(* "Rigid" quantification *)
|
|
54 |
RAll :: "('a => 'w::world form) => 'w form" (binder "RALL " 10)
|
|
55 |
REx :: "('a => 'w::world form) => 'w form" (binder "REX " 10)
|
|
56 |
|
|
57 |
syntax
|
|
58 |
"@tupleInt" :: "args => ('a * 'b, 'w) term" ("(1{[_]})")
|
|
59 |
|
|
60 |
translations
|
|
61 |
|
|
62 |
"{[x,y,z]}" == "{[x, {[y,z]} ]}"
|
|
63 |
"{[x,y]}" == "Pair [x, y]"
|
|
64 |
"{[x]}" => "x"
|
|
65 |
|
|
66 |
"u .= v" == "op =[u,v]"
|
|
67 |
"u .~= v" == ".~(u .= v)"
|
|
68 |
".~ A" == "Not[A]"
|
|
69 |
"A .& B" == "op &[A,B]"
|
|
70 |
"A .| B" == "op |[A,B]"
|
|
71 |
"A .-> B" == "op -->[A,B]"
|
|
72 |
".if A .then u .else v" == "If[A,u,v]"
|
|
73 |
"u .+ v" == "op +[u,v]"
|
|
74 |
"u .- v" == "op -[u,v]"
|
|
75 |
"u .* v" == "op *[u,v]"
|
|
76 |
|
|
77 |
"a .< b" == "op < [a,b]"
|
|
78 |
"a .<= b" == "op <= [a,b]"
|
|
79 |
"a .: A" == "op :[a,A]"
|
|
80 |
|
|
81 |
"holdsAt w (lift f x)" == "lift f x w"
|
|
82 |
"holdsAt w (lift2 f x y)" == "lift2 f x y w"
|
|
83 |
"holdsAt w (lift3 f x y z)" == "lift3 f x y z w"
|
|
84 |
|
|
85 |
"w |= A" => "A(w)"
|
|
86 |
|
|
87 |
rules
|
|
88 |
inteq_reflection "(x .= y) ==> (x == y)"
|
|
89 |
|
|
90 |
int_valid "TrueInt(A) == (!! w. w |= A)"
|
|
91 |
|
|
92 |
unl_con "(#c) w == c" (* constants *)
|
|
93 |
unl_lift "(f[x]) w == f(x w)"
|
|
94 |
unl_lift2 "(f[x,y]) w == f (x w) (y w)"
|
|
95 |
unl_lift3 "(f[x, y, z]) w == f (x w) (y w) (z w)"
|
|
96 |
|
|
97 |
unl_Rall "(RALL x. A(x)) w == ALL x. (w |= A(x))"
|
|
98 |
unl_Rex "(REX x. A(x)) w == EX x. (w |= A(x))"
|
|
99 |
end
|
|
100 |
|
|
101 |
ML
|