# HG changeset patch
# User boehmes
# Date 1257431089 -3600
# Node ID 153a27370a4214f2be6e9e0098c152327817798f
# Parent  f0c78a28e18e52d9532e90521a711d668c4a5958
handle let expressions inside terms by unfolding (instead of raising an exception),
added examples to test this feature

diff -r f0c78a28e18e -r 153a27370a42 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Nov 05 14:48:40 2009 +0100
+++ b/src/HOL/IsaMakefile	Thu Nov 05 15:24:49 2009 +0100
@@ -1344,7 +1344,15 @@
   SMT/Examples/cert/z3_linarith_15					\
   SMT/Examples/cert/z3_linarith_15.proof				\
   SMT/Examples/cert/z3_linarith_16					\
-  SMT/Examples/cert/z3_linarith_16.proof SMT/Examples/cert/z3_mono_01	\
+  SMT/Examples/cert/z3_linarith_16.proof				\
+  SMT/Examples/cert/z3_linarith_17					\
+  SMT/Examples/cert/z3_linarith_17.proof				\
+  SMT/Examples/cert/z3_linarith_18					\
+  SMT/Examples/cert/z3_linarith_18.proof				\
+  SMT/Examples/cert/z3_linarith_19					\
+  SMT/Examples/cert/z3_linarith_19.proof				\
+  SMT/Examples/cert/z3_linarith_20					\
+  SMT/Examples/cert/z3_linarith_20.proof SMT/Examples/cert/z3_mono_01	\
   SMT/Examples/cert/z3_mono_01.proof SMT/Examples/cert/z3_mono_02	\
   SMT/Examples/cert/z3_mono_02.proof SMT/Examples/cert/z3_nat_arith_01	\
   SMT/Examples/cert/z3_nat_arith_01.proof				\
diff -r f0c78a28e18e -r 153a27370a42 src/HOL/SMT/Examples/SMT_Examples.thy
--- a/src/HOL/SMT/Examples/SMT_Examples.thy	Thu Nov 05 14:48:40 2009 +0100
+++ b/src/HOL/SMT/Examples/SMT_Examples.thy	Thu Nov 05 15:24:49 2009 +0100
@@ -5,7 +5,7 @@
 header {* Examples for the 'smt' tactic. *}
 
 theory SMT_Examples
-imports SMT
+imports "../SMT"
 begin
 
 declare [[smt_solver=z3, z3_proofs=true]]
@@ -390,6 +390,26 @@
   by smt
 
 
+lemma "let P = 2 * x + 1 > x + (x::real) in P \<or> False \<or> P"
+  using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_linarith_17"]]
+  by smt
+
+lemma "x + (let y = x mod 2 in 2 * y + 1) \<ge> x + (1::int)"
+  using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_linarith_18"]]
+  by smt
+
+lemma "x + (let y = x mod 2 in y + y) < x + (3::int)"
+  using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_linarith_19"]]
+  by smt
+
+lemma 
+  assumes "x \<noteq> (0::real)"
+  shows "x + x \<noteq> (let P = (abs x > 1) in if P \<or> \<not>P then 4 else 2) * x"
+  using assms
+  using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_linarith_20"]]
+  by smt
+
+
 subsection {* Linear arithmetic with quantifiers *}
 
 lemma "~ (\<exists>x::int. False)"
diff -r f0c78a28e18e -r 153a27370a42 src/HOL/SMT/Examples/cert/z3_linarith_17
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_linarith_17	Thu Nov 05 15:24:49 2009 +0100
@@ -0,0 +1,8 @@
+(benchmark Isabelle
+:extrasorts ( T1)
+:extrafuns (
+  (uf_1 Real)
+ )
+:assumption (not (flet ($x1 (< (+ uf_1 uf_1) (+ (* 2.0 uf_1) 1.0))) (or $x1 (or false $x1))))
+:formula true
+)
diff -r f0c78a28e18e -r 153a27370a42 src/HOL/SMT/Examples/cert/z3_linarith_17.proof
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_linarith_17.proof	Thu Nov 05 15:24:49 2009 +0100
@@ -0,0 +1,52 @@
+#2 := false
+#8 := 1::real
+decl uf_1 :: real
+#4 := uf_1
+#6 := 2::real
+#7 := (* 2::real uf_1)
+#9 := (+ #7 1::real)
+#5 := (+ uf_1 uf_1)
+#10 := (< #5 #9)
+#11 := (or false #10)
+#12 := (or #10 #11)
+#13 := (not #12)
+#64 := (iff #13 false)
+#32 := (+ 1::real #7)
+#35 := (< #7 #32)
+#52 := (not #35)
+#62 := (iff #52 false)
+#1 := true
+#57 := (not true)
+#60 := (iff #57 false)
+#61 := [rewrite]: #60
+#58 := (iff #52 #57)
+#55 := (iff #35 true)
+#56 := [rewrite]: #55
+#59 := [monotonicity #56]: #58
+#63 := [trans #59 #61]: #62
+#53 := (iff #13 #52)
+#50 := (iff #12 #35)
+#45 := (or #35 #35)
+#48 := (iff #45 #35)
+#49 := [rewrite]: #48
+#46 := (iff #12 #45)
+#43 := (iff #11 #35)
+#38 := (or false #35)
+#41 := (iff #38 #35)
+#42 := [rewrite]: #41
+#39 := (iff #11 #38)
+#36 := (iff #10 #35)
+#33 := (= #9 #32)
+#34 := [rewrite]: #33
+#30 := (= #5 #7)
+#31 := [rewrite]: #30
+#37 := [monotonicity #31 #34]: #36
+#40 := [monotonicity #37]: #39
+#44 := [trans #40 #42]: #43
+#47 := [monotonicity #37 #44]: #46
+#51 := [trans #47 #49]: #50
+#54 := [monotonicity #51]: #53
+#65 := [trans #54 #63]: #64
+#29 := [asserted]: #13
+[mp #29 #65]: false
+unsat
diff -r f0c78a28e18e -r 153a27370a42 src/HOL/SMT/Examples/cert/z3_linarith_18
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_linarith_18	Thu Nov 05 15:24:49 2009 +0100
@@ -0,0 +1,7 @@
+(benchmark Isabelle
+:extrafuns (
+  (uf_1 Int)
+ )
+:assumption (not (<= (+ uf_1 1) (+ uf_1 (+ (* 2 (mod uf_1 2)) 1))))
+:formula true
+)
diff -r f0c78a28e18e -r 153a27370a42 src/HOL/SMT/Examples/cert/z3_linarith_18.proof
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_linarith_18.proof	Thu Nov 05 15:24:49 2009 +0100
@@ -0,0 +1,52 @@
+#2 := false
+#55 := 0::int
+#7 := 2::int
+decl uf_1 :: int
+#4 := uf_1
+#8 := (mod uf_1 2::int)
+#9 := (* 2::int #8)
+#56 := (>= #9 0::int)
+#51 := (not #56)
+#5 := 1::int
+#10 := (+ #9 1::int)
+#11 := (+ uf_1 #10)
+#6 := (+ uf_1 1::int)
+#12 := (<= #6 #11)
+#13 := (not #12)
+#58 := (iff #13 #51)
+#39 := (+ uf_1 #9)
+#40 := (+ 1::int #39)
+#30 := (+ 1::int uf_1)
+#45 := (<= #30 #40)
+#48 := (not #45)
+#52 := (iff #48 #51)
+#53 := (iff #45 #56)
+#54 := [rewrite]: #53
+#57 := [monotonicity #54]: #52
+#49 := (iff #13 #48)
+#46 := (iff #12 #45)
+#43 := (= #11 #40)
+#33 := (+ 1::int #9)
+#36 := (+ uf_1 #33)
+#41 := (= #36 #40)
+#42 := [rewrite]: #41
+#37 := (= #11 #36)
+#34 := (= #10 #33)
+#35 := [rewrite]: #34
+#38 := [monotonicity #35]: #37
+#44 := [trans #38 #42]: #43
+#31 := (= #6 #30)
+#32 := [rewrite]: #31
+#47 := [monotonicity #32 #44]: #46
+#50 := [monotonicity #47]: #49
+#59 := [trans #50 #57]: #58
+#29 := [asserted]: #13
+#60 := [mp #29 #59]: #51
+#107 := (>= #8 0::int)
+#1 := true
+#28 := [true-axiom]: true
+#135 := (or false #107)
+#136 := [th-lemma]: #135
+#137 := [unit-resolution #136 #28]: #107
+[th-lemma #137 #60]: false
+unsat
diff -r f0c78a28e18e -r 153a27370a42 src/HOL/SMT/Examples/cert/z3_linarith_19
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_linarith_19	Thu Nov 05 15:24:49 2009 +0100
@@ -0,0 +1,7 @@
+(benchmark Isabelle
+:extrafuns (
+  (uf_1 Int)
+ )
+:assumption (not (< (+ uf_1 (+ (mod uf_1 2) (mod uf_1 2))) (+ uf_1 3)))
+:formula true
+)
diff -r f0c78a28e18e -r 153a27370a42 src/HOL/SMT/Examples/cert/z3_linarith_19.proof
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_linarith_19.proof	Thu Nov 05 15:24:49 2009 +0100
@@ -0,0 +1,50 @@
+#2 := false
+#5 := 2::int
+decl uf_1 :: int
+#4 := uf_1
+#6 := (mod uf_1 2::int)
+#122 := (>= #6 2::int)
+#123 := (not #122)
+#1 := true
+#27 := [true-axiom]: true
+#133 := (or false #123)
+#134 := [th-lemma]: #133
+#135 := [unit-resolution #134 #27]: #123
+#9 := 3::int
+#29 := (* 2::int #6)
+#48 := (>= #29 3::int)
+#10 := (+ uf_1 3::int)
+#7 := (+ #6 #6)
+#8 := (+ uf_1 #7)
+#11 := (< #8 #10)
+#12 := (not #11)
+#55 := (iff #12 #48)
+#35 := (+ 3::int uf_1)
+#32 := (+ uf_1 #29)
+#38 := (< #32 #35)
+#41 := (not #38)
+#53 := (iff #41 #48)
+#46 := (not #48)
+#45 := (not #46)
+#51 := (iff #45 #48)
+#52 := [rewrite]: #51
+#49 := (iff #41 #45)
+#47 := (iff #38 #46)
+#44 := [rewrite]: #47
+#50 := [monotonicity #44]: #49
+#54 := [trans #50 #52]: #53
+#42 := (iff #12 #41)
+#39 := (iff #11 #38)
+#36 := (= #10 #35)
+#37 := [rewrite]: #36
+#33 := (= #8 #32)
+#30 := (= #7 #29)
+#31 := [rewrite]: #30
+#34 := [monotonicity #31]: #33
+#40 := [monotonicity #34 #37]: #39
+#43 := [monotonicity #40]: #42
+#56 := [trans #43 #54]: #55
+#28 := [asserted]: #12
+#57 := [mp #28 #56]: #48
+[th-lemma #57 #135]: false
+unsat
diff -r f0c78a28e18e -r 153a27370a42 src/HOL/SMT/Examples/cert/z3_linarith_20
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_linarith_20	Thu Nov 05 15:24:49 2009 +0100
@@ -0,0 +1,9 @@
+(benchmark Isabelle
+:extrasorts ( T1)
+:extrafuns (
+  (uf_1 Real)
+ )
+:assumption (not (= uf_1 0.0))
+:assumption (not (not (= (+ uf_1 uf_1) (* (ite (or (< 1.0 (ite (< uf_1 0.0) (~ uf_1) uf_1)) (not (< 1.0 (ite (< uf_1 0.0) (~ uf_1) uf_1)))) 4.0 2.0) uf_1))))
+:formula true
+)
diff -r f0c78a28e18e -r 153a27370a42 src/HOL/SMT/Examples/cert/z3_linarith_20.proof
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_linarith_20.proof	Thu Nov 05 15:24:49 2009 +0100
@@ -0,0 +1,118 @@
+#2 := false
+#5 := 0::real
+decl uf_1 :: real
+#4 := uf_1
+#94 := (<= uf_1 0::real)
+#17 := 2::real
+#40 := (* 2::real uf_1)
+#102 := (<= #40 0::real)
+#103 := (>= #40 0::real)
+#105 := (not #103)
+#104 := (not #102)
+#106 := (or #104 #105)
+#107 := (not #106)
+#88 := (= #40 0::real)
+#108 := (iff #88 #107)
+#109 := [rewrite]: #108
+#16 := 4::real
+#11 := (- uf_1)
+#10 := (< uf_1 0::real)
+#12 := (ite #10 #11 uf_1)
+#9 := 1::real
+#13 := (< 1::real #12)
+#14 := (not #13)
+#15 := (or #13 #14)
+#18 := (ite #15 4::real 2::real)
+#19 := (* #18 uf_1)
+#8 := (+ uf_1 uf_1)
+#20 := (= #8 #19)
+#21 := (not #20)
+#22 := (not #21)
+#89 := (iff #22 #88)
+#70 := (* 4::real uf_1)
+#73 := (= #40 #70)
+#86 := (iff #73 #88)
+#87 := [rewrite]: #86
+#84 := (iff #22 #73)
+#76 := (not #73)
+#79 := (not #76)
+#82 := (iff #79 #73)
+#83 := [rewrite]: #82
+#80 := (iff #22 #79)
+#77 := (iff #21 #76)
+#74 := (iff #20 #73)
+#71 := (= #19 #70)
+#68 := (= #18 4::real)
+#1 := true
+#63 := (ite true 4::real 2::real)
+#66 := (= #63 4::real)
+#67 := [rewrite]: #66
+#64 := (= #18 #63)
+#61 := (iff #15 true)
+#43 := -1::real
+#44 := (* -1::real uf_1)
+#47 := (ite #10 #44 uf_1)
+#50 := (< 1::real #47)
+#53 := (not #50)
+#56 := (or #50 #53)
+#59 := (iff #56 true)
+#60 := [rewrite]: #59
+#57 := (iff #15 #56)
+#54 := (iff #14 #53)
+#51 := (iff #13 #50)
+#48 := (= #12 #47)
+#45 := (= #11 #44)
+#46 := [rewrite]: #45
+#49 := [monotonicity #46]: #48
+#52 := [monotonicity #49]: #51
+#55 := [monotonicity #52]: #54
+#58 := [monotonicity #52 #55]: #57
+#62 := [trans #58 #60]: #61
+#65 := [monotonicity #62]: #64
+#69 := [trans #65 #67]: #68
+#72 := [monotonicity #69]: #71
+#41 := (= #8 #40)
+#42 := [rewrite]: #41
+#75 := [monotonicity #42 #72]: #74
+#78 := [monotonicity #75]: #77
+#81 := [monotonicity #78]: #80
+#85 := [trans #81 #83]: #84
+#90 := [trans #85 #87]: #89
+#39 := [asserted]: #22
+#91 := [mp #39 #90]: #88
+#110 := [mp #91 #109]: #107
+#111 := [not-or-elim #110]: #102
+#127 := (or #94 #104)
+#128 := [th-lemma]: #127
+#129 := [unit-resolution #128 #111]: #94
+#92 := (>= uf_1 0::real)
+#112 := [not-or-elim #110]: #103
+#130 := (or #92 #105)
+#131 := [th-lemma]: #130
+#132 := [unit-resolution #131 #112]: #92
+#114 := (not #94)
+#113 := (not #92)
+#115 := (or #113 #114)
+#95 := (and #92 #94)
+#98 := (not #95)
+#124 := (iff #98 #115)
+#116 := (not #115)
+#119 := (not #116)
+#122 := (iff #119 #115)
+#123 := [rewrite]: #122
+#120 := (iff #98 #119)
+#117 := (iff #95 #116)
+#118 := [rewrite]: #117
+#121 := [monotonicity #118]: #120
+#125 := [trans #121 #123]: #124
+#6 := (= uf_1 0::real)
+#7 := (not #6)
+#99 := (iff #7 #98)
+#96 := (iff #6 #95)
+#97 := [rewrite]: #96
+#100 := [monotonicity #97]: #99
+#38 := [asserted]: #7
+#101 := [mp #38 #100]: #98
+#126 := [mp #101 #125]: #115
+[unit-resolution #126 #132 #129]: false
+unsat
diff -r f0c78a28e18e -r 153a27370a42 src/HOL/SMT/Tools/smtlib_interface.ML
--- a/src/HOL/SMT/Tools/smtlib_interface.ML	Thu Nov 05 14:48:40 2009 +0100
+++ b/src/HOL/SMT/Tools/smtlib_interface.ML	Thu Nov 05 15:24:49 2009 +0100
@@ -79,29 +79,39 @@
 val tvar = prefix "?"
 val fvar = prefix "$"
 
+datatype lexpr =
+  LVar of string |
+  LTerm of lexpr list * (string, string) T.sterm
+
 fun wr_expr loc env t =
   (case t of
-    T.SVar i => wr1 (nth env i)
+    T.SVar i =>
+      (case nth env i of
+        LVar name => wr1 name
+      | LTerm (env', t') => wr_expr loc env' t')
   | T.SApp (n, ts) =>
       (case dest_marker t of
         SOME (loc', t') => wr_expr loc' env t'
       | NONE => wrn (wr_expr loc env) n ts)
   | T.SLet ((v, _), t1, t2) =>
-      if loc then raise SMT_Solver.SMT "SMTLIB: let expression in term"
+      if loc
+      then
+        let val (_, t1') = the (dest_marker t1)
+        in wr_expr loc (LTerm (env, t1') :: env) t2 end
       else
         let
           val (loc', t1') = the (dest_marker t1)
           val (kind, v') = if loc' then ("let", tvar v)  else ("flet", fvar v)
         in
           par (wr kind #> par (wr v' #> wr_expr loc' env t1') #>
-            wr_expr loc (v' :: env) t2)
+            wr_expr loc (LVar v' :: env) t2)
         end
   | T.SQuant (q, vs, ps, b) =>
       let
         val wr_quant = wr o (fn T.SForall => "forall" | T.SExists => "exists")
         fun wr_var (n, s) = par (wr (tvar n) #> wr1 s)
 
-        val wre = wr_expr loc (map (tvar o fst) (rev vs) @ env)
+        val wre = wr_expr loc (map (LVar o tvar o fst) (rev vs) @ env)
 
         fun wrp s ts = wr1 (":" ^ s ^ " {") #> fold wre ts #> wr1 "}"
         fun wr_pat (T.SPat ts) = wrp "pat" ts