# HG changeset patch # User wenzelm # Date 1005686415 -3600 # Node ID a0aab0b9f2e977a9b488bb77e42bcaae56185617 # Parent f3f7993ae6da956c7c8092f820b45d8f945b4c7c Generic inductive cases facility for (co)inductive definitions. diff -r f3f7993ae6da -r a0aab0b9f2e9 src/ZF/Tools/ind_cases.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Tools/ind_cases.ML Tue Nov 13 22:20:15 2001 +0100 @@ -0,0 +1,100 @@ +(* Title: ZF/Tools/ind_cases.ML + ID: $Id$ + Author: Markus Wenzel, LMU Muenchen + License: GPL (GNU GENERAL PUBLIC LICENSE) + +Generic inductive cases facility for (co)inductive definitions. +*) + +signature IND_CASES = +sig + val declare: string -> (simpset -> cterm -> thm) -> theory -> theory + val inductive_cases: ((bstring * Args.src list) * string list) -> theory -> theory + val setup: (theory -> theory) list +end; + +structure IndCases: IND_CASES = +struct + + +(* theory data *) + +structure IndCasesArgs = +struct + val name = "ZF/ind_cases"; + type T = (simpset -> cterm -> thm) Symtab.table; + + val empty = Symtab.empty; + val copy = I; + val finish = I; + val prep_ext = I; + fun merge (tab1, tab2) = Symtab.merge (K true) (tab1, tab2); + fun print _ _ = (); +end; + +structure IndCasesData = TheoryDataFun(IndCasesArgs); + +fun declare name f = IndCasesData.map (fn tab => Symtab.update ((name, f), tab)); + +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 ((name, srcs), props) thy = + let + val read_prop = ProofContext.read_prop (ProofContext.init thy); + val ths = map (smart_cases thy (Simplifier.simpset_of thy) read_prop) props; + val atts = map (Attrib.global_attribute thy) srcs; + in + thy |> IsarThy.have_theorems_i Drule.lemmaK + [(((name, atts), map Thm.no_attributes ths), Comment.none)] + end; + + +(* ind_cases method *) + +fun mk_cases_meth (ctxt, props) = + props + |> map (smart_cases (ProofContext.theory_of ctxt) (Simplifier.get_local_simpset 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 = OuterSyntax.Keyword in + +val ind_cases = + P.opt_thm_name ":" -- Scan.repeat1 P.prop --| P.marg_comment + >> (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;