1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7section "Distinct Proposition" 8 9theory Distinct_Prop (* part of non-AFP Word_Lib *) 10imports 11 "HOL_Lemmas" 12 "HOL-Library.Prefix_Order" 13begin 14 15primrec 16 distinct_prop :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a list \<Rightarrow> bool)" 17where 18 "distinct_prop P [] = True" 19| "distinct_prop P (x # xs) = ((\<forall>y\<in>set xs. P x y) \<and> distinct_prop P xs)" 20 21primrec 22 distinct_sets :: "'a set list \<Rightarrow> bool" 23where 24 "distinct_sets [] = True" 25| "distinct_sets (x#xs) = (x \<inter> \<Union> (set xs) = {} \<and> distinct_sets xs)" 26 27 28lemma distinct_prop_map: 29 "distinct_prop P (map f xs) = distinct_prop (\<lambda>x y. P (f x) (f y)) xs" 30 by (induct xs) auto 31 32lemma distinct_prop_append: 33 "distinct_prop P (xs @ ys) = 34 (distinct_prop P xs \<and> distinct_prop P ys \<and> (\<forall>x \<in> set xs. \<forall>y \<in> set ys. P x y))" 35 by (induct xs arbitrary: ys) (auto simp: conj_comms ball_Un) 36 37lemma distinct_prop_distinct: 38 "\<lbrakk> distinct xs; \<And>x y. \<lbrakk> x \<in> set xs; y \<in> set xs; x \<noteq> y \<rbrakk> \<Longrightarrow> P x y \<rbrakk> \<Longrightarrow> distinct_prop P xs" 39 by (induct xs) auto 40 41lemma distinct_prop_True [simp]: 42 "distinct_prop (\<lambda>x y. True) xs" 43 by (induct xs, auto) 44 45 46lemma distinct_prefix: 47 "\<lbrakk> distinct xs; ys \<le> xs \<rbrakk> \<Longrightarrow> distinct ys" 48 apply (induct xs arbitrary: ys; clarsimp) 49 apply (case_tac ys; clarsimp) 50 by (fastforce simp: less_eq_list_def dest: set_mono_prefix) 51 52lemma distinct_sets_prop: 53 "distinct_sets xs = distinct_prop (\<lambda>x y. x \<inter> y = {}) xs" 54 by (induct xs) auto 55 56lemma distinct_take_strg: 57 "distinct xs \<longrightarrow> distinct (take n xs)" 58 by simp 59 60lemma distinct_prop_prefixE: 61 "\<lbrakk> distinct_prop P ys; prefix xs ys \<rbrakk> \<Longrightarrow> distinct_prop P xs" 62 apply (induct xs arbitrary: ys; clarsimp) 63 apply (case_tac ys; clarsimp) 64 by (fastforce dest: set_mono_prefix) 65 66 67lemma distinct_sets_union_sub: 68 "\<lbrakk>x \<in> A; distinct_sets [A,B]\<rbrakk> \<Longrightarrow> A \<union> B - {x} = A - {x} \<union> B" 69 by (auto simp: distinct_sets_def) 70 71lemma distinct_sets_append: 72 "distinct_sets (xs @ ys) \<Longrightarrow> distinct_sets xs \<and> distinct_sets ys" 73 apply (subst distinct_sets_prop)+ 74 apply (subst (asm) distinct_sets_prop) 75 apply (subst (asm) distinct_prop_append) 76 apply clarsimp 77 done 78 79lemma distinct_sets_append1: 80 "distinct_sets (xs @ ys) \<Longrightarrow> distinct_sets xs" 81 by (drule distinct_sets_append, simp) 82 83lemma distinct_sets_append2: 84 "distinct_sets (xs @ ys) \<Longrightarrow> distinct_sets ys" 85 by (drule distinct_sets_append, simp) 86 87lemma distinct_sets_append_Cons: 88 "distinct_sets (xs @ a # ys) \<Longrightarrow> distinct_sets (xs @ ys)" 89 apply (subst distinct_sets_prop)+ 90 apply (subst (asm) distinct_sets_prop) 91 apply (subst distinct_prop_append) 92 apply (subst (asm) distinct_prop_append) 93 apply clarsimp 94 done 95 96lemma distinct_sets_append_Cons_disjoint: 97 "distinct_sets (xs @ a # ys) \<Longrightarrow> a \<inter> \<Union> (set xs) = {} " 98 apply (subst (asm) distinct_sets_prop) 99 apply (subst (asm) distinct_prop_append) 100 apply (subst Int_commute) 101 apply (subst Union_disjoint) 102 apply clarsimp 103 done 104 105lemma distinct_prop_take: 106 "\<lbrakk>distinct_prop P xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_prop P (take i xs)" 107 by (metis take_is_prefix distinct_prop_prefixE) 108 109lemma distinct_sets_take: 110 "\<lbrakk>distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_sets (take i xs)" 111 by (simp add: distinct_sets_prop distinct_prop_take) 112 113lemma distinct_prop_take_Suc: 114 "\<lbrakk>distinct_prop P xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_prop P (take (Suc i) xs)" 115 by (metis distinct_prop_take not_less take_all) 116 117lemma distinct_sets_take_Suc: 118 "\<lbrakk>distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_sets (take (Suc i) xs)" 119 by (simp add: distinct_sets_prop distinct_prop_take_Suc) 120 121lemma distinct_prop_rev: 122 "distinct_prop P (rev xs) = distinct_prop (\<lambda>y x. P x y) xs" 123 by (induct xs) (auto simp: distinct_prop_append) 124 125lemma distinct_sets_rev [simp]: 126 "distinct_sets (rev xs) = distinct_sets xs" 127 apply (unfold distinct_sets_prop) 128 apply (subst distinct_prop_rev) 129 apply (subst Int_commute) 130 apply clarsimp 131 done 132 133lemma distinct_sets_drop: 134 "\<lbrakk>distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_sets (drop i xs)" 135 apply (cases "i=0", simp) 136 apply (subst distinct_sets_rev [symmetric]) 137 apply (subst rev_drop) 138 apply (subst distinct_sets_take, simp_all) 139 done 140 141lemma distinct_sets_drop_Suc: 142 "\<lbrakk>distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_sets (drop (Suc i) xs)" 143 apply (subst distinct_sets_rev [symmetric]) 144 apply (subst rev_drop) 145 apply (subst distinct_sets_take, simp_all) 146 done 147 148lemma distinct_sets_take_nth: 149 "\<lbrakk>distinct_sets xs; i < length xs; x \<in> set (take i xs)\<rbrakk> \<Longrightarrow> x \<inter> xs ! i = {}" 150 apply (drule (1) distinct_sets_take_Suc) 151 apply (subst (asm) take_Suc_conv_app_nth, assumption) 152 apply (unfold distinct_sets_prop) 153 apply (subst (asm) distinct_prop_append) 154 apply clarsimp 155 done 156 157lemma distinct_sets_drop_nth: 158 "\<lbrakk>distinct_sets xs; i < length xs; x \<in> set (drop (Suc i) xs)\<rbrakk> \<Longrightarrow> x \<inter> xs ! i = {}" 159 apply (drule (1) distinct_sets_drop) 160 apply (subst (asm) drop_Suc_nth, assumption) 161 apply fastforce 162 done 163 164lemma distinct_sets_append_distinct: 165 "\<lbrakk>x \<in> set xs; y \<in> set ys; distinct_sets (xs @ ys)\<rbrakk> \<Longrightarrow> x \<inter> y = {}" 166 unfolding distinct_sets_prop by (clarsimp simp: distinct_prop_append) 167 168lemma distinct_sets_update: 169 "\<lbrakk>a \<subseteq> xs ! i; distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_sets (xs[i := a])" 170 apply (subst distinct_sets_prop) 171 apply (subst (asm) distinct_sets_prop) 172 apply (subst upd_conv_take_nth_drop, simp) 173 apply (subst distinct_prop_append) 174 apply (intro conjI) 175 apply (erule (1) distinct_prop_take) 176 apply (rule conjI|clarsimp)+ 177 apply (fold distinct_sets_prop) 178 apply (drule (1) distinct_sets_drop) 179 apply (subst (asm) drop_Suc_nth, assumption) 180 apply fastforce 181 apply (drule (1) distinct_sets_drop) 182 apply (subst (asm) drop_Suc_nth, assumption) 183 apply clarsimp 184 apply clarsimp 185 apply (rule conjI) 186 apply (drule (2) distinct_sets_take_nth) 187 apply blast 188 apply clarsimp 189 apply (thin_tac "P \<subseteq> Q" for P Q) 190 apply (subst (asm) id_take_nth_drop, assumption) 191 apply (drule distinct_sets_append_Cons) 192 apply (erule (2) distinct_sets_append_distinct) 193 done 194 195lemma distinct_sets_map_update: 196 "\<lbrakk>distinct_sets (map f xs); i < length xs; f a \<subseteq> f(xs ! i)\<rbrakk> 197 \<Longrightarrow> distinct_sets (map f (xs[i := a]))" 198 by (metis distinct_sets_update length_map map_update nth_map) 199 200lemma Union_list_update: 201 "\<lbrakk>i < length xs; distinct_sets (map f xs)\<rbrakk> 202 \<Longrightarrow> (\<Union>x\<in>set (xs [i := a]). f x) = (\<Union>x\<in>set xs. f x) - f (xs ! i) \<union> f a" 203 apply (induct xs arbitrary: i; clarsimp) 204 apply (case_tac i; (clarsimp, fastforce)) 205 done 206 207lemma fst_enumerate: 208 "i < length xs \<Longrightarrow> fst (enumerate n xs ! i) = i + n" 209 by (metis add.commute fst_conv nth_enumerate_eq) 210 211lemma snd_enumerate: 212 "i < length xs \<Longrightarrow> snd (enumerate n xs ! i) = xs ! i" 213 by (metis nth_enumerate_eq snd_conv) 214 215lemma enumerate_member: 216 assumes "i < length xs" 217 shows "(n + i, xs ! i) \<in> set (enumerate n xs)" 218proof - 219 have pair_unpack: "\<And>a b x. ((a, b) = x) = (a = fst x \<and> b = snd x)" by fastforce 220 from assms have "(n + i, xs ! i) = enumerate n xs ! i" 221 by (auto simp: fst_enumerate snd_enumerate pair_unpack) 222 with assms show ?thesis by simp 223qed 224 225lemma distinct_prop_nth: 226 "\<lbrakk> distinct_prop P ls; n < n'; n' < length ls \<rbrakk> \<Longrightarrow> P (ls ! n) (ls ! n')" 227 apply (induct ls arbitrary: n n'; simp) 228 apply (case_tac n'; simp) 229 apply (case_tac n; simp) 230 done 231 232end 233