76 val bitT: typ |
76 val bitT: typ |
77 val B0_const: term |
77 val B0_const: term |
78 val B1_const: term |
78 val B1_const: term |
79 val mk_bit: int -> term |
79 val mk_bit: int -> term |
80 val dest_bit: term -> int |
80 val dest_bit: term -> int |
81 val intT: typ |
|
82 val pls_const: term |
81 val pls_const: term |
83 val min_const: term |
82 val min_const: term |
84 val bit_const: term |
83 val bit_const: term |
85 val number_of_const: typ -> term |
84 val number_of_const: typ -> term |
86 val mk_binum: IntInf.int -> term |
85 val mk_numeral: IntInf.int -> term |
87 val dest_binum: term -> IntInf.int |
86 val dest_numeral: term -> IntInf.int |
88 val mk_int: IntInf.int -> term |
87 val mk_number: typ -> IntInf.int -> term |
|
88 val dest_number: term -> typ * IntInf.int |
|
89 val intT: typ |
89 val realT: typ |
90 val realT: typ |
|
91 val listT: typ -> typ |
|
92 val mk_list: typ -> term list -> term |
|
93 val dest_list: term -> term list |
90 val nibbleT: typ |
94 val nibbleT: typ |
91 val mk_nibble: int -> term |
95 val mk_nibble: int -> term |
92 val dest_nibble: term -> int |
96 val dest_nibble: term -> int |
93 val charT: typ |
97 val charT: typ |
94 val mk_char: int -> term |
98 val mk_char: int -> term |
95 val dest_char: term -> int |
99 val dest_char: term -> int |
96 val listT : typ -> typ |
|
97 val mk_list: typ -> term list -> term |
|
98 val dest_list: term -> term list |
|
99 val stringT: typ |
100 val stringT: typ |
100 val mk_string : string -> term |
101 val mk_string: string -> term |
101 val dest_string : term -> string |
102 val dest_string: term -> string |
102 end; |
103 end; |
103 |
104 |
104 structure HOLogic: HOLOGIC = |
105 structure HOLogic: HOLOGIC = |
105 struct |
106 struct |
106 |
107 |
321 |
322 |
322 val pls_const = Const ("Numeral.Pls", intT) |
323 val pls_const = Const ("Numeral.Pls", intT) |
323 and min_const = Const ("Numeral.Min", intT) |
324 and min_const = Const ("Numeral.Min", intT) |
324 and bit_const = Const ("Numeral.Bit", [intT, bitT] ---> intT); |
325 and bit_const = Const ("Numeral.Bit", [intT, bitT] ---> intT); |
325 |
326 |
326 fun mk_binum 0 = pls_const |
|
327 | mk_binum ~1 = min_const |
|
328 | mk_binum i = |
|
329 let val (q, r) = IntInf.divMod (i, 2) |
|
330 in bit_const $ mk_binum q $ mk_bit (IntInf.toInt r) end; |
|
331 |
|
332 fun dest_binum (Const ("Numeral.Pls", _)) = 0 |
|
333 | dest_binum (Const ("Numeral.Min", _)) = ~1 |
|
334 | dest_binum (Const ("Numeral.Bit", _) $ bs $ b) = |
|
335 2 * dest_binum bs + IntInf.fromInt (dest_bit b) |
|
336 | dest_binum t = raise TERM ("dest_binum", [t]); |
|
337 |
|
338 fun number_of_const T = Const ("Numeral.number_of", intT --> T); |
327 fun number_of_const T = Const ("Numeral.number_of", intT --> T); |
339 |
328 |
340 fun mk_int 0 = Const ("HOL.zero", intT) |
329 val mk_numeral = |
341 | mk_int 1 = Const ("HOL.one", intT) |
330 let |
342 | mk_int i = number_of_const intT $ mk_binum i; |
331 fun mk_bit n = if n = 0 then B0_const else B1_const; |
343 |
332 fun bin_of n = |
|
333 if n = 0 then pls_const |
|
334 else if n = ~1 then min_const |
|
335 else |
|
336 let |
|
337 val (q, r) = IntInf.divMod (n, 2); |
|
338 in bit_const $ bin_of q $ mk_bit r end; |
|
339 in bin_of end; |
|
340 |
|
341 fun dest_numeral (Const ("Numeral.Pls", _)) = IntInf.fromInt 0 |
|
342 | dest_numeral (Const ("Numeral.Min", _)) = IntInf.fromInt ~1 |
|
343 | dest_numeral (Const ("Numeral.Bit", _) $ bs $ b) = |
|
344 IntInf.fromInt (dest_bit b) + (2 * dest_numeral bs) |
|
345 | dest_numeral t = raise TERM ("dest_numeral", [t]); |
|
346 |
|
347 fun mk_number T 0 = Const ("HOL.zero", T) |
|
348 | mk_number T 1 = Const ("HOL.one", T) |
|
349 | mk_number T i = number_of_const T $ mk_numeral i; |
|
350 |
|
351 fun dest_number (Const ("HOL.zero", T)) = (T, 0) |
|
352 | dest_number (Const ("HOL.one", T)) = (T, 1) |
|
353 | dest_number (Const ("Numeral.number_of", Type ("fun", [_, T])) $ t) = (T, dest_numeral t) |
|
354 | dest_number t = raise TERM ("dest_number", [t]); |
344 |
355 |
345 (* real *) |
356 (* real *) |
346 |
357 |
347 val realT = Type ("RealDef.real", []); |
358 val realT = Type ("RealDef.real", []); |
348 |
359 |