src/Pure/Isar/induct_attrib.ML
author wenzelm
Wed Dec 05 03:15:32 2001 +0100 (2001-12-05)
changeset 12381 5177845a34f5
parent 12311 ce5f9e61c037
child 13105 3d1e7a199bdc
permissions -rw-r--r--
simplified NetRules;
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@11730
    11
  val vars_of: term -> term list
wenzelm@11656
    12
  val dest_global_rules: theory ->
wenzelm@11656
    13
    {type_cases: (string * thm) list, set_cases: (string * thm) list,
wenzelm@11656
    14
      type_induct: (string * thm) list, set_induct: (string * thm) list}
wenzelm@11656
    15
  val print_global_rules: theory -> unit
wenzelm@11656
    16
  val dest_local_rules: Proof.context ->
wenzelm@11656
    17
    {type_cases: (string * thm) list, set_cases: (string * thm) list,
wenzelm@11656
    18
      type_induct: (string * thm) list, set_induct: (string * thm) list}
wenzelm@11656
    19
  val print_local_rules: Proof.context -> unit
wenzelm@11730
    20
  val lookup_casesT : Proof.context -> string -> thm option
wenzelm@11656
    21
  val lookup_casesS : Proof.context -> string -> thm option
wenzelm@11730
    22
  val lookup_inductT : Proof.context -> string -> thm option
wenzelm@11656
    23
  val lookup_inductS : Proof.context -> string -> thm option
wenzelm@11730
    24
  val find_casesT: Proof.context -> typ -> thm list
wenzelm@11730
    25
  val find_casesS: Proof.context -> thm -> thm list
wenzelm@11730
    26
  val find_inductT: Proof.context -> typ -> thm list
wenzelm@11730
    27
  val find_inductS: Proof.context -> thm -> thm list
wenzelm@11656
    28
  val cases_type_global: string -> theory attribute
wenzelm@11656
    29
  val cases_set_global: string -> theory attribute
wenzelm@11656
    30
  val cases_type_local: string -> Proof.context attribute
wenzelm@11656
    31
  val cases_set_local: string -> Proof.context attribute
wenzelm@11656
    32
  val induct_type_global: string -> theory attribute
wenzelm@11656
    33
  val induct_set_global: string -> theory attribute
wenzelm@11656
    34
  val induct_type_local: string -> Proof.context attribute
wenzelm@11656
    35
  val induct_set_local: string -> Proof.context attribute
wenzelm@11656
    36
  val casesN: string
wenzelm@11656
    37
  val inductN: string
wenzelm@11656
    38
  val typeN: string
wenzelm@11656
    39
  val setN: string
wenzelm@11656
    40
  val setup: (theory -> theory) list
wenzelm@11656
    41
end;
wenzelm@11656
    42
wenzelm@11656
    43
structure InductAttrib: INDUCT_ATTRIB =
wenzelm@11656
    44
struct
wenzelm@11656
    45
wenzelm@11656
    46
wenzelm@11730
    47
(** misc utils **)
wenzelm@11730
    48
wenzelm@11730
    49
(* encode_type -- for indexing purposes *)
wenzelm@11730
    50
wenzelm@11730
    51
fun encode_type (Type (c, Ts)) = Term.list_comb (Const (c, dummyT), map encode_type Ts)
wenzelm@11730
    52
  | encode_type (TFree (a, _)) = Free (a, dummyT)
wenzelm@11730
    53
  | encode_type (TVar (a, _)) = Var (a, dummyT);
wenzelm@11730
    54
wenzelm@11730
    55
wenzelm@11730
    56
(* variables -- ordered left-to-right, preferring right *)
wenzelm@11730
    57
wenzelm@11730
    58
local
wenzelm@11730
    59
wenzelm@11730
    60
fun rev_vars_of tm =
wenzelm@11730
    61
  Term.foldl_aterms (fn (ts, t as Var _) => t :: ts | (ts, _) => ts) ([], tm)
wenzelm@11730
    62
  |> Library.distinct;
wenzelm@11730
    63
wenzelm@11730
    64
val mk_var = encode_type o #2 o Term.dest_Var;
wenzelm@11730
    65
wenzelm@11730
    66
in
wenzelm@11730
    67
wenzelm@11730
    68
val vars_of = rev o rev_vars_of;
wenzelm@11730
    69
wenzelm@11730
    70
fun first_var thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle LIST _ =>
wenzelm@11730
    71
  raise THM ("No variables in first premise of rule", 0, [thm]);
wenzelm@11730
    72
wenzelm@11730
    73
fun last_var thm = mk_var (hd (rev_vars_of (Thm.concl_of thm))) handle LIST _ =>
wenzelm@11730
    74
  raise THM ("No variables in conclusion of rule", 0, [thm]);
wenzelm@11730
    75
wenzelm@11730
    76
end;
wenzelm@11730
    77
wenzelm@11730
    78
wenzelm@11730
    79
wenzelm@11656
    80
(** global and local induct data **)
wenzelm@11656
    81
wenzelm@11656
    82
(* rules *)
wenzelm@11656
    83
wenzelm@11656
    84
type rules = (string * thm) NetRules.T;
wenzelm@11656
    85
wenzelm@12381
    86
val init_rules =
wenzelm@12381
    87
  NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso Thm.eq_thm (th1, th2));
wenzelm@11656
    88
wenzelm@11730
    89
fun lookup_rule (rs: rules) name = Library.assoc (NetRules.rules rs, name);
wenzelm@11656
    90
wenzelm@12055
    91
fun print_rules prt kind x rs =
wenzelm@11656
    92
  let val thms = map snd (NetRules.rules rs)
wenzelm@12055
    93
  in Pretty.writeln (Pretty.big_list kind (map (prt x) thms)) end;
wenzelm@12055
    94
wenzelm@12055
    95
fun print_all_rules prt x ((casesT, casesS), (inductT, inductS)) =
wenzelm@12055
    96
 (print_rules prt "induct type:" x inductT;
wenzelm@12055
    97
  print_rules prt "induct set:" x inductS;
wenzelm@12055
    98
  print_rules prt "cases type:" x casesT;
wenzelm@12055
    99
  print_rules prt "cases set:" x casesS);
wenzelm@11656
   100
wenzelm@11656
   101
wenzelm@11658
   102
(* theory data kind 'Isar/induction' *)
wenzelm@11656
   103
wenzelm@11656
   104
structure GlobalInductArgs =
wenzelm@11656
   105
struct
wenzelm@11658
   106
  val name = "Isar/induction";
wenzelm@11656
   107
  type T = (rules * rules) * (rules * rules);
wenzelm@11656
   108
wenzelm@11730
   109
  val empty =
wenzelm@11730
   110
    ((init_rules (first_var o #2), init_rules (Thm.major_prem_of o #2)),
wenzelm@11730
   111
     (init_rules (last_var o #2), init_rules (Thm.major_prem_of o #2)));
wenzelm@11656
   112
  val copy = I;
wenzelm@11656
   113
  val prep_ext = I;
wenzelm@11656
   114
  fun merge (((casesT1, casesS1), (inductT1, inductS1)),
wenzelm@11656
   115
      ((casesT2, casesS2), (inductT2, inductS2))) =
wenzelm@11656
   116
    ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
wenzelm@11656
   117
      (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)));
wenzelm@11656
   118
wenzelm@12102
   119
  fun print x = print_all_rules Display.pretty_thm_sg x;
wenzelm@11656
   120
wenzelm@11656
   121
  fun dest ((casesT, casesS), (inductT, inductS)) =
wenzelm@11656
   122
    {type_cases = NetRules.rules casesT,
wenzelm@11656
   123
     set_cases = NetRules.rules casesS,
wenzelm@11656
   124
     type_induct = NetRules.rules inductT,
wenzelm@11656
   125
     set_induct = NetRules.rules inductS};
wenzelm@11656
   126
end;
wenzelm@11656
   127
wenzelm@11656
   128
structure GlobalInduct = TheoryDataFun(GlobalInductArgs);
wenzelm@11656
   129
val print_global_rules = GlobalInduct.print;
wenzelm@11656
   130
val dest_global_rules = GlobalInductArgs.dest o GlobalInduct.get;
wenzelm@11656
   131
wenzelm@11656
   132
wenzelm@11658
   133
(* proof data kind 'Isar/induction' *)
wenzelm@11656
   134
wenzelm@11656
   135
structure LocalInductArgs =
wenzelm@11656
   136
struct
wenzelm@11658
   137
  val name = "Isar/induction";
wenzelm@11656
   138
  type T = GlobalInductArgs.T;
wenzelm@11656
   139
wenzelm@11656
   140
  fun init thy = GlobalInduct.get thy;
wenzelm@12102
   141
  fun print x = print_all_rules ProofContext.pretty_thm x;
wenzelm@11656
   142
end;
wenzelm@11656
   143
wenzelm@11656
   144
structure LocalInduct = ProofDataFun(LocalInductArgs);
wenzelm@11656
   145
val print_local_rules = LocalInduct.print;
wenzelm@11656
   146
val dest_local_rules = GlobalInductArgs.dest o LocalInduct.get;
wenzelm@11656
   147
wenzelm@11656
   148
wenzelm@11656
   149
(* access rules *)
wenzelm@11656
   150
wenzelm@11730
   151
val lookup_casesT = lookup_rule o #1 o #1 o LocalInduct.get;
wenzelm@11730
   152
val lookup_casesS = lookup_rule o #2 o #1 o LocalInduct.get;
wenzelm@11730
   153
val lookup_inductT = lookup_rule o #1 o #2 o LocalInduct.get;
wenzelm@11730
   154
val lookup_inductS = lookup_rule o #2 o #2 o LocalInduct.get;
wenzelm@11730
   155
wenzelm@11656
   156
wenzelm@11730
   157
fun find_rules which how ctxt x =
wenzelm@11784
   158
  map snd (NetRules.retrieve (which (LocalInduct.get ctxt)) (how x));
wenzelm@11730
   159
wenzelm@11730
   160
val find_casesT = find_rules (#1 o #1) encode_type;
wenzelm@11730
   161
val find_casesS = find_rules (#2 o #1) Thm.concl_of;
wenzelm@11730
   162
val find_inductT = find_rules (#1 o #2) encode_type;
wenzelm@11730
   163
val find_inductS = find_rules (#2 o #2) Thm.concl_of;
wenzelm@11656
   164
wenzelm@11656
   165
wenzelm@11656
   166
wenzelm@11656
   167
(** attributes **)
wenzelm@11656
   168
wenzelm@11656
   169
local
wenzelm@11656
   170
wenzelm@11656
   171
fun mk_att f g h name arg =
wenzelm@11656
   172
  let val (x, thm) = h arg in (f (g (name, thm)) x, thm) end;
wenzelm@11656
   173
wenzelm@11656
   174
fun add_casesT rule x = apfst (apfst (NetRules.insert rule)) x;
wenzelm@11656
   175
fun add_casesS rule x = apfst (apsnd (NetRules.insert rule)) x;
wenzelm@11656
   176
fun add_inductT rule x = apsnd (apfst (NetRules.insert rule)) x;
wenzelm@11656
   177
fun add_inductS rule x = apsnd (apsnd (NetRules.insert rule)) x;
wenzelm@11656
   178
wenzelm@11656
   179
fun consumes0 x = RuleCases.consumes_default 0 x;
wenzelm@11656
   180
fun consumes1 x = RuleCases.consumes_default 1 x;
wenzelm@11656
   181
wenzelm@11656
   182
in
wenzelm@11656
   183
wenzelm@11656
   184
val cases_type_global = mk_att GlobalInduct.map add_casesT consumes0;
wenzelm@11656
   185
val cases_set_global = mk_att GlobalInduct.map add_casesS consumes1;
wenzelm@11656
   186
val induct_type_global = mk_att GlobalInduct.map add_inductT consumes0;
wenzelm@11656
   187
val induct_set_global = mk_att GlobalInduct.map add_inductS consumes1;
wenzelm@11656
   188
wenzelm@11656
   189
val cases_type_local = mk_att LocalInduct.map add_casesT consumes0;
wenzelm@11656
   190
val cases_set_local = mk_att LocalInduct.map add_casesS consumes1;
wenzelm@11656
   191
val induct_type_local = mk_att LocalInduct.map add_inductT consumes0;
wenzelm@11656
   192
val induct_set_local = mk_att LocalInduct.map add_inductS consumes1;
wenzelm@11656
   193
wenzelm@11656
   194
end;
wenzelm@11656
   195
wenzelm@11656
   196
wenzelm@11656
   197
(** concrete syntax **)
wenzelm@11656
   198
wenzelm@11656
   199
val casesN = "cases";
wenzelm@11656
   200
val inductN = "induct";
wenzelm@11656
   201
wenzelm@11656
   202
val typeN = "type";
wenzelm@11656
   203
val setN = "set";
wenzelm@11656
   204
wenzelm@11656
   205
local
wenzelm@11656
   206
wenzelm@11791
   207
fun spec k cert =
wenzelm@11791
   208
  (Args.$$$ k -- Args.colon) |-- Args.!!! (Args.name >> cert) ||
wenzelm@11791
   209
  Args.$$$ k >> K "";
wenzelm@11656
   210
wenzelm@11656
   211
fun attrib sign_of add_type add_set = Scan.depend (fn x =>
wenzelm@11656
   212
  let val sg = sign_of x in
wenzelm@11791
   213
    spec typeN (Sign.certify_tyname sg o Sign.intern_tycon sg) >> add_type ||
wenzelm@11791
   214
    spec setN (Sign.certify_const sg o Sign.intern_const sg) >> add_set
wenzelm@11656
   215
  end >> pair x);
wenzelm@11656
   216
wenzelm@11656
   217
in
wenzelm@11656
   218
wenzelm@11656
   219
val cases_attr =
wenzelm@11656
   220
  (Attrib.syntax (attrib Theory.sign_of cases_type_global cases_set_global),
wenzelm@11656
   221
   Attrib.syntax (attrib ProofContext.sign_of cases_type_local cases_set_local));
wenzelm@11656
   222
wenzelm@11656
   223
val induct_attr =
wenzelm@11656
   224
  (Attrib.syntax (attrib Theory.sign_of induct_type_global induct_set_global),
wenzelm@11656
   225
   Attrib.syntax (attrib ProofContext.sign_of induct_type_local induct_set_local));
wenzelm@11656
   226
wenzelm@11656
   227
end;
wenzelm@11656
   228
wenzelm@11656
   229
wenzelm@11656
   230
wenzelm@11656
   231
(** theory setup **)
wenzelm@11656
   232
wenzelm@11656
   233
val setup =
wenzelm@11656
   234
  [GlobalInduct.init, LocalInduct.init,
wenzelm@11656
   235
   Attrib.add_attributes
wenzelm@11656
   236
    [(casesN, cases_attr, "declaration of cases rule for type or set"),
wenzelm@11656
   237
     (inductN, induct_attr, "declaration of induction rule for type or set")]];
wenzelm@11656
   238
wenzelm@11656
   239
end;