author | haftmann |
Wed, 20 May 2009 22:24:07 +0200 | |
changeset 31217 | c025f32afd4e |
parent 31195 | 12741f23527d |
child 31514 | fed8a95f54db |
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 |
|
31123 | 10 |
code_pred even |
11 |
using assms by (rule even.cases) |
|
12 |
||
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 |
|
31123 | 25 |
code_pred append |
26 |
using assms by (rule append.cases) |
|
27 |
||
28 |
thm append.equation |
|
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
29 |
|
31217 | 30 |
values "{(ys, xs). append xs ys [0, Suc 0, 2]}" |
31 |
values "{zs. append [0, Suc 0, 2] [17, 8] zs}" |
|
32 |
values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0,5]}" |
|
31195 | 33 |
|
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
34 |
|
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
35 |
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
|
36 |
for f where |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
37 |
"partition f [] [] []" |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
38 |
| "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
|
39 |
| "\<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
|
40 |
|
31123 | 41 |
code_pred partition |
42 |
using assms by (rule partition.cases) |
|
43 |
||
44 |
thm partition.equation |
|
45 |
||
31217 | 46 |
(*FIXME values 10 "{(ys, zs). partition (\<lambda>n. n mod 2 = 0) |
47 |
[0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"*) |
|
48 |
||
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset
|
49 |
|
31123 | 50 |
code_pred tranclp |
51 |
using assms by (rule tranclp.cases) |
|
52 |
||
53 |
thm tranclp.equation |
|
54 |
||
31217 | 55 |
inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where |
56 |
"succ 0 1" |
|
57 |
| "succ m n \<Longrightarrow> succ (Suc m) (Suc n)" |
|
58 |
||
59 |
code_pred succ |
|
60 |
using assms by (rule succ.cases) |
|
61 |
||
62 |
thm succ.equation |
|
63 |
||
64 |
values 20 "{n. tranclp succ 10 n}" |
|
65 |
values "{n. tranclp succ n 10}" |
|
66 |
values 20 "{(n, m). tranclp succ n m}" |
|
67 |
||
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
68 |
end |