Theory PathLemmas

theory PathLemmas
imports TheoremD14
begin

context LocalLexing begin

lemma characterize_𝒫:
  "(∀ i < length p. ∃u. p ! i ∈ 𝒵 (charslength (take i p)) u) ⟹ admissible p ⟹
  ∃ u. p ∈ 𝒫 (charslength p) u"
proof (induct p rule: rev_induct)
  case Nil
    show ?case by simp
next
  case (snoc a p)
    from snoc.prems have admissible_p: "admissible p"
      by (metis append_Nil2 is_prefix_admissible is_prefix_cancel is_prefix_empty) 
    {
      fix i :: nat
      assume ilen: "i < length p"
      then have "i < length (p@[a])"
        by (simp add: Suc_leI Suc_le_lessD trans_le_add1) 
      with snoc have "∃u. (p @ [a]) ! i ∈ 𝒵 (charslength (take i (p @ [a]))) u"
        by blast
      then obtain u where u: "(p @ [a]) ! i ∈ 𝒵 (charslength (take i (p @ [a]))) u" by blast
      from ilen have p_at: "(p @ [a]) ! i = p ! i" by (simp add: nth_append)  
      from ilen have p_take: "take i (p @ [a]) = take i p" by (simp add: less_or_eq_imp_le) 
      from u p_at p_take have p_i: "p ! i ∈ 𝒵 (charslength (take i p)) u" by simp 
      then have "∃ u. p ! i ∈ 𝒵 (charslength (take i p)) u" by blast
    }
    then have "∀ i < length p. ∃u. p ! i ∈ 𝒵 (charslength (take i p)) u" by auto
    with admissible_p snoc.hyps obtain u where u: "p ∈ 𝒫 (charslength p) u" by blast
    have "∃u. (p @ [a]) ! (length p) ∈ 𝒵 (charslength (take (length p) (p @ [a]))) u"
      using snoc
      by (metis (no_types, opaque_lifting) add_Suc_right append_Nil2 length_Cons length_append 
        less_Suc_eq_le less_or_eq_imp_le) 
    then obtain v where "(p @ [a]) ! (length p) ∈ 𝒵 (charslength (take (length p) (p @ [a]))) v"
      by blast
    then have v: "a ∈ 𝒵 (charslength p) v" by simp
    {
      assume v_leq_u: "v ≤ u"
      then have "a ∈ 𝒵 (charslength p) (Suc u)" using v
        by (meson LocalLexing.subset_fSuc LocalLexing_axioms 𝒵_subset_Suc subsetCE) 
      from path_append_token[OF u this snoc.prems(2)] 
      have "p @ [a] ∈ 𝒫 (charslength p) (Suc u)" by blast
      then have ?case using in_𝒫_charslength by blast 
    }
    note case_v_leq_u = this
    {
      assume u_less_v: "u < v"
      then obtain w where w: "v = Suc w" using less_imp_Suc_add by blast 
      with u_less_v have "u ≤ w" by arith
      with u have "p ∈ 𝒫 (charslength p) w" by (meson subsetCE subset_𝒫k) 
      from v w path_append_token[OF this _ snoc.prems(2)] 
      have "p @ [a] ∈ 𝒫 (charslength p) (Suc w)" by blast
      then have ?case using in_𝒫_charslength by blast 
    }
    note case_u_less_v = this
    
    show ?case using case_v_leq_u case_u_less_v not_le by blast 
qed

lemma drop_empty_tokens: 
  assumes p: "p ∈ 𝔓"
  assumes r: "r ≤ length p"
  assumes empty: "charslength (take r p) = 0"
  assumes admissible: "admissible (drop r p)"
  shows "drop r p ∈ 𝔓"
proof -
  have p_𝒵: "∀i<length p. ∃u. p ! i ∈ 𝒵 (charslength (take i p)) u" using p
    using tokens_nth_in_𝒵 by blast 
  obtain q where q: "q = drop r p" by blast
  {
    fix j :: nat
    assume j : "j < length q"
    have length_p_q_r: "length p = length q + r"
      using r q add.commute diff_add_inverse le_Suc_ex length_drop by simp
    have j_plus_r_bound: "j + r < length p" by (simp add: j length_p_q_r) 
    with p_𝒵 have "∃u. p ! (j + r) ∈ 𝒵 (charslength (take (j + r) p)) u" by blast
    then obtain u where u: "p ! (j + r) ∈ 𝒵 (charslength (take (j + r) p)) u" by blast
    have p_at_is_q_at: "p ! (j + r) = q ! j" by (simp add: add.commute q r) 
    have "take (j + r) p = (take r p) @ (take j q)" by (metis add.commute q take_add)
    with empty have "charslength (take (j + r) p) = charslength (take j q)" by auto
    with u p_at_is_q_at have "q ! j ∈ 𝒵 (charslength (take j q)) u" by simp
    then have "∃ u. q ! j ∈ 𝒵 (charslength (take j q)) u" by auto
  }
  then have "∀i<length q. ∃u. q ! i ∈ 𝒵 (charslength (take i q)) u" by blast
  from characterize_𝒫[OF this] have "∃u. q ∈ 𝒫 (charslength q) u" using admissible q by auto
  then show ?thesis using 𝔓_covers_𝒫 q by blast 
qed
  
end

end