merged
authorhaftmann
Sat, 19 Sep 2009 07:38:11 +0200
changeset 32684 139257823133
parent 32611 210fa627d767 (diff)
parent 32683 7c1fe854ca6a (current diff)
child 32685 29e4e567b5f4
merged
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Sep 19 07:38:03 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Sep 19 07:38:11 2009 +0200
@@ -38,9 +38,9 @@
   }
 
 datatype min_data = MinData of {
-  calls: int,
-  ratios: int,
-  lemmas: int
+  succs: int,
+  ab_ratios: int,
+  it_ratios: int
   }
 
 (* The first me_data component is only used if "minimize" is on.
@@ -52,8 +52,8 @@
   ShData{calls=calls, success=success, lemmas=lemmas, time_isa=time_isa,
     time_atp=time_atp, time_atp_fail=time_atp_fail}
 
-fun make_min_data (calls, ratios, lemmas) =
-  MinData{calls=calls, ratios=ratios, lemmas=lemmas}
+fun make_min_data (succs, ab_ratios, it_ratios) =
+  MinData{succs=succs, ab_ratios=ab_ratios, it_ratios=it_ratios}
 
 fun make_me_data (calls, success, time, timeout, lemmas, posns) =
   MeData{calls=calls, success=success, time=time, timeout=timeout, lemmas=lemmas, posns=posns}
@@ -61,7 +61,7 @@
 val empty_data =
   Data(make_sh_data (0, 0, 0, 0, 0, 0),
        make_me_data(0, 0, 0, 0, 0, []),
-       MinData{calls=0, ratios=0, lemmas=0},
+       MinData{succs=0, ab_ratios=0, it_ratios=0},
        make_me_data(0, 0, 0, 0, 0, []))
 
 fun map_sh_data f
@@ -70,8 +70,8 @@
         meda0, minda, meda)
 
 fun map_min_data f
-  (Data(shda, meda0, MinData{calls,ratios,lemmas}, meda)) =
-  Data(shda, meda0, make_min_data(f(calls,ratios,lemmas)), meda)
+  (Data(shda, meda0, MinData{succs,ab_ratios,it_ratios}, meda)) =
+  Data(shda, meda0, make_min_data(f(succs,ab_ratios,it_ratios)), meda)
 
 fun map_me_data0 f (Data (shda, MeData{calls,success,time,timeout,lemmas,posns}, minda, meda)) =
   Data(shda, make_me_data(f (calls,success,time,timeout,lemmas,posns)), minda, meda)
@@ -103,11 +103,14 @@
   map_sh_data (fn (calls, success, lemmas, time_isa, time_atp, time_atp_fail)
     => (calls, success, lemmas, time_isa, time_atp, time_atp_fail + t))
 
-val inc_min_calls =
-  map_min_data (fn (calls, ratios, lemmas) => (calls + 1, ratios, lemmas))
+val inc_min_succs =
+  map_min_data (fn (succs,ab_ratios,it_ratios) => (succs+1, ab_ratios, it_ratios))
 
-fun inc_min_ratios n =
-  map_min_data (fn (calls, ratios, lemmas) => (calls, ratios + n, lemmas))
+fun inc_min_ab_ratios r =
+  map_min_data (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios+r, it_ratios))
+
+fun inc_min_it_ratios r =
+  map_min_data (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios, it_ratios+r))
 
 val inc_metis_calls = map_me_data
  (fn (calls, success, time, timeout, lemmas,posns)
@@ -202,9 +205,10 @@
   else ()
  )
 
-fun log_min_data log calls ratios =
-  (log ("Number of minimizations: " ^ string_of_int calls);
-   log ("Minimization ratios: " ^ string_of_int ratios)
+fun log_min_data log succs ab_ratios it_ratios =
+  (log ("Number of successful minimizations: " ^ string_of_int succs);
+   log ("After/before ratios: " ^ string_of_int ab_ratios);
+   log ("Iterations ratios: " ^ string_of_int it_ratios)
   )
 
 in
@@ -215,7 +219,7 @@
     MeData{calls=metis_calls0,
       success=metis_success0, time=metis_time0, timeout=metis_timeout0,
       lemmas=metis_lemmas0,posns=metis_posns0},
-    MinData{calls=min_calls, ratios=min_ratios, lemmas=min_lemmas},
+    MinData{succs=min_succs, ab_ratios=ab_ratios, it_ratios=it_ratios},
     MeData{calls=metis_calls,
       success=metis_success, time=metis_time, timeout=metis_timeout,
       lemmas=metis_lemmas,posns=metis_posns})) =
@@ -228,7 +232,7 @@
       metis_success metis_time metis_timeout metis_lemmas  metis_posns else ();
     log "";
     if metis_calls0 > 0
-      then (log_min_data log min_calls min_ratios; log "";
+      then (log_min_data log min_succs ab_ratios it_ratios; log "";
             log_metis_data log "unminimized " sh_calls sh_success metis_calls0
               metis_success0 metis_time0 metis_timeout0 metis_lemmas0 metis_posns0)
       else ()
@@ -360,8 +364,9 @@
   in
     case minimize timeout st (these (!named_thms)) of
       (SOME (named_thms',its), msg) =>
-        (change_data id inc_min_calls;
-         change_data id (inc_min_ratios ((100*its) div n0));
+        (change_data id inc_min_succs;
+         change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));
+         change_data id (inc_min_it_ratios ((100*its) div n0));
          if length named_thms' = n0
          then log (minimize_tag id ^ "already minimal")
          else (named_thms := SOME named_thms';
@@ -396,7 +401,9 @@
     |> log o prefix (metis_tag id) 
   end
 
-fun sledgehammer_action args id (st as {log, ...}: Mirabelle.run_args) =
+fun sledgehammer_action args id (st as {log, pre, ...}: Mirabelle.run_args) =
+  if can Logic.dest_conjunction (Thm.major_prem_of(snd(snd(Proof.get_goal pre))))
+  then () else
   let
     val metis_fns = (inc_metis_calls, inc_metis_success, inc_metis_time,
         inc_metis_timeout, inc_metis_lemmas, inc_metis_posns)
--- a/src/HOL/Tools/inductive.ML	Sat Sep 19 07:38:03 2009 +0200
+++ b/src/HOL/Tools/inductive.ML	Sat Sep 19 07:38:11 2009 +0200
@@ -103,6 +103,7 @@
       "(P & True) = P" "(True & P) = P"
     by (fact simp_thms)+};
 
+val simp_thms'' = inf_fun_eq :: inf_bool_eq :: simp_thms';
 
 
 (** context data **)
@@ -559,7 +560,7 @@
         [rewrite_goals_tac [inductive_conj_def],
          DETERM (rtac raw_fp_induct 1),
          REPEAT (resolve_tac [le_funI, le_boolI] 1),
-         rewrite_goals_tac (inf_fun_eq :: inf_bool_eq :: simp_thms'),
+         rewrite_goals_tac simp_thms'',
          (*This disjE separates out the introduction rules*)
          REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])),
          (*Now break down the individual cases.  No disjE here in case
@@ -568,7 +569,7 @@
          REPEAT (FIRSTGOAL
            (resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))),
          EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule
-             (inductive_conj_def :: rec_preds_defs @ simp_thms') prem,
+             (inductive_conj_def :: rec_preds_defs @ simp_thms'') prem,
            conjI, refl] 1)) prems)]);
 
     val lemma = SkipProof.prove ctxt'' [] []