src/HOL/NSA/StarDef.thy
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 47108 2a1953f0d20d
child 47328 9f11a3cd84b1
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
     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)
    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 definition "star = (UNIV :: (nat \<Rightarrow> 'a) set) // starrel"
    43 
    44 typedef (open) 'a star = "star :: (nat \<Rightarrow> 'a) set set"
    45   unfolding star_def by (auto intro: quotientI)
    46 
    47 definition
    48   star_n :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a star" where
    49   "star_n X = Abs_star (starrel `` {X})"
    50 
    51 theorem star_cases [case_names star_n, cases type: star]:
    52   "(\<And>X. x = star_n X \<Longrightarrow> P) \<Longrightarrow> P"
    53 by (cases x, unfold star_n_def star_def, erule quotientE, fast)
    54 
    55 lemma all_star_eq: "(\<forall>x. P x) = (\<forall>X. P (star_n X))"
    56 by (auto, rule_tac x=x in star_cases, simp)
    57 
    58 lemma ex_star_eq: "(\<exists>x. P x) = (\<exists>X. P (star_n X))"
    59 by (auto, rule_tac x=x in star_cases, auto)
    60 
    61 text {* Proving that @{term starrel} is an equivalence relation *}
    62 
    63 lemma starrel_iff [iff]: "((X,Y) \<in> starrel) = ({n. X n = Y n} \<in> \<U>)"
    64 by (simp add: starrel_def)
    65 
    66 lemma equiv_starrel: "equiv UNIV starrel"
    67 proof (rule equivI)
    68   show "refl starrel" by (simp add: refl_on_def)
    69   show "sym starrel" by (simp add: sym_def eq_commute)
    70   show "trans starrel" by (auto intro: transI elim!: ultra)
    71 qed
    72 
    73 lemmas equiv_starrel_iff =
    74   eq_equiv_class_iff [OF equiv_starrel UNIV_I UNIV_I]
    75 
    76 lemma starrel_in_star: "starrel``{x} \<in> star"
    77 by (simp add: star_def quotientI)
    78 
    79 lemma star_n_eq_iff: "(star_n X = star_n Y) = ({n. X n = Y n} \<in> \<U>)"
    80 by (simp add: star_n_def Abs_star_inject starrel_in_star equiv_starrel_iff)
    81 
    82 
    83 subsection {* Transfer principle *}
    84 
    85 text {* This introduction rule starts each transfer proof. *}
    86 lemma transfer_start:
    87   "P \<equiv> {n. Q} \<in> \<U> \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
    88 by (subgoal_tac "P \<equiv> Q", simp, simp add: atomize_eq)
    89 
    90 text {*Initialize transfer tactic.*}
    91 use "transfer.ML"
    92 setup Transfer.setup
    93 
    94 text {* Transfer introduction rules. *}
    95 
    96 lemma transfer_ex [transfer_intro]:
    97   "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
    98     \<Longrightarrow> \<exists>x::'a star. p x \<equiv> {n. \<exists>x. P n x} \<in> \<U>"
    99 by (simp only: ex_star_eq FreeUltrafilterNat.Collect_ex)
   100 
   101 lemma transfer_all [transfer_intro]:
   102   "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
   103     \<Longrightarrow> \<forall>x::'a star. p x \<equiv> {n. \<forall>x. P n x} \<in> \<U>"
   104 by (simp only: all_star_eq FreeUltrafilterNat.Collect_all)
   105 
   106 lemma transfer_not [transfer_intro]:
   107   "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>\<rbrakk> \<Longrightarrow> \<not> p \<equiv> {n. \<not> P n} \<in> \<U>"
   108 by (simp only: FreeUltrafilterNat.Collect_not)
   109 
   110 lemma transfer_conj [transfer_intro]:
   111   "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
   112     \<Longrightarrow> p \<and> q \<equiv> {n. P n \<and> Q n} \<in> \<U>"
   113 by (simp only: FreeUltrafilterNat.Collect_conj)
   114 
   115 lemma transfer_disj [transfer_intro]:
   116   "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
   117     \<Longrightarrow> p \<or> q \<equiv> {n. P n \<or> Q n} \<in> \<U>"
   118 by (simp only: FreeUltrafilterNat.Collect_disj)
   119 
   120 lemma transfer_imp [transfer_intro]:
   121   "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
   122     \<Longrightarrow> p \<longrightarrow> q \<equiv> {n. P n \<longrightarrow> Q n} \<in> \<U>"
   123 by (simp only: imp_conv_disj transfer_disj transfer_not)
   124 
   125 lemma transfer_iff [transfer_intro]:
   126   "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
   127     \<Longrightarrow> p = q \<equiv> {n. P n = Q n} \<in> \<U>"
   128 by (simp only: iff_conv_conj_imp transfer_conj transfer_imp)
   129 
   130 lemma transfer_if_bool [transfer_intro]:
   131   "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; x \<equiv> {n. X n} \<in> \<U>; y \<equiv> {n. Y n} \<in> \<U>\<rbrakk>
   132     \<Longrightarrow> (if p then x else y) \<equiv> {n. if P n then X n else Y n} \<in> \<U>"
   133 by (simp only: if_bool_eq_conj transfer_conj transfer_imp transfer_not)
   134 
   135 lemma transfer_eq [transfer_intro]:
   136   "\<lbrakk>x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk> \<Longrightarrow> x = y \<equiv> {n. X n = Y n} \<in> \<U>"
   137 by (simp only: star_n_eq_iff)
   138 
   139 lemma transfer_if [transfer_intro]:
   140   "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk>
   141     \<Longrightarrow> (if p then x else y) \<equiv> star_n (\<lambda>n. if P n then X n else Y n)"
   142 apply (rule eq_reflection)
   143 apply (auto simp add: star_n_eq_iff transfer_not elim!: ultra)
   144 done
   145 
   146 lemma transfer_fun_eq [transfer_intro]:
   147   "\<lbrakk>\<And>X. f (star_n X) = g (star_n X) 
   148     \<equiv> {n. F n (X n) = G n (X n)} \<in> \<U>\<rbrakk>
   149       \<Longrightarrow> f = g \<equiv> {n. F n = G n} \<in> \<U>"
   150 by (simp only: fun_eq_iff transfer_all)
   151 
   152 lemma transfer_star_n [transfer_intro]: "star_n X \<equiv> star_n (\<lambda>n. X n)"
   153 by (rule reflexive)
   154 
   155 lemma transfer_bool [transfer_intro]: "p \<equiv> {n. p} \<in> \<U>"
   156 by (simp add: atomize_eq)
   157 
   158 
   159 subsection {* Standard elements *}
   160 
   161 definition
   162   star_of :: "'a \<Rightarrow> 'a star" where
   163   "star_of x == star_n (\<lambda>n. x)"
   164 
   165 definition
   166   Standard :: "'a star set" where
   167   "Standard = range star_of"
   168 
   169 text {* Transfer tactic should remove occurrences of @{term star_of} *}
   170 setup {* Transfer.add_const "StarDef.star_of" *}
   171 
   172 declare star_of_def [transfer_intro]
   173 
   174 lemma star_of_inject: "(star_of x = star_of y) = (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 {* Internal functions *}
   182 
   183 definition
   184   Ifun :: "('a \<Rightarrow> 'b) star \<Rightarrow> 'a star \<Rightarrow> 'b star" ("_ \<star> _" [300,301] 300) where
   185   "Ifun f \<equiv> \<lambda>x. Abs_star
   186        (\<Union>F\<in>Rep_star f. \<Union>X\<in>Rep_star x. starrel``{\<lambda>n. F n (X n)})"
   187 
   188 lemma Ifun_congruent2:
   189   "congruent2 starrel starrel (\<lambda>F X. starrel``{\<lambda>n. F n (X n)})"
   190 by (auto simp add: congruent2_def equiv_starrel_iff elim!: ultra)
   191 
   192 lemma Ifun_star_n: "star_n F \<star> star_n X = star_n (\<lambda>n. F n (X n))"
   193 by (simp add: Ifun_def star_n_def Abs_star_inverse starrel_in_star
   194     UN_equiv_class2 [OF equiv_starrel equiv_starrel Ifun_congruent2])
   195 
   196 text {* Transfer tactic should remove occurrences of @{term Ifun} *}
   197 setup {* Transfer.add_const "StarDef.Ifun" *}
   198 
   199 lemma transfer_Ifun [transfer_intro]:
   200   "\<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))"
   201 by (simp only: Ifun_star_n)
   202 
   203 lemma Ifun_star_of [simp]: "star_of f \<star> star_of x = star_of (f x)"
   204 by (transfer, rule refl)
   205 
   206 lemma Standard_Ifun [simp]:
   207   "\<lbrakk>f \<in> Standard; x \<in> Standard\<rbrakk> \<Longrightarrow> f \<star> x \<in> Standard"
   208 by (auto simp add: Standard_def)
   209 
   210 text {* Nonstandard extensions of functions *}
   211 
   212 definition
   213   starfun :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a star \<Rightarrow> 'b star)"  ("*f* _" [80] 80) where
   214   "starfun f == \<lambda>x. star_of f \<star> x"
   215 
   216 definition
   217   starfun2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a star \<Rightarrow> 'b star \<Rightarrow> 'c star)"
   218     ("*f2* _" [80] 80) where
   219   "starfun2 f == \<lambda>x y. star_of f \<star> x \<star> y"
   220 
   221 declare starfun_def [transfer_unfold]
   222 declare starfun2_def [transfer_unfold]
   223 
   224 lemma starfun_star_n: "( *f* f) (star_n X) = star_n (\<lambda>n. f (X n))"
   225 by (simp only: starfun_def star_of_def Ifun_star_n)
   226 
   227 lemma starfun2_star_n:
   228   "( *f2* f) (star_n X) (star_n Y) = star_n (\<lambda>n. f (X n) (Y n))"
   229 by (simp only: starfun2_def star_of_def Ifun_star_n)
   230 
   231 lemma starfun_star_of [simp]: "( *f* f) (star_of x) = star_of (f x)"
   232 by (transfer, rule refl)
   233 
   234 lemma starfun2_star_of [simp]: "( *f2* f) (star_of x) = *f* f x"
   235 by (transfer, rule refl)
   236 
   237 lemma Standard_starfun [simp]: "x \<in> Standard \<Longrightarrow> starfun f x \<in> Standard"
   238 by (simp add: starfun_def)
   239 
   240 lemma Standard_starfun2 [simp]:
   241   "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> starfun2 f x y \<in> Standard"
   242 by (simp add: starfun2_def)
   243 
   244 lemma Standard_starfun_iff:
   245   assumes inj: "\<And>x y. f x = f y \<Longrightarrow> x = y"
   246   shows "(starfun f x \<in> Standard) = (x \<in> Standard)"
   247 proof
   248   assume "x \<in> Standard"
   249   thus "starfun f x \<in> Standard" by simp
   250 next
   251   have inj': "\<And>x y. starfun f x = starfun f y \<Longrightarrow> x = y"
   252     using inj by transfer
   253   assume "starfun f x \<in> Standard"
   254   then obtain b where b: "starfun f x = star_of b"
   255     unfolding Standard_def ..
   256   hence "\<exists>x. starfun f x = star_of b" ..
   257   hence "\<exists>a. f a = b" by transfer
   258   then obtain a where "f a = b" ..
   259   hence "starfun f (star_of a) = star_of b" by transfer
   260   with b have "starfun f x = starfun f (star_of a)" by simp
   261   hence "x = star_of a" by (rule inj')
   262   thus "x \<in> Standard"
   263     unfolding Standard_def by auto
   264 qed
   265 
   266 lemma Standard_starfun2_iff:
   267   assumes inj: "\<And>a b a' b'. f a b = f a' b' \<Longrightarrow> a = a' \<and> b = b'"
   268   shows "(starfun2 f x y \<in> Standard) = (x \<in> Standard \<and> y \<in> Standard)"
   269 proof
   270   assume "x \<in> Standard \<and> y \<in> Standard"
   271   thus "starfun2 f x y \<in> Standard" by simp
   272 next
   273   have inj': "\<And>x y z w. starfun2 f x y = starfun2 f z w \<Longrightarrow> x = z \<and> y = w"
   274     using inj by transfer
   275   assume "starfun2 f x y \<in> Standard"
   276   then obtain c where c: "starfun2 f x y = star_of c"
   277     unfolding Standard_def ..
   278   hence "\<exists>x y. starfun2 f x y = star_of c" by auto
   279   hence "\<exists>a b. f a b = c" by transfer
   280   then obtain a b where "f a b = c" by auto
   281   hence "starfun2 f (star_of a) (star_of b) = star_of c"
   282     by transfer
   283   with c have "starfun2 f x y = starfun2 f (star_of a) (star_of b)"
   284     by simp
   285   hence "x = star_of a \<and> y = star_of b"
   286     by (rule inj')
   287   thus "x \<in> Standard \<and> y \<in> Standard"
   288     unfolding Standard_def by auto
   289 qed
   290 
   291 
   292 subsection {* Internal predicates *}
   293 
   294 definition unstar :: "bool star \<Rightarrow> bool" where
   295   "unstar b \<longleftrightarrow> 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 set_eq_iff 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: set_eq_iff 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_eq, rule refl)
   405 
   406 lemma starset_diff: "*s* (A - B) = *s* A - *s* B"
   407 by (transfer set_diff_eq, 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_eq, 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 instance star :: (Rings.dvd) Rings.dvd ..
   526 
   527 instantiation star :: (Divides.div) Divides.div
   528 begin
   529 
   530 definition
   531   star_div_def:     "(op div) \<equiv> *f2* (op div)"
   532 
   533 definition
   534   star_mod_def:     "(op mod) \<equiv> *f2* (op mod)"
   535 
   536 instance ..
   537 
   538 end
   539 
   540 instantiation star :: (ord) ord
   541 begin
   542 
   543 definition
   544   star_le_def:      "(op \<le>) \<equiv> *p2* (op \<le>)"
   545 
   546 definition
   547   star_less_def:    "(op <) \<equiv> *p2* (op <)"
   548 
   549 instance ..
   550 
   551 end
   552 
   553 lemmas star_class_defs [transfer_unfold] =
   554   star_zero_def     star_one_def
   555   star_add_def      star_diff_def     star_minus_def
   556   star_mult_def     star_divide_def   star_inverse_def
   557   star_le_def       star_less_def     star_abs_def       star_sgn_def
   558   star_div_def      star_mod_def
   559 
   560 text {* Class operations preserve standard elements *}
   561 
   562 lemma Standard_zero: "0 \<in> Standard"
   563 by (simp add: star_zero_def)
   564 
   565 lemma Standard_one: "1 \<in> Standard"
   566 by (simp add: star_one_def)
   567 
   568 lemma Standard_add: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x + y \<in> Standard"
   569 by (simp add: star_add_def)
   570 
   571 lemma Standard_diff: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x - y \<in> Standard"
   572 by (simp add: star_diff_def)
   573 
   574 lemma Standard_minus: "x \<in> Standard \<Longrightarrow> - x \<in> Standard"
   575 by (simp add: star_minus_def)
   576 
   577 lemma Standard_mult: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x * y \<in> Standard"
   578 by (simp add: star_mult_def)
   579 
   580 lemma Standard_divide: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x / y \<in> Standard"
   581 by (simp add: star_divide_def)
   582 
   583 lemma Standard_inverse: "x \<in> Standard \<Longrightarrow> inverse x \<in> Standard"
   584 by (simp add: star_inverse_def)
   585 
   586 lemma Standard_abs: "x \<in> Standard \<Longrightarrow> abs x \<in> Standard"
   587 by (simp add: star_abs_def)
   588 
   589 lemma Standard_div: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x div y \<in> Standard"
   590 by (simp add: star_div_def)
   591 
   592 lemma Standard_mod: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x mod y \<in> Standard"
   593 by (simp add: star_mod_def)
   594 
   595 lemmas Standard_simps [simp] =
   596   Standard_zero  Standard_one
   597   Standard_add  Standard_diff  Standard_minus
   598   Standard_mult  Standard_divide  Standard_inverse
   599   Standard_abs  Standard_div  Standard_mod
   600 
   601 text {* @{term star_of} preserves class operations *}
   602 
   603 lemma star_of_add: "star_of (x + y) = star_of x + star_of y"
   604 by transfer (rule refl)
   605 
   606 lemma star_of_diff: "star_of (x - y) = star_of x - star_of y"
   607 by transfer (rule refl)
   608 
   609 lemma star_of_minus: "star_of (-x) = - star_of x"
   610 by transfer (rule refl)
   611 
   612 lemma star_of_mult: "star_of (x * y) = star_of x * star_of y"
   613 by transfer (rule refl)
   614 
   615 lemma star_of_divide: "star_of (x / y) = star_of x / star_of y"
   616 by transfer (rule refl)
   617 
   618 lemma star_of_inverse: "star_of (inverse x) = inverse (star_of x)"
   619 by transfer (rule refl)
   620 
   621 lemma star_of_div: "star_of (x div y) = star_of x div star_of y"
   622 by transfer (rule refl)
   623 
   624 lemma star_of_mod: "star_of (x mod y) = star_of x mod star_of y"
   625 by transfer (rule refl)
   626 
   627 lemma star_of_abs: "star_of (abs x) = abs (star_of x)"
   628 by transfer (rule refl)
   629 
   630 text {* @{term star_of} preserves numerals *}
   631 
   632 lemma star_of_zero: "star_of 0 = 0"
   633 by transfer (rule refl)
   634 
   635 lemma star_of_one: "star_of 1 = 1"
   636 by transfer (rule refl)
   637 
   638 text {* @{term star_of} preserves orderings *}
   639 
   640 lemma star_of_less: "(star_of x < star_of y) = (x < y)"
   641 by transfer (rule refl)
   642 
   643 lemma star_of_le: "(star_of x \<le> star_of y) = (x \<le> y)"
   644 by transfer (rule refl)
   645 
   646 lemma star_of_eq: "(star_of x = star_of y) = (x = y)"
   647 by transfer (rule refl)
   648 
   649 text{*As above, for 0*}
   650 
   651 lemmas star_of_0_less = star_of_less [of 0, simplified star_of_zero]
   652 lemmas star_of_0_le   = star_of_le   [of 0, simplified star_of_zero]
   653 lemmas star_of_0_eq   = star_of_eq   [of 0, simplified star_of_zero]
   654 
   655 lemmas star_of_less_0 = star_of_less [of _ 0, simplified star_of_zero]
   656 lemmas star_of_le_0   = star_of_le   [of _ 0, simplified star_of_zero]
   657 lemmas star_of_eq_0   = star_of_eq   [of _ 0, simplified star_of_zero]
   658 
   659 text{*As above, for 1*}
   660 
   661 lemmas star_of_1_less = star_of_less [of 1, simplified star_of_one]
   662 lemmas star_of_1_le   = star_of_le   [of 1, simplified star_of_one]
   663 lemmas star_of_1_eq   = star_of_eq   [of 1, simplified star_of_one]
   664 
   665 lemmas star_of_less_1 = star_of_less [of _ 1, simplified star_of_one]
   666 lemmas star_of_le_1   = star_of_le   [of _ 1, simplified star_of_one]
   667 lemmas star_of_eq_1   = star_of_eq   [of _ 1, simplified star_of_one]
   668 
   669 lemmas star_of_simps [simp] =
   670   star_of_add     star_of_diff    star_of_minus
   671   star_of_mult    star_of_divide  star_of_inverse
   672   star_of_div     star_of_mod     star_of_abs
   673   star_of_zero    star_of_one
   674   star_of_less    star_of_le      star_of_eq
   675   star_of_0_less  star_of_0_le    star_of_0_eq
   676   star_of_less_0  star_of_le_0    star_of_eq_0
   677   star_of_1_less  star_of_1_le    star_of_1_eq
   678   star_of_less_1  star_of_le_1    star_of_eq_1
   679 
   680 subsection {* Ordering and lattice classes *}
   681 
   682 instance star :: (order) order
   683 apply (intro_classes)
   684 apply (transfer, rule less_le_not_le)
   685 apply (transfer, rule order_refl)
   686 apply (transfer, erule (1) order_trans)
   687 apply (transfer, erule (1) order_antisym)
   688 done
   689 
   690 instantiation star :: (semilattice_inf) semilattice_inf
   691 begin
   692 
   693 definition
   694   star_inf_def [transfer_unfold]: "inf \<equiv> *f2* inf"
   695 
   696 instance
   697   by default (transfer star_inf_def, auto)+
   698 
   699 end
   700 
   701 instantiation star :: (semilattice_sup) semilattice_sup
   702 begin
   703 
   704 definition
   705   star_sup_def [transfer_unfold]: "sup \<equiv> *f2* sup"
   706 
   707 instance
   708   by default (transfer star_sup_def, auto)+
   709 
   710 end
   711 
   712 instance star :: (lattice) lattice ..
   713 
   714 instance star :: (distrib_lattice) distrib_lattice
   715   by default (transfer, auto simp add: sup_inf_distrib1)
   716 
   717 lemma Standard_inf [simp]:
   718   "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> inf x y \<in> Standard"
   719 by (simp add: star_inf_def)
   720 
   721 lemma Standard_sup [simp]:
   722   "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> sup x y \<in> Standard"
   723 by (simp add: star_sup_def)
   724 
   725 lemma star_of_inf [simp]: "star_of (inf x y) = inf (star_of x) (star_of y)"
   726 by transfer (rule refl)
   727 
   728 lemma star_of_sup [simp]: "star_of (sup x y) = sup (star_of x) (star_of y)"
   729 by transfer (rule refl)
   730 
   731 instance star :: (linorder) linorder
   732 by (intro_classes, transfer, rule linorder_linear)
   733 
   734 lemma star_max_def [transfer_unfold]: "max = *f2* max"
   735 apply (rule ext, rule ext)
   736 apply (unfold max_def, transfer, fold max_def)
   737 apply (rule refl)
   738 done
   739 
   740 lemma star_min_def [transfer_unfold]: "min = *f2* min"
   741 apply (rule ext, rule ext)
   742 apply (unfold min_def, transfer, fold min_def)
   743 apply (rule refl)
   744 done
   745 
   746 lemma Standard_max [simp]:
   747   "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> max x y \<in> Standard"
   748 by (simp add: star_max_def)
   749 
   750 lemma Standard_min [simp]:
   751   "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> min x y \<in> Standard"
   752 by (simp add: star_min_def)
   753 
   754 lemma star_of_max [simp]: "star_of (max x y) = max (star_of x) (star_of y)"
   755 by transfer (rule refl)
   756 
   757 lemma star_of_min [simp]: "star_of (min x y) = min (star_of x) (star_of y)"
   758 by transfer (rule refl)
   759 
   760 
   761 subsection {* Ordered group classes *}
   762 
   763 instance star :: (semigroup_add) semigroup_add
   764 by (intro_classes, transfer, rule add_assoc)
   765 
   766 instance star :: (ab_semigroup_add) ab_semigroup_add
   767 by (intro_classes, transfer, rule add_commute)
   768 
   769 instance star :: (semigroup_mult) semigroup_mult
   770 by (intro_classes, transfer, rule mult_assoc)
   771 
   772 instance star :: (ab_semigroup_mult) ab_semigroup_mult
   773 by (intro_classes, transfer, rule mult_commute)
   774 
   775 instance star :: (comm_monoid_add) comm_monoid_add
   776 by (intro_classes, transfer, rule comm_monoid_add_class.add_0)
   777 
   778 instance star :: (monoid_mult) monoid_mult
   779 apply (intro_classes)
   780 apply (transfer, rule mult_1_left)
   781 apply (transfer, rule mult_1_right)
   782 done
   783 
   784 instance star :: (comm_monoid_mult) comm_monoid_mult
   785 by (intro_classes, transfer, rule mult_1)
   786 
   787 instance star :: (cancel_semigroup_add) cancel_semigroup_add
   788 apply (intro_classes)
   789 apply (transfer, erule add_left_imp_eq)
   790 apply (transfer, erule add_right_imp_eq)
   791 done
   792 
   793 instance star :: (cancel_ab_semigroup_add) cancel_ab_semigroup_add
   794 by (intro_classes, transfer, rule add_imp_eq)
   795 
   796 instance star :: (cancel_comm_monoid_add) cancel_comm_monoid_add ..
   797 
   798 instance star :: (ab_group_add) ab_group_add
   799 apply (intro_classes)
   800 apply (transfer, rule left_minus)
   801 apply (transfer, rule diff_minus)
   802 done
   803 
   804 instance star :: (ordered_ab_semigroup_add) ordered_ab_semigroup_add
   805 by (intro_classes, transfer, rule add_left_mono)
   806 
   807 instance star :: (ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
   808 
   809 instance star :: (ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le
   810 by (intro_classes, transfer, rule add_le_imp_le_left)
   811 
   812 instance star :: (ordered_comm_monoid_add) ordered_comm_monoid_add ..
   813 instance star :: (ordered_ab_group_add) ordered_ab_group_add ..
   814 
   815 instance star :: (ordered_ab_group_add_abs) ordered_ab_group_add_abs 
   816   by intro_classes (transfer,
   817     simp add: abs_ge_self abs_leI abs_triangle_ineq)+
   818 
   819 instance star :: (linordered_cancel_ab_semigroup_add) linordered_cancel_ab_semigroup_add ..
   820 
   821 
   822 subsection {* Ring and field classes *}
   823 
   824 instance star :: (semiring) semiring
   825 apply (intro_classes)
   826 apply (transfer, rule left_distrib)
   827 apply (transfer, rule right_distrib)
   828 done
   829 
   830 instance star :: (semiring_0) semiring_0 
   831 by intro_classes (transfer, simp)+
   832 
   833 instance star :: (semiring_0_cancel) semiring_0_cancel ..
   834 
   835 instance star :: (comm_semiring) comm_semiring 
   836 by (intro_classes, transfer, rule left_distrib)
   837 
   838 instance star :: (comm_semiring_0) comm_semiring_0 ..
   839 instance star :: (comm_semiring_0_cancel) comm_semiring_0_cancel ..
   840 
   841 instance star :: (zero_neq_one) zero_neq_one
   842 by (intro_classes, transfer, rule zero_neq_one)
   843 
   844 instance star :: (semiring_1) semiring_1 ..
   845 instance star :: (comm_semiring_1) comm_semiring_1 ..
   846 
   847 instance star :: (no_zero_divisors) no_zero_divisors
   848 by (intro_classes, transfer, rule no_zero_divisors)
   849 
   850 instance star :: (semiring_1_cancel) semiring_1_cancel ..
   851 instance star :: (comm_semiring_1_cancel) comm_semiring_1_cancel ..
   852 instance star :: (ring) ring ..
   853 instance star :: (comm_ring) comm_ring ..
   854 instance star :: (ring_1) ring_1 ..
   855 instance star :: (comm_ring_1) comm_ring_1 ..
   856 instance star :: (ring_no_zero_divisors) ring_no_zero_divisors ..
   857 instance star :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..
   858 instance star :: (idom) idom .. 
   859 
   860 instance star :: (division_ring) division_ring
   861 apply (intro_classes)
   862 apply (transfer, erule left_inverse)
   863 apply (transfer, erule right_inverse)
   864 apply (transfer, fact divide_inverse)
   865 done
   866 
   867 instance star :: (division_ring_inverse_zero) division_ring_inverse_zero
   868 by (intro_classes, transfer, rule inverse_zero)
   869 
   870 instance star :: (field) field
   871 apply (intro_classes)
   872 apply (transfer, erule left_inverse)
   873 apply (transfer, rule divide_inverse)
   874 done
   875 
   876 instance star :: (field_inverse_zero) field_inverse_zero
   877 apply intro_classes
   878 apply (rule inverse_zero)
   879 done
   880 
   881 instance star :: (ordered_semiring) ordered_semiring
   882 apply (intro_classes)
   883 apply (transfer, erule (1) mult_left_mono)
   884 apply (transfer, erule (1) mult_right_mono)
   885 done
   886 
   887 instance star :: (ordered_cancel_semiring) ordered_cancel_semiring ..
   888 
   889 instance star :: (linordered_semiring_strict) linordered_semiring_strict
   890 apply (intro_classes)
   891 apply (transfer, erule (1) mult_strict_left_mono)
   892 apply (transfer, erule (1) mult_strict_right_mono)
   893 done
   894 
   895 instance star :: (ordered_comm_semiring) ordered_comm_semiring
   896 by (intro_classes, transfer, rule mult_left_mono)
   897 
   898 instance star :: (ordered_cancel_comm_semiring) ordered_cancel_comm_semiring ..
   899 
   900 instance star :: (linordered_comm_semiring_strict) linordered_comm_semiring_strict
   901 by (intro_classes, transfer, rule mult_strict_left_mono)
   902 
   903 instance star :: (ordered_ring) ordered_ring ..
   904 instance star :: (ordered_ring_abs) ordered_ring_abs
   905   by intro_classes  (transfer, rule abs_eq_mult)
   906 
   907 instance star :: (abs_if) abs_if
   908 by (intro_classes, transfer, rule abs_if)
   909 
   910 instance star :: (sgn_if) sgn_if
   911 by (intro_classes, transfer, rule sgn_if)
   912 
   913 instance star :: (linordered_ring_strict) linordered_ring_strict ..
   914 instance star :: (ordered_comm_ring) ordered_comm_ring ..
   915 
   916 instance star :: (linordered_semidom) linordered_semidom
   917 by (intro_classes, transfer, rule zero_less_one)
   918 
   919 instance star :: (linordered_idom) linordered_idom ..
   920 instance star :: (linordered_field) linordered_field ..
   921 instance star :: (linordered_field_inverse_zero) linordered_field_inverse_zero ..
   922 
   923 
   924 subsection {* Power *}
   925 
   926 lemma star_power_def [transfer_unfold]:
   927   "(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x"
   928 proof (rule eq_reflection, rule ext, rule ext)
   929   fix n :: nat
   930   show "\<And>x::'a star. x ^ n = ( *f* (\<lambda>x. x ^ n)) x" 
   931   proof (induct n)
   932     case 0
   933     have "\<And>x::'a star. ( *f* (\<lambda>x. 1)) x = 1"
   934       by transfer simp
   935     then show ?case by simp
   936   next
   937     case (Suc n)
   938     have "\<And>x::'a star. x * ( *f* (\<lambda>x\<Colon>'a. x ^ n)) x = ( *f* (\<lambda>x\<Colon>'a. x * x ^ n)) x"
   939       by transfer simp
   940     with Suc show ?case by simp
   941   qed
   942 qed
   943 
   944 lemma Standard_power [simp]: "x \<in> Standard \<Longrightarrow> x ^ n \<in> Standard"
   945   by (simp add: star_power_def)
   946 
   947 lemma star_of_power [simp]: "star_of (x ^ n) = star_of x ^ n"
   948   by transfer (rule refl)
   949 
   950 
   951 subsection {* Number classes *}
   952 
   953 instance star :: (numeral) numeral ..
   954 
   955 lemma star_numeral_def [transfer_unfold]:
   956   "numeral k = star_of (numeral k)"
   957 by (induct k, simp_all only: numeral.simps star_of_one star_of_add)
   958 
   959 lemma Standard_numeral [simp]: "numeral k \<in> Standard"
   960 by (simp add: star_numeral_def)
   961 
   962 lemma star_of_numeral [simp]: "star_of (numeral k) = numeral k"
   963 by transfer (rule refl)
   964 
   965 lemma star_neg_numeral_def [transfer_unfold]:
   966   "neg_numeral k = star_of (neg_numeral k)"
   967 by (simp only: neg_numeral_def star_of_minus star_of_numeral)
   968 
   969 lemma Standard_neg_numeral [simp]: "neg_numeral k \<in> Standard"
   970 by (simp add: star_neg_numeral_def)
   971 
   972 lemma star_of_neg_numeral [simp]: "star_of (neg_numeral k) = neg_numeral k"
   973 by transfer (rule refl)
   974 
   975 lemma star_of_nat_def [transfer_unfold]: "of_nat n = star_of (of_nat n)"
   976 by (induct n, simp_all)
   977 
   978 lemmas star_of_compare_numeral [simp] =
   979   star_of_less [of "numeral k", simplified star_of_numeral]
   980   star_of_le   [of "numeral k", simplified star_of_numeral]
   981   star_of_eq   [of "numeral k", simplified star_of_numeral]
   982   star_of_less [of _ "numeral k", simplified star_of_numeral]
   983   star_of_le   [of _ "numeral k", simplified star_of_numeral]
   984   star_of_eq   [of _ "numeral k", simplified star_of_numeral]
   985   star_of_less [of "neg_numeral k", simplified star_of_numeral]
   986   star_of_le   [of "neg_numeral k", simplified star_of_numeral]
   987   star_of_eq   [of "neg_numeral k", simplified star_of_numeral]
   988   star_of_less [of _ "neg_numeral k", simplified star_of_numeral]
   989   star_of_le   [of _ "neg_numeral k", simplified star_of_numeral]
   990   star_of_eq   [of _ "neg_numeral k", simplified star_of_numeral] for k
   991 
   992 lemma Standard_of_nat [simp]: "of_nat n \<in> Standard"
   993 by (simp add: star_of_nat_def)
   994 
   995 lemma star_of_of_nat [simp]: "star_of (of_nat n) = of_nat n"
   996 by transfer (rule refl)
   997 
   998 lemma star_of_int_def [transfer_unfold]: "of_int z = star_of (of_int z)"
   999 by (rule_tac z=z in int_diff_cases, simp)
  1000 
  1001 lemma Standard_of_int [simp]: "of_int z \<in> Standard"
  1002 by (simp add: star_of_int_def)
  1003 
  1004 lemma star_of_of_int [simp]: "star_of (of_int z) = of_int z"
  1005 by transfer (rule refl)
  1006 
  1007 instance star :: (semiring_char_0) semiring_char_0 proof
  1008   have "inj (star_of :: 'a \<Rightarrow> 'a star)" by (rule injI) simp
  1009   then have "inj (star_of \<circ> of_nat :: nat \<Rightarrow> 'a star)" using inj_of_nat by (rule inj_comp)
  1010   then show "inj (of_nat :: nat \<Rightarrow> 'a star)" by (simp add: comp_def)
  1011 qed
  1012 
  1013 instance star :: (ring_char_0) ring_char_0 ..
  1014 
  1015 
  1016 subsection {* Finite class *}
  1017 
  1018 lemma starset_finite: "finite A \<Longrightarrow> *s* A = star_of ` A"
  1019 by (erule finite_induct, simp_all)
  1020 
  1021 instance star :: (finite) finite
  1022 apply (intro_classes)
  1023 apply (subst starset_UNIV [symmetric])
  1024 apply (subst starset_finite [OF finite])
  1025 apply (rule finite_imageI [OF finite])
  1026 done
  1027 
  1028 end