author | nipkow |
Wed, 15 Jul 1998 12:02:19 +0200 | |
changeset 5146 | 1ea751ae62b2 |
parent 5134 | 51f81581e3d9 |
child 8624 | 69619f870939 |
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 |
||
5134 | 9 |
ParRed = Lambda + Commutation + Recdef + |
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" |
5146 | 22 |
app "[| s => s'; t => t' |] ==> s $ t => s' $ t'" |
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 |
1120 | 27 |
|
5134 | 28 |
recdef cd "measure size" |
1900 | 29 |
"cd(Var n) = Var n" |
5146 | 30 |
"cd(Var n $ t) = Var n $ cd t" |
31 |
"cd((s1 $ s2) $ t) = cd(s1 $ s2) $ cd t" |
|
32 |
"cd(Abs u $ t) = (cd u)[cd t/0]" |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1900
diff
changeset
|
33 |
"cd(Abs s) = Abs(cd s)" |
1120 | 34 |
end |