Theory Derivations

theory Derivations
  imports
    CFG
begin

section ‹Adjusted content from AFP/LocalLexing›

type_synonym 'a derivation = "(nat × 'a rule) list"

lemma is_word_empty: "is_word 𝒢 []" by (auto simp add: is_word_def)

lemma derives1_implies_derives[simp]:
  "derives1 𝒢 a b ⟹ derives 𝒢 a b"
  by (auto simp add: derives_def derivations_def derivations1_def)

lemma derives_trans:
  "derives 𝒢 a b ⟹ derives 𝒢 b c ⟹ derives 𝒢 a c"
  by (auto simp add: derives_def derivations_def)

lemma derives1_eq_derivations1:
  "derives1 𝒢 x y = ((x, y) ∈ derivations1 𝒢)"
  by (simp add: derivations1_def)

lemma derives_induct[consumes 1, case_names Base Step]:
  assumes derives: "derives 𝒢 a b"
  assumes Pa: "P a"
  assumes induct: "⋀y z. derives 𝒢 a y ⟹ derives1 𝒢 y z ⟹ P y ⟹ P z"
  shows "P b"
proof -
  note rtrancl_lemma = rtrancl_induct[where a = a and b = b and r = "derivations1 𝒢" and P=P]
  from derives Pa induct rtrancl_lemma show "P b"
    by (metis derives_def derivations_def derives1_eq_derivations1)
qed

definition Derives1 :: "'a cfg ⇒ 'a list ⇒ nat ⇒ 'a rule ⇒ 'a list ⇒ bool" where
  "Derives1 𝒢 u i r v ≡ ∃ x y A α. 
    u = x @ [A] @ y ∧
    v = x @ α @ y ∧
    (A, α) ∈ set (ℜ 𝒢) ∧ r = (A, α) ∧ i = length x"  

lemma Derives1_split:
  "Derives1 𝒢 u i r v ⟹ ∃ x y. u = x @ [fst r] @ y ∧ v = x @ (snd r) @ y ∧ length x = i"
  by (metis Derives1_def fst_conv snd_conv)

lemma Derives1_implies_derives1: "Derives1 𝒢 u i r v ⟹ derives1 𝒢 u v"
  by (auto simp add: Derives1_def derives1_def)

lemma derives1_implies_Derives1: "derives1 𝒢 u v ⟹ ∃ i r. Derives1 𝒢 u i r v"
  by (auto simp add: Derives1_def derives1_def)

fun Derivation :: "'a cfg ⇒ 'a list ⇒ 'a derivation ⇒ 'a list ⇒ bool" where
  "Derivation _ a [] b = (a = b)"
| "Derivation 𝒢 a (d#D) b = (∃ x. Derives1 𝒢 a (fst d) (snd d) x ∧ Derivation 𝒢 x D b)"

lemma Derivation_implies_derives: "Derivation 𝒢 a D b ⟹ derives 𝒢 a b"
proof (induct D arbitrary: a b)
  case Nil thus ?case 
    by (simp add: derives_def derivations_def)
next
  case (Cons d D)
  note ihyps = this
  from ihyps have "∃ x. Derives1 𝒢 a (fst d) (snd d) x ∧ Derivation 𝒢 x D b" by auto
  then obtain x where "Derives1 𝒢 a (fst d) (snd d) x" and xb: "Derivation 𝒢 x D b" by blast
  with Derives1_implies_derives1 have d1: "derives 𝒢 a x" by fastforce
  from ihyps xb have d2:"derives 𝒢 x b" by simp
  show "derives 𝒢 a b" by (rule derives_trans[OF d1 d2])
qed 

lemma Derivation_Derives1: "Derivation 𝒢 a S y ⟹ Derives1 𝒢 y i r z ⟹ Derivation 𝒢 a (S@[(i,r)]) z"
proof (induct S arbitrary: a y z i r)
  case Nil thus ?case by simp
next
  case (Cons s S) thus ?case 
    by (metis Derivation.simps(2) append_Cons) 
qed

lemma derives_implies_Derivation: "derives 𝒢 a b ⟹ ∃ D. Derivation 𝒢 a D b"
proof (induct rule: derives_induct)
  case Base
  show ?case by (rule exI[where x="[]"], simp)
next
  case (Step y z)
  note ihyps = this
  from ihyps obtain D where ay: "Derivation 𝒢 a D y" by blast
  from ihyps derives1_implies_Derives1 obtain i r where yz: "Derives1 𝒢 y i r z" by blast
  from Derivation_Derives1[OF ay yz] show ?case by auto
qed

lemma Derives1_rule [elim]: "Derives1 𝒢 a i r b ⟹ r ∈ set (ℜ 𝒢)"
  using Derives1_def by metis

lemma Derivation_append: "Derivation 𝒢 a (D@E) c = (∃ b. Derivation 𝒢 a D b ∧ Derivation 𝒢 b E c)"
  by (induct D arbitrary: a c E) auto

lemma Derivation_implies_append: 
  "Derivation 𝒢 a D b ⟹ Derivation 𝒢 b E c ⟹ Derivation 𝒢 a (D@E) c"
  using Derivation_append by blast


section ‹Additional derivation lemmas›

lemma Derives1_prepend:
  assumes "Derives1 𝒢 u i r v"
  shows "Derives1 𝒢 (w@u) (i + length w) r (w@v)"
proof -
  obtain x y A α where *:
    "u = x @ [A] @ y" "v = x @ α @ y"
    "(A, α) ∈ set (ℜ 𝒢)" "r = (A, α)" "i = length x"
    using assms Derives1_def by (smt (verit))
  hence "w@u = w @ x @ [A] @ y" "w@v = w @ x @ α @ y"
    by auto
  thus ?thesis
    unfolding Derives1_def using *
    apply (rule_tac exI[where x="w@x"])
    apply (rule_tac exI[where x="y"])
    by simp
qed

lemma Derivation_prepend:
  "Derivation 𝒢 b D b' ⟹ Derivation 𝒢 (a@b) (map (λ(i, r). (i + length a, r)) D) (a@b')"
  using Derives1_prepend by (induction D arbitrary: b b') (auto, fast)

lemma Derives1_append:
  assumes "Derives1 𝒢 u i r v"
  shows "Derives1 𝒢 (u@w) i r (v@w)"
proof -
  obtain x y A α where *: 
    "u = x @ [A] @ y" "v = x @ α @ y"
    "(A, α) ∈ set (ℜ 𝒢)" "r = (A, α)" "i = length x"
    using assms Derives1_def by (smt (verit))
  hence "u@w = x @ [A] @ y @ w" "v@w = x @ α @ y @ w"
    by auto
  thus ?thesis
    unfolding Derives1_def using *
    apply (rule_tac exI[where x="x"])
    apply (rule_tac exI[where x="y@w"])
    by blast
qed

lemma Derivation_append':
  "Derivation 𝒢 a D a' ⟹ Derivation 𝒢 (a@b) D (a'@b)"
  using Derives1_append by (induction D arbitrary: a a') (auto, fast)

lemma Derivation_append_rewrite:
  assumes "Derivation 𝒢 a D (b @ c @ d) " "Derivation 𝒢 c E c'"
  shows "∃F. Derivation 𝒢 a F (b @ c' @ d)"
  using assms Derivation_append' Derivation_prepend Derivation_implies_append by fast

lemma derives1_if_valid_rule:
  "(A, α) ∈ set (ℜ 𝒢) ⟹ derives1 𝒢 [A] α"
  unfolding derives1_def
  apply (rule_tac exI[where x="[]"])
  apply (rule_tac exI[where x="[]"])
  by simp

lemma derives_if_valid_rule:
  "(A, α) ∈ set (ℜ 𝒢) ⟹ derives 𝒢 [A] α"
  using derives1_if_valid_rule by fastforce

lemma Derivation_from_empty:
  "Derivation 𝒢 [] D a ⟹ a = []"
  by (cases D) (auto simp: Derives1_def)

lemma Derivation_concat_split:
  "Derivation 𝒢 (a@b) D c ⟹ ∃E F a' b'. Derivation 𝒢 a E a' ∧ Derivation 𝒢 b F b' ∧
     c = a' @ b' ∧ length E ≤ length D ∧ length F ≤ length D"
proof (induction D arbitrary: a b)
  case Nil
  thus ?case
    by (metis Derivation.simps(1) order_refl)
next
  case (Cons d D)
  then obtain ab where *: "Derives1 𝒢 (a@b) (fst d) (snd d) ab" "Derivation 𝒢 ab D c"
    by auto
  then obtain x y A α where #:
    "a@b = x @ [A] @ y" "ab = x @ α @ y" "(A,α) ∈ set (ℜ 𝒢)" "snd d = (A,α)" "fst d = length x"
    using * unfolding Derives1_def by blast
  show ?case
  proof (cases "length a ≤ length x")
    case True
    hence ab_def: 
      "a = take (length a) x" 
      "b = drop (length a) x @ [A] @ y"
      "ab = take (length a) x @ drop (length a) x @ α @ y"
      using #(1,2) True by (metis append_eq_append_conv_if)+
    then obtain E F a' b' where IH:
      "Derivation 𝒢 (take (length a) x) E a'"
      "Derivation 𝒢 (drop (length a) x @ α @ y) F b'"
      "c = a' @ b'"
      "length E ≤ length D"
      "length F ≤ length D"
      using Cons *(2) by blast
    have "Derives1 𝒢 b (fst d - length a) (snd d) (drop (length a) x @ α @ y)"
      unfolding Derives1_def using *(1) #(3-5) ab_def(2) by (metis length_drop)
    hence "Derivation 𝒢 b ((fst d - length a, snd d) # F) b'"
      using IH(2) by force
    moreover have "Derivation 𝒢 a E a'"
      using IH(1) ab_def(1) by fastforce
    ultimately show ?thesis
      using IH(3-5) by fastforce
  next
    case False
    hence a_def: "a = x @ [A] @ take (length a - length x - 1) y"
      using #(1) append_eq_conv_conj[of a b "x @ [A] @ y"] take_all_iff take_append
      by (metis append_Cons append_Nil diff_is_0_eq le_cases take_Cons')
    hence b_def: "b = drop (length a - length x - 1) y"
      using #(1) by (metis List.append.assoc append_take_drop_id same_append_eq)
    have "ab = x @ α @ take (length a - length x - 1) y @ drop (length a - length x - 1) y"
      using #(2) by force
    then obtain E F a' b' where IH:
      "Derivation 𝒢 (x @ α @ take (length a - length x - 1) y) E a'"
      "Derivation 𝒢 (drop (length a - length x - 1) y) F b'"
      "c = a' @ b'"
      "length E ≤ length D"
      "length F ≤ length D"
      using Cons.IH[of "x @ α @ take (length a - length x - 1) y" "drop (length a - length x - 1) y"] *(2) by auto
    have "Derives1 𝒢 a (fst d) (snd d) (x @ α @ take (length a - length x - 1) y)"
      unfolding Derives1_def using #(3-5) a_def by blast
    hence "Derivation 𝒢 a ((fst d, snd d) # E) a'"
      using IH(1) by fastforce
    moreover have "Derivation 𝒢 b F b'"
      using b_def IH(2) by blast
    ultimately show ?thesis
      using IH(3-5) by fastforce
  qed
qed

lemma Derivation_𝔖1:
  assumes "Derivation 𝒢 [𝔖 𝒢] D ω" "is_word 𝒢 ω"
  shows "∃α E. Derivation 𝒢 α E ω ∧ (𝔖 𝒢,α) ∈ set (ℜ 𝒢)"
proof (cases D)
  case Nil
  thus ?thesis
    using assms by (auto simp: is_word_def nonterminals_def)
next
  case (Cons d D)
  then obtain α where "Derives1 𝒢 [𝔖 𝒢] (fst d) (snd d) α" "Derivation 𝒢 α D ω"
    using assms by auto
  hence "(𝔖 𝒢, α) ∈ set (ℜ 𝒢)"
    unfolding Derives1_def
    by (simp add: Cons_eq_append_conv)
  thus ?thesis
    using ‹Derivation 𝒢 α D ω› by auto
qed

end