theory ListLibLemmas

lemma list_swap_one': "x \<notin> set list \<Longrightarrow> y \<in> set list \<Longrightarrow> set (list_swap list x y) = insert x (set (list)) - {y}" apply (induct list) apply (simp add: list_swap_def)+ apply (intro impI conjI) apply blast+ done

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