Theory ListInf_Prefix

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

section ‹Prefices on finite and infinite lists›

theory ListInf_Prefix
imports "HOL-Library.Sublist" ListInf
begin

subsection ‹Additional list prefix results›

lemma prefix_eq_prefix_take_ex: "prefix xs ys = (∃n. ys ↓ n = xs)"
apply (unfold prefix_def, safe)
apply (rule_tac x="length xs" in exI, simp)
apply (rule_tac x="ys ↑ n" in exI, simp)
done

lemma prefix_take_eq_prefix_take_ex: "(ys ↓ (length xs) = xs) = (∃n. ys ↓ n = xs)"
by (fastforce simp: min_def)

lemma prefix_eq_prefix_take: "prefix xs ys = (ys ↓ (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 ↓ (length xs) = xs ∧ xs ≠ ys) =
  ((∃n. ys ↓ n = xs) ∧ xs ≠ ys)"
by (simp add: prefix_take_eq_prefix_take_ex)

lemma strict_prefix_eq_strict_prefix_take_ex: "strict_prefix xs ys = ((∃n. ys ↓ n = xs) ∧ xs ≠ ys)"
by (simp add: strict_prefix_def prefix_eq_prefix_take_ex)
lemma strict_prefix_eq_strict_prefix_take: "strict_prefix xs ys = (ys ↓ (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: "prefix (xs ↓ n) xs"
by (rule take_is_prefix)

lemma eq_imp_prefix: "xs = (ys::'a list) ⟹ prefix xs ys"
by simp

lemma le_take_imp_prefix: "a ≤ b ⟹ prefix (xs ↓ a) (xs ↓ b)"
by (fastforce simp: prefix_eq_prefix_take_ex min_def)

lemma take_prefix_imp_le: "
  ⟦ a ≤ length xs; prefix (xs ↓ a) (xs ↓ b) ⟧ ⟹ a ≤ b"
by (drule prefix_length_le, simp)

lemma take_prefixeq_le_conv: "
  a ≤ length xs ⟹ prefix (xs ↓ a) (xs ↓ 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]: "prefix a (a @ b)"
by (unfold prefix_def, blast)

lemma prefix_imp_take_eq: "
  ⟦ n ≤ length xs; prefix xs ys ⟧ ⟹ xs ↓ n = ys ↓ n"
by (clarsimp simp: prefix_def)

lemma prefix_length_le_eq_conv: "(prefix 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 ⟹ prefix (ys ↓ length xs) xs = prefix xs ys"
by (fastforce simp: prefix_eq_prefix_take)

lemma append_eq_imp_take: "
  ⟦ k ≤ length xs; length r1 = k; r1 @ r2 = xs ⟧ ⟹ r1 = xs ↓ k"
by fastforce

lemma take_the_conv: "
  xs ↓ 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 ↓ k" in exI)
 apply (intro conjI)
   apply (simp add: min_eqR)
  apply (rule_tac x="xs ↑ k" in exI, simp)
 apply fastforce
apply fastforce
done


lemma prefix_refl: "prefix xs (xs::'a list)"
by (rule prefix_order.order_refl)

lemma prefix_trans: "⟦ prefix xs ys; prefix (ys::'a list) zs ⟧ ⟹ prefix xs zs"
by (rule prefix_order.order_trans)

lemma prefixeq_antisym: "⟦ prefix xs ys; prefix (ys::'a list) xs ⟧ ⟹ xs = ys"
by (rule prefix_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 (fastforce 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 (fastforce 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)
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 if_split_asm)
apply (case_tac i)
apply (simp add: equal_pair_def)+
done

(* 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

corollary equal_pair_count_maximality1a[rule_format]: "
  equal_pair_count ps = length ps ∨ ¬ equal_pair (ps!equal_pair_count ps)"
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)
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


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)
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"] 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"
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)

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)

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)

lemma inf_prefix_length_correct: "
  i < inf_prefix_length xs ys ⟹ xs ! i = ys ! i"
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

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)"
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

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 ↓ n = ys ↓ 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)
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 "⊓" 70)
  where "xs ⊓ ys ≡ xs ↓ (inf_prefix_length xs ys)"

lemma length_inf_prefix: "length (xs ⊓ ys) = inf_prefix_length xs ys"
by (simp add: inf_prefix_def min_eqR inf_prefix_length_leL)

lemma inf_prefix_commute: "xs ⊓ ys = ys ⊓ xs"
by (simp add: inf_prefix_def inf_prefix_length_commute[of ys] inf_prefix_length_take_correct)

lemma inf_prefix_takeL: "xs ⊓ ys = xs ↓ (inf_prefix_length xs ys)"
by (simp add: inf_prefix_def)

lemma inf_prefix_takeR: "xs ⊓ ys = ys ↓ (inf_prefix_length xs ys)"
by (subst inf_prefix_commute, subst inf_prefix_length_commute, rule inf_prefix_takeL)

lemma inf_prefix_correct: "i < length (xs ⊓ ys) ⟹ xs ! i = ys ! i"
by (simp add: length_inf_prefix inf_prefix_length_correct)

corollary inf_prefix_correctL: "
  i < length (xs ⊓ ys) ⟹ (xs ⊓ ys) ! i = xs ! i"
by (simp add: inf_prefix_takeL)

corollary inf_prefix_correctR: "
  i < length (xs ⊓ ys) ⟹ (xs ⊓ ys) ! i = ys ! i"
by (simp add: inf_prefix_takeR)

lemma inf_prefix_take_correct: "
  n ≤ length (xs ⊓ ys) ⟹ xs ↓ n = ys ↓ n"
by (simp add: length_inf_prefix inf_prefix_length_take_correct)

lemma is_inf_prefix[rule_format]: "
  ⟦ length zs = length (xs ⊓ ys);
    ⋀i. i < length (xs ⊓ ys) ⟹ zs ! i = xs ! i ∧ zs ! i = ys ! i ⟧ ⟹
  zs = xs ⊓ ys"
by (simp add: list_eq_iff inf_prefix_def)

lemma hd_inf_prefix_Nil: "hd xs ≠ hd ys ⟹ xs ⊓ ys = []"
by (simp add: inf_prefix_def hd_inf_prefix_length_0)

lemma inf_prefix_Nil_imp_hd_neq: "
  ⟦ xs ≠ []; ys ≠ []; xs ⊓ 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) ⊓ (zs @ ys)) =
  length zs + length (xs ⊓ ys)"
by (simp add: length_inf_prefix)

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

lemma hd_neq_inf_prefix_append: "
  hd xs ≠ hd ys ⟹ (zs @ xs) ⊓ (zs @ ys) = zs"
by (simp add: hd_inf_prefix_Nil)

lemma inf_prefix_NilL[simp]: "[] ⊓ ys = []"
by (simp del: length_0_conv add: length_0_conv[symmetric] length_inf_prefix)

corollary inf_prefix_NilR[simp]: "xs ⊓ [] = []"
by (simp add: inf_prefix_commute)

lemmas inf_prefix_Nil = inf_prefix_NilL inf_prefix_NilR

lemma inf_prefix_Cons[simp]: "(a # xs) ⊓ (a # ys) = a # xs ⊓ ys"
by (insert inf_prefix_append[of "[a]" xs ys], simp)

corollary inf_prefix_hd[simp]: "hd ((a # xs) ⊓ (a # ys)) = a"
by simp


lemma inf_prefix_le1: "prefix (xs ⊓ ys) xs"
by (simp add: inf_prefix_takeL take_imp_prefix)

lemma inf_prefix_le2: "prefix (xs ⊓ ys) ys"
by (simp add: inf_prefix_takeR take_imp_prefix)

lemma le_inf_prefix_iff: "prefix x (y ⊓ z) = (prefix x y ∧ prefix x z)"
apply (rule iffI)
 apply (blast intro: prefix_order.order_trans inf_prefix_le1 inf_prefix_le2)
apply (clarsimp simp: prefix_def)
done

lemma le_imp_le_inf_prefix: "⟦ prefix x y; prefix x z ⟧ ⟹ prefix x (y ⊓ z)"
by (rule le_inf_prefix_iff[THEN iffD2], simp)

interpretation prefix:
  semilattice_inf
    "(⊓) :: 'a list ⇒ 'a list ⇒ 'a list"
    "prefix"
    "strict_prefix"
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›

definition iprefix :: "'a list ⇒ 'a ilist ⇒ bool"  (infixl "⊑" 50)
  where "xs ⊑ f ≡ ∃g. f = xs ⌢ g"

lemma iprefix_eq_iprefix_take: "(xs ⊑ f) = (f ⇓ length xs = xs)"
apply (unfold iprefix_def)
apply (rule iffI)
 apply clarsimp
apply (rule_tac x="f ⇑ (length xs)" in exI)
apply (subst i_append_i_take_i_drop_id[where n="length xs", symmetric], simp)
done

lemma iprefix_take_eq_iprefix_take_ex: "
  (f ⇓ length xs = xs) = (∃n. f ⇓ n = xs)"
apply (rule iffI)
 apply (rule_tac x="length xs" in exI, assumption)
apply clarsimp
done

lemma iprefix_eq_iprefix_take_ex: "(xs ⊑ f) = (∃n. f ⇓ n = xs)"
by (simp add: iprefix_eq_iprefix_take iprefix_take_eq_iprefix_take_ex)

lemma i_take_imp_iprefix[intro]: "f ⇓ n ⊑ f"
by (simp add: iprefix_eq_iprefix_take)

lemma i_take_prefix_le_conv: "prefix (f ⇓ a) (f ⇓ b) = (a ≤ b)"
by (fastforce simp: prefix_eq_prefix_take list_eq_iff)

lemma i_append_imp_iprefix[simp,intro]: "xs ⊑ xs ⌢ f"
by (simp add: iprefix_def)

lemma iprefix_imp_take_eq: "
  ⟦ n ≤ length xs; xs ⊑ f ⟧ ⟹ xs ↓ n = f ⇓ n"
by (clarsimp simp: iprefix_eq_iprefix_take_ex min_eqR)

lemma prefixeq_iprefix_trans: "⟦ prefix xs ys; ys ⊑ f ⟧ ⟹ xs ⊑ f"
by (fastforce simp: iprefix_eq_iprefix_take_ex prefix_eq_prefix_take_ex)

lemma i_take_length_prefix_conv: "prefix (f ⇓ length xs) xs = (xs ⊑ f)"
by (simp add: iprefix_eq_iprefix_take prefix_length_le_eq_conv[symmetric])

lemma iprefixI[intro?]: "f = xs ⌢ g ⟹ xs ⊑ f"
by (unfold iprefix_def, simp)

lemma iprefixE[elim?]: "⟦ xs ⊑ f; ⋀g. f = xs ⌢ g ⟹ C ⟧ ⟹ C"
by (unfold iprefix_def, blast)

lemma Nil_iprefix[iff]: "[] ⊑ f"
by (unfold iprefix_def, simp)

lemma same_prefix_iprefix[simp]: "(xs @ ys ⊑ xs ⌢ f) = (ys ⊑ f)"
by (simp add: iprefix_eq_iprefix_take)

lemma prefix_iprefix[simp]: "prefix xs ys ⟹ xs ⊑ ys ⌢ f"
by (clarsimp simp: prefix_def iprefix_def i_append_assoc[symmetric] simp del: i_append_assoc)

lemma append_iprefixD: "xs @ ys ⊑ f ⟹ xs ⊑ f"
by (clarsimp simp: iprefix_def i_append_assoc[symmetric] simp del: i_append_assoc)

lemma iprefix_length_le_imp_prefix: "
  ⟦ xs ⊑ ys ⌢ f; length xs ≤ length ys ⟧ ⟹ prefix xs ys"
by (clarsimp simp: iprefix_eq_iprefix_take_ex take_is_prefix)

lemma iprefix_i_append: "
  (xs ⊑ ys ⌢ f) = (prefix xs ys ∨ (∃zs. xs = ys @ zs ∧ zs ⊑ 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 ⇓ (length xs - length ys)" in exI)
 apply (simp add: iprefix_eq_iprefix_take)
apply fastforce
done

lemma i_append_one_iprefix: "
  xs ⊑ f ⟹ xs @ [f (length xs)] ⊑ f"
by (simp add: iprefix_eq_iprefix_take i_take_Suc_conv_app_nth)

lemma iprefix_same_length_le: "
  ⟦ xs ⊑ f; ys ⊑ f; length xs ≤ length ys ⟧ ⟹ prefix xs ys"
by (clarsimp simp: iprefix_eq_iprefix_take_ex i_take_prefix_le_conv)

lemma iprefix_same_cases: "
  ⟦ xs ⊑ f; ys ⊑ f ⟧ ⟹ prefix xs ys ∨ prefix ys xs"
apply (case_tac "length xs ≤ length ys")
apply (simp add: iprefix_same_length_le)+
done

lemma set_mono_iprefix: "xs ⊑ f ⟹ set xs ⊆ range f"
by (unfold iprefix_def, fastforce)

end