# HG changeset patch # User berghofe # Date 1207237779 -7200 # Node ID 96e82c7861faaefe1c4eb20bf660f941888dfe75 # Parent 777f334ff652aefc0f3ce244fe978c8b7a106b4c - use SkipProof.prove_global instead of Goal.prove_global - added skip_mono flag to inductive definition package diff -r 777f334ff652 -r 96e82c7861fa src/HOL/Tools/datatype_abs_proofs.ML --- 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, diff -r 777f334ff652 -r 96e82c7861fa src/HOL/Tools/datatype_rep_proofs.ML --- 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,