theory ListLibLemmas

lemma list_swap_does_swap:
       "\<lbrakk>distinct list; after_in_list list desta = Some srca\<rbrakk>
       \<Longrightarrow> after_in_list (list_swap list srca desta) srca = Some desta" apply (induct list srca rule: after_in_list.induct) apply (simp add: list_swap_def)+ apply (elim conjE) apply (intro impI conjI,simp_all) apply (frule after_in_list_in_list,simp)+ done

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