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

src/HOL/Nitpick_Examples/Record_Nits.thy

author | paulson <lp15@cam.ac.uk> |

Mon Feb 22 14:37:56 2016 +0000 (2016-02-22) | |

changeset 62379 | 340738057c8c |

parent 58889 | 5b7a9633cfa8 |

child 63167 | 0909deb8059b |

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

An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!

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 section {* Examples Featuring Nitpick Applied to Records *}

10 theory Record_Nits

11 imports Main

12 begin

14 nitpick_params [verbose, card = 1-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