clarified Skip_Proof.cheat_tac: more standard tactic;
authorwenzelm
Wed Mar 27 14:50:30 2013 +0100 (2013-03-27)
changeset 51552c713c9505f68
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;
src/HOL/TPTP/atp_problem_import.ML
src/HOL/TPTP/sledgehammer_tactics.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
src/HOL/Tools/Quickcheck/quickcheck_common.ML
src/Pure/Isar/method.ML
src/Pure/goal.ML
src/Pure/skip_proof.ML
     1.1 --- a/src/HOL/TPTP/atp_problem_import.ML	Wed Mar 27 14:19:18 2013 +0100
     1.2 +++ b/src/HOL/TPTP/atp_problem_import.ML	Wed Mar 27 14:50:30 2013 +0100
     1.3 @@ -175,7 +175,7 @@
     1.4          val (outcome, _) =
     1.5            Nitpick.pick_nits_in_term state params Nitpick.Normal i n step subst
     1.6                                      [] [] conj
     1.7 -      in if outcome = "none" then Skip_Proof.cheat_tac thy th else Seq.empty end
     1.8 +      in if outcome = "none" then ALLGOALS Skip_Proof.cheat_tac th else Seq.empty end
     1.9    end
    1.10  
    1.11  fun atp_tac ctxt completeness override_params timeout prover =
     2.1 --- a/src/HOL/TPTP/sledgehammer_tactics.ML	Wed Mar 27 14:19:18 2013 +0100
     2.2 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Wed Mar 27 14:50:30 2013 +0100
     2.3 @@ -64,12 +64,11 @@
     2.4  
     2.5  fun sledgehammer_as_oracle_tac ctxt override_params fact_override i th =
     2.6    let
     2.7 -    val thy = Proof_Context.theory_of ctxt
     2.8      val override_params =
     2.9        override_params @
    2.10        [("preplay_timeout", "0"),
    2.11         ("minimize", "false")]
    2.12      val xs = run_prover override_params fact_override i i ctxt th
    2.13 -  in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
    2.14 +  in if is_some xs then ALLGOALS Skip_Proof.cheat_tac th else Seq.empty end
    2.15  
    2.16  end;
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Mar 27 14:19:18 2013 +0100
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Mar 27 14:50:30 2013 +0100
     3.3 @@ -1180,7 +1180,7 @@
     3.4  fun define_quickcheck_predicate t thy =
     3.5    let
     3.6      val (vs, t') = strip_abs t
     3.7 -    val vs' = Variable.variant_frees (Proof_Context.init_global thy) [] vs
     3.8 +    val vs' = Variable.variant_frees (Proof_Context.init_global thy) [] vs (* FIXME proper context!? *)
     3.9      val t'' = subst_bounds (map Free (rev vs'), t')
    3.10      val (prems, concl) = strip_horn t''
    3.11      val constname = "quickcheck"
    3.12 @@ -1191,8 +1191,9 @@
    3.13      val t = Logic.list_implies
    3.14        (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
    3.15         HOLogic.mk_Trueprop (list_comb (const, map Free vs')))
    3.16 -    val tac = fn _ => Skip_Proof.cheat_tac thy1
    3.17 -    val intro = Goal.prove (Proof_Context.init_global thy1) (map fst vs') [] t tac
    3.18 +    val intro =
    3.19 +      Goal.prove (Proof_Context.init_global thy1) (map fst vs') [] t
    3.20 +        (fn _ => ALLGOALS Skip_Proof.cheat_tac)
    3.21    in
    3.22      ((((full_constname, constT), vs'), intro), thy1)
    3.23    end
     4.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Mar 27 14:19:18 2013 +0100
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Mar 27 14:50:30 2013 +0100
     4.3 @@ -134,7 +134,7 @@
     4.4    
     4.5  fun split_all_pairs thy th =
     4.6    let
     4.7 -    val ctxt = Proof_Context.init_global thy
     4.8 +    val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
     4.9      val ((_, [th']), _) = Variable.import true [th] ctxt
    4.10      val t = prop_of th'
    4.11      val frees = Term.add_frees t [] 
    4.12 @@ -148,8 +148,9 @@
    4.13        in ((Free (x, T), HOLogic.mk_ptuple paths T (map Free xTs)), nctxt') end
    4.14      val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt 
    4.15      val t' = Pattern.rewrite_term thy rewr [] t
    4.16 -    val tac = Skip_Proof.cheat_tac thy
    4.17 -    val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn _ => tac)
    4.18 +    val th'' =
    4.19 +      Goal.prove ctxt (Term.add_free_names t' []) [] t'
    4.20 +        (fn _ => ALLGOALS Skip_Proof.cheat_tac)
    4.21      val th''' = Local_Defs.unfold ctxt [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}] th''
    4.22    in
    4.23      th'''
     5.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Wed Mar 27 14:19:18 2013 +0100
     5.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Wed Mar 27 14:50:30 2013 +0100
     5.3 @@ -127,13 +127,13 @@
     5.4  
     5.5  fun flatten_intros constname intros thy =
     5.6    let
     5.7 -    val ctxt = Proof_Context.init_global thy
     5.8 +    val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
     5.9      val ((_, intros), ctxt') = Variable.import true intros ctxt
    5.10      val (intros', (local_defs, thy')) = (fold_map o fold_map_atoms)
    5.11        (flatten constname) (map prop_of intros) ([], thy)
    5.12      val ctxt'' = Proof_Context.transfer thy' ctxt'
    5.13 -    val tac = fn _ => Skip_Proof.cheat_tac thy'
    5.14 -    val intros'' = map (fn t => Goal.prove ctxt'' [] [] t tac) intros'
    5.15 +    val intros'' =
    5.16 +      map (fn t => Goal.prove ctxt'' [] [] t (fn _ => ALLGOALS Skip_Proof.cheat_tac)) intros'
    5.17        |> Variable.export ctxt'' ctxt
    5.18    in
    5.19      (intros'', (local_defs, thy'))
     6.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Wed Mar 27 14:19:18 2013 +0100
     6.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Wed Mar 27 14:50:30 2013 +0100
     6.3 @@ -491,7 +491,7 @@
     6.4  
     6.5  fun prove_pred options thy clauses preds pred (_, mode) (moded_clauses, compiled_term) =
     6.6    let
     6.7 -    val ctxt = Proof_Context.init_global thy
     6.8 +    val ctxt = Proof_Context.init_global thy   (* FIXME proper context!? *)
     6.9      val clauses = case AList.lookup (op =) clauses pred of SOME rs => rs | NONE => []
    6.10    in
    6.11      Goal.prove ctxt (Term.add_free_names compiled_term []) [] compiled_term
    6.12 @@ -503,7 +503,7 @@
    6.13          THEN print_tac options "proved one direction"
    6.14          THEN prove_other_direction options ctxt pred mode moded_clauses
    6.15          THEN print_tac options "proved other direction")
    6.16 -      else (fn _ => Skip_Proof.cheat_tac thy))
    6.17 +      else (fn _ => ALLGOALS Skip_Proof.cheat_tac))
    6.18    end;
    6.19  
    6.20  end;
    6.21 \ No newline at end of file
     7.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Mar 27 14:19:18 2013 +0100
     7.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Mar 27 14:50:30 2013 +0100
     7.3 @@ -376,7 +376,7 @@
     7.4        let
     7.5          val eqs_t = mk_equations consts
     7.6          val eqs = map (fn eq => Goal.prove lthy argnames [] eq
     7.7 -          (fn _ => Skip_Proof.cheat_tac (Proof_Context.theory_of lthy))) eqs_t
     7.8 +          (fn _ => ALLGOALS Skip_Proof.cheat_tac)) eqs_t
     7.9        in
    7.10          fold (fn (name, eq) => Local_Theory.note
    7.11            ((Binding.qualify true prfx
     8.1 --- a/src/Pure/Isar/method.ML	Wed Mar 27 14:19:18 2013 +0100
     8.2 +++ b/src/Pure/Isar/method.ML	Wed Mar 27 14:50:30 2013 +0100
     8.3 @@ -20,7 +20,7 @@
     8.4    val SIMPLE_METHOD: tactic -> method
     8.5    val SIMPLE_METHOD': (int -> tactic) -> method
     8.6    val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
     8.7 -  val cheating: bool -> Proof.context -> method
     8.8 +  val cheating: bool -> method
     8.9    val intro: thm list -> method
    8.10    val elim: thm list -> method
    8.11    val unfold: thm list -> Proof.context -> method
    8.12 @@ -112,7 +112,7 @@
    8.13  
    8.14  in
    8.15  
    8.16 -fun insert_tac [] i = all_tac
    8.17 +fun insert_tac [] _ = all_tac
    8.18    | insert_tac facts i = EVERY (map (fn th => cut_rule_tac th i) facts);
    8.19  
    8.20  val insert_facts = METHOD (ALLGOALS o insert_tac);
    8.21 @@ -127,10 +127,10 @@
    8.22  
    8.23  (* cheating *)
    8.24  
    8.25 -fun cheating int ctxt =
    8.26 +fun cheating int = METHOD (fn _ => fn st =>
    8.27    if int orelse ! quick_and_dirty then
    8.28 -    METHOD (K (Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt)))
    8.29 -  else error "Cheating requires quick_and_dirty mode!";
    8.30 +    ALLGOALS Skip_Proof.cheat_tac st
    8.31 +  else error "Cheating requires quick_and_dirty mode!");
    8.32  
    8.33  
    8.34  (* unfold intro/elim rules *)
    8.35 @@ -296,7 +296,7 @@
    8.36  val default_text = Source (Args.src (("default", []), Position.none));
    8.37  val this_text = Basic (K this);
    8.38  val done_text = Basic (K (SIMPLE_METHOD all_tac));
    8.39 -fun sorry_text int = Basic (cheating int);
    8.40 +fun sorry_text int = Basic (K (cheating int));
    8.41  
    8.42  fun finish_text (NONE, immed) = Basic (finish immed)
    8.43    | finish_text (SOME txt, immed) = Then [txt, Basic (finish immed)];
     9.1 --- a/src/Pure/goal.ML	Wed Mar 27 14:19:18 2013 +0100
     9.2 +++ b/src/Pure/goal.ML	Wed Mar 27 14:50:30 2013 +0100
     9.3 @@ -324,7 +324,7 @@
     9.4  
     9.5  fun prove_sorry ctxt xs asms prop tac =
     9.6    if ! quick_and_dirty then
     9.7 -    prove ctxt xs asms prop (fn _ => Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt))
     9.8 +    prove ctxt xs asms prop (fn _ => ALLGOALS Skip_Proof.cheat_tac)
     9.9    else (if future_enabled () then prove_future else prove) ctxt xs asms prop tac;
    9.10  
    9.11  fun prove_sorry_global thy xs asms prop tac =
    10.1 --- a/src/Pure/skip_proof.ML	Wed Mar 27 14:19:18 2013 +0100
    10.2 +++ b/src/Pure/skip_proof.ML	Wed Mar 27 14:50:30 2013 +0100
    10.3 @@ -9,7 +9,7 @@
    10.4    val report: Proof.context -> unit
    10.5    val make_thm_cterm: cterm -> thm
    10.6    val make_thm: theory -> term -> thm
    10.7 -  val cheat_tac: theory -> tactic
    10.8 +  val cheat_tac: int -> tactic
    10.9  end;
   10.10  
   10.11  structure Skip_Proof: SKIP_PROOF =
   10.12 @@ -32,7 +32,7 @@
   10.13  
   10.14  (* cheat_tac *)
   10.15  
   10.16 -fun cheat_tac thy st =
   10.17 -  ALLGOALS (rtac (make_thm thy (Var (("A", 0), propT)))) st;
   10.18 +fun cheat_tac i st =
   10.19 +  rtac (make_thm (Thm.theory_of_thm st) (Var (("A", 0), propT))) i st;
   10.20  
   10.21  end;