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