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)"
by (simp add: count_eq)

lemma count_0: "(∀x. count_list B x = 0) = (B = [])"
by (simp add: count_list_0_iff)

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"
by (simp add: count_eq multiset_eq_iff)

lemma perm_count_conv: "mset A = mset B ⟷ (∀ x. count_list A x = count_list B x)"
by (simp add: count_eq multiset_eq_iff)


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
    thus ?thesis by(simp add:distinct_remdups_id)
  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)"
      apply(simp add: xs remdups_append) done 
    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)"
  by(simp add: rem_def)

lemma length_rem: "length (rem x xs) <= length xs"
  by(simp add: rem_def)

lemma rem_notin: "x ~: set xs ==> rem x xs = xs"
  apply(simp add: rem_def)
  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)
     apply (simp_all add: weak)
    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(simp add: y'_def)
    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)"
  apply(simp add: perm_count_conv)
  apply(simp add: multiset_eq_iff)
  apply(simp add: count_count)
  done

lemma set_of_multiset_of_list: "set_of (multiset_of_list A) = set A"
  by (induct A) auto
*)
end