Theory ListInf_Prefix

(*  Title:      ListInf_Prefix.thy
    Date:       Oct 2006
    Author:     David Trachtenherz
*)

header {* Prefices on finite and infinite lists *}

theory ListInf_Prefix
imports "$ISABELLE_HOME/src/HOL/Library/List_Prefix" ListInf
begin



subsection {* Additional list prefix results *}

lemma prefix_eq_prefix_take_ex: "(xs ≤ ys) = (∃n. ys \<down> n = xs)"
apply (unfold prefix_def, safe)
apply (rule_tac x="length xs" in exI, simp)
apply (rule_tac x="ys \<up> n" in exI, simp)
done

lemma prefix_take_eq_prefix_take_ex: "(ys \<down> (length xs) = xs) = (∃n. ys \<down> n = xs)"
by (fastsimp simp: min_def)

lemma prefix_eq_prefix_take: "(xs ≤ ys) = (ys \<down> (length xs) = xs)"
by (simp only: prefix_eq_prefix_take_ex prefix_take_eq_prefix_take_ex)

lemma strict_prefix_take_eq_strict_prefix_take_ex: "
  (ys \<down> (length xs) = xs ∧ xs ≠ ys) = 
  ((∃n. ys \<down> n = xs) ∧ xs ≠ ys)"
by (simp add: prefix_take_eq_prefix_take_ex)

lemma strict_prefix_eq_strict_prefix_take_ex: "(xs < ys) = ((∃n. ys \<down> n = xs) ∧ xs ≠ ys)"
by (simp add: strict_prefix_def prefix_eq_prefix_take_ex)
lemma strict_prefix_eq_strict_prefix_take: "(xs < ys) = (ys \<down> (length xs) = xs ∧ xs ≠ ys)"
by (simp only: strict_prefix_eq_strict_prefix_take_ex strict_prefix_take_eq_strict_prefix_take_ex)


 
lemma take_imp_prefix: "xs \<down> n ≤ xs"
by (rule take_is_prefix)

lemma eq_imp_prefix: "xs = (ys::'a list) ==> xs ≤ ys"
by simp

lemma le_take_imp_prefix: "a ≤ b ==> xs \<down> a ≤ xs \<down> b"
by (fastsimp simp: prefix_eq_prefix_take_ex min_def)

lemma take_prefix_imp_le: "
  [| a ≤ length xs; xs \<down> a ≤ xs \<down> b |] ==> a ≤ b"
by (drule prefix_length_le, simp)

lemma take_prefix_le_conv: "
  a ≤ length xs ==> (xs \<down> a ≤ xs \<down> b) = (a ≤ b)"
apply (rule iffI)
 apply (rule take_prefix_imp_le, assumption+)
apply (rule le_take_imp_prefix, assumption+)
done
lemma append_imp_prefix[simp, intro]: "a ≤ a @ b"
by (unfold prefix_def, blast)

lemma prefix_imp_take_eq: "
  [| n ≤ length xs; xs ≤ ys |] ==> xs \<down> n = ys \<down> n"
by (clarsimp simp: prefix_def)

lemma prefix_length_le_eq_conv: "(xs ≤ ys ∧ length ys ≤ length xs) = (xs = ys)"
apply (rule iffI)
 apply (erule conjE)
 apply (frule prefix_length_le)
 apply (simp add: prefix_eq_prefix_take)
apply simp
done

lemma take_length_prefix_conv: "
  length xs ≤ length ys ==> (ys \<down> length xs ≤ xs) = (xs ≤ ys)"
by (fastsimp simp: prefix_eq_prefix_take)

lemma append_eq_imp_take: "
  [| k ≤ length xs; length r1 = k; r1 @ r2 = xs |] ==> r1 = xs \<down> k"
by fastsimp

lemma take_the_conv: "
  xs \<down> k = (if length xs ≤ k then xs else (THE r. length r = k ∧ (∃r2. r @ r2 = xs)))"
apply (clarsimp simp: linorder_not_le)
apply (rule the1I2)
 apply (simp add: Ex1_def)
 apply (rule_tac x="xs \<down> k" in exI)
 apply (intro conjI)
   apply (simp add: min_eqR)
  apply (rule_tac x="xs \<up> k" in exI, simp)
 apply fastsimp
apply fastsimp
done


lemma prefix_refl: "xs ≤ (xs::'a list)"
by (rule order_refl)

lemma prefix_trans: "[| xs ≤ ys; (ys::'a list) ≤ zs |] ==> xs ≤ zs"
by (rule order_trans)

lemma prefix_antisym: "[| xs ≤ ys; (ys::'a list) ≤ xs |] ==> xs = ys"
by (rule order_antisym)



subsection {* Counting equal pairs *}
text {* Counting number of equal elements in two lists *}

definition
  mirror_pair :: "('a × 'b) => ('b × 'a)"
where
  "mirror_pair p ≡ (snd p, fst p)"

lemma zip_mirror[rule_format]: "
  [| i < min (length xs) (length ys);
    p1 = (zip xs ys) ! i; p2 = (zip ys xs) ! i |] ==> 
  mirror_pair p1 = p2"
by (simp add: mirror_pair_def)

definition
  equal_pair :: "('a × 'a) => bool"
where
  "equal_pair p ≡ (fst p = snd p)"

lemma mirror_pair_equal: "equal_pair (mirror_pair p) = (equal_pair p)"
by (fastsimp simp: mirror_pair_def equal_pair_def)

primrec
  equal_pair_count :: "('a × 'a) list => nat"
where
  "equal_pair_count [] = 0"
| "equal_pair_count (p # ps) = (
    if (fst p = snd p)
      then Suc (equal_pair_count ps)
      else 0)"

lemma equal_pair_count_le: "equal_pair_count xs ≤ length xs"
by (induct xs, simp_all)

lemma equal_pair_count_0: "
  fst (hd ps) ≠ snd (hd ps) ==> equal_pair_count ps = 0"
by (case_tac ps, simp_all)

lemma equal_pair_count_Suc: "
  equal_pair_count ((a, a) # ps) = Suc (equal_pair_count ps)" 
by simp


lemma equal_pair_count_eq_pairwise[rule_format]: "
  [| length ps1 = length ps2; 
    ∀i<length ps2. equal_pair (ps1 ! i) = equal_pair(ps2 ! i) |]
  ==> equal_pair_count ps1 = equal_pair_count ps2"
apply (induct rule: list_induct2)
 apply simp
apply (fastsimp simp add: equal_pair_def)
done

lemma equal_pair_count_mirror_pairwise[rule_format]: "
  [| length ps1 = length ps2; 
    ∀i<length ps2. ps1 ! i = mirror_pair (ps2 ! i) |]
  ==> equal_pair_count ps1 = equal_pair_count ps2"
apply (rule equal_pair_count_eq_pairwise, assumption)
thm mirror_pair_equal
apply (simp add: mirror_pair_equal)
done

(* The lemma states that all pairs with index < equal_pair_count ps
  are equal. It does not deal with maximality of equal_pair_count *)
lemma equal_pair_count_correct:"
  !!i. i < equal_pair_count ps ==> equal_pair (ps ! i)"
apply (induct ps)
 apply simp
apply simp
apply (split split_if_asm)
apply (case_tac i)
apply (simp add: equal_pair_def)+
done
thm equal_pair_count_correct

(* For @{text "i = equal_pair_count ps"} holds:
  either @{text "ps ! i"} not an equal pair,
  or all pairs are equal (@{text "equal_pair_count = length ps"}) *)
lemma equal_pair_count_maximality_aux[rule_format]: "!!i. 
  i = equal_pair_count ps ==> length ps = i ∨ ¬ equal_pair (ps ! i)"
apply (induct ps)
 apply simp
apply (simp add: equal_pair_def)
done
thm equal_pair_count_maximality_aux
corollary equal_pair_count_maximality1a[rule_format]: "
  equal_pair_count ps = length ps ∨ ¬ equal_pair (ps!equal_pair_count ps)"
thm equal_pair_count_maximality_aux[of "equal_pair_count ps" ps, simplified]
apply (insert equal_pair_count_maximality_aux[of "equal_pair_count ps" ps])
apply clarsimp
done

corollary equal_pair_count_maximality1b[rule_format]: "
  equal_pair_count ps ≠ length ps ==>
  ¬ equal_pair (ps!equal_pair_count ps)"
by (insert equal_pair_count_maximality1a[of ps], simp)

lemma equal_pair_count_maximality2a[rule_format]: "
  equal_pair_count ps = length ps ∨ (* either all pairs are equal *)
  (∀i≥equal_pair_count ps.(∃j≤i. ¬equal_pair (ps ! j)))"
apply clarsimp
apply (rule_tac x="equal_pair_count ps" in exI)
thm equal_pair_count_maximality1b equal_pair_count_le
apply (simp add: equal_pair_count_maximality1b equal_pair_count_le)
done
corollary equal_pair_count_maximality2b[rule_format]: "
  equal_pair_count ps ≠ length ps ==>
  ∀i≥equal_pair_count ps.(∃j≤i. ¬equal_pair (ps!j))"
by (insert equal_pair_count_maximality2a[of ps], simp)

lemmas equal_pair_count_maximality =
  equal_pair_count_maximality1a equal_pair_count_maximality1b
  equal_pair_count_maximality2a equal_pair_count_maximality2b
thm 
  equal_pair_count_correct[no_vars]
  equal_pair_count_maximality[no_vars]





subsection {* Prefix length *}

text {* Length of the prefix infimum *}
definition
  inf_prefix_length :: "'a list => 'a list => nat"
where
  "inf_prefix_length xs ys ≡ equal_pair_count (zip xs ys)"

value "int (inf_prefix_length [1::int,2,3,4,7,8,15] [1::int,2,3,4,7,15])"
value "int (inf_prefix_length [1::int,2,3,4] [1::int,2,3,4,7,15])"
value "int (inf_prefix_length [] [1::int,2,3,4,7,15])"
value "int (inf_prefix_length [1::int,2,3,4,5] [1::int,2,3,4,5])"

lemma inf_prefix_length_commute[rule_format]:
  "inf_prefix_length xs ys = inf_prefix_length ys xs"
apply (unfold inf_prefix_length_def)
thm equal_pair_count_mirror_pairwise
apply (insert equal_pair_count_mirror_pairwise[of "zip xs ys" "zip ys xs"])
apply (simp add: equal_pair_count_mirror_pairwise[of "zip xs ys" "zip ys xs"] min_ac mirror_pair_def)
done

lemma inf_prefix_length_leL[intro]: 
  "inf_prefix_length xs ys ≤ length xs"
apply (unfold inf_prefix_length_def)
apply (insert equal_pair_count_le[of "zip xs ys"])
apply simp
done
corollary inf_prefix_length_leR[intro]:
  "inf_prefix_length xs ys ≤ length ys"
thm inf_prefix_length_commute[of xs ys]
by (simp add: inf_prefix_length_commute[of xs] inf_prefix_length_leL)
lemmas inf_prefix_length_le =
  inf_prefix_length_leL 
  inf_prefix_length_leR

lemma inf_prefix_length_le_min[rule_format]:
  "inf_prefix_length xs ys ≤ min (length xs) (length ys)"
by (simp add: inf_prefix_length_le)

thm equal_pair_count_0
lemma hd_inf_prefix_length_0: "
  hd xs ≠ hd ys ==> inf_prefix_length xs ys = 0"
apply (unfold inf_prefix_length_def)
apply (case_tac "xs = []", simp)
apply (case_tac "ys = []", simp)
apply (simp add: equal_pair_count_0 hd_zip)
done

lemma inf_prefix_length_NilL[simp]: "inf_prefix_length [] ys = 0"
by (simp add: inf_prefix_length_def)
lemma inf_prefix_length_NilR[simp]: "inf_prefix_length xs [] = 0"
by (simp add: inf_prefix_length_def)

thm equal_pair_count_Suc
lemma inf_prefix_length_Suc[simp]: "
  inf_prefix_length (a # xs) (a # ys) = Suc (inf_prefix_length xs ys)"
by (simp add: inf_prefix_length_def)

thm equal_pair_count_correct
lemma inf_prefix_length_correct: "
  i < inf_prefix_length xs ys ==> xs ! i = ys ! i"
thm order_less_le_trans[OF _ inf_prefix_length_leL]
apply (frule order_less_le_trans[OF _ inf_prefix_length_leL])
apply (frule order_less_le_trans[OF _ inf_prefix_length_leR])
apply (unfold inf_prefix_length_def)
apply (drule equal_pair_count_correct)
apply (simp add: equal_pair_def)
done

corollary nth_neq_imp_inf_prefix_length_le: "
  xs ! i ≠ ys ! i ==> inf_prefix_length xs ys ≤ i"
apply (rule ccontr)
apply (simp add: inf_prefix_length_correct)
done


thm equal_pair_count_maximality1b
lemma inf_prefix_length_maximality1[rule_format]: "
  inf_prefix_length xs ys ≠ min (length xs) (length ys) ==>
  xs ! (inf_prefix_length xs ys) ≠ ys ! (inf_prefix_length xs ys)"
thm equal_pair_count_maximality1b[of "zip xs ys"]
thm equal_pair_count_maximality1b[of "zip xs ys", folded inf_prefix_length_def]
apply (insert equal_pair_count_maximality1b[of "zip xs ys", folded inf_prefix_length_def], simp)
apply (drule neq_le_trans)
 apply (simp add: inf_prefix_length_le)
apply (simp add:  inf_prefix_length_def equal_pair_def)
done

thm equal_pair_count_maximality2b
corollary inf_prefix_length_maximality2[rule_format]: "
  [| inf_prefix_length xs ys ≠ min (length xs) (length ys);
    inf_prefix_length xs ys ≤ i |] ==> 
  ∃j≤i. xs ! j ≠ ys ! j"
apply (rule_tac x="inf_prefix_length xs ys" in exI)
apply (simp add: inf_prefix_length_maximality1 inf_prefix_length_le_min)
done

lemmas inf_prefix_length_maximality =
  inf_prefix_length_maximality1 inf_prefix_length_maximality2

lemma inf_prefix_length_append[simp]: "
  inf_prefix_length (zs @ xs) (zs @ ys) =
  length zs + inf_prefix_length xs ys"
apply (induct zs)
 apply simp
apply (simp add: inf_prefix_length_def)
done

lemma inf_prefix_length_take_correct: "
  n ≤ inf_prefix_length xs ys ==> xs \<down> n = ys \<down> n"
apply (frule order_trans[OF _ inf_prefix_length_leL])
apply (frule order_trans[OF _ inf_prefix_length_leR])
apply (simp add: list_eq_iff inf_prefix_length_correct)
done

lemma inf_prefix_length_0_imp_hd_neq: "
  [| xs ≠ []; ys ≠ []; inf_prefix_length xs ys = 0 |] ==> hd xs ≠ hd ys"
apply (rule ccontr)
thm inf_prefix_length_maximality2[of xs ys 0]
apply (insert inf_prefix_length_maximality2[of xs ys 0])
apply (simp add: hd_eq_first)
done



subsection {* Prefix infimum *}

definition
  inf_prefix :: "'a list => 'a list => 'a list"  (infixl "\<sqinter>" 70)
where
  "xs \<sqinter> ys ≡ xs \<down> (inf_prefix_length xs ys)"

lemma length_inf_prefix: "length (xs \<sqinter> ys) = inf_prefix_length xs ys"
by (simp add: inf_prefix_def min_eqR inf_prefix_length_leL)

lemma inf_prefix_commute: "xs \<sqinter> ys = ys \<sqinter> xs"
by (simp add: inf_prefix_def inf_prefix_length_commute[of ys] inf_prefix_length_take_correct)

lemma inf_prefix_takeL: "xs \<sqinter> ys = xs \<down> (inf_prefix_length xs ys)"
by (simp add: inf_prefix_def)
lemma inf_prefix_takeR: "xs \<sqinter> ys = ys \<down> (inf_prefix_length xs ys)"
by (subst inf_prefix_commute, subst inf_prefix_length_commute, rule inf_prefix_takeL)

thm inf_prefix_length_correct
lemma inf_prefix_correct: "i < length (xs \<sqinter> ys) ==> xs ! i = ys ! i"
by (simp add: length_inf_prefix inf_prefix_length_correct)
corollary inf_prefix_correctL: "
  i < length (xs \<sqinter> ys) ==> (xs \<sqinter> ys) ! i = xs ! i"
by (simp add: inf_prefix_takeL)
corollary inf_prefix_correctR: "
  i < length (xs \<sqinter> ys) ==> (xs \<sqinter> ys) ! i = ys ! i"
by (simp add: inf_prefix_takeR)

thm inf_prefix_length_take_correct
lemma inf_prefix_take_correct: "
  n ≤ length (xs \<sqinter> ys) ==> xs \<down> n = ys \<down> n"
by (simp add: length_inf_prefix inf_prefix_length_take_correct)

lemma is_inf_prefix[rule_format]: "
  [| length zs = length (xs \<sqinter> ys); 
    !!i. i < length (xs \<sqinter> ys) ==> zs ! i = xs ! i ∧ zs ! i = ys ! i |] ==>
  zs = xs \<sqinter> ys"
by (simp add: list_eq_iff inf_prefix_def)

thm hd_inf_prefix_length_0
lemma hd_inf_prefix_Nil: "hd xs ≠ hd ys ==> xs \<sqinter> ys = []"
by (simp add: inf_prefix_def hd_inf_prefix_length_0)

thm inf_prefix_length_0_imp_hd_neq
lemma inf_prefix_Nil_imp_hd_neq: "
  [| xs ≠ []; ys ≠ []; xs \<sqinter> ys = [] |] ==> hd xs ≠ hd ys"
by (simp add: inf_prefix_def inf_prefix_length_0_imp_hd_neq)

lemma length_inf_prefix_append[simp]: "
  length ((zs @ xs) \<sqinter> (zs @ ys)) = 
  length zs + length (xs \<sqinter> ys)"
by (simp add: length_inf_prefix)

lemma inf_prefix_append[simp]: "(zs @ xs) \<sqinter> (zs @ ys) = zs @ (xs \<sqinter> ys)"
apply (rule is_inf_prefix[symmetric], simp)
apply (clarsimp simp: nth_append)
thm inf_prefix_correctL inf_prefix_correctR
apply (intro conjI inf_prefix_correctL inf_prefix_correctR, simp+)
done

lemma hd_neq_inf_prefix_append: "
  hd xs ≠ hd ys ==> (zs @ xs) \<sqinter> (zs @ ys) = zs"
by (simp add: hd_inf_prefix_Nil)



thm inf_prefix_length_NilL
lemma inf_prefix_NilL[simp]: "[] \<sqinter> ys = []"
by (simp del: length_0_conv add: length_0_conv[symmetric] length_inf_prefix)
corollary inf_prefix_NilR[simp]: "xs \<sqinter> [] = []"
by (simp add: inf_prefix_commute)
lemmas inf_prefix_Nil = inf_prefix_NilL inf_prefix_NilR
thm inf_prefix_Nil

lemma inf_prefix_Cons[simp]: "(a # xs) \<sqinter> (a # ys) = a # xs \<sqinter> ys"
by (insert inf_prefix_append[of "[a]" xs ys], simp)
corollary inf_prefix_hd[simp]: "hd ((a # xs) \<sqinter> (a # ys)) = a"
by simp


lemma inf_prefix_le1: "xs \<sqinter> ys ≤ xs"
by (simp add: inf_prefix_takeL take_imp_prefix)
lemma inf_prefix_le2: "xs \<sqinter> ys ≤ ys"
by (simp add: inf_prefix_takeR take_imp_prefix)

thm min_le_iff_conj
lemma le_inf_prefix_iff: "(x ≤ y \<sqinter> z) = (x ≤ y ∧ x ≤ z)"
apply (rule iffI)
 apply (blast intro: order_trans inf_prefix_le1 inf_prefix_le2)
apply (clarsimp simp: prefix_def)
done
lemma le_imp_le_inf_prefix: "[| x ≤ y; x ≤ z |] ==> x ≤ y \<sqinter> z"
thm le_inf_prefix_iff[THEN iffD2]
by (rule le_inf_prefix_iff[THEN iffD2], simp)

interpretation prefix:
  semilattice_inf
    "op ≤ :: 'a list => 'a list => bool"
    "op < :: 'a list => 'a list => bool"
    "op \<sqinter> :: 'a list => 'a list => 'a list"
apply intro_locales
apply (rule class.semilattice_inf_axioms.intro)
apply (rule inf_prefix_le1)
apply (rule inf_prefix_le2)
apply (rule le_imp_le_inf_prefix, assumption+)
done



subsection {* Prefices for infinite lists *}

thm prefix_def
term "λx y. x ≤ (y::'a list)"
definition
  iprefix :: "'a list => 'a ilist => bool" (infixl "\<sqsubseteq>" 50)
where
  "xs \<sqsubseteq> f ≡ ∃g. f = xs \<frown> g"

thm prefix_eq_prefix_take
lemma iprefix_eq_iprefix_take: "(xs \<sqsubseteq> f) = (f \<Down> length xs = xs)"
apply (unfold iprefix_def)
apply (rule iffI)
 apply clarsimp
apply (rule_tac x="f \<Up> (length xs)" in exI)
thm i_append_i_take_i_drop_id
apply (subst i_append_i_take_i_drop_id[where n="length xs", symmetric], simp)
done

thm prefix_take_eq_prefix_take_ex
lemma iprefix_take_eq_iprefix_take_ex: "
  (f \<Down> length xs = xs) = (∃n. f \<Down> n = xs)"
apply (rule iffI)
 apply (rule_tac x="length xs" in exI, assumption)
apply clarsimp
done

thm prefix_eq_prefix_take_ex
lemma iprefix_eq_iprefix_take_ex: "(xs \<sqsubseteq> f) = (∃n. f \<Down> n = xs)"
by (simp add: iprefix_eq_iprefix_take iprefix_take_eq_iprefix_take_ex)

thm take_imp_prefix
lemma i_take_imp_iprefix[intro]: "f \<Down> n \<sqsubseteq> f"
by (simp add: iprefix_eq_iprefix_take)

thm take_prefix_le_conv
lemma i_take_prefix_le_conv: "(f \<Down> a ≤ f \<Down> b) = (a ≤ b)"
by (fastsimp simp: prefix_eq_prefix_take list_eq_iff)

thm append_imp_prefix
lemma i_append_imp_iprefix[simp,intro]: "xs \<sqsubseteq> xs \<frown> f"
by (simp add: iprefix_def)

thm prefix_imp_take_eq
lemma iprefix_imp_take_eq: "
  [| n ≤ length xs; xs \<sqsubseteq> f |] ==> xs \<down> n = f \<Down> n"
by (clarsimp simp: iprefix_eq_iprefix_take_ex min_eqR)

thm prefix_refl
thm prefix_trans
thm prefix_antisym
lemma prefix_iprefix_trans: "[| xs ≤ ys; ys \<sqsubseteq> f |] ==> xs \<sqsubseteq> f"
by (fastsimp simp: iprefix_eq_iprefix_take_ex prefix_eq_prefix_take_ex)

thm take_length_prefix_conv
lemma i_take_length_prefix_conv: "(f \<Down> length xs ≤ xs) = (xs \<sqsubseteq> f)"
thm prefix_length_le_eq_conv
by (simp add: iprefix_eq_iprefix_take prefix_length_le_eq_conv[symmetric])

thm List_Prefix.prefixI
lemma iprefixI[intro?]: "f = xs \<frown> g ==> xs \<sqsubseteq> f"
by (unfold iprefix_def, simp)
thm List_Prefix.prefixE
lemma iprefixE[elim?]: "[| xs \<sqsubseteq> f; !!g. f = xs \<frown> g ==> C |] ==> C"
by (unfold iprefix_def, blast)


thm List_Prefix.Nil_prefix
lemma Nil_iprefix[iff]: "[] \<sqsubseteq> f"
by (unfold iprefix_def, simp)

thm List_Prefix.same_prefix_prefix
lemma same_prefix_iprefix[simp]: "(xs @ ys \<sqsubseteq> xs \<frown> f) = (ys \<sqsubseteq> f)"
by (simp add: iprefix_eq_iprefix_take)

thm List_Prefix.prefix_prefix
lemma prefix_iprefix[simp]: "xs ≤ ys ==> xs \<sqsubseteq> ys \<frown> f"
by (clarsimp simp: prefix_def iprefix_def i_append_assoc[symmetric] simp del: i_append_assoc)

thm List_Prefix.append_prefixD
lemma append_iprefixD: "xs @ ys \<sqsubseteq> f ==> xs \<sqsubseteq> f"
by (clarsimp simp: iprefix_def i_append_assoc[symmetric] simp del: i_append_assoc)

lemma iprefix_length_le_imp_prefix: "
  [| xs \<sqsubseteq> ys \<frown> f; length xs ≤ length ys |] ==> xs ≤ ys"
by (clarsimp simp: iprefix_eq_iprefix_take_ex take_is_prefix)

thm List_Prefix.prefix_append
lemma iprefix_i_append: "
  (xs \<sqsubseteq> ys \<frown> f) = (xs ≤ ys ∨ (∃zs. xs = ys @ zs ∧ zs \<sqsubseteq> f))"
apply (rule iffI)
 apply (case_tac "length xs ≤ length ys")
  apply (blast intro: iprefix_length_le_imp_prefix)
 apply (rule disjI2)
 apply (rule_tac x="f \<Down> (length xs - length ys)" in exI)
 apply (simp add: iprefix_eq_iprefix_take)
apply fastsimp
done

lemma i_append_one_iprefix: "
  xs \<sqsubseteq> f ==> xs @ [f (length xs)] \<sqsubseteq> f"
by (simp add: iprefix_eq_iprefix_take i_take_Suc_conv_app_nth)

lemma iprefix_same_length_le: "
  [| xs \<sqsubseteq> f; ys \<sqsubseteq> f; length xs ≤ length ys |] ==> xs ≤ ys"
by (clarsimp simp: iprefix_eq_iprefix_take_ex i_take_prefix_le_conv)

thm List_Prefix.prefix_same_cases
lemma iprefix_same_cases: "
  [| xs \<sqsubseteq> f; ys \<sqsubseteq> f |] ==> xs ≤ ys ∨ ys ≤ xs"
apply (case_tac "length xs ≤ length ys")
apply (simp add: iprefix_same_length_le)+
done

thm List_Prefix.set_mono_prefix
lemma set_mono_iprefix: "xs \<sqsubseteq> f ==> set xs ⊆ range f"
by (unfold iprefix_def, fastsimp)

end