Theory MainTheorems

theory MainTheorems
imports PathLemmas
begin

context LocalLexing begin

theorem ℑ_is_generated_by_𝔓: "ℑ = Gen 𝔓"
proof -
  have "wellformed_items (ℐ (length Doc))"
    using wellformed_items_ℐ by auto
  then have "⋀ x. x ∈ ℐ (length Doc) ⟹ item_end x ≤ length Doc"
    using wellformed_item_def wellformed_items_def by blast
  then have "ℐ (length Doc) ⊆ items_le (length Doc) (ℐ (length Doc))"
    by (auto simp only: items_le_def)  
  then have "ℐ (length Doc) = items_le (length Doc) (ℐ (length Doc))"
    using items_le_is_filter by blast
  then have ℑ_altdef: "ℑ = items_le (length Doc) (ℐ (length Doc))" using ℑ_def by auto
  have "⋀ p. p ∈ (𝒬 (length Doc)) ⟹ charslength p ≤ length Doc"
    using 𝔓_are_doc_tokens 𝔓_def doc_tokens_length by auto
  then have "𝒬 (length Doc) ⊆ paths_le (length Doc) (𝒬 (length Doc))"
    by (auto simp only: paths_le_def)
  then have "𝒬 (length Doc) = paths_le (length Doc) (𝒬 (length Doc))"
    using paths_le_is_filter by blast
  then have 𝔓_altdef: "𝔓 = paths_le (length Doc) (𝒬 (length Doc))" using 𝔓_def by auto
  show ?thesis using ℑ_altdef 𝔓_altdef thmD14 by auto
qed

definition finished_item :: "symbol list ⇒ item"
where
  "finished_item α = Item (𝔖, α) (length α) 0 (length Doc)"

lemma item_rule_finished_item[simp]: "item_rule (finished_item α) = (𝔖, α)"
  by (simp add: finished_item_def)

lemma item_origin_finished_item[simp]: "item_origin (finished_item α) = 0"
  by (simp add: finished_item_def)

lemma item_end_finished_item[simp]: "item_end (finished_item α) = length Doc"
  by (simp add: finished_item_def)

lemma item_dot_finished_item[simp]: "item_dot (finished_item α) = length α"
  by (simp add: finished_item_def)

lemma item_rhs_finished_item[simp]: "item_rhs (finished_item α) = α"
  by (simp add: finished_item_def)

lemma item_α_finished_item[simp]: "item_α (finished_item α) = α"
  by (simp add: finished_item_def item_α_def)

lemma item_nonterminal_finished_item[simp]: "item_nonterminal (finished_item α) = 𝔖"
  by (simp add: finished_item_def item_nonterminal_def)
  
lemma Derives1_of_singleton:
  assumes "Derives1 [N] i r α"
  shows "i = 0 ∧ r = (N, α)"
proof -
  from assms have "i = 0" using Derives1_bound
    using length_Cons less_Suc0 list.size(3) by fastforce 
  then show ?thesis using assms
    using Derives1_def append_Cons append_self_conv append_self_conv2 length_0_conv 
      list.inject by auto
qed    

definition pvalid_with :: "tokens ⇒ item ⇒ nat ⇒ symbol list ⇒ bool"
where
  "pvalid_with p x u γ = 
     (wellformed_tokens p ∧
     wellformed_item x ∧
     u ≤ length p ∧
     charslength p = item_end x ∧
     charslength (take u p) = item_origin x ∧
     is_derivation (terminals (take u p) @ [item_nonterminal x] @ γ) ∧
     derives (item_α x) (terminals (drop u p)))"

lemma pvalid_with: "pvalid p x = (∃ u γ. pvalid_with p x u γ)"
  using pvalid_def pvalid_with_def by blast

theorem Completeness:
  assumes p_in_ll: "p ∈ ll"
  shows "∃ α. pvalid_with p (finished_item α) 0 [] ∧ finished_item α ∈ ℑ"
proof -
  have p: "p ∈ 𝔓 ∧ charslength p = length Doc ∧ terminals p ∈ ℒ"
    using p_in_ll ll_def by auto
  then have derives_p: "derives [𝔖] (terminals p)"
    using ℒ_def is_derivation_def mem_Collect_eq by blast
  then have "∃ D. Derivation [𝔖] D (terminals p)"
    by (simp add: derives_implies_Derivation)   
  then obtain D where D: "Derivation [𝔖] D (terminals p)" by blast
  have is_word_p: "is_word (terminals p)"  using leftlang p by blast
  have not_is_word_𝔖: "¬ (is_word [𝔖])" using is_nonterminal_startsymbol is_terminal_nonterminal 
    is_word_cons by blast  
  have "D ≠ []" using D is_word_p not_is_word_𝔖 using Derivation.simps(1) by force
  then have "∃ d D'. D = d#D'" using D Derivation.elims(2) by blast 
  then obtain d D' where d: "D = d#D'" by blast
  have "∃ α. Derives1 [𝔖] (fst d) (snd d) α ∧ derives α (terminals p)"
    using d D Derivation.simps(2) Derivation_implies_derives by blast 
  then obtain α where α: "Derives1 [𝔖] (fst d) (snd d) α ∧ derives α (terminals p)" by blast
  then have snd_d_in_ℜ: "snd d ∈ ℜ" using Derives1_rule by blast 
  with α have snd_d: "snd d = (𝔖, α)" using Derives1_of_singleton by blast
  have wellformed_p: "wellformed_tokens p" by (simp add: 𝔓_wellformed p)
  have wellformed_finished_item: "wellformed_item (finished_item α)"  
    apply (auto simp add: wellformed_item_def)
    using snd_d snd_d_in_ℜ by metis    
  have pvalid_with: "pvalid_with p (finished_item α) 0 []" 
    apply (auto simp add: pvalid_with_def)
    using wellformed_p apply blast
    using wellformed_finished_item apply blast
    using p apply (simp add: finished_item_def)
    apply (simp add: is_derivation_def)
    by (simp add: α)
  then have "pvalid p (finished_item α)" using pvalid_def pvalid_with_def by blast 
  then have "finished_item α ∈ Gen 𝔓" using Gen_def mem_Collect_eq p by blast
  then have "finished_item α ∈ ℑ" using ℑ_is_generated_by_𝔓 by blast 
  with pvalid_with show ?thesis by blast
qed
  
theorem Soundness:
  assumes finished_item_α: "finished_item α ∈ ℑ"
  shows "∃ p. pvalid_with p (finished_item α) 0 [] ∧ p ∈ ll"
proof -
  have "finished_item α ∈ Gen 𝔓"
    using ℑ_is_generated_by_𝔓 finished_item_α by auto 
  then obtain p where p: "p ∈ 𝔓 ∧ pvalid p (finished_item α)"
    using Gen_implies_pvalid by blast 
  have pvalid_p_finished_item: "pvalid  p (finished_item α)" using p by blast
  from iffD1[OF pvalid_def this, simplified] obtain r γ where pvalid:
    "wellformed_tokens p ∧
     wellformed_item (finished_item α) ∧
     r ≤ length p ∧
     length (chars p) = length Doc ∧
     chars (take r p) = [] ∧
     is_derivation (take r (terminals p) @ 𝔖 # γ) ∧ derives α (drop r (terminals p))"
     by  blast
  have "item_rule (finished_item α) ∈ ℜ" using pvalid
    using wellformed_item_def by blast
  then have "(𝔖, α) ∈ ℜ" by simp 
  then have is_derivation_α: "is_derivation α" by (simp add: is_derivation_def leftderives_rule)
  have drop_r_p_in_𝔓: "drop r p ∈ 𝔓"
    apply (rule drop_empty_tokens)
    using p apply blast
    using pvalid apply blast
    using pvalid apply simp
    by (metis append_Nil2 derives_trans is_derivation_α is_derivation_def 
      is_derivation_implies_admissible is_word_terminals_drop pvalid terminals_drop)
  then have in_ll: "drop r p ∈ ll"
    apply (auto simp add: ll_def) 
    apply (metis append_Nil append_take_drop_id chars_append pvalid) 
    using is_derivation_α pvalid
    by (metis (no_types, lifting) ℒ_def derives_trans is_derivation_def 
      is_word_terminals_drop mem_Collect_eq terminals_drop)
  have "pvalid_with (drop r p) (finished_item α) 0 []"
    apply (auto simp add: pvalid_with_def)
    using 𝔓_wellformed drop_r_p_in_𝔓 apply blast 
    using pvalid apply blast
    apply (metis append_Nil append_take_drop_id chars_append pvalid)
    apply (simp add: is_derivation_def)
    using pvalid by blast
  with in_ll show ?thesis by auto
qed

lemma is_finished_and_finished_item:
  assumes wellformed_x: "wellformed_item x"
  shows "is_finished x = (∃ α. x = finished_item α)"
proof -
  {
    assume is_finished_x: "is_finished x"
    obtain α where α: "α = item_rhs x" by blast
    have "x = finished_item α"
      apply (rule item.expand)
      apply auto
      using α is_finished_def is_finished_x item_nonterminal_def item_rhs_def apply auto[1]
      using α assms is_complete_def is_finished_def is_finished_x wellformed_item_def apply auto[1]
      using is_finished_def is_finished_x apply blast
      using is_finished_def is_finished_x by auto
    then have "∃ α. x = finished_item α" by blast
  }
  note left_implies_right = this
  {
    assume "∃ α. x = finished_item α"
    then obtain α where α: "x = finished_item α" by blast
    have "is_finished x" by (simp add: α is_finished_def is_complete_def)
  }
  note right_implies_left = this
  show ?thesis using left_implies_right right_implies_left by blast
qed 

theorem Correctness:
  shows "(ll ≠ {}) = earley_recognised"
proof -
  have 1: "(ll ≠ {}) = (∃ α. finished_item α ∈ ℑ)"
    using Soundness Completeness ex_in_conv by fastforce
  have 2: "(∃ α. finished_item α ∈ ℑ) = (∃ x ∈ ℑ. is_finished x)"
    using ℑ_def is_finished_and_finished_item wellformed_items_ℐ wellformed_items_def by auto
  show ?thesis using earley_recognised_def 1 2 by blast
qed 

end

end