1(* Title: HOL/UNITY/ListOrder.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1998 University of Cambridge 4 5Lists are partially ordered by Charpentier's Generalized Prefix Relation 6 (xs,ys) : genPrefix(r) 7 if ys = xs' @ zs where length xs = length xs' 8 and corresponding elements of xs, xs' are pairwise related by r 9 10Also overloads <= and < for lists! 11*) 12 13section \<open>The Prefix Ordering on Lists\<close> 14 15theory ListOrder 16imports Main 17begin 18 19inductive_set 20 genPrefix :: "('a * 'a)set => ('a list * 'a list)set" 21 for r :: "('a * 'a)set" 22 where 23 Nil: "([],[]) \<in> genPrefix(r)" 24 25 | prepend: "[| (xs,ys) \<in> genPrefix(r); (x,y) \<in> r |] ==> 26 (x#xs, y#ys) \<in> genPrefix(r)" 27 28 | append: "(xs,ys) \<in> genPrefix(r) ==> (xs, ys@zs) \<in> genPrefix(r)" 29 30instantiation list :: (type) ord 31begin 32 33definition 34 prefix_def: "xs <= zs \<longleftrightarrow> (xs, zs) \<in> genPrefix Id" 35 36definition 37 strict_prefix_def: "xs < zs \<longleftrightarrow> xs \<le> zs \<and> \<not> zs \<le> (xs :: 'a list)" 38 39instance .. 40 41(*Constants for the <= and >= relations, used below in translations*) 42 43end 44 45definition Le :: "(nat*nat) set" where 46 "Le == {(x,y). x <= y}" 47 48definition Ge :: "(nat*nat) set" where 49 "Ge == {(x,y). y <= x}" 50 51abbreviation 52 pfixLe :: "[nat list, nat list] => bool" (infixl "pfixLe" 50) where 53 "xs pfixLe ys == (xs,ys) \<in> genPrefix Le" 54 55abbreviation 56 pfixGe :: "[nat list, nat list] => bool" (infixl "pfixGe" 50) where 57 "xs pfixGe ys == (xs,ys) \<in> genPrefix Ge" 58 59 60subsection\<open>preliminary lemmas\<close> 61 62lemma Nil_genPrefix [iff]: "([], xs) \<in> genPrefix r" 63by (cut_tac genPrefix.Nil [THEN genPrefix.append], auto) 64 65lemma genPrefix_length_le: "(xs,ys) \<in> genPrefix r \<Longrightarrow> length xs <= length ys" 66by (erule genPrefix.induct, auto) 67 68lemma cdlemma: 69 "[| (xs', ys') \<in> genPrefix r |] 70 ==> (\<forall>x xs. xs' = x#xs \<longrightarrow> (\<exists>y ys. ys' = y#ys & (x,y) \<in> r & (xs, ys) \<in> genPrefix r))" 71apply (erule genPrefix.induct, blast, blast) 72apply (force intro: genPrefix.append) 73done 74 75(*As usual converting it to an elimination rule is tiresome*) 76lemma cons_genPrefixE [elim!]: 77 "[| (x#xs, zs) \<in> genPrefix r; 78 !!y ys. [| zs = y#ys; (x,y) \<in> r; (xs, ys) \<in> genPrefix r |] ==> P 79 |] ==> P" 80by (drule cdlemma, simp, blast) 81 82lemma Cons_genPrefix_Cons [iff]: 83 "((x#xs,y#ys) \<in> genPrefix r) = ((x,y) \<in> r \<and> (xs,ys) \<in> genPrefix r)" 84by (blast intro: genPrefix.prepend) 85 86 87subsection\<open>genPrefix is a partial order\<close> 88 89lemma refl_genPrefix: "refl r ==> refl (genPrefix r)" 90apply (unfold refl_on_def, auto) 91apply (induct_tac "x") 92prefer 2 apply (blast intro: genPrefix.prepend) 93apply (blast intro: genPrefix.Nil) 94done 95 96lemma genPrefix_refl [simp]: "refl r \<Longrightarrow> (l,l) \<in> genPrefix r" 97by (erule refl_onD [OF refl_genPrefix UNIV_I]) 98 99lemma genPrefix_mono: "r<=s ==> genPrefix r <= genPrefix s" 100apply clarify 101apply (erule genPrefix.induct) 102apply (auto intro: genPrefix.append) 103done 104 105 106(** Transitivity **) 107 108(*A lemma for proving genPrefix_trans_O*) 109lemma append_genPrefix: 110 "(xs @ ys, zs) \<in> genPrefix r \<Longrightarrow> (xs, zs) \<in> genPrefix r" 111 by (induct xs arbitrary: zs) auto 112 113(*Lemma proving transitivity and more*) 114lemma genPrefix_trans_O: 115 assumes "(x, y) \<in> genPrefix r" 116 shows "\<And>z. (y, z) \<in> genPrefix s \<Longrightarrow> (x, z) \<in> genPrefix (r O s)" 117 apply (atomize (full)) 118 using assms 119 apply induct 120 apply blast 121 apply (blast intro: genPrefix.prepend) 122 apply (blast dest: append_genPrefix) 123 done 124 125lemma genPrefix_trans: 126 "(x, y) \<in> genPrefix r \<Longrightarrow> (y, z) \<in> genPrefix r \<Longrightarrow> trans r 127 \<Longrightarrow> (x, z) \<in> genPrefix r" 128 apply (rule trans_O_subset [THEN genPrefix_mono, THEN subsetD]) 129 apply assumption 130 apply (blast intro: genPrefix_trans_O) 131 done 132 133lemma prefix_genPrefix_trans: 134 "[| x<=y; (y,z) \<in> genPrefix r |] ==> (x, z) \<in> genPrefix r" 135apply (unfold prefix_def) 136apply (drule genPrefix_trans_O, assumption) 137apply simp 138done 139 140lemma genPrefix_prefix_trans: 141 "[| (x,y) \<in> genPrefix r; y<=z |] ==> (x,z) \<in> genPrefix r" 142apply (unfold prefix_def) 143apply (drule genPrefix_trans_O, assumption) 144apply simp 145done 146 147lemma trans_genPrefix: "trans r ==> trans (genPrefix r)" 148by (blast intro: transI genPrefix_trans) 149 150 151(** Antisymmetry **) 152 153lemma genPrefix_antisym: 154 assumes 1: "(xs, ys) \<in> genPrefix r" 155 and 2: "antisym r" 156 and 3: "(ys, xs) \<in> genPrefix r" 157 shows "xs = ys" 158 using 1 3 159proof induct 160 case Nil 161 then show ?case by blast 162next 163 case prepend 164 then show ?case using 2 by (simp add: antisym_def) 165next 166 case (append xs ys zs) 167 then show ?case 168 apply - 169 apply (subgoal_tac "length zs = 0", force) 170 apply (drule genPrefix_length_le)+ 171 apply (simp del: length_0_conv) 172 done 173qed 174 175lemma antisym_genPrefix: "antisym r ==> antisym (genPrefix r)" 176 by (blast intro: antisymI genPrefix_antisym) 177 178 179subsection\<open>recursion equations\<close> 180 181lemma genPrefix_Nil [simp]: "((xs, []) \<in> genPrefix r) = (xs = [])" 182 by (induct xs) auto 183 184lemma same_genPrefix_genPrefix [simp]: 185 "refl r \<Longrightarrow> ((xs@ys, xs@zs) \<in> genPrefix r) = ((ys,zs) \<in> genPrefix r)" 186 by (induct xs) (simp_all add: refl_on_def) 187 188lemma genPrefix_Cons: 189 "((xs, y#ys) \<in> genPrefix r) = 190 (xs=[] | (\<exists>z zs. xs=z#zs & (z,y) \<in> r & (zs,ys) \<in> genPrefix r))" 191 by (cases xs) auto 192 193lemma genPrefix_take_append: 194 "[| refl r; (xs,ys) \<in> genPrefix r |] 195 ==> (xs@zs, take (length xs) ys @ zs) \<in> genPrefix r" 196apply (erule genPrefix.induct) 197apply (frule_tac [3] genPrefix_length_le) 198apply (simp_all (no_asm_simp) add: diff_is_0_eq [THEN iffD2]) 199done 200 201lemma genPrefix_append_both: 202 "[| refl r; (xs,ys) \<in> genPrefix r; length xs = length ys |] 203 ==> (xs@zs, ys @ zs) \<in> genPrefix r" 204apply (drule genPrefix_take_append, assumption) 205apply simp 206done 207 208 209(*NOT suitable for rewriting since [y] has the form y#ys*) 210lemma append_cons_eq: "xs @ y # ys = (xs @ [y]) @ ys" 211by auto 212 213lemma aolemma: 214 "[| (xs,ys) \<in> genPrefix r; refl r |] 215 ==> length xs < length ys \<longrightarrow> (xs @ [ys ! length xs], ys) \<in> genPrefix r" 216apply (erule genPrefix.induct) 217 apply blast 218 apply simp 219txt\<open>Append case is hardest\<close> 220apply simp 221apply (frule genPrefix_length_le [THEN le_imp_less_or_eq]) 222apply (erule disjE) 223apply (simp_all (no_asm_simp) add: neq_Nil_conv nth_append) 224apply (blast intro: genPrefix.append, auto) 225apply (subst append_cons_eq, fast intro: genPrefix_append_both genPrefix.append) 226done 227 228lemma append_one_genPrefix: 229 "[| (xs,ys) \<in> genPrefix r; length xs < length ys; refl r |] 230 ==> (xs @ [ys ! length xs], ys) \<in> genPrefix r" 231by (blast intro: aolemma [THEN mp]) 232 233 234(** Proving the equivalence with Charpentier's definition **) 235 236lemma genPrefix_imp_nth: 237 "i < length xs \<Longrightarrow> (xs, ys) \<in> genPrefix r \<Longrightarrow> (xs ! i, ys ! i) \<in> r" 238 apply (induct xs arbitrary: i ys) 239 apply auto 240 apply (case_tac i) 241 apply auto 242 done 243 244lemma nth_imp_genPrefix: 245 "length xs <= length ys \<Longrightarrow> 246 (\<forall>i. i < length xs \<longrightarrow> (xs ! i, ys ! i) \<in> r) \<Longrightarrow> 247 (xs, ys) \<in> genPrefix r" 248 apply (induct xs arbitrary: ys) 249 apply (simp_all add: less_Suc_eq_0_disj all_conj_distrib) 250 apply (case_tac ys) 251 apply (force+) 252 done 253 254lemma genPrefix_iff_nth: 255 "((xs,ys) \<in> genPrefix r) = 256 (length xs <= length ys & (\<forall>i. i < length xs \<longrightarrow> (xs!i, ys!i) \<in> r))" 257apply (blast intro: genPrefix_length_le genPrefix_imp_nth nth_imp_genPrefix) 258done 259 260 261subsection\<open>The type of lists is partially ordered\<close> 262 263declare refl_Id [iff] 264 antisym_Id [iff] 265 trans_Id [iff] 266 267lemma prefix_refl [iff]: "xs <= (xs::'a list)" 268by (simp add: prefix_def) 269 270lemma prefix_trans: "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs" 271apply (unfold prefix_def) 272apply (blast intro: genPrefix_trans) 273done 274 275lemma prefix_antisym: "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys" 276apply (unfold prefix_def) 277apply (blast intro: genPrefix_antisym) 278done 279 280lemma prefix_less_le_not_le: "!!xs::'a list. (xs < zs) = (xs <= zs & \<not> zs \<le> xs)" 281by (unfold strict_prefix_def, auto) 282 283instance list :: (type) order 284 by (intro_classes, 285 (assumption | rule prefix_refl prefix_trans prefix_antisym 286 prefix_less_le_not_le)+) 287 288(*Monotonicity of "set" operator WRT prefix*) 289lemma set_mono: "xs <= ys ==> set xs <= set ys" 290apply (unfold prefix_def) 291apply (erule genPrefix.induct, auto) 292done 293 294 295(** recursion equations **) 296 297lemma Nil_prefix [iff]: "[] <= xs" 298by (simp add: prefix_def) 299 300lemma prefix_Nil [simp]: "(xs <= []) = (xs = [])" 301by (simp add: prefix_def) 302 303lemma Cons_prefix_Cons [simp]: "(x#xs <= y#ys) = (x=y & xs<=ys)" 304by (simp add: prefix_def) 305 306lemma same_prefix_prefix [simp]: "(xs@ys <= xs@zs) = (ys <= zs)" 307by (simp add: prefix_def) 308 309lemma append_prefix [iff]: "(xs@ys <= xs) = (ys <= [])" 310by (insert same_prefix_prefix [of xs ys "[]"], simp) 311 312lemma prefix_appendI [simp]: "xs <= ys ==> xs <= ys@zs" 313apply (unfold prefix_def) 314apply (erule genPrefix.append) 315done 316 317lemma prefix_Cons: 318 "(xs <= y#ys) = (xs=[] | (\<exists>zs. xs=y#zs \<and> zs <= ys))" 319by (simp add: prefix_def genPrefix_Cons) 320 321lemma append_one_prefix: 322 "[| xs <= ys; length xs < length ys |] ==> xs @ [ys ! length xs] <= ys" 323apply (unfold prefix_def) 324apply (simp add: append_one_genPrefix) 325done 326 327lemma prefix_length_le: "xs <= ys ==> length xs <= length ys" 328apply (unfold prefix_def) 329apply (erule genPrefix_length_le) 330done 331 332lemma splemma: "xs<=ys ==> xs~=ys --> length xs < length ys" 333apply (unfold prefix_def) 334apply (erule genPrefix.induct, auto) 335done 336 337lemma strict_prefix_length_less: "xs < ys ==> length xs < length ys" 338apply (unfold strict_prefix_def) 339apply (blast intro: splemma [THEN mp]) 340done 341 342lemma mono_length: "mono length" 343by (blast intro: monoI prefix_length_le) 344 345(*Equivalence to the definition used in Lex/Prefix.thy*) 346lemma prefix_iff: "(xs <= zs) = (\<exists>ys. zs = xs@ys)" 347apply (unfold prefix_def) 348apply (auto simp add: genPrefix_iff_nth nth_append) 349apply (rule_tac x = "drop (length xs) zs" in exI) 350apply (rule nth_equalityI) 351apply (simp_all (no_asm_simp) add: nth_append) 352done 353 354lemma prefix_snoc [simp]: "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)" 355apply (simp add: prefix_iff) 356apply (rule iffI) 357 apply (erule exE) 358 apply (rename_tac "zs") 359 apply (rule_tac xs = zs in rev_exhaust) 360 apply simp 361 apply clarify 362 apply (simp del: append_assoc add: append_assoc [symmetric], force) 363done 364 365lemma prefix_append_iff: 366 "(xs <= ys@zs) = (xs <= ys | (\<exists>us. xs = ys@us & us <= zs))" 367apply (rule_tac xs = zs in rev_induct) 368 apply force 369apply (simp del: append_assoc add: append_assoc [symmetric], force) 370done 371 372(*Although the prefix ordering is not linear, the prefixes of a list 373 are linearly ordered.*) 374lemma common_prefix_linear: 375 fixes xs ys zs :: "'a list" 376 shows "xs <= zs \<Longrightarrow> ys <= zs \<Longrightarrow> xs <= ys | ys <= xs" 377 by (induct zs rule: rev_induct) auto 378 379subsection\<open>pfixLe, pfixGe: properties inherited from the translations\<close> 380 381(** pfixLe **) 382 383lemma refl_Le [iff]: "refl Le" 384by (unfold refl_on_def Le_def, auto) 385 386lemma antisym_Le [iff]: "antisym Le" 387by (unfold antisym_def Le_def, auto) 388 389lemma trans_Le [iff]: "trans Le" 390by (unfold trans_def Le_def, auto) 391 392lemma pfixLe_refl [iff]: "x pfixLe x" 393by simp 394 395lemma pfixLe_trans: "[| x pfixLe y; y pfixLe z |] ==> x pfixLe z" 396by (blast intro: genPrefix_trans) 397 398lemma pfixLe_antisym: "[| x pfixLe y; y pfixLe x |] ==> x = y" 399by (blast intro: genPrefix_antisym) 400 401lemma prefix_imp_pfixLe: "xs<=ys ==> xs pfixLe ys" 402apply (unfold prefix_def Le_def) 403apply (blast intro: genPrefix_mono [THEN [2] rev_subsetD]) 404done 405 406lemma refl_Ge [iff]: "refl Ge" 407by (unfold refl_on_def Ge_def, auto) 408 409lemma antisym_Ge [iff]: "antisym Ge" 410by (unfold antisym_def Ge_def, auto) 411 412lemma trans_Ge [iff]: "trans Ge" 413by (unfold trans_def Ge_def, auto) 414 415lemma pfixGe_refl [iff]: "x pfixGe x" 416by simp 417 418lemma pfixGe_trans: "[| x pfixGe y; y pfixGe z |] ==> x pfixGe z" 419by (blast intro: genPrefix_trans) 420 421lemma pfixGe_antisym: "[| x pfixGe y; y pfixGe x |] ==> x = y" 422by (blast intro: genPrefix_antisym) 423 424lemma prefix_imp_pfixGe: "xs<=ys ==> xs pfixGe ys" 425apply (unfold prefix_def Ge_def) 426apply (blast intro: genPrefix_mono [THEN [2] rev_subsetD]) 427done 428 429end 430