author | haftmann |
Tue, 14 Jul 2009 16:27:32 +0200 | |
changeset 32069 | 6d28bbd33e2c |
parent 31879 | 39bff8d9b032 |
child 32310 | 89f3c616a2d1 |
child 32340 | b4632820e74c |
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 |
|
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
21 |
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
|
22 |
append_Nil: "append [] xs xs" |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
23 |
| 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
|
24 |
|
31514 | 25 |
inductive rev |
26 |
where |
|
27 |
"rev [] []" |
|
28 |
| "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys" |
|
29 |
||
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
|
30 |
code_pred rev . |
31123 | 31 |
|
32 |
thm append.equation |
|
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
33 |
|
31217 | 34 |
values "{(ys, xs). append xs ys [0, Suc 0, 2]}" |
35 |
values "{zs. append [0, Suc 0, 2] [17, 8] zs}" |
|
36 |
values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0,5]}" |
|
31195 | 37 |
|
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
38 |
|
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
39 |
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
|
40 |
for f where |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
41 |
"partition f [] [] []" |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
42 |
| "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
|
43 |
| "\<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
|
44 |
|
31551
995d6b90e9d6
making isatest happy; but misunderstanding remains
bulwahn
parents:
31550
diff
changeset
|
45 |
(* FIXME: correct handling of parameters *) |
995d6b90e9d6
making isatest happy; but misunderstanding remains
bulwahn
parents:
31550
diff
changeset
|
46 |
(* |
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
|
47 |
ML {* reset Predicate_Compile.do_proofs *} |
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 |
|
31551
995d6b90e9d6
making isatest happy; but misunderstanding remains
bulwahn
parents:
31550
diff
changeset
|
51 |
ML {* set Predicate_Compile.do_proofs *} |
995d6b90e9d6
making isatest happy; but misunderstanding remains
bulwahn
parents:
31550
diff
changeset
|
52 |
*) |
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 *) |
31217 | 55 |
(*FIXME values 10 "{(ys, zs). partition (\<lambda>n. n mod 2 = 0) |
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
|
56 |
[0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}" *) |
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 |
|
31217 | 58 |
|
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
|
59 |
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
|
60 |
"r a b ==> tranclp r a b" |
31876
9ab571673059
added diagnostic printing; changed proof for parameters; moved code
bulwahn
parents:
31580
diff
changeset
|
61 |
"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
|
62 |
by auto |
31573
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
63 |
|
31575 | 64 |
(* Setup requires quick and dirty proof *) |
31879 | 65 |
(* |
31573
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 |
31879 | 73 |
*) |
31217 | 74 |
inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where |
75 |
"succ 0 1" |
|
76 |
| "succ m n \<Longrightarrow> succ (Suc m) (Suc n)" |
|
77 |
||
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
|
78 |
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
|
79 |
|
31217 | 80 |
thm succ.equation |
31573
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
81 |
(* FIXME: why does this not terminate? *) |
31514 | 82 |
(* |
31217 | 83 |
values 20 "{n. tranclp succ 10 n}" |
84 |
values "{n. tranclp succ n 10}" |
|
85 |
values 20 "{(n, m). tranclp succ n m}" |
|
31514 | 86 |
*) |
31217 | 87 |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
88 |
end |