src/Tools/induct.ML
changeset 27140 327a73f02d5f
parent 26940 80df961f7900
child 27323 385c0ce33173
equal deleted inserted replaced
27139:a1f3c7b5ce9c 27140:327a73f02d5f
    34   val find_inductP: Proof.context -> term -> thm list
    34   val find_inductP: Proof.context -> term -> thm list
    35   val find_coinductT: Proof.context -> typ -> thm list
    35   val find_coinductT: Proof.context -> typ -> thm list
    36   val find_coinductP: Proof.context -> term -> thm list
    36   val find_coinductP: Proof.context -> term -> thm list
    37   val cases_type: string -> attribute
    37   val cases_type: string -> attribute
    38   val cases_pred: string -> attribute
    38   val cases_pred: string -> attribute
       
    39   val cases_del: attribute
    39   val induct_type: string -> attribute
    40   val induct_type: string -> attribute
    40   val induct_pred: string -> attribute
    41   val induct_pred: string -> attribute
       
    42   val induct_del: attribute
    41   val coinduct_type: string -> attribute
    43   val coinduct_type: string -> attribute
    42   val coinduct_pred: string -> attribute
    44   val coinduct_pred: string -> attribute
       
    45   val coinduct_del: attribute
    43   val casesN: string
    46   val casesN: string
    44   val inductN: string
    47   val inductN: string
    45   val coinductN: string
    48   val coinductN: string
    46   val typeN: string
    49   val typeN: string
    47   val predN: string
    50   val predN: string
   112 
   115 
   113 val init_rules =
   116 val init_rules =
   114   NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso
   117   NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso
   115     Thm.eq_thm_prop (th1, th2));
   118     Thm.eq_thm_prop (th1, th2));
   116 
   119 
       
   120 fun filter_rules (rs: rules) th =
       
   121   filter (fn (_, th') => Thm.eq_thm_prop (th, th')) (NetRules.rules rs);
       
   122 
   117 fun lookup_rule (rs: rules) = AList.lookup (op =) (NetRules.rules rs);
   123 fun lookup_rule (rs: rules) = AList.lookup (op =) (NetRules.rules rs);
   118 
   124 
   119 fun pretty_rules ctxt kind rs =
   125 fun pretty_rules ctxt kind rs =
   120   let val thms = map snd (NetRules.rules rs)
   126   let val thms = map snd (NetRules.rules rs)
   121   in Pretty.big_list kind (map (ProofContext.pretty_thm ctxt) thms) end;
   127   in Pretty.big_list kind (map (ProofContext.pretty_thm ctxt) thms) end;
   122 
   128 
   123 
   129 
   124 (* context data *)
   130 (* context data *)
   125 
   131 
   126 structure Induct = GenericDataFun
   132 structure InductData = GenericDataFun
   127 (
   133 (
   128   type T = (rules * rules) * (rules * rules) * (rules * rules);
   134   type T = (rules * rules) * (rules * rules) * (rules * rules);
   129   val empty =
   135   val empty =
   130     ((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)),
   136     ((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)),
   131      (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
   137      (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
   136     ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesP1, casesP2)),
   142     ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesP1, casesP2)),
   137       (NetRules.merge (inductT1, inductT2), NetRules.merge (inductP1, inductP2)),
   143       (NetRules.merge (inductT1, inductT2), NetRules.merge (inductP1, inductP2)),
   138       (NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductP1, coinductP2)));
   144       (NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductP1, coinductP2)));
   139 );
   145 );
   140 
   146 
   141 val get_local = Induct.get o Context.Proof;
   147 val get_local = InductData.get o Context.Proof;
   142 
   148 
   143 fun dest_rules ctxt =
   149 fun dest_rules ctxt =
   144   let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP)) = get_local ctxt in
   150   let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP)) = get_local ctxt in
   145     {type_cases = NetRules.rules casesT,
   151     {type_cases = NetRules.rules casesT,
   146      pred_cases = NetRules.rules casesP,
   152      pred_cases = NetRules.rules casesP,
   192 (** attributes **)
   198 (** attributes **)
   193 
   199 
   194 local
   200 local
   195 
   201 
   196 fun mk_att f g name arg =
   202 fun mk_att f g name arg =
   197   let val (x, thm) = g arg in (Induct.map (f (name, thm)) x, thm) end;
   203   let val (x, thm) = g arg in (InductData.map (f (name, thm)) x, thm) end;
       
   204 
       
   205 fun del_att which = Thm.declaration_attribute (fn th => InductData.map (which (pairself (fn rs =>
       
   206   fold NetRules.delete (filter_rules rs th) rs))));
   198 
   207 
   199 fun map1 f (x, y, z) = (f x, y, z);
   208 fun map1 f (x, y, z) = (f x, y, z);
   200 fun map2 f (x, y, z) = (x, f y, z);
   209 fun map2 f (x, y, z) = (x, f y, z);
   201 fun map3 f (x, y, z) = (x, y, f z);
   210 fun map3 f (x, y, z) = (x, y, f z);
   202 
   211 
   205 fun add_inductT rule x = map2 (apfst (NetRules.insert rule)) x;
   214 fun add_inductT rule x = map2 (apfst (NetRules.insert rule)) x;
   206 fun add_inductP rule x = map2 (apsnd (NetRules.insert rule)) x;
   215 fun add_inductP rule x = map2 (apsnd (NetRules.insert rule)) x;
   207 fun add_coinductT rule x = map3 (apfst (NetRules.insert rule)) x;
   216 fun add_coinductT rule x = map3 (apfst (NetRules.insert rule)) x;
   208 fun add_coinductP rule x = map3 (apsnd (NetRules.insert rule)) x;
   217 fun add_coinductP rule x = map3 (apsnd (NetRules.insert rule)) x;
   209 
   218 
   210 fun consumes0 x = RuleCases.consumes_default 0 x;
   219 val consumes0 = RuleCases.consumes_default 0;
   211 fun consumes1 x = RuleCases.consumes_default 1 x;
   220 val consumes1 = RuleCases.consumes_default 1;
   212 
   221 
   213 in
   222 in
   214 
   223 
   215 val cases_type = mk_att add_casesT consumes0;
   224 val cases_type = mk_att add_casesT consumes0;
   216 val cases_pred = mk_att add_casesP consumes1;
   225 val cases_pred = mk_att add_casesP consumes1;
       
   226 val cases_del = del_att map1;
       
   227 
   217 val induct_type = mk_att add_inductT consumes0;
   228 val induct_type = mk_att add_inductT consumes0;
   218 val induct_pred = mk_att add_inductP consumes1;
   229 val induct_pred = mk_att add_inductP consumes1;
       
   230 val induct_del = del_att map2;
       
   231 
   219 val coinduct_type = mk_att add_coinductT consumes0;
   232 val coinduct_type = mk_att add_coinductT consumes0;
   220 val coinduct_pred = mk_att add_coinductP consumes1;
   233 val coinduct_pred = mk_att add_coinductP consumes1;
       
   234 val coinduct_del = del_att map3;
   221 
   235 
   222 end;
   236 end;
   223 
   237 
   224 
   238 
   225 
   239 
   237 
   251 
   238 fun spec k arg =
   252 fun spec k arg =
   239   Scan.lift (Args.$$$ k -- Args.colon) |-- arg ||
   253   Scan.lift (Args.$$$ k -- Args.colon) |-- arg ||
   240   Scan.lift (Args.$$$ k) >> K "";
   254   Scan.lift (Args.$$$ k) >> K "";
   241 
   255 
   242 fun attrib add_type add_pred = Attrib.syntax
   256 fun attrib add_type add_pred del = Attrib.syntax
   243  (spec typeN Args.tyname >> add_type ||
   257  (spec typeN Args.tyname >> add_type ||
   244   spec predN Args.const >> add_pred ||
   258   spec predN Args.const >> add_pred ||
   245   spec setN Args.const >> add_pred);
   259   spec setN Args.const >> add_pred ||
   246 
   260   Scan.lift Args.del >> K del);
   247 val cases_att = attrib cases_type cases_pred;
   261 
   248 val induct_att = attrib induct_type induct_pred;
   262 val cases_att = attrib cases_type cases_pred cases_del;
   249 val coinduct_att = attrib coinduct_type coinduct_pred;
   263 val induct_att = attrib induct_type induct_pred induct_del;
       
   264 val coinduct_att = attrib coinduct_type coinduct_pred coinduct_del;
   250 
   265 
   251 in
   266 in
   252 
   267 
   253 val attrib_setup = Attrib.add_attributes
   268 val attrib_setup = Attrib.add_attributes
   254  [(casesN, cases_att, "declaration of cases rule for type or predicate/set"),
   269  [(casesN, cases_att, "declaration of cases rule"),
   255   (inductN, induct_att, "declaration of induction rule for type or predicate/set"),
   270   (inductN, induct_att, "declaration of induction rule"),
   256   (coinductN, coinduct_att, "declaration of coinduction rule for type or predicate/set")];
   271   (coinductN, coinduct_att, "declaration of coinduction rule")];
   257 
   272 
   258 end;
   273 end;
   259 
   274 
   260 
   275 
   261 
   276