theory ListLibLemmas

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