theory Matchbounds_Impl
imports
TA.Tree_Automata_Impl
Raise_Consistency
QTRS.Trs_Impl
TA.Signature_Extension
QTRS.QDP_Framework_Impl
"../Auxiliaries/Multiset_Code"
QTRS.Map_Choice
begin
no_notation fun_rel_syn (infixr "→" 60)
lemma [code]:
"Matchbounds.roof (l, r) = (
let xs = vars_term_list r in (λt.
let xt = vars_term t in
(∀x∈set xs. x ∈ xt)))"
unfolding Let_def roof.simps by (rule ext, simp) blast
definition ta_bounded :: "('q, 'f × nat) ta ⇒ nat ⇒ bool" where
"ta_bounded TA c ≡ ∀ f n. (f,n) ∈ ta_syms TA ⟶ height f ≤ c"
context
fixes R :: "('f × nat, 'v) trs"
and TA :: "('q, 'f × nat) ta"
and L :: "('f, 'v) terms"
and rel :: "'q rel"
and c :: nat
assumes choice: "left_linear_trs R ∨ ta_det TA ∧ state_raise_consistent TA rel"
and fin: "finite (ta_rules TA)"
and compat: "state_compatible TA rel R"
and coh: "state_coherent TA rel"
and incl: "(lift_term 0) ` L ⊆ ta_lang TA"
and tab: "ta_bounded TA c"
begin
lemma raise_step_boundedI: assumes var_cond: "⋀ l r. (l,r) ∈ R ⟹ vars_term r ⊆ vars_term l"
shows "raise_step_bounded c R L"
proof -
let ?ta_lang = "ta_lang :: ('q, 'f × nat) ta ⇒ ('f × nat, 'v) term set"
let ?choice = "left_linear_trs R"
def step ≡ "if ?choice then rstep R else raise_step R"
def G ≡ "⋃(funas_term ` ?ta_lang TA)"
from ta_syms_lang[of _ TA] have sub: "⋃(funas_term ` (ta_lang TA)) ⊆ ta_syms TA" by auto
from finite_subset[OF this finite_ta_syms[OF fin]] have fin: "finite G" unfolding G_def .
note raise = state_raise_compatible[OF _ coh _ compat var_cond subset_refl]
note ll = state_compatible[OF compat coh disjI1 var_cond subset_refl]
have G: "⋃(funas_term ` {t. ∃ s . s ∈ lift_term 0 ` L ∧ (s,t) ∈ step^*}) ⊆ G"
using choice incl raise ll unfolding G_def step_def
by (cases ?choice, force+)
from finite_list[OF fin] obtain Gl where fin: "G = set Gl" by auto
let ?h = "(λ(f,n). height f)"
{
fix s t f n
assume "s ∈ lift_term 0 ` L" "(s,t) ∈ step^*" "(f,n) ∈ funas_term t"
hence "(f,n) ∈ funas_term t" and "funas_term t ⊆ G" using G unfolding fin by auto
from this sub have "(f,n) ∈ ta_syms TA" unfolding G_def by auto
with tab[unfolded ta_bounded_def]
have "height f ≤ c" by blast
} note bound = this
show "raise_step_bounded c R L"
proof (cases ?choice)
case False
with bound show ?thesis
unfolding bounded_defs step_def by auto
next
case True
with bound show ?thesis
by (intro rstep_bounded_left_linear_imp_raise_bounded[OF _ True],
unfold bounded_defs step_def, auto)
qed
qed
lemma e_bounds:
assumes SN: "locally_terminating (cover e Strict_TRS RR ∪ Matchbounds.raise)"
and F: "finite F"
and RR: "finite RR"
and R: "R = cover e Strict_TRS RR"
and var_cond: "⋀ l r. (l,r) ∈ RR ⟹ vars_term r ⊆ vars_term l"
and L: "⋃(funas_term ` L) ⊆ F"
shows "SN_on (rstep RR) L"
proof -
from raise_step_boundedI[unfolded R, OF cover_var_condition[OF var_cond]]
have "e_raise_bounded e c RR L" unfolding e_raise_bounded_def .
from e_raise_bounded[OF var_cond SN RR F L this]
show "SN_on (rstep RR) L" .
qed
end
definition cover_bound where
"cover_bound c e ee R ≡ {(l,r). (l,r) ∈ cover e ee R ∧ (∀ f n. (f,n) ∈ funas_term l ⟶ height f ≤ c)}"
lemma ta_contains_ground_terms_of: assumes "ta_contains F H TA qfin"
shows "ground_terms_of F H ⊆ ta_lang TA"
using ta_contains_both[OF assms] unfolding ground_terms_of_def by auto
context
fixes TA :: "('q,'f × nat)ta"
and qfin :: "'q set"
and c :: nat
and G H :: "'f sig"
and rel :: "'q rel"
assumes fin: "finite (ta_rules TA)"
and coh: "state_coherent TA rel"
and finG: "finite G" and finH: "finite H"
and contain: "ta_contains ((λ(f,n). (lift 0 f,n)) ` G) ((λ(f,n). (lift 0 f,n)) ` H) TA qfin"
and qfin_final: "qfin ⊆ ta_final TA"
and qfin: "∃ q ∈ qfin. q ∈ ta_rhs_states TA"
and tab: "ta_bounded TA c"
and inf: "infinite (UNIV :: 'f set)"
begin
lemma create_constant_in_ta_generic: fixes R :: "('f,'v)rules"
assumes
choice: "left_linear_trs (set R) ∨ ta_det TA ∧ state_raise_consistent TA rel"
shows "∃ q const F F' TA'. G ∪ {(const,0)} = F ∧ H ∪ {(const,0)} = F' ∧
(∀ e ee S. S ⊆ set R ⟶ state_compatible TA rel (cover_bound c e ee S) ⟶
state_compatible TA' rel (cover e ee S))
∧ lift_term 0 ` ground_terms_of F F' ⊆ (ta_lang TA' :: ('f × nat,'v)terms)
∧ state_coherent TA' rel
∧ (left_linear_trs (set R) ∨ ta_det TA' ∧ state_raise_consistent TA' rel)
∧ ta_bounded TA' c
∧ TA' = ⦇ ta_final = (ta_final TA), ta_rules = insert ((const,0) [] → q) (ta_rules TA), ta_eps = ta_eps TA ⦈"
proof -
let ?lz = "(λ(f,n). (lift 0 f,n))"
from qfin obtain q where q: "q ∈ qfin ∧ q ∈ ta_rhs_states TA" by auto
def FF ≡ "(fst ` r_sym ` ta_rules TA ∪ funas_trs (set R))"
from finite_set[of "funas_trs_list R"] have finR: "finite (funas_trs (set R))" by simp
from finite_list[OF finG] obtain G' where G': "set G' = G" by auto
from finite_list[OF finH] obtain H' where H': "set H' = H" by auto
have "finite (fst ` r_sym ` ta_rules TA)" using fin by auto
hence "finite (fst ` FF)" using finG finH finR FF_def by auto
from ex_new_if_finite[OF inf this] obtain const where nconst: "const ∉ (fst ` FF)" by auto
hence "(const,0) ∉ FF" by force
hence constR: "(const,0) ∉ funas_trs (set R)" unfolding FF_def by auto
let ?TA = "⦇ ta_final = (ta_final TA), ta_rules = insert ((const,0) [] → q) (ta_rules TA), ta_eps = ta_eps TA ⦈"
obtain TA' where TA': "TA' = ?TA" by auto
let ?F = "(const,0) # G'"
let ?F' = "(const,0) # H'"
obtain F where F: "F = ?F" by simp
obtain F' where F': "F' = ?F'" by simp
have const: "(const,0) ∈ set F" by (simp add: F)
have main: "(∀ e ee S. S ⊆ set R ⟶ state_compatible TA rel (cover_bound c e ee S) ⟶
state_compatible TA' rel (cover e ee S))
∧ ta_contains (?lz ` set F) (?lz ` set F') TA' qfin
∧ state_coherent TA' rel
∧ ta_bounded TA' c
∧ (left_linear_trs (set R) ∨ ta_det TA' ∧ state_raise_consistent TA' rel)
" (is "?comp ∧ ?cont ∧ ?coh ∧ ?tab ∧ ?choice")
proof -
note coh = coh[unfolded state_coherent_def]
from TA' coh have coh1: "rel `` ta_final TA' ⊆ ta_final TA'" by auto
have ?choice
proof (cases "left_linear_trs (set R)")
case False
with choice have det: "ta_det TA" and raise: "state_raise_consistent TA rel" by auto
{
fix qs q' h
assume "((const,h) qs → q') ∈ ta_rules TA"
hence "((const,h),length qs) ∈ r_sym ` ta_rules TA" by force
hence "⋀ f. f (((const,h),length qs)) ∈ f ` (r_sym ` ta_rules TA)" by auto
from this[of "fst o fst"] have "const ∈ fst ` FF" unfolding FF_def by auto
with nconst have False by auto
} note no_const = this
from raise have raise: "state_raise_consistent TA' rel" using no_const unfolding TA'
state_raise_consistent_def by auto blast
from det no_const have det: "ta_det TA'" unfolding ta_det_def TA' by auto
from raise det show ?thesis by auto
qed auto
have ?coh unfolding state_coherent_def
proof (rule conjI, rule conjI[OF coh1], intro allI impI)
fix f qs q i qi
assume rule: "(f qs → q) ∈ ta_rules TA'" and ass: "i < length qs" "(qs ! i, qi) ∈ rel"
from rule[unfolded TA'] ass have "(f qs → q) ∈ ta_rules TA" by auto
from coh[THEN conjunct1, THEN conjunct2, rule_format, OF this ass]
show "∃q'. (f qs[i := qi] → q') ∈ ta_rules TA' ∧ (q, q') ∈ rel" unfolding TA' by auto
next
show "rel¯ O ta_eps TA' ⊆ (ta_eps TA')⇧* O rel¯" using coh TA' by auto
qed
note d = ta_contains_def
{
fix G H Q
assume contain: "ta_contains_aux (?lz ` G) qfin TA Q" and H: "H = insert (const,0) G" and Q: "qfin ⊆ Q"
note d = ta_contains_aux_def
{
fix f n
assume fn: "(f,n) ∈ ?lz ` H"
hence "∀ qs'. length qs' = n ∧ set qs' ⊆ qfin ⟶ (∃ q q'. (f qs' → q) ∈ ta_rules ?TA ∧ q' ∈ Q ∧ (q,q') ∈ (ta_eps ?TA)^* )"
proof (cases "(f,n) = ((const,0),0)")
case True
thus ?thesis using q Q by auto
next
case False
with fn have fn: "(f,n) ∈ ?lz ` G" unfolding H by auto
hence fn: "(f,n) ∈ ?lz ` G" by auto
then obtain g where f: "f = (g,0)" and g: "(g,n) ∈ G" by auto
show ?thesis
proof (intro allI impI)
fix qs'
assume len: "length qs' = n ∧ set qs' ⊆ qfin"
from contain[unfolded d, simplified, rule_format, of g 0 qs'] g len
obtain q q' where "(g, 0) qs' → q ∈ ta_rules TA ∧ q' ∈ Q ∧ (q, q') ∈ (ta_eps TA)⇧*" by force
thus "∃ q q'. (f qs' → q) ∈ ta_rules ?TA ∧ q' ∈ Q ∧ (q,q') ∈ (ta_eps ?TA)^*"
unfolding f by auto
qed
qed
}
hence "ta_contains_aux (?lz ` H) qfin ?TA Q" unfolding d ta.simps by blast
} note convert = this
from contain[unfolded d]
have aux: "ta_contains_aux (?lz ` G) qfin TA qfin"
"ta_contains_aux (?lz ` H) qfin TA (ta_final TA)" by auto
have fin: "ta_final ?TA = ta_final TA" by simp
have "ta_contains_aux (?lz ` set F) qfin ?TA qfin"
by (rule convert[OF aux(1)], insert G' F, auto)
moreover have "ta_contains_aux (?lz ` set F') qfin ?TA (ta_final ?TA)" unfolding fin
by (rule convert[OF aux(2)], insert qfin_final H' F', auto)
ultimately have cont: "ta_contains (?lz ` set F) (?lz ` set F') ?TA qfin" unfolding d
unfolding ta_contains_def by auto
have ?tab using tab unfolding TA' ta_bounded_def by (auto simp: ta_syms_def)
have ?comp
proof (intro allI impI)
fix e ee S
assume SR: "S ⊆ set R" and compat: "state_compatible TA rel (cover_bound c e ee S)"
have "state_compatible ?TA rel (cover e ee S)"
unfolding state_compatible_def
proof (clarify)
fix l r
assume lr: "(l,r) ∈ cover e ee S"
and lsyms: "funas_term l ⊆ ta_syms ?TA"
from tab[unfolded ta_bounded_def, rule_format] have c: "⋀ f n. (f,n) ∈ ta_syms TA' ⟹ height f ≤ c" unfolding TA'
by (auto simp: ta_syms_def)
from c lsyms lr have lr: "(l,r) ∈ cover_bound c e ee S" unfolding cover_bound_def TA'[symmetric]
by blast
from lsyms have lsyms: "funas_term l ⊆ insert ((const,0),0) (ta_syms TA)" unfolding ta_syms_def by auto
from lr obtain ll rr where llrr:"(ll,rr) ∈ S" and base:"ll = base_term l"
unfolding cover_bound_def cover_def by auto
{
assume "((const,0),0) ∈ funas_term l"
hence "base ((const,0),0) ∈ funas_term ll" unfolding base
unfolding funas_term_map_funs_term by force
hence "(const,0) ∈ funas_term ll" by auto
with set_mp[OF SR llrr] constR have False unfolding funas_trs_def funas_rule_def [abs_def] by auto
} hence const_new: "((const,0),0) ∉ funas_term l" ..
with lsyms have lsyms: "funas_term l ⊆ ta_syms TA" by auto
from compat[unfolded state_compatible_def] lr lsyms have
compat: "rule_state_compatible TA rel (l,r)" by auto
{
fix q'
assume q': "(q,q') ∈ (ta_eps TA)^*"
from q[unfolded ta_rhs_states_def] obtain q'' rule where
q: "(q'',q) ∈ (ta_eps TA)^*" and rule: "rule ∈ ta_rules TA" and sym: "r_rhs rule = q''" by auto
from q' q have q': "(q'',q') ∈ (ta_eps TA)^*" by auto
with rule sym
have "q' ∈ ta_rhs_states TA" unfolding ta_rhs_states_def by blast
}
hence ta_rhs_states: "ta_rhs_states ?TA = ta_rhs_states TA" unfolding ta_rhs_states_def by auto
show "rule_state_compatible ?TA rel (l,r)"
unfolding rule_state_compatible_def ta_rhs_states
proof (rule, intro allI impI)
fix τ
assume τ: "τ ` vars_term l ⊆ ta_rhs_states TA"
obtain rr where rr: "map_vars_term τ r = rr" by auto
show "ta_res ?TA (map_vars_term τ l) ⊆ rel^-1 `` ta_res ?TA (map_vars_term τ r)"
proof
fix q'
assume "q' ∈ ta_res ?TA (map_vars_term τ l)"
hence "q' ∈ ta_res TA (map_vars_term τ l)" using const_new
proof (induct l arbitrary: q')
case (Var x) thus ?case by auto
next
case (Fun f ls)
from Fun(3) have f: "(f,length ls) ≠ ((const,0),0)" by auto
from Fun(2)[unfolded term.map ta_res.simps]
obtain q2 qs where rule: "(f qs → q2) ∈ ta_rules ?TA" and len: "length qs = length (map (map_vars_term τ) ls)"
and ind: "∀i < length ls. qs ! i ∈ map (ta_res ?TA) (map (map_vars_term τ) ls) ! i"
and q2: "(q2,q') ∈ (ta_eps TA)^*" by auto
from rule len f have rule: "(f qs → q2) ∈ ta_rules TA" by auto
show ?case
proof (unfold term.map ta_res.simps, rule, intro exI conjI, rule HOL.refl, rule rule, rule q2,
rule len, intro allI impI)
fix i
assume i: "i < length (map (map_vars_term τ) ls)"
hence i': "i < length ls" by auto
from i' have mem: "ls ! i ∈ set ls" by auto
with Fun(3) have nmem: "((const,0),0) ∉ funas_term (ls ! i)" by auto
show "qs ! i ∈ map (ta_res TA) (map (map_vars_term τ) ls) ! i"
unfolding nth_map[OF i] nth_map[OF i']
by (rule Fun(1)[OF mem _ nmem], insert ind i', auto)
qed
qed
with compat[unfolded rule_state_compatible_def] τ
have "q' ∈ rel^-1 `` ta_res TA (map_vars_term τ r)" by auto
then obtain q'' where rel: "(q',q'') ∈ rel" and q'': "q'' ∈ ta_res TA (map_vars_term τ r)" by auto
from q'' have "q'' ∈ ta_res ?TA (map_vars_term τ r)" unfolding rr
proof (induct rr arbitrary: q'')
case (Var q) thus ?case by auto
next
case (Fun f ts q')
from Fun(2) obtain q2 qs where rule: "(f qs → q2) ∈ ta_rules ?TA"
and len: "length qs = length ts"
and rec: "⋀i. i < length ts ⟹ qs ! i ∈ ta_res TA (ts ! i)"
and q: "(q2,q') ∈ (ta_eps TA)^*"
by auto
{
fix i
assume i: "i < length ts"
hence "ts ! i ∈ set ts" by auto
from Fun(1)[OF this rec[OF i]]
have "qs ! i ∈ ta_res ?TA (ts ! i)" by auto
}
with rule len q show ?case by auto
qed
with rel
show "q' ∈ rel^-1 `` ta_res ?TA (map_vars_term τ r)" by auto
qed
qed
qed
thus "state_compatible TA' rel (cover e ee S)" unfolding TA' .
qed
thus ?thesis using contain ‹?coh› ‹?choice› ‹?tab› cont unfolding TA' by auto
qed
hence ?comp and ?cont by auto
have lift: "lift_term 0 ` ground_terms_of (set F) (set F') ⊆ (ta_lang TA' :: ('f × nat,'v)term set)" (is "?L ⊆ _ ")
proof (rule subset_trans[OF _ ta_contains_both[OF ‹?cont›]], rule, clarify)
fix s
assume s: "s ∈ ground_terms_of (set F) (set F')"
let ?F = "?lz ` set F"
let ?ls = "lift_term 0 s"
from s[unfolded ground_terms_of_def, simplified]
have F: "(⋃x∈set (args s). funas_term x) ⊆ set F"
and root: "the (root s) ∈ set F'" and gs: "ground s" by auto
from gs obtain g ts where s: "s = Fun g ts" by (cases s, auto)
from F s have F: "(⋃x∈set ts. funas_term x) ⊆ set F" by auto
from root s have root: "(g,length ts) ∈ set F'" by auto
let ?ts = "map (lift_term 0) ts"
from s have ls: "?ls = Fun (g, 0) ?ts" by simp
from ls root have root: "the (root ?ls) ∈ ?lz ` set F'" by auto
{
fix lt
assume "lt ∈ set (args ?ls)"
then obtain t where lt: "lt = lift_term 0 t" and t: "t ∈ set ts" unfolding s by auto
from t F gs s have "funas_term t ⊆ set F" "ground t" by auto
hence "ground lt ∧ funas_term lt ⊆ ?F" unfolding lt
proof (induct t)
case (Fun f ss)
{
fix s
assume s: "s ∈ set ss"
from Fun(3) s have g: "ground s" by auto
from Fun(2) s have wf: "funas_term s ⊆ set F" by auto
from Fun(1)[OF s wf g] have "ground (lift_term 0 s)" "funas_term (lift_term 0 s) ⊆ ?F"
by force+
} note ind = this
from Fun(2) have f: "((f,0), length ss) ∈ ?F" by auto
from ind f
show ?case by force
qed simp
}
with root
show "⋃(funas_term ` set (args ?ls)) ⊆ ?F ∧
the (root ?ls) ∈ ?lz ` set F' ∧
ground ?ls" unfolding s by auto
qed
show ?thesis
by (rule exI[of _ q], rule exI[of _ const], rule exI[of _ "set F"], rule exI[of _ "set F'"], rule exI[of _ TA'],
insert ‹?comp› ‹?cont› lift main, auto simp: F finG G' TA' F' H')
qed
lemma create_constant_in_ta: fixes R :: "('f,'v)rules"
assumes
choice: "left_linear_trs (set R) ∨ ta_det TA ∧ state_raise_consistent TA rel"
and compat: "state_compatible TA rel (cover_bound c e ee (set R))" (is "state_compatible _ _ ?R")
shows "∃ q const F F' TA'. G ∪ {(const,0)} = F ∧ H ∪ {(const,0)} = F'
∧ state_compatible TA' rel (cover e ee (set R))
∧ lift_term 0 ` ground_terms_of F F' ⊆ (ta_lang TA' :: ('f × nat,'v)terms)
∧ state_coherent TA' rel
∧ (left_linear_trs (set R) ∨ ta_det TA' ∧ state_raise_consistent TA' rel)
∧ ta_bounded TA' c
∧ TA' = ⦇ ta_final = (ta_final TA), ta_rules = insert ((const,0) [] → q) (ta_rules TA), ta_eps = ta_eps TA ⦈"
proof -
let ?Q = "λ TA'. ∀ e ee S. S ⊆ set R ⟶ state_compatible TA rel (cover_bound c e ee S) ⟶
state_compatible TA' rel (cover e ee S)"
def P ≡ "λ q const F F' TA'. G ∪ {(const,0)} = F ∧ H ∪ {(const,0)} = F' ∧
?Q TA'
∧ lift_term 0 ` ground_terms_of F F' ⊆ (ta_lang TA' :: ('f × nat,'v)terms)
∧ state_coherent TA' rel
∧ (left_linear_trs (set R) ∨ ta_det TA' ∧ state_raise_consistent TA' rel)
∧ ta_bounded TA' c
∧ TA' = ⦇ ta_final = (ta_final TA), ta_rules = insert ((const,0) [] → q) (ta_rules TA), ta_eps = ta_eps TA ⦈"
from create_constant_in_ta_generic[OF choice]
have "∃ q const F F' TA'. P q const F F' TA'" unfolding P_def .
then obtain q const F F' TA' where main: "P q const F F' TA'" by blast
hence Q: "?Q TA'" unfolding P_def by blast
note * = Q[rule_format, OF _ compat] main[unfolded P_def]
show ?thesis
by (rule exI[of _ q], rule exI[of _ const], rule exI[of _ F], rule exI[of _ F'], rule exI[of _ TA'],
insert *, auto)
qed
lemma create_constant_in_ta_two: fixes R1 R2 :: "('f,'v)rules"
assumes
choice: "left_linear_trs (set (R1 @ R2)) ∨ ta_det TA ∧ state_raise_consistent TA rel"
and compat1: "state_compatible TA rel (cover_bound c e1 ee1 (set R1))" (is "state_compatible _ _ ?R1")
and compat2: "state_compatible TA rel (cover_bound c e2 ee2 (set R2))" (is "state_compatible _ _ ?R2")
shows "∃ q const F F' TA'. G ∪ {(const,0)} = F ∧ H ∪ {(const,0)} = F'
∧ state_compatible TA' rel (cover e1 ee1 (set R1))
∧ state_compatible TA' rel (cover e2 ee2 (set R2))
∧ lift_term 0 ` ground_terms_of F F' ⊆ (ta_lang TA' :: ('f × nat,'v)terms)
∧ state_coherent TA' rel
∧ (left_linear_trs (set R1 ∪ set R2) ∨ ta_det TA' ∧ state_raise_consistent TA' rel)
∧ ta_bounded TA' c
∧ TA' = ⦇ ta_final = (ta_final TA), ta_rules = insert ((const,0) [] → q) (ta_rules TA), ta_eps = ta_eps TA ⦈"
proof -
let ?Q = "λ TA'. ∀ e ee S. S ⊆ set (R1 @ R2) ⟶ state_compatible TA rel (cover_bound c e ee S) ⟶
state_compatible TA' rel (cover e ee S)"
def P ≡ "λ q const F F' TA'. G ∪ {(const,0)} = F ∧ H ∪ {(const,0)} = F' ∧
?Q TA'
∧ lift_term 0 ` ground_terms_of F F' ⊆ (ta_lang TA' :: ('f × nat,'v)terms)
∧ state_coherent TA' rel
∧ (left_linear_trs (set (R1 @ R2)) ∨ ta_det TA' ∧ state_raise_consistent TA' rel)
∧ ta_bounded TA' c
∧ TA' = ⦇ ta_final = (ta_final TA), ta_rules = insert ((const,0) [] → q) (ta_rules TA), ta_eps = ta_eps TA ⦈"
from create_constant_in_ta_generic[OF choice]
have "∃ q const F F' TA'. P q const F F' TA'" unfolding P_def .
then obtain q const F F' TA' where main: "P q const F F' TA'" by blast
hence "?Q TA'" unfolding P_def by blast
note * = this[rule_format, OF _ compat1]
this[rule_format, OF _ compat2]
main[unfolded P_def]
show ?thesis
by (rule exI[of _ q], rule exI[of _ const], rule exI[of _ F], rule exI[of _ F'], rule exI[of _ TA'],
insert *, auto)
qed
end
lemma funas_term_ground_terms_of: "⋃(funas_term ` ground_terms_of F F') ⊆ F ∪ F'"
proof -
{
fix t
assume "t ∈ ground_terms_of F F'"
note * = this[unfolded ground_terms_of_def]
from * obtain f ts where t: "t = Fun f ts" by (cases t, auto)
with * have "funas_term t ⊆ F ∪ F'" by auto
}
thus ?thesis by auto
qed
locale bounds_impl =
fixes R S :: "('f,'v)rules" and TA and rel :: "'q rel" and e and c and c_opt and G H :: "'f sig" and qfin
assumes
choice: "left_linear_trs (set (R @ S)) ∨ ta_det TA ∧ state_raise_consistent TA rel"
and fin: "finite (ta_rules TA)"
and compat: "state_compatible TA rel (cover_bound c e Strict_TRS (set R))"
and compat2: "state_compatible TA rel (cover_bound c Matchbounds.match (Weak_TRS c_opt) (set S))"
and coh: "state_coherent TA rel"
and tab: "ta_bounded TA c"
and qfin: "∃ q ∈ qfin. q ∈ ta_rhs_states TA"
and qfin_final: "qfin ⊆ ta_final TA"
and inf: "infinite (UNIV :: 'f set)"
and finG: "finite G"
and finH: "finite H"
and contain: "ta_contains ((λ(f,n). (lift 0 f,n)) ` G) ((λ(f,n). (lift 0 f,n)) ` H) TA qfin"
and wf: "wf_trs (set R ∪ set S)"
begin
lemma match_bounds_linear_impl:
assumes match: "e = Matchbounds.match"
and non_duplicating: "⋀ l r. (l,r) ∈ set R ⟹ vars_term_ms r ⊆# vars_term_ms l"
and rcm: "set (roots_of_cm cm) ⊆ H"
and scm: "set (stackable_of_cm cm) ⊆ G"
shows "deriv_bound_measure_class (rstep (set R)) cm (Comp_Poly 1)"
proof -
let ?match = Matchbounds.match
from wf[unfolded wf_trs_def] have varcond: "⋀ l r. (l,r) ∈ set R ⟹ vars_term r ⊆ vars_term l" by auto
from create_constant_in_ta_two[OF fin coh finG finH contain qfin_final qfin tab inf choice compat compat2,
unfolded match]
obtain q const F F' TA' where "G ∪ {(const,0)} = F ∧ H ∪ {(const,0)} = F'
∧ state_compatible TA' rel (cover ?match Strict_TRS (set R))
∧ state_compatible TA' rel (cover ?match (Weak_TRS c_opt) (set S))
∧ lift_term 0 ` ground_terms_of F F' ⊆ (ta_lang TA' :: ('f × nat, 'v) terms)
∧ state_coherent TA' rel
∧ (left_linear_trs (set R ∪ set S) ∨ ta_det TA' ∧ state_raise_consistent TA' rel)
∧ ta_bounded TA' c
∧ TA' = ⦇ ta_final = (ta_final TA), ta_rules = insert ((const,0) [] → q) (ta_rules TA), ta_eps = ta_eps TA ⦈
" (is "?GF ∧ ?HF ∧ ?comp ∧ _ ∧ ?cont ∧ ?coh ∧ ?choice ∧ ?tab ∧ ?TA") by metis
hence compat: ?comp and contain: ?cont and ?coh ?choice ?HF ?GF ?TA ?tab by auto
let ?R = "cover Matchbounds.match Strict_TRS (set R)"
from ‹?choice› cover_left_linear have choice: "left_linear_trs ?R ∨ ta_det TA' ∧ state_raise_consistent TA' rel"
unfolding left_linear_trs_union by blast
have finTA: "finite (ta_rules TA')"
unfolding ‹?TA› using fin by auto
have varcond: "⋀ l r. (l, r) ∈ ?R ⟹ vars_term r ⊆ vars_term l"
by (rule cover_var_condition[OF varcond])
from raise_step_boundedI[OF choice finTA ‹?comp› ‹?coh› ‹?cont› ‹?tab› varcond]
have bounded: "e_raise_bounded Matchbounds.match c (set R) (ground_terms_of F F')"
unfolding e_raise_bounded_def by blast
from ‹?GF› ‹?HF› rcm scm have cm:
"set (stackable_of_cm cm) ⊆ F"
"set (roots_of_cm cm) ⊆ F'"
and c: "(const,0) ∈ F"
by auto
show ?thesis
by (rule match_raise_bounded_linear_complexity[OF _ finite_set funas_term_ground_terms_of _ cm c non_duplicating bounded],
insert wf, auto simp: wf_trs_def)
qed
lemma match_bounds_linear_rel_impl:
assumes match: "e = Matchbounds.match"
and non_duplicating: "⋀ l r. (l,r) ∈ set R ∪ set S ⟹ vars_term_ms r ⊆# vars_term_ms l"
and scm: "set (stackable_of_cm cm) ⊆ G"
and rcm: "set (roots_of_cm cm) ⊆ H"
and c_opt: "weak_kind_condition c c_opt (set R)"
shows "deriv_bound_measure_class (relto (rstep (set R)) (rstep (set S))) cm (Comp_Poly 1)"
proof -
let ?match = Matchbounds.match
from wf[unfolded wf_trs_def] have varcond: "⋀ l r. (l,r) ∈ set R ∪ set S ⟹ vars_term r ⊆ vars_term l" by auto
from create_constant_in_ta_two[OF fin coh finG finH contain qfin_final qfin tab inf choice compat compat2, unfolded match]
obtain q const F F' TA' where "G ∪ {(const,0)} = F ∧ H ∪ {(const,0)} = F'
∧ state_compatible TA' rel (cover ?match Strict_TRS (set R))
∧ state_compatible TA' rel (cover ?match (Weak_TRS c_opt) (set S))
∧ lift_term 0 ` ground_terms_of F F' ⊆ (ta_lang TA' :: ('f × nat, 'v) terms)
∧ state_coherent TA' rel
∧ (left_linear_trs (set R ∪ set S) ∨ ta_det TA' ∧ state_raise_consistent TA' rel)
∧ ta_bounded TA' c
∧ TA' = ⦇ ta_final = (ta_final TA), ta_rules = insert ((const,0) [] → q) (ta_rules TA), ta_eps = ta_eps TA ⦈
" (is "?GF ∧ ?HF ∧ ?comp ∧ ?comp2 ∧ ?cont ∧ ?coh ∧ ?choice ∧ ?tab ∧ ?TA") by metis
hence compat: ?comp ?comp2 and contain: ?cont and ?HF ?coh ?choice ?GF ?tab ?TA by auto
let ?R = "cover Matchbounds.match Strict_TRS (set R)"
let ?S = "cover Matchbounds.match (Weak_TRS c_opt) (set S)"
from ‹?choice› have choice: "left_linear_trs (?R ∪ ?S) ∨ ta_det TA' ∧ state_raise_consistent TA' rel"
unfolding left_linear_trs_union using cover_left_linear by blast
have finTA: "finite (ta_rules TA')"
unfolding ‹?TA› using fin by auto
from compat have compat: "state_compatible TA' rel (?R ∪ ?S)" unfolding state_compatible_union by blast
have varcond: "⋀ l r. (l, r) ∈ ?R ∪ ?S ⟹ vars_term r ⊆ vars_term l"
using cover_var_condition[of _ _ _ ?match] varcond by blast
from raise_step_boundedI[OF choice finTA compat ‹?coh› ‹?cont› ‹?tab› varcond]
have bounded: "match_raise_rel_bounded c c_opt (set R) (set S) (ground_terms_of F F')"
unfolding match_raise_rel_bounded_def by blast
from ‹?GF› ‹?HF› rcm scm have cm:
"set (stackable_of_cm cm) ⊆ F"
"set (roots_of_cm cm) ⊆ F'"
and c: "(const,0) ∈ F"
by auto
show ?thesis
by (rule match_raise_bounded_linear_complexity_rel[OF wf _ funas_term_ground_terms_of
_ cm c c_opt non_duplicating bounded], insert
finite_set[of "R @ S"] , auto)
qed
lemma e_bounds_impl:
assumes SN: "locally_terminating (cover e Strict_TRS (set R) ∪ Matchbounds.raise)"
and GR: "funas_trs (set R) ⊆ G" and
G: "set (stackable_of_cm cm) ⊆ G" "set (roots_of_cm cm) ⊆ G"
and H: "H = G"
shows "SN (rstep (set R))"
proof -
let ?R = "cover e Strict_TRS (set R)"
from wf[unfolded wf_trs_def] have varcond: "⋀ l r. (l,r) ∈ set R ⟹ vars_term r ⊆ vars_term l" by auto
from create_constant_in_ta_two[OF fin coh finG finH contain qfin_final qfin tab inf choice compat compat2]
obtain q const F F' TA' where "G ∪ {(const,0)} = F ∧ H ∪ {(const,0)} = F'
∧ state_compatible TA' rel ?R
∧ lift_term 0 ` ground_terms_of F F' ⊆ (ta_lang TA' :: ('f × nat, 'v) terms)
∧ state_coherent TA' rel
∧ (left_linear_trs (set R ∪ set S) ∨ ta_det TA' ∧ state_raise_consistent TA' rel)
∧ ta_bounded TA' c
∧ TA' = ⦇ ta_final = (ta_final TA), ta_rules = insert ((const,0) [] → q) (ta_rules TA), ta_eps = ta_eps TA ⦈
" (is "?GF ∧ ?HF ∧ ?comp ∧ ?cont ∧ ?coh ∧ ?choice ∧ ?tab ∧ ?TA") by metis
hence compat: ?comp and contain: ?cont and ?GF ?HF ?coh ?choice ?GF ?TA ?tab by auto
from ‹?choice› have choice: "left_linear_trs ?R ∨ ta_det TA' ∧ state_raise_consistent TA' rel"
unfolding left_linear_trs_union using cover_left_linear by blast
have subF: "funas_trs (set R) ⊆ F" using GR ‹?GF› by auto
have finR: "finite (set R)" by auto
have c: "(const, 0) ∈ F" using ‹?GF› by auto
let ?wF = "{t . funas_term t ⊆ F} :: ('f,'v)terms"
let ?L = "{t. t ∈ ?wF ∧ ground t}"
from H ‹?GF› ‹?HF› have F': "F' = F" by auto
have L: "?L ⊆ ground_terms_of F F'" unfolding F'
proof (clarify)
fix t
assume "ground t" and "funas_term t ⊆ F"
thus "t ∈ ground_terms_of F F" unfolding ground_terms_of_def
by (cases t, auto)
qed
from finG ‹?GF› have finF: "finite F" by auto
show ?thesis
proof (rule SN_wf_ground[OF c subF])
fix t :: "('f,'v)term"
assume "funas_term t ⊆ F" "ground t"
hence t: "t ∈ ?L" by auto
have "SN_on (rstep (set R)) ?L"
proof (rule e_bounds[OF choice _ ‹?comp› ‹?coh› _ ‹?tab› SN finF finR])
show "lift_term 0 ` {t ∈ ?wF. ground t} ⊆ ta_lang TA'" using ‹?cont› L by auto
show "finite (ta_rules TA')"
unfolding ‹?TA› using fin by auto
qed (insert wf[unfolded wf_trs_def], auto)
thus "SN_on (rstep (set R)) {t}" using t unfolding SN_on_def by blast
qed
qed
end
fun flatten_term_enum_filter :: "(('f,'v)term ⇒ bool) ⇒ ('f list,'v)term ⇒ ('f,'v)term list"
where "flatten_term_enum_filter f (Var x) = (let tx = Var x in if f tx then [tx] else [])"
| "flatten_term_enum_filter f (Fun fs ts) = (
let lts = map (flatten_term_enum_filter f) ts
in (if Bex (set lts) (λ ts. ts = []) then [] else
(let ss = concat_lists lts
in filter f (concat (map (λ f. map (Fun f) ss) fs)))))"
lemma flatten_term_enum_filter:
shows "set (flatten_term_enum_filter f t) = {u. instance_term u (map_funs_term set t) ∧ (∀ v ⊴ u. f v)}"
proof (induct t)
case (Var x)
show ?case (is "_ = ?R")
proof -
{
fix t
assume "t ∈ ?R"
hence "t = Var x" by (cases t, auto)
}
thus ?thesis using supteq_Var_id[of x] by (auto simp: Let_def)
qed
next
case (Fun fs ts)
show ?case (is "?L = ?R")
proof -
{
fix i
assume "i < length ts"
hence "ts ! i ∈ set ts" by auto
note Fun[OF this]
} note ind = this
have idL: "?L = {Fun g ss | g ss. g ∈ set fs ∧ length ss = length ts ∧ f (Fun g ss) ∧ (∀i<length ts. ss ! i ∈ set (flatten_term_enum_filter f (ts ! i)))}" (is "_ = ?M1") by (simp add: Let_def set_conv_nth[of ts], auto)
let ?R1 = "{Fun g ss | g ss. g ∈ set fs ∧ length ss = length ts ∧ f (Fun g ss) ∧ (∀ i<length ss. instance_term (ss ! i) (map_funs_term set (ts ! i)) ∧ (∀ u ⊴ (ss ! i). f u))}"
{
fix u
have "(u ∈ ?R) = (u ∈ ?R1)"
proof (cases u)
case (Fun g ss)
show ?thesis unfolding Fun
by (auto simp: Fun_supteq set_conv_nth[of ss])
qed auto
}
hence idR: "?R = ?R1" by auto
show ?case unfolding idL idR using ind by auto
qed
qed
definition inverse_base_term :: "('f,'v)term ⇒ nat ⇒ ('f × nat,'v)term list"
where "inverse_base_term l c ≡ let hs = [0..< Suc c] in flatten_term_enum (map_funs_term (λ f. map (λ h. lift h f) hs) l)"
lemma inverse_base_term: "set (inverse_base_term l c) =
{l'. base_term l' = (l :: ('f,'v)term) ∧ (∀ f n. (f,n) ∈ funas_term l' ⟶ height f ≤ c)}"
proof -
obtain cs where cs: "cs = [0..<Suc c]" by auto
let ?m = "map_funs_term (λf. set (map (λh. lift h f) cs))"
let ?i = "λ u l. instance_term u (?m l)"
let ?h = "λl. (∀ f n. (f,n) ∈ funas_term l ⟶ height f ≤ c)"
let ?b = "λl' l. base_term l' = l ∧ ?h l'"
let ?I = "λl. {u. ?i u l}"
let ?B = "λl. {u. ?b u l}"
have "?I l = ?B l"
proof (induct l)
case (Var x)
{
fix u
have "(u ∈ ?I (Var x)) = (u ∈ ?B (Var x))"
by (cases u, auto)
}
thus ?case by auto
next
case (Fun f ss) note ind = this
let ?s = "Fun f ss"
{
fix u
have "(u ∈ (?I ?s)) = (u ∈ (?B ?s))"
proof (cases u)
case (Var x)
thus ?thesis by auto
next
case (Fun g ts)
let ?t = "Fun g ts"
obtain gg cc where g: "g = (gg,cc)" by (cases g, auto)
show ?thesis
proof (cases "length ts = length ss ∧ gg = f ∧ cc ≤ c")
case False
thus ?thesis unfolding Fun g cs by auto
next
case True
hence len: "length ts = length ss" and u: "u = Fun (f,cc) ts"
and cc: "cc ≤ c" and cc2: "cc ∈ set cs" using Fun g unfolding cs by auto
{
fix i
assume "i < length ss"
hence "ss ! i ∈ set ss" by auto
from ind[OF this]
have "?i (ts ! i) (ss ! i) = ?b (ts ! i) (ss ! i)" by auto
} note ind = this
have "?i u ?s = ?b u ?s" unfolding u term.map funas_term.simps
set_map set_conv_nth[of ts]
by (simp add: len cc cc2, unfold map_nth_eq_conv[OF len, of base_term] , insert ind, simp, blast)
thus ?thesis by auto
qed
qed
}
thus ?case by simp
qed
thus ?thesis unfolding inverse_base_term_def Let_def flatten_term_enum cs map_funs_term_comp o_def .
qed
definition inverse_base_term_filter :: "(('f × nat,'v)term ⇒ bool) ⇒ ('f,'v)term ⇒ nat ⇒ ('f × nat,'v)term list"
where "inverse_base_term_filter filt l c ≡ let hs = [0..< Suc c] in flatten_term_enum_filter filt (map_funs_term (λ f. map (λ h. lift h f) hs) l)"
lemma inverse_base_term_filter: "set (inverse_base_term_filter filt l c) =
{l'. base_term l' = (l :: ('f,'v)term) ∧ (∀ u ⊴ l'. filt u) ∧ (∀ f n. (f,n) ∈ funas_term l' ⟶ height f ≤ c)}"
proof -
obtain cs where cs: "cs = [0..<Suc c]" by auto
let ?m = "map_funs_term (λf. set (map (λh. lift h f) cs))"
let ?f = "λ u. (∀ v ⊴ u. filt v)"
let ?i' = "λ u l. instance_term u (?m l)"
let ?i = "λ u l. ?i' u l ∧ ?f u"
let ?h = "λl. (∀ f n. (f,n) ∈ funas_term l ⟶ height f ≤ c)"
let ?b' = "λl' l. base_term l' = l ∧ ?h l'"
let ?b = "λl' l. base_term l' = l ∧ ?f l' ∧ ?h l'"
let ?I = "λl. {u. ?i u l}"
let ?B = "λl. {u. ?b u l}"
{
fix u
have "?i u l = ?b u l"
proof (induct l arbitrary: u)
case (Var x u)
show ?case by (cases u, auto)
next
case (Fun f ss u) note ind = this
let ?s = "Fun f ss"
show ?case
proof (cases u)
case (Var x)
thus ?thesis by auto
next
case (Fun g ts)
let ?t = "Fun g ts"
obtain gg cc where g: "g = (gg,cc)" by (cases g, auto)
show ?thesis
proof (cases "length ts = length ss ∧ gg = f ∧ cc ≤ c ∧ ?f ?t")
case False
thus ?thesis unfolding Fun g cs by auto
next
case True
hence len: "length ts = length ss" and u: "u = Fun (f,cc) ts"
and cc: "cc ≤ c" and cc2: "cc ∈ set cs" and ff: "?f (Fun (f,cc) ts)" using Fun g unfolding cs by auto
{
fix i
assume i: "i < length ss"
with len have "ts ! i ∈ set ts" by auto
hence sub: "Fun (f,cc) ts ⊵ ts ! i" by auto
have ff: "?f (ts ! i)"
proof(intro allI impI)
fix v
assume "ts ! i ⊵ v"
with sub have "Fun (f,cc) ts ⊵ v" by (rule supteq_trans)
with ff show "filt v" by auto
qed
from i have "ss ! i ∈ set ss" by auto
from ind[OF this, of "ts ! i"] ff
have "?i' (ts ! i) (ss ! i) = ?b' (ts ! i) (ss ! i)"
by auto
} note ind = this
show "?i u ?s = ?b u ?s" unfolding u term.map funas_term.simps
set_map set_conv_nth[of ts]
by (simp add: len cc cc2, unfold map_nth_eq_conv[OF len, of base_term] , insert ind, simp, blast)
qed
qed
qed
}
thus ?thesis unfolding inverse_base_term_filter_def Let_def flatten_term_enum_filter cs map_funs_term_comp o_def by auto
qed
declare compute_height.simps[code del]
hide_const br
lemma compute_height_code[code]:
"compute_height Strict_TRS bl br = (λ l x. Suc x)"
"compute_height (Weak_TRS (Some c)) bl br = (if size (funs_term_ms bl) ≥ size (funs_term_ms br) then
(λ l x. if lift_term x bl = l then min c x else min c (Suc x)) else
(λ l x. min c (Suc x)))"
"compute_height (Weak_TRS None) bl br = (if size (funs_term_ms bl) ≥ size (funs_term_ms br) then
(λ l x. if lift_term x bl = l then x else (Suc x)) else
(λ l x. Suc x))"
by (intro ext, simp)+
definition cover_bound_list_filter :: "(('f × nat,'v)term ⇒ bool) ⇒ (('f,'v)rule ⇒ ('f,'v)term ⇒ bool) ⇒ relation_kind ⇒ nat ⇒ ('f,'v)rules ⇒ ('f × nat,'v)rule list"
where "cover_bound_list_filter filt ff gg c R ≡ concat (map (λ(l,r).
let ch = compute_height gg l r;
ee = ff (l,r) in map
(λ l'. ((l', lift_term
(ch l' (min_list (map height (sym_collect (λ t'. ee (base_term t')) l')))) r)))
(inverse_base_term_filter filt l c))
R)"
lemma cover_bound_list_filter: "set (cover_bound_list_filter ff e ee c (R :: ('f,'v)rules)) = (cover_bound c e ee (set R) ∩ {(l,r). (∀ u ⊴ l. ff u)})" (is "?L = ?R")
proof -
obtain h where h: "h = (λ l' l r. compute_height ee l r l' (min_list (map height (sym_collect (λt'. e (l,r) (base_term t')) l'))))" by auto
obtain RR where RR: "cover_bound c e ee (set R) ∩ {(l,r). (∀ u ⊴ l. ff u)} = RR" by auto
let ?f = "λl. (∀ u ⊴ l. ff u)"
{
fix l' r'
assume l'r': "(l',r') ∈ ?L"
from l'r'[unfolded cover_bound_list_filter_def Let_def]
obtain l r where lr: "(l,r) ∈ set R" and
l'r': "(l',r') ∈ set (map (λl'. (l', lift_term (h l' l r) r)) (inverse_base_term_filter ff l c))"
unfolding h set_concat set_map by force
hence
r': "r' = lift_term (h l' l r) r"
and l': "l' ∈ set (inverse_base_term_filter ff l c)"
by auto
from l'[unfolded inverse_base_term_filter]
have l': "base_term l' = l"
and c: "∀ f n. (f,n) ∈ funas_term l' ⟶ height f ≤ c"
and f: "?f l'" by auto
from lr r' l' c have cover: "(l',r') ∈ cover e ee (set R)" unfolding cover_def h by auto
have "(l',r') ∈ ?R" using c cover f unfolding cover_bound_def by auto
}
moreover
{
fix l' r'
assume "(l',r') ∈ ?R"
hence cover: "(l',r') ∈ cover e ee (set R)"
and c: "∀ f n. (f,n) ∈ funas_term l' ⟶ height f ≤ c"
and f: "?f l'"
unfolding cover_bound_def by auto
from cover[unfolded cover_def]
obtain l r where
lr: "(l,r) ∈ set R"
and r': "r' = lift_term (h l' l r) r"
and l': "base_term l' = l"
unfolding h by simp blast
from c l' f have l': "l' ∈ set (inverse_base_term_filter ff l c)"
unfolding inverse_base_term_filter by auto
have "(l',r') ∈ ?L"
by (unfold cover_bound_list_filter_def Let_def set_concat set_map, rule, rule, rule lr, unfold set_map r' h, rule, rule refl, rule l')
}
ultimately show ?thesis unfolding RR by force
qed
lemma remove_compatible_rules:
assumes compat: "state_compatible TA rel (cover_bound e ee c R ∩ {(l,r). ff l r})"
and filter: "⋀ l r. ¬ ff l r ⟹ rule_state_compatible TA rel (l,r)"
shows "state_compatible TA rel (cover_bound e ee c R)"
using assms unfolding state_compatible_def by blast
datatype boundstype = Roof | Match
fun boundstype_fun :: "boundstype ⇒ ('f,'v) rule ⇒ ('f,'v)term ⇒ bool"
where "boundstype_fun Roof = Matchbounds.roof"
| "boundstype_fun Match = Matchbounds.match"
fun bounds_condition :: "boundstype ⇒ ('f :: show ,'v :: show)rules ⇒ shows check"
where "bounds_condition Roof _ = succeed"
| "bounds_condition Match R = (check_all (λ(l,r). vars_term_ms r ⊆# vars_term_ms l) R
<+? (λ (l,r). shows ''rule '' +@+ shows_rule (l,r) +@+ shows '' is duplicating''))"
lemma bounds_condition: assumes ok: "isOK(bounds_condition type R)"
and wf: "wf_trs (set R)"
shows "locally_terminating (cover (boundstype_fun type) Strict_TRS (set R) ∪ Matchbounds.raise)"
proof (cases type)
case Roof
show ?thesis unfolding Roof
using roof_raise_locally_SN[OF wf]
by auto
next
case Match
show ?thesis unfolding Match
by (unfold boundstype_fun.simps, rule match_raise_locally_SN[OF wf],
insert ok[unfolded Match], auto)
qed
context
begin
private fun relation_as_list :: "'q ta_relation ⇒ shows + ('q × 'q) list" where
"relation_as_list (Some_Relation rel) = return rel"
| "relation_as_list Id_Relation = return []"
| "relation_as_list Decision_Proc = error (shows ''decision procedure not available for non-left linear TRSs'')"
| "relation_as_list Decision_Proc_Old = error (shows ''decision procedure not available for non-left linear TRSs'')"
definition check_state_raise_consistent :: "('q :: {linorder,show},('f :: show) × nat)tree_automaton ⇒ ('q × 'q) list ⇒ shows check" where
"check_state_raise_consistent TA rel = do {
let rels = set rel;
let rls = ta_rules_impl' TA;
check_allm (λ r1. case r1 of TA_rule (f1,i1) qs1 q1 ⇒
check_allm (λ r2. case r2 of TA_rule (f2,i2) qs2 q2 ⇒
if (f1 = f2 ∧ i1 < i2 ∧ qs1 = qs2) then check ((q1,q2) ∈ rels)
(shows ''problem with raise consistency because of automaton-rules '' +@+ shows_nl
+@+ shows r1 +@+ shows_nl +@+ shows r2 +@+ shows_nl +@+ shows q1 +@+ shows '' is not >>^* ''
+@+ shows q2) else succeed) rls) rls
}"
lemma check_state_raise_consistent[simp]:
"isOK(check_state_raise_consistent TA rel) = state_raise_consistent (ta_of_ta TA) (set rel)"
unfolding check_state_raise_consistent_def Let_def state_raise_consistent_def
by (cases TA, fastforce split: ta_rule.splits)
definition check_ta_bounded where
"check_ta_bounded TA c ≡ check_all (λ (f,n). height f ≤ c) (map fst (rm.to_list (ta_rules_impl TA)))
<+? (λ (f,n). shows f +@+ shows '' is symbol in TA with height larger than c = '' +@+ shows c)"
datatype ('f,'q)bounds_info = Bounds_Info (boundstype: boundstype) nat "'q list" "('q, 'f × nat) tree_automaton" "'q ta_relation"
definition construct_c_opt :: "nat ⇒ ('f,'v)rules ⇒ nat option" where
"construct_c_opt c R = (if non_collapsing_impl R then Some c else None)"
lemma construct_c_opt[simp]: "weak_kind_condition c (construct_c_opt c R) (set R)"
unfolding construct_c_opt_def
by (auto split: if_splits)
primrec check_bounds_generic :: "('f :: {show,linorder},'q :: {show,linorder})bounds_info ⇒
('f,'v :: {show,linorder})rules ⇒ ('f,'v)rules ⇒
('f × nat)list ⇒ ('f × nat)list ⇒ shows check" where
"check_bounds_generic (Bounds_Info type c qfin preTA rel) R S F G = (do {
let c_opt = construct_c_opt c R;
let RS = R @ S;
TA ← generate_ta_cond preTA rel;
let rell = rel_checker rel;
check_wf_trs RS;
check (set qfin ⊆ rs.α (ta_final_impl TA)) (shows ''explicitly mentioned final states must be final'');
(if isOK(check_left_linear_trs RS) then succeed else
do {
check_det preTA <+? (λ s. shows ''for non left-linear TRS we require det. automaton'' +@+ shows_nl +@+ s);
rel_list ← relation_as_list rel;
check_state_raise_consistent preTA rel_list
});
bounds_condition type RS;
check_ta_bounded TA c;
check (Bex (set qfin) (λ q. rs.memb q (ta_rhs_states_set TA))) (shows ''did not find mentioned final state in TA'');
ta_contains_impl (map (λ(f,n). (lift 0 f,n)) F) (map (λ(f,n). (lift 0 f,n)) G) TA qfin
<+? (λ fqs. shows ''it could not be guaranteed that lift0(T(Sigma)) is accepted by TA'' +@+ shows_nl +@+
(shows ''there is no transition from '' +@+ shows fqs +@+ shows '' to a final state''));
state_compatible_eff_list TA rell (cover_bound_list_filter (λ l. ¬ rule_state_compatible_heuristic TA l) (boundstype_fun type) Strict_TRS c R)
<+? (λ (lr,lr_rhs,q). shows ''TA is not compatible with TRS'' +@+ shows_nl
+@+ shows ''for rule '' +@+ shows_rule lr +@+ shows_nl
+@+ shows ''which is instantiated by states to '' +@+ shows_rule lr_rhs +@+ shows_nl
+@+ shows ''the state '' +@+ shows q +@+ shows '' is only reachable from the lhs'' +@+ shows_nl);
state_compatible_eff_list TA rell (cover_bound_list_filter (λ l. ¬ rule_state_compatible_heuristic TA l) Matchbounds.match (Weak_TRS c_opt) c S)
<+? (λ (lr,lr_rhs,q). shows ''TA is not compatible with relative TRS'' +@+ shows_nl
+@+ shows ''for rule '' +@+ shows_rule lr +@+ shows_nl
+@+ shows ''which is instantiated by states to '' +@+ shows_rule lr_rhs +@+ shows_nl
+@+ shows ''the state '' +@+ shows q +@+ shows '' is only reachable from the lhs'' +@+ shows_nl)
})"
lemma check_bounds_generic: assumes ok: "isOK(check_bounds_generic
(info :: ('f,'q :: {linorder,show})bounds_info) (R :: ('f :: {linorder,show},'v :: {linorder, show})rules)
S F G)"
and inf: "infinite (UNIV :: 'f set)"
shows "(∃ ta rel qfin c c_opt.
bounds_impl R S (ta :: ('q,'f × nat)ta) rel (boundstype_fun (boundstype info)) c c_opt (set F) (set G) qfin
∧ weak_kind_condition c c_opt (set R))
∧ isOK (bounds_condition (boundstype info) (R @ S))"
proof -
obtain type c qfin preTA rel where info: "info = Bounds_Info type c qfin preTA rel"
by (cases info, blast+)
let ?c_opt = "construct_c_opt c R"
let ?rel = "rel_checker rel"
let ?rell = "relation_of rel"
note ok = ok[unfolded info, simplified, unfolded Let_def]
from ok obtain TA where TA: "generate_ta_cond preTA rel = return TA" by auto
from generate_ta_cond[OF this] have inv: "ta_inv TA ?rel ?rell" and TA2: "TA = generate_ta preTA" by auto
let ?filt = "λ l. ¬ rule_state_compatible_heuristic TA l"
let ?sfilt = "λ l. (∀ u ⊴ l. ?filt u)"
let ?relll = "relation_as_list rel"
let ?e = "(boundstype_fun type)"
let ?e2 = Matchbounds.match
interpret ta_inv TA ?rel ?rell by fact
have [simp]: "ta_of_ta preTA = TA'" unfolding TA2 generate_ta by simp
note ok = ok[unfolded check_bounds_generic.simps Let_def TA, simplified]
from ok have
wf: "wf_trs (set R ∪ set S)"
and choice: "left_linear_trs (set (R @ S)) ∨ ta_det (ta_of TA)
∧ isOK ?relll ∧ state_raise_consistent (ta_of TA) (set (projr ?relll))" (is "_ ∨ ?det")
and qfin: "∃ q ∈ set qfin. rs.memb q (ta_rhs_states_set TA)"
and c: "isOK(check_ta_bounded TA c)"
and cond: "isOK(bounds_condition type (R @ S))"
and contain: "isOK(ta_contains_impl (map (λ(f,n). (lift 0 f,n)) F) (map (λ(f,n). (lift 0 f,n)) G) TA qfin)"
and compat: "isOK(state_compatible_eff_list TA ?rel (cover_bound_list_filter ?filt ?e Strict_TRS c R))"
and compat2: "isOK(state_compatible_eff_list TA ?rel (cover_bound_list_filter ?filt ?e2 (Weak_TRS ?c_opt) c S))"
and final: "set qfin ⊆ ta_final (ta_of TA)"
by (auto simp: ta_final)
from choice have choice: "left_linear_trs (set (R @ S)) ∨ ta_det (ta_of TA) ∧ state_raise_consistent (ta_of TA) ?rell"
proof
assume ?det
have "state_raise_consistent (ta_of TA) ?rell"
proof (cases rel)
case Id_Relation
with ‹?det› show ?thesis by (auto simp: state_raise_consistent_def)
qed (insert ‹?det›, auto)
with ‹?det› show ?thesis by simp
qed auto
from qfin have qfin: "∃ q ∈ set qfin. q ∈ ta_rhs_states TA'" using ta_rhs_states_set by (auto simp: rs.correct)
let ?C = "cover_bound c ?e Strict_TRS (set R)"
let ?Cf = "cover_bound c ?e Strict_TRS (set R) ∩ {(l,r). ?sfilt l}"
from c have c': "⋀ fn. fn ∈ set (rm.to_list (ta_rules_impl TA)) ⟹ case fst fn of (f,n) ⇒ height f ≤ c"
unfolding check_ta_bounded_def by auto
{
fix f n
assume "(f,n) ∈ ta_syms TA'"
then obtain rule where rule: "rule ∈ ta_rules TA'" and n: "r_sym rule = (f,n)"
unfolding ta_syms_def by auto
let ?crule = "conv_ta_rule (ta_epss_impl TA) rule"
from rule have crule: "?crule ∈ conv_ta_rule (ta_epss_impl TA) ` ta_rules TA'" by auto
from n have n: "r_sym_impl ?crule = (f,n)" by (cases rule, auto)
let ?rm = "ta_rules_impl TA"
from rm_set_lookup3[OF crule, unfolded n]
obtain rls where "rm.α ?rm (f,n) = Some rls" by force
hence "map_of (rm.to_list ?rm) (f,n) = Some rls" by (auto simp: rm.correct)
from map_of_SomeD[OF this]
have "((f,n),rls) ∈ set (rm.to_list ?rm)" .
from c'[OF this] have "height f ≤ c" by simp
} note c = this
hence tab: "ta_bounded TA' c" unfolding ta_bounded_def by auto
note var_cond = wf[unfolded wf_trs_def]
{
fix U e ee
assume sub: "set U ⊆ set (R @ S)"
and compat: "isOK(state_compatible_eff_list TA ?rel (cover_bound_list_filter ?filt e ee c U))"
let ?C = "cover_bound c e ee (set U)"
let ?Cf = "?C ∩ {(l, r). ∀u⊴l. ¬ rule_state_compatible_heuristic TA u}"
have "state_compatible TA' ?rell ?Cf"
proof (rule state_compatible_eff_list[OF _ compat, unfolded cover_bound_list_filter])
fix l r
assume "(l,r) ∈ ?Cf"
hence "(l,r) ∈ cover e ee (set U)" unfolding cover_bound_def by auto
from cover_var_condition[OF _ this] var_cond sub
show "vars_term r ⊆ vars_term l" by auto
qed
hence compat: "state_compatible TA' ?rell ?C"
by (rule remove_compatible_rules, insert rule_state_compatible_heuristic_subteq, blast)
} note compat_conv = this
from compat_conv[OF _ compat]
have compat: "state_compatible TA' ?rell ?C" by auto
from compat_conv[OF _ compat2]
have compatS: "state_compatible TA' ?rell (cover_bound c Matchbounds.match (Weak_TRS ?c_opt) (set S))" by auto
obtain fin rls eps where preTA: "preTA = Tree_Automaton fin rls eps" by (cases preTA, auto)
from generate_ta_rules[of fin rls eps] have "ta_rules (ta_of TA) = set rls" using TA2 preTA by auto
hence fin: "finite (ta_rules (ta_of TA))" by auto
have wkc: "weak_kind_condition c ?c_opt (set R)" by simp
have "bounds_impl R S TA' ?rell ?e c ?c_opt (set F) (set G) (set qfin)"
by (unfold_locales, insert final choice fin compat compatS coherent tab qfin inf finite_set wf
ta_contains_impl[OF contain], auto)
with wkc have bounds: "∃ ta rel qfin c c_opt. bounds_impl R S (ta :: ('q,'f × nat)ta) rel
(boundstype_fun (boundstype info)) c c_opt (set F) (set G) qfin
∧ weak_kind_condition c c_opt (set R)"
unfolding info by force
from cond have cond: "isOK (bounds_condition (boundstype info) (R @ S))" unfolding info by simp
from bounds cond show ?thesis by blast
qed
lemma check_bounds: assumes ok: "isOK(check_bounds_generic (info :: ('f,'q :: {linorder,show})bounds_info) (R :: ('f :: {linorder,show},'v :: {linorder, show})rules) []
(funas_trs_list R) (funas_trs_list R))"
and inf: "infinite (UNIV :: 'f set)"
shows "SN (rstep (set R))"
proof -
let ?S = "[]"
let ?bt = "boundstype info"
let ?F = "set (funas_trs_list R)"
from check_bounds_generic[OF ok inf] obtain ta :: "('q,'f × nat)ta" and rel qfin c c_opt where
bounds: "bounds_impl R ?S ta rel (boundstype_fun ?bt) c c_opt ?F ?F qfin"
and cond: "isOK (bounds_condition ?bt R)" by auto
interpret bounds_impl R ?S ta rel "boundstype_fun ?bt" c c_opt ?F ?F qfin by fact
show ?thesis
by (rule e_bounds_impl[where cm = "Derivational_Complexity (funas_trs_list R)",
OF bounds_condition[OF cond]], insert wf, auto)
qed
lemma check_bounds_complexity: assumes ok: "isOK(check_bounds_generic (info :: ('f,'q :: {linorder,show})bounds_info)
(R :: ('f :: {linorder,show},'v :: {linorder, show})rules) []
(stackable_of_cm cm) (roots_of_cm cm))"
and inf: "infinite (UNIV :: 'f set)"
and bt: "boundstype info = Match"
shows "deriv_bound_measure_class (rstep (set R)) cm (Comp_Poly 1)"
proof -
let ?S = "[]"
let ?scm = "stackable_of_cm cm"
let ?rcm = "roots_of_cm cm"
from check_bounds_generic[OF ok inf, unfolded bt] obtain ta :: "('q,'f × nat)ta" and rel qfin c c_opt where
bounds: "bounds_impl R ?S ta rel (boundstype_fun Match) c c_opt (set ?scm) (set ?rcm) qfin"
and cond: "isOK (bounds_condition Match R)" by auto
interpret bounds_impl R ?S ta rel "boundstype_fun Match" c c_opt "set ?scm" "set ?rcm" qfin by fact
from match_bounds_linear_impl[of cm] cond show ?thesis by auto
qed
lemma check_bounds_complexity_rel: assumes ok: "isOK(check_bounds_generic (info :: ('f,'q :: {linorder,show})bounds_info)
(R :: ('f :: {linorder,show},'v :: {linorder, show})rules) S
(stackable_of_cm cm) (roots_of_cm cm))"
and inf: "infinite (UNIV :: 'f set)"
and bt: "boundstype info = Match"
shows "deriv_bound_measure_class (relto (rstep (set R)) (rstep (set S))) cm (Comp_Poly 1)"
proof -
let ?scm = "stackable_of_cm cm"
let ?rcm = "roots_of_cm cm"
from check_bounds_generic[OF ok inf, unfolded bt] obtain ta :: "('q,'f × nat)ta" and rel qfin c c_opt where
bounds: "bounds_impl R S ta rel (boundstype_fun Match) c c_opt (set ?scm) (set ?rcm) qfin"
and cond: "isOK (bounds_condition Match (R @ S))"
and wkc: "weak_kind_condition c c_opt (set R)" by auto
interpret bounds_impl R S ta rel "boundstype_fun Match" c c_opt "set ?scm" "set ?rcm" qfin by fact
show ?thesis
by (rule match_bounds_linear_rel_impl[of cm], insert cond wkc, auto)
qed
end
definition
bounds_tt ::
"('tp, 'f, 'v :: {show,linorder}) tp_ops ⇒
('f::{show,linorder}, 'q::{show,linorder}) bounds_info ⇒
'tp ⇒ shows check"
where
"bounds_tt I info tp ≡ do {
let r = tp_ops.rules I tp;
let f = funas_trs_list r;
check_bounds_generic info r [] f f
}"
lemma bounds_tt: fixes info :: "('f::{show,linorder}, 'q::{show,linorder}) bounds_info"
assumes "tp_spec I" and ok: "isOK (bounds_tt I info tp)"
and inf: "infinite (UNIV :: 'f set)"
shows "SN_qrel (tp_ops.qreltrs I tp)"
proof -
interpret tp_spec I by fact
from check_bounds[OF ok[unfolded bounds_tt_def Let_def, simplified] inf]
have SN: "SN_qrel (NFS tp, {}, set (R tp) ∪ set (Rw tp), {})" by simp
show ?thesis unfolding qreltrs_sound
by (rule SN_qrel_mono[OF _ _ _ SN]) simp_all
qed
definition
bounds_complexity ::
"('tp, 'f, 'v :: {show,linorder}) tp_ops ⇒
('f::{show,linorder}, 'q::{show,linorder}) bounds_info ⇒
('f,'v)complexity_measure ⇒ complexity_class ⇒
'tp ⇒ shows check"
where
"bounds_complexity I info cm cc tp ≡ do {
check (Comp_Poly 1 ≤ cc) (shows ''can only ensure linear complexity'');
check (boundstype info = Match) (shows ''complexity analysis requires boundstype match'');
check_bounds_generic info (tp_ops.rules I tp) [] (stackable_of_cm cm) (roots_of_cm cm)
} <+? (λ s. shows ''problem in ensuring match boundedness of '' +@+ shows_nl +@+
shows_tp I tp +@+ shows_nl +@+ s)"
lemma bounds_complexity: fixes info :: "('f::{show,linorder}, 'q::{show,linorder}) bounds_info"
assumes "tp_spec I" and ok: "isOK (bounds_complexity I info cm cc tp)"
and inf: "infinite (UNIV :: 'f set)"
shows "deriv_bound_measure_class (rel_qrstep (tp_ops.qreltrs I tp)) cm cc"
proof -
interpret tp_spec I by fact
note isOK_if [simp]
from ok[unfolded bounds_complexity_def Let_def, simplified]
have cc: "O_of (Comp_Poly 1) ⊆ O_of cc" and bt: "boundstype info = Match"
and ok: "isOK (check_bounds_generic info (rules tp) [] (stackable_of_cm cm) (roots_of_cm cm))" by auto
from check_bounds_complexity[OF ok inf bt]
have bound: "deriv_bound_measure_class (rstep (set (rules tp))) cm (Comp_Poly 1)" .
show ?thesis
by (rule deriv_bound_measure_class_trancl_mono[OF _ _ _ bound], simp, rule relto_trancl_subset, insert cc, auto)
qed
definition
bounds_complexity_rel ::
"('tp, 'f, 'v :: {show,key}) tp_ops ⇒
('f::{show,key}, 'q::{show,linorder}) bounds_info ⇒
('f,'v)rules ⇒
('f,'v)complexity_measure ⇒ complexity_class ⇒
'tp ⇒ 'tp result"
where
"bounds_complexity_rel I info Rdelete cm cc tp ≡ do {
let R = tp_ops.R I tp;
let Rw = tp_ops.Rw I tp;
let R2 = ceta_list_diff R Rdelete;
check_subseteq Rdelete (tp_ops.rules I tp) (* this is not required, just for early error detection *)
<+? (λ lr. shows ''could not find rule '' +@+ shows_rule lr +@+ shows '' in current complexity problem'');
check (Comp_Poly 1 ≤ cc) (shows ''can only ensure linear complexity'');
check (boundstype info = Match) (shows ''complexity analysis requires boundstype match'');
let all = tp_ops.rules I tp;
check_bounds_generic info Rdelete (Rw @ R2) (stackable_of_cm cm) (roots_of_cm cm);
return (tp_ops.mk I (tp_ops.nfs I tp) (tp_ops.Q I tp) R2 (list_union Rw Rdelete))
} <+? (λ s. shows ''problem in ensuring match-RT boundedness of '' +@+ shows_nl +@+
shows_tp I tp +@+ shows_nl +@+ shows ''with deletion of rules'' +@+ shows_nl +@+ shows_trs Rdelete +@+ s)"
lemma bounds_complexity_rel: fixes info :: "('f::{show,key}, 'q::{show,linorder}) bounds_info"
assumes "tp_spec I" and res: "bounds_complexity_rel I info Rdelete cm cc tp = return tp'"
and inf: "infinite (UNIV :: 'f set)"
and rec: "deriv_bound_measure_class (rel_qrstep (tp_ops.qreltrs I tp')) cm cc"
shows "deriv_bound_measure_class (rel_qrstep (tp_ops.qreltrs I tp)) cm cc"
proof -
interpret tp_spec I by fact
note isOK_if [simp]
let ?R = "R tp"
let ?Rw = "Rw tp"
let ?diff = "ceta_list_diff ?R Rdelete"
let ?union = "list_union ?Rw Rdelete"
from res[unfolded bounds_complexity_rel_def Let_def, simplified]
have cc: "O_of (Comp_Poly 1) ⊆ O_of cc" and bt: "boundstype info = Match"
and ok: "isOK (check_bounds_generic info Rdelete (?Rw @ ?diff) (stackable_of_cm cm) (roots_of_cm cm))"
and tp': "tp' = mk (NFS tp) (Q tp) ?diff ?union" by auto
from rec[unfolded tp', simplified]
have rec: "deriv_bound_measure_class
(relto (qrstep (NFS tp) (set (Q tp)) (set (R tp) - set Rdelete))
(qrstep (NFS tp) (set (Q tp)) (set (Rw tp) ∪ set Rdelete)))
cm cc" .
from check_bounds_complexity_rel[OF ok inf bt]
have bnd: "deriv_bound_measure_class (relto (rstep (set Rdelete)) (rstep (set (?Rw @ ?diff))))
cm (Comp_Poly 1)" .
have bnd: "deriv_bound_measure_class
(relto
(qrstep (NFS tp) (set (Q tp)) (set (R tp) - set Rdelete) ∪ qrstep (NFS tp) (set (Q tp)) (set Rdelete))
(qrstep (NFS tp) (set (Q tp)) (set (Rw tp))))
cm cc"
by (rule deriv_bound_relto_measure_class_union[OF rec[unfolded qrstep_union]
deriv_bound_measure_class_mono[OF relto_mono _ cc bnd]], auto)
show ?thesis unfolding qreltrs_sound split
by (rule deriv_bound_measure_class_mono[OF relto_mono subset_refl subset_refl bnd], auto)
qed
end