--- a/src/HOL/Boogie/Tools/boogie_commands.ML Sun Apr 25 08:25:34 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML Mon Apr 26 07:47:18 2010 +0200
@@ -99,7 +99,7 @@
|> (fn ctxt1 => ctxt1
|> prepare
|-> (fn us => fn ctxt2 => ctxt2
- |> Proof.theorem_i NONE (fn thmss => fn ctxt =>
+ |> Proof.theorem NONE (fn thmss => fn ctxt =>
let val export = map (finish ctxt1) o ProofContext.export ctxt ctxt2
in after_qed (map export thmss) ctxt end) [map (rpair []) us]))
end
@@ -188,7 +188,7 @@
fun prove thy meth vc =
ProofContext.init thy
- |> Proof.theorem_i NONE (K I) [[(Boogie_VCs.prop_of_vc vc, [])]]
+ |> Proof.theorem NONE (K I) [[(Boogie_VCs.prop_of_vc vc, [])]]
|> Proof.apply meth
|> Seq.hd
|> Proof.global_done_proof
--- a/src/HOL/HOL.thy Sun Apr 25 08:25:34 2010 +0200
+++ b/src/HOL/HOL.thy Mon Apr 26 07:47:18 2010 +0200
@@ -1869,7 +1869,7 @@
proof
assume "PROP ?ofclass"
show "PROP ?eq"
- by (tactic {* ALLGOALS (rtac (Drule.unconstrainTs @{thm equals_eq})) *})
+ by (tactic {* ALLGOALS (rtac (Thm.unconstrain_allTs @{thm equals_eq})) *})
(fact `PROP ?ofclass`)
next
assume "PROP ?eq"
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Sun Apr 25 08:25:34 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Mon Apr 26 07:47:18 2010 +0200
@@ -1444,7 +1444,7 @@
lemma infnorm_eq_1_imp: assumes "infnorm (x::real^2) = 1" shows "abs(x$1) \<le> 1" "abs(x$2) \<le> 1"
using assms unfolding infnorm_eq_1_2 by auto
-lemma fashoda_unit: fixes f g::"real^1 \<Rightarrow> real^2"
+lemma fashoda_unit: fixes f g::"real \<Rightarrow> real^2"
assumes "f ` {- 1..1} \<subseteq> {- 1..1}" "g ` {- 1..1} \<subseteq> {- 1..1}"
"continuous_on {- 1..1} f" "continuous_on {- 1..1} g"
"f (- 1)$1 = - 1" "f 1$1 = 1" "g (- 1) $2 = -1" "g 1 $2 = 1"
@@ -1457,13 +1457,13 @@
have lem2:"\<forall>z. z\<noteq>0 \<longrightarrow> infnorm(sqprojection z) = 1" unfolding sqprojection_def
unfolding infnorm_mul[unfolded smult_conv_scaleR] unfolding abs_inverse real_abs_infnorm
unfolding infnorm_eq_0[THEN sym] by auto
- let ?F = "(\<lambda>w::real^2. (f \<circ> vec1 \<circ> (\<lambda>x. x$1)) w - (g \<circ> vec1 \<circ> (\<lambda>x. x$2)) w)"
- have *:"\<And>i. vec1 ` (\<lambda>x::real^2. x $ i) ` {- 1..1} = {- 1..1::real^1}"
+ let ?F = "(\<lambda>w::real^2. (f \<circ> (\<lambda>x. x$1)) w - (g \<circ> (\<lambda>x. x$2)) w)"
+ have *:"\<And>i. (\<lambda>x::real^2. x $ i) ` {- 1..1} = {- 1..1::real}"
apply(rule set_ext) unfolding image_iff Bex_def mem_interval apply rule defer
- apply(rule_tac x="dest_vec1 x" in exI) apply rule apply(rule_tac x="vec (dest_vec1 x)" in exI) by auto
- { fix x assume "x \<in> (\<lambda>w. (f \<circ> vec1 \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> vec1 \<circ> (\<lambda>x. x $ 2)) w) ` {- 1..1::real^2}"
+ apply(rule_tac x="vec x" in exI) by auto
+ { fix x assume "x \<in> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w) ` {- 1..1::real^2}"
then guess w unfolding image_iff .. note w = this
- hence "x \<noteq> 0" using as[of "vec1 (w$1)" "vec1 (w$2)"] unfolding mem_interval by auto} note x0=this
+ hence "x \<noteq> 0" using as[of "w$1" "w$2"] unfolding mem_interval by auto} note x0=this
have 21:"\<And>i::2. i\<noteq>1 \<Longrightarrow> i=2" using UNIV_2 by auto
have 1:"{- 1<..<1::real^2} \<noteq> {}" unfolding interval_eq_empty by auto
have 2:"continuous_on {- 1..1} (negatex \<circ> sqprojection \<circ> ?F)" apply(rule continuous_on_intros continuous_on_component continuous_on_vec1)+
@@ -1494,50 +1494,50 @@
unfolding sqprojection_def vector_component_simps Cart_nth.scaleR real_scaleR_def
unfolding zero_less_mult_iff mult_less_0_iff by(auto simp add:field_simps) qed
note lem3 = this[rule_format]
- have x1:"vec1 (x $ 1) \<in> {- 1..1::real^1}" "vec1 (x $ 2) \<in> {- 1..1::real^1}" using x(1) unfolding mem_interval by auto
- hence nz:"f (vec1 (x $ 1)) - g (vec1 (x $ 2)) \<noteq> 0" unfolding right_minus_eq apply-apply(rule as) by auto
+ have x1:"x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}" using x(1) unfolding mem_interval by auto
+ hence nz:"f (x $ 1) - g (x $ 2) \<noteq> 0" unfolding right_minus_eq apply-apply(rule as) by auto
have "x $ 1 = -1 \<or> x $ 1 = 1 \<or> x $ 2 = -1 \<or> x $ 2 = 1" using nx unfolding infnorm_eq_1_2 by auto
thus False proof- fix P Q R S
presume "P \<or> Q \<or> R \<or> S" "P\<Longrightarrow>False" "Q\<Longrightarrow>False" "R\<Longrightarrow>False" "S\<Longrightarrow>False" thus False by auto
- next assume as:"x$1 = 1" hence "vec1 (x$1) = 1" unfolding Cart_eq by auto
- hence *:"f (vec1 (x $ 1)) $ 1 = 1" using assms(6) by auto
- have "sqprojection (f (vec1 (x$1)) - g (vec1 (x$2))) $ 1 < 0"
+ next assume as:"x$1 = 1"
+ hence *:"f (x $ 1) $ 1 = 1" using assms(6) by auto
+ have "sqprojection (f (x$1) - g (x$2)) $ 1 < 0"
using x(2)[unfolded o_def Cart_eq,THEN spec[where x=1]]
unfolding as negatex_def vector_2 by auto moreover
- from x1 have "g (vec1 (x $ 2)) \<in> {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto
+ from x1 have "g (x $ 2) \<in> {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto
ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval
apply(erule_tac x=1 in allE) by auto
- next assume as:"x$1 = -1" hence "vec1 (x$1) = - 1" unfolding Cart_eq by auto
- hence *:"f (vec1 (x $ 1)) $ 1 = - 1" using assms(5) by auto
- have "sqprojection (f (vec1 (x$1)) - g (vec1 (x$2))) $ 1 > 0"
+ next assume as:"x$1 = -1"
+ hence *:"f (x $ 1) $ 1 = - 1" using assms(5) by auto
+ have "sqprojection (f (x$1) - g (x$2)) $ 1 > 0"
using x(2)[unfolded o_def Cart_eq,THEN spec[where x=1]]
unfolding as negatex_def vector_2 by auto moreover
- from x1 have "g (vec1 (x $ 2)) \<in> {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto
+ from x1 have "g (x $ 2) \<in> {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto
ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval
apply(erule_tac x=1 in allE) by auto
- next assume as:"x$2 = 1" hence "vec1 (x$2) = 1" unfolding Cart_eq by auto
- hence *:"g (vec1 (x $ 2)) $ 2 = 1" using assms(8) by auto
- have "sqprojection (f (vec1 (x$1)) - g (vec1 (x$2))) $ 2 > 0"
+ next assume as:"x$2 = 1"
+ hence *:"g (x $ 2) $ 2 = 1" using assms(8) by auto
+ have "sqprojection (f (x$1) - g (x$2)) $ 2 > 0"
using x(2)[unfolded o_def Cart_eq,THEN spec[where x=2]]
unfolding as negatex_def vector_2 by auto moreover
- from x1 have "f (vec1 (x $ 1)) \<in> {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto
+ from x1 have "f (x $ 1) \<in> {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto
ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval
apply(erule_tac x=2 in allE) by auto
- next assume as:"x$2 = -1" hence "vec1 (x$2) = - 1" unfolding Cart_eq by auto
- hence *:"g (vec1 (x $ 2)) $ 2 = - 1" using assms(7) by auto
- have "sqprojection (f (vec1 (x$1)) - g (vec1 (x$2))) $ 2 < 0"
+ next assume as:"x$2 = -1"
+ hence *:"g (x $ 2) $ 2 = - 1" using assms(7) by auto
+ have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0"
using x(2)[unfolded o_def Cart_eq,THEN spec[where x=2]]
unfolding as negatex_def vector_2 by auto moreover
- from x1 have "f (vec1 (x $ 1)) \<in> {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto
+ from x1 have "f (x $ 1) \<in> {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto
ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval
apply(erule_tac x=2 in allE) by auto qed(auto) qed
-lemma fashoda_unit_path: fixes f ::"real^1 \<Rightarrow> real^2" and g ::"real^1 \<Rightarrow> real^2"
+lemma fashoda_unit_path: fixes f ::"real \<Rightarrow> real^2" and g ::"real \<Rightarrow> real^2"
assumes "path f" "path g" "path_image f \<subseteq> {- 1..1}" "path_image g \<subseteq> {- 1..1}"
"(pathstart f)$1 = -1" "(pathfinish f)$1 = 1" "(pathstart g)$2 = -1" "(pathfinish g)$2 = 1"
obtains z where "z \<in> path_image f" "z \<in> path_image g" proof-
note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def]
- def iscale \<equiv> "\<lambda>z::real^1. inverse 2 *\<^sub>R (z + 1)"
+ def iscale \<equiv> "\<lambda>z::real. inverse 2 *\<^sub>R (z + 1)"
have isc:"iscale ` {- 1..1} \<subseteq> {0..1}" unfolding iscale_def by(auto)
have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t" proof(rule fashoda_unit)
show "(f \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}" "(g \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}"
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sun Apr 25 08:25:34 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Apr 26 07:47:18 2010 +0200
@@ -401,9 +401,38 @@
lemma convex_halfspace_gt: "convex {x. inner a x > b}"
using convex_halfspace_lt[of "-a" "-b"] by auto
+lemma convex_real_interval:
+ fixes a b :: "real"
+ shows "convex {a..}" and "convex {..b}"
+ and "convex {a<..}" and "convex {..<b}"
+ and "convex {a..b}" and "convex {a<..b}"
+ and "convex {a..<b}" and "convex {a<..<b}"
+proof -
+ have "{a..} = {x. a \<le> inner 1 x}" by auto
+ thus 1: "convex {a..}" by (simp only: convex_halfspace_ge)
+ have "{..b} = {x. inner 1 x \<le> b}" by auto
+ thus 2: "convex {..b}" by (simp only: convex_halfspace_le)
+ have "{a<..} = {x. a < inner 1 x}" by auto
+ thus 3: "convex {a<..}" by (simp only: convex_halfspace_gt)
+ have "{..<b} = {x. inner 1 x < b}" by auto
+ thus 4: "convex {..<b}" by (simp only: convex_halfspace_lt)
+ have "{a..b} = {a..} \<inter> {..b}" by auto
+ thus "convex {a..b}" by (simp only: convex_Int 1 2)
+ have "{a<..b} = {a<..} \<inter> {..b}" by auto
+ thus "convex {a<..b}" by (simp only: convex_Int 3 2)
+ have "{a..<b} = {a..} \<inter> {..<b}" by auto
+ thus "convex {a..<b}" by (simp only: convex_Int 1 4)
+ have "{a<..<b} = {a<..} \<inter> {..<b}" by auto
+ thus "convex {a<..<b}" by (simp only: convex_Int 3 4)
+qed
+
+lemma convex_box:
+ assumes "\<And>i. convex {x. P i x}"
+ shows "convex {x. \<forall>i. P i (x$i)}"
+using assms unfolding convex_def by auto
+
lemma convex_positive_orthant: "convex {x::real^'n. (\<forall>i. 0 \<le> x$i)}"
- unfolding convex_def apply auto apply(erule_tac x=i in allE)+
- apply(rule add_nonneg_nonneg) by(auto simp add: mult_nonneg_nonneg)
+by (rule convex_box, simp add: atLeast_def [symmetric] convex_real_interval)
subsection {* Explicit expressions for convexity in terms of arbitrary sums. *}
@@ -2580,11 +2609,11 @@
"midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)"
definition
- open_segment :: "real ^ 'n \<Rightarrow> real ^ 'n \<Rightarrow> (real ^ 'n) set" where
+ open_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" where
"open_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 < u \<and> u < 1}"
definition
- closed_segment :: "real ^ 'n \<Rightarrow> real ^ 'n \<Rightarrow> (real ^ 'n) set" where
+ closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" where
"closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \<le> u \<and> u \<le> 1}"
definition "between = (\<lambda> (a,b). closed_segment a b)"
@@ -2655,12 +2684,14 @@
unfolding segment_convex_hull apply(rule_tac[!] hull_subset[unfolded subset_eq, rule_format]) by auto
lemma segment_furthest_le:
+ fixes a b x y :: "real ^ 'n"
assumes "x \<in> closed_segment a b" shows "norm(y - x) \<le> norm(y - a) \<or> norm(y - x) \<le> norm(y - b)" proof-
obtain z where "z\<in>{a, b}" "norm (x - y) \<le> norm (z - y)" using simplex_furthest_le[of "{a, b}" y]
using assms[unfolded segment_convex_hull] by auto
thus ?thesis by(auto simp add:norm_minus_commute) qed
lemma segment_bound:
+ fixes x a b :: "real ^ 'n"
assumes "x \<in> closed_segment a b"
shows "norm(x - a) \<le> norm(b - a)" "norm(x - b) \<le> norm(b - a)"
using segment_furthest_le[OF assms, of a]
@@ -2842,23 +2873,42 @@
subsection {* Paths. *}
-definition "path (g::real^1 \<Rightarrow> real^'n) \<longleftrightarrow> continuous_on {0 .. 1} g"
-
-definition "pathstart (g::real^1 \<Rightarrow> real^'n) = g 0"
-
-definition "pathfinish (g::real^1 \<Rightarrow> real^'n) = g 1"
-
-definition "path_image (g::real^1 \<Rightarrow> real^'n) = g ` {0 .. 1}"
-
-definition "reversepath (g::real^1 \<Rightarrow> real^'n) = (\<lambda>x. g(1 - x))"
-
-definition joinpaths:: "(real^1 \<Rightarrow> real^'n) \<Rightarrow> (real^1 \<Rightarrow> real^'n) \<Rightarrow> (real^1 \<Rightarrow> real^'n)" (infixr "+++" 75)
- where "joinpaths g1 g2 = (\<lambda>x. if dest_vec1 x \<le> ((1 / 2)::real) then g1 (2 *\<^sub>R x) else g2(2 *\<^sub>R x - 1))"
-definition "simple_path (g::real^1 \<Rightarrow> real^'n) \<longleftrightarrow>
+text {* TODO: Once @{const continuous_on} is generalized to arbitrary
+topological spaces, all of these concepts should be similarly generalized. *}
+
+definition
+ path :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> bool"
+ where "path g \<longleftrightarrow> continuous_on {0 .. 1} g"
+
+definition
+ pathstart :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> 'a"
+ where "pathstart g = g 0"
+
+definition
+ pathfinish :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> 'a"
+ where "pathfinish g = g 1"
+
+definition
+ path_image :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> 'a set"
+ where "path_image g = g ` {0 .. 1}"
+
+definition
+ reversepath :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> (real \<Rightarrow> 'a)"
+ where "reversepath g = (\<lambda>x. g(1 - x))"
+
+definition
+ joinpaths :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> (real \<Rightarrow> 'a)"
+ (infixr "+++" 75)
+ where "g1 +++ g2 = (\<lambda>x. if x \<le> 1/2 then g1 (2 * x) else g2 (2 * x - 1))"
+
+definition
+ simple_path :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> bool"
+ where "simple_path g \<longleftrightarrow>
(\<forall>x\<in>{0..1}. \<forall>y\<in>{0..1}. g x = g y \<longrightarrow> x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0)"
-definition "injective_path (g::real^1 \<Rightarrow> real^'n) \<longleftrightarrow>
- (\<forall>x\<in>{0..1}. \<forall>y\<in>{0..1}. g x = g y \<longrightarrow> x = y)"
+definition
+ injective_path :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> bool"
+ where "injective_path g \<longleftrightarrow> (\<forall>x\<in>{0..1}. \<forall>y\<in>{0..1}. g x = g y \<longrightarrow> x = y)"
subsection {* Some lemmas about these concepts. *}
@@ -2870,20 +2920,19 @@
unfolding path_image_def image_is_empty interval_eq_empty by auto
lemma pathstart_in_path_image[intro]: "(pathstart g) \<in> path_image g"
- unfolding pathstart_def path_image_def apply(rule imageI)
- unfolding mem_interval_1 vec_1[THEN sym] dest_vec1_vec by auto
+ unfolding pathstart_def path_image_def by auto
lemma pathfinish_in_path_image[intro]: "(pathfinish g) \<in> path_image g"
- unfolding pathfinish_def path_image_def apply(rule imageI)
- unfolding mem_interval_1 vec_1[THEN sym] dest_vec1_vec by auto
+ unfolding pathfinish_def path_image_def by auto
lemma connected_path_image[intro]: "path g \<Longrightarrow> connected(path_image g)"
- unfolding path_def path_image_def apply(rule connected_continuous_image, assumption)
- by(rule convex_connected, rule convex_interval)
+ unfolding path_def path_image_def
+ apply (erule connected_continuous_image)
+ by(rule convex_connected, rule convex_real_interval)
lemma compact_path_image[intro]: "path g \<Longrightarrow> compact(path_image g)"
- unfolding path_def path_image_def apply(rule compact_continuous_image, assumption)
- by(rule compact_interval)
+ unfolding path_def path_image_def
+ by (erule compact_continuous_image, rule compact_real_interval)
lemma reversepath_reversepath[simp]: "reversepath(reversepath g) = g"
unfolding reversepath_def by auto
@@ -2897,15 +2946,13 @@
lemma pathstart_join[simp]: "pathstart(g1 +++ g2) = pathstart g1"
unfolding pathstart_def joinpaths_def pathfinish_def by auto
-lemma pathfinish_join[simp]:"pathfinish(g1 +++ g2) = pathfinish g2" proof-
- have "2 *\<^sub>R 1 - 1 = (1::real^1)" unfolding Cart_eq by(auto simp add:vector_component_simps)
- thus ?thesis unfolding pathstart_def joinpaths_def pathfinish_def
- unfolding vec_1[THEN sym] dest_vec1_vec by auto qed
+lemma pathfinish_join[simp]:"pathfinish(g1 +++ g2) = pathfinish g2"
+ unfolding pathstart_def joinpaths_def pathfinish_def by auto
lemma path_image_reversepath[simp]: "path_image(reversepath g) = path_image g" proof-
have *:"\<And>g. path_image(reversepath g) \<subseteq> path_image g"
unfolding path_image_def subset_eq reversepath_def Ball_def image_iff apply(rule,rule,erule bexE)
- apply(rule_tac x="1 - xa" in bexI) by(auto simp add:vector_le_def vector_component_simps elim!:ballE)
+ apply(rule_tac x="1 - xa" in bexI) by auto
show ?thesis using *[of g] *[of "reversepath g"] unfolding reversepath_reversepath by auto qed
lemma path_reversepath[simp]: "path(reversepath g) \<longleftrightarrow> path g" proof-
@@ -2913,7 +2960,7 @@
apply(rule continuous_on_compose[unfolded o_def, of _ "\<lambda>x. 1 - x"])
apply(rule continuous_on_sub, rule continuous_on_const, rule continuous_on_id)
apply(rule continuous_on_subset[of "{0..1}"], assumption) by auto
- show ?thesis using *[of g] *[of "reversepath g"] unfolding reversepath_reversepath by auto qed
+ show ?thesis using *[of "reversepath g"] *[of g] unfolding reversepath_reversepath by (rule iffI) qed
lemmas reversepath_simps = path_reversepath path_image_reversepath pathstart_reversepath pathfinish_reversepath
@@ -2921,48 +2968,50 @@
unfolding path_def pathfinish_def pathstart_def apply rule defer apply(erule conjE) proof-
assume as:"continuous_on {0..1} (g1 +++ g2)"
have *:"g1 = (\<lambda>x. g1 (2 *\<^sub>R x)) \<circ> (\<lambda>x. (1/2) *\<^sub>R x)"
- "g2 = (\<lambda>x. g2 (2 *\<^sub>R x - 1)) \<circ> (\<lambda>x. (1/2) *\<^sub>R (x + 1))" unfolding o_def by auto
- have "op *\<^sub>R (1 / 2) ` {0::real^1..1} \<subseteq> {0..1}" "(\<lambda>x. (1 / 2) *\<^sub>R (x + 1)) ` {(0::real^1)..1} \<subseteq> {0..1}"
- unfolding image_smult_interval by auto
+ "g2 = (\<lambda>x. g2 (2 *\<^sub>R x - 1)) \<circ> (\<lambda>x. (1/2) *\<^sub>R (x + 1))"
+ unfolding o_def by (auto simp add: add_divide_distrib)
+ have "op *\<^sub>R (1 / 2) ` {0::real..1} \<subseteq> {0..1}" "(\<lambda>x. (1 / 2) *\<^sub>R (x + 1)) ` {(0::real)..1} \<subseteq> {0..1}"
+ by auto
thus "continuous_on {0..1} g1 \<and> continuous_on {0..1} g2" apply -apply rule
apply(subst *) defer apply(subst *) apply (rule_tac[!] continuous_on_compose)
apply (rule continuous_on_cmul, rule continuous_on_add, rule continuous_on_id, rule continuous_on_const) defer
apply (rule continuous_on_cmul, rule continuous_on_id) apply(rule_tac[!] continuous_on_eq[of _ "g1 +++ g2"]) defer prefer 3
apply(rule_tac[1-2] continuous_on_subset[of "{0 .. 1}"]) apply(rule as, assumption, rule as, assumption)
apply(rule) defer apply rule proof-
- fix x assume "x \<in> op *\<^sub>R (1 / 2) ` {0::real^1..1}"
- hence "dest_vec1 x \<le> 1 / 2" unfolding image_iff by(auto simp add: vector_component_simps)
+ fix x assume "x \<in> op *\<^sub>R (1 / 2) ` {0::real..1}"
+ hence "x \<le> 1 / 2" unfolding image_iff by auto
thus "(g1 +++ g2) x = g1 (2 *\<^sub>R x)" unfolding joinpaths_def by auto next
- fix x assume "x \<in> (\<lambda>x. (1 / 2) *\<^sub>R (x + 1)) ` {0::real^1..1}"
- hence "dest_vec1 x \<ge> 1 / 2" unfolding image_iff by(auto simp add: vector_component_simps)
- thus "(g1 +++ g2) x = g2 (2 *\<^sub>R x - 1)" proof(cases "dest_vec1 x = 1 / 2")
- case True hence "x = (1/2) *\<^sub>R 1" unfolding Cart_eq by(auto simp add: forall_1 vector_component_simps)
- thus ?thesis unfolding joinpaths_def using assms[unfolded pathstart_def pathfinish_def] by auto
+ fix x assume "x \<in> (\<lambda>x. (1 / 2) *\<^sub>R (x + 1)) ` {0::real..1}"
+ hence "x \<ge> 1 / 2" unfolding image_iff by auto
+ thus "(g1 +++ g2) x = g2 (2 *\<^sub>R x - 1)" proof(cases "x = 1 / 2")
+ case True hence "x = (1/2) *\<^sub>R 1" unfolding Cart_eq by auto
+ thus ?thesis unfolding joinpaths_def using assms[unfolded pathstart_def pathfinish_def] by (auto simp add: mult_ac)
qed (auto simp add:le_less joinpaths_def) qed
next assume as:"continuous_on {0..1} g1" "continuous_on {0..1} g2"
- have *:"{0 .. 1::real^1} = {0.. (1/2)*\<^sub>R 1} \<union> {(1/2) *\<^sub>R 1 .. 1}" by(auto simp add: vector_component_simps)
- have **:"op *\<^sub>R 2 ` {0..(1 / 2) *\<^sub>R 1} = {0..1::real^1}" apply(rule set_ext, rule) unfolding image_iff
- defer apply(rule_tac x="(1/2)*\<^sub>R x" in bexI) by(auto simp add: vector_component_simps)
- have ***:"(\<lambda>x. 2 *\<^sub>R x - 1) ` {(1 / 2) *\<^sub>R 1..1} = {0..1::real^1}"
- unfolding image_affinity_interval[of _ "- 1", unfolded diff_def[symmetric]] and interval_eq_empty_1
- by(auto simp add: vector_component_simps)
- have ****:"\<And>x::real^1. x $ 1 * 2 = 1 \<longleftrightarrow> x = (1/2) *\<^sub>R 1" unfolding Cart_eq by(auto simp add: forall_1 vector_component_simps)
- show "continuous_on {0..1} (g1 +++ g2)" unfolding * apply(rule continuous_on_union) apply(rule closed_interval)+ proof-
+ have *:"{0 .. 1::real} = {0.. (1/2)*\<^sub>R 1} \<union> {(1/2) *\<^sub>R 1 .. 1}" by auto
+ have **:"op *\<^sub>R 2 ` {0..(1 / 2) *\<^sub>R 1} = {0..1::real}" apply(rule set_ext, rule) unfolding image_iff
+ defer apply(rule_tac x="(1/2)*\<^sub>R x" in bexI) by auto
+ have ***:"(\<lambda>x. 2 *\<^sub>R x - 1) ` {(1 / 2) *\<^sub>R 1..1} = {0..1::real}"
+ apply (auto simp add: image_def)
+ apply (rule_tac x="(x + 1) / 2" in bexI)
+ apply (auto simp add: add_divide_distrib)
+ done
+ show "continuous_on {0..1} (g1 +++ g2)" unfolding * apply(rule continuous_on_union) apply (rule closed_real_atLeastAtMost)+ proof-
show "continuous_on {0..(1 / 2) *\<^sub>R 1} (g1 +++ g2)" apply(rule continuous_on_eq[of _ "\<lambda>x. g1 (2 *\<^sub>R x)"]) defer
unfolding o_def[THEN sym] apply(rule continuous_on_compose) apply(rule continuous_on_cmul, rule continuous_on_id)
- unfolding ** apply(rule as(1)) unfolding joinpaths_def by(auto simp add: vector_component_simps) next
+ unfolding ** apply(rule as(1)) unfolding joinpaths_def by auto next
show "continuous_on {(1/2)*\<^sub>R1..1} (g1 +++ g2)" apply(rule continuous_on_eq[of _ "g2 \<circ> (\<lambda>x. 2 *\<^sub>R x - 1)"]) defer
apply(rule continuous_on_compose) apply(rule continuous_on_sub, rule continuous_on_cmul, rule continuous_on_id, rule continuous_on_const)
unfolding *** o_def joinpaths_def apply(rule as(2)) using assms[unfolded pathstart_def pathfinish_def]
- by(auto simp add: vector_component_simps ****) qed qed
+ by (auto simp add: mult_ac) qed qed
lemma path_image_join_subset: "path_image(g1 +++ g2) \<subseteq> (path_image g1 \<union> path_image g2)" proof
fix x assume "x \<in> path_image (g1 +++ g2)"
- then obtain y where y:"y\<in>{0..1}" "x = (if dest_vec1 y \<le> 1 / 2 then g1 (2 *\<^sub>R y) else g2 (2 *\<^sub>R y - 1))"
+ then obtain y where y:"y\<in>{0..1}" "x = (if y \<le> 1 / 2 then g1 (2 *\<^sub>R y) else g2 (2 *\<^sub>R y - 1))"
unfolding path_image_def image_iff joinpaths_def by auto
- thus "x \<in> path_image g1 \<union> path_image g2" apply(cases "dest_vec1 y \<le> 1/2")
+ thus "x \<in> path_image g1 \<union> path_image g2" apply(cases "y \<le> 1/2")
apply(rule_tac UnI1) defer apply(rule_tac UnI2) unfolding y(2) path_image_def using y(1)
- by(auto intro!: imageI simp add: vector_component_simps) qed
+ by(auto intro!: imageI) qed
lemma subset_path_image_join:
assumes "path_image g1 \<subseteq> s" "path_image g2 \<subseteq> s" shows "path_image(g1 +++ g2) \<subseteq> s"
@@ -2975,13 +3024,12 @@
fix x assume "x \<in> path_image g1"
then obtain y where y:"y\<in>{0..1}" "x = g1 y" unfolding path_image_def image_iff by auto
thus "x \<in> path_image (g1 +++ g2)" unfolding joinpaths_def path_image_def image_iff
- apply(rule_tac x="(1/2) *\<^sub>R y" in bexI) by(auto simp add: vector_component_simps) next
+ apply(rule_tac x="(1/2) *\<^sub>R y" in bexI) by auto next
fix x assume "x \<in> path_image g2"
then obtain y where y:"y\<in>{0..1}" "x = g2 y" unfolding path_image_def image_iff by auto
- moreover have *:"y $ 1 = 0 \<Longrightarrow> y = 0" unfolding Cart_eq by auto
- ultimately show "x \<in> path_image (g1 +++ g2)" unfolding joinpaths_def path_image_def image_iff
+ then show "x \<in> path_image (g1 +++ g2)" unfolding joinpaths_def path_image_def image_iff
apply(rule_tac x="(1/2) *\<^sub>R (y + 1)" in bexI) using assms(3)[unfolded pathfinish_def pathstart_def]
- by(auto simp add: vector_component_simps) qed
+ by (auto simp add: add_divide_distrib) qed
lemma not_in_path_image_join:
assumes "x \<notin> path_image g1" "x \<notin> path_image g2" shows "x \<notin> path_image(g1 +++ g2)"
@@ -2990,7 +3038,7 @@
lemma simple_path_reversepath: assumes "simple_path g" shows "simple_path (reversepath g)"
using assms unfolding simple_path_def reversepath_def apply- apply(rule ballI)+
apply(erule_tac x="1-x" in ballE, erule_tac x="1-y" in ballE)
- unfolding mem_interval_1 by(auto simp add:vector_component_simps)
+ unfolding mem_interval_1 by auto
(** move this **)
declare vector_scaleR_component[simp]
@@ -3001,42 +3049,42 @@
shows "simple_path(g1 +++ g2)"
unfolding simple_path_def proof((rule ballI)+, rule impI) let ?g = "g1 +++ g2"
note inj = assms(1,2)[unfolded injective_path_def, rule_format]
- fix x y::"real^1" assume xy:"x \<in> {0..1}" "y \<in> {0..1}" "?g x = ?g y"
- show "x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0" proof(case_tac "x$1 \<le> 1/2",case_tac[!] "y$1 \<le> 1/2", unfold not_le)
- assume as:"x $ 1 \<le> 1 / 2" "y $ 1 \<le> 1 / 2"
+ fix x y::"real" assume xy:"x \<in> {0..1}" "y \<in> {0..1}" "?g x = ?g y"
+ show "x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0" proof(case_tac "x \<le> 1/2",case_tac[!] "y \<le> 1/2", unfold not_le)
+ assume as:"x \<le> 1 / 2" "y \<le> 1 / 2"
hence "g1 (2 *\<^sub>R x) = g1 (2 *\<^sub>R y)" using xy(3) unfolding joinpaths_def by auto
moreover have "2 *\<^sub>R x \<in> {0..1}" "2 *\<^sub>R y \<in> {0..1}" using xy(1,2) as
- unfolding mem_interval_1 by(auto simp add:vector_component_simps)
+ unfolding mem_interval_1 by auto
ultimately show ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] by auto
- next assume as:"x $ 1 > 1 / 2" "y $ 1 > 1 / 2"
+ next assume as:"x > 1 / 2" "y > 1 / 2"
hence "g2 (2 *\<^sub>R x - 1) = g2 (2 *\<^sub>R y - 1)" using xy(3) unfolding joinpaths_def by auto
- moreover have "2 *\<^sub>R x - 1 \<in> {0..1}" "2 *\<^sub>R y - 1 \<in> {0..1}" using xy(1,2) as unfolding mem_interval_1 by(auto simp add:vector_component_simps)
+ moreover have "2 *\<^sub>R x - 1 \<in> {0..1}" "2 *\<^sub>R y - 1 \<in> {0..1}" using xy(1,2) as unfolding mem_interval_1 by auto
ultimately show ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] by auto
- next assume as:"x $ 1 \<le> 1 / 2" "y $ 1 > 1 / 2"
+ next assume as:"x \<le> 1 / 2" "y > 1 / 2"
hence "?g x \<in> path_image g1" "?g y \<in> path_image g2" unfolding path_image_def joinpaths_def
- using xy(1,2)[unfolded mem_interval_1] by(auto simp add:vector_component_simps intro!: imageI)
+ using xy(1,2)[unfolded mem_interval_1] by auto
moreover have "?g y \<noteq> pathstart g2" using as(2) unfolding pathstart_def joinpaths_def
using inj(2)[of "2 *\<^sub>R y - 1" 0] and xy(2)[unfolded mem_interval_1]
- by(auto simp add:vector_component_simps field_simps Cart_eq)
+ by (auto simp add: field_simps)
ultimately have *:"?g x = pathstart g1" using assms(4) unfolding xy(3) by auto
hence "x = 0" unfolding pathstart_def joinpaths_def using as(1) and xy(1)[unfolded mem_interval_1]
- using inj(1)[of "2 *\<^sub>R x" 0] by(auto simp add:vector_component_simps)
+ using inj(1)[of "2 *\<^sub>R x" 0] by auto
moreover have "y = 1" using * unfolding xy(3) assms(3)[THEN sym]
unfolding joinpaths_def pathfinish_def using as(2) and xy(2)[unfolded mem_interval_1]
- using inj(2)[of "2 *\<^sub>R y - 1" 1] by (auto simp add:vector_component_simps Cart_eq)
- ultimately show ?thesis by auto
- next assume as:"x $ 1 > 1 / 2" "y $ 1 \<le> 1 / 2"
+ using inj(2)[of "2 *\<^sub>R y - 1" 1] by auto
+ ultimately show ?thesis by auto
+ next assume as:"x > 1 / 2" "y \<le> 1 / 2"
hence "?g x \<in> path_image g2" "?g y \<in> path_image g1" unfolding path_image_def joinpaths_def
- using xy(1,2)[unfolded mem_interval_1] by(auto simp add:vector_component_simps intro!: imageI)
+ using xy(1,2)[unfolded mem_interval_1] by auto
moreover have "?g x \<noteq> pathstart g2" using as(1) unfolding pathstart_def joinpaths_def
using inj(2)[of "2 *\<^sub>R x - 1" 0] and xy(1)[unfolded mem_interval_1]
- by(auto simp add:vector_component_simps field_simps Cart_eq)
+ by (auto simp add: field_simps)
ultimately have *:"?g y = pathstart g1" using assms(4) unfolding xy(3) by auto
hence "y = 0" unfolding pathstart_def joinpaths_def using as(2) and xy(2)[unfolded mem_interval_1]
- using inj(1)[of "2 *\<^sub>R y" 0] by(auto simp add:vector_component_simps)
+ using inj(1)[of "2 *\<^sub>R y" 0] by auto
moreover have "x = 1" using * unfolding xy(3)[THEN sym] assms(3)[THEN sym]
unfolding joinpaths_def pathfinish_def using as(1) and xy(1)[unfolded mem_interval_1]
- using inj(2)[of "2 *\<^sub>R x - 1" 1] by(auto simp add:vector_component_simps Cart_eq)
+ using inj(2)[of "2 *\<^sub>R x - 1" 1] by auto
ultimately show ?thesis by auto qed qed
lemma injective_path_join:
@@ -3045,45 +3093,41 @@
shows "injective_path(g1 +++ g2)"
unfolding injective_path_def proof(rule,rule,rule) let ?g = "g1 +++ g2"
note inj = assms(1,2)[unfolded injective_path_def, rule_format]
- have *:"\<And>x y::real^1. 2 *\<^sub>R x = 1 \<Longrightarrow> 2 *\<^sub>R y = 1 \<Longrightarrow> x = y" unfolding Cart_eq forall_1 by(auto simp del:dest_vec1_eq)
fix x y assume xy:"x \<in> {0..1}" "y \<in> {0..1}" "(g1 +++ g2) x = (g1 +++ g2) y"
- show "x = y" proof(cases "x$1 \<le> 1/2", case_tac[!] "y$1 \<le> 1/2", unfold not_le)
- assume "x $ 1 \<le> 1 / 2" "y $ 1 \<le> 1 / 2" thus ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] and xy
- unfolding mem_interval_1 joinpaths_def by(auto simp add:vector_component_simps)
- next assume "x $ 1 > 1 / 2" "y $ 1 > 1 / 2" thus ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] and xy
- unfolding mem_interval_1 joinpaths_def by(auto simp add:vector_component_simps)
- next assume as:"x $ 1 \<le> 1 / 2" "y $ 1 > 1 / 2"
+ show "x = y" proof(cases "x \<le> 1/2", case_tac[!] "y \<le> 1/2", unfold not_le)
+ assume "x \<le> 1 / 2" "y \<le> 1 / 2" thus ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] and xy
+ unfolding mem_interval_1 joinpaths_def by auto
+ next assume "x > 1 / 2" "y > 1 / 2" thus ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] and xy
+ unfolding mem_interval_1 joinpaths_def by auto
+ next assume as:"x \<le> 1 / 2" "y > 1 / 2"
hence "?g x \<in> path_image g1" "?g y \<in> path_image g2" unfolding path_image_def joinpaths_def
- using xy(1,2)[unfolded mem_interval_1] by(auto simp add:vector_component_simps intro!: imageI)
+ using xy(1,2)[unfolded mem_interval_1] by auto
hence "?g x = pathfinish g1" "?g y = pathstart g2" using assms(4) unfolding assms(3) xy(3) by auto
thus ?thesis using as and inj(1)[of "2 *\<^sub>R x" 1] inj(2)[of "2 *\<^sub>R y - 1" 0] and xy(1,2)
unfolding pathstart_def pathfinish_def joinpaths_def mem_interval_1
- by(auto simp add:vector_component_simps intro:*)
- next assume as:"x $ 1 > 1 / 2" "y $ 1 \<le> 1 / 2"
+ by auto
+ next assume as:"x > 1 / 2" "y \<le> 1 / 2"
hence "?g x \<in> path_image g2" "?g y \<in> path_image g1" unfolding path_image_def joinpaths_def
- using xy(1,2)[unfolded mem_interval_1] by(auto simp add:vector_component_simps intro!: imageI)
+ using xy(1,2)[unfolded mem_interval_1] by auto
hence "?g x = pathstart g2" "?g y = pathfinish g1" using assms(4) unfolding assms(3) xy(3) by auto
thus ?thesis using as and inj(2)[of "2 *\<^sub>R x - 1" 0] inj(1)[of "2 *\<^sub>R y" 1] and xy(1,2)
unfolding pathstart_def pathfinish_def joinpaths_def mem_interval_1
- by(auto simp add:vector_component_simps intro:*) qed qed
+ by auto qed qed
lemmas join_paths_simps = path_join path_image_join pathstart_join pathfinish_join
subsection {* Reparametrizing a closed curve to start at some chosen point. *}
-definition "shiftpath a (f::real^1 \<Rightarrow> real^'n) =
- (\<lambda>x. if dest_vec1 (a + x) \<le> 1 then f(a + x) else f(a + x - 1))"
+definition "shiftpath a (f::real \<Rightarrow> 'a::metric_space) =
+ (\<lambda>x. if (a + x) \<le> 1 then f(a + x) else f(a + x - 1))"
lemma pathstart_shiftpath: "a \<le> 1 \<Longrightarrow> pathstart(shiftpath a g) = g a"
unfolding pathstart_def shiftpath_def by auto
-(** move this **)
-declare forall_1[simp] ex_1[simp]
-
lemma pathfinish_shiftpath: assumes "0 \<le> a" "pathfinish g = pathstart g"
shows "pathfinish(shiftpath a g) = g a"
using assms unfolding pathstart_def pathfinish_def shiftpath_def
- by(auto simp add: vector_component_simps)
+ by auto
lemma endpoints_shiftpath:
assumes "pathfinish g = pathstart g" "a \<in> {0 .. 1}"
@@ -3098,39 +3142,38 @@
lemma path_shiftpath:
assumes "path g" "pathfinish g = pathstart g" "a \<in> {0..1}"
shows "path(shiftpath a g)" proof-
- have *:"{0 .. 1} = {0 .. 1-a} \<union> {1-a .. 1}" using assms(3) by(auto simp add: vector_component_simps)
+ have *:"{0 .. 1} = {0 .. 1-a} \<union> {1-a .. 1}" using assms(3) by auto
have **:"\<And>x. x + a = 1 \<Longrightarrow> g (x + a - 1) = g (x + a)"
using assms(2)[unfolded pathfinish_def pathstart_def] by auto
show ?thesis unfolding path_def shiftpath_def * apply(rule continuous_on_union)
- apply(rule closed_interval)+ apply(rule continuous_on_eq[of _ "g \<circ> (\<lambda>x. a + x)"]) prefer 3
+ apply(rule closed_real_atLeastAtMost)+ apply(rule continuous_on_eq[of _ "g \<circ> (\<lambda>x. a + x)"]) prefer 3
apply(rule continuous_on_eq[of _ "g \<circ> (\<lambda>x. a - 1 + x)"]) defer prefer 3
apply(rule continuous_on_intros)+ prefer 2 apply(rule continuous_on_intros)+
apply(rule_tac[1-2] continuous_on_subset[OF assms(1)[unfolded path_def]])
- using assms(3) and ** by(auto simp add:vector_component_simps field_simps Cart_eq) qed
+ using assms(3) and ** by(auto, auto simp add: field_simps) qed
lemma shiftpath_shiftpath: assumes "pathfinish g = pathstart g" "a \<in> {0..1}" "x \<in> {0..1}"
shows "shiftpath (1 - a) (shiftpath a g) x = g x"
- using assms unfolding pathfinish_def pathstart_def shiftpath_def
- by(auto simp add: vector_component_simps)
+ using assms unfolding pathfinish_def pathstart_def shiftpath_def by auto
lemma path_image_shiftpath:
assumes "a \<in> {0..1}" "pathfinish g = pathstart g"
shows "path_image(shiftpath a g) = path_image g" proof-
- { fix x assume as:"g 1 = g 0" "x \<in> {0..1::real^1}" " \<forall>y\<in>{0..1} \<inter> {x. \<not> a $ 1 + x $ 1 \<le> 1}. g x \<noteq> g (a + y - 1)"
- hence "\<exists>y\<in>{0..1} \<inter> {x. a $ 1 + x $ 1 \<le> 1}. g x = g (a + y)" proof(cases "a \<le> x")
+ { fix x assume as:"g 1 = g 0" "x \<in> {0..1::real}" " \<forall>y\<in>{0..1} \<inter> {x. \<not> a + x \<le> 1}. g x \<noteq> g (a + y - 1)"
+ hence "\<exists>y\<in>{0..1} \<inter> {x. a + x \<le> 1}. g x = g (a + y)" proof(cases "a \<le> x")
case False thus ?thesis apply(rule_tac x="1 + x - a" in bexI)
using as(1,2) and as(3)[THEN bspec[where x="1 + x - a"]] and assms(1)
- by(auto simp add:vector_component_simps field_simps atomize_not) next
+ by(auto simp add: field_simps atomize_not) next
case True thus ?thesis using as(1-2) and assms(1) apply(rule_tac x="x - a" in bexI)
- by(auto simp add:vector_component_simps field_simps) qed }
- thus ?thesis using assms unfolding shiftpath_def path_image_def pathfinish_def pathstart_def
- by(auto simp add:vector_component_simps image_iff) qed
+ by(auto simp add: field_simps) qed }
+ thus ?thesis using assms unfolding shiftpath_def path_image_def pathfinish_def pathstart_def
+ by(auto simp add: image_iff) qed
subsection {* Special case of straight-line paths. *}
definition
- linepath :: "real ^ 'n \<Rightarrow> real ^ 'n \<Rightarrow> real ^ 1 \<Rightarrow> real ^ 'n" where
- "linepath a b = (\<lambda>x. (1 - dest_vec1 x) *\<^sub>R a + dest_vec1 x *\<^sub>R b)"
+ linepath :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> real \<Rightarrow> 'a" where
+ "linepath a b = (\<lambda>x. (1 - x) *\<^sub>R a + x *\<^sub>R b)"
lemma pathstart_linepath[simp]: "pathstart(linepath a b) = a"
unfolding pathstart_def linepath_def by auto
@@ -3151,30 +3194,36 @@
lemma path_image_linepath[simp]: "path_image(linepath a b) = (closed_segment a b)"
unfolding path_image_def segment linepath_def apply (rule set_ext, rule) defer
unfolding mem_Collect_eq image_iff apply(erule exE) apply(rule_tac x="u *\<^sub>R 1" in bexI)
- by(auto simp add:vector_component_simps)
+ by auto
lemma reversepath_linepath[simp]: "reversepath(linepath a b) = linepath b a"
- unfolding reversepath_def linepath_def by(rule ext, auto simp add:vector_component_simps)
-
-lemma injective_path_linepath: assumes "a \<noteq> b" shows "injective_path(linepath a b)" proof-
- { obtain i where i:"a$i \<noteq> b$i" using assms[unfolded Cart_eq] by auto
- fix x y::"real^1" assume "x $ 1 *\<^sub>R b + y $ 1 *\<^sub>R a = x $ 1 *\<^sub>R a + y $ 1 *\<^sub>R b"
- hence "x$1 * (b$i - a$i) = y$1 * (b$i - a$i)" unfolding Cart_eq by(auto simp add:field_simps vector_component_simps)
- hence "x = y" unfolding mult_cancel_right Cart_eq using i(1) by(auto simp add:field_simps) }
- thus ?thesis unfolding injective_path_def linepath_def by(auto simp add:vector_component_simps algebra_simps) qed
+ unfolding reversepath_def linepath_def by(rule ext, auto)
+
+lemma injective_path_linepath:
+ assumes "a \<noteq> b" shows "injective_path(linepath a b)"
+proof -
+ { fix x y :: "real"
+ assume "x *\<^sub>R b + y *\<^sub>R a = x *\<^sub>R a + y *\<^sub>R b"
+ hence "(x - y) *\<^sub>R a = (x - y) *\<^sub>R b" by (simp add: algebra_simps)
+ with assms have "x = y" by simp }
+ thus ?thesis unfolding injective_path_def linepath_def by(auto simp add: algebra_simps) qed
lemma simple_path_linepath[intro]: "a \<noteq> b \<Longrightarrow> simple_path(linepath a b)" by(auto intro!: injective_imp_simple_path injective_path_linepath)
subsection {* Bounding a point away from a path. *}
-lemma not_on_path_ball: assumes "path g" "z \<notin> path_image g"
+lemma not_on_path_ball:
+ fixes g :: "real \<Rightarrow> 'a::heine_borel"
+ assumes "path g" "z \<notin> path_image g"
shows "\<exists>e>0. ball z e \<inter> (path_image g) = {}" proof-
obtain a where "a\<in>path_image g" "\<forall>y\<in>path_image g. dist z a \<le> dist z y"
using distance_attains_inf[OF _ path_image_nonempty, of g z]
using compact_path_image[THEN compact_imp_closed, OF assms(1)] by auto
thus ?thesis apply(rule_tac x="dist z a" in exI) using assms(2) by(auto intro!: dist_pos_lt) qed
-lemma not_on_path_cball: assumes "path g" "z \<notin> path_image g"
+lemma not_on_path_cball:
+ fixes g :: "real \<Rightarrow> 'a::heine_borel"
+ assumes "path g" "z \<notin> path_image g"
shows "\<exists>e>0. cball z e \<inter> (path_image g) = {}" proof-
obtain e where "ball z e \<inter> path_image g = {}" "e>0" using not_on_path_ball[OF assms] by auto
moreover have "cball z (e/2) \<subseteq> ball z e" using `e>0` by auto
@@ -3191,14 +3240,14 @@
lemma path_component_refl: assumes "x \<in> s" shows "path_component s x x"
unfolding path_defs apply(rule_tac x="\<lambda>u. x" in exI) using assms
- by(auto intro!:continuous_on_intros)
+ by(auto intro!:continuous_on_intros)
lemma path_component_refl_eq: "path_component s x x \<longleftrightarrow> x \<in> s"
- by(auto intro!: path_component_mem path_component_refl)
+ by(auto intro!: path_component_mem path_component_refl)
lemma path_component_sym: "path_component s x y \<Longrightarrow> path_component s y x"
- using assms unfolding path_component_def apply(erule exE) apply(rule_tac x="reversepath g" in exI)
- by(auto simp add: reversepath_simps)
+ using assms unfolding path_component_def apply(erule exE) apply(rule_tac x="reversepath g" in exI)
+ by auto
lemma path_component_trans: assumes "path_component s x y" "path_component s y z" shows "path_component s x z"
using assms unfolding path_component_def apply- apply(erule exE)+ apply(rule_tac x="g +++ ga" in exI) by(auto simp add: path_image_join)
@@ -3233,7 +3282,9 @@
subsection {* Some useful lemmas about path-connectedness. *}
-lemma convex_imp_path_connected: assumes "convex s" shows "path_connected s"
+lemma convex_imp_path_connected:
+ fixes s :: "'a::real_normed_vector set"
+ assumes "convex s" shows "path_connected s"
unfolding path_connected_def apply(rule,rule,rule_tac x="linepath x y" in exI)
unfolding path_image_linepath using assms[unfolded convex_contains_segment] by auto
@@ -3243,15 +3294,18 @@
then obtain x1 x2 where obt:"x1\<in>e1\<inter>s" "x2\<in>e2\<inter>s" by auto
then obtain g where g:"path g" "path_image g \<subseteq> s" "pathstart g = x1" "pathfinish g = x2"
using assms[unfolded path_connected_def,rule_format,of x1 x2] by auto
- have *:"connected {0..1::real^1}" by(auto intro!: convex_connected convex_interval)
+ have *:"connected {0..1::real}" by(auto intro!: convex_connected convex_real_interval)
have "{0..1} \<subseteq> {x \<in> {0..1}. g x \<in> e1} \<union> {x \<in> {0..1}. g x \<in> e2}" using as(3) g(2)[unfolded path_defs] by blast
moreover have "{x \<in> {0..1}. g x \<in> e1} \<inter> {x \<in> {0..1}. g x \<in> e2} = {}" using as(4) g(2)[unfolded path_defs] unfolding subset_eq by auto
- moreover have "{x \<in> {0..1}. g x \<in> e1} \<noteq> {} \<and> {x \<in> {0..1}. g x \<in> e2} \<noteq> {}" using g(3,4)[unfolded path_defs] using obt by(auto intro!: exI)
+ moreover have "{x \<in> {0..1}. g x \<in> e1} \<noteq> {} \<and> {x \<in> {0..1}. g x \<in> e2} \<noteq> {}" using g(3,4)[unfolded path_defs] using obt
+ by (simp add: ex_in_conv [symmetric], metis zero_le_one order_refl)
ultimately show False using *[unfolded connected_local not_ex,rule_format, of "{x\<in>{0..1}. g x \<in> e1}" "{x\<in>{0..1}. g x \<in> e2}"]
using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(1)]
using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(2)] by auto qed
-lemma open_path_component: assumes "open s" shows "open(path_component s x)"
+lemma open_path_component:
+ fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*)
+ assumes "open s" shows "open(path_component s x)"
unfolding open_contains_ball proof
fix y assume as:"y \<in> path_component s x"
hence "y\<in>s" apply- apply(rule path_component_mem(2)) unfolding mem_def by auto
@@ -3261,7 +3315,10 @@
apply(rule path_component_of_subset[OF e(2)]) apply(rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format]) using `e>0`
using as[unfolded mem_def] by auto qed qed
-lemma open_non_path_component: assumes "open s" shows "open(s - path_component s x)" unfolding open_contains_ball proof
+lemma open_non_path_component:
+ fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*)
+ assumes "open s" shows "open(s - path_component s x)"
+ unfolding open_contains_ball proof
fix y assume as:"y\<in>s - path_component s x"
then obtain e where e:"e>0" "ball y e \<subseteq> s" using assms[unfolded open_contains_ball] by auto
show "\<exists>e>0. ball y e \<subseteq> s - path_component s x" apply(rule_tac x=e in exI) apply(rule,rule `e>0`,rule,rule) defer proof(rule ccontr)
@@ -3271,7 +3328,9 @@
apply(rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format]) by auto
thus False using as by auto qed(insert e(2), auto) qed
-lemma connected_open_path_connected: assumes "open s" "connected s" shows "path_connected s"
+lemma connected_open_path_connected:
+ fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*)
+ assumes "open s" "connected s" shows "path_connected s"
unfolding path_connected_component_set proof(rule,rule,rule path_component_subset, rule)
fix x y assume "x \<in> s" "y \<in> s" show "y \<in> path_component s x" proof(rule ccontr)
assume "y \<notin> path_component s x" moreover
@@ -3300,8 +3359,10 @@
unfolding path_connected_def by auto
lemma path_connected_singleton: "path_connected {a}"
- unfolding path_connected_def apply(rule,rule)
- apply(rule_tac x="linepath a a" in exI) by(auto simp add:segment scaleR_left_diff_distrib)
+ unfolding path_connected_def pathstart_def pathfinish_def path_image_def
+ apply (clarify, rule_tac x="\<lambda>x. a" in exI, simp add: image_constant_conv)
+ apply (simp add: path_def continuous_on_const)
+ done
lemma path_connected_Un: assumes "path_connected s" "path_connected t" "s \<inter> t \<noteq> {}"
shows "path_connected (s \<union> t)" unfolding path_connected_component proof(rule,rule)
--- a/src/HOL/Nominal/nominal_inductive.ML Sun Apr 25 08:25:34 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Mon Apr 26 07:47:18 2010 +0200
@@ -543,7 +543,7 @@
in
ctxt'' |>
- Proof.theorem_i NONE (fn thss => fn ctxt =>
+ Proof.theorem NONE (fn thss => fn ctxt =>
let
val rec_name = space_implode "_" (map Long_Name.base_name names);
val rec_qualified = Binding.qualify false rec_name;
--- a/src/HOL/Nominal/nominal_inductive2.ML Sun Apr 25 08:25:34 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Mon Apr 26 07:47:18 2010 +0200
@@ -445,7 +445,7 @@
in
ctxt'' |>
- Proof.theorem_i NONE (fn thss => fn ctxt =>
+ Proof.theorem NONE (fn thss => fn ctxt =>
let
val rec_name = space_implode "_" (map Long_Name.base_name names);
val rec_qualified = Binding.qualify false rec_name;
--- a/src/HOL/Nominal/nominal_primrec.ML Sun Apr 25 08:25:34 2010 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Mon Apr 26 07:47:18 2010 +0200
@@ -363,7 +363,7 @@
in
lthy' |>
Variable.add_fixes (map fst lsrs) |> snd |>
- Proof.theorem_i NONE
+ Proof.theorem NONE
(fn thss => fn goal_ctxt =>
let
val simps = ProofContext.export goal_ctxt lthy' (flat thss);
--- a/src/HOL/Tools/Datatype/datatype_data.ML Sun Apr 25 08:25:34 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Mon Apr 26 07:47:18 2010 +0200
@@ -436,7 +436,7 @@
in
thy
|> ProofContext.init
- |> Proof.theorem_i NONE after_qed' ((map o map) (rpair []) (flat rules))
+ |> Proof.theorem NONE after_qed' ((map o map) (rpair []) (flat rules))
end;
val rep_datatype = gen_rep_datatype Sign.cert_term;
--- a/src/HOL/Tools/Function/function.ML Sun Apr 25 08:25:34 2010 +0200
+++ b/src/HOL/Tools/Function/function.ML Mon Apr 26 07:47:18 2010 +0200
@@ -120,7 +120,7 @@
end
in
lthy
- |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
+ |> Proof.theorem NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
|> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
end
@@ -177,7 +177,7 @@
|> ProofContext.note_thmss ""
[((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),
[([Goal.norm_result termination], [])])] |> snd
- |> Proof.theorem_i NONE afterqed [[(goal, [])]]
+ |> Proof.theorem NONE afterqed [[(goal, [])]]
end
val termination_proof = gen_termination_proof Syntax.check_term
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Apr 25 08:25:34 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Apr 26 07:47:18 2010 +0200
@@ -3059,7 +3059,7 @@
) options [const]))
end
in
- Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy''
+ Proof.theorem NONE after_qed (map (single o (rpair [])) cases_rules) lthy''
end;
val code_pred = generic_code_pred (K I);
--- a/src/HOL/Tools/Quotient/quotient_typ.ML Sun Apr 25 08:25:34 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML Mon Apr 26 07:47:18 2010 +0200
@@ -45,7 +45,7 @@
val goals' = map (rpair []) goals
fun after_qed' thms = after_qed (the_single thms)
in
- Proof.theorem_i NONE after_qed' [goals'] ctxt
+ Proof.theorem NONE after_qed' [goals'] ctxt
end
--- a/src/HOL/Tools/choice_specification.ML Sun Apr 25 08:25:34 2010 +0200
+++ b/src/HOL/Tools/choice_specification.ML Mon Apr 26 07:47:18 2010 +0200
@@ -226,7 +226,7 @@
in
thy
|> ProofContext.init
- |> Proof.theorem_i NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]]
+ |> Proof.theorem NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]]
end;
--- a/src/HOL/Tools/typedef.ML Sun Apr 25 08:25:34 2010 +0200
+++ b/src/HOL/Tools/typedef.ML Mon Apr 26 07:47:18 2010 +0200
@@ -282,7 +282,7 @@
val ((goal, goal_pat, typedef_result), lthy') =
prepare_typedef prep_term def name (b, args, mx) set opt_morphs lthy;
fun after_qed [[th]] = snd o typedef_result th;
- in Proof.theorem_i NONE after_qed [[(goal, [goal_pat])]] lthy' end;
+ in Proof.theorem NONE after_qed [[(goal, [goal_pat])]] lthy' end;
in
--- a/src/HOLCF/Tools/pcpodef.ML Sun Apr 25 08:25:34 2010 +0200
+++ b/src/HOLCF/Tools/pcpodef.ML Mon Apr 26 07:47:18 2010 +0200
@@ -328,7 +328,7 @@
prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy;
fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
| after_qed _ = raise Fail "cpodef_proof";
- in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
+ in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
fun gen_pcpodef_proof prep_term prep_constraint
((def, name), (b, raw_args, mx), set, opt_morphs) thy =
@@ -339,7 +339,7 @@
prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy;
fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
| after_qed _ = raise Fail "pcpodef_proof";
- in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
+ in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
in
--- a/src/Pure/Isar/calculation.ML Sun Apr 25 08:25:34 2010 +0200
+++ b/src/Pure/Isar/calculation.ML Mon Apr 26 07:47:18 2010 +0200
@@ -13,11 +13,11 @@
val sym_add: attribute
val sym_del: attribute
val symmetric: attribute
- val also: (Facts.ref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
- val also_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
- val finally: (Facts.ref * Attrib.src list) list option -> bool ->
+ val also: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
+ val also_cmd: (Facts.ref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
+ val finally: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
+ val finally_cmd: (Facts.ref * Attrib.src list) list option -> bool ->
Proof.state -> Proof.state Seq.seq
- val finally_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
val moreover: bool -> Proof.state -> Proof.state
val ultimately: bool -> Proof.state -> Proof.state
end;
@@ -148,10 +148,10 @@
state |> maintain_calculation final calc))
end;
-val also = calculate Proof.get_thmss false;
-val also_i = calculate (K I) false;
-val finally = calculate Proof.get_thmss true;
-val finally_i = calculate (K I) true;
+val also = calculate (K I) false;
+val also_cmd = calculate Proof.get_thmss_cmd false;
+val finally = calculate (K I) true;
+val finally_cmd = calculate Proof.get_thmss_cmd true;
(* moreover and ultimately *)
--- a/src/Pure/Isar/class_target.ML Sun Apr 25 08:25:34 2010 +0200
+++ b/src/Pure/Isar/class_target.ML Mon Apr 26 07:47:18 2010 +0200
@@ -163,7 +163,7 @@
Symtab.empty
|> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) =>
Symtab.map_default (class, []) (insert (op =) tyco)) arities)
- ((#arities o Sorts.rep_algebra) algebra);
+ (Sorts.arities_of algebra);
val the_arities = these o Symtab.lookup arities;
fun mk_arity class tyco =
let
@@ -370,7 +370,7 @@
in
thy
|> ProofContext.init
- |> Proof.theorem_i NONE after_qed [[(mk_prop thy classrel, [])]]
+ |> Proof.theorem NONE after_qed [[(mk_prop thy classrel, [])]]
end;
in
@@ -539,7 +539,7 @@
end;
val instantiation_instance = gen_instantiation_instance (fn after_qed => fn ts =>
- Proof.theorem_i NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts));
+ Proof.theorem NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts));
fun prove_instantiation_instance tac = gen_instantiation_instance (fn after_qed =>
fn ts => fn lthy => after_qed (map (fn t => Goal.prove lthy [] [] t
@@ -595,7 +595,7 @@
in
thy
|> ProofContext.init
- |> Proof.theorem_i NONE after_qed (map (fn t => [(t, [])]) arities)
+ |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) arities)
end;
--- a/src/Pure/Isar/element.ML Sun Apr 25 08:25:34 2010 +0200
+++ b/src/Pure/Isar/element.ML Mon Apr 26 07:47:18 2010 +0200
@@ -283,10 +283,10 @@
in
fun witness_proof after_qed wit_propss =
- gen_witness_proof (Proof.theorem_i NONE) (fn wits => fn _ => after_qed wits)
+ gen_witness_proof (Proof.theorem NONE) (fn wits => fn _ => after_qed wits)
wit_propss [];
-val witness_proof_eqs = gen_witness_proof (Proof.theorem_i NONE);
+val witness_proof_eqs = gen_witness_proof (Proof.theorem NONE);
fun witness_local_proof after_qed cmd wit_propss goal_ctxt int =
gen_witness_proof (fn after_qed' => fn propss =>
--- a/src/Pure/Isar/isar_cmd.ML Sun Apr 25 08:25:34 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Mon Apr 26 07:47:18 2010 +0200
@@ -219,10 +219,10 @@
fun goal opt_chain goal stmt int =
opt_chain #> goal NONE (K I) stmt int;
-val have = goal I Proof.have;
-val hence = goal Proof.chain Proof.have;
-val show = goal I Proof.show;
-val thus = goal Proof.chain Proof.show;
+val have = goal I Proof.have_cmd;
+val hence = goal Proof.chain Proof.have_cmd;
+val show = goal I Proof.show_cmd;
+val thus = goal Proof.chain Proof.show_cmd;
(* local endings *)
@@ -393,7 +393,7 @@
let
val thy = Toplevel.theory_of state;
val {classes = (space, algebra), ...} = Type.rep_tsig (Sign.tsig_of thy);
- val {classes, ...} = Sorts.rep_algebra algebra;
+ val classes = Sorts.classes_of algebra;
fun entry (c, (i, (_, cs))) =
(i, {name = Name_Space.extern space c, ID = c, parents = cs,
dir = "", unfold = true, path = ""});
@@ -403,7 +403,7 @@
in Present.display_graph gr end);
fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
- Thm_Deps.thm_deps (Proof.get_thmss (Toplevel.enter_proof_body state) args));
+ Thm_Deps.thm_deps (Proof.get_thmss_cmd (Toplevel.enter_proof_body state) args));
(* find unused theorems *)
@@ -437,12 +437,12 @@
local
fun string_of_stmts state args =
- Proof.get_thmss state args
+ Proof.get_thmss_cmd state args
|> map (Element.pretty_statement (Proof.context_of state) Thm.theoremK)
|> Pretty.chunks2 |> Pretty.string_of;
fun string_of_thms state args =
- Pretty.string_of (Display.pretty_thms (Proof.context_of state) (Proof.get_thmss state args));
+ Pretty.string_of (Display.pretty_thms (Proof.context_of state) (Proof.get_thmss_cmd state args));
fun string_of_prfs full state arg =
Pretty.string_of
@@ -460,7 +460,7 @@
end
| SOME args => Pretty.chunks
(map (Proof_Syntax.pretty_proof_of (Proof.context_of state) full)
- (Proof.get_thmss state args)));
+ (Proof.get_thmss_cmd state args)));
fun string_of_prop state s =
let
--- a/src/Pure/Isar/isar_syn.ML Sun Apr 25 08:25:34 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML Mon Apr 26 07:47:18 2010 +0200
@@ -542,27 +542,27 @@
val _ =
OuterSyntax.command "from" "forward chaining from given facts"
(K.tag_proof K.prf_chain)
- (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss)));
+ (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss_cmd)));
val _ =
OuterSyntax.command "with" "forward chaining from given and current facts"
(K.tag_proof K.prf_chain)
- (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss)));
+ (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss_cmd)));
val _ =
OuterSyntax.command "note" "define facts"
(K.tag_proof K.prf_decl)
- (SpecParse.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss)));
+ (SpecParse.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss_cmd)));
val _ =
OuterSyntax.command "using" "augment goal facts"
(K.tag_proof K.prf_decl)
- (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using)));
+ (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using_cmd)));
val _ =
OuterSyntax.command "unfolding" "unfold definitions in goal and facts"
(K.tag_proof K.prf_decl)
- (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding)));
+ (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding_cmd)));
(* proof context *)
@@ -570,17 +570,17 @@
val _ =
OuterSyntax.command "fix" "fix local variables (Skolem constants)"
(K.tag_proof K.prf_asm)
- (P.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix)));
+ (P.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix_cmd)));
val _ =
OuterSyntax.command "assume" "assume propositions"
(K.tag_proof K.prf_asm)
- (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume)));
+ (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd)));
val _ =
OuterSyntax.command "presume" "assume propositions, to be established later"
(K.tag_proof K.prf_asm)
- (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume)));
+ (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd)));
val _ =
OuterSyntax.command "def" "local definition"
@@ -588,24 +588,24 @@
(P.and_list1
(SpecParse.opt_thm_name ":" --
((P.binding -- P.opt_mixfix) -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp)))
- >> (Toplevel.print oo (Toplevel.proof o Proof.def)));
+ >> (Toplevel.print oo (Toplevel.proof o Proof.def_cmd)));
val _ =
OuterSyntax.command "obtain" "generalized existence"
(K.tag_proof K.prf_asm_goal)
(P.parname -- Scan.optional (P.fixes --| P.where_) [] -- SpecParse.statement
- >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain x y z)));
+ >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain_cmd x y z)));
val _ =
OuterSyntax.command "guess" "wild guessing (unstructured)"
(K.tag_proof K.prf_asm_goal)
- (Scan.optional P.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess)));
+ (Scan.optional P.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess_cmd)));
val _ =
OuterSyntax.command "let" "bind text variables"
(K.tag_proof K.prf_decl)
(P.and_list1 (P.and_list1 P.term -- (P.$$$ "=" |-- P.term))
- >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind)));
+ >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind_cmd)));
val case_spec =
(P.$$$ "(" |-- P.!!! (P.xname -- Scan.repeat1 (P.maybe P.name) --| P.$$$ ")") ||
@@ -614,7 +614,7 @@
val _ =
OuterSyntax.command "case" "invoke local context"
(K.tag_proof K.prf_asm)
- (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case)));
+ (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case_cmd)));
(* proof structure *)
@@ -711,12 +711,12 @@
val _ =
OuterSyntax.command "also" "combine calculation and current facts"
(K.tag_proof K.prf_decl)
- (calc_args >> (Toplevel.proofs' o Calculation.also));
+ (calc_args >> (Toplevel.proofs' o Calculation.also_cmd));
val _ =
OuterSyntax.command "finally" "combine calculation and current facts, exhibit result"
(K.tag_proof K.prf_chain)
- (calc_args >> (Toplevel.proofs' o Calculation.finally));
+ (calc_args >> (Toplevel.proofs' o Calculation.finally_cmd));
val _ =
OuterSyntax.command "moreover" "augment calculation by current facts"
--- a/src/Pure/Isar/obtain.ML Sun Apr 25 08:25:34 2010 +0200
+++ b/src/Pure/Isar/obtain.ML Mon Apr 26 07:47:18 2010 +0200
@@ -39,14 +39,14 @@
signature OBTAIN =
sig
val thatN: string
- val obtain: string -> (binding * string option * mixfix) list ->
+ val obtain: string -> (binding * typ option * mixfix) list ->
+ (Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state
+ val obtain_cmd: string -> (binding * string option * mixfix) list ->
(Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
- val obtain_i: string -> (binding * typ option * mixfix) list ->
- (Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state
val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
((string * cterm) list * thm list) * Proof.context
- val guess: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
- val guess_i: (binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
+ val guess: (binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
+ val guess_cmd: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
end;
structure Obtain: OBTAIN =
@@ -148,26 +148,26 @@
fun after_qed _ =
Proof.local_qed (NONE, false)
#> `Proof.the_fact #-> (fn rule =>
- Proof.fix_i vars
- #> Proof.assm_i (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms);
+ Proof.fix vars
+ #> Proof.assm (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms);
in
state
|> Proof.enter_forward
- |> Proof.have_i NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int
+ |> Proof.have NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int
|> Proof.proof (SOME Method.succeed_text) |> Seq.hd
- |> Proof.fix_i [(Binding.name thesisN, NONE, NoSyn)]
- |> Proof.assume_i
+ |> Proof.fix [(Binding.name thesisN, NONE, NoSyn)]
+ |> Proof.assume
[((Binding.name that_name, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
|> `Proof.the_facts
||> Proof.chain_facts chain_facts
- ||> Proof.show_i NONE after_qed [(Thm.empty_binding, [(thesis, [])])] false
+ ||> Proof.show NONE after_qed [(Thm.empty_binding, [(thesis, [])])] false
|-> Proof.refine_insert
end;
in
-val obtain = gen_obtain Attrib.attribute ProofContext.read_vars ProofContext.read_propp;
-val obtain_i = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp;
+val obtain = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp;
+val obtain_cmd = gen_obtain Attrib.attribute ProofContext.read_vars ProofContext.read_propp;
end;
@@ -290,8 +290,8 @@
in
state'
|> Proof.map_context (K ctxt')
- |> Proof.fix_i (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
- |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm_i
+ |> Proof.fix (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
+ |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm
(obtain_export fix_ctxt rule (map cert ts)) [(Thm.empty_binding, asms)])
|> Proof.bind_terms Auto_Bind.no_facts
end;
@@ -307,7 +307,7 @@
state
|> Proof.enter_forward
|> Proof.begin_block
- |> Proof.fix_i [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
+ |> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
|> Proof.chain_facts chain_facts
|> Proof.local_goal print_result (K I) (apsnd (rpair I))
"guess" before_qed after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])]
@@ -316,8 +316,8 @@
in
-val guess = gen_guess ProofContext.read_vars;
-val guess_i = gen_guess ProofContext.cert_vars;
+val guess = gen_guess ProofContext.cert_vars;
+val guess_cmd = gen_guess ProofContext.read_vars;
end;
--- a/src/Pure/Isar/proof.ML Sun Apr 25 08:25:34 2010 +0200
+++ b/src/Pure/Isar/proof.ML Mon Apr 26 07:47:18 2010 +0200
@@ -41,37 +41,35 @@
val raw_goal: state -> {context: context, facts: thm list, goal: thm}
val goal: state -> {context: context, facts: thm list, goal: thm}
val simple_goal: state -> {context: context, goal: thm}
- val match_bind: (string list * string) list -> state -> state
- val match_bind_i: (term list * term) list -> state -> state
- val let_bind: (string list * string) list -> state -> state
- val let_bind_i: (term list * term) list -> state -> state
- val fix: (binding * string option * mixfix) list -> state -> state
- val fix_i: (binding * typ option * mixfix) list -> state -> state
+ val let_bind: (term list * term) list -> state -> state
+ val let_bind_cmd: (string list * string) list -> state -> state
+ val fix: (binding * typ option * mixfix) list -> state -> state
+ val fix_cmd: (binding * string option * mixfix) list -> state -> state
val assm: Assumption.export ->
+ (Thm.binding * (term * term list) list) list -> state -> state
+ val assm_cmd: Assumption.export ->
(Attrib.binding * (string * string list) list) list -> state -> state
- val assm_i: Assumption.export ->
- (Thm.binding * (term * term list) list) list -> state -> state
- val assume: (Attrib.binding * (string * string list) list) list -> state -> state
- val assume_i: (Thm.binding * (term * term list) list) list -> state -> state
- val presume: (Attrib.binding * (string * string list) list) list -> state -> state
- val presume_i: (Thm.binding * (term * term list) list) list -> state -> state
- val def: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
- val def_i: (Thm.binding * ((binding * mixfix) * (term * term list))) list -> state -> state
+ val assume: (Thm.binding * (term * term list) list) list -> state -> state
+ val assume_cmd: (Attrib.binding * (string * string list) list) list -> state -> state
+ val presume: (Thm.binding * (term * term list) list) list -> state -> state
+ val presume_cmd: (Attrib.binding * (string * string list) list) list -> state -> state
+ val def: (Thm.binding * ((binding * mixfix) * (term * term list))) list -> state -> state
+ val def_cmd: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
val chain: state -> state
val chain_facts: thm list -> state -> state
- val get_thmss: state -> (Facts.ref * Attrib.src list) list -> thm list
- val note_thmss: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
- val note_thmss_i: (Thm.binding * (thm list * attribute list) list) list -> state -> state
- val from_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
- val from_thmss_i: ((thm list * attribute list) list) list -> state -> state
- val with_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
- val with_thmss_i: ((thm list * attribute list) list) list -> state -> state
- val using: ((Facts.ref * Attrib.src list) list) list -> state -> state
- val using_i: ((thm list * attribute list) list) list -> state -> state
- val unfolding: ((Facts.ref * Attrib.src list) list) list -> state -> state
- val unfolding_i: ((thm list * attribute list) list) list -> state -> state
- val invoke_case: string * string option list * Attrib.src list -> state -> state
- val invoke_case_i: string * string option list * attribute list -> state -> state
+ val get_thmss_cmd: state -> (Facts.ref * Attrib.src list) list -> thm list
+ val note_thmss: (Thm.binding * (thm list * attribute list) list) list -> state -> state
+ val note_thmss_cmd: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
+ val from_thmss: ((thm list * attribute list) list) list -> state -> state
+ val from_thmss_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
+ val with_thmss: ((thm list * attribute list) list) list -> state -> state
+ val with_thmss_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
+ val using: ((thm list * attribute list) list) list -> state -> state
+ val using_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
+ val unfolding: ((thm list * attribute list) list) list -> state -> state
+ val unfolding_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
+ val invoke_case: string * string option list * attribute list -> state -> state
+ val invoke_case_cmd: string * string option list * Attrib.src list -> state -> state
val begin_block: state -> state
val next_block: state -> state
val end_block: state -> state
@@ -87,9 +85,9 @@
((binding * 'a list) * 'b) list -> state -> state
val local_qed: Method.text option * bool -> state -> state
val theorem: Method.text option -> (thm list list -> context -> context) ->
+ (term * term list) list list -> context -> state
+ val theorem_cmd: Method.text option -> (thm list list -> context -> context) ->
(string * string list) list list -> context -> state
- val theorem_i: Method.text option -> (thm list list -> context -> context) ->
- (term * term list) list list -> context -> state
val global_qed: Method.text option * bool -> state -> context
val local_terminal_proof: Method.text * Method.text option -> state -> state
val local_default_proof: state -> state
@@ -102,13 +100,13 @@
val global_skip_proof: bool -> state -> context
val global_done_proof: state -> context
val have: Method.text option -> (thm list list -> state -> state) ->
+ (Thm.binding * (term * term list) list) list -> bool -> state -> state
+ val have_cmd: Method.text option -> (thm list list -> state -> state) ->
(Attrib.binding * (string * string list) list) list -> bool -> state -> state
- val have_i: Method.text option -> (thm list list -> state -> state) ->
- (Thm.binding * (term * term list) list) list -> bool -> state -> state
val show: Method.text option -> (thm list list -> state -> state) ->
+ (Thm.binding * (term * term list) list) list -> bool -> state -> state
+ val show_cmd: Method.text option -> (thm list list -> state -> state) ->
(Attrib.binding * (string * string list) list) list -> bool -> state -> state
- val show_i: Method.text option -> (thm list list -> state -> state) ->
- (Thm.binding * (term * term list) list) list -> bool -> state -> state
val schematic_goal: state -> bool
val is_relevant: state -> bool
val local_future_proof: (state -> ('a * state) Future.future) ->
@@ -523,22 +521,20 @@
(** context elements **)
-(* bindings *)
+(* let bindings *)
local
fun gen_bind bind args state =
state
|> assert_forward
- |> map_context (bind args #> snd)
+ |> map_context (bind true args #> snd)
|> put_facts NONE;
in
-val match_bind = gen_bind (ProofContext.match_bind false);
-val match_bind_i = gen_bind (ProofContext.match_bind_i false);
-val let_bind = gen_bind (ProofContext.match_bind true);
-val let_bind_i = gen_bind (ProofContext.match_bind_i true);
+val let_bind = gen_bind ProofContext.match_bind_i;
+val let_bind_cmd = gen_bind ProofContext.match_bind;
end;
@@ -554,8 +550,8 @@
in
-val fix = gen_fix (fn ctxt => fn args => fst (ProofContext.read_vars args ctxt));
-val fix_i = gen_fix (K I);
+val fix = gen_fix (K I);
+val fix_cmd = gen_fix (fn ctxt => fn args => fst (ProofContext.read_vars args ctxt));
end;
@@ -572,12 +568,12 @@
in
-val assm = gen_assume ProofContext.add_assms Attrib.attribute;
-val assm_i = gen_assume ProofContext.add_assms_i (K I);
-val assume = assm Assumption.assume_export;
-val assume_i = assm_i Assumption.assume_export;
-val presume = assm Assumption.presume_export;
-val presume_i = assm_i Assumption.presume_export;
+val assm = gen_assume ProofContext.add_assms_i (K I);
+val assm_cmd = gen_assume ProofContext.add_assms Attrib.attribute;
+val assume = assm Assumption.assume_export;
+val assume_cmd = assm_cmd Assumption.assume_export;
+val presume = assm Assumption.presume_export;
+val presume_cmd = assm_cmd Assumption.presume_export;
end;
@@ -605,8 +601,8 @@
in
-val def = gen_def Attrib.attribute ProofContext.read_vars ProofContext.match_bind;
-val def_i = gen_def (K I) ProofContext.cert_vars ProofContext.match_bind_i;
+val def = gen_def (K I) ProofContext.cert_vars ProofContext.match_bind_i;
+val def_cmd = gen_def Attrib.attribute ProofContext.read_vars ProofContext.match_bind;
end;
@@ -646,18 +642,18 @@
in
-val note_thmss = gen_thmss (K []) I #2 Attrib.attribute ProofContext.get_fact;
-val note_thmss_i = gen_thmss (K []) I #2 (K I) (K I);
+val note_thmss = gen_thmss (K []) I #2 (K I) (K I);
+val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute ProofContext.get_fact;
-val from_thmss = gen_thmss (K []) chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
-val from_thmss_i = gen_thmss (K []) chain #2 (K I) (K I) o no_binding;
+val from_thmss = gen_thmss (K []) chain #2 (K I) (K I) o no_binding;
+val from_thmss_cmd = gen_thmss (K []) chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
-val with_thmss = gen_thmss the_facts chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
-val with_thmss_i = gen_thmss the_facts chain #2 (K I) (K I) o no_binding;
+val with_thmss = gen_thmss the_facts chain #2 (K I) (K I) o no_binding;
+val with_thmss_cmd = gen_thmss the_facts chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
-fun get_thmss state srcs = the_facts (note_thmss [((Binding.empty, []), srcs)] state);
+fun get_thmss_cmd state srcs = the_facts (note_thmss_cmd [((Binding.empty, []), srcs)] state);
end;
@@ -686,10 +682,10 @@
in
-val using = gen_using append_using (K (K I)) Attrib.attribute ProofContext.get_fact;
-val using_i = gen_using append_using (K (K I)) (K I) (K I);
-val unfolding = gen_using unfold_using unfold_goals Attrib.attribute ProofContext.get_fact;
-val unfolding_i = gen_using unfold_using unfold_goals (K I) (K I);
+val using = gen_using append_using (K (K I)) (K I) (K I);
+val using_cmd = gen_using append_using (K (K I)) Attrib.attribute ProofContext.get_fact;
+val unfolding = gen_using unfold_using unfold_goals (K I) (K I);
+val unfolding_cmd = gen_using unfold_using unfold_goals Attrib.attribute ProofContext.get_fact;
end;
@@ -709,15 +705,15 @@
val assumptions = asms |> map (fn (a, ts) => ((qualified_binding a, atts), map (rpair []) ts));
in
state'
- |> assume_i assumptions
+ |> assume assumptions
|> bind_terms Auto_Bind.no_facts
- |> `the_facts |-> (fn thms => note_thmss_i [((Binding.name name, []), [(thms, [])])])
+ |> `the_facts |-> (fn thms => note_thmss [((Binding.name name, []), [(thms, [])])])
end;
in
-val invoke_case = gen_invoke_case Attrib.attribute;
-val invoke_case_i = gen_invoke_case (K I);
+val invoke_case = gen_invoke_case (K I);
+val invoke_case_cmd = gen_invoke_case Attrib.attribute;
end;
@@ -790,15 +786,16 @@
local
-fun implicit_vars dest add props =
+val is_var =
+ can (dest_TVar o Logic.dest_type o Logic.dest_term) orf
+ can (dest_Var o Logic.dest_term);
+
+fun implicit_vars props =
let
- val (explicit_vars, props') = take_prefix (can dest) props |>> map dest;
- val vars = rev (subtract (op =) explicit_vars (fold add props []));
- val _ =
- if null vars then ()
- else warning ("Goal statement contains unbound schematic variable(s): " ^
- commas_quote (map (Term.string_of_vname o fst) vars));
- in (rev vars, props') end;
+ val (var_props, props') = take_prefix is_var props;
+ val explicit_vars = fold Term.add_vars var_props [];
+ val vars = filter_out (member (op =) explicit_vars) (fold Term.add_vars props []);
+ in map (Logic.mk_term o Var) vars end;
fun refine_terms n =
refine (Method.Basic (K (RAW_METHOD
@@ -823,11 +820,8 @@
|> map_context_result (fn ctxt => swap (prepp (ctxt, raw_propp)));
val props = flat propss;
- val (_, props') =
- implicit_vars (dest_TVar o Logic.dest_type o Logic.dest_term) Term.add_tvars props;
- val (vars, _) = implicit_vars (dest_Var o Logic.dest_term) Term.add_vars props';
-
- val propss' = map (Logic.mk_term o Var) vars :: propss;
+ val vars = implicit_vars props;
+ val propss' = vars :: propss;
val goal_propss = filter_out null propss';
val goal =
cert (Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss))
@@ -903,8 +897,8 @@
init ctxt
|> generic_goal (prepp #> ProofContext.auto_fixes) "" before_qed (K I, after_qed) propp;
-val theorem = global_goal ProofContext.bind_propp_schematic;
-val theorem_i = global_goal ProofContext.bind_propp_schematic_i;
+val theorem = global_goal ProofContext.bind_propp_schematic_i;
+val theorem_cmd = global_goal ProofContext.bind_propp_schematic;
fun global_qeds txt =
end_proof true txt
@@ -976,10 +970,10 @@
in
-val have = gen_have Attrib.attribute ProofContext.bind_propp;
-val have_i = gen_have (K I) ProofContext.bind_propp_i;
-val show = gen_show Attrib.attribute ProofContext.bind_propp;
-val show_i = gen_show (K I) ProofContext.bind_propp_i;
+val have = gen_have (K I) ProofContext.bind_propp_i;
+val have_cmd = gen_have Attrib.attribute ProofContext.bind_propp;
+val show = gen_show (K I) ProofContext.bind_propp_i;
+val show_cmd = gen_show Attrib.attribute ProofContext.bind_propp;
end;
--- a/src/Pure/Isar/specification.ML Sun Apr 25 08:25:34 2010 +0200
+++ b/src/Pure/Isar/specification.ML Mon Apr 26 07:47:18 2010 +0200
@@ -403,7 +403,7 @@
goal_ctxt
|> ProofContext.note_thmss "" [((Binding.name Auto_Bind.assmsN, []), [(prems, [])])]
|> snd
- |> Proof.theorem_i before_qed after_qed' (map snd stmt)
+ |> Proof.theorem before_qed after_qed' (map snd stmt)
|> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
|> tap (fn state => not schematic andalso Proof.schematic_goal state andalso
error "Illegal schematic goal statement")
--- a/src/Pure/ML/ml_thms.ML Sun Apr 25 08:25:34 2010 +0200
+++ b/src/Pure/ML/ml_thms.ML Mon Apr 26 07:47:18 2010 +0200
@@ -64,7 +64,7 @@
fun after_qed res goal_ctxt =
put_thms (i, map prep_result (ProofContext.export goal_ctxt ctxt (flat res))) goal_ctxt;
val ctxt' = ctxt
- |> Proof.theorem_i NONE after_qed propss
+ |> Proof.theorem NONE after_qed propss
|> Proof.global_terminal_proof methods;
val (a, background') = background
|> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i);
--- a/src/Pure/Thy/thy_output.ML Sun Apr 25 08:25:34 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML Mon Apr 26 07:47:18 2010 +0200
@@ -574,7 +574,7 @@
val prop_src =
(case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos));
val _ = context
- |> Proof.theorem_i NONE (K I) [[(prop, [])]]
+ |> Proof.theorem NONE (K I) [[(prop, [])]]
|> Proof.global_terminal_proof methods;
in output (maybe_pretty_source (pretty_term context) prop_src [prop]) end);
--- a/src/Pure/axclass.ML Sun Apr 25 08:25:34 2010 +0200
+++ b/src/Pure/axclass.ML Mon Apr 26 07:47:18 2010 +0200
@@ -13,8 +13,8 @@
val add_arity: thm -> theory -> theory
val prove_classrel: class * class -> tactic -> theory -> theory
val prove_arity: string * sort list * sort -> tactic -> theory -> theory
- val get_info: theory -> class ->
- {def: thm, intro: thm, axioms: thm list, params: (string * typ) list}
+ type info = {def: thm, intro: thm, axioms: thm list, params: (string * typ) list}
+ val get_info: theory -> class -> info
val class_intros: theory -> thm list
val class_of_param: theory -> string -> class option
val cert_classrel: theory -> class * class -> class * class
@@ -37,8 +37,6 @@
val param_of_inst: theory -> string * string -> string
val inst_of_param: theory -> string -> (string * string) option
val thynames_of_arity: theory -> class * string -> string list
- val introN: string
- val axiomsN: string
end;
structure AxClass: AX_CLASS =
@@ -46,6 +44,18 @@
(** theory data **)
+(* axclass info *)
+
+type info =
+ {def: thm,
+ intro: thm,
+ axioms: thm list,
+ params: (string * typ) list};
+
+fun make_axclass (def, intro, axioms, params): info =
+ {def = def, intro = intro, axioms = axioms, params = params};
+
+
(* class parameters (canonical order) *)
type param = string * class;
@@ -57,188 +67,265 @@
" for " ^ Pretty.string_of_sort pp [c] ^
(if c = c' then "" else " and " ^ Pretty.string_of_sort pp [c'])));
-fun merge_params _ ([], qs) = qs
- | merge_params pp (ps, qs) =
- fold_rev (fn q => if member (op =) ps q then I else add_param pp q) qs ps;
+
+(* setup data *)
+
+datatype data = Data of
+ {axclasses: info Symtab.table,
+ params: param list,
+ proven_classrels: (thm * proof) Symreltab.table,
+ proven_arities: ((class * sort list) * ((thm * string) * proof)) list Symtab.table,
+ (*arity theorems with theory name*)
+ inst_params:
+ (string * thm) Symtab.table Symtab.table *
+ (*constant name ~> type constructor ~> (constant name, equation)*)
+ (string * string) Symtab.table (*constant name ~> (constant name, type constructor)*),
+ diff_merge_classrels: (class * class) list};
+
+fun make_data
+ (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =
+ Data {axclasses = axclasses, params = params, proven_classrels = proven_classrels,
+ proven_arities = proven_arities, inst_params = inst_params,
+ diff_merge_classrels = diff_merge_classrels};
+
+structure Data = Theory_Data_PP
+(
+ type T = data;
+ val empty =
+ make_data (Symtab.empty, [], Symreltab.empty, Symtab.empty, (Symtab.empty, Symtab.empty), []);
+ val extend = I;
+ fun merge pp
+ (Data {axclasses = axclasses1, params = params1, proven_classrels = proven_classrels1,
+ proven_arities = proven_arities1, inst_params = inst_params1,
+ diff_merge_classrels = diff_merge_classrels1},
+ Data {axclasses = axclasses2, params = params2, proven_classrels = proven_classrels2,
+ proven_arities = proven_arities2, inst_params = inst_params2,
+ diff_merge_classrels = diff_merge_classrels2}) =
+ let
+ val axclasses' = Symtab.merge (K true) (axclasses1, axclasses2);
+ val params' =
+ if null params1 then params2
+ else fold_rev (fn q => if member (op =) params1 q then I else add_param pp q) params2 params1;
+
+ (*transitive closure of classrels and arity completion is done in Theory.at_begin hook*)
+ val proven_classrels' = Symreltab.join (K #1) (proven_classrels1, proven_classrels2);
+ val proven_arities' =
+ Symtab.join (K (Library.merge (eq_fst op =))) (proven_arities1, proven_arities2);
+
+ val classrels1 = Symreltab.keys proven_classrels1;
+ val classrels2 = Symreltab.keys proven_classrels2;
+ val diff_merge_classrels' =
+ subtract (op =) classrels1 classrels2 @
+ subtract (op =) classrels2 classrels1 @
+ diff_merge_classrels1 @ diff_merge_classrels2;
+
+ val inst_params' =
+ (Symtab.join (K (Symtab.merge (K true))) (#1 inst_params1, #1 inst_params2),
+ Symtab.merge (K true) (#2 inst_params1, #2 inst_params2));
+ in
+ make_data (axclasses', params', proven_classrels', proven_arities', inst_params',
+ diff_merge_classrels')
+ end;
+);
+
+fun map_data f =
+ Data.map (fn Data {axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels} =>
+ make_data (f (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels)));
+
+fun map_axclasses f =
+ map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
+ (f axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels));
+
+fun map_params f =
+ map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
+ (axclasses, f params, proven_classrels, proven_arities, inst_params, diff_merge_classrels));
+
+fun map_proven_classrels f =
+ map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
+ (axclasses, params, f proven_classrels, proven_arities, inst_params, diff_merge_classrels));
+
+fun map_proven_arities f =
+ map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
+ (axclasses, params, proven_classrels, f proven_arities, inst_params, diff_merge_classrels));
+
+fun map_inst_params f =
+ map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
+ (axclasses, params, proven_classrels, proven_arities, f inst_params, diff_merge_classrels));
+
+val clear_diff_merge_classrels =
+ map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, _) =>
+ (axclasses, params, proven_classrels, proven_arities, inst_params, []));
+
+val rep_data = Data.get #> (fn Data args => args);
+
+val axclasses_of = #axclasses o rep_data;
+val params_of = #params o rep_data;
+val proven_classrels_of = #proven_classrels o rep_data;
+val proven_arities_of = #proven_arities o rep_data;
+val inst_params_of = #inst_params o rep_data;
+val diff_merge_classrels_of = #diff_merge_classrels o rep_data;
-(* axclasses *)
-
-val introN = "intro";
-val superN = "super";
-val axiomsN = "axioms";
+(* maintain axclasses *)
-datatype axclass = AxClass of
- {def: thm,
- intro: thm,
- axioms: thm list,
- params: (string * typ) list};
+fun get_info thy c =
+ (case Symtab.lookup (axclasses_of thy) c of
+ SOME info => info
+ | NONE => error ("No such axclass: " ^ quote c));
-type axclasses = axclass Symtab.table * param list;
-
-fun make_axclass ((def, intro, axioms), params) = AxClass
- {def = def, intro = intro, axioms = axioms, params = params};
-
-fun merge_axclasses pp ((tab1, params1), (tab2, params2)) : axclasses =
- (Symtab.merge (K true) (tab1, tab2), merge_params pp (params1, params2));
+fun class_intros thy =
+ let
+ fun add_intro c = (case try (get_info thy) c of SOME {intro, ...} => cons intro | _ => I);
+ val classes = Sign.all_classes thy;
+ in map (Thm.class_triv thy) classes @ fold add_intro classes [] end;
-(* instances *)
+(* maintain params *)
+
+fun all_params_of thy S =
+ let val params = params_of thy;
+ in fold (fn (x, c) => if Sign.subsort thy (S, [c]) then cons x else I) params [] end;
+
+fun class_of_param thy = AList.lookup (op =) (params_of thy);
+
+
+(* maintain instances *)
val classrel_prefix = "classrel_";
val arity_prefix = "arity_";
-type instances =
- ((class * class) * thm) list * (*classrel theorems*)
- ((class * sort list) * (thm * string)) list Symtab.table; (*arity theorems with theory name*)
-
-fun merge_instances ((classrel1, arities1): instances, (classrel2, arities2)) =
- (merge (eq_fst op =) (classrel1, classrel2),
- Symtab.join (K (merge (eq_fst op =))) (arities1, arities2));
-
-
-(* instance parameters *)
-
-type inst_params =
- (string * thm) Symtab.table Symtab.table
- (*constant name ~> type constructor ~> (constant name, equation)*)
- * (string * string) Symtab.table; (*constant name ~> (constant name, type constructor)*)
-
-fun merge_inst_params ((const_param1, param_const1), (const_param2, param_const2)) =
- (Symtab.join (K (Symtab.merge (K true))) (const_param1, const_param2),
- Symtab.merge (K true) (param_const1, param_const2));
-
-
-(* setup data *)
-
-structure AxClassData = Theory_Data_PP
-(
- type T = axclasses * (instances * inst_params);
- val empty = ((Symtab.empty, []), (([], Symtab.empty), (Symtab.empty, Symtab.empty)));
- val extend = I;
- fun merge pp ((axclasses1, (instances1, inst_params1)), (axclasses2, (instances2, inst_params2))) =
- (merge_axclasses pp (axclasses1, axclasses2),
- (merge_instances (instances1, instances2), merge_inst_params (inst_params1, inst_params2)));
-);
-
-
-(* maintain axclasses *)
-
-val get_axclasses = #1 o AxClassData.get;
-val map_axclasses = AxClassData.map o apfst;
-
-val lookup_def = Symtab.lookup o #1 o get_axclasses;
-
-fun get_info thy c =
- (case lookup_def thy c of
- SOME (AxClass info) => info
- | NONE => error ("No such axclass: " ^ quote c));
-
-fun class_intros thy =
- let
- fun add_intro c =
- (case lookup_def thy c of SOME (AxClass {intro, ...}) => cons intro | _ => I);
- val classes = Sign.all_classes thy;
- in map (Thm.class_triv thy) classes @ fold add_intro classes [] end;
-
-
-fun get_params thy pred =
- let val params = #2 (get_axclasses thy);
- in fold (fn (x, c) => if pred c then cons x else I) params [] end;
-
-fun all_params_of thy S = get_params thy (fn c => Sign.subsort thy (S, [c]));
-
-fun class_of_param thy = AList.lookup (op =) (#2 (get_axclasses thy));
-
-
-(* maintain instances *)
-
fun instance_name (a, c) = Long_Name.base_name c ^ "_" ^ Long_Name.base_name a;
-val get_instances = #1 o #2 o AxClassData.get;
-val map_instances = AxClassData.map o apsnd o apfst;
-
fun the_classrel thy (c1, c2) =
- (case AList.lookup (op =) (#1 (get_instances thy)) (c1, c2) of
- SOME th => Thm.transfer thy th
+ (case Symreltab.lookup (proven_classrels_of thy) (c1, c2) of
+ SOME classrel => classrel
| NONE => error ("Unproven class relation " ^
Syntax.string_of_classrel (ProofContext.init thy) [c1, c2]));
-fun put_classrel arg = map_instances (fn (classrel, arities) =>
- (insert (eq_fst op =) arg classrel, arities));
+fun the_classrel_thm thy = Thm.transfer thy o #1 o the_classrel thy;
+fun the_classrel_prf thy = #2 o the_classrel thy;
+
+fun put_trancl_classrel ((c1, c2), th) thy =
+ let
+ val cert = Thm.cterm_of thy;
+ val certT = Thm.ctyp_of thy;
+
+ val classes = Sorts.classes_of (Sign.classes_of thy);
+ val classrels = proven_classrels_of thy;
+
+ fun reflcl_classrel (c1', c2') =
+ if c1' = c2'
+ then Thm.trivial (cert (Logic.mk_of_class (TVar ((Name.aT, 0), []), c1')))
+ else the_classrel_thm thy (c1', c2');
+ fun gen_classrel (c1_pred, c2_succ) =
+ let
+ val th' = ((reflcl_classrel (c1_pred, c1) RS th) RS reflcl_classrel (c2, c2_succ))
+ |> Drule.instantiate' [SOME (certT (TVar ((Name.aT, 0), [])))] []
+ |> Thm.close_derivation;
+ val prf' = Thm.proof_of th';
+ in ((c1_pred, c2_succ), (th', prf')) end;
+
+ val new_classrels =
+ Library.map_product pair (c1 :: Graph.imm_preds classes c1) (c2 :: Graph.imm_succs classes c2)
+ |> filter_out (Symreltab.defined classrels)
+ |> map gen_classrel;
+ val needed = not (null new_classrels);
+ in
+ (needed,
+ if needed then map_proven_classrels (fold Symreltab.update new_classrels) thy
+ else thy)
+ end;
+
+fun complete_classrels thy =
+ let
+ val classrels = proven_classrels_of thy;
+ val diff_merge_classrels = diff_merge_classrels_of thy;
+ val (needed, thy') = (false, thy) |>
+ fold (fn c12 => fn (needed, thy) =>
+ put_trancl_classrel (c12, Symreltab.lookup classrels c12 |> the |> #1) thy
+ |>> (fn b => needed orelse b))
+ diff_merge_classrels;
+ in
+ if null diff_merge_classrels then NONE
+ else SOME (clear_diff_merge_classrels thy')
+ end;
fun the_arity thy a (c, Ss) =
- (case AList.lookup (op =) (Symtab.lookup_list (#2 (get_instances thy)) a) (c, Ss) of
- SOME (th, _) => Thm.transfer thy th
+ (case AList.lookup (op =) (Symtab.lookup_list (proven_arities_of thy) a) (c, Ss) of
+ SOME arity => arity
| NONE => error ("Unproven type arity " ^
Syntax.string_of_arity (ProofContext.init thy) (a, Ss, [c])));
+fun the_arity_thm thy a c_Ss = the_arity thy a c_Ss |> #1 |> #1 |> Thm.transfer thy;
+fun the_arity_prf thy a c_Ss = the_arity thy a c_Ss |> #2;
+
fun thynames_of_arity thy (c, a) =
- Symtab.lookup_list (#2 (get_instances thy)) a
- |> map_filter (fn ((c', _), (_, name)) => if c = c' then SOME name else NONE)
+ Symtab.lookup_list (proven_arities_of thy) a
+ |> map_filter (fn ((c', _), ((_, name),_)) => if c = c' then SOME name else NONE)
|> rev;
-fun insert_arity_completions thy (t, ((c, Ss), (th, thy_name))) arities =
+fun insert_arity_completions thy (t, ((c, Ss), ((th, thy_name), _))) arities =
let
val algebra = Sign.classes_of thy;
val super_class_completions =
Sign.super_classes thy c
|> filter_out (fn c1 => exists (fn ((c2, Ss2), _) => c1 = c2
andalso Sorts.sorts_le algebra (Ss2, Ss)) (Symtab.lookup_list arities t));
- val completions = map (fn c1 => (Sorts.classrel_derivation algebra
- (fn (th, c2) => fn c3 => th RS the_classrel thy (c2, c3)) (th, c) c1
- |> Thm.close_derivation, c1)) super_class_completions;
- val arities' = fold (fn (th1, c1) => Symtab.cons_list (t, ((c1, Ss), (th1, thy_name))))
+ val names_and_Ss = Name.names Name.context Name.aT (map (K []) Ss);
+ val completions = super_class_completions |> map (fn c1 =>
+ let
+ val th1 = (th RS the_classrel_thm thy (c, c1))
+ |> Drule.instantiate' (map (SOME o ctyp_of thy o TVar o apfst (rpair 0)) names_and_Ss) []
+ |> Thm.close_derivation;
+ val prf1 = Thm.proof_of th1;
+ in (((th1, thy_name), prf1), c1) end);
+ val arities' = fold (fn (th_thy_prf1, c1) => Symtab.cons_list (t, ((c1, Ss), th_thy_prf1)))
completions arities;
in (null completions, arities') end;
fun put_arity ((t, Ss, c), th) thy =
let
- val arity' = (t, ((c, Ss), (th, Context.theory_name thy)));
+ val arity' = (t, ((c, Ss), ((th, Context.theory_name thy), Thm.proof_of th)));
in
thy
- |> map_instances (fn (classrel, arities) => (classrel,
- arities
- |> Symtab.insert_list (eq_fst op =) arity'
- |> insert_arity_completions thy arity'
- |> snd))
+ |> map_proven_arities
+ (Symtab.insert_list (eq_fst op =) arity' #>
+ insert_arity_completions thy arity' #> snd)
end;
fun complete_arities thy =
let
- val arities = snd (get_instances thy);
+ val arities = proven_arities_of thy;
val (finished, arities') = arities
|> fold_map (insert_arity_completions thy) (Symtab.dest_list arities);
in
- if forall I finished then NONE
- else SOME (thy |> map_instances (fn (classrel, _) => (classrel, arities')))
+ if forall I finished
+ then NONE
+ else SOME (map_proven_arities (K arities') thy)
end;
-val _ = Context.>> (Context.map_theory (Theory.at_begin complete_arities));
+val _ = Context.>> (Context.map_theory
+ (Theory.at_begin complete_classrels #> Theory.at_begin complete_arities));
(* maintain instance parameters *)
-val get_inst_params = #2 o #2 o AxClassData.get;
-val map_inst_params = AxClassData.map o apsnd o apsnd;
+fun get_inst_param thy (c, tyco) =
+ (case Symtab.lookup (the_default Symtab.empty (Symtab.lookup (#1 (inst_params_of thy)) c)) tyco of
+ SOME c' => c'
+ | NONE => error ("No instance parameter for constant " ^ quote c ^ " on type " ^ quote tyco));
-fun get_inst_param thy (c, tyco) =
- case Symtab.lookup ((the_default Symtab.empty o Symtab.lookup (fst (get_inst_params thy))) c) tyco
- of SOME c' => c'
- | NONE => error ("No instance parameter for constant " ^ quote c
- ^ " on type constructor " ^ quote tyco);
-
-fun add_inst_param (c, tyco) inst = (map_inst_params o apfst
- o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
+fun add_inst_param (c, tyco) inst =
+ (map_inst_params o apfst o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
#> (map_inst_params o apsnd) (Symtab.update_new (fst inst, (c, tyco)));
-val inst_of_param = Symtab.lookup o snd o get_inst_params;
+val inst_of_param = Symtab.lookup o #2 o inst_params_of;
val param_of_inst = fst oo get_inst_param;
-fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst)
- (get_inst_params thy) [];
+fun inst_thms thy =
+ Symtab.fold (Symtab.fold (cons o #2 o #2) o #2) (#1 (inst_params_of thy)) [];
fun get_inst_tyco consts = try (fst o dest_Type o the_single o Consts.typargs consts);
@@ -248,18 +335,20 @@
fun unoverload_conv thy = MetaSimplifier.rewrite true (inst_thms thy);
fun overload_conv thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy));
-fun lookup_inst_param consts params (c, T) = case get_inst_tyco consts (c, T)
- of SOME tyco => AList.lookup (op =) params (c, tyco)
- | NONE => NONE;
+fun lookup_inst_param consts params (c, T) =
+ (case get_inst_tyco consts (c, T) of
+ SOME tyco => AList.lookup (op =) params (c, tyco)
+ | NONE => NONE);
fun unoverload_const thy (c_ty as (c, _)) =
- if is_some (class_of_param thy c)
- then case get_inst_tyco (Sign.consts_of thy) c_ty
- of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
- | NONE => c
+ if is_some (class_of_param thy c) then
+ (case get_inst_tyco (Sign.consts_of thy) c_ty of
+ SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
+ | NONE => c)
else c;
+
(** instances **)
(* class relations *)
@@ -331,6 +420,8 @@
(* primitive rules *)
+val shyps_topped = forall null o #shyps o Thm.rep_thm;
+
fun add_classrel raw_th thy =
let
val th = Thm.strip_shyps (Thm.transfer thy raw_th);
@@ -338,10 +429,14 @@
fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
val rel = Logic.dest_classrel prop handle TERM _ => err ();
val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
+ val th' = th
+ |> Drule.instantiate' [SOME (ctyp_of thy (TVar ((Name.aT, 0), [c1])))] []
+ |> Thm.unconstrain_allTs;
+ val _ = shyps_topped th' orelse raise Fail "add_classrel: nontop shyps after unconstrain";
in
thy
|> Sign.primitive_classrel (c1, c2)
- |> put_classrel ((c1, c2), Thm.close_derivation (Drule.unconstrainTs th))
+ |> (snd oo put_trancl_classrel) ((c1, c2), th')
|> perhaps complete_arities
end;
@@ -351,17 +446,22 @@
val prop = Thm.plain_prop_of th;
fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
- val T = Type (t, map TFree (Name.names Name.context Name.aT Ss));
+ val names = Name.names Name.context Name.aT Ss;
+ val T = Type (t, map TFree names);
val missing_params = Sign.complete_sort thy [c]
|> maps (these o Option.map #params o try (get_info thy))
|> filter_out (fn (const, _) => can (get_inst_param thy) (const, t))
|> (map o apsnd o map_atyps) (K T);
val _ = map (Sign.certify_sort thy) Ss = Ss orelse err ();
+ val th' = th
+ |> Drule.instantiate' (map (SOME o ctyp_of thy o TVar o apfst (rpair 0)) names) []
+ |> Thm.unconstrain_allTs;
+ val _ = shyps_topped th' orelse raise Fail "add_arity: nontop shyps after unconstrain";
in
thy
|> fold (snd oo declare_overloaded) missing_params
|> Sign.primitive_arity (t, Ss, [c])
- |> put_arity ((t, Ss, c), Thm.close_derivation (Drule.unconstrainTs th))
+ |> put_arity ((t, Ss, c), th')
end;
@@ -483,25 +583,24 @@
def_thy
|> Sign.qualified_path true bconst
|> PureThy.note_thmss ""
- [((Binding.name introN, []), [([Drule.export_without_context raw_intro], [])]),
- ((Binding.name superN, []), [(map Drule.export_without_context raw_classrel, [])]),
- ((Binding.name axiomsN, []),
+ [((Binding.name "intro", []), [([Drule.export_without_context raw_intro], [])]),
+ ((Binding.name "super", []), [(map Drule.export_without_context raw_classrel, [])]),
+ ((Binding.name "axioms", []),
[(map (fn th => Drule.export_without_context (class_triv RS th)) raw_axioms, [])])]
||> Sign.restore_naming def_thy;
(* result *)
- val axclass = make_axclass ((def, intro, axioms), params);
+ val axclass = make_axclass (def, intro, axioms, params);
val result_thy =
facts_thy
- |> fold put_classrel (map (pair class) super ~~ classrel)
+ |> fold (snd oo put_trancl_classrel) (map (pair class) super ~~ classrel)
|> Sign.qualified_path false bconst
|> PureThy.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> snd
|> Sign.restore_naming facts_thy
- |> map_axclasses (fn (axclasses, parameters) =>
- (Symtab.update (class, axclass) axclasses,
- fold (fn (x, _) => add_param pp (x, class)) params parameters));
+ |> map_axclasses (Symtab.update (class, axclass))
+ |> map_params (fold (fn (x, _) => add_param pp (x, class)) params);
in (class, result_thy) end;
--- a/src/Pure/display.ML Sun Apr 25 08:25:34 2010 +0200
+++ b/src/Pure/display.ML Mon Apr 26 07:47:18 2010 +0200
@@ -182,7 +182,8 @@
val extern_const = Name_Space.extern (#1 constants);
val {classes, default, types, ...} = Type.rep_tsig tsig;
val (class_space, class_algebra) = classes;
- val {classes, arities} = Sorts.rep_algebra class_algebra;
+ val classes = Sorts.classes_of class_algebra;
+ val arities = Sorts.arities_of class_algebra;
val clsses = Name_Space.dest_table (class_space, Symtab.make (Graph.dest classes));
val tdecls = Name_Space.dest_table types;
--- a/src/Pure/drule.ML Sun Apr 25 08:25:34 2010 +0200
+++ b/src/Pure/drule.ML Mon Apr 26 07:47:18 2010 +0200
@@ -106,7 +106,6 @@
val dummy_thm: thm
val sort_constraintI: thm
val sort_constraint_eq: thm
- val unconstrainTs: thm -> thm
val with_subgoal: int -> (thm -> thm) -> thm -> thm
val comp_no_flatten: thm * int -> int -> thm -> thm
val rename_bvars: (string * string) list -> thm -> thm
@@ -204,12 +203,6 @@
(** Standardization of rules **)
-(* type classes and sorts *)
-
-fun unconstrainTs th =
- fold (Thm.unconstrainT o Thm.ctyp_of (Thm.theory_of_thm th) o TVar)
- (Thm.fold_terms Term.add_tvars th []) th;
-
(*Generalization over a list of variables*)
val forall_intr_list = fold_rev forall_intr;
--- a/src/Pure/sorts.ML Sun Apr 25 08:25:34 2010 +0200
+++ b/src/Pure/sorts.ML Mon Apr 26 07:47:18 2010 +0200
@@ -25,9 +25,8 @@
val insert_term: term -> sort OrdList.T -> sort OrdList.T
val insert_terms: term list -> sort OrdList.T -> sort OrdList.T
type algebra
- val rep_algebra: algebra ->
- {classes: serial Graph.T,
- arities: (class * (class * sort list)) list Symtab.table}
+ val classes_of: algebra -> serial Graph.T
+ val arities_of: algebra -> (class * (class * sort list)) list Symtab.table
val all_classes: algebra -> class list
val super_classes: algebra -> class -> class list
val class_less: algebra -> class * class -> bool
@@ -116,10 +115,8 @@
{classes: serial Graph.T,
arities: (class * (class * sort list)) list Symtab.table};
-fun rep_algebra (Algebra args) = args;
-
-val classes_of = #classes o rep_algebra;
-val arities_of = #arities o rep_algebra;
+fun classes_of (Algebra {classes, ...}) = classes;
+fun arities_of (Algebra {arities, ...}) = arities;
fun make_algebra (classes, arities) =
Algebra {classes = classes, arities = arities};
--- a/src/Pure/thm.ML Sun Apr 25 08:25:34 2010 +0200
+++ b/src/Pure/thm.ML Mon Apr 26 07:47:18 2010 +0200
@@ -92,8 +92,6 @@
val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
val instantiate_cterm: (ctyp * ctyp) list * (cterm * cterm) list -> cterm -> cterm
val trivial: cterm -> thm
- val of_class: ctyp * class -> thm
- val unconstrainT: ctyp -> thm -> thm
val dest_state: thm * int -> (term * term) list * term list * term * term
val lift_rule: cterm -> thm -> thm
val incr_indexes: int -> thm -> thm
@@ -139,6 +137,9 @@
val adjust_maxidx_thm: int -> thm -> thm
val varifyT_global: thm -> thm
val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
+ val of_class: ctyp * class -> thm
+ val unconstrainT: ctyp -> thm -> thm
+ val unconstrain_allTs: thm -> thm
val freezeT: thm -> thm
val assumption: int -> thm -> thm Seq.seq
val eq_assumption: int -> thm -> thm
@@ -1240,6 +1241,11 @@
prop = Logic.list_implies (constraints, unconstrain prop)})
end;
+fun unconstrain_allTs th =
+ fold (unconstrainT o ctyp_of (theory_of_thm th) o TVar)
+ (fold_terms Term.add_tvars th []) th;
+
+
(* Replace all TFrees not fixed or in the hyps by new TVars *)
fun varifyT_global' fixed (Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
let