author | haftmann |
Mon, 26 Jan 2009 22:14:17 +0100 | |
changeset 29629 | 5111ce425e7a |
parent 29025 | 8c8859c0d734 |
child 29997 | f6756c097c2d |
child 30240 | 5b25fee0362c |
permissions | -rw-r--r-- |
29629 | 1 |
(* Title: HOL/Library/Numeral_Type.thy |
2 |
Author: Brian Huffman |
|
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
3 |
*) |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
4 |
|
29629 | 5 |
header {* Numeral Syntax for Types *} |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
6 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
7 |
theory Numeral_Type |
27487 | 8 |
imports Plain "~~/src/HOL/Presburger" |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
9 |
begin |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
10 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
11 |
subsection {* Preliminary lemmas *} |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
12 |
(* These should be moved elsewhere *) |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
13 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
14 |
lemma (in type_definition) univ: |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
15 |
"UNIV = Abs ` A" |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
16 |
proof |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
17 |
show "Abs ` A \<subseteq> UNIV" by (rule subset_UNIV) |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
18 |
show "UNIV \<subseteq> Abs ` A" |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
19 |
proof |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
20 |
fix x :: 'b |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
21 |
have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric]) |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
22 |
moreover have "Rep x \<in> A" by (rule Rep) |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
23 |
ultimately show "x \<in> Abs ` A" by (rule image_eqI) |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
24 |
qed |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
25 |
qed |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
26 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
27 |
lemma (in type_definition) card: "card (UNIV :: 'b set) = card A" |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
28 |
by (simp add: univ card_image inj_on_def Abs_inject) |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
29 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
30 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
31 |
subsection {* Cardinalities of types *} |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
32 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
33 |
syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))") |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
34 |
|
28920 | 35 |
translations "CARD(t)" => "CONST card (CONST UNIV \<Colon> t set)" |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
36 |
|
24407 | 37 |
typed_print_translation {* |
38 |
let |
|
28920 | 39 |
fun card_univ_tr' show_sorts _ [Const (@{const_name UNIV}, Type(_,[T,_]))] = |
24407 | 40 |
Syntax.const "_type_card" $ Syntax.term_of_typ show_sorts T; |
28920 | 41 |
in [(@{const_syntax card}, card_univ_tr')] |
24407 | 42 |
end |
43 |
*} |
|
44 |
||
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
45 |
lemma card_unit: "CARD(unit) = 1" |
26153 | 46 |
unfolding UNIV_unit by simp |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
47 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
48 |
lemma card_bool: "CARD(bool) = 2" |
26153 | 49 |
unfolding UNIV_bool by simp |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
50 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
51 |
lemma card_prod: "CARD('a::finite \<times> 'b::finite) = CARD('a) * CARD('b)" |
26153 | 52 |
unfolding UNIV_Times_UNIV [symmetric] by (simp only: card_cartesian_product) |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
53 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
54 |
lemma card_sum: "CARD('a::finite + 'b::finite) = CARD('a) + CARD('b)" |
26153 | 55 |
unfolding UNIV_Plus_UNIV [symmetric] by (simp only: finite card_Plus) |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
56 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
57 |
lemma card_option: "CARD('a::finite option) = Suc CARD('a)" |
26153 | 58 |
unfolding insert_None_conv_UNIV [symmetric] |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
59 |
apply (subgoal_tac "(None::'a option) \<notin> range Some") |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
60 |
apply (simp add: finite card_image) |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
61 |
apply fast |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
62 |
done |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
63 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
64 |
lemma card_set: "CARD('a::finite set) = 2 ^ CARD('a)" |
26153 | 65 |
unfolding Pow_UNIV [symmetric] |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
66 |
by (simp only: card_Pow finite numeral_2_eq_2) |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
67 |
|
25378 | 68 |
|
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
69 |
subsection {* Numeral Types *} |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
70 |
|
24406 | 71 |
typedef (open) num0 = "UNIV :: nat set" .. |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
72 |
typedef (open) num1 = "UNIV :: unit set" .. |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
73 |
typedef (open) 'a bit0 = "UNIV :: (bool * 'a) set" .. |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
74 |
typedef (open) 'a bit1 = "UNIV :: (bool * 'a) option set" .. |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
75 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
76 |
instance num1 :: finite |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
77 |
proof |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
78 |
show "finite (UNIV::num1 set)" |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
79 |
unfolding type_definition.univ [OF type_definition_num1] |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
80 |
using finite by (rule finite_imageI) |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
81 |
qed |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
82 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
83 |
instance bit0 :: (finite) finite |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
84 |
proof |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
85 |
show "finite (UNIV::'a bit0 set)" |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
86 |
unfolding type_definition.univ [OF type_definition_bit0] |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
87 |
using finite by (rule finite_imageI) |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
88 |
qed |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
89 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
90 |
instance bit1 :: (finite) finite |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
91 |
proof |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
92 |
show "finite (UNIV::'a bit1 set)" |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
93 |
unfolding type_definition.univ [OF type_definition_bit1] |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
94 |
using finite by (rule finite_imageI) |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
95 |
qed |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
96 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
97 |
lemma card_num1: "CARD(num1) = 1" |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
98 |
unfolding type_definition.card [OF type_definition_num1] |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
99 |
by (simp only: card_unit) |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
100 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
101 |
lemma card_bit0: "CARD('a::finite bit0) = 2 * CARD('a)" |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
102 |
unfolding type_definition.card [OF type_definition_bit0] |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
103 |
by (simp only: card_prod card_bool) |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
104 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
105 |
lemma card_bit1: "CARD('a::finite bit1) = Suc (2 * CARD('a))" |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
106 |
unfolding type_definition.card [OF type_definition_bit1] |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
107 |
by (simp only: card_prod card_option card_bool) |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
108 |
|
24406 | 109 |
lemma card_num0: "CARD (num0) = 0" |
26506
c4202c67fe3e
No longer imports InfiniteSet, ATP_Linkup is sufficient.
chaieb
parents:
26153
diff
changeset
|
110 |
by (simp add: infinite_UNIV_nat card_eq_0_iff type_definition.card [OF type_definition_num0]) |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
111 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
112 |
lemmas card_univ_simps [simp] = |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
113 |
card_unit |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
114 |
card_bool |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
115 |
card_prod |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
116 |
card_sum |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
117 |
card_option |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
118 |
card_set |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
119 |
card_num1 |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
120 |
card_bit0 |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
121 |
card_bit1 |
24406 | 122 |
card_num0 |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
123 |
|
25378 | 124 |
|
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
125 |
subsection {* Syntax *} |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
126 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
127 |
syntax |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
128 |
"_NumeralType" :: "num_const => type" ("_") |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
129 |
"_NumeralType0" :: type ("0") |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
130 |
"_NumeralType1" :: type ("1") |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
131 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
132 |
translations |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
133 |
"_NumeralType1" == (type) "num1" |
24406 | 134 |
"_NumeralType0" == (type) "num0" |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
135 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
136 |
parse_translation {* |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
137 |
let |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
138 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
139 |
val num1_const = Syntax.const "Numeral_Type.num1"; |
24406 | 140 |
val num0_const = Syntax.const "Numeral_Type.num0"; |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
141 |
val B0_const = Syntax.const "Numeral_Type.bit0"; |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
142 |
val B1_const = Syntax.const "Numeral_Type.bit1"; |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
143 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
144 |
fun mk_bintype n = |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
145 |
let |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
146 |
fun mk_bit n = if n = 0 then B0_const else B1_const; |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
147 |
fun bin_of n = |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
148 |
if n = 1 then num1_const |
24406 | 149 |
else if n = 0 then num0_const |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
150 |
else if n = ~1 then raise TERM ("negative type numeral", []) |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
151 |
else |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24407
diff
changeset
|
152 |
let val (q, r) = Integer.div_mod n 2; |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
153 |
in mk_bit r $ bin_of q end; |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
154 |
in bin_of n end; |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
155 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
156 |
fun numeral_tr (*"_NumeralType"*) [Const (str, _)] = |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24407
diff
changeset
|
157 |
mk_bintype (valOf (Int.fromString str)) |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
158 |
| numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts); |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
159 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
160 |
in [("_NumeralType", numeral_tr)] end; |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
161 |
*} |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
162 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
163 |
print_translation {* |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
164 |
let |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
165 |
fun int_of [] = 0 |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24407
diff
changeset
|
166 |
| int_of (b :: bs) = b + 2 * int_of bs; |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
167 |
|
24406 | 168 |
fun bin_of (Const ("num0", _)) = [] |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
169 |
| bin_of (Const ("num1", _)) = [1] |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
170 |
| bin_of (Const ("bit0", _) $ bs) = 0 :: bin_of bs |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
171 |
| bin_of (Const ("bit1", _) $ bs) = 1 :: bin_of bs |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
172 |
| bin_of t = raise TERM("bin_of", [t]); |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
173 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
174 |
fun bit_tr' b [t] = |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
175 |
let |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
176 |
val rev_digs = b :: bin_of t handle TERM _ => raise Match |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
177 |
val i = int_of rev_digs; |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24407
diff
changeset
|
178 |
val num = string_of_int (abs i); |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
179 |
in |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
180 |
Syntax.const "_NumeralType" $ Syntax.free num |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
181 |
end |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
182 |
| bit_tr' b _ = raise Match; |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
183 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
184 |
in [("bit0", bit_tr' 0), ("bit1", bit_tr' 1)] end; |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
185 |
*} |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
186 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
187 |
|
25378 | 188 |
subsection {* Classes with at least 1 and 2 *} |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
189 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
190 |
text {* Class finite already captures "at least 1" *} |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
191 |
|
24407 | 192 |
lemma zero_less_card_finite [simp]: |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
193 |
"0 < CARD('a::finite)" |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
194 |
proof (cases "CARD('a::finite) = 0") |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
195 |
case False thus ?thesis by (simp del: card_0_eq) |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
196 |
next |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
197 |
case True |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
198 |
thus ?thesis by (simp add: finite) |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
199 |
qed |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
200 |
|
24407 | 201 |
lemma one_le_card_finite [simp]: |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
202 |
"Suc 0 <= CARD('a::finite)" |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
203 |
by (simp add: less_Suc_eq_le [symmetric] zero_less_card_finite) |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
204 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
205 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
206 |
text {* Class for cardinality "at least 2" *} |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
207 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
208 |
class card2 = finite + |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
209 |
assumes two_le_card: "2 <= CARD('a)" |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
210 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
211 |
lemma one_less_card: "Suc 0 < CARD('a::card2)" |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
212 |
using two_le_card [where 'a='a] by simp |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
213 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
214 |
instance bit0 :: (finite) card2 |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
215 |
by intro_classes (simp add: one_le_card_finite) |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
216 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
217 |
instance bit1 :: (finite) card2 |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
218 |
by intro_classes (simp add: one_le_card_finite) |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
219 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
220 |
subsection {* Examples *} |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
221 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
222 |
lemma "CARD(0) = 0" by simp |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
223 |
lemma "CARD(17) = 17" by simp |
28920 | 224 |
|
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
225 |
end |