src/ZF/Tools/ind_cases.ML

absorb structures Decompose and Descent into Termination, to simplify further restructuring

(*  Title:      ZF/Tools/ind_cases.ML
    ID:         $Id$
    Author:     Markus Wenzel, LMU Muenchen

Generic inductive cases facility for (co)inductive definitions.
*)

signature IND_CASES =
sig
  val declare: string -> (simpset -> cterm -> thm) -> theory -> theory
  val inductive_cases: (Attrib.binding * string list) list -> theory -> theory
  val setup: theory -> theory
end;

structure IndCases: IND_CASES =
struct


(* theory data *)

structure IndCasesData = Theory_Data
(
  type T = (simpset -> cterm -> thm) Symtab.table;
  val empty = Symtab.empty;
  val extend = I;
  fun merge data = Symtab.merge (K true) data;
);


fun declare name f = IndCasesData.map (Symtab.update (name, f));

fun smart_cases thy ss read_prop s =
  let
    fun err msg = cat_error msg ("Malformed set membership statement: " ^ s);
    val A = read_prop s handle ERROR msg => err msg;
    val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (FOLogic.dest_Trueprop
      (Logic.strip_imp_concl A)))))) handle TERM _ => err "";
  in
    (case Symtab.lookup (IndCasesData.get thy) c of
      NONE => error ("Unknown inductive cases rule for set " ^ quote c)
    | SOME f => f ss (Thm.cterm_of thy A))
  end;


(* inductive_cases command *)

fun inductive_cases args thy =
  let
    val mk_cases = smart_cases thy (global_simpset_of thy) (Syntax.read_prop_global thy);
    val facts = args |> map (fn ((name, srcs), props) =>
      ((name, map (Attrib.attribute thy) srcs),
        map (Thm.no_attributes o single o mk_cases) props));
  in thy |> PureThy.note_thmss "" facts |> snd end;


(* ind_cases method *)

val setup =
  Method.setup @{binding "ind_cases"}
    (Scan.lift (Scan.repeat1 Args.name_source) >>
      (fn props => fn ctxt =>
        props
        |> map (smart_cases (ProofContext.theory_of ctxt) (simpset_of ctxt) (Syntax.read_prop ctxt))
        |> Method.erule 0))
    "dynamic case analysis on sets";


(* outer syntax *)

local structure P = OuterParse and K = OuterKeyword in

val _ =
  OuterSyntax.command "inductive_cases"
    "create simplified instances of elimination rules (improper)" K.thy_script
    (P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop)
      >> (Toplevel.theory o inductive_cases));

end;

end;