- use SkipProof.prove_global instead of Goal.prove_global
- added skip_mono flag to inductive definition package
--- a/src/HOL/Tools/datatype_abs_proofs.ML Thu Apr 03 17:43:01 2008 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Thu Apr 03 17:49:39 2008 +0200
@@ -70,7 +70,7 @@
(split_conj_thm (cterm_instantiate insts' induct), i)) RSN (2, rev_mp))
in
- Goal.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
+ SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
(fn prems => EVERY
[rtac induct' 1,
REPEAT (rtac TrueI 1),
@@ -156,7 +156,8 @@
val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
InductivePackage.add_inductive_global (serial_string ())
{quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
- alt_name = big_rec_name', coind = false, no_elim = false, no_ind = true}
+ alt_name = big_rec_name', coind = false, no_elim = false, no_ind = true,
+ skip_mono = true}
(map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
(map dest_Free rec_fns)
(map (fn x => (("", []), x)) rec_intr_ts) [] thy0;
@@ -216,7 +217,7 @@
THEN rewtac (mk_meta_eq choice_eq), rec_intrs),
descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts);
- in split_conj_thm (Goal.prove_global thy1 [] []
+ in split_conj_thm (SkipProof.prove_global thy1 [] []
(HOLogic.mk_Trueprop (mk_conj rec_unique_ts)) (K tac))
end;
@@ -250,7 +251,7 @@
val _ = message "Proving characteristic theorems for primrec combinators ..."
- val rec_thms = map (fn t => Goal.prove_global thy2 [] [] t
+ val rec_thms = map (fn t => SkipProof.prove_global thy2 [] [] t
(fn _ => EVERY
[rewrite_goals_tac reccomb_defs,
rtac the1_equality 1,
@@ -328,7 +329,7 @@
end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~
(Library.take (length newTs, reccomb_names)));
- val case_thms = map (map (fn t => Goal.prove_global thy2 [] [] t
+ val case_thms = map (map (fn t => SkipProof.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)
@@ -361,8 +362,8 @@
val tacf = K (EVERY [rtac exhaustion' 1, ALLGOALS (asm_simp_tac
(HOL_ss addsimps (dist_rewrites' @ inject @ case_thms')))])
in
- (Goal.prove_global thy [] [] t1 tacf,
- Goal.prove_global thy [] [] t2 tacf)
+ (SkipProof.prove_global thy [] [] t1 tacf,
+ SkipProof.prove_global thy [] [] t2 tacf)
end;
val split_thm_pairs = map prove_split_thms
@@ -381,7 +382,7 @@
fun prove_weak_case_congs new_type_names descr sorts thy =
let
fun prove_weak_case_cong t =
- Goal.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
+ SkipProof.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
@@ -402,7 +403,7 @@
hyp_subst_tac i, REPEAT (rtac exI i), rtac refl i]
| tac i n = rtac disjI2 i THEN tac i (n - 1)
in
- Goal.prove_global thy [] [] t (fn _ =>
+ SkipProof.prove_global thy [] [] t (fn _ =>
EVERY [rtac allI 1,
exh_tac (K exhaustion) 1,
ALLGOALS (fn i => tac i (i-1))])
@@ -424,7 +425,7 @@
val nchotomy'' = cterm_instantiate
[(cert (hd (add_term_vars (concl_of nchotomy', []))), cert Ma)] nchotomy'
in
- Goal.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
+ SkipProof.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_rep_proofs.ML Thu Apr 03 17:43:01 2008 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Thu Apr 03 17:49:39 2008 +0200
@@ -177,8 +177,9 @@
val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
InductivePackage.add_inductive_global (serial_string ())
- {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK, alt_name = big_rec_name,
- coind = false, no_elim = true, no_ind = false}
+ {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
+ alt_name = big_rec_name, coind = false, no_elim = true, no_ind = false,
+ skip_mono = true}
(map (fn s => ((s, UnivT'), NoSyn)) rep_set_names') []
(map (fn x => (("", []), x)) intr_ts) [] thy1;
@@ -346,7 +347,7 @@
(* prove characteristic equations *)
val rewrites = def_thms @ (map mk_meta_eq rec_rewrites);
- val char_thms' = map (fn eqn => Goal.prove_global thy' [] [] eqn
+ val char_thms' = map (fn eqn => SkipProof.prove_global thy' [] [] eqn
(fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) eqns;
in (thy', char_thms' @ char_thms) end;
@@ -368,7 +369,7 @@
val Ts = map (TFree o rpair HOLogic.typeS)
(Name.variant_list used (replicate i "'t"));
val f = Free ("f", Ts ---> U)
- in Goal.prove_global thy [] [] (Logic.mk_implies
+ in SkipProof.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,
@@ -401,7 +402,7 @@
val inj_thms' = map snd newT_iso_inj_thms @
map (fn r => r RS @{thm injD}) inj_thms;
- val inj_thm = Goal.prove_global thy5 [] []
+ val inj_thm = SkipProof.prove_global thy5 [] []
(HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
[(indtac induction [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
REPEAT (EVERY
@@ -427,7 +428,7 @@
(split_conj_thm inj_thm);
val elem_thm =
- Goal.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
+ SkipProof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
(fn _ =>
EVERY [(indtac induction [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
rewrite_goals_tac rewrites,
@@ -464,7 +465,7 @@
val iso_thms = if length descr = 1 then [] else
Library.drop (length newTs, split_conj_thm
- (Goal.prove_global thy5 [] [] iso_t (fn _ => EVERY
+ (SkipProof.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 ::
@@ -494,7 +495,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 Goal.prove_global thy5 [] [] eqn (fn _ => EVERY
+ in SkipProof.prove_global thy5 [] [] eqn (fn _ => EVERY
[resolve_tac inj_thms 1,
rewrite_goals_tac rewrites,
rtac refl 3,
@@ -516,7 +517,7 @@
fun prove_distinct_thms (_, []) = []
| prove_distinct_thms (dist_rewrites', t::_::ts) =
let
- val dist_thm = Goal.prove_global thy5 [] [] t (fn _ =>
+ val dist_thm = SkipProof.prove_global thy5 [] [] t (fn _ =>
EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1])
in dist_thm::(standard (dist_thm RS not_sym))::
(prove_distinct_thms (dist_rewrites', ts))
@@ -538,7 +539,7 @@
(iso_inj_thms @
[In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject,
Lim_inject, Suml_inject, Sumr_inject]))
- in Goal.prove_global thy5 [] [] t (fn _ => EVERY
+ in SkipProof.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,
@@ -588,7 +589,7 @@
val cert = cterm_of thy6;
- val indrule_lemma = Goal.prove_global thy6 [] []
+ val indrule_lemma = SkipProof.prove_global thy6 [] []
(Logic.mk_implies
(HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems),
HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY
@@ -603,7 +604,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 = Goal.prove_global thy6 []
+ val dt_induct = SkipProof.prove_global thy6 []
(Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
(fn prems => EVERY
[rtac indrule_lemma' 1,