author  wenzelm 
Tue, 03 Jul 2007 20:26:08 +0200  
changeset 23551  84f0996a530b 
parent 23282  dfc459989d24 
child 23879  4776af8be741 
permissions  rwrr 
17296  1 
(* Title : HOL/Hyperreal/StarClasses.thy 
2 
ID : $Id$ 

3 
Author : Brian Huffman 

4 
*) 

5 

6 
header {* Class Instances *} 

7 

8 
theory StarClasses 

17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17332
diff
changeset

9 
imports StarDef 
17296  10 
begin 
11 

17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

12 
subsection {* Syntactic classes *} 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

13 

22316  14 
instance star :: (zero) zero 
15 
star_zero_def: "0 \<equiv> star_of 0" .. 

16 

17 
instance star :: (one) one 

18 
star_one_def: "1 \<equiv> star_of 1" .. 

19 

20 
instance star :: (plus) plus 

21 
star_add_def: "(op +) \<equiv> *f2* (op +)" .. 

22 

23 
instance star :: (times) times 

24 
star_mult_def: "(op *) \<equiv> *f2* (op *)" .. 

17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

25 

22316  26 
instance star :: (minus) minus 
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17332
diff
changeset

27 
star_minus_def: "uminus \<equiv> *f* uminus" 
22316  28 
star_diff_def: "(op ) \<equiv> *f2* (op )" 
29 
star_abs_def: "abs \<equiv> *f* abs" .. 

30 

31 
instance star :: (inverse) inverse 

17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17332
diff
changeset

32 
star_divide_def: "(op /) \<equiv> *f2* (op /)" 
22316  33 
star_inverse_def: "inverse \<equiv> *f* inverse" .. 
34 

35 
instance star :: (number) number 

36 
star_number_def: "number_of b \<equiv> star_of (number_of b)" .. 

37 

22993  38 
instance star :: (Divides.div) Divides.div 
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17332
diff
changeset

39 
star_div_def: "(op div) \<equiv> *f2* (op div)" 
22316  40 
star_mod_def: "(op mod) \<equiv> *f2* (op mod)" .. 
41 

42 
instance star :: (power) power 

43 
star_power_def: "(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x" .. 

17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

44 

22452
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

45 
instance star :: (ord) ord 
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

46 
star_le_def: "(op \<le>) \<equiv> *p2* (op \<le>)" 
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

47 
star_less_def: "(op <) \<equiv> *p2* (op <)" .. 
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

48 

17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

49 
lemmas star_class_defs [transfer_unfold] = 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

50 
star_zero_def star_one_def star_number_def 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

51 
star_add_def star_diff_def star_minus_def 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

52 
star_mult_def star_divide_def star_inverse_def 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

53 
star_le_def star_less_def star_abs_def 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

54 
star_div_def star_mod_def star_power_def 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

55 

20719  56 
text {* Class operations preserve standard elements *} 
57 

58 
lemma Standard_zero: "0 \<in> Standard" 

59 
by (simp add: star_zero_def) 

60 

61 
lemma Standard_one: "1 \<in> Standard" 

62 
by (simp add: star_one_def) 

63 

64 
lemma Standard_number_of: "number_of b \<in> Standard" 

65 
by (simp add: star_number_def) 

66 

67 
lemma Standard_add: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x + y \<in> Standard" 

68 
by (simp add: star_add_def) 

69 

70 
lemma Standard_diff: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x  y \<in> Standard" 

71 
by (simp add: star_diff_def) 

72 

73 
lemma Standard_minus: "x \<in> Standard \<Longrightarrow>  x \<in> Standard" 

74 
by (simp add: star_minus_def) 

75 

76 
lemma Standard_mult: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x * y \<in> Standard" 

77 
by (simp add: star_mult_def) 

78 

79 
lemma Standard_divide: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x / y \<in> Standard" 

80 
by (simp add: star_divide_def) 

81 

82 
lemma Standard_inverse: "x \<in> Standard \<Longrightarrow> inverse x \<in> Standard" 

83 
by (simp add: star_inverse_def) 

84 

85 
lemma Standard_abs: "x \<in> Standard \<Longrightarrow> abs x \<in> Standard" 

86 
by (simp add: star_abs_def) 

87 

88 
lemma Standard_div: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x div y \<in> Standard" 

89 
by (simp add: star_div_def) 

90 

91 
lemma Standard_mod: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x mod y \<in> Standard" 

92 
by (simp add: star_mod_def) 

93 

94 
lemma Standard_power: "x \<in> Standard \<Longrightarrow> x ^ n \<in> Standard" 

95 
by (simp add: star_power_def) 

96 

97 
lemmas Standard_simps [simp] = 

98 
Standard_zero Standard_one Standard_number_of 

99 
Standard_add Standard_diff Standard_minus 

100 
Standard_mult Standard_divide Standard_inverse 

101 
Standard_abs Standard_div Standard_mod 

102 
Standard_power 

103 

17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

104 
text {* @{term star_of} preserves class operations *} 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

105 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

106 
lemma star_of_add: "star_of (x + y) = star_of x + star_of y" 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

107 
by transfer (rule refl) 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

108 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

109 
lemma star_of_diff: "star_of (x  y) = star_of x  star_of y" 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

110 
by transfer (rule refl) 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

111 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

112 
lemma star_of_minus: "star_of (x) =  star_of x" 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

113 
by transfer (rule refl) 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

114 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

115 
lemma star_of_mult: "star_of (x * y) = star_of x * star_of y" 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

116 
by transfer (rule refl) 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

117 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

118 
lemma star_of_divide: "star_of (x / y) = star_of x / star_of y" 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

119 
by transfer (rule refl) 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

120 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

121 
lemma star_of_inverse: "star_of (inverse x) = inverse (star_of x)" 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

122 
by transfer (rule refl) 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

123 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

124 
lemma star_of_div: "star_of (x div y) = star_of x div star_of y" 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

125 
by transfer (rule refl) 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

126 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

127 
lemma star_of_mod: "star_of (x mod y) = star_of x mod star_of y" 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

128 
by transfer (rule refl) 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

129 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

130 
lemma star_of_power: "star_of (x ^ n) = star_of x ^ n" 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

131 
by transfer (rule refl) 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

132 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

133 
lemma star_of_abs: "star_of (abs x) = abs (star_of x)" 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

134 
by transfer (rule refl) 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

135 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

136 
text {* @{term star_of} preserves numerals *} 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

137 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

138 
lemma star_of_zero: "star_of 0 = 0" 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

139 
by transfer (rule refl) 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

140 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

141 
lemma star_of_one: "star_of 1 = 1" 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

142 
by transfer (rule refl) 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

143 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

144 
lemma star_of_number_of: "star_of (number_of x) = number_of x" 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

145 
by transfer (rule refl) 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

146 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

147 
text {* @{term star_of} preserves orderings *} 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

148 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

149 
lemma star_of_less: "(star_of x < star_of y) = (x < y)" 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

150 
by transfer (rule refl) 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

151 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

152 
lemma star_of_le: "(star_of x \<le> star_of y) = (x \<le> y)" 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

153 
by transfer (rule refl) 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

154 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

155 
lemma star_of_eq: "(star_of x = star_of y) = (x = y)" 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

156 
by transfer (rule refl) 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

157 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

158 
text{*As above, for 0*} 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

159 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

160 
lemmas star_of_0_less = star_of_less [of 0, simplified star_of_zero] 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

161 
lemmas star_of_0_le = star_of_le [of 0, simplified star_of_zero] 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

162 
lemmas star_of_0_eq = star_of_eq [of 0, simplified star_of_zero] 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

163 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

164 
lemmas star_of_less_0 = star_of_less [of _ 0, simplified star_of_zero] 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

165 
lemmas star_of_le_0 = star_of_le [of _ 0, simplified star_of_zero] 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

166 
lemmas star_of_eq_0 = star_of_eq [of _ 0, simplified star_of_zero] 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

167 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

168 
text{*As above, for 1*} 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

169 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

170 
lemmas star_of_1_less = star_of_less [of 1, simplified star_of_one] 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

171 
lemmas star_of_1_le = star_of_le [of 1, simplified star_of_one] 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

172 
lemmas star_of_1_eq = star_of_eq [of 1, simplified star_of_one] 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

173 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

174 
lemmas star_of_less_1 = star_of_less [of _ 1, simplified star_of_one] 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

175 
lemmas star_of_le_1 = star_of_le [of _ 1, simplified star_of_one] 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

176 
lemmas star_of_eq_1 = star_of_eq [of _ 1, simplified star_of_one] 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

177 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

178 
text{*As above, for numerals*} 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

179 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

180 
lemmas star_of_number_less = 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

181 
star_of_less [of "number_of w", standard, simplified star_of_number_of] 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

182 
lemmas star_of_number_le = 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

183 
star_of_le [of "number_of w", standard, simplified star_of_number_of] 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

184 
lemmas star_of_number_eq = 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

185 
star_of_eq [of "number_of w", standard, simplified star_of_number_of] 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

186 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

187 
lemmas star_of_less_number = 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

188 
star_of_less [of _ "number_of w", standard, simplified star_of_number_of] 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

189 
lemmas star_of_le_number = 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

190 
star_of_le [of _ "number_of w", standard, simplified star_of_number_of] 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

191 
lemmas star_of_eq_number = 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

192 
star_of_eq [of _ "number_of w", standard, simplified star_of_number_of] 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

193 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

194 
lemmas star_of_simps [simp] = 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

195 
star_of_add star_of_diff star_of_minus 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

196 
star_of_mult star_of_divide star_of_inverse 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

197 
star_of_div star_of_mod 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

198 
star_of_power star_of_abs 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

199 
star_of_zero star_of_one star_of_number_of 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

200 
star_of_less star_of_le star_of_eq 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

201 
star_of_0_less star_of_0_le star_of_0_eq 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

202 
star_of_less_0 star_of_le_0 star_of_eq_0 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

203 
star_of_1_less star_of_1_le star_of_1_eq 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

204 
star_of_less_1 star_of_le_1 star_of_eq_1 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

205 
star_of_number_less star_of_number_le star_of_number_eq 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

206 
star_of_less_number star_of_le_number star_of_eq_number 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

207 

22452
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

208 
subsection {* Ordering and lattice classes *} 
17296  209 

210 
instance star :: (order) order 

211 
apply (intro_classes) 

22316  212 
apply (transfer, rule order_less_le) 
17296  213 
apply (transfer, rule order_refl) 
214 
apply (transfer, erule (1) order_trans) 

215 
apply (transfer, erule (1) order_antisym) 

216 
done 

217 

22452
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

218 
instance star :: (lower_semilattice) lower_semilattice 
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

219 
star_inf_def [transfer_unfold]: "inf \<equiv> *f2* inf" 
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

220 
by default (transfer star_inf_def, auto)+ 
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

221 

8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

222 
instance star :: (upper_semilattice) upper_semilattice 
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

223 
star_sup_def [transfer_unfold]: "sup \<equiv> *f2* sup" 
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

224 
by default (transfer star_sup_def, auto)+ 
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

225 

8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

226 
instance star :: (lattice) lattice .. 
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

227 

8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

228 
instance star :: (distrib_lattice) distrib_lattice 
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

229 
by default (transfer, auto simp add: sup_inf_distrib1) 
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

230 

8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

231 
lemma Standard_inf [simp]: 
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

232 
"\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> inf x y \<in> Standard" 
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

233 
by (simp add: star_inf_def) 
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

234 

8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

235 
lemma Standard_sup [simp]: 
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

236 
"\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> sup x y \<in> Standard" 
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

237 
by (simp add: star_sup_def) 
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

238 

8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

239 
lemma star_of_inf [simp]: "star_of (inf x y) = inf (star_of x) (star_of y)" 
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

240 
by transfer (rule refl) 
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

241 

8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

242 
lemma star_of_sup [simp]: "star_of (sup x y) = sup (star_of x) (star_of y)" 
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

243 
by transfer (rule refl) 
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset

244 

17296  245 
instance star :: (linorder) linorder 
246 
by (intro_classes, transfer, rule linorder_linear) 

247 

20720  248 
lemma star_max_def [transfer_unfold]: "max = *f2* max" 
249 
apply (rule ext, rule ext) 

250 
apply (unfold max_def, transfer, fold max_def) 

251 
apply (rule refl) 

252 
done 

253 

254 
lemma star_min_def [transfer_unfold]: "min = *f2* min" 

255 
apply (rule ext, rule ext) 

256 
apply (unfold min_def, transfer, fold min_def) 

257 
apply (rule refl) 

258 
done 

259 

260 
lemma Standard_max [simp]: 

261 
"\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> max x y \<in> Standard" 

262 
by (simp add: star_max_def) 

263 

264 
lemma Standard_min [simp]: 

265 
"\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> min x y \<in> Standard" 

266 
by (simp add: star_min_def) 

267 

268 
lemma star_of_max [simp]: "star_of (max x y) = max (star_of x) (star_of y)" 

269 
by transfer (rule refl) 

270 

271 
lemma star_of_min [simp]: "star_of (min x y) = min (star_of x) (star_of y)" 

272 
by transfer (rule refl) 

273 

17296  274 

17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

275 
subsection {* Ordered group classes *} 
17296  276 

277 
instance star :: (semigroup_add) semigroup_add 

278 
by (intro_classes, transfer, rule add_assoc) 

279 

280 
instance star :: (ab_semigroup_add) ab_semigroup_add 

281 
by (intro_classes, transfer, rule add_commute) 

282 

283 
instance star :: (semigroup_mult) semigroup_mult 

284 
by (intro_classes, transfer, rule mult_assoc) 

285 

286 
instance star :: (ab_semigroup_mult) ab_semigroup_mult 

287 
by (intro_classes, transfer, rule mult_commute) 

288 

289 
instance star :: (comm_monoid_add) comm_monoid_add 

22384
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22316
diff
changeset

290 
by (intro_classes, transfer, rule comm_monoid_add_class.zero_plus.add_0) 
17296  291 

292 
instance star :: (monoid_mult) monoid_mult 

293 
apply (intro_classes) 

294 
apply (transfer, rule mult_1_left) 

295 
apply (transfer, rule mult_1_right) 

296 
done 

297 

298 
instance star :: (comm_monoid_mult) comm_monoid_mult 

299 
by (intro_classes, transfer, rule mult_1) 

300 

301 
instance star :: (cancel_semigroup_add) cancel_semigroup_add 

302 
apply (intro_classes) 

303 
apply (transfer, erule add_left_imp_eq) 

304 
apply (transfer, erule add_right_imp_eq) 

305 
done 

306 

307 
instance star :: (cancel_ab_semigroup_add) cancel_ab_semigroup_add 

308 
by (intro_classes, transfer, rule add_imp_eq) 

309 

310 
instance star :: (ab_group_add) ab_group_add 

311 
apply (intro_classes) 

312 
apply (transfer, rule left_minus) 

313 
apply (transfer, rule diff_minus) 

314 
done 

315 

316 
instance star :: (pordered_ab_semigroup_add) pordered_ab_semigroup_add 

317 
by (intro_classes, transfer, rule add_left_mono) 

318 

319 
instance star :: (pordered_cancel_ab_semigroup_add) pordered_cancel_ab_semigroup_add .. 

320 

321 
instance star :: (pordered_ab_semigroup_add_imp_le) pordered_ab_semigroup_add_imp_le 

322 
by (intro_classes, transfer, rule add_le_imp_le_left) 

323 

324 
instance star :: (pordered_ab_group_add) pordered_ab_group_add .. 

325 
instance star :: (ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add .. 

326 
instance star :: (lordered_ab_group_meet) lordered_ab_group_meet .. 

327 
instance star :: (lordered_ab_group_meet) lordered_ab_group_meet .. 

328 
instance star :: (lordered_ab_group) lordered_ab_group .. 

329 

330 
instance star :: (lordered_ab_group_abs) lordered_ab_group_abs 

17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

331 
by (intro_classes, transfer, rule abs_lattice) 
17296  332 

17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17332
diff
changeset

333 
subsection {* Ring and field classes *} 
17296  334 

335 
instance star :: (semiring) semiring 

336 
apply (intro_classes) 

337 
apply (transfer, rule left_distrib) 

338 
apply (transfer, rule right_distrib) 

339 
done 

340 

21199
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20720
diff
changeset

341 
instance star :: (semiring_0) semiring_0 
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20720
diff
changeset

342 
by intro_classes (transfer, simp)+ 
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20720
diff
changeset

343 

17296  344 
instance star :: (semiring_0_cancel) semiring_0_cancel .. 
345 

346 
instance star :: (comm_semiring) comm_semiring 

347 
by (intro_classes, transfer, rule distrib) 

348 

349 
instance star :: (comm_semiring_0) comm_semiring_0 .. 

350 
instance star :: (comm_semiring_0_cancel) comm_semiring_0_cancel .. 

351 

20633  352 
instance star :: (zero_neq_one) zero_neq_one 
17296  353 
by (intro_classes, transfer, rule zero_neq_one) 
354 

355 
instance star :: (semiring_1) semiring_1 .. 

356 
instance star :: (comm_semiring_1) comm_semiring_1 .. 

357 

20633  358 
instance star :: (no_zero_divisors) no_zero_divisors 
17296  359 
by (intro_classes, transfer, rule no_zero_divisors) 
360 

361 
instance star :: (semiring_1_cancel) semiring_1_cancel .. 

362 
instance star :: (comm_semiring_1_cancel) comm_semiring_1_cancel .. 

363 
instance star :: (ring) ring .. 

364 
instance star :: (comm_ring) comm_ring .. 

365 
instance star :: (ring_1) ring_1 .. 

366 
instance star :: (comm_ring_1) comm_ring_1 .. 

22992  367 
instance star :: (ring_no_zero_divisors) ring_no_zero_divisors .. 
23551
84f0996a530b
rename class dom to ring_1_no_zero_divisors (cf. HOL/Ring_and_Field.thy 1.84 by huffman);
wenzelm
parents:
23282
diff
changeset

368 
instance star :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors .. 
17296  369 
instance star :: (idom) idom .. 
370 

20540  371 
instance star :: (division_ring) division_ring 
372 
apply (intro_classes) 

373 
apply (transfer, erule left_inverse) 

374 
apply (transfer, erule right_inverse) 

375 
done 

376 

17296  377 
instance star :: (field) field 
378 
apply (intro_classes) 

379 
apply (transfer, erule left_inverse) 

380 
apply (transfer, rule divide_inverse) 

381 
done 

382 

383 
instance star :: (division_by_zero) division_by_zero 

384 
by (intro_classes, transfer, rule inverse_zero) 

385 

386 
instance star :: (pordered_semiring) pordered_semiring 

387 
apply (intro_classes) 

388 
apply (transfer, erule (1) mult_left_mono) 

389 
apply (transfer, erule (1) mult_right_mono) 

390 
done 

391 

392 
instance star :: (pordered_cancel_semiring) pordered_cancel_semiring .. 

393 

394 
instance star :: (ordered_semiring_strict) ordered_semiring_strict 

395 
apply (intro_classes) 

396 
apply (transfer, erule (1) mult_strict_left_mono) 

397 
apply (transfer, erule (1) mult_strict_right_mono) 

398 
done 

399 

400 
instance star :: (pordered_comm_semiring) pordered_comm_semiring 

22384
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22316
diff
changeset

401 
by (intro_classes, transfer, rule mult_mono1_class.times_zero_less_eq_less.mult_mono) 
17296  402 

403 
instance star :: (pordered_cancel_comm_semiring) pordered_cancel_comm_semiring .. 

404 

405 
instance star :: (ordered_comm_semiring_strict) ordered_comm_semiring_strict 

22518  406 
by (intro_classes, transfer, rule ordered_comm_semiring_strict_class.plus_less_eq_less_zero_times.mult_strict_mono) 
17296  407 

408 
instance star :: (pordered_ring) pordered_ring .. 

409 
instance star :: (lordered_ring) lordered_ring .. 

410 

20633  411 
instance star :: (abs_if) abs_if 
17296  412 
by (intro_classes, transfer, rule abs_if) 
413 

414 
instance star :: (ordered_ring_strict) ordered_ring_strict .. 

415 
instance star :: (pordered_comm_ring) pordered_comm_ring .. 

416 

417 
instance star :: (ordered_semidom) ordered_semidom 

418 
by (intro_classes, transfer, rule zero_less_one) 

419 

420 
instance star :: (ordered_idom) ordered_idom .. 

421 
instance star :: (ordered_field) ordered_field .. 

422 

17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

423 
subsection {* Power classes *} 
17296  424 

425 
text {* 

426 
Proving the class axiom @{thm [source] power_Suc} for type 

427 
@{typ "'a star"} is a little tricky, because it quantifies 

428 
over values of type @{typ nat}. The transfer principle does 

429 
not handle quantification over nonstar types in general, 

430 
but we can work around this by fixing an arbitrary @{typ nat} 

431 
value, and then applying the transfer principle. 

432 
*} 

433 

434 
instance star :: (recpower) recpower 

435 
proof 

436 
show "\<And>a::'a star. a ^ 0 = 1" 

437 
by transfer (rule power_0) 

438 
next 

439 
fix n show "\<And>a::'a star. a ^ Suc n = a * a ^ n" 

440 
by transfer (rule power_Suc) 

441 
qed 

442 

17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

443 
subsection {* Number classes *} 
17296  444 

20720  445 
lemma star_of_nat_def [transfer_unfold]: "of_nat n = star_of (of_nat n)" 
446 
by (induct_tac n, simp_all) 

447 

448 
lemma Standard_of_nat [simp]: "of_nat n \<in> Standard" 

449 
by (simp add: star_of_nat_def) 

17296  450 

17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

451 
lemma star_of_of_nat [simp]: "star_of (of_nat n) = of_nat n" 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

452 
by transfer (rule refl) 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

453 

20720  454 
lemma star_of_int_def [transfer_unfold]: "of_int z = star_of (of_int z)" 
455 
by (rule_tac z=z in int_diff_cases, simp) 

456 

457 
lemma Standard_of_int [simp]: "of_int z \<in> Standard" 

458 
by (simp add: star_of_int_def) 

17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

459 

4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

460 
lemma star_of_of_int [simp]: "star_of (of_int z) = of_int z" 
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17296
diff
changeset

461 
by transfer (rule refl) 
17296  462 

23282
dfc459989d24
add axclass semiring_char_0 for types where of_nat is injective
huffman
parents:
22993
diff
changeset

463 
instance star :: (semiring_char_0) semiring_char_0 
dfc459989d24
add axclass semiring_char_0 for types where of_nat is injective
huffman
parents:
22993
diff
changeset

464 
by (intro_classes, simp only: star_of_nat_def star_of_eq of_nat_eq_iff) 
dfc459989d24
add axclass semiring_char_0 for types where of_nat is injective
huffman
parents:
22993
diff
changeset

465 

dfc459989d24
add axclass semiring_char_0 for types where of_nat is injective
huffman
parents:
22993
diff
changeset

466 
instance star :: (ring_char_0) ring_char_0 .. 
22911
2f5e8d70a179
new axclass ring_char_0 for rings with characteristic 0, used for of_int_eq_iff and related lemmas
huffman
parents:
22518
diff
changeset

467 

17296  468 
instance star :: (number_ring) number_ring 
469 
by (intro_classes, simp only: star_number_def star_of_int_def number_of_eq) 

470 

17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17332
diff
changeset

471 
subsection {* Finite class *} 
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17332
diff
changeset

472 

e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17332
diff
changeset

473 
lemma starset_finite: "finite A \<Longrightarrow> *s* A = star_of ` A" 
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17332
diff
changeset

474 
by (erule finite_induct, simp_all) 
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17332
diff
changeset

475 

e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17332
diff
changeset

476 
instance star :: (finite) finite 
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17332
diff
changeset

477 
apply (intro_classes) 
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17332
diff
changeset

478 
apply (subst starset_UNIV [symmetric]) 
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17332
diff
changeset

479 
apply (subst starset_finite [OF finite]) 
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17332
diff
changeset

480 
apply (rule finite_imageI [OF finite]) 
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17332
diff
changeset

481 
done 
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17332
diff
changeset

482 

17296  483 
end 