src/HOL/SMT_Examples/SMT_Tests.thy
changeset 56819 ad1bbed53788
parent 56727 75f4fdafb285
child 56859 bc50d5e04e90
equal deleted inserted replaced
56818:689a3eeb6f9e 56819:ad1bbed53788
   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 smt2+
   734   by smt+ (* FIXME: bad Z3-4.3.x proof with smt2 *)
   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>"