author  haftmann 
Mon, 21 Jan 2008 08:43:32 +0100  
changeset 25932  db0fd0ecdcd4 
parent 25919  8b1c0d434824 
child 25967  dd602eb20f3f 
permissions  rwrr 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
24630
diff
changeset

1 
(* Title: HOL/Tools/Int.ML 
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

3 
Author: Makarius 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

4 

543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

5 
Logical operations on numerals (see also HOL/hologic.ML). 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

6 
*) 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

7 

543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

8 
signature NUMERAL = 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

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

10 
val mk_cnumeral: int > cterm 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23575
diff
changeset

11 
val mk_cnumber: ctyp > int > cterm 
25932  12 
val add_code: string > bool > bool > string > theory > theory 
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

13 
end; 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

14 

543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

15 
structure Numeral: NUMERAL = 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

16 
struct 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

17 

543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

18 
(* numeral *) 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

19 

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

20 
fun mk_cbit 0 = @{cterm "Int.bit.B0"} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
24630
diff
changeset

21 
 mk_cbit 1 = @{cterm "Int.bit.B1"} 
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

22 
 mk_cbit _ = raise CTERM ("mk_cbit", []); 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

23 

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

24 
fun mk_cnumeral 0 = @{cterm "Int.Pls"} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
24630
diff
changeset

25 
 mk_cnumeral ~1 = @{cterm "Int.Min"} 
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

26 
 mk_cnumeral i = 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23575
diff
changeset

27 
let val (q, r) = Integer.div_mod i 2 in 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
24630
diff
changeset

28 
Thm.capply (Thm.capply @{cterm "Int.Bit"} (mk_cnumeral q)) (mk_cbit r) 
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

29 
end; 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

30 

543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

31 

543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

32 
(* number *) 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

33 

543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

34 
local 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

35 

543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

36 
val zero = @{cpat "0"}; 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

37 
val zeroT = Thm.ctyp_of_term zero; 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

38 

543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

39 
val one = @{cpat "1"}; 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

40 
val oneT = Thm.ctyp_of_term one; 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

41 

543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

42 
val number_of = @{cpat "number_of"}; 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

43 
val numberT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term number_of))); 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

44 

543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

45 
fun instT T V = Thm.instantiate_cterm ([(V, T)], []); 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

46 

543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

47 
in 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

48 

543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

49 
fun mk_cnumber T 0 = instT T zeroT zero 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

50 
 mk_cnumber T 1 = instT T oneT one 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

51 
 mk_cnumber T i = Thm.capply (instT T numberT number_of) (mk_cnumeral i); 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

52 

543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

53 
end; 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

54 

25932  55 

56 
(* code generator *) 

57 

58 
fun add_code number_of negative unbounded target = 

59 
CodeTarget.add_pretty_numeral target unbounded negative number_of 

60 
@{const_name Int.B0} @{const_name Int.B1} 

61 
@{const_name Int.Pls} @{const_name Int.Min} 

62 
@{const_name Int.Bit}; 

63 

23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

64 
end; 