src/Pure/Isar/induct_attrib.ML
author wenzelm
Wed Oct 03 21:01:53 2001 +0200 (2001-10-03)
changeset 11658 4200394242c5
parent 11656 e499dceca569
child 11665 7324f018ea15
permissions -rw-r--r--
Isar/induct_attrib.ML;
wenzelm@11658
     1
(*  Title:      Pure/Isar/induct_attrib.ML
wenzelm@11656
     2
    ID:         $Id$
wenzelm@11656
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@11656
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@11656
     5
wenzelm@11656
     6
Declaration of rules for cases and induction.
wenzelm@11656
     7
*)
wenzelm@11656
     8
wenzelm@11656
     9
signature INDUCT_ATTRIB =
wenzelm@11656
    10
sig
wenzelm@11656
    11
  val dest_global_rules: theory ->
wenzelm@11656
    12
    {type_cases: (string * thm) list, set_cases: (string * thm) list,
wenzelm@11656
    13
      type_induct: (string * thm) list, set_induct: (string * thm) list}
wenzelm@11656
    14
  val print_global_rules: theory -> unit
wenzelm@11656
    15
  val dest_local_rules: Proof.context ->
wenzelm@11656
    16
    {type_cases: (string * thm) list, set_cases: (string * thm) list,
wenzelm@11656
    17
      type_induct: (string * thm) list, set_induct: (string * thm) list}
wenzelm@11656
    18
  val print_local_rules: Proof.context -> unit
wenzelm@11656
    19
  val get_cases : Proof.context -> (string * thm) NetRules.T * (string * thm) NetRules.T
wenzelm@11656
    20
  val get_induct : Proof.context -> (string * thm) NetRules.T * (string * thm) NetRules.T
wenzelm@11656
    21
  val lookup_casesS : Proof.context -> string -> thm option
wenzelm@11656
    22
  val lookup_casesT : Proof.context -> string -> thm option
wenzelm@11656
    23
  val lookup_inductS : Proof.context -> string -> thm option
wenzelm@11656
    24
  val lookup_inductT : Proof.context -> string -> thm option
wenzelm@11656
    25
  val cases_type_global: string -> theory attribute
wenzelm@11656
    26
  val cases_set_global: string -> theory attribute
wenzelm@11656
    27
  val cases_type_local: string -> Proof.context attribute
wenzelm@11656
    28
  val cases_set_local: string -> Proof.context attribute
wenzelm@11656
    29
  val induct_type_global: string -> theory attribute
wenzelm@11656
    30
  val induct_set_global: string -> theory attribute
wenzelm@11656
    31
  val induct_type_local: string -> Proof.context attribute
wenzelm@11656
    32
  val induct_set_local: string -> Proof.context attribute
wenzelm@11656
    33
  val casesN: string
wenzelm@11656
    34
  val inductN: string
wenzelm@11656
    35
  val typeN: string
wenzelm@11656
    36
  val setN: string
wenzelm@11656
    37
  val setup: (theory -> theory) list
wenzelm@11656
    38
end;
wenzelm@11656
    39
wenzelm@11656
    40
structure InductAttrib: INDUCT_ATTRIB =
wenzelm@11656
    41
struct
wenzelm@11656
    42
wenzelm@11656
    43
wenzelm@11656
    44
(** global and local induct data **)
wenzelm@11656
    45
wenzelm@11656
    46
(* rules *)
wenzelm@11656
    47
wenzelm@11656
    48
type rules = (string * thm) NetRules.T;
wenzelm@11656
    49
wenzelm@11656
    50
fun eq_rule ((s1:string, th1), (s2, th2)) = s1 = s2 andalso Thm.eq_thm (th1, th2);
wenzelm@11656
    51
wenzelm@11656
    52
val type_rules = NetRules.init eq_rule (Thm.concl_of o #2);
wenzelm@11656
    53
val set_rules = NetRules.init eq_rule (Thm.major_prem_of o #2);
wenzelm@11656
    54
wenzelm@11656
    55
fun lookup_rule (rs:rules) name = Library.assoc (NetRules.rules rs, name);
wenzelm@11656
    56
wenzelm@11656
    57
fun print_rules kind sg rs =
wenzelm@11656
    58
  let val thms = map snd (NetRules.rules rs)
wenzelm@11656
    59
  in Pretty.writeln (Pretty.big_list kind (map (Display.pretty_thm_sg sg) thms)) end;
wenzelm@11656
    60
wenzelm@11656
    61
wenzelm@11658
    62
(* theory data kind 'Isar/induction' *)
wenzelm@11656
    63
wenzelm@11656
    64
structure GlobalInductArgs =
wenzelm@11656
    65
struct
wenzelm@11658
    66
  val name = "Isar/induction";
wenzelm@11656
    67
  type T = (rules * rules) * (rules * rules);
wenzelm@11656
    68
wenzelm@11656
    69
  val empty = ((type_rules, set_rules), (type_rules, set_rules));
wenzelm@11656
    70
  val copy = I;
wenzelm@11656
    71
  val prep_ext = I;
wenzelm@11656
    72
  fun merge (((casesT1, casesS1), (inductT1, inductS1)),
wenzelm@11656
    73
      ((casesT2, casesS2), (inductT2, inductS2))) =
wenzelm@11656
    74
    ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
wenzelm@11656
    75
      (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)));
wenzelm@11656
    76
wenzelm@11656
    77
  fun print sg ((casesT, casesS), (inductT, inductS)) =
wenzelm@11656
    78
    (print_rules "type cases:" sg casesT;
wenzelm@11656
    79
      print_rules "set cases:" sg casesS;
wenzelm@11656
    80
      print_rules "type induct:" sg inductT;
wenzelm@11656
    81
      print_rules "set induct:" sg inductS);
wenzelm@11656
    82
wenzelm@11656
    83
  fun dest ((casesT, casesS), (inductT, inductS)) =
wenzelm@11656
    84
    {type_cases = NetRules.rules casesT,
wenzelm@11656
    85
     set_cases = NetRules.rules casesS,
wenzelm@11656
    86
     type_induct = NetRules.rules inductT,
wenzelm@11656
    87
     set_induct = NetRules.rules inductS};
wenzelm@11656
    88
end;
wenzelm@11656
    89
wenzelm@11656
    90
structure GlobalInduct = TheoryDataFun(GlobalInductArgs);
wenzelm@11656
    91
val print_global_rules = GlobalInduct.print;
wenzelm@11656
    92
val dest_global_rules = GlobalInductArgs.dest o GlobalInduct.get;
wenzelm@11656
    93
wenzelm@11656
    94
wenzelm@11658
    95
(* proof data kind 'Isar/induction' *)
wenzelm@11656
    96
wenzelm@11656
    97
structure LocalInductArgs =
wenzelm@11656
    98
struct
wenzelm@11658
    99
  val name = "Isar/induction";
wenzelm@11656
   100
  type T = GlobalInductArgs.T;
wenzelm@11656
   101
wenzelm@11656
   102
  fun init thy = GlobalInduct.get thy;
wenzelm@11656
   103
  fun print x = GlobalInductArgs.print (ProofContext.sign_of x);
wenzelm@11656
   104
end;
wenzelm@11656
   105
wenzelm@11656
   106
structure LocalInduct = ProofDataFun(LocalInductArgs);
wenzelm@11656
   107
val print_local_rules = LocalInduct.print;
wenzelm@11656
   108
val dest_local_rules = GlobalInductArgs.dest o LocalInduct.get;
wenzelm@11656
   109
wenzelm@11656
   110
wenzelm@11656
   111
(* access rules *)
wenzelm@11656
   112
wenzelm@11656
   113
val get_cases = #1 o LocalInduct.get;
wenzelm@11656
   114
val get_induct = #2 o LocalInduct.get;
wenzelm@11656
   115
wenzelm@11656
   116
val lookup_casesT = lookup_rule o #1 o get_cases;
wenzelm@11656
   117
val lookup_casesS = lookup_rule o #2 o get_cases;
wenzelm@11656
   118
val lookup_inductT = lookup_rule o #1 o get_induct;
wenzelm@11656
   119
val lookup_inductS = lookup_rule o #2 o get_induct;
wenzelm@11656
   120
wenzelm@11656
   121
wenzelm@11656
   122
wenzelm@11656
   123
(** attributes **)
wenzelm@11656
   124
wenzelm@11656
   125
local
wenzelm@11656
   126
wenzelm@11656
   127
fun mk_att f g h name arg =
wenzelm@11656
   128
  let val (x, thm) = h arg in (f (g (name, thm)) x, thm) end;
wenzelm@11656
   129
wenzelm@11656
   130
fun add_casesT rule x = apfst (apfst (NetRules.insert rule)) x;
wenzelm@11656
   131
fun add_casesS rule x = apfst (apsnd (NetRules.insert rule)) x;
wenzelm@11656
   132
fun add_inductT rule x = apsnd (apfst (NetRules.insert rule)) x;
wenzelm@11656
   133
fun add_inductS rule x = apsnd (apsnd (NetRules.insert rule)) x;
wenzelm@11656
   134
wenzelm@11656
   135
fun consumes0 x = RuleCases.consumes_default 0 x;
wenzelm@11656
   136
fun consumes1 x = RuleCases.consumes_default 1 x;
wenzelm@11656
   137
wenzelm@11656
   138
in
wenzelm@11656
   139
wenzelm@11656
   140
val cases_type_global = mk_att GlobalInduct.map add_casesT consumes0;
wenzelm@11656
   141
val cases_set_global = mk_att GlobalInduct.map add_casesS consumes1;
wenzelm@11656
   142
val induct_type_global = mk_att GlobalInduct.map add_inductT consumes0;
wenzelm@11656
   143
val induct_set_global = mk_att GlobalInduct.map add_inductS consumes1;
wenzelm@11656
   144
wenzelm@11656
   145
val cases_type_local = mk_att LocalInduct.map add_casesT consumes0;
wenzelm@11656
   146
val cases_set_local = mk_att LocalInduct.map add_casesS consumes1;
wenzelm@11656
   147
val induct_type_local = mk_att LocalInduct.map add_inductT consumes0;
wenzelm@11656
   148
val induct_set_local = mk_att LocalInduct.map add_inductS consumes1;
wenzelm@11656
   149
wenzelm@11656
   150
end;
wenzelm@11656
   151
wenzelm@11656
   152
wenzelm@11656
   153
(** concrete syntax **)
wenzelm@11656
   154
wenzelm@11656
   155
val casesN = "cases";
wenzelm@11656
   156
val inductN = "induct";
wenzelm@11656
   157
wenzelm@11656
   158
val typeN = "type";
wenzelm@11656
   159
val setN = "set";
wenzelm@11656
   160
wenzelm@11656
   161
local
wenzelm@11656
   162
wenzelm@11656
   163
fun spec k = (Args.$$$ k -- Args.colon) |-- Args.!!! Args.name;
wenzelm@11656
   164
wenzelm@11656
   165
fun attrib sign_of add_type add_set = Scan.depend (fn x =>
wenzelm@11656
   166
  let val sg = sign_of x in
wenzelm@11656
   167
    spec typeN >> (add_type o Sign.certify_tycon sg o Sign.intern_tycon sg) ||
wenzelm@11656
   168
    spec setN  >> (add_set o Sign.certify_const sg o Sign.intern_const sg)
wenzelm@11656
   169
  end >> pair x);
wenzelm@11656
   170
wenzelm@11656
   171
in
wenzelm@11656
   172
wenzelm@11656
   173
val cases_attr =
wenzelm@11656
   174
  (Attrib.syntax (attrib Theory.sign_of cases_type_global cases_set_global),
wenzelm@11656
   175
   Attrib.syntax (attrib ProofContext.sign_of cases_type_local cases_set_local));
wenzelm@11656
   176
wenzelm@11656
   177
val induct_attr =
wenzelm@11656
   178
  (Attrib.syntax (attrib Theory.sign_of induct_type_global induct_set_global),
wenzelm@11656
   179
   Attrib.syntax (attrib ProofContext.sign_of induct_type_local induct_set_local));
wenzelm@11656
   180
wenzelm@11656
   181
end;
wenzelm@11656
   182
wenzelm@11656
   183
wenzelm@11656
   184
wenzelm@11656
   185
(** theory setup **)
wenzelm@11656
   186
wenzelm@11656
   187
val setup =
wenzelm@11656
   188
  [GlobalInduct.init, LocalInduct.init,
wenzelm@11656
   189
   Attrib.add_attributes
wenzelm@11656
   190
    [(casesN, cases_attr, "declaration of cases rule for type or set"),
wenzelm@11656
   191
     (inductN, induct_attr, "declaration of induction rule for type or set")]];
wenzelm@11656
   192
wenzelm@11656
   193
end;