theory ListLibLemmas

lemma swap_distinct: "x \<in> set list \<Longrightarrow> y \<in> set list \<Longrightarrow> distinct list \<Longrightarrow> distinct (list_swap list x y)" apply (induct list) apply (simp add: list_swap_def)+ apply (intro impI conjI,simp_all) apply (simp add: map_ignore2 map_ignore2' swap_distinct_helper | elim conjE | force)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set list; y \<in> set list; distinct list\<rbrakk> \<Longrightarrow> distinct (list_swap list x y) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> set []; y \<in> set []; distinct []\<rbrakk> \<Longrightarrow> distinct (list_swap [] x y)
 2. \<And>a list. \<lbrakk>\<lbrakk>x \<in> set list; y \<in> set list; distinct list\<rbrakk> \<Longrightarrow> distinct (list_swap list x y); x \<in> set (a # list); y \<in> set (a # list); distinct (a # list)\<rbrakk> \<Longrightarrow> distinct (list_swap (a # list) x y) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<lbrakk>x \<in> set list; y \<in> set list\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>xa. if xa = x then y else if xa = y then x else xa) list); x = a \<or> x \<in> set list; y = a \<or> y \<in> set list; a \<notin> set list \<and> distinct list\<rbrakk> \<Longrightarrow> (a = y \<longrightarrow> (y = x \<longrightarrow> x \<notin> set list \<and> distinct (map (\<lambda>xa. if xa = x then y else if xa = y then x else xa) list)) \<and> (y \<noteq> x \<longrightarrow> x \<notin> (\<lambda>a. y) ` (set list \<inter> {x}) \<and> x \<notin> (\<lambda>a. x) ` (set list \<inter> {xa. xa \<noteq> x} \<inter> {y}) \<and> distinct (map (\<lambda>xa. if xa = x then y else if xa = y then x else xa) list))) \<and> (a \<noteq> y \<longrightarrow> (a = x \<longrightarrow> y \<notin> (\<lambda>a. y) ` (set list \<inter> {x}) \<and> y \<notin> (\<lambda>a. x) ` (set list \<inter> {xa. xa \<noteq> x} \<inter> {y}) \<and> distinct (map (\<lambda>xa. if xa = x then y else if xa = y then x else xa) list)) \<and> (a \<noteq> x \<longrightarrow> a \<notin> (\<lambda>a. y) ` (set list \<inter> {x}) \<and> a \<notin> (\<lambda>a. x) ` (set list \<inter> {xa. xa \<noteq> x} \<inter> {y}) \<and> distinct (map (\<lambda>xa. if xa = x then y else if xa = y then x else xa) list))) proof (prove)
goal (4 subgoals):
 1. \<And>a list. \<lbrakk>x \<notin> set list \<and> distinct list; a = x; y = x\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>xa. if xa = x then y else if xa = y then x else xa) list)
 2. \<And>a list. \<lbrakk>x \<in> set list; y \<notin> set list \<and> distinct list; a = y; y \<noteq> x\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>xa. if xa = x then y else if xa = y then x else xa) list)
 3. \<And>a list. \<lbrakk>y \<in> set list; x \<notin> set list \<and> distinct list; x \<noteq> y; a = x\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>xa. if xa = x then y else if xa = y then x else xa) list)
 4. \<And>a list. \<lbrakk>distinct (map (\<lambda>xa. if xa = x then y else if xa = y then x else xa) list); x \<in> set list; y \<in> set list; a \<notin> set list \<and> distinct list; a \<noteq> y; a \<noteq> x\<rbrakk> \<Longrightarrow> a \<notin> (\<lambda>a. x) ` (set list \<inter> {xa. xa \<noteq> x} \<inter> {y}) proof (prove)
goal:
No subgoals!