7 |
7 |
8 open Conversion; |
8 open Conversion; |
9 |
9 |
10 AddIs (Sconv.intrs @ Sconv1.intrs); |
10 AddIs (Sconv.intrs @ Sconv1.intrs); |
11 |
11 |
12 goal Conversion.thy |
12 Goal |
13 "!!u. m<--->n ==> n<--->m"; |
13 "!!u. m<--->n ==> n<--->m"; |
14 by (etac Sconv.induct 1); |
14 by (etac Sconv.induct 1); |
15 by (etac Sconv1.induct 1); |
15 by (etac Sconv1.induct 1); |
16 by (ALLGOALS Blast_tac); |
16 by (ALLGOALS Blast_tac); |
17 qed "conv_sym"; |
17 qed "conv_sym"; |
18 |
18 |
19 (* ------------------------------------------------------------------------- *) |
19 (* ------------------------------------------------------------------------- *) |
20 (* Church_Rosser Theorem *) |
20 (* Church_Rosser Theorem *) |
21 (* ------------------------------------------------------------------------- *) |
21 (* ------------------------------------------------------------------------- *) |
22 |
22 |
23 goal Conversion.thy |
23 Goal |
24 "!!u. m<--->n ==> EX p.(m --->p) & (n ---> p)"; |
24 "!!u. m<--->n ==> EX p.(m --->p) & (n ---> p)"; |
25 by (etac Sconv.induct 1); |
25 by (etac Sconv.induct 1); |
26 by (etac Sconv1.induct 1); |
26 by (etac Sconv1.induct 1); |
27 by (blast_tac (claset() addIs [red1D1,redD2]) 1); |
27 by (blast_tac (claset() addIs [red1D1,redD2]) 1); |
28 by (blast_tac (claset() addIs [red1D1,redD2]) 1); |
28 by (blast_tac (claset() addIs [red1D1,redD2]) 1); |