'HOL/inductive' theory data;
authorwenzelm
Fri Apr 16 14:48:16 1999 +0200 (1999-04-16)
changeset 64379bdfe07ba8e9
parent 6436 90eab99706e3
child 6438 e55a1869ed38
'HOL/inductive' theory data;
src/HOL/Inductive.thy
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Inductive.thy	Fri Apr 16 14:43:26 1999 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Fri Apr 16 14:48:16 1999 +0200
     1.3 @@ -1,2 +1,6 @@
     1.4  
     1.5 -Inductive = Gfp + Prod + Sum
     1.6 +Inductive = Gfp + Prod + Sum +
     1.7 +
     1.8 +setup InductivePackage.setup
     1.9 +
    1.10 +end
     2.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Apr 16 14:43:26 1999 +0200
     2.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Apr 16 14:48:16 1999 +0200
     2.3 @@ -31,14 +31,19 @@
     2.4  signature INDUCTIVE_PACKAGE =
     2.5  sig
     2.6    val quiet_mode: bool ref
     2.7 +  val get_inductive: theory -> string ->
     2.8 +    {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
     2.9 +      induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    2.10 +  val print_inductives: theory -> unit
    2.11    val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
    2.12      ((bstring * term) * theory attribute list) list -> thm list -> thm list -> theory -> theory *
    2.13        {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    2.14 -       intrs: thm list, mk_cases: string -> thm, mono: thm, unfold:thm}
    2.15 +       intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    2.16    val add_inductive: bool -> bool -> string list -> ((bstring * string) * Args.src list) list ->
    2.17      (xstring * Args.src list) list -> (xstring * Args.src list) list -> theory -> theory *
    2.18        {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    2.19 -       intrs:thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    2.20 +       intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    2.21 +  val setup: (theory -> theory) list
    2.22  end;
    2.23  
    2.24  structure InductivePackage: INDUCTIVE_PACKAGE =
    2.25 @@ -140,6 +145,48 @@
    2.26  
    2.27  
    2.28  
    2.29 +(*** theory data ***)
    2.30 +
    2.31 +(* data kind 'HOL/inductive' *)
    2.32 +
    2.33 +type inductive_info =
    2.34 +  {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
    2.35 +    induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm};
    2.36 +
    2.37 +structure InductiveArgs =
    2.38 +struct
    2.39 +  val name = "HOL/inductive";
    2.40 +  type T = inductive_info Symtab.table;
    2.41 +
    2.42 +  val empty = Symtab.empty;
    2.43 +  val prep_ext = I;
    2.44 +  val merge: T * T -> T = Symtab.merge (K true);
    2.45 +
    2.46 +  fun print sg tab =
    2.47 +    Pretty.writeln (Pretty.strs ("(co)inductives:" ::
    2.48 +      map (Sign.cond_extern sg Sign.constK o fst) (Symtab.dest tab)));
    2.49 +end;
    2.50 +
    2.51 +structure InductiveData = TheoryDataFun(InductiveArgs);
    2.52 +val print_inductives = InductiveData.print;
    2.53 +
    2.54 +
    2.55 +(* get and put data *)
    2.56 +
    2.57 +fun get_inductive thy name =
    2.58 +  (case Symtab.lookup (InductiveData.get thy, name) of
    2.59 +    Some info => info
    2.60 +  | None => error ("Unknown (co)inductive set " ^ quote name));
    2.61 +
    2.62 +fun put_inductives names info thy =
    2.63 +  let
    2.64 +    fun upd (tab, name) = Symtab.update_new ((name, info), tab);
    2.65 +    val tab = foldl upd (InductiveData.get thy, names)
    2.66 +      handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name);
    2.67 +  in InductiveData.put tab thy end;
    2.68 +
    2.69 +
    2.70 +
    2.71  (*** properties of (co)inductive sets ***)
    2.72  
    2.73  (** elimination rules **)
    2.74 @@ -578,17 +625,20 @@
    2.75      val cTs = map (try' (HOLogic.dest_setT o fastype_of)
    2.76        "Recursive component not of type set: " sign) cs;
    2.77  
    2.78 -    val cnames = map (try' (Sign.base_name o fst o dest_Const o head_of)
    2.79 +    val full_cnames = map (try' (fst o dest_Const o head_of)
    2.80        "Recursive set not previously declared as constant: " sign) cs;
    2.81 +    val cnames = map Sign.base_name full_cnames;
    2.82  
    2.83      val _ = assert_all Syntax.is_identifier cnames	(* FIXME why? *)
    2.84         (fn a => "Base name of recursive set not an identifier: " ^ a);
    2.85      val _ = seq (check_rule sign cs o snd o fst) intros;
    2.86 -  in
    2.87 -    (if ! quick_and_dirty then add_ind_axm else add_ind_def)
    2.88 -      verbose declare_consts alt_name coind no_elim no_ind cs intros monos
    2.89 -      con_defs thy params paramTs cTs cnames
    2.90 -  end;
    2.91 +
    2.92 +    val (thy1, result) =
    2.93 +      (if ! quick_and_dirty then add_ind_axm else add_ind_def)
    2.94 +        verbose declare_consts alt_name coind no_elim no_ind cs intros monos
    2.95 +        con_defs thy params paramTs cTs cnames;
    2.96 +    val thy2 = thy1 |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result);
    2.97 +  in (thy2, result) end;
    2.98  
    2.99  
   2.100  
   2.101 @@ -641,7 +691,14 @@
   2.102  
   2.103  
   2.104  
   2.105 -(** outer syntax **)
   2.106 +(** package setup **)
   2.107 +
   2.108 +(* setup theory *)
   2.109 +
   2.110 +val setup = [InductiveData.init];
   2.111 +
   2.112 +
   2.113 +(* outer syntax *)
   2.114  
   2.115  local open OuterParse in
   2.116