Theory Sequence

(*  Title:      HOL/HOLCF/IOA/Sequence.thy
    Author:     Olaf Müller
*)

section ‹Sequences over flat domains with lifted elements›

theory Sequence
imports Seq
begin

default_sort type

type_synonym 'a Seq = "'a lift seq"

definition Consq :: "'a ⇒ 'a Seq → 'a Seq"
  where "Consq a = (LAM s. Def a ## s)"

definition Filter :: "('a ⇒ bool) ⇒ 'a Seq → 'a Seq"
  where "Filter P = sfilter ⋅ (flift2 P)"

definition Map :: "('a ⇒ 'b) ⇒ 'a Seq → 'b Seq"
  where "Map f = smap ⋅ (flift2 f)"

definition Forall :: "('a ⇒ bool) ⇒ 'a Seq ⇒ bool"
  where "Forall P = sforall (flift2 P)"

definition Last :: "'a Seq → 'a lift"
  where "Last = slast"

definition Dropwhile :: "('a ⇒ bool) ⇒ 'a Seq → 'a Seq"
  where "Dropwhile P = sdropwhile ⋅ (flift2 P)"

definition Takewhile :: "('a ⇒ bool) ⇒ 'a Seq → 'a Seq"
  where "Takewhile P = stakewhile ⋅ (flift2 P)"

definition Zip :: "'a Seq → 'b Seq → ('a * 'b) Seq"
  where "Zip =
    (fix ⋅ (LAM h t1 t2.
      case t1 of
        nil ⇒ nil
      | x ## xs ⇒
          (case t2 of
            nil ⇒ UU
          | y ## ys ⇒
              (case x of
                UU ⇒ UU
              | Def a ⇒
                  (case y of
                    UU ⇒ UU
                  | Def b ⇒ Def (a, b) ## (h ⋅ xs ⋅ ys))))))"

definition Flat :: "'a Seq seq → 'a Seq"
  where "Flat = sflat"

definition Filter2 :: "('a ⇒ bool) ⇒ 'a Seq → 'a Seq"
  where "Filter2 P =
    (fix ⋅
      (LAM h t.
        case t of
          nil ⇒ nil
        | x ## xs ⇒
            (case x of
              UU ⇒ UU
            | Def y ⇒ (if P y then x ## (h ⋅ xs) else h ⋅ xs))))"

abbreviation Consq_syn  ("(_/↝_)" [66, 65] 65)
  where "a ↝ s ≡ Consq a ⋅ s"


subsection ‹List enumeration›

syntax
  "_totlist" :: "args ⇒ 'a Seq"  ("[(_)!]")
  "_partlist" :: "args ⇒ 'a Seq"  ("[(_)?]")
translations
  "[x, xs!]" ⇌ "x ↝ [xs!]"
  "[x!]" ⇌ "x↝nil"
  "[x, xs?]" ⇌ "x ↝ [xs?]"
  "[x?]" ⇌ "x ↝ CONST bottom"


declare andalso_and [simp]
declare andalso_or [simp]


subsection ‹Recursive equations of operators›

subsubsection ‹Map›

lemma Map_UU: "Map f ⋅ UU = UU"
  by (simp add: Map_def)

lemma Map_nil: "Map f ⋅ nil = nil"
  by (simp add: Map_def)

lemma Map_cons: "Map f ⋅ (x ↝ xs) = (f x) ↝ Map f ⋅ xs"
  by (simp add: Map_def Consq_def flift2_def)


subsubsection ‹Filter›

lemma Filter_UU: "Filter P ⋅ UU = UU"
  by (simp add: Filter_def)

lemma Filter_nil: "Filter P ⋅ nil = nil"
  by (simp add: Filter_def)

lemma Filter_cons: "Filter P ⋅ (x ↝ xs) = (if P x then x ↝ (Filter P ⋅ xs) else Filter P ⋅ xs)"
  by (simp add: Filter_def Consq_def flift2_def If_and_if)


subsubsection ‹Forall›

lemma Forall_UU: "Forall P UU"
  by (simp add: Forall_def sforall_def)

lemma Forall_nil: "Forall P nil"
  by (simp add: Forall_def sforall_def)

lemma Forall_cons: "Forall P (x ↝ xs) = (P x ∧ Forall P xs)"
  by (simp add: Forall_def sforall_def Consq_def flift2_def)


subsubsection ‹Conc›

lemma Conc_cons: "(x ↝ xs) @@ y = x ↝ (xs @@ y)"
  by (simp add: Consq_def)


subsubsection ‹Takewhile›

lemma Takewhile_UU: "Takewhile P ⋅ UU = UU"
  by (simp add: Takewhile_def)

lemma Takewhile_nil: "Takewhile P ⋅ nil = nil"
  by (simp add: Takewhile_def)

lemma Takewhile_cons:
  "Takewhile P ⋅ (x ↝ xs) = (if P x then x ↝ (Takewhile P ⋅ xs) else nil)"
  by (simp add: Takewhile_def Consq_def flift2_def If_and_if)


subsubsection ‹DropWhile›

lemma Dropwhile_UU: "Dropwhile P ⋅ UU = UU"
  by (simp add: Dropwhile_def)

lemma Dropwhile_nil: "Dropwhile P ⋅ nil = nil"
  by (simp add: Dropwhile_def)

lemma Dropwhile_cons: "Dropwhile P ⋅ (x ↝ xs) = (if P x then Dropwhile P ⋅ xs else x ↝ xs)"
  by (simp add: Dropwhile_def Consq_def flift2_def If_and_if)


subsubsection ‹Last›

lemma Last_UU: "Last ⋅ UU = UU"
  by (simp add: Last_def)

lemma Last_nil: "Last ⋅ nil = UU"
  by (simp add: Last_def)

lemma Last_cons: "Last ⋅ (x ↝ xs) = (if xs = nil then Def x else Last ⋅ xs)"
  by (cases xs) (simp_all add: Last_def Consq_def)


subsubsection ‹Flat›

lemma Flat_UU: "Flat ⋅ UU = UU"
  by (simp add: Flat_def)

lemma Flat_nil: "Flat ⋅ nil = nil"
  by (simp add: Flat_def)

lemma Flat_cons: "Flat ⋅ (x ## xs) = x @@ (Flat ⋅ xs)"
  by (simp add: Flat_def Consq_def)


subsubsection ‹Zip›

lemma Zip_unfold:
  "Zip =
    (LAM t1 t2.
      case t1 of
        nil ⇒ nil
      | x ## xs ⇒
          (case t2 of
            nil ⇒ UU
          | y ## ys ⇒
              (case x of
                UU ⇒ UU
              | Def a ⇒
                  (case y of
                    UU ⇒ UU
                  | Def b ⇒ Def (a, b) ## (Zip ⋅ xs ⋅ ys)))))"
  apply (rule trans)
  apply (rule fix_eq4)
  apply (rule Zip_def)
  apply (rule beta_cfun)
  apply simp
  done

lemma Zip_UU1: "Zip ⋅ UU ⋅ y = UU"
  apply (subst Zip_unfold)
  apply simp
  done

lemma Zip_UU2: "x ≠ nil ⟹ Zip ⋅ x ⋅ UU = UU"
  apply (subst Zip_unfold)
  apply simp
  apply (cases x)
  apply simp_all
  done

lemma Zip_nil: "Zip ⋅ nil ⋅ y = nil"
  apply (subst Zip_unfold)
  apply simp
  done

lemma Zip_cons_nil: "Zip ⋅ (x ↝ xs) ⋅ nil = UU"
  apply (subst Zip_unfold)
  apply (simp add: Consq_def)
  done

lemma Zip_cons: "Zip ⋅ (x ↝ xs) ⋅ (y ↝ ys) = (x, y) ↝ Zip ⋅ xs ⋅ ys"
  apply (rule trans)
  apply (subst Zip_unfold)
  apply simp
  apply (simp add: Consq_def)
  done

lemmas [simp del] =
  sfilter_UU sfilter_nil sfilter_cons
  smap_UU smap_nil smap_cons
  sforall2_UU sforall2_nil sforall2_cons
  slast_UU slast_nil slast_cons
  stakewhile_UU  stakewhile_nil  stakewhile_cons
  sdropwhile_UU  sdropwhile_nil  sdropwhile_cons
  sflat_UU sflat_nil sflat_cons
  szip_UU1 szip_UU2 szip_nil szip_cons_nil szip_cons

lemmas [simp] =
  Filter_UU Filter_nil Filter_cons
  Map_UU Map_nil Map_cons
  Forall_UU Forall_nil Forall_cons
  Last_UU Last_nil Last_cons
  Conc_cons
  Takewhile_UU Takewhile_nil Takewhile_cons
  Dropwhile_UU Dropwhile_nil Dropwhile_cons
  Zip_UU1 Zip_UU2 Zip_nil Zip_cons_nil Zip_cons


subsection ‹Cons›

lemma Consq_def2: "a ↝ s = Def a ## s"
  by (simp add: Consq_def)

lemma Seq_exhaust: "x = UU ∨ x = nil ∨ (∃a s. x = a ↝ s)"
  apply (simp add: Consq_def2)
  apply (cut_tac seq.nchotomy)
  apply (fast dest: not_Undef_is_Def [THEN iffD1])
  done

lemma Seq_cases: obtains "x = UU" | "x = nil" | a s where "x = a ↝ s"
  apply (cut_tac x="x" in Seq_exhaust)
  apply (erule disjE)
  apply simp
  apply (erule disjE)
  apply simp
  apply (erule exE)+
  apply simp
  done

lemma Cons_not_UU: "a ↝ s ≠ UU"
  apply (subst Consq_def2)
  apply simp
  done

lemma Cons_not_less_UU: "¬ (a ↝ x) ⊑ UU"
  apply (rule notI)
  apply (drule below_antisym)
  apply simp
  apply (simp add: Cons_not_UU)
  done

lemma Cons_not_less_nil: "¬ a ↝ s ⊑ nil"
  by (simp add: Consq_def2)

lemma Cons_not_nil: "a ↝ s ≠ nil"
  by (simp add: Consq_def2)

lemma Cons_not_nil2: "nil ≠ a ↝ s"
  by (simp add: Consq_def2)

lemma Cons_inject_eq: "a ↝ s = b ↝ t ⟷ a = b ∧ s = t"
  by (simp add: Consq_def2 scons_inject_eq)

lemma Cons_inject_less_eq: "a ↝ s ⊑ b ↝ t ⟷ a = b ∧ s ⊑ t"
  by (simp add: Consq_def2)

lemma seq_take_Cons: "seq_take (Suc n) ⋅ (a ↝ x) = a ↝ (seq_take n ⋅ x)"
  by (simp add: Consq_def)

lemmas [simp] =
  Cons_not_nil2 Cons_inject_eq Cons_inject_less_eq seq_take_Cons
  Cons_not_UU Cons_not_less_UU Cons_not_less_nil Cons_not_nil


subsection ‹Induction›

lemma Seq_induct:
  assumes "adm P"
    and "P UU"
    and "P nil"
    and "⋀a s. P s ⟹ P (a ↝ s)"
  shows "P x"
  apply (insert assms)
  apply (erule (2) seq.induct)
  apply defined
  apply (simp add: Consq_def)
  done

lemma Seq_FinitePartial_ind:
  assumes "P UU"
    and "P nil"
    and "⋀a s. P s ⟹ P (a ↝ s)"
  shows "seq_finite x ⟶ P x"
  apply (insert assms)
  apply (erule (1) seq_finite_ind)
  apply defined
  apply (simp add: Consq_def)
  done

lemma Seq_Finite_ind:
  assumes "Finite x"
    and "P nil"
    and "⋀a s. Finite s ⟹ P s ⟹ P (a ↝ s)"
  shows "P x"
  apply (insert assms)
  apply (erule (1) Finite.induct)
  apply defined
  apply (simp add: Consq_def)
  done


subsection ‹‹HD› and ‹TL››

lemma HD_Cons [simp]: "HD ⋅ (x ↝ y) = Def x"
  by (simp add: Consq_def)

lemma TL_Cons [simp]: "TL ⋅ (x ↝ y) = y"
  by (simp add: Consq_def)


subsection ‹‹Finite›, ‹Partial›, ‹Infinite››

lemma Finite_Cons [simp]: "Finite (a ↝ xs) = Finite xs"
  by (simp add: Consq_def2 Finite_cons)

lemma FiniteConc_1: "Finite (x::'a Seq) ⟹ Finite y ⟶ Finite (x @@ y)"
  apply (erule Seq_Finite_ind)
  apply simp_all
  done

lemma FiniteConc_2: "Finite (z::'a Seq) ⟹ ∀x y. z = x @@ y ⟶ Finite x ∧ Finite y"
  apply (erule Seq_Finite_ind)
  text ‹‹nil››
  apply (intro strip)
  apply (rule_tac x="x" in Seq_cases, simp_all)
  text ‹‹cons››
  apply (intro strip)
  apply (rule_tac x="x" in Seq_cases, simp_all)
  apply (rule_tac x="y" in Seq_cases, simp_all)
  done

lemma FiniteConc [simp]: "Finite (x @@ y) ⟷ Finite (x::'a Seq) ∧ Finite y"
  apply (rule iffI)
  apply (erule FiniteConc_2 [rule_format])
  apply (rule refl)
  apply (rule FiniteConc_1 [rule_format])
  apply auto
  done


lemma FiniteMap1: "Finite s ⟹ Finite (Map f ⋅ s)"
  apply (erule Seq_Finite_ind)
  apply simp_all
  done

lemma FiniteMap2: "Finite s ⟹ ∀t. s = Map f ⋅ t ⟶ Finite t"
  apply (erule Seq_Finite_ind)
  apply (intro strip)
  apply (rule_tac x="t" in Seq_cases, simp_all)
  text ‹‹main case››
  apply auto
  apply (rule_tac x="t" in Seq_cases, simp_all)
  done

lemma Map2Finite: "Finite (Map f ⋅ s) = Finite s"
  apply auto
  apply (erule FiniteMap2 [rule_format])
  apply (rule refl)
  apply (erule FiniteMap1)
  done


lemma FiniteFilter: "Finite s ⟹ Finite (Filter P ⋅ s)"
  apply (erule Seq_Finite_ind)
  apply simp_all
  done


subsection ‹‹Conc››

lemma Conc_cong: "⋀x::'a Seq. Finite x ⟹ (x @@ y) = (x @@ z) ⟷ y = z"
  apply (erule Seq_Finite_ind)
  apply simp_all
  done

lemma Conc_assoc: "(x @@ y) @@ z = (x::'a Seq) @@ y @@ z"
  apply (rule_tac x="x" in Seq_induct)
  apply simp_all
  done

lemma nilConc [simp]: "s@@ nil = s"
  apply (induct s)
  apply simp
  apply simp
  apply simp
  apply simp
  done


(*Should be same as nil_is_Conc2 when all nils are turned to right side!*)
lemma nil_is_Conc: "nil = x @@ y ⟷ (x::'a Seq) = nil ∧ y = nil"
  apply (rule_tac x="x" in Seq_cases)
  apply auto
  done

lemma nil_is_Conc2: "x @@ y = nil ⟷ (x::'a Seq) = nil ∧ y = nil"
  apply (rule_tac x="x" in Seq_cases)
  apply auto
  done


subsection ‹Last›

lemma Finite_Last1: "Finite s ⟹ s ≠ nil ⟶ Last ⋅ s ≠ UU"
  by (erule Seq_Finite_ind) simp_all

lemma Finite_Last2: "Finite s ⟹ Last ⋅ s = UU ⟶ s = nil"
  by (erule Seq_Finite_ind) auto


subsection ‹Filter, Conc›

lemma FilterPQ: "Filter P ⋅ (Filter Q ⋅ s) = Filter (λx. P x ∧ Q x) ⋅ s"
  by (rule_tac x="s" in Seq_induct) simp_all

lemma FilterConc: "Filter P ⋅ (x @@ y) = (Filter P ⋅ x @@ Filter P ⋅ y)"
  by (simp add: Filter_def sfiltersconc)


subsection ‹Map›

lemma MapMap: "Map f ⋅ (Map g ⋅ s) = Map (f ∘ g) ⋅ s"
  by (rule_tac x="s" in Seq_induct) simp_all

lemma MapConc: "Map f ⋅ (x @@ y) = (Map f ⋅ x) @@ (Map f ⋅ y)"
  by (rule_tac x="x" in Seq_induct) simp_all

lemma MapFilter: "Filter P ⋅ (Map f ⋅ x) = Map f ⋅ (Filter (P ∘ f) ⋅ x)"
  by (rule_tac x="x" in Seq_induct) simp_all

lemma nilMap: "nil = (Map f ⋅ s) ⟶ s = nil"
  by (rule_tac x="s" in Seq_cases) simp_all

lemma ForallMap: "Forall P (Map f ⋅ s) = Forall (P ∘ f) s"
  apply (rule_tac x="s" in Seq_induct)
  apply (simp add: Forall_def sforall_def)
  apply simp_all
  done


subsection ‹Forall›

lemma ForallPForallQ1: "Forall P ys ∧ (∀x. P x ⟶ Q x) ⟶ Forall Q ys"
  apply (rule_tac x="ys" in Seq_induct)
  apply (simp add: Forall_def sforall_def)
  apply simp_all
  done

lemmas ForallPForallQ =
  ForallPForallQ1 [THEN mp, OF conjI, OF _ allI, OF _ impI]

lemma Forall_Conc_impl: "Forall P x ∧ Forall P y ⟶ Forall P (x @@ y)"
  apply (rule_tac x="x" in Seq_induct)
  apply (simp add: Forall_def sforall_def)
  apply simp_all
  done

lemma Forall_Conc [simp]: "Finite x ⟹ Forall P (x @@ y) ⟷ Forall P x ∧ Forall P y"
  by (erule Seq_Finite_ind) simp_all

lemma ForallTL1: "Forall P s ⟶ Forall P (TL ⋅ s)"
  apply (rule_tac x="s" in Seq_induct)
  apply (simp add: Forall_def sforall_def)
  apply simp_all
  done

lemmas ForallTL = ForallTL1 [THEN mp]

lemma ForallDropwhile1: "Forall P s ⟶ Forall P (Dropwhile Q ⋅ s)"
  apply (rule_tac x="s" in Seq_induct)
  apply (simp add: Forall_def sforall_def)
  apply simp_all
  done

lemmas ForallDropwhile = ForallDropwhile1 [THEN mp]


(*only admissible in t, not if done in s*)
lemma Forall_prefix: "∀s. Forall P s ⟶ t ⊑ s ⟶ Forall P t"
  apply (rule_tac x="t" in Seq_induct)
  apply (simp add: Forall_def sforall_def)
  apply simp_all
  apply (intro strip)
  apply (rule_tac x="sa" in Seq_cases)
  apply simp
  apply auto
  done

lemmas Forall_prefixclosed = Forall_prefix [rule_format]

lemma Forall_postfixclosed: "Finite h ⟹ Forall P s ⟹ s= h @@ t ⟹ Forall P t"
  by auto


lemma ForallPFilterQR1:
  "(∀x. P x ⟶ Q x = R x) ∧ Forall P tr ⟶ Filter Q ⋅ tr = Filter R ⋅ tr"
  apply (rule_tac x="tr" in Seq_induct)
  apply (simp add: Forall_def sforall_def)
  apply simp_all
  done

lemmas ForallPFilterQR = ForallPFilterQR1 [THEN mp, OF conjI, OF allI]


subsection ‹Forall, Filter›

lemma ForallPFilterP: "Forall P (Filter P ⋅ x)"
  by (simp add: Filter_def Forall_def forallPsfilterP)

(*holds also in other direction, then equal to forallPfilterP*)
lemma ForallPFilterPid1: "Forall P x ⟶ Filter P ⋅ x = x"
  apply (rule_tac x="x" in Seq_induct)
  apply (simp add: Forall_def sforall_def Filter_def)
  apply simp_all
  done

lemmas ForallPFilterPid = ForallPFilterPid1 [THEN mp]

(*holds also in other direction*)
lemma ForallnPFilterPnil1: "Finite ys ⟹ Forall (λx. ¬ P x) ys ⟶ Filter P ⋅ ys = nil"
  by (erule Seq_Finite_ind) simp_all

lemmas ForallnPFilterPnil = ForallnPFilterPnil1 [THEN mp]


(*holds also in other direction*)
lemma ForallnPFilterPUU1: "¬ Finite ys ∧ Forall (λx. ¬ P x) ys ⟶ Filter P ⋅ ys = UU"
  apply (rule_tac x="ys" in Seq_induct)
  apply (simp add: Forall_def sforall_def)
  apply simp_all
  done

lemmas ForallnPFilterPUU = ForallnPFilterPUU1 [THEN mp, OF conjI]


(*inverse of ForallnPFilterPnil*)
lemma FilternPnilForallP [rule_format]: "Filter P ⋅ ys = nil ⟶ Forall (λx. ¬ P x) ys ∧ Finite ys"
  apply (rule_tac x="ys" in Seq_induct)
  text ‹adm›
  apply (simp add: Forall_def sforall_def)
  text ‹base cases›
  apply simp
  apply simp
  text ‹main case›
  apply simp
  done

(*inverse of ForallnPFilterPUU*)
lemma FilternPUUForallP:
  assumes "Filter P ⋅ ys = UU"
  shows "Forall (λx. ¬ P x) ys ∧ ¬ Finite ys"
proof
  show "Forall (λx. ¬ P x) ys"
  proof (rule classical)
    assume "¬ ?thesis"
    then have "Filter P ⋅ ys ≠ UU"
      apply (rule rev_mp)
      apply (induct ys rule: Seq_induct)
      apply (simp add: Forall_def sforall_def)
      apply simp_all
      done
    with assms show ?thesis by contradiction
  qed
  show "¬ Finite ys"
  proof
    assume "Finite ys"
    then have "Filter P⋅ys ≠ UU"
      by (rule Seq_Finite_ind) simp_all
    with assms show False by contradiction
  qed
qed


lemma ForallQFilterPnil:
  "Forall Q ys ⟹ Finite ys ⟹ (⋀x. Q x ⟹ ¬ P x) ⟹ Filter P ⋅ ys = nil"
  apply (erule ForallnPFilterPnil)
  apply (erule ForallPForallQ)
  apply auto
  done

lemma ForallQFilterPUU: "¬ Finite ys ⟹ Forall Q ys ⟹ (⋀x. Q x ⟹ ¬ P x) ⟹ Filter P ⋅ ys = UU"
  apply (erule ForallnPFilterPUU)
  apply (erule ForallPForallQ)
  apply auto
  done


subsection ‹Takewhile, Forall, Filter›

lemma ForallPTakewhileP [simp]: "Forall P (Takewhile P ⋅ x)"
  by (simp add: Forall_def Takewhile_def sforallPstakewhileP)


lemma ForallPTakewhileQ [simp]: "(⋀x. Q x ⟹ P x) ⟹ Forall P (Takewhile Q ⋅ x)"
  apply (rule ForallPForallQ)
  apply (rule ForallPTakewhileP)
  apply auto
  done


lemma FilterPTakewhileQnil [simp]:
  "Finite (Takewhile Q ⋅ ys) ⟹ (⋀x. Q x ⟹ ¬ P x) ⟹ Filter P ⋅ (Takewhile Q ⋅ ys) = nil"
  apply (erule ForallnPFilterPnil)
  apply (rule ForallPForallQ)
  apply (rule ForallPTakewhileP)
  apply auto
  done

lemma FilterPTakewhileQid [simp]:
  "(⋀x. Q x ⟹ P x) ⟹ Filter P ⋅ (Takewhile Q ⋅ ys) = Takewhile Q ⋅ ys"
  apply (rule ForallPFilterPid)
  apply (rule ForallPForallQ)
  apply (rule ForallPTakewhileP)
  apply auto
  done


lemma Takewhile_idempotent: "Takewhile P ⋅ (Takewhile P ⋅ s) = Takewhile P ⋅ s"
  apply (rule_tac x="s" in Seq_induct)
  apply (simp add: Forall_def sforall_def)
  apply simp_all
  done

lemma ForallPTakewhileQnP [simp]:
  "Forall P s ⟶ Takewhile (λx. Q x ∨ (¬ P x)) ⋅ s = Takewhile Q ⋅ s"
  apply (rule_tac x="s" in Seq_induct)
  apply (simp add: Forall_def sforall_def)
  apply simp_all
  done

lemma ForallPDropwhileQnP [simp]:
  "Forall P s ⟶ Dropwhile (λx. Q x ∨ (¬ P x)) ⋅ s = Dropwhile Q ⋅ s"
  apply (rule_tac x="s" in Seq_induct)
  apply (simp add: Forall_def sforall_def)
  apply simp_all
  done


lemma TakewhileConc1: "Forall P s ⟶ Takewhile P ⋅ (s @@ t) = s @@ (Takewhile P ⋅ t)"
  apply (rule_tac x="s" in Seq_induct)
  apply (simp add: Forall_def sforall_def)
  apply simp_all
  done

lemmas TakewhileConc = TakewhileConc1 [THEN mp]

lemma DropwhileConc1: "Finite s ⟹ Forall P s ⟶ Dropwhile P ⋅ (s @@ t) = Dropwhile P ⋅ t"
  by (erule Seq_Finite_ind) simp_all

lemmas DropwhileConc = DropwhileConc1 [THEN mp]


subsection ‹Coinductive characterizations of Filter›

lemma divide_Seq_lemma:
  "HD ⋅ (Filter P ⋅ y) = Def x ⟶
    y = (Takewhile (λx. ¬ P x) ⋅ y) @@ (x ↝ TL ⋅ (Dropwhile (λa. ¬ P a) ⋅ y)) ∧
    Finite (Takewhile (λx. ¬ P x) ⋅ y) ∧ P x"
  (* FIX: pay attention: is only admissible with chain-finite package to be added to
          adm test and Finite f x admissibility *)
  apply (rule_tac x="y" in Seq_induct)
  apply (simp add: adm_subst [OF _ adm_Finite])
  apply simp
  apply simp
  apply (case_tac "P a")
   apply simp
   apply blast
  text ‹‹¬ P a››
  apply simp
  done

lemma divide_Seq: "(x ↝ xs) ⊑ Filter P ⋅ y ⟹
  y = ((Takewhile (λa. ¬ P a) ⋅ y) @@ (x ↝ TL ⋅ (Dropwhile (λa. ¬ P a) ⋅ y))) ∧
  Finite (Takewhile (λa. ¬ P a) ⋅ y) ∧ P x"
  apply (rule divide_Seq_lemma [THEN mp])
  apply (drule_tac f="HD" and x="x ↝ xs" in  monofun_cfun_arg)
  apply simp
  done


lemma nForall_HDFilter: "¬ Forall P y ⟶ (∃x. HD ⋅ (Filter (λa. ¬ P a) ⋅ y) = Def x)"
  unfolding not_Undef_is_Def [symmetric]
  apply (induct y rule: Seq_induct)
  apply (simp add: Forall_def sforall_def)
  apply simp_all
  done


lemma divide_Seq2:
  "¬ Forall P y ⟹
    ∃x. y = Takewhile P⋅y @@ (x ↝ TL ⋅ (Dropwhile P ⋅ y)) ∧ Finite (Takewhile P ⋅ y) ∧ ¬ P x"
  apply (drule nForall_HDFilter [THEN mp])
  apply safe
  apply (rule_tac x="x" in exI)
  apply (cut_tac P1="λx. ¬ P x" in divide_Seq_lemma [THEN mp])
  apply auto
  done


lemma divide_Seq3:
  "¬ Forall P y ⟹ ∃x bs rs. y = (bs @@ (x↝rs)) ∧ Finite bs ∧ Forall P bs ∧ ¬ P x"
  apply (drule divide_Seq2)
  apply fastforce
  done

lemmas [simp] = FilterPQ FilterConc Conc_cong


subsection ‹Take-lemma›

lemma seq_take_lemma: "(∀n. seq_take n ⋅ x = seq_take n ⋅ x') ⟷ x = x'"
  apply (rule iffI)
  apply (rule seq.take_lemma)
  apply auto
  done

lemma take_reduction1:
  "∀n. ((∀k. k < n ⟶ seq_take k ⋅ y1 = seq_take k ⋅ y2) ⟶
    seq_take n ⋅ (x @@ (t ↝ y1)) =  seq_take n ⋅ (x @@ (t ↝ y2)))"
  apply (rule_tac x="x" in Seq_induct)
  apply simp_all
  apply (intro strip)
  apply (case_tac "n")
  apply auto
  apply (case_tac "n")
  apply auto
  done

lemma take_reduction:
  "x = y ⟹ s = t ⟹ (⋀k. k < n ⟹ seq_take k ⋅ y1 = seq_take k ⋅ y2)
    ⟹ seq_take n ⋅ (x @@ (s ↝ y1)) = seq_take n ⋅ (y @@ (t ↝ y2))"
  by (auto intro!: take_reduction1 [rule_format])


text ‹
  Take-lemma and take-reduction for ‹⊑› instead of ‹=›.
›
          
lemma take_reduction_less1:
  "∀n. ((∀k. k < n ⟶ seq_take k ⋅ y1 ⊑ seq_take k⋅y2) ⟶
    seq_take n ⋅ (x @@ (t ↝ y1)) ⊑ seq_take n ⋅ (x @@ (t ↝ y2)))"
  apply (rule_tac x="x" in Seq_induct)
  apply simp_all
  apply (intro strip)
  apply (case_tac "n")
  apply auto
  apply (case_tac "n")
  apply auto
  done

lemma take_reduction_less:
  "x = y ⟹ s = t ⟹ (⋀k. k < n ⟹ seq_take k ⋅ y1 ⊑ seq_take k ⋅ y2) ⟹
    seq_take n ⋅ (x @@ (s ↝ y1)) ⊑ seq_take n ⋅ (y @@ (t ↝ y2))"
  by (auto intro!: take_reduction_less1 [rule_format])

lemma take_lemma_less1:
  assumes "⋀n. seq_take n ⋅ s1 ⊑ seq_take n ⋅ s2"
  shows "s1 ⊑ s2"
  apply (rule_tac t="s1" in seq.reach [THEN subst])
  apply (rule_tac t="s2" in seq.reach [THEN subst])
  apply (rule lub_mono)
  apply (rule seq.chain_take [THEN ch2ch_Rep_cfunL])
  apply (rule seq.chain_take [THEN ch2ch_Rep_cfunL])
  apply (rule assms)
  done

lemma take_lemma_less: "(∀n. seq_take n ⋅ x ⊑ seq_take n ⋅ x') ⟷ x ⊑ x'"
  apply (rule iffI)
  apply (rule take_lemma_less1)
  apply auto
  apply (erule monofun_cfun_arg)
  done


text ‹Take-lemma proof principles.›

lemma take_lemma_principle1:
  assumes "⋀s. Forall Q s ⟹ A s ⟹ f s = g s"
    and "⋀s1 s2 y. Forall Q s1 ⟹ Finite s1 ⟹
      ¬ Q y ⟹ A (s1 @@ y ↝ s2) ⟹ f (s1 @@ y ↝ s2) = g (s1 @@ y ↝ s2)"
  shows "A x ⟶ f x = g x"
  using assms by (cases "Forall Q x") (auto dest!: divide_Seq3)

lemma take_lemma_principle2:
  assumes "⋀s. Forall Q s ⟹ A s ⟹ f s = g s"
    and "⋀s1 s2 y. Forall Q s1 ⟹ Finite s1 ⟹ ¬ Q y ⟹ A (s1 @@ y ↝ s2) ⟹
      ∀n. seq_take n ⋅ (f (s1 @@ y ↝ s2)) = seq_take n ⋅ (g (s1 @@ y ↝ s2))"
  shows "A x ⟶ f x = g x"
  using assms
  apply (cases "Forall Q x")
  apply (auto dest!: divide_Seq3)
  apply (rule seq.take_lemma)
  apply auto
  done


text ‹
  Note: in the following proofs the ordering of proof steps is very important,
  as otherwise either ‹Forall Q s1› would be in the IH as assumption (then
  rule useless) or it is not possible to strengthen the IH apply doing a
  forall closure of the sequence ‹t› (then rule also useless). This is also
  the reason why the induction rule (‹nat_less_induct› or ‹nat_induct›) has to
  to be imbuilt into the rule, as induction has to be done early and the take
  lemma has to be used in the trivial direction afterwards for the
  ‹Forall Q x› case.
›

lemma take_lemma_induct:
  assumes "⋀s. Forall Q s ⟹ A s ⟹ f s = g s"
    and "⋀s1 s2 y n.
      ∀t. A t ⟶ seq_take n ⋅ (f t) = seq_take n ⋅ (g t) ⟹
      Forall Q s1 ⟹ Finite s1 ⟹ ¬ Q y ⟹ A (s1 @@ y ↝ s2) ⟹
      seq_take (Suc n) ⋅ (f (s1 @@ y ↝ s2)) =
      seq_take (Suc n) ⋅ (g (s1 @@ y ↝ s2))"
  shows "A x ⟶ f x = g x"
  apply (insert assms)
  apply (rule impI)
  apply (rule seq.take_lemma)
  apply (rule mp)
  prefer 2 apply assumption
  apply (rule_tac x="x" in spec)
  apply (rule nat.induct)
  apply simp
  apply (rule allI)
  apply (case_tac "Forall Q xa")
  apply (force intro!: seq_take_lemma [THEN iffD2, THEN spec])
  apply (auto dest!: divide_Seq3)
  done


lemma take_lemma_less_induct:
  assumes "⋀s. Forall Q s ⟹ A s ⟹ f s = g s"
    and "⋀s1 s2 y n.
      ∀t m. m < n ⟶ A t ⟶ seq_take m ⋅ (f t) = seq_take m ⋅ (g t) ⟹
      Forall Q s1 ⟹ Finite s1 ⟹ ¬ Q y ⟹ A (s1 @@ y ↝ s2) ⟹
      seq_take n ⋅ (f (s1 @@ y ↝ s2)) =
      seq_take n ⋅ (g (s1 @@ y ↝ s2))"
  shows "A x ⟶ f x = g x"
  apply (insert assms)
  apply (rule impI)
  apply (rule seq.take_lemma)
  apply (rule mp)
  prefer 2 apply assumption
  apply (rule_tac x="x" in spec)
  apply (rule nat_less_induct)
  apply (rule allI)
  apply (case_tac "Forall Q xa")
  apply (force intro!: seq_take_lemma [THEN iffD2, THEN spec])
  apply (auto dest!: divide_Seq3)
  done



lemma take_lemma_in_eq_out:
  assumes "A UU ⟹ f UU = g UU"
    and "A nil ⟹ f nil = g nil"
    and "⋀s y n.
      ∀t. A t ⟶ seq_take n ⋅ (f t) = seq_take n ⋅ (g t) ⟹ A (y ↝ s) ⟹
      seq_take (Suc n) ⋅ (f (y ↝ s)) =
      seq_take (Suc n) ⋅ (g (y ↝ s))"
  shows "A x ⟶ f x = g x"
  apply (insert assms)
  apply (rule impI)
  apply (rule seq.take_lemma)
  apply (rule mp)
  prefer 2 apply assumption
  apply (rule_tac x="x" in spec)
  apply (rule nat.induct)
  apply simp
  apply (rule allI)
  apply (rule_tac x="xa" in Seq_cases)
  apply simp_all
  done


subsection ‹Alternative take_lemma proofs›

subsubsection ‹Alternative Proof of FilterPQ›

declare FilterPQ [simp del]


(*In general: How to do this case without the same adm problems
  as for the entire proof?*)
lemma Filter_lemma1:
  "Forall (λx. ¬ (P x ∧ Q x)) s ⟶
    Filter P ⋅ (Filter Q ⋅ s) = Filter (λx. P x ∧ Q x) ⋅ s"
  apply (rule_tac x="s" in Seq_induct)
  apply (simp add: Forall_def sforall_def)
  apply simp_all
  done

lemma Filter_lemma2: "Finite s ⟹
  Forall (λx. ¬ P x ∨ ¬ Q x) s ⟶ Filter P ⋅ (Filter Q ⋅ s) = nil"
  by (erule Seq_Finite_ind) simp_all

lemma Filter_lemma3: "Finite s ⟹
  Forall (λx. ¬ P x ∨ ¬ Q x) s ⟶ Filter (λx. P x ∧ Q x) ⋅ s = nil"
  by (erule Seq_Finite_ind) simp_all

lemma FilterPQ_takelemma: "Filter P ⋅ (Filter Q ⋅ s) = Filter (λx. P x ∧ Q x) ⋅ s"
  apply (rule_tac A1="λx. True" and Q1="λx. ¬ (P x ∧ Q x)" and x1="s" in
    take_lemma_induct [THEN mp])
  (*better support for A = λx. True*)
  apply (simp add: Filter_lemma1)
  apply (simp add: Filter_lemma2 Filter_lemma3)
  apply simp
  done

declare FilterPQ [simp]


subsubsection ‹Alternative Proof of ‹MapConc››

lemma MapConc_takelemma: "Map f ⋅ (x @@ y) = (Map f ⋅ x) @@ (Map f ⋅ y)"
  apply (rule_tac A1="λx. True" and x1="x" in take_lemma_in_eq_out [THEN mp])
  apply auto
  done

ML ‹
fun Seq_case_tac ctxt s i =
  Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] [] @{thm Seq_cases} i
  THEN hyp_subst_tac ctxt i THEN hyp_subst_tac ctxt (i + 1) THEN hyp_subst_tac ctxt (i + 2);

(* on a↝s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
fun Seq_case_simp_tac ctxt s i =
  Seq_case_tac ctxt s i
  THEN asm_simp_tac ctxt (i + 2)
  THEN asm_full_simp_tac ctxt (i + 1)
  THEN asm_full_simp_tac ctxt i;

(* rws are definitions to be unfolded for admissibility check *)
fun Seq_induct_tac ctxt s rws i =
  Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] [] @{thm Seq_induct} i
  THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt (i + 1))))
  THEN simp_tac (ctxt addsimps rws) i;

fun Seq_Finite_induct_tac ctxt i =
  eresolve_tac ctxt @{thms Seq_Finite_ind} i
  THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt i)));

fun pair_tac ctxt s =
  Rule_Insts.res_inst_tac ctxt [((("y", 0), Position.none), s)] [] @{thm prod.exhaust}
  THEN' hyp_subst_tac ctxt THEN' asm_full_simp_tac ctxt;

(* induction on a sequence of pairs with pairsplitting and simplification *)
fun pair_induct_tac ctxt s rws i =
  Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] [] @{thm Seq_induct} i
  THEN pair_tac ctxt "a" (i + 3)
  THEN (REPEAT_DETERM (CHANGED (simp_tac ctxt (i + 1))))
  THEN simp_tac (ctxt addsimps rws) i;
›

method_setup Seq_case =
  ‹Scan.lift Parse.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_tac ctxt s))›

method_setup Seq_case_simp =
  ‹Scan.lift Parse.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_simp_tac ctxt s))›

method_setup Seq_induct =
  ‹Scan.lift Parse.embedded --
    Scan.optional ((Scan.lift (Args.$$$ "simp" -- Args.colon) |-- Attrib.thms)) []
    >> (fn (s, rws) => fn ctxt => SIMPLE_METHOD' (Seq_induct_tac ctxt s rws))›

method_setup Seq_Finite_induct =
  ‹Scan.succeed (SIMPLE_METHOD' o Seq_Finite_induct_tac)›

method_setup pair =
  ‹Scan.lift Parse.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (pair_tac ctxt s))›

method_setup pair_induct =
  ‹Scan.lift Parse.embedded --
    Scan.optional ((Scan.lift (Args.$$$ "simp" -- Args.colon) |-- Attrib.thms)) []
    >> (fn (s, rws) => fn ctxt => SIMPLE_METHOD' (pair_induct_tac ctxt s rws))›

lemma Mapnil: "Map f ⋅ s = nil ⟷ s = nil"
  by (Seq_case_simp s)

lemma MapUU: "Map f ⋅ s = UU ⟷ s = UU"
  by (Seq_case_simp s)

lemma MapTL: "Map f ⋅ (TL ⋅ s) = TL ⋅ (Map f ⋅ s)"
  by (Seq_induct s)

end