- use SkipProof.prove_global instead of Goal.prove_global
authorberghofe
Thu Apr 03 17:49:39 2008 +0200 (2008-04-03)
changeset 2653196e82c7861fa
parent 26530 777f334ff652
child 26532 3fc9730403c1
- use SkipProof.prove_global instead of Goal.prove_global
- added skip_mono flag to inductive definition package
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_rep_proofs.ML
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Thu Apr 03 17:43:01 2008 +0200
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Thu Apr 03 17:49:39 2008 +0200
     1.3 @@ -70,7 +70,7 @@
     1.4            (split_conj_thm (cterm_instantiate insts' induct), i)) RSN (2, rev_mp))
     1.5  
     1.6        in
     1.7 -        Goal.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
     1.8 +        SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
     1.9            (fn prems => EVERY
    1.10              [rtac induct' 1,
    1.11               REPEAT (rtac TrueI 1),
    1.12 @@ -156,7 +156,8 @@
    1.13      val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
    1.14          InductivePackage.add_inductive_global (serial_string ())
    1.15            {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
    1.16 -            alt_name = big_rec_name', coind = false, no_elim = false, no_ind = true}
    1.17 +            alt_name = big_rec_name', coind = false, no_elim = false, no_ind = true,
    1.18 +            skip_mono = true}
    1.19            (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
    1.20            (map dest_Free rec_fns)
    1.21            (map (fn x => (("", []), x)) rec_intr_ts) [] thy0;
    1.22 @@ -216,7 +217,7 @@
    1.23                THEN rewtac (mk_meta_eq choice_eq), rec_intrs),
    1.24              descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts);
    1.25  
    1.26 -      in split_conj_thm (Goal.prove_global thy1 [] []
    1.27 +      in split_conj_thm (SkipProof.prove_global thy1 [] []
    1.28          (HOLogic.mk_Trueprop (mk_conj rec_unique_ts)) (K tac))
    1.29        end;
    1.30  
    1.31 @@ -250,7 +251,7 @@
    1.32  
    1.33      val _ = message "Proving characteristic theorems for primrec combinators ..."
    1.34  
    1.35 -    val rec_thms = map (fn t => Goal.prove_global thy2 [] [] t
    1.36 +    val rec_thms = map (fn t => SkipProof.prove_global thy2 [] [] t
    1.37        (fn _ => EVERY
    1.38          [rewrite_goals_tac reccomb_defs,
    1.39           rtac the1_equality 1,
    1.40 @@ -328,7 +329,7 @@
    1.41          end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~
    1.42            (Library.take (length newTs, reccomb_names)));
    1.43  
    1.44 -    val case_thms = map (map (fn t => Goal.prove_global thy2 [] [] t
    1.45 +    val case_thms = map (map (fn t => SkipProof.prove_global thy2 [] [] t
    1.46        (fn _ => EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1])))
    1.47            (DatatypeProp.make_cases new_type_names descr sorts thy2)
    1.48  
    1.49 @@ -361,8 +362,8 @@
    1.50          val tacf = K (EVERY [rtac exhaustion' 1, ALLGOALS (asm_simp_tac
    1.51            (HOL_ss addsimps (dist_rewrites' @ inject @ case_thms')))])
    1.52        in
    1.53 -        (Goal.prove_global thy [] [] t1 tacf,
    1.54 -         Goal.prove_global thy [] [] t2 tacf)
    1.55 +        (SkipProof.prove_global thy [] [] t1 tacf,
    1.56 +         SkipProof.prove_global thy [] [] t2 tacf)
    1.57        end;
    1.58  
    1.59      val split_thm_pairs = map prove_split_thms
    1.60 @@ -381,7 +382,7 @@
    1.61  fun prove_weak_case_congs new_type_names descr sorts thy =
    1.62    let
    1.63      fun prove_weak_case_cong t =
    1.64 -       Goal.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
    1.65 +       SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
    1.66           (fn prems => EVERY [rtac ((hd prems) RS arg_cong) 1])
    1.67  
    1.68      val weak_case_congs = map prove_weak_case_cong (DatatypeProp.make_weak_case_congs
    1.69 @@ -402,7 +403,7 @@
    1.70                hyp_subst_tac i, REPEAT (rtac exI i), rtac refl i]
    1.71            | tac i n = rtac disjI2 i THEN tac i (n - 1)
    1.72        in 
    1.73 -        Goal.prove_global thy [] [] t (fn _ =>
    1.74 +        SkipProof.prove_global thy [] [] t (fn _ =>
    1.75            EVERY [rtac allI 1,
    1.76             exh_tac (K exhaustion) 1,
    1.77             ALLGOALS (fn i => tac i (i-1))])
    1.78 @@ -424,7 +425,7 @@
    1.79          val nchotomy'' = cterm_instantiate
    1.80            [(cert (hd (add_term_vars (concl_of nchotomy', []))), cert Ma)] nchotomy'
    1.81        in
    1.82 -        Goal.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
    1.83 +        SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
    1.84            (fn prems => 
    1.85              let val simplify = asm_simp_tac (HOL_ss addsimps (prems @ case_rewrites))
    1.86              in EVERY [simp_tac (HOL_ss addsimps [hd prems]) 1,
     2.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Apr 03 17:43:01 2008 +0200
     2.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Apr 03 17:49:39 2008 +0200
     2.3 @@ -177,8 +177,9 @@
     2.4  
     2.5      val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
     2.6          InductivePackage.add_inductive_global (serial_string ())
     2.7 -          {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK, alt_name = big_rec_name,
     2.8 -            coind = false, no_elim = true, no_ind = false}
     2.9 +          {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
    2.10 +           alt_name = big_rec_name, coind = false, no_elim = true, no_ind = false,
    2.11 +           skip_mono = true}
    2.12            (map (fn s => ((s, UnivT'), NoSyn)) rep_set_names') []
    2.13            (map (fn x => (("", []), x)) intr_ts) [] thy1;
    2.14  
    2.15 @@ -346,7 +347,7 @@
    2.16          (* prove characteristic equations *)
    2.17  
    2.18          val rewrites = def_thms @ (map mk_meta_eq rec_rewrites);
    2.19 -        val char_thms' = map (fn eqn => Goal.prove_global thy' [] [] eqn
    2.20 +        val char_thms' = map (fn eqn => SkipProof.prove_global thy' [] [] eqn
    2.21            (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) eqns;
    2.22  
    2.23        in (thy', char_thms' @ char_thms) end;
    2.24 @@ -368,7 +369,7 @@
    2.25              val Ts = map (TFree o rpair HOLogic.typeS)
    2.26                (Name.variant_list used (replicate i "'t"));
    2.27              val f = Free ("f", Ts ---> U)
    2.28 -          in Goal.prove_global thy [] [] (Logic.mk_implies
    2.29 +          in SkipProof.prove_global thy [] [] (Logic.mk_implies
    2.30              (HOLogic.mk_Trueprop (HOLogic.list_all
    2.31                 (map (pair "x") Ts, S $ app_bnds f i)),
    2.32               HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
    2.33 @@ -401,7 +402,7 @@
    2.34          val inj_thms' = map snd newT_iso_inj_thms @
    2.35            map (fn r => r RS @{thm injD}) inj_thms;
    2.36  
    2.37 -        val inj_thm = Goal.prove_global thy5 [] []
    2.38 +        val inj_thm = SkipProof.prove_global thy5 [] []
    2.39            (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
    2.40              [(indtac induction [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    2.41               REPEAT (EVERY
    2.42 @@ -427,7 +428,7 @@
    2.43                               (split_conj_thm inj_thm);
    2.44  
    2.45          val elem_thm = 
    2.46 -            Goal.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
    2.47 +            SkipProof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
    2.48                (fn _ =>
    2.49                 EVERY [(indtac induction [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    2.50                  rewrite_goals_tac rewrites,
    2.51 @@ -464,7 +465,7 @@
    2.52  
    2.53      val iso_thms = if length descr = 1 then [] else
    2.54        Library.drop (length newTs, split_conj_thm
    2.55 -        (Goal.prove_global thy5 [] [] iso_t (fn _ => EVERY
    2.56 +        (SkipProof.prove_global thy5 [] [] iso_t (fn _ => EVERY
    2.57             [(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    2.58              REPEAT (rtac TrueI 1),
    2.59              rewrite_goals_tac (mk_meta_eq choice_eq ::
    2.60 @@ -494,7 +495,7 @@
    2.61        let
    2.62          val inj_thms = map fst newT_iso_inj_thms;
    2.63          val rewrites = @{thm o_def} :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
    2.64 -      in Goal.prove_global thy5 [] [] eqn (fn _ => EVERY
    2.65 +      in SkipProof.prove_global thy5 [] [] eqn (fn _ => EVERY
    2.66          [resolve_tac inj_thms 1,
    2.67           rewrite_goals_tac rewrites,
    2.68           rtac refl 3,
    2.69 @@ -516,7 +517,7 @@
    2.70      fun prove_distinct_thms (_, []) = []
    2.71        | prove_distinct_thms (dist_rewrites', t::_::ts) =
    2.72            let
    2.73 -            val dist_thm = Goal.prove_global thy5 [] [] t (fn _ =>
    2.74 +            val dist_thm = SkipProof.prove_global thy5 [] [] t (fn _ =>
    2.75                EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1])
    2.76            in dist_thm::(standard (dist_thm RS not_sym))::
    2.77              (prove_distinct_thms (dist_rewrites', ts))
    2.78 @@ -538,7 +539,7 @@
    2.79          (iso_inj_thms @
    2.80            [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject,
    2.81             Lim_inject, Suml_inject, Sumr_inject]))
    2.82 -      in Goal.prove_global thy5 [] [] t (fn _ => EVERY
    2.83 +      in SkipProof.prove_global thy5 [] [] t (fn _ => EVERY
    2.84          [rtac iffI 1,
    2.85           REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
    2.86           dresolve_tac rep_congs 1, dtac box_equals 1,
    2.87 @@ -588,7 +589,7 @@
    2.88  
    2.89      val cert = cterm_of thy6;
    2.90  
    2.91 -    val indrule_lemma = Goal.prove_global thy6 [] []
    2.92 +    val indrule_lemma = SkipProof.prove_global thy6 [] []
    2.93        (Logic.mk_implies
    2.94          (HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems),
    2.95           HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY
    2.96 @@ -603,7 +604,7 @@
    2.97      val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
    2.98  
    2.99      val dt_induct_prop = DatatypeProp.make_ind descr sorts;
   2.100 -    val dt_induct = Goal.prove_global thy6 []
   2.101 +    val dt_induct = SkipProof.prove_global thy6 []
   2.102        (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
   2.103        (fn prems => EVERY
   2.104          [rtac indrule_lemma' 1,