author | bulwahn |
Tue, 04 Aug 2009 08:34:56 +0200 | |
changeset 32317 | b4b871808223 |
parent 32316 | 1d83ac469459 |
child 32318 | bca7fd849829 |
permissions | -rw-r--r-- |
31129
d2cead76fca2
split Predicate_Compile examples into separate theory
haftmann
parents:
31123
diff
changeset
|
1 |
theory Predicate_Compile_ex |
d2cead76fca2
split Predicate_Compile examples into separate theory
haftmann
parents:
31123
diff
changeset
|
2 |
imports Complex_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 |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
21 |
append_Nil: "append [] xs xs" |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
22 |
| append_Cons: "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)" |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
23 |
|
31514 | 24 |
inductive rev |
25 |
where |
|
26 |
"rev [] []" |
|
27 |
| "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys" |
|
28 |
||
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
|
29 |
code_pred rev . |
31123 | 30 |
|
31 |
thm append.equation |
|
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
32 |
|
31217 | 33 |
values "{(ys, xs). append xs ys [0, Suc 0, 2]}" |
34 |
values "{zs. append [0, Suc 0, 2] [17, 8] zs}" |
|
35 |
values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0,5]}" |
|
31195 | 36 |
|
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
37 |
|
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
38 |
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
|
39 |
for f where |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
40 |
"partition f [] [] []" |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
41 |
| "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
|
42 |
| "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)" |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
43 |
|
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
|
44 |
code_pred partition . |
31123 | 45 |
|
46 |
thm partition.equation |
|
32314
66bbad0bfef9
changed resolving depending predicates and fetching in the predicate compiler
bulwahn
parents:
32310
diff
changeset
|
47 |
|
66bbad0bfef9
changed resolving depending predicates and fetching in the predicate compiler
bulwahn
parents:
32310
diff
changeset
|
48 |
inductive is_even :: "nat \<Rightarrow> bool" |
66bbad0bfef9
changed resolving depending predicates and fetching in the predicate compiler
bulwahn
parents:
32310
diff
changeset
|
49 |
where |
66bbad0bfef9
changed resolving depending predicates and fetching in the predicate compiler
bulwahn
parents:
32310
diff
changeset
|
50 |
"n mod 2 = 0 \<Longrightarrow> is_even n" |
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 |
code_pred is_even . |
31123 | 53 |
|
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
|
54 |
(* TODO: requires to handle abstractions in parameter positions correctly *) |
32314
66bbad0bfef9
changed resolving depending predicates and fetching in the predicate compiler
bulwahn
parents:
32310
diff
changeset
|
55 |
values 10 "{(ys, zs). partition is_even |
66bbad0bfef9
changed resolving depending predicates and fetching in the predicate compiler
bulwahn
parents:
32310
diff
changeset
|
56 |
[0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}" |
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
|
57 |
|
32314
66bbad0bfef9
changed resolving depending predicates and fetching in the predicate compiler
bulwahn
parents:
32310
diff
changeset
|
58 |
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
|
59 |
values 10 "{zs. partition is_even zs [0, 7] [3, 5]}" |
31217 | 60 |
|
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
|
61 |
lemma [code_pred_intros]: |
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
|
62 |
"r a b ==> tranclp r a b" |
31876
9ab571673059
added diagnostic printing; changed proof for parameters; moved code
bulwahn
parents:
31580
diff
changeset
|
63 |
"r a b ==> tranclp r b c ==> tranclp r a c" |
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
|
64 |
by auto |
31573
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
65 |
|
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
66 |
code_pred tranclp |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
67 |
proof - |
31580 | 68 |
case tranclp |
69 |
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
|
70 |
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
|
71 |
|
31123 | 72 |
thm tranclp.equation |
32317 | 73 |
(* |
32316
1d83ac469459
added generator compilation of higher-order predicates; refined mode analysis for generators; some tuning
bulwahn
parents:
32314
diff
changeset
|
74 |
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
|
75 |
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
|
76 |
|
1d83ac469459
added generator compilation of higher-order predicates; refined mode analysis for generators; some tuning
bulwahn
parents:
32314
diff
changeset
|
77 |
thm tranclp.rpred_equation |
32317 | 78 |
*) |
31217 | 79 |
inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where |
80 |
"succ 0 1" |
|
81 |
| "succ m n \<Longrightarrow> succ (Suc m) (Suc n)" |
|
82 |
||
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
|
83 |
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
|
84 |
|
31217 | 85 |
thm succ.equation |
32314
66bbad0bfef9
changed resolving depending predicates and fetching in the predicate compiler
bulwahn
parents:
32310
diff
changeset
|
86 |
(* FIXME: why does this not terminate? -- value chooses mode [] --> [1] and then starts enumerating all successors *) |
31514 | 87 |
(* |
31217 | 88 |
values 20 "{n. tranclp succ 10 n}" |
89 |
values "{n. tranclp succ n 10}" |
|
90 |
values 20 "{(n, m). tranclp succ n m}" |
|
31514 | 91 |
*) |
31217 | 92 |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
93 |
end |