theory Distinct_Prop

lemma distinct_sets_update:
 "\<lbrakk>a \<subseteq> xs ! i; distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_sets (xs[i := a])" apply (subst distinct_sets_prop) apply (subst (asm) distinct_sets_prop) apply (subst upd_conv_take_nth_drop, simp) apply (subst distinct_prop_append) apply (intro conjI) apply (erule (1) distinct_prop_take) apply (rule conjI|clarsimp)+ apply (fold distinct_sets_prop) apply (drule (1) distinct_sets_drop) apply (subst (asm) drop_Suc_nth, assumption) apply fastforce apply (drule (1) distinct_sets_drop) apply (subst (asm) drop_Suc_nth, assumption) apply clarsimp apply clarsimp apply (rule conjI) apply (drule (2) distinct_sets_take_nth) apply blast apply clarsimp apply (thin_tac "P \<subseteq> Q" for P Q) apply (subst (asm) id_take_nth_drop, assumption) apply (drule distinct_sets_append_Cons) apply (erule (2) distinct_sets_append_distinct) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<subseteq> xs ! i; distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_sets (xs[i := a]) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<subseteq> xs ! i; distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_prop (\<lambda>x y. x \<inter> y = {}) (xs[i := a]) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<subseteq> xs ! i; distinct_prop (\<lambda>x y. x \<inter> y = {}) xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_prop (\<lambda>x y. x \<inter> y = {}) (xs[i := a]) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<subseteq> xs ! i; distinct_prop (\<lambda>x y. x \<inter> y = {}) xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_prop (\<lambda>x y. x \<inter> y = {}) (take i xs @ a # drop (Suc i) xs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<subseteq> xs ! i; distinct_prop (\<lambda>x y. x \<inter> y = {}) xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_prop (\<lambda>x y. x \<inter> y = {}) (take i xs) \<and> distinct_prop (\<lambda>x y. x \<inter> y = {}) (a # drop (Suc i) xs) \<and> (\<forall>x\<in>set (take i xs). \<forall>y\<in>set (a # drop (Suc i) xs). x \<inter> y = {}) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>a \<subseteq> xs ! i; distinct_prop (\<lambda>x y. x \<inter> y = {}) xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_prop (\<lambda>x y. x \<inter> y = {}) (take i xs)
 2. \<lbrakk>a \<subseteq> xs ! i; distinct_prop (\<lambda>x y. x \<inter> y = {}) xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_prop (\<lambda>x y. x \<inter> y = {}) (a # drop (Suc i) xs)
 3. \<lbrakk>a \<subseteq> xs ! i; distinct_prop (\<lambda>x y. x \<inter> y = {}) xs; i < length xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (take i xs). \<forall>y\<in>set (a # drop (Suc i) xs). x \<inter> y = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<subseteq> xs ! i; distinct_prop (\<lambda>x y. x \<inter> y = {}) xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_prop (\<lambda>x y. x \<inter> y = {}) (a # drop (Suc i) xs)
 2. \<lbrakk>a \<subseteq> xs ! i; distinct_prop (\<lambda>x y. x \<inter> y = {}) xs; i < length xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (take i xs). \<forall>y\<in>set (a # drop (Suc i) xs). x \<inter> y = {} proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>a \<subseteq> xs ! i; distinct_prop (\<lambda>x y. x \<inter> y = {}) xs; i < length xs; y \<in> set (drop (Suc i) xs)\<rbrakk> \<Longrightarrow> a \<inter> y = {}
 2. \<lbrakk>a \<subseteq> xs ! i; distinct_prop (\<lambda>x y. x \<inter> y = {}) xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_prop (\<lambda>x y. x \<inter> y = {}) (drop (Suc i) xs)
 3. \<lbrakk>a \<subseteq> xs ! i; distinct_prop (\<lambda>x y. x \<inter> y = {}) xs; i < length xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (take i xs). \<forall>y\<in>set (a # drop (Suc i) xs). x \<inter> y = {} proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>a \<subseteq> xs ! i; distinct_sets xs; i < length xs; y \<in> set (drop (Suc i) xs)\<rbrakk> \<Longrightarrow> a \<inter> y = {}
 2. \<lbrakk>a \<subseteq> xs ! i; distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_sets (drop (Suc i) xs)
 3. \<lbrakk>a \<subseteq> xs ! i; distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (take i xs). \<forall>y\<in>set (a # drop (Suc i) xs). x \<inter> y = {} proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>a \<subseteq> xs ! i; i < length xs; y \<in> set (drop (Suc i) xs); distinct_sets (drop i xs)\<rbrakk> \<Longrightarrow> a \<inter> y = {}
 2. \<lbrakk>a \<subseteq> xs ! i; distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_sets (drop (Suc i) xs)
 3. \<lbrakk>a \<subseteq> xs ! i; distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (take i xs). \<forall>y\<in>set (a # drop (Suc i) xs). x \<inter> y = {} proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>a \<subseteq> xs ! i; i < length xs; y \<in> set (drop (Suc i) xs); distinct_sets (xs ! i # drop (Suc i) xs)\<rbrakk> \<Longrightarrow> a \<inter> y = {}
 2. \<lbrakk>a \<subseteq> xs ! i; distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_sets (drop (Suc i) xs)
 3. \<lbrakk>a \<subseteq> xs ! i; distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (take i xs). \<forall>y\<in>set (a # drop (Suc i) xs). x \<inter> y = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<subseteq> xs ! i; distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_sets (drop (Suc i) xs)
 2. \<lbrakk>a \<subseteq> xs ! i; distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (take i xs). \<forall>y\<in>set (a # drop (Suc i) xs). x \<inter> y = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<subseteq> xs ! i; i < length xs; distinct_sets (drop i xs)\<rbrakk> \<Longrightarrow> distinct_sets (drop (Suc i) xs)
 2. \<lbrakk>a \<subseteq> xs ! i; distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (take i xs). \<forall>y\<in>set (a # drop (Suc i) xs). x \<inter> y = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<subseteq> xs ! i; i < length xs; distinct_sets (xs ! i # drop (Suc i) xs)\<rbrakk> \<Longrightarrow> distinct_sets (drop (Suc i) xs)
 2. \<lbrakk>a \<subseteq> xs ! i; distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (take i xs). \<forall>y\<in>set (a # drop (Suc i) xs). x \<inter> y = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<subseteq> xs ! i; distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (take i xs). \<forall>y\<in>set (a # drop (Suc i) xs). x \<inter> y = {} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>a \<subseteq> xs ! i; distinct_sets xs; i < length xs; x \<in> set (take i xs)\<rbrakk> \<Longrightarrow> x \<inter> a = {} \<and> (\<forall>y\<in>set (drop (Suc i) xs). x \<inter> y = {}) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>a \<subseteq> xs ! i; distinct_sets xs; i < length xs; x \<in> set (take i xs)\<rbrakk> \<Longrightarrow> x \<inter> a = {}
 2. \<And>x. \<lbrakk>a \<subseteq> xs ! i; distinct_sets xs; i < length xs; x \<in> set (take i xs)\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (drop (Suc i) xs). x \<inter> y = {} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>a \<subseteq> xs ! i; i < length xs; x \<in> set (take i xs); x \<inter> xs ! i = {}\<rbrakk> \<Longrightarrow> x \<inter> a = {}
 2. \<And>x. \<lbrakk>a \<subseteq> xs ! i; distinct_sets xs; i < length xs; x \<in> set (take i xs)\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (drop (Suc i) xs). x \<inter> y = {} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>a \<subseteq> xs ! i; distinct_sets xs; i < length xs; x \<in> set (take i xs)\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (drop (Suc i) xs). x \<inter> y = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>a \<subseteq> xs ! i; distinct_sets xs; i < length xs; x \<in> set (take i xs); y \<in> set (drop (Suc i) xs)\<rbrakk> \<Longrightarrow> x \<inter> y = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>distinct_sets xs; i < length xs; x \<in> set (take i xs); y \<in> set (drop (Suc i) xs)\<rbrakk> \<Longrightarrow> x \<inter> y = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>distinct_sets (take i xs @ xs ! i # drop (Suc i) xs); i < length xs; x \<in> set (take i xs); y \<in> set (drop (Suc i) xs)\<rbrakk> \<Longrightarrow> x \<inter> y = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>i < length xs; x \<in> set (take i xs); y \<in> set (drop (Suc i) xs); distinct_sets (take i xs @ drop (Suc i) xs)\<rbrakk> \<Longrightarrow> x \<inter> y = {} proof (prove)
goal:
No subgoals!