src/HOL/Library/LSC.thy
author bulwahn
Fri Mar 11 10:37:35 2011 +0100 (2011-03-11)
changeset 41905 e2611bc96022
child 41908 3bd9a21366d2
permissions -rw-r--r--
adding files for prototype of lazysmallcheck
bulwahn@41905
     1
(* Author: Lukas Bulwahn, TU Muenchen *)
bulwahn@41905
     2
bulwahn@41905
     3
header {* Counterexample generator based on LazySmallCheck *}
bulwahn@41905
     4
bulwahn@41905
     5
theory LSC
bulwahn@41905
     6
imports Main "~~/src/HOL/Library/Code_Char"
bulwahn@41905
     7
uses ("~~/src/HOL/Tools/LSC/lazysmallcheck.ML")
bulwahn@41905
     8
begin
bulwahn@41905
     9
bulwahn@41905
    10
subsection {* Counterexample generator *}
bulwahn@41905
    11
bulwahn@41905
    12
subsubsection {* LSC's deep representation of types of terms *}
bulwahn@41905
    13
bulwahn@41905
    14
datatype type = SumOfProd "type list list"
bulwahn@41905
    15
bulwahn@41905
    16
datatype "term" = Var "code_numeral list" type | Ctr code_numeral "term list"
bulwahn@41905
    17
bulwahn@41905
    18
datatype 'a cons = C type "(term list => 'a) list"
bulwahn@41905
    19
bulwahn@41905
    20
subsubsection {* auxilary functions for LSC *}
bulwahn@41905
    21
bulwahn@41905
    22
definition nth :: "'a list => code_numeral => 'a"
bulwahn@41905
    23
where
bulwahn@41905
    24
  "nth xs i = List.nth xs (Code_Numeral.nat_of i)"
bulwahn@41905
    25
bulwahn@41905
    26
lemma [code]:
bulwahn@41905
    27
  "nth (x # xs) i = (if i = 0 then x else nth xs (i - 1))"
bulwahn@41905
    28
unfolding nth_def by (cases i) simp
bulwahn@41905
    29
bulwahn@41905
    30
definition error :: "char list => 'a"
bulwahn@41905
    31
where
bulwahn@41905
    32
  "error = undefined"
bulwahn@41905
    33
bulwahn@41905
    34
code_const error ("Haskell" "error")
bulwahn@41905
    35
bulwahn@41905
    36
definition toEnum' :: "code_numeral => char"
bulwahn@41905
    37
where
bulwahn@41905
    38
  "toEnum' = undefined"
bulwahn@41905
    39
bulwahn@41905
    40
code_const toEnum' ("Haskell" "(toEnum . fromInteger)")
bulwahn@41905
    41
bulwahn@41905
    42
subsubsection {* LSC's basic operations *}
bulwahn@41905
    43
bulwahn@41905
    44
type_synonym 'a series = "code_numeral => 'a cons"
bulwahn@41905
    45
bulwahn@41905
    46
definition empty :: "'a series"
bulwahn@41905
    47
where
bulwahn@41905
    48
  "empty d = C (SumOfProd []) []"
bulwahn@41905
    49
  
bulwahn@41905
    50
definition cons :: "'a => 'a series"
bulwahn@41905
    51
where
bulwahn@41905
    52
  "cons a d = (C (SumOfProd [[]]) [(%_. a)])"
bulwahn@41905
    53
bulwahn@41905
    54
fun conv :: "(term list => 'a) list => term => 'a"
bulwahn@41905
    55
where
bulwahn@41905
    56
  "conv cs (Var p _) = error (Char Nibble0 Nibble0 # map toEnum' p)"
bulwahn@41905
    57
| "conv cs (Ctr i xs) = (nth cs i) xs"
bulwahn@41905
    58
bulwahn@41905
    59
fun nonEmpty :: "type => bool"
bulwahn@41905
    60
where
bulwahn@41905
    61
  "nonEmpty (SumOfProd ps) = (\<not> (List.null ps))"
bulwahn@41905
    62
bulwahn@41905
    63
definition "apply" :: "('a => 'b) series => 'a series => 'b series"
bulwahn@41905
    64
where
bulwahn@41905
    65
  "apply f a d =
bulwahn@41905
    66
     (case f d of C (SumOfProd ps) cfs =>
bulwahn@41905
    67
       case a (d - 1) of C ta cas =>
bulwahn@41905
    68
       let
bulwahn@41905
    69
         shallow = (d > 0 \<and> nonEmpty ta);
bulwahn@41905
    70
         cs = [(%xs'. (case xs' of [] => undefined | x # xs => cf xs (conv cas x))). shallow, cf <- cfs]
bulwahn@41905
    71
       in C (SumOfProd [ta # p. shallow, p <- ps]) cs)"
bulwahn@41905
    72
bulwahn@41905
    73
definition sum :: "'a series => 'a series => 'a series"
bulwahn@41905
    74
where
bulwahn@41905
    75
  "sum a b d =
bulwahn@41905
    76
    (case a d of C (SumOfProd ssa) ca => 
bulwahn@41905
    77
      case b d of C (SumOfProd ssb) cb =>
bulwahn@41905
    78
      C (SumOfProd (ssa @ ssb)) (ca @ cb))"
bulwahn@41905
    79
bulwahn@41905
    80
definition cons0 :: "'a => 'a series"
bulwahn@41905
    81
where
bulwahn@41905
    82
  "cons0 f = cons f"
bulwahn@41905
    83
bulwahn@41905
    84
bulwahn@41905
    85
subsubsection {* LSC's type class for enumeration *}
bulwahn@41905
    86
bulwahn@41905
    87
class serial =
bulwahn@41905
    88
  fixes series :: "code_numeral => 'a cons"
bulwahn@41905
    89
bulwahn@41905
    90
definition cons1 :: "('a::serial => 'b) => 'b series"
bulwahn@41905
    91
where
bulwahn@41905
    92
  "cons1 f = apply (cons f) series"
bulwahn@41905
    93
bulwahn@41905
    94
definition cons2 :: "('a :: serial => 'b :: serial => 'c) => 'c series"
bulwahn@41905
    95
where
bulwahn@41905
    96
  "cons2 f = apply (apply (cons f) series) series"
bulwahn@41905
    97
  
bulwahn@41905
    98
instantiation unit :: serial
bulwahn@41905
    99
begin
bulwahn@41905
   100
bulwahn@41905
   101
definition
bulwahn@41905
   102
  "series = cons0 ()"
bulwahn@41905
   103
bulwahn@41905
   104
instance ..
bulwahn@41905
   105
bulwahn@41905
   106
end
bulwahn@41905
   107
bulwahn@41905
   108
instantiation bool :: serial
bulwahn@41905
   109
begin
bulwahn@41905
   110
bulwahn@41905
   111
definition
bulwahn@41905
   112
  "series = sum (cons0 True) (cons0 False)" 
bulwahn@41905
   113
bulwahn@41905
   114
instance ..
bulwahn@41905
   115
bulwahn@41905
   116
end
bulwahn@41905
   117
bulwahn@41905
   118
instantiation option :: (serial) serial
bulwahn@41905
   119
begin
bulwahn@41905
   120
bulwahn@41905
   121
definition
bulwahn@41905
   122
  "series = sum (cons0 None) (cons1 Some)"
bulwahn@41905
   123
bulwahn@41905
   124
instance ..
bulwahn@41905
   125
bulwahn@41905
   126
end
bulwahn@41905
   127
bulwahn@41905
   128
instantiation sum :: (serial, serial) serial
bulwahn@41905
   129
begin
bulwahn@41905
   130
bulwahn@41905
   131
definition
bulwahn@41905
   132
  "series = sum (cons1 Inl) (cons1 Inr)"
bulwahn@41905
   133
bulwahn@41905
   134
instance ..
bulwahn@41905
   135
bulwahn@41905
   136
end
bulwahn@41905
   137
bulwahn@41905
   138
instantiation list :: (serial) serial
bulwahn@41905
   139
begin
bulwahn@41905
   140
bulwahn@41905
   141
function series_list :: "'a list series"
bulwahn@41905
   142
where
bulwahn@41905
   143
  "series_list d = sum (cons []) (apply (apply (cons Cons) series) series_list) d"
bulwahn@41905
   144
by pat_completeness auto
bulwahn@41905
   145
bulwahn@41905
   146
termination sorry
bulwahn@41905
   147
bulwahn@41905
   148
instance ..
bulwahn@41905
   149
bulwahn@41905
   150
end
bulwahn@41905
   151
bulwahn@41905
   152
instantiation nat :: serial
bulwahn@41905
   153
begin
bulwahn@41905
   154
bulwahn@41905
   155
function series_nat :: "nat series"
bulwahn@41905
   156
where
bulwahn@41905
   157
  "series_nat d = sum (cons 0) (apply (cons Suc) series_nat) d"
bulwahn@41905
   158
by pat_completeness auto
bulwahn@41905
   159
bulwahn@41905
   160
termination sorry
bulwahn@41905
   161
bulwahn@41905
   162
instance ..
bulwahn@41905
   163
bulwahn@41905
   164
end
bulwahn@41905
   165
bulwahn@41905
   166
instantiation Enum.finite_1 :: serial
bulwahn@41905
   167
begin
bulwahn@41905
   168
bulwahn@41905
   169
definition series_finite_1 :: "Enum.finite_1 series"
bulwahn@41905
   170
where
bulwahn@41905
   171
  "series_finite_1 = cons (Enum.finite_1.a\<^isub>1 :: Enum.finite_1)"
bulwahn@41905
   172
bulwahn@41905
   173
instance ..
bulwahn@41905
   174
bulwahn@41905
   175
end
bulwahn@41905
   176
bulwahn@41905
   177
instantiation Enum.finite_2 :: serial
bulwahn@41905
   178
begin
bulwahn@41905
   179
bulwahn@41905
   180
definition series_finite_2 :: "Enum.finite_2 series"
bulwahn@41905
   181
where
bulwahn@41905
   182
  "series_finite_2 = sum (cons (Enum.finite_2.a\<^isub>1 :: Enum.finite_2)) (cons (Enum.finite_2.a\<^isub>2 :: Enum.finite_2))"
bulwahn@41905
   183
bulwahn@41905
   184
instance ..
bulwahn@41905
   185
bulwahn@41905
   186
end
bulwahn@41905
   187
bulwahn@41905
   188
instantiation Enum.finite_3 :: serial
bulwahn@41905
   189
begin
bulwahn@41905
   190
bulwahn@41905
   191
definition series_finite_3 :: "Enum.finite_3 series"
bulwahn@41905
   192
where
bulwahn@41905
   193
  "series_finite_3 = sum (cons (Enum.finite_3.a\<^isub>1 :: Enum.finite_3)) (sum (cons (Enum.finite_3.a\<^isub>2 :: Enum.finite_3)) (cons (Enum.finite_3.a\<^isub>3 :: Enum.finite_3)))"
bulwahn@41905
   194
bulwahn@41905
   195
instance ..
bulwahn@41905
   196
bulwahn@41905
   197
end
bulwahn@41905
   198
bulwahn@41905
   199
subsubsection {* class is_testable *}
bulwahn@41905
   200
bulwahn@41905
   201
text {* The class is_testable ensures that all necessary type instances are generated. *}
bulwahn@41905
   202
bulwahn@41905
   203
class is_testable
bulwahn@41905
   204
bulwahn@41905
   205
instance bool :: is_testable ..
bulwahn@41905
   206
bulwahn@41905
   207
instance "fun" :: ("{term_of, serial}", is_testable) is_testable ..
bulwahn@41905
   208
bulwahn@41905
   209
definition ensure_testable :: "'a :: is_testable => 'a :: is_testable"
bulwahn@41905
   210
where
bulwahn@41905
   211
  "ensure_testable f = f"
bulwahn@41905
   212
bulwahn@41905
   213
subsubsection {* Setting up the counterexample generator *}
bulwahn@41905
   214
  
bulwahn@41905
   215
use "Tools/LSC/lazysmallcheck.ML"
bulwahn@41905
   216
bulwahn@41905
   217
setup {* Lazysmallcheck.setup *}
bulwahn@41905
   218
bulwahn@41905
   219
end