# HG changeset patch # User wenzelm # Date 1329256087 -3600 # Node ID f310e9eabf60eafe00dbf32d5ea3987ee19f6719 # Parent c7c85ff6de2a5bf602e39efa45b505d350443294# Parent dac966e4e51d87967cc5fee13b8bb48a5f71d7c4 merged diff -r c7c85ff6de2a -r f310e9eabf60 NEWS --- 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 diff -r c7c85ff6de2a -r f310e9eabf60 doc-src/TutorialI/Protocol/Event.thy --- 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] diff -r c7c85ff6de2a -r f310e9eabf60 doc-src/ZF/ZF_examples.thy --- 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 \ 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] consts acc :: "i => i" diff -r c7c85ff6de2a -r f310e9eabf60 src/HOL/Auth/Event.thy --- 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] diff -r c7c85ff6de2a -r f310e9eabf60 src/HOL/Auth/Smartcard/EventSC.thy --- 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] diff -r c7c85ff6de2a -r f310e9eabf60 src/HOL/Boogie/Tools/boogie_tactics.ML --- 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) diff -r c7c85ff6de2a -r f310e9eabf60 src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy --- 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) (* ------------------------------------------------------------------ *) diff -r c7c85ff6de2a -r f310e9eabf60 src/HOL/IMPP/Natural.thy --- 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-> t ==> ? n. -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 diff -r c7c85ff6de2a -r f310e9eabf60 src/HOL/Prolog/Test.thy --- 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 diff -r c7c85ff6de2a -r f310e9eabf60 src/HOL/Prolog/prolog.ML --- 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 *) diff -r c7c85ff6de2a -r f310e9eabf60 src/HOL/Quotient.thy --- 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 = diff -r c7c85ff6de2a -r f310e9eabf60 src/HOL/SET_Protocol/Event_SET.thy --- 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}*} diff -r c7c85ff6de2a -r f310e9eabf60 src/HOL/Set.thy --- 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 {* diff -r c7c85ff6de2a -r f310e9eabf60 src/HOL/Tools/Function/induction_schema.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 diff -r c7c85ff6de2a -r f310e9eabf60 src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML --- 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 diff -r c7c85ff6de2a -r f310e9eabf60 src/HOL/Tools/Quotient/quotient_tacs.ML --- 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' diff -r c7c85ff6de2a -r f310e9eabf60 src/HOL/Tools/SMT/smt_solver.ML --- 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) diff -r c7c85ff6de2a -r f310e9eabf60 src/HOL/Tools/SMT/z3_proof_reconstruction.ML --- 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') diff -r c7c85ff6de2a -r f310e9eabf60 src/HOL/UNITY/Project.thy --- 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\project h UNIV G \ A ensures B; G \ stable (extend_set h A - extend_set h B) |] ==> extend h F\G \ (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\G \ (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 diff -r c7c85ff6de2a -r f310e9eabf60 src/Provers/classical.ML --- 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); diff -r c7c85ff6de2a -r f310e9eabf60 src/Pure/Isar/method.ML --- 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; diff -r c7c85ff6de2a -r f310e9eabf60 src/Pure/Isar/proof.ML --- 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 *) diff -r c7c85ff6de2a -r f310e9eabf60 src/Pure/Isar/rule_insts.ML --- 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 >> diff -r c7c85ff6de2a -r f310e9eabf60 src/Pure/drule.ML --- 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; diff -r c7c85ff6de2a -r f310e9eabf60 src/Pure/raw_simplifier.ML --- 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; diff -r c7c85ff6de2a -r f310e9eabf60 src/Pure/simplifier.ML --- 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; diff -r c7c85ff6de2a -r f310e9eabf60 src/Pure/tactic.ML --- 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 ***) diff -r c7c85ff6de2a -r f310e9eabf60 src/Pure/tactical.ML --- 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)); diff -r c7c85ff6de2a -r f310e9eabf60 src/Pure/thm.ML --- 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 diff -r c7c85ff6de2a -r f310e9eabf60 src/ZF/AC/Hartog.thy --- 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 \ X" lemma Ords_in_set: "\a. Ord(a) --> a \ X ==> P" -apply (rule_tac X1 = "{y \ X. Ord (y) }" in ON_class [THEN revcut_rl]) +apply (rule_tac X = "{y \ X. Ord (y) }" in ON_class [elim_format]) apply fast done diff -r c7c85ff6de2a -r f310e9eabf60 src/ZF/AC/WO6_WO1.thy --- 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]) diff -r c7c85ff6de2a -r f310e9eabf60 src/ZF/Cardinal.thy --- 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) diff -r c7c85ff6de2a -r f310e9eabf60 src/ZF/Finite.thy --- 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)"