1(* Title: HOL/Nonstandard_Analysis/StarDef.thy 2 Author: Jacques D. Fleuriot and Brian Huffman 3*) 4 5section \<open>Construction of Star Types Using Ultrafilters\<close> 6 7theory StarDef 8 imports Free_Ultrafilter 9begin 10 11subsection \<open>A Free Ultrafilter over the Naturals\<close> 12 13definition FreeUltrafilterNat :: "nat filter" (\<open>\<U>\<close>) 14 where "\<U> = (SOME U. freeultrafilter U)" 15 16lemma freeultrafilter_FreeUltrafilterNat: "freeultrafilter \<U>" 17 unfolding FreeUltrafilterNat_def 18 by (simp add: freeultrafilter_Ex someI_ex) 19 20interpretation FreeUltrafilterNat: freeultrafilter \<U> 21 by (rule freeultrafilter_FreeUltrafilterNat) 22 23 24subsection \<open>Definition of \<open>star\<close> type constructor\<close> 25 26definition starrel :: "((nat \<Rightarrow> 'a) \<times> (nat \<Rightarrow> 'a)) set" 27 where "starrel = {(X, Y). eventually (\<lambda>n. X n = Y n) \<U>}" 28 29definition "star = (UNIV :: (nat \<Rightarrow> 'a) set) // starrel" 30 31typedef 'a star = "star :: (nat \<Rightarrow> 'a) set set" 32 by (auto simp: star_def intro: quotientI) 33 34definition star_n :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a star" 35 where "star_n X = Abs_star (starrel `` {X})" 36 37theorem star_cases [case_names star_n, cases type: star]: 38 obtains X where "x = star_n X" 39 by (cases x) (auto simp: star_n_def star_def elim: quotientE) 40 41lemma all_star_eq: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>X. P (star_n X))" 42 by (metis star_cases) 43 44lemma ex_star_eq: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>X. P (star_n X))" 45 by (metis star_cases) 46 47text \<open>Proving that \<^term>\<open>starrel\<close> is an equivalence relation.\<close> 48 49lemma starrel_iff [iff]: "(X, Y) \<in> starrel \<longleftrightarrow> eventually (\<lambda>n. X n = Y n) \<U>" 50 by (simp add: starrel_def) 51 52lemma equiv_starrel: "equiv UNIV starrel" 53proof (rule equivI) 54 show "refl starrel" by (simp add: refl_on_def) 55 show "sym starrel" by (simp add: sym_def eq_commute) 56 show "trans starrel" by (intro transI) (auto elim: eventually_elim2) 57qed 58 59lemmas equiv_starrel_iff = eq_equiv_class_iff [OF equiv_starrel UNIV_I UNIV_I] 60 61lemma starrel_in_star: "starrel``{x} \<in> star" 62 by (simp add: star_def quotientI) 63 64lemma star_n_eq_iff: "star_n X = star_n Y \<longleftrightarrow> eventually (\<lambda>n. X n = Y n) \<U>" 65 by (simp add: star_n_def Abs_star_inject starrel_in_star equiv_starrel_iff) 66 67 68subsection \<open>Transfer principle\<close> 69 70text \<open>This introduction rule starts each transfer proof.\<close> 71lemma transfer_start: "P \<equiv> eventually (\<lambda>n. Q) \<U> \<Longrightarrow> Trueprop P \<equiv> Trueprop Q" 72 by (simp add: FreeUltrafilterNat.proper) 73 74text \<open>Standard principles that play a central role in the transfer tactic.\<close> 75definition Ifun :: "('a \<Rightarrow> 'b) star \<Rightarrow> 'a star \<Rightarrow> 'b star" (\<open>(_ \<star>/ _)\<close> [300, 301] 300) 76 where "Ifun f \<equiv> 77 \<lambda>x. Abs_star (\<Union>F\<in>Rep_star f. \<Union>X\<in>Rep_star x. starrel``{\<lambda>n. F n (X n)})" 78 79lemma Ifun_congruent2: "congruent2 starrel starrel (\<lambda>F X. starrel``{\<lambda>n. F n (X n)})" 80 by (auto simp add: congruent2_def equiv_starrel_iff elim!: eventually_rev_mp) 81 82lemma Ifun_star_n: "star_n F \<star> star_n X = star_n (\<lambda>n. F n (X n))" 83 by (simp add: Ifun_def star_n_def Abs_star_inverse starrel_in_star 84 UN_equiv_class2 [OF equiv_starrel equiv_starrel Ifun_congruent2]) 85 86lemma transfer_Ifun: "f \<equiv> star_n F \<Longrightarrow> x \<equiv> star_n X \<Longrightarrow> f \<star> x \<equiv> star_n (\<lambda>n. F n (X n))" 87 by (simp only: Ifun_star_n) 88 89definition star_of :: "'a \<Rightarrow> 'a star" 90 where "star_of x \<equiv> star_n (\<lambda>n. x)" 91 92text \<open>Initialize transfer tactic.\<close> 93ML_file \<open>transfer_principle.ML\<close> 94 95method_setup transfer = 96 \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (Transfer_Principle.transfer_tac ctxt ths))\<close> 97 "transfer principle" 98 99 100text \<open>Transfer introduction rules.\<close> 101 102lemma transfer_ex [transfer_intro]: 103 "(\<And>X. p (star_n X) \<equiv> eventually (\<lambda>n. P n (X n)) \<U>) \<Longrightarrow> 104 \<exists>x::'a star. p x \<equiv> eventually (\<lambda>n. \<exists>x. P n x) \<U>" 105 by (simp only: ex_star_eq eventually_ex) 106 107lemma transfer_all [transfer_intro]: 108 "(\<And>X. p (star_n X) \<equiv> eventually (\<lambda>n. P n (X n)) \<U>) \<Longrightarrow> 109 \<forall>x::'a star. p x \<equiv> eventually (\<lambda>n. \<forall>x. P n x) \<U>" 110 by (simp only: all_star_eq FreeUltrafilterNat.eventually_all_iff) 111 112lemma transfer_not [transfer_intro]: "p \<equiv> eventually P \<U> \<Longrightarrow> \<not> p \<equiv> eventually (\<lambda>n. \<not> P n) \<U>" 113 by (simp only: FreeUltrafilterNat.eventually_not_iff) 114 115lemma transfer_conj [transfer_intro]: 116 "p \<equiv> eventually P \<U> \<Longrightarrow> q \<equiv> eventually Q \<U> \<Longrightarrow> p \<and> q \<equiv> eventually (\<lambda>n. P n \<and> Q n) \<U>" 117 by (simp only: eventually_conj_iff) 118 119lemma transfer_disj [transfer_intro]: 120 "p \<equiv> eventually P \<U> \<Longrightarrow> q \<equiv> eventually Q \<U> \<Longrightarrow> p \<or> q \<equiv> eventually (\<lambda>n. P n \<or> Q n) \<U>" 121 by (simp only: FreeUltrafilterNat.eventually_disj_iff) 122 123lemma transfer_imp [transfer_intro]: 124 "p \<equiv> eventually P \<U> \<Longrightarrow> q \<equiv> eventually Q \<U> \<Longrightarrow> p \<longrightarrow> q \<equiv> eventually (\<lambda>n. P n \<longrightarrow> Q n) \<U>" 125 by (simp only: FreeUltrafilterNat.eventually_imp_iff) 126 127lemma transfer_iff [transfer_intro]: 128 "p \<equiv> eventually P \<U> \<Longrightarrow> q \<equiv> eventually Q \<U> \<Longrightarrow> p = q \<equiv> eventually (\<lambda>n. P n = Q n) \<U>" 129 by (simp only: FreeUltrafilterNat.eventually_iff_iff) 130 131lemma transfer_if_bool [transfer_intro]: 132 "p \<equiv> eventually P \<U> \<Longrightarrow> x \<equiv> eventually X \<U> \<Longrightarrow> y \<equiv> eventually Y \<U> \<Longrightarrow> 133 (if p then x else y) \<equiv> eventually (\<lambda>n. if P n then X n else Y n) \<U>" 134 by (simp only: if_bool_eq_conj transfer_conj transfer_imp transfer_not) 135 136lemma transfer_eq [transfer_intro]: 137 "x \<equiv> star_n X \<Longrightarrow> y \<equiv> star_n Y \<Longrightarrow> x = y \<equiv> eventually (\<lambda>n. X n = Y n) \<U>" 138 by (simp only: star_n_eq_iff) 139 140lemma transfer_if [transfer_intro]: 141 "p \<equiv> eventually (\<lambda>n. P n) \<U> \<Longrightarrow> x \<equiv> star_n X \<Longrightarrow> y \<equiv> star_n Y \<Longrightarrow> 142 (if p then x else y) \<equiv> star_n (\<lambda>n. if P n then X n else Y n)" 143 by (rule eq_reflection) (auto simp: star_n_eq_iff transfer_not elim!: eventually_mono) 144 145lemma transfer_fun_eq [transfer_intro]: 146 "(\<And>X. f (star_n X) = g (star_n X) \<equiv> eventually (\<lambda>n. F n (X n) = G n (X n)) \<U>) \<Longrightarrow> 147 f = g \<equiv> eventually (\<lambda>n. F n = G n) \<U>" 148 by (simp only: fun_eq_iff transfer_all) 149 150lemma transfer_star_n [transfer_intro]: "star_n X \<equiv> star_n (\<lambda>n. X n)" 151 by (rule reflexive) 152 153lemma transfer_bool [transfer_intro]: "p \<equiv> eventually (\<lambda>n. p) \<U>" 154 by (simp add: FreeUltrafilterNat.proper) 155 156 157subsection \<open>Standard elements\<close> 158 159definition Standard :: "'a star set" 160 where "Standard = range star_of" 161 162text \<open>Transfer tactic should remove occurrences of \<^term>\<open>star_of\<close>.\<close> 163setup \<open>Transfer_Principle.add_const \<^const_name>\<open>star_of\<close>\<close> 164 165lemma star_of_inject: "star_of x = star_of y \<longleftrightarrow> x = y" 166 by transfer (rule refl) 167 168lemma Standard_star_of [simp]: "star_of x \<in> Standard" 169 by (simp add: Standard_def) 170 171 172subsection \<open>Internal functions\<close> 173 174text \<open>Transfer tactic should remove occurrences of \<^term>\<open>Ifun\<close>.\<close> 175setup \<open>Transfer_Principle.add_const \<^const_name>\<open>Ifun\<close>\<close> 176 177lemma Ifun_star_of [simp]: "star_of f \<star> star_of x = star_of (f x)" 178 by transfer (rule refl) 179 180lemma Standard_Ifun [simp]: "f \<in> Standard \<Longrightarrow> x \<in> Standard \<Longrightarrow> f \<star> x \<in> Standard" 181 by (auto simp add: Standard_def) 182 183 184text \<open>Nonstandard extensions of functions.\<close> 185 186definition starfun :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a star \<Rightarrow> 'b star" (\<open>*f* _\<close> [80] 80) 187 where "starfun f \<equiv> \<lambda>x. star_of f \<star> x" 188 189definition starfun2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a star \<Rightarrow> 'b star \<Rightarrow> 'c star" (\<open>*f2* _\<close> [80] 80) 190 where "starfun2 f \<equiv> \<lambda>x y. star_of f \<star> x \<star> y" 191 192declare starfun_def [transfer_unfold] 193declare starfun2_def [transfer_unfold] 194 195lemma starfun_star_n: "( *f* f) (star_n X) = star_n (\<lambda>n. f (X n))" 196 by (simp only: starfun_def star_of_def Ifun_star_n) 197 198lemma starfun2_star_n: "( *f2* f) (star_n X) (star_n Y) = star_n (\<lambda>n. f (X n) (Y n))" 199 by (simp only: starfun2_def star_of_def Ifun_star_n) 200 201lemma starfun_star_of [simp]: "( *f* f) (star_of x) = star_of (f x)" 202 by transfer (rule refl) 203 204lemma starfun2_star_of [simp]: "( *f2* f) (star_of x) = *f* f x" 205 by transfer (rule refl) 206 207lemma Standard_starfun [simp]: "x \<in> Standard \<Longrightarrow> starfun f x \<in> Standard" 208 by (simp add: starfun_def) 209 210lemma Standard_starfun2 [simp]: "x \<in> Standard \<Longrightarrow> y \<in> Standard \<Longrightarrow> starfun2 f x y \<in> Standard" 211 by (simp add: starfun2_def) 212 213lemma Standard_starfun_iff: 214 assumes inj: "\<And>x y. f x = f y \<Longrightarrow> x = y" 215 shows "starfun f x \<in> Standard \<longleftrightarrow> x \<in> Standard" 216proof 217 assume "x \<in> Standard" 218 then show "starfun f x \<in> Standard" by simp 219next 220 from inj have inj': "\<And>x y. starfun f x = starfun f y \<Longrightarrow> x = y" 221 by transfer 222 assume "starfun f x \<in> Standard" 223 then obtain b where b: "starfun f x = star_of b" 224 unfolding Standard_def .. 225 then have "\<exists>x. starfun f x = star_of b" .. 226 then have "\<exists>a. f a = b" by transfer 227 then obtain a where "f a = b" .. 228 then have "starfun f (star_of a) = star_of b" by transfer 229 with b have "starfun f x = starfun f (star_of a)" by simp 230 then have "x = star_of a" by (rule inj') 231 then show "x \<in> Standard" by (simp add: Standard_def) 232qed 233 234lemma Standard_starfun2_iff: 235 assumes inj: "\<And>a b a' b'. f a b = f a' b' \<Longrightarrow> a = a' \<and> b = b'" 236 shows "starfun2 f x y \<in> Standard \<longleftrightarrow> x \<in> Standard \<and> y \<in> Standard" 237proof 238 assume "x \<in> Standard \<and> y \<in> Standard" 239 then show "starfun2 f x y \<in> Standard" by simp 240next 241 have inj': "\<And>x y z w. starfun2 f x y = starfun2 f z w \<Longrightarrow> x = z \<and> y = w" 242 using inj by transfer 243 assume "starfun2 f x y \<in> Standard" 244 then obtain c where c: "starfun2 f x y = star_of c" 245 unfolding Standard_def .. 246 then have "\<exists>x y. starfun2 f x y = star_of c" by auto 247 then have "\<exists>a b. f a b = c" by transfer 248 then obtain a b where "f a b = c" by auto 249 then have "starfun2 f (star_of a) (star_of b) = star_of c" by transfer 250 with c have "starfun2 f x y = starfun2 f (star_of a) (star_of b)" by simp 251 then have "x = star_of a \<and> y = star_of b" by (rule inj') 252 then show "x \<in> Standard \<and> y \<in> Standard" by (simp add: Standard_def) 253qed 254 255 256subsection \<open>Internal predicates\<close> 257 258definition unstar :: "bool star \<Rightarrow> bool" 259 where "unstar b \<longleftrightarrow> b = star_of True" 260 261lemma unstar_star_n: "unstar (star_n P) \<longleftrightarrow> eventually P \<U>" 262 by (simp add: unstar_def star_of_def star_n_eq_iff) 263 264lemma unstar_star_of [simp]: "unstar (star_of p) = p" 265 by (simp add: unstar_def star_of_inject) 266 267text \<open>Transfer tactic should remove occurrences of \<^term>\<open>unstar\<close>.\<close> 268setup \<open>Transfer_Principle.add_const \<^const_name>\<open>unstar\<close>\<close> 269 270lemma transfer_unstar [transfer_intro]: "p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> eventually P \<U>" 271 by (simp only: unstar_star_n) 272 273definition starP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a star \<Rightarrow> bool" (\<open>*p* _\<close> [80] 80) 274 where "*p* P = (\<lambda>x. unstar (star_of P \<star> x))" 275 276definition starP2 :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a star \<Rightarrow> 'b star \<Rightarrow> bool" (\<open>*p2* _\<close> [80] 80) 277 where "*p2* P = (\<lambda>x y. unstar (star_of P \<star> x \<star> y))" 278 279declare starP_def [transfer_unfold] 280declare starP2_def [transfer_unfold] 281 282lemma starP_star_n: "( *p* P) (star_n X) = eventually (\<lambda>n. P (X n)) \<U>" 283 by (simp only: starP_def star_of_def Ifun_star_n unstar_star_n) 284 285lemma starP2_star_n: "( *p2* P) (star_n X) (star_n Y) = (eventually (\<lambda>n. P (X n) (Y n)) \<U>)" 286 by (simp only: starP2_def star_of_def Ifun_star_n unstar_star_n) 287 288lemma starP_star_of [simp]: "( *p* P) (star_of x) = P x" 289 by transfer (rule refl) 290 291lemma starP2_star_of [simp]: "( *p2* P) (star_of x) = *p* P x" 292 by transfer (rule refl) 293 294 295subsection \<open>Internal sets\<close> 296 297definition Iset :: "'a set star \<Rightarrow> 'a star set" 298 where "Iset A = {x. ( *p2* (\<in>)) x A}" 299 300lemma Iset_star_n: "(star_n X \<in> Iset (star_n A)) = (eventually (\<lambda>n. X n \<in> A n) \<U>)" 301 by (simp add: Iset_def starP2_star_n) 302 303text \<open>Transfer tactic should remove occurrences of \<^term>\<open>Iset\<close>.\<close> 304setup \<open>Transfer_Principle.add_const \<^const_name>\<open>Iset\<close>\<close> 305 306lemma transfer_mem [transfer_intro]: 307 "x \<equiv> star_n X \<Longrightarrow> a \<equiv> Iset (star_n A) \<Longrightarrow> x \<in> a \<equiv> eventually (\<lambda>n. X n \<in> A n) \<U>" 308 by (simp only: Iset_star_n) 309 310lemma transfer_Collect [transfer_intro]: 311 "(\<And>X. p (star_n X) \<equiv> eventually (\<lambda>n. P n (X n)) \<U>) \<Longrightarrow> 312 Collect p \<equiv> Iset (star_n (\<lambda>n. Collect (P n)))" 313 by (simp add: atomize_eq set_eq_iff all_star_eq Iset_star_n) 314 315lemma transfer_set_eq [transfer_intro]: 316 "a \<equiv> Iset (star_n A) \<Longrightarrow> b \<equiv> Iset (star_n B) \<Longrightarrow> a = b \<equiv> eventually (\<lambda>n. A n = B n) \<U>" 317 by (simp only: set_eq_iff transfer_all transfer_iff transfer_mem) 318 319lemma transfer_ball [transfer_intro]: 320 "a \<equiv> Iset (star_n A) \<Longrightarrow> (\<And>X. p (star_n X) \<equiv> eventually (\<lambda>n. P n (X n)) \<U>) \<Longrightarrow> 321 \<forall>x\<in>a. p x \<equiv> eventually (\<lambda>n. \<forall>x\<in>A n. P n x) \<U>" 322 by (simp only: Ball_def transfer_all transfer_imp transfer_mem) 323 324lemma transfer_bex [transfer_intro]: 325 "a \<equiv> Iset (star_n A) \<Longrightarrow> (\<And>X. p (star_n X) \<equiv> eventually (\<lambda>n. P n (X n)) \<U>) \<Longrightarrow> 326 \<exists>x\<in>a. p x \<equiv> eventually (\<lambda>n. \<exists>x\<in>A n. P n x) \<U>" 327 by (simp only: Bex_def transfer_ex transfer_conj transfer_mem) 328 329lemma transfer_Iset [transfer_intro]: "a \<equiv> star_n A \<Longrightarrow> Iset a \<equiv> Iset (star_n (\<lambda>n. A n))" 330 by simp 331 332 333text \<open>Nonstandard extensions of sets.\<close> 334 335definition starset :: "'a set \<Rightarrow> 'a star set" (\<open>*s* _\<close> [80] 80) 336 where "starset A = Iset (star_of A)" 337 338declare starset_def [transfer_unfold] 339 340lemma starset_mem: "star_of x \<in> *s* A \<longleftrightarrow> x \<in> A" 341 by transfer (rule refl) 342 343lemma starset_UNIV: "*s* (UNIV::'a set) = (UNIV::'a star set)" 344 by (transfer UNIV_def) (rule refl) 345 346lemma starset_empty: "*s* {} = {}" 347 by (transfer empty_def) (rule refl) 348 349lemma starset_insert: "*s* (insert x A) = insert (star_of x) ( *s* A)" 350 by (transfer insert_def Un_def) (rule refl) 351 352lemma starset_Un: "*s* (A \<union> B) = *s* A \<union> *s* B" 353 by (transfer Un_def) (rule refl) 354 355lemma starset_Int: "*s* (A \<inter> B) = *s* A \<inter> *s* B" 356 by (transfer Int_def) (rule refl) 357 358lemma starset_Compl: "*s* -A = -( *s* A)" 359 by (transfer Compl_eq) (rule refl) 360 361lemma starset_diff: "*s* (A - B) = *s* A - *s* B" 362 by (transfer set_diff_eq) (rule refl) 363 364lemma starset_image: "*s* (f ` A) = ( *f* f) ` ( *s* A)" 365 by (transfer image_def) (rule refl) 366 367lemma starset_vimage: "*s* (f -` A) = ( *f* f) -` ( *s* A)" 368 by (transfer vimage_def) (rule refl) 369 370lemma starset_subset: "( *s* A \<subseteq> *s* B) \<longleftrightarrow> A \<subseteq> B" 371 by (transfer subset_eq) (rule refl) 372 373lemma starset_eq: "( *s* A = *s* B) \<longleftrightarrow> A = B" 374 by transfer (rule refl) 375 376lemmas starset_simps [simp] = 377 starset_mem starset_UNIV 378 starset_empty starset_insert 379 starset_Un starset_Int 380 starset_Compl starset_diff 381 starset_image starset_vimage 382 starset_subset starset_eq 383 384 385subsection \<open>Syntactic classes\<close> 386 387instantiation star :: (zero) zero 388begin 389 definition star_zero_def: "0 \<equiv> star_of 0" 390 instance .. 391end 392 393instantiation star :: (one) one 394begin 395 definition star_one_def: "1 \<equiv> star_of 1" 396 instance .. 397end 398 399instantiation star :: (plus) plus 400begin 401 definition star_add_def: "(+) \<equiv> *f2* (+)" 402 instance .. 403end 404 405instantiation star :: (times) times 406begin 407 definition star_mult_def: "((*)) \<equiv> *f2* ((*))" 408 instance .. 409end 410 411instantiation star :: (uminus) uminus 412begin 413 definition star_minus_def: "uminus \<equiv> *f* uminus" 414 instance .. 415end 416 417instantiation star :: (minus) minus 418begin 419 definition star_diff_def: "(-) \<equiv> *f2* (-)" 420 instance .. 421end 422 423instantiation star :: (abs) abs 424begin 425 definition star_abs_def: "abs \<equiv> *f* abs" 426 instance .. 427end 428 429instantiation star :: (sgn) sgn 430begin 431 definition star_sgn_def: "sgn \<equiv> *f* sgn" 432 instance .. 433end 434 435instantiation star :: (divide) divide 436begin 437 definition star_divide_def: "divide \<equiv> *f2* divide" 438 instance .. 439end 440 441instantiation star :: (inverse) inverse 442begin 443 definition star_inverse_def: "inverse \<equiv> *f* inverse" 444 instance .. 445end 446 447instance star :: (Rings.dvd) Rings.dvd .. 448 449instantiation star :: (modulo) modulo 450begin 451 definition star_mod_def: "(mod) \<equiv> *f2* (mod)" 452 instance .. 453end 454 455instantiation star :: (ord) ord 456begin 457 definition star_le_def: "(\<le>) \<equiv> *p2* (\<le>)" 458 definition star_less_def: "(<) \<equiv> *p2* (<)" 459 instance .. 460end 461 462lemmas star_class_defs [transfer_unfold] = 463 star_zero_def star_one_def 464 star_add_def star_diff_def star_minus_def 465 star_mult_def star_divide_def star_inverse_def 466 star_le_def star_less_def star_abs_def star_sgn_def 467 star_mod_def 468 469 470text \<open>Class operations preserve standard elements.\<close> 471 472lemma Standard_zero: "0 \<in> Standard" 473 by (simp add: star_zero_def) 474 475lemma Standard_one: "1 \<in> Standard" 476 by (simp add: star_one_def) 477 478lemma Standard_add: "x \<in> Standard \<Longrightarrow> y \<in> Standard \<Longrightarrow> x + y \<in> Standard" 479 by (simp add: star_add_def) 480 481lemma Standard_diff: "x \<in> Standard \<Longrightarrow> y \<in> Standard \<Longrightarrow> x - y \<in> Standard" 482 by (simp add: star_diff_def) 483 484lemma Standard_minus: "x \<in> Standard \<Longrightarrow> - x \<in> Standard" 485 by (simp add: star_minus_def) 486 487lemma Standard_mult: "x \<in> Standard \<Longrightarrow> y \<in> Standard \<Longrightarrow> x * y \<in> Standard" 488 by (simp add: star_mult_def) 489 490lemma Standard_divide: "x \<in> Standard \<Longrightarrow> y \<in> Standard \<Longrightarrow> x / y \<in> Standard" 491 by (simp add: star_divide_def) 492 493lemma Standard_inverse: "x \<in> Standard \<Longrightarrow> inverse x \<in> Standard" 494 by (simp add: star_inverse_def) 495 496lemma Standard_abs: "x \<in> Standard \<Longrightarrow> \<bar>x\<bar> \<in> Standard" 497 by (simp add: star_abs_def) 498 499lemma Standard_mod: "x \<in> Standard \<Longrightarrow> y \<in> Standard \<Longrightarrow> x mod y \<in> Standard" 500 by (simp add: star_mod_def) 501 502lemmas Standard_simps [simp] = 503 Standard_zero Standard_one 504 Standard_add Standard_diff Standard_minus 505 Standard_mult Standard_divide Standard_inverse 506 Standard_abs Standard_mod 507 508 509text \<open>\<^term>\<open>star_of\<close> preserves class operations.\<close> 510 511lemma star_of_add: "star_of (x + y) = star_of x + star_of y" 512 by transfer (rule refl) 513 514lemma star_of_diff: "star_of (x - y) = star_of x - star_of y" 515 by transfer (rule refl) 516 517lemma star_of_minus: "star_of (-x) = - star_of x" 518 by transfer (rule refl) 519 520lemma star_of_mult: "star_of (x * y) = star_of x * star_of y" 521 by transfer (rule refl) 522 523lemma star_of_divide: "star_of (x / y) = star_of x / star_of y" 524 by transfer (rule refl) 525 526lemma star_of_inverse: "star_of (inverse x) = inverse (star_of x)" 527 by transfer (rule refl) 528 529lemma star_of_mod: "star_of (x mod y) = star_of x mod star_of y" 530 by transfer (rule refl) 531 532lemma star_of_abs: "star_of \<bar>x\<bar> = \<bar>star_of x\<bar>" 533 by transfer (rule refl) 534 535 536text \<open>\<^term>\<open>star_of\<close> preserves numerals.\<close> 537 538lemma star_of_zero: "star_of 0 = 0" 539 by transfer (rule refl) 540 541lemma star_of_one: "star_of 1 = 1" 542 by transfer (rule refl) 543 544 545text \<open>\<^term>\<open>star_of\<close> preserves orderings.\<close> 546 547lemma star_of_less: "(star_of x < star_of y) = (x < y)" 548by transfer (rule refl) 549 550lemma star_of_le: "(star_of x \<le> star_of y) = (x \<le> y)" 551by transfer (rule refl) 552 553lemma star_of_eq: "(star_of x = star_of y) = (x = y)" 554by transfer (rule refl) 555 556 557text \<open>As above, for \<open>0\<close>.\<close> 558 559lemmas star_of_0_less = star_of_less [of 0, simplified star_of_zero] 560lemmas star_of_0_le = star_of_le [of 0, simplified star_of_zero] 561lemmas star_of_0_eq = star_of_eq [of 0, simplified star_of_zero] 562 563lemmas star_of_less_0 = star_of_less [of _ 0, simplified star_of_zero] 564lemmas star_of_le_0 = star_of_le [of _ 0, simplified star_of_zero] 565lemmas star_of_eq_0 = star_of_eq [of _ 0, simplified star_of_zero] 566 567 568text \<open>As above, for \<open>1\<close>.\<close> 569 570lemmas star_of_1_less = star_of_less [of 1, simplified star_of_one] 571lemmas star_of_1_le = star_of_le [of 1, simplified star_of_one] 572lemmas star_of_1_eq = star_of_eq [of 1, simplified star_of_one] 573 574lemmas star_of_less_1 = star_of_less [of _ 1, simplified star_of_one] 575lemmas star_of_le_1 = star_of_le [of _ 1, simplified star_of_one] 576lemmas star_of_eq_1 = star_of_eq [of _ 1, simplified star_of_one] 577 578lemmas star_of_simps [simp] = 579 star_of_add star_of_diff star_of_minus 580 star_of_mult star_of_divide star_of_inverse 581 star_of_mod star_of_abs 582 star_of_zero star_of_one 583 star_of_less star_of_le star_of_eq 584 star_of_0_less star_of_0_le star_of_0_eq 585 star_of_less_0 star_of_le_0 star_of_eq_0 586 star_of_1_less star_of_1_le star_of_1_eq 587 star_of_less_1 star_of_le_1 star_of_eq_1 588 589 590subsection \<open>Ordering and lattice classes\<close> 591 592instance star :: (order) order 593proof 594 show "\<And>x y::'a star. (x < y) = (x \<le> y \<and> \<not> y \<le> x)" 595 by transfer (rule less_le_not_le) 596 show "\<And>x::'a star. x \<le> x" 597 by transfer (rule order_refl) 598 show "\<And>x y z::'a star. \<lbrakk>x \<le> y; y \<le> z\<rbrakk> \<Longrightarrow> x \<le> z" 599 by transfer (rule order_trans) 600 show "\<And>x y::'a star. \<lbrakk>x \<le> y; y \<le> x\<rbrakk> \<Longrightarrow> x = y" 601 by transfer (rule order_antisym) 602qed 603 604instantiation star :: (semilattice_inf) semilattice_inf 605begin 606 definition star_inf_def [transfer_unfold]: "inf \<equiv> *f2* inf" 607 instance by (standard; transfer) auto 608end 609 610instantiation star :: (semilattice_sup) semilattice_sup 611begin 612 definition star_sup_def [transfer_unfold]: "sup \<equiv> *f2* sup" 613 instance by (standard; transfer) auto 614end 615 616instance star :: (lattice) lattice .. 617 618instance star :: (distrib_lattice) distrib_lattice 619 by (standard; transfer) (auto simp add: sup_inf_distrib1) 620 621lemma Standard_inf [simp]: "x \<in> Standard \<Longrightarrow> y \<in> Standard \<Longrightarrow> inf x y \<in> Standard" 622 by (simp add: star_inf_def) 623 624lemma Standard_sup [simp]: "x \<in> Standard \<Longrightarrow> y \<in> Standard \<Longrightarrow> sup x y \<in> Standard" 625 by (simp add: star_sup_def) 626 627lemma star_of_inf [simp]: "star_of (inf x y) = inf (star_of x) (star_of y)" 628 by transfer (rule refl) 629 630lemma star_of_sup [simp]: "star_of (sup x y) = sup (star_of x) (star_of y)" 631 by transfer (rule refl) 632 633instance star :: (linorder) linorder 634 by (intro_classes, transfer, rule linorder_linear) 635 636lemma star_max_def [transfer_unfold]: "max = *f2* max" 637 unfolding max_def 638 by (intro ext, transfer, simp) 639 640lemma star_min_def [transfer_unfold]: "min = *f2* min" 641 unfolding min_def 642 by (intro ext, transfer, simp) 643 644lemma Standard_max [simp]: "x \<in> Standard \<Longrightarrow> y \<in> Standard \<Longrightarrow> max x y \<in> Standard" 645 by (simp add: star_max_def) 646 647lemma Standard_min [simp]: "x \<in> Standard \<Longrightarrow> y \<in> Standard \<Longrightarrow> min x y \<in> Standard" 648 by (simp add: star_min_def) 649 650lemma star_of_max [simp]: "star_of (max x y) = max (star_of x) (star_of y)" 651 by transfer (rule refl) 652 653lemma star_of_min [simp]: "star_of (min x y) = min (star_of x) (star_of y)" 654 by transfer (rule refl) 655 656 657subsection \<open>Ordered group classes\<close> 658 659instance star :: (semigroup_add) semigroup_add 660 by (intro_classes, transfer, rule add.assoc) 661 662instance star :: (ab_semigroup_add) ab_semigroup_add 663 by (intro_classes, transfer, rule add.commute) 664 665instance star :: (semigroup_mult) semigroup_mult 666 by (intro_classes, transfer, rule mult.assoc) 667 668instance star :: (ab_semigroup_mult) ab_semigroup_mult 669 by (intro_classes, transfer, rule mult.commute) 670 671instance star :: (comm_monoid_add) comm_monoid_add 672 by (intro_classes, transfer, rule comm_monoid_add_class.add_0) 673 674instance star :: (monoid_mult) monoid_mult 675 apply intro_classes 676 apply (transfer, rule mult_1_left) 677 apply (transfer, rule mult_1_right) 678 done 679 680instance star :: (power) power .. 681 682instance star :: (comm_monoid_mult) comm_monoid_mult 683 by (intro_classes, transfer, rule mult_1) 684 685instance star :: (cancel_semigroup_add) cancel_semigroup_add 686 apply intro_classes 687 apply (transfer, erule add_left_imp_eq) 688 apply (transfer, erule add_right_imp_eq) 689 done 690 691instance star :: (cancel_ab_semigroup_add) cancel_ab_semigroup_add 692 by intro_classes (transfer, simp add: diff_diff_eq)+ 693 694instance star :: (cancel_comm_monoid_add) cancel_comm_monoid_add .. 695 696instance star :: (ab_group_add) ab_group_add 697 apply intro_classes 698 apply (transfer, rule left_minus) 699 apply (transfer, rule diff_conv_add_uminus) 700 done 701 702instance star :: (ordered_ab_semigroup_add) ordered_ab_semigroup_add 703 by (intro_classes, transfer, rule add_left_mono) 704 705instance star :: (ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add .. 706 707instance star :: (ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le 708 by (intro_classes, transfer, rule add_le_imp_le_left) 709 710instance star :: (ordered_comm_monoid_add) ordered_comm_monoid_add .. 711instance star :: (ordered_ab_semigroup_monoid_add_imp_le) ordered_ab_semigroup_monoid_add_imp_le .. 712instance star :: (ordered_cancel_comm_monoid_add) ordered_cancel_comm_monoid_add .. 713instance star :: (ordered_ab_group_add) ordered_ab_group_add .. 714 715instance star :: (ordered_ab_group_add_abs) ordered_ab_group_add_abs 716 by intro_classes (transfer, simp add: abs_ge_self abs_leI abs_triangle_ineq)+ 717 718instance star :: (linordered_cancel_ab_semigroup_add) linordered_cancel_ab_semigroup_add .. 719 720 721subsection \<open>Ring and field classes\<close> 722 723instance star :: (semiring) semiring 724 by (intro_classes; transfer) (fact distrib_right distrib_left)+ 725 726instance star :: (semiring_0) semiring_0 727 by (intro_classes; transfer) simp_all 728 729instance star :: (semiring_0_cancel) semiring_0_cancel .. 730 731instance star :: (comm_semiring) comm_semiring 732 by (intro_classes; transfer) (fact distrib_right) 733 734instance star :: (comm_semiring_0) comm_semiring_0 .. 735instance star :: (comm_semiring_0_cancel) comm_semiring_0_cancel .. 736 737instance star :: (zero_neq_one) zero_neq_one 738 by (intro_classes; transfer) (fact zero_neq_one) 739 740instance star :: (semiring_1) semiring_1 .. 741instance star :: (comm_semiring_1) comm_semiring_1 .. 742 743declare dvd_def [transfer_refold] 744 745instance star :: (comm_semiring_1_cancel) comm_semiring_1_cancel 746 by (intro_classes; transfer) (fact right_diff_distrib') 747 748instance star :: (semiring_no_zero_divisors) semiring_no_zero_divisors 749 by (intro_classes; transfer) (fact no_zero_divisors) 750 751instance star :: (semiring_1_no_zero_divisors) semiring_1_no_zero_divisors .. 752 753instance star :: (semiring_no_zero_divisors_cancel) semiring_no_zero_divisors_cancel 754 by (intro_classes; transfer) simp_all 755 756instance star :: (semiring_1_cancel) semiring_1_cancel .. 757instance star :: (ring) ring .. 758instance star :: (comm_ring) comm_ring .. 759instance star :: (ring_1) ring_1 .. 760instance star :: (comm_ring_1) comm_ring_1 .. 761instance star :: (semidom) semidom .. 762 763instance star :: (semidom_divide) semidom_divide 764 by (intro_classes; transfer) simp_all 765 766instance star :: (ring_no_zero_divisors) ring_no_zero_divisors .. 767instance star :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors .. 768instance star :: (idom) idom .. 769instance star :: (idom_divide) idom_divide .. 770 771instance star :: (division_ring) division_ring 772 by (intro_classes; transfer) (simp_all add: divide_inverse) 773 774instance star :: (field) field 775 by (intro_classes; transfer) (simp_all add: divide_inverse) 776 777instance star :: (ordered_semiring) ordered_semiring 778 by (intro_classes; transfer) (fact mult_left_mono mult_right_mono)+ 779 780instance star :: (ordered_cancel_semiring) ordered_cancel_semiring .. 781 782instance star :: (linordered_semiring_strict) linordered_semiring_strict 783 by (intro_classes; transfer) (fact mult_strict_left_mono mult_strict_right_mono)+ 784 785instance star :: (ordered_comm_semiring) ordered_comm_semiring 786 by (intro_classes; transfer) (fact mult_left_mono) 787 788instance star :: (ordered_cancel_comm_semiring) ordered_cancel_comm_semiring .. 789 790instance star :: (linordered_comm_semiring_strict) linordered_comm_semiring_strict 791 by (intro_classes; transfer) (fact mult_strict_left_mono) 792 793instance star :: (ordered_ring) ordered_ring .. 794 795instance star :: (ordered_ring_abs) ordered_ring_abs 796 by (intro_classes; transfer) (fact abs_eq_mult) 797 798instance star :: (abs_if) abs_if 799 by (intro_classes; transfer) (fact abs_if) 800 801instance star :: (linordered_ring_strict) linordered_ring_strict .. 802instance star :: (ordered_comm_ring) ordered_comm_ring .. 803 804instance star :: (linordered_semidom) linordered_semidom 805 by (intro_classes; transfer) (fact zero_less_one le_add_diff_inverse2)+ 806 807instance star :: (linordered_idom) linordered_idom 808 by (intro_classes; transfer) (fact sgn_if) 809 810instance star :: (linordered_field) linordered_field .. 811 812instance star :: (algebraic_semidom) algebraic_semidom .. 813 814instantiation star :: (normalization_semidom) normalization_semidom 815begin 816 817definition unit_factor_star :: "'a star \<Rightarrow> 'a star" 818 where [transfer_unfold]: "unit_factor_star = *f* unit_factor" 819 820definition normalize_star :: "'a star \<Rightarrow> 'a star" 821 where [transfer_unfold]: "normalize_star = *f* normalize" 822 823instance 824 by standard (transfer; simp add: is_unit_unit_factor unit_factor_mult)+ 825 826end 827 828instance star :: (semidom_modulo) semidom_modulo 829 by standard (transfer; simp) 830 831 832 833subsection \<open>Power\<close> 834 835lemma star_power_def [transfer_unfold]: "(^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x" 836proof (rule eq_reflection, rule ext, rule ext) 837 show "x ^ n = ( *f* (\<lambda>x. x ^ n)) x" for n :: nat and x :: "'a star" 838 proof (induct n arbitrary: x) 839 case 0 840 have "\<And>x::'a star. ( *f* (\<lambda>x. 1)) x = 1" 841 by transfer simp 842 then show ?case by simp 843 next 844 case (Suc n) 845 have "\<And>x::'a star. x * ( *f* (\<lambda>x::'a. x ^ n)) x = ( *f* (\<lambda>x::'a. x * x ^ n)) x" 846 by transfer simp 847 with Suc show ?case by simp 848 qed 849qed 850 851lemma Standard_power [simp]: "x \<in> Standard \<Longrightarrow> x ^ n \<in> Standard" 852 by (simp add: star_power_def) 853 854lemma star_of_power [simp]: "star_of (x ^ n) = star_of x ^ n" 855 by transfer (rule refl) 856 857 858subsection \<open>Number classes\<close> 859 860instance star :: (numeral) numeral .. 861 862lemma star_numeral_def [transfer_unfold]: "numeral k = star_of (numeral k)" 863 by (induct k) (simp_all only: numeral.simps star_of_one star_of_add) 864 865lemma Standard_numeral [simp]: "numeral k \<in> Standard" 866 by (simp add: star_numeral_def) 867 868lemma star_of_numeral [simp]: "star_of (numeral k) = numeral k" 869 by transfer (rule refl) 870 871lemma star_of_nat_def [transfer_unfold]: "of_nat n = star_of (of_nat n)" 872 by (induct n) simp_all 873 874lemmas star_of_compare_numeral [simp] = 875 star_of_less [of "numeral k", simplified star_of_numeral] 876 star_of_le [of "numeral k", simplified star_of_numeral] 877 star_of_eq [of "numeral k", simplified star_of_numeral] 878 star_of_less [of _ "numeral k", simplified star_of_numeral] 879 star_of_le [of _ "numeral k", simplified star_of_numeral] 880 star_of_eq [of _ "numeral k", simplified star_of_numeral] 881 star_of_less [of "- numeral k", simplified star_of_numeral] 882 star_of_le [of "- numeral k", simplified star_of_numeral] 883 star_of_eq [of "- numeral k", simplified star_of_numeral] 884 star_of_less [of _ "- numeral k", simplified star_of_numeral] 885 star_of_le [of _ "- numeral k", simplified star_of_numeral] 886 star_of_eq [of _ "- numeral k", simplified star_of_numeral] for k 887 888lemma Standard_of_nat [simp]: "of_nat n \<in> Standard" 889 by (simp add: star_of_nat_def) 890 891lemma star_of_of_nat [simp]: "star_of (of_nat n) = of_nat n" 892 by transfer (rule refl) 893 894lemma star_of_int_def [transfer_unfold]: "of_int z = star_of (of_int z)" 895 by (rule int_diff_cases [of z]) simp 896 897lemma Standard_of_int [simp]: "of_int z \<in> Standard" 898 by (simp add: star_of_int_def) 899 900lemma star_of_of_int [simp]: "star_of (of_int z) = of_int z" 901 by transfer (rule refl) 902 903instance star :: (semiring_char_0) semiring_char_0 904proof 905 have "inj (star_of :: 'a \<Rightarrow> 'a star)" 906 by (rule injI) simp 907 then have "inj (star_of \<circ> of_nat :: nat \<Rightarrow> 'a star)" 908 using inj_of_nat by (rule inj_compose) 909 then show "inj (of_nat :: nat \<Rightarrow> 'a star)" 910 by (simp add: comp_def) 911qed 912 913instance star :: (ring_char_0) ring_char_0 .. 914 915 916subsection \<open>Finite class\<close> 917 918lemma starset_finite: "finite A \<Longrightarrow> *s* A = star_of ` A" 919 by (erule finite_induct) simp_all 920 921instance star :: (finite) finite 922proof intro_classes 923 show "finite (UNIV::'a star set)" 924 by (metis starset_UNIV finite finite_imageI starset_finite) 925qed 926 927end 928