push normalization further -- avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)
authorblanchet
Wed Dec 12 00:14:58 2012 +0100 (2012-12-12 ago)
changeset 504815d147d492792
parent 50480 d466ebc27810
child 50482 d7be7ccf428b
push normalization further -- avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Dec 11 22:19:39 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Dec 12 00:14:58 2012 +0100
     1.3 @@ -25,6 +25,7 @@
     1.4      -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
     1.5    val backquote_thm : Proof.context -> thm -> string
     1.6    val clasimpset_rule_table_of : Proof.context -> status Termtab.table
     1.7 +  val normalize_eq : term -> term
     1.8    val maybe_instantiate_inducts :
     1.9      Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
    1.10      -> (((unit -> string) * 'a) * thm) list
    1.11 @@ -309,9 +310,20 @@
    1.12                    |> add Inductive [] I spec_intros
    1.13    end
    1.14  
    1.15 +fun normalize_eq (t as @{const Trueprop}
    1.16 +        $ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2)) =
    1.17 +    if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t
    1.18 +    else HOLogic.mk_Trueprop (t0 $ t2 $ t1)
    1.19 +  | normalize_eq (t as @{const Trueprop} $ (@{const Not}
    1.20 +        $ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2))) =
    1.21 +    if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t
    1.22 +    else HOLogic.mk_Trueprop (HOLogic.mk_not (t0 $ t2 $ t1))
    1.23 +  | normalize_eq t = t
    1.24 +
    1.25  fun uniquify xs =
    1.26    Termtab.fold (cons o snd)
    1.27 -               (fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty) []
    1.28 +      (fold (Termtab.default o `(normalize_eq o prop_of o snd)) xs
    1.29 +            Termtab.empty) []
    1.30  
    1.31  fun struct_induct_rule_on th =
    1.32    case Logic.strip_horn (prop_of th) of
    1.33 @@ -395,7 +407,7 @@
    1.34              (not (Config.get ctxt ignore_no_atp) andalso
    1.35               is_package_def name0) orelse
    1.36              exists (fn s => String.isSuffix s name0)
    1.37 -                    (multi_base_blacklist ctxt ho_atp)) then
    1.38 +                   (multi_base_blacklist ctxt ho_atp)) then
    1.39            I
    1.40          else
    1.41            let