10 for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
10 for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
11 where |
11 where |
12 base: "rtrancl_path r x [] x" |
12 base: "rtrancl_path r x [] x" |
13 | step: "r x y \<Longrightarrow> rtrancl_path r y ys z \<Longrightarrow> rtrancl_path r x (y # ys) z" |
13 | step: "r x y \<Longrightarrow> rtrancl_path r y ys z \<Longrightarrow> rtrancl_path r x (y # ys) z" |
14 |
14 |
15 lemma rtranclp_eq_rtrancl_path: "r\<^sup>*\<^sup>* x y = (\<exists>xs. rtrancl_path r x xs y)" |
15 lemma rtranclp_eq_rtrancl_path: "r\<^sup>*\<^sup>* x y \<longleftrightarrow> (\<exists>xs. rtrancl_path r x xs y)" |
16 proof |
16 proof |
17 assume "r\<^sup>*\<^sup>* x y" |
17 show "\<exists>xs. rtrancl_path r x xs y" if "r\<^sup>*\<^sup>* x y" |
18 then show "\<exists>xs. rtrancl_path r x xs y" |
18 using that |
19 proof (induct rule: converse_rtranclp_induct) |
19 proof (induct rule: converse_rtranclp_induct) |
20 case base |
20 case base |
21 have "rtrancl_path r y [] y" by (rule rtrancl_path.base) |
21 have "rtrancl_path r y [] y" by (rule rtrancl_path.base) |
22 then show ?case .. |
22 then show ?case .. |
23 next |
23 next |
26 obtain xs where "rtrancl_path r z xs y" .. |
26 obtain xs where "rtrancl_path r z xs y" .. |
27 with \<open>r x z\<close> have "rtrancl_path r x (z # xs) y" |
27 with \<open>r x z\<close> have "rtrancl_path r x (z # xs) y" |
28 by (rule rtrancl_path.step) |
28 by (rule rtrancl_path.step) |
29 then show ?case .. |
29 then show ?case .. |
30 qed |
30 qed |
31 next |
31 show "r\<^sup>*\<^sup>* x y" if "\<exists>xs. rtrancl_path r x xs y" |
32 assume "\<exists>xs. rtrancl_path r x xs y" |
32 proof - |
33 then obtain xs where "rtrancl_path r x xs y" .. |
33 from that obtain xs where "rtrancl_path r x xs y" .. |
34 then show "r\<^sup>*\<^sup>* x y" |
34 then show ?thesis |
35 proof induct |
35 proof induct |
36 case (base x) |
36 case (base x) |
37 show ?case by (rule rtranclp.rtrancl_refl) |
37 show ?case |
38 next |
38 by (rule rtranclp.rtrancl_refl) |
39 case (step x y ys z) |
39 next |
40 from \<open>r x y\<close> \<open>r\<^sup>*\<^sup>* y z\<close> show ?case |
40 case (step x y ys z) |
41 by (rule converse_rtranclp_into_rtranclp) |
41 from \<open>r x y\<close> \<open>r\<^sup>*\<^sup>* y z\<close> show ?case |
|
42 by (rule converse_rtranclp_into_rtranclp) |
|
43 qed |
42 qed |
44 qed |
43 qed |
45 qed |
44 |
46 |
45 lemma rtrancl_path_trans: |
47 lemma rtrancl_path_trans: |
46 assumes xy: "rtrancl_path r x xs y" |
48 assumes xy: "rtrancl_path r x xs y" |
47 and yz: "rtrancl_path r y ys z" |
49 and yz: "rtrancl_path r y ys z" |
48 shows "rtrancl_path r x (xs @ ys) z" using xy yz |
50 shows "rtrancl_path r x (xs @ ys) z" using xy yz |
49 proof (induct arbitrary: z) |
51 proof (induct arbitrary: z) |
50 case (base x) |
52 case (base x) |
51 then show ?case by simp |
53 then show ?case by simp |
52 next |
54 next |
58 then show ?case by simp |
60 then show ?case by simp |
59 qed |
61 qed |
60 |
62 |
61 lemma rtrancl_path_appendE: |
63 lemma rtrancl_path_appendE: |
62 assumes xz: "rtrancl_path r x (xs @ y # ys) z" |
64 assumes xz: "rtrancl_path r x (xs @ y # ys) z" |
63 obtains "rtrancl_path r x (xs @ [y]) y" and "rtrancl_path r y ys z" using xz |
65 obtains "rtrancl_path r x (xs @ [y]) y" and "rtrancl_path r y ys z" |
|
66 using xz |
64 proof (induct xs arbitrary: x) |
67 proof (induct xs arbitrary: x) |
65 case Nil |
68 case Nil |
66 then have "rtrancl_path r x (y # ys) z" by simp |
69 then have "rtrancl_path r x (y # ys) z" by simp |
67 then obtain xy: "r x y" and yz: "rtrancl_path r y ys z" |
70 then obtain xy: "r x y" and yz: "rtrancl_path r y ys z" |
68 by cases auto |
71 by cases auto |
69 from xy have "rtrancl_path r x [y] y" |
72 from xy have "rtrancl_path r x [y] y" |
70 by (rule rtrancl_path.step [OF _ rtrancl_path.base]) |
73 by (rule rtrancl_path.step [OF _ rtrancl_path.base]) |
71 then have "rtrancl_path r x ([] @ [y]) y" by simp |
74 then have "rtrancl_path r x ([] @ [y]) y" by simp |
72 then show ?thesis using yz by (rule Nil) |
75 then show thesis using yz by (rule Nil) |
73 next |
76 next |
74 case (Cons a as) |
77 case (Cons a as) |
75 then have "rtrancl_path r x (a # (as @ y # ys)) z" by simp |
78 then have "rtrancl_path r x (a # (as @ y # ys)) z" by simp |
76 then obtain xa: "r x a" and az: "rtrancl_path r a (as @ y # ys) z" |
79 then obtain xa: "r x a" and az: "rtrancl_path r a (as @ y # ys) z" |
77 by cases auto |
80 by cases auto |
78 show ?thesis |
81 show thesis |
79 proof (rule Cons(1) [OF _ az]) |
82 proof (rule Cons(1) [OF _ az]) |
80 assume "rtrancl_path r y ys z" |
83 assume "rtrancl_path r y ys z" |
81 assume "rtrancl_path r a (as @ [y]) y" |
84 assume "rtrancl_path r a (as @ [y]) y" |
82 with xa have "rtrancl_path r x (a # (as @ [y])) y" |
85 with xa have "rtrancl_path r x (a # (as @ [y])) y" |
83 by (rule rtrancl_path.step) |
86 by (rule rtrancl_path.step) |
84 then have "rtrancl_path r x ((a # as) @ [y]) y" |
87 then have "rtrancl_path r x ((a # as) @ [y]) y" |
85 by simp |
88 by simp |
86 then show ?thesis using \<open>rtrancl_path r y ys z\<close> |
89 then show thesis using \<open>rtrancl_path r y ys z\<close> |
87 by (rule Cons(2)) |
90 by (rule Cons(2)) |
88 qed |
91 qed |
89 qed |
92 qed |
90 |
93 |
91 lemma rtrancl_path_distinct: |
94 lemma rtrancl_path_distinct: |
92 assumes xy: "rtrancl_path r x xs y" |
95 assumes xy: "rtrancl_path r x xs y" |
93 obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')" using xy |
96 obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')" |
|
97 using xy |
94 proof (induct xs rule: measure_induct_rule [of length]) |
98 proof (induct xs rule: measure_induct_rule [of length]) |
95 case (less xs) |
99 case (less xs) |
96 show ?case |
100 show ?case |
97 proof (cases "distinct (x # xs)") |
101 proof (cases "distinct (x # xs)") |
98 case True |
102 case True |
136 base: "rtrancl_tab r xs x x" |
140 base: "rtrancl_tab r xs x x" |
137 | step: "x \<notin> set xs \<Longrightarrow> r x y \<Longrightarrow> rtrancl_tab r (x # xs) y z \<Longrightarrow> rtrancl_tab r xs x z" |
141 | step: "x \<notin> set xs \<Longrightarrow> r x y \<Longrightarrow> rtrancl_tab r (x # xs) y z \<Longrightarrow> rtrancl_tab r xs x z" |
138 |
142 |
139 lemma rtrancl_path_imp_rtrancl_tab: |
143 lemma rtrancl_path_imp_rtrancl_tab: |
140 assumes path: "rtrancl_path r x xs y" |
144 assumes path: "rtrancl_path r x xs y" |
141 and x: "distinct (x # xs)" |
145 and x: "distinct (x # xs)" |
142 and ys: "({x} \<union> set xs) \<inter> set ys = {}" |
146 and ys: "({x} \<union> set xs) \<inter> set ys = {}" |
143 shows "rtrancl_tab r ys x y" using path x ys |
147 shows "rtrancl_tab r ys x y" |
|
148 using path x ys |
144 proof (induct arbitrary: ys) |
149 proof (induct arbitrary: ys) |
145 case base |
150 case base |
146 show ?case by (rule rtrancl_tab.base) |
151 show ?case |
|
152 by (rule rtrancl_tab.base) |
147 next |
153 next |
148 case (step x y zs z) |
154 case (step x y zs z) |
149 then have "x \<notin> set ys" by auto |
155 then have "x \<notin> set ys" |
150 from step have "distinct (y # zs)" by simp |
156 by auto |
|
157 from step have "distinct (y # zs)" |
|
158 by simp |
151 moreover from step have "({y} \<union> set zs) \<inter> set (x # ys) = {}" |
159 moreover from step have "({y} \<union> set zs) \<inter> set (x # ys) = {}" |
152 by auto |
160 by auto |
153 ultimately have "rtrancl_tab r (x # ys) y z" |
161 ultimately have "rtrancl_tab r (x # ys) y z" |
154 by (rule step) |
162 by (rule step) |
155 with \<open>x \<notin> set ys\<close> \<open>r x y\<close> |
163 with \<open>x \<notin> set ys\<close> \<open>r x y\<close> show ?case |
156 show ?case by (rule rtrancl_tab.step) |
164 by (rule rtrancl_tab.step) |
157 qed |
165 qed |
158 |
166 |
159 lemma rtrancl_tab_imp_rtrancl_path: |
167 lemma rtrancl_tab_imp_rtrancl_path: |
160 assumes tab: "rtrancl_tab r ys x y" |
168 assumes tab: "rtrancl_tab r ys x y" |
161 obtains xs where "rtrancl_path r x xs y" using tab |
169 obtains xs where "rtrancl_path r x xs y" |
|
170 using tab |
162 proof induct |
171 proof induct |
163 case base |
172 case base |
164 from rtrancl_path.base show ?case by (rule base) |
173 from rtrancl_path.base show ?case |
165 next |
174 by (rule base) |
166 case step show ?case by (iprover intro: step rtrancl_path.step) |
175 next |
167 qed |
176 case step |
168 |
177 show ?case |
169 lemma rtranclp_eq_rtrancl_tab_nil: "r\<^sup>*\<^sup>* x y = rtrancl_tab r [] x y" |
178 by (iprover intro: step rtrancl_path.step) |
|
179 qed |
|
180 |
|
181 lemma rtranclp_eq_rtrancl_tab_nil: "r\<^sup>*\<^sup>* x y \<longleftrightarrow> rtrancl_tab r [] x y" |
170 proof |
182 proof |
171 assume "r\<^sup>*\<^sup>* x y" |
183 show "rtrancl_tab r [] x y" if "r\<^sup>*\<^sup>* x y" |
172 then obtain xs where "rtrancl_path r x xs y" |
184 proof - |
173 by (auto simp add: rtranclp_eq_rtrancl_path) |
185 from that obtain xs where "rtrancl_path r x xs y" |
174 then obtain xs' where xs': "rtrancl_path r x xs' y" |
186 by (auto simp add: rtranclp_eq_rtrancl_path) |
175 and distinct: "distinct (x # xs')" |
187 then obtain xs' where xs': "rtrancl_path r x xs' y" and distinct: "distinct (x # xs')" |
176 by (rule rtrancl_path_distinct) |
188 by (rule rtrancl_path_distinct) |
177 have "({x} \<union> set xs') \<inter> set [] = {}" by simp |
189 have "({x} \<union> set xs') \<inter> set [] = {}" |
178 with xs' distinct show "rtrancl_tab r [] x y" |
190 by simp |
179 by (rule rtrancl_path_imp_rtrancl_tab) |
191 with xs' distinct show ?thesis |
180 next |
192 by (rule rtrancl_path_imp_rtrancl_tab) |
181 assume "rtrancl_tab r [] x y" |
193 qed |
182 then obtain xs where "rtrancl_path r x xs y" |
194 show "r\<^sup>*\<^sup>* x y" if "rtrancl_tab r [] x y" |
183 by (rule rtrancl_tab_imp_rtrancl_path) |
195 proof - |
184 then show "r\<^sup>*\<^sup>* x y" |
196 from that obtain xs where "rtrancl_path r x xs y" |
185 by (auto simp add: rtranclp_eq_rtrancl_path) |
197 by (rule rtrancl_tab_imp_rtrancl_path) |
186 qed |
198 then show ?thesis |
187 |
199 by (auto simp add: rtranclp_eq_rtrancl_path) |
188 declare rtranclp_rtrancl_eq[code del] |
200 qed |
189 declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro] |
201 qed |
190 |
202 |
191 code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce |
203 declare rtranclp_rtrancl_eq [code del] |
|
204 declare rtranclp_eq_rtrancl_tab_nil [THEN iffD2, code_pred_intro] |
|
205 |
|
206 code_pred rtranclp |
|
207 using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce |
192 |
208 |
193 end |
209 end |