theory ListLibLemmas

lemma list_swap_does_swap':
  "distinct list \<Longrightarrow> after_in_list list srca = Some desta \<Longrightarrow>
                after_in_list (list_swap list srca desta) srca =
          after_in_list list 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 (case_tac xs) apply (clarsimp+)[2] apply (case_tac xs) apply clarsimp+ done

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