# HG changeset patch # User wenzelm # Date 1364392230 -3600 # Node ID c713c9505f6879e40953b189c0f24ddc1a72d0c6 # Parent 88d1d19fb74f451bcd3e1b178937dc0583aed95d clarified Skip_Proof.cheat_tac: more standard tactic; clarified Method.cheating: check quick_and_dirty when it is actually applied; diff -r 88d1d19fb74f -r c713c9505f68 src/HOL/TPTP/atp_problem_import.ML --- a/src/HOL/TPTP/atp_problem_import.ML Wed Mar 27 14:19:18 2013 +0100 +++ b/src/HOL/TPTP/atp_problem_import.ML Wed Mar 27 14:50:30 2013 +0100 @@ -175,7 +175,7 @@ val (outcome, _) = Nitpick.pick_nits_in_term state params Nitpick.Normal i n step subst [] [] conj - in if outcome = "none" then Skip_Proof.cheat_tac thy th else Seq.empty end + in if outcome = "none" then ALLGOALS Skip_Proof.cheat_tac th else Seq.empty end end fun atp_tac ctxt completeness override_params timeout prover = diff -r 88d1d19fb74f -r c713c9505f68 src/HOL/TPTP/sledgehammer_tactics.ML --- a/src/HOL/TPTP/sledgehammer_tactics.ML Wed Mar 27 14:19:18 2013 +0100 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML Wed Mar 27 14:50:30 2013 +0100 @@ -64,12 +64,11 @@ fun sledgehammer_as_oracle_tac ctxt override_params fact_override i th = let - val thy = Proof_Context.theory_of ctxt val override_params = override_params @ [("preplay_timeout", "0"), ("minimize", "false")] val xs = run_prover override_params fact_override i i ctxt th - in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end + in if is_some xs then ALLGOALS Skip_Proof.cheat_tac th else Seq.empty end end; diff -r 88d1d19fb74f -r c713c9505f68 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Mar 27 14:19:18 2013 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Mar 27 14:50:30 2013 +0100 @@ -1180,7 +1180,7 @@ fun define_quickcheck_predicate t thy = let val (vs, t') = strip_abs t - val vs' = Variable.variant_frees (Proof_Context.init_global thy) [] vs + val vs' = Variable.variant_frees (Proof_Context.init_global thy) [] vs (* FIXME proper context!? *) val t'' = subst_bounds (map Free (rev vs'), t') val (prems, concl) = strip_horn t'' val constname = "quickcheck" @@ -1191,8 +1191,9 @@ val t = Logic.list_implies (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]), HOLogic.mk_Trueprop (list_comb (const, map Free vs'))) - val tac = fn _ => Skip_Proof.cheat_tac thy1 - val intro = Goal.prove (Proof_Context.init_global thy1) (map fst vs') [] t tac + val intro = + Goal.prove (Proof_Context.init_global thy1) (map fst vs') [] t + (fn _ => ALLGOALS Skip_Proof.cheat_tac) in ((((full_constname, constT), vs'), intro), thy1) end diff -r 88d1d19fb74f -r c713c9505f68 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed Mar 27 14:19:18 2013 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed Mar 27 14:50:30 2013 +0100 @@ -134,7 +134,7 @@ fun split_all_pairs thy th = let - val ctxt = Proof_Context.init_global thy + val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *) val ((_, [th']), _) = Variable.import true [th] ctxt val t = prop_of th' val frees = Term.add_frees t [] @@ -148,8 +148,9 @@ in ((Free (x, T), HOLogic.mk_ptuple paths T (map Free xTs)), nctxt') end val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt val t' = Pattern.rewrite_term thy rewr [] t - val tac = Skip_Proof.cheat_tac thy - val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn _ => tac) + val th'' = + Goal.prove ctxt (Term.add_free_names t' []) [] t' + (fn _ => ALLGOALS Skip_Proof.cheat_tac) val th''' = Local_Defs.unfold ctxt [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}] th'' in th''' diff -r 88d1d19fb74f -r c713c9505f68 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Wed Mar 27 14:19:18 2013 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Wed Mar 27 14:50:30 2013 +0100 @@ -127,13 +127,13 @@ fun flatten_intros constname intros thy = let - val ctxt = Proof_Context.init_global thy + val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *) val ((_, intros), ctxt') = Variable.import true intros ctxt val (intros', (local_defs, thy')) = (fold_map o fold_map_atoms) (flatten constname) (map prop_of intros) ([], thy) val ctxt'' = Proof_Context.transfer thy' ctxt' - val tac = fn _ => Skip_Proof.cheat_tac thy' - val intros'' = map (fn t => Goal.prove ctxt'' [] [] t tac) intros' + val intros'' = + map (fn t => Goal.prove ctxt'' [] [] t (fn _ => ALLGOALS Skip_Proof.cheat_tac)) intros' |> Variable.export ctxt'' ctxt in (intros'', (local_defs, thy')) diff -r 88d1d19fb74f -r c713c9505f68 src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Wed Mar 27 14:19:18 2013 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Wed Mar 27 14:50:30 2013 +0100 @@ -491,7 +491,7 @@ fun prove_pred options thy clauses preds pred (_, mode) (moded_clauses, compiled_term) = let - val ctxt = Proof_Context.init_global thy + val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *) val clauses = case AList.lookup (op =) clauses pred of SOME rs => rs | NONE => [] in Goal.prove ctxt (Term.add_free_names compiled_term []) [] compiled_term @@ -503,7 +503,7 @@ THEN print_tac options "proved one direction" THEN prove_other_direction options ctxt pred mode moded_clauses THEN print_tac options "proved other direction") - else (fn _ => Skip_Proof.cheat_tac thy)) + else (fn _ => ALLGOALS Skip_Proof.cheat_tac)) end; end; \ No newline at end of file diff -r 88d1d19fb74f -r c713c9505f68 src/HOL/Tools/Quickcheck/quickcheck_common.ML --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Wed Mar 27 14:19:18 2013 +0100 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Wed Mar 27 14:50:30 2013 +0100 @@ -376,7 +376,7 @@ let val eqs_t = mk_equations consts val eqs = map (fn eq => Goal.prove lthy argnames [] eq - (fn _ => Skip_Proof.cheat_tac (Proof_Context.theory_of lthy))) eqs_t + (fn _ => ALLGOALS Skip_Proof.cheat_tac)) eqs_t in fold (fn (name, eq) => Local_Theory.note ((Binding.qualify true prfx diff -r 88d1d19fb74f -r c713c9505f68 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Wed Mar 27 14:19:18 2013 +0100 +++ b/src/Pure/Isar/method.ML Wed Mar 27 14:50:30 2013 +0100 @@ -20,7 +20,7 @@ val SIMPLE_METHOD: tactic -> method val SIMPLE_METHOD': (int -> tactic) -> method val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method - val cheating: bool -> Proof.context -> method + val cheating: bool -> method val intro: thm list -> method val elim: thm list -> method val unfold: thm list -> Proof.context -> method @@ -112,7 +112,7 @@ in -fun insert_tac [] i = all_tac +fun insert_tac [] _ = all_tac | insert_tac facts i = EVERY (map (fn th => cut_rule_tac th i) facts); val insert_facts = METHOD (ALLGOALS o insert_tac); @@ -127,10 +127,10 @@ (* cheating *) -fun cheating int ctxt = +fun cheating int = METHOD (fn _ => fn st => if int orelse ! quick_and_dirty then - METHOD (K (Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt))) - else error "Cheating requires quick_and_dirty mode!"; + ALLGOALS Skip_Proof.cheat_tac st + else error "Cheating requires quick_and_dirty mode!"); (* unfold intro/elim rules *) @@ -296,7 +296,7 @@ val default_text = Source (Args.src (("default", []), Position.none)); val this_text = Basic (K this); val done_text = Basic (K (SIMPLE_METHOD all_tac)); -fun sorry_text int = Basic (cheating int); +fun sorry_text int = Basic (K (cheating int)); fun finish_text (NONE, immed) = Basic (finish immed) | finish_text (SOME txt, immed) = Then [txt, Basic (finish immed)]; diff -r 88d1d19fb74f -r c713c9505f68 src/Pure/goal.ML --- a/src/Pure/goal.ML Wed Mar 27 14:19:18 2013 +0100 +++ b/src/Pure/goal.ML Wed Mar 27 14:50:30 2013 +0100 @@ -324,7 +324,7 @@ fun prove_sorry ctxt xs asms prop tac = if ! quick_and_dirty then - prove ctxt xs asms prop (fn _ => Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt)) + prove ctxt xs asms prop (fn _ => ALLGOALS Skip_Proof.cheat_tac) else (if future_enabled () then prove_future else prove) ctxt xs asms prop tac; fun prove_sorry_global thy xs asms prop tac = diff -r 88d1d19fb74f -r c713c9505f68 src/Pure/skip_proof.ML --- a/src/Pure/skip_proof.ML Wed Mar 27 14:19:18 2013 +0100 +++ b/src/Pure/skip_proof.ML Wed Mar 27 14:50:30 2013 +0100 @@ -9,7 +9,7 @@ val report: Proof.context -> unit val make_thm_cterm: cterm -> thm val make_thm: theory -> term -> thm - val cheat_tac: theory -> tactic + val cheat_tac: int -> tactic end; structure Skip_Proof: SKIP_PROOF = @@ -32,7 +32,7 @@ (* cheat_tac *) -fun cheat_tac thy st = - ALLGOALS (rtac (make_thm thy (Var (("A", 0), propT)))) st; +fun cheat_tac i st = + rtac (make_thm (Thm.theory_of_thm st) (Var (("A", 0), propT))) i st; end;