summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Nitpick_Examples/Record_Nits.thy

author | blanchet |

Mon Dec 14 10:59:46 2009 +0100 (2009-12-14) | |

changeset 34083 | 652719832159 |

parent 33197 | de6285ebcc05 |

child 35076 | cc19e2aef17e |

permissions | -rw-r--r-- |

make Nitpick tests more robust by specifying SAT solver, singlethreading (in Kodkod, not in Isabelle), and higher time limits

1 (* Title: HOL/Nitpick_Examples/Record_Nits.thy

2 Author: Jasmin Blanchette, TU Muenchen

3 Copyright 2009

5 Examples featuring Nitpick applied to records.

6 *)

8 header {* Examples Featuring Nitpick Applied to Records *}

10 theory Record_Nits

11 imports Main

12 begin

14 nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]

16 record point2d =

17 xc :: int

18 yc :: int

20 lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x, yc := y\<rparr>"

21 nitpick [expect = none]

22 sorry

24 lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x\<rparr>"

25 nitpick [expect = genuine]

26 oops

28 lemma "p\<lparr>xc := x, yc := y\<rparr> \<noteq> p"

29 nitpick [expect = genuine]

30 oops

32 lemma "p\<lparr>xc := x, yc := y\<rparr> = p"

33 nitpick [expect = genuine]

34 oops

36 record point3d = point2d +

37 zc :: int

39 lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x, yc := y, zc := z\<rparr>"

40 nitpick [expect = none]

41 sorry

43 lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x\<rparr>"

44 nitpick [expect = genuine]

45 oops

47 lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>zc := z\<rparr>"

48 nitpick [expect = genuine]

49 oops

51 lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> \<noteq> p"

52 nitpick [expect = genuine]

53 oops

55 lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> = p"

56 nitpick [expect = genuine]

57 oops

59 record point4d = point3d +

60 wc :: int

62 lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr>"

63 nitpick [expect = none]

64 sorry

66 lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x\<rparr>"

67 nitpick [expect = genuine]

68 oops

70 lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>zc := z\<rparr>"

71 nitpick [expect = genuine]

72 oops

74 lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>wc := w\<rparr>"

75 nitpick [expect = genuine]

76 oops

78 lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> \<noteq> p"

79 nitpick [expect = genuine]

80 oops

82 lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> = p"

83 nitpick [expect = genuine]

84 oops

86 end