author | wenzelm |
Sun, 28 Nov 2010 14:01:20 +0100 | |
changeset 40781 | ba5be5c3d477 |
parent 39159 | 0dec18004e75 |
child 42793 | 88bee9f6eec7 |
permissions | -rw-r--r-- |
39157
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39126
diff
changeset
|
1 |
(* Title: HOL/Proofs/Lambda/Commutation.thy |
1476 | 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 |
|
39126
ee117c5b3b75
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents:
36862
diff
changeset
|
10 |
declare [[syntax_ambiguity_level = 100]] |
ee117c5b3b75
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents:
36862
diff
changeset
|
11 |
|
ee117c5b3b75
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents:
36862
diff
changeset
|
12 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
13 |
subsection {* Basic definitions *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
14 |
|
19086 | 15 |
definition |
22270 | 16 |
square :: "['a => 'a => bool, 'a => 'a => bool, 'a => 'a => bool, 'a => 'a => bool] => bool" where |
19086 | 17 |
"square R S T U = |
22270 | 18 |
(\<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
|
19 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19363
diff
changeset
|
20 |
definition |
22270 | 21 |
commute :: "['a => 'a => bool, 'a => 'a => bool] => bool" where |
19086 | 22 |
"commute R S = square R S S R" |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
23 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19363
diff
changeset
|
24 |
definition |
22270 | 25 |
diamond :: "('a => 'a => bool) => bool" where |
19086 | 26 |
"diamond R = commute R R" |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
27 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19363
diff
changeset
|
28 |
definition |
22270 | 29 |
Church_Rosser :: "('a => 'a => bool) => bool" where |
19086 | 30 |
"Church_Rosser R = |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22270
diff
changeset
|
31 |
(\<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
|
32 |
|
19363 | 33 |
abbreviation |
22270 | 34 |
confluent :: "('a => 'a => bool) => bool" where |
35 |
"confluent R == diamond (R^**)" |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
36 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
37 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
38 |
subsection {* Basic lemmas *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
39 |
|
25972 | 40 |
subsubsection {* @{text "square"} *} |
1278 | 41 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
42 |
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
|
43 |
apply (unfold square_def) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
44 |
apply blast |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
45 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
46 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
47 |
lemma square_subset: |
22270 | 48 |
"[| 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
|
49 |
apply (unfold square_def) |
22270 | 50 |
apply (blast dest: predicate2D) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
51 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
52 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
53 |
lemma square_reflcl: |
22270 | 54 |
"[| 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
|
55 |
apply (unfold square_def) |
22270 | 56 |
apply (blast dest: predicate2D) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
57 |
done |
1278 | 58 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
59 |
lemma square_rtrancl: |
22270 | 60 |
"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
|
61 |
apply (unfold square_def) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
62 |
apply (intro strip) |
23750 | 63 |
apply (erule rtranclp_induct) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
64 |
apply blast |
23750 | 65 |
apply (blast intro: rtranclp.rtrancl_into_rtrancl) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
66 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
67 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
68 |
lemma square_rtrancl_reflcl_commute: |
22270 | 69 |
"square R S (S^**) (R^==) ==> commute (R^**) (S^**)" |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
70 |
apply (unfold commute_def) |
22270 | 71 |
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
|
72 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
73 |
|
1278 | 74 |
|
25972 | 75 |
subsubsection {* @{text "commute"} *} |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
76 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
77 |
lemma commute_sym: "commute R S ==> commute S R" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
78 |
apply (unfold commute_def) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
79 |
apply (blast intro: square_sym) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
80 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
81 |
|
22270 | 82 |
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
|
83 |
apply (unfold commute_def) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
84 |
apply (blast intro: square_rtrancl square_sym) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
85 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
86 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
87 |
lemma commute_Un: |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22270
diff
changeset
|
88 |
"[| 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
|
89 |
apply (unfold commute_def square_def) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
90 |
apply blast |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
91 |
done |
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 |
|
25972 | 94 |
subsubsection {* @{text "diamond"}, @{text "confluence"}, and @{text "union"} *} |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
95 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
96 |
lemma diamond_Un: |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22270
diff
changeset
|
97 |
"[| 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
|
98 |
apply (unfold diamond_def) |
23815 | 99 |
apply (blast intro: commute_Un commute_sym) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
100 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
101 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
102 |
lemma diamond_confluent: "diamond R ==> confluent R" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
103 |
apply (unfold diamond_def) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
104 |
apply (erule commute_rtrancl) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
105 |
done |
1278 | 106 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
107 |
lemma square_reflcl_confluent: |
22270 | 108 |
"square R R (R^==) (R^==) ==> confluent R" |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
109 |
apply (unfold diamond_def) |
22270 | 110 |
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
|
111 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
112 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
113 |
lemma confluent_Un: |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22270
diff
changeset
|
114 |
"[| confluent R; confluent S; commute (R^**) (S^**) |] ==> confluent (sup R S)" |
23750 | 115 |
apply (rule rtranclp_sup_rtranclp [THEN subst]) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
116 |
apply (blast dest: diamond_Un intro: diamond_confluent) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
117 |
done |
1278 | 118 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
119 |
lemma diamond_to_confluence: |
22270 | 120 |
"[| 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
|
121 |
apply (force intro: diamond_confluent |
23750 | 122 |
dest: rtranclp_subset [symmetric]) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
123 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
124 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
125 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
126 |
subsection {* Church-Rosser *} |
1278 | 127 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
128 |
lemma Church_Rosser_confluent: "Church_Rosser R = confluent R" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
129 |
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
|
130 |
apply (tactic {* safe_tac HOL_cs *}) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
131 |
apply (tactic {* |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
132 |
blast_tac (HOL_cs addIs |
39159 | 133 |
[@{thm sup_ge2} RS @{thm rtranclp_mono} RS @{thm predicate2D} RS @{thm rtranclp_trans}, |
134 |
@{thm rtranclp_converseI}, @{thm conversepI}, |
|
135 |
@{thm sup_ge1} RS @{thm rtranclp_mono} RS @{thm predicate2D}]) 1 *}) |
|
23750 | 136 |
apply (erule rtranclp_induct) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
137 |
apply blast |
23750 | 138 |
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
|
139 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
8624
diff
changeset
|
140 |
|
13089 | 141 |
|
142 |
subsection {* Newman's lemma *} |
|
143 |
||
13349
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
144 |
text {* Proof by Stefan Berghofer *} |
13346 | 145 |
|
13343 | 146 |
theorem newman: |
22270 | 147 |
assumes wf: "wfP (R\<inverse>\<inverse>)" |
148 |
and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow> |
|
149 |
\<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d" |
|
150 |
shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow> |
|
151 |
\<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
|
152 |
using wf |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
153 |
proof induct |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
154 |
case (less x b c) |
23464 | 155 |
have xc: "R\<^sup>*\<^sup>* x c" by fact |
156 |
have xb: "R\<^sup>*\<^sup>* x b" by fact thus ?case |
|
23750 | 157 |
proof (rule converse_rtranclpE) |
13349
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
158 |
assume "x = b" |
22270 | 159 |
with xc have "R\<^sup>*\<^sup>* b c" by simp |
17589 | 160 |
thus ?thesis by iprover |
13349
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
161 |
next |
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
162 |
fix y |
22270 | 163 |
assume xy: "R x y" |
164 |
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
|
165 |
from xc show ?thesis |
23750 | 166 |
proof (rule converse_rtranclpE) |
13349
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
167 |
assume "x = c" |
22270 | 168 |
with xb have "R\<^sup>*\<^sup>* c b" by simp |
17589 | 169 |
thus ?thesis by iprover |
13089 | 170 |
next |
13349
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
171 |
fix y' |
22270 | 172 |
assume y'c: "R\<^sup>*\<^sup>* y' c" |
173 |
assume xy': "R x y'" |
|
174 |
with xy have "\<exists>u. R\<^sup>*\<^sup>* y u \<and> R\<^sup>*\<^sup>* y' u" by (rule lc) |
|
175 |
then obtain u where yu: "R\<^sup>*\<^sup>* y u" and y'u: "R\<^sup>*\<^sup>* y' u" by iprover |
|
176 |
from xy have "R\<inverse>\<inverse> y x" .. |
|
177 |
from this and yb yu have "\<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* u d" by (rule less) |
|
178 |
then obtain v where bv: "R\<^sup>*\<^sup>* b v" and uv: "R\<^sup>*\<^sup>* u v" by iprover |
|
179 |
from xy' have "R\<inverse>\<inverse> y' x" .. |
|
23750 | 180 |
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
|
181 |
moreover note y'c |
22270 | 182 |
ultimately have "\<exists>d. R\<^sup>*\<^sup>* v d \<and> R\<^sup>*\<^sup>* c d" by (rule less) |
183 |
then obtain w where vw: "R\<^sup>*\<^sup>* v w" and cw: "R\<^sup>*\<^sup>* c w" by iprover |
|
23750 | 184 |
from bv vw have "R\<^sup>*\<^sup>* b w" by (rule rtranclp_trans) |
17589 | 185 |
with cw show ?thesis by iprover |
13089 | 186 |
qed |
187 |
qed |
|
188 |
qed |
|
189 |
||
13349
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
190 |
text {* |
28455
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
191 |
Alternative version. Partly automated by Tobias |
13349
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
192 |
Nipkow. Takes 2 minutes (2002). |
13346 | 193 |
|
28455
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
194 |
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
|
195 |
*} |
13346 | 196 |
|
13349
7d4441c8c46a
Added "using" to the beginning of original newman proof again, because
berghofe
parents:
13346
diff
changeset
|
197 |
theorem newman': |
22270 | 198 |
assumes wf: "wfP (R\<inverse>\<inverse>)" |
199 |
and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow> |
|
200 |
\<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d" |
|
201 |
shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow> |
|
202 |
\<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d" |
|
18241 | 203 |
using wf |
13346 | 204 |
proof induct |
205 |
case (less x b c) |
|
22270 | 206 |
note IH = `\<And>y b c. \<lbrakk>R\<inverse>\<inverse> y x; R\<^sup>*\<^sup>* y b; R\<^sup>*\<^sup>* y c\<rbrakk> |
207 |
\<Longrightarrow> \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d` |
|
23464 | 208 |
have xc: "R\<^sup>*\<^sup>* x c" by fact |
209 |
have xb: "R\<^sup>*\<^sup>* x b" by fact |
|
13346 | 210 |
thus ?case |
23750 | 211 |
proof (rule converse_rtranclpE) |
13346 | 212 |
assume "x = b" |
22270 | 213 |
with xc have "R\<^sup>*\<^sup>* b c" by simp |
17589 | 214 |
thus ?thesis by iprover |
13346 | 215 |
next |
216 |
fix y |
|
22270 | 217 |
assume xy: "R x y" |
218 |
assume yb: "R\<^sup>*\<^sup>* y b" |
|
13346 | 219 |
from xc show ?thesis |
23750 | 220 |
proof (rule converse_rtranclpE) |
13346 | 221 |
assume "x = c" |
22270 | 222 |
with xb have "R\<^sup>*\<^sup>* c b" by simp |
17589 | 223 |
thus ?thesis by iprover |
13346 | 224 |
next |
225 |
fix y' |
|
22270 | 226 |
assume y'c: "R\<^sup>*\<^sup>* y' c" |
227 |
assume xy': "R x y'" |
|
228 |
with xy obtain u where u: "R\<^sup>*\<^sup>* y u" "R\<^sup>*\<^sup>* y' u" |
|
18241 | 229 |
by (blast dest: lc) |
13346 | 230 |
from yb u y'c show ?thesis |
23750 | 231 |
by (blast del: rtranclp.rtrancl_refl |
232 |
intro: rtranclp_trans |
|
22270 | 233 |
dest: IH [OF conversepI, OF xy] IH [OF conversepI, OF xy']) |
13346 | 234 |
qed |
235 |
qed |
|
236 |
qed |
|
237 |
||
28455
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
238 |
text {* |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
239 |
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
|
240 |
is completely automatic. |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
241 |
*} |
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 |
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
|
244 |
by simp |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
245 |
|
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
246 |
theorem newman'': |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
247 |
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
|
248 |
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
|
249 |
\<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
|
250 |
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
|
251 |
\<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
|
252 |
using wf |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
253 |
proof induct |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
254 |
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
|
255 |
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
|
256 |
\<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
|
257 |
show ?case |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
258 |
by (coherent |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
259 |
`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
|
260 |
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
|
261 |
eq_imp_rtranclp |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
262 |
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
|
263 |
rtranclp_trans |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
264 |
lc IH [OF conversepI] |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
265 |
converse_rtranclpE) |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
266 |
qed |
a79701b14a30
Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents:
25972
diff
changeset
|
267 |
|
10179 | 268 |
end |