author | kuncar |
Fri, 27 Sep 2013 14:43:26 +0200 | |
changeset 53952 | b2781a3ce958 |
parent 53827 | 62c2f66ff9b2 |
child 54633 | 86e0b402994c |
permissions | -rw-r--r-- |
33197 | 1 |
(* Title: HOL/Nitpick_Examples/Manual_Nits.thy |
2 |
Author: Jasmin Blanchette, TU Muenchen |
|
53808 | 3 |
Copyright 2009-2013 |
33197 | 4 |
|
5 |
Examples from the Nitpick manual. |
|
6 |
*) |
|
7 |
||
8 |
header {* Examples from the Nitpick Manual *} |
|
9 |
||
37477
e482320bcbfe
adjusted Nitpick examples to latest changes + make them slightly faster
blanchet
parents:
36268
diff
changeset
|
10 |
(* The "expect" arguments to Nitpick in this theory and the other example |
e482320bcbfe
adjusted Nitpick examples to latest changes + make them slightly faster
blanchet
parents:
36268
diff
changeset
|
11 |
theories are there so that the example can also serve as a regression test |
e482320bcbfe
adjusted Nitpick examples to latest changes + make them slightly faster
blanchet
parents:
36268
diff
changeset
|
12 |
suite. *) |
e482320bcbfe
adjusted Nitpick examples to latest changes + make them slightly faster
blanchet
parents:
36268
diff
changeset
|
13 |
|
33197 | 14 |
theory Manual_Nits |
53808 | 15 |
imports Main Real "~~/src/HOL/Library/Quotient_Product" "~~/src/HOL/BNF/BNF" |
33197 | 16 |
begin |
17 |
||
45053 | 18 |
chapter {* 2. First Steps *} |
33197 | 19 |
|
46104 | 20 |
nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240] |
33197 | 21 |
|
45053 | 22 |
subsection {* 2.1. Propositional Logic *} |
33197 | 23 |
|
24 |
lemma "P \<longleftrightarrow> Q" |
|
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
25 |
nitpick [expect = genuine] |
33197 | 26 |
apply auto |
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
27 |
nitpick [expect = genuine] 1 |
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
28 |
nitpick [expect = genuine] 2 |
33197 | 29 |
oops |
30 |
||
45053 | 31 |
subsection {* 2.2. Type Variables *} |
33197 | 32 |
|
46104 | 33 |
lemma "x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A" |
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
34 |
nitpick [verbose, expect = genuine] |
33197 | 35 |
oops |
36 |
||
45053 | 37 |
subsection {* 2.3. Constants *} |
33197 | 38 |
|
46104 | 39 |
lemma "x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A" |
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
40 |
nitpick [show_consts, expect = genuine] |
39362
ee65900bfced
adapt examples to latest Nitpick changes + speed them up a little bit
blanchet
parents:
39302
diff
changeset
|
41 |
nitpick [dont_specialize, show_consts, expect = genuine] |
33197 | 42 |
oops |
43 |
||
46104 | 44 |
lemma "\<exists>!x. x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A" |
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
45 |
nitpick [expect = none] |
42959 | 46 |
nitpick [card 'a = 1\<emdash>50, expect = none] |
33197 | 47 |
(* sledgehammer *) |
46104 | 48 |
by (metis the_equality) |
33197 | 49 |
|
45053 | 50 |
subsection {* 2.4. Skolemization *} |
33197 | 51 |
|
52 |
lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x" |
|
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
53 |
nitpick [expect = genuine] |
33197 | 54 |
oops |
55 |
||
56 |
lemma "\<exists>x. \<forall>f. f x = x" |
|
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
57 |
nitpick [expect = genuine] |
33197 | 58 |
oops |
59 |
||
60 |
lemma "refl r \<Longrightarrow> sym r" |
|
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
61 |
nitpick [expect = genuine] |
33197 | 62 |
oops |
63 |
||
45053 | 64 |
subsection {* 2.5. Natural Numbers and Integers *} |
33197 | 65 |
|
66 |
lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n" |
|
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
67 |
nitpick [expect = genuine] |
46104 | 68 |
nitpick [binary_ints, bits = 16, expect = genuine] |
33197 | 69 |
oops |
70 |
||
71 |
lemma "\<forall>n. Suc n \<noteq> n \<Longrightarrow> P" |
|
42421
6bc725d60593
increase "auto"'s timeout in example to help SML/NJ
blanchet
parents:
42208
diff
changeset
|
72 |
nitpick [card nat = 100, check_potential, tac_timeout = 5, expect = genuine] |
33197 | 73 |
oops |
74 |
||
75 |
lemma "P Suc" |
|
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
76 |
nitpick [expect = none] |
33197 | 77 |
oops |
78 |
||
79 |
lemma "P (op +\<Colon>nat\<Rightarrow>nat\<Rightarrow>nat)" |
|
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
80 |
nitpick [card nat = 1, expect = genuine] |
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
81 |
nitpick [card nat = 2, expect = none] |
33197 | 82 |
oops |
83 |
||
45053 | 84 |
subsection {* 2.6. Inductive Datatypes *} |
33197 | 85 |
|
86 |
lemma "hd (xs @ [y, y]) = hd xs" |
|
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
87 |
nitpick [expect = genuine] |
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
88 |
nitpick [show_consts, show_datatypes, expect = genuine] |
33197 | 89 |
oops |
90 |
||
91 |
lemma "\<lbrakk>length xs = 1; length ys = 1\<rbrakk> \<Longrightarrow> xs = ys" |
|
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
92 |
nitpick [show_datatypes, expect = genuine] |
33197 | 93 |
oops |
94 |
||
45053 | 95 |
subsection {* 2.7. Typedefs, Records, Rationals, and Reals *} |
33197 | 96 |
|
49812
e3945ddcb9aa
eliminated some remaining uses of typedef with implicit set definition;
wenzelm
parents:
48812
diff
changeset
|
97 |
definition "three = {0\<Colon>nat, 1, 2}" |
49834 | 98 |
typedef three = three |
49812
e3945ddcb9aa
eliminated some remaining uses of typedef with implicit set definition;
wenzelm
parents:
48812
diff
changeset
|
99 |
unfolding three_def by blast |
33197 | 100 |
|
101 |
definition A :: three where "A \<equiv> Abs_three 0" |
|
102 |
definition B :: three where "B \<equiv> Abs_three 1" |
|
103 |
definition C :: three where "C \<equiv> Abs_three 2" |
|
104 |
||
46104 | 105 |
lemma "\<lbrakk>A \<in> X; B \<in> X\<rbrakk> \<Longrightarrow> c \<in> X" |
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
106 |
nitpick [show_datatypes, expect = genuine] |
33197 | 107 |
oops |
108 |
||
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35185
diff
changeset
|
109 |
fun my_int_rel where |
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35185
diff
changeset
|
110 |
"my_int_rel (x, y) (u, v) = (x + v = u + y)" |
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35185
diff
changeset
|
111 |
|
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35185
diff
changeset
|
112 |
quotient_type my_int = "nat \<times> nat" / my_int_rel |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
113 |
by (auto simp add: equivp_def fun_eq_iff) |
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35185
diff
changeset
|
114 |
|
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35185
diff
changeset
|
115 |
definition add_raw where |
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35185
diff
changeset
|
116 |
"add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u\<Colon>nat), y + (v\<Colon>nat))" |
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35185
diff
changeset
|
117 |
|
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35185
diff
changeset
|
118 |
quotient_definition "add\<Colon>my_int \<Rightarrow> my_int \<Rightarrow> my_int" is add_raw |
47092 | 119 |
unfolding add_raw_def by auto |
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35185
diff
changeset
|
120 |
|
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35185
diff
changeset
|
121 |
lemma "add x y = add x x" |
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
122 |
nitpick [show_datatypes, expect = genuine] |
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35185
diff
changeset
|
123 |
oops |
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35185
diff
changeset
|
124 |
|
35711
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35710
diff
changeset
|
125 |
ML {* |
35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset
|
126 |
fun my_int_postproc _ _ _ T (Const _ $ (Const _ $ t1 $ t2)) = |
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset
|
127 |
HOLogic.mk_number T (snd (HOLogic.dest_number t1) |
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset
|
128 |
- snd (HOLogic.dest_number t2)) |
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset
|
129 |
| my_int_postproc _ _ _ _ t = t |
35711
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35710
diff
changeset
|
130 |
*} |
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35710
diff
changeset
|
131 |
|
38288 | 132 |
declaration {* |
38284
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38242
diff
changeset
|
133 |
Nitpick_Model.register_term_postprocessor @{typ my_int} my_int_postproc |
38242 | 134 |
*} |
35711
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35710
diff
changeset
|
135 |
|
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35710
diff
changeset
|
136 |
lemma "add x y = add x x" |
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35710
diff
changeset
|
137 |
nitpick [show_datatypes] |
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35710
diff
changeset
|
138 |
oops |
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35710
diff
changeset
|
139 |
|
33197 | 140 |
record point = |
141 |
Xcoord :: int |
|
142 |
Ycoord :: int |
|
143 |
||
144 |
lemma "Xcoord (p\<Colon>point) = Xcoord (q\<Colon>point)" |
|
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
145 |
nitpick [show_datatypes, expect = genuine] |
33197 | 146 |
oops |
147 |
||
148 |
lemma "4 * x + 3 * (y\<Colon>real) \<noteq> 1 / 2" |
|
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
149 |
nitpick [show_datatypes, expect = genuine] |
33197 | 150 |
oops |
151 |
||
45053 | 152 |
subsection {* 2.8. Inductive and Coinductive Predicates *} |
33197 | 153 |
|
154 |
inductive even where |
|
155 |
"even 0" | |
|
156 |
"even n \<Longrightarrow> even (Suc (Suc n))" |
|
157 |
||
158 |
lemma "\<exists>n. even n \<and> even (Suc n)" |
|
35710 | 159 |
nitpick [card nat = 50, unary_ints, verbose, expect = potential] |
33197 | 160 |
oops |
161 |
||
35710 | 162 |
lemma "\<exists>n \<le> 49. even n \<and> even (Suc n)" |
38184 | 163 |
nitpick [card nat = 50, unary_ints, expect = genuine] |
33197 | 164 |
oops |
165 |
||
166 |
inductive even' where |
|
167 |
"even' (0\<Colon>nat)" | |
|
168 |
"even' 2" | |
|
169 |
"\<lbrakk>even' m; even' n\<rbrakk> \<Longrightarrow> even' (m + n)" |
|
170 |
||
171 |
lemma "\<exists>n \<in> {0, 2, 4, 6, 8}. \<not> even' n" |
|
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
172 |
nitpick [card nat = 10, unary_ints, verbose, show_consts, expect = genuine] |
33197 | 173 |
oops |
174 |
||
175 |
lemma "even' (n - 2) \<Longrightarrow> even' n" |
|
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
176 |
nitpick [card nat = 10, show_consts, expect = genuine] |
33197 | 177 |
oops |
178 |
||
179 |
coinductive nats where |
|
180 |
"nats (x\<Colon>nat) \<Longrightarrow> nats x" |
|
181 |
||
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45694
diff
changeset
|
182 |
lemma "nats = (\<lambda>n. n \<in> {0, 1, 2, 3, 4})" |
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
183 |
nitpick [card nat = 10, show_consts, expect = genuine] |
33197 | 184 |
oops |
185 |
||
186 |
inductive odd where |
|
187 |
"odd 1" | |
|
188 |
"\<lbrakk>odd m; even n\<rbrakk> \<Longrightarrow> odd (m + n)" |
|
189 |
||
190 |
lemma "odd n \<Longrightarrow> odd (n - 2)" |
|
46105 | 191 |
nitpick [card nat = 4, show_consts, expect = genuine] |
33197 | 192 |
oops |
193 |
||
45053 | 194 |
subsection {* 2.9. Coinductive Datatypes *} |
33197 | 195 |
|
53808 | 196 |
codatatype 'a llist = LNil | LCons 'a "'a llist" |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35312
diff
changeset
|
197 |
|
53827 | 198 |
primcorec iterates where |
199 |
"iterates f a = LCons a (iterates f (f a))" |
|
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35312
diff
changeset
|
200 |
|
33197 | 201 |
lemma "xs \<noteq> LCons a xs" |
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
202 |
nitpick [expect = genuine] |
33197 | 203 |
oops |
204 |
||
205 |
lemma "\<lbrakk>xs = LCons a xs; ys = iterates (\<lambda>b. a) b\<rbrakk> \<Longrightarrow> xs = ys" |
|
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
206 |
nitpick [verbose, expect = genuine] |
33197 | 207 |
oops |
208 |
||
209 |
lemma "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> xs = ys" |
|
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
210 |
nitpick [bisim_depth = -1, show_datatypes, expect = quasi_genuine] |
42959 | 211 |
nitpick [card = 1\<emdash>5, expect = none] |
33197 | 212 |
sorry |
213 |
||
45053 | 214 |
subsection {* 2.10. Boxing *} |
33197 | 215 |
|
216 |
datatype tm = Var nat | Lam tm | App tm tm |
|
217 |
||
218 |
primrec lift where |
|
219 |
"lift (Var j) k = Var (if j < k then j else j + 1)" | |
|
220 |
"lift (Lam t) k = Lam (lift t (k + 1))" | |
|
221 |
"lift (App t u) k = App (lift t k) (lift u k)" |
|
222 |
||
223 |
primrec loose where |
|
224 |
"loose (Var j) k = (j \<ge> k)" | |
|
225 |
"loose (Lam t) k = loose t (Suc k)" | |
|
226 |
"loose (App t u) k = (loose t k \<or> loose u k)" |
|
227 |
||
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
228 |
primrec subst\<^sub>1 where |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
229 |
"subst\<^sub>1 \<sigma> (Var j) = \<sigma> j" | |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
230 |
"subst\<^sub>1 \<sigma> (Lam t) = |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
231 |
Lam (subst\<^sub>1 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 1) t)" | |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
232 |
"subst\<^sub>1 \<sigma> (App t u) = App (subst\<^sub>1 \<sigma> t) (subst\<^sub>1 \<sigma> u)" |
33197 | 233 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
234 |
lemma "\<not> loose t 0 \<Longrightarrow> subst\<^sub>1 \<sigma> t = t" |
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
235 |
nitpick [verbose, expect = genuine] |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
236 |
nitpick [eval = "subst\<^sub>1 \<sigma> t", expect = genuine] |
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
237 |
(* nitpick [dont_box, expect = unknown] *) |
33197 | 238 |
oops |
239 |
||
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
240 |
primrec subst\<^sub>2 where |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
241 |
"subst\<^sub>2 \<sigma> (Var j) = \<sigma> j" | |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
242 |
"subst\<^sub>2 \<sigma> (Lam t) = |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
243 |
Lam (subst\<^sub>2 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 0) t)" | |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
244 |
"subst\<^sub>2 \<sigma> (App t u) = App (subst\<^sub>2 \<sigma> t) (subst\<^sub>2 \<sigma> u)" |
33197 | 245 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
246 |
lemma "\<not> loose t 0 \<Longrightarrow> subst\<^sub>2 \<sigma> t = t" |
42959 | 247 |
nitpick [card = 1\<emdash>5, expect = none] |
33197 | 248 |
sorry |
249 |
||
45053 | 250 |
subsection {* 2.11. Scope Monotonicity *} |
33197 | 251 |
|
252 |
lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)" |
|
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
253 |
nitpick [verbose, expect = genuine] |
33197 | 254 |
oops |
255 |
||
256 |
lemma "\<exists>g. \<forall>x\<Colon>'b. g (f x) = x \<Longrightarrow> \<forall>y\<Colon>'a. \<exists>x. y = f x" |
|
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
257 |
nitpick [mono, expect = none] |
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
258 |
nitpick [expect = genuine] |
33197 | 259 |
oops |
260 |
||
45053 | 261 |
subsection {* 2.12. Inductive Properties *} |
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
262 |
|
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
263 |
inductive_set reach where |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
264 |
"(4\<Colon>nat) \<in> reach" | |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
265 |
"n \<in> reach \<Longrightarrow> n < 4 \<Longrightarrow> 3 * n + 1 \<in> reach" | |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
266 |
"n \<in> reach \<Longrightarrow> n + 2 \<in> reach" |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
267 |
|
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
268 |
lemma "n \<in> reach \<Longrightarrow> 2 dvd n" |
38184 | 269 |
(* nitpick *) |
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
270 |
apply (induct set: reach) |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
271 |
apply auto |
42959 | 272 |
nitpick [card = 1\<emdash>4, bits = 1\<emdash>4, expect = none] |
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
273 |
apply (thin_tac "n \<in> reach") |
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
274 |
nitpick [expect = genuine] |
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
275 |
oops |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
276 |
|
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
277 |
lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<noteq> 0" |
38184 | 278 |
(* nitpick *) |
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
279 |
apply (induct set: reach) |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
280 |
apply auto |
42959 | 281 |
nitpick [card = 1\<emdash>4, bits = 1\<emdash>4, expect = none] |
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
282 |
apply (thin_tac "n \<in> reach") |
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
283 |
nitpick [expect = genuine] |
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
284 |
oops |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
285 |
|
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
286 |
lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<ge> 4" |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
287 |
by (induct set: reach) arith+ |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
288 |
|
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
289 |
datatype 'a bin_tree = Leaf 'a | Branch "'a bin_tree" "'a bin_tree" |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
290 |
|
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
291 |
primrec labels where |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
292 |
"labels (Leaf a) = {a}" | |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
293 |
"labels (Branch t u) = labels t \<union> labels u" |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
294 |
|
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
295 |
primrec swap where |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
296 |
"swap (Leaf c) a b = |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
297 |
(if c = a then Leaf b else if c = b then Leaf a else Leaf c)" | |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
298 |
"swap (Branch t u) a b = Branch (swap t a b) (swap u a b)" |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
299 |
|
35180
c57dba973391
more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents:
35078
diff
changeset
|
300 |
lemma "{a, b} \<subseteq> labels t \<Longrightarrow> labels (swap t a b) = labels t" |
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
301 |
(* nitpick *) |
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
302 |
proof (induct t) |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
303 |
case Leaf thus ?case by simp |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
304 |
next |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
305 |
case (Branch t u) thus ?case |
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
306 |
(* nitpick *) |
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
307 |
nitpick [non_std, show_all, expect = genuine] |
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
308 |
oops |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
309 |
|
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
310 |
lemma "labels (swap t a b) = |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
311 |
(if a \<in> labels t then |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
312 |
if b \<in> labels t then labels t else (labels t - {a}) \<union> {b} |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
313 |
else |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
314 |
if b \<in> labels t then (labels t - {b}) \<union> {a} else labels t)" |
35309
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35284
diff
changeset
|
315 |
(* nitpick *) |
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
316 |
proof (induct t) |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
317 |
case Leaf thus ?case by simp |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
318 |
next |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
319 |
case (Branch t u) thus ?case |
42959 | 320 |
nitpick [non_std, card = 1\<emdash>4, expect = none] |
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
321 |
by auto |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
322 |
qed |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
323 |
|
45053 | 324 |
section {* 3. Case Studies *} |
33197 | 325 |
|
36268 | 326 |
nitpick_params [max_potential = 0] |
33197 | 327 |
|
45053 | 328 |
subsection {* 3.1. A Context-Free Grammar *} |
33197 | 329 |
|
330 |
datatype alphabet = a | b |
|
331 |
||
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
332 |
inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
333 |
"[] \<in> S\<^sub>1" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
334 |
| "w \<in> A\<^sub>1 \<Longrightarrow> b # w \<in> S\<^sub>1" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
335 |
| "w \<in> B\<^sub>1 \<Longrightarrow> a # w \<in> S\<^sub>1" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
336 |
| "w \<in> S\<^sub>1 \<Longrightarrow> a # w \<in> A\<^sub>1" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
337 |
| "w \<in> S\<^sub>1 \<Longrightarrow> b # w \<in> S\<^sub>1" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
338 |
| "\<lbrakk>v \<in> B\<^sub>1; v \<in> B\<^sub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>1" |
33197 | 339 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
340 |
theorem S\<^sub>1_sound: |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
341 |
"w \<in> S\<^sub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
342 |
nitpick [expect = genuine] |
33197 | 343 |
oops |
344 |
||
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
345 |
inductive_set S\<^sub>2 and A\<^sub>2 and B\<^sub>2 where |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
346 |
"[] \<in> S\<^sub>2" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
347 |
| "w \<in> A\<^sub>2 \<Longrightarrow> b # w \<in> S\<^sub>2" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
348 |
| "w \<in> B\<^sub>2 \<Longrightarrow> a # w \<in> S\<^sub>2" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
349 |
| "w \<in> S\<^sub>2 \<Longrightarrow> a # w \<in> A\<^sub>2" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
350 |
| "w \<in> S\<^sub>2 \<Longrightarrow> b # w \<in> B\<^sub>2" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
351 |
| "\<lbrakk>v \<in> B\<^sub>2; v \<in> B\<^sub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>2" |
33197 | 352 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
353 |
theorem S\<^sub>2_sound: |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
354 |
"w \<in> S\<^sub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
355 |
nitpick [expect = genuine] |
33197 | 356 |
oops |
357 |
||
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
358 |
inductive_set S\<^sub>3 and A\<^sub>3 and B\<^sub>3 where |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
359 |
"[] \<in> S\<^sub>3" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
360 |
| "w \<in> A\<^sub>3 \<Longrightarrow> b # w \<in> S\<^sub>3" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
361 |
| "w \<in> B\<^sub>3 \<Longrightarrow> a # w \<in> S\<^sub>3" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
362 |
| "w \<in> S\<^sub>3 \<Longrightarrow> a # w \<in> A\<^sub>3" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
363 |
| "w \<in> S\<^sub>3 \<Longrightarrow> b # w \<in> B\<^sub>3" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
364 |
| "\<lbrakk>v \<in> B\<^sub>3; w \<in> B\<^sub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>3" |
33197 | 365 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
366 |
theorem S\<^sub>3_sound: |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
367 |
"w \<in> S\<^sub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
42959 | 368 |
nitpick [card = 1\<emdash>5, expect = none] |
33197 | 369 |
sorry |
370 |
||
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
371 |
theorem S\<^sub>3_complete: |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
372 |
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^sub>3" |
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
373 |
nitpick [expect = genuine] |
33197 | 374 |
oops |
375 |
||
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
376 |
inductive_set S\<^sub>4 and A\<^sub>4 and B\<^sub>4 where |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
377 |
"[] \<in> S\<^sub>4" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
378 |
| "w \<in> A\<^sub>4 \<Longrightarrow> b # w \<in> S\<^sub>4" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
379 |
| "w \<in> B\<^sub>4 \<Longrightarrow> a # w \<in> S\<^sub>4" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
380 |
| "w \<in> S\<^sub>4 \<Longrightarrow> a # w \<in> A\<^sub>4" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
381 |
| "\<lbrakk>v \<in> A\<^sub>4; w \<in> A\<^sub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^sub>4" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
382 |
| "w \<in> S\<^sub>4 \<Longrightarrow> b # w \<in> B\<^sub>4" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
383 |
| "\<lbrakk>v \<in> B\<^sub>4; w \<in> B\<^sub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>4" |
33197 | 384 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
385 |
theorem S\<^sub>4_sound: |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
386 |
"w \<in> S\<^sub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
42959 | 387 |
nitpick [card = 1\<emdash>5, expect = none] |
33197 | 388 |
sorry |
389 |
||
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
390 |
theorem S\<^sub>4_complete: |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
391 |
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^sub>4" |
42959 | 392 |
nitpick [card = 1\<emdash>5, expect = none] |
33197 | 393 |
sorry |
394 |
||
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
395 |
theorem S\<^sub>4_A\<^sub>4_B\<^sub>4_sound_and_complete: |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
396 |
"w \<in> S\<^sub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
397 |
"w \<in> A\<^sub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
398 |
"w \<in> B\<^sub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1" |
42959 | 399 |
nitpick [card = 1\<emdash>5, expect = none] |
33197 | 400 |
sorry |
401 |
||
45053 | 402 |
subsection {* 3.2. AA Trees *} |
33197 | 403 |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset
|
404 |
datatype 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree" |
33197 | 405 |
|
406 |
primrec data where |
|
407 |
"data \<Lambda> = undefined" | |
|
408 |
"data (N x _ _ _) = x" |
|
409 |
||
410 |
primrec dataset where |
|
411 |
"dataset \<Lambda> = {}" | |
|
412 |
"dataset (N x _ t u) = {x} \<union> dataset t \<union> dataset u" |
|
413 |
||
414 |
primrec level where |
|
415 |
"level \<Lambda> = 0" | |
|
416 |
"level (N _ k _ _) = k" |
|
417 |
||
418 |
primrec left where |
|
419 |
"left \<Lambda> = \<Lambda>" | |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
420 |
"left (N _ _ t\<^sub>1 _) = t\<^sub>1" |
33197 | 421 |
|
422 |
primrec right where |
|
423 |
"right \<Lambda> = \<Lambda>" | |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
424 |
"right (N _ _ _ t\<^sub>2) = t\<^sub>2" |
33197 | 425 |
|
426 |
fun wf where |
|
427 |
"wf \<Lambda> = True" | |
|
428 |
"wf (N _ k t u) = |
|
429 |
(if t = \<Lambda> then |
|
430 |
k = 1 \<and> (u = \<Lambda> \<or> (level u = 1 \<and> left u = \<Lambda> \<and> right u = \<Lambda>)) |
|
431 |
else |
|
432 |
wf t \<and> wf u \<and> u \<noteq> \<Lambda> \<and> level t < k \<and> level u \<le> k \<and> level (right u) < k)" |
|
433 |
||
434 |
fun skew where |
|
435 |
"skew \<Lambda> = \<Lambda>" | |
|
436 |
"skew (N x k t u) = |
|
437 |
(if t \<noteq> \<Lambda> \<and> k = level t then |
|
438 |
N (data t) k (left t) (N x k (right t) u) |
|
439 |
else |
|
440 |
N x k t u)" |
|
441 |
||
442 |
fun split where |
|
443 |
"split \<Lambda> = \<Lambda>" | |
|
444 |
"split (N x k t u) = |
|
445 |
(if u \<noteq> \<Lambda> \<and> k = level (right u) then |
|
446 |
N (data u) (Suc k) (N x k t (left u)) (right u) |
|
447 |
else |
|
448 |
N x k t u)" |
|
449 |
||
450 |
theorem dataset_skew_split: |
|
451 |
"dataset (skew t) = dataset t" |
|
452 |
"dataset (split t) = dataset t" |
|
42959 | 453 |
nitpick [card = 1\<emdash>5, expect = none] |
33197 | 454 |
sorry |
455 |
||
456 |
theorem wf_skew_split: |
|
457 |
"wf t \<Longrightarrow> skew t = t" |
|
458 |
"wf t \<Longrightarrow> split t = t" |
|
42959 | 459 |
nitpick [card = 1\<emdash>5, expect = none] |
33197 | 460 |
sorry |
461 |
||
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
462 |
primrec insort\<^sub>1 where |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
463 |
"insort\<^sub>1 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" | |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
464 |
"insort\<^sub>1 (N y k t u) x = |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
465 |
(* (split \<circ> skew) *) (N y k (if x < y then insort\<^sub>1 t x else t) |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
466 |
(if x > y then insort\<^sub>1 u x else u))" |
33197 | 467 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
468 |
theorem wf_insort\<^sub>1: "wf t \<Longrightarrow> wf (insort\<^sub>1 t x)" |
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents:
35665
diff
changeset
|
469 |
nitpick [expect = genuine] |
33197 | 470 |
oops |
471 |
||
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
472 |
theorem wf_insort\<^sub>1_nat: "wf t \<Longrightarrow> wf (insort\<^sub>1 t (x\<Colon>nat))" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
473 |
nitpick [eval = "insort\<^sub>1 t x", expect = genuine] |
33197 | 474 |
oops |
475 |
||
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
476 |
primrec insort\<^sub>2 where |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
477 |
"insort\<^sub>2 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" | |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
478 |
"insort\<^sub>2 (N y k t u) x = |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
479 |
(split \<circ> skew) (N y k (if x < y then insort\<^sub>2 t x else t) |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
480 |
(if x > y then insort\<^sub>2 u x else u))" |
33197 | 481 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
482 |
theorem wf_insort\<^sub>2: "wf t \<Longrightarrow> wf (insort\<^sub>2 t x)" |
42959 | 483 |
nitpick [card = 1\<emdash>5, expect = none] |
33197 | 484 |
sorry |
485 |
||
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51523
diff
changeset
|
486 |
theorem dataset_insort\<^sub>2: "dataset (insort\<^sub>2 t x) = {x} \<union> dataset t" |
42959 | 487 |
nitpick [card = 1\<emdash>5, expect = none] |
33197 | 488 |
sorry |
489 |
||
490 |
end |