Theory Misc

(*  Title:       Miscellanneous Definitions and Lemmas
    Author:      Peter Lammich <peter.lammich@uni-muenster.de>
    Maintainer:  Peter Lammich <peter.lammich@uni-muenster.de>
*)

section ‹Miscellanneous Definitions and Lemmas›

theory Misc
imports Main "HOL-Library.Multiset" "HOL-Library.Subseq_Order"
begin
text_raw ‹\label{thy:Misc}›

text ‹Here we provide a collection of miscellaneous definitions and helper lemmas›

subsection "Miscellanneous (1)"
text ‹This stuff is used in this theory itself, and thus occurs in first place. There is another ,,Miscellaneous''-section at the end of this theory›
subsubsection "AC-operators"
  
text ‹Locale to declare AC-laws as simplification rules›
locale AC =
  fixes f
  assumes commute[simp]: "f x y = f y x"
  assumes assoc[simp]: "f (f x y) z = f x (f y z)"

lemma (in AC) left_commute[simp]: "f x (f y z) = f y (f x z)"
  by (simp only: assoc[symmetric]) simp

text ‹Locale to define functions from surjective, unique relations›
locale su_rel_fun =
  fixes F and f
  assumes unique: "⟦(A,B)∈F; (A,B')∈F⟧ ⟹ B=B'"
  assumes surjective: "⟦!!B. (A,B)∈F ⟹ P⟧ ⟹ P"
  assumes f_def: "f A == THE B. (A,B)∈F"

lemma (in su_rel_fun) repr1: "(A,f A)∈F" proof (unfold f_def)
  obtain B where "(A,B)∈F" by (rule surjective)
  with theI[where P="λB. (A,B)∈F", OF this] show "(A, THE x. (A, x) ∈ F) ∈ F" by (blast intro: unique)
qed
  
lemma (in su_rel_fun) repr2: "(A,B)∈F ⟹ B=f A" using repr1
  by (blast intro: unique)

lemma (in su_rel_fun) repr: "(f A = B) = ((A,B)∈F)" using repr1 repr2
  by (blast) 


subsection ‹Abbreviations for list order›

abbreviation ileq :: "'a list ⇒ 'a list ⇒ bool"  (infix "≼" 50) where
  "(≼) ≡ (≤)"

abbreviation ilt :: "'a list ⇒ 'a list ⇒ bool"  (infix "≺" 50) where
  "(≺) ≡ (<)"


subsection ‹Multisets›

(*
  The following is a syntax extension for multisets. Unfortunately, it depends on a change in the Library/Multiset.thy, so it is commented out here, until it will be incorporated 
  into Library/Multiset.thy by its maintainers.

  The required change in Library/Multiset.thy is removing the syntax for single:
     - single :: "'a => 'a multiset"    ("{#_#}")
     + single :: "'a => 'a multiset"

  And adding the following translations instead:
  
     + syntax
     + "_multiset" :: "args ⇒ 'a multiset" ("{#(_)#}")

     + translations
     +   "{#x, xs#}" == "{#x#} + {#xs#}" 
     +   "{# x #}" == "single x"

  This translates "{# … #}" into a sum of singletons, that is parenthesized to the right. ?? Can we also achieve left-parenthesizing ??

*)


  (* Let's try what happens if declaring AC-rules for multiset union as simp-rules *)
(*declare union_ac[simp] -- don't do it !*)

subsubsection ‹Case distinction›

lemma multiset_induct'[case_names empty add]: "⟦P {#}; ⋀M x. P M ⟹ P ({#x#}+M)⟧ ⟹ P M"
  by (induct rule: multiset_induct) (auto simp add: union_commute)

subsubsection ‹Count›
  lemma count_ne_remove: "⟦ x ~= t⟧ ⟹ count S x = count (S-{#t#}) x"
    by (auto)
  lemma mset_empty_count[simp]: "(∀p. count M p = 0) = (M={#})"
    by (auto simp add: multiset_eq_iff)

subsubsection ‹Union, difference and intersection›

  lemma size_diff_se: "⟦t ∈# S⟧ ⟹ size S = size (S - {#t#}) + 1" proof (unfold size_multiset_overloaded_eq)
    let ?SIZE = "sum (count S) (set_mset S)"
    assume A: "t ∈# S"
    from A have SPLITPRE: "finite (set_mset S) & {t}⊆(set_mset S)" by auto
    hence "?SIZE = sum (count S) (set_mset S - {t}) + sum (count S) {t}" by (blast dest: sum.subset_diff)
    hence "?SIZE = sum (count S) (set_mset S - {t}) + count (S) t" by auto
    moreover with A have "count S t = count (S-{#t#}) t + 1" by auto
    ultimately have D: "?SIZE = sum (count S) (set_mset S - {t}) + count (S-{#t#}) t + 1" by (arith)
    moreover have "sum (count S) (set_mset S - {t}) = sum (count (S-{#t#})) (set_mset S - {t})" proof -
      have "ALL x:(set_mset S - {t}) . count S x = count (S-{#t#}) x" by (auto iff add: count_ne_remove)
      thus ?thesis by simp
    qed
    ultimately have D: "?SIZE = sum (count (S-{#t#})) (set_mset S - {t}) + count (S-{#t#}) t + 1" by (simp)
    moreover
    { assume CASE: "t ∉# S - {#t#}"
      from CASE have "set_mset S - {t} = set_mset (S - {#t#})"
        by (simp add: at_most_one_mset_mset_diff)
      with CASE D have "?SIZE = sum (count (S-{#t#})) (set_mset (S - {#t#})) + 1"
        by (simp add: not_in_iff)
    }
    moreover
    { assume CASE: "t ∈# S - {#t#}"
      from CASE have 1: "set_mset S = set_mset (S-{#t#})"
        by (rule more_than_one_mset_mset_diff [symmetric])
      moreover from D have "?SIZE = sum (count (S-{#t#})) (set_mset S - {t}) + sum (count (S-{#t#})) {t} + 1" by simp
      moreover from SPLITPRE sum.subset_diff have "sum (count (S-{#t#})) (set_mset S) = sum (count (S-{#t#})) (set_mset S - {t}) + sum (count (S-{#t#})) {t}" by (blast)
      ultimately have "?SIZE = sum (count (S-{#t#})) (set_mset (S-{#t#})) + 1" by simp
    }
    ultimately show "?SIZE = sum (count (S-{#t#})) (set_mset (S - {#t#})) + 1" by blast
  qed

  (* TODO: Check whether this proof can be done simpler *)
  lemma mset_union_diff_comm: "t ∈# S ⟹ T + (S - {#t#}) = (T + S) - {#t#}" proof -
    assume "t ∈# S"
    then obtain S' where S: "S = add_mset t S'"
      by (metis insert_DiffM)
    then show ?thesis
      by auto
  qed

  lemma mset_right_cancel_union: "⟦a ∈# A+B; ~(a ∈# B)⟧ ⟹ a∈#A"
    by (simp)
  lemma mset_left_cancel_union: "⟦a ∈# A+B; ~(a ∈# A)⟧ ⟹ a∈#B"
    by (simp)
  
  lemmas mset_cancel_union = mset_right_cancel_union mset_left_cancel_union

  lemma mset_right_cancel_elem: "⟦a ∈# A+{#b#}; a~=b⟧ ⟹ a∈#A"
    apply(subgoal_tac "~(a ∈# {#b#})")
    apply(auto)
  done

  lemma mset_left_cancel_elem: "⟦a ∈# {#b#}+A; a~=b⟧ ⟹ a∈#A"
    apply(subgoal_tac "~(a ∈# {#b#})")
    apply(auto)
  done

  lemmas mset_cancel_elem = mset_right_cancel_elem mset_left_cancel_elem

  lemma mset_diff_cancel1elem[simp]: "~(a ∈# B) ⟹ {#a#}-B = {#a#}" proof -
    assume A: "~(a ∈# B)"
    hence "count ({#a#}-B) a = count ({#a#}) a" by (auto simp add: not_in_iff)
    moreover have "ALL e . e~=a ⟶ count ({#a#}-B) e = count ({#a#}) e" by auto
    ultimately show ?thesis by (auto simp add: multiset_eq_iff)
  qed

  (*lemma union_diff_assoc_se: "t ∈# B ⟹ (A+B)-{#t#} = A + (B-{#t#})"
    by (auto iff add: multiset_eq_iff)
  lemma union_diff_assoc_se2: "t ∈# A ⟹ (A+B)-{#t#} = (A-{#t#}) + B"
    by (auto iff add: multiset_eq_iff)
  lemmas union_diff_assoc_se = union_diff_assoc_se1 union_diff_assoc_se2*)

  lemma union_diff_assoc: "C-B={#} ⟹ (A+B)-C = A + (B-C)"
    by (simp add: multiset_eq_iff)

  lemma mset_union_2_elem: "{#a#}+{#b#} = M + {#c#} ⟹ {#a#}=M & b=c | a=c & {#b#}=M"
    by (auto simp: add_eq_conv_diff)

  lemma mset_un_cases[cases set, case_names left right]:
    "⟦a ∈# A + B; a∈#A ⟹ P; a∈#B ⟹ P⟧ ⟹ P"
    by (auto)

  lemma mset_unplusm_dist_cases[cases set, case_names left right]:
    assumes A: "add_mset s A = B+C"
    assumes L: "⟦B=add_mset s (B-{#s#}); A=(B-{#s#})+C⟧ ⟹ P"
    assumes R: "⟦C=add_mset s (C-{#s#}); A=B+(C-{#s#})⟧ ⟹ P" 
    shows P
  proof -
    from A[symmetric] have "s ∈# B+C" by simp
    thus ?thesis proof (cases rule: mset_un_cases)
      case left hence 1: "B=add_mset s (B-{#s#})" by simp
      with A have "add_mset s A = add_mset s ((B-{#s#})+C)" by (simp add: union_ac)
      hence 2: "A = (B-{#s#})+C" by (simp)
      from L[OF 1 2] show ?thesis .
    next
      case right hence 1: "C=add_mset s (C-{#s#})" by simp
      with A have "add_mset s A = add_mset s (B+(C-{#s#}))" by (simp add: union_ac)
      hence 2: "A = B+(C-{#s#})" by (simp)
      from R[OF 1 2] show ?thesis .
    qed
  qed

  lemma mset_unplusm_dist_cases2[cases set, case_names left right]:
    assumes A: "B+C = add_mset s A"
    assumes L: "⟦B=add_mset s (B-{#s#}); A=(B-{#s#})+C⟧ ⟹ P"
    assumes R: "⟦C=add_mset s (C-{#s#}); A=B+(C-{#s#})⟧ ⟹ P" 
    shows P
    using mset_unplusm_dist_cases[OF A[symmetric]] L R by blast

  lemma mset_single_cases[cases set, case_names loc env]: 
    assumes A: "add_mset s c = add_mset r' c'" 
    assumes CASES: "⟦s=r'; c=c'⟧ ⟹ P" "⟦c'={#s#}+(c'-{#s#}); c={#r'#}+(c-{#r'#}); c-{#r'#} = c'-{#s#} ⟧ ⟹ P" 
    shows "P"
  proof -
    { assume CASE: "s=r'"
      with A have "c=c'" by simp
      with CASE CASES have ?thesis by auto
    } moreover {
      assume CASE: "s≠r'"
      have "s∈#{#s#}+c" by simp
      with A have "s ∈# {#r'#} + c'" by simp
      with CASE have "s ∈# c'" 
        by simp
      from insert_DiffM[OF this, symmetric] have 1: "c' = add_mset s (c' - {#s#})" .
      with A have "{#s#}+c = {#s#}+({#r'#}+(c' - {#s#}))" by (auto simp add: union_ac)
      hence 2: "c={#r'#}+(c' - {#s#})" by (auto)
      hence 3: "c-{#r'#} = (c' - {#s#})" by auto
      from 1 2 3 CASES have ?thesis by auto
    } ultimately show ?thesis by blast
  qed

  lemma mset_single_cases'[cases set, case_names loc env]: 
    assumes A: "add_mset s c = add_mset r' c'" 
    assumes CASES: "⟦s=r'; c=c'⟧ ⟹ P" "!!cc. ⟦c'={#s#}+cc; c={#r'#}+cc; c'-{#s#}=cc; c-{#r'#}=cc⟧ ⟹ P" 
    shows "P"
    using A  CASES by (auto elim!: mset_single_cases)

  lemma mset_single_cases2[cases set, case_names loc env]: 
    assumes A: "add_mset s c = add_mset r' c'" 
    assumes CASES: "⟦s=r'; c=c'⟧ ⟹ P" "⟦c'=(c'-{#s#})+{#s#}; c=(c-{#r'#})+{#r'#}; c-{#r'#} = c'-{#s#} ⟧ ⟹ P" 
    shows "P" 
  proof -
    from A have "add_mset s c = add_mset r' c'" by simp
    thus ?thesis proof (cases rule: mset_single_cases)
      case loc with CASES show ?thesis by simp
    next
      case env with CASES show ?thesis by (simp add: union_ac)
    qed
  qed

  lemma mset_single_cases2'[cases set, case_names loc env]: 
    assumes A: "add_mset s c = add_mset r' c'" 
    assumes CASES: "⟦s=r'; c=c'⟧ ⟹ P" "!!cc. ⟦c'=cc+{#s#}; c=cc+{#r'#}; c'-{#s#}=cc; c-{#r'#}=cc⟧ ⟹ P" 
    shows "P"
    using A  CASES by (auto elim!: mset_single_cases2)

  lemma mset_un_single_un_cases [consumes 1, case_names left right]:
    assumes A: "add_mset a A = B + C"
      and CASES: "a ∈# B ⟹ A = (B - {#a#}) + C ⟹ P"
        "a ∈# C ⟹ A = B + (C - {#a#}) ⟹ P"
    shows P
  proof -
    have "a ∈# A+{#a#}" by simp
    with A have "a ∈# B+C" by auto
    thus ?thesis proof (cases rule: mset_un_cases)
      case left hence "B=B-{#a#}+{#a#}" by auto
      with A have "A+{#a#} = (B-{#a#})+C+{#a#}" by (auto simp add: union_ac)
      hence "A=(B-{#a#})+C" by simp
      with CASES(1)[OF left] show ?thesis by blast
    next
      case right hence "C=C-{#a#}+{#a#}" by auto
      with A have "A+{#a#} = B+(C-{#a#})+{#a#}" by (auto simp add: union_ac)
      hence "A=B+(C-{#a#})" by simp
      with CASES(2)[OF right] show ?thesis by blast
    qed
  qed

      (* TODO: Can this proof be done more automatically ? *)
  lemma mset_distrib[consumes 1, case_names dist]: assumes A: "(A::'a multiset)+B = M+N" "!!Am An Bm Bn. ⟦A=Am+An; B=Bm+Bn; M=Am+Bm; N=An+Bn⟧ ⟹ P" shows "P"
  proof -
    have BN_MA: "B - N = M - A"
      by (metis (no_types) add_diff_cancel_right assms(1) union_commute)
    have H: "A = A∩# C + (A - C) ∩# D" if "A + B = C + D" for A B C D :: "'a multiset"
      by (metis add.commute diff_intersect_left_idem mset_subset_eq_add_left subset_eq_diff_conv
          subset_mset.add_diff_inverse subset_mset.inf_absorb1 subset_mset.inf_le1 that)
    have A': "A = A∩# M + (A - M) ∩# N"
      using A(1) H by blast
    moreover have B': "B = (B - N) ∩# M + B∩# N"
      using A(1) H[of B A N M] by (auto simp: ac_simps)
    moreover have "M = A ∩# M + (B - N) ∩# M"
      using H[of M N A B] BN_MA[symmetric] A(1) by (metis (no_types) diff_intersect_left_idem
          diff_union_cancelR multiset_inter_commute subset_mset.diff_add subset_mset.inf.cobounded1
          union_commute)
    moreover have "N = (A - M) ∩# N + B ∩# N"
      by (metis A' assms(1) diff_union_cancelL inter_union_distrib_left inter_union_distrib_right
          mset_subset_eq_multiset_union_diff_commute subset_mset.inf.cobounded1 subset_mset.inf.commute)
    ultimately show P
      using A(2) by blast
  qed


subsubsection ‹Singleton multisets›   

lemma mset_size_le1_cases[case_names empty singleton,consumes 1]: "⟦ size M ≤ Suc 0; M={#} ⟹ P; !!m. M={#m#} ⟹ P ⟧ ⟹ P"
  by (cases M) auto

lemma diff_union_single_conv2:
  "a ∈# J ⟹ J + I - {#a#} = (J - {#a#}) + I"
  using diff_union_single_conv [of a J I]
  by (simp add: union_ac)

lemmas diff_union_single_convs = diff_union_single_conv diff_union_single_conv2

lemma mset_contains_eq: "(m ∈# M) = ({#m#}+(M-{#m#})=M)" proof (auto)
  assume "add_mset m (M - {#m#}) = M"
  moreover have "m ∈# {#m#} + (M - {#m#})" by simp
  ultimately show "m ∈# M" by simp
qed


subsubsection ‹Pointwise ordering›

  lemma mset_le_incr_right1: "(a::'a multiset)⊆#b ⟹ a⊆#b+c" using mset_subset_eq_mono_add[of a b "{#}" c, simplified] .
  lemma mset_le_incr_right2: "(a::'a multiset)⊆#b ⟹ a⊆#c+b" using mset_le_incr_right1
    by (auto simp add: union_commute)
  lemmas mset_le_incr_right = mset_le_incr_right1 mset_le_incr_right2

  lemma mset_le_decr_left1: "(a::'a multiset)+c⊆#b ⟹ a⊆#b" using mset_le_incr_right1 mset_subset_eq_mono_add_right_cancel
    by blast
  lemma mset_le_decr_left2: "c+(a::'a multiset)⊆#b ⟹ a⊆#b" using mset_le_decr_left1
    by (auto simp add: union_ac)
  lemma mset_le_add_mset_decr_left1: "add_mset c a⊆#(b::'a multiset) ⟹ a⊆#b"
    by (simp add: mset_subset_eq_insertD subset_mset.dual_order.strict_implies_order)
  lemma mset_le_add_mset_decr_left2: "add_mset c a⊆#(b::'a multiset) ⟹ {#c#}⊆#b"
    by (simp add: mset_subset_eq_insertD subset_mset.dual_order.strict_implies_order)

  lemmas mset_le_decr_left = mset_le_decr_left1 mset_le_decr_left2 mset_le_add_mset_decr_left1
    mset_le_add_mset_decr_left2
  
  lemma mset_le_subtract: "(A::'a multiset)⊆#B ⟹ A-C ⊆# B-C"
    apply (unfold subseteq_mset_def)
    apply auto
    apply (subgoal_tac "count A a ≤ count B a")
    apply arith
    apply simp
    done

  lemma mset_union_subset: "(A::'a multiset)+B ⊆# C ⟹ A⊆#C ∧ B⊆#C"
    by (auto dest: mset_le_decr_left)
 
  lemma mset_le_add_mset: "add_mset x B ⊆# C ⟹ {#x#}⊆#C ∧ B⊆#(C::'a multiset)"
    by (auto dest: mset_le_decr_left)
  
  lemma mset_le_subtract_left: "(A::'a multiset)+B ⊆# X ⟹ B ⊆# X-A ∧ A⊆#X"
    by (auto dest: mset_le_subtract[of "A+B" "X" "A"] mset_union_subset)
  lemma mset_le_subtract_right: "(A::'a multiset)+B ⊆# X ⟹ A ⊆# X-B ∧ B⊆#X"
    by (auto dest: mset_le_subtract[of "A+B" "X" "B"] mset_union_subset)

lemma mset_le_subtract_add_mset_left: "add_mset x B ⊆# (X::'a multiset) ⟹ B ⊆# X-{#x#} ∧ {#x#}⊆#X"
    by (auto dest: mset_le_subtract[of "add_mset x B" "X" "{#x#}"] mset_le_add_mset)

  lemma mset_le_subtract_add_mset_right: "add_mset x B ⊆# (X::'a multiset) ⟹ {#x#} ⊆# X-B ∧ B⊆#X"
    by (auto dest: mset_le_subtract[of "add_mset x B" "X" "B"] mset_le_add_mset)

  lemma mset_le_addE: "⟦ (xs::'a multiset) ⊆# ys; !!zs. ys=xs+zs ⟹ P ⟧ ⟹ P" using mset_subset_eq_exists_conv
    by blast

  declare subset_mset.diff_add[simp, intro]

  lemma mset_2dist2_cases:
    assumes A: "{#a, b#} ⊆# A + B"
    assumes CASES: "{#a, b#} ⊆# A ⟹ P" "{#a, b#} ⊆# B ⟹ P"
      "a ∈# A ⟹ b ∈# B ⟹ P" "a ∈# B ⟹ b ∈# A ⟹ P"
    shows "P"
  proof -
    from A have "count A a + count B a ≥ 1"
      "count A b + count B b ≥ 1"
      using mset_subset_eq_count [of "{#a, b#}" "A + B" a] mset_subset_eq_count [of "{#a, b#}" "A + B" b]
      by (auto split: if_splits)
    then have B: "a ∈# A ∨ a ∈# B"
      "b ∈# A ∨ b ∈# B"
      by (auto simp add: not_in_iff Suc_le_eq)
    { assume C: "a ∈# A" "b ∈# A - {#a#}" 
      with mset_subset_eq_mono_add [of "{#a#}" "{#a#}" "{#b#}" "A-{#a#}"]
      have "{#a, b#} ⊆# A" by (auto simp: add_mset_commute)
    } moreover {
      assume C: "a ∈# A" "b ∉# A - {#a#}"
      with B A have "b ∈# B"
        by (auto simp: insert_subset_eq_iff diff_union_single_convs
            simp del: subset_mset.add_diff_assoc2)
    } moreover {
      assume C: "a ∉# A" "b ∈# B - {#a#}"
      with A have "a ∈# B" using B by blast
      with C mset_subset_eq_mono_add [of "{#a#}" "{#a#}" "{#b#}" "B-{#a#}"]
      have "{#a, b#} ⊆# B" by (auto simp: add_mset_commute)
    } moreover {
      assume C: "a ∉# A" "b ∉# B - {#a#}"
      with A have "a ∈# B ∧ b ∈# A"
        apply (intro conjI)
         apply (auto dest!: mset_subset_eq_insertD simp: insert_union_subset_iff; fail)[]
        by (metis (no_types, lifting) B(1) add_mset_remove_trivial insert_DiffM2 
            mset_diff_cancel1elem single_subset_iff subset_eq_diff_conv subset_mset.diff_diff_right
            union_single_eq_member)
    } ultimately show P using CASES by blast
  qed

  lemma mset_union_subset_s: "{#a#}+B ⊆# C ⟹ a ∈# C ∧ B ⊆# C"
    by (drule mset_union_subset) simp
  
  lemma mset_le_single_cases[consumes 1, case_names empty singleton]: "⟦M⊆#{#a#}; M={#} ⟹ P; M={#a#} ⟹ P⟧ ⟹ P"
    by (induct M) auto
      
  lemma mset_le_distrib[consumes 1, case_names dist]: "⟦X⊆#(A::'a multiset)+B; !!Xa Xb. ⟦X=Xa+Xb; Xa⊆#A; Xb⊆#B⟧ ⟹ P ⟧ ⟹ P"
    by (auto elim!: mset_le_addE mset_distrib)

  lemma mset_le_mono_add_single: "⟦a ∈# ys; b ∈# ws⟧ ⟹ {#a, b#} ⊆# ys + ws" using mset_subset_eq_mono_add[of "{#a#}" _ "{#b#}", simplified] by (simp add: add_mset_commute)

  lemma mset_size1elem: "⟦size P ≤ 1; q ∈# P⟧ ⟹ P={#q#}"
    by (auto elim: mset_size_le1_cases)
  lemma mset_size2elem: "⟦size P ≤ 2; {#q#}+{#q'#} ⊆# P⟧ ⟹ P={#q#}+{#q'#}"
    by (auto elim: mset_le_addE)


subsubsection ‹Image under function›

notation image_mset (infixr "`#" 90)

lemma mset_map_single_rightE[consumes 1, case_names orig]: "⟦f `# P = {#y#}; !!x. ⟦ P={#x#}; f x = y ⟧ ⟹ Q ⟧ ⟹ Q"
  by (cases P) auto

lemma mset_map_split_orig: "!!M1 M2. ⟦f `# P = M1+M2; !!P1 P2. ⟦P=P1+P2; f `# P1 = M1; f `# P2 = M2⟧ ⟹ Q ⟧ ⟹ Q"
  apply (induct P)
  apply fastforce
  apply (force elim!: mset_un_single_un_cases simp add: union_ac) (* TODO: This proof need's quite long. Try to write a faster one. *)
  done

lemma mset_map_id: "⟦!!x. f (g x) = x⟧ ⟹ f `# g `# X = X"
  by (induct X) auto

text ‹The following is a very specialized lemma. Intuitively, it splits the original multiset›
text ‹The following is a very specialized   by a splitting of some pointwise supermultiset of its image.

  Application:
  This lemma came in handy when proving the correctness of a constraint system that collects at most k sized submultisets of the sets of spawned threads.
›
lemma mset_map_split_orig_le: assumes A: "f `# P ⊆# M1+M2" and EX: "!!P1 P2. ⟦P=P1+P2; f `# P1 ⊆# M1; f `# P2 ⊆# M2⟧ ⟹ Q" shows "Q"
  using A EX by (auto elim: mset_le_distrib mset_map_split_orig)


subsection ‹Lists›

subsubsection ‹Reverse lists›
  lemma list_rev_decomp[rule_format]: "l~=[] ⟶ (EX ll e . l = ll@[e])"
    apply(induct_tac l)
    apply(auto)
  done
    
  (* Was already there as rev_induct
  lemma list_rev_induct: "⟦P []; !! l e . P l ⟹ P (l@[e]) ⟧ ⟹ P l"
    by (blast intro: rev_induct)
  proof (induct l rule: measure_induct[of length])
    fix x :: "'a list"
    assume A: "∀y. length y < length x ⟶ P [] ⟶ (∀x xa. P (x::'a list) ⟶ P (x @ [xa])) ⟶ P y" "P []" and IS: "⋀l e. P l ⟹ P (l @ [e])"
    show "P x" proof (cases "x=[]")
      assume "x=[]" with A show ?thesis by simp
    next
      assume CASE: "x~=[]"
      then obtain xx e where DECOMP: "x=xx@[e]" by (blast dest: list_rev_decomp)
      hence LEN: "length xx < length x" by auto
      with A IS have "P xx" by auto
      with IS have "P (xx@[e])" by auto
      with DECOMP show ?thesis by auto
    qed
  qed
  *)

  text ‹Caution: Same order of case variables in snoc-case as @{thm [source] rev_exhaust}, the other way round than @{thm [source] rev_induct} !›
  lemma length_compl_rev_induct[case_names Nil snoc]: "⟦P []; !! l e . ⟦!! ll . length ll <= length l ⟹ P ll⟧ ⟹ P (l@[e])⟧ ⟹ P l"
    apply(induct_tac l rule: length_induct)
    apply(case_tac "xs" rule: rev_cases)
    apply(auto)
  done

  lemma list_append_eq_Cons_cases: "⟦ys@zs = x#xs; ⟦ys=[]; zs=x#xs⟧ ⟹ P; !!ys'. ⟦ ys=x#ys'; ys'@zs=xs ⟧ ⟹ P ⟧ ⟹ P"
    by (auto iff add: append_eq_Cons_conv)
  lemma list_Cons_eq_append_cases: "⟦x#xs = ys@zs; ⟦ys=[]; zs=x#xs⟧ ⟹ P; !!ys'. ⟦ ys=x#ys'; ys'@zs=xs ⟧ ⟹ P ⟧ ⟹ P"
    by (auto iff add: Cons_eq_append_conv)

subsubsection "folding"

text "Ugly lemma about foldl over associative operator with left and right neutral element"
lemma foldl_A1_eq: "!!i. ⟦ !! e. f n e = e; !! e. f e n = e; !!a b c. f a (f b c) = f (f a b) c ⟧ ⟹ foldl f i ww = f i (foldl f n ww)"
proof (induct ww)
  case Nil thus ?case by simp
next
  case (Cons a ww i) note IHP[simplified]=this
  have "foldl f i (a # ww) = foldl f (f i a) ww" by simp
  also from IHP have "… = f (f i a) (foldl f n ww)" by blast
  also from IHP(4) have "… = f i (f a (foldl f n ww))" by simp
  also from IHP(1)[OF IHP(2,3,4), where i=a] have "… = f i (foldl f a ww)" by simp
  also from IHP(2)[of a] have "… = f i (foldl f (f n a) ww)" by simp
  also have "… = f i (foldl f n (a#ww))" by simp
  finally show ?case .
qed

lemmas foldl_conc_empty_eq = foldl_A1_eq[of "(@)" "[]", simplified]
lemmas foldl_un_empty_eq = foldl_A1_eq[of "(∪)" "{}", simplified, OF Un_assoc[symmetric]]

lemma foldl_set: "foldl (∪) {} l = ⋃{x. x∈set l}"
  apply (induct l)
  apply simp_all
  apply (subst foldl_un_empty_eq)
  apply auto
  done


subsubsection ‹Miscellaneous›
  lemma length_compl_induct[case_names Nil Cons]: "⟦P []; !! e l . ⟦!! ll . length ll <= length l ⟹ P ll⟧ ⟹ P (e#l)⟧ ⟹ P l"
    apply(induct_tac l rule: length_induct)
    apply(case_tac "xs")
    apply(auto)
  done


  text ‹Simultaneous induction over two lists, prepending an element to one of the lists in each step›
  lemma list_2pre_induct[case_names base left right]: assumes BASE: "P [] []" and LEFT: "!!e w1' w2. P w1' w2 ⟹ P (e#w1') w2" and RIGHT: "!!e w1 w2'. P w1 w2' ⟹ P w1 (e#w2')" shows "P w1 w2" 
  proof -
    { ― ‹The proof is done by induction over the sum of the lengths of the lists›
      fix n
      have "!!w1 w2. ⟦length w1 + length w2 = n; P [] []; !!e w1' w2. P w1' w2 ⟹ P (e#w1') w2; !!e w1 w2'. P w1 w2' ⟹ P w1 (e#w2') ⟧ ⟹ P w1 w2 " 
        apply (induct n)
        apply simp
        apply (case_tac w1)
        apply auto
        apply (case_tac w2)
        apply auto
        done
    } from this[OF _ BASE LEFT RIGHT] show ?thesis by blast
  qed


  lemma list_decomp_1: "length l=1 ⟹ EX a . l=[a]"
    by (case_tac l, auto)

  lemma list_decomp_2: "length l=2 ⟹ EX a b . l=[a,b]"
    by (case_tac l, auto simp add: list_decomp_1)


  lemma drop_all_conc: "drop (length a) (a@b) = b"
    by (simp)

  lemma list_rest_coinc: "⟦length s2 <= length s1; s1@r1 = s2@r2⟧ ⟹ EX r1p . r2=r1p@r1"
  proof -
    assume A: "length s2 <= length s1" "s1@r1 = s2@r2"
    hence "r1 = drop (length s1) (s2@r2)" by (auto simp only:drop_all_conc dest: sym)
    moreover from A have "length s1 = length s1 - length s2 + length s2" by arith
    ultimately have "r1 = drop ((length s1 - length s2)) r2" by (auto)
    hence "r2 = take ((length s1 - length s2)) r2 @ r1" by auto
    thus ?thesis by auto
  qed

  lemma list_tail_coinc: "n1#r1 = n2#r2 ⟹ n1=n2 & r1=r2"
    by (auto)


  lemma last_in_set[intro]: "⟦l≠[]⟧ ⟹ last l ∈ set l"
    by (induct l) auto

subsection ‹Induction on nat›
  lemma nat_compl_induct[case_names 0 Suc]: "⟦P 0; !! n . ALL nn . nn <= n ⟶ P nn ⟹ P (Suc n)⟧ ⟹ P n"
    apply(induct_tac n rule: nat_less_induct)
    apply(case_tac n)
    apply(auto)
  done


subsection ‹Functions of type @{typ "bool⇒bool"}›
  lemma boolfun_cases_helper: "g=(λx. False) | g=(λx. x) | g=(λx. True) | g= (λx. ¬x)" 
  proof -
    { assume "g False" "g True"
      hence "g = (λx. True)" by (rule_tac ext, case_tac x, auto)
    } moreover {
      assume "g False" "¬g True"
      hence "g = (λx. ¬x)" by (rule_tac ext, case_tac x, auto)
    } moreover {
      assume "¬g False" "g True"
      hence "g = (λx. x)" by (rule_tac ext, case_tac x, auto)
    } moreover {
      assume "¬g False" "¬g True"
      hence "g = (λx. False)" by (rule_tac ext, case_tac x, auto)
    } ultimately show ?thesis by fast
  qed

  lemma boolfun_cases[case_names False Id True Neg]: "⟦g=(λx. False) ⟹ P g; g=(λx. x) ⟹ P g; g=(λx. True) ⟹ P g; g=(λx. ¬x) ⟹ P g⟧ ⟹ P g"
  proof -
    note boolfun_cases_helper[of g]
    moreover assume "g=(λx. False) ⟹ P g" "g=(λx. x) ⟹ P g" "g=(λx. True) ⟹ P g" "g=(λx. ¬x) ⟹ P g"
    ultimately show ?thesis by fast
  qed


  subsection ‹Definite and indefinite description›
  text "Combined definite and indefinite description for binary predicate"
  lemma some_theI: assumes EX: "∃a b . P a b" and BUN: "!! b1 b2 . ⟦∃a . P a b1; ∃a . P a b2⟧ ⟹ b1=b2" 
    shows "P (SOME a . ∃b . P a b) (THE b . ∃a . P a b)"
  proof -
    from EX have "EX b . P (SOME a . EX b . P a b) b" by (rule someI_ex)
    moreover from EX have "EX b . EX a . P a b" by blast
    with BUN theI'[of "λb . EX a . P a b"] have "EX a . P a (THE b . EX a . P a b)" by (unfold Ex1_def, blast)
    moreover note BUN
    ultimately show ?thesis by (fast)
  qed
  


end