src/Pure/Isar/induct_attrib.ML
author wenzelm
Tue Dec 05 22:14:42 2006 +0100 (2006-12-05)
changeset 21658 5e31241e1e3c
parent 21506 b2a673894ce5
child 22360 26ead7ed4f4b
permissions -rw-r--r--
Attrib.internal: morphism;
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@21506
    11
  val dest_rules: Proof.context ->
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@21506
    15
  val print_rules: Proof.context -> unit
wenzelm@11730
    16
  val lookup_casesT : Proof.context -> string -> thm option
wenzelm@11656
    17
  val lookup_casesS : Proof.context -> string -> thm option
wenzelm@11730
    18
  val lookup_inductT : Proof.context -> string -> thm option
wenzelm@11656
    19
  val lookup_inductS : Proof.context -> string -> thm option
wenzelm@18210
    20
  val lookup_coinductT : Proof.context -> string -> thm option
wenzelm@18210
    21
  val lookup_coinductS : Proof.context -> string -> thm option
wenzelm@11730
    22
  val find_casesT: Proof.context -> typ -> thm list
wenzelm@18226
    23
  val find_casesS: Proof.context -> term -> thm list
wenzelm@11730
    24
  val find_inductT: Proof.context -> typ -> thm list
wenzelm@18226
    25
  val find_inductS: Proof.context -> term -> thm list
wenzelm@18210
    26
  val find_coinductT: Proof.context -> typ -> thm list
wenzelm@18226
    27
  val find_coinductS: Proof.context -> term -> thm list
wenzelm@18728
    28
  val cases_type: string -> attribute
wenzelm@18728
    29
  val cases_set: string -> attribute
wenzelm@18728
    30
  val induct_type: string -> attribute
wenzelm@18728
    31
  val induct_set: string -> attribute
wenzelm@18728
    32
  val coinduct_type: string -> attribute
wenzelm@18728
    33
  val coinduct_set: string -> attribute
wenzelm@11656
    34
  val casesN: string
wenzelm@11656
    35
  val inductN: string
wenzelm@18210
    36
  val coinductN: string
wenzelm@11656
    37
  val typeN: string
wenzelm@11656
    38
  val setN: string
wenzelm@11656
    39
end;
wenzelm@11656
    40
wenzelm@11656
    41
structure InductAttrib: INDUCT_ATTRIB =
wenzelm@11656
    42
struct
wenzelm@11656
    43
wenzelm@11656
    44
wenzelm@11730
    45
(** misc utils **)
wenzelm@11730
    46
wenzelm@11730
    47
(* encode_type -- for indexing purposes *)
wenzelm@11730
    48
wenzelm@11730
    49
fun encode_type (Type (c, Ts)) = Term.list_comb (Const (c, dummyT), map encode_type Ts)
wenzelm@11730
    50
  | encode_type (TFree (a, _)) = Free (a, dummyT)
wenzelm@11730
    51
  | encode_type (TVar (a, _)) = Var (a, dummyT);
wenzelm@11730
    52
wenzelm@11730
    53
wenzelm@11730
    54
(* variables -- ordered left-to-right, preferring right *)
wenzelm@11730
    55
wenzelm@18210
    56
fun vars_of tm =
wenzelm@19046
    57
  rev (distinct (op =) (Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm []));
wenzelm@11730
    58
wenzelm@18210
    59
local
wenzelm@11730
    60
wenzelm@11730
    61
val mk_var = encode_type o #2 o Term.dest_Var;
wenzelm@11730
    62
wenzelm@18210
    63
fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle Empty =>
wenzelm@18210
    64
  raise THM ("No variables in conclusion of rule", 0, [thm]);
wenzelm@18210
    65
wenzelm@11730
    66
in
wenzelm@11730
    67
wenzelm@18210
    68
fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle Empty =>
wenzelm@18210
    69
  raise THM ("No variables in major premise of rule", 0, [thm]);
wenzelm@11730
    70
wenzelm@18210
    71
val left_var_concl = concl_var hd;
wenzelm@18210
    72
val right_var_concl = concl_var List.last;
wenzelm@11730
    73
wenzelm@11730
    74
end;
wenzelm@11730
    75
wenzelm@11730
    76
wenzelm@11730
    77
wenzelm@18637
    78
(** induct data **)
wenzelm@11656
    79
wenzelm@11656
    80
(* rules *)
wenzelm@11656
    81
wenzelm@11656
    82
type rules = (string * thm) NetRules.T;
wenzelm@11656
    83
wenzelm@12381
    84
val init_rules =
wenzelm@13105
    85
  NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso
wenzelm@13105
    86
    Drule.eq_thm_prop (th1, th2));
wenzelm@11656
    87
wenzelm@17184
    88
fun lookup_rule (rs: rules) = AList.lookup (op =) (NetRules.rules rs);
wenzelm@11656
    89
wenzelm@18637
    90
fun pretty_rules ctxt kind rs =
wenzelm@11656
    91
  let val thms = map snd (NetRules.rules rs)
wenzelm@18637
    92
  in Pretty.big_list kind (map (ProofContext.pretty_thm ctxt) thms) end;
wenzelm@11656
    93
wenzelm@11656
    94
wenzelm@18637
    95
(* context data *)
wenzelm@11656
    96
wenzelm@18637
    97
fun dest ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) =
wenzelm@18637
    98
  {type_cases = NetRules.rules casesT,
wenzelm@18637
    99
   set_cases = NetRules.rules casesS,
wenzelm@18637
   100
   type_induct = NetRules.rules inductT,
wenzelm@18637
   101
   set_induct = NetRules.rules inductS,
wenzelm@18637
   102
   type_coinduct = NetRules.rules coinductT,
wenzelm@18637
   103
   set_coinduct = NetRules.rules coinductS};
wenzelm@18637
   104
wenzelm@18637
   105
structure Induct = GenericDataFun
wenzelm@18637
   106
(
wenzelm@18210
   107
  val name = "Isar/induct";
wenzelm@18210
   108
  type T = (rules * rules) * (rules * rules) * (rules * rules);
wenzelm@11656
   109
wenzelm@11730
   110
  val empty =
wenzelm@18210
   111
    ((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)),
wenzelm@18210
   112
     (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
wenzelm@18210
   113
     (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)));
wenzelm@18637
   114
wenzelm@16424
   115
  val extend = I;
wenzelm@18637
   116
wenzelm@18210
   117
  fun merge _ (((casesT1, casesS1), (inductT1, inductS1), (coinductT1, coinductS1)),
wenzelm@18210
   118
      ((casesT2, casesS2), (inductT2, inductS2), (coinductT2, coinductS2))) =
wenzelm@11656
   119
    ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
wenzelm@18210
   120
      (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)),
wenzelm@18210
   121
      (NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductS1, coinductS2)));
wenzelm@11656
   122
wenzelm@18637
   123
  fun print generic ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) =
wenzelm@18637
   124
    let val ctxt = Context.proof_of generic in
wenzelm@18637
   125
     [pretty_rules ctxt "coinduct type:" coinductT,
wenzelm@18637
   126
      pretty_rules ctxt "coinduct set:" coinductS,
wenzelm@18637
   127
      pretty_rules ctxt "induct type:" inductT,
wenzelm@18637
   128
      pretty_rules ctxt "induct set:" inductS,
wenzelm@18637
   129
      pretty_rules ctxt "cases type:" casesT,
wenzelm@18637
   130
      pretty_rules ctxt "cases set:" casesS]
wenzelm@18637
   131
     |> Pretty.chunks |> Pretty.writeln
wenzelm@18637
   132
    end
wenzelm@18637
   133
);
wenzelm@11656
   134
wenzelm@18708
   135
val _ = Context.add_setup Induct.init;
wenzelm@21506
   136
val print_rules = Induct.print o Context.Proof;
wenzelm@21506
   137
val dest_rules = dest o Induct.get o Context.Proof;
wenzelm@11656
   138
wenzelm@18637
   139
val get_local = Induct.get o Context.Proof;
wenzelm@11656
   140
wenzelm@11656
   141
wenzelm@11656
   142
(* access rules *)
wenzelm@11656
   143
wenzelm@18637
   144
val lookup_casesT = lookup_rule o #1 o #1 o get_local;
wenzelm@18637
   145
val lookup_casesS = lookup_rule o #2 o #1 o get_local;
wenzelm@18637
   146
val lookup_inductT = lookup_rule o #1 o #2 o get_local;
wenzelm@18637
   147
val lookup_inductS = lookup_rule o #2 o #2 o get_local;
wenzelm@18637
   148
val lookup_coinductT = lookup_rule o #1 o #3 o get_local;
wenzelm@18637
   149
val lookup_coinductS = lookup_rule o #2 o #3 o get_local;
wenzelm@11730
   150
wenzelm@11656
   151
wenzelm@11730
   152
fun find_rules which how ctxt x =
wenzelm@18637
   153
  map snd (NetRules.retrieve (which (get_local ctxt)) (how x));
wenzelm@11730
   154
wenzelm@11730
   155
val find_casesT = find_rules (#1 o #1) encode_type;
wenzelm@18226
   156
val find_casesS = find_rules (#2 o #1) I;
wenzelm@11730
   157
val find_inductT = find_rules (#1 o #2) encode_type;
wenzelm@18226
   158
val find_inductS = find_rules (#2 o #2) I;
wenzelm@18210
   159
val find_coinductT = find_rules (#1 o #3) encode_type;
wenzelm@18226
   160
val find_coinductS = find_rules (#2 o #3) I;
wenzelm@11656
   161
wenzelm@11656
   162
wenzelm@11656
   163
wenzelm@11656
   164
(** attributes **)
wenzelm@11656
   165
wenzelm@11656
   166
local
wenzelm@11656
   167
wenzelm@18637
   168
fun mk_att f g name arg =
wenzelm@18637
   169
  let val (x, thm) = g arg in (Induct.map (f (name, thm)) x, thm) end;
wenzelm@11656
   170
wenzelm@18210
   171
fun map1 f (x, y, z) = (f x, y, z);
wenzelm@18210
   172
fun map2 f (x, y, z) = (x, f y, z);
wenzelm@18210
   173
fun map3 f (x, y, z) = (x, y, f z);
wenzelm@18210
   174
wenzelm@18210
   175
fun add_casesT rule x = map1 (apfst (NetRules.insert rule)) x;
wenzelm@18210
   176
fun add_casesS rule x = map1 (apsnd (NetRules.insert rule)) x;
wenzelm@18210
   177
fun add_inductT rule x = map2 (apfst (NetRules.insert rule)) x;
wenzelm@18210
   178
fun add_inductS rule x = map2 (apsnd (NetRules.insert rule)) x;
wenzelm@18210
   179
fun add_coinductT rule x = map3 (apfst (NetRules.insert rule)) x;
wenzelm@18210
   180
fun add_coinductS rule x = map3 (apsnd (NetRules.insert rule)) x;
wenzelm@11656
   181
wenzelm@11656
   182
fun consumes0 x = RuleCases.consumes_default 0 x;
wenzelm@11656
   183
fun consumes1 x = RuleCases.consumes_default 1 x;
wenzelm@11656
   184
wenzelm@11656
   185
in
wenzelm@11656
   186
wenzelm@18637
   187
val cases_type = mk_att add_casesT consumes0;
wenzelm@18637
   188
val cases_set = mk_att add_casesS consumes1;
wenzelm@18637
   189
val induct_type = mk_att add_inductT consumes0;
wenzelm@18637
   190
val induct_set = mk_att add_inductS consumes1;
wenzelm@18637
   191
val coinduct_type = mk_att add_coinductT consumes0;
wenzelm@18637
   192
val coinduct_set = mk_att add_coinductS consumes1;
wenzelm@11656
   193
wenzelm@11656
   194
end;
wenzelm@11656
   195
wenzelm@11656
   196
wenzelm@18637
   197
wenzelm@11656
   198
(** concrete syntax **)
wenzelm@11656
   199
wenzelm@11656
   200
val casesN = "cases";
wenzelm@11656
   201
val inductN = "induct";
wenzelm@18210
   202
val coinductN = "coinduct";
wenzelm@11656
   203
wenzelm@11656
   204
val typeN = "type";
wenzelm@11656
   205
val setN = "set";
wenzelm@11656
   206
wenzelm@11656
   207
local
wenzelm@11656
   208
wenzelm@15703
   209
fun spec k arg =
wenzelm@15703
   210
  Scan.lift (Args.$$$ k -- Args.colon) |-- arg ||
wenzelm@15703
   211
  Scan.lift (Args.$$$ k) >> K "";
wenzelm@11656
   212
wenzelm@18637
   213
fun attrib add_type add_set =
wenzelm@18637
   214
  Attrib.syntax (spec typeN Args.tyname >> add_type || spec setN Args.const >> add_set);
wenzelm@11656
   215
wenzelm@11656
   216
in
wenzelm@11656
   217
wenzelm@18637
   218
val cases_att = attrib cases_type cases_set;
wenzelm@18637
   219
val induct_att = attrib induct_type induct_set;
wenzelm@18637
   220
val coinduct_att = attrib coinduct_type coinduct_set;
wenzelm@18210
   221
wenzelm@11656
   222
end;
wenzelm@11656
   223
wenzelm@15801
   224
val _ = Context.add_setup
wenzelm@18708
   225
 (Attrib.add_attributes
wenzelm@18728
   226
  [(casesN, cases_att, "declaration of cases rule for type or set"),
wenzelm@18728
   227
   (inductN, induct_att, "declaration of induction rule for type or set"),
wenzelm@18728
   228
   (coinductN, coinduct_att, "declaration of coinduction rule for type or set")]);
wenzelm@11656
   229
wenzelm@11656
   230
end;