--- a/Admin/Mercurial/cvsids Wed Mar 11 11:40:58 2009 +0100
+++ b/Admin/Mercurial/cvsids Wed Mar 11 11:41:14 2009 +0100
@@ -1,5 +1,6 @@
Identifiers of some old CVS file versions
=========================================
-src/Pure/type.ML 1.65 0d984ee030a1
+src/Pure/type.ML 1.65 0d984ee030a1
+src/Pure/General/file.ML 1.18 6cdd6a8da9b9
--- a/NEWS Wed Mar 11 11:40:58 2009 +0100
+++ b/NEWS Wed Mar 11 11:41:14 2009 +0100
@@ -244,7 +244,8 @@
* Theory HOL/Decisioin_Procs/Approximation.thy provides the new proof method
"approximation". It proves formulas on real values by using interval arithmetic.
In the formulas are also the transcendental functions sin, cos, tan, atan, ln,
-exp and the constant pi are allowed. For examples see HOL/ex/ApproximationEx.thy.
+exp and the constant pi are allowed. For examples see
+HOL/Descision_Procs/ex/Approximation_Ex.thy.
* Theory "Reflection" now resides in HOL/Library.
--- a/src/HOL/Code_Eval.thy Wed Mar 11 11:40:58 2009 +0100
+++ b/src/HOL/Code_Eval.thy Wed Mar 11 11:41:14 2009 +0100
@@ -134,6 +134,10 @@
lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
lemma [code, code del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" ..
+lemma [code, code del]:
+ "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
+lemma [code, code del]:
+ "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Eval.term_of c =
(let (n, m) = nibble_pair_of_char c
--- a/src/HOL/Decision_Procs/Approximation.thy Wed Mar 11 11:40:58 2009 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Wed Mar 11 11:41:14 2009 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Reflection/Approximation.thy
+(* Title: HOL/Decision_Procs/Approximation.thy
Author: Johannes Hoelzl <hoelzl@in.tum.de> 2008 / 2009
*)
--- a/src/HOL/Decision_Procs/Cooper.thy Wed Mar 11 11:40:58 2009 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy Wed Mar 11 11:41:14 2009 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Reflection/Cooper.thy
+(* Title: HOL/Decision_Procs/Cooper.thy
Author: Amine Chaieb
*)
--- a/src/HOL/Decision_Procs/Decision_Procs.thy Wed Mar 11 11:40:58 2009 +0100
+++ b/src/HOL/Decision_Procs/Decision_Procs.thy Wed Mar 11 11:41:14 2009 +0100
@@ -1,5 +1,7 @@
+header {* Various decision procedures. typically involving reflection *}
+
theory Decision_Procs
-imports Cooper Ferrack MIR Approximation Dense_Linear_Order
+imports Cooper Ferrack MIR Approximation Dense_Linear_Order "ex/Approximation_Ex" "ex/Dense_Linear_Order_Ex"
begin
end
\ No newline at end of file
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Mar 11 11:40:58 2009 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Mar 11 11:41:14 2009 +0100
@@ -1,4 +1,4 @@
-(* Title : HOL/Dense_Linear_Order.thy
+(* Title : HOL/Decision_Procs/Dense_Linear_Order.thy
Author : Amine Chaieb, TU Muenchen
*)
--- a/src/HOL/Decision_Procs/Ferrack.thy Wed Mar 11 11:40:58 2009 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy Wed Mar 11 11:41:14 2009 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Reflection/Ferrack.thy
+(* Title: HOL/Decision_Procs/Ferrack.thy
Author: Amine Chaieb
*)
--- a/src/HOL/Decision_Procs/MIR.thy Wed Mar 11 11:40:58 2009 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy Wed Mar 11 11:41:14 2009 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Reflection/MIR.thy
+(* Title: HOL/Decision_Procs/MIR.thy
Author: Amine Chaieb
*)
--- a/src/HOL/Decision_Procs/cooper_tac.ML Wed Mar 11 11:40:58 2009 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Wed Mar 11 11:41:14 2009 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Reflection/cooper_tac.ML
+(* Title: HOL/Decision_Procs/cooper_tac.ML
Author: Amine Chaieb, TU Muenchen
*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Wed Mar 11 11:41:14 2009 +0100
@@ -0,0 +1,52 @@
+(* Title: HOL/ex/ApproximationEx.thy
+ Author: Johannes Hoelzl <hoelzl@in.tum.de> 2009
+*)
+
+theory Approximation_Ex
+imports Complex_Main "~~/src/HOL/Decision_Procs/Approximation"
+begin
+
+text {*
+
+Here are some examples how to use the approximation method.
+
+The parameter passed to the method specifies the precision used by the computations, it is specified
+as number of bits to calculate. When a variable is used it needs to be bounded by an interval. This
+interval is specified as a conjunction of the lower and upper bound. It must have the form
+@{text "\<lbrakk> l\<^isub>1 \<le> x\<^isub>1 \<and> x\<^isub>1 \<le> u\<^isub>1 ; \<dots> ; l\<^isub>n \<le> x\<^isub>n \<and> x\<^isub>n \<le> u\<^isub>n \<rbrakk> \<Longrightarrow> F"} where @{term F} is the formula, and
+@{text "x\<^isub>1, \<dots>, x\<^isub>n"} are the variables. The lower bounds @{text "l\<^isub>1, \<dots>, l\<^isub>n"} and the upper bounds
+@{text "u\<^isub>1, \<dots>, u\<^isub>n"} must either be integer numerals, floating point numbers or of the form
+@{term "m * pow2 e"} to specify a exact floating point value.
+
+*}
+
+section "Compute some transcendental values"
+
+lemma "\<bar> ln 2 - 544531980202654583340825686620847 / 785593587443817081832229725798400 \<bar> < inverse (2^51) "
+ by (approximation 80)
+
+lemma "\<bar> exp 1.626 - 5.083499996273 \<bar> < (inverse 10 ^ 10 :: real)"
+ by (approximation 80)
+
+lemma "\<bar> sqrt 2 - 1.4142135623730951 \<bar> < inverse 10 ^ 16"
+ by (approximation 80)
+
+lemma "\<bar> pi - 3.1415926535897932385 \<bar> < inverse 10 ^ 18"
+ by (approximation 80)
+
+section "Use variable ranges"
+
+lemma "0.5 \<le> x \<and> x \<le> 4.5 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
+ by (approximation 10)
+
+lemma "0.49 \<le> x \<and> x \<le> 4.49 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
+ by (approximation 20)
+
+lemma "1 * pow2 -1 \<le> x \<and> x \<le> 9 * pow2 -1 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
+ by (approximation 10)
+
+lemma "0 \<le> x \<and> x \<le> 1 \<Longrightarrow> 0 \<le> sin x"
+ by (approximation 10)
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy Wed Mar 11 11:41:14 2009 +0100
@@ -0,0 +1,153 @@
+(* Author: Amine Chaieb, TU Muenchen *)
+
+header {* Examples for Ferrante and Rackoff's quantifier elimination procedure *}
+
+theory Dense_Linear_Order_Ex
+imports Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
+begin
+
+lemma
+ "\<exists>(y::'a::{ordered_field,recpower,number_ring, division_by_zero}) <2. x + 3* y < 0 \<and> x - y >0"
+ by ferrack
+
+lemma "~ (ALL x (y::'a::{ordered_field,recpower,number_ring, division_by_zero}). x < y --> 10*x < 11*y)"
+ by ferrack
+
+lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x < y --> (10*(x + 5*y + -1) < 60*y)"
+ by ferrack
+
+lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x ~= y --> x < y"
+ by ferrack
+
+lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y"
+ by ferrack
+
+lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y"
+ by ferrack
+
+lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX (y::'a::{ordered_field,recpower,number_ring, division_by_zero}). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)"
+ by ferrack
+
+lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) < 0. (EX (y::'a::{ordered_field,recpower,number_ring, division_by_zero}) > 0. 7*x + y > 0 & x - y <= 9)"
+ by ferrack
+
+lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)"
+ by ferrack
+
+lemma "EX x. (ALL (y::'a::{ordered_field,recpower,number_ring, division_by_zero}). y < 2 --> 2*(y - x) \<le> 0 )"
+ by ferrack
+
+lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)"
+ by ferrack
+
+lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. x + y < z --> y >= z --> x < 0"
+ by ferrack
+
+lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0"
+ by ferrack
+
+lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. abs (x + y) <= z --> (abs z = z)"
+ by ferrack
+
+lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0"
+ by ferrack
+
+lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. (abs (5*x+3*y+z) <= 5*x+3*y+z & abs (5*x+3*y+z) >= - (5*x+3*y+z)) | (abs (5*x+3*y+z) >= 5*x+3*y+z & abs (5*x+3*y+z) <= - (5*x+3*y+z))"
+ by ferrack
+
+lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)"
+ by ferrack
+
+lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)"
+ by ferrack
+
+lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX z>0. abs (x - y) <= z )"
+ by ferrack
+
+lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
+ by ferrack
+
+lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)"
+ by ferrack
+
+lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
+ by ferrack
+
+lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero})>0. (ALL y. (EX z. 13* abs z \<noteq> abs (12*y - x) & 5*x - 3*(abs y) <= 7*z))"
+ by ferrack
+
+lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). abs (4*x + 17) < 4 & (ALL y . abs (x*34 - 34*y - 9) \<noteq> 0 \<longrightarrow> (EX z. 5*x - 3*abs y <= 7*z))"
+ by ferrack
+
+lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y > abs (23*x - 9). (ALL z > abs (3*y - 19* abs x). x+z > 2*y))"
+ by ferrack
+
+lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y< abs (3*x - 1). (ALL z >= (3*abs x - 1). abs (12*x - 13*y + 19*z) > abs (23*x) ))"
+ by ferrack
+
+lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). abs x < 100 & (ALL y > x. (EX z<2*y - x. 5*x - 3*y <= 7*z))"
+ by ferrack
+
+lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. 7*x<3*y --> 5*y < 7*z --> z < 2*w --> 7*(2*w-x) > 2*y"
+ by ferrack
+
+lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89"
+ by ferrack
+
+lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. 5*x + 3*z - 17*w + 7* (y - 8*x + z) <= max y (7*z - x + w)"
+ by ferrack
+
+lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)"
+ by ferrack
+
+lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. (EX w >= (x+y+z). w <= abs x + abs y + abs z)"
+ by ferrack
+
+lemma "~(ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y z w. 3* x + z*4 = 3*y & x + y < z & x> w & 3*x < w + y))"
+ by ferrack
+
+lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX z w. abs (x-y) = (z-w) & z*1234 < 233*x & w ~= y)"
+ by ferrack
+
+lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w))"
+ by ferrack
+
+lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. (ALL w >= abs (x+y+z). w >= abs x + abs y + abs z)"
+ by ferrack
+
+lemma "EX z. (ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX w >= (x+y+z). w <= abs x + abs y + abs z))"
+ by ferrack
+
+lemma "EX z. (ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) < abs z. (EX y w. x< y & x < z & x> w & 3*x < w + y))"
+ by ferrack
+
+lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX z. (ALL w. abs (x-y) = abs (z-w) --> z < x & w ~= y))"
+ by ferrack
+
+lemma "EX y. (ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)))"
+ by ferrack
+
+lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) z. (ALL w >= 13*x - 4*z. (EX y. w >= abs x + abs y + z))"
+ by ferrack
+
+lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (ALL y < x. (EX z > (x+y).
+ (ALL w. 5*w + 10*x - z >= y --> w + 7*x + 3*z >= 2*y)))"
+ by ferrack
+
+lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (ALL y. (EX z > y.
+ (ALL w . w < 13 --> w + 10*x - z >= y --> 5*w + 7*x + 13*z >= 2*y)))"
+ by ferrack
+
+lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)"
+ by ferrack
+
+lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))"
+ by ferrack
+
+lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (x + z) < w - y)))"
+ by ferrack
+
+lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y. abs y ~= abs x & (ALL z> max x y. (EX w. w ~= y & w ~= z & 3*w - z >= x + y)))"
+ by ferrack
+
+end
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Wed Mar 11 11:40:58 2009 +0100
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Wed Mar 11 11:41:14 2009 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Reflection/ferrack_tac.ML
+(* Title: HOL/Decision_Procs/ferrack_tac.ML
Author: Amine Chaieb, TU Muenchen
*)
--- a/src/HOL/Decision_Procs/mir_tac.ML Wed Mar 11 11:40:58 2009 +0100
+++ b/src/HOL/Decision_Procs/mir_tac.ML Wed Mar 11 11:41:14 2009 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Reflection/mir_tac.ML
+(* Title: HOL/Decision_Procs/mir_tac.ML
Author: Amine Chaieb, TU Muenchen
*)
--- a/src/HOL/FunDef.thy Wed Mar 11 11:40:58 2009 +0100
+++ b/src/HOL/FunDef.thy Wed Mar 11 11:41:14 2009 +0100
@@ -225,10 +225,10 @@
subsection {* Concrete orders for SCNP termination proofs *}
definition "pair_less = less_than <*lex*> less_than"
-definition "pair_leq = pair_less^="
+definition [code del]: "pair_leq = pair_less^="
definition "max_strict = max_ext pair_less"
-definition "max_weak = max_ext pair_leq \<union> {({}, {})}"
-definition "min_strict = min_ext pair_less"
+definition [code del]: "max_weak = max_ext pair_leq \<union> {({}, {})}"
+definition [code del]: "min_strict = min_ext pair_less"
definition "min_weak = min_ext pair_leq \<union> {({}, {})}"
lemma wf_pair_less[simp]: "wf pair_less"
--- a/src/HOL/IsaMakefile Wed Mar 11 11:40:58 2009 +0100
+++ b/src/HOL/IsaMakefile Wed Mar 11 11:41:14 2009 +0100
@@ -680,6 +680,8 @@
Decision_Procs/MIR.thy \
Decision_Procs/mir_tac.ML \
Decision_Procs/Decision_Procs.thy \
+ Decision_Procs/ex/Dense_Linear_Order_Ex.thy \
+ Decision_Procs/ex/Approximation_Ex.thy \
Decision_Procs/ROOT.ML
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Decision_Procs
@@ -823,13 +825,13 @@
$(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy \
Library/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy \
- ex/ApproximationEx.thy ex/Arith_Examples.thy \
+ ex/Arith_Examples.thy \
ex/Arithmetic_Series_Complex.thy ex/BT.thy ex/BinEx.thy \
ex/Binary.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy \
ex/CodegenSML_Test.thy ex/Codegenerator.thy \
ex/Codegenerator_Pretty.thy ex/Coherent.thy \
ex/Commutative_RingEx.thy ex/Commutative_Ring_Complete.thy \
- ex/Dense_Linear_Order_Ex.thy ex/Efficient_Nat_examples.thy \
+ ex/Efficient_Nat_examples.thy \
ex/Eval_Examples.thy ex/ExecutableContent.thy \
ex/Formal_Power_Series_Examples.thy ex/Fundefs.thy \
ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \
--- a/src/HOL/Library/Multiset.thy Wed Mar 11 11:40:58 2009 +0100
+++ b/src/HOL/Library/Multiset.thy Wed Mar 11 11:41:14 2009 +0100
@@ -1487,7 +1487,7 @@
by auto
definition "ms_strict = mult pair_less"
-definition "ms_weak = ms_strict \<union> Id"
+definition [code del]: "ms_weak = ms_strict \<union> Id"
lemma ms_reduction_pair: "reduction_pair (ms_strict, ms_weak)"
unfolding reduction_pair_def ms_strict_def ms_weak_def pair_less_def
--- a/src/HOL/Predicate.thy Wed Mar 11 11:40:58 2009 +0100
+++ b/src/HOL/Predicate.thy Wed Mar 11 11:41:14 2009 +0100
@@ -588,7 +588,39 @@
by (simp add: adjunct_sup sup_assoc sup_commute sup_left_commute)
qed
-declare eq_pred_def [code, code del]
+primrec contained :: "'a seq \<Rightarrow> 'a pred \<Rightarrow> bool" where
+ "contained Empty Q \<longleftrightarrow> True"
+ | "contained (Insert x P) Q \<longleftrightarrow> eval Q x \<and> P \<le> Q"
+ | "contained (Join P xq) Q \<longleftrightarrow> P \<le> Q \<and> contained xq Q"
+
+lemma single_less_eq_eval:
+ "single x \<le> P \<longleftrightarrow> eval P x"
+ by (auto simp add: single_def less_eq_pred_def mem_def)
+
+lemma contained_less_eq:
+ "contained xq Q \<longleftrightarrow> pred_of_seq xq \<le> Q"
+ by (induct xq) (simp_all add: single_less_eq_eval)
+
+lemma less_eq_pred_code [code]:
+ "Seq f \<le> Q = (case f ()
+ of Empty \<Rightarrow> True
+ | Insert x P \<Rightarrow> eval Q x \<and> P \<le> Q
+ | Join P xq \<Rightarrow> P \<le> Q \<and> contained xq Q)"
+ by (cases "f ()")
+ (simp_all add: Seq_def single_less_eq_eval contained_less_eq)
+
+lemma eq_pred_code [code]:
+ fixes P Q :: "'a::eq pred"
+ shows "eq_class.eq P Q \<longleftrightarrow> P \<le> Q \<and> Q \<le> P"
+ unfolding eq by auto
+
+lemma [code]:
+ "pred_case f P = f (eval P)"
+ by (cases P) simp
+
+lemma [code]:
+ "pred_rec f P = f (eval P)"
+ by (cases P) simp
no_notation
inf (infixl "\<sqinter>" 70) and
@@ -601,6 +633,6 @@
hide (open) type pred seq
hide (open) const Pred eval single bind if_pred not_pred
- Empty Insert Join Seq member "apply" adjunct
+ Empty Insert Join Seq member pred_of_seq "apply" adjunct
end
--- a/src/HOL/Tools/datatype_package.ML Wed Mar 11 11:40:58 2009 +0100
+++ b/src/HOL/Tools/datatype_package.ML Wed Mar 11 11:41:14 2009 +0100
@@ -677,15 +677,14 @@
val thy = ProofContext.theory_of ctxt;
val (vs, cos) = the_datatype_spec thy dtco;
val ty = Type (dtco, map TFree vs);
- fun pretty_typ_br ty =
- let
- val p = Syntax.pretty_typ ctxt ty;
- val s = explode (Pretty.str_of p); (* FIXME do not inspect pretty output! *)
- in if member (op =) s " " then Pretty.enclose "(" ")" [p] else p end;
+ fun pretty_typ_bracket (ty as Type (_, _ :: _)) =
+ Pretty.enclose "(" ")" [Syntax.pretty_typ ctxt ty]
+ | pretty_typ_bracket ty =
+ Syntax.pretty_typ ctxt ty;
fun pretty_constr (co, tys) =
(Pretty.block o Pretty.breaks)
(Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
- map pretty_typ_br tys);
+ map pretty_typ_bracket tys);
val pretty_datatype =
Pretty.block
(Pretty.command "datatype" :: Pretty.brk 1 ::
--- a/src/HOL/Wellfounded.thy Wed Mar 11 11:40:58 2009 +0100
+++ b/src/HOL/Wellfounded.thy Wed Mar 11 11:41:14 2009 +0100
@@ -960,4 +960,10 @@
declare "prod.size" [noatp]
+lemma [code]:
+ "size (P :: 'a Predicate.pred) = 0" by (cases P) simp
+
+lemma [code]:
+ "pred_size f P = 0" by (cases P) simp
+
end
--- a/src/HOL/ex/ApproximationEx.thy Wed Mar 11 11:40:58 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,52 +0,0 @@
-(* Title: HOL/ex/ApproximationEx.thy
- Author: Johannes Hoelzl <hoelzl@in.tum.de> 2009
-*)
-
-theory ApproximationEx
-imports "~~/src/HOL/Decision_Procs/Approximation"
-begin
-
-text {*
-
-Here are some examples how to use the approximation method.
-
-The parameter passed to the method specifies the precision used by the computations, it is specified
-as number of bits to calculate. When a variable is used it needs to be bounded by an interval. This
-interval is specified as a conjunction of the lower and upper bound. It must have the form
-@{text "\<lbrakk> l\<^isub>1 \<le> x\<^isub>1 \<and> x\<^isub>1 \<le> u\<^isub>1 ; \<dots> ; l\<^isub>n \<le> x\<^isub>n \<and> x\<^isub>n \<le> u\<^isub>n \<rbrakk> \<Longrightarrow> F"} where @{term F} is the formula, and
-@{text "x\<^isub>1, \<dots>, x\<^isub>n"} are the variables. The lower bounds @{text "l\<^isub>1, \<dots>, l\<^isub>n"} and the upper bounds
-@{text "u\<^isub>1, \<dots>, u\<^isub>n"} must either be integer numerals, floating point numbers or of the form
-@{term "m * pow2 e"} to specify a exact floating point value.
-
-*}
-
-section "Compute some transcendental values"
-
-lemma "\<bar> ln 2 - 544531980202654583340825686620847 / 785593587443817081832229725798400 \<bar> < inverse (2^51) "
- by (approximation 80)
-
-lemma "\<bar> exp 1.626 - 5.083499996273 \<bar> < (inverse 10 ^ 10 :: real)"
- by (approximation 80)
-
-lemma "\<bar> sqrt 2 - 1.4142135623730951 \<bar> < inverse 10 ^ 16"
- by (approximation 80)
-
-lemma "\<bar> pi - 3.1415926535897932385 \<bar> < inverse 10 ^ 18"
- by (approximation 80)
-
-section "Use variable ranges"
-
-lemma "0.5 \<le> x \<and> x \<le> 4.5 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
- by (approximation 10)
-
-lemma "0.49 \<le> x \<and> x \<le> 4.49 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
- by (approximation 20)
-
-lemma "1 * pow2 -1 \<le> x \<and> x \<le> 9 * pow2 -1 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
- by (approximation 10)
-
-lemma "0 \<le> x \<and> x \<le> 1 \<Longrightarrow> 0 \<le> sin x"
- by (approximation 10)
-
-end
-
--- a/src/HOL/ex/Dense_Linear_Order_Ex.thy Wed Mar 11 11:40:58 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,153 +0,0 @@
-(* Author: Amine Chaieb, TU Muenchen *)
-
-header {* Examples for Ferrante and Rackoff's quantifier elimination procedure *}
-
-theory Dense_Linear_Order_Ex
-imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Main
-begin
-
-lemma
- "\<exists>(y::'a::{ordered_field,recpower,number_ring, division_by_zero}) <2. x + 3* y < 0 \<and> x - y >0"
- by ferrack
-
-lemma "~ (ALL x (y::'a::{ordered_field,recpower,number_ring, division_by_zero}). x < y --> 10*x < 11*y)"
- by ferrack
-
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x < y --> (10*(x + 5*y + -1) < 60*y)"
- by ferrack
-
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x ~= y --> x < y"
- by ferrack
-
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y"
- by ferrack
-
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y"
- by ferrack
-
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX (y::'a::{ordered_field,recpower,number_ring, division_by_zero}). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)"
- by ferrack
-
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) < 0. (EX (y::'a::{ordered_field,recpower,number_ring, division_by_zero}) > 0. 7*x + y > 0 & x - y <= 9)"
- by ferrack
-
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)"
- by ferrack
-
-lemma "EX x. (ALL (y::'a::{ordered_field,recpower,number_ring, division_by_zero}). y < 2 --> 2*(y - x) \<le> 0 )"
- by ferrack
-
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)"
- by ferrack
-
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. x + y < z --> y >= z --> x < 0"
- by ferrack
-
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0"
- by ferrack
-
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. abs (x + y) <= z --> (abs z = z)"
- by ferrack
-
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0"
- by ferrack
-
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. (abs (5*x+3*y+z) <= 5*x+3*y+z & abs (5*x+3*y+z) >= - (5*x+3*y+z)) | (abs (5*x+3*y+z) >= 5*x+3*y+z & abs (5*x+3*y+z) <= - (5*x+3*y+z))"
- by ferrack
-
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)"
- by ferrack
-
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)"
- by ferrack
-
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX z>0. abs (x - y) <= z )"
- by ferrack
-
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
- by ferrack
-
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)"
- by ferrack
-
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
- by ferrack
-
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero})>0. (ALL y. (EX z. 13* abs z \<noteq> abs (12*y - x) & 5*x - 3*(abs y) <= 7*z))"
- by ferrack
-
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). abs (4*x + 17) < 4 & (ALL y . abs (x*34 - 34*y - 9) \<noteq> 0 \<longrightarrow> (EX z. 5*x - 3*abs y <= 7*z))"
- by ferrack
-
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y > abs (23*x - 9). (ALL z > abs (3*y - 19* abs x). x+z > 2*y))"
- by ferrack
-
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y< abs (3*x - 1). (ALL z >= (3*abs x - 1). abs (12*x - 13*y + 19*z) > abs (23*x) ))"
- by ferrack
-
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). abs x < 100 & (ALL y > x. (EX z<2*y - x. 5*x - 3*y <= 7*z))"
- by ferrack
-
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. 7*x<3*y --> 5*y < 7*z --> z < 2*w --> 7*(2*w-x) > 2*y"
- by ferrack
-
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89"
- by ferrack
-
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. 5*x + 3*z - 17*w + 7* (y - 8*x + z) <= max y (7*z - x + w)"
- by ferrack
-
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)"
- by ferrack
-
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. (EX w >= (x+y+z). w <= abs x + abs y + abs z)"
- by ferrack
-
-lemma "~(ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y z w. 3* x + z*4 = 3*y & x + y < z & x> w & 3*x < w + y))"
- by ferrack
-
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX z w. abs (x-y) = (z-w) & z*1234 < 233*x & w ~= y)"
- by ferrack
-
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w))"
- by ferrack
-
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. (ALL w >= abs (x+y+z). w >= abs x + abs y + abs z)"
- by ferrack
-
-lemma "EX z. (ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX w >= (x+y+z). w <= abs x + abs y + abs z))"
- by ferrack
-
-lemma "EX z. (ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) < abs z. (EX y w. x< y & x < z & x> w & 3*x < w + y))"
- by ferrack
-
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX z. (ALL w. abs (x-y) = abs (z-w) --> z < x & w ~= y))"
- by ferrack
-
-lemma "EX y. (ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)))"
- by ferrack
-
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) z. (ALL w >= 13*x - 4*z. (EX y. w >= abs x + abs y + z))"
- by ferrack
-
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (ALL y < x. (EX z > (x+y).
- (ALL w. 5*w + 10*x - z >= y --> w + 7*x + 3*z >= 2*y)))"
- by ferrack
-
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (ALL y. (EX z > y.
- (ALL w . w < 13 --> w + 10*x - z >= y --> 5*w + 7*x + 13*z >= 2*y)))"
- by ferrack
-
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)"
- by ferrack
-
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))"
- by ferrack
-
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (x + z) < w - y)))"
- by ferrack
-
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y. abs y ~= abs x & (ALL z> max x y. (EX w. w ~= y & w ~= z & 3*w - z >= x + y)))"
- by ferrack
-
-end
--- a/src/HOL/ex/ExecutableContent.thy Wed Mar 11 11:40:58 2009 +0100
+++ b/src/HOL/ex/ExecutableContent.thy Wed Mar 11 11:41:14 2009 +0100
@@ -24,24 +24,6 @@
"~~/src/HOL/ex/Records"
begin
-lemma [code, code del]:
- "(size :: 'a::size Predicate.pred => nat) = size" ..
-lemma [code, code del]:
- "pred_size = pred_size" ..
-lemma [code, code del]:
- "pred_case = pred_case" ..
-lemma [code, code del]:
- "pred_rec = pred_rec" ..
-lemma [code, code del]:
- "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
-lemma [code, code del]:
- "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
-
-text {* However, some aren't executable *}
-
-declare pair_leq_def[code del]
-declare max_weak_def[code del]
-declare min_weak_def[code del]
-declare ms_weak_def[code del]
+declare min_weak_def [code del]
end
--- a/src/HOL/ex/ROOT.ML Wed Mar 11 11:40:58 2009 +0100
+++ b/src/HOL/ex/ROOT.ML Wed Mar 11 11:41:14 2009 +0100
@@ -60,7 +60,6 @@
"Code_Antiq",
"Termination",
"Coherent",
- "Dense_Linear_Order_Ex",
"PresburgerEx",
"ReflectionEx",
"BinEx",
--- a/src/Pure/General/name_space.ML Wed Mar 11 11:40:58 2009 +0100
+++ b/src/Pure/General/name_space.ML Wed Mar 11 11:41:14 2009 +0100
@@ -33,6 +33,8 @@
val full_name: naming -> binding -> string
val external_names: naming -> string -> string list
val add_path: string -> naming -> naming
+ val root_path: naming -> naming
+ val parent_path: naming -> naming
val no_base_names: naming -> naming
val qualified_names: naming -> naming
val sticky_prefix: string -> naming -> naming
@@ -189,10 +191,13 @@
val default_naming = make_naming ([], false, false);
fun add_path elems = map_naming (fn (path, no_base_names, qualified_names) =>
- if elems = "//" then ([], no_base_names, true)
- else if elems = "/" then ([], no_base_names, qualified_names)
- else if elems = ".." then (perhaps (try (#1 o split_last)) path, no_base_names, qualified_names)
- else (path @ map (rpair false) (Long_Name.explode elems), no_base_names, qualified_names));
+ (path @ map (rpair false) (Long_Name.explode elems), no_base_names, qualified_names));
+
+val root_path = map_naming (fn (_, no_base_names, qualified_names) =>
+ ([], no_base_names, qualified_names));
+
+val parent_path = map_naming (fn (path, no_base_names, qualified_names) =>
+ (perhaps (try (#1 o split_last)) path, no_base_names, qualified_names));
fun sticky_prefix elems = map_naming (fn (path, no_base_names, qualified_names) =>
(path @ map (rpair true) (Long_Name.explode elems), no_base_names, qualified_names));
--- a/src/Pure/Isar/proof.ML Wed Mar 11 11:40:58 2009 +0100
+++ b/src/Pure/Isar/proof.ML Wed Mar 11 11:41:14 2009 +0100
@@ -677,18 +677,19 @@
local
+fun qualified_binding a =
+ Binding.qualify true (Long_Name.qualifier a) (Binding.name (Long_Name.base_name a));
+
fun gen_invoke_case prep_att (name, xs, raw_atts) state =
let
val atts = map (prep_att (theory_of state)) raw_atts;
val (asms, state') = state |> map_context_result (fn ctxt =>
ctxt |> ProofContext.apply_case (ProofContext.get_case ctxt name xs));
- val assumptions = asms |> map (fn (a, ts) => ((Binding.name a, atts), map (rpair []) ts));
+ val assumptions = asms |> map (fn (a, ts) => ((qualified_binding a, atts), map (rpair []) ts));
in
state'
- |> map_context (ProofContext.qualified_names #> ProofContext.no_base_names)
|> assume_i assumptions
|> add_binds_i AutoBind.no_facts
- |> map_context (ProofContext.restore_naming (context_of state))
|> `the_facts |-> (fn thms => note_thmss_i [((Binding.name name, []), [(thms, [])])])
end;
--- a/src/Pure/Isar/proof_context.ML Wed Mar 11 11:40:58 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML Wed Mar 11 11:41:14 2009 +0100
@@ -97,9 +97,8 @@
val get_thms: Proof.context -> xstring -> thm list
val get_thm: Proof.context -> xstring -> thm
val add_path: string -> Proof.context -> Proof.context
- val no_base_names: Proof.context -> Proof.context
+ val sticky_prefix: string -> Proof.context -> Proof.context
val qualified_names: Proof.context -> Proof.context
- val sticky_prefix: string -> Proof.context -> Proof.context
val restore_naming: Proof.context -> Proof.context -> Proof.context
val reset_naming: Proof.context -> Proof.context
val note_thmss: string -> (Thm.binding * (Facts.ref * attribute list) list) list ->
@@ -263,9 +262,11 @@
fun transfer_syntax thy =
map_syntax (LocalSyntax.rebuild thy) #>
- map_consts (fn (local_consts, _) =>
- let val thy_consts = Sign.consts_of thy
- in (Consts.merge (local_consts, thy_consts), thy_consts) end);
+ map_consts (fn consts as (local_consts, global_consts) =>
+ let val thy_consts = Sign.consts_of thy in
+ if Consts.eq_consts (thy_consts, global_consts) then consts
+ else (Consts.merge (local_consts, thy_consts), thy_consts)
+ end);
fun transfer thy = Context.transfer_proof thy #> transfer_syntax thy;
@@ -945,9 +946,8 @@
(* name space operations *)
val add_path = map_naming o NameSpace.add_path;
-val no_base_names = map_naming NameSpace.no_base_names;
+val sticky_prefix = map_naming o NameSpace.sticky_prefix;
val qualified_names = map_naming NameSpace.qualified_names;
-val sticky_prefix = map_naming o NameSpace.sticky_prefix;
val restore_naming = map_naming o K o naming_of;
val reset_naming = map_naming (K local_naming);
--- a/src/Pure/Isar/toplevel.ML Wed Mar 11 11:40:58 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML Wed Mar 11 11:41:14 2009 +0100
@@ -293,7 +293,10 @@
local
fun debugging f x =
- if ! debug then exception_trace (fn () => f x)
+ if ! debug then
+ (case exception_trace (fn () => SOME (f x) handle UNDEF => NONE) of
+ SOME y => y
+ | NONE => raise UNDEF)
else f x;
fun toplevel_error f x =
--- a/src/Pure/consts.ML Wed Mar 11 11:40:58 2009 +0100
+++ b/src/Pure/consts.ML Wed Mar 11 11:41:14 2009 +0100
@@ -8,6 +8,7 @@
signature CONSTS =
sig
type T
+ val eq_consts: T * T -> bool
val abbrevs_of: T -> string list -> (term * term) list
val dest: T ->
{constants: (typ * term option) NameSpace.table,
@@ -53,6 +54,13 @@
constraints: typ Symtab.table,
rev_abbrevs: (term * term) list Symtab.table};
+fun eq_consts
+ (Consts {decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1},
+ Consts {decls = decls2, constraints = constraints2, rev_abbrevs = rev_abbrevs2}) =
+ pointer_eq (decls1, decls2) andalso
+ pointer_eq (constraints1, constraints2) andalso
+ pointer_eq (rev_abbrevs1, rev_abbrevs2);
+
fun make_consts (decls, constraints, rev_abbrevs) =
Consts {decls = decls, constraints = constraints, rev_abbrevs = rev_abbrevs};
--- a/src/Pure/sign.ML Wed Mar 11 11:40:58 2009 +0100
+++ b/src/Pure/sign.ML Wed Mar 11 11:41:14 2009 +0100
@@ -122,13 +122,13 @@
val add_trrules_i: ast Syntax.trrule list -> theory -> theory
val del_trrules_i: ast Syntax.trrule list -> theory -> theory
val add_path: string -> theory -> theory
+ val root_path: theory -> theory
val parent_path: theory -> theory
- val root_path: theory -> theory
+ val sticky_prefix: string -> theory -> theory
+ val no_base_names: theory -> theory
+ val qualified_names: theory -> theory
val absolute_path: theory -> theory
val local_path: theory -> theory
- val no_base_names: theory -> theory
- val qualified_names: theory -> theory
- val sticky_prefix: string -> theory -> theory
val restore_naming: theory -> theory -> theory
val hide_class: bool -> string -> theory -> theory
val hide_type: bool -> string -> theory -> theory
@@ -619,17 +619,18 @@
(* naming *)
val add_path = map_naming o NameSpace.add_path;
+val root_path = map_naming NameSpace.root_path;
+val parent_path = map_naming NameSpace.parent_path;
+val sticky_prefix = map_naming o NameSpace.sticky_prefix;
val no_base_names = map_naming NameSpace.no_base_names;
val qualified_names = map_naming NameSpace.qualified_names;
-val sticky_prefix = map_naming o NameSpace.sticky_prefix;
-val restore_naming = map_naming o K o naming_of;
-val parent_path = add_path "..";
-val root_path = add_path "/";
-val absolute_path = add_path "//";
+val absolute_path = root_path o qualified_names;
fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
+val restore_naming = map_naming o K o naming_of;
+
(* hide names *)