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