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