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