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

src/HOL/Nitpick_Examples/Record_Nits.thy

author | wenzelm |

Thu Feb 11 23:00:22 2010 +0100 (2010-02-11) | |

changeset 35115 | 446c5063e4fd |

parent 35078 | 6fd1052fe463 |

child 35284 | 9edc2bd6d2bd |

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

modernized translations;

formal markup of @{syntax_const} and @{const_syntax};

minor tuning;

formal markup of @{syntax_const} and @{const_syntax};

minor tuning;

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 [sat_solver = MiniSat_JNI, 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