# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1556640212 -3600
# Node ID b21efbf6429208a8c6536dba13f92f19b3795ea5
# Parent  e48c0b5897a6160d5c2817c7d750add34fae1c28
yet more de-applying

diff -r e48c0b5897a6 -r b21efbf64292 src/HOL/Nonstandard_Analysis/HyperNat.thy
--- a/src/HOL/Nonstandard_Analysis/HyperNat.thy	Tue Apr 30 15:49:15 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/HyperNat.thy	Tue Apr 30 17:03:32 2019 +0100
@@ -154,12 +154,14 @@
 lemma hypnat_of_nat_Suc [simp]: "hypnat_of_nat (Suc n) = hypnat_of_nat n + 1"
   by transfer simp
 
-lemma of_nat_eq_add [rule_format]: "\<forall>d::hypnat. of_nat m = of_nat n + d \<longrightarrow> d \<in> range of_nat"
-  apply (induct n)
-   apply (auto simp add: add.assoc)
-  apply (case_tac x)
-   apply (auto simp add: add.commute [of 1])
-  done
+lemma of_nat_eq_add: 
+  fixes d::hypnat
+  shows "of_nat m = of_nat n + d \<Longrightarrow> d \<in> range of_nat"
+proof (induct n arbitrary: d)
+  case (Suc n)
+  then show ?case
+    by (metis Nats_def Nats_eq_Standard Standard_simps(4) hypnat_diff_add_inverse of_nat_in_Nats)
+qed auto
 
 lemma Nats_diff [simp]: "a \<in> Nats \<Longrightarrow> b \<in> Nats \<Longrightarrow> a - b \<in> Nats" for a b :: hypnat
   by (simp add: Nats_eq_Standard)
@@ -224,37 +226,22 @@
   by (simp add: HNatInfinite_def)
 
 lemma Nats_downward_closed: "x \<in> Nats \<Longrightarrow> y \<le> x \<Longrightarrow> y \<in> Nats" for x y :: hypnat
-  apply (simp only: linorder_not_less [symmetric])
-  apply (erule contrapos_np)
-  apply (drule HNatInfinite_not_Nats_iff [THEN iffD2])
-  apply (erule (1) Nats_less_HNatInfinite)
-  done
+  using HNatInfinite_not_Nats_iff Nats_le_HNatInfinite by fastforce
 
 lemma HNatInfinite_upward_closed: "x \<in> HNatInfinite \<Longrightarrow> x \<le> y \<Longrightarrow> y \<in> HNatInfinite"
-  apply (simp only: HNatInfinite_not_Nats_iff)
-  apply (erule contrapos_nn)
-  apply (erule (1) Nats_downward_closed)
-  done
+  using HNatInfinite_not_Nats_iff Nats_downward_closed by blast
 
 lemma HNatInfinite_add: "x \<in> HNatInfinite \<Longrightarrow> x + y \<in> HNatInfinite"
-  apply (erule HNatInfinite_upward_closed)
-  apply (rule hypnat_le_add1)
-  done
+  using HNatInfinite_upward_closed hypnat_le_add1 by blast
 
 lemma HNatInfinite_add_one: "x \<in> HNatInfinite \<Longrightarrow> x + 1 \<in> HNatInfinite"
   by (rule HNatInfinite_add)
 
-lemma HNatInfinite_diff: "x \<in> HNatInfinite \<Longrightarrow> y \<in> Nats \<Longrightarrow> x - y \<in> HNatInfinite"
-  apply (frule (1) Nats_le_HNatInfinite)
-  apply (simp only: HNatInfinite_not_Nats_iff)
-  apply (erule contrapos_nn)
-  apply (drule (1) Nats_add, simp)
-  done
+lemma HNatInfinite_diff: "\<lbrakk>x \<in> HNatInfinite; y \<in> Nats\<rbrakk> \<Longrightarrow> x - y \<in> HNatInfinite"
+  by (metis HNatInfinite_not_Nats_iff Nats_add Nats_le_HNatInfinite le_add_diff_inverse)
 
 lemma HNatInfinite_is_Suc: "x \<in> HNatInfinite \<Longrightarrow> \<exists>y. x = y + 1" for x :: hypnat
-  apply (rule_tac x = "x - (1::hypnat) " in exI)
-  apply (simp add: Nats_le_HNatInfinite)
-  done
+  using hypnat_gt_zero_iff2 zero_less_HNatInfinite by blast
 
 
 subsection \<open>Existence of an infinite hypernatural number\<close>
@@ -308,32 +295,29 @@
 
 text \<open>\<^term>\<open>HNatInfinite = {N. \<forall>n \<in> Nats. n < N}\<close>\<close>
 
-(*??delete? similar reasoning in hypnat_omega_gt_SHNat above*)
-lemma HNatInfinite_FreeUltrafilterNat_lemma:
-  assumes "\<forall>N::nat. eventually (\<lambda>n. f n \<noteq> N) \<U>"
-  shows "eventually (\<lambda>n. N < f n) \<U>"
-  apply (induct N)
-  using assms
-   apply (drule_tac x = 0 in spec, simp)
-  using assms
-  apply (drule_tac x = "Suc N" in spec)
-  apply (auto elim: eventually_elim2)
-  done
+text\<open>unused, but possibly interesting\<close>
+lemma HNatInfinite_FreeUltrafilterNat_eventually:
+  assumes "\<And>k::nat. eventually (\<lambda>n. f n \<noteq> k) \<U>"
+  shows "eventually (\<lambda>n. m < f n) \<U>"
+proof (induct m)
+  case 0
+  then show ?case
+    using assms eventually_mono by fastforce
+next
+  case (Suc m)
+  then show ?case
+    using assms [of "Suc m"] eventually_elim2 by fastforce
+qed
 
 lemma HNatInfinite_iff: "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"
-  apply (safe intro!: Nats_less_HNatInfinite)
-  apply (auto simp add: HNatInfinite_def)
-  done
+  using HNatInfinite_def Nats_less_HNatInfinite by auto
 
 
 subsubsection \<open>Alternative Characterization of \<^term>\<open>HNatInfinite\<close> using Free Ultrafilter\<close>
 
 lemma HNatInfinite_FreeUltrafilterNat:
   "star_n X \<in> HNatInfinite \<Longrightarrow> \<forall>u. eventually (\<lambda>n. u < X n) \<U>"
-  apply (auto simp add: HNatInfinite_iff SHNat_eq)
-  apply (drule_tac x="star_of u" in spec, simp)
-  apply (simp add: star_of_def star_less_def starP2_star_n)
-  done
+  by (metis (full_types) starP2_star_of starP_star_n star_less_def star_of_less_HNatInfinite)
 
 lemma FreeUltrafilterNat_HNatInfinite:
   "\<forall>u. eventually (\<lambda>n. u < X n) \<U> \<Longrightarrow> star_n X \<in> HNatInfinite"
diff -r e48c0b5897a6 -r b21efbf64292 src/HOL/Nonstandard_Analysis/NatStar.thy
--- a/src/HOL/Nonstandard_Analysis/NatStar.thy	Tue Apr 30 15:49:15 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/NatStar.thy	Tue Apr 30 17:03:32 2019 +0100
@@ -15,33 +15,49 @@
   by (simp add: hypnat_omega_def starfun_def star_of_def Ifun_star_n)
 
 lemma starset_n_Un: "*sn* (\<lambda>n. (A n) \<union> (B n)) = *sn* A \<union> *sn* B"
-  apply (simp add: starset_n_def star_n_eq_starfun_whn Un_def)
-  apply (rule_tac x=whn in spec, transfer, simp)
-  done
+proof -
+  have "\<And>N. Iset ((*f* (\<lambda>n. {x. x \<in> A n \<or> x \<in> B n})) N) =
+    {x. x \<in> Iset ((*f* A) N) \<or> x \<in> Iset ((*f* B) N)}"
+    by transfer simp
+  then show ?thesis
+    by (simp add: starset_n_def star_n_eq_starfun_whn Un_def)
+qed
 
 lemma InternalSets_Un: "X \<in> InternalSets \<Longrightarrow> Y \<in> InternalSets \<Longrightarrow> X \<union> Y \<in> InternalSets"
   by (auto simp add: InternalSets_def starset_n_Un [symmetric])
 
 lemma starset_n_Int: "*sn* (\<lambda>n. A n \<inter> B n) = *sn* A \<inter> *sn* B"
-  apply (simp add: starset_n_def star_n_eq_starfun_whn Int_def)
-  apply (rule_tac x=whn in spec, transfer, simp)
-  done
+proof -
+  have "\<And>N. Iset ((*f* (\<lambda>n. {x. x \<in> A n \<and> x \<in> B n})) N) =
+    {x. x \<in> Iset ((*f* A) N) \<and> x \<in> Iset ((*f* B) N)}"
+    by transfer simp
+  then show ?thesis
+    by (simp add: starset_n_def star_n_eq_starfun_whn Int_def)
+qed
 
 lemma InternalSets_Int: "X \<in> InternalSets \<Longrightarrow> Y \<in> InternalSets \<Longrightarrow> X \<inter> Y \<in> InternalSets"
   by (auto simp add: InternalSets_def starset_n_Int [symmetric])
 
 lemma starset_n_Compl: "*sn* ((\<lambda>n. - A n)) = - ( *sn* A)"
-  apply (simp add: starset_n_def star_n_eq_starfun_whn Compl_eq)
-  apply (rule_tac x=whn in spec, transfer, simp)
-  done
+proof -
+  have "\<And>N. Iset ((*f* (\<lambda>n. {x. x \<notin> A n})) N) =
+    {x. x \<notin> Iset ((*f* A) N)}"
+    by transfer simp
+  then show ?thesis
+    by (simp add: starset_n_def star_n_eq_starfun_whn Compl_eq)
+qed
 
 lemma InternalSets_Compl: "X \<in> InternalSets \<Longrightarrow> - X \<in> InternalSets"
   by (auto simp add: InternalSets_def starset_n_Compl [symmetric])
 
 lemma starset_n_diff: "*sn* (\<lambda>n. (A n) - (B n)) = *sn* A - *sn* B"
-  apply (simp add: starset_n_def star_n_eq_starfun_whn set_diff_eq)
-  apply (rule_tac x=whn in spec, transfer, simp)
-  done
+proof -
+  have "\<And>N. Iset ((*f* (\<lambda>n. {x. x \<in> A n \<and> x \<notin> B n})) N) =
+    {x. x \<in> Iset ((*f* A) N) \<and> x \<notin> Iset ((*f* B) N)}"
+    by transfer simp
+  then show ?thesis
+    by (simp add: starset_n_def star_n_eq_starfun_whn set_diff_eq)
+qed
 
 lemma InternalSets_diff: "X \<in> InternalSets \<Longrightarrow> Y \<in> InternalSets \<Longrightarrow> X - Y \<in> InternalSets"
   by (auto simp add: InternalSets_def starset_n_diff [symmetric])
@@ -59,9 +75,7 @@
   by (auto simp add: InternalSets_def starset_starset_n_eq)
 
 lemma InternalSets_UNIV_diff: "X \<in> InternalSets \<Longrightarrow> UNIV - X \<in> InternalSets"
-  apply (subgoal_tac "UNIV - X = - X")
-   apply (auto intro: InternalSets_Compl)
-  done
+  by (simp add: InternalSets_Compl diff_eq)
 
 
 subsection \<open>Nonstandard Extensions of Functions\<close>
@@ -104,10 +118,7 @@
 
 lemma starfun_inverse_real_of_nat_eq:
   "N \<in> HNatInfinite \<Longrightarrow> ( *f* (\<lambda>x::nat. inverse (real x))) N = inverse (hypreal_of_hypnat N)"
-  apply (rule_tac f1 = inverse in starfun_o2 [THEN subst])
-  apply (subgoal_tac "hypreal_of_hypnat N \<noteq> 0")
-   apply (simp_all add: zero_less_HNatInfinite starfunNat_real_of_nat)
-  done
+  by (metis of_hypnat_def starfun_inverse2)
 
 text \<open>Internal functions -- some redundancy with \<open>*f*\<close> now.\<close>
 
@@ -144,10 +155,7 @@
 
 lemma starfunNat_inverse_real_of_nat_Infinitesimal [simp]:
   "N \<in> HNatInfinite \<Longrightarrow> ( *f* (\<lambda>x. inverse (real x))) N \<in> Infinitesimal"
-  apply (rule_tac f1 = inverse in starfun_o2 [THEN subst])
-  apply (subgoal_tac "hypreal_of_hypnat N \<noteq> 0")
-   apply (simp_all add: zero_less_HNatInfinite starfunNat_real_of_nat)
-  done
+  using starfun_inverse_real_of_nat_eq by auto
 
 
 subsection \<open>Nonstandard Characterization of Induction\<close>
@@ -166,23 +174,22 @@
 lemma starP2_eq_iff2: "( *p2* (\<lambda>x y. x = y)) X Y \<longleftrightarrow> X = Y"
   by (simp add: starP2_eq_iff)
 
-lemma nonempty_nat_set_Least_mem: "c \<in> S \<Longrightarrow> (LEAST n. n \<in> S) \<in> S"
-  for S :: "nat set"
-  by (erule LeastI)
+lemma nonempty_set_star_has_least_lemma:
+  "\<exists>n\<in>S. \<forall>m\<in>S. n \<le> m" if "S \<noteq> {}" for S :: "nat set"
+proof
+  show "\<forall>m\<in>S. (LEAST n. n \<in> S) \<le> m"
+    by (simp add: Least_le)
+  show "(LEAST n. n \<in> S) \<in> S"
+    by (meson that LeastI_ex equals0I)
+qed
 
 lemma nonempty_set_star_has_least:
   "\<And>S::nat set star. Iset S \<noteq> {} \<Longrightarrow> \<exists>n \<in> Iset S. \<forall>m \<in> Iset S. n \<le> m"
-  apply (transfer empty_def)
-  apply (rule_tac x="LEAST n. n \<in> S" in bexI)
-   apply (simp add: Least_le)
-  apply (rule LeastI_ex, auto)
-  done
+  using nonempty_set_star_has_least_lemma by (transfer empty_def)
 
 lemma nonempty_InternalNatSet_has_least: "S \<in> InternalSets \<Longrightarrow> S \<noteq> {} \<Longrightarrow> \<exists>n \<in> S. \<forall>m \<in> S. n \<le> m"
   for S :: "hypnat set"
-  apply (clarsimp simp add: InternalSets_def starset_n_def)
-  apply (erule nonempty_set_star_has_least)
-  done
+  by (force simp add: InternalSets_def starset_n_def dest!: nonempty_set_star_has_least)
 
 text \<open>Goldblatt, page 129 Thm 11.3.2.\<close>
 lemma internal_induct_lemma:
diff -r e48c0b5897a6 -r b21efbf64292 src/HOL/Nonstandard_Analysis/StarDef.thy
--- a/src/HOL/Nonstandard_Analysis/StarDef.thy	Tue Apr 30 15:49:15 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/StarDef.thy	Tue Apr 30 17:03:32 2019 +0100
@@ -14,11 +14,8 @@
   where "\<U> = (SOME U. freeultrafilter U)"
 
 lemma freeultrafilter_FreeUltrafilterNat: "freeultrafilter \<U>"
-  apply (unfold FreeUltrafilterNat_def)
-  apply (rule someI_ex)
-  apply (rule freeultrafilter_Ex)
-  apply (rule infinite_UNIV_nat)
-  done
+  unfolding FreeUltrafilterNat_def
+  by (simp add: freeultrafilter_Ex someI_ex)
 
 interpretation FreeUltrafilterNat: freeultrafilter \<U>
   by (rule freeultrafilter_FreeUltrafilterNat)
@@ -42,16 +39,10 @@
   by (cases x) (auto simp: star_n_def star_def elim: quotientE)
 
 lemma all_star_eq: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>X. P (star_n X))"
-  apply auto
-  apply (rule_tac x = x in star_cases)
-  apply simp
-  done
+  by (metis star_cases)
 
 lemma ex_star_eq: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>X. P (star_n X))"
-  apply auto
-  apply (rule_tac x=x in star_cases)
-  apply auto
-  done
+  by (metis star_cases)
 
 text \<open>Proving that \<^term>\<open>starrel\<close> is an equivalence relation.\<close>
 
@@ -599,12 +590,16 @@
 subsection \<open>Ordering and lattice classes\<close>
 
 instance star :: (order) order
-  apply intro_classes
-     apply (transfer, rule less_le_not_le)
-    apply (transfer, rule order_refl)
-   apply (transfer, erule (1) order_trans)
-  apply (transfer, erule (1) order_antisym)
-  done
+proof 
+  show "\<And>x y::'a star. (x < y) = (x \<le> y \<and> \<not> y \<le> x)"
+    by transfer (rule less_le_not_le)
+  show "\<And>x::'a star. x \<le> x"
+    by transfer (rule order_refl)
+  show "\<And>x y z::'a star. \<lbrakk>x \<le> y; y \<le> z\<rbrakk> \<Longrightarrow> x \<le> z"
+    by transfer (rule order_trans)
+  show "\<And>x y::'a star. \<lbrakk>x \<le> y; y \<le> x\<rbrakk> \<Longrightarrow> x = y"
+    by transfer (rule order_antisym)
+qed
 
 instantiation star :: (semilattice_inf) semilattice_inf
 begin
@@ -639,16 +634,12 @@
   by (intro_classes, transfer, rule linorder_linear)
 
 lemma star_max_def [transfer_unfold]: "max = *f2* max"
-  apply (rule ext, rule ext)
-  apply (unfold max_def, transfer, fold max_def)
-  apply (rule refl)
-  done
+  unfolding max_def
+  by (intro ext, transfer, simp)
 
 lemma star_min_def [transfer_unfold]: "min = *f2* min"
-  apply (rule ext, rule ext)
-  apply (unfold min_def, transfer, fold min_def)
-  apply (rule refl)
-  done
+  unfolding min_def
+  by (intro ext, transfer, simp)
 
 lemma Standard_max [simp]: "x \<in> Standard \<Longrightarrow> y \<in> Standard \<Longrightarrow> max x y \<in> Standard"
   by (simp add: star_max_def)
@@ -928,10 +919,9 @@
   by (erule finite_induct) simp_all
 
 instance star :: (finite) finite
-  apply intro_classes
-  apply (subst starset_UNIV [symmetric])
-  apply (subst starset_finite [OF finite])
-  apply (rule finite_imageI [OF finite])
-  done
+proof intro_classes
+  show "finite (UNIV::'a star set)"
+    by (metis starset_UNIV finite finite_imageI starset_finite)
+qed
 
 end