src/ZF/Tools/ind_cases.ML
author wenzelm
Fri Apr 27 22:47:30 2012 +0200 (2012-04-27 ago)
changeset 47815 43f677b3ae91
parent 46961 5c6955f487e5
child 54742 7a86358a3c0b
permissions -rw-r--r--
clarified signature;
     1 (*  Title:      ZF/Tools/ind_cases.ML
     2     Author:     Markus Wenzel, LMU Muenchen
     3 
     4 Generic inductive cases facility for (co)inductive definitions.
     5 *)
     6 
     7 signature IND_CASES =
     8 sig
     9   val declare: string -> (Proof.context -> conv) -> theory -> theory
    10   val inductive_cases: (Attrib.binding * string list) list -> theory -> theory
    11   val setup: theory -> theory
    12 end;
    13 
    14 structure IndCases: IND_CASES =
    15 struct
    16 
    17 
    18 (* theory data *)
    19 
    20 structure IndCasesData = Theory_Data
    21 (
    22   type T = (Proof.context -> conv) Symtab.table;
    23   val empty = Symtab.empty;
    24   val extend = I;
    25   fun merge data = Symtab.merge (K true) data;
    26 );
    27 
    28 
    29 fun declare name f = IndCasesData.map (Symtab.update (name, f));
    30 
    31 fun smart_cases ctxt s =
    32   let
    33     val thy = Proof_Context.theory_of ctxt;
    34     fun err msg = cat_error msg ("Malformed set membership statement: " ^ s);
    35     val A = Syntax.read_prop ctxt s handle ERROR msg => err msg;
    36     val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (FOLogic.dest_Trueprop
    37       (Logic.strip_imp_concl A)))))) handle TERM _ => err "";
    38   in
    39     (case Symtab.lookup (IndCasesData.get thy) c of
    40       NONE => error ("Unknown inductive cases rule for set " ^ quote c)
    41     | SOME f => f ctxt (Thm.cterm_of thy A))
    42   end;
    43 
    44 
    45 (* inductive_cases command *)
    46 
    47 fun inductive_cases args thy =
    48   let
    49     val ctxt = Proof_Context.init_global thy;
    50     val facts = args |> map (fn ((name, srcs), props) =>
    51       ((name, map (Attrib.attribute_cmd_global thy) srcs),
    52         map (Thm.no_attributes o single o smart_cases ctxt) props));
    53   in thy |> Global_Theory.note_thmss "" facts |> snd end;
    54 
    55 
    56 (* ind_cases method *)
    57 
    58 val setup =
    59   Method.setup @{binding "ind_cases"}
    60     (Scan.lift (Scan.repeat1 Args.name_source) >>
    61       (fn props => fn ctxt => Method.erule 0 (map (smart_cases ctxt) props)))
    62     "dynamic case analysis on sets";
    63 
    64 
    65 (* outer syntax *)
    66 
    67 val _ =
    68   Outer_Syntax.command @{command_spec "inductive_cases"}
    69     "create simplified instances of elimination rules (improper)"
    70     (Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Scan.repeat1 Parse.prop)
    71       >> (Toplevel.theory o inductive_cases));
    72 
    73 end;
    74