author blanchet Sun, 15 Dec 2013 20:09:13 +0100 changeset 54758 ba488d89614a parent 54757 4960647932ec child 54759 b632390b5966
simplify generated propositions
```--- a/src/HOL/Tools/ATP/atp_util.ML	Sun Dec 15 19:01:06 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML	Sun Dec 15 20:09:13 2013 +0100
@@ -283,11 +283,13 @@
| s_not (@{const True}) = @{const False}
| s_not (@{const Not} \$ t) = t
| s_not t = @{const Not} \$ t
+
fun s_conj (@{const True}, t2) = t2
| s_conj (t1, @{const True}) = t1
| s_conj (@{const False}, _) = @{const False}
| s_conj (_, @{const False}) = @{const False}
| s_conj (t1, t2) = if t1 aconv t2 then t1 else HOLogic.mk_conj (t1, t2)
+
fun s_disj (@{const False}, t2) = t2
| s_disj (t1, @{const False}) = t1
| s_disj (@{const True}, _) = @{const True}```
```--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sun Dec 15 19:01:06 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sun Dec 15 20:09:13 2013 +0100
@@ -89,11 +89,10 @@

fun alist_cons_list eq (k, v) = AList.map_default eq (k, []) (cons v)

-(* FIXME: use "prop_of_clause" defined below *)
HOLogic.dest_Trueprop
-    #> curry HOLogic.mk_imp (Library.foldr1 HOLogic.mk_conj (map HOLogic.dest_Trueprop hyps))
+    #> curry s_imp (Library.foldr1 s_conj (map HOLogic.dest_Trueprop hyps))
#> HOLogic.mk_Trueprop

fun inline_z3_hypotheses _ _ [] = []
@@ -115,12 +114,22 @@
end
end

-(* No "real" literals means only type information (tfree_tcs, clsrel, or
-   clsarity). *)
-fun is_only_type_information t = t aconv @{term True}
+fun simplify_prop (@{const Not} \$ t) = s_not (simplify_prop t)
+  | simplify_prop (@{const conj} \$ t \$ u) = s_conj (simplify_prop t, simplify_prop u)
+  | simplify_prop (@{const disj} \$ t \$ u) = s_disj (simplify_prop t, simplify_prop u)
+  | simplify_prop (@{const implies} \$ t \$ u) = s_imp (simplify_prop t, simplify_prop u)
+  | simplify_prop (@{const HOL.eq (bool)} \$ t \$ u) = s_iff (simplify_prop t, simplify_prop u)
+  | simplify_prop (t \$ u) = simplify_prop t \$ simplify_prop u
+  | simplify_prop (Abs (s, T, t)) = Abs (s, T, simplify_prop t)
+  | simplify_prop t = t

-(* Discard facts; consolidate adjacent lines that prove the same formula, since
-   they differ only in type information.*)
+fun simplify_line (name, role, t, rule, deps) = (name, role, simplify_prop t, rule, deps)
+
+(* No "real" literals means only type information (tfree_tcs, clsrel, or clsarity). *)
+fun is_only_type_information t = t aconv @{prop True}
+
+(* Discard facts; consolidate adjacent lines that prove the same formula, since they differ only in
+   type information.*)
fun add_line_pass1 (line as (name as (_, ss), role, t, rule, [])) lines =
(* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire)
internal facts or definitions. *)
@@ -134,7 +143,8 @@
map (replace_dependencies_in_line (name, [])) lines
| add_line_pass1 line lines = line :: lines

-(* Recursively delete empty lines (type information) from the proof. *)
+(* Recursively delete empty lines (type information) from the proof.
+   (FIXME: needed? And why is "delete_dependency" so complicated?) *)
fun add_line_pass2 (line as (name, _, t, _, [])) lines =
if is_only_type_information t then delete_dependency name lines else line :: lines
| add_line_pass2 line lines = line :: lines
@@ -142,7 +152,7 @@
fold_rev add_line_pass2 (map (replace_dependencies_in_line (name, [])) lines) []

fun add_line_pass3 res [] = rev res
-  | add_line_pass3 res ((line as (name as (_, ss), role, t, rule, deps)) :: lines) =
+  | add_line_pass3 res ((name as (_, ss), role, t, rule, deps) :: lines) =
if role <> Plain orelse is_skolemize_rule rule orelse is_arith_rule rule orelse
(* the last line must be kept *)
null lines orelse
@@ -150,7 +160,7 @@
andalso length deps >= 2 andalso
(* don't keep next to last line, which usually results in a trivial step *)
not (can the_single lines)) then
-      add_line_pass3 (line :: res) lines
+      add_line_pass3 ((name, role, simplify_prop t, rule, deps) :: res) lines
else
add_line_pass3 res (map (replace_dependencies_in_line (name, deps)) lines)

@@ -161,8 +171,10 @@
fun kill_useless_labels_in_proof proof =
let
val used_ls = add_labels_of_proof proof []
+
fun kill_label l = if member (op =) used_ls l then l else no_label
fun kill_assms assms = map (apfst kill_label) assms
+
fun kill_step (Prove (qs, xs, l, t, subproofs, by)) =
Prove (qs, xs, kill_label l, t, map kill_proof subproofs, by)
| kill_step step = step
@@ -172,18 +184,16 @@
kill_proof proof
end

-fun prefix_of_depth n = replicate_string (n + 1)
-
val assume_prefix = "a"
val have_prefix = "f"

val relabel_proof =
let
-    fun fresh_label depth prefix (old as (l, subst, next)) =
+    fun fresh_label depth prefix (accum as (l, subst, next)) =
if l = no_label then
-        old
+        accum
else
-        let val l' = (prefix_of_depth depth prefix, next) in
+        let val l' = (replicate_string (depth + 1) prefix, next) in
(l', (l, l') :: subst, next + 1)
end

@@ -264,6 +274,7 @@
val atp_proof =
atp_proof
|> inline_z3_defs []
+          |> map simplify_line
|> inline_z3_hypotheses [] []
|> rpair [] |-> fold_rev add_line_pass1
|> rpair [] |-> fold_rev add_line_pass2
@@ -301,21 +312,21 @@
val steps =
Symtab.empty
|> fold (fn (name as (s, _), role, t, rule, _) =>
-                      Symtab.update_new (s, (rule,
-                        t |> (if is_clause_tainted [name] then
-                                role <> Conjecture ? s_not_prop
-                                #> fold exists_of (map Var (Term.add_vars t []))
-                              else
-                                I))))
-                  atp_proof
+              Symtab.update_new (s, (rule, t
+                |> (if is_clause_tainted [name] then
+                      role <> Conjecture ? s_not_prop
+                      #> fold exists_of (map Var (Term.add_vars t []))
+                    else
+                      I))))
+            atp_proof

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

fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> close_form
| prop_of_clause names =
let
-              val lits =
-                map (HOLogic.dest_Trueprop o snd) (map_filter (Symtab.lookup steps o fst) names)
+              val lits = map (HOLogic.dest_Trueprop o snd)
+                (map_filter (Symtab.lookup steps o fst) names)
in
(case List.partition (can HOLogic.dest_not) lits of
(negs as _ :: _, pos as _ :: _) =>
@@ -405,9 +416,7 @@
|> isar_try0 ? try0 preplay_timeout preplay_interface
|> postprocess_remove_unreferenced_steps (isar_try0 ? min_deps_of_step preplay_interface)
|> `overall_preplay_stats
-          ||> (chain_direct_proof
-            #> kill_useless_labels_in_proof
-            #> relabel_proof)
+          ||> (chain_direct_proof #> kill_useless_labels_in_proof #> relabel_proof)

val isar_text =
string_of_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count isar_proof```