22 apply simp |
22 apply simp |
23 apply (subgoal_tac "{ja. Suc ja < j} = {0..<j - Suc 0}") |
23 apply (subgoal_tac "{ja. Suc ja < j} = {0..<j - Suc 0}") |
24 apply (subgoal_tac "{ja. j \<le> Suc ja \<and> Suc ja < k} = {j - Suc 0..<k - Suc 0}") |
24 apply (subgoal_tac "{ja. j \<le> Suc ja \<and> Suc ja < k} = {j - Suc 0..<k - Suc 0}") |
25 apply (subgoal_tac "{j. Suc j < k} = {0..<k - Suc 0}") |
25 apply (subgoal_tac "{j. Suc j < k} = {0..<k - Suc 0}") |
26 apply simp |
26 apply simp |
27 apply fastsimp |
27 apply fastforce |
28 apply fastsimp |
28 apply fastforce |
29 apply fastsimp |
29 apply fastforce |
30 apply fastsimp |
30 apply fastforce |
31 apply (erule_tac x="i - 1" in meta_allE) |
31 apply (erule_tac x="i - 1" in meta_allE) |
32 apply (erule_tac x="j - 1" in meta_allE) |
32 apply (erule_tac x="j - 1" in meta_allE) |
33 apply (erule_tac x="k - 1" in meta_allE) |
33 apply (erule_tac x="k - 1" in meta_allE) |
34 apply (subgoal_tac " {ja. i \<le> Suc ja \<and> Suc ja < j} = {i - 1 ..<j - 1}") |
34 apply (subgoal_tac " {ja. i \<le> Suc ja \<and> Suc ja < j} = {i - 1 ..<j - 1}") |
35 apply (subgoal_tac " {ja. j \<le> Suc ja \<and> Suc ja < k} = {j - 1..<k - 1}") |
35 apply (subgoal_tac " {ja. j \<le> Suc ja \<and> Suc ja < k} = {j - 1..<k - 1}") |
36 apply (subgoal_tac "{j. i \<le> Suc j \<and> Suc j < k} = {i - 1..<k - 1}") |
36 apply (subgoal_tac "{j. i \<le> Suc j \<and> Suc j < k} = {i - 1..<k - 1}") |
37 apply (subgoal_tac " i - 1 \<le> j - 1 \<and> j - 1 \<le> k - 1") |
37 apply (subgoal_tac " i - 1 \<le> j - 1 \<and> j - 1 \<le> k - 1") |
38 apply simp |
38 apply simp |
39 apply fastsimp |
39 apply fastforce |
40 apply fastsimp |
40 apply fastforce |
41 apply fastsimp |
41 apply fastforce |
42 apply fastsimp |
42 apply fastforce |
43 done |
43 done |
44 |
44 |
45 lemma sublist_update1: "i \<notin> inds \<Longrightarrow> sublist (xs[i := v]) inds = sublist xs inds" |
45 lemma sublist_update1: "i \<notin> inds \<Longrightarrow> sublist (xs[i := v]) inds = sublist xs inds" |
46 apply (induct xs arbitrary: i inds) |
46 apply (induct xs arbitrary: i inds) |
47 apply simp |
47 apply simp |
141 |
141 |
142 lemma sublist_eq_subseteq: " \<lbrakk> inds' \<subseteq> inds; sublist xs inds = sublist ys inds \<rbrakk> \<Longrightarrow> sublist xs inds' = sublist ys inds'" |
142 lemma sublist_eq_subseteq: " \<lbrakk> inds' \<subseteq> inds; sublist xs inds = sublist ys inds \<rbrakk> \<Longrightarrow> sublist xs inds' = sublist ys inds'" |
143 apply (induct xs arbitrary: ys inds inds') |
143 apply (induct xs arbitrary: ys inds inds') |
144 apply simp |
144 apply simp |
145 apply (drule sym, rule sym) |
145 apply (drule sym, rule sym) |
146 apply (simp add: sublist_Nil, fastsimp) |
146 apply (simp add: sublist_Nil, fastforce) |
147 apply (case_tac ys) |
147 apply (case_tac ys) |
148 apply (simp add: sublist_Nil, fastsimp) |
148 apply (simp add: sublist_Nil, fastforce) |
149 apply (auto simp add: sublist_Cons) |
149 apply (auto simp add: sublist_Cons) |
150 apply (erule_tac x="list" in meta_allE) |
150 apply (erule_tac x="list" in meta_allE) |
151 apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE) |
151 apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE) |
152 apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE) |
152 apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE) |
153 apply fastsimp |
153 apply fastforce |
154 apply (erule_tac x="list" in meta_allE) |
154 apply (erule_tac x="list" in meta_allE) |
155 apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE) |
155 apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE) |
156 apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE) |
156 apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE) |
157 apply fastsimp |
157 apply fastforce |
158 done |
158 done |
159 |
159 |
160 lemma sublist_eq: "\<lbrakk> \<forall>i \<in> inds. ((i < length xs) \<and> (i < length ys)) \<or> ((i \<ge> length xs ) \<and> (i \<ge> length ys)); \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> sublist xs inds = sublist ys inds" |
160 lemma sublist_eq: "\<lbrakk> \<forall>i \<in> inds. ((i < length xs) \<and> (i < length ys)) \<or> ((i \<ge> length xs ) \<and> (i \<ge> length ys)); \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> sublist xs inds = sublist ys inds" |
161 apply (induct xs arbitrary: ys inds) |
161 apply (induct xs arbitrary: ys inds) |
162 apply simp |
162 apply simp |
164 apply (case_tac ys) |
164 apply (case_tac ys) |
165 apply (simp add: sublist_Nil) |
165 apply (simp add: sublist_Nil) |
166 apply (auto simp add: sublist_Cons) |
166 apply (auto simp add: sublist_Cons) |
167 apply (erule_tac x="list" in meta_allE) |
167 apply (erule_tac x="list" in meta_allE) |
168 apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE) |
168 apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE) |
169 apply fastsimp |
169 apply fastforce |
170 apply (erule_tac x="list" in meta_allE) |
170 apply (erule_tac x="list" in meta_allE) |
171 apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE) |
171 apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE) |
172 apply fastsimp |
172 apply fastforce |
173 done |
173 done |
174 |
174 |
175 lemma sublist_eq_samelength: "\<lbrakk> length xs = length ys; \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> sublist xs inds = sublist ys inds" |
175 lemma sublist_eq_samelength: "\<lbrakk> length xs = length ys; \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> sublist xs inds = sublist ys inds" |
176 by (rule sublist_eq, auto) |
176 by (rule sublist_eq, auto) |
177 |
177 |