moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
authorwenzelm
Wed Oct 03 20:55:31 2001 +0200 (2001-10-03)
changeset 11656e499dceca569
parent 11655 923e4d0d36d5
child 11657 03c4a5c08a79
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
src/HOL/Tools/induct_attrib.ML
src/Pure/Isar/induct_attrib.ML
     1.1 --- a/src/HOL/Tools/induct_attrib.ML	Wed Oct 03 20:54:16 2001 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,193 +0,0 @@
     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;
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/Isar/induct_attrib.ML	Wed Oct 03 20:55:31 2001 +0200
     2.3 @@ -0,0 +1,193 @@
     2.4 +(*  Title:      HOL/Tools/induct_attrib.ML
     2.5 +    ID:         $Id$
     2.6 +    Author:     Markus Wenzel, TU Muenchen
     2.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     2.8 +
     2.9 +Declaration of rules for cases and induction.
    2.10 +*)
    2.11 +
    2.12 +signature INDUCT_ATTRIB =
    2.13 +sig
    2.14 +  val dest_global_rules: theory ->
    2.15 +    {type_cases: (string * thm) list, set_cases: (string * thm) list,
    2.16 +      type_induct: (string * thm) list, set_induct: (string * thm) list}
    2.17 +  val print_global_rules: theory -> unit
    2.18 +  val dest_local_rules: Proof.context ->
    2.19 +    {type_cases: (string * thm) list, set_cases: (string * thm) list,
    2.20 +      type_induct: (string * thm) list, set_induct: (string * thm) list}
    2.21 +  val print_local_rules: Proof.context -> unit
    2.22 +  val get_cases : Proof.context -> (string * thm) NetRules.T * (string * thm) NetRules.T
    2.23 +  val get_induct : Proof.context -> (string * thm) NetRules.T * (string * thm) NetRules.T
    2.24 +  val lookup_casesS : Proof.context -> string -> thm option
    2.25 +  val lookup_casesT : Proof.context -> string -> thm option
    2.26 +  val lookup_inductS : Proof.context -> string -> thm option
    2.27 +  val lookup_inductT : Proof.context -> string -> thm option
    2.28 +  val cases_type_global: string -> theory attribute
    2.29 +  val cases_set_global: string -> theory attribute
    2.30 +  val cases_type_local: string -> Proof.context attribute
    2.31 +  val cases_set_local: string -> Proof.context attribute
    2.32 +  val induct_type_global: string -> theory attribute
    2.33 +  val induct_set_global: string -> theory attribute
    2.34 +  val induct_type_local: string -> Proof.context attribute
    2.35 +  val induct_set_local: string -> Proof.context attribute
    2.36 +  val casesN: string
    2.37 +  val inductN: string
    2.38 +  val typeN: string
    2.39 +  val setN: string
    2.40 +  val setup: (theory -> theory) list
    2.41 +end;
    2.42 +
    2.43 +structure InductAttrib: INDUCT_ATTRIB =
    2.44 +struct
    2.45 +
    2.46 +
    2.47 +(** global and local induct data **)
    2.48 +
    2.49 +(* rules *)
    2.50 +
    2.51 +type rules = (string * thm) NetRules.T;
    2.52 +
    2.53 +fun eq_rule ((s1:string, th1), (s2, th2)) = s1 = s2 andalso Thm.eq_thm (th1, th2);
    2.54 +
    2.55 +val type_rules = NetRules.init eq_rule (Thm.concl_of o #2);
    2.56 +val set_rules = NetRules.init eq_rule (Thm.major_prem_of o #2);
    2.57 +
    2.58 +fun lookup_rule (rs:rules) name = Library.assoc (NetRules.rules rs, name);
    2.59 +
    2.60 +fun print_rules kind sg rs =
    2.61 +  let val thms = map snd (NetRules.rules rs)
    2.62 +  in Pretty.writeln (Pretty.big_list kind (map (Display.pretty_thm_sg sg) thms)) end;
    2.63 +
    2.64 +
    2.65 +(* theory data kind 'HOL/induction' *)
    2.66 +
    2.67 +structure GlobalInductArgs =
    2.68 +struct
    2.69 +  val name = "HOL/induction";
    2.70 +  type T = (rules * rules) * (rules * rules);
    2.71 +
    2.72 +  val empty = ((type_rules, set_rules), (type_rules, set_rules));
    2.73 +  val copy = I;
    2.74 +  val prep_ext = I;
    2.75 +  fun merge (((casesT1, casesS1), (inductT1, inductS1)),
    2.76 +      ((casesT2, casesS2), (inductT2, inductS2))) =
    2.77 +    ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
    2.78 +      (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)));
    2.79 +
    2.80 +  fun print sg ((casesT, casesS), (inductT, inductS)) =
    2.81 +    (print_rules "type cases:" sg casesT;
    2.82 +      print_rules "set cases:" sg casesS;
    2.83 +      print_rules "type induct:" sg inductT;
    2.84 +      print_rules "set induct:" sg inductS);
    2.85 +
    2.86 +  fun dest ((casesT, casesS), (inductT, inductS)) =
    2.87 +    {type_cases = NetRules.rules casesT,
    2.88 +     set_cases = NetRules.rules casesS,
    2.89 +     type_induct = NetRules.rules inductT,
    2.90 +     set_induct = NetRules.rules inductS};
    2.91 +end;
    2.92 +
    2.93 +structure GlobalInduct = TheoryDataFun(GlobalInductArgs);
    2.94 +val print_global_rules = GlobalInduct.print;
    2.95 +val dest_global_rules = GlobalInductArgs.dest o GlobalInduct.get;
    2.96 +
    2.97 +
    2.98 +(* proof data kind 'HOL/induction' *)
    2.99 +
   2.100 +structure LocalInductArgs =
   2.101 +struct
   2.102 +  val name = "HOL/induction";
   2.103 +  type T = GlobalInductArgs.T;
   2.104 +
   2.105 +  fun init thy = GlobalInduct.get thy;
   2.106 +  fun print x = GlobalInductArgs.print (ProofContext.sign_of x);
   2.107 +end;
   2.108 +
   2.109 +structure LocalInduct = ProofDataFun(LocalInductArgs);
   2.110 +val print_local_rules = LocalInduct.print;
   2.111 +val dest_local_rules = GlobalInductArgs.dest o LocalInduct.get;
   2.112 +
   2.113 +
   2.114 +(* access rules *)
   2.115 +
   2.116 +val get_cases = #1 o LocalInduct.get;
   2.117 +val get_induct = #2 o LocalInduct.get;
   2.118 +
   2.119 +val lookup_casesT = lookup_rule o #1 o get_cases;
   2.120 +val lookup_casesS = lookup_rule o #2 o get_cases;
   2.121 +val lookup_inductT = lookup_rule o #1 o get_induct;
   2.122 +val lookup_inductS = lookup_rule o #2 o get_induct;
   2.123 +
   2.124 +
   2.125 +
   2.126 +(** attributes **)
   2.127 +
   2.128 +local
   2.129 +
   2.130 +fun mk_att f g h name arg =
   2.131 +  let val (x, thm) = h arg in (f (g (name, thm)) x, thm) end;
   2.132 +
   2.133 +fun add_casesT rule x = apfst (apfst (NetRules.insert rule)) x;
   2.134 +fun add_casesS rule x = apfst (apsnd (NetRules.insert rule)) x;
   2.135 +fun add_inductT rule x = apsnd (apfst (NetRules.insert rule)) x;
   2.136 +fun add_inductS rule x = apsnd (apsnd (NetRules.insert rule)) x;
   2.137 +
   2.138 +fun consumes0 x = RuleCases.consumes_default 0 x;
   2.139 +fun consumes1 x = RuleCases.consumes_default 1 x;
   2.140 +
   2.141 +in
   2.142 +
   2.143 +val cases_type_global = mk_att GlobalInduct.map add_casesT consumes0;
   2.144 +val cases_set_global = mk_att GlobalInduct.map add_casesS consumes1;
   2.145 +val induct_type_global = mk_att GlobalInduct.map add_inductT consumes0;
   2.146 +val induct_set_global = mk_att GlobalInduct.map add_inductS consumes1;
   2.147 +
   2.148 +val cases_type_local = mk_att LocalInduct.map add_casesT consumes0;
   2.149 +val cases_set_local = mk_att LocalInduct.map add_casesS consumes1;
   2.150 +val induct_type_local = mk_att LocalInduct.map add_inductT consumes0;
   2.151 +val induct_set_local = mk_att LocalInduct.map add_inductS consumes1;
   2.152 +
   2.153 +end;
   2.154 +
   2.155 +
   2.156 +(** concrete syntax **)
   2.157 +
   2.158 +val casesN = "cases";
   2.159 +val inductN = "induct";
   2.160 +
   2.161 +val typeN = "type";
   2.162 +val setN = "set";
   2.163 +
   2.164 +local
   2.165 +
   2.166 +fun spec k = (Args.$$$ k -- Args.colon) |-- Args.!!! Args.name;
   2.167 +
   2.168 +fun attrib sign_of add_type add_set = Scan.depend (fn x =>
   2.169 +  let val sg = sign_of x in
   2.170 +    spec typeN >> (add_type o Sign.certify_tycon sg o Sign.intern_tycon sg) ||
   2.171 +    spec setN  >> (add_set o Sign.certify_const sg o Sign.intern_const sg)
   2.172 +  end >> pair x);
   2.173 +
   2.174 +in
   2.175 +
   2.176 +val cases_attr =
   2.177 +  (Attrib.syntax (attrib Theory.sign_of cases_type_global cases_set_global),
   2.178 +   Attrib.syntax (attrib ProofContext.sign_of cases_type_local cases_set_local));
   2.179 +
   2.180 +val induct_attr =
   2.181 +  (Attrib.syntax (attrib Theory.sign_of induct_type_global induct_set_global),
   2.182 +   Attrib.syntax (attrib ProofContext.sign_of induct_type_local induct_set_local));
   2.183 +
   2.184 +end;
   2.185 +
   2.186 +
   2.187 +
   2.188 +(** theory setup **)
   2.189 +
   2.190 +val setup =
   2.191 +  [GlobalInduct.init, LocalInduct.init,
   2.192 +   Attrib.add_attributes
   2.193 +    [(casesN, cases_attr, "declaration of cases rule for type or set"),
   2.194 +     (inductN, induct_attr, "declaration of induction rule for type or set")]];
   2.195 +
   2.196 +end;