src/HOL/Tools/inductive_package.ML
changeset 6437 9bdfe07ba8e9
parent 6430 69400c97d3bf
child 6521 16c425fc00cb
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Apr 16 14:43:26 1999 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Apr 16 14:48:16 1999 +0200
     1.3 @@ -31,14 +31,19 @@
     1.4  signature INDUCTIVE_PACKAGE =
     1.5  sig
     1.6    val quiet_mode: bool ref
     1.7 +  val get_inductive: theory -> string ->
     1.8 +    {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
     1.9 +      induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    1.10 +  val print_inductives: theory -> unit
    1.11    val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
    1.12      ((bstring * term) * theory attribute list) list -> thm list -> thm list -> theory -> theory *
    1.13        {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    1.14 -       intrs: thm list, mk_cases: string -> thm, mono: thm, unfold:thm}
    1.15 +       intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    1.16    val add_inductive: bool -> bool -> string list -> ((bstring * string) * Args.src list) list ->
    1.17      (xstring * Args.src list) list -> (xstring * Args.src list) list -> theory -> theory *
    1.18        {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    1.19 -       intrs:thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    1.20 +       intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    1.21 +  val setup: (theory -> theory) list
    1.22  end;
    1.23  
    1.24  structure InductivePackage: INDUCTIVE_PACKAGE =
    1.25 @@ -140,6 +145,48 @@
    1.26  
    1.27  
    1.28  
    1.29 +(*** theory data ***)
    1.30 +
    1.31 +(* data kind 'HOL/inductive' *)
    1.32 +
    1.33 +type inductive_info =
    1.34 +  {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
    1.35 +    induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm};
    1.36 +
    1.37 +structure InductiveArgs =
    1.38 +struct
    1.39 +  val name = "HOL/inductive";
    1.40 +  type T = inductive_info Symtab.table;
    1.41 +
    1.42 +  val empty = Symtab.empty;
    1.43 +  val prep_ext = I;
    1.44 +  val merge: T * T -> T = Symtab.merge (K true);
    1.45 +
    1.46 +  fun print sg tab =
    1.47 +    Pretty.writeln (Pretty.strs ("(co)inductives:" ::
    1.48 +      map (Sign.cond_extern sg Sign.constK o fst) (Symtab.dest tab)));
    1.49 +end;
    1.50 +
    1.51 +structure InductiveData = TheoryDataFun(InductiveArgs);
    1.52 +val print_inductives = InductiveData.print;
    1.53 +
    1.54 +
    1.55 +(* get and put data *)
    1.56 +
    1.57 +fun get_inductive thy name =
    1.58 +  (case Symtab.lookup (InductiveData.get thy, name) of
    1.59 +    Some info => info
    1.60 +  | None => error ("Unknown (co)inductive set " ^ quote name));
    1.61 +
    1.62 +fun put_inductives names info thy =
    1.63 +  let
    1.64 +    fun upd (tab, name) = Symtab.update_new ((name, info), tab);
    1.65 +    val tab = foldl upd (InductiveData.get thy, names)
    1.66 +      handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name);
    1.67 +  in InductiveData.put tab thy end;
    1.68 +
    1.69 +
    1.70 +
    1.71  (*** properties of (co)inductive sets ***)
    1.72  
    1.73  (** elimination rules **)
    1.74 @@ -578,17 +625,20 @@
    1.75      val cTs = map (try' (HOLogic.dest_setT o fastype_of)
    1.76        "Recursive component not of type set: " sign) cs;
    1.77  
    1.78 -    val cnames = map (try' (Sign.base_name o fst o dest_Const o head_of)
    1.79 +    val full_cnames = map (try' (fst o dest_Const o head_of)
    1.80        "Recursive set not previously declared as constant: " sign) cs;
    1.81 +    val cnames = map Sign.base_name full_cnames;
    1.82  
    1.83      val _ = assert_all Syntax.is_identifier cnames	(* FIXME why? *)
    1.84         (fn a => "Base name of recursive set not an identifier: " ^ a);
    1.85      val _ = seq (check_rule sign cs o snd o fst) intros;
    1.86 -  in
    1.87 -    (if ! quick_and_dirty then add_ind_axm else add_ind_def)
    1.88 -      verbose declare_consts alt_name coind no_elim no_ind cs intros monos
    1.89 -      con_defs thy params paramTs cTs cnames
    1.90 -  end;
    1.91 +
    1.92 +    val (thy1, result) =
    1.93 +      (if ! quick_and_dirty then add_ind_axm else add_ind_def)
    1.94 +        verbose declare_consts alt_name coind no_elim no_ind cs intros monos
    1.95 +        con_defs thy params paramTs cTs cnames;
    1.96 +    val thy2 = thy1 |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result);
    1.97 +  in (thy2, result) end;
    1.98  
    1.99  
   1.100  
   1.101 @@ -641,7 +691,14 @@
   1.102  
   1.103  
   1.104  
   1.105 -(** outer syntax **)
   1.106 +(** package setup **)
   1.107 +
   1.108 +(* setup theory *)
   1.109 +
   1.110 +val setup = [InductiveData.init];
   1.111 +
   1.112 +
   1.113 +(* outer syntax *)
   1.114  
   1.115  local open OuterParse in
   1.116