author | haftmann |
Thu, 28 Jan 2010 11:48:49 +0100 | |
changeset 34974 | 18b41bba42b5 |
parent 21425 | c11ab38b78a7 |
child 35265 | 3fd8c3edf639 |
permissions | -rw-r--r-- |
13208 | 1 |
(* Title: HOL/Prolog/Func.thy |
2 |
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) |
|
3 |
*) |
|
9015 | 4 |
|
17311 | 5 |
header {* Untyped functional language, with call by value semantics *} |
9015 | 6 |
|
17311 | 7 |
theory Func |
34974
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
21425
diff
changeset
|
8 |
imports HOHH Algebras |
17311 | 9 |
begin |
9015 | 10 |
|
17311 | 11 |
typedecl tm |
9015 | 12 |
|
17311 | 13 |
consts |
14 |
abs :: "(tm => tm) => tm" |
|
15 |
app :: "tm => tm => tm" |
|
16 |
||
17 |
cond :: "tm => tm => tm => tm" |
|
18 |
"fix" :: "(tm => tm) => tm" |
|
9015 | 19 |
|
17311 | 20 |
true :: tm |
21 |
false :: tm |
|
21425 | 22 |
"and" :: "tm => tm => tm" (infixr "and" 999) |
23 |
eq :: "tm => tm => tm" (infixr "eq" 999) |
|
9015 | 24 |
|
20713
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
17311
diff
changeset
|
25 |
Z :: tm ("Z") |
17311 | 26 |
S :: "tm => tm" |
9015 | 27 |
(* |
17311 | 28 |
"++", "--", |
29 |
"**" :: tm => tm => tm (infixr 999) |
|
9015 | 30 |
*) |
17311 | 31 |
eval :: "[tm, tm] => bool" |
9015 | 32 |
|
17311 | 33 |
instance tm :: plus .. |
34 |
instance tm :: minus .. |
|
35 |
instance tm :: times .. |
|
9015 | 36 |
|
17311 | 37 |
axioms eval: " |
9015 | 38 |
|
39 |
eval (abs RR) (abs RR).. |
|
40 |
eval (app F X) V :- eval F (abs R) & eval X U & eval (R U) V.. |
|
41 |
||
42 |
eval (cond P L1 R1) D1 :- eval P true & eval L1 D1.. |
|
43 |
eval (cond P L2 R2) D2 :- eval P false & eval R2 D2.. |
|
44 |
eval (fix G) W :- eval (G (fix G)) W.. |
|
45 |
||
46 |
eval true true .. |
|
47 |
eval false false.. |
|
48 |
eval (P and Q) true :- eval P true & eval Q true .. |
|
49 |
eval (P and Q) false :- eval P false | eval Q false.. |
|
17311 | 50 |
eval (A1 eq B1) true :- eval A1 C1 & eval B1 C1.. |
9015 | 51 |
eval (A2 eq B2) false :- True.. |
52 |
||
53 |
eval Z Z.. |
|
54 |
eval (S N) (S M) :- eval N M.. |
|
55 |
eval ( Z + M) K :- eval M K.. |
|
56 |
eval ((S N) + M) (S K) :- eval (N + M) K.. |
|
57 |
eval (N - Z) K :- eval N K.. |
|
58 |
eval ((S N) - (S M)) K :- eval (N- M) K.. |
|
59 |
eval ( Z * M) Z.. |
|
60 |
eval ((S N) * M) K :- eval (N * M) L & eval (L + M) K" |
|
61 |
||
21425 | 62 |
|
63 |
lemmas prog_Func = eval |
|
64 |
||
65 |
lemma "eval ((S (S Z)) + (S Z)) ?X" |
|
66 |
apply (prolog prog_Func) |
|
67 |
done |
|
68 |
||
69 |
lemma "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z) |
|
70 |
(n * (app fact (n - (S Z))))))) (S (S (S Z)))) ?X" |
|
71 |
apply (prolog prog_Func) |
|
72 |
done |
|
17311 | 73 |
|
9015 | 74 |
end |