theory ListLibLemmas

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