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