author  haftmann 
Wed, 11 Mar 2009 15:56:51 +0100  
changeset 30450  7655e6533209 
parent 30304  d8e4cd2ac2a1 
child 30453  1e7e0d171653 
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 
30450  14 
val Trueprop: term 
15 
val mk_Trueprop: term > term 

16 
val dest_Trueprop: term > term 

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

17 
val true_const: term 
7073  18 
val false_const: term 
923  19 
val mk_setT: typ > typ 
20 
val dest_setT: typ > typ 

30450  21 
val Collect_const: typ > term 
22 
val mk_Collect: string * typ * term > term 

23 
val mk_mem: term * term > term 

24 
val dest_mem: term > term * term 

25 
val mk_set: typ > term list > term 

26 
val dest_set: term > term list 

27 
val mk_UNIV: typ > term 

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

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

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

30 
val conj_elims: thm > thm list 
923  31 
val conj: term 
32 
val disj: term 

33 
val imp: term 

8429  34 
val Not: term 
7690  35 
val mk_conj: term * term > term 
36 
val mk_disj: term * term > term 

37 
val mk_imp: term * term > term 

16835  38 
val mk_not: term > term 
15151  39 
val dest_conj: term > term list 
15945  40 
val dest_disj: term > term list 
24958  41 
val disjuncts: term > term list 
4571  42 
val dest_imp: term > term * term 
15151  43 
val dest_not: term > term 
923  44 
val eq_const: typ > term 
21829
016eff9c5699
simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
wenzelm
parents:
21820
diff
changeset

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

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

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

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

51 
val mk_exists: string * typ * term > term 
15945  52 
val choice_const: typ > term 
21829
016eff9c5699
simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
wenzelm
parents:
21820
diff
changeset

53 
val class_eq: string 
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 
23745  72 
val dest_tuple: term > term list 
73 
val ap_split: typ > typ > term > term 

74 
val prod_factors: term > int list list 

75 
val dest_tuple': int list list > term > term list 

76 
val prodT_factors': int list list > typ > typ list 

77 
val ap_split': int list list > typ > typ > term > term 

78 
val mk_tuple': int list list > typ > term list > term 

79 
val mk_tupleT: int list list > typ list > typ 

80 
val strip_split: term > term * typ list * int list list 

5207  81 
val natT: typ 
82 
val zero: term 

83 
val is_zero: term > bool 

84 
val mk_Suc: term > term 

85 
val dest_Suc: term > term 

21621  86 
val Suc_zero: term 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23745
diff
changeset

87 
val mk_nat: int > term 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23745
diff
changeset

88 
val dest_nat: term > int 
22994  89 
val class_size: string 
90 
val size_const: typ > term 

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

92 
val intT: typ 
7073  93 
val pls_const: term 
94 
val min_const: term 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26036
diff
changeset

95 
val bit0_const: term 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26036
diff
changeset

96 
val bit1_const: term 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26036
diff
changeset

97 
val mk_bit: int > term 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26036
diff
changeset

98 
val dest_bit: term > int 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23745
diff
changeset

99 
val mk_numeral: int > term 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23745
diff
changeset

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

101 
val number_of_const: typ > term 
23269  102 
val add_numerals: term > (term * typ) list > (term * typ) list 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23745
diff
changeset

103 
val mk_number: typ > int > term 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23745
diff
changeset

104 
val dest_number: term > typ * int 
21778
66440bf72cdc
binary numerals: restricted to actual abstract syntax;
wenzelm
parents:
21755
diff
changeset

105 
val realT: typ 
21755  106 
val nibbleT: typ 
107 
val mk_nibble: int > term 

108 
val dest_nibble: term > int 

109 
val charT: typ 

110 
val mk_char: int > term 

111 
val dest_char: term > int 

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

112 
val listT: typ > typ 
25887  113 
val nil_const: typ > term 
114 
val cons_const: typ > term 

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

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

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

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

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

119 
val dest_string: term > string 
923  120 
end; 
121 

122 
structure HOLogic: HOLOGIC = 

123 
struct 

124 

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

125 
(* HOL syntax *) 
923  126 

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

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

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

129 

923  130 

2510  131 
(* bool and set *) 
923  132 

8275  133 
val boolN = "bool"; 
134 
val boolT = Type (boolN, []); 

923  135 

9856  136 
val true_const = Const ("True", boolT); 
137 
val false_const = Const ("False", boolT); 

7073  138 

26804
e2b1e6868c2f
Adapted functions mk_setT and dest_setT to encoding of sets as predicates.
berghofe
parents:
26086
diff
changeset

139 
fun mk_setT T = T > boolT; 
923  140 

26804
e2b1e6868c2f
Adapted functions mk_setT and dest_setT to encoding of sets as predicates.
berghofe
parents:
26086
diff
changeset

141 
fun dest_setT (Type ("fun", [T, Type ("bool", [])])) = T 
3794  142 
 dest_setT T = raise TYPE ("dest_setT: set type expected", [T], []); 
923  143 

30450  144 
fun mk_set T ts = 
145 
let 

146 
val sT = mk_setT T; 

147 
val empty = Const ("Orderings.bot", sT); 

148 
fun insert t u = Const ("insert", T > sT > sT) $ t $ u; 

149 
in fold_rev insert ts empty end; 

150 

151 
fun mk_UNIV T = Const ("Set.UNIV", mk_setT T); 

152 

153 
fun dest_set (Const ("Orderings.bot", _)) = [] 

154 
 dest_set (Const ("insert", _) $ t $ u) = t :: dest_set u 

155 
 dest_set t = raise TERM ("dest_set", [t]); 

156 

157 
fun Collect_const T = Const ("Collect", (T > boolT) > mk_setT T); 

158 
fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T, t); 

159 

160 
fun mk_mem (x, A) = 

161 
let val setT = fastype_of A in 

162 
Const ("op :", dest_setT setT > setT > boolT) $ x $ A 

163 
end; 

164 

165 
fun dest_mem (Const ("op :", _) $ x $ A) = (x, A) 

166 
 dest_mem t = raise TERM ("dest_mem", [t]); 

167 

8275  168 

7073  169 
(* logic *) 
923  170 

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

172 

173 
fun mk_Trueprop P = Trueprop $ P; 

174 

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

3794  176 
 dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); 
923  177 

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

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

179 
let 
23576
1ffe739e5ee0
removed dest_cTrueprop (cf. ObjectLogic.dest_judgment);
wenzelm
parents:
23566
diff
changeset

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

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

182 
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

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

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

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

186 
let 
23576
1ffe739e5ee0
removed dest_cTrueprop (cf. ObjectLogic.dest_judgment);
wenzelm
parents:
23566
diff
changeset

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

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

189 
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

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

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

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

193 

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

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

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

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

197 

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

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

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

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

201 
and Not = @{term "Not"}; 
923  202 

7690  203 
fun mk_conj (t1, t2) = conj $ t1 $ t2 
204 
and mk_disj (t1, t2) = disj $ t1 $ t2 

16835  205 
and mk_imp (t1, t2) = imp $ t1 $ t2 
206 
and mk_not t = Not $ t; 

7690  207 

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

210 

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

213 

24958  214 
(*Like dest_disj, but flattens disjunctions however nested*) 
215 
fun disjuncts_aux (Const ("op ", _) $ t $ t') disjs = disjuncts_aux t (disjuncts_aux t' disjs) 

216 
 disjuncts_aux t disjs = t::disjs; 

217 

218 
fun disjuncts t = disjuncts_aux t []; 

219 

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

220 
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

221 
 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

222 

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

8302  225 

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

228 

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

231 

923  232 
fun all_const T = Const ("All", [T > boolT] > boolT); 
233 
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

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

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

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

238 

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

23247  241 
val class_eq = "HOL.eq"; 
21045  242 

923  243 

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

244 
(* binary operations and relations *) 
2510  245 

246 
fun mk_binop c (t, u) = 

247 
let val T = fastype_of t in 

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

249 
end; 

250 

251 
fun mk_binrel c (t, u) = 

252 
let val T = fastype_of t in 

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

254 
end; 

255 

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

256 
(*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

257 
way of handling polymorphic operators.*) 
2510  258 
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

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

2510  262 

263 

4571  264 
(* unit *) 
265 

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

11604  268 
fun is_unitT (Type ("Product_Type.unit", [])) = true 
9362  269 
 is_unitT _ = false; 
270 

11604  271 
val unit = Const ("Product_Type.Unity", unitT); 
4571  272 

11604  273 
fun is_unit (Const ("Product_Type.Unity", _)) = true 
4571  274 
 is_unit _ = false; 
275 

276 

277 
(* prod *) 

278 

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

280 

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

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

283 

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

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

14048  288 
pair_const T1 T2 $ t1 $ t2 
4571  289 
end; 
290 

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

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

293 

294 
fun mk_fst p = 

295 
let val pT = fastype_of p in 

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

297 
end; 

298 

299 
fun mk_snd p = 

300 
let val pT = fastype_of p in 

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

302 
end; 

303 

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

306 

307 
fun mk_split t = 

308 
(case Term.fastype_of t of 

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

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

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

312 

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

313 
(*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

314 
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

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

316 

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

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

15570  320 
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

321 
 mk_tuple T (t::_) = t; 
4571  322 

23745  323 
fun dest_tuple (Const ("Pair", _) $ t $ u) = dest_tuple t @ dest_tuple u 
324 
 dest_tuple t = [t]; 

325 

326 
(*In ap_split S T u, term u expects separate arguments for the factors of S, 

327 
with result type T. The call creates a new term expecting one argument 

328 
of type S.*) 

329 
fun ap_split T T3 u = 

330 
let 

331 
fun ap (T :: Ts) = 

332 
(case T of 

333 
Type ("*", [T1, T2]) => 

334 
split_const (T1, T2, Ts > T3) $ ap (T1 :: T2 :: Ts) 

335 
 _ => Abs ("x", T, ap Ts)) 

336 
 ap [] = 

337 
let val k = length (prodT_factors T) 

338 
in list_comb (incr_boundvars k u, map Bound (k  1 downto 0)) end 

339 
in ap [T] end; 

340 

341 

25172  342 
(* operations on tuples with specific arities *) 
343 
(* 

344 
an "arity" of a tuple is a list of lists of integers 

345 
("factors"), denoting paths to subterms that are pairs 

346 
*) 

23745  347 

348 
fun prod_err s = raise TERM (s ^ ": inconsistent use of products", []); 

349 

350 
fun prod_factors t = 

351 
let 

352 
fun factors p (Const ("Pair", _) $ t $ u) = 

353 
p :: factors (1::p) t @ factors (2::p) u 

354 
 factors p _ = [] 

355 
in factors [] t end; 

356 

357 
fun dest_tuple' ps = 

358 
let 

359 
fun dest p t = if p mem ps then (case t of 

360 
Const ("Pair", _) $ t $ u => 

361 
dest (1::p) t @ dest (2::p) u 

362 
 _ => prod_err "dest_tuple'") else [t] 

363 
in dest [] end; 

364 

365 
fun prodT_factors' ps = 

366 
let 

367 
fun factors p T = if p mem ps then (case T of 

368 
Type ("*", [T1, T2]) => 

369 
factors (1::p) T1 @ factors (2::p) T2 

370 
 _ => prod_err "prodT_factors'") else [T] 

371 
in factors [] end; 

372 

373 
(*In ap_split' ps S T u, term u expects separate arguments for the factors of S, 

374 
with result type T. The call creates a new term expecting one argument 

375 
of type S.*) 

376 
fun ap_split' ps T T3 u = 

377 
let 

378 
fun ap ((p, T) :: pTs) = 

379 
if p mem ps then (case T of 

380 
Type ("*", [T1, T2]) => 

381 
split_const (T1, T2, map snd pTs > T3) $ 

382 
ap ((1::p, T1) :: (2::p, T2) :: pTs) 

383 
 _ => prod_err "ap_split'") 

384 
else Abs ("x", T, ap pTs) 

385 
 ap [] = 

386 
let val k = length ps 

387 
in list_comb (incr_boundvars (k + 1) u, map Bound (k downto 0)) end 

388 
in ap [([], T)] end; 

389 

390 
fun mk_tuple' ps = 

391 
let 

392 
fun mk p T ts = 

393 
if p mem ps then (case T of 

394 
Type ("*", [T1, T2]) => 

395 
let 

396 
val (t, ts') = mk (1::p) T1 ts; 

397 
val (u, ts'') = mk (2::p) T2 ts' 

398 
in (pair_const T1 T2 $ t $ u, ts'') end 

399 
 _ => prod_err "mk_tuple'") 

400 
else (hd ts, tl ts) 

401 
in fst oo mk [] end; 

402 

403 
fun mk_tupleT ps = 

404 
let 

405 
fun mk p Ts = 

406 
if p mem ps then 

407 
let 

408 
val (T, Ts') = mk (1::p) Ts; 

409 
val (U, Ts'') = mk (2::p) Ts' 

410 
in (mk_prodT (T, U), Ts'') end 

411 
else (hd Ts, tl Ts) 

412 
in fst o mk [] end; 

413 

414 
fun strip_split t = 

415 
let 

416 
fun strip [] qs Ts t = (t, Ts, qs) 

417 
 strip (p :: ps) qs Ts (Const ("split", _) $ t) = 

418 
strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) Ts t 

419 
 strip (p :: ps) qs Ts (Abs (s, T, t)) = strip ps qs (T :: Ts) t 

420 
 strip (p :: ps) qs Ts t = strip ps qs 

421 
(hd (binder_types (fastype_of1 (Ts, t))) :: Ts) 

422 
(incr_boundvars 1 t $ Bound 0) 

423 
in strip [[]] [] [] t end; 

424 

5207  425 

426 
(* nat *) 

427 

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

429 

22994  430 
val zero = Const ("HOL.zero_class.zero", natT); 
5207  431 

22994  432 
fun is_zero (Const ("HOL.zero_class.zero", _)) = true 
5207  433 
 is_zero _ = false; 
434 

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

436 

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

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

439 

21621  440 
val Suc_zero = mk_Suc zero; 
441 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23745
diff
changeset

442 
fun mk_nat n = 
22994  443 
let 
444 
fun mk 0 = zero 

23297  445 
 mk n = mk_Suc (mk (n  1)); 
23576
1ffe739e5ee0
removed dest_cTrueprop (cf. ObjectLogic.dest_judgment);
wenzelm
parents:
23566
diff
changeset

446 
in if n < 0 then raise TERM ("mk_nat: negative number", []) else mk n end; 
5207  447 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23745
diff
changeset

448 
fun dest_nat (Const ("HOL.zero_class.zero", _)) = 0 
23297  449 
 dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1 
5207  450 
 dest_nat t = raise TERM ("dest_nat", [t]); 
451 

22994  452 
val class_size = "Nat.size"; 
453 

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

455 

5207  456 

26036  457 
(* index *) 
458 

459 
val indexT = Type ("Code_Index.index", []); 

460 

461 

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

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

463 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25887
diff
changeset

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

465 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25887
diff
changeset

466 
val pls_const = Const ("Int.Pls", intT) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25887
diff
changeset

467 
and min_const = Const ("Int.Min", intT) 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26036
diff
changeset

468 
and bit0_const = Const ("Int.Bit0", intT > intT) 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26036
diff
changeset

469 
and bit1_const = Const ("Int.Bit1", intT > intT); 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26036
diff
changeset

470 

3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26036
diff
changeset

471 
fun mk_bit 0 = bit0_const 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26036
diff
changeset

472 
 mk_bit 1 = bit1_const 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26036
diff
changeset

473 
 mk_bit _ = raise TERM ("mk_bit", []); 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26036
diff
changeset

474 

3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26036
diff
changeset

475 
fun dest_bit (Const ("Int.Bit0", _)) = 0 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26036
diff
changeset

476 
 dest_bit (Const ("Int.Bit1", _)) = 1 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26036
diff
changeset

477 
 dest_bit t = raise TERM ("dest_bit", [t]); 
8768  478 

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

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

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

481 
 mk_numeral i = 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23745
diff
changeset

482 
let val (q, r) = Integer.div_mod i 2; 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26036
diff
changeset

483 
in mk_bit r $ mk_numeral q end; 
13755  484 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25887
diff
changeset

485 
fun dest_numeral (Const ("Int.Pls", _)) = 0 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25887
diff
changeset

486 
 dest_numeral (Const ("Int.Min", _)) = ~1 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26036
diff
changeset

487 
 dest_numeral (Const ("Int.Bit0", _) $ bs) = 2 * dest_numeral bs 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26036
diff
changeset

488 
 dest_numeral (Const ("Int.Bit1", _) $ bs) = 2 * dest_numeral bs + 1 
21829
016eff9c5699
simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
wenzelm
parents:
21820
diff
changeset

489 
 dest_numeral t = raise TERM ("dest_numeral", [t]); 
13755  490 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25887
diff
changeset

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

492 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25887
diff
changeset

493 
fun add_numerals (Const ("Int.number_class.number_of", Type (_, [_, T])) $ t) = cons (t, T) 
23269  494 
 add_numerals (t $ u) = add_numerals t #> add_numerals u 
495 
 add_numerals (Abs (_, _, t)) = add_numerals t 

496 
 add_numerals _ = I; 

22391  497 

22994  498 
fun mk_number T 0 = Const ("HOL.zero_class.zero", T) 
499 
 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

500 
 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

501 

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

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25887
diff
changeset

504 
 dest_number (Const ("Int.number_class.number_of", Type ("fun", [_, T])) $ t) = 
22994  505 
(T, dest_numeral t) 
21820
2f2b6a965ccc
introduced mk/dest_numeral/number for mk/dest_binum etc.
haftmann
parents:
21788
diff
changeset

506 
 dest_number t = raise TERM ("dest_number", [t]); 
13755  507 

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

508 

13755  509 
(* real *) 
510 

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

513 

21755  514 
(* nibble *) 
515 

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

13755  517 

21755  518 
fun mk_nibble n = 
519 
let val s = 

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

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

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

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

17083  524 

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

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

528 
NONE => err () 

529 
 SOME c => 

530 
if size c <> 1 then err () 

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

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

533 
else err ()) 

534 
end; 

15062  535 

21455  536 

537 
(* char *) 

538 

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

540 

21755  541 
fun mk_char n = 
542 
if 0 <= n andalso n <= 255 then 

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

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

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

21455  546 

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

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

21455  550 

21755  551 

552 
(* list *) 

21455  553 

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

25887  556 
fun nil_const T = Const ("List.list.Nil", listT T); 
557 

558 
fun cons_const T = 

559 
let val lT = listT T 

560 
in Const ("List.list.Cons", T > lT > lT) end; 

561 

21755  562 
fun mk_list T ts = 
21455  563 
let 
21755  564 
val lT = listT T; 
565 
val Nil = Const ("List.list.Nil", lT); 

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

567 
in fold_rev Cons ts Nil end; 

568 

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

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

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

21455  572 

573 

574 
(* string *) 

575 

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

576 
val stringT = Type ("List.string", []); 
21455  577 

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

21455  580 

923  581 
end; 