author | bulwahn |
Wed, 23 Sep 2009 16:20:12 +0200 | |
changeset 32665 | 8bf46a97ff79 |
parent 32579 | 73ad5dbf1034 |
child 32668 | b2de45007537 |
permissions | -rw-r--r-- |
31129
d2cead76fca2
split Predicate_Compile examples into separate theory
haftmann
parents:
31123
diff
changeset
|
1 |
theory Predicate_Compile_ex |
32318
bca7fd849829
improved use of context with cases rule in predicate compiler; predicate compiler based on Main for faster debugging
bulwahn
parents:
32317
diff
changeset
|
2 |
imports Main Predicate_Compile |
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 |
|
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
|
10 |
code_pred even . |
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 |
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
14 |
|
31217 | 15 |
values "{x. even 2}" |
16 |
values "{x. odd 2}" |
|
17 |
values 10 "{n. even n}" |
|
18 |
values 10 "{n. odd n}" |
|
31195 | 19 |
|
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
20 |
inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where |
32340 | 21 |
"append [] xs xs" |
22 |
| "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
|
23 |
|
32340 | 24 |
code_pred append . |
31123 | 25 |
|
26 |
thm append.equation |
|
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
27 |
|
31217 | 28 |
values "{(ys, xs). append xs ys [0, Suc 0, 2]}" |
29 |
values "{zs. append [0, Suc 0, 2] [17, 8] zs}" |
|
30 |
values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0,5]}" |
|
31195 | 31 |
|
32340 | 32 |
inductive rev where |
33 |
"rev [] []" |
|
34 |
| "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys" |
|
35 |
||
36 |
code_pred rev . |
|
37 |
||
38 |
thm rev.equation |
|
39 |
||
40 |
values "{xs. rev [0, 1, 2, 3::nat] xs}" |
|
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
41 |
|
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
42 |
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
|
43 |
for f where |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
44 |
"partition f [] [] []" |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
45 |
| "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
|
46 |
| "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)" |
32665
8bf46a97ff79
extending predicate compiler and proof procedure to support tuples; testing predicate wirh HOL-MicroJava semantics
bulwahn
parents:
32579
diff
changeset
|
47 |
ML {* set Toplevel.debug *} |
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
|
48 |
code_pred partition . |
31123 | 49 |
|
50 |
thm partition.equation |
|
32314
66bbad0bfef9
changed resolving depending predicates and fetching in the predicate compiler
bulwahn
parents:
32310
diff
changeset
|
51 |
|
66bbad0bfef9
changed resolving depending predicates and fetching in the predicate compiler
bulwahn
parents:
32310
diff
changeset
|
52 |
inductive is_even :: "nat \<Rightarrow> bool" |
66bbad0bfef9
changed resolving depending predicates and fetching in the predicate compiler
bulwahn
parents:
32310
diff
changeset
|
53 |
where |
66bbad0bfef9
changed resolving depending predicates and fetching in the predicate compiler
bulwahn
parents:
32310
diff
changeset
|
54 |
"n mod 2 = 0 \<Longrightarrow> is_even n" |
66bbad0bfef9
changed resolving depending predicates and fetching in the predicate compiler
bulwahn
parents:
32310
diff
changeset
|
55 |
|
66bbad0bfef9
changed resolving depending predicates and fetching in the predicate compiler
bulwahn
parents:
32310
diff
changeset
|
56 |
code_pred is_even . |
31123 | 57 |
|
32314
66bbad0bfef9
changed resolving depending predicates and fetching in the predicate compiler
bulwahn
parents:
32310
diff
changeset
|
58 |
values 10 "{(ys, zs). partition is_even |
66bbad0bfef9
changed resolving depending predicates and fetching in the predicate compiler
bulwahn
parents:
32310
diff
changeset
|
59 |
[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
|
60 |
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
|
61 |
values 10 "{zs. partition is_even zs [0, 7] [3, 5]}" |
31217 | 62 |
|
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
|
63 |
lemma [code_pred_intros]: |
32340 | 64 |
"r a b \<Longrightarrow> tranclp r a b" |
65 |
"r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c" |
|
66 |
by auto |
|
31573
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
67 |
|
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
68 |
code_pred tranclp |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
69 |
proof - |
31580 | 70 |
case tranclp |
71 |
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
|
72 |
qed |
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
|
73 |
|
31123 | 74 |
thm tranclp.equation |
32317 | 75 |
(* |
32316
1d83ac469459
added generator compilation of higher-order predicates; refined mode analysis for generators; some tuning
bulwahn
parents:
32314
diff
changeset
|
76 |
setup {* Predicate_Compile.add_sizelim_equations [@{const_name tranclp}] *} |
1d83ac469459
added generator compilation of higher-order predicates; refined mode analysis for generators; some tuning
bulwahn
parents:
32314
diff
changeset
|
77 |
setup {* fn thy => exception_trace (fn () => Predicate_Compile.add_quickcheck_equations [@{const_name tranclp}] thy) *} |
1d83ac469459
added generator compilation of higher-order predicates; refined mode analysis for generators; some tuning
bulwahn
parents:
32314
diff
changeset
|
78 |
|
1d83ac469459
added generator compilation of higher-order predicates; refined mode analysis for generators; some tuning
bulwahn
parents:
32314
diff
changeset
|
79 |
thm tranclp.rpred_equation |
32317 | 80 |
*) |
32340 | 81 |
|
31217 | 82 |
inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where |
83 |
"succ 0 1" |
|
84 |
| "succ m n \<Longrightarrow> succ (Suc m) (Suc n)" |
|
85 |
||
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
|
86 |
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
|
87 |
|
31217 | 88 |
thm succ.equation |
32340 | 89 |
|
90 |
values 10 "{(m, n). succ n m}" |
|
91 |
values "{m. succ 0 m}" |
|
92 |
values "{m. succ m 0}" |
|
93 |
||
32314
66bbad0bfef9
changed resolving depending predicates and fetching in the predicate compiler
bulwahn
parents:
32310
diff
changeset
|
94 |
(* FIXME: why does this not terminate? -- value chooses mode [] --> [1] and then starts enumerating all successors *) |
32355 | 95 |
|
31514 | 96 |
(* |
31217 | 97 |
values 20 "{n. tranclp succ 10 n}" |
98 |
values "{n. tranclp succ n 10}" |
|
99 |
values 20 "{(n, m). tranclp succ n m}" |
|
31514 | 100 |
*) |
31217 | 101 |
|
32424 | 102 |
subsection{* IMP *} |
103 |
||
104 |
types |
|
105 |
var = nat |
|
106 |
state = "int list" |
|
107 |
||
108 |
datatype com = |
|
109 |
Skip | |
|
110 |
Ass var "state => int" | |
|
111 |
Seq com com | |
|
112 |
IF "state => bool" com com | |
|
113 |
While "state => bool" com |
|
114 |
||
115 |
inductive exec :: "com => state => state => bool" where |
|
116 |
"exec Skip s s" | |
|
117 |
"exec (Ass x e) s (s[x := e(s)])" | |
|
118 |
"exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" | |
|
119 |
"b s ==> exec c1 s t ==> exec (IF b c1 c2) s t" | |
|
120 |
"~b s ==> exec c2 s t ==> exec (IF b c1 c2) s t" | |
|
121 |
"~b s ==> exec (While b c) s s" | |
|
122 |
"b s1 ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3" |
|
123 |
||
124 |
code_pred exec . |
|
125 |
||
126 |
values "{t. exec |
|
127 |
(While (%s. s!0 > 0) (Seq (Ass 0 (%s. s!0 - 1)) (Ass 1 (%s. s!1 + 1)))) |
|
128 |
[3,5] t}" |
|
129 |
||
130 |
||
32408 | 131 |
subsection{* CCS *} |
132 |
||
133 |
text{* This example formalizes finite CCS processes without communication or |
|
134 |
recursion. For simplicity, labels are natural numbers. *} |
|
135 |
||
136 |
datatype proc = nil | pre nat proc | or proc proc | par proc proc |
|
137 |
||
138 |
inductive step :: "proc \<Rightarrow> nat \<Rightarrow> proc \<Rightarrow> bool" where |
|
139 |
"step (pre n p) n p" | |
|
140 |
"step p1 a q \<Longrightarrow> step (or p1 p2) a q" | |
|
141 |
"step p2 a q \<Longrightarrow> step (or p1 p2) a q" | |
|
142 |
"step p1 a q \<Longrightarrow> step (par p1 p2) a (par q p2)" | |
|
143 |
"step p2 a q \<Longrightarrow> step (par p1 p2) a (par p1 q)" |
|
144 |
||
145 |
code_pred step . |
|
146 |
||
147 |
inductive steps where |
|
148 |
"steps p [] p" | |
|
149 |
"step p a q \<Longrightarrow> steps q as r \<Longrightarrow> steps p (a#as) r" |
|
150 |
||
151 |
code_pred steps . |
|
152 |
||
153 |
values 5 |
|
154 |
"{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}" |
|
155 |
||
156 |
(* FIXME |
|
157 |
values 3 "{(a,q). step (par nil nil) a q}" |
|
158 |
*) |
|
159 |
||
32579 | 160 |
|
161 |
inductive divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where |
|
162 |
"k < l \<Longrightarrow> divmod_rel k l 0 k" |
|
163 |
| "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r" |
|
164 |
||
165 |
code_pred divmod_rel .. |
|
166 |
||
167 |
value [code] "Predicate.singleton (divmod_rel_1_2 1705 42)" |
|
168 |
||
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
169 |
end |