Theory TheoremD13

theory TheoremD13
imports TheoremD12
begin

context LocalLexing begin

lemma pointwise_natUnion_swap:
  assumes pointwise_f: "pointwise f"
  shows "f (natUnion G) = natUnion (λ u. f (G u))"
proof -
  note f_simp = pointwise_simp[OF pointwise_f]
  have h1: "f (natUnion G) = ⋃ {f {x} |x. x ∈ (natUnion G)}" using f_simp by blast
  have h2: "⋀ x. f (G x) =  ⋃ {f {y} |y. y ∈ G x}" using f_simp by metis
  show ?thesis
    apply (subst h1)
    apply (subst h2)
    apply (simp add: natUnion_def)
    by blast
qed    

lemma pointwise_Gen: "pointwise Gen"
  by (simp add: pointwise_def Gen_def, blast)
    
lemma thmD13_part1:
  assumes start: "items_le k (𝒥 k 0) = Gen (paths_le k (𝒫 k 0))"
  assumes valid_k: "k ≤ length Doc"
  shows "items_le k (𝒥 k u) = Gen (paths_le k (𝒫 k u)) ∧ 𝒯 k u = 𝒵 k u"
proof (induct u)
  case 0 
    then show ?case using start by auto
next
  case (Suc u) 
    from Suc have sub: "items_le k (𝒥 k (Suc u)) ⊆ Gen (paths_le k (𝒫 k (Suc u)))"
      using thmD9 valid_k by blast
    from Suc have sup: "items_le k (𝒥 k (Suc u)) ⊇ Gen (paths_le k (𝒫 k (Suc u)))"
      using thmD12 by blast
    from Suc have tokens: "𝒯 k (Suc u) = 𝒵 k (Suc u)"
      using 𝒯_equals_𝒵_induct_step by blast
    from sub sup tokens show ?case by blast
qed

lemma thmD13_part2:      
  assumes start: "items_le k (𝒥 k 0) = Gen (paths_le k (𝒫 k 0))"
  assumes valid_k: "k ≤ length Doc"
  shows "items_le k (ℐ k) = Gen (paths_le k (𝒬 k))"
proof -
  note part1 = thmD13_part1[OF start valid_k]
  have e1: "items_le k (ℐ k) = natUnion (λ u. items_le k (𝒥 k u))"
    using items_le_pointwise pointwise_natUnion_swap by auto 
  have e2: "natUnion (λ u. items_le k (𝒥 k u)) = natUnion  (λ u. Gen (paths_le k (𝒫 k u)))"
    using part1 by auto
  have e3: "natUnion (λ u. Gen (paths_le k (𝒫 k u))) = Gen (natUnion (λ u. paths_le k (𝒫 k u)))"
    using pointwise_Gen pointwise_natUnion_swap by fastforce 
  have e4: "natUnion (λ u. paths_le k (𝒫 k u)) = paths_le k (natUnion (λ u. 𝒫 k u))"
    using paths_le_pointwise pointwise_natUnion_swap by fastforce   
  from e1 e2 e3 e4 show ?thesis by simp
qed
    
theorem thmD13:      
  assumes start: "items_le k (𝒥 k 0) = Gen (paths_le k (𝒫 k 0))"
  assumes valid_k: "k ≤ length Doc"
  shows "items_le k (𝒥 k u) = Gen (paths_le k (𝒫 k u)) ∧ 𝒯 k u = 𝒵 k u 
    ∧ items_le k (ℐ k) = Gen (paths_le k (𝒬 k))"
using thmD13_part1[OF start valid_k] thmD13_part2[OF start valid_k] by blast

end

end