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