src/HOL/ex/Quickcheck_Narrowing_Examples.thy
author bulwahn
Tue, 07 Jun 2011 11:10:58 +0200
changeset 43239 42f82fda796b
parent 42184 1d4fae76ba5e
child 43318 825f4f0dcf71
permissions -rw-r--r--
adding examples with existentials
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
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
41932
e8f113ce8a94 adapting Quickcheck_Narrowing and example file to new names
bulwahn
parents: 41931
diff changeset
     6
header {* Examples for narrowing-based testing  *}
41907
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
     7
41932
e8f113ce8a94 adapting Quickcheck_Narrowing and example file to new names
bulwahn
parents: 41931
diff changeset
     8
theory Quickcheck_Narrowing_Examples
41937
a369f8ba5425 adapting example file to renaming of the quickcheck tester
bulwahn
parents: 41934
diff changeset
     9
imports "~~/src/HOL/Library/Quickcheck_Narrowing"
41907
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
42020
2da02764d523 translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents: 41963
diff changeset
    12
subsection {* Minimalistic examples *}
42021
52551c0a3374 extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents: 42020
diff changeset
    13
(*
42020
2da02764d523 translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents: 41963
diff changeset
    14
lemma
2da02764d523 translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents: 41963
diff changeset
    15
  "x = y"
42021
52551c0a3374 extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents: 42020
diff changeset
    16
quickcheck[tester = narrowing, finite_types = false, default_type = int, expect = counterexample]
41907
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
    17
oops
42021
52551c0a3374 extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents: 42020
diff changeset
    18
*)
41907
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
    19
(*
42020
2da02764d523 translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents: 41963
diff changeset
    20
lemma
2da02764d523 translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents: 41963
diff changeset
    21
  "x = y"
2da02764d523 translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents: 41963
diff changeset
    22
quickcheck[tester = narrowing, finite_types = true, expect = counterexample]
41907
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
    23
oops
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
43239
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    26
(*declare [[quickcheck_narrowing_overlord]]*)
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    27
subsection {* Simple examples with existentials *}
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    28
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    29
lemma
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    30
  "\<exists> y :: nat. \<forall> x. x = y"
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    31
quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    32
oops
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    33
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    34
lemma
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    35
  "x > 1 --> (\<exists>y :: nat. x < y & y <= 1)"
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    36
quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    37
oops
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    38
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    39
lemma
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    40
  "x > 2 --> (\<exists>y :: nat. x < y & y <= 2)"
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    41
quickcheck[tester = narrowing, finite_types = false, size = 10]
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    42
oops
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    43
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    44
lemma
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    45
  "\<forall> x. \<exists> y :: nat. x > 3 --> (y < x & y > 3)"
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    46
quickcheck[tester = narrowing, finite_types = false, size = 7]
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    47
oops
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    48
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    49
text {* A false conjecture derived from an partial copy-n-paste of @{thm not_distinct_decomp} *}
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    50
lemma
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    51
  "~ distinct ws ==> EX xs ys zs y. ws = xs @ [y] @ ys @ [y]"
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    52
quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    53
oops
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    54
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    55
text {* A false conjecture derived from theorems @{thm split_list_first} and @{thm split_list_last} *}  
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    56
lemma
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    57
  "x : set xs ==> EX ys zs. xs = ys @ x # zs & x ~: set zs & x ~: set ys"
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    58
quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    59
oops
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    60
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    61
text {* A false conjecture derived from @{thm map_eq_Cons_conv} with a typo *}
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    62
lemma
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    63
  "(map f xs = y # ys) = (EX z zs. xs = z' # zs & f z = y & map f zs = ys)"
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    64
quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    65
oops
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    66
42020
2da02764d523 translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents: 41963
diff changeset
    67
subsection {* Simple list examples *}
2da02764d523 translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents: 41963
diff changeset
    68
2da02764d523 translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents: 41963
diff changeset
    69
lemma "rev xs = xs"
43239
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    70
quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
42020
2da02764d523 translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents: 41963
diff changeset
    71
oops
2da02764d523 translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents: 41963
diff changeset
    72
43239
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    73
(* FIXME: integer has strange representation! *)
42020
2da02764d523 translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents: 41963
diff changeset
    74
lemma "rev xs = xs"
43239
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    75
quickcheck[tester = narrowing, finite_types = false, default_type = int, expect = counterexample]
42021
52551c0a3374 extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents: 42020
diff changeset
    76
oops
42184
1d4fae76ba5e adapting Quickcheck_Narrowing (overseen in 234ec7011e5d); commenting out some examples temporarily
bulwahn
parents: 42024
diff changeset
    77
(*
42021
52551c0a3374 extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents: 42020
diff changeset
    78
lemma "rev xs = xs"
42023
1bd4b6d1c482 adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
bulwahn
parents: 42021
diff changeset
    79
  quickcheck[tester = narrowing, finite_types = true, expect = counterexample]
1bd4b6d1c482 adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
bulwahn
parents: 42021
diff changeset
    80
oops
42184
1d4fae76ba5e adapting Quickcheck_Narrowing (overseen in 234ec7011e5d); commenting out some examples temporarily
bulwahn
parents: 42024
diff changeset
    81
*)
42023
1bd4b6d1c482 adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
bulwahn
parents: 42021
diff changeset
    82
subsection {* Simple examples with functions *}
1bd4b6d1c482 adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
bulwahn
parents: 42021
diff changeset
    83
1bd4b6d1c482 adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
bulwahn
parents: 42021
diff changeset
    84
lemma "map f xs = map g xs"
43239
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    85
  quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
42020
2da02764d523 translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents: 41963
diff changeset
    86
oops
2da02764d523 translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents: 41963
diff changeset
    87
42023
1bd4b6d1c482 adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
bulwahn
parents: 42021
diff changeset
    88
lemma "map f xs = map f ys ==> xs = ys"
43239
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    89
  quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
42024
51df23535105 handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents: 42023
diff changeset
    90
oops
51df23535105 handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents: 42023
diff changeset
    91
51df23535105 handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents: 42023
diff changeset
    92
lemma
51df23535105 handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents: 42023
diff changeset
    93
  "list_all2 P (rev xs) (rev ys) = list_all2 P xs (rev ys)"
43239
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
    94
  quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
42024
51df23535105 handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents: 42023
diff changeset
    95
oops
51df23535105 handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents: 42023
diff changeset
    96
51df23535105 handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents: 42023
diff changeset
    97
lemma "map f xs = F f xs"
51df23535105 handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents: 42023
diff changeset
    98
  quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
51df23535105 handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents: 42023
diff changeset
    99
oops
51df23535105 handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents: 42023
diff changeset
   100
43239
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
   101
lemma "map f xs = F f xs"
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
   102
  quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
   103
oops
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
   104
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
   105
(* requires some work...*)
42f82fda796b adding examples with existentials
bulwahn
parents: 42184
diff changeset
   106
(*
42024
51df23535105 handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents: 42023
diff changeset
   107
lemma "R O S = S O R"
51df23535105 handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents: 42023
diff changeset
   108
  quickcheck[tester = narrowing, size = 2]
51df23535105 handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents: 42023
diff changeset
   109
oops
51df23535105 handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents: 42023
diff changeset
   110
*)
51df23535105 handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents: 42023
diff changeset
   111
41907
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   112
subsection {* AVL Trees *}
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
datatype 'a tree = ET |  MKT 'a "'a tree" "'a tree" nat
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
primrec set_of :: "'a tree \<Rightarrow> 'a set"
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   117
where
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   118
"set_of ET = {}" |
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   119
"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
   120
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   121
primrec height :: "'a tree \<Rightarrow> nat"
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
"height ET = 0" |
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   124
"height (MKT x l r h) = max (height l) (height r) + 1"
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   125
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   126
primrec avl :: "'a tree \<Rightarrow> bool"
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   127
where
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   128
"avl ET = True" |
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   129
"avl (MKT x l r h) =
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   130
 ((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
   131
  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
   132
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   133
primrec is_ord :: "('a::order) tree \<Rightarrow> bool"
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   134
where
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   135
"is_ord ET = True" |
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   136
"is_ord (MKT n l r h) =
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   137
 ((\<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
   138
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   139
primrec is_in :: "('a::order) \<Rightarrow> 'a tree \<Rightarrow> bool"
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   140
where
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   141
 "is_in k ET = False" |
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   142
 "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
   143
                           if k < n then (is_in k l)
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   144
                           else (is_in k r))"
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   145
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   146
primrec ht :: "'a tree \<Rightarrow> nat"
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   147
where
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   148
"ht ET = 0" |
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   149
"ht (MKT x l r h) = h"
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   150
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   151
definition
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   152
 mkt :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   153
"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
   154
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   155
(* replaced MKT lrn lrl lrr by MKT lrr lrl *)
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   156
fun l_bal where
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   157
"l_bal(n, MKT ln ll lr h, r) =
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   158
 (if ht ll < ht lr
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   159
  then case lr of ET \<Rightarrow> ET (* impossible *)
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   160
                | MKT lrn lrr lrl lrh \<Rightarrow>
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   161
                  mkt lrn (mkt ln ll lrl) (mkt n lrr r)
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   162
  else mkt ln ll (mkt n lr r))"
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   163
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   164
fun r_bal where
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   165
"r_bal(n, l, MKT rn rl rr h) =
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   166
 (if ht rl > ht rr
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   167
  then case rl of ET \<Rightarrow> ET (* impossible *)
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   168
                | 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
   169
  else mkt rn (mkt n l rl) rr)"
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   170
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   171
primrec insrt :: "'a::order \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   172
where
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   173
"insrt x ET = MKT x ET ET 1" |
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   174
"insrt x (MKT n l r h) = 
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   175
   (if x=n
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   176
    then MKT n l r h
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   177
    else if x<n
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   178
         then let l' = insrt x l; hl' = ht l'; hr = ht r
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   179
              in if hl' = 2+hr then l_bal(n,l',r)
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   180
                 else MKT n l' r (1 + max hl' hr)
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   181
         else let r' = insrt x r; hl = ht l; hr' = ht r'
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   182
              in if hr' = 2+hl then r_bal(n,l,r')
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   183
                 else MKT n l r' (1 + max hl hr'))"
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   184
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   185
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   186
subsubsection {* Necessary setup for code generation *}
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   187
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   188
primrec set_of'
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   189
where 
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   190
  "set_of' ET = []"
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   191
| "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
   192
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   193
lemma set_of':
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   194
  "set (set_of' t) = set_of t"
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   195
by (induct t) auto
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   196
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   197
lemma is_ord_mkt:
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   198
  "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
   199
by (simp add: set_of')
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   200
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   201
declare is_ord.simps(1)[code] is_ord_mkt[code]
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   202
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   203
subsubsection {* Invalid Lemma due to typo in lbal *}
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   204
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   205
lemma is_ord_l_bal:
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   206
 "\<lbrakk> is_ord(MKT (x :: nat) l r h); height l = height r + 2 \<rbrakk> \<Longrightarrow> is_ord(l_bal(x,l,r))"
42184
1d4fae76ba5e adapting Quickcheck_Narrowing (overseen in 234ec7011e5d); commenting out some examples temporarily
bulwahn
parents: 42024
diff changeset
   207
quickcheck[tester = narrowing, finite_types = false, default_type = nat, size = 6, timeout = 1000, expect = counterexample]
41907
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   208
oops
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   209
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   210
b04e16854c08 adding an example theory for Lazysmallcheck prototype
bulwahn
parents:
diff changeset
   211
end