theory Max_Polynomial_Impl
imports
Max_Polynomial Ordered_Algebra_Impl
"../LTS/IA_Checker"
"Check-NT.Term_Order_Impl"
begin
locale max_poly_encoding_impl =
verbose.encoder: encoding_impl
where default_fun = "λx. max_poly.MaxF" +
verbose: pre_encoded_ord_algebra
where less_eq = "op ≤" and less = "op <" and I = max_poly.I and E = verbose.encoder.E
begin
text {*
We simplify the encoding terms. It is shown to preserve semantics, but the fact doesn't matter
for soundness.
*}
definition "simplified_alist = map (map_prod id max_poly.simplify) alist"
sublocale encoder: encoding_impl
where alist = "simplified_alist"
and default_fun = "λ_. max_poly.MaxF" .
sublocale pre_encoded_ord_algebra
where less_eq = "op ≤"
and less = "op <"
and I = max_poly.I
and E = encoder.E .
definition "check_less_term h s t = IA.check_formula h (encode s ⊏⇩I encode t)"
definition "check_less_eq_term h s t = IA.check_formula h (encode s ⊑⇩I encode t)"
definition "check_ws_fun_arg h f n i = do {
check (i < n) (shows ''bad argument number'');
IA.check_formula h (Var i ⊑⇩I encoder.E f n)
}"
definition [simp]: "create_max_poly_redtriple = ⦇
redtriple.valid = encoder.check_encoding,
s = (λ(s, t). check_less_term default t s),
ns = (λ(s, t). check_less_eq_term default t s),
nst = (λ(s, t). check_less_eq_term default t s),
af = (λ(f, n). {0..<n} - set (constant_positions f n)),
mono_af = empty_af,
mono = (λ s_ns_nst. error (shows ''monotonicity of max-poly is not yet supported'')),
desc = shows ''a max polynomial interpretation'',
not_ws_ns = Some (map fst simplified_alist),
cpx = no_complexity_check
⦈"
lemma af_compatible:
"af_compatible (λ(f, n). {0..<n} - set (constant_positions f n)) (rel_of op ⊒⇩t)"
(is "af_compatible ?pi _")
proof -
{
fix f and s t :: "('a, 'b) term" and bef aft :: "('a, 'b) term list"
let ?ss = "bef @ s # aft"
let ?n = "Suc (length bef + length aft)"
assume "length bef ∉ ?pi (f, ?n)"
then have "length bef ∈ set (constant_positions f ?n)" by auto
from constant_atD [OF constant_positions [OF this], of "map (λs. ⟦s⟧α) ?ss" "⟦t⟧α" for α, simplified]
have "Fun f (bef @ s # aft) ⊒⇩t Fun f (bef @ t # aft)"
by (auto simp: nth_append list_update_append)
}
then show ?thesis unfolding af_compatible_def by blast
qed
context
assumes ok: "isOK encoder.check_encoding"
begin
interpretation encoder: encoding where E = encoder.E by (fact encoder.check_encoding[OF ok])
interpretation max_poly_encoding where E = encoder.E ..
lemma check_less_term:
assumes "isOK (check_less_term h s t)" shows "s ⊏⇩t t"
by (intro less_term_via_IA IA.check_formula, insert assms, unfold check_less_term_def, auto)
lemma check_less_eq_term:
assumes "isOK (check_less_eq_term h s t)" shows "s ⊑⇩t t"
by (intro less_eq_term_via_IA IA.check_formula, insert assms, unfold check_less_eq_term_def, auto)
lemmas redpair = redpair
lemma check_ws_fun_arg:
assumes "isOK (check_ws_fun_arg h f n i)" shows "ws_fun_arg (rel_of op ⊒⇩t) (f, n) i"
using assms by (intro ws_fun_arg_via_IA IA.check_formula, auto simp: check_ws_fun_arg_def)
end
lemma default_E: "(f, n) ∉ fst ` set simplified_alist ⟹
encoder.E f n = Fun max_poly.MaxF (map Var [0..<n])"
by (auto simp: encoder.E_def split: option.split dest!: map_of_SomeD)
end
lemma le_max_list: "(x::nat) ∈ set xs ⟹ x ≤ max_list xs"
using split_list by fastforce
lemma le_max_list1: "(x::nat) ∈ set xs ⟹ x ≤ max_list1 xs"
by (subst max_list_as_max_list1 [symmetric]) (auto simp: le_max_list)
lemma max_poly_redtriple: "generic_redtriple_impl max_poly_encoding_impl.create_max_poly_redtriple"
proof (unfold_locales, goal_cases)
case (1 rp s_list ns_list nst_list)
interpret max_poly_encoding_impl rp.
from 1(1)[simplified] interpret encoder: encoding where E = encoder.E by (rule encoder.check_encoding)
interpret max_poly_encoding where E = encoder.E..
interpret redpair_order "rel_of op ⊐⇩t" "rel_of op ⊒⇩t"..
interpret redtriple_order "rel_of op ⊐⇩t" "rel_of op ⊒⇩t" "rel_of op ⊒⇩t"
by ((unfold_locales; fact?), insert term.less_imp_le, auto)
note 1 = 1 [simplified]
note 2 = check_less_eq_term [OF 1(1), of "default"] check_less_term [OF 1(1), of "default"]
have 3: "set s_list ⊆ rel_of op ⊐⇩t"
using 1(2) [rule_format] and 2(2)
by auto
have 4: "set ns_list ⊆ rel_of op ⊒⇩t"
using 1(3)[rule_format] and 2(1)
by auto
have 5: "set nst_list ⊆ rel_of op ⊒⇩t"
using 1(4)[rule_format] and 2(1)
by auto
have [simp]: "map fst rp = map fst simplified_alist" by (auto simp: simplified_alist_def)
have [simp]: "map (snd ∘ fst) rp = map (snd ∘ fst) simplified_alist"
unfolding map_map [symmetric] by simp
define n where "n ≡ max_list1 (map (snd ∘ fst) rp) + 1"
then have m: "⋀c m. m ≥ n ⟹ (c, Suc (Suc m)) ∉ set (map fst rp)"
apply (auto simp:)
apply (subgoal_tac "Suc (Suc m) ≤ max_list1 (map (snd ∘ fst) simplified_alist)")
apply simp
apply (rule le_max_list1, force)
done
have 6: "∀m≥n. ∀c. ce_trs (c, m) ⊆ rel_of op ⊒⇩t"
proof -
{
fix m c and l r :: "('a, _) term"
assume nm: "n ≤ m" and "(l, r) ∈ ce_trs (c,m)"
then obtain s t where l: "l = Fun c ([s,t] @ replicate m (Var undefined))" (is "_ = Fun _ ?ls") and r: "r = s ∨ r = t"
unfolding ce_trs.simps by auto
have len: "length ?ls = Suc (Suc m)" by simp
have id: "[0..<Suc (Suc m)] = [0,1] @ map (Suc o Suc) [0 ..< m]"
unfolding map_map [symmetric] and map_Suc_upt
by (auto simp: upt_conv_Cons)
from m [OF nm] have "∀ α. ∃ k.⟦l⟧α = max (⟦s⟧ α) (max (⟦t⟧α) k)"
unfolding default_E [OF m [OF nm, simplified]]
and id and l and eval.simps and len and length_map
by (auto)
from choice [OF this] obtain k where "⟦l⟧α = max (⟦s⟧α) (max (⟦t⟧α) (k α))" for α by blast
with r have "l ⊒⇩t r" by (auto intro: max.cobounded1)
then have "(l,r) ∈ rel_of op ⊒⇩t" by auto
}
then show ?thesis by auto
qed
show ?case
apply (rule exI[of _ "rel_of op ⊐⇩t"], intro exI[of _ "rel_of op ⊒⇩t"] conjI, unfold_locales)
apply (auto intro!: 3 4 5 6 empty_af af_compatible simp:ws_fun_arg_def no_complexity_check_def o_def nth_map dest!:default_E intro!: less_eq_termI le_max_list)
apply (metis (no_types, lifting) in_set_conv_nth length_map nth_image_indices nth_map)
done
qed
declare max_poly_encoding_impl.check_less_term_def [code]
declare max_poly_encoding_impl.check_less_eq_term_def [code]
declare max_poly_encoding_impl.simplified_alist_def [code]
declare max_poly_encoding_impl.create_max_poly_redtriple_def [code]
declare pre_encoded_algebra.constant_positions_def [code]
end