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