author | wenzelm |
Wed, 06 Jul 2016 20:19:51 +0200 | |
changeset 63404 | a95e7432d86c |
parent 62957 | a9c40cf517d1 |
child 63612 | 7195acc2fe93 |
permissions | -rw-r--r-- |
10213 | 1 |
(* Title: HOL/Transitive_Closure.thy |
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 |
Copyright 1992 University of Cambridge |
|
4 |
*) |
|
5 |
||
60758 | 6 |
section \<open>Reflexive and Transitive closure of a relation\<close> |
12691 | 7 |
|
15131 | 8 |
theory Transitive_Closure |
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
9 |
imports Relation |
15131 | 10 |
begin |
12691 | 11 |
|
48891 | 12 |
ML_file "~~/src/Provers/trancl.ML" |
13 |
||
60758 | 14 |
text \<open> |
61799 | 15 |
\<open>rtrancl\<close> is reflexive/transitive closure, |
16 |
\<open>trancl\<close> is transitive closure, |
|
17 |
\<open>reflcl\<close> is reflexive closure. |
|
12691 | 18 |
|
19 |
These postfix operators have \emph{maximum priority}, forcing their |
|
20 |
operands to be atomic. |
|
60758 | 21 |
\<close> |
10213 | 22 |
|
61681
ca53150406c9
option "inductive_defs" controls exposure of def and mono facts;
wenzelm
parents:
61424
diff
changeset
|
23 |
context |
62093 | 24 |
notes [[inductive_internals]] |
61681
ca53150406c9
option "inductive_defs" controls exposure of def and mono facts;
wenzelm
parents:
61424
diff
changeset
|
25 |
begin |
ca53150406c9
option "inductive_defs" controls exposure of def and mono facts;
wenzelm
parents:
61424
diff
changeset
|
26 |
|
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
27 |
inductive_set rtrancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" ("(_\<^sup>*)" [1000] 999) |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
28 |
for r :: "('a \<times> 'a) set" |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
29 |
where |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
30 |
rtrancl_refl [intro!, Pure.intro!, simp]: "(a, a) \<in> r\<^sup>*" |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
31 |
| rtrancl_into_rtrancl [Pure.intro]: "(a, b) \<in> r\<^sup>* \<Longrightarrow> (b, c) \<in> r \<Longrightarrow> (a, c) \<in> r\<^sup>*" |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
32 |
|
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
33 |
inductive_set trancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" ("(_\<^sup>+)" [1000] 999) |
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
34 |
for r :: "('a \<times> 'a) set" |
22262 | 35 |
where |
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
36 |
r_into_trancl [intro, Pure.intro]: "(a, b) \<in> r \<Longrightarrow> (a, b) \<in> r\<^sup>+" |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
37 |
| trancl_into_trancl [Pure.intro]: "(a, b) \<in> r\<^sup>+ \<Longrightarrow> (b, c) \<in> r \<Longrightarrow> (a, c) \<in> r\<^sup>+" |
11327
cd2c27a23df1
Transitive closure is now defined via "inductive".
berghofe
parents:
11115
diff
changeset
|
38 |
|
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
39 |
notation |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
40 |
rtranclp ("(_\<^sup>*\<^sup>*)" [1000] 1000) and |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
41 |
tranclp ("(_\<^sup>+\<^sup>+)" [1000] 1000) |
13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset
|
42 |
|
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
43 |
declare |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
44 |
rtrancl_def [nitpick_unfold del] |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
45 |
rtranclp_def [nitpick_unfold del] |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
46 |
trancl_def [nitpick_unfold del] |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
47 |
tranclp_def [nitpick_unfold del] |
33878
85102f57b4a8
removed "nitpick_def" attributes from (r)trancl(p), since "Nitpick.thy" overrides these
blanchet
parents:
33656
diff
changeset
|
48 |
|
61681
ca53150406c9
option "inductive_defs" controls exposure of def and mono facts;
wenzelm
parents:
61424
diff
changeset
|
49 |
end |
ca53150406c9
option "inductive_defs" controls exposure of def and mono facts;
wenzelm
parents:
61424
diff
changeset
|
50 |
|
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
51 |
abbreviation reflcl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" ("(_\<^sup>=)" [1000] 999) |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
52 |
where "r\<^sup>= \<equiv> r \<union> Id" |
10213 | 53 |
|
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
54 |
abbreviation reflclp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(_\<^sup>=\<^sup>=)" [1000] 1000) |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
55 |
where "r\<^sup>=\<^sup>= \<equiv> sup r op =" |
22262 | 56 |
|
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
57 |
notation (ASCII) |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
58 |
rtrancl ("(_^*)" [1000] 999) and |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
59 |
trancl ("(_^+)" [1000] 999) and |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
60 |
reflcl ("(_^=)" [1000] 999) and |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
61 |
rtranclp ("(_^**)" [1000] 1000) and |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
62 |
tranclp ("(_^++)" [1000] 1000) and |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
63 |
reflclp ("(_^==)" [1000] 1000) |
12691 | 64 |
|
65 |
||
60758 | 66 |
subsection \<open>Reflexive closure\<close> |
26271 | 67 |
|
63404 | 68 |
lemma refl_reflcl[simp]: "refl (r\<^sup>=)" |
69 |
by (simp add: refl_on_def) |
|
26271 | 70 |
|
63404 | 71 |
lemma antisym_reflcl[simp]: "antisym (r\<^sup>=) = antisym r" |
72 |
by (simp add: antisym_def) |
|
26271 | 73 |
|
63404 | 74 |
lemma trans_reflclI[simp]: "trans r \<Longrightarrow> trans (r\<^sup>=)" |
75 |
unfolding trans_def by blast |
|
26271 | 76 |
|
63404 | 77 |
lemma reflclp_idemp [simp]: "(P\<^sup>=\<^sup>=)\<^sup>=\<^sup>= = P\<^sup>=\<^sup>=" |
78 |
by blast |
|
79 |
||
26271 | 80 |
|
60758 | 81 |
subsection \<open>Reflexive-transitive closure\<close> |
12691 | 82 |
|
32883
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32601
diff
changeset
|
83 |
lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) op =) = (\<lambda>x y. (x, y) \<in> r \<union> Id)" |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
84 |
by (auto simp add: fun_eq_iff) |
22262 | 85 |
|
63404 | 86 |
lemma r_into_rtrancl [intro]: "\<And>p. p \<in> r \<Longrightarrow> p \<in> r\<^sup>*" |
61799 | 87 |
\<comment> \<open>\<open>rtrancl\<close> of \<open>r\<close> contains \<open>r\<close>\<close> |
12691 | 88 |
apply (simp only: split_tupled_all) |
89 |
apply (erule rtrancl_refl [THEN rtrancl_into_rtrancl]) |
|
90 |
done |
|
91 |
||
63404 | 92 |
lemma r_into_rtranclp [intro]: "r x y \<Longrightarrow> r\<^sup>*\<^sup>* x y" |
61799 | 93 |
\<comment> \<open>\<open>rtrancl\<close> of \<open>r\<close> contains \<open>r\<close>\<close> |
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
94 |
by (erule rtranclp.rtrancl_refl [THEN rtranclp.rtrancl_into_rtrancl]) |
22262 | 95 |
|
63404 | 96 |
lemma rtranclp_mono: "r \<le> s \<Longrightarrow> r\<^sup>*\<^sup>* \<le> s\<^sup>*\<^sup>*" |
61799 | 97 |
\<comment> \<open>monotonicity of \<open>rtrancl\<close>\<close> |
22262 | 98 |
apply (rule predicate2I) |
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
99 |
apply (erule rtranclp.induct) |
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
100 |
apply (rule_tac [2] rtranclp.rtrancl_into_rtrancl, blast+) |
12691 | 101 |
done |
102 |
||
63404 | 103 |
lemma mono_rtranclp[mono]: "(\<And>a b. x a b \<longrightarrow> y a b) \<Longrightarrow> x\<^sup>*\<^sup>* a b \<longrightarrow> y\<^sup>*\<^sup>* a b" |
60681 | 104 |
using rtranclp_mono[of x y] by auto |
105 |
||
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
106 |
lemmas rtrancl_mono = rtranclp_mono [to_set] |
22262 | 107 |
|
26179
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
108 |
theorem rtranclp_induct [consumes 1, case_names base step, induct set: rtranclp]: |
63404 | 109 |
assumes a: "r\<^sup>*\<^sup>* a b" |
110 |
and cases: "P a" "\<And>y z. r\<^sup>*\<^sup>* a y \<Longrightarrow> r y z \<Longrightarrow> P y \<Longrightarrow> P z" |
|
111 |
shows "P b" |
|
112 |
using a by (induct x\<equiv>a b) (rule cases)+ |
|
12691 | 113 |
|
25425
9191942c4ead
Removed some case_names and consumes attributes that are now no longer
berghofe
parents:
25295
diff
changeset
|
114 |
lemmas rtrancl_induct [induct set: rtrancl] = rtranclp_induct [to_set] |
22262 | 115 |
|
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
116 |
lemmas rtranclp_induct2 = |
63404 | 117 |
rtranclp_induct[of _ "(ax,ay)" "(bx,by)", split_rule, consumes 1, case_names refl step] |
22262 | 118 |
|
14404
4952c5a92e04
Transitive_Closure: added consumes and case_names attributes
nipkow
parents:
14398
diff
changeset
|
119 |
lemmas rtrancl_induct2 = |
63404 | 120 |
rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete), consumes 1, case_names refl step] |
18372 | 121 |
|
63404 | 122 |
lemma refl_rtrancl: "refl (r\<^sup>*)" |
123 |
unfolding refl_on_def by fast |
|
19228 | 124 |
|
60758 | 125 |
text \<open>Transitivity of transitive closure.\<close> |
63404 | 126 |
lemma trans_rtrancl: "trans (r\<^sup>*)" |
12823 | 127 |
proof (rule transI) |
128 |
fix x y z |
|
129 |
assume "(x, y) \<in> r\<^sup>*" |
|
130 |
assume "(y, z) \<in> r\<^sup>*" |
|
26179
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
131 |
then show "(x, z) \<in> r\<^sup>*" |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
132 |
proof induct |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
133 |
case base |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
134 |
show "(x, y) \<in> r\<^sup>*" by fact |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
135 |
next |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
136 |
case (step u v) |
60758 | 137 |
from \<open>(x, u) \<in> r\<^sup>*\<close> and \<open>(u, v) \<in> r\<close> |
26179
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
138 |
show "(x, v) \<in> r\<^sup>*" .. |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
139 |
qed |
12823 | 140 |
qed |
12691 | 141 |
|
45607 | 142 |
lemmas rtrancl_trans = trans_rtrancl [THEN transD] |
12691 | 143 |
|
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
144 |
lemma rtranclp_trans: |
63404 | 145 |
assumes "r\<^sup>*\<^sup>* x y" |
146 |
and "r\<^sup>*\<^sup>* y z" |
|
147 |
shows "r\<^sup>*\<^sup>* x z" |
|
148 |
using assms(2,1) by induct iprover+ |
|
22262 | 149 |
|
26174
9efd4c04eaa4
rtranclE, tranclE: tuned statement, added case_names;
wenzelm
parents:
25425
diff
changeset
|
150 |
lemma rtranclE [cases set: rtrancl]: |
63404 | 151 |
fixes a b :: 'a |
152 |
assumes major: "(a, b) \<in> r\<^sup>*" |
|
26174
9efd4c04eaa4
rtranclE, tranclE: tuned statement, added case_names;
wenzelm
parents:
25425
diff
changeset
|
153 |
obtains |
9efd4c04eaa4
rtranclE, tranclE: tuned statement, added case_names;
wenzelm
parents:
25425
diff
changeset
|
154 |
(base) "a = b" |
63404 | 155 |
| (step) y where "(a, y) \<in> r\<^sup>*" and "(y, b) \<in> r" |
61799 | 156 |
\<comment> \<open>elimination of \<open>rtrancl\<close> -- by induction on a special formula\<close> |
63404 | 157 |
apply (subgoal_tac "a = b \<or> (\<exists>y. (a, y) \<in> r\<^sup>* \<and> (y, b) \<in> r)") |
18372 | 158 |
apply (rule_tac [2] major [THEN rtrancl_induct]) |
159 |
prefer 2 apply blast |
|
160 |
prefer 2 apply blast |
|
26174
9efd4c04eaa4
rtranclE, tranclE: tuned statement, added case_names;
wenzelm
parents:
25425
diff
changeset
|
161 |
apply (erule asm_rl exE disjE conjE base step)+ |
18372 | 162 |
done |
12691 | 163 |
|
63404 | 164 |
lemma rtrancl_Int_subset: "Id \<subseteq> s \<Longrightarrow> (r\<^sup>* \<inter> s) O r \<subseteq> s \<Longrightarrow> r\<^sup>* \<subseteq> s" |
22080
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset
|
165 |
apply (rule subsetI) |
61032
b57df8eecad6
standardized some occurences of ancient "split" alias
haftmann
parents:
60758
diff
changeset
|
166 |
apply auto |
b57df8eecad6
standardized some occurences of ancient "split" alias
haftmann
parents:
60758
diff
changeset
|
167 |
apply (erule rtrancl_induct) |
b57df8eecad6
standardized some occurences of ancient "split" alias
haftmann
parents:
60758
diff
changeset
|
168 |
apply auto |
22080
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset
|
169 |
done |
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset
|
170 |
|
63404 | 171 |
lemma converse_rtranclp_into_rtranclp: "r a b \<Longrightarrow> r\<^sup>*\<^sup>* b c \<Longrightarrow> r\<^sup>*\<^sup>* a c" |
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
172 |
by (rule rtranclp_trans) iprover+ |
22262 | 173 |
|
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
174 |
lemmas converse_rtrancl_into_rtrancl = converse_rtranclp_into_rtranclp [to_set] |
12691 | 175 |
|
63404 | 176 |
text \<open>\<^medskip> More @{term "r\<^sup>*"} equations and inclusions.\<close> |
12691 | 177 |
|
63404 | 178 |
lemma rtranclp_idemp [simp]: "(r\<^sup>*\<^sup>*)\<^sup>*\<^sup>* = r\<^sup>*\<^sup>*" |
22262 | 179 |
apply (auto intro!: order_antisym) |
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
180 |
apply (erule rtranclp_induct) |
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
181 |
apply (rule rtranclp.rtrancl_refl) |
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
182 |
apply (blast intro: rtranclp_trans) |
12691 | 183 |
done |
184 |
||
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
185 |
lemmas rtrancl_idemp [simp] = rtranclp_idemp [to_set] |
22262 | 186 |
|
63404 | 187 |
lemma rtrancl_idemp_self_comp [simp]: "R\<^sup>* O R\<^sup>* = R\<^sup>*" |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
188 |
apply (rule set_eqI) |
12691 | 189 |
apply (simp only: split_tupled_all) |
190 |
apply (blast intro: rtrancl_trans) |
|
191 |
done |
|
192 |
||
63404 | 193 |
lemma rtrancl_subset_rtrancl: "r \<subseteq> s\<^sup>* \<Longrightarrow> r\<^sup>* \<subseteq> s\<^sup>*" |
26179
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
194 |
apply (drule rtrancl_mono) |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
195 |
apply simp |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
196 |
done |
12691 | 197 |
|
63404 | 198 |
lemma rtranclp_subset: "R \<le> S \<Longrightarrow> S \<le> R\<^sup>*\<^sup>* \<Longrightarrow> S\<^sup>*\<^sup>* = R\<^sup>*\<^sup>*" |
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
199 |
apply (drule rtranclp_mono) |
26179
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
200 |
apply (drule rtranclp_mono) |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
201 |
apply simp |
12691 | 202 |
done |
203 |
||
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
204 |
lemmas rtrancl_subset = rtranclp_subset [to_set] |
22262 | 205 |
|
63404 | 206 |
lemma rtranclp_sup_rtranclp: "(sup (R\<^sup>*\<^sup>*) (S\<^sup>*\<^sup>*))\<^sup>*\<^sup>* = (sup R S)\<^sup>*\<^sup>*" |
207 |
by (blast intro!: rtranclp_subset intro: rtranclp_mono [THEN predicate2D]) |
|
12691 | 208 |
|
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
209 |
lemmas rtrancl_Un_rtrancl = rtranclp_sup_rtranclp [to_set] |
22262 | 210 |
|
63404 | 211 |
lemma rtranclp_reflclp [simp]: "(R\<^sup>=\<^sup>=)\<^sup>*\<^sup>* = R\<^sup>*\<^sup>*" |
212 |
by (blast intro!: rtranclp_subset) |
|
22262 | 213 |
|
50616 | 214 |
lemmas rtrancl_reflcl [simp] = rtranclp_reflclp [to_set] |
12691 | 215 |
|
63404 | 216 |
lemma rtrancl_r_diff_Id: "(r - Id)\<^sup>* = r\<^sup>*" |
12691 | 217 |
apply (rule sym) |
14208 | 218 |
apply (rule rtrancl_subset, blast, clarify) |
12691 | 219 |
apply (rename_tac a b) |
26179
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
220 |
apply (case_tac "a = b") |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
221 |
apply blast |
44921 | 222 |
apply blast |
12691 | 223 |
done |
224 |
||
63404 | 225 |
lemma rtranclp_r_diff_Id: "(inf r op \<noteq>)\<^sup>*\<^sup>* = r\<^sup>*\<^sup>*" |
22262 | 226 |
apply (rule sym) |
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
227 |
apply (rule rtranclp_subset) |
26179
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
228 |
apply blast+ |
22262 | 229 |
done |
230 |
||
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
231 |
theorem rtranclp_converseD: |
63404 | 232 |
assumes "(r\<inverse>\<inverse>)\<^sup>*\<^sup>* x y" |
233 |
shows "r\<^sup>*\<^sup>* y x" |
|
234 |
using assms by induct (iprover intro: rtranclp_trans dest!: conversepD)+ |
|
12691 | 235 |
|
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
236 |
lemmas rtrancl_converseD = rtranclp_converseD [to_set] |
22262 | 237 |
|
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
238 |
theorem rtranclp_converseI: |
63404 | 239 |
assumes "r\<^sup>*\<^sup>* y x" |
240 |
shows "(r\<inverse>\<inverse>)\<^sup>*\<^sup>* x y" |
|
241 |
using assms by induct (iprover intro: rtranclp_trans conversepI)+ |
|
12691 | 242 |
|
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
243 |
lemmas rtrancl_converseI = rtranclp_converseI [to_set] |
22262 | 244 |
|
63404 | 245 |
lemma rtrancl_converse: "(r^-1)\<^sup>* = (r\<^sup>*)^-1" |
12691 | 246 |
by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI) |
247 |
||
63404 | 248 |
lemma sym_rtrancl: "sym r \<Longrightarrow> sym (r\<^sup>*)" |
19228 | 249 |
by (simp only: sym_conv_converse_eq rtrancl_converse [symmetric]) |
250 |
||
34909
a799687944af
Tuned some proofs; nicer case names for some of the induction / cases rules.
berghofe
parents:
33878
diff
changeset
|
251 |
theorem converse_rtranclp_induct [consumes 1, case_names base step]: |
63404 | 252 |
assumes major: "r\<^sup>*\<^sup>* a b" |
253 |
and cases: "P b" "\<And>y z. r y z \<Longrightarrow> r\<^sup>*\<^sup>* z b \<Longrightarrow> P z \<Longrightarrow> P y" |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12823
diff
changeset
|
254 |
shows "P a" |
26179
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
255 |
using rtranclp_converseI [OF major] |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
256 |
by induct (iprover intro: cases dest!: conversepD rtranclp_converseD)+ |
12691 | 257 |
|
25425
9191942c4ead
Removed some case_names and consumes attributes that are now no longer
berghofe
parents:
25295
diff
changeset
|
258 |
lemmas converse_rtrancl_induct = converse_rtranclp_induct [to_set] |
22262 | 259 |
|
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
260 |
lemmas converse_rtranclp_induct2 = |
63404 | 261 |
converse_rtranclp_induct [of _ "(ax,ay)" "(bx,by)", split_rule, consumes 1, case_names refl step] |
22262 | 262 |
|
14404
4952c5a92e04
Transitive_Closure: added consumes and case_names attributes
nipkow
parents:
14398
diff
changeset
|
263 |
lemmas converse_rtrancl_induct2 = |
26179
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
264 |
converse_rtrancl_induct [of "(ax,ay)" "(bx,by)", split_format (complete), |
63404 | 265 |
consumes 1, case_names refl step] |
12691 | 266 |
|
34909
a799687944af
Tuned some proofs; nicer case names for some of the induction / cases rules.
berghofe
parents:
33878
diff
changeset
|
267 |
lemma converse_rtranclpE [consumes 1, case_names base step]: |
63404 | 268 |
assumes major: "r\<^sup>*\<^sup>* x z" |
269 |
and cases: "x = z \<Longrightarrow> P" "\<And>y. r x y \<Longrightarrow> r\<^sup>*\<^sup>* y z \<Longrightarrow> P" |
|
18372 | 270 |
shows P |
63404 | 271 |
apply (subgoal_tac "x = z \<or> (\<exists>y. r x y \<and> r\<^sup>*\<^sup>* y z)") |
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
272 |
apply (rule_tac [2] major [THEN converse_rtranclp_induct]) |
18372 | 273 |
prefer 2 apply iprover |
274 |
prefer 2 apply iprover |
|
275 |
apply (erule asm_rl exE disjE conjE cases)+ |
|
276 |
done |
|
12691 | 277 |
|
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
278 |
lemmas converse_rtranclE = converse_rtranclpE [to_set] |
22262 | 279 |
|
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
280 |
lemmas converse_rtranclpE2 = converse_rtranclpE [of _ "(xa,xb)" "(za,zb)", split_rule] |
22262 | 281 |
|
282 |
lemmas converse_rtranclE2 = converse_rtranclE [of "(xa,xb)" "(za,zb)", split_rule] |
|
12691 | 283 |
|
63404 | 284 |
lemma r_comp_rtrancl_eq: "r O r\<^sup>* = r\<^sup>* O r" |
12691 | 285 |
by (blast elim: rtranclE converse_rtranclE |
286 |
intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl) |
|
287 |
||
63404 | 288 |
lemma rtrancl_unfold: "r\<^sup>* = Id \<union> r\<^sup>* O r" |
15551 | 289 |
by (auto intro: rtrancl_into_rtrancl elim: rtranclE) |
290 |
||
31690 | 291 |
lemma rtrancl_Un_separatorE: |
63404 | 292 |
"(a, b) \<in> (P \<union> Q)\<^sup>* \<Longrightarrow> \<forall>x y. (a, x) \<in> P\<^sup>* \<longrightarrow> (x, y) \<in> Q \<longrightarrow> x = y \<Longrightarrow> (a, b) \<in> P\<^sup>*" |
293 |
apply (induct rule:rtrancl.induct) |
|
294 |
apply blast |
|
295 |
apply (blast intro:rtrancl_trans) |
|
296 |
done |
|
31690 | 297 |
|
298 |
lemma rtrancl_Un_separator_converseE: |
|
63404 | 299 |
"(a, b) \<in> (P \<union> Q)\<^sup>* \<Longrightarrow> \<forall>x y. (x, b) \<in> P\<^sup>* \<longrightarrow> (y, x) \<in> Q \<longrightarrow> y = x \<Longrightarrow> (a, b) \<in> P\<^sup>*" |
300 |
apply (induct rule:converse_rtrancl_induct) |
|
301 |
apply blast |
|
302 |
apply (blast intro:rtrancl_trans) |
|
303 |
done |
|
31690 | 304 |
|
34970 | 305 |
lemma Image_closed_trancl: |
63404 | 306 |
assumes "r `` X \<subseteq> X" |
307 |
shows "r\<^sup>* `` X = X" |
|
34970 | 308 |
proof - |
63404 | 309 |
from assms have **: "{y. \<exists>x\<in>X. (x, y) \<in> r} \<subseteq> X" |
310 |
by auto |
|
311 |
have "x \<in> X" if 1: "(y, x) \<in> r\<^sup>*" and 2: "y \<in> X" for x y |
|
34970 | 312 |
proof - |
63404 | 313 |
from 1 show "x \<in> X" |
34970 | 314 |
proof induct |
63404 | 315 |
case base |
316 |
show ?case by (fact 2) |
|
34970 | 317 |
next |
63404 | 318 |
case step |
319 |
with ** show ?case by auto |
|
34970 | 320 |
qed |
321 |
qed |
|
322 |
then show ?thesis by auto |
|
323 |
qed |
|
324 |
||
12691 | 325 |
|
60758 | 326 |
subsection \<open>Transitive closure\<close> |
10331 | 327 |
|
63404 | 328 |
lemma trancl_mono: "\<And>p. p \<in> r\<^sup>+ \<Longrightarrow> r \<subseteq> s \<Longrightarrow> p \<in> s\<^sup>+" |
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
329 |
apply (simp add: split_tupled_all) |
13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset
|
330 |
apply (erule trancl.induct) |
26179
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
331 |
apply (iprover dest: subsetD)+ |
12691 | 332 |
done |
333 |
||
63404 | 334 |
lemma r_into_trancl': "\<And>p. p \<in> r \<Longrightarrow> p \<in> r\<^sup>+" |
13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset
|
335 |
by (simp only: split_tupled_all) (erule r_into_trancl) |
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset
|
336 |
|
63404 | 337 |
text \<open>\<^medskip> Conversions between \<open>trancl\<close> and \<open>rtrancl\<close>.\<close> |
12691 | 338 |
|
63404 | 339 |
lemma tranclp_into_rtranclp: "r\<^sup>+\<^sup>+ a b \<Longrightarrow> r\<^sup>*\<^sup>* a b" |
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
340 |
by (erule tranclp.induct) iprover+ |
12691 | 341 |
|
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
342 |
lemmas trancl_into_rtrancl = tranclp_into_rtranclp [to_set] |
22262 | 343 |
|
63404 | 344 |
lemma rtranclp_into_tranclp1: |
345 |
assumes "r\<^sup>*\<^sup>* a b" |
|
346 |
shows "r b c \<Longrightarrow> r\<^sup>+\<^sup>+ a c" |
|
347 |
using assms by (induct arbitrary: c) iprover+ |
|
12691 | 348 |
|
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
349 |
lemmas rtrancl_into_trancl1 = rtranclp_into_tranclp1 [to_set] |
22262 | 350 |
|
63404 | 351 |
lemma rtranclp_into_tranclp2: "r a b \<Longrightarrow> r\<^sup>*\<^sup>* b c \<Longrightarrow> r\<^sup>+\<^sup>+ a c" |
61799 | 352 |
\<comment> \<open>intro rule from \<open>r\<close> and \<open>rtrancl\<close>\<close> |
26179
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
353 |
apply (erule rtranclp.cases) |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
354 |
apply iprover |
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
355 |
apply (rule rtranclp_trans [THEN rtranclp_into_tranclp1]) |
26179
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
356 |
apply (simp | rule r_into_rtranclp)+ |
12691 | 357 |
done |
358 |
||
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
359 |
lemmas rtrancl_into_trancl2 = rtranclp_into_tranclp2 [to_set] |
22262 | 360 |
|
61799 | 361 |
text \<open>Nice induction rule for \<open>trancl\<close>\<close> |
26179
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
362 |
lemma tranclp_induct [consumes 1, case_names base step, induct pred: tranclp]: |
63404 | 363 |
assumes a: "r\<^sup>+\<^sup>+ a b" |
364 |
and cases: "\<And>y. r a y \<Longrightarrow> P y" "\<And>y z. r\<^sup>+\<^sup>+ a y \<Longrightarrow> r y z \<Longrightarrow> P y \<Longrightarrow> P z" |
|
365 |
shows "P b" |
|
366 |
using a by (induct x\<equiv>a b) (iprover intro: cases)+ |
|
12691 | 367 |
|
25425
9191942c4ead
Removed some case_names and consumes attributes that are now no longer
berghofe
parents:
25295
diff
changeset
|
368 |
lemmas trancl_induct [induct set: trancl] = tranclp_induct [to_set] |
22262 | 369 |
|
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
370 |
lemmas tranclp_induct2 = |
63404 | 371 |
tranclp_induct [of _ "(ax,ay)" "(bx,by)", split_rule, consumes 1, case_names base step] |
22262 | 372 |
|
22172 | 373 |
lemmas trancl_induct2 = |
26179
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
374 |
trancl_induct [of "(ax,ay)" "(bx,by)", split_format (complete), |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
375 |
consumes 1, case_names base step] |
22172 | 376 |
|
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
377 |
lemma tranclp_trans_induct: |
63404 | 378 |
assumes major: "r\<^sup>+\<^sup>+ x y" |
379 |
and cases: "\<And>x y. r x y \<Longrightarrow> P x y" "\<And>x y z. r\<^sup>+\<^sup>+ x y \<Longrightarrow> P x y \<Longrightarrow> r\<^sup>+\<^sup>+ y z \<Longrightarrow> P y z \<Longrightarrow> P x z" |
|
18372 | 380 |
shows "P x y" |
61799 | 381 |
\<comment> \<open>Another induction rule for trancl, incorporating transitivity\<close> |
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
382 |
by (iprover intro: major [THEN tranclp_induct] cases) |
12691 | 383 |
|
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
384 |
lemmas trancl_trans_induct = tranclp_trans_induct [to_set] |
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
385 |
|
26174
9efd4c04eaa4
rtranclE, tranclE: tuned statement, added case_names;
wenzelm
parents:
25425
diff
changeset
|
386 |
lemma tranclE [cases set: trancl]: |
63404 | 387 |
assumes "(a, b) \<in> r\<^sup>+" |
26174
9efd4c04eaa4
rtranclE, tranclE: tuned statement, added case_names;
wenzelm
parents:
25425
diff
changeset
|
388 |
obtains |
63404 | 389 |
(base) "(a, b) \<in> r" |
390 |
| (step) c where "(a, c) \<in> r\<^sup>+" and "(c, b) \<in> r" |
|
26174
9efd4c04eaa4
rtranclE, tranclE: tuned statement, added case_names;
wenzelm
parents:
25425
diff
changeset
|
391 |
using assms by cases simp_all |
10980 | 392 |
|
63404 | 393 |
lemma trancl_Int_subset: "r \<subseteq> s \<Longrightarrow> (r\<^sup>+ \<inter> s) O r \<subseteq> s \<Longrightarrow> r\<^sup>+ \<subseteq> s" |
22080
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset
|
394 |
apply (rule subsetI) |
61032
b57df8eecad6
standardized some occurences of ancient "split" alias
haftmann
parents:
60758
diff
changeset
|
395 |
apply auto |
26179
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
396 |
apply (erule trancl_induct) |
61032
b57df8eecad6
standardized some occurences of ancient "split" alias
haftmann
parents:
60758
diff
changeset
|
397 |
apply auto |
22080
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset
|
398 |
done |
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset
|
399 |
|
63404 | 400 |
lemma trancl_unfold: "r\<^sup>+ = r \<union> r\<^sup>+ O r" |
15551 | 401 |
by (auto intro: trancl_into_trancl elim: tranclE) |
402 |
||
63404 | 403 |
text \<open>Transitivity of @{term "r\<^sup>+"}\<close> |
404 |
lemma trans_trancl [simp]: "trans (r\<^sup>+)" |
|
13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset
|
405 |
proof (rule transI) |
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset
|
406 |
fix x y z |
63404 | 407 |
assume "(x, y) \<in> r\<^sup>+" |
408 |
assume "(y, z) \<in> r\<^sup>+" |
|
409 |
then show "(x, z) \<in> r\<^sup>+" |
|
26179
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
410 |
proof induct |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
411 |
case (base u) |
63404 | 412 |
from \<open>(x, y) \<in> r\<^sup>+\<close> and \<open>(y, u) \<in> r\<close> |
413 |
show "(x, u) \<in> r\<^sup>+" .. |
|
26179
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
414 |
next |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
415 |
case (step u v) |
63404 | 416 |
from \<open>(x, u) \<in> r\<^sup>+\<close> and \<open>(u, v) \<in> r\<close> |
417 |
show "(x, v) \<in> r\<^sup>+" .. |
|
26179
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
418 |
qed |
13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset
|
419 |
qed |
12691 | 420 |
|
45607 | 421 |
lemmas trancl_trans = trans_trancl [THEN transD] |
12691 | 422 |
|
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
423 |
lemma tranclp_trans: |
63404 | 424 |
assumes "r\<^sup>+\<^sup>+ x y" |
425 |
and "r\<^sup>+\<^sup>+ y z" |
|
426 |
shows "r\<^sup>+\<^sup>+ x z" |
|
427 |
using assms(2,1) by induct iprover+ |
|
22262 | 428 |
|
63404 | 429 |
lemma trancl_id [simp]: "trans r \<Longrightarrow> r\<^sup>+ = r" |
26179
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
430 |
apply auto |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
431 |
apply (erule trancl_induct) |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
432 |
apply assumption |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
433 |
apply (unfold trans_def) |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
434 |
apply blast |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
435 |
done |
19623 | 436 |
|
26179
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
437 |
lemma rtranclp_tranclp_tranclp: |
63404 | 438 |
assumes "r\<^sup>*\<^sup>* x y" |
439 |
shows "\<And>z. r\<^sup>+\<^sup>+ y z \<Longrightarrow> r\<^sup>+\<^sup>+ x z" |
|
440 |
using assms by induct (iprover intro: tranclp_trans)+ |
|
12691 | 441 |
|
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
442 |
lemmas rtrancl_trancl_trancl = rtranclp_tranclp_tranclp [to_set] |
22262 | 443 |
|
63404 | 444 |
lemma tranclp_into_tranclp2: "r a b \<Longrightarrow> r\<^sup>+\<^sup>+ b c \<Longrightarrow> r\<^sup>+\<^sup>+ a c" |
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
445 |
by (erule tranclp_trans [OF tranclp.r_into_trancl]) |
22262 | 446 |
|
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
447 |
lemmas trancl_into_trancl2 = tranclp_into_tranclp2 [to_set] |
12691 | 448 |
|
63404 | 449 |
lemma tranclp_converseI: "(r\<^sup>+\<^sup>+)\<inverse>\<inverse> x y \<Longrightarrow> (r\<inverse>\<inverse>)\<^sup>+\<^sup>+ x y" |
22262 | 450 |
apply (drule conversepD) |
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
451 |
apply (erule tranclp_induct) |
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
452 |
apply (iprover intro: conversepI tranclp_trans)+ |
12691 | 453 |
done |
454 |
||
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
455 |
lemmas trancl_converseI = tranclp_converseI [to_set] |
22262 | 456 |
|
63404 | 457 |
lemma tranclp_converseD: "(r\<inverse>\<inverse>)\<^sup>+\<^sup>+ x y \<Longrightarrow> (r\<^sup>+\<^sup>+)\<inverse>\<inverse> x y" |
22262 | 458 |
apply (rule conversepI) |
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
459 |
apply (erule tranclp_induct) |
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
460 |
apply (iprover dest: conversepD intro: tranclp_trans)+ |
13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset
|
461 |
done |
12691 | 462 |
|
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
463 |
lemmas trancl_converseD = tranclp_converseD [to_set] |
22262 | 464 |
|
63404 | 465 |
lemma tranclp_converse: "(r\<inverse>\<inverse>)\<^sup>+\<^sup>+ = (r\<^sup>+\<^sup>+)\<inverse>\<inverse>" |
466 |
by (fastforce simp add: fun_eq_iff intro!: tranclp_converseI dest!: tranclp_converseD) |
|
22262 | 467 |
|
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
468 |
lemmas trancl_converse = tranclp_converse [to_set] |
12691 | 469 |
|
63404 | 470 |
lemma sym_trancl: "sym r \<Longrightarrow> sym (r\<^sup>+)" |
19228 | 471 |
by (simp only: sym_conv_converse_eq trancl_converse [symmetric]) |
472 |
||
34909
a799687944af
Tuned some proofs; nicer case names for some of the induction / cases rules.
berghofe
parents:
33878
diff
changeset
|
473 |
lemma converse_tranclp_induct [consumes 1, case_names base step]: |
63404 | 474 |
assumes major: "r\<^sup>+\<^sup>+ a b" |
475 |
and cases: "\<And>y. r y b \<Longrightarrow> P y" "\<And>y z. r y z \<Longrightarrow> r\<^sup>+\<^sup>+ z b \<Longrightarrow> P z \<Longrightarrow> P y" |
|
18372 | 476 |
shows "P a" |
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
477 |
apply (rule tranclp_induct [OF tranclp_converseI, OF conversepI, OF major]) |
18372 | 478 |
apply (rule cases) |
22262 | 479 |
apply (erule conversepD) |
35216 | 480 |
apply (blast intro: assms dest!: tranclp_converseD) |
18372 | 481 |
done |
12691 | 482 |
|
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
483 |
lemmas converse_trancl_induct = converse_tranclp_induct [to_set] |
22262 | 484 |
|
63404 | 485 |
lemma tranclpD: "R\<^sup>+\<^sup>+ x y \<Longrightarrow> \<exists>z. R x z \<and> R\<^sup>*\<^sup>* z y" |
26179
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
486 |
apply (erule converse_tranclp_induct) |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
487 |
apply auto |
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
488 |
apply (blast intro: rtranclp_trans) |
12691 | 489 |
done |
490 |
||
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
491 |
lemmas tranclD = tranclpD [to_set] |
22262 | 492 |
|
31577 | 493 |
lemma converse_tranclpE: |
494 |
assumes major: "tranclp r x z" |
|
63404 | 495 |
and base: "r x z \<Longrightarrow> P" |
496 |
and step: "\<And> y. r x y \<Longrightarrow> tranclp r y z \<Longrightarrow> P" |
|
31577 | 497 |
shows P |
498 |
proof - |
|
63404 | 499 |
from tranclpD [OF major] obtain y where "r x y" and "rtranclp r y z" |
500 |
by iprover |
|
31577 | 501 |
from this(2) show P |
502 |
proof (cases rule: rtranclp.cases) |
|
503 |
case rtrancl_refl |
|
63404 | 504 |
with \<open>r x y\<close> base show P |
505 |
by iprover |
|
31577 | 506 |
next |
507 |
case rtrancl_into_rtrancl |
|
508 |
from this have "tranclp r y z" |
|
509 |
by (iprover intro: rtranclp_into_tranclp1) |
|
63404 | 510 |
with \<open>r x y\<close> step show P |
511 |
by iprover |
|
31577 | 512 |
qed |
513 |
qed |
|
514 |
||
515 |
lemmas converse_tranclE = converse_tranclpE [to_set] |
|
516 |
||
63404 | 517 |
lemma tranclD2: "(x, y) \<in> R\<^sup>+ \<Longrightarrow> \<exists>z. (x, z) \<in> R\<^sup>* \<and> (z, y) \<in> R" |
25295
12985023be5e
tranclD2 (tranclD at the other end) + trancl_power
kleing
parents:
23743
diff
changeset
|
518 |
by (blast elim: tranclE intro: trancl_into_rtrancl) |
12985023be5e
tranclD2 (tranclD at the other end) + trancl_power
kleing
parents:
23743
diff
changeset
|
519 |
|
63404 | 520 |
lemma irrefl_tranclI: "r\<inverse> \<inter> r\<^sup>* = {} \<Longrightarrow> (x, x) \<notin> r\<^sup>+" |
18372 | 521 |
by (blast elim: tranclE dest: trancl_into_rtrancl) |
12691 | 522 |
|
63404 | 523 |
lemma irrefl_trancl_rD: "\<forall>x. (x, x) \<notin> r\<^sup>+ \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> x \<noteq> y" |
12691 | 524 |
by (blast dest: r_into_trancl) |
525 |
||
63404 | 526 |
lemma trancl_subset_Sigma_aux: "(a, b) \<in> r\<^sup>* \<Longrightarrow> r \<subseteq> A \<times> A \<Longrightarrow> a = b \<or> a \<in> A" |
18372 | 527 |
by (induct rule: rtrancl_induct) auto |
12691 | 528 |
|
63404 | 529 |
lemma trancl_subset_Sigma: "r \<subseteq> A \<times> A \<Longrightarrow> r\<^sup>+ \<subseteq> A \<times> A" |
13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset
|
530 |
apply (rule subsetI) |
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset
|
531 |
apply (simp only: split_tupled_all) |
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset
|
532 |
apply (erule tranclE) |
26179
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
533 |
apply (blast dest!: trancl_into_rtrancl trancl_subset_Sigma_aux)+ |
12691 | 534 |
done |
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
535 |
|
63404 | 536 |
lemma reflclp_tranclp [simp]: "(r\<^sup>+\<^sup>+)\<^sup>=\<^sup>= = r\<^sup>*\<^sup>*" |
22262 | 537 |
apply (safe intro!: order_antisym) |
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
538 |
apply (erule tranclp_into_rtranclp) |
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
539 |
apply (blast elim: rtranclp.cases dest: rtranclp_into_tranclp1) |
11084 | 540 |
done |
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
541 |
|
50616 | 542 |
lemmas reflcl_trancl [simp] = reflclp_tranclp [to_set] |
22262 | 543 |
|
63404 | 544 |
lemma trancl_reflcl [simp]: "(r\<^sup>=)\<^sup>+ = r\<^sup>*" |
11084 | 545 |
apply safe |
14208 | 546 |
apply (drule trancl_into_rtrancl, simp) |
547 |
apply (erule rtranclE, safe) |
|
548 |
apply (rule r_into_trancl, simp) |
|
11084 | 549 |
apply (rule rtrancl_into_trancl1) |
14208 | 550 |
apply (erule rtrancl_reflcl [THEN equalityD2, THEN subsetD], fast) |
11084 | 551 |
done |
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
552 |
|
63404 | 553 |
lemma rtrancl_trancl_reflcl [code]: "r\<^sup>* = (r\<^sup>+)\<^sup>=" |
45140 | 554 |
by simp |
555 |
||
63404 | 556 |
lemma trancl_empty [simp]: "{}\<^sup>+ = {}" |
11084 | 557 |
by (auto elim: trancl_induct) |
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
558 |
|
63404 | 559 |
lemma rtrancl_empty [simp]: "{}\<^sup>* = Id" |
11084 | 560 |
by (rule subst [OF reflcl_trancl]) simp |
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
561 |
|
63404 | 562 |
lemma rtranclpD: "R\<^sup>*\<^sup>* a b \<Longrightarrow> a = b \<or> a \<noteq> b \<and> R\<^sup>+\<^sup>+ a b" |
563 |
by (force simp add: reflclp_tranclp [symmetric] simp del: reflclp_tranclp) |
|
22262 | 564 |
|
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
565 |
lemmas rtranclD = rtranclpD [to_set] |
11084 | 566 |
|
63404 | 567 |
lemma rtrancl_eq_or_trancl: "(x,y) \<in> R\<^sup>* \<longleftrightarrow> x = y \<or> x \<noteq> y \<and> (x, y) \<in> R\<^sup>+" |
16514 | 568 |
by (fast elim: trancl_into_rtrancl dest: rtranclD) |
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
569 |
|
63404 | 570 |
lemma trancl_unfold_right: "r\<^sup>+ = r\<^sup>* O r" |
571 |
by (auto dest: tranclD2 intro: rtrancl_into_trancl1) |
|
33656
fc1af6753233
a few lemmas for point-free reasoning about transitive closure
krauss
parents:
32901
diff
changeset
|
572 |
|
63404 | 573 |
lemma trancl_unfold_left: "r\<^sup>+ = r O r\<^sup>*" |
574 |
by (auto dest: tranclD intro: rtrancl_into_trancl2) |
|
33656
fc1af6753233
a few lemmas for point-free reasoning about transitive closure
krauss
parents:
32901
diff
changeset
|
575 |
|
63404 | 576 |
lemma trancl_insert: "(insert (y, x) r)\<^sup>+ = r\<^sup>+ \<union> {(a, b). (a, y) \<in> r\<^sup>* \<and> (x, b) \<in> r\<^sup>*}" |
61799 | 577 |
\<comment> \<open>primitive recursion for \<open>trancl\<close> over finite relations\<close> |
57178 | 578 |
apply (rule equalityI) |
579 |
apply (rule subsetI) |
|
580 |
apply (simp only: split_tupled_all) |
|
581 |
apply (erule trancl_induct, blast) |
|
582 |
apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl trancl_trans) |
|
583 |
apply (rule subsetI) |
|
584 |
apply (blast intro: trancl_mono rtrancl_mono |
|
585 |
[THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2) |
|
586 |
done |
|
587 |
||
588 |
lemma trancl_insert2: |
|
63404 | 589 |
"(insert (a, b) r)\<^sup>+ = r\<^sup>+ \<union> {(x, y). ((x, a) \<in> r\<^sup>+ \<or> x = a) \<and> ((b, y) \<in> r\<^sup>+ \<or> y = b)}" |
590 |
by (auto simp add: trancl_insert rtrancl_eq_or_trancl) |
|
57178 | 591 |
|
63404 | 592 |
lemma rtrancl_insert: "(insert (a,b) r)\<^sup>* = r\<^sup>* \<union> {(x, y). (x, a) \<in> r\<^sup>* \<and> (b, y) \<in> r\<^sup>*}" |
593 |
using trancl_insert[of a b r] |
|
594 |
by (simp add: rtrancl_trancl_reflcl del: reflcl_trancl) blast |
|
57178 | 595 |
|
33656
fc1af6753233
a few lemmas for point-free reasoning about transitive closure
krauss
parents:
32901
diff
changeset
|
596 |
|
60758 | 597 |
text \<open>Simplifying nested closures\<close> |
33656
fc1af6753233
a few lemmas for point-free reasoning about transitive closure
krauss
parents:
32901
diff
changeset
|
598 |
|
63404 | 599 |
lemma rtrancl_trancl_absorb[simp]: "(R\<^sup>*)\<^sup>+ = R\<^sup>*" |
600 |
by (simp add: trans_rtrancl) |
|
33656
fc1af6753233
a few lemmas for point-free reasoning about transitive closure
krauss
parents:
32901
diff
changeset
|
601 |
|
63404 | 602 |
lemma trancl_rtrancl_absorb[simp]: "(R\<^sup>+)\<^sup>* = R\<^sup>*" |
603 |
by (subst reflcl_trancl[symmetric]) simp |
|
33656
fc1af6753233
a few lemmas for point-free reasoning about transitive closure
krauss
parents:
32901
diff
changeset
|
604 |
|
63404 | 605 |
lemma rtrancl_reflcl_absorb[simp]: "(R\<^sup>*)\<^sup>= = R\<^sup>*" |
606 |
by auto |
|
33656
fc1af6753233
a few lemmas for point-free reasoning about transitive closure
krauss
parents:
32901
diff
changeset
|
607 |
|
fc1af6753233
a few lemmas for point-free reasoning about transitive closure
krauss
parents:
32901
diff
changeset
|
608 |
|
61799 | 609 |
text \<open>\<open>Domain\<close> and \<open>Range\<close>\<close> |
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
610 |
|
63404 | 611 |
lemma Domain_rtrancl [simp]: "Domain (R\<^sup>*) = UNIV" |
11084 | 612 |
by blast |
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
613 |
|
63404 | 614 |
lemma Range_rtrancl [simp]: "Range (R\<^sup>*) = UNIV" |
11084 | 615 |
by blast |
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
616 |
|
63404 | 617 |
lemma rtrancl_Un_subset: "(R\<^sup>* \<union> S\<^sup>*) \<subseteq> (R \<union> S)\<^sup>*" |
11084 | 618 |
by (rule rtrancl_Un_rtrancl [THEN subst]) fast |
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
619 |
|
63404 | 620 |
lemma in_rtrancl_UnI: "x \<in> R\<^sup>* \<or> x \<in> S\<^sup>* \<Longrightarrow> x \<in> (R \<union> S)\<^sup>*" |
11084 | 621 |
by (blast intro: subsetD [OF rtrancl_Un_subset]) |
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
622 |
|
63404 | 623 |
lemma trancl_domain [simp]: "Domain (r\<^sup>+) = Domain r" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46664
diff
changeset
|
624 |
by (unfold Domain_unfold) (blast dest: tranclD) |
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
625 |
|
63404 | 626 |
lemma trancl_range [simp]: "Range (r\<^sup>+) = Range r" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46664
diff
changeset
|
627 |
unfolding Domain_converse [symmetric] by (simp add: trancl_converse [symmetric]) |
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
628 |
|
63404 | 629 |
lemma Not_Domain_rtrancl: "x \<notin> Domain R \<Longrightarrow> (x, y) \<in> R\<^sup>* \<longleftrightarrow> x = y" |
12691 | 630 |
apply auto |
26179
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
631 |
apply (erule rev_mp) |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
632 |
apply (erule rtrancl_induct) |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
633 |
apply auto |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
634 |
done |
11327
cd2c27a23df1
Transitive closure is now defined via "inductive".
berghofe
parents:
11115
diff
changeset
|
635 |
|
63404 | 636 |
lemma trancl_subset_Field2: "r\<^sup>+ \<subseteq> Field r \<times> Field r" |
29609 | 637 |
apply clarify |
638 |
apply (erule trancl_induct) |
|
639 |
apply (auto simp add: Field_def) |
|
640 |
done |
|
641 |
||
63404 | 642 |
lemma finite_trancl[simp]: "finite (r\<^sup>+) = finite r" |
29609 | 643 |
apply auto |
644 |
prefer 2 |
|
645 |
apply (rule trancl_subset_Field2 [THEN finite_subset]) |
|
646 |
apply (rule finite_SigmaI) |
|
647 |
prefer 3 |
|
648 |
apply (blast intro: r_into_trancl' finite_subset) |
|
649 |
apply (auto simp add: finite_Field) |
|
650 |
done |
|
651 |
||
61799 | 652 |
text \<open>More about converse \<open>rtrancl\<close> and \<open>trancl\<close>, should |
60758 | 653 |
be merged with main body.\<close> |
12428
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset
|
654 |
|
14337
e13731554e50
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
nipkow
parents:
14208
diff
changeset
|
655 |
lemma single_valued_confluent: |
63404 | 656 |
"single_valued r \<Longrightarrow> (x, y) \<in> r\<^sup>* \<Longrightarrow> (x, z) \<in> r\<^sup>* \<Longrightarrow> (y, z) \<in> r\<^sup>* \<or> (z, y) \<in> r\<^sup>*" |
26179
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
657 |
apply (erule rtrancl_induct) |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
658 |
apply simp |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
659 |
apply (erule disjE) |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
660 |
apply (blast elim:converse_rtranclE dest:single_valuedD) |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
661 |
apply(blast intro:rtrancl_trans) |
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
662 |
done |
14337
e13731554e50
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
nipkow
parents:
14208
diff
changeset
|
663 |
|
63404 | 664 |
lemma r_r_into_trancl: "(a, b) \<in> R \<Longrightarrow> (b, c) \<in> R \<Longrightarrow> (a, c) \<in> R\<^sup>+" |
12428
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset
|
665 |
by (fast intro: trancl_trans) |
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset
|
666 |
|
63404 | 667 |
lemma trancl_into_trancl: "(a, b) \<in> r\<^sup>+ \<Longrightarrow> (b, c) \<in> r \<Longrightarrow> (a, c) \<in> r\<^sup>+" |
668 |
apply (induct rule: trancl_induct) |
|
12428
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset
|
669 |
apply (fast intro: r_r_into_trancl) |
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset
|
670 |
apply (fast intro: r_r_into_trancl trancl_trans) |
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset
|
671 |
done |
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset
|
672 |
|
63404 | 673 |
lemma tranclp_rtranclp_tranclp: "r\<^sup>+\<^sup>+ a b \<Longrightarrow> r\<^sup>*\<^sup>* b c \<Longrightarrow> r\<^sup>+\<^sup>+ a c" |
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
674 |
apply (drule tranclpD) |
26179
bc5d582d6cfe
rtranclp_induct, tranclp_induct: added case_names;
wenzelm
parents:
26174
diff
changeset
|
675 |
apply (elim exE conjE) |
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
676 |
apply (drule rtranclp_trans, assumption) |
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
677 |
apply (drule rtranclp_into_tranclp2, assumption, assumption) |
12428
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset
|
678 |
done |
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset
|
679 |
|
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
680 |
lemmas trancl_rtrancl_trancl = tranclp_rtranclp_tranclp [to_set] |
22262 | 681 |
|
12691 | 682 |
lemmas transitive_closure_trans [trans] = |
683 |
r_r_into_trancl trancl_trans rtrancl_trans |
|
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
684 |
trancl.trancl_into_trancl trancl_into_trancl2 |
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
685 |
rtrancl.rtrancl_into_rtrancl converse_rtrancl_into_rtrancl |
12691 | 686 |
rtrancl_trancl_trancl trancl_rtrancl_trancl |
12428
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset
|
687 |
|
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
688 |
lemmas transitive_closurep_trans' [trans] = |
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
689 |
tranclp_trans rtranclp_trans |
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
690 |
tranclp.trancl_into_trancl tranclp_into_tranclp2 |
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
691 |
rtranclp.rtrancl_into_rtrancl converse_rtranclp_into_rtranclp |
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset
|
692 |
rtranclp_tranclp_tranclp tranclp_rtranclp_tranclp |
22262 | 693 |
|
12428
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset
|
694 |
declare trancl_into_rtrancl [elim] |
11327
cd2c27a23df1
Transitive closure is now defined via "inductive".
berghofe
parents:
11115
diff
changeset
|
695 |
|
63404 | 696 |
|
60758 | 697 |
subsection \<open>The power operation on relations\<close> |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
698 |
|
63404 | 699 |
text \<open>\<open>R ^^ n = R O \<dots> O R\<close>, the n-fold composition of \<open>R\<close>\<close> |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
700 |
|
30971 | 701 |
overloading |
63404 | 702 |
relpow \<equiv> "compow :: nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" |
703 |
relpowp \<equiv> "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" |
|
30971 | 704 |
begin |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
705 |
|
63404 | 706 |
primrec relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" |
707 |
where |
|
708 |
"relpow 0 R = Id" |
|
709 |
| "relpow (Suc n) R = (R ^^ n) O R" |
|
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
710 |
|
63404 | 711 |
primrec relpowp :: "nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" |
712 |
where |
|
713 |
"relpowp 0 R = HOL.eq" |
|
714 |
| "relpowp (Suc n) R = (R ^^ n) OO R" |
|
47202 | 715 |
|
30971 | 716 |
end |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
717 |
|
47202 | 718 |
lemma relpowp_relpow_eq [pred_set_conv]: |
63404 | 719 |
"(\<lambda>x y. (x, y) \<in> R) ^^ n = (\<lambda>x y. (x, y) \<in> R ^^ n)" for R :: "'a rel" |
47433
07f4bf913230
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
griff
parents:
47202
diff
changeset
|
720 |
by (induct n) (simp_all add: relcompp_relcomp_eq) |
47202 | 721 |
|
63404 | 722 |
text \<open>For code generation:\<close> |
46360
5cb81e3fa799
adding code generation for relpow by copying the ideas for code generation of funpow
bulwahn
parents:
46347
diff
changeset
|
723 |
|
63404 | 724 |
definition relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" |
725 |
where relpow_code_def [code_abbrev]: "relpow = compow" |
|
46360
5cb81e3fa799
adding code generation for relpow by copying the ideas for code generation of funpow
bulwahn
parents:
46347
diff
changeset
|
726 |
|
63404 | 727 |
definition relpowp :: "nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" |
728 |
where relpowp_code_def [code_abbrev]: "relpowp = compow" |
|
47492
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
729 |
|
46360
5cb81e3fa799
adding code generation for relpow by copying the ideas for code generation of funpow
bulwahn
parents:
46347
diff
changeset
|
730 |
lemma [code]: |
5cb81e3fa799
adding code generation for relpow by copying the ideas for code generation of funpow
bulwahn
parents:
46347
diff
changeset
|
731 |
"relpow (Suc n) R = (relpow n R) O R" |
5cb81e3fa799
adding code generation for relpow by copying the ideas for code generation of funpow
bulwahn
parents:
46347
diff
changeset
|
732 |
"relpow 0 R = Id" |
5cb81e3fa799
adding code generation for relpow by copying the ideas for code generation of funpow
bulwahn
parents:
46347
diff
changeset
|
733 |
by (simp_all add: relpow_code_def) |
5cb81e3fa799
adding code generation for relpow by copying the ideas for code generation of funpow
bulwahn
parents:
46347
diff
changeset
|
734 |
|
47492
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
735 |
lemma [code]: |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
736 |
"relpowp (Suc n) R = (R ^^ n) OO R" |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
737 |
"relpowp 0 R = HOL.eq" |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
738 |
by (simp_all add: relpowp_code_def) |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
739 |
|
46360
5cb81e3fa799
adding code generation for relpow by copying the ideas for code generation of funpow
bulwahn
parents:
46347
diff
changeset
|
740 |
hide_const (open) relpow |
47492
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
741 |
hide_const (open) relpowp |
46360
5cb81e3fa799
adding code generation for relpow by copying the ideas for code generation of funpow
bulwahn
parents:
46347
diff
changeset
|
742 |
|
63404 | 743 |
lemma relpow_1 [simp]: "R ^^ 1 = R" for R :: "('a \<times> 'a) set" |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
744 |
by simp |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
745 |
|
63404 | 746 |
lemma relpowp_1 [simp]: "P ^^ 1 = P" for P :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
47492
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
747 |
by (fact relpow_1 [to_pred]) |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
748 |
|
63404 | 749 |
lemma relpow_0_I: "(x, x) \<in> R ^^ 0" |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
750 |
by simp |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
751 |
|
63404 | 752 |
lemma relpowp_0_I: "(P ^^ 0) x x" |
47492
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
753 |
by (fact relpow_0_I [to_pred]) |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
754 |
|
63404 | 755 |
lemma relpow_Suc_I: "(x, y) \<in> R ^^ n \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> (x, z) \<in> R ^^ Suc n" |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
756 |
by auto |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
757 |
|
63404 | 758 |
lemma relpowp_Suc_I: "(P ^^ n) x y \<Longrightarrow> P y z \<Longrightarrow> (P ^^ Suc n) x z" |
47492
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
759 |
by (fact relpow_Suc_I [to_pred]) |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
760 |
|
63404 | 761 |
lemma relpow_Suc_I2: "(x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ n \<Longrightarrow> (x, z) \<in> R ^^ Suc n" |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
43596
diff
changeset
|
762 |
by (induct n arbitrary: z) (simp, fastforce) |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
763 |
|
63404 | 764 |
lemma relpowp_Suc_I2: "P x y \<Longrightarrow> (P ^^ n) y z \<Longrightarrow> (P ^^ Suc n) x z" |
47492
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
765 |
by (fact relpow_Suc_I2 [to_pred]) |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
766 |
|
63404 | 767 |
lemma relpow_0_E: "(x, y) \<in> R ^^ 0 \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> P" |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
768 |
by simp |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
769 |
|
63404 | 770 |
lemma relpowp_0_E: "(P ^^ 0) x y \<Longrightarrow> (x = y \<Longrightarrow> Q) \<Longrightarrow> Q" |
47492
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
771 |
by (fact relpow_0_E [to_pred]) |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
772 |
|
63404 | 773 |
lemma relpow_Suc_E: "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<And>y. (x, y) \<in> R ^^ n \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P) \<Longrightarrow> P" |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
774 |
by auto |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
775 |
|
63404 | 776 |
lemma relpowp_Suc_E: "(P ^^ Suc n) x z \<Longrightarrow> (\<And>y. (P ^^ n) x y \<Longrightarrow> P y z \<Longrightarrow> Q) \<Longrightarrow> Q" |
47492
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
777 |
by (fact relpow_Suc_E [to_pred]) |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
778 |
|
46362 | 779 |
lemma relpow_E: |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
780 |
"(x, z) \<in> R ^^ n \<Longrightarrow> (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P) |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
781 |
\<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in> R ^^ m \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P) |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
782 |
\<Longrightarrow> P" |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
783 |
by (cases n) auto |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
784 |
|
47492
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
785 |
lemma relpowp_E: |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
786 |
"(P ^^ n) x z \<Longrightarrow> (n = 0 \<Longrightarrow> x = z \<Longrightarrow> Q) |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
787 |
\<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (P ^^ m) x y \<Longrightarrow> P y z \<Longrightarrow> Q) |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
788 |
\<Longrightarrow> Q" |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
789 |
by (fact relpow_E [to_pred]) |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
790 |
|
63404 | 791 |
lemma relpow_Suc_D2: "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<exists>y. (x, y) \<in> R \<and> (y, z) \<in> R ^^ n)" |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
792 |
apply (induct n arbitrary: x z) |
46362 | 793 |
apply (blast intro: relpow_0_I elim: relpow_0_E relpow_Suc_E) |
794 |
apply (blast intro: relpow_Suc_I elim: relpow_0_E relpow_Suc_E) |
|
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
795 |
done |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
796 |
|
63404 | 797 |
lemma relpowp_Suc_D2: "(P ^^ Suc n) x z \<Longrightarrow> \<exists>y. P x y \<and> (P ^^ n) y z" |
47492
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
798 |
by (fact relpow_Suc_D2 [to_pred]) |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
799 |
|
63404 | 800 |
lemma relpow_Suc_E2: "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<And>y. (x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ n \<Longrightarrow> P) \<Longrightarrow> P" |
46362 | 801 |
by (blast dest: relpow_Suc_D2) |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
802 |
|
63404 | 803 |
lemma relpowp_Suc_E2: "(P ^^ Suc n) x z \<Longrightarrow> (\<And>y. P x y \<Longrightarrow> (P ^^ n) y z \<Longrightarrow> Q) \<Longrightarrow> Q" |
47492
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
804 |
by (fact relpow_Suc_E2 [to_pred]) |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
805 |
|
63404 | 806 |
lemma relpow_Suc_D2': "\<forall>x y z. (x, y) \<in> R ^^ n \<and> (y, z) \<in> R \<longrightarrow> (\<exists>w. (x, w) \<in> R \<and> (w, z) \<in> R ^^ n)" |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
807 |
by (induct n) (simp_all, blast) |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
808 |
|
63404 | 809 |
lemma relpowp_Suc_D2': "\<forall>x y z. (P ^^ n) x y \<and> P y z \<longrightarrow> (\<exists>w. P x w \<and> (P ^^ n) w z)" |
47492
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
810 |
by (fact relpow_Suc_D2' [to_pred]) |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
811 |
|
46362 | 812 |
lemma relpow_E2: |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
813 |
"(x, z) \<in> R ^^ n \<Longrightarrow> (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P) |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
814 |
\<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ m \<Longrightarrow> P) |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
815 |
\<Longrightarrow> P" |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
816 |
apply (cases n, simp) |
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
54412
diff
changeset
|
817 |
apply (rename_tac nat) |
46362 | 818 |
apply (cut_tac n=nat and R=R in relpow_Suc_D2', simp, blast) |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
819 |
done |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
820 |
|
47492
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
821 |
lemma relpowp_E2: |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
822 |
"(P ^^ n) x z \<Longrightarrow> (n = 0 \<Longrightarrow> x = z \<Longrightarrow> Q) |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
823 |
\<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> P x y \<Longrightarrow> (P ^^ m) y z \<Longrightarrow> Q) |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
824 |
\<Longrightarrow> Q" |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
825 |
by (fact relpow_E2 [to_pred]) |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
826 |
|
63404 | 827 |
lemma relpow_add: "R ^^ (m + n) = R^^m O R^^n" |
45976 | 828 |
by (induct n) auto |
31351 | 829 |
|
47492
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
830 |
lemma relpowp_add: "P ^^ (m + n) = P ^^ m OO P ^^ n" |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
831 |
by (fact relpow_add [to_pred]) |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
832 |
|
46362 | 833 |
lemma relpow_commute: "R O R ^^ n = R ^^ n O R" |
63404 | 834 |
by (induct n) (simp_all add: O_assoc [symmetric]) |
31970
ccaadfcf6941
move rel_pow_commute: "R O R ^^ n = R ^^ n O R" to Transitive_Closure
krauss
parents:
31690
diff
changeset
|
835 |
|
47492
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
836 |
lemma relpowp_commute: "P OO P ^^ n = P ^^ n OO P" |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
837 |
by (fact relpow_commute [to_pred]) |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
838 |
|
63404 | 839 |
lemma relpow_empty: "0 < n \<Longrightarrow> ({} :: ('a \<times> 'a) set) ^^ n = {}" |
45153 | 840 |
by (cases n) auto |
45116
f947eeef6b6f
adding lemma about rel_pow in Transitive_Closure for executable equation of the (refl) transitive closure
bulwahn
parents:
44921
diff
changeset
|
841 |
|
63404 | 842 |
lemma relpowp_bot: "0 < n \<Longrightarrow> (\<bottom> :: 'a \<Rightarrow> 'a \<Rightarrow> bool) ^^ n = \<bottom>" |
47492
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
843 |
by (fact relpow_empty [to_pred]) |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
844 |
|
46362 | 845 |
lemma rtrancl_imp_UN_relpow: |
63404 | 846 |
assumes "p \<in> R\<^sup>*" |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
847 |
shows "p \<in> (\<Union>n. R ^^ n)" |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
848 |
proof (cases p) |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
849 |
case (Pair x y) |
63404 | 850 |
with assms have "(x, y) \<in> R\<^sup>*" by simp |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
851 |
then have "(x, y) \<in> (\<Union>n. R ^^ n)" proof induct |
63404 | 852 |
case base |
853 |
show ?case by (blast intro: relpow_0_I) |
|
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
854 |
next |
63404 | 855 |
case step |
856 |
then show ?case by (blast intro: relpow_Suc_I) |
|
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
857 |
qed |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
858 |
with Pair show ?thesis by simp |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
859 |
qed |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
860 |
|
47492
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
861 |
lemma rtranclp_imp_Sup_relpowp: |
63404 | 862 |
assumes "(P\<^sup>*\<^sup>*) x y" |
47492
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
863 |
shows "(\<Squnion>n. P ^^ n) x y" |
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61378
diff
changeset
|
864 |
using assms and rtrancl_imp_UN_relpow [of "(x, y)", to_pred] by simp |
47492
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
865 |
|
46362 | 866 |
lemma relpow_imp_rtrancl: |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
867 |
assumes "p \<in> R ^^ n" |
63404 | 868 |
shows "p \<in> R\<^sup>*" |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
869 |
proof (cases p) |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
870 |
case (Pair x y) |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
871 |
with assms have "(x, y) \<in> R ^^ n" by simp |
63404 | 872 |
then have "(x, y) \<in> R\<^sup>*" proof (induct n arbitrary: x y) |
873 |
case 0 |
|
874 |
then show ?case by simp |
|
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
875 |
next |
63404 | 876 |
case Suc |
877 |
then show ?case |
|
46362 | 878 |
by (blast elim: relpow_Suc_E intro: rtrancl_into_rtrancl) |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
879 |
qed |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
880 |
with Pair show ?thesis by simp |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
881 |
qed |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
882 |
|
63404 | 883 |
lemma relpowp_imp_rtranclp: "(P ^^ n) x y \<Longrightarrow> (P\<^sup>*\<^sup>*) x y" |
884 |
using relpow_imp_rtrancl [of "(x, y)", to_pred] by simp |
|
47492
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
885 |
|
63404 | 886 |
lemma rtrancl_is_UN_relpow: "R\<^sup>* = (\<Union>n. R ^^ n)" |
46362 | 887 |
by (blast intro: rtrancl_imp_UN_relpow relpow_imp_rtrancl) |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
888 |
|
63404 | 889 |
lemma rtranclp_is_Sup_relpowp: "P\<^sup>*\<^sup>* = (\<Squnion>n. P ^^ n)" |
47492
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
890 |
using rtrancl_is_UN_relpow [to_pred, of P] by auto |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
891 |
|
63404 | 892 |
lemma rtrancl_power: "p \<in> R\<^sup>* \<longleftrightarrow> (\<exists>n. p \<in> R ^^ n)" |
46362 | 893 |
by (simp add: rtrancl_is_UN_relpow) |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
894 |
|
63404 | 895 |
lemma rtranclp_power: "(P\<^sup>*\<^sup>*) x y \<longleftrightarrow> (\<exists>n. (P ^^ n) x y)" |
47492
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
896 |
by (simp add: rtranclp_is_Sup_relpowp) |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
897 |
|
63404 | 898 |
lemma trancl_power: "p \<in> R\<^sup>+ \<longleftrightarrow> (\<exists>n > 0. p \<in> R ^^ n)" |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
899 |
apply (cases p) |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
900 |
apply simp |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
901 |
apply (rule iffI) |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
902 |
apply (drule tranclD2) |
46362 | 903 |
apply (clarsimp simp: rtrancl_is_UN_relpow) |
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62093
diff
changeset
|
904 |
apply (rule_tac x="Suc x" in exI) |
47433
07f4bf913230
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
griff
parents:
47202
diff
changeset
|
905 |
apply (clarsimp simp: relcomp_unfold) |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
43596
diff
changeset
|
906 |
apply fastforce |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
907 |
apply clarsimp |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
908 |
apply (case_tac n, simp) |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
909 |
apply clarsimp |
46362 | 910 |
apply (drule relpow_imp_rtrancl) |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
911 |
apply (drule rtrancl_into_trancl1) apply auto |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
912 |
done |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
913 |
|
63404 | 914 |
lemma tranclp_power: "(P\<^sup>+\<^sup>+) x y \<longleftrightarrow> (\<exists>n > 0. (P ^^ n) x y)" |
47492
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
915 |
using trancl_power [to_pred, of P "(x, y)"] by simp |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
916 |
|
63404 | 917 |
lemma rtrancl_imp_relpow: "p \<in> R\<^sup>* \<Longrightarrow> \<exists>n. p \<in> R ^^ n" |
46362 | 918 |
by (auto dest: rtrancl_imp_UN_relpow) |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
919 |
|
63404 | 920 |
lemma rtranclp_imp_relpowp: "(P\<^sup>*\<^sup>*) x y \<Longrightarrow> \<exists>n. (P ^^ n) x y" |
47492
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
921 |
by (auto dest: rtranclp_imp_Sup_relpowp) |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
922 |
|
63404 | 923 |
text \<open>By Sternagel/Thiemann:\<close> |
924 |
lemma relpow_fun_conv: "(a, b) \<in> R ^^ n \<longleftrightarrow> (\<exists>f. f 0 = a \<and> f n = b \<and> (\<forall>i<n. (f i, f (Suc i)) \<in> R))" |
|
41987 | 925 |
proof (induct n arbitrary: b) |
63404 | 926 |
case 0 |
927 |
show ?case by auto |
|
41987 | 928 |
next |
929 |
case (Suc n) |
|
930 |
show ?case |
|
47433
07f4bf913230
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
griff
parents:
47202
diff
changeset
|
931 |
proof (simp add: relcomp_unfold Suc) |
63404 | 932 |
show "(\<exists>y. (\<exists>f. f 0 = a \<and> f n = y \<and> (\<forall>i<n. (f i,f(Suc i)) \<in> R)) \<and> (y,b) \<in> R) \<longleftrightarrow> |
933 |
(\<exists>f. f 0 = a \<and> f(Suc n) = b \<and> (\<forall>i<Suc n. (f i, f (Suc i)) \<in> R))" |
|
41987 | 934 |
(is "?l = ?r") |
935 |
proof |
|
936 |
assume ?l |
|
63404 | 937 |
then obtain c f |
938 |
where 1: "f 0 = a" "f n = c" "\<And>i. i < n \<Longrightarrow> (f i, f (Suc i)) \<in> R" "(c,b) \<in> R" |
|
939 |
by auto |
|
41987 | 940 |
let ?g = "\<lambda> m. if m = Suc n then b else f m" |
63404 | 941 |
show ?r by (rule exI[of _ ?g]) (simp add: 1) |
41987 | 942 |
next |
943 |
assume ?r |
|
63404 | 944 |
then obtain f where 1: "f 0 = a" "b = f (Suc n)" "\<And>i. i < Suc n \<Longrightarrow> (f i, f (Suc i)) \<in> R" |
945 |
by auto |
|
41987 | 946 |
show ?l by (rule exI[of _ "f n"], rule conjI, rule exI[of _ f], insert 1, auto) |
947 |
qed |
|
948 |
qed |
|
949 |
qed |
|
950 |
||
63404 | 951 |
lemma relpowp_fun_conv: "(P ^^ n) x y \<longleftrightarrow> (\<exists>f. f 0 = x \<and> f n = y \<and> (\<forall>i<n. P (f i) (f (Suc i))))" |
47492
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
952 |
by (fact relpow_fun_conv [to_pred]) |
2631a12fb2d1
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Christian Sternagel
parents:
47433
diff
changeset
|
953 |
|
46362 | 954 |
lemma relpow_finite_bounded1: |
63404 | 955 |
fixes R :: "('a \<times> 'a) set" |
956 |
assumes "finite R" and "k > 0" |
|
957 |
shows "R^^k \<subseteq> (\<Union>n\<in>{n. 0 < n \<and> n \<le> card R}. R^^n)" (is "_ \<subseteq> ?r") |
|
958 |
proof - |
|
959 |
have "(a, b) \<in> R^^(Suc k) \<Longrightarrow> \<exists>n. 0 < n \<and> n \<le> card R \<and> (a, b) \<in> R^^n" for a b k |
|
960 |
proof (induct k arbitrary: b) |
|
961 |
case 0 |
|
962 |
then have "R \<noteq> {}" by auto |
|
963 |
with card_0_eq[OF \<open>finite R\<close>] have "card R \<ge> Suc 0" by auto |
|
964 |
then show ?case using 0 by force |
|
965 |
next |
|
966 |
case (Suc k) |
|
967 |
then obtain a' where "(a, a') \<in> R^^(Suc k)" and "(a', b) \<in> R" |
|
968 |
by auto |
|
969 |
from Suc(1)[OF \<open>(a, a') \<in> R^^(Suc k)\<close>] obtain n where "n \<le> card R" and "(a, a') \<in> R ^^ n" |
|
970 |
by auto |
|
971 |
have "(a, b) \<in> R^^(Suc n)" |
|
972 |
using \<open>(a, a') \<in> R^^n\<close> and \<open>(a', b)\<in> R\<close> by auto |
|
973 |
from \<open>n \<le> card R\<close> consider "n < card R" | "n = card R" by force |
|
974 |
then show ?case |
|
975 |
proof cases |
|
976 |
case 1 |
|
977 |
then show ?thesis |
|
978 |
using \<open>(a, b) \<in> R^^(Suc n)\<close> Suc_leI[OF \<open>n < card R\<close>] by blast |
|
41987 | 979 |
next |
63404 | 980 |
case 2 |
981 |
from \<open>(a, b) \<in> R ^^ (Suc n)\<close> [unfolded relpow_fun_conv] |
|
982 |
obtain f where "f 0 = a" and "f (Suc n) = b" |
|
983 |
and steps: "\<And>i. i \<le> n \<Longrightarrow> (f i, f (Suc i)) \<in> R" by auto |
|
984 |
let ?p = "\<lambda>i. (f i, f(Suc i))" |
|
985 |
let ?N = "{i. i \<le> n}" |
|
986 |
have "?p ` ?N \<subseteq> R" |
|
987 |
using steps by auto |
|
988 |
from card_mono[OF assms(1) this] have "card (?p ` ?N) \<le> card R" . |
|
989 |
also have "\<dots> < card ?N" |
|
990 |
using \<open>n = card R\<close> by simp |
|
991 |
finally have "\<not> inj_on ?p ?N" |
|
992 |
by (rule pigeonhole) |
|
993 |
then obtain i j where i: "i \<le> n" and j: "j \<le> n" and ij: "i \<noteq> j" and pij: "?p i = ?p j" |
|
994 |
by (auto simp: inj_on_def) |
|
995 |
let ?i = "min i j" |
|
996 |
let ?j = "max i j" |
|
997 |
have i: "?i \<le> n" and j: "?j \<le> n" and pij: "?p ?i = ?p ?j" and ij: "?i < ?j" |
|
998 |
using i j ij pij unfolding min_def max_def by auto |
|
999 |
from i j pij ij obtain i j where i: "i \<le> n" and j: "j \<le> n" and ij: "i < j" |
|
1000 |
and pij: "?p i = ?p j" |
|
1001 |
by blast |
|
1002 |
let ?g = "\<lambda>l. if l \<le> i then f l else f (l + (j - i))" |
|
1003 |
let ?n = "Suc (n - (j - i))" |
|
1004 |
have abl: "(a, b) \<in> R ^^ ?n" |
|
1005 |
unfolding relpow_fun_conv |
|
1006 |
proof (rule exI[of _ ?g], intro conjI impI allI) |
|
1007 |
show "?g ?n = b" |
|
1008 |
using \<open>f(Suc n) = b\<close> j ij by auto |
|
1009 |
next |
|
1010 |
fix k |
|
1011 |
assume "k < ?n" |
|
1012 |
show "(?g k, ?g (Suc k)) \<in> R" |
|
1013 |
proof (cases "k < i") |
|
1014 |
case True |
|
1015 |
with i have "k \<le> n" |
|
1016 |
by auto |
|
1017 |
from steps[OF this] show ?thesis |
|
1018 |
using True by simp |
|
41987 | 1019 |
next |
63404 | 1020 |
case False |
1021 |
then have "i \<le> k" by auto |
|
1022 |
show ?thesis |
|
1023 |
proof (cases "k = i") |
|
41987 | 1024 |
case True |
63404 | 1025 |
then show ?thesis |
1026 |
using ij pij steps[OF i] by simp |
|
41987 | 1027 |
next |
1028 |
case False |
|
63404 | 1029 |
with \<open>i \<le> k\<close> have "i < k" by auto |
1030 |
then have small: "k + (j - i) \<le> n" |
|
1031 |
using \<open>k<?n\<close> by arith |
|
41987 | 1032 |
show ?thesis |
63404 | 1033 |
using steps[OF small] \<open>i<k\<close> by auto |
41987 | 1034 |
qed |
63404 | 1035 |
qed |
1036 |
qed (simp add: \<open>f 0 = a\<close>) |
|
1037 |
moreover have "?n \<le> n" |
|
1038 |
using i j ij by arith |
|
1039 |
ultimately show ?thesis |
|
1040 |
using \<open>n = card R\<close> by blast |
|
41987 | 1041 |
qed |
63404 | 1042 |
qed |
1043 |
then show ?thesis |
|
1044 |
using gr0_implies_Suc[OF \<open>k > 0\<close>] by auto |
|
41987 | 1045 |
qed |
1046 |
||
46362 | 1047 |
lemma relpow_finite_bounded: |
63404 | 1048 |
fixes R :: "('a \<times> 'a) set" |
1049 |
assumes "finite R" |
|
1050 |
shows "R^^k \<subseteq> (UN n:{n. n \<le> card R}. R^^n)" |
|
1051 |
apply (cases k) |
|
1052 |
apply force |
|
1053 |
using relpow_finite_bounded1[OF assms, of k] |
|
1054 |
apply auto |
|
1055 |
done |
|
41987 | 1056 |
|
63404 | 1057 |
lemma rtrancl_finite_eq_relpow: "finite R \<Longrightarrow> R\<^sup>* = (\<Union>n\<in>{n. n \<le> card R}. R^^n)" |
1058 |
by (fastforce simp: rtrancl_power dest: relpow_finite_bounded) |
|
41987 | 1059 |
|
63404 | 1060 |
lemma trancl_finite_eq_relpow: "finite R \<Longrightarrow> R\<^sup>+ = (\<Union>n\<in>{n. 0 < n \<and> n \<le> card R}. R^^n)" |
1061 |
apply (auto simp: trancl_power) |
|
1062 |
apply (auto dest: relpow_finite_bounded1) |
|
1063 |
done |
|
41987 | 1064 |
|
47433
07f4bf913230
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
griff
parents:
47202
diff
changeset
|
1065 |
lemma finite_relcomp[simp,intro]: |
63404 | 1066 |
assumes "finite R" and "finite S" |
1067 |
shows "finite (R O S)" |
|
41987 | 1068 |
proof- |
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62093
diff
changeset
|
1069 |
have "R O S = (\<Union>(x, y)\<in>R. \<Union>(u, v)\<in>S. if u = y then {(x, v)} else {})" |
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62093
diff
changeset
|
1070 |
by (force simp add: split_def image_constant_conv split: if_splits) |
63404 | 1071 |
then show ?thesis |
1072 |
using assms by clarsimp |
|
41987 | 1073 |
qed |
1074 |
||
63404 | 1075 |
lemma finite_relpow [simp, intro]: |
1076 |
fixes R :: "('a \<times> 'a) set" |
|
1077 |
assumes "finite R" |
|
1078 |
shows "n > 0 \<Longrightarrow> finite (R^^n)" |
|
1079 |
apply (induct n) |
|
1080 |
apply simp |
|
1081 |
apply (case_tac n) |
|
1082 |
apply (simp_all add: assms) |
|
1083 |
done |
|
41987 | 1084 |
|
46362 | 1085 |
lemma single_valued_relpow: |
63404 | 1086 |
fixes R :: "('a \<times> 'a) set" |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30549
diff
changeset
|
1087 |
shows "single_valued R \<Longrightarrow> single_valued (R ^^ n)" |
63404 | 1088 |
apply (induct n arbitrary: R) |
1089 |
apply simp_all |
|
1090 |
apply (rule single_valuedI) |
|
1091 |
apply (fast dest: single_valuedD elim: relpow_Suc_E) |
|
1092 |
done |
|
15551 | 1093 |
|
45140 | 1094 |
|
60758 | 1095 |
subsection \<open>Bounded transitive closure\<close> |
45140 | 1096 |
|
1097 |
definition ntrancl :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" |
|
63404 | 1098 |
where "ntrancl n R = (\<Union>i\<in>{i. 0 < i \<and> i \<le> Suc n}. R ^^ i)" |
45140 | 1099 |
|
63404 | 1100 |
lemma ntrancl_Zero [simp, code]: "ntrancl 0 R = R" |
45140 | 1101 |
proof |
1102 |
show "R \<subseteq> ntrancl 0 R" |
|
1103 |
unfolding ntrancl_def by fastforce |
|
1104 |
next |
|
63404 | 1105 |
have "0 < i \<and> i \<le> Suc 0 \<longleftrightarrow> i = 1" for i |
1106 |
by auto |
|
1107 |
then show "ntrancl 0 R \<le> R" |
|
45140 | 1108 |
unfolding ntrancl_def by auto |
1109 |
qed |
|
1110 |
||
63404 | 1111 |
lemma ntrancl_Suc [simp]: "ntrancl (Suc n) R = ntrancl n R O (Id \<union> R)" |
45140 | 1112 |
proof |
1113 |
{ |
|
1114 |
fix a b |
|
1115 |
assume "(a, b) \<in> ntrancl (Suc n) R" |
|
1116 |
from this obtain i where "0 < i" "i \<le> Suc (Suc n)" "(a, b) \<in> R ^^ i" |
|
1117 |
unfolding ntrancl_def by auto |
|
1118 |
have "(a, b) \<in> ntrancl n R O (Id \<union> R)" |
|
1119 |
proof (cases "i = 1") |
|
1120 |
case True |
|
60758 | 1121 |
from this \<open>(a, b) \<in> R ^^ i\<close> show ?thesis |
45140 | 1122 |
unfolding ntrancl_def by auto |
1123 |
next |
|
1124 |
case False |
|
60758 | 1125 |
from this \<open>0 < i\<close> obtain j where j: "i = Suc j" "0 < j" |
45140 | 1126 |
by (cases i) auto |
60758 | 1127 |
from this \<open>(a, b) \<in> R ^^ i\<close> obtain c where c1: "(a, c) \<in> R ^^ j" and c2:"(c, b) \<in> R" |
45140 | 1128 |
by auto |
60758 | 1129 |
from c1 j \<open>i \<le> Suc (Suc n)\<close> have "(a, c) \<in> ntrancl n R" |
45140 | 1130 |
unfolding ntrancl_def by fastforce |
1131 |
from this c2 show ?thesis by fastforce |
|
1132 |
qed |
|
1133 |
} |
|
63404 | 1134 |
then show "ntrancl (Suc n) R \<subseteq> ntrancl n R O (Id \<union> R)" |
45140 | 1135 |
by auto |
1136 |
show "ntrancl n R O (Id \<union> R) \<subseteq> ntrancl (Suc n) R" |
|
1137 |
unfolding ntrancl_def by fastforce |
|
1138 |
qed |
|
1139 |
||
63404 | 1140 |
lemma [code]: "ntrancl (Suc n) r = (let r' = ntrancl n r in r' \<union> r' O r)" |
1141 |
by (auto simp: Let_def) |
|
46347
54870ad19af4
new code equation for ntrancl that allows computation of the transitive closure of sets on infinite types as well
bulwahn
parents:
46127
diff
changeset
|
1142 |
|
63404 | 1143 |
lemma finite_trancl_ntranl: "finite R \<Longrightarrow> trancl R = ntrancl (card R - 1) R" |
46362 | 1144 |
by (cases "card R") (auto simp add: trancl_finite_eq_relpow relpow_empty ntrancl_def) |
45140 | 1145 |
|
1146 |
||
60758 | 1147 |
subsection \<open>Acyclic relations\<close> |
45139 | 1148 |
|
63404 | 1149 |
definition acyclic :: "('a \<times> 'a) set \<Rightarrow> bool" |
1150 |
where "acyclic r \<longleftrightarrow> (\<forall>x. (x,x) \<notin> r\<^sup>+)" |
|
45139 | 1151 |
|
63404 | 1152 |
abbreviation acyclicP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" |
1153 |
where "acyclicP r \<equiv> acyclic {(x, y). r x y}" |
|
45139 | 1154 |
|
63404 | 1155 |
lemma acyclic_irrefl [code]: "acyclic r \<longleftrightarrow> irrefl (r\<^sup>+)" |
45139 | 1156 |
by (simp add: acyclic_def irrefl_def) |
1157 |
||
63404 | 1158 |
lemma acyclicI: "\<forall>x. (x, x) \<notin> r\<^sup>+ \<Longrightarrow> acyclic r" |
45139 | 1159 |
by (simp add: acyclic_def) |
1160 |
||
54412 | 1161 |
lemma (in order) acyclicI_order: |
1162 |
assumes *: "\<And>a b. (a, b) \<in> r \<Longrightarrow> f b < f a" |
|
1163 |
shows "acyclic r" |
|
1164 |
proof - |
|
63404 | 1165 |
have "f b < f a" if "(a, b) \<in> r\<^sup>+" for a b |
1166 |
using that by induct (auto intro: * less_trans) |
|
54412 | 1167 |
then show ?thesis |
1168 |
by (auto intro!: acyclicI) |
|
1169 |
qed |
|
1170 |
||
63404 | 1171 |
lemma acyclic_insert [iff]: "acyclic (insert (y, x) r) \<longleftrightarrow> acyclic r \<and> (x, y) \<notin> r\<^sup>*" |
1172 |
apply (simp add: acyclic_def trancl_insert) |
|
1173 |
apply (blast intro: rtrancl_trans) |
|
1174 |
done |
|
45139 | 1175 |
|
63404 | 1176 |
lemma acyclic_converse [iff]: "acyclic (r\<inverse>) \<longleftrightarrow> acyclic r" |
1177 |
by (simp add: acyclic_def trancl_converse) |
|
45139 | 1178 |
|
1179 |
lemmas acyclicP_converse [iff] = acyclic_converse [to_pred] |
|
1180 |
||
63404 | 1181 |
lemma acyclic_impl_antisym_rtrancl: "acyclic r \<Longrightarrow> antisym (r\<^sup>*)" |
1182 |
apply (simp add: acyclic_def antisym_def) |
|
1183 |
apply (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl) |
|
1184 |
done |
|
45139 | 1185 |
|
1186 |
(* Other direction: |
|
1187 |
acyclic = no loops |
|
1188 |
antisym = only self loops |
|
63404 | 1189 |
Goalw [acyclic_def,antisym_def] "antisym( r\<^sup>* ) \<Longrightarrow> acyclic(r - Id) |
1190 |
\<Longrightarrow> antisym( r\<^sup>* ) = acyclic(r - Id)"; |
|
45139 | 1191 |
*) |
1192 |
||
63404 | 1193 |
lemma acyclic_subset: "acyclic s \<Longrightarrow> r \<subseteq> s \<Longrightarrow> acyclic r" |
1194 |
unfolding acyclic_def by (blast intro: trancl_mono) |
|
45139 | 1195 |
|
1196 |
||
60758 | 1197 |
subsection \<open>Setup of transitivity reasoner\<close> |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
14565
diff
changeset
|
1198 |
|
60758 | 1199 |
ML \<open> |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
14565
diff
changeset
|
1200 |
|
32215 | 1201 |
structure Trancl_Tac = Trancl_Tac |
1202 |
( |
|
1203 |
val r_into_trancl = @{thm trancl.r_into_trancl}; |
|
1204 |
val trancl_trans = @{thm trancl_trans}; |
|
1205 |
val rtrancl_refl = @{thm rtrancl.rtrancl_refl}; |
|
1206 |
val r_into_rtrancl = @{thm r_into_rtrancl}; |
|
1207 |
val trancl_into_rtrancl = @{thm trancl_into_rtrancl}; |
|
1208 |
val rtrancl_trancl_trancl = @{thm rtrancl_trancl_trancl}; |
|
1209 |
val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl}; |
|
1210 |
val rtrancl_trans = @{thm rtrancl_trans}; |
|
15096 | 1211 |
|
30107
f3b3b0e3d184
Fixed nonexhaustive match problem in decomp, to make it fail more gracefully
berghofe
parents:
29609
diff
changeset
|
1212 |
fun decomp (@{const Trueprop} $ t) = |
63404 | 1213 |
let |
1214 |
fun dec (Const (@{const_name Set.member}, _) $ (Const (@{const_name Pair}, _) $ a $ b) $ rel) = |
|
1215 |
let |
|
1216 |
fun decr (Const (@{const_name rtrancl}, _ ) $ r) = (r,"r*") |
|
1217 |
| decr (Const (@{const_name trancl}, _ ) $ r) = (r,"r+") |
|
1218 |
| decr r = (r,"r"); |
|
1219 |
val (rel,r) = decr (Envir.beta_eta_contract rel); |
|
1220 |
in SOME (a,b,rel,r) end |
|
1221 |
| dec _ = NONE |
|
1222 |
in dec t end |
|
30107
f3b3b0e3d184
Fixed nonexhaustive match problem in decomp, to make it fail more gracefully
berghofe
parents:
29609
diff
changeset
|
1223 |
| decomp _ = NONE; |
32215 | 1224 |
); |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
14565
diff
changeset
|
1225 |
|
32215 | 1226 |
structure Tranclp_Tac = Trancl_Tac |
1227 |
( |
|
1228 |
val r_into_trancl = @{thm tranclp.r_into_trancl}; |
|
1229 |
val trancl_trans = @{thm tranclp_trans}; |
|
1230 |
val rtrancl_refl = @{thm rtranclp.rtrancl_refl}; |
|
1231 |
val r_into_rtrancl = @{thm r_into_rtranclp}; |
|
1232 |
val trancl_into_rtrancl = @{thm tranclp_into_rtranclp}; |
|
1233 |
val rtrancl_trancl_trancl = @{thm rtranclp_tranclp_tranclp}; |
|
1234 |
val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp}; |
|
1235 |
val rtrancl_trans = @{thm rtranclp_trans}; |
|
22262 | 1236 |
|
30107
f3b3b0e3d184
Fixed nonexhaustive match problem in decomp, to make it fail more gracefully
berghofe
parents:
29609
diff
changeset
|
1237 |
fun decomp (@{const Trueprop} $ t) = |
63404 | 1238 |
let |
1239 |
fun dec (rel $ a $ b) = |
|
1240 |
let |
|
1241 |
fun decr (Const (@{const_name rtranclp}, _ ) $ r) = (r,"r*") |
|
1242 |
| decr (Const (@{const_name tranclp}, _ ) $ r) = (r,"r+") |
|
1243 |
| decr r = (r,"r"); |
|
1244 |
val (rel,r) = decr rel; |
|
1245 |
in SOME (a, b, rel, r) end |
|
1246 |
| dec _ = NONE |
|
1247 |
in dec t end |
|
30107
f3b3b0e3d184
Fixed nonexhaustive match problem in decomp, to make it fail more gracefully
berghofe
parents:
29609
diff
changeset
|
1248 |
| decomp _ = NONE; |
32215 | 1249 |
); |
60758 | 1250 |
\<close> |
22262 | 1251 |
|
60758 | 1252 |
setup \<open> |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50616
diff
changeset
|
1253 |
map_theory_simpset (fn ctxt => ctxt |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50616
diff
changeset
|
1254 |
addSolver (mk_solver "Trancl" Trancl_Tac.trancl_tac) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50616
diff
changeset
|
1255 |
addSolver (mk_solver "Rtrancl" Trancl_Tac.rtrancl_tac) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50616
diff
changeset
|
1256 |
addSolver (mk_solver "Tranclp" Tranclp_Tac.trancl_tac) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50616
diff
changeset
|
1257 |
addSolver (mk_solver "Rtranclp" Tranclp_Tac.rtrancl_tac)) |
60758 | 1258 |
\<close> |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
14565
diff
changeset
|
1259 |
|
32215 | 1260 |
|
60758 | 1261 |
text \<open>Optional methods.\<close> |
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
14565
diff
changeset
|
1262 |
|
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
14565
diff
changeset
|
1263 |
method_setup trancl = |
60758 | 1264 |
\<open>Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.trancl_tac)\<close> |
1265 |
\<open>simple transitivity reasoner\<close> |
|
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
14565
diff
changeset
|
1266 |
method_setup rtrancl = |
60758 | 1267 |
\<open>Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.rtrancl_tac)\<close> |
1268 |
\<open>simple transitivity reasoner\<close> |
|
22262 | 1269 |
method_setup tranclp = |
60758 | 1270 |
\<open>Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.trancl_tac)\<close> |
1271 |
\<open>simple transitivity reasoner (predicate version)\<close> |
|
22262 | 1272 |
method_setup rtranclp = |
60758 | 1273 |
\<open>Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.rtrancl_tac)\<close> |
1274 |
\<open>simple transitivity reasoner (predicate version)\<close> |
|
15076
4b3d280ef06a
New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
14565
diff
changeset
|
1275 |
|
10213 | 1276 |
end |