(*  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: ((bstring * Attrib.src list) * string list) list -> theory -> theory

   val setup: theory -> theory

 end;

 structure IndCases: IND_CASES =

 struct

 (* theory data *)

 structure IndCasesData = TheoryDataFun

 (

   type T = (simpset -> cterm -> thm) Symtab.table;

   val empty = Symtab.empty;

   val copy = I;

   val extend = I;

   fun merge _ tabs : T = Symtab.merge (K true) tabs;

 );

 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 read_prop = Syntax.read_prop (ProofContext.init thy);

     val mk_cases = smart_cases thy (Simplifier.simpset_of thy) read_prop;

     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_i "" facts |> snd end;

 (* ind_cases method *)

 fun mk_cases_meth (props, ctxt) =

   props

   |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt) (Syntax.read_prop ctxt))

   |> Method.erule 0;

 val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name));

 (* package setup *)

 val setup =

   Method.add_methods

     [("ind_cases", mk_cases_meth oo mk_cases_args, "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;