--- 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
--- 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
--- 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 \<open>
\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 ->
--- 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 "\<And>x. x \<in> s \<Longrightarrow> finite (t x)"
+ shows "finite {(i, j) |i j. i \<in> s \<and> j \<in> t i}"
+ using assms
+proof induct
+ case (insert x s)
+ have *: "{(i, j) |i j. i \<in> insert x s \<and> j \<in> t i} =
+ (\<lambda>y. (x,y)) ` (t x) \<union> {(i, j) |i j. i \<in> s \<and> j \<in> t i}" by auto
+ show ?case
+ unfolding *
+ apply (rule finite_UnI)
+ using insert
+ apply auto
+ done
+qed auto
+
+
lemma le_left_mono: "x \<le> y \<Longrightarrow> y \<le> a \<longrightarrow> x \<le> (a::'a::preorder)"
by (auto intro: order_trans)
@@ -1633,11 +1651,16 @@
then show "\<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
by force
qed
- from choice[OF this] guess k .. note k=conjunctD2[OF this[rule_format],rule_format]
-
+ then obtain k where k: "\<And>x. 0 < k x"
+ "\<And>i x. \<lbrakk>i \<in> d; x \<notin> i\<rbrakk> \<Longrightarrow> ball x (k x) \<inter> 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"
+ "\<And>p. \<lbrakk>p tagged_partial_division_of cbox a b; g fine p\<rbrakk>
+ \<Longrightarrow> (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x - integral k f)) < e / 2"
+ by (metis (no_types, lifting))
let ?g = "\<lambda>x. g x \<inter> ball x (k x)"
show ?case
apply (rule_tac x="?g" in exI)
@@ -1716,15 +1739,12 @@
assume y: "y \<in> cbox a b"
then have "\<exists>x l. (x, l) \<in> p \<and> y\<in>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) \<in> p" "y \<in> l" by metis
then have "\<exists>k. k \<in> d \<and> y \<in> k"
using y unfolding d'(6)[symmetric] by auto
- then guess i .. note i = conjunctD2[OF this]
+ then obtain i where i: "i \<in> d" "y \<in> i" by metis
have "x \<in> 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 \<in> \<Union>{k. \<exists>x. (x, k) \<in> p'}"
unfolding p'_def Union_iff
apply (rule_tac x="i \<inter> l" in bexI)
@@ -1735,12 +1755,7 @@
qed
then have "(\<Sum>(x, k)\<in>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 **: "\<bar>(\<Sum>(x,k)\<in>p'. norm (content k *\<^sub>R f x)) - (\<Sum>(x,k)\<in>p'. norm (integral k f))\<bar> < e / 2"
unfolding split_def
using p''
--- 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 \<Rightarrow> ennreal"
assumes Mf: "f \<in> borel_measurable borel"
--- 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 "\<And>x. x \<in> s \<Longrightarrow> finite (t x)"
- shows "finite {(i, j) |i j. i \<in> s \<and> j \<in> t i}"
- using assms
-proof induct
- case (insert x s)
- have *: "{(i, j) |i j. i \<in> insert x s \<and> j \<in> t i} =
- (\<lambda>y. (x,y)) ` (t x) \<union> {(i, j) |i j. i \<in> s \<and> j \<in> 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 "\<And>i. i \<in> S \<Longrightarrow> finite (T i)"
@@ -210,18 +193,18 @@
subsection \<open>The notion of a gauge --- simply an open set containing the point.\<close>
-definition "gauge d \<longleftrightarrow> (\<forall>x. x \<in> d x \<and> open (d x))"
+definition "gauge \<gamma> \<longleftrightarrow> (\<forall>x. x \<in> \<gamma> x \<and> open (\<gamma> x))"
lemma gaugeI:
- assumes "\<And>x. x \<in> g x"
- and "\<And>x. open (g x)"
- shows "gauge g"
+ assumes "\<And>x. x \<in> \<gamma> x"
+ and "\<And>x. open (\<gamma> x)"
+ shows "gauge \<gamma>"
using assms unfolding gauge_def by auto
lemma gaugeD[dest]:
- assumes "gauge d"
- shows "x \<in> d x"
- and "open (d x)"
+ assumes "gauge \<gamma>"
+ shows "x \<in> \<gamma> x"
+ and "open (\<gamma> x)"
using assms unfolding gauge_def by auto
lemma gauge_ball_dependent: "\<forall>x. 0 < e x \<Longrightarrow> gauge (\<lambda>x. ball x (e x))"
@@ -233,7 +216,7 @@
lemma gauge_trivial[intro!]: "gauge (\<lambda>x. ball x 1)"
by (rule gauge_ball) auto
-lemma gauge_Int[intro]: "gauge d1 \<Longrightarrow> gauge d2 \<Longrightarrow> gauge (\<lambda>x. d1 x \<inter> d2 x)"
+lemma gauge_Int[intro]: "gauge \<gamma>1 \<Longrightarrow> gauge \<gamma>2 \<Longrightarrow> gauge (\<lambda>x. \<gamma>1 x \<inter> \<gamma>2 x)"
unfolding gauge_def by auto
lemma gauge_reflect:
@@ -244,10 +227,10 @@
lemma gauge_Inter:
assumes "finite S"
- and "\<And>d. d\<in>S \<Longrightarrow> gauge (f d)"
- shows "gauge (\<lambda>x. \<Inter>{f d x | d. d \<in> S})"
+ and "\<And>u. u\<in>S \<Longrightarrow> gauge (f u)"
+ shows "gauge (\<lambda>x. \<Inter>{f u x | u. u \<in> S})"
proof -
- have *: "\<And>x. {f d x |d. d \<in> S} = (\<lambda>d. f d x) ` S"
+ have *: "\<And>x. {f u x |u. u \<in> S} = (\<lambda>u. f u x) ` S"
by auto
show ?thesis
unfolding gauge_def unfolding *
@@ -314,18 +297,15 @@
assume "s = {{a}}" "K\<in>s"
then have "\<exists>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 \<in> s" have "x = {a}"
- by (metis \<open>s division_of cbox a a\<close> cbox_sing division_ofD(2) division_ofD(3) subset_singletonD x)
- }
+ have "x = {a}" if "x \<in> s" for x
+ by (metis \<open>s division_of cbox a a\<close> cbox_sing division_ofD(2) division_ofD(3) subset_singletonD that)
moreover have "s \<noteq> {}"
using \<open>s division_of cbox a a\<close> by auto
ultimately show ?r
@@ -401,11 +381,8 @@
have *: "\<And>s. \<Union>{x\<in>s. x \<noteq> {}} = \<Union>s"
by auto
show "\<Union>?A = s1 \<inter> 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 \<in> ?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 "\<exists>p. p division_of (s \<inter> t)"
using assms division_inter by blast
-lemma elementary_inters:
+lemma elementary_Inter:
assumes "finite f"
and "f \<noteq> {}"
and "\<forall>s\<in>f. \<exists>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 \<in> p"
unfolding p_def
by (auto simp add: box_eq_empty cbox_def intro!: image_eqI[where x="\<lambda>(i::'a)\<in>Basis. (c, d)"])
- {
- fix i :: 'a
- assume "i \<in> Basis"
- with incl nonempty have "a \<bullet> i \<le> c \<bullet> i" "c \<bullet> i \<le> d \<bullet> i" "d \<bullet> i \<le> b \<bullet> i"
- unfolding box_eq_empty subset_box by (auto simp: not_le)
- }
- note ord = this
+ have ord: "a \<bullet> i \<le> c \<bullet> i" "c \<bullet> i \<le> d \<bullet> i" "d \<bullet> i \<le> b \<bullet> i" if "i \<in> 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: "\<And>x. x \<in> p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})"
by (meson Diff_subset division_of_subset)
have "\<exists>d. d division_of \<Inter>((\<lambda>i. \<Union>(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 \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)" ..
have "d \<union> p division_of cbox a b"
@@ -719,12 +692,7 @@
obtains p where "(insert (cbox a b) p) division_of (cbox a b \<union> 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: "\<And>f s. \<Union>\<Union>(f ` s) = \<Union>((\<lambda>x. \<Union>(f x)) ` s)"
- by auto
- have lem2: "\<And>f s. f \<noteq> {} \<Longrightarrow> \<Union>{s \<union> t |t. t \<in> f} = s \<union> \<Union>f"
+ have "\<Union>?D = (\<Union>x\<in>p. \<Union>insert (cbox a b) (q x))"
by auto
- show "\<Union>?D = cbox a b \<union> \<Union>p"
- unfolding * lem1
- unfolding lem2[OF \<open>p \<noteq> {}\<close>, of "cbox a b", symmetric]
- using q(6) by auto
+ also have "... = \<Union>{cbox a b \<union> t |t. t \<in> p}"
+ using q(6) by auto
+ also have "... = cbox a b \<union> \<Union>p"
+ using \<open>p \<noteq> {}\<close> by auto
+ finally show "\<Union>?D = cbox a b \<union> \<Union>p" .
show "K \<subseteq> cbox a b \<union> \<Union>p" "K \<noteq> {}" if "K \<in> ?D" for K
using q that by blast+
show "\<exists>a b. K = cbox a b" if "K \<in> ?D" for K
@@ -920,7 +887,7 @@
apply auto
done
then obtain r2 where r2: "r2 division_of (\<Union>(r1 - p)) \<inter> (\<Union>q)"
- by (metis assms(2) divq(6) elementary_inter)
+ by (metis assms(2) divq(6) elementary_Int)
{
fix x
assume x: "x \<in> T" "x \<notin> S"
@@ -1130,9 +1097,8 @@
assumes "s tagged_partial_division_of i"
and "t \<subseteq> 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 \<Longrightarrow> (x, k) \<in> p \<Longrightarrow> x \<in> i"
@@ -1183,28 +1149,28 @@
qed
lemma tagged_division_unions:
- assumes "finite iset"
- and "\<forall>i\<in>iset. pfn i tagged_division_of i"
- and "\<forall>i1\<in>iset. \<forall>i2\<in>iset. i1 \<noteq> i2 \<longrightarrow> interior(i1) \<inter> interior(i2) = {}"
- shows "\<Union>(pfn ` iset) tagged_division_of (\<Union>iset)"
+ assumes "finite I"
+ and "\<forall>i\<in>I. pfn i tagged_division_of i"
+ and "\<forall>i1\<in>I. \<forall>i2\<in>I. i1 \<noteq> i2 \<longrightarrow> interior(i1) \<inter> interior(i2) = {}"
+ shows "\<Union>(pfn ` I) tagged_division_of (\<Union>I)"
proof (rule tagged_division_ofI)
note assm = tagged_division_ofD[OF assms(2)[rule_format]]
- show "finite (\<Union>(pfn ` iset))"
+ show "finite (\<Union>(pfn ` I))"
using assms by auto
- have "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` iset)} = \<Union>((\<lambda>i. \<Union>{k. \<exists>x. (x, k) \<in> pfn i}) ` iset)"
+ have "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` I)} = \<Union>((\<lambda>i. \<Union>{k. \<exists>x. (x, k) \<in> pfn i}) ` I)"
by blast
- also have "\<dots> = \<Union>iset"
+ also have "\<dots> = \<Union>I"
using assm(6) by auto
- finally show "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` iset)} = \<Union>iset" .
+ finally show "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` I)} = \<Union>I" .
fix x k
- assume xk: "(x, k) \<in> \<Union>(pfn ` iset)"
- then obtain i where i: "i \<in> iset" "(x, k) \<in> pfn i"
+ assume xk: "(x, k) \<in> \<Union>(pfn ` I)"
+ then obtain i where i: "i \<in> I" "(x, k) \<in> pfn i"
by auto
- show "x \<in> k" "\<exists>a b. k = cbox a b" "k \<subseteq> \<Union>iset"
+ show "x \<in> k" "\<exists>a b. k = cbox a b" "k \<subseteq> \<Union>I"
using assm(2-4)[OF i] using i(1) by auto
fix x' k'
- assume xk': "(x', k') \<in> \<Union>(pfn ` iset)" "(x, k) \<noteq> (x', k')"
- then obtain i' where i': "i' \<in> iset" "(x', k') \<in> pfn i'"
+ assume xk': "(x', k') \<in> \<Union>(pfn ` I)" "(x, k) \<noteq> (x', k')"
+ then obtain i' where i': "i' \<in> I" "(x', k') \<in> pfn i'"
by auto
have *: "\<And>a b. i \<noteq> i' \<Longrightarrow> a \<subseteq> i \<Longrightarrow> b \<subseteq> i' \<Longrightarrow> interior a \<inter> 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 "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i" "a\<bullet>k < c" "c < b\<bullet>k"
+ assumes d: "d division_of (cbox a b)"
+ and altb: "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i" "a\<bullet>k < c" "c < b\<bullet>k"
and "l \<in> d"
and disj: "interval_lowerbound l\<bullet>k = c \<or> interval_upperbound l\<bullet>k = c"
and k: "k \<in> Basis"
@@ -1390,14 +1356,12 @@
division_points (cbox a b) d" (is "?D2 \<subset> ?D")
proof -
have ab: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>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 \<open>l \<in> d\<close> by blast
have uv: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i" "\<forall>i\<in>Basis. a\<bullet>i \<le> u\<bullet>i \<and> v\<bullet>i \<le> b\<bullet>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 \<inter> {x. x \<bullet> k \<le> interval_upperbound l \<bullet> k}) \<bullet> k = interval_upperbound l \<bullet> k"
"interval_upperbound (cbox a b \<inter> {x. x \<bullet> k \<le> interval_lowerbound l \<bullet> k}) \<bullet> k = interval_lowerbound l \<bullet> k"
unfolding l interval_split[OF k] interval_bounds[OF uv(1)]
@@ -1406,11 +1370,7 @@
have "\<exists>x. x \<in> ?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)\<bullet>k)" in exI, force simp add: *)
- apply (rule_tac x="(k,(interval_upperbound l)\<bullet>k)" in exI, force simp add: *)
- done
+ by (force simp add: *)
moreover have "?D1 \<subseteq> ?D"
by (auto simp add: assms division_points_subset)
ultimately show "?D1 \<subset> ?D"
@@ -1423,11 +1383,7 @@
have "\<exists>x. x \<in> ?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)\<bullet>k)" in exI, force simp add: *)
- apply (rule_tac x="(k,(interval_upperbound l)\<bullet>k)" in exI, force simp add: *)
- done
+ by (force simp add: *)
moreover have "?D2 \<subseteq> ?D"
by (auto simp add: assms division_points_subset)
ultimately show "?D2 \<subset> ?D"
@@ -1769,39 +1725,28 @@
done
next
fix a b c :: real
- assume "\<forall>a b. b \<le> a \<longrightarrow> g {a .. b} = \<^bold>1"
- and "\<forall>a b c. a < c \<and> c < b \<longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
+ assume eq1: "\<forall>a b. b \<le> a \<longrightarrow> g {a .. b} = \<^bold>1"
+ and eqg: "\<forall>a b c. a < c \<and> c < b \<longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
and "a \<le> c"
and "c \<le> b"
- note as = this[rule_format]
show "g {a..c} \<^bold>* g {c..b} = g {a..b}"
proof (cases "c = a \<or> c = b")
case False
then show ?thesis
- apply -
- apply (subst as(2))
- using as(3-)
- apply auto
- done
+ using eqg \<open>a \<le> c\<close> \<open>c \<le> b\<close> 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 \<open>Some basic combining lemmas.\<close>
lemma tagged_division_Union_exists:
- assumes "finite iset"
- and "\<forall>i\<in>iset. \<exists>p. p tagged_division_of i \<and> d fine p"
- and "\<forall>i1\<in>iset. \<forall>i2\<in>iset. i1 \<noteq> i2 \<longrightarrow> interior i1 \<inter> interior i2 = {}"
- and "\<Union>iset = i"
+ assumes "finite I"
+ and "\<forall>i\<in>I. \<exists>p. p tagged_division_of i \<and> d fine p"
+ and "\<forall>i1\<in>I. \<forall>i2\<in>I. i1 \<noteq> i2 \<longrightarrow> interior i1 \<inter> interior i2 = {}"
+ and "\<Union>I = i"
obtains p where "p tagged_division_of i" and "d fine p"
proof -
obtain pfn where pfn:
- "\<And>x. x \<in> iset \<Longrightarrow> pfn x tagged_division_of x"
- "\<And>x. x \<in> iset \<Longrightarrow> d fine pfn x"
+ "\<And>x. x \<in> I \<Longrightarrow> pfn x tagged_division_of x"
+ "\<And>x. x \<in> I \<Longrightarrow> d fine pfn x"
using bchoice[OF assms(2)] by auto
show thesis
- apply (rule_tac p="\<Union>(pfn ` iset)" in that)
+ apply (rule_tac p="\<Union>(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: "\<And>i. i\<in>Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
by (force simp: mem_box)
- { fix f
- have "\<lbrakk>finite f;
+ have UN_cases: "\<lbrakk>finite f;
\<And>s. s\<in>f \<Longrightarrow> P s;
\<And>s. s\<in>f \<Longrightarrow> \<exists>a b. s = cbox a b;
- \<And>s t. s\<in>f \<Longrightarrow> t\<in>f \<Longrightarrow> s \<noteq> t \<Longrightarrow> interior s \<inter> interior t = {}\<rbrakk> \<Longrightarrow> P (\<Union>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
+ \<And>s t. s\<in>f \<Longrightarrow> t\<in>f \<Longrightarrow> s \<noteq> t \<Longrightarrow> interior s \<inter> interior t = {}\<rbrakk> \<Longrightarrow> P (\<Union>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. \<forall>i\<in>Basis. (c\<bullet>i = a\<bullet>i) \<and> (d\<bullet>i = (a\<bullet>i + b\<bullet>i) / 2) \<or>
(c\<bullet>i = (a\<bullet>i + b\<bullet>i) / 2) \<and> (d\<bullet>i = b\<bullet>i)}"
let ?PP = "\<lambda>c d. \<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i"
@@ -2110,13 +2052,12 @@
then show "\<exists>c d. ?P i c d"
by blast
qed
+ then obtain \<alpha> \<beta> where
+ "\<forall>i\<in>Basis. (\<alpha> \<bullet> i = a \<bullet> i \<and> \<beta> \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
+ \<alpha> \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> \<beta> \<bullet> i = b \<bullet> i) \<and> \<alpha> \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> \<beta> \<bullet> i"
+ by (auto simp: choice_Basis_iff)
then show "x\<in>\<Union>?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 \<bullet> i - c \<bullet> i) \<le> snd x \<bullet> i - fst x \<bullet> 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 \<bullet> i \<le> fst (f x) \<bullet> i \<and>
fst (f x) \<bullet> i \<le> snd (f x) \<bullet> i \<and>
snd (f x) \<bullet> i \<le> snd x \<bullet> i \<and>
- 2 * (snd (f x) \<bullet> i - fst (f x) \<bullet> i) \<le> snd x \<bullet> i - fst x \<bullet> i)"
- apply -
- apply (drule choice)
- apply blast
- done
+ 2 * (snd (f x) \<bullet> i - fst (f x) \<bullet> i) \<le> snd x \<bullet> i - fst x \<bullet> 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: "\<And>n. \<not> P (cbox (A(Suc n)) (B(Suc n))) \<and>
(\<forall>i\<in>Basis. A(n)\<bullet>i \<le> A(Suc n)\<bullet>i \<and> A(Suc n)\<bullet>i \<le> B(Suc n)\<bullet>i \<and> B(Suc n)\<bullet>i \<le> B(n)\<bullet>i \<and>
@@ -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 \<open>\<not> P (cbox a b)\<close> f by auto
next
case (Suc n)
show ?case
@@ -2230,8 +2161,7 @@
next
case (Suc n)
have "B (Suc n) \<bullet> i - A (Suc n) \<bullet> i \<le> (B n \<bullet> i - A n \<bullet> 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 "\<dots> \<le> (b \<bullet> i - a \<bullet> 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 "\<not> (\<exists>p. p tagged_division_of (cbox a b) \<and> g fine p) \<Longrightarrow> False"
- then obtain p where "p tagged_division_of (cbox a b)" "g fine p"
- by blast
- then show thesis ..
+proof (cases "\<exists>p. p tagged_division_of (cbox a b) \<and> g fine p")
+ case True
+ then show ?thesis
+ using that by auto
next
- assume as: "\<not> (\<exists>p. p tagged_division_of (cbox a b) \<and> g fine p)"
+ case False
+ assume "\<not> (\<exists>p. p tagged_division_of (cbox a b) \<and> g fine p)"
obtain x where x:
"x \<in> (cbox a b)"
"\<And>e. 0 < e \<Longrightarrow>
@@ -2310,10 +2240,10 @@
cbox c d \<subseteq> ball x e \<and>
cbox c d \<subseteq> (cbox a b) \<and>
\<not> (\<exists>p. p tagged_division_of cbox c d \<and> g fine p)"
- apply (rule interval_bisection[of "\<lambda>s. \<exists>p. p tagged_division_of s \<and> g fine p", OF _ _ as])
+ apply (rule interval_bisection[of "\<lambda>s. \<exists>p. p tagged_division_of s \<and> 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 \<subseteq> 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 \<Union>{k. \<exists>x. (x, k) \<in> p}"
and "d fine q1"
and q1I: "\<And>x k. \<lbrakk>(x, k)\<in>p; k \<subseteq> d x\<rbrakk> \<Longrightarrow> (x, k) \<in> 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 *: "\<Union>{l. \<exists>y. (y,l) \<in> insert xk p} = k \<union> \<Union>{l. \<exists>y. (y,l) \<in> 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. \<exists>x. (x, k) \<in> 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) \<inter> interior (\<Union>{k. \<exists>x. (x, k) \<in> 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 "\<And>T. T \<in> {k. \<exists>x. (x, k) \<in> p} \<Longrightarrow> \<exists>a b. T = cbox a b"
+ using p(4) by auto
+ show "\<And>T. T \<in> {k. \<exists>x. (x, k) \<in> p} \<Longrightarrow> interior (cbox u v) \<inter> interior T = {}"
+ by clarify (metis insert.hyps(2) insert_iff interior_cbox p(5) uv xk)
+ qed
show ?case
proof (cases "cbox u v \<subseteq> 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)} \<union> q1 tagged_division_of \<Union>{k. \<exists>x. (x, k) \<in> 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)} \<union> 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: \<open>d fine q1\<close> q1I uv xk)
+ using \<open>d fine q1\<close> 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 \<union> 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 \<open>d fine q1\<close> simp add: False q1I uv xk)
--- 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 -
--- 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 @@
\<close>
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 = ""]]
--- 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;
--- 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 \<in> {n. n < 256}" by simp
qed
+setup_lifting type_definition_char
+
definition char_of_nat :: "nat \<Rightarrow> 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 \<open>Strings as dedicated type\<close>
--- 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 **)
--- 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
\<close>
--- 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
--- 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 =
--- 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;
--- 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;
--- 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;
--- 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;
--- 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);
--- 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
--- 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;
--- 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;
--- 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);
--- 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]
--- 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;
--- 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