(* Author: Moritz Roos, Tobias Nipkow *) section ‹Dyck Languages over Type ‹syms›› theory Dyck_Language_Syms imports Dyck_Language.Dyck_Language Context_Free_Grammar.Context_Free_Grammar begin section‹Versions of \<^const>‹bal› and restriction to ‹Γ› for @{type syms}› subsection‹Function \<^term>‹bal_tm›› definition bal_tm where ‹bal_tm = bal o (map destTm) o (filter isTm)› lemma bal_tm_empty[simp]: ‹bal_tm []› by (simp add: bal_tm_def) lemma bal_tm_append[simp]: ‹bal_tm xs ⟹ bal_tm ys ⟹ bal_tm (xs @ ys)› unfolding bal_tm_def by simp lemma bal_tm_surr[simp]: ‹bal_tm xs ⟹ bal_tm (Tm (Open a) # xs @ [Tm (Close a)])› unfolding bal_tm_def by simp lemma bal_tm_prepend_Nt[simp]: ‹bal_tm (Nt A # xs) = bal_tm xs› by (simp add: bal_tm_def) lemma bal_tm2[simp]: "bal_tm [Tm (Open a), Tm (Close a)]" using bal_tm_surr[of "[]"] by simp lemma bal_iff_bal_tm[simp]: ‹bal_tm (map Tm xs) = bal xs› unfolding bal_tm_def by simp lemma bal_tm_append_inv: "bal_tm (u @ v) ⟹ bal_tm u ⟹ bal_tm v" unfolding bal_tm_def by(auto dest: bal_append_inv) lemma bal_tm_inside: "bal_tm b ⟹ bal_tm (v @ b @ w) = bal_tm (v @ w)" unfolding bal_tm_def by(auto) subsection‹Function ‹snds_in_tm›› text‹Restriction to ‹Γ› for a list of symbols:› definition snds_in_tm where ‹snds_in_tm Γ w = (snd ` set(map destTm (filter isTm w)) ⊆ Γ)› lemma snds_in_tm_Nt[simp]: ‹snds_in_tm Γ (Nt A # xs) = snds_in_tm Γ xs› unfolding snds_in_tm_def by auto lemma snds_in_tm_append[simp]: ‹snds_in_tm Γ (xs@ys) = (snds_in_tm Γ xs ∧ snds_in_tm Γ ys)› unfolding snds_in_tm_def by auto lemma Dyck_langI_tm[simp]: ‹xs ∈ Dyck_lang Γ ⟷ bal_tm (map Tm xs) ∧ snds_in_tm Γ (map Tm xs)› unfolding bal_tm_def snds_in_tm_def by auto (* subsection‹Lifting \<^const>‹bal› and \<^const>‹bal_stk› to @{type syms}› subsubsection‹Function ‹bal_stk_tm›› text‹A version of \<^term>‹bal_stk› but for a symbol list that might contain nonterminals (they are ignored via filtering).› definition bal_stk_tm :: "'t list ⇒ ('n, 't bracket) syms ⇒ 't list * ('n, 't bracket) syms" where ‹bal_stk_tm x y ≡ (fst ((bal_stk x o map destTm o filter isTm) y), map Tm (snd ((bal_stk x o map destTm o filter isTm) y)))› lemma bal_stk_tm_append: "bal_stk_tm s1 (xs @ ys) = (let (s1',xs') = bal_stk_tm s1 xs in bal_stk_tm s1' (xs' @ ys))" unfolding bal_stk_tm_def apply simp by (metis (no_types, lifting) bal_stk_append split_beta) lemma bal_stk_tm_append_if[simp]: "bal_stk_tm s1 xs = (s2,[]) ⟹ bal_stk_tm s1 (xs @ ys) = bal_stk_tm s2 ys" by(simp add: bal_stk_tm_append[of _ xs]) lemma bal_stk_tm_if_bal_tm: "bal_tm xs ⟹ bal_stk_tm s xs = (s,[])" unfolding bal_stk_tm_def by (simp add: bal_tm_def bal_stk_if_bal)+ lemma bal_tm_insert_AB: assumes u: "bal_tm u" shows "u = v@w ⟹ bal_tm (v @ Tm (Open x) # Tm (Close x) # w)" using u unfolding bal_tm_def by (auto intro!: bal_insert_AB) lemma bal_tm_insert_Nt: "bal_tm u ⟹ u = v@w ⟹ bal_tm (v @ Nt A # w)" unfolding bal_tm_def by auto corollary bal_stk_tm_iff_bal_tm: "bal_stk_tm [] w = ([],[]) ⟷ bal_tm w" unfolding bal_stk_tm_def bal_tm_def o_def by (metis bal_stk_iff_bal map_is_Nil_conv split_pairs) lemma bal_stk_tm_append_inv: ‹bal_stk_tm s1 (xs@ys) = (s1', []) ⟹ let (s1', xs') = bal_stk_tm s1 xs in bal_stk_tm s1 xs = (s1', [])› unfolding bal_stk_tm_def Let_def apply auto by (smt (verit, del_insts) case_prodE sndI bal_stk_append_inv surjective_pairing) *) end