Theory TheoremD9

theory TheoremD9
imports TheoremD8
begin

context LocalLexing begin

definition items_le :: "nat ⇒ items ⇒ items"
where
  "items_le k I = { x . x ∈ I ∧ item_end x ≤ k }"

definition items_eq :: "nat ⇒ items ⇒ items"
where
  "items_eq k I = { x . x ∈ I ∧ item_end x = k }"

definition paths_le :: "nat ⇒ tokens set ⇒ tokens set"
where 
  "paths_le k P = { p . p ∈ P ∧ charslength p ≤ k }"

definition paths_eq :: "nat ⇒ tokens set ⇒ tokens set"
where
  "paths_eq k P = { p . p ∈ P ∧ charslength p = k }"

lemma items_le_pointwise: "pointwise (items_le k)"
  by (auto simp add: pointwise_def items_le_def)

lemma items_le_is_filter: "items_le k I ⊆ I"
  by (auto simp add: items_le_def)

lemma items_eq_pointwise: "pointwise (items_eq k)"
  by (auto simp add: pointwise_def items_eq_def)

lemma items_eq_is_filter: "items_eq k I ⊆ I"
  by (auto simp add: items_eq_def)

lemma paths_le_pointwise: "pointwise (paths_le k)"
  by (auto simp add: pointwise_def paths_le_def)

lemma paths_le_continuous: "continuous (paths_le k)"
  by (simp add: paths_le_pointwise pointbased_implies_continuous pointwise_implies_pointbased)

lemma paths_le_mono: "mono (paths_le k)"
  by (simp add: continuous_imp_mono paths_le_continuous)
   
lemma paths_le_is_filter: "paths_le k P ⊆ P"
  by (auto simp add: paths_le_def)

lemma paths_eq_pointwise: "pointwise (paths_eq k)"
  by (auto simp add: pointwise_def paths_eq_def)

lemma paths_eq_is_filter: "paths_eq k P ⊆ P"
  by (auto simp add: paths_eq_def)

lemma Predict_item_end: "x ∈ Predict k Y ⟹ item_end x = k ∨ x ∈ Y"
  using Predict_def by auto
  
lemma Complete_item_end: "x ∈ Complete k Y ⟹ item_end x = k ∨ x ∈ Y"
  using Complete_def by auto

lemma 𝒥_0_0_item_end: "x ∈ 𝒥 0 0 ⟹ item_end x = 0"
  apply (simp add: π_def)
  proof (induct rule: limit_induct)
    case (Init x) thus ?case by (auto simp add: Init_def)
  next
    case (Iterate x Y) 
    then have "x ∈ Complete 0 (Predict 0 Y)" by (simp add: Scan_empty)
    then have "item_end x = 0 ∨ x ∈ Predict 0 Y" using Complete_item_end by blast
    then have "item_end x = 0 ∨ x ∈ Y" using Predict_item_end by blast 
    then show ?case using Iterate by blast
  qed

lemma items_le_𝒥_0_0: "items_le 0 (𝒥 0 0) = 𝒥 0 0"
  using LocalLexing.𝒥_0_0_item_end LocalLexing.items_le_def LocalLexing_axioms by blast

lemma paths_le_𝒫_0_0: "paths_le 0 (𝒫 0 0) = 𝒫 0 0"
  by (auto simp add: paths_le_def)

definition empty_tokens :: "token set ⇒ token set"
where
  "empty_tokens T = { t . t ∈ T ∧ chars_of_token t = [] }"

lemma items_le_Predict: "items_le k (Predict k I) = Predict k (items_le k I)"
  by (auto simp add: items_le_def Predict_def bin_def)

lemma items_le_Complete: 
  "wellformed_items I ⟹ items_le k (Complete k I) = Complete k (items_le k I)"
  by (auto simp add: items_le_def Complete_def bin_def is_complete_def wellformed_items_def 
    wellformed_item_def)

lemma items_le_Scan:
  "items_le k (Scan T k I) = Scan (empty_tokens T) k (items_le k I)"
  by (auto simp add: items_le_def Scan_def bin_def empty_tokens_def)

lemma wellformed_items_Gen: "wellformed_items (Gen P)"
  using Gen_implies_pvalid pvalid_def wellformed_items_def by blast
  
lemma wellformed_𝒥_0_0: "wellformed_items (𝒥 0 0)"
  using thmD8 wellformed_items_Gen by auto

lemma wellformed_items_Predict: 
  "wellformed_items I ⟹ wellformed_items (Predict k I)"
  by (auto simp add: wellformed_items_def wellformed_item_def Predict_def bin_def)

lemma wellformed_items_Complete:
  "wellformed_items I ⟹ wellformed_items (Complete k I)"
  apply (auto simp add: wellformed_items_def wellformed_item_def Complete_def bin_def)
  apply (metis dual_order.trans)
  using is_complete_def next_symbol_not_complete not_less_eq_eq by blast

lemma 𝒳_length_bound: "(t, c) ∈ 𝒳 k ⟹ k + length c ≤ length Doc"
  using 𝒳_is_prefix is_prefix_length not_le by fastforce

lemma wellformed_items_Scan:
  "wellformed_items I ⟹ T ⊆ 𝒳 k ⟹ wellformed_items (Scan T k I)"
  apply (auto simp add: wellformed_items_def wellformed_item_def Scan_def bin_def 𝒳_length_bound)
  using is_complete_def next_symbol_not_complete not_less_eq_eq by blast

lemma wellformed_items_π:
  assumes "wellformed_items I"
  assumes "T ⊆ 𝒳 k"
  shows "wellformed_items (π k T I)"
proof -
  {
    fix x :: item
    have "x ∈ π k T I ⟹ wellformed_item x"
    proof (simp add: π_def, induct rule: limit_induct)
      case (Init x) thus ?case using assms(1) by (simp add: wellformed_items_def) 
    next
      case (Iterate x Y)
      have "wellformed_items Y" by (simp add: Iterate.hyps(1) wellformed_items_def)
      then have "wellformed_items (Scan T k (Complete k (Predict k Y)))"
        by (simp add: assms(2) wellformed_items_Complete wellformed_items_Predict 
          wellformed_items_Scan)
      then show ?case by (simp add: Iterate.hyps(2) wellformed_items_def) 
    qed
  }
  then show ?thesis using wellformed_items_def by auto  
qed   

lemma 𝒥_subset_Suc_u: "𝒥 k u ⊆ 𝒥 k (Suc u)"
  by (metis Complete_π_fix Complete_subset_π 𝒥.simps(1) 𝒥.simps(2) 𝒥.simps(3) not0_implies_Suc)

lemma mono_TokensAt: "mono (TokensAt k)"
  by (auto simp add: mono_def TokensAt_def bin_def)
    
lemma 𝒯_subset_TokensAt: "𝒯 k u ⊆ TokensAt k (𝒥 k u)"
proof (induct u)
  case 0 thus ?case by simp
next
  case (Suc u)
    have 1: "Tokens k (𝒯 k u) (𝒥 k u) = Sel (𝒯 k u) (TokensAt k (𝒥 k u))"
      by (simp add: Tokens_def)
    have 2: "Sel (𝒯 k u) (TokensAt k (𝒥 k u)) ⊆ TokensAt k (𝒥 k u)"
      by (simp add: Sel_upper_bound Suc.hyps)
    have "𝒯 k (Suc u) ⊆ TokensAt k (𝒥 k u)"
      by (simp add: 1 2)
    then show ?case
      by (meson 𝒥_subset_Suc_u mono_TokensAt mono_subset_elem subset_iff)
qed      

lemma TokensAt_subset_𝒳: "TokensAt k I ⊆ 𝒳 k"
  using TokensAt_def 𝒳_def is_terminal_def by auto
  
lemma wellformed_items_𝒥_induct_u: 
  assumes "wellformed_items (𝒥 k u)"
  shows "wellformed_items (𝒥 k (Suc u))"
proof -
  {
    fix x :: item
    have "x ∈ 𝒥 k (Suc u) ⟹ wellformed_item x"
    proof (simp add: π_def, induct rule: limit_induct)
      case (Init x)
        with assms show ?case by (auto simp add: wellformed_items_def)
    next
      case (Iterate p Y)
        from Iterate(1) have wellformed_Y: "wellformed_items Y"
          by (auto simp add: wellformed_items_def)
        then have "wellformed_items (Complete k (Predict k Y))"
          by (simp add: wellformed_items_Complete wellformed_items_Predict)
        then have "wellformed_items (Scan (Tokens k (𝒯 k u) (𝒥 k u)) k (Complete k (Predict k Y)))"
          apply (rule_tac wellformed_items_Scan)
          apply simp
          apply (simp add: Tokens_def)
          by (meson Sel_upper_bound TokensAt_subset_𝒳 𝒯_subset_TokensAt subset_trans)
        then show ?case
          using Iterate.hyps(2) wellformed_items_def by blast
    qed
  }
  then show ?thesis
    using wellformed_items_def by blast 
qed      

lemma wellformed_items_𝒥_k_u_if_0: "wellformed_items (𝒥 k 0) ⟹ wellformed_items (𝒥 k u)"
  apply (induct u)
  apply (simp)
  using wellformed_items_𝒥_induct_u by blast

lemma wellformed_items_natUnion: "(⋀ k. wellformed_items (I k)) ⟹ wellformed_items (natUnion I)"
  by (auto simp add: natUnion_def wellformed_items_def) 

lemma wellformed_items_ℐ_k_if_0: "wellformed_items (𝒥 k 0) ⟹ wellformed_items (ℐ k)" 
  apply (simp)
  apply (rule wellformed_items_natUnion)
  using wellformed_items_𝒥_k_u_if_0 by blast
 
lemma wellformed_items_𝒥_ℐ: "wellformed_items (𝒥 k u) ∧ wellformed_items (ℐ k)"
proof (induct k arbitrary: u)
  case 0
    show ?case
      using wellformed_𝒥_0_0 wellformed_items_ℐ_k_if_0 wellformed_items_𝒥_k_u_if_0 by blast 
next
  case (Suc k)
    have 0: "wellformed_items (𝒥 (Suc k) 0)"
      apply simp
      using Suc.hyps wellformed_items_π by auto      
    then show ?case
      using wellformed_items_ℐ_k_if_0 wellformed_items_𝒥_k_u_if_0 by blast
qed

lemma wellformed_items_𝒥: "wellformed_items (𝒥 k u)"
by (simp add: wellformed_items_𝒥_ℐ)

lemma wellformed_items_ℐ: "wellformed_items (ℐ k)"
using wellformed_items_𝒥_ℐ by blast

lemma funpower_consume_function:
  assumes law: "⋀ X. P X ⟹ f (g X) = h (f X) ∧ P (g X)"
  shows "P I ⟹ P (funpower g n I) ∧ f (funpower g n I) = funpower h n (f I)"
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then have S1: "P (funpower g n I)" and S2: "f (funpower g n I) = funpower h n (f I)"
    by auto
  have law1: "⋀ X. P X ⟹ f (g X) = h (f X)" using law by auto
  have law2: "⋀ X. P X ⟹ P (g X)" using law by auto
  show ?case
    apply simp
    apply (subst law1[where X="funpower g n I"])
    apply (simp add: S1)
    apply (subst S2) 
    apply auto
    apply (rule law2)
    apply (simp add: S1)
    done
qed
    
lemma limit_consume_function:
  assumes continuous: "continuous f"
  assumes law: "⋀ X. P X ⟹ f (g X) = h (f X) ∧ P (g X)"
  assumes setmonotone: "setmonotone g"
  shows "P I ⟹ f (limit g I) = limit h (f I)"
proof -
  have 1: "f (limit g I) = f (natUnion (λn. funpower g n I))"
    by (simp add: limit_def)
  have "chain (λn. funpower g n I)" by (simp add: setmonotone setmonotone_implies_chain_funpower)
  from continuous_apply[OF continuous this]
  have swap: "f (natUnion (λn. funpower g n I)) = natUnion (f ∘ (λn. funpower g n I))" by blast
  have "f o (λn. funpower g n I) = (λ n. f (funpower g n I))" by auto
  also have "P I ⟹ (λ n. f (funpower g n I)) = (λ n. funpower h n (f I))"
    by (metis funpower_consume_function[where P=P and f=f and g=g and h=h, OF law, simplified])
  ultimately have "P I ⟹ f o (λn. funpower g n I) = (λ n. funpower h n (f I))" by auto
  with swap have 2: "P I ⟹ f (natUnion (λn. funpower g n I)) = natUnion (λ n. funpower h n (f I))"
    by auto
  have 3: "natUnion (λ n. funpower h n (f I)) = limit h (f I)"
    by (simp add: limit_def)
  assume "P I"
  with 1 2 3 show ?thesis by auto
qed

lemma items_le_π_swap: 
  assumes wellformed_I: "wellformed_items I"
  assumes T: "T ⊆ 𝒳 k"
  shows "items_le k (π k T I) = π k (empty_tokens T) (items_le k I)"
proof -
  let ?g = "(Scan T k) o (Complete k) o (Predict k)"
  let ?h = "(Scan (empty_tokens T) k) o (Complete k) o (Predict k)" 
  have law1: "⋀ I. wellformed_items I ⟹ items_le k (?g I) = ?h (items_le k I)"
    using LocalLexing.wellformed_items_Predict LocalLexing_axioms items_le_Complete 
      items_le_Predict items_le_Scan by auto
  have law2: "⋀ I. wellformed_items I ⟹ wellformed_items (?g I)"
    by (simp add: T wellformed_items_Complete wellformed_items_Predict wellformed_items_Scan)
  show ?thesis
    apply (subst π_functional)
    apply (subst limit_consume_function[where P="wellformed_items" and h="?h"])
    apply (simp add: items_le_pointwise pointbased_implies_continuous pointwise_implies_pointbased)
    using law1 law2 apply blast
    apply (simp add: π_step_regular regular_implies_setmonotone)
    apply (rule wellformed_I)
    apply (subst π_functional)
    apply blast
    done
qed
    
lemma items_le_idempotent: "items_le k (items_le k I) = items_le k I"
  using items_le_def by auto 

lemma paths_le_idempotent: "paths_le k (paths_le k P) = paths_le k P"
  using paths_le_def by auto

lemma items_le_fix_D:
  assumes items_le_fix: "items_le k I = I"
  assumes x_dom: "x ∈ I" 
  shows "item_end x ≤ k"
using items_le_def items_le_fix x_dom by blast

lemma remove_paths_le_in_subset_Gen:
  assumes "items_le k I = I"
  assumes "I ⊆ Gen P"
  shows "I ⊆ Gen (paths_le k P)"
proof -
  {
    fix x :: item
    assume x_dom: "x ∈ I"
    then have x_item_end:  "item_end x ≤ k" using assms items_le_fix_D by auto 
    have "x ∈ Gen P" using assms x_dom by auto 
    then obtain p where p: "p ∈ P ∧ pvalid p x" using Gen_implies_pvalid by blast 
    have charslength_p: "charslength p ≤ k" using p pvalid_item_end x_item_end by auto 
    then have "p ∈ paths_le k P" by (simp add: p paths_le_def) 
    then have "x ∈ Gen (paths_le k P)" using Gen_def p by blast 
  }
  then show ?thesis by blast 
qed

lemma mono_Gen: "mono Gen"
  by (auto simp add: mono_def Gen_def)

lemma empty_tokens_idempotent: "empty_tokens (empty_tokens T) = empty_tokens T"
  by (auto simp add: empty_tokens_def)

lemma empty_tokens_is_filter: "empty_tokens T ⊆ T"
  by (auto simp add: empty_tokens_def)

lemma items_le_paths_le: "items_le k (Gen P) = Gen (paths_le k P)"
  using LocalLexing.Gen_def LocalLexing.items_le_def LocalLexing_axioms paths_le_def 
  pvalid_item_end by auto      

lemma bin_items_le[symmetric]: "bin I k = bin (items_le k I) k"
  by (auto simp add: bin_def items_le_def)

lemma TokensAt_items_le[symmetric]: "TokensAt k I = TokensAt k (items_le k I)"
  using TokensAt_def bin_items_le by blast

lemma by_length_paths_le[symmetric]: "by_length k P = by_length k (paths_le k P)"
  using by_length.simps paths_le_def by auto

lemma 𝒲_paths_le[symmetric]: "𝒲 P k = 𝒲 (paths_le k P) k"
  using 𝒲_def by_length_paths_le by blast

theorem 𝒯_equals_𝒵_induct_step: 
  assumes induct: "items_le k (𝒥 k u) = Gen (paths_le k (𝒫 k u))"
  assumes induct_tokens: "𝒯 k u = 𝒵 k u"
  shows "𝒯 k (Suc u) = 𝒵 k (Suc u)"
proof -
  have "TokensAt k (𝒥 k u) = TokensAt k (items_le k (𝒥 k u))"
    using TokensAt_items_le by blast
  also have "TokensAt k (items_le k (𝒥 k u)) = TokensAt k (Gen (paths_le k (𝒫 k u)))"
    using induct by auto
  ultimately have TokensAt_le: "TokensAt k (𝒥 k u) = TokensAt k (Gen (paths_le k (𝒫 k u)))"
    by auto
  have "TokensAt k (𝒥 k u) = 𝒲 (𝒫 k u) k"
    apply (subst TokensAt_le)
    apply (subst 𝒲_paths_le[symmetric])
    apply (rule_tac thmD4[symmetric])
    using 𝔓_covers_𝒫 paths_le_is_filter by blast
  then show ?thesis
    by (simp add: induct_tokens Tokens_def 𝒴_def)
qed 

theorem thmD9:
  assumes induct: "items_le k (𝒥 k u) = Gen (paths_le k (𝒫 k u))"
  assumes induct_tokens: "𝒯 k u = 𝒵 k u"
  assumes k: "k ≤ length Doc"
  shows "items_le k (𝒥 k (Suc u)) ⊆ Gen (paths_le k (𝒫 k (Suc u)))"
proof -
  have t1: "items_le k (𝒥 k (Suc u)) = items_le k (π k (𝒯 k (Suc u)) (𝒥 k u))"
    by auto
  have t2: "items_le k (π k (𝒯 k (Suc u)) (𝒥 k u)) = 
    π k (empty_tokens (𝒯 k (Suc u))) (items_le k (𝒥 k u))"
    apply (subst items_le_π_swap)
    apply (simp add: wellformed_items_𝒥)
    using TokensAt_subset_𝒳 𝒯_subset_TokensAt apply blast
    by blast
  have t3: "π k (empty_tokens (𝒯 k (Suc u))) (items_le k (𝒥 k u)) =
    π k (empty_tokens (𝒯 k (Suc u))) (Gen (paths_le k (𝒫 k u)))"
    using induct by auto
  have 𝒫_subset: "𝒫 k u ⊆ 𝒫 k (Suc u)" using subset_𝒫Suc by blast
  then have "paths_le k (𝒫 k u) ⊆ paths_le k (𝒫 k (Suc u))"
    by (simp add: mono_subset_elem paths_le_mono subsetI)
  with mono_Gen have "Gen (paths_le k (𝒫 k u)) ⊆ Gen (paths_le k (𝒫 k (Suc u)))"
    by (simp add: mono_subset_elem subsetI)
  then have t4: "π k (empty_tokens (𝒯 k (Suc u))) (Gen (paths_le k (𝒫 k u))) ⊆
    π k (empty_tokens (𝒯 k (Suc u))) (Gen (paths_le k (𝒫 k (Suc u))))"
    by (rule monoD[OF mono_π]) 
  have 𝒯_eq_𝒵: "𝒯 k (Suc u) = 𝒵 k (Suc u)"
    using 𝒯_equals_𝒵_induct_step assms(1) induct_tokens by blast  
  have t5: "π k (empty_tokens (𝒯 k (Suc u))) (Gen (paths_le k (𝒫 k (Suc u)))) ⊆ 
    Gen (paths_le k (𝒫 k (Suc u)))"
    apply (rule_tac remove_paths_le_in_subset_Gen)
    apply (subst items_le_π_swap)
    using wellformed_items_Gen apply blast
    using 𝒯_eq_𝒵 𝒵_subset_𝒳 empty_tokens_is_filter apply blast    
    apply (simp only: empty_tokens_idempotent paths_le_idempotent items_le_paths_le)
    apply (rule_tac thmD5)
    using items_le_is_filter items_le_paths_le apply blast
    apply (rule k)
    using 𝒯_eq_𝒵 empty_tokens_is_filter by blast
  from t1 t2 t3 t4 t5 show ?thesis using subset_trans by blast
qed      
  
end

end