author | paulson <lp15@cam.ac.uk> |
Tue, 27 Sep 2022 18:02:34 +0100 | |
changeset 76217 | 8655344f1cf6 |
parent 76216 | 9fc34f76b4e8 |
child 76219 | cf7db6353322 |
permissions | -rw-r--r-- |
41777 | 1 |
(* Title: ZF/ex/Commutation.thy |
76214 | 2 |
Author: Tobias Nipkow \<and> Sidi Ould Ehmety |
11042 | 3 |
Copyright 1995 TU Muenchen |
4 |
||
35762 | 5 |
Commutation theory for proving the Church Rosser theorem. |
11042 | 6 |
*) |
7 |
||
65449
c82e63b11b8b
clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;
wenzelm
parents:
46822
diff
changeset
|
8 |
theory Commutation imports ZF begin |
11042 | 9 |
|
21233 | 10 |
definition |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
11 |
square :: "[i, i, i, i] \<Rightarrow> o" where |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
12 |
"square(r,s,t,u) \<equiv> |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
13 |
(\<forall>a b. \<langle>a,b\<rangle> \<in> r \<longrightarrow> (\<forall>c. \<langle>a, c\<rangle> \<in> s \<longrightarrow> (\<exists>x. \<langle>b,x\<rangle> \<in> t \<and> \<langle>c,x\<rangle> \<in> u)))" |
11042 | 14 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
15 |
definition |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
16 |
commute :: "[i, i] \<Rightarrow> o" where |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
17 |
"commute(r,s) \<equiv> square(r,s,s,r)" |
11042 | 18 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
19 |
definition |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
20 |
diamond :: "i\<Rightarrow>o" where |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
21 |
"diamond(r) \<equiv> commute(r, r)" |
12867 | 22 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
23 |
definition |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
24 |
strip :: "i\<Rightarrow>o" where |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
25 |
"strip(r) \<equiv> commute(r^*, r)" |
12867 | 26 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
27 |
definition |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
28 |
Church_Rosser :: "i \<Rightarrow> o" where |
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
29 |
"Church_Rosser(r) \<equiv> (\<forall>x y. \<langle>x,y\<rangle> \<in> (r \<union> converse(r))^* \<longrightarrow> |
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
30 |
(\<exists>z. \<langle>x,z\<rangle> \<in> r^* \<and> \<langle>y,z\<rangle> \<in> r^*))" |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
31 |
|
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
32 |
definition |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
33 |
confluent :: "i\<Rightarrow>o" where |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
34 |
"confluent(r) \<equiv> diamond(r^*)" |
12867 | 35 |
|
36 |
||
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
37 |
lemma square_sym: "square(r,s,t,u) \<Longrightarrow> square(s,r,u,t)" |
21233 | 38 |
unfolding square_def by blast |
12867 | 39 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
40 |
lemma square_subset: "\<lbrakk>square(r,s,t,u); t \<subseteq> t'\<rbrakk> \<Longrightarrow> square(r,s,t',u)" |
21233 | 41 |
unfolding square_def by blast |
12867 | 42 |
|
43 |
||
21233 | 44 |
lemma square_rtrancl: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
45 |
"square(r,s,s,t) \<Longrightarrow> field(s)<=field(t) \<Longrightarrow> square(r^*,s,s,t^*)" |
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13248
diff
changeset
|
46 |
apply (unfold square_def, clarify) |
12867 | 47 |
apply (erule rtrancl_induct) |
48 |
apply (blast intro: rtrancl_refl) |
|
49 |
apply (blast intro: rtrancl_into_rtrancl) |
|
50 |
done |
|
11042 | 51 |
|
12867 | 52 |
(* A special case of square_rtrancl_on *) |
21233 | 53 |
lemma diamond_strip: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
54 |
"diamond(r) \<Longrightarrow> strip(r)" |
76217 | 55 |
unfolding diamond_def commute_def strip_def |
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13248
diff
changeset
|
56 |
apply (rule square_rtrancl, simp_all) |
12867 | 57 |
done |
58 |
||
59 |
(*** commute ***) |
|
60 |
||
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
61 |
lemma commute_sym: "commute(r,s) \<Longrightarrow> commute(s,r)" |
21233 | 62 |
unfolding commute_def by (blast intro: square_sym) |
12867 | 63 |
|
21233 | 64 |
lemma commute_rtrancl: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
65 |
"commute(r,s) \<Longrightarrow> field(r)=field(s) \<Longrightarrow> commute(r^*,s^*)" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
66 |
unfolding commute_def |
12867 | 67 |
apply (rule square_rtrancl) |
21233 | 68 |
apply (rule square_sym [THEN square_rtrancl, THEN square_sym]) |
12867 | 69 |
apply (simp_all add: rtrancl_field) |
70 |
done |
|
71 |
||
72 |
||
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
73 |
lemma confluentD: "confluent(r) \<Longrightarrow> diamond(r^*)" |
12867 | 74 |
by (simp add: confluent_def) |
75 |
||
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
76 |
lemma strip_confluent: "strip(r) \<Longrightarrow> confluent(r)" |
76217 | 77 |
unfolding strip_def confluent_def diamond_def |
12867 | 78 |
apply (drule commute_rtrancl) |
79 |
apply (simp_all add: rtrancl_field) |
|
80 |
done |
|
81 |
||
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
82 |
lemma commute_Un: "\<lbrakk>commute(r,t); commute(s,t)\<rbrakk> \<Longrightarrow> commute(r \<union> s, t)" |
21233 | 83 |
unfolding commute_def square_def by blast |
11042 | 84 |
|
21233 | 85 |
lemma diamond_Un: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
86 |
"\<lbrakk>diamond(r); diamond(s); commute(r, s)\<rbrakk> \<Longrightarrow> diamond(r \<union> s)" |
21233 | 87 |
unfolding diamond_def by (blast intro: commute_Un commute_sym) |
12867 | 88 |
|
21233 | 89 |
lemma diamond_confluent: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
90 |
"diamond(r) \<Longrightarrow> confluent(r)" |
76217 | 91 |
unfolding diamond_def confluent_def |
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13248
diff
changeset
|
92 |
apply (erule commute_rtrancl, simp) |
12867 | 93 |
done |
94 |
||
21233 | 95 |
lemma confluent_Un: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
96 |
"\<lbrakk>confluent(r); confluent(s); commute(r^*, s^*); |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
97 |
relation(r); relation(s)\<rbrakk> \<Longrightarrow> confluent(r \<union> s)" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
98 |
unfolding confluent_def |
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13248
diff
changeset
|
99 |
apply (rule rtrancl_Un_rtrancl [THEN subst], auto) |
12867 | 100 |
apply (blast dest: diamond_Un intro: diamond_confluent [THEN confluentD]) |
101 |
done |
|
102 |
||
103 |
||
21233 | 104 |
lemma diamond_to_confluence: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
105 |
"\<lbrakk>diamond(r); s \<subseteq> r; r<= s^*\<rbrakk> \<Longrightarrow> confluent(s)" |
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13248
diff
changeset
|
106 |
apply (drule rtrancl_subset [symmetric], assumption) |
12867 | 107 |
apply (simp_all add: confluent_def) |
108 |
apply (blast intro: diamond_confluent [THEN confluentD]) |
|
109 |
done |
|
110 |
||
111 |
||
112 |
(*** Church_Rosser ***) |
|
113 |
||
21233 | 114 |
lemma Church_Rosser1: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
115 |
"Church_Rosser(r) \<Longrightarrow> confluent(r)" |
21233 | 116 |
apply (unfold confluent_def Church_Rosser_def square_def |
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13248
diff
changeset
|
117 |
commute_def diamond_def, auto) |
12867 | 118 |
apply (drule converseI) |
119 |
apply (simp (no_asm_use) add: rtrancl_converse [symmetric]) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13248
diff
changeset
|
120 |
apply (drule_tac x = b in spec) |
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13248
diff
changeset
|
121 |
apply (drule_tac x1 = c in spec [THEN mp]) |
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13248
diff
changeset
|
122 |
apply (rule_tac b = a in rtrancl_trans) |
12867 | 123 |
apply (blast intro: rtrancl_mono [THEN subsetD])+ |
124 |
done |
|
125 |
||
126 |
||
21233 | 127 |
lemma Church_Rosser2: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
128 |
"confluent(r) \<Longrightarrow> Church_Rosser(r)" |
21233 | 129 |
apply (unfold confluent_def Church_Rosser_def square_def |
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13248
diff
changeset
|
130 |
commute_def diamond_def, auto) |
12867 | 131 |
apply (frule fieldI1) |
132 |
apply (simp add: rtrancl_field) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13248
diff
changeset
|
133 |
apply (erule rtrancl_induct, auto) |
12867 | 134 |
apply (blast intro: rtrancl_refl) |
135 |
apply (blast del: rtrancl_refl intro: r_into_rtrancl rtrancl_trans)+ |
|
136 |
done |
|
137 |
||
138 |
||
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
41777
diff
changeset
|
139 |
lemma Church_Rosser: "Church_Rosser(r) \<longleftrightarrow> confluent(r)" |
21233 | 140 |
by (blast intro: Church_Rosser1 Church_Rosser2) |
12867 | 141 |
|
21233 | 142 |
end |