--- a/NEWS Tue Feb 14 20:13:07 2012 +0100
+++ b/NEWS Tue Feb 14 22:48:07 2012 +0100
@@ -135,14 +135,14 @@
* Renamed facts about the power operation on relations, i.e., relpow
to match the constant's name:
- rel_pow_1 ~> lemma relpow_1
+ rel_pow_1 ~> relpow_1
rel_pow_0_I ~> relpow_0_I
rel_pow_Suc_I ~> relpow_Suc_I
rel_pow_Suc_I2 ~> relpow_Suc_I2
rel_pow_0_E ~> relpow_0_E
rel_pow_Suc_E ~> relpow_Suc_E
rel_pow_E ~> relpow_E
- rel_pow_Suc_D2 ~> lemma relpow_Suc_D2
+ rel_pow_Suc_D2 ~> relpow_Suc_D2
rel_pow_Suc_E2 ~> relpow_Suc_E2
rel_pow_Suc_D2' ~> relpow_Suc_D2'
rel_pow_E2 ~> relpow_E2
--- a/doc-src/TutorialI/Protocol/Event.thy Tue Feb 14 20:13:07 2012 +0100
+++ b/doc-src/TutorialI/Protocol/Event.thy Tue Feb 14 22:48:07 2012 +0100
@@ -139,8 +139,8 @@
text{*Elimination rules: derive contradictions from old Says events containing
items known to be fresh*}
lemmas knows_Spy_partsEs =
- Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard]
- parts.Body [THEN revcut_rl, standard]
+ Says_imp_knows_Spy [THEN parts.Inj, elim_format]
+ parts.Body [elim_format]
lemmas Says_imp_analz_Spy = Says_imp_knows_Spy [THEN analz.Inj]
--- a/doc-src/ZF/ZF_examples.thy Tue Feb 14 20:13:07 2012 +0100
+++ b/doc-src/ZF/ZF_examples.thy Tue Feb 14 22:48:07 2012 +0100
@@ -80,7 +80,7 @@
emptyI: "0 \<in> Fin(A)"
consI: "[| a \<in> A; b \<in> Fin(A) |] ==> cons(a,b) \<in> Fin(A)"
type_intros empty_subsetI cons_subsetI PowI
- type_elims PowD [THEN revcut_rl]
+ type_elims PowD [elim_format]
consts acc :: "i => i"
--- a/src/HOL/Auth/Event.thy Tue Feb 14 20:13:07 2012 +0100
+++ b/src/HOL/Auth/Event.thy Tue Feb 14 22:48:07 2012 +0100
@@ -138,10 +138,10 @@
text{*Elimination rules: derive contradictions from old Says events containing
items known to be fresh*}
lemmas Says_imp_parts_knows_Spy =
- Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl]
+ Says_imp_knows_Spy [THEN parts.Inj, elim_format]
lemmas knows_Spy_partsEs =
- Says_imp_parts_knows_Spy parts.Body [THEN revcut_rl]
+ Says_imp_parts_knows_Spy parts.Body [elim_format]
lemmas Says_imp_analz_Spy = Says_imp_knows_Spy [THEN analz.Inj]
--- a/src/HOL/Auth/Smartcard/EventSC.thy Tue Feb 14 20:13:07 2012 +0100
+++ b/src/HOL/Auth/Smartcard/EventSC.thy Tue Feb 14 22:48:07 2012 +0100
@@ -237,8 +237,8 @@
text{*Elimination rules: derive contradictions from old Says events containing
items known to be fresh*}
lemmas knows_Spy_partsEs =
- Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl]
- parts.Body [THEN revcut_rl]
+ Says_imp_knows_Spy [THEN parts.Inj, elim_format]
+ parts.Body [elim_format]
--- a/src/HOL/Boogie/Tools/boogie_tactics.ML Tue Feb 14 20:13:07 2012 +0100
+++ b/src/HOL/Boogie/Tools/boogie_tactics.ML Tue Feb 14 22:48:07 2012 +0100
@@ -92,7 +92,7 @@
(Rule_Cases.make_common
(Proof_Context.theory_of ctxt,
Thm.prop_of (Rule_Cases.internalize_params st)) (map (rpair []) names))
- Tactical.all_tac st))
+ all_tac st))
in
val setup_boogie_cases = Method.setup @{binding boogie_cases}
(Scan.succeed boogie_cases)
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy Tue Feb 14 20:13:07 2012 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy Tue Feb 14 22:48:07 2012 +0100
@@ -284,7 +284,7 @@
done
-(* generalizing the proof above to a tactic *)
+(* generalizing the proof above to a proof method *)
ML {*
@@ -296,7 +296,7 @@
fun mkex_induct_tac ctxt sch exA exB =
let val ss = simpset_of ctxt in
- EVERY1[Seq_induct_tac ctxt sch defs,
+ EVERY'[Seq_induct_tac ctxt sch defs,
asm_full_simp_tac ss,
SELECT_GOAL (safe_tac (Proof_Context.init_global @{theory Fun})),
Seq_case_simp_tac ctxt exA,
@@ -313,6 +313,11 @@
end
*}
+method_setup mkex_induct = {*
+ Scan.lift (Args.name -- Args.name -- Args.name)
+ >> (fn ((sch, exA), exB) => fn ctxt => SIMPLE_METHOD' (mkex_induct_tac ctxt sch exA exB))
+*}
+
(*---------------------------------------------------------------------------
Projection of mkex(sch,exA,exB) onto A stutters on A
@@ -324,10 +329,7 @@
Filter (%a. a:act A)$sch << filter_act$exA &
Filter (%a. a:act B)$sch << filter_act$exB
--> stutter (asig_of A) (s,ProjA2$(snd (mkex A B sch (s,exA) (t,exB))))"
-
-apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
-done
-
+ by (mkex_induct sch exA exB)
lemma stutter_mkex_on_A: "[|
Forall (%x. x:act (A||B)) sch ;
@@ -354,8 +356,7 @@
Filter (%a. a:act A)$sch << filter_act$exA &
Filter (%a. a:act B)$sch << filter_act$exB
--> stutter (asig_of B) (t,ProjB2$(snd (mkex A B sch (s,exA) (t,exB))))"
-apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
-done
+ by (mkex_induct sch exA exB)
lemma stutter_mkex_on_B: "[|
@@ -385,8 +386,7 @@
Filter (%a. a:act B)$sch << filter_act$exB
--> Filter_ex2 (asig_of A)$(ProjA2$(snd (mkex A B sch (s,exA) (t,exB)))) =
Zip$(Filter (%a. a:act A)$sch)$(Map snd$exA)"
-apply (tactic {* mkex_induct_tac @{context} "sch" "exB" "exA" *})
-done
+ by (mkex_induct sch exB exA)
(*---------------------------------------------------------------------------
zip$(proj1$y)$(proj2$y) = y (using the lift operations)
@@ -448,8 +448,7 @@
Zip$(Filter (%a. a:act B)$sch)$(Map snd$exB)"
(* notice necessary change of arguments exA and exB *)
-apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
-done
+ by (mkex_induct sch exA exB)
(*---------------------------------------------------------------------------
@@ -485,8 +484,7 @@
Filter (%a. a:act B)$sch << filter_act$exB
--> Forall (%x. fst x : act (A ||B))
(snd (mkex A B sch (s,exA) (t,exB)))"
-apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
-done
+ by (mkex_induct sch exA exB)
(* ------------------------------------------------------------------ *)
--- a/src/HOL/IMPP/Natural.thy Tue Feb 14 20:13:07 2012 +0100
+++ b/src/HOL/IMPP/Natural.thy Tue Feb 14 22:48:07 2012 +0100
@@ -140,7 +140,7 @@
lemma evalc_evaln: "<c,s> -c-> t ==> ? n. <c,s> -n-> t"
apply (erule evalc.induct)
apply (tactic {* ALLGOALS (REPEAT o etac exE) *})
-apply (tactic {* TRYALL (EVERY' [datac @{thm evaln_max2} 1, REPEAT o eresolve_tac [exE, conjE]]) *})
+apply (tactic {* TRYALL (EVERY' [dtac @{thm evaln_max2}, assume_tac, REPEAT o eresolve_tac [exE, conjE]]) *})
apply (tactic {* ALLGOALS (rtac exI THEN' resolve_tac @{thms evaln.intros} THEN_ALL_NEW atac) *})
done
--- a/src/HOL/Prolog/Test.thy Tue Feb 14 20:13:07 2012 +0100
+++ b/src/HOL/Prolog/Test.thy Tue Feb 14 22:48:07 2012 +0100
@@ -270,11 +270,5 @@
apply (prolog prog_Test)
back
done
-(*
-back
--> problem with DEPTH_SOLVE:
-Exception- THM ("dest_state", 1, ["P x & P y --> P y"]) raised
-Exception raised at run-time
-*)
end
--- a/src/HOL/Prolog/prolog.ML Tue Feb 14 20:13:07 2012 +0100
+++ b/src/HOL/Prolog/prolog.ML Tue Feb 14 22:48:07 2012 +0100
@@ -71,7 +71,8 @@
(*val hyp_resolve_tac = Subgoal.FOCUS_PREMS (fn {prems, ...} =>
resolve_tac (maps atomizeD prems) 1);
-- is nice, but cannot instantiate unknowns in the assumptions *)
-fun hyp_resolve_tac i st = let
+val hyp_resolve_tac = SUBGOAL (fn (subgoal, i) =>
+ let
fun ap (Const(@{const_name All},_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a ,t))
| ap (Const(@{const_name HOL.implies},_)$_$t) =(case ap t of (k,_,t) => (k,true ,t))
| ap t = (0,false,t);
@@ -83,7 +84,6 @@
val (prems, Const(@{const_name Trueprop}, _)$concl) = rep_goal
(#3(dest_state (st,i)));
*)
- val subgoal = #3(Thm.dest_state (st,i));
val prems = Logic.strip_assums_hyp subgoal;
val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal);
fun drot_tac k i = DETERM (rotate_tac k i);
@@ -104,7 +104,7 @@
else no_tac);
val ptacs = mapn (fn n => fn t =>
pres_tac (ap (HOLogic.dest_Trueprop t)) n i) 0 prems;
- in Library.foldl (op APPEND) (no_tac, ptacs) st end;
+ in Library.foldl (op APPEND) (no_tac, ptacs) end);
fun ptac ctxt prog = let
val proga = maps (atomizeD ctxt) prog (* atomize the prog *)
--- a/src/HOL/Quotient.thy Tue Feb 14 20:13:07 2012 +0100
+++ b/src/HOL/Quotient.thy Tue Feb 14 22:48:07 2012 +0100
@@ -738,41 +738,41 @@
method_setup lifting =
{* Attrib.thms >> (fn thms => fn ctxt =>
- SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt [] thms))) *}
+ SIMPLE_METHOD' (Quotient_Tacs.lift_tac ctxt [] thms)) *}
{* lift theorems to quotient types *}
method_setup lifting_setup =
{* Attrib.thm >> (fn thm => fn ctxt =>
- SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_procedure_tac ctxt [] thm))) *}
+ SIMPLE_METHOD' (Quotient_Tacs.lift_procedure_tac ctxt [] thm)) *}
{* set up the three goals for the quotient lifting procedure *}
method_setup descending =
- {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_tac ctxt []))) *}
+ {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_tac ctxt [])) *}
{* decend theorems to the raw level *}
method_setup descending_setup =
- {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_procedure_tac ctxt []))) *}
+ {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_procedure_tac ctxt [])) *}
{* set up the three goals for the decending theorems *}
method_setup partiality_descending =
- {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.partiality_descend_tac ctxt []))) *}
+ {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_tac ctxt [])) *}
{* decend theorems to the raw level *}
method_setup partiality_descending_setup =
{* Scan.succeed (fn ctxt =>
- SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.partiality_descend_procedure_tac ctxt []))) *}
+ SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_procedure_tac ctxt [])) *}
{* set up the three goals for the decending theorems *}
method_setup regularize =
- {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.regularize_tac ctxt))) *}
+ {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.regularize_tac ctxt)) *}
{* prove the regularization goals from the quotient lifting procedure *}
method_setup injection =
- {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.all_injection_tac ctxt))) *}
+ {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.all_injection_tac ctxt)) *}
{* prove the rep/abs injection goals from the quotient lifting procedure *}
method_setup cleaning =
- {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.clean_tac ctxt))) *}
+ {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.clean_tac ctxt)) *}
{* prove the cleaning goals from the quotient lifting procedure *}
attribute_setup quot_lifted =
--- a/src/HOL/SET_Protocol/Event_SET.thy Tue Feb 14 20:13:07 2012 +0100
+++ b/src/HOL/SET_Protocol/Event_SET.thy Tue Feb 14 22:48:07 2012 +0100
@@ -126,8 +126,8 @@
(*Use with addSEs to derive contradictions from old Says events containing
items known to be fresh*)
lemmas knows_Spy_partsEs =
- Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl]
- parts.Body [THEN revcut_rl]
+ Says_imp_knows_Spy [THEN parts.Inj, elim_format]
+ parts.Body [elim_format]
subsection{*The Function @{term used}*}
--- a/src/HOL/Set.thy Tue Feb 14 20:13:07 2012 +0100
+++ b/src/HOL/Set.thy Tue Feb 14 22:48:07 2012 +0100
@@ -379,7 +379,7 @@
*}
declaration {* fn _ =>
- Classical.map_cs (fn cs => cs addbefore ("bspec", datac @{thm bspec} 1))
+ Classical.map_cs (fn cs => cs addbefore ("bspec", dtac @{thm bspec} THEN' assume_tac))
*}
ML {*
--- a/src/HOL/Tools/Function/induction_schema.ML Tue Feb 14 20:13:07 2012 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML Tue Feb 14 22:48:07 2012 +0100
@@ -344,6 +344,7 @@
fun mk_ind_tac comp_tac pres_tac term_tac ctxt facts =
+ (* FIXME proper use of facts!? *)
(ALLGOALS (Method.insert_tac facts)) THEN HEADGOAL (SUBGOAL (fn (t, i) =>
let
val (ctxt', _, cases, concl) = dest_hhf ctxt t
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Tue Feb 14 20:13:07 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Tue Feb 14 22:48:07 2012 +0100
@@ -308,7 +308,7 @@
val nargs = length (binder_types T)
val pred_case_rule = the_elim_of ctxt pred
in
- REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"}))
+ REPEAT_DETERM (CHANGED (rewrite_goals_tac @{thms split_paired_all}))
THEN print_tac options "before applying elim rule"
THEN etac (predfun_elim_of ctxt pred mode) 1
THEN etac pred_case_rule 1
@@ -385,7 +385,7 @@
val ho_args = ho_args_of mode args
in
etac @{thm bindE} 1
- THEN (REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"})))
+ THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac @{thms split_paired_all})))
THEN print_tac options "prove_expr2-before"
THEN etac (predfun_elim_of ctxt name mode) 1
THEN print_tac options "prove_expr2"
@@ -496,7 +496,7 @@
THEN (prove_clause2 options ctxt pred mode clause i)
in
(DETERM (TRY (rtac @{thm unit.induct} 1)))
- THEN (REPEAT_DETERM (CHANGED (rewtac @{thm split_paired_all})))
+ THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac @{thms split_paired_all})))
THEN (rtac (predfun_intro_of ctxt pred mode) 1)
THEN (REPEAT_DETERM (rtac @{thm refl} 2))
THEN (if null moded_clauses then
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Tue Feb 14 20:13:07 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Tue Feb 14 22:48:07 2012 +0100
@@ -364,7 +364,7 @@
| (_ $
(Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
(Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
- => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
+ => rtac @{thm babs_rsp} THEN' quotient_tac ctxt
| Const (@{const_name HOL.eq},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
(rtac @{thm refl} ORELSE'
--- a/src/HOL/Tools/SMT/smt_solver.ML Tue Feb 14 20:13:07 2012 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML Tue Feb 14 22:48:07 2012 +0100
@@ -39,8 +39,8 @@
{outcome: SMT_Failure.failure option, used_facts: ('a * thm) list}
(*tactic*)
- val smt_tac: Proof.context -> thm list -> int -> Tactical.tactic
- val smt_tac': Proof.context -> thm list -> int -> Tactical.tactic
+ val smt_tac: Proof.context -> thm list -> int -> tactic
+ val smt_tac': Proof.context -> thm list -> int -> tactic
(*setup*)
val setup: theory -> theory
@@ -357,7 +357,7 @@
fun tag_prems thms = map (pair ~1 o pair NONE) thms
fun resolve (SOME thm) = Tactic.rtac thm 1
- | resolve NONE = Tactical.no_tac
+ | resolve NONE = no_tac
fun tac prove ctxt rules =
CONVERSION (SMT_Normalize.atomize_conv ctxt)
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Tue Feb 14 20:13:07 2012 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Tue Feb 14 22:48:07 2012 +0100
@@ -724,14 +724,14 @@
THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))),
Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt [] (fn ctxt' =>
Z3_Proof_Tools.by_tac (
- (Tactic.rtac @{thm iff_allI} ORELSE' K Tactical.all_tac)
+ (Tactic.rtac @{thm iff_allI} ORELSE' K all_tac)
THEN' NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
THEN_ALL_NEW (
NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt')
ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
Z3_Proof_Tools.by_abstraction 0 (true, true) ctxt [] (fn ctxt' =>
Z3_Proof_Tools.by_tac (
- (Tactic.rtac @{thm iff_allI} ORELSE' K Tactical.all_tac)
+ (Tactic.rtac @{thm iff_allI} ORELSE' K all_tac)
THEN' NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
THEN_ALL_NEW (
NAMED ctxt' "fast (full)" (HOL_fast_tac ctxt')
@@ -740,7 +740,7 @@
Z3_Proof_Tools.by_abstraction abstraction_depth (true, true) ctxt []
(fn ctxt' =>
Z3_Proof_Tools.by_tac (
- (Tactic.rtac @{thm iff_allI} ORELSE' K Tactical.all_tac)
+ (Tactic.rtac @{thm iff_allI} ORELSE' K all_tac)
THEN' NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac simpset)
THEN_ALL_NEW (
NAMED ctxt' "fast (deepen)" (HOL_fast_tac ctxt')
--- a/src/HOL/UNITY/Project.thy Tue Feb 14 20:13:07 2012 +0100
+++ b/src/HOL/UNITY/Project.thy Tue Feb 14 22:48:07 2012 +0100
@@ -544,7 +544,7 @@
"[| F\<squnion>project h UNIV G \<in> A ensures B;
G \<in> stable (extend_set h A - extend_set h B) |]
==> extend h F\<squnion>G \<in> (extend_set h A) ensures (extend_set h B)"
-apply (rule project_ensures_D_lemma [of _ UNIV, THEN revcut_rl], auto)
+apply (rule project_ensures_D_lemma [of _ UNIV, elim_format], auto)
done
lemma (in Extend) project_Ensures_D:
@@ -553,7 +553,7 @@
extend_set h B) |]
==> extend h F\<squnion>G \<in> (extend_set h A) Ensures (extend_set h B)"
apply (unfold Ensures_def)
-apply (rule project_ensures_D_lemma [THEN revcut_rl])
+apply (rule project_ensures_D_lemma [elim_format])
apply (auto simp add: project_set_reachable_extend_eq [symmetric])
done
--- a/src/Provers/classical.ML Tue Feb 14 20:13:07 2012 +0100
+++ b/src/Provers/classical.ML Tue Feb 14 22:48:07 2012 +0100
@@ -670,8 +670,8 @@
fun cs addbefore (name, tac1) = cs addWrapper (name, fn _ => fn tac2 => tac1 APPEND' tac2);
fun cs addafter (name, tac2) = cs addWrapper (name, fn _ => fn tac1 => tac1 APPEND' tac2);
-fun cs addD2 (name, thm) = cs addafter (name, datac thm 1);
-fun cs addE2 (name, thm) = cs addafter (name, eatac thm 1);
+fun cs addD2 (name, thm) = cs addafter (name, dtac thm THEN' assume_tac);
+fun cs addE2 (name, thm) = cs addafter (name, etac thm THEN' assume_tac);
fun cs addSD2 (name, thm) = cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
fun cs addSE2 (name, thm) = cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
--- a/src/Pure/Isar/method.ML Tue Feb 14 20:13:07 2012 +0100
+++ b/src/Pure/Isar/method.ML Tue Feb 14 22:48:07 2012 +0100
@@ -4,16 +4,8 @@
Isar proof methods.
*)
-signature BASIC_METHOD =
-sig
- val FINDGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
- val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
- val rule_trace: bool Config.T
-end;
-
signature METHOD =
sig
- include BASIC_METHOD
type method
val apply: (Proof.context -> method) -> Proof.context -> thm list -> cases_tactic
val RAW_METHOD_CASES: (thm list -> cases_tactic) -> method
@@ -42,6 +34,7 @@
val all_assm_tac: Proof.context -> tactic
val assumption: Proof.context -> method
val close: bool -> Proof.context -> method
+ val rule_trace: bool Config.T
val trace: Proof.context -> thm list -> unit
val rule_tac: thm list -> thm list -> int -> tactic
val some_rule_tac: thm list -> Proof.context -> thm list -> int -> tactic
@@ -89,18 +82,6 @@
structure Method: METHOD =
struct
-(** generic tools **)
-
-(* goal addressing *)
-
-fun FINDGOAL tac st =
- let fun find i n = if i > n then Seq.fail else Seq.APPEND (tac i, find (i + 1) n)
- in find 1 (Thm.nprems_of st) st end;
-
-fun HEADGOAL tac = tac 1;
-
-
-
(** proof methods **)
(* datatype method *)
@@ -483,9 +464,6 @@
end;
-structure Basic_Method: BASIC_METHOD = Method;
-open Basic_Method;
-
val RAW_METHOD_CASES = Method.RAW_METHOD_CASES;
val RAW_METHOD = Method.RAW_METHOD;
val METHOD_CASES = Method.METHOD_CASES;
--- a/src/Pure/Isar/proof.ML Tue Feb 14 20:13:07 2012 +0100
+++ b/src/Pure/Isar/proof.ML Tue Feb 14 22:48:07 2012 +0100
@@ -36,7 +36,6 @@
val refine: Method.text -> state -> state Seq.seq
val refine_end: Method.text -> state -> state Seq.seq
val refine_insert: thm list -> state -> state
- val goal_tac: thm -> int -> tactic
val refine_goals: (context -> thm -> unit) -> context -> thm list -> state -> state Seq.seq
val raw_goal: state -> {context: context, facts: thm list, goal: thm}
val goal: state -> {context: context, facts: thm list, goal: thm}
@@ -444,6 +443,8 @@
(* refine via sub-proof *)
+local
+
fun finish_tac 0 = K all_tac
| finish_tac n =
Goal.norm_hhf_tac THEN'
@@ -457,6 +458,12 @@
Tactic.rtac rule THEN'
finish_tac (Thm.nprems_of rule);
+fun FINDGOAL tac st =
+ let fun find i n = if i > n then Seq.fail else Seq.APPEND (tac i, find (i + 1) n)
+ in find 1 (Thm.nprems_of st) st end;
+
+in
+
fun refine_goals print_rule inner raw_rules state =
let
val (outer, (_, goal)) = get_goal state;
@@ -467,6 +474,8 @@
|> (fn rules => Seq.lift set_goal (EVERY (map refine rules) goal) state)
end;
+end;
+
(* conclude_goal *)
--- a/src/Pure/Isar/rule_insts.ML Tue Feb 14 20:13:07 2012 +0100
+++ b/src/Pure/Isar/rule_insts.ML Tue Feb 14 22:48:07 2012 +0100
@@ -15,7 +15,6 @@
val dres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
val thin_tac: Proof.context -> string -> int -> tactic
val subgoal_tac: Proof.context -> string -> int -> tactic
- val subgoals_tac: Proof.context -> string list -> int -> tactic
val method: (Proof.context -> (indexname * string) list -> thm -> int -> tactic) ->
(Proof.context -> thm list -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
end;
@@ -211,11 +210,11 @@
val tinsts = filter_out has_type_var insts;
(* Tactic *)
- fun tac i st =
+ fun tac i st = CSUBGOAL (fn (cgoal, _) =>
let
- val (_, _, Bi, _) = Thm.dest_state (st, i);
- val params = Logic.strip_params Bi; (*params of subgoal i as string typ pairs*)
- val params = rev (Term.rename_wrt_term Bi params)
+ val goal = term_of cgoal;
+ val params = Logic.strip_params goal; (*params of subgoal i as string typ pairs*)
+ val params = rev (Term.rename_wrt_term goal params)
(*as they are printed: bound variables with*)
(*the same name are renamed during printing*)
@@ -267,14 +266,10 @@
val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc);
val rule = Drule.instantiate_normalize
(map lifttvar envT', map liftpair cenv)
- (Thm.lift_rule (Thm.cprem_of st i) thm)
+ (Thm.lift_rule cgoal thm)
in
- if i > nprems_of st then no_tac st
- else st |>
- compose_tac (bires_flag, rule, nprems_of thm) i
- end
- handle TERM (msg,_) => (warning msg; no_tac st)
- | THM (msg,_,_) => (warning msg; no_tac st);
+ compose_tac (bires_flag, rule, nprems_of thm) i
+ end) i st;
in tac end;
val res_inst_tac = bires_inst_tac false;
@@ -314,7 +309,6 @@
(*Introduce the given proposition as lemma and subgoal*)
fun subgoal_tac ctxt A = DETERM o res_inst_tac ctxt [(("psi", 0), A)] cut_rl;
-fun subgoals_tac ctxt As = EVERY' (map (subgoal_tac ctxt) As);
@@ -355,7 +349,8 @@
Method.setup (Binding.name "cut_tac") cut_inst_meth "cut rule (dynamic instantiation)" #>
Method.setup (Binding.name "subgoal_tac")
(Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name_source) >>
- (fn (quant, props) => fn ctxt => SIMPLE_METHOD'' quant (subgoals_tac ctxt props)))
+ (fn (quant, props) => fn ctxt =>
+ SIMPLE_METHOD'' quant (EVERY' (map (subgoal_tac ctxt) props))))
"insert subgoal (dynamic instantiation)" #>
Method.setup (Binding.name "thin_tac")
(Args.goal_spec -- Scan.lift Args.name_source >>
--- a/src/Pure/drule.ML Tue Feb 14 20:13:07 2012 +0100
+++ b/src/Pure/drule.ML Tue Feb 14 22:48:07 2012 +0100
@@ -4,7 +4,7 @@
Derived rules and other operations on theorems.
*)
-infix 0 RS RSN RL RLN MRS MRL OF COMP INCR_COMP COMP_INCR;
+infix 0 RS RSN RL RLN MRS OF COMP INCR_COMP COMP_INCR;
signature BASIC_DRULE =
sig
@@ -35,7 +35,6 @@
val RLN: thm list * (int * thm list) -> thm list
val RL: thm list * thm list -> thm list
val MRS: thm list * thm -> thm
- val MRL: thm list list * thm list -> thm list
val OF: thm * thm list -> thm
val compose: thm * int * thm -> thm list
val COMP: thm * thm -> thm
@@ -390,12 +389,6 @@
| rs_aux i (rl::rls) = rl RSN (i, rs_aux (i+1) rls)
in rs_aux 1 rls end;
-(*As above, but for rule lists*)
-fun rlss MRL bottom_rls =
- let fun rs_aux i [] = bottom_rls
- | rs_aux i (rls::rlss) = rls RLN (i, rs_aux (i+1) rlss)
- in rs_aux 1 rlss end;
-
(*A version of MRS with more appropriate argument order*)
fun bottom_rl OF rls = rls MRS bottom_rl;
--- a/src/Pure/raw_simplifier.ML Tue Feb 14 20:13:07 2012 +0100
+++ b/src/Pure/raw_simplifier.ML Tue Feb 14 22:48:07 2012 +0100
@@ -55,7 +55,6 @@
val rewrite_goals_rule: thm list -> thm -> thm
val rewrite_goals_tac: thm list -> tactic
val rewrite_goal_tac: thm list -> int -> tactic
- val rewtac: thm -> tactic
val prune_params_tac: tactic
val fold_rule: thm list -> thm -> thm
val fold_goals_tac: thm list -> tactic
@@ -124,9 +123,7 @@
val rewrite_term: theory -> thm list -> (term -> term option) list -> term -> term
val rewrite_thm: bool * bool * bool ->
(simpset -> thm -> thm option) -> simpset -> thm -> thm
- val rewrite_goal_rule: bool * bool * bool ->
- (simpset -> thm -> thm option) -> simpset -> int -> thm -> thm
- val asm_rewrite_goal_tac: bool * bool * bool ->
+ val generic_rewrite_goal_tac: bool * bool * bool ->
(simpset -> tactic) -> simpset -> int -> tactic
val rewrite: bool -> thm list -> conv
val simplify: bool -> thm list -> thm -> thm
@@ -1294,28 +1291,21 @@
Conv.fconv_rule (Conv.prems_conv ~1 (rewrite_cterm (true, true, true) simple_prover
(global_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
-(*Rewrite the subgoal of a proof state (represented by a theorem)*)
-fun rewrite_goal_rule mode prover ss i thm =
- if 0 < i andalso i <= Thm.nprems_of thm
- then Conv.gconv_rule (rewrite_cterm mode prover ss) i thm
- else raise THM ("rewrite_goal_rule", i, [thm]);
-
(** meta-rewriting tactics **)
(*Rewrite all subgoals*)
fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
-fun rewtac def = rewrite_goals_tac [def];
(*Rewrite one subgoal*)
-fun asm_rewrite_goal_tac mode prover_tac ss i thm =
+fun generic_rewrite_goal_tac mode prover_tac ss i thm =
if 0 < i andalso i <= Thm.nprems_of thm then
Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ss) i thm)
else Seq.empty;
fun rewrite_goal_tac rews =
let val ss = empty_ss addsimps rews in
- fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac)
+ fn i => fn st => generic_rewrite_goal_tac (true, false, false) (K no_tac)
(global_context (Thm.theory_of_thm st) ss) i st
end;
--- a/src/Pure/simplifier.ML Tue Feb 14 20:13:07 2012 +0100
+++ b/src/Pure/simplifier.ML Tue Feb 14 22:48:07 2012 +0100
@@ -239,7 +239,7 @@
(rev (if safe then solvers else unsafe_solvers)));
fun simp_loop_tac i =
- Raw_Simplifier.asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN
+ Raw_Simplifier.generic_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN
(solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i));
in simp_loop_tac end;
--- a/src/Pure/tactic.ML Tue Feb 14 20:13:07 2012 +0100
+++ b/src/Pure/tactic.ML Tue Feb 14 22:48:07 2012 +0100
@@ -22,9 +22,6 @@
val dtac: thm -> int -> tactic
val etac: thm -> int -> tactic
val ftac: thm -> int -> tactic
- val datac: thm -> int -> int -> tactic
- val eatac: thm -> int -> int -> tactic
- val fatac: thm -> int -> int -> tactic
val ares_tac: thm list -> int -> tactic
val solve_tac: thm list -> int -> tactic
val bimatch_tac: (bool * thm) list -> int -> tactic
@@ -62,7 +59,6 @@
signature TACTIC =
sig
include BASIC_TACTIC
- val innermost_params: int -> thm -> (string * typ) list
val insert_tagged_brl: 'a * (bool * thm) ->
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
@@ -140,9 +136,6 @@
fun dtac rl = dresolve_tac [rl];
fun etac rl = eresolve_tac [rl];
fun ftac rl = forward_tac [rl];
-fun datac thm j = EVERY' (dtac thm::replicate j atac);
-fun eatac thm j = EVERY' (etac thm::replicate j atac);
-fun fatac thm j = EVERY' (ftac thm::replicate j atac);
(*Use an assumption or some rules ... A popular combination!*)
fun ares_tac rules = assume_tac ORELSE' resolve_tac rules;
@@ -183,11 +176,6 @@
val dups = distinct (eq_fst (op aconv)) (goals ~~ (1 upto length goals));
in EVERY (rev (map (distinct_subgoal_tac o snd) dups)) state end;
-(*Determine print names of goal parameters (reversed)*)
-fun innermost_params i st =
- let val (_, _, Bi, _) = Thm.dest_state (st, i)
- in Term.rename_wrt_term Bi (Logic.strip_params Bi) end;
-
(*** Applications of cut_rl ***)
--- a/src/Pure/tactical.ML Tue Feb 14 20:13:07 2012 +0100
+++ b/src/Pure/tactical.ML Tue Feb 14 22:48:07 2012 +0100
@@ -5,7 +5,7 @@
*)
infix 1 THEN THEN' THEN_ALL_NEW;
-infix 0 ORELSE APPEND INTLEAVE ORELSE' APPEND' INTLEAVE';
+infix 0 ORELSE APPEND ORELSE' APPEND';
infix 0 THEN_ELSE;
signature TACTICAL =
@@ -14,12 +14,10 @@
val THEN: tactic * tactic -> tactic
val ORELSE: tactic * tactic -> tactic
val APPEND: tactic * tactic -> tactic
- val INTLEAVE: tactic * tactic -> tactic
val THEN_ELSE: tactic * (tactic*tactic) -> tactic
val THEN': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
val ORELSE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
val APPEND': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
- val INTLEAVE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
val all_tac: tactic
val no_tac: tactic
val DETERM: tactic -> tactic
@@ -50,6 +48,7 @@
val ALLGOALS: (int -> tactic) -> tactic
val SOMEGOAL: (int -> tactic) -> tactic
val FIRSTGOAL: (int -> tactic) -> tactic
+ val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
val REPEAT_SOME: (int -> tactic) -> tactic
val REPEAT_DETERM_SOME: (int -> tactic) -> tactic
val REPEAT_FIRST: (int -> tactic) -> tactic
@@ -100,11 +99,6 @@
fun (tac1 APPEND tac2) st =
Seq.append (tac1 st) (Seq.make(fn()=> Seq.pull (tac2 st)));
-(*Like APPEND, but interleaves results of tac1 and tac2.*)
-fun (tac1 INTLEAVE tac2) st =
- Seq.interleave(tac1 st,
- Seq.make(fn()=> Seq.pull (tac2 st)));
-
(*Conditional tactic.
tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2)
tac1 THEN tac2 = tac1 THEN_ELSE (tac2, no_tac)
@@ -120,7 +114,6 @@
fun (tac1 THEN' tac2) x = tac1 x THEN tac2 x;
fun (tac1 ORELSE' tac2) x = tac1 x ORELSE tac2 x;
fun (tac1 APPEND' tac2) x = tac1 x APPEND tac2 x;
-fun (tac1 INTLEAVE' tac2) x = tac1 x INTLEAVE tac2 x;
(*passes all proofs through unchanged; identity of THEN*)
fun all_tac st = Seq.single st;
@@ -322,6 +315,9 @@
let fun find (i,n) = if i>n then no_tac else tac(i) ORELSE find (i+1,n)
in find(1, nprems_of st)st end;
+(*First subgoal only.*)
+fun HEADGOAL tac = tac 1;
+
(*Repeatedly solve some using tac. *)
fun REPEAT_SOME tac = REPEAT1 (SOMEGOAL (REPEAT1 o tac));
fun REPEAT_DETERM_SOME tac = REPEAT_DETERM1 (SOMEGOAL (REPEAT_DETERM1 o tac));
--- a/src/Pure/thm.ML Tue Feb 14 20:13:07 2012 +0100
+++ b/src/Pure/thm.ML Tue Feb 14 22:48:07 2012 +0100
@@ -136,7 +136,6 @@
val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
val varifyT_global: thm -> thm
val legacy_freezeT: thm -> thm
- val dest_state: thm * int -> (term * term) list * term list * term * term
val lift_rule: cterm -> thm -> thm
val incr_indexes: int -> thm -> thm
val assumption: int -> thm -> thm Seq.seq
--- a/src/ZF/AC/Hartog.thy Tue Feb 14 20:13:07 2012 +0100
+++ b/src/ZF/AC/Hartog.thy Tue Feb 14 22:48:07 2012 +0100
@@ -13,7 +13,7 @@
"Hartog(X) == LEAST i. ~ i \<lesssim> X"
lemma Ords_in_set: "\<forall>a. Ord(a) --> a \<in> X ==> P"
-apply (rule_tac X1 = "{y \<in> X. Ord (y) }" in ON_class [THEN revcut_rl])
+apply (rule_tac X = "{y \<in> X. Ord (y) }" in ON_class [elim_format])
apply fast
done
--- a/src/ZF/AC/WO6_WO1.thy Tue Feb 14 20:13:07 2012 +0100
+++ b/src/ZF/AC/WO6_WO1.thy Tue Feb 14 22:48:07 2012 +0100
@@ -526,7 +526,7 @@
apply (rule allI)
apply (case_tac "A=0")
apply (fast intro!: well_ord_Memrel nat_0I [THEN nat_into_Ord])
-apply (rule_tac x1 = A in lemma_iv [THEN revcut_rl])
+apply (rule_tac x = A in lemma_iv [elim_format])
apply (erule exE)
apply (drule WO6_imp_NN_not_empty)
apply (erule Un_subset_iff [THEN iffD1, THEN conjE])
--- a/src/ZF/Cardinal.thy Tue Feb 14 20:13:07 2012 +0100
+++ b/src/ZF/Cardinal.thy Tue Feb 14 22:48:07 2012 +0100
@@ -869,7 +869,7 @@
apply (simp add: eqpoll_0_iff, clarify)
apply (subgoal_tac "EX u. u:A")
apply (erule exE)
-apply (rule Diff_sing_eqpoll [THEN revcut_rl])
+apply (rule Diff_sing_eqpoll [elim_format])
prefer 2 apply assumption
apply assumption
apply (rule_tac b = A in cons_Diff [THEN subst], assumption)
--- a/src/ZF/Finite.thy Tue Feb 14 20:13:07 2012 +0100
+++ b/src/ZF/Finite.thy Tue Feb 14 22:48:07 2012 +0100
@@ -27,7 +27,7 @@
emptyI: "0 : Fin(A)"
consI: "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)"
type_intros empty_subsetI cons_subsetI PowI
- type_elims PowD [THEN revcut_rl]
+ type_elims PowD [elim_format]
inductive
domains "FiniteFun(A,B)" <= "Fin(A*B)"