src/Tools/induct.ML
changeset 30560 0cc3b7f03ade
parent 30528 7173bf123335
child 30722 623d4831c8cf
     1.1 --- a/src/Tools/induct.ML	Tue Mar 17 14:12:06 2009 +0100
     1.2 +++ b/src/Tools/induct.ML	Tue Mar 17 14:12:43 2009 +0100
     1.3 @@ -111,19 +111,19 @@
     1.4  
     1.5  (* rules *)
     1.6  
     1.7 -type rules = (string * thm) NetRules.T;
     1.8 +type rules = (string * thm) Item_Net.T;
     1.9  
    1.10  val init_rules =
    1.11 -  NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso
    1.12 +  Item_Net.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso
    1.13      Thm.eq_thm_prop (th1, th2));
    1.14  
    1.15  fun filter_rules (rs: rules) th =
    1.16 -  filter (fn (_, th') => Thm.eq_thm_prop (th, th')) (NetRules.rules rs);
    1.17 +  filter (fn (_, th') => Thm.eq_thm_prop (th, th')) (Item_Net.content rs);
    1.18  
    1.19 -fun lookup_rule (rs: rules) = AList.lookup (op =) (NetRules.rules rs);
    1.20 +fun lookup_rule (rs: rules) = AList.lookup (op =) (Item_Net.content rs);
    1.21  
    1.22  fun pretty_rules ctxt kind rs =
    1.23 -  let val thms = map snd (NetRules.rules rs)
    1.24 +  let val thms = map snd (Item_Net.content rs)
    1.25    in Pretty.big_list kind (map (ProofContext.pretty_thm ctxt) thms) end;
    1.26  
    1.27  
    1.28 @@ -139,21 +139,21 @@
    1.29    val extend = I;
    1.30    fun merge _ (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1)),
    1.31        ((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2))) =
    1.32 -    ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesP1, casesP2)),
    1.33 -      (NetRules.merge (inductT1, inductT2), NetRules.merge (inductP1, inductP2)),
    1.34 -      (NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductP1, coinductP2)));
    1.35 +    ((Item_Net.merge (casesT1, casesT2), Item_Net.merge (casesP1, casesP2)),
    1.36 +      (Item_Net.merge (inductT1, inductT2), Item_Net.merge (inductP1, inductP2)),
    1.37 +      (Item_Net.merge (coinductT1, coinductT2), Item_Net.merge (coinductP1, coinductP2)));
    1.38  );
    1.39  
    1.40  val get_local = InductData.get o Context.Proof;
    1.41  
    1.42  fun dest_rules ctxt =
    1.43    let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP)) = get_local ctxt in
    1.44 -    {type_cases = NetRules.rules casesT,
    1.45 -     pred_cases = NetRules.rules casesP,
    1.46 -     type_induct = NetRules.rules inductT,
    1.47 -     pred_induct = NetRules.rules inductP,
    1.48 -     type_coinduct = NetRules.rules coinductT,
    1.49 -     pred_coinduct = NetRules.rules coinductP}
    1.50 +    {type_cases = Item_Net.content casesT,
    1.51 +     pred_cases = Item_Net.content casesP,
    1.52 +     type_induct = Item_Net.content inductT,
    1.53 +     pred_induct = Item_Net.content inductP,
    1.54 +     type_coinduct = Item_Net.content coinductT,
    1.55 +     pred_coinduct = Item_Net.content coinductP}
    1.56    end;
    1.57  
    1.58  fun print_rules ctxt =
    1.59 @@ -184,7 +184,7 @@
    1.60  
    1.61  
    1.62  fun find_rules which how ctxt x =
    1.63 -  map snd (NetRules.retrieve (which (get_local ctxt)) (how x));
    1.64 +  map snd (Item_Net.retrieve (which (get_local ctxt)) (how x));
    1.65  
    1.66  val find_casesT = find_rules (#1 o #1) encode_type;
    1.67  val find_casesP = find_rules (#2 o #1) I;
    1.68 @@ -203,18 +203,18 @@
    1.69    let val (x, thm) = g arg in (InductData.map (f (name, thm)) x, thm) end;
    1.70  
    1.71  fun del_att which = Thm.declaration_attribute (fn th => InductData.map (which (pairself (fn rs =>
    1.72 -  fold NetRules.delete (filter_rules rs th) rs))));
    1.73 +  fold Item_Net.delete (filter_rules rs th) rs))));
    1.74  
    1.75  fun map1 f (x, y, z) = (f x, y, z);
    1.76  fun map2 f (x, y, z) = (x, f y, z);
    1.77  fun map3 f (x, y, z) = (x, y, f z);
    1.78  
    1.79 -fun add_casesT rule x = map1 (apfst (NetRules.insert rule)) x;
    1.80 -fun add_casesP rule x = map1 (apsnd (NetRules.insert rule)) x;
    1.81 -fun add_inductT rule x = map2 (apfst (NetRules.insert rule)) x;
    1.82 -fun add_inductP rule x = map2 (apsnd (NetRules.insert rule)) x;
    1.83 -fun add_coinductT rule x = map3 (apfst (NetRules.insert rule)) x;
    1.84 -fun add_coinductP rule x = map3 (apsnd (NetRules.insert rule)) x;
    1.85 +fun add_casesT rule x = map1 (apfst (Item_Net.insert rule)) x;
    1.86 +fun add_casesP rule x = map1 (apsnd (Item_Net.insert rule)) x;
    1.87 +fun add_inductT rule x = map2 (apfst (Item_Net.insert rule)) x;
    1.88 +fun add_inductP rule x = map2 (apsnd (Item_Net.insert rule)) x;
    1.89 +fun add_coinductT rule x = map3 (apfst (Item_Net.insert rule)) x;
    1.90 +fun add_coinductP rule x = map3 (apsnd (Item_Net.insert rule)) x;
    1.91  
    1.92  val consumes0 = RuleCases.consumes_default 0;
    1.93  val consumes1 = RuleCases.consumes_default 1;