# HG changeset patch # User eberlm # Date 1501862630 -7200 # Node ID 1f66c7d77002149f9f339136e03f2e9b1292562b # Parent 56f8bfe1211cdac8f0be259b6247a277fcb00ded# Parent 1a8441ec5cedb5d53350bc5e5d514912a74c8dd9 Merged diff -r 56f8bfe1211c -r 1f66c7d77002 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Thu Aug 03 13:35:28 2017 +0200 +++ b/Admin/components/components.sha1 Fri Aug 04 18:03:50 2017 +0200 @@ -5,6 +5,7 @@ e7ffe4238b61a3c1ee87aca4421e7a612e09b836 ci-extras-1.tar.gz 70105fd6fbfd1a868383fc510772b95234325d31 csdp-6.x.tar.gz 2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7 cvc3-2.4.1.tar.gz +3682476dc5e915cf260764fa5b86f1ebdab57507 cvc4-1.5.tar.gz a5e02b5e990da4275dc5d4480c3b72fc73160c28 cvc4-1.5pre-1.tar.gz 4d9658fd2688ae8ac78da8fdfcbf85960f871b71 cvc4-1.5pre-2.tar.gz b01fdb93f2dc2b8bcfd41c6091d91b37d6e240f9 cvc4-1.5pre-3.tar.gz diff -r 56f8bfe1211c -r 1f66c7d77002 Admin/components/main --- a/Admin/components/main Thu Aug 03 13:35:28 2017 +0200 +++ b/Admin/components/main Fri Aug 04 18:03:50 2017 +0200 @@ -1,7 +1,7 @@ #main components for everyday use, without big impact on overall build time bash_process-1.2.1 csdp-6.x -cvc4-1.5pre-4 +cvc4-1.5 e-1.8 isabelle_fonts-20160830 jdk-8u131 diff -r 56f8bfe1211c -r 1f66c7d77002 src/Doc/Implementation/Local_Theory.thy --- a/src/Doc/Implementation/Local_Theory.thy Thu Aug 03 13:35:28 2017 +0200 +++ b/src/Doc/Implementation/Local_Theory.thy Fri Aug 04 18:03:50 2017 +0200 @@ -91,8 +91,7 @@ text %mlref \ \begin{mldecls} @{index_ML_type local_theory: Proof.context} \\ - @{index_ML Named_Target.init: "(local_theory -> local_theory) option -> - string -> theory -> local_theory"} \\[1ex] + @{index_ML Named_Target.init: "string -> theory -> local_theory"} \\[1ex] @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) -> local_theory -> (term * (string * thm)) * local_theory"} \\ @{index_ML Local_Theory.note: "Attrib.binding * thm list -> diff -r 56f8bfe1211c -r 1f66c7d77002 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Aug 03 13:35:28 2017 +0200 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Fri Aug 04 18:03:50 2017 +0200 @@ -7,6 +7,24 @@ imports Lebesgue_Measure Henstock_Kurzweil_Integration Complete_Measure Set_Integral begin +lemma finite_product_dependent: (*FIXME DELETE*) + assumes "finite s" + and "\x. x \ s \ finite (t x)" + shows "finite {(i, j) |i j. i \ s \ j \ t i}" + using assms +proof induct + case (insert x s) + have *: "{(i, j) |i j. i \ insert x s \ j \ t i} = + (\y. (x,y)) ` (t x) \ {(i, j) |i j. i \ s \ j \ t i}" by auto + show ?case + unfolding * + apply (rule finite_UnI) + using insert + apply auto + done +qed auto + + lemma le_left_mono: "x \ y \ y \ a \ x \ (a::'a::preorder)" by (auto intro: order_trans) @@ -1633,11 +1651,16 @@ then show "\e>0. \i\d. x \ i \ ball x e \ i = {}" by force qed - from choice[OF this] guess k .. note k=conjunctD2[OF this[rule_format],rule_format] - + then obtain k where k: "\x. 0 < k x" + "\i x. \i \ d; x \ i\ \ ball x (k x) \ i = {}" + by metis have "e/2 > 0" using e by auto - from henstock_lemma[OF assms(1) this] guess g . note g=this[rule_format] + from henstock_lemma[OF assms(1) this] + obtain g where g: "gauge g" + "\p. \p tagged_partial_division_of cbox a b; g fine p\ + \ (\(x, k)\p. norm (content k *\<^sub>R f x - integral k f)) < e / 2" + by (metis (no_types, lifting)) let ?g = "\x. g x \ ball x (k x)" show ?case apply (rule_tac x="?g" in exI) @@ -1716,15 +1739,12 @@ assume y: "y \ cbox a b" then have "\x l. (x, l) \ p \ y\l" unfolding p'(6)[symmetric] by auto - then guess x l by (elim exE) note xl=conjunctD2[OF this] + then obtain x l where xl: "(x, l) \ p" "y \ l" by metis then have "\k. k \ d \ y \ k" using y unfolding d'(6)[symmetric] by auto - then guess i .. note i = conjunctD2[OF this] + then obtain i where i: "i \ d" "y \ i" by metis have "x \ i" - using fineD[OF p(3) xl(1)] - using k(2)[OF i(1), of x] - using i(2) xl(2) - by auto + using fineD[OF p(3) xl(1)] using k(2) i xl by auto then show "y \ \{k. \x. (x, k) \ p'}" unfolding p'_def Union_iff apply (rule_tac x="i \ l" in bexI) @@ -1735,12 +1755,7 @@ qed then have "(\(x, k)\p'. norm (content k *\<^sub>R f x - integral k f)) < e / 2" - apply - - apply (rule g(2)[rule_format]) - unfolding tagged_division_of_def - apply safe - apply (rule gp') - done + using g(2) gp' tagged_division_of_def by blast then have **: "\(\(x,k)\p'. norm (content k *\<^sub>R f x)) - (\(x,k)\p'. norm (integral k f))\ < e / 2" unfolding split_def using p'' diff -r 56f8bfe1211c -r 1f66c7d77002 src/HOL/Analysis/Lebesgue_Integral_Substitution.thy --- a/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy Thu Aug 03 13:35:28 2017 +0200 +++ b/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy Fri Aug 04 18:03:50 2017 +0200 @@ -12,6 +12,7 @@ imports Interval_Integral begin + lemma nn_integral_substitution_aux: fixes f :: "real \ ennreal" assumes Mf: "f \ borel_measurable borel" diff -r 56f8bfe1211c -r 1f66c7d77002 src/HOL/Analysis/Tagged_Division.thy --- a/src/HOL/Analysis/Tagged_Division.thy Thu Aug 03 13:35:28 2017 +0200 +++ b/src/HOL/Analysis/Tagged_Division.thy Fri Aug 04 18:03:50 2017 +0200 @@ -10,23 +10,6 @@ Topology_Euclidean_Space begin -lemma finite_product_dependent: (*FIXME DELETE*) - assumes "finite s" - and "\x. x \ s \ finite (t x)" - shows "finite {(i, j) |i j. i \ s \ j \ t i}" - using assms -proof induct - case (insert x s) - have *: "{(i, j) |i j. i \ insert x s \ j \ t i} = - (\y. (x,y)) ` (t x) \ {(i, j) |i j. i \ s \ j \ t i}" by auto - show ?case - unfolding * - apply (rule finite_UnI) - using insert - apply auto - done -qed auto - lemma sum_Sigma_product: assumes "finite S" and "\i. i \ S \ finite (T i)" @@ -210,18 +193,18 @@ subsection \The notion of a gauge --- simply an open set containing the point.\ -definition "gauge d \ (\x. x \ d x \ open (d x))" +definition "gauge \ \ (\x. x \ \ x \ open (\ x))" lemma gaugeI: - assumes "\x. x \ g x" - and "\x. open (g x)" - shows "gauge g" + assumes "\x. x \ \ x" + and "\x. open (\ x)" + shows "gauge \" using assms unfolding gauge_def by auto lemma gaugeD[dest]: - assumes "gauge d" - shows "x \ d x" - and "open (d x)" + assumes "gauge \" + shows "x \ \ x" + and "open (\ x)" using assms unfolding gauge_def by auto lemma gauge_ball_dependent: "\x. 0 < e x \ gauge (\x. ball x (e x))" @@ -233,7 +216,7 @@ lemma gauge_trivial[intro!]: "gauge (\x. ball x 1)" by (rule gauge_ball) auto -lemma gauge_Int[intro]: "gauge d1 \ gauge d2 \ gauge (\x. d1 x \ d2 x)" +lemma gauge_Int[intro]: "gauge \1 \ gauge \2 \ gauge (\x. \1 x \ \2 x)" unfolding gauge_def by auto lemma gauge_reflect: @@ -244,10 +227,10 @@ lemma gauge_Inter: assumes "finite S" - and "\d. d\S \ gauge (f d)" - shows "gauge (\x. \{f d x | d. d \ S})" + and "\u. u\S \ gauge (f u)" + shows "gauge (\x. \{f u x | u. u \ S})" proof - - have *: "\x. {f d x |d. d \ S} = (\d. f d x) ` S" + have *: "\x. {f u x |u. u \ S} = (\u. f u x) ` S" by auto show ?thesis unfolding gauge_def unfolding * @@ -314,18 +297,15 @@ assume "s = {{a}}" "K\s" then have "\x y. K = cbox x y" apply (rule_tac x=a in exI)+ - apply (force simp: cbox_sing) + apply force done } ultimately show ?l unfolding division_of_def cbox_sing by auto next assume ?l - { - fix x - assume x: "x \ s" have "x = {a}" - by (metis \s division_of cbox a a\ cbox_sing division_ofD(2) division_ofD(3) subset_singletonD x) - } + have "x = {a}" if "x \ s" for x + by (metis \s division_of cbox a a\ cbox_sing division_ofD(2) division_ofD(3) subset_singletonD that) moreover have "s \ {}" using \s division_of cbox a a\ by auto ultimately show ?r @@ -401,11 +381,8 @@ have *: "\s. \{x\s. x \ {}} = \s" by auto show "\?A = s1 \ s2" - apply (rule set_eqI) - unfolding * and UN_iff - using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)] - apply auto - done + unfolding * + using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)] by auto { fix k assume "k \ ?A" @@ -461,14 +438,14 @@ unfolding * by auto qed -lemma elementary_inter: +lemma elementary_Int: fixes s t :: "'a::euclidean_space set" assumes "p1 division_of s" and "p2 division_of t" shows "\p. p division_of (s \ t)" using assms division_inter by blast -lemma elementary_inters: +lemma elementary_Inter: assumes "finite f" and "f \ {}" and "\s\f. \p. p division_of (s::('a::euclidean_space) set)" @@ -488,7 +465,7 @@ moreover obtain px where "px division_of x" using insert(5)[rule_format,OF insertI1] .. ultimately show ?thesis - by (simp add: elementary_inter Inter_insert) + by (simp add: elementary_Int Inter_insert) qed qed auto @@ -548,13 +525,9 @@ show "cbox c d \ p" unfolding p_def by (auto simp add: box_eq_empty cbox_def intro!: image_eqI[where x="\(i::'a)\Basis. (c, d)"]) - { - fix i :: 'a - assume "i \ Basis" - with incl nonempty have "a \ i \ c \ i" "c \ i \ d \ i" "d \ i \ b \ i" - unfolding box_eq_empty subset_box by (auto simp: not_le) - } - note ord = this + have ord: "a \ i \ c \ i" "c \ i \ d \ i" "d \ i \ b \ i" if "i \ Basis" for i + using incl nonempty that + unfolding box_eq_empty subset_box by (auto simp: not_le) show "p division_of (cbox a b)" proof (rule division_ofI) @@ -665,8 +638,8 @@ then have di: "\x. x \ p \ \d. d division_of \(q x - {x})" by (meson Diff_subset division_of_subset) have "\d. d division_of \((\i. \(q i - {i})) ` p)" - apply (rule elementary_inters [OF finite_imageI[OF p(1)]]) - apply (auto dest: di simp: False elementary_inters [OF finite_imageI[OF p(1)]]) + apply (rule elementary_Inter [OF finite_imageI[OF p(1)]]) + apply (auto dest: di simp: False elementary_Inter [OF finite_imageI[OF p(1)]]) done then obtain d where d: "d division_of \((\i. \(q i - {i})) ` p)" .. have "d \ p division_of cbox a b" @@ -719,12 +692,7 @@ obtains p where "(insert (cbox a b) p) division_of (cbox a b \ cbox c d)" proof (cases "cbox c d = {}") case True - show ?thesis - apply (rule that[of "{}"]) - unfolding True - using assms - apply auto - done + with assms that show ?thesis by force next case False show ?thesis @@ -812,14 +780,13 @@ by auto show "finite ?D" using "*" pdiv(1) q(1) by auto - have lem1: "\f s. \\(f ` s) = \((\x. \(f x)) ` s)" - by auto - have lem2: "\f s. f \ {} \ \{s \ t |t. t \ f} = s \ \f" + have "\?D = (\x\p. \insert (cbox a b) (q x))" by auto - show "\?D = cbox a b \ \p" - unfolding * lem1 - unfolding lem2[OF \p \ {}\, of "cbox a b", symmetric] - using q(6) by auto + also have "... = \{cbox a b \ t |t. t \ p}" + using q(6) by auto + also have "... = cbox a b \ \p" + using \p \ {}\ by auto + finally show "\?D = cbox a b \ \p" . show "K \ cbox a b \ \p" "K \ {}" if "K \ ?D" for K using q that by blast+ show "\a b. K = cbox a b" if "K \ ?D" for K @@ -920,7 +887,7 @@ apply auto done then obtain r2 where r2: "r2 division_of (\(r1 - p)) \ (\q)" - by (metis assms(2) divq(6) elementary_inter) + by (metis assms(2) divq(6) elementary_Int) { fix x assume x: "x \ T" "x \ S" @@ -1130,9 +1097,8 @@ assumes "s tagged_partial_division_of i" and "t \ s" shows "t tagged_partial_division_of i" - using assms + using assms finite_subset[OF assms(2)] unfolding tagged_partial_division_of_def - using finite_subset[OF assms(2)] by blast lemma tag_in_interval: "p tagged_division_of i \ (x, k) \ p \ x \ i" @@ -1183,28 +1149,28 @@ qed lemma tagged_division_unions: - assumes "finite iset" - and "\i\iset. pfn i tagged_division_of i" - and "\i1\iset. \i2\iset. i1 \ i2 \ interior(i1) \ interior(i2) = {}" - shows "\(pfn ` iset) tagged_division_of (\iset)" + assumes "finite I" + and "\i\I. pfn i tagged_division_of i" + and "\i1\I. \i2\I. i1 \ i2 \ interior(i1) \ interior(i2) = {}" + shows "\(pfn ` I) tagged_division_of (\I)" proof (rule tagged_division_ofI) note assm = tagged_division_ofD[OF assms(2)[rule_format]] - show "finite (\(pfn ` iset))" + show "finite (\(pfn ` I))" using assms by auto - have "\{k. \x. (x, k) \ \(pfn ` iset)} = \((\i. \{k. \x. (x, k) \ pfn i}) ` iset)" + have "\{k. \x. (x, k) \ \(pfn ` I)} = \((\i. \{k. \x. (x, k) \ pfn i}) ` I)" by blast - also have "\ = \iset" + also have "\ = \I" using assm(6) by auto - finally show "\{k. \x. (x, k) \ \(pfn ` iset)} = \iset" . + finally show "\{k. \x. (x, k) \ \(pfn ` I)} = \I" . fix x k - assume xk: "(x, k) \ \(pfn ` iset)" - then obtain i where i: "i \ iset" "(x, k) \ pfn i" + assume xk: "(x, k) \ \(pfn ` I)" + then obtain i where i: "i \ I" "(x, k) \ pfn i" by auto - show "x \ k" "\a b. k = cbox a b" "k \ \iset" + show "x \ k" "\a b. k = cbox a b" "k \ \I" using assm(2-4)[OF i] using i(1) by auto fix x' k' - assume xk': "(x', k') \ \(pfn ` iset)" "(x, k) \ (x', k')" - then obtain i' where i': "i' \ iset" "(x', k') \ pfn i'" + assume xk': "(x', k') \ \(pfn ` I)" "(x, k) \ (x', k')" + then obtain i' where i': "i' \ I" "(x', k') \ pfn i'" by auto have *: "\a b. i \ i' \ a \ i \ b \ i' \ interior a \ interior b = {}" using i(1) i'(1) @@ -1379,8 +1345,8 @@ lemma division_points_psubset: fixes a :: "'a::euclidean_space" - assumes "d division_of (cbox a b)" - and "\i\Basis. a\i < b\i" "a\k < c" "c < b\k" + assumes d: "d division_of (cbox a b)" + and altb: "\i\Basis. a\i < b\i" "a\k < c" "c < b\k" and "l \ d" and disj: "interval_lowerbound l\k = c \ interval_upperbound l\k = c" and k: "k \ Basis" @@ -1390,14 +1356,12 @@ division_points (cbox a b) d" (is "?D2 \ ?D") proof - have ab: "\i\Basis. a\i \ b\i" - using assms(2) by (auto intro!:less_imp_le) - guess u v using division_ofD(4)[OF assms(1,5)] by (elim exE) note l=this + using altb by (auto intro!:less_imp_le) + obtain u v where l: "l = cbox u v" + using d \l \ d\ by blast have uv: "\i\Basis. u\i \ v\i" "\i\Basis. a\i \ u\i \ v\i \ b\i" - using division_ofD(2,2,3)[OF assms(1,5)] unfolding l box_ne_empty - using subset_box(1) - apply auto - apply blast+ - done + apply (metis assms(5) box_ne_empty(1) cbox_division_memE d l) + by (metis assms(5) box_ne_empty(1) cbox_division_memE d l subset_box(1)) have *: "interval_upperbound (cbox a b \ {x. x \ k \ interval_upperbound l \ k}) \ k = interval_upperbound l \ k" "interval_upperbound (cbox a b \ {x. x \ k \ interval_lowerbound l \ k}) \ k = interval_lowerbound l \ k" unfolding l interval_split[OF k] interval_bounds[OF uv(1)] @@ -1406,11 +1370,7 @@ have "\x. x \ ?D - ?D1" using assms(3-) unfolding division_points_def interval_bounds[OF ab] - apply - - apply (erule disjE) - apply (rule_tac x="(k,(interval_lowerbound l)\k)" in exI, force simp add: *) - apply (rule_tac x="(k,(interval_upperbound l)\k)" in exI, force simp add: *) - done + by (force simp add: *) moreover have "?D1 \ ?D" by (auto simp add: assms division_points_subset) ultimately show "?D1 \ ?D" @@ -1423,11 +1383,7 @@ have "\x. x \ ?D - ?D2" using assms(3-) unfolding division_points_def interval_bounds[OF ab] - apply - - apply (erule disjE) - apply (rule_tac x="(k,(interval_lowerbound l)\k)" in exI, force simp add: *) - apply (rule_tac x="(k,(interval_upperbound l)\k)" in exI, force simp add: *) - done + by (force simp add: *) moreover have "?D2 \ ?D" by (auto simp add: assms division_points_subset) ultimately show "?D2 \ ?D" @@ -1769,39 +1725,28 @@ done next fix a b c :: real - assume "\a b. b \ a \ g {a .. b} = \<^bold>1" - and "\a b c. a < c \ c < b \ g {a..c} \<^bold>* g {c..b} = g {a..b}" + assume eq1: "\a b. b \ a \ g {a .. b} = \<^bold>1" + and eqg: "\a b c. a < c \ c < b \ g {a..c} \<^bold>* g {c..b} = g {a..b}" and "a \ c" and "c \ b" - note as = this[rule_format] show "g {a..c} \<^bold>* g {c..b} = g {a..b}" proof (cases "c = a \ c = b") case False then show ?thesis - apply - - apply (subst as(2)) - using as(3-) - apply auto - done + using eqg \a \ c\ \c \ b\ by auto next case True then show ?thesis proof assume *: "c = a" then have "g {a .. c} = \<^bold>1" - apply - - apply (rule as(1)[rule_format]) - apply auto - done + using eq1 by blast then show ?thesis unfolding * by auto next assume *: "c = b" then have "g {c .. b} = \<^bold>1" - apply - - apply (rule as(1)[rule_format]) - apply auto - done + using eq1 by blast then show ?thesis unfolding * by auto qed @@ -1934,18 +1879,18 @@ subsection \Some basic combining lemmas.\ lemma tagged_division_Union_exists: - assumes "finite iset" - and "\i\iset. \p. p tagged_division_of i \ d fine p" - and "\i1\iset. \i2\iset. i1 \ i2 \ interior i1 \ interior i2 = {}" - and "\iset = i" + assumes "finite I" + and "\i\I. \p. p tagged_division_of i \ d fine p" + and "\i1\I. \i2\I. i1 \ i2 \ interior i1 \ interior i2 = {}" + and "\I = i" obtains p where "p tagged_division_of i" and "d fine p" proof - obtain pfn where pfn: - "\x. x \ iset \ pfn x tagged_division_of x" - "\x. x \ iset \ d fine pfn x" + "\x. x \ I \ pfn x tagged_division_of x" + "\x. x \ I \ d fine pfn x" using bchoice[OF assms(2)] by auto show thesis - apply (rule_tac p="\(pfn ` iset)" in that) + apply (rule_tac p="\(pfn ` I)" in that) using assms(1) assms(3) assms(4) pfn(1) tagged_division_unions apply force by (metis (mono_tags, lifting) fine_Union imageE pfn(2)) qed @@ -1972,25 +1917,22 @@ using assms(1,3) by metis then have ab: "\i. i\Basis \ a \ i \ b \ i" by (force simp: mem_box) - { fix f - have "\finite f; + have UN_cases: "\finite f; \s. s\f \ P s; \s. s\f \ \a b. s = cbox a b; - \s t. s\f \ t\f \ s \ t \ interior s \ interior t = {}\ \ P (\f)" - proof (induct f rule: finite_induct) - case empty - show ?case - using assms(1) by auto - next - case (insert x f) - show ?case - unfolding Union_insert - apply (rule assms(2)[rule_format]) - using Int_interior_Union_intervals [of f "interior x"] - apply (auto simp: insert) - by (metis IntI empty_iff insert.hyps(2) insert.prems(3) insert_iff) - qed - } note UN_cases = this + \s t. s\f \ t\f \ s \ t \ interior s \ interior t = {}\ \ P (\f)" for f + proof (induct f rule: finite_induct) + case empty + show ?case + using assms(1) by auto + next + case (insert x f) + show ?case + unfolding Union_insert + apply (rule assms(2)[rule_format]) + using Int_interior_Union_intervals [of f "interior x"] + by (metis (no_types, lifting) insert insert_iff open_interior) + qed let ?A = "{cbox c d | c d::'a. \i\Basis. (c\i = a\i) \ (d\i = (a\i + b\i) / 2) \ (c\i = (a\i + b\i) / 2) \ (d\i = b\i)}" let ?PP = "\c d. \i\Basis. a\i \ c\i \ c\i \ d\i \ d\i \ b\i \ 2 * (d\i - c\i) \ b\i - a\i" @@ -2110,13 +2052,12 @@ then show "\c d. ?P i c d" by blast qed + then obtain \ \ where + "\i\Basis. (\ \ i = a \ i \ \ \ i = (a \ i + b \ i) / 2 \ + \ \ i = (a \ i + b \ i) / 2 \ \ \ i = b \ i) \ \ \ i \ x \ i \ x \ i \ \ \ i" + by (auto simp: choice_Basis_iff) then show "x\\?A" - unfolding Union_iff Bex_def mem_Collect_eq choice_Basis_iff - apply auto - apply (rule_tac x="cbox xa xaa" in exI) - unfolding mem_box - apply auto - done + by (force simp add: mem_box) qed finally show False using assms by auto @@ -2148,10 +2089,7 @@ 2 * (d \ i - c \ i) \ snd x \ i - fst x \ i" by (rule interval_bisection_step[of P, OF assms(1-2) as]) then show ?thesis - apply - - apply (rule_tac x="(c,d)" in exI) - apply auto - done + by (rule_tac x="(c,d)" in exI) auto qed qed then obtain f where f: @@ -2162,11 +2100,7 @@ fst x \ i \ fst (f x) \ i \ fst (f x) \ i \ snd (f x) \ i \ snd (f x) \ i \ snd x \ i \ - 2 * (snd (f x) \ i - fst (f x) \ i) \ snd x \ i - fst x \ i)" - apply - - apply (drule choice) - apply blast - done + 2 * (snd (f x) \ i - fst (f x) \ i) \ snd x \ i - fst x \ i)" by metis define AB A B where ab_def: "AB n = (f ^^ n) (a,b)" "A n = fst(AB n)" "B n = snd(AB n)" for n have [simp]: "A 0 = a" "B 0 = b" and ABRAW: "\n. \ P (cbox (A(Suc n)) (B(Suc n))) \ (\i\Basis. A(n)\i \ A(Suc n)\i \ A(Suc n)\i \ B(Suc n)\i \ B(Suc n)\i \ B(n)\i \ @@ -2179,10 +2113,7 @@ proof (induct n) case 0 then show ?case - unfolding S - apply (rule f[rule_format]) using assms(3) - apply auto - done + unfolding S using \\ P (cbox a b)\ f by auto next case (Suc n) show ?case @@ -2230,8 +2161,7 @@ next case (Suc n) have "B (Suc n) \ i - A (Suc n) \ i \ (B n \ i - A n \ i) / 2" - using AB(3) that - using AB(4)[of i n] using i by auto + using AB(3) that AB(4)[of i n] using i by auto also have "\ \ (b \ i - a \ i) / 2 ^ Suc n" using Suc by (auto simp add: field_simps) finally show ?case . @@ -2295,13 +2225,13 @@ fixes a b :: "'a::euclidean_space" assumes "gauge g" obtains p where "p tagged_division_of (cbox a b)" "g fine p" -proof - - presume "\ (\p. p tagged_division_of (cbox a b) \ g fine p) \ False" - then obtain p where "p tagged_division_of (cbox a b)" "g fine p" - by blast - then show thesis .. +proof (cases "\p. p tagged_division_of (cbox a b) \ g fine p") + case True + then show ?thesis + using that by auto next - assume as: "\ (\p. p tagged_division_of (cbox a b) \ g fine p)" + case False + assume "\ (\p. p tagged_division_of (cbox a b) \ g fine p)" obtain x where x: "x \ (cbox a b)" "\e. 0 < e \ @@ -2310,10 +2240,10 @@ cbox c d \ ball x e \ cbox c d \ (cbox a b) \ \ (\p. p tagged_division_of cbox c d \ g fine p)" - apply (rule interval_bisection[of "\s. \p. p tagged_division_of s \ g fine p", OF _ _ as]) + apply (rule interval_bisection[of "\s. \p. p tagged_division_of s \ g fine p", OF _ _ False]) apply (simp add: fine_def) apply (metis tagged_division_union fine_Un) - apply (auto simp: ) + apply auto done obtain e where e: "e > 0" "ball x e \ g x" using gaugeD[OF assms, of x] unfolding open_contains_ball by auto @@ -2325,7 +2255,7 @@ by blast have "g fine {(x, cbox c d)}" unfolding fine_def using e using c_d(2) by auto - then show False + then show ?thesis using tagged_division_of_self[OF c_d(1)] using c_d by auto qed @@ -2369,70 +2299,52 @@ proof (induct p) case empty show ?case - apply (rule_tac x="{}" in exI) - unfolding fine_def - apply auto - done + by (force simp add: fine_def) next case (insert xk p) - guess x k using surj_pair[of xk] by (elim exE) note xk=this - note tagged_partial_division_subset[OF insert(4) subset_insertI] - from insert(3)[OF this insert(5)] + obtain x k where xk: "xk = (x, k)" + using surj_pair[of xk] by metis obtain q1 where q1: "q1 tagged_division_of \{k. \x. (x, k) \ p}" and "d fine q1" and q1I: "\x k. \(x, k)\p; k \ d x\ \ (x, k) \ q1" - by (force simp add: ) + using case_prodD tagged_partial_division_subset[OF insert(4) subset_insertI] + by (metis (mono_tags, lifting) insert.hyps(3) insert.prems(2)) have *: "\{l. \y. (y,l) \ insert xk p} = k \ \{l. \y. (y,l) \ p}" unfolding xk by auto note p = tagged_partial_division_ofD[OF insert(4)] - from p(4)[unfolded xk, OF insertI1] guess u v by (elim exE) note uv=this - + obtain u v where uv: "k = cbox u v" + using p(4)[unfolded xk, OF insertI1] by blast have "finite {k. \x. (x, k) \ p}" apply (rule finite_subset[of _ "snd ` p"]) - using p - apply safe - apply (metis image_iff snd_conv) - apply auto - done + using image_iff apply fastforce + using insert.hyps(1) by blast then have int: "interior (cbox u v) \ interior (\{k. \x. (x, k) \ p}) = {}" - apply (rule Int_interior_Union_intervals) - apply (rule open_interior) - unfolding mem_Collect_eq - apply (erule_tac[!] exE) - apply (drule p(4)[OF insertI2]) - apply assumption - apply (rule p(5)) - unfolding uv xk - apply (rule insertI1) - apply (rule insertI2) - apply assumption - using insert(2) - unfolding uv xk - apply auto - done + proof (rule Int_interior_Union_intervals) + show "open (interior (cbox u v))" + by auto + show "\T. T \ {k. \x. (x, k) \ p} \ \a b. T = cbox a b" + using p(4) by auto + show "\T. T \ {k. \x. (x, k) \ p} \ interior (cbox u v) \ interior T = {}" + by clarify (metis insert.hyps(2) insert_iff interior_cbox p(5) uv xk) + qed show ?case proof (cases "cbox u v \ d x") case True - then show ?thesis + have "{(x, cbox u v)} tagged_division_of cbox u v" + by (simp add: p(2) uv xk tagged_division_of_self) + then have "{(x, cbox u v)} \ q1 tagged_division_of \{k. \x. (x, k) \ insert xk p}" + unfolding * uv by (metis (no_types, lifting) int q1 tagged_division_union) + with True show ?thesis apply (rule_tac x="{(x,cbox u v)} \ q1" in exI) - apply rule - unfolding * uv - apply (rule tagged_division_union) - apply (rule tagged_division_of_self) - apply (rule p[unfolded xk uv] insertI1)+ - apply (rule q1) - apply (rule int) - apply rule - apply (rule fine_Un) - apply (subst fine_def) - apply (auto simp add: \d fine q1\ q1I uv xk) + using \d fine q1\ fine_def q1I uv xk apply fastforce done next case False - from fine_division_exists[OF assms(2), of u v] guess q2 . note q2=this + obtain q2 where q2: "q2 tagged_division_of cbox u v" "d fine q2" + using fine_division_exists[OF assms(2)] by blast show ?thesis apply (rule_tac x="q2 \ q1" in exI) - apply rule + apply (intro conjI) unfolding * uv apply (rule tagged_division_union q2 q1 int fine_Un)+ apply (auto intro: q1 q2 fine_Un \d fine q1\ simp add: False q1I uv xk) diff -r 56f8bfe1211c -r 1f66c7d77002 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Thu Aug 03 13:35:28 2017 +0200 +++ b/src/HOL/Library/Multiset.thy Fri Aug 04 18:03:50 2017 +0200 @@ -3458,8 +3458,7 @@ end -lemma [code]: "sum_mset (mset xs) = sum_list xs" - by (induct xs) simp_all +declare sum_mset_sum_list [code] lemma [code]: "prod_mset (mset xs) = fold times xs 1" proof - diff -r 56f8bfe1211c -r 1f66c7d77002 src/HOL/SMT.thy --- a/src/HOL/SMT.thy Thu Aug 03 13:35:28 2017 +0200 +++ b/src/HOL/SMT.thy Fri Aug 04 18:03:50 2017 +0200 @@ -246,7 +246,7 @@ \ declare [[cvc3_options = ""]] -declare [[cvc4_options = "--full-saturate-quant --inst-when=full-last-call --inst-no-entail --term-db-mode=relevant"]] +declare [[cvc4_options = "--full-saturate-quant --inst-when=full-last-call --inst-no-entail --term-db-mode=relevant --multi-trigger-linear"]] declare [[verit_options = ""]] declare [[z3_options = ""]] diff -r 56f8bfe1211c -r 1f66c7d77002 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Thu Aug 03 13:35:28 2017 +0200 +++ b/src/HOL/Statespace/state_space.ML Fri Aug 04 18:03:50 2017 +0200 @@ -298,7 +298,7 @@ fun add_declaration name decl thy = thy - |> Named_Target.init NONE name + |> Named_Target.init name |> (fn lthy => Local_Theory.declaration {syntax = false, pervasive = false} (decl lthy) lthy) |> Local_Theory.exit_global; diff -r 56f8bfe1211c -r 1f66c7d77002 src/HOL/String.thy --- a/src/HOL/String.thy Thu Aug 03 13:35:28 2017 +0200 +++ b/src/HOL/String.thy Fri Aug 04 18:03:50 2017 +0200 @@ -16,6 +16,8 @@ show "Suc 0 \ {n. n < 256}" by simp qed +setup_lifting type_definition_char + definition char_of_nat :: "nat \ char" where "char_of_nat n = Abs_char (n mod 256)" @@ -304,6 +306,9 @@ "char_of_integer n = Enum.enum ! (nat_of_integer n mod 256)" by (simp add: char_of_integer_def enum_char_unfold) +lifting_update char.lifting +lifting_forget char.lifting + subsection \Strings as dedicated type\ diff -r 56f8bfe1211c -r 1f66c7d77002 src/HOL/Tools/code_evaluation.ML --- a/src/HOL/Tools/code_evaluation.ML Thu Aug 03 13:35:28 2017 +0200 +++ b/src/HOL/Tools/code_evaluation.ML Fri Aug 04 18:03:50 2017 +0200 @@ -20,8 +20,9 @@ (* formal definition *) -fun add_term_of tyco raw_vs thy = +fun add_term_of_inst tyco thy = let + val ((raw_vs, _), _) = Code.get_type thy tyco; val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs; val ty = Type (tyco, map TFree vs); val lhs = Const (@{const_name term_of}, ty --> @{typ term}) @@ -39,11 +40,11 @@ |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt []) end; -fun ensure_term_of (tyco, (vs, _)) thy = +fun ensure_term_of_inst tyco thy = let val need_inst = not (Sorts.has_instance (Sign.classes_of thy) tyco @{sort term_of}) andalso Sorts.has_instance (Sign.classes_of thy) tyco @{sort typerep}; - in if need_inst then add_term_of tyco vs thy else thy end; + in if need_inst then add_term_of_inst tyco thy else thy end; fun for_term_of_instance tyco vs f thy = let @@ -74,20 +75,19 @@ |> Thm.varifyT_global end; -fun add_term_of_code tyco vs raw_cs thy = +fun add_term_of_code_datatype tyco vs raw_cs thy = let val ty = Type (tyco, map TFree vs); val cs = (map o apsnd o apsnd o map o map_atyps) (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs; - val const = Axclass.param_of_inst thy (@{const_name term_of}, tyco); val eqs = map (mk_term_of_eq thy ty) cs; in thy |> Code.declare_default_eqns_global (map (rpair true) eqs) end; -fun ensure_term_of_code (tyco, (vs, cs)) = - for_term_of_instance tyco vs (fn tyco => fn vs => add_term_of_code tyco vs cs); +fun ensure_term_of_code_datatype (tyco, (vs, cs)) = + for_term_of_instance tyco vs (fn tyco => fn vs => add_term_of_code_datatype tyco vs cs); (* code equations for abstypes *) @@ -105,31 +105,29 @@ |> Thm.varifyT_global end; -fun add_abs_term_of_code tyco vs abs raw_ty_rep proj thy = +fun add_term_of_code_abstype tyco vs abs raw_ty_rep projection thy = let val ty = Type (tyco, map TFree vs); val ty_rep = map_atyps (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_ty_rep; - val const = Axclass.param_of_inst thy (@{const_name term_of}, tyco); - val eq = mk_abs_term_of_eq thy ty abs ty_rep proj; + val eq = mk_abs_term_of_eq thy ty abs ty_rep projection; in thy |> Code.declare_default_eqns_global [(eq, true)] end; -fun ensure_abs_term_of_code (tyco, (vs, {abstractor = (abs, (_, ty)), +fun ensure_term_of_code_abstype (tyco, (vs, {abstractor = (abs, (_, ty)), projection, ...})) = for_term_of_instance tyco vs - (fn tyco => fn vs => add_abs_term_of_code tyco vs abs ty projection); + (fn tyco => fn vs => add_term_of_code_abstype tyco vs abs ty projection); (* setup *) val _ = Theory.setup - (Code.datatype_interpretation ensure_term_of - #> Code.abstype_interpretation ensure_term_of - #> Code.datatype_interpretation ensure_term_of_code - #> Code.abstype_interpretation ensure_abs_term_of_code); + (Code.type_interpretation ensure_term_of_inst + #> Code.datatype_interpretation ensure_term_of_code_datatype + #> Code.abstype_interpretation ensure_term_of_code_abstype); (** termifying syntax **) diff -r 56f8bfe1211c -r 1f66c7d77002 src/HOL/Typerep.thy --- a/src/HOL/Typerep.thy Thu Aug 03 13:35:28 2017 +0200 +++ b/src/HOL/Typerep.thy Fri Aug 04 18:03:50 2017 +0200 @@ -72,8 +72,7 @@ add_typerep @{type_name fun} #> Typedef.interpretation (Local_Theory.background_theory o ensure_typerep) -#> Code.datatype_interpretation (ensure_typerep o fst) -#> Code.abstype_interpretation (ensure_typerep o fst) +#> Code.type_interpretation ensure_typerep end \ diff -r 56f8bfe1211c -r 1f66c7d77002 src/Pure/Isar/bundle.ML --- a/src/Pure/Isar/bundle.ML Thu Aug 03 13:35:28 2017 +0200 +++ b/src/Pure/Isar/bundle.ML Fri Aug 04 18:03:50 2017 +0200 @@ -175,18 +175,17 @@ fun init binding thy = thy - |> Sign.change_begin - |> set_target [] - |> Proof_Context.init_global - |> Local_Theory.init (Sign.naming_of thy) + |> Generic_Target.init + {background_naming = Sign.naming_of thy, + setup = set_target [] #> Proof_Context.init_global, + conclude = conclude false binding #> #2} {define = bad_operation, notes = bundle_notes, abbrev = bad_operation, declaration = K bundle_declaration, theory_registration = bad_operation, locale_dependency = bad_operation, - pretty = pretty binding, - exit = conclude false binding #> #2 #> Local_Theory.target_of #> Sign.change_end_local} + pretty = pretty binding} end; @@ -216,7 +215,8 @@ |> prep_decl ([], []) I raw_elems; in lthy' |> Local_Theory.init_target - (Local_Theory.background_naming_of lthy) (Local_Theory.operations_of lthy) after_close + {background_naming = Local_Theory.background_naming_of lthy, after_close = after_close} + (Local_Theory.operations_of lthy) end; in diff -r 56f8bfe1211c -r 1f66c7d77002 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Thu Aug 03 13:35:28 2017 +0200 +++ b/src/Pure/Isar/class.ML Fri Aug 04 18:03:50 2017 +0200 @@ -683,26 +683,26 @@ | NONE => NONE); in thy - |> Sign.change_begin - |> Proof_Context.init_global - |> Instantiation.put (make_instantiation ((tycos, vs, sort), params)) - |> fold (Variable.declare_typ o TFree) vs - |> fold (Variable.declare_names o Free o snd) params - |> (Overloading.map_improvable_syntax) (K {primary_constraints = primary_constraints, - secondary_constraints = [], improve = improve, subst = K NONE, - no_subst_in_abbrev_mode = false, unchecks = []}) - |> Overloading.activate_improvable_syntax - |> Context.proof_map (Syntax_Phases.term_check 0 "resorting" resort_check) - |> synchronize_inst_syntax - |> Local_Theory.init (Sign.naming_of thy) + |> Generic_Target.init + {background_naming = Sign.naming_of thy, + setup = Proof_Context.init_global + #> Instantiation.put (make_instantiation ((tycos, vs, sort), params)) + #> fold (Variable.declare_typ o TFree) vs + #> fold (Variable.declare_names o Free o snd) params + #> (Overloading.map_improvable_syntax) (K {primary_constraints = primary_constraints, + secondary_constraints = [], improve = improve, subst = K NONE, + no_subst_in_abbrev_mode = false, unchecks = []}) + #> Overloading.activate_improvable_syntax + #> Context.proof_map (Syntax_Phases.term_check 0 "resorting" resort_check) + #> synchronize_inst_syntax, + conclude = conclude} {define = Generic_Target.define foundation, notes = Generic_Target.notes Generic_Target.theory_target_notes, abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev, declaration = K Generic_Target.theory_declaration, theory_registration = Generic_Target.theory_registration, locale_dependency = fn _ => error "Not possible in instantiation target", - pretty = pretty, - exit = conclude #> Local_Theory.target_of #> Sign.change_end_local} + pretty = pretty} end; fun instantiation_cmd arities thy = diff -r 56f8bfe1211c -r 1f66c7d77002 src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML Thu Aug 03 13:35:28 2017 +0200 +++ b/src/Pure/Isar/class_declaration.ML Fri Aug 04 18:03:50 2017 +0200 @@ -327,7 +327,7 @@ #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class #> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class))) |> snd - |> Named_Target.init NONE class + |> Named_Target.init class |> pair class end; diff -r 56f8bfe1211c -r 1f66c7d77002 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Thu Aug 03 13:35:28 2017 +0200 +++ b/src/Pure/Isar/code.ML Fri Aug 04 18:03:50 2017 +0200 @@ -30,16 +30,15 @@ val pretty_cert: theory -> cert -> Pretty.T list (*executable code*) + type constructors + type abs_type + val type_interpretation: (string -> theory -> theory) -> theory -> theory + val datatype_interpretation: (string * constructors -> theory -> theory) -> theory -> theory + val abstype_interpretation: (string * abs_type -> theory -> theory) -> theory -> theory val declare_datatype_global: (string * typ) list -> theory -> theory val declare_datatype_cmd: string list -> theory -> theory - val datatype_interpretation: - (string * ((string * sort) list * (string * ((string * sort) list * typ list)) list) - -> theory -> theory) -> theory -> theory val declare_abstype: thm -> local_theory -> local_theory val declare_abstype_global: thm -> theory -> theory - val abstype_interpretation: - (string * ((string * sort) list * {abs_rep: thm, abstractor: string * ((string * sort) list * typ), - projection: string}) -> theory -> theory) -> theory -> theory val declare_default_eqns: (thm * bool) list -> local_theory -> local_theory val declare_default_eqns_global: (thm * bool) list -> theory -> theory val declare_eqns: (thm * bool) list -> local_theory -> local_theory @@ -52,8 +51,7 @@ val declare_unimplemented_global: string -> theory -> theory val declare_case_global: thm -> theory -> theory val declare_undefined_global: string -> theory -> theory - val get_type: theory -> string - -> ((string * sort) list * (string * ((string * sort) list * typ list)) list) * bool + val get_type: theory -> string -> constructors * bool val get_type_of_constr_or_abstr: theory -> string -> (string * bool) option val is_constr: theory -> string -> bool val is_abstr: theory -> string -> bool @@ -277,9 +275,6 @@ local -fun tap_serial (table : 'a T) key = - Option.map (hd o #history) (Symtab.lookup table key); - fun merge_history join_same ({entry = entry1, history = history1, ...}, {entry = entry2, history = history2, ...}) = let @@ -338,7 +333,7 @@ NONE => false | SOME (_, Abstractor {abstractor = (abs', _), projection, more_abstract_functions, ...}) => abs = abs' andalso (c = projection orelse member (op =) more_abstract_functions c)); - fun check_datatypes (c, case_spec) = + fun check_datatypes (_, case_spec) = let val (tycos, required_constructors) = associated_datatypes case_spec; val allowed_constructors = @@ -348,10 +343,6 @@ in subset (op =) (required_constructors, allowed_constructors) end; val all_constructors = maps (fst o constructors_of) all_types; - val all_abstract_functions = - maps abstract_functions_of all_types; - val case_combinators = - maps case_combinators_of all_types; val functions = History.join fst (functions1, functions2) |> fold (History.suppress o fst) all_constructors |> History.suppress_except check_abstype; @@ -552,6 +543,9 @@ fun lookup_vs_type_spec thy = History.lookup ((types_of o specs_of) thy); +type constructors = + (string * sort) list * (string * ((string * sort) list * typ list)) list; + fun get_type thy tyco = case lookup_vs_type_spec thy tyco of SOME (vs, type_spec) => apfst (pair vs) (constructors_of type_spec) | NONE => Sign.arity_number thy tyco @@ -560,6 +554,9 @@ |> rpair [] |> rpair false; +type abs_type = + (string * sort) list * {abs_rep: thm, abstractor: string * ((string * sort) list * typ), projection: string}; + fun get_abstype_spec thy tyco = case lookup_vs_type_spec thy tyco of SOME (vs, Abstractor {abs_rep, abstractor, projection, ...}) => (vs, {abs_rep = abs_rep, abstractor = abstractor, projection = projection}) @@ -1003,7 +1000,7 @@ Nothing (constrain_cert_thm thy sorts cert_thm) | constrain_cert thy sorts (Equations (cert_thm, propers)) = Equations (constrain_cert_thm thy sorts cert_thm, propers) - | constrain_cert thy _ (cert as Projection _) = + | constrain_cert _ _ (cert as Projection _) = cert | constrain_cert thy sorts (Abstract (abs_thm, tyco)) = Abstract (snd (constrain_thm thy (fst (typscheme_abs thy abs_thm)) sorts abs_thm), tyco); @@ -1074,8 +1071,8 @@ (SOME (Thm.varifyT_global abs_thm), true))]) end; -fun pretty_cert thy (cert as Nothing _) = - [Pretty.str "(unimplemented)"] +fun pretty_cert _ (Nothing _) = + [] | pretty_cert thy (cert as Equations _) = (map_filter (Option.map (Thm.pretty_thm_global thy o @@ -1263,6 +1260,40 @@ (** declaration of executable ingredients **) +(* plugins for dependent applications *) + +structure Codetype_Plugin = Plugin(type T = string); + +val codetype_plugin = Plugin_Name.declare_setup @{binding codetype}; + +fun type_interpretation f = + Codetype_Plugin.interpretation codetype_plugin + (fn tyco => Local_Theory.background_theory + (fn thy => + thy + |> Sign.root_path + |> Sign.add_path (Long_Name.qualifier tyco) + |> f tyco + |> Sign.restore_naming thy)); + +fun datatype_interpretation f = + type_interpretation (fn tyco => fn thy => + case get_type thy tyco of + (spec, false) => f (tyco, spec) thy + | (_, true) => thy + ); + +fun abstype_interpretation f = + type_interpretation (fn tyco => fn thy => + case try (get_abstype_spec thy) tyco of + SOME spec => f (tyco, spec) thy + | NONE => thy + ); + +fun register_tyco_for_plugin tyco = + Named_Target.theory_map (Codetype_Plugin.data_default tyco); + + (* abstract code declarations *) local @@ -1302,19 +1333,6 @@ |> map_types (History.register tyco vs_typ_spec) end; -structure Datatype_Plugin = Plugin(type T = string); - -val datatype_plugin = Plugin_Name.declare_setup @{binding datatype_code}; - -fun datatype_interpretation f = - Datatype_Plugin.interpretation datatype_plugin - (fn tyco => Local_Theory.background_theory (fn thy => - thy - |> Sign.root_path - |> Sign.add_path (Long_Name.qualifier tyco) - |> f (tyco, fst (get_type thy tyco)) - |> Sign.restore_naming thy)); - fun declare_datatype_global proto_constrs thy = let fun unoverload_const_typ (c, ty) = @@ -1325,21 +1343,12 @@ thy |> modify_specs (register_type (tyco, (vs, Constructors {constructors = cos, case_combinators = []}))) - |> Named_Target.theory_map (Datatype_Plugin.data_default tyco) + |> register_tyco_for_plugin tyco end; fun declare_datatype_cmd raw_constrs thy = declare_datatype_global (map (read_bare_const thy) raw_constrs) thy; -structure Abstype_Plugin = Plugin(type T = string); - -val abstype_plugin = Plugin_Name.declare_setup @{binding abstype_code}; - -fun abstype_interpretation f = - Abstype_Plugin.interpretation abstype_plugin - (fn tyco => - Local_Theory.background_theory (fn thy => f (tyco, get_abstype_spec thy tyco) thy)); - fun generic_declare_abstype strictness proto_thm thy = case check_abstype_cert strictness thy proto_thm of SOME (tyco, (vs, (abstractor as (abs, (_, ty)), (proj, abs_rep)))) => @@ -1348,7 +1357,7 @@ (tyco, (vs, Abstractor {abstractor = abstractor, projection = proj, abs_rep = abs_rep, more_abstract_functions = []})) #> register_fun_spec proj (Proj (Logic.varify_types_global (mk_proj tyco vs ty abs proj), (tyco, abs)))) - |> Named_Target.theory_map (Abstype_Plugin.data_default tyco) + |> register_tyco_for_plugin tyco | NONE => thy; val declare_abstype_global = generic_declare_abstype Strict; diff -r 56f8bfe1211c -r 1f66c7d77002 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Thu Aug 03 13:35:28 2017 +0200 +++ b/src/Pure/Isar/expression.ML Fri Aug 04 18:03:50 2017 +0200 @@ -825,7 +825,7 @@ val loc_ctxt = thy' |> Locale.register_locale binding (extraTs, params) (asm, rev defs) (a_intro, b_intro) axioms hyp_spec [] (rev notes) (rev deps') - |> Named_Target.init NONE name + |> Named_Target.init name |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes'; in (name, loc_ctxt) end; diff -r 56f8bfe1211c -r 1f66c7d77002 src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Thu Aug 03 13:35:28 2017 +0200 +++ b/src/Pure/Isar/generic_target.ML Fri Aug 04 18:03:50 2017 +0200 @@ -76,6 +76,11 @@ local_theory -> local_theory val locale_dependency: string -> string * morphism -> (morphism * bool) option -> morphism -> local_theory -> local_theory + + (*initialisation*) + val init: {background_naming: Name_Space.naming, setup: theory -> Proof.context, + conclude: local_theory -> local_theory} -> + Local_Theory.operations -> theory -> local_theory end structure Generic_Target: GENERIC_TARGET = @@ -417,4 +422,16 @@ fun locale_abbrev locale = abbrev (locale_target_abbrev locale); + +(** initialisation **) + +fun init {background_naming, setup, conclude} operations thy = + thy + |> Sign.change_begin + |> setup + |> Local_Theory.init + {background_naming = background_naming, + exit = conclude #> Local_Theory.target_of #> Sign.change_end_local} + operations; + end; diff -r 56f8bfe1211c -r 1f66c7d77002 src/Pure/Isar/interpretation.ML --- a/src/Pure/Isar/interpretation.ML Thu Aug 03 13:35:28 2017 +0200 +++ b/src/Pure/Isar/interpretation.ML Fri Aug 04 18:03:50 2017 +0200 @@ -220,7 +220,7 @@ fun gen_global_sublocale prep_loc prep_interpretation raw_locale expression raw_defs raw_eqns thy = let - val lthy = Named_Target.init NONE (prep_loc thy raw_locale) thy; + val lthy = Named_Target.init (prep_loc thy raw_locale) thy; fun setup_proof after_qed = Element.witness_proof_eqs (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit); diff -r 56f8bfe1211c -r 1f66c7d77002 src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Thu Aug 03 13:35:28 2017 +0200 +++ b/src/Pure/Isar/local_theory.ML Fri Aug 04 18:03:50 2017 +0200 @@ -65,13 +65,14 @@ val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory val type_alias: binding -> string -> local_theory -> local_theory val const_alias: binding -> string -> local_theory -> local_theory - val init: Name_Space.naming -> operations -> Proof.context -> local_theory + val init: {background_naming: Name_Space.naming, exit: local_theory -> Proof.context} -> + operations -> Proof.context -> local_theory val exit: local_theory -> Proof.context val exit_global: local_theory -> theory val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory - val init_target: Name_Space.naming -> operations -> (local_theory -> local_theory) -> - local_theory -> Binding.scope * local_theory + val init_target: {background_naming: Name_Space.naming, after_close: local_theory -> local_theory} -> + operations -> local_theory -> Binding.scope * local_theory val open_target: local_theory -> Binding.scope * local_theory val close_target: local_theory -> local_theory end; @@ -95,19 +96,19 @@ local_theory -> local_theory, locale_dependency: string * morphism -> (morphism * bool) option -> morphism -> local_theory -> local_theory, - pretty: local_theory -> Pretty.T list, - exit: local_theory -> Proof.context}; + pretty: local_theory -> Pretty.T list}; type lthy = {background_naming: Name_Space.naming, operations: operations, after_close: local_theory -> local_theory, + exit: local_theory -> Proof.context, brittle: bool, target: Proof.context}; -fun make_lthy (background_naming, operations, after_close, brittle, target) : lthy = +fun make_lthy (background_naming, operations, after_close, exit, brittle, target) : lthy = {background_naming = background_naming, operations = operations, - after_close = after_close, brittle = brittle, target = target}; + after_close = after_close, exit = exit, brittle = brittle, target = target}; (* context data *) @@ -146,16 +147,16 @@ fun map_top f = assert #> - Data.map (fn {background_naming, operations, after_close, brittle, target} :: parents => - make_lthy (f (background_naming, operations, after_close, brittle, target)) :: parents); + Data.map (fn {background_naming, operations, after_close, exit, brittle, target} :: parents => + make_lthy (f (background_naming, operations, after_close, exit, brittle, target)) :: parents); fun reset lthy = #target (top_of lthy) |> Data.put (Data.get lthy); fun map_contexts f lthy = let val n = level lthy in lthy |> (Data.map o map_index) - (fn (i, {background_naming, operations, after_close, brittle, target}) => - make_lthy (background_naming, operations, after_close, brittle, + (fn (i, {background_naming, operations, after_close, exit, brittle, target}) => + make_lthy (background_naming, operations, after_close, exit, brittle, target |> Context_Position.set_visible false |> f (n - i - 1) @@ -168,8 +169,8 @@ fun mark_brittle lthy = if level lthy = 1 then - map_top (fn (background_naming, operations, after_close, _, target) => - (background_naming, operations, after_close, true, target)) lthy + map_top (fn (background_naming, operations, after_close, exit, _, target) => + (background_naming, operations, after_close, exit, true, target)) lthy else lthy; fun assert_nonbrittle lthy = @@ -182,8 +183,8 @@ val background_naming_of = #background_naming o top_of; fun map_background_naming f = - map_top (fn (background_naming, operations, after_close, brittle, target) => - (f background_naming, operations, after_close, brittle, target)); + map_top (fn (background_naming, operations, after_close, exit, brittle, target) => + (f background_naming, operations, after_close, exit, brittle, target)); val restore_background_naming = map_background_naming o K o background_naming_of; @@ -348,12 +349,14 @@ (* outermost target *) -fun init background_naming operations target = +fun init {background_naming, exit} operations target = target |> Data.map - (fn [] => [make_lthy (background_naming, operations, I, false, target)] + (fn [] => [make_lthy (background_naming, operations, I, exit, false, target)] | _ => error "Local theory already initialized"); -val exit = operation #exit; +val exit_of = #exit o bottom_of; + +fun exit lthy = exit_of lthy lthy; val exit_global = Proof_Context.theory_of o exit; fun exit_result f (x, lthy) = @@ -372,18 +375,19 @@ (* nested targets *) -fun init_target background_naming operations after_close lthy = +fun init_target {background_naming, after_close} operations lthy = let val _ = assert lthy; val after_close' = Proof_Context.restore_naming lthy #> after_close; val (scope, target) = Proof_Context.new_scope lthy; val lthy' = target - |> Data.map (cons (make_lthy (background_naming, operations, after_close', true, target))); + |> Data.map (cons (make_lthy (background_naming, operations, after_close', exit_of lthy, true, target))); in (scope, lthy') end; fun open_target lthy = - init_target (background_naming_of lthy) (operations_of lthy) I lthy; + init_target {background_naming = background_naming_of lthy, after_close = I} + (operations_of lthy) lthy; fun close_target lthy = let diff -r 56f8bfe1211c -r 1f66c7d77002 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Thu Aug 03 13:35:28 2017 +0200 +++ b/src/Pure/Isar/locale.ML Fri Aug 04 18:03:50 2017 +0200 @@ -88,6 +88,7 @@ val print_locale: theory -> bool -> xstring * Position.T -> unit val print_registrations: Proof.context -> xstring * Position.T -> unit val print_dependencies: Proof.context -> bool -> morphism -> (string * morphism) list -> unit + val pretty_locale: theory -> bool -> string -> Pretty.T list val pretty_locale_deps: theory -> {name: string, parents: string list, body: Pretty.T} list end; @@ -699,13 +700,12 @@ activate_all name thy cons_elem (K (Morphism.transfer_morphism thy)) (empty_idents, []) |> snd |> rev; in - Pretty.block - (Pretty.keyword1 "locale" :: Pretty.brk 1 :: pretty_name locale_ctxt name :: - maps (fn elem => [Pretty.fbrk, Pretty.chunks (Element.pretty_ctxt locale_ctxt elem)]) elems) + Pretty.keyword1 "locale" :: Pretty.brk 1 :: pretty_name locale_ctxt name :: + maps (fn elem => [Pretty.fbrk, Pretty.chunks (Element.pretty_ctxt locale_ctxt elem)]) elems end; fun print_locale thy show_facts raw_name = - Pretty.writeln (pretty_locale thy show_facts (check thy raw_name)); + Pretty.writeln (Pretty.block (pretty_locale thy show_facts (check thy raw_name))); fun print_registrations ctxt raw_name = let @@ -732,7 +732,7 @@ fun make_node name = {name = name, parents = map (fst o fst) (dependencies_of thy name), - body = pretty_locale thy false name}; + body = Pretty.block (pretty_locale thy false name)}; val names = sort_strings (Name_Space.fold_table (cons o #1) (Locales.get thy) []); in map make_node names end; diff -r 56f8bfe1211c -r 1f66c7d77002 src/Pure/Isar/named_target.ML --- a/src/Pure/Isar/named_target.ML Thu Aug 03 13:35:28 2017 +0200 +++ b/src/Pure/Isar/named_target.ML Fri Aug 04 18:03:50 2017 +0200 @@ -2,7 +2,7 @@ Author: Makarius Author: Florian Haftmann, TU Muenchen -Targets for theory, locale, class -- at the bottom the nested structure. +Targets for theory, locale, class -- at the bottom of the nested structure. *) signature NAMED_TARGET = @@ -11,7 +11,9 @@ val locale_of: local_theory -> string option val bottom_locale_of: local_theory -> string option val class_of: local_theory -> string option - val init: (local_theory -> local_theory) option -> string -> theory -> local_theory + val init: string -> theory -> local_theory + val init': {setup: local_theory -> local_theory, conclude: local_theory -> local_theory} -> + string -> theory -> local_theory val theory_init: theory -> local_theory val theory_map: (local_theory -> local_theory) -> theory -> theory val begin: xstring * Position.T -> theory -> local_theory @@ -25,41 +27,53 @@ (* context data *) +datatype target = Theory | Locale of string | Class of string; + +fun target_of_ident _ "" = Theory + | target_of_ident thy ident = + if Locale.defined thy ident + then (if Class.is_class thy ident then Class else Locale) ident + else error ("No such locale: " ^ quote ident); + +fun ident_of_target Theory = "" + | ident_of_target (Locale locale) = locale + | ident_of_target (Class class) = class; + +fun target_is_theory (SOME Theory) = true + | target_is_theory _ = false; + +fun locale_of_target (SOME (Locale locale)) = SOME locale + | locale_of_target (SOME (Class locale)) = SOME locale + | locale_of_target _ = NONE; + +fun class_of_target (SOME (Class class)) = SOME class + | class_of_target _ = NONE; + structure Data = Proof_Data ( - type T = (string * bool) option; + type T = target option; fun init _ = NONE; ); -val get_bottom_data = Data.get; +val get_bottom_target = Data.get; -fun get_data lthy = +fun get_target lthy = if Local_Theory.level lthy = 1 - then get_bottom_data lthy + then get_bottom_target lthy else NONE; -fun is_theory lthy = - (case get_data lthy of - SOME ("", _) => true - | _ => false); - -fun target_of lthy = - (case get_data lthy of +fun ident_of lthy = + case get_target lthy of NONE => error "Not in a named target" - | SOME (target, _) => target); + | SOME target => ident_of_target target; -fun locale_name_of NONE = NONE - | locale_name_of (SOME ("", _)) = NONE - | locale_name_of (SOME (locale, _)) = SOME locale; +val is_theory = target_is_theory o get_target; -val locale_of = locale_name_of o get_data; +val locale_of = locale_of_target o get_target; -val bottom_locale_of = locale_name_of o get_bottom_data; +val bottom_locale_of = locale_of_target o get_bottom_target; -fun class_of lthy = - (case get_data lthy of - SOME (class, true) => SOME class - | _ => NONE); +val class_of = class_of_target o get_target; (* operations *) @@ -74,94 +88,60 @@ #-> (fn (lhs, def) => Class.const class ((b, mx), lhs) params #> pair (lhs, def)); -fun foundation ("", _) = Generic_Target.theory_target_foundation - | foundation (locale, false) = locale_foundation locale - | foundation (class, true) = class_foundation class; - -fun notes ("", _) = Generic_Target.theory_target_notes - | notes (locale, _) = Generic_Target.locale_target_notes locale; - -fun abbrev ("", _) = Generic_Target.theory_abbrev - | abbrev (locale, false) = Generic_Target.locale_abbrev locale - | abbrev (class, true) = Class.abbrev class; - -fun declaration ("", _) _ decl = Generic_Target.theory_declaration decl - | declaration (locale, _) flags decl = Generic_Target.locale_declaration locale flags decl; - -fun theory_registration ("", _) = Generic_Target.theory_registration - | theory_registration _ = (fn _ => error "Not possible in theory target"); - -fun locale_dependency ("", false) = (fn _ => error "Not possible in locale target") - | locale_dependency ("", true) = (fn _ => error "Not possible in class target") - | locale_dependency (locale, _) = Generic_Target.locale_dependency locale; +fun operations Theory = + {define = Generic_Target.define Generic_Target.theory_target_foundation, + notes = Generic_Target.notes Generic_Target.theory_target_notes, + abbrev = Generic_Target.theory_abbrev, + declaration = fn _ => Generic_Target.theory_declaration, + theory_registration = Generic_Target.theory_registration, + locale_dependency = fn _ => error "Not possible in theory target", + pretty = fn ctxt => [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1, + Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))]]} + | operations (Locale locale) = + {define = Generic_Target.define (locale_foundation locale), + notes = Generic_Target.notes (Generic_Target.locale_target_notes locale), + abbrev = Generic_Target.locale_abbrev locale, + declaration = Generic_Target.locale_declaration locale, + theory_registration = fn _ => error "Not possible in locale target", + locale_dependency = Generic_Target.locale_dependency locale, + pretty = fn ctxt => Locale.pretty_locale (Proof_Context.theory_of ctxt) false locale} + | operations (Class class) = + {define = Generic_Target.define (class_foundation class), + notes = Generic_Target.notes (Generic_Target.locale_target_notes class), + abbrev = Class.abbrev class, + declaration = Generic_Target.locale_declaration class, + theory_registration = fn _ => error "Not possible in class target", + locale_dependency = Generic_Target.locale_dependency class, + pretty = fn ctxt => Class.pretty_specification (Proof_Context.theory_of ctxt) class}; -fun pretty (target, is_class) ctxt = - if target = "" then - [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1, - Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))]] - else if is_class then Class.pretty_specification (Proof_Context.theory_of ctxt) target - else - (* FIXME pretty locale content *) - let - val target_name = [Pretty.keyword1 "locale", Pretty.brk 1, Locale.pretty_name ctxt target]; - val fixes = - map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) - (#1 (Proof_Context.inferred_fixes ctxt)); - val assumes = - map (fn A => (Binding.empty_atts, [(Thm.term_of A, [])])) - (Assumption.all_assms_of ctxt); - val elems = - (if null fixes then [] else [Element.Fixes fixes]) @ - (if null assumes then [] else [Element.Assumes assumes]); - in - if null elems then [Pretty.block target_name] - else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) :: - map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))] - end; +fun setup_context Theory = Proof_Context.init_global + | setup_context (Locale locale) = Locale.init locale + | setup_context (Class class) = Class.init class; - -(* init *) - -fun make_name_data _ "" = ("", false) - | make_name_data thy target = - if Locale.defined thy target - then (target, Class.is_class thy target) - else error ("No such locale: " ^ quote target); - -fun init_context ("", _) = Proof_Context.init_global - | init_context (locale, false) = Locale.init locale - | init_context (class, true) = Class.init class; - -fun init before_exit target thy = +fun init' {setup, conclude} ident thy = let - val name_data = make_name_data thy target; - val background_naming = - Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name target); + val target = target_of_ident thy ident; in thy - |> Sign.change_begin - |> init_context name_data - |> is_none before_exit ? Data.put (SOME name_data) - |> Local_Theory.init background_naming - {define = Generic_Target.define (foundation name_data), - notes = Generic_Target.notes (notes name_data), - abbrev = abbrev name_data, - declaration = declaration name_data, - theory_registration = theory_registration name_data, - locale_dependency = locale_dependency name_data, - pretty = pretty name_data, - exit = the_default I before_exit - #> Local_Theory.target_of #> Sign.change_end_local} + |> Generic_Target.init + {background_naming = Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name ident), + setup = setup_context target #> setup, + conclude = conclude} + (operations target) end; -val theory_init = init NONE ""; +fun init ident thy = + init' {setup = Data.put (SOME (target_of_ident thy ident)), conclude = I} ident thy; + +val theory_init = init ""; + fun theory_map f = theory_init #> f #> Local_Theory.exit_global; (* toplevel interaction *) fun begin ("-", _) thy = theory_init thy - | begin target thy = init NONE (Locale.check thy target) thy; + | begin target thy = init (Locale.check thy target) thy; val exit = Local_Theory.assert_bottom #> Local_Theory.exit_global; @@ -172,7 +152,7 @@ | switch NONE (Context.Proof lthy) = (Context.Proof o Local_Theory.reset, lthy) | switch (SOME name) (Context.Proof lthy) = - (Context.Proof o init NONE (target_of lthy) o exit, + (Context.Proof o init (ident_of lthy) o exit, (begin name o exit o Local_Theory.assert_nonbrittle) lthy); end; diff -r 56f8bfe1211c -r 1f66c7d77002 src/Pure/Isar/overloading.ML --- a/src/Pure/Isar/overloading.ML Thu Aug 03 13:35:28 2017 +0200 +++ b/src/Pure/Isar/overloading.ML Fri Aug 04 18:03:50 2017 +0200 @@ -193,21 +193,21 @@ (Term.dest_Const (prep_const ctxt const), (v, checked))); in thy - |> Sign.change_begin - |> Proof_Context.init_global - |> Data.put overloading - |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading - |> activate_improvable_syntax - |> synchronize_syntax - |> Local_Theory.init (Sign.naming_of thy) + |> Generic_Target.init + {background_naming = Sign.naming_of thy, + setup = Proof_Context.init_global + #> Data.put overloading + #> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading + #> activate_improvable_syntax + #> synchronize_syntax, + conclude = conclude} {define = Generic_Target.define foundation, notes = Generic_Target.notes Generic_Target.theory_target_notes, abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev, declaration = K Generic_Target.theory_declaration, theory_registration = Generic_Target.theory_registration, locale_dependency = fn _ => error "Not possible in overloading target", - pretty = pretty, - exit = conclude #> Local_Theory.target_of #> Sign.change_end_local} + pretty = pretty} end; val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const); diff -r 56f8bfe1211c -r 1f66c7d77002 src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Thu Aug 03 13:35:28 2017 +0200 +++ b/src/Tools/Code/code_ml.ML Fri Aug 04 18:03:50 2017 +0200 @@ -59,7 +59,6 @@ fun print_sml_stmt tyco_syntax const_syntax reserved is_constr deresolve = let val deresolve_const = deresolve o Constant; - val deresolve_class = deresolve o Type_Class; val deresolve_classrel = deresolve o Class_Relation; val deresolve_inst = deresolve o Class_Instance; fun print_tyco_expr (sym, []) = (str o deresolve) sym @@ -372,7 +371,6 @@ fun print_ocaml_stmt tyco_syntax const_syntax reserved is_constr deresolve = let val deresolve_const = deresolve o Constant; - val deresolve_class = deresolve o Type_Class; val deresolve_classrel = deresolve o Class_Relation; val deresolve_inst = deresolve o Class_Instance; fun print_tyco_expr (sym, []) = (str o deresolve) sym @@ -676,6 +674,8 @@ in pair (if Code_Namespace.is_public export then type_decl_p :: map print_classparam_decl classparams + else if null classrels andalso null classparams + then [type_decl_p] (*work around weakness in export calculation*) else [concat [str "type", print_dicttyp (class, ITyVar v)]]) (Pretty.chunks ( doublesemicolon [type_decl_p] diff -r 56f8bfe1211c -r 1f66c7d77002 src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Thu Aug 03 13:35:28 2017 +0200 +++ b/src/Tools/Code/code_preproc.ML Fri Aug 04 18:03:50 2017 +0200 @@ -306,7 +306,9 @@ AList.make (snd o Graph.get_node eqngr) (Graph.keys eqngr) |> (map o apfst) (Code.string_of_const thy) |> sort (string_ord o apply2 fst) - |> map (fn (s, cert) => (Pretty.block o Pretty.fbreaks) (Pretty.str s :: Code.pretty_cert thy cert)) + |> (map o apsnd) (Code.pretty_cert thy) + |> filter_out (null o snd) + |> map (fn (s, ps) => (Pretty.block o Pretty.fbreaks) (Pretty.str s :: ps)) |> Pretty.chunks end; diff -r 56f8bfe1211c -r 1f66c7d77002 src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Thu Aug 03 13:35:28 2017 +0200 +++ b/src/Tools/Code/code_scala.ML Fri Aug 04 18:03:50 2017 +0200 @@ -83,7 +83,6 @@ let val (vs_tys, body) = Code_Thingol.unfold_abs t; val (ps, vars') = fold_map (print_abs_head tyvars) vs_tys vars; - val vars' = intro_vars (map_filter fst vs_tys) vars; in brackets (ps @| print_term tyvars false some_thm vars' NOBR body) end @@ -183,22 +182,22 @@ (fn (v, sort) => (Pretty.block o map str) (lookup_tyvar tyvars v :: maps (fn class => [" : ", deresolve_class class]) sort)) NOBR (str s) vs; - fun print_defhead export tyvars vars const vs params tys ty = + fun print_defhead tyvars vars const vs params tys ty = concat [str "def", constraint (applify "(" ")" (fn (param, ty) => constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty)) NOBR (print_context tyvars vs (deresolve_const const)) (params ~~ tys)) (print_typ tyvars NOBR ty), str "="]; - fun print_def export const (vs, ty) [] = + fun print_def const (vs, ty) [] = let val (tys, ty') = Code_Thingol.unfold_fun ty; val params = Name.invent (snd reserved) "a" (length tys); val tyvars = intro_tyvars vs reserved; val vars = intro_vars params reserved; in - concat [print_defhead export tyvars vars const vs params tys ty', + concat [print_defhead tyvars vars const vs params tys ty', str ("sys.error(\"" ^ const ^ "\")")] end - | print_def export const (vs, ty) eqs = + | print_def const (vs, ty) eqs = let val tycos = fold (fn ((ts, t), _) => fold Code_Thingol.add_tyconames (t :: ts)) eqs []; @@ -230,7 +229,7 @@ tuplify (map (print_term tyvars true some_thm vars' NOBR) ts), str "=>", print_rhs vars' eq] end; - val head = print_defhead export tyvars vars2 const vs params tys' ty'; + val head = print_defhead tyvars vars2 const vs params tys' ty'; in if simple then concat [head, print_rhs vars2 (hd eqs)] else @@ -269,9 +268,9 @@ str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}") (map print_classparam_instance (inst_params @ superinst_params)) end; - fun print_stmt (Constant const, (export, Fun ((vs, ty), raw_eqs))) = - print_def export const (vs, ty) (filter (snd o snd) raw_eqs) - | print_stmt (Type_Constructor tyco, (export, Datatype (vs, cos))) = + fun print_stmt (Constant const, (_, Fun ((vs, ty), raw_eqs))) = + print_def const (vs, ty) (filter (snd o snd) raw_eqs) + | print_stmt (Type_Constructor tyco, (_, Datatype (vs, cos))) = let val tyvars = intro_tyvars (map (rpair []) vs) reserved; fun print_co ((co, vs_args), tys) = @@ -288,7 +287,7 @@ NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs :: map print_co cos) end - | print_stmt (Type_Class class, (export, Class ((v, (classrels, classparams)), insts))) = + | print_stmt (Type_Class class, (_, Class ((v, (classrels, classparams)), insts))) = let val tyvars = intro_tyvars [(v, [class])] reserved; fun add_typarg s = Pretty.block