# HG changeset patch # User wenzelm # Date 1346671192 -7200 # Node ID 7b6beb7e99c1c3620e37b9cf495fd08aaeb9f5e7 # Parent d2ed455fa3d2a9ee82dc96ba4952f7f7eea30343# Parent fdc301f592c439475485aac963121cf742474a29 merge, resolving trivial conflict; diff -r d2ed455fa3d2 -r 7b6beb7e99c1 src/HOL/Codatatype/BNF_Library.thy --- a/src/HOL/Codatatype/BNF_Library.thy Mon Sep 03 11:54:21 2012 +0200 +++ b/src/HOL/Codatatype/BNF_Library.thy Mon Sep 03 13:19:52 2012 +0200 @@ -8,7 +8,9 @@ header {* Library for Bounded Natural Functors *} theory BNF_Library -imports "../Ordinals_and_Cardinals/Cardinal_Arithmetic" "~~/src/HOL/Library/List_Prefix" +imports + "../Ordinals_and_Cardinals/Cardinal_Arithmetic" + "~~/src/HOL/Library/Prefix_Order" Equiv_Relations_More begin @@ -634,7 +636,7 @@ shows "PROP P x y" by (rule `(\x y. PROP P x y)`) -(*Extended List_Prefix*) +(*Extended Sublist*) definition prefCl where "prefCl Kl = (\ kl1 kl2. kl1 \ kl2 \ kl2 \ Kl \ kl1 \ Kl)" diff -r d2ed455fa3d2 -r 7b6beb7e99c1 src/HOL/Codatatype/Examples/TreeFI.thy --- a/src/HOL/Codatatype/Examples/TreeFI.thy Mon Sep 03 11:54:21 2012 +0200 +++ b/src/HOL/Codatatype/Examples/TreeFI.thy Mon Sep 03 13:19:52 2012 +0200 @@ -12,6 +12,8 @@ imports ListF begin +hide_const (open) Sublist.sub + codata_raw treeFI: 'tree = "'a \ 'tree listF" lemma treeFIBNF_listF_set[simp]: "treeFIBNF_set2 (i, xs) = listF_set xs" diff -r d2ed455fa3d2 -r 7b6beb7e99c1 src/HOL/Codatatype/Examples/TreeFsetI.thy --- a/src/HOL/Codatatype/Examples/TreeFsetI.thy Mon Sep 03 11:54:21 2012 +0200 +++ b/src/HOL/Codatatype/Examples/TreeFsetI.thy Mon Sep 03 13:19:52 2012 +0200 @@ -12,6 +12,8 @@ imports "../Codatatype" begin +hide_const (open) Sublist.sub + definition pair_fun (infixr "\" 50) where "f \ g \ \x. (f x, g x)" diff -r d2ed455fa3d2 -r 7b6beb7e99c1 src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML diff -r d2ed455fa3d2 -r 7b6beb7e99c1 src/HOL/Codegenerator_Test/Candidates.thy --- a/src/HOL/Codegenerator_Test/Candidates.thy Mon Sep 03 11:54:21 2012 +0200 +++ b/src/HOL/Codegenerator_Test/Candidates.thy Mon Sep 03 13:19:52 2012 +0200 @@ -7,7 +7,7 @@ imports Complex_Main Library - "~~/src/HOL/Library/List_Prefix" + "~~/src/HOL/Library/Sublist" "~~/src/HOL/Number_Theory/Primes" "~~/src/HOL/ex/Records" begin diff -r d2ed455fa3d2 -r 7b6beb7e99c1 src/HOL/Library/List_Prefix.thy --- a/src/HOL/Library/List_Prefix.thy Mon Sep 03 11:54:21 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,382 +0,0 @@ -(* Title: HOL/Library/List_Prefix.thy - Author: Tobias Nipkow and Markus Wenzel, TU Muenchen -*) - -header {* List prefixes and postfixes *} - -theory List_Prefix -imports List Main -begin - -subsection {* Prefix order on lists *} - -instantiation list :: (type) "{order, bot}" -begin - -definition - prefix_def: "xs \ ys \ (\zs. ys = xs @ zs)" - -definition - strict_prefix_def: "xs < ys \ xs \ ys \ xs \ (ys::'a list)" - -definition - "bot = []" - -instance proof -qed (auto simp add: prefix_def strict_prefix_def bot_list_def) - -end - -lemma prefixI [intro?]: "ys = xs @ zs ==> xs \ ys" - unfolding prefix_def by blast - -lemma prefixE [elim?]: - assumes "xs \ ys" - obtains zs where "ys = xs @ zs" - using assms unfolding prefix_def by blast - -lemma strict_prefixI' [intro?]: "ys = xs @ z # zs ==> xs < ys" - unfolding strict_prefix_def prefix_def by blast - -lemma strict_prefixE' [elim?]: - assumes "xs < ys" - obtains z zs where "ys = xs @ z # zs" -proof - - from `xs < ys` obtain us where "ys = xs @ us" and "xs \ ys" - unfolding strict_prefix_def prefix_def by blast - with that show ?thesis by (auto simp add: neq_Nil_conv) -qed - -lemma strict_prefixI [intro?]: "xs \ ys ==> xs \ ys ==> xs < (ys::'a list)" - unfolding strict_prefix_def by blast - -lemma strict_prefixE [elim?]: - fixes xs ys :: "'a list" - assumes "xs < ys" - obtains "xs \ ys" and "xs \ ys" - using assms unfolding strict_prefix_def by blast - - -subsection {* Basic properties of prefixes *} - -theorem Nil_prefix [iff]: "[] \ xs" - by (simp add: prefix_def) - -theorem prefix_Nil [simp]: "(xs \ []) = (xs = [])" - by (induct xs) (simp_all add: prefix_def) - -lemma prefix_snoc [simp]: "(xs \ ys @ [y]) = (xs = ys @ [y] \ xs \ ys)" -proof - assume "xs \ ys @ [y]" - then obtain zs where zs: "ys @ [y] = xs @ zs" .. - show "xs = ys @ [y] \ xs \ ys" - by (metis append_Nil2 butlast_append butlast_snoc prefixI zs) -next - assume "xs = ys @ [y] \ xs \ ys" - then show "xs \ ys @ [y]" - by (metis order_eq_iff order_trans prefixI) -qed - -lemma Cons_prefix_Cons [simp]: "(x # xs \ y # ys) = (x = y \ xs \ ys)" - by (auto simp add: prefix_def) - -lemma less_eq_list_code [code]: - "([]\'a\{equal, ord} list) \ xs \ True" - "(x\'a\{equal, ord}) # xs \ [] \ False" - "(x\'a\{equal, ord}) # xs \ y # ys \ x = y \ xs \ ys" - by simp_all - -lemma same_prefix_prefix [simp]: "(xs @ ys \ xs @ zs) = (ys \ zs)" - by (induct xs) simp_all - -lemma same_prefix_nil [iff]: "(xs @ ys \ xs) = (ys = [])" - by (metis append_Nil2 append_self_conv order_eq_iff prefixI) - -lemma prefix_prefix [simp]: "xs \ ys ==> xs \ ys @ zs" - by (metis order_le_less_trans prefixI strict_prefixE strict_prefixI) - -lemma append_prefixD: "xs @ ys \ zs \ xs \ zs" - by (auto simp add: prefix_def) - -theorem prefix_Cons: "(xs \ y # ys) = (xs = [] \ (\zs. xs = y # zs \ zs \ ys))" - by (cases xs) (auto simp add: prefix_def) - -theorem prefix_append: - "(xs \ ys @ zs) = (xs \ ys \ (\us. xs = ys @ us \ us \ zs))" - apply (induct zs rule: rev_induct) - apply force - apply (simp del: append_assoc add: append_assoc [symmetric]) - apply (metis append_eq_appendI) - done - -lemma append_one_prefix: - "xs \ ys ==> length xs < length ys ==> xs @ [ys ! length xs] \ ys" - unfolding prefix_def - by (metis Cons_eq_appendI append_eq_appendI append_eq_conv_conj - eq_Nil_appendI nth_drop') - -theorem prefix_length_le: "xs \ ys ==> length xs \ length ys" - by (auto simp add: prefix_def) - -lemma prefix_same_cases: - "(xs\<^isub>1::'a list) \ ys \ xs\<^isub>2 \ ys \ xs\<^isub>1 \ xs\<^isub>2 \ xs\<^isub>2 \ xs\<^isub>1" - unfolding prefix_def by (metis append_eq_append_conv2) - -lemma set_mono_prefix: "xs \ ys \ set xs \ set ys" - by (auto simp add: prefix_def) - -lemma take_is_prefix: "take n xs \ xs" - unfolding prefix_def by (metis append_take_drop_id) - -lemma map_prefixI: "xs \ ys \ map f xs \ map f ys" - by (auto simp: prefix_def) - -lemma prefix_length_less: "xs < ys \ length xs < length ys" - by (auto simp: strict_prefix_def prefix_def) - -lemma strict_prefix_simps [simp, code]: - "xs < [] \ False" - "[] < x # xs \ True" - "x # xs < y # ys \ x = y \ xs < ys" - by (simp_all add: strict_prefix_def cong: conj_cong) - -lemma take_strict_prefix: "xs < ys \ take n xs < ys" - apply (induct n arbitrary: xs ys) - apply (case_tac ys, simp_all)[1] - apply (metis order_less_trans strict_prefixI take_is_prefix) - done - -lemma not_prefix_cases: - assumes pfx: "\ ps \ ls" - obtains - (c1) "ps \ []" and "ls = []" - | (c2) a as x xs where "ps = a#as" and "ls = x#xs" and "x = a" and "\ as \ xs" - | (c3) a as x xs where "ps = a#as" and "ls = x#xs" and "x \ a" -proof (cases ps) - case Nil then show ?thesis using pfx by simp -next - case (Cons a as) - note c = `ps = a#as` - show ?thesis - proof (cases ls) - case Nil then show ?thesis by (metis append_Nil2 pfx c1 same_prefix_nil) - next - case (Cons x xs) - show ?thesis - proof (cases "x = a") - case True - have "\ as \ xs" using pfx c Cons True by simp - with c Cons True show ?thesis by (rule c2) - next - case False - with c Cons show ?thesis by (rule c3) - qed - qed -qed - -lemma not_prefix_induct [consumes 1, case_names Nil Neq Eq]: - assumes np: "\ ps \ ls" - and base: "\x xs. P (x#xs) []" - and r1: "\x xs y ys. x \ y \ P (x#xs) (y#ys)" - and r2: "\x xs y ys. \ x = y; \ xs \ ys; P xs ys \ \ P (x#xs) (y#ys)" - shows "P ps ls" using np -proof (induct ls arbitrary: ps) - case Nil then show ?case - by (auto simp: neq_Nil_conv elim!: not_prefix_cases intro!: base) -next - case (Cons y ys) - then have npfx: "\ ps \ (y # ys)" by simp - then obtain x xs where pv: "ps = x # xs" - by (rule not_prefix_cases) auto - show ?case by (metis Cons.hyps Cons_prefix_Cons npfx pv r1 r2) -qed - - -subsection {* Parallel lists *} - -definition - parallel :: "'a list => 'a list => bool" (infixl "\" 50) where - "(xs \ ys) = (\ xs \ ys \ \ ys \ xs)" - -lemma parallelI [intro]: "\ xs \ ys ==> \ ys \ xs ==> xs \ ys" - unfolding parallel_def by blast - -lemma parallelE [elim]: - assumes "xs \ ys" - obtains "\ xs \ ys \ \ ys \ xs" - using assms unfolding parallel_def by blast - -theorem prefix_cases: - obtains "xs \ ys" | "ys < xs" | "xs \ ys" - unfolding parallel_def strict_prefix_def by blast - -theorem parallel_decomp: - "xs \ ys ==> \as b bs c cs. b \ c \ xs = as @ b # bs \ ys = as @ c # cs" -proof (induct xs rule: rev_induct) - case Nil - then have False by auto - then show ?case .. -next - case (snoc x xs) - show ?case - proof (rule prefix_cases) - assume le: "xs \ ys" - then obtain ys' where ys: "ys = xs @ ys'" .. - show ?thesis - proof (cases ys') - assume "ys' = []" - then show ?thesis by (metis append_Nil2 parallelE prefixI snoc.prems ys) - next - fix c cs assume ys': "ys' = c # cs" - then show ?thesis - by (metis Cons_eq_appendI eq_Nil_appendI parallelE prefixI - same_prefix_prefix snoc.prems ys) - qed - next - assume "ys < xs" then have "ys \ xs @ [x]" by (simp add: strict_prefix_def) - with snoc have False by blast - then show ?thesis .. - next - assume "xs \ ys" - with snoc obtain as b bs c cs where neq: "(b::'a) \ c" - and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs" - by blast - from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp - with neq ys show ?thesis by blast - qed -qed - -lemma parallel_append: "a \ b \ a @ c \ b @ d" - apply (rule parallelI) - apply (erule parallelE, erule conjE, - induct rule: not_prefix_induct, simp+)+ - done - -lemma parallel_appendI: "xs \ ys \ x = xs @ xs' \ y = ys @ ys' \ x \ y" - by (simp add: parallel_append) - -lemma parallel_commute: "a \ b \ b \ a" - unfolding parallel_def by auto - - -subsection {* Postfix order on lists *} - -definition - postfix :: "'a list => 'a list => bool" ("(_/ >>= _)" [51, 50] 50) where - "(xs >>= ys) = (\zs. xs = zs @ ys)" - -lemma postfixI [intro?]: "xs = zs @ ys ==> xs >>= ys" - unfolding postfix_def by blast - -lemma postfixE [elim?]: - assumes "xs >>= ys" - obtains zs where "xs = zs @ ys" - using assms unfolding postfix_def by blast - -lemma postfix_refl [iff]: "xs >>= xs" - by (auto simp add: postfix_def) -lemma postfix_trans: "\xs >>= ys; ys >>= zs\ \ xs >>= zs" - by (auto simp add: postfix_def) -lemma postfix_antisym: "\xs >>= ys; ys >>= xs\ \ xs = ys" - by (auto simp add: postfix_def) - -lemma Nil_postfix [iff]: "xs >>= []" - by (simp add: postfix_def) -lemma postfix_Nil [simp]: "([] >>= xs) = (xs = [])" - by (auto simp add: postfix_def) - -lemma postfix_ConsI: "xs >>= ys \ x#xs >>= ys" - by (auto simp add: postfix_def) -lemma postfix_ConsD: "xs >>= y#ys \ xs >>= ys" - by (auto simp add: postfix_def) - -lemma postfix_appendI: "xs >>= ys \ zs @ xs >>= ys" - by (auto simp add: postfix_def) -lemma postfix_appendD: "xs >>= zs @ ys \ xs >>= ys" - by (auto simp add: postfix_def) - -lemma postfix_is_subset: "xs >>= ys ==> set ys \ set xs" -proof - - assume "xs >>= ys" - then obtain zs where "xs = zs @ ys" .. - then show ?thesis by (induct zs) auto -qed - -lemma postfix_ConsD2: "x#xs >>= y#ys ==> xs >>= ys" -proof - - assume "x#xs >>= y#ys" - then obtain zs where "x#xs = zs @ y#ys" .. - then show ?thesis - by (induct zs) (auto intro!: postfix_appendI postfix_ConsI) -qed - -lemma postfix_to_prefix [code]: "xs >>= ys \ rev ys \ rev xs" -proof - assume "xs >>= ys" - then obtain zs where "xs = zs @ ys" .. - then have "rev xs = rev ys @ rev zs" by simp - then show "rev ys <= rev xs" .. -next - assume "rev ys <= rev xs" - then obtain zs where "rev xs = rev ys @ zs" .. - then have "rev (rev xs) = rev zs @ rev (rev ys)" by simp - then have "xs = rev zs @ ys" by simp - then show "xs >>= ys" .. -qed - -lemma distinct_postfix: "distinct xs \ xs >>= ys \ distinct ys" - by (clarsimp elim!: postfixE) - -lemma postfix_map: "xs >>= ys \ map f xs >>= map f ys" - by (auto elim!: postfixE intro: postfixI) - -lemma postfix_drop: "as >>= drop n as" - unfolding postfix_def - apply (rule exI [where x = "take n as"]) - apply simp - done - -lemma postfix_take: "xs >>= ys \ xs = take (length xs - length ys) xs @ ys" - by (clarsimp elim!: postfixE) - -lemma parallelD1: "x \ y \ \ x \ y" - by blast - -lemma parallelD2: "x \ y \ \ y \ x" - by blast - -lemma parallel_Nil1 [simp]: "\ x \ []" - unfolding parallel_def by simp - -lemma parallel_Nil2 [simp]: "\ [] \ x" - unfolding parallel_def by simp - -lemma Cons_parallelI1: "a \ b \ a # as \ b # bs" - by auto - -lemma Cons_parallelI2: "\ a = b; as \ bs \ \ a # as \ b # bs" - by (metis Cons_prefix_Cons parallelE parallelI) - -lemma not_equal_is_parallel: - assumes neq: "xs \ ys" - and len: "length xs = length ys" - shows "xs \ ys" - using len neq -proof (induct rule: list_induct2) - case Nil - then show ?case by simp -next - case (Cons a as b bs) - have ih: "as \ bs \ as \ bs" by fact - show ?case - proof (cases "a = b") - case True - then have "as \ bs" using Cons by simp - then show ?thesis by (rule Cons_parallelI2 [OF True ih]) - next - case False - then show ?thesis by (rule Cons_parallelI1) - qed -qed - -end diff -r d2ed455fa3d2 -r 7b6beb7e99c1 src/HOL/Library/Prefix_Order.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Prefix_Order.thy Mon Sep 03 13:19:52 2012 +0200 @@ -0,0 +1,40 @@ +(* Title: HOL/Library/Sublist.thy + Author: Tobias Nipkow and Markus Wenzel, TU Muenchen +*) + +header {* Prefix order on lists as order class instance *} + +theory Prefix_Order +imports Sublist +begin + +instantiation list :: (type) order +begin + +definition "(xs::'a list) \ ys \ prefixeq xs ys" +definition "(xs::'a list) < ys \ xs \ ys \ \ (ys \ xs)" + +instance by (default, unfold less_eq_list_def less_list_def) auto + +end + +lemmas prefixI [intro?] = prefixeqI [folded less_eq_list_def] +lemmas prefixE [elim?] = prefixeqE [folded less_eq_list_def] +lemmas strict_prefixI' [intro?] = prefixI' [folded less_list_def] +lemmas strict_prefixE' [elim?] = prefixE' [folded less_list_def] +lemmas strict_prefixI [intro?] = prefixI [folded less_list_def] +lemmas strict_prefixE [elim?] = prefixE [folded less_list_def] +theorems Nil_prefix [iff] = Nil_prefixeq [folded less_eq_list_def] +theorems prefix_Nil [simp] = prefixeq_Nil [folded less_eq_list_def] +lemmas prefix_snoc [simp] = prefixeq_snoc [folded less_eq_list_def] +lemmas Cons_prefix_Cons [simp] = Cons_prefixeq_Cons [folded less_eq_list_def] +lemmas same_prefix_prefix [simp] = same_prefixeq_prefixeq [folded less_eq_list_def] +lemmas same_prefix_nil [iff] = same_prefixeq_nil [folded less_eq_list_def] +lemmas prefix_prefix [simp] = prefixeq_prefixeq [folded less_eq_list_def] +theorems prefix_Cons = prefixeq_Cons [folded less_eq_list_def] +theorems prefix_length_le = prefixeq_length_le [folded less_eq_list_def] +lemmas strict_prefix_simps [simp, code] = prefix_simps [folded less_list_def] +lemmas not_prefix_induct [consumes 1, case_names Nil Neq Eq] = + not_prefixeq_induct [folded less_eq_list_def] + +end diff -r d2ed455fa3d2 -r 7b6beb7e99c1 src/HOL/Library/Sublist.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Sublist.thy Mon Sep 03 13:19:52 2012 +0200 @@ -0,0 +1,692 @@ +(* Title: HOL/Library/Sublist.thy + Author: Tobias Nipkow and Markus Wenzel, TU Muenchen + Author: Christian Sternagel, JAIST +*) + +header {* List prefixes, suffixes, and embedding*} + +theory Sublist +imports Main +begin + +subsection {* Prefix order on lists *} + +definition prefixeq :: "'a list => 'a list => bool" where + "prefixeq xs ys \ (\zs. ys = xs @ zs)" + +definition prefix :: "'a list => 'a list => bool" where + "prefix xs ys \ prefixeq xs ys \ xs \ ys" + +interpretation prefix_order: order prefixeq prefix + by default (auto simp: prefixeq_def prefix_def) + +interpretation prefix_bot: bot prefixeq prefix Nil + by default (simp add: prefixeq_def) + +lemma prefixeqI [intro?]: "ys = xs @ zs ==> prefixeq xs ys" + unfolding prefixeq_def by blast + +lemma prefixeqE [elim?]: + assumes "prefixeq xs ys" + obtains zs where "ys = xs @ zs" + using assms unfolding prefixeq_def by blast + +lemma prefixI' [intro?]: "ys = xs @ z # zs ==> prefix xs ys" + unfolding prefix_def prefixeq_def by blast + +lemma prefixE' [elim?]: + assumes "prefix xs ys" + obtains z zs where "ys = xs @ z # zs" +proof - + from `prefix xs ys` obtain us where "ys = xs @ us" and "xs \ ys" + unfolding prefix_def prefixeq_def by blast + with that show ?thesis by (auto simp add: neq_Nil_conv) +qed + +lemma prefixI [intro?]: "prefixeq xs ys ==> xs \ ys ==> prefix xs ys" + unfolding prefix_def by blast + +lemma prefixE [elim?]: + fixes xs ys :: "'a list" + assumes "prefix xs ys" + obtains "prefixeq xs ys" and "xs \ ys" + using assms unfolding prefix_def by blast + + +subsection {* Basic properties of prefixes *} + +theorem Nil_prefixeq [iff]: "prefixeq [] xs" + by (simp add: prefixeq_def) + +theorem prefixeq_Nil [simp]: "(prefixeq xs []) = (xs = [])" + by (induct xs) (simp_all add: prefixeq_def) + +lemma prefixeq_snoc [simp]: "prefixeq xs (ys @ [y]) \ xs = ys @ [y] \ prefixeq xs ys" +proof + assume "prefixeq xs (ys @ [y])" + then obtain zs where zs: "ys @ [y] = xs @ zs" .. + show "xs = ys @ [y] \ prefixeq xs ys" + by (metis append_Nil2 butlast_append butlast_snoc prefixeqI zs) +next + assume "xs = ys @ [y] \ prefixeq xs ys" + then show "prefixeq xs (ys @ [y])" + by (metis prefix_order.eq_iff prefix_order.order_trans prefixeqI) +qed + +lemma Cons_prefixeq_Cons [simp]: "prefixeq (x # xs) (y # ys) = (x = y \ prefixeq xs ys)" + by (auto simp add: prefixeq_def) + +lemma prefixeq_code [code]: + "prefixeq [] xs \ True" + "prefixeq (x # xs) [] \ False" + "prefixeq (x # xs) (y # ys) \ x = y \ prefixeq xs ys" + by simp_all + +lemma same_prefixeq_prefixeq [simp]: "prefixeq (xs @ ys) (xs @ zs) = prefixeq ys zs" + by (induct xs) simp_all + +lemma same_prefixeq_nil [iff]: "prefixeq (xs @ ys) xs = (ys = [])" + by (metis append_Nil2 append_self_conv prefix_order.eq_iff prefixeqI) + +lemma prefixeq_prefixeq [simp]: "prefixeq xs ys ==> prefixeq xs (ys @ zs)" + by (metis prefix_order.le_less_trans prefixeqI prefixE prefixI) + +lemma append_prefixeqD: "prefixeq (xs @ ys) zs \ prefixeq xs zs" + by (auto simp add: prefixeq_def) + +theorem prefixeq_Cons: "prefixeq xs (y # ys) = (xs = [] \ (\zs. xs = y # zs \ prefixeq zs ys))" + by (cases xs) (auto simp add: prefixeq_def) + +theorem prefixeq_append: + "prefixeq xs (ys @ zs) = (prefixeq xs ys \ (\us. xs = ys @ us \ prefixeq us zs))" + apply (induct zs rule: rev_induct) + apply force + apply (simp del: append_assoc add: append_assoc [symmetric]) + apply (metis append_eq_appendI) + done + +lemma append_one_prefixeq: + "prefixeq xs ys ==> length xs < length ys ==> prefixeq (xs @ [ys ! length xs]) ys" + unfolding prefixeq_def + by (metis Cons_eq_appendI append_eq_appendI append_eq_conv_conj + eq_Nil_appendI nth_drop') + +theorem prefixeq_length_le: "prefixeq xs ys ==> length xs \ length ys" + by (auto simp add: prefixeq_def) + +lemma prefixeq_same_cases: + "prefixeq (xs\<^isub>1::'a list) ys \ prefixeq xs\<^isub>2 ys \ prefixeq xs\<^isub>1 xs\<^isub>2 \ prefixeq xs\<^isub>2 xs\<^isub>1" + unfolding prefixeq_def by (metis append_eq_append_conv2) + +lemma set_mono_prefixeq: "prefixeq xs ys \ set xs \ set ys" + by (auto simp add: prefixeq_def) + +lemma take_is_prefixeq: "prefixeq (take n xs) xs" + unfolding prefixeq_def by (metis append_take_drop_id) + +lemma map_prefixeqI: "prefixeq xs ys \ prefixeq (map f xs) (map f ys)" + by (auto simp: prefixeq_def) + +lemma prefixeq_length_less: "prefix xs ys \ length xs < length ys" + by (auto simp: prefix_def prefixeq_def) + +lemma prefix_simps [simp, code]: + "prefix xs [] \ False" + "prefix [] (x # xs) \ True" + "prefix (x # xs) (y # ys) \ x = y \ prefix xs ys" + by (simp_all add: prefix_def cong: conj_cong) + +lemma take_prefix: "prefix xs ys \ prefix (take n xs) ys" + apply (induct n arbitrary: xs ys) + apply (case_tac ys, simp_all)[1] + apply (metis prefix_order.less_trans prefixI take_is_prefixeq) + done + +lemma not_prefixeq_cases: + assumes pfx: "\ prefixeq ps ls" + obtains + (c1) "ps \ []" and "ls = []" + | (c2) a as x xs where "ps = a#as" and "ls = x#xs" and "x = a" and "\ prefixeq as xs" + | (c3) a as x xs where "ps = a#as" and "ls = x#xs" and "x \ a" +proof (cases ps) + case Nil then show ?thesis using pfx by simp +next + case (Cons a as) + note c = `ps = a#as` + show ?thesis + proof (cases ls) + case Nil then show ?thesis by (metis append_Nil2 pfx c1 same_prefixeq_nil) + next + case (Cons x xs) + show ?thesis + proof (cases "x = a") + case True + have "\ prefixeq as xs" using pfx c Cons True by simp + with c Cons True show ?thesis by (rule c2) + next + case False + with c Cons show ?thesis by (rule c3) + qed + qed +qed + +lemma not_prefixeq_induct [consumes 1, case_names Nil Neq Eq]: + assumes np: "\ prefixeq ps ls" + and base: "\x xs. P (x#xs) []" + and r1: "\x xs y ys. x \ y \ P (x#xs) (y#ys)" + and r2: "\x xs y ys. \ x = y; \ prefixeq xs ys; P xs ys \ \ P (x#xs) (y#ys)" + shows "P ps ls" using np +proof (induct ls arbitrary: ps) + case Nil then show ?case + by (auto simp: neq_Nil_conv elim!: not_prefixeq_cases intro!: base) +next + case (Cons y ys) + then have npfx: "\ prefixeq ps (y # ys)" by simp + then obtain x xs where pv: "ps = x # xs" + by (rule not_prefixeq_cases) auto + show ?case by (metis Cons.hyps Cons_prefixeq_Cons npfx pv r1 r2) +qed + + +subsection {* Parallel lists *} + +definition + parallel :: "'a list => 'a list => bool" (infixl "\" 50) where + "(xs \ ys) = (\ prefixeq xs ys \ \ prefixeq ys xs)" + +lemma parallelI [intro]: "\ prefixeq xs ys ==> \ prefixeq ys xs ==> xs \ ys" + unfolding parallel_def by blast + +lemma parallelE [elim]: + assumes "xs \ ys" + obtains "\ prefixeq xs ys \ \ prefixeq ys xs" + using assms unfolding parallel_def by blast + +theorem prefixeq_cases: + obtains "prefixeq xs ys" | "prefix ys xs" | "xs \ ys" + unfolding parallel_def prefix_def by blast + +theorem parallel_decomp: + "xs \ ys ==> \as b bs c cs. b \ c \ xs = as @ b # bs \ ys = as @ c # cs" +proof (induct xs rule: rev_induct) + case Nil + then have False by auto + then show ?case .. +next + case (snoc x xs) + show ?case + proof (rule prefixeq_cases) + assume le: "prefixeq xs ys" + then obtain ys' where ys: "ys = xs @ ys'" .. + show ?thesis + proof (cases ys') + assume "ys' = []" + then show ?thesis by (metis append_Nil2 parallelE prefixeqI snoc.prems ys) + next + fix c cs assume ys': "ys' = c # cs" + then show ?thesis + by (metis Cons_eq_appendI eq_Nil_appendI parallelE prefixeqI + same_prefixeq_prefixeq snoc.prems ys) + qed + next + assume "prefix ys xs" then have "prefixeq ys (xs @ [x])" by (simp add: prefix_def) + with snoc have False by blast + then show ?thesis .. + next + assume "xs \ ys" + with snoc obtain as b bs c cs where neq: "(b::'a) \ c" + and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs" + by blast + from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp + with neq ys show ?thesis by blast + qed +qed + +lemma parallel_append: "a \ b \ a @ c \ b @ d" + apply (rule parallelI) + apply (erule parallelE, erule conjE, + induct rule: not_prefixeq_induct, simp+)+ + done + +lemma parallel_appendI: "xs \ ys \ x = xs @ xs' \ y = ys @ ys' \ x \ y" + by (simp add: parallel_append) + +lemma parallel_commute: "a \ b \ b \ a" + unfolding parallel_def by auto + + +subsection {* Suffix order on lists *} + +definition + suffixeq :: "'a list => 'a list => bool" where + "suffixeq xs ys = (\zs. ys = zs @ xs)" + +definition suffix :: "'a list \ 'a list \ bool" where + "suffix xs ys \ \us. ys = us @ xs \ us \ []" + +lemma suffix_imp_suffixeq: + "suffix xs ys \ suffixeq xs ys" + by (auto simp: suffixeq_def suffix_def) + +lemma suffixeqI [intro?]: "ys = zs @ xs ==> suffixeq xs ys" + unfolding suffixeq_def by blast + +lemma suffixeqE [elim?]: + assumes "suffixeq xs ys" + obtains zs where "ys = zs @ xs" + using assms unfolding suffixeq_def by blast + +lemma suffixeq_refl [iff]: "suffixeq xs xs" + by (auto simp add: suffixeq_def) +lemma suffix_trans: + "suffix xs ys \ suffix ys zs \ suffix xs zs" + by (auto simp: suffix_def) +lemma suffixeq_trans: "\suffixeq xs ys; suffixeq ys zs\ \ suffixeq xs zs" + by (auto simp add: suffixeq_def) +lemma suffixeq_antisym: "\suffixeq xs ys; suffixeq ys xs\ \ xs = ys" + by (auto simp add: suffixeq_def) + +lemma suffixeq_tl [simp]: "suffixeq (tl xs) xs" + by (induct xs) (auto simp: suffixeq_def) + +lemma suffix_tl [simp]: "xs \ [] \ suffix (tl xs) xs" + by (induct xs) (auto simp: suffix_def) + +lemma Nil_suffixeq [iff]: "suffixeq [] xs" + by (simp add: suffixeq_def) +lemma suffixeq_Nil [simp]: "(suffixeq xs []) = (xs = [])" + by (auto simp add: suffixeq_def) + +lemma suffixeq_ConsI: "suffixeq xs ys \ suffixeq xs (y#ys)" + by (auto simp add: suffixeq_def) +lemma suffixeq_ConsD: "suffixeq (x#xs) ys \ suffixeq xs ys" + by (auto simp add: suffixeq_def) + +lemma suffixeq_appendI: "suffixeq xs ys \ suffixeq xs (zs @ ys)" + by (auto simp add: suffixeq_def) +lemma suffixeq_appendD: "suffixeq (zs @ xs) ys \ suffixeq xs ys" + by (auto simp add: suffixeq_def) + +lemma suffix_set_subset: + "suffix xs ys \ set xs \ set ys" by (auto simp: suffix_def) + +lemma suffixeq_set_subset: + "suffixeq xs ys \ set xs \ set ys" by (auto simp: suffixeq_def) + +lemma suffixeq_ConsD2: "suffixeq (x#xs) (y#ys) ==> suffixeq xs ys" +proof - + assume "suffixeq (x#xs) (y#ys)" + then obtain zs where "y#ys = zs @ x#xs" .. + then show ?thesis + by (induct zs) (auto intro!: suffixeq_appendI suffixeq_ConsI) +qed + +lemma suffixeq_to_prefixeq [code]: "suffixeq xs ys \ prefixeq (rev xs) (rev ys)" +proof + assume "suffixeq xs ys" + then obtain zs where "ys = zs @ xs" .. + then have "rev ys = rev xs @ rev zs" by simp + then show "prefixeq (rev xs) (rev ys)" .. +next + assume "prefixeq (rev xs) (rev ys)" + then obtain zs where "rev ys = rev xs @ zs" .. + then have "rev (rev ys) = rev zs @ rev (rev xs)" by simp + then have "ys = rev zs @ xs" by simp + then show "suffixeq xs ys" .. +qed + +lemma distinct_suffixeq: "distinct ys \ suffixeq xs ys \ distinct xs" + by (clarsimp elim!: suffixeqE) + +lemma suffixeq_map: "suffixeq xs ys \ suffixeq (map f xs) (map f ys)" + by (auto elim!: suffixeqE intro: suffixeqI) + +lemma suffixeq_drop: "suffixeq (drop n as) as" + unfolding suffixeq_def + apply (rule exI [where x = "take n as"]) + apply simp + done + +lemma suffixeq_take: "suffixeq xs ys \ ys = take (length ys - length xs) ys @ xs" + by (clarsimp elim!: suffixeqE) + +lemma suffixeq_suffix_reflclp_conv: + "suffixeq = suffix\<^sup>=\<^sup>=" +proof (intro ext iffI) + fix xs ys :: "'a list" + assume "suffixeq xs ys" + show "suffix\<^sup>=\<^sup>= xs ys" + proof + assume "xs \ ys" + with `suffixeq xs ys` show "suffix xs ys" by (auto simp: suffixeq_def suffix_def) + qed +next + fix xs ys :: "'a list" + assume "suffix\<^sup>=\<^sup>= xs ys" + thus "suffixeq xs ys" + proof + assume "suffix xs ys" thus "suffixeq xs ys" by (rule suffix_imp_suffixeq) + next + assume "xs = ys" thus "suffixeq xs ys" by (auto simp: suffixeq_def) + qed +qed + +lemma parallelD1: "x \ y \ \ prefixeq x y" + by blast + +lemma parallelD2: "x \ y \ \ prefixeq y x" + by blast + +lemma parallel_Nil1 [simp]: "\ x \ []" + unfolding parallel_def by simp + +lemma parallel_Nil2 [simp]: "\ [] \ x" + unfolding parallel_def by simp + +lemma Cons_parallelI1: "a \ b \ a # as \ b # bs" + by auto + +lemma Cons_parallelI2: "\ a = b; as \ bs \ \ a # as \ b # bs" + by (metis Cons_prefixeq_Cons parallelE parallelI) + +lemma not_equal_is_parallel: + assumes neq: "xs \ ys" + and len: "length xs = length ys" + shows "xs \ ys" + using len neq +proof (induct rule: list_induct2) + case Nil + then show ?case by simp +next + case (Cons a as b bs) + have ih: "as \ bs \ as \ bs" by fact + show ?case + proof (cases "a = b") + case True + then have "as \ bs" using Cons by simp + then show ?thesis by (rule Cons_parallelI2 [OF True ih]) + next + case False + then show ?thesis by (rule Cons_parallelI1) + qed +qed + +lemma suffix_reflclp_conv: + "suffix\<^sup>=\<^sup>= = suffixeq" + by (intro ext) (auto simp: suffixeq_def suffix_def) + +lemma suffix_lists: + "suffix xs ys \ ys \ lists A \ xs \ lists A" + unfolding suffix_def by auto + + +subsection {* Embedding on lists *} + +inductive + emb :: "('a \ 'a \ bool) \ 'a list \ 'a list \ bool" + for P :: "('a \ 'a \ bool)" +where + emb_Nil [intro, simp]: "emb P [] ys" +| emb_Cons [intro] : "emb P xs ys \ emb P xs (y#ys)" +| emb_Cons2 [intro]: "P x y \ emb P xs ys \ emb P (x#xs) (y#ys)" + +lemma emb_Nil2 [simp]: + assumes "emb P xs []" shows "xs = []" + using assms by (cases rule: emb.cases) auto + +lemma emb_Cons_Nil [simp]: + "emb P (x#xs) [] = False" +proof - + { assume "emb P (x#xs) []" + from emb_Nil2 [OF this] have False by simp + } moreover { + assume False + hence "emb P (x#xs) []" by simp + } ultimately show ?thesis by blast +qed + +lemma emb_append2 [intro]: + "emb P xs ys \ emb P xs (zs @ ys)" + by (induct zs) auto + +lemma emb_prefix [intro]: + assumes "emb P xs ys" shows "emb P xs (ys @ zs)" + using assms + by (induct arbitrary: zs) auto + +lemma emb_ConsD: + assumes "emb P (x#xs) ys" + shows "\us v vs. ys = us @ v # vs \ P x v \ emb P xs vs" +using assms +proof (induct x\"x#xs" y\"ys" arbitrary: x xs ys) + case emb_Cons thus ?case by (metis append_Cons) +next + case (emb_Cons2 x y xs ys) + thus ?case by (cases xs) (auto, blast+) +qed + +lemma emb_appendD: + assumes "emb P (xs @ ys) zs" + shows "\us vs. zs = us @ vs \ emb P xs us \ emb P ys vs" +using assms +proof (induction xs arbitrary: ys zs) + case Nil thus ?case by auto +next + case (Cons x xs) + then obtain us v vs where "zs = us @ v # vs" + and "P x v" and "emb P (xs @ ys) vs" by (auto dest: emb_ConsD) + with Cons show ?case by (metis append_Cons append_assoc emb_Cons2 emb_append2) +qed + +lemma emb_suffix: + assumes "emb P xs ys" and "suffix ys zs" + shows "emb P xs zs" + using assms(2) and emb_append2 [OF assms(1)] by (auto simp: suffix_def) + +lemma emb_suffixeq: + assumes "emb P xs ys" and "suffixeq ys zs" + shows "emb P xs zs" + using assms and emb_suffix unfolding suffixeq_suffix_reflclp_conv by auto + +lemma emb_length: "emb P xs ys \ length xs \ length ys" + by (induct rule: emb.induct) auto + +(*FIXME: move*) +definition transp_on :: "('a \ 'a \ bool) \ 'a set \ bool" where + "transp_on P A \ \a\A. \b\A. \c\A. P a b \ P b c \ P a c" +lemma transp_onI [Pure.intro]: + "(\a b c. \a \ A; b \ A; c \ A; P a b; P b c\ \ P a c) \ transp_on P A" + unfolding transp_on_def by blast + +lemma transp_on_emb: + assumes "transp_on P A" + shows "transp_on (emb P) (lists A)" +proof + fix xs ys zs + assume "emb P xs ys" and "emb P ys zs" + and "xs \ lists A" and "ys \ lists A" and "zs \ lists A" + thus "emb P xs zs" + proof (induction arbitrary: zs) + case emb_Nil show ?case by blast + next + case (emb_Cons xs ys y) + from emb_ConsD [OF `emb P (y#ys) zs`] obtain us v vs + where zs: "zs = us @ v # vs" and "P y v" and "emb P ys vs" by blast + hence "emb P ys (v#vs)" by blast + hence "emb P ys zs" unfolding zs by (rule emb_append2) + from emb_Cons.IH [OF this] and emb_Cons.prems show ?case by simp + next + case (emb_Cons2 x y xs ys) + from emb_ConsD [OF `emb P (y#ys) zs`] obtain us v vs + where zs: "zs = us @ v # vs" and "P y v" and "emb P ys vs" by blast + with emb_Cons2 have "emb P xs vs" by simp + moreover have "P x v" + proof - + from zs and `zs \ lists A` have "v \