src/HOL/Tools/inductive_package.ML
 changeset 6424 ceab9e663e08 parent 6394 3d9fd50fcc43 child 6427 fd36b2e7d80e
```     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Apr 14 14:41:01 1999 +0200
1.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Apr 14 14:42:23 1999 +0200
1.3 @@ -5,16 +5,17 @@
1.4      Copyright   1994  University of Cambridge
1.5                  1998  TU Muenchen
1.6
1.7 -(Co)Inductive Definition module for HOL
1.8 +(Co)Inductive Definition module for HOL.
1.9
1.10  Features:
1.11 -* least or greatest fixedpoints
1.12 -* user-specified product and sum constructions
1.13 -* mutually recursive definitions
1.14 -* definitions involving arbitrary monotone operators
1.15 -* automatically proves introduction and elimination rules
1.16 +  * least or greatest fixedpoints
1.17 +  * user-specified product and sum constructions
1.18 +  * mutually recursive definitions
1.19 +  * definitions involving arbitrary monotone operators
1.20 +  * automatically proves introduction and elimination rules
1.21
1.22 -The recursive sets must *already* be declared as constants in parent theory!
1.23 +The recursive sets must *already* be declared as constants in the
1.24 +current theory!
1.25
1.26    Introduction rules have the form
1.27    [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk |]
1.28 @@ -23,33 +24,39 @@
1.29    ti, t are any terms
1.30    Sj, Sk are two of the sets being defined in mutual recursion
1.31
1.32 -Sums are used only for mutual recursion;
1.33 -Products are used only to derive "streamlined" induction rules for relations
1.34 +Sums are used only for mutual recursion.  Products are used only to
1.35 +derive "streamlined" induction rules for relations.
1.36  *)
1.37
1.38  signature INDUCTIVE_PACKAGE =
1.39  sig
1.40 -  val quiet_mode : bool ref
1.41 -  val add_inductive_i : bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
1.42 -    term list -> thm list -> thm list -> theory -> theory *
1.43 -      {defs:thm list, elims:thm list, raw_induct:thm, induct:thm,
1.44 -       intrs:thm list,
1.45 -       mk_cases:string -> thm, mono:thm,
1.46 -       unfold:thm}
1.47 -  val add_inductive : bool -> bool -> string list -> string list
1.48 -    -> xstring list -> xstring list -> theory -> theory *
1.49 -      {defs:thm list, elims:thm list, raw_induct:thm, induct:thm,
1.50 -       intrs:thm list,
1.51 -       mk_cases:string -> thm, mono:thm,
1.52 -       unfold:thm}
1.53 +  val quiet_mode: bool ref
1.54 +  val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
1.55 +    ((bstring * term) * theory attribute list) list -> thm list -> thm list -> theory -> theory *
1.56 +      {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
1.57 +       intrs: thm list, mk_cases: string -> thm, mono: thm, unfold:thm}
1.58 +  val add_inductive: bool -> bool -> string list -> ((bstring * string) * Args.src list) list ->
1.59 +    (xstring * Args.src list) list -> (xstring * Args.src list) list -> theory -> theory *
1.60 +      {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
1.61 +       intrs:thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
1.62  end;
1.63
1.64 -structure InductivePackage : INDUCTIVE_PACKAGE =
1.65 +structure InductivePackage: INDUCTIVE_PACKAGE =
1.66  struct
1.67
1.68 +(** utilities **)
1.69 +
1.70 +(* messages *)
1.71 +
1.72  val quiet_mode = ref false;
1.73  fun message s = if !quiet_mode then () else writeln s;
1.74
1.75 +fun coind_prefix true = "co"
1.76 +  | coind_prefix false = "";
1.77 +
1.78 +
1.79 +(* misc *)
1.80 +
1.81  (*For proving monotonicity of recursion operator*)
1.82  val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono,
1.83                     ex_mono, Collect_mono, in_mono, vimage_mono];
1.84 @@ -94,7 +101,9 @@
1.85        Abs ("y", cT, mk_inj cs sumT c (Bound 0)) \$ t
1.86    end;
1.87
1.88 -(**************************** well-formedness checks **************************)
1.89 +
1.90 +
1.91 +(** well-formedness checks **)
1.92
1.93  fun err_in_rule sign t msg = error ("Ill-formed introduction rule\n" ^
1.94    (Sign.string_of_term sign t) ^ "\n" ^ msg);
1.95 @@ -121,7 +130,7 @@
1.96
1.97    in (case (HOLogic.dest_Trueprop o Logic.strip_imp_concl) r of
1.98          (Const ("op :", _) \$ _ \$ u) =>
1.99 -          if u mem cs then map (check_prem o HOLogic.dest_Trueprop)
1.100 +          if u mem cs then seq (check_prem o HOLogic.dest_Trueprop)
1.101              (Logic.strip_imp_prems r)
1.102            else err_in_rule sign r msg1
1.103        | _ => err_in_rule sign r msg1)
1.104 @@ -129,9 +138,11 @@
1.105
1.106  fun try' f msg sign t = (f t) handle _ => error (msg ^ Sign.string_of_term sign t);
1.107
1.108 -(*********************** properties of (co)inductive sets *********************)
1.109 +
1.110
1.111 -(***************************** elimination rules ******************************)
1.112 +(*** properties of (co)inductive sets ***)
1.113 +
1.114 +(** elimination rules **)
1.115
1.116  fun mk_elims cs cTs params intr_ts =
1.117    let
1.118 @@ -161,7 +172,9 @@
1.119      map mk_elim (cs ~~ cTs)
1.120    end;
1.121
1.122 -(***************** premises and conclusions of induction rules ****************)
1.123 +
1.124 +
1.125 +(** premises and conclusions of induction rules **)
1.126
1.127  fun mk_indrule cs cTs params intr_ts =
1.128    let
1.129 @@ -217,9 +230,11 @@
1.130    in (preds, ind_prems, mutual_ind_concl)
1.131    end;
1.132
1.133 -(********************** proofs for (co)inductive sets *************************)
1.134 +
1.135
1.136 -(**************************** prove monotonicity ******************************)
1.137 +(*** proofs for (co)inductive sets ***)
1.138 +
1.139 +(** prove monotonicity **)
1.140
1.141  fun prove_mono setT fp_fun monos thy =
1.142    let
1.143 @@ -231,7 +246,9 @@
1.144
1.145    in mono end;
1.146
1.147 -(************************* prove introduction rules ***************************)
1.148 +
1.149 +
1.150 +(** prove introduction rules **)
1.151
1.152  fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy =
1.153    let
1.154 @@ -261,7 +278,9 @@
1.155
1.156    in (intrs, unfold) end;
1.157
1.158 -(*************************** prove elimination rules **************************)
1.159 +
1.160 +
1.161 +(** prove elimination rules **)
1.162
1.163  fun prove_elims cs cTs params intr_ts unfold rec_sets_defs thy =
1.164    let
1.165 @@ -283,6 +302,7 @@
1.166
1.167    in elims end;
1.168
1.169 +
1.170  (** derivation of simplified elimination rules **)
1.171
1.172  (*Applies freeness of the given constructors, which *must* be unfolded by
1.173 @@ -308,7 +328,9 @@
1.174       | None => error ("mk_cases: string '" ^ s ^ "' not of form 't : S_i'")
1.175    end;
1.176
1.177 -(**************************** prove induction rule ****************************)
1.178 +
1.179 +
1.180 +(** prove induction rule **)
1.181
1.182  fun prove_indrule cs cTs sumT rec_const params intr_ts mono
1.183      fp_def rec_sets_defs thy =
1.184 @@ -376,13 +398,17 @@
1.185    in standard (split_rule (induct RS lemma))
1.186    end;
1.187
1.188 -(*************** definitional introduction of (co)inductive sets **************)
1.189 +
1.190 +
1.191 +(*** specification of (co)inductive sets ****)
1.192 +
1.193 +(** definitional introduction of (co)inductive sets **)
1.194
1.195  fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
1.196 -    intr_ts monos con_defs thy params paramTs cTs cnames =
1.197 +    intros monos con_defs thy params paramTs cTs cnames =
1.198    let
1.199 -    val _ = if verbose then message ("Proofs for " ^
1.200 -      (if coind then "co" else "") ^ "inductive set(s) " ^ commas cnames) else ();
1.201 +    val _ = if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
1.202 +      commas_quote cnames) else ();
1.203
1.204      val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
1.205      val setT = HOLogic.mk_setT sumT;
1.206 @@ -390,6 +416,8 @@
1.207      val fp_name = if coind then Sign.intern_const (Theory.sign_of Gfp.thy) "gfp"
1.208        else Sign.intern_const (Theory.sign_of Lfp.thy) "lfp";
1.209
1.210 +    val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
1.211 +
1.212      val used = foldr add_term_names (intr_ts, []);
1.213      val [sname, xname] = variantlist (["S", "x"], used);
1.214
1.215 @@ -444,7 +472,7 @@
1.216
1.217      (* get definitions from theory *)
1.218
1.219 -    val fp_def::rec_sets_defs = get_thms thy' "defs";
1.220 +    val fp_def::rec_sets_defs = PureThy.get_thms thy' "defs";
1.221
1.222      (* prove and store theorems *)
1.223
1.224 @@ -463,13 +491,13 @@
1.225      val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct
1.226        else standard (raw_induct RSN (2, rev_mp));
1.227
1.228 -    val thy'' = thy' |>
1.229 -      PureThy.add_thmss [(("intrs", intrs), [])] |>
1.230 -      (if no_elim then I else PureThy.add_thmss
1.231 -        [(("elims", elims), [])]) |>
1.232 -      (if no_ind then I else PureThy.add_thms
1.233 -        [(((if coind then "co" else "") ^ "induct", induct), [])]) |>
1.234 -      Theory.parent_path;
1.235 +    val thy'' = thy'
1.236 +      |> PureThy.add_thmss [(("intrs", intrs), [])]
1.237 +      |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)
1.238 +      |> (if no_elim then I else PureThy.add_thmss [(("elims", elims), [])])
1.239 +      |> (if no_ind then I else PureThy.add_thms
1.240 +        [((coind_prefix coind ^ "induct", induct), [])])
1.241 +      |> Theory.parent_path;
1.242
1.243    in (thy'',
1.244      {defs = fp_def::rec_sets_defs,
1.245 @@ -482,43 +510,45 @@
1.246       induct = induct})
1.247    end;
1.248
1.249 -(***************** axiomatic introduction of (co)inductive sets ***************)
1.250 +
1.251 +
1.252 +(** axiomatic introduction of (co)inductive sets **)
1.253
1.254  fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs
1.255 -    intr_ts monos con_defs thy params paramTs cTs cnames =
1.256 +    intros monos con_defs thy params paramTs cTs cnames =
1.257    let
1.258 -    val _ = if verbose then message ("Adding axioms for " ^
1.259 -      (if coind then "co" else "") ^ "inductive set(s) " ^ commas cnames) else ();
1.260 +    val _ = if verbose then message ("Adding axioms for " ^ coind_prefix coind ^
1.261 +      "inductive set(s) " ^ commas_quote cnames) else ();
1.262
1.263      val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
1.264
1.265 +    val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
1.266      val elim_ts = mk_elims cs cTs params intr_ts;
1.267
1.268      val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
1.269      val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl);
1.270
1.271 -    val thy' = thy |>
1.272 -      (if declare_consts then
1.273 -        Theory.add_consts_i (map (fn (c, n) =>
1.274 -          (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
1.275 -       else I) |>
1.277 -      PureThy.add_axiomss_i [(("intrs", intr_ts), []), (("elims", elim_ts), [])] |>
1.278 -      (if coind then I
1.279 -       else PureThy.add_axioms_i [(("internal_induct", ind_t), [])]);
1.280 +    val thy' = thy
1.281 +      |> (if declare_consts then
1.283 +              (map (fn (c, n) => (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
1.284 +         else I)
1.286 +      |> PureThy.add_axiomss_i [(("intrs", intr_ts), []), (("elims", elim_ts), [])]
1.287 +      |> (if coind then I else PureThy.add_axioms_i [(("internal_induct", ind_t), [])]);
1.288
1.289 -    val intrs = get_thms thy' "intrs";
1.290 -    val elims = get_thms thy' "elims";
1.291 +    val intrs = PureThy.get_thms thy' "intrs";
1.292 +    val elims = PureThy.get_thms thy' "elims";
1.293      val raw_induct = if coind then TrueI else
1.294 -      standard (split_rule (get_thm thy' "internal_induct"));
1.295 +      standard (split_rule (PureThy.get_thm thy' "internal_induct"));
1.296      val induct = if coind orelse length cs > 1 then raw_induct
1.297        else standard (raw_induct RSN (2, rev_mp));
1.298
1.299 -    val thy'' = thy' |>
1.300 -      (if coind then I
1.301 -       else PureThy.add_thms [(("induct", induct), [])]) |>
1.302 -      Theory.parent_path
1.303 -
1.304 +    val thy'' =
1.305 +      thy'
1.306 +      |> (if coind then I else PureThy.add_thms [(("induct", induct), [])])
1.307 +      |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)
1.308 +      |> Theory.parent_path;
1.309    in (thy'',
1.310      {defs = [],
1.311       mono = TrueI,
1.312 @@ -530,14 +560,14 @@
1.313       induct = induct})
1.314    end;
1.315
1.316 -(********************** introduction of (co)inductive sets ********************)
1.317 +
1.318 +
1.319 +(** introduction of (co)inductive sets **)
1.320
1.321  fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
1.322 -    intr_ts monos con_defs thy =
1.323 +    intros monos con_defs thy =
1.324    let
1.325 -    val _ = Theory.requires thy "Inductive"
1.326 -      ((if coind then "co" else "") ^ "inductive definitions");
1.327 -
1.328 +    val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
1.329      val sign = Theory.sign_of thy;
1.330
1.331      (*parameters should agree for all mutually recursive components*)
1.332 @@ -551,24 +581,27 @@
1.333      val cnames = map (try' (Sign.base_name o fst o dest_Const o head_of)
1.334        "Recursive set not previously declared as constant: " sign) cs;
1.335
1.336 -    val _ = assert_all Syntax.is_identifier cnames
1.337 +    val _ = assert_all Syntax.is_identifier cnames	(* FIXME why? *)
1.338         (fn a => "Base name of recursive set not an identifier: " ^ a);
1.339 -
1.340 -    val _ = map (check_rule sign cs) intr_ts;
1.341 -
1.342 +    val _ = seq (check_rule sign cs o snd o fst) intros;
1.343    in
1.345 -      verbose declare_consts alt_name coind no_elim no_ind cs intr_ts monos
1.346 -        con_defs thy params paramTs cTs cnames
1.348 +      verbose declare_consts alt_name coind no_elim no_ind cs intros monos
1.349 +      con_defs thy params paramTs cTs cnames
1.350    end;
1.351
1.352 -(***************************** external interface *****************************)
1.353 +
1.354
1.355 -fun add_inductive verbose coind c_strings intr_strings monos con_defs thy =
1.356 +(** external interface **)
1.357 +
1.358 +fun add_inductive verbose coind c_strings intro_srcs raw_monos raw_con_defs thy =
1.359    let
1.360      val sign = Theory.sign_of thy;
1.361      val cs = map (readtm (Theory.sign_of thy) HOLogic.termTVar) c_strings;
1.362 -    val intr_ts = map (readtm (Theory.sign_of thy) propT) intr_strings;
1.363 +
1.364 +    val intr_names = map (fst o fst) intro_srcs;
1.365 +    val intr_ts = map (readtm (Theory.sign_of thy) propT o snd o fst) intro_srcs;
1.366 +    val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
1.367
1.368      (* the following code ensures that each recursive set *)
1.369      (* always has the same type in all introduction rules *)
1.370 @@ -598,9 +631,37 @@
1.371      val cs'' = map subst cs';
1.372      val intr_ts'' = map subst intr_ts';
1.373
1.374 -  in add_inductive_i verbose false "" coind false false cs'' intr_ts''
1.375 -    (PureThy.get_thmss thy monos)
1.376 -    (PureThy.get_thmss thy con_defs) thy
1.377 +    val ((thy', con_defs), monos) = thy
1.378 +      |> IsarThy.apply_theorems raw_monos
1.379 +      |> apfst (IsarThy.apply_theorems raw_con_defs);
1.380 +  in
1.381 +    add_inductive_i verbose false "" coind false false cs''
1.382 +      ((intr_names ~~ intr_ts'') ~~ intr_atts) monos con_defs thy'
1.383    end;
1.384
1.385 +
1.386 +
1.387 +(** outer syntax **)
1.388 +
1.389 +local open OuterParse in
1.390 +
1.391 +fun mk_ind coind (((sets, intrs), monos), con_defs) =
1.392 +  #1 o add_inductive true coind sets (map (fn ((x, y), z) => ((x, z), y)) intrs) monos con_defs;
1.393 +
1.394 +fun ind_decl coind =
1.395 +  Scan.repeat1 term --
1.396 +  (\$\$\$ "intrs" |-- !!! (Scan.repeat1 (opt_thm_name ":" -- term))) --
1.397 +  Scan.optional (\$\$\$ "monos" |-- !!! xthms1) [] --
1.398 +  Scan.optional (\$\$\$ "con_defs" |-- !!! xthms1) []
1.399 +  >> (Toplevel.theory o mk_ind coind);
1.400 +
1.401 +val inductiveP = OuterSyntax.command "inductive" "define inductive sets" (ind_decl false);
1.402 +val coinductiveP = OuterSyntax.command "coinductive" "define coinductive sets" (ind_decl true);
1.403 +
1.404 +val _ = OuterSyntax.add_keywords ["intrs", "monos", "con_defs"];
1.405 +val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP];
1.406 +
1.407  end;
1.408 +
1.409 +
1.410 +end;
```