author | nipkow |
Mon, 04 Nov 1996 17:23:37 +0100 | |
changeset 2159 | e650a3f6f600 |
parent 1900 | c7a869229091 |
child 3001 | 8f89a99d2b00 |
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 |
||
1269 | 9 |
ParRed = Lambda + Commutation + |
1120 | 10 |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1900
diff
changeset
|
11 |
consts par_beta :: "(dB * dB) set" |
1120 | 12 |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1900
diff
changeset
|
13 |
syntax "=>" :: [dB,dB] => bool (infixl 50) |
1120 | 14 |
|
15 |
translations |
|
16 |
"s => t" == "(s,t) : par_beta" |
|
17 |
||
1789 | 18 |
inductive par_beta |
1120 | 19 |
intrs |
20 |
var "Var n => Var n" |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1900
diff
changeset
|
21 |
abs "s => t ==> Abs s => Abs t" |
1120 | 22 |
app "[| s => s'; t => t' |] ==> s @ t => s' @ t'" |
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1900
diff
changeset
|
23 |
beta "[| s => s'; t => t' |] ==> (Abs s) @ t => s'[t'/0]" |
1120 | 24 |
|
25 |
consts |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1900
diff
changeset
|
26 |
cd :: dB => dB |
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1900
diff
changeset
|
27 |
deAbs :: dB => dB |
1120 | 28 |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1900
diff
changeset
|
29 |
primrec cd dB |
1900 | 30 |
"cd(Var n) = Var n" |
31 |
"cd(s @ t) = (case s of |
|
1120 | 32 |
Var n => s @ (cd t) | |
33 |
s1 @ s2 => (cd s) @ (cd t) | |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1900
diff
changeset
|
34 |
Abs u => deAbs(cd s)[cd t/0])" |
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1900
diff
changeset
|
35 |
"cd(Abs s) = Abs(cd s)" |
1120 | 36 |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1900
diff
changeset
|
37 |
primrec deAbs dB |
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1900
diff
changeset
|
38 |
"deAbs(Var n) = Var n" |
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1900
diff
changeset
|
39 |
"deAbs(s @ t) = s @ t" |
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1900
diff
changeset
|
40 |
"deAbs(Abs s) = s" |
1120 | 41 |
end |