src/Pure/Isar/induct_attrib.ML
author wenzelm
Tue Oct 16 00:32:34 2001 +0200 (2001-10-16)
changeset 11791 2c201f3b018e
parent 11784 b66b198ee29a
child 12055 a9c44895cc8c
permissions -rw-r--r--
allow empty set/type name;
     1 (*  Title:      Pure/Isar/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 vars_of: term -> term list
    12   val dest_global_rules: theory ->
    13     {type_cases: (string * thm) list, set_cases: (string * thm) list,
    14       type_induct: (string * thm) list, set_induct: (string * thm) list}
    15   val print_global_rules: theory -> unit
    16   val dest_local_rules: Proof.context ->
    17     {type_cases: (string * thm) list, set_cases: (string * thm) list,
    18       type_induct: (string * thm) list, set_induct: (string * thm) list}
    19   val print_local_rules: Proof.context -> unit
    20   val lookup_casesT : Proof.context -> string -> thm option
    21   val lookup_casesS : Proof.context -> string -> thm option
    22   val lookup_inductT : Proof.context -> string -> thm option
    23   val lookup_inductS : Proof.context -> string -> thm option
    24   val find_casesT: Proof.context -> typ -> thm list
    25   val find_casesS: Proof.context -> thm -> thm list
    26   val find_inductT: Proof.context -> typ -> thm list
    27   val find_inductS: Proof.context -> thm -> thm list
    28   val cases_type_global: string -> theory attribute
    29   val cases_set_global: string -> theory attribute
    30   val cases_type_local: string -> Proof.context attribute
    31   val cases_set_local: string -> Proof.context attribute
    32   val induct_type_global: string -> theory attribute
    33   val induct_set_global: string -> theory attribute
    34   val induct_type_local: string -> Proof.context attribute
    35   val induct_set_local: string -> Proof.context attribute
    36   val casesN: string
    37   val inductN: string
    38   val typeN: string
    39   val setN: string
    40   val setup: (theory -> theory) list
    41 end;
    42 
    43 structure InductAttrib: INDUCT_ATTRIB =
    44 struct
    45 
    46 
    47 (** misc utils **)
    48 
    49 (* encode_type -- for indexing purposes *)
    50 
    51 fun encode_type (Type (c, Ts)) = Term.list_comb (Const (c, dummyT), map encode_type Ts)
    52   | encode_type (TFree (a, _)) = Free (a, dummyT)
    53   | encode_type (TVar (a, _)) = Var (a, dummyT);
    54 
    55 
    56 (* variables -- ordered left-to-right, preferring right *)
    57 
    58 local
    59 
    60 fun rev_vars_of tm =
    61   Term.foldl_aterms (fn (ts, t as Var _) => t :: ts | (ts, _) => ts) ([], tm)
    62   |> Library.distinct;
    63 
    64 val mk_var = encode_type o #2 o Term.dest_Var;
    65 
    66 in
    67 
    68 val vars_of = rev o rev_vars_of;
    69 
    70 fun first_var thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle LIST _ =>
    71   raise THM ("No variables in first premise of rule", 0, [thm]);
    72 
    73 fun last_var thm = mk_var (hd (rev_vars_of (Thm.concl_of thm))) handle LIST _ =>
    74   raise THM ("No variables in conclusion of rule", 0, [thm]);
    75 
    76 end;
    77 
    78 
    79 
    80 (** global and local induct data **)
    81 
    82 (* rules *)
    83 
    84 type rules = (string * thm) NetRules.T;
    85 
    86 val init_rules = NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2
    87   andalso Thm.eq_thm (th1, th2)) (K 0);
    88 
    89 fun lookup_rule (rs: rules) name = Library.assoc (NetRules.rules rs, name);
    90 
    91 fun print_rules kind sg rs =
    92   let val thms = map snd (NetRules.rules rs)
    93   in Pretty.writeln (Pretty.big_list kind (map (Display.pretty_thm_sg sg) thms)) end;
    94 
    95 
    96 (* theory data kind 'Isar/induction' *)
    97 
    98 structure GlobalInductArgs =
    99 struct
   100   val name = "Isar/induction";
   101   type T = (rules * rules) * (rules * rules);
   102 
   103   val empty =
   104     ((init_rules (first_var o #2), init_rules (Thm.major_prem_of o #2)),
   105      (init_rules (last_var o #2), init_rules (Thm.major_prem_of o #2)));
   106   val copy = I;
   107   val prep_ext = I;
   108   fun merge (((casesT1, casesS1), (inductT1, inductS1)),
   109       ((casesT2, casesS2), (inductT2, inductS2))) =
   110     ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
   111       (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)));
   112 
   113   fun print sg ((casesT, casesS), (inductT, inductS)) =
   114     (print_rules "induct type:" sg inductT;
   115       print_rules "induct set:" sg inductS;
   116       print_rules "cases type:" sg casesT;
   117       print_rules "cases set:" sg casesS);
   118 
   119   fun dest ((casesT, casesS), (inductT, inductS)) =
   120     {type_cases = NetRules.rules casesT,
   121      set_cases = NetRules.rules casesS,
   122      type_induct = NetRules.rules inductT,
   123      set_induct = NetRules.rules inductS};
   124 end;
   125 
   126 structure GlobalInduct = TheoryDataFun(GlobalInductArgs);
   127 val print_global_rules = GlobalInduct.print;
   128 val dest_global_rules = GlobalInductArgs.dest o GlobalInduct.get;
   129 
   130 
   131 (* proof data kind 'Isar/induction' *)
   132 
   133 structure LocalInductArgs =
   134 struct
   135   val name = "Isar/induction";
   136   type T = GlobalInductArgs.T;
   137 
   138   fun init thy = GlobalInduct.get thy;
   139   fun print x = GlobalInductArgs.print (ProofContext.sign_of x);
   140 end;
   141 
   142 structure LocalInduct = ProofDataFun(LocalInductArgs);
   143 val print_local_rules = LocalInduct.print;
   144 val dest_local_rules = GlobalInductArgs.dest o LocalInduct.get;
   145 
   146 
   147 (* access rules *)
   148 
   149 val lookup_casesT = lookup_rule o #1 o #1 o LocalInduct.get;
   150 val lookup_casesS = lookup_rule o #2 o #1 o LocalInduct.get;
   151 val lookup_inductT = lookup_rule o #1 o #2 o LocalInduct.get;
   152 val lookup_inductS = lookup_rule o #2 o #2 o LocalInduct.get;
   153 
   154 
   155 fun find_rules which how ctxt x =
   156   map snd (NetRules.retrieve (which (LocalInduct.get ctxt)) (how x));
   157 
   158 val find_casesT = find_rules (#1 o #1) encode_type;
   159 val find_casesS = find_rules (#2 o #1) Thm.concl_of;
   160 val find_inductT = find_rules (#1 o #2) encode_type;
   161 val find_inductS = find_rules (#2 o #2) Thm.concl_of;
   162 
   163 
   164 
   165 (** attributes **)
   166 
   167 local
   168 
   169 fun mk_att f g h name arg =
   170   let val (x, thm) = h arg in (f (g (name, thm)) x, thm) end;
   171 
   172 fun add_casesT rule x = apfst (apfst (NetRules.insert rule)) x;
   173 fun add_casesS rule x = apfst (apsnd (NetRules.insert rule)) x;
   174 fun add_inductT rule x = apsnd (apfst (NetRules.insert rule)) x;
   175 fun add_inductS rule x = apsnd (apsnd (NetRules.insert rule)) x;
   176 
   177 fun consumes0 x = RuleCases.consumes_default 0 x;
   178 fun consumes1 x = RuleCases.consumes_default 1 x;
   179 
   180 in
   181 
   182 val cases_type_global = mk_att GlobalInduct.map add_casesT consumes0;
   183 val cases_set_global = mk_att GlobalInduct.map add_casesS consumes1;
   184 val induct_type_global = mk_att GlobalInduct.map add_inductT consumes0;
   185 val induct_set_global = mk_att GlobalInduct.map add_inductS consumes1;
   186 
   187 val cases_type_local = mk_att LocalInduct.map add_casesT consumes0;
   188 val cases_set_local = mk_att LocalInduct.map add_casesS consumes1;
   189 val induct_type_local = mk_att LocalInduct.map add_inductT consumes0;
   190 val induct_set_local = mk_att LocalInduct.map add_inductS consumes1;
   191 
   192 end;
   193 
   194 
   195 (** concrete syntax **)
   196 
   197 val casesN = "cases";
   198 val inductN = "induct";
   199 
   200 val typeN = "type";
   201 val setN = "set";
   202 
   203 local
   204 
   205 fun spec k cert =
   206   (Args.$$$ k -- Args.colon) |-- Args.!!! (Args.name >> cert) ||
   207   Args.$$$ k >> K "";
   208 
   209 fun attrib sign_of add_type add_set = Scan.depend (fn x =>
   210   let val sg = sign_of x in
   211     spec typeN (Sign.certify_tyname sg o Sign.intern_tycon sg) >> add_type ||
   212     spec setN (Sign.certify_const sg o Sign.intern_const sg) >> add_set
   213   end >> pair x);
   214 
   215 in
   216 
   217 val cases_attr =
   218   (Attrib.syntax (attrib Theory.sign_of cases_type_global cases_set_global),
   219    Attrib.syntax (attrib ProofContext.sign_of cases_type_local cases_set_local));
   220 
   221 val induct_attr =
   222   (Attrib.syntax (attrib Theory.sign_of induct_type_global induct_set_global),
   223    Attrib.syntax (attrib ProofContext.sign_of induct_type_local induct_set_local));
   224 
   225 end;
   226 
   227 
   228 
   229 (** theory setup **)
   230 
   231 val setup =
   232   [GlobalInduct.init, LocalInduct.init,
   233    Attrib.add_attributes
   234     [(casesN, cases_attr, "declaration of cases rule for type or set"),
   235      (inductN, induct_attr, "declaration of induction rule for type or set")]];
   236 
   237 end;