operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
--- a/NEWS Sat Oct 17 16:40:41 2009 +0200
+++ b/NEWS Sat Oct 17 16:58:03 2009 +0200
@@ -250,6 +250,9 @@
Syntax.pretty_typ/term directly, preferably with proper context
instead of global theory.
+* Operations of structure Skip_Proof (formerly SkipProof) no longer
+require quick_and_dirty mode, which avoids critical setmp.
+
*** System ***
--- a/src/HOL/Import/import.ML Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Import/import.ML Sat Oct 17 16:58:03 2009 +0200
@@ -26,7 +26,7 @@
fun import_tac ctxt (thyname, thmname) =
if ! quick_and_dirty
- then SkipProof.cheat_tac (ProofContext.theory_of ctxt)
+ then Skip_Proof.cheat_tac (ProofContext.theory_of ctxt)
else
fn th =>
let
--- a/src/HOL/Import/replay.ML Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Import/replay.ML Sat Oct 17 16:58:03 2009 +0200
@@ -320,7 +320,7 @@
fun replay_chached_thm int_thms thyname thmname =
let
- fun th_of thy = setmp_CRITICAL quick_and_dirty true (SkipProof.make_thm thy)
+ fun th_of thy = Skip_Proof.make_thm thy
fun err msg = raise ERR "replay_cached_thm" msg
val _ = writeln ("Replaying (from cache) "^thmname^" ...")
fun rps [] thy = thy
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Sat Oct 17 16:58:03 2009 +0200
@@ -69,7 +69,7 @@
(split_conj_thm (cterm_instantiate insts' induct)) i) RSN (2, rev_mp))
in
- SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
+ Skip_Proof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
(fn {prems, ...} => EVERY
[rtac induct' 1,
REPEAT (rtac TrueI 1),
@@ -215,7 +215,7 @@
(((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1
THEN rewrite_goals_tac [mk_meta_eq choice_eq], rec_intrs));
- in split_conj_thm (SkipProof.prove_global thy1 [] []
+ in split_conj_thm (Skip_Proof.prove_global thy1 [] []
(HOLogic.mk_Trueprop (mk_conj rec_unique_ts)) (K tac))
end;
@@ -250,7 +250,7 @@
val _ = message config "Proving characteristic theorems for primrec combinators ..."
- val rec_thms = map (fn t => SkipProof.prove_global thy2 [] [] t
+ val rec_thms = map (fn t => Skip_Proof.prove_global thy2 [] [] t
(fn _ => EVERY
[rewrite_goals_tac reccomb_defs,
rtac the1_equality 1,
@@ -330,7 +330,7 @@
Library.take (length newTs, reccomb_names)) ([], thy1)
||> Theory.checkpoint;
- val case_thms = map (map (fn t => SkipProof.prove_global thy2 [] [] t
+ val case_thms = map (map (fn t => Skip_Proof.prove_global thy2 [] [] t
(fn _ => EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1])))
(DatatypeProp.make_cases new_type_names descr sorts thy2)
in
@@ -364,8 +364,8 @@
val tacf = K (EVERY [rtac exhaustion' 1, ALLGOALS (asm_simp_tac
(HOL_ss addsimps (dist_rewrites' @ inject @ case_thms')))])
in
- (SkipProof.prove_global thy [] [] t1 tacf,
- SkipProof.prove_global thy [] [] t2 tacf)
+ (Skip_Proof.prove_global thy [] [] t1 tacf,
+ Skip_Proof.prove_global thy [] [] t2 tacf)
end;
val split_thm_pairs = map prove_split_thms
@@ -384,7 +384,7 @@
fun prove_weak_case_congs new_type_names descr sorts thy =
let
fun prove_weak_case_cong t =
- SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
+ Skip_Proof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
(fn {prems, ...} => EVERY [rtac ((hd prems) RS arg_cong) 1])
val weak_case_congs = map prove_weak_case_cong (DatatypeProp.make_weak_case_congs
@@ -405,7 +405,7 @@
hyp_subst_tac i, REPEAT (rtac exI i), rtac refl i]
| tac i n = rtac disjI2 i THEN tac i (n - 1)
in
- SkipProof.prove_global thy [] [] t (fn _ =>
+ Skip_Proof.prove_global thy [] [] t (fn _ =>
EVERY [rtac allI 1,
exh_tac (K exhaustion) 1,
ALLGOALS (fn i => tac i (i-1))])
@@ -427,7 +427,7 @@
val [v] = Term.add_vars (concl_of nchotomy') [];
val nchotomy'' = cterm_instantiate [(cert (Var v), cert Ma)] nchotomy'
in
- SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
+ Skip_Proof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
(fn {prems, ...} =>
let val simplify = asm_simp_tac (HOL_ss addsimps (prems @ case_rewrites))
in EVERY [simp_tac (HOL_ss addsimps [hd prems]) 1,
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Sat Oct 17 16:58:03 2009 +0200
@@ -384,7 +384,7 @@
val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
val simpset = Simplifier.context (ProofContext.init thy) (HOL_basic_ss addsimps
(map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms @ distinct_thms)));
- fun prove prop = SkipProof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
+ fun prove prop = Skip_Proof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
|> Simpdata.mk_eq;
in map (rpair true o prove) (triv_injects @ injects @ distincts) @ [(prove refl, false)] end;
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Sat Oct 17 16:58:03 2009 +0200
@@ -344,7 +344,7 @@
(* prove characteristic equations *)
val rewrites = def_thms @ (map mk_meta_eq rec_rewrites);
- val char_thms' = map (fn eqn => SkipProof.prove_global thy' [] [] eqn
+ val char_thms' = map (fn eqn => Skip_Proof.prove_global thy' [] [] eqn
(fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) eqns;
in (thy', char_thms' @ char_thms) end;
@@ -366,7 +366,7 @@
val Ts = map (TFree o rpair HOLogic.typeS)
(Name.variant_list used (replicate i "'t"));
val f = Free ("f", Ts ---> U)
- in SkipProof.prove_global thy [] [] (Logic.mk_implies
+ in Skip_Proof.prove_global thy [] [] (Logic.mk_implies
(HOLogic.mk_Trueprop (HOLogic.list_all
(map (pair "x") Ts, S $ app_bnds f i)),
HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
@@ -403,7 +403,7 @@
val inj_thms' = map snd newT_iso_inj_thms @
map (fn r => r RS @{thm injD}) inj_thms;
- val inj_thm = SkipProof.prove_global thy5 [] []
+ val inj_thm = Skip_Proof.prove_global thy5 [] []
(HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
[(indtac induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
REPEAT (EVERY
@@ -429,7 +429,7 @@
(split_conj_thm inj_thm);
val elem_thm =
- SkipProof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
+ Skip_Proof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
(fn _ =>
EVERY [(indtac induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
rewrite_goals_tac rewrites,
@@ -466,7 +466,7 @@
val iso_thms = if length descr = 1 then [] else
Library.drop (length newTs, split_conj_thm
- (SkipProof.prove_global thy5 [] [] iso_t (fn _ => EVERY
+ (Skip_Proof.prove_global thy5 [] [] iso_t (fn _ => EVERY
[(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
REPEAT (rtac TrueI 1),
rewrite_goals_tac (mk_meta_eq choice_eq ::
@@ -496,7 +496,7 @@
let
val inj_thms = map fst newT_iso_inj_thms;
val rewrites = @{thm o_def} :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
- in SkipProof.prove_global thy5 [] [] eqn (fn _ => EVERY
+ in Skip_Proof.prove_global thy5 [] [] eqn (fn _ => EVERY
[resolve_tac inj_thms 1,
rewrite_goals_tac rewrites,
rtac refl 3,
@@ -520,7 +520,7 @@
fun prove [] = []
| prove (t :: ts) =
let
- val dist_thm = SkipProof.prove_global thy5 [] [] t (fn _ =>
+ val dist_thm = Skip_Proof.prove_global thy5 [] [] t (fn _ =>
EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1])
in dist_thm :: Drule.standard (dist_thm RS not_sym) :: prove ts end;
in prove ts end;
@@ -535,7 +535,7 @@
(iso_inj_thms @
[In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject,
Lim_inject, Suml_inject, Sumr_inject]))
- in SkipProof.prove_global thy5 [] [] t (fn _ => EVERY
+ in Skip_Proof.prove_global thy5 [] [] t (fn _ => EVERY
[rtac iffI 1,
REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
dresolve_tac rep_congs 1, dtac box_equals 1,
@@ -585,7 +585,7 @@
val cert = cterm_of thy6;
- val indrule_lemma = SkipProof.prove_global thy6 [] []
+ val indrule_lemma = Skip_Proof.prove_global thy6 [] []
(Logic.mk_implies
(HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems),
HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY
@@ -600,7 +600,7 @@
val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
val dt_induct_prop = DatatypeProp.make_ind descr sorts;
- val dt_induct = SkipProof.prove_global thy6 []
+ val dt_induct = Skip_Proof.prove_global thy6 []
(Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
(fn {prems, ...} => EVERY
[rtac indrule_lemma' 1,
--- a/src/HOL/Tools/Function/size.ML Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Tools/Function/size.ML Sat Oct 17 16:58:03 2009 +0200
@@ -164,7 +164,7 @@
fun prove_unfolded_size_eqs size_ofp fs =
if null recTs2 then []
- else split_conj_thm (SkipProof.prove ctxt xs []
+ else split_conj_thm (Skip_Proof.prove ctxt xs []
(HOLogic.mk_Trueprop (mk_conj (replicate l HOLogic.true_const @
map (mk_unfolded_size_eq (AList.lookup op =
(new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs)
@@ -198,7 +198,7 @@
fun prove_size_eqs p size_fns size_ofp simpset =
maps (fn (((_, (_, _, constrs)), size_const), T) =>
- map (fn constr => Drule.standard (SkipProof.prove ctxt [] []
+ map (fn constr => Drule.standard (Skip_Proof.prove ctxt [] []
(gen_mk_size_eq p (AList.lookup op = (new_type_names ~~ size_fns))
size_ofp size_const T constr)
(fn _ => simp_tac simpset 1))) constrs)
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML Sat Oct 17 16:58:03 2009 +0200
@@ -108,7 +108,7 @@
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 = setmp_CRITICAL quick_and_dirty true (SkipProof.cheat_tac thy)
+ val tac = Skip_Proof.cheat_tac thy
val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn {...} => tac)
val th''' = LocalDefs.unfold ctxt [@{thm split_conv}] th''
in
@@ -117,7 +117,7 @@
fun normalize_equation thy th =
mk_meta_equation th
- |> Pred_Compile_Set.unfold_set_notation
+ |> Pred_Compile_Set.unfold_set_notation
|> full_fun_cong_expand
|> split_all_pairs thy
|> tap check_equation_format
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML Sat Oct 17 16:58:03 2009 +0200
@@ -56,7 +56,7 @@
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 tac = fn _ => setmp_CRITICAL quick_and_dirty true (SkipProof.cheat_tac thy')
+ val tac = fn _ => Skip_Proof.cheat_tac thy'
val intros'' = map (fn t => Goal.prove ctxt' [] [] t tac) intros'
|> Variable.export ctxt' ctxt
in
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML Sat Oct 17 16:58:03 2009 +0200
@@ -58,7 +58,7 @@
val t = Logic.list_implies
(map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs')))
- val tac = fn _ => setmp_CRITICAL quick_and_dirty true (SkipProof.cheat_tac thy')
+ val tac = fn _ => Skip_Proof.cheat_tac thy'
val intro = Goal.prove (ProofContext.init thy') (map fst vs') [] t tac
val _ = tracing (Display.string_of_thm ctxt' intro)
val thy'' = thy'
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Oct 17 16:58:03 2009 +0200
@@ -661,7 +661,7 @@
val _ = tracing (commas (map (Display.string_of_thm_global thy) pre_intros))
val nparams = guess_nparams T
val pre_elim =
- (Drule.standard o (setmp_CRITICAL quick_and_dirty true (SkipProof.make_thm thy)))
+ (Drule.standard o Skip_Proof.make_thm thy)
(mk_casesrule (ProofContext.init thy) nparams pre_intros)
in register_predicate (pre_intros, pre_elim, nparams) thy end
@@ -2082,7 +2082,7 @@
THEN print_tac "proved one direction"
THEN prove_other_direction thy modes pred mode moded_clauses
THEN print_tac "proved other direction")
- else (fn _ => setmp_CRITICAL quick_and_dirty true SkipProof.cheat_tac thy))
+ else fn _ => Skip_Proof.cheat_tac thy)
end;
(* composition of mode inference, definition, compilation and proof *)
@@ -2110,8 +2110,7 @@
(join_preds_modes moded_clauses compiled_terms)
fun prove_by_skip thy _ _ _ _ compiled_terms =
- map_preds_modes (fn pred => fn mode => fn t =>
- Drule.standard (setmp_CRITICAL quick_and_dirty true (SkipProof.make_thm thy) t))
+ map_preds_modes (fn pred => fn mode => fn t => Drule.standard (Skip_Proof.make_thm thy t))
compiled_terms
fun prepare_intrs thy prednames =
--- a/src/HOL/Tools/inductive.ML Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Tools/inductive.ML Sat Oct 17 16:58:03 2009 +0200
@@ -321,7 +321,7 @@
fun prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt =
(message (quiet_mode orelse skip_mono andalso !quick_and_dirty orelse fork_mono)
" Proving monotonicity ...";
- (if skip_mono then SkipProof.prove else if fork_mono then Goal.prove_future else Goal.prove) ctxt
+ (if skip_mono then Skip_Proof.prove else if fork_mono then Goal.prove_future else Goal.prove) ctxt
[] []
(HOLogic.mk_Trueprop
(Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
@@ -350,7 +350,7 @@
val rules = [refl, TrueI, notFalseI, exI, conjI];
val intrs = map_index (fn (i, intr) => rulify
- (SkipProof.prove ctxt (map (fst o dest_Free) params) [] intr (fn _ => EVERY
+ (Skip_Proof.prove ctxt (map (fst o dest_Free) params) [] intr (fn _ => EVERY
[rewrite_goals_tac rec_preds_defs,
rtac (unfold RS iffD2) 1,
EVERY1 (select_disj (length intr_ts) (i + 1)),
@@ -395,7 +395,7 @@
val prems = HOLogic.mk_Trueprop (list_comb (c, params @ frees)) ::
map mk_elim_prem (map #1 c_intrs)
in
- (SkipProof.prove ctxt'' [] prems P
+ (Skip_Proof.prove ctxt'' [] prems P
(fn {prems, ...} => EVERY
[cut_facts_tac [hd prems] 1,
rewrite_goals_tac rec_preds_defs,
@@ -558,7 +558,7 @@
val raw_fp_induct = (mono RS (fp_def RS @{thm def_lfp_induct}));
- val induct = SkipProof.prove ctxt'' [] ind_prems ind_concl
+ val induct = Skip_Proof.prove ctxt'' [] ind_prems ind_concl
(fn {prems, ...} => EVERY
[rewrite_goals_tac [inductive_conj_def],
DETERM (rtac raw_fp_induct 1),
@@ -575,7 +575,7 @@
(inductive_conj_def :: rec_preds_defs @ simp_thms'') prem,
conjI, refl] 1)) prems)]);
- val lemma = SkipProof.prove ctxt'' [] []
+ val lemma = Skip_Proof.prove ctxt'' [] []
(Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn _ => EVERY
[rewrite_goals_tac rec_preds_defs,
REPEAT (EVERY
--- a/src/HOL/Tools/quickcheck_generators.ML Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Sat Oct 17 16:58:03 2009 +0200
@@ -149,7 +149,7 @@
val tac = ALLGOALS (rtac rule)
THEN ALLGOALS (simp_tac rew_ss)
THEN (ALLGOALS (ProofContext.fact_tac (flat eqs2)))
- val simp = SkipProof.prove lthy' [v] [] eq (K tac);
+ val simp = Skip_Proof.prove lthy' [v] [] eq (K tac);
in (simp, lthy') end;
end;
@@ -185,7 +185,7 @@
ALLGOALS (simp_tac (HOL_ss addsimps proj_simps))
THEN ALLGOALS (EqSubst.eqsubst_tac ctxt [0] [aux_simp])
THEN ALLGOALS (simp_tac (HOL_ss addsimps [fst_conv, snd_conv]));
- in (map (fn prop => SkipProof.prove lthy [v] [] prop tac) eqs, lthy) end;
+ in (map (fn prop => Skip_Proof.prove lthy [v] [] prop tac) eqs, lthy) end;
in
lthy
|> random_aux_primrec aux_eq'
@@ -206,7 +206,7 @@
let
val ext_simps = map (fn thm => fun_cong OF [fun_cong OF [thm]]) proto_simps;
val tac = ALLGOALS (ProofContext.fact_tac ext_simps);
- in (map (fn prop => SkipProof.prove lthy vs [] prop (K tac)) eqs, lthy) end;
+ in (map (fn prop => Skip_Proof.prove lthy vs [] prop (K tac)) eqs, lthy) end;
val b = Binding.qualify true prfx (Binding.qualify true name (Binding.name "simps"));
in
lthy
--- a/src/HOL/Tools/record.ML Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Tools/record.ML Sat Oct 17 16:58:03 2009 +0200
@@ -1040,7 +1040,7 @@
if ! record_quick_and_dirty_sensitive andalso ! quick_and_dirty then
Goal.prove (ProofContext.init thy) [] []
(Logic.list_implies (map Logic.varify asms, Logic.varify prop))
- (K (SkipProof.cheat_tac @{theory HOL}))
+ (K (Skip_Proof.cheat_tac @{theory HOL}))
(*Drule.standard can take quite a while for large records, thats why
we varify the proposition manually here.*)
else
--- a/src/HOL/Tools/sat_funcs.ML Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Tools/sat_funcs.ML Sat Oct 17 16:58:03 2009 +0200
@@ -337,7 +337,7 @@
val _ = if !trace_sat then
tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead."
else ()
- val False_thm = SkipProof.make_thm @{theory} (HOLogic.Trueprop $ HOLogic.false_const)
+ val False_thm = Skip_Proof.make_thm @{theory} (HOLogic.Trueprop $ HOLogic.false_const)
in
(* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold *)
(* Thm.weaken sorted_clauses' would be quadratic, since we sorted *)
--- a/src/HOL/Tools/typedef.ML Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Tools/typedef.ML Sat Oct 17 16:58:03 2009 +0200
@@ -199,8 +199,7 @@
(*test theory errors now!*)
val test_thy = Theory.copy thy;
- val _ = test_thy
- |> typedef_result (setmp_CRITICAL quick_and_dirty true (SkipProof.make_thm test_thy) goal);
+ val _ = typedef_result (Skip_Proof.make_thm test_thy goal) test_thy;
in (set, goal, goal_pat, typedef_result) end
handle ERROR msg =>
--- a/src/HOL/ex/predicate_compile.ML Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML Sat Oct 17 16:58:03 2009 +0200
@@ -114,10 +114,10 @@
val do_proofs = Unsynchronized.ref true;
fun mycheat_tac thy i st =
- (Tactic.rtac (SkipProof.make_thm thy (Var (("A", 0), propT))) i) st
+ (Tactic.rtac (Skip_Proof.make_thm thy (Var (("A", 0), propT))) i) st
fun remove_last_goal thy st =
- (Tactic.rtac (SkipProof.make_thm thy (Var (("A", 0), propT))) (nprems_of st)) st
+ (Tactic.rtac (Skip_Proof.make_thm thy (Var (("A", 0), propT))) (nprems_of st)) st
(* reference to preprocessing of InductiveSet package *)
@@ -1866,7 +1866,7 @@
(join_preds_modes moded_clauses compiled_terms)
fun prove_by_skip thy _ _ _ _ compiled_terms =
- map_preds_modes (fn pred => fn mode => fn t => Drule.standard (SkipProof.make_thm thy t))
+ map_preds_modes (fn pred => fn mode => fn t => Drule.standard (Skip_Proof.make_thm thy t))
compiled_terms
fun prepare_intrs thy prednames =
--- a/src/Pure/Isar/class.ML Sat Oct 17 16:40:41 2009 +0200
+++ b/src/Pure/Isar/class.ML Sat Oct 17 16:58:03 2009 +0200
@@ -76,7 +76,7 @@
val ((_, [thm']), _) = Variable.import true [thm] empty_ctxt;
val thm'' = Morphism.thm (const_morph $> eq_morph) thm';
val tac = ALLGOALS (ProofContext.fact_tac [thm'']);
- in SkipProof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
+ in Skip_Proof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
val assm_intro = Option.map prove_assm_intro
(fst (Locale.intros_of thy class));
@@ -93,7 +93,7 @@
(Tactic.match_tac (axclass_intro :: sup_of_classes
@ loc_axiom_intros @ base_sort_trivs)
ORELSE' Tactic.assume_tac));
- val of_class = SkipProof.prove_global thy [] [] of_class_prop (K tac);
+ val of_class = Skip_Proof.prove_global thy [] [] of_class_prop (K tac);
in (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) end;
--- a/src/Pure/Isar/class_target.ML Sat Oct 17 16:40:41 2009 +0200
+++ b/src/Pure/Isar/class_target.ML Sat Oct 17 16:58:03 2009 +0200
@@ -239,7 +239,7 @@
[Option.map (Drule.standard' o Element.conclude_witness) some_wit,
(fst o rules thy) sub];
val tac = EVERY (map (TRYALL o Tactic.rtac) intros);
- val classrel = SkipProof.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
+ val classrel = Skip_Proof.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
(K tac);
val diff_sort = Sign.complete_sort thy [sup]
|> subtract (op =) (Sign.complete_sort thy [sub])
--- a/src/Pure/Isar/skip_proof.ML Sat Oct 17 16:40:41 2009 +0200
+++ b/src/Pure/Isar/skip_proof.ML Sat Oct 17 16:58:03 2009 +0200
@@ -1,7 +1,8 @@
(* Title: Pure/Isar/skip_proof.ML
Author: Markus Wenzel, TU Muenchen
-Skipping proofs -- quick_and_dirty mode.
+Skipping proofs -- via oracle (in quick and dirty mode) or by forking
+(parallel mode).
*)
signature SKIP_PROOF =
@@ -14,15 +15,13 @@
({prems: thm list, context: Proof.context} -> tactic) -> thm
end;
-structure SkipProof: SKIP_PROOF =
+structure Skip_Proof: SKIP_PROOF =
struct
(* oracle setup *)
val (_, skip_proof) = Context.>>> (Context.map_theory_result
- (Thm.add_oracle (Binding.name "skip_proof", fn (thy, prop) =>
- if ! quick_and_dirty then Thm.cterm_of thy prop
- else error "Proof may be skipped in quick_and_dirty mode only!")));
+ (Thm.add_oracle (Binding.name "skip_proof", fn (thy, prop) => Thm.cterm_of thy prop)));
(* basic cheating *)
@@ -36,7 +35,7 @@
(if Goal.future_enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop
(fn args => fn st =>
if ! quick_and_dirty
- then setmp_CRITICAL quick_and_dirty true (cheat_tac (ProofContext.theory_of ctxt)) st
+ then cheat_tac (ProofContext.theory_of ctxt) st
else tac args st);
fun prove_global thy xs asms prop tac =
--- a/src/Pure/codegen.ML Sat Oct 17 16:40:41 2009 +0200
+++ b/src/Pure/codegen.ML Sat Oct 17 16:58:03 2009 +0200
@@ -280,8 +280,7 @@
let
val x = Free (Name.variant (OldTerm.add_term_names (t, [])) "x", fastype_of t);
(* fake definition *)
- val eq = setmp_CRITICAL quick_and_dirty true (SkipProof.make_thm thy)
- (Logic.mk_equals (x, t));
+ val eq = Skip_Proof.make_thm thy (Logic.mk_equals (x, t));
fun err () = error "preprocess_term: bad preprocessor"
in case map prop_of (preprocess thy [eq]) of
[Const ("==", _) $ x' $ t'] => if x = x' then t' else err ()