src/Pure/Isar/induct_attrib.ML
author wenzelm
Sun Jul 08 19:51:58 2007 +0200 (2007-07-08)
changeset 23655 d2d1138e0ddc
parent 22846 fb79144af9a3
permissions -rw-r--r--
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
     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: Proof.context ->
    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: Proof.context -> 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 -> attribute
    29   val cases_set: string -> attribute
    30   val induct_type: string -> attribute
    31   val induct_set: string -> attribute
    32   val coinduct_type: string -> attribute
    33   val coinduct_set: string -> 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   rev (distinct (op =) (Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm []));
    58 
    59 local
    60 
    61 val mk_var = encode_type o #2 o Term.dest_Var;
    62 
    63 fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle Empty =>
    64   raise THM ("No variables in conclusion of rule", 0, [thm]);
    65 
    66 in
    67 
    68 fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle Empty =>
    69   raise THM ("No variables in major premise of rule", 0, [thm]);
    70 
    71 val left_var_concl = concl_var hd;
    72 val right_var_concl = concl_var List.last;
    73 
    74 end;
    75 
    76 
    77 
    78 (** induct data **)
    79 
    80 (* rules *)
    81 
    82 type rules = (string * thm) NetRules.T;
    83 
    84 val init_rules =
    85   NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso
    86     Thm.eq_thm_prop (th1, th2));
    87 
    88 fun lookup_rule (rs: rules) = AList.lookup (op =) (NetRules.rules rs);
    89 
    90 fun pretty_rules ctxt kind rs =
    91   let val thms = map snd (NetRules.rules rs)
    92   in Pretty.big_list kind (map (ProofContext.pretty_thm ctxt) thms) end;
    93 
    94 
    95 (* context data *)
    96 
    97 structure Induct = GenericDataFun
    98 (
    99   type T = (rules * rules) * (rules * rules) * (rules * rules);
   100   val empty =
   101     ((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)),
   102      (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
   103      (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)));
   104   val extend = I;
   105   fun merge _ (((casesT1, casesS1), (inductT1, inductS1), (coinductT1, coinductS1)),
   106       ((casesT2, casesS2), (inductT2, inductS2), (coinductT2, coinductS2))) =
   107     ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
   108       (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)),
   109       (NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductS1, coinductS2)));
   110 );
   111 
   112 val get_local = Induct.get o Context.Proof;
   113 
   114 fun dest_rules ctxt =
   115   let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in
   116     {type_cases = NetRules.rules casesT,
   117      set_cases = NetRules.rules casesS,
   118      type_induct = NetRules.rules inductT,
   119      set_induct = NetRules.rules inductS,
   120      type_coinduct = NetRules.rules coinductT,
   121      set_coinduct = NetRules.rules coinductS}
   122   end;
   123 
   124 fun print_rules ctxt =
   125   let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in
   126    [pretty_rules ctxt "coinduct type:" coinductT,
   127     pretty_rules ctxt "coinduct set:" coinductS,
   128     pretty_rules ctxt "induct type:" inductT,
   129     pretty_rules ctxt "induct set:" inductS,
   130     pretty_rules ctxt "cases type:" casesT,
   131     pretty_rules ctxt "cases set:" casesS]
   132     |> Pretty.chunks |> Pretty.writeln
   133   end;
   134 
   135 
   136 (* access rules *)
   137 
   138 val lookup_casesT = lookup_rule o #1 o #1 o get_local;
   139 val lookup_casesS = lookup_rule o #2 o #1 o get_local;
   140 val lookup_inductT = lookup_rule o #1 o #2 o get_local;
   141 val lookup_inductS = lookup_rule o #2 o #2 o get_local;
   142 val lookup_coinductT = lookup_rule o #1 o #3 o get_local;
   143 val lookup_coinductS = lookup_rule o #2 o #3 o get_local;
   144 
   145 
   146 fun find_rules which how ctxt x =
   147   map snd (NetRules.retrieve (which (get_local ctxt)) (how x));
   148 
   149 val find_casesT = find_rules (#1 o #1) encode_type;
   150 val find_casesS = find_rules (#2 o #1) I;
   151 val find_inductT = find_rules (#1 o #2) encode_type;
   152 val find_inductS = find_rules (#2 o #2) I;
   153 val find_coinductT = find_rules (#1 o #3) encode_type;
   154 val find_coinductS = find_rules (#2 o #3) I;
   155 
   156 
   157 
   158 (** attributes **)
   159 
   160 local
   161 
   162 fun mk_att f g name arg =
   163   let val (x, thm) = g arg in (Induct.map (f (name, thm)) x, thm) end;
   164 
   165 fun map1 f (x, y, z) = (f x, y, z);
   166 fun map2 f (x, y, z) = (x, f y, z);
   167 fun map3 f (x, y, z) = (x, y, f z);
   168 
   169 fun add_casesT rule x = map1 (apfst (NetRules.insert rule)) x;
   170 fun add_casesS rule x = map1 (apsnd (NetRules.insert rule)) x;
   171 fun add_inductT rule x = map2 (apfst (NetRules.insert rule)) x;
   172 fun add_inductS rule x = map2 (apsnd (NetRules.insert rule)) x;
   173 fun add_coinductT rule x = map3 (apfst (NetRules.insert rule)) x;
   174 fun add_coinductS rule x = map3 (apsnd (NetRules.insert rule)) x;
   175 
   176 fun consumes0 x = RuleCases.consumes_default 0 x;
   177 fun consumes1 x = RuleCases.consumes_default 1 x;
   178 
   179 in
   180 
   181 val cases_type = mk_att add_casesT consumes0;
   182 val cases_set = mk_att add_casesS consumes1;
   183 val induct_type = mk_att add_inductT consumes0;
   184 val induct_set = mk_att add_inductS consumes1;
   185 val coinduct_type = mk_att add_coinductT consumes0;
   186 val coinduct_set = mk_att add_coinductS consumes1;
   187 
   188 end;
   189 
   190 
   191 
   192 (** concrete syntax **)
   193 
   194 val casesN = "cases";
   195 val inductN = "induct";
   196 val coinductN = "coinduct";
   197 
   198 val typeN = "type";
   199 val setN = "set";
   200 
   201 local
   202 
   203 fun spec k arg =
   204   Scan.lift (Args.$$$ k -- Args.colon) |-- arg ||
   205   Scan.lift (Args.$$$ k) >> K "";
   206 
   207 fun attrib add_type add_set =
   208   Attrib.syntax (spec typeN Args.tyname >> add_type || spec setN Args.const >> add_set);
   209 
   210 in
   211 
   212 val cases_att = attrib cases_type cases_set;
   213 val induct_att = attrib induct_type induct_set;
   214 val coinduct_att = attrib coinduct_type coinduct_set;
   215 
   216 end;
   217 
   218 val _ = Context.add_setup
   219  (Attrib.add_attributes
   220   [(casesN, cases_att, "declaration of cases rule for type or set"),
   221    (inductN, induct_att, "declaration of induction rule for type or set"),
   222    (coinductN, coinduct_att, "declaration of coinduction rule for type or set")]);
   223 
   224 end;