theory Max_Polynomial
imports Ordered_Algebra "../LTS/Integer_Arithmetic" Ring_Hom "HOL-Algebra/Ring"
begin
section {* Max-Polynomial Interpretations *}
subsection {* Missing product_lists *}
lemma product_lists_eq_Nil_iff [simp]: "product_lists xss = [] ⟷ [] ∈ set xss"
by (induct xss, auto)
text {*
Clearly the above simp rule is in a good direction. But also
@{term "product_lists xss = []"} is a good simplification rule.
*}
lemma product_lists_Nil[simp]: "[] ∈ set xss ⟹ product_lists xss = []" by simp
primrec product_indices where
"product_indices [] = [[]]"
| "product_indices (n#ns) = concat (map (λx. map (Cons x) (product_indices ns)) [0..<n])"
lemma length_product_indices[simp]:
"length (product_indices ns) = prod_list ns"
by (induct ns, auto simp: length_concat o_def sum_list_triv)
lemma product_lists_indices:
"product_lists xss = map (zipf nth xss) (product_indices (map length xss))"
by (induct xss, auto simp: o_def map_concat intro!: arg_cong[of _ _ concat] nth_equalityI)
lemma length_product_lists' [simp]:
"length (product_lists xss) = prod_list (map length xss)"
by (simp add: product_lists_indices)
lemma product_lists_map_map:
"product_lists (map (map f) xss) = map (map f) (product_lists xss)"
by (induct xss, auto simp: o_def product_lists_indices)
lemma product_lists_elements:
"[] ∉ set xss ⟹ ⋃ set (map set (product_lists xss)) = ⋃ set (map set xss)"
by (induct xss, auto)
lemma product_lists_elements2:
assumes "xs ∈ set (product_lists xss)" and "x ∈ set xs"
shows "∃xs' ∈ set xss. x ∈ set xs'"
by (insert assms product_lists_elements, cases "[] ∈ set xss", auto)
lemma in_set_product_lists_nth:
assumes "ys ∈ set (product_lists xss)"
and "i < length xss"
shows "ys ! i ∈ set (xss ! i)"
proof (insert assms, induct xss arbitrary: i ys)
case (Cons xs xss)
then show ?case by (cases i, auto)
qed simp
subsection {* Fundamental Results *}
lemma prod_list_map_filter:
assumes "⋀x. x ∈ set xs ⟹ ¬ P x ⟹ f x = 1"
shows "prod_list (map f (filter P xs)) = prod_list (map f xs)"
using assms by (induct xs, auto)
context non_strict_order
begin
lemma antisym: "x ≤ y ⟹ y ≤ x ⟹ x = y"
using max_comm[of x y] by (auto simp: max_def)
lemma total: "x ≤ y ∨ y ≤ x"
by (metis max_ge_y max_def)
end
hide_class SN_Orders.ordered_semiring_0 SN_Orders.ordered_semiring_1
context zero_less_one begin
subclass zero_neq_one using zero_less_one by (unfold_locales, blast)
lemma zero_le_one[intro!]: "0 ≤ 1" by (auto simp: le_less)
end
class ordered_semigroup_mult_zero = order + semigroup_mult + mult_zero +
assumes mult_right_mono: "⋀a b c. a ≤ b ⟹ c ≥ 0 ⟹ a * c ≤ b * c"
assumes mult_left_mono: "⋀a b c. a ≤ b ⟹ c ≥ 0 ⟹ c * a ≤ c * b"
begin
lemma mult_mono: "a ≤ b ⟹ c ≤ d ⟹ 0 ≤ b ⟹ 0 ≤ c ⟹ a * c ≤ b * d"
apply (erule (1) mult_right_mono [THEN order_trans])
apply (erule (1) mult_left_mono)
done
lemma mult_mono': "a ≤ b ⟹ c ≤ d ⟹ 0 ≤ a ⟹ 0 ≤ c ⟹ a * c ≤ b * d"
by (rule mult_mono) (fast intro: order_trans)+
lemma mult_nonneg_nonneg [simp]: "0 ≤ a ⟹ 0 ≤ b ⟹ 0 ≤ a * b"
using mult_left_mono [of 0 b a] by simp
lemma mult_nonneg_nonpos: "0 ≤ a ⟹ b ≤ 0 ⟹ a * b ≤ 0"
using mult_left_mono [of b 0 a] by simp
lemma mult_nonpos_nonneg: "a ≤ 0 ⟹ 0 ≤ b ⟹ a * b ≤ 0"
using mult_right_mono [of a 0 b] by simp
text ‹Legacy -- use @{thm [source] mult_nonpos_nonneg}.›
lemma mult_nonneg_nonpos2: "0 ≤ a ⟹ b ≤ 0 ⟹ b * a ≤ 0"
by (drule mult_right_mono [of b 0]) auto
lemma split_mult_neg_le: "(0 ≤ a ∧ b ≤ 0) ∨ (a ≤ 0 ∧ 0 ≤ b) ⟹ a * b ≤ 0"
by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
end
subclass (in Rings.ordered_semiring_0) ordered_semigroup_mult_zero
by (unfold_locales; fact mult_right_mono mult_left_mono)
class ordered_monoid_mult_zero = ordered_semigroup_mult_zero + monoid_mult + zero_less_one
begin
lemma prod_list_nonneg:
assumes "⋀x. x ∈ set xs ⟹ x ≥ 0"
shows "prod_list xs ≥ 0"
using assms by (induct xs, auto)
end
class ordered_semiring_1 = ordered_semiring_0 + monoid_mult + zero_less_one
begin
subclass semiring_1..
lemma prod_list_nonneg:
assumes "⋀x. x ∈ set xs ⟹ x ≥ 0"
shows "prod_list xs ≥ 0"
using assms by (induct xs, auto)
lemma prod_list_nonneg_nth:
assumes "⋀i. i < length xs ⟹ xs ! i ≥ 0"
shows "prod_list xs ≥ 0"
using assms by (auto intro!: prod_list_nonneg simp: in_set_conv_nth)
end
text {* Currently (Isabelle 2017), @{class linordered_semiring_1} is not a subclass of
@{class ordered_semiring_1}, but in the difference everything is negative, so the axioms of
@{class ordered_semiring} make no sense.
*}
lemma (in linordered_semiring_1)
assumes a0: "0 < a" shows "0 < 1"
proof (rule ccontr)
assume "¬ 0 < 1" then have "1 ≤ 0" by auto
from mult_nonpos_nonneg[OF this] a0 have "a ≤ 0" by auto
with a0 show False by auto
qed
class linordered_semiring_1 = linordered_semiring + semiring_1 + zero_less_one
subclass (in linordered_semiring_1) ordered_semiring_1..
instance nat :: linordered_semiring_1..
instance int :: linordered_semiring_1..
instance rat :: linordered_semiring_1..
instance real :: linordered_semiring_1..
lemma concat_map_map [simp]: "concat (map (map f) xss) = map f (concat xss)"
by (induct xss, auto)
lemma Max_le_Max:
assumes X: "finite X" "X ≠ {}" and Y: "finite Y" "Y ≠ {}"
shows "Max X ≤ Max Y ⟷ (∀x∈X. ∃y∈Y. x ≤ y)"
by (meson Max.boundedE Max_ge_iff Max_in assms)
lemma Max_less_Max:
assumes X: "finite X" "X ≠ {}" and Y: "finite Y" "Y ≠ {}"
shows "Max X < Max Y ⟷ (∀x∈X. ∃y∈Y. x < y)"
by (meson Max_less_iff assms eq_Max_iff less_le_trans)
definition max_list1 where
"max_list1 xs ≡ if xs = [] then undefined else foldr max (butlast xs) (last xs)"
lemma max_list1_Cons[simp]: "max_list1 (x#xs) = (if xs = [] then x else max x (max_list1 xs))"
by (auto simp: max_list1_def)
text {* @{const max_list1} is @{term "Max ∘ set"}, but the latter require a total order. *}
lemma max_list1_as_Max:
shows "max_list1 xs = Max (set xs)"
proof (cases "xs = []")
case True
then show ?thesis by (auto simp: Max.eq_fold' option.the_def max_list1_def)
next
case False
then show ?thesis
proof (induct xs)
case (Cons x xs)
then show ?case by (cases "xs = []", auto simp: max_def)
qed auto
qed
definition max_list where
"max_list xs ≡ foldr max xs bot"
lemma max_list_Nil[simp]: "max_list [] = bot"
and max_list_Cons[simp]: "max_list (x#xs) = max x (max_list xs)"
by (auto simp: max_list_def)
lemma (in order_bot) max_bot [simp]:
"max bot x = x" "max x bot = x" by (auto simp: max_def)
lemma max_list_as_max_list1_bot:
shows "max_list xs = max_list1 (xs @ [bot])"
by (induct xs, auto)
lemma max_list_as_max_list1:
fixes xs :: "'a :: order_bot list"
assumes "xs ≠ []" shows "max_list xs = max_list1 xs"
by (insert assms, induct xs, auto)
lemma max_list_append [simp]:
fixes xs ys :: "'a :: {linorder,order_bot} list"
shows "max_list (xs @ ys) = max (max_list xs) (max_list ys)"
by (induct xs arbitrary: ys, auto simp: ac_simps)
lemma max_list_concat:
fixes xss :: "'a :: {linorder,order_bot} list list"
shows "max_list (concat xss) = max_list (map max_list xss)"
by (induct xss, auto)
lemma max_list1_append:
fixes xs ys :: "'a :: linorder list"
shows "max_list1 (xs @ ys) = (if xs = [] then max_list1 ys else if ys = [] then max_list1 xs else max (max_list1 xs) (max_list1 ys))"
by (induct xs arbitrary: ys, auto simp: ac_simps)
lemma max_list1_concat:
fixes xss :: "'a :: linorder list list"
assumes "[] ∉ set xss"
shows "max_list1 (concat xss) = max_list1 (map max_list1 xss)"
by (insert assms, induct xss, simp, insert List.last_in_set, force simp: max_list1_append)
lemma max_list1_mem: "xs ≠ [] ⟹ max_list1 xs ∈ set xs"
proof (induct xs)
case (Cons x xs)
then show ?case by (cases xs, auto simp: max_def)
qed auto
lemma max_list_map_filter:
fixes f :: "_ ⇒ 'a :: order_bot"
assumes "⋀x. x ∈ set xs ⟹ ¬ P x ⟹ f x = bot"
shows "max_list (map f (filter P xs)) = max_list (map f xs)"
using assms by (induct xs, auto)
lemma max_list_cong:
assumes "⋀x. x ∈ set xs ⟹ f x = g x"
shows "max_list (map f xs) = max_list (map g xs)"
using assms by (induct xs, auto)
lemma hom_max:
assumes "f x = f y ∨ (f x ≤ f y ⟷ x ≤ y)"
shows "f (max x y) = max (f x) (f y)"
using assms by (auto simp: max_def)
lemma hom_max_list1:
assumes "⋀x y. x ∈ set xs ⟹ y ∈ set xs ⟹ f x = f y ∨ (f x ≤ f y ⟷ x ≤ y)" and "xs ≠ []"
shows "f (max_list1 xs) = max_list1 (map f xs)"
proof (insert assms, induct xs)
case IH: (Cons x xs)
show ?case
proof (cases xs)
case [simp]: (Cons y ys)
from IH have "max_list1 (map f xs) = f (max_list1 xs)" by auto
with max_list1_mem[of xs] hom_max[of f, OF IH.prems(1)]
show ?thesis by auto
qed auto
qed auto
locale ord_hom = fixes hom
assumes ord_hom_condition: "⋀x y. hom x = hom y ∨ (hom x ≤ hom y ⟷ x ≤ y)"
begin
lemmas hom_max = hom_max[of hom, OF ord_hom_condition]
lemmas hom_max_list1 = hom_max_list1[of _ hom, OF ord_hom_condition]
end
locale ord_hom_strict = fixes hom
assumes hom_le_hom[simp]: "⋀x y. hom x ≤ hom y ⟷ x ≤ y"
begin
sublocale ord_hom by (unfold_locales, auto)
end
locale linorder_hom = fixes hom :: "'a :: linorder ⇒ 'b :: linorder"
assumes mono: "x ≤ y ⟹ hom x ≤ hom y"
begin
sublocale ord_hom using mono by (unfold_locales, auto)
text {* @{thm mono_Max_commute} is derivable *}
lemma hom_Max:
assumes finX: "finite X" and X0: "X ≠ {}" shows "hom (Max X) = Max (hom ` X)"
proof-
obtain xs where "set xs = X" using finX finite_list by auto
with X0 hom_max_list1[unfolded max_list1_as_Max, of xs] show ?thesis by auto
qed
end
interpretation add_hom: ord_hom "λy :: 'a :: ordered_ab_semigroup_add_imp_le. x + y"
by (unfold_locales, auto)
interpretation add_hom_right: ord_hom "λx :: 'a :: ordered_ab_semigroup_add_imp_le. x + y"
by (unfold_locales, auto)
interpretation int_hom: linorder_hom int by (unfold_locales, auto)
lemma sum_list_max_list1:
fixes xss :: "'a :: {linordered_semiring} list list"
assumes "[] ∉ set xss"
shows "sum_list (map max_list1 xss) = max_list1 (map sum_list (product_lists xss))"
proof (insert assms, induct xss)
case (Cons xs xss)
show ?case
proof (cases "xss = []")
case False
have [simp]: "max_list1 (map (λxs. x + sum_list xs) (product_lists xss)) = x + sum_list (map max_list1 xss)" for x
proof-
have "map (λxs. x + sum_list xs) (product_lists xss) = map (λy. x + y) (map sum_list (product_lists xss))"
by auto
also have "max_list1 … = x + max_list1 (map sum_list (product_lists xss))"
apply (rule hom_max_list1[symmetric])
using False Cons by auto
also have "… = x + sum_list (map max_list1 xss)" using Cons by auto
finally show ?thesis.
qed
show ?thesis
apply (auto simp:map_concat)
apply (subst max_list1_concat)
using Cons apply force
apply (simp add: o_def)
apply (subst add_hom_right.hom_max_list1) using False Cons.prems by auto
qed (auto simp: o_def)
qed simp
lemma prod_list_max_list1:
fixes xss :: "'a :: {linordered_nonzero_semiring,linordered_semiring} list list"
assumes "[] ∉ set xss" and "⋀x. x ∈ ⋃(set ` set xss) ⟹ x ≥ 0"
shows "prod_list (map max_list1 xss) = max_list1 (map prod_list (product_lists xss))"
proof (insert assms, induct xss)
case (Cons xs xss)
show ?case
proof (cases "xss = []")
case False
{ fix x :: 'a assume "x ∈ set xs"
with Cons.prems have x0: "x ≥ 0" by auto
have "map (λxs. x * prod_list xs) (product_lists xss) = map (λy. x * y) (map prod_list (product_lists xss))"
by auto
also have "max_list1 … = x * max_list1 (map prod_list (product_lists xss))"
apply (rule hom_max_list1[symmetric])
using False Cons.prems x0 by (auto intro!: monoI mult_left_mono)
also have "… = x * prod_list (map max_list1 xss)" using Cons by auto
finally have "max_list1 (map (λxs. x * prod_list xs) (product_lists xss)) = …".
}
note 1 = map_cong[OF refl this]
from Cons.prems have "(⋀x. x ∈ ⋃(set ` set xss) ⟹ x ≥ 0)" "[] ∉ set xss" by auto
then have 2: "prod_list (map max_list1 xss) ≥ 0"
proof (induct xss)
case (Cons xs xss)
then have "max_list1 xs ≥ 0" using max_list1_mem[of xs] by auto
with Cons show ?case by auto
qed (auto)
from Cons.prems have 3: "xs ≠ []" by auto
have "max_list1 xs ≥ 0" using Cons.prems max_list1_mem[of xs] by auto
show ?thesis
apply (auto simp:map_concat)
apply (subst max_list1_concat)
using Cons.prems apply force
apply (simp add: o_def)
apply (subst 1, assumption)
apply (subst hom_max_list1[of _ "λx. x * _"]) using mult_right_mono[OF _2] 3 by auto
qed (auto simp: o_def)
qed simp
text {* We implement max-polynomial interpretations as an instance of @{locale encoded_algebra}.
As a target algebra, we introduce a $G$-algebra where $G = \{+,\times,\max\}$. *}
locale max_poly_locale
begin
datatype sig = ConstF nat | SumF | ProdF | MaxF
primrec I where
"I (ConstF n) = (λx. n)"
| "I SumF = sum_list"
| "I ProdF = prod_list"
| "I MaxF = max_list"
abbreviation const where "const n ≡ Fun (ConstF n) []"
sublocale wf_weak_mono_algebra less_eq less I
proof
fix f ls rs and a b :: nat
assume ba: "b ≤ a"
then show "I f (ls @ b # rs) ≤ I f (ls @ a # rs)"
proof(cases f)
case [simp]: MaxF
note ba
also have "a ≤ max_list (ls @ a # rs)" by auto
finally show ?thesis by auto
qed auto
qed
sublocale algebra_constant I const by (unfold_locales, auto)
fun simplify where
"simplify (Var x) = Var x"
| "simplify (Fun (ConstF n) ss) = const n"
| "simplify (Fun SumF ss) = (
let ss' = filter (λs. s ≠ const 0) (map simplify ss) in
case ss' of [] ⇒ const 0 | [s] ⇒ s | _ ⇒ Fun SumF ss'
)"
| "simplify (Fun ProdF ss) = (
let ss' = filter (λs. s ≠ const 1) (map simplify ss) in
if const 0 ∈ set ss' then const 0
else case ss' of [] ⇒ const 1 | [s] ⇒ s | _ ⇒ Fun ProdF ss'
)"
| "simplify (Fun MaxF ss) = (
let ss' = filter (λs. s ≠ const 0) (map simplify ss) in
case ss' of [] ⇒ const 0 | [s] ⇒ s | _ ⇒ Fun MaxF ss'
)"
lemma list_caseE:
assumes "case xs of [] ⇒ a | x # ys ⇒ b x ys"
and "xs = [] ⟹ a ⟹ thesis"
and "⋀x ys. xs = x#ys ⟹ b x ys ⟹ thesis"
shows thesis
using assms
by (cases xs, auto)
lemma vars_term_simplify: "vars_term (simplify s) ⊆ vars_term s"
proof (rule subsetI, induct s rule: simplify.induct)
case (1 v)
then show ?case by simp
next
case (2 n ss)
then show ?case by simp
next
case IH: (3 ss)
from IH.prems have "x ∈ ⋃(vars_term ` set (filter (λs. s ≠ const 0) (map simplify ss)))"
by (auto simp: Let_def list.case_distrib simp del: set_filter elim!: list_caseE)
also have "… ⊆ vars_term (Fun SumF ss)" using IH.hyps by auto
finally show ?case.
next
case IH: (4 ss)
let ?ss = "filter (λs. s ≠ const 1) (map simplify ss)"
from IH.prems have "x ∈ ⋃(vars_term ` set ?ss)"
by (cases "const 0 ∈ set ?ss", auto simp: Let_def list.case_distrib simp del: set_filter elim!: list_caseE)
also have "… ⊆ vars_term (Fun ProdF ss)" using IH.hyps by auto
finally show ?case.
next
case IH: (5 ss)
from IH.prems have "x ∈ ⋃(vars_term ` set (filter (λs. s ≠ const 0) (map simplify ss)))"
by (auto simp: Let_def list.case_distrib simp del: set_filter elim!: list_caseE)
also have "… ⊆ vars_term (Fun MaxF ss)" using IH.hyps by auto
finally show ?case.
qed
lemma eval_SumF_filter_0:
"⟦Fun SumF (filter (λs. s ≠ const 0) ss)⟧ = ⟦Fun SumF ss⟧"
by (auto intro!: ext sum_list_map_filter)
lemma eval_MaxF_filter_0:
"⟦Fun MaxF (filter (λs. s ≠ const 0) ss)⟧ = ⟦Fun MaxF ss⟧"
by (auto intro!: ext max_list_map_filter)
lemma eval_ProdF_filter_1:
"⟦Fun ProdF (filter (λs. s ≠ const (Suc 0)) ss)⟧ = ⟦Fun ProdF ss⟧"
by (auto intro!: ext prod_list_map_filter)
lemma eval_ProdF_with_0:
"∃s ∈ set ss. s = const 0 ⟹ ⟦Fun ProdF ss⟧ = ⟦const 0⟧"
by (intro ext, induct ss, auto)
lemma simplify_lemma:
"⟦case ss of [] ⇒ const 0 | [s] ⇒ s | _ ⇒ Fun SumF ss⟧ = ⟦Fun SumF ss⟧"
"⟦case ss of [] ⇒ const 1 | [s] ⇒ s | _ ⇒ Fun ProdF ss⟧ = ⟦Fun ProdF ss⟧"
"⟦case ss of [] ⇒ const 0 | [s] ⇒ s | _ ⇒ Fun MaxF ss⟧ = ⟦Fun MaxF ss⟧"
by (atomize(full), cases ss rule: list_3_cases, auto simp: bot_nat_def)
lemma simplify [simp]: "⟦simplify s⟧ = ⟦s⟧"
proof (intro ext, induct s rule: simplify.induct)
case (1 x α)
then show ?case by simp
next
case (2 n ss α)
then show ?case by (auto simp: simplify_lemma)
next
case (3 ss α)
then show ?case by (auto simp: Let_def simplify_lemma eval_SumF_filter_0 intro!:sum_list_cong)
next
case (4 ss α)
then show ?case
by (force simp: Let_def simplify_lemma eval_ProdF_filter_1[simplified] prod_list_zero_iff image_def intro: prod_list_cong)
next
case (5 ss α)
then show ?case by (auto simp: Let_def simplify_lemma eval_MaxF_filter_0 o_def intro:max_list_cong)
qed
end
derive compare max_poly_locale.sig
thm weak_mono_algebra.weak_mono
interpretation max_poly: max_poly_locale.
subsection {* Translation to Integer Arithmetic *}
context IA_locale
begin
lemma to_int_iff:
assumes α: "assignment α" and s: "s :⇩f IntT" and t: "t :⇩f IntT"
shows "to_int (⟦s⟧α) < to_int (⟦t⟧α) ⟷ ⟦s⟧α < ⟦t⟧α"
and "to_int (⟦s⟧α) ≤ to_int (⟦t⟧α) ⟷ ⟦s⟧α ≤ ⟦t⟧α"
and "to_int (⟦s⟧α) = to_int (⟦t⟧α) ⟷ ⟦s⟧α = ⟦t⟧α"
using s t by (auto dest!: eval_types[OF α])
end
context max_poly_locale
begin
primrec to_IA where
"to_IA (Var x) = [Var (x,IA.IntT)]"
| "to_IA (Fun f ss) = (case f of (ConstF n) ⇒ [Fun (IA.ConstF n) []]
| MaxF ⇒ if ss = [] then [IA.const 0] else concat (map to_IA ss)
| SumF ⇒
if ss = [] then [Fun (IA.SumF 0) []]
else map (Fun (IA.SumF (length ss))) (product_lists (map to_IA ss))
| ProdF ⇒
if ss = [] then [Fun (IA.ProdF 0) []]
else map (Fun (IA.ProdF (length ss))) (product_lists (map to_IA ss))
)"
lemma to_IA_induct[case_names Var ConstF SumF ProdF MaxF SumF0 ProdF0 MaxF0]:
assumes "⋀x. P (Var x)"
and "⋀n ss. P (Fun (ConstF n) ss)"
and "⋀ss. ss ≠ [] ⟹ (⋀s. s ∈ set ss ⟹ P s) ⟹ P (Fun SumF ss)"
and "⋀ss. ss ≠ [] ⟹ (⋀s. s ∈ set ss ⟹ P s) ⟹ P (Fun ProdF ss)"
and "⋀ss. ss ≠ [] ⟹ (⋀s. s ∈ set ss ⟹ P s) ⟹ P (Fun MaxF ss)"
and "P (Fun SumF [])"
and "P (Fun ProdF [])"
and "P (Fun MaxF [])"
shows "P s"
by (insert assms, induction_schema, metis term.exhaust sig.exhaust, lexicographic_order)
lemma to_IA_has_type:
"s' ∈ set (to_IA s) ⟹ IA.has_type s' IA.IntT"
apply (induct s arbitrary:s' rule: to_IA_induct, auto simp:in_set_product_lists_length product_lists_set)
apply (metis length_map list_all2_nthD2 nth_map nth_mem)
apply (metis length_map list_all2_nthD2 nth_map nth_mem)
done
lemma to_IA_eq_NilE[elim!]: "to_IA s = [] ⟹ thesis" by (induct s rule: to_IA_induct, auto)
definition "to_IA_assignment α ≡ λ(x,t). case t of IA.IntT ⇒ IA.Int (int (α x)) | _ ⇒ IA.Bool False"
lemma to_IA_assignment: "IA.assignment (to_IA_assignment α)"
by (intro IA.assignmentI, auto simp: to_IA_assignment_def split: IA.ty.split)
definition "eval_via_IA s α ≡ map (λt. IA.eval t (to_IA_assignment α)) (to_IA s)"
lemma eval_via_IA_eq_NilE[elim!]: "eval_via_IA s α = [] ⟹ thesis"
by (auto simp: eval_via_IA_def)
lemma eval_via_IA_range: "set (eval_via_IA s α) ⊆ range IA.Int"
proof-
have "set (eval_via_IA s α) ⊆ set (map (λt. IA.eval t (to_IA_assignment α)) (to_IA s) @ [IA.Int 0])"
by (unfold eval_via_IA_def, auto)
also have "… ⊆ range IA.Int"
using to_IA_assignment[of α]
by (auto dest!: to_IA_has_type IA.eval_types)
finally show ?thesis.
qed
lemma max_list1_eval_via_IA_range:
"max_list1 (eval_via_IA s α) ∈ range IA.Int"
proof-
note max_list1_mem
also note eval_via_IA_range
finally show ?thesis by force
qed
end
interpretation int_hom: comm_semiring_hom int by (unfold_locales, auto)
instantiation IA.val :: plus
begin
fun plus_val where
"plus_val (IA.Int x) (IA.Int y) = IA.Int (x + y)"
| "plus_val (IA.Bool x) (IA.Bool y) = IA.Bool (x ∨ y)"
instance..
end
instantiation IA.val :: times
begin
fun times_val where
"times_val (IA.Int x) (IA.Int y) = IA.Int (x * y)"
| "times_val (IA.Bool x) (IA.Bool y) = IA.Bool (x ∧ y)"
instance..
end
definition listprod where "listprod G xs ≡ foldr (mult G) xs (one G)"
lemma listprod_Nil[simp]: "listprod G [] = one G" by (auto simp: listprod_def)
lemma listprod_Cons[simp]: "listprod G (x#xs) = mult G x (listprod G xs)" by (auto simp: listprod_def)
lemma nth_ConsI: "(i = 0 ⟹ P x) ⟹ (⋀j. i = Suc j ⟹ P (xs!j)) ⟹ P ((x#xs)!i)"
by (cases i, auto)
lemma (in comm_monoid) listprod_as_finprod:
assumes "set xs ⊆ carrier G"
shows "listprod G xs = finprod G (nth xs) {..<length xs}"
apply (insert assms, induct xs, auto simp: lessThan_Suc_eq_insert_0)
apply (subst finprod_insert)
apply (auto intro!: nth_ConsI[of _ "λx. x ∈ carrier G"])
apply (subst finprod_reindex, auto)
done
definition listsum where "listsum R ≡ listprod ⦇ carrier = carrier R, mult = add R, one = zero R ⦈"
lemma listsum_Nil[simp]: "listsum R [] = zero R" by (auto simp: listsum_def)
lemma listsum_Cons[simp]: "listsum R (x#xs) = add R x (listsum R xs)" by (auto simp: listsum_def)
lemmas (in ring) listsum_as_finsum = add.listprod_as_finprod[folded listsum_def]
context IA_locale begin
definition "ring_Int ≡ ⦇ carrier = range IA.Int, mult = op *, one = IA.Int 1, zero = IA.Int 0, add = op + ⦈"
end
interpretation IA_ring_Int: Ring.ring "IA.ring_Int"
rewrites [simp]: "carrier IA.ring_Int = range IA.Int"
and [simp]: "mult IA.ring_Int = op *"
and [simp]: "one IA.ring_Int = IA.Int 1"
and [simp]: "zero IA.ring_Int = IA.Int 0"
and [simp]: "add IA.ring_Int = op +"
and [simp]: "Units IA.ring_Int = { IA.Int 1, IA.Int (-1) }"
by (unfold_locales, auto simp: IA.ring_Int_def Units_def field_simps zmult_eq_1_iff intro: exI[of _ "-_"])
interpretation IA_Int_hom: plus_hom IA.Int by (unfold_locales, auto)
interpretation IA_Int_hom: ord_hom_strict IA.Int by (unfold_locales, auto)
lemma IA_Int_sum_list: "IA.Int (sum_list xs) = listsum IA.ring_Int (map IA.Int xs)"
by (induct xs, auto simp:lessThan_Suc_eq_insert_0 IA_Int_hom.hom_add)
lemma listsum_IA:
assumes "set vs ⊆ range IA.Int"
shows "listsum IA.ring_Int vs = IA.Int (sum_list (map IA.to_int vs))"
using IA_Int_sum_list[of "map IA.to_int vs"] assms map_idI[of vs "IA.Int ∘ IA.to_int"] by force
context max_poly_locale
begin
lemma eval_via_IA_ge_0: "v ∈ set (eval_via_IA s α) ⟹ IA.to_int v ≥ 0"
proof (unfold eval_via_IA_def, induct s arbitrary:v rule: to_IA_induct)
case (Var x)
then show ?case by (auto simp: to_IA_assignment_def)
next
case (SumF ss)
from this(1,3)
show ?case
apply (auto simp: o_def image_def in_set_product_lists_length intro!:sum_list_ge_0_nth)
apply(drule(1) in_set_product_lists_nth[of _ "map to_IA ss", simplified])
using SumF(2)[OF nth_mem] apply auto
done
next
case (ProdF ss)
from this(1,3)
show ?case
apply (auto simp: o_def image_def in_set_product_lists_length intro!:prod_list_nonneg_nth)
apply(drule in_set_product_lists_nth[of _ "map to_IA ss", simplified])
using ProdF(2)[OF nth_mem] apply auto
done
qed auto
lemma eval_via_IA:
fixes f α
defines "f ≡ λs. eval_via_IA s α"
shows "int (⟦s⟧ α) = IA.to_int (max_list1 (f s))"
proof (induct s rule: to_IA_induct)
case (Var x)
show ?case by (simp add: eval_via_IA_def to_IA_assignment_def IA_Int_hom.hom_max[symmetric] f_def)
next
case (ConstF n ss)
show ?case by (simp add: eval_via_IA_def IA_Int_hom.hom_max[symmetric] f_def)
next
case (SumF ss)
note ss = this(1) and 1 = map_ext[OF this(2)[unfolded atomize_imp]]
have "int (⟦Fun SumF ss⟧ α) = (∑s←ss. IA.to_int (max_list1 (f s)))"
by (auto simp: image_def int_hom.hom_sum_list o_def 1)
also have "… = (∑s←ss. (max_list1 (map IA.to_int (f s))))"
apply (rule arg_cong[of _ _sum_list])
apply (rule map_cong[OF refl])
apply (rule hom_max_list1)
by (auto simp: o_def f_def dest!: subsetD[OF eval_via_IA_range])
also have "… = sum_list (map max_list1 (map (map IA.to_int) (map f ss)))"
by (auto simp: o_def)
also have "… = max_list1 (map sum_list (product_lists (map (map IA.to_int) (map f ss))))"
by (intro sum_list_max_list1, auto simp:o_def f_def)
also have "… = max_list1 (map sum_list (product_lists (map (map (IA.to_int ∘ (λt. IA.eval t (to_IA_assignment α)))) (map to_IA ss))))"
by (auto simp: o_def f_def eval_via_IA_def)
also have "… = max_list1 (map IA.to_int (f (Fun SumF ss)))"
by (subst product_lists_map_map, auto simp: o_def f_def eval_via_IA_def ss)
also have "… = IA.to_int (max_list1 (f (Fun SumF ss)))"
by (rule hom_max_list1[symmetric], auto simp: f_def dest!: subsetD[OF eval_via_IA_range])
finally show ?case.
next
case (ProdF ss)
note ss = this(1) and 1 = map_ext[OF this(2)[unfolded atomize_imp]]
have "int (⟦Fun ProdF ss⟧ α) = (∏s←ss. IA.to_int (max_list1 (f s)))"
by (auto simp: image_def int_hom.hom_prod_list o_def 1)
also have "… = (∏s←ss. (max_list1 (map IA.to_int (f s))))"
apply (rule arg_cong[of _ _prod_list])
apply (rule map_cong[OF refl])
apply (rule hom_max_list1)
by (auto simp: o_def f_def dest!: subsetD[OF eval_via_IA_range])
also have "… = prod_list (map max_list1 (map (map IA.to_int) (map f ss)))"
by (auto simp: o_def)
also have "… = max_list1 (map prod_list (product_lists (map (map IA.to_int) (map f ss))))"
by (intro prod_list_max_list1, auto simp:o_def f_def intro:eval_via_IA_ge_0)
also have "… = max_list1 (map prod_list (product_lists (map (map (IA.to_int ∘ (λt. IA.eval t (to_IA_assignment α)))) (map to_IA ss))))"
by (auto simp: o_def f_def eval_via_IA_def)
also have "… = max_list1 (map IA.to_int (f (Fun ProdF ss)))"
by (subst product_lists_map_map, auto simp: o_def f_def eval_via_IA_def ss)
also have "… = IA.to_int (max_list1 (f (Fun ProdF ss)))"
by (rule hom_max_list1[symmetric], auto simp: f_def dest!: subsetD[OF eval_via_IA_range])
finally show ?case.
next
case (MaxF ss)
note ss = this(1) and 1 = map_ext[OF this(2)[unfolded atomize_imp]]
have "⟦Fun MaxF ss⟧α = max_list1 (map (λs. ⟦s⟧α) ss)"
using ss by (auto simp: max_list_as_max_list1)
also have "int … = max_list1 (map (λx. IA.to_int (max_list1 (f x))) ss)"
using ss by (auto simp: o_def int_hom.hom_max_list1 1)
also have "… = max_list1 (map (λs. max_list1 (map IA.to_int (f s))) ss)"
apply (rule arg_cong[of _ _ max_list1])
apply (rule map_cong[OF refl])
apply (rule hom_max_list1)
by (auto simp: o_def f_def dest!: subsetD[OF eval_via_IA_range])
also have "… = max_list1 (map max_list1 (map (map IA.to_int) (map f ss)))"
by (auto simp: o_def)
also have "… = max_list1 (concat (map (map IA.to_int ∘ f) ss))"
apply (subst max_list1_concat[symmetric])
using ss by (auto simp: f_def eval_via_IA_def)
also have "… = max_list1 (concat (map (map (IA.to_int ∘ (λt. IA.eval t (to_IA_assignment α)))) (map to_IA ss)))"
by (auto simp: o_def f_def eval_via_IA_def)
also have "… = max_list1 (map IA.to_int (f (Fun MaxF ss)))"
apply (unfold concat_map_map)
by (auto simp: o_def f_def eval_via_IA_def ss)
also have "… = IA.to_int (max_list1 (f (Fun MaxF ss)))"
by (rule hom_max_list1[symmetric], auto simp: f_def dest!: subsetD[OF eval_via_IA_range])
finally show ?case.
qed (auto simp: f_def eval_via_IA_def bot_nat_def)
definition le_via_IA (infix "⊑⇩I" 50) where "s ⊑⇩I t ≡
Conjunction (map (λs'. disj_atoms (map (λt'. Fun IA.LeF [s', t']) (to_IA t))) (to_IA s))"
lemma formula_le_via_IA [intro!]: "IA.formula (s ⊑⇩I t)"
by (auto simp: le_via_IA_def less_Suc_eq dest: to_IA_has_type)
lemma le_via_IA:
assumes "IA.valid (s ⊑⇩I t)" shows "s ⊑⇩t t"
proof
fix α :: "_ ⇒ nat"
from IA.validD[OF assms to_IA_assignment, of α]
have "∀s' ∈ set (to_IA s). ∃t' ∈ set (to_IA t).
IA.eval s' (to_IA_assignment α) ≤ IA.eval t' (to_IA_assignment α)"
by (auto simp: le_via_IA_def IA.to_int_iff[OF to_IA_assignment to_IA_has_type to_IA_has_type] elim!: ballE)
then have "max_list1 (eval_via_IA s α) ≤ max_list1 (eval_via_IA t α)"
by (unfold max_list1_as_Max eval_via_IA_def, subst Max_le_Max, auto)
then have "int (⟦s⟧ α) ≤ int (⟦t⟧ α)"
unfolding eval_via_IA
by (metis IA_Int_hom.hom_le_hom IA.val.sel(1) imageE max_list1_eval_via_IA_range)
then show "⟦s⟧ α ≤ ⟦t⟧ α" by auto
qed
definition less_via_IA (infix "⊏⇩I" 50) where "s ⊏⇩I t ≡
Conjunction (map (λs'. disj_atoms (map (λt'. Fun IA.LessF [s', t']) (to_IA t))) (to_IA s))"
lemma formula_less_via_IA [intro!]: "IA.formula (s ⊏⇩I t)"
by (auto simp: less_via_IA_def less_Suc_eq dest: to_IA_has_type)
lemma less_via_IA:
assumes "IA.valid (s ⊏⇩I t)" shows "s ⊏⇩t t"
proof
fix α :: "_ ⇒ nat"
from IA.validD[OF assms to_IA_assignment, of α]
have "∀s' ∈ set (to_IA s). ∃t' ∈ set (to_IA t). IA.eval s' (to_IA_assignment α) < IA.eval t' (to_IA_assignment α)"
by (auto simp: less_via_IA_def IA.to_int_iff[OF to_IA_assignment to_IA_has_type to_IA_has_type] elim!: ballE)
then have "max_list1 (eval_via_IA s α) < max_list1 (eval_via_IA t α)"
by (unfold max_list1_as_Max eval_via_IA_def, subst Max_less_Max, auto)
then have "int (⟦s⟧ α) < int (⟦t⟧ α)"
unfolding eval_via_IA
by (metis IA.less_IA_value_simps(3) IA.val.collapse(1) IA.val.discI(1) imageE max_list1_eval_via_IA_range)
then show "⟦s⟧ α < ⟦t⟧ α" by auto
qed
end
subsection {* Max-Polynomial Interpretations *}
text {* Now we encode arbitrary $F$-terms into the @{type max_poly.sig}-terms. *}
locale max_poly_encoding = encoded_ordered_algebra
where less_eq = "op ≤" and less = "op <" and I = max_poly.I
begin
sublocale encoded_wf_weak_mono_algebra where less_eq = "op ≤" and less = "op <" and I = max_poly.I
by (unfold_locales, fact max_poly.append_Cons_le_append_Cons)
lemmas redpair = redpair.redpair_axioms
lemma less_term_via_IA:
assumes "IA.valid (encode s ⊏⇩I encode t)" shows "s ⊏⇩t t"
using max_poly.less_via_IA[OF assms] by (auto intro!: less_termI)
lemma less_eq_term_via_IA:
assumes "IA.valid (encode s ⊑⇩I encode t)" shows "s ⊑⇩t t"
using max_poly.le_via_IA[OF assms] by (auto intro!: less_eq_termI)
lemma ws_fun_arg_via_IA:
assumes "IA.valid (Var i ⊑⇩I E f n)"
shows "ws_fun_arg (rel_of op ⊒⇩t) (f,n) i"
proof (intro ws_fun_argI, unfold mem_Collect_eq prod.case, intro less_eq_termI)
fix ts :: "('a,'b) term list" and α
assume n: "length ts = n" and i_n: "i < n"
note max_poly.le_via_IA[OF assms]
then
have "α i ≤ max_poly.eval (E f n) α" for α by auto
note this[of "λi. ⟦ts!i⟧α"]
also have "target.eval (E f n) (λi. ⟦ts ! i⟧ α) = ⟦Fun f ts⟧ α"
using n encoder.var_domain by auto
finally show "⟦ts ! i⟧ α ≤ ⟦Fun f ts⟧ α".
qed
end
end