Theory Greibach_Normal_Form
theory Greibach_Normal_Form
imports
"Context_Free_Grammar.Context_Free_Grammar"
"Context_Free_Grammar.Epsilon_Elimination"
"Context_Free_Grammar.Replace_Terminals"
Fresh_Identifiers.Fresh_Nat
begin
declare relpowp.simps(2)[simp del]
lemma set_fold_union: "set (fold List.union xss ys) = ⋃(set ` set xss) ∪ set ys"
apply (induction xss arbitrary: ys)
by auto
lemma distinct_fold_union: "distinct (fold List.union xss ys) ⟷ distinct ys"
by (induction xss arbitrary: ys; simp)
text ‹Lemmas for @{const Option.these}:›
lemma these_eq_Collect: "Option.these X = {x. Some x ∈ X}"
by (auto simp: in_these_eq)
lemma these_image: "Option.these (f ` X) = {y. ∃x ∈ X. f x = Some y}"
by (force simp: these_eq_Collect image_def)
lemma these_eq_image_Diff: "Option.these X = the ` (X - {None})"
by (auto simp: Option.these_def)
lemma inj_on_theI: "None ∉ X ⟹ inj_on the X"
apply (auto intro!:inj_onI)
by (metis option.exhaust_sel)
lemma finite_these: "finite (Option.these X) ⟷ finite X"
by (auto simp: these_eq_image_Diff finite_image_iff inj_on_theI)
lemma finite_image_filter: "finite (Option.image_filter f X) ⟷ finite (f ` X)"
by (auto simp: Option.image_filter_eq finite_these)
section ‹Definition of Greibach Normal Forms›
text ‹This theory formalizes a method to transform a set of productions into
Greibach Normal Form (GNF) \<^cite>‹Greibach›.
A grammar is in GNF iff the rhss of each production is a terminal followed by nonterminals.›
definition GNF where
"GNF P = (∀(A,α) ∈ P. ∃a Bs. α = Tm a # map Nt Bs)"
abbreviation gnf where
"gnf P ≡ GNF (set P)"
lemma GNF_I: "(⋀A α. (A,α) ∈ P ⟹ ∃a Bs. α = Tm a # map Nt Bs) ⟹ GNF P"
by (auto simp: GNF_def)
lemma GNF_Un: "GNF (P ∪ Q) ⟷ GNF P ∧ GNF Q"
by (auto simp: GNF_def ball_Un)
text ‹We first concentrate on the essential property of the GNF:
every production starts with a ‹Tm›; the tail of a rhs can contain further terminals.
We call such grammars are \emph{head GNF}, and formalize as ‹GNF_hd› below.
This more liberal definition of GNF is also found elsewhere \cite{BlumK99}.
›
definition GNF_hd :: "('n,'t)Prods ⇒ bool" where
"GNF_hd P = (∀(A, w) ∈ P. ∃t v. w = Tm t # v)"
abbreviation gnf_hd :: "('n,'t)prods ⇒ bool" where
"gnf_hd P ≡ GNF_hd (set P)"
section ‹Transformation to Head GNF›
text ‹The algorithm to obtain head GNF consists of two phases:
▪ ‹Solve_tri› converts the productions into a ‹Triangular› form, where Nt ‹Ai› does not
depend on Nts ‹Ai, …, An›. This involves the elimination of left-recursion and is the heart
of the algorithm.
▪ ‹Expand_tri_rec› expands the triangular form by substituting in:
Due to triangular form, ‹A0› productions satisfy ‹GNF_hd› and we can substitute
them into the heads of the remaining productions. Now all ‹A1› productions satisfy ‹GNF_hd›,
and we continue until all productions satisfy ‹GNF_hd›.
This is essentially the algorithm given by Hopcroft and Ullman \cite{HopcroftU79},
except that we can drop the conversion to Chomsky Normal Form because of our more liberal ‹GNF_hd›.
›
text ‹Depend on: ‹A› depends on ‹B› if there is a rule ‹A → B w›:›
definition dep_on :: "('n,'t) Prods ⇒ 'n ⇒ 'n set" where
"dep_on P A = {B. ∃w. (A, Nt B # w) ∈ P}"
definition Subst_hd :: "('n,'t)Prods ⇒ ('n,'t)Prods ⇒ ('n,'t)Prods" where
"Subst_hd P X = P - X ∪ {(A,v@w) | A v w. ∃B. (B,v) ∈ P ∧ (A, Nt B # w) ∈ X}"
lemma Subst_hd_image_filter: "Subst_hd P X = P - X ∪
Option.image_filter
(λ((A, Nt B # α), (B',β)) ⇒ if B = B' then Some (A,β@α) else None | _ ⇒ None)
(X × P)"
apply (unfold Subst_hd_def)
apply (rule arg_cong[where f = "λx. P - X ∪ x"])
apply (auto simp add: Option.image_filter_eq these_image
prod.case_distrib[of "λx. x = _"]
list.case_distrib[of "λx. x = _"]
sym.case_distrib[of "λx. x = _"]
if_distrib[of "λx. x = _"] cong: prod.case_cong list.case_cong sym.case_cong)
apply (force)
apply (auto split: list.splits sym.splits)
done
lemma finite_Subst_hd: "finite P ⟹ finite X ⟹ finite (Subst_hd P X)"
by (auto simp: Subst_hd_image_filter finite_image_filter)
definition subst_hd :: "('n,'t)prods ⇒ ('n,'t)prods ⇒ ('n,'t)prods" where
"subst_hd ps xs = minus_list_set ps xs @
List.map_filter (λ((A,Nt B # α),(B',β)) ⇒
if B = B' then Some (A,β@α) else None | _ ⇒ None) (List.product xs ps)"
lemma set_subst_hd: "set (subst_hd ps xs) = Subst_hd (set ps) (set xs)"
by (simp add: subst_hd_def image_filter_set_eq[symmetric] Subst_hd_image_filter)
text ‹Expand head: Replace all rules ‹A → B w› where ‹B ∈ Ss›
(‹Ss› = solved Nts in ‹Triangular› form)
by ‹A → v w› where ‹B → v›. Starting from the end of ‹Ss›.›
fun Expand_hd_rec :: "'n ⇒ 'n list ⇒ ('n,'t)Prods ⇒ ('n,'t)Prods" where
"Expand_hd_rec A [] P = P" |
"Expand_hd_rec A (S#Ss) P =
(let P' = Expand_hd_rec A Ss P;
X = {r ∈ P'. ∃w. r = (A, Nt S # w)}
in Subst_hd P' X)"
fun expand_hd_rec :: "'n ⇒ 'n list ⇒ ('n,'t)prods ⇒ ('n,'t)prods" where
"expand_hd_rec A [] ps = ps" |
"expand_hd_rec A (B#Bs) ps =
(let ps' = expand_hd_rec A Bs ps;
xs = filter (λ(A', Nt B' # w) ⇒ A' = A ∧ B' = B | _ ⇒ False) ps'
in subst_hd ps' xs)"
lemma set_expand_hd_rec: "set (expand_hd_rec A Bs ps) = Expand_hd_rec A Bs (set ps)"
proof (induction Bs arbitrary: ps)
case Nil
then show ?case by simp
next
case (Cons B Bs)
have 1: "{r ∈ P'. ∃w. r = (A, Nt B # w)} = Set.filter (λ(A', Nt B' # w) ⇒ A' = A ∧ B' = B | _ ⇒ False) P'"
for P'
apply (auto)
by (simp_all split: list.splits sym.splits)
show ?case by (simp add:Let_def 1 set_subst_hd Cons)
qed
declare Expand_hd_rec.simps(1)[code]
lemma Expand_hd_rec_Cons_code[code]: "Expand_hd_rec A (S#Ss) P =
(let R' = Expand_hd_rec A Ss P;
X = {w ∈ Rhss R' A. w ≠ [] ∧ hd w = Nt S};
Y = (⋃(B,v) ∈ R'. ⋃w ∈ X. if hd w ≠ Nt B then {} else {(A,v @ tl w)})
in R' - ({A} × X) ∪ Y)"
by(simp add: Rhss_def Let_def neq_Nil_conv Ball_def hd_append Subst_hd_def split: if_splits, safe, force+)
text ‹Remove left-recursions: Remove left-recursive rules ‹A → A w›:›
definition Rm_lrec :: "'n ⇒ ('n,'t)Prods ⇒ ('n,'t)Prods" where
"Rm_lrec A P = P - {(A,Nt A # v)|v. True}"
lemma Rm_lrec_code[code]:
"Rm_lrec A P = {Aw ∈ P. let (A',w) = Aw in A' ≠ A ∨ w = [] ∨ hd w ≠ Nt A}"
by(auto simp add: Rm_lrec_def neq_Nil_conv)
definition rm_lrec :: "'n ⇒ ('n,'t) prods ⇒ ('n,'t) prods" where
"rm_lrec A ps = filter (λ(A', Nt A'' # α) ⇒ A' ≠ A ∨ A'' ≠ A | _ ⇒ True) ps"
lemma set_rm_lrec: "set (rm_lrec A ps) = Rm_lrec A (set ps)"
by (auto simp: rm_lrec_def Rm_lrec_def split: list.splits sym.splits)
text ‹Make right-recursion of left-recursion: Conversion from left-recursion to right-recursion:
Split ‹A›-rules into ‹A → u› and ‹A → A v›.
Keep ‹A → u› but replace ‹A → A v› by ‹A → u A'›, ‹A' → v›, ‹A' → v A'›.
The then part of the if statement is only an optimisation, so that we do not introduce the
‹A → u A'› rules if we do not introduce any ‹A'› rules, but the function also works, if we always
enter the else part.›
definition Rrec_of_lrec :: "'n ⇒ 'n ⇒ ('n,'t)Prods ⇒ ('n,'t)Prods" where
"Rrec_of_lrec A A' P =
(let V = {v. (A,Nt A # v) ∈ P ∧ v ≠ []};
U = {u. (A,u) ∈ P ∧ (∄v. u = Nt A # v) }
in if V = {} then {A}×U
else {A}×U ∪ {(A, u @ [Nt A'])|u. u∈U} ∪ {A'}×V ∪ {(A', v @ [Nt A']) |v. v∈V})"
lemma Rrec_of_lrec_code[code]: "Rrec_of_lrec A A' P =
(let RA = Rhss P A;
V = tl ` {w ∈ RA. w ≠ [] ∧ hd w = Nt A ∧ tl w ≠ []};
U = {u ∈ RA. u = [] ∨ hd u ≠ Nt A }
in if V = {} then {A}×U
else {A}×U ∪ {(A, u @ [Nt A'])|u. u∈U} ∪ {A'}×V ∪ {(A', v @ [Nt A']) |v. v∈V})"
proof -
let ?RA = "Rhss P A"
let ?Vc = "tl ` {w ∈ ?RA. w ≠ [] ∧ hd w = Nt A ∧ tl w ≠ []}"
let ?Uc = "{u ∈ ?RA. u = [] ∨ hd u ≠ Nt A }"
let ?V = "{v. (A,Nt A # v) ∈ P ∧ v ≠ []}"
let ?U = "{u. (A,u) ∈ P ∧ ¬(∃v. u = Nt A # v) }"
have 1: "?V = ?Vc" by (auto simp add: Rhss_def neq_Nil_conv image_def)
moreover have 2: "?U = ?Uc" by (auto simp add: Rhss_def neq_Nil_conv)
ultimately show ?thesis
unfolding Rrec_of_lrec_def Let_def by presburger
qed
definition rrec_of_lrec :: "'n ⇒ 'n ⇒ ('n,'t)prods ⇒ ('n,'t)prods" where
"rrec_of_lrec A A' ps =
(let vs = [v. (B, Nt C # v) ← ps, B = A ∧ C = A ∧ v ≠ []];
us = [u. (B,u) ← ps, B = A ∧ (case u of Nt C # w ⇒ C ≠ A | _ ⇒ True) ]
in if vs = [] then [(A,u). u ← us]
else [(A,u). u ← us] @
[(A, u @ [Nt A']). u ← us] @
[(A', v). v ← vs] @
[(A', v @ [Nt A']). v ← vs])"
lemma set_rrec_of_lrec: "set (rrec_of_lrec A A' ps) = Rrec_of_lrec A A' (set ps)"
proof-
define vs where "vs = [v. (B, Nt C # v) ← ps, B = A ∧ C = A ∧ v ≠ []]"
define us where "us = [u. (B,u) ← ps, B = A ∧ (case u of Nt C # w ⇒ C ≠ A | _ ⇒ True) ]"
have 1: "{v. (A,Nt A # v) ∈ (set ps) ∧ v ≠ []} = set vs"
by (auto simp: vs_def)
have 2: "{u. (A,u) ∈ set ps ∧ (∄v. u = Nt A # v) } = set us"
apply (auto split: list.splits sym.splits simp: neq_Nil_conv us_def)
apply (metis sym.exhaust)
by (metis neq_Nil_conv sym.exhaust)
show ?thesis
apply (unfold Rrec_of_lrec_def 1 2)
apply (unfold rrec_of_lrec_def)
apply (fold vs_def us_def)
by (auto simp add: Let_def)
qed
text ‹Solve left-recursions: Solves the left-recursion of Nt ‹A› by replacing it with a
right-recursion on a fresh Nt ‹A'›. The fresh Nt ‹A'› is also given as a parameter.›
definition Solve_lrec :: "'n ⇒ 'n ⇒ ('n,'t)Prods ⇒ ('n,'t)Prods" where
"Solve_lrec A A' P = Rm_lrec A P ∪ Rrec_of_lrec A A' P"
lemmas Solve_lrec_defs = Solve_lrec_def Rm_lrec_def Rrec_of_lrec_def Let_def Nts_def
definition solve_lrec :: "'n ⇒ 'n ⇒ ('n,'t)prods ⇒ ('n,'t)prods" where
"solve_lrec A A' P = rm_lrec A P @ rrec_of_lrec A A' P"
lemma set_solve_lrec: "set (solve_lrec A A' ps) = Solve_lrec A A' (set ps)"
by (simp add: solve_lrec_def Solve_lrec_def set_rm_lrec set_rrec_of_lrec)
text ‹Solve Triangular: Put ‹R› into Triangular form wrt ‹As› (using the new Nts ‹As'›).
In each step ‹A#As›, first the remaining Nts in ‹As› are solved, then ‹A› is solved.
This should mean that in the result of the outermost ‹Expand_hd_rec A As›, ‹A› only depends on ‹A›.
Then the ‹A› rules in the result of ‹Solve_lrec A A'› are already in GNF. More precisely:
the result should be in ‹Triangular› form.›
fun Solve_tri :: "'a list ⇒ 'a list ⇒ ('a, 'b) Prods ⇒ ('a, 'b) Prods" where
"Solve_tri (A#As) (A'#As') P = Solve_lrec A A' (Expand_hd_rec A As (Solve_tri As As' P))" |
"Solve_tri _ _ P = P"
fun solve_tri :: "'a list ⇒ 'a list ⇒ ('a, 'b) prods ⇒ ('a, 'b) prods" where
"solve_tri (A#As) (A'#As') ps = solve_lrec A A' (expand_hd_rec A As (solve_tri As As' ps))" |
"solve_tri _ _ ps = ps"
lemma set_solve_tri: "set (solve_tri As As' ps) = Solve_tri As As' (set ps)"
by (induction rule: solve_tri.induct, simp_all add: set_solve_lrec set_expand_hd_rec)
text ‹Triangular form wrt ‹[A1,…,An]› means that ‹Ai› must not depend on ‹Ai, …, An›.
In particular: ‹A0› does not depend on any ‹Ai›, its rules are already in GNF.
Therefore one can convert a ‹Triangular› form into GNF by backwards substitution:
The rules for ‹Ai› are used to expand the heads of all ‹A(i+1),…,An› rules,
starting with ‹A0›.›
fun Triangular :: "'n list ⇒ ('n × ('n, 't) sym list) set ⇒ bool" where
"Triangular [] P = True" |
"Triangular (A#As) P = (dep_on P A ∩ ({A} ∪ set As) = {} ∧ Triangular As P)"
text ‹Remove self loops: Removes all productions of the form ‹A → A›.›
definition Rm_self_loops :: "('n,'t) Prods ⇒ ('n,'t) Prods" where
"Rm_self_loops P = {(A,α)∈P. α ≠ [Nt A]}"
text ‹Expand triangular: Expands all head-Nts of productions with a Lhs in ‹As›
(‹Triangular (rev As)›). In each step ‹A#As› first all Nts in ‹As› are expanded, then every rule
‹A → B w› is expanded if ‹B ∈ set As›. If the productions were in ‹Triangular› form wrt ‹rev As›
then ‹Ai› only depends on ‹A(i+1), …, An› which have already been expanded in the first part
of the step and are in GNF. Then the all ‹A›-productions are also is in GNF after expansion.›
fun Expand_tri :: "'n list ⇒ ('n,'t)Prods ⇒ ('n,'t)Prods" where
"Expand_tri [] P = P" |
"Expand_tri (A#As) P =
(let P' = Expand_tri As P;
X = {r ∈ P'. ∃w B. r = (A, Nt B # w) ∧ B ∈ set As}
in Subst_hd P' X)"
fun expand_tri :: "'n list ⇒ ('n,'t)prods ⇒ ('n,'t)prods" where
"expand_tri [] P = P" |
"expand_tri (A#As) P =
(let P' = expand_tri As P;
X = filter (λ(A',Nt B # α) ⇒ A' = A ∧ B ∈ set As | _ ⇒ False) P'
in subst_hd P' X)"
lemma set_expand_tri: "set (expand_tri As P) = Expand_tri As (set P)"
proof-
have 1: "(∃w B. r = (A, Nt B # w) ∧ B ∈ X) =
(case r of (A',Nt B # α) ⇒ A' = A ∧ B ∈ X | _ ⇒ False)" for r A X
apply (auto simp: neq_Nil_conv split: list.splits sym.splits)
apply (metis destTm.cases)
by (metis sym.exhaust)
show ?thesis
by (induction rule: expand_tri.induct, simp_all add: set_subst_hd Let_def 1 )
qed
declare Expand_tri.simps(1)[code]
lemma Expand_tri_Cons_code[code]: "Expand_tri (S#Ss) R =
(let P' = Expand_tri Ss R;
X = {w ∈ Rhss P' S. w ≠ [] ∧ hd w ∈ Nt ` set Ss};
Y = (⋃(B,v) ∈ P'. ⋃w ∈ X. if hd w ≠ Nt B then {} else {(S,v @ tl w)})
in P' - ({S} × X) ∪ Y)"
by(simp add: Let_def Rhss_def neq_Nil_conv Ball_def Subst_hd_def, safe, force+)
text ‹The main function ‹GNF_hd_of› converts into ‹GNF_hd›:›
definition GNF_hd_of :: "'n::fresh list ⇒ ('n,'t) Prods ⇒ ('n,'t) Prods" where
"GNF_hd_of As P =
(let As' = freshs (set As) As
in Expand_tri (As' @ rev As) (Solve_tri As As' (Eps_elim P)))"
definition gnf_hd_of :: "('n::fresh,'t)prods ⇒ ('n,'t)prods" where
"gnf_hd_of P =
(let As = nts P; As' = freshs (set As) As
in expand_tri (As' @ rev As) (solve_tri As As' (eps_elim P)))"
lemma set_gnf_hd_of: "set (gnf_hd_of P) = GNF_hd_of (nts P) (set P)"
by (simp add: GNF_hd_of_def gnf_hd_of_def set_expand_tri set_solve_tri set_eps_elim Let_def)
section ‹Some Basic Lemmas›
subsection ‹‹Eps_free› preservation›
lemma Eps_free_Expand_hd_rec: "Eps_free R ⟹ Eps_free (Expand_hd_rec A Ss R)"
by (induction A Ss R rule: Expand_hd_rec.induct)
(auto simp add: Eps_free_def Let_def Subst_hd_def)
lemma Eps_free_Solve_lrec: "Eps_free R ⟹ Eps_free (Solve_lrec A A' R)"
unfolding Solve_lrec_defs Eps_free_def by (auto)
lemma Eps_free_Solve_tri: "Eps_free R ⟹ Eps_free (Solve_tri As As' R)"
by (induction As As' R rule: Solve_tri.induct)
(auto simp add: Eps_free_Solve_lrec Eps_free_Expand_hd_rec)
lemma Eps_free_Expand_tri: "Eps_free R ⟹ Eps_free (Expand_tri As R)"
by (induction As R rule: Expand_tri.induct) (auto simp add: Let_def Eps_free_def Subst_hd_def)
subsection ‹Lemmas about ‹Nts› and ‹dep_on››
lemma dep_on_Un[simp]: "dep_on (R ∪ S) A = dep_on R A ∪ dep_on S A"
by(auto simp add: dep_on_def)
lemma dep_on_empty[simp]: "dep_on {} A = {}"
by (simp add: dep_on_def)
lemma dep_on_insert: "dep_on (insert (A,w) P) A' =
(if A = A' then case w of Nt B # w' ⇒ {B} | _ ⇒ {} else {}) ∪ dep_on P A'"
by (auto simp: dep_on_def split: list.splits sym.splits)
lemma Expand_hd_rec_preserves_neq: "B ≠ A ⟹ (B,w) ∈ Expand_hd_rec A Ss R ⟷ (B,w) ∈ R"
by(induction A Ss R rule: Expand_hd_rec.induct) (auto simp add: Let_def Subst_hd_def)
text ‹Let ‹R› be epsilon-free and in ‹Triangular› form wrt ‹Bs›.
After ‹Expand_hd_rec A Bs R›, ‹A› depends only on what ‹A› depended on before or
what one of the ‹B ∈ Bs› depends on, but ‹A› does not depend on the ‹Bs›:›
lemma dep_on_Expand_hd_rec:
"⟦ Eps_free R; Triangular Bs R; distinct Bs; A ∉ set Bs ⟧
⟹ dep_on (Expand_hd_rec A Bs R) A ⊆ (dep_on R A ∪ (⋃B∈set Bs. dep_on R B)) - set Bs"
proof(induction A Bs R rule: Expand_hd_rec.induct)
case (1 A R)
then show ?case by simp
next
case (2 A B Bs R)
then show ?case
by(fastforce simp add: Let_def dep_on_def Cons_eq_append_conv Eps_free_Expand_hd_rec Eps_free_Nil
Subst_hd_def Expand_hd_rec_preserves_neq set_eq_iff)
qed
lemma Expand_hd_rec_id: "dep_on P A ∩ set As = {} ⟹ Expand_hd_rec A As P = P"
by (induction As, auto simp: dep_on_def Subst_hd_def)
lemma dep_on_subs_Nts: "dep_on R A ⊆ Nts R"
by (auto simp add: Nts_def dep_on_def)
section ‹Transformations and Symbols›
lemma Lhss_Subst_hd: "Lhss (Subst_hd P X) ⊆ Lhss P ∪ Lhss X"
by (auto simp: Lhss_def Subst_hd_def)
lemma Rhs_Nts_Subst_hd: "Rhs_Nts (Subst_hd P X) ⊆ Rhs_Nts P ∪ Rhs_Nts X"
by (auto simp: Subst_hd_def Rhs_Nts_def Nts_syms_def split: prod.splits)
lemma Nts_Subst_hd: "Nts (Subst_hd P X) ⊆ Nts P ∪ Nts X"
using Un_mono[OF Lhss_Subst_hd Rhs_Nts_Subst_hd]
by (simp add: Nts_Lhss_Rhs_Nts ac_simps)
lemma Tms_Subst_hd: "Tms (Subst_hd P X) ⊆ Tms P ∪ Tms X"
by (auto simp: Subst_hd_def Tms_def Tms_syms_def split: prod.splits)
lemma Lhss_Expand_hd_rec: "Lhss (Expand_hd_rec A Ss P) ⊆ Lhss P"
and Tms_Expand_hd_rec: "Tms (Expand_hd_rec A Ss P) ⊆ Tms P"
and Rhs_Nts_Expand_hd_rec: "Rhs_Nts (Expand_hd_rec A Ss P) ⊆ Rhs_Nts P"
proof (atomize(full), induction Ss arbitrary: P)
case Nil
show ?case by simp
next
case (Cons S Ss)
define P' where "P' = Expand_hd_rec A Ss P"
define X where "X = {r ∈ P'. ∃w. r = (A, Nt S # w)}"
have "Lhss X ⊆ Lhss P'" and "Tms X ⊆ Tms P'" and "Rhs_Nts X ⊆ Rhs_Nts P'"
by (auto simp: X_def Lhss_def Tms_def Tms_syms_def Rhs_Nts_def Nts_syms_def)
moreover from Cons
have "Lhss P' ⊆ Lhss P" and "Tms P' ⊆ Tms P" and "Rhs_Nts P' ⊆ Rhs_Nts P" by (auto simp: P'_def)
ultimately show ?case
by (auto simp flip: P'_def X_def dest!: subsetD[OF Lhss_Subst_hd] subsetD[OF Tms_Subst_hd] subsetD[OF Rhs_Nts_Subst_hd])
qed
lemma Nts_Expand_hd_rec: "Nts (Expand_hd_rec A Ss P) ⊆ Nts P"
using Un_mono[OF Lhss_Expand_hd_rec Rhs_Nts_Expand_hd_rec]
by (simp add: Nts_Lhss_Rhs_Nts ac_simps)
lemma Tms_Solve_lrec: "Tms (Solve_lrec A A' P) ⊆ Tms P"
by (auto simp: Tms_def Tms_syms_def Solve_lrec_defs)
lemma Lhss_Solve_lrec: "Lhss (Solve_lrec A A' P) ⊆ Lhss P ∪ {A'}"
by (auto simp: Lhss_def Solve_lrec_defs)
lemma Rhs_Nts_Solve_lrec: "Rhs_Nts (Solve_lrec A A' P) ⊆ Rhs_Nts P ∪ {A'}"
by (auto simp: Rhs_Nts_def Solve_lrec_defs)
lemma Nts_Solve_lrec: "Nts (Solve_lrec A A' P) ⊆ Nts P ∪ {A'}"
using Lhss_Solve_lrec[of A A' P] Rhs_Nts_Solve_lrec[of A A' P]
by (auto simp: Nts_Lhss_Rhs_Nts)
lemma Lhss_Solve_tri: "Lhss (Solve_tri As As' P) ⊆ Lhss P ∪ set As'"
and Tms_Solve_tri: "Tms (Solve_tri As As' P) ⊆ Tms P"
and Rhs_Nts_Solve_tri: "Rhs_Nts (Solve_tri As As' P) ⊆ Rhs_Nts P ∪ set As'"
apply (induction rule: Solve_tri.induct)
by (auto dest!:
subsetD[OF Lhss_Solve_lrec] subsetD[OF Lhss_Expand_hd_rec]
subsetD[OF Tms_Solve_lrec] subsetD[OF Tms_Expand_hd_rec]
subsetD[OF Rhs_Nts_Solve_lrec] subsetD[OF Rhs_Nts_Expand_hd_rec])
lemma Nts_Solve_tri: "Nts (Solve_tri As As' P) ⊆ Nts P ∪ set As'"
using Lhss_Solve_tri[of As As' P] Rhs_Nts_Solve_tri[of As As' P]
by (auto simp: Nts_Lhss_Rhs_Nts)
lemma Lhss_Expand_tri: "Lhss (Expand_tri As P) ⊆ Lhss P"
and Tms_Expand_tri: "Tms (Expand_tri As P) ⊆ Tms P"
and Rhs_Nts_Expand_tri: "Rhs_Nts (Expand_tri As P) ⊆ Rhs_Nts P"
proof (atomize(full), induction As)
case Nil
show ?case by simp
next
case (Cons A As)
define P' where "P' = Expand_tri As P"
define X where "X = {r ∈ P'. ∃w B. r = (A, Nt B # w) ∧ B ∈ set As}"
from Cons have 1: "Lhss P' ⊆ Lhss P" "Tms P' ⊆ Tms P" "Rhs_Nts P' ⊆ Rhs_Nts P"
by (auto simp: P'_def)
have 2: "Lhss X ⊆ Lhss P'" "Tms X ⊆ Tms P'" "Rhs_Nts X ⊆ Rhs_Nts P'"
by (auto simp: X_def Lhss_def Tms_def Rhs_Nts_def)
show ?case
by (auto simp flip: P'_def X_def
dest!: subsetD[OF Lhss_Subst_hd] subsetD[OF Tms_Subst_hd] subsetD[OF Rhs_Nts_Subst_hd]
1[THEN subsetD] 2[THEN subsetD])
qed
lemma Nts_Expand_tri: "Nts (Expand_tri As P) ⊆ Nts P"
using Lhss_Expand_tri[of As P] Rhs_Nts_Expand_tri[of As P]
by (auto simp: Nts_Lhss_Rhs_Nts)
lemma Lhss_GNF_hd_of: "Lhss (GNF_hd_of As P) ⊆ Lhss P ∪ set (freshs (set As) As)"
by (auto simp: GNF_hd_of_def Let_def
dest!: subsetD[OF Lhss_Expand_tri] subsetD[OF Lhss_Solve_tri] subsetD[OF Lhss_Eps_elim])
lemma Rhs_Nts_GNF_hd_of: "Rhs_Nts (GNF_hd_of As P) ⊆ Rhs_Nts P ∪ set (freshs (set As) As)"
by (auto simp: GNF_hd_of_def Let_def
dest!: subsetD[OF Rhs_Nts_Expand_tri] subsetD[OF Rhs_Nts_Solve_tri] subsetD[OF Rhs_Nts_Eps_elim])
lemma Tms_GNF_hd_of: "Tms (GNF_hd_of As P) ⊆ Tms P"
by (auto simp: GNF_hd_of_def Let_def
dest!: subsetD[OF Tms_Expand_tri] subsetD[OF Tms_Solve_tri] subsetD[OF Tms_Eps_elim])
lemma Nts_GNF_hd_of: "Nts (GNF_hd_of As P) ⊆ Nts P ∪ set (freshs (set As) As)"
using Lhss_GNF_hd_of[of As P] Rhs_Nts_GNF_hd_of[of As P]
by (auto simp: Nts_Lhss_Rhs_Nts)
subsection ‹Lemmas about ‹Triangular››
lemma tri_Snoc_impl_tri: "Triangular (As @ [A]) R ⟹ Triangular As R"
by (induction As R rule: Triangular.induct, auto)
text ‹If two parts of the productions are ‹Triangular› and no Nts from the first part depend on
ones of the second they are also ‹Triangular› when put together.›
lemma Triangular_append:
"⟦Triangular As R; Triangular Bs R; ∀A∈set As. dep_on R A ∩ set Bs = {}⟧
⟹ Triangular (As@Bs) R"
by (induction As) auto
section ‹Function ‹Solve_tri›: Remove Left-Recursion and Convert into Triangular Form›
subsection ‹Basic Lemmas›
text ‹Mostly about rule inclusions in ‹Solve_lrec›.›
lemma Solve_lrec_rule_simp1: "A ≠ B ⟹ A ≠ B' ⟹ (A, w) ∈ Solve_lrec B B' R ⟷ (A, w) ∈ R"
unfolding Solve_lrec_defs by (auto)
lemma Solve_lrec_rule_simp3: "A ≠ A' ⟹ A' ∉ Nts R ⟹ Eps_free R
⟹ (A, [Nt A']) ∉ Solve_lrec A A' R"
unfolding Solve_lrec_defs by (auto simp: Eps_free_def)
lemma Solve_lrec_rule_simp7: "A' ≠ A ⟹ A' ∉ Nts R ⟹ (A', Nt A' # w) ∉ Solve_lrec A A' R"
unfolding Solve_lrec_defs by(auto simp: neq_Nil_conv split: prod.splits)
lemma Solve_lrec_rule_simp8: "A' ∉ Nts R ⟹ B ≠ A' ⟹ B ≠ A
⟹ (B, Nt A' # w) ∉ Solve_lrec A A' R"
unfolding Solve_lrec_defs by (auto split: prod.splits)
lemma dep_on_Expand_hd_rec_simp2: "B ≠ A ⟹ dep_on (Expand_hd_rec A As R) B = dep_on R B"
by (auto simp add: dep_on_def Expand_hd_rec_preserves_neq)
lemma dep_on_Solve_lrec_simp2: "A ≠ B ⟹ A' ≠ B ⟹ dep_on (Solve_lrec A A' R) B = dep_on R B"
unfolding Solve_lrec_defs dep_on_def by (auto)
lemma Solve_lrec_id: "A ∉ dep_on P A ⟹ Solve_lrec A A' P = P"
by (auto simp: Solve_lrec_defs dep_on_def)
lemma Solve_tri_id:
"⟦Triangular As P; length As' = length As⟧ ⟹ Solve_tri As As' P = P"
by (induction rule: Solve_tri.induct, simp_all add: Expand_hd_rec_id Solve_lrec_id)
subsection ‹Triangular Form›
text
‹‹Expand_hd_rec› preserves ‹Triangular›, if it does not expand a Nt considered in ‹Triangular›.›
lemma Triangular_Expand_hd_rec: "⟦A ∉ set As; Triangular As R⟧ ⟹ Triangular As (Expand_hd_rec A Bs R)"
by (induction As) (auto simp add: dep_on_Expand_hd_rec_simp2)
text ‹Solving a Nt not considered by ‹Triangular› preserves the ‹Triangular› property.›
lemma Triangular_Solve_lrec: "⟦A ∉ set As; A' ∉ set As; Triangular As R⟧
⟹ Triangular As (Solve_lrec A A' R)"
proof(induction As)
case Nil
then show ?case by simp
next
case (Cons a As)
have "Triangular (a # As) (Solve_lrec A A' R) =
(dep_on (Solve_lrec A A' R) a ∩ ({a} ∪ set As) = {} ∧ Triangular As (Solve_lrec A A' R))"
by simp
also have "... = (dep_on (Solve_lrec A A' R) a ∩ ({a} ∪ set As) = {})" using Cons by auto
also have "... = (dep_on R a ∩ ({a} ∪ set As) = {})" using Cons dep_on_Solve_lrec_simp2
by (metis list.set_intros(1))
then show ?case using Cons by auto
qed
text ‹Solving more Nts does not remove the ‹Triangular› property of previously solved Nts.›
lemma part_Triangular_induct_step:
"⟦Eps_free R; distinct ((A#As)@(A'#As')); Triangular As (Solve_tri As As' R)⟧
⟹ Triangular As (Solve_tri (A#As) (A'#As') R)"
by (cases "As = []")
(auto simp add: Triangular_Expand_hd_rec Triangular_Solve_lrec)
text ‹Couple of small lemmas about ‹dep_on› and the solving of left-recursion.›
lemma Rm_lrec_rem_own_dep: "A ∉ dep_on (Rm_lrec A R) A"
by (auto simp add: dep_on_def Rm_lrec_def)
lemma Rrec_of_lrec_has_no_own_dep: "A ≠ A' ⟹ A ∉ dep_on (Rrec_of_lrec A A' R) A"
by (auto simp add: dep_on_def Rrec_of_lrec_def Let_def Cons_eq_append_conv)
lemma Solve_lrec_no_own_dep: "A ≠ A' ⟹ A ∉ dep_on (Solve_lrec A A' R) A"
by (auto simp add: Solve_lrec_def Rm_lrec_rem_own_dep Rrec_of_lrec_has_no_own_dep)
lemma Solve_lrec_no_new_own_dep: "A ≠ A' ⟹ A' ∉ Nts R ⟹ A' ∉ dep_on (Solve_lrec A A' R) A'"
by (auto simp add: dep_on_def Solve_lrec_rule_simp7)
lemma dep_on_rem_lrec_simp: "dep_on (Rm_lrec A R) A = dep_on R A - {A}"
by (auto simp add: dep_on_def Rm_lrec_def)
lemma dep_on_Rrec_of_lrec_simp:
"Eps_free R ⟹ A ≠ A' ⟹ dep_on (Rrec_of_lrec A A' R) A = dep_on R A - {A}"
using Eps_freeE_Cons[of R A "[]"]
by (auto simp add: dep_on_def Rrec_of_lrec_def Let_def Cons_eq_append_conv)
lemma dep_on_Solve_lrec_simp:
"⟦Eps_free R; A ≠ A'⟧ ⟹ dep_on (Solve_lrec A A' R) A = dep_on R A - {A}"
by (simp add: dep_on_rem_lrec_simp dep_on_Rrec_of_lrec_simp Solve_lrec_def)
lemma dep_on_Solve_tri_simp: "B ∉ set As ⟹ B ∉ set As'
⟹ dep_on (Solve_tri As As' R) B = dep_on R B"
proof (induction As As' R rule: Solve_tri.induct)
case *: (1 A As A' As' R)
have "dep_on (Solve_tri (A#As) (A'#As') R) B = dep_on (Expand_hd_rec A As (Solve_tri As As' R)) B"
using * by (auto simp add: dep_on_Solve_lrec_simp2)
then show ?case using * by (auto simp add: dep_on_Expand_hd_rec_simp2)
qed auto
text ‹Induction step for showing that ‹Solve_tri› removes dependencies of previously solved Nts.›
lemma Triangular_dep_on_induct_step:
assumes "Eps_free R" "distinct ((A#As)@A'#As')" "Triangular As (Solve_tri As As' R)"
shows "dep_on (Solve_tri (A # As) (A' # As') R) A ∩ ({A} ∪ set As) = {}"
proof(cases "As = []")
case True
with assms Solve_lrec_no_own_dep show ?thesis by fastforce
next
case False
have "Eps_free (Solve_tri As As' R)"
using assms Eps_free_Solve_tri by auto
then have test: "X ∈ set As ⟹ X ∉ dep_on (Expand_hd_rec A As (Solve_tri As As' R)) A" for X
using assms dep_on_Expand_hd_rec
by (metis distinct.simps(2) distinct_append insert_Diff subset_Diff_insert)
have A: "Triangular As (Solve_tri (A # As) (A' # As') R)"
using part_Triangular_induct_step assms by metis
have "dep_on (Solve_tri (A # As) (A' # As') R) A ∩ ({A} ∪ set As)
= (dep_on (Expand_hd_rec A As (Solve_tri As As' R)) A - {A}) ∩ ({A} ∪ set As)"
using assms by (simp add: dep_on_Solve_lrec_simp Eps_free_Solve_tri Eps_free_Expand_hd_rec)
also have "... = dep_on (Expand_hd_rec A As (Solve_tri As As' R)) A ∩ set As"
using assms by auto
also have "... = {}" using test by fastforce
finally show ?thesis by auto
qed
theorem Triangular_Solve_tri_orig:
"⟦ Eps_free P; length As ≤ length As'; distinct(As @ As')⟧
⟹ Triangular As (Solve_tri As As' P)"
proof(induction As As' P rule: Solve_tri.induct)
case *: (1 A As A' As' R)
then have "length As ≤ length As' ∧ distinct (As @ As')" by auto
then have A: "Triangular As (Solve_tri (A # As) (A' # As') R)"
using part_Triangular_induct_step * by metis
have "(dep_on (Solve_tri (A # As) (A' # As') R) A ∩ ({A} ∪ set As) = {})"
using Triangular_dep_on_induct_step *
by (metis ‹length As ≤ length As' ∧ distinct (As @ As')›)
then show ?case using A by simp
qed auto
lemma dep_on_Solve_tri_Nts_R:
"⟦Eps_free R; B ∈ set As; distinct (As @ As'); set As' ∩ Nts R = {}; length As ≤ length As'⟧
⟹ dep_on (Solve_tri As As' R) B ⊆ Nts R"
proof (induction As As' R arbitrary: B rule: Solve_tri.induct)
case *: (1 A As A' As' R)
then have F1: "dep_on (Solve_tri As As' R) B ⊆ Nts R"
by (cases "B = A") (simp_all add: dep_on_Solve_tri_simp dep_on_subs_Nts)
then have F2: "dep_on (Expand_hd_rec A As (Solve_tri As As' R)) B ⊆ Nts R"
proof (cases "B = A")
case True
have "Triangular As (Solve_tri As As' R)" using * by (auto simp add: Triangular_Solve_tri_orig)
then have "dep_on (Expand_hd_rec A As (Solve_tri As As' R)) B ⊆ dep_on (Solve_tri As As' R) B
∪ ⋃ (dep_on (Solve_tri As As' R) ` set As) - set As"
using * True by (auto simp add: dep_on_Expand_hd_rec Eps_free_Solve_tri)
also have "... ⊆ Nts R" using * F1 by auto
finally show ?thesis.
next
case False
then show ?thesis using F1 by (auto simp add: dep_on_Expand_hd_rec_simp2)
qed
then have "dep_on (Solve_lrec A A' (Expand_hd_rec A As (Solve_tri As As' R))) B ⊆ Nts R"
proof (cases "B = A")
case True
then show ?thesis
using * F2 by (auto simp add: dep_on_Solve_lrec_simp Eps_free_Solve_tri Eps_free_Expand_hd_rec)
next
case False
have "B ≠ A'" using * by auto
then show ?thesis using * F2 False by (simp add: dep_on_Solve_lrec_simp2)
qed
then show ?case by simp
qed auto
lemma Triangular_unused_Nts: "set As ∩ Nts R = {} ⟹ Triangular As R"
proof (induction As)
case Nil
then show ?case by auto
next
case (Cons a As)
have "dep_on R a ⊆ Nts R" by (simp add: dep_on_subs_Nts)
then have "dep_on R a ∩ (set As ∪ {a}) = {}" using Cons by auto
then show ?case using Cons by auto
qed
text ‹The newly added Nts in ‹Solve_lrec› are in ‹Triangular› form wrt ‹rev As'›.›
lemma Triangular_Solve_tri_new:
"⟦set As' ∩ Nts R = {}; distinct (As @ As')⟧
⟹ Triangular (rev As') (Solve_tri As As' R)"
proof (induction As As' R rule: Solve_tri.induct)
case *: (1 A As A' As' R)
then have "Triangular (rev As') (Solve_tri As As' R)" by simp
then have "Triangular (rev As') (Expand_hd_rec A As (Solve_tri As As' R))"
using * by (auto simp add: Triangular_Expand_hd_rec)
then have F1: "Triangular (rev As') (Solve_tri (A#As) (A'#As') R)"
using * by (auto simp add: Triangular_Solve_lrec)
have "Nts (Solve_tri As As' R) ⊆ Nts R ∪ set As'" using * by (auto simp add: Nts_Solve_tri)
then have F_nts: "Nts (Expand_hd_rec A As (Solve_tri As As' R)) ⊆ Nts R ∪ set As'"
using Nts_Expand_hd_rec[of A As "(Solve_tri As As' R)"] by auto
then have "A' ∉ dep_on (Solve_lrec A A' (Expand_hd_rec A As (Solve_tri As As' R))) A'"
using * Solve_lrec_no_new_own_dep[of A A'] by auto
then have F2: "Triangular [A'] (Solve_tri (A#As) (A'#As') R)" by auto
have "∀a∈set As'. dep_on (Solve_tri (A#As) (A'#As') R) a ∩ set [A'] = {}"
proof
fix a
assume "a ∈ set As'"
then have "A' ∉ Nts (Expand_hd_rec A As (Solve_tri As As' R)) ∧ a ≠ A" using F_nts * by auto
then show "dep_on (Solve_tri (A#As) (A'#As') R) a ∩ set [A'] = {}"
using * Solve_lrec_rule_simp8[of A' "(Expand_hd_rec A As (Solve_tri As As' R))" a A]
Solve_lrec_rule_simp7[of A']
by (cases "a = A'") (auto simp add: dep_on_def)
qed
then have "Triangular (rev (A'#As')) (Solve_tri (A#As) (A'#As') R)"
using F1 F2 by (auto simp add: Triangular_append)
then show ?case by auto
qed (auto simp add:Triangular_unused_Nts)
text ‹The entire set of productions is in ‹Triangular› form after ‹Solve_tri› wrt ‹As@(rev As')›.›
theorem Triangular_Solve_tri:
assumes "Eps_free P" "length As ≤ length As'" "distinct(As @ As')" "Nts P ⊆ set As"
shows "Triangular (As@(rev As')) (Solve_tri As As' P)"
proof -
from assms have 1: "Triangular As (Solve_tri As As' P)" by (auto simp add: Triangular_Solve_tri_orig)
have "set As' ∩ Nts P = {}" using assms by auto
then have 2: "Triangular (rev As') (Solve_tri As As' P)"
using assms by (auto simp add: Triangular_Solve_tri_new)
have "set As' ∩ Nts P = {}" using assms by auto
then have "∀A∈set As. dep_on (Solve_tri As As' P) A ⊆ Nts P"
using assms by (auto simp add: dep_on_Solve_tri_Nts_R)
then have "∀A∈set As. dep_on (Solve_tri As As' P) A ∩ set As' = {}" using assms by auto
then show ?thesis using 1 2 by (auto simp add: Triangular_append)
qed
subsection ‹‹Solve_lrec› Preserves Language›
subsubsection ‹@{prop "Lang (Solve_lrec B B' R) A ⊇ Lang R A"}›
text ‹Restricted to productions with one lhs (‹A›), and no ‹A → A› productions
if there is a derivation from ‹u› to ‹A # v› then ‹u› must start with Nt ‹A›.›
lemma lrec_lemma1:
assumes "S = {x. (∃v. x = (A, v) ∧ x ∈ R)}" "Rm_self_loops S ⊢ u ⇒l(n) Nt A#v"
shows "∃u'. u = Nt A # u'"
proof (rule ccontr)
assume neg: "∄u'. u = Nt A # u'"
show "False"
proof (cases "u = []")
case True
then show ?thesis using assms by simp
next
case False
then show ?thesis
proof (cases "∃t. hd u = Tm t")
case True
then show ?thesis using assms neg
by (metis (no_types, lifting) False deriveln_Tm_Cons hd_Cons_tl list.inject)
next
case False
then have "∃B u'. u = Nt B # u' ∧ B ≠ A" using assms neg
by (metis deriveln_from_empty list.sel(1) neq_Nil_conv sym.exhaust)
then obtain B u' where B_not_A: "u = Nt B # u' ∧ B ≠ A" by blast
then have "∃w. (B, w) ∈ Rm_self_loops S" using assms neg
by (metis (no_types, lifting) derivels_Nt_Cons relpowp_imp_rtranclp)
then obtain w where elem: "(B, w) ∈ Rm_self_loops S" by blast
have "(B, w) ∉ Rm_self_loops S" using B_not_A assms by (auto simp add: Rm_self_loops_def)
then show ?thesis using elem by simp
qed
qed
qed
text ‹Restricted to productions with one lhs (‹A›), and no ‹A → A› productions
if there is a derivation from ‹u› to ‹A # v› then ‹u› must start with Nt ‹A› and there
exists a prefix of ‹A # v› s.t. a left-derivation from ‹[Nt A]› to that prefix exists.›
lemma lrec_lemma2:
assumes "S = {x. (∃v. x = (A, v) ∧ x ∈ R)}" "Eps_free R"
shows "Rm_self_loops S ⊢ u ⇒l(n) Nt A#v ⟹
∃u' v'. u = Nt A # u' ∧ v = v' @ u' ∧ (Rm_self_loops S) ⊢ [Nt A] ⇒l(n) Nt A # v'"
proof (induction n arbitrary: u)
case 0
then show ?case by simp
next
case (Suc n)
have "∃u'. u = Nt A # u'" using lrec_lemma1[of S] Suc assms by auto
then obtain u' where u'_prop: "u = Nt A # u'" by blast
then have "∃w. (A,w) ∈ (Rm_self_loops S) ∧ (Rm_self_loops S) ⊢ w @ u' ⇒l(n) Nt A # v"
using Suc by (auto simp add: deriveln_Nt_Cons split: prod.split)
then obtain w where w_prop:
"(A,w) ∈ (Rm_self_loops S) ∧ (Rm_self_loops S) ⊢ w @ u' ⇒l(n) Nt A # v"
by blast
then have "∃u'' v''. w @ u' = Nt A # u'' ∧ v = v'' @ u'' ∧
(Rm_self_loops S) ⊢ [Nt A] ⇒l(n) Nt A # v''"
using Suc.IH Suc by auto
then obtain u'' v'' where u''_prop: "w @ u' = Nt A # u'' ∧ v = v'' @ u''" and
ln_derive: "(Rm_self_loops S) ⊢ [Nt A] ⇒l(n) Nt A # v''"
by blast
have "w ≠ [] ∧ w ≠ [Nt A]"
using Suc w_prop assms by (auto simp add: Eps_free_Nil Rm_self_loops_def split: prod.splits)
then have "∃u1. u1 ≠ [] ∧ w = Nt A # u1 ∧ u'' = u1 @ u'"
using u''_prop by (metis Cons_eq_append_conv)
then obtain u1 where u1_prop: "u1 ≠ [] ∧ w = Nt A # u1 ∧ u'' = u1 @ u'" by blast
then have 1: "u = Nt A # u' ∧ v = (v'' @ u1) @ u'" using u'_prop u''_prop by auto
have 2: "(Rm_self_loops S) ⊢ [Nt A] @ u1 ⇒l(n) Nt A # v'' @ u1"
using ln_derive deriveln_append
by fastforce
have "(Rm_self_loops S) ⊢ [Nt A] ⇒l [Nt A] @ u1"
using w_prop u''_prop u1_prop
by (simp add: derivel_Nt_Cons)
then have "(Rm_self_loops S) ⊢ [Nt A] ⇒l(Suc n) Nt A # v'' @ u1"
using ln_derive
by (meson 2 relpowp_Suc_I2)
then show ?case using 1 by blast
qed
text ‹Restricted to productions with one lhs (‹A›), and no ‹A → A› productions
if there is a left-derivation from ‹[Nt A]› to ‹A # u› then there exists a derivation
from ‹[Nt A']› to ‹u@[Nt A]› and if ‹u ≠ []› also to ‹u› in ‹Solve_lrec A A' R›.›
lemma lrec_lemma3:
assumes "S = {x. (∃v. x = (A, v) ∧ x ∈ R)}" "Eps_free R"
shows "Rm_self_loops S ⊢ [Nt A] ⇒l(n) Nt A # u
⟹ Solve_lrec A A' S ⊢ [Nt A'] ⇒(n) u @ [Nt A'] ∧
(u ≠ [] ⟶ Solve_lrec A A' S ⊢ [Nt A'] ⇒(n) u)"
proof(induction n arbitrary: u)
case 0
then show ?case by (simp)
next
case (Suc n)
then have "∃w. (A,w) ∈ Rm_self_loops S ∧ Rm_self_loops S ⊢ w ⇒l(n) Nt A # u"
by (auto simp add: deriveln_Nt_Cons split: prod.splits)
then obtain w where w_prop1: "(A,w) ∈ (Rm_self_loops S) ∧ (Rm_self_loops S) ⊢ w ⇒l(n) Nt A#u"
by blast
then have "∃w' u'. w = Nt A # w' ∧ u = u' @ w' ∧ (Rm_self_loops S) ⊢ [Nt A] ⇒l(n) Nt A # u'"
using lrec_lemma2[of S] Suc assms by auto
then obtain w' u' where w_prop2: "w = Nt A # w' ∧ u = u' @ w'" and
ln_derive: "Rm_self_loops S ⊢ [Nt A] ⇒l(n) Nt A # u'" by blast
then have "w' ≠ []" using w_prop1 Suc by (auto simp add: Rm_self_loops_def)
have "(A, w) ∈ S" using Suc.prems(1) w_prop1 by (auto simp add: Rm_self_loops_def)
then have prod_in_Solve_lrec: "(A', w' @ [Nt A']) ∈ Solve_lrec A A' S"
using w_prop2 ‹w' ≠ []› unfolding Solve_lrec_defs by (auto)
have 1: "Solve_lrec A A' S ⊢ [Nt A'] ⇒(n) u' @ [Nt A']" using Suc.IH Suc ln_derive by auto
then have 2: "Solve_lrec A A' S ⊢ [Nt A'] ⇒(Suc n) u' @ w' @ [Nt A']"
using prod_in_Solve_lrec by (simp add: derive_prepend derive_singleton relpowp_Suc_I)
have "(A', w') ∈ Solve_lrec A A' S" using w_prop2 ‹w' ≠ []› ‹(A, w) ∈ S›
unfolding Solve_lrec_defs by (auto)
then have "Solve_lrec A A' S ⊢ [Nt A'] ⇒(Suc n) u' @ w'"
using 1 by (simp add: derive_prepend derive_singleton relpowp_Suc_I)
then show ?case using w_prop2 2 by simp
qed
text ‹A left derivation from ‹p› (‹hd p = Nt A›) to ‹q› (‹hd q ≠ Nt A›) can be split into
a left-recursive part, only using left-recursive productions ‹A → A # w›,
one left derivation step consuming Nt ‹A› using some rule ‹A → B # v› where ‹B ≠ Nt A›
and a left-derivation comprising the rest of the derivation.›
lemma lrec_decomp:
assumes "S = {x. (∃v. x = (A, v) ∧ x ∈ R)}" "Eps_free R"
shows "⟦ hd p = Nt A; hd q ≠ Nt A; R ⊢ p ⇒l(n) q ⟧
⟹ ∃u w m k. S ⊢ p ⇒l(m) Nt A # u ∧ S ⊢ Nt A # u ⇒l w ∧ hd w ≠ Nt A ∧
R ⊢ w ⇒l(k) q ∧ n = m + k + 1"
proof (induction n arbitrary: p)
case 0
then have pq_not_Nil: "p ≠ [] ∧ q ≠ []" using Eps_free_derives_Nil assms
by simp
have "p = q" using 0 by auto
then show ?case using pq_not_Nil 0 by auto
next
case (Suc n)
then have pq_not_Nil: "p ≠ [] ∧ q ≠ []"
using Eps_free_deriveln_Nil assms by fastforce
have ex_p': "∃p'. p = Nt A # p'" using pq_not_Nil Suc
by (metis hd_Cons_tl)
then obtain p' where P: "p = Nt A # p'" by blast
have "∄q'. q = Nt A # q'" using pq_not_Nil Suc
by fastforce
then have "∃w. (A,w) ∈ R ∧ R ⊢ w @ p' ⇒l(n) q" using Suc P by (auto simp add: deriveln_Nt_Cons)
then obtain w where w_prop: "(A,w) ∈ R ∧ R ⊢ w @ p' ⇒l(n) q" by blast
then have prod_in_S: "(A, w) ∈ S" using Suc assms by auto
show ?case
proof (cases "∃w'. w = Nt A # w'")
case True
then obtain w' where "w = Nt A # w'" by blast
then have "∃u w'' m k. S ⊢ w @ p' ⇒l(m) Nt A # u ∧ S ⊢ Nt A # u ⇒l w'' ∧
hd w'' ≠ Nt A ∧ R ⊢ w'' ⇒l(k) q ∧ n = m + k + 1"
using Suc.IH Suc.prems w_prop by auto
then obtain u w'' m k where propo: "S ⊢ w @ p' ⇒l(m) Nt A # u ∧ S ⊢ Nt A # u ⇒l w'' ∧
hd w'' ≠ Nt A ∧ R ⊢ w'' ⇒l(k) q ∧ n = m + k + 1"
by blast
then have "S ⊢ Nt A # p' ⇒l(Suc m) Nt A # u"
using prod_in_S P by (meson derivel_Nt_Cons relpowp_Suc_I2)
then have "S ⊢ p ⇒l(Suc m) Nt A # u ∧ S ⊢ Nt A # u ⇒l w'' ∧
hd w'' ≠ Nt A ∧ R ⊢ w'' ⇒l(k) q ∧ Suc n = Suc m + k + 1"
using P propo by auto
then show ?thesis by blast
next
case False
then have "w ≠ [] ∧ hd w ≠ Nt A" using Suc w_prop assms
by (metis Eps_free_Nil list.collapse)
then have "S ⊢ p ⇒l(0) Nt A # p' ∧ S ⊢ Nt A # p' ⇒l w @ p' ∧ hd (w @ p') ≠ Nt A ∧
R ⊢ w @ p' ⇒l(n) q ∧ Suc n = 0 + n + 1"
using P w_prop prod_in_S by (auto simp add: derivel_Nt_Cons)
then show ?thesis by blast
qed
qed
text ‹Every derivation resulting in a word has a derivation in ‹Solve_lrec B B' R›.›
lemma tm_derive_impl_Solve_lrec_derive:
assumes "Eps_free R" "B ≠ B'" "B' ∉ Nts R"
shows "⟦ p ≠ []; R ⊢ p ⇒(n) map Tm q⟧ ⟹ Solve_lrec B B' R ⊢ p ⇒* map Tm q"
proof (induction n arbitrary: p q rule: nat_less_induct)
case (1 n)
then show ?case
proof (cases "Solve_lrec B B' R = R - {(B, [Nt B])}")
case True
have 2: "Rm_self_loops R ⊆ R - {(B, [Nt B])}" by (auto simp add: Rm_self_loops_def)
have "Rm_self_loops R ⊢ p ⇒* map Tm q"
using "1.prems"(2)
by (auto simp: Rm_self_loops_def no_self_loops_derives relpowp_imp_rtranclp)
then show ?thesis
using 2 by (simp add: True derives_mono)
next
case Solve_lrec_not_R: False
then show ?thesis
proof (cases "Nts_syms p = {}")
case True
then obtain pt where "p = map Tm pt" using Nts_syms_empty_iff by blast
then have "map Tm q = p"
using deriven_from_TmsD "1.prems"(2) by blast
then show ?thesis by simp
next
case False
then have "∃C pt p2. p = map Tm pt @ Nt C # p2" using non_word_has_first_Nt[of p] by auto
then obtain C pt p2 where P: "p = map Tm pt @ Nt C # p2" by blast
then have "R ⊢ map Tm pt @ Nt C # p2 ⇒l(n) map Tm q"
using "1.prems" by (simp add: deriveln_iff_deriven)
then have "∃q2. map Tm q = map Tm pt @ q2 ∧ R ⊢ Nt C # p2 ⇒l(n) q2"
by (simp add: deriveln_map_Tm_append[of "n" R "pt" "Nt C # p2" "map Tm q"])
then obtain q2 where P1: "map Tm q = map Tm pt @ q2 ∧ R ⊢ Nt C # p2 ⇒l(n) q2" by blast
then have "n ≠ 0"
by (metis False P Nts_syms_map_Tm relpowp_0_E)
then have "∃m. n = Suc m"
by (meson old.nat.exhaust)
then obtain m where n_Suc: "n = Suc m" by blast
have "∃q2t. q2 = map Tm q2t"
by (metis P1 append_eq_map_conv)
then obtain q2t where q2_tms: "q2 = map Tm q2t" by blast
then show ?thesis
proof (cases "C = B")
case True
then have n_derive: "R ⊢ Nt B # p2 ⇒(n) q2" using P1
by (simp add: deriveln_imp_deriven)
have "∄v2. q2 = Nt B #v2 ∧ R ⊢ p2 ⇒(n) v2" using q2_tms by auto
then have "∃n1 n2 w v1 v2. n = Suc (n1 + n2) ∧ q2 = v1 @ v2 ∧
(B,w) ∈ R ∧ R ⊢ w ⇒(n1) v1 ∧ R ⊢ p2 ⇒(n2) v2" using n_derive deriven_Cons_decomp
by (smt (verit) sym.inject(1))
then obtain n1 n2 w v1 v2 where decomp: "n = Suc (n1 + n2) ∧ q2 = v1 @ v2 ∧
(B,w) ∈ R ∧ R ⊢ w ⇒(n1) v1 ∧ R ⊢ p2 ⇒(n2) v2" by blast
then have derive_from_singleton: "R ⊢ [Nt B] ⇒(Suc n1) v1"
using deriven_Suc_decomp_left by force
have "v1 ≠ []"
using assms(1) Eps_free_deriven_Nil derive_from_singleton by auto
then have "∃v1t. v1 = map Tm v1t"
using decomp append_eq_map_conv q2_tms by blast
then obtain v1t where v1_tms: "v1 = map Tm v1t" by blast
then have v1_hd: "hd v1 ≠ Nt B"
by (metis Nil_is_map_conv ‹v1 ≠ []› hd_map sym.distinct(1))
have deriveln_from_singleton: "R ⊢ [Nt B] ⇒l(Suc n1) v1" using v1_tms derive_from_singleton
by (simp add: deriveln_iff_deriven)
text ‹This is the interesting bit where we use other lemmas to prove that we can replace a
specific part of the derivation which is a left-recursion by a right-recursion in the
new productions.›
let ?S = "{x. (∃v. x = (B, v) ∧ x ∈ R)}"
have "∃u w m k. ?S ⊢ [Nt B] ⇒l(m) Nt B # u ∧ ?S ⊢ Nt B # u ⇒l w ∧
hd w ≠ Nt B ∧ R ⊢ w ⇒l(k) v1 ∧ Suc n1 = m + k + 1"
using deriveln_from_singleton v1_hd assms lrec_decomp[of ?S B R "[Nt B]" v1 "Suc n1"] by auto
then obtain u w2 m2 k where l_decomp: "?S ⊢ [Nt B] ⇒l(m2) Nt B # u ∧ ?S ⊢ Nt B # u ⇒l w2
∧ hd w2 ≠ Nt B ∧ R ⊢ w2 ⇒l(k) v1 ∧ Suc n1 = m2 + k + 1"
by blast
then have "∃w2'. (B,w2') ∈ ?S ∧ w2 = w2' @ u" by (simp add: derivel_Nt_Cons)
then obtain w2' where w2'_prod: "(B,w2') ∈ ?S ∧ w2 = w2' @ u" by blast
then have w2'_props: "w2' ≠ [] ∧ hd w2' ≠ Nt B"
by (metis (mono_tags, lifting) assms(1) Eps_free_Nil l_decomp
hd_append mem_Collect_eq)
have Solve_lrec_subset: "Solve_lrec B B' ?S ⊆ Solve_lrec B B' R"
unfolding Solve_lrec_defs by (auto)
have "Solve_lrec B B' ?S ⊢ [Nt B] ⇒* w2"
proof(cases "u = []")
case True
have "(B, w2') ∈ Solve_lrec B B' ?S"
using w2'_props w2'_prod unfolding Solve_lrec_defs by (auto)
then show ?thesis
by (simp add: True bu_prod derives_if_bu w2'_prod)
next
case False
have solved_prod: "(B, w2' @ [Nt B']) ∈ Solve_lrec B B' ?S"
using w2'_props w2'_prod Solve_lrec_not_R unfolding Solve_lrec_defs by (auto)
have "Rm_self_loops ?S ⊢ [Nt B] ⇒l* Nt B # u"
apply (unfold Rm_self_loops_def no_self_loops_derivels)
using l_decomp by (auto simp: relpowp_imp_rtranclp)
then have "∃ln. Rm_self_loops ?S ⊢ [Nt B] ⇒l(ln) Nt B # u"
by (simp add: rtranclp_power)
then obtain ln where "Rm_self_loops ?S ⊢ [Nt B] ⇒l(ln) Nt B # u" by blast
then have "(Solve_lrec B B' ?S) ⊢ [Nt B'] ⇒(ln) u"
using lrec_lemma3[of ?S B R ln u] assms False by auto
then have rrec_derive: "(Solve_lrec B B' ?S) ⊢ w2' @ [Nt B'] ⇒(ln) w2' @ u"
by (simp add: deriven_prepend)
have "(Solve_lrec B B' ?S) ⊢ [Nt B] ⇒ w2' @ [Nt B']"
using solved_prod by (simp add: derive_singleton)
then have "(Solve_lrec B B' ?S) ⊢ [Nt B] ⇒* w2' @ u"
using rrec_derive by (simp add: converse_rtranclp_into_rtranclp relpowp_imp_rtranclp)
then show ?thesis using w2'_prod by auto
qed
then have 2: "Solve_lrec B B' R ⊢ [Nt B] ⇒* w2"
using Solve_lrec_subset by (simp add: derives_mono)
text ‹From here on all the smaller derivations are concatenated after applying the IH.›
have fact2: "R ⊢ w2 ⇒l(k) v1 ∧ Suc n1 = m2 + k + 1" using l_decomp by auto
then have "k < n"
using decomp by linarith
then have 3: "Solve_lrec B B' R ⊢ w2 ⇒* v1" using "1.IH" v1_tms fact2
by (metis deriveln_iff_deriven derives_from_empty relpowp_imp_rtranclp)
have 4: "Solve_lrec B B' R ⊢ [Nt B] ⇒* v1" using 2 3
by auto
have "∃v2t. v2 = map Tm v2t" using decomp append_eq_map_conv q2_tms by blast
then obtain v2t where v2_tms: "v2 = map Tm v2t" by blast
have "n2 < n" using decomp by auto
then have 5: "Solve_lrec B B' R ⊢ p2 ⇒* v2" using "1.IH" decomp v2_tms
by (metis derives_from_empty relpowp_imp_rtranclp)
have "Solve_lrec B B' R ⊢ Nt B # p2 ⇒* q2" using 4 5 decomp
by (metis append_Cons append_Nil derives_append_decomp)
then show ?thesis
by (simp add: P P1 True derives_prepend)
next
case C_not_B: False
then have "∃w. (C, w) ∈ R ∧ R ⊢ w @ p2 ⇒l(m) q2"
by (metis P1 derivel_Nt_Cons relpowp_Suc_D2 n_Suc)
then obtain w where P2: "(C, w) ∈ R ∧ R ⊢ w @ p2 ⇒l(m) q2" by blast
then have rule_in_Solve_lrec: "(C, w) ∈ (Solve_lrec B B' R)"
using C_not_B by (auto simp add: Solve_lrec_def Rm_lrec_def)
have derivem: "R ⊢ w @ p2 ⇒(m) q2" using q2_tms P2 by (auto simp add: deriveln_iff_deriven)
have "w @ p2 ≠ []"
using assms(1) Eps_free_Nil P2 by fastforce
then have "(Solve_lrec B B' R) ⊢ w @ p2 ⇒* q2" using "1.IH" q2_tms n_Suc derivem
by auto
then have "(Solve_lrec B B' R) ⊢ Nt C # p2 ⇒* q2"
using rule_in_Solve_lrec by (auto simp add: derives_Cons_rule)
then show ?thesis
by (simp add: P P1 derives_prepend)
qed
qed
qed
qed
corollary Lang_incl_Lang_Solve_lrec:
"⟦ Eps_free R; B ≠ B'; B' ∉ Nts R⟧ ⟹ Lang R A ⊆ Lang (Solve_lrec B B' R) A"
by(auto simp: Lang_def intro: tm_derive_impl_Solve_lrec_derive dest: rtranclp_imp_relpowp)
subsubsection ‹\<^prop>‹Lang (Solve_lrec B B' R) A ⊆ Lang R A››
text ‹Restricted to right-recursive productions of one Nt (‹A' → w @ [Nt A']›)
if there is a right-derivation from ‹u› to ‹v @ [Nt A']› then u ends in Nt ‹A'›.›
lemma rrec_lemma1:
assumes "S = {x. ∃v. x = (A', v @ [Nt A']) ∧ x ∈ Solve_lrec A A' R}" "S ⊢ u ⇒r(n) v @ [Nt A']"
shows "∃u'. u = u' @ [Nt A']"
proof (rule ccontr)
assume neg: "∄u'. u = u' @ [Nt A']"
show "False"
proof (cases "u = []")
case True
then show ?thesis using assms derivern_imp_deriven by fastforce
next
case u_not_Nil: False
then show ?thesis
proof (cases "∃t. last u = Tm t")
case True
then show ?thesis using assms neg
by (metis (lifting) u_not_Nil append_butlast_last_id derivern_snoc_Tm last_snoc)
next
case False
then have "∃B u'. u = u' @ [Nt B] ∧ B ≠ A'" using assms neg u_not_Nil
by (metis append_butlast_last_id sym.exhaust)
then obtain B u' where B_not_A': "u = u' @ [Nt B] ∧ B ≠ A'" by blast
then have "∃w. (B, w) ∈ S" using assms neg
by (metis (lifting) derivers_snoc_Nt relpowp_imp_rtranclp)
then obtain w where elem: "(B, w) ∈ S" by blast
have "(B, w) ∉ S" using B_not_A' assms by auto
then show ?thesis using elem by simp
qed
qed
qed
text ‹‹Solve_lrec› does not add productions of the form ‹A' → Nt A'›.›
lemma Solve_lrec_no_self_loop: "Eps_free R ⟹ A' ∉ Nts R ⟹ (A', [Nt A']) ∉ Solve_lrec A A' R"
unfolding Solve_lrec_defs by (auto)
text ‹Restricted to right-recursive productions of one Nt (‹A' → w @ [Nt A']›) if there is a
right-derivation from ‹u› to ‹v @ [Nt A']› then u ends in Nt ‹A'› and there exists a suffix
of ‹v @ [Nt A']› s.t. there is a right-derivation from ‹[Nt A']› to that suffix.›
lemma rrec_lemma2:
assumes "S = {x. (∃v. x = (A', v @ [Nt A']) ∧ x ∈ Solve_lrec A A' R)}" "Eps_free R" "A' ∉ Nts R"
shows "S ⊢ u ⇒r(n) v @ [Nt A']
⟹ ∃u' v'. u = u' @ [Nt A'] ∧ v = u' @ v' ∧ S ⊢ [Nt A'] ⇒r(n) v' @ [Nt A']"
proof (induction n arbitrary: u)
case 0
then show ?case by simp
next
case (Suc n)
have "∃u'. u = u' @ [Nt A']" using rrec_lemma1[of S] Suc.prems assms by auto
then obtain u' where u'_prop: "u = u' @ [Nt A']" by blast
then have "∃w. (A',w) ∈ S ∧ S ⊢ u' @ w ⇒r(n) v @ [Nt A']"
using Suc by (auto simp add: derivern_snoc_Nt)
then obtain w where w_prop: "(A',w) ∈ S ∧ S ⊢ u' @ w ⇒r(n) v @ [Nt A']" by blast
then have "∃u'' v''. u' @ w = u'' @ [Nt A'] ∧ v = u'' @ v'' ∧ S ⊢ [Nt A'] ⇒r(n) v'' @ [Nt A']"
using Suc.IH Suc by auto
then obtain u'' v'' where u''_prop: "u' @ w = u'' @ [Nt A'] ∧ v = u'' @ v'' ∧
S ⊢ [Nt A'] ⇒r(n) v'' @ [Nt A']"
by blast
have "w ≠ [] ∧ w ≠ [Nt A']"
using Suc.IH assms w_prop Solve_lrec_no_self_loop by fastforce
then have "∃u1. u1 ≠ [] ∧ w = u1 @ [Nt A'] ∧ u'' = u' @ u1"
using u''_prop
by (metis (no_types, opaque_lifting) append.left_neutral append1_eq_conv
append_assoc rev_exhaust)
then obtain u1 where u1_prop: "u1 ≠ [] ∧ w = u1 @ [Nt A'] ∧ u'' = u' @ u1" by blast
then have 1: "u = u' @ [Nt A'] ∧ v = u' @ (u1 @ v'')" using u'_prop u''_prop by auto
have 2: "S ⊢ u1 @ [Nt A'] ⇒r(n) u1 @ v'' @ [Nt A']" using u''_prop derivern_prepend
by fastforce
have "S ⊢ [Nt A'] ⇒r u1 @ [Nt A']" using w_prop u''_prop u1_prop
by (simp add: deriver_singleton)
then have "S ⊢ [Nt A'] ⇒r(Suc n) u1 @ v'' @ [Nt A']" using u''_prop
by (meson 2 relpowp_Suc_I2)
then show ?case using 1
by auto
qed
text ‹Restricted to right-recursive productions of one Nt (‹A' → w @ [Nt A']›)
if there is a restricted right-derivation in ‹Solve_lrec› from ‹[Nt A']› to ‹u @ [Nt A']›
then there exists a derivation in ‹R› from ‹[Nt A]› to ‹A # u›.›
lemma rrec_lemma3:
assumes "S = {x. (∃v. x = (A', v @ [Nt A']) ∧ x ∈ Solve_lrec A A' R)}" "Eps_free R"
"A' ∉ Nts R" "A ≠ A'"
shows "S ⊢ [Nt A'] ⇒r(n) u @ [Nt A'] ⟹ R ⊢ [Nt A] ⇒(n) Nt A # u"
proof(induction n arbitrary: u)
case 0
then show ?case by (simp)
next
case (Suc n)
then have "∃w. (A',w) ∈ S ∧ S ⊢ w ⇒r(n) u @ [Nt A']"
by (auto simp add: derivern_singleton split: prod.splits)
then obtain w where w_prop1: "(A',w) ∈ S ∧ S ⊢ w ⇒r(n) u @ [Nt A']" by blast
then have "∃u' v'. w = u' @ [Nt A'] ∧ u = u' @ v' ∧ S ⊢ [Nt A'] ⇒r(n) v' @ [Nt A']"
using rrec_lemma2[of S] assms by auto
then obtain u' v' where u'v'_prop: "w = u' @ [Nt A'] ∧ u = u' @ v'
∧ S ⊢ [Nt A'] ⇒r(n) v' @ [Nt A']"
by blast
then have 1: "R ⊢ [Nt A] ⇒(n) Nt A # v'" using Suc.IH by auto
have "(A', u' @ [Nt A']) ∈ Solve_lrec A A' R ⟶ (A, Nt A # u') ∈ R"
using assms unfolding Solve_lrec_defs by (auto)
then have "(A, Nt A # u') ∈ R" using u'v'_prop assms(1) w_prop1 by auto
then have "R ⊢ [Nt A] ⇒ Nt A # u'"
by (simp add: derive_singleton)
then have "R ⊢ [Nt A] @ v' ⇒ Nt A # u' @ v'"
by (metis Cons_eq_appendI derive_append)
then have "R ⊢ [Nt A] ⇒(Suc n) Nt A # (u' @ v')" using 1
by (simp add: relpowp_Suc_I)
then show ?case using u'v'_prop by simp
qed
text ‹A right derivation from ‹p@[Nt A']› to ‹q› (‹last q ≠ Nt A'›) can be split into a
right-recursive part, only using right-recursive productions with Nt ‹A'›,
one right derivation step consuming Nt ‹A'› using some rule ‹A' → as@[Nt B]› where ‹Nt B ≠ Nt A'›
and a right-derivation comprising the rest of the derivation.›
lemma rrec_decomp:
assumes "S = {x. (∃v. x = (A', v @ [Nt A']) ∧ x ∈ Solve_lrec A A' R)}" "Eps_free R"
"A ≠ A'" "A' ∉ Nts R"
shows "⟦A' ∉ Nts_syms p; last q ≠ Nt A'; Solve_lrec A A' R ⊢ p @ [Nt A'] ⇒r(n) q⟧
⟹ ∃u w m k. S ⊢ p @ [Nt A'] ⇒r(m) u @ [Nt A']
∧ Solve_lrec A A' R ⊢ u @ [Nt A'] ⇒r w ∧ A' ∉ Nts_syms w
∧ Solve_lrec A A' R ⊢ w ⇒r(k) q ∧ n = m + k + 1"
proof (induction n arbitrary: p)
case 0
then have pq_not_Nil: "p @ [Nt A'] ≠ [] ∧ q ≠ []" using Eps_free_derives_Nil
by auto
have "p = q" using 0 by auto
then show ?case using pq_not_Nil 0 by auto
next
case (Suc n)
have pq_not_Nil: "p @ [Nt A'] ≠ [] ∧ q ≠ []"
using assms Suc.prems Eps_free_deriven_Nil Eps_free_Solve_lrec derivern_imp_deriven
by (metis (no_types, lifting) snoc_eq_iff_butlast)
have "∄q'. q = q' @ [Nt A']" using pq_not_Nil Suc.prems
by fastforce
then have "∃w. (A',w) ∈ (Solve_lrec A A' R) ∧ (Solve_lrec A A' R) ⊢ p @ w ⇒r(n) q"
using Suc.prems by (auto simp add: derivern_snoc_Nt)
then obtain w where w_prop: "(A',w) ∈ (Solve_lrec A A' R) ∧ Solve_lrec A A' R ⊢ p @ w ⇒r(n) q"
by blast
show ?case
proof (cases "(A', w) ∈ S")
case True
then have "∃w'. w = w' @ [Nt A']"
by (simp add: assms(1))
then obtain w' where w_decomp: "w = w' @ [Nt A']" by blast
then have "A' ∉ Nts_syms (p @ w')" using assms Suc.prems True
unfolding Solve_lrec_defs by (auto split: if_splits)
then have "∃u w'' m k. S ⊢ p @ w ⇒r(m) u @ [Nt A'] ∧ Solve_lrec A A' R ⊢ u @ [Nt A'] ⇒r w''
∧ A' ∉ Nts_syms w'' ∧ Solve_lrec A A' R ⊢ w'' ⇒r(k) q ∧ n = m + k + 1"
using Suc.IH Suc.prems w_prop w_decomp by (metis (lifting) append_assoc)
then obtain u w'' m k where propo:
"S ⊢ p @ w ⇒r(m) u @ [Nt A'] ∧ Solve_lrec A A' R ⊢ u @ [Nt A'] ⇒r w'' ∧ A' ∉ Nts_syms w''
∧ Solve_lrec A A' R ⊢ w'' ⇒r(k) q ∧ n = m + k + 1"
by blast
then have "S ⊢ p @ [Nt A'] ⇒r(Suc m) u @ [Nt A']" using True
by (meson deriver_snoc_Nt relpowp_Suc_I2)
then have "S ⊢ p @ [Nt A'] ⇒r(Suc m) u @ [Nt A'] ∧ Solve_lrec A A' R ⊢ u @ [Nt A'] ⇒r w''
∧ A' ∉ Nts_syms w'' ∧ Solve_lrec A A' R ⊢ w'' ⇒r(k) q ∧ Suc n = Suc m + k + 1"
using propo by auto
then show ?thesis by blast
next
case False
then have "last w ≠ Nt A'" using assms
by (metis (mono_tags, lifting) Eps_freeE_Cons Eps_free_Solve_lrec
append_butlast_last_id list.distinct(1) mem_Collect_eq w_prop)
then have "A' ∉ Nts_syms w" using assms w_prop
unfolding Solve_lrec_defs by (auto split: if_splits)
then have "w ≠ [] ∧ A' ∉ Nts_syms w" using assms w_prop False
by (metis (mono_tags, lifting) Eps_free_Nil Eps_free_Solve_lrec)
then have "S ⊢ p @ [Nt A'] ⇒r(0) p @ [Nt A'] ∧ Solve_lrec A A' R ⊢ p @ [Nt A'] ⇒r p @ w
∧ A' ∉ Nts_syms (p @ w) ∧ Solve_lrec A A' R ⊢ p @ w ⇒r(n) q ∧ Suc n = 0 + n + 1"
using w_prop Suc.prems by (auto simp add: deriver_snoc_Nt)
then show ?thesis by blast
qed
qed
text ‹Every word derived by ‹Solve_lrec B B' R› can be derived by ‹R›.›
lemma tm_Solve_lrec_derive_impl_derive:
assumes "Eps_free R" "B ≠ B'" "B' ∉ Nts R"
shows "⟦ p ≠ []; B' ∉ Nts_syms p; (Solve_lrec B B' R) ⊢ p ⇒(n) map Tm q⟧ ⟹ R ⊢ p ⇒* map Tm q"
proof (induction arbitrary: p q rule: nat_less_induct)
case (1 n)
let ?R' = "(Solve_lrec B B' R)"
show ?case
proof (cases "Nts_syms p = {}")
case True
then show ?thesis
using "1.prems"(3) deriven_from_TmsD derives_from_Tms_iff
by (metis Nts_syms_empty_iff)
next
case False
from non_word_has_last_Nt[OF this] have "∃C pt p2. p = p2 @ [Nt C] @ map Tm pt" by blast
then obtain C pt p2 where p_decomp: "p = p2 @ [Nt C] @ map Tm pt" by blast
then have "∃pt' At w k m. ?R' ⊢ p2 ⇒(k) map Tm pt' ∧ ?R' ⊢ w ⇒(m) map Tm At ∧ (C, w) ∈ ?R'
∧ q = pt' @ At @ pt ∧ n = Suc(k + m)"
using "1.prems" word_decomp1[of n ?R' p2 C pt q] by auto
then obtain pt' At w k m
where P: "?R' ⊢ p2 ⇒(k) map Tm pt' ∧ ?R' ⊢ w ⇒(m) map Tm At ∧ (C, w) ∈ ?R'
∧ q = pt' @ At @ pt ∧ n = Suc(k + m)"
by blast
then have pre1: "m < n" by auto
have "B' ∉ Nts_syms p2 ∧ k < n" using P "1.prems" p_decomp by auto
then have p2_not_Nil_derive: "p2 ≠ [] ⟶ R ⊢ p2 ⇒* map Tm pt'" using 1 P by blast
have "p2 = [] ⟶ map Tm pt' = []" using P
by auto
then have p2_derive: "R ⊢ p2 ⇒* map Tm pt'" using p2_not_Nil_derive by auto
have "R ⊢ [Nt C] ⇒* map Tm At"
proof(cases "C = B")
case C_is_B: True
then show ?thesis
proof (cases "last w = Nt B'")
case True
let ?S = "{x. (∃v. x = (B', v @ [Nt B']) ∧ x ∈ Solve_lrec B B' R)}"
have "∃w1. w = w1 @ [Nt B']" using True
by (metis assms(1) Eps_free_Nil Eps_free_Solve_lrec P append_butlast_last_id)
then obtain w1 where w_decomp: "w = w1 @ [Nt B']" by blast
then have "∃w1' b k1 m1. ?R' ⊢ w1 ⇒(k1) w1' ∧ ?R' ⊢ [Nt B'] ⇒(m1) b ∧ map Tm At = w1' @ b
∧ m = k1 + m1"
using P deriven_append_decomp by blast
then obtain w1' b k1 m1
where w_derive_decomp: "?R' ⊢ w1 ⇒(k1) w1' ∧ ?R' ⊢ [Nt B'] ⇒(m1) b
∧ map Tm At = w1' @ b ∧ m = k1 + m1"
by blast
then have "∃w1t bt. w1' = map Tm w1t ∧ b = map Tm bt"
by (meson map_eq_append_conv)
then obtain w1t bt where tms: "w1' = map Tm w1t ∧ b = map Tm bt" by blast
have pre1: "k1 < n ∧ m1 < n" using w_derive_decomp P by auto
have pre2: "w1 ≠ []" using w_decomp C_is_B P assms by (auto simp add: Solve_lrec_rule_simp3)
have Bw1_in_R: "(B, w1) ∈ R"
using w_decomp P C_is_B assms
unfolding Solve_lrec_defs by (auto split: if_splits)
then have pre3: "B' ∉ Nts_syms w1" using assms by (auto simp add: Nts_def)
have "R ⊢ w1 ⇒* map Tm w1t" using pre1 pre2 pre3 w_derive_decomp "1.IH" tms by blast
then have w1'_derive: "R ⊢ [Nt B] ⇒* w1'" using Bw1_in_R tms
by (simp add: derives_Cons_rule)
have "last [Nt B'] = Nt B' ∧ last (map Tm bt) ≠ Nt B'"
by (metis assms(1) Eps_free_deriven_Nil Eps_free_Solve_lrec last_ConsL last_map
list.map_disc_iff not_Cons_self2 sym.distinct(1) tms w_derive_decomp)
then have "∃u v m2 k2. ?S ⊢ [Nt B'] ⇒r(m2) u @ [Nt B'] ∧ ?R' ⊢ u @ [Nt B'] ⇒r v
∧ B' ∉ Nts_syms v ∧ ?R' ⊢ v ⇒r(k2) map Tm bt ∧ m1 = m2 + k2 + 1"
using rrec_decomp[of ?S B' B R "[]" "map Tm bt" m1] w_derive_decomp assms "1.prems" tms
by (simp add: derivern_iff_deriven)
then obtain u v m2 k2
where rec_decomp: "?S ⊢ [Nt B'] ⇒r(m2) u @ [Nt B'] ∧ ?R' ⊢ u @ [Nt B'] ⇒r v
∧ B' ∉ Nts_syms v ∧ ?R' ⊢ v ⇒r(k2) map Tm bt ∧ m1 = m2 + k2 + 1"
by blast
then have Bu_derive: "R ⊢ [Nt B] ⇒(m2) Nt B # u"
using assms rrec_lemma3 by fastforce
have "∃v'. (B', v') ∈ ?R' ∧ v = u @ v'" using rec_decomp
by (simp add: deriver_snoc_Nt)
then obtain v' where v_decomp: "(B', v') ∈ ?R' ∧ v = u @ v'" by blast
then have "(B, Nt B # v') ∈ R"
using assms rec_decomp unfolding Solve_lrec_defs by (auto split: if_splits)
then have "R ⊢ [Nt B] ⇒ Nt B # v'"
by (simp add: derive_singleton)
then have "R ⊢ [Nt B] @ v' ⇒* Nt B # u @ v'"
by (metis Bu_derive append_Cons derives_append rtranclp_power)
then have Buv'_derive: "R ⊢ [Nt B] ⇒* Nt B # u @ v'"
using ‹R ⊢ [Nt B] ⇒ Nt B # v'› by force
have pre2: "k2 < n" using rec_decomp pre1 by auto
have "v ≠ []" using rec_decomp
by (metis (lifting) assms(1) Eps_free_deriven_Nil Eps_free_Solve_lrec tms
deriven_from_TmsD derivern_imp_deriven list.simps(8) not_Cons_self2 w_derive_decomp)
then have "R ⊢ v ⇒* map Tm bt"
using "1.IH" 1 pre2 rec_decomp
by (auto simp add: derivern_iff_deriven)
then have "R ⊢ [Nt B] ⇒* Nt B # map Tm bt" using Buv'_derive v_decomp
by (meson derives_Cons rtranclp_trans)
then have "R ⊢ [Nt B] ⇒* [Nt B] @ map Tm bt" by auto
then have "R ⊢ [Nt B] ⇒* w1' @ map Tm bt" using w1'_derive derives_append
by (metis rtranclp_trans)
then show ?thesis using tms w_derive_decomp C_is_B by auto
next
case False
have pre2: "w ≠ []" using P assms(1)
by (meson Eps_free_Nil Eps_free_Solve_lrec)
then have 2: "(C, w) ∈ R"
using P False "1.prems" p_decomp C_is_B
unfolding Solve_lrec_defs by (auto split: if_splits)
then have pre3: "B' ∉ Nts_syms w" using P assms(3) by (auto simp add: Nts_def)
have "R ⊢ w ⇒* map Tm At" using "1.IH" assms pre1 pre2 pre3 P by blast
then show ?thesis using 2
by (meson bu_prod derives_bu_iff rtranclp_trans)
qed
next
case False
then have 2: "(C, w) ∈ R"
using P "1.prems"(2) p_decomp
by (auto simp add: Solve_lrec_rule_simp1)
then have pre2: "B' ∉ Nts_syms w" using P assms(3) by (auto simp add: Nts_def)
have pre3: "w ≠ []" using assms(1) 2 by (auto simp add: Eps_free_def)
have "R ⊢ w ⇒* map Tm At" using "1.IH" pre1 pre2 pre3 P by blast
then show ?thesis using 2
by (meson bu_prod derives_bu_iff rtranclp_trans)
qed
then show ?thesis using p2_derive
by (metis P derives_append derives_append_decomp map_append p_decomp)
qed
qed
corollary Lang_Solve_lrec_incl_Lang:
assumes "Eps_free R" "B ≠ B'" "B' ∉ Nts R" "A ≠ B'"
shows "Lang (Solve_lrec B B' R) A ⊆ Lang R A"
proof
fix w
assume "w ∈ Lang (Solve_lrec B B' R) A"
then have "Solve_lrec B B' R ⊢ [Nt A] ⇒* map Tm w" by (simp add: Lang_def)
then have "∃n. Solve_lrec B B' R ⊢ [Nt A] ⇒(n) map Tm w"
by (simp add: rtranclp_power)
then obtain n where "(Solve_lrec B B' R) ⊢ [Nt A] ⇒(n) map Tm w" by blast
then have "R ⊢ [Nt A] ⇒* map Tm w" using tm_Solve_lrec_derive_impl_derive[of R] assms by auto
then show "w ∈ Lang R A" by (simp add: Lang_def)
qed
corollary Solve_lrec_Lang:
"⟦ Eps_free R; B ≠ B'; B' ∉ Nts R; A ≠ B'⟧ ⟹ Lang (Solve_lrec B B' R) A = Lang R A"
using Lang_Solve_lrec_incl_Lang Lang_incl_Lang_Solve_lrec by fastforce
subsection ‹‹Expand_hd_rec› Preserves Language›
text ‹Every rhs of an ‹Expand_hd_rec P› production is derivable by ‹P›.›
lemma Expand_hd_rec_is_deriveable: "(A, w) ∈ Expand_hd_rec B As P ⟹ P ⊢ [Nt A] ⇒* w"
proof (induction B As P arbitrary: A w rule: Expand_hd_rec.induct)
case (1 B R)
then show ?case
by (simp add: bu_prod derives_if_bu)
next
case (2 B S Ss R)
then show ?case
proof (cases "B = A")
case True
then have Aw_or_ACv: "(A, w) ∈ Expand_hd_rec A Ss R ∨ (∃C v. (A, Nt C # v) ∈ Expand_hd_rec A Ss R)"
using 2 by (auto simp add: Let_def Subst_hd_def)
then show ?thesis
proof (cases "(A, w) ∈ Expand_hd_rec A Ss R")
case True
then show ?thesis using 2 True by (auto simp add: Let_def Subst_hd_def)
next
case False
then have "∃ v wv. w = v @ wv ∧ (A, Nt S#wv) ∈ Expand_hd_rec A Ss R ∧ (S, v) ∈ Expand_hd_rec A Ss R"
using 2 True by (auto simp add: Let_def Subst_hd_def)
then obtain v wv
where P: "w = v @ wv ∧ (A, Nt S # wv) ∈ Expand_hd_rec A Ss R ∧ (S, v) ∈ Expand_hd_rec A Ss R"
by blast
then have tr: "R ⊢ [Nt A] ⇒* [Nt S] @ wv" using 2 True by simp
have "R ⊢ [Nt S] ⇒* v" using 2 True P by simp
then show ?thesis using P tr derives_append
by (metis rtranclp_trans)
qed
next
case False
then show ?thesis using 2 by (auto simp add: Let_def Subst_hd_def)
qed
qed
lemma Expand_hd_rec_incl1: "Lang (Expand_hd_rec B As P) A ⊆ Lang P A"
by (meson DersD DersI Lang_subset_if_Ders_subset derives_simul_rules Expand_hd_rec_is_deriveable subsetI)
text ‹This lemma expects a set of quadruples ‹(A, a1, B, a2)›. Each quadruple encodes a specific Nt
in a specific rule ‹A → a1 @ Nt B # a2› (this encodes Nt ‹B›) which should be expanded,
by replacing the Nt with every rule for that Nt and then removing the original rule.
This expansion contains the original productions Language.›
lemma exp_includes_Lang:
assumes S_props: "∀x ∈ S. ∃A a1 B a2. x = (A, a1, B, a2) ∧ (A, a1 @ Nt B # a2) ∈ R"
shows "Lang R A
⊆ Lang (R - {x. ∃A a1 B a2. x = (A, a1 @ Nt B # a2) ∧ (A, a1, B, a2) ∈ S }
∪ {x. ∃A v a1 a2 B. x = (A,a1@v@a2) ∧ (A, a1, B, a2) ∈ S ∧ (B,v) ∈ R}) A"
proof
fix x
assume x_Lang: "x ∈ Lang R A"
let ?S' = "{x. ∃A a1 B a2. x = (A, a1 @ Nt B # a2) ∧ (A, a1, B, a2) ∈ S }"
let ?E = "{x. ∃A v a1 a2 B. x = (A,a1@v@a2) ∧ (A, a1, B, a2) ∈ S ∧ (B,v) ∈ R}"
let ?subst = "R - ?S' ∪ ?E"
have S'_sub: "?S' ⊆ R" using S_props by auto
have "(N, ts) ∈ ?S' ⟹ ∃B. B ∈ Nts_syms ts" for N ts by fastforce
then have terminal_prods_stay: "(N, ts) ∈ R ⟹ Nts_syms ts = {} ⟹ (N, ts) ∈ ?subst" for N ts
by auto
have "R ⊢ p ⇒(n) map Tm x ⟹ ?subst ⊢ p ⇒* map Tm x" for p n
proof (induction n arbitrary: p x rule: nat_less_induct)
case (1 n)
then show ?case
proof (cases "∃pt. p = map Tm pt")
case True
then obtain pt where "p = map Tm pt" by blast
then show ?thesis using "1.prems" deriven_from_TmsD derives_from_Tms_iff by blast
next
case False
then have "∃uu V ww. p = uu @ Nt V # ww"
by (smt (verit, best) "1.prems" deriven_Suc_decomp_left relpowp_E)
then obtain uu V ww where p_eq: "p = uu @ Nt V # ww" by blast
then have "¬ R ⊢ p ⇒(0) map Tm x"
using False by auto
then have "∃m. n = Suc m"
using "1.prems" old.nat.exhaust by blast
then obtain m where n_Suc: "n = Suc m" by blast
then have "∃v. (V, v) ∈ R ∧ R ⊢ uu @ v @ ww ⇒(m) map Tm x"
using 1 p_eq by (auto simp add: deriven_start_sent)
then obtain v where start_deriven: "(V, v) ∈ R ∧ R ⊢ uu @ v @ ww ⇒(m) map Tm x" by blast
then show ?thesis
proof (cases "(V, v) ∈ ?S'")
case True
then have "∃a1 B a2. v = a1 @ Nt B # a2 ∧ (V, a1, B, a2) ∈ S" by blast
then obtain a1 B a2 where v_eq: "v = a1 @ Nt B # a2 ∧ (V, a1, B, a2) ∈ S" by blast
then have m_deriven: "R ⊢ (uu @ a1) @ Nt B # (a2 @ ww) ⇒(m) map Tm x"
using start_deriven by auto
then have "¬ R ⊢ (uu @ a1) @ Nt B # (a2 @ ww) ⇒(0) map Tm x"
by (metis (mono_tags, lifting) append.left_neutral append_Cons derive.intros insertI1
not_derive_from_Tms relpowp.simps(1))
then have "∃k. m = Suc k"
using m_deriven "1.prems" old.nat.exhaust by blast
then obtain k where m_Suc: "m = Suc k" by blast
then have "∃b. (B, b) ∈ R ∧ R ⊢ (uu @ a1) @ b @ (a2 @ ww) ⇒(k) map Tm x"
using m_deriven deriven_start_sent[where ?u = "uu@a1" and ?w = "a2 @ ww"]
by (auto simp add: m_Suc)
then obtain b
where second_deriven: "(B, b) ∈ R ∧ R ⊢ (uu @ a1) @ b @ (a2 @ ww) ⇒(k) map Tm x"
by blast
then have expd_rule_subst: "(V, a1 @ b @ a2) ∈ ?subst" using v_eq by auto
have "k < n" using n_Suc m_Suc by auto
then have subst_derives: "?subst ⊢ uu @ a1 @ b @ a2 @ ww ⇒* map Tm x"
using 1 second_deriven by (auto)
have "?subst ⊢ [Nt V] ⇒* a1 @ b @ a2" using expd_rule_subst
by (meson derive_singleton r_into_rtranclp)
then have "?subst ⊢ [Nt V] @ ww ⇒* a1 @ b @ a2 @ ww"
using derives_append[of ?subst "[Nt V]" "a1 @ b @ a2"]
by simp
then have "?subst ⊢ Nt V # ww ⇒* a1 @ b @ a2 @ ww"
by simp
then have "?subst ⊢ uu @ Nt V # ww ⇒* uu @ a1 @ b @ a2 @ ww"
using derives_prepend[of ?subst "[Nt V] @ ww"]
by simp
then show ?thesis using subst_derives by (auto simp add: p_eq v_eq)
next
case False
then have Vv_subst: "(V,v) ∈ ?subst" using S_props start_deriven by auto
then have "?subst ⊢ uu @ v @ ww ⇒* map Tm x" using 1 start_deriven n_Suc by auto
then show ?thesis using Vv_subst derives_append_decomp
by (metis (no_types, lifting) derives_Cons_rule p_eq)
qed
qed
qed
then have "R ⊢ p ⇒* map Tm x ⟹ ?subst ⊢ p ⇒* map Tm x" for p
by (meson rtranclp_power)
then show "x ∈ Lang ?subst A" using x_Lang by (auto simp add: Lang_def)
qed
lemma Expand_hd_rec_incl2: "Lang (Expand_hd_rec B As P) A ⊇ Lang P A"
proof (induction B As P rule: Expand_hd_rec.induct)
case (1 A R)
then show ?case by simp
next
case (2 C H Ss R)
let ?R' = "Expand_hd_rec C Ss R"
let ?X = "{r ∈ ?R'. ∃w. r = (C, Nt H # w)}"
have "Expand_hd_rec C (H # Ss) R = Subst_hd ?R' ?X" by (auto simp: Let_def)
let ?S = "{x. ∃A w. x = (A, [], H, w) ∧ (A, Nt H # w) ∈ ?X}"
let ?S' = "{x. ∃A a1 B a2. x = (A, a1 @ Nt B # a2) ∧ (A, a1, B, a2) ∈ ?S}"
let ?E = "{x. ∃A v a1 a2 B. x = (A,a1@v@a2) ∧ (A, a1, B, a2) ∈ ?S ∧ (B,v) ∈ ?R'}"
have S'_eq_X: "?S' = ?X" by fastforce
have E_eq_Y: "?E = {(A,v@w) | A v w. ∃B. (B,v) ∈ ?R' ∧ (A, Nt B # w) ∈ ?X}" by fastforce
have "∀x ∈ ?S. ∃A a1 B a2. x = (A, a1, B, a2) ∧ (A, a1 @ Nt B # a2) ∈ ?R'" by fastforce
then have Lang_sub: "Lang ?R' A ⊆ Lang (?R' - ?S' ∪ ?E) A"
using exp_includes_Lang[of ?S] by auto
have "Lang R A ⊆ Lang ?R' A" using 2 by simp
also have "... ⊆ Lang (?R' - ?S' ∪ ?E) A" using Lang_sub by simp
also have "... ⊆ Lang (Subst_hd ?R' ?X) A" using S'_eq_X E_eq_Y by (simp add: Subst_hd_def)
finally show ?case by (simp add: Let_def)
qed
theorem Expand_hd_rec_Lang: "Lang (Expand_hd_rec B As P) A = Lang P A"
using Expand_hd_rec_incl1[of B As P A] Expand_hd_rec_incl2[of P A B As] by auto
subsection ‹‹Solve_tri› Preserves Language›
lemma Lang_Solve_tri:
"⟦ Eps_free P; length As ≤ length As'; distinct(As @ As'); Nts P ∩ set As' = {}; A ∉ set As'⟧
⟹ Lang (Solve_tri As As' P) A = Lang P A"
proof (induction As As' P rule: Solve_tri.induct)
case *: (1 Aa As A' As' R)
then have e_free1: "Eps_free (Expand_hd_rec Aa As (Solve_tri As As' R))"
by (simp add: Eps_free_Expand_hd_rec Eps_free_Solve_tri)
have "length As ≤ length As'" using * by simp
then have "Nts (Expand_hd_rec Aa As (Solve_tri As As' R)) ⊆ Nts R ∪ set As'"
using * Nts_Expand_hd_rec Nts_Solve_tri
by (metis subset_trans)
then have nts1: " A' ∉ Nts (Expand_hd_rec Aa As (Solve_tri As As' R))"
using * Nts_Expand_hd_rec Nts_Solve_tri by auto
have "Lang (Solve_tri (Aa # As) (A' # As') R) A
= Lang (Solve_lrec Aa A' (Expand_hd_rec Aa As (Solve_tri As As' R))) A"
by simp
also have "... = Lang (Expand_hd_rec Aa As (Solve_tri As As' R)) A"
using nts1 e_free1 * Solve_lrec_Lang[of "Expand_hd_rec Aa As (Solve_tri As As' R)" Aa A' A]
by (simp)
also have "... = Lang (Solve_tri As As' R) A" by (simp add: Expand_hd_rec_Lang)
finally show ?case using * by (auto)
qed auto
section ‹Function ‹Expand_hd_rec›: Convert Triangular Form into GNF›
subsection ‹‹Expand_hd_rec›: Result is in ‹GNF_hd››
lemma dep_on_helper: "dep_on R A = {} ⟹ (A, w) ∈ R ⟹ w = [] ∨ (∃T wt. w = Tm T # wt)"
using neq_Nil_conv[of w] by (simp add: dep_on_def) (metis sym.exhaust)
lemma GNF_hd_iff_dep_on:
assumes "Eps_free P"
shows "GNF_hd P ⟷ (∀A ∈ Nts P. dep_on P A = {})" (is "?L=?R")
proof
assume ?L
then show ?R by (auto simp add: GNF_hd_def dep_on_def)
next
assume assm: ?R
have 1: "∀(B, w) ∈ P. ∃T wt. w = Tm T # wt ∨ w = []"
proof
fix x
assume "x ∈ P"
then have "case x of (B, w) ⇒ dep_on P B = {}" using assm by (auto simp add: Nts_def)
then show "case x of (B, w) ⇒ ∃T wt. w = Tm T # wt ∨ w = []"
using ‹x ∈ P› dep_on_helper by fastforce
qed
have 2: "∀(B, w) ∈ P. w ≠ []" using assms assm by (auto simp add: Eps_free_def)
have "∀(B, w) ∈ P. ∃T wt. w = Tm T # wt" using 1 2 by auto
then show "GNF_hd P" by (auto simp add: GNF_hd_def)
qed
lemma Expand_tri_simp1: "A ∉ set As ⟹ (A,w) ∈ Expand_tri As P ⟷ (A,w) ∈ P"
by (induction As P rule: Expand_tri.induct) (auto simp add: Let_def Subst_hd_def)
text ‹If none of the expanded Nts depend on ‹A› then any rule depending on ‹A› in ‹Expand_tri As R›
must already have been in ‹R›.›
lemma helper_Expand_tri2:
"⟦Eps_free R; A ∉ set As; ∀C ∈ set As. A ∉ (dep_on R C); B ≠ A; (B, Nt A # w) ∈ Expand_tri As R⟧
⟹ (B, Nt A # w) ∈ R"
proof (induction As R arbitrary: B w rule: Expand_tri.induct)
case (1 R)
then show ?case by simp
next
case (2 S Ss R)
have "(B, Nt A # w) ∈ Expand_tri Ss R"
proof (cases "B = S")
case B_is_S: True
let ?R' = "Expand_tri Ss R"
let ?X = "{(Al,Bw) ∈ ?R'. Al=S ∧ (∃w B. Bw = Nt B # w ∧ B ∈ set (Ss))}"
let ?Y = "{(S,v@w) |v w. ∃B. (S, Nt B # w) ∈ ?X ∧ (B,v) ∈ ?R'}"
have "(B, Nt A # w) ∉ ?X" using 2 by auto
then have 3: "(B, Nt A # w) ∈ ?R' ∨ (B, Nt A # w) ∈ ?Y" using 2
by (auto simp add: Let_def Subst_hd_def)
then show ?thesis
proof (cases "(B, Nt A # w) ∈ ?R'")
case True
then show ?thesis by simp
next
case False
then have "(B, Nt A # w) ∈ ?Y" using 3 by simp
then have "∃v wa Ba. Nt A # w = v @ wa ∧ (S, Nt Ba # wa) ∈ Expand_tri Ss R ∧ Ba ∈ set Ss
∧ (Ba, v) ∈ Expand_tri Ss R"
by (auto simp add: Let_def)
then obtain v wa Ba
where P: "Nt A # w = v @ wa ∧ (S, Nt Ba # wa) ∈ Expand_tri Ss R ∧ Ba ∈ set Ss
∧ (Ba, v) ∈ Expand_tri Ss R"
by blast
have "Eps_free (Expand_tri Ss R)" using 2 by (auto simp add: Eps_free_Expand_tri)
then have "v ≠ []" using P by (auto simp add: Eps_free_def)
then have v_hd: "hd v = Nt A" using P by (metis hd_append list.sel(1))
then have "∃va. v = Nt A # va"
by (metis ‹v ≠ []› list.collapse)
then obtain va where P2: "v = Nt A # va" by blast
then have "(Ba, v) ∈ R" using 2 P
by (metis list.set_intros(2))
then have "A ∈ dep_on R Ba" using v_hd P2 by (auto simp add: dep_on_def)
then show ?thesis using 2 P by auto
qed
next
case False
then show ?thesis using 2 by (auto simp add: Let_def Subst_hd_def)
qed
then show ?case using 2 by auto
qed
text ‹In a Triangular form no Nts depend on the last Nt in the list.›
lemma Triangular_snoc_dep_on: "Triangular (As@[A]) R ⟹ ∀C ∈ set As. A ∉ (dep_on R C)"
by (induction As) auto
lemma Triangular_helper1: "Triangular As R ⟹ A ∈ set As ⟹ A ∉ dep_on R A"
by (induction As) auto
lemma dep_on_Expand_tri:
"⟦Eps_free R; Triangular (rev As) R; distinct As; A ∈ set As⟧
⟹ dep_on (Expand_tri As R) A ∩ set As = {}"
proof(induction As R arbitrary: A rule: Expand_tri.induct)
case (1 R)
then show ?case by simp
next
case (2 S Ss R)
then have Eps_free_exp_Ss: "Eps_free (Expand_tri Ss R)"
by (simp add: Eps_free_Expand_tri)
have dep_on_fact: "∀C ∈ set Ss. S ∉ (dep_on R C)"
using 2 by (auto simp add: Triangular_snoc_dep_on)
then show ?case
proof (cases "A = S")
case True
have F1: "(S, Nt S # w) ∉ Expand_tri Ss R" for w
proof(rule ccontr)
assume "¬((S, Nt S # w) ∉ Expand_tri Ss R)"
then have "(S, Nt S # w) ∈ R" using 2 by (auto simp add: Expand_tri_simp1)
then have N: "S ∈ dep_on R A" using True by (auto simp add: dep_on_def)
have "S ∉ dep_on R A" using 2 True by (auto simp add: Triangular_helper1)
then show "False" using N by simp
qed
have F2: "(S, Nt S # w) ∉ Expand_tri (S#Ss) R" for w
proof
assume "(S, Nt S # w) ∈ Expand_tri (S#Ss) R"
then have "∃v wa B. Nt S # w = v @ wa ∧ B ∈ set Ss ∧ (S, Nt B # wa) ∈ Expand_tri Ss R
∧ (B, v) ∈ Expand_tri Ss R"
using 2 F1 by (auto simp add: Let_def Subst_hd_def)
then obtain v wa B
where v_wa_B_P: "Nt S # w = v @ wa ∧ B ∈ set Ss ∧ (S, Nt B # wa) ∈ Expand_tri Ss R
∧ (B, v) ∈ Expand_tri Ss R"
by blast
then have "v ≠ [] ∧ (∃va. v = Nt S # va)" using Eps_free_exp_Ss
by (metis Eps_free_Nil append_eq_Cons_conv)
then obtain va where vP: "v ≠ [] ∧ v = Nt S # va" by blast
then have "(B, v) ∈ R"
using v_wa_B_P 2 dep_on_fact helper_Expand_tri2[of R S Ss B] True by auto
then have "S ∈ dep_on R B" using vP by (auto simp add: dep_on_def)
then show "False" using dep_on_fact v_wa_B_P by auto
qed
have "(S, Nt x # w) ∉ Expand_tri (S#Ss) R" if asm: "x ∈ set Ss" for x w
proof
assume assm: "(S, Nt x # w) ∈ Expand_tri (S # Ss) R"
then have "∃v wa B. Nt x # w = v @ wa ∧ (S, Nt B # wa) ∈ Expand_tri Ss R ∧ B ∈ set Ss
∧ (B, v) ∈ Expand_tri Ss R"
using 2 asm by (auto simp add: Let_def Subst_hd_def)
then obtain v wa B
where v_wa_B_P:"Nt x # w = v @ wa ∧ (S, Nt B # wa) ∈ Expand_tri Ss R ∧ B ∈ set Ss
∧ (B, v) ∈ Expand_tri Ss R"
by blast
then have dep_on_IH: "dep_on (Expand_tri Ss R) B ∩ set Ss = {}"
using 2 by (auto simp add: tri_Snoc_impl_tri)
have "v ≠ [] ∧ (∃va. v = Nt x # va)" using Eps_free_exp_Ss v_wa_B_P
by (metis Eps_free_Nil append_eq_Cons_conv)
then obtain va where vP: "v ≠ [] ∧ v = Nt x # va" by blast
then have "x ∈ dep_on (Expand_tri Ss R) B" using v_wa_B_P by (auto simp add: dep_on_def)
then show "False" using dep_on_IH v_wa_B_P asm assm by auto
qed
then show ?thesis using 2 True F2 by (auto simp add: Let_def dep_on_def)
next
case False
have "(A, Nt S # w) ∉ Expand_tri Ss R" for w
proof
assume "(A, Nt S # w) ∈ Expand_tri Ss R"
then have "(A, Nt S # w) ∈ R" using 2 helper_Expand_tri2 dep_on_fact
by (metis False distinct.simps(2))
then have F: "S ∈ dep_on R A" by (auto simp add: dep_on_def)
have "S ∉ dep_on R A" using dep_on_fact False 2 by auto
then show "False" using F by simp
qed
then show ?thesis using 2 False by (auto simp add: tri_Snoc_impl_tri Let_def dep_on_def Subst_hd_def)
qed
qed
text ‹If the entire ‹Triangular› form is expanded, the result is in GNF:›
theorem GNF_hd_Expand_tri:
assumes "Eps_free R" "Triangular (rev As) R" "distinct As" "Nts R ⊆ set As"
shows "GNF_hd (Expand_tri As R)"
by (metis Eps_free_Expand_tri GNF_hd_iff_dep_on Int_absorb2 Nts_Expand_tri assms dep_on_Expand_tri
dep_on_subs_Nts subset_trans subsetD)
text ‹Any set of productions can be transformed into GNF via ‹Expand_tri (Solve_tri)›.›
theorem GNF_hd_Expand_Solve_tri:
assumes assms: "Eps_free R" "distinct (As @ As')" "Nts R ⊆ set As" "length As ≤ length As'"
shows "GNF_hd (Expand_tri (As' @ rev As) (Solve_tri As As' R))"
proof -
from assms have tri: "Triangular (As @ rev As') (Solve_tri As As' R)"
by (simp add: Int_commute Triangular_Solve_tri)
have "Nts (Solve_tri As As' R) ⊆ set As ∪ set As'" using assms Nts_Solve_tri by fastforce
then show ?thesis
using GNF_hd_Expand_tri[of "(Solve_tri As As' R)" "(As' @ rev As)"] assms tri
by (auto simp add: Eps_free_Solve_tri)
qed
subsection ‹‹Expand_tri› Preserves Language›
text ‹Similar to the proof of Language equivalence of ‹Expand_hd_rec›.›
text ‹All productions in ‹Expand_tri As P› are derivable by ‹P›.›
lemma Expand_tri_prods_deirvable: "(B, bs) ∈ Expand_tri As P ⟹ P ⊢ [Nt B] ⇒* bs"
proof (induction As P arbitrary: B bs rule: Expand_tri.induct)
case (1 R)
then show ?case
by (simp add: bu_prod derives_if_bu)
next
case (2 A As R)
then show ?case
proof (cases "B ∈ set (A#As)")
case True
then show ?thesis
proof (cases "B = A")
case True
then have "∃C cw v.(bs = cw@v ∧ (B, Nt C#v) ∈ (Expand_tri As R) ∧ (C,cw) ∈ (Expand_tri As R))
∨ (B, bs) ∈ (Expand_tri As R)"
using 2 by (auto simp add: Let_def Subst_hd_def)
then obtain C cw v
where "(bs = cw @ v ∧ (B, Nt C # v) ∈ (Expand_tri As R) ∧ (C, cw) ∈ (Expand_tri As R))
∨ (B, bs) ∈ (Expand_tri As R)"
by blast
then have "(bs = cw @ v ∧ R ⊢ [Nt B] ⇒* [Nt C] @ v ∧ R ⊢ [Nt C] ⇒* cw) ∨ R ⊢ [Nt B] ⇒* bs"
using "2.IH" by auto
then show ?thesis by (meson derives_append rtranclp_trans)
next
case False
then have "(B, bs) ∈ (Expand_tri As R)" using 2 by (auto simp add: Let_def Subst_hd_def)
then show ?thesis using "2.IH" by (simp add: bu_prod derives_if_bu)
qed
next
case False
then have "(B, bs) ∈ R" using 2 by (auto simp: Expand_tri_simp1 simp del: Expand_tri.simps)
then show ?thesis by (simp add: bu_prod derives_if_bu)
qed
qed
text ‹Language Preservation:›
lemma Expand_tri_Lang: "Lang (Expand_tri As P) A = Lang P A"
proof
have "(B, bs) ∈ (Expand_tri As P) ⟹ P ⊢ [Nt B] ⇒* bs" for B bs
by (simp add: Expand_tri_prods_deirvable)
then have "Expand_tri As P ⊢ [Nt A] ⇒* map Tm x ⟹ P ⊢ [Nt A] ⇒* map Tm x" for x
using derives_simul_rules by blast
then show "Lang (Expand_tri As P) A ⊆ Lang P A" by(auto simp add: Lang_def)
next
show "Lang P A ⊆ Lang (Expand_tri As P) A"
proof (induction As P rule: Expand_tri.induct)
case (1 R)
then show ?case by simp
next
case (2 D Ds R)
let ?R' = "Expand_tri Ds R"
let ?X = "{r ∈ ?R'. (∃w B. r = (D, Nt B # w) ∧ B ∈ set (Ds))}"
let ?Y = "{(D,v@w) | v w. ∃B. (B,v) ∈ ?R' ∧ (D, Nt B # w) ∈ ?X}"
have F1: "Expand_tri (D#Ds) R = ?R' - ?X ∪ ?Y" by (auto simp: Let_def Subst_hd_def)
let ?S = "{x. ∃A w H. x = (A, [], H, w) ∧ (A, Nt H # w) ∈ ?X}"
let ?S' = "{x. ∃A a1 B a2. x = (A, a1 @ Nt B # a2) ∧ (A, a1, B, a2) ∈ ?S}"
let ?E = "{x. ∃A v a1 a2 B. x = (A,a1@v@a2) ∧ (A, a1, B, a2) ∈ ?S ∧ (B,v) ∈ ?R'}"
have S'_eq_X: "?S' = ?X" by fastforce
have E_eq_Y: "?E = ?Y" by fastforce
have "∀x ∈ ?S. ∃A a1 B a2. x = (A, a1, B, a2) ∧ (A, a1 @ Nt B # a2) ∈ ?R'" by fastforce
have "Lang R A ⊆ Lang (Expand_tri Ds R) A" using 2 by simp
also have "... ⊆ Lang (?R' - ?S' ∪ ?E) A"
using exp_includes_Lang[of ?S] by auto
also have "... = Lang (Expand_tri (D#Ds) R) A" using S'_eq_X E_eq_Y F1 by fastforce
finally show ?case.
qed
qed
section ‹Function @{const GNF_hd_of}: Conversion to @{const GNF_hd}›
text ‹All epsilon-free grammars can be put into GNF while preserving their language.›
text ‹Putting the productions into GNF via ‹Expand_tri (Solve_tri)› preserves the language.›
lemma Lang_Expand_Solve_tri:
assumes "Eps_free P" "length As ≤ length As'" "distinct (As @ As')" "Nts P ∩ set As' = {}" "A ∉ set As'"
shows "Lang (Expand_tri (As' @ rev As) (Solve_tri As As' P)) A = Lang P A"
using Lang_Solve_tri[OF assms] Expand_tri_Lang[of "(As' @ rev As)"] by blast
text ‹Any grammar can be brought into head GNF.›
theorem GNF_hd_GNF_hd_of: "distinct As ⟹ Nts P ⊆ set As ⟹ GNF_hd (GNF_hd_of As P)"
unfolding GNF_hd_of_def Let_def
apply (rule GNF_hd_Expand_Solve_tri[OF Eps_free_Eps_elim])
using Nts_Eps_elim[of P]
by(simp_all add: freshs_distinct freshs_disj length_freshs)
corollary gnf_hd_gnf_hd_of: "gnf_hd (gnf_hd_of ps)"
unfolding set_gnf_hd_of
apply (rule GNF_hd_GNF_hd_of)
by (simp_all add: set_nts distinct_nts)
lemma distinct_app_freshs: "⟦ distinct As; As' = freshs (set As) As ⟧ ⟹
distinct (As @ As')"
using freshs_disj[of "set As" As]
by (auto simp: distinct_nts freshs_distinct)
text ‹‹GNF_hd_of› preserves the language (modulo ‹[]›):›
theorem Lang_GNF_hd_of: "distinct As ⟹ Nts P ⊆ set As ⟹ A ∈ set As ⟹ Lang (GNF_hd_of As P) A = Lang P A - {[]}"
unfolding GNF_hd_of_def Let_def
apply(rule Lang_Expand_Solve_tri[OF Eps_free_Eps_elim, simplified Lang_Eps_elim])
apply (simp add: length_freshs)
apply (rule distinct_app_freshs;simp_all)
apply (metis (no_types, lifting) ext Int_assoc Int_empty_right Nts_Eps_elim
distinct_app_freshs distinct_append inf.orderE)
apply (meson List.finite_set disjoint_iff freshs_disj subsetD)
done
corollary lang_gnf_hd_of: "A ∈ set (nts ps) ⟹ lang (gnf_hd_of ps) A = lang ps A - {[]}"
unfolding set_gnf_hd_of
apply (rule Lang_GNF_hd_of)
by (auto simp: set_nts distinct_nts)
text ‹Two simple examples:›
lemma "gnf_hd_of [(0, [Nt(0::nat), Tm (1::int)])] = [(1, [Tm 1]), (1, [Tm 1, Nt 1])]"
by eval
lemma "gnf_hd_of [(0, [Nt(0::nat), Tm (1::int)]), (0, [Tm 2]), (8, []), (9, [Nt 8])] =
[(0, [Tm 2]), (0, [Tm 2]), (0, [Tm 2, Nt 1]), (1, [Tm 1]), (1, [Tm 1, Nt 1])]"
by eval
text ‹Example 4.10 \cite{HopcroftU79}:
‹P0› is the input; ‹P1› is the result after Step 1; ‹P3› is the result after Step 2 and 3.›
lemma
"let
P0 =
[(1::int, [Nt 2, Nt 3]), (2,[Nt 3, Nt 1]), (2, [Tm (1::int)]), (3,[Nt 1, Nt 2]), (3,[Tm 0])];
P1 =
[(1, [Nt 2, Nt 3]), (2, [Nt 3, Nt 1]), (2, [Tm 1]),
(3, [Tm 1, Nt 3, Nt 2, Nt 4]), (3, [Tm 0, Nt 4]), (3, [Tm 1, Nt 3, Nt 2]), (3, [Tm 0]),
(4, [Nt 1, Nt 3, Nt 2]), (4, [Nt 1, Nt 3, Nt 2, Nt 4])];
P2 =
[(1, [Tm 1, Nt 3, Nt 2, Nt 4, Nt 1, Nt 3]), (1, [Tm 1, Nt 3, Nt 2, Nt 1, Nt 3]),
(1, [Tm 0, Nt 4, Nt 1, Nt 3]), (1, [Tm 0, Nt 1, Nt 3]), (1, [Tm 1, Nt 3]),
(2, [Tm 1, Nt 3, Nt 2, Nt 4, Nt 1]), (2, [Tm 1, Nt 3, Nt 2, Nt 1]),
(2, [Tm 0, Nt 4, Nt 1]), (2, [Tm 0, Nt 1]), (2, [Tm 1]),
(3, [Tm 1, Nt 3, Nt 2, Nt 4]), (3, [Tm 1, Nt 3, Nt 2]),
(3, [Tm 0, Nt 4]), (3, [Tm 0]),
(4, [Tm 1, Nt 3, Nt 2, Nt 4, Nt 1, Nt 3, Nt 3, Nt 2, Nt 4]), (4, [Tm 1, Nt 3, Nt 2, Nt 4, Nt 1, Nt 3, Nt 3, Nt 2]),
(4, [Tm 0, Nt 4, Nt 1, Nt 3, Nt 3, Nt 2, Nt 4]), (4, [Tm 0, Nt 4, Nt 1, Nt 3, Nt 3, Nt 2]),
(4, [Tm 1, Nt 3, Nt 3, Nt 2, Nt 4]), (4, [Tm 1, Nt 3, Nt 3, Nt 2]),
(4, [Tm 1, Nt 3, Nt 2, Nt 1, Nt 3, Nt 3, Nt 2, Nt 4]), (4, [Tm 1, Nt 3, Nt 2, Nt 1, Nt 3, Nt 3, Nt 2]),
(4, [Tm 0, Nt 1, Nt 3, Nt 3, Nt 2, Nt 4]), (4, [Tm 0, Nt 1, Nt 3, Nt 3, Nt 2])]
in
Solve_tri [3,2,1] [4,5,6] (set P0) = set P1 ∧ Expand_tri [4,1,2,3] (set P1) = set P2"
by eval
section ‹Full Greibach Normal Form›
text ‹One can easily convert head GNF into full GNF by replacing tail terminals
by fresh nonterminals.›
definition Bad_Tms_GNF :: "('n,'t) Prods ⇒ 't set" where
"Bad_Tms_GNF P = ⋃{Tms_syms α | α. ∃A x. (A,x#α) ∈ P}"
definition bad_tms_gnf :: "('n,'t) prods ⇒ 't list" where
"bad_tms_gnf P = fold List.union [tms_syms α. (A,x#α) ← P] []"
lemma set_bad_tms_gnf: "set (bad_tms_gnf P) = Bad_Tms_GNF (set P)"
by (force simp: Bad_Tms_GNF_def bad_tms_gnf_def set_fold_union image_Collect set_tms_syms)
lemma distinct_bad_tms_gnf: "distinct (bad_tms_gnf P)"
by (simp add: bad_tms_gnf_def distinct_fold_union)
lemma GNF_Replace_Tm_tl:
assumes P: "GNF_hd P" and Pf: "Bad_Tms_GNF P ⊆ dom f"
shows "GNF (Replace_Tm_tl f P)"
apply (unfold Replace_Tm_tl_def Replace_Tm_def set_append GNF_Un)
proof (intro conjI GNF_I)
fix A α' assume "(A,α') ∈ {(A, replace_Tm_tl_syms f α) | A α. (A,α) ∈ P}"
then obtain α where AP: "(A,α) ∈ P" and α': "α' = replace_Tm_tl_syms f α" by auto
from AP P obtain a β where [simp]: "α = Tm a # β" by (auto simp: GNF_hd_def)
from α' have [simp]: "α' = Tm a # map (replace_Tm_sym f) β" by (auto simp: replace_Tm_tl_syms_def)
define Bs where "Bs ≡ [case x of Nt B ⇒ B | Tm b ⇒ the (f b). x ← β]"
from Pf AP have "Tms_syms β ⊆ dom f" by (force simp: Bad_Tms_GNF_def)
then have "map (replace_Tm_sym f) β = map Nt Bs"
by (unfold Bs_def, induction β, auto simp: replace_Tm_sym_simps split: sym.splits option.splits)
with α' have "α' = Tm a # map Nt Bs" by simp
then show "∃a Bs. α' = Tm a # map Nt Bs" by blast
qed (auto simp: Replace_Tm_new_def)
definition GNF_of :: "'n list ⇒ 't list ⇒ ('n::fresh0,'t)Prods ⇒ ('n,'t)Prods" where
[code_unfold]: "GNF_of As as P =
(let As' = freshs (set As) As;
P' = Expand_tri (As' @ rev As) (Solve_tri As As' (Eps_elim P))
in Replace_Tm_tl (fresh_map (set As ∪ set As') as) P')"
value "GNF_of [1,2,3] [0,1] {
(1::nat, [Nt 2, Nt 3]),
(2,[Nt 3, Nt 1]), (2, [Tm (1::int)]),
(3,[Nt 1, Nt 2]), (3,[Tm 0])}"
definition gnf_of :: "('n::fresh0,'t)prods ⇒ ('n,'t)prods" where
"gnf_of P =
(let As = nts P;
As' = freshs (set As) As;
P' = expand_tri (As' @ rev As) (solve_tri As As' (eps_elim P));
f = fresh_assoc (set As ∪ set As') (bad_tms_gnf P')
in replace_Tm_tl f P')"
lemma set_gnf_of: "set (gnf_of P) = GNF_of (nts P) (bad_tms_gnf (gnf_hd_of P)) (set P)"
by (simp add: gnf_of_def GNF_of_def Let_def set_replace_Tm_tl set_expand_tri
set_solve_tri set_eps_elim distinct_fold_union map_fst_fresh_assoc distinct_bad_tms_gnf
map_of_fresh_assoc gnf_hd_of_def)
lemma GNF_of_via_GNF_hd_of:
"GNF_of As as P =
(let As' = freshs (set As) As;
f = fresh_map (set As ∪ set As') as
in Replace_Tm_tl f (GNF_hd_of As P))"
by (auto simp: GNF_of_def GNF_hd_of_def Let_def)
theorem GNF_GNF_of:
assumes As: "distinct As" and PAs: "Nts P ⊆ set As"
and Pas: "Bad_Tms_GNF (GNF_hd_of As P) ⊆ set as"
shows "GNF (GNF_of As as P)"
apply (unfold GNF_of_via_GNF_hd_of Let_def)
apply (rule GNF_Replace_Tm_tl)
using GNF_hd_GNF_hd_of[OF As PAs] Pas
by (simp_all add: dom_fresh_map)
theorem Lang_GNF_of:
assumes As: "distinct As" and PAs: "Nts P ⊆ set As"
and Pas: "Bad_Tms_GNF (GNF_hd_of As P) ⊆ set as"
and AAs: "A ∈ set As"
shows "Lang (GNF_of As as P) A = Lang P A - {[]}"
proof-
define As' where "As' = freshs (set As) As"
define f where "f = fresh_map (set As ∪ set As') as"
show ?thesis
apply (unfold GNF_of_via_GNF_hd_of Let_def)
apply (fold As'_def)
apply (fold f_def)
apply (fold Lang_GNF_hd_of[OF As PAs AAs])
proof (rule Lang_Replace_Tm_tl[OF _ _ ])
show "inj_on f (dom f)"
apply (unfold f_def dom_fresh_map)
apply (rule fresh_map_inj_on)
by simp
from fresh_map_disj[of "set As ∪ set As'" as, simplified, folded f_def]
Nts_GNF_hd_of[of As P, folded As'_def] AAs PAs
show "A ∉ ran f" and "ran f ∩ Nts (GNF_hd_of As P) = {}" by auto
qed
qed
corollary gnf_gnf_of: "gnf (gnf_of P)"
apply (unfold set_gnf_of)
apply (rule GNF_GNF_of)
using distinct_nts by (auto simp: set_nts set_bad_tms_gnf set_gnf_hd_of)
theorem lang_gnf_of:
assumes A: "A ∈ set (nts P)"
shows "lang (gnf_of P) A = lang P A - {[]}"
apply (unfold set_gnf_of)
apply (rule Lang_GNF_of)
using distinct_nts A by (auto simp: set_nts set_bad_tms_gnf set_gnf_hd_of)
value "remdups (gnf_of [
(1::nat, [Nt 2, Nt 3]),
(2,[Nt 3, Nt 1]), (2, [Tm (1::int)]),
(3,[Nt 1, Nt 2]), (3,[Tm 0])])"
section ‹Complexity›
text ‹Our method has exponential complexity, which we demonstrate below.
Alternative polynomial methods are described in the literature \cite{BlumK99}.
We start with an informal proof that the blowup of the whole method can be as bad
as $2^{n^2}$, where $n$ is the number of non terminals, and the starting grammar has $4n$ productions.
Consider this grammar, where ‹a› and ‹b› are terminals and we use nested alternatives in the obvious way:
‹A0 → A1 (a | b) | A2 (a | b) | ... | An (a | b) | a | b›
‹A(i+1) → Ai (a | b)›
Expanding all alternatives makes this a grammar of size $4n$.
When converting this grammar into Triangular form, starting with ‹A0›, we find that ‹A0› remains the
same after ‹Expand_hd_rec›, and ‹Solve_lrec› introduces a new additional production for every ‹A0› production,
which we will ignore to simplify things:
Then every ‹Expand_hd_rec› step yields for ‹Ai› these number of productions:
(1) ‹2^(i+1)› productions with rhs ‹Ak (a | b)^(i+1)› for every ‹k ∈ [i+1, n]›,
(2) ‹2^(i+1)› productions with rhs ‹(a | b)^(i+1)›,
(3) ‹2^(i+1)› productions with rhs ‹Ai (a | b)^(i+1)›.
Note that ‹(a | b)^(i+1)› represents all words of length ‹i+1› over ‹{a,b}›.
Solving the left recursion again introduces a new additional production for every production of form (1) and (2),
which we will again ignore for simplicity.
The productions of (3) get removed by ‹Solve_lrec›.
We will not consider the productions of the newly introduced nonterminals.
In the Triangular form, every ‹Ai› has at least ‹2^(i+1)› productions starting with terminals (2)
and ‹2^(i+1)› productions with rhs starting with ‹Ak› for every ‹k ∈ [i+1, n]›.
When expanding the Triangular form starting from ‹An›, which has at least the ‹2^(i+1)› productions from (2),
we observe that the number of productions of ‹Ai› (denoted by ‹#Ai›) is ‹#Ai ≥ 2^(i+1) * #A(i+1)›
(Only considering the productions of the form ‹A(i+1) (a | b)^(i+1)›).
This yields that ‹#Ai ≥ 2^(i+1) * 2^((i+2) + ... + (n+1)) = 2^((i+1) + (i+2) + ... (n+1))›.
Thus ‹#A0 ≥ 2^(1 + 2 + ... + n + (n+1)) = 2^((n+1)*(n+2)/2)›.
Below we prove formally that ‹Expand_tri› can cause exponential blowup.›
text ‹Bad grammar: Constructs a grammar which leads to a exponential blowup when expanded
by ‹Expand_tri›:›
fun bad_grammar :: "nat ⇒ (nat,bool) prods" where
"bad_grammar 0 = [(0, [Tm False]), (0, [Tm True])]"
|"bad_grammar (Suc n) = [(Suc n, Nt n # [Tm False]), (Suc n, Nt n # [Tm True])] @ bad_grammar n"
value "nts (bad_grammar 4)"
lemma bad_gram_simp1: "n < m ⟹ (m,w) ∉ set (bad_grammar n)"
by (induction n rule: bad_grammar.induct) auto
lemma Expand_tri_insert_simp:
"B ∉ set As ⟹ Expand_tri As (insert (B,w) R) = insert (B,w) (Expand_tri As R)"
apply (induction As R rule: Expand_tri.induct)
apply (auto simp add: Let_def Subst_hd_def)apply auto done
lemma Expand_tri_bad_grammar_simp1:
"Expand_tri (rev [0..<Suc n]) (set (bad_grammar (Suc n))) =
{(Suc n, Nt n # [Tm False]), (Suc n, Nt n # [Tm True])} ∪
Expand_tri (rev [0..<Suc n]) (set (bad_grammar n))"
proof (induction n)
case 0
then show ?case by (auto simp: Subst_hd_def)
next
case (Suc n)
have 1: "rev [0..< Suc (Suc n)] = Suc n # rev [0..<Suc n]" by simp
define S where "S ≡ Expand_tri (rev [0..<Suc n]) (set (bad_grammar n))"
show ?case
unfolding 1
apply (simp del: upt_Suc bad_grammar.simps(2)
add: bad_grammar.simps(2)[of "Suc n"] Expand_tri_insert_simp Suc
S_def[symmetric] Subst_hd_def)
by auto
qed
lemma finite_bad_grammar: "finite (set (bad_grammar As))"
by (induction As rule: bad_grammar.induct) (auto simp: bad_grammar.simps(2))
lemma finite_Expand_tri: "finite R ⟹ finite (Expand_tri As R)"
proof (induction As R rule: Expand_tri.induct)
case (1 R)
then show ?case by simp
next
case (2 S Ss R)
let ?S = "{(A, v @ w) |A v w. ∃B. (B, v) ∈ Expand_tri Ss R ∧ (A, Nt B # w) ∈ Expand_tri Ss R ∧ A = S ∧ B ∈ set Ss}"
let ?f = "λ((A,w),(B,v)). (A, v @ (tl w))"
have "?S ⊆ ?f ` (Expand_tri Ss R × Expand_tri Ss R)"
proof
fix x
assume "x ∈ ?S"
then have "∃S v B w. (S,Nt B # w) ∈ Expand_tri Ss R ∧ (B,v) ∈ Expand_tri Ss R ∧ x = (S, v @ w)"
by blast
then obtain S v B w
where P: "(S, Nt B # w) ∈ Expand_tri Ss R ∧ (B, v) ∈ Expand_tri Ss R ∧ x = (S, v @ w)"
by blast
then have 1: "((S, Nt B # w), (B ,v)) ∈ ((Expand_tri Ss R) × (Expand_tri Ss R))" by auto
have "?f ((S, Nt B # w), (B ,v)) = (S, v @ w)" by auto
then have "(S, v @ w) ∈ ?f ` ((Expand_tri Ss R) × (Expand_tri Ss R))" using 1 by force
then show "x ∈ ?f ` ((Expand_tri Ss R) × (Expand_tri Ss R))" using P by simp
qed
then have "finite ?S"
by (meson "2.IH" "2.prems" finite_SigmaI finite_surj)
with 2 show ?case by (auto simp add: Let_def Subst_hd_def)
qed
text ‹The last Nt expanded by ‹Expand_tri› has an exponential number of productions.›
lemma bad_gram_last_expanded_card:
"card ({v. (n, v) ∈ Expand_tri (rev [0..<Suc n]) (set (bad_grammar n))}) = 2 ^ Suc n"
proof(induction n)
case 0
have 4: "{v. v = [Tm False] ∨ v = [Tm True]} = {[Tm False], [Tm True]}" by auto
show ?case by (auto simp: 4 Subst_hd_def)
next
case (Suc n)
have 1: "rev [0..<Suc (Suc n)] = Suc n # rev [0..<Suc n]" by simp
note upt_Suc[simp del]
let ?R = "Expand_tri (rev [0..<Suc (Suc n)]) (set (bad_grammar (Suc n)))"
let ?S = "{v. (Suc n, v) ∈ ?R}"
let ?Rn = "Expand_tri (rev [0..<Suc n]) (set (bad_grammar n))"
let ?Sn = "{v. (n, v) ∈ ?Rn}"
let ?R' = "Expand_tri (rev [0..<Suc n]) (set (bad_grammar (Suc n)))"
let ?X = "{(Al,Bw) ∈ ?R'. Al=Suc n ∧ (∃w B. Bw = Nt B # w ∧ B ≤ n)}"
let ?Y = "{(Suc n, v@w) |v w. ∃B. (Suc n, Nt B # w) ∈ ?X ∧ (B,v) ∈ ?R'}"
have 4: "(Suc n, Bw) ∈ ?R' ⟷ (Suc n, Bw) ∈ set (bad_grammar (Suc n))" for Bw
by (simp add: Expand_tri_simp1)
have "?X = {(Al,Bw) ∈ set (bad_grammar (Suc n)). Al = Suc n ∧ (∃w B. Bw = Nt B#w ∧ B ≤ n)}"
by (auto simp add: Expand_tri_simp1)
also have "... = {(Suc n, Nt n # [Tm False]), (Suc n, Nt n # [Tm True])}"
by (auto simp: bad_gram_simp1)
finally have 5: "?X = …".
then have cons5: "?X = {(Suc n, Nt n # [Tm False]), (Suc n, Nt n # [Tm True])}" by simp
have 6: "?R' = {(Suc n, [Nt n, Tm False]), (Suc n, [Nt n, Tm True])} ∪ Expand_tri (rev[0..<Suc n]) (set (bad_grammar n))"
using Expand_tri_bad_grammar_simp1
by simp
have 8: "(Suc n, w) ∉ Expand_tri (rev [0..<Suc n]) (set (bad_grammar n))" for w
by (simp add: bad_gram_simp1 Expand_tri_simp1)
then have 7: "{(Suc n, [Nt n, Tm False]), (Suc n, [Nt n, Tm True])} ∩ Expand_tri (rev [0..<Suc n]) (set (bad_grammar n)) = {}"
by auto
have "?R' - ?X = Expand_tri (rev [0..<Suc n]) (set (bad_grammar n))" using 7 6 5 by simp
have S_from_Y: "?S = {v. (Suc n, v) ∈ ?Y}"
by (auto simp: 1 Let_def Expand_tri_simp1 bad_gram_simp1 Expand_tri_insert_simp Subst_hd_def)
note bad_grammar.simps(2)[simp del]
have Y_decomp: "?Y = {(Suc n, v @ [Tm False]) | v. (n,v) ∈ ?R'} ∪ {(Suc n, v @ [Tm True]) | v. (n,v) ∈ ?R'}"
(is "?Y = ?Z")
proof
show "?Y ⊆ ?Z"
proof
fix x
assume assm: "x ∈ ?Y"
then have "∃v w. x = (Suc n, v @ w) ∧ (∃B. (Suc n, Nt B # w) ∈ ?X ∧ (B,v) ∈ ?R')" by blast
then obtain v w where P: "x = (Suc n, v @ w) ∧ (∃B. (Suc n, Nt B # w) ∈ ?X ∧ (B,v) ∈ ?R')" by blast
then have cfact:"(Suc n, Nt n # w) ∈ ?X ∧ (n,v) ∈ ?R'" using cons5
by (metis (no_types, lifting) Pair_inject insert_iff list.inject singletonD sym.inject(1))
then have "w = [Tm False] ∨ w = [Tm True]" using cons5
by (metis (no_types, lifting) empty_iff insertE list.inject prod.inject)
then show "x ∈ ?Z" using P cfact by auto
qed
next
show "?Z ⊆ ?Y"
using cons5 by auto
qed
from Y_decomp have S_decomp: "?S = {v@[Tm False] | v. (n,v) ∈ ?R'} ∪ {v@[Tm True] | v. (n,v) ∈ ?R'}"
using S_from_Y by auto
have cardCvR: "card {v. (n, v) ∈ ?R'} = 2 ^ Suc n" using Suc 6 by auto
have "bij_betw (λx. x@[Tm False]) {v. (n, v) ∈ ?R'} {v@[Tm False] | v. (n, v) ∈ ?R'}"
by (auto simp add: bij_betw_def inj_on_def)
then have cardS1: "card {v@[Tm False] | v. (n, v) ∈ ?R'} = 2 ^ Suc n"
using cardCvR by (auto simp add: bij_betw_same_card)
have "bij_betw (λx. x@[Tm True]) {v. (n, v) ∈ ?R'} {v@[Tm True] | v. (n,v) ∈ ?R'}"
by (auto simp add: bij_betw_def inj_on_def)
then have cardS2: "card {v@[Tm True] | v. (n,v) ∈ ?R'} = 2 ^ Suc n"
using cardCvR by (auto simp add: bij_betw_same_card)
have fin_R': "finite ?R'" using finite_bad_grammar finite_Expand_tri by blast
let ?f1 = "λ(C,v). v@[Tm False]"
have "{v@[Tm False] | v. (n,v) ∈ ?R'} ⊆ ?f1 ` ?R'" by auto
then have fin1: "finite {v@[Tm False] | v. (n,v) ∈ ?R'}"
using fin_R' by (meson finite_SigmaI finite_surj)
let ?f2 = "λ(C,v). v@[Tm True]"
have "{v@[Tm True] | v. (n,v) ∈ ?R'} ⊆ ?f2 ` ?R'" by auto
then have fin2: "finite {v@[Tm True] | v. (n,v) ∈ ?R'}"
using fin_R' by (meson finite_SigmaI finite_surj)
have fin_sets: "finite {v@[Tm False] | v. (n,v) ∈ ?R'} ∧ finite {v@[Tm True] | v. (n,v) ∈ ?R'}"
using fin1 fin2 by simp
have "{v@[Tm False] | v. (n,v) ∈ ?R'} ∩ {v@[Tm True] | v. (n,v) ∈ ?R'} = {}" by auto
then have "card ?S = 2^(Suc n) + 2^(Suc n)"
using S_decomp cardS1 cardS2 fin_sets
by (auto simp add: card_Un_disjoint)
then show ?case by auto
qed
text ‹The productions resulting from ‹Expand_tri (bad_grammar)› have at least exponential size.›
theorem Expand_tri_blowup:
"card (Expand_tri (rev [0..<Suc n]) (set (bad_grammar n))) ≥ 2^(Suc n)"
(is "card ?R ≥ _")
proof -
have fin: "finite ?R"
using finite_bad_grammar finite_Expand_tri by blast
have "{v. (n,v) ∈ ?R} ⊆ snd ` ?R" by (force simp del: upt_Suc simp: image_def)
from fin card_mono[OF _ this, unfolded bad_gram_last_expanded_card]
card_image_le[OF fin, of snd]
show ?thesis by (auto simp del: upt_Suc)
qed
lemma in_dep_on_bad_grammar: "n ∈ dep_on (set (bad_grammar m)) l ⟷ l = Suc n ∧ n < m"
by (induction m, auto simp: dep_on_insert)
lemma Triangular_bad_grammar: "Triangular [m..<n] (set (bad_grammar l))"
proof (induction "n-m" arbitrary: n m)
case 0
then show ?case by (auto simp: dep_on_def)
next
case (Suc d)
then have 1: "[m..<n] = m # [Suc m..<n]" by (simp add: upt_conv_Cons)
from Suc have "d = n - Suc m" by simp
from Suc(1)[OF this]
show ?case by (auto simp add: 1 in_dep_on_bad_grammar)
qed
lemma Solve_tri_bad_grammar:
"length As' = Suc n ⟹ Solve_tri [0..<Suc n] As' (set (bad_grammar l)) = set (bad_grammar l)"
apply (rule Solve_tri_id[OF Triangular_bad_grammar]) by simp
end