author | haftmann |
Thu, 08 Jul 2010 16:19:24 +0200 | |
changeset 37744 | 3daaf23b9ab4 |
parent 36862 | 952b2b102a0a |
child 39126 | ee117c5b3b75 |
permissions | -rw-r--r-- |
1476 | 1 |
(* Title: HOL/Lambda/Commutation.thy |
2 |
Author: Tobias Nipkow |
|
1278 | 3 |
Copyright 1995 TU Muenchen |
4 |
*) |
|
5 |
||
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
6 |
header {* Abstract commutation and confluence notions *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
7 |
|
16417 | 8 |
theory Commutation imports Main begin |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
9 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
10 |
subsection {* Basic definitions *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
11 |
|
19086 | 12 |
definition |
22270 | 13 |
square :: "['a => 'a => bool, 'a => 'a => bool, 'a => 'a => bool, 'a => 'a => bool] => bool" where |
19086 | 14 |
"square R S T U = |
22270 | 15 |
(\<forall>x y. R x y --> (\<forall>z. S x z --> (\<exists>u. T y u \<and> U z u)))" |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
16 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19363
diff
changeset
|
17 |
definition |
22270 | 18 |
commute :: "['a => 'a => bool, 'a => 'a => bool] => bool" where |
19086 | 19 |
"commute R S = square R S S R" |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
20 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19363
diff
changeset
|
21 |
definition |
22270 | 22 |
diamond :: "('a => 'a => bool) => bool" where |
19086 | 23 |
"diamond R = commute R R" |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
24 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19363
diff
changeset
|
25 |
definition |
22270 | 26 |
Church_Rosser :: "('a => 'a => bool) => bool" where |
19086 | 27 |
"Church_Rosser R = |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22270
diff
changeset
|
28 |
(\<forall>x y. (sup R (R^--1))^** x y --> (\<exists>z. R^** x z \<and> R^** y z))" |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
29 |
|
19363 | 30 |
abbreviation |
22270 | 31 |
confluent :: "('a => 'a => bool) => bool" where |
32 |
"confluent R == diamond (R^**)" |
|
9811
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 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
35 |
subsection {* Basic lemmas *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
36 |
|
25972 | 37 |
subsubsection {* @{text "square"} *} |
1278 | 38 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
39 |
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
|
40 |
apply (unfold square_def) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
41 |
apply blast |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
42 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
43 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
44 |
lemma square_subset: |
22270 | 45 |
"[| square R S T U; T \<le> T' |] ==> square R S T' U" |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
46 |
apply (unfold square_def) |
22270 | 47 |
apply (blast dest: predicate2D) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
48 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
49 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
50 |
lemma square_reflcl: |
22270 | 51 |
"[| square R S T (R^==); S \<le> T |] ==> square (R^==) S T (R^==)" |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
52 |
apply (unfold square_def) |
22270 | 53 |
apply (blast dest: predicate2D) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
54 |
done |
1278 | 55 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
56 |
lemma square_rtrancl: |
22270 | 57 |
"square R S S T ==> square (R^**) S S (T^**)" |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
58 |
apply (unfold square_def) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
59 |
apply (intro strip) |
23750 | 60 |
apply (erule rtranclp_induct) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
61 |
apply blast |
23750 | 62 |
apply (blast intro: rtranclp.rtrancl_into_rtrancl) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
63 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
64 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
65 |
lemma square_rtrancl_reflcl_commute: |
22270 | 66 |
"square R S (S^**) (R^==) ==> commute (R^**) (S^**)" |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
67 |
apply (unfold commute_def) |
22270 | 68 |
apply (fastsimp dest: square_reflcl square_sym [THEN square_rtrancl]) |
9811
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 |
|
25972 | 72 |
subsubsection {* @{text "commute"} *} |
9811
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 |
|
22270 | 79 |
lemma commute_rtrancl: "commute R S ==> commute (R^**) (S^**)" |
9811
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: |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22270
diff
changeset
|
85 |
"[| commute R T; commute S T |] ==> commute (sup R S) T" |
9811
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 |
|
25972 | 91 |
subsubsection {* @{text "diamond"}, @{text "confluence"}, and @{text "union"} *} |
9811
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: |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22270
diff
changeset
|
94 |
"[| diamond R; diamond S; commute R S |] ==> diamond (sup R S)" |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
95 |
apply (unfold diamond_def) |
23815 | 96 |
apply (blast intro: commute_Un commute_sym) |
9811
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: |
22270 | 105 |
"square R R (R^==) (R^==) ==> confluent R" |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
106 |
apply (unfold diamond_def) |
22270 | 107 |
apply (fast intro: square_rtrancl_reflcl_commute elim: square_subset) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
108 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
109 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
110 |
lemma confluent_Un: |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22270
diff
changeset
|
111 |
"[| confluent R; confluent S; commute (R^**) (S^**) |] ==> confluent (sup R S)" |
23750 | 112 |
apply (rule rtranclp_sup_rtranclp [THEN subst]) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
113 |
apply (blast dest: diamond_Un intro: diamond_confluent) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
114 |
done |
1278 | 115 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
116 |
lemma diamond_to_confluence: |
22270 | 117 |
"[| diamond R; T \<le> R; R \<le> T^** |] ==> confluent T" |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
118 |
apply (force intro: diamond_confluent |
23750 | 119 |
dest: rtranclp_subset [symmetric]) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
120 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
121 |
|
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 |
subsection {* Church-Rosser *} |
1278 | 124 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
125 |
lemma Church_Rosser_confluent: "Church_Rosser R = confluent R" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
126 |
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
|
127 |
apply (tactic {* safe_tac HOL_cs *}) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
128 |
apply (tactic {* |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
129 |
blast_tac (HOL_cs addIs |
23750 | 130 |
[thm "sup_ge2" RS thm "rtranclp_mono" RS thm "predicate2D" RS thm "rtranclp_trans", |
131 |
thm "rtranclp_converseI", thm "conversepI", |
|
132 |
thm "sup_ge1" RS thm "rtranclp_mono" RS thm "predicate2D"]) 1 *}) |
|
133 |
apply (erule rtranclp_induct) |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
134 |
apply blast |
23750 | 135 |
apply (blast del: rtranclp.rtrancl_refl intro: rtranclp_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: |
22270 | 144 |
assumes wf: "wfP (R\<inverse>\<inverse>)" |
145 |
and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow> |
|
146 |
\<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d" |
|
147 |
shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow> |
|
148 |
\<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d" |
|
13349
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) |
23464 | 152 |
have xc: "R\<^sup>*\<^sup>* x c" by fact |
153 |
have xb: "R\<^sup>*\<^sup>* x b" by fact thus ?case |
|
23750 | 154 |
proof (rule converse_rtranclpE) |
13349
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
155 |
assume "x = b" |
22270 | 156 |
with xc have "R\<^sup>*\<^sup>* b c" by simp |
17589 | 157 |
thus ?thesis by iprover |
13349
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 |
22270 | 160 |
assume xy: "R x y" |
161 |
assume yb: "R\<^sup>*\<^sup>* y b" |
|
13349
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
162 |
from xc show ?thesis |
23750 | 163 |
proof (rule converse_rtranclpE) |
13349
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
164 |
assume "x = c" |
22270 | 165 |
with xb have "R\<^sup>*\<^sup>* c b" by simp |
17589 | 166 |
thus ?thesis by iprover |
13089 | 167 |
next |
13349
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
168 |
fix y' |
22270 | 169 |
assume y'c: "R\<^sup>*\<^sup>* y' c" |
170 |
assume xy': "R x y'" |
|
171 |
with xy have "\<exists>u. R\<^sup>*\<^sup>* y u \<and> R\<^sup>*\<^sup>* y' u" by (rule lc) |
|
172 |
then obtain u where yu: "R\<^sup>*\<^sup>* y u" and y'u: "R\<^sup>*\<^sup>* y' u" by iprover |
|
173 |
from xy have "R\<inverse>\<inverse> y x" .. |
|
174 |
from this and yb yu have "\<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* u d" by (rule less) |
|
175 |
then obtain v where bv: "R\<^sup>*\<^sup>* b v" and uv: "R\<^sup>*\<^sup>* u v" by iprover |
|
176 |
from xy' have "R\<inverse>\<inverse> y' x" .. |
|
23750 | 177 |
moreover from y'u and uv have "R\<^sup>*\<^sup>* y' v" by (rule rtranclp_trans) |
13349
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
178 |
moreover note y'c |
22270 | 179 |
ultimately have "\<exists>d. R\<^sup>*\<^sup>* v d \<and> R\<^sup>*\<^sup>* c d" by (rule less) |
180 |
then obtain w where vw: "R\<^sup>*\<^sup>* v w" and cw: "R\<^sup>*\<^sup>* c w" by iprover |
|
23750 | 181 |
from bv vw have "R\<^sup>*\<^sup>* b w" by (rule rtranclp_trans) |
17589 | 182 |
with cw show ?thesis by iprover |
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 {* |
28455
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
188 |
Alternative version. Partly automated by Tobias |
13349
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 |
|
28455
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
191 |
This is the maximal amount of automation possible using @{text blast}. |
13349
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': |
22270 | 195 |
assumes wf: "wfP (R\<inverse>\<inverse>)" |
196 |
and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow> |
|
197 |
\<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d" |
|
198 |
shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow> |
|
199 |
\<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d" |
|
18241 | 200 |
using wf |
13346 | 201 |
proof induct |
202 |
case (less x b c) |
|
22270 | 203 |
note IH = `\<And>y b c. \<lbrakk>R\<inverse>\<inverse> y x; R\<^sup>*\<^sup>* y b; R\<^sup>*\<^sup>* y c\<rbrakk> |
204 |
\<Longrightarrow> \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d` |
|
23464 | 205 |
have xc: "R\<^sup>*\<^sup>* x c" by fact |
206 |
have xb: "R\<^sup>*\<^sup>* x b" by fact |
|
13346 | 207 |
thus ?case |
23750 | 208 |
proof (rule converse_rtranclpE) |
13346 | 209 |
assume "x = b" |
22270 | 210 |
with xc have "R\<^sup>*\<^sup>* b c" by simp |
17589 | 211 |
thus ?thesis by iprover |
13346 | 212 |
next |
213 |
fix y |
|
22270 | 214 |
assume xy: "R x y" |
215 |
assume yb: "R\<^sup>*\<^sup>* y b" |
|
13346 | 216 |
from xc show ?thesis |
23750 | 217 |
proof (rule converse_rtranclpE) |
13346 | 218 |
assume "x = c" |
22270 | 219 |
with xb have "R\<^sup>*\<^sup>* c b" by simp |
17589 | 220 |
thus ?thesis by iprover |
13346 | 221 |
next |
222 |
fix y' |
|
22270 | 223 |
assume y'c: "R\<^sup>*\<^sup>* y' c" |
224 |
assume xy': "R x y'" |
|
225 |
with xy obtain u where u: "R\<^sup>*\<^sup>* y u" "R\<^sup>*\<^sup>* y' u" |
|
18241 | 226 |
by (blast dest: lc) |
13346 | 227 |
from yb u y'c show ?thesis |
23750 | 228 |
by (blast del: rtranclp.rtrancl_refl |
229 |
intro: rtranclp_trans |
|
22270 | 230 |
dest: IH [OF conversepI, OF xy] IH [OF conversepI, OF xy']) |
13346 | 231 |
qed |
232 |
qed |
|
233 |
qed |
|
234 |
||
28455
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
235 |
text {* |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
236 |
Using the coherent logic prover, the proof of the induction step |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
237 |
is completely automatic. |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
238 |
*} |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
239 |
|
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
240 |
lemma eq_imp_rtranclp: "x = y \<Longrightarrow> r\<^sup>*\<^sup>* x y" |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
241 |
by simp |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
242 |
|
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
243 |
theorem newman'': |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
244 |
assumes wf: "wfP (R\<inverse>\<inverse>)" |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
245 |
and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow> |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
246 |
\<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d" |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
247 |
shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow> |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
248 |
\<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d" |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
249 |
using wf |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
250 |
proof induct |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
251 |
case (less x b c) |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
252 |
note IH = `\<And>y b c. \<lbrakk>R\<inverse>\<inverse> y x; R\<^sup>*\<^sup>* y b; R\<^sup>*\<^sup>* y c\<rbrakk> |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
253 |
\<Longrightarrow> \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d` |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
254 |
show ?case |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
255 |
by (coherent |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
256 |
`R\<^sup>*\<^sup>* x c` `R\<^sup>*\<^sup>* x b` |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
257 |
refl [where 'a='a] sym |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
258 |
eq_imp_rtranclp |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
259 |
r_into_rtranclp [of R] |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
260 |
rtranclp_trans |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
261 |
lc IH [OF conversepI] |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
262 |
converse_rtranclpE) |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
263 |
qed |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
264 |
|
10179 | 265 |
end |