0
|
1 |
(* Title: HOL/hol.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 1993 University of Cambridge
|
|
5 |
|
|
6 |
Higher-Order Logic
|
|
7 |
*)
|
|
8 |
|
|
9 |
HOL = Pure +
|
|
10 |
|
|
11 |
classes
|
|
12 |
term < logic
|
|
13 |
plus < term
|
|
14 |
minus < term
|
|
15 |
times < term
|
|
16 |
|
11
|
17 |
default
|
|
18 |
term
|
0
|
19 |
|
|
20 |
types
|
49
|
21 |
bool
|
25
|
22 |
letbinds, letbind 0
|
38
|
23 |
case_syn,cases_syn 0
|
0
|
24 |
|
|
25 |
arities
|
|
26 |
fun :: (term, term) term
|
|
27 |
bool :: term
|
|
28 |
|
|
29 |
|
|
30 |
consts
|
|
31 |
|
|
32 |
(* Constants *)
|
|
33 |
|
4
|
34 |
Trueprop :: "bool => prop" ("(_)" 5)
|
|
35 |
not :: "bool => bool" ("~ _" [40] 40)
|
0
|
36 |
True, False :: "bool"
|
|
37 |
if :: "[bool, 'a, 'a] => 'a"
|
|
38 |
Inv :: "('a => 'b) => ('b => 'a)"
|
|
39 |
|
|
40 |
(* Binders *)
|
|
41 |
|
4
|
42 |
Eps :: "('a => bool) => 'a" (binder "@" 10)
|
|
43 |
All :: "('a => bool) => bool" (binder "! " 10)
|
|
44 |
Ex :: "('a => bool) => bool" (binder "? " 10)
|
|
45 |
Ex1 :: "('a => bool) => bool" (binder "?! " 10)
|
0
|
46 |
|
4
|
47 |
Let :: "['a, 'a => 'b] => 'b"
|
25
|
48 |
"_bind" :: "[idt, 'a] => letbind" ("(2_ =/ _)" 10)
|
|
49 |
"" :: "letbind => letbinds" ("_")
|
|
50 |
"_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _")
|
|
51 |
"_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10)
|
0
|
52 |
|
38
|
53 |
(* Case expressions *)
|
|
54 |
|
|
55 |
"@case" :: "['a, cases_syn] => 'b" ("(case _ of/ _)" 10)
|
|
56 |
"@case1" :: "['a, 'b] => case_syn" ("(2_ =>/ _)" 10)
|
|
57 |
"" :: "case_syn => cases_syn" ("_")
|
|
58 |
"@case2" :: "[case_syn,cases_syn] => cases_syn" ("_/ | _")
|
|
59 |
|
0
|
60 |
(* Alternative Quantifiers *)
|
|
61 |
|
4
|
62 |
"*All" :: "[idts, bool] => bool" ("(3ALL _./ _)" 10)
|
|
63 |
"*Ex" :: "[idts, bool] => bool" ("(3EX _./ _)" 10)
|
|
64 |
"*Ex1" :: "[idts, bool] => bool" ("(3EX! _./ _)" 10)
|
0
|
65 |
|
|
66 |
(* Infixes *)
|
|
67 |
|
4
|
68 |
o :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixr 50)
|
11
|
69 |
"=" :: "['a, 'a] => bool" (infixl 50)
|
|
70 |
"~=" :: "['a, 'a] => bool" ("(_ ~=/ _)" [50, 51] 50)
|
4
|
71 |
"&" :: "[bool, bool] => bool" (infixr 35)
|
|
72 |
"|" :: "[bool, bool] => bool" (infixr 30)
|
|
73 |
"-->" :: "[bool, bool] => bool" (infixr 25)
|
0
|
74 |
|
|
75 |
(* Overloaded Constants *)
|
|
76 |
|
4
|
77 |
"+" :: "['a::plus, 'a] => 'a" (infixl 65)
|
|
78 |
"-" :: "['a::minus, 'a] => 'a" (infixl 65)
|
|
79 |
"*" :: "['a::times, 'a] => 'a" (infixl 70)
|
0
|
80 |
|
|
81 |
|
|
82 |
translations
|
|
83 |
"ALL xs. P" => "! xs. P"
|
|
84 |
"EX xs. P" => "? xs. P"
|
|
85 |
"EX! xs. P" => "?! xs. P"
|
11
|
86 |
"x ~= y" == "~ (x = y)"
|
25
|
87 |
"_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))"
|
|
88 |
"let x = a in e" == "Let(a, %x. e)"
|
0
|
89 |
|
|
90 |
rules
|
|
91 |
|
|
92 |
eq_reflection "(x=y) ==> (x==y)"
|
|
93 |
|
|
94 |
(* Basic Rules *)
|
|
95 |
|
|
96 |
refl "t = t::'a"
|
|
97 |
subst "[| s = t; P(s) |] ==> P(t::'a)"
|
|
98 |
ext "(!!x::'a. f(x)::'b = g(x)) ==> (%x.f(x)) = (%x.g(x))"
|
|
99 |
selectI "P(x::'a) ==> P(@x.P(x))"
|
|
100 |
|
|
101 |
impI "(P ==> Q) ==> P-->Q"
|
|
102 |
mp "[| P-->Q; P |] ==> Q"
|
|
103 |
|
|
104 |
(* Definitions *)
|
|
105 |
|
66
|
106 |
True_def "True == ((%x::bool.x)=(%x.x))"
|
|
107 |
All_def "All == (%P. P = (%x.True))"
|
|
108 |
Ex_def "Ex == (%P. P(@x.P(x)))"
|
|
109 |
False_def "False == (!P.P)"
|
|
110 |
not_def "not == (%P. P-->False)"
|
|
111 |
and_def "op & == (%P Q. !R. (P-->Q-->R) --> R)"
|
|
112 |
or_def "op | == (%P Q. !R. (P-->R) --> (Q-->R) --> R)"
|
|
113 |
Ex1_def "Ex1 == (%P. ? x. P(x) & (! y. P(y) --> y=x))"
|
|
114 |
Let_def "Let(s, f) == f(s)"
|
0
|
115 |
|
|
116 |
(* Axioms *)
|
|
117 |
|
|
118 |
iff "(P-->Q) --> (Q-->P) --> (P=Q)"
|
|
119 |
True_or_False "(P=True) | (P=False)"
|
|
120 |
|
|
121 |
(* Misc Definitions *)
|
|
122 |
|
66
|
123 |
Inv_def "Inv == (%(f::'a=>'b) y. @x. f(x)=y)"
|
|
124 |
o_def "op o == (%(f::'b=>'c) g (x::'a). f(g(x)))"
|
0
|
125 |
|
66
|
126 |
if_def "if == (%P x y.@z::'a. (P=True --> z=x) & (P=False --> z=y))"
|
0
|
127 |
|
|
128 |
end
|
|
129 |
|
|
130 |
|
|
131 |
ML
|
|
132 |
|
|
133 |
(** Choice between the HOL and Isabelle style of quantifiers **)
|
|
134 |
|
|
135 |
val HOL_quantifiers = ref true;
|
|
136 |
|
4
|
137 |
fun alt_ast_tr' (name, alt_name) =
|
0
|
138 |
let
|
|
139 |
fun ast_tr' (*name*) args =
|
|
140 |
if ! HOL_quantifiers then raise Match
|
4
|
141 |
else Syntax.mk_appl (Syntax.Constant alt_name) args;
|
0
|
142 |
in
|
|
143 |
(name, ast_tr')
|
|
144 |
end;
|
|
145 |
|
|
146 |
|
|
147 |
val print_ast_translation =
|
7
|
148 |
map alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")];
|
0
|
149 |
|