quick_and_dirty_prove_goalw_cterm;
authorwenzelm
Mon Oct 22 17:58:26 2001 +0200 (2001-10-22 ago)
changeset 11880a625de9ad62a
parent 11879 1a386a1e002c
child 11881 b46b1bdbe3f5
quick_and_dirty_prove_goalw_cterm;
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Oct 22 17:58:11 2001 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Oct 22 17:58:26 2001 +0200
     1.3 @@ -476,7 +476,7 @@
     1.4  
     1.5  fun prove_mono setT fp_fun monos thy =
     1.6   (message "  Proving monotonicity ...";
     1.7 -  Goals.prove_goalw_cterm []      (*NO SkipProof.prove_goalw_cterm here!*)
     1.8 +  Goals.prove_goalw_cterm []      (*NO quick_and_dirty_prove_goalw_cterm here!*)
     1.9      (Thm.cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
    1.10        (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
    1.11      (fn _ => [rtac monoI 1, REPEAT (ares_tac (flat (map mk_mono monos) @ get_monos thy) 1)]));
    1.12 @@ -495,7 +495,7 @@
    1.13        | select_disj _ 1 = [rtac disjI1]
    1.14        | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
    1.15  
    1.16 -    val intrs = map (fn (i, intr) => SkipProof.prove_goalw_cterm thy rec_sets_defs
    1.17 +    val intrs = map (fn (i, intr) => quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
    1.18        (Thm.cterm_of (Theory.sign_of thy) intr) (fn prems =>
    1.19         [(*insert prems and underlying sets*)
    1.20         cut_facts_tac prems 1,
    1.21 @@ -524,7 +524,7 @@
    1.22      val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject];
    1.23    in
    1.24      mk_elims cs cTs params intr_ts intr_names |> map (fn (t, cases) =>
    1.25 -      SkipProof.prove_goalw_cterm thy rec_sets_defs
    1.26 +      quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
    1.27          (Thm.cterm_of (Theory.sign_of thy) t) (fn prems =>
    1.28            [cut_facts_tac [hd prems] 1,
    1.29             dtac (unfold RS subst) 1,
    1.30 @@ -652,14 +652,14 @@
    1.31      (* simplification rules for vimage and Collect *)
    1.32  
    1.33      val vimage_simps = if length cs < 2 then [] else
    1.34 -      map (fn c => SkipProof.prove_goalw_cterm thy [] (Thm.cterm_of sign
    1.35 +      map (fn c => quick_and_dirty_prove_goalw_cterm thy [] (Thm.cterm_of sign
    1.36          (HOLogic.mk_Trueprop (HOLogic.mk_eq
    1.37            (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
    1.38             HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
    1.39               nth_elem (find_index_eq c cs, preds)))))
    1.40          (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1])) cs;
    1.41  
    1.42 -    val induct = SkipProof.prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of sign
    1.43 +    val induct = quick_and_dirty_prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of sign
    1.44        (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
    1.45          [rtac (impI RS allI) 1,
    1.46           DETERM (etac (mono RS (fp_def RS def_lfp_induct)) 1),
    1.47 @@ -674,7 +674,7 @@
    1.48           EVERY (map (fn prem =>
    1.49             DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
    1.50  
    1.51 -    val lemma = SkipProof.prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of sign
    1.52 +    val lemma = quick_and_dirty_prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of sign
    1.53        (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
    1.54          [cut_facts_tac prems 1,
    1.55           REPEAT (EVERY