Theory Earley_Recognizer
theory Earley_Recognizer
imports
Earley_Fixpoint
begin
section ‹Earley recognizer›
subsection ‹List auxilaries›
fun filter_with_index' :: "nat ⇒ ('a ⇒ bool) ⇒ 'a list ⇒ ('a × nat) list" where
"filter_with_index' _ _ [] = []"
| "filter_with_index' i P (x#xs) = (
if P x then (x,i) # filter_with_index' (i+1) P xs
else filter_with_index' (i+1) P xs)"
definition filter_with_index :: "('a ⇒ bool) ⇒ 'a list ⇒ ('a × nat) list" where
"filter_with_index P xs = filter_with_index' 0 P xs"
lemma filter_with_index'_P:
"(x, n) ∈ set (filter_with_index' i P xs) ⟹ P x"
by (induction xs arbitrary: i) (auto split: if_splits)
lemma filter_with_index_P:
"(x, n) ∈ set (filter_with_index P xs) ⟹ P x"
by (metis filter_with_index'_P filter_with_index_def)
lemma filter_with_index'_cong_filter:
"map fst (filter_with_index' i P xs) = filter P xs"
by (induction xs arbitrary: i) auto
lemma filter_with_index_cong_filter:
"map fst (filter_with_index P xs) = filter P xs"
by (simp add: filter_with_index'_cong_filter filter_with_index_def)
lemma size_index_filter_with_index':
"(x, n) ∈ set (filter_with_index' i P xs) ⟹ n ≥ i"
by (induction xs arbitrary: i) (auto simp: Suc_leD split: if_splits)
lemma index_filter_with_index'_lt_length:
"(x, n) ∈ set (filter_with_index' i P xs) ⟹ n-i < length xs"
by (induction xs arbitrary: i)(auto simp: less_Suc_eq_0_disj split: if_splits; metis Suc_diff_Suc leI)+
lemma index_filter_with_index_lt_length:
"(x, n) ∈ set (filter_with_index P xs) ⟹ n < length xs"
by (metis filter_with_index_def index_filter_with_index'_lt_length minus_nat.diff_0)
lemma filter_with_index'_nth:
"(x, n) ∈ set (filter_with_index' i P xs) ⟹ xs ! (n-i) = x"
proof (induction xs arbitrary: i)
case (Cons y xs)
show ?case
proof (cases "x = y")
case True
thus ?thesis
using Cons by (auto simp: nth_Cons' split: if_splits)
next
case False
hence "(x, n) ∈ set (filter_with_index' (i+1) P xs)"
using Cons.prems by (cases xs) (auto split: if_splits)
hence "n ≥ i + 1" "xs ! (n - i - 1) = x"
by (auto simp: size_index_filter_with_index' Cons.IH)
thus ?thesis
by simp
qed
qed simp
lemma filter_with_index_nth:
"(x, n) ∈ set (filter_with_index P xs) ⟹ xs ! n = x"
by (metis diff_zero filter_with_index'_nth filter_with_index_def)
lemma filter_with_index_nonempty:
"x ∈ set xs ⟹ P x ⟹ filter_with_index P xs ≠ []"
by (metis filter_empty_conv filter_with_index_cong_filter list.map(1))
lemma filter_with_index'_Ex_first:
"(∃x i xs'. filter_with_index' n P xs = (x, i)#xs') ⟷ (∃x ∈ set xs. P x)"
by (induction xs arbitrary: n) auto
lemma filter_with_index_Ex_first:
"(∃x i xs'. filter_with_index P xs = (x, i)#xs') ⟷ (∃x ∈ set xs. P x)"
using filter_with_index'_Ex_first filter_with_index_def by metis
subsection ‹Definitions›