author  wenzelm 
Tue, 03 Jul 2007 22:27:11 +0200  
changeset 23555  16e5fd18905c 
parent 23297  06f108974fa1 
child 23566  b65692d4adcd 
permissions  rwrr 
923  1 
(* Title: HOL/hologic.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson and Markus Wenzel 

4 

5 
Abstract syntax operations for HOL. 

6 
*) 

7 

8 
signature HOLOGIC = 

9 
sig 

12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11818
diff
changeset

10 
val typeS: sort 
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11818
diff
changeset

11 
val typeT: typ 
8275  12 
val boolN: string 
923  13 
val boolT: typ 
21829
016eff9c5699
simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
wenzelm
parents:
21820
diff
changeset

14 
val true_const: term 
7073  15 
val false_const: term 
923  16 
val mk_setT: typ > typ 
17 
val dest_setT: typ > typ 

15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15945
diff
changeset

18 
val Trueprop: term 
923  19 
val mk_Trueprop: term > term 
20 
val dest_Trueprop: term > term 

23555
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

21 
val dest_cTrueprop: cterm > cterm 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

22 
val Trueprop_conv: conv > conv 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

23 
val conj_intr: thm > thm > thm 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

24 
val conj_elim: thm > thm * thm 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

25 
val conj_elims: thm > thm list 
923  26 
val conj: term 
27 
val disj: term 

28 
val imp: term 

8429  29 
val Not: term 
7690  30 
val mk_conj: term * term > term 
31 
val mk_disj: term * term > term 

32 
val mk_imp: term * term > term 

16835  33 
val mk_not: term > term 
15151  34 
val dest_conj: term > term list 
15945  35 
val dest_disj: term > term list 
4571  36 
val dest_imp: term > term * term 
15151  37 
val dest_not: term > term 
11683  38 
val dest_concls: term > term list 
923  39 
val eq_const: typ > term 
21829
016eff9c5699
simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
wenzelm
parents:
21820
diff
changeset

40 
val mk_eq: term * term > term 
016eff9c5699
simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
wenzelm
parents:
21820
diff
changeset

41 
val dest_eq: term > term * term 
923  42 
val all_const: typ > term 
21829
016eff9c5699
simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
wenzelm
parents:
21820
diff
changeset

43 
val mk_all: string * typ * term > term 
016eff9c5699
simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
wenzelm
parents:
21820
diff
changeset

44 
val list_all: (string * typ) list * term > term 
923  45 
val exists_const: typ > term 
21829
016eff9c5699
simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
wenzelm
parents:
21820
diff
changeset

46 
val mk_exists: string * typ * term > term 
15945  47 
val choice_const: typ > term 
923  48 
val Collect_const: typ > term 
49 
val mk_Collect: string * typ * term > term 

21829
016eff9c5699
simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
wenzelm
parents:
21820
diff
changeset

50 
val class_eq: string 
923  51 
val mk_mem: term * term > term 
6380  52 
val dest_mem: term > term * term 
11818  53 
val mk_UNIV: typ > term 
2510  54 
val mk_binop: string > term * term > term 
55 
val mk_binrel: string > term * term > term 

56 
val dest_bin: string > typ > term > term * term 

4571  57 
val unitT: typ 
9362  58 
val is_unitT: typ > bool 
4571  59 
val unit: term 
60 
val is_unit: term > bool 

61 
val mk_prodT: typ * typ > typ 

62 
val dest_prodT: typ > typ * typ 

14048  63 
val pair_const: typ > typ > term 
4571  64 
val mk_prod: term * term > term 
65 
val dest_prod: term > term * term 

66 
val mk_fst: term > term 

67 
val mk_snd: term > term 

21829
016eff9c5699
simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
wenzelm
parents:
21820
diff
changeset

68 
val split_const: typ * typ * typ > term 
18285  69 
val mk_split: term > term 
5096
84b00be693b4
Moved most of the Prod_Syntax  stuff to HOLogic.
berghofe
parents:
4571
diff
changeset

70 
val prodT_factors: typ > typ list 
84b00be693b4
Moved most of the Prod_Syntax  stuff to HOLogic.
berghofe
parents:
4571
diff
changeset

71 
val mk_tuple: typ > term list > term 
5207  72 
val natT: typ 
73 
val zero: term 

74 
val is_zero: term > bool 

75 
val mk_Suc: term > term 

76 
val dest_Suc: term > term 

21621  77 
val Suc_zero: term 
23247  78 
val mk_nat: integer > term 
79 
val dest_nat: term > integer 

22994  80 
val class_size: string 
81 
val size_const: typ > term 

15620
8ccdc8bc66a2
replaced bool by a new datatype "bit" for binary numerals
paulson
parents:
15595
diff
changeset

82 
val bitT: typ 
8ccdc8bc66a2
replaced bool by a new datatype "bit" for binary numerals
paulson
parents:
15595
diff
changeset

83 
val B0_const: term 
8ccdc8bc66a2
replaced bool by a new datatype "bit" for binary numerals
paulson
parents:
15595
diff
changeset

84 
val B1_const: term 
21778
66440bf72cdc
binary numerals: restricted to actual abstract syntax;
wenzelm
parents:
21755
diff
changeset

85 
val mk_bit: int > term 
66440bf72cdc
binary numerals: restricted to actual abstract syntax;
wenzelm
parents:
21755
diff
changeset

86 
val dest_bit: term > int 
21829
016eff9c5699
simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
wenzelm
parents:
21820
diff
changeset

87 
val intT: typ 
7073  88 
val pls_const: term 
89 
val min_const: term 

90 
val bit_const: term 

23247  91 
val mk_numeral: integer > term 
92 
val dest_numeral: term > integer 

21829
016eff9c5699
simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
wenzelm
parents:
21820
diff
changeset

93 
val number_of_const: typ > term 
23269  94 
val add_numerals: term > (term * typ) list > (term * typ) list 
23247  95 
val mk_number: typ > integer > term 
96 
val dest_number: term > typ * integer 

21778
66440bf72cdc
binary numerals: restricted to actual abstract syntax;
wenzelm
parents:
21755
diff
changeset

97 
val realT: typ 
21755  98 
val nibbleT: typ 
99 
val mk_nibble: int > term 

100 
val dest_nibble: term > int 

101 
val charT: typ 

102 
val mk_char: int > term 

103 
val dest_char: term > int 

21829
016eff9c5699
simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
wenzelm
parents:
21820
diff
changeset

104 
val listT: typ > typ 
016eff9c5699
simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
wenzelm
parents:
21820
diff
changeset

105 
val mk_list: typ > term list > term 
016eff9c5699
simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
wenzelm
parents:
21820
diff
changeset

106 
val dest_list: term > term list 
21778
66440bf72cdc
binary numerals: restricted to actual abstract syntax;
wenzelm
parents:
21755
diff
changeset

107 
val stringT: typ 
21820
2f2b6a965ccc
introduced mk/dest_numeral/number for mk/dest_binum etc.
haftmann
parents:
21788
diff
changeset

108 
val mk_string: string > term 
2f2b6a965ccc
introduced mk/dest_numeral/number for mk/dest_binum etc.
haftmann
parents:
21788
diff
changeset

109 
val dest_string: term > string 
923  110 
end; 
111 

112 
structure HOLogic: HOLOGIC = 

113 
struct 

114 

12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11818
diff
changeset

115 
(* HOL syntax *) 
923  116 

12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11818
diff
changeset

117 
val typeS: sort = ["HOL.type"]; 
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11818
diff
changeset

118 
val typeT = TypeInfer.anyT typeS; 
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11818
diff
changeset

119 

923  120 

2510  121 
(* bool and set *) 
923  122 

8275  123 
val boolN = "bool"; 
124 
val boolT = Type (boolN, []); 

923  125 

9856  126 
val true_const = Const ("True", boolT); 
127 
val false_const = Const ("False", boolT); 

7073  128 

923  129 
fun mk_setT T = Type ("set", [T]); 
130 

131 
fun dest_setT (Type ("set", [T])) = T 

3794  132 
 dest_setT T = raise TYPE ("dest_setT: set type expected", [T], []); 
923  133 

8275  134 

7073  135 
(* logic *) 
923  136 

137 
val Trueprop = Const ("Trueprop", boolT > propT); 

138 

139 
fun mk_Trueprop P = Trueprop $ P; 

140 

141 
fun dest_Trueprop (Const ("Trueprop", _) $ P) = P 

3794  142 
 dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); 
923  143 

23555
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

144 
fun dest_cTrueprop ct = 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

145 
if can dest_Trueprop (Thm.term_of ct) then Thm.dest_arg ct 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

146 
else raise CTERM ("cdest_Trueprop", [ct]); 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

147 

16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

148 
fun Trueprop_conv conv ct = 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

149 
if can dest_Trueprop (Thm.term_of ct) then Conv.arg_conv conv ct 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

150 
else raise CTERM ("Trueprop_conv", [ct]); 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

151 

16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

152 
fun conj_intr thP thQ = 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

153 
let 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

154 
val (P, Q) = pairself (dest_cTrueprop o Thm.cprop_of) (thP, thQ) 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

155 
handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]); 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

156 
val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]); 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

157 
in Drule.implies_elim_list (inst @{thm conjI}) [thP, thQ] end; 
923  158 

23555
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

159 
fun conj_elim thPQ = 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

160 
let 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

161 
val (P, Q) = Thm.dest_binop (dest_cTrueprop (Thm.cprop_of thPQ)) 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

162 
handle CTERM (msg, _) => raise THM (msg, 0, [thPQ]); 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

163 
val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]); 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

164 
val thP = Thm.implies_elim (inst @{thm conjunct1}) thPQ; 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

165 
val thQ = Thm.implies_elim (inst @{thm conjunct2}) thPQ; 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

166 
in (thP, thQ) end; 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

167 

16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

168 
fun conj_elims th = 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

169 
let val (th1, th2) = conj_elim th 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

170 
in conj_elims th1 @ conj_elims th2 end handle THM _ => [th]; 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

171 

16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

172 
val conj = @{term "op &"} 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

173 
and disj = @{term "op "} 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

174 
and imp = @{term "op >"} 
16e5fd18905c
assume basic HOL context for compilation (antiquotations);
wenzelm
parents:
23297
diff
changeset

175 
and Not = @{term "Not"}; 
923  176 

7690  177 
fun mk_conj (t1, t2) = conj $ t1 $ t2 
178 
and mk_disj (t1, t2) = disj $ t1 $ t2 

16835  179 
and mk_imp (t1, t2) = imp $ t1 $ t2 
180 
and mk_not t = Not $ t; 

7690  181 

15151  182 
fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t' 
183 
 dest_conj t = [t]; 

184 

15945  185 
fun dest_disj (Const ("op ", _) $ t $ t') = t :: dest_disj t' 
186 
 dest_disj t = [t]; 

187 

4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4294
diff
changeset

188 
fun dest_imp (Const("op >",_) $ A $ B) = (A, B) 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4294
diff
changeset

189 
 dest_imp t = raise TERM ("dest_imp", [t]); 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4294
diff
changeset

190 

15151  191 
fun dest_not (Const ("Not", _) $ t) = t 
192 
 dest_not t = raise TERM ("dest_not", [t]); 

8302  193 

11683  194 
fun imp_concl_of t = imp_concl_of (#2 (dest_imp t)) handle TERM _ => t; 
195 
val dest_concls = map imp_concl_of o dest_conj o dest_Trueprop; 

196 

923  197 
fun eq_const T = Const ("op =", [T, T] > boolT); 
198 
fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u; 

199 

6031  200 
fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs) 
201 
 dest_eq t = raise TERM ("dest_eq", [t]) 

202 

923  203 
fun all_const T = Const ("All", [T > boolT] > boolT); 
204 
fun mk_all (x, T, P) = all_const T $ absfree (x, T, P); 

21173
663a7b39894c
removed is_Trueprop (use can dest_Trueprop'' instead);
wenzelm
parents:
21078
diff
changeset

205 
fun list_all (xs, t) = fold_rev (fn (x, T) => fn P => all_const T $ Abs (x, T, P)) xs t; 
923  206 

207 
fun exists_const T = Const ("Ex", [T > boolT] > boolT); 

208 
fun mk_exists (x, T, P) = exists_const T $ absfree (x, T, P); 

209 

21755  210 
fun choice_const T = Const("Hilbert_Choice.Eps", (T > boolT) > T); 
15945  211 

923  212 
fun Collect_const T = Const ("Collect", [T > boolT] > mk_setT T); 
213 
fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T, t); 

214 

23247  215 
val class_eq = "HOL.eq"; 
21045  216 

923  217 
fun mk_mem (x, A) = 
218 
let val setT = fastype_of A in 

219 
Const ("op :", [dest_setT setT, setT] > boolT) $ x $ A 

220 
end; 

221 

6380  222 
fun dest_mem (Const ("op :", _) $ x $ A) = (x, A) 
223 
 dest_mem t = raise TERM ("dest_mem", [t]); 

224 

11818  225 
fun mk_UNIV T = Const ("UNIV", mk_setT T); 
226 

923  227 

13743
f8f9393be64c
Fixed bug in simpdata.ML that prevented the use of congruence rules from a
ballarin
parents:
13640
diff
changeset

228 
(* binary operations and relations *) 
2510  229 

230 
fun mk_binop c (t, u) = 

231 
let val T = fastype_of t in 

232 
Const (c, [T, T] > T) $ t $ u 

233 
end; 

234 

235 
fun mk_binrel c (t, u) = 

236 
let val T = fastype_of t in 

237 
Const (c, [T, T] > boolT) $ t $ u 

238 
end; 

239 

14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14103
diff
changeset

240 
(*destruct the application of a binary operator. The dummyT case is a crude 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14103
diff
changeset

241 
way of handling polymorphic operators.*) 
2510  242 
fun dest_bin c T (tm as Const (c', Type ("fun", [T', _])) $ t $ u) = 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14103
diff
changeset

243 
if c = c' andalso (T=T' orelse T=dummyT) then (t, u) 
3794  244 
else raise TERM ("dest_bin " ^ c, [tm]) 
245 
 dest_bin c _ tm = raise TERM ("dest_bin " ^ c, [tm]); 

2510  246 

247 

4571  248 
(* unit *) 
249 

11604  250 
val unitT = Type ("Product_Type.unit", []); 
4571  251 

11604  252 
fun is_unitT (Type ("Product_Type.unit", [])) = true 
9362  253 
 is_unitT _ = false; 
254 

11604  255 
val unit = Const ("Product_Type.Unity", unitT); 
4571  256 

11604  257 
fun is_unit (Const ("Product_Type.Unity", _)) = true 
4571  258 
 is_unit _ = false; 
259 

260 

261 
(* prod *) 

262 

263 
fun mk_prodT (T1, T2) = Type ("*", [T1, T2]); 

264 

265 
fun dest_prodT (Type ("*", [T1, T2])) = (T1, T2) 

266 
 dest_prodT T = raise TYPE ("dest_prodT", [T], []); 

267 

14048  268 
fun pair_const T1 T2 = Const ("Pair", [T1, T2] > mk_prodT (T1, T2)); 
269 

4571  270 
fun mk_prod (t1, t2) = 
271 
let val T1 = fastype_of t1 and T2 = fastype_of t2 in 

14048  272 
pair_const T1 T2 $ t1 $ t2 
4571  273 
end; 
274 

275 
fun dest_prod (Const ("Pair", _) $ t1 $ t2) = (t1, t2) 

276 
 dest_prod t = raise TERM ("dest_prod", [t]); 

277 

278 
fun mk_fst p = 

279 
let val pT = fastype_of p in 

280 
Const ("fst", pT > fst (dest_prodT pT)) $ p 

281 
end; 

282 

283 
fun mk_snd p = 

284 
let val pT = fastype_of p in 

285 
Const ("snd", pT > snd (dest_prodT pT)) $ p 

286 
end; 

287 

18285  288 
fun split_const (A, B, C) = 
289 
Const ("split", (A > B > C) > mk_prodT (A, B) > C); 

290 

291 
fun mk_split t = 

292 
(case Term.fastype_of t of 

293 
T as (Type ("fun", [A, Type ("fun", [B, C])])) => 

294 
Const ("split", T > mk_prodT (A, B) > C) $ t 

295 
 _ => raise TERM ("mk_split: bad body type", [t])); 

296 

5096
84b00be693b4
Moved most of the Prod_Syntax  stuff to HOLogic.
berghofe
parents:
4571
diff
changeset

297 
(*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*) 
84b00be693b4
Moved most of the Prod_Syntax  stuff to HOLogic.
berghofe
parents:
4571
diff
changeset

298 
fun prodT_factors (Type ("*", [T1, T2])) = prodT_factors T1 @ prodT_factors T2 
84b00be693b4
Moved most of the Prod_Syntax  stuff to HOLogic.
berghofe
parents:
4571
diff
changeset

299 
 prodT_factors T = [T]; 
84b00be693b4
Moved most of the Prod_Syntax  stuff to HOLogic.
berghofe
parents:
4571
diff
changeset

300 

84b00be693b4
Moved most of the Prod_Syntax  stuff to HOLogic.
berghofe
parents:
4571
diff
changeset

301 
(*Makes a nested tuple from a list, following the product type structure*) 
16971  302 
fun mk_tuple (Type ("*", [T1, T2])) tms = 
303 
mk_prod (mk_tuple T1 tms, 

15570  304 
mk_tuple T2 (Library.drop (length (prodT_factors T1), tms))) 
5096
84b00be693b4
Moved most of the Prod_Syntax  stuff to HOLogic.
berghofe
parents:
4571
diff
changeset

305 
 mk_tuple T (t::_) = t; 
4571  306 

5207  307 

308 
(* nat *) 

309 

310 
val natT = Type ("nat", []); 

311 

22994  312 
val zero = Const ("HOL.zero_class.zero", natT); 
5207  313 

22994  314 
fun is_zero (Const ("HOL.zero_class.zero", _)) = true 
5207  315 
 is_zero _ = false; 
316 

317 
fun mk_Suc t = Const ("Suc", natT > natT) $ t; 

318 

319 
fun dest_Suc (Const ("Suc", _) $ t) = t 

320 
 dest_Suc t = raise TERM ("dest_Suc", [t]); 

321 

21621  322 
val Suc_zero = mk_Suc zero; 
323 

23297  324 
fun mk_nat (n: integer) = 
22994  325 
let 
326 
fun mk 0 = zero 

23297  327 
 mk n = mk_Suc (mk (n  1)); 
328 
in if n < 0 then raise TERM ("mk_nat: negative numeral", []) else mk n end; 

5207  329 

23297  330 
fun dest_nat (Const ("HOL.zero_class.zero", _)) = (0: integer) 
331 
 dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1 

5207  332 
 dest_nat t = raise TERM ("dest_nat", [t]); 
333 

22994  334 
val class_size = "Nat.size"; 
335 

336 
fun size_const T = Const ("Nat.size_class.size", T > natT); 

337 

5207  338 

21778
66440bf72cdc
binary numerals: restricted to actual abstract syntax;
wenzelm
parents:
21755
diff
changeset

339 
(* bit *) 
7073  340 

15620
8ccdc8bc66a2
replaced bool by a new datatype "bit" for binary numerals
paulson
parents:
15595
diff
changeset

341 
val bitT = Type ("Numeral.bit", []); 
8ccdc8bc66a2
replaced bool by a new datatype "bit" for binary numerals
paulson
parents:
15595
diff
changeset

342 

8ccdc8bc66a2
replaced bool by a new datatype "bit" for binary numerals
paulson
parents:
15595
diff
changeset

343 
val B0_const = Const ("Numeral.bit.B0", bitT); 
8ccdc8bc66a2
replaced bool by a new datatype "bit" for binary numerals
paulson
parents:
15595
diff
changeset

344 
val B1_const = Const ("Numeral.bit.B1", bitT); 
8ccdc8bc66a2
replaced bool by a new datatype "bit" for binary numerals
paulson
parents:
15595
diff
changeset

345 

21778
66440bf72cdc
binary numerals: restricted to actual abstract syntax;
wenzelm
parents:
21755
diff
changeset

346 
fun mk_bit 0 = B0_const 
66440bf72cdc
binary numerals: restricted to actual abstract syntax;
wenzelm
parents:
21755
diff
changeset

347 
 mk_bit 1 = B1_const 
66440bf72cdc
binary numerals: restricted to actual abstract syntax;
wenzelm
parents:
21755
diff
changeset

348 
 mk_bit _ = raise TERM ("mk_bit", []); 
66440bf72cdc
binary numerals: restricted to actual abstract syntax;
wenzelm
parents:
21755
diff
changeset

349 

66440bf72cdc
binary numerals: restricted to actual abstract syntax;
wenzelm
parents:
21755
diff
changeset

350 
fun dest_bit (Const ("Numeral.bit.B0", _)) = 0 
66440bf72cdc
binary numerals: restricted to actual abstract syntax;
wenzelm
parents:
21755
diff
changeset

351 
 dest_bit (Const ("Numeral.bit.B1", _)) = 1 
66440bf72cdc
binary numerals: restricted to actual abstract syntax;
wenzelm
parents:
21755
diff
changeset

352 
 dest_bit t = raise TERM ("dest_bit", [t]); 
66440bf72cdc
binary numerals: restricted to actual abstract syntax;
wenzelm
parents:
21755
diff
changeset

353 

66440bf72cdc
binary numerals: restricted to actual abstract syntax;
wenzelm
parents:
21755
diff
changeset

354 

66440bf72cdc
binary numerals: restricted to actual abstract syntax;
wenzelm
parents:
21755
diff
changeset

355 
(* binary numerals and int  nonunique representation due to leading zeros/ones! *) 
66440bf72cdc
binary numerals: restricted to actual abstract syntax;
wenzelm
parents:
21755
diff
changeset

356 

66440bf72cdc
binary numerals: restricted to actual abstract syntax;
wenzelm
parents:
21755
diff
changeset

357 
val intT = Type ("IntDef.int", []); 
66440bf72cdc
binary numerals: restricted to actual abstract syntax;
wenzelm
parents:
21755
diff
changeset

358 

20485  359 
val pls_const = Const ("Numeral.Pls", intT) 
360 
and min_const = Const ("Numeral.Min", intT) 

23247  361 
and bit_const = Const ("Numeral.Bit", intT > bitT > intT); 
8768  362 

21829
016eff9c5699
simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
wenzelm
parents:
21820
diff
changeset

363 
fun mk_numeral 0 = pls_const 
016eff9c5699
simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
wenzelm
parents:
21820
diff
changeset

364 
 mk_numeral ~1 = min_const 
016eff9c5699
simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
wenzelm
parents:
21820
diff
changeset

365 
 mk_numeral i = 
23247  366 
let val (q, r) = Integer.divmod i 2 
367 
in bit_const $ mk_numeral q $ mk_bit (Integer.machine_int r) end; 

13755  368 

21829
016eff9c5699
simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
wenzelm
parents:
21820
diff
changeset

369 
fun dest_numeral (Const ("Numeral.Pls", _)) = 0 
016eff9c5699
simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
wenzelm
parents:
21820
diff
changeset

370 
 dest_numeral (Const ("Numeral.Min", _)) = ~1 
016eff9c5699
simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
wenzelm
parents:
21820
diff
changeset

371 
 dest_numeral (Const ("Numeral.Bit", _) $ bs $ b) = 
23297  372 
2 * dest_numeral bs + Integer.int (dest_bit b) 
21829
016eff9c5699
simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
wenzelm
parents:
21820
diff
changeset

373 
 dest_numeral t = raise TERM ("dest_numeral", [t]); 
13755  374 

22994  375 
fun number_of_const T = Const ("Numeral.number_class.number_of", intT > T); 
21820
2f2b6a965ccc
introduced mk/dest_numeral/number for mk/dest_binum etc.
haftmann
parents:
21788
diff
changeset

376 

23269  377 
fun add_numerals (Const ("Numeral.number_class.number_of", Type (_, [_, T])) $ t) = cons (t, T) 
378 
 add_numerals (t $ u) = add_numerals t #> add_numerals u 

379 
 add_numerals (Abs (_, _, t)) = add_numerals t 

380 
 add_numerals _ = I; 

22391  381 

22994  382 
fun mk_number T 0 = Const ("HOL.zero_class.zero", T) 
383 
 mk_number T 1 = Const ("HOL.one_class.one", T) 

21820
2f2b6a965ccc
introduced mk/dest_numeral/number for mk/dest_binum etc.
haftmann
parents:
21788
diff
changeset

384 
 mk_number T i = number_of_const T $ mk_numeral i; 
2f2b6a965ccc
introduced mk/dest_numeral/number for mk/dest_binum etc.
haftmann
parents:
21788
diff
changeset

385 

22994  386 
fun dest_number (Const ("HOL.zero_class.zero", T)) = (T, 0) 
387 
 dest_number (Const ("HOL.one_class.one", T)) = (T, 1) 

388 
 dest_number (Const ("Numeral.number_class.number_of", Type ("fun", [_, T])) $ t) = 

389 
(T, dest_numeral t) 

21820
2f2b6a965ccc
introduced mk/dest_numeral/number for mk/dest_binum etc.
haftmann
parents:
21788
diff
changeset

390 
 dest_number t = raise TERM ("dest_number", [t]); 
13755  391 

21829
016eff9c5699
simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
wenzelm
parents:
21820
diff
changeset

392 

13755  393 
(* real *) 
394 

16971  395 
val realT = Type ("RealDef.real", []); 
13755  396 

397 

21755  398 
(* nibble *) 
399 

400 
val nibbleT = Type ("List.nibble", []); 

13755  401 

21755  402 
fun mk_nibble n = 
403 
let val s = 

404 
if 0 <= n andalso n <= 9 then chr (n + ord "0") 

405 
else if 10 <= n andalso n <= 15 then chr (n + ord "A"  10) 

406 
else raise TERM ("mk_nibble", []) 

407 
in Const ("List.nibble.Nibble" ^ s, nibbleT) end; 

17083  408 

21755  409 
fun dest_nibble t = 
410 
let fun err () = raise TERM ("dest_nibble", [t]) in 

411 
(case try (unprefix "List.nibble.Nibble" o fst o Term.dest_Const) t of 

412 
NONE => err () 

413 
 SOME c => 

414 
if size c <> 1 then err () 

415 
else if "0" <= c andalso c <= "9" then ord c  ord "0" 

416 
else if "A" <= c andalso c <= "F" then ord c  ord "A" + 10 

417 
else err ()) 

418 
end; 

15062  419 

21455  420 

421 
(* char *) 

422 

423 
val charT = Type ("List.char", []); 

424 

21755  425 
fun mk_char n = 
426 
if 0 <= n andalso n <= 255 then 

427 
Const ("List.char.Char", nibbleT > nibbleT > charT) $ 

428 
mk_nibble (n div 16) $ mk_nibble (n mod 16) 

429 
else raise TERM ("mk_char", []); 

21455  430 

21755  431 
fun dest_char (Const ("List.char.Char", _) $ t $ u) = 
432 
dest_nibble t * 16 + dest_nibble u 

433 
 dest_char t = raise TERM ("dest_char", [t]); 

21455  434 

21755  435 

436 
(* list *) 

21455  437 

21755  438 
fun listT T = Type ("List.list", [T]); 
21455  439 

21755  440 
fun mk_list T ts = 
21455  441 
let 
21755  442 
val lT = listT T; 
443 
val Nil = Const ("List.list.Nil", lT); 

444 
fun Cons t u = Const ("List.list.Cons", T > lT > lT) $ t $ u; 

445 
in fold_rev Cons ts Nil end; 

446 

447 
fun dest_list (Const ("List.list.Nil", _)) = [] 

448 
 dest_list (Const ("List.list.Cons", _) $ t $ u) = t :: dest_list u 

449 
 dest_list t = raise TERM ("dest_list", [t]); 

21455  450 

451 

452 
(* string *) 

453 

21820
2f2b6a965ccc
introduced mk/dest_numeral/number for mk/dest_binum etc.
haftmann
parents:
21788
diff
changeset

454 
val stringT = Type ("List.string", []); 
21455  455 

21755  456 
val mk_string = mk_list charT o map (mk_char o ord) o explode; 
457 
val dest_string = implode o map (chr o dest_char) o dest_list; 

21455  458 

923  459 
end; 