1(* Title: ZF/UNITY/GenPrefix.thy 2 Author: Sidi O Ehmety, Cambridge University Computer Laboratory 3 Copyright 2001 University of Cambridge 4 5<xs,ys>:gen_prefix(r) 6 if ys = xs' @ zs where length(xs) = length(xs') 7 and corresponding elements of xs, xs' are pairwise related by r 8 9Based on Lex/Prefix 10*) 11 12section\<open>Charpentier's Generalized Prefix Relation\<close> 13 14theory GenPrefix 15imports ZF 16begin 17 18definition (*really belongs in ZF/Trancl*) 19 part_order :: "[i, i] => o" where 20 "part_order(A, r) == refl(A,r) & trans[A](r) & antisym(r)" 21 22consts 23 gen_prefix :: "[i, i] => i" 24 25inductive 26 (* Parameter A is the domain of zs's elements *) 27 28 domains "gen_prefix(A, r)" \<subseteq> "list(A)*list(A)" 29 30 intros 31 Nil: "<[],[]>:gen_prefix(A, r)" 32 33 prepend: "[| <xs,ys>:gen_prefix(A, r); <x,y>:r; x \<in> A; y \<in> A |] 34 ==> <Cons(x,xs), Cons(y,ys)>: gen_prefix(A, r)" 35 36 append: "[| <xs,ys>:gen_prefix(A, r); zs:list(A) |] 37 ==> <xs, ys@zs>:gen_prefix(A, r)" 38 type_intros app_type list.Nil list.Cons 39 40definition 41 prefix :: "i=>i" where 42 "prefix(A) == gen_prefix(A, id(A))" 43 44definition 45 strict_prefix :: "i=>i" where 46 "strict_prefix(A) == prefix(A) - id(list(A))" 47 48 49(* less or equal and greater or equal over prefixes *) 50 51abbreviation 52 pfixLe :: "[i, i] => o" (infixl "pfixLe" 50) where 53 "xs pfixLe ys == <xs, ys>:gen_prefix(nat, Le)" 54 55abbreviation 56 pfixGe :: "[i, i] => o" (infixl "pfixGe" 50) where 57 "xs pfixGe ys == <xs, ys>:gen_prefix(nat, Ge)" 58 59 60lemma reflD: 61 "[| refl(A, r); x \<in> A |] ==> <x,x>:r" 62apply (unfold refl_def, auto) 63done 64 65(*** preliminary lemmas ***) 66 67lemma Nil_gen_prefix: "xs \<in> list(A) ==> <[], xs> \<in> gen_prefix(A, r)" 68by (drule gen_prefix.append [OF gen_prefix.Nil], simp) 69declare Nil_gen_prefix [simp] 70 71 72lemma gen_prefix_length_le: "<xs,ys> \<in> gen_prefix(A, r) ==> length(xs) \<le> length(ys)" 73apply (erule gen_prefix.induct) 74apply (subgoal_tac [3] "ys \<in> list (A) ") 75apply (auto dest: gen_prefix.dom_subset [THEN subsetD] 76 intro: le_trans simp add: length_app) 77done 78 79 80lemma Cons_gen_prefix_aux: 81 "[| <xs', ys'> \<in> gen_prefix(A, r) |] 82 ==> (\<forall>x xs. x \<in> A \<longrightarrow> xs'= Cons(x,xs) \<longrightarrow> 83 (\<exists>y ys. y \<in> A & ys' = Cons(y,ys) & 84 <x,y>:r & <xs, ys> \<in> gen_prefix(A, r)))" 85apply (erule gen_prefix.induct) 86prefer 3 apply (force intro: gen_prefix.append, auto) 87done 88 89lemma Cons_gen_prefixE: 90 "[| <Cons(x,xs), zs> \<in> gen_prefix(A, r); 91 !!y ys. [|zs = Cons(y, ys); y \<in> A; x \<in> A; <x,y>:r; 92 <xs,ys> \<in> gen_prefix(A, r) |] ==> P |] ==> P" 93apply (frule gen_prefix.dom_subset [THEN subsetD], auto) 94apply (blast dest: Cons_gen_prefix_aux) 95done 96declare Cons_gen_prefixE [elim!] 97 98lemma Cons_gen_prefix_Cons: 99"(<Cons(x,xs),Cons(y,ys)> \<in> gen_prefix(A, r)) 100 \<longleftrightarrow> (x \<in> A & y \<in> A & <x,y>:r & <xs,ys> \<in> gen_prefix(A, r))" 101apply (auto intro: gen_prefix.prepend) 102done 103declare Cons_gen_prefix_Cons [iff] 104 105(** Monotonicity of gen_prefix **) 106 107lemma gen_prefix_mono2: "r<=s ==> gen_prefix(A, r) \<subseteq> gen_prefix(A, s)" 108apply clarify 109apply (frule gen_prefix.dom_subset [THEN subsetD], clarify) 110apply (erule rev_mp) 111apply (erule gen_prefix.induct) 112apply (auto intro: gen_prefix.append) 113done 114 115lemma gen_prefix_mono1: "A<=B ==>gen_prefix(A, r) \<subseteq> gen_prefix(B, r)" 116apply clarify 117apply (frule gen_prefix.dom_subset [THEN subsetD], clarify) 118apply (erule rev_mp) 119apply (erule_tac P = "y \<in> list (A) " in rev_mp) 120apply (erule_tac P = "xa \<in> list (A) " in rev_mp) 121apply (erule gen_prefix.induct) 122apply (simp (no_asm_simp)) 123apply clarify 124apply (erule ConsE)+ 125apply (auto dest: gen_prefix.dom_subset [THEN subsetD] 126 intro: gen_prefix.append list_mono [THEN subsetD]) 127done 128 129lemma gen_prefix_mono: "[| A \<subseteq> B; r \<subseteq> s |] ==> gen_prefix(A, r) \<subseteq> gen_prefix(B, s)" 130apply (rule subset_trans) 131apply (rule gen_prefix_mono1) 132apply (rule_tac [2] gen_prefix_mono2, auto) 133done 134 135(*** gen_prefix order ***) 136 137(* reflexivity *) 138lemma refl_gen_prefix: "refl(A, r) ==> refl(list(A), gen_prefix(A, r))" 139apply (unfold refl_def, auto) 140apply (induct_tac "x", auto) 141done 142declare refl_gen_prefix [THEN reflD, simp] 143 144(* Transitivity *) 145(* A lemma for proving gen_prefix_trans_comp *) 146 147lemma append_gen_prefix [rule_format (no_asm)]: "xs \<in> list(A) ==> 148 \<forall>zs. <xs @ ys, zs> \<in> gen_prefix(A, r) \<longrightarrow> <xs, zs>: gen_prefix(A, r)" 149apply (erule list.induct) 150apply (auto dest: gen_prefix.dom_subset [THEN subsetD]) 151done 152 153(* Lemma proving transitivity and more*) 154 155lemma gen_prefix_trans_comp [rule_format (no_asm)]: 156 "<x, y>: gen_prefix(A, r) ==> 157 (\<forall>z \<in> list(A). <y,z> \<in> gen_prefix(A, s)\<longrightarrow><x, z> \<in> gen_prefix(A, s O r))" 158apply (erule gen_prefix.induct) 159apply (auto elim: ConsE simp add: Nil_gen_prefix) 160apply (subgoal_tac "ys \<in> list (A) ") 161prefer 2 apply (blast dest: gen_prefix.dom_subset [THEN subsetD]) 162apply (drule_tac xs = ys and r = s in append_gen_prefix, auto) 163done 164 165lemma trans_comp_subset: "trans(r) ==> r O r \<subseteq> r" 166by (auto dest: transD) 167 168lemma trans_gen_prefix: "trans(r) ==> trans(gen_prefix(A,r))" 169apply (simp (no_asm) add: trans_def) 170apply clarify 171apply (rule trans_comp_subset [THEN gen_prefix_mono2, THEN subsetD], assumption) 172apply (rule gen_prefix_trans_comp) 173apply (auto dest: gen_prefix.dom_subset [THEN subsetD]) 174done 175 176lemma trans_on_gen_prefix: 177 "trans(r) ==> trans[list(A)](gen_prefix(A, r))" 178apply (drule_tac A = A in trans_gen_prefix) 179apply (unfold trans_def trans_on_def, blast) 180done 181 182lemma prefix_gen_prefix_trans: 183 "[| <x,y> \<in> prefix(A); <y, z> \<in> gen_prefix(A, r); r<=A*A |] 184 ==> <x, z> \<in> gen_prefix(A, r)" 185apply (unfold prefix_def) 186apply (rule_tac P = "%r. <x,z> \<in> gen_prefix (A, r) " in right_comp_id [THEN subst]) 187apply (blast dest: gen_prefix_trans_comp gen_prefix.dom_subset [THEN subsetD])+ 188done 189 190 191lemma gen_prefix_prefix_trans: 192"[| <x,y> \<in> gen_prefix(A,r); <y, z> \<in> prefix(A); r<=A*A |] 193 ==> <x, z> \<in> gen_prefix(A, r)" 194apply (unfold prefix_def) 195apply (rule_tac P = "%r. <x,z> \<in> gen_prefix (A, r) " in left_comp_id [THEN subst]) 196apply (blast dest: gen_prefix_trans_comp gen_prefix.dom_subset [THEN subsetD])+ 197done 198 199(** Antisymmetry **) 200 201lemma nat_le_lemma [rule_format]: "n \<in> nat ==> \<forall>b \<in> nat. n #+ b \<le> n \<longrightarrow> b = 0" 202by (induct_tac "n", auto) 203 204lemma antisym_gen_prefix: "antisym(r) ==> antisym(gen_prefix(A, r))" 205apply (simp (no_asm) add: antisym_def) 206apply (rule impI [THEN allI, THEN allI]) 207apply (erule gen_prefix.induct, blast) 208apply (simp add: antisym_def, blast) 209txt\<open>append case is hardest\<close> 210apply clarify 211apply (subgoal_tac "length (zs) = 0") 212apply (subgoal_tac "ys \<in> list (A) ") 213prefer 2 apply (blast dest: gen_prefix.dom_subset [THEN subsetD]) 214apply (drule_tac psi = "<ys @ zs, xs> \<in> gen_prefix (A,r) " in asm_rl) 215apply simp 216apply (subgoal_tac "length (ys @ zs) = length (ys) #+ length (zs) &ys \<in> list (A) &xs \<in> list (A) ") 217prefer 2 apply (blast intro: length_app dest: gen_prefix.dom_subset [THEN subsetD]) 218apply (drule gen_prefix_length_le)+ 219apply clarify 220apply simp 221apply (drule_tac j = "length (xs) " in le_trans) 222apply blast 223apply (auto intro: nat_le_lemma) 224done 225 226(*** recursion equations ***) 227 228lemma gen_prefix_Nil: "xs \<in> list(A) ==> <xs, []> \<in> gen_prefix(A,r) \<longleftrightarrow> (xs = [])" 229by (induct_tac "xs", auto) 230declare gen_prefix_Nil [simp] 231 232lemma same_gen_prefix_gen_prefix: 233 "[| refl(A, r); xs \<in> list(A) |] ==> 234 <xs@ys, xs@zs>: gen_prefix(A, r) \<longleftrightarrow> <ys,zs> \<in> gen_prefix(A, r)" 235apply (unfold refl_def) 236apply (induct_tac "xs") 237apply (simp_all (no_asm_simp)) 238done 239declare same_gen_prefix_gen_prefix [simp] 240 241lemma gen_prefix_Cons: "[| xs \<in> list(A); ys \<in> list(A); y \<in> A |] ==> 242 <xs, Cons(y,ys)> \<in> gen_prefix(A,r) \<longleftrightarrow> 243 (xs=[] | (\<exists>z zs. xs=Cons(z,zs) & z \<in> A & <z,y>:r & <zs,ys> \<in> gen_prefix(A,r)))" 244apply (induct_tac "xs", auto) 245done 246 247lemma gen_prefix_take_append: "[| refl(A,r); <xs,ys> \<in> gen_prefix(A, r); zs \<in> list(A) |] 248 ==> <xs@zs, take(length(xs), ys) @ zs> \<in> gen_prefix(A, r)" 249apply (erule gen_prefix.induct) 250apply (simp (no_asm_simp)) 251apply (frule_tac [!] gen_prefix.dom_subset [THEN subsetD], auto) 252apply (frule gen_prefix_length_le) 253apply (subgoal_tac "take (length (xs), ys) \<in> list (A) ") 254apply (simp_all (no_asm_simp) add: diff_is_0_iff [THEN iffD2] take_type) 255done 256 257lemma gen_prefix_append_both: "[| refl(A, r); <xs,ys> \<in> gen_prefix(A,r); 258 length(xs) = length(ys); zs \<in> list(A) |] 259 ==> <xs@zs, ys @ zs> \<in> gen_prefix(A, r)" 260apply (drule_tac zs = zs in gen_prefix_take_append, assumption+) 261apply (subgoal_tac "take (length (xs), ys) =ys") 262apply (auto intro!: take_all dest: gen_prefix.dom_subset [THEN subsetD]) 263done 264 265(*NOT suitable for rewriting since [y] has the form y#ys*) 266lemma append_cons_conv: "xs \<in> list(A) ==> xs @ Cons(y, ys) = (xs @ [y]) @ ys" 267by (auto simp add: app_assoc) 268 269lemma append_one_gen_prefix_lemma [rule_format]: 270 "[| <xs,ys> \<in> gen_prefix(A, r); refl(A, r) |] 271 ==> length(xs) < length(ys) \<longrightarrow> 272 <xs @ [nth(length(xs), ys)], ys> \<in> gen_prefix(A, r)" 273apply (erule gen_prefix.induct, blast) 274apply (frule gen_prefix.dom_subset [THEN subsetD], clarify) 275apply (simp_all add: length_type) 276(* Append case is hardest *) 277apply (frule gen_prefix_length_le [THEN le_iff [THEN iffD1]]) 278apply (frule gen_prefix.dom_subset [THEN subsetD], clarify) 279apply (subgoal_tac "length (xs) :nat&length (ys) :nat &length (zs) :nat") 280prefer 2 apply (blast intro: length_type, clarify) 281apply (simp_all add: nth_append length_type length_app) 282apply (rule conjI) 283apply (blast intro: gen_prefix.append) 284apply (erule_tac V = "length (xs) < length (ys) \<longrightarrow>u" for u in thin_rl) 285apply (erule_tac a = zs in list.cases, auto) 286apply (rule_tac P1 = "%x. <u(x), v>:w" for u v w in nat_diff_split [THEN iffD2]) 287apply auto 288apply (simplesubst append_cons_conv) 289apply (rule_tac [2] gen_prefix.append) 290apply (auto elim: ConsE simp add: gen_prefix_append_both) 291done 292 293lemma append_one_gen_prefix: "[| <xs,ys>: gen_prefix(A, r); length(xs) < length(ys); refl(A, r) |] 294 ==> <xs @ [nth(length(xs), ys)], ys> \<in> gen_prefix(A, r)" 295apply (blast intro: append_one_gen_prefix_lemma) 296done 297 298 299(** Proving the equivalence with Charpentier's definition **) 300 301lemma gen_prefix_imp_nth_lemma [rule_format]: "xs \<in> list(A) ==> 302 \<forall>ys \<in> list(A). \<forall>i \<in> nat. i < length(xs) 303 \<longrightarrow> <xs, ys>: gen_prefix(A, r) \<longrightarrow> <nth(i, xs), nth(i, ys)>:r" 304apply (induct_tac "xs", simp, clarify) 305apply simp 306apply (erule natE, auto) 307done 308 309lemma gen_prefix_imp_nth: "[| <xs,ys> \<in> gen_prefix(A,r); i < length(xs)|] 310 ==> <nth(i, xs), nth(i, ys)>:r" 311apply (cut_tac A = A in gen_prefix.dom_subset) 312apply (rule gen_prefix_imp_nth_lemma) 313apply (auto simp add: lt_nat_in_nat) 314done 315 316lemma nth_imp_gen_prefix [rule_format]: "xs \<in> list(A) ==> 317 \<forall>ys \<in> list(A). length(xs) \<le> length(ys) 318 \<longrightarrow> (\<forall>i. i < length(xs) \<longrightarrow> <nth(i, xs), nth(i,ys)>:r) 319 \<longrightarrow> <xs, ys> \<in> gen_prefix(A, r)" 320apply (induct_tac "xs") 321apply (simp_all (no_asm_simp)) 322apply clarify 323apply (erule_tac a = ys in list.cases, simp) 324apply (force intro!: nat_0_le simp add: lt_nat_in_nat) 325done 326 327lemma gen_prefix_iff_nth: "(<xs,ys> \<in> gen_prefix(A,r)) \<longleftrightarrow> 328 (xs \<in> list(A) & ys \<in> list(A) & length(xs) \<le> length(ys) & 329 (\<forall>i. i < length(xs) \<longrightarrow> <nth(i,xs), nth(i, ys)>: r))" 330apply (rule iffI) 331apply (frule gen_prefix.dom_subset [THEN subsetD]) 332apply (frule gen_prefix_length_le, auto) 333apply (rule_tac [2] nth_imp_gen_prefix) 334apply (drule gen_prefix_imp_nth) 335apply (auto simp add: lt_nat_in_nat) 336done 337 338(** prefix is a partial order: **) 339 340lemma refl_prefix: "refl(list(A), prefix(A))" 341apply (unfold prefix_def) 342apply (rule refl_gen_prefix) 343apply (auto simp add: refl_def) 344done 345declare refl_prefix [THEN reflD, simp] 346 347lemma trans_prefix: "trans(prefix(A))" 348apply (unfold prefix_def) 349apply (rule trans_gen_prefix) 350apply (auto simp add: trans_def) 351done 352 353lemmas prefix_trans = trans_prefix [THEN transD] 354 355lemma trans_on_prefix: "trans[list(A)](prefix(A))" 356apply (unfold prefix_def) 357apply (rule trans_on_gen_prefix) 358apply (auto simp add: trans_def) 359done 360 361lemmas prefix_trans_on = trans_on_prefix [THEN trans_onD] 362 363(* Monotonicity of "set" operator WRT prefix *) 364 365lemma set_of_list_prefix_mono: 366"<xs,ys> \<in> prefix(A) ==> set_of_list(xs) \<subseteq> set_of_list(ys)" 367 368apply (unfold prefix_def) 369apply (erule gen_prefix.induct) 370apply (subgoal_tac [3] "xs \<in> list (A) &ys \<in> list (A) ") 371prefer 4 apply (blast dest: gen_prefix.dom_subset [THEN subsetD]) 372apply (auto simp add: set_of_list_append) 373done 374 375(** recursion equations **) 376 377lemma Nil_prefix: "xs \<in> list(A) ==> <[],xs> \<in> prefix(A)" 378 379apply (unfold prefix_def) 380apply (simp (no_asm_simp) add: Nil_gen_prefix) 381done 382declare Nil_prefix [simp] 383 384 385lemma prefix_Nil: "<xs, []> \<in> prefix(A) \<longleftrightarrow> (xs = [])" 386 387apply (unfold prefix_def, auto) 388apply (frule gen_prefix.dom_subset [THEN subsetD]) 389apply (drule_tac psi = "<xs, []> \<in> gen_prefix (A, id (A))" in asm_rl) 390apply (simp add: gen_prefix_Nil) 391done 392declare prefix_Nil [iff] 393 394lemma Cons_prefix_Cons: 395"<Cons(x,xs), Cons(y,ys)> \<in> prefix(A) \<longleftrightarrow> (x=y & <xs,ys> \<in> prefix(A) & y \<in> A)" 396apply (unfold prefix_def, auto) 397done 398declare Cons_prefix_Cons [iff] 399 400lemma same_prefix_prefix: 401"xs \<in> list(A)==> <xs@ys,xs@zs> \<in> prefix(A) \<longleftrightarrow> (<ys,zs> \<in> prefix(A))" 402apply (unfold prefix_def) 403apply (subgoal_tac "refl (A,id (A))") 404apply (simp (no_asm_simp)) 405apply (auto simp add: refl_def) 406done 407declare same_prefix_prefix [simp] 408 409lemma same_prefix_prefix_Nil: "xs \<in> list(A) ==> <xs@ys,xs> \<in> prefix(A) \<longleftrightarrow> (<ys,[]> \<in> prefix(A))" 410apply (rule_tac P = "%x. <u, x>:v \<longleftrightarrow> w(x)" for u v w in app_right_Nil [THEN subst]) 411apply (rule_tac [2] same_prefix_prefix, auto) 412done 413declare same_prefix_prefix_Nil [simp] 414 415lemma prefix_appendI: 416"[| <xs,ys> \<in> prefix(A); zs \<in> list(A) |] ==> <xs,ys@zs> \<in> prefix(A)" 417apply (unfold prefix_def) 418apply (erule gen_prefix.append, assumption) 419done 420declare prefix_appendI [simp] 421 422lemma prefix_Cons: 423"[| xs \<in> list(A); ys \<in> list(A); y \<in> A |] ==> 424 <xs,Cons(y,ys)> \<in> prefix(A) \<longleftrightarrow> 425 (xs=[] | (\<exists>zs. xs=Cons(y,zs) & <zs,ys> \<in> prefix(A)))" 426apply (unfold prefix_def) 427apply (auto simp add: gen_prefix_Cons) 428done 429 430lemma append_one_prefix: 431 "[| <xs,ys> \<in> prefix(A); length(xs) < length(ys) |] 432 ==> <xs @ [nth(length(xs),ys)], ys> \<in> prefix(A)" 433apply (unfold prefix_def) 434apply (subgoal_tac "refl (A, id (A))") 435apply (simp (no_asm_simp) add: append_one_gen_prefix) 436apply (auto simp add: refl_def) 437done 438 439lemma prefix_length_le: 440"<xs,ys> \<in> prefix(A) ==> length(xs) \<le> length(ys)" 441apply (unfold prefix_def) 442apply (blast dest: gen_prefix_length_le) 443done 444 445lemma prefix_type: "prefix(A)<=list(A)*list(A)" 446apply (unfold prefix_def) 447apply (blast intro!: gen_prefix.dom_subset) 448done 449 450lemma strict_prefix_type: 451"strict_prefix(A) \<subseteq> list(A)*list(A)" 452apply (unfold strict_prefix_def) 453apply (blast intro!: prefix_type [THEN subsetD]) 454done 455 456lemma strict_prefix_length_lt_aux: 457 "<xs,ys> \<in> prefix(A) ==> xs\<noteq>ys \<longrightarrow> length(xs) < length(ys)" 458apply (unfold prefix_def) 459apply (erule gen_prefix.induct, clarify) 460apply (subgoal_tac [!] "ys \<in> list(A) & xs \<in> list(A)") 461apply (auto dest: gen_prefix.dom_subset [THEN subsetD] 462 simp add: length_type) 463apply (subgoal_tac "length (zs) =0") 464apply (drule_tac [2] not_lt_imp_le) 465apply (rule_tac [5] j = "length (ys) " in lt_trans2) 466apply auto 467done 468 469lemma strict_prefix_length_lt: 470 "<xs,ys>:strict_prefix(A) ==> length(xs) < length(ys)" 471apply (unfold strict_prefix_def) 472apply (rule strict_prefix_length_lt_aux [THEN mp]) 473apply (auto dest: prefix_type [THEN subsetD]) 474done 475 476(*Equivalence to the definition used in Lex/Prefix.thy*) 477lemma prefix_iff: 478 "<xs,zs> \<in> prefix(A) \<longleftrightarrow> (\<exists>ys \<in> list(A). zs = xs@ys) & xs \<in> list(A)" 479apply (unfold prefix_def) 480apply (auto simp add: gen_prefix_iff_nth lt_nat_in_nat nth_append nth_type app_type length_app) 481apply (subgoal_tac "drop (length (xs), zs) \<in> list (A) ") 482apply (rule_tac x = "drop (length (xs), zs) " in bexI) 483apply safe 484 prefer 2 apply (simp add: length_type drop_type) 485apply (rule nth_equalityI) 486apply (simp_all (no_asm_simp) add: nth_append app_type drop_type length_app length_drop) 487apply (rule nat_diff_split [THEN iffD2], simp_all, clarify) 488apply (drule_tac i = "length (zs) " in leI) 489apply (force simp add: le_subset_iff, safe) 490apply (subgoal_tac "length (xs) #+ (i #- length (xs)) = i") 491apply (subst nth_drop) 492apply (simp_all (no_asm_simp) add: leI split: nat_diff_split) 493done 494 495lemma prefix_snoc: 496"[|xs \<in> list(A); ys \<in> list(A); y \<in> A |] ==> 497 <xs, ys@[y]> \<in> prefix(A) \<longleftrightarrow> (xs = ys@[y] | <xs,ys> \<in> prefix(A))" 498apply (simp (no_asm) add: prefix_iff) 499apply (rule iffI, clarify) 500apply (erule_tac xs = ysa in rev_list_elim, simp) 501apply (simp add: app_type app_assoc [symmetric]) 502apply (auto simp add: app_assoc app_type) 503done 504declare prefix_snoc [simp] 505 506lemma prefix_append_iff [rule_format]: "zs \<in> list(A) ==> \<forall>xs \<in> list(A). \<forall>ys \<in> list(A). 507 (<xs, ys@zs> \<in> prefix(A)) \<longleftrightarrow> 508 (<xs,ys> \<in> prefix(A) | (\<exists>us. xs = ys@us & <us,zs> \<in> prefix(A)))" 509apply (erule list_append_induct, force, clarify) 510apply (rule iffI) 511apply (simp add: add: app_assoc [symmetric]) 512apply (erule disjE) 513apply (rule disjI2) 514apply (rule_tac x = "y @ [x]" in exI) 515apply (simp add: add: app_assoc [symmetric], force+) 516done 517 518 519(*Although the prefix ordering is not linear, the prefixes of a list 520 are linearly ordered.*) 521lemma common_prefix_linear_lemma [rule_format]: "[| zs \<in> list(A); xs \<in> list(A); ys \<in> list(A) |] 522 ==> <xs, zs> \<in> prefix(A) \<longrightarrow> <ys,zs> \<in> prefix(A) 523 \<longrightarrow><xs,ys> \<in> prefix(A) | <ys,xs> \<in> prefix(A)" 524apply (erule list_append_induct, auto) 525done 526 527lemma common_prefix_linear: "[|<xs, zs> \<in> prefix(A); <ys,zs> \<in> prefix(A) |] 528 ==> <xs,ys> \<in> prefix(A) | <ys,xs> \<in> prefix(A)" 529apply (cut_tac prefix_type) 530apply (blast del: disjCI intro: common_prefix_linear_lemma) 531done 532 533 534(*** pfixLe, pfixGe \<in> properties inherited from the translations ***) 535 536 537 538(** pfixLe **) 539 540lemma refl_Le: "refl(nat,Le)" 541 542apply (unfold refl_def, auto) 543done 544declare refl_Le [simp] 545 546lemma antisym_Le: "antisym(Le)" 547apply (unfold antisym_def) 548apply (auto intro: le_anti_sym) 549done 550declare antisym_Le [simp] 551 552lemma trans_on_Le: "trans[nat](Le)" 553apply (unfold trans_on_def, auto) 554apply (blast intro: le_trans) 555done 556declare trans_on_Le [simp] 557 558lemma trans_Le: "trans(Le)" 559apply (unfold trans_def, auto) 560apply (blast intro: le_trans) 561done 562declare trans_Le [simp] 563 564lemma part_order_Le: "part_order(nat,Le)" 565by (unfold part_order_def, auto) 566declare part_order_Le [simp] 567 568lemma pfixLe_refl: "x \<in> list(nat) ==> x pfixLe x" 569by (blast intro: refl_gen_prefix [THEN reflD] refl_Le) 570declare pfixLe_refl [simp] 571 572lemma pfixLe_trans: "[| x pfixLe y; y pfixLe z |] ==> x pfixLe z" 573by (blast intro: trans_gen_prefix [THEN transD] trans_Le) 574 575lemma pfixLe_antisym: "[| x pfixLe y; y pfixLe x |] ==> x = y" 576by (blast intro: antisym_gen_prefix [THEN antisymE] antisym_Le) 577 578 579lemma prefix_imp_pfixLe: 580"<xs,ys>:prefix(nat)==> xs pfixLe ys" 581 582apply (unfold prefix_def) 583apply (rule gen_prefix_mono [THEN subsetD], auto) 584done 585 586lemma refl_Ge: "refl(nat, Ge)" 587by (unfold refl_def Ge_def, auto) 588declare refl_Ge [iff] 589 590lemma antisym_Ge: "antisym(Ge)" 591apply (unfold antisym_def Ge_def) 592apply (auto intro: le_anti_sym) 593done 594declare antisym_Ge [iff] 595 596lemma trans_Ge: "trans(Ge)" 597apply (unfold trans_def Ge_def) 598apply (auto intro: le_trans) 599done 600declare trans_Ge [iff] 601 602lemma pfixGe_refl: "x \<in> list(nat) ==> x pfixGe x" 603by (blast intro: refl_gen_prefix [THEN reflD]) 604declare pfixGe_refl [simp] 605 606lemma pfixGe_trans: "[| x pfixGe y; y pfixGe z |] ==> x pfixGe z" 607by (blast intro: trans_gen_prefix [THEN transD]) 608 609lemma pfixGe_antisym: "[| x pfixGe y; y pfixGe x |] ==> x = y" 610by (blast intro: antisym_gen_prefix [THEN antisymE]) 611 612lemma prefix_imp_pfixGe: 613 "<xs,ys>:prefix(nat) ==> xs pfixGe ys" 614apply (unfold prefix_def Ge_def) 615apply (rule gen_prefix_mono [THEN subsetD], auto) 616done 617(* Added by Sidi \<in> prefix and take *) 618 619lemma prefix_imp_take: 620"<xs, ys> \<in> prefix(A) ==> xs = take(length(xs), ys)" 621 622apply (unfold prefix_def) 623apply (erule gen_prefix.induct) 624apply (subgoal_tac [3] "length (xs) :nat") 625apply (auto dest: gen_prefix.dom_subset [THEN subsetD] simp add: length_type) 626apply (frule gen_prefix.dom_subset [THEN subsetD]) 627apply (frule gen_prefix_length_le) 628apply (auto simp add: take_append) 629apply (subgoal_tac "length (xs) #- length (ys) =0") 630apply (simp_all (no_asm_simp) add: diff_is_0_iff) 631done 632 633lemma prefix_length_equal: "[|<xs,ys> \<in> prefix(A); length(xs)=length(ys)|] ==> xs = ys" 634apply (cut_tac A = A in prefix_type) 635apply (drule subsetD, auto) 636apply (drule prefix_imp_take) 637apply (erule trans, simp) 638done 639 640lemma prefix_length_le_equal: "[|<xs,ys> \<in> prefix(A); length(ys) \<le> length(xs)|] ==> xs = ys" 641by (blast intro: prefix_length_equal le_anti_sym prefix_length_le) 642 643lemma take_prefix [rule_format]: "xs \<in> list(A) ==> \<forall>n \<in> nat. <take(n, xs), xs> \<in> prefix(A)" 644apply (unfold prefix_def) 645apply (erule list.induct, simp, clarify) 646apply (erule natE, auto) 647done 648 649lemma prefix_take_iff: "<xs,ys> \<in> prefix(A) \<longleftrightarrow> (xs=take(length(xs), ys) & xs \<in> list(A) & ys \<in> list(A))" 650apply (rule iffI) 651apply (frule prefix_type [THEN subsetD]) 652apply (blast intro: prefix_imp_take, clarify) 653apply (erule ssubst) 654apply (blast intro: take_prefix length_type) 655done 656 657lemma prefix_imp_nth: "[| <xs,ys> \<in> prefix(A); i < length(xs)|] ==> nth(i,xs) = nth(i,ys)" 658by (auto dest!: gen_prefix_imp_nth simp add: prefix_def) 659 660lemma nth_imp_prefix: 661 "[|xs \<in> list(A); ys \<in> list(A); length(xs) \<le> length(ys); 662 !!i. i < length(xs) ==> nth(i, xs) = nth(i,ys)|] 663 ==> <xs,ys> \<in> prefix(A)" 664apply (auto simp add: prefix_def nth_imp_gen_prefix) 665apply (auto intro!: nth_imp_gen_prefix simp add: prefix_def) 666apply (blast intro: nth_type lt_trans2) 667done 668 669 670lemma length_le_prefix_imp_prefix: "[|length(xs) \<le> length(ys); 671 <xs,zs> \<in> prefix(A); <ys,zs> \<in> prefix(A)|] ==> <xs,ys> \<in> prefix(A)" 672apply (cut_tac A = A in prefix_type) 673apply (rule nth_imp_prefix, blast, blast) 674 apply assumption 675apply (rule_tac b = "nth (i,zs)" in trans) 676 apply (blast intro: prefix_imp_nth) 677apply (blast intro: sym prefix_imp_nth prefix_length_le lt_trans2) 678done 679 680end 681