--- a/src/HOL/Complex.thy Thu Sep 03 15:50:40 2015 +0200
+++ b/src/HOL/Complex.thy Fri Sep 04 09:15:15 2015 +0200
@@ -527,6 +527,9 @@
(auto simp: complex_eq_iff norm_complex_def power2_eq_square[symmetric] of_real_power[symmetric]
simp del: of_real_power)
+lemma complex_div_cnj: "a / b = (a * cnj b) / (norm b)^2"
+ using complex_norm_square by auto
+
lemma Re_complex_div_eq_0: "Re (a / b) = 0 \<longleftrightarrow> Re (a * cnj b) = 0"
by (auto simp add: Re_divide)
@@ -567,6 +570,18 @@
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_divide_of_real [simp]: "Re (z / of_real r) = Re z / r"
+ by (simp add: Re_divide power2_eq_square)
+
+lemma Im_divide_of_real [simp]: "Im (z / of_real r) = Im z / r"
+ by (simp add: Im_divide power2_eq_square)
+
+lemma Re_divide_Reals: "r \<in> Reals \<Longrightarrow> Re (z / r) = Re z / Re r"
+ by (metis Re_divide_of_real of_real_Re)
+
+lemma Im_divide_Reals: "r \<in> Reals \<Longrightarrow> Im (z / r) = Im z / Re r"
+ by (metis Im_divide_of_real of_real_Re)
+
lemma Re_setsum[simp]: "Re (setsum f s) = (\<Sum>x\<in>s. Re (f x))"
by (induct s rule: infinite_finite_induct) auto
@@ -588,6 +603,12 @@
lemma summable_Im: "summable f \<Longrightarrow> summable (\<lambda>x. Im (f x))"
unfolding summable_complex_iff by blast
+lemma complex_is_Nat_iff: "z \<in> \<nat> \<longleftrightarrow> Im z = 0 \<and> (\<exists>i. Re z = of_nat i)"
+ by (auto simp: Nats_def complex_eq_iff)
+
+lemma complex_is_Int_iff: "z \<in> \<int> \<longleftrightarrow> Im z = 0 \<and> (\<exists>i. Re z = of_int i)"
+ by (auto simp: Ints_def complex_eq_iff)
+
lemma complex_is_Real_iff: "z \<in> \<real> \<longleftrightarrow> Im z = 0"
by (auto simp: Reals_def complex_eq_iff)
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Thu Sep 03 15:50:40 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Sep 04 09:15:15 2015 +0200
@@ -1140,10 +1140,6 @@
subsection "Derivative"
-lemma differentiable_at_imp_differentiable_on:
- "(\<forall>x\<in>(s::(real^'n) set). f differentiable at x) \<Longrightarrow> f differentiable_on s"
- by (metis differentiable_at_withinI differentiable_on_def)
-
definition "jacobian f net = matrix(frechet_derivative f net)"
lemma jacobian_works:
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Thu Sep 03 15:50:40 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Fri Sep 04 09:15:15 2015 +0200
@@ -1,7 +1,7 @@
section \<open>Complex path integrals and Cauchy's integral theorem\<close>
theory Cauchy_Integral_Thm
-imports Complex_Transcendental Path_Connected
+imports Complex_Transcendental Weierstrass
begin
@@ -2512,13 +2512,14 @@
apply (rule path_integrable_holomorphic [OF contf os Finite_Set.finite.emptyI g])
using fh by (simp add: complex_differentiable_def holomorphic_on_open os)
-lemma path_integrable_inversediff:
+lemma continuous_on_inversediff:
+ fixes z:: "'a::real_normed_field" shows "z \<notin> s \<Longrightarrow> continuous_on s (\<lambda>w. 1 / (w - z))"
+ by (rule continuous_intros | force)+
+
+corollary path_integrable_inversediff:
"\<lbrakk>valid_path g; z \<notin> path_image g\<rbrakk> \<Longrightarrow> (\<lambda>w. 1 / (w-z)) path_integrable_on g"
-apply (rule path_integrable_holomorphic_simple [of "UNIV-{z}"])
- apply (rule continuous_intros | simp)+
- apply blast
-apply (simp add: holomorphic_on_open open_delete)
-apply (force intro: derivative_eq_intros)
+apply (rule path_integrable_holomorphic_simple [of "UNIV-{z}", OF continuous_on_inversediff])
+apply (auto simp: holomorphic_on_open open_delete intro!: derivative_eq_intros)
done
text{*Key fact that path integral is the same for a "nearby" path. This is the
@@ -2688,7 +2689,7 @@
\<subseteq> ball (p t) (ee (p t))"
apply (intro subset_path_image_join pi_hgn pi_ghn')
using `N>0` Suc.prems
- apply (auto simp: dist_norm field_simps ptgh_ee)
+ apply (auto simp: dist_norm field_simps closed_segment_eq_real_ivl ptgh_ee)
done
have pi0: "(f has_path_integral 0)
(subpath (n/ N) ((Suc n)/N) g +++ linepath(g ((Suc n) / N)) (h((Suc n) / N)) +++
@@ -2778,4 +2779,64 @@
using path_integral_nearby [OF assms, where Ends=False]
by simp_all
+lemma valid_path_polynomial_function:
+ fixes p :: "real \<Rightarrow> 'b::euclidean_space"
+ shows "polynomial_function p \<Longrightarrow> valid_path p"
+apply (simp add: valid_path_def)
+apply (rule differentiable_on_imp_piecewise_differentiable [OF differentiable_at_imp_differentiable_on])
+using differentiable_def has_vector_derivative_def
+apply (blast intro: dest: has_vector_derivative_polynomial_function)
+done
+
+lemma path_integral_bound_exists:
+assumes s: "open s"
+ and g: "valid_path g"
+ and pag: "path_image g \<subseteq> s"
+ shows "\<exists>L. 0 < L \<and>
+ (\<forall>f B. f holomorphic_on s \<and> (\<forall>z \<in> s. norm(f z) \<le> B)
+ \<longrightarrow> norm(path_integral g f) \<le> L*B)"
+proof -
+have "path g" using g
+ by (simp add: valid_path_imp_path)
+then obtain d::real and p
+ where d: "0 < d"
+ and p: "polynomial_function p" "path_image p \<subseteq> s"
+ and pi: "\<And>f. f holomorphic_on s \<Longrightarrow> path_integral g f = path_integral p f"
+ using path_integral_nearby_ends [OF s `path g` pag]
+ apply clarify
+ apply (drule_tac x=g in spec)
+ apply (simp only: assms)
+ apply (force simp: valid_path_polynomial_function dest: path_approx_polynomial_function)
+ done
+then obtain p' where p': "polynomial_function p'"
+ "\<And>x. (p has_vector_derivative (p' x)) (at x)"
+ using has_vector_derivative_polynomial_function by force
+then have "bounded(p' ` {0..1})"
+ using continuous_on_polymonial_function
+ by (force simp: intro!: compact_imp_bounded compact_continuous_image)
+then obtain L where L: "L>0" and nop': "\<And>x. x \<in> {0..1} \<Longrightarrow> norm (p' x) \<le> L"
+ by (force simp: bounded_pos)
+{ fix f B
+ assume f: "f holomorphic_on s"
+ and B: "\<And>z. z\<in>s \<Longrightarrow> cmod (f z) \<le> B"
+ then have "f path_integrable_on p \<and> valid_path p"
+ using p s
+ by (blast intro: valid_path_polynomial_function path_integrable_holomorphic_simple holomorphic_on_imp_continuous_on)
+ moreover have "\<And>x. x \<in> {0..1} \<Longrightarrow> cmod (vector_derivative p (at x)) * cmod (f (p x)) \<le> L * B"
+ apply (rule mult_mono)
+ apply (subst Derivative.vector_derivative_at; force intro: p' nop')
+ using L B p
+ apply (auto simp: path_image_def image_subset_iff)
+ done
+ ultimately have "cmod (path_integral g f) \<le> L * B"
+ apply (simp add: pi [OF f])
+ apply (simp add: path_integral_integral)
+ apply (rule order_trans [OF integral_norm_bound_integral])
+ apply (auto simp: mult.commute integral_norm_bound_integral path_integrable_on [symmetric] norm_mult)
+ done
+} then
+show ?thesis
+ by (force simp: L path_integral_integral)
+qed
+
end
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Sep 03 15:50:40 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Sep 04 09:15:15 2015 +0200
@@ -6375,7 +6375,7 @@
using segment_furthest_le[OF assms, of b]
by (auto simp add:norm_minus_commute)
-lemma segment_refl: "closed_segment a a = {a}"
+lemma segment_refl [simp]: "closed_segment a a = {a}"
unfolding segment by (auto simp add: algebra_simps)
lemma closed_segment_commute: "closed_segment a b = closed_segment b a"
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Thu Sep 03 15:50:40 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Fri Sep 04 09:15:15 2015 +0200
@@ -138,7 +138,7 @@
qed
lemma DERIV_caratheodory_within:
- "(f has_field_derivative l) (at x within s) \<longleftrightarrow>
+ "(f has_field_derivative l) (at x within s) \<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
@@ -209,6 +209,15 @@
using has_derivative_at_within
by blast
+lemma differentiable_at_imp_differentiable_on:
+ "(\<And>x. x \<in> s \<Longrightarrow> f differentiable at x) \<Longrightarrow> f differentiable_on s"
+ by (metis differentiable_at_withinI differentiable_on_def)
+
+corollary differentiable_iff_scaleR:
+ fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
+ shows "f differentiable F \<longleftrightarrow> (\<exists>d. (f has_derivative (\<lambda>x. x *\<^sub>R d)) F)"
+ by (auto simp: differentiable_def dest: has_derivative_linear linear_imp_scaleR)
+
lemma differentiable_within_open: (* TODO: delete *)
assumes "a \<in> s"
and "open s"
@@ -2241,6 +2250,24 @@
apply auto
done
+lemma has_vector_derivative_id_at [simp]: "vector_derivative (\<lambda>x. x) (at a) = 1"
+ by (simp add: vector_derivative_at)
+
+lemma vector_derivative_minus_at [simp]:
+ "f differentiable at a
+ \<Longrightarrow> vector_derivative (\<lambda>x. - f x) (at a) = - vector_derivative f (at a)"
+ by (simp add: vector_derivative_at has_vector_derivative_minus vector_derivative_works [symmetric])
+
+lemma vector_derivative_add_at [simp]:
+ "\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk>
+ \<Longrightarrow> vector_derivative (\<lambda>x. f x + g x) (at a) = vector_derivative f (at a) + vector_derivative g (at a)"
+ by (simp add: vector_derivative_at has_vector_derivative_add vector_derivative_works [symmetric])
+
+lemma vector_derivative_diff_at [simp]:
+ "\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk>
+ \<Longrightarrow> vector_derivative (\<lambda>x. f x - g x) (at a) = vector_derivative f (at a) - vector_derivative g (at a)"
+ by (simp add: vector_derivative_at has_vector_derivative_diff vector_derivative_works [symmetric])
+
lemma vector_derivative_within_closed_interval:
assumes "a < b"
and "x \<in> cbox a b"
--- a/src/HOL/Tools/BNF/bnf_def.ML Thu Sep 03 15:50:40 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Fri Sep 04 09:15:15 2015 +0200
@@ -808,10 +808,6 @@
end
end;
- fun maybe_restore lthy_old lthy =
- lthy |> not (Context.eq_thy (apply2 Proof_Context.theory_of (lthy_old, lthy)))
- ? Local_Theory.restore;
-
val map_bind_def =
(fn () => def_qualify (if Binding.is_empty map_b then mk_prefix_binding mapN else map_b),
map_rhs);
@@ -830,10 +826,11 @@
(bnf_set_terms, raw_set_defs)),
(bnf_bd_term, raw_bd_def)), (lthy, lthy_old)) =
no_defs_lthy
+ |> Local_Theory.open_target |> snd
|> maybe_define true map_bind_def
||>> apfst split_list o fold_map (maybe_define true) set_binds_defs
||>> maybe_define true bd_bind_def
- ||> `(maybe_restore no_defs_lthy);
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
@@ -929,9 +926,10 @@
val (((bnf_rel_term, raw_rel_def), (bnf_wit_terms, raw_wit_defs)), (lthy, lthy_old)) =
lthy
+ |> Local_Theory.open_target |> snd
|> maybe_define (is_some rel_rhs_opt) rel_bind_def
||>> apfst split_list o fold_map (maybe_define (not (null wit_rhss))) wit_binds_defs
- ||> `(maybe_restore lthy);
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
val bnf_rel_def = Morphism.thm phi raw_rel_def;
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Sep 03 15:50:40 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 04 09:15:15 2015 +0200
@@ -1219,8 +1219,9 @@
#> not (Config.get lthy0 bnf_note_all) ? Binding.concealed;
val ((cst, (_, def)), (lthy', lthy)) = lthy0
+ |> Local_Theory.open_target |> snd
|> Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs))
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy lthy';
@@ -2135,10 +2136,11 @@
#> not (Config.get no_defs_lthy bnf_note_all) ? Binding.concealed;
val ((raw_ctrs, raw_ctr_defs), (lthy', lthy)) = no_defs_lthy
+ |> Local_Theory.open_target |> snd
|> apfst split_list o @{fold_map 3} (fn b => fn mx => fn rhs =>
Local_Theory.define ((b, mx), ((maybe_conceal_def_binding b, []), rhs)) #>> apsnd snd)
ctr_bindings ctr_mixfixes ctr_rhss
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy lthy';
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Thu Sep 03 15:50:40 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Fri Sep 04 09:15:15 2015 +0200
@@ -396,8 +396,9 @@
resTs (map (Binding.suffix_name ("_" ^ recN)) bs) (([], []), lthy)
|>> map_prod rev rev;
val ((raw_co_recs, raw_co_rec_defs), (lthy, raw_lthy)) = lthy
+ |> Local_Theory.open_target |> snd
|> mk_recs
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism raw_lthy lthy;
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Thu Sep 03 15:50:40 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Fri Sep 04 09:15:15 2015 +0200
@@ -303,8 +303,9 @@
val ((coalg_free, (_, coalg_def_free)), (lthy, lthy_old)) =
lthy
+ |> Local_Theory.open_target |> snd
|> Local_Theory.define ((coalg_bind, NoSyn), (coalg_def_bind, coalg_spec))
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
val coalg = fst (Term.dest_Const (Morphism.term phi coalg_free));
@@ -382,8 +383,9 @@
val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) =
lthy
+ |> Local_Theory.open_target |> snd
|> Local_Theory.define ((mor_bind, NoSyn), (mor_def_bind, mor_spec))
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
val mor = fst (Term.dest_Const (Morphism.term phi mor_free));
@@ -530,8 +532,9 @@
val ((bis_free, (_, bis_def_free)), (lthy, lthy_old)) =
lthy
+ |> Local_Theory.open_target |> snd
|> Local_Theory.define ((bis_bind, NoSyn), (bis_def_bind, bis_spec))
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
val bis = fst (Term.dest_Const (Morphism.term phi bis_free));
@@ -653,10 +656,11 @@
val ((lsbis_frees, (_, lsbis_def_frees)), (lthy, lthy_old)) =
lthy
+ |> Local_Theory.open_target |> snd
|> fold_map (fn i => Local_Theory.define
((lsbis_bind i, NoSyn), (lsbis_def_bind i, lsbis_spec i))) ks
|>> apsnd split_list o split_list
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
@@ -738,8 +742,9 @@
val ((sbd_free, (_, sbd_def_free)), (lthy, lthy_old)) =
lthy
+ |> Local_Theory.open_target |> snd
|> Local_Theory.define ((sbd_bind, NoSyn), (sbd_def_bind, sbd_spec))
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
@@ -836,11 +841,12 @@
val ((isNode_frees, (_, isNode_def_frees)), (lthy, lthy_old)) =
lthy
+ |> Local_Theory.open_target |> snd
|> @{fold_map 3} (fn i => fn x => fn sets => Local_Theory.define
((isNode_bind i, NoSyn), (isNode_def_bind i, isNode_spec sets x i)))
ks xs isNode_setss
|>> apsnd split_list o split_list
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
@@ -875,10 +881,11 @@
val ((carT_frees, (_, carT_def_frees)), (lthy, lthy_old)) =
lthy
+ |> Local_Theory.open_target |> snd
|> fold_map (fn i =>
Local_Theory.define ((carT_bind i, NoSyn), (carT_def_bind i, carT_spec i))) ks
|>> apsnd split_list o split_list
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
@@ -907,11 +914,12 @@
val ((strT_frees, (_, strT_def_frees)), (lthy, lthy_old)) =
lthy
+ |> Local_Theory.open_target |> snd
|> @{fold_map 3} (fn i => fn mapFT => fn FT => Local_Theory.define
((strT_bind i, NoSyn), (strT_def_bind i, strT_spec mapFT FT i)))
ks tree_maps treeFTs
|>> apsnd split_list o split_list
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
@@ -976,8 +984,9 @@
val ((Lev_free, (_, Lev_def_free)), (lthy, lthy_old)) =
lthy
+ |> Local_Theory.open_target |> snd
|> Local_Theory.define ((Lev_bind, NoSyn), (Lev_def_bind, Lev_spec))
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
@@ -1019,8 +1028,9 @@
val ((rv_free, (_, rv_def_free)), (lthy, lthy_old)) =
lthy
+ |> Local_Theory.open_target |> snd
|> Local_Theory.define ((rv_bind, NoSyn), (rv_def_bind, rv_spec))
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
@@ -1061,10 +1071,11 @@
val ((beh_frees, (_, beh_def_frees)), (lthy, lthy_old)) =
lthy
+ |> Local_Theory.open_target |> snd
|> @{fold_map 2} (fn i => fn z =>
Local_Theory.define ((beh_bind i, NoSyn), (beh_def_bind i, beh_spec i z))) ks zs
|>> apsnd split_list o split_list
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
@@ -1336,12 +1347,13 @@
val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) =
lthy
+ |> Local_Theory.open_target |> snd
|> @{fold_map 6} (fn i => fn rep => fn str => fn mapx => fn Jz => fn Jz' =>
Local_Theory.define ((dtor_bind i, NoSyn),
(dtor_def_bind i, dtor_spec rep str mapx Jz Jz')))
ks Rep_Ts str_finals map_FTs Jzs Jzs'
|>> apsnd split_list o split_list
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
fun mk_dtors passive =
@@ -1381,12 +1393,13 @@
val ((unfold_frees, (_, unfold_def_frees)), (lthy, lthy_old)) =
lthy
+ |> Local_Theory.open_target |> snd
|> @{fold_map 4} (fn i => fn abs => fn f => fn z =>
Local_Theory.define ((unfold_bind i, NoSyn), (unfold_def_bind i, unfold_spec abs f z)))
ks Abs_Ts (map (fn i => HOLogic.mk_comp
(mk_proj (nth lsbisAs (i - 1)), mk_beh ss i)) ks) zs
|>> apsnd split_list o split_list
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
val unfolds = map (Morphism.term phi) unfold_frees;
@@ -1474,10 +1487,11 @@
val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) =
lthy
+ |> Local_Theory.open_target |> snd
|> fold_map (fn i =>
Local_Theory.define ((ctor_bind i, NoSyn), (ctor_def_bind i, ctor_spec i))) ks
|>> apsnd split_list o split_list
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
fun mk_ctors params =
@@ -1546,11 +1560,12 @@
val ((corec_frees, (_, corec_def_frees)), (lthy, lthy_old)) =
lthy
+ |> Local_Theory.open_target |> snd
|> @{fold_map 3} (fn i => fn T => fn AT =>
Local_Theory.define ((corec_bind i, NoSyn), (corec_def_bind i, corec_spec i T AT)))
ks Ts activeAs
|>> apsnd split_list o split_list
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
val corecs = map (Morphism.term phi) corec_frees;
@@ -1742,11 +1757,12 @@
val ((col_frees, (_, col_def_frees)), (lthy, lthy_old)) =
lthy
+ |> Local_Theory.open_target |> snd
|> @{fold_map 4} (fn j => fn Zero => fn hrec => fn hrec' => Local_Theory.define
((col_bind j, NoSyn), (col_def_bind j, col_spec j Zero hrec hrec')))
ls Zeros hrecs hrecs'
|>> apsnd split_list o split_list
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Thu Sep 03 15:50:40 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Fri Sep 04 09:15:15 2015 +0200
@@ -251,8 +251,9 @@
val ((alg_free, (_, alg_def_free)), (lthy, lthy_old)) =
lthy
+ |> Local_Theory.open_target |> snd
|> Local_Theory.define ((alg_bind, NoSyn), (alg_def_bind, alg_spec))
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
val alg = fst (Term.dest_Const (Morphism.term phi alg_free));
@@ -331,8 +332,9 @@
val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) =
lthy
+ |> Local_Theory.open_target |> snd
|> Local_Theory.define ((mor_bind, NoSyn), (mor_def_bind, mor_spec))
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
val mor = fst (Term.dest_Const (Morphism.term phi mor_free));
@@ -472,8 +474,9 @@
val ((sbd_free, (_, sbd_def_free)), (lthy, lthy_old)) =
lthy
+ |> Local_Theory.open_target |> snd
|> Local_Theory.define ((sbd_bind, NoSyn), (sbd_def_bind, sbd_spec))
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
@@ -656,10 +659,11 @@
val ((min_alg_frees, (_, min_alg_def_frees)), (lthy, lthy_old)) =
lthy
+ |> Local_Theory.open_target |> snd
|> fold_map (fn i => Local_Theory.define
((min_alg_bind i, NoSyn), (min_alg_def_bind i, min_alg_spec i))) ks
|>> apsnd split_list o split_list
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
val min_algs = map (fst o Term.dest_Const o Morphism.term phi) min_alg_frees;
@@ -768,10 +772,11 @@
val ((str_init_frees, (_, str_init_def_frees)), (lthy, lthy_old)) =
lthy
+ |> Local_Theory.open_target |> snd
|> fold_map (fn i => Local_Theory.define
((str_init_bind i, NoSyn), (str_init_def_bind i, str_init_spec i))) ks
|>> apsnd split_list o split_list
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
val str_inits =
@@ -926,12 +931,13 @@
val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) =
lthy
+ |> Local_Theory.open_target |> snd
|> @{fold_map 4} (fn i => fn abs => fn str => fn mapx =>
Local_Theory.define
((ctor_bind i, NoSyn), (ctor_def_bind i, ctor_spec abs str mapx)))
ks Abs_Ts str_inits map_FT_inits
|>> apsnd split_list o split_list
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
fun mk_ctors passive =
@@ -978,10 +984,11 @@
val ((fold_frees, (_, fold_def_frees)), (lthy, lthy_old)) =
lthy
+ |> Local_Theory.open_target |> snd
|> fold_map (fn i =>
Local_Theory.define ((fold_bind i, NoSyn), (fold_def_bind i, fold_spec i))) ks
|>> apsnd split_list o split_list
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
val folds = map (Morphism.term phi) fold_frees;
@@ -1086,10 +1093,11 @@
val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) =
lthy
+ |> Local_Theory.open_target |> snd
|> fold_map (fn i =>
Local_Theory.define ((dtor_bind i, NoSyn), (dtor_def_bind i, dtor_spec i))) ks
|>> apsnd split_list o split_list
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
fun mk_dtors params =
@@ -1157,10 +1165,11 @@
val ((rec_frees, (_, rec_def_frees)), (lthy, lthy_old)) =
lthy
+ |> Local_Theory.open_target |> snd
|> @{fold_map 3} (fn i => fn T => fn AT =>
Local_Theory.define ((rec_bind i, NoSyn), (rec_def_bind i, rec_spec i T AT))) ks Ts activeAs
|>> apsnd split_list o split_list
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
val recs = map (Morphism.term phi) rec_frees;
@@ -1417,8 +1426,9 @@
val ((sbd0_free, (_, sbd0_def_free)), (lthy, lthy_old)) =
lthy
+ |> Local_Theory.open_target |> snd
|> Local_Theory.define ((sbd0_bind, NoSyn), (sbd0_def_bind, sbd0_spec))
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Thu Sep 03 15:50:40 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Sep 04 09:15:15 2015 +0200
@@ -183,14 +183,15 @@
val nested_size_gen_o_maps_complete = forall (not o null) nested_size_gen_o_mapss;
val nested_size_gen_o_maps = fold (union Thm.eq_thm_prop) nested_size_gen_o_mapss [];
- val ((raw_size_consts, raw_size_defs), (lthy1', lthy1)) = lthy0
+ val ((raw_size_consts, raw_size_defs), (lthy1, lthy1_old)) = lthy0
+ |> Local_Theory.open_target |> snd
|> apfst split_list o @{fold_map 2} (fn b => fn rhs =>
Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs))
#>> apsnd snd)
size_bs size_rhss
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
- val phi = Proof_Context.export_morphism lthy1 lthy1';
+ val phi = Proof_Context.export_morphism lthy1_old lthy1;
val size_defs = map (Morphism.thm phi) raw_size_defs;
--- a/src/HOL/Tools/BNF/bnf_util.ML Thu Sep 03 15:50:40 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML Fri Sep 04 09:15:15 2015 +0200
@@ -145,10 +145,9 @@
val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (Binding.path_of b)) b;
val ((name, info), (lthy, lthy_old)) =
lthy
- |> Proof_Context.concealed
+ |> Local_Theory.open_target |> snd
|> Typedef.add_typedef true (b', Ts, mx) set opt_morphs tac
- ||> Proof_Context.restore_naming lthy
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
in
((name, Typedef.transform_info phi info), lthy)
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Thu Sep 03 15:50:40 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Sep 04 09:15:15 2015 +0200
@@ -503,12 +503,13 @@
(Const (@{const_name The}, (B --> HOLogic.boolT) --> B) $
Term.lambda w (Library.foldr1 HOLogic.mk_disj (@{map 3} mk_case_disj xctrs xfs xss)));
- val ((raw_case, (_, raw_case_def)), (lthy', lthy)) = no_defs_lthy
+ val ((raw_case, (_, raw_case_def)), (lthy, lthy_old)) = no_defs_lthy
+ |> Local_Theory.open_target |> snd
|> Local_Theory.define ((case_binding, NoSyn),
((Binding.concealed (Thm.def_binding case_binding), []), case_rhs))
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
- val phi = Proof_Context.export_morphism lthy lthy';
+ val phi = Proof_Context.export_morphism lthy_old lthy;
val case_def = Morphism.thm phi raw_case_def;
@@ -549,9 +550,9 @@
forall (forall Binding.is_empty) (raw_disc_bindings :: raw_sel_bindingss) andalso
null sel_default_eqs;
- val (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy') =
+ val (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy) =
if no_discs_sels then
- (true, [], [], [], [], [], lthy')
+ (true, [], [], [], [], [], lthy)
else
let
val all_sel_bindings = flat sel_bindingss;
@@ -623,6 +624,7 @@
val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) =
lthy
+ |> Local_Theory.open_target |> snd
|> apfst split_list o @{fold_map 3} (fn k => fn exist_xs_u_eq_ctr => fn b =>
if Binding.is_empty b then
if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def)
@@ -636,7 +638,7 @@
||>> apfst split_list o fold_map (fn (b, proto_sels) =>
Specification.definition (SOME (b, NONE, NoSyn),
((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy lthy';
@@ -1122,7 +1124,7 @@
(ctr_sugar, lthy' |> register_ctr_sugar plugins ctr_sugar)
end;
in
- (goalss, after_qed, lthy')
+ (goalss, after_qed, lthy)
end;
fun free_constructors kind tacss = (fn (goalss, after_qed, lthy) =>
--- a/src/HOL/Tools/typedef.ML Thu Sep 03 15:50:40 2015 +0200
+++ b/src/HOL/Tools/typedef.ML Fri Sep 04 09:15:15 2015 +0200
@@ -65,10 +65,15 @@
fun merge data = Symtab.merge_list (K true) data;
);
-val get_info = Symtab.lookup_list o Data.get o Context.Proof;
-val get_info_global = Symtab.lookup_list o Data.get o Context.Theory;
+fun get_info_generic context =
+ Symtab.lookup_list (Data.get context) #>
+ map (transform_info (Morphism.transfer_morphism (Context.theory_of context)));
-fun put_info name info = Data.map (Symtab.cons_list (name, info));
+val get_info = get_info_generic o Context.Proof;
+val get_info_global = get_info_generic o Context.Theory;
+
+fun put_info name info =
+ Data.map (Symtab.cons_list (name, transform_info Morphism.trim_context_morphism info));
(* global interpretation *)
@@ -289,4 +294,3 @@
>> (fn ((((vs, t), mx), A), morphs) => fn lthy => typedef_cmd ((t, vs, mx), A, morphs) lthy));
end;
-
--- a/src/HOL/Typedef.thy Thu Sep 03 15:50:40 2015 +0200
+++ b/src/HOL/Typedef.thy Fri Sep 04 09:15:15 2015 +0200
@@ -13,12 +13,11 @@
fixes Rep and Abs and A
assumes Rep: "Rep x \<in> A"
and Rep_inverse: "Abs (Rep x) = x"
- and Abs_inverse: "y \<in> A ==> Rep (Abs y) = y"
+ and Abs_inverse: "y \<in> A \<Longrightarrow> Rep (Abs y) = y"
-- \<open>This will be axiomatized for each typedef!\<close>
begin
-lemma Rep_inject:
- "(Rep x = Rep y) = (x = y)"
+lemma Rep_inject: "Rep x = Rep y \<longleftrightarrow> x = y"
proof
assume "Rep x = Rep y"
then have "Abs (Rep x) = Abs (Rep y)" by (simp only:)
@@ -27,44 +26,44 @@
ultimately show "x = y" by simp
next
assume "x = y"
- thus "Rep x = Rep y" by (simp only:)
+ then show "Rep x = Rep y" by (simp only:)
qed
lemma Abs_inject:
- assumes x: "x \<in> A" and y: "y \<in> A"
- shows "(Abs x = Abs y) = (x = y)"
+ assumes "x \<in> A" and "y \<in> A"
+ shows "Abs x = Abs y \<longleftrightarrow> x = y"
proof
assume "Abs x = Abs y"
then have "Rep (Abs x) = Rep (Abs y)" by (simp only:)
- moreover from x have "Rep (Abs x) = x" by (rule Abs_inverse)
- moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse)
+ moreover from \<open>x \<in> A\<close> have "Rep (Abs x) = x" by (rule Abs_inverse)
+ moreover from \<open>y \<in> A\<close> have "Rep (Abs y) = y" by (rule Abs_inverse)
ultimately show "x = y" by simp
next
assume "x = y"
- thus "Abs x = Abs y" by (simp only:)
+ then show "Abs x = Abs y" by (simp only:)
qed
lemma Rep_cases [cases set]:
- assumes y: "y \<in> A"
- and hyp: "!!x. y = Rep x ==> P"
+ assumes "y \<in> A"
+ and hyp: "\<And>x. y = Rep x \<Longrightarrow> P"
shows P
proof (rule hyp)
- from y have "Rep (Abs y) = y" by (rule Abs_inverse)
- thus "y = Rep (Abs y)" ..
+ from \<open>y \<in> A\<close> have "Rep (Abs y) = y" by (rule Abs_inverse)
+ then show "y = Rep (Abs y)" ..
qed
lemma Abs_cases [cases type]:
- assumes r: "!!y. x = Abs y ==> y \<in> A ==> P"
+ assumes r: "\<And>y. x = Abs y \<Longrightarrow> y \<in> A \<Longrightarrow> P"
shows P
proof (rule r)
have "Abs (Rep x) = x" by (rule Rep_inverse)
- thus "x = Abs (Rep x)" ..
+ then show "x = Abs (Rep x)" ..
show "Rep x \<in> A" by (rule Rep)
qed
lemma Rep_induct [induct set]:
assumes y: "y \<in> A"
- and hyp: "!!x. P (Rep x)"
+ and hyp: "\<And>x. P (Rep x)"
shows "P y"
proof -
have "P (Rep (Abs y))" by (rule hyp)
@@ -73,7 +72,7 @@
qed
lemma Abs_induct [induct type]:
- assumes r: "!!y. y \<in> A ==> P (Abs y)"
+ assumes r: "\<And>y. y \<in> A \<Longrightarrow> P (Abs y)"
shows "P x"
proof -
have "Rep x \<in> A" by (rule Rep)
@@ -84,25 +83,24 @@
lemma Rep_range: "range Rep = A"
proof
- show "range Rep <= A" using Rep by (auto simp add: image_def)
- show "A <= range Rep"
+ show "range Rep \<subseteq> A" using Rep by (auto simp add: image_def)
+ show "A \<subseteq> range Rep"
proof
- fix x assume "x : A"
- hence "x = Rep (Abs x)" by (rule Abs_inverse [symmetric])
- thus "x : range Rep" by (rule range_eqI)
+ fix x assume "x \<in> A"
+ then have "x = Rep (Abs x)" by (rule Abs_inverse [symmetric])
+ then show "x \<in> range Rep" by (rule range_eqI)
qed
qed
lemma Abs_image: "Abs ` A = UNIV"
proof
- show "Abs ` A <= UNIV" by (rule subset_UNIV)
-next
- show "UNIV <= Abs ` A"
+ show "Abs ` A \<subseteq> UNIV" by (rule subset_UNIV)
+ show "UNIV \<subseteq> Abs ` A"
proof
fix x
have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric])
- moreover have "Rep x : A" by (rule Rep)
- ultimately show "x : Abs ` A" by (rule image_eqI)
+ moreover have "Rep x \<in> A" by (rule Rep)
+ ultimately show "x \<in> Abs ` A" by (rule image_eqI)
qed
qed
--- a/src/Pure/General/completion.scala Thu Sep 03 15:50:40 2015 +0200
+++ b/src/Pure/General/completion.scala Fri Sep 04 09:15:15 2015 +0200
@@ -135,6 +135,10 @@
/** semantic completion **/
+ def clean_name(s: String): Option[String] =
+ if (s == "" || s == "_") None
+ else Some(s.reverseIterator.dropWhile(_ == '_').toList.reverse.mkString)
+
def report_no_completion(pos: Position.T): String =
YXML.string_of_tree(Semantic.Info(pos, No_Completion))
--- a/src/Tools/jEdit/src/bibtex_jedit.scala Thu Sep 03 15:50:40 2015 +0200
+++ b/src/Tools/jEdit/src/bibtex_jedit.scala Fri Sep 04 09:15:15 2015 +0200
@@ -79,12 +79,16 @@
{
for {
Text.Info(r, name) <- rendering.citation(JEdit_Lib.before_caret_range(text_area, rendering))
+ name1 <- Completion.clean_name(name)
+
original <- JEdit_Lib.try_get_text(text_area.getBuffer, r)
- orig = Library.perhaps_unquote(original)
- entries = complete(name).filter(_ != orig)
+ original1 <- Completion.clean_name(Library.perhaps_unquote(original))
+
+ entries = complete(name1).filter(_ != original1)
if entries.nonEmpty
+
items =
- entries.map({
+ entries.sorted.map({
case entry =>
val full_name = Long_Name.qualify(Markup.CITATION, entry)
val description = List(entry, "(BibTeX entry)")