src/HOL/Tools/datatype_rep_proofs.ML
changeset 26531 96e82c7861fa
parent 26475 3cc1e48d0ce1
child 26626 c6231d64d264
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Apr 03 17:43:01 2008 +0200
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Apr 03 17:49:39 2008 +0200
     1.3 @@ -177,8 +177,9 @@
     1.4  
     1.5      val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
     1.6          InductivePackage.add_inductive_global (serial_string ())
     1.7 -          {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK, alt_name = big_rec_name,
     1.8 -            coind = false, no_elim = true, no_ind = false}
     1.9 +          {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
    1.10 +           alt_name = big_rec_name, coind = false, no_elim = true, no_ind = false,
    1.11 +           skip_mono = true}
    1.12            (map (fn s => ((s, UnivT'), NoSyn)) rep_set_names') []
    1.13            (map (fn x => (("", []), x)) intr_ts) [] thy1;
    1.14  
    1.15 @@ -346,7 +347,7 @@
    1.16          (* prove characteristic equations *)
    1.17  
    1.18          val rewrites = def_thms @ (map mk_meta_eq rec_rewrites);
    1.19 -        val char_thms' = map (fn eqn => Goal.prove_global thy' [] [] eqn
    1.20 +        val char_thms' = map (fn eqn => SkipProof.prove_global thy' [] [] eqn
    1.21            (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) eqns;
    1.22  
    1.23        in (thy', char_thms' @ char_thms) end;
    1.24 @@ -368,7 +369,7 @@
    1.25              val Ts = map (TFree o rpair HOLogic.typeS)
    1.26                (Name.variant_list used (replicate i "'t"));
    1.27              val f = Free ("f", Ts ---> U)
    1.28 -          in Goal.prove_global thy [] [] (Logic.mk_implies
    1.29 +          in SkipProof.prove_global thy [] [] (Logic.mk_implies
    1.30              (HOLogic.mk_Trueprop (HOLogic.list_all
    1.31                 (map (pair "x") Ts, S $ app_bnds f i)),
    1.32               HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
    1.33 @@ -401,7 +402,7 @@
    1.34          val inj_thms' = map snd newT_iso_inj_thms @
    1.35            map (fn r => r RS @{thm injD}) inj_thms;
    1.36  
    1.37 -        val inj_thm = Goal.prove_global thy5 [] []
    1.38 +        val inj_thm = SkipProof.prove_global thy5 [] []
    1.39            (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
    1.40              [(indtac induction [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    1.41               REPEAT (EVERY
    1.42 @@ -427,7 +428,7 @@
    1.43                               (split_conj_thm inj_thm);
    1.44  
    1.45          val elem_thm = 
    1.46 -            Goal.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
    1.47 +            SkipProof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
    1.48                (fn _ =>
    1.49                 EVERY [(indtac induction [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    1.50                  rewrite_goals_tac rewrites,
    1.51 @@ -464,7 +465,7 @@
    1.52  
    1.53      val iso_thms = if length descr = 1 then [] else
    1.54        Library.drop (length newTs, split_conj_thm
    1.55 -        (Goal.prove_global thy5 [] [] iso_t (fn _ => EVERY
    1.56 +        (SkipProof.prove_global thy5 [] [] iso_t (fn _ => EVERY
    1.57             [(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    1.58              REPEAT (rtac TrueI 1),
    1.59              rewrite_goals_tac (mk_meta_eq choice_eq ::
    1.60 @@ -494,7 +495,7 @@
    1.61        let
    1.62          val inj_thms = map fst newT_iso_inj_thms;
    1.63          val rewrites = @{thm o_def} :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
    1.64 -      in Goal.prove_global thy5 [] [] eqn (fn _ => EVERY
    1.65 +      in SkipProof.prove_global thy5 [] [] eqn (fn _ => EVERY
    1.66          [resolve_tac inj_thms 1,
    1.67           rewrite_goals_tac rewrites,
    1.68           rtac refl 3,
    1.69 @@ -516,7 +517,7 @@
    1.70      fun prove_distinct_thms (_, []) = []
    1.71        | prove_distinct_thms (dist_rewrites', t::_::ts) =
    1.72            let
    1.73 -            val dist_thm = Goal.prove_global thy5 [] [] t (fn _ =>
    1.74 +            val dist_thm = SkipProof.prove_global thy5 [] [] t (fn _ =>
    1.75                EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1])
    1.76            in dist_thm::(standard (dist_thm RS not_sym))::
    1.77              (prove_distinct_thms (dist_rewrites', ts))
    1.78 @@ -538,7 +539,7 @@
    1.79          (iso_inj_thms @
    1.80            [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject,
    1.81             Lim_inject, Suml_inject, Sumr_inject]))
    1.82 -      in Goal.prove_global thy5 [] [] t (fn _ => EVERY
    1.83 +      in SkipProof.prove_global thy5 [] [] t (fn _ => EVERY
    1.84          [rtac iffI 1,
    1.85           REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
    1.86           dresolve_tac rep_congs 1, dtac box_equals 1,
    1.87 @@ -588,7 +589,7 @@
    1.88  
    1.89      val cert = cterm_of thy6;
    1.90  
    1.91 -    val indrule_lemma = Goal.prove_global thy6 [] []
    1.92 +    val indrule_lemma = SkipProof.prove_global thy6 [] []
    1.93        (Logic.mk_implies
    1.94          (HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems),
    1.95           HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY
    1.96 @@ -603,7 +604,7 @@
    1.97      val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
    1.98  
    1.99      val dt_induct_prop = DatatypeProp.make_ind descr sorts;
   1.100 -    val dt_induct = Goal.prove_global thy6 []
   1.101 +    val dt_induct = SkipProof.prove_global thy6 []
   1.102        (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
   1.103        (fn prems => EVERY
   1.104          [rtac indrule_lemma' 1,