author wenzelm Wed, 27 Mar 2013 14:50:30 +0100 changeset 51552 c713c9505f68 parent 51551 88d1d19fb74f child 51553 63327f679cff
clarified Skip_Proof.cheat_tac: more standard tactic; clarified Method.cheating: check quick_and_dirty when it is actually applied;
```--- 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 =```
```--- 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;```
```--- 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```
```--- 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'''```
```--- 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'))```
```--- 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```
```--- 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```
```--- 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)];```
```--- 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 =```
```--- 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;```