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

src/HOL/Nitpick_Examples/Record_Nits.thy

author | wenzelm |

Tue Sep 03 01:12:40 2013 +0200 (2013-09-03) | |

changeset 53374 | a14d2a854c02 |

parent 48812 | 9509fc5485b2 |

child 54633 | 86e0b402994c |

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

tuned proofs -- clarified flow of facts wrt. calculation;

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

2 Author: Jasmin Blanchette, TU Muenchen

3 Copyright 2009-2011

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\<emdash>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