src/HOL/SMT_Examples/SMT_Tests.thy
 changeset 56819 ad1bbed53788 parent 56727 75f4fdafb285 child 56859 bc50d5e04e90
equal inserted replaced
`   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>"`