author  haftmann 
Mon, 26 Jan 2009 22:14:17 +0100  
changeset 29629  5111ce425e7a 
parent 29025  8c8859c0d734 
child 29997  f6756c097c2d 
child 30240  5b25fee0362c 
permissions  rwrr 
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 