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