src/HOL/SMT_Examples/SMT_Tests.thy
changeset 56727 75f4fdafb285
parent 56112 040424c3800d
child 56819 ad1bbed53788
equal deleted inserted replaced
56726:9fba10c97aef 56727:75f4fdafb285
   125   "\<exists>x. P x \<longrightarrow> (\<exists>y. P x \<and> P y)"
   125   "\<exists>x. P x \<longrightarrow> (\<exists>y. P x \<and> P y)"
   126   "(\<exists>x. P x) \<or> R \<longleftrightarrow> (\<exists>x. P x \<or> R)"
   126   "(\<exists>x. P x) \<or> R \<longleftrightarrow> (\<exists>x. P x \<or> R)"
   127   "\<exists>x. P x \<longrightarrow> P a \<and> P b"
   127   "\<exists>x. P x \<longrightarrow> P a \<and> P b"
   128   "\<exists>x. (\<exists>y. P y) \<longrightarrow> P x"
   128   "\<exists>x. (\<exists>y. P y) \<longrightarrow> P x"
   129   "(\<exists>x. Q \<longrightarrow> P x) \<longleftrightarrow> (Q \<longrightarrow> (\<exists>x. P x))"
   129   "(\<exists>x. Q \<longrightarrow> P x) \<longleftrightarrow> (Q \<longrightarrow> (\<exists>x. P x))"
   130   oops (* smt2 FIXME: requires Z3 4.3.1 *)
   130   by smt2+
   131 
   131 
   132 lemma
   132 lemma
   133   "(\<not>(\<exists>x. P x)) \<longleftrightarrow> (\<forall>x. \<not> P x)"
   133   "(\<not>(\<exists>x. P x)) \<longleftrightarrow> (\<forall>x. \<not> P x)"
   134   "(\<exists>x. P x \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P x) \<longrightarrow> Q"
   134   "(\<exists>x. P x \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P x) \<longrightarrow> Q"
   135   "(\<forall>x y. R x y = x) \<longrightarrow> (\<exists>y. R x y) = R x c"
   135   "(\<forall>x y. R x y = x) \<longrightarrow> (\<exists>y. R x y) = R x c"
   136   "(if P x then \<not>(\<exists>y. P y) else (\<forall>y. \<not>P y)) \<longrightarrow> P x \<longrightarrow> P y"
   136   "(if P x then \<not>(\<exists>y. P y) else (\<forall>y. \<not>P y)) \<longrightarrow> P x \<longrightarrow> P y"
   137   "(\<forall>x y. R x y = x) \<and> (\<forall>x. \<exists>y. R x y) = (\<forall>x. R x c) \<longrightarrow> (\<exists>y. R x y) = R x c"
   137   "(\<forall>x y. R x y = x) \<and> (\<forall>x. \<exists>y. R x y) = (\<forall>x. R x c) \<longrightarrow> (\<exists>y. R x y) = R x c"
   138   by smt+ (* smt2 FIXME: Option *)
   138   by smt2+
   139 
   139 
   140 lemma
   140 lemma
   141   "\<forall>x. \<exists>y. f x y = f x (g x)"
   141   "\<forall>x. \<exists>y. f x y = f x (g x)"
   142   "(\<not>\<not>(\<exists>x. P x)) \<longleftrightarrow> (\<not>(\<forall>x. \<not> P x))"
   142   "(\<not>\<not>(\<exists>x. P x)) \<longleftrightarrow> (\<not>(\<forall>x. \<not> P x))"
   143   "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)"
   143   "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)"
   144   "\<exists>x. if x = y then (\<forall>y. y = x \<or> y \<noteq> x) else (\<forall>y. y = (x, x) \<or> y \<noteq> (x, x))"
   144   "\<exists>x. if x = y then (\<forall>y. y = x \<or> y \<noteq> x) else (\<forall>y. y = (x, x) \<or> y \<noteq> (x, x))"
   145   "\<exists>x. if x = y then (\<exists>y. y = x \<or> y \<noteq> x) else (\<exists>y. y = (x, x) \<or> y \<noteq> (x, x))"
   145   "\<exists>x. if x = y then (\<exists>y. y = x \<or> y \<noteq> x) else (\<exists>y. y = (x, x) \<or> y \<noteq> (x, x))"
   146   "(\<exists>x. \<forall>y. P x \<longleftrightarrow> P y) \<longrightarrow> ((\<exists>x. P x) \<longleftrightarrow> (\<forall>y. P y))"
   146   "(\<exists>x. \<forall>y. P x \<longleftrightarrow> P y) \<longrightarrow> ((\<exists>x. P x) \<longleftrightarrow> (\<forall>y. P y))"
   147   "\<exists>z. P z \<longrightarrow> (\<forall>x. P x)"
   147   "\<exists>z. P z \<longrightarrow> (\<forall>x. P x)"
   148   "(\<exists>y. \<forall>x. R x y) \<longrightarrow> (\<forall>x. \<exists>y. R x y)"
   148   "(\<exists>y. \<forall>x. R x y) \<longrightarrow> (\<forall>x. \<exists>y. R x y)"
   149   by smt+ (* smt2 FIXME: requires Z3 4.3.1 *)
   149   by smt2+
   150 
   150 
   151 lemma
   151 lemma
   152   "(\<exists>!x. P x) \<longrightarrow> (\<exists>x. P x)"
   152   "(\<exists>!x. P x) \<longrightarrow> (\<exists>x. P x)"
   153   "(\<exists>!x. P x) \<longleftrightarrow> (\<exists>x. P x \<and> (\<forall>y. y \<noteq> x \<longrightarrow> \<not>P y))"
   153   "(\<exists>!x. P x) \<longleftrightarrow> (\<exists>x. P x \<and> (\<forall>y. y \<noteq> x \<longrightarrow> \<not>P y))"
   154   "P a \<longrightarrow> (\<forall>x. P x \<longrightarrow> x = a) \<longrightarrow> (\<exists>!x. P x)"
   154   "P a \<longrightarrow> (\<forall>x. P x \<longrightarrow> x = a) \<longrightarrow> (\<exists>!x. P x)"
   172   "let P = (\<forall>x. Q x) in if P then P else \<not>P"
   172   "let P = (\<forall>x. Q x) in if P then P else \<not>P"
   173   by smt2+
   173   by smt2+
   174 
   174 
   175 lemma
   175 lemma
   176   "a \<noteq> b \<and> a \<noteq> c \<and> b \<noteq> c \<and> (\<forall>x y. f x = f y \<longrightarrow> y = x) \<longrightarrow> f a \<noteq> f b"
   176   "a \<noteq> b \<and> a \<noteq> c \<and> b \<noteq> c \<and> (\<forall>x y. f x = f y \<longrightarrow> y = x) \<longrightarrow> f a \<noteq> f b"
       
   177   using [[smt2_oracle=true]] (* FIXME: disable refine_inj_axiom in Z3 *)
   177   by smt2
   178   by smt2
   178 
   179 
   179 lemma
   180 lemma
   180   "(\<forall>x y z. f x y = f x z \<longrightarrow> y = z) \<and> b \<noteq> c \<longrightarrow> f a b \<noteq> f a c"
   181   "(\<forall>x y z. f x y = f x z \<longrightarrow> y = z) \<and> b \<noteq> c \<longrightarrow> f a b \<noteq> f a c"
   181   "(\<forall>x y z. f x y = f z y \<longrightarrow> x = z) \<and> a \<noteq> d \<longrightarrow> f a b \<noteq> f d b"
   182   "(\<forall>x y z. f x y = f z y \<longrightarrow> x = z) \<and> a \<noteq> d \<longrightarrow> f a b \<noteq> f d b"
       
   183   using [[smt2_oracle=true]] (* FIXME: disable refine_inj_axiom in Z3 *)
   182   by smt2+
   184   by smt2+
   183 
   185 
   184 
   186 
   185 section {* Guidance for quantifier heuristics: patterns and weights *}
   187 section {* Guidance for quantifier heuristics: patterns and weights *}
   186 
   188 
   246   "x \<equiv> y \<Longrightarrow> (f x :: 'b::type) \<equiv> f y"
   248   "x \<equiv> y \<Longrightarrow> (f x :: 'b::type) \<equiv> f y"
   247   "(\<And>x. g x) \<Longrightarrow> g a \<or> a"
   249   "(\<And>x. g x) \<Longrightarrow> g a \<or> a"
   248   "(\<And>x y. h x y \<and> h y x) \<Longrightarrow> \<forall>x. h x x"
   250   "(\<And>x y. h x y \<and> h y x) \<Longrightarrow> \<forall>x. h x x"
   249   "(p \<or> q) \<and> \<not>p \<Longrightarrow> q"
   251   "(p \<or> q) \<and> \<not>p \<Longrightarrow> q"
   250   "(a \<and> b) \<or> (c \<and> d) \<Longrightarrow> (a \<and> b) \<or> (c \<and> d)"
   252   "(a \<and> b) \<or> (c \<and> d) \<Longrightarrow> (a \<and> b) \<or> (c \<and> d)"
   251   by smt+ (* smt2 FIXME: Option *)
   253   by smt2+
   252 
   254 
   253 
   255 
   254 section {* Natural numbers *}
   256 section {* Natural numbers *}
   255 
   257 
   256 lemma
   258 lemma
   727   "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
   729   "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
   728      p \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> = p"
   730      p \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> = p"
   729   "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
   731   "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
   730      p \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p"
   732      p \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p"
   731   using point.simps bw_point.simps
   733   using point.simps bw_point.simps
   732   by smt+ (* smt2 FIXME: Option *)
   734   by smt2+
   733 
   735 
   734 lemma
   736 lemma
   735   "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> cx = 3, cy = 4, black = w \<rparr>"
   737   "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> cx = 3, cy = 4, black = w \<rparr>"
   736   "\<lparr> cx = 3, cy = 4, black = True \<rparr> \<lparr> black := False \<rparr> =
   738   "\<lparr> cx = 3, cy = 4, black = True \<rparr> \<lparr> black := False \<rparr> =
   737      \<lparr> cx = 3, cy = 4, black = False \<rparr>"
   739      \<lparr> cx = 3, cy = 4, black = False \<rparr>"
   905   "i1 = i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v2"
   907   "i1 = i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v2"
   906   "i1 = i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v2"
   908   "i1 = i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v2"
   907   "i1 \<noteq> i2 \<and>i1 \<noteq> i3 \<and>  i2 \<noteq> i3 \<longrightarrow> (f (i1 := v1, i2 := v2)) i3 = f i3"
   909   "i1 \<noteq> i2 \<and>i1 \<noteq> i3 \<and>  i2 \<noteq> i3 \<longrightarrow> (f (i1 := v1, i2 := v2)) i3 = f i3"
   908   using fun_upd_same fun_upd_apply
   910   using fun_upd_same fun_upd_apply
   909   by smt2+
   911   by smt2+
   910 
       
   911 
   912 
   912 
   913 
   913 section {* Sets *}
   914 section {* Sets *}
   914 
   915 
   915 lemma Empty: "x \<notin> {}" by simp
   916 lemma Empty: "x \<notin> {}" by simp