--- a/src/HOL/Deriv.thy Fri Mar 07 20:46:27 2014 +0100
+++ b/src/HOL/Deriv.thy Fri Mar 07 20:50:02 2014 +0100
@@ -389,11 +389,29 @@
lemma FDERIV_divide[simp, FDERIV_intros]:
fixes f :: "_ \<Rightarrow> 'a::real_normed_div_algebra"
- assumes g: "FDERIV g x : s :> g'"
- assumes x: "f x \<noteq> 0" and f: "FDERIV f x : s :> f'"
- shows "FDERIV (\<lambda>x. g x / f x) x : s :> (\<lambda>h. - g x * (inverse (f x) * f' h * inverse (f x)) + g' h / f x)"
- using FDERIV_mult[OF g FDERIV_inverse[OF x f]]
- by (simp add: divide_inverse)
+ assumes f: "FDERIV f x : s :> f'" and g: "FDERIV g x : s :> g'"
+ assumes x: "g x \<noteq> 0"
+ shows "FDERIV (\<lambda>x. f x / g x) x : s :>
+ (\<lambda>h. - f x * (inverse (g x) * g' h * inverse (g x)) + f' h / g x)"
+ using FDERIV_mult[OF f FDERIV_inverse[OF x g]]
+ by (simp add: divide_inverse field_simps)
+
+text{*Conventional form requires mult-AC laws. Types real and complex only.*}
+lemma FDERIV_divide'[FDERIV_intros]:
+ fixes f :: "_ \<Rightarrow> 'a::real_normed_field"
+ assumes f: "FDERIV f x : s :> f'" and g: "FDERIV g x : s :> g'" and x: "g x \<noteq> 0"
+ shows "FDERIV (\<lambda>x. f x / g x) x : s :>
+ (\<lambda>h. (f' h * g x - f x * g' h) / (g x * g x))"
+proof -
+ { fix h
+ have "f' h / g x - f x * (inverse (g x) * g' h * inverse (g x)) =
+ (f' h * g x - f x * g' h) / (g x * g x)"
+ by (simp add: divide_inverse field_simps nonzero_inverse_mult_distrib x)
+ }
+ then show ?thesis
+ using FDERIV_divide [OF f g] x
+ by simp
+qed
subsection {* Uniqueness *}
@@ -605,6 +623,10 @@
"DERIV f x : s :> D ==> DERIV (%x. c * f x) x : s :> c*D"
by (drule DERIV_mult' [OF DERIV_const], simp)
+lemma DERIV_cmult_right:
+ "DERIV f x : s :> D ==> DERIV (%x. f x * c) x : s :> D * c"
+ using DERIV_cmult by (force simp add: mult_ac)
+
lemma DERIV_cmult_Id [simp]: "DERIV (op * c) x : s :> c"
by (cut_tac c = c and x = x in DERIV_ident [THEN DERIV_cmult], simp)
@@ -674,13 +696,33 @@
using FDERIV_compose[of f "\<lambda>x. x * D" x s g "\<lambda>x. x * E"]
by (auto simp: deriv_fderiv ac_simps dest: FDERIV_subset)
+corollary DERIV_chain2: "DERIV f (g x) :> Da \<Longrightarrow> DERIV g x : s :> Db \<Longrightarrow> DERIV (%x. f (g x)) x : s :> Da * Db"
+ by (rule DERIV_chain')
+
text {* Standard version *}
lemma DERIV_chain: "DERIV f (g x) :> Da \<Longrightarrow> DERIV g x : s :> Db \<Longrightarrow> DERIV (f o g) x : s :> Da * Db"
by (drule (1) DERIV_chain', simp add: o_def mult_commute)
-lemma DERIV_chain2: "DERIV f (g x) :> Da \<Longrightarrow> DERIV g x : s :> Db \<Longrightarrow> DERIV (%x. f (g x)) x : s :> Da * Db"
- by (auto dest: DERIV_chain simp add: o_def)
+lemma DERIV_image_chain:
+ "DERIV f (g x) : (g ` s) :> Da \<Longrightarrow> DERIV g x : s :> Db \<Longrightarrow> DERIV (f o g) x : s :> Da * Db"
+ using FDERIV_in_compose [of g "\<lambda>x. x * Db" x s f "\<lambda>x. x * Da "]
+ by (simp add: deriv_fderiv o_def mult_ac)
+
+(*These two are from HOL Light: HAS_COMPLEX_DERIVATIVE_CHAIN*)
+lemma DERIV_chain_s:
+ assumes "(\<And>x. x \<in> s \<Longrightarrow> DERIV g x :> g'(x))"
+ and "DERIV f x :> f'"
+ and "f x \<in> s"
+ shows "DERIV (\<lambda>x. g(f x)) x :> f' * g'(f x)"
+ by (metis (full_types) DERIV_chain' mult_commute assms)
+
+lemma DERIV_chain3: (*HAS_COMPLEX_DERIVATIVE_CHAIN_UNIV*)
+ assumes "(\<And>x. DERIV g x :> g'(x))"
+ and "DERIV f x :> f'"
+ shows "DERIV (\<lambda>x. g(f x)) x :> f' * g'(f x)"
+ by (metis UNIV_I DERIV_chain_s [of UNIV] assms)
+
subsubsection {* @{text "DERIV_intros"} *}
@@ -748,7 +790,7 @@
text {* Caratheodory formulation of derivative at a point *}
-lemma CARAT_DERIV:
+lemma CARAT_DERIV: (*FIXME: SUPERSEDED BY THE ONE IN Deriv.thy. But still used by NSA/HDeriv.thy*)
"(DERIV f x :> l) \<longleftrightarrow> (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> isCont g x \<and> g x = l)"
(is "?lhs = ?rhs")
proof
--- a/src/HOL/Fun_Def.thy Fri Mar 07 20:46:27 2014 +0100
+++ b/src/HOL/Fun_Def.thy Fri Mar 07 20:50:02 2014 +0100
@@ -83,7 +83,6 @@
by (simp add: wfP_def)
ML_file "Tools/Function/function_core.ML"
-ML_file "Tools/Function/sum_tree.ML"
ML_file "Tools/Function/mutual.ML"
ML_file "Tools/Function/pattern_split.ML"
ML_file "Tools/Function/relation.ML"
--- a/src/HOL/Fun_Def_Base.thy Fri Mar 07 20:46:27 2014 +0100
+++ b/src/HOL/Fun_Def_Base.thy Fri Mar 07 20:50:02 2014 +0100
@@ -12,5 +12,6 @@
ML_file "Tools/Function/function_common.ML"
ML_file "Tools/Function/context_tree.ML"
setup Function_Ctx_Tree.setup
+ML_file "Tools/Function/sum_tree.ML"
end
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Fri Mar 07 20:46:27 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Fri Mar 07 20:50:02 2014 +0100
@@ -142,6 +142,48 @@
by (simp add: bounded_linear_mult_right has_derivative_within)
qed
+subsubsection {*Caratheodory characterization*}
+
+lemma DERIV_within_iff:
+ "(DERIV f a : s :> D) \<longleftrightarrow> ((\<lambda>z. (f z - f a) / (z - a)) ---> D) (at a within s)"
+proof -
+ have 1: "\<And>w y. ~(w = a) ==> y / (w - a) - D = (y - (w - a)*D)/(w - a)"
+ by (metis divide_diff_eq_iff eq_iff_diff_eq_0)
+ show ?thesis
+ apply (simp add: deriv_fderiv has_derivative_within bounded_linear_mult_left)
+ apply (simp add: LIM_zero_iff [where l = D, symmetric])
+ apply (simp add: Lim_within dist_norm)
+ apply (simp add: nonzero_norm_divide [symmetric])
+ apply (simp add: 1 diff_add_eq_diff_diff)
+ done
+qed
+
+lemma DERIV_caratheodory_within:
+ "(DERIV f x : s :> l) \<longleftrightarrow>
+ (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> continuous (at x within s) g \<and> g x = l)"
+ (is "?lhs = ?rhs")
+proof
+ assume der: "DERIV f x : s :> l"
+ show ?rhs
+ proof (intro exI conjI)
+ let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
+ show "\<forall>z. f z - f x = ?g z * (z-x)" by simp
+ show "continuous (at x within s) ?g" using der
+ by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
+ show "?g x = l" by simp
+ qed
+next
+ assume ?rhs
+ then obtain g where
+ "(\<forall>z. f z - f x = g z * (z-x))" and "continuous (at x within s) g" and "g x = l" by blast
+ thus "(DERIV f x : s :> l)"
+ by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
+qed
+
+lemma CARAT_DERIV: (*FIXME: REPLACES THE ONE IN Deriv.thy*)
+ "(DERIV f x :> l) \<longleftrightarrow> (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> isCont g x \<and> g x = l)"
+by (rule DERIV_caratheodory_within)
+
subsubsection {* Limit transformation for derivatives *}
@@ -151,20 +193,10 @@
and "\<forall>x'\<in>s. dist x' x < d \<longrightarrow> f x' = g x'"
and "(f has_derivative f') (at x within s)"
shows "(g has_derivative f') (at x within s)"
- using assms(4)
+ using assms
unfolding has_derivative_within
- apply -
- apply (erule conjE)
- apply rule
- apply assumption
- apply (rule Lim_transform_within[OF assms(1)])
- defer
- apply assumption
- apply rule
- apply rule
- apply (drule assms(3)[rule_format])
- using assms(3)[rule_format, OF assms(2)]
- apply auto
+ apply clarify
+ apply (rule Lim_transform_within, auto)
done
lemma has_derivative_transform_at:
@@ -181,20 +213,10 @@
and "\<forall>y\<in>s. f y = g y"
and "(f has_derivative f') (at x)"
shows "(g has_derivative f') (at x)"
- using assms(4)
+ using assms
unfolding has_derivative_at
- apply -
- apply (erule conjE)
- apply rule
- apply assumption
- apply (rule Lim_transform_within_open[OF assms(1,2)])
- defer
- apply assumption
- apply rule
- apply rule
- apply (drule assms(3)[rule_format])
- using assms(3)[rule_format, OF assms(2)]
- apply auto
+ apply clarify
+ apply (rule Lim_transform_within_open[OF assms(1,2)], auto)
done
subsection {* Differentiability *}
@@ -275,17 +297,11 @@
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
shows "(f ---> 0) (at a within s) \<Longrightarrow> ((\<lambda>x. norm(x - a) *\<^sub>R f x) ---> 0) (at a within s)"
unfolding Lim_within
- apply rule
- apply rule
+ apply (auto simp: )
apply (erule_tac x=e in allE)
- apply (erule impE)
- apply assumption
- apply (erule exE)
- apply (erule conjE)
+ apply (auto simp: )
apply (rule_tac x="min d 1" in exI)
- apply rule
- defer
- apply rule
+ apply (auto simp: )
apply (erule_tac x=x in ballE)
unfolding dist_norm diff_0_right
apply (auto intro!: mult_strict_mono[of _ "1::real", unfolded mult_1_left])
@@ -334,24 +350,12 @@
proof
assume ?lhs
then show ?rhs
- unfolding has_derivative_within
- apply -
- apply (erule conjE)
- apply rule
- apply assumption
- unfolding Lim_within
- apply rule
+ unfolding has_derivative_within Lim_within
+ apply clarify
apply (erule_tac x=e in allE)
- apply rule
- apply (erule impE)
- apply assumption
- apply (erule exE)
+ apply safe
apply (rule_tac x=d in exI)
- apply (erule conjE)
- apply rule
- apply assumption
- apply rule
- apply rule
+ apply clarify
proof-
fix x y e d
assume as:
@@ -384,39 +388,14 @@
next
assume ?rhs
then show ?lhs
- unfolding has_derivative_within Lim_within
- apply -
- apply (erule conjE)
- apply rule
- apply assumption
- apply rule
- apply (erule_tac x="e/2" in allE)
- apply rule
- apply (erule impE)
- defer
- apply (erule exE)
- apply (rule_tac x=d in exI)
- apply (erule conjE)
- apply rule
- apply assumption
- apply rule
- apply rule
+ apply (auto simp: has_derivative_within Lim_within)
+ apply (erule_tac x="e/2" in allE, auto)
+ apply (rule_tac x=d in exI, auto)
unfolding dist_norm diff_0_right norm_scaleR
- apply (erule_tac x=xa in ballE)
- apply (erule impE)
- proof -
- fix e d y
- assume "bounded_linear f'"
- and "0 < e"
- and "0 < d"
- and "y \<in> s"
- and "0 < norm (y - x) \<and> norm (y - x) < d"
- and "norm (f y - f x - f' (y - x)) \<le> e / 2 * norm (y - x)"
- then show "\<bar>1 / norm (y - x)\<bar> * norm (f y - (f x + f' (y - x))) < e"
- apply (rule_tac le_less_trans[of _ "e/2"])
- apply (auto intro!: mult_imp_div_pos_le simp add: algebra_simps)
- done
- qed auto
+ apply (erule_tac x=xa in ballE, auto)
+ apply (rule_tac y="e/2" in le_less_trans)
+ apply (auto intro!: mult_imp_div_pos_le simp add: algebra_simps)
+ done
qed
lemma has_derivative_at_alt:
@@ -488,11 +467,8 @@
done
qed
then have *: "netlimit (at x within s) = x"
- apply -
- apply (rule netlimit_within)
- unfolding trivial_limit_within
- apply simp
- done
+ apply (auto intro!: netlimit_within)
+ by (metis trivial_limit_within)
show ?thesis
apply (rule linear_eq_stdbasis)
unfolding linear_conv_bounded_linear
@@ -621,13 +597,8 @@
and "x \<in> {a..b}"
and "(f has_derivative f') (at x within {a..b})"
shows "frechet_derivative f (at x within {a..b}) = f'"
- apply (rule frechet_derivative_unique_within_closed_interval[where f=f])
- apply (rule assms(1,2))+
- unfolding frechet_derivative_works[symmetric]
- unfolding differentiable_def
- using assms(3)
- apply auto
- done
+ using assms
+ by (metis Derivative.differentiableI frechet_derivative_unique_within_closed_interval frechet_derivative_works)
subsection {* The traditional Rolle theorem in one dimension *}
@@ -778,12 +749,7 @@
proof (cases "d \<in> box a b \<or> c \<in> box a b")
case True
then show ?thesis
- apply (erule_tac disjE)
- apply (rule_tac x=d in bexI)
- apply (rule_tac[3] x=c in bexI)
- using d c
- apply (auto simp: box_real)
- done
+ by (metis c(2) d(2) interval_open_subset_closed subset_iff)
next
def e \<equiv> "(a + b) /2"
case False
@@ -791,10 +757,7 @@
using d c assms(2) by (auto simp: box_real)
then have "\<And>x. x \<in> {a..b} \<Longrightarrow> f x = f d"
using c d
- apply -
- apply (erule_tac x=x in ballE)+
- apply auto
- done
+ by force
then show ?thesis
apply (rule_tac x=e in bexI)
unfolding e_def
@@ -806,23 +769,11 @@
then obtain x where x: "x \<in> box a b" "(\<forall>y\<in>box a b. f x \<le> f y) \<or> (\<forall>y\<in>box a b. f y \<le> f x)" ..
then have "f' x = (\<lambda>v. 0)"
apply (rule_tac differential_zero_maxmin[of x "box a b" f "f' x"])
- defer
- apply (rule open_interval)
- apply (rule assms(4)[unfolded has_derivative_at[symmetric],THEN bspec[where x=x]])
- apply assumption
- unfolding o_def
- apply (erule disjE)
- apply (rule disjI2)
+ using assms
apply auto
done
then show ?thesis
- apply (rule_tac x=x in bexI)
- unfolding o_def
- apply rule
- apply (drule_tac x=v in fun_cong)
- using x(1)
- apply auto
- done
+ by (metis x(1))
qed
@@ -847,10 +798,7 @@
"x \<in> box a b"
"(\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)" ..
then show ?thesis
- apply (rule_tac x=x in bexI)
- apply (drule fun_cong[of _ _ "b - a"])
- apply (auto simp: box_real)
- done
+ by (metis (erased, hide_lams) assms(1) box_real diff_less_iff(1) eq_iff_diff_eq_0 linordered_field_class.sign_simps(41) nonzero_mult_divide_cancel_right not_real_square_gt_zero times_divide_eq_left)
qed
lemma mvt_simple:
@@ -1196,11 +1144,7 @@
proof -
case goal1
then have *: "e / B >0"
- apply -
- apply (rule divide_pos_pos)
- using `B > 0`
- apply auto
- done
+ by (metis `0 < B` divide_pos_pos)
obtain d' where d':
"0 < d'"
"\<forall>z. norm (z - y) < d' \<longrightarrow> norm (g z - g y - g' (z - y)) \<le> e / B * norm (g z - g y)"
@@ -1209,10 +1153,7 @@
using real_lbound_gt_zero[OF d(1) d'(1)] by blast
show ?case
apply (rule_tac x=k in exI)
- apply rule
- defer
- apply rule
- apply rule
+ apply auto
proof -
fix z
assume as: "norm (z - y) < k"
@@ -1296,9 +1237,7 @@
apply (rule continuous_on_interior[OF _ assms(3)])
apply (rule continuous_on_inv[OF assms(4,1)])
apply (rule assms(2,5) assms(5)[rule_format] open_interior assms(3))+
- apply rule
- apply (rule *)
- apply assumption
+ apply (metis *)
done
qed
@@ -1554,9 +1493,7 @@
using linear_inverse_left
by auto
moreover have *:"\<forall>t\<subseteq>s. x \<in> interior t \<longrightarrow> f x \<in> interior (f ` t)"
- apply rule
- apply rule
- apply rule
+ apply clarify
apply (rule sussmann_open_mapping)
apply (rule assms ling)+
apply auto
@@ -1604,12 +1541,8 @@
then show ?case
using assms(4) by auto
qed
- ultimately show ?thesis
- apply -
- apply (rule has_derivative_inverse_basic_x[OF assms(5)])
- using assms
- apply auto
- done
+ ultimately show ?thesis using assms
+ by (metis has_derivative_inverse_basic_x open_interior)
qed
text {* A rewrite based on the other domain. *}
@@ -2078,10 +2011,7 @@
show ?thesis
apply (rule *)
apply (rule has_derivative_sequence[OF assms(1) _ assms(3), of "\<lambda>n x. f n x + (f 0 a - f n a)"])
- apply rule
- apply rule
- apply (rule has_derivative_add_const, rule assms(2)[rule_format])
- apply assumption
+ apply (metis assms(2) has_derivative_add_const)
apply (rule `a \<in> s`)
apply auto
done
@@ -2097,11 +2027,7 @@
have *: "\<forall>n. \<exists>f f'. \<forall>x\<in>s.
(f has_derivative (f' x)) (at x within s) \<and>
(\<forall>h. norm(f' x h - g' x h) \<le> inverse (real (Suc n)) * norm h)"
- apply rule
- using assms(2)
- apply (erule_tac x="inverse (real (Suc n))" in allE)
- apply auto
- done
+ by (metis assms(2) inverse_positive_iff_positive real_of_nat_Suc_gt_zero)
obtain f where
*: "\<forall>x. \<exists>f'. \<forall>xa\<in>s. FDERIV (f x) xa : s :> f' xa \<and>
(\<forall>h. norm (f' xa h - g' xa h) \<le> inverse (real (Suc x)) * norm h)"
@@ -2157,11 +2083,7 @@
shows "\<exists>g. \<forall>x\<in>s. ((\<lambda>n. f n x) sums_seq (g x)) k \<and> (g has_derivative g' x) (at x within s)"
unfolding sums_seq_def
apply (rule has_derivative_sequence[OF assms(1) _ assms(3)])
- apply rule
- apply rule
- apply (rule has_derivative_setsum)
- apply (rule assms(2)[rule_format])
- apply assumption
+ apply (metis assms(2) has_derivative_setsum)
using assms(4-5)
unfolding sums_seq_def
apply auto
@@ -2296,10 +2218,9 @@
lemma has_vector_derivative_cmul_eq:
assumes "c \<noteq> 0"
shows "(((\<lambda>x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net \<longleftrightarrow> (f has_vector_derivative f') net)"
- apply rule
+ apply (rule iffI)
apply (drule has_vector_derivative_cmul[where c="1/c"])
- defer
- apply (rule has_vector_derivative_cmul)
+ apply (rule_tac [2] has_vector_derivative_cmul)
using assms
apply auto
done
--- a/src/HOL/NthRoot.thy Fri Mar 07 20:46:27 2014 +0100
+++ b/src/HOL/NthRoot.thy Fri Mar 07 20:50:02 2014 +0100
@@ -534,14 +534,35 @@
subsection {* Square Root of Sum of Squares *}
-lemma real_sqrt_sum_squares_ge_zero: "0 \<le> sqrt (x\<^sup>2 + y\<^sup>2)"
- by simp (* TODO: delete *)
+lemma sum_squares_bound:
+ fixes x:: "'a::linordered_field"
+ shows "2*x*y \<le> x^2 + y^2"
+proof -
+ have "(x-y)^2 = x*x - 2*x*y + y*y"
+ by algebra
+ then have "0 \<le> x^2 - 2*x*y + y^2"
+ by (metis sum_power2_ge_zero zero_le_double_add_iff_zero_le_single_add power2_eq_square)
+ then show ?thesis
+ by arith
+qed
-declare real_sqrt_sum_squares_ge_zero [THEN abs_of_nonneg, simp]
+lemma arith_geo_mean:
+ fixes u:: "'a::linordered_field" assumes "u\<^sup>2 = x*y" "x\<ge>0" "y\<ge>0" shows "u \<le> (x + y)/2"
+ apply (rule power2_le_imp_le)
+ using sum_squares_bound assms
+ apply (auto simp: zero_le_mult_iff)
+ by (auto simp: algebra_simps power2_eq_square)
+
+lemma arith_geo_mean_sqrt:
+ fixes x::real assumes "x\<ge>0" "y\<ge>0" shows "sqrt(x*y) \<le> (x + y)/2"
+ apply (rule arith_geo_mean)
+ using assms
+ apply (auto simp: zero_le_mult_iff)
+ done
lemma real_sqrt_sum_squares_mult_ge_zero [simp]:
"0 \<le> sqrt ((x\<^sup>2 + y\<^sup>2)*(xa\<^sup>2 + ya\<^sup>2))"
- by (simp add: zero_le_mult_iff)
+ by (metis real_sqrt_ge_0_iff split_mult_pos_le sum_power2_ge_zero)
lemma real_sqrt_sum_squares_mult_squared_eq [simp]:
"(sqrt ((x\<^sup>2 + y\<^sup>2) * (xa\<^sup>2 + ya\<^sup>2)))\<^sup>2 = (x\<^sup>2 + y\<^sup>2) * (xa\<^sup>2 + ya\<^sup>2)"
--- a/src/HOL/String.thy Fri Mar 07 20:46:27 2014 +0100
+++ b/src/HOL/String.thy Fri Mar 07 20:50:02 2014 +0100
@@ -3,7 +3,7 @@
header {* Character and string types *}
theory String
-imports List Enum
+imports Enum
begin
subsection {* Characters and strings *}
@@ -443,4 +443,3 @@
hide_type (open) literal
end
-
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Mar 07 20:46:27 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Mar 07 20:50:02 2014 +0100
@@ -478,8 +478,8 @@
define_co_rec Least_FP fpT Cs (mk_binding recN)
(fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_rec,
map4 (fn ctor_rec_absT => fn rep => fn fs => fn xsss =>
- mk_case_absumprod ctor_rec_absT rep fs
- (map (mk_tuple_balanced o map HOLogic.mk_tuple) xsss) (map flat_rec_arg_args xsss))
+ mk_case_absumprod ctor_rec_absT rep fs (map (map HOLogic.mk_tuple) xsss)
+ (map flat_rec_arg_args xsss))
ctor_rec_absTs reps fss xssss)))
end;
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Mar 07 20:46:27 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Mar 07 20:50:02 2014 +0100
@@ -128,6 +128,7 @@
val split_conj_prems: int -> thm -> thm
val mk_sumTN: typ list -> typ
+ val mk_tupleT_balanced: typ list -> typ
val mk_sumprodT_balanced: typ list list -> typ
val mk_proj: typ -> int -> int -> term
@@ -136,14 +137,15 @@
val Inl_const: typ -> typ -> term
val Inr_const: typ -> typ -> term
+ val mk_tuple_balanced: term list -> term
+ val mk_tuple1_balanced: typ list -> term list -> term
val mk_case_sum: term * term -> term
val mk_case_sumN: term list -> term
- val mk_case_absumprod: typ -> term -> term list -> term list -> term list list -> term
+ val mk_case_absumprod: typ -> term -> term list -> term list list -> term list list -> term
val mk_Inl: typ -> term -> term
val mk_Inr: typ -> term -> term
- val mk_tuple_balanced: term list -> term
val mk_absumprod: typ -> term -> int -> int -> term list -> term
val dest_sumT: typ -> typ * typ
@@ -374,35 +376,24 @@
fun Inr_const LT RT = Const (@{const_name Inr}, RT --> mk_sumT (LT, RT));
fun mk_Inr LT t = Inr_const LT (fastype_of t) $ t;
-(* FIXME: reuse "mk_inj" in function package *)
-fun mk_InN_balanced sum_T n t k =
- let
- fun repair_types T (Const (s as @{const_name Inl}, _) $ t) = repair_inj_types T s fst t
- | repair_types T (Const (s as @{const_name Inr}, _) $ t) = repair_inj_types T s snd t
- | repair_types _ t = t
- and repair_inj_types T s get t =
- let val T' = get (dest_sumT T) in
- Const (s, T' --> T) $ repair_types T' t
- end;
- in
- Balanced_Tree.access {left = mk_Inl dummyT, right = mk_Inr dummyT, init = t} n k
- |> repair_types sum_T
- end;
+fun mk_prod1 bound_Ts (t, u) =
+ HOLogic.pair_const (fastype_of1 (bound_Ts, t)) (fastype_of1 (bound_Ts, u)) $ t $ u;
-fun mk_tuple_balanced [] = HOLogic.unit
- | mk_tuple_balanced ts = Balanced_Tree.make HOLogic.mk_prod ts;
+fun mk_tuple1_balanced _ [] = HOLogic.unit
+ | mk_tuple1_balanced bound_Ts ts = Balanced_Tree.make (mk_prod1 bound_Ts) ts;
+
+val mk_tuple_balanced = mk_tuple1_balanced [];
fun mk_absumprod absT abs0 n k ts =
let val abs = mk_abs absT abs0;
- in abs $ mk_InN_balanced (domain_type (fastype_of abs)) n (mk_tuple_balanced ts) k end;
+ in abs $ Sum_Tree.mk_inj (domain_type (fastype_of abs)) n k (mk_tuple_balanced ts) end;
fun mk_case_sum (f, g) =
let
- val fT = fastype_of f;
- val gT = fastype_of g;
+ val (fT, T') = dest_funT (fastype_of f);
+ val (gT, _) = dest_funT (fastype_of g);
in
- Const (@{const_name case_sum},
- fT --> gT --> mk_sumT (domain_type fT, domain_type gT) --> range_type fT) $ f $ g
+ Sum_Tree.mk_sumcase fT gT T' f g
end;
val mk_case_sumN = Library.foldr1 mk_case_sum;
@@ -411,8 +402,9 @@
fun mk_tupled_fun f x xs =
if xs = [x] then f else HOLogic.tupled_lambda x (Term.list_comb (f, xs));
-fun mk_case_absumprod absT rep fs xs xss =
- HOLogic.mk_comp (mk_case_sumN_balanced (map3 mk_tupled_fun fs xs xss), mk_rep absT rep);
+fun mk_case_absumprod absT rep fs xss xss' =
+ HOLogic.mk_comp (mk_case_sumN_balanced (map3 mk_tupled_fun fs (map mk_tuple_balanced xss) xss'),
+ mk_rep absT rep);
fun If_const T = Const (@{const_name If}, HOLogic.boolT --> T --> T --> T);
fun mk_If p t f = let val T = fastype_of t in If_const T $ p $ t $ f end;
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Mar 07 20:46:27 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Mar 07 20:50:02 2014 +0100
@@ -477,7 +477,7 @@
val undef_const = Const (@{const_name undefined}, dummyT);
-val abs_tuple = HOLogic.tupled_lambda o HOLogic.mk_tuple;
+val abs_tuple_balanced = HOLogic.tupled_lambda o mk_tuple_balanced;
fun abstract vs =
let
@@ -489,10 +489,6 @@
end;
in abs 0 end;
-fun mk_prod1 bound_Ts (t, u) =
- HOLogic.pair_const (fastype_of1 (bound_Ts, t)) (fastype_of1 (bound_Ts, u)) $ t $ u;
-fun mk_tuple1 bound_Ts = the_default HOLogic.unit o try (foldr1 (mk_prod1 bound_Ts));
-
type coeqn_data_disc = {
fun_name: string,
fun_T: typ,
@@ -734,12 +730,12 @@
if is_none (#pred (nth ctr_specs ctr_no)) then I else
s_conjs prems
|> curry subst_bounds (List.rev fun_args)
- |> HOLogic.tupled_lambda (HOLogic.mk_tuple fun_args)
+ |> abs_tuple_balanced fun_args
|> K |> nth_map (the (#pred (nth ctr_specs ctr_no)));
fun build_corec_arg_no_call (sel_eqns : coeqn_data_sel list) sel =
find_first (curry (op =) sel o #sel) sel_eqns
- |> try (fn SOME {fun_args, rhs_term, ...} => abs_tuple fun_args rhs_term)
+ |> try (fn SOME {fun_args, rhs_term, ...} => abs_tuple_balanced fun_args rhs_term)
|> the_default undef_const
|> K;
@@ -752,9 +748,9 @@
fun rewrite_stop _ t = if has_call t then @{term False} else @{term True};
fun rewrite_end _ t = if has_call t then undef_const else t;
fun rewrite_cont bound_Ts t =
- if has_call t then mk_tuple1 bound_Ts (snd (strip_comb t)) else undef_const;
+ if has_call t then mk_tuple1_balanced bound_Ts (snd (strip_comb t)) else undef_const;
fun massage f _ = massage_let_if_case lthy has_call f bound_Ts rhs_term
- |> abs_tuple fun_args;
+ |> abs_tuple_balanced fun_args;
in
(massage rewrite_stop, massage rewrite_end, massage rewrite_cont)
end);
@@ -770,7 +766,7 @@
| rewrite bound_Ts (t as _ $ _) =
let val (u, vs) = strip_comb t in
if is_Free u andalso has_call u then
- Inr_const U T $ mk_tuple1 bound_Ts vs
+ Inr_const U T $ mk_tuple1_balanced bound_Ts vs
else if try (fst o dest_Const) u = SOME @{const_name case_prod} then
map (rewrite bound_Ts) vs |> chop 1
|>> HOLogic.mk_split o the_single
@@ -789,7 +785,7 @@
fun build t =
rhs_term
|> massage_nested_corec_call lthy has_call massage bound_Ts (range_type (fastype_of t))
- |> abs_tuple fun_args;
+ |> abs_tuple_balanced fun_args;
in
build
end);
@@ -827,7 +823,7 @@
|> fold2 (fold o build_corec_arg_disc) ctr_specss disc_eqnss
|> fold2 (fold o build_corec_args_sel lthy has_call) sel_eqnss ctr_specss;
fun currys [] t = t
- | currys Ts t = t $ mk_tuple1 (List.rev Ts) (map Bound (length Ts - 1 downto 0))
+ | currys Ts t = t $ mk_tuple1_balanced (List.rev Ts) (map Bound (length Ts - 1 downto 0))
|> fold_rev (Term.abs o pair Name.uu) Ts;
(*
@@ -907,7 +903,7 @@
val thy = Proof_Context.theory_of lthy;
val (bs, mxs) = map_split (apfst fst) fixes;
- val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> HOLogic.mk_tupleT) fixes |> split_list;
+ val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> mk_tupleT_balanced) fixes |> split_list;
val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, HOLogic.typeS)) (bs ~~ arg_Ts) of
[] => ()
--- a/src/HOL/Tools/Function/function_elims.ML Fri Mar 07 20:46:27 2014 +0100
+++ b/src/HOL/Tools/Function/function_elims.ML Fri Mar 07 20:50:02 2014 +0100
@@ -114,7 +114,7 @@
val args = HOLogic.mk_tuple arg_vars;
val domT = R |> dest_Free |> snd |> hd o snd o dest_Type;
- val sumtree_inj = SumTree.mk_inj domT n_fs (idx+1) args;
+ val sumtree_inj = Sum_Tree.mk_inj domT n_fs (idx+1) args;
val cprop = cert prop;
@@ -155,4 +155,3 @@
end;
end;
-
--- a/src/HOL/Tools/Function/induction_schema.ML Fri Mar 07 20:46:27 2014 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML Fri Mar 07 20:50:02 2014 +0100
@@ -11,7 +11,6 @@
val induction_schema_tac : Proof.context -> thm list -> tactic
end
-
structure Induction_Schema : INDUCTION_SCHEMA =
struct
@@ -111,7 +110,7 @@
fun PT_of (SchemeBranch { xs, ...}) =
foldr1 HOLogic.mk_prodT (map snd xs)
- val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) (map PT_of branches)
+ val ST = Balanced_Tree.make (uncurry Sum_Tree.mk_sumT) (map PT_of branches)
in
IndScheme {T=ST, cases=map mk_case cases', branches=branches }
end
@@ -146,7 +145,7 @@
fun mk_ineqs R (IndScheme {T, cases, branches}) =
let
fun inject i ts =
- SumTree.mk_inj T (length branches) (i + 1) (foldr1 HOLogic.mk_prod ts)
+ Sum_Tree.mk_inj T (length branches) (i + 1) (foldr1 HOLogic.mk_prod ts)
val thesis = Free ("thesis", HOLogic.boolT) (* FIXME *)
@@ -199,7 +198,7 @@
|> Object_Logic.drop_judgment thy
|> HOLogic.tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
in
- SumTree.mk_sumcases HOLogic.boolT (map brnch branches)
+ Sum_Tree.mk_sumcases HOLogic.boolT (map brnch branches)
end
fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss
@@ -212,7 +211,7 @@
val scases_idx = map_index I scases
fun inject i ts =
- SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts)
+ Sum_Tree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts)
val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches)
val P_comp = mk_ind_goal ctxt branches
@@ -372,12 +371,12 @@
fun project (i, SchemeBranch {xs, ...}) =
let
val inst = (foldr1 HOLogic.mk_prod (map Free xs))
- |> SumTree.mk_inj ST (length branches) (i + 1)
+ |> Sum_Tree.mk_inj ST (length branches) (i + 1)
|> cert
in
indthm
|> Drule.instantiate' [] [SOME inst]
- |> simplify (put_simpset SumTree.sumcase_split_ss ctxt'')
+ |> simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt'')
|> Conv.fconv_rule (ind_rulify ctxt'')
end
--- a/src/HOL/Tools/Function/measure_functions.ML Fri Mar 07 20:46:27 2014 +0100
+++ b/src/HOL/Tools/Function/measure_functions.ML Fri Mar 07 20:50:02 2014 +0100
@@ -6,10 +6,8 @@
signature MEASURE_FUNCTIONS =
sig
-
val get_measure_functions : Proof.context -> typ -> term list
val setup : theory -> theory
-
end
structure MeasureFunctions : MEASURE_FUNCTIONS =
@@ -40,12 +38,12 @@
fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero)
fun mk_funorder_funs (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
- map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT)
- @ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
+ map (fn m => Sum_Tree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT)
+ @ map (fn m => Sum_Tree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
| mk_funorder_funs T = [ constant_1 T ]
fun mk_ext_base_funs ctxt (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
- map_product (SumTree.mk_sumcase fT sT HOLogic.natT)
+ map_product (Sum_Tree.mk_sumcase fT sT HOLogic.natT)
(mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT)
| mk_ext_base_funs ctxt T = find_measures ctxt T
--- a/src/HOL/Tools/Function/mutual.ML Fri Mar 07 20:46:27 2014 +0100
+++ b/src/HOL/Tools/Function/mutual.ML Fri Mar 07 20:50:02 2014 +0100
@@ -6,7 +6,6 @@
signature FUNCTION_MUTUAL =
sig
-
val prepare_function_mutual : Function_Common.function_config
-> string (* defname *)
-> ((string * typ) * mixfix) list
@@ -15,10 +14,8 @@
-> ((thm (* goalstate *)
* (thm -> Function_Common.function_result) (* proof continuation *)
) * local_theory)
-
end
-
structure Function_Mutual: FUNCTION_MUTUAL =
struct
@@ -88,8 +85,8 @@
val dresultTs = distinct (op =) resultTs
val n' = length dresultTs
- val RST = Balanced_Tree.make (uncurry SumTree.mk_sumT) dresultTs
- val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) argTs
+ val RST = Balanced_Tree.make (uncurry Sum_Tree.mk_sumT) dresultTs
+ val ST = Balanced_Tree.make (uncurry Sum_Tree.mk_sumT) argTs
val fsum_type = ST --> RST
@@ -101,7 +98,7 @@
val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *)
val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1
- val f_exp = SumTree.mk_proj RST n' i' (Free fsum_var $ SumTree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars))
+ val f_exp = Sum_Tree.mk_proj RST n' i' (Free fsum_var $ Sum_Tree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars))
val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp)
val rew = (n, fold_rev lambda vars f_exp)
@@ -117,8 +114,8 @@
val rhs' = rhs
|> map_aterms (fn t as Free (n, _) => the_default t (AList.lookup (op =) rews n) | t => t)
in
- (qs, gs, SumTree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args),
- Envir.beta_norm (SumTree.mk_inj RST n' i' rhs'))
+ (qs, gs, Sum_Tree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args),
+ Envir.beta_norm (Sum_Tree.mk_inj RST n' i' rhs'))
end
val qglrs = map convert_eqs fqgars
@@ -227,21 +224,21 @@
end
val Ps = map2 mk_P parts newPs
- val case_exp = SumTree.mk_sumcases HOLogic.boolT Ps
+ val case_exp = Sum_Tree.mk_sumcases HOLogic.boolT Ps
val induct_inst =
Thm.forall_elim (cert case_exp) induct
- |> full_simplify (put_simpset SumTree.sumcase_split_ss ctxt)
+ |> full_simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt)
|> full_simplify (put_simpset HOL_basic_ss ctxt addsimps all_f_defs)
fun project rule (MutualPart {cargTs, i, ...}) k =
let
val afs = map_index (fn (j,T) => Free ("a" ^ string_of_int (j + k), T)) cargTs (* FIXME! *)
- val inj = SumTree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs)
+ val inj = Sum_Tree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs)
in
(rule
|> Thm.forall_elim (cert inj)
- |> full_simplify (put_simpset SumTree.sumcase_split_ss ctxt)
+ |> full_simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt)
|> fold_rev (Thm.forall_intr o cert) (afs @ newPs),
k + length cargTs)
end
@@ -260,7 +257,7 @@
val cert = cterm_of (Proof_Context.theory_of ctxt)
- val sumtree_inj = SumTree.mk_inj ST n i args
+ val sumtree_inj = Sum_Tree.mk_inj ST n i args
val sum_elims =
@{thms HOL.notE[OF Sum_Type.sum.distinct(1)] HOL.notE[OF Sum_Type.sum.distinct(2)]}
--- a/src/HOL/Tools/Function/sum_tree.ML Fri Mar 07 20:46:27 2014 +0100
+++ b/src/HOL/Tools/Function/sum_tree.ML Fri Mar 07 20:50:02 2014 +0100
@@ -16,7 +16,7 @@
val mk_sumcases: typ -> term list -> term
end
-structure SumTree: SUM_TREE =
+structure Sum_Tree: SUM_TREE =
struct
(* Theory dependencies *)
--- a/src/HOL/Tools/Function/termination.ML Fri Mar 07 20:46:27 2014 +0100
+++ b/src/HOL/Tools/Function/termination.ML Fri Mar 07 20:50:02 2014 +0100
@@ -6,7 +6,6 @@
signature TERMINATION =
sig
-
type data
datatype cell = Less of thm | LessEq of thm * thm | None of thm * thm | False of thm
@@ -122,7 +121,7 @@
(* Build case expression *)
fun mk_sumcases (sk, _, _, _, _) T fs =
mk_tree (fn i => (nth fs i, domain_type (fastype_of (nth fs i))))
- (fn ((f, fT), (g, gT)) => (SumTree.mk_sumcase fT gT T f g, SumTree.mk_sumT fT gT))
+ (fn ((f, fT), (g, gT)) => (Sum_Tree.mk_sumcase fT gT T f g, Sum_Tree.mk_sumT fT gT))
sk
|> fst