src/HOL/Hyperreal/HyperNat.thy

 
 text{*Proving that @{term hypnatrel} is an equivalence relation*}
 
 lemma hypnatrel_iff:
      "((X,Y) \<in> hypnatrel) = ({n. X n = Y n}: FreeUltrafilterNat)"
-apply (unfold hypnatrel_def, fast)
+apply (simp add: hypnatrel_def)
 done
 
 lemma hypnatrel_refl: "(x,x) \<in> hypnatrel"
-by (unfold hypnatrel_def, auto)
+by (simp add: hypnatrel_def)
 
 lemma hypnatrel_sym: "(x,y) \<in> hypnatrel ==> (y,x) \<in> hypnatrel"
 by (auto simp add: hypnatrel_def eq_commute)
 
 lemma hypnatrel_trans [rule_format (no_asm)]:
      "(x,y) \<in> hypnatrel --> (y,z) \<in> hypnatrel --> (x,z) \<in> hypnatrel"
-apply (unfold hypnatrel_def, auto, ultra)
-done
+by (auto simp add: hypnatrel_def, ultra)
 
 lemma equiv_hypnatrel:
      "equiv UNIV hypnatrel"
 apply (simp add: equiv_def refl_def sym_def trans_def hypnatrel_refl)
 apply (blast intro: hypnatrel_sym hypnatrel_trans)

 (* (hypnatrel `` {x} = hypnatrel `` {y}) = ((x,y) \<in> hypnatrel) *)
 lemmas equiv_hypnatrel_iff =
     eq_equiv_class_iff [OF equiv_hypnatrel UNIV_I UNIV_I, simp]
 
 lemma hypnatrel_in_hypnat [simp]: "hypnatrel``{x}:hypnat"
-by (unfold hypnat_def hypnatrel_def quotient_def, blast)
+by (simp add: hypnat_def hypnatrel_def quotient_def, blast)
 
 lemma inj_on_Abs_hypnat: "inj_on Abs_hypnat hypnat"
 apply (rule inj_on_inverseI)
 apply (erule Abs_hypnat_inverse)
 done

 by (simp add: hypnatrel_def)
 
 declare lemma_hypnatrel_refl [simp]
 
 lemma hypnat_empty_not_mem: "{} \<notin> hypnat"
-apply (unfold hypnat_def)
+apply (simp add: hypnat_def)
 apply (auto elim!: quotientE equalityCE)
 done
 
 declare hypnat_empty_not_mem [simp]
 

 apply (rule_tac x1=z in Rep_hypnat [unfolded hypnat_def, THEN quotientE])
 apply (drule_tac f = Abs_hypnat in arg_cong)
 apply (force simp add: Rep_hypnat_inverse)
 done
 
+theorem hypnat_cases [case_names Abs_hypnat, cases type: hypnat]:
+    "(!!x. z = Abs_hypnat(hypnatrel``{x}) ==> P) ==> P"
+by (rule eq_Abs_hypnat [of z], blast)
+
 subsection{*Hypernat Addition*}
 
 lemma hypnat_add_congruent2:
      "congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n + Y n})"
-apply (unfold congruent2_def, auto, ultra)
+apply (simp add: congruent2_def, auto, ultra)
 done
 
 lemma hypnat_add:
   "Abs_hypnat(hypnatrel``{%n. X n}) + Abs_hypnat(hypnatrel``{%n. Y n}) =
    Abs_hypnat(hypnatrel``{%n. X n + Y n})"
 by (simp add: hypnat_add_def UN_equiv_class2 [OF equiv_hypnatrel hypnat_add_congruent2])
 
 lemma hypnat_add_commute: "(z::hypnat) + w = w + z"
-apply (rule eq_Abs_hypnat [of z])
-apply (rule eq_Abs_hypnat [of w])
+apply (cases z, cases w)
 apply (simp add: add_ac hypnat_add)
 done
 
 lemma hypnat_add_assoc: "((z1::hypnat) + z2) + z3 = z1 + (z2 + z3)"
-apply (rule eq_Abs_hypnat [of z1])
-apply (rule eq_Abs_hypnat [of z2])
-apply (rule eq_Abs_hypnat [of z3])
+apply (cases z1, cases z2, cases z3)
 apply (simp add: hypnat_add nat_add_assoc)
 done
 
 lemma hypnat_add_zero_left: "(0::hypnat) + z = z"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
 apply (simp add: hypnat_zero_def hypnat_add)
 done
 
 instance hypnat :: plus_ac0
   by (intro_classes,

 subsection{*Subtraction inverse on @{typ hypreal}*}
 
 
 lemma hypnat_minus_congruent2:
     "congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n - Y n})"
-apply (unfold congruent2_def, auto, ultra)
+apply (simp add: congruent2_def, auto, ultra)
 done
 
 lemma hypnat_minus:
   "Abs_hypnat(hypnatrel``{%n. X n}) - Abs_hypnat(hypnatrel``{%n. Y n}) =
    Abs_hypnat(hypnatrel``{%n. X n - Y n})"
 by (simp add: hypnat_minus_def UN_equiv_class2 [OF equiv_hypnatrel hypnat_minus_congruent2])
 
 lemma hypnat_minus_zero: "z - z = (0::hypnat)"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
 apply (simp add: hypnat_zero_def hypnat_minus)
 done
 
 lemma hypnat_diff_0_eq_0: "(0::hypnat) - n = 0"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
 apply (simp add: hypnat_minus hypnat_zero_def)
 done
 
 declare hypnat_minus_zero [simp] hypnat_diff_0_eq_0 [simp]
 
 lemma hypnat_add_is_0: "(m+n = (0::hypnat)) = (m=0 & n=0)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
 apply (auto intro: FreeUltrafilterNat_subset dest: FreeUltrafilterNat_Int simp add: hypnat_zero_def hypnat_add)
 done
 
 declare hypnat_add_is_0 [iff]
 
 lemma hypnat_diff_diff_left: "(i::hypnat) - j - k = i - (j+k)"
-apply (rule eq_Abs_hypnat [of i])
-apply (rule eq_Abs_hypnat [of j])
-apply (rule eq_Abs_hypnat [of k])
+apply (cases i, cases j, cases k)
 apply (simp add: hypnat_minus hypnat_add diff_diff_left)
 done
 
 lemma hypnat_diff_commute: "(i::hypnat) - j - k = i-k-j"
 by (simp add: hypnat_diff_diff_left hypnat_add_commute)
 
 lemma hypnat_diff_add_inverse: "((n::hypnat) + m) - n = m"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
 apply (simp add: hypnat_minus hypnat_add)
 done
 declare hypnat_diff_add_inverse [simp]
 
 lemma hypnat_diff_add_inverse2:  "((m::hypnat) + n) - n = m"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
 apply (simp add: hypnat_minus hypnat_add)
 done
 declare hypnat_diff_add_inverse2 [simp]
 
 lemma hypnat_diff_cancel: "((k::hypnat) + m) - (k+n) = m - n"
-apply (rule eq_Abs_hypnat [of k])
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases k, cases m, cases n)
 apply (simp add: hypnat_minus hypnat_add)
 done
 declare hypnat_diff_cancel [simp]
 
 lemma hypnat_diff_cancel2: "((m::hypnat) + k) - (n+k) = m - n"
 by (simp add: hypnat_add_commute [of _ k])
 declare hypnat_diff_cancel2 [simp]
 
 lemma hypnat_diff_add_0: "(n::hypnat) - (n+m) = (0::hypnat)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
 apply (simp add: hypnat_zero_def hypnat_minus hypnat_add)
 done
 declare hypnat_diff_add_0 [simp]
 
 
 subsection{*Hyperreal Multiplication*}
 
 lemma hypnat_mult_congruent2:
     "congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n * Y n})"
-by (unfold congruent2_def, auto, ultra)
+by (simp add: congruent2_def, auto, ultra)
 
 lemma hypnat_mult:
   "Abs_hypnat(hypnatrel``{%n. X n}) * Abs_hypnat(hypnatrel``{%n. Y n}) =
    Abs_hypnat(hypnatrel``{%n. X n * Y n})"
 by (simp add: hypnat_mult_def UN_equiv_class2 [OF equiv_hypnatrel hypnat_mult_congruent2])
 
 lemma hypnat_mult_commute: "(z::hypnat) * w = w * z"
-apply (rule eq_Abs_hypnat [of z])
-apply (rule eq_Abs_hypnat [of w])
+apply (cases z, cases w)
 apply (simp add: hypnat_mult mult_ac)
 done
 
 lemma hypnat_mult_assoc: "((z1::hypnat) * z2) * z3 = z1 * (z2 * z3)"
-apply (rule eq_Abs_hypnat [of z1])
-apply (rule eq_Abs_hypnat [of z2])
-apply (rule eq_Abs_hypnat [of z3])
+apply (cases z1, cases z2, cases z3)
 apply (simp add: hypnat_mult mult_assoc)
 done
 
 lemma hypnat_mult_1: "(1::hypnat) * z = z"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
 apply (simp add: hypnat_mult hypnat_one_def)
 done
 
 lemma hypnat_diff_mult_distrib: "((m::hypnat) - n) * k = (m * k) - (n * k)"
-apply (rule eq_Abs_hypnat [of k])
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases k, cases m, cases n)
 apply (simp add: hypnat_mult hypnat_minus diff_mult_distrib)
 done
 
 lemma hypnat_diff_mult_distrib2: "(k::hypnat) * (m - n) = (k * m) - (k * n)"
 by (simp add: hypnat_diff_mult_distrib hypnat_mult_commute [of k])
 
 lemma hypnat_add_mult_distrib: "((z1::hypnat) + z2) * w = (z1 * w) + (z2 * w)"
-apply (rule eq_Abs_hypnat [of z1])
-apply (rule eq_Abs_hypnat [of z2])
-apply (rule eq_Abs_hypnat [of w])
+apply (cases z1, cases z2, cases w)
 apply (simp add: hypnat_mult hypnat_add add_mult_distrib)
 done
 
 lemma hypnat_add_mult_distrib2: "(w::hypnat) * (z1 + z2) = (w * z1) + (w * z2)"
 by (simp add: hypnat_mult_commute [of w] hypnat_add_mult_distrib)

 subsection{*Properties of The @{text "\<le>"} Relation*}
 
 lemma hypnat_le:
       "(Abs_hypnat(hypnatrel``{%n. X n}) \<le> Abs_hypnat(hypnatrel``{%n. Y n})) =
        ({n. X n \<le> Y n} \<in> FreeUltrafilterNat)"
-apply (unfold hypnat_le_def)
+apply (simp add: hypnat_le_def)
 apply (auto intro!: lemma_hypnatrel_refl, ultra)
 done
 
 lemma hypnat_le_refl: "w \<le> (w::hypnat)"
-apply (rule eq_Abs_hypnat [of w])
+apply (cases w)
 apply (simp add: hypnat_le)
 done
 
 lemma hypnat_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::hypnat)"
-apply (rule eq_Abs_hypnat [of i])
-apply (rule eq_Abs_hypnat [of j])
-apply (rule eq_Abs_hypnat [of k])
+apply (cases i, cases j, cases k)
 apply (simp add: hypnat_le, ultra)
 done
 
 lemma hypnat_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::hypnat)"
-apply (rule eq_Abs_hypnat [of z])
-apply (rule eq_Abs_hypnat [of w])
+apply (cases z, cases w)
 apply (simp add: hypnat_le, ultra)
 done
 
 (* Axiom 'order_less_le' of class 'order': *)
 lemma hypnat_less_le: "((w::hypnat) < z) = (w \<le> z & w \<noteq> z)"

  (assumption |
   rule hypnat_le_refl hypnat_le_trans hypnat_le_anti_sym hypnat_less_le)+
 
 (* Axiom 'linorder_linear' of class 'linorder': *)
 lemma hypnat_le_linear: "(z::hypnat) \<le> w | w \<le> z"
-apply (rule eq_Abs_hypnat [of z])
-apply (rule eq_Abs_hypnat [of w])
+apply (cases z, cases w)
 apply (auto simp add: hypnat_le, ultra)
 done
 
 instance hypnat :: linorder
   by (intro_classes, rule hypnat_le_linear)
 
 lemma hypnat_add_left_mono: "x \<le> y ==> z + x \<le> z + (y::hypnat)"
-apply (rule eq_Abs_hypnat [of x])
-apply (rule eq_Abs_hypnat [of y])
-apply (rule eq_Abs_hypnat [of z])
+apply (cases x, cases y, cases z)
 apply (auto simp add: hypnat_le hypnat_add)
 done
 
 lemma hypnat_mult_less_mono2: "[| (0::hypnat)<z; x<y |] ==> z*x<z*y"
-apply (rule eq_Abs_hypnat [of x])
-apply (rule eq_Abs_hypnat [of y])
-apply (rule eq_Abs_hypnat [of z])
+apply (cases x, cases y, cases z)
 apply (simp add: hypnat_zero_def  hypnat_mult linorder_not_le [symmetric])
 apply (auto simp add: hypnat_le, ultra)
 done
 
 

   show "x < y ==> 0 < z ==> z * x < z * y"
     by (simp add: hypnat_mult_less_mono2)
 qed
 
 lemma hypnat_le_zero_cancel [iff]: "(n \<le> (0::hypnat)) = (n = 0)"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
 apply (simp add: hypnat_zero_def hypnat_le)
 done
 
 lemma hypnat_mult_is_0 [simp]: "(m*n = (0::hypnat)) = (m=0 | n=0)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
 apply (auto simp add: hypnat_zero_def hypnat_mult, ultra+)
 done
 
 lemma hypnat_diff_is_0_eq [simp]: "((m::hypnat) - n = 0) = (m \<le> n)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
 apply (simp add: hypnat_le hypnat_minus hypnat_zero_def)
 done
 
 
 

 apply (auto simp add: hypnat_le  linorder_not_le [symmetric])
 apply (ultra+)
 done
 
 lemma hypnat_not_less0 [iff]: "~ n < (0::hypnat)"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
 apply (auto simp add: hypnat_zero_def hypnat_less)
 done
 
 lemma hypnat_less_one [iff]:
       "(n < (1::hypnat)) = (n=0)"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
 apply (auto simp add: hypnat_zero_def hypnat_one_def hypnat_less)
 done
 
 lemma hypnat_add_diff_inverse: "~ m<n ==> n+(m-n) = (m::hypnat)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
 apply (simp add: hypnat_minus hypnat_add hypnat_less split: nat_diff_split, ultra)
 done
 
 lemma hypnat_le_add_diff_inverse [simp]: "n \<le> m ==> n+(m-n) = (m::hypnat)"
 by (simp add: hypnat_add_diff_inverse linorder_not_less [symmetric])

       by (auto simp add: hypnat_add_self_not_less order_less_imp_le 
                          hypnat_diff_is_0_eq [THEN iffD2])
 next
   case False
     thus ?thesis
-      by (auto simp add: linorder_not_less dest: order_le_less_trans); 
+      by (auto simp add: linorder_not_less dest: order_le_less_trans) 
 qed
 
 
 subsection{*The Embedding @{term hypnat_of_nat} Preserves Ring and 
       Order Properties*}

 apply (case_tac x) 
 apply (auto simp add: add_commute [of 1]) 
 done
 
 lemma Nats_diff [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> (a-b :: hypnat) \<in> Nats"
-apply (auto simp add: of_nat_eq_add Nats_def split: hypnat_diff_split)
-done
+by (auto simp add: of_nat_eq_add Nats_def split: hypnat_diff_split)
 
 lemma lemma_unbounded_set [simp]: "{n::nat. m < n} \<in> FreeUltrafilterNat"
 apply (insert finite_atMost [of m]) 
 apply (simp add: atMost_def) 
 apply (drule FreeUltrafilterNat_finite) 
-apply (drule FreeUltrafilterNat_Compl_mem) 
-apply ultra
+apply (drule FreeUltrafilterNat_Compl_mem, ultra)
 done
 
 lemma Compl_Collect_le: "- {n::nat. N \<le> n} = {n. n < N}"
 by (simp add: Collect_neg_eq [symmetric] linorder_not_le) 
 
 
 lemma hypnat_of_nat_eq:
      "hypnat_of_nat m  = Abs_hypnat(hypnatrel``{%n::nat. m})"
 apply (induct m) 
-apply (simp_all add: hypnat_zero_def hypnat_one_def hypnat_add); 
+apply (simp_all add: hypnat_zero_def hypnat_one_def hypnat_add) 
 done
 
 lemma SHNat_eq: "Nats = {n. \<exists>N. n = hypnat_of_nat N}"
 by (force simp add: hypnat_of_nat_def Nats_def) 
 

 apply (simp add: Compl_Collect_le finite_nat_segment) 
 done
 
 (* Infinite hypernatural not in embedded Nats *)
 lemma SHNAT_omega_not_mem [simp]: "whn \<notin> Nats"
-apply (blast dest: hypnat_omega_gt_SHNat) 
-done
+by (blast dest: hypnat_omega_gt_SHNat)
 
 lemma hypnat_of_nat_less_whn [simp]: "hypnat_of_nat n < whn"
 apply (insert hypnat_omega_gt_SHNat [of "hypnat_of_nat n"])
 apply (simp add: hypnat_of_nat_def) 
 done

 Free Ultrafilter*}
 
 lemma HNatInfinite_FreeUltrafilterNat:
      "x \<in> HNatInfinite 
       ==> \<exists>X \<in> Rep_hypnat x. \<forall>u. {n. u < X n}:  FreeUltrafilterNat"
-apply (rule eq_Abs_hypnat [of x])
+apply (cases x)
 apply (auto simp add: HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
 apply (rule bexI [OF _ lemma_hypnatrel_refl], clarify) 
 apply (auto simp add: hypnat_of_nat_def hypnat_less)
 done
 
 lemma FreeUltrafilterNat_HNatInfinite:
      "\<exists>X \<in> Rep_hypnat x. \<forall>u. {n. u < X n}:  FreeUltrafilterNat
       ==> x \<in> HNatInfinite"
-apply (rule eq_Abs_hypnat [of x])
+apply (cases x)
 apply (auto simp add: hypnat_less HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
 apply (drule spec, ultra, auto) 
 done
 
 lemma HNatInfinite_FreeUltrafilterNat_iff:

 done
 
 lemma HNatInfinite_SHNat_add:
      "[| x \<in> HNatInfinite; y \<in> Nats |] ==> x + y \<in> HNatInfinite"
 apply (auto simp add: HNatInfinite_not_Nats_iff) 
-apply (drule_tac a = "x + y" in Nats_diff)
-apply (auto ); 
+apply (drule_tac a = "x + y" in Nats_diff, auto) 
 done
 
 lemma HNatInfinite_Nats_imp_less: "[| x \<in> HNatInfinite; y \<in> Nats |] ==> y < x"
 by (simp add: HNatInfinite_iff) 
 

        simp add: lemma_hyprel_FUFN)
 done
 
 lemma hypreal_of_hypnat_inject [simp]:
      "(hypreal_of_hypnat m = hypreal_of_hypnat n) = (m=n)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
 apply (auto simp add: hypreal_of_hypnat)
 done
 
 lemma hypreal_of_hypnat_zero: "hypreal_of_hypnat 0 = 0"
 by (simp add: hypnat_zero_def hypreal_zero_def hypreal_of_hypnat)

 lemma hypreal_of_hypnat_one: "hypreal_of_hypnat (1::hypnat) = 1"
 by (simp add: hypnat_one_def hypreal_one_def hypreal_of_hypnat)
 
 lemma hypreal_of_hypnat_add [simp]:
      "hypreal_of_hypnat (m + n) = hypreal_of_hypnat m + hypreal_of_hypnat n"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
 apply (simp add: hypreal_of_hypnat hypreal_add hypnat_add real_of_nat_add)
 done
 
 lemma hypreal_of_hypnat_mult [simp]:
      "hypreal_of_hypnat (m * n) = hypreal_of_hypnat m * hypreal_of_hypnat n"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
 apply (simp add: hypreal_of_hypnat hypreal_mult hypnat_mult real_of_nat_mult)
 done
 
 lemma hypreal_of_hypnat_less_iff [simp]:
      "(hypreal_of_hypnat n < hypreal_of_hypnat m) = (n < m)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
 apply (simp add: hypreal_of_hypnat hypreal_less hypnat_less)
 done
 
 lemma hypreal_of_hypnat_eq_zero_iff: "(hypreal_of_hypnat N = 0) = (N = 0)"
 by (simp add: hypreal_of_hypnat_zero [symmetric])
 declare hypreal_of_hypnat_eq_zero_iff [simp]
 
 lemma hypreal_of_hypnat_ge_zero [simp]: "0 \<le> hypreal_of_hypnat n"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
 apply (simp add: hypreal_of_hypnat hypreal_zero_num hypreal_le)
 done
 
 lemma HNatInfinite_inverse_Infinitesimal [simp]:
      "n \<in> HNatInfinite ==> inverse (hypreal_of_hypnat n) \<in> Infinitesimal"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
 apply (auto simp add: hypreal_of_hypnat hypreal_inverse 
       HNatInfinite_FreeUltrafilterNat_iff Infinitesimal_FreeUltrafilterNat_iff2)
 apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
 apply (drule_tac x = "m + 1" in spec, ultra)
 done