src/ZF/Tools/ind_cases.ML
author wenzelm
Fri, 19 Jan 2007 22:08:08 +0100
changeset 22101 6d13239d5f52
parent 21879 a3efbae45735
child 22846 fb79144af9a3
permissions -rw-r--r--
moved parts of OuterParse to SpecParse;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12174
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
     1
(*  Title:      ZF/Tools/ind_cases.ML
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, LMU Muenchen
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
     4
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
     5
Generic inductive cases facility for (co)inductive definitions.
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
     6
*)
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
     7
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
     8
signature IND_CASES =
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
     9
sig
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    10
  val declare: string -> (simpset -> cterm -> thm) -> theory -> theory
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15531
diff changeset
    11
  val inductive_cases: ((bstring * Attrib.src list) * string list) list -> theory -> theory
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18678
diff changeset
    12
  val setup: theory -> theory
12174
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    13
end;
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    14
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    15
structure IndCases: IND_CASES =
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    16
struct
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    17
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    18
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    19
(* theory data *)
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    20
16424
18a07ad8fea8 accomodate change of TheoryDataFun;
wenzelm
parents: 15705
diff changeset
    21
structure IndCasesData = TheoryDataFun
18a07ad8fea8 accomodate change of TheoryDataFun;
wenzelm
parents: 15705
diff changeset
    22
(struct
12174
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    23
  val name = "ZF/ind_cases";
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    24
  type T = (simpset -> cterm -> thm) Symtab.table;
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    25
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    26
  val empty = Symtab.empty;
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    27
  val copy = I;
16424
18a07ad8fea8 accomodate change of TheoryDataFun;
wenzelm
parents: 15705
diff changeset
    28
  val extend = I;
18a07ad8fea8 accomodate change of TheoryDataFun;
wenzelm
parents: 15705
diff changeset
    29
  fun merge _ tabs : T = Symtab.merge (K true) tabs;
12174
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    30
  fun print _ _ = ();
16424
18a07ad8fea8 accomodate change of TheoryDataFun;
wenzelm
parents: 15705
diff changeset
    31
end);
12174
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    32
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    33
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17224
diff changeset
    34
fun declare name f = IndCasesData.map (Symtab.update (name, f));
12174
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    35
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    36
fun smart_cases thy ss read_prop s =
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    37
  let
18678
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18418
diff changeset
    38
    fun err msg = cat_error msg ("Malformed set membership statement: " ^ s);
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18418
diff changeset
    39
    val A = read_prop s handle ERROR msg => err msg;
12174
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    40
    val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (FOLogic.dest_Trueprop
18678
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18418
diff changeset
    41
      (Logic.strip_imp_concl A)))))) handle TERM _ => err "";
12174
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    42
  in
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17224
diff changeset
    43
    (case Symtab.lookup (IndCasesData.get thy) c of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15032
diff changeset
    44
      NONE => error ("Unknown inductive cases rule for set " ^ quote c)
20342
wenzelm
parents: 18799
diff changeset
    45
    | SOME f => f ss (Thm.cterm_of thy A))
12174
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    46
  end;
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    47
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    48
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    49
(* inductive_cases command *)
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    50
12609
fb073a34b537 'inductive_cases': support 'and' form;
wenzelm
parents: 12311
diff changeset
    51
fun inductive_cases args thy =
12174
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    52
  let
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    53
    val read_prop = ProofContext.read_prop (ProofContext.init thy);
12609
fb073a34b537 'inductive_cases': support 'and' form;
wenzelm
parents: 12311
diff changeset
    54
    val mk_cases = smart_cases thy (Simplifier.simpset_of thy) read_prop;
fb073a34b537 'inductive_cases': support 'and' form;
wenzelm
parents: 12311
diff changeset
    55
    val facts = args |> map (fn ((name, srcs), props) =>
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    56
      ((name, map (Attrib.attribute thy) srcs),
12876
a70df1e5bf10 got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents: 12716
diff changeset
    57
        map (Thm.no_attributes o single o mk_cases) props));
20916
ee6e3597bb4d PureThy.note_thmss_i;
wenzelm
parents: 20342
diff changeset
    58
  in thy |> PureThy.note_thmss_i "" facts |> snd end;
12174
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    59
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    60
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    61
(* ind_cases method *)
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    62
21879
a3efbae45735 switched argument order in *.syntax lifters
haftmann
parents: 20916
diff changeset
    63
fun mk_cases_meth (props, ctxt) =
12174
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    64
  props
15032
02aed07e01bf local_cla/simpset_of;
wenzelm
parents: 14981
diff changeset
    65
  |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt)
12174
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    66
    (ProofContext.read_prop ctxt))
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    67
  |> Method.erule 0;
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    68
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    69
val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name));
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    70
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    71
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    72
(* package setup *)
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    73
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    74
val setup =
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18678
diff changeset
    75
 (IndCasesData.init #>
12174
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    76
  Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18678
diff changeset
    77
    "dynamic case analysis on sets")]);
12174
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    78
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    79
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    80
(* outer syntax *)
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    81
17057
0934ac31985f OuterKeyword;
wenzelm
parents: 16424
diff changeset
    82
local structure P = OuterParse and K = OuterKeyword in
12174
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    83
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    84
val ind_cases =
22101
6d13239d5f52 moved parts of OuterParse to SpecParse;
wenzelm
parents: 21879
diff changeset
    85
  P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop)
12174
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    86
  >> (Toplevel.theory o inductive_cases);
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    87
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    88
val inductive_casesP =
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    89
  OuterSyntax.command "inductive_cases"
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    90
    "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    91
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    92
val _ = OuterSyntax.add_parsers [inductive_casesP];
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    93
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    94
end;
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    95
a0aab0b9f2e9 Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff changeset
    96
end;
15705
b5edb9dcec9a *** MESSAGE REFERS TO PREVIOUS VERSION ***
wenzelm
parents: 15703
diff changeset
    97