src/HOL/SMT_Examples/SMT_Tests.thy
 changeset 56859 bc50d5e04e90 parent 56819 ad1bbed53788 child 57165 7b1bf424ec5f
equal 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>"`