Theory Multiset_Extension2
section ‹Multiset extension of order pairs in the other direction›
text ‹Many term orders are formulated in the other direction, i.e., they use
strong normalization of $>$ instead of well-foundedness of $<$. Here, we
flip the direction of the multiset extension of two orders, connect it to existing interfaces,
and prove some further properties of the multiset extension.›
theory Multiset_Extension2
imports
List_Order
Multiset_Extension_Pair
begin
subsection ‹List based characterization of @{const multpw}›
lemma multpw_listI:
assumes "length xs = length ys" "X = mset xs" "Y = mset ys"
"∀i. i < length ys ⟶ (xs ! i, ys ! i) ∈ ns"
shows "(X, Y) ∈ multpw ns"
using assms
proof (induct xs arbitrary: ys X Y)
case (Nil ys) then show ?case by (cases ys) (auto intro: multpw.intros)
next
case Cons1: (Cons x xs ys' X Y) then show ?case
proof (cases ys')
case (Cons y ys)
then have "∀i. i < length ys ⟶ (xs ! i, ys ! i) ∈ ns" using Cons1(5) by fastforce
then show ?thesis using Cons1(2,5) by (auto intro!: multpw.intros simp: Cons(1) Cons1)
qed auto
qed
lemma multpw_listE:
assumes "(X, Y) ∈ multpw ns"
obtains xs ys where "length xs = length ys" "X = mset xs" "Y = mset ys"
"∀i. i < length ys ⟶ (xs ! i, ys ! i) ∈ ns"
using assms
proof (induct X Y arbitrary: thesis rule: multpw.induct)
case (add x y X Y)
then obtain xs ys where "length xs = length ys" "X = mset xs"
"Y = mset ys" "(∀i. i < length ys ⟶ (xs ! i, ys ! i) ∈ ns)" by blast
then show ?case using add(1) by (intro add(4)[of "x # xs" "y # ys"]) (auto, case_tac i, auto)
qed auto
subsection‹Definition of the multiset extension of $>$-orders›
text‹We define here the non-strict extension of the order pair $(\geqslant, >)$ --
usually written as (ns, s) in the sources --
by just flipping the directions twice.›
definition ns_mul_ext :: "'a rel ⇒ 'a rel ⇒ 'a multiset rel"
where "ns_mul_ext ns s ≡ (mult2_alt_ns (ns¯) (s¯))¯"
lemma ns_mul_extI:
assumes "A = A1 + A2" and "B = B1 + B2"
and "(A1, B1) ∈ multpw ns"
and "⋀b. b ∈# B2 ⟹ ∃a. a ∈# A2 ∧ (a, b) ∈ s"
shows "(A, B) ∈ ns_mul_ext ns s"
using assms by (auto simp: ns_mul_ext_def multpw_converse intro!: mult2_alt_nsI)
lemma ns_mul_extE:
assumes "(A, B) ∈ ns_mul_ext ns s"
obtains A1 A2 B1 B2 where "A = A1 + A2" and "B = B1 + B2"
and "(A1, B1) ∈ multpw ns"
and "⋀b. b ∈# B2 ⟹ ∃a. a ∈# A2 ∧ (a, b) ∈ s"
using assms by (auto simp: ns_mul_ext_def multpw_converse elim!: mult2_alt_nsE)
lemmas ns_mul_extI_old = ns_mul_extI[OF _ _ multpw_listI[OF _ refl refl], rule_format]
text‹Same for the "greater than" order on multisets.›
definition s_mul_ext :: "'a rel ⇒ 'a rel ⇒ 'a multiset rel"
where "s_mul_ext ns s ≡ (mult2_alt_s (ns¯) (s¯))¯"
lemma s_mul_extI:
assumes "A = A1 + A2" and "B = B1 + B2"
and "(A1, B1) ∈ multpw ns"
and "A2 ≠ {#}" and "⋀b. b ∈# B2 ⟹ ∃a. a ∈# A2 ∧ (a, b) ∈ s"
shows "(A, B) ∈ s_mul_ext ns s"
using assms by (auto simp: s_mul_ext_def multpw_converse intro!: mult2_alt_sI)
lemma s_mul_extE:
assumes "(A, B) ∈ s_mul_ext ns s"
obtains A1 A2 B1 B2 where "A = A1 + A2" and "B = B1 + B2"
and "(A1, B1) ∈ multpw ns"
and "A2 ≠ {#}" and "⋀b. b ∈# B2 ⟹ ∃a. a ∈# A2 ∧ (a, b) ∈ s"
using assms by (auto simp: s_mul_ext_def multpw_converse elim!: mult2_alt_sE)
lemmas s_mul_extI_old = s_mul_extI[OF _ _ multpw_listI[OF _ refl refl], rule_format]
subsection‹Basic properties›
lemma s_mul_ext_mono:
assumes "ns ⊆ ns'" "s ⊆ s'" shows "s_mul_ext ns s ⊆ s_mul_ext ns' s'"
unfolding s_mul_ext_def using assms mono_mult2_alt[of "ns¯" "ns'¯" "s¯" "s'¯"] by simp
lemma ns_mul_ext_mono:
assumes "ns ⊆ ns'" "s ⊆ s'" shows "ns_mul_ext ns s ⊆ ns_mul_ext ns' s'"
unfolding ns_mul_ext_def using assms mono_mult2_alt[of "ns¯" "ns'¯" "s¯" "s'¯"] by simp
lemma s_mul_ext_local_mono:
assumes sub: "(set_mset xs × set_mset ys) ∩ ns ⊆ ns'" "(set_mset xs × set_mset ys) ∩ s ⊆ s'"
and rel: "(xs,ys) ∈ s_mul_ext ns s"
shows "(xs,ys) ∈ s_mul_ext ns' s'"
using rel s_mul_ext_mono[OF sub] mult2_alt_local[of ys xs False "ns¯" "s¯"]
by (auto simp: s_mul_ext_def converse_Int ac_simps converse_Times)
lemma ns_mul_ext_local_mono:
assumes sub: "(set_mset xs × set_mset ys) ∩ ns ⊆ ns'" "(set_mset xs × set_mset ys) ∩ s ⊆ s'"
and rel: "(xs,ys) ∈ ns_mul_ext ns s"
shows "(xs,ys) ∈ ns_mul_ext ns' s'"
using rel ns_mul_ext_mono[OF sub] mult2_alt_local[of ys xs True "ns¯" "s¯"]
by (auto simp: ns_mul_ext_def converse_Int ac_simps converse_Times)
lemma s_mul_ext_ord_s [mono]:
assumes "⋀s t. ord s t ⟶ ord' s t"
shows "(s, t) ∈ s_mul_ext ns {(s,t). ord s t} ⟶ (s, t) ∈ s_mul_ext ns {(s,t). ord' s t}"
using assms s_mul_ext_mono by (metis (mono_tags) case_prod_conv mem_Collect_eq old.prod.exhaust subset_eq)
lemma ns_mul_ext_ord_s [mono]:
assumes "⋀s t. ord s t ⟶ ord' s t"
shows "(s, t) ∈ ns_mul_ext ns {(s,t). ord s t} ⟶ (s, t) ∈ ns_mul_ext ns {(s,t). ord' s t}"
using assms ns_mul_ext_mono by (metis (mono_tags) case_prod_conv mem_Collect_eq old.prod.exhaust subset_eq)
text‹The empty multiset is the minimal element for these orders›
lemma ns_mul_ext_bottom: "(A,{#}) ∈ ns_mul_ext ns s"
by (auto intro!: ns_mul_extI)
lemma ns_mul_ext_bottom_uniqueness:
assumes "({#},A) ∈ ns_mul_ext ns s"
shows "A = {#}"
using assms by (auto simp: ns_mul_ext_def mult2_alt_ns_def)
lemma ns_mul_ext_bottom2:
assumes "(A,B) ∈ ns_mul_ext ns s"
and "B ≠ {#}"
shows "A ≠ {#}"
using assms by (auto simp: ns_mul_ext_def mult2_alt_ns_def)
lemma s_mul_ext_bottom:
assumes "A ≠ {#}"
shows "(A,{#}) ∈ s_mul_ext ns s"
using assms by (auto simp: s_mul_ext_def mult2_alt_s_def)
lemma s_mul_ext_bottom_strict:
"({#},A) ∉ s_mul_ext ns s"
by (auto simp: s_mul_ext_def mult2_alt_s_def)
text‹Obvious introduction rules.›
lemma all_ns_ns_mul_ext:
assumes "length as = length bs"
and "∀i. i < length bs ⟶ (as ! i, bs ! i) ∈ ns"
shows "(mset as, mset bs) ∈ ns_mul_ext ns s"
using assms by (auto intro!: ns_mul_extI[of _ _ "{#}" _ _ "{#}"] multpw_listI)
lemma all_s_s_mul_ext:
assumes "A ≠ {#}"
and "∀b. b ∈# B ⟶ (∃a. a ∈# A ∧ (a,b) ∈ s)"
shows "(A, B) ∈ s_mul_ext ns s"
using assms by (auto intro!: s_mul_extI[of _ "{#}" _ _ "{#}"] multpw_listI)
text‹Being stricly lesser than implies being lesser than›
lemma s_ns_mul_ext:
assumes "(A, B) ∈ s_mul_ext ns s"
shows "(A, B) ∈ ns_mul_ext ns s"
using assms by (simp add: s_mul_ext_def ns_mul_ext_def mult2_alt_s_implies_mult2_alt_ns)
text‹The non-strict order is reflexive.›
lemma multpw_refl':
assumes "locally_refl ns A"
shows "(A, A) ∈ multpw ns"
proof -
have "Restr Id (set_mset A) ⊆ ns" using assms by (auto simp: locally_refl_def)
from refl_multpw[of Id] multpw_local[of A A Id] mono_multpw[OF this]
show ?thesis by (auto simp: refl_on_def)
qed
lemma ns_mul_ext_refl_local:
assumes "locally_refl ns A"
shows "(A, A) ∈ ns_mul_ext ns s"
using assms by (auto intro!: ns_mul_extI[of A A "{#}" A A "{#}" ns s] multpw_refl')
lemma ns_mul_ext_refl:
assumes "refl ns"
shows "(A, A) ∈ ns_mul_ext ns s"
using assms ns_mul_ext_refl_local[of ns A s] unfolding refl_on_def locally_refl_def by auto
text‹The orders are union-compatible›
lemma ns_s_mul_ext_union_multiset_l:
assumes "(A, B) ∈ ns_mul_ext ns s"
and "C ≠ {#}"
and "∀d. d ∈# D ⟶ (∃c. c ∈# C ∧ (c,d) ∈ s)"
shows "(A + C, B + D) ∈ s_mul_ext ns s"
using assms unfolding ns_mul_ext_def s_mul_ext_def
by (auto intro!: converseI mult2_alt_ns_s_add mult2_alt_sI[of _ "{#}" _ _ "{#}"])
lemma s_mul_ext_union_compat:
assumes "(A, B) ∈ s_mul_ext ns s"
and "locally_refl ns C"
shows "(A + C, B + C) ∈ s_mul_ext ns s"
using assms ns_mul_ext_refl_local[OF assms(2)] unfolding ns_mul_ext_def s_mul_ext_def
by (auto intro!: converseI mult2_alt_s_ns_add)
lemma ns_mul_ext_union_compat:
assumes "(A, B) ∈ ns_mul_ext ns s"
and "locally_refl ns C"
shows "(A + C, B + C) ∈ ns_mul_ext ns s"
using assms ns_mul_ext_refl_local[OF assms(2)] unfolding ns_mul_ext_def s_mul_ext_def
by (auto intro!: converseI mult2_alt_ns_ns_add)
context
fixes NS :: "'a rel"
assumes NS: "refl NS"
begin
lemma refl_imp_locally_refl: "locally_refl NS A" using NS unfolding refl_on_def locally_refl_def by auto
lemma supseteq_imp_ns_mul_ext:
assumes "A ⊇# B"
shows "(A, B) ∈ ns_mul_ext NS S"
using assms
by (auto intro!: ns_mul_extI[of A B "A - B" B B "{#}"] multpw_refl' refl_imp_locally_refl
simp: subset_mset.add_diff_inverse)
lemma supset_imp_s_mul_ext:
assumes "A ⊃# B"
shows "(A, B) ∈ s_mul_ext NS S"
using assms subset_mset.add_diff_inverse[of B A]
by (auto intro!: s_mul_extI[of A B "A - B" B B "{#}"] multpw_refl' refl_imp_locally_refl
simp: Diff_eq_empty_iff_mset)
end
definition mul_ext :: "('a ⇒ 'a ⇒ bool × bool) ⇒ 'a list ⇒ 'a list ⇒ bool × bool"
where "mul_ext f xs ys ≡ let s = {(x,y). fst (f x y)}; ns = {(x,y). snd (f x y)}
in ((mset xs,mset ys) ∈ s_mul_ext ns s, (mset xs, mset ys) ∈ ns_mul_ext ns s)"
definition "smulextp f m n ⟷ (m, n) ∈ s_mul_ext {(x, y). snd (f x y)} {(x, y). fst (f x y)}"
definition "nsmulextp f m n ⟷ (m, n) ∈ ns_mul_ext {(x, y). snd (f x y)} {(x, y). fst (f x y)}"
lemma smulextp_cong[fundef_cong]:
assumes "xs1 = ys1"
and "xs2 = ys2"
and "⋀ x x'. x ∈# ys1 ⟹ x' ∈# ys2 ⟹ f x x' = g x x'"
shows "smulextp f xs1 xs2 = smulextp g ys1 ys2"
unfolding smulextp_def
proof
assume "(xs1, xs2) ∈ s_mul_ext {(x, y). snd (f x y)} {(x, y). fst (f x y)}"
from s_mul_ext_local_mono[OF _ _ this, of "{(x, y). snd (g x y)}" "{(x, y). fst (g x y)}"]
show "(ys1, ys2) ∈ s_mul_ext {(x, y). snd (g x y)} {(x, y). fst (g x y)}"
using assms by force
next
assume "(ys1, ys2) ∈ s_mul_ext {(x, y). snd (g x y)} {(x, y). fst (g x y)}"
from s_mul_ext_local_mono[OF _ _ this, of "{(x, y). snd (f x y)}" "{(x, y). fst (f x y)}"]
show "(xs1, xs2) ∈ s_mul_ext {(x, y). snd (f x y)} {(x, y). fst (f x y)}"
using assms by force
qed
lemma nsmulextp_cong[fundef_cong]:
assumes "xs1 = ys1"
and "xs2 = ys2"
and "⋀ x x'. x ∈# ys1 ⟹ x' ∈# ys2 ⟹ f x x' = g x x'"
shows "nsmulextp f xs1 xs2 = nsmulextp g ys1 ys2"
unfolding nsmulextp_def
proof
assume "(xs1, xs2) ∈ ns_mul_ext {(x, y). snd (f x y)} {(x, y). fst (f x y)}"
from ns_mul_ext_local_mono[OF _ _ this, of "{(x, y). snd (g x y)}" "{(x, y). fst (g x y)}"]
show "(ys1, ys2) ∈ ns_mul_ext {(x, y). snd (g x y)} {(x, y). fst (g x y)}"
using assms by force
next
assume "(ys1, ys2) ∈ ns_mul_ext {(x, y). snd (g x y)} {(x, y). fst (g x y)}"
from ns_mul_ext_local_mono[OF _ _ this, of "{(x, y). snd (f x y)}" "{(x, y). fst (f x y)}"]
show "(xs1, xs2) ∈ ns_mul_ext {(x, y). snd (f x y)} {(x, y). fst (f x y)}"
using assms by force
qed
definition "mulextp f m n = (smulextp f m n, nsmulextp f m n)"
lemma mulextp_cong[fundef_cong]:
assumes "xs1 = ys1"
and "xs2 = ys2"
and "⋀ x x'. x ∈# ys1 ⟹ x' ∈# ys2 ⟹ f x x' = g x x'"
shows "mulextp f xs1 xs2 = mulextp g ys1 ys2"
unfolding mulextp_def using assms by (auto cong: nsmulextp_cong smulextp_cong)
lemma mset_s_mul_ext:
"(mset xs, mset ys) ∈ s_mul_ext {(x, y). snd (f x y)} {(x, y).fst (f x y)} ⟷
fst (mul_ext f xs ys)"
by (auto simp: mul_ext_def Let_def)
lemma mset_ns_mul_ext:
"(mset xs, mset ys) ∈ ns_mul_ext {(x, y). snd (f x y)} {(x, y).fst (f x y)} ⟷
snd (mul_ext f xs ys)"
by (auto simp: mul_ext_def Let_def)
lemma smulextp_mset_code:
"smulextp f (mset xs) (mset ys) ⟷ fst (mul_ext f xs ys)"
unfolding smulextp_def mset_s_mul_ext ..
lemma nsmulextp_mset_code:
"nsmulextp f (mset xs) (mset ys) ⟷ snd (mul_ext f xs ys)"
unfolding nsmulextp_def mset_ns_mul_ext ..
lemma nstri_mul_ext_map:
assumes "⋀s t. s ∈ set ss ⟹ t ∈ set ts ⟹ fst (order s t) ⟹ fst (order' (f s) (f t))"
and "⋀s t. s ∈ set ss ⟹ t ∈ set ts ⟹ snd (order s t) ⟹ snd (order' (f s) (f t))"
and "snd (mul_ext order ss ts)"
shows "snd (mul_ext order' (map f ss) (map f ts))"
using assms mult2_alt_map[of "mset ts" "mset ss" "{(t, s). snd (order s t)}" f f
"{(t, s). snd (order' s t)}" "{(t, s). fst (order s t)}" "{(t, s). fst (order' s t)}" True]
by (auto simp: mul_ext_def ns_mul_ext_def converse_unfold)
lemma stri_mul_ext_map:
assumes "⋀s t. s ∈ set ss ⟹ t ∈ set ts ⟹ fst (order s t) ⟹ fst (order' (f s) (f t))"
and "⋀s t. s ∈ set ss ⟹ t ∈ set ts ⟹ snd (order s t) ⟹ snd (order' (f s) (f t))"
and "fst (mul_ext order ss ts)"
shows "fst (mul_ext order' (map f ss) (map f ts))"
using assms mult2_alt_map[of "mset ts" "mset ss" "{(t,s). snd (order s t)}" f f
"{(t, s). snd (order' s t)}" "{(t, s). fst (order s t)}" "{(t, s). fst (order' s t)}" False]
by (auto simp: mul_ext_def s_mul_ext_def converse_unfold)
lemma mul_ext_arg_empty: "snd (mul_ext f [] xs) ⟹ xs = []"
unfolding mul_ext_def Let_def by (auto simp: ns_mul_ext_def mult2_alt_def)
text ‹The non-strict order is irreflexive›
lemma s_mul_ext_irrefl: assumes irr: "irrefl_on (set_mset A) S"
and S_NS: "S ⊆ NS"
and compat: "S O NS ⊆ S"
shows "(A,A) ∉ s_mul_ext NS S" using irr
proof (induct A rule: wf_induct[OF wf_measure[of size]])
case (1 A)
show ?case
proof
assume "(A,A) ∈ s_mul_ext NS S"
from s_mul_extE[OF this]
obtain A1 A2 B1 B2 where
A: "A = A1 + A2"
and B: "A = B1 + B2"
and AB1: "(A1, B1) ∈ multpw NS"
and ne: "A2 ≠ {#}"
and S: "⋀b. b ∈# B2 ⟹ ∃a. a ∈# A2 ∧ (a, b) ∈ S"
by blast
from multpw_listE[OF AB1] obtain as1 bs1 where
l1: "length as1 = length bs1"
and A1: "A1 = mset as1"
and B1: "B1 = mset bs1"
and NS: "⋀ i. i<length bs1 ⟹ (as1 ! i, bs1 ! i) ∈ NS" by blast
note NSS = NS
note SS = S
obtain as2 where A2: "A2 = mset as2" by (metis ex_mset)
obtain bs2 where B2: "B2 = mset bs2" by (metis ex_mset)
define as where "as = as1 @ as2"
define bs where "bs = bs1 @ bs2"
have as: "A = mset as" unfolding A A1 A2 as_def by simp
have bs: "A = mset bs" unfolding B B1 B2 bs_def by simp
from as bs have abs: "mset as = mset bs" by simp
hence set_ab: "set as = set bs" by (rule mset_eq_setD)
let ?n = "length bs"
have las: "length as = ?n"
using mset_eq_length abs by fastforce
let ?m = "length bs1"
define decr where "decr j i ≡
(as ! j, bs ! i) ∈ NS ∧ (i < ?m ⟶ j = i) ∧ (?m ≤ i ⟶ ?m ≤ j ∧ (as ! j, bs ! i) ∈ S)" for i j
define step where "step i j k =
(i < ?n ∧ j < ?n ∧ k < ?n ∧ bs ! k = as ! j ∧ decr j i)"
for i j k
{
fix i
assume i: "i < ?n"
let ?b = "bs ! i"
have "∃ j. j < ?n ∧ decr j i"
proof (cases "i < ?m")
case False
with i have "?b ∈ set bs2" unfolding bs_def
by (auto simp: nth_append)
hence "?b ∈# B2" unfolding B2 by auto
from S[OF this, unfolded A2] obtain a where a: "a ∈ set as2" and S: "(a, ?b) ∈ S"
by auto
from a obtain k where a: "a = as2 ! k" and k: "k < length as2" unfolding set_conv_nth by auto
have "a = as ! (?m + k)" unfolding a as_def l1[symmetric] by simp
from S[unfolded this] S_NS False k
show ?thesis unfolding decr_def
by (intro exI[of _ "?m + k"], auto simp: las[symmetric] l1[symmetric] as_def)
next
case True
from NS[OF this] i True show ?thesis unfolding decr_def
by (auto simp: as_def bs_def l1 nth_append)
qed (insert i NS)
from this[unfolded set_conv_nth] las
obtain j where j: "j < ?n" and decr: "decr j i" by auto
let ?a = "as ! j"
from j las have "?a ∈ set as" by auto
from this[unfolded set_ab, unfolded set_conv_nth] obtain k where
k: "k < ?n" and id: "?a = bs ! k" by auto
have "∃ j k. step i j k"
using j k decr id i unfolding step_def by metis
}
hence "∀ i. ∃ j k. i < ?n ⟶ step i j k" by blast
from choice[OF this] obtain J' where "∀ i. ∃ k. i < ?n ⟶ step i (J' i) k" by blast
from choice[OF this] obtain K' where
step: "⋀ i. i < ?n ⟹ step i (J' i) (K' i)" by blast
define I where "I i = (K'^^i) 0" for i
define J where "J i = J' (I i)" for i
define K where "K i = K' (I i)" for i
from ne have "A ≠ {#}" unfolding A by auto
hence "set as ≠ {}" unfolding as by auto
hence "length as ≠ 0" by simp
hence n0: "0 < ?n" using las by auto
{
fix n
have "step (I n) (J n) (K n)"
proof (induct n)
case 0
from step[OF n0] show ?case unfolding I_def J_def K_def by auto
next
case (Suc n)
from Suc have "K n < ?n" unfolding step_def by auto
from step[OF this] show ?case unfolding J_def K_def I_def by auto
qed
}
note step = this
have "I n ∈ {..<?n}" for n using step[of n] unfolding step_def by auto
hence "I ` UNIV ⊆ {..<?n}" by auto
from finite_subset[OF this] have "finite (I ` UNIV)" by simp
from pigeonhole_infinite[OF _ this] obtain m where
"infinite {i. I i = I m}" by auto
hence "∃ m'. m' > m ∧ I m' = I m"
by (simp add: infinite_nat_iff_unbounded)
then obtain m' where *: "m < m'" "I m' = I m" by auto
let ?P = "λ n. ∃ m. n ≠ 0 ∧ I (n + m) = I m"
define n where "n = (LEAST n. ?P n)"
have "∃ n. ?P n"
by (rule exI[of _ "m' - m"], rule exI[of _ m], insert *, auto)
from LeastI_ex[of ?P, OF this, folded n_def]
obtain m where n: "n ≠ 0" and Im: "I (n + m) = I m" by auto
let ?M = "{m..<m+n}"
{
fix i j
assume *: "m ≤ i" "i < j" "j < n + m"
define k where "k = j - i"
have k0: "k ≠ 0" and j: "j = k + i" and kn: "k < n" using * unfolding k_def by auto
from not_less_Least[of _ ?P, folded n_def, OF kn] k0
have "I i ≠ I j" unfolding j by metis
}
hence inj: "inj_on I ?M" unfolding inj_on_def
by (metis add.commute atLeastLessThan_iff linorder_neqE_nat)
define b where "b i = bs ! I i" for i
have bnm: "b (n + m) = b m" unfolding b_def Im ..
{
fix i
from step[of i, unfolded step_def]
have id: "bs ! K i = as ! J i" and decr: "decr (J i) (I i)" by auto
from id decr[unfolded decr_def] have "(bs ! K i, bs ! I i) ∈ NS" by auto
also have "K i = I (Suc i)" unfolding I_def K_def by auto
finally have "(b (Suc i), b i) ∈ NS" unfolding b_def by auto
} note NS = this
{
fix i j :: nat
assume "i ≤ j"
then obtain k where j: "j = i + k" by (rule less_eqE)
have "(b j, b i) ∈ NS^*" unfolding j
proof (induct k)
case (Suc k)
thus ?case using NS[of "i + k"] by auto
qed auto
} note NSstar = this
{
assume "∃ i ∈ ?M. I i ≥ ?m"
then obtain k where k: "k ∈ ?M" and I: "I k ≥ ?m" by auto
from step[of k, unfolded step_def]
have id: "bs ! K k = as ! J k" and decr: "decr (J k) (I k)" by auto
from id decr[unfolded decr_def] I have "(bs ! K k, bs ! I k) ∈ S" by auto
also have "K k = I (Suc k)" unfolding I_def K_def by auto
finally have S: "(b (Suc k), b k) ∈ S" unfolding b_def by auto
from k have "m ≤ k" by auto
from NSstar[OF this] have NS1: "(b k, b m) ∈ NS^*" .
from k have "Suc k ≤ n + m" by auto
from NSstar[OF this, unfolded bnm] have NS2: "(b m, b (Suc k)) ∈ NS^*" .
from NS1 NS2 have "(b k, b (Suc k)) ∈ NS^*" by simp
with S have "(b (Suc k), b (Suc k)) ∈ S O NS^*" by auto
also have "… ⊆ S" using compat
by (metis compat_tr_compat converse_inward(1) converse_mono converse_relcomp)
finally have contradiction: "b (Suc k) ∉ set_mset A" using 1 unfolding irrefl_on_def by auto
have "b (Suc k) ∈ set bs" unfolding b_def using step[of "Suc k"] unfolding step_def
by auto
also have "set bs = set_mset A" unfolding bs by auto
finally have False using contradiction by auto
}
hence only_NS: "i ∈ ?M ⟹ I i < ?m" for i by force
{
fix i
assume i: "i ∈ ?M"
from step[of i, unfolded step_def] have *: "I i < ?n" "K i < ?n"
and id: "bs ! K i = as ! J i" and decr: "decr (J i) (I i)" by auto
from decr[unfolded decr_def] only_NS[OF i] have "J i = I i" by auto
with id have id: "bs ! K i = as ! I i" by auto
note only_NS[OF i] id
} note pre_result = this
{
fix i
assume i: "i ∈ ?M"
have *: "I i < ?m" "K i < ?m"
proof (rule pre_result[OF i])
have "∃ j ∈ ?M. K i = I j"
proof (cases "Suc i ∈ ?M")
case True
show ?thesis by (rule bexI[OF _ True], auto simp: K_def I_def)
next
case False
with i have id: "n + m = Suc i" by auto
hence id: "K i = I m" by (subst Im[symmetric], unfold id, auto simp: K_def I_def)
with i show ?thesis by (intro bexI[of _ m], auto simp: K_def I_def)
qed
with pre_result show "K i < ?m" by auto
qed
from pre_result(2)[OF i] * l1 have "bs1 ! K i = as1 ! I i" "K i = I (Suc i)"
unfolding as_def bs_def by (auto simp: nth_append K_def I_def)
with * have "bs1 ! I (Suc i) = as1 ! I i" "I i < ?m" "I (Suc i) < ?m"
by auto
} note pre_identities = this
define M where "M = ?M"
note inj = inj[folded M_def]
define nxt where "nxt i = (if Suc i = n + m then m else Suc i)" for i
define prv where "prv i = (if i = m then n + m - 1 else i - 1)" for i
{
fix i
assume "i ∈ M"
hence i: "i ∈ ?M" unfolding M_def by auto
from i n have inM: "nxt i ∈ M" "prv i ∈ M" "nxt (prv i) = i" "prv (nxt i) = i"
unfolding nxt_def prv_def by (auto simp: M_def)
from i pre_identities[OF i] pre_identities[of m] Im n
have nxt: "bs1 ! I (nxt i) = as1 ! I i"
unfolding nxt_def prv_def by (auto simp: M_def)
note nxt inM
} note identities = this
note identities = identities[folded M_def]
define Drop where "Drop = I ` M"
define rem_idx where "rem_idx = filter (λ i. i ∉ Drop) [0..<?m]"
define drop_idx where "drop_idx = filter (λ i. i ∈ Drop) [0..<?m]"
define as1' where "as1' = map ((!) as1) rem_idx"
define bs1' where "bs1' = map ((!) bs1) rem_idx"
define as1'' where "as1'' = map ((!) as1) drop_idx"
define bs1'' where "bs1'' = map ((!) bs1) drop_idx"
{
fix as1 :: "'a list" and D :: "nat set"
define I where "I = [0..< length as1]"
have "mset as1 = mset (map ((!) as1) I)" unfolding I_def
by (rule arg_cong[of _ _ mset], intro nth_equalityI, auto)
also have "… = mset (map ((!) as1) (filter (λ i. i ∈ D) I))
+ mset (map ((!) as1) (filter (λ i. i ∉ D) I))"
by (induct I, auto)
also have "I = [0..< length as1]" by fact
finally have "mset as1 = mset (map ((!) as1) (filter (λi. i ∈ D) [0..<length as1])) + mset (map ((!) as1) (filter (λi. i ∉ D) [0..<length as1]))" .
} note split = this
from split[of bs1 Drop, folded rem_idx_def drop_idx_def, folded bs1'_def bs1''_def]
have bs1: "mset bs1 = mset bs1'' + mset bs1'" .
from split[of as1 Drop, unfolded l1, folded rem_idx_def drop_idx_def, folded as1'_def as1''_def]
have as1: "mset as1 = mset as1'' + mset as1'" .
define I' where "I' = the_inv_into M I"
have bij: "bij_betw I M Drop" using inj unfolding Drop_def by (rule inj_on_imp_bij_betw)
from the_inv_into_f_f[OF inj, folded I'_def] have I'I: "i ∈ M ⟹ I' (I i) = i" for i by auto
from bij I'I have II': "i ∈ Drop ⟹ I (I' i) = i" for i
by (simp add: I'_def f_the_inv_into_f_bij_betw)
from II' I'I identities bij have Drop_M: "i ∈ Drop ⟹ I' i ∈ M" for i
using Drop_def by force
have M_Drop: "i ∈ M ⟹ I i ∈ Drop" for i unfolding Drop_def by auto
{
fix x
assume "x ∈ Drop"
then obtain i where i: "i ∈ M" and x: "x = I i" unfolding Drop_def by auto
have "x < ?m" unfolding x using i pre_identities[of i] unfolding M_def by auto
} note Drop_m = this
hence drop_idx: "set drop_idx = Drop" unfolding M_def drop_idx_def set_filter set_upt by auto
have "mset as1'' = mset (map ((!) as1) drop_idx)" unfolding as1''_def mset_map by auto
also have "drop_idx = map (I o I') drop_idx" using drop_idx by (intro nth_equalityI, auto intro!: II'[symmetric])
also have "map ((!) as1) … = map (λ i. as1 ! I i) (map I' drop_idx)" by auto
also have "… = map (λ i. bs1 ! I (nxt i)) (map I' drop_idx)"
by (rule map_cong[OF refl], rule identities(1)[symmetric], insert drop_idx Drop_M, auto)
also have "… = map ((!) bs1) (map (I o nxt o I') drop_idx)"
by auto
also have "mset … = image_mset ((!) bs1) (image_mset (I o nxt o I') (mset drop_idx))" unfolding mset_map ..
also have "image_mset (I o nxt o I') (mset drop_idx) = image_mset I (image_mset nxt (image_mset I' (mset drop_idx)))"
by (metis multiset.map_comp)
also have "image_mset nxt (image_mset I' (mset drop_idx)) = image_mset I' (mset drop_idx)"
proof -
have dist: "distinct drop_idx" unfolding drop_idx_def by auto
have injI': "inj_on I' Drop" using II' by (rule inj_on_inverseI)
have "mset drop_idx = mset_set Drop" unfolding drop_idx[symmetric]
by (rule mset_set_set[symmetric, OF dist])
from image_mset_mset_set[OF injI', folded this]
have "image_mset I' (mset drop_idx) = mset_set (I' ` Drop)" by auto
also have "I' ` Drop = M" using II' I'I M_Drop Drop_M by force
finally have id: "image_mset I' (mset drop_idx) = mset_set M" .
have inj_nxt: "inj_on nxt M" using identities by (intro inj_on_inverseI)
have nxt: "nxt ` M = M" using identities by force
show ?thesis unfolding id image_mset_mset_set[OF inj_nxt] nxt ..
qed
also have "image_mset I … = mset drop_idx" unfolding multiset.map_comp using II'
by (intro multiset.map_ident_strong, auto simp: drop_idx)
also have "image_mset ((!) bs1) … = mset bs1''" unfolding bs1''_def mset_map ..
finally have bs1'': "mset bs1'' = mset as1''" ..
let ?A = "mset as1' + mset as2"
let ?B = "mset bs1' + mset bs2"
from as1 bs1'' have as1: "mset as1 = mset bs1'' + mset as1'" by auto
have A: "A = mset bs1'' + ?A" unfolding A A1 A2 as1 by auto
have B: "A = mset bs1'' + ?B" unfolding B B1 B2 bs1 by auto
from A[unfolded B] have AB: "?A = ?B" by simp
have l1': "length as1' = length bs1'" unfolding as1'_def bs1'_def by auto
have NS: "(mset as1', mset bs1') ∈ multpw NS"
proof (rule multpw_listI[OF l1' refl refl], intro allI impI)
fix i
assume i: "i < length bs1'"
hence "rem_idx ! i ∈ set rem_idx" unfolding bs1'_def by (auto simp: nth_append)
hence ri: "rem_idx ! i < ?m" unfolding rem_idx_def by auto
from NSS[OF this] i
show "(as1' ! i, bs1' ! i) ∈ NS" unfolding as1'_def bs1'_def by (auto simp: nth_append)
qed
have S: "(mset as1' + mset as2, ?B) ∈ s_mul_ext NS S"
by (intro s_mul_extI[OF refl refl NS], unfold A2[symmetric] B2[symmetric], rule ne, rule S)
have irr: "irrefl_on (set_mset ?B) S" using 1(2) B unfolding irrefl_on_def by simp
have "M ≠ {}" unfolding M_def using n by auto
hence "Drop ≠ {}" unfolding Drop_def by auto
with drop_idx have "drop_idx ≠ []" by auto
hence "bs1'' ≠ []" unfolding bs1''_def by auto
hence "?B ⊂# A" unfolding B by (simp add: subset_mset.less_le)
hence "size ?B < size A" by (rule mset_subset_size)
thus False using 1(1) AB S irr by auto
qed
qed
lemma mul_ext_irrefl: assumes "⋀ x. x ∈ set xs ⟹ ¬ fst (rel x x)"
and "⋀ x y z. fst (rel x y) ⟹ snd (rel y z) ⟹ fst (rel x z)"
and "⋀ x y. fst (rel x y) ⟹ snd (rel x y)"
shows "¬ fst (mul_ext rel xs xs)"
unfolding mul_ext_def Let_def fst_conv
by (rule s_mul_ext_irrefl, insert assms, auto simp: irrefl_on_def)
text ‹The non-strict order is transitive.›
lemma ns_mul_ext_trans:
assumes "trans s" "trans ns" "compatible_l ns s" "compatible_r ns s" "refl ns"
and "(A, B) ∈ ns_mul_ext ns s"
and "(B, C) ∈ ns_mul_ext ns s"
shows "(A, C) ∈ ns_mul_ext ns s"
using assms unfolding compatible_l_def compatible_r_def ns_mul_ext_def
using trans_mult2_ns[of "s¯" "ns¯"]
by (auto simp: mult2_ns_eq_mult2_ns_alt converse_relcomp[symmetric]) (metis trans_def)
text‹The strict order is trans.›
lemma s_mul_ext_trans:
assumes "trans s" "trans ns" "compatible_l ns s" "compatible_r ns s" "refl ns"
and "(A, B) ∈ s_mul_ext ns s"
and "(B, C) ∈ s_mul_ext ns s"
shows "(A, C) ∈ s_mul_ext ns s"
using assms unfolding compatible_l_def compatible_r_def s_mul_ext_def
using trans_mult2_s[of "s¯" "ns¯"]
by (auto simp: mult2_s_eq_mult2_s_alt converse_relcomp[symmetric]) (metis trans_def)
text‹The strict order is compatible on the left with the non strict one›
lemma s_ns_mul_ext_trans:
assumes "trans s" "trans ns" "compatible_l ns s" "compatible_r ns s" "refl ns"
and "(A, B) ∈ s_mul_ext ns s"
and "(B, C) ∈ ns_mul_ext ns s"
shows "(A, C) ∈ s_mul_ext ns s"
using assms unfolding compatible_l_def compatible_r_def s_mul_ext_def ns_mul_ext_def
using compat_mult2(1)[of "s¯" "ns¯"]
by (auto simp: mult2_s_eq_mult2_s_alt mult2_ns_eq_mult2_ns_alt converse_relcomp[symmetric])
text‹The strict order is compatible on the right with the non-strict one.›
lemma ns_s_mul_ext_trans:
assumes "trans s" "trans ns" "compatible_l ns s" "compatible_r ns s" "refl ns"
and "(A, B) ∈ ns_mul_ext ns s"
and "(B, C) ∈ s_mul_ext ns s"
shows "(A, C) ∈ s_mul_ext ns s"
using assms unfolding compatible_l_def compatible_r_def s_mul_ext_def ns_mul_ext_def
using compat_mult2(2)[of "s¯" "ns¯"]
by (auto simp: mult2_s_eq_mult2_s_alt mult2_ns_eq_mult2_ns_alt converse_relcomp[symmetric])
text‹@{const s_mul_ext} is strongly normalizing›
lemma SN_s_mul_ext_strong:
assumes "order_pair s ns"
and "∀y. y ∈# M ⟶ SN_on s {y}"
shows "SN_on (s_mul_ext ns s) {M}"
using mult2_s_eq_mult2_s_alt[of "ns¯" "s¯"] assms wf_below_pointwise[of "s¯" "set_mset M"]
unfolding SN_on_iff_wf_below s_mul_ext_def order_pair_def compat_pair_def pre_order_pair_def
by (auto intro!: wf_below_mult2_s_local simp: converse_relcomp[symmetric])
lemma SN_s_mul_ext:
assumes "order_pair s ns" "SN s"
shows "SN (s_mul_ext ns s)"
using SN_s_mul_ext_strong[OF assms(1)] assms(2)
by (auto simp: SN_on_def)
lemma (in order_pair) mul_ext_order_pair:
"order_pair (s_mul_ext NS S) (ns_mul_ext NS S)" (is "order_pair ?S ?NS")
proof
from s_mul_ext_trans trans_S trans_NS compat_NS_S compat_S_NS refl_NS
show "trans ?S" unfolding trans_def compatible_l_def compatible_r_def by blast
next
from ns_mul_ext_trans trans_S trans_NS compat_NS_S compat_S_NS refl_NS
show "trans ?NS" unfolding trans_def compatible_l_def compatible_r_def by blast
next
from ns_s_mul_ext_trans trans_S trans_NS compat_NS_S compat_S_NS refl_NS
show "?NS O ?S ⊆ ?S" unfolding trans_def compatible_l_def compatible_r_def by blast
next
from s_ns_mul_ext_trans trans_S trans_NS compat_NS_S compat_S_NS refl_NS
show "?S O ?NS ⊆ ?S" unfolding trans_def compatible_l_def compatible_r_def by blast
next
from ns_mul_ext_refl[OF refl_NS, of _ S]
show "refl ?NS" unfolding refl_on_def by fast
qed
lemma (in SN_order_pair) mul_ext_SN_order_pair: "SN_order_pair (s_mul_ext NS S) (ns_mul_ext NS S)"
(is "SN_order_pair ?S ?NS")
proof -
from mul_ext_order_pair
interpret order_pair ?S ?NS .
have "order_pair S NS" by unfold_locales
then interpret SN_ars ?S using SN_s_mul_ext[of S NS] SN by unfold_locales
show ?thesis by unfold_locales
qed
lemma mul_ext_compat:
assumes compat: "⋀ s t u. ⟦s ∈ set ss; t ∈ set ts; u ∈ set us⟧ ⟹
(snd (f s t) ∧ fst (f t u) ⟶ fst (f s u)) ∧
(fst (f s t) ∧ snd (f t u) ⟶ fst (f s u)) ∧
(snd (f s t) ∧ snd (f t u) ⟶ snd (f s u)) ∧
(fst (f s t) ∧ fst (f t u) ⟶ fst (f s u))"
shows "
(snd (mul_ext f ss ts) ∧ fst (mul_ext f ts us) ⟶ fst (mul_ext f ss us)) ∧
(fst (mul_ext f ss ts) ∧ snd (mul_ext f ts us) ⟶ fst (mul_ext f ss us)) ∧
(snd (mul_ext f ss ts) ∧ snd (mul_ext f ts us) ⟶ snd (mul_ext f ss us)) ∧
(fst (mul_ext f ss ts) ∧ fst (mul_ext f ts us) ⟶ fst (mul_ext f ss us)) "
proof -
let ?s = "{(x, y). fst (f x y)}¯" and ?ns = "{(x, y). snd (f x y)}¯"
have [dest]: "(mset ts, mset ss) ∈ mult2_alt b2 ?ns ?s ⟹ (mset us, mset ts) ∈ mult2_alt b1 ?ns ?s ⟹
(mset us, mset ss) ∈ mult2_alt (b1 ∧ b2) ?ns ?s" for b1 b2
using assms by (auto intro!: trans_mult2_alt_local[of _ "mset ts"] simp: in_multiset_in_set)
show ?thesis by (auto simp: mul_ext_def s_mul_ext_def ns_mul_ext_def Let_def)
qed
lemma mul_ext_cong[fundef_cong]:
assumes "mset xs1 = mset ys1"
and "mset xs2 = mset ys2"
and "⋀ x x'. x ∈ set ys1 ⟹ x' ∈ set ys2 ⟹ f x x' = g x x'"
shows "mul_ext f xs1 xs2 = mul_ext g ys1 ys2"
using assms
mult2_alt_map[of "mset xs2" "mset xs1" "{(x, y). snd (f x y)}¯" id id "{(x, y). snd (g x y)}¯"
"{(x, y). fst (f x y)}¯" "{(x, y). fst (g x y)}¯"]
mult2_alt_map[of "mset ys2" "mset ys1" "{(x, y). snd (g x y)}¯" id id "{(x, y). snd (f x y)}¯"
"{(x, y). fst (g x y)}¯" "{(x, y). fst (f x y)}¯"]
by (auto simp: mul_ext_def s_mul_ext_def ns_mul_ext_def Let_def in_multiset_in_set)
lemma all_nstri_imp_mul_nstri:
assumes "∀i<length ys. snd (f (xs ! i) (ys ! i))"
and "length xs = length ys"
shows "snd (mul_ext f xs ys)"
proof-
from assms(1) have "∀i. i < length ys ⟶ (xs ! i, ys ! i) ∈ {(x,y). snd (f x y)}" by simp
from all_ns_ns_mul_ext[OF assms(2) this] show ?thesis by (simp add: mul_ext_def)
qed
lemma relation_inter:
shows "{(x,y). P x y} ∩ {(x,y). Q x y} = {(x,y). P x y ∧ Q x y}"
by blast
lemma mul_ext_unfold:
"(x,y) ∈ {(a,b). fst (mul_ext g a b)} ⟷ (mset x, mset y) ∈ (s_mul_ext {(a,b). snd (g a b)} {(a,b). fst (g a b)})"
unfolding mul_ext_def by (simp add: Let_def)
text ‹The next lemma is a local version of strong-normalization of
the multiset extension, where the base-order only has to be strongly normalizing
on elements of the multisets. This will be crucial for orders that are defined recursively
on terms, such as RPO or WPO.›
lemma mul_ext_SN:
assumes "∀x. snd (g x x)"
and "∀x y z. fst (g x y) ⟶ snd (g y z) ⟶ fst (g x z)"
and "∀x y z. snd (g x y) ⟶ fst (g y z) ⟶ fst (g x z)"
and "∀x y z. snd (g x y) ⟶ snd (g y z) ⟶ snd (g x z)"
and "∀x y z. fst (g x y) ⟶ fst (g y z) ⟶ fst (g x z)"
shows "SN {(ys, xs).
(∀y∈set ys. SN_on {(s ,t). fst (g s t)} {y}) ∧
fst (mul_ext g ys xs)}"
proof -
let ?R1 = "λxs ys. ∀y∈ set ys. SN_on {(s ,t). fst (g s t)} {y}"
let ?R2 = "λxs ys. fst (mul_ext g ys xs)"
let ?s = "{(x,y). fst (g x y)}" and ?ns = "{(x,y). snd (g x y)}"
have OP: "order_pair ?s ?ns" using assms(1-5)
by unfold_locales ((unfold refl_on_def trans_def)?, blast)+
let ?R = "{(ys, xs). ?R1 xs ys ∧ ?R2 xs ys}"
let ?Sn = "SN_on ?R"
{
fix ys xs
assume R_ys_xs: "(ys, xs) ∈ ?R"
let ?mys = "mset ys"
let ?mxs = "mset xs"
from R_ys_xs have HSN_ys: "∀y. y ∈ set ys ⟶ SN_on ?s {y}" by simp
with in_multiset_in_set[of ys] have "∀y. y ∈# ?mys ⟶ SN_on ?s {y}" by simp
from SN_s_mul_ext_strong[OF OP this] and mul_ext_unfold
have "SN_on {(ys,xs). fst (mul_ext g ys xs)} {ys}" by fast
from relation_inter[of ?R2 ?R1] and SN_on_weakening[OF this]
have "SN_on ?R {ys}" by blast
}
then have Hyp: "∀ys xs. (ys,xs) ∈ ?R ⟶ SN_on ?R {ys}" by auto
{
fix ys
have "SN_on ?R {ys}"
proof (cases "∃ xs. (ys, xs) ∈ ?R")
case True with Hyp show ?thesis by simp
next
case False then show ?thesis by auto
qed
}
then show ?thesis unfolding SN_on_def by simp
qed
lemma mul_ext_stri_imp_nstri:
assumes "fst (mul_ext f as bs)"
shows "snd (mul_ext f as bs)"
using assms and s_ns_mul_ext unfolding mul_ext_def by (auto simp: Let_def)
lemma ns_ns_mul_ext_union_compat:
assumes "(A,B) ∈ ns_mul_ext ns s"
and "(C,D) ∈ ns_mul_ext ns s"
shows "(A + C, B + D) ∈ ns_mul_ext ns s"
using assms by (auto simp: ns_mul_ext_def intro: mult2_alt_ns_ns_add)
lemma s_ns_mul_ext_union_compat:
assumes "(A,B) ∈ s_mul_ext ns s"
and "(C,D) ∈ ns_mul_ext ns s"
shows "(A + C, B + D) ∈ s_mul_ext ns s"
using assms by (auto simp: s_mul_ext_def ns_mul_ext_def intro: mult2_alt_s_ns_add)
lemma ns_ns_mul_ext_union_compat_rtrancl: assumes refl: "refl ns"
and AB: "(A, B) ∈ (ns_mul_ext ns s)⇧*"
and CD: "(C, D) ∈ (ns_mul_ext ns s)⇧*"
shows "(A + C, B + D) ∈ (ns_mul_ext ns s)⇧*"
proof -
{
fix A B C
assume "(A, B) ∈ (ns_mul_ext ns s)⇧*"
then have "(A + C, B + C) ∈ (ns_mul_ext ns s)⇧*"
proof (induct rule: rtrancl_induct)
case (step B D)
have "(C, C) ∈ ns_mul_ext ns s"
by (rule ns_mul_ext_refl, insert refl, auto simp: locally_refl_def refl_on_def)
from ns_ns_mul_ext_union_compat[OF step(2) this] step(3)
show ?case by auto
qed auto
}
from this[OF AB, of C] this[OF CD, of B]
show ?thesis by (auto simp: ac_simps)
qed
subsection ‹Multisets as order on lists›
interpretation mul_ext_list: list_order_extension
"λs ns. {(as, bs). (mset as, mset bs) ∈ s_mul_ext ns s}"
"λs ns. {(as, bs). (mset as, mset bs) ∈ ns_mul_ext ns s}"
proof -
let ?m = "mset :: ('a list ⇒ 'a multiset)"
let ?S = "λs ns. {(as, bs). (?m as, ?m bs) ∈ s_mul_ext ns s}"
let ?NS = "λs ns. {(as, bs). (?m as, ?m bs) ∈ ns_mul_ext ns s}"
show "list_order_extension ?S ?NS"
proof (rule list_order_extension.intro)
fix s ns
let ?s = "?S s ns"
let ?ns = "?NS s ns"
assume "SN_order_pair s ns"
then interpret SN_order_pair s ns .
interpret SN_order_pair "(s_mul_ext ns s)" "(ns_mul_ext ns s)"
by (rule mul_ext_SN_order_pair)
show "SN_order_pair ?s ?ns"
proof
show "refl ?ns" using refl_NS unfolding refl_on_def by blast
show "?ns O ?s ⊆ ?s" using compat_NS_S by blast
show "?s O ?ns ⊆ ?s" using compat_S_NS by blast
show "trans ?ns" using trans_NS unfolding trans_def by blast
show "trans ?s" using trans_S unfolding trans_def by blast
show "SN ?s" using SN_inv_image[OF SN, of ?m, unfolded inv_image_def] .
qed
next
fix S f NS as bs
assume "⋀a b. (a, b) ∈ S ⟹ (f a, f b) ∈ S"
"⋀a b. (a, b) ∈ NS ⟹ (f a, f b) ∈ NS"
"(as, bs) ∈ ?S S NS"
then show "(map f as, map f bs) ∈ ?S S NS"
using mult2_alt_map[of _ _ "NS¯" f f "NS¯" "S¯" "S¯"] by (auto simp: mset_map s_mul_ext_def)
next
fix S f NS as bs
assume "⋀a b. (a, b) ∈ S ⟹ (f a, f b) ∈ S"
"⋀a b. (a, b) ∈ NS ⟹ (f a, f b) ∈ NS"
"(as, bs) ∈ ?NS S NS"
then show "(map f as, map f bs) ∈ ?NS S NS"
using mult2_alt_map[of _ _ "NS¯" f f "NS¯" "S¯" "S¯"] by (auto simp: mset_map ns_mul_ext_def)
next
fix as bs :: "'a list" and NS S :: "'a rel"
assume ass: "length as = length bs"
"⋀i. i < length bs ⟹ (as ! i, bs ! i) ∈ NS"
show "(as, bs) ∈ ?NS S NS"
by (rule, unfold split, rule all_ns_ns_mul_ext, insert ass, auto)
qed
qed
lemma s_mul_ext_singleton [simp, intro]:
assumes "(a, b) ∈ s"
shows "({#a#}, {#b#}) ∈ s_mul_ext ns s"
using assms by (auto simp: s_mul_ext_def mult2_alt_s_single)
lemma ns_mul_ext_singleton [simp, intro]:
"(a, b) ∈ ns ⟹ ({#a#}, {#b#}) ∈ ns_mul_ext ns s"
by (auto simp: ns_mul_ext_def multpw_converse intro: multpw_implies_mult2_alt_ns multpw_single)
lemma ns_mul_ext_singleton2:
"(a, b) ∈ s ⟹ ({#a#}, {#b#}) ∈ ns_mul_ext ns s"
by (intro s_ns_mul_ext s_mul_ext_singleton)
lemma s_mul_ext_self_extend_left:
assumes "A ≠ {#}" and "locally_refl W B"
shows "(A + B, B) ∈ s_mul_ext W S"
proof -
have "(A + B, {#} + B) ∈ s_mul_ext W S"
using assms by (intro s_mul_ext_union_compat) (auto dest: s_mul_ext_bottom)
then show ?thesis by simp
qed
lemma s_mul_ext_ne_extend_left:
assumes "A ≠ {#}" and "(B, C) ∈ ns_mul_ext W S"
shows "(A + B, C) ∈ s_mul_ext W S"
using assms
proof -
have "(A + B, {#} + C) ∈ s_mul_ext W S"
using assms by (intro s_ns_mul_ext_union_compat)
(auto simp: s_mul_ext_bottom dest: s_ns_mul_ext)
then show ?thesis by (simp add: ac_simps)
qed
lemma s_mul_ext_extend_left:
assumes "(B, C) ∈ s_mul_ext W S"
shows "(A + B, C) ∈ s_mul_ext W S"
using assms
proof -
have "(B + A, C + {#}) ∈ s_mul_ext W S"
using assms by (intro s_ns_mul_ext_union_compat)
(auto simp: ns_mul_ext_bottom dest: s_ns_mul_ext)
then show ?thesis by (simp add: ac_simps)
qed
lemma mul_ext_mono:
assumes "⋀x y. ⟦x ∈ set xs; y ∈ set ys; fst (P x y)⟧ ⟹ fst (P' x y)"
and "⋀x y. ⟦x ∈ set xs; y ∈ set ys; snd (P x y)⟧ ⟹ snd (P' x y)"
shows
"fst (mul_ext P xs ys) ⟹ fst (mul_ext P' xs ys)"
"snd (mul_ext P xs ys) ⟹ snd (mul_ext P' xs ys)"
unfolding mul_ext_def Let_def fst_conv snd_conv
proof -
assume mem: "(mset xs, mset ys) ∈ s_mul_ext {(x, y). snd (P x y)} {(x, y). fst (P x y)}"
show "(mset xs, mset ys) ∈ s_mul_ext {(x, y). snd (P' x y)} {(x, y). fst (P' x y)}"
by (rule s_mul_ext_local_mono[OF _ _ mem], insert assms, auto)
next
assume mem: "(mset xs, mset ys) ∈ ns_mul_ext {(x, y). snd (P x y)} {(x, y). fst (P x y)}"
show "(mset xs, mset ys) ∈ ns_mul_ext {(x, y). snd (P' x y)} {(x, y). fst (P' x y)}"
by (rule ns_mul_ext_local_mono[OF _ _ mem], insert assms, auto)
qed
subsection ‹Special case: non-strict order is equality›
lemma ns_mul_ext_IdE:
assumes "(M, N) ∈ ns_mul_ext Id R"
obtains X and Y and Z where "M = X + Z" and "N = Y + Z"
and "∀y ∈ set_mset Y. ∃x ∈ set_mset X. (x, y) ∈ R"
using assms
by (auto simp: ns_mul_ext_def elim!: mult2_alt_nsE) (insert union_commute, blast)
lemma ns_mul_ext_IdI:
assumes "M = X + Z" and "N = Y + Z" and "∀y ∈ set_mset Y. ∃x ∈ set_mset X. (x, y) ∈ R"
shows "(M, N) ∈ ns_mul_ext Id R"
using assms mult2_alt_nsI[of N Z Y M Z X Id "R¯"]
by (auto simp: ns_mul_ext_def)
lemma s_mul_ext_IdE:
assumes "(M, N) ∈ s_mul_ext Id R"
obtains X and Y and Z where "X ≠ {#}" and "M = X + Z" and "N = Y + Z"
and "∀y ∈ set_mset Y. ∃x ∈ set_mset X. (x, y) ∈ R"
using assms
by (auto simp: s_mul_ext_def elim!: mult2_alt_sE) (metis union_commute)
lemma s_mul_ext_IdI:
assumes "X ≠ {#}" and "M = X + Z" and "N = Y + Z"
and "∀y ∈ set_mset Y. ∃x ∈ set_mset X. (x, y) ∈ R"
shows "(M, N) ∈ s_mul_ext Id R"
using assms mult2_alt_sI[of N Z Y M Z X Id "R¯"]
by (auto simp: s_mul_ext_def ac_simps)
lemma mult_s_mul_ext_conv:
assumes "trans R"
shows "(mult (R¯))¯ = s_mul_ext Id R"
using mult2_s_eq_mult2_s_alt[of Id "R¯"] assms
by (auto simp: s_mul_ext_def refl_Id mult2_s_def)
lemma ns_mul_ext_Id_eq:
"ns_mul_ext Id R = (s_mul_ext Id R)⇧="
by (auto simp add: ns_mul_ext_def s_mul_ext_def mult2_alt_ns_conv)
lemma subseteq_mset_imp_ns_mul_ext_Id:
assumes "A ⊆# B"
shows "(B, A) ∈ ns_mul_ext Id R"
proof -
obtain C where [simp]: "B = C + A" using assms by (auto simp: mset_subset_eq_exists_conv ac_simps)
have "(C + A, {#} + A) ∈ ns_mul_ext Id R"
by (intro ns_mul_ext_IdI [of _ C A _ "{#}"]) auto
then show ?thesis by simp
qed
lemma subset_mset_imp_s_mul_ext_Id:
assumes "A ⊂# B"
shows "(B, A) ∈ s_mul_ext Id R"
using assms by (intro supset_imp_s_mul_ext) (auto simp: refl_Id)
end