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