src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 54081 c7e9f1df30bb
parent 54080 540835cf11ed
child 54083 824db6ab3339
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Oct 08 20:56:35 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Oct 08 21:19:46 2013 +0200
     1.3 @@ -133,30 +133,31 @@
     1.4    in fst (norm t (([], 0), ([], 0))) end
     1.5  
     1.6  fun status_of_thm css name th =
     1.7 -  let val t = prop_of th in
     1.8 -    (* FIXME: use structured name *)
     1.9 -    if String.isSubstring ".induct" name andalso may_be_induction t then
    1.10 -      Induction
    1.11 -    else if Termtab.is_empty css then
    1.12 -      General
    1.13 -    else
    1.14 -      let val t = normalize_vars t in
    1.15 -        case Termtab.lookup css t of
    1.16 -          SOME status => status
    1.17 -        | NONE =>
    1.18 -          let val concl = Logic.strip_imp_concl t in
    1.19 -            case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl of
    1.20 -              SOME lrhss =>
    1.21 -              let
    1.22 -                val prems = Logic.strip_imp_prems t
    1.23 -                val t' = Logic.list_implies (prems, Logic.mk_equals lrhss)
    1.24 -              in
    1.25 -                Termtab.lookup css t' |> the_default General
    1.26 -              end
    1.27 -            | NONE => General
    1.28 -          end
    1.29 -      end
    1.30 -  end
    1.31 +  if Termtab.is_empty css then
    1.32 +    General
    1.33 +  else
    1.34 +    let val t = prop_of th in
    1.35 +      (* FIXME: use structured name *)
    1.36 +      if String.isSubstring ".induct" name andalso may_be_induction t then
    1.37 +        Induction
    1.38 +      else
    1.39 +        let val t = normalize_vars t in
    1.40 +          case Termtab.lookup css t of
    1.41 +            SOME status => status
    1.42 +          | NONE =>
    1.43 +            let val concl = Logic.strip_imp_concl t in
    1.44 +              case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl of
    1.45 +                SOME lrhss =>
    1.46 +                let
    1.47 +                  val prems = Logic.strip_imp_prems t
    1.48 +                  val t' = Logic.list_implies (prems, Logic.mk_equals lrhss)
    1.49 +                in
    1.50 +                  Termtab.lookup css t' |> the_default General
    1.51 +                end
    1.52 +              | NONE => General
    1.53 +            end
    1.54 +        end
    1.55 +    end
    1.56  
    1.57  fun stature_of_thm global assms chained css name th =
    1.58    (scope_of_thm global assms chained th, status_of_thm css name th)
    1.59 @@ -231,10 +232,11 @@
    1.60  
    1.61  val sep_that = Long_Name.separator ^ Obtain.thatN
    1.62  
    1.63 +val skolem_thesis = Name.skolem Auto_Bind.thesisN
    1.64 +
    1.65  fun is_that_fact th =
    1.66 -  String.isSuffix sep_that (Thm.get_name_hint th)
    1.67 -  andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
    1.68 -                           | _ => false) (prop_of th)
    1.69 +  exists_subterm (fn Free (s, _) => s = skolem_thesis | _ => false) (prop_of th)
    1.70 +  andalso String.isSuffix sep_that (Thm.get_name_hint th)
    1.71  
    1.72  datatype interest = Deal_Breaker | Interesting | Boring
    1.73  
    1.74 @@ -472,12 +474,12 @@
    1.75        Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
    1.76      val is_blacklisted_or_something = is_blacklisted_or_something ctxt ho_atp
    1.77      fun add_facts global foldx facts =
    1.78 -      foldx (fn (name0, ths) =>
    1.79 +      foldx (fn (name0, ths) => fn accum =>
    1.80          if name0 <> "" andalso
    1.81             forall (not o member Thm.eq_thm_prop add_ths) ths andalso
    1.82             (Facts.is_concealed facts name0 orelse
    1.83              (not generous andalso is_blacklisted_or_something name0)) then
    1.84 -          I
    1.85 +          accum
    1.86          else
    1.87            let
    1.88              val n = length ths
    1.89 @@ -487,32 +489,30 @@
    1.90                  NONE => false
    1.91                | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
    1.92            in
    1.93 -            pair n
    1.94 -            #> fold_rev (fn th => fn (j, accum) =>
    1.95 -                   (j - 1,
    1.96 -                    if not (member Thm.eq_thm_prop add_ths th) andalso
    1.97 -                       (is_likely_tautology_too_meta_or_too_technical th orelse
    1.98 -                        is_too_complex (prop_of th)) then
    1.99 -                      accum
   1.100 -                    else
   1.101 -                      let
   1.102 -                        val new =
   1.103 -                          (((fn () =>
   1.104 -                                if name0 = "" then
   1.105 -                                  backquote_thm ctxt th
   1.106 -                                else
   1.107 -                                  [Facts.extern ctxt facts name0,
   1.108 -                                   Name_Space.extern ctxt full_space name0]
   1.109 -                                  |> distinct (op =)
   1.110 -                                  |> find_first check_thms
   1.111 -                                  |> the_default name0
   1.112 -                                  |> make_name reserved multi j),
   1.113 -                             stature_of_thm global assms chained css name0 th),
   1.114 -                           th)
   1.115 -                      in
   1.116 -                        accum |> (if multi then apsnd else apfst) (cons new)
   1.117 -                      end)) ths
   1.118 -            #> snd
   1.119 +            snd (fold_rev (fn th => fn (j, accum as (uni_accum, multi_accum)) =>
   1.120 +              (j - 1,
   1.121 +               if not (member Thm.eq_thm_prop add_ths th) andalso
   1.122 +                  (is_likely_tautology_too_meta_or_too_technical th orelse
   1.123 +                   is_too_complex (prop_of th)) then
   1.124 +                 accum
   1.125 +               else
   1.126 +                 let
   1.127 +                   val new =
   1.128 +                     (((fn () =>
   1.129 +                           if name0 = "" then
   1.130 +                             backquote_thm ctxt th
   1.131 +                           else
   1.132 +                             [Facts.extern ctxt facts name0,
   1.133 +                              Name_Space.extern ctxt full_space name0]
   1.134 +                             |> find_first check_thms
   1.135 +                             |> the_default name0
   1.136 +                             |> make_name reserved multi j),
   1.137 +                        stature_of_thm global assms chained css name0 th),
   1.138 +                      th)
   1.139 +                 in
   1.140 +                   if multi then (uni_accum, new :: multi_accum)
   1.141 +                   else (new :: uni_accum, multi_accum)
   1.142 +                 end)) ths (n, accum))
   1.143            end)
   1.144    in
   1.145      (* The single-theorem names go before the multiple-theorem ones (e.g.,