theory SCNP_Impl
imports
SCNP
"Check-NT.Term_Order_Impl"
List_Order_Impl
QTRS.Trs_Impl
QTRS.Map_Choice
begin
hide_const (open) Almost_Full.af
type_synonym 'f scnp_af = "(('f × nat) × (nat × nat) list) list"
lemma check_scnp_af:
assumes rt: "ce_af_redtriple_order S NS NST π"
and ext: "list_order_extension s_ext ns_ext"
shows "ce_af_scnp S NS NST s_ext ns_ext π"
proof -
from rt interpret ce_af_redtriple_order S NS NST π .
from ext interpret list_order_extension s_ext ns_ext .
show ?thesis ..
qed
definition scnp_desc :: "('f :: show) scnp_af ⇒ string ⇒ shows"
where
"scnp_desc af mu =
shows ''SCNP-version with mu = '' ∘ shows mu ∘ shows '' and the level mapping defined by '' ∘ shows_nl ∘
shows_sep (λ((f, n), as). shows ''pi('' ∘ shows f ∘ shows '') = '' ∘
showsp_list (λ _ (p, l).
shows ''('' ∘ (if p < n then shows (Suc p) else shows ''epsilon'') ∘
shows '','' ∘ shows l ∘ shows '')'') 0 as)
shows_nl af ∘ shows_nl"
definition scnp_arity :: "'f scnp_af ⇒ nat"
where
"scnp_arity af = max_list (map (λ (fi,ijs). length ijs) af)"
definition label_s_ns_impl :: "(('f :: show, 'v :: show)rule ⇒ shows check)
⇒ (('f :: show, 'v :: show)rule ⇒ shows check) ⇒ ('f,'v)term × nat
⇒ ('f,'v)term × nat ⇒ bool × bool"
where "label_s_ns_impl cS cNS s t ≡ case s of (s',i) ⇒ case t of (t',j) ⇒
if isOK(cS (s',t')) then (True,True) else
if isOK(cNS (s',t')) then (i > j, i ≥ j) else (False, False)"
abbreviation fun_to_rel :: "('a ⇒ 'a ⇒ bool) ⇒ 'a rel" where
"fun_to_rel f ≡ {(a,b). f a b}"
lemma label_s_impl: assumes "isOK(cS (s,t)) ⟹ S s t"
and "isOK(cNS (s,t)) ⟹ NS s t"
and "fst (label_s_ns_impl cS cNS (s,i) (t,j))"
shows "((s,i), (t,j)) ∈ lex_two (fun_to_rel S) (fun_to_rel NS) (fun_to_rel (op >))"
using assms unfolding label_s_ns_impl_def split
by (cases "isOK(cS (s,t))", simp, cases "isOK(cNS (s,t))", auto)
lemma label_ns_impl: assumes "isOK(cS (s,t)) ⟹ S s t"
and "isOK(cNS (s,t)) ⟹ NS s t"
and "snd (label_s_ns_impl cS cNS (s,i) (t,j))"
shows "((s,i), (t,j)) ∈ lex_two (fun_to_rel S) (fun_to_rel NS) (fun_to_rel (op ≥))"
using assms unfolding label_s_ns_impl_def split
by (cases "isOK(cS (s,t))", simp, cases "isOK(cNS (s,t))", auto)
definition NST_label_mul_impl :: "(('f,'v)term × nat) list_ext_impl
⇒ (('f × nat) ⇒ (nat × nat)list)
⇒ (('f, 'v)rule ⇒ shows check)
⇒ (('f, 'v)rule ⇒ shows check)
⇒ ('f :: show ,'v :: show)rule ⇒ shows check"
where "NST_label_mul_impl list_ext af cS cNS st ≡
case st of (Fun f ss, Fun g ts) ⇒ check (snd (list_ext (label_s_ns_impl cS cNS) (lterms af (Fun f ss)) (lterms af (Fun g ts))))
(shows ''cannot orient pair '' +@+ shows_rule st +@+ shows '' weakly:'' +@+ shows_nl
+@+ shows (lterms af (Fun f ss)) +@+ shows '' >=mu '' +@+ shows (lterms af (Fun g ts)) +@+ shows '' could not be ensured'')
| _ ⇒ error (shows ''roots of '' +@+ shows_rule st +@+ shows '' must be non-variable'')"
definition S_label_mul_impl :: "(('f,'v)term × nat) list_ext_impl
⇒ (('f × nat) ⇒ (nat × nat)list)
⇒ (('f, 'v)rule ⇒ shows check)
⇒ (('f, 'v)rule ⇒ shows check)
⇒ ('f :: show ,'v :: show)rule ⇒ shows check"
where "S_label_mul_impl list_ext af cS cNS st ≡
case st of (Fun f ss, Fun g ts) ⇒ check (fst (list_ext (label_s_ns_impl cS cNS) (lterms af (Fun f ss)) (lterms af (Fun g ts))))
(shows ''cannot orient pair '' +@+ shows_rule st +@+ shows '' strictly:'' +@+ shows_nl
+@+ shows (lterms af (Fun f ss)) +@+ shows '' >mu '' +@+ shows (lterms af (Fun g ts)) +@+ shows '' could not be ensured'')
| _ ⇒ error (shows ''roots of '' +@+ shows_rule st +@+ shows '' must be non-variable'')"
definition generate_scnp_rp :: "(('f,'v)term × nat) list_ext_impl ⇒ string ⇒ 'f scnp_af ⇒ ('a ⇒ ('f :: {key,show},'v :: show)redtriple) ⇒ 'a ⇒ ('f,'v)root_redtriple"
where "generate_scnp_rp list_ext list_ext_name af rti x ≡
let rt = rti x;
af' = fun_of_map (ceta_map_of af) [];
pi = redtriple.af rt;
cS = redtriple.s rt;
cNS = redtriple.ns rt
in ⦇ root_redtriple.valid = redtriple.valid rt,
s = S_label_mul_impl list_ext af' cS cNS,
ns = redtriple.ns rt,
nst = NST_label_mul_impl list_ext af' cS cNS,
af = pi,
aft = scnp_af_to_af af' pi,
desc = scnp_desc af list_ext_name +@+ redtriple.desc rt ⦈"
lemma generate_scnp_rp: assumes "generic_redtriple_impl (rti :: ('a ⇒ ('f ::{show,key},'v ::show)redtriple))"
and list_ext: "∃ s_ext ns_ext. list_order_extension_impl s_ext ns_ext list_ext"
shows "generic_root_redtriple_impl (generate_scnp_rp list_ext list_ext_name af rti)"
proof
fix rp :: 'a and s_list ns_list nst_list :: "('f,'v)rule list"
let ?rp = "generate_scnp_rp list_ext list_ext_name af rti rp :: ('f,'v)root_redtriple"
let ?rp' = "rti rp"
let ?π = "redtriple.af ?rp'"
let ?af = "fun_of_map (ceta_map_of af) []"
let ?cpx = "redtriple.cpx (rti rp)"
let ?cpx' = "λ cm cc. isOK(?cpx cm cc)"
from list_ext obtain s_ext ns_ext where "list_order_extension_impl s_ext ns_ext list_ext" by blast
then interpret list_order_extension_impl s_ext ns_ext list_ext .
have list_ext: "list_order_extension s_ext ns_ext" ..
note gdef = generate_scnp_rp_def[of list_ext list_ext_name af rti rp, unfolded Let_def]
assume v: "isOK( root_redtriple.valid ?rp)" and S: "isOK(check_allm (root_redtriple.s ?rp) s_list)"
and NS: "isOK(check_allm (root_redtriple.ns ?rp) ns_list)"
and NST: "isOK(check_allm (root_redtriple.nst ?rp) nst_list)"
from v[unfolded gdef] have v: "isOK(redtriple.valid ?rp')" by auto
let ?cs = "redtriple.s ?rp'"
let ?cns = "redtriple.ns ?rp'"
let ?cS = "S_label_mul_impl list_ext ?af ?cs ?cns"
from NS have NS: "isOK(check_allm ?cns ns_list)" unfolding gdef by auto
from S have S': "isOK(check_allm ?cS s_list)" unfolding gdef by auto
let ?cNST = "NST_label_mul_impl list_ext ?af ?cs ?cns"
from NST have NST': "isOK(check_allm ?cNST nst_list)" unfolding gdef by auto
interpret generic_redtriple_impl rti by fact
obtain all where all: "all = s_list @ nst_list" by auto
let ?all = "(concat o concat) (map (λ(s,t). map (λ si. map (Pair si) (map fst (lterms ?af t ))) (map fst (lterms ?af s))) all)"
let ?ns = "filter (λ sitj. isOK(?cns sitj)) ?all"
let ?nss = "ns_list @ ?ns"
let ?s = "filter (λ sitj. isOK(?cs sitj)) ?all"
have S: "isOK (check_allm ?cs ?s)" by auto
have NS: "isOK (check_allm ?cns ?nss)" using NS by auto
from generate_redtriple[OF v S NS, of Nil]
obtain S NS NST mono_af
where ce_af: "cpx_ce_af_redtriple_order S NS NST ?π mono_af ?cpx'"
and S: "set ?s ⊆ S"
and NS: "set ?ns ⊆ NS"
and NS2: "set ns_list ⊆ NS" by auto
have pi: "root_redtriple.af ?rp = ?π" unfolding gdef by simp
interpret foo: cpx_ce_af_redtriple_order S NS NST ?π mono_af ?cpx' by fact
have ce_af: "ce_af_redtriple_order S NS NST ?π" ..
from check_scnp_af[OF ce_af list_ext]
interpret ce_af_scnp S NS NST ?af s_ext ns_ext ?π .
{
fix f ss g ts si i tj j
assume mem: "(Fun f ss,Fun g ts) ∈ set all" and
mems: "(si,i) ∈ set (lterms ?af (Fun f ss))" and
memt: "(tj,j) ∈ set (lterms ?af (Fun g ts))"
have id: "(si,tj) = (si, fst (tj,j))" by simp
have all: "(si,tj) ∈ set ?all" unfolding o_def set_concat set_map
by (rule, rule, rule, rule mem, unfold set_map map_map o_def, rule, rule refl, rule mems, unfold set_map fst_conv, rule,
rule id, rule memt)
have "isOK(?cs (si,tj)) ⟹ (si,tj) ∈ S" "isOK(?cns (si,tj)) ⟹ (si,tj) ∈ NS"
proof -
assume "isOK(?cs (si,tj))" with all have "(si,tj) ∈ set ?s" by auto
with S show "(si,tj) ∈ S" by blast
next
assume "isOK(?cns (si,tj))" with all have "(si,tj) ∈ set ?ns" by auto
with NS show "(si,tj) ∈ NS" by blast
qed
} note ok = this
{
fix f ss g ts
assume mem: "(Fun f ss, Fun g ts) ∈ set all"
have "set (lterms ?af (Fun f ss)) × set (lterms ?af (Fun g ts)) ∩
{(x,y). snd (label_s_ns_impl ?cs ?cns x y)} ⊆ label_ns"
proof (clarify)
fix si i tj j
assume rel: "snd (label_s_ns_impl ?cs ?cns (si,i) (tj,j))" and
mems: "(si,i) ∈ set (lterms ?af (Fun f ss))" and
memt: "(tj,j) ∈ set (lterms ?af (Fun g ts))"
have "((si,i),(tj,j)) ∈ lex_two (fun_to_rel (λ s t. (s,t) ∈ S)) (fun_to_rel (λ s t. (s,t) ∈ NS)) ge"
by (rule label_ns_impl[OF _ _ rel])
(rule ok[OF mem mems memt], simp)+
thus "((si,i),(tj,j)) ∈ label_ns" unfolding label_ns_def by simp
qed
} note non_strict = this
{
fix f ss g ts
assume mem: "(Fun f ss, Fun g ts) ∈ set all"
have "set (lterms ?af (Fun f ss)) × set (lterms ?af (Fun g ts)) ∩
{(x,y). fst (label_s_ns_impl ?cs ?cns x y)} ⊆ label_s"
proof (clarify)
fix si i tj j
assume rel: "fst (label_s_ns_impl ?cs ?cns (si,i) (tj,j))" and
mems: "(si,i) ∈ set (lterms ?af (Fun f ss))" and
memt: "(tj,j) ∈ set (lterms ?af (Fun g ts))"
have "((si,i),(tj,j)) ∈ lex_two (fun_to_rel (λ s t. (s,t) ∈ S)) (fun_to_rel (λ s t. (s,t) ∈ NS)) gt"
by (rule label_s_impl[OF _ _ rel],
(rule ok[OF mem mems memt], simp)+)
thus "((si,i),(tj,j)) ∈ label_s" unfolding label_s_def by simp
qed
} note strict = this
show "∃ S NS NST. ce_af_root_redtriple_order S NS NST (root_redtriple.af ?rp) (root_redtriple.aft ?rp) ∧ set s_list ⊆ S ∧ set ns_list ⊆ NS ∧ set nst_list ⊆ NST" unfolding pi
unfolding generate_scnp_rp_def Let_def root_redtriple.simps
proof (intro exI conjI, rule ce_af_scnp_mul)
show "set ns_list ⊆ NS" by (rule NS2)
next
show "set s_list ⊆ S_label_mul"
proof
fix s t
assume mem: "(s,t) ∈ set s_list"
hence all: "(s,t) ∈ set all" unfolding all by auto
from mem S' have "isOK(S_label_mul_impl list_ext ?af ?cs ?cns (s,t))" by auto
note S' = this[unfolded S_label_mul_impl_def split]
from S' obtain f ss where s: "s = Fun f ss" by (cases s, auto)
from S' obtain g ts where t: "t = Fun g ts" unfolding s by (cases t, auto)
from S'[unfolded s t]
have S': "fst (list_ext (label_s_ns_impl ?cs ?cns) (lterms ?af (Fun f ss)) (lterms ?af (Fun g ts)))" by simp
note all = all[unfolded s t]
show "(s,t) ∈ S_label_mul" unfolding s t S_label_mul_def
proof (rule, intro exI conjI, rule refl)
show "(lterms ?af (Fun f ss),
lterms ?af (Fun g ts)) ∈ s_ext label_s label_ns"
by (rule s_ext_local_mono, rule strict[OF all], rule non_strict[OF all], unfold list_ext_s, insert S', auto)
qed
qed
next
show "set nst_list ⊆ NST_label_mul"
proof
fix s t
assume mem: "(s,t) ∈ set nst_list"
hence all: "(s,t) ∈ set all" unfolding all by auto
from mem NST' have "isOK(NST_label_mul_impl list_ext ?af ?cs ?cns (s,t))" by auto
note NST' = this[unfolded NST_label_mul_impl_def split]
from NST' obtain f ss where s: "s = Fun f ss" by (cases s, auto)
from NST' obtain g ts where t: "t = Fun g ts" unfolding s by (cases t, auto)
from NST'[unfolded s t]
have NST': "snd (list_ext (label_s_ns_impl ?cs ?cns) (lterms ?af (Fun f ss)) (lterms ?af (Fun g ts)))" by simp
note all = all[unfolded s t]
show "(s,t) ∈ NST_label_mul" unfolding s t NST_label_mul_def
proof (rule, intro exI conjI, rule refl)
show "(lterms ?af (Fun f ss),
lterms ?af (Fun g ts)) ∈ ns_ext label_s label_ns"
by (rule ns_ext_local_mono, rule strict[OF all], rule non_strict[OF all], insert NST', unfold list_ext_ns, auto)
qed
qed
qed
qed
end