|
1 (* |
|
2 ID: $Id$ |
|
3 Author: Brian Huffman |
|
4 |
|
5 Numeral Syntax for Types |
|
6 *) |
|
7 |
|
8 header "Numeral Syntax for Types" |
|
9 |
|
10 theory Numeral_Type |
|
11 imports Infinite_Set |
|
12 begin |
|
13 |
|
14 subsection {* Preliminary lemmas *} |
|
15 (* These should be moved elsewhere *) |
|
16 |
|
17 lemma inj_Inl [simp]: "inj_on Inl A" |
|
18 by (rule inj_onI, simp) |
|
19 |
|
20 lemma inj_Inr [simp]: "inj_on Inr A" |
|
21 by (rule inj_onI, simp) |
|
22 |
|
23 lemma inj_Some [simp]: "inj_on Some A" |
|
24 by (rule inj_onI, simp) |
|
25 |
|
26 lemma card_Plus: |
|
27 "[| finite A; finite B |] ==> card (A <+> B) = card A + card B" |
|
28 unfolding Plus_def |
|
29 apply (subgoal_tac "Inl ` A \<inter> Inr ` B = {}") |
|
30 apply (simp add: card_Un_disjoint card_image) |
|
31 apply fast |
|
32 done |
|
33 |
|
34 lemma (in type_definition) univ: |
|
35 "UNIV = Abs ` A" |
|
36 proof |
|
37 show "Abs ` A \<subseteq> UNIV" by (rule subset_UNIV) |
|
38 show "UNIV \<subseteq> Abs ` A" |
|
39 proof |
|
40 fix x :: 'b |
|
41 have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric]) |
|
42 moreover have "Rep x \<in> A" by (rule Rep) |
|
43 ultimately show "x \<in> Abs ` A" by (rule image_eqI) |
|
44 qed |
|
45 qed |
|
46 |
|
47 lemma (in type_definition) card: "card (UNIV :: 'b set) = card A" |
|
48 by (simp add: univ card_image inj_on_def Abs_inject) |
|
49 |
|
50 |
|
51 subsection {* Cardinalities of types *} |
|
52 |
|
53 syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))") |
|
54 |
|
55 translations "CARD(t)" => "card (UNIV::t set)" |
|
56 |
|
57 lemma card_unit: "CARD(unit) = 1" |
|
58 unfolding univ_unit by simp |
|
59 |
|
60 lemma card_bool: "CARD(bool) = 2" |
|
61 unfolding univ_bool by simp |
|
62 |
|
63 lemma card_prod: "CARD('a::finite \<times> 'b::finite) = CARD('a) * CARD('b)" |
|
64 unfolding univ_prod by (simp only: card_cartesian_product) |
|
65 |
|
66 lemma card_sum: "CARD('a::finite + 'b::finite) = CARD('a) + CARD('b)" |
|
67 unfolding univ_sum by (simp only: finite card_Plus) |
|
68 |
|
69 lemma card_option: "CARD('a::finite option) = Suc CARD('a)" |
|
70 unfolding univ_option |
|
71 apply (subgoal_tac "(None::'a option) \<notin> range Some") |
|
72 apply (simp add: finite card_image) |
|
73 apply fast |
|
74 done |
|
75 |
|
76 lemma card_set: "CARD('a::finite set) = 2 ^ CARD('a)" |
|
77 unfolding univ_set |
|
78 by (simp only: card_Pow finite numeral_2_eq_2) |
|
79 |
|
80 subsection {* Numeral Types *} |
|
81 |
|
82 typedef (open) pls = "UNIV :: nat set" .. |
|
83 typedef (open) num1 = "UNIV :: unit set" .. |
|
84 typedef (open) 'a bit0 = "UNIV :: (bool * 'a) set" .. |
|
85 typedef (open) 'a bit1 = "UNIV :: (bool * 'a) option set" .. |
|
86 |
|
87 instance num1 :: finite |
|
88 proof |
|
89 show "finite (UNIV::num1 set)" |
|
90 unfolding type_definition.univ [OF type_definition_num1] |
|
91 using finite by (rule finite_imageI) |
|
92 qed |
|
93 |
|
94 instance bit0 :: (finite) finite |
|
95 proof |
|
96 show "finite (UNIV::'a bit0 set)" |
|
97 unfolding type_definition.univ [OF type_definition_bit0] |
|
98 using finite by (rule finite_imageI) |
|
99 qed |
|
100 |
|
101 instance bit1 :: (finite) finite |
|
102 proof |
|
103 show "finite (UNIV::'a bit1 set)" |
|
104 unfolding type_definition.univ [OF type_definition_bit1] |
|
105 using finite by (rule finite_imageI) |
|
106 qed |
|
107 |
|
108 lemma card_num1: "CARD(num1) = 1" |
|
109 unfolding type_definition.card [OF type_definition_num1] |
|
110 by (simp only: card_unit) |
|
111 |
|
112 lemma card_bit0: "CARD('a::finite bit0) = 2 * CARD('a)" |
|
113 unfolding type_definition.card [OF type_definition_bit0] |
|
114 by (simp only: card_prod card_bool) |
|
115 |
|
116 lemma card_bit1: "CARD('a::finite bit1) = Suc (2 * CARD('a))" |
|
117 unfolding type_definition.card [OF type_definition_bit1] |
|
118 by (simp only: card_prod card_option card_bool) |
|
119 |
|
120 lemma card_pls: "CARD (pls) = 0" |
|
121 by (simp add: type_definition.card [OF type_definition_pls]) |
|
122 |
|
123 lemmas card_univ_simps [simp] = |
|
124 card_unit |
|
125 card_bool |
|
126 card_prod |
|
127 card_sum |
|
128 card_option |
|
129 card_set |
|
130 card_num1 |
|
131 card_bit0 |
|
132 card_bit1 |
|
133 card_pls |
|
134 |
|
135 subsection {* Syntax *} |
|
136 |
|
137 |
|
138 syntax |
|
139 "_NumeralType" :: "num_const => type" ("_") |
|
140 "_NumeralType0" :: type ("0") |
|
141 "_NumeralType1" :: type ("1") |
|
142 |
|
143 translations |
|
144 "_NumeralType1" == (type) "num1" |
|
145 "_NumeralType0" == (type) "pls" |
|
146 |
|
147 parse_translation {* |
|
148 let |
|
149 |
|
150 val num1_const = Syntax.const "Numeral_Type.num1"; |
|
151 val pls_const = Syntax.const "Numeral_Type.pls"; |
|
152 val B0_const = Syntax.const "Numeral_Type.bit0"; |
|
153 val B1_const = Syntax.const "Numeral_Type.bit1"; |
|
154 |
|
155 fun mk_bintype n = |
|
156 let |
|
157 fun mk_bit n = if n = 0 then B0_const else B1_const; |
|
158 fun bin_of n = |
|
159 if n = 1 then num1_const |
|
160 else if n = 0 then pls_const |
|
161 else if n = ~1 then raise TERM ("negative type numeral", []) |
|
162 else |
|
163 let val (q, r) = IntInf.divMod (n, 2); |
|
164 in mk_bit r $ bin_of q end; |
|
165 in bin_of n end; |
|
166 |
|
167 fun numeral_tr (*"_NumeralType"*) [Const (str, _)] = |
|
168 mk_bintype (valOf (IntInf.fromString str)) |
|
169 | numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts); |
|
170 |
|
171 in [("_NumeralType", numeral_tr)] end; |
|
172 *} |
|
173 |
|
174 print_translation {* |
|
175 let |
|
176 fun int_of [] = 0 |
|
177 | int_of (b :: bs) = IntInf.fromInt b + (2 * int_of bs); |
|
178 |
|
179 fun bin_of (Const ("pls", _)) = [] |
|
180 | bin_of (Const ("num1", _)) = [1] |
|
181 | bin_of (Const ("bit0", _) $ bs) = 0 :: bin_of bs |
|
182 | bin_of (Const ("bit1", _) $ bs) = 1 :: bin_of bs |
|
183 | bin_of t = raise TERM("bin_of", [t]); |
|
184 |
|
185 fun bit_tr' b [t] = |
|
186 let |
|
187 val rev_digs = b :: bin_of t handle TERM _ => raise Match |
|
188 val i = int_of rev_digs; |
|
189 val num = IntInf.toString (IntInf.abs i); |
|
190 in |
|
191 Syntax.const "_NumeralType" $ Syntax.free num |
|
192 end |
|
193 | bit_tr' b _ = raise Match; |
|
194 |
|
195 in [("bit0", bit_tr' 0), ("bit1", bit_tr' 1)] end; |
|
196 *} |
|
197 |
|
198 |
|
199 subsection {* Classes with at values least 1 and 2 *} |
|
200 |
|
201 text {* Class finite already captures "at least 1" *} |
|
202 |
|
203 lemma zero_less_card_finite: |
|
204 "0 < CARD('a::finite)" |
|
205 proof (cases "CARD('a::finite) = 0") |
|
206 case False thus ?thesis by (simp del: card_0_eq) |
|
207 next |
|
208 case True |
|
209 thus ?thesis by (simp add: finite) |
|
210 qed |
|
211 |
|
212 lemma one_le_card_finite: |
|
213 "Suc 0 <= CARD('a::finite)" |
|
214 by (simp add: less_Suc_eq_le [symmetric] zero_less_card_finite) |
|
215 |
|
216 |
|
217 text {* Class for cardinality "at least 2" *} |
|
218 |
|
219 class card2 = finite + |
|
220 assumes two_le_card: "2 <= CARD('a)" |
|
221 |
|
222 lemma one_less_card: "Suc 0 < CARD('a::card2)" |
|
223 using two_le_card [where 'a='a] by simp |
|
224 |
|
225 instance bit0 :: (finite) card2 |
|
226 by intro_classes (simp add: one_le_card_finite) |
|
227 |
|
228 instance bit1 :: (finite) card2 |
|
229 by intro_classes (simp add: one_le_card_finite) |
|
230 |
|
231 subsection {* Examples *} |
|
232 |
|
233 term "TYPE(10)" |
|
234 |
|
235 lemma "CARD(0) = 0" by simp |
|
236 lemma "CARD(17) = 17" by simp |
|
237 |
|
238 end |