wneuper/isa: comparison src/HOL/SMT_Examples/SMT

equal deleted inserted replaced

-:04aeda922be2
+:e9b2782c4f99
 "(0::nat) div 3 = 0"
 "(1::nat) div 3 = 0"
 "(3::nat) div 3 = 1"
 "(x::nat) div 3 \<le> x"
 "(x div 3 = x) = (x = 0)"
+using [[z3_with_extensions]]
 by smt+
 lemma
 "(0::nat) mod 0 = 0"
 "(x::nat) mod 0 = x"
 "(0::nat) mod 3 = 0"
 "(1::nat) mod 3 = 1"
 "(3::nat) mod 3 = 0"
 "x mod 3 < 3"
 "(x mod 3 = x) = (x < 3)"
+using [[z3_with_extensions]]
 by smt+
 lemma
 "(x::nat) = x div 1 * 1 + x mod 1"
 "x = x div 3 * 3 + x mod 3"
+using [[z3_with_extensions]]
 by smt+
 lemma
 "min (x::nat) y \<le> x"
 "min x y \<le> y"
 "(-3::int) div 3 = -1"
 "(-5::int) div 3 = -2"
 "(-1::int) div -3 = 0"
 "(-3::int) div -3 = 1"
 "(-5::int) div -3 = 1"
+using [[z3_with_extensions]]
 by smt+
 lemma
 "(0::int) mod 0 = 0"
 "(x::int) mod 0 = x"
 "(-1::int) mod -3 = -1"
 "(-3::int) mod -3 = 0"
 "(-5::int) mod -3 = -2"
 "x mod 3 < 3"
 "(x mod 3 = x) \<longrightarrow> (x < 3)"
+using [[z3_with_extensions]]
 by smt+
 lemma
 "(x::int) = x div 1 * 1 + x mod 1"
 "x = x div 3 * 3 + x mod 3"
+using [[z3_with_extensions]]
 by smt+
 lemma
 "abs (x::int) \<ge> 0"
 "(abs x = 0) = (x = 0)"
 "(-1::real) / 3 = - 1 / 3"
 "(-1::real) / -3 = 1 / 3"
 "(x::real) / 1 = x"
 "x > 0 \<longrightarrow> x / 3 < x"
 "x < 0 \<longrightarrow> x / 3 > x"
+using [[z3_with_extensions]]
 by smt+
 lemma
 "(3::real) * (x / 3) = x"
 "(x * 3) / 3 = x"
 "x > 0 \<longrightarrow> 2 * x / 3 < x"
 "x < 0 \<longrightarrow> 2 * x / 3 > x"
+using [[z3_with_extensions]]
 by smt+
 lemma
 "abs (x::real) \<ge> 0"
 "(abs x = 0) = (x = 0)"
 "(fst (x, y) = snd (x, y)) = (x = y)"
 "p1 = (x, y) \<and> p2 = (y, x) \<longrightarrow> fst p1 = snd p2"
 "(fst (x, y) = snd (x, y)) = (x = y)"
 "(fst p = snd p) = (p = (snd p, fst p))"
 using fst_conv snd_conv pair_collapse
-using [[smt_datatypes, smt_oracle]]
+using [[smt_datatypes, smt_oracle, z3_with_extensions]]
 by smt+
 lemma
 "[x] \<noteq> Nil"
 "[x, y] \<noteq> Nil"
 "hd [x, y, z] = x"
 "tl [x, y, z] = [y, z]"
 "hd (tl [x, y, z]) = y"
 "tl (tl [x, y, z]) = [z]"
 using hd.simps tl.simps(2)
-using [[smt_datatypes, smt_oracle]]
+using [[smt_datatypes, smt_oracle, z3_with_extensions]]
 by smt+
 lemma
 "fst (hd [(a, b)]) = a"
 "snd (hd [(a, b)]) = b"
 using fst_conv snd_conv pair_collapse hd.simps tl.simps(2)
-using [[smt_datatypes, smt_oracle]]
+using [[smt_datatypes, smt_oracle, z3_with_extensions]]
 by smt+
 subsubsection {* Records *}
 "p1 = p2 \<longrightarrow> cx p1 = cx p2"
 "p1 = p2 \<longrightarrow> cy p1 = cy p2"
 "cx p1 \<noteq> cx p2 \<longrightarrow> p1 \<noteq> p2"
 "cy p1 \<noteq> cy p2 \<longrightarrow> p1 \<noteq> p2"
 using point.simps
-using [[smt_datatypes, smt_oracle]]
+using [[smt_datatypes, smt_oracle, z3_with_extensions]]
 using [[z3_options="AUTO_CONFIG=false"]]
 by smt+
 lemma
 "cx \<lparr> cx = 3, cy = 4 \<rparr> = 3"
 "\<lparr> cx = 3, cy = 4 \<rparr> \<lparr> cx := 5 \<rparr> = \<lparr> cx = 5, cy = 4 \<rparr>"
 "\<lparr> cx = 3, cy = 4 \<rparr> \<lparr> cy := 6 \<rparr> = \<lparr> cx = 3, cy = 6 \<rparr>"
 "p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p"
 "p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr> = p"
 using point.simps
-using [[smt_datatypes, smt_oracle]]
+using [[smt_datatypes, smt_oracle, z3_with_extensions]]
 using [[z3_options="AUTO_CONFIG=false"]]
 by smt+
 lemma
 "cy (p \<lparr> cx := a \<rparr>) = cy p"
 "cx (p \<lparr> cy := a \<rparr>) = cx p"
 "p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr>"
 using point.simps
-using [[smt_datatypes, smt_oracle]]
+using [[smt_datatypes, smt_oracle, z3_with_extensions]]
 using [[z3_options="AUTO_CONFIG=false"]]
 by smt+
 lemma
 "p1 = p2 \<longrightarrow> cx p1 = cx p2"
 "p1 = p2 \<longrightarrow> black p1 = black p2"
 "cx p1 \<noteq> cx p2 \<longrightarrow> p1 \<noteq> p2"
 "cy p1 \<noteq> cy p2 \<longrightarrow> p1 \<noteq> p2"
 "black p1 \<noteq> black p2 \<longrightarrow> p1 \<noteq> p2"
 using point.simps bw_point.simps
-using [[smt_datatypes, smt_oracle]]
+using [[smt_datatypes, smt_oracle, z3_with_extensions]]
 by smt+
 lemma
 "cx \<lparr> cx = 3, cy = 4, black = b \<rparr> = 3"
 "cy \<lparr> cx = 3, cy = 4, black = b \<rparr> = 4"
 "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
 p \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> = p"
 "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
 p \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p"
 using point.simps bw_point.simps
-using [[smt_datatypes, smt_oracle]]
+using [[smt_datatypes, smt_oracle, z3_with_extensions]]
 using [[z3_options="AUTO_CONFIG=false"]]
 by smt+
 lemma
 "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> cx = 3, cy = 4, black = w \<rparr>"
 lemma
 "p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> =
 p \<lparr> black := True \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr>"
 using point.simps bw_point.simps
-using [[smt_datatypes, smt_oracle]]
+using [[smt_datatypes, smt_oracle, z3_with_extensions]]
 using [[z3_options="AUTO_CONFIG=false"]]
 by smt
 subsubsection {* Type definitions *}
 "n2 = n2"
 "n1 \<noteq> n2"
 "nplus n1 n1 = n2"
 "nplus n1 n2 = n3"
 using n1_def n2_def n3_def nplus_def
-using [[smt_datatypes, smt_oracle]]
+using [[smt_datatypes, smt_oracle, z3_with_extensions]]
 using [[z3_options="AUTO_CONFIG=false"]]
 by smt+

changeset 49084	e9b2782c4f99
parent 48026	ade3fc826af3
child 50849	b27bbb021df1