theory Conditional_Rewriting_Impl
imports
Conditional_Rewriting
QTRS.Trs_Impl
begin
lemma forallM_cong [fundef_cong]:
assumes "xs = ys" and "⋀x. x ∈ set ys ⟹ f x = g x"
shows "forallM f xs = forallM g ys"
using assms by (induct ys arbitrary: xs) simp_all
lemma check_eq_Inr [termination_simp]: "check b e = Inr y ⟷ b"
by (cases b) (auto simp: check_def)
type_synonym ('f, 'v) crules = "('f, 'v) crule list"
definition "shows_eq' fun var = shows_rule' fun var '' ->* ''"
abbreviation "shows_eq ≡ shows_eq' shows shows"
definition "shows_conditions' fun var = shows_sep (shows_eq' fun var) (shows '', '')"
abbreviation "shows_conditions ≡ shows_conditions' shows shows"
definition shows_crule' :: "('f ⇒ shows) ⇒ ('v ⇒ shows) ⇒ ('f, 'v) crule ⇒ shows"
where
"shows_crule' fun var cr =
shows_rule' fun var '' -> '' (fst cr) ∘
(if snd cr = [] then id else shows '' | '') ∘
shows_conditions' fun var (snd cr)"
abbreviation "shows_crule ≡ shows_crule' shows shows"
definition
shows_crules' :: "('f ⇒ shows) ⇒ ('v ⇒ shows) ⇒ ('f, 'v) crules ⇒ shows"
where
"shows_crules' fun var ctrs =
shows_list_gen (shows_crule' fun var) [] [] [CHR ''⏎''] [] ctrs ∘ shows_nl"
abbreviation "shows_crules ≡ shows_crules' shows shows"
definition
shows_ctrs' :: "('f ⇒ shows) ⇒ ('v ⇒ shows) ⇒ ('f, 'v) crules ⇒ shows"
where
"shows_ctrs' fun var R = shows ''CTRS:'' ∘ shows_nl ∘ shows_nl ∘ shows_crules' fun var R"
abbreviation "shows_ctrs ≡ shows_ctrs' shows shows"
definition "shows_coverlap ρ⇩1 ρ⇩2 p =
shows ''overlap of conditional rules '' ∘ shows_crule ρ⇩1 ∘ shows '' and '' ∘ shows_crule ρ⇩2 ∘
shows '' at position '' ∘ shows p"
definition check_type3 :: "('f :: show, 'v :: show) crules ⇒ shows check"
where
"check_type3 R = do {
check_allm (λcr. check_subseteq (vars_term_list (snd (fst cr))) (vars_term_list (fst (fst cr)) @ vars_trs_list (snd cr))
<+? (λx. shows ''variable '' ∘ shows x
∘ shows '' occurs only in right-hand side of rule '' ∘ shows_crule cr ∘ shows_nl)) R
} <+? (λe. shows ''the CTRS is not of type 3'' ∘ shows_nl ∘ e)"
lemma check_type3 [simp]:
"isOK (check_type3 R) = type3 (set R)"
unfolding check_type3_def type3_def by force
definition X_impl :: "('f, 'v) crule ⇒ nat ⇒ 'v list"
where "X_impl cr i =
concat (vars_term_list (fst (fst cr)) # (map (vars_term_list ∘ snd) (take i (snd cr)) ))"
lemma X_impl [simp]:
"set (X_impl cr i) = X_vars cr i"
unfolding X_impl_def X_vars_def by force
definition Y_impl :: "('f, 'v) crule ⇒ nat ⇒ 'v list"
where "Y_impl cr i =
vars_term_list (snd (fst cr)) @ vars_term_list (snd ((snd cr) ! i)) @ (vars_trs_list (drop (Suc i) (snd cr)))"
lemma Y_impl:
"set (Y_impl cr i) = Y_vars cr i"
unfolding Y_impl_def Y_vars_def by force
definition check_dctrs :: "('f :: show, 'v :: show) crules ⇒ shows check"
where
"check_dctrs R = do {
check_allm
(λcr.
check_allm
(λi.
check_subseteq (vars_term_list (fst (snd cr ! i))) (X_impl cr i)
<+? (λx. shows ''variable '' ∘ shows x ∘ shows '' in condition ''
∘ shows_rule (snd cr ! i) ∘ shows '' of rule ''
∘ shows_crule cr ∘ shows ''violates DCTRS condition'' ∘ shows_nl)
) [0..<length (snd cr)]
) R
} <+? (λe. shows ''the CTRS is not deterministic'' ∘ shows_nl ∘ e)"
lemma check_dctrs [simp]:
"isOK (check_dctrs R) = dctrs (set R)"
by (auto simp add: check_dctrs_def dctrs_def atLeast0LessThan)
definition check_wf_ctrs :: "('f :: show, 'v :: show) crules ⇒ shows check"
where
"check_wf_ctrs R = do {
check_varcond_no_Var_lhs (map fst R);
check_dctrs R;
check_type3 R
} <+? (λe. shows ''the CTRS is not well-formed'' ∘ shows_nl ∘ e)"
lemma check_wf_ctrs [simp]:
"isOK (check_wf_ctrs R) = wf_ctrs (set R)"
by (force simp: check_wf_ctrs_def wf_ctrs_def)
definition funs_crule_list :: "('f, 'v) crule ⇒ 'f list"
where
"funs_crule_list r = add_funs_rule (fst r) (funs_trs_list (snd r))"
lemma funs_crule_list_sound [simp]:
"set (funs_crule_list r) = funs_crule r"
by (simp add: funs_crule_list_def funs_crule_def)
definition funs_ctrs_list :: "('f, 'v) crule list ⇒ 'f list"
where
"funs_ctrs_list trs = concat (map funs_crule_list trs)"
lemma funs_ctrs_list_sound [simp]:
"set (funs_ctrs_list r) = funs_ctrs (set r)"
by (simp add: funs_ctrs_list_def funs_ctrs_def)
abbreviation "terms_of_crule ρ ≡ (clhs ρ # crhs ρ # terms_of_rules (snd ρ))"
definition "match_crule ρ⇩1 ρ⇩2 = do {
ts ← zip_option (terms_of_crule ρ⇩2) (terms_of_crule ρ⇩1);
match_list Var ts
}"
abbreviation "term_of_crule ρ ≡ Fun (SOME f. True) (clhs ρ # crhs ρ # terms_of_rules (snd ρ))"
lemma match_crule_alt_def:
"match_crule ρ⇩1 ρ⇩2 = match (term_of_crule ρ⇩1) (term_of_crule ρ⇩2)"
by (cases "zip_option (terms_of_crule ρ⇩1) (terms_of_crule ρ⇩2)")
(auto simp: match_crule_def match_def match_list_def decompose_def split: option.splits)
definition check_properly_oriented :: "('f :: show, 'v :: show) crules ⇒ shows check"
where
"check_properly_oriented R =
check_dctrs (filter (λ((l, r), cs). ¬ vars_term r ⊆ vars_term l) R)
<+? (λe. shows ''the CTRS is not properly oriented'' ∘ shows_nl ∘ e)"
lemma check_properly_oriented [simp]:
"isOK (check_properly_oriented R) = properly_oriented (set R)"
by (simp add: check_properly_oriented_def properly_oriented_def X_vars_def dctrs_def) (fastforce)
definition check_extended_properly_oriented :: "('f :: show, 'v ::show) crules ⇒ shows check"
where
"check_extended_properly_oriented R =
check (extended_properly_oriented (set R))
(shows ''the given CTRS is not extended properly oriented'' ∘ shows_nl)"
lemma check_extended_properly_oriented [simp]:
"isOK (check_extended_properly_oriented R) = extended_properly_oriented (set R)"
by (simp add: check_extended_properly_oriented_def)
definition check_Ru_NF ::
"('f :: {key,show}, 'v :: show) term ⇒ ('f, 'v) crules ⇒ shows check"
where
"check_Ru_NF s R = check
(is_NF_trs (map fst R) s)
(shows ''the term '' ∘ shows_term s ∘ shows '' is not an Ru normal form'' ∘ shows_nl)"
lemma check_Ru_NF [simp]:
"isOK (check_Ru_NF s R) ⟷ s ∈ NF (rstep (Ru (set R)))"
by (simp add: check_Ru_NF_def Ru_def)
definition check_constructor_term ::
"('f :: show, 'v :: show) term ⇒ ('f :: show, 'v :: show) crules ⇒ shows check"
where
"check_constructor_term s R = check
(funas_term s ⊆ funas_ctrs (set R) - set (defined_list (map fst R)))
(shows ''the term '' ∘ shows_term s ∘ shows '' is not a constructor term'' ∘ shows_nl)"
lemma check_constructor_term [simp]:
"isOK (check_constructor_term s R) =
(funas_term s ⊆ funas_ctrs (set R) - { f. defined (Ru (set R)) f })"
by (simp add: check_constructor_term_def Ru_def)
definition check_right_stable :: "('f :: {key,show}, 'v :: show) crules ⇒ shows check"
where
"check_right_stable R = check_allm (λr.
check_allm (λi. do {
let t⇩i = snd (snd r ! i);
check_disjoint
(vars_term_list (fst (fst r)) @
(concat (map (λ(s, t). vars_term_list s) (take (Suc i) (snd r)))) @
(concat (map (λ(s, t). vars_term_list t) (take i (snd r)))))
(vars_term_list t⇩i)
<+? (λx. shows ''variable '' ∘ shows x ∘ shows '' in rhs of condition '' ∘
shows i ∘ shows '' is not fresh'' ∘ shows_nl);
choice [(check_linear_term t⇩i ⪢ check_constructor_term t⇩i R),
(check_ground_term t⇩i ⪢ check_Ru_NF t⇩i R)] <+? shows_sep id shows_nl
}
) [0..< length (snd r)]
) R
<+? (λe. shows ''the CTRS is not right stable'' ∘ shows_nl ∘ e)"
lemma check_right_stable [simp]:
"isOK (check_right_stable R) = right_stable (set R)"
unfolding check_right_stable_def
using [[simproc del: list_to_set_comprehension]]
by (simp add: right_stable_def Let_def atLeast0LessThan case_prod_beta) (blast)
datatype ('f, 'v) cstep_proof =
Cstep_step "('f, 'v) crule" pos "('f, 'v) subst"
(cstep_src : "('f, 'v) term")
(cstep_trg : "('f, 'v) term")
"('f, 'v) cstep_proof list list"
lemma [termination_simp]:
"i < length xs ⟹ size_list size (xs ! i) < size_list (size_list size) xs"
proof (induct xs arbitrary: i)
case (Cons x xs)
then show ?case by (cases i) (auto simp add: less_Suc_eq trans_less_add2)
qed simp
definition
"check_crule_variants r r' = do {
let rs = fst r # conds r;
let rs' = fst r' # conds r';
check (match_rules rs rs' ≠ None ∧ match_rules rs' rs ≠ None)
(shows_crule r ∘ shows '' and '' ∘ shows_crule r' ∘ shows '' are not variants of each other'' ∘ shows_nl)
}"
lemma check_crule_variants [elim!]:
assumes "isOK (check_crule_variants r r')"
obtains p where "p ∙ r = r'"
using assms
by (cases r rule: crule_cases; cases r' rule: crule_cases)
(auto simp: check_crule_variants_def eqvt dest: match_rules_imp_variants)
definition
"check_variant_in_ctrs R r =
check_exm (check_crule_variants r) R (shows_sep id id)
<+? (λ_. shows ''rule '' ∘ shows_crule r ∘ shows '' is not a variant of any rule in:'' ∘
shows_nl ∘ shows_ctrs R)"
lemma check_variant_in_ctrs:
assumes "isOK (check_variant_in_ctrs R r)"
obtains p where "p ∙ r ∈ set R"
using assms
by (cases r rule: crule_cases) (force simp: check_variant_in_ctrs_def eqvt)
fun check_cstep and check_csteps
where
"check_cstep R (Cstep_step ((l, r), cs) p σ s t pss) = do {
check_variant_in_ctrs R ((l, r), cs);
check (length pss = length cs) (shows ''mismatch between number of conditions and number of rewrite sequences'');
check (s = replace_at s p (l ⋅ σ)) (shows s ∘ shows '' does not contain an instance of '' ∘ shows l);
check (t = replace_at s p (r ⋅ σ)) (shows t ∘ shows '' does not contain an instance of '' ∘ shows r);
check_allm (λi. check_csteps R (fst (cs ! i) ⋅ σ) (snd (cs ! i) ⋅ σ) (pss ! i)) [0..<length cs]
}"
| "check_csteps R s t [] = check (s = t)
(shows ''empty rewrite sequence but source '' ∘ shows s ∘ shows '' and target '' ∘ shows t ∘ shows '' differ'')"
| "check_csteps R s t [p] = do {
check (cstep_src p = s) (shows (cstep_src p) ∘ shows '' does not match the source '' ∘ shows s);
check (cstep_trg p = t) (shows (cstep_trg p) ∘ shows '' does not match the target '' ∘ shows t);
check_cstep R p
}"
| "check_csteps R s t (p # ps) = do {
check (cstep_src p = s) (shows (cstep_src p) ∘ shows '' does not match the source '' ∘ shows s);
check_cstep R p;
check_csteps R (cstep_trg p) t ps
}"
lemma
fixes R :: "('f :: show, 'v :: {infinite, show}) crule list"
shows check_cstep: "isOK (check_cstep R p) ⟹ (cstep_src p, cstep_trg p) ∈ cstep (set R)"
and check_csteps: "isOK (check_csteps R s t ps) ⟹ (s, t) ∈ (cstep (set R))⇧*"
proof (induct R p and R s t ps rule: check_cstep_check_csteps.induct)
case (1 R l r cs p σ s t pss)
from 1 obtain π where *: "π ∙ ((l, r), cs) ∈ set R" by (auto elim: check_variant_in_ctrs)
from 1 have "x < length cs ⟹
(fst (cs ! x) ⋅ σ, snd (cs ! x) ⋅ σ) ∈ (cstep (set R))⇧*" for x
by (auto simp: check_eq_Inr)
then have **: "(a, b) ∈ set cs ⟹ (a ⋅ σ, b ⋅ σ) ∈ (cstep (set R))⇧*" for a b
by (metis fst_conv in_set_idx snd_conv)
from 1 show ?case using *
apply (auto simp: check_eq_Inr)
apply (intro cstepI [of "π ∙ l" "π ∙ r" "π ∙ cs" "set R" "sop (-π) ∘⇩s σ" s "ctxt_of_pos_term p s"])
by (auto simp: ** eqvt)
qed (auto simp: check_eq_Inr)
lemma check_cstep_eq_Inr:
fixes R :: "('f :: show, 'v :: {infinite, show}) crule list"
shows "check_cstep R p = Inr () ⟹ (cstep_src p, cstep_trg p) ∈ cstep (set R)"
using check_cstep [of R p] by (auto elim!: check_variant_in_ctrs)
lemma check_csteps':
fixes R :: "('f :: show, 'v :: {infinite, show}) crule list"
shows "isOK (check_csteps R s t ps) ⟹
(if ps = [] then s = t else s = cstep_src (ps ! 0) ∧ t = cstep_trg (last ps)) ∧
(∀i<length ps. (cstep_src (ps ! i), cstep_trg (ps ! i)) ∈ cstep (set R) ∧
(i < length ps - 1 ⟶ cstep_trg (ps ! i) = cstep_src (ps ! Suc i)))"
apply (induct R s t ps arbitrary: rule: check_cstep_check_csteps.induct(2))
apply simp
apply (auto simp: isOK_def check_eq_Inr check_cstep_eq_Inr check_csteps split: if_splits sum.splits)
apply (metis check_cstep_eq_Inr less_Suc0 less_antisym nth_Cons_0 nth_Cons_Suc)
apply (metis (mono_tags, lifting) One_nat_def Suc_pred check_cstep_eq_Inr less_Suc0 not_less_eq nth_Cons')
apply (case_tac i)
apply auto
done
lemma conds_sat_rel_perm:
fixes cs :: "('f, 'v::infinite) rules" and π :: "'v perm"
assumes "∀σ. (∀(u, v) ∈ set (π ∙ cs). (u ⋅ σ, v ⋅ σ) ∈ (cstep R)⇧*) ⟶ (π ∙ s ⋅ σ, π ∙ t ⋅ σ) ∈ S"
shows "∀σ. (∀(u, v) ∈ set cs. (u ⋅ σ, v ⋅ σ) ∈ (cstep R)⇧*) ⟶ (s ⋅ σ, t ⋅ σ) ∈ S"
proof (intro allI impI)
fix σ
assume "∀(u, v) ∈ set cs. (u ⋅ σ, v ⋅ σ) ∈ (cstep R)⇧*"
with assms [THEN spec, of "sop (-π) ∘⇩s σ"]
have "(π ∙ s ⋅ (sop (-π) ∘⇩s σ), π ∙ t ⋅ (sop (-π) ∘⇩s σ)) ∈ S" by (force simp: eqvt)
then show "(s ⋅ σ, t ⋅ σ) ∈ S" by auto
qed
end