Theory Sequence

theory Sequence
  imports Main "HOL-Library.Sublist"
begin

lemma last_concat:
  "last xss ≠ [] ⟹ concat xss ≠ [] ⟹ last (concat xss) = last (last xss)"
  by (metis append_Nil2 append_butlast_last_id concat.simps concat_append last_appendR)


― ‹The following definition should keep track of transitive closures over a given relation.
   To allow the storage of meta-data (i.e., the rewrite step used to compute a tuple) we concatenate
   via a predicate.›

inductive_set sequence for I P where
  base [simp, intro!]: "x ∈ I ⟹ [x] ∈ sequence I P"
| trans_step [intro]: "x ∈ I ⟹ y # ys ∈ sequence I P ⟹ P x y ⟹ x # y # ys ∈ sequence I P"

lemma sequence_hd_to_I:
  "x # xs ∈ sequence I P ⟹ x ∈ I"
  using sequence.cases by auto

abbreviation "seq_to_rel f xs ≡ (fst (f (hd xs)), snd (f (last xs)))"

lemma sequence_mono1:
  "I ⊆ U ⟹ sequence I P ⊆ sequence U P"
proof -
  assume sub: "I ⊆ U"
  {fix xs assume "xs ∈ sequence I P" then have "xs ∈ sequence U P"
      using sub by (induct) auto}
  then show ?thesis by blast
qed

lemma sequence_mono2:
  "P ≤ Q ⟹ sequence I P ⊆ sequence I Q"
proof -
  assume p: "P ≤ Q"
  {fix xs assume "xs ∈ sequence I P" then have "xs ∈ sequence I Q"
      using p by (induct) auto}
  then show ?thesis by blast
qed

lemma no_empty_seq [simp]:
  "[] ∉ sequence I P ⟷ True"
  "[] ∈ sequence I P ⟷ False"
  using sequence.cases by auto

lemma seq_not_NilD:
  "xs ∈ sequence I P ⟹ xs ≠ []"
  using sequence.cases by auto

lemma seq_singeltonD [dest]:
  "[x] ∈ sequence I P ⟹ x ∈ I"
  using sequence.cases by auto

lemma seq_in_I:
  "xs ∈ sequence I P ⟹ x ∈ set xs ⟹ x ∈ I"
  by (induct rule: sequence.induct) auto

lemma sequence_members [simp]:
  "⋃ (set ` sequence I P) = I"
  by (auto dest: seq_in_I)


lemma sequence_ConsI [intro]:
  assumes "x ∈ I" and "xs ≠ [] ⟹ P x (hd xs) ∧ xs ∈ sequence I P"
  shows "x # xs ∈ sequence I P"
proof (cases xs)
  case Nil then show ?thesis using assms(1) by auto
next
  case (Cons y ys)
  show ?thesis using assms unfolding Cons
    by (intro trans_step) auto
qed

lemma sequence_propI:
  assumes "⋀ x. x ∈ set xs ⟹ x ∈ I" "xs ≠ []"
    and "⋀ i. Suc i < length xs ⟹ P (xs ! i) (xs ! Suc i)"
  shows "xs ∈ sequence I P" using assms
  by (induct xs) (force simp: nth_Cons' hd_conv_nth)+

lemma seq_property_head:
  assumes "(x # y # xs) ∈ sequence I P"
  shows "P x y" using assms
  using sequence.cases by auto

lemma seq_property_head':
  assumes "(x # ys) ∈ sequence I P" "ys ≠ []"
  shows "P x (hd ys)" using assms
  using seq_property_head
  by (cases ys) (auto simp add: seq_property_head)

lemma suffix_seq_in_seq:
  assumes "xs ∈ sequence I P" "suffix ys xs" "ys ≠ []"
  shows "ys ∈ sequence I P" using assms
proof (induct xs arbitrary: ys)
  case (base x) then show ?case
    by (simp add: suffix_Cons)
qed (auto simp: suffix_Cons)

lemma prefix_seq_in_seq:
  assumes "ys ∈ sequence I P" "prefix xs ys" "xs ≠ []"
  shows "xs ∈ sequence I P" using assms
proof (induct ys arbitrary: xs rule: list.induct)
  case (Cons x ys)
  obtain xs' where [simp]: "xs = x # xs'" using Cons(3, 4)
    by (force simp: prefix_Cons)
  have pr: "prefix xs' ys" using Cons(3) by auto
  show ?case
  proof (cases "xs' = []")
    case True
    then show ?thesis using Cons by (auto dest: sequence_hd_to_I)
  next
    case False
    have "x ∈ I" using Cons(2) by (auto dest: sequence_hd_to_I)
    then show ?thesis using False Cons(1)[of xs'] Cons(2-)
      apply (cases ys) apply auto
      by (metis list.sel(1) list.sel(3) list.simps(3) prefix_Cons seq_property_head sequence_ConsI suffix_seq_in_seq suffix_tl)
  qed
qed auto

lemma sublist_seq_in_seq:
  assumes "xs ∈ sequence I P" and "sublist ys xs" and "ys ≠ []"
  shows "ys ∈ sequence I P"
proof -
  from assms(2) obtain us ss where xs: "xs = us @ ys @ ss"
    unfolding sublist_def by blast
  from suffix_seq_in_seq[OF assms(1), of "ys @ ss"]
  have "ys @ ss ∈ sequence I P" using assms(3) unfolding xs
    using suffixI by blast
  from prefix_seq_in_seq[OF this _ assms(3)] show ?thesis
    using prefixI by blast
qed


lemma seq_append_seq:
  assumes "xs @ ys ∈ sequence I P"
  shows "xs ≠ [] ⟹ xs ∈ sequence I P" "ys ≠ [] ⟹ ys ∈ sequence I P"
proof -
  show "xs ≠ [] ⟹ xs ∈ sequence I P"
    using prefix_seq_in_seq[OF assms, of xs]  by force
next
  show "ys ≠ [] ⟹ ys ∈ sequence I P"
    using suffix_seq_in_seq[OF assms, of ys]
    using suffixI by blast
qed

lemma tail_seq_in_seq:
  assumes "xs ∈ sequence I P" "tl xs ≠ []"
  shows "tl xs ∈ sequence I P"
  using suffix_seq_in_seq[OF assms(1)] assms(2-) 
  by auto

lemma seq_property:
  assumes "xs ∈ sequence I P" "Suc i < length xs"
  shows "P (xs ! i) (xs ! Suc i)"
proof -
  let ?ys = "drop i xs"
  show ?thesis using assms(2-)
    using seq_property_head[of "hd ?ys" "hd (tl ?ys)" "tl (tl ?ys)"]
    using suffix_seq_in_seq[OF assms(1), of "drop i xs"]
    by (metis Cons_nth_drop_Suc Suc_lessD list.distinct(1) seq_property_head suffix_drop)
qed

lemma seq_last_append_prop:
  "xs @ [x] ∈ sequence I P ⟹ xs ≠ [] ⟹ P (last xs) x"
  using seq_property[of "xs @ [x]" I P "length xs - 1"]
  by (auto simp: nth_append last_conv_nth)

lemma sequence_converse_induct [consumes 1, case_names base step]:
  assumes "xs ∈ sequence I P"
    and "⋀x. x ∈ I ⟹ R [x]"
    and IH: "⋀x ys. x ∈ I ⟹ ys ∈ sequence I P ⟹ ys ≠ [] ⟹ R ys ⟹ P (last ys) x ⟹ R (ys @ [x])"
  shows "R xs" using assms(1)
proof (induct xs rule: rev_induct)
  case (snoc x xs) show ?case
  proof (cases xs)
    case [simp]: Nil show ?thesis using seq_in_I[OF snoc(2)]
      by (auto intro!: assms(2)[of x])
  next
    case [simp]: (Cons y ys)
    from prefix_seq_in_seq[OF snoc(2)] have "y # ys ∈ sequence I P" by auto
    then show ?thesis using snoc IH[where ?ys = "y # ys" and ?x = x]
      using seq_last_append_prop[OF snoc(2)]
      using seq_in_I[OF snoc(2), of x]
      by auto
  qed
qed auto

lemma sequence_concat_onP [intro]:
  assumes "xs ∈ sequence I P" "ys ∈ sequence I P"
    and "P (last xs) (hd ys)"
  shows "xs @ ys ∈ sequence I P" using assms
proof (induct xs rule: list.induct)
  case (Cons x xs) note IH = this
  have "xs ≠ [] ⟹ xs @ ys ∈ sequence I P" using tail_seq_in_seq[OF IH(2)] IH by auto
  moreover have "xs ≠ [] ⟹ P x (hd xs)" using IH(2) seq_property_head[of x "hd xs" "tl xs"]
    by (cases xs) auto
  ultimately show ?case using IH(2-) seq_in_I[OF IH(2), of x]
    by (auto split!: if_splits intro: sequence_ConsI)
qed auto

lemma sequence_member_min:
  "xs ∈ sequence I P ⟹ xs ∈ sequence (set xs) P"
proof (induct rule: sequence.induct)
  case (trans_step x y ys)
  then show ?case using sequence_mono1[of _ "insert x (insert y (set ys))"]
    by (intro sequence_ConsI[where ?xs = "y # ys"]) auto
qed auto


lemma sequence_concat_cl [intro!]:
  assumes "⋀ xs. xs ∈ set xss ⟹ xs ∈ sequence I P" "xss ≠ []"
    and "⋀ i. Suc i < length xss ⟹ P (last (xss ! i)) (hd (xss ! Suc i))"
  shows "concat xss ∈ sequence I P" using assms
proof (induct xss rule: rev_induct)
  case (snoc a xss) show ?case
  proof (cases "xss = []")
    case True
    then show ?thesis using snoc(2) by auto
  next
    case False
    then have *: "last xss ≠ []" "concat xss ≠ []" using snoc(2) last_in_set[OF False]
      by simp_all (metis ‹last xss ∈ set xss› no_empty_seq)+
    have fh: "xs ∈ set xss ⟹ xs ∈ sequence I P" for xs using snoc(2)[of xs]
      by (auto simp: nth_append split!: if_splits)
    have sh: "Suc i < length xss ⟹ P (last (xss ! i)) (hd (xss ! Suc i))" for i
      using snoc(4)[of i] by (auto simp: nth_append split!: if_splits)
    from snoc(1)[OF fh _ sh] snoc(3) False have "concat xss ∈ sequence I P"
      by auto
    moreover have "a ∈ sequence I P" using snoc(2) by auto
    ultimately show ?thesis using snoc(4)[of "length xss - 1"] False
      by (auto simp: last_concat[OF *] last_conv_nth[OF False] nth_append)
  qed
qed auto


(* Refactor all
lemma sequence_trans_PI:
  assumes  "xs ∈ sequence I P"
    and "⋀ i j k. k < length xs ⟹ i < j ⟹ j < k ⟹ P (xs ! i) (xs ! j) ⟹ P (xs ! j) (xs ! k) ⟹ P (xs ! i) (xs ! k)" 
    and "i < length xs" and "j < i"
  shows "P (xs ! j) (xs ! i)" using assms
proof (induct "i - j" arbitrary: i)
  case (Suc x)
  from Suc(6) obtain n where [simp]: "i = Suc n" by (cases i) auto
  have "j < n ⟹ R (xs ! j) (xs ! n)" using Suc(1)[of n] Suc(2-) by auto
  then show ?case using Suc(2-)
    by (cases "j < n") (auto simp: less_Suc_eq_le)
qed auto


lemma sequence_refl_trans_PI:
  assumes  "xs ∈ sequence I P" and "transp R" and "reflp R"
    and "i < length xs" "j ≤ i"
    and "⋀ i. Suc i < length xs ⟹ R (xs ! i) (xs ! Suc i)"
  shows "R (xs ! j) (xs ! i)" using sequence_trans_PI[OF assms(1, 2, 4)] assms
  by (cases "j = i") (auto simp: reflp_def)

lemma sequence_refl_sym_trans_PI:
  assumes  "xs ∈ sequence I P" and "transp R" and "reflp R" and "symp R"
    and "i < length xs" "j < length xs"
    and "⋀ i. Suc i < length xs ⟹ R (xs ! i) (xs ! Suc i)"
  shows "R (xs ! j) (xs ! i)"
proof -
  have "i < j ⟹ R (xs ! i) (xs ! j)"
    using sequence_trans_PI[OF assms(1, 2, 6) _ assms(7)]
    by auto
  moreover have "j ≤ i ⟹ R (xs ! j) (xs ! i)"
    using sequence_refl_trans_PI[OF assms(1 - 3) assms(5) _ assms(7)]
    by auto
  ultimately show ?thesis using assms(4)
    by (cases "i < j", auto) (simp add: sympD)
qed
*)

(* To do refactoring *)
― ‹A sequence is conform to a relation if for each sequence the tuple
   containing the first and last element belongs to the relation›

definition seq_rel_spec where
  "seq_rel_spec f S R ⟷ [] ∉ S ∧ (∀ xs ∈ S. seq_to_rel f xs ∈ R)"

― ‹A relation is conform to a sequence if for all pairs in the relation there exists
   a sequence such that the first and last element corresponds to the first and second element of the tuple›
definition rel_seq_spec where
  "rel_seq_spec f R S ⟷ [] ∉ S ∧ (∀ s t. (s, t) ∈ R ⟶ (∃ xs ∈ S. (s, t) = seq_to_rel f xs))"

definition rel_seq_strict_spec where
  "rel_seq_strict_spec f R S ⟷ rel_seq_spec f R S ∧ (∀ xs ∈ S. set (map f xs) ⊆ R)"

lemma rel_seq_spec_nempty [simp]:
  "rel_seq_spec f R S ⟹ [] ∉ S"
  by (simp add: rel_seq_spec_def)

lemma rel_seq_strict_spec [simp]:
  "rel_seq_strict_spec f R S ⟹ rel_seq_spec f R S"
  "rel_seq_strict_spec f R S ⟹ [] ∉ S"
  by (auto simp add: rel_seq_strict_spec_def)

lemma rel_seq_specE [elim]:
  assumes "rel_seq_spec f R S" "(s, t) ∈ R"
  obtains xs where "xs ∈ S" "xs ≠ []" "s = fst (f (hd xs))" "t = snd (f (last xs))"
  using assms unfolding rel_seq_spec_def
  by auto

lemma rel_seq_strict_specE [elim]:
  assumes "rel_seq_strict_spec f R S" "(s, t) ∈ R"
  obtains xs where "xs ∈ S" "xs ≠ []" "s = fst (f (hd xs))" "t = snd (f (last xs))" "∀ i < length xs. f (xs ! i) ∈ R"
  using assms unfolding rel_seq_strict_spec_def
  by (auto simp: image_subset_iff)

lemma rel_seq_specI [intro!]:
  "[] ∉ S ⟹ (⋀ s t. (s, t) ∈ R ⟹ ∃ xs ∈ S. s = fst (f (hd xs)) ∧ t = snd (f (last xs))) ⟹ rel_seq_spec f R S"
  unfolding rel_seq_spec_def by auto

lemma seq_rel_specD [dest]:
  "seq_rel_spec f S R ⟹ xs ≠ [] ⟹ xs ∈ S ⟹ (fst (f (hd xs)), snd (f (last xs))) ∈ R"
  unfolding seq_rel_spec_def by auto

definition pred_impl_eq_on where
  "pred_impl_eq_on f I U P ⟷ (∀ x y. x ∈ I ⟶ y ∈ U ⟶ P x y ⟶ snd (f x) = fst (f y))"

definition eq_impl_pred_on where
  "eq_impl_pred_on f I U P ⟷ (∀ x y. x ∈ I ⟶ y ∈ U ⟶ snd (f x) = fst (f y) ⟶ P x y)"

definition seq_impl_in_rel_on where
  "seq_impl_in_rel_on f r I P ⟷ f ` I ⊆ r ∧ pred_impl_eq_on f I I P"

definition rel_impl_in_seq_on where
  "rel_impl_in_seq_on f r I P ⟷ r ⊆ f ` I ∧ eq_impl_pred_on f I I P"

lemma sequence_hd_last_to_trancl:
  assumes "f ` I ⊆ r"
   and "⋀ x y. x ∈ I ⟹ y ∈ I ⟹ P x y ⟹ snd (f x) = fst (f y)"
   and "xs ∈ sequence I P"
 shows "(fst (f (hd xs)), snd (f (last xs))) ∈ r⇧+" using assms(3)
proof (induct xs)
  case (base x)
  then show ?case using assms(1)
    by (simp add: image_subset_iff r_into_trancl')
next
  case (trans_step x y ys)
  from trans_step(2) have "y ∈ I" using seq_in_I by force
  from assms(2)[OF _ this, of x] assms(1) trans_step(1, 4)
  have "snd (f x) = fst (f y)" "f x ∈ r⇧+"
    by (simp_all add: image_subset_iff r_into_trancl')
  then show ?case using trans_step(3)
    by auto (metis prod.collapse trancl_trans)+
qed

lemma trancl_to_sequence:
  assumes "r ⊆ f ` I"
   and "⋀ x y. x ∈ I ⟹ y ∈ I ⟹ f x ∈ r ⟹ f y ∈ r ⟹ snd (f x) = fst (f y) ⟹ P x y"
   and "(s, t) ∈ r⇧+"
 shows "∃ xs. fst (f (hd xs)) = s ∧ snd (f (last xs)) = t ∧ xs ∈ sequence I P ∧
   (∀ i < length xs. f (xs ! i) ∈ r)" using assms(3)
proof (induct rule: converse_trancl_induct)
  case (base s)
  then obtain x where "x ∈ I" "f x = (s, t)" using assms(1) by auto
  then show ?case using base
    by (intro exI[of _ "[x]"]) auto
next
  case (step s u)
  from step(1, 3) assms(1) obtain x xs where elem: "x ∈ I" "f x = (s, u)"
    and list: "fst (f (hd xs)) = u" "snd (f (last xs)) = t"
      "xs ∈ sequence I P" "∀ i < length xs. f (xs ! i) ∈ r"
        by auto
  from assms(2)[OF elem(1), of "hd xs"] list(3, 4) step(1)
  have "P x (hd xs)" using seq_in_I 
    by (cases xs) (fastforce simp: elem(2) hd_conv_nth simp flip: list(1))+ 
  then show ?case using list elem step(1)
    by (intro exI[of _ "x # xs"]) (auto simp: nth_Cons')
qed


definition seq_comp where
  "seq_comp P R S = {xs| xs ys zs. xs = ys @ zs ∧ ys ∈ R ∧ zs ∈ S ∧ ys ≠ [] ∧ zs ≠ [] ∧ P (last ys) (hd zs)}"


lemma seq_comp_nempty[simp]: "[] ∉ seq_comp P R S"
  by (auto simp: seq_comp_def)

lemma seq_compE [elim]:
  assumes "xs ∈ seq_comp P R S"
  obtains ys zs where "ys ≠ []" "zs ≠ []" " xs = ys @ zs" "ys ∈ R" "zs ∈ S" "P (last ys) (hd zs)"
  using assms unfolding seq_comp_def
  by auto

lemma seq_comp_appendI [intro]:
  "xs ≠ [] ⟹ ys ≠ [] ⟹ xs ∈ R ⟹ ys ∈ S ⟹ P (last xs) (hd ys) ⟹ xs @ ys ∈ seq_comp P R S"
  by (auto simp: seq_comp_def)

lemma seq_comp_rel_conf:
  assumes "seq_rel_spec f S R" "seq_rel_spec f S' R'"
    and "pred_impl_eq_on f (⋃ (set ` S)) (⋃ (set ` S')) P"
  shows "seq_rel_spec f (seq_comp P S S') (R O R')"
  using seq_rel_specD[OF assms(1)] seq_rel_specD[OF assms(2)]
  using assms(3) unfolding pred_impl_eq_on_def
  by (auto simp: seq_rel_spec_def relcomp_unfold elim!: seq_compE)
     (metis last_in_set list.set_sel(1))

lemma relcomp_seq_conf:
  assumes "rel_seq_spec f R S" "rel_seq_spec f R' S'"
    and "eq_impl_pred_on f (⋃ (set ` S)) (⋃ (set ` S')) P"
  shows "rel_seq_spec f (R O R') (seq_comp P S S')"
proof -
  {fix s t assume "(s, t) ∈ R O R'"
    then obtain u where comp: "(s, u) ∈ R" "(u, t) ∈ R'" by auto
    from rel_seq_specE[OF assms(1) this(1)] rel_seq_specE[OF assms(2) this(2)]
    obtain xs ys where
      rep: "xs ∈ S" "xs ≠ []" "s = fst (f (hd xs))" "u = snd (f (last xs))"
      "ys ∈ S'" "ys ≠ []" "u = fst (f (hd ys))" "t = snd (f (last ys))"
        by metis
    from assms(3) rep have "P (last xs) (hd ys)" by (force simp: eq_impl_pred_on_def)
    then have mem: "xs @ ys ∈ seq_comp P S S'" using rep by auto
    have "∃ xs ∈ seq_comp P S S'. s = fst (f (hd xs)) ∧ t = snd (f (last xs))"
      using rep(2, 3, 6, 8) by (intro bexI[OF _ mem]) auto}
  then show ?thesis by auto
qed

end