src/ZF/Induct/Multiset.thy
author wenzelm
Mon, 24 Apr 2017 23:10:01 +0200
changeset 65576 8376f83f9094
parent 63040 eb4ddd18d635
child 69587 53982d5ec0bb
permissions -rw-r--r--
recovered document from 0f3fdf689bf9;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12089
diff changeset
     1
(*  Title:      ZF/Induct/Multiset.thy
12089
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
     2
    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
     3
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
     4
A definitional theory of multisets,
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
     5
including a wellfoundedness proof for the multiset order.
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
     6
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
     7
The theory features ordinal multisets and the usual ordering.
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
     8
*)
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
     9
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
    10
theory Multiset
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
    11
imports FoldSet Acc
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
    12
begin
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
    13
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 20898
diff changeset
    14
abbreviation (input)
61798
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 61393
diff changeset
    15
  \<comment> \<open>Short cut for multiset space\<close>
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 20898
diff changeset
    16
  Mult :: "i=>i" where
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 20898
diff changeset
    17
  "Mult(A) == A -||> nat-{0}"
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
    18
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    19
definition
12891
92af5c3a10fb a new definition of "restrict"
paulson
parents: 12860
diff changeset
    20
  (* This is the original "restrict" from ZF.thy.
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
    21
     Restricts the function f to the domain A
12891
92af5c3a10fb a new definition of "restrict"
paulson
parents: 12860
diff changeset
    22
     FIXME: adapt Multiset to the new "restrict". *)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    23
  funrestrict :: "[i,i] => i"  where
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
    24
  "funrestrict(f,A) == \<lambda>x \<in> A. f`x"
12891
92af5c3a10fb a new definition of "restrict"
paulson
parents: 12860
diff changeset
    25
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    26
definition
12089
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
    27
  (* M is a multiset *)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    28
  multiset :: "i => o"  where
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
    29
  "multiset(M) == \<exists>A. M \<in> A -> nat-{0} & Finite(A)"
12089
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
    30
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    31
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    32
  mset_of :: "i=>i"  where
12089
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
    33
  "mset_of(M) == domain(M)"
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
    34
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    35
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    36
  munion    :: "[i, i] => i" (infixl "+#" 65)  where
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
    37
  "M +# N == \<lambda>x \<in> mset_of(M) \<union> mset_of(N).
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
    38
     if x \<in> mset_of(M) \<inter> mset_of(N) then  (M`x) #+ (N`x)
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
    39
     else (if x \<in> mset_of(M) then M`x else N`x)"
12089
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
    40
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    41
definition
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12891
diff changeset
    42
  (*convert a function to a multiset by eliminating 0*)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    43
  normalize :: "i => i"  where
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12891
diff changeset
    44
  "normalize(f) ==
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
    45
       if (\<exists>A. f \<in> A -> nat & Finite(A)) then
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
    46
            funrestrict(f, {x \<in> mset_of(f). 0 < f`x})
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12891
diff changeset
    47
       else 0"
12089
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
    48
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    49
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    50
  mdiff  :: "[i, i] => i" (infixl "-#" 65)  where
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
    51
  "M -# N ==  normalize(\<lambda>x \<in> mset_of(M).
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26417
diff changeset
    52
                        if x \<in> mset_of(N) then M`x #- N`x else M`x)"
12089
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
    53
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    54
definition
12089
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
    55
  (* set of elements of a multiset *)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    56
  msingle :: "i => i"    ("{#_#}")  where
12089
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
    57
  "{#a#} == {<a, 1>}"
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
    58
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    59
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    60
  MCollect :: "[i, i=>o] => i"  (*comprehension*)  where
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
    61
  "MCollect(M, P) == funrestrict(M, {x \<in> mset_of(M). P(x)})"
12089
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
    62
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    63
definition
58318
f95754ca7082 fixed some spelling mistakes
blanchet
parents: 57492
diff changeset
    64
  (* Counts the number of occurrences of an element in a multiset *)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    65
  mcount :: "[i, i] => i"  where
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
    66
  "mcount(M, a) == if a \<in> mset_of(M) then  M`a else 0"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
    67
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    68
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    69
  msize :: "i => i"  where
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
    70
  "msize(M) == setsum(%a. $# mcount(M,a), mset_of(M))"
12089
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
    71
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 20898
diff changeset
    72
abbreviation
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 20898
diff changeset
    73
  melem :: "[i,i] => o"    ("(_/ :# _)" [50, 51] 50)  where
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 20898
diff changeset
    74
  "a :# M == a \<in> mset_of(M)"
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 20898
diff changeset
    75
12089
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
    76
syntax
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
    77
  "_MColl" :: "[pttrn, i, o] => i" ("(1{# _ \<in> _./ _#})")
12089
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
    78
translations
61393
8673ec68c798 tuned syntax -- more symbols;
wenzelm
parents: 60770
diff changeset
    79
  "{#x \<in> M. P#}" == "CONST MCollect(M, \<lambda>x. P)"
12089
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
    80
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
    81
  (* multiset orderings *)
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
    82
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    83
definition
12089
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
    84
   (* multirel1 has to be a set (not a predicate) so that we can form
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
    85
      its transitive closure and reason about wf(.) and acc(.) *)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    86
  multirel1 :: "[i,i]=>i"  where
12089
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
    87
  "multirel1(A, r) ==
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
    88
     {<M, N> \<in> Mult(A)*Mult(A).
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
    89
      \<exists>a \<in> A. \<exists>M0 \<in> Mult(A). \<exists>K \<in> Mult(A).
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
    90
      N=M0 +# {#a#} & M=M0 +# K & (\<forall>b \<in> mset_of(K). <b,a> \<in> r)}"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
    91
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    92
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    93
  multirel :: "[i, i] => i"  where
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46822
diff changeset
    94
  "multirel(A, r) == multirel1(A, r)^+"
12089
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
    95
12860
7fc3fbfed8ef Multiset: added the translation Mult(A) => A-||>nat-{0}
paulson
parents: 12610
diff changeset
    96
  (* ordinal multiset orderings *)
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
    97
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    98
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    99
  omultiset :: "i => o"  where
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   100
  "omultiset(M) == \<exists>i. Ord(i) & M \<in> Mult(field(Memrel(i)))"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   101
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
   102
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
   103
  mless :: "[i, i] => o" (infixl "<#" 50)  where
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   104
  "M <# N ==  \<exists>i. Ord(i) & <M, N> \<in> multirel(field(Memrel(i)), Memrel(i))"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   105
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
   106
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
   107
  mle  :: "[i, i] => o"  (infixl "<#=" 50)  where
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   108
  "M <#= N == (omultiset(M) & M = N) | M <# N"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   109
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   110
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59788
diff changeset
   111
subsection\<open>Properties of the original "restrict" from ZF.thy\<close>
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   112
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   113
lemma funrestrict_subset: "[| f \<in> Pi(C,B);  A\<subseteq>C |] ==> funrestrict(f,A) \<subseteq> f"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   114
by (auto simp add: funrestrict_def lam_def intro: apply_Pair)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   115
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   116
lemma funrestrict_type:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   117
    "[| !!x. x \<in> A ==> f`x \<in> B(x) |] ==> funrestrict(f,A) \<in> Pi(A,B)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   118
by (simp add: funrestrict_def lam_type)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   119
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   120
lemma funrestrict_type2: "[| f \<in> Pi(C,B);  A\<subseteq>C |] ==> funrestrict(f,A) \<in> Pi(A,B)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   121
by (blast intro: apply_type funrestrict_type)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   122
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   123
lemma funrestrict [simp]: "a \<in> A ==> funrestrict(f,A) ` a = f`a"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   124
by (simp add: funrestrict_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   125
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   126
lemma funrestrict_empty [simp]: "funrestrict(f,0) = 0"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   127
by (simp add: funrestrict_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   128
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   129
lemma domain_funrestrict [simp]: "domain(funrestrict(f,C)) = C"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   130
by (auto simp add: funrestrict_def lam_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   131
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   132
lemma fun_cons_funrestrict_eq:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   133
     "f \<in> cons(a, b) -> B ==> f = cons(<a, f ` a>, funrestrict(f, b))"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   134
apply (rule equalityI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   135
prefer 2 apply (blast intro: apply_Pair funrestrict_subset [THEN subsetD])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   136
apply (auto dest!: Pi_memberD simp add: funrestrict_def lam_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   137
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   138
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   139
declare domain_of_fun [simp]
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   140
declare domainE [rule del]
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   141
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   142
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59788
diff changeset
   143
text\<open>A useful simplification rule\<close>
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   144
lemma multiset_fun_iff:
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   145
     "(f \<in> A -> nat-{0}) \<longleftrightarrow> f \<in> A->nat&(\<forall>a \<in> A. f`a \<in> nat & 0 < f`a)"
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   146
apply safe
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   147
apply (rule_tac [4] B1 = "range (f) " in Pi_mono [THEN subsetD])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   148
apply (auto intro!: Ord_0_lt
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   149
            dest: apply_type Diff_subset [THEN Pi_mono, THEN subsetD]
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   150
            simp add: range_of_fun apply_iff)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   151
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   152
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   153
(** The multiset space  **)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   154
lemma multiset_into_Mult: "[| multiset(M); mset_of(M)\<subseteq>A |] ==> M \<in> Mult(A)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   155
apply (simp add: multiset_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   156
apply (auto simp add: multiset_fun_iff mset_of_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   157
apply (rule_tac B1 = "nat-{0}" in FiniteFun_mono [THEN subsetD], simp_all)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   158
apply (rule Finite_into_Fin [THEN [2] Fin_mono [THEN subsetD], THEN fun_FiniteFunI])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   159
apply (simp_all (no_asm_simp) add: multiset_fun_iff)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   160
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   161
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   162
lemma Mult_into_multiset: "M \<in> Mult(A) ==> multiset(M) & mset_of(M)\<subseteq>A"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   163
apply (simp add: multiset_def mset_of_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   164
apply (frule FiniteFun_is_fun)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   165
apply (drule FiniteFun_domain_Fin)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   166
apply (frule FinD, clarify)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   167
apply (rule_tac x = "domain (M) " in exI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   168
apply (blast intro: Fin_into_Finite)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   169
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   170
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   171
lemma Mult_iff_multiset: "M \<in> Mult(A) \<longleftrightarrow> multiset(M) & mset_of(M)\<subseteq>A"
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   172
by (blast dest: Mult_into_multiset intro: multiset_into_Mult)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   173
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   174
lemma multiset_iff_Mult_mset_of: "multiset(M) \<longleftrightarrow> M \<in> Mult(mset_of(M))"
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   175
by (auto simp add: Mult_iff_multiset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   176
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   177
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59788
diff changeset
   178
text\<open>The @{term multiset} operator\<close>
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   179
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   180
(* the empty multiset is 0 *)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   181
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   182
lemma multiset_0 [simp]: "multiset(0)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   183
by (auto intro: FiniteFun.intros simp add: multiset_iff_Mult_mset_of)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   184
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   185
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59788
diff changeset
   186
text\<open>The @{term mset_of} operator\<close>
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   187
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   188
lemma multiset_set_of_Finite [simp]: "multiset(M) ==> Finite(mset_of(M))"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   189
by (simp add: multiset_def mset_of_def, auto)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   190
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   191
lemma mset_of_0 [iff]: "mset_of(0) = 0"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   192
by (simp add: mset_of_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   193
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   194
lemma mset_is_0_iff: "multiset(M) ==> mset_of(M)=0 \<longleftrightarrow> M=0"
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   195
by (auto simp add: multiset_def mset_of_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   196
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   197
lemma mset_of_single [iff]: "mset_of({#a#}) = {a}"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   198
by (simp add: msingle_def mset_of_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   199
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   200
lemma mset_of_union [iff]: "mset_of(M +# N) = mset_of(M) \<union> mset_of(N)"
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   201
by (simp add: mset_of_def munion_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   202
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   203
lemma mset_of_diff [simp]: "mset_of(M)\<subseteq>A ==> mset_of(M -# N) \<subseteq> A"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   204
by (auto simp add: mdiff_def multiset_def normalize_def mset_of_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   205
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   206
(* msingle *)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   207
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   208
lemma msingle_not_0 [iff]: "{#a#} \<noteq> 0 & 0 \<noteq> {#a#}"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   209
by (simp add: msingle_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   210
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   211
lemma msingle_eq_iff [iff]: "({#a#} = {#b#}) \<longleftrightarrow>  (a = b)"
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   212
by (simp add: msingle_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   213
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   214
lemma msingle_multiset [iff,TC]: "multiset({#a#})"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   215
apply (simp add: multiset_def msingle_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   216
apply (rule_tac x = "{a}" in exI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   217
apply (auto intro: Finite_cons Finite_0 fun_extend3)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   218
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   219
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   220
(** normalize **)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   221
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 35112
diff changeset
   222
lemmas Collect_Finite = Collect_subset [THEN subset_Finite]
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   223
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   224
lemma normalize_idem [simp]: "normalize(normalize(f)) = normalize(f)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   225
apply (simp add: normalize_def funrestrict_def mset_of_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   226
apply (case_tac "\<exists>A. f \<in> A -> nat & Finite (A) ")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   227
apply clarify
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   228
apply (drule_tac x = "{x \<in> domain (f) . 0 < f ` x}" in spec)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   229
apply auto
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   230
apply (auto  intro!: lam_type simp add: Collect_Finite)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   231
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   232
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   233
lemma normalize_multiset [simp]: "multiset(M) ==> normalize(M) = M"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   234
by (auto simp add: multiset_def normalize_def mset_of_def funrestrict_def multiset_fun_iff)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   235
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   236
lemma multiset_normalize [simp]: "multiset(normalize(f))"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   237
apply (simp add: normalize_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   238
apply (simp add: normalize_def mset_of_def multiset_def, auto)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   239
apply (rule_tac x = "{x \<in> A . 0<f`x}" in exI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   240
apply (auto intro: Collect_subset [THEN subset_Finite] funrestrict_type)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   241
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   242
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   243
(** Typechecking rules for union and difference of multisets **)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   244
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   245
(* union *)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   246
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   247
lemma munion_multiset [simp]: "[| multiset(M); multiset(N) |] ==> multiset(M +# N)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   248
apply (unfold multiset_def munion_def mset_of_def, auto)
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   249
apply (rule_tac x = "A \<union> Aa" in exI)
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   250
apply (auto intro!: lam_type intro: Finite_Un simp add: multiset_fun_iff zero_less_add)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   251
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   252
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   253
(* difference *)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   254
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   255
lemma mdiff_multiset [simp]: "multiset(M -# N)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   256
by (simp add: mdiff_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   257
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   258
(** Algebraic properties of multisets **)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   259
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   260
(* Union *)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   261
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   262
lemma munion_0 [simp]: "multiset(M) ==> M +# 0 = M & 0 +# M = M"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   263
apply (simp add: multiset_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   264
apply (auto simp add: munion_def mset_of_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   265
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   266
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   267
lemma munion_commute: "M +# N = N +# M"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   268
by (auto intro!: lam_cong simp add: munion_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   269
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   270
lemma munion_assoc: "(M +# N) +# K = M +# (N +# K)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   271
apply (unfold munion_def mset_of_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   272
apply (rule lam_cong, auto)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   273
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   274
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   275
lemma munion_lcommute: "M +# (N +# K) = N +# (M +# K)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   276
apply (unfold munion_def mset_of_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   277
apply (rule lam_cong, auto)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   278
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   279
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   280
lemmas munion_ac = munion_commute munion_assoc munion_lcommute
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   281
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   282
(* Difference *)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   283
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   284
lemma mdiff_self_eq_0 [simp]: "M -# M = 0"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   285
by (simp add: mdiff_def normalize_def mset_of_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   286
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   287
lemma mdiff_0 [simp]: "0 -# M = 0"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   288
by (simp add: mdiff_def normalize_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   289
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   290
lemma mdiff_0_right [simp]: "multiset(M) ==> M -# 0 = M"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   291
by (auto simp add: multiset_def mdiff_def normalize_def multiset_fun_iff mset_of_def funrestrict_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   292
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   293
lemma mdiff_union_inverse2 [simp]: "multiset(M) ==> M +# {#a#} -# {#a#} = M"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   294
apply (unfold multiset_def munion_def mdiff_def msingle_def normalize_def mset_of_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   295
apply (auto cong add: if_cong simp add: ltD multiset_fun_iff funrestrict_def subset_Un_iff2 [THEN iffD1])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   296
prefer 2 apply (force intro!: lam_type)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   297
apply (subgoal_tac [2] "{x \<in> A \<union> {a} . x \<noteq> a \<and> x \<in> A} = A")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   298
apply (rule fun_extension, auto)
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   299
apply (drule_tac x = "A \<union> {a}" in spec)
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   300
apply (simp add: Finite_Un)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   301
apply (force intro!: lam_type)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   302
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   303
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   304
(** Count of elements **)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   305
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   306
lemma mcount_type [simp,TC]: "multiset(M) ==> mcount(M, a) \<in> nat"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   307
by (auto simp add: multiset_def mcount_def mset_of_def multiset_fun_iff)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   308
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   309
lemma mcount_0 [simp]: "mcount(0, a) = 0"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   310
by (simp add: mcount_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   311
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   312
lemma mcount_single [simp]: "mcount({#b#}, a) = (if a=b then 1 else 0)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   313
by (simp add: mcount_def mset_of_def msingle_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   314
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   315
lemma mcount_union [simp]: "[| multiset(M); multiset(N) |]
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   316
                     ==>  mcount(M +# N, a) = mcount(M, a) #+ mcount (N, a)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   317
apply (auto simp add: multiset_def multiset_fun_iff mcount_def munion_def mset_of_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   318
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   319
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   320
lemma mcount_diff [simp]:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   321
     "multiset(M) ==> mcount(M -# N, a) = mcount(M, a) #- mcount(N, a)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   322
apply (simp add: multiset_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   323
apply (auto dest!: not_lt_imp_le
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   324
     simp add: mdiff_def multiset_fun_iff mcount_def normalize_def mset_of_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   325
apply (force intro!: lam_type)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   326
apply (force intro!: lam_type)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   327
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   328
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   329
lemma mcount_elem: "[| multiset(M); a \<in> mset_of(M) |] ==> 0 < mcount(M, a)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   330
apply (simp add: multiset_def, clarify)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   331
apply (simp add: mcount_def mset_of_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   332
apply (simp add: multiset_fun_iff)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   333
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   334
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   335
(** msize **)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   336
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   337
lemma msize_0 [simp]: "msize(0) = #0"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   338
by (simp add: msize_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   339
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   340
lemma msize_single [simp]: "msize({#a#}) = #1"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   341
by (simp add: msize_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   342
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   343
lemma msize_type [simp,TC]: "msize(M) \<in> int"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   344
by (simp add: msize_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   345
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   346
lemma msize_zpositive: "multiset(M)==> #0 $\<le> msize(M)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   347
by (auto simp add: msize_def intro: g_zpos_imp_setsum_zpos)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   348
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   349
lemma msize_int_of_nat: "multiset(M) ==> \<exists>n \<in> nat. msize(M)= $# n"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   350
apply (rule not_zneg_int_of)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   351
apply (simp_all (no_asm_simp) add: msize_type [THEN znegative_iff_zless_0] not_zless_iff_zle msize_zpositive)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   352
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   353
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   354
lemma not_empty_multiset_imp_exist:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   355
     "[| M\<noteq>0; multiset(M) |] ==> \<exists>a \<in> mset_of(M). 0 < mcount(M, a)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   356
apply (simp add: multiset_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   357
apply (erule not_emptyE)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   358
apply (auto simp add: mset_of_def mcount_def multiset_fun_iff)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   359
apply (blast dest!: fun_is_rel)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   360
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   361
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   362
lemma msize_eq_0_iff: "multiset(M) ==> msize(M)=#0 \<longleftrightarrow> M=0"
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   363
apply (simp add: msize_def, auto)
59788
6f7b6adac439 prefer local fixes;
wenzelm
parents: 58318
diff changeset
   364
apply (rule_tac P = "setsum (u,v) \<noteq> #0" for u v in swap)
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   365
apply blast
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   366
apply (drule not_empty_multiset_imp_exist, assumption, clarify)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   367
apply (subgoal_tac "Finite (mset_of (M) - {a}) ")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   368
 prefer 2 apply (simp add: Finite_Diff)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   369
apply (subgoal_tac "setsum (%x. $# mcount (M, x), cons (a, mset_of (M) -{a}))=#0")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   370
 prefer 2 apply (simp add: cons_Diff, simp)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   371
apply (subgoal_tac "#0 $\<le> setsum (%x. $# mcount (M, x), mset_of (M) - {a}) ")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   372
apply (rule_tac [2] g_zpos_imp_setsum_zpos)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   373
apply (auto simp add: Finite_Diff not_zless_iff_zle [THEN iff_sym] znegative_iff_zless_0 [THEN iff_sym])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   374
apply (rule not_zneg_int_of [THEN bexE])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   375
apply (auto simp del: int_of_0 simp add: int_of_add [symmetric] int_of_0 [symmetric])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   376
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   377
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   378
lemma setsum_mcount_Int:
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   379
     "Finite(A) ==> setsum(%a. $# mcount(N, a), A \<inter> mset_of(N))
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26417
diff changeset
   380
                  = setsum(%a. $# mcount(N, a), A)"
18415
eb68dc98bda2 improved proofs;
wenzelm
parents: 16973
diff changeset
   381
apply (induct rule: Finite_induct)
eb68dc98bda2 improved proofs;
wenzelm
parents: 16973
diff changeset
   382
 apply auto
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   383
apply (subgoal_tac "Finite (B \<inter> mset_of (N))")
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   384
prefer 2 apply (blast intro: subset_Finite)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   385
apply (auto simp add: mcount_def Int_cons_left)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   386
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   387
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   388
lemma msize_union [simp]:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   389
     "[| multiset(M); multiset(N) |] ==> msize(M +# N) = msize(M) $+ msize(N)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   390
apply (simp add: msize_def setsum_Un setsum_addf int_of_add setsum_mcount_Int)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   391
apply (subst Int_commute)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   392
apply (simp add: setsum_mcount_Int)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   393
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   394
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   395
lemma msize_eq_succ_imp_elem: "[|msize(M)= $# succ(n); n \<in> nat|] ==> \<exists>a. a \<in> mset_of(M)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   396
apply (unfold msize_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   397
apply (blast dest: setsum_succD)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   398
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   399
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   400
(** Equality of multisets **)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   401
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   402
lemma equality_lemma:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   403
     "[| multiset(M); multiset(N); \<forall>a. mcount(M, a)=mcount(N, a) |]
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   404
      ==> mset_of(M)=mset_of(N)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   405
apply (simp add: multiset_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   406
apply (rule sym, rule equalityI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   407
apply (auto simp add: multiset_fun_iff mcount_def mset_of_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   408
apply (drule_tac [!] x=x in spec)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   409
apply (case_tac [2] "x \<in> Aa", case_tac "x \<in> A", auto)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   410
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   411
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   412
lemma multiset_equality:
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   413
  "[| multiset(M); multiset(N) |]==> M=N\<longleftrightarrow>(\<forall>a. mcount(M, a)=mcount(N, a))"
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   414
apply auto
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   415
apply (subgoal_tac "mset_of (M) = mset_of (N) ")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   416
prefer 2 apply (blast intro: equality_lemma)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   417
apply (simp add: multiset_def mset_of_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   418
apply (auto simp add: multiset_fun_iff)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   419
apply (rule fun_extension)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   420
apply (blast, blast)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   421
apply (drule_tac x = x in spec)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   422
apply (auto simp add: mcount_def mset_of_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   423
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   424
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   425
(** More algebraic properties of multisets **)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   426
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   427
lemma munion_eq_0_iff [simp]: "[|multiset(M); multiset(N)|]==>(M +# N =0) \<longleftrightarrow> (M=0 & N=0)"
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   428
by (auto simp add: multiset_equality)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   429
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   430
lemma empty_eq_munion_iff [simp]: "[|multiset(M); multiset(N)|]==>(0=M +# N) \<longleftrightarrow> (M=0 & N=0)"
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   431
apply (rule iffI, drule sym)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   432
apply (simp_all add: multiset_equality)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   433
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   434
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   435
lemma munion_right_cancel [simp]:
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   436
     "[| multiset(M); multiset(N); multiset(K) |]==>(M +# K = N +# K)\<longleftrightarrow>(M=N)"
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   437
by (auto simp add: multiset_equality)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   438
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   439
lemma munion_left_cancel [simp]:
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   440
  "[|multiset(K); multiset(M); multiset(N)|] ==>(K +# M = K +# N) \<longleftrightarrow> (M = N)"
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   441
by (auto simp add: multiset_equality)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   442
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   443
lemma nat_add_eq_1_cases: "[| m \<in> nat; n \<in> nat |] ==> (m #+ n = 1) \<longleftrightarrow> (m=1 & n=0) | (m=0 & n=1)"
18415
eb68dc98bda2 improved proofs;
wenzelm
parents: 16973
diff changeset
   444
by (induct_tac n) auto
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   445
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   446
lemma munion_is_single:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46822
diff changeset
   447
     "[|multiset(M); multiset(N)|]
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   448
      ==> (M +# N = {#a#}) \<longleftrightarrow>  (M={#a#} & N=0) | (M = 0 & N = {#a#})"
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   449
apply (simp (no_asm_simp) add: multiset_equality)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   450
apply safe
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   451
apply simp_all
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   452
apply (case_tac "aa=a")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   453
apply (drule_tac [2] x = aa in spec)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   454
apply (drule_tac x = a in spec)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   455
apply (simp add: nat_add_eq_1_cases, simp)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   456
apply (case_tac "aaa=aa", simp)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   457
apply (drule_tac x = aa in spec)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   458
apply (simp add: nat_add_eq_1_cases)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   459
apply (case_tac "aaa=a")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   460
apply (drule_tac [4] x = aa in spec)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   461
apply (drule_tac [3] x = a in spec)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   462
apply (drule_tac [2] x = aaa in spec)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   463
apply (drule_tac x = aa in spec)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   464
apply (simp_all add: nat_add_eq_1_cases)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   465
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   466
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   467
lemma msingle_is_union: "[| multiset(M); multiset(N) |]
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   468
  ==> ({#a#} = M +# N) \<longleftrightarrow> ({#a#} = M  & N=0 | M = 0 & {#a#} = N)"
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   469
apply (subgoal_tac " ({#a#} = M +# N) \<longleftrightarrow> (M +# N = {#a#}) ")
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   470
apply (simp (no_asm_simp) add: munion_is_single)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   471
apply blast
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   472
apply (blast dest: sym)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   473
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   474
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   475
(** Towards induction over multisets **)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   476
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   477
lemma setsum_decr:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   478
"Finite(A)
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   479
  ==>  (\<forall>M. multiset(M) \<longrightarrow>
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   480
  (\<forall>a \<in> mset_of(M). setsum(%z. $# mcount(M(a:=M`a #- 1), z), A) =
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   481
  (if a \<in> A then setsum(%z. $# mcount(M, z), A) $- #1
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   482
           else setsum(%z. $# mcount(M, z), A))))"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   483
apply (unfold multiset_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   484
apply (erule Finite_induct)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   485
apply (auto simp add: multiset_fun_iff)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   486
apply (unfold mset_of_def mcount_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   487
apply (case_tac "x \<in> A", auto)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   488
apply (subgoal_tac "$# M ` x $+ #-1 = $# M ` x $- $# 1")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   489
apply (erule ssubst)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   490
apply (rule int_of_diff, auto)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   491
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   492
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   493
lemma setsum_decr2:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   494
     "Finite(A)
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   495
      ==> \<forall>M. multiset(M) \<longrightarrow> (\<forall>a \<in> mset_of(M).
16973
b2a894562b8f simprocs: Simplifier.inherit_bounds;
wenzelm
parents: 15481
diff changeset
   496
           setsum(%x. $# mcount(funrestrict(M, mset_of(M)-{a}), x), A) =
b2a894562b8f simprocs: Simplifier.inherit_bounds;
wenzelm
parents: 15481
diff changeset
   497
           (if a \<in> A then setsum(%x. $# mcount(M, x), A) $- $# M`a
b2a894562b8f simprocs: Simplifier.inherit_bounds;
wenzelm
parents: 15481
diff changeset
   498
            else setsum(%x. $# mcount(M, x), A)))"
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   499
apply (simp add: multiset_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   500
apply (erule Finite_induct)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   501
apply (auto simp add: multiset_fun_iff mcount_def mset_of_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   502
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   503
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   504
lemma setsum_decr3: "[| Finite(A); multiset(M); a \<in> mset_of(M) |]
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   505
      ==> setsum(%x. $# mcount(funrestrict(M, mset_of(M)-{a}), x), A - {a}) =
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   506
          (if a \<in> A then setsum(%x. $# mcount(M, x), A) $- $# M`a
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   507
           else setsum(%x. $# mcount(M, x), A))"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   508
apply (subgoal_tac "setsum (%x. $# mcount (funrestrict (M, mset_of (M) -{a}),x),A-{a}) = setsum (%x. $# mcount (funrestrict (M, mset_of (M) -{a}),x),A) ")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   509
apply (rule_tac [2] setsum_Diff [symmetric])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   510
apply (rule sym, rule ssubst, blast)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   511
apply (rule sym, drule setsum_decr2, auto)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   512
apply (simp add: mcount_def mset_of_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   513
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   514
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   515
lemma nat_le_1_cases: "n \<in> nat ==> n \<le> 1 \<longleftrightarrow> (n=0 | n=1)"
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   516
by (auto elim: natE)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   517
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   518
lemma succ_pred_eq_self: "[| 0<n; n \<in> nat |] ==> succ(n #- 1) = n"
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   519
apply (subgoal_tac "1 \<le> n")
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   520
apply (drule add_diff_inverse2, auto)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   521
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   522
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59788
diff changeset
   523
text\<open>Specialized for use in the proof below.\<close>
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   524
lemma multiset_funrestict:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   525
     "\<lbrakk>\<forall>a\<in>A. M ` a \<in> nat \<and> 0 < M ` a; Finite(A)\<rbrakk>
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   526
      \<Longrightarrow> multiset(funrestrict(M, A - {a}))"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   527
apply (simp add: multiset_def multiset_fun_iff)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   528
apply (rule_tac x="A-{a}" in exI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   529
apply (auto intro: Finite_Diff funrestrict_type)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   530
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   531
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   532
lemma multiset_induct_aux:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   533
  assumes prem1: "!!M a. [| multiset(M); a\<notin>mset_of(M); P(M) |] ==> P(cons(<a, 1>, M))"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   534
      and prem2: "!!M b. [| multiset(M); b \<in> mset_of(M); P(M) |] ==> P(M(b:= M`b #+ 1))"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   535
  shows
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   536
  "[| n \<in> nat; P(0) |]
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   537
     ==> (\<forall>M. multiset(M)\<longrightarrow>
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   538
  (setsum(%x. $# mcount(M, x), {x \<in> mset_of(M). 0 < M`x}) = $# n) \<longrightarrow> P(M))"
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   539
apply (erule nat_induct, clarify)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   540
apply (frule msize_eq_0_iff)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   541
apply (auto simp add: mset_of_def multiset_def multiset_fun_iff msize_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   542
apply (subgoal_tac "setsum (%x. $# mcount (M, x), A) =$# succ (x) ")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   543
apply (drule setsum_succD, auto)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   544
apply (case_tac "1 <M`a")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   545
apply (drule_tac [2] not_lt_imp_le)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   546
apply (simp_all add: nat_le_1_cases)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   547
apply (subgoal_tac "M= (M (a:=M`a #- 1)) (a:= (M (a:=M`a #- 1))`a #+ 1) ")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   548
apply (rule_tac [2] A = A and B = "%x. nat" and D = "%x. nat" in fun_extension)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   549
apply (rule_tac [3] update_type)+
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   550
apply (simp_all (no_asm_simp))
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   551
 apply (rule_tac [2] impI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   552
 apply (rule_tac [2] succ_pred_eq_self [symmetric])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   553
apply (simp_all (no_asm_simp))
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   554
apply (rule subst, rule sym, blast, rule prem2)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   555
apply (simp (no_asm) add: multiset_def multiset_fun_iff)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   556
apply (rule_tac x = A in exI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   557
apply (force intro: update_type)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   558
apply (simp (no_asm_simp) add: mset_of_def mcount_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   559
apply (drule_tac x = "M (a := M ` a #- 1) " in spec)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   560
apply (drule mp, drule_tac [2] mp, simp_all)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   561
apply (rule_tac x = A in exI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   562
apply (auto intro: update_type)
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   563
apply (subgoal_tac "Finite ({x \<in> cons (a, A) . x\<noteq>a\<longrightarrow>0<M`x}) ")
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   564
prefer 2 apply (blast intro: Collect_subset [THEN subset_Finite] Finite_cons)
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   565
apply (drule_tac A = "{x \<in> cons (a, A) . x\<noteq>a\<longrightarrow>0<M`x}" in setsum_decr)
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   566
apply (drule_tac x = M in spec)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   567
apply (subgoal_tac "multiset (M) ")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   568
 prefer 2
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   569
 apply (simp add: multiset_def multiset_fun_iff)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   570
 apply (rule_tac x = A in exI, force)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   571
apply (simp_all add: mset_of_def)
59788
6f7b6adac439 prefer local fixes;
wenzelm
parents: 58318
diff changeset
   572
apply (drule_tac psi = "\<forall>x \<in> A. u(x)" for u in asm_rl)
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   573
apply (drule_tac x = a in bspec)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   574
apply (simp (no_asm_simp))
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   575
apply (subgoal_tac "cons (a, A) = A")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   576
prefer 2 apply blast
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   577
apply simp
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   578
apply (subgoal_tac "M=cons (<a, M`a>, funrestrict (M, A-{a}))")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   579
 prefer 2
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   580
 apply (rule fun_cons_funrestrict_eq)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   581
 apply (subgoal_tac "cons (a, A-{a}) = A")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   582
  apply force
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   583
  apply force
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   584
apply (rule_tac a = "cons (<a, 1>, funrestrict (M, A - {a}))" in ssubst)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   585
apply simp
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   586
apply (frule multiset_funrestict, assumption)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   587
apply (rule prem1, assumption)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   588
apply (simp add: mset_of_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   589
apply (drule_tac x = "funrestrict (M, A-{a}) " in spec)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   590
apply (drule mp)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   591
apply (rule_tac x = "A-{a}" in exI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   592
apply (auto intro: Finite_Diff funrestrict_type simp add: funrestrict)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   593
apply (frule_tac A = A and M = M and a = a in setsum_decr3)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   594
apply (simp (no_asm_simp) add: multiset_def multiset_fun_iff)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   595
apply blast
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   596
apply (simp (no_asm_simp) add: mset_of_def)
59788
6f7b6adac439 prefer local fixes;
wenzelm
parents: 58318
diff changeset
   597
apply (drule_tac b = "if u then v else w" for u v w in sym, simp_all)
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   598
apply (subgoal_tac "{x \<in> A - {a} . 0 < funrestrict (M, A - {x}) ` x} = A - {a}")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   599
apply (auto intro!: setsum_cong simp add: zdiff_eq_iff zadd_commute multiset_def multiset_fun_iff mset_of_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   600
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   601
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   602
lemma multiset_induct2:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   603
  "[| multiset(M); P(0);
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   604
    (!!M a. [| multiset(M); a\<notin>mset_of(M); P(M) |] ==> P(cons(<a, 1>, M)));
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   605
    (!!M b. [| multiset(M); b \<in> mset_of(M);  P(M) |] ==> P(M(b:= M`b #+ 1))) |]
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   606
     ==> P(M)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   607
apply (subgoal_tac "\<exists>n \<in> nat. setsum (\<lambda>x. $# mcount (M, x), {x \<in> mset_of (M) . 0 < M ` x}) = $# n")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   608
apply (rule_tac [2] not_zneg_int_of)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   609
apply (simp_all (no_asm_simp) add: znegative_iff_zless_0 not_zless_iff_zle)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   610
apply (rule_tac [2] g_zpos_imp_setsum_zpos)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   611
prefer 2 apply (blast intro:  multiset_set_of_Finite Collect_subset [THEN subset_Finite])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   612
 prefer 2 apply (simp add: multiset_def multiset_fun_iff, clarify)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   613
apply (rule multiset_induct_aux [rule_format], auto)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   614
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   615
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   616
lemma munion_single_case1:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   617
     "[| multiset(M); a \<notin>mset_of(M) |] ==> M +# {#a#} = cons(<a, 1>, M)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   618
apply (simp add: multiset_def msingle_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   619
apply (auto simp add: munion_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   620
apply (unfold mset_of_def, simp)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   621
apply (rule fun_extension, rule lam_type, simp_all)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   622
apply (auto simp add: multiset_fun_iff fun_extend_apply)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   623
apply (drule_tac c = a and b = 1 in fun_extend3)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   624
apply (auto simp add: cons_eq Un_commute [of _ "{a}"])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   625
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   626
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   627
lemma munion_single_case2:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   628
     "[| multiset(M); a \<in> mset_of(M) |] ==> M +# {#a#} = M(a:=M`a #+ 1)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   629
apply (simp add: multiset_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   630
apply (auto simp add: munion_def multiset_fun_iff msingle_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   631
apply (unfold mset_of_def, simp)
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   632
apply (subgoal_tac "A \<union> {a} = A")
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   633
apply (rule fun_extension)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   634
apply (auto dest: domain_type intro: lam_type update_type)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   635
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   636
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   637
(* Induction principle for multisets *)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   638
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   639
lemma multiset_induct:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   640
  assumes M: "multiset(M)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   641
      and P0: "P(0)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   642
      and step: "!!M a. [| multiset(M); P(M) |] ==> P(M +# {#a#})"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   643
  shows "P(M)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   644
apply (rule multiset_induct2 [OF M])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   645
apply (simp_all add: P0)
20898
113c9516a2d7 attribute symmetric: zero_var_indexes;
wenzelm
parents: 18415
diff changeset
   646
apply (frule_tac [2] a = b in munion_single_case2 [symmetric])
113c9516a2d7 attribute symmetric: zero_var_indexes;
wenzelm
parents: 18415
diff changeset
   647
apply (frule_tac a = a in munion_single_case1 [symmetric])
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   648
apply (auto intro: step)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   649
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   650
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   651
(** MCollect **)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   652
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   653
lemma MCollect_multiset [simp]:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   654
     "multiset(M) ==> multiset({# x \<in> M. P(x)#})"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   655
apply (simp add: MCollect_def multiset_def mset_of_def, clarify)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   656
apply (rule_tac x = "{x \<in> A. P (x) }" in exI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   657
apply (auto dest: CollectD1 [THEN [2] apply_type]
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   658
            intro: Collect_subset [THEN subset_Finite] funrestrict_type)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   659
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   660
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   661
lemma mset_of_MCollect [simp]:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   662
     "multiset(M) ==> mset_of({# x \<in> M. P(x) #}) \<subseteq> mset_of(M)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   663
by (auto simp add: mset_of_def MCollect_def multiset_def funrestrict_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   664
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   665
lemma MCollect_mem_iff [iff]:
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   666
     "x \<in> mset_of({#x \<in> M. P(x)#}) \<longleftrightarrow>  x \<in> mset_of(M) & P(x)"
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   667
by (simp add: MCollect_def mset_of_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   668
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   669
lemma mcount_MCollect [simp]:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   670
     "mcount({# x \<in> M. P(x) #}, a) = (if P(a) then mcount(M,a) else 0)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   671
by (simp add: mcount_def MCollect_def mset_of_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   672
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   673
lemma multiset_partition: "multiset(M) ==> M = {# x \<in> M. P(x) #} +# {# x \<in> M. ~ P(x) #}"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   674
by (simp add: multiset_equality)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   675
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   676
lemma natify_elem_is_self [simp]:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   677
     "[| multiset(M); a \<in> mset_of(M) |] ==> natify(M`a) = M`a"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   678
by (auto simp add: multiset_def mset_of_def multiset_fun_iff)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   679
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   680
(* and more algebraic laws on multisets *)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   681
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   682
lemma munion_eq_conv_diff: "[| multiset(M); multiset(N) |]
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   683
  ==>  (M +# {#a#} = N +# {#b#}) \<longleftrightarrow>  (M = N & a = b |
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   684
       M = N -# {#a#} +# {#b#} & N = M -# {#b#} +# {#a#})"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   685
apply (simp del: mcount_single add: multiset_equality)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   686
apply (rule iffI, erule_tac [2] disjE, erule_tac [3] conjE)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   687
apply (case_tac "a=b", auto)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   688
apply (drule_tac x = a in spec)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   689
apply (drule_tac [2] x = b in spec)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   690
apply (drule_tac [3] x = aa in spec)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   691
apply (drule_tac [4] x = a in spec, auto)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   692
apply (subgoal_tac [!] "mcount (N,a) :nat")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   693
apply (erule_tac [3] natE, erule natE, auto)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   694
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   695
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   696
lemma melem_diff_single:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   697
"multiset(M) ==>
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   698
  k \<in> mset_of(M -# {#a#}) \<longleftrightarrow> (k=a & 1 < mcount(M,a)) | (k\<noteq> a & k \<in> mset_of(M))"
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   699
apply (simp add: multiset_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   700
apply (simp add: normalize_def mset_of_def msingle_def mdiff_def mcount_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   701
apply (auto dest: domain_type intro: zero_less_diff [THEN iffD1]
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   702
            simp add: multiset_fun_iff apply_iff)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   703
apply (force intro!: lam_type)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   704
apply (force intro!: lam_type)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   705
apply (force intro!: lam_type)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   706
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   707
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   708
lemma munion_eq_conv_exist:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   709
"[| M \<in> Mult(A); N \<in> Mult(A) |]
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   710
  ==> (M +# {#a#} = N +# {#b#}) \<longleftrightarrow>
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   711
      (M=N & a=b | (\<exists>K \<in> Mult(A). M= K +# {#b#} & N=K +# {#a#}))"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   712
by (auto simp add: Mult_iff_multiset melem_diff_single munion_eq_conv_diff)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   713
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   714
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59788
diff changeset
   715
subsection\<open>Multiset Orderings\<close>
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   716
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   717
(* multiset on a domain A are finite functions from A to nat-{0} *)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   718
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   719
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   720
(* multirel1 type *)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   721
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   722
lemma multirel1_type: "multirel1(A, r) \<subseteq> Mult(A)*Mult(A)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   723
by (auto simp add: multirel1_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   724
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   725
lemma multirel1_0 [simp]: "multirel1(0, r) =0"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   726
by (auto simp add: multirel1_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   727
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   728
lemma multirel1_iff:
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   729
" <N, M> \<in> multirel1(A, r) \<longleftrightarrow>
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   730
  (\<exists>a. a \<in> A &
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   731
  (\<exists>M0. M0 \<in> Mult(A) & (\<exists>K. K \<in> Mult(A) &
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   732
   M=M0 +# {#a#} & N=M0 +# K & (\<forall>b \<in> mset_of(K). <b,a> \<in> r))))"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   733
by (auto simp add: multirel1_def Mult_iff_multiset Bex_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   734
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   735
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59788
diff changeset
   736
text\<open>Monotonicity of @{term multirel1}\<close>
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   737
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   738
lemma multirel1_mono1: "A\<subseteq>B ==> multirel1(A, r)\<subseteq>multirel1(B, r)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   739
apply (auto simp add: multirel1_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   740
apply (auto simp add: Un_subset_iff Mult_iff_multiset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   741
apply (rule_tac x = a in bexI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   742
apply (rule_tac x = M0 in bexI, simp)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   743
apply (rule_tac x = K in bexI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   744
apply (auto simp add: Mult_iff_multiset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   745
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   746
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   747
lemma multirel1_mono2: "r\<subseteq>s ==> multirel1(A,r)\<subseteq>multirel1(A, s)"
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46822
diff changeset
   748
apply (simp add: multirel1_def, auto)
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   749
apply (rule_tac x = a in bexI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   750
apply (rule_tac x = M0 in bexI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   751
apply (simp_all add: Mult_iff_multiset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   752
apply (rule_tac x = K in bexI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   753
apply (simp_all add: Mult_iff_multiset, auto)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   754
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   755
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   756
lemma multirel1_mono:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   757
     "[| A\<subseteq>B; r\<subseteq>s |] ==> multirel1(A, r) \<subseteq> multirel1(B, s)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   758
apply (rule subset_trans)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   759
apply (rule multirel1_mono1)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   760
apply (rule_tac [2] multirel1_mono2, auto)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   761
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   762
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59788
diff changeset
   763
subsection\<open>Toward the proof of well-foundedness of multirel1\<close>
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   764
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   765
lemma not_less_0 [iff]: "<M,0> \<notin> multirel1(A, r)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   766
by (auto simp add: multirel1_def Mult_iff_multiset)
12089
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
   767
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   768
lemma less_munion: "[| <N, M0 +# {#a#}> \<in> multirel1(A, r); M0 \<in> Mult(A) |] ==>
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   769
  (\<exists>M. <M, M0> \<in> multirel1(A, r) & N = M +# {#a#}) |
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   770
  (\<exists>K. K \<in> Mult(A) & (\<forall>b \<in> mset_of(K). <b, a> \<in> r) & N = M0 +# K)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   771
apply (frule multirel1_type [THEN subsetD])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   772
apply (simp add: multirel1_iff)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   773
apply (auto simp add: munion_eq_conv_exist)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   774
apply (rule_tac x="Ka +# K" in exI, auto, simp add: Mult_iff_multiset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   775
apply (simp (no_asm_simp) add: munion_left_cancel munion_assoc)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   776
apply (auto simp add: munion_commute)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   777
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   778
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   779
lemma multirel1_base: "[| M \<in> Mult(A); a \<in> A |] ==> <M, M +# {#a#}> \<in> multirel1(A, r)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   780
apply (auto simp add: multirel1_iff)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   781
apply (simp add: Mult_iff_multiset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   782
apply (rule_tac x = a in exI, clarify)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   783
apply (rule_tac x = M in exI, simp)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   784
apply (rule_tac x = 0 in exI, auto)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   785
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   786
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   787
lemma acc_0: "acc(0)=0"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   788
by (auto intro!: equalityI dest: acc.dom_subset [THEN subsetD])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   789
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   790
lemma lemma1: "[| \<forall>b \<in> A. <b,a> \<in> r \<longrightarrow>
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   791
    (\<forall>M \<in> acc(multirel1(A, r)). M +# {#b#}:acc(multirel1(A, r)));
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   792
    M0 \<in> acc(multirel1(A, r)); a \<in> A;
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   793
    \<forall>M. <M,M0> \<in> multirel1(A, r) \<longrightarrow> M +# {#a#} \<in> acc(multirel1(A, r)) |]
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   794
  ==> M0 +# {#a#} \<in> acc(multirel1(A, r))"
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 15201
diff changeset
   795
apply (subgoal_tac "M0 \<in> Mult(A) ")
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   796
 prefer 2
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   797
 apply (erule acc.cases)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   798
 apply (erule fieldE)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   799
 apply (auto dest: multirel1_type [THEN subsetD])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   800
apply (rule accI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   801
apply (rename_tac "N")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   802
apply (drule less_munion, blast)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   803
apply (auto simp add: Mult_iff_multiset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   804
apply (erule_tac P = "\<forall>x \<in> mset_of (K) . <x, a> \<in> r" in rev_mp)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   805
apply (erule_tac P = "mset_of (K) \<subseteq>A" in rev_mp)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   806
apply (erule_tac M = K in multiset_induct)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   807
(* three subgoals *)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46822
diff changeset
   808
(* subgoal 1 \<in> the induction base case *)
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   809
apply (simp (no_asm_simp))
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46822
diff changeset
   810
(* subgoal 2 \<in> the induction general case *)
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   811
apply (simp add: Ball_def Un_subset_iff, clarify)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   812
apply (drule_tac x = aa in spec, simp)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   813
apply (subgoal_tac "aa \<in> A")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   814
prefer 2 apply blast
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   815
apply (drule_tac x = "M0 +# M" and P =
59788
6f7b6adac439 prefer local fixes;
wenzelm
parents: 58318
diff changeset
   816
       "%x. x \<in> acc(multirel1(A, r)) \<longrightarrow> Q(x)" for Q in spec)
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   817
apply (simp add: munion_assoc [symmetric])
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46822
diff changeset
   818
(* subgoal 3 \<in> additional conditions *)
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   819
apply (auto intro!: multirel1_base [THEN fieldI2] simp add: Mult_iff_multiset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   820
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   821
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   822
lemma lemma2: "[| \<forall>b \<in> A. <b,a> \<in> r
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   823
   \<longrightarrow> (\<forall>M \<in> acc(multirel1(A, r)). M +# {#b#} :acc(multirel1(A, r)));
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   824
        M \<in> acc(multirel1(A, r)); a \<in> A|] ==> M +# {#a#} \<in> acc(multirel1(A, r))"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   825
apply (erule acc_induct)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   826
apply (blast intro: lemma1)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   827
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   828
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   829
lemma lemma3: "[| wf[A](r); a \<in> A |]
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   830
      ==> \<forall>M \<in> acc(multirel1(A, r)). M +# {#a#} \<in> acc(multirel1(A, r))"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   831
apply (erule_tac a = a in wf_on_induct, blast)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   832
apply (blast intro: lemma2)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   833
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   834
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   835
lemma lemma4: "multiset(M) ==> mset_of(M)\<subseteq>A \<longrightarrow>
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   836
   wf[A](r) \<longrightarrow> M \<in> field(multirel1(A, r)) \<longrightarrow> M \<in> acc(multirel1(A, r))"
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   837
apply (erule multiset_induct)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   838
(* proving the base case *)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   839
apply clarify
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   840
apply (rule accI, force)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   841
apply (simp add: multirel1_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   842
(* Proving the general case *)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   843
apply clarify
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   844
apply simp
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   845
apply (subgoal_tac "mset_of (M) \<subseteq>A")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   846
prefer 2 apply blast
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   847
apply clarify
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   848
apply (drule_tac a = a in lemma3, blast)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   849
apply (subgoal_tac "M \<in> field (multirel1 (A,r))")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   850
apply blast
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   851
apply (rule multirel1_base [THEN fieldI1])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   852
apply (auto simp add: Mult_iff_multiset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   853
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   854
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   855
lemma all_accessible: "[| wf[A](r); M \<in> Mult(A); A \<noteq> 0|] ==> M \<in> acc(multirel1(A, r))"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   856
apply (erule not_emptyE)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   857
apply  (rule lemma4 [THEN mp, THEN mp, THEN mp])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   858
apply (rule_tac [4] multirel1_base [THEN fieldI1])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   859
apply  (auto simp add: Mult_iff_multiset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   860
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   861
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   862
lemma wf_on_multirel1: "wf[A](r) ==> wf[A-||>nat-{0}](multirel1(A, r))"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   863
apply (case_tac "A=0")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   864
apply (simp (no_asm_simp))
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   865
apply (rule wf_imp_wf_on)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   866
apply (rule wf_on_field_imp_wf)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   867
apply (simp (no_asm_simp) add: wf_on_0)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   868
apply (rule_tac A = "acc (multirel1 (A,r))" in wf_on_subset_A)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   869
apply (rule wf_on_acc)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   870
apply (blast intro: all_accessible)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   871
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   872
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   873
lemma wf_multirel1: "wf(r) ==>wf(multirel1(field(r), r))"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   874
apply (simp (no_asm_use) add: wf_iff_wf_on_field)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   875
apply (drule wf_on_multirel1)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   876
apply (rule_tac A = "field (r) -||> nat - {0}" in wf_on_subset_A)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   877
apply (simp (no_asm_simp))
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   878
apply (rule field_rel_subset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   879
apply (rule multirel1_type)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   880
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   881
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   882
(** multirel **)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   883
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   884
lemma multirel_type: "multirel(A, r) \<subseteq> Mult(A)*Mult(A)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   885
apply (simp add: multirel_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   886
apply (rule trancl_type [THEN subset_trans])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   887
apply (auto dest: multirel1_type [THEN subsetD])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   888
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   889
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   890
(* Monotonicity of multirel *)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   891
lemma multirel_mono:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   892
     "[| A\<subseteq>B; r\<subseteq>s |] ==> multirel(A, r)\<subseteq>multirel(B,s)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   893
apply (simp add: multirel_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   894
apply (rule trancl_mono)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   895
apply (rule multirel1_mono, auto)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   896
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   897
63040
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 61798
diff changeset
   898
(* Equivalence of multirel with the usual (closure-free) definition *)
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   899
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   900
lemma add_diff_eq: "k \<in> nat ==> 0 < k \<longrightarrow> n #+ k #- 1 = n #+ (k #- 1)"
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   901
by (erule nat_induct, auto)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   902
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   903
lemma mdiff_union_single_conv: "[|a \<in> mset_of(J); multiset(I); multiset(J) |]
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   904
   ==> I +# J -# {#a#} = I +# (J-# {#a#})"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   905
apply (simp (no_asm_simp) add: multiset_equality)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   906
apply (case_tac "a \<notin> mset_of (I) ")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   907
apply (auto simp add: mcount_def mset_of_def multiset_def multiset_fun_iff)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   908
apply (auto dest: domain_type simp add: add_diff_eq)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   909
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   910
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   911
lemma diff_add_commute: "[| n \<le> m;  m \<in> nat; n \<in> nat; k \<in> nat |] ==> m #- n #+ k = m #+ k #- n"
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   912
by (auto simp add: le_iff less_iff_succ_add)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   913
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   914
(* One direction *)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   915
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   916
lemma multirel_implies_one_step:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   917
"<M,N> \<in> multirel(A, r) ==>
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   918
     trans[A](r) \<longrightarrow>
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   919
     (\<exists>I J K.
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   920
         I \<in> Mult(A) & J \<in> Mult(A) &  K \<in> Mult(A) &
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   921
         N = I +# J & M = I +# K & J \<noteq> 0 &
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   922
        (\<forall>k \<in> mset_of(K). \<exists>j \<in> mset_of(J). <k,j> \<in> r))"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   923
apply (simp add: multirel_def Ball_def Bex_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   924
apply (erule converse_trancl_induct)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   925
apply (simp_all add: multirel1_iff Mult_iff_multiset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   926
(* Two subgoals remain *)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   927
(* Subgoal 1 *)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   928
apply clarify
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   929
apply (rule_tac x = M0 in exI, force)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   930
(* Subgoal 2 *)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   931
apply clarify
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 46953
diff changeset
   932
apply hypsubst_thin
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   933
apply (case_tac "a \<in> mset_of (Ka) ")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   934
apply (rule_tac x = I in exI, simp (no_asm_simp))
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   935
apply (rule_tac x = J in exI, simp (no_asm_simp))
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   936
apply (rule_tac x = " (Ka -# {#a#}) +# K" in exI, simp (no_asm_simp))
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   937
apply (simp_all add: Un_subset_iff)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   938
apply (simp (no_asm_simp) add: munion_assoc [symmetric])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   939
apply (drule_tac t = "%M. M-#{#a#}" in subst_context)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   940
apply (simp add: mdiff_union_single_conv melem_diff_single, clarify)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   941
apply (erule disjE, simp)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   942
apply (erule disjE, simp)
59788
6f7b6adac439 prefer local fixes;
wenzelm
parents: 58318
diff changeset
   943
apply (drule_tac x = a and P = "%x. x :# Ka \<longrightarrow> Q(x)" for Q in spec)
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   944
apply clarify
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   945
apply (rule_tac x = xa in exI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   946
apply (simp (no_asm_simp))
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   947
apply (blast dest: trans_onD)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   948
(* new we know that  a\<notin>mset_of(Ka) *)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   949
apply (subgoal_tac "a :# I")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   950
apply (rule_tac x = "I-#{#a#}" in exI, simp (no_asm_simp))
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   951
apply (rule_tac x = "J+#{#a#}" in exI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   952
apply (simp (no_asm_simp) add: Un_subset_iff)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   953
apply (rule_tac x = "Ka +# K" in exI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   954
apply (simp (no_asm_simp) add: Un_subset_iff)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   955
apply (rule conjI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   956
apply (simp (no_asm_simp) add: multiset_equality mcount_elem [THEN succ_pred_eq_self])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   957
apply (rule conjI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   958
apply (drule_tac t = "%M. M-#{#a#}" in subst_context)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   959
apply (simp add: mdiff_union_inverse2)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   960
apply (simp_all (no_asm_simp) add: multiset_equality)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   961
apply (rule diff_add_commute [symmetric])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   962
apply (auto intro: mcount_elem)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   963
apply (subgoal_tac "a \<in> mset_of (I +# Ka) ")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   964
apply (drule_tac [2] sym, auto)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   965
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   966
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   967
lemma melem_imp_eq_diff_union [simp]: "[| a \<in> mset_of(M); multiset(M) |] ==> M -# {#a#} +# {#a#} = M"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   968
by (simp add: multiset_equality mcount_elem [THEN succ_pred_eq_self])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   969
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   970
lemma msize_eq_succ_imp_eq_union:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   971
     "[| msize(M)=$# succ(n); M \<in> Mult(A); n \<in> nat |]
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   972
      ==> \<exists>a N. M = N +# {#a#} & N \<in> Mult(A) & a \<in> A"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   973
apply (drule msize_eq_succ_imp_elem, auto)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   974
apply (rule_tac x = a in exI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   975
apply (rule_tac x = "M -# {#a#}" in exI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   976
apply (frule Mult_into_multiset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   977
apply (simp (no_asm_simp))
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   978
apply (auto simp add: Mult_iff_multiset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   979
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   980
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   981
(* The second direction *)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   982
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   983
lemma one_step_implies_multirel_lemma [rule_format (no_asm)]:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   984
"n \<in> nat ==>
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   985
   (\<forall>I J K.
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   986
    I \<in> Mult(A) & J \<in> Mult(A) & K \<in> Mult(A) &
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   987
   (msize(J) = $# n & J \<noteq>0 &  (\<forall>k \<in> mset_of(K).  \<exists>j \<in> mset_of(J). <k, j> \<in> r))
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
   988
    \<longrightarrow> <I +# K, I +# J> \<in> multirel(A, r))"
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   989
apply (simp add: Mult_iff_multiset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   990
apply (erule nat_induct, clarify)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   991
apply (drule_tac M = J in msize_eq_0_iff, auto)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   992
(* one subgoal remains *)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   993
apply (subgoal_tac "msize (J) =$# succ (x) ")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   994
 prefer 2 apply simp
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   995
apply (frule_tac A = A in msize_eq_succ_imp_eq_union)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   996
apply (simp_all add: Mult_iff_multiset, clarify)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   997
apply (rename_tac "J'", simp)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   998
apply (case_tac "J' = 0")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
   999
apply (simp add: multirel_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1000
apply (rule r_into_trancl, clarify)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1001
apply (simp add: multirel1_iff Mult_iff_multiset, force)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1002
(*Now we know J' \<noteq>  0*)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1003
apply (drule sym, rotate_tac -1, simp)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1004
apply (erule_tac V = "$# x = msize (J') " in thin_rl)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1005
apply (frule_tac M = K and P = "%x. <x,a> \<in> r" in multiset_partition)
59788
6f7b6adac439 prefer local fixes;
wenzelm
parents: 58318
diff changeset
  1006
apply (erule_tac P = "\<forall>k \<in> mset_of (K) . P(k)" for P in rev_mp)
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1007
apply (erule ssubst)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1008
apply (simp add: Ball_def, auto)
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 15201
diff changeset
  1009
apply (subgoal_tac "< (I +# {# x \<in> K. <x, a> \<in> r#}) +# {# x \<in> K. <x, a> \<notin> r#}, (I +# {# x \<in> K. <x, a> \<in> r#}) +# J'> \<in> multirel(A, r) ")
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1010
 prefer 2
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1011
 apply (drule_tac x = "I +# {# x \<in> K. <x, a> \<in> r#}" in spec)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1012
 apply (rotate_tac -1)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1013
 apply (drule_tac x = "J'" in spec)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1014
 apply (rotate_tac -1)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1015
 apply (drule_tac x = "{# x \<in> K. <x, a> \<notin> r#}" in spec, simp) apply blast
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1016
apply (simp add: munion_assoc [symmetric] multirel_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1017
apply (rule_tac b = "I +# {# x \<in> K. <x, a> \<in> r#} +# J'" in trancl_trans, blast)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1018
apply (rule r_into_trancl)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1019
apply (simp add: multirel1_iff Mult_iff_multiset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1020
apply (rule_tac x = a in exI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1021
apply (simp (no_asm_simp))
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1022
apply (rule_tac x = "I +# J'" in exI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1023
apply (auto simp add: munion_ac Un_subset_iff)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1024
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1025
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1026
lemma one_step_implies_multirel:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1027
     "[| J \<noteq> 0;  \<forall>k \<in> mset_of(K). \<exists>j \<in> mset_of(J). <k,j> \<in> r;
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1028
         I \<in> Mult(A); J \<in> Mult(A); K \<in> Mult(A) |]
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1029
      ==> <I+#K, I+#J> \<in> multirel(A, r)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1030
apply (subgoal_tac "multiset (J) ")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1031
 prefer 2 apply (simp add: Mult_iff_multiset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1032
apply (frule_tac M = J in msize_int_of_nat)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1033
apply (auto intro: one_step_implies_multirel_lemma)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1034
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1035
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1036
(** Proving that multisets are partially ordered **)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1037
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1038
(*irreflexivity*)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1039
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1040
lemma multirel_irrefl_lemma:
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
  1041
     "Finite(A) ==> part_ord(A, r) \<longrightarrow> (\<forall>x \<in> A. \<exists>y \<in> A. <x,y> \<in> r) \<longrightarrow>A=0"
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1042
apply (erule Finite_induct)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1043
apply (auto dest: subset_consI [THEN [2] part_ord_subset])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1044
apply (auto simp add: part_ord_def irrefl_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1045
apply (drule_tac x = xa in bspec)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1046
apply (drule_tac [2] a = xa and b = x in trans_onD, auto)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1047
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1048
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1049
lemma irrefl_on_multirel:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1050
     "part_ord(A, r) ==> irrefl(Mult(A), multirel(A, r))"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1051
apply (simp add: irrefl_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1052
apply (subgoal_tac "trans[A](r) ")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1053
 prefer 2 apply (simp add: part_ord_def, clarify)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1054
apply (drule multirel_implies_one_step, clarify)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1055
apply (simp add: Mult_iff_multiset, clarify)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1056
apply (subgoal_tac "Finite (mset_of (K))")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1057
apply (frule_tac r = r in multirel_irrefl_lemma)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1058
apply (frule_tac B = "mset_of (K) " in part_ord_subset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1059
apply simp_all
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1060
apply (auto simp add: multiset_def mset_of_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1061
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1062
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1063
lemma trans_on_multirel: "trans[Mult(A)](multirel(A, r))"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1064
apply (simp add: multirel_def trans_on_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1065
apply (blast intro: trancl_trans)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1066
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1067
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1068
lemma multirel_trans:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1069
 "[| <M, N> \<in> multirel(A, r); <N, K> \<in> multirel(A, r) |] ==>  <M, K> \<in> multirel(A,r)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1070
apply (simp add: multirel_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1071
apply (blast intro: trancl_trans)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1072
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1073
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1074
lemma trans_multirel: "trans(multirel(A,r))"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1075
apply (simp add: multirel_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1076
apply (rule trans_trancl)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1077
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1078
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1079
lemma part_ord_multirel: "part_ord(A,r) ==> part_ord(Mult(A), multirel(A, r))"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1080
apply (simp (no_asm) add: part_ord_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1081
apply (blast intro: irrefl_on_multirel trans_on_multirel)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1082
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1083
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1084
(** Monotonicity of multiset union **)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1085
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1086
lemma munion_multirel1_mono:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1087
"[|<M,N> \<in> multirel1(A, r); K \<in> Mult(A) |] ==> <K +# M, K +# N> \<in> multirel1(A, r)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1088
apply (frule multirel1_type [THEN subsetD])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1089
apply (auto simp add: multirel1_iff Mult_iff_multiset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1090
apply (rule_tac x = a in exI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1091
apply (simp (no_asm_simp))
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1092
apply (rule_tac x = "K+#M0" in exI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1093
apply (simp (no_asm_simp) add: Un_subset_iff)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1094
apply (rule_tac x = Ka in exI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1095
apply (simp (no_asm_simp) add: munion_assoc)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1096
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1097
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1098
lemma munion_multirel_mono2:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1099
 "[| <M, N> \<in> multirel(A, r); K \<in> Mult(A) |]==><K +# M, K +# N> \<in> multirel(A, r)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1100
apply (frule multirel_type [THEN subsetD])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1101
apply (simp (no_asm_use) add: multirel_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1102
apply clarify
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1103
apply (drule_tac psi = "<M,N> \<in> multirel1 (A, r) ^+" in asm_rl)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1104
apply (erule rev_mp)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1105
apply (erule rev_mp)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1106
apply (erule rev_mp)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1107
apply (erule trancl_induct, clarify)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1108
apply (blast intro: munion_multirel1_mono r_into_trancl, clarify)
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 15201
diff changeset
  1109
apply (subgoal_tac "y \<in> Mult(A) ")
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1110
 prefer 2
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1111
 apply (blast dest: multirel_type [unfolded multirel_def, THEN subsetD])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1112
apply (subgoal_tac "<K +# y, K +# z> \<in> multirel1 (A, r) ")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1113
prefer 2 apply (blast intro: munion_multirel1_mono)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1114
apply (blast intro: r_into_trancl trancl_trans)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1115
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1116
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1117
lemma munion_multirel_mono1:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1118
     "[|<M, N> \<in> multirel(A, r); K \<in> Mult(A)|] ==> <M +# K, N +# K> \<in> multirel(A, r)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1119
apply (frule multirel_type [THEN subsetD])
59788
6f7b6adac439 prefer local fixes;
wenzelm
parents: 58318
diff changeset
  1120
apply (rule_tac P = "%x. <x,u> \<in> multirel(A, r)" for u in munion_commute [THEN subst])
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 15201
diff changeset
  1121
apply (subst munion_commute [of N])
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1122
apply (rule munion_multirel_mono2)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1123
apply (auto simp add: Mult_iff_multiset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1124
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1125
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1126
lemma munion_multirel_mono:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1127
     "[|<M,K> \<in> multirel(A, r); <N,L> \<in> multirel(A, r)|]
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1128
      ==> <M +# N, K +# L> \<in> multirel(A, r)"
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 15201
diff changeset
  1129
apply (subgoal_tac "M \<in> Mult(A) & N \<in> Mult(A) & K \<in> Mult(A) & L \<in> Mult(A) ")
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1130
prefer 2 apply (blast dest: multirel_type [THEN subsetD])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1131
apply (blast intro: munion_multirel_mono1 multirel_trans munion_multirel_mono2)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1132
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1133
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1134
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59788
diff changeset
  1135
subsection\<open>Ordinal Multisets\<close>
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1136
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1137
(* A \<subseteq> B ==>  field(Memrel(A)) \<subseteq> field(Memrel(B)) *)
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 35112
diff changeset
  1138
lemmas field_Memrel_mono = Memrel_mono [THEN field_mono]
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1139
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1140
(*
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1141
[| Aa \<subseteq> Ba; A \<subseteq> B |] ==>
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1142
multirel(field(Memrel(Aa)), Memrel(A))\<subseteq> multirel(field(Memrel(Ba)), Memrel(B))
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1143
*)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1144
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1145
lemmas multirel_Memrel_mono = multirel_mono [OF field_Memrel_mono Memrel_mono]
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1146
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1147
lemma omultiset_is_multiset [simp]: "omultiset(M) ==> multiset(M)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1148
apply (simp add: omultiset_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1149
apply (auto simp add: Mult_iff_multiset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1150
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1151
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1152
lemma munion_omultiset [simp]: "[| omultiset(M); omultiset(N) |] ==> omultiset(M +# N)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1153
apply (simp add: omultiset_def, clarify)
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
  1154
apply (rule_tac x = "i \<union> ia" in exI)
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1155
apply (simp add: Mult_iff_multiset Ord_Un Un_subset_iff)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1156
apply (blast intro: field_Memrel_mono)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1157
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1158
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1159
lemma mdiff_omultiset [simp]: "omultiset(M) ==> omultiset(M -# N)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1160
apply (simp add: omultiset_def, clarify)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1161
apply (simp add: Mult_iff_multiset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1162
apply (rule_tac x = i in exI)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1163
apply (simp (no_asm_simp))
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1164
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1165
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1166
(** Proving that Memrel is a partial order **)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1167
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1168
lemma irrefl_Memrel: "Ord(i) ==> irrefl(field(Memrel(i)), Memrel(i))"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1169
apply (rule irreflI, clarify)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1170
apply (subgoal_tac "Ord (x) ")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1171
prefer 2 apply (blast intro: Ord_in_Ord)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1172
apply (drule_tac i = x in ltI [THEN lt_irrefl], auto)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1173
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1174
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
  1175
lemma trans_iff_trans_on: "trans(r) \<longleftrightarrow> trans[field(r)](r)"
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1176
by (simp add: trans_on_def trans_def, auto)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1177
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1178
lemma part_ord_Memrel: "Ord(i) ==>part_ord(field(Memrel(i)), Memrel(i))"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1179
apply (simp add: part_ord_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1180
apply (simp (no_asm) add: trans_iff_trans_on [THEN iff_sym])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1181
apply (blast intro: trans_Memrel irrefl_Memrel)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1182
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1183
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1184
(*
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1185
  Ord(i) ==>
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1186
  part_ord(field(Memrel(i))-||>nat-{0}, multirel(field(Memrel(i)), Memrel(i)))
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1187
*)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1188
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 35112
diff changeset
  1189
lemmas part_ord_mless = part_ord_Memrel [THEN part_ord_multirel]
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1190
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1191
(*irreflexivity*)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1192
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1193
lemma mless_not_refl: "~(M <# M)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1194
apply (simp add: mless_def, clarify)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1195
apply (frule multirel_type [THEN subsetD])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1196
apply (drule part_ord_mless)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1197
apply (simp add: part_ord_def irrefl_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1198
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1199
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1200
(* N<N ==> R *)
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 35112
diff changeset
  1201
lemmas mless_irrefl = mless_not_refl [THEN notE, elim!]
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1202
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1203
(*transitivity*)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1204
lemma mless_trans: "[| K <# M; M <# N |] ==> K <# N"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1205
apply (simp add: mless_def, clarify)
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
  1206
apply (rule_tac x = "i \<union> ia" in exI)
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1207
apply (blast dest: multirel_Memrel_mono [OF Un_upper1 Un_upper1, THEN subsetD]
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1208
                   multirel_Memrel_mono [OF Un_upper2 Un_upper2, THEN subsetD]
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1209
        intro: multirel_trans Ord_Un)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1210
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1211
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1212
(*asymmetry*)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1213
lemma mless_not_sym: "M <# N ==> ~ N <# M"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1214
apply clarify
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1215
apply (rule mless_not_refl [THEN notE])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1216
apply (erule mless_trans, assumption)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1217
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1218
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1219
lemma mless_asym: "[| M <# N; ~P ==> N <# M |] ==> P"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1220
by (blast dest: mless_not_sym)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1221
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1222
lemma mle_refl [simp]: "omultiset(M) ==> M <#= M"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1223
by (simp add: mle_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1224
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1225
(*anti-symmetry*)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1226
lemma mle_antisym:
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1227
     "[| M <#= N;  N <#= M |] ==> M = N"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1228
apply (simp add: mle_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1229
apply (blast dest: mless_not_sym)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1230
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1231
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1232
(*transitivity*)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1233
lemma mle_trans: "[| K <#= M; M <#= N |] ==> K <#= N"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1234
apply (simp add: mle_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1235
apply (blast intro: mless_trans)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1236
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1237
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
  1238
lemma mless_le_iff: "M <# N \<longleftrightarrow> (M <#= N & M \<noteq> N)"
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1239
by (simp add: mle_def, auto)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1240
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1241
(** Monotonicity of mless **)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1242
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1243
lemma munion_less_mono2: "[| M <# N; omultiset(K) |] ==> K +# M <# K +# N"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1244
apply (simp add: mless_def omultiset_def, clarify)
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 45602
diff changeset
  1245
apply (rule_tac x = "i \<union> ia" in exI)
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1246
apply (simp add: Mult_iff_multiset Ord_Un Un_subset_iff)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1247
apply (rule munion_multirel_mono2)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1248
 apply (blast intro: multirel_Memrel_mono [THEN subsetD])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1249
apply (simp add: Mult_iff_multiset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1250
apply (blast intro: field_Memrel_mono [THEN subsetD])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1251
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1252
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1253
lemma munion_less_mono1: "[| M <# N; omultiset(K) |] ==> M +# K <# N +# K"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1254
by (force dest: munion_less_mono2 simp add: munion_commute)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1255
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1256
lemma mless_imp_omultiset: "M <# N ==> omultiset(M) & omultiset(N)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1257
by (auto simp add: mless_def omultiset_def dest: multirel_type [THEN subsetD])
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1258
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1259
lemma munion_less_mono: "[| M <# K; N <# L |] ==> M +# N <# K +# L"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1260
apply (frule_tac M = M in mless_imp_omultiset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1261
apply (frule_tac M = N in mless_imp_omultiset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1262
apply (blast intro: munion_less_mono1 munion_less_mono2 mless_trans)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1263
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1264
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1265
(* <#= *)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1266
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1267
lemma mle_imp_omultiset: "M <#= N ==> omultiset(M) & omultiset(N)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1268
by (auto simp add: mle_def mless_imp_omultiset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1269
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1270
lemma mle_mono: "[| M <#= K;  N <#= L |] ==> M +# N <#= K +# L"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1271
apply (frule_tac M = M in mle_imp_omultiset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1272
apply (frule_tac M = N in mle_imp_omultiset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1273
apply (auto simp add: mle_def intro: munion_less_mono1 munion_less_mono2 munion_less_mono)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1274
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1275
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1276
lemma omultiset_0 [iff]: "omultiset(0)"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1277
by (auto simp add: omultiset_def Mult_iff_multiset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1278
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1279
lemma empty_leI [simp]: "omultiset(M) ==> 0 <#= M"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1280
apply (simp add: mle_def mless_def)
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 15201
diff changeset
  1281
apply (subgoal_tac "\<exists>i. Ord (i) & M \<in> Mult(field(Memrel(i))) ")
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1282
 prefer 2 apply (simp add: omultiset_def)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1283
apply (case_tac "M=0", simp_all, clarify)
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 15201
diff changeset
  1284
apply (subgoal_tac "<0 +# 0, 0 +# M> \<in> multirel(field (Memrel(i)), Memrel(i))")
15201
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1285
apply (rule_tac [2] one_step_implies_multirel)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1286
apply (auto simp add: Mult_iff_multiset)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1287
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1288
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1289
lemma munion_upper1: "[| omultiset(M); omultiset(N) |] ==> M <#= M +# N"
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1290
apply (subgoal_tac "M +# 0 <#= M +# N")
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1291
apply (rule_tac [2] mle_mono, auto)
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1292
done
d73f9d49d835 converted ZF/Induct/Multiset to Isar script
paulson
parents: 14046
diff changeset
  1293
12089
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
  1294
end