author | bulwahn |
Fri, 11 Mar 2011 15:21:13 +0100 | |
changeset 41934 | db9cfca34085 |
parent 41932 | src/HOL/ex/Quickcheck_Narrowing.thy@e8f113ce8a94 |
child 41937 | a369f8ba5425 |
permissions | -rw-r--r-- |
41932
e8f113ce8a94
adapting Quickcheck_Narrowing and example file to new names
bulwahn
parents:
41931
diff
changeset
|
1 |
(* Title: HOL/ex/Quickcheck_Narrowing_Examples.thy |
41907 | 2 |
Author: Lukas Bulwahn |
3 |
Copyright 2011 TU Muenchen |
|
4 |
*) |
|
5 |
||
41932
e8f113ce8a94
adapting Quickcheck_Narrowing and example file to new names
bulwahn
parents:
41931
diff
changeset
|
6 |
header {* Examples for narrowing-based testing *} |
41907 | 7 |
|
41932
e8f113ce8a94
adapting Quickcheck_Narrowing and example file to new names
bulwahn
parents:
41931
diff
changeset
|
8 |
theory Quickcheck_Narrowing_Examples |
41907 | 9 |
imports "~~/src/HOL/Library/LSC" |
10 |
begin |
|
11 |
||
12 |
subsection {* Simple list examples *} |
|
13 |
||
14 |
lemma "rev xs = xs" |
|
15 |
quickcheck[tester = lazy_exhaustive, finite_types = false, default_type = nat, expect = counterexample] |
|
16 |
oops |
|
17 |
||
18 |
text {* Example fails due to some strange thing... *} |
|
19 |
(* |
|
20 |
lemma "rev xs = xs" |
|
21 |
quickcheck[tester = lazy_exhaustive, finite_types = true] |
|
22 |
oops |
|
23 |
*) |
|
24 |
||
25 |
subsection {* AVL Trees *} |
|
26 |
||
27 |
datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat |
|
28 |
||
29 |
primrec set_of :: "'a tree \<Rightarrow> 'a set" |
|
30 |
where |
|
31 |
"set_of ET = {}" | |
|
32 |
"set_of (MKT n l r h) = insert n (set_of l \<union> set_of r)" |
|
33 |
||
34 |
primrec height :: "'a tree \<Rightarrow> nat" |
|
35 |
where |
|
36 |
"height ET = 0" | |
|
37 |
"height (MKT x l r h) = max (height l) (height r) + 1" |
|
38 |
||
39 |
primrec avl :: "'a tree \<Rightarrow> bool" |
|
40 |
where |
|
41 |
"avl ET = True" | |
|
42 |
"avl (MKT x l r h) = |
|
43 |
((height l = height r \<or> height l = 1+height r \<or> height r = 1+height l) \<and> |
|
44 |
h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)" |
|
45 |
||
46 |
primrec is_ord :: "('a::order) tree \<Rightarrow> bool" |
|
47 |
where |
|
48 |
"is_ord ET = True" | |
|
49 |
"is_ord (MKT n l r h) = |
|
50 |
((\<forall>n' \<in> set_of l. n' < n) \<and> (\<forall>n' \<in> set_of r. n < n') \<and> is_ord l \<and> is_ord r)" |
|
51 |
||
52 |
primrec is_in :: "('a::order) \<Rightarrow> 'a tree \<Rightarrow> bool" |
|
53 |
where |
|
54 |
"is_in k ET = False" | |
|
55 |
"is_in k (MKT n l r h) = (if k = n then True else |
|
56 |
if k < n then (is_in k l) |
|
57 |
else (is_in k r))" |
|
58 |
||
59 |
primrec ht :: "'a tree \<Rightarrow> nat" |
|
60 |
where |
|
61 |
"ht ET = 0" | |
|
62 |
"ht (MKT x l r h) = h" |
|
63 |
||
64 |
definition |
|
65 |
mkt :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where |
|
66 |
"mkt x l r = MKT x l r (max (ht l) (ht r) + 1)" |
|
67 |
||
68 |
(* replaced MKT lrn lrl lrr by MKT lrr lrl *) |
|
69 |
fun l_bal where |
|
70 |
"l_bal(n, MKT ln ll lr h, r) = |
|
71 |
(if ht ll < ht lr |
|
72 |
then case lr of ET \<Rightarrow> ET (* impossible *) |
|
73 |
| MKT lrn lrr lrl lrh \<Rightarrow> |
|
74 |
mkt lrn (mkt ln ll lrl) (mkt n lrr r) |
|
75 |
else mkt ln ll (mkt n lr r))" |
|
76 |
||
77 |
fun r_bal where |
|
78 |
"r_bal(n, l, MKT rn rl rr h) = |
|
79 |
(if ht rl > ht rr |
|
80 |
then case rl of ET \<Rightarrow> ET (* impossible *) |
|
81 |
| MKT rln rll rlr h \<Rightarrow> mkt rln (mkt n l rll) (mkt rn rlr rr) |
|
82 |
else mkt rn (mkt n l rl) rr)" |
|
83 |
||
84 |
primrec insrt :: "'a::order \<Rightarrow> 'a tree \<Rightarrow> 'a tree" |
|
85 |
where |
|
86 |
"insrt x ET = MKT x ET ET 1" | |
|
87 |
"insrt x (MKT n l r h) = |
|
88 |
(if x=n |
|
89 |
then MKT n l r h |
|
90 |
else if x<n |
|
91 |
then let l' = insrt x l; hl' = ht l'; hr = ht r |
|
92 |
in if hl' = 2+hr then l_bal(n,l',r) |
|
93 |
else MKT n l' r (1 + max hl' hr) |
|
94 |
else let r' = insrt x r; hl = ht l; hr' = ht r' |
|
95 |
in if hr' = 2+hl then r_bal(n,l,r') |
|
96 |
else MKT n l r' (1 + max hl hr'))" |
|
97 |
||
98 |
||
99 |
subsubsection {* Necessary setup for code generation *} |
|
100 |
||
101 |
primrec set_of' |
|
102 |
where |
|
103 |
"set_of' ET = []" |
|
104 |
| "set_of' (MKT n l r h) = n # (set_of' l @ set_of' r)" |
|
105 |
||
106 |
lemma set_of': |
|
107 |
"set (set_of' t) = set_of t" |
|
108 |
by (induct t) auto |
|
109 |
||
110 |
lemma is_ord_mkt: |
|
111 |
"is_ord (MKT n l r h) = ((ALL n': set (set_of' l). n' < n) & (ALL n': set (set_of' r). n < n') & is_ord l & is_ord r)" |
|
112 |
by (simp add: set_of') |
|
113 |
||
114 |
declare is_ord.simps(1)[code] is_ord_mkt[code] |
|
115 |
||
116 |
subsection {* Necessary instantiation for quickcheck generator *} |
|
117 |
||
118 |
instantiation tree :: (serial) serial |
|
119 |
begin |
|
120 |
||
121 |
function series_tree |
|
122 |
where |
|
123 |
"series_tree d = sum (cons ET) (apply (apply (apply (apply (cons MKT) series) series_tree) series_tree) series) d" |
|
124 |
by pat_completeness auto |
|
125 |
||
41912
1848775589e5
adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC
bulwahn
parents:
41910
diff
changeset
|
126 |
termination proof (relation "measure nat_of") |
1848775589e5
adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC
bulwahn
parents:
41910
diff
changeset
|
127 |
qed (auto simp add: of_int_inverse nat_of_def) |
41907 | 128 |
|
129 |
instance .. |
|
130 |
||
131 |
end |
|
132 |
||
133 |
subsubsection {* Invalid Lemma due to typo in lbal *} |
|
134 |
||
135 |
lemma is_ord_l_bal: |
|
136 |
"\<lbrakk> is_ord(MKT (x :: nat) l r h); height l = height r + 2 \<rbrakk> \<Longrightarrow> is_ord(l_bal(x,l,r))" |
|
41913
34360908cb78
increasing timeout of example for counterexample generation
bulwahn
parents:
41912
diff
changeset
|
137 |
quickcheck[tester = lazy_exhaustive, finite_types = false, default_type = nat, size = 1, timeout = 100, expect = counterexample] |
41907 | 138 |
oops |
139 |
||
140 |
||
141 |
end |