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

src/HOL/Nitpick_Examples/Record_Nits.thy

author | krauss |

Mon Apr 04 09:32:50 2011 +0200 (2011-04-04) | |

changeset 42208 | 02513eb26eb7 |

parent 41278 | 8e1cde88aae6 |

child 42959 | ee829022381d |

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

raised timeouts further, for SML/NJ -- because of variations in machines/compilers, fixed timeouts can merely prevent non-termination, not enforce particular performance characteristics.

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

2 Author: Jasmin Blanchette, TU Muenchen

3 Copyright 2009, 2010

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 [verbose, card = 1\<midarrow>6, max_potential = 0,

15 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]

17 record point2d =

18 xc :: int

19 yc :: int

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

22 nitpick [expect = none]

23 sorry

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

26 nitpick [expect = genuine]

27 oops

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

30 nitpick [expect = genuine]

31 oops

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

34 nitpick [expect = genuine]

35 oops

37 record point3d = point2d +

38 zc :: int

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

41 nitpick [expect = none]

42 sorry

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

45 nitpick [expect = genuine]

46 oops

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

49 nitpick [expect = genuine]

50 oops

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

53 nitpick [expect = genuine]

54 oops

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

57 nitpick [expect = genuine]

58 oops

60 record point4d = point3d +

61 wc :: int

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

64 nitpick [expect = none]

65 sorry

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

68 nitpick [expect = genuine]

69 oops

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

72 nitpick [expect = genuine]

73 oops

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

76 nitpick [expect = genuine]

77 oops

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

80 nitpick [expect = genuine]

81 oops

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

84 nitpick [expect = genuine]

85 oops

87 end