--- a/src/HOL/Code_Numeral.thy Tue Feb 25 23:12:48 2014 +0100
+++ b/src/HOL/Code_Numeral.thy Tue Feb 25 23:14:51 2014 +0100
@@ -928,6 +928,11 @@
hide_const (open) Nat
+lifting_update integer.lifting
+lifting_forget integer.lifting
+
+lifting_update natural.lifting
+lifting_forget natural.lifting
code_reflect Code_Numeral
datatypes natural = _
--- a/src/HOL/Complex.thy Tue Feb 25 23:12:48 2014 +0100
+++ b/src/HOL/Complex.thy Tue Feb 25 23:14:51 2014 +0100
@@ -557,6 +557,109 @@
bounded_linear.isCont [OF bounded_linear_cnj]
+subsection{*Basic Lemmas*}
+
+lemma complex_eq_0: "z=0 \<longleftrightarrow> (Re z)\<^sup>2 + (Im z)\<^sup>2 = 0"
+ by (metis complex_Im_zero complex_Re_zero complex_eqI sum_power2_eq_zero_iff)
+
+lemma complex_neq_0: "z\<noteq>0 \<longleftrightarrow> (Re z)\<^sup>2 + (Im z)\<^sup>2 > 0"
+by (metis complex_eq_0 less_numeral_extra(3) sum_power2_gt_zero_iff)
+
+lemma complex_norm_square: "of_real ((norm z)\<^sup>2) = z * cnj z"
+apply (cases z, auto)
+by (metis complex_of_real_def of_real_add of_real_power power2_eq_square)
+
+lemma complex_div_eq_0:
+ "(Re(a / b) = 0 \<longleftrightarrow> Re(a * cnj b) = 0) & (Im(a / b) = 0 \<longleftrightarrow> Im(a * cnj b) = 0)"
+proof (cases "b=0")
+ case True then show ?thesis by auto
+next
+ case False
+ show ?thesis
+ proof (cases b)
+ case (Complex x y)
+ then have "x\<^sup>2 + y\<^sup>2 > 0"
+ by (metis Complex_eq_0 False sum_power2_gt_zero_iff)
+ then have "!!u v. u / (x\<^sup>2 + y\<^sup>2) + v / (x\<^sup>2 + y\<^sup>2) = (u + v) / (x\<^sup>2 + y\<^sup>2)"
+ by (metis add_divide_distrib)
+ with Complex False show ?thesis
+ by (auto simp: complex_divide_def)
+ qed
+qed
+
+lemma re_complex_div_eq_0: "Re(a / b) = 0 \<longleftrightarrow> Re(a * cnj b) = 0"
+ and im_complex_div_eq_0: "Im(a / b) = 0 \<longleftrightarrow> Im(a * cnj b) = 0"
+using complex_div_eq_0 by auto
+
+
+lemma complex_div_gt_0:
+ "(Re(a / b) > 0 \<longleftrightarrow> Re(a * cnj b) > 0) & (Im(a / b) > 0 \<longleftrightarrow> Im(a * cnj b) > 0)"
+proof (cases "b=0")
+ case True then show ?thesis by auto
+next
+ case False
+ show ?thesis
+ proof (cases b)
+ case (Complex x y)
+ then have "x\<^sup>2 + y\<^sup>2 > 0"
+ by (metis Complex_eq_0 False sum_power2_gt_zero_iff)
+ moreover have "!!u v. u / (x\<^sup>2 + y\<^sup>2) + v / (x\<^sup>2 + y\<^sup>2) = (u + v) / (x\<^sup>2 + y\<^sup>2)"
+ by (metis add_divide_distrib)
+ ultimately show ?thesis using Complex False `0 < x\<^sup>2 + y\<^sup>2`
+ apply (simp add: complex_divide_def zero_less_divide_iff less_divide_eq)
+ apply (metis less_divide_eq mult_zero_left diff_conv_add_uminus minus_divide_left)
+ done
+ qed
+qed
+
+lemma re_complex_div_gt_0: "Re(a / b) > 0 \<longleftrightarrow> Re(a * cnj b) > 0"
+ and im_complex_div_gt_0: "Im(a / b) > 0 \<longleftrightarrow> Im(a * cnj b) > 0"
+using complex_div_gt_0 by auto
+
+lemma re_complex_div_ge_0: "Re(a / b) \<ge> 0 \<longleftrightarrow> Re(a * cnj b) \<ge> 0"
+ by (metis le_less re_complex_div_eq_0 re_complex_div_gt_0)
+
+lemma im_complex_div_ge_0: "Im(a / b) \<ge> 0 \<longleftrightarrow> Im(a * cnj b) \<ge> 0"
+ by (metis im_complex_div_eq_0 im_complex_div_gt_0 le_less)
+
+lemma re_complex_div_lt_0: "Re(a / b) < 0 \<longleftrightarrow> Re(a * cnj b) < 0"
+ by (smt re_complex_div_eq_0 re_complex_div_gt_0)
+
+lemma im_complex_div_lt_0: "Im(a / b) < 0 \<longleftrightarrow> Im(a * cnj b) < 0"
+ by (metis im_complex_div_eq_0 im_complex_div_gt_0 less_asym neq_iff)
+
+lemma re_complex_div_le_0: "Re(a / b) \<le> 0 \<longleftrightarrow> Re(a * cnj b) \<le> 0"
+ by (metis not_le re_complex_div_gt_0)
+
+lemma im_complex_div_le_0: "Im(a / b) \<le> 0 \<longleftrightarrow> Im(a * cnj b) \<le> 0"
+ by (metis im_complex_div_gt_0 not_le)
+
+lemma Re_setsum: "finite s \<Longrightarrow> Re(setsum f s) = setsum (%x. Re(f x)) s"
+ by (induct s rule: finite_induct) auto
+
+lemma Im_setsum: "finite s \<Longrightarrow> Im(setsum f s) = setsum (%x. Im(f x)) s"
+ by (induct s rule: finite_induct) auto
+
+lemma Complex_setsum': "finite s \<Longrightarrow> setsum (%x. Complex (f x) 0) s = Complex (setsum f s) 0"
+ by (induct s rule: finite_induct) auto
+
+lemma Complex_setsum: "finite s \<Longrightarrow> Complex (setsum f s) 0 = setsum (%x. Complex (f x) 0) s"
+ by (metis Complex_setsum')
+
+lemma cnj_setsum: "finite s \<Longrightarrow> cnj (setsum f s) = setsum (%x. cnj (f x)) s"
+ by (induct s rule: finite_induct) (auto simp: complex_cnj_add)
+
+lemma Reals_cnj_iff: "z \<in> \<real> \<longleftrightarrow> cnj z = z"
+by (metis Reals_cases Reals_of_real complex.exhaust complex.inject complex_cnj
+ complex_of_real_def equal_neg_zero)
+
+lemma Complex_in_Reals: "Complex x 0 \<in> \<real>"
+ by (metis Reals_of_real complex_of_real_def)
+
+lemma in_Reals_norm: "z \<in> \<real> \<Longrightarrow> norm(z) = abs(Re z)"
+ by (metis Re_complex_of_real Reals_cases norm_of_real)
+
+
subsection{*Finally! Polar Form for Complex Numbers*}
subsubsection {* $\cos \theta + i \sin \theta$ *}
--- a/src/HOL/Library/Code_Target_Int.thy Tue Feb 25 23:12:48 2014 +0100
+++ b/src/HOL/Library/Code_Target_Int.thy Tue Feb 25 23:14:51 2014 +0100
@@ -12,6 +12,10 @@
declare [[code drop: integer_of_int]]
+context
+includes integer.lifting
+begin
+
lemma [code]:
"integer_of_int (int_of_integer k) = k"
by transfer rule
@@ -86,6 +90,7 @@
lemma [code]:
"k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
by transfer rule
+end
lemma (in ring_1) of_int_code_if:
"of_int k = (if k = 0 then 0
@@ -105,7 +110,7 @@
lemma [code]:
"nat = nat_of_integer \<circ> of_int"
- by transfer (simp add: fun_eq_iff)
+ including integer.lifting by transfer (simp add: fun_eq_iff)
code_identifier
code_module Code_Target_Int \<rightharpoonup>
--- a/src/HOL/Library/Code_Target_Nat.thy Tue Feb 25 23:12:48 2014 +0100
+++ b/src/HOL/Library/Code_Target_Nat.thy Tue Feb 25 23:14:51 2014 +0100
@@ -10,6 +10,10 @@
subsection {* Implementation for @{typ nat} *}
+context
+includes natural.lifting integer.lifting
+begin
+
lift_definition Nat :: "integer \<Rightarrow> nat"
is nat
.
@@ -96,6 +100,8 @@
"num_of_nat = num_of_integer \<circ> of_nat"
by transfer (simp add: fun_eq_iff)
+end
+
lemma (in semiring_1) of_nat_code_if:
"of_nat n = (if n = 0 then 0
else let
@@ -120,7 +126,7 @@
lemma [code abstract]:
"integer_of_nat (nat k) = max 0 (integer_of_int k)"
- by transfer auto
+ including integer.lifting by transfer auto
lemma term_of_nat_code [code]:
-- {* Use @{term Code_Numeral.nat_of_integer} in term reconstruction
@@ -139,7 +145,7 @@
"nat_of_integer 0 = 0"
"nat_of_integer 1 = 1"
"nat_of_integer (numeral k) = numeral k"
- by (transfer, simp)+
+ including integer.lifting by (transfer, simp)+
code_identifier
code_module Code_Target_Nat \<rightharpoonup>
--- a/src/HOL/Library/FSet.thy Tue Feb 25 23:12:48 2014 +0100
+++ b/src/HOL/Library/FSet.thy Tue Feb 25 23:14:51 2014 +0100
@@ -176,16 +176,8 @@
lift_definition ffilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Set.filter
parametric Lifting_Set.filter_transfer unfolding Set.filter_def by simp
-lemma compose_rel_to_Domainp:
- assumes "left_unique R"
- assumes "(R ===> op=) P P'"
- shows "(R OO Lifting.invariant P' OO R\<inverse>\<inverse>) x y \<longleftrightarrow> Domainp R x \<and> P x \<and> x = y"
-using assms unfolding OO_def conversep_iff Domainp_iff left_unique_def fun_rel_def invariant_def
-by blast
-
lift_definition fPow :: "'a fset \<Rightarrow> 'a fset fset" is Pow parametric Pow_transfer
-by (subst compose_rel_to_Domainp [OF _ finite_transfer]) (auto intro: transfer_raw finite_subset
- simp add: fset.pcr_cr_eq[symmetric] Domainp_set fset.domain_eq)
+by (simp add: finite_subset)
lift_definition fcard :: "'a fset \<Rightarrow> nat" is card parametric card_transfer .
@@ -194,13 +186,10 @@
lift_definition fthe_elem :: "'a fset \<Rightarrow> 'a" is the_elem .
-(* FIXME why is not invariant here unfolded ? *)
-lift_definition fbind :: "'a fset \<Rightarrow> ('a \<Rightarrow> 'b fset) \<Rightarrow> 'b fset" is Set.bind parametric bind_transfer
-unfolding invariant_def Set.bind_def by clarsimp metis
+lift_definition fbind :: "'a fset \<Rightarrow> ('a \<Rightarrow> 'b fset) \<Rightarrow> 'b fset" is Set.bind parametric bind_transfer
+by (simp add: Set.bind_def)
-lift_definition ffUnion :: "'a fset fset \<Rightarrow> 'a fset" is Union parametric Union_transfer
-by (subst(asm) compose_rel_to_Domainp [OF _ finite_transfer])
- (auto intro: transfer_raw simp add: fset.pcr_cr_eq[symmetric] Domainp_set fset.domain_eq invariant_def)
+lift_definition ffUnion :: "'a fset fset \<Rightarrow> 'a fset" is Union parametric Union_transfer by simp
lift_definition fBall :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Ball parametric Ball_transfer .
lift_definition fBex :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Bex parametric Bex_transfer .
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue Feb 25 23:12:48 2014 +0100
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue Feb 25 23:14:51 2014 +0100
@@ -7,6 +7,7 @@
begin
subsection {* Square root of complex numbers *}
+
definition csqrt :: "complex \<Rightarrow> complex" where
"csqrt z = (if Im z = 0 then
if 0 \<le> Re z then Complex (sqrt(Re z)) 0
@@ -54,6 +55,39 @@
ultimately show ?thesis by blast
qed
+lemma csqrt_Complex: "x \<ge> 0 \<Longrightarrow> csqrt (Complex x 0) = Complex (sqrt x) 0"
+ by (simp add: csqrt_def)
+
+lemma csqrt_0 [simp]: "csqrt 0 = 0"
+ by (simp add: csqrt_def)
+
+lemma csqrt_1 [simp]: "csqrt 1 = 1"
+ by (simp add: csqrt_def)
+
+lemma csqrt_principal: "0 < Re(csqrt(z)) | Re(csqrt(z)) = 0 & 0 \<le> Im(csqrt(z))"
+proof (cases z)
+ case (Complex x y)
+ then show ?thesis
+ using real_sqrt_sum_squares_ge1 [of "x" y]
+ real_sqrt_sum_squares_ge1 [of "-x" y]
+ real_sqrt_sum_squares_eq_cancel [of x y]
+ apply (auto simp: csqrt_def intro!: Rings.ordered_ring_class.split_mult_pos_le)
+ apply (metis add_commute diff_add_cancel le_add_same_cancel1 real_sqrt_sum_squares_ge1)
+ by (metis add_commute less_eq_real_def power_minus_Bit0 real_0_less_add_iff real_sqrt_sum_squares_eq_cancel)
+qed
+
+lemma Re_csqrt: "0 \<le> Re(csqrt z)"
+ by (metis csqrt_principal le_less)
+
+lemma csqrt_square: "(0 < Re z | Re z = 0 & 0 \<le> Im z) \<Longrightarrow> csqrt (z^2) = z"
+ using csqrt [of "z^2"] csqrt_principal [of "z^2"]
+ by (cases z) (auto simp: power2_eq_iff)
+
+lemma csqrt_eq_0 [simp]: "csqrt z = 0 \<longleftrightarrow> z = 0"
+ by auto (metis csqrt power_eq_0_iff)
+
+lemma csqrt_eq_1 [simp]: "csqrt z = 1 \<longleftrightarrow> z = 1"
+ by auto (metis csqrt power2_eq_1_iff)
subsection{* More lemmas about module of complex numbers *}
@@ -64,27 +98,29 @@
lemma complex_mod_triangle_sub: "cmod w \<le> cmod (w + z) + norm z"
using complex_mod_triangle_ineq2[of "w + z" "-z"] by auto
-subsection{* Basic lemmas about complex polynomials *}
+subsection{* Basic lemmas about polynomials *}
lemma poly_bound_exists:
- shows "\<exists>m. m > 0 \<and> (\<forall>z. cmod z <= r \<longrightarrow> cmod (poly p z) \<le> m)"
+ fixes p:: "('a::{comm_semiring_0,real_normed_div_algebra}) poly"
+ shows "\<exists>m. m > 0 \<and> (\<forall>z. norm z <= r \<longrightarrow> norm (poly p z) \<le> m)"
proof(induct p)
case 0 thus ?case by (rule exI[where x=1], simp)
next
case (pCons c cs)
- from pCons.hyps obtain m where m: "\<forall>z. cmod z \<le> r \<longrightarrow> cmod (poly cs z) \<le> m"
+ from pCons.hyps obtain m where m: "\<forall>z. norm z \<le> r \<longrightarrow> norm (poly cs z) \<le> m"
by blast
- let ?k = " 1 + cmod c + \<bar>r * m\<bar>"
+ let ?k = " 1 + norm c + \<bar>r * m\<bar>"
have kp: "?k > 0" using abs_ge_zero[of "r*m"] norm_ge_zero[of c] by arith
- {fix z
- assume H: "cmod z \<le> r"
- from m H have th: "cmod (poly cs z) \<le> m" by blast
+ {fix z :: 'a
+ assume H: "norm z \<le> r"
+ from m H have th: "norm (poly cs z) \<le> m" by blast
from H have rp: "r \<ge> 0" using norm_ge_zero[of z] by arith
- have "cmod (poly (pCons c cs) z) \<le> cmod c + cmod (z* poly cs z)"
+ have "norm (poly (pCons c cs) z) \<le> norm c + norm (z* poly cs z)"
using norm_triangle_ineq[of c "z* poly cs z"] by simp
- also have "\<dots> \<le> cmod c + r*m" using mult_mono[OF H th rp norm_ge_zero[of "poly cs z"]] by (simp add: norm_mult)
+ also have "\<dots> \<le> norm c + r*m" using mult_mono[OF H th rp norm_ge_zero[of "poly cs z"]]
+ by (simp add: norm_mult)
also have "\<dots> \<le> ?k" by simp
- finally have "cmod (poly (pCons c cs) z) \<le> ?k" .}
+ finally have "norm (poly (pCons c cs) z) \<le> ?k" .}
with kp show ?case by blast
qed
@@ -140,7 +176,9 @@
lemma psize_eq_0_iff [simp]: "psize p = 0 \<longleftrightarrow> p = 0"
unfolding psize_def by simp
-lemma poly_offset: "\<exists> q. psize q = psize p \<and> (\<forall>x. poly q (x::complex) = poly p (a + x))"
+lemma poly_offset:
+ fixes p:: "('a::comm_ring_1) poly"
+ shows "\<exists> q. psize q = psize p \<and> (\<forall>x. poly q x = poly p (a + x))"
proof (intro exI conjI)
show "psize (offset_poly p a) = psize p"
unfolding psize_def
@@ -297,8 +335,9 @@
text{* Polynomial is continuous. *}
lemma poly_cont:
+ fixes p:: "('a::{comm_semiring_0,real_normed_div_algebra}) poly"
assumes ep: "e > 0"
- shows "\<exists>d >0. \<forall>w. 0 < cmod (w - z) \<and> cmod (w - z) < d \<longrightarrow> cmod (poly p w - poly p z) < e"
+ shows "\<exists>d >0. \<forall>w. 0 < norm (w - z) \<and> norm (w - z) < d \<longrightarrow> norm (poly p w - poly p z) < e"
proof-
obtain q where q: "degree q = degree p" "\<And>x. poly q x = poly p (z + x)"
proof
@@ -316,7 +355,7 @@
next
case (pCons c cs)
from poly_bound_exists[of 1 "cs"]
- obtain m where m: "m > 0" "\<And>z. cmod z \<le> 1 \<Longrightarrow> cmod (poly cs z) \<le> m" by blast
+ obtain m where m: "m > 0" "\<And>z. norm z \<le> 1 \<Longrightarrow> norm (poly cs z) \<le> m" by blast
from ep m(1) have em0: "e/m > 0" by (simp add: field_simps)
have one0: "1 > (0::real)" by arith
from real_lbound_gt_zero[OF one0 em0]
@@ -326,12 +365,12 @@
show ?case
proof(rule ex_forward[OF real_lbound_gt_zero[OF one0 em0]], clarsimp simp add: norm_mult)
fix d w
- assume H: "d > 0" "d < 1" "d < e/m" "w\<noteq>z" "cmod (w-z) < d"
- hence d1: "cmod (w-z) \<le> 1" "d \<ge> 0" by simp_all
+ assume H: "d > 0" "d < 1" "d < e/m" "w\<noteq>z" "norm (w-z) < d"
+ hence d1: "norm (w-z) \<le> 1" "d \<ge> 0" by simp_all
from H(3) m(1) have dme: "d*m < e" by (simp add: field_simps)
- from H have th: "cmod (w-z) \<le> d" by simp
+ from H have th: "norm (w-z) \<le> d" by simp
from mult_mono[OF th m(2)[OF d1(1)] d1(2) norm_ge_zero] dme
- show "cmod (w - z) * cmod (poly cs (w - z)) < e" by simp
+ show "norm (w - z) * norm (poly cs (w - z)) < e" by simp
qed
qed
qed
@@ -448,41 +487,42 @@
text {* Nonzero polynomial in z goes to infinity as z does. *}
lemma poly_infinity:
+ fixes p:: "('a::{comm_semiring_0,real_normed_div_algebra}) poly"
assumes ex: "p \<noteq> 0"
- shows "\<exists>r. \<forall>z. r \<le> cmod z \<longrightarrow> d \<le> cmod (poly (pCons a p) z)"
+ shows "\<exists>r. \<forall>z. r \<le> norm z \<longrightarrow> d \<le> norm (poly (pCons a p) z)"
using ex
proof(induct p arbitrary: a d)
case (pCons c cs a d)
{assume H: "cs \<noteq> 0"
- with pCons.hyps obtain r where r: "\<forall>z. r \<le> cmod z \<longrightarrow> d + cmod a \<le> cmod (poly (pCons c cs) z)" by blast
+ with pCons.hyps obtain r where r: "\<forall>z. r \<le> norm z \<longrightarrow> d + norm a \<le> norm (poly (pCons c cs) z)" by blast
let ?r = "1 + \<bar>r\<bar>"
- {fix z assume h: "1 + \<bar>r\<bar> \<le> cmod z"
- have r0: "r \<le> cmod z" using h by arith
+ {fix z::'a assume h: "1 + \<bar>r\<bar> \<le> norm z"
+ have r0: "r \<le> norm z" using h by arith
from r[rule_format, OF r0]
- have th0: "d + cmod a \<le> 1 * cmod(poly (pCons c cs) z)" by arith
- from h have z1: "cmod z \<ge> 1" by arith
+ have th0: "d + norm a \<le> 1 * norm(poly (pCons c cs) z)" by arith
+ from h have z1: "norm z \<ge> 1" by arith
from order_trans[OF th0 mult_right_mono[OF z1 norm_ge_zero[of "poly (pCons c cs) z"]]]
- have th1: "d \<le> cmod(z * poly (pCons c cs) z) - cmod a"
+ have th1: "d \<le> norm(z * poly (pCons c cs) z) - norm a"
unfolding norm_mult by (simp add: algebra_simps)
- from complex_mod_triangle_sub[of "z * poly (pCons c cs) z" a]
- have th2: "cmod(z * poly (pCons c cs) z) - cmod a \<le> cmod (poly (pCons a (pCons c cs)) z)"
+ from norm_diff_ineq[of "z * poly (pCons c cs) z" a]
+ have th2: "norm(z * poly (pCons c cs) z) - norm a \<le> norm (poly (pCons a (pCons c cs)) z)"
by (simp add: algebra_simps)
- from th1 th2 have "d \<le> cmod (poly (pCons a (pCons c cs)) z)" by arith}
+ from th1 th2 have "d \<le> norm (poly (pCons a (pCons c cs)) z)" by arith}
hence ?case by blast}
moreover
{assume cs0: "\<not> (cs \<noteq> 0)"
with pCons.prems have c0: "c \<noteq> 0" by simp
from cs0 have cs0': "cs = 0" by simp
- {fix z
- assume h: "(\<bar>d\<bar> + cmod a) / cmod c \<le> cmod z"
- from c0 have "cmod c > 0" by simp
- from h c0 have th0: "\<bar>d\<bar> + cmod a \<le> cmod (z*c)"
+ {fix z::'a
+ assume h: "(\<bar>d\<bar> + norm a) / norm c \<le> norm z"
+ from c0 have "norm c > 0" by simp
+ from h c0 have th0: "\<bar>d\<bar> + norm a \<le> norm (z*c)"
by (simp add: field_simps norm_mult)
have ath: "\<And>mzh mazh ma. mzh <= mazh + ma ==> abs(d) + ma <= mzh ==> d <= mazh" by arith
- from complex_mod_triangle_sub[of "z*c" a ]
- have th1: "cmod (z * c) \<le> cmod (a + z * c) + cmod a"
+ from norm_diff_ineq[of "z*c" a ]
+ have th1: "norm (z * c) \<le> norm (a + z * c) + norm a"
by (simp add: algebra_simps)
- from ath[OF th1 th0] have "d \<le> cmod (poly (pCons a (pCons c cs)) z)"
+ from ath[OF th1 th0] have "d \<le> norm (poly (pCons a (pCons c cs)) z)"
using cs0' by simp}
then have ?case by blast}
ultimately show ?case by blast
@@ -816,7 +856,7 @@
from h have "poly p x = 0" by (subst s, simp)
with pq0 have "poly q x = 0" by blast
with r xa have "poly r x = 0"
- by (auto simp add: uminus_add_conv_diff)}
+ by auto}
note impth = this
from IH[rule_format, OF dsn, of s r] impth ds0
have "s dvd (r ^ (degree s))" by blast
@@ -911,44 +951,38 @@
(* Arithmetic operations on multivariate polynomials. *)
lemma mpoly_base_conv:
- "(0::complex) \<equiv> poly 0 x" "c \<equiv> poly [:c:] x" "x \<equiv> poly [:0,1:] x" by simp_all
+ fixes x :: "'a::comm_ring_1"
+ shows "0 = poly 0 x" "c = poly [:c:] x" "x = poly [:0,1:] x"
+ by simp_all
lemma mpoly_norm_conv:
- "poly [:0:] (x::complex) \<equiv> poly 0 x" "poly [:poly 0 y:] x \<equiv> poly 0 x" by simp_all
+ fixes x :: "'a::comm_ring_1"
+ shows "poly [:0:] x = poly 0 x" "poly [:poly 0 y:] x = poly 0 x" by simp_all
lemma mpoly_sub_conv:
- "poly p (x::complex) - poly q x \<equiv> poly p x + -1 * poly q x"
+ fixes x :: "'a::comm_ring_1"
+ shows "poly p x - poly q x = poly p x + -1 * poly q x"
by simp
-lemma poly_pad_rule: "poly p x = 0 ==> poly (pCons 0 p) x = (0::complex)" by simp
+lemma poly_pad_rule: "poly p x = 0 ==> poly (pCons 0 p) x = 0" by simp
-lemma poly_cancel_eq_conv: "p = (0::complex) \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> (q = 0) \<equiv> (a * q - b * p = 0)" apply (atomize (full)) by auto
-
-lemma resolve_eq_raw: "poly 0 x \<equiv> 0" "poly [:c:] x \<equiv> (c::complex)" by auto
+lemma poly_cancel_eq_conv:
+ fixes x :: "'a::field"
+ shows "x = 0 \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> (y = 0) = (a * y - b * x = 0)"
+ by auto
lemma poly_divides_pad_rule:
- fixes p q :: "complex poly"
+ fixes p:: "('a::comm_ring_1) poly"
assumes pq: "p dvd q"
- shows "p dvd (pCons (0::complex) q)"
+shows "p dvd (pCons 0 q)"
proof-
have "pCons 0 q = q * [:0,1:]" by simp
then have "q dvd (pCons 0 q)" ..
with pq show ?thesis by (rule dvd_trans)
qed
-lemma poly_divides_pad_const_rule:
- fixes p q :: "complex poly"
- assumes pq: "p dvd q"
- shows "p dvd (smult a q)"
-proof-
- have "smult a q = q * [:a:]" by simp
- then have "q dvd smult a q" ..
- with pq show ?thesis by (rule dvd_trans)
-qed
-
-
lemma poly_divides_conv0:
- fixes p :: "complex poly"
+ fixes p:: "('a::field) poly"
assumes lgpq: "degree q < degree p" and lq:"p \<noteq> 0"
shows "p dvd q \<equiv> q = 0" (is "?lhs \<equiv> ?rhs")
proof-
@@ -969,9 +1003,10 @@
qed
lemma poly_divides_conv1:
- assumes a0: "a\<noteq> (0::complex)" and pp': "(p::complex poly) dvd p'"
+ fixes p:: "('a::field) poly"
+ assumes a0: "a\<noteq> 0" and pp': "p dvd p'"
and qrp': "smult a q - p' \<equiv> r"
- shows "p dvd q \<equiv> p dvd (r::complex poly)" (is "?lhs \<equiv> ?rhs")
+ shows "p dvd q \<equiv> p dvd r" (is "?lhs \<equiv> ?rhs")
proof-
{
from pp' obtain t where t: "p' = p * t" ..
@@ -1034,8 +1069,9 @@
thus "p dvd (q ^ n) \<longleftrightarrow> p dvd r" by simp
qed
-lemma complex_entire: "(z::complex) \<noteq> 0 \<and> w \<noteq> 0 \<equiv> z*w \<noteq> 0" by simp
-
-lemma poly_const_conv: "poly [:c:] (x::complex) = y \<longleftrightarrow> c = y" by simp
+lemma poly_const_conv:
+ fixes x :: "'a::comm_ring_1"
+ shows "poly [:c:] x = y \<longleftrightarrow> c = y" by simp
end
+
--- a/src/HOL/Lifting.thy Tue Feb 25 23:12:48 2014 +0100
+++ b/src/HOL/Lifting.thy Tue Feb 25 23:14:51 2014 +0100
@@ -296,7 +296,10 @@
shows "x = y"
using assms by (simp add: invariant_def)
-lemma fun_rel_eq_invariant:
+lemma fun_rel_eq_invariant: "(op= ===> Lifting.invariant P) = Lifting.invariant (\<lambda>f. \<forall>x. P(f x))"
+unfolding invariant_def fun_rel_def by auto
+
+lemma fun_rel_invariant_rel:
shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
by (auto simp add: invariant_def fun_rel_def)
@@ -591,6 +594,21 @@
subsection {* Domains *}
+lemma composed_equiv_rel_invariant:
+ assumes "left_unique R"
+ assumes "(R ===> op=) P P'"
+ assumes "Domainp R = P''"
+ shows "(R OO Lifting.invariant P' OO R\<inverse>\<inverse>) = Lifting.invariant (inf P'' P)"
+using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def fun_rel_def invariant_def
+fun_eq_iff by blast
+
+lemma composed_equiv_rel_eq_invariant:
+ assumes "left_unique R"
+ assumes "Domainp R = P"
+ shows "(R OO op= OO R\<inverse>\<inverse>) = Lifting.invariant P"
+using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def invariant_def
+fun_eq_iff is_equality_def by metis
+
lemma pcr_Domainp_par_left_total:
assumes "Domainp B = P"
assumes "left_total A"
--- a/src/HOL/Quotient_Examples/Lift_DList.thy Tue Feb 25 23:12:48 2014 +0100
+++ b/src/HOL/Quotient_Examples/Lift_DList.thy Tue Feb 25 23:14:51 2014 +0100
@@ -45,19 +45,7 @@
lift_definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" is List.foldr .
-lift_definition concat :: "'a dlist dlist \<Rightarrow> 'a dlist" is "remdups o List.concat"
-proof -
- {
- fix x y
- have "list_all2 cr_dlist x y \<Longrightarrow> x = List.map list_of_dlist y"
- unfolding list_all2_iff cr_dlist_def by (induction x y rule: list_induct2') auto
- }
- note cr = this
- fix x :: "'a list list" and y :: "'a list list"
- assume "(list_all2 cr_dlist OO Lifting.invariant distinct OO (list_all2 cr_dlist)\<inverse>\<inverse>) x y"
- then have "x = y" by (auto dest: cr simp add: Lifting.invariant_def)
- then show "?thesis x y" unfolding Lifting.invariant_def by auto
-qed
+lift_definition concat :: "'a dlist dlist \<Rightarrow> 'a dlist" is "remdups o List.concat" by auto
text {* We can export code: *}
--- a/src/HOL/Quotient_Examples/Lift_FSet.thy Tue Feb 25 23:12:48 2014 +0100
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy Tue Feb 25 23:14:51 2014 +0100
@@ -71,7 +71,7 @@
using Quotient_rel [OF Quotient_fset] by simp
lift_definition fconcat :: "'a fset fset \<Rightarrow> 'a fset" is concat parametric concat_transfer
-proof -
+proof (simp only: fset.pcr_cr_eq)
fix xss yss :: "'a list list"
assume "(list_all2 cr_fset OO list_eq OO (list_all2 cr_fset)\<inverse>\<inverse>) xss yss"
then obtain uss vss where
--- a/src/HOL/Tools/Lifting/lifting_def.ML Tue Feb 25 23:12:48 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Tue Feb 25 23:14:51 2014 +0100
@@ -29,7 +29,7 @@
fun mono_eq_prover ctxt prop =
let
- val rules = ((Transfer.get_relator_eq_raw ctxt) @ (Lifting_Info.get_reflexivity_rules ctxt))
+ val rules = Lifting_Info.get_reflexivity_rules ctxt
in
SOME (Goal.prove ctxt [] [] prop (K (REPEAT_ALL_NEW (resolve_tac rules) 1)))
handle ERROR _ => NONE
@@ -443,20 +443,81 @@
|> register_code_eq abs_eq_thm opt_rep_eq_thm (rty_forced, qty)
end
+local
+ val invariant_assms_tac_fixed_rules = map (Transfer.prep_transfer_domain_thm @{context})
+ [@{thm pcr_Domainp_total}, @{thm pcr_Domainp_par_left_total}, @{thm pcr_Domainp_par},
+ @{thm pcr_Domainp}]
+in
fun mk_readable_rsp_thm_eq tm lthy =
let
val ctm = cterm_of (Proof_Context.theory_of lthy) tm
+ (* This is not very cheap way of getting the rules but we have only few active
+ liftings in the current setting *)
+ fun get_cr_pcr_eqs ctxt =
+ let
+ fun collect (data : Lifting_Info.quotient) l =
+ if is_some (#pcr_info data)
+ then ((Thm.symmetric o safe_mk_meta_eq o #pcr_cr_eq o the o #pcr_info) data :: l)
+ else l
+ val table = Lifting_Info.get_quotients ctxt
+ in
+ Symtab.fold (fn (_, data) => fn l => collect data l) table []
+ end
+
+ fun assms_rewr_conv tactic rule ct =
+ let
+ fun prove_extra_assms thm =
+ let
+ val assms = cprems_of thm
+ fun finish thm = if Thm.no_prems thm then SOME (Goal.conclude thm) else NONE
+ fun prove ctm = Option.mapPartial finish (SINGLE tactic (Goal.init ctm))
+ in
+ map_interrupt prove assms
+ end
+
+ fun cconl_of thm = Drule.strip_imp_concl (cprop_of thm)
+ fun lhs_of thm = fst (Thm.dest_equals (cconl_of thm))
+ fun rhs_of thm = snd (Thm.dest_equals (cconl_of thm))
+ val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule;
+ val lhs = lhs_of rule1;
+ val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
+ val rule3 =
+ Thm.instantiate (Thm.match (lhs, ct)) rule2
+ handle Pattern.MATCH => raise CTERM ("assms_rewr_conv", [lhs, ct]);
+ val proved_assms = prove_extra_assms rule3
+ in
+ case proved_assms of
+ SOME proved_assms =>
+ let
+ val rule3 = proved_assms MRSL rule3
+ val rule4 =
+ if lhs_of rule3 aconvc ct then rule3
+ else
+ let val ceq = Thm.dest_fun2 (Thm.cprop_of rule3)
+ in rule3 COMP Thm.trivial (Thm.mk_binop ceq ct (rhs_of rule3)) end
+ in Thm.transitive rule4 (Thm.beta_conversion true (rhs_of rule4)) end
+ | NONE => Conv.no_conv ct
+ end
+
+ fun assms_rewrs_conv tactic rules = Conv.first_conv (map (assms_rewr_conv tactic) rules)
+
fun simp_arrows_conv ctm =
let
val unfold_conv = Conv.rewrs_conv
[@{thm fun_rel_eq_invariant[THEN eq_reflection]},
+ @{thm fun_rel_invariant_rel[THEN eq_reflection]},
@{thm fun_rel_eq[THEN eq_reflection]},
@{thm fun_rel_eq_rel[THEN eq_reflection]},
@{thm fun_rel_def[THEN eq_reflection]}]
fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
+ val invariant_assms_tac_rules = @{thm left_unique_composition} ::
+ invariant_assms_tac_fixed_rules @ (Transfer.get_transfer_raw lthy)
+ val invariant_assms_tac = (TRY o REPEAT_ALL_NEW (resolve_tac invariant_assms_tac_rules)
+ THEN_ALL_NEW (DETERM o Transfer.eq_tac lthy)) 1
val invariant_commute_conv = Conv.bottom_conv
- (K (Conv.try_conv (Conv.rewrs_conv (Lifting_Info.get_invariant_commute_rules lthy)))) lthy
+ (K (Conv.try_conv (assms_rewrs_conv invariant_assms_tac
+ (Lifting_Info.get_invariant_commute_rules lthy)))) lthy
val relator_eq_conv = Conv.bottom_conv
(K (Conv.try_conv (Conv.rewrs_conv (Transfer.get_relator_eq lthy)))) lthy
in
@@ -467,8 +528,9 @@
end
val unfold_ret_val_invs = Conv.bottom_conv
- (K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy
- val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv simp_arrows_conv)
+ (K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy
+ val cr_to_pcr_conv = Raw_Simplifier.rewrite lthy false (get_cr_pcr_eqs lthy)
+ val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv (cr_to_pcr_conv then_conv simp_arrows_conv))
val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
val beta_conv = Thm.beta_conversion true
@@ -477,6 +539,7 @@
in
Object_Logic.rulify lthy (eq_thm RS Drule.equal_elim_rule2)
end
+end
fun rename_to_tnames ctxt term =
let
--- a/src/HOL/Tools/Lifting/lifting_info.ML Tue Feb 25 23:12:48 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Tue Feb 25 23:14:51 2014 +0100
@@ -516,6 +516,11 @@
#> relfexivity_rule_setup
#> relator_distr_attribute_setup
+(* setup fixed invariant rules *)
+
+val _ = Context.>> (fold (Invariant_Commute.add_thm o Transfer.prep_transfer_domain_thm @{context})
+ [@{thm composed_equiv_rel_invariant}, @{thm composed_equiv_rel_eq_invariant}])
+
(* outer syntax commands *)
val _ =
--- a/src/HOL/Tools/Lifting/lifting_term.ML Tue Feb 25 23:12:48 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_term.ML Tue Feb 25 23:14:51 2014 +0100
@@ -447,16 +447,6 @@
end
fun rewrs_imp rules = first_imp (map rewr_imp rules)
-
- fun map_interrupt f l =
- let
- fun map_interrupt' _ [] l = SOME (rev l)
- | map_interrupt' f (x::xs) l = (case f x of
- NONE => NONE
- | SOME v => map_interrupt' f xs (v::l))
- in
- map_interrupt' f l []
- end
in
(*
--- a/src/HOL/Tools/Lifting/lifting_util.ML Tue Feb 25 23:12:48 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_util.ML Tue Feb 25 23:14:51 2014 +0100
@@ -31,6 +31,7 @@
val relation_types: typ -> typ * typ
val mk_HOL_eq: thm -> thm
val safe_HOL_meta_eq: thm -> thm
+ val map_interrupt: ('a -> 'b option) -> 'a list -> 'b list option
end
@@ -121,4 +122,14 @@
fun safe_HOL_meta_eq r = mk_HOL_eq r handle Thm.THM _ => r
+fun map_interrupt f l =
+ let
+ fun map_interrupt' _ [] l = SOME (rev l)
+ | map_interrupt' f (x::xs) l = (case f x of
+ NONE => NONE
+ | SOME v => map_interrupt' f xs (v::l))
+ in
+ map_interrupt' f l []
+ end
+
end
--- a/src/HOL/Tools/transfer.ML Tue Feb 25 23:12:48 2014 +0100
+++ b/src/HOL/Tools/transfer.ML Tue Feb 25 23:14:51 2014 +0100
@@ -25,10 +25,13 @@
val transfer_raw_del: thm -> Context.generic -> Context.generic
val transferred_attribute: thm list -> attribute
val untransferred_attribute: thm list -> attribute
+ val prep_transfer_domain_thm: Proof.context -> thm -> thm
val transfer_domain_add: attribute
val transfer_domain_del: attribute
val transfer_rule_of_term: Proof.context -> bool -> term -> thm
val transfer_rule_of_lhs: Proof.context -> term -> thm
+ val eq_tac: Proof.context -> int -> tactic
+ val transfer_step_tac: Proof.context -> int -> tactic
val transfer_tac: bool -> Proof.context -> int -> tactic
val transfer_prover_tac: Proof.context -> int -> tactic
val gen_frees_tac: (string * typ) list -> Proof.context -> int -> tactic
@@ -346,11 +349,14 @@
(** Adding transfer domain rules **)
-fun add_transfer_domain_thm thm ctxt =
- (add_transfer_thm o abstract_equalities_domain (Context.proof_of ctxt) o detect_transfer_rules) thm ctxt
+fun prep_transfer_domain_thm ctxt thm =
+ (abstract_equalities_domain ctxt o detect_transfer_rules) thm
-fun del_transfer_domain_thm thm ctxt =
- (del_transfer_thm o abstract_equalities_domain (Context.proof_of ctxt) o detect_transfer_rules) thm ctxt
+fun add_transfer_domain_thm thm ctxt = (add_transfer_thm o
+ prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt
+
+fun del_transfer_domain_thm thm ctxt = (del_transfer_thm o
+ prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt
(** Transfer proof method **)
@@ -571,7 +577,13 @@
|> Thm.instantiate (map tinst binsts, map inst binsts)
end
-fun eq_tac eq_rules = TRY o REPEAT_ALL_NEW (resolve_tac eq_rules) THEN_ALL_NEW rtac @{thm is_equality_eq}
+fun eq_rules_tac eq_rules = TRY o REPEAT_ALL_NEW (resolve_tac eq_rules)
+ THEN_ALL_NEW rtac @{thm is_equality_eq}
+
+fun eq_tac ctxt = eq_rules_tac (get_relator_eq_raw ctxt)
+
+fun transfer_step_tac ctxt = (REPEAT_ALL_NEW (resolve_tac (get_transfer_raw ctxt))
+ THEN_ALL_NEW (DETERM o eq_rules_tac (get_relator_eq_raw ctxt)))
fun transfer_tac equiv ctxt i =
let
@@ -587,7 +599,7 @@
rtac start_rule i THEN
(rtac (transfer_rule_of_term ctxt equiv (HOLogic.dest_Trueprop t))
THEN_ALL_NEW
- (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_tac eq_rules))
+ (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules))
ORELSE' end_tac)) (i + 1)
handle TERM (_, ts) => raise TERM (err_msg, ts)
in
@@ -612,7 +624,7 @@
rtac @{thm transfer_prover_start} i,
((rtac rule1 ORELSE' (CONVERSION expand_eq_in_rel THEN' rtac rule1))
THEN_ALL_NEW
- (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_tac eq_rules))) (i+1),
+ (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules))) (i+1),
rtac @{thm refl} i]
end)
@@ -640,7 +652,7 @@
(rtac rule
THEN_ALL_NEW
(SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)
- THEN_ALL_NEW (DETERM o eq_tac eq_rules)))) 1
+ THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1
handle TERM (_, ts) => raise TERM (err_msg, ts)
val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
val tnames = map (fst o dest_TFree o snd) instT
@@ -676,7 +688,7 @@
(rtac rule
THEN_ALL_NEW
(SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)
- THEN_ALL_NEW (DETERM o eq_tac eq_rules)))) 1
+ THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1
handle TERM (_, ts) => raise TERM (err_msg, ts)
val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
val tnames = map (fst o dest_TFree o snd) instT
--- a/src/HOL/Topological_Spaces.thy Tue Feb 25 23:12:48 2014 +0100
+++ b/src/HOL/Topological_Spaces.thy Tue Feb 25 23:14:51 2014 +0100
@@ -1706,6 +1706,11 @@
unfolding continuous_on_open_invariant
by (metis open_Int Int_absorb Int_commute[of s] Int_assoc[of _ _ s])
+corollary continuous_imp_open_vimage:
+ assumes "continuous_on s f" "open s" "open B" "f -` B \<subseteq> s"
+ shows "open (f -` B)"
+by (metis assms continuous_on_open_vimage le_iff_inf)
+
lemma continuous_on_closed_invariant:
"continuous_on s f \<longleftrightarrow> (\<forall>B. closed B \<longrightarrow> (\<exists>A. closed A \<and> A \<inter> s = f -` B \<inter> s))"
proof -
--- a/src/HOL/Transcendental.thy Tue Feb 25 23:12:48 2014 +0100
+++ b/src/HOL/Transcendental.thy Tue Feb 25 23:14:51 2014 +0100
@@ -52,6 +52,12 @@
finally show ?case .
qed
+corollary power_diff_sumr2: --{*COMPLEX_POLYFUN in HOL Light*}
+ fixes x :: "'a::{comm_ring,monoid_mult}"
+ shows "x^n - y^n = (x - y) * (\<Sum>i=0..<n. y^(n - Suc i) * x^i)"
+using lemma_realpow_diff_sumr2[of x "n - 1" y]
+by (cases "n = 0") (simp_all add: field_simps)
+
lemma lemma_realpow_rev_sumr:
"(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) =
(\<Sum>p=0..<Suc n. (x ^ (n - p)) * (y ^ p))"