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

src/HOL/Nitpick_Examples/Induct_Nits.thy

author | wenzelm |

Tue Oct 10 19:23:03 2017 +0200 (2017-10-10) | |

changeset 66831 | 29ea2b900a05 |

parent 63167 | 0909deb8059b |

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

tuned: each session has at most one defining entry;

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

2 Author: Jasmin Blanchette, TU Muenchen

3 Copyright 2009-2011

5 Examples featuring Nitpick applied to (co)inductive definitions.

6 *)

8 section \<open>Examples Featuring Nitpick Applied to (Co)inductive Definitions\<close>

10 theory Induct_Nits

11 imports Main

12 begin

14 nitpick_params [verbose, card = 1-8, unary_ints,

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

17 inductive p1 :: "nat \<Rightarrow> bool" where

18 "p1 0" |

19 "p1 n \<Longrightarrow> p1 (n + 2)"

21 coinductive q1 :: "nat \<Rightarrow> bool" where

22 "q1 0" |

23 "q1 n \<Longrightarrow> q1 (n + 2)"

25 lemma "p1 = q1"

26 nitpick [expect = none]

27 nitpick [wf, expect = none]

28 nitpick [non_wf, expect = none]

29 nitpick [non_wf, dont_star_linear_preds, expect = none]

30 oops

32 lemma "p1 \<noteq> q1"

33 nitpick [expect = potential]

34 nitpick [wf, expect = potential]

35 nitpick [non_wf, expect = potential]

36 nitpick [non_wf, dont_star_linear_preds, expect = potential]

37 oops

39 lemma "p1 (n - 2) \<Longrightarrow> p1 n"

40 nitpick [expect = genuine]

41 nitpick [non_wf, expect = genuine]

42 nitpick [non_wf, dont_star_linear_preds, expect = genuine]

43 oops

45 lemma "q1 (n - 2) \<Longrightarrow> q1 n"

46 nitpick [expect = genuine]

47 nitpick [non_wf, expect = genuine]

48 nitpick [non_wf, dont_star_linear_preds, expect = genuine]

49 oops

51 inductive p2 :: "nat \<Rightarrow> bool" where

52 "p2 n \<Longrightarrow> p2 n"

54 coinductive q2 :: "nat \<Rightarrow> bool" where

55 "q2 n \<Longrightarrow> q2 n"

57 lemma "p2 = bot"

58 nitpick [expect = none]

59 nitpick [dont_star_linear_preds, expect = none]

60 sorry

62 lemma "q2 = bot"

63 nitpick [expect = genuine]

64 nitpick [dont_star_linear_preds, expect = genuine]

65 nitpick [wf, expect = quasi_genuine]

66 oops

68 lemma "p2 = top"

69 nitpick [expect = genuine]

70 nitpick [dont_star_linear_preds, expect = genuine]

71 oops

73 lemma "q2 = top"

74 nitpick [expect = none]

75 nitpick [dont_star_linear_preds, expect = none]

76 nitpick [wf, expect = quasi_genuine]

77 sorry

79 lemma "p2 = q2"

80 nitpick [expect = genuine]

81 nitpick [dont_star_linear_preds, expect = genuine]

82 oops

84 lemma "p2 n"

85 nitpick [expect = genuine]

86 nitpick [dont_star_linear_preds, expect = genuine]

87 nitpick [dont_specialize, expect = genuine]

88 oops

90 lemma "q2 n"

91 nitpick [expect = none]

92 nitpick [dont_star_linear_preds, expect = none]

93 sorry

95 lemma "\<not> p2 n"

96 nitpick [expect = none]

97 nitpick [dont_star_linear_preds, expect = none]

98 sorry

100 lemma "\<not> q2 n"

101 nitpick [expect = genuine]

102 nitpick [dont_star_linear_preds, expect = genuine]

103 nitpick [dont_specialize, expect = genuine]

104 oops

106 inductive p3 and p4 where

107 "p3 0" |

108 "p3 n \<Longrightarrow> p4 (Suc n)" |

109 "p4 n \<Longrightarrow> p3 (Suc n)"

111 coinductive q3 and q4 where

112 "q3 0" |

113 "q3 n \<Longrightarrow> q4 (Suc n)" |

114 "q4 n \<Longrightarrow> q3 (Suc n)"

116 lemma "p3 = q3"

117 nitpick [expect = none]

118 nitpick [non_wf, expect = none]

119 sorry

121 lemma "p4 = q4"

122 nitpick [expect = none]

123 nitpick [non_wf, expect = none]

124 sorry

126 lemma "p3 = top - p4"

127 nitpick [expect = none]

128 nitpick [non_wf, expect = none]

129 sorry

131 lemma "q3 = top - q4"

132 nitpick [expect = none]

133 nitpick [non_wf, expect = none]

134 sorry

136 lemma "inf p3 q4 \<noteq> bot"

137 nitpick [expect = potential]

138 nitpick [non_wf, expect = potential]

139 sorry

141 lemma "inf q3 p4 \<noteq> bot"

142 nitpick [expect = potential]

143 nitpick [non_wf, expect = potential]

144 sorry

146 lemma "sup p3 q4 \<noteq> top"

147 nitpick [expect = potential]

148 nitpick [non_wf, expect = potential]

149 sorry

151 lemma "sup q3 p4 \<noteq> top"

152 nitpick [expect = potential]

153 nitpick [non_wf, expect = potential]

154 sorry

156 end