Theory Validity

theory Validity 
imports LLEarleyParsing Derivations
begin

context LocalLexing begin

definition wellformed_token :: "token ⇒ bool"
where
  "wellformed_token t = is_terminal (terminal_of_token t)"

definition wellformed_tokens :: "tokens ⇒ bool"
where
  "wellformed_tokens ts = list_all wellformed_token ts"

definition doc_tokens :: "tokens ⇒ bool"
where
  "doc_tokens p = (wellformed_tokens p ∧ is_prefix (chars p) Doc)"

definition wellformed_item :: "item ⇒ bool"
where 
  "wellformed_item x = (
    item_rule x ∈ ℜ ∧ 
    item_origin x ≤ item_end x ∧ 
    item_end x ≤ length Doc ∧
    item_dot x ≤ length (item_rhs x))"

definition wellformed_items :: "items ⇒ bool"
where
  "wellformed_items X = (∀ x ∈ X. wellformed_item x)"

lemma is_word_terminals: "wellformed_tokens p ⟹ is_word (terminals p)"
by (simp add: is_word_def list_all_length terminals_def wellformed_token_def wellformed_tokens_def)

lemma is_word_subset: "is_word x ⟹ set y ⊆ set x ⟹ is_word y"
by (metis (mono_tags, opaque_lifting) in_set_conv_nth is_word_def list_all_length subsetCE)
 
lemma is_word_terminals_take: "wellformed_tokens p ⟹ is_word(terminals (take n p))"
by (metis append_take_drop_id is_word_terminals list_all_append wellformed_tokens_def)

lemma is_word_terminals_drop: "wellformed_tokens p ⟹ is_word(terminals (drop n p))"
by (metis append_take_drop_id is_word_terminals list_all_append wellformed_tokens_def)

definition pvalid :: "tokens ⇒ item ⇒ bool"
where
  "pvalid 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)))"

definition Gen :: "tokens set ⇒ items"
where
  "Gen P = { x | x p. p ∈ P ∧ pvalid p x }"

lemma "wellformed_items (Gen P)"
  by (auto simp add: Gen_def pvalid_def wellformed_items_def)

lemma "wellformed_items (Init)"
  by (auto simp add: wellformed_items_def Init_def init_item_def wellformed_item_def)

definition pvalid_left :: "tokens ⇒ item ⇒ bool"
where
  "pvalid_left 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_leftderivation (terminals (take u p) @ [item_nonterminal x] @ γ) ∧
     leftderives (item_α x) (terminals (drop u p)))"

lemma pvalid_left: "pvalid p x = pvalid_left p x"
proof -
  have right_imp_left: "pvalid_left p x ⟹ pvalid p x"
    by (meson CFG.leftderives_implies_derives CFG_axioms LocalLexing.pvalid_def 
        LocalLexing.pvalid_left_def LocalLexing_axioms leftderivation_implies_derivation)
  have left_imp_right: "pvalid p x ⟹ pvalid_left p x"
  proof -
    assume "pvalid p x"
    then obtain u γ where 
      "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))" by (simp add: pvalid_def, blast)
    thus ?thesis
      apply (auto simp add: pvalid_left_def)
      apply (rule_tac x=u in exI)
      apply auto
      apply (simp add: is_leftderivation_def)
      apply (rule_tac derives_implies_leftderives_cons[where b=γ])
      apply (erule is_word_terminals_take)
      apply (simp add: is_derivation_def)
      by (metis derives_implies_leftderives is_word_terminals_drop)
  qed
  show ?thesis by (metis left_imp_right right_imp_left)
qed
  
lemma ℒ⇩P_wellformed_tokens: "terminals p ∈ ℒ⇩P ⟹ wellformed_tokens p"
by (metis (mono_tags, lifting) ℒ⇩P_is_word is_word_def length_map list_all_length 
    nth_map terminals_def wellformed_token_def wellformed_tokens_def)

end

end