Theory Earley
theory Earley
imports
Derivations
begin
section ‹Slices›
fun slice :: "'a list ⇒ nat ⇒ nat ⇒ 'a list" where
"slice [] _ _ = []"
| "slice (x#xs) _ 0 = []"
| "slice (x#xs) 0 (Suc b) = x # slice xs 0 b"
| "slice (x#xs) (Suc a) (Suc b) = slice xs a b"
syntax
slice :: "'a list ⇒ nat ⇒ nat ⇒ 'a list" ("_⇘_'/_⇙" [1000,0,0] 1000)
notation (latex output)
"slice" ("_⇘_'/_⇙" [1000,0,0] 1000)
lemma slice_drop_take:
"slice xs a b = drop a (take b xs)"
by (induction xs a b rule: slice.induct) auto
lemma slice_append_aux:
"Suc b ≤ c ⟹ slice (x#xs) (Suc b) c = slice xs b (c-1)"
using Suc_le_D by fastforce
lemma slice_concat:
"a ≤ b ⟹ b ≤ c ⟹ slice xs a b @ slice xs b c = slice xs a c"
proof (induction xs a b arbitrary: c rule: slice.induct)
case (3 b x xs)
then show ?case
using Suc_le_D by(fastforce simp: slice_append_aux)
qed (auto simp: slice_append_aux)
lemma slice_concat_Ex:
"a ≤ c ⟹ slice xs a c = ys @ zs ⟹ ∃b. ys = slice xs a b ∧ zs = slice xs b c ∧ a ≤ b ∧ b ≤ c"
proof (induction xs a c arbitrary: ys zs rule: slice.induct)
case (3 x xs b)
show ?case
proof (cases ys)
case Nil
then obtain zs' where "x # slice xs 0 b = x # zs'" "x # zs' = zs"
using "3.prems"(2) by auto
thus ?thesis
using Nil by force
next
case (Cons y ys')
then obtain ys' where "x # slice xs 0 b = x # ys' @ zs" "x # ys' = ys"
using "3.prems"(2) by auto
thus ?thesis
using "3.IH"[of ys' zs] by force
qed
next
case (4 a b x xs)
thus ?case
by (auto, metis slice.simps(4) Suc_le_mono)
qed auto
lemma slice_nth:
"a < length xs ⟹ slice xs a (a+1) = [xs!a]"
unfolding slice_drop_take
by (metis Cons_nth_drop_Suc One_nat_def diff_add_inverse drop_take take_Suc_Cons take_eq_Nil)
lemma slice_append_nth:
"a ≤ b ⟹ b < length xs ⟹ slice xs a b @ [xs!b] = slice xs a (b+1)"
by (metis le_add1 slice_concat slice_nth)
lemma slice_empty:
"b ≤ a ⟹ slice xs a b = []"
by (simp add: slice_drop_take)
lemma slice_id[simp]:
"slice xs 0 (length xs) = xs"
by (simp add: slice_drop_take)
lemma slice_singleton:
"b ≤ length xs ⟹ [x] = slice xs a b ⟹ b = a + 1"
by (induction xs a b rule: slice.induct) (auto simp: slice_drop_take)
section ‹Earley recognizer›
subsection ‹Earley items›
definition lhs_rule :: "'a rule ⇒ 'a" where
"lhs_rule ≡ fst"
definition rhs_rule :: "'a rule ⇒ 'a list" where
"rhs_rule ≡ snd"