author  huffman 
Wed, 17 Nov 2010 11:39:44 0800  
changeset 40620  7a9278de19ad 
parent 40420  552563ea3304 
child 40639  f1f0e6adca0a 
permissions  rwrr 
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

1 
(* Author: Lukas Bulwahn, TU Muenchen *) 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

2 

552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

3 
header {* Another simple counterexample generator *} 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

4 

552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

5 
theory Smallcheck 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

6 
imports Quickcheck 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

7 
uses ("Tools/smallvalue_generators.ML") 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

8 
begin 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

9 

552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

10 

40620  11 
subsection {* small value generator type classes *} 
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

12 

552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

13 
class small = term_of + 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

14 
fixes small :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option" 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

15 

552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

16 
instantiation unit :: small 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

17 
begin 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

18 

552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

19 
definition "find_first f d = f ()" 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

20 

552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

21 
instance .. 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

22 

552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

23 
end 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

24 

552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

25 
instantiation int :: small 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

26 
begin 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

27 

552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

28 
function small' :: "(int => term list option) => int => int => term list option" 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

29 
where "small' f d i = (if d < i then None else (case f i of Some t => Some t  None => small' f d (i + 1)))" 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

30 
by pat_completeness auto 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

31 

552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

32 
termination 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

33 
by (relation "measure (%(_, d, i). nat (d + 1  i))") auto 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

34 

552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

35 
definition "small f d = small' f (Code_Numeral.int_of d) ( (Code_Numeral.int_of d))" 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

36 

552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

37 
instance .. 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

38 

552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

39 
end 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

40 

552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

41 
instantiation prod :: (small, small) small 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

42 
begin 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

43 

552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

44 
definition 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

45 
"small f d = small (%x. small (%y. f (x, y)) d) d" 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

46 

552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

47 
instance .. 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

48 

552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

49 
end 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

50 

40620  51 
subsection {* Defining combinators for any firstorder data type *} 
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

52 

552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

53 
definition catch_match :: "term list option => term list option => term list option" 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

54 
where 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

55 
[code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)" 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

56 

552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

57 
code_const catch_match 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

58 
(SML "(_) handle Match => _") 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

59 

552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

60 
use "Tools/smallvalue_generators.ML" 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

61 

552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

62 
(* We do not activate smallcheck yet. 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

63 
setup {* Smallvalue_Generators.setup *} 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

64 
*) 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

65 

552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

66 
hide_fact catch_match_def 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

67 
hide_const (open) catch_match 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

68 

552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

69 
end 