Theory Pre_Star_CNF
section ‹$Pre^*$ Optimized for Grammars in CNF›
theory Pre_Star_CNF
imports Pre_Star
begin
text‹
Bouajjani et al. \<^cite>‹bouajjani2000efficient› have proposed in an improved algorithm
for grammars in extended Chomsky Normal Form.
This theory proves core properties (correctness and termination) of the algorithm.
›
subsection‹Preliminaries›
text ‹Extended Chomsky Normal Form:›
definition CNF1 :: "('n, 't) Prods ⇒ bool" where
"CNF1 P ≡ (∀(A, β) ∈ P.
(β = []) ∨
(∃a. β = [Tm a]) ∨
(∃B. β = [Nt B]) ∨
(∃B C. β = [Nt B, Nt C])
)"
type_synonym ('s, 'n, 't) tran = "'s × ('n, 't) sym × 's"
type_synonym ('s, 'n, 't) trans = "('s, 'n, 't) tran set"
type_synonym ('s, 'n, 't) directT = "('s, 'n, 't) tran ⇒ ('s, 'n, 't) trans"
type_synonym ('s, 'n, 't) implT = "('s, 'n, 't) tran ⇒ (('s, 'n, 't) tran × ('s, 'n, 't) tran) set"
record ('s, 'n, 't) alg_state =
rel :: "('s, 'n, 't) trans"
trans :: "('s, 'n, 't) trans"
direct :: "('s, 'n, 't) directT"
impl :: "('s, 'n, 't) implT"
subsection‹Procedure›
definition alg_state_new :: "('n, 't) Prods ⇒ 's set ⇒ ('s, 'n, 't) trans ⇒ ('s, 'n, 't) alg_state" where
"alg_state_new P Q T ≡ ⦇
rel = {},
trans = T
∪ { (q, Nt A, q) | q A. (A, []) ∈ P ∧ q ∈ Q }
∪ { (q, Nt A, q') | q q' A. ∃a. (A, [Tm a]) ∈ P ∧ (q, Tm a, q') ∈ T ∧ q ∈ Q ∧ q' ∈ Q },
direct = (λ(q, X, q'). case X of
Nt B ⇒ { (q, Nt A, q') | A. (A, [Nt B]) ∈ P ∧ q ∈ Q ∧ q' ∈ Q } |
Tm b ⇒ {}
),
impl = (λ(q, X, q'). case X of
Nt B ⇒ { ((q', Nt C, q''), (q, Nt A, q'')) | q'' A C. (A, [Nt B, Nt C]) ∈ P ∧ q ∈ Q ∧ q' ∈ Q ∧ q'' ∈ Q } |
Tm b ⇒ {}
)
⦈"
definition alg_inner_pre :: "('s, 'n, 't) alg_state ⇒ ('s, 'n, 't) tran ⇒ ('s, 'n, 't) alg_state" where
"alg_inner_pre S t ≡ S ⦇
rel := (rel S) ∪ {t},
trans := ((trans S) - {t}) ∪ direct S t,
direct := (direct S) (t := {})
⦈"
definition alg_inner_post :: "('s, 'n, 't) alg_state ⇒ ('s, 'n, 't) tran ⇒ ('s, 'n, 't) alg_state" where
"alg_inner_post S t ≡ (
let i = impl S t in
S ⦇
trans := (trans S) ∪
snd ` { (t', t'') ∈ i. t' ∈ rel S },
direct := (λt'. direct S t' ∪
snd ` { (t'2, t'') ∈ i. t' = t'2 ∧ t' ∉ rel S }
),
impl := (impl S) (t := {})
⦈
)"
definition alg_outer_step :: "('s, 'n, 't) alg_state ⇒ ('s, 'n, 't) tran ⇒ ('s, 'n, 't) alg_state" where
"alg_outer_step S t ≡ alg_inner_post (alg_inner_pre S t) t"
abbreviation "alg_outer_step_lts S t ≡ rel S ∪ {t}"
abbreviation "alg_outer_step_trans S t ≡ (trans S) - {t} ∪ direct S t ∪ snd ` { (t', t'') ∈ impl S t. t' ∈ rel S ∪ {t} }"
abbreviation "alg_outer_step_trans' S t ≡ (trans S) - {t} ∪ direct S t ∪ {t''. ∃t'. (t', t'') ∈ impl S t ∧ t' ∈ rel S ∪ {t} }"
abbreviation "alg_outer_step_direct S t ≡ (λt'. ((direct S) (t := {})) t' ∪ snd ` { (t'2, t'') ∈ impl S t. t' = t'2 ∧ t' ∉ (rel S) ∪ {t} })"
abbreviation "alg_outer_step_direct' S t ≡ (λt'. ((direct S) (t := {})) t' ∪ {t''. (t', t'') ∈ impl S t ∧ t' ∉ (rel S) ∪ {t} })"
abbreviation "alg_outer_step_impl S t ≡ (impl S) (t := {})"
lemma alg_outer_step_trans_eq[simp]:
"alg_outer_step_trans S t = alg_outer_step_trans' S t"
by (standard; force)
lemma alg_outer_step_direct_eq[simp]:
"alg_outer_step_direct S t = alg_outer_step_direct' S t"
by force
lemma alg_outer_step_simps[simp]:
shows "rel (alg_outer_step S t) = alg_outer_step_lts S t"
and "trans (alg_outer_step S t) = alg_outer_step_trans S t"
and "direct (alg_outer_step S t) = alg_outer_step_direct S t"
and "impl (alg_outer_step S t) = alg_outer_step_impl S t"
proof -
define R where "R ≡ rel S ∪ {t}"
define T where "T ≡ ((trans S) - {t}) ∪ direct S t"
define D where "D ≡ (direct S) (t := {})"
define I where "I ≡ impl S"
note defs = R_def T_def D_def I_def
have R_subst: "rel (alg_inner_pre S t) = R"
by (simp add: R_def alg_inner_pre_def)
have T_subst: "trans (alg_inner_pre S t) = T"
by (simp add: T_def alg_inner_pre_def)
have D_subst: "direct (alg_inner_pre S t) = D"
by (simp add: D_def alg_inner_pre_def)
have I_subst: "impl (alg_inner_pre S t) = I"
by (simp add: I_def alg_inner_pre_def)
note substs = R_subst T_subst D_subst I_subst
have "rel (alg_inner_post (alg_inner_pre S t) t) = R ∪ {t}"
unfolding alg_inner_post_def substs
by (metis (no_types, lifting) R_def R_subst Un_absorb Un_insert_right alg_state.select_convs(1) alg_state.surjective alg_state.update_convs(2,3,4) sup_bot.right_neutral)
then show "rel (alg_outer_step S t) = rel S ∪ {t}"
by (simp add: substs defs alg_outer_step_def)
have "trans (alg_inner_post (alg_inner_pre S t) t) = T ∪ snd ` { (t', t'') ∈ I t. t' ∈ R }"
unfolding alg_inner_post_def substs
by (metis (no_types, lifting) alg_state.select_convs(2) alg_state.surjective alg_state.update_convs(2,3,4))
then show "trans (alg_outer_step S t) = alg_outer_step_trans S t"
by (simp add: substs defs alg_outer_step_def)
have "direct (alg_inner_post (alg_inner_pre S t) t) = (λt'. D t' ∪ snd ` { (t'2, t'') ∈ I t. t' = t'2 ∧ t' ∉ R })"
unfolding alg_inner_post_def substs
using alg_state.select_convs(3) alg_state.surjective alg_state.update_convs(1,2,3,4)
proof -
have "∀p. direct (alg_inner_pre S t ⦇trans := T ∪ snd ` {(pa, p). (pa, p) ∈ I t ∧ pa ∈ R}, direct := λp. D p ∪ snd ` {(pb, pa). (pb, pa) ∈ I t ∧ p = pb ∧ p ∉ R}, impl := I(t := {})⦈) p = D p ∪ snd ` {(pb, pa). (pb, pa) ∈ I t ∧ p = pb ∧ p ∉ R}"
by simp
then show "direct (let r = I t in alg_inner_pre S t ⦇trans := T ∪ snd ` {(pa, p). (pa, p) ∈ r ∧ pa ∈ R}, direct := λp. D p ∪ snd ` {(pb, pa). (pb, pa) ∈ r ∧ p = pb ∧ p ∉ R}, impl := I(t := {})⦈) = (λp. D p ∪ snd ` {(pb, pa). (pb, pa) ∈ I t ∧ p = pb ∧ p ∉ R})"
by meson
qed
then show "direct (alg_outer_step S t) = alg_outer_step_direct S t"
by (simp add: substs defs alg_outer_step_def)
have "impl (alg_inner_post (alg_inner_pre S t) t) = I (t := {})"
unfolding alg_inner_post_def substs
by (metis (no_types, lifting) alg_state.select_convs(4) alg_state.surjective alg_state.update_convs(4))
then show "impl (alg_outer_step S t) = alg_outer_step_impl S t"
by (simp add: substs defs alg_outer_step_def)
qed
definition alg_outer :: "('s, 'n, 't) alg_state ⇒ ('s, 'n, 't) alg_state option" where
"alg_outer ≡ while_option (λS. trans S ≠ {}) (λS. alg_outer_step S (SOME x. x ∈ trans S))"
lemma alg_outer_rule:
assumes "⋀S x. P S ⟹ x ∈ trans S ⟹ P (alg_outer_step S x)"
and "alg_outer S = Some S'"
shows "P S ⟹ P S'"
proof -
let ?b = "λS. trans S ≠ {}"
let ?c = "λS. alg_outer_step S (SOME x. x ∈ trans S)"
have "⋀S. P S ⟹ trans S ≠ {} ⟹ P (alg_outer_step S (SOME x. x ∈ trans S))"
by (simp add: assms some_in_eq)
with assms(2) show "P S ⟹ P S'"
unfolding alg_outer_def using while_option_rule[where b="?b" and c="?c"] by blast
qed
subsection‹Correctness›
subsubsection‹Subset›
definition pre_star_alg_sub_inv :: "('s, 'n, 't) trans ⇒ ('s, 'n, 't) alg_state ⇒ bool" where
"pre_star_alg_sub_inv T' S ≡ (
(trans S) ⊆ T' ∧ (rel S) ⊆ T' ∧
(∀t' ∈ T'. ∀t ∈ direct S t'. t ∈ T') ∧
(∀t ∈ T'. ∀(t', t'') ∈ impl S t. t' ∈ T' ⟶ t'' ∈ T')
)"
lemma alg_state_new_inv:
assumes "pre_star_lts P Q T = Some T'"
shows "pre_star_alg_sub_inv T' (alg_state_new P Q T)"
proof -
define S where "S = alg_state_new P Q T"
have invR: "(rel S) ⊆ T'"
by (simp add: S_def alg_state_new_def)
have invT: "(trans S) ⊆ T'"
using pre_star_lts_mono[OF assms] pre_star_lts_refl[OF assms] pre_star_lts_singleton[OF assms]
by(auto simp add: S_def alg_state_new_def)
have "⋀q q' X t. (q, X, q') ∈ T' ⟹ t ∈ direct S (q, X, q') ⟹ t ∈ T'"
proof -
fix t and q X q'
assume "(q, X, q') ∈ T'" and t_in: "t ∈ direct S (q, X, q')"
show "t ∈ T'" proof (cases X)
case (Nt B)
then have "direct S (q, X, q') = { (q, Nt A, q') | A. (A, [Nt B]) ∈ P ∧ q ∈ Q ∧ q' ∈ Q }"
by (simp add: S_def alg_state_new_def)
then obtain A where t_split: "t = (q, Nt A, q')"
and "(A, [Nt B]) ∈ P"
and inQ: "q ∈ Q ∧ q' ∈ Q"
using prod_cases3 t_in by auto
moreover have "(q, Nt B, q') ∈ T'"
using ‹(q, X, q') ∈ T'› Nt by blast
moreover note assms
ultimately have "(q, Nt A, q') ∈ T'"
by (intro pre_star_lts_singleton) (use inQ in blast)+
then show ?thesis
by (simp add: t_split)
next
case (Tm b)
then have "direct S (q, X, q') = {}"
by (simp add: S_def alg_state_new_def)
then show ?thesis
using t_in by blast
qed
qed
then have invD: "∀t' ∈ T'. ∀t ∈ direct S t'. t ∈ T'"
by fast
have "⋀t t' t''. t ∈ T' ⟹ (t', t'') ∈ impl S t ⟹ t' ∈ T' ⟹ t'' ∈ T'"
proof -
fix t t' t''
assume "t ∈ T'" and "(t', t'') ∈ impl S t" and "t' ∈ T'"
obtain q q' X⇩1 where t_split: "t = (q, X⇩1, q')"
by (elim prod_cases3)
show "t'' ∈ T'" proof (cases X⇩1)
case (Nt B)
have "impl S t = {((q', Nt C, q''), (q, Nt A, q'')) |q'' A C.
(A, [Nt B, Nt C]) ∈ P ∧ q ∈ Q ∧ q' ∈ Q ∧ q'' ∈ Q}"
by (simp add: S_def t_split Nt alg_state_new_def)
then obtain q'' A C where t'_split: "t' = (q', Nt C, q'')"
and t''_split: "t'' = (q, Nt A, q'')" and "(A, [Nt B, Nt C]) ∈ P"
and inQ: "q ∈ Q ∧ q' ∈ Q & q'' ∈ Q"
using ‹(t', t'') ∈ impl S t› by force
note ‹(A, [Nt B, Nt C]) ∈ P› and assms
moreover have "(q', Nt C, q'') ∈ T'"
using ‹t' ∈ T'› by (simp add: t'_split)
moreover have "(q, Nt B, q') ∈ T'"
using ‹t ∈ T'› by (simp add: t_split Nt)
ultimately have "(q, Nt A, q'') ∈ T'"
by (intro pre_star_lts_impl) (use inQ in blast)+
then show ?thesis
unfolding t''_split by assumption
next
case (Tm b)
have "impl S t = {}"
by (simp add: S_def t_split Tm alg_state_new_def)
then show ?thesis
using ‹(t', t'') ∈ impl S t› by simp
qed
qed
then have invI: "∀t ∈ T'. ∀(t', t'') ∈ impl S t. t' ∈ T' ⟶ t'' ∈ T'"
by fast
from invR invT invD invI show ?thesis
unfolding pre_star_alg_sub_inv_def S_def by blast
qed
lemma alg_outer_step_inv:
assumes "pre_star_lts P Q T = Some T'" and "t ∈ trans S" and "pre_star_alg_sub_inv T' S"
shows "pre_star_alg_sub_inv T' (alg_outer_step S t)"
proof -
note inv[simp] = assms(3)[unfolded pre_star_alg_sub_inv_def]
have [simp]: "t ∈ T'"
using assms(2) assms(3) unfolding pre_star_alg_sub_inv_def by blast
moreover have invi: "∀(t', t'') ∈ impl (alg_outer_step S t) t. t' ∈ T' ⟶ t'' ∈ T'"
by simp
moreover have invR: "rel (alg_outer_step S t) ⊆ T'"
by simp
moreover have invT: "trans (alg_outer_step S t) ⊆ T'"
unfolding alg_outer_step_simps(2) alg_outer_step_trans_eq
using inv invi ‹t ∈ T'› by blast
moreover have invD: "∀t' ∈ T'. ∀t ∈ direct (alg_outer_step S t) t'. t ∈ T'"
unfolding alg_outer_step_simps(3) alg_outer_step_direct_eq using inv invi ‹t ∈ T'›
by (metis (no_types, lifting) Un_iff case_prod_conv empty_iff fun_upd_apply mem_Collect_eq)
moreover have invI: "∀t⇩2 ∈ T'. ∀(t', t'') ∈ impl (alg_outer_step S t) t⇩2. t' ∈ T' ⟶ t'' ∈ T'"
by simp
ultimately show ?thesis
unfolding pre_star_alg_sub_inv_def by blast
qed
lemma alg_outer_inv:
assumes "pre_star_lts P Q T = Some T'" and "pre_star_alg_sub_inv T' S"
and "alg_outer S = Some S'"
shows "pre_star_alg_sub_inv T' S'"
proof -
note assms' = assms(1,2) assms(3)[unfolded alg_outer_def]
have "⋀s. pre_star_alg_sub_inv T' s ⟹ trans s ≠ {} ⟹
pre_star_alg_sub_inv T' (alg_outer_step s (SOME x. x ∈ trans s))"
by (rule alg_outer_step_inv; use assms someI_ex in fast)
then show ?thesis
by (rule while_option_rule[where P="pre_star_alg_sub_inv T'"]) (use assms' in blast)+
qed
lemma pre_star_alg_sub:
fixes P and T
assumes "alg_outer (alg_state_new P Q T) = Some S'" and "pre_star_lts P Q T = Some T'"
shows "rel S' ⊆ T'"
proof -
have "pre_star_alg_sub_inv T' (alg_state_new P Q T)"
using assms by (elim alg_state_new_inv)
with assms have "pre_star_alg_sub_inv T' S'"
by (intro alg_outer_inv[where S="alg_state_new P Q T" and T'=T' and S'=S']; simp)
then show ?thesis
unfolding pre_star_alg_sub_inv_def by blast
qed
subsubsection‹Super-Set›
lemma alg_outer_fixpoint: "alg_outer S = Some S' ⟹ alg_outer S' = Some S'"
unfolding alg_outer_def by (metis (lifting) while_option_stop while_option_unfold)
lemma pre_star_alg_trans_empty: "alg_outer S = Some S' ⟹ trans S' = {}"
using while_option_stop unfolding alg_outer_def by fast
lemma alg_outer_step_direct: "t ≠ t' ⟹ direct S t' ⊆ direct (alg_outer_step S t) t'"
by simp
lemma alg_outer_step_impl: "(impl S) (t := {}) = impl (alg_outer_step S t)"
by simp
lemma alg_outer_step_impl_to_trans[intro]:
assumes "(t', t'') ∈ impl S t" and "t' ∈ rel S ∨ t = t'"
shows "t'' ∈ trans (alg_outer_step S t)"
using assms unfolding alg_outer_step_simps alg_outer_step_trans_eq by blast
lemma alg_outer_step_impl_to_direct[intro]:
assumes "(t', t'') ∈ impl S t" and "t' ∉ rel S" and "t ≠ t'"
shows "t'' ∈ direct (alg_outer_step S t) t'"
using assms unfolding alg_outer_step_simps alg_outer_step_direct_eq by blast
lemma pre_star_alg_trans_to_lts:
assumes "alg_outer S = Some S'"
shows "trans S ⊆ rel S'"
proof
fix x
assume "x ∈ trans S"
have "x ∈ trans S' ∨ x ∈ rel S'"
by (rule alg_outer_rule[where P="λS. x ∈ trans S ∨ x ∈ rel S"]; use assms ‹x ∈ trans S› in auto)
then show "x ∈ rel S'"
using assms pre_star_alg_trans_empty by blast
qed
lemma pre_star_alg_direct_to_lts:
fixes S⇩0 :: "('s, 'n, 't) alg_state"
assumes "alg_outer S⇩0 = Some S'"
and "t ∉ rel S⇩0" and "t ∈ rel S'"
shows "direct S⇩0 t ⊆ rel S'"
proof -
let ?I = "λS. (t ∉ rel S ∧ direct S⇩0 t ⊆ direct S t) ∨ (direct S⇩0 t ⊆ rel S ∪ trans S)"
have "⋀S t. ?I S ⟹ t ∈ trans S ⟹ ?I (alg_outer_step S t)"
proof -
fix S :: "('s, 'n, 't) alg_state" and t'
assume assm1: "(t ∉ rel S ∧ direct S⇩0 t ⊆ direct S t) ∨ (direct S⇩0 t ⊆ rel S ∪ trans S)"
and assm2: "t' ∈ trans S"
show "?I (alg_outer_step S t')"
proof (cases "t = t'")
case True
then show ?thesis
using assm1 by auto
next
case False
consider "t ∉ rel S ∧ direct S⇩0 t ⊆ direct S t" | "direct S⇩0 t ⊆ rel S ∪ trans S"
using assm1 by blast
then show ?thesis
by (cases; auto)
qed
qed
with assms have "?I S'"
by (elim alg_outer_rule[where P="?I"]) simp+
then show ?thesis
using assms pre_star_alg_trans_empty by blast
qed
lemma pre_star_alg_impl_to_lts:
fixes S⇩0 :: "('s, 'n, 't) alg_state"
assumes "alg_outer S⇩0 = Some S'"
and "t ∉ rel S⇩0" and "t' ∉ rel S⇩0"
and "(t', t'') ∈ impl S⇩0 t"
and "t ∈ rel S'" and "t' ∈ rel S'"
shows "t'' ∈ rel S'"
proof -
let ?I = "λS. (t ∉ rel S ∧ (t', t'') ∈ impl S t)
∨ (t' ∉ rel S ∧ t'' ∈ direct S t')
∨ (t'' ∈ rel S ∪ trans S)"
have "⋀S x. ?I S ⟹ x ∈ trans S ⟹ ?I (alg_outer_step S x)"
proof -
fix S :: "('s, 'n, 't) alg_state" and x
assume "?I S" and "x ∈ trans S"
then show "?I (alg_outer_step S x)"
proof (elim disjE)
assume assm1: "x ∈ trans S" and assm2: "t ∉ rel S ∧ (t', t'') ∈ impl S t"
then show "?I (alg_outer_step S x)"
proof (cases "x = t")
case True
then show ?thesis
proof (cases "t' ∈ rel S ∨ t = t'")
case True
with assm2 have "t'' ∈ trans (alg_outer_step S t)"
by (intro alg_outer_step_impl_to_trans[of t' t'' S t]; simp)
then show ?thesis
by (simp add: ‹x = t›)
next
case False
then have "t' ∉ rel S ∪ {t}"
using False by blast
then have "t' ∉ rel (alg_outer_step S t)"
by simp
moreover with False assm2 have "t'' ∈ direct (alg_outer_step S t) t'"
by (intro alg_outer_step_impl_to_direct[of t' t'' S t]; simp)
ultimately show ?thesis
by (simp add: ‹x = t›)
qed
next
case False
then show ?thesis
using alg_outer_step_impl assm2 by simp
qed
next
assume assm1: "x ∈ trans S" and assm2: "t' ∉ rel S ∧ t'' ∈ direct S t'"
then show "?I (alg_outer_step S x)"
by (cases "x = t'"; simp)
next
assume "x ∈ trans S" and "t'' ∈ rel S ∪ trans S"
then show "?I (alg_outer_step S x)"
by force
qed
qed
with assms have "?I S'"
by (elim alg_outer_rule[where P="?I"]) simp+
then show ?thesis proof (elim disjE)
assume "t ∉ rel S' ∧ (t', t'') ∈ impl S' t"
then show "t'' ∈ rel S'"
using assms(5) by blast
next
assume "t' ∉ rel S' ∧ t'' ∈ direct S' t'"
moreover have "alg_outer S' = Some S'"
using assms(1) by (rule alg_outer_fixpoint)
ultimately show "t'' ∈ rel S'"
using pre_star_alg_direct_to_lts assms(6) by blast
next
assume " t'' ∈ rel S' ∪ trans S'"
then show "t'' ∈ rel S'"
using assms(1) pre_star_alg_trans_empty by blast
qed
qed
lemma pre_star_alg_new_refl_to_trans:
assumes "S = alg_state_new P Q T" and "(A, []) ∈ P" and "q ∈ Q"
shows "(q, Nt A, q) ∈ trans S"
using assms by (simp add: alg_state_new_def)
lemma pre_star_alg_refl_to_lts:
assumes "alg_outer (alg_state_new P Q T) = Some S'" and "(A, []) ∈ P" and "q ∈ Q"
shows "(q, Nt A, q) ∈ rel S'"
using assms pre_star_alg_new_refl_to_trans pre_star_alg_trans_to_lts by fast
lemma pre_star_alg_singleton_nt_to_lts:
assumes "alg_outer (alg_state_new P Q T) = Some S'"
and "(A, [Nt B]) ∈ P" and "q ∈ Q" and "q' ∈ Q"
shows "(q, Nt B, q') ∈ rel S' ⟹ (q, Nt A, q') ∈ rel S'"
proof -
have "(q, Nt A, q') ∈ direct (alg_state_new P Q T) (q, Nt B, q')"
using assms by (simp add: alg_state_new_def)
moreover have "(q, Nt B, q') ∉ rel (alg_state_new P Q T)"
by (simp add: alg_state_new_def)
ultimately show "(q, Nt B, q') ∈ rel S' ⟹ (q, Nt A, q') ∈ rel S'"
using assms(1) pre_star_alg_direct_to_lts by blast
qed
lemma pre_star_alg_tm_only_from_delta:
fixes S' :: "('s, 'n, 't) alg_state"
assumes "alg_outer (alg_state_new P Q T) = Some S'"
and "(q, Tm b, q') ∈ rel S'" and "q ∈ Q" and "q' ∈ Q"
shows "(q, Tm b, q') ∈ T"
proof -
define i where "i ≡ (λt. t = (q, Tm b::('n, 't) sym, q') ⟶ t ∈ T)"
define I :: "('s, 'n, 't) alg_state ⇒ bool"
where "I ≡ (λS. (∀t ∈ rel S. i t) ∧ (∀t ∈ trans S. i t)
∧ (∀t. ∀t' ∈ direct S t. i t') ∧ (∀t. ∀(t', t'') ∈ impl S t. i t' ∧ i t''))"
have "I (alg_state_new P Q T)"
unfolding alg_state_new_def I_def i_def
by (auto split: sym.splits intro: sym.exhaust)
moreover have "⋀S t. I S ⟹ t ∈ trans S ⟹ I (alg_outer_step S t)"
unfolding I_def i_def alg_outer_step_simps
by (auto split: sym.splits; blast)
ultimately have "I S'"
using assms(1) by (elim alg_outer_rule)
then show ?thesis
using assms(2) by (simp add: I_def i_def)
qed
lemma pre_star_alg_singleton_tm_to_lts:
assumes "alg_outer (alg_state_new P Q T) = Some S'" and "(A, [Tm b]) ∈ P"
and "(q, Tm b, q') ∈ rel S'" and "q ∈ Q" and "q' ∈ Q"
shows "(q, Nt A, q') ∈ rel S'"
proof -
have "(q, Tm b, q') ∈ T"
using assms pre_star_alg_tm_only_from_delta by fast
then have "(q, Nt A, q') ∈ trans (alg_state_new P Q T)"
by (auto simp: alg_state_new_def assms)
then show ?thesis
using pre_star_alg_trans_to_lts assms(1) by blast
qed
lemma pre_star_alg_singleton_to_lts:
assumes "alg_outer (alg_state_new P Q T) = Some S'"
and "(A, [X]) ∈ P" and "q ∈ Q" and "q' ∈ Q"
shows "(q, X, q') ∈ rel S' ⟹ (q, Nt A, q') ∈ rel S'"
using assms pre_star_alg_singleton_nt_to_lts pre_star_alg_singleton_tm_to_lts by (cases X; fast)
lemma pre_star_alg_dual_to_lts:
assumes "alg_outer (alg_state_new P Q T) = Some S'" and "(A, [Nt B, Nt C]) ∈ P"
and "(q, Nt B, q') ∈ rel S'" and "(q', Nt C, q'') ∈ rel S'"
and "q ∈ Q" and "q' ∈ Q" and "q'' ∈ Q"
shows "(q, Nt A, q'') ∈ rel S'"
proof -
define S where [simp]: "S ≡ alg_state_new P Q T"
have "(q, Nt B, q') ∉ rel S" and "(q', Nt C, q'') ∉ rel S"
by (simp add: alg_state_new_def)+
moreover have "((q', Nt C, q''), (q, Nt A, q'')) ∈ impl S (q, Nt B, q')"
using assms by (simp add: alg_state_new_def)
moreover have "alg_outer S = Some S'"
by (simp add: assms(1))
ultimately show ?thesis
using assms(3,4) by (elim pre_star_alg_impl_to_lts; force)
qed
lemma pre_star_alg_sup:
fixes P and T :: "('s, 'n, 't) trans" and q⇩0
defines "Q ≡ {q⇩0} ∪ states_lts T"
defines "S ≡ alg_state_new P Q T"
assumes "alg_outer S = Some S'"
and "pre_star_lts P Q T = Some T'"
and "CNF1 P"
shows "T' ⊆ rel S'"
proof -
have base: "T ⊆ rel S'" and "Q = {q⇩0} ∪ states_lts T"
proof
fix t
assume "t ∈ T"
then have "t ∈ trans S"
by (simp add: S_def alg_state_new_def)
then show "t ∈ rel S'"
using assms(3) pre_star_alg_trans_to_lts by blast
next
show "Q = {q⇩0} ∪ states_lts T"
by (simp add: Q_def)
qed
define b where "b ≡ (λT::('s, 'n, 't) trans. T ∪ pre_lts P Q T ≠ T)"
define c where "c ≡ (λT::('s, 'n, 't) trans. T ∪ pre_lts P Q T)"
have "⋀t T. Q = {q⇩0} ∪ states_lts T ⟹ T ⊆ rel S' ⟹ t ∈ pre_lts P Q T ⟹ t ∈ rel S'"
proof -
fix T and t
assume q_reach: "Q = {q⇩0} ∪ states_lts T" "T ⊆ rel S'" and t_src: "t ∈ pre_lts P Q T"
then obtain q q' A β where t_split: "t = (q, Nt A, q')" and "(A, β) ∈ P" and "q' ∈ steps_lts T β q"
unfolding pre_lts_def by blast
moreover have q_in: "q ∈ Q ∧ q' ∈ Q"
using t_src calculation steps_states_lts[of T] unfolding pre_lts_def q_reach(1)
using fst_conv by blast
ultimately consider "β = []" | "∃X. β = [X]" | "∃B C. β = [Nt B, Nt C]"
using assms(5)[unfolded CNF1_def] by fast
then have "(q, Nt A, q') ∈ rel S'" proof (cases)
case 1
then have "q = q'"
using ‹q' ∈ steps_lts T β q› by (simp add: Steps_lts_def)
moreover have "(A, []) ∈ P"
using ‹(A, β) ∈ P›[unfolded 1] by assumption
ultimately show ?thesis
using assms(2,3) q_in pre_star_alg_refl_to_lts by fast
next
case 2
then obtain X where β_split: "β = [X]"
by blast
then have "(q, X, q') ∈ rel S'"
using ‹q' ∈ steps_lts T β q› ‹T ⊆ rel S'› by (auto simp: Steps_lts_def Step_lts_def step_lts_def)
moreover have "(A, [X]) ∈ P"
using ‹(A, β) ∈ P›[unfolded β_split] by assumption
ultimately show ?thesis
using assms(2,3) q_in pre_star_alg_singleton_to_lts by fast
next
case 3
then obtain B C where β_split: "β = [Nt B, Nt C]"
by blast
then obtain q'' where "q' ∈ steps_lts T [Nt C] q''" and "q'' ∈ steps_lts T [Nt B] q"
using β_split ‹q' ∈ steps_lts T β q› Steps_lts_split by force
then have "(q, Nt B, q'') ∈ rel S'" and "(q'', Nt C, q') ∈ rel S'"
using ‹q' ∈ steps_lts T β q› ‹T ⊆ rel S'› by (auto simp: steps_lts_defs)
moreover have "(q, Nt B, q'') ∈ T"
using ‹q'' ∈ steps_lts T [Nt B] q› by (auto simp: steps_lts_defs)
moreover have "q'' ∈ Q"
using q_reach(1) steps_states_lts[of T Q q] q_in ‹q'' ∈ steps_lts T [Nt B] q› by blast
moreover have "(A, [Nt B, Nt C]) ∈ P"
using ‹(A, β) ∈ P›[unfolded β_split] by assumption
ultimately show ?thesis
using assms(2,3) q_in pre_star_alg_dual_to_lts by fast
qed
then show "t ∈ rel S'"
by (simp add: t_split)
qed
moreover have "⋀T. Q = {q⇩0} ∪ states_lts T ⟹ Q = {q⇩0} ∪ states_lts (T ∪ pre_lts P Q T)"
using states_pre_lts unfolding states_lts_Un
by (metis Un_assoc Un_upper2 sup.order_iff)
ultimately have step: "⋀T. (T ⊆ rel S' ∧ Q = {q⇩0} ∪ states_lts T) ⟹ T ∪ pre_lts P Q T ≠ T
⟹ (T ∪ pre_lts P Q T ⊆ rel S' ∧ Q = {q⇩0} ∪ states_lts (T ∪ pre_lts P Q T))"
by (smt (verit, del_insts) Un_iff subset_eq)
note base step
moreover note assms(4)[unfolded pre_star_lts_def] b_def c_def
ultimately have "T' ⊆ rel S' ∧ Q = {q⇩0} ∪ states_lts T'"
by (elim pre_star_lts_rule; use assms in simp)
then show "T' ⊆ rel S'"
by simp
qed
subsection‹Termination›
definition "alg_state_m_d S ≡ ({t. direct S t ≠ {}})"
definition "alg_state_m_i S ≡ ({t. impl S t ≠ {}})"
lemma alg_state_m_i_step_weak:
assumes "t ∈ trans S"
shows "alg_state_m_i (alg_outer_step S t) ⊆ alg_state_m_i S"
by (auto simp: alg_state_m_i_def)
lemma alg_state_m_i_step:
assumes "t ∈ trans S" and "impl S t ≠ {}"
shows "alg_state_m_i (alg_outer_step S t) ⊂ alg_state_m_i S"
using assms by (auto simp: alg_state_m_i_def)
lemma alg_state_m_d_step_weak:
assumes "t ∈ trans S" and "impl S t = {}"
shows "alg_state_m_d (alg_outer_step S t) ⊆ alg_state_m_d S"
using assms by (auto simp: alg_state_m_d_def)
lemma alg_state_m_d_step:
assumes "t ∈ trans S" and "impl S t = {}" and "direct S t ≠ {}"
shows "alg_state_m_d (alg_outer_step S t) ⊂ alg_state_m_d S"
using assms by (auto simp: alg_state_m_d_def)
lemma alg_state_m_trans_step:
assumes "t ∈ trans S" and "impl S t = {}" and "direct S t = {}"
shows "trans (alg_outer_step S t) ⊂ trans S"
using assms by auto
lemmas alg_state_m_intros = alg_state_m_i_step_weak alg_state_m_i_step
alg_state_m_d_step_weak alg_state_m_d_step alg_state_m_trans_step
definition "alg_state_comp ≡ lex_prod less_than (lex_prod less_than less_than)"
definition alg_state_measure :: "('s, 'n, 't) alg_state ⇒ (nat × nat × nat)" where
"alg_state_measure S ≡ (card (alg_state_m_i S), card (alg_state_m_d S), card (trans S))"
lemma wf_alg_state_comp: "wf (inv_image alg_state_comp alg_state_measure)"
unfolding alg_state_comp_def by (intro wf_inv_image) blast
definition alg_state_fin_inv :: "('s, 'n, 't) alg_state ⇒ bool" where
"alg_state_fin_inv S ≡ (
finite (rel S) ∧ finite (trans S) ∧
(∀t. finite (direct S t)) ∧ finite (alg_state_m_d S) ∧
(∀t. finite (impl S t)) ∧ finite (alg_state_m_i S)
)"
lemma alg_state_fin_inv_step:
assumes "alg_state_fin_inv S"
and "t ∈ trans S"
shows "alg_state_fin_inv (alg_outer_step S t)"
unfolding alg_state_fin_inv_def
proof (intro conjI)
show "finite (rel (alg_outer_step S t))"
by (simp add: assms[unfolded alg_state_fin_inv_def])
next
have "{t''. ∃t'. (t', t'') ∈ impl S t ∧ t' ∈ alg_outer_step_lts S t} ⊆ snd ` impl S t"
by force
moreover have "finite (snd ` impl S t)"
using assms[unfolded alg_state_fin_inv_def] by blast
ultimately have "finite {t''. ∃t'. (t', t'') ∈ impl S t ∧ t' ∈ alg_outer_step_lts S t}"
by (elim finite_subset)
then show "finite (trans (alg_outer_step S t))"
using assms[unfolded alg_state_fin_inv_def]
unfolding alg_outer_step_simps alg_outer_step_trans_eq by blast
next
have "⋀t'. {t''. (t', t'') ∈ impl S t ∧ t' ∉ alg_outer_step_lts S t} ⊆ snd ` impl S t"
by force
moreover have "finite (snd ` impl S t)"
using assms[unfolded alg_state_fin_inv_def] by blast
ultimately have "⋀t'. finite {t''. (t', t'') ∈ impl S t ∧ t' ∉ alg_outer_step_lts S t}"
using finite_subset by blast
moreover have "⋀t'. finite (((direct S)(t := {})) t')"
using assms[unfolded alg_state_fin_inv_def] by (auto simp: alg_state_m_d_def)
ultimately show "∀t'. finite (direct (alg_outer_step S t) t')"
unfolding alg_outer_step_simps alg_outer_step_direct_eq by blast
next
have "alg_state_m_d (alg_outer_step S t) ⊆ alg_state_m_d S ∪ fst ` impl S t"
unfolding alg_outer_step_simps alg_state_m_d_def by (auto, force)
moreover have "finite (alg_state_m_d S ∪ fst ` impl S t)"
using assms[unfolded alg_state_fin_inv_def] by blast
ultimately show "finite (alg_state_m_d (alg_outer_step S t))"
using finite_subset by blast
next
show "∀t'. finite (impl (alg_outer_step S t) t')"
by (simp add: assms[unfolded alg_state_fin_inv_def])
next
have "finite (alg_state_m_i S)"
by (simp add: assms(1)[unfolded alg_state_fin_inv_def])
moreover have "alg_state_m_i (alg_outer_step S t) ⊆ alg_state_m_i S"
using assms(2) by (rule alg_state_m_i_step_weak)
ultimately show "finite (alg_state_m_i (alg_outer_step S t))"
by (elim finite_subset)
qed
lemma alg_state_fin_inv_step':
assumes "alg_state_fin_inv s" and "trans s ≠ {}"
shows "alg_state_fin_inv (alg_outer_step s (SOME x. x ∈ trans s))"
using assms alg_state_fin_inv_step by (metis some_in_eq)
lemma wf_alg_outer_step:
defines "b ≡ (λS. trans S ≠ {})"
and "c ≡ (λS. alg_outer_step S (SOME x. x ∈ trans S))"
shows "wf {(t, s). (alg_state_fin_inv s ∧ b s) ∧ t = c s}"
proof -
have "⋀S t. t ∈ trans S ⟹ alg_state_fin_inv S ⟹ b S ⟹ (alg_outer_step S t, S) ∈ inv_image alg_state_comp alg_state_measure"
proof -
fix S and t
assume "t ∈ trans S" and inv: "alg_state_fin_inv S" and "b S"
obtain n1 n2 n3 where n_def: "alg_state_measure S = (n1, n2, n3)"
using prod_cases3 by blast
then have n1_def: "n1 = card (alg_state_m_i S) ∧ finite (alg_state_m_i S)"
and n2_def: "n2 = card (alg_state_m_d S) ∧ finite (alg_state_m_d S)"
and n3_def: "n3 = card (trans S) ∧ finite (trans S)"
using inv by (simp add: alg_state_measure_def alg_state_fin_inv_def)+
define S' where "S' ≡ alg_outer_step S t"
obtain m1 m2 m3 where m_def: "alg_state_measure S' = (m1, m2, m3)"
using prod_cases3 by blast
moreover have "alg_state_fin_inv S'"
using inv ‹t ∈ trans S› alg_state_fin_inv_step unfolding S'_def b_def by blast
ultimately have m1_def: "m1 = card (alg_state_m_i S') ∧ finite (alg_state_m_i S')"
and m2_def: "m2 = card (alg_state_m_d S') ∧ finite (alg_state_m_d S')"
and m3_def: "m3 = card (trans S') ∧ finite (trans S')"
by (simp add: S'_def alg_state_measure_def alg_state_fin_inv_def)+
consider (red1) "impl S t ≠ {}"
| (red2) "impl S t = {} ∧ direct S t ≠ {}"
| (red3) "impl S t = {} ∧ direct S t = {}"
by blast
then have "((m1, m2, m3), (n1, n2, n3)) ∈ alg_state_comp"
proof (cases)
case red1
with ‹t ∈ trans S› have "alg_state_m_i S' ⊂ alg_state_m_i S"
by (simp add: alg_state_m_intros[where t=t and S=S] S'_def)+
then have "m1 < n1"
using m1_def n1_def by (simp add: psubset_card_mono)
then show ?thesis
by (simp add: alg_state_comp_def)
next
case red2
with ‹t ∈ trans S› have "alg_state_m_i S' ⊆ alg_state_m_i S"
and "alg_state_m_d S' ⊂ alg_state_m_d S"
by (simp add: alg_state_m_intros[where t=t and S=S] S'_def)+
then have "m1 ≤ n1" and "m2 < n2"
using m1_def m2_def n1_def n2_def
by (simp add: psubset_card_mono card_mono)+
then show ?thesis
by (auto simp: alg_state_comp_def)
next
case red3
then have "alg_state_m_i S' ⊆ alg_state_m_i S"
and "alg_state_m_d S' ⊆ alg_state_m_d S"
and "trans S' ⊂ trans S"
using ‹t ∈ trans S› alg_state_m_intros[where t=t and S=S] by (simp add: S'_def)+
then have "m1 ≤ n1" and "m2 ≤ n2" and "m3 < n3"
using m1_def m2_def m3_def n1_def n2_def n3_def
by (simp add: psubset_card_mono card_mono)+
then show ?thesis
by (auto simp: alg_state_comp_def)
qed
then show "(alg_outer_step S t, S) ∈ inv_image alg_state_comp alg_state_measure"
using m_def n_def by (simp add: S'_def)
qed
then have "{(t, s). (alg_state_fin_inv s ∧ b s) ∧ t = c s} ⊆ inv_image alg_state_comp alg_state_measure"
unfolding c_def b_def
by (smt (verit, ccfv_SIG) all_not_in_conv mem_Collect_eq old.prod.case some_eq_imp subrelI)
with wf_alg_state_comp show ?thesis
by (rule wf_subset)
qed
lemma alg_outer_terminates:
assumes "alg_state_fin_inv S"
shows "∃S'. alg_outer S = Some S'"
unfolding alg_outer_def
by (intro wf_while_option_Some; use wf_alg_outer_step alg_state_fin_inv_step' assms in fast)
lemma alg_state_new_fin_inv:
fixes T :: "('s, 'n, 't) trans"
assumes "finite P" and "finite Q" and "finite T"
shows "alg_state_fin_inv (alg_state_new P Q T)"
unfolding alg_state_fin_inv_def
proof (intro conjI)
show "finite (rel (alg_state_new P Q T))"
by (simp add: alg_state_new_def)
next
note assms(3)
moreover have "finite {(q, Nt A, q) |q A. (A, []) ∈ P ∧ q ∈ Q}"
by (rule finite_subset[where B="Q × (Nt ` fst ` P) × Q"]; use assms in force)
moreover have "finite {(q, Nt A, q') |q q' A. ∃a. (A, [Tm a]) ∈ P ∧ (q, Tm a, q') ∈ T ∧ q ∈ Q ∧ q' ∈ Q}"
by (rule finite_subset[where B="Q × (Nt ` fst ` P) × Q"]; use assms in force)
ultimately show "finite (trans (alg_state_new P Q T))"
by (simp add: alg_state_new_def)
next
have "⋀q q' B. finite {(q, Nt A, q') |A. (A, [Nt B]) ∈ P ∧ q ∈ Q ∧ q' ∈ Q}"
by (rule finite_subset[where B="Q × (Nt ` fst ` P) × Q"]; use assms in force)
then show "∀t. finite (direct (alg_state_new P Q T) t)"
unfolding alg_state_new_def by (auto split: sym.split)
next
have "alg_state_m_d (alg_state_new P Q T) ⊆ Q × hd ` snd ` P × Q"
unfolding alg_state_new_def alg_state_m_d_def by (auto split: sym.splits) force
moreover have "finite (hd ` snd ` P )"
using assms(1) by simp
ultimately show "finite (alg_state_m_d (alg_state_new P Q T))"
using assms(2) finite_subset by blast
next
have "⋀t. impl (alg_state_new P Q T) t ⊆ (Q × hd ` tl ` snd ` P × Q) × (Q × Nt ` fst ` P × Q)"
unfolding alg_state_new_def by (auto split: sym.splits) force+
moreover have "finite ((Q × hd ` tl ` snd ` P × Q) × (Q × Nt ` fst ` P × Q))"
using assms(1,2) by simp
ultimately show "∀t. finite (impl (alg_state_new P Q T) t)"
using finite_subset by blast
next
have "alg_state_m_i (alg_state_new P Q T) ⊆ Q × hd ` snd ` P × Q"
unfolding alg_state_new_def alg_state_m_i_def by (auto split: sym.splits) force
moreover have "finite (hd ` snd ` P )"
using assms(1) by simp
ultimately show "finite (alg_state_m_i (alg_state_new P Q T))"
using assms(2) finite_subset by blast
qed
subsection‹Final Algorithm›
definition pre_star_code_cnf :: "('n, 't) Prods ⇒ ('s, ('n, 't) sym) auto ⇒ ('s, ('n, 't) sym) auto" where
"pre_star_code_cnf P M ≡ (
let Q = {auto.start M} ∪ states_lts (auto.lts M) in
let S = alg_state_new P Q (auto.lts M) in
case alg_outer S of
Some S' ⇒ M ⦇ auto.lts := (rel S') ⦈
)"
lemma pre_star_code_cnf_correct:
assumes "finite P" and "finite (auto.lts M)" and cnf: "CNF1 P"
shows "Lang_auto (pre_star_code_cnf P M) = pre_star P (Lang_auto M)"
proof -
define Q where "Q ≡ {auto.start M} ∪ states_lts (auto.lts M)"
have "finite Q"
using assms(2) by (auto simp add: states_lts_def Q_def)
define S where "S ≡ alg_state_new P Q (auto.lts M)"
have "alg_state_fin_inv S"
using alg_state_new_fin_inv assms(1,2) ‹finite Q› by (simp add: S_def)
then obtain S' where S'_def: "alg_outer S = Some S'"
using alg_outer_terminates by blast
obtain T' where T'_def: "pre_star_lts P Q (auto.lts M) = Some T'"
using pre_star_lts_terminates assms(1,2) ‹finite Q›
by (metis Q_def sup_ge2)
moreover have "rel S' ⊆ T'"
using S'_def T'_def pre_star_alg_sub unfolding S_def by blast
moreover have "T' ⊆ rel S'"
using S'_def T'_def cnf pre_star_alg_sup unfolding S_def Q_def by fast
ultimately have "rel S' = T'"
by simp
have "pre_star_auto P M = pre_star_code_cnf P M"
unfolding pre_star_auto_def pre_star_code_cnf_def
using T'_def S'_def ‹rel S' = T'› unfolding S_def Q_def by simp
then show ?thesis
using pre_star_auto_correct assms(1,2) by metis
qed
end