--- a/Admin/isatest/isatest-stats Mon Mar 23 08:14:58 2009 +0100
+++ b/Admin/isatest/isatest-stats Mon Mar 23 08:16:24 2009 +0100
@@ -31,6 +31,8 @@
HOL-UNITY \
HOL-Word \
HOL-ex \
+ HOLCF \
+ IOA \
ZF \
ZF-Constructible \
ZF-UNITY"
--- a/Admin/isatest/settings/at-mac-poly-5.1-para Mon Mar 23 08:14:58 2009 +0100
+++ b/Admin/isatest/settings/at-mac-poly-5.1-para Mon Mar 23 08:16:24 2009 +0100
@@ -4,7 +4,7 @@
ML_SYSTEM="polyml-5.2.1"
ML_PLATFORM="x86-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="--mutable 200 --immutable 800"
+ ML_OPTIONS="--mutable 800 --immutable 2000"
ISABELLE_HOME_USER=~/isabelle-at-mac-poly-e
--- a/NEWS Mon Mar 23 08:14:58 2009 +0100
+++ b/NEWS Mon Mar 23 08:16:24 2009 +0100
@@ -685,6 +685,12 @@
Syntax.read_term_global etc.; see also OldGoals.read_term as last
resort for legacy applications.
+* Disposed old declarations, tactics, tactic combinators that refer to
+the simpset or claset of an implicit theory (such as Addsimps,
+Simp_tac, SIMPSET). INCOMPATIBILITY, should use @{simpset} etc. in
+embedded ML text, or local_simpset_of with a proper context passed as
+explicit runtime argument.
+
* Antiquotations: block-structured compilation context indicated by
\<lbrace> ... \<rbrace>; additional antiquotation forms:
--- a/doc-src/IsarOverview/Isar/Induction.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/doc-src/IsarOverview/Isar/Induction.thy Mon Mar 23 08:16:24 2009 +0100
@@ -143,14 +143,14 @@
universally quantifies all \emph{vars} before the induction. Hence
they can be replaced by \emph{arbitrary} values in the proof.
-The nice thing about generalization via @{text"arbitrary:"} is that in
-the induction step the claim is available in unquantified form but
+Generalization via @{text"arbitrary"} is particularly convenient
+if the induction step is a structured proof as opposed to the automatic
+example above. Then the claim is available in unquantified form but
with the generalized variables replaced by @{text"?"}-variables, ready
-for instantiation. In the above example the
-induction hypothesis is @{text"itrev xs ?ys = rev xs @ ?ys"}.
+for instantiation. In the above example, in the @{const[source] Cons} case the
+induction hypothesis is @{text"itrev xs ?ys = rev xs @ ?ys"} (available
+under the name @{const[source] Cons}).
-For the curious: @{text"arbitrary:"} introduces @{text"\<And>"}
-behind the scenes.
\subsection{Inductive proofs of conditional formulae}
\label{sec:full-Ind}
--- a/doc-src/IsarOverview/Isar/Logic.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/doc-src/IsarOverview/Isar/Logic.thy Mon Mar 23 08:16:24 2009 +0100
@@ -30,8 +30,8 @@
show A by(rule a)
qed
-text{*\noindent Single-identifier formulae such as @{term A} need not
-be enclosed in double quotes. However, we will continue to do so for
+text{*\noindent As you see above, single-identifier formulae such as @{term A}
+need not be enclosed in double quotes. However, we will continue to do so for
uniformity.
Instead of applying fact @{text a} via the @{text rule} method, we can
--- a/doc-src/IsarOverview/Isar/document/Induction.tex Mon Mar 23 08:14:58 2009 +0100
+++ b/doc-src/IsarOverview/Isar/document/Induction.tex Mon Mar 23 08:16:24 2009 +0100
@@ -342,14 +342,14 @@
universally quantifies all \emph{vars} before the induction. Hence
they can be replaced by \emph{arbitrary} values in the proof.
-The nice thing about generalization via \isa{arbitrary{\isacharcolon}} is that in
-the induction step the claim is available in unquantified form but
+Generalization via \isa{arbitrary} is particularly convenient
+if the induction step is a structured proof as opposed to the automatic
+example above. Then the claim is available in unquantified form but
with the generalized variables replaced by \isa{{\isacharquery}}-variables, ready
-for instantiation. In the above example the
-induction hypothesis is \isa{itrev\ xs\ {\isacharquery}ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ {\isacharquery}ys}.
+for instantiation. In the above example, in the \isa{Cons} case the
+induction hypothesis is \isa{itrev\ xs\ {\isacharquery}ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ {\isacharquery}ys} (available
+under the name \isa{Cons}).
-For the curious: \isa{arbitrary{\isacharcolon}} introduces \isa{{\isasymAnd}}
-behind the scenes.
\subsection{Inductive proofs of conditional formulae}
\label{sec:full-Ind}
--- a/doc-src/IsarOverview/Isar/document/Logic.tex Mon Mar 23 08:14:58 2009 +0100
+++ b/doc-src/IsarOverview/Isar/document/Logic.tex Mon Mar 23 08:16:24 2009 +0100
@@ -93,8 +93,8 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-\noindent Single-identifier formulae such as \isa{A} need not
-be enclosed in double quotes. However, we will continue to do so for
+\noindent As you see above, single-identifier formulae such as \isa{A}
+need not be enclosed in double quotes. However, we will continue to do so for
uniformity.
Instead of applying fact \isa{a} via the \isa{rule} method, we can
--- a/doc-src/TutorialI/Documents/Documents.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/doc-src/TutorialI/Documents/Documents.thy Mon Mar 23 08:16:24 2009 +0100
@@ -617,7 +617,7 @@
same types as they have in the main goal statement.
\medskip Several further kinds of antiquotations and options are
- available \cite{isabelle-sys}. Here are a few commonly used
+ available \cite{isabelle-isar-ref}. Here are a few commonly used
combinations:
\medskip
--- a/doc-src/TutorialI/Documents/document/Documents.tex Mon Mar 23 08:14:58 2009 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Mon Mar 23 08:16:24 2009 +0100
@@ -691,7 +691,7 @@
same types as they have in the main goal statement.
\medskip Several further kinds of antiquotations and options are
- available \cite{isabelle-sys}. Here are a few commonly used
+ available \cite{isabelle-isar-ref}. Here are a few commonly used
combinations:
\medskip
--- a/doc-src/TutorialI/Protocol/Message.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/doc-src/TutorialI/Protocol/Message.thy Mon Mar 23 08:16:24 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Auth/Message
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
@@ -830,9 +829,9 @@
(*Prove base case (subgoal i) and simplify others. A typical base case
concerns Crypt K X \<notin> Key`shrK`bad and cannot be proved by rewriting
alone.*)
-fun prove_simple_subgoals_tac i =
- force_tac (claset(), simpset() addsimps [@{thm image_eq_UN}]) i THEN
- ALLGOALS Asm_simp_tac
+fun prove_simple_subgoals_tac (cs, ss) i =
+ force_tac (cs, ss addsimps [@{thm image_eq_UN}]) i THEN
+ ALLGOALS (asm_simp_tac ss)
(*Analysis of Fake cases. Also works for messages that forward unknown parts,
but this application is no longer necessary if analz_insert_eq is used.
@@ -857,8 +856,7 @@
(cs addIs [analz_insertI,
impOfSubs analz_subset_parts]) 4 1))
-(*The explicit claset and simpset arguments help it work with Isar*)
-fun gen_spy_analz_tac (cs,ss) i =
+fun spy_analz_tac (cs,ss) i =
DETERM
(SELECT_GOAL
(EVERY
@@ -870,8 +868,6 @@
simp_tac ss 1,
REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)
-
-fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i
*}
text{*By default only @{text o_apply} is built-in. But in the presence of
@@ -919,7 +915,7 @@
lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
method_setup spy_analz = {*
- Scan.succeed (SIMPLE_METHOD' o gen_spy_analz_tac o local_clasimpset_of) *}
+ Scan.succeed (SIMPLE_METHOD' o spy_analz_tac o local_clasimpset_of) *}
"for proving the Fake case when analz is involved"
method_setup atomic_spy_analz = {*
--- a/doc-src/TutorialI/Protocol/Public.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/doc-src/TutorialI/Protocol/Public.thy Mon Mar 23 08:16:24 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Auth/Public
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
@@ -153,15 +152,15 @@
(*Tactic for possibility theorems*)
ML {*
-fun possibility_tac st = st |>
+fun possibility_tac ctxt =
REPEAT (*omit used_Says so that Nonces start from different traces!*)
- (ALLGOALS (simp_tac (@{simpset} delsimps [used_Says]))
+ (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [used_Says]))
THEN
REPEAT_FIRST (eq_assume_tac ORELSE'
resolve_tac [refl, conjI, @{thm Nonce_supply}]));
*}
-method_setup possibility = {* Scan.succeed (K (SIMPLE_METHOD possibility_tac)) *}
+method_setup possibility = {* Scan.succeed (SIMPLE_METHOD o possibility_tac) *}
"for proving possibility theorems"
end
--- a/doc-src/TutorialI/Rules/rules.tex Mon Mar 23 08:14:58 2009 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex Mon Mar 23 08:16:24 2009 +0100
@@ -2138,11 +2138,11 @@
\index{*insert (method)|(}%
The \isa{insert} method
-inserts a given theorem as a new assumption of the current subgoal. This
+inserts a given theorem as a new assumption of all subgoals. This
already is a forward step; moreover, we may (as always when using a
theorem) apply
\isa{of}, \isa{THEN} and other directives. The new assumption can then
-be used to help prove the subgoal.
+be used to help prove the subgoals.
For example, consider this theorem about the divides relation. The first
proof step inserts the distributive law for
--- a/doc-src/TutorialI/Sets/sets.tex Mon Mar 23 08:14:58 2009 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex Mon Mar 23 08:16:24 2009 +0100
@@ -299,7 +299,7 @@
\isa{UN x:A.\ B} in \textsc{ascii}. Indexed union satisfies this basic law:
\begin{isabelle}
(b\ \isasymin\
-(\isasymUnion x\isasymin A. B\ x) =\ (\isasymexists x\isasymin A.\
+(\isasymUnion x\isasymin A. B\ x)) =\ (\isasymexists x\isasymin A.\
b\ \isasymin\ B\ x)
\rulenamedx{UN_iff}
\end{isabelle}
@@ -414,12 +414,12 @@
$k$-element subsets of~$A$ is \index{binomial coefficients}
$\binom{n}{k}$.
-\begin{warn}
-The term \isa{finite\ A} is defined via a syntax translation as an
-abbreviation for \isa{A {\isasymin} Finites}, where the constant
-\cdx{Finites} denotes the set of all finite sets of a given type. There
-is no constant \isa{finite}.
-\end{warn}
+%\begin{warn}
+%The term \isa{finite\ A} is defined via a syntax translation as an
+%abbreviation for \isa{A {\isasymin} Finites}, where the constant
+%\cdx{Finites} denotes the set of all finite sets of a given type. There
+%is no constant \isa{finite}.
+%\end{warn}
\index{sets|)}
--- a/doc-src/TutorialI/Types/Overloading2.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/doc-src/TutorialI/Types/Overloading2.thy Mon Mar 23 08:16:24 2009 +0100
@@ -15,7 +15,7 @@
size xs = size ys \<and> (\<forall>i<size xs. xs!i <<= ys!i)"
text{*\noindent
-The infix function @{text"!"} yields the nth element of a list.
+The infix function @{text"!"} yields the nth element of a list, starting with 0.
\begin{warn}
A type constructor can be instantiated in only one way to
--- a/doc-src/TutorialI/Types/document/Overloading2.tex Mon Mar 23 08:14:58 2009 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading2.tex Mon Mar 23 08:16:24 2009 +0100
@@ -46,7 +46,7 @@
\ \ \ \ \ \ \ \ \ \ \ \ \ \ size\ xs\ {\isacharequal}\ size\ ys\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isacharless}size\ xs{\isachardot}\ xs{\isacharbang}i\ {\isacharless}{\isacharless}{\isacharequal}\ ys{\isacharbang}i{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
-The infix function \isa{{\isacharbang}} yields the nth element of a list.
+The infix function \isa{{\isacharbang}} yields the nth element of a list, starting with 0.
\begin{warn}
A type constructor can be instantiated in only one way to
--- a/src/CCL/Type.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/CCL/Type.thy Mon Mar 23 08:16:24 2009 +0100
@@ -1,5 +1,4 @@
(* Title: CCL/Type.thy
- ID: $Id$
Author: Martin Coen
Copyright 1993 University of Cambridge
*)
@@ -409,7 +408,7 @@
fun mk_genIs thy defs genXH gen_mono s = prove_goalw thy defs s
(fn prems => [rtac (genXH RS iffD2) 1,
- SIMPSET' simp_tac 1,
+ simp_tac (simpset_of thy) 1,
TRY (fast_tac (@{claset} addIs
([genXH RS iffD2,gen_mono RS coinduct3_mono_lemma RS lfpI]
@ prems)) 1)])
@@ -442,8 +441,8 @@
"<[],[]> : POgen(lfp(%x. POgen(x) Un R Un PO))",
"[| <h,h'> : lfp(%x. POgen(x) Un R Un PO); <t,t'> : lfp(%x. POgen(x) Un R Un PO) |] ==> <h$t,h'$t'> : POgen(lfp(%x. POgen(x) Un R Un PO))"];
-fun POgen_tac (rla,rlb) i =
- SELECT_GOAL (CLASET safe_tac) i THEN
+fun POgen_tac ctxt (rla,rlb) i =
+ SELECT_GOAL (safe_tac (local_claset_of ctxt)) i THEN
rtac (rlb RS (rla RS (thm "ssubst_pair"))) i THEN
(REPEAT (resolve_tac (POgenIs @ [thm "PO_refl" RS (thm "POgen_mono" RS ci3_AI)] @
(POgenIs RL [thm "POgen_mono" RS ci3_AgenI]) @ [thm "POgen_mono" RS ci3_RI]) i));
--- a/src/FOL/blastdata.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/FOL/blastdata.ML Mon Mar 23 08:16:24 2009 +0100
@@ -1,5 +1,5 @@
-(*** Applying BlastFun to create Blast_tac ***)
+(*** Applying BlastFun to create blast_tac ***)
structure Blast_Data =
struct
type claset = Cla.claset
@@ -10,13 +10,10 @@
val contr_tac = Cla.contr_tac
val dup_intr = Cla.dup_intr
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
- val claset = Cla.claset
- val rep_cs = Cla.rep_cs
+ val rep_cs = Cla.rep_cs
val cla_modifiers = Cla.cla_modifiers;
val cla_meth' = Cla.cla_meth'
end;
structure Blast = BlastFun(Blast_Data);
-
-val Blast_tac = Blast.Blast_tac
-and blast_tac = Blast.blast_tac;
+val blast_tac = Blast.blast_tac;
--- a/src/FOL/simpdata.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/FOL/simpdata.ML Mon Mar 23 08:16:24 2009 +0100
@@ -117,8 +117,6 @@
val split_asm_tac = Splitter.split_asm_tac;
val op addsplits = Splitter.addsplits;
val op delsplits = Splitter.delsplits;
-val Addsplits = Splitter.Addsplits;
-val Delsplits = Splitter.Delsplits;
(*** Standard simpsets ***)
--- a/src/HOL/Arith_Tools.thy Mon Mar 23 08:14:58 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,388 +0,0 @@
-(* Title: HOL/Arith_Tools.thy
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Author: Amine Chaieb, TU Muenchen
-*)
-
-header {* Setup of arithmetic tools *}
-
-theory Arith_Tools
-imports NatBin
-uses
- "~~/src/Provers/Arith/cancel_numeral_factor.ML"
- "~~/src/Provers/Arith/extract_common_term.ML"
- "Tools/int_factor_simprocs.ML"
- "Tools/nat_simprocs.ML"
- "Tools/Qelim/qelim.ML"
-begin
-
-subsection {* Simprocs for the Naturals *}
-
-declaration {* K nat_simprocs_setup *}
-
-subsubsection{*For simplifying @{term "Suc m - K"} and @{term "K - Suc m"}*}
-
-text{*Where K above is a literal*}
-
-lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"
-by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split)
-
-text {*Now just instantiating @{text n} to @{text "number_of v"} does
- the right simplification, but with some redundant inequality
- tests.*}
-lemma neg_number_of_pred_iff_0:
- "neg (number_of (Int.pred v)::int) = (number_of v = (0::nat))"
-apply (subgoal_tac "neg (number_of (Int.pred v)) = (number_of v < Suc 0) ")
-apply (simp only: less_Suc_eq_le le_0_eq)
-apply (subst less_number_of_Suc, simp)
-done
-
-text{*No longer required as a simprule because of the @{text inverse_fold}
- simproc*}
-lemma Suc_diff_number_of:
- "Int.Pls < v ==>
- Suc m - (number_of v) = m - (number_of (Int.pred v))"
-apply (subst Suc_diff_eq_diff_pred)
-apply simp
-apply (simp del: nat_numeral_1_eq_1)
-apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric]
- neg_number_of_pred_iff_0)
-done
-
-lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
-by (simp add: numerals split add: nat_diff_split)
-
-
-subsubsection{*For @{term nat_case} and @{term nat_rec}*}
-
-lemma nat_case_number_of [simp]:
- "nat_case a f (number_of v) =
- (let pv = number_of (Int.pred v) in
- if neg pv then a else f (nat pv))"
-by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0)
-
-lemma nat_case_add_eq_if [simp]:
- "nat_case a f ((number_of v) + n) =
- (let pv = number_of (Int.pred v) in
- if neg pv then nat_case a f n else f (nat pv + n))"
-apply (subst add_eq_if)
-apply (simp split add: nat.split
- del: nat_numeral_1_eq_1
- add: nat_numeral_1_eq_1 [symmetric]
- numeral_1_eq_Suc_0 [symmetric]
- neg_number_of_pred_iff_0)
-done
-
-lemma nat_rec_number_of [simp]:
- "nat_rec a f (number_of v) =
- (let pv = number_of (Int.pred v) in
- if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"
-apply (case_tac " (number_of v) ::nat")
-apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0)
-apply (simp split add: split_if_asm)
-done
-
-lemma nat_rec_add_eq_if [simp]:
- "nat_rec a f (number_of v + n) =
- (let pv = number_of (Int.pred v) in
- if neg pv then nat_rec a f n
- else f (nat pv + n) (nat_rec a f (nat pv + n)))"
-apply (subst add_eq_if)
-apply (simp split add: nat.split
- del: nat_numeral_1_eq_1
- add: nat_numeral_1_eq_1 [symmetric]
- numeral_1_eq_Suc_0 [symmetric]
- neg_number_of_pred_iff_0)
-done
-
-
-subsubsection{*Various Other Lemmas*}
-
-text {*Evens and Odds, for Mutilated Chess Board*}
-
-text{*Lemmas for specialist use, NOT as default simprules*}
-lemma nat_mult_2: "2 * z = (z+z::nat)"
-proof -
- have "2*z = (1 + 1)*z" by simp
- also have "... = z+z" by (simp add: left_distrib)
- finally show ?thesis .
-qed
-
-lemma nat_mult_2_right: "z * 2 = (z+z::nat)"
-by (subst mult_commute, rule nat_mult_2)
-
-text{*Case analysis on @{term "n<2"}*}
-lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
-by arith
-
-lemma div2_Suc_Suc [simp]: "Suc(Suc m) div 2 = Suc (m div 2)"
-by arith
-
-lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
-by (simp add: nat_mult_2 [symmetric])
-
-lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2"
-apply (subgoal_tac "m mod 2 < 2")
-apply (erule less_2_cases [THEN disjE])
-apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1)
-done
-
-lemma mod2_gr_0 [simp]: "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)"
-apply (subgoal_tac "m mod 2 < 2")
-apply (force simp del: mod_less_divisor, simp)
-done
-
-text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*}
-
-lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
-by simp
-
-lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"
-by simp
-
-text{*Can be used to eliminate long strings of Sucs, but not by default*}
-lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
-by simp
-
-
-text{*These lemmas collapse some needless occurrences of Suc:
- at least three Sucs, since two and fewer are rewritten back to Suc again!
- We already have some rules to simplify operands smaller than 3.*}
-
-lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
-by (simp add: Suc3_eq_add_3)
-
-lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
-by (simp add: Suc3_eq_add_3)
-
-lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
-by (simp add: Suc3_eq_add_3)
-
-lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
-by (simp add: Suc3_eq_add_3)
-
-lemmas Suc_div_eq_add3_div_number_of =
- Suc_div_eq_add3_div [of _ "number_of v", standard]
-declare Suc_div_eq_add3_div_number_of [simp]
-
-lemmas Suc_mod_eq_add3_mod_number_of =
- Suc_mod_eq_add3_mod [of _ "number_of v", standard]
-declare Suc_mod_eq_add3_mod_number_of [simp]
-
-
-subsubsection{*Special Simplification for Constants*}
-
-text{*These belong here, late in the development of HOL, to prevent their
-interfering with proofs of abstract properties of instances of the function
-@{term number_of}*}
-
-text{*These distributive laws move literals inside sums and differences.*}
-lemmas left_distrib_number_of = left_distrib [of _ _ "number_of v", standard]
-declare left_distrib_number_of [simp]
-
-lemmas right_distrib_number_of = right_distrib [of "number_of v", standard]
-declare right_distrib_number_of [simp]
-
-
-lemmas left_diff_distrib_number_of =
- left_diff_distrib [of _ _ "number_of v", standard]
-declare left_diff_distrib_number_of [simp]
-
-lemmas right_diff_distrib_number_of =
- right_diff_distrib [of "number_of v", standard]
-declare right_diff_distrib_number_of [simp]
-
-
-text{*These are actually for fields, like real: but where else to put them?*}
-lemmas zero_less_divide_iff_number_of =
- zero_less_divide_iff [of "number_of w", standard]
-declare zero_less_divide_iff_number_of [simp,noatp]
-
-lemmas divide_less_0_iff_number_of =
- divide_less_0_iff [of "number_of w", standard]
-declare divide_less_0_iff_number_of [simp,noatp]
-
-lemmas zero_le_divide_iff_number_of =
- zero_le_divide_iff [of "number_of w", standard]
-declare zero_le_divide_iff_number_of [simp,noatp]
-
-lemmas divide_le_0_iff_number_of =
- divide_le_0_iff [of "number_of w", standard]
-declare divide_le_0_iff_number_of [simp,noatp]
-
-
-(****
-IF times_divide_eq_right and times_divide_eq_left are removed as simprules,
-then these special-case declarations may be useful.
-
-text{*These simprules move numerals into numerators and denominators.*}
-lemma times_recip_eq_right [simp]: "a * (1/c) = a / (c::'a::field)"
-by (simp add: times_divide_eq)
-
-lemma times_recip_eq_left [simp]: "(1/c) * a = a / (c::'a::field)"
-by (simp add: times_divide_eq)
-
-lemmas times_divide_eq_right_number_of =
- times_divide_eq_right [of "number_of w", standard]
-declare times_divide_eq_right_number_of [simp]
-
-lemmas times_divide_eq_right_number_of =
- times_divide_eq_right [of _ _ "number_of w", standard]
-declare times_divide_eq_right_number_of [simp]
-
-lemmas times_divide_eq_left_number_of =
- times_divide_eq_left [of _ "number_of w", standard]
-declare times_divide_eq_left_number_of [simp]
-
-lemmas times_divide_eq_left_number_of =
- times_divide_eq_left [of _ _ "number_of w", standard]
-declare times_divide_eq_left_number_of [simp]
-
-****)
-
-text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}. It looks
- strange, but then other simprocs simplify the quotient.*}
-
-lemmas inverse_eq_divide_number_of =
- inverse_eq_divide [of "number_of w", standard]
-declare inverse_eq_divide_number_of [simp]
-
-
-text {*These laws simplify inequalities, moving unary minus from a term
-into the literal.*}
-lemmas less_minus_iff_number_of =
- less_minus_iff [of "number_of v", standard]
-declare less_minus_iff_number_of [simp,noatp]
-
-lemmas le_minus_iff_number_of =
- le_minus_iff [of "number_of v", standard]
-declare le_minus_iff_number_of [simp,noatp]
-
-lemmas equation_minus_iff_number_of =
- equation_minus_iff [of "number_of v", standard]
-declare equation_minus_iff_number_of [simp,noatp]
-
-
-lemmas minus_less_iff_number_of =
- minus_less_iff [of _ "number_of v", standard]
-declare minus_less_iff_number_of [simp,noatp]
-
-lemmas minus_le_iff_number_of =
- minus_le_iff [of _ "number_of v", standard]
-declare minus_le_iff_number_of [simp,noatp]
-
-lemmas minus_equation_iff_number_of =
- minus_equation_iff [of _ "number_of v", standard]
-declare minus_equation_iff_number_of [simp,noatp]
-
-
-text{*To Simplify Inequalities Where One Side is the Constant 1*}
-
-lemma less_minus_iff_1 [simp,noatp]:
- fixes b::"'b::{ordered_idom,number_ring}"
- shows "(1 < - b) = (b < -1)"
-by auto
-
-lemma le_minus_iff_1 [simp,noatp]:
- fixes b::"'b::{ordered_idom,number_ring}"
- shows "(1 \<le> - b) = (b \<le> -1)"
-by auto
-
-lemma equation_minus_iff_1 [simp,noatp]:
- fixes b::"'b::number_ring"
- shows "(1 = - b) = (b = -1)"
-by (subst equation_minus_iff, auto)
-
-lemma minus_less_iff_1 [simp,noatp]:
- fixes a::"'b::{ordered_idom,number_ring}"
- shows "(- a < 1) = (-1 < a)"
-by auto
-
-lemma minus_le_iff_1 [simp,noatp]:
- fixes a::"'b::{ordered_idom,number_ring}"
- shows "(- a \<le> 1) = (-1 \<le> a)"
-by auto
-
-lemma minus_equation_iff_1 [simp,noatp]:
- fixes a::"'b::number_ring"
- shows "(- a = 1) = (a = -1)"
-by (subst minus_equation_iff, auto)
-
-
-text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
-
-lemmas mult_less_cancel_left_number_of =
- mult_less_cancel_left [of "number_of v", standard]
-declare mult_less_cancel_left_number_of [simp,noatp]
-
-lemmas mult_less_cancel_right_number_of =
- mult_less_cancel_right [of _ "number_of v", standard]
-declare mult_less_cancel_right_number_of [simp,noatp]
-
-lemmas mult_le_cancel_left_number_of =
- mult_le_cancel_left [of "number_of v", standard]
-declare mult_le_cancel_left_number_of [simp,noatp]
-
-lemmas mult_le_cancel_right_number_of =
- mult_le_cancel_right [of _ "number_of v", standard]
-declare mult_le_cancel_right_number_of [simp,noatp]
-
-
-text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
-
-lemmas le_divide_eq_number_of1 [simp] = le_divide_eq [of _ _ "number_of w", standard]
-lemmas divide_le_eq_number_of1 [simp] = divide_le_eq [of _ "number_of w", standard]
-lemmas less_divide_eq_number_of1 [simp] = less_divide_eq [of _ _ "number_of w", standard]
-lemmas divide_less_eq_number_of1 [simp] = divide_less_eq [of _ "number_of w", standard]
-lemmas eq_divide_eq_number_of1 [simp] = eq_divide_eq [of _ _ "number_of w", standard]
-lemmas divide_eq_eq_number_of1 [simp] = divide_eq_eq [of _ "number_of w", standard]
-
-
-subsubsection{*Optional Simplification Rules Involving Constants*}
-
-text{*Simplify quotients that are compared with a literal constant.*}
-
-lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w", standard]
-lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w", standard]
-lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w", standard]
-lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w", standard]
-lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w", standard]
-lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w", standard]
-
-
-text{*Not good as automatic simprules because they cause case splits.*}
-lemmas divide_const_simps =
- le_divide_eq_number_of divide_le_eq_number_of less_divide_eq_number_of
- divide_less_eq_number_of eq_divide_eq_number_of divide_eq_eq_number_of
- le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
-
-text{*Division By @{text "-1"}*}
-
-lemma divide_minus1 [simp]:
- "x/-1 = -(x::'a::{field,division_by_zero,number_ring})"
-by simp
-
-lemma minus1_divide [simp]:
- "-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)"
-by (simp add: divide_inverse inverse_minus_eq)
-
-lemma half_gt_zero_iff:
- "(0 < r/2) = (0 < (r::'a::{ordered_field,division_by_zero,number_ring}))"
-by auto
-
-lemmas half_gt_zero = half_gt_zero_iff [THEN iffD2, standard]
-declare half_gt_zero [simp]
-
-(* The following lemma should appear in Divides.thy, but there the proof
- doesn't work. *)
-
-lemma nat_dvd_not_less:
- "[| 0 < m; m < n |] ==> \<not> n dvd (m::nat)"
- by (unfold dvd_def) auto
-
-ML {*
-val divide_minus1 = @{thm divide_minus1};
-val minus1_divide = @{thm minus1_divide};
-*}
-
-end
--- a/src/HOL/Auth/Message.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/Auth/Message.thy Mon Mar 23 08:16:24 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Auth/Message
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
@@ -848,9 +847,9 @@
(*Prove base case (subgoal i) and simplify others. A typical base case
concerns Crypt K X \<notin> Key`shrK`bad and cannot be proved by rewriting
alone.*)
-fun prove_simple_subgoals_tac i =
- CLASIMPSET' (fn (cs, ss) => force_tac (cs, ss addsimps [@{thm image_eq_UN}])) i THEN
- ALLGOALS (SIMPSET' asm_simp_tac)
+fun prove_simple_subgoals_tac (cs, ss) i =
+ force_tac (cs, ss addsimps [@{thm image_eq_UN}]) i THEN
+ ALLGOALS (asm_simp_tac ss)
(*Analysis of Fake cases. Also works for messages that forward unknown parts,
but this application is no longer necessary if analz_insert_eq is used.
@@ -875,8 +874,7 @@
(cs addIs [@{thm analz_insertI},
impOfSubs @{thm analz_subset_parts}]) 4 1))
-(*The explicit claset and simpset arguments help it work with Isar*)
-fun gen_spy_analz_tac (cs,ss) i =
+fun spy_analz_tac (cs,ss) i =
DETERM
(SELECT_GOAL
(EVERY
@@ -888,8 +886,6 @@
REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)
-val spy_analz_tac = CLASIMPSET' gen_spy_analz_tac;
-
end
*}
@@ -941,7 +937,7 @@
lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
method_setup spy_analz = {*
- Scan.succeed (SIMPLE_METHOD' o Message.gen_spy_analz_tac o local_clasimpset_of) *}
+ Scan.succeed (SIMPLE_METHOD' o Message.spy_analz_tac o local_clasimpset_of) *}
"for proving the Fake case when analz is involved"
method_setup atomic_spy_analz = {*
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Mar 23 08:16:24 2009 +0100
@@ -299,7 +299,7 @@
*} "Langford's algorithm for quantifier elimination in dense linear orders"
-section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields -- see @{text "Arith_Tools.thy"} *}
+section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields *}
text {* Linear order without upper bounds *}
--- a/src/HOL/Decision_Procs/MIR.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy Mon Mar 23 08:16:24 2009 +0100
@@ -3783,8 +3783,7 @@
also from mult_left_mono[OF xp] np have "?N s \<le> real n * x + ?N s" by simp
finally have "?N (Floor s) \<le> real n * x + ?N s" .
moreover
- {from mult_strict_left_mono[OF x1] np
- have "real n *x + ?N s < real n + ?N s" by simp
+ {from x1 np have "real n *x + ?N s < real n + ?N s" by simp
also from real_of_int_floor_add_one_gt[where r="?N s"]
have "\<dots> < real n + ?N (Floor s) + 1" by simp
finally have "real n *x + ?N s < ?N (Floor s) + real (n+1)" by simp}
@@ -3809,8 +3808,7 @@
moreover from mult_left_mono_neg[OF xp] nn have "?N s \<ge> real n * x + ?N s" by simp
ultimately have "?N (Floor s) + 1 > real n * x + ?N s" by arith
moreover
- {from mult_strict_left_mono_neg[OF x1, where c="real n"] nn
- have "real n *x + ?N s \<ge> real n + ?N s" by simp
+ {from x1 nn have "real n *x + ?N s \<ge> real n + ?N s" by simp
moreover from real_of_int_floor_le[where r="?N s"] have "real n + ?N s \<ge> real n + ?N (Floor s)" by simp
ultimately have "real n *x + ?N s \<ge> ?N (Floor s) + real n"
by (simp only: algebra_simps)}
--- a/src/HOL/Divides.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/Divides.thy Mon Mar 23 08:16:24 2009 +0100
@@ -1148,4 +1148,9 @@
with j show ?thesis by blast
qed
+lemma nat_dvd_not_less:
+ fixes m n :: nat
+ shows "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
+by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
+
end
--- a/src/HOL/Groebner_Basis.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/Groebner_Basis.thy Mon Mar 23 08:16:24 2009 +0100
@@ -5,7 +5,7 @@
header {* Semiring normalization and Groebner Bases *}
theory Groebner_Basis
-imports Arith_Tools
+imports NatBin
uses
"Tools/Groebner_Basis/misc.ML"
"Tools/Groebner_Basis/normalizer_data.ML"
--- a/src/HOL/HOL.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/HOL.thy Mon Mar 23 08:16:24 2009 +0100
@@ -1018,12 +1018,10 @@
val contr_tac = Classical.contr_tac
val dup_intr = Classical.dup_intr
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
- val claset = Classical.claset
val rep_cs = Classical.rep_cs
val cla_modifiers = Classical.cla_modifiers
val cla_meth' = Classical.cla_meth'
);
-val Blast_tac = Blast.Blast_tac;
val blast_tac = Blast.blast_tac;
*}
--- a/src/HOL/IMPP/Hoare.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/IMPP/Hoare.thy Mon Mar 23 08:16:24 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/IMPP/Hoare.thy
- ID: $Id$
Author: David von Oheimb
Copyright 1999 TUM
*)
@@ -219,7 +218,7 @@
apply (rule hoare_derivs.conseq, intro strip, tactic "smp_tac 2 1", clarify, tactic "smp_tac 1 1",rule exI, rule exI, erule (1) conjI)
prefer 7
apply (rule_tac hoare_derivs.Body, drule_tac spec, erule_tac mp, fast)
-apply (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) (thms "hoare_derivs.intros")) THEN_ALL_NEW CLASET' fast_tac) *})
+apply (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) (thms "hoare_derivs.intros")) THEN_ALL_NEW (fast_tac @{claset})) *})
done
lemma weak_Body: "G|-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}"
@@ -291,7 +290,7 @@
simp_tac @{simpset}, clarify_tac @{claset}, REPEAT o smp_tac 1]) *})
apply (simp_all (no_asm_use) add: triple_valid_def2)
apply (intro strip, tactic "smp_tac 2 1", blast) (* conseq *)
-apply (tactic {* ALLGOALS (CLASIMPSET' clarsimp_tac) *}) (* Skip, Ass, Local *)
+apply (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *}) (* Skip, Ass, Local *)
prefer 3 apply (force) (* Call *)
apply (erule_tac [2] evaln_elim_cases) (* If *)
apply blast+
@@ -336,17 +335,17 @@
lemma MGF_lemma1 [rule_format (no_asm)]: "state_not_singleton ==>
!pn:dom body. G|-{=}.BODY pn.{->} ==> WT c --> G|-{=}.c.{->}"
apply (induct_tac c)
-apply (tactic {* ALLGOALS (CLASIMPSET' clarsimp_tac) *})
+apply (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *})
prefer 7 apply (fast intro: domI)
apply (erule_tac [6] MGT_alternD)
apply (unfold MGT_def)
apply (drule_tac [7] bspec, erule_tac [7] domI)
-apply (rule_tac [7] escape, tactic {* CLASIMPSET' clarsimp_tac 7 *},
+apply (rule_tac [7] escape, tactic {* clarsimp_tac @{clasimpset} 7 *},
rule_tac [7] P1 = "%Z' s. s= (setlocs Z newlocs) [Loc Arg ::= fun Z]" in hoare_derivs.Call [THEN conseq1], erule_tac [7] conseq12)
apply (erule_tac [!] thin_rl)
apply (rule hoare_derivs.Skip [THEN conseq2])
apply (rule_tac [2] hoare_derivs.Ass [THEN conseq1])
-apply (rule_tac [3] escape, tactic {* CLASIMPSET' clarsimp_tac 3 *},
+apply (rule_tac [3] escape, tactic {* clarsimp_tac @{clasimpset} 3 *},
rule_tac [3] P1 = "%Z' s. s= (Z[Loc loc::=fun Z])" in hoare_derivs.Local [THEN conseq1],
erule_tac [3] conseq12)
apply (erule_tac [5] hoare_derivs.Comp, erule_tac [5] conseq12)
@@ -365,7 +364,7 @@
shows "finite U ==> uG = mgt_call`U ==>
!G. G <= uG --> n <= card uG --> card G = card uG - n --> (!c. wt c --> P G {mgt c})"
apply (induct_tac n)
-apply (tactic {* ALLGOALS (CLASIMPSET' clarsimp_tac) *})
+apply (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *})
apply (subgoal_tac "G = mgt_call ` U")
prefer 2
apply (simp add: card_seteq finite_imageI)
--- a/src/HOL/Int.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/Int.thy Mon Mar 23 08:16:24 2009 +0100
@@ -1256,14 +1256,14 @@
by (simp add: algebra_simps diff_number_of_eq [symmetric])
+
+
subsection {* The Set of Integers *}
context ring_1
begin
-definition
- Ints :: "'a set"
-where
+definition Ints :: "'a set" where
[code del]: "Ints = range of_int"
end
@@ -1854,7 +1854,7 @@
qed
-subsection{*Integer Powers*}
+subsection {* Integer Powers *}
instantiation int :: recpower
begin
@@ -1896,6 +1896,161 @@
lemmas zpower_int = int_power [symmetric]
+
+subsection {* Further theorems on numerals *}
+
+subsubsection{*Special Simplification for Constants*}
+
+text{*These distributive laws move literals inside sums and differences.*}
+
+lemmas left_distrib_number_of [simp] =
+ left_distrib [of _ _ "number_of v", standard]
+
+lemmas right_distrib_number_of [simp] =
+ right_distrib [of "number_of v", standard]
+
+lemmas left_diff_distrib_number_of [simp] =
+ left_diff_distrib [of _ _ "number_of v", standard]
+
+lemmas right_diff_distrib_number_of [simp] =
+ right_diff_distrib [of "number_of v", standard]
+
+text{*These are actually for fields, like real: but where else to put them?*}
+
+lemmas zero_less_divide_iff_number_of [simp, noatp] =
+ zero_less_divide_iff [of "number_of w", standard]
+
+lemmas divide_less_0_iff_number_of [simp, noatp] =
+ divide_less_0_iff [of "number_of w", standard]
+
+lemmas zero_le_divide_iff_number_of [simp, noatp] =
+ zero_le_divide_iff [of "number_of w", standard]
+
+lemmas divide_le_0_iff_number_of [simp, noatp] =
+ divide_le_0_iff [of "number_of w", standard]
+
+
+text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}. It looks
+ strange, but then other simprocs simplify the quotient.*}
+
+lemmas inverse_eq_divide_number_of [simp] =
+ inverse_eq_divide [of "number_of w", standard]
+
+text {*These laws simplify inequalities, moving unary minus from a term
+into the literal.*}
+
+lemmas less_minus_iff_number_of [simp, noatp] =
+ less_minus_iff [of "number_of v", standard]
+
+lemmas le_minus_iff_number_of [simp, noatp] =
+ le_minus_iff [of "number_of v", standard]
+
+lemmas equation_minus_iff_number_of [simp, noatp] =
+ equation_minus_iff [of "number_of v", standard]
+
+lemmas minus_less_iff_number_of [simp, noatp] =
+ minus_less_iff [of _ "number_of v", standard]
+
+lemmas minus_le_iff_number_of [simp, noatp] =
+ minus_le_iff [of _ "number_of v", standard]
+
+lemmas minus_equation_iff_number_of [simp, noatp] =
+ minus_equation_iff [of _ "number_of v", standard]
+
+
+text{*To Simplify Inequalities Where One Side is the Constant 1*}
+
+lemma less_minus_iff_1 [simp,noatp]:
+ fixes b::"'b::{ordered_idom,number_ring}"
+ shows "(1 < - b) = (b < -1)"
+by auto
+
+lemma le_minus_iff_1 [simp,noatp]:
+ fixes b::"'b::{ordered_idom,number_ring}"
+ shows "(1 \<le> - b) = (b \<le> -1)"
+by auto
+
+lemma equation_minus_iff_1 [simp,noatp]:
+ fixes b::"'b::number_ring"
+ shows "(1 = - b) = (b = -1)"
+by (subst equation_minus_iff, auto)
+
+lemma minus_less_iff_1 [simp,noatp]:
+ fixes a::"'b::{ordered_idom,number_ring}"
+ shows "(- a < 1) = (-1 < a)"
+by auto
+
+lemma minus_le_iff_1 [simp,noatp]:
+ fixes a::"'b::{ordered_idom,number_ring}"
+ shows "(- a \<le> 1) = (-1 \<le> a)"
+by auto
+
+lemma minus_equation_iff_1 [simp,noatp]:
+ fixes a::"'b::number_ring"
+ shows "(- a = 1) = (a = -1)"
+by (subst minus_equation_iff, auto)
+
+
+text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
+
+lemmas mult_less_cancel_left_number_of [simp, noatp] =
+ mult_less_cancel_left [of "number_of v", standard]
+
+lemmas mult_less_cancel_right_number_of [simp, noatp] =
+ mult_less_cancel_right [of _ "number_of v", standard]
+
+lemmas mult_le_cancel_left_number_of [simp, noatp] =
+ mult_le_cancel_left [of "number_of v", standard]
+
+lemmas mult_le_cancel_right_number_of [simp, noatp] =
+ mult_le_cancel_right [of _ "number_of v", standard]
+
+
+text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
+
+lemmas le_divide_eq_number_of1 [simp] = le_divide_eq [of _ _ "number_of w", standard]
+lemmas divide_le_eq_number_of1 [simp] = divide_le_eq [of _ "number_of w", standard]
+lemmas less_divide_eq_number_of1 [simp] = less_divide_eq [of _ _ "number_of w", standard]
+lemmas divide_less_eq_number_of1 [simp] = divide_less_eq [of _ "number_of w", standard]
+lemmas eq_divide_eq_number_of1 [simp] = eq_divide_eq [of _ _ "number_of w", standard]
+lemmas divide_eq_eq_number_of1 [simp] = divide_eq_eq [of _ "number_of w", standard]
+
+
+subsubsection{*Optional Simplification Rules Involving Constants*}
+
+text{*Simplify quotients that are compared with a literal constant.*}
+
+lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w", standard]
+lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w", standard]
+lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w", standard]
+lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w", standard]
+lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w", standard]
+lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w", standard]
+
+
+text{*Not good as automatic simprules because they cause case splits.*}
+lemmas divide_const_simps =
+ le_divide_eq_number_of divide_le_eq_number_of less_divide_eq_number_of
+ divide_less_eq_number_of eq_divide_eq_number_of divide_eq_eq_number_of
+ le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
+
+text{*Division By @{text "-1"}*}
+
+lemma divide_minus1 [simp]:
+ "x/-1 = -(x::'a::{field,division_by_zero,number_ring})"
+by simp
+
+lemma minus1_divide [simp]:
+ "-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)"
+by (simp add: divide_inverse inverse_minus_eq)
+
+lemma half_gt_zero_iff:
+ "(0 < r/2) = (0 < (r::'a::{ordered_field,division_by_zero,number_ring}))"
+by auto
+
+lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2, standard]
+
+
subsection {* Configuration of the code generator *}
code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int"
--- a/src/HOL/IntDiv.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/IntDiv.thy Mon Mar 23 08:16:24 2009 +0100
@@ -8,6 +8,10 @@
theory IntDiv
imports Int Divides FunDef
+uses
+ "~~/src/Provers/Arith/cancel_numeral_factor.ML"
+ "~~/src/Provers/Arith/extract_common_term.ML"
+ ("Tools/int_factor_simprocs.ML")
begin
definition divmod_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" where
@@ -920,9 +924,10 @@
next
assume "a\<noteq>0" and le_a: "0\<le>a"
hence a_pos: "1 \<le> a" by arith
- hence one_less_a2: "1 < 2*a" by arith
+ hence one_less_a2: "1 < 2 * a" by arith
hence le_2a: "2 * (1 + b mod a) \<le> 2 * a"
- by (simp add: mult_le_cancel_left add_commute [of 1] add1_zle_eq)
+ unfolding mult_le_cancel_left
+ by (simp add: add1_zle_eq add_commute [of 1])
with a_pos have "0 \<le> b mod a" by simp
hence le_addm: "0 \<le> 1 mod (2*a) + 2*(b mod a)"
by (simp add: mod_pos_pos_trivial one_less_a2)
@@ -1357,6 +1362,11 @@
qed
+subsection {* Simproc setup *}
+
+use "Tools/int_factor_simprocs.ML"
+
+
subsection {* Code generation *}
definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
--- a/src/HOL/IsaMakefile Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/IsaMakefile Mon Mar 23 08:16:24 2009 +0100
@@ -204,7 +204,6 @@
@$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
- Arith_Tools.thy \
ATP_Linkup.thy \
Code_Eval.thy \
Code_Message.thy \
--- a/src/HOL/Library/Euclidean_Space.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/Library/Euclidean_Space.thy Mon Mar 23 08:16:24 2009 +0100
@@ -6,8 +6,9 @@
theory Euclidean_Space
imports
- Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
- Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type Inner_Product
+ Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
+ Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type
+ Inner_Product
uses ("normarith.ML")
begin
--- a/src/HOL/Library/Topology_Euclidean_Space.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy Mon Mar 23 08:16:24 2009 +0100
@@ -6,10 +6,9 @@
header {* Elementary topology in Euclidean space. *}
theory Topology_Euclidean_Space
- imports SEQ Euclidean_Space
+imports SEQ Euclidean_Space
begin
-
declare fstcart_pastecart[simp] sndcart_pastecart[simp]
subsection{* General notion of a topology *}
@@ -474,7 +473,7 @@
have th0: "\<And>d x y z. (d x z :: real) <= d x y + d y z \<Longrightarrow> d y z = d z y
==> ~(d x y * 2 < d x z \<and> d z y * 2 < d x z)" by arith
have "?P ?U ?V" using dist_pos_lt[OF xy] th0[of dist,OF dist_triangle dist_sym]
- by (auto simp add: dist_refl expand_set_eq Arith_Tools.less_divide_eq_number_of1)
+ by (auto simp add: dist_refl expand_set_eq less_divide_eq_number_of1)
then show ?thesis by blast
qed
@@ -662,7 +661,7 @@
have "?k/2 \<ge> 0" using kp by simp
then obtain w where w: "dist y w = ?k/ 2" by (metis vector_choose_dist)
from iT[unfolded expand_set_eq mem_interior]
- have "\<not> ball w (?k/4) \<subseteq> T" using kp by (auto simp add: Arith_Tools.less_divide_eq_number_of1)
+ have "\<not> ball w (?k/4) \<subseteq> T" using kp by (auto simp add: less_divide_eq_number_of1)
then obtain z where z: "dist w z < ?k/4" "z \<notin> T" by (auto simp add: subset_eq)
have "z \<notin> T \<and> z\<noteq> y \<and> dist z y < d \<and> dist x z < e" using z apply simp
using w e(1) d apply (auto simp only: dist_sym)
@@ -1323,7 +1322,7 @@
assume "e>0"
hence *:"eventually (\<lambda>x. dist (f x) l < e/2) net"
"eventually (\<lambda>x. dist (g x) m < e/2) net" using as
- by (auto intro: tendstoD simp del: Arith_Tools.less_divide_eq_number_of1)
+ by (auto intro: tendstoD simp del: less_divide_eq_number_of1)
hence "eventually (\<lambda>x. dist (f x + g x) (l + m) < e) net"
proof(cases "trivial_limit net")
case True
@@ -1494,8 +1493,7 @@
have thy: "norm (y' - y) * norm x' < e / (2 * norm x + 2 * norm y + 2) * (1 + norm x)"
using mult_strict_mono'[OF h(4) * norm_ge_zero norm_ge_zero] by auto
also have "\<dots> \<le> e/2" apply simp unfolding divide_le_eq
- using th1 th0 `e>0` apply auto
- unfolding mult_assoc and real_mult_le_cancel_iff2[OF `e>0`] by auto
+ using th1 th0 `e>0` by auto
finally have "norm x' * norm (y' - y) + norm (x' - x) * norm y < e"
using thx and e by (simp add: field_simps) }
@@ -3558,7 +3556,7 @@
{ fix y assume "dist y (c *s x) < e * \<bar>c\<bar>"
hence "norm ((1 / c) *s y - x) < e" unfolding dist_def
using norm_mul[of c "(1 / c) *s y - x", unfolded vector_ssub_ldistrib, unfolded vector_smult_assoc] assms(1)
- mult_less_imp_less_left[of "abs c" "norm ((1 / c) *s y - x)" e, unfolded real_mult_commute[of "abs c" e]] assms(1)[unfolded zero_less_abs_iff[THEN sym]] by simp
+ assms(1)[unfolded zero_less_abs_iff[THEN sym]] by (simp del:zero_less_abs_iff)
hence "y \<in> op *s c ` s" using rev_image_eqI[of "(1 / c) *s y" s y "op *s c"] e[THEN spec[where x="(1 / c) *s y"]] assms(1) unfolding dist_def vector_smult_assoc by auto }
ultimately have "\<exists>e>0. \<forall>x'. dist x' (c *s x) < e \<longrightarrow> x' \<in> op *s c ` s" apply(rule_tac x="e * abs c" in exI) by auto }
thus ?thesis unfolding open_def by auto
@@ -3957,7 +3955,7 @@
hence fx0:"f x \<noteq> 0" using `l \<noteq> 0` by auto
hence fxl0: "(f x) * l \<noteq> 0" using `l \<noteq> 0` by auto
from * have **:"\<bar>f x - l\<bar> < l\<twosuperior> * e / 2" by auto
- have "\<bar>f x\<bar> * 2 \<ge> \<bar>l\<bar>" using * by (auto simp del: Arith_Tools.less_divide_eq_number_of1)
+ have "\<bar>f x\<bar> * 2 \<ge> \<bar>l\<bar>" using * by (auto simp del: less_divide_eq_number_of1)
hence "\<bar>f x\<bar> * 2 * \<bar>l\<bar> \<ge> \<bar>l\<bar> * \<bar>l\<bar>" unfolding mult_le_cancel_right by auto
hence "\<bar>f x * l\<bar> * 2 \<ge> \<bar>l\<bar>^2" unfolding real_mult_commute and power2_eq_square by auto
hence ***:"inverse \<bar>f x * l\<bar> \<le> inverse (l\<twosuperior> / 2)" using fxl0
@@ -4319,7 +4317,7 @@
have "a$i < b$i" using as[THEN spec[where x=i]] by auto
hence "a$i < ((1/2) *s (a+b)) $ i" "((1/2) *s (a+b)) $ i < b$i"
unfolding vector_smult_component and vector_add_component
- by (auto simp add: Arith_Tools.less_divide_eq_number_of1) }
+ by (auto simp add: less_divide_eq_number_of1) }
hence "{a <..< b} \<noteq> {}" using mem_interval(1)[of "?x" a b] by auto }
ultimately show ?th1 by blast
@@ -4334,7 +4332,7 @@
have "a$i \<le> b$i" using as[THEN spec[where x=i]] by auto
hence "a$i \<le> ((1/2) *s (a+b)) $ i" "((1/2) *s (a+b)) $ i \<le> b$i"
unfolding vector_smult_component and vector_add_component
- by (auto simp add: Arith_Tools.less_divide_eq_number_of1) }
+ by (auto simp add: less_divide_eq_number_of1) }
hence "{a .. b} \<noteq> {}" using mem_interval(2)[of "?x" a b] by auto }
ultimately show ?th2 by blast
qed
@@ -4398,13 +4396,13 @@
{ fix j
have "c $ j < ?x $ j \<and> ?x $ j < d $ j" unfolding Cart_lambda_beta
apply(cases "j=i") using as(2)[THEN spec[where x=j]]
- by (auto simp add: Arith_Tools.less_divide_eq_number_of1 as2) }
+ by (auto simp add: less_divide_eq_number_of1 as2) }
hence "?x\<in>{c<..<d}" unfolding mem_interval by auto
moreover
have "?x\<notin>{a .. b}"
unfolding mem_interval apply auto apply(rule_tac x=i in exI)
using as(2)[THEN spec[where x=i]] and as2
- by (auto simp add: Arith_Tools.less_divide_eq_number_of1)
+ by (auto simp add: less_divide_eq_number_of1)
ultimately have False using as by auto }
hence "a$i \<le> c$i" by(rule ccontr)auto
moreover
@@ -4413,13 +4411,13 @@
{ fix j
have "d $ j > ?x $ j \<and> ?x $ j > c $ j" unfolding Cart_lambda_beta
apply(cases "j=i") using as(2)[THEN spec[where x=j]]
- by (auto simp add: Arith_Tools.less_divide_eq_number_of1 as2) }
+ by (auto simp add: less_divide_eq_number_of1 as2) }
hence "?x\<in>{c<..<d}" unfolding mem_interval by auto
moreover
have "?x\<notin>{a .. b}"
unfolding mem_interval apply auto apply(rule_tac x=i in exI)
using as(2)[THEN spec[where x=i]] and as2
- by (auto simp add: Arith_Tools.less_divide_eq_number_of1)
+ by (auto simp add: less_divide_eq_number_of1)
ultimately have False using as by auto }
hence "b$i \<ge> d$i" by(rule ccontr)auto
ultimately
@@ -4450,7 +4448,7 @@
lemma inter_interval: fixes a :: "'a::linorder^'n::finite" shows
"{a .. b} \<inter> {c .. d} = {(\<chi> i. max (a$i) (c$i)) .. (\<chi> i. min (b$i) (d$i))}"
unfolding expand_set_eq and Int_iff and mem_interval
- by (auto simp add: Arith_Tools.less_divide_eq_number_of1 intro!: bexI)
+ by (auto simp add: less_divide_eq_number_of1 intro!: bexI)
(* Moved interval_open_subset_closed a bit upwards *)
@@ -4565,7 +4563,7 @@
have "a $ i < ((1 / 2) *s (a + b)) $ i \<and> ((1 / 2) *s (a + b)) $ i < b $ i"
using assms[unfolded interval_ne_empty, THEN spec[where x=i]]
unfolding vector_smult_component and vector_add_component
- by(auto simp add: Arith_Tools.less_divide_eq_number_of1) }
+ by(auto simp add: less_divide_eq_number_of1) }
thus ?thesis unfolding mem_interval by auto
qed
@@ -5633,7 +5631,7 @@
{ assume as:"dist a b > dist (f n x) (f n y)"
then obtain Na Nb where "\<forall>m\<ge>Na. dist (f (r m) x) a < (dist a b - dist (f n x) (f n y)) / 2"
and "\<forall>m\<ge>Nb. dist (f (r m) y) b < (dist a b - dist (f n x) (f n y)) / 2"
- using lima limb unfolding h_def Lim_sequentially by (fastsimp simp del: Arith_Tools.less_divide_eq_number_of1)
+ using lima limb unfolding h_def Lim_sequentially by (fastsimp simp del: less_divide_eq_number_of1)
hence "dist (f (r (Na + Nb + n)) x - f (r (Na + Nb + n)) y) (a - b) < dist a b - dist (f n x) (f n y)"
apply(erule_tac x="Na+Nb+n" in allE)
apply(erule_tac x="Na+Nb+n" in allE) apply simp
--- a/src/HOL/Modelcheck/mucke_oracle.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Mon Mar 23 08:16:24 2009 +0100
@@ -109,7 +109,7 @@
(
OldGoals.push_proof();
OldGoals.goalw_cterm [] (cterm_of sign trm);
-by (SIMPSET' simp_tac 1);
+by (simp_tac (simpset_of sign) 1);
let
val if_tmp_result = result()
in
--- a/src/HOL/NatBin.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/NatBin.thy Mon Mar 23 08:16:24 2009 +0100
@@ -7,6 +7,7 @@
theory NatBin
imports IntDiv
+uses ("Tools/nat_simprocs.ML")
begin
text {*
@@ -40,9 +41,7 @@
subsection {* Predicate for negative binary numbers *}
-definition
- neg :: "int \<Rightarrow> bool"
-where
+definition neg :: "int \<Rightarrow> bool" where
"neg Z \<longleftrightarrow> Z < 0"
lemma not_neg_int [simp]: "~ neg (of_nat n)"
@@ -818,4 +817,159 @@
"(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
by (simp add: nat_mult_div_cancel1)
+
+subsection {* Simprocs for the Naturals *}
+
+use "Tools/nat_simprocs.ML"
+declaration {* K nat_simprocs_setup *}
+
+subsubsection{*For simplifying @{term "Suc m - K"} and @{term "K - Suc m"}*}
+
+text{*Where K above is a literal*}
+
+lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"
+by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split)
+
+text {*Now just instantiating @{text n} to @{text "number_of v"} does
+ the right simplification, but with some redundant inequality
+ tests.*}
+lemma neg_number_of_pred_iff_0:
+ "neg (number_of (Int.pred v)::int) = (number_of v = (0::nat))"
+apply (subgoal_tac "neg (number_of (Int.pred v)) = (number_of v < Suc 0) ")
+apply (simp only: less_Suc_eq_le le_0_eq)
+apply (subst less_number_of_Suc, simp)
+done
+
+text{*No longer required as a simprule because of the @{text inverse_fold}
+ simproc*}
+lemma Suc_diff_number_of:
+ "Int.Pls < v ==>
+ Suc m - (number_of v) = m - (number_of (Int.pred v))"
+apply (subst Suc_diff_eq_diff_pred)
+apply simp
+apply (simp del: nat_numeral_1_eq_1)
+apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric]
+ neg_number_of_pred_iff_0)
+done
+
+lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
+by (simp add: numerals split add: nat_diff_split)
+
+
+subsubsection{*For @{term nat_case} and @{term nat_rec}*}
+
+lemma nat_case_number_of [simp]:
+ "nat_case a f (number_of v) =
+ (let pv = number_of (Int.pred v) in
+ if neg pv then a else f (nat pv))"
+by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0)
+
+lemma nat_case_add_eq_if [simp]:
+ "nat_case a f ((number_of v) + n) =
+ (let pv = number_of (Int.pred v) in
+ if neg pv then nat_case a f n else f (nat pv + n))"
+apply (subst add_eq_if)
+apply (simp split add: nat.split
+ del: nat_numeral_1_eq_1
+ add: nat_numeral_1_eq_1 [symmetric]
+ numeral_1_eq_Suc_0 [symmetric]
+ neg_number_of_pred_iff_0)
+done
+
+lemma nat_rec_number_of [simp]:
+ "nat_rec a f (number_of v) =
+ (let pv = number_of (Int.pred v) in
+ if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"
+apply (case_tac " (number_of v) ::nat")
+apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0)
+apply (simp split add: split_if_asm)
+done
+
+lemma nat_rec_add_eq_if [simp]:
+ "nat_rec a f (number_of v + n) =
+ (let pv = number_of (Int.pred v) in
+ if neg pv then nat_rec a f n
+ else f (nat pv + n) (nat_rec a f (nat pv + n)))"
+apply (subst add_eq_if)
+apply (simp split add: nat.split
+ del: nat_numeral_1_eq_1
+ add: nat_numeral_1_eq_1 [symmetric]
+ numeral_1_eq_Suc_0 [symmetric]
+ neg_number_of_pred_iff_0)
+done
+
+
+subsubsection{*Various Other Lemmas*}
+
+text {*Evens and Odds, for Mutilated Chess Board*}
+
+text{*Lemmas for specialist use, NOT as default simprules*}
+lemma nat_mult_2: "2 * z = (z+z::nat)"
+proof -
+ have "2*z = (1 + 1)*z" by simp
+ also have "... = z+z" by (simp add: left_distrib)
+ finally show ?thesis .
+qed
+
+lemma nat_mult_2_right: "z * 2 = (z+z::nat)"
+by (subst mult_commute, rule nat_mult_2)
+
+text{*Case analysis on @{term "n<2"}*}
+lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
+by arith
+
+lemma div2_Suc_Suc [simp]: "Suc(Suc m) div 2 = Suc (m div 2)"
+by arith
+
+lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
+by (simp add: nat_mult_2 [symmetric])
+
+lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2"
+apply (subgoal_tac "m mod 2 < 2")
+apply (erule less_2_cases [THEN disjE])
+apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1)
+done
+
+lemma mod2_gr_0 [simp]: "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)"
+apply (subgoal_tac "m mod 2 < 2")
+apply (force simp del: mod_less_divisor, simp)
+done
+
+text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*}
+
+lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
+by simp
+
+lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"
+by simp
+
+text{*Can be used to eliminate long strings of Sucs, but not by default*}
+lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
+by simp
+
+
+text{*These lemmas collapse some needless occurrences of Suc:
+ at least three Sucs, since two and fewer are rewritten back to Suc again!
+ We already have some rules to simplify operands smaller than 3.*}
+
+lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
+by (simp add: Suc3_eq_add_3)
+
+lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
+by (simp add: Suc3_eq_add_3)
+
+lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
+by (simp add: Suc3_eq_add_3)
+
+lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
+by (simp add: Suc3_eq_add_3)
+
+lemmas Suc_div_eq_add3_div_number_of =
+ Suc_div_eq_add3_div [of _ "number_of v", standard]
+declare Suc_div_eq_add3_div_number_of [simp]
+
+lemmas Suc_mod_eq_add3_mod_number_of =
+ Suc_mod_eq_add3_mod [of _ "number_of v", standard]
+declare Suc_mod_eq_add3_mod_number_of [simp]
+
end
--- a/src/HOL/OrderedGroup.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/OrderedGroup.thy Mon Mar 23 08:16:24 2009 +0100
@@ -316,6 +316,9 @@
lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
by (simp add: algebra_simps)
+lemma diff_eq_0_iff_eq [simp, noatp]: "a - b = 0 \<longleftrightarrow> a = b"
+by (simp add: algebra_simps)
+
end
subsection {* (Partially) Ordered Groups *}
@@ -1296,7 +1299,7 @@
done
lemma eq_eqI: "(x::'a::ab_group_add) - y = x' - y' \<Longrightarrow> (x = y) = (x' = y')"
-by (simp add: eq_iff_diff_eq_0[of x y] eq_iff_diff_eq_0[of x' y'])
+by (simp only: eq_iff_diff_eq_0[of x y] eq_iff_diff_eq_0[of x' y'])
lemma diff_def: "(x::'a::ab_group_add) - y == x + (-y)"
by (simp add: diff_minus)
@@ -1344,7 +1347,6 @@
text{*Simplification of @{term "x-y < 0"}, etc.*}
lemmas diff_less_0_iff_less [simp, noatp] = less_iff_diff_less_0 [symmetric]
-lemmas diff_eq_0_iff_eq [simp, noatp] = eq_iff_diff_eq_0 [symmetric]
lemmas diff_le_0_iff_le [simp, noatp] = le_iff_diff_le_0 [symmetric]
ML {*
--- a/src/HOL/Presburger.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/Presburger.thy Mon Mar 23 08:16:24 2009 +0100
@@ -7,6 +7,7 @@
theory Presburger
imports Groebner_Basis SetInterval
uses
+ "Tools/Qelim/qelim.ML"
"Tools/Qelim/cooper_data.ML"
"Tools/Qelim/generated_cooper.ML"
("Tools/Qelim/cooper.ML")
--- a/src/HOL/Rational.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/Rational.thy Mon Mar 23 08:16:24 2009 +0100
@@ -691,7 +691,6 @@
\<longleftrightarrow> Fract a b < Fract c d"
using not_zero `b * d > 0`
by (simp add: of_rat_rat of_int_divide_less_eq of_int_mult [symmetric] del: of_int_mult)
- (auto intro: mult_strict_right_mono mult_right_less_imp_less)
qed
lemma of_rat_less_eq:
--- a/src/HOL/Ring_and_Field.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/Ring_and_Field.thy Mon Mar 23 08:16:24 2009 +0100
@@ -534,7 +534,156 @@
by (simp add: divide_inverse)
lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
-by (simp add: divide_inverse algebra_simps)
+by (simp add: divide_inverse algebra_simps)
+
+text{*There is no slick version using division by zero.*}
+lemma inverse_add:
+ "[| a \<noteq> 0; b \<noteq> 0 |]
+ ==> inverse a + inverse b = (a + b) * inverse a * inverse b"
+by (simp add: division_ring_inverse_add mult_ac)
+
+lemma nonzero_mult_divide_mult_cancel_left [simp, noatp]:
+assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/b"
+proof -
+ have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
+ by (simp add: divide_inverse nonzero_inverse_mult_distrib)
+ also have "... = a * inverse b * (inverse c * c)"
+ by (simp only: mult_ac)
+ also have "... = a * inverse b" by simp
+ finally show ?thesis by (simp add: divide_inverse)
+qed
+
+lemma nonzero_mult_divide_mult_cancel_right [simp, noatp]:
+ "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (b * c) = a / b"
+by (simp add: mult_commute [of _ c])
+
+lemma divide_1 [simp]: "a / 1 = a"
+by (simp add: divide_inverse)
+
+lemma times_divide_eq_right: "a * (b / c) = (a * b) / c"
+by (simp add: divide_inverse mult_assoc)
+
+lemma times_divide_eq_left: "(b / c) * a = (b * a) / c"
+by (simp add: divide_inverse mult_ac)
+
+text {* These are later declared as simp rules. *}
+lemmas times_divide_eq [noatp] = times_divide_eq_right times_divide_eq_left
+
+lemma add_frac_eq:
+ assumes "y \<noteq> 0" and "z \<noteq> 0"
+ shows "x / y + w / z = (x * z + w * y) / (y * z)"
+proof -
+ have "x / y + w / z = (x * z) / (y * z) + (y * w) / (y * z)"
+ using assms by simp
+ also have "\<dots> = (x * z + y * w) / (y * z)"
+ by (simp only: add_divide_distrib)
+ finally show ?thesis
+ by (simp only: mult_commute)
+qed
+
+text{*Special Cancellation Simprules for Division*}
+
+lemma nonzero_mult_divide_cancel_right [simp, noatp]:
+ "b \<noteq> 0 \<Longrightarrow> a * b / b = a"
+using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp
+
+lemma nonzero_mult_divide_cancel_left [simp, noatp]:
+ "a \<noteq> 0 \<Longrightarrow> a * b / a = b"
+using nonzero_mult_divide_mult_cancel_left [of 1 a b] by simp
+
+lemma nonzero_divide_mult_cancel_right [simp, noatp]:
+ "\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> b / (a * b) = 1 / a"
+using nonzero_mult_divide_mult_cancel_right [of a b 1] by simp
+
+lemma nonzero_divide_mult_cancel_left [simp, noatp]:
+ "\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / (a * b) = 1 / b"
+using nonzero_mult_divide_mult_cancel_left [of b a 1] by simp
+
+lemma nonzero_mult_divide_mult_cancel_left2 [simp, noatp]:
+ "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (c * a) / (b * c) = a / b"
+using nonzero_mult_divide_mult_cancel_left [of b c a] by (simp add: mult_ac)
+
+lemma nonzero_mult_divide_mult_cancel_right2 [simp, noatp]:
+ "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (c * b) = a / b"
+using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: mult_ac)
+
+lemma minus_divide_left: "- (a / b) = (-a) / b"
+by (simp add: divide_inverse)
+
+lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a / b) = a / (- b)"
+by (simp add: divide_inverse nonzero_inverse_minus_eq)
+
+lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"
+by (simp add: divide_inverse nonzero_inverse_minus_eq)
+
+lemma divide_minus_left [simp, noatp]: "(-a) / b = - (a / b)"
+by (simp add: divide_inverse)
+
+lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
+by (simp add: diff_minus add_divide_distrib)
+
+lemma add_divide_eq_iff:
+ "z \<noteq> 0 \<Longrightarrow> x + y / z = (z * x + y) / z"
+by (simp add: add_divide_distrib)
+
+lemma divide_add_eq_iff:
+ "z \<noteq> 0 \<Longrightarrow> x / z + y = (x + z * y) / z"
+by (simp add: add_divide_distrib)
+
+lemma diff_divide_eq_iff:
+ "z \<noteq> 0 \<Longrightarrow> x - y / z = (z * x - y) / z"
+by (simp add: diff_divide_distrib)
+
+lemma divide_diff_eq_iff:
+ "z \<noteq> 0 \<Longrightarrow> x / z - y = (x - z * y) / z"
+by (simp add: diff_divide_distrib)
+
+lemma nonzero_eq_divide_eq: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"
+proof -
+ assume [simp]: "c \<noteq> 0"
+ have "a = b / c \<longleftrightarrow> a * c = (b / c) * c" by simp
+ also have "... \<longleftrightarrow> a * c = b" by (simp add: divide_inverse mult_assoc)
+ finally show ?thesis .
+qed
+
+lemma nonzero_divide_eq_eq: "c \<noteq> 0 \<Longrightarrow> b / c = a \<longleftrightarrow> b = a * c"
+proof -
+ assume [simp]: "c \<noteq> 0"
+ have "b / c = a \<longleftrightarrow> (b / c) * c = a * c" by simp
+ also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult_assoc)
+ finally show ?thesis .
+qed
+
+lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a"
+by simp
+
+lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"
+by (erule subst, simp)
+
+lemmas field_eq_simps[noatp] = algebra_simps
+ (* pull / out*)
+ add_divide_eq_iff divide_add_eq_iff
+ diff_divide_eq_iff divide_diff_eq_iff
+ (* multiply eqn *)
+ nonzero_eq_divide_eq nonzero_divide_eq_eq
+(* is added later:
+ times_divide_eq_left times_divide_eq_right
+*)
+
+text{*An example:*}
+lemma "\<lbrakk>a\<noteq>b; c\<noteq>d; e\<noteq>f\<rbrakk> \<Longrightarrow> ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) = 1"
+apply(subgoal_tac "(c-d)*(e-f)*(a-b) \<noteq> 0")
+ apply(simp add:field_eq_simps)
+apply(simp)
+done
+
+lemma diff_frac_eq:
+ "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y - w / z = (x * z - w * y) / (y * z)"
+by (simp add: field_eq_simps times_divide_eq)
+
+lemma frac_eq_eq:
+ "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (x / y = w / z) = (x * z = w * y)"
+by (simp add: field_eq_simps times_divide_eq)
end
@@ -987,6 +1136,27 @@
"c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
by (simp add: not_less [symmetric] mult_less_cancel_left_disj)
+lemma mult_le_cancel_left_pos:
+ "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b"
+by (auto simp: mult_le_cancel_left)
+
+lemma mult_le_cancel_left_neg:
+ "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a"
+by (auto simp: mult_le_cancel_left)
+
+end
+
+context ordered_ring_strict
+begin
+
+lemma mult_less_cancel_left_pos:
+ "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b"
+by (auto simp: mult_less_cancel_left)
+
+lemma mult_less_cancel_left_neg:
+ "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"
+by (auto simp: mult_less_cancel_left)
+
end
text{*Legacy - use @{text algebra_simps} *}
@@ -1191,12 +1361,6 @@
thus ?thesis by force
qed
-text{*There is no slick version using division by zero.*}
-lemma inverse_add:
- "[|a \<noteq> 0; b \<noteq> 0|]
- ==> inverse a + inverse b = (a+b) * inverse a * inverse (b::'a::field)"
-by (simp add: division_ring_inverse_add mult_ac)
-
lemma inverse_divide [simp]:
"inverse (a/b) = b / (a::'a::{field,division_by_zero})"
by (simp add: divide_inverse mult_commute)
@@ -1208,44 +1372,18 @@
field} but none for class @{text field} and @{text nonzero_divides}
because the latter are covered by a simproc. *}
-lemma nonzero_mult_divide_mult_cancel_left[simp,noatp]:
-assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/(b::'a::field)"
-proof -
- have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
- by (simp add: divide_inverse nonzero_inverse_mult_distrib)
- also have "... = a * inverse b * (inverse c * c)"
- by (simp only: mult_ac)
- also have "... = a * inverse b" by simp
- finally show ?thesis by (simp add: divide_inverse)
-qed
-
lemma mult_divide_mult_cancel_left:
"c\<noteq>0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})"
apply (cases "b = 0")
apply (simp_all add: nonzero_mult_divide_mult_cancel_left)
done
-lemma nonzero_mult_divide_mult_cancel_right [noatp]:
- "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (b*c) = a/(b::'a::field)"
-by (simp add: mult_commute [of _ c] nonzero_mult_divide_mult_cancel_left)
-
lemma mult_divide_mult_cancel_right:
"c\<noteq>0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})"
apply (cases "b = 0")
apply (simp_all add: nonzero_mult_divide_mult_cancel_right)
done
-lemma divide_1 [simp]: "a/1 = (a::'a::field)"
-by (simp add: divide_inverse)
-
-lemma times_divide_eq_right: "a * (b/c) = (a*b) / (c::'a::field)"
-by (simp add: divide_inverse mult_assoc)
-
-lemma times_divide_eq_left: "(b/c) * a = (b*a) / (c::'a::field)"
-by (simp add: divide_inverse mult_ac)
-
-lemmas times_divide_eq[noatp] = times_divide_eq_right times_divide_eq_left
-
lemma divide_divide_eq_right [simp,noatp]:
"a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
by (simp add: divide_inverse mult_ac)
@@ -1254,20 +1392,6 @@
"(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
by (simp add: divide_inverse mult_assoc)
-lemma add_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
- x / y + w / z = (x * z + w * y) / (y * z)"
-apply (subgoal_tac "x / y = (x * z) / (y * z)")
-apply (erule ssubst)
-apply (subgoal_tac "w / z = (w * y) / (y * z)")
-apply (erule ssubst)
-apply (rule add_divide_distrib [THEN sym])
-apply (subst mult_commute)
-apply (erule nonzero_mult_divide_mult_cancel_left [THEN sym])
-apply assumption
-apply (erule nonzero_mult_divide_mult_cancel_right [THEN sym])
-apply assumption
-done
-
subsubsection{*Special Cancellation Simprules for Division*}
@@ -1276,140 +1400,29 @@
shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"
by (simp add: mult_divide_mult_cancel_left)
-lemma nonzero_mult_divide_cancel_right[simp,noatp]:
- "b \<noteq> 0 \<Longrightarrow> a * b / b = (a::'a::field)"
-using nonzero_mult_divide_mult_cancel_right[of 1 b a] by simp
-
-lemma nonzero_mult_divide_cancel_left[simp,noatp]:
- "a \<noteq> 0 \<Longrightarrow> a * b / a = (b::'a::field)"
-using nonzero_mult_divide_mult_cancel_left[of 1 a b] by simp
-
-
-lemma nonzero_divide_mult_cancel_right[simp,noatp]:
- "\<lbrakk> a\<noteq>0; b\<noteq>0 \<rbrakk> \<Longrightarrow> b / (a * b) = 1/(a::'a::field)"
-using nonzero_mult_divide_mult_cancel_right[of a b 1] by simp
-
-lemma nonzero_divide_mult_cancel_left[simp,noatp]:
- "\<lbrakk> a\<noteq>0; b\<noteq>0 \<rbrakk> \<Longrightarrow> a / (a * b) = 1/(b::'a::field)"
-using nonzero_mult_divide_mult_cancel_left[of b a 1] by simp
-
-
-lemma nonzero_mult_divide_mult_cancel_left2[simp,noatp]:
- "[|b\<noteq>0; c\<noteq>0|] ==> (c*a) / (b*c) = a/(b::'a::field)"
-using nonzero_mult_divide_mult_cancel_left[of b c a] by(simp add:mult_ac)
-
-lemma nonzero_mult_divide_mult_cancel_right2[simp,noatp]:
- "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (c*b) = a/(b::'a::field)"
-using nonzero_mult_divide_mult_cancel_right[of b c a] by(simp add:mult_ac)
-
subsection {* Division and Unary Minus *}
-lemma nonzero_minus_divide_left: "b \<noteq> 0 ==> - (a/b) = (-a) / (b::'a::field)"
-by (simp add: divide_inverse)
-
-lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a/b) = a / -(b::'a::field)"
-by (simp add: divide_inverse nonzero_inverse_minus_eq)
-
-lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a)/(-b) = a / (b::'a::field)"
-by (simp add: divide_inverse nonzero_inverse_minus_eq)
-
-lemma minus_divide_left: "- (a/b) = (-a) / (b::'a::field)"
-by (simp add: divide_inverse)
-
lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"
by (simp add: divide_inverse)
-
-text{*The effect is to extract signs from divisions*}
-lemmas divide_minus_left[noatp] = minus_divide_left [symmetric]
-lemmas divide_minus_right[noatp] = minus_divide_right [symmetric]
-declare divide_minus_left [simp] divide_minus_right [simp]
-
-lemma minus_divide_divide [simp]:
+lemma divide_minus_right [simp, noatp]:
+ "a / -(b::'a::{field,division_by_zero}) = -(a / b)"
+by (simp add: divide_inverse)
+
+lemma minus_divide_divide:
"(-a)/(-b) = a / (b::'a::{field,division_by_zero})"
apply (cases "b=0", simp)
apply (simp add: nonzero_minus_divide_divide)
done
-lemma diff_divide_distrib: "(a-b)/(c::'a::field) = a/c - b/c"
-by (simp add: diff_minus add_divide_distrib)
-
-lemma add_divide_eq_iff:
- "(z::'a::field) \<noteq> 0 \<Longrightarrow> x + y/z = (z*x + y)/z"
-by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)
-
-lemma divide_add_eq_iff:
- "(z::'a::field) \<noteq> 0 \<Longrightarrow> x/z + y = (x + z*y)/z"
-by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)
-
-lemma diff_divide_eq_iff:
- "(z::'a::field) \<noteq> 0 \<Longrightarrow> x - y/z = (z*x - y)/z"
-by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)
-
-lemma divide_diff_eq_iff:
- "(z::'a::field) \<noteq> 0 \<Longrightarrow> x/z - y = (x - z*y)/z"
-by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)
-
-lemma nonzero_eq_divide_eq: "c\<noteq>0 ==> ((a::'a::field) = b/c) = (a*c = b)"
-proof -
- assume [simp]: "c\<noteq>0"
- have "(a = b/c) = (a*c = (b/c)*c)" by simp
- also have "... = (a*c = b)" by (simp add: divide_inverse mult_assoc)
- finally show ?thesis .
-qed
-
-lemma nonzero_divide_eq_eq: "c\<noteq>0 ==> (b/c = (a::'a::field)) = (b = a*c)"
-proof -
- assume [simp]: "c\<noteq>0"
- have "(b/c = a) = ((b/c)*c = a*c)" by simp
- also have "... = (b = a*c)" by (simp add: divide_inverse mult_assoc)
- finally show ?thesis .
-qed
-
lemma eq_divide_eq:
"((a::'a::{field,division_by_zero}) = b/c) = (if c\<noteq>0 then a*c = b else a=0)"
-by (simp add: nonzero_eq_divide_eq)
+by (simp add: nonzero_eq_divide_eq)
lemma divide_eq_eq:
"(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
-by (force simp add: nonzero_divide_eq_eq)
-
-lemma divide_eq_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>
- b = a * c ==> b / c = a"
-by (subst divide_eq_eq, simp)
-
-lemma eq_divide_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>
- a * c = b ==> a = b / c"
-by (subst eq_divide_eq, simp)
-
-
-lemmas field_eq_simps[noatp] = algebra_simps
- (* pull / out*)
- add_divide_eq_iff divide_add_eq_iff
- diff_divide_eq_iff divide_diff_eq_iff
- (* multiply eqn *)
- nonzero_eq_divide_eq nonzero_divide_eq_eq
-(* is added later:
- times_divide_eq_left times_divide_eq_right
-*)
-
-text{*An example:*}
-lemma fixes a b c d e f :: "'a::field"
-shows "\<lbrakk>a\<noteq>b; c\<noteq>d; e\<noteq>f \<rbrakk> \<Longrightarrow> ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) = 1"
-apply(subgoal_tac "(c-d)*(e-f)*(a-b) \<noteq> 0")
- apply(simp add:field_eq_simps)
-apply(simp)
-done
-
-
-lemma diff_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
- x / y - w / z = (x * z - w * y) / (y * z)"
-by (simp add:field_eq_simps times_divide_eq)
-
-lemma frac_eq_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
- (x / y = w / z) = (x * z = w * y)"
-by (simp add:field_eq_simps times_divide_eq)
+by (force simp add: nonzero_divide_eq_eq)
subsection {* Ordered Fields *}
--- a/src/HOL/SET-Protocol/Cardholder_Registration.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/SET-Protocol/Cardholder_Registration.thy Mon Mar 23 08:16:24 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Auth/SET/Cardholder_Registration
- ID: $Id$
Authors: Giampaolo Bella, Fabio Massacci, Lawrence C Paulson,
Piero Tramontano
*)
@@ -263,7 +262,7 @@
THEN set_cr.SET_CR5 [of concl: C i KC3 NC3 KC2 CardSecret],
THEN Says_to_Gets,
THEN set_cr.SET_CR6 [of concl: i C KC2]])
-apply (tactic "PublicSET.basic_possibility_tac")
+apply basic_possibility
apply (simp_all (no_asm_simp) add: symKeys_neq_imp_neq)
done
--- a/src/HOL/SET-Protocol/MessageSET.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/SET-Protocol/MessageSET.thy Mon Mar 23 08:16:24 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Auth/SET/MessageSET
- ID: $Id$
Authors: Giampaolo Bella, Fabio Massacci, Lawrence C Paulson
*)
@@ -846,9 +845,9 @@
(*Prove base case (subgoal i) and simplify others. A typical base case
concerns Crypt K X \<notin> Key`shrK`bad and cannot be proved by rewriting
alone.*)
-fun prove_simple_subgoals_tac i =
- CLASIMPSET' (fn (cs, ss) => force_tac (cs, ss addsimps [@{thm image_eq_UN}])) i THEN
- ALLGOALS (SIMPSET' asm_simp_tac)
+fun prove_simple_subgoals_tac (cs, ss) i =
+ force_tac (cs, ss addsimps [@{thm image_eq_UN}]) i THEN
+ ALLGOALS (asm_simp_tac ss)
(*Analysis of Fake cases. Also works for messages that forward unknown parts,
but this application is no longer necessary if analz_insert_eq is used.
@@ -873,8 +872,7 @@
(cs addIs [@{thm analz_insertI},
impOfSubs @{thm analz_subset_parts}]) 4 1))
-(*The explicit claset and simpset arguments help it work with Isar*)
-fun gen_spy_analz_tac (cs,ss) i =
+fun spy_analz_tac (cs,ss) i =
DETERM
(SELECT_GOAL
(EVERY
@@ -887,8 +885,6 @@
REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)
-val spy_analz_tac = CLASIMPSET' gen_spy_analz_tac;
-
end
*}
(*>*)
@@ -941,7 +937,7 @@
method_setup spy_analz = {*
Scan.succeed (fn ctxt =>
- SIMPLE_METHOD' (MessageSET.gen_spy_analz_tac (local_clasimpset_of ctxt))) *}
+ SIMPLE_METHOD' (MessageSET.spy_analz_tac (local_clasimpset_of ctxt))) *}
"for proving the Fake case when analz is involved"
method_setup atomic_spy_analz = {*
--- a/src/HOL/SET-Protocol/PublicSET.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/SET-Protocol/PublicSET.thy Mon Mar 23 08:16:24 2009 +0100
@@ -1,6 +1,5 @@
(* Title: HOL/Auth/SET/PublicSET
- ID: $Id$
- Authors: Giampaolo Bella, Fabio Massacci, Lawrence C Paulson
+ Authors: Giampaolo Bella, Fabio Massacci, Lawrence C Paulson
*)
header{*The Public-Key Theory, Modified for SET*}
@@ -348,22 +347,19 @@
structure PublicSET =
struct
-(*Tactic for possibility theorems (Isar interface)*)
-fun gen_possibility_tac ss state = state |>
+(*Tactic for possibility theorems*)
+fun possibility_tac ctxt =
REPEAT (*omit used_Says so that Nonces start from different traces!*)
- (ALLGOALS (simp_tac (ss delsimps [@{thm used_Says}, @{thm used_Notes}]))
+ (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [@{thm used_Says}, @{thm used_Notes}]))
THEN
REPEAT_FIRST (eq_assume_tac ORELSE'
resolve_tac [refl, conjI, @{thm Nonce_supply}]))
-(*Tactic for possibility theorems (ML script version)*)
-fun possibility_tac state = gen_possibility_tac (simpset_of (Thm.theory_of_thm state)) state
-
(*For harder protocols (such as SET_CR!), where we have to set up some
nonces and keys initially*)
-fun basic_possibility_tac st = st |>
+fun basic_possibility_tac ctxt =
REPEAT
- (ALLGOALS (asm_simp_tac (simpset_of (Thm.theory_of_thm st) setSolver safe_solver))
+ (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver))
THEN
REPEAT_FIRST (resolve_tac [refl, conjI]))
@@ -371,10 +367,12 @@
*}
method_setup possibility = {*
- Scan.succeed (fn ctxt =>
- SIMPLE_METHOD (PublicSET.gen_possibility_tac (local_simpset_of ctxt))) *}
+ Scan.succeed (SIMPLE_METHOD o PublicSET.possibility_tac) *}
"for proving possibility theorems"
+method_setup basic_possibility = {*
+ Scan.succeed (SIMPLE_METHOD o PublicSET.basic_possibility_tac) *}
+ "for proving possibility theorems"
subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*}
--- a/src/HOL/SET-Protocol/Purchase.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/SET-Protocol/Purchase.thy Mon Mar 23 08:16:24 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Auth/SET/Purchase
- ID: $Id$
Authors: Giampaolo Bella, Fabio Massacci, Lawrence C Paulson
*)
@@ -335,7 +334,7 @@
THEN set_pur.AuthResUns [of concl: "PG j" M KP LID_M XID],
THEN Says_to_Gets,
THEN set_pur.PRes])
-apply (tactic "PublicSET.basic_possibility_tac")
+apply basic_possibility
apply (simp_all add: used_Cons symKeys_neq_imp_neq)
done
@@ -371,7 +370,7 @@
THEN set_pur.AuthResS [of concl: "PG j" M KP LID_M XID],
THEN Says_to_Gets,
THEN set_pur.PRes])
-apply (tactic "PublicSET.basic_possibility_tac")
+apply basic_possibility
apply (auto simp add: used_Cons symKeys_neq_imp_neq)
done
--- a/src/HOL/Series.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/Series.thy Mon Mar 23 08:16:24 2009 +0100
@@ -557,7 +557,6 @@
apply (induct_tac "na", auto)
apply (rule_tac y = "c * norm (f (N + n))" in order_trans)
apply (auto intro: mult_right_mono simp add: summable_def)
-apply (simp add: mult_ac)
apply (rule_tac x = "norm (f N) * (1/ (1 - c)) / (c ^ N)" in exI)
apply (rule sums_divide)
apply (rule sums_mult)
--- a/src/HOL/SizeChange/sct.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/SizeChange/sct.ML Mon Mar 23 08:16:24 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/SizeChange/sct.ML
- ID: $Id$
Author: Alexander Krauss, TU Muenchen
Tactics for size change termination.
@@ -183,8 +182,10 @@
fun rand (_ $ t) = t
-fun setup_probe_goal thy domT Dtab Mtab (i, j) =
+fun setup_probe_goal ctxt domT Dtab Mtab (i, j) =
let
+ val css = local_clasimpset_of ctxt
+ val thy = ProofContext.theory_of ctxt
val RD1 = get_elem (Dtab i)
val RD2 = get_elem (Dtab j)
val Ms1 = get_elem (Mtab i)
@@ -200,12 +201,12 @@
val saved_state = HOLogic.mk_Trueprop (mk_stepP RD1 RD2 mvar1 mvar2 relvar)
|> cterm_of thy
|> Goal.init
- |> CLASIMPSET auto_tac |> Seq.hd
+ |> auto_tac css |> Seq.hd
val no_step = saved_state
|> forall_intr (cterm_of thy relvar)
|> forall_elim (cterm_of thy (Abs ("", HOLogic.natT, Abs ("", HOLogic.natT, HOLogic.false_const))))
- |> CLASIMPSET auto_tac |> Seq.hd
+ |> auto_tac css |> Seq.hd
in
if Thm.no_prems no_step
@@ -218,7 +219,7 @@
val with_m1 = saved_state
|> forall_intr (cterm_of thy mvar1)
|> forall_elim (cterm_of thy M1)
- |> CLASIMPSET auto_tac |> Seq.hd
+ |> auto_tac css |> Seq.hd
fun set_m2 j =
let
@@ -226,15 +227,15 @@
val with_m2 = with_m1
|> forall_intr (cterm_of thy mvar2)
|> forall_elim (cterm_of thy M2)
- |> CLASIMPSET auto_tac |> Seq.hd
+ |> auto_tac css |> Seq.hd
val decr = forall_intr (cterm_of thy relvar)
#> forall_elim (cterm_of thy @{const HOL.less(nat)})
- #> CLASIMPSET auto_tac #> Seq.hd
+ #> auto_tac css #> Seq.hd
val decreq = forall_intr (cterm_of thy relvar)
#> forall_elim (cterm_of thy @{const HOL.less_eq(nat)})
- #> CLASIMPSET auto_tac #> Seq.hd
+ #> auto_tac css #> Seq.hd
val thm1 = decr with_m2
in
@@ -266,17 +267,17 @@
fun mk_edge m G n = HOLogic.mk_prod (m, HOLogic.mk_prod (G, n))
-val in_graph_tac =
+fun in_graph_tac ctxt =
simp_tac (HOL_basic_ss addsimps has_edge_simps) 1
- THEN SIMPSET (fn x => simp_tac x 1) (* FIXME reduce simpset *)
+ THEN (simp_tac (local_simpset_of ctxt) 1) (* FIXME reduce simpset *)
-fun approx_tac (NoStep thm) = rtac disjI1 1 THEN rtac thm 1
- | approx_tac (Graph (G, thm)) =
+fun approx_tac _ (NoStep thm) = rtac disjI1 1 THEN rtac thm 1
+ | approx_tac ctxt (Graph (G, thm)) =
rtac disjI2 1
THEN rtac exI 1
THEN rtac conjI 1
THEN rtac thm 2
- THEN in_graph_tac
+ THEN (in_graph_tac ctxt)
fun all_less_tac [] = rtac all_less_zero 1
| all_less_tac (t :: ts) = rtac all_less_Suc 1
@@ -292,7 +293,7 @@
fun mk_call_graph ctxt (st : thm) =
let
- val thy = theory_of_thm st
+ val thy = ProofContext.theory_of ctxt
val _ $ _ $ RDlist $ _ = HOLogic.dest_Trueprop (hd (prems_of st))
val RDs = HOLogic.dest_list RDlist
@@ -316,7 +317,7 @@
val pairs = matrix indices indices
val parts = map_matrix (fn (n,m) =>
(timeap_msg (string_of_int n ^ "," ^ string_of_int m)
- (setup_probe_goal thy domT Dtab Mtab) (n,m))) pairs
+ (setup_probe_goal ctxt domT Dtab Mtab) (n,m))) pairs
val s = fold_index (fn (i, cs) => fold_index (fn (j, Graph (G, _)) => prefix ("(" ^ string_of_int i ^ "," ^ string_of_int j ^ "): " ^
@@ -333,8 +334,8 @@
val sound_int_goal = HOLogic.mk_Trueprop (mk_sound_int ACG RDlist mfuns)
val tac =
- (SIMPSET (unfold_tac [sound_int_def, len_simp]))
- THEN all_less_tac (map (all_less_tac o map approx_tac) parts)
+ unfold_tac [sound_int_def, len_simp] (local_simpset_of ctxt)
+ THEN all_less_tac (map (all_less_tac o map (approx_tac ctxt)) parts)
in
tac (instantiate' [] [SOME (cterm_of thy ACG), SOME (cterm_of thy mfuns)] st)
end
--- a/src/HOL/Tools/Qelim/qelim.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/Tools/Qelim/qelim.ML Mon Mar 23 08:16:24 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Tools/Qelim/qelim.ML
- ID: $Id$
Author: Amine Chaieb, TU Muenchen
Generic quantifier elimination conversions for HOL formulae.
@@ -26,11 +25,12 @@
case (term_of p) of
Const(s,T)$_$_ =>
if domain_type T = HOLogic.boolT
- andalso s mem ["op &","op |","op -->","op ="]
+ andalso member (op =) [@{const_name "op &"}, @{const_name "op |"},
+ @{const_name "op -->"}, @{const_name "op ="}] s
then binop_conv (conv env) p
else atcv env p
- | Const("Not",_)$_ => arg_conv (conv env) p
- | Const("Ex",_)$Abs(s,_,_) =>
+ | Const(@{const_name "Not"},_)$_ => arg_conv (conv env) p
+ | Const(@{const_name "Ex"},_)$Abs(s,_,_) =>
let
val (e,p0) = Thm.dest_comb p
val (x,p') = Thm.dest_abs (SOME s) p0
@@ -41,8 +41,8 @@
val (l,r) = Thm.dest_equals (cprop_of th')
in if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th))
else Thm.transitive (Thm.transitive th th') (conv env r) end
- | Const("Ex",_)$ _ => (Thm.eta_long_conversion then_conv conv env) p
- | Const("All",_)$_ =>
+ | Const(@{const_name "Ex"},_)$ _ => (Thm.eta_long_conversion then_conv conv env) p
+ | Const(@{const_name "All"},_)$_ =>
let
val p = Thm.dest_arg p
val ([(_,T)],[]) = Thm.match (@{cpat "All"}, Thm.dest_fun p)
--- a/src/HOL/Tools/cnf_funcs.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/Tools/cnf_funcs.ML Mon Mar 23 08:16:24 2009 +0100
@@ -51,51 +51,46 @@
structure cnf : CNF =
struct
-fun thm_by_auto (G : string) : thm =
- prove_goal (the_context ()) G (fn prems => [cut_facts_tac prems 1, CLASIMPSET auto_tac]);
+val clause2raw_notE = @{lemma "[| P; ~P |] ==> False" by auto};
+val clause2raw_not_disj = @{lemma "[| ~P; ~Q |] ==> ~(P | Q)" by auto};
+val clause2raw_not_not = @{lemma "P ==> ~~P" by auto};
-(* Thm.thm *)
-val clause2raw_notE = thm_by_auto "[| P; ~P |] ==> False";
-val clause2raw_not_disj = thm_by_auto "[| ~P; ~Q |] ==> ~(P | Q)";
-val clause2raw_not_not = thm_by_auto "P ==> ~~P";
+val iff_refl = @{lemma "(P::bool) = P" by auto};
+val iff_trans = @{lemma "[| (P::bool) = Q; Q = R |] ==> P = R" by auto};
+val conj_cong = @{lemma "[| P = P'; Q = Q' |] ==> (P & Q) = (P' & Q')" by auto};
+val disj_cong = @{lemma "[| P = P'; Q = Q' |] ==> (P | Q) = (P' | Q')" by auto};
-val iff_refl = thm_by_auto "(P::bool) = P";
-val iff_trans = thm_by_auto "[| (P::bool) = Q; Q = R |] ==> P = R";
-val conj_cong = thm_by_auto "[| P = P'; Q = Q' |] ==> (P & Q) = (P' & Q')";
-val disj_cong = thm_by_auto "[| P = P'; Q = Q' |] ==> (P | Q) = (P' | Q')";
-
-val make_nnf_imp = thm_by_auto "[| (~P) = P'; Q = Q' |] ==> (P --> Q) = (P' | Q')";
-val make_nnf_iff = thm_by_auto "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (P = Q) = ((P' | NQ) & (NP | Q'))";
-val make_nnf_not_false = thm_by_auto "(~False) = True";
-val make_nnf_not_true = thm_by_auto "(~True) = False";
-val make_nnf_not_conj = thm_by_auto "[| (~P) = P'; (~Q) = Q' |] ==> (~(P & Q)) = (P' | Q')";
-val make_nnf_not_disj = thm_by_auto "[| (~P) = P'; (~Q) = Q' |] ==> (~(P | Q)) = (P' & Q')";
-val make_nnf_not_imp = thm_by_auto "[| P = P'; (~Q) = Q' |] ==> (~(P --> Q)) = (P' & Q')";
-val make_nnf_not_iff = thm_by_auto "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (~(P = Q)) = ((P' | Q') & (NP | NQ))";
-val make_nnf_not_not = thm_by_auto "P = P' ==> (~~P) = P'";
+val make_nnf_imp = @{lemma "[| (~P) = P'; Q = Q' |] ==> (P --> Q) = (P' | Q')" by auto};
+val make_nnf_iff = @{lemma "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (P = Q) = ((P' | NQ) & (NP | Q'))" by auto};
+val make_nnf_not_false = @{lemma "(~False) = True" by auto};
+val make_nnf_not_true = @{lemma "(~True) = False" by auto};
+val make_nnf_not_conj = @{lemma "[| (~P) = P'; (~Q) = Q' |] ==> (~(P & Q)) = (P' | Q')" by auto};
+val make_nnf_not_disj = @{lemma "[| (~P) = P'; (~Q) = Q' |] ==> (~(P | Q)) = (P' & Q')" by auto};
+val make_nnf_not_imp = @{lemma "[| P = P'; (~Q) = Q' |] ==> (~(P --> Q)) = (P' & Q')" by auto};
+val make_nnf_not_iff = @{lemma "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (~(P = Q)) = ((P' | Q') & (NP | NQ))" by auto};
+val make_nnf_not_not = @{lemma "P = P' ==> (~~P) = P'" by auto};
-val simp_TF_conj_True_l = thm_by_auto "[| P = True; Q = Q' |] ==> (P & Q) = Q'";
-val simp_TF_conj_True_r = thm_by_auto "[| P = P'; Q = True |] ==> (P & Q) = P'";
-val simp_TF_conj_False_l = thm_by_auto "P = False ==> (P & Q) = False";
-val simp_TF_conj_False_r = thm_by_auto "Q = False ==> (P & Q) = False";
-val simp_TF_disj_True_l = thm_by_auto "P = True ==> (P | Q) = True";
-val simp_TF_disj_True_r = thm_by_auto "Q = True ==> (P | Q) = True";
-val simp_TF_disj_False_l = thm_by_auto "[| P = False; Q = Q' |] ==> (P | Q) = Q'";
-val simp_TF_disj_False_r = thm_by_auto "[| P = P'; Q = False |] ==> (P | Q) = P'";
+val simp_TF_conj_True_l = @{lemma "[| P = True; Q = Q' |] ==> (P & Q) = Q'" by auto};
+val simp_TF_conj_True_r = @{lemma "[| P = P'; Q = True |] ==> (P & Q) = P'" by auto};
+val simp_TF_conj_False_l = @{lemma "P = False ==> (P & Q) = False" by auto};
+val simp_TF_conj_False_r = @{lemma "Q = False ==> (P & Q) = False" by auto};
+val simp_TF_disj_True_l = @{lemma "P = True ==> (P | Q) = True" by auto};
+val simp_TF_disj_True_r = @{lemma "Q = True ==> (P | Q) = True" by auto};
+val simp_TF_disj_False_l = @{lemma "[| P = False; Q = Q' |] ==> (P | Q) = Q'" by auto};
+val simp_TF_disj_False_r = @{lemma "[| P = P'; Q = False |] ==> (P | Q) = P'" by auto};
-val make_cnf_disj_conj_l = thm_by_auto "[| (P | R) = PR; (Q | R) = QR |] ==> ((P & Q) | R) = (PR & QR)";
-val make_cnf_disj_conj_r = thm_by_auto "[| (P | Q) = PQ; (P | R) = PR |] ==> (P | (Q & R)) = (PQ & PR)";
+val make_cnf_disj_conj_l = @{lemma "[| (P | R) = PR; (Q | R) = QR |] ==> ((P & Q) | R) = (PR & QR)" by auto};
+val make_cnf_disj_conj_r = @{lemma "[| (P | Q) = PQ; (P | R) = PR |] ==> (P | (Q & R)) = (PQ & PR)" by auto};
-val make_cnfx_disj_ex_l = thm_by_auto "((EX (x::bool). P x) | Q) = (EX x. P x | Q)";
-val make_cnfx_disj_ex_r = thm_by_auto "(P | (EX (x::bool). Q x)) = (EX x. P | Q x)";
-val make_cnfx_newlit = thm_by_auto "(P | Q) = (EX x. (P | x) & (Q | ~x))";
-val make_cnfx_ex_cong = thm_by_auto "(ALL (x::bool). P x = Q x) ==> (EX x. P x) = (EX x. Q x)";
+val make_cnfx_disj_ex_l = @{lemma "((EX (x::bool). P x) | Q) = (EX x. P x | Q)" by auto};
+val make_cnfx_disj_ex_r = @{lemma "(P | (EX (x::bool). Q x)) = (EX x. P | Q x)" by auto};
+val make_cnfx_newlit = @{lemma "(P | Q) = (EX x. (P | x) & (Q | ~x))" by auto};
+val make_cnfx_ex_cong = @{lemma "(ALL (x::bool). P x = Q x) ==> (EX x. P x) = (EX x. Q x)" by auto};
-val weakening_thm = thm_by_auto "[| P; Q |] ==> Q";
+val weakening_thm = @{lemma "[| P; Q |] ==> Q" by auto};
-val cnftac_eq_imp = thm_by_auto "[| P = Q; P |] ==> Q";
+val cnftac_eq_imp = @{lemma "[| P = Q; P |] ==> Q" by auto};
-(* Term.term -> bool *)
fun is_atom (Const ("False", _)) = false
| is_atom (Const ("True", _)) = false
| is_atom (Const ("op &", _) $ _ $ _) = false
@@ -105,11 +100,9 @@
| is_atom (Const ("Not", _) $ _) = false
| is_atom _ = true;
-(* Term.term -> bool *)
fun is_literal (Const ("Not", _) $ x) = is_atom x
| is_literal x = is_atom x;
-(* Term.term -> bool *)
fun is_clause (Const ("op |", _) $ x $ y) = is_clause x andalso is_clause y
| is_clause x = is_literal x;
--- a/src/HOL/Tools/function_package/fundef_core.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_core.ML Mon Mar 23 08:16:24 2009 +0100
@@ -691,8 +691,9 @@
(* FIXME: This should probably use fixed goals, to be more reliable and faster *)
-fun mk_domain_intro thy (Globals {domT, ...}) R R_cases clause =
+fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause =
let
+ val thy = ProofContext.theory_of ctxt
val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...},
qglr = (oqs, _, _, _), ...} = clause
val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
@@ -702,7 +703,7 @@
Goal.init goal
|> (SINGLE (resolve_tac [accI] 1)) |> the
|> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1)) |> the
- |> (SINGLE (CLASIMPSET auto_tac)) |> the
+ |> (SINGLE (auto_tac (local_clasimpset_of ctxt))) |> the
|> Goal.conclude
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
end
@@ -831,7 +832,7 @@
((rtac (G_induct OF [a]))
THEN_ALL_NEW (rtac accI)
THEN_ALL_NEW (etac R_cases)
- THEN_ALL_NEW (SIMPSET' asm_full_simp_tac)) 1)
+ THEN_ALL_NEW (asm_full_simp_tac (local_simpset_of octxt))) 1)
val default_thm = (forall_intr_vars graph_implies_dom) COMP (f_def COMP fundef_default_value)
@@ -849,9 +850,9 @@
(fn _ =>
rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
- THEN (SIMPSET' simp_default_tac 1)
+ THEN (simp_default_tac (local_simpset_of ctxt) 1)
THEN (etac not_acc_down 1)
- THEN ((etac R_cases) THEN_ALL_NEW (SIMPSET' simp_default_tac)) 1)
+ THEN ((etac R_cases) THEN_ALL_NEW (simp_default_tac (local_simpset_of ctxt))) 1)
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
end
in
@@ -935,7 +936,7 @@
val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule newthy globals R R_elim) xclauses
val dom_intros = if domintros
- then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro newthy globals R R_elim)) xclauses)
+ then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro lthy globals R R_elim)) xclauses)
else NONE
val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE
--- a/src/HOL/Tools/function_package/mutual.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/Tools/function_package/mutual.ML Mon Mar 23 08:16:24 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Tools/function_package/mutual.ML
- ID: $Id$
Author: Alexander Krauss, TU Muenchen
A package for general recursive function definitions.
@@ -207,7 +206,7 @@
(HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
(fn _ => (LocalDefs.unfold_tac ctxt all_orig_fdefs)
THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
- THEN SIMPSET' (fn ss => simp_tac (ss addsimps SumTree.proj_in_rules)) 1)
+ THEN (simp_tac (local_simpset_of ctxt addsimps SumTree.proj_in_rules)) 1)
|> restore_cond
|> export
end
--- a/src/HOL/Tools/function_package/scnp_reconstruct.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/Tools/function_package/scnp_reconstruct.ML Mon Mar 23 08:16:24 2009 +0100
@@ -291,7 +291,7 @@
THEN (rtac @{thm rp_inv_image_rp} 1)
THEN (rtac (order_rpair ms_rp label) 1)
THEN PRIMITIVE (instantiate' [] [SOME level_mapping])
- THEN unfold_tac @{thms rp_inv_image_def} (simpset_of thy)
+ THEN unfold_tac @{thms rp_inv_image_def} (local_simpset_of ctxt)
THEN LocalDefs.unfold_tac ctxt
(@{thms split_conv} @ @{thms fst_conv} @ @{thms snd_conv})
THEN REPEAT (SOMEGOAL (resolve_tac [@{thm Un_least}, @{thm empty_subsetI}]))
@@ -395,7 +395,7 @@
fun gen_sizechange_tac orders autom_tac ctxt err_cont =
TRY (FundefCommon.apply_termination_rule ctxt 1)
- THEN TRY Termination.wf_union_tac
+ THEN TRY (Termination.wf_union_tac ctxt)
THEN
(rtac @{thm wf_empty} 1
ORELSE gen_decomp_scnp_tac orders autom_tac ctxt err_cont 1)
--- a/src/HOL/Tools/function_package/termination.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/Tools/function_package/termination.ML Mon Mar 23 08:16:24 2009 +0100
@@ -40,7 +40,7 @@
val REPEAT : ttac -> ttac
- val wf_union_tac : tactic
+ val wf_union_tac : Proof.context -> tactic
end
@@ -276,9 +276,9 @@
in
-fun wf_union_tac st =
+fun wf_union_tac ctxt st =
let
- val thy = theory_of_thm st
+ val thy = ProofContext.theory_of ctxt
val cert = cterm_of (theory_of_thm st)
val ((trueprop $ (wf $ rel)) :: ineqs) = prems_of st
@@ -303,7 +303,7 @@
THEN' ((rtac @{thm refl}) (* unification instantiates all Vars *)
ORELSE' ((rtac @{thm conjI})
THEN' (rtac @{thm refl})
- THEN' (CLASET' blast_tac))) (* Solve rest of context... not very elegant *)
+ THEN' (blast_tac (local_claset_of ctxt)))) (* Solve rest of context... not very elegant *)
) i
in
((PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
--- a/src/HOL/Tools/int_factor_simprocs.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/Tools/int_factor_simprocs.ML Mon Mar 23 08:16:24 2009 +0100
@@ -218,9 +218,30 @@
val simplify_one = Arith_Data.simplify_meta_eq
[@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}];
-fun cancel_simplify_meta_eq cancel_th ss th =
+fun cancel_simplify_meta_eq ss cancel_th th =
simplify_one ss (([th, cancel_th]) MRS trans);
+local
+ val Tp_Eq = Thm.reflexive(Thm.cterm_of (@{theory HOL}) HOLogic.Trueprop)
+ fun Eq_True_elim Eq =
+ Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI}
+in
+fun sign_conv pos_th neg_th ss t =
+ let val T = fastype_of t;
+ val zero = Const(@{const_name HOL.zero}, T);
+ val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT);
+ val pos = less $ zero $ t and neg = less $ t $ zero
+ fun prove p =
+ Option.map Eq_True_elim (LinArith.lin_arith_simproc ss p)
+ handle THM _ => NONE
+ in case prove pos of
+ SOME th => SOME(th RS pos_th)
+ | NONE => (case prove neg of
+ SOME th => SOME(th RS neg_th)
+ | NONE => NONE)
+ end;
+end
+
structure CancelFactorCommon =
struct
val mk_sum = long_mk_prod
@@ -231,6 +252,7 @@
val trans_tac = K Arith_Data.trans_tac
val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
+ val simplify_meta_eq = cancel_simplify_meta_eq
end;
(*mult_cancel_left requires a ring with no zero divisors.*)
@@ -239,7 +261,27 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
- val simplify_meta_eq = cancel_simplify_meta_eq @{thm mult_cancel_left}
+ val simp_conv = K (K (SOME @{thm mult_cancel_left}))
+);
+
+(*for ordered rings*)
+structure LeCancelFactor = ExtractCommonTermFun
+ (open CancelFactorCommon
+ val prove_conv = Arith_Data.prove_conv
+ val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq}
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
+ val simp_conv = sign_conv
+ @{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg}
+);
+
+(*for ordered rings*)
+structure LessCancelFactor = ExtractCommonTermFun
+ (open CancelFactorCommon
+ val prove_conv = Arith_Data.prove_conv
+ val mk_bal = HOLogic.mk_binrel @{const_name HOL.less}
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
+ val simp_conv = sign_conv
+ @{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg}
);
(*zdiv_zmult_zmult1_if is for integer division (div).*)
@@ -248,7 +290,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name Divides.div}
val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT
- val simplify_meta_eq = cancel_simplify_meta_eq @{thm zdiv_zmult_zmult1_if}
+ val simp_conv = K (K (SOME @{thm zdiv_zmult_zmult1_if}))
);
structure IntModCancelFactor = ExtractCommonTermFun
@@ -256,7 +298,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name Divides.mod}
val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} HOLogic.intT
- val simplify_meta_eq = cancel_simplify_meta_eq @{thm zmod_zmult_zmult1}
+ val simp_conv = K (K (SOME @{thm zmod_zmult_zmult1}))
);
structure IntDvdCancelFactor = ExtractCommonTermFun
@@ -264,7 +306,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} Term.dummyT
- val simplify_meta_eq = cancel_simplify_meta_eq @{thm dvd_mult_cancel_left}
+ val simp_conv = K (K (SOME @{thm dvd_mult_cancel_left}))
);
(*Version for all fields, including unordered ones (type complex).*)
@@ -273,7 +315,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name HOL.divide}
val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
- val simplify_meta_eq = cancel_simplify_meta_eq @{thm mult_divide_mult_cancel_left_if}
+ val simp_conv = K (K (SOME @{thm mult_divide_mult_cancel_left_if}))
);
val cancel_factors =
@@ -281,7 +323,15 @@
[("ring_eq_cancel_factor",
["(l::'a::{idom}) * m = n",
"(l::'a::{idom}) = m * n"],
- K EqCancelFactor.proc),
+ K EqCancelFactor.proc),
+ ("ordered_ring_le_cancel_factor",
+ ["(l::'a::ordered_ring) * m <= n",
+ "(l::'a::ordered_ring) <= m * n"],
+ K LeCancelFactor.proc),
+ ("ordered_ring_less_cancel_factor",
+ ["(l::'a::ordered_ring) * m < n",
+ "(l::'a::ordered_ring) < m * n"],
+ K LessCancelFactor.proc),
("int_div_cancel_factor",
["((l::int) * m) div n", "(l::int) div (m * n)"],
K IntDivCancelFactor.proc),
--- a/src/HOL/Tools/meson.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/Tools/meson.ML Mon Mar 23 08:16:24 2009 +0100
@@ -25,7 +25,7 @@
val skolemize_prems_tac: thm list -> int -> tactic
val MESON: (thm list -> thm list) -> (thm list -> tactic) -> int -> tactic
val best_meson_tac: (thm -> int) -> int -> tactic
- val safe_best_meson_tac: int -> tactic
+ val safe_best_meson_tac: claset -> int -> tactic
val depth_meson_tac: int -> tactic
val prolog_step_tac': thm list -> int -> tactic
val iter_deepen_prolog_tac: thm list -> tactic
@@ -33,7 +33,7 @@
val make_meta_clause: thm -> thm
val make_meta_clauses: thm list -> thm list
val meson_claset_tac: thm list -> claset -> int -> tactic
- val meson_tac: int -> tactic
+ val meson_tac: claset -> int -> tactic
val negate_head: thm -> thm
val select_literal: int -> thm -> thm
val skolemize_tac: int -> tactic
@@ -589,8 +589,8 @@
(prolog_step_tac (make_horns cls) 1));
(*First, breaks the goal into independent units*)
-val safe_best_meson_tac =
- SELECT_GOAL (TRY (CLASET safe_tac) THEN
+fun safe_best_meson_tac cs =
+ SELECT_GOAL (TRY (safe_tac cs) THEN
TRYALL (best_meson_tac size_of_subgoals));
(** Depth-first search version **)
@@ -634,7 +634,7 @@
fun meson_claset_tac ths cs =
SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths));
-val meson_tac = CLASET' (meson_claset_tac []);
+val meson_tac = meson_claset_tac [];
(**** Code to support ordinary resolution, rather than Model Elimination ****)
--- a/src/HOL/Tools/nat_simprocs.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/Tools/nat_simprocs.ML Mon Mar 23 08:16:24 2009 +0100
@@ -352,7 +352,7 @@
val simplify_one = Arith_Data.simplify_meta_eq
[@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_1}, @{thm numeral_1_eq_Suc_0}];
-fun cancel_simplify_meta_eq cancel_th ss th =
+fun cancel_simplify_meta_eq ss cancel_th th =
simplify_one ss (([th, cancel_th]) MRS trans);
structure CancelFactorCommon =
@@ -365,6 +365,7 @@
val trans_tac = K Arith_Data.trans_tac
val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
+ val simplify_meta_eq = cancel_simplify_meta_eq
end;
structure EqCancelFactor = ExtractCommonTermFun
@@ -372,7 +373,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
- val simplify_meta_eq = cancel_simplify_meta_eq @{thm nat_mult_eq_cancel_disj}
+ val simp_conv = K(K (SOME @{thm nat_mult_eq_cancel_disj}))
);
structure LessCancelFactor = ExtractCommonTermFun
@@ -380,7 +381,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less}
val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
- val simplify_meta_eq = cancel_simplify_meta_eq @{thm nat_mult_less_cancel_disj}
+ val simp_conv = K(K (SOME @{thm nat_mult_less_cancel_disj}))
);
structure LeCancelFactor = ExtractCommonTermFun
@@ -388,7 +389,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq}
val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
- val simplify_meta_eq = cancel_simplify_meta_eq @{thm nat_mult_le_cancel_disj}
+ val simp_conv = K(K (SOME @{thm nat_mult_le_cancel_disj}))
);
structure DivideCancelFactor = ExtractCommonTermFun
@@ -396,7 +397,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name Divides.div}
val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
- val simplify_meta_eq = cancel_simplify_meta_eq @{thm nat_mult_div_cancel_disj}
+ val simp_conv = K(K (SOME @{thm nat_mult_div_cancel_disj}))
);
structure DvdCancelFactor = ExtractCommonTermFun
@@ -404,7 +405,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT
- val simplify_meta_eq = cancel_simplify_meta_eq @{thm nat_mult_dvd_cancel_disj}
+ val simp_conv = K(K (SOME @{thm nat_mult_dvd_cancel_disj}))
);
val cancel_factor =
--- a/src/HOL/Tools/simpdata.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/Tools/simpdata.ML Mon Mar 23 08:16:24 2009 +0100
@@ -147,8 +147,6 @@
val op addsplits = Splitter.addsplits;
val op delsplits = Splitter.delsplits;
-val Addsplits = Splitter.Addsplits;
-val Delsplits = Splitter.Delsplits;
(* integration of simplifier with classical reasoner *)
--- a/src/HOL/UNITY/UNITY_tactics.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/UNITY/UNITY_tactics.ML Mon Mar 23 08:16:24 2009 +0100
@@ -59,6 +59,6 @@
th RS @{thm o_equiv_assoc} |> simplify (HOL_ss addsimps [@{thm o_assoc}]),
th RS @{thm o_equiv_apply} |> simplify (HOL_ss addsimps [@{thm o_def}, @{thm sub_def}])];
-Addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair});
-
-Addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map});
+Simplifier.change_simpset (fn ss => ss
+ addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair})
+ addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map}));
--- a/src/HOL/Word/WordArith.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/Word/WordArith.thy Mon Mar 23 08:16:24 2009 +0100
@@ -511,10 +511,13 @@
addcongs @{thms power_False_cong}
fun uint_arith_tacs ctxt =
- let fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty
+ let
+ fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty;
+ val cs = local_claset_of ctxt;
+ val ss = local_simpset_of ctxt;
in
- [ CLASET' clarify_tac 1,
- SIMPSET' (full_simp_tac o uint_arith_ss_of) 1,
+ [ clarify_tac cs 1,
+ full_simp_tac (uint_arith_ss_of ss) 1,
ALLGOALS (full_simp_tac (HOL_ss addsplits @{thms uint_splits}
addcongs @{thms power_False_cong})),
rewrite_goals_tac @{thms word_size},
@@ -698,6 +701,7 @@
apply (erule (2) udvd_decr0)
done
+ML{*Delsimprocs cancel_factors*}
lemma udvd_incr2_K:
"p < a + s ==> a <= a + s ==> K udvd s ==> K udvd p - a ==> a <= p ==>
0 < K ==> p <= p + K & p + K <= a + s"
@@ -713,6 +717,7 @@
apply arith
apply simp
done
+ML{*Delsimprocs cancel_factors*}
(* links with rbl operations *)
lemma word_succ_rbl:
@@ -1069,10 +1074,13 @@
addcongs @{thms power_False_cong}
fun unat_arith_tacs ctxt =
- let fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty
+ let
+ fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty;
+ val cs = local_claset_of ctxt;
+ val ss = local_simpset_of ctxt;
in
- [ CLASET' clarify_tac 1,
- SIMPSET' (full_simp_tac o unat_arith_ss_of) 1,
+ [ clarify_tac cs 1,
+ full_simp_tac (unat_arith_ss_of ss) 1,
ALLGOALS (full_simp_tac (HOL_ss addsplits @{thms unat_splits}
addcongs @{thms power_False_cong})),
rewrite_goals_tac @{thms word_size},
--- a/src/HOL/ex/Classical.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOL/ex/Classical.thy Mon Mar 23 08:16:24 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/ex/Classical
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
*)
@@ -430,7 +429,7 @@
lemma "(\<forall>x y z. R(x,y) & R(y,z) --> R(x,z)) &
(\<forall>x. \<exists>y. R(x,y)) -->
~ (\<forall>x. P x = (\<forall>y. R(x,y) --> ~ P y))"
-by (tactic{*Meson.safe_best_meson_tac 1*})
+by (tactic{*Meson.safe_best_meson_tac @{claset} 1*})
--{*In contrast, @{text meson} is SLOW: 7.6s on griffon*}
@@ -724,7 +723,7 @@
(\<forall>x y. bird x & snail y \<longrightarrow> ~eats x y) &
(\<forall>x. (caterpillar x \<or> snail x) \<longrightarrow> (\<exists>y. plant y & eats x y))
\<longrightarrow> (\<exists>x y. animal x & animal y & (\<exists>z. grain z & eats y z & eats x y))"
-by (tactic{*Meson.safe_best_meson_tac 1*})
+by (tactic{*Meson.safe_best_meson_tac @{claset} 1*})
--{*Nearly twice as fast as @{text meson},
which performs iterative deepening rather than best-first search*}
--- a/src/HOLCF/FOCUS/Buffer.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOLCF/FOCUS/Buffer.thy Mon Mar 23 08:16:24 2009 +0100
@@ -98,8 +98,11 @@
by (erule subst, rule refl)
ML {*
-fun B_prover s tac eqs = prove_goal (the_context ()) s (fn prems => [cut_facts_tac prems 1,
- tac 1, auto_tac (claset(), simpset() addsimps eqs)]);
+fun B_prover s tac eqs =
+ let val thy = the_context () in
+ prove_goal thy s (fn prems => [cut_facts_tac prems 1,
+ tac 1, auto_tac (claset_of thy, simpset_of thy addsimps eqs)])
+ end;
fun prove_forw s thm = B_prover s (dtac (thm RS iffD1)) [];
fun prove_backw s thm eqs = B_prover s (rtac (thm RS iffD2)) eqs;
--- a/src/HOLCF/IOA/Modelcheck/Cockpit.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOLCF/IOA/Modelcheck/Cockpit.thy Mon Mar 23 08:16:24 2009 +0100
@@ -102,18 +102,18 @@
(* to prove, that info is always set at the recent alarm *)
lemma cockpit_implements_Info_while_Al: "cockpit =<| Info_while_Al"
-apply (tactic {* is_sim_tac (thms "aut_simps") 1 *})
+apply (tactic {* is_sim_tac @{simpset} (thms "aut_simps") 1 *})
done
(* to prove that before any alarm arrives (and after each acknowledgment),
info remains at None *)
lemma cockpit_implements_Info_before_Al: "cockpit =<| Info_before_Al"
-apply (tactic {* is_sim_tac (thms "aut_simps") 1 *})
+apply (tactic {* is_sim_tac @{simpset} (thms "aut_simps") 1 *})
done
(* to prove that before any alarm would be acknowledged, it must be arrived *)
lemma cockpit_implements_Al_before_Ack: "cockpit_hide =<| Al_before_Ack"
-apply (tactic {* is_sim_tac (thms "aut_simps") 1 *})
+apply (tactic {* is_sim_tac @{simpset} (thms "aut_simps") 1 *})
apply auto
done
--- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy Mon Mar 23 08:16:24 2009 +0100
@@ -278,14 +278,14 @@
by (REPEAT (rtac impI 1));
by (REPEAT (dtac eq_reflection 1));
(* Bis hierher wird im Kapitel 4 erl"autert, ab hier im Kapitel 5 *)
-by (full_simp_tac ((simpset() delcongs (if_weak_cong :: weak_case_congs)
+by (full_simp_tac ((simpset_of sign delcongs (if_weak_cong :: weak_case_congs)
delsimps [not_iff,split_part])
addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @
rename_simps @ ioa_simps @ asig_simps)) 1);
by (full_simp_tac
(Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1);
by (REPEAT (if_full_simp_tac
- (simpset() delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1));
+ (simpset_of sign delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1));
by (call_mucke_tac 1);
(* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *)
by (atac 1);
--- a/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy Mon Mar 23 08:16:24 2009 +0100
@@ -18,18 +18,18 @@
(* is_sim_tac makes additionally to call_sim_tac some simplifications,
which are suitable for implementation realtion formulas *)
-fun is_sim_tac thm_list = SUBGOAL (fn (goal, i) =>
+fun is_sim_tac ss thm_list = SUBGOAL (fn (goal, i) =>
EVERY [REPEAT (etac thin_rl i),
- simp_tac (simpset() addsimps [ioa_implements_def]) i,
+ simp_tac (ss addsimps [ioa_implements_def]) i,
rtac conjI i,
rtac conjI (i+1),
TRY(call_sim_tac thm_list (i+2)),
TRY(atac (i+2)),
REPEAT(rtac refl (i+2)),
- simp_tac (simpset() addsimps (thm_list @
+ simp_tac (ss addsimps (thm_list @
comp_simps @ restrict_simps @ hide_simps @
rename_simps @ ioa_simps @ asig_simps)) (i+1),
- simp_tac (simpset() addsimps (thm_list @
+ simp_tac (ss addsimps (thm_list @
comp_simps @ restrict_simps @ hide_simps @
rename_simps @ ioa_simps @ asig_simps)) (i)]);
--- a/src/HOLCF/IOA/Modelcheck/Ring3.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOLCF/IOA/Modelcheck/Ring3.thy Mon Mar 23 08:16:24 2009 +0100
@@ -114,7 +114,7 @@
(* property to prove: at most one (of 3) members of the ring will
declare itself to leader *)
lemma at_most_one_leader: "ring =<| one_leader"
-apply (tactic {* is_sim_tac (thms "aut_simps") 1 *})
+apply (tactic {* is_sim_tac @{simpset} (thms "aut_simps") 1 *})
apply auto
done
--- a/src/HOLCF/IOA/ex/TrivEx.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOLCF/IOA/ex/TrivEx.thy Mon Mar 23 08:16:24 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/TrivEx.thy
- ID: $Id$
Author: Olaf Müller
*)
@@ -66,7 +65,7 @@
apply (rule AbsRuleT1)
apply (rule h_abs_is_abstraction)
apply (rule MC_result)
-apply (tactic "abstraction_tac 1")
+apply abstraction
apply (simp add: h_abs_def)
done
--- a/src/HOLCF/IOA/ex/TrivEx2.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOLCF/IOA/ex/TrivEx2.thy Mon Mar 23 08:16:24 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/TrivEx.thy
- ID: $Id$
Author: Olaf Müller
*)
@@ -85,7 +84,7 @@
txt {* is_abstraction *}
apply (rule h_abs_is_abstraction)
txt {* temp_weakening *}
-apply (tactic "abstraction_tac 1")
+apply abstraction
apply (erule Enabled_implication)
done
@@ -96,7 +95,7 @@
apply (rule AbsRuleT2)
apply (rule h_abs_is_liveabstraction)
apply (rule MC_result)
-apply (tactic "abstraction_tac 1")
+apply abstraction
apply (simp add: h_abs_def)
done
--- a/src/HOLCF/IOA/meta_theory/Abstraction.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy Mon Mar 23 08:16:24 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/meta_theory/Abstraction.thy
- ID: $Id$
Author: Olaf Müller
*)
@@ -605,12 +604,15 @@
strength_Diamond strength_Leadsto weak_WF weak_SF
ML {*
-fun abstraction_tac i =
- SELECT_GOAL (CLASIMPSET (fn (cs, ss) =>
- auto_tac (cs addSIs @{thms weak_strength_lemmas},
- ss addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}]))) i
+fun abstraction_tac ctxt =
+ let val (cs, ss) = local_clasimpset_of ctxt in
+ SELECT_GOAL (auto_tac (cs addSIs @{thms weak_strength_lemmas},
+ ss addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}]))
+ end
*}
+method_setup abstraction = {* Scan.succeed (SIMPLE_METHOD' o abstraction_tac) *} ""
+
use "ioa_package.ML"
end
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Mon Mar 23 08:16:24 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/meta_theory/Sequence.thy
- ID: $Id$
Author: Olaf Müller
Sequences over flat domains with lifted elements.
@@ -340,7 +339,7 @@
lemma Seq_induct:
"!! P. [| adm P; P UU; P nil; !! a s. P s ==> P (a>>s)|] ==> P x"
apply (erule (2) seq.ind)
-apply (tactic {* def_tac 1 *})
+apply defined
apply (simp add: Consq_def)
done
@@ -348,14 +347,14 @@
"!! P.[|P UU;P nil; !! a s. P s ==> P(a>>s) |]
==> seq_finite x --> P x"
apply (erule (1) seq_finite_ind)
-apply (tactic {* def_tac 1 *})
+apply defined
apply (simp add: Consq_def)
done
lemma Seq_Finite_ind:
"!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a>>s) |] ==> P x"
apply (erule (1) Finite.induct)
-apply (tactic {* def_tac 1 *})
+apply defined
apply (simp add: Consq_def)
done
--- a/src/HOLCF/IOA/meta_theory/Traces.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOLCF/IOA/meta_theory/Traces.thy Mon Mar 23 08:16:24 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOLCF/IOA/meta_theory/Traces.thy
- ID: $Id$
Author: Olaf Müller
*)
@@ -327,7 +326,7 @@
apply (simp (no_asm_simp))
apply (drule Finite_Last1 [THEN mp])
apply assumption
-apply (tactic "def_tac 1")
+apply defined
done
declare laststate_UU [simp] laststate_nil [simp] laststate_cons [simp]
--- a/src/HOLCF/Lift.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/HOLCF/Lift.thy Mon Mar 23 08:16:24 2009 +0100
@@ -56,15 +56,13 @@
by (cases x) simp_all
text {*
- For @{term "x ~= UU"} in assumptions @{text def_tac} replaces @{text
+ For @{term "x ~= UU"} in assumptions @{text defined} replaces @{text
x} by @{text "Def a"} in conclusion. *}
-ML {*
- local val lift_definedE = thm "lift_definedE"
- in val def_tac = SIMPSET' (fn ss =>
- etac lift_definedE THEN' asm_simp_tac ss)
- end;
-*}
+method_setup defined = {*
+ Scan.succeed (fn ctxt => SIMPLE_METHOD'
+ (etac @{thm lift_definedE} THEN' asm_simp_tac (local_simpset_of ctxt)))
+*} ""
lemma DefE: "Def x = \<bottom> \<Longrightarrow> R"
by simp
--- a/src/Provers/Arith/extract_common_term.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Provers/Arith/extract_common_term.ML Mon Mar 23 08:16:24 2009 +0100
@@ -25,7 +25,8 @@
(*proof tools*)
val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
val norm_tac: simpset -> tactic (*proves the result*)
- val simplify_meta_eq: simpset -> thm -> thm (*simplifies the result*)
+ val simplify_meta_eq: simpset -> thm -> thm -> thm (*simplifies the result*)
+ val simp_conv: simpset -> term -> thm option (*proves simp thm*)
end;
@@ -58,6 +59,9 @@
and terms2 = Data.dest_sum t2
val u = find_common (terms1,terms2)
+ val simp_th =
+ case Data.simp_conv ss u of NONE => raise TERM("no simp", [])
+ | SOME th => th
val terms1' = Data.find_first u terms1
and terms2' = Data.find_first u terms2
and T = Term.fastype_of u
@@ -66,7 +70,7 @@
Data.prove_conv [Data.norm_tac ss] ctxt prems
(t', Data.mk_bal (Data.mk_sum T (u::terms1'), Data.mk_sum T (u::terms2')))
in
- Option.map (export o Data.simplify_meta_eq ss) reshape
+ Option.map (export o Data.simplify_meta_eq ss simp_th) reshape
end
(* FIXME avoid handling of generic exceptions *)
handle TERM _ => NONE
--- a/src/Provers/blast.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Provers/blast.ML Mon Mar 23 08:16:24 2009 +0100
@@ -48,7 +48,6 @@
val contr_tac : int -> tactic
val dup_intr : thm -> thm
val hyp_subst_tac : bool -> int -> tactic
- val claset : unit -> claset
val rep_cs : (* dependent on classical.ML *)
claset -> {safeIs: thm list, safeEs: thm list,
hazIs: thm list, hazEs: thm list,
@@ -77,7 +76,6 @@
val depth_tac : claset -> int -> int -> tactic
val depth_limit : int Config.T
val blast_tac : claset -> int -> tactic
- val Blast_tac : int -> tactic
val setup : theory -> theory
(*debugging tools*)
val stats : bool ref
@@ -89,7 +87,7 @@
val instVars : term -> (unit -> unit)
val toTerm : int -> term -> Term.term
val readGoal : theory -> string -> term
- val tryInThy : theory -> int -> string ->
+ val tryInThy : theory -> claset -> int -> string ->
(int->tactic) list * branch list list * (int*int*exn) list
val normBr : branch -> branch
end;
@@ -1283,7 +1281,6 @@
((if !trace then warning ("blast: " ^ s) else ());
Seq.empty);
-fun Blast_tac i = blast_tac (Data.claset()) i;
(*** For debugging: these apply the prover to a subgoal and return
@@ -1294,11 +1291,11 @@
(*Read a string to make an initial, singleton branch*)
fun readGoal thy s = Syntax.read_prop_global thy s |> fromTerm thy |> rand |> mkGoal;
-fun tryInThy thy lim s =
+fun tryInThy thy cs lim s =
let
val state as State {fullTrace = ft, ...} = initialize thy;
val res = timeap prove
- (state, start_timing(), Data.claset(), [initBranch ([readGoal thy s], lim)], I);
+ (state, start_timing(), cs, [initBranch ([readGoal thy s], lim)], I);
val _ = fullTrace := !ft;
in res end;
--- a/src/Provers/clasimp.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Provers/clasimp.ML Mon Mar 23 08:16:24 2009 +0100
@@ -26,8 +26,6 @@
type clasimpset
val get_css: Context.generic -> clasimpset
val map_css: (clasimpset -> clasimpset) -> Context.generic -> Context.generic
- val change_clasimpset: (clasimpset -> clasimpset) -> unit
- val clasimpset: unit -> clasimpset
val local_clasimpset_of: Proof.context -> clasimpset
val addSIs2: clasimpset * thm list -> clasimpset
val addSEs2: clasimpset * thm list -> clasimpset
@@ -42,19 +40,10 @@
val addss': claset * simpset -> claset
val addIffs: clasimpset * thm list -> clasimpset
val delIffs: clasimpset * thm list -> clasimpset
- val AddIffs: thm list -> unit
- val DelIffs: thm list -> unit
- val CLASIMPSET: (clasimpset -> tactic) -> tactic
- val CLASIMPSET': (clasimpset -> 'a -> tactic) -> 'a -> tactic
val clarsimp_tac: clasimpset -> int -> tactic
- val Clarsimp_tac: int -> tactic
val mk_auto_tac: clasimpset -> int -> int -> tactic
val auto_tac: clasimpset -> tactic
- val Auto_tac: tactic
- val auto: unit -> unit
val force_tac: clasimpset -> int -> tactic
- val Force_tac: int -> tactic
- val force: int -> unit
val fast_simp_tac: clasimpset -> int -> tactic
val slow_simp_tac: clasimpset -> int -> tactic
val best_simp_tac: clasimpset -> int -> tactic
@@ -84,9 +73,6 @@
let val (cs', ss') = f (get_css context)
in context |> Classical.map_cs (K cs') |> Simplifier.map_ss (K ss') end;
-fun change_clasimpset f = Context.>> (fn context => (Context.the_theory context; map_css f context));
-fun clasimpset () = (Classical.claset (), Simplifier.simpset ());
-
fun local_clasimpset_of ctxt =
(Classical.local_claset_of ctxt, Simplifier.local_simpset_of ctxt);
@@ -168,9 +154,6 @@
Simplifier.addsimps);
val op delIffs = Library.foldl (delIff Classical.delrules Simplifier.delsimps);
-fun AddIffs thms = change_clasimpset (fn css => css addIffs thms);
-fun DelIffs thms = change_clasimpset (fn css => css delIffs thms);
-
fun addIffs_generic (x, ths) =
Library.foldl (addIff (addXEs, addXIs) (addXEs, addXIs) #1) ((x, ()), ths) |> #1;
@@ -182,19 +165,10 @@
(* tacticals *)
-fun CLASIMPSET tacf state =
- Classical.CLASET (fn cs => Simplifier.SIMPSET (fn ss => tacf (cs, ss))) state;
-
-fun CLASIMPSET' tacf i state =
- Classical.CLASET (fn cs => Simplifier.SIMPSET (fn ss => tacf (cs, ss) i)) state;
-
-
fun clarsimp_tac (cs, ss) =
safe_asm_full_simp_tac ss THEN_ALL_NEW
Classical.clarify_tac (cs addSss ss);
-fun Clarsimp_tac i = clarsimp_tac (clasimpset ()) i;
-
(* auto_tac *)
@@ -231,8 +205,6 @@
end;
fun auto_tac css = mk_auto_tac css 4 2;
-fun Auto_tac st = auto_tac (clasimpset ()) st;
-fun auto () = by Auto_tac;
(* force_tac *)
@@ -242,8 +214,6 @@
Classical.clarify_tac cs' 1,
IF_UNSOLVED (Simplifier.asm_full_simp_tac ss 1),
ALLGOALS (Classical.first_best_tac cs')]) end;
-fun Force_tac i = force_tac (clasimpset ()) i;
-fun force i = by (Force_tac i);
(* basic combinations *)
--- a/src/Provers/classical.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Provers/classical.ML Mon Mar 23 08:16:24 2009 +0100
@@ -69,11 +69,7 @@
val appSWrappers : claset -> wrapper
val appWrappers : claset -> wrapper
- val change_claset: (claset -> claset) -> unit
val claset_of: theory -> claset
- val claset: unit -> claset
- val CLASET: (claset -> tactic) -> tactic
- val CLASET': (claset -> 'a -> tactic) -> 'a -> tactic
val local_claset_of : Proof.context -> claset
val fast_tac : claset -> int -> tactic
@@ -107,24 +103,6 @@
val inst_step_tac : claset -> int -> tactic
val inst0_step_tac : claset -> int -> tactic
val instp_step_tac : claset -> int -> tactic
-
- val AddDs : thm list -> unit
- val AddEs : thm list -> unit
- val AddIs : thm list -> unit
- val AddSDs : thm list -> unit
- val AddSEs : thm list -> unit
- val AddSIs : thm list -> unit
- val Delrules : thm list -> unit
- val Safe_tac : tactic
- val Safe_step_tac : int -> tactic
- val Clarify_tac : int -> tactic
- val Clarify_step_tac : int -> tactic
- val Step_tac : int -> tactic
- val Fast_tac : int -> tactic
- val Best_tac : int -> tactic
- val Slow_tac : int -> tactic
- val Slow_best_tac : int -> tactic
- val Deepen_tac : int -> int -> tactic
end;
signature CLASSICAL =
@@ -870,23 +848,9 @@
fun map_context_cs f = GlobalClaset.map (apsnd
(fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
-fun change_claset f = Context.>> (Context.map_theory (map_claset f));
-
fun claset_of thy =
let val (cs, ctxt_cs) = GlobalClaset.get thy
in context_cs (ProofContext.init thy) cs (ctxt_cs) end;
-val claset = claset_of o ML_Context.the_global_context;
-
-fun CLASET tacf st = tacf (claset_of (Thm.theory_of_thm st)) st;
-fun CLASET' tacf i st = tacf (claset_of (Thm.theory_of_thm st)) i st;
-
-fun AddDs args = change_claset (fn cs => cs addDs args);
-fun AddEs args = change_claset (fn cs => cs addEs args);
-fun AddIs args = change_claset (fn cs => cs addIs args);
-fun AddSDs args = change_claset (fn cs => cs addSDs args);
-fun AddSEs args = change_claset (fn cs => cs addSEs args);
-fun AddSIs args = change_claset (fn cs => cs addSIs args);
-fun Delrules args = change_claset (fn cs => cs delrules args);
(* context dependent components *)
@@ -930,21 +894,6 @@
val rule_del = attrib delrule o ContextRules.rule_del;
-(* tactics referring to the implicit claset *)
-
-(*the abstraction over the proof state delays the dereferencing*)
-fun Safe_tac st = safe_tac (claset()) st;
-fun Safe_step_tac i st = safe_step_tac (claset()) i st;
-fun Clarify_step_tac i st = clarify_step_tac (claset()) i st;
-fun Clarify_tac i st = clarify_tac (claset()) i st;
-fun Step_tac i st = step_tac (claset()) i st;
-fun Fast_tac i st = fast_tac (claset()) i st;
-fun Best_tac i st = best_tac (claset()) i st;
-fun Slow_tac i st = slow_tac (claset()) i st;
-fun Slow_best_tac i st = slow_best_tac (claset()) i st;
-fun Deepen_tac m = deepen_tac (claset()) m;
-
-
end;
@@ -972,15 +921,12 @@
(** proof methods **)
-fun METHOD_CLASET tac ctxt = METHOD (tac ctxt (local_claset_of ctxt));
-fun METHOD_CLASET' tac ctxt = METHOD (HEADGOAL o tac ctxt (local_claset_of ctxt));
-
-
local
-fun some_rule_tac ctxt (CS {xtra_netpair, ...}) facts = SUBGOAL (fn (goal, i) =>
+fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) =>
let
val [rules1, rules2, rules4] = ContextRules.find_rules false facts goal ctxt;
+ val CS {xtra_netpair, ...} = local_claset_of ctxt;
val rules3 = ContextRules.find_rules_netpair true facts goal xtra_netpair;
val rules = rules1 @ rules2 @ rules3 @ rules4;
val ruleq = Drule.multi_resolves facts rules;
@@ -990,16 +936,15 @@
end)
THEN_ALL_NEW Goal.norm_hhf_tac;
-fun rule_tac [] ctxt cs facts = some_rule_tac ctxt cs facts
- | rule_tac rules _ _ facts = Method.rule_tac rules facts;
+in
-fun default_tac rules ctxt cs facts =
- HEADGOAL (rule_tac rules ctxt cs facts) ORELSE
+fun rule_tac ctxt [] facts = some_rule_tac ctxt facts
+ | rule_tac _ rules facts = Method.rule_tac rules facts;
+
+fun default_tac ctxt rules facts =
+ HEADGOAL (rule_tac ctxt rules facts) ORELSE
Class.default_intro_tac ctxt facts;
-in
- val rule = METHOD_CLASET' o rule_tac;
- val default = METHOD_CLASET o default_tac;
end;
@@ -1033,9 +978,11 @@
(** setup_methods **)
val setup_methods =
- Method.setup @{binding default} (Attrib.thms >> default)
+ Method.setup @{binding default}
+ (Attrib.thms >> (fn rules => fn ctxt => METHOD (default_tac ctxt rules)))
"apply some intro/elim rule (potentially classical)" #>
- Method.setup @{binding rule} (Attrib.thms >> rule)
+ Method.setup @{binding rule}
+ (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules)))
"apply some intro/elim rule (potentially classical)" #>
Method.setup @{binding contradiction} (Scan.succeed (K contradiction))
"proof by contradiction" #>
--- a/src/Provers/splitter.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Provers/splitter.ML Mon Mar 23 08:16:24 2009 +0100
@@ -35,8 +35,6 @@
val split_asm_tac : thm list -> int -> tactic
val addsplits : simpset * thm list -> simpset
val delsplits : simpset * thm list -> simpset
- val Addsplits : thm list -> unit
- val Delsplits : thm list -> unit
val split_add: attribute
val split_del: attribute
val split_modifiers : Method.modifier parser list
@@ -453,9 +451,6 @@
in Simplifier.delloop (ss, split_name name asm)
end in Library.foldl delsplit (ss,splits) end;
-fun Addsplits splits = (change_simpset (fn ss => ss addsplits splits));
-fun Delsplits splits = (change_simpset (fn ss => ss delsplits splits));
-
(* attributes *)
--- a/src/Pure/Concurrent/future.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/Concurrent/future.ML Mon Mar 23 08:16:24 2009 +0100
@@ -44,6 +44,7 @@
val join_result: 'a future -> 'a Exn.result
val join: 'a future -> 'a
val map: ('a -> 'b) -> 'a future -> 'b future
+ val interruptible_task: ('a -> 'b) -> 'a -> 'b
val interrupt_task: string -> unit
val cancel_group: group -> unit
val cancel: 'a future -> unit
@@ -236,7 +237,7 @@
fun future_job group (e: unit -> 'a) =
let
val result = ref (NONE: 'a Exn.result option);
- val job = Multithreading.with_attributes (Thread.getAttributes ())
+ val job = Multithreading.with_attributes Multithreading.restricted_interrupts
(fn _ => fn ok =>
let
val res = if ok then Exn.capture e () else Exn.Exn Exn.Interrupt;
@@ -350,6 +351,15 @@
(* cancellation *)
+fun interruptible_task f x =
+ if Multithreading.available then
+ Multithreading.with_attributes
+ (if is_some (thread_data ())
+ then Multithreading.restricted_interrupts
+ else Multithreading.regular_interrupts)
+ (fn _ => f) x
+ else interruptible f x;
+
(*interrupt: permissive signal, may get ignored*)
fun interrupt_task id = SYNCHRONIZED "interrupt"
(fn () => Task_Queue.interrupt_external (! queue) id);
--- a/src/Pure/General/antiquote.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/General/antiquote.ML Mon Mar 23 08:16:24 2009 +0100
@@ -11,11 +11,12 @@
Antiq of Symbol_Pos.T list * Position.T |
Open of Position.T |
Close of Position.T
- val is_antiq: 'a antiquote -> bool
+ val is_text: 'a antiquote -> bool
+ val report: ('a -> unit) -> 'a antiquote -> unit
+ val check_nesting: 'a antiquote list -> unit
val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list
val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
- val read: (Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list) ->
- Symbol_Pos.T list * Position.T -> 'a antiquote list
+ val read: Symbol_Pos.T list * Position.T -> Symbol_Pos.T list antiquote list
end;
structure Antiquote: ANTIQUOTE =
@@ -29,8 +30,18 @@
Open of Position.T |
Close of Position.T;
-fun is_antiq (Text _) = false
- | is_antiq _ = true;
+fun is_text (Text _) = true
+ | is_text _ = false;
+
+
+(* report *)
+
+val report_antiq = Position.report Markup.antiq;
+
+fun report report_text (Text x) = report_text x
+ | report _ (Antiq (_, pos)) = report_antiq pos
+ | report _ (Open pos) = report_antiq pos
+ | report _ (Close pos) = report_antiq pos;
(* check_nesting *)
@@ -83,13 +94,9 @@
(* read *)
-fun report_antiq (Antiq (_, pos)) = Position.report Markup.antiq pos
- | report_antiq _ = ();
-
-fun read _ ([], _) = []
- | read scanner (syms, pos) =
- (case Scan.read Symbol_Pos.stopper (Scan.repeat scanner) syms of
- SOME xs => (List.app report_antiq xs; check_nesting xs; xs)
- | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
+fun read (syms, pos) =
+ (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_text) syms of
+ SOME xs => (List.app (report (K ())) xs; check_nesting xs; xs)
+ | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
end;
--- a/src/Pure/General/markup.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/General/markup.ML Mon Mar 23 08:16:24 2009 +0100
@@ -62,6 +62,14 @@
val propN: string val prop: T
val attributeN: string val attribute: string -> T
val methodN: string val method: string -> T
+ val ML_keywordN: string val ML_keyword: T
+ val ML_identN: string val ML_ident: T
+ val ML_tvarN: string val ML_tvar: T
+ val ML_numeralN: string val ML_numeral: T
+ val ML_charN: string val ML_char: T
+ val ML_stringN: string val ML_string: T
+ val ML_commentN: string val ML_comment: T
+ val ML_malformedN: string val ML_malformed: T
val ML_sourceN: string val ML_source: T
val doc_sourceN: string val doc_source: T
val antiqN: string val antiq: T
@@ -213,6 +221,18 @@
val (methodN, method) = markup_string "method" nameN;
+(* ML syntax *)
+
+val (ML_keywordN, ML_keyword) = markup_elem "ML_keyword";
+val (ML_identN, ML_ident) = markup_elem "ML_ident";
+val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar";
+val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
+val (ML_charN, ML_char) = markup_elem "ML_char";
+val (ML_stringN, ML_string) = markup_elem "ML_string";
+val (ML_commentN, ML_comment) = markup_elem "ML_comment";
+val (ML_malformedN, ML_malformed) = markup_elem "ML_malformed";
+
+
(* embedded source text *)
val (ML_sourceN, ML_source) = markup_elem "ML_source";
--- a/src/Pure/General/markup.scala Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/General/markup.scala Mon Mar 23 08:16:24 2009 +0100
@@ -80,6 +80,18 @@
val DOC_ANTIQ = "doc_antiq"
+ /* ML syntax */
+
+ val ML_KEYWORD = "ML_keyword"
+ val ML_IDENT = "ML_ident"
+ val ML_TVAR = "ML_tvar"
+ val ML_NUMERAL = "ML_numeral"
+ val ML_CHAR = "ML_char"
+ val ML_STRING = "ML_string"
+ val ML_COMMENT = "ML_comment"
+ val ML_MALFORMED = "ML_malformed"
+
+
/* outer syntax */
val KEYWORD_DECL = "keyword_decl"
--- a/src/Pure/General/pretty.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/General/pretty.ML Mon Mar 23 08:16:24 2009 +0100
@@ -19,9 +19,6 @@
a unit for breaking).
*)
-type pprint_args = (output -> unit) * (int -> unit) * (int -> unit) *
- (unit -> unit) * (unit -> unit);
-
signature PRETTY =
sig
val default_indent: string -> int -> output
@@ -49,6 +46,7 @@
val commas: T list -> T list
val enclose: string -> string -> T list -> T
val enum: string -> string -> string -> T list -> T
+ val position: Position.T -> T
val list: string -> string -> T list -> T
val str_list: string -> string -> string list -> T
val big_list: string -> T list -> T
@@ -57,7 +55,8 @@
val setmargin: int -> unit
val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b
val setdepth: int -> unit
- val pprint: T -> pprint_args -> unit
+ val to_ML: T -> ML_Pretty.pretty
+ val from_ML: ML_Pretty.pretty -> T
val symbolicN: string
val output_buffer: T -> Buffer.T
val output: T -> output
@@ -159,6 +158,9 @@
fun enum sep lpar rpar prts = enclose lpar rpar (separate sep prts);
+val position =
+ enum "," "{" "}" o map (fn (x, y) => str (x ^ "=" ^ y)) o Position.properties_of;
+
val list = enum ",";
fun str_list lpar rpar strs = list lpar rpar (map str strs);
@@ -318,20 +320,16 @@
| fmt (Break (true, _)) = Buffer.add (output_spaces 1);
in fmt (prune prt) Buffer.empty end;
-(*ML toplevel pretty printing*)
-fun pprint prt (put_str0, begin_blk, put_brk, put_fbrk, end_blk) =
- let
- fun put_str "" = ()
- | put_str s = put_str0 s;
- fun pp (Block (m, prts, ind, _)) =
- let val (bg, en) = Markup.output m
- in put_str bg; begin_blk ind; pp_lst prts; end_blk (); put_str en end
- | pp (String (s, _)) = put_str s
- | pp (Break (false, wd)) = put_brk wd
- | pp (Break (true, _)) = put_fbrk ()
- and pp_lst [] = ()
- | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
- in pp (prune prt) end;
+
+(* ML toplevel pretty printing *)
+
+fun to_ML (Block (m, prts, ind, _)) = ML_Pretty.Block (Markup.output m, map to_ML prts, ind)
+ | to_ML (String s) = ML_Pretty.String s
+ | to_ML (Break b) = ML_Pretty.Break b;
+
+fun from_ML (ML_Pretty.Block (_, prts, ind)) = blk (ind, map from_ML prts)
+ | from_ML (ML_Pretty.String s) = String s
+ | from_ML (ML_Pretty.Break b) = Break b;
(* output interfaces *)
--- a/src/Pure/General/secure.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/General/secure.ML Mon Mar 23 08:16:24 2009 +0100
@@ -14,6 +14,7 @@
val use_file: ML_NameSpace.nameSpace ->
(string -> unit) * (string -> 'a) -> bool -> string -> unit
val use: string -> unit
+ val toplevel_pp: string list -> string -> unit
val commit: unit -> unit
val system_out: string -> string * int
val system: string -> int
@@ -41,6 +42,8 @@
fun raw_use_text ns = use_text ML_Parse.fix_ints (Position.str_of oo Position.line_file) ns;
fun raw_use_file ns = use_file ML_Parse.fix_ints (Position.str_of oo Position.line_file) ns;
+fun raw_toplevel_pp x =
+ toplevel_pp ML_Parse.fix_ints (Position.str_of oo Position.line_file) Output.ml_output x;
fun use_text ns pos pr verbose txt =
(secure_mltext (); raw_use_text ns pos pr verbose txt);
@@ -50,6 +53,8 @@
fun use name = use_file ML_NameSpace.global Output.ml_output true name;
+fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp path pp);
+
(*commit is dynamically bound!*)
fun commit () = raw_use_text ML_NameSpace.global (0, "") Output.ml_output false "commit();";
@@ -73,5 +78,6 @@
val use_text = Secure.use_text;
val use_file = Secure.use_file;
fun use s = Secure.use s handle ERROR msg => (writeln msg; raise Fail "ML error");
+val toplevel_pp = Secure.toplevel_pp;
val system_out = Secure.system_out;
val system = Secure.system;
--- a/src/Pure/General/table.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/General/table.ML Mon Mar 23 08:16:24 2009 +0100
@@ -383,3 +383,6 @@
structure Inttab = TableFun(type key = int val ord = int_ord);
structure Symtab = TableFun(type key = string val ord = fast_string_ord);
+structure Symreltab = TableFun(type key = string * string
+ val ord = prod_ord fast_string_ord fast_string_ord);
+
--- a/src/Pure/IsaMakefile Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/IsaMakefile Mon Mar 23 08:16:24 2009 +0100
@@ -20,17 +20,17 @@
## Pure
BOOTSTRAP_FILES = ML-Systems/exn.ML ML-Systems/ml_name_space.ML \
- ML-Systems/mosml.ML ML-Systems/multithreading.ML \
- ML-Systems/multithreading_polyml.ML ML-Systems/overloading_smlnj.ML \
- ML-Systems/polyml-4.1.3.ML ML-Systems/polyml-4.1.4.ML \
- ML-Systems/polyml-4.2.0.ML ML-Systems/polyml-5.0.ML \
- ML-Systems/polyml-5.1.ML ML-Systems/polyml-experimental.ML \
- ML-Systems/polyml.ML ML-Systems/polyml_common.ML \
- ML-Systems/polyml_old_compiler4.ML \
- ML-Systems/polyml_old_compiler5.ML ML-Systems/proper_int.ML \
- ML-Systems/smlnj.ML ML-Systems/system_shell.ML \
- ML-Systems/thread_dummy.ML ML-Systems/time_limit.ML \
- ML-Systems/universal.ML
+ ML-Systems/ml_pretty.ML ML-Systems/mosml.ML \
+ ML-Systems/multithreading.ML ML-Systems/multithreading_polyml.ML \
+ ML-Systems/overloading_smlnj.ML ML-Systems/polyml-4.1.3.ML \
+ ML-Systems/polyml-4.1.4.ML ML-Systems/polyml-4.2.0.ML \
+ ML-Systems/polyml-5.0.ML ML-Systems/polyml-5.1.ML \
+ ML-Systems/polyml-experimental.ML ML-Systems/polyml.ML \
+ ML-Systems/polyml_common.ML ML-Systems/polyml_old_compiler4.ML \
+ ML-Systems/polyml_old_compiler5.ML ML-Systems/polyml_pp.ML \
+ ML-Systems/proper_int.ML ML-Systems/smlnj.ML \
+ ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML \
+ ML-Systems/time_limit.ML ML-Systems/universal.ML
RAW: $(OUT)/RAW
@@ -69,7 +69,8 @@
Isar/spec_parse.ML Isar/specification.ML Isar/theory_target.ML \
Isar/toplevel.ML Isar/value_parse.ML ML/ml_antiquote.ML \
ML/ml_context.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML \
- ML/ml_thms.ML ML-Systems/install_pp_polyml.ML Proof/extraction.ML \
+ ML/ml_test.ML ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \
+ ML-Systems/install_pp_polyml-experimental.ML Proof/extraction.ML \
Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \
Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/ROOT.ML \
ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML \
--- a/src/Pure/Isar/proof_context.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML Mon Mar 23 08:16:24 2009 +0100
@@ -36,7 +36,6 @@
val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
val extern_fact: Proof.context -> string -> xstring
val pretty_term_abbrev: Proof.context -> term -> Pretty.T
- val pretty_thm_legacy: thm -> Pretty.T
val pretty_thm: Proof.context -> thm -> Pretty.T
val pretty_thms: Proof.context -> thm list -> Pretty.T
val pretty_fact: Proof.context -> string * thm list -> Pretty.T
@@ -296,10 +295,6 @@
fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt);
-fun pretty_thm_legacy th =
- let val thy = Thm.theory_of_thm th
- in Display.pretty_thm_aux (Syntax.pp_global thy) true false [] th end;
-
fun pretty_thm ctxt th =
let val asms = map Thm.term_of (Assumption.all_assms_of ctxt)
in Display.pretty_thm_aux (Syntax.pp ctxt) false true asms th end;
--- a/src/Pure/Isar/proof_display.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/Isar/proof_display.ML Mon Mar 23 08:16:24 2009 +0100
@@ -6,12 +6,12 @@
signature PROOF_DISPLAY =
sig
- val pprint_context: Proof.context -> pprint_args -> unit
- val pprint_typ: theory -> typ -> pprint_args -> unit
- val pprint_term: theory -> term -> pprint_args -> unit
- val pprint_ctyp: ctyp -> pprint_args -> unit
- val pprint_cterm: cterm -> pprint_args -> unit
- val pprint_thm: thm -> pprint_args -> unit
+ val pp_context: Proof.context -> Pretty.T
+ val pp_thm: thm -> Pretty.T
+ val pp_typ: theory -> typ -> Pretty.T
+ val pp_term: theory -> term -> Pretty.T
+ val pp_ctyp: ctyp -> Pretty.T
+ val pp_cterm: cterm -> Pretty.T
val print_theorems_diff: theory -> theory -> unit
val print_theorems: theory -> unit
val pretty_full_theory: bool -> theory -> Pretty.T
@@ -26,18 +26,20 @@
(* toplevel pretty printing *)
-fun pprint_context ctxt = Pretty.pprint
+fun pp_context ctxt =
(if ! ProofContext.debug then
Pretty.quote (Pretty.big_list "proof context:" (ProofContext.pretty_context ctxt))
else Pretty.str "<context>");
-fun pprint pretty thy = Pretty.pprint o Pretty.quote o pretty (Syntax.init_pretty_global thy);
+fun pp_thm th =
+ let val thy = Thm.theory_of_thm th
+ in Display.pretty_thm_aux (Syntax.pp_global thy) true false [] th end;
-val pprint_typ = pprint Syntax.pretty_typ;
-val pprint_term = pprint Syntax.pretty_term;
-fun pprint_ctyp cT = pprint_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
-fun pprint_cterm ct = pprint_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
-val pprint_thm = Pretty.pprint o ProofContext.pretty_thm_legacy;
+val pp_typ = Pretty.quote oo Syntax.pretty_typ_global;
+val pp_term = Pretty.quote oo Syntax.pretty_term_global;
+
+fun pp_ctyp cT = pp_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
+fun pp_cterm ct = pp_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
(* theorems and theory *)
--- a/src/Pure/Isar/toplevel.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML Mon Mar 23 08:16:24 2009 +0100
@@ -311,7 +311,7 @@
fun controlled_execution f =
f
|> debugging
- |> interruptible;
+ |> Future.interruptible_task;
fun program f =
(f
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/install_pp_polyml-experimental.ML Mon Mar 23 08:16:24 2009 +0100
@@ -0,0 +1,27 @@
+(* Title: Pure/ML-Systems/install_pp_polyml-experimental.ML
+
+Extra toplevel pretty-printing for Poly/ML; experimental version for
+Poly/ML 5.3.
+*)
+
+local
+
+fun pretty_future depth (pretty: 'a * int -> pretty) (x: 'a future) =
+ (case Future.peek x of
+ NONE => PrettyString "<future>"
+ | SOME (Exn.Exn _) => PrettyString "<failed>"
+ | SOME (Exn.Result y) => pretty (y, depth));
+
+fun pretty_lazy depth (pretty: 'a * int -> pretty) (x: 'a lazy) =
+ (case Lazy.peek x of
+ NONE => PrettyString "<lazy>"
+ | SOME (Exn.Exn _) => PrettyString "<failed>"
+ | SOME (Exn.Result y) => pretty (y, depth));
+
+in
+
+val _ = addPrettyPrinter pretty_future;
+val _ = addPrettyPrinter pretty_lazy;
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_pretty.ML Mon Mar 23 08:16:24 2009 +0100
@@ -0,0 +1,16 @@
+(* Title: Pure/ML-Systems/ml_pretty.ML
+ Author: Makarius
+
+Raw datatype for ML pretty printing.
+*)
+
+structure ML_Pretty =
+struct
+
+datatype pretty =
+ Block of (string * string) * pretty list * int |
+ String of string * int |
+ Break of bool * int;
+
+end;
+
--- a/src/Pure/ML-Systems/mosml.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/ML-Systems/mosml.ML Mon Mar 23 08:16:24 2009 +0100
@@ -45,6 +45,7 @@
use "ML-Systems/multithreading.ML";
use "ML-Systems/time_limit.ML";
use "ML-Systems/ml_name_space.ML";
+use "ML-Systems/ml_pretty.ML";
(*low-level pointer equality*)
@@ -118,10 +119,8 @@
Meta.printLength := n);
end;
-(*interface for toplevel pretty printers, see also Pure/pure_setup.ML*)
-(*the documentation refers to an installPP but I couldn't fine it!*)
-fun make_pp path pprint = ();
-fun install_pp _ = ();
+(*dummy implementation*)
+fun toplevel_pp _ _ _ _ _ = ();
(*dummy implementation*)
fun ml_prompts p1 p2 = ();
--- a/src/Pure/ML-Systems/multithreading.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/ML-Systems/multithreading.ML Mon Mar 23 08:16:24 2009 +0100
@@ -21,6 +21,7 @@
val enabled: unit -> bool
val no_interrupts: Thread.threadAttribute list
val regular_interrupts: Thread.threadAttribute list
+ val restricted_interrupts: Thread.threadAttribute list
val with_attributes: Thread.threadAttribute list ->
(Thread.threadAttribute list -> 'a -> 'b) -> 'a -> 'b
val self_critical: unit -> bool
@@ -46,6 +47,9 @@
val regular_interrupts =
[Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
+val restricted_interrupts =
+ [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce];
+
fun with_attributes _ f x = f [] x;
--- a/src/Pure/ML-Systems/multithreading_polyml.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Mon Mar 23 08:16:24 2009 +0100
@@ -69,6 +69,9 @@
val regular_interrupts =
[Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
+val restricted_interrupts =
+ [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce];
+
val safe_interrupts = map
(fn Thread.InterruptState Thread.InterruptAsynch =>
Thread.InterruptState Thread.InterruptAsynchOnce
--- a/src/Pure/ML-Systems/polyml-4.1.3.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-4.1.3.ML Mon Mar 23 08:16:24 2009 +0100
@@ -8,6 +8,7 @@
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/polyml_common.ML";
use "ML-Systems/polyml_old_compiler4.ML";
+use "ML-Systems/polyml_pp.ML";
val pointer_eq = Address.wordEq;
--- a/src/Pure/ML-Systems/polyml-4.1.4.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-4.1.4.ML Mon Mar 23 08:16:24 2009 +0100
@@ -8,6 +8,7 @@
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/polyml_common.ML";
use "ML-Systems/polyml_old_compiler4.ML";
+use "ML-Systems/polyml_pp.ML";
val pointer_eq = Address.wordEq;
--- a/src/Pure/ML-Systems/polyml-4.2.0.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-4.2.0.ML Mon Mar 23 08:16:24 2009 +0100
@@ -7,6 +7,7 @@
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/polyml_common.ML";
use "ML-Systems/polyml_old_compiler4.ML";
+use "ML-Systems/polyml_pp.ML";
val pointer_eq = Address.wordEq;
--- a/src/Pure/ML-Systems/polyml-5.0.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-5.0.ML Mon Mar 23 08:16:24 2009 +0100
@@ -7,6 +7,7 @@
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/polyml_common.ML";
use "ML-Systems/polyml_old_compiler5.ML";
+use "ML-Systems/polyml_pp.ML";
val pointer_eq = PolyML.pointerEq;
--- a/src/Pure/ML-Systems/polyml-5.1.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-5.1.ML Mon Mar 23 08:16:24 2009 +0100
@@ -6,6 +6,7 @@
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/polyml_common.ML";
use "ML-Systems/polyml_old_compiler5.ML";
+use "ML-Systems/polyml_pp.ML";
val pointer_eq = PolyML.pointerEq;
--- a/src/Pure/ML-Systems/polyml-experimental.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-experimental.ML Mon Mar 23 08:16:24 2009 +0100
@@ -12,13 +12,6 @@
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-(* toplevel pretty printers *)
-
-(*dummy version*)
-fun make_pp path pprint = ();
-fun install_pp _ = ();
-
-
(* runtime compilation *)
structure ML_NameSpace =
@@ -75,3 +68,20 @@
in use_text tune str_of_pos name_space (1, name) output verbose txt end;
end;
+
+
+(* toplevel pretty printing *)
+
+fun pretty_ml (PrettyBlock (ind, _, _, prts)) = ML_Pretty.Block (("", ""), map pretty_ml prts, ind)
+ | pretty_ml (PrettyString s) = ML_Pretty.String (s, size s)
+ | pretty_ml (PrettyBreak (wd, _)) = ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2));
+
+fun ml_pretty (ML_Pretty.Block (_, prts, ind)) = PrettyBlock (ind, false, [], map ml_pretty prts)
+ | ml_pretty (ML_Pretty.String (s, _)) = PrettyString s
+ | ml_pretty (ML_Pretty.Break (false, wd)) = PrettyBreak (wd, 0)
+ | ml_pretty (ML_Pretty.Break (true, _)) = PrettyBreak (99999, 0);
+
+fun toplevel_pp tune str_of_pos output (_: string list) pp =
+ use_text tune str_of_pos ML_NameSpace.global (1, "pp") output false
+ ("addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
+
--- a/src/Pure/ML-Systems/polyml.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/ML-Systems/polyml.ML Mon Mar 23 08:16:24 2009 +0100
@@ -68,3 +68,6 @@
in use_text tune str_of_pos name_space (1, name) output verbose txt end;
end;
+
+use "ML-Systems/polyml_pp.ML";
+
--- a/src/Pure/ML-Systems/polyml_common.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML Mon Mar 23 08:16:24 2009 +0100
@@ -10,6 +10,7 @@
use "ML-Systems/time_limit.ML";
use "ML-Systems/system_shell.ML";
use "ML-Systems/ml_name_space.ML";
+use "ML-Systems/ml_pretty.ML";
(** ML system and platform related **)
@@ -73,13 +74,8 @@
fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
-(* toplevel pretty printing (see also Pure/pure_setup.ML) *)
+(* print depth *)
-fun make_pp _ pprint (str, blk, brk, en) _ _ obj =
- pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
- fn () => brk (99999, 0), en);
-
-(*print depth*)
local
val depth = ref 10;
in
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/polyml_pp.ML Mon Mar 23 08:16:24 2009 +0100
@@ -0,0 +1,20 @@
+(* Title: Pure/ML-Systems/polyml_pp.ML
+
+Toplevel pretty printing for Poly/ML before 5.3.
+*)
+
+fun ml_pprint (print, begin_blk, brk, end_blk) =
+ let
+ fun str "" = ()
+ | str s = print s;
+ fun pprint (ML_Pretty.Block ((bg, en), prts, ind)) =
+ (str bg; begin_blk (ind, false); List.app pprint prts; end_blk (); str en)
+ | pprint (ML_Pretty.String (s, _)) = str s
+ | pprint (ML_Pretty.Break (false, wd)) = brk (wd, 0)
+ | pprint (ML_Pretty.Break (true, _)) = brk (99999, 0);
+ in pprint end;
+
+fun toplevel_pp tune str_of_pos output (_: string list) pp =
+ use_text tune str_of_pos ML_NameSpace.global (1, "pp") output false
+ ("install_pp (fn args => fn _ => fn _ => ml_pprint args o Pretty.to_ML o (" ^ pp ^ "))");
+
--- a/src/Pure/ML-Systems/smlnj.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML Mon Mar 23 08:16:24 2009 +0100
@@ -13,6 +13,7 @@
use "ML-Systems/multithreading.ML";
use "ML-Systems/system_shell.ML";
use "ML-Systems/ml_name_space.ML";
+use "ML-Systems/ml_pretty.ML";
(*low-level pointer equality*)
@@ -97,22 +98,6 @@
fun makestring x = "dummy string for SML New Jersey";
-(* toplevel pretty printing (see also Pure/pure_setup.ML) *)
-
-fun make_pp path pprint =
- let
- open PrettyPrint;
-
- fun pp pps obj =
- pprint obj
- (string pps, openHOVBox pps o Rel o dest_int,
- fn wd => break pps {nsp=dest_int wd, offset=0}, fn () => newline pps,
- fn () => closeBox pps);
- in (path, pp) end;
-
-fun install_pp (path, pp) = CompilerPPTable.install_pp path pp;
-
-
(* ML command execution *)
fun use_text (tune: string -> string) _ _ (line: int, name) (print, err) verbose txt =
@@ -144,6 +129,26 @@
("structure " ^ name ^ " = struct end");
+(* toplevel pretty printing *)
+
+fun ml_pprint pps =
+ let
+ fun str "" = ()
+ | str s = PrettyPrint.string pps s;
+ fun pprint (ML_Pretty.Block ((bg, en), prts, ind)) =
+ (str bg; PrettyPrint.openHOVBox pps (PrettyPrint.Rel (dest_int ind));
+ List.app pprint prts; PrettyPrint.closeBox pps; str en)
+ | pprint (ML_Pretty.String (s, _)) = str s
+ | pprint (ML_Pretty.Break (false, wd)) = PrettyPrint.break pps {nsp = dest_int wd, offset = 0}
+ | pprint (ML_Pretty.Break (true, _)) = PrettyPrint.newline pps;
+ in pprint end;
+
+fun toplevel_pp tune str_of_pos output path pp =
+ use_text tune str_of_pos ML_NameSpace.global (1, "pp") output false
+ ("CompilerPPTable.install_pp [" ^ String.concatWith "," (map (fn s => "\"" ^ s ^ "\"") path) ^
+ "] (fn pps => ml_pprint pps o Pretty.to_ML o (" ^ pp ^ "))");
+
+
(** interrupts **)
--- a/src/Pure/ML/ml_context.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/ML/ml_context.ML Mon Mar 23 08:16:24 2009 +0100
@@ -29,6 +29,8 @@
(Proof.context -> string * string) * Proof.context
val add_antiq: string -> (Position.T -> antiq context_parser) -> unit
val trace: bool ref
+ val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
+ Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
val eval_wrapper: (string -> unit) * (string -> 'a) -> bool ->
Position.T -> Symbol_Pos.text -> unit
val eval: bool -> Position.T -> Symbol_Pos.text -> unit
@@ -190,45 +192,44 @@
>> (fn ((x, pos), y) => Args.src ((x, y), pos));
val struct_name = "Isabelle";
+val begin_env = ML_Lex.tokenize ("structure " ^ struct_name ^ " =\nstruct\n");
+val end_env = ML_Lex.tokenize "end;";
-fun eval_antiquotes (txt, pos) opt_context =
+in
+
+fun eval_antiquotes (ants, pos) opt_context =
let
- val syms = Symbol_Pos.explode (txt, pos);
- val ants = Antiquote.read ML_Lex.scan_antiq (syms, pos);
val opt_ctxt = Option.map (Context.Proof o Context.proof_of) opt_context;
val ((ml_env, ml_body), opt_ctxt') =
- if not (exists Antiquote.is_antiq ants)
- then (("", Symbol.escape (Symbol_Pos.content syms)), opt_ctxt)
+ if forall Antiquote.is_text ants
+ then (([], map (fn Antiquote.Text tok => tok) ants), opt_ctxt)
else
let
val ctxt =
(case opt_ctxt of
- NONE => error ("Unknown context -- cannot expand ML antiquotations" ^
- Position.str_of pos)
+ NONE => error ("No context -- cannot expand ML antiquotations" ^ Position.str_of pos)
| SOME ctxt => Context.proof_of ctxt);
val lex = #1 (OuterKeyword.get_lexicons ());
- fun no_decl _ = ("", "");
+ fun no_decl _ = ([], []);
- fun expand (Antiquote.Text tok) state =
- (K ("", Symbol.escape (ML_Lex.content_of tok)), state)
+ fun expand (Antiquote.Text tok) state = (K ([], [tok]), state)
| expand (Antiquote.Antiq x) (scope, background) =
let
val context = Stack.top scope;
val (f, context') = antiquotation (T.read_antiq lex antiq x) context;
val (decl, background') = f {background = background, struct_name = struct_name};
- in (decl, (Stack.map_top (K context') scope, background')) end
+ val decl' = pairself ML_Lex.tokenize o decl;
+ in (decl', (Stack.map_top (K context') scope, background')) end
| expand (Antiquote.Open _) (scope, background) =
(no_decl, (Stack.push scope, background))
| expand (Antiquote.Close _) (scope, background) =
(no_decl, (Stack.pop scope, background));
val (decls, (_, ctxt')) = fold_map expand ants (Stack.init ctxt, ctxt);
- val ml = decls |> map (fn decl => decl ctxt') |> split_list |> pairself implode;
+ val ml = decls |> map (fn decl => decl ctxt') |> split_list |> pairself flat;
in (ml, SOME (Context.Proof ctxt')) end;
- in (("structure " ^ struct_name ^ " =\nstruct\n" ^ ml_env ^ "end;", ml_body), opt_ctxt') end;
-
-in
+ in ((begin_env @ ml_env @ end_env, ml_body), opt_ctxt') end;
val trace = ref false;
@@ -239,13 +240,15 @@
(*prepare source text*)
val _ = Position.report Markup.ML_source pos;
- val ((env, body), env_ctxt) = eval_antiquotes (txt, pos) (Context.thread_data ());
+ val ants = ML_Lex.read_antiq (Symbol_Pos.explode (txt, pos), pos);
+ val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ())
+ |>> pairself (implode o map ML_Lex.text_of);
val _ = if ! trace then tracing (cat_lines [env, body]) else ();
(*prepare static ML environment*)
val _ = Context.setmp_thread_data env_ctxt
(fn () => (eval_raw Position.none false env; Context.thread_data ())) ()
- |> (fn NONE => () | SOME context' => Context.>> (ML_Env.put (ML_Env.get context')));
+ |> (fn NONE => () | SOME context' => Context.>> (inherit_env context'));
(*eval ML*)
val _ = eval_raw pos verbose body;
--- a/src/Pure/ML/ml_lex.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/ML/ml_lex.ML Mon Mar 23 08:16:24 2009 +0100
@@ -13,15 +13,17 @@
val stopper: token Scan.stopper
val is_regular: token -> bool
val is_improper: token -> bool
- val pos_of: token -> string
+ val pos_of: token -> Position.T
val kind_of: token -> token_kind
val content_of: token -> string
+ val text_of: token -> string
+ val report_token: token -> unit
val keywords: string list
- val scan_antiq: Symbol_Pos.T list -> token Antiquote.antiquote * Symbol_Pos.T list
val source: (Symbol.symbol, 'a) Source.source ->
(token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source)
Source.source) Source.source
val tokenize: string -> token list
+ val read_antiq: Symbol_Pos.T list * Position.T -> token Antiquote.antiquote list
end;
structure ML_Lex: ML_LEX =
@@ -40,10 +42,8 @@
(* position *)
-fun position_of (Token ((pos, _), _)) = pos;
-fun end_position_of (Token ((_, pos), _)) = pos;
-
-val pos_of = Position.str_of o position_of;
+fun pos_of (Token ((pos, _), _)) = pos;
+fun end_pos_of (Token ((_, pos), _)) = pos;
(* control tokens *)
@@ -55,7 +55,7 @@
| is_eof _ = false;
val stopper =
- Scan.stopper (fn [] => eof | toks => mk_eof (end_position_of (List.last toks))) is_eof;
+ Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof;
(* token content *)
@@ -65,6 +65,11 @@
fun kind_of (Token (_, (k, _))) = k;
+fun text_of tok =
+ (case kind_of tok of
+ Error msg => error msg
+ | _ => Symbol.escape (content_of tok));
+
fun is_regular (Token (_, (Error _, _))) = false
| is_regular (Token (_, (EOF, _))) = false
| is_regular _ = true;
@@ -74,6 +79,27 @@
| is_improper _ = false;
+(* markup *)
+
+val token_kind_markup =
+ fn Keyword => Markup.ML_keyword
+ | Ident => Markup.ML_ident
+ | LongIdent => Markup.ML_ident
+ | TypeVar => Markup.ML_tvar
+ | Word => Markup.ML_numeral
+ | Int => Markup.ML_numeral
+ | Real => Markup.ML_numeral
+ | Char => Markup.ML_char
+ | String => Markup.ML_string
+ | Space => Markup.none
+ | Comment => Markup.ML_comment
+ | Error _ => Markup.ML_malformed
+ | EOF => Markup.none;
+
+fun report_token (Token ((pos, _), (kind, _))) =
+ Position.report (token_kind_markup kind) pos;
+
+
(** scanners **)
@@ -182,7 +208,7 @@
end;
-(* token source *)
+(* scan tokens *)
local
@@ -202,20 +228,31 @@
scan_ident >> token Ident ||
scan_typevar >> token TypeVar));
+val scan_antiq = Antiquote.scan || scan_ml >> Antiquote.Text;
+
fun recover msg =
Scan.many (((not o Symbol.is_blank) andf Symbol.is_regular) o symbol)
>> (fn cs => [token (Error msg) cs]);
in
-val scan_antiq = Antiquote.scan || scan_ml >> Antiquote.Text;
-
fun source src =
Symbol_Pos.source (Position.line 1) src
|> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_ml)) (SOME (false, recover));
val tokenize = Source.of_string #> source #> Source.exhaust;
+fun read_antiq (syms, pos) =
+ (Source.of_list syms
+ |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq))
+ (SOME (false, fn msg => recover msg >> map Antiquote.Text))
+ |> Source.exhaust
+ |> tap (List.app (Antiquote.report report_token))
+ |> tap Antiquote.check_nesting
+ |> tap (List.app (fn Antiquote.Text tok => ignore (text_of tok) | _ => ())))
+ handle ERROR msg =>
+ cat_error msg ("The error(s) above occurred in ML source" ^ Position.str_of pos);
+
end;
end;
--- a/src/Pure/ML/ml_parse.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/ML/ml_parse.ML Mon Mar 23 08:16:24 2009 +0100
@@ -20,7 +20,7 @@
fun !!! scan =
let
fun get_pos [] = " (past end-of-file!)"
- | get_pos (tok :: _) = T.pos_of tok;
+ | get_pos (tok :: _) = Position.str_of (T.pos_of tok);
fun err (toks, NONE) = "SML syntax error" ^ get_pos toks
| err (toks, SOME msg) = "SML syntax error" ^ get_pos toks ^ ": " ^ msg;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_test.ML Mon Mar 23 08:16:24 2009 +0100
@@ -0,0 +1,119 @@
+(* Title: Pure/ML/ml_test.ML
+ Author: Makarius
+
+Test of advanced ML compiler invocation in Poly/ML 5.3.
+*)
+
+signature ML_TEST =
+sig
+ val get_result: Proof.context -> PolyML.parseTree option
+ val eval: bool -> bool -> Position.T -> ML_Lex.token list -> unit
+end
+
+structure ML_Test: ML_TEST =
+struct
+
+(* eval ML source tokens *)
+
+structure Result = GenericDataFun
+(
+ type T = PolyML.parseTree option;
+ val empty = NONE;
+ fun extend _ = NONE;
+ fun merge _ _ = NONE;
+);
+
+val get_result = Result.get o Context.Proof;
+
+fun eval do_run verbose pos toks =
+ let
+ val (print, err) = Output.ml_output;
+
+ val input = toks |> map (fn tok =>
+ (serial (), (String.explode (ML_Lex.text_of tok), ML_Lex.pos_of tok)));
+ val index_pos = Inttab.lookup (Inttab.make (map (apsnd snd) input));
+
+ fun pos_of ({file, startLine = line, startPosition = i, endPosition = j, ...}: location) =
+ (case (index_pos i, index_pos j) of
+ (SOME p, SOME q) => Position.encode_range (p, q)
+ | (SOME p, NONE) => p
+ | _ => Position.line_file line file);
+
+ val in_buffer = ref (map (apsnd fst) input);
+ val current_line = ref (the_default 1 (Position.line_of pos));
+ fun get () =
+ (case ! in_buffer of
+ [] => NONE
+ | (_, []) :: rest => (in_buffer := rest; get ())
+ | (i, c :: cs) :: rest =>
+ (in_buffer := (i, cs) :: rest;
+ if c = #"\n" then current_line := ! current_line + 1 else ();
+ SOME c));
+ fun get_index () = (case ! in_buffer of [] => 0 | (i, _) :: _ => i);
+
+ val out_buffer = ref ([]: string list);
+ fun put s = out_buffer := s :: ! out_buffer;
+ fun output () = implode (rev (! out_buffer));
+
+ fun put_message {message, hard, location, context = _} =
+ (put (if hard then "Error: " else "Warning: ");
+ put (Pretty.string_of (Pretty.from_ML (pretty_ml message)));
+ put (Position.str_of (pos_of location) ^ "\n"));
+
+ fun result_fun (parse_tree, code) () =
+ (Context.>> (Result.put parse_tree); (if is_none code then warning "Static Errors" else ()));
+
+ val parameters =
+ [PolyML.Compiler.CPOutStream put,
+ PolyML.Compiler.CPNameSpace ML_Context.name_space,
+ PolyML.Compiler.CPErrorMessageProc put_message,
+ PolyML.Compiler.CPLineNo (fn () => ! current_line),
+ PolyML.Compiler.CPLineOffset get_index,
+ PolyML.Compiler.CPFileName (the_default "ML" (Position.file_of pos)),
+ PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
+ (if do_run then [] else [PolyML.Compiler.CPCompilerResultFun result_fun]);
+ val _ =
+ (while not (List.null (! in_buffer)) do
+ PolyML.compiler (get, parameters) ())
+ handle exn =>
+ (put ("Exception- " ^ General.exnMessage exn ^ " raised");
+ err (output ()); raise exn);
+ in if verbose then print (output ()) else () end;
+
+
+(* ML test command *)
+
+fun ML_test do_run (txt, pos) =
+ let
+ val _ = Position.report Markup.ML_source pos;
+ val ants = ML_Lex.read_antiq (Symbol_Pos.explode (txt, pos), pos);
+ val ((env, body), env_ctxt) = ML_Context.eval_antiquotes (ants, pos) (Context.thread_data ());
+
+ val _ = Context.setmp_thread_data env_ctxt
+ (fn () => (eval true false Position.none env; Context.thread_data ())) ()
+ |> (fn NONE => () | SOME context' => Context.>> (ML_Context.inherit_env context'));
+ val _ = eval do_run true pos body;
+ val _ = eval true false Position.none (ML_Lex.tokenize "structure Isabelle = struct end");
+ in () end;
+
+
+local structure P = OuterParse and K = OuterKeyword in
+
+fun inherit_env (context as Context.Proof lthy) =
+ Context.Proof (LocalTheory.map_contexts (ML_Context.inherit_env context) lthy)
+ | inherit_env context = context;
+
+val _ =
+ OuterSyntax.command "ML_test" "advanced ML compiler test" (K.tag_ml K.thy_decl)
+ (P.ML_source >> (fn src =>
+ Toplevel.generic_theory (ML_Context.exec (fn () => ML_test true src) #> inherit_env)));
+
+val _ =
+ OuterSyntax.command "ML_parse" "advanced ML compiler test (parse only)" (K.tag_ml K.thy_decl)
+ (P.ML_source >> (fn src =>
+ Toplevel.generic_theory (ML_Context.exec (fn () => ML_test false src) #> inherit_env)));
+
+end;
+
+end;
+
--- a/src/Pure/ROOT.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/ROOT.ML Mon Mar 23 08:16:24 2009 +0100
@@ -101,4 +101,6 @@
(*configuration for Proof General*)
cd "ProofGeneral"; use "ROOT.ML"; cd "..";
+if ml_system = "polyml-experimental" then use "ML/ml_test.ML" else ();
use "pure_setup.ML";
+
--- a/src/Pure/Syntax/ast.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/Syntax/ast.ML Mon Mar 23 08:16:24 2009 +0100
@@ -20,7 +20,6 @@
val str_of_ast: ast -> string
val pretty_ast: ast -> Pretty.T
val pretty_rule: ast * ast -> Pretty.T
- val pprint_ast: ast -> pprint_args -> unit
val fold_ast: string -> ast list -> ast
val fold_ast_p: string -> ast list * ast -> ast
val unfold_ast: string -> ast -> ast list
@@ -79,8 +78,6 @@
| pretty_ast (Appl asts) =
Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
-val pprint_ast = Pretty.pprint o pretty_ast;
-
fun pretty_rule (lhs, rhs) =
Pretty.block [pretty_ast lhs, Pretty.str " ->", Pretty.brk 2, pretty_ast rhs];
--- a/src/Pure/Thy/latex.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/Thy/latex.ML Mon Mar 23 08:16:24 2009 +0100
@@ -117,7 +117,7 @@
else if T.is_kind T.Verbatim tok then
let
val (txt, pos) = T.source_position_of tok;
- val ants = Antiquote.read Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
+ val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
val out = implode (map output_syms_antiq ants);
in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
else output_syms s
--- a/src/Pure/Thy/thy_output.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML Mon Mar 23 08:16:24 2009 +0100
@@ -156,9 +156,9 @@
end
| expand (Antiquote.Open _) = ""
| expand (Antiquote.Close _) = "";
- val ants = Antiquote.read Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
+ val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
in
- if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
+ if Toplevel.is_toplevel state andalso not (forall Antiquote.is_text ants) then
error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos)
else implode (map expand ants)
end;
--- a/src/Pure/context.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/context.ML Mon Mar 23 08:16:24 2009 +0100
@@ -27,8 +27,6 @@
val display_names: theory -> string list
val pretty_thy: theory -> Pretty.T
val string_of_thy: theory -> string
- val pprint_thy: theory -> pprint_args -> unit
- val pprint_thy_ref: theory_ref -> pprint_args -> unit
val pretty_abbrev_thy: theory -> Pretty.T
val str_of_thy: theory -> string
val deref: theory_ref -> theory
@@ -228,7 +226,6 @@
val pretty_thy = Pretty.str_list "{" "}" o display_names;
val string_of_thy = Pretty.string_of o pretty_thy;
-val pprint_thy = Pretty.pprint o pretty_thy;
fun pretty_abbrev_thy thy =
let
@@ -256,8 +253,6 @@
else thy_ref
end;
-val pprint_thy_ref = Pretty.pprint o pretty_thy o deref;
-
(* build ids *)
--- a/src/Pure/mk Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/mk Mon Mar 23 08:16:24 2009 +0100
@@ -92,6 +92,7 @@
-e "val ml_platform = \"$ML_PLATFORM\";" \
-e "use\"$COMPAT\" handle _ => exit 1;" \
-e "structure Isar = struct fun main () = () end;" \
+ -e "ml_prompts \"ML> \" \"ML# \";" \
-q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1
RC="$?"
elif [ -n "$RAW_SESSION" ]; then
@@ -112,6 +113,7 @@
-e "val ml_system = \"$ML_SYSTEM\";" \
-e "val ml_platform = \"$ML_PLATFORM\";" \
-e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
+ -e "ml_prompts \"ML> \" \"ML# \";" \
-f -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
RC="$?"
fi
--- a/src/Pure/pure_setup.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/pure_setup.ML Mon Mar 23 08:16:24 2009 +0100
@@ -27,29 +27,30 @@
(* ML toplevel pretty printing *)
-install_pp (make_pp ["Task_Queue", "task"] (Pretty.pprint o Pretty.str o Task_Queue.str_of_task));
-install_pp (make_pp ["Task_Queue", "group"] (Pretty.pprint o Pretty.str o Task_Queue.str_of_group));
-install_pp (make_pp ["Position", "T"] (Pretty.pprint o Pretty.enum "," "{" "}" o
- map (fn (x, y) => Pretty.str (x ^ "=" ^ y)) o Position.properties_of));
-install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm);
-install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm);
-install_pp (make_pp ["Binding", "binding"] (Pretty.pprint o Pretty.str o quote o Binding.str_of));
-install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp);
-install_pp (make_pp ["Context", "theory"] Context.pprint_thy);
-install_pp (make_pp ["Context", "theory_ref"] Context.pprint_thy_ref);
-install_pp (make_pp ["Context", "proof"] ProofDisplay.pprint_context);
-install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast);
-install_pp (make_pp ["typ"] (ProofDisplay.pprint_typ Pure.thy));
-install_pp (make_pp ["Path", "T"] (Pretty.pprint o Pretty.str o quote o Path.implode));
-install_pp (make_pp ["File", "ident"] (Pretty.pprint o Pretty.str o quote o File.rep_ident));
+toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
+toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
+toplevel_pp ["Position", "T"] "Pretty.position";
+toplevel_pp ["Binding", "binding"] "Pretty.str o quote o Binding.str_of";
+toplevel_pp ["Thm", "thm"] "ProofDisplay.pp_thm";
+toplevel_pp ["Thm", "cterm"] "ProofDisplay.pp_cterm";
+toplevel_pp ["Thm", "ctyp"] "ProofDisplay.pp_ctyp";
+toplevel_pp ["typ"] "ProofDisplay.pp_typ Pure.thy";
+toplevel_pp ["Context", "theory"] "Context.pretty_thy";
+toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref";
+toplevel_pp ["Context", "proof"] "ProofDisplay.pp_context";
+toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast";
+toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode";
+toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident";
-if String.isPrefix "polyml" ml_system then use "ML-Systems/install_pp_polyml.ML"
+if File.exists (Path.explode ("ML-Systems/install_pp_" ^ ml_system ^ ".ML"))
+then use ("ML-Systems/install_pp_" ^ ml_system ^ ".ML")
+else if String.isPrefix "polyml" ml_system
+then use "ML-Systems/install_pp_polyml.ML"
else ();
(* misc *)
val cd = File.cd o Path.explode;
-ml_prompts "ML> " "ML# ";
Proofterm.proofs := 0;
--- a/src/Pure/simplifier.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Pure/simplifier.ML Mon Mar 23 08:16:24 2009 +0100
@@ -10,15 +10,8 @@
include BASIC_META_SIMPLIFIER
val change_simpset: (simpset -> simpset) -> unit
val simpset_of: theory -> simpset
- val simpset: unit -> simpset
- val SIMPSET: (simpset -> tactic) -> tactic
- val SIMPSET': (simpset -> 'a -> tactic) -> 'a -> tactic
- val Addsimps: thm list -> unit
- val Delsimps: thm list -> unit
val Addsimprocs: simproc list -> unit
val Delsimprocs: simproc list -> unit
- val Addcongs: thm list -> unit
- val Delcongs: thm list -> unit
val local_simpset_of: Proof.context -> simpset
val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic
val safe_asm_full_simp_tac: simpset -> int -> tactic
@@ -27,11 +20,6 @@
val full_simp_tac: simpset -> int -> tactic
val asm_lr_simp_tac: simpset -> int -> tactic
val asm_full_simp_tac: simpset -> int -> tactic
- val Simp_tac: int -> tactic
- val Asm_simp_tac: int -> tactic
- val Full_simp_tac: int -> tactic
- val Asm_lr_simp_tac: int -> tactic
- val Asm_full_simp_tac: int -> tactic
val simplify: simpset -> thm -> thm
val asm_simplify: simpset -> thm -> thm
val full_simplify: simpset -> thm -> thm
@@ -138,17 +126,9 @@
fun map_simpset f = Context.theory_map (map_ss f);
fun change_simpset f = Context.>> (Context.map_theory (map_simpset f));
fun simpset_of thy = MetaSimplifier.context (ProofContext.init thy) (get_ss (Context.Theory thy));
-val simpset = simpset_of o ML_Context.the_global_context;
-fun SIMPSET tacf st = tacf (simpset_of (Thm.theory_of_thm st)) st;
-fun SIMPSET' tacf i st = tacf (simpset_of (Thm.theory_of_thm st)) i st;
-
-fun Addsimps args = change_simpset (fn ss => ss addsimps args);
-fun Delsimps args = change_simpset (fn ss => ss delsimps args);
fun Addsimprocs args = change_simpset (fn ss => ss addsimprocs args);
fun Delsimprocs args = change_simpset (fn ss => ss delsimprocs args);
-fun Addcongs args = change_simpset (fn ss => ss addcongs args);
-fun Delcongs args = change_simpset (fn ss => ss delcongs args);
(* local simpset *)
@@ -283,13 +263,6 @@
val asm_full_simp_tac = generic_simp_tac false (true, true, true);
val safe_asm_full_simp_tac = generic_simp_tac true (true, true, true);
-(*the abstraction over the proof state delays the dereferencing*)
-fun Simp_tac i st = simp_tac (simpset ()) i st;
-fun Asm_simp_tac i st = asm_simp_tac (simpset ()) i st;
-fun Full_simp_tac i st = full_simp_tac (simpset ()) i st;
-fun Asm_lr_simp_tac i st = asm_lr_simp_tac (simpset ()) i st;
-fun Asm_full_simp_tac i st = asm_full_simp_tac (simpset ()) i st;
-
(* conversions *)
--- a/src/Sequents/LK.thy Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Sequents/LK.thy Mon Mar 23 08:16:24 2009 +0100
@@ -226,9 +226,9 @@
lemma split_if: "|- P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"
apply (rule_tac P = Q in cut)
- apply (tactic {* simp_tac (simpset () addsimps @{thms if_P}) 2 *})
+ apply (tactic {* simp_tac (@{simpset} addsimps @{thms if_P}) 2 *})
apply (rule_tac P = "~Q" in cut)
- apply (tactic {* simp_tac (simpset() addsimps @{thms if_not_P}) 2 *})
+ apply (tactic {* simp_tac (@{simpset} addsimps @{thms if_not_P}) 2 *})
apply (tactic {* fast_tac LK_pack 1 *})
done
--- a/src/Tools/code/code_haskell.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Tools/code/code_haskell.ML Mon Mar 23 08:16:24 2009 +0100
@@ -42,18 +42,18 @@
of [] => []
| classbinds => Pretty.enum "," "(" ")" (
map (fn (v, class) =>
- str (class_name class ^ " " ^ Code_Name.lookup_var tyvars v)) classbinds)
+ str (class_name class ^ " " ^ Code_Printer.lookup_var tyvars v)) classbinds)
@@ str " => ";
fun pr_typforall tyvars vs = case map fst vs
of [] => []
| vnames => str "forall " :: Pretty.breaks
- (map (str o Code_Name.lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
+ (map (str o Code_Printer.lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
fun pr_tycoexpr tyvars fxy (tyco, tys) =
brackify fxy (str tyco :: map (pr_typ tyvars BR) tys)
and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
of NONE => pr_tycoexpr tyvars fxy (deresolve tyco, tys)
| SOME (i, pr) => pr (pr_typ tyvars) fxy tys)
- | pr_typ tyvars fxy (ITyVar v) = (str o Code_Name.lookup_var tyvars) v;
+ | pr_typ tyvars fxy (ITyVar v) = (str o Code_Printer.lookup_var tyvars) v;
fun pr_typdecl tyvars (vs, tycoexpr) =
Pretty.block (pr_typcontext tyvars vs @| pr_tycoexpr tyvars NOBR tycoexpr);
fun pr_typscheme tyvars (vs, ty) =
@@ -69,7 +69,7 @@
pr_term tyvars thm vars BR t2
])
| pr_term tyvars thm vars fxy (IVar v) =
- (str o Code_Name.lookup_var vars) v
+ (str o Code_Printer.lookup_var vars) v
| pr_term tyvars thm vars fxy (t as _ `|-> _) =
let
val (binds, t') = Code_Thingol.unfold_abs t;
@@ -127,7 +127,7 @@
| pr_case tyvars thm vars fxy ((_, []), _) = str "error \"empty case\"";
fun pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), []))) =
let
- val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
+ val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
val n = (length o fst o Code_Thingol.unfold_fun) ty;
in
Pretty.chunks [
@@ -150,7 +150,7 @@
| pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) =
let
val eqs = filter (snd o snd) raw_eqs;
- val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
+ val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
fun pr_eq ((ts, t), (thm, _)) =
let
val consts = map_filter
@@ -158,8 +158,8 @@
then NONE else (SOME o Long_Name.base_name o deresolve) c)
((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
val vars = init_syms
- |> Code_Name.intro_vars consts
- |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+ |> Code_Printer.intro_vars consts
+ |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
(insert (op =)) ts []);
in
semicolon (
@@ -182,7 +182,7 @@
end
| pr_stmt (name, Code_Thingol.Datatype (_, (vs, []))) =
let
- val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
+ val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
in
semicolon [
str "data",
@@ -191,7 +191,7 @@
end
| pr_stmt (name, Code_Thingol.Datatype (_, (vs, [(co, [ty])]))) =
let
- val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
+ val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
in
semicolon (
str "newtype"
@@ -204,7 +204,7 @@
end
| pr_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
let
- val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
+ val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
fun pr_co (co, tys) =
concat (
(str o deresolve_base) co
@@ -222,7 +222,7 @@
end
| pr_stmt (name, Code_Thingol.Class (_, (v, (superclasses, classparams)))) =
let
- val tyvars = Code_Name.intro_vars [v] init_syms;
+ val tyvars = Code_Printer.intro_vars [v] init_syms;
fun pr_classparam (classparam, ty) =
semicolon [
(str o deresolve_base) classparam,
@@ -234,7 +234,7 @@
Pretty.block [
str "class ",
Pretty.block (pr_typcontext tyvars [(v, map fst superclasses)]),
- str (deresolve_base name ^ " " ^ Code_Name.lookup_var tyvars v),
+ str (deresolve_base name ^ " " ^ Code_Printer.lookup_var tyvars v),
str " where {"
],
str "};"
@@ -244,7 +244,7 @@
let
val split_abs_pure = (fn (v, _) `|-> t => SOME (v, t) | _ => NONE);
val unfold_abs_pure = Code_Thingol.unfoldr split_abs_pure;
- val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
+ val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
fun pr_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam
of NONE => semicolon [
(str o deresolve_base) classparam,
@@ -259,8 +259,8 @@
val proto_rhs = Code_Thingol.eta_expand k (c_inst, []);
val (vs, rhs) = unfold_abs_pure proto_rhs;
val vars = init_syms
- |> Code_Name.intro_vars (the_list const)
- |> Code_Name.intro_vars vs;
+ |> Code_Printer.intro_vars (the_list const)
+ |> Code_Printer.intro_vars vs;
val lhs = IConst (classparam, ([], tys)) `$$ map IVar vs;
(*dictionaries are not relevant at this late stage*)
in
@@ -288,20 +288,20 @@
let
val module_alias = if is_some module_name then K module_name else raw_module_alias;
val reserved_names = Name.make_context reserved_names;
- val mk_name_module = Code_Name.mk_name_module reserved_names module_prefix module_alias program;
+ val mk_name_module = Code_Printer.mk_name_module reserved_names module_prefix module_alias program;
fun add_stmt (name, (stmt, deps)) =
let
- val (module_name, base) = Code_Name.dest_name name;
+ val (module_name, base) = Code_Printer.dest_name name;
val module_name' = mk_name_module module_name;
val mk_name_stmt = yield_singleton Name.variants;
fun add_fun upper (nsp_fun, nsp_typ) =
let
val (base', nsp_fun') =
- mk_name_stmt (if upper then Code_Name.first_upper base else base) nsp_fun
+ mk_name_stmt (if upper then Code_Printer.first_upper base else base) nsp_fun
in (base', (nsp_fun', nsp_typ)) end;
fun add_typ (nsp_fun, nsp_typ) =
let
- val (base', nsp_typ') = mk_name_stmt (Code_Name.first_upper base) nsp_typ
+ val (base', nsp_typ') = mk_name_stmt (Code_Printer.first_upper base) nsp_typ
in (base', (nsp_fun, nsp_typ')) end;
val add_name = case stmt
of Code_Thingol.Fun _ => add_fun false
@@ -330,7 +330,7 @@
(Graph.get_node program name, Graph.imm_succs program name))
(Graph.strong_conn program |> flat)) Symtab.empty;
fun deresolver name = (fst o the o AList.lookup (op =) ((fst o snd o the
- o Symtab.lookup hs_program) ((mk_name_module o fst o Code_Name.dest_name) name))) name
+ o Symtab.lookup hs_program) ((mk_name_module o fst o Code_Printer.dest_name) name))) name
handle Option => error ("Unknown statement name: " ^ labelled_name name);
in (deresolver, hs_program) end;
@@ -357,7 +357,7 @@
andalso forall (deriv' tycos) tys
| deriv' _ (ITyVar _) = true
in deriv [] tyco end;
- val reserved_names = Code_Name.make_vars reserved_names;
+ val reserved_names = Code_Printer.make_vars reserved_names;
fun pr_stmt qualified = pr_haskell_stmt naming labelled_name
syntax_class syntax_tyco syntax_const reserved_names
(if qualified then deresolver else Long_Name.base_name o deresolver)
--- a/src/Tools/code/code_ml.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Tools/code/code_ml.ML Mon Mar 23 08:16:24 2009 +0100
@@ -50,8 +50,8 @@
val pr_label_classparam = Long_Name.base_name o Long_Name.qualifier;
fun pr_dicts fxy ds =
let
- fun pr_dictvar (v, (_, 1)) = Code_Name.first_upper v ^ "_"
- | pr_dictvar (v, (i, _)) = Code_Name.first_upper v ^ string_of_int (i+1) ^ "_";
+ fun pr_dictvar (v, (_, 1)) = Code_Printer.first_upper v ^ "_"
+ | pr_dictvar (v, (i, _)) = Code_Printer.first_upper v ^ string_of_int (i+1) ^ "_";
fun pr_proj [] p =
p
| pr_proj [p'] p =
@@ -87,7 +87,7 @@
fun pr_term is_closure thm vars fxy (IConst c) =
pr_app is_closure thm vars fxy (c, [])
| pr_term is_closure thm vars fxy (IVar v) =
- str (Code_Name.lookup_var vars v)
+ str (Code_Printer.lookup_var vars v)
| pr_term is_closure thm vars fxy (t as t1 `$ t2) =
(case Code_Thingol.unfold_const_app t
of SOME c_ts => pr_app is_closure thm vars fxy c_ts
@@ -182,7 +182,7 @@
then NONE else (SOME o Long_Name.base_name o deresolve) c)
(Code_Thingol.fold_constnames (insert (op =)) t []);
val vars = reserved_names
- |> Code_Name.intro_vars consts;
+ |> Code_Printer.intro_vars consts;
in
concat [
str "val",
@@ -207,8 +207,8 @@
then NONE else (SOME o Long_Name.base_name o deresolve) c)
((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
val vars = reserved_names
- |> Code_Name.intro_vars consts
- |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+ |> Code_Printer.intro_vars consts
+ |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
(insert (op =)) ts []);
in
concat (
@@ -266,7 +266,7 @@
in Pretty.chunks (ps @| Pretty.block ([p, str ";"])) end
| pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
let
- val w = Code_Name.first_upper v ^ "_";
+ val w = Code_Printer.first_upper v ^ "_";
fun pr_superclass_field (class, classrel) =
(concat o map str) [
pr_label_classrel classrel, ":", "'" ^ v, deresolve class
@@ -362,8 +362,8 @@
let
fun pr_dicts fxy ds =
let
- fun pr_dictvar (v, (_, 1)) = "_" ^ Code_Name.first_upper v
- | pr_dictvar (v, (i, _)) = "_" ^ Code_Name.first_upper v ^ string_of_int (i+1);
+ fun pr_dictvar (v, (_, 1)) = "_" ^ Code_Printer.first_upper v
+ | pr_dictvar (v, (i, _)) = "_" ^ Code_Printer.first_upper v ^ string_of_int (i+1);
fun pr_proj ps p =
fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p
fun pr_dict fxy (DictConst (inst, dss)) =
@@ -395,7 +395,7 @@
fun pr_term is_closure thm vars fxy (IConst c) =
pr_app is_closure thm vars fxy (c, [])
| pr_term is_closure thm vars fxy (IVar v) =
- str (Code_Name.lookup_var vars v)
+ str (Code_Printer.lookup_var vars v)
| pr_term is_closure thm vars fxy (t as t1 `$ t2) =
(case Code_Thingol.unfold_const_app t
of SOME c_ts => pr_app is_closure thm vars fxy c_ts
@@ -468,8 +468,8 @@
val x = Name.variant (map_filter I fished1) "x";
val fished2 = map_index (fillup_param x) fished1;
val (fished3, _) = Name.variants fished2 Name.context;
- val vars' = Code_Name.intro_vars fished3 vars;
- in map (Code_Name.lookup_var vars') fished3 end;
+ val vars' = Code_Printer.intro_vars fished3 vars;
+ in map (Code_Printer.lookup_var vars') fished3 end;
fun pr_stmt (MLExc (name, n)) =
let
val exc_str =
@@ -491,7 +491,7 @@
then NONE else (SOME o Long_Name.base_name o deresolve) c)
(Code_Thingol.fold_constnames (insert (op =)) t []);
val vars = reserved_names
- |> Code_Name.intro_vars consts;
+ |> Code_Printer.intro_vars consts;
in
concat [
str "let",
@@ -511,8 +511,8 @@
then NONE else (SOME o Long_Name.base_name o deresolve) c)
((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
val vars = reserved_names
- |> Code_Name.intro_vars consts
- |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+ |> Code_Printer.intro_vars consts
+ |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
(insert (op =)) ts []);
in concat [
(Pretty.block o Pretty.commas)
@@ -527,8 +527,8 @@
then NONE else (SOME o Long_Name.base_name o deresolve) c)
((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
val vars = reserved_names
- |> Code_Name.intro_vars consts
- |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+ |> Code_Printer.intro_vars consts
+ |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
(insert (op =)) ts []);
in
concat (
@@ -556,7 +556,7 @@
((fold o Code_Thingol.fold_constnames)
(insert (op =)) (map (snd o fst) eqs) []);
val vars = reserved_names
- |> Code_Name.intro_vars consts;
+ |> Code_Printer.intro_vars consts;
val dummy_parms = (map str o fish_params vars o map (fst o fst)) eqs;
in
Pretty.block (
@@ -623,7 +623,7 @@
in Pretty.chunks (ps @| Pretty.block ([p, str ";;"])) end
| pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
let
- val w = "_" ^ Code_Name.first_upper v;
+ val w = "_" ^ Code_Printer.first_upper v;
fun pr_superclass_field (class, classrel) =
(concat o map str) [
deresolve classrel, ":", "'" ^ v, deresolve class
@@ -765,11 +765,11 @@
let
val (x, nsp_typ') = f nsp_typ
in (x, (nsp_fun, nsp_typ')) end;
- val mk_name_module = Code_Name.mk_name_module reserved_names NONE module_alias program;
+ val mk_name_module = Code_Printer.mk_name_module reserved_names NONE module_alias program;
fun mk_name_stmt upper name nsp =
let
- val (_, base) = Code_Name.dest_name name;
- val base' = if upper then Code_Name.first_upper base else base;
+ val (_, base) = Code_Printer.dest_name name;
+ val base' = if upper then Code_Printer.first_upper base else base;
val ([base''], nsp') = Name.variants [base'] nsp;
in (base'', nsp') end;
fun rearrange_fun name (tysm as (vs, ty), raw_eqs) =
@@ -853,7 +853,7 @@
[]
|> fold (fold (insert (op =)) o Graph.imm_succs program) names
|> subtract (op =) names;
- val (module_names, _) = (split_list o map Code_Name.dest_name) names;
+ val (module_names, _) = (split_list o map Code_Printer.dest_name) names;
val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
handle Empty =>
error ("Different namespace prefixes for mutual dependencies:\n"
@@ -863,7 +863,7 @@
val module_name_path = Long_Name.explode module_name;
fun add_dep name name' =
let
- val module_name' = (mk_name_module o fst o Code_Name.dest_name) name';
+ val module_name' = (mk_name_module o fst o Code_Printer.dest_name) name';
in if module_name = module_name' then
map_node module_name_path (Graph.add_edge (name, name'))
else let
@@ -891,7 +891,7 @@
(rev (Graph.strong_conn program)));
fun deresolver prefix name =
let
- val module_name = (fst o Code_Name.dest_name) name;
+ val module_name = (fst o Code_Printer.dest_name) name;
val module_name' = (Long_Name.explode o mk_name_module) module_name;
val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
val stmt_name =
@@ -914,7 +914,7 @@
val module_name = if null stmt_names then raw_module_name else SOME "Code";
val (deresolver, nodes) = ml_node_of_program labelled_name module_name
reserved_names raw_module_alias program;
- val reserved_names = Code_Name.make_vars reserved_names;
+ val reserved_names = Code_Printer.make_vars reserved_names;
fun pr_node prefix (Dummy _) =
NONE
| pr_node prefix (Stmt (_, stmt)) = if null stmt_names orelse
--- a/src/Tools/code/code_name.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Tools/code/code_name.ML Mon Mar 23 08:16:24 2009 +0100
@@ -6,45 +6,20 @@
signature CODE_NAME =
sig
- structure StringPairTab: TABLE
- val first_upper: string -> string
- val first_lower: string -> string
- val dest_name: string -> string * string
-
val purify_var: string -> string
val purify_tvar: string -> string
- val purify_sym: string -> string
- val purify_base: bool -> string -> string
+ val purify_base: string -> string
val check_modulename: string -> string
- type var_ctxt
- val make_vars: string list -> var_ctxt
- val intro_vars: string list -> var_ctxt -> var_ctxt
- val lookup_var: var_ctxt -> string -> string
-
val read_const_exprs: theory -> string list -> string list * string list
- val mk_name_module: Name.context -> string option -> (string -> string option)
- -> 'a Graph.T -> string -> string
end;
structure Code_Name: CODE_NAME =
struct
-(** auxiliary **)
-
-structure StringPairTab =
- TableFun(type key = string * string val ord = prod_ord fast_string_ord fast_string_ord);
-
-val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
-val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
-
-val dest_name =
- apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
-
-
(** purification **)
-fun purify_name upper lower =
+fun purify_name upper =
let
fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'";
val is_junk = not o is_valid andf Symbol.is_regular;
@@ -55,9 +30,8 @@
--| junk))
::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk));
fun upper_lower cs = if upper then nth_map 0 Symbol.to_ascii_upper cs
- else if lower then (if forall Symbol.is_ascii_upper cs
- then map else nth_map 0) Symbol.to_ascii_lower cs
- else cs;
+ else (if forall Symbol.is_ascii_upper cs
+ then map else nth_map 0) Symbol.to_ascii_lower cs;
in
explode
#> scan_valids
@@ -68,7 +42,7 @@
end;
fun purify_var "" = "x"
- | purify_var v = purify_name false true v;
+ | purify_var v = purify_name false v;
fun purify_tvar "" = "'a"
| purify_tvar v =
@@ -81,52 +55,29 @@
(Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.is_regular))
#> implode
#> Long_Name.explode
- #> map (purify_name true false);
+ #> map (purify_name true);
(*FIMXE non-canonical function treating non-canonical names*)
-fun purify_base _ "op &" = "and"
- | purify_base _ "op |" = "or"
- | purify_base _ "op -->" = "implies"
- | purify_base _ "{}" = "empty"
- | purify_base _ "op :" = "member"
- | purify_base _ "op Int" = "intersect"
- | purify_base _ "op Un" = "union"
- | purify_base _ "*" = "product"
- | purify_base _ "+" = "sum"
- | purify_base lower s = if String.isPrefix "op =" s
- then "eq" ^ purify_name false lower s
- else purify_name false lower s;
-
-val purify_sym = purify_base false;
+fun purify_base "op &" = "and"
+ | purify_base "op |" = "or"
+ | purify_base "op -->" = "implies"
+ | purify_base "op :" = "member"
+ | purify_base "*" = "product"
+ | purify_base "+" = "sum"
+ | purify_base s = if String.isPrefix "op =" s
+ then "eq" ^ purify_name false s
+ else purify_name false s;
fun check_modulename mn =
let
val mns = Long_Name.explode mn;
- val mns' = map (purify_name true false) mns;
+ val mns' = map (purify_name true) mns;
in
if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "\n"
^ "perhaps try " ^ quote (Long_Name.implode mns'))
end;
-(** variable name contexts **)
-
-type var_ctxt = string Symtab.table * Name.context;
-
-fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty,
- Name.make_context names);
-
-fun intro_vars names (namemap, namectxt) =
- let
- val (names', namectxt') = Name.variants names namectxt;
- val namemap' = fold2 (curry Symtab.update) names names' namemap;
- in (namemap', namectxt') end;
-
-fun lookup_var (namemap, _) name = case Symtab.lookup namemap name
- of SOME name' => name'
- | NONE => error ("Invalid name in context: " ^ quote name);
-
-
(** misc **)
fun read_const_exprs thy =
@@ -150,22 +101,4 @@
else ([Code_Unit.read_const thy s], []);
in pairself flat o split_list o map read_const_expr end;
-fun mk_name_module reserved_names module_prefix module_alias program =
- let
- fun mk_alias name = case module_alias name
- of SOME name' => name'
- | NONE => name
- |> Long_Name.explode
- |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names))
- |> Long_Name.implode;
- fun mk_prefix name = case module_prefix
- of SOME module_prefix => Long_Name.append module_prefix name
- | NONE => name;
- val tab =
- Symtab.empty
- |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
- o fst o dest_name o fst)
- program
- in the o Symtab.lookup tab end;
-
end;
--- a/src/Tools/code/code_printer.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Tools/code/code_printer.ML Mon Mar 23 08:16:24 2009 +0100
@@ -16,6 +16,13 @@
val semicolon: Pretty.T list -> Pretty.T
val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T
+ val first_upper: string -> string
+ val first_lower: string -> string
+ type var_ctxt
+ val make_vars: string list -> var_ctxt
+ val intro_vars: string list -> var_ctxt -> var_ctxt
+ val lookup_var: var_ctxt -> string -> string
+
type lrx
val L: lrx
val R: lrx
@@ -42,14 +49,14 @@
-> fixity -> 'a list -> Pretty.T)) option * OuterParse.token list
val simple_const_syntax: (int * ((fixity -> iterm -> Pretty.T)
-> fixity -> (iterm * itype) list -> Pretty.T)) option -> const_syntax option
- val gen_pr_app: (thm -> Code_Name.var_ctxt -> const * iterm list -> Pretty.T list)
- -> (thm -> Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
+ val gen_pr_app: (thm -> var_ctxt -> const * iterm list -> Pretty.T list)
+ -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
-> (string -> const_syntax option) -> Code_Thingol.naming
- -> thm -> Code_Name.var_ctxt -> fixity -> const * iterm list -> Pretty.T
+ -> thm -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
val gen_pr_bind: ((string option * Pretty.T option) * itype -> Pretty.T)
- -> (thm -> Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
+ -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
-> thm -> fixity
- -> (string option * iterm option) * itype -> Code_Name.var_ctxt -> Pretty.T * Code_Name.var_ctxt
+ -> (string option * iterm option) * itype -> var_ctxt -> Pretty.T * var_ctxt
type literals
val Literals: { literal_char: string -> string, literal_string: string -> string,
@@ -60,6 +67,10 @@
val literal_numeral: literals -> bool -> int -> string
val literal_list: literals -> Pretty.T list -> Pretty.T
val infix_cons: literals -> int * string
+
+ val mk_name_module: Name.context -> string option -> (string -> string option)
+ -> 'a Graph.T -> string -> string
+ val dest_name: string -> string * string
end;
structure Code_Printer : CODE_PRINTER =
@@ -83,6 +94,27 @@
| enum_default default sep opn cls xs = Pretty.enum sep opn cls xs;
+(** names and variable name contexts **)
+
+type var_ctxt = string Symtab.table * Name.context;
+
+fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty,
+ Name.make_context names);
+
+fun intro_vars names (namemap, namectxt) =
+ let
+ val (names', namectxt') = Name.variants names namectxt;
+ val namemap' = fold2 (curry Symtab.update) names names' namemap;
+ in (namemap', namectxt') end;
+
+fun lookup_var (namemap, _) name = case Symtab.lookup namemap name
+ of SOME name' => name'
+ | NONE => error ("Invalid name in context: " ^ quote name);
+
+val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
+val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
+
+
(** syntax printer **)
(* binding priorities *)
@@ -125,8 +157,8 @@
type tyco_syntax = int * ((fixity -> itype -> Pretty.T)
-> fixity -> itype list -> Pretty.T);
-type const_syntax = int * ((Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
- -> Code_Thingol.naming -> thm -> Code_Name.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
+type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
+ -> Code_Thingol.naming -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
fun simple_const_syntax x = (Option.map o apsnd)
(fn pretty => fn pr => fn naming => fn thm => fn vars => pretty (pr vars)) x;
@@ -150,9 +182,9 @@
val vs = case pat
of SOME pat => Code_Thingol.fold_varnames (insert (op =)) pat []
| NONE => [];
- val vars' = Code_Name.intro_vars (the_list v) vars;
- val vars'' = Code_Name.intro_vars vs vars';
- val v' = Option.map (Code_Name.lookup_var vars') v;
+ val vars' = intro_vars (the_list v) vars;
+ val vars'' = intro_vars vs vars';
+ val v' = Option.map (lookup_var vars') v;
val pat' = Option.map (pr_term thm vars'' fxy) pat;
in (pr_bind ((v', pat'), ty), vars'') end;
@@ -239,4 +271,28 @@
val literal_list = #literal_list o dest_Literals;
val infix_cons = #infix_cons o dest_Literals;
+
+(** module name spaces **)
+
+val dest_name =
+ apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
+
+fun mk_name_module reserved_names module_prefix module_alias program =
+ let
+ fun mk_alias name = case module_alias name
+ of SOME name' => name'
+ | NONE => name
+ |> Long_Name.explode
+ |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names))
+ |> Long_Name.implode;
+ fun mk_prefix name = case module_prefix
+ of SOME module_prefix => Long_Name.append module_prefix name
+ | NONE => name;
+ val tab =
+ Symtab.empty
+ |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
+ o fst o dest_name o fst)
+ program
+ in the o Symtab.lookup tab end;
+
end; (*struct*)
--- a/src/Tools/code/code_target.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Tools/code/code_target.ML Mon Mar 23 08:16:24 2009 +0100
@@ -82,11 +82,9 @@
(** theory data **)
-structure StringPairTab = Code_Name.StringPairTab;
-
datatype name_syntax_table = NameSyntaxTable of {
class: string Symtab.table,
- instance: unit StringPairTab.table,
+ instance: unit Symreltab.table,
tyco: tyco_syntax Symtab.table,
const: const_syntax Symtab.table
};
@@ -99,7 +97,7 @@
NameSyntaxTable { class = class2, instance = instance2, tyco = tyco2, const = const2 }) =
mk_name_syntax_table (
(Symtab.join (K snd) (class1, class2),
- StringPairTab.join (K snd) (instance1, instance2)),
+ Symreltab.join (K snd) (instance1, instance2)),
(Symtab.join (K snd) (tyco1, tyco2),
Symtab.join (K snd) (const1, const2))
);
@@ -194,7 +192,7 @@
thy
|> (CodeTargetData.map o apfst oo Symtab.map_default)
(target, mk_target ((serial (), seri), (([], Symtab.empty),
- (mk_name_syntax_table ((Symtab.empty, StringPairTab.empty), (Symtab.empty, Symtab.empty)),
+ (mk_name_syntax_table ((Symtab.empty, Symreltab.empty), (Symtab.empty, Symtab.empty)),
Symtab.empty))))
((map_target o apfst o apsnd o K) seri)
end;
@@ -262,11 +260,11 @@
in if add_del then
thy
|> (map_name_syntax target o apfst o apsnd)
- (StringPairTab.update (inst, ()))
+ (Symreltab.update (inst, ()))
else
thy
|> (map_name_syntax target o apfst o apsnd)
- (StringPairTab.delete_safe inst)
+ (Symreltab.delete_safe inst)
end;
fun gen_add_syntax_tyco prep_tyco target raw_tyco raw_syn thy =
@@ -407,7 +405,7 @@
|>> map_filter I;
val (names_class, class') = distill_names Code_Thingol.lookup_class class;
val names_inst = map_filter (Code_Thingol.lookup_instance naming)
- (StringPairTab.keys instance);
+ (Symreltab.keys instance);
val (names_tyco, tyco') = distill_names Code_Thingol.lookup_tyco tyco;
val (names_const, const') = distill_names Code_Thingol.lookup_const const;
val names_hidden = names_class @ names_inst @ names_tyco @ names_const;
--- a/src/Tools/code/code_thingol.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/Tools/code/code_thingol.ML Mon Mar 23 08:16:24 2009 +0100
@@ -242,7 +242,7 @@
fun namify thy get_basename get_thyname name =
let
val prefix = get_thyname thy name;
- val base = (Code_Name.purify_base true o get_basename) name;
+ val base = (Code_Name.purify_base o get_basename) name;
in Long_Name.append prefix base end;
in
@@ -261,13 +261,11 @@
(* data *)
-structure StringPairTab = Code_Name.StringPairTab;
-
datatype naming = Naming of {
class: class Symtab.table * Name.context,
- classrel: string StringPairTab.table * Name.context,
+ classrel: string Symreltab.table * Name.context,
tyco: string Symtab.table * Name.context,
- instance: string StringPairTab.table * Name.context,
+ instance: string Symreltab.table * Name.context,
const: string Symtab.table * Name.context
}
@@ -275,9 +273,9 @@
val empty_naming = Naming {
class = (Symtab.empty, Name.context),
- classrel = (StringPairTab.empty, Name.context),
+ classrel = (Symreltab.empty, Name.context),
tyco = (Symtab.empty, Name.context),
- instance = (StringPairTab.empty, Name.context),
+ instance = (Symreltab.empty, Name.context),
const = (Symtab.empty, Name.context)
};
@@ -334,22 +332,22 @@
val lookup_class = add_suffix suffix_class
oo Symtab.lookup o fst o #class o dest_Naming;
val lookup_classrel = add_suffix suffix_classrel
- oo StringPairTab.lookup o fst o #classrel o dest_Naming;
+ oo Symreltab.lookup o fst o #classrel o dest_Naming;
val lookup_tyco = add_suffix suffix_tyco
oo Symtab.lookup o fst o #tyco o dest_Naming;
val lookup_instance = add_suffix suffix_instance
- oo StringPairTab.lookup o fst o #instance o dest_Naming;
+ oo Symreltab.lookup o fst o #instance o dest_Naming;
val lookup_const = add_suffix suffix_const
oo Symtab.lookup o fst o #const o dest_Naming;
fun declare_class thy = declare thy map_class
lookup_class Symtab.update_new namify_class;
fun declare_classrel thy = declare thy map_classrel
- lookup_classrel StringPairTab.update_new namify_classrel;
+ lookup_classrel Symreltab.update_new namify_classrel;
fun declare_tyco thy = declare thy map_tyco
lookup_tyco Symtab.update_new namify_tyco;
fun declare_instance thy = declare thy map_instance
- lookup_instance StringPairTab.update_new namify_instance;
+ lookup_instance Symreltab.update_new namify_instance;
fun declare_const thy = declare thy map_const
lookup_const Symtab.update_new namify_const;
--- a/src/ZF/Tools/inductive_package.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/ZF/Tools/inductive_package.ML Mon Mar 23 08:16:24 2009 +0100
@@ -16,7 +16,6 @@
dom_subset : thm, (*inclusion of recursive set in dom*)
intrs : thm list, (*introduction rules*)
elim : thm, (*case analysis theorem*)
- mk_cases : string -> thm, (*generates case theorems*)
induct : thm, (*main induction rule*)
mutual_induct : thm}; (*mutual induction rule*)
@@ -275,9 +274,6 @@
(basic_elim_tac THEN ALLGOALS (asm_full_simp_tac ss) THEN basic_elim_tac)
(Thm.assume A RS elim)
|> Drule.standard';
- fun mk_cases a = make_cases (*delayed evaluation of body!*)
- (simpset ())
- let val thy = Thm.theory_of_thm elim in cterm_of thy (Syntax.read_prop_global thy a) end;
fun induction_rules raw_induct thy =
let
@@ -548,7 +544,6 @@
dom_subset = dom_subset',
intrs = intrs'',
elim = elim',
- mk_cases = mk_cases,
induct = induct,
mutual_induct = mutual_induct})
end;
--- a/src/ZF/int_arith.ML Mon Mar 23 08:14:58 2009 +0100
+++ b/src/ZF/int_arith.ML Mon Mar 23 08:16:24 2009 +0100
@@ -145,7 +145,7 @@
val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys
fun numeral_simp_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
- THEN ALLGOALS (SIMPSET' (fn simpset => asm_simp_tac (Simplifier.inherit_context ss simpset)))
+ THEN ALLGOALS (asm_simp_tac (local_simpset_of (Simplifier.the_context ss)))
val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s @ mult_1s)
end;