src/Pure/Isar/induct_attrib.ML
changeset 11656 e499dceca569
child 11658 4200394242c5
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Isar/induct_attrib.ML	Wed Oct 03 20:55:31 2001 +0200
     1.3 @@ -0,0 +1,193 @@
     1.4 +(*  Title:      HOL/Tools/induct_attrib.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.8 +
     1.9 +Declaration of rules for cases and induction.
    1.10 +*)
    1.11 +
    1.12 +signature INDUCT_ATTRIB =
    1.13 +sig
    1.14 +  val dest_global_rules: theory ->
    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 +  val print_global_rules: theory -> unit
    1.18 +  val dest_local_rules: Proof.context ->
    1.19 +    {type_cases: (string * thm) list, set_cases: (string * thm) list,
    1.20 +      type_induct: (string * thm) list, set_induct: (string * thm) list}
    1.21 +  val print_local_rules: Proof.context -> unit
    1.22 +  val get_cases : Proof.context -> (string * thm) NetRules.T * (string * thm) NetRules.T
    1.23 +  val get_induct : Proof.context -> (string * thm) NetRules.T * (string * thm) NetRules.T
    1.24 +  val lookup_casesS : Proof.context -> string -> thm option
    1.25 +  val lookup_casesT : Proof.context -> string -> thm option
    1.26 +  val lookup_inductS : Proof.context -> string -> thm option
    1.27 +  val lookup_inductT : Proof.context -> string -> thm option
    1.28 +  val cases_type_global: string -> theory attribute
    1.29 +  val cases_set_global: string -> theory attribute
    1.30 +  val cases_type_local: string -> Proof.context attribute
    1.31 +  val cases_set_local: string -> Proof.context attribute
    1.32 +  val induct_type_global: string -> theory attribute
    1.33 +  val induct_set_global: string -> theory attribute
    1.34 +  val induct_type_local: string -> Proof.context attribute
    1.35 +  val induct_set_local: string -> Proof.context attribute
    1.36 +  val casesN: string
    1.37 +  val inductN: string
    1.38 +  val typeN: string
    1.39 +  val setN: string
    1.40 +  val setup: (theory -> theory) list
    1.41 +end;
    1.42 +
    1.43 +structure InductAttrib: INDUCT_ATTRIB =
    1.44 +struct
    1.45 +
    1.46 +
    1.47 +(** global and local induct data **)
    1.48 +
    1.49 +(* rules *)
    1.50 +
    1.51 +type rules = (string * thm) NetRules.T;
    1.52 +
    1.53 +fun eq_rule ((s1:string, th1), (s2, th2)) = s1 = s2 andalso Thm.eq_thm (th1, th2);
    1.54 +
    1.55 +val type_rules = NetRules.init eq_rule (Thm.concl_of o #2);
    1.56 +val set_rules = NetRules.init eq_rule (Thm.major_prem_of o #2);
    1.57 +
    1.58 +fun lookup_rule (rs:rules) name = Library.assoc (NetRules.rules rs, name);
    1.59 +
    1.60 +fun print_rules kind sg rs =
    1.61 +  let val thms = map snd (NetRules.rules rs)
    1.62 +  in Pretty.writeln (Pretty.big_list kind (map (Display.pretty_thm_sg sg) thms)) end;
    1.63 +
    1.64 +
    1.65 +(* theory data kind 'HOL/induction' *)
    1.66 +
    1.67 +structure GlobalInductArgs =
    1.68 +struct
    1.69 +  val name = "HOL/induction";
    1.70 +  type T = (rules * rules) * (rules * rules);
    1.71 +
    1.72 +  val empty = ((type_rules, set_rules), (type_rules, set_rules));
    1.73 +  val copy = I;
    1.74 +  val prep_ext = I;
    1.75 +  fun merge (((casesT1, casesS1), (inductT1, inductS1)),
    1.76 +      ((casesT2, casesS2), (inductT2, inductS2))) =
    1.77 +    ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
    1.78 +      (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)));
    1.79 +
    1.80 +  fun print sg ((casesT, casesS), (inductT, inductS)) =
    1.81 +    (print_rules "type cases:" sg casesT;
    1.82 +      print_rules "set cases:" sg casesS;
    1.83 +      print_rules "type induct:" sg inductT;
    1.84 +      print_rules "set induct:" sg inductS);
    1.85 +
    1.86 +  fun dest ((casesT, casesS), (inductT, inductS)) =
    1.87 +    {type_cases = NetRules.rules casesT,
    1.88 +     set_cases = NetRules.rules casesS,
    1.89 +     type_induct = NetRules.rules inductT,
    1.90 +     set_induct = NetRules.rules inductS};
    1.91 +end;
    1.92 +
    1.93 +structure GlobalInduct = TheoryDataFun(GlobalInductArgs);
    1.94 +val print_global_rules = GlobalInduct.print;
    1.95 +val dest_global_rules = GlobalInductArgs.dest o GlobalInduct.get;
    1.96 +
    1.97 +
    1.98 +(* proof data kind 'HOL/induction' *)
    1.99 +
   1.100 +structure LocalInductArgs =
   1.101 +struct
   1.102 +  val name = "HOL/induction";
   1.103 +  type T = GlobalInductArgs.T;
   1.104 +
   1.105 +  fun init thy = GlobalInduct.get thy;
   1.106 +  fun print x = GlobalInductArgs.print (ProofContext.sign_of x);
   1.107 +end;
   1.108 +
   1.109 +structure LocalInduct = ProofDataFun(LocalInductArgs);
   1.110 +val print_local_rules = LocalInduct.print;
   1.111 +val dest_local_rules = GlobalInductArgs.dest o LocalInduct.get;
   1.112 +
   1.113 +
   1.114 +(* access rules *)
   1.115 +
   1.116 +val get_cases = #1 o LocalInduct.get;
   1.117 +val get_induct = #2 o LocalInduct.get;
   1.118 +
   1.119 +val lookup_casesT = lookup_rule o #1 o get_cases;
   1.120 +val lookup_casesS = lookup_rule o #2 o get_cases;
   1.121 +val lookup_inductT = lookup_rule o #1 o get_induct;
   1.122 +val lookup_inductS = lookup_rule o #2 o get_induct;
   1.123 +
   1.124 +
   1.125 +
   1.126 +(** attributes **)
   1.127 +
   1.128 +local
   1.129 +
   1.130 +fun mk_att f g h name arg =
   1.131 +  let val (x, thm) = h arg in (f (g (name, thm)) x, thm) end;
   1.132 +
   1.133 +fun add_casesT rule x = apfst (apfst (NetRules.insert rule)) x;
   1.134 +fun add_casesS rule x = apfst (apsnd (NetRules.insert rule)) x;
   1.135 +fun add_inductT rule x = apsnd (apfst (NetRules.insert rule)) x;
   1.136 +fun add_inductS rule x = apsnd (apsnd (NetRules.insert rule)) x;
   1.137 +
   1.138 +fun consumes0 x = RuleCases.consumes_default 0 x;
   1.139 +fun consumes1 x = RuleCases.consumes_default 1 x;
   1.140 +
   1.141 +in
   1.142 +
   1.143 +val cases_type_global = mk_att GlobalInduct.map add_casesT consumes0;
   1.144 +val cases_set_global = mk_att GlobalInduct.map add_casesS consumes1;
   1.145 +val induct_type_global = mk_att GlobalInduct.map add_inductT consumes0;
   1.146 +val induct_set_global = mk_att GlobalInduct.map add_inductS consumes1;
   1.147 +
   1.148 +val cases_type_local = mk_att LocalInduct.map add_casesT consumes0;
   1.149 +val cases_set_local = mk_att LocalInduct.map add_casesS consumes1;
   1.150 +val induct_type_local = mk_att LocalInduct.map add_inductT consumes0;
   1.151 +val induct_set_local = mk_att LocalInduct.map add_inductS consumes1;
   1.152 +
   1.153 +end;
   1.154 +
   1.155 +
   1.156 +(** concrete syntax **)
   1.157 +
   1.158 +val casesN = "cases";
   1.159 +val inductN = "induct";
   1.160 +
   1.161 +val typeN = "type";
   1.162 +val setN = "set";
   1.163 +
   1.164 +local
   1.165 +
   1.166 +fun spec k = (Args.$$$ k -- Args.colon) |-- Args.!!! Args.name;
   1.167 +
   1.168 +fun attrib sign_of add_type add_set = Scan.depend (fn x =>
   1.169 +  let val sg = sign_of x in
   1.170 +    spec typeN >> (add_type o Sign.certify_tycon sg o Sign.intern_tycon sg) ||
   1.171 +    spec setN  >> (add_set o Sign.certify_const sg o Sign.intern_const sg)
   1.172 +  end >> pair x);
   1.173 +
   1.174 +in
   1.175 +
   1.176 +val cases_attr =
   1.177 +  (Attrib.syntax (attrib Theory.sign_of cases_type_global cases_set_global),
   1.178 +   Attrib.syntax (attrib ProofContext.sign_of cases_type_local cases_set_local));
   1.179 +
   1.180 +val induct_attr =
   1.181 +  (Attrib.syntax (attrib Theory.sign_of induct_type_global induct_set_global),
   1.182 +   Attrib.syntax (attrib ProofContext.sign_of induct_type_local induct_set_local));
   1.183 +
   1.184 +end;
   1.185 +
   1.186 +
   1.187 +
   1.188 +(** theory setup **)
   1.189 +
   1.190 +val setup =
   1.191 +  [GlobalInduct.init, LocalInduct.init,
   1.192 +   Attrib.add_attributes
   1.193 +    [(casesN, cases_attr, "declaration of cases rule for type or set"),
   1.194 +     (inductN, induct_attr, "declaration of induction rule for type or set")]];
   1.195 +
   1.196 +end;