theory Dual_Multiset
imports
QTRS.List_Order
QTRS.Util
begin
abbreviation dms_order_idx_i where "dms_order_idx_i S NS idx ss ts i ≡
fst (idx i) < length ts ∧
(snd (idx i) ⟶ (ss ! i, ts ! fst (idx i)) ∈ S) ∧
(¬ snd (idx i) ⟶ (ss ! i, ts ! fst (idx i)) ∈ NS) ∧
(¬ snd (idx i) ⟶ (∀ i' < length ss. fst (idx i) = fst (idx i') ⟶ i = i'))"
abbreviation dms_order_idx where "dms_order_idx S NS idx ss ts stri ≡ (∀ i < length ss. dms_order_idx_i S NS idx ss ts i) ∧ (stri ⟶ (∃ j < length ts. (∀ i < length ss. idx i ≠ (j,False))))"
definition dms_order :: "nat ⇒ bool ⇒ 'a rel ⇒ 'a rel ⇒ 'a list rel"
where "dms_order n stri S NS ≡ { (ss,ts). (length ts ≤ n ∨ length ss = length ts)
∧ (∃ idx. dms_order_idx S NS idx ss ts stri)}"
lemma dms_orderI:
assumes "length ts ≤ n ∨ length ss = length ts"
"⋀ i. i < length ss ⟹ dms_order_idx_i S NS idx ss ts i"
"stri ⟹ ∃ j < length ts. (∀ i < length ss. idx i ≠ (j,False))"
shows "(ss,ts) ∈ dms_order n stri S NS"
using assms unfolding dms_order_def by blast
lemma dms_order_refl: assumes "⋀ s. (s,s) ∈ NS"
shows "(ss,ss) ∈ dms_order n False S NS"
by (rule dms_orderI[of ss n ss "λ i. (i,False)"], insert assms, auto)
lemma dms_order_trans: assumes trans: "S O NS ⊆ S" "NS O S ⊆ S" "trans NS" "trans S"
and mem1: "(ss1,ss2) ∈ dms_order n stri1 S NS"
and mem2: "(ss2,ss3) ∈ dms_order n stri2 S NS"
shows "(ss1,ss3) ∈ dms_order n (stri1 ∨ stri2) S NS"
proof -
let ?n1 = "length ss1"
let ?n2 = "length ss2"
let ?n3 = "length ss3"
note mem1 = mem1[unfolded dms_order_def]
note mem2 = mem2[unfolded dms_order_def]
from mem1 have n1: "?n2 ≤ n ∨ ?n1 = ?n2" by auto
from mem2 have n2: "?n3 ≤ n ∨ ?n2 = ?n3" by auto
have n: "?n3 ≤ n ∨ ?n1 = ?n3"
by (cases "?n2 = ?n3", insert n1 n2, auto)
note mem = dms_orderI[OF n]
let ?Q = "dms_order_idx_i S NS"
let ?P = "dms_order_idx S NS"
from mem1 obtain idx1 where mem1: "?P idx1 ss1 ss2 stri1" by blast
from mem2 obtain idx2 where mem2: "?P idx2 ss2 ss3 stri2" by blast
let ?idx = "λ i. case idx1 i of (i',str) ⇒ case idx2 i' of (i'',str') ⇒ (i'',str ∨ str')"
obtain idx where idx: "idx = ?idx " by auto
{
fix i
assume i: "i < ?n1"
obtain i' str1 where idx1: "idx1 i = (i',str1)" by force
obtain i'' str2 where idx2: "idx2 i' = (i'',str2)" by force
note mem1i = mem1[THEN conjunct1, rule_format, OF i, unfolded idx1 fst_conv snd_conv]
from mem1i have i': "i' < ?n2" by simp
note mem2i = mem2[THEN conjunct1, rule_format, OF i', unfolded idx2 fst_conv snd_conv]
from mem2i have i'': "i'' < ?n3" by simp
have "?Q idx ss1 ss3 i" unfolding idx idx1 split idx2 fst_conv snd_conv
proof(intro conjI impI, rule i'')
assume one: "str1 ∨ str2"
show "(ss1 ! i, ss3 ! i'') ∈ S"
proof (cases str1)
case False
with one have str1: "¬ str1" and str2: "str2" by auto
from str1 mem1i have one: "(ss1 ! i, ss2 ! i') ∈ NS" by auto
from str2 mem2i have two: "(ss2 ! i', ss3 ! i'') ∈ S" by auto
from trans(2) one two show ?thesis by blast
next
case True
with mem1i have one: "(ss1 ! i, ss2 ! i') ∈ S" by auto
show ?thesis
proof (cases str2)
case False
with mem2i have two: "(ss2 ! i', ss3 ! i'') ∈ NS" by auto
from trans(1) one two show ?thesis by blast
next
case True
with mem2i have two: "(ss2 ! i', ss3 ! i'') ∈ S" by auto
from trans(4) one two show ?thesis unfolding trans_def by blast
qed
qed
next
assume "¬ (str1 ∨ str2)"
hence str1: "¬ str1" and str2: "¬ str2" by auto
from str1 mem1i have one: "(ss1 ! i, ss2 ! i') ∈ NS" by auto
from str2 mem2i have two: "(ss2 ! i', ss3 ! i'') ∈ NS" by auto
from trans(3) one two show "(ss1 ! i, ss3 ! i'') ∈ NS" unfolding trans_def by blast
next
assume "¬ (str1 ∨ str2)"
hence str1: "¬ str1" and str2: "¬ str2" by auto
let ?R = "λ i'. i'' = fst (?idx i') ⟶ i = i'"
show "∀ i' < ?n1. ?R i'"
proof (intro allI impI)
fix j
assume j: "j < ?n1" and idx: "i'' = fst (?idx j)"
obtain j' str1' where idx1': "idx1 j = (j',str1')" by force
obtain j'' str2' where idx2': "idx2 j' = (j'',str2')" by force
note mem1j = mem1[THEN conjunct1, rule_format, OF j, unfolded idx1' fst_conv snd_conv]
from mem1j have j': "j' < ?n2" by simp
note mem2j = mem2[THEN conjunct1, rule_format, OF i', unfolded idx2' fst_conv snd_conv]
from mem1i str1 j have one: "i' = fst (idx1 j) ⟹ i = j" by auto
from mem2i str2 j' have two: "i'' = fst (idx2 j') ⟹ i' = j'" by auto
show "i = j"
by (rule one, unfold idx1' fst_conv, rule two, unfold idx2',
unfold idx idx1' split idx2', simp)
qed
qed
} note Q = this
note mem = mem[of idx]
show ?thesis
proof (rule mem, rule Q)
assume "stri1 ∨ stri2"
thus "∃ j < ?n3. ∀ i < ?n1. idx i ≠ (j, False)"
proof
assume stri2
with mem2 obtain j where j: "j < ?n3" and neq: "⋀ i. i < ?n2 ⟹ (idx2 i ≠ (j, False))" by auto
show ?thesis
proof (intro exI conjI allI impI, rule j)
fix i
assume i: "i < ?n1"
obtain i' str1 where idx1: "idx1 i = (i',str1)" by force
obtain i'' str2 where idx2: "idx2 i' = (i'',str2)" by force
note mem1i = mem1[THEN conjunct1, rule_format, OF i, unfolded idx1 fst_conv snd_conv]
from mem1i have i': "i' < ?n2" by simp
show "idx i ≠ (j, False)" using neq[OF i'] unfolding idx idx1 split idx2 by auto
qed
next
assume stri1
with mem1 obtain j where j: "j < ?n2" and neq: "⋀ i. i < ?n1 ⟹ (idx1 i ≠ (j, False))" by auto
let ?j = "fst (idx2 j)"
from mem2 j have j': "?j < ?n3" by auto
show ?thesis
proof (intro exI conjI allI impI, rule j')
fix i
assume i: "i < ?n1"
obtain i' str1 where idx1: "idx1 i = (i',str1)" by force
obtain i'' str2 where idx2: "idx2 i' = (i'',str2)" by force
note mem1i = mem1[THEN conjunct1, rule_format, OF i, unfolded idx1 fst_conv snd_conv]
from mem1i have i': "i' < ?n2" by simp
show "idx i ≠ (?j, False)" unfolding idx idx1 split idx2
proof (cases "i' = j")
case True
show "(i'', str1 ∨ str2) ≠ (?j, False)"
using neq[OF i] unfolding idx1 unfolding True by auto
next
case False note ij = this
show "(i'',str1 ∨ str2) ≠ (?j, False)"
proof (cases "str2")
case True thus ?thesis by simp
next
case False
with mem2[THEN conjunct1, rule_format, OF i', unfolded idx2 snd_conv fst_conv]
have "⋀ j. j < ?n2 ⟹ i'' = fst (idx2 j) ⟹ i' = j" by blast
from this[OF j] ij show ?thesis by auto
qed
qed
qed
qed
qed
qed
lemma (in order_pair) dms_order_order_pair: "order_pair (dms_order n True S NS) (dms_order n False S NS)" (is "order_pair ?S ?NS")
proof -
note trans = dms_order_trans[OF compat_S_NS compat_NS_S trans_NS trans_S, of _ _ n]
show ?thesis
proof
show "refl ?NS" using refl_NS unfolding refl_on_def
using dms_order_refl[of NS _ n S] by auto
next
show "trans ?S" unfolding trans_def using trans[of _ _ True _ True, simplified] by blast
next
show "trans ?NS" unfolding trans_def using trans[of _ _ False _ False, simplified] by blast
next
show "?S O ?NS ⊆ ?S" using trans[of _ _ True _ False, simplified] by blast
next
show "?NS O ?S ⊆ ?S" using trans[of _ _ False _ True, simplified] by blast
qed
qed
context
begin
qualified fun trace where "trace idxs (Suc 0) = 0"
| "trace idxs (Suc i) = (fst (idxs i (trace idxs i)))"
end
lemma (in SN_order_pair) dms_order_SN_order_pair: "SN_order_pair (dms_order n True S NS) (dms_order n False S NS)" (is "SN_order_pair ?S ?NS")
proof -
interpret dms_order: order_pair ?S ?NS
by (rule dms_order_order_pair)
show ?thesis
proof
let ?b = "λ (f :: nat ⇒ 'a list) b. (∀ i. length (f i) ≤ b)"
obtain size where size: "size = (λ f. LEAST b. ?b f b)" by auto
{
fix f
assume steps: "⋀ i. (f i, f (Suc i)) ∈ ?S"
from steps have False
proof (induct f rule: wf_induct[OF wf_measure[of size]])
case (1 f)
note steps = 1(2)
let ?P = "λ idx i. dms_order_idx S NS idx (f i) (f (Suc i)) True"
{
fix i
from steps[of i, unfolded dms_order_def] have "∃ idx. ?P idx i" by blast
}
from choice[OF allI[OF this]] have "∃ idx. ∀ i. ?P (idx i) i" .
then obtain idx where idx: "⋀ i. ?P (idx i) i" by blast
let ?Q = "λ i. dms_order_idx_i S NS (idx i) (f i) (f (Suc i))"
obtain t where t: "t = Dual_Multiset.trace idx" by auto
obtain s where s: "s = (λ i. snd (idx i (t i)))" by auto
{
fix i
have "t (Suc i) < length (f (Suc i))"
proof (induct i)
case 0
show ?case using idx[of 0] t by auto
next
case (Suc i)
show ?case using idx[THEN conjunct1, rule_format, OF Suc] t by auto
qed
} note len = this
{
fix i
assume "i > (0 :: nat)"
then obtain j where i: "i = Suc j" by (cases i, auto)
from len[of j] have "t i < length (f i)" unfolding i by simp
} note len = this
{
fix i
assume "i > (0 :: nat)"
then obtain j where i: "i = Suc j" by (cases i, auto)
have "idx i (t i) = (t (Suc i), s i)"
unfolding i s t by simp
} note idx_ts = this
let ?f = "λ i. f i ! t i"
obtain g where g: "g = (λ i. ?f (Suc i))" by auto
have Suc0: "⋀ i. Suc i > (0 :: nat)" by simp
{
fix i
assume "s (Suc i)"
hence "(g i, g (Suc i)) ∈ S"
using idx[THEN conjunct1, rule_format, OF len[OF Suc0[of i]]]
unfolding idx_ts[OF Suc0] g by simp
} note stri = this
{
fix i
assume "¬ s (Suc i)"
hence "(g i, g (Suc i)) ∈ NS"
using idx[THEN conjunct1, rule_format, OF len[OF Suc0[of i]]]
unfolding idx_ts[OF Suc0] g by simp
} note nstri = this
from SN have SN_g0: "SN_on S {g 0}" unfolding SN_defs by auto
from stri nstri have "∀ i. (g i, g (Suc i)) ∈ NS ∪ S" by auto
from non_strict_ending[OF this compat_NS_S, OF SN_g0]
obtain j where not_stri: "⋀ i. i ≥ j ⟹ (g i, g (Suc i)) ∉ S" by auto
{
fix i
assume ij: "i > j"
hence 0: "i > 0" and ij: "i - Suc 0 ≥ j" by auto
from not_stri[OF ij] stri[of "i - Suc 0"] have "¬ s (Suc (i - Suc 0))" by auto
with 0 have "¬ s i" by auto
with idx_ts[OF 0] have "idx i (t i) = (t (Suc i), False)" by simp
} note idx_False = this
let ?j = "Suc j"
obtain h where h: "h = shift (λ i. remove_nth (t i) (f i)) ?j" by auto
obtain idx' where idx': "idx' = shift (λ i j.
(adjust_idx_rev (t (Suc i)) (fst (idx i (adjust_idx (t i) j))), snd (idx i (adjust_idx (t i) j)))) ?j" by auto
{
fix i
have "t (i + ?j) < length (f (i + ?j))"
by (rule len, simp)
} note tlen = this
{
fix i
have "length (f (i + ?j)) = Suc (length (h i))"
unfolding h shift.simps
by (rule remove_nth_len[OF tlen])
} note len = this
{
fix i
let ?ij = "i + ?j"
let ?i = "t ?ij"
let ?sij = "Suc i + ?j"
let ?si = "t ?sij"
note tleni = tlen[of i]
{
fix k
let ?k = "adjust_idx ?i k"
assume "k < length (h i)"
have "idx' i k = (adjust_idx_rev ?si (fst (idx ?ij ?k)), snd (idx ?ij ?k))" unfolding idx' by simp
} note idx' = this
{
fix k
assume "k < length (h i)"
from this[unfolded h, simplified]
have "k < length (remove_nth ?i (f ?ij))" by simp
from adjust_idx_length[OF tlen this]
have alen: "adjust_idx ?i k < length (f ?ij)" .
from idx[THEN conjunct1, rule_format, OF alen]
have dms_order: "dms_order_idx_i S NS (idx ?ij) (f ?ij) (f (Suc ?ij)) (adjust_idx ?i k)" .
note alen dms_order
} note alen_dms_order = this
{
fix k
let ?k = "adjust_idx ?i k"
assume klen: "k < length (h i)"
from idx[of ?ij, THEN conjunct1, rule_format, OF tlen[of i]]
have dms_order: "dms_order_idx_i S NS (idx ?ij) (f ?ij) (f (Suc ?ij)) ?i" .
from dms_order[THEN conjunct2]
have eq: "⋀ i'. ¬ snd (idx ?ij ?i) ⟹ i' < length (f ?ij) ⟹ fst (idx ?ij ?i) = fst (idx ?ij i') ⟹ ?i = i'" by auto
have "fst (idx ?ij ?k) ≠ ?si"
proof
assume "fst (idx ?ij ?k) = ?si"
hence id: "fst (idx ?ij ?i) = fst (idx ?ij ?k)" unfolding t by simp
have klen: "k < length (remove_nth ?i (f ?ij))"
using klen remove_nth_len[OF tlen[of i]] unfolding h by simp
from idx_False[of ?ij] have "¬ snd (idx ?ij ?i)" by simp
note eq = eq[OF this adjust_idx_length[OF tlen klen] id]
with adjust_idx_i[of ?i k]
show False by simp
qed
} note neq = this
have "(h i, h (Suc i)) ∈ ?S"
proof (rule dms_orderI)
from len have len: "⋀ i. length (h i) = length (f (i + ?j)) - Suc 0" by simp
show "length (h (Suc i)) ≤ n ∨ length (h i) = length (h (Suc i))"
unfolding len using steps[of ?ij, unfolded dms_order_def] by auto
next
fix k
assume k: "k < length (h i)"
from alen_dms_order[OF k]
have alen: "adjust_idx ?i k < length (f ?ij)"
and dms_order: "dms_order_idx_i S NS (idx ?ij) (f ?ij) (f (Suc ?ij)) (adjust_idx ?i k)" .
let ?k = "adjust_idx ?i k"
have neqk:
"fst (idx ?ij ?k) ≠ ?si" by (rule neq[OF k])
show "dms_order_idx_i S NS (idx' i) (h i) (h (Suc i)) k"
proof (intro conjI impI allI,
unfold idx'[OF k] fst_conv snd_conv h shift.simps adjust_idx_nth[OF tleni] adjust_idx_rev2[OF neqk] adjust_idx_nth[OF tlen[of "Suc i"]])
assume "snd (idx ?ij ?k)"
thus "(f ?ij ! ?k, f ?sij ! fst (idx ?ij ?k)) ∈ S"
using dms_order by auto
next
assume "¬ snd (idx ?ij ?k)"
thus "(f ?ij ! ?k, f ?sij ! fst (idx ?ij ?k)) ∈ NS"
using dms_order by auto
next
show "adjust_idx_rev ?si (fst (idx ?ij ?k)) < length (remove_nth ?si (f ?sij))"
by (rule adjust_idx_rev_length, insert dms_order neqk tlen[of "Suc i"], auto)
next
fix k'
assume nstri: "¬ snd (idx ?ij ?k)"
and k': "k' < length (remove_nth ?i (f ?ij))"
and id: "adjust_idx_rev ?si (fst (idx ?ij ?k)) = fst (idx' i k')"
have k'h: "k' < length (h i)" using k' unfolding h by simp
let ?k' = "adjust_idx ?i k'"
from id[unfolded idx'[OF k'h]]
have id: "adjust_idx_rev ?si (fst (idx ?ij ?k)) = adjust_idx_rev ?si (fst (idx ?ij ?k'))" (is "?l = ?r") by simp
hence "adjust_idx ?si ?l = adjust_idx ?si ?r" by simp
from this[unfolded adjust_idx_rev2[OF neqk] adjust_idx_rev2[OF neq[OF k'h]]]
have id: "fst (idx ?ij ?k) = fst (idx ?ij ?k')" .
from dms_order[THEN conjunct2]
have eq: "⋀ k'. ¬ snd (idx ?ij ?k) ⟹ k' < length (f ?ij) ⟹ fst (idx ?ij ?k) = fst (idx ?ij k') ⟹ ?k = k'" by auto
from eq[OF nstri adjust_idx_length[OF tlen k'] id]
have "adjust_idx_rev ?i ?k = adjust_idx_rev ?i ?k'" by simp
thus "k = k'" unfolding adjust_idx_rev1 by simp
qed
next
from idx[THEN conjunct2, of "?ij"] obtain k
where k: "k < length (f ?sij)"
and neqk: "⋀ k'. k' < length (f ?ij) ⟹ idx ?ij k' ≠ (k,False)" by auto
let ?k = "adjust_idx_rev ?si k"
from idx_False[of ?ij] have idxi: "idx ?ij ?i = (?si, False)" by simp
have ksi: "k ≠ ?si"
proof
assume "k = ?si"
with idxi have "idx ?ij ?i = (k,False)" by simp
with neqk[OF tlen] show False by simp
qed
have kh: "?k < length (h (Suc i))" unfolding h shift.simps
by (rule adjust_idx_rev_length[OF tlen k ksi])
show "∃ k < length (h (Suc i)). ∀ k' < length (h i). idx' i k' ≠ (k, False)"
proof (intro exI conjI allI impI, rule kh)
fix k'
assume k': "k' < length (h i)"
let ?k' = "adjust_idx ?i k'"
have ak': "?k' < length (f ?ij)"
by (rule adjust_idx_length[OF tlen], insert k', unfold h, simp)
from neqk[OF ak'] have neqk: "idx ?ij ?k' ≠ (k,False)" .
show "idx' i k' ≠ (?k, False)"
proof
assume id: "idx' i k' = (?k, False)"
from this[unfolded idx'[OF k']]
have id: "adjust_idx_rev ?si (fst (idx ?ij ?k')) =
adjust_idx_rev ?si k" (is "?l = ?r") and nstri: "¬ snd (idx ?ij ?k')" unfolding t by auto
from id have "adjust_idx ?si ?l = adjust_idx ?si ?r" by simp
from this[unfolded adjust_idx_rev2[OF ksi] adjust_idx_rev2[OF neq[OF k']]] have id: "fst (idx ?ij ?k') = k" .
have "idx ?ij ?k' = (fst (idx ?ij ?k'), snd (idx ?ij ?k'))" by simp
also have "... = (k, False)" unfolding id using nstri by simp
also have "... ≠ idx ?ij ?k'" using neqk by simp
finally show False by simp
qed
qed
qed
} note hsteps = this
show False
proof (rule 1(1)[rule_format, of h, OF _ hsteps])
show "(h,f) ∈ measure size" unfolding in_measure
proof -
{
fix f
assume steps: "⋀ i. (f i, f (Suc i)) ∈ ?S"
let ?n = "max n (length (f 0))"
{
fix i
have "length (f i) ≤ ?n"
proof (induct i)
case (Suc i)
from steps[of i, unfolded dms_order_def] Suc show ?case by auto
qed simp
}
hence "?b f ?n" by simp
from LeastI[of "?b f", OF this] have bound: "?b f (size f)" unfolding size .
have bound2: "∃ i. length (f i) = size f"
proof (rule ccontr)
assume "¬ ?thesis"
hence neq: "⋀ i. length (f i) ≠ size f" by auto
{
fix i
from neq[of i] bound[rule_format, of i] have "length (f i) < size f" by auto
hence "length (f i) ≤ size f - Suc 0" by auto
}
from Least_le[of "?b f", OF allI[OF this]] have "size f ≤ size f - Suc 0" unfolding size by simp
hence "size f = 0" by simp
with bound[rule_format, of 0] neq[of 0] show False by simp
qed
note bound bound2
} note size = this
from size(2)[of h, OF hsteps] obtain i where "length (h i) = size h"
by blast
hence "size h = length (h i)" by simp
also have "... < length (f (i + ?j))" unfolding h
unfolding remove_nth_len[OF tlen[of i]] by simp
also have "... ≤ size f" using size(1)[of f, OF steps] by auto
finally show "size h < size f" .
qed
qed
qed
}
thus "SN ?S" unfolding SN_defs by auto
qed
qed
lemma dms_order_map: assumes fS: "⋀a b. (a, b) ∈ S ⟹ (f a, f b) ∈ S"
and fNS: "⋀a b. (a, b) ∈ NS ⟹ (f a, f b) ∈ NS"
and mem: "(ss1, ss2) ∈ dms_order n stri S NS"
shows "(map f ss1, map f ss2) ∈ dms_order n stri S NS"
proof -
let ?Q = "dms_order_idx_i S NS"
let ?P = "dms_order_idx S NS"
note mem = mem[unfolded dms_order_def]
let ?n1 = "length ss1"
let ?n2 = "length ss2"
let ?n1' = "length (map f ss1)"
let ?n2' = "length (map f ss2)"
from mem have "?n2' ≤ n ∨ ?n1' = ?n2'" by simp
note dms_order = dms_orderI[OF this]
from mem obtain idx where mem: "?P idx ss1 ss2 stri" unfolding dms_order_def by blast
hence "stri ⟹ ∃ j < ?n2'. (∀ i < ?n1'. idx i ≠ (j,False))" by auto
note dms_order = dms_order[OF _ this]
show ?thesis
proof (rule dms_order)
fix i
assume "i < ?n1'"
hence i: "i < ?n1" by simp
with mem have Q: "?Q idx ss1 ss2 i" by simp
let ?i = "fst (idx i)"
from Q i have i': "?i < ?n2" by simp
show "?Q idx (map f ss1) (map f ss2) i"
proof (intro conjI impI, unfold nth_map[OF i] nth_map[OF i'])
assume stri: "snd (idx i)"
show "(f (ss1 ! i), f (ss2 ! ?i)) ∈ S"
by (rule fS, insert Q i stri, auto)
next
assume nstri: "¬ snd (idx i)"
show "(f (ss1 ! i), f (ss2 ! ?i)) ∈ NS"
by (rule fNS, insert Q i nstri, auto)
qed (insert i' Q, auto)
qed
qed
interpretation dms_order: list_order_extension "dms_order n True" "dms_order n False"
proof -
let ?S = "dms_order n True"
let ?NS = "dms_order n False"
show "list_order_extension ?S ?NS"
proof (rule list_order_extension.intro[OF _ dms_order_map dms_order_map])
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 .
show "SN_order_pair ?s ?ns" by (rule dms_order_SN_order_pair)
next
fix as bs :: "'b list" and NS S :: "'b rel"
let ?n1 = "length as"
let ?n2 = "length bs"
assume len: "?n1 = ?n2" and ns: "⋀ i. i < ?n2 ⟹ (as ! i, bs ! i) ∈ NS"
show "(as,bs) ∈ ?NS S NS"
proof (rule dms_orderI)
fix i
assume "i < ?n1"
thus "dms_order_idx_i S NS (λ i. (i,False)) as bs i" using ns len by auto
qed (insert len, auto)
qed
qed
lemma dms_order_mono:
assumes ns: "set ss1 × set ss2 ∩ NS ⊆ NS'"
and s: "set ss1 × set ss2 ∩ S ⊆ S'"
and mem: "(ss1,ss2) ∈ dms_order n stri S NS"
shows "(ss1,ss2) ∈ dms_order n stri S' NS'"
proof -
let ?Q = "dms_order_idx_i S NS"
let ?Q' = "dms_order_idx_i S' NS'"
let ?P = "dms_order_idx S NS"
note mem = mem[unfolded dms_order_def]
let ?n1 = "length ss1"
let ?n2 = "length ss2"
from mem have "?n2 ≤ n ∨ ?n1 = ?n2" by simp
note dms = dms_orderI[OF this]
from mem obtain idx where mem: "?P idx ss1 ss2 stri" unfolding dms_order_def by blast
hence "stri ⟹ ∃ j < ?n2. (∀ i < ?n1. idx i ≠ (j,False))" by auto
note dms = dms[OF _ this]
show ?thesis
proof (rule dms)
fix i
assume i: "i < length ss1"
hence si: "ss1 ! i ∈ set ss1" by auto
from mem i have Q: "?Q idx ss1 ss2 i" by simp
let ?j = "fst (idx i)"
from Q i have "?j < length ss2" by auto
hence sj: "ss2 ! ?j ∈ set ss2" by auto
show "?Q' idx ss1 ss2 i"
proof(intro conjI allI impI)
assume "snd (idx i)"
with Q si sj s show "(ss1 ! i, ss2 ! ?j) ∈ S'" by auto
next
assume "¬ snd (idx i)"
with Q si sj ns show "(ss1 ! i, ss2 ! ?j) ∈ NS'" by auto
qed (insert Q, auto)
qed
qed
end