# HG changeset patch
# User boehmes
# Date 1264174701 -3600
# Node ID 1d5ee19ef9404b81c76447c1a54dba5ab38d045c
# Parent  cd7c98fdab809bcb7ea3bfba1208d9d5974c8e10
support skolem constant for extensional arrays in Z3 proofs

diff -r cd7c98fdab80 -r 1d5ee19ef940 src/HOL/SMT/SMT_Base.thy
--- a/src/HOL/SMT/SMT_Base.thy	Fri Jan 22 16:33:44 2010 +0100
+++ b/src/HOL/SMT/SMT_Base.thy	Fri Jan 22 16:38:21 2010 +0100
@@ -89,7 +89,17 @@
 
 definition "apply" where "apply f x = f x"
 
-lemmas array_rules = apply_def fun_upd_same fun_upd_other fun_upd_upd ext
+definition array_ext where "array_ext a b = (SOME x. a = b \<or> a x \<noteq> b x)"
+
+lemma fun_upd_eq: "(f = f (x := y)) = (f x = y)"
+proof
+  assume "f = f(x:=y)"
+  hence "f x = (f(x:=y)) x" by simp
+  thus "f x = y" by simp
+qed (auto simp add: ext)
+
+lemmas array_rules =
+  ext fun_upd_apply fun_upd_same fun_upd_other fun_upd_upd fun_upd_eq apply_def
 
 
 section {* First-order logic *}
diff -r cd7c98fdab80 -r 1d5ee19ef940 src/HOL/SMT/Tools/z3_proof.ML
--- a/src/HOL/SMT/Tools/z3_proof.ML	Fri Jan 22 16:33:44 2010 +0100
+++ b/src/HOL/SMT/Tools/z3_proof.ML	Fri Jan 22 16:38:21 2010 +0100
@@ -136,6 +136,7 @@
       | (Sym ("rem", _), [t, u]) => T.mk_rem t u
       | (Sym ("select", _), [m, k]) => T.mk_access m k
       | (Sym ("store", _), [m, k, v]) => T.mk_update m k v
+      | (Sym ("array-ext", _), [m1, m2]) => T.mk_array_ext m1 m2
       | (Sym ("pattern", _), _) => T.mk_true
       | (Sym (n, _), ts) =>
           (case Symtab.lookup ttab n of
diff -r cd7c98fdab80 -r 1d5ee19ef940 src/HOL/SMT/Tools/z3_proof_rules.ML
--- a/src/HOL/SMT/Tools/z3_proof_rules.ML	Fri Jan 22 16:33:44 2010 +0100
+++ b/src/HOL/SMT/Tools/z3_proof_rules.ML	Fri Jan 22 16:38:21 2010 +0100
@@ -669,6 +669,7 @@
 fun def_axiom ctxt ct =
   Thm (try_apply ctxt "def_axiom" [
     ("conj/disj", prove_def_axiom),
+    ("simp", by_tac (Simplifier.simp_tac HOL_ss)),
     ("fast", by_tac (Classical.fast_tac claset)),
     ("simp+fast", by_tac (Simplifier.simp_tac HOL_ss THEN_ALL_NEW
       Classical.fast_tac claset))] ct)
@@ -1157,9 +1158,14 @@
 (** theory lemmas: linear arithmetic, arrays **)
 local
   val array_ss = HOL_ss addsimps @{thms array_rules}
+  val array_pre_ss = HOL_ss addsimps @{thms apply_def array_ext_def}
   fun array_tac thms =
     Tactic.cut_facts_tac thms
-    THEN' Simplifier.asm_full_simp_tac array_ss
+    THEN' (Simplifier.asm_full_simp_tac array_pre_ss)
+    THEN' (SOLVED' (Simplifier.asm_full_simp_tac array_ss) ORELSE'
+      Tactic.rtac @{thm someI2_ex}
+      THEN_ALL_NEW (SOLVED' (Simplifier.asm_full_simp_tac array_ss) ORELSE'
+        Classical.fast_tac HOL_cs))
 
   fun full_arith_tac ctxt thms =
     Tactic.cut_facts_tac thms
@@ -1263,6 +1269,8 @@
 
   fun simp_tac thms = CHANGED o Simplifier.simp_tac (z3_simpset addsimps thms)
     ORELSE' Classical.best_tac HOL_cs
+  fun simp_arith_tac ctxt thms = Simplifier.simp_tac (z3_simpset addsimps thms)
+    THEN_ALL_NEW Arith_Data.arith_tac ctxt
 in
 fun rewrite ctxt thms ct =
   let val rules_net = Z3_Rewrite_Rules.get ctxt
@@ -1274,6 +1282,7 @@
       ("arith", by_tac' (arith_eq_tac ctxt)),
       ("classical", by_tac' (Classical.best_tac HOL_cs)),
       ("simp", by_tac' (simp_tac thms)),
+      ("simp+arith", by_tac' (simp_arith_tac ctxt thms)),
       ("full arith", by_tac' (Arith_Data.arith_tac ctxt))] (T.mk_prop ct))
   end
 end
diff -r cd7c98fdab80 -r 1d5ee19ef940 src/HOL/SMT/Tools/z3_proof_terms.ML
--- a/src/HOL/SMT/Tools/z3_proof_terms.ML	Fri Jan 22 16:33:44 2010 +0100
+++ b/src/HOL/SMT/Tools/z3_proof_terms.ML	Fri Jan 22 16:38:21 2010 +0100
@@ -36,6 +36,7 @@
 
   val mk_access: preterm -> preterm -> preterm
   val mk_update: preterm -> preterm -> preterm -> preterm
+  val mk_array_ext: preterm -> preterm -> preterm
 
   val mk_int_num: int -> preterm
   val mk_real_frac_num: int * int option -> preterm
@@ -195,6 +196,11 @@
   let val cTs = Thm.dest_ctyp (ctyp_of_preterm array)
   in mk_fun (instTs cTs update) [array, index, value] end
 
+val array_ext = mk_inst_pair (Thm.dest_ctyp o destT1) @{cpat array_ext}
+fun mk_array_ext a1 a2 =
+  let val cTs = Thm.dest_ctyp (ctyp_of_preterm a1)
+  in mk_fun (instTs cTs array_ext) [a1, a2] end
+
 
 fun mk_int_num i = mk_fun (Numeral.mk_cnumber @{ctyp int} i) []
 fun mk_real_num i = mk_fun (Numeral.mk_cnumber @{ctyp real} i) []