--- 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 *}
--- 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
--- 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
--- 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) []