|
1 (* Title: HOL/ex/LSC_Examples.thy |
|
2 Author: Lukas Bulwahn |
|
3 Copyright 2011 TU Muenchen |
|
4 *) |
|
5 |
|
6 header {* Examples for invoking lazysmallcheck (LSC) *} |
|
7 |
|
8 theory LSC_Examples |
|
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 |
|
126 termination sorry |
|
127 |
|
128 instance .. |
|
129 |
|
130 end |
|
131 |
|
132 code_thms implies |
|
133 declare simp_thms(17,19)[code del] |
|
134 code_thms implies |
|
135 |
|
136 subsubsection {* Invalid Lemma due to typo in lbal *} |
|
137 |
|
138 lemma is_ord_l_bal: |
|
139 "\<lbrakk> is_ord(MKT (x :: nat) l r h); height l = height r + 2 \<rbrakk> \<Longrightarrow> is_ord(l_bal(x,l,r))" |
|
140 quickcheck[tester = lazy_exhaustive, finite_types = false, default_type = nat, size = 1, timeout = 80, expect = counterexample] |
|
141 oops |
|
142 |
|
143 |
|
144 end |