|
11042
|
1 |
(* Title: HOL/Lambda/Commutation.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow & Sidi Ould Ehmety
|
|
|
4 |
Copyright 1995 TU Muenchen
|
|
|
5 |
|
|
|
6 |
Commutation theory for proving the Church Rosser theorem
|
|
|
7 |
ported from Isabelle/HOL by Sidi Ould Ehmety
|
|
|
8 |
*)
|
|
|
9 |
|
|
|
10 |
Commutation = Main +
|
|
|
11 |
|
|
|
12 |
constdefs
|
|
|
13 |
square :: [i, i, i, i] => o
|
|
|
14 |
"square(r,s,t,u) ==
|
|
11316
|
15 |
(\\<forall>a b. <a,b>:r --> (\\<forall>c. <a, c>:s
|
|
|
16 |
--> (\\<exists>x. <b,x>:t & <c,x>:u)))"
|
|
11042
|
17 |
|
|
|
18 |
commute :: [i, i] => o
|
|
|
19 |
"commute(r,s) == square(r,s,s,r)"
|
|
|
20 |
|
|
|
21 |
diamond :: i=>o
|
|
|
22 |
"diamond(r) == commute(r, r)"
|
|
|
23 |
|
|
|
24 |
strip :: i=>o
|
|
|
25 |
"strip(r) == commute(r^*, r)"
|
|
|
26 |
|
|
|
27 |
Church_Rosser :: i => o
|
|
11316
|
28 |
"Church_Rosser(r) == (\\<forall>x y. <x,y>: (r Un converse(r))^* -->
|
|
|
29 |
(\\<exists>z. <x,z>:r^* & <y,z>:r^*))"
|
|
11042
|
30 |
confluent :: i=>o
|
|
|
31 |
"confluent(r) == diamond(r^*)"
|
|
|
32 |
end
|