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