src/ZF/UNITY/MultisetSum.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 46823 57bf0cecb366
child 58871 c399ae4b836f
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37936
1e4c5015a72e updated some headers;
wenzelm
parents: 32960
diff changeset
     1
(*  Title:      ZF/UNITY/MultisetSum.thy
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     2
    Author:     Sidi O Ehmety
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     3
*)
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     4
15202
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
     5
header {*Setsum for Multisets*}
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
     6
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
     7
theory MultisetSum
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
     8
imports "../Induct/Multiset"
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
     9
begin
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    10
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 15202
diff changeset
    11
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 15202
diff changeset
    12
  lcomm :: "[i, i, [i,i]=>i]=>o"  where
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    13
  "lcomm(A, B, f) ==
15202
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    14
   (\<forall>x \<in> A. \<forall>y \<in> A. \<forall>z \<in> B. f(x, f(y, z))= f(y, f(x, z)))  &
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    15
   (\<forall>x \<in> A. \<forall>y \<in> B. f(x, y) \<in> B)"
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    16
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 15202
diff changeset
    17
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 15202
diff changeset
    18
  general_setsum :: "[i,i,i, [i,i]=>i, i=>i] =>i"  where
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    19
   "general_setsum(C, B, e, f, g) ==
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    20
    if Finite(C) then fold[cons(e, B)](%x y. f(g(x), y), e, C) else e"
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    21
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 15202
diff changeset
    22
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 15202
diff changeset
    23
  msetsum :: "[i=>i, i, i]=>i"  where
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    24
  "msetsum(g, C, B) == normalize(general_setsum(C, Mult(B), 0, op +#, g))"
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    25
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 15202
diff changeset
    26
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 15202
diff changeset
    27
definition  (* sum for naturals *)
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 15202
diff changeset
    28
  nsetsum :: "[i=>i, i] =>i"  where
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    29
  "nsetsum(g, C) == general_setsum(C, nat, 0, op #+, g)"
15202
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    30
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    31
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    32
lemma mset_of_normalize: "mset_of(normalize(M)) \<subseteq> mset_of(M)"
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    33
by (auto simp add: mset_of_def normalize_def)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    34
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    35
lemma general_setsum_0 [simp]: "general_setsum(0, B, e, f, g) = e"
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    36
by (simp add: general_setsum_def)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    37
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    38
lemma general_setsum_cons [simp]: 
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    39
"[| C \<in> Fin(A); a \<in> A; a\<notin>C; e \<in> B; \<forall>x \<in> A. g(x) \<in> B; lcomm(B, B, f) |] ==>  
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    40
  general_setsum(cons(a, C), B, e, f, g) =  
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    41
    f(g(a), general_setsum(C, B, e, f,g))"
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    42
apply (simp add: general_setsum_def)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    43
apply  (auto simp add: Fin_into_Finite [THEN Finite_cons] cons_absorb)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    44
prefer 2 apply (blast dest: Fin_into_Finite)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    45
apply (rule fold_typing.fold_cons)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    46
apply (auto simp add: fold_typing_def lcomm_def)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    47
done
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    48
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    49
(** lcomm **)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    50
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    51
lemma lcomm_mono: "[| C\<subseteq>A; lcomm(A, B, f) |] ==> lcomm(C, B,f)"
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    52
by (auto simp add: lcomm_def, blast)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    53
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    54
lemma munion_lcomm [simp]: "lcomm(Mult(A), Mult(A), op +#)"
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    55
by (auto simp add: lcomm_def Mult_iff_multiset munion_lcommute)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    56
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    57
(** msetsum **)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    58
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    59
lemma multiset_general_setsum: 
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    60
     "[| C \<in> Fin(A); \<forall>x \<in> A. multiset(g(x))& mset_of(g(x))\<subseteq>B  |]   
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    61
      ==> multiset(general_setsum(C, B -||> nat - {0}, 0, \<lambda>u v. u +# v, g))"
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    62
apply (erule Fin_induct, auto)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    63
apply (subst general_setsum_cons)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    64
apply (auto simp add: Mult_iff_multiset)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    65
done
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    66
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    67
lemma msetsum_0 [simp]: "msetsum(g, 0, B) = 0"
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    68
by (simp add: msetsum_def)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    69
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    70
lemma msetsum_cons [simp]: 
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    71
  "[| C \<in> Fin(A); a\<notin>C; a \<in> A; \<forall>x \<in> A. multiset(g(x)) & mset_of(g(x))\<subseteq>B  |]   
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    72
   ==> msetsum(g, cons(a, C), B) = g(a) +#  msetsum(g, C, B)"
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    73
apply (simp add: msetsum_def)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    74
apply (subst general_setsum_cons)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    75
apply (auto simp add: multiset_general_setsum Mult_iff_multiset)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    76
done
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    77
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    78
(* msetsum type *)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    79
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    80
lemma msetsum_multiset: "multiset(msetsum(g, C, B))"
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    81
by (simp add: msetsum_def)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    82
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    83
lemma mset_of_msetsum: 
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    84
     "[| C \<in> Fin(A); \<forall>x \<in> A. multiset(g(x)) & mset_of(g(x))\<subseteq>B |]   
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    85
      ==> mset_of(msetsum(g, C, B))\<subseteq>B"
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    86
by (erule Fin_induct, auto)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    87
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    88
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    89
(*The reversed orientation looks more natural, but LOOPS as a simprule!*)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    90
lemma msetsum_Un_Int: 
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    91
     "[| C \<in> Fin(A); D \<in> Fin(A); \<forall>x \<in> A. multiset(g(x)) & mset_of(g(x))\<subseteq>B |]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 37936
diff changeset
    92
      ==> msetsum(g, C \<union> D, B) +# msetsum(g, C \<inter> D, B)  
15202
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    93
        = msetsum(g, C, B) +# msetsum(g, D, B)"
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    94
apply (erule Fin_induct)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 37936
diff changeset
    95
apply (subgoal_tac [2] "cons (x, y) \<union> D = cons (x, y \<union> D) ")
15202
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    96
apply (auto simp add: msetsum_multiset)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 37936
diff changeset
    97
apply (subgoal_tac "y \<union> D \<in> Fin (A) & y \<inter> D \<in> Fin (A) ")
15202
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    98
apply clarify
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
    99
apply (case_tac "x \<in> D")
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 37936
diff changeset
   100
apply (subgoal_tac [2] "cons (x, y) \<inter> D = y \<inter> D")
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 37936
diff changeset
   101
apply (subgoal_tac "cons (x, y) \<inter> D = cons (x, y \<inter> D) ")
15202
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   102
apply (simp_all (no_asm_simp) add: cons_absorb munion_assoc msetsum_multiset)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   103
apply (simp (no_asm_simp) add: munion_lcommute msetsum_multiset)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   104
apply auto
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   105
done
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   106
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   107
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   108
lemma msetsum_Un_disjoint:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 37936
diff changeset
   109
     "[| C \<in> Fin(A); D \<in> Fin(A); C \<inter> D = 0;  
15202
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   110
         \<forall>x \<in> A. multiset(g(x)) & mset_of(g(x))\<subseteq>B |]  
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 37936
diff changeset
   111
      ==> msetsum(g, C \<union> D, B) = msetsum(g, C, B) +# msetsum(g,D, B)"
15202
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   112
apply (subst msetsum_Un_Int [symmetric])
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   113
apply (auto simp add: msetsum_multiset)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   114
done
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   115
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   116
lemma UN_Fin_lemma [rule_format (no_asm)]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 37936
diff changeset
   117
     "I \<in> Fin(A) ==> (\<forall>i \<in> I. C(i) \<in> Fin(B)) \<longrightarrow> (\<Union>i \<in> I. C(i)):Fin(B)"
15202
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   118
by (erule Fin_induct, auto)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   119
 
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   120
lemma msetsum_UN_disjoint [rule_format (no_asm)]:
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   121
     "[| I \<in> Fin(K); \<forall>i \<in> K. C(i) \<in> Fin(A) |] ==>  
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 37936
diff changeset
   122
      (\<forall>x \<in> A. multiset(f(x)) & mset_of(f(x))\<subseteq>B) \<longrightarrow>   
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 37936
diff changeset
   123
      (\<forall>i \<in> I. \<forall>j \<in> I. i\<noteq>j \<longrightarrow> C(i) \<inter> C(j) = 0) \<longrightarrow>  
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24893
diff changeset
   124
        msetsum(f, \<Union>i \<in> I. C(i), B) = msetsum (%i. msetsum(f, C(i),B), I, B)"
15202
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   125
apply (erule Fin_induct, auto)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   126
apply (subgoal_tac "\<forall>i \<in> y. x \<noteq> i")
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   127
 prefer 2 apply blast
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 37936
diff changeset
   128
apply (subgoal_tac "C(x) \<inter> (\<Union>i \<in> y. C (i)) = 0")
15202
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   129
 prefer 2 apply blast
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   130
apply (subgoal_tac " (\<Union>i \<in> y. C (i)):Fin (A) & C(x) :Fin (A) ")
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   131
prefer 2 apply (blast intro: UN_Fin_lemma dest: FinD, clarify)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   132
apply (simp (no_asm_simp) add: msetsum_Un_disjoint)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   133
apply (subgoal_tac "\<forall>x \<in> K. multiset (msetsum (f, C(x), B)) & mset_of (msetsum (f, C(x), B)) \<subseteq> B")
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   134
apply (simp (no_asm_simp))
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   135
apply clarify
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   136
apply (drule_tac x = xa in bspec)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   137
apply (simp_all (no_asm_simp) add: msetsum_multiset mset_of_msetsum)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   138
done
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   139
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   140
lemma msetsum_addf: 
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   141
    "[| C \<in> Fin(A);  
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   142
      \<forall>x \<in> A. multiset(f(x)) & mset_of(f(x))\<subseteq>B;  
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   143
      \<forall>x \<in> A. multiset(g(x)) & mset_of(g(x))\<subseteq>B |] ==> 
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   144
      msetsum(%x. f(x) +# g(x), C, B) = msetsum(f, C, B) +# msetsum(g, C, B)"
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   145
apply (subgoal_tac "\<forall>x \<in> A. multiset (f(x) +# g(x)) & mset_of (f(x) +# g(x)) \<subseteq> B")
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   146
apply (erule Fin_induct)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   147
apply (auto simp add: munion_ac) 
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   148
done
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   149
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   150
lemma msetsum_cong: 
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   151
    "[| C=D; !!x. x \<in> D ==> f(x) = g(x) |]
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   152
     ==> msetsum(f, C, B) = msetsum(g, D, B)"
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   153
by (simp add: msetsum_def general_setsum_def cong add: fold_cong)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   154
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   155
lemma multiset_union_diff: "[| multiset(M); multiset(N) |] ==> M +# N -# N = M"
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   156
by (simp add: multiset_equality)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   157
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   158
lemma msetsum_Un: "[| C \<in> Fin(A); D \<in> Fin(A);  
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   159
  \<forall>x \<in> A. multiset(f(x)) & mset_of(f(x)) \<subseteq> B  |]  
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 37936
diff changeset
   160
   ==> msetsum(f, C \<union> D, B) =  
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 37936
diff changeset
   161
          msetsum(f, C, B) +# msetsum(f, D, B) -# msetsum(f, C \<inter> D, B)"
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 37936
diff changeset
   162
apply (subgoal_tac "C \<union> D \<in> Fin (A) & C \<inter> D \<in> Fin (A) ")
15202
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   163
apply clarify
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   164
apply (subst msetsum_Un_Int [symmetric])
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   165
apply (simp_all (no_asm_simp) add: msetsum_multiset multiset_union_diff)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   166
apply (blast dest: FinD)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   167
done
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   168
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   169
lemma nsetsum_0 [simp]: "nsetsum(g, 0)=0"
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   170
by (simp add: nsetsum_def)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   171
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   172
lemma nsetsum_cons [simp]: 
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   173
     "[| Finite(C); x\<notin>C |] ==> nsetsum(g, cons(x, C))= g(x) #+ nsetsum(g, C)"
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   174
apply (simp add: nsetsum_def general_setsum_def)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   175
apply (rule_tac A = "cons (x, C)" in fold_typing.fold_cons)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   176
apply (auto intro: Finite_cons_lemma simp add: fold_typing_def)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   177
done
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   178
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   179
lemma nsetsum_type [simp,TC]: "nsetsum(g, C) \<in> nat"
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   180
apply (case_tac "Finite (C) ")
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   181
 prefer 2 apply (simp add: nsetsum_def general_setsum_def)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   182
apply (erule Finite_induct, auto)
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   183
done
d14a6e421a65 converting UNITY/MultisetSum.ML to Isar script
paulson
parents: 14052
diff changeset
   184
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
   185
end