theory Unraveling_Impl
imports
Unraveling
Conditional_Rewriting_Impl
QTRS.QDP_Framework_Impl
begin
definition create_ctxts :: "('f, 'v) rules ⇒ (nat ⇒ ('f, 'v) ctxt) option"
where
"create_ctxts R =
(case R of
[] ⇒ None
| Cons l RR ⇒ do {
cs ← Option_Monad.mapM (λ(l, r).
(case l of
Fun U (t # ts) ⇒ Some (More U [] □ ts)
| _ ⇒ None)) RR;
let n = length cs;
Some (λi. if i < length cs then cs ! i else □) })"
definition
create_U ::
"(('f, 'v) crule × ('f, 'v) rules) list ⇒ (('f, 'v) crule ⇒ nat ⇒ ('f, 'v) ctxt) option"
where
"create_U c_rs = do {
cr_ctxts ← Option_Monad.mapM (λ (cr, rs). do {
guard (length rs = Suc (length (snd cr)));
ctxt ← create_ctxts rs;
Some (cr, ctxt)
}) c_rs;
let m = map_of cr_ctxts;
Some (λ cr. case m cr of None ⇒ (λ _. □) | Some ctxt ⇒ ctxt)
}"
declare unraveling.lhs_n.simps[code] unraveling.rhs_n.simps[code]
definition
rules_impl :: "(('f, 'v) crule ⇒ nat ⇒ ('f, 'v) ctxt) ⇒ ('f, 'v) crule ⇒ ('f, 'v) rules"
where
"rules_impl U cr = map (λi.
(unraveling.lhs_n U cr i, unraveling.rhs_n U cr i)) [0 ..< Suc (length (snd cr))]"
lemma rules_impl[simp]: "set (rules_impl U cr) = unraveling.rules U cr"
proof -
interpret unraveling "{}" U .
obtain n where n: "Suc (length (snd cr)) = n" by auto
have "{0..<Suc (length (snd cr))} = {i. i < Suc (length (snd cr))}" (is "?l = _")
unfolding n by auto
also have "... = {i. i ≤ length (snd cr)}" (is "_ = ?r") by auto
finally have id: "?l = ?r" .
show ?thesis unfolding rules_def rules_impl_def
by (simp del: upt_Suc add: id)
qed
definition check_unraveling :: "(('f :: show,'v :: show)crule × ('f,'v)rules)list ⇒ ('f,'v)crules ⇒ ('f,'v)rules result"
where "check_unraveling c_rs ctrs ≡ do {
check_subseteq ctrs (map fst c_rs) <+?
(λ cr. shows ''did not find rule '' +@+ shows_crule cr +@+ shows_nl);
U ← case create_U c_rs of None ⇒ error (shows ''unable to extract unraveling contexts'') | Some U ⇒ return U;
check_allm (λ (c,rs). check (rules_impl U c = rs) (shows ''problem with rules of '' +@+ shows_crule c +@+ shows_nl)) c_rs;
return (concat (map snd c_rs))
} <+? (λ e. shows ''problem in unraveling '' +@+ shows_nl +@+ e)"
lemma check_unraveling:
assumes ok: "check_unraveling c_rs ctrs = return r"
and SN: "SN (rstep (set r))"
shows "quasi_reductive (set ctrs)"
proof -
note ok = ok[unfolded check_unraveling_def, simplified]
from ok obtain U where U: "create_U c_rs = Some U" by (cases "create_U c_rs", auto)
note ok = ok[unfolded U, simplified]
from ok have r: "r = concat (map snd c_rs)" by simp
interpret unraveling "set ctrs" U .
show ?thesis
proof (rule SN_quasi_reductive, rule SN_subset[OF SN rstep_mono])
show "UR ⊆ set r"
proof(rule subsetI)
fix lr
assume lr: "lr ∈ UR"
from this[unfolded UR_def] obtain cr where cr: "cr ∈ set ctrs"
and lr: "lr ∈ rules cr" by auto
from ok cr obtain rs where mem: "(cr,rs) ∈ set c_rs" by auto
from ok mem have "rules_impl U cr = rs" by auto
from arg_cong[OF this, of set] have "rules cr = set rs" by simp
with lr have lr: "lr ∈ set rs" by auto
with mem show "lr ∈ set r" unfolding r by force
qed
qed
qed
definition check_Z_vars :: "('f :: show,'v :: show) crules ⇒ (('f, 'v) crule ⇒ nat ⇒ 'v list) ⇒ shows check"
where
"check_Z_vars crs Z = do {
check_allm
(λcr .
check_allm
(λi. do {
check_subseteq (list_inter (X_impl cr i) (Y_impl cr i)) (Z cr i)
<+? (λx. ''Variable '' +#+ shows x +@+ '' does not occur in variable list of '' +#+ shows (Suc i) +@+ ''. U-symbol'' +#+ shows_nl);
check (distinct (Z cr i))
('' variables in additional arguments of U-symbols are not distinct. '' +#+ shows_nl)
} <+? (λe. ''conditions for variable-lists in U-symbols for '' +#+ shows_crule cr +@+ '' are violated.'' +#+ shows_nl +@+ e)
) [0..<length (snd cr)]
) crs
} <+? (λe. ''The CTRS does not fulfill the condition on Z variables. '' +#+ shows_nl +@+ e)"
lemma check_Z_vars[simp]:
"isOK (check_Z_vars c_rs Z) = unraveling.Z_vars (set c_rs) Z"
by (simp add: check_Z_vars_def unraveling.Z_vars_def Y_impl atLeast0LessThan) (blast)
definition create_zs :: "('f, 'v) rules ⇒ (nat ⇒ 'v list) option"
where
"create_zs R =
(case R of
[] ⇒ None
| Cons l RR ⇒ do {
cs ← Option_Monad.mapM (λ(l, r).
(case l of
Fun U (t # ts) ⇒ Some (map the_Var ts)
| _ ⇒ None)) RR;
Some (λi. if i < length cs then (cs ! i) else [])})"
definition create_Z :: "(('f, 'v) crule × ('f, 'v) rules) list ⇒ (('f, 'v) crule ⇒ nat ⇒ 'v list) option"
where "create_Z c_rs = do {
cr_zs ← Option_Monad.mapM (λ (cr, rs). do {
zs ← create_zs rs;
Some (cr, zs)
}) c_rs;
let mc = map_of cr_zs;
Some (λ cr. case mc cr of None ⇒ (λ _. []) | Some zs ⇒ zs)
}"
definition create_Umap_cr :: "('f, 'v) crule ⇒ ('f, 'v) rules ⇒ (('f × (('f, 'v) crule × nat)) list) option"
where "create_Umap_cr cr R = (case R of
[] ⇒ None
| Cons l RR ⇒ Option_Monad.mapM (λ((l, r), i).
(case l of Fun U (t # ts) ⇒ Some (U,(cr,i)) | _ ⇒ None)) (zip RR [0..<length RR])) "
definition create_Umap :: "(('f, 'v) crule × ('f, 'v) rules) list ⇒ ('f ⇒ (('f, 'v) crule × nat) option)"
where "create_Umap c_rs = ( case Option_Monad.mapM (λ (cr, rs). create_Umap_cr cr rs) c_rs of
None ⇒ (λ _ .None) | Some u ⇒ map_of (concat u))"
abbreviation si :: "('f,'v) crule ⇒ nat => ('f,'v) term" where "si ρ i ≡ fst ((snd ρ)!i)"
abbreviation ti :: "('f,'v) crule ⇒ nat => ('f,'v) term" where "ti ρ i ≡ snd ((snd ρ)!i)"
definition check_prefix_equivalent :: "('f::show, 'v::show) crule ⇒ ('f, 'v) crule ⇒ nat ⇒ shows check"
where "check_prefix_equivalent ρ ρ' n = do {
check (n < length (snd ρ)) (''There are fewer than '' +#+ shows n +@+ '' conditions in '' +#+ shows_crule ρ);
check (n < length (snd ρ')) (''There are fewer than '' +#+ shows n +@+ '' conditions in '' +#+ shows_crule ρ');
check (fst (fst ρ) = fst (fst ρ')) (shows ''Left-hand sides are different.'');
check_allm
(λi. check (ti ρ i = ti ρ' i) (''Rhs of conditions are different ''+#+ shows_nl))
[0..<n];
check_allm
(λi. check (si ρ i = si ρ' i) (''Lhs of conditions are different ''+#+ shows_nl))
[0..<Suc n]
} <+? (λe. ''Rules'' +#+ shows_crule ρ +@+ '' and '' +#+ shows_crule ρ' +@+ '' are not '' +#+ shows n +@+ '' equivalent.'' +#+ shows_nl +@+ e)"
lemma prefix_equivalent:
"isOK(check_prefix_equivalent ρ ρ' n) = prefix_equivalent ρ ρ' n"
unfolding prefix_equivalent_def check_prefix_equivalent_def isOK_update_error
isOK_bind isOK_check isOK_forallM set_upt by fastforce
definition check_f ::
"('f, 'v) crule ⇒ nat ⇒ 'f ⇒ ('f::show, 'v::show) crule list ⇒ (('f, 'v) crule ⇒ nat ⇒ ('f, 'v) ctxt) ⇒ shows check"
where "check_f cr' j f crs U =
check_allm
(λcr.
check_allm
(λi.
case U (cr:: ('f, 'v) crule) (i::nat) of More g b c aft ⇒ (
if f = g then ( do{
check (i = j) (''Same symbol occurs at different levels'' +#+ shows_nl);
check_allm (λk. check (U cr k = U cr' k) (''Contexts are different ''+#+ shows_nl)) [0..< Suc j];
check_prefix_equivalent cr cr' j} <+? (λe. ''Rules'' +#+ shows_crule cr +@+ '' and '' +#+ shows_crule cr' +@+ '' share a symbol.'' +#+ shows_nl +@+ e))
else succeed)
| _ ⇒ succeed
) [0..<length (snd cr)]
) crs"
lemma check_f:
"isOK(check_f ρ j f crs (U:: (('f, 'v) crule ⇒ nat ⇒ ('f::show, 'v::show) ctxt))) =
(∀ ρ' n' g b c a. (ρ' ∈ (set crs) ∧ n' < length (snd ρ') ∧ U ρ' n' = More g b c a) ⟶
f ≠ g ∨ (j = n' ∧ (∀i ≤j. U ρ i = U ρ' i) ∧ prefix_equivalent ρ' ρ j))"
proof-
let ?check = "λ cr' j cr i . case U cr i of More g b c aft ⇒ (
if f = g then ( do{
check (i = j) (''Same symbol occurs at different levels'' +#+ shows_nl);
check_allm (λk. check (U cr k = U cr' k) (''Contexts are different ''+#+ shows_nl)) [0..<Suc j];
check_prefix_equivalent cr cr' j} <+? (λe. ''Rules'' +#+ shows_crule cr +@+ '' and '' +#+ shows_crule cr' +@+ '' share a symbol.'' +#+ shows_nl +@+ e))
else succeed)
| _ ⇒ succeed"
{ fix cr ::"('f,'v) crule" fix cr' i j
let ?check = "?check cr' j cr i"
have aux:"⋀P j. (∀x∈set [0..<Suc j]. P x) = (∀x ≤ j. P x)" by auto
have "isOK (?check) = (∀ g b c a. ( U cr i = More g b c a) ⟶ f ≠ g ∨ (j = i ∧ (∀i ≤j. U cr i = U cr' i) ∧ prefix_equivalent cr cr' j))"
proof(cases "U cr i", simp)
case (More g b c a)
thus ?thesis unfolding More ctxt.split isOK_error is_OK_if_return(2)
unfolding isOK_update_error isOK_bind isOK_check isOK_forallM prefix_equivalent aux by auto
qed
} note aux = this
have aux':"⋀P j. (∀x∈set [0..<j]. P x) = (∀x < j. P x)" by auto
{fix cr cr' j
have "isOK(check_allm (λi. ?check cr' j cr i ) [0..<length (snd cr)]) =
(∀ n' g b c a. (n' < length (snd cr) ∧ U cr n' = More g b c a) ⟶
f ≠ g ∨ (j = n' ∧ (∀i ≤j. U cr i = U cr' i) ∧ prefix_equivalent cr cr' j))"
unfolding isOK_update_error isOK_forallM aux aux' by blast
} note * = this
show ?thesis unfolding check_f_def isOK_update_error unfolding isOK_forallM * by metis
qed
definition check_U_cond ::
"(('f::show, 'v::show) crule ⇒ nat ⇒ ('f, 'v) ctxt) ⇒ ('f, 'v) crule list ⇒ 'f list ⇒ (('f, 'v) crule ⇒ nat ⇒ 'v list) ⇒ shows check"
where "check_U_cond U crs F Z = do {
check_allm
(λcr .
check_allm
(λi. (case U cr i of
More f [] □ aft ⇒ do {
(*check (Umap f = Some (cr,i)) (shows '' The internally generated symbol map does not match. '');*)
check_disjoint [f] F <+? (λx. ''The function symbol '' +#+ show f +#+ '' is not fresh. '' +#+ shows_nl);
check (aft = map Var (Z cr i)) (shows '' U does not map to Z vars '');
check_f cr i f crs U
} <+? (λe. ''Conditions for '' +#+ shows_crule cr +@+ '' at '' +#+ shows i +@+ '' are violated.'' +#+ shows_nl +@+ e)
| _ ⇒ error (shows '' Unexpected empty context.'')
)) [0..<length (snd cr)]
) crs
} <+? (λe. ''The CTRS does not fulfill the condition on the U symbols.'' +#+ shows_nl +@+ e)"
lemma pe:"prefix_equivalent cr cr' n = prefix_equivalent cr' cr n"
unfolding prefix_equivalent_def by fastforce
lemma check_U_cond[simp]:
"isOK(check_U_cond U crs F Z) = U_cond U (set crs) (set F) Z" (is "?check = ?sem")
proof -
let ?U = "λ ρ n. (∃ f. (U ρ n = (More f Nil Hole (map Var (Z ρ n))) ∧ f ∉ (set F) ∧
(∀ ρ' n' g b c a. (ρ' ∈ (set crs) ∧ n' < length (snd ρ') ∧ U ρ' n' = More g b c a) ⟶
f ≠ g ∨ (n = n' ∧ (∀i ≤n. U ρ i = U ρ' i) ∧ prefix_equivalent ρ ρ' n))))"
let ?C = "λ cr i. case U cr i of
More f [] □ aft ⇒ do {
check_disjoint [f] F <+? (λx. ''The function symbol '' +#+ show f +#+ '' is not fresh. '' +#+ shows_nl);
check (aft = map Var (Z cr i)) (shows '' U does not map to Z vars '');
check_f cr i f crs U
} <+?(λe. ''Conditions for '' +#+ shows_crule cr +@+ '' at '' +#+ shows i +@+ '' are violated.'' +#+ shows_nl +@+ e)
| _ ⇒ error (shows '' Unexpected empty context.'')"
show ?thesis
proof
assume ?check
show ?sem
proof (rule U_condI)
fix cr i
assume cr: "cr ∈ set crs" and i: "i < length (snd cr)"
with ‹?check› have ok: "isOK(?C cr i)" unfolding check_U_cond_def by auto
hence "∃f b c a. U cr i = More f b c a" using isOK_error by (cases "U cr i", auto)
then obtain f b c a where 0:"U cr i = More f b c a" by blast
from ok[unfolded 0] isOK_error have b:"b=[]" by (cases b, auto)
from ok[unfolded 0 b, simplified] isOK_error ctxt.exhaust have c:"c=□" by (cases c, auto)
note ok = ok[unfolded 0[unfolded b c], simplified]
note 2 = conjunct1[OF conjunct2[OF ok]]
from ok have a:"a = map Var (Z cr i)" by auto
from conjunct2[OF conjunct2[OF ok], unfolded check_f] conjunct1[OF ok]
0[unfolded a b c] 2 pe
show "?U cr i" by blast
qed
next
assume ?sem
show ?check unfolding check_U_cond_def isOK_forallM isOK_update_error set_upt
proof (intro ballI)
fix cr i
assume cr: "cr ∈ set crs" and "i ∈ {0..<length (snd cr)}"
hence i: "i < length (snd cr)" by auto
let ?A = "λf. U cr i = More f [] □ (map Var (Z cr i))"
let ?C' = "λf. f ∉ set F"
let ?D = "λf. (∀ ρ' n' g b c a. (ρ' ∈ (set crs) ∧ n' < length (snd ρ') ∧ U ρ' n' = More g b c a) ⟶
f ≠ g ∨ (i = n' ∧ (∀j ≤i. U cr j = U ρ' j) ∧ prefix_equivalent cr ρ' i))"
from U_condD[OF ‹?sem› cr i] obtain f where "?A f ∧ ?C' f ∧ ?D f" by blast
hence A:"?A f" and C:"?C' f" and D:"?D f" by (fast+)
from D pe have 4:"isOK (check_f cr i f crs U)" unfolding check_f by blast
from C 4 show "isOK (?C cr i)" unfolding A ctxt.case list.case by force
qed
qed
qed
definition check_source_preserving ::
"('f::show, 'v::show) crules ⇒ (('f, 'v) crule ⇒ nat ⇒ 'v :: show list) ⇒ shows check"
where "check_source_preserving crs (Zv :: (('f, 'v) crule ⇒ nat ⇒ 'v list)) =
check_allm
(λcr.
check_allm
(λi.
check_subseteq (vars_term_list (fst (fst cr))) (Zv cr i) <+?
(λ x. shows ''Some variable in lhs does not occur in Z_'' +@+ shows i +@+ shows ''. ⏎'' )
<+? (λe. ''The unraveling is not source preserving for rule '' +#+ shows_crule cr +@+ shows_nl +@+ e)
) [0..<length (snd cr)]
) crs"
lemma source_preserving [simp]:
"isOK (check_source_preserving crs Z) = source_preserving (set crs) Z"
unfolding source_preserving_def check_source_preserving_def by force
definition check_sp_unraveling :: "(('f :: show,'v :: show)crule × ('f,'v)rules)list ⇒ ('f::show,'v::show)crules ⇒ ('f,'v)rules result"
where
"check_sp_unraveling c_rs ctrs = do {
check_same_set ctrs (map fst c_rs) <+? (λ cr. shows ''did not find rule '' +@+ shows_crule cr +@+ shows_nl);
U ← case create_U c_rs of None ⇒ error (shows ''unable to extract unraveling contexts'') | Some U ⇒ return U;
Z ← case create_Z c_rs of None ⇒ error (shows ''unable to extract Z variables'') | Some Z ⇒ return Z;
Umap ← return (create_Umap c_rs);
check_U_cond U ctrs (funs_ctrs_list ctrs) Z;
check_Z_vars ctrs Z;
check_dctrs ctrs;
check_type3 ctrs;
check_allm (λ (c,rs). check (rules_impl U c = rs) (shows ''problem with rules of '' +@+ shows_crule c +@+ shows_nl)) c_rs;
check_left_linear_trs (concat (map snd c_rs)) <+? (λ e. shows ''the unraveled TRS is not left-linear '' +@+ shows_nl +@+ e);
check_wf_ctrs ctrs <+? (λ e. shows ''the CTRS is not well-formed '' +@+ shows_nl +@+ e);
check_source_preserving ctrs Z <+? (λ e. shows ''unraveling is not source preserving '' +@+ shows_nl +@+ e);
return (concat (map snd c_rs))
} <+? (λe. ''preconditions on the unraveling are not satisfied'' +#+ shows_nl +@+ e)"
lemma check_sp_unraveling_CR:
assumes ok: "check_sp_unraveling c_rs ctrs = return (ur :: ('f :: show, string) rules)"
and inf: "infinite (UNIV :: 'f set)"
and CR: "CR (rstep (set (ur :: ('f :: show, string) rules)))"
shows "CR (cstep (set ctrs))"
proof -
note ok = ok[unfolded check_sp_unraveling_def, simplified]
from ok obtain U where U: "create_U c_rs = Some U" by (cases "create_U c_rs", auto)
from ok obtain Z where Z: "create_Z c_rs = Some Z" by (cases "create_Z c_rs", auto)
note ok = ok[unfolded U Z, simplified]
from ok have ur: "ur = concat (map snd c_rs)" by simp
from ok source_preserving have z:"source_preserving (set ctrs) Z" by auto
from ok check_left_linear_trs have ll:"left_linear_trs (set ur)" by auto
from ok have wf:"wf_ctrs (set ctrs)" by auto
from ok have U_cond: "U_cond U (set ctrs) (funs_ctrs (set ctrs)) Z" by auto
interpret unraveling "set ctrs" U .
have ur1:"UR ⊆ set ur"
proof(rule subsetI)
fix lr
assume lr: "lr ∈ UR"
from this[unfolded UR_def] obtain cr where cr: "cr ∈ set ctrs"
and lr: "lr ∈ rules cr" by auto
from ok cr obtain rs where mem: "(cr,rs) ∈ set c_rs" by auto
from ok mem have "rules_impl U cr = rs" by auto
from arg_cong[OF this, of set] have "rules cr = set rs" by simp
with lr have lr: "lr ∈ set rs" by auto
with mem show "lr ∈ set ur" unfolding ur by force
qed
have ur2:"UR ⊇ set ur"
proof(rule subsetI)
fix lr
assume lr: "lr ∈ set ur"
from this[unfolded ur set_concat set_map] have "∃(cr,rs) ∈ set c_rs. lr ∈ set rs" by fastforce
then obtain cr rs where mem:"(cr,rs) ∈ set c_rs" "lr ∈ set rs" by blast
with ok have a:"∀x∈set c_rs. case x of (c, rs) ⇒ rules_impl U c = rs" by meson
from imageI[OF mem(1), of fst] conjunct1[OF ok] have mem':"cr ∈ set ctrs" by simp
from a[rule_format, OF mem(1), unfolded split] mem(2) have "lr ∈ rules cr" by force
with mem' show "lr ∈ UR" unfolding UR_def by blast
qed
with ur1 have ur:"UR = set ur" by auto
show ?thesis
proof (rule CR_imp_CR)
show "infinite (UNIV :: string set)" by (rule infinite_UNIV_listI)
show "infinite (UNIV :: 'f set)" by (rule inf)
qed (insert ur z ll CR wf ok, auto)
qed
hide_const (open) rules_impl create_U create_zs create_Z U_cond check_U_cond check_Z_vars
check_f si ti
end