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