theory Reduction_Pair_Implementations
imports
Matrix_Poly
Argument_Filter
Poly_Order
RPO_Memoized
SCNP_Impl
List_Order_Implementations
KBO_Impl
WPO_Impl
Monotone_Algebra
"../Termination_and_Complexity/Max_Polynomial_Impl"
Sqrt_Babylonian.Sqrt_Babylonian
begin
hide_const (open) pi
datatype 'f redtriple_impl =
Int_carrier "('f, int) lpoly_interL"
| Int_nl_carrier "('f, int) poly_inter_list"
| Rat_carrier "('f, rat) lpoly_interL"
| Rat_nl_carrier rat "('f, rat) poly_inter_list"
| Real_carrier "('f, real) lpoly_interL"
| Real_nl_carrier real "('f, real) poly_inter_list"
| Arctic_carrier "('f, arctic) lpoly_interL"
| Arctic_rat_carrier "('f, rat arctic_delta) lpoly_interL"
| Int_mat_carrier nat nat "('f, int mat) lpoly_interL"
| Rat_mat_carrier nat nat "('f, rat mat) lpoly_interL"
| Real_mat_carrier nat nat "('f, real mat) lpoly_interL"
| Arctic_mat_carrier nat "('f, arctic mat) lpoly_interL"
| Arctic_rat_mat_carrier nat "('f, rat arctic_delta mat) lpoly_interL"
| RPO "'f status_prec_repr" "'f afs_list"
| KBO "'f prec_weight_repr" "'f afs_list"
| WPO "'f wpo_params" "'f redtriple_impl"
| Max_poly "('f, max_poly.sig) encoder_inter"
definition faulty_non_inf_order :: "string ⇒ 'a ⇒ ('f :: show, 'v :: show) non_inf_order"
where
"faulty_non_inf_order s F = ⦇
non_inf_order.valid = error (shows_string s),
ns = λ _. succeed,
cc = λ _. succeed,
af = λ _ _. Wild,
desc = id ⦈"
lemma faulty_non_inf_order: "generic_non_inf_order_impl faulty_non_inf_order"
by (unfold_locales) (simp add: faulty_non_inf_order_def)
fun filter_prec_weight_repr :: "('f × nat ⇒ af_entry) ⇒ 'f prec_weight_repr ⇒ 'f filtered prec_weight_repr"
where
"filter_prec_weight_repr π (prw, w0) = (
let
fprw = filter (λ (fn, e). case π fn of Collapse _ ⇒ False | AFList _ ⇒ True) prw;
mprw = map (λ ((f, n), e).
((FPair f n, case π (f, n) of AFList l ⇒ length l | Collapse _ ⇒ 0), e)) fprw
in (mprw, w0))"
fun prec_repr_to_pr :: "'f status_prec_repr ⇒ ('f :: key) filtered × nat ⇒ nat"
where
"prec_repr_to_pr prs = (
let m = ceta_map_of prs in (λ (fp,n).
(case fp of
FPair f a ⇒
(case m (f, a) of
None ⇒ 0
| Some x ⇒ fst x))))"
fun prec_repr_to_status :: "'f status_prec_repr ⇒ ('f :: key) filtered × nat ⇒ order_tag"
where
"prec_repr_to_status prs = (
let m = ceta_map_of prs in (λ (fp,n).
(case fp of
FPair f a ⇒
(case m (f, a) of
None ⇒ Lex
| Some x ⇒ snd x))))"
term max_poly_encoding_impl.create_max_poly_redtriple
primrec get_redtriple :: "('f :: {key, show}) redtriple_impl ⇒ ('f, string) redtriple"
where
"get_redtriple (Int_carrier I) = int_redtriple I"
| "get_redtriple (Int_nl_carrier I) = create_nlpoly_redtriple succeed (1 :: int) (op >) True True I"
| "get_redtriple (Rat_carrier I) = delta_redtriple 1 I"
| "get_redtriple (Rat_nl_carrier d I) = delta_nl_redtriple d I"
| "get_redtriple (Real_carrier I) = delta_redtriple 1 I"
| "get_redtriple (Real_nl_carrier d I) = delta_nl_redtriple d I"
| "get_redtriple (Arctic_carrier I) = arctic_redtriple I"
| "get_redtriple (Arctic_rat_carrier I) = arctic_delta_redtriple I"
| "get_redtriple (Int_mat_carrier n sd I) = int_mat_redtriple n sd I"
| "get_redtriple (Rat_mat_carrier n sd I) = delta_mat_redtriple n sd 1 I"
| "get_redtriple (Real_mat_carrier n sd I) = delta_mat_redtriple n sd 1 I"
| "get_redtriple (Arctic_mat_carrier n I) = arctic_mat_redtriple n I"
| "get_redtriple (Arctic_rat_mat_carrier n I) = arctic_delta_mat_redtriple n I"
| "get_redtriple (RPO precτ pi) =
af_redtriple pi (create_RPO_redtriple
(λ pr. (prec_repr_to_pr pr, prec_repr_to_status pr)) precτ)"
| "get_redtriple (KBO precw pi) =
af_redtriple pi (create_KBO_redtriple (filter_prec_weight_repr (afs_of' pi)) precw)"
| "get_redtriple (WPO params rp) =
wpo_redtriple (get_redtriple rp) params"
| "get_redtriple (Max_poly alist) = max_poly_encoding_impl.create_max_poly_redtriple alist"
lemma get_redtriple:
"generic_redtriple_impl get_redtriple"
proof
fix rp :: "('f :: {key, show}) redtriple_impl"
and s_list ns_list nst_list :: "('f, string) rules"
let ?rp = "get_redtriple rp :: ('f, string) redtriple"
let ?all = "s_list @ ns_list @ nst_list"
let ?ws = "redtriple.not_ws_ns ?rp"
assume v: "isOK (redtriple.valid ?rp)"
and S: "isOK (check_allm (redtriple.s ?rp) s_list)"
and NS: "isOK (check_allm (redtriple.ns ?rp) ns_list)"
and NST: "isOK (check_allm (redtriple.nst ?rp) nst_list)"
thus
"∃ S NS NST. cpx_ce_af_redtriple_order S NS NST (redtriple.af ?rp) (redtriple.mono_af ?rp) (λ cm cc. isOK(redtriple.cpx ?rp cm cc)) ∧
set s_list ⊆ S ∧ set ns_list ⊆ NS ∧ set nst_list ⊆ NST ∧
not_ws_info NS ?ws ∧
(isOK (redtriple.mono ?rp ?all) ⟶
mono_ce_af_redtriple_order S NS NST (redtriple.af ?rp) ∧ ctxt.closed S)"
proof (induct rp arbitrary: s_list ns_list nst_list)
case (Int_carrier I)
thus ?case unfolding get_redtriple.simps
by (intro generic_redtriple_impl.generate_redtriple [OF int_redtriple], auto)
next
case (Int_nl_carrier I) note ass = this
let ?I = "create_nlpoly_redtriple succeed (1 :: int) (op >) True True"
interpret mono_matrix_carrier "op >" 1 nat int_mono by (rule int_complexity)
have "cpx_poly_order_carrier (1 :: int) (op >) True True nat" ..
from poly_order_carrier_to_generic_redtriple_impl [OF this]
have rp: "generic_redtriple_impl ?I" .
show ?case unfolding get_redtriple.simps
by (rule generic_redtriple_impl.generate_redtriple[OF rp], insert ass, auto)
next
case (Rat_carrier I)
thus ?case unfolding get_redtriple.simps
by (intro generic_redtriple_impl.generate_redtriple[OF delta_redtriple], auto)
next
case (Real_carrier I)
thus ?case unfolding get_redtriple.simps
by (intro generic_redtriple_impl.generate_redtriple[OF delta_redtriple], auto)
next
case (Rat_nl_carrier d I)
thus ?case unfolding get_redtriple.simps
by (intro generic_redtriple_impl.generate_redtriple[OF delta_nl_redtriple], auto)
next
case (Real_nl_carrier d I)
thus ?case unfolding get_redtriple.simps
by (intro generic_redtriple_impl.generate_redtriple[OF delta_nl_redtriple], auto)
next
case (Arctic_carrier I)
thus ?case unfolding get_redtriple.simps
by (intro generic_redtriple_impl.generate_redtriple[OF arctic_redtriple], auto)
next
case (Arctic_rat_carrier I)
thus ?case unfolding get_redtriple.simps
by (intro generic_redtriple_impl.generate_redtriple[OF arctic_delta_redtriple], auto)
next
case (Int_mat_carrier n sd I)
thus ?case unfolding get_redtriple.simps
by (intro generic_redtriple_impl.generate_redtriple[OF int_mat_redtriple], auto)
next
case (Rat_mat_carrier n sd I)
thus ?case unfolding get_redtriple.simps
by (intro generic_redtriple_impl.generate_redtriple[OF delta_mat_redtriple], auto)
next
case (Real_mat_carrier n sd I)
thus ?case unfolding get_redtriple.simps
by (intro generic_redtriple_impl.generate_redtriple[OF delta_mat_redtriple], auto)
next
case (Arctic_mat_carrier n I)
thus ?case unfolding get_redtriple.simps
by (intro generic_redtriple_impl.generate_redtriple[OF arctic_mat_redtriple], auto)
next
case (Arctic_rat_mat_carrier n I)
thus ?case unfolding get_redtriple.simps
by (intro generic_redtriple_impl.generate_redtriple[OF arctic_delta_mat_redtriple], auto)
next
case (RPO precτ pi) note ass = this
let ?one = "create_RPO_redtriple (λpr. (prec_repr_to_pr pr, prec_repr_to_status pr))"
have rp: "generic_redtriple_impl ?one" ..
from af_redtriple[OF rp]
have rp: "generic_redtriple_impl (λ I. af_redtriple pi (?one I))" .
show ?case unfolding get_redtriple.simps
by (rule generic_redtriple_impl.generate_redtriple[OF rp], insert ass, auto)
next
case (KBO precw pi) note ass = this
let ?one = "create_KBO_redtriple (filter_prec_weight_repr (afs_of' pi))"
have rp: "generic_redtriple_impl ?one" ..
from af_redtriple[OF rp]
have rp: "generic_redtriple_impl (λ I. af_redtriple pi (?one I))" .
show ?case unfolding get_redtriple.simps
by (rule generic_redtriple_impl.generate_redtriple[OF rp], insert ass, auto)
next
case (WPO params rp) note IH = this
let ?rp = "get_redtriple rp"
show ?case unfolding get_redtriple.simps
by (rule generic_redtriple_impl.generate_redtriple[OF wpo_redtriple],
rule IH(1), insert IH(2-), auto)
next
case IH: (Max_poly alist)
then show ?case
unfolding get_redtriple.simps
by (intro generic_redtriple_impl.generate_redtriple [OF max_poly_redtriple], auto)
qed
qed
definition sqrt_real :: "real ⇒ real list"
where
"sqrt_real x = (if x ≥ 0 then let y = sqrt x in remdups [y, -y] else [])"
lemma sqrt_real[simp]: "set (sqrt_real x) = {y. y * y = x}"
unfolding sqrt_real_def Let_def
by (cases "x ≥ 0", auto)
fun
get_non_inf_order ::
"('f :: {key, show}) redtriple_impl ⇒ ('f × nat) list ⇒ ('f,'v :: {show, linorder}) non_inf_order"
where
"get_non_inf_order (Int_nl_carrier I) =
create_nlpoly_non_inf_order succeed (1 :: int) (op >) True True sqrt_int I"
| "get_non_inf_order (Rat_nl_carrier d I) = delta_non_inf_order d sqrt_rat I"
| "get_non_inf_order (Real_nl_carrier d I) = delta_non_inf_order d sqrt_real I"
| "get_non_inf_order _ =
faulty_non_inf_order ''only integers, rationals and reals are supported for non-inf orders''"
lemma get_non_inf_order:
"generic_non_inf_order_impl get_non_inf_order"
proof
fix rp :: "('f :: {key, show}) redtriple_impl"
and F and ns_list :: "('f, 'v :: {show, linorder}) rules" and cc
let ?rp = "get_non_inf_order rp F :: ('f, 'v) non_inf_order"
assume v: "isOK (non_inf_order.valid ?rp)"
and cc: "isOK (check_allm (non_inf_order.cc ?rp) cc)"
and NS: "isOK (check_allm (non_inf_order.ns ?rp) ns_list)"
show "∃ S NS.
non_inf_order_trs S NS (set F) (non_inf_order.af ?rp) ∧
set ns_list ⊆ NS ∧ Ball (set cc) (cc_satisfied (set F) S NS)"
proof (cases rp)
case (Int_nl_carrier I)
hence id: "?rp = (create_nlpoly_non_inf_order succeed (1 :: int) (op >) True True sqrt_int) I F"
(is "_ = ?I I F") by simp
have "non_inf_poly_order_carrier (1 :: int) (op >) True True"
by (unfold_locales, insert non_inf_int_gt, auto simp: mult_right_mono_neg)
from non_inf_poly_order_carrier_to_generic_non_inf_order[OF this]
have rp: "generic_non_inf_order_impl ?I" .
show ?thesis by (simp only: id, rule generic_non_inf_order_impl.generate_non_inf_order[of ?I, OF rp v[simplified id] NS[simplified id] cc[simplified id]])
next
case (Rat_nl_carrier d I)
hence id: "?rp = (delta_non_inf_order d sqrt_rat) I F" by simp
show ?thesis unfolding id
by (rule generic_non_inf_order_impl.generate_non_inf_order[OF delta_non_inf_order], insert NS v cc id, auto)
next
case (Real_nl_carrier d I)
hence id: "?rp = (delta_non_inf_order d sqrt_real) I F" by simp
show ?thesis unfolding id
by (rule generic_non_inf_order_impl.generate_non_inf_order[OF delta_non_inf_order], insert NS v cc id, auto)
qed (insert v, auto simp: faulty_non_inf_order_def)
qed
datatype ('f) root_redtriple_impl = SCNP list_order_type "'f scnp_af" "'f redtriple_impl"
hide_const (open) Almost_Full.af
primrec
get_root_redtriple :: "('f :: {key, show}) root_redtriple_impl ⇒ ('f, string) root_redtriple"
where
"get_root_redtriple (SCNP type af rp) =
generate_scnp_rp (list_ext (scnp_arity af) type) (list_ext_name type) af get_redtriple rp"
lemma get_root_redtriple:
"generic_root_redtriple_impl get_root_redtriple"
proof
fix rrp :: "('f :: {key, show}) root_redtriple_impl"
and s_list ns_list nst_list :: "('f, string) rule list"
let ?r = "get_root_redtriple rrp :: ('f, string) root_redtriple"
assume ass: "isOK (root_redtriple.valid ?r)"
"isOK (check_allm (root_redtriple.s ?r) s_list)"
"isOK (check_allm (root_redtriple.ns ?r) ns_list)"
"isOK (check_allm (root_redtriple.nst ?r) nst_list)"
show "∃ s ns nst.
ce_af_root_redtriple_order s ns nst (root_redtriple.af ?r) (root_redtriple.aft ?r) ∧
set s_list ⊆ s ∧ set ns_list ⊆ ns ∧ set nst_list ⊆ nst"
proof (cases rrp)
case (SCNP t af rp)
show ?thesis unfolding SCNP get_root_redtriple.simps
by (rule generic_root_redtriple_impl.generate_root_redtriple
[OF generate_scnp_rp[OF get_redtriple list_ext], OF ass[unfolded SCNP get_root_redtriple.simps]])
qed
qed
end