clasohm@923
|
1 |
(* Title: HOL/HOL.thy
|
clasohm@923
|
2 |
ID: $Id$
|
clasohm@923
|
3 |
Author: Tobias Nipkow
|
clasohm@923
|
4 |
Copyright 1993 University of Cambridge
|
clasohm@923
|
5 |
|
wenzelm@2260
|
6 |
Higher-Order Logic.
|
clasohm@923
|
7 |
*)
|
clasohm@923
|
8 |
|
clasohm@923
|
9 |
HOL = CPure +
|
clasohm@923
|
10 |
|
wenzelm@2260
|
11 |
|
wenzelm@2260
|
12 |
(** Core syntax **)
|
wenzelm@2260
|
13 |
|
wenzelm@3947
|
14 |
global
|
wenzelm@3947
|
15 |
|
clasohm@923
|
16 |
classes
|
clasohm@923
|
17 |
term < logic
|
clasohm@923
|
18 |
|
clasohm@923
|
19 |
default
|
clasohm@923
|
20 |
term
|
clasohm@923
|
21 |
|
clasohm@923
|
22 |
types
|
clasohm@923
|
23 |
bool
|
clasohm@923
|
24 |
|
clasohm@923
|
25 |
arities
|
clasohm@923
|
26 |
fun :: (term, term) term
|
clasohm@923
|
27 |
bool :: term
|
clasohm@923
|
28 |
|
clasohm@923
|
29 |
|
clasohm@923
|
30 |
consts
|
clasohm@923
|
31 |
|
clasohm@923
|
32 |
(* Constants *)
|
clasohm@923
|
33 |
|
clasohm@1370
|
34 |
Trueprop :: bool => prop ("(_)" 5)
|
paulson@2720
|
35 |
Not :: bool => bool ("~ _" [40] 40)
|
clasohm@1370
|
36 |
True, False :: bool
|
clasohm@1370
|
37 |
If :: [bool, 'a, 'a] => 'a ("(if (_)/ then (_)/ else (_))" 10)
|
wenzelm@3947
|
38 |
arbitrary :: 'a
|
clasohm@923
|
39 |
|
clasohm@923
|
40 |
(* Binders *)
|
clasohm@923
|
41 |
|
clasohm@1370
|
42 |
Eps :: ('a => bool) => 'a
|
clasohm@1370
|
43 |
All :: ('a => bool) => bool (binder "! " 10)
|
clasohm@1370
|
44 |
Ex :: ('a => bool) => bool (binder "? " 10)
|
clasohm@1370
|
45 |
Ex1 :: ('a => bool) => bool (binder "?! " 10)
|
clasohm@1370
|
46 |
Let :: ['a, 'a => 'b] => 'b
|
clasohm@923
|
47 |
|
clasohm@923
|
48 |
(* Infixes *)
|
clasohm@923
|
49 |
|
clasohm@1370
|
50 |
o :: ['b => 'c, 'a => 'b, 'a] => 'c (infixl 55)
|
clasohm@1370
|
51 |
"=" :: ['a, 'a] => bool (infixl 50)
|
clasohm@1370
|
52 |
"&" :: [bool, bool] => bool (infixr 35)
|
clasohm@1370
|
53 |
"|" :: [bool, bool] => bool (infixr 30)
|
clasohm@1370
|
54 |
"-->" :: [bool, bool] => bool (infixr 25)
|
clasohm@923
|
55 |
|
clasohm@923
|
56 |
|
wenzelm@2260
|
57 |
(* Overloaded Constants *)
|
wenzelm@2260
|
58 |
|
wenzelm@2260
|
59 |
axclass
|
wenzelm@2260
|
60 |
plus < term
|
wenzelm@2260
|
61 |
|
wenzelm@2260
|
62 |
axclass
|
wenzelm@2260
|
63 |
minus < term
|
wenzelm@2260
|
64 |
|
wenzelm@2260
|
65 |
axclass
|
wenzelm@2260
|
66 |
times < term
|
wenzelm@2260
|
67 |
|
paulson@3370
|
68 |
axclass
|
paulson@3370
|
69 |
power < term
|
paulson@3370
|
70 |
|
wenzelm@2260
|
71 |
consts
|
paulson@3370
|
72 |
"+" :: ['a::plus, 'a] => 'a (infixl 65)
|
clasohm@1370
|
73 |
"-" :: ['a::minus, 'a] => 'a (infixl 65)
|
clasohm@1370
|
74 |
"*" :: ['a::times, 'a] => 'a (infixl 70)
|
paulson@3370
|
75 |
(*See Nat.thy for "^"*)
|
wenzelm@2260
|
76 |
|
wenzelm@3820
|
77 |
|
wenzelm@2260
|
78 |
(** Additional concrete syntax **)
|
wenzelm@2260
|
79 |
|
clasohm@923
|
80 |
types
|
clasohm@923
|
81 |
letbinds letbind
|
clasohm@923
|
82 |
case_syn cases_syn
|
clasohm@923
|
83 |
|
clasohm@923
|
84 |
syntax
|
clasohm@923
|
85 |
|
clasohm@1370
|
86 |
"~=" :: ['a, 'a] => bool (infixl 50)
|
clasohm@923
|
87 |
|
wenzelm@2368
|
88 |
"@Eps" :: [pttrn, bool] => 'a ("(3@ _./ _)" [0, 10] 10)
|
nipkow@1068
|
89 |
|
clasohm@923
|
90 |
(* Alternative Quantifiers *)
|
clasohm@923
|
91 |
|
wenzelm@2368
|
92 |
"*All" :: [idts, bool] => bool ("(3ALL _./ _)" [0, 10] 10)
|
wenzelm@2368
|
93 |
"*Ex" :: [idts, bool] => bool ("(3EX _./ _)" [0, 10] 10)
|
wenzelm@2368
|
94 |
"*Ex1" :: [idts, bool] => bool ("(3EX! _./ _)" [0, 10] 10)
|
clasohm@923
|
95 |
|
clasohm@923
|
96 |
(* Let expressions *)
|
clasohm@923
|
97 |
|
clasohm@1370
|
98 |
"_bind" :: [pttrn, 'a] => letbind ("(2_ =/ _)" 10)
|
clasohm@1370
|
99 |
"" :: letbind => letbinds ("_")
|
clasohm@1370
|
100 |
"_binds" :: [letbind, letbinds] => letbinds ("_;/ _")
|
clasohm@1370
|
101 |
"_Let" :: [letbinds, 'a] => 'a ("(let (_)/ in (_))" 10)
|
clasohm@923
|
102 |
|
clasohm@923
|
103 |
(* Case expressions *)
|
clasohm@923
|
104 |
|
clasohm@1370
|
105 |
"@case" :: ['a, cases_syn] => 'b ("(case _ of/ _)" 10)
|
clasohm@1370
|
106 |
"@case1" :: ['a, 'b] => case_syn ("(2_ =>/ _)" 10)
|
clasohm@1370
|
107 |
"" :: case_syn => cases_syn ("_")
|
clasohm@1370
|
108 |
"@case2" :: [case_syn, cases_syn] => cases_syn ("_/ | _")
|
clasohm@923
|
109 |
|
clasohm@923
|
110 |
translations
|
clasohm@923
|
111 |
"x ~= y" == "~ (x = y)"
|
wenzelm@3842
|
112 |
"@ x. b" == "Eps (%x. b)"
|
clasohm@923
|
113 |
"ALL xs. P" => "! xs. P"
|
clasohm@923
|
114 |
"EX xs. P" => "? xs. P"
|
clasohm@923
|
115 |
"EX! xs. P" => "?! xs. P"
|
clasohm@923
|
116 |
"_Let (_binds b bs) e" == "_Let b (_Let bs e)"
|
nipkow@1114
|
117 |
"let x = a in e" == "Let a (%x. e)"
|
clasohm@923
|
118 |
|
wenzelm@3820
|
119 |
syntax ("" output)
|
wenzelm@3820
|
120 |
"op =" :: ['a, 'a] => bool ("(_ =/ _)" [51, 51] 50)
|
wenzelm@3820
|
121 |
"op ~=" :: ['a, 'a] => bool ("(_ ~=/ _)" [51, 51] 50)
|
wenzelm@2260
|
122 |
|
wenzelm@2260
|
123 |
syntax (symbols)
|
wenzelm@2762
|
124 |
Not :: bool => bool ("\\<not> _" [40] 40)
|
wenzelm@2260
|
125 |
"op &" :: [bool, bool] => bool (infixr "\\<and>" 35)
|
wenzelm@2260
|
126 |
"op |" :: [bool, bool] => bool (infixr "\\<or>" 30)
|
wenzelm@2260
|
127 |
"op -->" :: [bool, bool] => bool (infixr "\\<midarrow>\\<rightarrow>" 25)
|
wenzelm@2260
|
128 |
"op o" :: ['b => 'c, 'a => 'b, 'a] => 'c (infixl "\\<circ>" 55)
|
wenzelm@2260
|
129 |
"op ~=" :: ['a, 'a] => bool (infixl "\\<noteq>" 50)
|
wenzelm@2368
|
130 |
"@Eps" :: [pttrn, bool] => 'a ("(3\\<epsilon>_./ _)" [0, 10] 10)
|
wenzelm@2368
|
131 |
"! " :: [idts, bool] => bool ("(3\\<forall>_./ _)" [0, 10] 10)
|
wenzelm@2368
|
132 |
"? " :: [idts, bool] => bool ("(3\\<exists>_./ _)" [0, 10] 10)
|
wenzelm@2368
|
133 |
"?! " :: [idts, bool] => bool ("(3\\<exists>!_./ _)" [0, 10] 10)
|
wenzelm@2552
|
134 |
"@case1" :: ['a, 'b] => case_syn ("(2_ \\<Rightarrow>/ _)" 10)
|
wenzelm@3068
|
135 |
(*"@case2" :: [case_syn, cases_syn] => cases_syn ("_/ \\<orelse> _")*)
|
wenzelm@2372
|
136 |
|
wenzelm@3820
|
137 |
syntax (symbols output)
|
wenzelm@3820
|
138 |
"op ~=" :: ['a, 'a] => bool ("(_ \\<noteq>/ _)" [51, 51] 50)
|
wenzelm@3820
|
139 |
"*All" :: [idts, bool] => bool ("(3\\<forall>_./ _)" [0, 10] 10)
|
wenzelm@3820
|
140 |
"*Ex" :: [idts, bool] => bool ("(3\\<exists>_./ _)" [0, 10] 10)
|
wenzelm@3820
|
141 |
"*Ex1" :: [idts, bool] => bool ("(3\\<exists>!_./ _)" [0, 10] 10)
|
wenzelm@3820
|
142 |
|
wenzelm@2260
|
143 |
|
wenzelm@2260
|
144 |
|
wenzelm@2260
|
145 |
(** Rules and definitions **)
|
wenzelm@2260
|
146 |
|
wenzelm@3947
|
147 |
local
|
wenzelm@3947
|
148 |
|
clasohm@923
|
149 |
rules
|
clasohm@923
|
150 |
|
clasohm@923
|
151 |
eq_reflection "(x=y) ==> (x==y)"
|
clasohm@923
|
152 |
|
clasohm@923
|
153 |
(* Basic Rules *)
|
clasohm@923
|
154 |
|
clasohm@923
|
155 |
refl "t = (t::'a)"
|
clasohm@923
|
156 |
subst "[| s = t; P(s) |] ==> P(t::'a)"
|
wenzelm@3842
|
157 |
ext "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
|
wenzelm@3842
|
158 |
selectI "P (x::'a) ==> P (@x. P x)"
|
clasohm@923
|
159 |
|
clasohm@923
|
160 |
impI "(P ==> Q) ==> P-->Q"
|
clasohm@923
|
161 |
mp "[| P-->Q; P |] ==> Q"
|
clasohm@923
|
162 |
|
clasohm@923
|
163 |
defs
|
clasohm@923
|
164 |
|
wenzelm@3842
|
165 |
True_def "True == ((%x::bool. x) = (%x. x))"
|
wenzelm@3842
|
166 |
All_def "All(P) == (P = (%x. True))"
|
wenzelm@3842
|
167 |
Ex_def "Ex(P) == P(@x. P(x))"
|
wenzelm@3842
|
168 |
False_def "False == (!P. P)"
|
clasohm@923
|
169 |
not_def "~ P == P-->False"
|
clasohm@923
|
170 |
and_def "P & Q == !R. (P-->Q-->R) --> R"
|
clasohm@923
|
171 |
or_def "P | Q == !R. (P-->R) --> (Q-->R) --> R"
|
clasohm@923
|
172 |
Ex1_def "Ex1(P) == ? x. P(x) & (! y. P(y) --> y=x)"
|
clasohm@923
|
173 |
|
clasohm@923
|
174 |
rules
|
clasohm@923
|
175 |
(* Axioms *)
|
clasohm@923
|
176 |
|
clasohm@923
|
177 |
iff "(P-->Q) --> (Q-->P) --> (P=Q)"
|
clasohm@923
|
178 |
True_or_False "(P=True) | (P=False)"
|
clasohm@923
|
179 |
|
clasohm@923
|
180 |
defs
|
clasohm@923
|
181 |
(* Misc Definitions *)
|
clasohm@923
|
182 |
|
clasohm@923
|
183 |
Let_def "Let s f == f(s)"
|
clasohm@923
|
184 |
o_def "(f::'b=>'c) o g == (%(x::'a). f(g(x)))"
|
nipkow@973
|
185 |
if_def "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
|
wenzelm@4371
|
186 |
arbitrary_def "False ==> arbitrary == (@x. False)"
|
clasohm@923
|
187 |
|
nipkow@3320
|
188 |
|
clasohm@923
|
189 |
end
|
clasohm@923
|
190 |
|
wenzelm@2260
|
191 |
|
clasohm@923
|
192 |
ML
|
clasohm@923
|
193 |
|
wenzelm@4793
|
194 |
|
wenzelm@4793
|
195 |
(** initial HOL theory setup **)
|
wenzelm@4793
|
196 |
|
wenzelm@4793
|
197 |
val thy_setup = [Simplifier.setup, ClasetThyData.setup, ThyData.setup];
|
wenzelm@4793
|
198 |
|
wenzelm@4793
|
199 |
|
clasohm@923
|
200 |
(** Choice between the HOL and Isabelle style of quantifiers **)
|
clasohm@923
|
201 |
|
clasohm@923
|
202 |
val HOL_quantifiers = ref true;
|
clasohm@923
|
203 |
|
clasohm@923
|
204 |
fun alt_ast_tr' (name, alt_name) =
|
clasohm@923
|
205 |
let
|
clasohm@923
|
206 |
fun ast_tr' (*name*) args =
|
clasohm@923
|
207 |
if ! HOL_quantifiers then raise Match
|
clasohm@923
|
208 |
else Syntax.mk_appl (Syntax.Constant alt_name) args;
|
clasohm@923
|
209 |
in
|
clasohm@923
|
210 |
(name, ast_tr')
|
clasohm@923
|
211 |
end;
|
clasohm@923
|
212 |
|
clasohm@923
|
213 |
|
clasohm@923
|
214 |
val print_ast_translation =
|
clasohm@923
|
215 |
map alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")];
|