41907

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
