author | nipkow |
Mon, 22 May 1995 16:00:26 +0200 | |
changeset 1126 | 50ac36140e21 |
parent 1124 | a6233ea105a4 |
child 1269 | ee011b365770 |
permissions | -rw-r--r-- |
1120 | 1 |
(* Title: HOL/Lambda/ParRed.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1995 TU Muenchen |
|
5 |
||
6 |
Parallel reduction and a complete developments function "cd". |
|
7 |
*) |
|
8 |
||
9 |
ParRed = Lambda + Confluence + |
|
10 |
||
11 |
consts par_beta :: "(db * db) set" |
|
12 |
||
13 |
syntax "=>" :: "[db,db] => bool" (infixl 50) |
|
14 |
||
15 |
translations |
|
16 |
"s => t" == "(s,t) : par_beta" |
|
17 |
||
18 |
inductive "par_beta" |
|
19 |
intrs |
|
20 |
var "Var n => Var n" |
|
21 |
abs "s => t ==> Fun s => Fun t" |
|
22 |
app "[| s => s'; t => t' |] ==> s @ t => s' @ t'" |
|
1124
a6233ea105a4
Polished the presentation making it completely definitional.
nipkow
parents:
1120
diff
changeset
|
23 |
beta "[| s => s'; t => t' |] ==> (Fun s) @ t => s'[t'/0]" |
1120 | 24 |
|
25 |
consts |
|
26 |
cd :: "db => db" |
|
27 |
deFun :: "db => db" |
|
28 |
||
29 |
primrec cd db |
|
30 |
cd_Var "cd(Var n) = Var n" |
|
31 |
cd_App "cd(s @ t) = (case s of |
|
32 |
Var n => s @ (cd t) | |
|
33 |
s1 @ s2 => (cd s) @ (cd t) | |
|
1124
a6233ea105a4
Polished the presentation making it completely definitional.
nipkow
parents:
1120
diff
changeset
|
34 |
Fun u => deFun(cd s)[cd t/0])" |
1120 | 35 |
cd_Fun "cd(Fun s) = Fun(cd s)" |
36 |
||
37 |
primrec deFun db |
|
38 |
deFun_Var "deFun(Var n) = Var n" |
|
39 |
deFun_App "deFun(s @ t) = s @ t" |
|
40 |
deFun_Fun "deFun(Fun s) = s" |
|
41 |
end |