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.276 -      Theory.add_path rec_name |>
   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.282 +            Theory.add_consts_i
   1.283 +              (map (fn (c, n) => (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
   1.284 +         else I)
   1.285 +      |> Theory.add_path rec_name
   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.344 -    (if !quick_and_dirty then add_ind_axm else add_ind_def)
   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.347 +    (if ! quick_and_dirty then add_ind_axm else add_ind_def)
   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;