comments
authornipkow
Thu Jun 07 15:08:18 2018 +0200 (11 months ago)
changeset 684056a0852b8e5a8
parent 68404 05605481935d
child 68406 6beb45f6cf67
child 68407 fd61a2e4e1f9
comments
src/Pure/raw_simplifier.ML
     1.1 --- a/src/Pure/raw_simplifier.ML	Wed Jun 06 18:20:03 2018 +0200
     1.2 +++ b/src/Pure/raw_simplifier.ML	Thu Jun 07 15:08:18 2018 +0200
     1.3 @@ -591,6 +591,27 @@
     1.4    let val rews = extract_rews ctxt sym (map (Thm.transfer' ctxt) thms);
     1.5    in fold (fold comb o mk_rrule) rews ctxt end;
     1.6  
     1.7 +(*
     1.8 +This code checks if the symetric version of a rule is already in the simpset.
     1.9 +However, the variable names in the two versions of the rule may differ.
    1.10 +Thus the current test modulo eq_rrule is too weak to be useful
    1.11 +and needs to be refined.
    1.12 +
    1.13 +fun present ctxt rules (rrule as {thm, elhs, ...}) =
    1.14 +  (Net.insert_term eq_rrule (Thm.term_of elhs, trim_context_rrule rrule) rules;
    1.15 +   false)
    1.16 +  handle Net.INSERT =>
    1.17 +    (cond_warning ctxt
    1.18 +       (fn () => print_thm ctxt "Symmetric rewrite rule already in simpset:" ("", thm));
    1.19 +     true);
    1.20 +
    1.21 +fun sym_present ctxt thms =
    1.22 +  let
    1.23 +    val rews = extract_rews ctxt true (map (Thm.transfer' ctxt) thms);
    1.24 +    val rrules = map mk_rrule2 (flat(map (mk_rrule ctxt) rews))
    1.25 +    val Simpset({rules, ...},_) = simpset_of ctxt
    1.26 +  in exists (present ctxt rules) rrules end
    1.27 +*)
    1.28  in
    1.29  
    1.30  fun ctxt addsimps thms =
    1.31 @@ -606,6 +627,12 @@
    1.32    comb_simps ctxt (del_rrule false) (map mk_rrule2 o mk_rrule ctxt) false thms;
    1.33  
    1.34  fun add_simp thm ctxt = ctxt addsimps [thm];
    1.35 +(*
    1.36 +with check for presence of symmetric version:
    1.37 +  if sym_present ctxt [thm]
    1.38 +  then (cond_warning ctxt (fn () => print_thm ctxt "Ignoring rewrite rule:" ("", thm)); ctxt)
    1.39 +  else ctxt addsimps [thm];
    1.40 +*)
    1.41  fun del_simp thm ctxt = ctxt delsimps [thm];
    1.42  fun flip_simp thm ctxt = addsymsimps (delsimps_quiet ctxt [thm]) [thm];
    1.43