theory WPO_Impl
imports
WPO
"Check-NT.Term_Order_Impl"
Status_Impl
QTRS.Term_Impl
"Check-NT.Name"
begin
definition compare_bools :: "bool × bool ⇒ bool × bool ⇒ bool" where
"compare_bools p1 p2 ≡ (fst p1 ⟶ fst p2) ∧ (snd p1 ⟶ snd p2)"
notation compare_bools ("(_/ ≤cb _)" [51,51] 50)
lemma lex_ext_unbounded_cb: assumes "⋀ i. i < length xs ⟹ i < length ys ⟹ f (xs ! i) (ys ! i) ≤cb g (xs ! i) (ys ! i)"
shows "lex_ext_unbounded f xs ys ≤cb lex_ext_unbounded g xs ys"
unfolding compare_bools_def
by (rule lex_ext_unbounded_mono,
insert assms[unfolded compare_bools_def], auto)
context
fixes "pr" :: "('f × nat ⇒ 'f × nat ⇒ bool × bool)"
and prl :: "'f × nat ⇒ bool"
and cS cNS :: "('f,'v)term ⇒ ('f,'v)term ⇒ bool"
and σ :: "'f status"
begin
fun wpo_ub :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ bool × bool"
where
"wpo_ub s t = (case s of Var x ⇒ (False,
case t of
Var y ⇒ x = y
| Fun g ts ⇒ cNS s t ∧ status σ (g,length ts) = [] ∧ prl (g,length ts))
| Fun f ss ⇒ if cS s t then (True,True)
else let ff = (f,length ss); sf = status σ ff in
if cNS s t then if (∃ i ∈ set sf. snd (wpo_ub (ss ! i) t)) then (True,True)
else (case t of Var _ ⇒ (False,False) | Fun g ts ⇒
let gg = (g,length ts); sg = status σ gg in
case pr ff gg of (prs,prns) ⇒
if prns ∧ (∀ j ∈ set sg. fst (wpo_ub s (ts ! j))) then
if prs then (True, True) else
lex_ext_unbounded wpo_ub (map (λ i. ss ! i) sf)
(map (λ i. ts ! i) sg)
else (False, False))
else (False,False))"
declare wpo_ub.simps[simp del]
abbreviation "wpo_orig ≡ wpo pr prl"
lemma wpo_ub: assumes "⋀ si tj. s ⊵ si ⟹ t ⊵ tj ⟹ (cS si tj, cNS si tj) ≤cb ((si,tj) ∈ S, (si,tj) ∈ NS)"
and "⋀ f. f ∈ funas_term t ⟹ length (status σ f) ≤ n"
shows "wpo_ub s t ≤cb wpo_orig n S NS σ s t"
using assms
proof (induct s t rule: wpo.induct[of S NS σ _ "pr" prl n])
case (1 s t)
note IH = 1(1-3)
note cb = 1(4)
note n = 1(5)
note cbd = compare_bools_def
note simps = wpo_ub.simps[of s t] wpo.simps[of "pr" prl n S NS σ s t]
let ?wpo = "wpo_orig n S NS σ"
let ?cb = "λ s t. (cS s t, cNS s t) ≤cb ((s, t) ∈ S, (s, t) ∈ NS)"
let ?goal = "λ s t. wpo_ub s t ≤cb ?wpo s t"
from cb[of s t] have cb_st: "?cb s t" by auto
show ?case
proof (cases s)
case (Var x) note s = this
show ?thesis
proof (cases t)
case (Var y) note t = this
show ?thesis unfolding simps unfolding s t cbd by simp
next
case (Fun g ts) note t = this
show ?thesis unfolding simps using cb_st unfolding s t cbd by auto
qed
next
case (Fun f ss) note s = this
let ?f = "(f,length ss)"
let ?sf = "status σ ?f"
let ?s = "Fun f ss"
show ?thesis
proof (cases "(s,t) ∈ S ∨ ¬ cNS s t")
case True
with cb_st show ?thesis unfolding simps unfolding s cbd by auto
next
case False
with cb_st have *: "(s,t) ∉ S" "(s,t) ∈ NS" "((s,t) ∉ S) = True" "((s,t) ∈ NS) = True" "cS s t = False" "cNS s t = True"
unfolding cbd by auto
note IH = IH[OF s *(1-2)]
show ?thesis
proof (cases "(∃ i ∈ set ?sf. snd (?wpo (ss ! i) t))")
case True
thus ?thesis unfolding simps using True * unfolding s cbd by auto
next
case False
{
fix i
assume i: "i ∈ set ?sf"
from status_aux[OF i]
have "?goal (ss ! i) t"
by (intro IH(1)[OF i cb n], auto simp: s)
}
with False have sub: "(∃ i ∈ set ?sf. snd (wpo_ub (ss ! i) t)) = False" unfolding cbd by auto
note IH = IH(2-3)[OF False]
show ?thesis
proof (cases "wpo_ub s t = (False,False)")
case True
thus ?thesis unfolding cbd by auto
next
case False note noFF = this
note False = False[unfolded simps * Let_def, unfolded s term.simps sub, simplified]
from False obtain g ts where t: "t = Fun g ts" by (cases t, auto)
let ?g = "(g,length ts)"
let ?sg = "status σ ?g"
let ?t = "Fun g ts"
obtain ps pns where p: "pr ?f ?g = (ps, pns)" by force
note IH = IH[OF t p[symmetric]]
note False = False[unfolded t p split term.simps]
from False have pns: "pns = True" by (cases pns, auto)
{
fix j
assume j: "j ∈ set ?sg"
from status_aux[OF j]
have cb: "?goal s (ts ! j)"
by (intro IH(1)[OF j cb n], auto simp: t)
from j False have "fst (wpo_ub s (ts ! j))" unfolding s by (auto split: if_splits)
with cb have "fst (?wpo s (ts ! j))" unfolding cbd by auto
}
hence cond: "pns ∧ (∀ j ∈ set ?sg. fst (?wpo s (ts ! j)))" using pns by auto
note IH = IH(2)[OF cond]
from cond have cond: "(pns ∧ (∀ j ∈ set ?sg. fst (?wpo ?s (ts ! j)))) = True" unfolding s by simp
note simps = simps[unfolded * Let_def, unfolded s t term.simps if_False if_True sub[unfolded t] p split cond]
show ?thesis
proof (cases ps)
case True
thus ?thesis unfolding s t unfolding simps cbd by auto
next
case False
note IH = IH[OF this _ _ cb n, unfolded s t length_map]
let ?msf = "map (op ! ss) ?sf"
let ?msg = "map (op ! ts) ?sg"
from n[of ?g, unfolded t] have "length (?msg) ≤ n" by auto
hence ub: "lex_ext_unbounded ?wpo ?msf ?msg =
lex_ext ?wpo n ?msf ?msg"
unfolding lex_ext_unbounded_iff lex_ext_iff by auto
{
fix i
assume "i < length ?msf"
hence "?msf ! i ∈ set ?msf" unfolding set_conv_nth by blast
also have "set ?msf ⊆ set ss" using status[of σ f "length ss"]
unfolding set_conv_nth by force
finally have "?msf ! i ∈ set ss" .
} note msf = this
{
fix i
assume "i < length ?msg"
hence "?msg ! i ∈ set ?msg" unfolding set_conv_nth by blast
also have "set ?msg ⊆ set ts" using status[of σ g "length ts"]
unfolding set_conv_nth by force
finally have "?msg ! i ∈ set ts" .
} note msg = this
from False simps noFF
have "wpo_ub s t = lex_ext_unbounded wpo_ub ?msf ?msg"
unfolding s t simps by (auto split: if_splits)
also have "… ≤cb lex_ext_unbounded ?wpo ?msf ?msg"
by (rule lex_ext_unbounded_cb, rule IH, insert msf msg, auto)
finally show ?thesis unfolding ub s t simps(2) cbd by auto
qed
qed
qed
qed
qed
qed
end
definition af_wpo :: "'f af ⇒ 'f status ⇒ 'f af" where
"af_wpo π σ f = (set (status σ f) ∪ π f)"
lemma af_wpo_compat: "af_compatible π NS ⟹ af_compatible (af_wpo π σ) NS"
unfolding af_compatible_def af_wpo_def by auto
lemma af_wpo_status: "af_compatible_status (af_wpo π σ) σ"
unfolding af_compatible_status_def af_wpo_def by auto
definition faulty_redtriple :: "'f itself ⇒ 'v itself ⇒ shows ⇒ shows ⇒ ('f,'v)redtriple" where
"faulty_redtriple _ _ err desc = ⦇
redtriple.valid = error err,
s = (λ _. succeed),
ns = (λ _. succeed),
nst = (λ _. succeed),
af = full_af,
mono_af = empty_af,
mono = (λ _ . succeed),
desc = desc,
not_ws_ns = None,
cpx = no_complexity_check⦈"
lemma faulty_redtriple[simp]: "¬ isOK (redtriple.valid (faulty_redtriple a b c d))"
unfolding faulty_redtriple_def by simp
fun check_status_ws_info :: "'f status
⇒ (('f,string)rule ⇒ shows check)
⇒ (('f :: show) × nat) list option
⇒ shows check" where
"check_status_ws_info σ cns None = error (shows ''missing weak-subterm status of base reduction pair'')"
| "check_status_ws_info σ cns (Some fs) = check_allm (λ f.
check_allm (λ i. cns (Fun (fst f) (map (λ i. Var (show i)) [0 ..< snd f]), Var (show i))
<+? (λ _. shows ''according to weak-mon. information of order, argument #'' +@+ shows (Suc i) +@+
shows '' must not occur in status of '' +@+ shows f)) (status σ f)) fs"
type_synonym 'f wpo_params = "(('f × nat) × (nat × nat list))list"
fun shows_wpo_params :: "('f :: show) wpo_params ⇒ shows" where
"shows_wpo_params params = (shows ''status and precedence '' +@+ shows_nl +@+ (shows_sep (λ (f,(p,s)).
shows ''symbol '' +@+ shows f +@+ shows '': precedence = '' +@+ shows p
+@+ shows '' status = '' +@+ shows s
) shows_nl params))"
definition wpo_redtriple :: "('f :: {key,show}, string)redtriple
⇒ 'f wpo_params
⇒ ('f,string)redtriple" where
"wpo_redtriple rt params ≡
let stat = map (λ (f,ps). (f, snd ps)) params;
pr = fun_of_map_fun' (ceta_map_of params) (λ _. 0) fst;
desc = shows ''WPO with '' +@+ shows_wpo_params params +@+ shows_nl
+@+ shows ''over the following reduction pair:'' +@+ shows_nl +@+ redtriple.desc rt
in
(case status_of stat of
None ⇒ faulty_redtriple (TYPE('f)) (TYPE(string)) (shows ''problem with indices in status of WPO!'') desc
| Some σ ⇒
let
s = (λ s t. isOK(redtriple.s rt (s,t)));
ns = (λ s t. isOK(redtriple.ns rt (s,t)));
wpo = wpo_ub (prc_nat pr) (prl_nat pr) s ns σ;
wpo_s = (λ (s,t). check (fst (wpo s t)) (shows s +@+ shows '' >wpo '' +@+ shows t +@+ shows '' could not be ensured''));
wpo_ns = (λ (s,t). check (snd (wpo s t)) (shows s +@+ shows '' >=wpo '' +@+ shows t +@+ shows '' could not be ensured''))
in ⦇ redtriple.valid = do {redtriple.valid rt; check_status_ws_info σ (redtriple.ns rt) (redtriple.not_ws_ns rt)} ,
s = wpo_s,
ns = wpo_ns,
nst = wpo_ns,
af = af_wpo (redtriple.af rt) σ,
mono_af = empty_af, (* TODO: this is too crude *)
mono = (λ _ . check_allm (λ ((f,n),idx). check (set idx = set [0..< n]) (
shows ''for monotonicity, status must be complete, but status of '' +@+
shows (f,n) +@+ shows '' is '' +@+ shows (map Suc idx))) stat),
desc = desc,
not_ws_ns = Some (map fst stat),
cpx = no_complexity_check⦈)"
lemma wpo_redtriple: assumes gen: "⋀ s ns nst. isOK(redtriple.valid rt) ⟹
isOK (try forallM (redtriple.s rt) s catch (λx. Inl (snd x))) ⟹
isOK (try forallM (redtriple.ns rt) ns catch (λx. Inl (snd x))) ⟹
isOK (try forallM (redtriple.nst rt) nst catch (λx. Inl (snd x))) ⟹
∃S NS NST.
cpx_ce_af_redtriple_order S NS NST (redtriple.af rt) (redtriple.mono_af rt) (λ cm cc. isOK(redtriple.cpx rt cm cc)) ∧
set s ⊆ S ∧
set ns ⊆ NS ∧
set nst ⊆ NST ∧
not_ws_info NS (redtriple.not_ws_ns rt) ∧
(isOK (redtriple.mono rt (s @ ns @ nst)) ⟶
mono_ce_af_redtriple_order S NS NST (redtriple.af rt) ∧ ctxt.closed S)"
shows "generic_redtriple_impl (wpo_redtriple rt)"
proof
fix param and s_list ns_list nst_list
let ?rp = "wpo_redtriple rt param"
let ?pi = "redtriple.af ?rp"
let ?mpi = "redtriple.mono_af ?rp"
let ?cpx = "redtriple.cpx ?rp"
let ?Cpx = "λ cm cc. isOK(?cpx cm cc)"
let ?s = "λ s t. isOK(redtriple.s ?rp (s,t))"
let ?ns = "λ s t. isOK(redtriple.ns ?rp (s,t))"
let ?stat = "map (λ (f,ps). (f, snd ps)) param"
assume valid: "isOK(redtriple.valid ?rp)" and stri: "isOK (check_allm (redtriple.s ?rp) s_list)"
and nstri: "isOK (check_allm (redtriple.ns ?rp) ns_list)"
and nstrit: "isOK (check_allm (redtriple.nst ?rp) nst_list)"
let ?rp' = "rt"
let ?pi' = "redtriple.af ?rp'"
let ?mpi' = "redtriple.mono_af ?rp'"
let ?cpx' = "redtriple.cpx ?rp'"
let ?Cpx' = "λ cm cc. isOK(?cpx' cm cc)"
let ?s' = "λ s t. isOK(redtriple.s ?rp' (s,t))"
let ?ns' = "λ s t. isOK(redtriple.ns ?rp' (s,t))"
let ?pr = "fun_of_map_fun' (ceta_map_of param) (λ _. 0) fst"
let ?prc = "prc_nat ?pr"
let ?prl = "prl_nat ?pr"
let ?ws' = "redtriple.not_ws_ns ?rp'"
note d = wpo_redtriple_def[unfolded Let_def]
note valid = valid[unfolded d param split]
from valid obtain σ where stat: "status_of ?stat = Some σ" by (cases "status_of ?stat", auto)
note param = param stat
note valid = valid[unfolded stat]
note stri = stri[unfolded d param split]
note nstri = nstri[unfolded d param split]
note nstrit = nstrit[unfolded d param split]
let ?wpo = "wpo_ub (prc_nat ?pr) (prl_nat ?pr) ?s' ?ns' σ"
from valid have status_ws: "isOK(check_status_ws_info σ (redtriple.ns ?rp') ?ws')"
and "isOK(redtriple.valid ?rp')" by auto
note gen = gen[OF this(2)]
from status_ws obtain fs where ws': "?ws' = Some fs" by (cases ?ws', auto)
from status_ws[unfolded ws']
have status_ws: "⋀ f i. f ∈ set fs ⟹ i ∈ set (status σ f) ⟹
?ns' (Fun (fst f) (map (λi. Var (show i)) [0..<snd f])) (Var (show i))" by auto
def all ≡ "s_list @ ns_list @ nst_list"
def subts ≡ "[(u,v) . (s,t) <- all, u <- supteq_list s, v <- supteq_list t]"
def s ≡ "filter (λ (s,t). ?s' s t) subts"
def ns ≡ "(filter (λ (s,t). ?ns' s t) subts) @ [(Fun (fst f) (map (λi. Var (show i)) [0..<snd f]), Var (show i)) .
f <- fs, i <- status σ f]"
have "∃S NS NST.
cpx_ce_af_redtriple_order S NS NST ?pi' ?mpi' ?Cpx' ∧
set s ⊆ S ∧ set ns ⊆ NS ∧ set [] ⊆ NST ∧
not_ws_info NS ?ws' ∧
(isOK (redtriple.mono rt (s @ ns @ [])) ⟶
mono_ce_af_redtriple_order S NS NST ?pi' ∧ ctxt.closed S)"
by (rule gen, insert status_ws, auto simp: s_def ns_def)
then obtain S NS NST where
rt: "cpx_ce_af_redtriple_order S NS NST ?pi' ?mpi' ?Cpx'"
and orient: "set s ⊆ S ∧ set ns ⊆ NS"
and ws: "not_ws_info NS ?ws'" by blast
def n ≡ "max_list [ length (status σ f) . (s,t) <- all, f <- funas_term_list t]"
interpret cpx_ce_af_redtriple_order S NS NST ?pi' ?mpi' ?Cpx' by fact
interpret precedence ?prc ?prl ..
note cb = compare_bools_def
let ?wpoo = "wpo_orig ?prc ?prl n S NS σ"
let ?wpo_s = "{(s, t). fst (?wpoo s t)}"
let ?wpo_ns = "{(s, t). snd (?wpoo s t)}"
{
fix s t
assume st: "(s,t) ∈ set all"
have "?wpo s t ≤cb ?wpoo s t"
proof (rule wpo_ub)
fix si tj
assume "s ⊵ si" "t ⊵ tj"
with st have sitj: "(si,tj) ∈ set subts" unfolding subts_def by force
with orient
show "(?s' si tj, ?ns' si tj)
≤cb ((si, tj) ∈ S, (si, tj) ∈ NS)" unfolding s_def ns_def cb by auto
next
fix f
assume f: "f ∈ funas_term t"
show "length (status σ f) ≤ n" unfolding n_def
by (rule max_list, insert f st, auto)
qed
} note cb_all = this[unfolded cb]
interpret wpo_alg_pr NS S ?prc ?prl n σ
proof
show "S ⊆ NS" by (rule S_imp_NS)
fix i fn
assume i: "i ∈ set (status σ fn)"
obtain f n where f: "fn = (f,n)" by force
show "ws_fun_arg NS fn i"
proof (cases "fn ∈ set fs")
case False
with ws[unfolded ws'] show ?thesis by (auto simp: f)
next
case True
let ?l = "Fun f (map (λi. Var (show i)) [0..<n])"
let ?r = "Var (show i)"
have ns: "(?l, ?r) ∈ NS" using orient i True unfolding ns_def f by force
show ?thesis unfolding f
proof (rule ws_fun_argI)
fix ts :: "('a,string)term list"
assume len: "length ts = n" and i: "i < n"
def inv ≡ "λ s. ts ! (the_inv show s)"
{
fix i
have "inv (show i) = ts ! i" unfolding inv_def
using the_inv_f_f[OF show_nat_inj] by auto
}
with subst.closedD[OF subst_NS ns, of inv]
show "(Fun f ts, ts ! i) ∈ NS"
by (auto simp: o_def len[symmetric] map_nth)
qed
qed
qed
from af_compat have "af_compatible ?pi' NS" .
from af_wpo_compat[OF this, of σ] have pi: "af_compatible ?pi NS"
unfolding param d split by auto
from af_wpo_status[of ?pi' σ] have pi2: "af_compatible_status ?pi σ"
unfolding param d split by auto
let ?m = "max_list (map (snd o fst) ?stat)"
have σ: "∃n. ∀m≥n. ∀f. {0, 1} ⊆ set (status σ (f, Suc (Suc m)))"
proof (rule exI[of _ ?m], intro allI impI)
fix k f
assume k: "?m ≤ k"
let ?k = "Suc (Suc k)"
from k have "?m < ?k" by auto
with max_list[of ?k "map (snd o fst) ?stat"]
have "(f,?k) ∉ fst ` set ?stat" by force
from status_of_default[OF stat this]
show "{0,1} ⊆ set (status σ (f,Suc (Suc k)))" by auto
qed
from wpo_ce_af_redtriple_order[OF σ pi pi2]
have mono: "mono_ce_af_redtriple_order ?wpo_s ?wpo_ns ?wpo_ns ?pi" by simp
interpret mono_ce_af_redtriple_order ?wpo_s ?wpo_ns ?wpo_ns ?pi by fact
have mpi: "?mpi = empty_af" unfolding wpo_redtriple_def Let_def stat
by simp
interpret cpx_ce_af_redtriple_order ?wpo_s ?wpo_ns ?wpo_ns ?pi ?mpi ?Cpx unfolding mpi
by (unfold_locales, auto simp: param d empty_af no_complexity_check_def)
have cpx: "cpx_ce_af_redtriple_order ?wpo_s ?wpo_ns ?wpo_ns ?pi ?mpi ?Cpx" ..
let ?ws = "redtriple.not_ws_ns ?rp"
have 1: "set s_list ⊆ ?wpo_s" using stri cb_all unfolding all_def by auto
have 2: "set ns_list ⊆ ?wpo_ns" using nstri cb_all unfolding all_def by auto
have 3: "set nst_list ⊆ ?wpo_ns" using nstrit cb_all unfolding all_def by auto
have "not_ws_info ?wpo_ns (Some (map fst ?stat))" unfolding not_ws_info.simps
proof (intro allI impI)
fix fk i
assume nmem: "fk ∉ set (map fst ?stat)"
obtain f k where f: "fk = (f,k)" by force
with nmem have "(f,k) ∉ fst ` set ?stat" by force
from status_of_default[OF stat this]
subterm_wpo_ns_arg[of _ f]
show "ws_fun_arg ?wpo_ns fk i" unfolding f
by (intro ws_fun_argI, auto)
qed
hence 4: "not_ws_info ?wpo_ns ?ws" by (simp add: param d)
show "∃S NS NST. cpx_ce_af_redtriple_order S NS NST ?pi ?mpi ?Cpx ∧
set s_list ⊆ S ∧
set ns_list ⊆ NS ∧
set nst_list ⊆ NST ∧
not_ws_info NS ?ws ∧
(isOK (redtriple.mono ?rp (s_list @ ns_list @ nst_list)) ⟶
mono_ce_af_redtriple_order S NS NST ?pi ∧ ctxt.closed S)"
proof (intro exI conjI, rule cpx, rule 1, rule 2, rule 3, rule 4, intro impI conjI mono ctxt_closed_WPO_S)
fix f m
assume mono: "isOK (redtriple.mono ?rp (s_list @ ns_list @ nst_list))"
show "set (status σ (f, m)) = {0..<m}"
proof (cases "map_of ?stat (f,m)")
case None
from status_of_default[OF stat this[unfolded map_of_eq_None_iff]]
show ?thesis by auto
next
case (Some idx)
from map_of_SomeD[OF this] mono show ?thesis
by (auto simp: d param status_of_Some[OF stat] Some)
qed
qed
qed
end