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