theory ListLibLemmas

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

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