declare coinduct rule;
authorwenzelm
Tue Nov 22 19:34:40 2005 +0100 (2005-11-22 ago)
changeset 18222a8ccacce3b52
parent 18221 93302908b8eb
child 18223 20830cb4428c
declare coinduct rule;
tuned;
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Nov 22 14:32:01 2005 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Nov 22 19:34:40 2005 +0100
     1.3 @@ -83,8 +83,6 @@
     1.4  
     1.5  (** theory data **)
     1.6  
     1.7 -(* data kind 'HOL/inductive' *)
     1.8 -
     1.9  type inductive_info =
    1.10    {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
    1.11      induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm};
    1.12 @@ -121,12 +119,9 @@
    1.13  
    1.14  val the_mk_cases = (#mk_cases o #2) oo the_inductive;
    1.15  
    1.16 -fun put_inductives names info thy =
    1.17 -  let
    1.18 -    fun upd ((tab, monos), name) = (Symtab.update_new (name, info) tab, monos);
    1.19 -    val tab_monos = Library.foldl upd (InductiveData.get thy, names)
    1.20 -      handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name);
    1.21 -  in InductiveData.put tab_monos thy end;
    1.22 +fun put_inductives names info = InductiveData.map (apfst (fn tab =>
    1.23 +  fold (fn name => Symtab.update_new (name, info)) names tab
    1.24 +    handle Symtab.DUP dup => error ("Duplicate definition of (co)inductive set " ^ quote dup)));
    1.25  
    1.26  
    1.27  
    1.28 @@ -316,10 +311,11 @@
    1.29      ((name, arule), att)
    1.30    end;
    1.31  
    1.32 -val rulify =
    1.33 -  standard o
    1.34 -  hol_simplify inductive_rulify2 o hol_simplify inductive_rulify1 o
    1.35 -  hol_simplify inductive_conj;
    1.36 +val rulify =  (* FIXME norm_hhf *)
    1.37 +  hol_simplify inductive_conj
    1.38 +  #> hol_simplify inductive_rulify1
    1.39 +  #> hol_simplify inductive_rulify2
    1.40 +  #> standard;
    1.41  
    1.42  end;
    1.43  
    1.44 @@ -450,7 +446,7 @@
    1.45              RS mp |> Thm.permute_prems 0 ~1 |> Drule.standard;
    1.46        in names ~~ map proj (1 upto n) end;
    1.47  
    1.48 -fun add_cases_induct no_elim no_induct names elims induct =
    1.49 +fun add_cases_induct no_elim no_induct coind names elims induct =
    1.50    let
    1.51      fun cases_spec (name, elim) thy =
    1.52        thy
    1.53 @@ -459,9 +455,12 @@
    1.54        |> Theory.parent_path;
    1.55      val cases_specs = if no_elim then [] else map2 cases_spec (names, elims);
    1.56  
    1.57 +    val induct_att =
    1.58 +      if coind then InductAttrib.coinduct_set_global else InductAttrib.induct_set_global;
    1.59      fun induct_spec (name, th) = #1 o PureThy.add_thms
    1.60 -      [(("", RuleCases.save induct th), [InductAttrib.induct_set_global name])];
    1.61 -    val induct_specs = if no_induct then [] else map induct_spec (project_rules names induct);
    1.62 +      [(("", RuleCases.save induct th), [induct_att name])];
    1.63 +    val induct_specs =
    1.64 +      if no_induct then [] else map induct_spec (project_rules names induct);
    1.65    in Library.apply (cases_specs @ induct_specs) end;
    1.66  
    1.67  
    1.68 @@ -493,7 +492,7 @@
    1.69        | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
    1.70  
    1.71      val intrs = (1 upto (length intr_ts) ~~ intr_ts) |> map (fn (i, intr) =>
    1.72 -      rulify (standard (SkipProof.prove thy [] [] intr (fn _ => EVERY
    1.73 +      rulify (SkipProof.prove thy [] [] intr (fn _ => EVERY
    1.74         [rewrite_goals_tac rec_sets_defs,
    1.75          stac unfold 1,
    1.76          REPEAT (resolve_tac [vimageI2, CollectI] 1),
    1.77 @@ -503,7 +502,7 @@
    1.78            backtracking may occur if the premises have extra variables!*)
    1.79          DEPTH_SOLVE_1 (resolve_tac [refl, exI, conjI] 1 APPEND assume_tac 1),
    1.80          (*Now solve the equations like Inl 0 = Inl ?b2*)
    1.81 -        REPEAT (rtac refl 1)]))))
    1.82 +        REPEAT (rtac refl 1)])))
    1.83  
    1.84    in (intrs, unfold) end;
    1.85  
    1.86 @@ -527,7 +526,6 @@
    1.87             REPEAT (FIRSTGOAL (eresolve_tac rules2)),
    1.88             EVERY (map (fn prem =>
    1.89               DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_sets_defs prem, conjI] 1)) (tl prems))])
    1.90 -        |> standard
    1.91          |> rulify
    1.92          |> RuleCases.name cases)
    1.93    end;
    1.94 @@ -762,7 +760,7 @@
    1.95  
    1.96      val mono = prove_mono setT fp_fun monos thy'
    1.97  
    1.98 -  in (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) end;
    1.99 +  in (thy', rec_name, mono, fp_def, rec_sets_defs, rec_const, sumT) end;
   1.100  
   1.101  fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
   1.102      intros monos thy params paramTs cTs cnames induct_cases =
   1.103 @@ -773,7 +771,7 @@
   1.104  
   1.105      val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
   1.106  
   1.107 -    val (thy1, mono, fp_def, rec_sets_defs, rec_const, sumT) =
   1.108 +    val (thy1, rec_name, mono, fp_def, rec_sets_defs, rec_const, sumT) =
   1.109        mk_ind_def declare_consts alt_name coind cs intr_ts monos thy
   1.110          params paramTs cTs cnames;
   1.111  
   1.112 @@ -788,19 +786,23 @@
   1.113          prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
   1.114            rec_sets_defs thy1;
   1.115      val induct =
   1.116 -      if coind orelse no_ind orelse length cs > 1 then (raw_induct, [RuleCases.consumes 0])
   1.117 -      else (raw_induct RSN (2, rev_mp), [RuleCases.consumes 1]);
   1.118 +      if coind then
   1.119 +        (raw_induct, [RuleCases.case_names [rec_name],
   1.120 +          RuleCases.case_conclusion_binops rec_name induct_cases,
   1.121 +          RuleCases.consumes 1])
   1.122 +      else if no_ind orelse length cs > 1 then
   1.123 +        (raw_induct, [RuleCases.case_names induct_cases, RuleCases.consumes 0])
   1.124 +      else (raw_induct RSN (2, rev_mp), [RuleCases.case_names induct_cases, RuleCases.consumes 1]);
   1.125  
   1.126      val (thy2, intrs') =
   1.127        thy1 |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts);
   1.128 -    val (thy3, ([intrs'', elims'], [induct'])) =
   1.129 +    val (thy3, ([_, elims'], [induct'])) =
   1.130        thy2
   1.131        |> PureThy.add_thmss
   1.132          [(("intros", intrs'), []),
   1.133            (("elims", elims), [RuleCases.consumes 1])]
   1.134        |>>> PureThy.add_thms
   1.135 -        [((coind_prefix coind ^ "induct", rulify (#1 induct)),
   1.136 -         (RuleCases.case_names induct_cases :: #2 induct))]
   1.137 +        [((coind_prefix coind ^ "induct", rulify (#1 induct)), #2 induct)]
   1.138        |>> Theory.parent_path;
   1.139    in (thy3,
   1.140      {defs = fp_def :: rec_sets_defs,
   1.141 @@ -846,7 +848,7 @@
   1.142          thy params paramTs cTs cnames induct_cases;
   1.143      val thy2 = thy1
   1.144        |> put_inductives cnames ({names = cnames, coind = coind}, result)
   1.145 -      |> add_cases_induct no_elim (no_ind orelse coind orelse length cs > 1)
   1.146 +      |> add_cases_induct no_elim (no_ind orelse length cs > 1) coind
   1.147            cnames elims induct;
   1.148    in (thy2, result) end;
   1.149