src/Provers/typedsimp.ML
changeset 33339 d41f77196338
parent 32960 69916a850301
child 35021 c839a4c670c6
equal deleted inserted replaced
33338:de76079f973a 33339:d41f77196338
    62   [| a=b: N; reduce(succ(b), c) |] ==> succ(a)=c: N   *)
    62   [| a=b: N; reduce(succ(b), c) |] ==> succ(a)=c: N   *)
    63 fun subconv_rule rl = rl RS trans_red;
    63 fun subconv_rule rl = rl RS trans_red;
    64 
    64 
    65 (*If the rule proves an equality then add both forms to simp_rls
    65 (*If the rule proves an equality then add both forms to simp_rls
    66   else add the rule to other_rls*)
    66   else add the rule to other_rls*)
    67 fun add_rule (rl, (simp_rls, other_rls)) =
    67 fun add_rule rl (simp_rls, other_rls) =
    68     (simp_rule rl :: resimp_rule rl :: simp_rls, other_rls)
    68     (simp_rule rl :: resimp_rule rl :: simp_rls, other_rls)
    69     handle THM _ => (simp_rls, rl :: other_rls);
    69     handle THM _ => (simp_rls, rl :: other_rls);
    70 
    70 
    71 (*Given the list rls, return the pair (simp_rls, other_rls).*)
    71 (*Given the list rls, return the pair (simp_rls, other_rls).*)
    72 fun process_rules rls = List.foldr add_rule ([],[]) rls;
    72 fun process_rules rls = fold_rev add_rule rls ([], []);
    73 
    73 
    74 (*Given list of rewrite rules, return list of both forms, reject others*)
    74 (*Given list of rewrite rules, return list of both forms, reject others*)
    75 fun process_rewrites rls = 
    75 fun process_rewrites rls = 
    76   case process_rules rls of
    76   case process_rules rls of
    77       (simp_rls,[])  =>  simp_rls
    77       (simp_rls,[])  =>  simp_rls