handle let expressions inside terms by unfolding (instead of raising an exception),
authorboehmes
Thu Nov 05 15:24:49 2009 +0100 (2009-11-05)
changeset 33446153a27370a42
parent 33445 f0c78a28e18e
child 33447 6895b9cadc7c
handle let expressions inside terms by unfolding (instead of raising an exception),
added examples to test this feature
src/HOL/IsaMakefile
src/HOL/SMT/Examples/SMT_Examples.thy
src/HOL/SMT/Examples/cert/z3_linarith_17
src/HOL/SMT/Examples/cert/z3_linarith_17.proof
src/HOL/SMT/Examples/cert/z3_linarith_18
src/HOL/SMT/Examples/cert/z3_linarith_18.proof
src/HOL/SMT/Examples/cert/z3_linarith_19
src/HOL/SMT/Examples/cert/z3_linarith_19.proof
src/HOL/SMT/Examples/cert/z3_linarith_20
src/HOL/SMT/Examples/cert/z3_linarith_20.proof
src/HOL/SMT/Tools/smtlib_interface.ML
     1.1 --- a/src/HOL/IsaMakefile	Thu Nov 05 14:48:40 2009 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Thu Nov 05 15:24:49 2009 +0100
     1.3 @@ -1344,7 +1344,15 @@
     1.4    SMT/Examples/cert/z3_linarith_15					\
     1.5    SMT/Examples/cert/z3_linarith_15.proof				\
     1.6    SMT/Examples/cert/z3_linarith_16					\
     1.7 -  SMT/Examples/cert/z3_linarith_16.proof SMT/Examples/cert/z3_mono_01	\
     1.8 +  SMT/Examples/cert/z3_linarith_16.proof				\
     1.9 +  SMT/Examples/cert/z3_linarith_17					\
    1.10 +  SMT/Examples/cert/z3_linarith_17.proof				\
    1.11 +  SMT/Examples/cert/z3_linarith_18					\
    1.12 +  SMT/Examples/cert/z3_linarith_18.proof				\
    1.13 +  SMT/Examples/cert/z3_linarith_19					\
    1.14 +  SMT/Examples/cert/z3_linarith_19.proof				\
    1.15 +  SMT/Examples/cert/z3_linarith_20					\
    1.16 +  SMT/Examples/cert/z3_linarith_20.proof SMT/Examples/cert/z3_mono_01	\
    1.17    SMT/Examples/cert/z3_mono_01.proof SMT/Examples/cert/z3_mono_02	\
    1.18    SMT/Examples/cert/z3_mono_02.proof SMT/Examples/cert/z3_nat_arith_01	\
    1.19    SMT/Examples/cert/z3_nat_arith_01.proof				\
     2.1 --- a/src/HOL/SMT/Examples/SMT_Examples.thy	Thu Nov 05 14:48:40 2009 +0100
     2.2 +++ b/src/HOL/SMT/Examples/SMT_Examples.thy	Thu Nov 05 15:24:49 2009 +0100
     2.3 @@ -5,7 +5,7 @@
     2.4  header {* Examples for the 'smt' tactic. *}
     2.5  
     2.6  theory SMT_Examples
     2.7 -imports SMT
     2.8 +imports "../SMT"
     2.9  begin
    2.10  
    2.11  declare [[smt_solver=z3, z3_proofs=true]]
    2.12 @@ -390,6 +390,26 @@
    2.13    by smt
    2.14  
    2.15  
    2.16 +lemma "let P = 2 * x + 1 > x + (x::real) in P \<or> False \<or> P"
    2.17 +  using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_linarith_17"]]
    2.18 +  by smt
    2.19 +
    2.20 +lemma "x + (let y = x mod 2 in 2 * y + 1) \<ge> x + (1::int)"
    2.21 +  using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_linarith_18"]]
    2.22 +  by smt
    2.23 +
    2.24 +lemma "x + (let y = x mod 2 in y + y) < x + (3::int)"
    2.25 +  using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_linarith_19"]]
    2.26 +  by smt
    2.27 +
    2.28 +lemma 
    2.29 +  assumes "x \<noteq> (0::real)"
    2.30 +  shows "x + x \<noteq> (let P = (abs x > 1) in if P \<or> \<not>P then 4 else 2) * x"
    2.31 +  using assms
    2.32 +  using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_linarith_20"]]
    2.33 +  by smt
    2.34 +
    2.35 +
    2.36  subsection {* Linear arithmetic with quantifiers *}
    2.37  
    2.38  lemma "~ (\<exists>x::int. False)"
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/SMT/Examples/cert/z3_linarith_17	Thu Nov 05 15:24:49 2009 +0100
     3.3 @@ -0,0 +1,8 @@
     3.4 +(benchmark Isabelle
     3.5 +:extrasorts ( T1)
     3.6 +:extrafuns (
     3.7 +  (uf_1 Real)
     3.8 + )
     3.9 +:assumption (not (flet ($x1 (< (+ uf_1 uf_1) (+ (* 2.0 uf_1) 1.0))) (or $x1 (or false $x1))))
    3.10 +:formula true
    3.11 +)
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/SMT/Examples/cert/z3_linarith_17.proof	Thu Nov 05 15:24:49 2009 +0100
     4.3 @@ -0,0 +1,52 @@
     4.4 +#2 := false
     4.5 +#8 := 1::real
     4.6 +decl uf_1 :: real
     4.7 +#4 := uf_1
     4.8 +#6 := 2::real
     4.9 +#7 := (* 2::real uf_1)
    4.10 +#9 := (+ #7 1::real)
    4.11 +#5 := (+ uf_1 uf_1)
    4.12 +#10 := (< #5 #9)
    4.13 +#11 := (or false #10)
    4.14 +#12 := (or #10 #11)
    4.15 +#13 := (not #12)
    4.16 +#64 := (iff #13 false)
    4.17 +#32 := (+ 1::real #7)
    4.18 +#35 := (< #7 #32)
    4.19 +#52 := (not #35)
    4.20 +#62 := (iff #52 false)
    4.21 +#1 := true
    4.22 +#57 := (not true)
    4.23 +#60 := (iff #57 false)
    4.24 +#61 := [rewrite]: #60
    4.25 +#58 := (iff #52 #57)
    4.26 +#55 := (iff #35 true)
    4.27 +#56 := [rewrite]: #55
    4.28 +#59 := [monotonicity #56]: #58
    4.29 +#63 := [trans #59 #61]: #62
    4.30 +#53 := (iff #13 #52)
    4.31 +#50 := (iff #12 #35)
    4.32 +#45 := (or #35 #35)
    4.33 +#48 := (iff #45 #35)
    4.34 +#49 := [rewrite]: #48
    4.35 +#46 := (iff #12 #45)
    4.36 +#43 := (iff #11 #35)
    4.37 +#38 := (or false #35)
    4.38 +#41 := (iff #38 #35)
    4.39 +#42 := [rewrite]: #41
    4.40 +#39 := (iff #11 #38)
    4.41 +#36 := (iff #10 #35)
    4.42 +#33 := (= #9 #32)
    4.43 +#34 := [rewrite]: #33
    4.44 +#30 := (= #5 #7)
    4.45 +#31 := [rewrite]: #30
    4.46 +#37 := [monotonicity #31 #34]: #36
    4.47 +#40 := [monotonicity #37]: #39
    4.48 +#44 := [trans #40 #42]: #43
    4.49 +#47 := [monotonicity #37 #44]: #46
    4.50 +#51 := [trans #47 #49]: #50
    4.51 +#54 := [monotonicity #51]: #53
    4.52 +#65 := [trans #54 #63]: #64
    4.53 +#29 := [asserted]: #13
    4.54 +[mp #29 #65]: false
    4.55 +unsat
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/SMT/Examples/cert/z3_linarith_18	Thu Nov 05 15:24:49 2009 +0100
     5.3 @@ -0,0 +1,7 @@
     5.4 +(benchmark Isabelle
     5.5 +:extrafuns (
     5.6 +  (uf_1 Int)
     5.7 + )
     5.8 +:assumption (not (<= (+ uf_1 1) (+ uf_1 (+ (* 2 (mod uf_1 2)) 1))))
     5.9 +:formula true
    5.10 +)
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/SMT/Examples/cert/z3_linarith_18.proof	Thu Nov 05 15:24:49 2009 +0100
     6.3 @@ -0,0 +1,52 @@
     6.4 +#2 := false
     6.5 +#55 := 0::int
     6.6 +#7 := 2::int
     6.7 +decl uf_1 :: int
     6.8 +#4 := uf_1
     6.9 +#8 := (mod uf_1 2::int)
    6.10 +#9 := (* 2::int #8)
    6.11 +#56 := (>= #9 0::int)
    6.12 +#51 := (not #56)
    6.13 +#5 := 1::int
    6.14 +#10 := (+ #9 1::int)
    6.15 +#11 := (+ uf_1 #10)
    6.16 +#6 := (+ uf_1 1::int)
    6.17 +#12 := (<= #6 #11)
    6.18 +#13 := (not #12)
    6.19 +#58 := (iff #13 #51)
    6.20 +#39 := (+ uf_1 #9)
    6.21 +#40 := (+ 1::int #39)
    6.22 +#30 := (+ 1::int uf_1)
    6.23 +#45 := (<= #30 #40)
    6.24 +#48 := (not #45)
    6.25 +#52 := (iff #48 #51)
    6.26 +#53 := (iff #45 #56)
    6.27 +#54 := [rewrite]: #53
    6.28 +#57 := [monotonicity #54]: #52
    6.29 +#49 := (iff #13 #48)
    6.30 +#46 := (iff #12 #45)
    6.31 +#43 := (= #11 #40)
    6.32 +#33 := (+ 1::int #9)
    6.33 +#36 := (+ uf_1 #33)
    6.34 +#41 := (= #36 #40)
    6.35 +#42 := [rewrite]: #41
    6.36 +#37 := (= #11 #36)
    6.37 +#34 := (= #10 #33)
    6.38 +#35 := [rewrite]: #34
    6.39 +#38 := [monotonicity #35]: #37
    6.40 +#44 := [trans #38 #42]: #43
    6.41 +#31 := (= #6 #30)
    6.42 +#32 := [rewrite]: #31
    6.43 +#47 := [monotonicity #32 #44]: #46
    6.44 +#50 := [monotonicity #47]: #49
    6.45 +#59 := [trans #50 #57]: #58
    6.46 +#29 := [asserted]: #13
    6.47 +#60 := [mp #29 #59]: #51
    6.48 +#107 := (>= #8 0::int)
    6.49 +#1 := true
    6.50 +#28 := [true-axiom]: true
    6.51 +#135 := (or false #107)
    6.52 +#136 := [th-lemma]: #135
    6.53 +#137 := [unit-resolution #136 #28]: #107
    6.54 +[th-lemma #137 #60]: false
    6.55 +unsat
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/SMT/Examples/cert/z3_linarith_19	Thu Nov 05 15:24:49 2009 +0100
     7.3 @@ -0,0 +1,7 @@
     7.4 +(benchmark Isabelle
     7.5 +:extrafuns (
     7.6 +  (uf_1 Int)
     7.7 + )
     7.8 +:assumption (not (< (+ uf_1 (+ (mod uf_1 2) (mod uf_1 2))) (+ uf_1 3)))
     7.9 +:formula true
    7.10 +)
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/SMT/Examples/cert/z3_linarith_19.proof	Thu Nov 05 15:24:49 2009 +0100
     8.3 @@ -0,0 +1,50 @@
     8.4 +#2 := false
     8.5 +#5 := 2::int
     8.6 +decl uf_1 :: int
     8.7 +#4 := uf_1
     8.8 +#6 := (mod uf_1 2::int)
     8.9 +#122 := (>= #6 2::int)
    8.10 +#123 := (not #122)
    8.11 +#1 := true
    8.12 +#27 := [true-axiom]: true
    8.13 +#133 := (or false #123)
    8.14 +#134 := [th-lemma]: #133
    8.15 +#135 := [unit-resolution #134 #27]: #123
    8.16 +#9 := 3::int
    8.17 +#29 := (* 2::int #6)
    8.18 +#48 := (>= #29 3::int)
    8.19 +#10 := (+ uf_1 3::int)
    8.20 +#7 := (+ #6 #6)
    8.21 +#8 := (+ uf_1 #7)
    8.22 +#11 := (< #8 #10)
    8.23 +#12 := (not #11)
    8.24 +#55 := (iff #12 #48)
    8.25 +#35 := (+ 3::int uf_1)
    8.26 +#32 := (+ uf_1 #29)
    8.27 +#38 := (< #32 #35)
    8.28 +#41 := (not #38)
    8.29 +#53 := (iff #41 #48)
    8.30 +#46 := (not #48)
    8.31 +#45 := (not #46)
    8.32 +#51 := (iff #45 #48)
    8.33 +#52 := [rewrite]: #51
    8.34 +#49 := (iff #41 #45)
    8.35 +#47 := (iff #38 #46)
    8.36 +#44 := [rewrite]: #47
    8.37 +#50 := [monotonicity #44]: #49
    8.38 +#54 := [trans #50 #52]: #53
    8.39 +#42 := (iff #12 #41)
    8.40 +#39 := (iff #11 #38)
    8.41 +#36 := (= #10 #35)
    8.42 +#37 := [rewrite]: #36
    8.43 +#33 := (= #8 #32)
    8.44 +#30 := (= #7 #29)
    8.45 +#31 := [rewrite]: #30
    8.46 +#34 := [monotonicity #31]: #33
    8.47 +#40 := [monotonicity #34 #37]: #39
    8.48 +#43 := [monotonicity #40]: #42
    8.49 +#56 := [trans #43 #54]: #55
    8.50 +#28 := [asserted]: #12
    8.51 +#57 := [mp #28 #56]: #48
    8.52 +[th-lemma #57 #135]: false
    8.53 +unsat
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/SMT/Examples/cert/z3_linarith_20	Thu Nov 05 15:24:49 2009 +0100
     9.3 @@ -0,0 +1,9 @@
     9.4 +(benchmark Isabelle
     9.5 +:extrasorts ( T1)
     9.6 +:extrafuns (
     9.7 +  (uf_1 Real)
     9.8 + )
     9.9 +:assumption (not (= uf_1 0.0))
    9.10 +: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))))
    9.11 +:formula true
    9.12 +)
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/SMT/Examples/cert/z3_linarith_20.proof	Thu Nov 05 15:24:49 2009 +0100
    10.3 @@ -0,0 +1,118 @@
    10.4 +#2 := false
    10.5 +#5 := 0::real
    10.6 +decl uf_1 :: real
    10.7 +#4 := uf_1
    10.8 +#94 := (<= uf_1 0::real)
    10.9 +#17 := 2::real
   10.10 +#40 := (* 2::real uf_1)
   10.11 +#102 := (<= #40 0::real)
   10.12 +#103 := (>= #40 0::real)
   10.13 +#105 := (not #103)
   10.14 +#104 := (not #102)
   10.15 +#106 := (or #104 #105)
   10.16 +#107 := (not #106)
   10.17 +#88 := (= #40 0::real)
   10.18 +#108 := (iff #88 #107)
   10.19 +#109 := [rewrite]: #108
   10.20 +#16 := 4::real
   10.21 +#11 := (- uf_1)
   10.22 +#10 := (< uf_1 0::real)
   10.23 +#12 := (ite #10 #11 uf_1)
   10.24 +#9 := 1::real
   10.25 +#13 := (< 1::real #12)
   10.26 +#14 := (not #13)
   10.27 +#15 := (or #13 #14)
   10.28 +#18 := (ite #15 4::real 2::real)
   10.29 +#19 := (* #18 uf_1)
   10.30 +#8 := (+ uf_1 uf_1)
   10.31 +#20 := (= #8 #19)
   10.32 +#21 := (not #20)
   10.33 +#22 := (not #21)
   10.34 +#89 := (iff #22 #88)
   10.35 +#70 := (* 4::real uf_1)
   10.36 +#73 := (= #40 #70)
   10.37 +#86 := (iff #73 #88)
   10.38 +#87 := [rewrite]: #86
   10.39 +#84 := (iff #22 #73)
   10.40 +#76 := (not #73)
   10.41 +#79 := (not #76)
   10.42 +#82 := (iff #79 #73)
   10.43 +#83 := [rewrite]: #82
   10.44 +#80 := (iff #22 #79)
   10.45 +#77 := (iff #21 #76)
   10.46 +#74 := (iff #20 #73)
   10.47 +#71 := (= #19 #70)
   10.48 +#68 := (= #18 4::real)
   10.49 +#1 := true
   10.50 +#63 := (ite true 4::real 2::real)
   10.51 +#66 := (= #63 4::real)
   10.52 +#67 := [rewrite]: #66
   10.53 +#64 := (= #18 #63)
   10.54 +#61 := (iff #15 true)
   10.55 +#43 := -1::real
   10.56 +#44 := (* -1::real uf_1)
   10.57 +#47 := (ite #10 #44 uf_1)
   10.58 +#50 := (< 1::real #47)
   10.59 +#53 := (not #50)
   10.60 +#56 := (or #50 #53)
   10.61 +#59 := (iff #56 true)
   10.62 +#60 := [rewrite]: #59
   10.63 +#57 := (iff #15 #56)
   10.64 +#54 := (iff #14 #53)
   10.65 +#51 := (iff #13 #50)
   10.66 +#48 := (= #12 #47)
   10.67 +#45 := (= #11 #44)
   10.68 +#46 := [rewrite]: #45
   10.69 +#49 := [monotonicity #46]: #48
   10.70 +#52 := [monotonicity #49]: #51
   10.71 +#55 := [monotonicity #52]: #54
   10.72 +#58 := [monotonicity #52 #55]: #57
   10.73 +#62 := [trans #58 #60]: #61
   10.74 +#65 := [monotonicity #62]: #64
   10.75 +#69 := [trans #65 #67]: #68
   10.76 +#72 := [monotonicity #69]: #71
   10.77 +#41 := (= #8 #40)
   10.78 +#42 := [rewrite]: #41
   10.79 +#75 := [monotonicity #42 #72]: #74
   10.80 +#78 := [monotonicity #75]: #77
   10.81 +#81 := [monotonicity #78]: #80
   10.82 +#85 := [trans #81 #83]: #84
   10.83 +#90 := [trans #85 #87]: #89
   10.84 +#39 := [asserted]: #22
   10.85 +#91 := [mp #39 #90]: #88
   10.86 +#110 := [mp #91 #109]: #107
   10.87 +#111 := [not-or-elim #110]: #102
   10.88 +#127 := (or #94 #104)
   10.89 +#128 := [th-lemma]: #127
   10.90 +#129 := [unit-resolution #128 #111]: #94
   10.91 +#92 := (>= uf_1 0::real)
   10.92 +#112 := [not-or-elim #110]: #103
   10.93 +#130 := (or #92 #105)
   10.94 +#131 := [th-lemma]: #130
   10.95 +#132 := [unit-resolution #131 #112]: #92
   10.96 +#114 := (not #94)
   10.97 +#113 := (not #92)
   10.98 +#115 := (or #113 #114)
   10.99 +#95 := (and #92 #94)
  10.100 +#98 := (not #95)
  10.101 +#124 := (iff #98 #115)
  10.102 +#116 := (not #115)
  10.103 +#119 := (not #116)
  10.104 +#122 := (iff #119 #115)
  10.105 +#123 := [rewrite]: #122
  10.106 +#120 := (iff #98 #119)
  10.107 +#117 := (iff #95 #116)
  10.108 +#118 := [rewrite]: #117
  10.109 +#121 := [monotonicity #118]: #120
  10.110 +#125 := [trans #121 #123]: #124
  10.111 +#6 := (= uf_1 0::real)
  10.112 +#7 := (not #6)
  10.113 +#99 := (iff #7 #98)
  10.114 +#96 := (iff #6 #95)
  10.115 +#97 := [rewrite]: #96
  10.116 +#100 := [monotonicity #97]: #99
  10.117 +#38 := [asserted]: #7
  10.118 +#101 := [mp #38 #100]: #98
  10.119 +#126 := [mp #101 #125]: #115
  10.120 +[unit-resolution #126 #132 #129]: false
  10.121 +unsat
    11.1 --- a/src/HOL/SMT/Tools/smtlib_interface.ML	Thu Nov 05 14:48:40 2009 +0100
    11.2 +++ b/src/HOL/SMT/Tools/smtlib_interface.ML	Thu Nov 05 15:24:49 2009 +0100
    11.3 @@ -79,29 +79,39 @@
    11.4  val tvar = prefix "?"
    11.5  val fvar = prefix "$"
    11.6  
    11.7 +datatype lexpr =
    11.8 +  LVar of string |
    11.9 +  LTerm of lexpr list * (string, string) T.sterm
   11.10 +
   11.11  fun wr_expr loc env t =
   11.12    (case t of
   11.13 -    T.SVar i => wr1 (nth env i)
   11.14 +    T.SVar i =>
   11.15 +      (case nth env i of
   11.16 +        LVar name => wr1 name
   11.17 +      | LTerm (env', t') => wr_expr loc env' t')
   11.18    | T.SApp (n, ts) =>
   11.19        (case dest_marker t of
   11.20          SOME (loc', t') => wr_expr loc' env t'
   11.21        | NONE => wrn (wr_expr loc env) n ts)
   11.22    | T.SLet ((v, _), t1, t2) =>
   11.23 -      if loc then raise SMT_Solver.SMT "SMTLIB: let expression in term"
   11.24 +      if loc
   11.25 +      then
   11.26 +        let val (_, t1') = the (dest_marker t1)
   11.27 +        in wr_expr loc (LTerm (env, t1') :: env) t2 end
   11.28        else
   11.29          let
   11.30            val (loc', t1') = the (dest_marker t1)
   11.31            val (kind, v') = if loc' then ("let", tvar v)  else ("flet", fvar v)
   11.32          in
   11.33            par (wr kind #> par (wr v' #> wr_expr loc' env t1') #>
   11.34 -            wr_expr loc (v' :: env) t2)
   11.35 +            wr_expr loc (LVar v' :: env) t2)
   11.36          end
   11.37    | T.SQuant (q, vs, ps, b) =>
   11.38        let
   11.39          val wr_quant = wr o (fn T.SForall => "forall" | T.SExists => "exists")
   11.40          fun wr_var (n, s) = par (wr (tvar n) #> wr1 s)
   11.41  
   11.42 -        val wre = wr_expr loc (map (tvar o fst) (rev vs) @ env)
   11.43 +        val wre = wr_expr loc (map (LVar o tvar o fst) (rev vs) @ env)
   11.44  
   11.45          fun wrp s ts = wr1 (":" ^ s ^ " {") #> fold wre ts #> wr1 "}"
   11.46          fun wr_pat (T.SPat ts) = wrp "pat" ts