author | berghofe |
Thu, 11 Jul 2002 16:57:14 +0200 | |
changeset 13349 | 7d4441c8c46a |
parent 13346 | 6918b6d5192b |
child 13550 | 5a176b8dda84 |
permissions | -rw-r--r-- |
1476 | 1 |
(* Title: HOL/Lambda/Commutation.thy |
1278 | 2 |
ID: $Id$ |
1476 | 3 |
Author: Tobias Nipkow |
1278 | 4 |
Copyright 1995 TU Muenchen |
5 |
*) |
|
6 |
||
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
7 |
header {* Abstract commutation and confluence notions *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
8 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
9 |
theory Commutation = Main: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
10 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
11 |
subsection {* Basic definitions *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
12 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
13 |
constdefs |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
14 |
square :: "[('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set] => bool" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
15 |
"square R S T U == |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
16 |
\<forall>x y. (x, y) \<in> R --> (\<forall>z. (x, z) \<in> S --> (\<exists>u. (y, u) \<in> T \<and> (z, u) \<in> U))" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
17 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
18 |
commute :: "[('a \<times> 'a) set, ('a \<times> 'a) set] => bool" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
19 |
"commute R S == square R S S R" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
20 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
21 |
diamond :: "('a \<times> 'a) set => bool" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
22 |
"diamond R == commute R R" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
23 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
24 |
Church_Rosser :: "('a \<times> 'a) set => bool" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
25 |
"Church_Rosser R == |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
26 |
\<forall>x y. (x, y) \<in> (R \<union> R^-1)^* --> (\<exists>z. (x, z) \<in> R^* \<and> (y, z) \<in> R^*)" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
27 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
28 |
syntax |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
29 |
confluent :: "('a \<times> 'a) set => bool" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
30 |
translations |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
31 |
"confluent R" == "diamond (R^*)" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
32 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
33 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
34 |
subsection {* Basic lemmas *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
35 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
36 |
subsubsection {* square *} |
1278 | 37 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
38 |
lemma square_sym: "square R S T U ==> square S R U T" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
39 |
apply (unfold square_def) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
40 |
apply blast |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
41 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
42 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
43 |
lemma square_subset: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
44 |
"[| square R S T U; T \<subseteq> T' |] ==> square R S T' U" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
45 |
apply (unfold square_def) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
46 |
apply blast |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
47 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
48 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
49 |
lemma square_reflcl: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
50 |
"[| square R S T (R^=); S \<subseteq> T |] ==> square (R^=) S T (R^=)" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
51 |
apply (unfold square_def) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
52 |
apply blast |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
53 |
done |
1278 | 54 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
55 |
lemma square_rtrancl: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
56 |
"square R S S T ==> square (R^*) S S (T^*)" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
57 |
apply (unfold square_def) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
58 |
apply (intro strip) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
59 |
apply (erule rtrancl_induct) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
60 |
apply blast |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
61 |
apply (blast intro: rtrancl_into_rtrancl) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
62 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
63 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
64 |
lemma square_rtrancl_reflcl_commute: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
65 |
"square R S (S^*) (R^=) ==> commute (R^*) (S^*)" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
66 |
apply (unfold commute_def) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
67 |
apply (fastsimp dest: square_reflcl square_sym [THEN square_rtrancl] |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
68 |
elim: r_into_rtrancl) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
69 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
70 |
|
1278 | 71 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
72 |
subsubsection {* commute *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
73 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
74 |
lemma commute_sym: "commute R S ==> commute S R" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
75 |
apply (unfold commute_def) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
76 |
apply (blast intro: square_sym) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
77 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
78 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
79 |
lemma commute_rtrancl: "commute R S ==> commute (R^*) (S^*)" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
80 |
apply (unfold commute_def) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
81 |
apply (blast intro: square_rtrancl square_sym) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
82 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
83 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
84 |
lemma commute_Un: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
85 |
"[| commute R T; commute S T |] ==> commute (R \<union> S) T" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
86 |
apply (unfold commute_def square_def) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
87 |
apply blast |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
88 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
89 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
90 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
91 |
subsubsection {* diamond, confluence, and union *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
92 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
93 |
lemma diamond_Un: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
94 |
"[| diamond R; diamond S; commute R S |] ==> diamond (R \<union> S)" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
95 |
apply (unfold diamond_def) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
96 |
apply (assumption | rule commute_Un commute_sym)+ |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
97 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
98 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
99 |
lemma diamond_confluent: "diamond R ==> confluent R" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
100 |
apply (unfold diamond_def) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
101 |
apply (erule commute_rtrancl) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
102 |
done |
1278 | 103 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
104 |
lemma square_reflcl_confluent: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
105 |
"square R R (R^=) (R^=) ==> confluent R" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
106 |
apply (unfold diamond_def) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
107 |
apply (fast intro: square_rtrancl_reflcl_commute r_into_rtrancl |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
108 |
elim: square_subset) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
109 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
110 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
111 |
lemma confluent_Un: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
112 |
"[| confluent R; confluent S; commute (R^*) (S^*) |] ==> confluent (R \<union> S)" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
113 |
apply (rule rtrancl_Un_rtrancl [THEN subst]) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
114 |
apply (blast dest: diamond_Un intro: diamond_confluent) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
115 |
done |
1278 | 116 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
117 |
lemma diamond_to_confluence: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
118 |
"[| diamond R; T \<subseteq> R; R \<subseteq> T^* |] ==> confluent T" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
119 |
apply (force intro: diamond_confluent |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
120 |
dest: rtrancl_subset [symmetric]) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
121 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
122 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
123 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
124 |
subsection {* Church-Rosser *} |
1278 | 125 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
126 |
lemma Church_Rosser_confluent: "Church_Rosser R = confluent R" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
127 |
apply (unfold square_def commute_def diamond_def Church_Rosser_def) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
128 |
apply (tactic {* safe_tac HOL_cs *}) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
129 |
apply (tactic {* |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
130 |
blast_tac (HOL_cs addIs |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
131 |
[Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans, |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
132 |
rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD]) 1 *}) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
133 |
apply (erule rtrancl_induct) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
134 |
apply blast |
10212 | 135 |
apply (blast del: rtrancl_refl intro: rtrancl_trans) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
136 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
137 |
|
13089 | 138 |
|
139 |
subsection {* Newman's lemma *} |
|
140 |
||
13349
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
141 |
text {* Proof by Stefan Berghofer *} |
13346 | 142 |
|
13343 | 143 |
theorem newman: |
13089 | 144 |
assumes wf: "wf (R\<inverse>)" |
145 |
and lc: "\<And>a b c. (a, b) \<in> R \<Longrightarrow> (a, c) \<in> R \<Longrightarrow> |
|
146 |
\<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" |
|
13349
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
147 |
shows "\<And>b c. (a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow> |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
148 |
\<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
149 |
using wf |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
150 |
proof induct |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
151 |
case (less x b c) |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
152 |
have xc: "(x, c) \<in> R\<^sup>*" . |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
153 |
have xb: "(x, b) \<in> R\<^sup>*" . thus ?case |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
154 |
proof (rule converse_rtranclE) |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
155 |
assume "x = b" |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
156 |
with xc have "(b, c) \<in> R\<^sup>*" by simp |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
157 |
thus ?thesis by rules |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
158 |
next |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
159 |
fix y |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
160 |
assume xy: "(x, y) \<in> R" |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
161 |
assume yb: "(y, b) \<in> R\<^sup>*" |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
162 |
from xc show ?thesis |
13089 | 163 |
proof (rule converse_rtranclE) |
13349
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
164 |
assume "x = c" |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
165 |
with xb have "(c, b) \<in> R\<^sup>*" by simp |
13089 | 166 |
thus ?thesis by rules |
167 |
next |
|
13349
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
168 |
fix y' |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
169 |
assume y'c: "(y', c) \<in> R\<^sup>*" |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
170 |
assume xy': "(x, y') \<in> R" |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
171 |
with xy have "\<exists>u. (y, u) \<in> R\<^sup>* \<and> (y', u) \<in> R\<^sup>*" by (rule lc) |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
172 |
then obtain u where yu: "(y, u) \<in> R\<^sup>*" and y'u: "(y', u) \<in> R\<^sup>*" by rules |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
173 |
from xy have "(y, x) \<in> R\<inverse>" .. |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
174 |
from this and yb yu have "\<exists>d. (b, d) \<in> R\<^sup>* \<and> (u, d) \<in> R\<^sup>*" by (rule less) |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
175 |
then obtain v where bv: "(b, v) \<in> R\<^sup>*" and uv: "(u, v) \<in> R\<^sup>*" by rules |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
176 |
from xy' have "(y', x) \<in> R\<inverse>" .. |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
177 |
moreover from y'u and uv have "(y', v) \<in> R\<^sup>*" by (rule rtrancl_trans) |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
178 |
moreover note y'c |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
179 |
ultimately have "\<exists>d. (v, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" by (rule less) |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
180 |
then obtain w where vw: "(v, w) \<in> R\<^sup>*" and cw: "(c, w) \<in> R\<^sup>*" by rules |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
181 |
from bv vw have "(b, w) \<in> R\<^sup>*" by (rule rtrancl_trans) |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
182 |
with cw show ?thesis by rules |
13089 | 183 |
qed |
184 |
qed |
|
185 |
qed |
|
186 |
||
13349
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
187 |
text {* |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
188 |
\medskip Alternative version. Partly automated by Tobias |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
189 |
Nipkow. Takes 2 minutes (2002). |
13346 | 190 |
|
13349
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
191 |
This is the maximal amount of automation possible at the moment. |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
192 |
*} |
13346 | 193 |
|
13349
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
194 |
theorem newman': |
13346 | 195 |
assumes wf: "wf (R\<inverse>)" |
196 |
and lc: "\<And>a b c. (a, b) \<in> R \<Longrightarrow> (a, c) \<in> R \<Longrightarrow> |
|
197 |
\<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" |
|
198 |
shows "\<And>b c. (a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow> |
|
199 |
\<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" |
|
200 |
using wf |
|
201 |
proof induct |
|
202 |
case (less x b c) |
|
203 |
have IH: "\<And>y b c. \<lbrakk>(y,x) \<in> R\<inverse>; (y,b) \<in> R\<^sup>*; (y,c) \<in> R\<^sup>*\<rbrakk> |
|
204 |
\<Longrightarrow> \<exists>d. (b,d) \<in> R\<^sup>* \<and> (c,d) \<in> R\<^sup>*" by(rule less) |
|
205 |
have xc: "(x, c) \<in> R\<^sup>*" . |
|
206 |
have xb: "(x, b) \<in> R\<^sup>*" . |
|
207 |
thus ?case |
|
208 |
proof (rule converse_rtranclE) |
|
209 |
assume "x = b" |
|
210 |
with xc have "(b, c) \<in> R\<^sup>*" by simp |
|
211 |
thus ?thesis by rules |
|
212 |
next |
|
213 |
fix y |
|
214 |
assume xy: "(x, y) \<in> R" |
|
215 |
assume yb: "(y, b) \<in> R\<^sup>*" |
|
216 |
from xc show ?thesis |
|
217 |
proof (rule converse_rtranclE) |
|
218 |
assume "x = c" |
|
219 |
with xb have "(c, b) \<in> R\<^sup>*" by simp |
|
220 |
thus ?thesis by rules |
|
221 |
next |
|
222 |
fix y' |
|
223 |
assume y'c: "(y', c) \<in> R\<^sup>*" |
|
224 |
assume xy': "(x, y') \<in> R" |
|
225 |
with xy obtain u where u: "(y, u) \<in> R\<^sup>*" "(y', u) \<in> R\<^sup>*" |
|
226 |
by (blast dest:lc) |
|
227 |
from yb u y'c show ?thesis |
|
228 |
by(blast intro:rtrancl_trans |
|
229 |
dest:IH[OF xy[symmetric]] IH[OF xy'[symmetric]]) |
|
230 |
qed |
|
231 |
qed |
|
232 |
qed |
|
233 |
||
10179 | 234 |
end |