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