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