src/Pure/Isar/induct_attrib.ML
author wenzelm
Sat Nov 19 14:21:07 2005 +0100 (2005-11-19)
changeset 18210 ad4b8567f6eb
parent 17184 3d80209e9a53
child 18226 8fde30f5cca6
permissions -rw-r--r--
added coinduct attribute;
tuned;
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
wenzelm@11656
     5
Declaration of rules for cases and induction.
wenzelm@11656
     6
*)
wenzelm@11656
     7
wenzelm@11656
     8
signature INDUCT_ATTRIB =
wenzelm@11656
     9
sig
wenzelm@11730
    10
  val vars_of: term -> term list
wenzelm@11656
    11
  val dest_global_rules: theory ->
wenzelm@11656
    12
    {type_cases: (string * thm) list, set_cases: (string * thm) list,
wenzelm@18210
    13
      type_induct: (string * thm) list, set_induct: (string * thm) list,
wenzelm@18210
    14
      type_coinduct: (string * thm) list, set_coinduct: (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@18210
    18
      type_induct: (string * thm) list, set_induct: (string * thm) list,
wenzelm@18210
    19
      type_coinduct: (string * thm) list, set_coinduct: (string * thm) list}
wenzelm@11656
    20
  val print_local_rules: Proof.context -> unit
wenzelm@11730
    21
  val lookup_casesT : Proof.context -> string -> thm option
wenzelm@11656
    22
  val lookup_casesS : Proof.context -> string -> thm option
wenzelm@11730
    23
  val lookup_inductT : Proof.context -> string -> thm option
wenzelm@11656
    24
  val lookup_inductS : Proof.context -> string -> thm option
wenzelm@18210
    25
  val lookup_coinductT : Proof.context -> string -> thm option
wenzelm@18210
    26
  val lookup_coinductS : Proof.context -> string -> thm option
wenzelm@11730
    27
  val find_casesT: Proof.context -> typ -> thm list
wenzelm@11730
    28
  val find_casesS: Proof.context -> thm -> thm list
wenzelm@11730
    29
  val find_inductT: Proof.context -> typ -> thm list
wenzelm@11730
    30
  val find_inductS: Proof.context -> thm -> thm list
wenzelm@18210
    31
  val find_coinductT: Proof.context -> typ -> thm list
wenzelm@18210
    32
  val find_coinductS: Proof.context -> thm -> thm list
wenzelm@11656
    33
  val cases_type_global: string -> theory attribute
wenzelm@11656
    34
  val cases_set_global: string -> theory attribute
wenzelm@11656
    35
  val cases_type_local: string -> Proof.context attribute
wenzelm@11656
    36
  val cases_set_local: string -> Proof.context attribute
wenzelm@11656
    37
  val induct_type_global: string -> theory attribute
wenzelm@11656
    38
  val induct_set_global: string -> theory attribute
wenzelm@11656
    39
  val induct_type_local: string -> Proof.context attribute
wenzelm@11656
    40
  val induct_set_local: string -> Proof.context attribute
wenzelm@18210
    41
  val coinduct_type_global: string -> theory attribute
wenzelm@18210
    42
  val coinduct_set_global: string -> theory attribute
wenzelm@18210
    43
  val coinduct_type_local: string -> Proof.context attribute
wenzelm@18210
    44
  val coinduct_set_local: string -> Proof.context attribute
wenzelm@11656
    45
  val casesN: string
wenzelm@11656
    46
  val inductN: string
wenzelm@18210
    47
  val coinductN: string
wenzelm@11656
    48
  val typeN: string
wenzelm@11656
    49
  val setN: string
wenzelm@11656
    50
end;
wenzelm@11656
    51
wenzelm@11656
    52
structure InductAttrib: INDUCT_ATTRIB =
wenzelm@11656
    53
struct
wenzelm@11656
    54
wenzelm@11656
    55
wenzelm@11730
    56
(** misc utils **)
wenzelm@11730
    57
wenzelm@11730
    58
(* encode_type -- for indexing purposes *)
wenzelm@11730
    59
wenzelm@11730
    60
fun encode_type (Type (c, Ts)) = Term.list_comb (Const (c, dummyT), map encode_type Ts)
wenzelm@11730
    61
  | encode_type (TFree (a, _)) = Free (a, dummyT)
wenzelm@11730
    62
  | encode_type (TVar (a, _)) = Var (a, dummyT);
wenzelm@11730
    63
wenzelm@11730
    64
wenzelm@11730
    65
(* variables -- ordered left-to-right, preferring right *)
wenzelm@11730
    66
wenzelm@18210
    67
fun vars_of tm =
wenzelm@18210
    68
  Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm []
wenzelm@18210
    69
  |> Library.distinct
wenzelm@18210
    70
  |> rev;
wenzelm@11730
    71
wenzelm@18210
    72
local
wenzelm@11730
    73
wenzelm@11730
    74
val mk_var = encode_type o #2 o Term.dest_Var;
wenzelm@11730
    75
wenzelm@18210
    76
fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle Empty =>
wenzelm@18210
    77
  raise THM ("No variables in conclusion of rule", 0, [thm]);
wenzelm@18210
    78
wenzelm@11730
    79
in
wenzelm@11730
    80
wenzelm@18210
    81
fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle Empty =>
wenzelm@18210
    82
  raise THM ("No variables in major premise of rule", 0, [thm]);
wenzelm@11730
    83
wenzelm@18210
    84
val left_var_concl = concl_var hd;
wenzelm@18210
    85
val right_var_concl = concl_var List.last;
wenzelm@11730
    86
wenzelm@11730
    87
end;
wenzelm@11730
    88
wenzelm@11730
    89
wenzelm@11730
    90
wenzelm@11656
    91
(** global and local induct data **)
wenzelm@11656
    92
wenzelm@11656
    93
(* rules *)
wenzelm@11656
    94
wenzelm@11656
    95
type rules = (string * thm) NetRules.T;
wenzelm@11656
    96
wenzelm@12381
    97
val init_rules =
wenzelm@13105
    98
  NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso
wenzelm@13105
    99
    Drule.eq_thm_prop (th1, th2));
wenzelm@11656
   100
wenzelm@17184
   101
fun lookup_rule (rs: rules) = AList.lookup (op =) (NetRules.rules rs);
wenzelm@11656
   102
wenzelm@18210
   103
fun pretty_rules prt kind x rs =
wenzelm@11656
   104
  let val thms = map snd (NetRules.rules rs)
wenzelm@18210
   105
  in Pretty.big_list kind (map (prt x) thms) end;
wenzelm@12055
   106
wenzelm@18210
   107
fun print_all_rules prt x ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) =
wenzelm@18210
   108
 [pretty_rules prt "coinduct type:" x coinductT,
wenzelm@18210
   109
  pretty_rules prt "coinduct set:" x coinductS,
wenzelm@18210
   110
  pretty_rules prt "induct type:" x inductT,
wenzelm@18210
   111
  pretty_rules prt "induct set:" x inductS,
wenzelm@18210
   112
  pretty_rules prt "cases type:" x casesT,
wenzelm@18210
   113
  pretty_rules prt "cases set:" x casesS]
wenzelm@18210
   114
 |> Pretty.chunks |> Pretty.writeln;
wenzelm@11656
   115
wenzelm@11656
   116
wenzelm@18210
   117
(* theory data *)
wenzelm@11656
   118
wenzelm@11656
   119
structure GlobalInductArgs =
wenzelm@11656
   120
struct
wenzelm@18210
   121
  val name = "Isar/induct";
wenzelm@18210
   122
  type T = (rules * rules) * (rules * rules) * (rules * rules);
wenzelm@11656
   123
wenzelm@11730
   124
  val empty =
wenzelm@18210
   125
    ((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)),
wenzelm@18210
   126
     (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
wenzelm@18210
   127
     (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)));
wenzelm@11656
   128
  val copy = I;
wenzelm@16424
   129
  val extend = I;
wenzelm@18210
   130
  fun merge _ (((casesT1, casesS1), (inductT1, inductS1), (coinductT1, coinductS1)),
wenzelm@18210
   131
      ((casesT2, casesS2), (inductT2, inductS2), (coinductT2, coinductS2))) =
wenzelm@11656
   132
    ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
wenzelm@18210
   133
      (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)),
wenzelm@18210
   134
      (NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductS1, coinductS2)));
wenzelm@11656
   135
wenzelm@12102
   136
  fun print x = print_all_rules Display.pretty_thm_sg x;
wenzelm@11656
   137
wenzelm@18210
   138
  fun dest ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) =
wenzelm@11656
   139
    {type_cases = NetRules.rules casesT,
wenzelm@11656
   140
     set_cases = NetRules.rules casesS,
wenzelm@11656
   141
     type_induct = NetRules.rules inductT,
wenzelm@18210
   142
     set_induct = NetRules.rules inductS,
wenzelm@18210
   143
     type_coinduct = NetRules.rules coinductT,
wenzelm@18210
   144
     set_coinduct = NetRules.rules coinductS};
wenzelm@11656
   145
end;
wenzelm@11656
   146
wenzelm@11656
   147
structure GlobalInduct = TheoryDataFun(GlobalInductArgs);
wenzelm@15801
   148
val _ = Context.add_setup [GlobalInduct.init];
wenzelm@11656
   149
val print_global_rules = GlobalInduct.print;
wenzelm@11656
   150
val dest_global_rules = GlobalInductArgs.dest o GlobalInduct.get;
wenzelm@11656
   151
wenzelm@11656
   152
wenzelm@18210
   153
(* proof data *)
wenzelm@11656
   154
wenzelm@16424
   155
structure LocalInduct = ProofDataFun
wenzelm@16424
   156
(struct
wenzelm@18210
   157
  val name = "Isar/induct";
wenzelm@11656
   158
  type T = GlobalInductArgs.T;
wenzelm@11656
   159
wenzelm@11656
   160
  fun init thy = GlobalInduct.get thy;
wenzelm@12102
   161
  fun print x = print_all_rules ProofContext.pretty_thm x;
wenzelm@16424
   162
end);
wenzelm@11656
   163
wenzelm@15801
   164
val _ = Context.add_setup [LocalInduct.init];
wenzelm@11656
   165
val print_local_rules = LocalInduct.print;
wenzelm@11656
   166
val dest_local_rules = GlobalInductArgs.dest o LocalInduct.get;
wenzelm@11656
   167
wenzelm@11656
   168
wenzelm@11656
   169
(* access rules *)
wenzelm@11656
   170
wenzelm@11730
   171
val lookup_casesT = lookup_rule o #1 o #1 o LocalInduct.get;
wenzelm@11730
   172
val lookup_casesS = lookup_rule o #2 o #1 o LocalInduct.get;
wenzelm@11730
   173
val lookup_inductT = lookup_rule o #1 o #2 o LocalInduct.get;
wenzelm@11730
   174
val lookup_inductS = lookup_rule o #2 o #2 o LocalInduct.get;
wenzelm@18210
   175
val lookup_coinductT = lookup_rule o #1 o #3 o LocalInduct.get;
wenzelm@18210
   176
val lookup_coinductS = lookup_rule o #2 o #3 o LocalInduct.get;
wenzelm@11730
   177
wenzelm@11656
   178
wenzelm@11730
   179
fun find_rules which how ctxt x =
wenzelm@11784
   180
  map snd (NetRules.retrieve (which (LocalInduct.get ctxt)) (how x));
wenzelm@11730
   181
wenzelm@11730
   182
val find_casesT = find_rules (#1 o #1) encode_type;
wenzelm@11730
   183
val find_casesS = find_rules (#2 o #1) Thm.concl_of;
wenzelm@11730
   184
val find_inductT = find_rules (#1 o #2) encode_type;
wenzelm@11730
   185
val find_inductS = find_rules (#2 o #2) Thm.concl_of;
wenzelm@18210
   186
val find_coinductT = find_rules (#1 o #3) encode_type;
wenzelm@18210
   187
val find_coinductS = find_rules (#2 o #3) Thm.concl_of;
wenzelm@11656
   188
wenzelm@11656
   189
wenzelm@11656
   190
wenzelm@11656
   191
(** attributes **)
wenzelm@11656
   192
wenzelm@11656
   193
local
wenzelm@11656
   194
wenzelm@11656
   195
fun mk_att f g h name arg =
wenzelm@11656
   196
  let val (x, thm) = h arg in (f (g (name, thm)) x, thm) end;
wenzelm@11656
   197
wenzelm@18210
   198
fun map1 f (x, y, z) = (f x, y, z);
wenzelm@18210
   199
fun map2 f (x, y, z) = (x, f y, z);
wenzelm@18210
   200
fun map3 f (x, y, z) = (x, y, f z);
wenzelm@18210
   201
wenzelm@18210
   202
fun add_casesT rule x = map1 (apfst (NetRules.insert rule)) x;
wenzelm@18210
   203
fun add_casesS rule x = map1 (apsnd (NetRules.insert rule)) x;
wenzelm@18210
   204
fun add_inductT rule x = map2 (apfst (NetRules.insert rule)) x;
wenzelm@18210
   205
fun add_inductS rule x = map2 (apsnd (NetRules.insert rule)) x;
wenzelm@18210
   206
fun add_coinductT rule x = map3 (apfst (NetRules.insert rule)) x;
wenzelm@18210
   207
fun add_coinductS rule x = map3 (apsnd (NetRules.insert rule)) x;
wenzelm@11656
   208
wenzelm@11656
   209
fun consumes0 x = RuleCases.consumes_default 0 x;
wenzelm@11656
   210
fun consumes1 x = RuleCases.consumes_default 1 x;
wenzelm@11656
   211
wenzelm@11656
   212
in
wenzelm@11656
   213
wenzelm@11656
   214
val cases_type_global = mk_att GlobalInduct.map add_casesT consumes0;
wenzelm@11656
   215
val cases_set_global = mk_att GlobalInduct.map add_casesS consumes1;
wenzelm@11656
   216
val induct_type_global = mk_att GlobalInduct.map add_inductT consumes0;
wenzelm@11656
   217
val induct_set_global = mk_att GlobalInduct.map add_inductS consumes1;
wenzelm@18210
   218
val coinduct_type_global = mk_att GlobalInduct.map add_coinductT consumes0;
wenzelm@18210
   219
val coinduct_set_global = mk_att GlobalInduct.map add_coinductS consumes1;
wenzelm@11656
   220
wenzelm@11656
   221
val cases_type_local = mk_att LocalInduct.map add_casesT consumes0;
wenzelm@11656
   222
val cases_set_local = mk_att LocalInduct.map add_casesS consumes1;
wenzelm@11656
   223
val induct_type_local = mk_att LocalInduct.map add_inductT consumes0;
wenzelm@11656
   224
val induct_set_local = mk_att LocalInduct.map add_inductS consumes1;
wenzelm@18210
   225
val coinduct_type_local = mk_att LocalInduct.map add_coinductT consumes0;
wenzelm@18210
   226
val coinduct_set_local = mk_att LocalInduct.map add_coinductS consumes1;
wenzelm@11656
   227
wenzelm@11656
   228
end;
wenzelm@11656
   229
wenzelm@11656
   230
wenzelm@11656
   231
(** concrete syntax **)
wenzelm@11656
   232
wenzelm@11656
   233
val casesN = "cases";
wenzelm@11656
   234
val inductN = "induct";
wenzelm@18210
   235
val coinductN = "coinduct";
wenzelm@11656
   236
wenzelm@11656
   237
val typeN = "type";
wenzelm@11656
   238
val setN = "set";
wenzelm@11656
   239
wenzelm@11656
   240
local
wenzelm@11656
   241
wenzelm@15703
   242
fun spec k arg =
wenzelm@15703
   243
  Scan.lift (Args.$$$ k -- Args.colon) |-- arg ||
wenzelm@15703
   244
  Scan.lift (Args.$$$ k) >> K "";
wenzelm@11656
   245
wenzelm@15703
   246
fun attrib tyname const add_type add_set =
wenzelm@15703
   247
  Attrib.syntax (spec typeN tyname >> add_type || spec setN const >> add_set);
wenzelm@11656
   248
wenzelm@11656
   249
in
wenzelm@11656
   250
wenzelm@11656
   251
val cases_attr =
wenzelm@15703
   252
 (attrib Args.global_tyname Args.global_const cases_type_global cases_set_global,
wenzelm@15703
   253
  attrib Args.local_tyname Args.local_const cases_type_local cases_set_local);
wenzelm@11656
   254
wenzelm@11656
   255
val induct_attr =
wenzelm@15703
   256
 (attrib Args.global_tyname Args.global_const induct_type_global induct_set_global,
wenzelm@15703
   257
  attrib Args.local_tyname Args.local_const induct_type_local induct_set_local);
wenzelm@11656
   258
wenzelm@18210
   259
val coinduct_attr =
wenzelm@18210
   260
 (attrib Args.global_tyname Args.global_const coinduct_type_global coinduct_set_global,
wenzelm@18210
   261
  attrib Args.local_tyname Args.local_const coinduct_type_local coinduct_set_local);
wenzelm@18210
   262
wenzelm@11656
   263
end;
wenzelm@11656
   264
wenzelm@15801
   265
val _ = Context.add_setup
wenzelm@15801
   266
 [Attrib.add_attributes
wenzelm@15801
   267
  [(casesN, cases_attr, "declaration of cases rule for type or set"),
wenzelm@18210
   268
   (inductN, induct_attr, "declaration of induction rule for type or set"),
wenzelm@18210
   269
   (coinductN, coinduct_attr, "declaration of coinduction rule for type or set")]];
wenzelm@11656
   270
wenzelm@11656
   271
end;