src/ZF/Tools/ind_cases.ML
author wenzelm
Thu Jan 19 21:22:08 2006 +0100 (2006-01-19 ago)
changeset 18708 4b3dadb4fe33
parent 18678 dd0c569fa43d
child 18728 6790126ab5f6
permissions -rw-r--r--
setup: theory -> theory;
     1 (*  Title:      ZF/Tools/ind_cases.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, LMU Muenchen
     4 
     5 Generic inductive cases facility for (co)inductive definitions.
     6 *)
     7 
     8 signature IND_CASES =
     9 sig
    10   val declare: string -> (simpset -> cterm -> thm) -> theory -> theory
    11   val inductive_cases: ((bstring * Attrib.src list) * string list) list -> theory -> theory
    12   val setup: theory -> theory
    13 end;
    14 
    15 structure IndCases: IND_CASES =
    16 struct
    17 
    18 
    19 (* theory data *)
    20 
    21 structure IndCasesData = TheoryDataFun
    22 (struct
    23   val name = "ZF/ind_cases";
    24   type T = (simpset -> cterm -> thm) Symtab.table;
    25 
    26   val empty = Symtab.empty;
    27   val copy = I;
    28   val extend = I;
    29   fun merge _ tabs : T = Symtab.merge (K true) tabs;
    30   fun print _ _ = ();
    31 end);
    32 
    33 
    34 fun declare name f = IndCasesData.map (Symtab.update (name, f));
    35 
    36 fun smart_cases thy ss read_prop s =
    37   let
    38     fun err msg = cat_error msg ("Malformed set membership statement: " ^ s);
    39     val A = read_prop s handle ERROR msg => err msg;
    40     val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (FOLogic.dest_Trueprop
    41       (Logic.strip_imp_concl A)))))) handle TERM _ => err "";
    42   in
    43     (case Symtab.lookup (IndCasesData.get thy) c of
    44       NONE => error ("Unknown inductive cases rule for set " ^ quote c)
    45     | SOME f => f ss (Thm.cterm_of (Theory.sign_of thy) A))
    46   end;
    47 
    48 
    49 (* inductive_cases command *)
    50 
    51 fun inductive_cases args thy =
    52   let
    53     val read_prop = ProofContext.read_prop (ProofContext.init thy);
    54     val mk_cases = smart_cases thy (Simplifier.simpset_of thy) read_prop;
    55     val facts = args |> map (fn ((name, srcs), props) =>
    56       ((name, map (Attrib.global_attribute thy) srcs),
    57         map (Thm.no_attributes o single o mk_cases) props));
    58   in thy |> IsarThy.theorems_i Drule.lemmaK facts |> snd end;
    59 
    60 
    61 (* ind_cases method *)
    62 
    63 fun mk_cases_meth (ctxt, props) =
    64   props
    65   |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt)
    66     (ProofContext.read_prop ctxt))
    67   |> Method.erule 0;
    68 
    69 val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name));
    70 
    71 
    72 (* package setup *)
    73 
    74 val setup =
    75  (IndCasesData.init #>
    76   Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
    77     "dynamic case analysis on sets")]);
    78 
    79 
    80 (* outer syntax *)
    81 
    82 local structure P = OuterParse and K = OuterKeyword in
    83 
    84 val ind_cases =
    85   P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop)
    86   >> (Toplevel.theory o inductive_cases);
    87 
    88 val inductive_casesP =
    89   OuterSyntax.command "inductive_cases"
    90     "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
    91 
    92 val _ = OuterSyntax.add_parsers [inductive_casesP];
    93 
    94 end;
    95 
    96 end;
    97