--- a/Admin/update-keywords Wed Aug 17 07:13:13 2011 +0200
+++ b/Admin/update-keywords Wed Aug 17 18:51:27 2011 +0200
@@ -12,7 +12,8 @@
isabelle keywords \
"$LOG/Pure.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" "$LOG/HOL-Boogie.gz" \
- "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz" "$LOG/HOL-SPARK.gz"
+ "$LOG/HOL-Library.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz" \
+ "$LOG/HOL-SPARK.gz"
isabelle keywords -k ZF \
"$LOG/Pure.gz" "$LOG/FOL.gz" "$LOG/ZF.gz"
--- a/etc/isar-keywords-ZF.el Wed Aug 17 07:13:13 2011 +0200
+++ b/etc/isar-keywords-ZF.el Wed Aug 17 18:51:27 2011 +0200
@@ -40,12 +40,9 @@
"classrel"
"codatatype"
"code_datatype"
- "code_library"
- "code_module"
"coinductive"
"commit"
"consts"
- "consts_code"
"context"
"corollary"
"datatype"
@@ -194,7 +191,6 @@
"typed_print_translation"
"typedecl"
"types"
- "types_code"
"ultimately"
"undo"
"undos_proof"
@@ -219,11 +215,9 @@
"case_eqns"
"con_defs"
"constrains"
- "contains"
"defines"
"domains"
"elimination"
- "file"
"fixes"
"for"
"identifier"
@@ -354,11 +348,8 @@
"classrel"
"codatatype"
"code_datatype"
- "code_library"
- "code_module"
"coinductive"
"consts"
- "consts_code"
"context"
"datatype"
"declaration"
@@ -410,7 +401,6 @@
"typed_print_translation"
"typedecl"
"types"
- "types_code"
"use"))
(defconst isar-keywords-theory-script
--- a/etc/isar-keywords.el Wed Aug 17 07:13:13 2011 +0200
+++ b/etc/isar-keywords.el Wed Aug 17 18:51:27 2011 +0200
@@ -1,6 +1,6 @@
;;
;; Keyword classification tables for Isabelle/Isar.
-;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Nominal + HOL-Statespace + HOL-SPARK.
+;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Library + HOL-Nominal + HOL-Statespace + HOL-SPARK.
;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
;;
--- a/src/HOL/Deriv.thy Wed Aug 17 07:13:13 2011 +0200
+++ b/src/HOL/Deriv.thy Wed Aug 17 18:51:27 2011 +0200
@@ -670,7 +670,7 @@
|] ==> \<exists>x. a \<le> x & x \<le> b & f(x) = y"
apply (subgoal_tac "- f a \<le> -y & -y \<le> - f b", clarify)
apply (drule IVT [where f = "%x. - f x"], assumption)
-apply (auto intro: isCont_minus)
+apply simp_all
done
(*HOL style here: object-level formulations*)
@@ -750,7 +750,7 @@
with M1 have M3: "\<forall>x. a \<le> x & x \<le> b --> f x < M"
by (fastsimp simp add: linorder_not_le [symmetric])
hence "\<forall>x. a \<le> x & x \<le> b --> isCont (%x. inverse (M - f x)) x"
- by (auto simp add: isCont_inverse isCont_diff con)
+ by (auto simp add: con)
from isCont_bounded [OF le this]
obtain k where k: "!!x. a \<le> x & x \<le> b --> inverse (M - f x) \<le> k" by auto
have Minv: "!!x. a \<le> x & x \<le> b --> 0 < inverse (M - f (x))"
@@ -1059,8 +1059,8 @@
(f(b) - f(a) = (b-a) * l)"
proof -
let ?F = "%x. f x - ((f b - f a) / (b-a)) * x"
- have contF: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?F x" using con
- by (fast intro: isCont_diff isCont_const isCont_mult isCont_ident)
+ have contF: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?F x"
+ using con by (fast intro: isCont_intros)
have difF: "\<forall>x. a < x \<and> x < b \<longrightarrow> ?F differentiable x"
proof (clarify)
fix x::real
@@ -1353,7 +1353,7 @@
==> \<exists>z. \<bar>z-x\<bar> \<le> d & f z < f x"
apply (insert lemma_isCont_inj
[where f = "%x. - f x" and g = "%y. g(-y)" and x = x and d = d])
-apply (simp add: isCont_minus linorder_not_le)
+apply (simp add: linorder_not_le)
done
text{*Show there's an interval surrounding @{term "f(x)"} in
@@ -1509,27 +1509,9 @@
let ?h = "\<lambda>x. (f b - f a)*(g x) - (g b - g a)*(f x)"
from assms have "a < b" by simp
moreover have "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?h x"
- proof -
- have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. f b - f a) x" by simp
- with gc have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. (f b - f a) * g x) x"
- by (auto intro: isCont_mult)
- moreover
- have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. g b - g a) x" by simp
- with fc have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. (g b - g a) * f x) x"
- by (auto intro: isCont_mult)
- ultimately show ?thesis
- by (fastsimp intro: isCont_diff)
- qed
- moreover
- have "\<forall>x. a < x \<and> x < b \<longrightarrow> ?h differentiable x"
- proof -
- have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. f b - f a) differentiable x" by simp
- with gd have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. (f b - f a) * g x) differentiable x" by simp
- moreover
- have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. g b - g a) differentiable x" by simp
- with fd have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. (g b - g a) * f x) differentiable x" by simp
- ultimately show ?thesis by simp
- qed
+ using fc gc by simp
+ moreover have "\<forall>x. a < x \<and> x < b \<longrightarrow> ?h differentiable x"
+ using fd gd by simp
ultimately have "\<exists>l z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" by (rule MVT)
then obtain l where ldef: "\<exists>z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" ..
then obtain c where cdef: "a < c \<and> c < b \<and> DERIV ?h c :> l \<and> ?h b - ?h a = (b - a) * l" ..
--- a/src/HOL/Library/Inner_Product.thy Wed Aug 17 07:13:13 2011 +0200
+++ b/src/HOL/Library/Inner_Product.thy Wed Aug 17 18:51:27 2011 +0200
@@ -175,6 +175,8 @@
bounded_linear "\<lambda>y::'a::real_inner. inner x y"
by (rule inner.bounded_linear_right)
+declare inner.isCont [simp]
+
subsection {* Class instances *}
--- a/src/HOL/Library/Product_Vector.thy Wed Aug 17 07:13:13 2011 +0200
+++ b/src/HOL/Library/Product_Vector.thy Wed Aug 17 18:51:27 2011 +0200
@@ -359,6 +359,16 @@
(simp add: subsetD [OF `A \<times> B \<subseteq> S`])
qed
+lemma isCont_fst [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a"
+ unfolding isCont_def by (rule tendsto_fst)
+
+lemma isCont_snd [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. snd (f x)) a"
+ unfolding isCont_def by (rule tendsto_snd)
+
+lemma isCont_Pair [simp]:
+ "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) a"
+ unfolding isCont_def by (rule tendsto_Pair)
+
lemma Cauchy_fst: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. fst (X n))"
unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le])
@@ -381,10 +391,6 @@
then show "\<exists>n0. \<forall>m\<ge>n0. \<forall>n\<ge>n0. dist (X m, Y m) (X n, Y n) < r" ..
qed
-lemma isCont_Pair [simp]:
- "\<lbrakk>isCont f x; isCont g x\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) x"
- unfolding isCont_def by (rule tendsto_Pair)
-
subsection {* Product is a complete metric space *}
instance prod :: (complete_space, complete_space) complete_space
--- a/src/HOL/Lim.thy Wed Aug 17 07:13:13 2011 +0200
+++ b/src/HOL/Lim.thy Wed Aug 17 18:51:27 2011 +0200
@@ -321,9 +321,6 @@
"g -- a --> l \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> f l"
by (rule tendsto)
-lemma (in bounded_linear) cont: "f -- a --> f a"
-by (rule LIM [OF LIM_ident])
-
lemma (in bounded_linear) LIM_zero:
"g -- a --> 0 \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> 0"
by (rule tendsto_zero)
@@ -401,39 +398,46 @@
lemma isCont_const [simp]: "isCont (\<lambda>x. k) a"
unfolding isCont_def by (rule LIM_const)
-lemma isCont_norm:
+lemma isCont_norm [simp]:
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
unfolding isCont_def by (rule LIM_norm)
-lemma isCont_rabs: "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x :: real\<bar>) a"
+lemma isCont_rabs [simp]:
+ fixes f :: "'a::topological_space \<Rightarrow> real"
+ shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x\<bar>) a"
unfolding isCont_def by (rule LIM_rabs)
-lemma isCont_add:
+lemma isCont_add [simp]:
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
unfolding isCont_def by (rule LIM_add)
-lemma isCont_minus:
+lemma isCont_minus [simp]:
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
unfolding isCont_def by (rule LIM_minus)
-lemma isCont_diff:
+lemma isCont_diff [simp]:
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
unfolding isCont_def by (rule LIM_diff)
-lemma isCont_mult:
+lemma isCont_mult [simp]:
fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra"
shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a"
unfolding isCont_def by (rule LIM_mult)
-lemma isCont_inverse:
+lemma isCont_inverse [simp]:
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. inverse (f x)) a"
unfolding isCont_def by (rule LIM_inverse)
+lemma isCont_divide [simp]:
+ fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_field"
+ shows "\<lbrakk>isCont f a; isCont g a; g a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x / g x) a"
+ unfolding isCont_def by (rule tendsto_divide)
+
lemma isCont_LIM_compose:
"\<lbrakk>isCont g l; f -- a --> l\<rbrakk> \<Longrightarrow> (\<lambda>x. g (f x)) -- a --> g l"
unfolding isCont_def by (rule LIM_compose)
@@ -459,37 +463,40 @@
lemma isCont_o: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (g o f) a"
unfolding o_def by (rule isCont_o2)
-lemma (in bounded_linear) isCont: "isCont f a"
- unfolding isCont_def by (rule cont)
+lemma (in bounded_linear) isCont:
+ "isCont g a \<Longrightarrow> isCont (\<lambda>x. f (g x)) a"
+ unfolding isCont_def by (rule LIM)
lemma (in bounded_bilinear) isCont:
"\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
unfolding isCont_def by (rule LIM)
-lemmas isCont_scaleR = scaleR.isCont
+lemmas isCont_scaleR [simp] = scaleR.isCont
-lemma isCont_of_real:
+lemma isCont_of_real [simp]:
"isCont f a \<Longrightarrow> isCont (\<lambda>x. of_real (f x)::'b::real_normed_algebra_1) a"
- unfolding isCont_def by (rule LIM_of_real)
+ by (rule of_real.isCont)
-lemma isCont_power:
+lemma isCont_power [simp]:
fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
unfolding isCont_def by (rule LIM_power)
-lemma isCont_sgn:
+lemma isCont_sgn [simp]:
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a"
unfolding isCont_def by (rule LIM_sgn)
-lemma isCont_abs [simp]: "isCont abs (a::real)"
-by (rule isCont_rabs [OF isCont_ident])
+lemma isCont_setsum [simp]:
+ fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::real_normed_vector"
+ fixes A :: "'a set"
+ shows "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>A. f i x) a"
+ unfolding isCont_def by (simp add: tendsto_setsum)
-lemma isCont_setsum:
- fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::real_normed_vector"
- fixes A :: "'a set" assumes "finite A"
- shows "\<forall> i \<in> A. isCont (f i) x \<Longrightarrow> isCont (\<lambda> x. \<Sum> i \<in> A. f i x) x"
- unfolding isCont_def by (simp add: tendsto_setsum)
+lemmas isCont_intros =
+ isCont_ident isCont_const isCont_norm isCont_rabs isCont_add isCont_minus
+ isCont_diff isCont_mult isCont_inverse isCont_divide isCont_scaleR
+ isCont_of_real isCont_power isCont_sgn isCont_setsum
lemma LIM_less_bound: fixes f :: "real \<Rightarrow> real" assumes "b < x"
and all_le: "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and isCont: "isCont f x"
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Wed Aug 17 07:13:13 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Wed Aug 17 18:51:27 2011 +0200
@@ -1100,8 +1100,7 @@
unfolding continuous_on_def by (intro ballI tendsto_intros)
lemma closed_positive_orthant: "closed {x::real^'n. \<forall>i. 0 \<le>x$i}"
- unfolding Collect_all_eq
- by (intro closed_INT ballI closed_Collect_le isCont_const vec_nth.isCont)
+ by (simp add: Collect_all_eq closed_INT closed_Collect_le)
lemma Lim_component_cart:
fixes f :: "'a \<Rightarrow> 'b::metric_space ^ 'n"
@@ -1287,13 +1286,11 @@
lemma closed_interval_left_cart: fixes b::"real^'n"
shows "closed {x::real^'n. \<forall>i. x$i \<le> b$i}"
- unfolding Collect_all_eq
- by (intro closed_INT ballI closed_Collect_le isCont_const vec_nth.isCont)
+ by (simp add: Collect_all_eq closed_INT closed_Collect_le)
lemma closed_interval_right_cart: fixes a::"real^'n"
shows "closed {x::real^'n. \<forall>i. a$i \<le> x$i}"
- unfolding Collect_all_eq
- by (intro closed_INT ballI closed_Collect_le isCont_const vec_nth.isCont)
+ by (simp add: Collect_all_eq closed_INT closed_Collect_le)
lemma is_interval_cart:"is_interval (s::(real^'n) set) \<longleftrightarrow>
(\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i. ((a$i \<le> x$i \<and> x$i \<le> b$i) \<or> (b$i \<le> x$i \<and> x$i \<le> a$i))) \<longrightarrow> x \<in> s)"
@@ -1301,19 +1298,19 @@
lemma closed_halfspace_component_le_cart:
shows "closed {x::real^'n. x$i \<le> a}"
- by (intro closed_Collect_le vec_nth.isCont isCont_const)
+ by (simp add: closed_Collect_le)
lemma closed_halfspace_component_ge_cart:
shows "closed {x::real^'n. x$i \<ge> a}"
- by (intro closed_Collect_le vec_nth.isCont isCont_const)
+ by (simp add: closed_Collect_le)
lemma open_halfspace_component_lt_cart:
shows "open {x::real^'n. x$i < a}"
- by (intro open_Collect_less vec_nth.isCont isCont_const)
+ by (simp add: open_Collect_less)
lemma open_halfspace_component_gt_cart:
shows "open {x::real^'n. x$i > a}"
- by (intro open_Collect_less vec_nth.isCont isCont_const)
+ by (simp add: open_Collect_less)
lemma Lim_component_le_cart: fixes f :: "'a \<Rightarrow> real^'n"
assumes "(f ---> l) net" "\<not> (trivial_limit net)" "eventually (\<lambda>x. f(x)$i \<le> b) net"
@@ -1352,8 +1349,7 @@
proof-
{ fix i::'n
have "closed {x::'a ^ 'n. P i \<longrightarrow> x$i = 0}"
- by (cases "P i", simp_all,
- intro closed_Collect_eq vec_nth.isCont isCont_const) }
+ by (cases "P i", simp_all add: closed_Collect_eq) }
thus ?thesis
unfolding Collect_all_eq by (simp add: closed_INT)
qed
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Aug 17 07:13:13 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Aug 17 18:51:27 2011 +0200
@@ -124,6 +124,8 @@
bounded_linear "\<lambda>x. euclidean_component x i"
by (rule bounded_linear_euclidean_component)
+declare euclidean_component.isCont [simp]
+
lemma euclidean_eqI:
fixes x y :: "'a::euclidean_space"
assumes "\<And>i. i < DIM('a) \<Longrightarrow> x $$ i = y $$ i" shows "x = y"
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Wed Aug 17 07:13:13 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Wed Aug 17 18:51:27 2011 +0200
@@ -408,6 +408,8 @@
apply (rule_tac x="1" in exI, simp add: norm_nth_le)
done
+declare vec_nth.isCont [simp]
+
instance vec :: (banach, finite) banach ..
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Aug 17 07:13:13 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Aug 17 18:51:27 2011 +0200
@@ -5229,37 +5229,37 @@
unfolding continuous_on by (rule ballI) (intro tendsto_intros)
lemma closed_halfspace_le: "closed {x. inner a x \<le> b}"
- by (intro closed_Collect_le inner.isCont isCont_const isCont_ident)
+ by (simp add: closed_Collect_le)
lemma closed_halfspace_ge: "closed {x. inner a x \<ge> b}"
- by (intro closed_Collect_le inner.isCont isCont_const isCont_ident)
+ by (simp add: closed_Collect_le)
lemma closed_hyperplane: "closed {x. inner a x = b}"
- by (intro closed_Collect_eq inner.isCont isCont_const isCont_ident)
+ by (simp add: closed_Collect_eq)
lemma closed_halfspace_component_le:
shows "closed {x::'a::euclidean_space. x$$i \<le> a}"
- by (intro closed_Collect_le euclidean_component.isCont isCont_const)
+ by (simp add: closed_Collect_le)
lemma closed_halfspace_component_ge:
shows "closed {x::'a::euclidean_space. x$$i \<ge> a}"
- by (intro closed_Collect_le euclidean_component.isCont isCont_const)
+ by (simp add: closed_Collect_le)
text {* Openness of halfspaces. *}
lemma open_halfspace_lt: "open {x. inner a x < b}"
- by (intro open_Collect_less inner.isCont isCont_const isCont_ident)
+ by (simp add: open_Collect_less)
lemma open_halfspace_gt: "open {x. inner a x > b}"
- by (intro open_Collect_less inner.isCont isCont_const isCont_ident)
+ by (simp add: open_Collect_less)
lemma open_halfspace_component_lt:
shows "open {x::'a::euclidean_space. x$$i < a}"
- by (intro open_Collect_less euclidean_component.isCont isCont_const)
+ by (simp add: open_Collect_less)
lemma open_halfspace_component_gt:
shows "open {x::'a::euclidean_space. x$$i > a}"
- by (intro open_Collect_less euclidean_component.isCont isCont_const)
+ by (simp add: open_Collect_less)
text{* Instantiation for intervals on @{text ordered_euclidean_space} *}
@@ -5297,15 +5297,13 @@
fixes a :: "'a\<Colon>ordered_euclidean_space"
shows "closed {.. a}"
unfolding eucl_atMost_eq_halfspaces
- by (intro closed_INT ballI closed_Collect_le
- euclidean_component.isCont isCont_const)
+ by (simp add: closed_INT closed_Collect_le)
lemma closed_eucl_atLeast[simp, intro]:
fixes a :: "'a\<Colon>ordered_euclidean_space"
shows "closed {a ..}"
unfolding eucl_atLeast_eq_halfspaces
- by (intro closed_INT ballI closed_Collect_le
- euclidean_component.isCont isCont_const)
+ by (simp add: closed_INT closed_Collect_le)
lemma open_vimage_euclidean_component: "open S \<Longrightarrow> open ((\<lambda>x. x $$ i) -` S)"
by (auto intro!: continuous_open_vimage)
--- a/src/HOL/Tools/ATP/atp_problem.ML Wed Aug 17 07:13:13 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Wed Aug 17 18:51:27 2011 +0200
@@ -19,7 +19,14 @@
datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
- datatype format = CNF | CNF_UEQ | FOF | TFF | THF
+ datatype thf_flavor = Without_Choice | With_Choice
+ datatype format =
+ CNF |
+ CNF_UEQ |
+ FOF |
+ TFF |
+ THF of thf_flavor
+
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
Decl of string * 'a * 'a ho_type |
@@ -73,6 +80,7 @@
bool option -> (bool option -> 'c -> 'd -> 'd) -> ('a, 'b, 'c) formula
-> 'd -> 'd
val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula
+ val is_format_thf : format -> bool
val is_format_typed : format -> bool
val tptp_lines_for_atp_problem : format -> string problem -> string list
val ensure_cnf_problem :
@@ -107,7 +115,14 @@
datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
-datatype format = CNF | CNF_UEQ | FOF | TFF | THF
+datatype thf_flavor = Without_Choice | With_Choice
+datatype format =
+ CNF |
+ CNF_UEQ |
+ FOF |
+ TFF |
+ THF of thf_flavor
+
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
Decl of string * 'a * 'a ho_type |
@@ -189,7 +204,11 @@
| formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
| formula_map f (AAtom tm) = AAtom (f tm)
-val is_format_typed = member (op =) [TFF, THF]
+fun is_format_thf (THF _) = true
+ | is_format_thf _ = false
+fun is_format_typed TFF = true
+ | is_format_typed (THF _) = true
+ | is_format_typed _ = false
fun string_for_kind Axiom = "axiom"
| string_for_kind Definition = "definition"
@@ -202,7 +221,7 @@
raise Fail "unexpected higher-order type in first-order format"
| strip_tff_type (AType s) = ([], s)
-fun string_for_type THF ty =
+fun string_for_type (THF _) ty =
let
fun aux _ (AType s) = s
| aux rhs (AFun (ty1, ty2)) =
@@ -228,7 +247,7 @@
| string_for_connective AIff = tptp_iff
fun string_for_bound_var format (s, ty) =
- s ^ (if format = TFF orelse format = THF then
+ s ^ (if is_format_typed format then
" " ^ tptp_has_type ^ " " ^
string_for_type format (ty |> the_default (AType tptp_individual_type))
else
@@ -241,7 +260,7 @@
"[" ^ commas (map (string_for_term format) ts) ^ "]"
else if is_tptp_equal s then
space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts)
- |> format = THF ? enclose "(" ")"
+ |> is_format_thf format ? enclose "(" ")"
else
(case (s = tptp_ho_forall orelse s = tptp_ho_exists, ts) of
(true, [AAbs ((s', ty), tm)]) =>
@@ -252,14 +271,14 @@
[(s', SOME ty)], AAtom tm))
| _ =>
let val ss = map (string_for_term format) ts in
- if format = THF then
+ if is_format_thf format then
"(" ^ space_implode (" " ^ tptp_app ^ " ") (s :: ss) ^ ")"
else
s ^ "(" ^ commas ss ^ ")"
end)
- | string_for_term THF (AAbs ((s, ty), tm)) =
- "(^[" ^ s ^ " : " ^ string_for_type THF ty ^ "] : " ^
- string_for_term THF tm ^ ")"
+ | string_for_term (format as THF _) (AAbs ((s, ty), tm)) =
+ "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "] : " ^
+ string_for_term format tm ^ ")"
| string_for_term _ _ = raise Fail "unexpected term in first-order format"
and string_for_formula format (AQuant (q, xs, phi)) =
string_for_quantifier q ^
@@ -270,10 +289,10 @@
(AConn (ANot, [AAtom (ATerm ("=" (* tptp_equal *), ts))])) =
space_implode (" " ^ tptp_not_infix ^ tptp_equal ^ " ")
(map (string_for_term format) ts)
- |> format = THF ? enclose "(" ")"
+ |> is_format_thf format ? enclose "(" ")"
| string_for_formula format (AConn (c, [phi])) =
string_for_connective c ^ " " ^
- (string_for_formula format phi |> format = THF ? enclose "(" ")")
+ (string_for_formula format phi |> is_format_thf format ? enclose "(" ")")
|> enclose "(" ")"
| string_for_formula format (AConn (c, phis)) =
space_implode (" " ^ string_for_connective c ^ " ")
@@ -290,7 +309,7 @@
| string_for_format CNF_UEQ = tptp_cnf
| string_for_format FOF = tptp_fof
| string_for_format TFF = tptp_tff
- | string_for_format THF = tptp_thf
+ | string_for_format (THF _) = tptp_thf
fun string_for_problem_line format (Decl (ident, sym, ty)) =
string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ " : " ^
--- a/src/HOL/Tools/ATP/atp_systems.ML Wed Aug 17 07:13:13 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Aug 17 18:51:27 2011 +0200
@@ -242,7 +242,7 @@
known_failures = [],
conj_sym_kind = Axiom,
prem_kind = Hypothesis,
- formats = [THF, FOF],
+ formats = [THF Without_Choice, FOF],
best_slices = fn ctxt =>
(* FUDGE *)
[(0.667, (false, (150, "simple_higher", sosN))),
@@ -265,7 +265,7 @@
known_failures = [(ProofMissing, "SZS status Theorem")],
conj_sym_kind = Axiom,
prem_kind = Hypothesis,
- formats = [THF],
+ formats = [THF With_Choice],
best_slices = K [(1.0, (true, (100, "simple_higher", "")))] (* FUDGE *)}
val satallax = (satallaxN, satallax_config)
--- a/src/HOL/Tools/ATP/atp_translate.ML Wed Aug 17 07:13:13 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Aug 17 18:51:27 2011 +0200
@@ -604,12 +604,14 @@
val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
fun choose_format formats (Simple_Types (order, level)) =
- if member (op =) formats THF then
- (THF, Simple_Types (order, level))
- else if member (op =) formats TFF then
- (TFF, Simple_Types (First_Order, level))
- else
- choose_format formats (Guards (Mangled_Monomorphic, level, Heavyweight))
+ (case find_first is_format_thf formats of
+ SOME format => (format, Simple_Types (order, level))
+ | NONE =>
+ if member (op =) formats TFF then
+ (TFF, Simple_Types (First_Order, level))
+ else
+ choose_format formats
+ (Guards (Mangled_Monomorphic, level, Heavyweight)))
| choose_format formats type_enc =
(case hd formats of
CNF_UEQ =>
@@ -760,7 +762,7 @@
(true, @{type_name bool}) => `I tptp_bool_type
| (true, @{type_name fun}) => `I tptp_fun_type
| _ => if s = homo_infinite_type_name andalso
- (format = TFF orelse format = THF) then
+ is_format_typed format then
`I tptp_individual_type
else
`make_fixed_type_const s,
--- a/src/Pure/General/position.ML Wed Aug 17 07:13:13 2011 +0200
+++ b/src/Pure/General/position.ML Wed Aug 17 18:51:27 2011 +0200
@@ -171,7 +171,7 @@
(case (line_of pos, file_of pos) of
(SOME i, NONE) => "(line " ^ string_of_int i ^ ")"
| (SOME i, SOME name) => "(line " ^ string_of_int i ^ " of " ^ quote name ^ ")"
- | (NONE, SOME name) => "(" ^ quote name ^ ")"
+ | (NONE, SOME name) => "(file " ^ quote name ^ ")"
| _ => "");
in
if null props then ""
--- a/src/Pure/PIDE/document.ML Wed Aug 17 07:13:13 2011 +0200
+++ b/src/Pure/PIDE/document.ML Wed Aug 17 18:51:27 2011 +0200
@@ -86,7 +86,6 @@
val clear_node = map_node (fn (header, _, _) => (header, Entries.empty, empty_exec));
fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
-fun remove_node name nodes = Graph.del_node name nodes handle Graph.UNDEF _ => nodes;
fun default_node name = Graph.default_node (name, empty_node);
fun update_node name f = default_node name #> Graph.map_node name f;
@@ -141,22 +140,19 @@
|> update_node name (edit_node edits)
| Header header =>
let
- val node = get_node nodes name;
- val nodes' = Graph.new_node (name, node) (remove_node name nodes);
- val parents =
- (case header of Exn.Res (_, parents, _) => parents | _ => [])
- |> filter (can (Graph.get_node nodes'));
- val (header', nodes'') =
- (header, Graph.add_deps_acyclic (name, parents) nodes')
- handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes')
- | Graph.UNDEF d => (Exn.Exn (ERROR ("Undefined theory entry: " ^ quote d)), nodes')
- in
- nodes''
- |> Graph.map_node name (set_header header')
- end));
+ val parents = (case header of Exn.Res (_, parents, _) => parents | _ => []);
+ val nodes1 = nodes
+ |> default_node name
+ |> fold default_node parents;
+ val nodes2 = nodes1
+ |> fold (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
+ val (header', nodes3) =
+ (header, Graph.add_deps_acyclic (name, parents) nodes2)
+ handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
+ in Graph.map_node name (set_header header') nodes3 end));
-fun def_node name (Version nodes) = Version (default_node name nodes);
-fun put_node (name, node) (Version nodes) = Version (update_node name (K node) nodes);
+fun put_node (name, node) (Version nodes) =
+ Version (update_node name (K node) nodes);
end;
@@ -331,10 +327,7 @@
let
val old_version = the_version state old_id;
val _ = Time.now (); (* FIXME odd workaround for polyml-5.4.0/x86_64 *)
- val new_version =
- old_version
- |> fold (def_node o #1) edits
- |> fold edit_nodes edits;
+ val new_version = fold edit_nodes edits old_version;
val updates =
nodes_of new_version |> Graph.schedule
@@ -347,16 +340,17 @@
let
val (thy_name, imports, uses) = Exn.release (get_header node);
(* FIXME provide files via Scala layer *)
- val dir = Path.dir (Path.explode name);
- val files = map (apfst Path.explode) uses;
+ val (dir, files) =
+ if ML_System.platform_is_cygwin then (Path.current, [])
+ else (Path.dir (Path.explode name), map (apfst Path.explode) uses);
val parents =
imports |> map (fn import =>
- (case AList.lookup (op =) deps import of
- SOME parent_future =>
- get_theory (Position.file_only (import ^ ".thy"))
- (#2 (Future.join parent_future))
- | NONE => Thy_Info.get_theory (Thy_Info.base_name import)));
+ (case Thy_Info.lookup_theory import of
+ SOME thy => thy
+ | NONE =>
+ get_theory (Position.file_only import)
+ (#2 (Future.join (the (AList.lookup (op =) deps import))))));
in Thy_Load.begin_theory dir thy_name imports files parents end
fun get_command id =
(id, the_command state id |> Future.map (Toplevel.modify_init init));
--- a/src/Pure/PIDE/document.scala Wed Aug 17 07:13:13 2011 +0200
+++ b/src/Pure/PIDE/document.scala Wed Aug 17 18:51:27 2011 +0200
@@ -53,9 +53,9 @@
case class Edits[A](edits: List[A]) extends Edit[A]
case class Header[A](header: Node_Header) extends Edit[A]
- def norm_header[A](f: String => String, header: Node_Header): Header[A] =
+ def norm_header[A](f: String => String, g: String => String, header: Node_Header): Header[A] =
header match {
- case Exn.Res(h) => Header[A](Exn.capture { h.norm_deps(f) })
+ case Exn.Res(h) => Header[A](Exn.capture { h.norm_deps(f, g) })
case exn => Header[A](exn)
}
--- a/src/Pure/System/session.scala Wed Aug 17 07:13:13 2011 +0200
+++ b/src/Pure/System/session.scala Wed Aug 17 18:51:27 2011 +0200
@@ -189,9 +189,15 @@
val syntax = current_syntax()
val previous = global_state().history.tip.version
- val norm_header =
- Document.Node.norm_header[Text.Edit](
- name => file_store.append(master_dir, Path.explode(name)), header)
+ def norm_import(s: String): String =
+ {
+ val name = Thy_Header.base_name(s)
+ if (thy_load.is_loaded(name)) name
+ else file_store.append(master_dir, Thy_Header.thy_path(Path.explode(s)))
+ }
+ def norm_use(s: String): String = file_store.append(master_dir, Path.explode(s))
+ val norm_header = Document.Node.norm_header[Text.Edit](norm_import, norm_use, header)
+
val text_edits = (name, norm_header) :: edits.map(edit => (name, edit))
val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) }
val change =
--- a/src/Pure/Thy/thy_header.scala Wed Aug 17 07:13:13 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala Wed Aug 17 18:51:27 2011 +0200
@@ -28,11 +28,16 @@
/* theory file name */
- private val Thy_Name = new Regex("""(.*?)([^/\\:]+)\.thy""")
+ private val Base_Name = new Regex(""".*?([^/\\:]+)""")
+ private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
- def thy_name(s: String): Option[(String, String)] =
- s match { case Thy_Name(prefix, name) => Some((prefix, name)) case _ => None }
+ def base_name(s: String): String =
+ s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
+ def thy_name(s: String): Option[String] =
+ s match { case Thy_Name(name) => Some(name) case _ => None }
+
+ def thy_path(path: Path): Path = path.ext("thy")
def thy_path(name: String): Path = Path.basic(name).ext("thy")
@@ -113,7 +118,7 @@
def map(f: String => String): Thy_Header =
Thy_Header(f(name), imports.map(f), uses.map(p => (f(p._1), p._2)))
- def norm_deps(f: String => String): Thy_Header =
- copy(imports = imports.map(name => f(name)), uses = uses.map(p => (f(p._1), p._2)))
+ def norm_deps(f: String => String, g: String => String): Thy_Header =
+ copy(imports = imports.map(name => f(name)), uses = uses.map(p => (g(p._1), p._2)))
}
--- a/src/Pure/Thy/thy_info.ML Wed Aug 17 07:13:13 2011 +0200
+++ b/src/Pure/Thy/thy_info.ML Wed Aug 17 18:51:27 2011 +0200
@@ -9,7 +9,6 @@
sig
datatype action = Update | Remove
val add_hook: (action -> string -> unit) -> unit
- val base_name: string -> string
val get_names: unit -> string list
val status: unit -> unit
val lookup_theory: string -> theory option
--- a/src/Tools/jEdit/src/plugin.scala Wed Aug 17 07:13:13 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Wed Aug 17 18:51:27 2011 +0200
@@ -190,9 +190,7 @@
{
val master_dir = buffer.getDirectory
val path = buffer.getSymlinkPath
- if (VFSManager.getVFSForPath(path).isInstanceOf[FileVFS])
- (Isabelle_System.posix_path(master_dir), Isabelle_System.posix_path(path))
- else (master_dir, path)
+ (master_dir, path)
}
@@ -210,8 +208,8 @@
case None =>
val (master_dir, path) = buffer_path(buffer)
Thy_Header.thy_name(path) match {
- case Some((prefix, name)) =>
- Some(Document_Model.init(session, buffer, master_dir, prefix + name, name))
+ case Some(name) =>
+ Some(Document_Model.init(session, buffer, master_dir, path, name))
case None => None
}
}
@@ -334,8 +332,8 @@
else {
val vfs = VFSManager.getVFSForPath(master_dir)
if (vfs.isInstanceOf[FileVFS])
- vfs.constructPath(master_dir, Isabelle_System.platform_path(path))
- // FIXME MiscUtilities.resolveSymlinks (!?)
+ MiscUtilities.resolveSymlinks(
+ vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
}
}