author  huffman 
Sun, 25 Mar 2012 20:15:39 +0200  
changeset 47108  2a1953f0d20d 
parent 46008  c296c75f4cf4 
child 47328  9f11a3cd84b1 
permissions  rwrr 
27468  1 
(* Title : HOL/Hyperreal/StarDef.thy 
2 
Author : Jacques D. Fleuriot and Brian Huffman 

3 
*) 

4 

5 
header {* Construction of Star Types Using Ultrafilters *} 

6 

7 
theory StarDef 

8 
imports Filter 

9 
uses ("transfer.ML") 

10 
begin 

11 

12 
subsection {* A Free Ultrafilter over the Naturals *} 

13 

14 
definition 

15 
FreeUltrafilterNat :: "nat set set" ("\<U>") where 

16 
"\<U> = (SOME U. freeultrafilter U)" 

17 

18 
lemma freeultrafilter_FreeUltrafilterNat: "freeultrafilter \<U>" 

19 
apply (unfold FreeUltrafilterNat_def) 

46008
c296c75f4cf4
reverted some changes for set>predicate transition, according to "hg log u berghofe r Isabelle2007:Isabelle2008";
wenzelm
parents:
45694
diff
changeset

20 
apply (rule someI_ex) 
27468  21 
apply (rule freeultrafilter_Ex) 
22 
apply (rule nat_infinite) 

23 
done 

24 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30198
diff
changeset

25 
interpretation FreeUltrafilterNat: freeultrafilter FreeUltrafilterNat 
27468  26 
by (rule freeultrafilter_FreeUltrafilterNat) 
27 

28 
text {* This rule takes the place of the old ultra tactic *} 

29 

30 
lemma ultra: 

31 
"\<lbrakk>{n. P n} \<in> \<U>; {n. P n \<longrightarrow> Q n} \<in> \<U>\<rbrakk> \<Longrightarrow> {n. Q n} \<in> \<U>" 

32 
by (simp add: Collect_imp_eq 

33 
FreeUltrafilterNat.Un_iff FreeUltrafilterNat.Compl_iff) 

34 

35 

36 
subsection {* Definition of @{text star} type constructor *} 

37 

38 
definition 

39 
starrel :: "((nat \<Rightarrow> 'a) \<times> (nat \<Rightarrow> 'a)) set" where 

40 
"starrel = {(X,Y). {n. X n = Y n} \<in> \<U>}" 

41 

45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45605
diff
changeset

42 
definition "star = (UNIV :: (nat \<Rightarrow> 'a) set) // starrel" 
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45605
diff
changeset

43 

4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45605
diff
changeset

44 
typedef (open) 'a star = "star :: (nat \<Rightarrow> 'a) set set" 
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45605
diff
changeset

45 
unfolding star_def by (auto intro: quotientI) 
27468  46 

47 
definition 

48 
star_n :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a star" where 

49 
"star_n X = Abs_star (starrel `` {X})" 

50 

51 
theorem star_cases [case_names star_n, cases type: star]: 

52 
"(\<And>X. x = star_n X \<Longrightarrow> P) \<Longrightarrow> P" 

53 
by (cases x, unfold star_n_def star_def, erule quotientE, fast) 

54 

55 
lemma all_star_eq: "(\<forall>x. P x) = (\<forall>X. P (star_n X))" 

56 
by (auto, rule_tac x=x in star_cases, simp) 

57 

58 
lemma ex_star_eq: "(\<exists>x. P x) = (\<exists>X. P (star_n X))" 

59 
by (auto, rule_tac x=x in star_cases, auto) 

60 

61 
text {* Proving that @{term starrel} is an equivalence relation *} 

62 

63 
lemma starrel_iff [iff]: "((X,Y) \<in> starrel) = ({n. X n = Y n} \<in> \<U>)" 

64 
by (simp add: starrel_def) 

65 

66 
lemma equiv_starrel: "equiv UNIV starrel" 

40815  67 
proof (rule equivI) 
30198  68 
show "refl starrel" by (simp add: refl_on_def) 
27468  69 
show "sym starrel" by (simp add: sym_def eq_commute) 
70 
show "trans starrel" by (auto intro: transI elim!: ultra) 

71 
qed 

72 

73 
lemmas equiv_starrel_iff = 

74 
eq_equiv_class_iff [OF equiv_starrel UNIV_I UNIV_I] 

75 

76 
lemma starrel_in_star: "starrel``{x} \<in> star" 

77 
by (simp add: star_def quotientI) 

78 

79 
lemma star_n_eq_iff: "(star_n X = star_n Y) = ({n. X n = Y n} \<in> \<U>)" 

80 
by (simp add: star_n_def Abs_star_inject starrel_in_star equiv_starrel_iff) 

81 

82 

83 
subsection {* Transfer principle *} 

84 

85 
text {* This introduction rule starts each transfer proof. *} 

86 
lemma transfer_start: 

87 
"P \<equiv> {n. Q} \<in> \<U> \<Longrightarrow> Trueprop P \<equiv> Trueprop Q" 

88 
by (subgoal_tac "P \<equiv> Q", simp, simp add: atomize_eq) 

89 

90 
text {*Initialize transfer tactic.*} 

91 
use "transfer.ML" 

92 
setup Transfer.setup 

93 

94 
text {* Transfer introduction rules. *} 

95 

96 
lemma transfer_ex [transfer_intro]: 

97 
"\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk> 

98 
\<Longrightarrow> \<exists>x::'a star. p x \<equiv> {n. \<exists>x. P n x} \<in> \<U>" 

99 
by (simp only: ex_star_eq FreeUltrafilterNat.Collect_ex) 

100 

101 
lemma transfer_all [transfer_intro]: 

102 
"\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk> 

103 
\<Longrightarrow> \<forall>x::'a star. p x \<equiv> {n. \<forall>x. P n x} \<in> \<U>" 

104 
by (simp only: all_star_eq FreeUltrafilterNat.Collect_all) 

105 

106 
lemma transfer_not [transfer_intro]: 

107 
"\<lbrakk>p \<equiv> {n. P n} \<in> \<U>\<rbrakk> \<Longrightarrow> \<not> p \<equiv> {n. \<not> P n} \<in> \<U>" 

108 
by (simp only: FreeUltrafilterNat.Collect_not) 

109 

110 
lemma transfer_conj [transfer_intro]: 

111 
"\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk> 

112 
\<Longrightarrow> p \<and> q \<equiv> {n. P n \<and> Q n} \<in> \<U>" 

113 
by (simp only: FreeUltrafilterNat.Collect_conj) 

114 

115 
lemma transfer_disj [transfer_intro]: 

116 
"\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk> 

117 
\<Longrightarrow> p \<or> q \<equiv> {n. P n \<or> Q n} \<in> \<U>" 

118 
by (simp only: FreeUltrafilterNat.Collect_disj) 

119 

120 
lemma transfer_imp [transfer_intro]: 

121 
"\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk> 

122 
\<Longrightarrow> p \<longrightarrow> q \<equiv> {n. P n \<longrightarrow> Q n} \<in> \<U>" 

123 
by (simp only: imp_conv_disj transfer_disj transfer_not) 

124 

125 
lemma transfer_iff [transfer_intro]: 

126 
"\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk> 

127 
\<Longrightarrow> p = q \<equiv> {n. P n = Q n} \<in> \<U>" 

128 
by (simp only: iff_conv_conj_imp transfer_conj transfer_imp) 

129 

130 
lemma transfer_if_bool [transfer_intro]: 

131 
"\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; x \<equiv> {n. X n} \<in> \<U>; y \<equiv> {n. Y n} \<in> \<U>\<rbrakk> 

132 
\<Longrightarrow> (if p then x else y) \<equiv> {n. if P n then X n else Y n} \<in> \<U>" 

133 
by (simp only: if_bool_eq_conj transfer_conj transfer_imp transfer_not) 

134 

135 
lemma transfer_eq [transfer_intro]: 

136 
"\<lbrakk>x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk> \<Longrightarrow> x = y \<equiv> {n. X n = Y n} \<in> \<U>" 

137 
by (simp only: star_n_eq_iff) 

138 

139 
lemma transfer_if [transfer_intro]: 

140 
"\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk> 

141 
\<Longrightarrow> (if p then x else y) \<equiv> star_n (\<lambda>n. if P n then X n else Y n)" 

142 
apply (rule eq_reflection) 

143 
apply (auto simp add: star_n_eq_iff transfer_not elim!: ultra) 

144 
done 

145 

146 
lemma transfer_fun_eq [transfer_intro]: 

147 
"\<lbrakk>\<And>X. f (star_n X) = g (star_n X) 

148 
\<equiv> {n. F n (X n) = G n (X n)} \<in> \<U>\<rbrakk> 

149 
\<Longrightarrow> f = g \<equiv> {n. F n = G n} \<in> \<U>" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

150 
by (simp only: fun_eq_iff transfer_all) 
27468  151 

152 
lemma transfer_star_n [transfer_intro]: "star_n X \<equiv> star_n (\<lambda>n. X n)" 

153 
by (rule reflexive) 

154 

155 
lemma transfer_bool [transfer_intro]: "p \<equiv> {n. p} \<in> \<U>" 

156 
by (simp add: atomize_eq) 

157 

158 

159 
subsection {* Standard elements *} 

160 

161 
definition 

162 
star_of :: "'a \<Rightarrow> 'a star" where 

163 
"star_of x == star_n (\<lambda>n. x)" 

164 

165 
definition 

166 
Standard :: "'a star set" where 

167 
"Standard = range star_of" 

168 

169 
text {* Transfer tactic should remove occurrences of @{term star_of} *} 

170 
setup {* Transfer.add_const "StarDef.star_of" *} 

171 

172 
declare star_of_def [transfer_intro] 

173 

174 
lemma star_of_inject: "(star_of x = star_of y) = (x = y)" 

175 
by (transfer, rule refl) 

176 

177 
lemma Standard_star_of [simp]: "star_of x \<in> Standard" 

178 
by (simp add: Standard_def) 

179 

180 

181 
subsection {* Internal functions *} 

182 

183 
definition 

184 
Ifun :: "('a \<Rightarrow> 'b) star \<Rightarrow> 'a star \<Rightarrow> 'b star" ("_ \<star> _" [300,301] 300) where 

185 
"Ifun f \<equiv> \<lambda>x. Abs_star 

186 
(\<Union>F\<in>Rep_star f. \<Union>X\<in>Rep_star x. starrel``{\<lambda>n. F n (X n)})" 

187 

188 
lemma Ifun_congruent2: 

189 
"congruent2 starrel starrel (\<lambda>F X. starrel``{\<lambda>n. F n (X n)})" 

190 
by (auto simp add: congruent2_def equiv_starrel_iff elim!: ultra) 

191 

192 
lemma Ifun_star_n: "star_n F \<star> star_n X = star_n (\<lambda>n. F n (X n))" 

193 
by (simp add: Ifun_def star_n_def Abs_star_inverse starrel_in_star 

194 
UN_equiv_class2 [OF equiv_starrel equiv_starrel Ifun_congruent2]) 

195 

196 
text {* Transfer tactic should remove occurrences of @{term Ifun} *} 

197 
setup {* Transfer.add_const "StarDef.Ifun" *} 

198 

199 
lemma transfer_Ifun [transfer_intro]: 

200 
"\<lbrakk>f \<equiv> star_n F; x \<equiv> star_n X\<rbrakk> \<Longrightarrow> f \<star> x \<equiv> star_n (\<lambda>n. F n (X n))" 

201 
by (simp only: Ifun_star_n) 

202 

203 
lemma Ifun_star_of [simp]: "star_of f \<star> star_of x = star_of (f x)" 

204 
by (transfer, rule refl) 

205 

206 
lemma Standard_Ifun [simp]: 

207 
"\<lbrakk>f \<in> Standard; x \<in> Standard\<rbrakk> \<Longrightarrow> f \<star> x \<in> Standard" 

208 
by (auto simp add: Standard_def) 

209 

210 
text {* Nonstandard extensions of functions *} 

211 

212 
definition 

213 
starfun :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a star \<Rightarrow> 'b star)" ("*f* _" [80] 80) where 

214 
"starfun f == \<lambda>x. star_of f \<star> x" 

215 

216 
definition 

217 
starfun2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a star \<Rightarrow> 'b star \<Rightarrow> 'c star)" 

218 
("*f2* _" [80] 80) where 

219 
"starfun2 f == \<lambda>x y. star_of f \<star> x \<star> y" 

220 

221 
declare starfun_def [transfer_unfold] 

222 
declare starfun2_def [transfer_unfold] 

223 

224 
lemma starfun_star_n: "( *f* f) (star_n X) = star_n (\<lambda>n. f (X n))" 

225 
by (simp only: starfun_def star_of_def Ifun_star_n) 

226 

227 
lemma starfun2_star_n: 

228 
"( *f2* f) (star_n X) (star_n Y) = star_n (\<lambda>n. f (X n) (Y n))" 

229 
by (simp only: starfun2_def star_of_def Ifun_star_n) 

230 

231 
lemma starfun_star_of [simp]: "( *f* f) (star_of x) = star_of (f x)" 

232 
by (transfer, rule refl) 

233 

234 
lemma starfun2_star_of [simp]: "( *f2* f) (star_of x) = *f* f x" 

235 
by (transfer, rule refl) 

236 

237 
lemma Standard_starfun [simp]: "x \<in> Standard \<Longrightarrow> starfun f x \<in> Standard" 

238 
by (simp add: starfun_def) 

239 

240 
lemma Standard_starfun2 [simp]: 

241 
"\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> starfun2 f x y \<in> Standard" 

242 
by (simp add: starfun2_def) 

243 

244 
lemma Standard_starfun_iff: 

245 
assumes inj: "\<And>x y. f x = f y \<Longrightarrow> x = y" 

246 
shows "(starfun f x \<in> Standard) = (x \<in> Standard)" 

247 
proof 

248 
assume "x \<in> Standard" 

249 
thus "starfun f x \<in> Standard" by simp 

250 
next 

251 
have inj': "\<And>x y. starfun f x = starfun f y \<Longrightarrow> x = y" 

252 
using inj by transfer 

253 
assume "starfun f x \<in> Standard" 

254 
then obtain b where b: "starfun f x = star_of b" 

255 
unfolding Standard_def .. 

256 
hence "\<exists>x. starfun f x = star_of b" .. 

257 
hence "\<exists>a. f a = b" by transfer 

258 
then obtain a where "f a = b" .. 

259 
hence "starfun f (star_of a) = star_of b" by transfer 

260 
with b have "starfun f x = starfun f (star_of a)" by simp 

261 
hence "x = star_of a" by (rule inj') 

262 
thus "x \<in> Standard" 

263 
unfolding Standard_def by auto 

264 
qed 

265 

266 
lemma Standard_starfun2_iff: 

267 
assumes inj: "\<And>a b a' b'. f a b = f a' b' \<Longrightarrow> a = a' \<and> b = b'" 

268 
shows "(starfun2 f x y \<in> Standard) = (x \<in> Standard \<and> y \<in> Standard)" 

269 
proof 

270 
assume "x \<in> Standard \<and> y \<in> Standard" 

271 
thus "starfun2 f x y \<in> Standard" by simp 

272 
next 

273 
have inj': "\<And>x y z w. starfun2 f x y = starfun2 f z w \<Longrightarrow> x = z \<and> y = w" 

274 
using inj by transfer 

275 
assume "starfun2 f x y \<in> Standard" 

276 
then obtain c where c: "starfun2 f x y = star_of c" 

277 
unfolding Standard_def .. 

278 
hence "\<exists>x y. starfun2 f x y = star_of c" by auto 

279 
hence "\<exists>a b. f a b = c" by transfer 

280 
then obtain a b where "f a b = c" by auto 

281 
hence "starfun2 f (star_of a) (star_of b) = star_of c" 

282 
by transfer 

283 
with c have "starfun2 f x y = starfun2 f (star_of a) (star_of b)" 

284 
by simp 

285 
hence "x = star_of a \<and> y = star_of b" 

286 
by (rule inj') 

287 
thus "x \<in> Standard \<and> y \<in> Standard" 

288 
unfolding Standard_def by auto 

289 
qed 

290 

291 

292 
subsection {* Internal predicates *} 

293 

294 
definition unstar :: "bool star \<Rightarrow> bool" where 

37765  295 
"unstar b \<longleftrightarrow> b = star_of True" 
27468  296 

297 
lemma unstar_star_n: "unstar (star_n P) = ({n. P n} \<in> \<U>)" 

298 
by (simp add: unstar_def star_of_def star_n_eq_iff) 

299 

300 
lemma unstar_star_of [simp]: "unstar (star_of p) = p" 

301 
by (simp add: unstar_def star_of_inject) 

302 

303 
text {* Transfer tactic should remove occurrences of @{term unstar} *} 

304 
setup {* Transfer.add_const "StarDef.unstar" *} 

305 

306 
lemma transfer_unstar [transfer_intro]: 

307 
"p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> {n. P n} \<in> \<U>" 

308 
by (simp only: unstar_star_n) 

309 

310 
definition 

311 
starP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a star \<Rightarrow> bool" ("*p* _" [80] 80) where 

312 
"*p* P = (\<lambda>x. unstar (star_of P \<star> x))" 

313 

314 
definition 

315 
starP2 :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a star \<Rightarrow> 'b star \<Rightarrow> bool" ("*p2* _" [80] 80) where 

316 
"*p2* P = (\<lambda>x y. unstar (star_of P \<star> x \<star> y))" 

317 

318 
declare starP_def [transfer_unfold] 

319 
declare starP2_def [transfer_unfold] 

320 

321 
lemma starP_star_n: "( *p* P) (star_n X) = ({n. P (X n)} \<in> \<U>)" 

322 
by (simp only: starP_def star_of_def Ifun_star_n unstar_star_n) 

323 

324 
lemma starP2_star_n: 

325 
"( *p2* P) (star_n X) (star_n Y) = ({n. P (X n) (Y n)} \<in> \<U>)" 

326 
by (simp only: starP2_def star_of_def Ifun_star_n unstar_star_n) 

327 

328 
lemma starP_star_of [simp]: "( *p* P) (star_of x) = P x" 

329 
by (transfer, rule refl) 

330 

331 
lemma starP2_star_of [simp]: "( *p2* P) (star_of x) = *p* P x" 

332 
by (transfer, rule refl) 

333 

334 

335 
subsection {* Internal sets *} 

336 

337 
definition 

338 
Iset :: "'a set star \<Rightarrow> 'a star set" where 

339 
"Iset A = {x. ( *p2* op \<in>) x A}" 

340 

341 
lemma Iset_star_n: 

342 
"(star_n X \<in> Iset (star_n A)) = ({n. X n \<in> A n} \<in> \<U>)" 

343 
by (simp add: Iset_def starP2_star_n) 

344 

345 
text {* Transfer tactic should remove occurrences of @{term Iset} *} 

346 
setup {* Transfer.add_const "StarDef.Iset" *} 

347 

348 
lemma transfer_mem [transfer_intro]: 

349 
"\<lbrakk>x \<equiv> star_n X; a \<equiv> Iset (star_n A)\<rbrakk> 

350 
\<Longrightarrow> x \<in> a \<equiv> {n. X n \<in> A n} \<in> \<U>" 

351 
by (simp only: Iset_star_n) 

352 

353 
lemma transfer_Collect [transfer_intro]: 

354 
"\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk> 

355 
\<Longrightarrow> Collect p \<equiv> Iset (star_n (\<lambda>n. Collect (P n)))" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

356 
by (simp add: atomize_eq set_eq_iff all_star_eq Iset_star_n) 
27468  357 

358 
lemma transfer_set_eq [transfer_intro]: 

359 
"\<lbrakk>a \<equiv> Iset (star_n A); b \<equiv> Iset (star_n B)\<rbrakk> 

360 
\<Longrightarrow> a = b \<equiv> {n. A n = B n} \<in> \<U>" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

361 
by (simp only: set_eq_iff transfer_all transfer_iff transfer_mem) 
27468  362 

363 
lemma transfer_ball [transfer_intro]: 

364 
"\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk> 

365 
\<Longrightarrow> \<forall>x\<in>a. p x \<equiv> {n. \<forall>x\<in>A n. P n x} \<in> \<U>" 

366 
by (simp only: Ball_def transfer_all transfer_imp transfer_mem) 

367 

368 
lemma transfer_bex [transfer_intro]: 

369 
"\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk> 

370 
\<Longrightarrow> \<exists>x\<in>a. p x \<equiv> {n. \<exists>x\<in>A n. P n x} \<in> \<U>" 

371 
by (simp only: Bex_def transfer_ex transfer_conj transfer_mem) 

372 

373 
lemma transfer_Iset [transfer_intro]: 

374 
"\<lbrakk>a \<equiv> star_n A\<rbrakk> \<Longrightarrow> Iset a \<equiv> Iset (star_n (\<lambda>n. A n))" 

375 
by simp 

376 

377 
text {* Nonstandard extensions of sets. *} 

378 

379 
definition 

380 
starset :: "'a set \<Rightarrow> 'a star set" ("*s* _" [80] 80) where 

381 
"starset A = Iset (star_of A)" 

382 

383 
declare starset_def [transfer_unfold] 

384 

385 
lemma starset_mem: "(star_of x \<in> *s* A) = (x \<in> A)" 

386 
by (transfer, rule refl) 

387 

388 
lemma starset_UNIV: "*s* (UNIV::'a set) = (UNIV::'a star set)" 

389 
by (transfer UNIV_def, rule refl) 

390 

391 
lemma starset_empty: "*s* {} = {}" 

392 
by (transfer empty_def, rule refl) 

393 

394 
lemma starset_insert: "*s* (insert x A) = insert (star_of x) ( *s* A)" 

395 
by (transfer insert_def Un_def, rule refl) 

396 

397 
lemma starset_Un: "*s* (A \<union> B) = *s* A \<union> *s* B" 

398 
by (transfer Un_def, rule refl) 

399 

400 
lemma starset_Int: "*s* (A \<inter> B) = *s* A \<inter> *s* B" 

401 
by (transfer Int_def, rule refl) 

402 

403 
lemma starset_Compl: "*s* A = ( *s* A)" 

404 
by (transfer Compl_eq, rule refl) 

405 

406 
lemma starset_diff: "*s* (A  B) = *s* A  *s* B" 

407 
by (transfer set_diff_eq, rule refl) 

408 

409 
lemma starset_image: "*s* (f ` A) = ( *f* f) ` ( *s* A)" 

410 
by (transfer image_def, rule refl) 

411 

412 
lemma starset_vimage: "*s* (f ` A) = ( *f* f) ` ( *s* A)" 

413 
by (transfer vimage_def, rule refl) 

414 

415 
lemma starset_subset: "( *s* A \<subseteq> *s* B) = (A \<subseteq> B)" 

416 
by (transfer subset_eq, rule refl) 

417 

418 
lemma starset_eq: "( *s* A = *s* B) = (A = B)" 

419 
by (transfer, rule refl) 

420 

421 
lemmas starset_simps [simp] = 

422 
starset_mem starset_UNIV 

423 
starset_empty starset_insert 

424 
starset_Un starset_Int 

425 
starset_Compl starset_diff 

426 
starset_image starset_vimage 

427 
starset_subset starset_eq 

428 

429 

430 
subsection {* Syntactic classes *} 

431 

432 
instantiation star :: (zero) zero 

433 
begin 

434 

435 
definition 

37765  436 
star_zero_def: "0 \<equiv> star_of 0" 
27468  437 

438 
instance .. 

439 

440 
end 

441 

442 
instantiation star :: (one) one 

443 
begin 

444 

445 
definition 

37765  446 
star_one_def: "1 \<equiv> star_of 1" 
27468  447 

448 
instance .. 

449 

450 
end 

451 

452 
instantiation star :: (plus) plus 

453 
begin 

454 

455 
definition 

37765  456 
star_add_def: "(op +) \<equiv> *f2* (op +)" 
27468  457 

458 
instance .. 

459 

460 
end 

461 

462 
instantiation star :: (times) times 

463 
begin 

464 

465 
definition 

37765  466 
star_mult_def: "(op *) \<equiv> *f2* (op *)" 
27468  467 

468 
instance .. 

469 

470 
end 

471 

472 
instantiation star :: (uminus) uminus 

473 
begin 

474 

475 
definition 

37765  476 
star_minus_def: "uminus \<equiv> *f* uminus" 
27468  477 

478 
instance .. 

479 

480 
end 

481 

482 
instantiation star :: (minus) minus 

483 
begin 

484 

485 
definition 

37765  486 
star_diff_def: "(op ) \<equiv> *f2* (op )" 
27468  487 

488 
instance .. 

489 

490 
end 

491 

492 
instantiation star :: (abs) abs 

493 
begin 

494 

495 
definition 

496 
star_abs_def: "abs \<equiv> *f* abs" 

497 

498 
instance .. 

499 

500 
end 

501 

502 
instantiation star :: (sgn) sgn 

503 
begin 

504 

505 
definition 

506 
star_sgn_def: "sgn \<equiv> *f* sgn" 

507 

508 
instance .. 

509 

510 
end 

511 

512 
instantiation star :: (inverse) inverse 

513 
begin 

514 

515 
definition 

516 
star_divide_def: "(op /) \<equiv> *f2* (op /)" 

517 

518 
definition 

519 
star_inverse_def: "inverse \<equiv> *f* inverse" 

520 

521 
instance .. 

522 

523 
end 

524 

35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35043
diff
changeset

525 
instance star :: (Rings.dvd) Rings.dvd .. 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27468
diff
changeset

526 

27468  527 
instantiation star :: (Divides.div) Divides.div 
528 
begin 

529 

530 
definition 

531 
star_div_def: "(op div) \<equiv> *f2* (op div)" 

532 

533 
definition 

534 
star_mod_def: "(op mod) \<equiv> *f2* (op mod)" 

535 

536 
instance .. 

537 

538 
end 

539 

540 
instantiation star :: (ord) ord 

541 
begin 

542 

543 
definition 

544 
star_le_def: "(op \<le>) \<equiv> *p2* (op \<le>)" 

545 

546 
definition 

547 
star_less_def: "(op <) \<equiv> *p2* (op <)" 

548 

549 
instance .. 

550 

551 
end 

552 

553 
lemmas star_class_defs [transfer_unfold] = 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

554 
star_zero_def star_one_def 
27468  555 
star_add_def star_diff_def star_minus_def 
556 
star_mult_def star_divide_def star_inverse_def 

557 
star_le_def star_less_def star_abs_def star_sgn_def 

30968
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30729
diff
changeset

558 
star_div_def star_mod_def 
27468  559 

560 
text {* Class operations preserve standard elements *} 

561 

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

563 
by (simp add: star_zero_def) 

564 

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

566 
by (simp add: star_one_def) 

567 

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

569 
by (simp add: star_add_def) 

570 

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

572 
by (simp add: star_diff_def) 

573 

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

575 
by (simp add: star_minus_def) 

576 

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

578 
by (simp add: star_mult_def) 

579 

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

581 
by (simp add: star_divide_def) 

582 

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

584 
by (simp add: star_inverse_def) 

585 

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

587 
by (simp add: star_abs_def) 

588 

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

590 
by (simp add: star_div_def) 

591 

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

593 
by (simp add: star_mod_def) 

594 

595 
lemmas Standard_simps [simp] = 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

596 
Standard_zero Standard_one 
27468  597 
Standard_add Standard_diff Standard_minus 
598 
Standard_mult Standard_divide Standard_inverse 

599 
Standard_abs Standard_div Standard_mod 

600 

601 
text {* @{term star_of} preserves class operations *} 

602 

603 
lemma star_of_add: "star_of (x + y) = star_of x + star_of y" 

604 
by transfer (rule refl) 

605 

606 
lemma star_of_diff: "star_of (x  y) = star_of x  star_of y" 

607 
by transfer (rule refl) 

608 

609 
lemma star_of_minus: "star_of (x) =  star_of x" 

610 
by transfer (rule refl) 

611 

612 
lemma star_of_mult: "star_of (x * y) = star_of x * star_of y" 

613 
by transfer (rule refl) 

614 

615 
lemma star_of_divide: "star_of (x / y) = star_of x / star_of y" 

616 
by transfer (rule refl) 

617 

618 
lemma star_of_inverse: "star_of (inverse x) = inverse (star_of x)" 

619 
by transfer (rule refl) 

620 

621 
lemma star_of_div: "star_of (x div y) = star_of x div star_of y" 

622 
by transfer (rule refl) 

623 

624 
lemma star_of_mod: "star_of (x mod y) = star_of x mod star_of y" 

625 
by transfer (rule refl) 

626 

627 
lemma star_of_abs: "star_of (abs x) = abs (star_of x)" 

628 
by transfer (rule refl) 

629 

630 
text {* @{term star_of} preserves numerals *} 

631 

632 
lemma star_of_zero: "star_of 0 = 0" 

633 
by transfer (rule refl) 

634 

635 
lemma star_of_one: "star_of 1 = 1" 

636 
by transfer (rule refl) 

637 

638 
text {* @{term star_of} preserves orderings *} 

639 

640 
lemma star_of_less: "(star_of x < star_of y) = (x < y)" 

641 
by transfer (rule refl) 

642 

643 
lemma star_of_le: "(star_of x \<le> star_of y) = (x \<le> y)" 

644 
by transfer (rule refl) 

645 

646 
lemma star_of_eq: "(star_of x = star_of y) = (x = y)" 

647 
by transfer (rule refl) 

648 

649 
text{*As above, for 0*} 

650 

651 
lemmas star_of_0_less = star_of_less [of 0, simplified star_of_zero] 

652 
lemmas star_of_0_le = star_of_le [of 0, simplified star_of_zero] 

653 
lemmas star_of_0_eq = star_of_eq [of 0, simplified star_of_zero] 

654 

655 
lemmas star_of_less_0 = star_of_less [of _ 0, simplified star_of_zero] 

656 
lemmas star_of_le_0 = star_of_le [of _ 0, simplified star_of_zero] 

657 
lemmas star_of_eq_0 = star_of_eq [of _ 0, simplified star_of_zero] 

658 

659 
text{*As above, for 1*} 

660 

661 
lemmas star_of_1_less = star_of_less [of 1, simplified star_of_one] 

662 
lemmas star_of_1_le = star_of_le [of 1, simplified star_of_one] 

663 
lemmas star_of_1_eq = star_of_eq [of 1, simplified star_of_one] 

664 

665 
lemmas star_of_less_1 = star_of_less [of _ 1, simplified star_of_one] 

666 
lemmas star_of_le_1 = star_of_le [of _ 1, simplified star_of_one] 

667 
lemmas star_of_eq_1 = star_of_eq [of _ 1, simplified star_of_one] 

668 

669 
lemmas star_of_simps [simp] = 

670 
star_of_add star_of_diff star_of_minus 

671 
star_of_mult star_of_divide star_of_inverse 

30968
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30729
diff
changeset

672 
star_of_div star_of_mod star_of_abs 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

673 
star_of_zero star_of_one 
27468  674 
star_of_less star_of_le star_of_eq 
675 
star_of_0_less star_of_0_le star_of_0_eq 

676 
star_of_less_0 star_of_le_0 star_of_eq_0 

677 
star_of_1_less star_of_1_le star_of_1_eq 

678 
star_of_less_1 star_of_le_1 star_of_eq_1 

679 

680 
subsection {* Ordering and lattice classes *} 

681 

682 
instance star :: (order) order 

683 
apply (intro_classes) 

27682  684 
apply (transfer, rule less_le_not_le) 
27468  685 
apply (transfer, rule order_refl) 
686 
apply (transfer, erule (1) order_trans) 

687 
apply (transfer, erule (1) order_antisym) 

688 
done 

689 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
31021
diff
changeset

690 
instantiation star :: (semilattice_inf) semilattice_inf 
27468  691 
begin 
692 

693 
definition 

694 
star_inf_def [transfer_unfold]: "inf \<equiv> *f2* inf" 

695 

696 
instance 

697 
by default (transfer star_inf_def, auto)+ 

698 

699 
end 

700 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
31021
diff
changeset

701 
instantiation star :: (semilattice_sup) semilattice_sup 
27468  702 
begin 
703 

704 
definition 

705 
star_sup_def [transfer_unfold]: "sup \<equiv> *f2* sup" 

706 

707 
instance 

708 
by default (transfer star_sup_def, auto)+ 

709 

710 
end 

711 

712 
instance star :: (lattice) lattice .. 

713 

714 
instance star :: (distrib_lattice) distrib_lattice 

715 
by default (transfer, auto simp add: sup_inf_distrib1) 

716 

717 
lemma Standard_inf [simp]: 

718 
"\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> inf x y \<in> Standard" 

719 
by (simp add: star_inf_def) 

720 

721 
lemma Standard_sup [simp]: 

722 
"\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> sup x y \<in> Standard" 

723 
by (simp add: star_sup_def) 

724 

725 
lemma star_of_inf [simp]: "star_of (inf x y) = inf (star_of x) (star_of y)" 

726 
by transfer (rule refl) 

727 

728 
lemma star_of_sup [simp]: "star_of (sup x y) = sup (star_of x) (star_of y)" 

729 
by transfer (rule refl) 

730 

731 
instance star :: (linorder) linorder 

732 
by (intro_classes, transfer, rule linorder_linear) 

733 

734 
lemma star_max_def [transfer_unfold]: "max = *f2* max" 

735 
apply (rule ext, rule ext) 

736 
apply (unfold max_def, transfer, fold max_def) 

737 
apply (rule refl) 

738 
done 

739 

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

741 
apply (rule ext, rule ext) 

742 
apply (unfold min_def, transfer, fold min_def) 

743 
apply (rule refl) 

744 
done 

745 

746 
lemma Standard_max [simp]: 

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

748 
by (simp add: star_max_def) 

749 

750 
lemma Standard_min [simp]: 

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

752 
by (simp add: star_min_def) 

753 

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

755 
by transfer (rule refl) 

756 

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

758 
by transfer (rule refl) 

759 

760 

761 
subsection {* Ordered group classes *} 

762 

763 
instance star :: (semigroup_add) semigroup_add 

764 
by (intro_classes, transfer, rule add_assoc) 

765 

766 
instance star :: (ab_semigroup_add) ab_semigroup_add 

767 
by (intro_classes, transfer, rule add_commute) 

768 

769 
instance star :: (semigroup_mult) semigroup_mult 

770 
by (intro_classes, transfer, rule mult_assoc) 

771 

772 
instance star :: (ab_semigroup_mult) ab_semigroup_mult 

773 
by (intro_classes, transfer, rule mult_commute) 

774 

775 
instance star :: (comm_monoid_add) comm_monoid_add 

28059  776 
by (intro_classes, transfer, rule comm_monoid_add_class.add_0) 
27468  777 

778 
instance star :: (monoid_mult) monoid_mult 

779 
apply (intro_classes) 

780 
apply (transfer, rule mult_1_left) 

781 
apply (transfer, rule mult_1_right) 

782 
done 

783 

784 
instance star :: (comm_monoid_mult) comm_monoid_mult 

785 
by (intro_classes, transfer, rule mult_1) 

786 

787 
instance star :: (cancel_semigroup_add) cancel_semigroup_add 

788 
apply (intro_classes) 

789 
apply (transfer, erule add_left_imp_eq) 

790 
apply (transfer, erule add_right_imp_eq) 

791 
done 

792 

793 
instance star :: (cancel_ab_semigroup_add) cancel_ab_semigroup_add 

794 
by (intro_classes, transfer, rule add_imp_eq) 

795 

29904  796 
instance star :: (cancel_comm_monoid_add) cancel_comm_monoid_add .. 
797 

27468  798 
instance star :: (ab_group_add) ab_group_add 
799 
apply (intro_classes) 

800 
apply (transfer, rule left_minus) 

801 
apply (transfer, rule diff_minus) 

802 
done 

803 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
31021
diff
changeset

804 
instance star :: (ordered_ab_semigroup_add) ordered_ab_semigroup_add 
27468  805 
by (intro_classes, transfer, rule add_left_mono) 
806 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
31021
diff
changeset

807 
instance star :: (ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add .. 
27468  808 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
31021
diff
changeset

809 
instance star :: (ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le 
27468  810 
by (intro_classes, transfer, rule add_le_imp_le_left) 
811 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
31021
diff
changeset

812 
instance star :: (ordered_comm_monoid_add) ordered_comm_monoid_add .. 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
31021
diff
changeset

813 
instance star :: (ordered_ab_group_add) ordered_ab_group_add .. 
27468  814 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
31021
diff
changeset

815 
instance star :: (ordered_ab_group_add_abs) ordered_ab_group_add_abs 
27468  816 
by intro_classes (transfer, 
817 
simp add: abs_ge_self abs_leI abs_triangle_ineq)+ 

818 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
31021
diff
changeset

819 
instance star :: (linordered_cancel_ab_semigroup_add) linordered_cancel_ab_semigroup_add .. 
27468  820 

821 

822 
subsection {* Ring and field classes *} 

823 

824 
instance star :: (semiring) semiring 

825 
apply (intro_classes) 

826 
apply (transfer, rule left_distrib) 

827 
apply (transfer, rule right_distrib) 

828 
done 

829 

830 
instance star :: (semiring_0) semiring_0 

831 
by intro_classes (transfer, simp)+ 

832 

833 
instance star :: (semiring_0_cancel) semiring_0_cancel .. 

834 

835 
instance star :: (comm_semiring) comm_semiring 

836 
by (intro_classes, transfer, rule left_distrib) 

837 

838 
instance star :: (comm_semiring_0) comm_semiring_0 .. 

839 
instance star :: (comm_semiring_0_cancel) comm_semiring_0_cancel .. 

840 

841 
instance star :: (zero_neq_one) zero_neq_one 

842 
by (intro_classes, transfer, rule zero_neq_one) 

843 

844 
instance star :: (semiring_1) semiring_1 .. 

845 
instance star :: (comm_semiring_1) comm_semiring_1 .. 

846 

847 
instance star :: (no_zero_divisors) no_zero_divisors 

848 
by (intro_classes, transfer, rule no_zero_divisors) 

849 

850 
instance star :: (semiring_1_cancel) semiring_1_cancel .. 

851 
instance star :: (comm_semiring_1_cancel) comm_semiring_1_cancel .. 

852 
instance star :: (ring) ring .. 

853 
instance star :: (comm_ring) comm_ring .. 

854 
instance star :: (ring_1) ring_1 .. 

855 
instance star :: (comm_ring_1) comm_ring_1 .. 

856 
instance star :: (ring_no_zero_divisors) ring_no_zero_divisors .. 

857 
instance star :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors .. 

858 
instance star :: (idom) idom .. 

859 

860 
instance star :: (division_ring) division_ring 

861 
apply (intro_classes) 

862 
apply (transfer, erule left_inverse) 

863 
apply (transfer, erule right_inverse) 

35083  864 
apply (transfer, fact divide_inverse) 
27468  865 
done 
866 

36412  867 
instance star :: (division_ring_inverse_zero) division_ring_inverse_zero 
868 
by (intro_classes, transfer, rule inverse_zero) 

869 

27468  870 
instance star :: (field) field 
871 
apply (intro_classes) 

872 
apply (transfer, erule left_inverse) 

873 
apply (transfer, rule divide_inverse) 

874 
done 

875 

36412  876 
instance star :: (field_inverse_zero) field_inverse_zero 
877 
apply intro_classes 

878 
apply (rule inverse_zero) 

879 
done 

27468  880 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
31021
diff
changeset

881 
instance star :: (ordered_semiring) ordered_semiring 
27468  882 
apply (intro_classes) 
883 
apply (transfer, erule (1) mult_left_mono) 

884 
apply (transfer, erule (1) mult_right_mono) 

885 
done 

886 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
31021
diff
changeset

887 
instance star :: (ordered_cancel_semiring) ordered_cancel_semiring .. 
27468  888 

35043
07dbdf60d5ad
dropped accidental duplication of "lin" prefix from cs. 108662d50512
haftmann
parents:
35035
diff
changeset

889 
instance star :: (linordered_semiring_strict) linordered_semiring_strict 
27468  890 
apply (intro_classes) 
891 
apply (transfer, erule (1) mult_strict_left_mono) 

892 
apply (transfer, erule (1) mult_strict_right_mono) 

893 
done 

894 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
31021
diff
changeset

895 
instance star :: (ordered_comm_semiring) ordered_comm_semiring 
38642
8fa437809c67
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents:
38621
diff
changeset

896 
by (intro_classes, transfer, rule mult_left_mono) 
27468  897 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
31021
diff
changeset

898 
instance star :: (ordered_cancel_comm_semiring) ordered_cancel_comm_semiring .. 
27468  899 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
31021
diff
changeset

900 
instance star :: (linordered_comm_semiring_strict) linordered_comm_semiring_strict 
38642
8fa437809c67
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents:
38621
diff
changeset

901 
by (intro_classes, transfer, rule mult_strict_left_mono) 
27468  902 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
31021
diff
changeset

903 
instance star :: (ordered_ring) ordered_ring .. 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
31021
diff
changeset

904 
instance star :: (ordered_ring_abs) ordered_ring_abs 
27468  905 
by intro_classes (transfer, rule abs_eq_mult) 
906 

907 
instance star :: (abs_if) abs_if 

908 
by (intro_classes, transfer, rule abs_if) 

909 

910 
instance star :: (sgn_if) sgn_if 

911 
by (intro_classes, transfer, rule sgn_if) 

912 

35043
07dbdf60d5ad
dropped accidental duplication of "lin" prefix from cs. 108662d50512
haftmann
parents:
35035
diff
changeset

913 
instance star :: (linordered_ring_strict) linordered_ring_strict .. 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
31021
diff
changeset

914 
instance star :: (ordered_comm_ring) ordered_comm_ring .. 
27468  915 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
31021
diff
changeset

916 
instance star :: (linordered_semidom) linordered_semidom 
27468  917 
by (intro_classes, transfer, rule zero_less_one) 
918 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
31021
diff
changeset

919 
instance star :: (linordered_idom) linordered_idom .. 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
31021
diff
changeset

920 
instance star :: (linordered_field) linordered_field .. 
36414  921 
instance star :: (linordered_field_inverse_zero) linordered_field_inverse_zero .. 
27468  922 

30968
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30729
diff
changeset

923 

10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30729
diff
changeset

924 
subsection {* Power *} 
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30729
diff
changeset

925 

10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30729
diff
changeset

926 
lemma star_power_def [transfer_unfold]: 
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30729
diff
changeset

927 
"(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x" 
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30729
diff
changeset

928 
proof (rule eq_reflection, rule ext, rule ext) 
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30729
diff
changeset

929 
fix n :: nat 
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30729
diff
changeset

930 
show "\<And>x::'a star. x ^ n = ( *f* (\<lambda>x. x ^ n)) x" 
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30729
diff
changeset

931 
proof (induct n) 
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30729
diff
changeset

932 
case 0 
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30729
diff
changeset

933 
have "\<And>x::'a star. ( *f* (\<lambda>x. 1)) x = 1" 
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30729
diff
changeset

934 
by transfer simp 
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30729
diff
changeset

935 
then show ?case by simp 
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30729
diff
changeset

936 
next 
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30729
diff
changeset

937 
case (Suc n) 
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30729
diff
changeset

938 
have "\<And>x::'a star. x * ( *f* (\<lambda>x\<Colon>'a. x ^ n)) x = ( *f* (\<lambda>x\<Colon>'a. x * x ^ n)) x" 
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30729
diff
changeset

939 
by transfer simp 
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30729
diff
changeset

940 
with Suc show ?case by simp 
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30729
diff
changeset

941 
qed 
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30729
diff
changeset

942 
qed 
27468  943 

30968
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30729
diff
changeset

944 
lemma Standard_power [simp]: "x \<in> Standard \<Longrightarrow> x ^ n \<in> Standard" 
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30729
diff
changeset

945 
by (simp add: star_power_def) 
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30729
diff
changeset

946 

10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30729
diff
changeset

947 
lemma star_of_power [simp]: "star_of (x ^ n) = star_of x ^ n" 
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30729
diff
changeset

948 
by transfer (rule refl) 
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30729
diff
changeset

949 

27468  950 

951 
subsection {* Number classes *} 

952 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

953 
instance star :: (numeral) numeral .. 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

954 

2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

955 
lemma star_numeral_def [transfer_unfold]: 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

956 
"numeral k = star_of (numeral k)" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

957 
by (induct k, simp_all only: numeral.simps star_of_one star_of_add) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

958 

2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

959 
lemma Standard_numeral [simp]: "numeral k \<in> Standard" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

960 
by (simp add: star_numeral_def) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

961 

2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

962 
lemma star_of_numeral [simp]: "star_of (numeral k) = numeral k" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

963 
by transfer (rule refl) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

964 

2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

965 
lemma star_neg_numeral_def [transfer_unfold]: 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

966 
"neg_numeral k = star_of (neg_numeral k)" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

967 
by (simp only: neg_numeral_def star_of_minus star_of_numeral) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

968 

2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

969 
lemma Standard_neg_numeral [simp]: "neg_numeral k \<in> Standard" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

970 
by (simp add: star_neg_numeral_def) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

971 

2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

972 
lemma star_of_neg_numeral [simp]: "star_of (neg_numeral k) = neg_numeral k" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

973 
by transfer (rule refl) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

974 

27468  975 
lemma star_of_nat_def [transfer_unfold]: "of_nat n = star_of (of_nat n)" 
976 
by (induct n, simp_all) 

977 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

978 
lemmas star_of_compare_numeral [simp] = 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

979 
star_of_less [of "numeral k", simplified star_of_numeral] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

980 
star_of_le [of "numeral k", simplified star_of_numeral] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

981 
star_of_eq [of "numeral k", simplified star_of_numeral] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

982 
star_of_less [of _ "numeral k", simplified star_of_numeral] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

983 
star_of_le [of _ "numeral k", simplified star_of_numeral] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

984 
star_of_eq [of _ "numeral k", simplified star_of_numeral] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

985 
star_of_less [of "neg_numeral k", simplified star_of_numeral] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

986 
star_of_le [of "neg_numeral k", simplified star_of_numeral] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

987 
star_of_eq [of "neg_numeral k", simplified star_of_numeral] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

988 
star_of_less [of _ "neg_numeral k", simplified star_of_numeral] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

989 
star_of_le [of _ "neg_numeral k", simplified star_of_numeral] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

990 
star_of_eq [of _ "neg_numeral k", simplified star_of_numeral] for k 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46008
diff
changeset

991 

27468  992 
lemma Standard_of_nat [simp]: "of_nat n \<in> Standard" 
993 
by (simp add: star_of_nat_def) 

994 

995 
lemma star_of_of_nat [simp]: "star_of (of_nat n) = of_nat n" 

996 
by transfer (rule refl) 

997 

998 
lemma star_of_int_def [transfer_unfold]: "of_int z = star_of (of_int z)" 

999 
by (rule_tac z=z in int_diff_cases, simp) 

1000 

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

1002 
by (simp add: star_of_int_def) 

1003 

1004 
lemma star_of_of_int [simp]: "star_of (of_int z) = of_int z" 

1005 
by transfer (rule refl) 

1006 

38621
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37765
diff
changeset

1007 
instance star :: (semiring_char_0) semiring_char_0 proof 
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37765
diff
changeset

1008 
have "inj (star_of :: 'a \<Rightarrow> 'a star)" by (rule injI) simp 
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37765
diff
changeset

1009 
then have "inj (star_of \<circ> of_nat :: nat \<Rightarrow> 'a star)" using inj_of_nat by (rule inj_comp) 
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37765
diff
changeset

1010 
then show "inj (of_nat :: nat \<Rightarrow> 'a star)" by (simp add: comp_def) 
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37765
diff
changeset

1011 
qed 
27468  1012 

1013 
instance star :: (ring_char_0) ring_char_0 .. 

1014 

1015 

1016 
subsection {* Finite class *} 

1017 

1018 
lemma starset_finite: "finite A \<Longrightarrow> *s* A = star_of ` A" 

1019 
by (erule finite_induct, simp_all) 

1020 

1021 
instance star :: (finite) finite 

1022 
apply (intro_classes) 

1023 
apply (subst starset_UNIV [symmetric]) 

1024 
apply (subst starset_finite [OF finite]) 

1025 
apply (rule finite_imageI [OF finite]) 

1026 
done 

1027 

1028 
end 