91 qed |
91 qed |
92 qed |
92 qed |
93 |
93 |
94 lemma rtrancl_path_distinct: |
94 lemma rtrancl_path_distinct: |
95 assumes xy: "rtrancl_path r x xs y" |
95 assumes xy: "rtrancl_path r x xs y" |
96 obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')" |
96 obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')" and "set xs' \<subseteq> set xs" |
97 using xy |
97 using xy |
98 proof (induct xs rule: measure_induct_rule [of length]) |
98 proof (induct xs rule: measure_induct_rule [of length]) |
99 case (less xs) |
99 case (less xs) |
100 show ?case |
100 show ?case |
101 proof (cases "distinct (x # xs)") |
101 proof (cases "distinct (x # xs)") |
102 case True |
102 case True |
103 with \<open>rtrancl_path r x xs y\<close> show ?thesis by (rule less) |
103 with \<open>rtrancl_path r x xs y\<close> show ?thesis by (rule less) simp |
104 next |
104 next |
105 case False |
105 case False |
106 then have "\<exists>as bs cs a. x # xs = as @ [a] @ bs @ [a] @ cs" |
106 then have "\<exists>as bs cs a. x # xs = as @ [a] @ bs @ [a] @ cs" |
107 by (rule not_distinct_decomp) |
107 by (rule not_distinct_decomp) |
108 then obtain as bs cs a where xxs: "x # xs = as @ [a] @ bs @ [a] @ cs" |
108 then obtain as bs cs a where xxs: "x # xs = as @ [a] @ bs @ [a] @ cs" |
110 show ?thesis |
110 show ?thesis |
111 proof (cases as) |
111 proof (cases as) |
112 case Nil |
112 case Nil |
113 with xxs have x: "x = a" and xs: "xs = bs @ a # cs" |
113 with xxs have x: "x = a" and xs: "xs = bs @ a # cs" |
114 by auto |
114 by auto |
115 from x xs \<open>rtrancl_path r x xs y\<close> have cs: "rtrancl_path r x cs y" |
115 from x xs \<open>rtrancl_path r x xs y\<close> have cs: "rtrancl_path r x cs y" "set cs \<subseteq> set xs" |
116 by (auto elim: rtrancl_path_appendE) |
116 by (auto elim: rtrancl_path_appendE) |
117 from xs have "length cs < length xs" by simp |
117 from xs have "length cs < length xs" by simp |
118 then show ?thesis |
118 then show ?thesis |
119 by (rule less(1)) (iprover intro: cs less(2))+ |
119 by (rule less(1))(blast intro: cs less(2) order_trans del: subsetI)+ |
120 next |
120 next |
121 case (Cons d ds) |
121 case (Cons d ds) |
122 with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)" |
122 with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)" |
123 by auto |
123 by auto |
124 with \<open>rtrancl_path r x xs y\<close> obtain xa: "rtrancl_path r x (ds @ [a]) a" |
124 with \<open>rtrancl_path r x xs y\<close> obtain xa: "rtrancl_path r x (ds @ [a]) a" |
125 and ay: "rtrancl_path r a (bs @ a # cs) y" |
125 and ay: "rtrancl_path r a (bs @ a # cs) y" |
126 by (auto elim: rtrancl_path_appendE) |
126 by (auto elim: rtrancl_path_appendE) |
127 from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE) |
127 from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE) |
128 with xa have xy: "rtrancl_path r x ((ds @ [a]) @ cs) y" |
128 with xa have xy: "rtrancl_path r x ((ds @ [a]) @ cs) y" |
129 by (rule rtrancl_path_trans) |
129 by (rule rtrancl_path_trans) |
|
130 from xs have set: "set ((ds @ [a]) @ cs) \<subseteq> set xs" by auto |
130 from xs have "length ((ds @ [a]) @ cs) < length xs" by simp |
131 from xs have "length ((ds @ [a]) @ cs) < length xs" by simp |
131 then show ?thesis |
132 then show ?thesis |
132 by (rule less(1)) (iprover intro: xy less(2))+ |
133 by (rule less(1))(blast intro: xy less(2) set[THEN subsetD])+ |
133 qed |
134 qed |
134 qed |
135 qed |
135 qed |
136 qed |
136 |
137 |
137 inductive rtrancl_tab :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
138 inductive rtrancl_tab :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |