23 |
23 |
24 lemma strip_lemma_r: |
24 lemma strip_lemma_r: |
25 "[|confluence(Spar_red1)|]==> strip" |
25 "[|confluence(Spar_red1)|]==> strip" |
26 apply (unfold confluence_def strip_def) |
26 apply (unfold confluence_def strip_def) |
27 apply (rule impI [THEN allI, THEN allI]) |
27 apply (rule impI [THEN allI, THEN allI]) |
28 apply (erule Spar_red.induct) |
28 apply (erule Spar_red.induct, fast) |
29 apply fast |
|
30 apply (fast intro: Spar_red.trans) |
29 apply (fast intro: Spar_red.trans) |
31 done |
30 done |
32 |
31 |
33 |
32 |
34 lemma strip_lemma_l: |
33 lemma strip_lemma_l: |
35 "strip==> confluence(Spar_red)" |
34 "strip==> confluence(Spar_red)" |
36 apply (unfold confluence_def strip_def) |
35 apply (unfold confluence_def strip_def) |
37 apply (rule impI [THEN allI, THEN allI]) |
36 apply (rule impI [THEN allI, THEN allI]) |
38 apply (erule Spar_red.induct) |
37 apply (erule Spar_red.induct, blast) |
39 apply blast |
|
40 apply clarify |
38 apply clarify |
41 apply (blast intro: Spar_red.trans) |
39 apply (blast intro: Spar_red.trans) |
42 done |
40 done |
43 |
41 |
44 (* ------------------------------------------------------------------------- *) |
42 (* ------------------------------------------------------------------------- *) |
45 (* Confluence *) |
43 (* Confluence *) |
46 (* ------------------------------------------------------------------------- *) |
44 (* ------------------------------------------------------------------------- *) |
47 |
45 |
48 |
46 |
49 lemma parallel_moves: "confluence(Spar_red1)" |
47 lemma parallel_moves: "confluence(Spar_red1)" |
50 apply (unfold confluence_def) |
48 apply (unfold confluence_def, clarify) |
51 apply clarify |
|
52 apply (frule simulation) |
49 apply (frule simulation) |
53 apply (frule_tac n = "z" in simulation) |
50 apply (frule_tac n = z in simulation, clarify) |
54 apply clarify |
51 apply (frule_tac v = va in paving) |
55 apply (frule_tac v = "va" in paving) |
|
56 apply (force intro: completeness)+ |
52 apply (force intro: completeness)+ |
57 done |
53 done |
58 |
54 |
59 lemmas confluence_parallel_reduction = |
55 lemmas confluence_parallel_reduction = |
60 parallel_moves [THEN strip_lemma_r, THEN strip_lemma_l, standard] |
56 parallel_moves [THEN strip_lemma_r, THEN strip_lemma_l, standard] |
61 |
57 |
62 lemma lemma1: "[|confluence(Spar_red)|]==> confluence(Sred)" |
58 lemma lemma1: "[|confluence(Spar_red)|]==> confluence(Sred)" |
63 apply (unfold confluence_def, blast intro: par_red_red red_par_red) |
59 by (unfold confluence_def, blast intro: par_red_red red_par_red) |
64 done |
|
65 |
60 |
66 lemmas confluence_beta_reduction = |
61 lemmas confluence_beta_reduction = |
67 confluence_parallel_reduction [THEN lemma1, standard] |
62 confluence_parallel_reduction [THEN lemma1, standard] |
68 |
63 |
69 |
64 |
98 |
93 |
99 declare Sconv.intros [intro] |
94 declare Sconv.intros [intro] |
100 |
95 |
101 lemma conv_sym: "m<--->n ==> n<--->m" |
96 lemma conv_sym: "m<--->n ==> n<--->m" |
102 apply (erule Sconv.induct) |
97 apply (erule Sconv.induct) |
103 apply (erule Sconv1.induct) |
98 apply (erule Sconv1.induct, blast+) |
104 apply blast+ |
|
105 done |
99 done |
106 |
100 |
107 (* ------------------------------------------------------------------------- *) |
101 (* ------------------------------------------------------------------------- *) |
108 (* Church_Rosser Theorem *) |
102 (* Church_Rosser Theorem *) |
109 (* ------------------------------------------------------------------------- *) |
103 (* ------------------------------------------------------------------------- *) |