yet more de-applying
authorpaulson <lp15@cam.ac.uk>
Tue Apr 30 17:03:32 2019 +0100 (6 months ago)
changeset 70219b21efbf64292
parent 70218 e48c0b5897a6
child 70220 089753519be0
child 70222 bde8ccb73fd2
yet more de-applying
src/HOL/Nonstandard_Analysis/HyperNat.thy
src/HOL/Nonstandard_Analysis/NatStar.thy
src/HOL/Nonstandard_Analysis/StarDef.thy
     1.1 --- a/src/HOL/Nonstandard_Analysis/HyperNat.thy	Tue Apr 30 15:49:15 2019 +0100
     1.2 +++ b/src/HOL/Nonstandard_Analysis/HyperNat.thy	Tue Apr 30 17:03:32 2019 +0100
     1.3 @@ -154,12 +154,14 @@
     1.4  lemma hypnat_of_nat_Suc [simp]: "hypnat_of_nat (Suc n) = hypnat_of_nat n + 1"
     1.5    by transfer simp
     1.6  
     1.7 -lemma of_nat_eq_add [rule_format]: "\<forall>d::hypnat. of_nat m = of_nat n + d \<longrightarrow> d \<in> range of_nat"
     1.8 -  apply (induct n)
     1.9 -   apply (auto simp add: add.assoc)
    1.10 -  apply (case_tac x)
    1.11 -   apply (auto simp add: add.commute [of 1])
    1.12 -  done
    1.13 +lemma of_nat_eq_add: 
    1.14 +  fixes d::hypnat
    1.15 +  shows "of_nat m = of_nat n + d \<Longrightarrow> d \<in> range of_nat"
    1.16 +proof (induct n arbitrary: d)
    1.17 +  case (Suc n)
    1.18 +  then show ?case
    1.19 +    by (metis Nats_def Nats_eq_Standard Standard_simps(4) hypnat_diff_add_inverse of_nat_in_Nats)
    1.20 +qed auto
    1.21  
    1.22  lemma Nats_diff [simp]: "a \<in> Nats \<Longrightarrow> b \<in> Nats \<Longrightarrow> a - b \<in> Nats" for a b :: hypnat
    1.23    by (simp add: Nats_eq_Standard)
    1.24 @@ -224,37 +226,22 @@
    1.25    by (simp add: HNatInfinite_def)
    1.26  
    1.27  lemma Nats_downward_closed: "x \<in> Nats \<Longrightarrow> y \<le> x \<Longrightarrow> y \<in> Nats" for x y :: hypnat
    1.28 -  apply (simp only: linorder_not_less [symmetric])
    1.29 -  apply (erule contrapos_np)
    1.30 -  apply (drule HNatInfinite_not_Nats_iff [THEN iffD2])
    1.31 -  apply (erule (1) Nats_less_HNatInfinite)
    1.32 -  done
    1.33 +  using HNatInfinite_not_Nats_iff Nats_le_HNatInfinite by fastforce
    1.34  
    1.35  lemma HNatInfinite_upward_closed: "x \<in> HNatInfinite \<Longrightarrow> x \<le> y \<Longrightarrow> y \<in> HNatInfinite"
    1.36 -  apply (simp only: HNatInfinite_not_Nats_iff)
    1.37 -  apply (erule contrapos_nn)
    1.38 -  apply (erule (1) Nats_downward_closed)
    1.39 -  done
    1.40 +  using HNatInfinite_not_Nats_iff Nats_downward_closed by blast
    1.41  
    1.42  lemma HNatInfinite_add: "x \<in> HNatInfinite \<Longrightarrow> x + y \<in> HNatInfinite"
    1.43 -  apply (erule HNatInfinite_upward_closed)
    1.44 -  apply (rule hypnat_le_add1)
    1.45 -  done
    1.46 +  using HNatInfinite_upward_closed hypnat_le_add1 by blast
    1.47  
    1.48  lemma HNatInfinite_add_one: "x \<in> HNatInfinite \<Longrightarrow> x + 1 \<in> HNatInfinite"
    1.49    by (rule HNatInfinite_add)
    1.50  
    1.51 -lemma HNatInfinite_diff: "x \<in> HNatInfinite \<Longrightarrow> y \<in> Nats \<Longrightarrow> x - y \<in> HNatInfinite"
    1.52 -  apply (frule (1) Nats_le_HNatInfinite)
    1.53 -  apply (simp only: HNatInfinite_not_Nats_iff)
    1.54 -  apply (erule contrapos_nn)
    1.55 -  apply (drule (1) Nats_add, simp)
    1.56 -  done
    1.57 +lemma HNatInfinite_diff: "\<lbrakk>x \<in> HNatInfinite; y \<in> Nats\<rbrakk> \<Longrightarrow> x - y \<in> HNatInfinite"
    1.58 +  by (metis HNatInfinite_not_Nats_iff Nats_add Nats_le_HNatInfinite le_add_diff_inverse)
    1.59  
    1.60  lemma HNatInfinite_is_Suc: "x \<in> HNatInfinite \<Longrightarrow> \<exists>y. x = y + 1" for x :: hypnat
    1.61 -  apply (rule_tac x = "x - (1::hypnat) " in exI)
    1.62 -  apply (simp add: Nats_le_HNatInfinite)
    1.63 -  done
    1.64 +  using hypnat_gt_zero_iff2 zero_less_HNatInfinite by blast
    1.65  
    1.66  
    1.67  subsection \<open>Existence of an infinite hypernatural number\<close>
    1.68 @@ -308,32 +295,29 @@
    1.69  
    1.70  text \<open>\<^term>\<open>HNatInfinite = {N. \<forall>n \<in> Nats. n < N}\<close>\<close>
    1.71  
    1.72 -(*??delete? similar reasoning in hypnat_omega_gt_SHNat above*)
    1.73 -lemma HNatInfinite_FreeUltrafilterNat_lemma:
    1.74 -  assumes "\<forall>N::nat. eventually (\<lambda>n. f n \<noteq> N) \<U>"
    1.75 -  shows "eventually (\<lambda>n. N < f n) \<U>"
    1.76 -  apply (induct N)
    1.77 -  using assms
    1.78 -   apply (drule_tac x = 0 in spec, simp)
    1.79 -  using assms
    1.80 -  apply (drule_tac x = "Suc N" in spec)
    1.81 -  apply (auto elim: eventually_elim2)
    1.82 -  done
    1.83 +text\<open>unused, but possibly interesting\<close>
    1.84 +lemma HNatInfinite_FreeUltrafilterNat_eventually:
    1.85 +  assumes "\<And>k::nat. eventually (\<lambda>n. f n \<noteq> k) \<U>"
    1.86 +  shows "eventually (\<lambda>n. m < f n) \<U>"
    1.87 +proof (induct m)
    1.88 +  case 0
    1.89 +  then show ?case
    1.90 +    using assms eventually_mono by fastforce
    1.91 +next
    1.92 +  case (Suc m)
    1.93 +  then show ?case
    1.94 +    using assms [of "Suc m"] eventually_elim2 by fastforce
    1.95 +qed
    1.96  
    1.97  lemma HNatInfinite_iff: "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"
    1.98 -  apply (safe intro!: Nats_less_HNatInfinite)
    1.99 -  apply (auto simp add: HNatInfinite_def)
   1.100 -  done
   1.101 +  using HNatInfinite_def Nats_less_HNatInfinite by auto
   1.102  
   1.103  
   1.104  subsubsection \<open>Alternative Characterization of \<^term>\<open>HNatInfinite\<close> using Free Ultrafilter\<close>
   1.105  
   1.106  lemma HNatInfinite_FreeUltrafilterNat:
   1.107    "star_n X \<in> HNatInfinite \<Longrightarrow> \<forall>u. eventually (\<lambda>n. u < X n) \<U>"
   1.108 -  apply (auto simp add: HNatInfinite_iff SHNat_eq)
   1.109 -  apply (drule_tac x="star_of u" in spec, simp)
   1.110 -  apply (simp add: star_of_def star_less_def starP2_star_n)
   1.111 -  done
   1.112 +  by (metis (full_types) starP2_star_of starP_star_n star_less_def star_of_less_HNatInfinite)
   1.113  
   1.114  lemma FreeUltrafilterNat_HNatInfinite:
   1.115    "\<forall>u. eventually (\<lambda>n. u < X n) \<U> \<Longrightarrow> star_n X \<in> HNatInfinite"
     2.1 --- a/src/HOL/Nonstandard_Analysis/NatStar.thy	Tue Apr 30 15:49:15 2019 +0100
     2.2 +++ b/src/HOL/Nonstandard_Analysis/NatStar.thy	Tue Apr 30 17:03:32 2019 +0100
     2.3 @@ -15,33 +15,49 @@
     2.4    by (simp add: hypnat_omega_def starfun_def star_of_def Ifun_star_n)
     2.5  
     2.6  lemma starset_n_Un: "*sn* (\<lambda>n. (A n) \<union> (B n)) = *sn* A \<union> *sn* B"
     2.7 -  apply (simp add: starset_n_def star_n_eq_starfun_whn Un_def)
     2.8 -  apply (rule_tac x=whn in spec, transfer, simp)
     2.9 -  done
    2.10 +proof -
    2.11 +  have "\<And>N. Iset ((*f* (\<lambda>n. {x. x \<in> A n \<or> x \<in> B n})) N) =
    2.12 +    {x. x \<in> Iset ((*f* A) N) \<or> x \<in> Iset ((*f* B) N)}"
    2.13 +    by transfer simp
    2.14 +  then show ?thesis
    2.15 +    by (simp add: starset_n_def star_n_eq_starfun_whn Un_def)
    2.16 +qed
    2.17  
    2.18  lemma InternalSets_Un: "X \<in> InternalSets \<Longrightarrow> Y \<in> InternalSets \<Longrightarrow> X \<union> Y \<in> InternalSets"
    2.19    by (auto simp add: InternalSets_def starset_n_Un [symmetric])
    2.20  
    2.21  lemma starset_n_Int: "*sn* (\<lambda>n. A n \<inter> B n) = *sn* A \<inter> *sn* B"
    2.22 -  apply (simp add: starset_n_def star_n_eq_starfun_whn Int_def)
    2.23 -  apply (rule_tac x=whn in spec, transfer, simp)
    2.24 -  done
    2.25 +proof -
    2.26 +  have "\<And>N. Iset ((*f* (\<lambda>n. {x. x \<in> A n \<and> x \<in> B n})) N) =
    2.27 +    {x. x \<in> Iset ((*f* A) N) \<and> x \<in> Iset ((*f* B) N)}"
    2.28 +    by transfer simp
    2.29 +  then show ?thesis
    2.30 +    by (simp add: starset_n_def star_n_eq_starfun_whn Int_def)
    2.31 +qed
    2.32  
    2.33  lemma InternalSets_Int: "X \<in> InternalSets \<Longrightarrow> Y \<in> InternalSets \<Longrightarrow> X \<inter> Y \<in> InternalSets"
    2.34    by (auto simp add: InternalSets_def starset_n_Int [symmetric])
    2.35  
    2.36  lemma starset_n_Compl: "*sn* ((\<lambda>n. - A n)) = - ( *sn* A)"
    2.37 -  apply (simp add: starset_n_def star_n_eq_starfun_whn Compl_eq)
    2.38 -  apply (rule_tac x=whn in spec, transfer, simp)
    2.39 -  done
    2.40 +proof -
    2.41 +  have "\<And>N. Iset ((*f* (\<lambda>n. {x. x \<notin> A n})) N) =
    2.42 +    {x. x \<notin> Iset ((*f* A) N)}"
    2.43 +    by transfer simp
    2.44 +  then show ?thesis
    2.45 +    by (simp add: starset_n_def star_n_eq_starfun_whn Compl_eq)
    2.46 +qed
    2.47  
    2.48  lemma InternalSets_Compl: "X \<in> InternalSets \<Longrightarrow> - X \<in> InternalSets"
    2.49    by (auto simp add: InternalSets_def starset_n_Compl [symmetric])
    2.50  
    2.51  lemma starset_n_diff: "*sn* (\<lambda>n. (A n) - (B n)) = *sn* A - *sn* B"
    2.52 -  apply (simp add: starset_n_def star_n_eq_starfun_whn set_diff_eq)
    2.53 -  apply (rule_tac x=whn in spec, transfer, simp)
    2.54 -  done
    2.55 +proof -
    2.56 +  have "\<And>N. Iset ((*f* (\<lambda>n. {x. x \<in> A n \<and> x \<notin> B n})) N) =
    2.57 +    {x. x \<in> Iset ((*f* A) N) \<and> x \<notin> Iset ((*f* B) N)}"
    2.58 +    by transfer simp
    2.59 +  then show ?thesis
    2.60 +    by (simp add: starset_n_def star_n_eq_starfun_whn set_diff_eq)
    2.61 +qed
    2.62  
    2.63  lemma InternalSets_diff: "X \<in> InternalSets \<Longrightarrow> Y \<in> InternalSets \<Longrightarrow> X - Y \<in> InternalSets"
    2.64    by (auto simp add: InternalSets_def starset_n_diff [symmetric])
    2.65 @@ -59,9 +75,7 @@
    2.66    by (auto simp add: InternalSets_def starset_starset_n_eq)
    2.67  
    2.68  lemma InternalSets_UNIV_diff: "X \<in> InternalSets \<Longrightarrow> UNIV - X \<in> InternalSets"
    2.69 -  apply (subgoal_tac "UNIV - X = - X")
    2.70 -   apply (auto intro: InternalSets_Compl)
    2.71 -  done
    2.72 +  by (simp add: InternalSets_Compl diff_eq)
    2.73  
    2.74  
    2.75  subsection \<open>Nonstandard Extensions of Functions\<close>
    2.76 @@ -104,10 +118,7 @@
    2.77  
    2.78  lemma starfun_inverse_real_of_nat_eq:
    2.79    "N \<in> HNatInfinite \<Longrightarrow> ( *f* (\<lambda>x::nat. inverse (real x))) N = inverse (hypreal_of_hypnat N)"
    2.80 -  apply (rule_tac f1 = inverse in starfun_o2 [THEN subst])
    2.81 -  apply (subgoal_tac "hypreal_of_hypnat N \<noteq> 0")
    2.82 -   apply (simp_all add: zero_less_HNatInfinite starfunNat_real_of_nat)
    2.83 -  done
    2.84 +  by (metis of_hypnat_def starfun_inverse2)
    2.85  
    2.86  text \<open>Internal functions -- some redundancy with \<open>*f*\<close> now.\<close>
    2.87  
    2.88 @@ -144,10 +155,7 @@
    2.89  
    2.90  lemma starfunNat_inverse_real_of_nat_Infinitesimal [simp]:
    2.91    "N \<in> HNatInfinite \<Longrightarrow> ( *f* (\<lambda>x. inverse (real x))) N \<in> Infinitesimal"
    2.92 -  apply (rule_tac f1 = inverse in starfun_o2 [THEN subst])
    2.93 -  apply (subgoal_tac "hypreal_of_hypnat N \<noteq> 0")
    2.94 -   apply (simp_all add: zero_less_HNatInfinite starfunNat_real_of_nat)
    2.95 -  done
    2.96 +  using starfun_inverse_real_of_nat_eq by auto
    2.97  
    2.98  
    2.99  subsection \<open>Nonstandard Characterization of Induction\<close>
   2.100 @@ -166,23 +174,22 @@
   2.101  lemma starP2_eq_iff2: "( *p2* (\<lambda>x y. x = y)) X Y \<longleftrightarrow> X = Y"
   2.102    by (simp add: starP2_eq_iff)
   2.103  
   2.104 -lemma nonempty_nat_set_Least_mem: "c \<in> S \<Longrightarrow> (LEAST n. n \<in> S) \<in> S"
   2.105 -  for S :: "nat set"
   2.106 -  by (erule LeastI)
   2.107 +lemma nonempty_set_star_has_least_lemma:
   2.108 +  "\<exists>n\<in>S. \<forall>m\<in>S. n \<le> m" if "S \<noteq> {}" for S :: "nat set"
   2.109 +proof
   2.110 +  show "\<forall>m\<in>S. (LEAST n. n \<in> S) \<le> m"
   2.111 +    by (simp add: Least_le)
   2.112 +  show "(LEAST n. n \<in> S) \<in> S"
   2.113 +    by (meson that LeastI_ex equals0I)
   2.114 +qed
   2.115  
   2.116  lemma nonempty_set_star_has_least:
   2.117    "\<And>S::nat set star. Iset S \<noteq> {} \<Longrightarrow> \<exists>n \<in> Iset S. \<forall>m \<in> Iset S. n \<le> m"
   2.118 -  apply (transfer empty_def)
   2.119 -  apply (rule_tac x="LEAST n. n \<in> S" in bexI)
   2.120 -   apply (simp add: Least_le)
   2.121 -  apply (rule LeastI_ex, auto)
   2.122 -  done
   2.123 +  using nonempty_set_star_has_least_lemma by (transfer empty_def)
   2.124  
   2.125  lemma nonempty_InternalNatSet_has_least: "S \<in> InternalSets \<Longrightarrow> S \<noteq> {} \<Longrightarrow> \<exists>n \<in> S. \<forall>m \<in> S. n \<le> m"
   2.126    for S :: "hypnat set"
   2.127 -  apply (clarsimp simp add: InternalSets_def starset_n_def)
   2.128 -  apply (erule nonempty_set_star_has_least)
   2.129 -  done
   2.130 +  by (force simp add: InternalSets_def starset_n_def dest!: nonempty_set_star_has_least)
   2.131  
   2.132  text \<open>Goldblatt, page 129 Thm 11.3.2.\<close>
   2.133  lemma internal_induct_lemma:
     3.1 --- a/src/HOL/Nonstandard_Analysis/StarDef.thy	Tue Apr 30 15:49:15 2019 +0100
     3.2 +++ b/src/HOL/Nonstandard_Analysis/StarDef.thy	Tue Apr 30 17:03:32 2019 +0100
     3.3 @@ -14,11 +14,8 @@
     3.4    where "\<U> = (SOME U. freeultrafilter U)"
     3.5  
     3.6  lemma freeultrafilter_FreeUltrafilterNat: "freeultrafilter \<U>"
     3.7 -  apply (unfold FreeUltrafilterNat_def)
     3.8 -  apply (rule someI_ex)
     3.9 -  apply (rule freeultrafilter_Ex)
    3.10 -  apply (rule infinite_UNIV_nat)
    3.11 -  done
    3.12 +  unfolding FreeUltrafilterNat_def
    3.13 +  by (simp add: freeultrafilter_Ex someI_ex)
    3.14  
    3.15  interpretation FreeUltrafilterNat: freeultrafilter \<U>
    3.16    by (rule freeultrafilter_FreeUltrafilterNat)
    3.17 @@ -42,16 +39,10 @@
    3.18    by (cases x) (auto simp: star_n_def star_def elim: quotientE)
    3.19  
    3.20  lemma all_star_eq: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>X. P (star_n X))"
    3.21 -  apply auto
    3.22 -  apply (rule_tac x = x in star_cases)
    3.23 -  apply simp
    3.24 -  done
    3.25 +  by (metis star_cases)
    3.26  
    3.27  lemma ex_star_eq: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>X. P (star_n X))"
    3.28 -  apply auto
    3.29 -  apply (rule_tac x=x in star_cases)
    3.30 -  apply auto
    3.31 -  done
    3.32 +  by (metis star_cases)
    3.33  
    3.34  text \<open>Proving that \<^term>\<open>starrel\<close> is an equivalence relation.\<close>
    3.35  
    3.36 @@ -599,12 +590,16 @@
    3.37  subsection \<open>Ordering and lattice classes\<close>
    3.38  
    3.39  instance star :: (order) order
    3.40 -  apply intro_classes
    3.41 -     apply (transfer, rule less_le_not_le)
    3.42 -    apply (transfer, rule order_refl)
    3.43 -   apply (transfer, erule (1) order_trans)
    3.44 -  apply (transfer, erule (1) order_antisym)
    3.45 -  done
    3.46 +proof 
    3.47 +  show "\<And>x y::'a star. (x < y) = (x \<le> y \<and> \<not> y \<le> x)"
    3.48 +    by transfer (rule less_le_not_le)
    3.49 +  show "\<And>x::'a star. x \<le> x"
    3.50 +    by transfer (rule order_refl)
    3.51 +  show "\<And>x y z::'a star. \<lbrakk>x \<le> y; y \<le> z\<rbrakk> \<Longrightarrow> x \<le> z"
    3.52 +    by transfer (rule order_trans)
    3.53 +  show "\<And>x y::'a star. \<lbrakk>x \<le> y; y \<le> x\<rbrakk> \<Longrightarrow> x = y"
    3.54 +    by transfer (rule order_antisym)
    3.55 +qed
    3.56  
    3.57  instantiation star :: (semilattice_inf) semilattice_inf
    3.58  begin
    3.59 @@ -639,16 +634,12 @@
    3.60    by (intro_classes, transfer, rule linorder_linear)
    3.61  
    3.62  lemma star_max_def [transfer_unfold]: "max = *f2* max"
    3.63 -  apply (rule ext, rule ext)
    3.64 -  apply (unfold max_def, transfer, fold max_def)
    3.65 -  apply (rule refl)
    3.66 -  done
    3.67 +  unfolding max_def
    3.68 +  by (intro ext, transfer, simp)
    3.69  
    3.70  lemma star_min_def [transfer_unfold]: "min = *f2* min"
    3.71 -  apply (rule ext, rule ext)
    3.72 -  apply (unfold min_def, transfer, fold min_def)
    3.73 -  apply (rule refl)
    3.74 -  done
    3.75 +  unfolding min_def
    3.76 +  by (intro ext, transfer, simp)
    3.77  
    3.78  lemma Standard_max [simp]: "x \<in> Standard \<Longrightarrow> y \<in> Standard \<Longrightarrow> max x y \<in> Standard"
    3.79    by (simp add: star_max_def)
    3.80 @@ -928,10 +919,9 @@
    3.81    by (erule finite_induct) simp_all
    3.82  
    3.83  instance star :: (finite) finite
    3.84 -  apply intro_classes
    3.85 -  apply (subst starset_UNIV [symmetric])
    3.86 -  apply (subst starset_finite [OF finite])
    3.87 -  apply (rule finite_imageI [OF finite])
    3.88 -  done
    3.89 +proof intro_classes
    3.90 +  show "finite (UNIV::'a star set)"
    3.91 +    by (metis starset_UNIV finite finite_imageI starset_finite)
    3.92 +qed
    3.93  
    3.94  end