# HG changeset patch # User haftmann # Date 1272260838 -7200 # Node ID c25aa1c50ce99f56b34dcbd2fe147cbe76ab220e # Parent c827275e530ec49efceda313240e4318a91b1c29# Parent 30bcceed0dc244e1cea657fe8b14ed713afbf1d1 merged diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/HOL/Boogie/Tools/boogie_commands.ML --- 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 diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/HOL/HOL.thy --- 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" diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy --- 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) \ 1" "abs(x$2) \ 1" using assms unfolding infnorm_eq_1_2 by auto -lemma fashoda_unit: fixes f g::"real^1 \ real^2" +lemma fashoda_unit: fixes f g::"real \ real^2" assumes "f ` {- 1..1} \ {- 1..1}" "g ` {- 1..1} \ {- 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:"\z. z\0 \ 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 = "(\w::real^2. (f \ vec1 \ (\x. x$1)) w - (g \ vec1 \ (\x. x$2)) w)" - have *:"\i. vec1 ` (\x::real^2. x $ i) ` {- 1..1} = {- 1..1::real^1}" + let ?F = "(\w::real^2. (f \ (\x. x$1)) w - (g \ (\x. x$2)) w)" + have *:"\i. (\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 \ (\w. (f \ vec1 \ (\x. x $ 1)) w - (g \ vec1 \ (\x. x $ 2)) w) ` {- 1..1::real^2}" + apply(rule_tac x="vec x" in exI) by auto + { fix x assume "x \ (\w. (f \ (\x. x $ 1)) w - (g \ (\x. x $ 2)) w) ` {- 1..1::real^2}" then guess w unfolding image_iff .. note w = this - hence "x \ 0" using as[of "vec1 (w$1)" "vec1 (w$2)"] unfolding mem_interval by auto} note x0=this + hence "x \ 0" using as[of "w$1" "w$2"] unfolding mem_interval by auto} note x0=this have 21:"\i::2. i\1 \ i=2" using UNIV_2 by auto have 1:"{- 1<..<1::real^2} \ {}" unfolding interval_eq_empty by auto have 2:"continuous_on {- 1..1} (negatex \ sqprojection \ ?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) \ {- 1..1::real^1}" "vec1 (x $ 2) \ {- 1..1::real^1}" using x(1) unfolding mem_interval by auto - hence nz:"f (vec1 (x $ 1)) - g (vec1 (x $ 2)) \ 0" unfolding right_minus_eq apply-apply(rule as) by auto + have x1:"x $ 1 \ {- 1..1::real}" "x $ 2 \ {- 1..1::real}" using x(1) unfolding mem_interval by auto + hence nz:"f (x $ 1) - g (x $ 2) \ 0" unfolding right_minus_eq apply-apply(rule as) by auto have "x $ 1 = -1 \ x $ 1 = 1 \ x $ 2 = -1 \ x $ 2 = 1" using nx unfolding infnorm_eq_1_2 by auto thus False proof- fix P Q R S presume "P \ Q \ R \ S" "P\False" "Q\False" "R\False" "S\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)) \ {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto + from x1 have "g (x $ 2) \ {- 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)) \ {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto + from x1 have "g (x $ 2) \ {- 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)) \ {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto + from x1 have "f (x $ 1) \ {- 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)) \ {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto + from x1 have "f (x $ 1) \ {- 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 \ real^2" and g ::"real^1 \ real^2" +lemma fashoda_unit_path: fixes f ::"real \ real^2" and g ::"real \ real^2" assumes "path f" "path g" "path_image f \ {- 1..1}" "path_image g \ {- 1..1}" "(pathstart f)$1 = -1" "(pathfinish f)$1 = 1" "(pathstart g)$2 = -1" "(pathfinish g)$2 = 1" obtains z where "z \ path_image f" "z \ path_image g" proof- note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def] - def iscale \ "\z::real^1. inverse 2 *\<^sub>R (z + 1)" + def iscale \ "\z::real. inverse 2 *\<^sub>R (z + 1)" have isc:"iscale ` {- 1..1} \ {0..1}" unfolding iscale_def by(auto) have "\s\{- 1..1}. \t\{- 1..1}. (f \ iscale) s = (g \ iscale) t" proof(rule fashoda_unit) show "(f \ iscale) ` {- 1..1} \ {- 1..1}" "(g \ iscale) ` {- 1..1} \ {- 1..1}" diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- 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 {.. inner 1 x}" by auto + thus 1: "convex {a..}" by (simp only: convex_halfspace_ge) + have "{..b} = {x. inner 1 x \ 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}" by auto + thus "convex {a..b}" by (simp only: convex_Int 1 2) + have "{a<..b} = {a<..} \ {..b}" by auto + thus "convex {a<..b}" by (simp only: convex_Int 3 2) + have "{a.. {.. {..i. convex {x. P i x}" + shows "convex {x. \i. P i (x$i)}" +using assms unfolding convex_def by auto + lemma convex_positive_orthant: "convex {x::real^'n. (\i. 0 \ 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 \ real ^ 'n \ (real ^ 'n) set" where + open_segment :: "'a::real_vector \ 'a \ 'a set" where "open_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 < u \ u < 1}" definition - closed_segment :: "real ^ 'n \ real ^ 'n \ (real ^ 'n) set" where + closed_segment :: "'a::real_vector \ 'a \ 'a set" where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \ u \ u \ 1}" definition "between = (\ (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 \ closed_segment a b" shows "norm(y - x) \ norm(y - a) \ norm(y - x) \ norm(y - b)" proof- obtain z where "z\{a, b}" "norm (x - y) \ 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 \ closed_segment a b" shows "norm(x - a) \ norm(b - a)" "norm(x - b) \ norm(b - a)" using segment_furthest_le[OF assms, of a] @@ -2842,23 +2873,42 @@ subsection {* Paths. *} -definition "path (g::real^1 \ real^'n) \ continuous_on {0 .. 1} g" - -definition "pathstart (g::real^1 \ real^'n) = g 0" - -definition "pathfinish (g::real^1 \ real^'n) = g 1" - -definition "path_image (g::real^1 \ real^'n) = g ` {0 .. 1}" - -definition "reversepath (g::real^1 \ real^'n) = (\x. g(1 - x))" - -definition joinpaths:: "(real^1 \ real^'n) \ (real^1 \ real^'n) \ (real^1 \ real^'n)" (infixr "+++" 75) - where "joinpaths g1 g2 = (\x. if dest_vec1 x \ ((1 / 2)::real) then g1 (2 *\<^sub>R x) else g2(2 *\<^sub>R x - 1))" -definition "simple_path (g::real^1 \ real^'n) \ +text {* TODO: Once @{const continuous_on} is generalized to arbitrary +topological spaces, all of these concepts should be similarly generalized. *} + +definition + path :: "(real \ 'a::metric_space) \ bool" + where "path g \ continuous_on {0 .. 1} g" + +definition + pathstart :: "(real \ 'a::metric_space) \ 'a" + where "pathstart g = g 0" + +definition + pathfinish :: "(real \ 'a::metric_space) \ 'a" + where "pathfinish g = g 1" + +definition + path_image :: "(real \ 'a::metric_space) \ 'a set" + where "path_image g = g ` {0 .. 1}" + +definition + reversepath :: "(real \ 'a::metric_space) \ (real \ 'a)" + where "reversepath g = (\x. g(1 - x))" + +definition + joinpaths :: "(real \ 'a::metric_space) \ (real \ 'a) \ (real \ 'a)" + (infixr "+++" 75) + where "g1 +++ g2 = (\x. if x \ 1/2 then g1 (2 * x) else g2 (2 * x - 1))" + +definition + simple_path :: "(real \ 'a::metric_space) \ bool" + where "simple_path g \ (\x\{0..1}. \y\{0..1}. g x = g y \ x = y \ x = 0 \ y = 1 \ x = 1 \ y = 0)" -definition "injective_path (g::real^1 \ real^'n) \ - (\x\{0..1}. \y\{0..1}. g x = g y \ x = y)" +definition + injective_path :: "(real \ 'a::metric_space) \ bool" + where "injective_path g \ (\x\{0..1}. \y\{0..1}. g x = g y \ 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) \ 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) \ 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 \ 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 \ 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 *:"\g. path_image(reversepath g) \ 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) \ path g" proof- @@ -2913,7 +2960,7 @@ apply(rule continuous_on_compose[unfolded o_def, of _ "\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 = (\x. g1 (2 *\<^sub>R x)) \ (\x. (1/2) *\<^sub>R x)" - "g2 = (\x. g2 (2 *\<^sub>R x - 1)) \ (\x. (1/2) *\<^sub>R (x + 1))" unfolding o_def by auto - have "op *\<^sub>R (1 / 2) ` {0::real^1..1} \ {0..1}" "(\x. (1 / 2) *\<^sub>R (x + 1)) ` {(0::real^1)..1} \ {0..1}" - unfolding image_smult_interval by auto + "g2 = (\x. g2 (2 *\<^sub>R x - 1)) \ (\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} \ {0..1}" "(\x. (1 / 2) *\<^sub>R (x + 1)) ` {(0::real)..1} \ {0..1}" + by auto thus "continuous_on {0..1} g1 \ 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 \ op *\<^sub>R (1 / 2) ` {0::real^1..1}" - hence "dest_vec1 x \ 1 / 2" unfolding image_iff by(auto simp add: vector_component_simps) + fix x assume "x \ op *\<^sub>R (1 / 2) ` {0::real..1}" + hence "x \ 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 \ (\x. (1 / 2) *\<^sub>R (x + 1)) ` {0::real^1..1}" - hence "dest_vec1 x \ 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 \ (\x. (1 / 2) *\<^sub>R (x + 1)) ` {0::real..1}" + hence "x \ 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} \ {(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 ***:"(\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 ****:"\x::real^1. x $ 1 * 2 = 1 \ 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} \ {(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 ***:"(\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 _ "\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 \ (\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) \ (path_image g1 \ path_image g2)" proof fix x assume "x \ path_image (g1 +++ g2)" - then obtain y where y:"y\{0..1}" "x = (if dest_vec1 y \ 1 / 2 then g1 (2 *\<^sub>R y) else g2 (2 *\<^sub>R y - 1))" + then obtain y where y:"y\{0..1}" "x = (if y \ 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 \ path_image g1 \ path_image g2" apply(cases "dest_vec1 y \ 1/2") + thus "x \ path_image g1 \ path_image g2" apply(cases "y \ 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 \ s" "path_image g2 \ s" shows "path_image(g1 +++ g2) \ s" @@ -2975,13 +3024,12 @@ fix x assume "x \ path_image g1" then obtain y where y:"y\{0..1}" "x = g1 y" unfolding path_image_def image_iff by auto thus "x \ 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 \ path_image g2" then obtain y where y:"y\{0..1}" "x = g2 y" unfolding path_image_def image_iff by auto - moreover have *:"y $ 1 = 0 \ y = 0" unfolding Cart_eq by auto - ultimately show "x \ path_image (g1 +++ g2)" unfolding joinpaths_def path_image_def image_iff + then show "x \ 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 \ path_image g1" "x \ path_image g2" shows "x \ 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 \ {0..1}" "y \ {0..1}" "?g x = ?g y" - show "x = y \ x = 0 \ y = 1 \ x = 1 \ y = 0" proof(case_tac "x$1 \ 1/2",case_tac[!] "y$1 \ 1/2", unfold not_le) - assume as:"x $ 1 \ 1 / 2" "y $ 1 \ 1 / 2" + fix x y::"real" assume xy:"x \ {0..1}" "y \ {0..1}" "?g x = ?g y" + show "x = y \ x = 0 \ y = 1 \ x = 1 \ y = 0" proof(case_tac "x \ 1/2",case_tac[!] "y \ 1/2", unfold not_le) + assume as:"x \ 1 / 2" "y \ 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 \ {0..1}" "2 *\<^sub>R y \ {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 \ {0..1}" "2 *\<^sub>R y - 1 \ {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 \ {0..1}" "2 *\<^sub>R y - 1 \ {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 \ 1 / 2" "y $ 1 > 1 / 2" + next assume as:"x \ 1 / 2" "y > 1 / 2" hence "?g x \ path_image g1" "?g y \ 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 \ 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 \ 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 \ 1 / 2" hence "?g x \ path_image g2" "?g y \ 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 \ 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 *:"\x y::real^1. 2 *\<^sub>R x = 1 \ 2 *\<^sub>R y = 1 \ x = y" unfolding Cart_eq forall_1 by(auto simp del:dest_vec1_eq) fix x y assume xy:"x \ {0..1}" "y \ {0..1}" "(g1 +++ g2) x = (g1 +++ g2) y" - show "x = y" proof(cases "x$1 \ 1/2", case_tac[!] "y$1 \ 1/2", unfold not_le) - assume "x $ 1 \ 1 / 2" "y $ 1 \ 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 \ 1 / 2" "y $ 1 > 1 / 2" + show "x = y" proof(cases "x \ 1/2", case_tac[!] "y \ 1/2", unfold not_le) + assume "x \ 1 / 2" "y \ 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 \ 1 / 2" "y > 1 / 2" hence "?g x \ path_image g1" "?g y \ 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 \ 1 / 2" + by auto + next assume as:"x > 1 / 2" "y \ 1 / 2" hence "?g x \ path_image g2" "?g y \ 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 \ real^'n) = - (\x. if dest_vec1 (a + x) \ 1 then f(a + x) else f(a + x - 1))" +definition "shiftpath a (f::real \ 'a::metric_space) = + (\x. if (a + x) \ 1 then f(a + x) else f(a + x - 1))" lemma pathstart_shiftpath: "a \ 1 \ 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 \ 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 \ {0 .. 1}" @@ -3098,39 +3142,38 @@ lemma path_shiftpath: assumes "path g" "pathfinish g = pathstart g" "a \ {0..1}" shows "path(shiftpath a g)" proof- - have *:"{0 .. 1} = {0 .. 1-a} \ {1-a .. 1}" using assms(3) by(auto simp add: vector_component_simps) + have *:"{0 .. 1} = {0 .. 1-a} \ {1-a .. 1}" using assms(3) by auto have **:"\x. x + a = 1 \ 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 \ (\x. a + x)"]) prefer 3 + apply(rule closed_real_atLeastAtMost)+ apply(rule continuous_on_eq[of _ "g \ (\x. a + x)"]) prefer 3 apply(rule continuous_on_eq[of _ "g \ (\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 \ {0..1}" "x \ {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 \ {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 \ {0..1::real^1}" " \y\{0..1} \ {x. \ a $ 1 + x $ 1 \ 1}. g x \ g (a + y - 1)" - hence "\y\{0..1} \ {x. a $ 1 + x $ 1 \ 1}. g x = g (a + y)" proof(cases "a \ x") + { fix x assume as:"g 1 = g 0" "x \ {0..1::real}" " \y\{0..1} \ {x. \ a + x \ 1}. g x \ g (a + y - 1)" + hence "\y\{0..1} \ {x. a + x \ 1}. g x = g (a + y)" proof(cases "a \ 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 \ real ^ 'n \ real ^ 1 \ real ^ 'n" where - "linepath a b = (\x. (1 - dest_vec1 x) *\<^sub>R a + dest_vec1 x *\<^sub>R b)" + linepath :: "'a::real_normed_vector \ 'a \ real \ 'a" where + "linepath a b = (\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 \ b" shows "injective_path(linepath a b)" proof- - { obtain i where i:"a$i \ 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 \ 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 \ b \ 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 \ path_image g" +lemma not_on_path_ball: + fixes g :: "real \ 'a::heine_borel" + assumes "path g" "z \ path_image g" shows "\e>0. ball z e \ (path_image g) = {}" proof- obtain a where "a\path_image g" "\y\path_image g. dist z a \ 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 \ path_image g" +lemma not_on_path_cball: + fixes g :: "real \ 'a::heine_borel" + assumes "path g" "z \ path_image g" shows "\e>0. cball z e \ (path_image g) = {}" proof- obtain e where "ball z e \ path_image g = {}" "e>0" using not_on_path_ball[OF assms] by auto moreover have "cball z (e/2) \ ball z e" using `e>0` by auto @@ -3191,14 +3240,14 @@ lemma path_component_refl: assumes "x \ s" shows "path_component s x x" unfolding path_defs apply(rule_tac x="\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 \ x \ 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 \ 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\e1\s" "x2\e2\s" by auto then obtain g where g:"path g" "path_image g \ 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} \ {x \ {0..1}. g x \ e1} \ {x \ {0..1}. g x \ e2}" using as(3) g(2)[unfolded path_defs] by blast moreover have "{x \ {0..1}. g x \ e1} \ {x \ {0..1}. g x \ e2} = {}" using as(4) g(2)[unfolded path_defs] unfolding subset_eq by auto - moreover have "{x \ {0..1}. g x \ e1} \ {} \ {x \ {0..1}. g x \ e2} \ {}" using g(3,4)[unfolded path_defs] using obt by(auto intro!: exI) + moreover have "{x \ {0..1}. g x \ e1} \ {} \ {x \ {0..1}. g x \ e2} \ {}" 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\{0..1}. g x \ e1}" "{x\{0..1}. g x \ 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 \ path_component s x" hence "y\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\s - path_component s x" then obtain e where e:"e>0" "ball y e \ s" using assms[unfolded open_contains_ball] by auto show "\e>0. ball y e \ 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 \ s" "y \ s" show "y \ path_component s x" proof(rule ccontr) assume "y \ 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="\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 \ t \ {}" shows "path_connected (s \ t)" unfolding path_connected_component proof(rule,rule) diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/HOL/Nominal/nominal_inductive.ML --- 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; diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/HOL/Nominal/nominal_inductive2.ML --- 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; diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/HOL/Nominal/nominal_primrec.ML --- 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); diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/HOL/Tools/Datatype/datatype_data.ML --- 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; diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/HOL/Tools/Function/function.ML --- 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 diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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); diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/HOL/Tools/Quotient/quotient_typ.ML --- 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 diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/HOL/Tools/choice_specification.ML --- 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; diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/HOL/Tools/typedef.ML --- 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 diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/HOLCF/Tools/pcpodef.ML --- 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 diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/Pure/Isar/calculation.ML --- 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 *) diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/Pure/Isar/class_target.ML --- 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; diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/Pure/Isar/element.ML --- 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 => diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/Pure/Isar/isar_cmd.ML --- 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 diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/Pure/Isar/isar_syn.ML --- 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.$$$ "\\" || 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" diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/Pure/Isar/obtain.ML --- 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; diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/Pure/Isar/proof.ML --- 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; diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/Pure/Isar/specification.ML --- 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") diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/Pure/ML/ml_thms.ML --- 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); diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/Pure/Thy/thy_output.ML --- 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); diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/Pure/axclass.ML --- 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; diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/Pure/display.ML --- 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; diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/Pure/drule.ML --- 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; diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/Pure/sorts.ML --- 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}; diff -r 30bcceed0dc2 -r c25aa1c50ce9 src/Pure/thm.ML --- 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