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 |
|
12867
|
10 |
theory Commutation = Main:
|
11042
|
11 |
|
|
12 |
constdefs
|
12867
|
13 |
square :: "[i, i, i, i] => o"
|
11042
|
14 |
"square(r,s,t,u) ==
|
12867
|
15 |
(\<forall>a b. <a,b> \<in> r --> (\<forall>c. <a, c> \<in> s --> (\<exists>x. <b,x> \<in> t & <c,x> \<in> u)))"
|
11042
|
16 |
|
12867
|
17 |
commute :: "[i, i] => o"
|
11042
|
18 |
"commute(r,s) == square(r,s,s,r)"
|
|
19 |
|
12867
|
20 |
diamond :: "i=>o"
|
|
21 |
"diamond(r) == commute(r, r)"
|
|
22 |
|
|
23 |
strip :: "i=>o"
|
|
24 |
"strip(r) == commute(r^*, r)"
|
|
25 |
|
|
26 |
Church_Rosser :: "i => o"
|
|
27 |
"Church_Rosser(r) == (\<forall>x y. <x,y> \<in> (r Un converse(r))^* -->
|
|
28 |
(\<exists>z. <x,z> \<in> r^* & <y,z> \<in> r^*))"
|
|
29 |
confluent :: "i=>o"
|
|
30 |
"confluent(r) == diamond(r^*)"
|
|
31 |
|
|
32 |
|
|
33 |
lemma square_sym: "square(r,s,t,u) ==> square(s,r,u,t)"
|
|
34 |
by (unfold square_def, blast)
|
|
35 |
|
|
36 |
lemma square_subset: "[| square(r,s,t,u); t \<subseteq> t' |] ==> square(r,s,t',u)"
|
|
37 |
by (unfold square_def, blast)
|
|
38 |
|
|
39 |
|
|
40 |
lemma square_rtrancl [rule_format]:
|
|
41 |
"square(r,s,s,t) --> field(s)<=field(t) --> square(r^*,s,s,t^*)"
|
|
42 |
apply (unfold square_def)
|
|
43 |
apply clarify
|
|
44 |
apply (erule rtrancl_induct)
|
|
45 |
apply (blast intro: rtrancl_refl)
|
|
46 |
apply (blast intro: rtrancl_into_rtrancl)
|
|
47 |
done
|
11042
|
48 |
|
12867
|
49 |
(* A special case of square_rtrancl_on *)
|
|
50 |
lemma diamond_strip:
|
|
51 |
"diamond(r) ==> strip(r)"
|
|
52 |
apply (unfold diamond_def commute_def strip_def)
|
|
53 |
apply (rule square_rtrancl)
|
|
54 |
apply simp_all
|
|
55 |
done
|
|
56 |
|
|
57 |
(*** commute ***)
|
|
58 |
|
|
59 |
lemma commute_sym:
|
|
60 |
"commute(r,s) ==> commute(s,r)"
|
|
61 |
by (unfold commute_def, blast intro: square_sym)
|
|
62 |
|
|
63 |
lemma commute_rtrancl [rule_format]:
|
|
64 |
"commute(r,s) ==> field(r)=field(s) --> commute(r^*,s^*)"
|
|
65 |
apply (unfold commute_def)
|
|
66 |
apply clarify
|
|
67 |
apply (rule square_rtrancl)
|
|
68 |
apply (rule square_sym [THEN square_rtrancl, THEN square_sym])
|
|
69 |
apply (simp_all add: rtrancl_field)
|
|
70 |
done
|
|
71 |
|
|
72 |
|
|
73 |
lemma confluentD: "confluent(r) ==> diamond(r^*)"
|
|
74 |
by (simp add: confluent_def)
|
|
75 |
|
|
76 |
lemma strip_confluent: "strip(r) ==> confluent(r)"
|
|
77 |
apply (unfold strip_def confluent_def diamond_def)
|
|
78 |
apply (drule commute_rtrancl)
|
|
79 |
apply (simp_all add: rtrancl_field)
|
|
80 |
done
|
|
81 |
|
|
82 |
lemma commute_Un: "[| commute(r,t); commute(s,t) |] ==> commute(r Un s, t)"
|
|
83 |
by (unfold commute_def square_def, blast)
|
11042
|
84 |
|
12867
|
85 |
lemma diamond_Un:
|
|
86 |
"[| diamond(r); diamond(s); commute(r, s) |] ==> diamond(r Un s)"
|
|
87 |
by (unfold diamond_def, blast intro: commute_Un commute_sym)
|
|
88 |
|
|
89 |
lemma diamond_confluent:
|
|
90 |
"diamond(r) ==> confluent(r)"
|
|
91 |
apply (unfold diamond_def confluent_def)
|
|
92 |
apply (erule commute_rtrancl)
|
|
93 |
apply simp
|
|
94 |
done
|
|
95 |
|
|
96 |
lemma confluent_Un:
|
|
97 |
"[| confluent(r); confluent(s); commute(r^*, s^*);
|
|
98 |
r \<subseteq> Sigma(A,B); s \<subseteq> Sigma(C,D) |] ==> confluent(r Un s)"
|
|
99 |
apply (unfold confluent_def)
|
|
100 |
apply (rule rtrancl_Un_rtrancl [THEN subst])
|
|
101 |
apply auto
|
|
102 |
apply (blast dest: diamond_Un intro: diamond_confluent [THEN confluentD])
|
|
103 |
done
|
|
104 |
|
|
105 |
|
|
106 |
lemma diamond_to_confluence:
|
|
107 |
"[| diamond(r); s \<subseteq> r; r<= s^* |] ==> confluent(s)"
|
|
108 |
apply (drule rtrancl_subset [symmetric])
|
|
109 |
apply assumption
|
|
110 |
apply (simp_all add: confluent_def)
|
|
111 |
apply (blast intro: diamond_confluent [THEN confluentD])
|
|
112 |
done
|
|
113 |
|
|
114 |
|
|
115 |
(*** Church_Rosser ***)
|
|
116 |
|
|
117 |
lemma Church_Rosser1:
|
|
118 |
"Church_Rosser(r) ==> confluent(r)"
|
|
119 |
apply (unfold confluent_def Church_Rosser_def square_def
|
|
120 |
commute_def diamond_def)
|
|
121 |
apply auto
|
|
122 |
apply (drule converseI)
|
|
123 |
apply (simp (no_asm_use) add: rtrancl_converse [symmetric])
|
|
124 |
apply (drule_tac x = "b" in spec)
|
|
125 |
apply (drule_tac x1 = "c" in spec [THEN mp])
|
|
126 |
apply (rule_tac b = "a" in rtrancl_trans)
|
|
127 |
apply (blast intro: rtrancl_mono [THEN subsetD])+
|
|
128 |
done
|
|
129 |
|
|
130 |
|
|
131 |
lemma Church_Rosser2:
|
|
132 |
"confluent(r) ==> Church_Rosser(r)"
|
|
133 |
apply (unfold confluent_def Church_Rosser_def square_def
|
|
134 |
commute_def diamond_def)
|
|
135 |
apply auto
|
|
136 |
apply (frule fieldI1)
|
|
137 |
apply (simp add: rtrancl_field)
|
|
138 |
apply (erule rtrancl_induct)
|
|
139 |
apply auto
|
|
140 |
apply (blast intro: rtrancl_refl)
|
|
141 |
apply (blast del: rtrancl_refl intro: r_into_rtrancl rtrancl_trans)+
|
|
142 |
done
|
|
143 |
|
|
144 |
|
|
145 |
lemma Church_Rosser: "Church_Rosser(r) <-> confluent(r)"
|
|
146 |
by (blast intro: Church_Rosser1 Church_Rosser2)
|
|
147 |
|
11042
|
148 |
end
|