src/HOL/SMT_Examples/SMT_Tests.thy
changeset 56859 bc50d5e04e90
parent 56819 ad1bbed53788
child 57165 7b1bf424ec5f
equal deleted inserted replaced
56858:0c3d0bc98abe 56859:bc50d5e04e90
   729   "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
   729   "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
   730      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"
   731   "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
   731   "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
   732      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"
   733   using point.simps bw_point.simps
   733   using point.simps bw_point.simps
   734   by smt+ (* FIXME: bad Z3-4.3.x proof with smt2 *)
   734   by smt+ (* smt2 FIXME: bad Z3 4.3.x proof *)
   735 
   735 
   736 lemma
   736 lemma
   737   "\<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>"
   738   "\<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> =
   739      \<lparr> cx = 3, cy = 4, black = False \<rparr>"
   739      \<lparr> cx = 3, cy = 4, black = False \<rparr>"