--- a/Admin/isatest/isatest-stats Sat Mar 21 03:24:35 2009 -0700
+++ b/Admin/isatest/isatest-stats Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/Admin/isatest/settings/at-mac-poly-5.1-para Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/NEWS Sat Mar 21 09:42:55 2009 -0700
@@ -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/TutorialI/Protocol/Message.thy Sat Mar 21 03:24:35 2009 -0700
+++ b/doc-src/TutorialI/Protocol/Message.thy Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/doc-src/TutorialI/Protocol/Public.thy Sat Mar 21 09:42:55 2009 -0700
@@ -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/src/CCL/Type.thy Sat Mar 21 03:24:35 2009 -0700
+++ b/src/CCL/Type.thy Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/FOL/blastdata.ML Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/FOL/simpdata.ML Sat Mar 21 09:42:55 2009 -0700
@@ -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/Auth/Message.thy Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOL/Auth/Message.thy Sat Mar 21 09:42:55 2009 -0700
@@ -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/HOL.thy Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOL/HOL.thy Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOL/IMPP/Hoare.thy Sat Mar 21 09:42:55 2009 -0700
@@ -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/Modelcheck/mucke_oracle.ML Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Sat Mar 21 09:42:55 2009 -0700
@@ -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/SET-Protocol/Cardholder_Registration.thy Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOL/SET-Protocol/Cardholder_Registration.thy Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOL/SET-Protocol/MessageSET.thy Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOL/SET-Protocol/PublicSET.thy Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOL/SET-Protocol/Purchase.thy Sat Mar 21 09:42:55 2009 -0700
@@ -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/SizeChange/sct.ML Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOL/SizeChange/sct.ML Sat Mar 21 09:42:55 2009 -0700
@@ -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/cnf_funcs.ML Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOL/Tools/cnf_funcs.ML Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOL/Tools/function_package/fundef_core.ML Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOL/Tools/function_package/mutual.ML Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOL/Tools/function_package/scnp_reconstruct.ML Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOL/Tools/function_package/termination.ML Sat Mar 21 09:42:55 2009 -0700
@@ -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/meson.ML Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOL/Tools/meson.ML Sat Mar 21 09:42:55 2009 -0700
@@ -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/simpdata.ML Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOL/Tools/simpdata.ML Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOL/UNITY/UNITY_tactics.ML Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOL/Word/WordArith.thy Sat Mar 21 09:42:55 2009 -0700
@@ -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},
@@ -1069,10 +1072,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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOL/ex/Classical.thy Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOLCF/FOCUS/Buffer.thy Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOLCF/IOA/Modelcheck/Cockpit.thy Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOLCF/IOA/Modelcheck/Ring3.thy Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOLCF/IOA/ex/TrivEx.thy Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOLCF/IOA/ex/TrivEx2.thy Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOLCF/IOA/meta_theory/Traces.thy Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/HOLCF/Lift.thy Sat Mar 21 09:42:55 2009 -0700
@@ -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/blast.ML Sat Mar 21 03:24:35 2009 -0700
+++ b/src/Provers/blast.ML Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/Provers/clasimp.ML Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/Provers/classical.ML Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/Provers/splitter.ML Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/Pure/Concurrent/future.ML Sat Mar 21 09:42:55 2009 -0700
@@ -236,7 +236,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;
--- a/src/Pure/General/antiquote.ML Sat Mar 21 03:24:35 2009 -0700
+++ b/src/Pure/General/antiquote.ML Sat Mar 21 09:42:55 2009 -0700
@@ -14,7 +14,7 @@
val is_antiq: 'a antiquote -> bool
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) ->
+ val read: ('a -> unit) -> (Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list) ->
Symbol_Pos.T list * Position.T -> 'a antiquote list
end;
@@ -83,13 +83,12 @@
(* read *)
-fun report_antiq (Antiq (_, pos)) = Position.report Markup.antiq pos
- | report_antiq _ = ();
-
-fun read _ ([], _) = []
- | read scanner (syms, pos) =
+fun read _ _ ([], _) = []
+ | read report 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)
+ SOME xs =>
+ (List.app (fn Antiq (_, pos) => Position.report Markup.antiq pos | Text x => report x) xs;
+ check_nesting xs; xs)
| NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
end;
--- a/src/Pure/General/markup.ML Sat Mar 21 03:24:35 2009 -0700
+++ b/src/Pure/General/markup.ML Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/Pure/General/markup.scala Sat Mar 21 09:42:55 2009 -0700
@@ -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/ML-Systems/multithreading.ML Sat Mar 21 03:24:35 2009 -0700
+++ b/src/Pure/ML-Systems/multithreading.ML Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Sat Mar 21 09:42:55 2009 -0700
@@ -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/ml_context.ML Sat Mar 21 03:24:35 2009 -0700
+++ b/src/Pure/ML/ml_context.ML Sat Mar 21 09:42:55 2009 -0700
@@ -194,7 +194,7 @@
fun eval_antiquotes (txt, pos) opt_context =
let
val syms = Symbol_Pos.explode (txt, pos);
- val ants = Antiquote.read ML_Lex.scan_antiq (syms, pos);
+ val ants = Antiquote.read ML_Lex.report_token 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)
--- a/src/Pure/ML/ml_lex.ML Sat Mar 21 03:24:35 2009 -0700
+++ b/src/Pure/ML/ml_lex.ML Sat Mar 21 09:42:55 2009 -0700
@@ -16,6 +16,8 @@
val pos_of: token -> string
val kind_of: token -> token_kind
val content_of: token -> string
+ val markup_of: token -> Markup.T
+ 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 ->
@@ -74,6 +76,26 @@
| is_improper _ = false;
+(* markup *)
+
+val markup_of = kind_of #>
+ (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 tok = Position.report (markup_of tok) (position_of tok);
+
+
(** scanners **)
--- a/src/Pure/Thy/latex.ML Sat Mar 21 03:24:35 2009 -0700
+++ b/src/Pure/Thy/latex.ML Sat Mar 21 09:42:55 2009 -0700
@@ -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 (K ()) Antiquote.scan_text (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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/Pure/Thy/thy_output.ML Sat Mar 21 09:42:55 2009 -0700
@@ -156,7 +156,7 @@
end
| expand (Antiquote.Open _) = ""
| expand (Antiquote.Close _) = "";
- val ants = Antiquote.read Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
+ val ants = Antiquote.read (K ()) Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
in
if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos)
--- a/src/Pure/mk Sat Mar 21 03:24:35 2009 -0700
+++ b/src/Pure/mk Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/Pure/pure_setup.ML Sat Mar 21 09:42:55 2009 -0700
@@ -50,6 +50,5 @@
(* misc *)
val cd = File.cd o Path.explode;
-ml_prompts "ML> " "ML# ";
Proofterm.proofs := 0;
--- a/src/Pure/simplifier.ML Sat Mar 21 03:24:35 2009 -0700
+++ b/src/Pure/simplifier.ML Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/Sequents/LK.thy Sat Mar 21 09:42:55 2009 -0700
@@ -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/ZF/Tools/inductive_package.ML Sat Mar 21 03:24:35 2009 -0700
+++ b/src/ZF/Tools/inductive_package.ML Sat Mar 21 09:42:55 2009 -0700
@@ -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 Sat Mar 21 03:24:35 2009 -0700
+++ b/src/ZF/int_arith.ML Sat Mar 21 09:42:55 2009 -0700
@@ -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;