--- a/NEWS Wed Aug 04 10:51:04 2010 +0200
+++ b/NEWS Wed Aug 04 10:52:29 2010 +0200
@@ -14,6 +14,10 @@
consistent view on symbols, while raw explode (or String.explode)
merely give a byte-oriented representation.
+* Theory loading: only the master source file is looked-up in the
+implicit load path, all other files are addressed relatively to its
+directory. Minor INCOMPATIBILITY, subtle change in semantics.
+
* Special treatment of ML file names has been discontinued.
Historically, optional extensions .ML or .sml were added on demand --
at the cost of clarity of file dependencies. Recall that Isabelle/ML
--- a/src/HOL/Algebra/UnivPoly.thy Wed Aug 04 10:51:04 2010 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Wed Aug 04 10:52:29 2010 +0200
@@ -1557,128 +1557,93 @@
assumes g_in_P [simp]: "g \<in> carrier P" and f_in_P [simp]: "f \<in> carrier P"
and g_not_zero: "g \<noteq> \<zero>\<^bsub>P\<^esub>"
shows "\<exists> q r (k::nat). (q \<in> carrier P) \<and> (r \<in> carrier P) \<and> (lcoeff g)(^)\<^bsub>R\<^esub>k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r \<and> (r = \<zero>\<^bsub>P\<^esub> | deg R r < deg R g)"
-proof -
+ using f_in_P
+proof (induct "deg R f" arbitrary: "f" rule: nat_less_induct)
+ case (1 f)
+ note f_in_P [simp] = "1.prems"
let ?pred = "(\<lambda> q r (k::nat).
- (q \<in> carrier P) \<and> (r \<in> carrier P) \<and> (lcoeff g)(^)\<^bsub>R\<^esub>k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r \<and> (r = \<zero>\<^bsub>P\<^esub> | deg R r < deg R g))"
- and ?lg = "lcoeff g"
- show ?thesis
- (*JE: we distinguish some particular cases where the solution is almost direct.*)
+ (q \<in> carrier P) \<and> (r \<in> carrier P)
+ \<and> (lcoeff g)(^)\<^bsub>R\<^esub>k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r \<and> (r = \<zero>\<^bsub>P\<^esub> | deg R r < deg R g))"
+ let ?lg = "lcoeff g" and ?lf = "lcoeff f"
+ show ?case
proof (cases "deg R f < deg R g")
- case True
- (*JE: if the degree of f is smaller than the one of g the solution is straightforward.*)
- (* CB: avoid exI3 *)
- have "?pred \<zero>\<^bsub>P\<^esub> f 0" using True by force
- then show ?thesis by fast
+ case True
+ have "?pred \<zero>\<^bsub>P\<^esub> f 0" using True by force
+ then show ?thesis by blast
next
case False then have deg_g_le_deg_f: "deg R g \<le> deg R f" by simp
{
- (*JE: we now apply the induction hypothesis with some additional facts required*)
- from f_in_P deg_g_le_deg_f show ?thesis
- proof (induct "deg R f" arbitrary: "f" rule: less_induct)
- case less
- note f_in_P [simp] = `f \<in> carrier P`
- and deg_g_le_deg_f = `deg R g \<le> deg R f`
- let ?k = "1::nat" and ?r = "(g \<otimes>\<^bsub>P\<^esub> (monom P (lcoeff f) (deg R f - deg R g))) \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> (lcoeff g \<odot>\<^bsub>P\<^esub> f)"
- and ?q = "monom P (lcoeff f) (deg R f - deg R g)"
- show "\<exists> q r (k::nat). q \<in> carrier P \<and> r \<in> carrier P \<and> lcoeff g (^) k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r & (r = \<zero>\<^bsub>P\<^esub> | deg R r < deg R g)"
- proof -
- (*JE: we first extablish the existence of a triple satisfying the previous equation.
- Then we will have to prove the second part of the predicate.*)
- have exist: "lcoeff g (^) ?k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> ?r"
- using minus_add
- using sym [OF a_assoc [of "g \<otimes>\<^bsub>P\<^esub> ?q" "\<ominus>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q)" "lcoeff g \<odot>\<^bsub>P\<^esub> f"]]
- using r_neg by auto
+ let ?k = "1::nat"
+ let ?f1 = "(g \<otimes>\<^bsub>P\<^esub> (monom P (?lf) (deg R f - deg R g))) \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> (?lg \<odot>\<^bsub>P\<^esub> f)"
+ let ?q = "monom P (?lf) (deg R f - deg R g)"
+ have f1_in_carrier: "?f1 \<in> carrier P" and q_in_carrier: "?q \<in> carrier P" by simp_all
+ show ?thesis
+ proof (cases "deg R f = 0")
+ case True
+ {
+ have deg_g: "deg R g = 0" using True using deg_g_le_deg_f by simp
+ have "?pred f \<zero>\<^bsub>P\<^esub> 1"
+ using deg_zero_impl_monom [OF g_in_P deg_g]
+ using sym [OF monom_mult_is_smult [OF coeff_closed [OF g_in_P, of 0] f_in_P]]
+ using deg_g by simp
+ then show ?thesis by blast
+ }
+ next
+ case False note deg_f_nzero = False
+ {
+ have exist: "lcoeff g (^) ?k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> ?f1"
+ by (simp add: minus_add r_neg sym [
+ OF a_assoc [of "g \<otimes>\<^bsub>P\<^esub> ?q" "\<ominus>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q)" "lcoeff g \<odot>\<^bsub>P\<^esub> f"]])
+ have deg_remainder_l_f: "deg R (\<ominus>\<^bsub>P\<^esub> ?f1) < deg R f"
+ proof (unfold deg_uminus [OF f1_in_carrier])
+ show "deg R ?f1 < deg R f"
+ proof (rule deg_lcoeff_cancel)
+ show "deg R (\<ominus>\<^bsub>P\<^esub> (?lg \<odot>\<^bsub>P\<^esub> f)) \<le> deg R f"
+ using deg_smult_ring [of ?lg f]
+ using lcoeff_nonzero2 [OF g_in_P g_not_zero] by simp
+ show "deg R (g \<otimes>\<^bsub>P\<^esub> ?q) \<le> deg R f"
+ by (simp add: monom_deg_mult [OF f_in_P g_in_P deg_g_le_deg_f, of ?lf])
+ show "coeff P (g \<otimes>\<^bsub>P\<^esub> ?q) (deg R f) = \<ominus> coeff P (\<ominus>\<^bsub>P\<^esub> (?lg \<odot>\<^bsub>P\<^esub> f)) (deg R f)"
+ unfolding coeff_mult [OF g_in_P monom_closed
+ [OF lcoeff_closed [OF f_in_P],
+ of "deg R f - deg R g"], of "deg R f"]
+ unfolding coeff_monom [OF lcoeff_closed
+ [OF f_in_P], of "(deg R f - deg R g)"]
+ using R.finsum_cong' [of "{..deg R f}" "{..deg R f}"
+ "(\<lambda>i. coeff P g i \<otimes> (if deg R f - deg R g = deg R f - i then ?lf else \<zero>))"
+ "(\<lambda>i. if deg R g = i then coeff P g i \<otimes> ?lf else \<zero>)"]
+ using R.finsum_singleton [of "deg R g" "{.. deg R f}" "(\<lambda>i. coeff P g i \<otimes> ?lf)"]
+ unfolding Pi_def using deg_g_le_deg_f by force
+ qed (simp_all add: deg_f_nzero)
+ qed
+ then obtain q' r' k'
+ where rem_desc: "?lg (^) (k'::nat) \<odot>\<^bsub>P\<^esub> (\<ominus>\<^bsub>P\<^esub> ?f1) = g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r'"
+ and rem_deg: "(r' = \<zero>\<^bsub>P\<^esub> \<or> deg R r' < deg R g)"
+ and q'_in_carrier: "q' \<in> carrier P" and r'_in_carrier: "r' \<in> carrier P"
+ using "1.hyps" using f1_in_carrier by blast
show ?thesis
- proof (cases "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < deg R g")
- (*JE: if the degree of the remainder satisfies the statement property we are done*)
- case True
- {
- show ?thesis
- proof (rule exI3 [of _ ?q "\<ominus>\<^bsub>P\<^esub> ?r" ?k], intro conjI)
- show "lcoeff g (^) ?k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> ?r" using exist by simp
- show "\<ominus>\<^bsub>P\<^esub> ?r = \<zero>\<^bsub>P\<^esub> \<or> deg R (\<ominus>\<^bsub>P\<^esub> ?r) < deg R g" using True by simp
- qed (simp_all)
- }
- next
- case False note n_deg_r_l_deg_g = False
- {
- (*JE: otherwise, we verify the conditions of the induction hypothesis.*)
- show ?thesis
- proof (cases "deg R f = 0")
- (*JE: the solutions are different if the degree of f is zero or not*)
- case True
- {
- have deg_g: "deg R g = 0" using True using deg_g_le_deg_f by simp
- have "lcoeff g (^) (1::nat) \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> f \<oplus>\<^bsub>P\<^esub> \<zero>\<^bsub>P\<^esub>"
- unfolding deg_g apply simp
- unfolding sym [OF monom_mult_is_smult [OF coeff_closed [OF g_in_P, of 0] f_in_P]]
- using deg_zero_impl_monom [OF g_in_P deg_g] by simp
- then show ?thesis using f_in_P by blast
- }
- next
- case False note deg_f_nzero = False
- {
- (*JE: now it only remains the case where the induction hypothesis can be used.*)
- (*JE: we first prove that the degree of the remainder is smaller than the one of f*)
- have deg_remainder_l_f: "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < deg R f"
- proof -
- have "deg R (\<ominus>\<^bsub>P\<^esub> ?r) = deg R ?r" using deg_uminus [of ?r] by simp
- also have "\<dots> < deg R f"
- proof (rule deg_lcoeff_cancel)
- show "deg R (\<ominus>\<^bsub>P\<^esub> (lcoeff g \<odot>\<^bsub>P\<^esub> f)) \<le> deg R f"
- using deg_smult_ring [of "lcoeff g" f]
- using lcoeff_nonzero2 [OF g_in_P g_not_zero] by simp
- show "deg R (g \<otimes>\<^bsub>P\<^esub> ?q) \<le> deg R f"
- using monom_deg_mult [OF _ g_in_P, of f "lcoeff f"] and deg_g_le_deg_f
- by simp
- show "coeff P (g \<otimes>\<^bsub>P\<^esub> ?q) (deg R f) = \<ominus> coeff P (\<ominus>\<^bsub>P\<^esub> (lcoeff g \<odot>\<^bsub>P\<^esub> f)) (deg R f)"
- unfolding coeff_mult [OF g_in_P monom_closed [OF lcoeff_closed [OF f_in_P], of "deg R f - deg R g"], of "deg R f"]
- unfolding coeff_monom [OF lcoeff_closed [OF f_in_P], of "(deg R f - deg R g)"]
- using R.finsum_cong' [of "{..deg R f}" "{..deg R f}"
- "(\<lambda>i. coeff P g i \<otimes> (if deg R f - deg R g = deg R f - i then lcoeff f else \<zero>))"
- "(\<lambda>i. if deg R g = i then coeff P g i \<otimes> lcoeff f else \<zero>)"]
- using R.finsum_singleton [of "deg R g" "{.. deg R f}" "(\<lambda>i. coeff P g i \<otimes> lcoeff f)"]
- unfolding Pi_def using deg_g_le_deg_f by force
- qed (simp_all add: deg_f_nzero)
- finally show "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < deg R f" .
- qed
- moreover have "\<ominus>\<^bsub>P\<^esub> ?r \<in> carrier P" by simp
- moreover obtain m where deg_rem_eq_m: "deg R (\<ominus>\<^bsub>P\<^esub> ?r) = m" by auto
- moreover have "deg R g \<le> deg R (\<ominus>\<^bsub>P\<^esub> ?r)" using n_deg_r_l_deg_g by simp
- (*JE: now, by applying the induction hypothesis, we obtain new quotient, remainder and exponent.*)
- ultimately obtain q' r' k'
- where rem_desc: "lcoeff g (^) (k'::nat) \<odot>\<^bsub>P\<^esub> (\<ominus>\<^bsub>P\<^esub> ?r) = g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r'"and rem_deg: "(r' = \<zero>\<^bsub>P\<^esub> \<or> deg R r' < deg R g)"
- and q'_in_carrier: "q' \<in> carrier P" and r'_in_carrier: "r' \<in> carrier P"
- using less by blast
- (*JE: we now prove that the new quotient, remainder and exponent can be used to get
- the quotient, remainder and exponent of the long division theorem*)
- show ?thesis
- proof (rule exI3 [of _ "((lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q')" r' "Suc k'"], intro conjI)
- show "(lcoeff g (^) (Suc k')) \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> ((lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q') \<oplus>\<^bsub>P\<^esub> r'"
- proof -
- have "(lcoeff g (^) (Suc k')) \<odot>\<^bsub>P\<^esub> f = (lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> ?r)"
- using smult_assoc1 exist by simp
- also have "\<dots> = (lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q) \<oplus>\<^bsub>P\<^esub> ((lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> ( \<ominus>\<^bsub>P\<^esub> ?r))"
- using UP_smult_r_distr by simp
- also have "\<dots> = (lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q) \<oplus>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r')"
- using rem_desc by simp
- also have "\<dots> = (lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q) \<oplus>\<^bsub>P\<^esub> g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r'"
- using sym [OF a_assoc [of "lcoeff g (^) k' \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q)" "g \<otimes>\<^bsub>P\<^esub> q'" "r'"]]
- using q'_in_carrier r'_in_carrier by simp
- also have "\<dots> = (lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> (?q \<otimes>\<^bsub>P\<^esub> g) \<oplus>\<^bsub>P\<^esub> q' \<otimes>\<^bsub>P\<^esub> g \<oplus>\<^bsub>P\<^esub> r'"
- using q'_in_carrier by (auto simp add: m_comm)
- also have "\<dots> = (((lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> ?q) \<otimes>\<^bsub>P\<^esub> g) \<oplus>\<^bsub>P\<^esub> q' \<otimes>\<^bsub>P\<^esub> g \<oplus>\<^bsub>P\<^esub> r'"
- using smult_assoc2 q'_in_carrier by auto
- also have "\<dots> = ((lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q') \<otimes>\<^bsub>P\<^esub> g \<oplus>\<^bsub>P\<^esub> r'"
- using sym [OF l_distr] and q'_in_carrier by auto
- finally show ?thesis using m_comm q'_in_carrier by auto
- qed
- qed (simp_all add: rem_deg q'_in_carrier r'_in_carrier)
- }
- qed
- }
- qed
- qed
+ proof (rule exI3 [of _ "((?lg (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q')" r' "Suc k'"], intro conjI)
+ show "(?lg (^) (Suc k')) \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> ((?lg (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q') \<oplus>\<^bsub>P\<^esub> r'"
+ proof -
+ have "(?lg (^) (Suc k')) \<odot>\<^bsub>P\<^esub> f = (?lg (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> ?f1)"
+ using smult_assoc1 [OF _ _ f_in_P] using exist by simp
+ also have "\<dots> = (?lg (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q) \<oplus>\<^bsub>P\<^esub> ((?lg (^) k') \<odot>\<^bsub>P\<^esub> ( \<ominus>\<^bsub>P\<^esub> ?f1))"
+ using UP_smult_r_distr by simp
+ also have "\<dots> = (?lg (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q) \<oplus>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r')"
+ unfolding rem_desc ..
+ also have "\<dots> = (?lg (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q) \<oplus>\<^bsub>P\<^esub> g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r'"
+ using sym [OF a_assoc [of "?lg (^) k' \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q)" "g \<otimes>\<^bsub>P\<^esub> q'" "r'"]]
+ using r'_in_carrier q'_in_carrier by simp
+ also have "\<dots> = (?lg (^) k') \<odot>\<^bsub>P\<^esub> (?q \<otimes>\<^bsub>P\<^esub> g) \<oplus>\<^bsub>P\<^esub> q' \<otimes>\<^bsub>P\<^esub> g \<oplus>\<^bsub>P\<^esub> r'"
+ using q'_in_carrier by (auto simp add: m_comm)
+ also have "\<dots> = (((?lg (^) k') \<odot>\<^bsub>P\<^esub> ?q) \<otimes>\<^bsub>P\<^esub> g) \<oplus>\<^bsub>P\<^esub> q' \<otimes>\<^bsub>P\<^esub> g \<oplus>\<^bsub>P\<^esub> r'"
+ using smult_assoc2 q'_in_carrier "1.prems" by auto
+ also have "\<dots> = ((?lg (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q') \<otimes>\<^bsub>P\<^esub> g \<oplus>\<^bsub>P\<^esub> r'"
+ using sym [OF l_distr] and q'_in_carrier by auto
+ finally show ?thesis using m_comm q'_in_carrier by auto
+ qed
+ qed (simp_all add: rem_deg q'_in_carrier r'_in_carrier)
+ }
qed
}
qed
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Aug 04 10:51:04 2010 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Aug 04 10:52:29 2010 +0200
@@ -5,8 +5,8 @@
header{* A formalization of Ferrante and Rackoff's procedure with polynomial parameters, see Paper in CALCULEMUS 2008 *}
theory Parametric_Ferrante_Rackoff
-imports Reflected_Multivariate_Polynomial
- "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
+imports Reflected_Multivariate_Polynomial
+ Dense_Linear_Order
Efficient_Nat
begin
--- a/src/HOL/IsaMakefile Wed Aug 04 10:51:04 2010 +0200
+++ b/src/HOL/IsaMakefile Wed Aug 04 10:52:29 2010 +0200
@@ -395,16 +395,16 @@
HOL-Library: HOL $(OUT)/HOL-Library
-$(OUT)/HOL-Library: $(OUT)/HOL Library/HOL_Library_ROOT.ML \
+$(OUT)/HOL-Library: $(OUT)/HOL Library/ROOT.ML \
$(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML \
Library/Abstract_Rat.thy $(SRC)/Tools/Adhoc_Overloading.thy \
- Library/AssocList.thy Library/BigO.thy Library/Binomial.thy \
+ Library/AssocList.thy Library/BigO.thy Library/Binomial.thy \
Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy \
Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy \
- Library/Code_Integer.thy Library/Code_Natural.thy \
+ Library/Code_Integer.thy Library/Code_Natural.thy \
Library/Code_Prolog.thy Tools/Predicate_Compile/code_prolog.ML \
Library/ContNotDenum.thy Library/Continuity.thy Library/Convex.thy \
- Library/Countable.thy Library/Diagonalize.thy Library/Dlist.thy \
+ Library/Countable.thy Library/Diagonalize.thy Library/Dlist.thy \
Library/Efficient_Nat.thy Library/Enum.thy Library/Eval_Witness.thy \
Library/Executable_Set.thy Library/Float.thy \
Library/Formal_Power_Series.thy Library/Fraction_Field.thy \
@@ -417,15 +417,14 @@
Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy \
Library/Monad_Syntax.thy Library/More_List.thy Library/More_Set.thy \
Library/Multiset.thy Library/Nat_Bijection.thy \
- Library/Nat_Infinity.thy \
- Library/Nested_Environment.thy Library/Numeral_Type.thy \
- Library/OptionalSugar.thy Library/Order_Relation.thy \
- Library/Permutation.thy Library/Permutations.thy \
- Library/Poly_Deriv.thy Library/Polynomial.thy \
- Library/Predicate_Compile_Quickcheck.thy Library/Preorder.thy \
- Library/Product_Vector.thy Library/Product_ord.thy \
- Library/Product_plus.thy Library/Quickcheck_Types.thy \
- Library/Quicksort.thy \
+ Library/Nat_Infinity.thy Library/Nested_Environment.thy \
+ Library/Numeral_Type.thy Library/OptionalSugar.thy \
+ Library/Order_Relation.thy Library/Permutation.thy \
+ Library/Permutations.thy Library/Poly_Deriv.thy \
+ Library/Polynomial.thy Library/Predicate_Compile_Quickcheck.thy \
+ Library/Preorder.thy Library/Product_Vector.thy \
+ Library/Product_ord.thy Library/Product_plus.thy \
+ Library/Quickcheck_Types.thy Library/Quicksort.thy \
Library/Quotient_List.thy Library/Quotient_Option.thy \
Library/Quotient_Product.thy Library/Quotient_Sum.thy \
Library/Quotient_Syntax.thy Library/Quotient_Type.thy \
@@ -440,7 +439,7 @@
$(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML \
Library/reflection.ML Library/reify_data.ML \
Library/document/root.bib Library/document/root.tex
- @cd Library; $(ISABELLE_TOOL) usedir -b -f HOL_Library_ROOT.ML $(OUT)/HOL HOL-Library
+ @cd Library; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL-Library
## HOL-Hahn_Banach
--- a/src/HOL/Library/HOL_Library_ROOT.ML Wed Aug 04 10:51:04 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,5 +0,0 @@
-
-(* Classical Higher-order Logic -- batteries included *)
-
-use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order",
- "Code_Char_chr", "Code_Integer", "Efficient_Nat", "Executable_Set", "Code_Prolog"];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/ROOT.ML Wed Aug 04 10:52:29 2010 +0200
@@ -0,0 +1,5 @@
+
+(* Classical Higher-order Logic -- batteries included *)
+
+use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order",
+ "Code_Char_chr", "Code_Integer", "Efficient_Nat", "Executable_Set", "Code_Prolog"];
--- a/src/HOL/Library/Sum_Of_Squares.thy Wed Aug 04 10:51:04 2010 +0200
+++ b/src/HOL/Library/Sum_Of_Squares.thy Wed Aug 04 10:52:29 2010 +0200
@@ -7,9 +7,9 @@
multiplication and ordering using semidefinite programming *}
theory Sum_Of_Squares
-imports Complex_Main (* "~~/src/HOL/Decision_Procs/Dense_Linear_Order" *)
+imports Complex_Main
uses
- "positivstellensatz.ML" (* duplicate use!? -- cf. Euclidian_Space.thy *)
+ "positivstellensatz.ML"
"Sum_Of_Squares/sum_of_squares.ML"
"Sum_Of_Squares/positivstellensatz_tools.ML"
"Sum_Of_Squares/sos_wrapper.ML"
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Aug 04 10:51:04 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Aug 04 10:52:29 2010 +0200
@@ -7,9 +7,10 @@
theory Euclidean_Space
imports
Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
- Infinite_Set
- Inner_Product L2_Norm Convex
-uses "positivstellensatz.ML" ("normarith.ML")
+ Infinite_Set Inner_Product L2_Norm Convex
+uses
+ "~~/src/HOL/Library/positivstellensatz.ML" (* FIXME duplicate use!? *)
+ ("normarith.ML")
begin
lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
--- a/src/HOL/Predicate_Compile_Examples/ROOT.ML Wed Aug 04 10:51:04 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML Wed Aug 04 10:52:29 2010 +0200
@@ -1,2 +1,2 @@
use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples", "Specialisation_Examples"];
-use_thys ["Code_Prolog_Examples"];
+if getenv "PROLOG_HOME" = "" then () else use_thys ["Code_Prolog_Examples"];
--- a/src/HOL/Subst/AList.thy Wed Aug 04 10:51:04 2010 +0200
+++ b/src/HOL/Subst/AList.thy Wed Aug 04 10:52:29 2010 +0200
@@ -1,28 +1,26 @@
-(* ID: $Id$
+(* Title: HOL/Subst/AList.thy
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-
*)
-header{*Association Lists*}
+header {* Association Lists *}
theory AList
imports Main
begin
-consts alist_rec :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
-primrec
+primrec alist_rec :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
+where
"alist_rec [] c d = c"
- "alist_rec (p # al) c d = d (fst p) (snd p) al (alist_rec al c d)"
+| "alist_rec (p # al) c d = d (fst p) (snd p) al (alist_rec al c d)"
-consts assoc :: "['a,'b,('a*'b) list] => 'b"
-primrec
+primrec assoc :: "['a,'b,('a*'b) list] => 'b"
+where
"assoc v d [] = d"
- "assoc v d (p # al) = (if v = fst p then snd p else assoc v d al)"
+| "assoc v d (p # al) = (if v = fst p then snd p else assoc v d al)"
lemma alist_induct:
- "[| P([]);
- !!x y xs. P(xs) ==> P((x,y)#xs) |] ==> P(l)"
+ "P [] \<Longrightarrow> (!!x y xs. P xs \<Longrightarrow> P ((x,y) # xs)) \<Longrightarrow> P l"
by (induct l) auto
end
--- a/src/HOL/Subst/Subst.thy Wed Aug 04 10:51:04 2010 +0200
+++ b/src/HOL/Subst/Subst.thy Wed Aug 04 10:52:29 2010 +0200
@@ -1,34 +1,36 @@
-(* Title: Subst/Subst.thy
- ID: $Id$
+(* Title: HOL/Subst/Subst.thy
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
*)
-header{*Substitutions on uterms*}
+header {* Substitutions on uterms *}
theory Subst
imports AList UTerm
begin
-consts
+primrec
subst :: "'a uterm => ('a * 'a uterm) list => 'a uterm" (infixl "<|" 55)
+where
+ subst_Var: "(Var v <| s) = assoc v (Var v) s"
+| subst_Const: "(Const c <| s) = Const c"
+| subst_Comb: "(Comb M N <| s) = Comb (M <| s) (N <| s)"
+
notation (xsymbols)
subst (infixl "\<lhd>" 55)
-primrec
- subst_Var: "(Var v \<lhd> s) = assoc v (Var v) s"
- subst_Const: "(Const c \<lhd> s) = Const c"
- subst_Comb: "(Comb M N \<lhd> s) = Comb (M \<lhd> s) (N \<lhd> s)"
definition
- subst_eq :: "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" (infixr "=$=" 52) where
- "r =$= s \<longleftrightarrow> (\<forall>t. t \<lhd> r = t \<lhd> s)"
+ subst_eq :: "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" (infixr "=$=" 52)
+ where "r =$= s \<longleftrightarrow> (\<forall>t. t \<lhd> r = t \<lhd> s)"
+
notation (xsymbols)
subst_eq (infixr "\<doteq>" 52)
definition
- comp :: "[('a*('a uterm)) list, ('a*('a uterm)) list] => ('a*('a uterm)) list"
- (infixl "<>" 56) where
- "al <> bl = alist_rec al bl (%x y xs g. (x,y \<lhd> bl)#g)"
+ comp :: "('a * 'a uterm) list \<Rightarrow> ('a * 'a uterm) list \<Rightarrow> ('a* 'a uterm) list"
+ (infixl "<>" 56)
+ where "al <> bl = alist_rec al bl (%x y xs g. (x,y \<lhd> bl) # g)"
+
notation (xsymbols)
comp (infixl "\<lozenge>" 56)
@@ -42,7 +44,7 @@
-subsection{*Basic Laws*}
+subsection {* Basic Laws *}
lemma subst_Nil [simp]: "t \<lhd> [] = t"
by (induct t) auto
@@ -54,9 +56,8 @@
apply (case_tac "t = Var v")
prefer 2
apply (erule rev_mp)+
- apply (rule_tac P =
- "%x. x \<noteq> Var v --> ~(Var v \<prec> x) --> x \<lhd> (v,t\<lhd>s) #s = x\<lhd>s"
- in uterm.induct)
+ apply (rule_tac P = "%x. x \<noteq> Var v \<longrightarrow> ~(Var v \<prec> x) \<longrightarrow> x \<lhd> (v,t\<lhd>s) #s = x\<lhd>s"
+ in uterm.induct)
apply auto
done
--- a/src/HOL/Subst/UTerm.thy Wed Aug 04 10:51:04 2010 +0200
+++ b/src/HOL/Subst/UTerm.thy Wed Aug 04 10:52:29 2010 +0200
@@ -1,52 +1,52 @@
-(* ID: $Id$
+(* Title: HOL/Subst/UTerm.thy
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
*)
-header{*Simple Term Structure for Unification*}
+header {* Simple Term Structure for Unification *}
theory UTerm
imports Main
begin
-text{*Binary trees with leaves that are constants or variables.*}
+text {* Binary trees with leaves that are constants or variables. *}
datatype 'a uterm =
Var 'a
| Const 'a
| Comb "'a uterm" "'a uterm"
-consts vars_of :: "'a uterm => 'a set"
-primrec
+primrec vars_of :: "'a uterm => 'a set"
+where
vars_of_Var: "vars_of (Var v) = {v}"
- vars_of_Const: "vars_of (Const c) = {}"
- vars_of_Comb: "vars_of (Comb M N) = (vars_of(M) Un vars_of(N))"
+| vars_of_Const: "vars_of (Const c) = {}"
+| vars_of_Comb: "vars_of (Comb M N) = (vars_of(M) Un vars_of(N))"
-consts occs :: "'a uterm => 'a uterm => bool" (infixl "<:" 54)
+primrec occs :: "'a uterm => 'a uterm => bool" (infixl "<:" 54)
+where
+ occs_Var: "u <: (Var v) = False"
+| occs_Const: "u <: (Const c) = False"
+| occs_Comb: "u <: (Comb M N) = (u = M | u = N | u <: M | u <: N)"
+
notation (xsymbols)
occs (infixl "\<prec>" 54)
-primrec
- occs_Var: "u \<prec> (Var v) = False"
- occs_Const: "u \<prec> (Const c) = False"
- occs_Comb: "u \<prec> (Comb M N) = (u=M | u=N | u \<prec> M | u \<prec> N)"
-consts
- uterm_size :: "'a uterm => nat"
-primrec
- uterm_size_Var: "uterm_size (Var v) = 0"
- uterm_size_Const: "uterm_size (Const c) = 0"
- uterm_size_Comb: "uterm_size (Comb M N) = Suc(uterm_size M + uterm_size N)"
+primrec uterm_size :: "'a uterm => nat"
+where
+ uterm_size_Var: "uterm_size (Var v) = 0"
+| uterm_size_Const: "uterm_size (Const c) = 0"
+| uterm_size_Comb: "uterm_size (Comb M N) = Suc(uterm_size M + uterm_size N)"
-lemma vars_var_iff: "(v \<in> vars_of(Var(w))) = (w=v)"
+lemma vars_var_iff: "(v \<in> vars_of (Var w)) = (w = v)"
by auto
-lemma vars_iff_occseq: "(x \<in> vars_of(t)) = (Var(x) \<prec> t | Var(x) = t)"
+lemma vars_iff_occseq: "(x \<in> vars_of t) = (Var x \<prec> t | Var x = t)"
by (induct t) auto
text{* Not used, but perhaps useful in other proofs *}
-lemma occs_vars_subset: "M\<prec>N \<Longrightarrow> vars_of(M) \<subseteq> vars_of(N)"
+lemma occs_vars_subset: "M \<prec> N \<Longrightarrow> vars_of M \<subseteq> vars_of N"
by (induct N) auto
@@ -54,7 +54,7 @@
"vars_of M Un vars_of N \<subseteq> (vars_of M Un A) Un (vars_of N Un B)"
by blast
-lemma finite_vars_of: "finite(vars_of M)"
+lemma finite_vars_of: "finite (vars_of M)"
by (induct M) auto
end
--- a/src/HOL/Subst/Unifier.thy Wed Aug 04 10:51:04 2010 +0200
+++ b/src/HOL/Subst/Unifier.thy Wed Aug 04 10:52:29 2010 +0200
@@ -1,26 +1,26 @@
-(* ID: $Id$
+(* Title: HOL/Subst/Unifier.thy
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
*)
-header{*Definition of Most General Unifier*}
+header {* Definition of Most General Unifier *}
theory Unifier
imports Subst
begin
definition
- Unifier :: "[('a * 'a uterm)list, 'a uterm, 'a uterm] => bool" where
- "Unifier s t u \<longleftrightarrow> t <| s = u <| s"
+ Unifier :: "('a * 'a uterm) list \<Rightarrow> 'a uterm \<Rightarrow> 'a uterm \<Rightarrow> bool"
+ where "Unifier s t u \<longleftrightarrow> t <| s = u <| s"
definition
- MoreGeneral :: "[('a * 'a uterm)list, ('a * 'a uterm)list] => bool" (infixr ">>" 52) where
- "r >> s \<longleftrightarrow> (\<exists>q. s =$= r <> q)"
+ MoreGeneral :: "('a * 'a uterm) list \<Rightarrow> ('a * 'a uterm) list \<Rightarrow> bool" (infixr ">>" 52)
+ where "r >> s \<longleftrightarrow> (\<exists>q. s =$= r <> q)"
definition
- MGUnifier :: "[('a * 'a uterm)list, 'a uterm, 'a uterm] => bool" where
- "MGUnifier s t u \<longleftrightarrow> Unifier s t u & (\<forall>r. Unifier r t u --> s >> r)"
+ MGUnifier :: "('a * 'a uterm) list \<Rightarrow> 'a uterm \<Rightarrow> 'a uterm \<Rightarrow> bool"
+ where "MGUnifier s t u \<longleftrightarrow> Unifier s t u & (\<forall>r. Unifier r t u --> s >> r)"
definition
Idem :: "('a * 'a uterm)list => bool" where
@@ -30,17 +30,17 @@
lemmas unify_defs = Unifier_def MoreGeneral_def MGUnifier_def
-subsection{*Unifiers*}
+subsection {* Unifiers *}
lemma Unifier_Comb [iff]: "Unifier s (Comb t u) (Comb v w) = (Unifier s t v & Unifier s u w)"
by (simp add: Unifier_def)
-lemma Cons_Unifier: "[| v ~: vars_of t; v ~: vars_of u; Unifier s t u |] ==> Unifier ((v,r)#s) t u"
+lemma Cons_Unifier: "v \<notin> vars_of t \<Longrightarrow> v \<notin> vars_of u \<Longrightarrow> Unifier s t u \<Longrightarrow> Unifier ((v, r) #s) t u"
by (simp add: Unifier_def repl_invariance)
-subsection{* Most General Unifiers*}
+subsection {* Most General Unifiers *}
lemma mgu_sym: "MGUnifier s t u = MGUnifier s u t"
by (simp add: unify_defs eq_commute)
@@ -64,26 +64,26 @@
done
-subsection{*Idempotence*}
+subsection {* Idempotence *}
-lemma Idem_Nil [iff]: "Idem([])"
+lemma Idem_Nil [iff]: "Idem []"
by (simp add: Idem_def)
-lemma Idem_iff: "Idem(s) = (sdom(s) Int srange(s) = {})"
+lemma Idem_iff: "Idem s = (sdom s Int srange s = {})"
by (simp add: Idem_def subst_eq_iff invariance dom_range_disjoint)
-lemma Var_Idem [intro!]: "~ (Var(v) <: t) ==> Idem([(v,t)])"
+lemma Var_Idem [intro!]: "~ (Var v <: t) ==> Idem [(v,t)]"
by (simp add: vars_iff_occseq Idem_iff srange_iff empty_iff_all_not)
lemma Unifier_Idem_subst:
- "[| Idem(r); Unifier s (t<|r) (u<|r) |]
- ==> Unifier (r <> s) (t <| r) (u <| r)"
+ "Idem(r) \<Longrightarrow> Unifier s (t<|r) (u<|r) \<Longrightarrow>
+ Unifier (r <> s) (t <| r) (u <| r)"
by (simp add: Idem_def Unifier_def comp_subst_subst)
lemma Idem_comp:
- "[| Idem(r); Unifier s (t <| r) (u <| r);
- !!q. Unifier q (t <| r) (u <| r) ==> s <> q =$= q
- |] ==> Idem(r <> s)"
+ "Idem r \<Longrightarrow> Unifier s (t <| r) (u <| r) \<Longrightarrow>
+ (!!q. Unifier q (t <| r) (u <| r) \<Longrightarrow> s <> q =$= q) \<Longrightarrow>
+ Idem (r <> s)"
apply (frule Unifier_Idem_subst, blast)
apply (force simp add: Idem_def subst_eq_iff)
done
--- a/src/HOL/Subst/Unify.thy Wed Aug 04 10:51:04 2010 +0200
+++ b/src/HOL/Subst/Unify.thy Wed Aug 04 10:52:29 2010 +0200
@@ -1,10 +1,9 @@
-(* ID: $Id$
+(* Title: HOL/Subst/Unify.thy
Author: Konrad Slind, Cambridge University Computer Laboratory
Copyright 1997 University of Cambridge
-
*)
-header{*Unification Algorithm*}
+header {* Unification Algorithm *}
theory Unify
imports Unifier
@@ -27,7 +26,7 @@
*}
definition
- unifyRel :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set" where
+ unifyRel :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set" where
"unifyRel = inv_image (finite_psubset <*lex*> measure uterm_size)
(%(M,N). (vars_of M Un vars_of N, M))"
--{*Termination relation for the Unify function:
--- a/src/HOLCF/IsaMakefile Wed Aug 04 10:51:04 2010 +0200
+++ b/src/HOLCF/IsaMakefile Wed Aug 04 10:52:29 2010 +0200
@@ -107,8 +107,8 @@
Library/Strict_Fun.thy \
Library/Sum_Cpo.thy \
Library/HOLCF_Library.thy \
- Library/HOLCF_Library_ROOT.ML
- @$(ISABELLE_TOOL) usedir -f HOLCF_Library_ROOT.ML $(OUT)/HOLCF Library
+ Library/ROOT.ML
+ @$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Library
## HOLCF-IMP
--- a/src/HOLCF/Library/HOLCF_Library_ROOT.ML Wed Aug 04 10:51:04 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-use_thys ["HOLCF_Library"];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Library/ROOT.ML Wed Aug 04 10:52:29 2010 +0200
@@ -0,0 +1,1 @@
+use_thys ["HOLCF_Library"];
--- a/src/Pure/Isar/isar_cmd.ML Wed Aug 04 10:51:04 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Wed Aug 04 10:52:29 2010 +0200
@@ -391,7 +391,7 @@
val thy = Toplevel.theory_of state;
val thy_session = Present.session_name thy;
- val all_thys = sort Thy_Info.thy_ord (thy :: Theory.ancestors_of thy);
+ val all_thys = rev (thy :: Theory.ancestors_of thy);
val gr = all_thys |> map (fn node =>
let
val name = Context.theory_name node;
--- a/src/Pure/ProofGeneral/pgip_isabelle.ML Wed Aug 04 10:51:04 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_isabelle.ML Wed Aug 04 10:52:29 2010 +0200
@@ -80,9 +80,9 @@
NONE => (NONE, NONE)
| SOME fname =>
let val path = Path.explode fname in
- case Thy_Load.test_file Path.current path of
- SOME _ => (SOME (PgipTypes.pgipurl_of_path path), NONE)
- | NONE => (NONE, SOME fname)
+ if can (Thy_Load.check_file [Path.current]) path
+ then (SOME (PgipTypes.pgipurl_of_path path), NONE)
+ else (NONE, SOME fname)
end);
in
{ descr=descr, url=url, line=line, column=column, char=NONE, length=NONE }
--- a/src/Pure/System/isar.ML Wed Aug 04 10:51:04 2010 +0200
+++ b/src/Pure/System/isar.ML Wed Aug 04 10:52:29 2010 +0200
@@ -68,8 +68,7 @@
fun find_and_undo _ [] = error "Undo history exhausted"
| find_and_undo which ((prev, tr) :: hist) =
- ((case Toplevel.init_of tr of SOME name => Thy_Info.kill_thy name | NONE => ());
- if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist);
+ if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist;
in
--- a/src/Pure/Thy/present.ML Wed Aug 04 10:51:04 2010 +0200
+++ b/src/Pure/Thy/present.ML Wed Aug 04 10:52:29 2010 +0200
@@ -462,7 +462,7 @@
val files_html = files |> map (fn (raw_path, loadit) =>
let
- val path = #1 (Thy_Load.check_file dir raw_path);
+ val path = #1 (Thy_Load.check_file [dir] raw_path);
val base = Path.base path;
val base_html = html_ext base;
val _ = add_file (Path.append html_prefix base_html,
--- a/src/Pure/Thy/thy_info.ML Wed Aug 04 10:51:04 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML Wed Aug 04 10:52:29 2010 +0200
@@ -15,7 +15,6 @@
val is_finished: string -> bool
val master_directory: string -> Path.T
val loaded_files: string -> Path.T list
- val thy_ord: theory * theory -> order
val remove_thy: string -> unit
val kill_thy: string -> unit
val use_thys: string list -> unit
@@ -144,8 +143,6 @@
fun merge _ = empty;
);
-val thy_ord = int_ord o pairself Update_Time.get;
-
(* remove theory *)
@@ -238,12 +235,13 @@
fun required_by _ [] = ""
| required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
-fun load_thy initiators update_time (deps: deps) text dir name parent_thys =
+fun load_thy initiators update_time (deps: deps) text name parent_thys =
let
val _ = kill_thy name;
val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators);
val {master = (thy_path, _), ...} = deps;
+ val dir = Path.dir thy_path;
val pos = Path.position thy_path;
val uses = map (apfst Path.explode) (#3 (Thy_Header.read pos text));
fun init () =
@@ -317,7 +315,7 @@
let
val text = (case opt_text of SOME text => text | NONE => File.read thy_path);
val update_time = serial ();
- in Task (parent_names, load_thy initiators update_time dep text dir' name) end);
+ in Task (parent_names, load_thy initiators update_time dep text name) end);
in (all_current, new_entry name parent_names task tasks') end)
end;
--- a/src/Pure/Thy/thy_load.ML Wed Aug 04 10:51:04 2010 +0200
+++ b/src/Pure/Thy/thy_load.ML Wed Aug 04 10:52:29 2010 +0200
@@ -22,8 +22,7 @@
val master_directory: theory -> Path.T
val require: Path.T -> theory -> theory
val provide: Path.T * (Path.T * File.ident) -> theory -> theory
- val test_file: Path.T -> Path.T -> (Path.T * File.ident) option
- val check_file: Path.T -> Path.T -> Path.T * File.ident
+ val check_file: Path.T list -> Path.T -> Path.T * File.ident
val check_thy: Path.T -> string -> Path.T * File.ident
val deps_thy: Path.T -> string ->
{master: Path.T * File.ident, text: string, imports: string list, uses: Path.T list}
@@ -110,45 +109,37 @@
(* check files *)
-local
-
-exception NOT_FOUND of Path.T list * Path.T;
-
-fun try_file dir src_path =
+fun get_file dirs src_path =
let
- val prfxs = search_path dir src_path;
val path = Path.expand src_path;
val _ = Path.is_current path andalso error "Bad file specification";
- val result =
- prfxs |> get_first (fn prfx =>
- let val full_path = File.full_path (Path.append prfx path)
- in Option.map (pair full_path) (File.ident full_path) end);
in
- (case result of
- SOME res => res
- | NONE => raise NOT_FOUND (prfxs, path))
+ dirs |> get_first (fn dir =>
+ let val full_path = File.full_path (Path.append dir path) in
+ (case File.ident full_path of
+ NONE => NONE
+ | SOME id => SOME (full_path, id))
+ end)
end;
-in
-
-fun test_file dir file =
- SOME (try_file dir file) handle NOT_FOUND _ => NONE;
+fun check_file dirs file =
+ (case get_file dirs file of
+ SOME path_id => path_id
+ | NONE => error ("Could not find file " ^ quote (Path.implode file) ^
+ "\nin " ^ commas_quote (map Path.implode dirs)));
-fun check_file dir file =
- try_file dir file handle NOT_FOUND (prfxs, path) =>
- error ("Could not find file " ^ quote (Path.implode path) ^
- "\nin " ^ commas_quote (map Path.implode prfxs));
-
-fun check_thy dir name = check_file dir (Thy_Header.thy_path name);
-
-end;
+fun check_thy master_dir name =
+ let
+ val thy_file = Thy_Header.thy_path name;
+ val dirs = search_path master_dir thy_file;
+ in check_file dirs thy_file end;
(* theory deps *)
-fun deps_thy dir name =
+fun deps_thy master_dir name =
let
- val master as (thy_path, _) = check_thy dir name;
+ val master as (thy_path, _) = check_thy master_dir name;
val text = File.read thy_path;
val (name', imports, uses) = Thy_Header.read (Path.position thy_path) text;
val _ = Thy_Header.consistent_name name name';
@@ -179,7 +170,7 @@
let
val {master_dir, provided, ...} = Files.get thy;
fun current (src_path, (_, id)) =
- (case test_file master_dir src_path of
+ (case get_file [master_dir] src_path of
NONE => false
| SOME (_, id') => id = id');
in can check_loaded thy andalso forall current provided end;
@@ -190,15 +181,15 @@
(* provide files *)
fun provide_file src_path thy =
- provide (src_path, check_file (master_directory thy) src_path) thy;
+ provide (src_path, check_file [master_directory thy] src_path) thy;
fun use_ml src_path =
if is_none (Context.thread_data ()) then
- ML_Context.eval_file (#1 (check_file Path.current src_path))
+ ML_Context.eval_file (#1 (check_file [Path.current] src_path))
else
let
val thy = ML_Context.the_global_context ();
- val (path, id) = check_file (master_directory thy) src_path;
+ val (path, id) = check_file [master_directory thy] src_path;
val _ = ML_Context.eval_file path;
val _ = Context.>> Local_Theory.propagate_ml_env;