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