7 |
7 |
8 open Conversion; |
8 open Conversion; |
9 |
9 |
10 val conv_ss = reduc_ss addsimps (Sconv1.intrs@[Sconv.one_step,Sconv.refl]); |
10 val conv_ss = reduc_ss addsimps (Sconv1.intrs@[Sconv.one_step,Sconv.refl]); |
11 |
11 |
12 val conv1_induct = Sconv1.mutual_induct RS spec RS spec RSN (2,rev_mp); |
|
13 val conv_induct = Sconv.mutual_induct RS spec RS spec RSN (2,rev_mp); |
|
14 |
|
15 goal Conversion.thy |
12 goal Conversion.thy |
16 "!!u.m<--->n ==> n<--->m"; |
13 "!!u.m<--->n ==> n<--->m"; |
17 by (etac conv_induct 1); |
14 by (etac Sconv.induct 1); |
18 by (etac conv1_induct 1); |
15 by (etac Sconv1.induct 1); |
19 by (resolve_tac [Sconv.trans] 4); |
16 by (resolve_tac [Sconv.trans] 4); |
20 by (ALLGOALS(asm_simp_tac (conv_ss) )); |
17 by (ALLGOALS(asm_simp_tac (conv_ss) )); |
21 val conv_sym = result(); |
18 val conv_sym = result(); |
22 |
19 |
23 (* ------------------------------------------------------------------------- *) |
20 (* ------------------------------------------------------------------------- *) |
24 (* Church_Rosser Theorem *) |
21 (* Church_Rosser Theorem *) |
25 (* ------------------------------------------------------------------------- *) |
22 (* ------------------------------------------------------------------------- *) |
26 |
23 |
27 goal Conversion.thy |
24 goal Conversion.thy |
28 "!!u.m<--->n ==> EX p.(m --->p) & (n ---> p)"; |
25 "!!u.m<--->n ==> EX p.(m --->p) & (n ---> p)"; |
29 by (etac conv_induct 1); |
26 by (etac Sconv.induct 1); |
30 by (etac conv1_induct 1); |
27 by (etac Sconv1.induct 1); |
31 by (fast_tac (reduc_cs addIs [red1D1,redD2]) 1); |
28 by (fast_tac (reduc_cs addIs [red1D1,redD2]) 1); |
32 by (fast_tac (reduc_cs addIs [red1D1,redD2]) 1); |
29 by (fast_tac (reduc_cs addIs [red1D1,redD2]) 1); |
33 by (fast_tac (reduc_cs addIs [red1D1,redD2]) 1); |
30 by (fast_tac (reduc_cs addIs [red1D1,redD2]) 1); |
34 by (cut_facts_tac [confluence_beta_reduction] 1); |
31 by (cut_facts_tac [confluence_beta_reduction] 1); |
35 by (rewtac confluence_def); |
32 by (rewtac confluence_def); |