added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
--- a/src/HOL/Complex/NSComplex.thy Mon Sep 12 23:13:46 2005 +0200
+++ b/src/HOL/Complex/NSComplex.thy Mon Sep 12 23:14:41 2005 +0200
@@ -68,21 +68,15 @@
hexpi :: "hcomplex => hcomplex"
"hexpi z == hcomplex_of_hypreal(( *f* exp) (hRe z)) * hcis (hIm z)"
-
-constdefs
HComplex :: "[hypreal,hypreal] => hcomplex"
-(* "HComplex x y == hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y"*)
- "HComplex == Ifun2_of Complex"
-
+ "HComplex == Ifun2_of Complex"
-consts
- "hcpow" :: "[hcomplex,hypnat] => hcomplex" (infixr "hcpow" 80)
+ hcpow :: "[hcomplex,hypnat] => hcomplex" (infixr "hcpow" 80)
+ "(z::hcomplex) hcpow (n::hypnat) == Ifun2_of (op ^) z n"
-defs
- (* hypernatural powers of nonstandard complex numbers *)
- hcpow_def:
- "(z::hcomplex) hcpow (n::hypnat)
- == Ifun2_of (op ^) z n"
+lemmas hcomplex_defs [transfer_unfold] =
+ hRe_def hIm_def hcmod_def iii_def hcnj_def hsgn_def harg_def hcis_def
+ hcomplex_of_hypreal_def hrcis_def hexpi_def HComplex_def hcpow_def
subsection{*Properties of Nonstandard Real and Imaginary Parts*}
@@ -95,7 +89,7 @@
lemma hcomplex_hRe_hIm_cancel_iff:
"!!w z. (w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))"
-by (unfold hRe_def hIm_def, transfer, rule complex_Re_Im_cancel_iff)
+by (transfer, rule complex_Re_Im_cancel_iff)
lemma hcomplex_equality [intro?]: "hRe z = hRe w ==> hIm z = hIm w ==> z = w"
by (simp add: hcomplex_hRe_hIm_cancel_iff)
@@ -116,18 +110,18 @@
subsection{*Addition for Nonstandard Complex Numbers*}
lemma hRe_add: "!!x y. hRe(x + y) = hRe(x) + hRe(y)"
-by (unfold hRe_def, transfer, rule complex_Re_add)
+by (transfer, rule complex_Re_add)
lemma hIm_add: "!!x y. hIm(x + y) = hIm(x) + hIm(y)"
-by (unfold hIm_def, transfer, rule complex_Im_add)
+by (transfer, rule complex_Im_add)
subsection{*More Minus Laws*}
lemma hRe_minus: "!!z. hRe(-z) = - hRe(z)"
-by (unfold hRe_def, transfer, rule complex_Re_minus)
+by (transfer, rule complex_Re_minus)
lemma hIm_minus: "!!z. hIm(-z) = - hIm(z)"
-by (unfold hIm_def, transfer, rule complex_Im_minus)
+by (transfer, rule complex_Im_minus)
lemma hcomplex_add_minus_eq_minus:
"x + y = (0::hcomplex) ==> x = -y"
@@ -179,7 +173,7 @@
lemma hcomplex_of_hypreal_cancel_iff [iff]:
"!!x y. (hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)"
-by (unfold hcomplex_of_hypreal_def, transfer, simp)
+by (transfer, simp)
lemma hcomplex_of_hypreal_one [simp]: "hcomplex_of_hypreal 1 = 1"
by (simp add: hcomplex_of_hypreal star_n_one_num)
@@ -189,31 +183,31 @@
lemma hcomplex_of_hypreal_minus [simp]:
"!!x. hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x"
-by (unfold hcomplex_of_hypreal_def, transfer, simp)
+by (transfer, simp)
lemma hcomplex_of_hypreal_inverse [simp]:
"!!x. hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)"
-by (unfold hcomplex_of_hypreal_def, transfer, simp)
+by (transfer, simp)
lemma hcomplex_of_hypreal_add [simp]:
"!!x y. hcomplex_of_hypreal (x + y) =
hcomplex_of_hypreal x + hcomplex_of_hypreal y"
-by (unfold hcomplex_of_hypreal_def, transfer, simp)
+by (transfer, simp)
lemma hcomplex_of_hypreal_diff [simp]:
"!!x y. hcomplex_of_hypreal (x - y) =
hcomplex_of_hypreal x - hcomplex_of_hypreal y "
-by (unfold hcomplex_of_hypreal_def, transfer, simp)
+by (transfer, simp)
lemma hcomplex_of_hypreal_mult [simp]:
"!!x y. hcomplex_of_hypreal (x * y) =
hcomplex_of_hypreal x * hcomplex_of_hypreal y"
-by (unfold hcomplex_of_hypreal_def, transfer, simp)
+by (transfer, simp)
lemma hcomplex_of_hypreal_divide [simp]:
"!!x y. hcomplex_of_hypreal(x/y) =
hcomplex_of_hypreal x / hcomplex_of_hypreal y"
-by (unfold hcomplex_of_hypreal_def, transfer, simp)
+by (transfer, simp)
lemma hRe_hcomplex_of_hypreal [simp]: "hRe(hcomplex_of_hypreal z) = z"
apply (cases z)
@@ -233,10 +227,10 @@
subsection{*HComplex theorems*}
lemma hRe_HComplex [simp]: "!!x y. hRe (HComplex x y) = x"
-by (unfold hRe_def HComplex_def, transfer, simp)
+by (transfer, simp)
lemma hIm_HComplex [simp]: "!!x y. hIm (HComplex x y) = y"
-by (unfold hIm_def HComplex_def, transfer, simp)
+by (transfer, simp)
text{*Relates the two nonstandard constructions*}
lemma HComplex_eq_Abs_star_Complex:
@@ -275,28 +269,28 @@
lemma HComplex_inject [simp]:
"!!x y x' y'. HComplex x y = HComplex x' y' = (x=x' & y=y')"
-by (unfold HComplex_def, transfer, simp)
+by (transfer, simp)
lemma HComplex_add [simp]:
"!!x1 y1 x2 y2. HComplex x1 y1 + HComplex x2 y2 = HComplex (x1+x2) (y1+y2)"
-by (unfold HComplex_def, transfer, simp)
+by (transfer, simp)
lemma HComplex_minus [simp]: "!!x y. - HComplex x y = HComplex (-x) (-y)"
-by (unfold HComplex_def, transfer, simp)
+by (transfer, simp)
lemma HComplex_diff [simp]:
"!!x1 y1 x2 y2. HComplex x1 y1 - HComplex x2 y2 = HComplex (x1-x2) (y1-y2)"
-by (unfold HComplex_def, transfer, rule complex_diff)
+by (transfer, rule complex_diff)
lemma HComplex_mult [simp]:
"!!x1 y1 x2 y2. HComplex x1 y1 * HComplex x2 y2 =
HComplex (x1*x2 - y1*y2) (x1*y2 + y1*x2)"
-by (unfold HComplex_def, transfer, rule complex_mult)
+by (transfer, rule complex_mult)
(*HComplex_inverse is proved below*)
lemma hcomplex_of_hypreal_eq: "!!r. hcomplex_of_hypreal r = HComplex r 0"
-apply (unfold hcomplex_of_hypreal_def HComplex_def, transfer)
+apply (transfer)
apply (simp add: complex_of_real_def)
done
@@ -318,11 +312,11 @@
lemma i_hcomplex_of_hypreal [simp]:
"!!r. iii * hcomplex_of_hypreal r = HComplex 0 r"
-by (unfold iii_def hcomplex_of_hypreal_def HComplex_def, transfer, rule i_complex_of_real)
+by (transfer, rule i_complex_of_real)
lemma hcomplex_of_hypreal_i [simp]:
"!!r. hcomplex_of_hypreal r * iii = HComplex 0 r"
-by (unfold iii_def hcomplex_of_hypreal_def HComplex_def, transfer, rule complex_of_real_i)
+by (transfer, rule complex_of_real_i)
subsection{*Conjugation*}
@@ -331,56 +325,54 @@
by (simp add: hcnj_def starfun)
lemma hcomplex_hcnj_cancel_iff [iff]: "!!x y. (hcnj x = hcnj y) = (x = y)"
-by (unfold hcnj_def, transfer, rule complex_cnj_cancel_iff)
+by (transfer, rule complex_cnj_cancel_iff)
lemma hcomplex_hcnj_hcnj [simp]: "!!z. hcnj (hcnj z) = z"
-by (unfold hcnj_def, transfer, rule complex_cnj_cnj)
+by (transfer, rule complex_cnj_cnj)
lemma hcomplex_hcnj_hcomplex_of_hypreal [simp]:
"!!x. hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x"
-by (unfold hcnj_def hcomplex_of_hypreal_def, transfer, rule complex_cnj_complex_of_real)
+by (transfer, rule complex_cnj_complex_of_real)
lemma hcomplex_hmod_hcnj [simp]: "!!z. hcmod (hcnj z) = hcmod z"
-by (unfold hcmod_def hcnj_def, transfer, rule complex_mod_cnj)
+by (transfer, rule complex_mod_cnj)
lemma hcomplex_hcnj_minus: "!!z. hcnj (-z) = - hcnj z"
-by (unfold hcnj_def, transfer, rule complex_cnj_minus)
+by (transfer, rule complex_cnj_minus)
lemma hcomplex_hcnj_inverse: "!!z. hcnj(inverse z) = inverse(hcnj z)"
-by (unfold hcnj_def, transfer, rule complex_cnj_inverse)
+by (transfer, rule complex_cnj_inverse)
lemma hcomplex_hcnj_add: "!!w z. hcnj(w + z) = hcnj(w) + hcnj(z)"
-by (unfold hcnj_def, transfer, rule complex_cnj_add)
+by (transfer, rule complex_cnj_add)
lemma hcomplex_hcnj_diff: "!!w z. hcnj(w - z) = hcnj(w) - hcnj(z)"
-by (unfold hcnj_def, transfer, rule complex_cnj_diff)
+by (transfer, rule complex_cnj_diff)
lemma hcomplex_hcnj_mult: "!!w z. hcnj(w * z) = hcnj(w) * hcnj(z)"
-by (unfold hcnj_def, transfer, rule complex_cnj_mult)
+by (transfer, rule complex_cnj_mult)
lemma hcomplex_hcnj_divide: "!!w z. hcnj(w / z) = (hcnj w)/(hcnj z)"
-by (unfold hcnj_def, transfer, rule complex_cnj_divide)
+by (transfer, rule complex_cnj_divide)
lemma hcnj_one [simp]: "hcnj 1 = 1"
-by (unfold hcnj_def, transfer, rule complex_cnj_one)
+by (transfer, rule complex_cnj_one)
lemma hcomplex_hcnj_zero [simp]: "hcnj 0 = 0"
-by (unfold hcnj_def, transfer, rule complex_cnj_zero)
+by (transfer, rule complex_cnj_zero)
lemma hcomplex_hcnj_zero_iff [iff]: "!!z. (hcnj z = 0) = (z = 0)"
-by (unfold hcnj_def, transfer, rule complex_cnj_zero_iff)
+by (transfer, rule complex_cnj_zero_iff)
lemma hcomplex_mult_hcnj:
"!!z. z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)"
-apply (unfold hcnj_def hcomplex_of_hypreal_def hRe_def hIm_def)
-apply (transfer, rule complex_mult_cnj)
-done
+by (transfer, rule complex_mult_cnj)
subsection{*More Theorems about the Function @{term hcmod}*}
lemma hcomplex_hcmod_eq_zero_cancel [simp]: "!!x. (hcmod x = 0) = (x = 0)"
-by (unfold hcmod_def, transfer, rule complex_mod_eq_zero_cancel)
+by (transfer, rule complex_mod_eq_zero_cancel)
lemma hcmod_hcomplex_of_hypreal_of_nat [simp]:
"hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n"
@@ -391,57 +383,57 @@
by (simp add: abs_if linorder_not_less)
lemma hcmod_minus [simp]: "!!x. hcmod (-x) = hcmod(x)"
-by (unfold hcmod_def, transfer, rule complex_mod_minus)
+by (transfer, rule complex_mod_minus)
lemma hcmod_mult_hcnj: "!!z. hcmod(z * hcnj(z)) = hcmod(z) ^ 2"
-by (unfold hcmod_def hcnj_def, transfer, rule complex_mod_mult_cnj)
+by (transfer, rule complex_mod_mult_cnj)
lemma hcmod_ge_zero [simp]: "!!x. (0::hypreal) \<le> hcmod x"
-by (unfold hcmod_def, transfer, rule complex_mod_ge_zero)
+by (transfer, rule complex_mod_ge_zero)
lemma hrabs_hcmod_cancel [simp]: "abs(hcmod x) = hcmod x"
by (simp add: abs_if linorder_not_less)
lemma hcmod_mult: "!!x y. hcmod(x*y) = hcmod(x) * hcmod(y)"
-by (unfold hcmod_def, transfer, rule complex_mod_mult)
+by (transfer, rule complex_mod_mult)
lemma hcmod_add_squared_eq:
"!!x y. hcmod(x + y) ^ 2 = hcmod(x) ^ 2 + hcmod(y) ^ 2 + 2 * hRe(x * hcnj y)"
-by (unfold hcmod_def hcnj_def hRe_def, transfer, rule complex_mod_add_squared_eq)
+by (transfer, rule complex_mod_add_squared_eq)
lemma hcomplex_hRe_mult_hcnj_le_hcmod [simp]:
"!!x y. hRe(x * hcnj y) \<le> hcmod(x * hcnj y)"
-by (unfold hcmod_def hcnj_def hRe_def, transfer, simp)
+by (transfer, simp)
lemma hcomplex_hRe_mult_hcnj_le_hcmod2 [simp]:
"!!x y. hRe(x * hcnj y) \<le> hcmod(x * y)"
-by (unfold hcmod_def hcnj_def hRe_def, transfer, simp)
+by (transfer, simp)
lemma hcmod_triangle_squared [simp]:
"!!x y. hcmod (x + y) ^ 2 \<le> (hcmod(x) + hcmod(y)) ^ 2"
-by (unfold hcmod_def, transfer, simp)
+by (transfer, simp)
lemma hcmod_triangle_ineq [simp]:
"!!x y. hcmod (x + y) \<le> hcmod(x) + hcmod(y)"
-by (unfold hcmod_def, transfer, simp)
+by (transfer, simp)
lemma hcmod_triangle_ineq2 [simp]:
"!!a b. hcmod(b + a) - hcmod b \<le> hcmod a"
-by (unfold hcmod_def, transfer, simp)
+by (transfer, simp)
lemma hcmod_diff_commute: "!!x y. hcmod (x - y) = hcmod (y - x)"
-by (unfold hcmod_def, transfer, rule complex_mod_diff_commute)
+by (transfer, rule complex_mod_diff_commute)
lemma hcmod_add_less:
"!!x y r s. [| hcmod x < r; hcmod y < s |] ==> hcmod (x + y) < r + s"
-by (unfold hcmod_def, transfer, rule complex_mod_add_less)
+by (transfer, rule complex_mod_add_less)
lemma hcmod_mult_less:
"!!x y r s. [| hcmod x < r; hcmod y < s |] ==> hcmod (x * y) < r * s"
-by (unfold hcmod_def, transfer, rule complex_mod_mult_less)
+by (transfer, rule complex_mod_mult_less)
lemma hcmod_diff_ineq [simp]: "!!a b. hcmod(a) - hcmod(b) \<le> hcmod(a + b)"
-by (unfold hcmod_def, transfer, simp)
+by (transfer, simp)
subsection{*A Few Nonlinear Theorems*}
@@ -451,15 +443,13 @@
lemma hcomplex_of_hypreal_hyperpow:
"!!x n. hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n"
-apply (unfold hcomplex_of_hypreal_def hyperpow_def hcpow_def)
-apply (transfer, rule complex_of_real_pow)
-done
+by (transfer, rule complex_of_real_pow)
lemma hcmod_hcpow: "!!x n. hcmod(x hcpow n) = hcmod(x) pow n"
-by (unfold hcmod_def hcpow_def hyperpow_def, transfer, rule complex_mod_complexpow)
+by (transfer, rule complex_mod_complexpow)
lemma hcmod_hcomplex_inverse: "!!x. hcmod(inverse x) = inverse(hcmod x)"
-by (unfold hcmod_def, transfer, rule complex_mod_inverse)
+by (transfer, rule complex_mod_inverse)
lemma hcmod_divide: "hcmod(x/y) = hcmod(x)/(hcmod y)"
by (simp add: divide_inverse hcmod_mult hcmod_hcomplex_inverse)
@@ -496,11 +486,11 @@
lemma hcpow_minus:
"!!x n. (-x::hcomplex) hcpow n =
(if ( *p* even) n then (x hcpow n) else -(x hcpow n))"
-by (unfold hcpow_def, transfer, rule neg_power_if)
+by (transfer, rule neg_power_if)
lemma hcpow_mult:
"!!r s n. ((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)"
-by (unfold hcpow_def, transfer, rule power_mult_distrib)
+by (transfer, rule power_mult_distrib)
lemma hcpow_zero [simp]: "0 hcpow (n + 1) = 0"
apply (simp add: star_n_zero_num star_n_one_num, cases n)
@@ -587,25 +577,23 @@
"!!x y. inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) =
hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) -
iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))"
-apply (unfold hcomplex_of_hypreal_def iii_def)
-apply (transfer, rule complex_inverse_complex_split)
-done
+by (transfer, rule complex_inverse_complex_split)
lemma HComplex_inverse:
"!!x y. inverse (HComplex x y) =
HComplex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))"
-by (unfold HComplex_def, transfer, rule complex_inverse)
+by (transfer, rule complex_inverse)
lemma hRe_mult_i_eq[simp]:
"!!y. hRe (iii * hcomplex_of_hypreal y) = 0"
-by (unfold hRe_def iii_def hcomplex_of_hypreal_def, transfer, simp)
+by (transfer, simp)
lemma hIm_mult_i_eq [simp]:
"!!y. hIm (iii * hcomplex_of_hypreal y) = y"
-by (unfold hIm_def iii_def hcomplex_of_hypreal_def, transfer, simp)
+by (transfer, simp)
lemma hcmod_mult_i [simp]: "!!y. hcmod (iii * hcomplex_of_hypreal y) = abs y"
-by (unfold hcmod_def iii_def hcomplex_of_hypreal_def, transfer, simp)
+by (transfer, simp)
lemma hcmod_mult_i2 [simp]: "hcmod (hcomplex_of_hypreal y * iii) = abs y"
by (simp only: hcmod_mult_i mult_commute)
@@ -619,11 +607,11 @@
lemma cos_harg_i_mult_zero_pos:
"!!y. 0 < y ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
-by (unfold harg_def HComplex_def, transfer, rule cos_arg_i_mult_zero_pos)
+by (transfer, rule cos_arg_i_mult_zero_pos)
lemma cos_harg_i_mult_zero_neg:
"!!y. y < 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
-by (unfold harg_def HComplex_def, transfer, rule cos_arg_i_mult_zero_neg)
+by (transfer, rule cos_arg_i_mult_zero_neg)
lemma cos_harg_i_mult_zero [simp]:
"y \<noteq> 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
@@ -632,7 +620,7 @@
lemma hcomplex_of_hypreal_zero_iff [simp]:
"!!y. (hcomplex_of_hypreal y = 0) = (y = 0)"
-by (unfold hcomplex_of_hypreal_def, transfer, simp)
+by (transfer, simp)
subsection{*Polar Form for Nonstandard Complex Numbers*}
@@ -651,7 +639,7 @@
lemma hcomplex_split_polar:
"!!z. \<exists>r a. z = hcomplex_of_hypreal r * (HComplex(( *f* cos) a)(( *f* sin) a))"
-by (unfold hcomplex_of_hypreal_def HComplex_def, transfer, rule complex_split_polar)
+by (transfer, rule complex_split_polar)
lemma hcis: "hcis (star_n X) = star_n (%n. cis (X n))"
by (simp add: hcis_def starfun)
@@ -691,7 +679,7 @@
lemma hcmod_unit_one [simp]:
"!!a. hcmod (HComplex (( *f* cos) a) (( *f* sin) a)) = 1"
-by (unfold hcmod_def HComplex_def, transfer, simp)
+by (transfer, simp)
lemma hcmod_complex_polar [simp]:
"hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
@@ -873,11 +861,7 @@
subsection{*Numerals and Arithmetic*}
lemma hcomplex_number_of_def: "(number_of w :: hcomplex) == of_int (Rep_Bin w)"
-apply (rule eq_reflection)
-apply (unfold star_number_def star_of_int_def)
-apply (rule star_of_inject [THEN iffD2])
-apply (rule number_of_eq)
-done
+by (transfer, rule number_of_eq [THEN eq_reflection])
lemma hcomplex_of_complex_of_nat:
"hcomplex_of_complex (of_nat n) = of_nat n"
--- a/src/HOL/Hyperreal/Filter.thy Mon Sep 12 23:13:46 2005 +0200
+++ b/src/HOL/Hyperreal/Filter.thy Mon Sep 12 23:14:41 2005 +0200
@@ -60,7 +60,7 @@
apply (auto elim: subset)
done
-subsubsection {* Free ultrafilters *}
+subsubsection {* Free Ultrafilters *}
locale freeultrafilter = ultrafilter +
assumes infinite: "A \<in> F \<Longrightarrow> infinite A"
@@ -73,7 +73,40 @@
lemma (in freeultrafilter) ultrafilter: "ultrafilter F"
by (rule ultrafilter.intro)
-subsection {* Maximal filter = ultrafilter *}
+subsection {* Collect properties *}
+
+lemma (in filter) Collect_ex:
+ "({n. \<exists>x. P n x} \<in> F) = (\<exists>X. {n. P n (X n)} \<in> F)"
+proof
+ assume "{n. \<exists>x. P n x} \<in> F"
+ hence "{n. P n (SOME x. P n x)} \<in> F"
+ by (auto elim: someI subset)
+ thus "\<exists>X. {n. P n (X n)} \<in> F" by fast
+next
+ show "\<exists>X. {n. P n (X n)} \<in> F \<Longrightarrow> {n. \<exists>x. P n x} \<in> F"
+ by (auto elim: subset)
+qed
+
+lemma (in filter) Collect_conj:
+ "({n. P n \<and> Q n} \<in> F) = ({n. P n} \<in> F \<and> {n. Q n} \<in> F)"
+by (subst Collect_conj_eq, rule Int_iff)
+
+lemma (in ultrafilter) Collect_not:
+ "({n. \<not> P n} \<in> F) = ({n. P n} \<notin> F)"
+by (subst Collect_neg_eq, rule Compl_iff)
+
+lemma (in ultrafilter) Collect_disj:
+ "({n. P n \<or> Q n} \<in> F) = ({n. P n} \<in> F \<or> {n. Q n} \<in> F)"
+by (subst Collect_disj_eq, rule Un_iff)
+
+lemma (in ultrafilter) Collect_all:
+ "({n. \<forall>x. P n x} \<in> F) = (\<forall>X. {n. P n (X n)} \<in> F)"
+apply (rule Not_eq_iff [THEN iffD1])
+apply (simp add: Collect_not [symmetric])
+apply (rule Collect_ex)
+done
+
+subsection {* Maximal filter = Ultrafilter *}
text {*
A filter F is an ultrafilter iff it is a maximal filter,
@@ -150,7 +183,7 @@
qed
qed
-subsection {* ultrafilter Theorem *}
+subsection {* Ultrafilter Theorem *}
text "A locale makes proof of ultrafilter Theorem more modular"
locale (open) UFT =
--- a/src/HOL/Hyperreal/HLog.thy Mon Sep 12 23:13:46 2005 +0200
+++ b/src/HOL/Hyperreal/HLog.thy Mon Sep 12 23:14:41 2005 +0200
@@ -26,47 +26,49 @@
hlog :: "[hypreal,hypreal] => hypreal"
"hlog a x == Ifun2_of log a x"
+declare powhr_def [transfer_unfold]
+declare hlog_def [transfer_unfold]
lemma powhr: "(star_n X) powhr (star_n Y) = star_n (%n. (X n) powr (Y n))"
by (simp add: powhr_def Ifun2_of_def star_of_def Ifun_star_n)
lemma powhr_one_eq_one [simp]: "!!a. 1 powhr a = 1"
-by (unfold powhr_def, transfer, simp)
+by (transfer, simp)
lemma powhr_mult:
"!!a x y. [| 0 < x; 0 < y |] ==> (x * y) powhr a = (x powhr a) * (y powhr a)"
-by (unfold powhr_def, transfer, rule powr_mult)
+by (transfer, rule powr_mult)
lemma powhr_gt_zero [simp]: "!!a x. 0 < x powhr a"
-by (unfold powhr_def, transfer, simp)
+by (transfer, simp)
lemma powhr_not_zero [simp]: "x powhr a \<noteq> 0"
by (rule powhr_gt_zero [THEN hypreal_not_refl2, THEN not_sym])
lemma powhr_divide:
"!!a x y. [| 0 < x; 0 < y |] ==> (x / y) powhr a = (x powhr a)/(y powhr a)"
-by (unfold powhr_def, transfer, rule powr_divide)
+by (transfer, rule powr_divide)
lemma powhr_add: "!!a b x. x powhr (a + b) = (x powhr a) * (x powhr b)"
-by (unfold powhr_def, transfer, rule powr_add)
+by (transfer, rule powr_add)
lemma powhr_powhr: "!!a b x. (x powhr a) powhr b = x powhr (a * b)"
-by (unfold powhr_def, transfer, rule powr_powr)
+by (transfer, rule powr_powr)
lemma powhr_powhr_swap: "!!a b x. (x powhr a) powhr b = (x powhr b) powhr a"
-by (unfold powhr_def, transfer, rule powr_powr_swap)
+by (transfer, rule powr_powr_swap)
lemma powhr_minus: "!!a x. x powhr (-a) = inverse (x powhr a)"
-by (unfold powhr_def, transfer, rule powr_minus)
+by (transfer, rule powr_minus)
lemma powhr_minus_divide: "x powhr (-a) = 1/(x powhr a)"
by (simp add: divide_inverse powhr_minus)
lemma powhr_less_mono: "!!a b x. [| a < b; 1 < x |] ==> x powhr a < x powhr b"
-by (unfold powhr_def, transfer, simp)
+by (transfer, simp)
lemma powhr_less_cancel: "!!a b x. [| x powhr a < x powhr b; 1 < x |] ==> a < b"
-by (unfold powhr_def, transfer, simp)
+by (transfer, simp)
lemma powhr_less_cancel_iff [simp]:
"1 < x ==> (x powhr a < x powhr b) = (a < b)"
@@ -82,32 +84,32 @@
by (simp add: hlog_def Ifun2_of_def star_of_def Ifun_star_n)
lemma hlog_starfun_ln: "!!x. ( *f* ln) x = hlog (( *f* exp) 1) x"
-by (unfold hlog_def, transfer, rule log_ln)
+by (transfer, rule log_ln)
lemma powhr_hlog_cancel [simp]:
"!!a x. [| 0 < a; a \<noteq> 1; 0 < x |] ==> a powhr (hlog a x) = x"
-by (unfold powhr_def hlog_def, transfer, simp)
+by (transfer, simp)
lemma hlog_powhr_cancel [simp]:
"!!a y. [| 0 < a; a \<noteq> 1 |] ==> hlog a (a powhr y) = y"
-by (unfold powhr_def hlog_def, transfer, simp)
+by (transfer, simp)
lemma hlog_mult:
"!!a x y. [| 0 < a; a \<noteq> 1; 0 < x; 0 < y |]
==> hlog a (x * y) = hlog a x + hlog a y"
-by (unfold powhr_def hlog_def, transfer, rule log_mult)
+by (transfer, rule log_mult)
lemma hlog_as_starfun:
"!!a x. [| 0 < a; a \<noteq> 1 |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a"
-by (unfold hlog_def, transfer, simp add: log_def)
+by (transfer, simp add: log_def)
lemma hlog_eq_div_starfun_ln_mult_hlog:
"!!a b x. [| 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x |]
==> hlog a x = (( *f* ln) b/( *f*ln) a) * hlog b x"
-by (unfold hlog_def, transfer, rule log_eq_div_ln_mult_log)
+by (transfer, rule log_eq_div_ln_mult_log)
lemma powhr_as_starfun: "!!a x. x powhr a = ( *f* exp) (a * ( *f* ln) x)"
-by (unfold powhr_def, transfer, simp add: powr_def)
+by (transfer, simp add: powr_def)
lemma HInfinite_powhr:
"[| x : HInfinite; 0 < x; a : HFinite - Infinitesimal;
@@ -131,10 +133,10 @@
by (rule hlog_as_starfun, auto)
lemma hlog_one [simp]: "!!a. hlog a 1 = 0"
-by (unfold hlog_def, transfer, simp)
+by (transfer, simp)
lemma hlog_eq_one [simp]: "!!a. [| 0 < a; a \<noteq> 1 |] ==> hlog a a = 1"
-by (unfold hlog_def, transfer, rule log_eq_one)
+by (transfer, rule log_eq_one)
lemma hlog_inverse:
"[| 0 < a; a \<noteq> 1; 0 < x |] ==> hlog a (inverse x) = - hlog a x"
@@ -148,7 +150,7 @@
lemma hlog_less_cancel_iff [simp]:
"!!a x y. [| 1 < a; 0 < x; 0 < y |] ==> (hlog a x < hlog a y) = (x < y)"
-by (unfold hlog_def, transfer, simp)
+by (transfer, simp)
lemma hlog_le_cancel_iff [simp]:
"[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x \<le> hlog a y) = (x \<le> y)"
--- a/src/HOL/Hyperreal/HTranscendental.thy Mon Sep 12 23:13:46 2005 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy Mon Sep 12 23:14:41 2005 +0200
@@ -131,7 +131,7 @@
lemma hypreal_sqrt_hyperpow_hrabs [simp]:
"!!x. ( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(x)"
-by (unfold hyperpow_def, transfer, simp)
+by (transfer, simp)
lemma star_sqrt_HFinite: "\<lbrakk>x \<in> HFinite; 0 \<le> x\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> HFinite"
apply (rule HFinite_square_iff [THEN iffD1])
--- a/src/HOL/Hyperreal/HyperNat.thy Mon Sep 12 23:13:46 2005 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy Mon Sep 12 23:14:41 2005 +0200
@@ -373,6 +373,7 @@
hypreal_of_hypnat :: "hypnat => hypreal"
"hypreal_of_hypnat == *f* real"
+declare hypreal_of_hypnat_def [transfer_unfold]
lemma HNat_hypreal_of_nat [simp]: "hypreal_of_nat N \<in> Nats"
by (simp add: hypreal_of_nat_def)
@@ -383,7 +384,7 @@
lemma hypreal_of_hypnat_inject [simp]:
"!!m n. (hypreal_of_hypnat m = hypreal_of_hypnat n) = (m=n)"
-by (unfold hypreal_of_hypnat_def, transfer, simp)
+by (transfer, simp)
lemma hypreal_of_hypnat_zero: "hypreal_of_hypnat 0 = 0"
by (simp add: star_n_zero_num hypreal_of_hypnat)
@@ -393,22 +394,22 @@
lemma hypreal_of_hypnat_add [simp]:
"!!m n. hypreal_of_hypnat (m + n) = hypreal_of_hypnat m + hypreal_of_hypnat n"
-by (unfold hypreal_of_hypnat_def, transfer, rule real_of_nat_add)
+by (transfer, rule real_of_nat_add)
lemma hypreal_of_hypnat_mult [simp]:
"!!m n. hypreal_of_hypnat (m * n) = hypreal_of_hypnat m * hypreal_of_hypnat n"
-by (unfold hypreal_of_hypnat_def, transfer, rule real_of_nat_mult)
+by (transfer, rule real_of_nat_mult)
lemma hypreal_of_hypnat_less_iff [simp]:
"!!m n. (hypreal_of_hypnat n < hypreal_of_hypnat m) = (n < m)"
-by (unfold hypreal_of_hypnat_def, transfer, simp)
+by (transfer, simp)
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]: "!!n. 0 \<le> hypreal_of_hypnat n"
-by (unfold hypreal_of_hypnat_def, transfer, simp)
+by (transfer, simp)
lemma HNatInfinite_inverse_Infinitesimal [simp]:
"n \<in> HNatInfinite ==> inverse (hypreal_of_hypnat n) \<in> Infinitesimal"
--- a/src/HOL/Hyperreal/HyperPow.thy Mon Sep 12 23:13:46 2005 +0200
+++ b/src/HOL/Hyperreal/HyperPow.thy Mon Sep 12 23:14:41 2005 +0200
@@ -24,7 +24,7 @@
defs
(* hypernatural powers of hyperreals *)
- hyperpow_def:
+ hyperpow_def [transfer_unfold]:
"(R::hypreal) pow (N::hypnat) == Ifun2_of (op ^) R N"
lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r"
@@ -104,46 +104,46 @@
by (simp add: hyperpow_def Ifun2_of_def star_of_def Ifun_star_n)
lemma hyperpow_zero [simp]: "!!n. (0::hypreal) pow (n + (1::hypnat)) = 0"
-by (unfold hyperpow_def, transfer, simp)
+by (transfer, simp)
lemma hyperpow_not_zero: "!!r n. r \<noteq> (0::hypreal) ==> r pow n \<noteq> 0"
-by (unfold hyperpow_def, transfer, simp)
+by (transfer, simp)
lemma hyperpow_inverse:
"!!r n. r \<noteq> (0::hypreal) ==> inverse(r pow n) = (inverse r) pow n"
-by (unfold hyperpow_def, transfer, rule power_inverse)
+by (transfer, rule power_inverse)
lemma hyperpow_hrabs: "!!r n. abs r pow n = abs (r pow n)"
-by (unfold hyperpow_def, transfer, rule power_abs [symmetric])
+by (transfer, rule power_abs [symmetric])
lemma hyperpow_add: "!!r n m. r pow (n + m) = (r pow n) * (r pow m)"
-by (unfold hyperpow_def, transfer, rule power_add)
+by (transfer, rule power_add)
lemma hyperpow_one [simp]: "!!r. r pow (1::hypnat) = r"
-by (unfold hyperpow_def, transfer, simp)
+by (transfer, simp)
lemma hyperpow_two:
"!!r. r pow ((1::hypnat) + (1::hypnat)) = r * r"
-by (unfold hyperpow_def, transfer, simp)
+by (transfer, simp)
lemma hyperpow_gt_zero: "!!r n. (0::hypreal) < r ==> 0 < r pow n"
-by (unfold hyperpow_def, transfer, rule zero_less_power)
+by (transfer, rule zero_less_power)
lemma hyperpow_ge_zero: "!!r n. (0::hypreal) \<le> r ==> 0 \<le> r pow n"
-by (unfold hyperpow_def, transfer, rule zero_le_power)
+by (transfer, rule zero_le_power)
lemma hyperpow_le:
"!!x y n. [|(0::hypreal) < x; x \<le> y|] ==> x pow n \<le> y pow n"
-by (unfold hyperpow_def, transfer, rule power_mono [OF _ order_less_imp_le])
+by (transfer, rule power_mono [OF _ order_less_imp_le])
lemma hyperpow_eq_one [simp]: "!!n. 1 pow n = (1::hypreal)"
-by (unfold hyperpow_def, transfer, simp)
+by (transfer, simp)
lemma hrabs_hyperpow_minus_one [simp]: "!!n. abs(-1 pow n) = (1::hypreal)"
-by (unfold hyperpow_def, transfer, simp)
+by (transfer, simp)
lemma hyperpow_mult: "!!r s n. (r * s) pow n = (r pow n) * (s pow n)"
-by (unfold hyperpow_def, transfer, rule power_mult_distrib)
+by (transfer, rule power_mult_distrib)
lemma hyperpow_two_le [simp]: "0 \<le> r pow (1 + 1)"
by (auto simp add: hyperpow_two zero_le_mult_iff)
@@ -176,11 +176,11 @@
lemma hyperpow_minus_one2 [simp]:
"!!n. -1 pow ((1 + 1)*n) = (1::hypreal)"
-by (unfold hyperpow_def, transfer, simp)
+by (transfer, simp)
lemma hyperpow_less_le:
"!!r n N. [|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
-by (unfold hyperpow_def, transfer, rule power_decreasing [OF order_less_imp_le])
+by (transfer, rule power_decreasing [OF order_less_imp_le])
lemma hyperpow_SHNat_le:
"[| 0 \<le> r; r \<le> (1::hypreal); N \<in> HNatInfinite |]
--- a/src/HOL/Hyperreal/NatStar.thy Mon Sep 12 23:13:46 2005 +0200
+++ b/src/HOL/Hyperreal/NatStar.thy Mon Sep 12 23:14:41 2005 +0200
@@ -13,7 +13,7 @@
lemma starset_n_Un: "*sn* (%n. (A n) Un (B n)) = *sn* A Un *sn* B"
apply (simp add: starset_n_def expand_set_eq all_star_eq)
-apply (simp add: Iset_star_n fuf_disj)
+apply (simp add: Iset_star_n ultrafilter.Collect_disj [OF ultrafilter_FUFNat])
done
lemma InternalSets_Un:
@@ -24,7 +24,7 @@
lemma starset_n_Int:
"*sn* (%n. (A n) Int (B n)) = *sn* A Int *sn* B"
apply (simp add: starset_n_def expand_set_eq all_star_eq)
-apply (simp add: Iset_star_n fuf_conj)
+apply (simp add: Iset_star_n filter.Collect_conj [OF filter_FUFNat])
done
lemma InternalSets_Int:
@@ -34,7 +34,7 @@
lemma starset_n_Compl: "*sn* ((%n. - A n)) = -( *sn* A)"
apply (simp add: starset_n_def expand_set_eq all_star_eq)
-apply (simp add: Iset_star_n fuf_not)
+apply (simp add: Iset_star_n ultrafilter.Collect_not [OF ultrafilter_FUFNat])
done
lemma InternalSets_Compl: "X \<in> InternalSets ==> -X \<in> InternalSets"
@@ -42,7 +42,8 @@
lemma starset_n_diff: "*sn* (%n. (A n) - (B n)) = *sn* A - *sn* B"
apply (simp add: starset_n_def expand_set_eq all_star_eq)
-apply (simp add: Iset_star_n fuf_conj fuf_not)
+apply (simp add: Iset_star_n filter.Collect_conj [OF filter_FUFNat]
+ ultrafilter.Collect_not [OF ultrafilter_FUFNat])
done
lemma InternalSets_diff:
@@ -99,14 +100,14 @@
text{*The hyperpow function as a nonstandard extension of realpow*}
lemma starfun_pow: "!!N. ( *f* (%n. r ^ n)) N = (hypreal_of_real r) pow N"
-by (unfold hyperpow_def, transfer, rule refl)
+by (transfer, rule refl)
lemma starfun_pow2:
"!!N. ( *f* (%n. (X n) ^ m)) N = ( *f* X) N pow hypnat_of_nat m"
-by (unfold hyperpow_def, transfer, rule refl)
+by (transfer, rule refl)
lemma starfun_pow3: "!!R. ( *f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n"
-by (unfold hyperpow_def, transfer, rule refl)
+by (transfer, rule refl)
text{*The @{term hypreal_of_hypnat} function as a nonstandard extension of
@{term real_of_nat} *}
--- a/src/HOL/Hyperreal/StarClasses.thy Mon Sep 12 23:13:46 2005 +0200
+++ b/src/HOL/Hyperreal/StarClasses.thy Mon Sep 12 23:14:41 2005 +0200
@@ -9,7 +9,148 @@
imports Transfer
begin
-subsection "HOL.thy"
+subsection {* Syntactic classes *}
+
+instance star :: (ord) ord ..
+instance star :: (zero) zero ..
+instance star :: (one) one ..
+instance star :: (plus) plus ..
+instance star :: (times) times ..
+instance star :: (minus) minus ..
+instance star :: (inverse) inverse ..
+instance star :: (number) number ..
+instance star :: ("Divides.div") "Divides.div" ..
+instance star :: (power) power ..
+
+defs (overloaded)
+ star_zero_def: "0 \<equiv> star_of 0"
+ star_one_def: "1 \<equiv> star_of 1"
+ star_number_def: "number_of b \<equiv> star_of (number_of b)"
+ star_add_def: "(op +) \<equiv> Ifun2_of (op +)"
+ star_diff_def: "(op -) \<equiv> Ifun2_of (op -)"
+ star_minus_def: "uminus \<equiv> Ifun_of uminus"
+ star_mult_def: "(op *) \<equiv> Ifun2_of (op *)"
+ star_divide_def: "(op /) \<equiv> Ifun2_of (op /)"
+ star_inverse_def: "inverse \<equiv> Ifun_of inverse"
+ star_le_def: "(op \<le>) \<equiv> Ipred2_of (op \<le>)"
+ star_less_def: "(op <) \<equiv> Ipred2_of (op <)"
+ star_abs_def: "abs \<equiv> Ifun_of abs"
+ star_div_def: "(op div) \<equiv> Ifun2_of (op div)"
+ star_mod_def: "(op mod) \<equiv> Ifun2_of (op mod)"
+ star_power_def: "(op ^) \<equiv> \<lambda>x n. Ifun_of (\<lambda>x. x ^ n) x"
+
+lemmas star_class_defs [transfer_unfold] =
+ star_zero_def star_one_def star_number_def
+ star_add_def star_diff_def star_minus_def
+ star_mult_def star_divide_def star_inverse_def
+ star_le_def star_less_def star_abs_def
+ star_div_def star_mod_def star_power_def
+
+text {* @{term star_of} preserves class operations *}
+
+lemma star_of_add: "star_of (x + y) = star_of x + star_of y"
+by transfer (rule refl)
+
+lemma star_of_diff: "star_of (x - y) = star_of x - star_of y"
+by transfer (rule refl)
+
+lemma star_of_minus: "star_of (-x) = - star_of x"
+by transfer (rule refl)
+
+lemma star_of_mult: "star_of (x * y) = star_of x * star_of y"
+by transfer (rule refl)
+
+lemma star_of_divide: "star_of (x / y) = star_of x / star_of y"
+by transfer (rule refl)
+
+lemma star_of_inverse: "star_of (inverse x) = inverse (star_of x)"
+by transfer (rule refl)
+
+lemma star_of_div: "star_of (x div y) = star_of x div star_of y"
+by transfer (rule refl)
+
+lemma star_of_mod: "star_of (x mod y) = star_of x mod star_of y"
+by transfer (rule refl)
+
+lemma star_of_power: "star_of (x ^ n) = star_of x ^ n"
+by transfer (rule refl)
+
+lemma star_of_abs: "star_of (abs x) = abs (star_of x)"
+by transfer (rule refl)
+
+text {* @{term star_of} preserves numerals *}
+
+lemma star_of_zero: "star_of 0 = 0"
+by transfer (rule refl)
+
+lemma star_of_one: "star_of 1 = 1"
+by transfer (rule refl)
+
+lemma star_of_number_of: "star_of (number_of x) = number_of x"
+by transfer (rule refl)
+
+text {* @{term star_of} preserves orderings *}
+
+lemma star_of_less: "(star_of x < star_of y) = (x < y)"
+by transfer (rule refl)
+
+lemma star_of_le: "(star_of x \<le> star_of y) = (x \<le> y)"
+by transfer (rule refl)
+
+lemma star_of_eq: "(star_of x = star_of y) = (x = y)"
+by transfer (rule refl)
+
+text{*As above, for 0*}
+
+lemmas star_of_0_less = star_of_less [of 0, simplified star_of_zero]
+lemmas star_of_0_le = star_of_le [of 0, simplified star_of_zero]
+lemmas star_of_0_eq = star_of_eq [of 0, simplified star_of_zero]
+
+lemmas star_of_less_0 = star_of_less [of _ 0, simplified star_of_zero]
+lemmas star_of_le_0 = star_of_le [of _ 0, simplified star_of_zero]
+lemmas star_of_eq_0 = star_of_eq [of _ 0, simplified star_of_zero]
+
+text{*As above, for 1*}
+
+lemmas star_of_1_less = star_of_less [of 1, simplified star_of_one]
+lemmas star_of_1_le = star_of_le [of 1, simplified star_of_one]
+lemmas star_of_1_eq = star_of_eq [of 1, simplified star_of_one]
+
+lemmas star_of_less_1 = star_of_less [of _ 1, simplified star_of_one]
+lemmas star_of_le_1 = star_of_le [of _ 1, simplified star_of_one]
+lemmas star_of_eq_1 = star_of_eq [of _ 1, simplified star_of_one]
+
+text{*As above, for numerals*}
+
+lemmas star_of_number_less =
+ star_of_less [of "number_of w", standard, simplified star_of_number_of]
+lemmas star_of_number_le =
+ star_of_le [of "number_of w", standard, simplified star_of_number_of]
+lemmas star_of_number_eq =
+ star_of_eq [of "number_of w", standard, simplified star_of_number_of]
+
+lemmas star_of_less_number =
+ star_of_less [of _ "number_of w", standard, simplified star_of_number_of]
+lemmas star_of_le_number =
+ star_of_le [of _ "number_of w", standard, simplified star_of_number_of]
+lemmas star_of_eq_number =
+ star_of_eq [of _ "number_of w", standard, simplified star_of_number_of]
+
+lemmas star_of_simps [simp] =
+ star_of_add star_of_diff star_of_minus
+ star_of_mult star_of_divide star_of_inverse
+ star_of_div star_of_mod
+ star_of_power star_of_abs
+ star_of_zero star_of_one star_of_number_of
+ star_of_less star_of_le star_of_eq
+ star_of_0_less star_of_0_le star_of_0_eq
+ star_of_less_0 star_of_le_0 star_of_eq_0
+ star_of_1_less star_of_1_le star_of_1_eq
+ star_of_less_1 star_of_le_1 star_of_eq_1
+ star_of_number_less star_of_number_le star_of_number_eq
+ star_of_less_number star_of_le_number star_of_eq_number
+
+subsection {* Ordering classes *}
instance star :: (order) order
apply (intro_classes)
@@ -23,7 +164,7 @@
by (intro_classes, transfer, rule linorder_linear)
-subsection "LOrder.thy"
+subsection {* Lattice ordering classes *}
text {*
Some extra trouble is necessary because the class axioms
@@ -57,17 +198,17 @@
instance star :: (lorder) lorder ..
-lemma star_join_def: "join \<equiv> Ifun2_of join"
+lemma star_join_def [transfer_unfold]: "join \<equiv> Ifun2_of join"
apply (rule is_join_unique[OF is_join_join, THEN eq_reflection])
apply (transfer is_join_def, rule is_join_join)
done
-lemma star_meet_def: "meet \<equiv> Ifun2_of meet"
+lemma star_meet_def [transfer_unfold]: "meet \<equiv> Ifun2_of meet"
apply (rule is_meet_unique[OF is_meet_meet, THEN eq_reflection])
apply (transfer is_meet_def, rule is_meet_meet)
done
-subsection "OrderedGroup.thy"
+subsection {* Ordered group classes *}
instance star :: (semigroup_add) semigroup_add
by (intro_classes, transfer, rule add_assoc)
@@ -123,9 +264,7 @@
instance star :: (lordered_ab_group) lordered_ab_group ..
instance star :: (lordered_ab_group_abs) lordered_ab_group_abs
-apply (intro_classes)
-apply (transfer star_join_def, rule abs_lattice)
-done
+by (intro_classes, transfer, rule abs_lattice)
text "Ring-and-Field.thy"
@@ -207,7 +346,7 @@
instance star :: (ordered_idom) ordered_idom ..
instance star :: (ordered_field) ordered_field ..
-subsection "Power.thy"
+subsection {* Power classes *}
text {*
Proving the class axiom @{thm [source] power_Suc} for type
@@ -227,11 +366,14 @@
by transfer (rule power_Suc)
qed
-subsection "Integ/Number.thy"
+subsection {* Number classes *}
-lemma star_of_nat_def: "of_nat n \<equiv> star_of (of_nat n)"
+lemma star_of_nat_def [transfer_unfold]: "of_nat n \<equiv> star_of (of_nat n)"
by (rule eq_reflection, induct_tac n, simp_all)
+lemma star_of_of_nat [simp]: "star_of (of_nat n) = of_nat n"
+by transfer (rule refl)
+
lemma int_diff_cases:
assumes prem: "\<And>m n. z = int m - int n \<Longrightarrow> P" shows "P"
apply (rule_tac z=z in int_cases)
@@ -239,19 +381,13 @@
apply (rule_tac m=0 and n="Suc n" in prem, simp)
done -- "Belongs in Integ/IntDef.thy"
-lemma star_of_int_def: "of_int z \<equiv> star_of (of_int z)"
- apply (rule eq_reflection)
- apply (rule_tac z=z in int_diff_cases)
- apply (simp add: star_of_nat_def)
-done
+lemma star_of_int_def [transfer_unfold]: "of_int z \<equiv> star_of (of_int z)"
+by (rule eq_reflection, rule_tac z=z in int_diff_cases, simp)
+
+lemma star_of_of_int [simp]: "star_of (of_int z) = of_int z"
+by transfer (rule refl)
instance star :: (number_ring) number_ring
by (intro_classes, simp only: star_number_def star_of_int_def number_of_eq)
-lemma star_of_of_nat [simp]: "star_of (of_nat n) = of_nat n"
-by (simp add: star_of_nat_def)
-
-lemma star_of_of_int [simp]: "star_of (of_int z) = of_int z"
-by (simp add: star_of_int_def)
-
end
--- a/src/HOL/Hyperreal/StarType.thy Mon Sep 12 23:13:46 2005 +0200
+++ b/src/HOL/Hyperreal/StarType.thy Mon Sep 12 23:14:41 2005 +0200
@@ -166,6 +166,10 @@
Ipred2_of :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a star \<Rightarrow> 'b star \<Rightarrow> bool)"
"Ipred2_of P \<equiv> \<lambda>x y. unstar (star_of P \<star> x \<star> y)"
+lemmas Ifun_defs =
+ Ifun_of_def Ifun2_def Ifun2_of_def
+ Ipred_def Ipred_of_def Ipred2_def Ipred2_of_def
+
lemma Ifun_of [simp]:
"Ifun_of f (star_of x) = star_of (f x)"
by (simp only: Ifun_of_def Ifun)
@@ -182,10 +186,6 @@
"Ipred2_of P (star_of x) (star_of y) = P x y"
by (simp only: Ipred2_of_def Ifun unstar)
-lemmas Ifun_defs =
- star_of_def Ifun_of_def Ifun2_def Ifun2_of_def
- Ipred_def Ipred_of_def Ipred2_def Ipred2_of_def
-
subsection {* Internal sets *}
@@ -201,147 +201,5 @@
by (simp add: Iset_def Ipred2_of_def star_of_def Ifun_star_n unstar_star_n)
-subsection {* Class constants *}
-
-instance star :: (ord) ord ..
-instance star :: (zero) zero ..
-instance star :: (one) one ..
-instance star :: (plus) plus ..
-instance star :: (times) times ..
-instance star :: (minus) minus ..
-instance star :: (inverse) inverse ..
-instance star :: (number) number ..
-instance star :: ("Divides.div") "Divides.div" ..
-instance star :: (power) power ..
-
-defs (overloaded)
- star_zero_def: "0 \<equiv> star_of 0"
- star_one_def: "1 \<equiv> star_of 1"
- star_number_def: "number_of b \<equiv> star_of (number_of b)"
- star_add_def: "(op +) \<equiv> Ifun2_of (op +)"
- star_diff_def: "(op -) \<equiv> Ifun2_of (op -)"
- star_minus_def: "uminus \<equiv> Ifun_of uminus"
- star_mult_def: "(op *) \<equiv> Ifun2_of (op *)"
- star_divide_def: "(op /) \<equiv> Ifun2_of (op /)"
- star_inverse_def: "inverse \<equiv> Ifun_of inverse"
- star_le_def: "(op \<le>) \<equiv> Ipred2_of (op \<le>)"
- star_less_def: "(op <) \<equiv> Ipred2_of (op <)"
- star_abs_def: "abs \<equiv> Ifun_of abs"
- star_div_def: "(op div) \<equiv> Ifun2_of (op div)"
- star_mod_def: "(op mod) \<equiv> Ifun2_of (op mod)"
- star_power_def: "(op ^) \<equiv> \<lambda>x n. Ifun_of (\<lambda>x. x ^ n) x"
-
-lemmas star_class_defs =
- star_zero_def star_one_def star_number_def
- star_add_def star_diff_def star_minus_def
- star_mult_def star_divide_def star_inverse_def
- star_le_def star_less_def star_abs_def
- star_div_def star_mod_def star_power_def
-
-text {* @{term star_of} preserves class operations *}
-
-lemma star_of_add: "star_of (x + y) = star_of x + star_of y"
-by (simp add: star_add_def)
-
-lemma star_of_diff: "star_of (x - y) = star_of x - star_of y"
-by (simp add: star_diff_def)
-
-lemma star_of_minus: "star_of (-x) = - star_of x"
-by (simp add: star_minus_def)
-
-lemma star_of_mult: "star_of (x * y) = star_of x * star_of y"
-by (simp add: star_mult_def)
-
-lemma star_of_divide: "star_of (x / y) = star_of x / star_of y"
-by (simp add: star_divide_def)
-
-lemma star_of_inverse: "star_of (inverse x) = inverse (star_of x)"
-by (simp add: star_inverse_def)
-
-lemma star_of_div: "star_of (x div y) = star_of x div star_of y"
-by (simp add: star_div_def)
-
-lemma star_of_mod: "star_of (x mod y) = star_of x mod star_of y"
-by (simp add: star_mod_def)
-
-lemma star_of_power: "star_of (x ^ n) = star_of x ^ n"
-by (simp add: star_power_def)
-
-lemma star_of_abs: "star_of (abs x) = abs (star_of x)"
-by (simp add: star_abs_def)
-
-text {* @{term star_of} preserves numerals *}
-
-lemma star_of_zero: "star_of 0 = 0"
-by (simp add: star_zero_def)
-
-lemma star_of_one: "star_of 1 = 1"
-by (simp add: star_one_def)
-
-lemma star_of_number_of: "star_of (number_of x) = number_of x"
-by (simp add: star_number_def)
-
-text {* @{term star_of} preserves orderings *}
-
-lemma star_of_less: "(star_of x < star_of y) = (x < y)"
-by (simp add: star_less_def)
-
-lemma star_of_le: "(star_of x \<le> star_of y) = (x \<le> y)"
-by (simp add: star_le_def)
-
-lemma star_of_eq: "(star_of x = star_of y) = (x = y)"
-by (rule star_of_inject)
-
-text{*As above, for 0*}
-
-lemmas star_of_0_less = star_of_less [of 0, simplified star_of_zero]
-lemmas star_of_0_le = star_of_le [of 0, simplified star_of_zero]
-lemmas star_of_0_eq = star_of_eq [of 0, simplified star_of_zero]
-
-lemmas star_of_less_0 = star_of_less [of _ 0, simplified star_of_zero]
-lemmas star_of_le_0 = star_of_le [of _ 0, simplified star_of_zero]
-lemmas star_of_eq_0 = star_of_eq [of _ 0, simplified star_of_zero]
-
-text{*As above, for 1*}
-
-lemmas star_of_1_less = star_of_less [of 1, simplified star_of_one]
-lemmas star_of_1_le = star_of_le [of 1, simplified star_of_one]
-lemmas star_of_1_eq = star_of_eq [of 1, simplified star_of_one]
-
-lemmas star_of_less_1 = star_of_less [of _ 1, simplified star_of_one]
-lemmas star_of_le_1 = star_of_le [of _ 1, simplified star_of_one]
-lemmas star_of_eq_1 = star_of_eq [of _ 1, simplified star_of_one]
-
-text{*As above, for numerals*}
-
-lemmas star_of_number_less =
- star_of_less [of "number_of b", simplified star_of_number_of, standard]
-lemmas star_of_number_le =
- star_of_le [of "number_of b", simplified star_of_number_of, standard]
-lemmas star_of_number_eq =
- star_of_eq [of "number_of b", simplified star_of_number_of, standard]
-
-lemmas star_of_less_number =
- star_of_less [of _ "number_of b", simplified star_of_number_of, standard]
-lemmas star_of_le_number =
- star_of_le [of _ "number_of b", simplified star_of_number_of, standard]
-lemmas star_of_eq_number =
- star_of_eq [of _ "number_of b", simplified star_of_number_of, standard]
-
-lemmas star_of_simps =
- star_of_add star_of_diff star_of_minus
- star_of_mult star_of_divide star_of_inverse
- star_of_div star_of_mod
- star_of_power star_of_abs
- star_of_zero star_of_one star_of_number_of
- star_of_less star_of_le star_of_eq
- star_of_0_less star_of_0_le star_of_0_eq
- star_of_less_0 star_of_le_0 star_of_eq_0
- star_of_1_less star_of_1_le star_of_1_eq
- star_of_less_1 star_of_le_1 star_of_eq_1
- star_of_number_less star_of_number_le star_of_number_eq
- star_of_less_number star_of_le_number star_of_eq_number
-
-declare star_of_simps [simp]
end
--- a/src/HOL/Hyperreal/Transfer.thy Mon Sep 12 23:13:46 2005 +0200
+++ b/src/HOL/Hyperreal/Transfer.thy Mon Sep 12 23:14:41 2005 +0200
@@ -7,70 +7,9 @@
theory Transfer
imports StarType
+uses ("transfer.ML")
begin
-subsection {* Preliminaries *}
-
-text {* These transform expressions like @{term "{n. f (P n)} \<in> \<U>"} *}
-
-lemma fuf_ex:
- "({n. \<exists>x. P n x} \<in> \<U>) = (\<exists>X. {n. P n (X n)} \<in> \<U>)"
-proof
- assume "{n. \<exists>x. P n x} \<in> \<U>"
- hence "{n. P n (SOME x. P n x)} \<in> \<U>"
- by (auto elim: someI filter.subset [OF filter_FUFNat])
- thus "\<exists>X. {n. P n (X n)} \<in> \<U>" by fast
-next
- show "\<exists>X. {n. P n (X n)} \<in> \<U> \<Longrightarrow> {n. \<exists>x. P n x} \<in> \<U>"
- by (auto elim: filter.subset [OF filter_FUFNat])
-qed
-
-lemma fuf_not: "({n. \<not> P n} \<in> \<U>) = ({n. P n} \<notin> \<U>)"
- apply (subst Collect_neg_eq)
- apply (rule ultrafilter.Compl_iff [OF ultrafilter_FUFNat])
-done
-
-lemma fuf_conj:
- "({n. P n \<and> Q n} \<in> \<U>) = ({n. P n} \<in> \<U> \<and> {n. Q n} \<in> \<U>)"
- apply (subst Collect_conj_eq)
- apply (rule filter.Int_iff [OF filter_FUFNat])
-done
-
-lemma fuf_disj:
- "({n. P n \<or> Q n} \<in> \<U>) = ({n. P n} \<in> \<U> \<or> {n. Q n} \<in> \<U>)"
- apply (subst Collect_disj_eq)
- apply (rule ultrafilter.Un_iff [OF ultrafilter_FUFNat])
-done
-
-lemma fuf_imp:
- "({n. P n \<longrightarrow> Q n} \<in> \<U>) = ({n. P n} \<in> \<U> \<longrightarrow> {n. Q n} \<in> \<U>)"
-by (simp only: imp_conv_disj fuf_disj fuf_not)
-
-lemma fuf_iff:
- "({n. P n = Q n} \<in> \<U>) = (({n. P n} \<in> \<U>) = ({n. Q n} \<in> \<U>))"
-by (simp add: iff_conv_conj_imp fuf_conj fuf_imp)
-
-lemma fuf_all:
- "({n. \<forall>x. P n x} \<in> \<U>) = (\<forall>X. {n. P n (X n)} \<in> \<U>)"
- apply (rule Not_eq_iff [THEN iffD1])
- apply (simp add: fuf_not [symmetric])
- apply (rule fuf_ex)
-done
-
-lemma fuf_if_bool:
- "({n. if P n then Q n else R n} \<in> \<U>) =
- (if {n. P n} \<in> \<U> then {n. Q n} \<in> \<U> else {n. R n} \<in> \<U>)"
-by (simp add: if_bool_eq_conj fuf_conj fuf_imp fuf_not)
-
-lemma fuf_eq:
- "({n. X n = Y n} \<in> \<U>) = (star_n X = star_n Y)"
-by (rule star_n_eq_iff [symmetric])
-
-lemma fuf_if:
- "star_n (\<lambda>n. if P n then X n else Y n) =
- (if {n. P n} \<in> \<U> then star_n X else star_n Y)"
-by (auto simp add: star_n_eq_iff fuf_not [symmetric] elim: ultra)
-
subsection {* Starting the transfer proof *}
text {*
@@ -88,6 +27,12 @@
"P \<equiv> {n. Q} \<in> \<U> \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
by (subgoal_tac "P \<equiv> Q", simp, simp add: atomize_eq)
+use "transfer.ML"
+setup Transfer.setup
+
+declare Ifun_defs [transfer_unfold]
+declare Iset_of_def [transfer_unfold]
+
subsection {* Transfer introduction rules *}
text {*
@@ -112,63 +57,57 @@
lemma transfer_not:
"\<lbrakk>p \<equiv> {n. P n} \<in> \<U>\<rbrakk> \<Longrightarrow> \<not> p \<equiv> {n. \<not> P n} \<in> \<U>"
-by (simp only: fuf_not)
+by (simp only: ultrafilter.Collect_not [OF ultrafilter_FUFNat])
lemma transfer_conj:
"\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
\<Longrightarrow> p \<and> q \<equiv> {n. P n \<and> Q n} \<in> \<U>"
-by (simp only: fuf_conj)
+by (simp only: filter.Collect_conj [OF filter_FUFNat])
lemma transfer_disj:
"\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
\<Longrightarrow> p \<or> q \<equiv> {n. P n \<or> Q n} \<in> \<U>"
-by (simp only: fuf_disj)
+by (simp only: ultrafilter.Collect_disj [OF ultrafilter_FUFNat])
lemma transfer_imp:
"\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
\<Longrightarrow> p \<longrightarrow> q \<equiv> {n. P n \<longrightarrow> Q n} \<in> \<U>"
-by (simp only: fuf_imp)
+by (simp only: imp_conv_disj transfer_disj transfer_not)
lemma transfer_iff:
"\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
\<Longrightarrow> p = q \<equiv> {n. P n = Q n} \<in> \<U>"
-by (simp only: fuf_iff)
+by (simp only: iff_conv_conj_imp transfer_conj transfer_imp)
lemma transfer_if_bool:
"\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; x \<equiv> {n. X n} \<in> \<U>; y \<equiv> {n. Y n} \<in> \<U>\<rbrakk>
\<Longrightarrow> (if p then x else y) \<equiv> {n. if P n then X n else Y n} \<in> \<U>"
-by (simp only: fuf_if_bool)
-
-lemma transfer_all_bool:
- "\<lbrakk>\<And>x. p x \<equiv> {n. P n x} \<in> \<U>\<rbrakk> \<Longrightarrow> \<forall>x::bool. p x \<equiv> {n. \<forall>x. P n x} \<in> \<U>"
-by (simp only: all_bool_eq fuf_conj)
-
-lemma transfer_ex_bool:
- "\<lbrakk>\<And>x. p x \<equiv> {n. P n x} \<in> \<U>\<rbrakk> \<Longrightarrow> \<exists>x::bool. p x \<equiv> {n. \<exists>x. P n x} \<in> \<U>"
-by (simp only: ex_bool_eq fuf_disj)
+by (simp only: if_bool_eq_conj transfer_conj transfer_imp transfer_not)
subsubsection {* Equals, If *}
lemma transfer_eq:
"\<lbrakk>x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk> \<Longrightarrow> x = y \<equiv> {n. X n = Y n} \<in> \<U>"
-by (simp only: fuf_eq)
+by (simp only: star_n_eq_iff)
lemma transfer_if:
"\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk>
\<Longrightarrow> (if p then x else y) \<equiv> star_n (\<lambda>n. if P n then X n else Y n)"
-by (simp only: fuf_if)
+apply (rule eq_reflection)
+apply (auto simp add: star_n_eq_iff transfer_not elim!: ultra)
+done
subsubsection {* Quantifiers *}
+lemma transfer_ex:
+ "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
+ \<Longrightarrow> \<exists>x::'a star. p x \<equiv> {n. \<exists>x. P n x} \<in> \<U>"
+by (simp only: ex_star_eq filter.Collect_ex [OF filter_FUFNat])
+
lemma transfer_all:
"\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
\<Longrightarrow> \<forall>x::'a star. p x \<equiv> {n. \<forall>x. P n x} \<in> \<U>"
-by (simp only: all_star_eq fuf_all)
-
-lemma transfer_ex:
- "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
- \<Longrightarrow> \<exists>x::'a star. p x \<equiv> {n. \<exists>x. P n x} \<in> \<U>"
-by (simp only: ex_star_eq fuf_ex)
+by (simp only: all_star_eq ultrafilter.Collect_all [OF ultrafilter_FUFNat])
lemma transfer_ex1:
"\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
@@ -220,20 +159,25 @@
\<Longrightarrow> \<exists>x\<in>a. p x \<equiv> {n. \<exists>x\<in>A n. P n x} \<in> \<U>"
by (simp only: Bex_def transfer_ex transfer_conj transfer_mem)
+
subsubsection {* Miscellaneous *}
lemma transfer_unstar:
"p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> {n. P n} \<in> \<U>"
by (simp only: unstar_star_n)
+lemma transfer_star_of: "star_of x \<equiv> star_n (\<lambda>n. x)"
+by (rule star_of_def)
+
lemma transfer_star_n: "star_n X \<equiv> star_n (\<lambda>n. X n)"
by (rule reflexive)
lemma transfer_bool: "p \<equiv> {n. p} \<in> \<U>"
by (simp add: atomize_eq)
-lemmas transfer_intros =
+lemmas transfer_intros [transfer_intro] =
transfer_star_n
+ transfer_star_of
transfer_Ifun
transfer_fun_eq
@@ -243,8 +187,6 @@
transfer_imp
transfer_iff
transfer_if_bool
- transfer_all_bool
- transfer_ex_bool
transfer_all
transfer_ex
@@ -261,148 +203,6 @@
transfer_ball
transfer_bex
-subsection {* Transfer tactic *}
-
-text {*
- We start by giving ML bindings for the theorems that
- will used by the transfer tactic. Ideally, some of the
- lists of theorems should be expandable.
- To @{text star_class_defs} we would like to add theorems
- about @{term nat_of}, @{term int_of}, @{term meet},
- @{term join}, etc.
- Also, we would like to create introduction rules for new
- constants.
-*}
-
-ML_setup {*
-val atomizers = map thm ["atomize_all", "atomize_imp", "atomize_eq"]
-val Ifun_defs = thms "Ifun_defs" @ [thm "Iset_of_def"]
-val star_class_defs = thms "star_class_defs"
-val transfer_defs = atomizers @ Ifun_defs @ star_class_defs
-
-val transfer_start = thm "transfer_start"
-val transfer_intros = thms "transfer_intros"
-val transfer_Ifun = thm "transfer_Ifun"
-*}
-
-text {*
- Next we define the ML function @{text unstar_term}.
- This function takes a term, and gives back an equivalent
- term that does not contain any references to the @{text star}
- type constructor. Hopefully the resulting term will still be
- type-correct: Any constant whose type contains @{text star}
- should either be polymorphic (so that it will still work at
- the un-starred instance) or listed in @{text star_consts}
- (so it can be removed).
- Maybe @{text star_consts} should be extensible?
-*}
-
-ML_setup {*
-local
- fun unstar_typ (Type ("StarType.star",[t])) = unstar_typ t
- | unstar_typ (Type (a, Ts)) = Type (a, map unstar_typ Ts)
- | unstar_typ T = T
-
- val star_consts =
- [ "StarType.star_of", "StarType.Ifun"
- , "StarType.Ifun_of", "StarType.Ifun2"
- , "StarType.Ifun2_of", "StarType.Ipred"
- , "StarType.Ipred_of", "StarType.Ipred2"
- , "StarType.Ipred2_of", "StarType.Iset"
- , "StarType.Iset_of", "StarType.unstar" ]
-
- fun is_star_const a = exists (fn x => x = a) star_consts
-in
- fun unstar_term (Const(a,T) $ x) = if (is_star_const a)
- then (unstar_term x)
- else (Const(a,unstar_typ T) $ unstar_term x)
- | unstar_term (f $ t) = unstar_term f $ unstar_term t
- | unstar_term (Const(a,T)) = Const(a,unstar_typ T)
- | unstar_term (Abs(a,T,t)) = Abs(a,unstar_typ T,unstar_term t)
- | unstar_term t = t
-end
-*}
-
-text {*
- The @{text transfer_thm_of} function takes a term that
- represents a proposition, and proves that it is logically
- equivalent to the un-starred version. Assuming all goes
- well, it returns a theorem asserting the equivalence.
-*}
-
-text {*
- TODO: We need some error messages for when things go
- wrong. Errors may be caused by constants that don't have
- matching introduction rules, or quantifiers over wrong types.
-*}
-
-ML_setup {*
-local
- val tacs =
- [ match_tac [transitive_thm] 1
- , resolve_tac [transfer_start] 1
- , REPEAT_ALL_NEW (resolve_tac transfer_intros) 1
- , match_tac [reflexive_thm] 1 ]
-in
- fun transfer_thm_of sg ths t =
- let val u = unstar_term t
- val e = Const("==", propT --> propT --> propT)
- val c = cterm_of sg (e $ t $ u)
- in prove_goalw_cterm (transfer_defs @ ths) c (fn _ => tacs)
- end
-end
-*}
-
-text {*
- Instead of applying the @{thm [source] transfer_start} rule
- right away, the proof of each transfer theorem starts with the
- transitivity rule @{text "\<lbrakk>P \<equiv> ?Q; ?Q \<equiv> P'\<rbrakk> \<Longrightarrow> P \<equiv> P'"}, which
- introduces a new unbound schematic variable @{text ?Q}. The first
- premise @{text "P \<equiv> ?Q"} is solved by recursively using
- @{thm [source] transfer_start} and @{thm [source] transfer_intros}.
- Each rule application adds constraints to the form of @{text ?Q};
- by the time the first premise is proved, @{text ?Q} is completely
- bound to the value of @{term P'}. Finally, the second premise is
- resolved with the reflexivity rule @{text "P' \<equiv> P'"}.
-*}
-
-text {*
- The delayed binding is necessary for the correct operation of the
- introduction rule @{thm [source] transfer_Ifun}:
- @{thm transfer_Ifun[of f _ x]}. With a subgoal of the form
- @{term "f \<star> x \<equiv> star_n (\<lambda>n. F n (X n))"}, we would like to bind @{text ?F}
- to @{text F} and @{text ?X} to @{term X}. Unfortunately, higher-order
- unification finds more than one possible match, and binds @{text ?F}
- to @{term "\<lambda>x. x"} by default. If the right-hand side of the subgoal
- contains an unbound schematic variable instead of the explicit
- application @{term "F n (X n)"}, then we can ensure that there is
- only one possible way to match the rule.
-*}
-
-ML_setup {*
-fun transfer_tac ths =
- SUBGOAL (fn (t,i) =>
- (fn th =>
- let val tr = transfer_thm_of (sign_of_thm th) ths t
- in rewrite_goals_tac [tr] th
- end
- )
- )
-*}
-
-text {*
- Finally we set up the @{text transfer} method. It takes
- an optional list of definitions as arguments; they are
- passed along to @{text transfer_thm_of}, which expands
- the definitions before attempting to prove the transfer
- theorem.
-*}
-
-method_setup transfer = {*
- Method.thms_args
- (fn ths => Method.SIMPLE_METHOD' HEADGOAL (transfer_tac ths))
-*} "transfer principle"
-
text {* Sample theorems *}
lemma Ifun_inject: "\<And>f g. (Ifun f = Ifun g) = (f = g)"
--- a/src/HOL/Hyperreal/transfer.ML Mon Sep 12 23:13:46 2005 +0200
+++ b/src/HOL/Hyperreal/transfer.ML Mon Sep 12 23:14:41 2005 +0200
@@ -127,13 +127,16 @@
val transfer_method = Method.SIMPLE_METHOD' HEADGOAL o transfer_tac;
val setup =
- [ TransferData.init
- , Attrib.add_attributes
- [ ("transfer_intro", intro_attr, "transfer introduction rule")
- , ("transfer_unfold", unfold_attr, "transfer unfolding rule")
- , ("transfer_refold", refold_attr, "transfer refolding rule")
- ]
- , Method.add_method
+ [ TransferData.init,
+ Attrib.add_attributes
+ [ ("transfer_intro", intro_attr,
+ "declaration of transfer introduction rule"),
+ ("transfer_unfold", unfold_attr,
+ "declaration of transfer unfolding rule"),
+ ("transfer_refold", refold_attr,
+ "declaration of transfer refolding rule")
+ ],
+ Method.add_method
("transfer", Method.thms_args transfer_method, "transfer principle")
];