author  haftmann 
Sat, 05 Jul 2014 11:01:53 +0200  
changeset 57514  bdc2c6b40bf2 
parent 46512  4f9f61f9b535 
child 58372  bfd497f2f4c2 
permissions  rwrr 
39157
b98909faaea8
more explicit HOLProofs 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 newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

6 
header {* Abstract commutation and confluence notions *} 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

7 

16417  8 
theory Commutation imports Main begin 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

9 

46512
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset

10 
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

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 newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

13 
subsection {* Basic definitions *} 
39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle 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 newstyle 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 newstyle 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 newstyle 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 newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

36 

39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

37 

39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

38 
subsection {* Basic lemmas *} 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

39 

25972  40 
subsubsection {* @{text "square"} *} 
1278  41 

9811
39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

43 
apply (unfold square_def) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

44 
apply blast 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

45 
done 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

46 

39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle 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 newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

51 
done 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

52 

39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle 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 newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

57 
done 
1278  58 

9811
39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

61 
apply (unfold square_def) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

62 
apply (intro strip) 
23750  63 
apply (erule rtranclp_induct) 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

66 
done 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

67 

39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

70 
apply (unfold commute_def) 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
42793
diff
changeset

71 
apply (fastforce dest: square_reflcl square_sym [THEN square_rtrancl]) 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

72 
done 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

73 

1278  74 

25972  75 
subsubsection {* @{text "commute"} *} 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

76 

39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

77 
lemma commute_sym: "commute R S ==> commute S R" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

78 
apply (unfold commute_def) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

79 
apply (blast intro: square_sym) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

80 
done 
39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

83 
apply (unfold commute_def) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

84 
apply (blast intro: square_rtrancl square_sym) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

85 
done 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

86 

39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

89 
apply (unfold commute_def square_def) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

90 
apply blast 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

91 
done 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

92 

39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

95 

39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle 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 newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

100 
done 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

101 

39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

102 
lemma diamond_confluent: "diamond R ==> confluent R" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

103 
apply (unfold diamond_def) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

104 
apply (erule commute_rtrancl) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

105 
done 
1278  106 

9811
39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle 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 newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

111 
done 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

112 

39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

116 
apply (blast dest: diamond_Un intro: diamond_confluent) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

117 
done 
1278  118 

9811
39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle 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 newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

123 
done 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

124 

39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

125 

39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

126 
subsection {* ChurchRosser *} 
1278  127 

9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

128 
lemma Church_Rosser_confluent: "Church_Rosser R = confluent R" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

129 
apply (unfold square_def commute_def diamond_def Church_Rosser_def) 
42793  130 
apply (tactic {* safe_tac (put_claset HOL_cs @{context}) *}) 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

131 
apply (tactic {* 
42793  132 
blast_tac (put_claset HOL_cs @{context} 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 newstyle 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 newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

139 
done 
39ffdb8cab03
HOL/Lambda: converted into newstyle 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 