author | bulwahn |
Sat, 24 Oct 2009 16:55:42 +0200 | |
changeset 33124 | 5378e61add1a |
parent 33123 | 3c7c4372f9ad |
child 33126 | bb8806eb5da7 |
permissions | -rw-r--r-- |
31129
d2cead76fca2
split Predicate_Compile examples into separate theory
haftmann
parents:
31123
diff
changeset
|
1 |
theory Predicate_Compile_ex |
33120 | 2 |
imports Main Predicate_Compile_Alternative_Defs |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
3 |
begin |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
4 |
|
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
5 |
inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
6 |
"even 0" |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
7 |
| "even n \<Longrightarrow> odd (Suc n)" |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
8 |
| "odd n \<Longrightarrow> even (Suc n)" |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
9 |
|
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
10 |
code_pred (mode: [], [1]) [show_steps, inductify] even . |
31550
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31514
diff
changeset
|
11 |
|
31514 | 12 |
thm odd.equation |
31123 | 13 |
thm even.equation |
33114
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
14 |
(* |
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
15 |
lemma unit: "unit_case f = (\<lambda>x. f)" |
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
16 |
apply (rule ext) |
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
17 |
apply (case_tac x) |
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
18 |
apply (simp only: unit.cases) |
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
19 |
done |
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
20 |
|
33114
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
21 |
lemma "even_1 (Suc (Suc n)) = even_1 n" |
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
22 |
thm even.equation(2) |
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
23 |
unfolding even.equation(1)[of "Suc (Suc n)"] |
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
24 |
unfolding odd.equation |
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
25 |
unfolding single_bind |
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
26 |
apply simp |
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
27 |
apply (simp add: unit) |
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
28 |
unfolding bind_single |
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
29 |
apply (rule refl) |
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
30 |
done |
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
31 |
*) |
31217 | 32 |
values "{x. even 2}" |
33 |
values "{x. odd 2}" |
|
34 |
values 10 "{n. even n}" |
|
35 |
values 10 "{n. odd n}" |
|
31195 | 36 |
|
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
37 |
inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where |
32340 | 38 |
"append [] xs xs" |
39 |
| "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)" |
|
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
40 |
|
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
41 |
code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) [inductify] append . |
33114
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
42 |
thm append.equation |
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
43 |
|
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
44 |
code_pred [rpred] append . |
31123 | 45 |
|
46 |
thm append.equation |
|
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
47 |
thm append.rpred_equation |
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
48 |
|
31217 | 49 |
values "{(ys, xs). append xs ys [0, Suc 0, 2]}" |
50 |
values "{zs. append [0, Suc 0, 2] [17, 8] zs}" |
|
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
51 |
values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}" |
31195 | 52 |
|
33111 | 53 |
value [code] "Predicate.the (append_1_2 [0::int, 1, 2] [3, 4, 5])" |
54 |
value [code] "Predicate.the (append_3 ([]::int list))" |
|
55 |
||
33116
b379ee2cddb1
changed importing introduction rules to fix the same type variables in all introduction rules; improved mode analysis for partially applied relations; added test case; tuned
bulwahn
parents:
33114
diff
changeset
|
56 |
subsection {* Tricky case with alternative rules *} |
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
57 |
|
33119
bf18c8174571
added theory with alternative definitions for the predicate compiler; cleaned up examples
bulwahn
parents:
33117
diff
changeset
|
58 |
text {* This cannot be handled correctly yet *} |
bf18c8174571
added theory with alternative definitions for the predicate compiler; cleaned up examples
bulwahn
parents:
33117
diff
changeset
|
59 |
(* |
33116
b379ee2cddb1
changed importing introduction rules to fix the same type variables in all introduction rules; improved mode analysis for partially applied relations; added test case; tuned
bulwahn
parents:
33114
diff
changeset
|
60 |
inductive append2 |
b379ee2cddb1
changed importing introduction rules to fix the same type variables in all introduction rules; improved mode analysis for partially applied relations; added test case; tuned
bulwahn
parents:
33114
diff
changeset
|
61 |
where |
b379ee2cddb1
changed importing introduction rules to fix the same type variables in all introduction rules; improved mode analysis for partially applied relations; added test case; tuned
bulwahn
parents:
33114
diff
changeset
|
62 |
"append2 [] xs xs" |
b379ee2cddb1
changed importing introduction rules to fix the same type variables in all introduction rules; improved mode analysis for partially applied relations; added test case; tuned
bulwahn
parents:
33114
diff
changeset
|
63 |
| "append2 xs ys zs \<Longrightarrow> append2 (x # xs) ys (x # zs)" |
b379ee2cddb1
changed importing introduction rules to fix the same type variables in all introduction rules; improved mode analysis for partially applied relations; added test case; tuned
bulwahn
parents:
33114
diff
changeset
|
64 |
|
b379ee2cddb1
changed importing introduction rules to fix the same type variables in all introduction rules; improved mode analysis for partially applied relations; added test case; tuned
bulwahn
parents:
33114
diff
changeset
|
65 |
lemma append2_Nil: "append2 [] (xs::'b list) xs" |
b379ee2cddb1
changed importing introduction rules to fix the same type variables in all introduction rules; improved mode analysis for partially applied relations; added test case; tuned
bulwahn
parents:
33114
diff
changeset
|
66 |
by (simp add: append2.intros(1)) |
b379ee2cddb1
changed importing introduction rules to fix the same type variables in all introduction rules; improved mode analysis for partially applied relations; added test case; tuned
bulwahn
parents:
33114
diff
changeset
|
67 |
|
b379ee2cddb1
changed importing introduction rules to fix the same type variables in all introduction rules; improved mode analysis for partially applied relations; added test case; tuned
bulwahn
parents:
33114
diff
changeset
|
68 |
lemmas [code_pred_intros] = append2_Nil append2.intros(2) |
b379ee2cddb1
changed importing introduction rules to fix the same type variables in all introduction rules; improved mode analysis for partially applied relations; added test case; tuned
bulwahn
parents:
33114
diff
changeset
|
69 |
|
b379ee2cddb1
changed importing introduction rules to fix the same type variables in all introduction rules; improved mode analysis for partially applied relations; added test case; tuned
bulwahn
parents:
33114
diff
changeset
|
70 |
code_pred append2 |
b379ee2cddb1
changed importing introduction rules to fix the same type variables in all introduction rules; improved mode analysis for partially applied relations; added test case; tuned
bulwahn
parents:
33114
diff
changeset
|
71 |
proof - |
b379ee2cddb1
changed importing introduction rules to fix the same type variables in all introduction rules; improved mode analysis for partially applied relations; added test case; tuned
bulwahn
parents:
33114
diff
changeset
|
72 |
case append2 |
b379ee2cddb1
changed importing introduction rules to fix the same type variables in all introduction rules; improved mode analysis for partially applied relations; added test case; tuned
bulwahn
parents:
33114
diff
changeset
|
73 |
from append2.cases[OF append2(1)] append2(2-3) show thesis by blast |
b379ee2cddb1
changed importing introduction rules to fix the same type variables in all introduction rules; improved mode analysis for partially applied relations; added test case; tuned
bulwahn
parents:
33114
diff
changeset
|
74 |
qed |
33119
bf18c8174571
added theory with alternative definitions for the predicate compiler; cleaned up examples
bulwahn
parents:
33117
diff
changeset
|
75 |
*) |
33112
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33111
diff
changeset
|
76 |
subsection {* Tricky cases with tuples *} |
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33111
diff
changeset
|
77 |
|
33105
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
78 |
inductive tupled_append :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool" |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
79 |
where |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
80 |
"tupled_append ([], xs, xs)" |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
81 |
| "tupled_append (xs, ys, zs) \<Longrightarrow> tupled_append (x # xs, ys, x # zs)" |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
82 |
|
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
83 |
code_pred tupled_append . |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
84 |
|
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
85 |
thm tupled_append.equation |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
86 |
(* |
33112
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33111
diff
changeset
|
87 |
TODO: values with tupled modes |
33105
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
88 |
values "{xs. tupled_append ([1,2,3], [4,5], xs)}" |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
89 |
*) |
33112
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33111
diff
changeset
|
90 |
|
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33111
diff
changeset
|
91 |
inductive tupled_append' |
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33111
diff
changeset
|
92 |
where |
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33111
diff
changeset
|
93 |
"tupled_append' ([], xs, xs)" |
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33111
diff
changeset
|
94 |
| "[| ys = fst (xa, y); x # zs = snd (xa, y); |
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33111
diff
changeset
|
95 |
tupled_append' (xs, ys, x # zs) |] ==> tupled_append' (x # xs, xa, y)" |
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
96 |
ML {* aconv *} |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
97 |
code_pred tupled_append' . |
33112
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33111
diff
changeset
|
98 |
thm tupled_append'.equation |
33114
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
99 |
(* TODO: Modeanalysis returns mode [2] ?? *) |
33112
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33111
diff
changeset
|
100 |
|
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33111
diff
changeset
|
101 |
inductive tupled_append'' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool" |
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33111
diff
changeset
|
102 |
where |
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33111
diff
changeset
|
103 |
"tupled_append'' ([], xs, xs)" |
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33111
diff
changeset
|
104 |
| "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, x # zs) \<Longrightarrow> tupled_append'' (x # xs, yszs)" |
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33111
diff
changeset
|
105 |
|
33113 | 106 |
thm tupled_append''.cases |
107 |
||
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
108 |
code_pred [inductify] tupled_append'' . |
33112
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33111
diff
changeset
|
109 |
thm tupled_append''.equation |
33114
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
110 |
(* TODO: Modeanalysis returns mode [2] ?? *) |
33112
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33111
diff
changeset
|
111 |
|
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33111
diff
changeset
|
112 |
inductive tupled_append''' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool" |
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33111
diff
changeset
|
113 |
where |
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33111
diff
changeset
|
114 |
"tupled_append''' ([], xs, xs)" |
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33111
diff
changeset
|
115 |
| "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \<Longrightarrow> tupled_append''' (x # xs, ys, x # zs)" |
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33111
diff
changeset
|
116 |
|
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
117 |
code_pred [inductify] tupled_append''' . |
33112
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33111
diff
changeset
|
118 |
thm tupled_append'''.equation |
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33111
diff
changeset
|
119 |
(* TODO: Missing a few modes *) |
33114
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
120 |
|
33113 | 121 |
inductive map_ofP :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" |
122 |
where |
|
123 |
"map_ofP ((a, b)#xs) a b" |
|
124 |
| "map_ofP xs a b \<Longrightarrow> map_ofP (x#xs) a b" |
|
33112
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33111
diff
changeset
|
125 |
|
33120 | 126 |
code_pred (mode: [1], [1, 2], [1, 2, 3], [1, 3]) map_ofP . |
33113 | 127 |
thm map_ofP.equation |
33112
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33111
diff
changeset
|
128 |
section {* reverse *} |
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33111
diff
changeset
|
129 |
|
32340 | 130 |
inductive rev where |
131 |
"rev [] []" |
|
132 |
| "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys" |
|
133 |
||
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
134 |
code_pred (mode: [1], [2], [1, 2]) rev . |
32340 | 135 |
|
136 |
thm rev.equation |
|
137 |
||
138 |
values "{xs. rev [0, 1, 2, 3::nat] xs}" |
|
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
139 |
|
33105
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
140 |
inductive tupled_rev where |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
141 |
"tupled_rev ([], [])" |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
142 |
| "tupled_rev (xs, xs') \<Longrightarrow> tupled_append (xs', [x], ys) \<Longrightarrow> tupled_rev (x#xs, ys)" |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
143 |
|
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
144 |
code_pred tupled_rev . |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
145 |
thm tupled_rev.equation |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
146 |
|
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
147 |
inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
148 |
for f where |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
149 |
"partition f [] [] []" |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
150 |
| "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs" |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
151 |
| "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)" |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
152 |
|
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
153 |
code_pred (mode: [1], [2, 3], [1, 2], [1, 3], [1, 2, 3]) partition . |
31123 | 154 |
|
33105
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
155 |
inductive tupled_partition :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<times> 'a list \<times> 'a list) \<Rightarrow> bool" |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
156 |
for f where |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
157 |
"tupled_partition f ([], [], [])" |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
158 |
| "f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, x # ys, zs)" |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
159 |
| "\<not> f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, ys, x # zs)" |
32314
66bbad0bfef9
changed resolving depending predicates and fetching in the predicate compiler
bulwahn
parents:
32310
diff
changeset
|
160 |
|
33105
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
161 |
code_pred tupled_partition . |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
162 |
|
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
163 |
thm tupled_partition.equation |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
164 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
165 |
inductive member |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
166 |
for xs |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
167 |
where "x \<in> set xs ==> member xs x" |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
168 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
169 |
lemma [code_pred_intros]: |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
170 |
"member (x#xs') x" |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
171 |
by (auto intro: member.intros) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
172 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
173 |
lemma [code_pred_intros]: |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
174 |
"member xs x ==> member (x'#xs) x" |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
175 |
by (auto intro: member.intros elim!: member.cases) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
176 |
(* strange bug must be repaired! *) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
177 |
(* |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
178 |
code_pred member sorry |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
179 |
*) |
32314
66bbad0bfef9
changed resolving depending predicates and fetching in the predicate compiler
bulwahn
parents:
32310
diff
changeset
|
180 |
inductive is_even :: "nat \<Rightarrow> bool" |
66bbad0bfef9
changed resolving depending predicates and fetching in the predicate compiler
bulwahn
parents:
32310
diff
changeset
|
181 |
where |
66bbad0bfef9
changed resolving depending predicates and fetching in the predicate compiler
bulwahn
parents:
32310
diff
changeset
|
182 |
"n mod 2 = 0 \<Longrightarrow> is_even n" |
66bbad0bfef9
changed resolving depending predicates and fetching in the predicate compiler
bulwahn
parents:
32310
diff
changeset
|
183 |
|
66bbad0bfef9
changed resolving depending predicates and fetching in the predicate compiler
bulwahn
parents:
32310
diff
changeset
|
184 |
code_pred is_even . |
31123 | 185 |
|
32314
66bbad0bfef9
changed resolving depending predicates and fetching in the predicate compiler
bulwahn
parents:
32310
diff
changeset
|
186 |
values 10 "{(ys, zs). partition is_even |
66bbad0bfef9
changed resolving depending predicates and fetching in the predicate compiler
bulwahn
parents:
32310
diff
changeset
|
187 |
[0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}" |
66bbad0bfef9
changed resolving depending predicates and fetching in the predicate compiler
bulwahn
parents:
32310
diff
changeset
|
188 |
values 10 "{zs. partition is_even zs [0, 2] [3, 5]}" |
66bbad0bfef9
changed resolving depending predicates and fetching in the predicate compiler
bulwahn
parents:
32310
diff
changeset
|
189 |
values 10 "{zs. partition is_even zs [0, 7] [3, 5]}" |
31217 | 190 |
|
31550
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31514
diff
changeset
|
191 |
lemma [code_pred_intros]: |
32340 | 192 |
"r a b \<Longrightarrow> tranclp r a b" |
193 |
"r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c" |
|
194 |
by auto |
|
31573
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
195 |
|
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
196 |
code_pred tranclp |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
197 |
proof - |
31580 | 198 |
case tranclp |
199 |
from this converse_tranclpE[OF this(1)] show thesis by metis |
|
31573
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
200 |
qed |
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
201 |
|
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
202 |
code_pred [inductify, rpred] tranclp . |
31123 | 203 |
thm tranclp.equation |
32316
1d83ac469459
added generator compilation of higher-order predicates; refined mode analysis for generators; some tuning
bulwahn
parents:
32314
diff
changeset
|
204 |
thm tranclp.rpred_equation |
33105
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
205 |
|
31217 | 206 |
inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where |
207 |
"succ 0 1" |
|
208 |
| "succ m n \<Longrightarrow> succ (Suc m) (Suc n)" |
|
209 |
||
31550
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31514
diff
changeset
|
210 |
code_pred succ . |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31514
diff
changeset
|
211 |
|
31217 | 212 |
thm succ.equation |
32340 | 213 |
|
214 |
values 10 "{(m, n). succ n m}" |
|
215 |
values "{m. succ 0 m}" |
|
216 |
values "{m. succ m 0}" |
|
217 |
||
32314
66bbad0bfef9
changed resolving depending predicates and fetching in the predicate compiler
bulwahn
parents:
32310
diff
changeset
|
218 |
(* FIXME: why does this not terminate? -- value chooses mode [] --> [1] and then starts enumerating all successors *) |
32355 | 219 |
|
31514 | 220 |
(* |
31217 | 221 |
values 20 "{n. tranclp succ 10 n}" |
222 |
values "{n. tranclp succ n 10}" |
|
223 |
values 20 "{(n, m). tranclp succ n m}" |
|
31514 | 224 |
*) |
31217 | 225 |
|
32424 | 226 |
subsection{* IMP *} |
227 |
||
228 |
types |
|
229 |
var = nat |
|
230 |
state = "int list" |
|
231 |
||
232 |
datatype com = |
|
233 |
Skip | |
|
234 |
Ass var "state => int" | |
|
235 |
Seq com com | |
|
236 |
IF "state => bool" com com | |
|
237 |
While "state => bool" com |
|
238 |
||
239 |
inductive exec :: "com => state => state => bool" where |
|
240 |
"exec Skip s s" | |
|
241 |
"exec (Ass x e) s (s[x := e(s)])" | |
|
242 |
"exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" | |
|
243 |
"b s ==> exec c1 s t ==> exec (IF b c1 c2) s t" | |
|
244 |
"~b s ==> exec c2 s t ==> exec (IF b c1 c2) s t" | |
|
245 |
"~b s ==> exec (While b c) s s" | |
|
246 |
"b s1 ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3" |
|
247 |
||
248 |
code_pred exec . |
|
249 |
||
250 |
values "{t. exec |
|
251 |
(While (%s. s!0 > 0) (Seq (Ass 0 (%s. s!0 - 1)) (Ass 1 (%s. s!1 + 1)))) |
|
252 |
[3,5] t}" |
|
253 |
||
33105
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
254 |
inductive tupled_exec :: "(com \<times> state \<times> state) \<Rightarrow> bool" where |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
255 |
"tupled_exec (Skip, s, s)" | |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
256 |
"tupled_exec (Ass x e, s, s[x := e(s)])" | |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
257 |
"tupled_exec (c1, s1, s2) ==> tupled_exec (c2, s2, s3) ==> tupled_exec (Seq c1 c2, s1, s3)" | |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
258 |
"b s ==> tupled_exec (c1, s, t) ==> tupled_exec (IF b c1 c2, s, t)" | |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
259 |
"~b s ==> tupled_exec (c2, s, t) ==> tupled_exec (IF b c1 c2, s, t)" | |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
260 |
"~b s ==> tupled_exec (While b c, s, s)" | |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
261 |
"b s1 ==> tupled_exec (c, s1, s2) ==> tupled_exec (While b c, s2, s3) ==> tupled_exec (While b c, s1, s3)" |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
262 |
|
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
263 |
code_pred tupled_exec . |
32424 | 264 |
|
32408 | 265 |
subsection{* CCS *} |
266 |
||
267 |
text{* This example formalizes finite CCS processes without communication or |
|
268 |
recursion. For simplicity, labels are natural numbers. *} |
|
269 |
||
270 |
datatype proc = nil | pre nat proc | or proc proc | par proc proc |
|
271 |
||
272 |
inductive step :: "proc \<Rightarrow> nat \<Rightarrow> proc \<Rightarrow> bool" where |
|
273 |
"step (pre n p) n p" | |
|
274 |
"step p1 a q \<Longrightarrow> step (or p1 p2) a q" | |
|
275 |
"step p2 a q \<Longrightarrow> step (or p1 p2) a q" | |
|
276 |
"step p1 a q \<Longrightarrow> step (par p1 p2) a (par q p2)" | |
|
277 |
"step p2 a q \<Longrightarrow> step (par p1 p2) a (par p1 q)" |
|
278 |
||
279 |
code_pred step . |
|
280 |
||
281 |
inductive steps where |
|
282 |
"steps p [] p" | |
|
283 |
"step p a q \<Longrightarrow> steps q as r \<Longrightarrow> steps p (a#as) r" |
|
284 |
||
285 |
code_pred steps . |
|
286 |
||
287 |
values 5 |
|
288 |
"{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}" |
|
289 |
||
290 |
(* FIXME |
|
291 |
values 3 "{(a,q). step (par nil nil) a q}" |
|
292 |
*) |
|
293 |
||
33105
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
294 |
inductive tupled_step :: "(proc \<times> nat \<times> proc) \<Rightarrow> bool" |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
295 |
where |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
296 |
"tupled_step (pre n p, n, p)" | |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
297 |
"tupled_step (p1, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" | |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
298 |
"tupled_step (p2, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" | |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
299 |
"tupled_step (p1, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par q p2)" | |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
300 |
"tupled_step (p2, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par p1 q)" |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
301 |
|
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
302 |
code_pred tupled_step . |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
303 |
thm tupled_step.equation |
1e4146bf841c
added tupled versions of examples for the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
304 |
|
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
305 |
subsection {* divmod *} |
32579 | 306 |
|
307 |
inductive divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where |
|
308 |
"k < l \<Longrightarrow> divmod_rel k l 0 k" |
|
309 |
| "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r" |
|
310 |
||
311 |
code_pred divmod_rel .. |
|
312 |
||
33111 | 313 |
value [code] "Predicate.the (divmod_rel_1_2 1705 42)" |
32579 | 314 |
|
32670 | 315 |
section {* Executing definitions *} |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
316 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
317 |
definition Min |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
318 |
where "Min s r x \<equiv> s x \<and> (\<forall>y. r x y \<longrightarrow> x = y)" |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
319 |
|
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
320 |
code_pred [inductify] Min . |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
321 |
|
32670 | 322 |
subsection {* Examples with lists *} |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33120
diff
changeset
|
323 |
(* |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
324 |
inductive filterP for Pa where |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
325 |
"(filterP::('a => bool) => 'a list => 'a list => bool) (Pa::'a => bool) [] []" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
326 |
| "[| (res::'a list) = (y::'a) # (resa::'a list); (filterP::('a => bool) => 'a list => 'a list => bool) (Pa::'a => bool) (xt::'a list) resa; Pa y |] |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
327 |
==> filterP Pa (y # xt) res" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
328 |
| "[| (filterP::('a => bool) => 'a list => 'a list => bool) (Pa::'a => bool) (xt::'a list) (res::'a list); ~ Pa (y::'a) |] ==> filterP Pa (y # xt) res" |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33120
diff
changeset
|
329 |
*) |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
330 |
(* |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
331 |
code_pred (inductify_all) (rpred) filterP . |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
332 |
thm filterP.rpred_equation |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
333 |
*) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
334 |
|
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
335 |
code_pred [inductify] lexord . |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
336 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
337 |
thm lexord.equation |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
338 |
|
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
339 |
lemma "(u, v) : lexord r ==> (x @ u, y @ v) : lexord r" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
340 |
(*quickcheck[generator=pred_compile]*) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
341 |
oops |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
342 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
343 |
lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
344 |
|
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
345 |
code_pred [inductify] lexn . |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
346 |
thm lexn.equation |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
347 |
|
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
348 |
code_pred [inductify] lenlex . |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
349 |
thm lenlex.equation |
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
350 |
|
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
351 |
code_pred [inductify, rpred] lenlex . |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
352 |
thm lenlex.rpred_equation |
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
353 |
|
32670 | 354 |
thm lists.intros |
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
355 |
code_pred [inductify] lists . |
32670 | 356 |
|
357 |
thm lists.equation |
|
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
358 |
|
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
359 |
section {* AVL Tree Example *} |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
360 |
|
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
361 |
datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
362 |
fun height :: "'a tree => nat" where |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
363 |
"height ET = 0" |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
364 |
| "height (MKT x l r h) = max (height l) (height r) + 1" |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
365 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
366 |
consts avl :: "'a tree => bool" |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
367 |
primrec |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
368 |
"avl ET = True" |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
369 |
"avl (MKT x l r h) = ((height l = height r \<or> height l = 1 + height r \<or> height r = 1+height l) \<and> |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
370 |
h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)" |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
371 |
|
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
372 |
code_pred [inductify] avl . |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
373 |
thm avl.equation |
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
374 |
|
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
375 |
fun set_of |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
376 |
where |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
377 |
"set_of ET = {}" |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
378 |
| "set_of (MKT n l r h) = insert n (set_of l \<union> set_of r)" |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
379 |
|
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33120
diff
changeset
|
380 |
|
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33120
diff
changeset
|
381 |
fun is_ord :: "nat tree => bool" |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
382 |
where |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
383 |
"is_ord ET = True" |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
384 |
| "is_ord (MKT n l r h) = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
385 |
((\<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)" |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
386 |
|
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
387 |
code_pred [inductify] set_of . |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
388 |
thm set_of.equation |
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
389 |
|
33120 | 390 |
text {* expected mode: [1], [1, 2] *} |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
391 |
(* FIXME *) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
392 |
(* |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
393 |
code_pred (inductify_all) is_ord . |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
394 |
thm is_ord.equation |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
395 |
*) |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
396 |
section {* Definitions about Relations *} |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
397 |
|
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
398 |
code_pred [inductify] converse . |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
399 |
thm converse.equation |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
400 |
|
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
401 |
code_pred [inductify] Domain . |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
402 |
thm Domain.equation |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
403 |
|
33114
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
404 |
section {* List functions *} |
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
405 |
|
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
406 |
code_pred [inductify] length . |
33114
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
407 |
thm size_listP.equation |
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
408 |
|
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
409 |
code_pred [inductify] concat . |
33114
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
410 |
thm concatP.equation |
4785ef554dcc
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
bulwahn
parents:
33113
diff
changeset
|
411 |
|
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
412 |
code_pred [inductify] hd . |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
413 |
code_pred [inductify] tl . |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
414 |
code_pred [inductify] last . |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
415 |
code_pred [inductify] butlast . |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
416 |
thm listsum.simps |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
417 |
(*code_pred [inductify] listsum .*) |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
418 |
code_pred [inductify] take . |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
419 |
code_pred [inductify] drop . |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
420 |
code_pred [inductify] zip . |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
421 |
code_pred [inductify] upt . |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
422 |
code_pred [inductify] remdups . |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
423 |
code_pred [inductify] remove1 . |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
424 |
code_pred [inductify] removeAll . |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
425 |
code_pred [inductify] distinct . |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
426 |
code_pred [inductify] replicate . |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
427 |
code_pred [inductify] splice . |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
428 |
code_pred [inductify] List.rev . |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
429 |
code_pred [inductify] foldr . |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
430 |
code_pred [inductify] foldl . |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
431 |
code_pred [inductify] filter . |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33120
diff
changeset
|
432 |
|
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33120
diff
changeset
|
433 |
definition test where "test xs = filter (\<lambda>x. x = (1::nat)) xs" |
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
434 |
(* |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
435 |
TODO: implement higher-order replacement correctly |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
436 |
code_pred [inductify] test . |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33120
diff
changeset
|
437 |
thm testP.equation |
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
438 |
code_pred [inductify, rpred] test . |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33120
diff
changeset
|
439 |
*) |
33119
bf18c8174571
added theory with alternative definitions for the predicate compiler; cleaned up examples
bulwahn
parents:
33117
diff
changeset
|
440 |
section {* Handling set operations *} |
bf18c8174571
added theory with alternative definitions for the predicate compiler; cleaned up examples
bulwahn
parents:
33117
diff
changeset
|
441 |
|
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
32665
diff
changeset
|
442 |
|
33116
b379ee2cddb1
changed importing introduction rules to fix the same type variables in all introduction rules; improved mode analysis for partially applied relations; added test case; tuned
bulwahn
parents:
33114
diff
changeset
|
443 |
|
32669
462b1dd67a58
added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo
bulwahn
parents:
32668
diff
changeset
|
444 |
section {* Context Free Grammar *} |
462b1dd67a58
added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo
bulwahn
parents:
32668
diff
changeset
|
445 |
|
462b1dd67a58
added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo
bulwahn
parents:
32668
diff
changeset
|
446 |
datatype alphabet = a | b |
462b1dd67a58
added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo
bulwahn
parents:
32668
diff
changeset
|
447 |
|
462b1dd67a58
added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo
bulwahn
parents:
32668
diff
changeset
|
448 |
inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where |
462b1dd67a58
added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo
bulwahn
parents:
32668
diff
changeset
|
449 |
"[] \<in> S\<^isub>1" |
462b1dd67a58
added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo
bulwahn
parents:
32668
diff
changeset
|
450 |
| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1" |
462b1dd67a58
added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo
bulwahn
parents:
32668
diff
changeset
|
451 |
| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1" |
462b1dd67a58
added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo
bulwahn
parents:
32668
diff
changeset
|
452 |
| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1" |
462b1dd67a58
added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo
bulwahn
parents:
32668
diff
changeset
|
453 |
| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1" |
462b1dd67a58
added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo
bulwahn
parents:
32668
diff
changeset
|
454 |
| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1" |
462b1dd67a58
added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo
bulwahn
parents:
32668
diff
changeset
|
455 |
|
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
456 |
code_pred [inductify] S\<^isub>1p . |
32669
462b1dd67a58
added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo
bulwahn
parents:
32668
diff
changeset
|
457 |
|
462b1dd67a58
added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo
bulwahn
parents:
32668
diff
changeset
|
458 |
thm S\<^isub>1p.equation |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33120
diff
changeset
|
459 |
(* |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
460 |
theorem S\<^isub>1_sound: |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
461 |
"w \<in> S\<^isub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
462 |
quickcheck[generator=pred_compile] |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
463 |
oops |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33120
diff
changeset
|
464 |
*) |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
465 |
inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
466 |
"[] \<in> S\<^isub>2" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
467 |
| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
468 |
| "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
469 |
| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
470 |
| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
471 |
| "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2" |
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
472 |
|
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
473 |
code_pred [inductify, rpred] S\<^isub>2 . |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
474 |
thm S\<^isub>2.rpred_equation |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
475 |
thm A\<^isub>2.rpred_equation |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
476 |
thm B\<^isub>2.rpred_equation |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
477 |
|
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
478 |
theorem S\<^isub>2_sound: |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
479 |
"w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
480 |
(*quickcheck[generator=SML]*) |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33120
diff
changeset
|
481 |
(*quickcheck[generator=pred_compile, size=15, iterations=100]*) |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
482 |
oops |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
483 |
|
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
484 |
inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
485 |
"[] \<in> S\<^isub>3" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
486 |
| "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
487 |
| "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
488 |
| "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
489 |
| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
490 |
| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
491 |
|
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
492 |
code_pred [inductify] S\<^isub>3 . |
33117
1413c62db675
higher-order arguments in different rules are fixed to one name in the predicate compiler
bulwahn
parents:
33116
diff
changeset
|
493 |
|
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
494 |
theorem S\<^isub>3_sound: |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
495 |
"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33120
diff
changeset
|
496 |
(*quickcheck[generator=pred_compile, size=10, iterations=1]*) |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
497 |
oops |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
498 |
|
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
499 |
lemma "\<not> (length w > 2) \<or> \<not> (length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b])" |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33120
diff
changeset
|
500 |
(*quickcheck[size=10, generator = pred_compile]*) |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
501 |
oops |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33120
diff
changeset
|
502 |
(* |
33108
9d9afd478016
added test for higher-order function inductification; added debug messages
bulwahn
parents:
33105
diff
changeset
|
503 |
inductive test |
9d9afd478016
added test for higher-order function inductification; added debug messages
bulwahn
parents:
33105
diff
changeset
|
504 |
where |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33120
diff
changeset
|
505 |
"length [x \<leftarrow> w. a = x] = length [x \<leftarrow> w. x = b] ==> test w" |
33108
9d9afd478016
added test for higher-order function inductification; added debug messages
bulwahn
parents:
33105
diff
changeset
|
506 |
ML {* @{term "[x \<leftarrow> w. x = a]"} *} |
9d9afd478016
added test for higher-order function inductification; added debug messages
bulwahn
parents:
33105
diff
changeset
|
507 |
code_pred (inductify_all) test . |
33116
b379ee2cddb1
changed importing introduction rules to fix the same type variables in all introduction rules; improved mode analysis for partially applied relations; added test case; tuned
bulwahn
parents:
33114
diff
changeset
|
508 |
|
b379ee2cddb1
changed importing introduction rules to fix the same type variables in all introduction rules; improved mode analysis for partially applied relations; added test case; tuned
bulwahn
parents:
33114
diff
changeset
|
509 |
thm test.equation |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33120
diff
changeset
|
510 |
*) |
33113 | 511 |
(* |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
512 |
theorem S\<^isub>3_complete: |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33120
diff
changeset
|
513 |
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. b = x] \<longrightarrow> w \<in> S\<^isub>3" |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
514 |
(*quickcheck[generator=SML]*) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
515 |
quickcheck[generator=pred_compile, size=10, iterations=100] |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
516 |
oops |
33113 | 517 |
*) |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
518 |
inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
519 |
"[] \<in> S\<^isub>4" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
520 |
| "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
521 |
| "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
522 |
| "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
523 |
| "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
524 |
| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
525 |
| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4" |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33120
diff
changeset
|
526 |
(* |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
527 |
theorem S\<^isub>4_sound: |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
528 |
"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
529 |
quickcheck[generator = pred_compile, size=2, iterations=1] |
32673
d5db9cf85401
replaced sorry by oops; removed old debug functions in predicate compiler
bulwahn
parents:
32672
diff
changeset
|
530 |
oops |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33120
diff
changeset
|
531 |
*) |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
532 |
theorem S\<^isub>4_complete: |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
533 |
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4" |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33120
diff
changeset
|
534 |
(*quickcheck[generator = pred_compile, size=5, iterations=1]*) |
32673
d5db9cf85401
replaced sorry by oops; removed old debug functions in predicate compiler
bulwahn
parents:
32672
diff
changeset
|
535 |
oops |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
536 |
|
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
537 |
theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete: |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
538 |
"w \<in> S\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
539 |
"w \<in> A\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
540 |
"w \<in> B\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
541 |
(*quickcheck[generator = pred_compile, size=5, iterations=1]*) |
32673
d5db9cf85401
replaced sorry by oops; removed old debug functions in predicate compiler
bulwahn
parents:
32672
diff
changeset
|
542 |
oops |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
543 |
|
33104 | 544 |
section {* Lambda *} |
32669
462b1dd67a58
added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo
bulwahn
parents:
32668
diff
changeset
|
545 |
|
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
546 |
datatype type = |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
547 |
Atom nat |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
548 |
| Fun type type (infixr "\<Rightarrow>" 200) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
549 |
|
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
550 |
datatype dB = |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
551 |
Var nat |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
552 |
| App dB dB (infixl "\<degree>" 200) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
553 |
| Abs type dB |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
554 |
|
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
555 |
primrec |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
556 |
nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a option" ("_\<langle>_\<rangle>" [90, 0] 91) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
557 |
where |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
558 |
"[]\<langle>i\<rangle> = None" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
559 |
| "(x # xs)\<langle>i\<rangle> = (case i of 0 \<Rightarrow> Some x | Suc j \<Rightarrow> xs \<langle>j\<rangle>)" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
560 |
|
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
561 |
(* |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
562 |
inductive nth_el' :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> bool" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
563 |
where |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
564 |
"nth_el' (x # xs) 0 x" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
565 |
| "nth_el' xs i y \<Longrightarrow> nth_el' (x # xs) (Suc i) y" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
566 |
*) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
567 |
inductive typing :: "type list \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ : _" [50, 50, 50] 50) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
568 |
where |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
569 |
Var [intro!]: "nth_el env x = Some T \<Longrightarrow> env \<turnstile> Var x : T" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
570 |
| Abs [intro!]: "T # env \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs T t : (T \<Rightarrow> U)" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
571 |
(* | App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U" *) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
572 |
| App [intro!]: "env \<turnstile> s : U \<Rightarrow> T \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
573 |
|
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
574 |
primrec |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
575 |
lift :: "[dB, nat] => dB" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
576 |
where |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
577 |
"lift (Var i) k = (if i < k then Var i else Var (i + 1))" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
578 |
| "lift (s \<degree> t) k = lift s k \<degree> lift t k" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
579 |
| "lift (Abs T s) k = Abs T (lift s (k + 1))" |
32669
462b1dd67a58
added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo
bulwahn
parents:
32668
diff
changeset
|
580 |
|
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
581 |
primrec |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
582 |
subst :: "[dB, dB, nat] => dB" ("_[_'/_]" [300, 0, 0] 300) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
583 |
where |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
584 |
subst_Var: "(Var i)[s/k] = |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
585 |
(if k < i then Var (i - 1) else if i = k then s else Var i)" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
586 |
| subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
587 |
| subst_Abs: "(Abs T t)[s/k] = Abs T (t[lift s 0 / k+1])" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
588 |
|
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
589 |
inductive beta :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<beta>" 50) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
590 |
where |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
591 |
beta [simp, intro!]: "Abs T s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
592 |
| appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
593 |
| appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
594 |
| abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs T s \<rightarrow>\<^sub>\<beta> Abs T t" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
595 |
|
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
596 |
lemma "Gamma \<turnstile> t : T \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> Gamma \<turnstile> t' : T" |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33120
diff
changeset
|
597 |
quickcheck[generator = pred_compile, size = 10, iterations = 100] |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
598 |
oops |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
599 |
|
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
600 |
lemma filter_eq_ConsD: |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
601 |
"filter P ys = x#xs \<Longrightarrow> |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
602 |
\<exists>us vs. ys = ts @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
603 |
(*quickcheck[generator = pred_compile]*) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32670
diff
changeset
|
604 |
oops |
32669
462b1dd67a58
added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo
bulwahn
parents:
32668
diff
changeset
|
605 |
|
462b1dd67a58
added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo
bulwahn
parents:
32668
diff
changeset
|
606 |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
607 |
end |