(* Title: ZF/Tools/ind_cases.ML ID: $Id: ind_cases.ML,v 1.14 2005/09/15 15:17:00 wenzelm Exp $ 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) list end; structure IndCases: IND_CASES = struct (* theory data *) structure IndCasesData = TheoryDataFun (struct val name = "ZF/ind_cases"; 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 print _ _ = (); end); fun declare name f = IndCasesData.map (Symtab.update (name, f)); fun smart_cases thy ss read_prop s = let fun err () = error ("Malformed set membership statement: " ^ s); val A = read_prop s handle ERROR => err (); 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 (Theory.sign_of thy) A)) end; (* inductive_cases command *) fun inductive_cases args thy = let val read_prop = ProofContext.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.global_attribute thy) srcs), map (Thm.no_attributes o single o mk_cases) props)); in thy |> IsarThy.theorems_i Drule.lemmaK facts |> #1 end; (* ind_cases method *) fun mk_cases_meth (ctxt, props) = props |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt) (ProofContext.read_prop ctxt)) |> Method.erule 0; val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name)); (* package setup *) val setup = [IndCasesData.init, 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 ind_cases = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop) >> (Toplevel.theory o inductive_cases); val inductive_casesP = OuterSyntax.command "inductive_cases" "create simplified instances of elimination rules (improper)" K.thy_script ind_cases; val _ = OuterSyntax.add_parsers [inductive_casesP]; end; end;