src/Pure/Isar/induct_attrib.ML
changeset 24830 a7b3ab44d993
parent 24829 e1214fa781ca
child 24831 887d1b32a1a5
     1.1 --- a/src/Pure/Isar/induct_attrib.ML	Thu Oct 04 14:42:11 2007 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,224 +0,0 @@
     1.4 -(*  Title:      Pure/Isar/induct_attrib.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Markus Wenzel, TU Muenchen
     1.7 -
     1.8 -Declaration of rules for cases and induction.
     1.9 -*)
    1.10 -
    1.11 -signature INDUCT_ATTRIB =
    1.12 -sig
    1.13 -  val vars_of: term -> term list
    1.14 -  val dest_rules: Proof.context ->
    1.15 -    {type_cases: (string * thm) list, set_cases: (string * thm) list,
    1.16 -      type_induct: (string * thm) list, set_induct: (string * thm) list,
    1.17 -      type_coinduct: (string * thm) list, set_coinduct: (string * thm) list}
    1.18 -  val print_rules: Proof.context -> unit
    1.19 -  val lookup_casesT : Proof.context -> string -> thm option
    1.20 -  val lookup_casesS : Proof.context -> string -> thm option
    1.21 -  val lookup_inductT : Proof.context -> string -> thm option
    1.22 -  val lookup_inductS : Proof.context -> string -> thm option
    1.23 -  val lookup_coinductT : Proof.context -> string -> thm option
    1.24 -  val lookup_coinductS : Proof.context -> string -> thm option
    1.25 -  val find_casesT: Proof.context -> typ -> thm list
    1.26 -  val find_casesS: Proof.context -> term -> thm list
    1.27 -  val find_inductT: Proof.context -> typ -> thm list
    1.28 -  val find_inductS: Proof.context -> term -> thm list
    1.29 -  val find_coinductT: Proof.context -> typ -> thm list
    1.30 -  val find_coinductS: Proof.context -> term -> thm list
    1.31 -  val cases_type: string -> attribute
    1.32 -  val cases_set: string -> attribute
    1.33 -  val induct_type: string -> attribute
    1.34 -  val induct_set: string -> attribute
    1.35 -  val coinduct_type: string -> attribute
    1.36 -  val coinduct_set: string -> attribute
    1.37 -  val casesN: string
    1.38 -  val inductN: string
    1.39 -  val coinductN: string
    1.40 -  val typeN: string
    1.41 -  val setN: string
    1.42 -end;
    1.43 -
    1.44 -structure InductAttrib: INDUCT_ATTRIB =
    1.45 -struct
    1.46 -
    1.47 -
    1.48 -(** misc utils **)
    1.49 -
    1.50 -(* encode_type -- for indexing purposes *)
    1.51 -
    1.52 -fun encode_type (Type (c, Ts)) = Term.list_comb (Const (c, dummyT), map encode_type Ts)
    1.53 -  | encode_type (TFree (a, _)) = Free (a, dummyT)
    1.54 -  | encode_type (TVar (a, _)) = Var (a, dummyT);
    1.55 -
    1.56 -
    1.57 -(* variables -- ordered left-to-right, preferring right *)
    1.58 -
    1.59 -fun vars_of tm =
    1.60 -  rev (distinct (op =) (Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm []));
    1.61 -
    1.62 -local
    1.63 -
    1.64 -val mk_var = encode_type o #2 o Term.dest_Var;
    1.65 -
    1.66 -fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle Empty =>
    1.67 -  raise THM ("No variables in conclusion of rule", 0, [thm]);
    1.68 -
    1.69 -in
    1.70 -
    1.71 -fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle Empty =>
    1.72 -  raise THM ("No variables in major premise of rule", 0, [thm]);
    1.73 -
    1.74 -val left_var_concl = concl_var hd;
    1.75 -val right_var_concl = concl_var List.last;
    1.76 -
    1.77 -end;
    1.78 -
    1.79 -
    1.80 -
    1.81 -(** induct data **)
    1.82 -
    1.83 -(* rules *)
    1.84 -
    1.85 -type rules = (string * thm) NetRules.T;
    1.86 -
    1.87 -val init_rules =
    1.88 -  NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso
    1.89 -    Thm.eq_thm_prop (th1, th2));
    1.90 -
    1.91 -fun lookup_rule (rs: rules) = AList.lookup (op =) (NetRules.rules rs);
    1.92 -
    1.93 -fun pretty_rules ctxt kind rs =
    1.94 -  let val thms = map snd (NetRules.rules rs)
    1.95 -  in Pretty.big_list kind (map (ProofContext.pretty_thm ctxt) thms) end;
    1.96 -
    1.97 -
    1.98 -(* context data *)
    1.99 -
   1.100 -structure Induct = GenericDataFun
   1.101 -(
   1.102 -  type T = (rules * rules) * (rules * rules) * (rules * rules);
   1.103 -  val empty =
   1.104 -    ((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)),
   1.105 -     (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
   1.106 -     (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)));
   1.107 -  val extend = I;
   1.108 -  fun merge _ (((casesT1, casesS1), (inductT1, inductS1), (coinductT1, coinductS1)),
   1.109 -      ((casesT2, casesS2), (inductT2, inductS2), (coinductT2, coinductS2))) =
   1.110 -    ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
   1.111 -      (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)),
   1.112 -      (NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductS1, coinductS2)));
   1.113 -);
   1.114 -
   1.115 -val get_local = Induct.get o Context.Proof;
   1.116 -
   1.117 -fun dest_rules ctxt =
   1.118 -  let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in
   1.119 -    {type_cases = NetRules.rules casesT,
   1.120 -     set_cases = NetRules.rules casesS,
   1.121 -     type_induct = NetRules.rules inductT,
   1.122 -     set_induct = NetRules.rules inductS,
   1.123 -     type_coinduct = NetRules.rules coinductT,
   1.124 -     set_coinduct = NetRules.rules coinductS}
   1.125 -  end;
   1.126 -
   1.127 -fun print_rules ctxt =
   1.128 -  let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in
   1.129 -   [pretty_rules ctxt "coinduct type:" coinductT,
   1.130 -    pretty_rules ctxt "coinduct set:" coinductS,
   1.131 -    pretty_rules ctxt "induct type:" inductT,
   1.132 -    pretty_rules ctxt "induct set:" inductS,
   1.133 -    pretty_rules ctxt "cases type:" casesT,
   1.134 -    pretty_rules ctxt "cases set:" casesS]
   1.135 -    |> Pretty.chunks |> Pretty.writeln
   1.136 -  end;
   1.137 -
   1.138 -
   1.139 -(* access rules *)
   1.140 -
   1.141 -val lookup_casesT = lookup_rule o #1 o #1 o get_local;
   1.142 -val lookup_casesS = lookup_rule o #2 o #1 o get_local;
   1.143 -val lookup_inductT = lookup_rule o #1 o #2 o get_local;
   1.144 -val lookup_inductS = lookup_rule o #2 o #2 o get_local;
   1.145 -val lookup_coinductT = lookup_rule o #1 o #3 o get_local;
   1.146 -val lookup_coinductS = lookup_rule o #2 o #3 o get_local;
   1.147 -
   1.148 -
   1.149 -fun find_rules which how ctxt x =
   1.150 -  map snd (NetRules.retrieve (which (get_local ctxt)) (how x));
   1.151 -
   1.152 -val find_casesT = find_rules (#1 o #1) encode_type;
   1.153 -val find_casesS = find_rules (#2 o #1) I;
   1.154 -val find_inductT = find_rules (#1 o #2) encode_type;
   1.155 -val find_inductS = find_rules (#2 o #2) I;
   1.156 -val find_coinductT = find_rules (#1 o #3) encode_type;
   1.157 -val find_coinductS = find_rules (#2 o #3) I;
   1.158 -
   1.159 -
   1.160 -
   1.161 -(** attributes **)
   1.162 -
   1.163 -local
   1.164 -
   1.165 -fun mk_att f g name arg =
   1.166 -  let val (x, thm) = g arg in (Induct.map (f (name, thm)) x, thm) end;
   1.167 -
   1.168 -fun map1 f (x, y, z) = (f x, y, z);
   1.169 -fun map2 f (x, y, z) = (x, f y, z);
   1.170 -fun map3 f (x, y, z) = (x, y, f z);
   1.171 -
   1.172 -fun add_casesT rule x = map1 (apfst (NetRules.insert rule)) x;
   1.173 -fun add_casesS rule x = map1 (apsnd (NetRules.insert rule)) x;
   1.174 -fun add_inductT rule x = map2 (apfst (NetRules.insert rule)) x;
   1.175 -fun add_inductS rule x = map2 (apsnd (NetRules.insert rule)) x;
   1.176 -fun add_coinductT rule x = map3 (apfst (NetRules.insert rule)) x;
   1.177 -fun add_coinductS rule x = map3 (apsnd (NetRules.insert rule)) x;
   1.178 -
   1.179 -fun consumes0 x = RuleCases.consumes_default 0 x;
   1.180 -fun consumes1 x = RuleCases.consumes_default 1 x;
   1.181 -
   1.182 -in
   1.183 -
   1.184 -val cases_type = mk_att add_casesT consumes0;
   1.185 -val cases_set = mk_att add_casesS consumes1;
   1.186 -val induct_type = mk_att add_inductT consumes0;
   1.187 -val induct_set = mk_att add_inductS consumes1;
   1.188 -val coinduct_type = mk_att add_coinductT consumes0;
   1.189 -val coinduct_set = mk_att add_coinductS consumes1;
   1.190 -
   1.191 -end;
   1.192 -
   1.193 -
   1.194 -
   1.195 -(** concrete syntax **)
   1.196 -
   1.197 -val casesN = "cases";
   1.198 -val inductN = "induct";
   1.199 -val coinductN = "coinduct";
   1.200 -
   1.201 -val typeN = "type";
   1.202 -val setN = "set";
   1.203 -
   1.204 -local
   1.205 -
   1.206 -fun spec k arg =
   1.207 -  Scan.lift (Args.$$$ k -- Args.colon) |-- arg ||
   1.208 -  Scan.lift (Args.$$$ k) >> K "";
   1.209 -
   1.210 -fun attrib add_type add_set =
   1.211 -  Attrib.syntax (spec typeN Args.tyname >> add_type || spec setN Args.const >> add_set);
   1.212 -
   1.213 -in
   1.214 -
   1.215 -val cases_att = attrib cases_type cases_set;
   1.216 -val induct_att = attrib induct_type induct_set;
   1.217 -val coinduct_att = attrib coinduct_type coinduct_set;
   1.218 -
   1.219 -end;
   1.220 -
   1.221 -val _ = Context.add_setup
   1.222 - (Attrib.add_attributes
   1.223 -  [(casesN, cases_att, "declaration of cases rule for type or set"),
   1.224 -   (inductN, induct_att, "declaration of induction rule for type or set"),
   1.225 -   (coinductN, coinduct_att, "declaration of coinduction rule for type or set")]);
   1.226 -
   1.227 -end;