src/HOL/Hyperreal/StarDef.thy
author wenzelm
Thu Jan 19 21:22:08 2006 +0100 (2006-01-19 ago)
changeset 18708 4b3dadb4fe33
parent 17443 f503dccdff27
child 19765 dfe940911617
permissions -rw-r--r--
setup: theory -> theory;
     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 constdefs
    16   FreeUltrafilterNat :: "nat set set"  ("\<U>")
    17     "\<U> \<equiv> SOME U. freeultrafilter U"
    18 
    19 lemma freeultrafilter_FUFNat: "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 FUFNat: freeultrafilter [FreeUltrafilterNat]
    27 by (cut_tac [!] freeultrafilter_FUFNat, simp_all add: freeultrafilter_def)
    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 FUFNat.F.Un_iff FUFNat.F.Compl_iff)
    34 
    35 
    36 subsection {* Definition of @{text star} type constructor *}
    37 
    38 constdefs
    39   starrel :: "((nat \<Rightarrow> 'a) \<times> (nat \<Rightarrow> 'a)) set"
    40     "starrel \<equiv> {(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 constdefs
    46   star_n :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a star"
    47   "star_n X \<equiv> 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 equiv.intro)
    66   show "reflexive starrel" by (simp add: refl_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 FUFNat.F.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 FUFNat.F.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: FUFNat.F.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: FUFNat.F.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: FUFNat.F.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: expand_fun_eq 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 constdefs
   160   star_of :: "'a \<Rightarrow> 'a star"
   161   "star_of x \<equiv> star_n (\<lambda>n. x)"
   162 
   163 text {* Transfer tactic should remove occurrences of @{term star_of} *}
   164 setup {* Transfer.add_const "StarDef.star_of" *}
   165 declare star_of_def [transfer_intro]
   166 
   167 lemma star_of_inject: "(star_of x = star_of y) = (x = y)"
   168 by (transfer, rule refl)
   169 
   170 
   171 subsection {* Internal functions *}
   172 
   173 constdefs
   174   Ifun :: "('a \<Rightarrow> 'b) star \<Rightarrow> 'a star \<Rightarrow> 'b star" ("_ \<star> _" [300,301] 300)
   175   "Ifun f \<equiv> \<lambda>x. Abs_star
   176        (\<Union>F\<in>Rep_star f. \<Union>X\<in>Rep_star x. starrel``{\<lambda>n. F n (X n)})"
   177 
   178 lemma Ifun_congruent2:
   179   "(\<lambda>F X. starrel``{\<lambda>n. F n (X n)}) respects2 starrel"
   180 by (auto simp add: congruent2_def equiv_starrel_iff elim!: ultra)
   181 
   182 lemma Ifun_star_n: "star_n F \<star> star_n X = star_n (\<lambda>n. F n (X n))"
   183 by (simp add: Ifun_def star_n_def Abs_star_inverse starrel_in_star
   184     UN_equiv_class2 [OF equiv_starrel equiv_starrel Ifun_congruent2])
   185 
   186 text {* Transfer tactic should remove occurrences of @{term Ifun} *}
   187 setup {* Transfer.add_const "StarDef.Ifun" *}
   188 
   189 lemma transfer_Ifun [transfer_intro]:
   190   "\<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))"
   191 by (simp only: Ifun_star_n)
   192 
   193 lemma Ifun_star_of [simp]: "star_of f \<star> star_of x = star_of (f x)"
   194 by (transfer, rule refl)
   195 
   196 text {* Nonstandard extensions of functions *}
   197 
   198 constdefs
   199   starfun :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a star \<Rightarrow> 'b star)"
   200     ("*f* _" [80] 80)
   201   "starfun f \<equiv> \<lambda>x. star_of f \<star> x"
   202 
   203   starfun2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a star \<Rightarrow> 'b star \<Rightarrow> 'c star)"
   204     ("*f2* _" [80] 80)
   205   "starfun2 f \<equiv> \<lambda>x y. star_of f \<star> x \<star> y"
   206 
   207 declare starfun_def [transfer_unfold]
   208 declare starfun2_def [transfer_unfold]
   209 
   210 lemma starfun_star_n: "( *f* f) (star_n X) = star_n (\<lambda>n. f (X n))"
   211 by (simp only: starfun_def star_of_def Ifun_star_n)
   212 
   213 lemma starfun2_star_n:
   214   "( *f2* f) (star_n X) (star_n Y) = star_n (\<lambda>n. f (X n) (Y n))"
   215 by (simp only: starfun2_def star_of_def Ifun_star_n)
   216 
   217 lemma starfun_star_of [simp]: "( *f* f) (star_of x) = star_of (f x)"
   218 by (transfer, rule refl)
   219 
   220 lemma starfun2_star_of [simp]: "( *f2* f) (star_of x) = *f* f x"
   221 by (transfer, rule refl)
   222 
   223 
   224 subsection {* Internal predicates *}
   225 
   226 constdefs
   227   unstar :: "bool star \<Rightarrow> bool"
   228   "unstar b \<equiv> b = star_of True"
   229 
   230 lemma unstar_star_n: "unstar (star_n P) = ({n. P n} \<in> \<U>)"
   231 by (simp add: unstar_def star_of_def star_n_eq_iff)
   232 
   233 lemma unstar_star_of [simp]: "unstar (star_of p) = p"
   234 by (simp add: unstar_def star_of_inject)
   235 
   236 text {* Transfer tactic should remove occurrences of @{term unstar} *}
   237 setup {* Transfer.add_const "StarDef.unstar" *}
   238 
   239 lemma transfer_unstar [transfer_intro]:
   240   "p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> {n. P n} \<in> \<U>"
   241 by (simp only: unstar_star_n)
   242 
   243 constdefs
   244   starP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a star \<Rightarrow> bool"
   245     ("*p* _" [80] 80)
   246   "*p* P \<equiv> \<lambda>x. unstar (star_of P \<star> x)"
   247 
   248   starP2 :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a star \<Rightarrow> 'b star \<Rightarrow> bool"
   249     ("*p2* _" [80] 80)
   250   "*p2* P \<equiv> \<lambda>x y. unstar (star_of P \<star> x \<star> y)"
   251 
   252 declare starP_def [transfer_unfold]
   253 declare starP2_def [transfer_unfold]
   254 
   255 lemma starP_star_n: "( *p* P) (star_n X) = ({n. P (X n)} \<in> \<U>)"
   256 by (simp only: starP_def star_of_def Ifun_star_n unstar_star_n)
   257 
   258 lemma starP2_star_n:
   259   "( *p2* P) (star_n X) (star_n Y) = ({n. P (X n) (Y n)} \<in> \<U>)"
   260 by (simp only: starP2_def star_of_def Ifun_star_n unstar_star_n)
   261 
   262 lemma starP_star_of [simp]: "( *p* P) (star_of x) = P x"
   263 by (transfer, rule refl)
   264 
   265 lemma starP2_star_of [simp]: "( *p2* P) (star_of x) = *p* P x"
   266 by (transfer, rule refl)
   267 
   268 
   269 subsection {* Internal sets *}
   270 
   271 constdefs
   272   Iset :: "'a set star \<Rightarrow> 'a star set"
   273   "Iset A \<equiv> {x. ( *p2* op \<in>) x A}"
   274 
   275 lemma Iset_star_n:
   276   "(star_n X \<in> Iset (star_n A)) = ({n. X n \<in> A n} \<in> \<U>)"
   277 by (simp add: Iset_def starP2_star_n)
   278 
   279 text {* Transfer tactic should remove occurrences of @{term Iset} *}
   280 setup {* Transfer.add_const "StarDef.Iset" *}
   281 
   282 lemma transfer_mem [transfer_intro]:
   283   "\<lbrakk>x \<equiv> star_n X; a \<equiv> Iset (star_n A)\<rbrakk>
   284     \<Longrightarrow> x \<in> a \<equiv> {n. X n \<in> A n} \<in> \<U>"
   285 by (simp only: Iset_star_n)
   286 
   287 lemma transfer_Collect [transfer_intro]:
   288   "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
   289     \<Longrightarrow> Collect p \<equiv> Iset (star_n (\<lambda>n. Collect (P n)))"
   290 by (simp add: atomize_eq expand_set_eq all_star_eq Iset_star_n)
   291 
   292 lemma transfer_set_eq [transfer_intro]:
   293   "\<lbrakk>a \<equiv> Iset (star_n A); b \<equiv> Iset (star_n B)\<rbrakk>
   294     \<Longrightarrow> a = b \<equiv> {n. A n = B n} \<in> \<U>"
   295 by (simp only: expand_set_eq transfer_all transfer_iff transfer_mem)
   296 
   297 lemma transfer_ball [transfer_intro]:
   298   "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
   299     \<Longrightarrow> \<forall>x\<in>a. p x \<equiv> {n. \<forall>x\<in>A n. P n x} \<in> \<U>"
   300 by (simp only: Ball_def transfer_all transfer_imp transfer_mem)
   301 
   302 lemma transfer_bex [transfer_intro]:
   303   "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
   304     \<Longrightarrow> \<exists>x\<in>a. p x \<equiv> {n. \<exists>x\<in>A n. P n x} \<in> \<U>"
   305 by (simp only: Bex_def transfer_ex transfer_conj transfer_mem)
   306 
   307 lemma transfer_Iset [transfer_intro]:
   308   "\<lbrakk>a \<equiv> star_n A\<rbrakk> \<Longrightarrow> Iset a \<equiv> Iset (star_n (\<lambda>n. A n))"
   309 by simp
   310 
   311 text {* Nonstandard extensions of sets. *}
   312 constdefs
   313   starset :: "'a set \<Rightarrow> 'a star set" ("*s* _" [80] 80)
   314   "starset A \<equiv> Iset (star_of A)"
   315 
   316 declare starset_def [transfer_unfold]
   317 
   318 lemma starset_mem: "(star_of x \<in> *s* A) = (x \<in> A)"
   319 by (transfer, rule refl)
   320 
   321 lemma starset_UNIV: "*s* (UNIV::'a set) = (UNIV::'a star set)"
   322 by (transfer UNIV_def, rule refl)
   323 
   324 lemma starset_empty: "*s* {} = {}"
   325 by (transfer empty_def, rule refl)
   326 
   327 lemma starset_insert: "*s* (insert x A) = insert (star_of x) ( *s* A)"
   328 by (transfer insert_def Un_def, rule refl)
   329 
   330 lemma starset_Un: "*s* (A \<union> B) = *s* A \<union> *s* B"
   331 by (transfer Un_def, rule refl)
   332 
   333 lemma starset_Int: "*s* (A \<inter> B) = *s* A \<inter> *s* B"
   334 by (transfer Int_def, rule refl)
   335 
   336 lemma starset_Compl: "*s* -A = -( *s* A)"
   337 by (transfer Compl_def, rule refl)
   338 
   339 lemma starset_diff: "*s* (A - B) = *s* A - *s* B"
   340 by (transfer set_diff_def, rule refl)
   341 
   342 lemma starset_image: "*s* (f ` A) = ( *f* f) ` ( *s* A)"
   343 by (transfer image_def, rule refl)
   344 
   345 lemma starset_vimage: "*s* (f -` A) = ( *f* f) -` ( *s* A)"
   346 by (transfer vimage_def, rule refl)
   347 
   348 lemma starset_subset: "( *s* A \<subseteq> *s* B) = (A \<subseteq> B)"
   349 by (transfer subset_def, rule refl)
   350 
   351 lemma starset_eq: "( *s* A = *s* B) = (A = B)"
   352 by (transfer, rule refl)
   353 
   354 lemmas starset_simps [simp] =
   355   starset_mem     starset_UNIV
   356   starset_empty   starset_insert
   357   starset_Un      starset_Int
   358   starset_Compl   starset_diff
   359   starset_image   starset_vimage
   360   starset_subset  starset_eq
   361 
   362 end