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