Now also proves monotonicity when in quick_and_dirty mode.
authorberghofe
Thu Jun 15 16:02:12 2000 +0200 (2000-06-15)
changeset 9072a4896cf23638
parent 9071 6416d5a5f712
child 9073 40d8dfac96b8
Now also proves monotonicity when in quick_and_dirty mode.
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Jun 14 18:24:41 2000 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Jun 15 16:02:12 2000 +0200
     1.3 @@ -592,20 +592,15 @@
     1.4  
     1.5  (** definitional introduction of (co)inductive sets **)
     1.6  
     1.7 -fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
     1.8 -    atts intros monos con_defs thy params paramTs cTs cnames induct_cases =
     1.9 +fun mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy
    1.10 +      params paramTs cTs cnames =
    1.11    let
    1.12 -    val _ = if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
    1.13 -      commas_quote cnames) else ();
    1.14 -
    1.15      val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
    1.16      val setT = HOLogic.mk_setT sumT;
    1.17  
    1.18      val fp_name = if coind then Sign.intern_const (Theory.sign_of Gfp.thy) "gfp"
    1.19        else Sign.intern_const (Theory.sign_of Lfp.thy) "lfp";
    1.20  
    1.21 -    val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
    1.22 -
    1.23      val used = foldr add_term_names (intr_ts, []);
    1.24      val [sname, xname] = variantlist (["S", "x"], used);
    1.25  
    1.26 @@ -659,10 +654,24 @@
    1.27        |> Theory.add_path rec_name
    1.28        |> PureThy.add_defss_i [(("defs", def_terms), [])];
    1.29  
    1.30 +    val mono = prove_mono setT fp_fun monos thy'
    1.31  
    1.32 -    (* prove and store theorems *)
    1.33 +  in
    1.34 +    (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) 
    1.35 +  end;
    1.36  
    1.37 -    val mono = prove_mono setT fp_fun monos thy';
    1.38 +fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
    1.39 +    atts intros monos con_defs thy params paramTs cTs cnames induct_cases =
    1.40 +  let
    1.41 +    val _ = if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
    1.42 +      commas_quote cnames) else ();
    1.43 +
    1.44 +    val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
    1.45 +
    1.46 +    val (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) =
    1.47 +      mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy
    1.48 +        params paramTs cTs cnames;
    1.49 +
    1.50      val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs
    1.51        rec_sets_defs thy';
    1.52      val elims = if no_elim then [] else
    1.53 @@ -705,41 +714,38 @@
    1.54  fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs
    1.55      atts intros monos con_defs thy params paramTs cTs cnames induct_cases =
    1.56    let
    1.57 -    val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
    1.58 +    val _ = message (coind_prefix coind ^ "inductive set(s) " ^ commas_quote cnames);
    1.59  
    1.60      val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
    1.61 +    val (thy', _, _, _, _, _) =
    1.62 +      mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy
    1.63 +        params paramTs cTs cnames;
    1.64      val (elim_ts, elim_cases) = Library.split_list (mk_elims cs cTs params intr_ts intr_names);
    1.65 -
    1.66      val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
    1.67      val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl);
    1.68      
    1.69 -    val thy' =
    1.70 -      thy
    1.71 -      |> (if declare_consts then
    1.72 -            Theory.add_consts_i
    1.73 -              (map (fn (c, n) => (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
    1.74 -         else I)
    1.75 -      |> Theory.add_path rec_name
    1.76 +    val thy'' =
    1.77 +      thy'
    1.78        |> (#1 o PureThy.add_axiomss_i [(("intrs", intr_ts), atts), (("raw_elims", elim_ts), [])])
    1.79        |> (if coind then I else
    1.80              #1 o PureThy.add_axioms_i [(("raw_induct", ind_t), [apsnd (standard o split_rule)])]);
    1.81  
    1.82 -    val intrs = PureThy.get_thms thy' "intrs";
    1.83 +    val intrs = PureThy.get_thms thy'' "intrs";
    1.84      val elims = map2 (fn (th, cases) => RuleCases.name cases th)
    1.85 -      (PureThy.get_thms thy' "raw_elims", elim_cases);
    1.86 -    val raw_induct = if coind then Drule.asm_rl else PureThy.get_thm thy' "raw_induct";
    1.87 +      (PureThy.get_thms thy'' "raw_elims", elim_cases);
    1.88 +    val raw_induct = if coind then Drule.asm_rl else PureThy.get_thm thy'' "raw_induct";
    1.89      val induct = if coind orelse length cs > 1 then raw_induct
    1.90        else standard (raw_induct RSN (2, rev_mp));
    1.91  
    1.92 -    val (thy'', ([elims'], intrs')) =
    1.93 -      thy'
    1.94 +    val (thy''', ([elims'], intrs')) =
    1.95 +      thy''
    1.96        |> PureThy.add_thmss [(("elims", elims), [])]
    1.97        |>> (if coind then I
    1.98            else #1 o PureThy.add_thms [(("induct", induct), [RuleCases.case_names induct_cases])])
    1.99        |>>> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)
   1.100        |>> Theory.parent_path;
   1.101 -    val induct' = if coind then raw_induct else PureThy.get_thm thy'' "induct";
   1.102 -  in (thy'',
   1.103 +    val induct' = if coind then raw_induct else PureThy.get_thm thy''' "induct";
   1.104 +  in (thy''',
   1.105      {defs = [],
   1.106       mono = Drule.asm_rl,
   1.107       unfold = Drule.asm_rl,