author blanchet Fri, 01 Aug 2014 23:29:50 +0200 changeset 57768 a63f14f1214c parent 57767 5bc204ca27ce child 57769 5ef0531d9db2
fine-tuned Isar reconstruction, esp. boolean simplifications
```--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Fri Aug 01 23:29:49 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Fri Aug 01 23:29:50 2014 +0200
@@ -107,13 +107,20 @@
let val t' = simplify_bool t in
if loose_bvar1 (t', 0) then all \$ Abs (s, T, t') else t'
end
-  | simplify_bool (@{const Not} \$ t) = s_not (simplify_bool t)
-  | simplify_bool (@{const conj} \$ t \$ u) = s_conj (simplify_bool t, simplify_bool u)
-  | simplify_bool (@{const disj} \$ t \$ u) = s_disj (simplify_bool t, simplify_bool u)
-  | simplify_bool (@{const implies} \$ t \$ u) = s_imp (simplify_bool t, simplify_bool u)
-  | simplify_bool (@{const HOL.eq (bool)} \$ t \$ u) = s_iff (simplify_bool t, simplify_bool u)
-  | simplify_bool (t as Const (@{const_name HOL.eq}, _) \$ u \$ v) =
-    if u aconv v then @{const True} else t
+  | simplify_bool (Const (@{const_name Not}, _) \$ t) = s_not (simplify_bool t)
+  | simplify_bool (Const (@{const_name conj}, _) \$ t \$ u) =
+    s_conj (simplify_bool t, simplify_bool u)
+  | simplify_bool (Const (@{const_name disj}, _) \$ t \$ u) =
+    s_disj (simplify_bool t, simplify_bool u)
+  | simplify_bool (Const (@{const_name implies}, _) \$ t \$ u) =
+    s_imp (simplify_bool t, simplify_bool u)
+  | simplify_bool ((t as Const (@{const_name HOL.eq}, _)) \$ u \$ v) =
+    (case (u, v) of
+      (Const (@{const_name True}, _), _) => v
+    | (u, Const (@{const_name True}, _)) => u
+    | (Const (@{const_name False}, _), v) => s_not v
+    | (u, Const (@{const_name False}, _)) => s_not u
+    | _ => if u aconv v then @{const True} else t \$ simplify_bool u \$ simplify_bool v)
| simplify_bool (t \$ u) = simplify_bool t \$ simplify_bool u
| simplify_bool (Abs (s, T, t)) = Abs (s, T, simplify_bool t)
| simplify_bool t = t
@@ -246,47 +253,27 @@

(* Higher-order translation. Variables are typed (although we don't use that information). Lambdas
-   are typed.
-
-  The code is similar to term_of_atp_fo. *)
-fun term_of_atp_ho ctxt textual sym_tab =
+   are typed. The code is similar to "term_of_atp_fo". *)
+fun term_of_atp_ho ctxt sym_tab =
let
val thy = Proof_Context.theory_of ctxt
-    val var_index = var_index_of_textual textual
+    val var_index = var_index_of_textual true

fun do_term opt_T u =
(case u of
AAbs(((var, ty), term), []) =>
let
val typ = typ_of_atp_type ctxt ty
-          val var_name = repair_var_name textual var
+          val var_name = repair_var_name true var
val tm = do_term NONE term
-        in quantify_over_var textual lambda' var_name typ tm end
+        in quantify_over_var true lambda' var_name typ tm end
| ATerm ((s, tys), us) =>
if s = ""
then error "Isar proof reconstruction failed because the ATP proof \
\contains unparsable material."
else if s = tptp_equal then
-          let
-            val ts = map (do_term NONE) us
-            fun equal_term ts =
-                list_comb (Const (@{const_name HOL.eq}, Type_Infer.anyT @{sort type}), ts)
-          in
-            if textual then
-              (case ts of
-                [t1, t2] =>
-                if loose_aconv (t1, t2) then
-                  @{const True}
-                else if Term.aconv_untyped (t2, @{const True}) then
-                  t1
-                else if Term.aconv_untyped (t1, @{const True}) then
-                  t2
-                else
-                  equal_term ts
-              | _ => equal_term ts)
-            else
-              equal_term ts
-          end
+          list_comb (Const (@{const_name HOL.eq}, Type_Infer.anyT @{sort type}),
+            map (do_term NONE) us)
else if not (null us) then
let
val args = List.map (do_term NONE) us
@@ -297,10 +284,10 @@
else if s = tptp_and then HOLogic.conj
else if s = tptp_implies then HOLogic.imp
else if s = tptp_iff orelse s = tptp_equal then HOLogic.eq_const dummyT
-        else if s = tptp_not_iff orelse s = tptp_not_equal then @{term "% P Q. Q ~= P"}
-        else if s = tptp_if then @{term "% P Q. Q --> P"}
-        else if s = tptp_not_and then @{term "% P Q. ~ (P & Q)"}
-        else if s = tptp_not_or then @{term "% P Q. ~ (P | Q)"}
+        else if s = tptp_not_iff orelse s = tptp_not_equal then @{term "%P Q. Q ~= P"}
+        else if s = tptp_if then @{term "%P Q. Q --> P"}
+        else if s = tptp_not_and then @{term "%P Q. ~ (P & Q)"}
+        else if s = tptp_not_or then @{term "%P Q. ~ (P | Q)"}
else if s = tptp_not then HOLogic.Not
else if s = tptp_ho_forall then HOLogic.all_const dummyT
else if s = tptp_ho_exists then HOLogic.exists_const dummyT
@@ -317,7 +304,7 @@
val Ts = map (typ_of_atp_type ctxt) tys @ map (typ_of_atp_term ctxt) type_us
val T =
(if not (null Ts) andalso robust_const_num_type_args thy s' = length Ts then
-                   if textual then try (Sign.const_instance thy) (s', Ts) else NONE
+                   try (Sign.const_instance thy) (s', Ts)
else
NONE)
|> (fn SOME T => T
@@ -343,10 +330,8 @@
(case unprefix_and_unascii fixed_var_prefix s of
SOME s => Free (s, T)
| NONE =>
-                  if textual andalso not (is_tptp_variable s) then
-                    Free (s |> textual ? (repair_var_name_raw #> fresh_up), T)
-                  else
-                    Var ((repair_var_name textual s, var_index), T))
+                  if not (is_tptp_variable s) then Free (s |> repair_var_name_raw |> fresh_up, T)
+                  else Var ((repair_var_name true s, var_index), T))
in list_comb (t, ts) end))
in do_term end

@@ -369,12 +354,8 @@
else if String.isPrefix native_type_prefix s then
@{const True} (* ignore TPTP type information *)
else if s = tptp_equal then
-          let val ts = map (do_term [] NONE) us in
-            if textual andalso length ts = 2 andalso loose_aconv (hd ts, List.last ts) then
-              @{const True}
-            else
-              list_comb (Const (@{const_name HOL.eq}, Type_Infer.anyT @{sort type}), ts)
-          end
+          list_comb (Const (@{const_name HOL.eq}, Type_Infer.anyT @{sort type}),
+            map (do_term [] NONE) us)
else
(case unprefix_and_unascii const_prefix s of
SOME s' =>
@@ -452,12 +433,10 @@
in do_term [] end

fun term_of_atp ctxt (ATP_Problem.THF _) type_enc =
-    if ATP_Problem_Generate.is_type_enc_higher_order type_enc
-    then term_of_atp_ho ctxt
+    if ATP_Problem_Generate.is_type_enc_higher_order type_enc then K (term_of_atp_ho ctxt)
else error "Unsupported Isar reconstruction."
| term_of_atp ctxt _ type_enc =
-    if not (ATP_Problem_Generate.is_type_enc_higher_order type_enc)
-    then term_of_atp_fo ctxt
+    if not (ATP_Problem_Generate.is_type_enc_higher_order type_enc) then term_of_atp_fo ctxt
else error "Unsupported Isar reconstruction."

fun term_of_atom ctxt format type_enc textual sym_tab pos (u as ATerm ((s, _), _)) =
@@ -633,6 +612,7 @@
|> prop_of_atp ctxt format type_enc true sym_tab
|> unlift_term lifted
|> uncombine_term thy
+        |> simplify_bool
in
SOME (name, role, t, rule, deps)
end```
```--- a/src/HOL/Tools/SMT2/smtlib2_isar.ML	Fri Aug 01 23:29:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smtlib2_isar.ML	Fri Aug 01 23:29:50 2014 +0200
@@ -11,15 +11,16 @@
val postprocess_step_conclusion: theory -> thm list -> term list -> term -> term
val normalizing_prems : Proof.context -> term -> (string * string list) list
val distinguish_conjecture_and_hypothesis : ''a list -> ''b -> ''b -> ''b list ->
-    (''a * 'c) list -> 'c list -> 'c -> 'c -> (ATP_Problem.atp_formula_role * 'c) option
+    (''a * 'c) list -> 'c list -> 'c -> (ATP_Problem.atp_formula_role * 'c) option
val unskolemize_names: term -> term
end;

structure SMTLIB2_Isar: SMTLIB2_ISAR =
struct

+open ATP_Util
open ATP_Problem
-open ATP_Util
+open ATP_Proof_Reconstruct

fun unlift_term ll_defs =
let
@@ -42,6 +43,7 @@
Raw_Simplifier.rewrite_term thy rewrite_rules []
#> Object_Logic.atomize_term thy
#> not (null ll_defs) ? unlift_term ll_defs
+  #> simplify_bool
#> unskolemize_names
#> HOLogic.mk_Trueprop

@@ -54,8 +56,8 @@
else
NONE)

-fun distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts hyp_ts concl_t
-    t =
+fun distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts hyp_ts
+    concl_t =
(case ss of
[s] => SOME (Axiom, the (AList.lookup (op =) fact_helper_ts s))
| _ =>```
```--- a/src/HOL/Tools/SMT2/verit_isar.ML	Fri Aug 01 23:29:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/verit_isar.ML	Fri Aug 01 23:29:50 2014 +0200
@@ -35,7 +35,7 @@
if rule = veriT_input_rule then
let val ss = the_list (AList.lookup (op =) fact_helper_ids (the (Int.fromString id))) in
(case distinguish_conjecture_and_hypothesis ss (the (Int.fromString id))
-                conjecture_id prem_ids fact_helper_ts hyp_ts concl_t concl of
+                conjecture_id prem_ids fact_helper_ts hyp_ts concl_t of
NONE => []
| SOME (role0, concl00) =>
let```
```--- a/src/HOL/Tools/SMT2/z3_new_isar.ML	Fri Aug 01 23:29:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_isar.ML	Fri Aug 01 23:29:50 2014 +0200
@@ -94,7 +94,7 @@
Z3_New_Proof.Asserted =>
let val ss = the_list (AList.lookup (op =) fact_helper_ids id) in
(case distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts
-                hyp_ts concl_t concl of
+                hyp_ts concl_t of
NONE => []
| SOME (role0, concl00) =>
let```
```--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Aug 01 23:29:49 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Aug 01 23:29:50 2014 +0200
@@ -89,7 +89,8 @@
line :: lines
else if role = Axiom then
lines (* axioms (facts) need no proof lines *)
-    else map (replace_dependencies_in_line (name, [])) lines
+    else
+      map (replace_dependencies_in_line (name, [])) lines
| add_line_pass1 line lines = line :: lines

fun add_lines_pass2 res _ [] = rev res
@@ -210,7 +211,7 @@

val rule_of_clause_id = fst o the o Symtab.lookup steps o fst

-        val finish_off = simplify_bool #> close_form #> rename_bound_vars
+        val finish_off = close_form #> rename_bound_vars

fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> finish_off
| prop_of_clause names =```
```--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Fri Aug 01 23:29:49 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Fri Aug 01 23:29:50 2014 +0200
@@ -98,7 +98,7 @@
subproofs1 @ subproofs2, (lfs, gfs), meths, comment1 ^ comment2), hopeless)
end

-val merge_slack_time = seconds 0.005
+val merge_slack_time = seconds 0.01
val merge_slack_factor = 1.5

fun adjust_merge_timeout max time =
@@ -117,7 +117,7 @@
val (compress_further, decrement_step_count) =
let
val number_of_steps = add_isar_steps (steps_of_isar_proof proof) 0
-          val target_number_of_steps = Real.round (Real.fromInt number_of_steps / compress)
+          val target_number_of_steps = Real.ceil (Real.fromInt number_of_steps / compress)
val delta = Unsynchronized.ref (number_of_steps - target_number_of_steps)
in
(fn () => !delta > 0, fn () => delta := !delta - 1)
@@ -273,8 +273,9 @@
if compress_further () then Proof (xs, assms, compress_steps steps) else proof
and compress_steps steps =
(* bottom-up: compress innermost proofs first *)
-        steps |> map (fn step => step |> compress_further () ? compress_sub_levels)
-              |> compress_further () ? compress_top_level
+        steps
+        |> map (fn step => step |> compress_further () ? compress_sub_levels)
+        |> compress_further () ? compress_top_level
and compress_sub_levels (Prove (qs, xs, l, t, subproofs, facts, meths, comment)) =
(* compress subproofs *)
Prove (qs, xs, l, t, map compress_proof subproofs, facts, meths, comment)```