src/ZF/Tools/ind_cases.ML
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 12876 a70df1e5bf10
child 15032 02aed07e01bf
permissions -rw-r--r--
Merged in license change from Isabelle2004
     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 * Args.src list) * string list) list -> theory -> theory
    12   val setup: (theory -> theory) list
    13 end;
    14 
    15 structure IndCases: IND_CASES =
    16 struct
    17 
    18 
    19 (* theory data *)
    20 
    21 structure IndCasesArgs =
    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 prep_ext = I;
    29   fun merge (tab1, tab2) = Symtab.merge (K true) (tab1, tab2);
    30   fun print _ _ = ();
    31 end;
    32 
    33 structure IndCasesData = TheoryDataFun(IndCasesArgs);
    34 
    35 fun declare name f = IndCasesData.map (fn tab => Symtab.update ((name, f), tab));
    36 
    37 fun smart_cases thy ss read_prop s =
    38   let
    39     fun err () = error ("Malformed set membership statement: " ^ s);
    40     val A = read_prop s handle ERROR => err ();
    41     val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (FOLogic.dest_Trueprop
    42       (Logic.strip_imp_concl A)))))) handle TERM _ => err ();
    43   in
    44     (case Symtab.lookup (IndCasesData.get thy, c) of
    45       None => error ("Unknown inductive cases rule for set " ^ quote c)
    46     | Some f => f ss (Thm.cterm_of (Theory.sign_of thy) A))
    47   end;
    48 
    49 
    50 (* inductive_cases command *)
    51 
    52 fun inductive_cases args thy =
    53   let
    54     val read_prop = ProofContext.read_prop (ProofContext.init thy);
    55     val mk_cases = smart_cases thy (Simplifier.simpset_of thy) read_prop;
    56     val facts = args |> map (fn ((name, srcs), props) =>
    57       ((name, map (Attrib.global_attribute thy) srcs),
    58         map (Thm.no_attributes o single o mk_cases) props));
    59   in thy |> IsarThy.theorems_i Drule.lemmaK facts |> #1 end;
    60 
    61 
    62 (* ind_cases method *)
    63 
    64 fun mk_cases_meth (ctxt, props) =
    65   props
    66   |> map (smart_cases (ProofContext.theory_of ctxt) (Simplifier.get_local_simpset ctxt)
    67     (ProofContext.read_prop ctxt))
    68   |> Method.erule 0;
    69 
    70 val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name));
    71 
    72 
    73 (* package setup *)
    74 
    75 val setup =
    76  [IndCasesData.init,
    77   Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
    78     "dynamic case analysis on sets")]];
    79 
    80 
    81 (* outer syntax *)
    82 
    83 local structure P = OuterParse and K = OuterSyntax.Keyword in
    84 
    85 val ind_cases =
    86   P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop)
    87   >> (Toplevel.theory o inductive_cases);
    88 
    89 val inductive_casesP =
    90   OuterSyntax.command "inductive_cases"
    91     "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
    92 
    93 val _ = OuterSyntax.add_parsers [inductive_casesP];
    94 
    95 end;
    96 
    97 end;