theory ListLibLemmas

lemma list_swap_preserve_Some_other:
 "\<lbrakk>z \<noteq> desta; z \<noteq> srca; after_in_list list srca = Some z\<rbrakk>
\<Longrightarrow> after_in_list (list_swap list srca desta) desta = Some z" apply (induct list srca rule: after_in_list.induct) apply (simp add: list_swap_def)+ apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>z \<noteq> desta; z \<noteq> srca; after_in_list list srca = Some z\<rbrakk> \<Longrightarrow> after_in_list (list_swap list srca desta) desta = Some z proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>z \<noteq> desta; z \<noteq> a; after_in_list [] a = Some z\<rbrakk> \<Longrightarrow> after_in_list (list_swap [] a desta) desta = Some z
 2. \<And>x a. \<lbrakk>z \<noteq> desta; z \<noteq> a; after_in_list [x] a = Some z\<rbrakk> \<Longrightarrow> after_in_list (list_swap [x] a desta) desta = Some z
 3. \<And>x y xs a. \<lbrakk>\<lbrakk>a \<noteq> x; z \<noteq> desta; z \<noteq> a; after_in_list (y # xs) a = Some z\<rbrakk> \<Longrightarrow> after_in_list (list_swap (y # xs) a desta) desta = Some z; z \<noteq> desta; z \<noteq> a; after_in_list (x # y # xs) a = Some z\<rbrakk> \<Longrightarrow> after_in_list (list_swap (x # y # xs) a desta) desta = Some z proof (prove)
goal (1 subgoal):
 1. \<And>x y xs a. \<lbrakk>\<lbrakk>a \<noteq> x; after_in_list (y # xs) a = Some z\<rbrakk> \<Longrightarrow> after_in_list ((if y = a then desta else if y = desta then a else y) # map (\<lambda>x. if x = a then desta else if x = desta then a else x) xs) desta = Some z; z \<noteq> desta; z \<noteq> a; (if a = x then Some y else after_in_list (y # xs) a) = Some z\<rbrakk> \<Longrightarrow> (x = desta \<longrightarrow> (desta = a \<longrightarrow> y \<noteq> a \<and> (y \<noteq> a \<longrightarrow> y = z)) \<and> (desta \<noteq> a \<longrightarrow> (y = desta \<longrightarrow> after_in_list (a # map (\<lambda>x. if x = a then desta else if x = desta then a else x) xs) desta = Some z) \<and> (y \<noteq> desta \<longrightarrow> (y = a \<longrightarrow> after_in_list (desta # map (\<lambda>x. if x = a then desta else if x = desta then a else x) xs) desta = Some z) \<and> (y \<noteq> a \<longrightarrow> after_in_list (y # map (\<lambda>x. if x = a then desta else if x = desta then a else x) xs) desta = Some z)))) \<and> (x \<noteq> desta \<longrightarrow> (x = a \<longrightarrow> y \<noteq> desta \<and> (y \<noteq> desta \<longrightarrow> y \<noteq> a \<and> (y \<noteq> a \<longrightarrow> y = z))) \<and> (x \<noteq> a \<longrightarrow> (y = desta \<longrightarrow> (desta = a \<longrightarrow> after_in_list (a # map (\<lambda>x. if x = a then desta else if x = desta then a else x) xs) a = Some z) \<and> (desta \<noteq> a \<longrightarrow> after_in_list (a # map (\<lambda>x. if x = a then desta else if x = desta then a else x) xs) desta = Some z)) \<and> (y \<noteq> desta \<longrightarrow> (y = a \<longrightarrow> after_in_list (desta # map (\<lambda>x. if x = a then desta else if x = desta then a else x) xs) desta = Some z) \<and> (y \<noteq> a \<longrightarrow> after_in_list (y # map (\<lambda>x. if x = a then desta else if x = desta then a else x) xs) desta = Some z)))) proof (prove)
goal:
No subgoals!