author boehmes Thu, 26 May 2011 22:02:40 +0200 changeset 42992 4fc15e3217eb parent 42991 3fa22920bf86 child 42993 da014b00d7a4
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
```--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Thu May 26 20:51:03 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Thu May 26 22:02:40 2011 +0200
@@ -360,7 +360,7 @@
in
fun def_axiom ctxt = Thm o try_apply ctxt [] [
named ctxt "conj/disj/distinct" prove_def_axiom,
-  Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' =>
+  Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' =>
named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac (simp_fast_tac ctxt')))]
end

@@ -421,7 +421,7 @@

fun prove_nnf ctxt = try_apply ctxt [] [
named ctxt "conj/disj" Z3_Proof_Literals.prove_conj_disj_eq,
-    Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' =>
+    Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' =>
named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac (simp_fast_tac ctxt')))]
in
fun nnf ctxt vars ps ct =
@@ -643,7 +643,7 @@

(* theory lemmas: linear arithmetic, arrays *)
fun th_lemma ctxt simpset thms = Thm o try_apply ctxt thms [
-  Z3_Proof_Tools.by_abstraction (false, true) ctxt thms (fn ctxt' =>
+  Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt thms (fn ctxt' =>
Z3_Proof_Tools.by_tac (
NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt')
ORELSE' NAMED ctxt' "simp+arith" (
@@ -693,26 +693,42 @@
(thm, snd (Assumption.add_assumes (#hyps (Thm.crep_thm thm)) ctxt))
in

+val abstraction_depth = 3
+  (*
+    This value was chosen large enough to potentially catch exceptions,
+    yet small enough to not cause too much harm.  The value might be
+    increased in the future, if reconstructing 'rewrite' fails on problems
+    that get too much abstracted to be reconstructable.
+  *)
+
fun rewrite simpset ths ct ctxt =
apfst Thm (declare_hyps ctxt (with_conv ctxt ths (try_apply ctxt [] [
named ctxt "conj/disj/distinct" prove_conj_disj_eq,
-    Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' =>
+    Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' =>
Z3_Proof_Tools.by_tac (
NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset)
THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))),
-    Z3_Proof_Tools.by_abstraction (false, true) ctxt [] (fn ctxt' =>
+    Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt [] (fn ctxt' =>
Z3_Proof_Tools.by_tac (
NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
THEN_ALL_NEW (
NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt')
ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
-    Z3_Proof_Tools.by_abstraction (true, true) ctxt [] (fn ctxt' =>
+    Z3_Proof_Tools.by_abstraction 0 (true, true) ctxt [] (fn ctxt' =>
Z3_Proof_Tools.by_tac (
NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
THEN_ALL_NEW (
NAMED ctxt' "fast (full)" (HOL_fast_tac ctxt')
ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
-    named ctxt "injectivity" (Z3_Proof_Methods.prove_injectivity ctxt)]) ct))
+    named ctxt "injectivity" (Z3_Proof_Methods.prove_injectivity ctxt),
+    Z3_Proof_Tools.by_abstraction abstraction_depth (true, true) ctxt []
+      (fn ctxt' =>
+        Z3_Proof_Tools.by_tac (
+          NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac simpset)
+          THEN_ALL_NEW (
+            NAMED ctxt' "fast (deepen)" (HOL_fast_tac ctxt')
+            ORELSE' NAMED ctxt' "arith (deepen)" (Arith_Data.arith_tac
+              ctxt'))))]) ct))

end
```
```--- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Thu May 26 20:51:03 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Thu May 26 22:02:40 2011 +0200
@@ -24,7 +24,7 @@
val match_instantiate: (cterm -> cterm) -> cterm -> thm -> thm
val by_tac: (int -> tactic) -> cterm -> thm
val make_hyp_def: thm -> Proof.context -> thm * Proof.context
-  val by_abstraction: bool * bool -> Proof.context -> thm list ->
+  val by_abstraction: int -> bool * bool -> Proof.context -> thm list ->
(Proof.context -> cterm -> thm) -> cterm -> thm

(*a faster COMP*)
@@ -147,7 +147,7 @@
val vs = map (Term.dest_Free o Thm.term_of) cvs'
in (Term.list_abs_free (vs, t), cvs') end

-fun fresh_abstraction cvs ct (cx as (ctxt, tab, idx, beta_norm)) =
+fun fresh_abstraction (_, cvs) ct (cx as (ctxt, tab, idx, beta_norm)) =
let val (t, cvs') = lambda_abstract cvs (Thm.term_of ct)
in
(case Termtab.lookup tab t of
@@ -163,78 +163,88 @@
in (cu, (ctxt', Termtab.update e tab, idx + 1, beta_norm')) end)
end

-fun abs_comb f g cvs ct =
+fun abs_comb f g dcvs ct =
let val (cf, cu) = Thm.dest_comb ct
-  in f cvs cf ##>> g cvs cu #>> uncurry Thm.capply end
+  in f dcvs cf ##>> g dcvs cu #>> uncurry Thm.capply end

fun abs_arg f = abs_comb (K pair) f

-fun abs_args f cvs ct =
+fun abs_args f dcvs ct =
(case Thm.term_of ct of
-    _ \$ _ => abs_comb (abs_args f) f cvs ct
+    _ \$ _ => abs_comb (abs_args f) f dcvs ct
| _ => pair ct)

-fun abs_list f g cvs ct =
+fun abs_list f g dcvs ct =
(case Thm.term_of ct of
Const (@{const_name Nil}, _) => pair ct
| Const (@{const_name Cons}, _) \$ _ \$ _ =>
-      abs_comb (abs_arg f) (abs_list f g) cvs ct
-  | _ => g cvs ct)
+      abs_comb (abs_arg f) (abs_list f g) dcvs ct
+  | _ => g dcvs ct)

-fun abs_abs f cvs ct =
+fun abs_abs f (depth, cvs) ct =
let val (cv, cu) = Thm.dest_abs NONE ct
-  in f (cv :: cvs) cu #>> Thm.cabs cv end
+  in f (depth, cv :: cvs) cu #>> Thm.cabs cv end

val is_atomic =
(fn Free _ => true | Var _ => true | Bound _ => true | _ => false)

-fun abstract (ext_logic, with_theories) =
+fun abstract depth (ext_logic, with_theories) =
let
fun abstr1 cvs ct = abs_arg abstr cvs ct
and abstr2 cvs ct = abs_comb abstr1 abstr cvs ct
and abstr3 cvs ct = abs_comb abstr2 abstr cvs ct
and abstr_abs cvs ct = abs_arg (abs_abs abstr) cvs ct

-    and abstr cvs ct =
+    and abstr (dcvs as (d, cvs)) ct =
(case Thm.term_of ct of
-        @{const Trueprop} \$ _ => abstr1 cvs ct
-      | @{const "==>"} \$ _ \$ _ => abstr2 cvs ct
+        @{const Trueprop} \$ _ => abstr1 dcvs ct
+      | @{const "==>"} \$ _ \$ _ => abstr2 dcvs ct
| @{const True} => pair ct
| @{const False} => pair ct
-      | @{const Not} \$ _ => abstr1 cvs ct
-      | @{const HOL.conj} \$ _ \$ _ => abstr2 cvs ct
-      | @{const HOL.disj} \$ _ \$ _ => abstr2 cvs ct
-      | @{const HOL.implies} \$ _ \$ _ => abstr2 cvs ct
-      | Const (@{const_name HOL.eq}, _) \$ _ \$ _ => abstr2 cvs ct
+      | @{const Not} \$ _ => abstr1 dcvs ct
+      | @{const HOL.conj} \$ _ \$ _ => abstr2 dcvs ct
+      | @{const HOL.disj} \$ _ \$ _ => abstr2 dcvs ct
+      | @{const HOL.implies} \$ _ \$ _ => abstr2 dcvs ct
+      | Const (@{const_name HOL.eq}, _) \$ _ \$ _ => abstr2 dcvs ct
| Const (@{const_name distinct}, _) \$ _ =>
-          if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
-          else fresh_abstraction cvs ct
+          if ext_logic then abs_arg (abs_list abstr fresh_abstraction) dcvs ct
+          else fresh_abstraction dcvs ct
| Const (@{const_name If}, _) \$ _ \$ _ \$ _ =>
-          if ext_logic then abstr3 cvs ct else fresh_abstraction cvs ct
+          if ext_logic then abstr3 dcvs ct else fresh_abstraction dcvs ct
| Const (@{const_name All}, _) \$ _ =>
-          if ext_logic then abstr_abs cvs ct else fresh_abstraction cvs ct
+          if ext_logic then abstr_abs dcvs ct else fresh_abstraction dcvs ct
| Const (@{const_name Ex}, _) \$ _ =>
-          if ext_logic then abstr_abs cvs ct else fresh_abstraction cvs ct
+          if ext_logic then abstr_abs dcvs ct else fresh_abstraction dcvs ct
| t => (fn cx =>
if is_atomic t orelse can HOLogic.dest_number t then (ct, cx)
else if with_theories andalso
Z3_Interface.is_builtin_theory_term (context_of cx) t
-          then abs_args abstr cvs ct cx
-          else fresh_abstraction cvs ct cx))
-  in abstr [] end
+          then abs_args abstr dcvs ct cx
+          else if d = 0 then fresh_abstraction dcvs ct cx
+          else
+            (case Term.strip_comb t of
+              (Const _, _) => abs_args abstr (d-1, cvs) ct cx
+            | (Free _, _) => abs_args abstr (d-1, cvs) ct cx
+            | _ => fresh_abstraction dcvs ct cx)))
+  in abstr (depth, []) end

val cimp = Thm.cterm_of @{theory} @{const "==>"}

-fun with_prems thms f ct =
+fun deepen depth f x =
+  if depth = 0 then f depth x
+  else (case try (f depth) x of SOME y => y | NONE => deepen (depth - 1) f x)
+
+fun with_prems depth thms f ct =
fold_rev (Thm.mk_binop cimp o Thm.cprop_of) thms ct
-  |> f
+  |> deepen depth f
|> fold (fn prem => fn th => Thm.implies_elim th prem) thms

in

-fun by_abstraction mode ctxt thms prove = with_prems thms (fn ct =>
-  let val (cu, cx) = abstract mode ct (abs_context ctxt)
-  in abs_instantiate cx (prove (context_of cx) cu) end)
+fun by_abstraction depth mode ctxt thms prove =
+  with_prems depth thms (fn d => fn ct =>
+    let val (cu, cx) = abstract d mode ct (abs_context ctxt)
+    in abs_instantiate cx (prove (context_of cx) cu) end)

end
```