# Theory PermutationLemmas

```section "Permutation Lemmas"

theory PermutationLemmas
imports "HOL-Library.Multiset"
begin

― ‹following function is very close to that in multisets- now we can make the connection that x <~~> y iff the multiset of x is the same as that of y›

subsection "perm, count equivalence"

lemma count_eq:
‹count_list xs x = Multiset.count (mset xs) x›
by (induction xs) simp_all

lemma perm_count: "mset A = mset B ⟹ (∀ x. count_list A x = count_list B x)"

lemma count_0: "(∀x. count_list B x = 0) = (B = [])"

lemma count_Suc: "count_list B a = Suc m ⟹ a : set B"
by (metis Zero_not_Suc count_notin)

lemma count_perm: "!! B. (∀ x. count_list A x = count_list B x) ⟹ mset A = mset B"

lemma perm_count_conv: "mset A = mset B ⟷ (∀ x. count_list A x = count_list B x)"

subsection "Properties closed under Perm and Contr hold for x iff hold for remdups x"

lemma remdups_append: "y : set ys --> remdups (ws@y#ys) = remdups (ws@ys)"
apply (induct ws, simp)
apply (case_tac "y = a", simp, simp)
done

lemma perm_contr': assumes perm[rule_format]: "! xs ys. mset xs = mset ys --> (P xs = P ys)"
and contr'[rule_format]: "! x xs. P(x#x#xs) = P (x#xs)"
shows "! xs. length xs = n --> (P xs = P (remdups xs))"
apply(induct n rule: nat_less_induct)
proof (safe)
fix xs :: "'a list"
assume a[rule_format]: "∀m<length xs. ∀ys. length ys = m ⟶ P ys = P (remdups ys)"
show "P xs = P (remdups xs)"
proof (cases "distinct xs")
case True
next
case False
from not_distinct_decomp[OF this] obtain ws ys zs y where xs: "xs = ws@[y]@ys@[y]@zs" by force
have "P xs = P (ws@[y]@ys@[y]@zs)" by (simp add: xs)
also have "... = P ([y,y]@ws@ys@zs)"
apply(rule perm) apply(rule iffD2[OF perm_count_conv]) apply rule apply(simp) done
also have "... = P ([y]@ws@ys@zs)" apply simp apply(rule contr') done
also have "... = P (ws@ys@[y]@zs)"
apply(rule perm) apply(rule iffD2[OF perm_count_conv]) apply rule apply(simp) done
also have "... = P (remdups (ws@ys@[y]@zs))"
apply(rule a) by(auto simp: xs)
also have "(remdups (ws@ys@[y]@zs)) = (remdups xs)"
finally show "P xs = P (remdups xs)" .
qed
qed

lemma perm_contr: assumes perm: "! xs ys. mset xs = mset ys --> (P xs = P ys)"
and contr': "! x xs. P(x#x#xs) = P (x#xs)"
shows "(P xs = P (remdups xs))"
apply(rule perm_contr'[OF perm contr', rule_format]) by force

subsection "List properties closed under Perm, Weak and Contr are monotonic in the set of the list"

definition
rem :: "'a => 'a list => 'a list" where
"rem x xs = filter (%y. y ~= x) xs"

lemma rem: "x ~: set (rem x xs)"

lemma length_rem: "length (rem x xs) <= length xs"

lemma rem_notin: "x ~: set xs ==> rem x xs = xs"
apply(rule filter_True)
apply force
done

lemma perm_weak_filter': assumes perm[rule_format]: "! xs ys. mset xs = mset ys --> (P xs = P ys)"
and weak[rule_format]: "! x xs. P xs --> P (x#xs)"
shows "! ys. P (ys@filter Q xs) --> P (ys@xs)"
proof (rule allI, rule impI)
fix ys
define zs where ‹zs = filter (Not ∘ Q) xs›
assume ‹P (ys @ filter Q xs)›
then have ‹P (filter Q xs @ ys)›
apply (subst perm) defer apply assumption apply simp done
then have ‹P (zs @ filter Q xs @ ys)›
apply (induction zs)
done
with zs_def show ‹P (ys @ xs)›
apply (subst perm) defer apply assumption apply simp done
qed

lemma perm_weak_filter: assumes perm: "! xs ys. mset xs = mset ys --> (P xs = P ys)"
and weak: "! x xs. P xs --> P (x#xs)"
shows "P (filter Q xs) ==> P xs"
using perm_weak_filter'[OF perm weak, rule_format, of "[]", simplified]
by blast

― ‹right, now in a position to prove that in presence of perm, contr and weak, set x leq set y and x : ded implies y : ded›

lemma perm_weak_contr_mono:
assumes perm: "! xs ys. mset xs = mset ys --> (P xs = P ys)"
and contr: "! x xs. P (x#x#xs) --> P (x#xs)"
and weak: "! x xs. P xs --> P (x#xs)"
and xy: "set x <= set y"
and Px : "P x"
shows "P y"
proof -
from contr weak have contr': "! x xs. P(x#x#xs) = P (x#xs)" by blast

define y' where "y' = filter (% z. z : set x) y"
from xy have "set x = set y'" apply(simp add: y'_def) apply blast done
hence rxry': "mset (remdups x) = mset (remdups y')"
using set_eq_iff_mset_remdups_eq by auto

from Px perm_contr[OF perm contr'] have Prx: "P (remdups x)" by simp
with rxry' have "P (remdups y')" apply (subst perm) defer apply assumption apply simp done

with perm_contr[OF perm contr'] have "P y'" by simp
thus "P y"
apply(rule perm_weak_filter[OF perm weak]) .
qed

(* No, not used
subsection "Following used in Soundness"

primrec multiset_of_list :: "'a list ⇒ 'a multiset"
where
"multiset_of_list [] = {#}"
| "multiset_of_list (x#xs) = {#x#} + multiset_of_list xs"

lemma count_count[symmetric]: "count x A = Multiset.count (multiset_of_list A) x"
by (induct A) simp_all

lemma perm_multiset: "A <~~> B = (multiset_of_list A = multiset_of_list B)"