author | hoelzl |
Mon, 03 Dec 2012 18:19:08 +0100 | |
changeset 50328 | 25b1e8686ce0 |
parent 50046 | 0051dc4f301f |
child 51143 | 0a2371e7ced3 |
permissions | -rw-r--r-- |
41905 | 1 |
(* Author: Lukas Bulwahn, TU Muenchen *) |
2 |
||
43356 | 3 |
header {* Counterexample generator performing narrowing-based testing *} |
41905 | 4 |
|
41930
1e008cc4883a
renaming lazysmallcheck ML file to Quickcheck_Narrowing
bulwahn
parents:
41929
diff
changeset
|
5 |
theory Quickcheck_Narrowing |
43312
7a31f9064f99
adapting Quickcheck_Narrowing: adding setup for characters; correcting import statement
bulwahn
parents:
43309
diff
changeset
|
6 |
imports Quickcheck_Exhaustive |
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46758
diff
changeset
|
7 |
keywords "find_unused_assms" :: diag |
41905 | 8 |
begin |
9 |
||
10 |
subsection {* Counterexample generator *} |
|
11 |
||
43308
fd6cc1378fec
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
bulwahn
parents:
43237
diff
changeset
|
12 |
text {* We create a new target for the necessary code generation setup. *} |
fd6cc1378fec
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
bulwahn
parents:
43237
diff
changeset
|
13 |
|
fd6cc1378fec
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
bulwahn
parents:
43237
diff
changeset
|
14 |
setup {* Code_Target.extend_target ("Haskell_Quickcheck", (Code_Haskell.target, K I)) *} |
fd6cc1378fec
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
bulwahn
parents:
43237
diff
changeset
|
15 |
|
41909
383bbdad1650
replacing strings in generated Code resolves the changing names of Typerep in lazysmallcheck prototype
bulwahn
parents:
41908
diff
changeset
|
16 |
subsubsection {* Code generation setup *} |
383bbdad1650
replacing strings in generated Code resolves the changing names of Typerep in lazysmallcheck prototype
bulwahn
parents:
41908
diff
changeset
|
17 |
|
383bbdad1650
replacing strings in generated Code resolves the changing names of Typerep in lazysmallcheck prototype
bulwahn
parents:
41908
diff
changeset
|
18 |
code_type typerep |
43308
fd6cc1378fec
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
bulwahn
parents:
43237
diff
changeset
|
19 |
(Haskell_Quickcheck "Typerep") |
41909
383bbdad1650
replacing strings in generated Code resolves the changing names of Typerep in lazysmallcheck prototype
bulwahn
parents:
41908
diff
changeset
|
20 |
|
383bbdad1650
replacing strings in generated Code resolves the changing names of Typerep in lazysmallcheck prototype
bulwahn
parents:
41908
diff
changeset
|
21 |
code_const Typerep.Typerep |
43308
fd6cc1378fec
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
bulwahn
parents:
43237
diff
changeset
|
22 |
(Haskell_Quickcheck "Typerep") |
41909
383bbdad1650
replacing strings in generated Code resolves the changing names of Typerep in lazysmallcheck prototype
bulwahn
parents:
41908
diff
changeset
|
23 |
|
43308
fd6cc1378fec
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
bulwahn
parents:
43237
diff
changeset
|
24 |
code_reserved Haskell_Quickcheck Typerep |
41909
383bbdad1650
replacing strings in generated Code resolves the changing names of Typerep in lazysmallcheck prototype
bulwahn
parents:
41908
diff
changeset
|
25 |
|
43341 | 26 |
subsubsection {* Type @{text "code_int"} for Haskell Quickcheck's Int type *} |
41908
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
27 |
|
49834 | 28 |
typedef code_int = "UNIV \<Colon> int set" |
41908
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
29 |
morphisms int_of of_int by rule |
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
30 |
|
42021
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
31 |
lemma of_int_int_of [simp]: |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
32 |
"of_int (int_of k) = k" |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
33 |
by (rule int_of_inverse) |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
34 |
|
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
35 |
lemma int_of_of_int [simp]: |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
36 |
"int_of (of_int n) = n" |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
37 |
by (rule of_int_inverse) (rule UNIV_I) |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
38 |
|
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
39 |
lemma code_int: |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
40 |
"(\<And>n\<Colon>code_int. PROP P n) \<equiv> (\<And>n\<Colon>int. PROP P (of_int n))" |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
41 |
proof |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
42 |
fix n :: int |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
43 |
assume "\<And>n\<Colon>code_int. PROP P n" |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
44 |
then show "PROP P (of_int n)" . |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
45 |
next |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
46 |
fix n :: code_int |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
47 |
assume "\<And>n\<Colon>int. PROP P (of_int n)" |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
48 |
then have "PROP P (of_int (int_of n))" . |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
49 |
then show "PROP P n" by simp |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
50 |
qed |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
51 |
|
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
52 |
|
41908
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
53 |
lemma int_of_inject [simp]: |
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
54 |
"int_of k = int_of l \<longleftrightarrow> k = l" |
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
55 |
by (rule int_of_inject) |
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
56 |
|
42021
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
57 |
lemma of_int_inject [simp]: |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
58 |
"of_int n = of_int m \<longleftrightarrow> n = m" |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
59 |
by (rule of_int_inject) (rule UNIV_I)+ |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
60 |
|
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
61 |
instantiation code_int :: equal |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
62 |
begin |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
63 |
|
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
64 |
definition |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
65 |
"HOL.equal k l \<longleftrightarrow> HOL.equal (int_of k) (int_of l)" |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
66 |
|
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
67 |
instance proof |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
68 |
qed (auto simp add: equal_code_int_def equal_int_def equal_int_refl) |
42021
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
69 |
|
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
70 |
end |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
71 |
|
41912
1848775589e5
adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC
bulwahn
parents:
41910
diff
changeset
|
72 |
definition nat_of :: "code_int => nat" |
1848775589e5
adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC
bulwahn
parents:
41910
diff
changeset
|
73 |
where |
1848775589e5
adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC
bulwahn
parents:
41910
diff
changeset
|
74 |
"nat_of i = nat (int_of i)" |
42980
859fe9cc0838
improving code_int setup in Quickcheck_Narrowing; adding partial_term_of class in Quickcheck_Narrowing
bulwahn
parents:
42024
diff
changeset
|
75 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
76 |
instantiation code_int :: "{minus, linordered_semidom, semiring_div, neg_numeral, linorder}" |
41908
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
77 |
begin |
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
78 |
|
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
79 |
definition [simp, code del]: |
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
80 |
"0 = of_int 0" |
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
81 |
|
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
82 |
definition [simp, code del]: |
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
83 |
"1 = of_int 1" |
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
84 |
|
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
85 |
definition [simp, code del]: |
42021
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
86 |
"n + m = of_int (int_of n + int_of m)" |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
87 |
|
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
88 |
definition [simp, code del]: |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
89 |
"- n = of_int (- int_of n)" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
90 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
91 |
definition [simp, code del]: |
41908
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
92 |
"n - m = of_int (int_of n - int_of m)" |
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
93 |
|
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
94 |
definition [simp, code del]: |
42021
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
95 |
"n * m = of_int (int_of n * int_of m)" |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
96 |
|
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
97 |
definition [simp, code del]: |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
98 |
"n div m = of_int (int_of n div int_of m)" |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
99 |
|
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
100 |
definition [simp, code del]: |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
101 |
"n mod m = of_int (int_of n mod int_of m)" |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
102 |
|
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
103 |
definition [simp, code del]: |
41908
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
104 |
"n \<le> m \<longleftrightarrow> int_of n \<le> int_of m" |
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
105 |
|
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
106 |
definition [simp, code del]: |
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
107 |
"n < m \<longleftrightarrow> int_of n < int_of m" |
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
108 |
|
42021
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
109 |
instance proof |
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
49834
diff
changeset
|
110 |
qed (auto simp add: code_int distrib_right zmult_zless_mono2) |
41908
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
111 |
|
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
112 |
end |
42980
859fe9cc0838
improving code_int setup in Quickcheck_Narrowing; adding partial_term_of class in Quickcheck_Narrowing
bulwahn
parents:
42024
diff
changeset
|
113 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
114 |
lemma int_of_numeral [simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
115 |
"int_of (numeral k) = numeral k" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
116 |
by (induct k) (simp_all only: numeral.simps plus_code_int_def |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
117 |
one_code_int_def of_int_inverse UNIV_I) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
118 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
119 |
definition Num :: "num \<Rightarrow> code_int" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
120 |
where [code_abbrev]: "Num = numeral" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
121 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
122 |
lemma [code_abbrev]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
123 |
"- numeral k = (neg_numeral k :: code_int)" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
124 |
by (unfold neg_numeral_def) simp |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
125 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
126 |
code_datatype "0::code_int" Num |
41908
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
127 |
|
42980
859fe9cc0838
improving code_int setup in Quickcheck_Narrowing; adding partial_term_of class in Quickcheck_Narrowing
bulwahn
parents:
42024
diff
changeset
|
128 |
lemma one_code_int_code [code, code_unfold]: |
41908
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
129 |
"(1\<Colon>code_int) = Numeral1" |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
130 |
by (simp only: numeral.simps) |
41908
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
131 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
132 |
definition div_mod :: "code_int \<Rightarrow> code_int \<Rightarrow> code_int \<times> code_int" where |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
133 |
[code del]: "div_mod n m = (n div m, n mod m)" |
42021
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
134 |
|
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
135 |
lemma [code]: |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
136 |
"n div m = fst (div_mod n m)" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
137 |
unfolding div_mod_def by simp |
42021
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
138 |
|
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
139 |
lemma [code]: |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
140 |
"n mod m = snd (div_mod n m)" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
141 |
unfolding div_mod_def by simp |
42021
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
142 |
|
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
143 |
lemma int_of_code [code]: |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
144 |
"int_of k = (if k = 0 then 0 |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
145 |
else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))" |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
146 |
proof - |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
147 |
have 1: "(int_of k div 2) * 2 + int_of k mod 2 = int_of k" |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
148 |
by (rule mod_div_equality) |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
149 |
have "int_of k mod 2 = 0 \<or> int_of k mod 2 = 1" by auto |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
150 |
from this show ?thesis |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
151 |
apply auto |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
152 |
apply (insert 1) by (auto simp add: mult_ac) |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
153 |
qed |
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
154 |
|
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
155 |
|
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
156 |
code_instance code_numeral :: equal |
43308
fd6cc1378fec
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
bulwahn
parents:
43237
diff
changeset
|
157 |
(Haskell_Quickcheck -) |
42021
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
158 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
159 |
setup {* fold (Numeral.add_code @{const_name Num} |
43308
fd6cc1378fec
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
bulwahn
parents:
43237
diff
changeset
|
160 |
false Code_Printer.literal_numeral) ["Haskell_Quickcheck"] *} |
42021
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
161 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
162 |
code_type code_int |
48565
7c497a239007
restored narrowing quickcheck after 6efff142bb54
haftmann
parents:
48253
diff
changeset
|
163 |
(Haskell_Quickcheck "Prelude.Int") |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
164 |
|
41908
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
165 |
code_const "0 \<Colon> code_int" |
43308
fd6cc1378fec
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
bulwahn
parents:
43237
diff
changeset
|
166 |
(Haskell_Quickcheck "0") |
41908
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
167 |
|
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
168 |
code_const "1 \<Colon> code_int" |
43308
fd6cc1378fec
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
bulwahn
parents:
43237
diff
changeset
|
169 |
(Haskell_Quickcheck "1") |
41908
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
170 |
|
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
171 |
code_const "minus \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> code_int" |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
172 |
(Haskell_Quickcheck infixl 6 "-") |
41908
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
173 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
174 |
code_const div_mod |
43308
fd6cc1378fec
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
bulwahn
parents:
43237
diff
changeset
|
175 |
(Haskell_Quickcheck "divMod") |
42021
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
176 |
|
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
177 |
code_const "HOL.equal \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> bool" |
43308
fd6cc1378fec
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
bulwahn
parents:
43237
diff
changeset
|
178 |
(Haskell_Quickcheck infix 4 "==") |
42021
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
179 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
180 |
code_const "less_eq \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> bool" |
43308
fd6cc1378fec
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
bulwahn
parents:
43237
diff
changeset
|
181 |
(Haskell_Quickcheck infix 4 "<=") |
41908
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
182 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
183 |
code_const "less \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> bool" |
43308
fd6cc1378fec
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
bulwahn
parents:
43237
diff
changeset
|
184 |
(Haskell_Quickcheck infix 4 "<") |
41908
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
185 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
186 |
code_abort of_int |
41908
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
187 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46950
diff
changeset
|
188 |
hide_const (open) Num div_mod |
42021
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
41965
diff
changeset
|
189 |
|
41961
fdd37cfcd4a3
renaming series and serial to narrowing in Quickcheck_Narrowing
bulwahn
parents:
41943
diff
changeset
|
190 |
subsubsection {* Narrowing's deep representation of types and terms *} |
41905 | 191 |
|
46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
192 |
datatype narrowing_type = Narrowing_sum_of_products "narrowing_type list list" |
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
193 |
datatype narrowing_term = Narrowing_variable "code_int list" narrowing_type | Narrowing_constructor code_int "narrowing_term list" |
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
194 |
datatype 'a narrowing_cons = Narrowing_cons narrowing_type "(narrowing_term list => 'a) list" |
41905 | 195 |
|
46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
196 |
primrec map_cons :: "('a => 'b) => 'a narrowing_cons => 'b narrowing_cons" |
43356 | 197 |
where |
46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
198 |
"map_cons f (Narrowing_cons ty cs) = Narrowing_cons ty (map (%c. f o c) cs)" |
43356 | 199 |
|
43341 | 200 |
subsubsection {* From narrowing's deep representation of terms to @{theory Code_Evaluation}'s terms *} |
42980
859fe9cc0838
improving code_int setup in Quickcheck_Narrowing; adding partial_term_of class in Quickcheck_Narrowing
bulwahn
parents:
42024
diff
changeset
|
201 |
|
859fe9cc0838
improving code_int setup in Quickcheck_Narrowing; adding partial_term_of class in Quickcheck_Narrowing
bulwahn
parents:
42024
diff
changeset
|
202 |
class partial_term_of = typerep + |
43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42980
diff
changeset
|
203 |
fixes partial_term_of :: "'a itself => narrowing_term => Code_Evaluation.term" |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42980
diff
changeset
|
204 |
|
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42980
diff
changeset
|
205 |
lemma partial_term_of_anything: "partial_term_of x nt \<equiv> t" |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42980
diff
changeset
|
206 |
by (rule eq_reflection) (cases "partial_term_of x nt", cases t, simp) |
43356 | 207 |
|
41964
13904699c859
tuned subsubsection names in Quickcheck_Narrowing
bulwahn
parents:
41962
diff
changeset
|
208 |
subsubsection {* Auxilary functions for Narrowing *} |
41905 | 209 |
|
41908
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
210 |
consts nth :: "'a list => code_int => 'a" |
41905 | 211 |
|
43308
fd6cc1378fec
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
bulwahn
parents:
43237
diff
changeset
|
212 |
code_const nth (Haskell_Quickcheck infixl 9 "!!") |
41905 | 213 |
|
41908
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
214 |
consts error :: "char list => 'a" |
41905 | 215 |
|
43308
fd6cc1378fec
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
bulwahn
parents:
43237
diff
changeset
|
216 |
code_const error (Haskell_Quickcheck "error") |
41905 | 217 |
|
41908
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
218 |
consts toEnum :: "code_int => char" |
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
219 |
|
48565
7c497a239007
restored narrowing quickcheck after 6efff142bb54
haftmann
parents:
48253
diff
changeset
|
220 |
code_const toEnum (Haskell_Quickcheck "Prelude.toEnum") |
41905 | 221 |
|
43316 | 222 |
consts marker :: "char" |
41905 | 223 |
|
43316 | 224 |
code_const marker (Haskell_Quickcheck "''\\0'") |
225 |
||
41961
fdd37cfcd4a3
renaming series and serial to narrowing in Quickcheck_Narrowing
bulwahn
parents:
41943
diff
changeset
|
226 |
subsubsection {* Narrowing's basic operations *} |
41905 | 227 |
|
46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
228 |
type_synonym 'a narrowing = "code_int => 'a narrowing_cons" |
41905 | 229 |
|
41961
fdd37cfcd4a3
renaming series and serial to narrowing in Quickcheck_Narrowing
bulwahn
parents:
41943
diff
changeset
|
230 |
definition empty :: "'a narrowing" |
41905 | 231 |
where |
46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
232 |
"empty d = Narrowing_cons (Narrowing_sum_of_products []) []" |
41905 | 233 |
|
41961
fdd37cfcd4a3
renaming series and serial to narrowing in Quickcheck_Narrowing
bulwahn
parents:
41943
diff
changeset
|
234 |
definition cons :: "'a => 'a narrowing" |
41905 | 235 |
where |
46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
236 |
"cons a d = (Narrowing_cons (Narrowing_sum_of_products [[]]) [(%_. a)])" |
41905 | 237 |
|
43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42980
diff
changeset
|
238 |
fun conv :: "(narrowing_term list => 'a) list => narrowing_term => 'a" |
41905 | 239 |
where |
46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
240 |
"conv cs (Narrowing_variable p _) = error (marker # map toEnum p)" |
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
241 |
| "conv cs (Narrowing_constructor i xs) = (nth cs i) xs" |
41905 | 242 |
|
46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
243 |
fun non_empty :: "narrowing_type => bool" |
41905 | 244 |
where |
46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
245 |
"non_empty (Narrowing_sum_of_products ps) = (\<not> (List.null ps))" |
41905 | 246 |
|
41961
fdd37cfcd4a3
renaming series and serial to narrowing in Quickcheck_Narrowing
bulwahn
parents:
41943
diff
changeset
|
247 |
definition "apply" :: "('a => 'b) narrowing => 'a narrowing => 'b narrowing" |
41905 | 248 |
where |
249 |
"apply f a d = |
|
46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
250 |
(case f d of Narrowing_cons (Narrowing_sum_of_products ps) cfs => |
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
251 |
case a (d - 1) of Narrowing_cons ta cas => |
41905 | 252 |
let |
46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
253 |
shallow = (d > 0 \<and> non_empty ta); |
41905 | 254 |
cs = [(%xs'. (case xs' of [] => undefined | x # xs => cf xs (conv cas x))). shallow, cf <- cfs] |
46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
255 |
in Narrowing_cons (Narrowing_sum_of_products [ta # p. shallow, p <- ps]) cs)" |
41905 | 256 |
|
41961
fdd37cfcd4a3
renaming series and serial to narrowing in Quickcheck_Narrowing
bulwahn
parents:
41943
diff
changeset
|
257 |
definition sum :: "'a narrowing => 'a narrowing => 'a narrowing" |
41905 | 258 |
where |
259 |
"sum a b d = |
|
46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
260 |
(case a d of Narrowing_cons (Narrowing_sum_of_products ssa) ca => |
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
261 |
case b d of Narrowing_cons (Narrowing_sum_of_products ssb) cb => |
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
262 |
Narrowing_cons (Narrowing_sum_of_products (ssa @ ssb)) (ca @ cb))" |
41905 | 263 |
|
41912
1848775589e5
adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC
bulwahn
parents:
41910
diff
changeset
|
264 |
lemma [fundef_cong]: |
1848775589e5
adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC
bulwahn
parents:
41910
diff
changeset
|
265 |
assumes "a d = a' d" "b d = b' d" "d = d'" |
1848775589e5
adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC
bulwahn
parents:
41910
diff
changeset
|
266 |
shows "sum a b d = sum a' b' d'" |
46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
267 |
using assms unfolding sum_def by (auto split: narrowing_cons.split narrowing_type.split) |
41912
1848775589e5
adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC
bulwahn
parents:
41910
diff
changeset
|
268 |
|
1848775589e5
adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC
bulwahn
parents:
41910
diff
changeset
|
269 |
lemma [fundef_cong]: |
1848775589e5
adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC
bulwahn
parents:
41910
diff
changeset
|
270 |
assumes "f d = f' d" "(\<And>d'. 0 <= d' & d' < d ==> a d' = a' d')" |
1848775589e5
adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC
bulwahn
parents:
41910
diff
changeset
|
271 |
assumes "d = d'" |
1848775589e5
adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC
bulwahn
parents:
41910
diff
changeset
|
272 |
shows "apply f a d = apply f' a' d'" |
1848775589e5
adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC
bulwahn
parents:
41910
diff
changeset
|
273 |
proof - |
1848775589e5
adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC
bulwahn
parents:
41910
diff
changeset
|
274 |
note assms moreover |
41930
1e008cc4883a
renaming lazysmallcheck ML file to Quickcheck_Narrowing
bulwahn
parents:
41929
diff
changeset
|
275 |
have "int_of (of_int 0) < int_of d' ==> int_of (of_int 0) <= int_of (of_int (int_of d' - int_of (of_int 1)))" |
41912
1848775589e5
adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC
bulwahn
parents:
41910
diff
changeset
|
276 |
by (simp add: of_int_inverse) |
1848775589e5
adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC
bulwahn
parents:
41910
diff
changeset
|
277 |
moreover |
41930
1e008cc4883a
renaming lazysmallcheck ML file to Quickcheck_Narrowing
bulwahn
parents:
41929
diff
changeset
|
278 |
have "int_of (of_int (int_of d' - int_of (of_int 1))) < int_of d'" |
41912
1848775589e5
adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC
bulwahn
parents:
41910
diff
changeset
|
279 |
by (simp add: of_int_inverse) |
1848775589e5
adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC
bulwahn
parents:
41910
diff
changeset
|
280 |
ultimately show ?thesis |
46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
281 |
unfolding apply_def by (auto split: narrowing_cons.split narrowing_type.split simp add: Let_def) |
41912
1848775589e5
adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC
bulwahn
parents:
41910
diff
changeset
|
282 |
qed |
1848775589e5
adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC
bulwahn
parents:
41910
diff
changeset
|
283 |
|
41961
fdd37cfcd4a3
renaming series and serial to narrowing in Quickcheck_Narrowing
bulwahn
parents:
41943
diff
changeset
|
284 |
subsubsection {* Narrowing generator type class *} |
41905 | 285 |
|
41961
fdd37cfcd4a3
renaming series and serial to narrowing in Quickcheck_Narrowing
bulwahn
parents:
41943
diff
changeset
|
286 |
class narrowing = |
46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
287 |
fixes narrowing :: "code_int => 'a narrowing_cons" |
41905 | 288 |
|
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43047
diff
changeset
|
289 |
datatype property = Universal narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Existential narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Property bool |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43047
diff
changeset
|
290 |
|
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43047
diff
changeset
|
291 |
(* FIXME: hard-wired maximal depth of 100 here *) |
43315
893de45ac28d
removing unneccessary manual instantiations and dead definitions; hiding more constants and facts
bulwahn
parents:
43314
diff
changeset
|
292 |
definition exists :: "('a :: {narrowing, partial_term_of} => property) => property" |
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43047
diff
changeset
|
293 |
where |
46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
294 |
"exists f = (case narrowing (100 :: code_int) of Narrowing_cons ty cs => Existential ty (\<lambda> t. f (conv cs t)) (partial_term_of (TYPE('a))))" |
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43047
diff
changeset
|
295 |
|
43315
893de45ac28d
removing unneccessary manual instantiations and dead definitions; hiding more constants and facts
bulwahn
parents:
43314
diff
changeset
|
296 |
definition "all" :: "('a :: {narrowing, partial_term_of} => property) => property" |
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43047
diff
changeset
|
297 |
where |
46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
298 |
"all f = (case narrowing (100 :: code_int) of Narrowing_cons ty cs => Universal ty (\<lambda>t. f (conv cs t)) (partial_term_of (TYPE('a))))" |
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43047
diff
changeset
|
299 |
|
41943 | 300 |
subsubsection {* class @{text is_testable} *} |
41905 | 301 |
|
41943 | 302 |
text {* The class @{text is_testable} ensures that all necessary type instances are generated. *} |
41905 | 303 |
|
304 |
class is_testable |
|
305 |
||
306 |
instance bool :: is_testable .. |
|
307 |
||
43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42980
diff
changeset
|
308 |
instance "fun" :: ("{term_of, narrowing, partial_term_of}", is_testable) is_testable .. |
41905 | 309 |
|
310 |
definition ensure_testable :: "'a :: is_testable => 'a :: is_testable" |
|
311 |
where |
|
312 |
"ensure_testable f = f" |
|
313 |
||
41910
709c04e7b703
adding serial instance of finite_4 in lazysmallcheck; changing code equations for implies
bulwahn
parents:
41909
diff
changeset
|
314 |
|
42022
101ce92333f4
adding a simple datatype for representing functions in Quickcheck_Narrowing
bulwahn
parents:
42021
diff
changeset
|
315 |
subsubsection {* Defining a simple datatype to represent functions in an incomplete and redundant way *} |
101ce92333f4
adding a simple datatype for representing functions in Quickcheck_Narrowing
bulwahn
parents:
42021
diff
changeset
|
316 |
|
101ce92333f4
adding a simple datatype for representing functions in Quickcheck_Narrowing
bulwahn
parents:
42021
diff
changeset
|
317 |
datatype ('a, 'b) ffun = Constant 'b | Update 'a 'b "('a, 'b) ffun" |
101ce92333f4
adding a simple datatype for representing functions in Quickcheck_Narrowing
bulwahn
parents:
42021
diff
changeset
|
318 |
|
101ce92333f4
adding a simple datatype for representing functions in Quickcheck_Narrowing
bulwahn
parents:
42021
diff
changeset
|
319 |
primrec eval_ffun :: "('a, 'b) ffun => 'a => 'b" |
101ce92333f4
adding a simple datatype for representing functions in Quickcheck_Narrowing
bulwahn
parents:
42021
diff
changeset
|
320 |
where |
101ce92333f4
adding a simple datatype for representing functions in Quickcheck_Narrowing
bulwahn
parents:
42021
diff
changeset
|
321 |
"eval_ffun (Constant c) x = c" |
101ce92333f4
adding a simple datatype for representing functions in Quickcheck_Narrowing
bulwahn
parents:
42021
diff
changeset
|
322 |
| "eval_ffun (Update x' y f) x = (if x = x' then y else eval_ffun f x)" |
101ce92333f4
adding a simple datatype for representing functions in Quickcheck_Narrowing
bulwahn
parents:
42021
diff
changeset
|
323 |
|
101ce92333f4
adding a simple datatype for representing functions in Quickcheck_Narrowing
bulwahn
parents:
42021
diff
changeset
|
324 |
hide_type (open) ffun |
101ce92333f4
adding a simple datatype for representing functions in Quickcheck_Narrowing
bulwahn
parents:
42021
diff
changeset
|
325 |
hide_const (open) Constant Update eval_ffun |
101ce92333f4
adding a simple datatype for representing functions in Quickcheck_Narrowing
bulwahn
parents:
42021
diff
changeset
|
326 |
|
42024
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42022
diff
changeset
|
327 |
datatype 'b cfun = Constant 'b |
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42022
diff
changeset
|
328 |
|
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42022
diff
changeset
|
329 |
primrec eval_cfun :: "'b cfun => 'a => 'b" |
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42022
diff
changeset
|
330 |
where |
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42022
diff
changeset
|
331 |
"eval_cfun (Constant c) y = c" |
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42022
diff
changeset
|
332 |
|
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42022
diff
changeset
|
333 |
hide_type (open) cfun |
45734
1024dd30da42
hide quickcheck constants Abs_cfun and Rep_cfun, to avoid clash with HOLCF
huffman
parents:
45001
diff
changeset
|
334 |
hide_const (open) Constant eval_cfun Abs_cfun Rep_cfun |
42024
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42022
diff
changeset
|
335 |
|
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42022
diff
changeset
|
336 |
subsubsection {* Setting up the counterexample generator *} |
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43047
diff
changeset
|
337 |
|
48891 | 338 |
ML_file "Tools/Quickcheck/narrowing_generators.ML" |
42024
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42022
diff
changeset
|
339 |
|
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42022
diff
changeset
|
340 |
setup {* Narrowing_Generators.setup *} |
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42022
diff
changeset
|
341 |
|
45001
5c8d7d6db682
ensuring that some constants are generated in the source code by adding calls in ensure_testable
bulwahn
parents:
43887
diff
changeset
|
342 |
definition narrowing_dummy_partial_term_of :: "('a :: partial_term_of) itself => narrowing_term => term" |
5c8d7d6db682
ensuring that some constants are generated in the source code by adding calls in ensure_testable
bulwahn
parents:
43887
diff
changeset
|
343 |
where |
5c8d7d6db682
ensuring that some constants are generated in the source code by adding calls in ensure_testable
bulwahn
parents:
43887
diff
changeset
|
344 |
"narrowing_dummy_partial_term_of = partial_term_of" |
5c8d7d6db682
ensuring that some constants are generated in the source code by adding calls in ensure_testable
bulwahn
parents:
43887
diff
changeset
|
345 |
|
46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
346 |
definition narrowing_dummy_narrowing :: "code_int => ('a :: narrowing) narrowing_cons" |
45001
5c8d7d6db682
ensuring that some constants are generated in the source code by adding calls in ensure_testable
bulwahn
parents:
43887
diff
changeset
|
347 |
where |
5c8d7d6db682
ensuring that some constants are generated in the source code by adding calls in ensure_testable
bulwahn
parents:
43887
diff
changeset
|
348 |
"narrowing_dummy_narrowing = narrowing" |
5c8d7d6db682
ensuring that some constants are generated in the source code by adding calls in ensure_testable
bulwahn
parents:
43887
diff
changeset
|
349 |
|
5c8d7d6db682
ensuring that some constants are generated in the source code by adding calls in ensure_testable
bulwahn
parents:
43887
diff
changeset
|
350 |
lemma [code]: |
5c8d7d6db682
ensuring that some constants are generated in the source code by adding calls in ensure_testable
bulwahn
parents:
43887
diff
changeset
|
351 |
"ensure_testable f = |
5c8d7d6db682
ensuring that some constants are generated in the source code by adding calls in ensure_testable
bulwahn
parents:
43887
diff
changeset
|
352 |
(let |
46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
353 |
x = narrowing_dummy_narrowing :: code_int => bool narrowing_cons; |
45001
5c8d7d6db682
ensuring that some constants are generated in the source code by adding calls in ensure_testable
bulwahn
parents:
43887
diff
changeset
|
354 |
y = narrowing_dummy_partial_term_of :: bool itself => narrowing_term => term; |
5c8d7d6db682
ensuring that some constants are generated in the source code by adding calls in ensure_testable
bulwahn
parents:
43887
diff
changeset
|
355 |
z = (conv :: _ => _ => unit) in f)" |
5c8d7d6db682
ensuring that some constants are generated in the source code by adding calls in ensure_testable
bulwahn
parents:
43887
diff
changeset
|
356 |
unfolding Let_def ensure_testable_def .. |
5c8d7d6db682
ensuring that some constants are generated in the source code by adding calls in ensure_testable
bulwahn
parents:
43887
diff
changeset
|
357 |
|
46308 | 358 |
subsection {* Narrowing for sets *} |
359 |
||
360 |
instantiation set :: (narrowing) narrowing |
|
361 |
begin |
|
362 |
||
363 |
definition "narrowing_set = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.cons set) narrowing" |
|
364 |
||
365 |
instance .. |
|
366 |
||
367 |
end |
|
45001
5c8d7d6db682
ensuring that some constants are generated in the source code by adding calls in ensure_testable
bulwahn
parents:
43887
diff
changeset
|
368 |
|
43356 | 369 |
subsection {* Narrowing for integers *} |
370 |
||
371 |
||
46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
372 |
definition drawn_from :: "'a list => 'a narrowing_cons" |
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
373 |
where "drawn_from xs = Narrowing_cons (Narrowing_sum_of_products (map (%_. []) xs)) (map (%x y. x) xs)" |
43356 | 374 |
|
375 |
function around_zero :: "int => int list" |
|
376 |
where |
|
377 |
"around_zero i = (if i < 0 then [] else (if i = 0 then [0] else around_zero (i - 1) @ [i, -i]))" |
|
378 |
by pat_completeness auto |
|
379 |
termination by (relation "measure nat") auto |
|
380 |
||
381 |
declare around_zero.simps[simp del] |
|
382 |
||
383 |
lemma length_around_zero: |
|
384 |
assumes "i >= 0" |
|
385 |
shows "length (around_zero i) = 2 * nat i + 1" |
|
386 |
proof (induct rule: int_ge_induct[OF assms]) |
|
387 |
case 1 |
|
388 |
from 1 show ?case by (simp add: around_zero.simps) |
|
389 |
next |
|
390 |
case (2 i) |
|
391 |
from 2 show ?case |
|
392 |
by (simp add: around_zero.simps[of "i + 1"]) |
|
393 |
qed |
|
394 |
||
395 |
instantiation int :: narrowing |
|
396 |
begin |
|
397 |
||
398 |
definition |
|
399 |
"narrowing_int d = (let (u :: _ => _ => unit) = conv; i = Quickcheck_Narrowing.int_of d in drawn_from (around_zero i))" |
|
400 |
||
401 |
instance .. |
|
402 |
||
403 |
end |
|
404 |
||
405 |
lemma [code, code del]: "partial_term_of (ty :: int itself) t == undefined" |
|
406 |
by (rule partial_term_of_anything)+ |
|
407 |
||
408 |
lemma [code]: |
|
46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
409 |
"partial_term_of (ty :: int itself) (Narrowing_variable p t) == Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Int.int'') [])" |
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
410 |
"partial_term_of (ty :: int itself) (Narrowing_constructor i []) == (if i mod 2 = 0 then |
43356 | 411 |
Code_Evaluation.term_of (- (int_of i) div 2) else Code_Evaluation.term_of ((int_of i + 1) div 2))" |
412 |
by (rule partial_term_of_anything)+ |
|
413 |
||
414 |
||
46589 | 415 |
subsection {* The @{text find_unused_assms} command *} |
416 |
||
48891 | 417 |
ML_file "Tools/Quickcheck/find_unused_assms.ML" |
46589 | 418 |
|
419 |
subsection {* Closing up *} |
|
420 |
||
46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
421 |
hide_type code_int narrowing_type narrowing_term narrowing_cons property |
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
422 |
hide_const int_of of_int nat_of map_cons nth error toEnum marker empty Narrowing_cons conv non_empty ensure_testable all exists drawn_from around_zero |
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
423 |
hide_const (open) Narrowing_variable Narrowing_constructor "apply" sum cons |
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46589
diff
changeset
|
424 |
hide_fact empty_def cons_def conv.simps non_empty.simps apply_def sum_def ensure_testable_def all_def exists_def |
42022
101ce92333f4
adding a simple datatype for representing functions in Quickcheck_Narrowing
bulwahn
parents:
42021
diff
changeset
|
425 |
|
45001
5c8d7d6db682
ensuring that some constants are generated in the source code by adding calls in ensure_testable
bulwahn
parents:
43887
diff
changeset
|
426 |
end |