theory Size_Change_Termination_Processors_Impl
imports
QTRS.QDP_Framework_Impl
"Check-NT.Q_Restricted_Rewriting_Impl"
Size_Change_Termination_Processors
Generic_Usable_Rules_Impl
Subterm_Criterion_Impl
"Check-NT.Dependency_Graph_Impl"
begin
subsection ‹Definitions of Processors›
definition check_sct_entry where
"check_sct_entry is_def S NST s t stri nstri ≡ do {
check_no_var s;
check_no_var t;
check_no_defined_root is_def t;
let m = num_args t;
let n = num_args s;
check_allm
(λi. check (i ≤ n) (''left-index to large'' +#+ shows i +@+ shows_nl))
(remdups (map fst (stri @ nstri)));
check_allm
(λj. check (j ≤ m)
(''right-index to large or argument violates usable-rules condition'' +#+ shows j))
(remdups (map snd (stri @ nstri)));
let ss = args s;
let ts = args t;
check_allm
(λ(i, j). check (isOK(S (get_arg s i, get_arg t j)))
(''problem with edge '' +#+ shows i +@+ '' -S-> '' +#+ shows j)) stri;
check_allm
(λ(i, j). check (isOK(NST (get_arg s i, get_arg t j)))
(''problem with edge '' +#+ shows i +@+ '' -NS-> '' +#+ shows j)) nstri
} <+? (λm. ''problems with DP '' +#+ shows_rule (s, t) +@+ shows_nl +@+ m)"
definition sct_entry_to_sts where
"sct_entry_to_sts s t stri nstri ≡ let
js = remdups (map snd (stri @ nstri))
in map (λ j. (s, get_arg t j)) js"
definition "fun_of_default m d ≡ let mm = map_of m in (λ i. case mm i of None ⇒ d | Some e ⇒ e)"
definition
sct_ur_af_proc ::
"('dpp, 'f, string) dpp_ops ⇒ ('f::{key,show}, string) redtriple ⇒
(('f, string) rule × ((nat × nat) list × (nat × nat) list)) list ⇒
('f, string) rules option ⇒ 'dpp ⇒
shows check"
where
"sct_ur_af_proc I rp Gs U_opt dpp ≡ do {
redtriple.valid rp;
let is_def = dpp_spec.is_defined I dpp;
let π = redtriple.af rp;
let S = redtriple.s rp;
let NS = redtriple.ns rp;
let NST = redtriple.nst rp;
let P = dpp_ops.pairs I dpp;
let GGs = filter (λ G. fst G ∈ set P) Gs; (* we filter here, so that later on the index lookup will always succeed *)
check_allm (λ (l,r). check_no_var l) (dpp_ops.rules I dpp);
check_allm (λ((s,t),(stri,nstri)). check_sct_entry is_def S NST s t stri nstri) GGs;
let sts = concat (map (λ((s,t),(stri,nstri)). sct_entry_to_sts s t stri nstri) GGs);
U ← smart_usable_rules_checker_impl I dpp π U_opt sts;
check_allm NS U
<+? (λs. ''problem when orienting usable rules'' +#+ shows_nl +@+ s);
let eidg = is_iedg_edge_dpp I dpp;
check_subseteq P (map fst Gs)
<+? (λs. ''there is no size-change graph for DP '' +#+ shows_rule s);
let n = length P;
let nums = [0 ..< n];
let numPs = zip P nums;
let num_of = fun_of_default numPs n;
check (check_SCT (λ(st,succs) (uv,_). uv ∈ set succs) (map (λ(st,(stri,nstri)).
let eidg_st = eidg st;
i = num_of st;
e = (i,map snd (filter (eidg_st o fst o fst) numPs)) in Scg e e stri nstri) GGs))
(''size-change analysis failed'' +#+ shows_nl)
} <+? (λs. ''could not apply the size-change processor with the following '' +#+ shows_nl +@+
redtriple.desc rp +@+ shows_nl +@+ ''for the following reason'' +#+ shows_nl +@+ s)
"
definition
sct_subterm_precise_proc ::
"('dpp, 'f::{key,show}, string) dpp_ops ⇒
(('f, string) rule × ((nat × nat) list × (nat × nat) list)) list ⇒
'dpp ⇒ shows check"
where
"sct_subterm_precise_proc I Gs dpp = do {
let P = dpp_ops.pairs I dpp;
let is_def = dpp_spec.is_defined I dpp;
let eidg = is_iedg_edge_dpp I dpp;
check_subseteq P (map fst Gs)
<+? (λs. ''there is no size-change graph for the pair '' +#+ shows_rule s);
let GGs = filter (λ G. fst G ∈ set P) Gs; (* we filter here, so that later on the index lookup will always succeed *)
check (dpp_ops.minimal I dpp ∨ dpp_ops.NFQ_subset_NF_rules I dpp) (shows ''minimality or innermost required'');
check_allm (λ (l,r). check_no_var l) (dpp_ops.rules I dpp);
check_allm (λ((s, t), (stri, nstri)). do {
check_no_var s;
check_no_var t;
check_no_defined_root is_def t;
let m = num_args t;
let n = num_args s;
check_allm (λ(i, j). check
(i ≤ n ∧ j ≤ m ∧ isOK (check_supt (get_arg s i) (get_arg t j)))
(''problem with edge '' +#+ shows i +@+ '' |> '' +#+ shows j +@+ shows_nl)) stri;
check_allm (λ(i, j). check
(i ≤ n ∧ j ≤ m ∧ isOK (check_supteq (get_arg s i) (get_arg t j)))
(''problem with edge '' +#+ shows i +@+ '' |>= '' +#+ shows j +@+ shows_nl)) nstri
} <+? (λm. ''problem with pair '' +#+ shows_rule (s, t) +@+ shows_nl +@+ m)) GGs;
let n = length P;
let nums = [0 ..< n];
let numPs = zip P nums;
let num_of = fun_of_default numPs n;
check (check_SCT (λ(st,succs) (uv,_). uv ∈ set succs) (map (λ (st,(stri,nstri)).
let eidg_st = eidg st;
i = num_of st;
e = (i,map snd (filter (eidg_st o fst o fst) numPs)) in Scg e e (remdups_sort stri) (remdups_sort nstri)) GGs))
(''size-change analysis failed'' +#+ shows_nl)
} <+? (λs. ''could not apply the size-change processor based on the subterm-relation''
+#+ shows_nl +@+ s)"
definition
sct_subterm_approx_proc ::
"('dpp, 'f::{key,show}, string) dpp_ops ⇒
(('f, string) rule × ((nat × nat) list × (nat × nat) list)) list ⇒
'dpp ⇒ shows check"
where
"sct_subterm_approx_proc I Gs dpp = do {
let P = dpp_ops.pairs I dpp;
let is_def = dpp_spec.is_defined I dpp;
check_subseteq P (map fst Gs)
<+? (λs. ''there is no size-change graph for the pair '' +#+ shows_rule s);
let GGs = filter (λ G. fst G ∈ set P) Gs; (* we filter here, so that later on the index lookup will always succeed *)
check (dpp_ops.minimal I dpp ∨ dpp_ops.NFQ_subset_NF_rules I dpp) (shows ''minimality or innermost required'');
check_allm (λ (l,r). check_no_var l) (dpp_ops.rules I dpp);
check_allm (λ((s, t), (stri, nstri)). do {
check_no_var s;
check_no_var t;
check_no_defined_root is_def t;
let m = num_args t;
let n = num_args s;
check_allm (λ(i, j). check
(i ≤ n ∧ j ≤ m ∧ isOK (check_supt (get_arg s i) (get_arg t j)))
(''problem with edge '' +#+ shows i +@+ '' |> '' +#+ shows j +@+ shows_nl)) stri;
check_allm (λ(i, j). check
(i ≤ n ∧ j ≤ m ∧ isOK (check_supteq (get_arg s i) (get_arg t j)))
(''problem with edge '' +#+ shows i +@+ '' |>= '' +#+ shows j +@+ shows_nl)) nstri
} <+? (λm. ''problem with pair '' +#+ shows_rule (s, t) +@+ shows_nl +@+ m)) GGs;
check (check_SCT (λ(_,g) (h,_). g = h) (remdups (map (λ (st,(stri,nstri)).
let e = (the (root (fst st)), the (root (snd st))) in Scg e e (remdups_sort stri) (remdups_sort nstri)) GGs)))
(''size-change analysis failed'' +#+ shows_nl)
} <+? (λs. ''could not apply the size-change processor based on the subterm-relation''
+#+ shows_nl +@+ s)"
definition
sct_subterm_proc ::
"('dpp, 'f::{key,show}, string) dpp_ops ⇒
(('f, string) rule × ((nat × nat) list × (nat × nat) list)) list ⇒
'dpp ⇒ shows check" where
"sct_subterm_proc I Gs dpp = (if isOK(sct_subterm_approx_proc I Gs dpp) then succeed else
sct_subterm_precise_proc I Gs dpp)"
subsection ‹Soundness Proofs›
lemma fun_of_default_index: assumes index: "indexed = zip as [0 ..< length as]"
and mem: "a ∈ set as"
shows "fun_of_default indexed d a < length as"
"as ! fun_of_default indexed d a = a"
"indexed ! fun_of_default indexed d a = (a,fun_of_default indexed d a)"
proof -
{
assume "map_of indexed a = None"
from this[unfolded map_of_eq_None_iff] mem have False
unfolding index set_conv_nth by force
}
then obtain i where i: "map_of indexed a = Some i" by auto
from map_of_SomeD[OF this, unfolded index]
have "i < length as" and "as ! i = a" unfolding set_conv_nth by auto
thus "fun_of_default indexed d a < length as"
"as ! fun_of_default indexed d a = a"
"indexed ! fun_of_default indexed d a = (a,fun_of_default indexed d a)"
using i unfolding fun_of_default_def index by auto
qed
lemma sct_subterm_precise_proc_sound: assumes I: "dpp_spec I"
and check: "isOK (sct_subterm_precise_proc I Gs d)"
shows "finite_dpp (dpp_ops.dpp I d)"
proof (rule ccontr)
interpret dpp_spec I by fact
assume not_finite: "¬ finite_dpp (dpp_ops.dpp I d)"
obtain P where P: "P = dpp_ops.pairs I d" by auto
obtain R where R: "R = dpp_ops.rules I d" by auto
obtain Q where Q: "Q = dpp_ops.Q I d" by auto
def GGs ≡ "filter (λ G. fst G ∈ set P) Gs"
let ?m = "M d"
from not_finite obtain s t σ
where mchain: "min_ichain (dpp_ops.dpp I d) s t σ" by (auto simp: finite_dpp_def)
let ?n = "length P"
def numPs ≡ "zip P [0 ..< ?n]"
let ?rd = remdups_sort
let ?entry = "λ st. (fun_of_default numPs ?n st,map snd (filter (is_iedg_edge_dpp I d st o fst o fst) numPs))"
let ?Gs = "map (λ(st, (stri, nstri)). Scg (?entry st) (?entry st) (?rd stri) (?rd nstri)) GGs"
let ?conn = "λ(st,i_st) (uv,i_uv). uv ∈ set i_st"
note check = check[unfolded sct_subterm_precise_proc_def Let_def, folded P, folded numPs_def GGs_def]
from check
have 1: "set P ⊆ fst ` set Gs ∧ check_SCT ?conn ?Gs" and nvar: "⋀ l r. (l,r) ∈ set R ⟹ is_Fun l"
and min_or_inn: "?m ∨ NF_terms (set Q) ⊆ NF_trs (set R)"
unfolding sct_subterm_precise_proc_def Let_def R Q by auto
let ?check2'' = "λf g s t stri nstri.
is_Fun s
∧ is_Fun t
∧ ¬ defined (set R) (the (root t))
∧ (∀(i, j)∈set stri.
i ≤ length (args s) ∧ j ≤ length (args t) ∧ f (get_arg s i, get_arg t j))
∧ (∀(i, j)∈set nstri.
i ≤ length (args s) ∧ j ≤ length (args t) ∧ g (get_arg s i, get_arg t j))"
let ?check2' = "?check2'' (λr. isOK (check_supt (fst r) (snd r)))
(λr. isOK (check_supteq (fst r) (snd r)))"
let ?check2 = "?check2'' (λr. r ∈ {⊳}) (λr. r ∈ {⊵})"
from check have "∀((s, t), (stri, nstri)) ∈ set GGs. ?check2' s t stri nstri"
by (force simp: sct_subterm_precise_proc_def Let_def R)
hence 2: "∀((s, t), (stri, nstri))∈set GGs. ?check2 s t stri nstri"
unfolding split_def unfolding isOK_check_supt isOK_check_supteq
unfolding fst_conv snd_conv .
let ?tuple = "λ s t. is_Fun s ∧ is_Fun t ∧ ¬ defined (set R) (the (root t))"
let ?graph = "λ s t. ∃stri nstri. (
Scg (?entry (s,t)) (?entry (s,t)) (?rd stri) (?rd nstri) ∈ set ?Gs
∧ (∀(i, j)∈set stri.
i ≤ length (args s) ∧ j ≤ length (args t) ∧ get_arg s i ⊳ get_arg t j)
∧ (∀(i, j)∈set nstri.
i ≤ length (args s) ∧ j ≤ length (args t) ∧ get_arg s i ⊵ get_arg t j))"
{
fix s t
assume memP: "(s,t) ∈ set P"
from memP 1 obtain stri nstri
where mem: "((s,t), (stri, nstri)) ∈ set Gs" by auto
with memP have memGs: "Scg (?entry (s,t)) (?entry (s,t)) (?rd stri) (?rd nstri) ∈ set ?Gs" unfolding GGs_def
by force
from mem memP and 2 have ch: "?check2 s t stri nstri" unfolding GGs_def by force
from ch have tuple: "?tuple s t" by force
from ch memGs have "?graph s t" unfolding split_def by auto
with tuple have "?tuple s t ∧ ?graph s t" by auto
}
hence tuple_graph: "∀ (s,t)∈set P. ?tuple s t ∧ ?graph s t" by auto
from tuple_graph have tuple: "∀ (s,t)∈set P. ?tuple s t" by auto
from tuple_graph have graph: "∀ (s,t)∈set P. ?graph s t" by auto
have min: "min_ichain (NFS d, ?m, set P, {}, set Q, set R, {}) s t σ"
unfolding P Q R
by (rule min_ichain_mono[OF mchain[unfolded dpp_spec_sound]], unfold dpp_spec_sound, auto)
show False
proof (rule sct_with_subterm[where info = ?entry and edg = ?conn, OF min tuple graph _ min_or_inn])
show "∀(l, r)∈set R. is_Fun l" using nvar by auto
next
fix st uv
assume mem: "(st,uv) ∈ DG (NFS d) (M d) (set P) (set Q) (set R)"
obtain s t u v where st: "st = (s,t)" "uv = (u,v)" by force
from mem[unfolded DG_def st] have mem_uv: "(u,v) ∈ set P" by auto
note * = is_iedg_edge_dpp_DG_sound[OF I mem[unfolded Q R st]]
fun_of_default_index[OF meta_eq_to_obj_eq[OF numPs_def] mem_uv]
show "?conn (?entry st) (?entry uv)" unfolding o_def st split
unfolding set_map set_filter
unfolding set_conv_nth
proof (rule image_eqI)
show "fun_of_default numPs ?n (u, v) = snd (numPs ! (fun_of_default numPs ?n (u,v)))"
using * by auto
show "numPs ! fun_of_default numPs ?n (u, v) ∈ {x ∈ {numPs ! i |i. i < length numPs}. is_iedg_edge_dpp I d (s, t) (fst (fst x))}"
by (auto intro!: exI[of _ "fun_of_default numPs ?n (u,v)"], insert *, auto simp: numPs_def)
qed
qed (insert 1, auto)
qed
lemma sct_subterm_approx_proc_sound: assumes I: "dpp_spec I"
and check: "isOK (sct_subterm_approx_proc I Gs d)"
shows "finite_dpp (dpp_ops.dpp I d)"
proof (rule ccontr)
interpret dpp_spec I by fact
assume not_finite: "¬ finite_dpp (dpp_ops.dpp I d)"
obtain P where P: "P = dpp_ops.pairs I d" by auto
obtain R where R: "R = dpp_ops.rules I d" by auto
obtain Q where Q: "Q = dpp_ops.Q I d" by auto
def GGs ≡ "filter (λ G. fst G ∈ set P) Gs"
let ?m = "M d"
from not_finite obtain s t σ
where mchain: "min_ichain (dpp_ops.dpp I d) s t σ" by (auto simp: finite_dpp_def)
let ?rd = remdups_sort
let ?entry = "λ st. (the (root (fst st)), the (root (snd st)))"
let ?Gs = "remdups (map (λ(st, (stri, nstri)). Scg (?entry st) (?entry st) (?rd stri) (?rd nstri)) GGs)"
let ?conn = "λ(_,f) (g,_). f = g"
note check = check[unfolded sct_subterm_approx_proc_def Let_def, folded P, folded GGs_def]
from check
have 1: "set P ⊆ fst ` set Gs ∧ check_SCT ?conn ?Gs" and nvar: "⋀ l r. (l,r) ∈ set R ⟹ is_Fun l"
and min_or_inn: "?m ∨ NF_terms (set Q) ⊆ NF_trs (set R)"
unfolding sct_subterm_approx_proc_def Let_def R Q by auto
let ?check2'' = "λf g s t stri nstri.
is_Fun s
∧ is_Fun t
∧ ¬ defined (set R) (the (root t))
∧ (∀(i, j)∈set stri.
i ≤ length (args s) ∧ j ≤ length (args t) ∧ f (get_arg s i, get_arg t j))
∧ (∀(i, j)∈set nstri.
i ≤ length (args s) ∧ j ≤ length (args t) ∧ g (get_arg s i, get_arg t j))"
let ?check2' = "?check2'' (λr. isOK (check_supt (fst r) (snd r)))
(λr. isOK (check_supteq (fst r) (snd r)))"
let ?check2 = "?check2'' (λr. r ∈ {⊳}) (λr. r ∈ {⊵})"
from check have "∀((s, t), (stri, nstri)) ∈ set GGs. ?check2' s t stri nstri"
by (force simp: sct_subterm_approx_proc_def Let_def R)
hence 2: "∀((s, t), (stri, nstri))∈set GGs. ?check2 s t stri nstri"
unfolding split_def unfolding isOK_check_supt isOK_check_supteq
unfolding fst_conv snd_conv .
let ?tuple = "λ s t. is_Fun s ∧ is_Fun t ∧ ¬ defined (set R) (the (root t))"
let ?graph = "λ s t. ∃stri nstri. (
Scg (?entry (s,t)) (?entry (s,t)) (?rd stri) (?rd nstri) ∈ set ?Gs
∧ (∀(i, j)∈set stri.
i ≤ length (args s) ∧ j ≤ length (args t) ∧ get_arg s i ⊳ get_arg t j)
∧ (∀(i, j)∈set nstri.
i ≤ length (args s) ∧ j ≤ length (args t) ∧ get_arg s i ⊵ get_arg t j))"
{
fix s t
assume memP: "(s,t) ∈ set P"
from memP 1 obtain stri nstri
where mem: "((s,t), (stri, nstri)) ∈ set Gs" by auto
with memP have memGs: "Scg (?entry (s,t)) (?entry (s,t)) (?rd stri) (?rd nstri) ∈ set ?Gs" unfolding GGs_def
by force
from mem memP and 2 have ch: "?check2 s t stri nstri" unfolding GGs_def by force
from ch have tuple: "?tuple s t" by force
from ch memGs have "?graph s t" unfolding split_def by auto
with tuple have "?tuple s t ∧ ?graph s t" by auto
}
hence tuple_graph: "∀ (s,t)∈set P. ?tuple s t ∧ ?graph s t" by auto
from tuple_graph have tuple: "∀ (s,t)∈set P. ?tuple s t" by auto
from tuple_graph have graph: "∀ (s,t)∈set P. ?graph s t" by auto
have min: "min_ichain (NFS d, ?m, set P, {}, set Q, set R, {}) s t σ"
unfolding P Q R
by (rule min_ichain_mono[OF mchain[unfolded dpp_spec_sound]], unfold dpp_spec_sound, auto)
show False
proof (rule sct_with_subterm[where info = ?entry and edg = ?conn, OF min tuple graph _ min_or_inn])
show "∀(l, r)∈set R. is_Fun l" using nvar by auto
next
fix st uv
assume mem: "(st,uv) ∈ DG (NFS d) (M d) (set P) (set Q) (set R)"
obtain s t u v where st: "st = (s,t)" "uv = (u,v)" by force
from mem[unfolded DG_def st] have mem_uv: "(u,v) ∈ set P" and mem_st: "(s,t) ∈ set P" by auto
from tuple mem_st obtain f ts where t: "t = Fun f ts" "¬ defined (set R) (f, length ts)" by (cases t, auto)
from tuple mem_uv obtain g us where u: "u = Fun g us" by (cases u, auto)
from mem[unfolded DG_def st] obtain σ τ where steps: "(t ⋅ σ, u ⋅ τ) ∈ (qrstep (NFS d) (set Q) (set R))⇧*" by auto
have "(t ⋅ σ, u ⋅ τ) ∈ (nrqrstep (NFS d) (set Q) (set R))⇧*"
by (rule qrsteps_imp_nrqrsteps[OF _ _ steps], insert nvar t, auto simp: applicable_rules_def defined_def)
from nrqrsteps_preserve_root[OF this]
show "?conn (?entry st) (?entry uv)" unfolding st t u by simp
qed (insert 1, auto)
qed
lemma sct_subterm_proc_sound: assumes I: "dpp_spec I"
and check: "isOK (sct_subterm_proc I Gs d)"
shows "finite_dpp (dpp_ops.dpp I d)"
using sct_subterm_approx_proc_sound[OF I, of Gs d]
sct_subterm_precise_proc_sound[OF I, of Gs d]
check unfolding sct_subterm_proc_def
by (auto split: if_splits)
lemma sct_ur_af_proc: assumes I: "dpp_spec I"
and grp: "generic_redtriple_impl grp"
and check: "isOK(sct_ur_af_proc I (grp rp) Gs U_opt d)"
shows "finite_dpp (dpp_ops.dpp I d)"
proof -
interpret dpp_spec I by fact
let ?Pd = P
let ?Rd = R
interpret generic_redtriple_impl grp by fact
show ?thesis
proof -
let ?R = "dpp_ops.rules I d"
let ?rp = "grp rp"
let ?rd = "λ x. x"
obtain strict nstrict nstrict_top π where ids: "redtriple.s ?rp = strict" and idn: "redtriple.ns ?rp = nstrict" and idnt: "redtriple.nst ?rp = nstrict_top" and idp: "redtriple.af ?rp = π" by auto
obtain P where P: "P = dpp_ops.pairs I d" by auto
obtain R where R: "R = dpp_ops.rules I d" by auto
obtain Q where Q: "Q = dpp_ops.Q I d" by auto
def GGs ≡ "filter (λ G. fst G ∈ set P) Gs"
let ?n = "length P"
def numPs ≡ "zip P [0 ..< ?n]"
let ?entry = "λ st. (fun_of_default numPs ?n st,map snd (filter (is_iedg_edge_dpp I d st o fst o fst) numPs))"
let ?Gs = "map (λ(st, (stri, nstri)). Scg (?entry st) (?entry st) (?rd stri) (?rd nstri)) GGs"
let ?conn = "λ(st,i_st) (uv,i_uv). uv ∈ set i_st"
note check = check[unfolded sct_ur_af_proc_def Let_def, folded P, folded GGs_def numPs_def, simplified, unfolded ids idn idnt idp Let_def]
let ?sts = "concat (map (λ((s,t),(stri,nstri)). sct_entry_to_sts s t stri nstri) GGs)"
let ?uchecker = "smart_usable_rules_checker_impl I d π U_opt ?sts"
from check have "isOK(?uchecker)" by simp
then obtain ur where uchecker: "?uchecker = return ur" by (cases ?uchecker, auto)
note check = check[unfolded uchecker, simplified]
let ?lhss = "concat (map (λ ((s,t),_). map (λ i. get_arg s i) [0 ..< Suc (length (args s))]) GGs)"
let ?rhss = "concat (map (λ ((s,t),_). map (λ i. get_arg t i) [0 ..< Suc (length (args t))]) GGs)"
let ?pairs = "concat (map (λ t. map (λ s. (s,t)) ?lhss) ?rhss)"
let ?stri = "filter (λ r. isOK(strict r)) ?pairs"
let ?nstri = "filter (λ r. isOK(nstrict r)) ?pairs"
let ?nstri_top = "filter (λ r. isOK(nstrict_top r)) ?pairs"
let ?cpx = "λ cm cc. isOK(redtriple.cpx ?rp cm cc)"
have stri: "isOK(check_allm strict ?stri)" by auto
from check have valid: "isOK(redtriple.valid ?rp)" and check1: "set P ⊆ fst ` set Gs"
"isOK(check_allm nstrict ur)"
"isOK(check_allm nstrict_top ?nstri_top)"
"check_SCT ?conn ?Gs"
by (auto simp: Let_def P)
from check have var: "⋀ l r. (l,r) ∈ set ?R ⟹ is_Fun l" by auto
from generate_redtriple[OF valid, simplified ids idn idnt, OF stri check1(2) check1(3)] obtain S NS NST mono_af where
redtriple: "cpx_ce_af_redtriple_order S NS NST π mono_af ?cpx" and
S: "set ?stri ⊆ S" and NS: "set ur ⊆ NS" and NST: "set ?nstri_top ⊆ NST" by (auto simp: idp)
interpret cpx_ce_af_redtriple_order S NS NST π mono_af ?cpx by fact
have ce: "ce_af_redtriple S NS NST π" ..
let ?nfs = "NFS d"
let ?m = "M d"
let ?wwf = "wwf_qtrs (set Q) (set R)"
from smart_usable_rules_checker_impl[OF I uchecker] have ur: "smart_usable_rules_checker ?nfs ?m ?wwf π (set Q) (rules d) U_opt (set ?sts) = Some ur" unfolding Q R by auto
note sct = generic_sct_redtriple[where info = ?entry and edg = ?conn and Gs = ?Gs]
note sct = sct[OF _ _ smart_usable_rules_checker NS ce _ _]
note check_sct = check1(4)
let ?check2b = "λ s t stri nstri. is_Fun s ∧ is_Fun t ∧ ¬ defined (set R) (the (root t)) ∧
(∀ i ∈ fst ` set (stri @ nstri). i ≤ length (args s)) ∧
(∀ j ∈ snd ` set (stri @ nstri). j ≤ length (args t)) ∧
(∀ (i,j) ∈ set stri. isOK(strict (get_arg s i,get_arg t j))) ∧
(∀ (i,j) ∈ set nstri. isOK(nstrict_top (get_arg s i,get_arg t j)))"
let ?check2a = "λ s t stri nstri. is_Fun s ∧ is_Fun t ∧ ¬ defined (set R) (the (root t)) ∧
(∀ i ∈ fst ` set (stri @ nstri). i ≤ length (args s)) ∧
(∀ j ∈ snd ` set (stri @ nstri). j ≤ length (args t)) ∧
(∀ (i,j) ∈ set stri. (get_arg s i,get_arg t j) ∈ S) ∧
(∀ (i,j) ∈ set nstri. (get_arg s i,get_arg t j) ∈ NST)"
let ?check2 = "λ s t stri nstri. is_Fun s ∧ is_Fun t ∧ ¬ defined (set R) (the (root t)) ∧
(∀ i ∈ fst ` set (stri @ nstri). i ≤ length (args s)) ∧
(∀ j ∈ snd ` set (stri @ nstri). j ≤ length (args t)) ∧
(∀ (i,j) ∈ set stri. (get_arg s i, get_arg t j) ∈ S) ∧
(∀ (i,j) ∈ set nstri. (get_arg s i, get_arg t j) ∈ NST)"
let ?is_def = "defined (set R)"
{
fix s t stri nstri
assume g: "((s,t),(stri,nstri)) ∈ set GGs"
with check
have "isOK(check_sct_entry ?is_def strict nstrict_top s t stri nstri)" by (auto simp: R)
hence check2b: "?check2b s t stri nstri"
unfolding check_sct_entry_def by (force simp: Let_def simp del: set_append map_append)
hence i: "⋀ ij. ij ∈ set stri ∪ set nstri ⟹ fst ij ≤ length (args s)"
and j: "⋀ ij. ij ∈ set stri ∪ set nstri ⟹ snd ij ≤ length (args t)"
by auto
{
fix i j
assume "(i,j) ∈ set stri ∪ set nstri"
from i[OF this] j[OF this] have i: "i ≤ length (args s)" and j: "j ≤ length (args t)"
by auto
from i have "i ∈ set [0 ..< Suc (length (args s))]" by auto
hence "get_arg s i ∈ set (map (get_arg s) [0..<Suc (length (args s))])" by auto
hence i: "get_arg s i ∈ set ?lhss" using g by force
from j have "j ∈ set [0 ..< Suc (length (args t))]" by auto
hence "get_arg t j ∈ set (map (get_arg t) [0..<Suc (length (args t))])" by auto
hence j: "get_arg t j ∈ set ?rhss" using g by force
from i j have "(get_arg s i, get_arg t j) ∈ set ?pairs" by (simp,blast)
} note ij_pairs = this
have stri: "∀ (i,j) ∈ set stri. (get_arg s i, get_arg t j) ∈ S"
proof (intro ballI, clarify)
fix i j
assume ij: "(i,j) ∈ set stri"
from ij check2b have ok: "isOK(strict (get_arg s i,get_arg t j))" by auto
from ij have ij: "(i,j) ∈ set stri ∪ set nstri" by auto
show "(get_arg s i, get_arg t j) ∈ S"
by (rule set_mp[OF S], insert ok ij_pairs[OF ij], simp)
qed
have nstri: "∀ (i,j) ∈ set nstri. (get_arg s i, get_arg t j) ∈ NST"
proof (intro ballI, clarify)
fix i j
assume ij: "(i,j) ∈ set nstri"
from NST have NST: "set ?nstri_top ⊆ NST" by blast
from ij check2b have ok: "isOK(nstrict_top (get_arg s i,get_arg t j))" by auto
from ij have ij: "(i,j) ∈ set stri ∪ set nstri" by auto
show "(get_arg s i, get_arg t j) ∈ NST"
by (rule set_mp[OF NST], insert ok ij_pairs[OF ij], simp)
qed
from check2b stri nstri
have check2a: "?check2a s t stri nstri" by blast
hence "?check2 s t stri nstri" by blast
} note check2 = this
let ?tuple = "λ s t. is_Fun s ∧ is_Fun t ∧ ¬ defined (set R) (the (root t))"
let ?pgraph = "λ s t stri non_stri. (
Scg (?entry (s,t)) (?entry (s,t)) (?rd stri) (?rd non_stri) ∈ set ?Gs ∧
(∀ (i,j) ∈ set stri. i ≤ length (args s) ∧ j ≤ length (args t) ∧ (get_arg s i, get_arg t j) ∈ S) ∧
(∀ (i,j) ∈ set non_stri. i ≤ length (args s) ∧ j ≤ length (args t) ∧ (get_arg s i, get_arg t j) ∈ NST))"
let ?graph = "λ s t. ∃ stri non_stri. ?pgraph s t stri non_stri"
{
fix s t
assume "(s,t) ∈ set P"
with check1 obtain stri nstri where mem: "((s,t),(stri,nstri)) ∈ set GGs" unfolding GGs_def by auto
hence memGs: "Scg (?entry (s,t)) (?entry (s,t)) (?rd stri) (?rd nstri) ∈ set ?Gs" by force
from check2[OF mem] have ch: "?check2 s t stri nstri" by blast
from ch have stri_ur: "∀ (i,j) ∈ set stri. i ≤ length (args s) ∧ j ≤ length (args t)"
unfolding is_Fun_Fun_conv by force
from ch have nstri_ur: "∀ (i,j) ∈ set nstri. i ≤ length (args s) ∧ j ≤ length (args t)"
unfolding is_Fun_Fun_conv by force
from ch have tuple: "?tuple s t" by force
from ch memGs stri_ur nstri_ur have "?pgraph s t stri nstri" by auto
hence "?graph s t" by blast
with tuple have "?tuple s t ∧ ?graph s t" by auto
}
hence tuple_graph: "∀ (s,t) ∈ set P. ?tuple s t ∧ ?graph s t" by auto
from tuple_graph have tuple: "∀ (s,t) ∈ set P. ?tuple s t" by blast
note sct = sct[OF tuple]
from tuple_graph have graph: "∀ (s,t) ∈ set P. ?graph s t" by blast
note sct = sct[unfolded R, OF var _ graph]
note sct = sct[where U_opt = U_opt]
show ?thesis unfolding dpp_spec_sound
proof (rule sct, unfold ur[symmetric] Q[symmetric] R[symmetric], simp,
rule arg_cong[where f = "smart_usable_rules_checker ?nfs ?m ?wwf π (set Q) R U_opt"],
unfold R,
unfold set_map)
note sts = sct_entry_to_sts_def[unfolded Let_def]
let ?one_cond = "λ s t j. ∃st ns. Scg (?entry (s, t)) (?entry (s, t)) st ns
∈ (λ(st, x, y). Scg (?entry st) (?entry st) (?rd x) (?rd y)) `
set GGs ∧
j ∈ snd ` set st ∪ snd ` set ns"
let ?one = "{(s, get_arg t j) | s t j . ?one_cond s t j}"
{
fix s t j
assume "?one_cond s t j"
then obtain st ns
where scg: "Scg (?entry (s,t)) (?entry (s,t)) st ns ∈ (λ(st', st, ns). Scg (?entry st') (?entry st') (?rd st) (?rd ns)) ` set GGs"
and j: "j ∈ snd ` set st ∪ snd ` set ns" by blast
{
fix s' t' st' ns'
assume mem: "((s',t'),st',ns') ∈ set GGs"
let ?zip = "zip P [0 ..< ?n]"
assume eq: "fun_of_default ?zip ?n (s,t) = fun_of_default ?zip ?n (s',t')"
from mem have "(s',t') ∈ set P" unfolding GGs_def by force
note * = fun_of_default_index[OF refl this, of ?n]
from * eq have "fun_of_default ?zip ?n (s,t) < ?n" by auto
hence "map_of ?zip (s,t) = Some (fun_of_default ?zip ?n (s,t))"
unfolding fun_of_default_def by (cases "map_of ?zip (s,t)", auto)
from map_of_SomeD[OF this, unfolded eq, unfolded set_zip] *
have "(s,t) = (s',t')" by auto
hence "s = s'" "t = t'" by auto
}
with scg have scg: "((s,t),?rd st,?rd ns) ∈ set GGs" unfolding numPs_def
by auto
have "(s, get_arg t j) ∈ set ?sts" unfolding set_concat set_map
by (rule, rule, rule scg, unfold sts, insert j, auto)
}
hence one: "?one ⊆ set ?sts" by blast
{
fix s tj
assume "(s,tj) ∈ set ?sts"
from this[unfolded sts] obtain t st ns j where
mem: "((s,t),st,ns) ∈ set GGs" and j: "j ∈ snd ` set st ∪ snd ` set ns" and tj: "tj = get_arg t j"
by force
have "(s,tj) ∈ ?one" unfolding tj
by (rule, intro exI conjI, rule refl, rule image_eqI[OF _ mem], insert j, auto)
}
hence two: "set ?sts ⊆ ?one" ..
from one two show "?one = set ?sts" by blast
next
show "set P = set (?Pd d) ∪ set (Pw d)" unfolding P by simp
next
show "set (rules d) = set (?Rd d) ∪ set (Rw d)" by simp
next
fix st uv
assume mem: "(st,uv) ∈ DG (NFS d) (M d) (set P) (set Q) (set (rules d))"
obtain s t u v where st: "st = (s,t)" "uv = (u,v)" by force
from mem[unfolded DG_def st] have mem_uv: "(u,v) ∈ set P" by auto
note * = is_iedg_edge_dpp_DG_sound[OF I mem[unfolded Q R st]]
fun_of_default_index[OF meta_eq_to_obj_eq[OF numPs_def] mem_uv]
show "?conn (?entry st) (?entry uv)" unfolding o_def st split
unfolding set_map set_filter
unfolding set_conv_nth
proof (rule image_eqI)
show "fun_of_default numPs ?n (u, v) = snd (numPs ! (fun_of_default numPs ?n (u,v)))"
using * by auto
show "numPs ! fun_of_default numPs ?n (u, v) ∈ {x ∈ {numPs ! i |i. i < length numPs}. is_iedg_edge_dpp I d (s, t) (fst (fst x))}"
by (auto intro!: exI[of _ "fun_of_default numPs ?n (u,v)"], insert *, auto simp: numPs_def)
qed
qed (insert check_sct, auto)
qed
qed
end