src/HOL/Tools/inductive_package.ML
changeset 8277 493707fcd8a6
parent 8100 6186ee807f2e
child 8293 4a0e17cf8f70
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Feb 22 21:39:38 2000 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Feb 22 21:45:20 2000 +0100
     1.3 @@ -36,6 +36,8 @@
     1.4      {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
     1.5        induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
     1.6    val print_inductives: theory -> unit
     1.7 +  val cases_of: Sign.sg -> string -> thm
     1.8 +  val cases: Sign.sg -> thm list
     1.9    val mono_add_global: theory attribute
    1.10    val mono_del_global: theory attribute
    1.11    val get_monos: theory -> thm list
    1.12 @@ -102,12 +104,30 @@
    1.13        handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name);
    1.14    in InductiveData.put tab_monos thy end;
    1.15  
    1.16 -val get_monos = snd o InductiveData.get;
    1.17 +
    1.18 +(* cases rules *)
    1.19  
    1.20 -fun put_monos thms thy = InductiveData.put (fst (InductiveData.get thy), thms) thy;
    1.21 +fun cases_of sg name =
    1.22 +  let
    1.23 +    fun find (None, (_, ({names, ...}, {elims, ...}): inductive_info)) =
    1.24 +          assoc (names ~~ elims, name)
    1.25 +      | find (some, _) = some;
    1.26 +    val (tab, _) = InductiveData.get_sg sg;
    1.27 +  in
    1.28 +    (case Symtab.foldl find (None, tab) of
    1.29 +      None => error ("Unknown (co)inductive set " ^ quote name)
    1.30 +    | Some thm => thm)
    1.31 +  end;
    1.32 +
    1.33 +fun cases sg = flat (map (#elims o #2 o #2) (Symtab.dest (#1 (InductiveData.get_sg sg))));
    1.34 +      
    1.35 +
    1.36  
    1.37  (** monotonicity rules **)
    1.38  
    1.39 +val get_monos = snd o InductiveData.get;
    1.40 +fun put_monos thms thy = InductiveData.put (fst (InductiveData.get thy), thms) thy;
    1.41 +
    1.42  fun mk_mono thm =
    1.43    let
    1.44      fun eq2mono thm' = [standard (thm' RS (thm' RS eq_to_mono))] @