# HG changeset patch
# User nipkow
# Date 907924564 -7200
# Node ID 15b7f12ad91903d5a79abf237b5465f359968bdd
# Parent  ac627075b808a1a6e8068aaea26d985737ac5dcb
Multisets at last!

diff -r ac627075b808 -r 15b7f12ad919 src/HOL/Induct/Multiset.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Multiset.ML	Fri Oct 09 11:16:04 1998 +0200
@@ -0,0 +1,448 @@
+(*  Title:      HOL/Induct/Multiset.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+*)
+
+Addsimps [Abs_multiset_inverse,Rep_multiset_inverse,Rep_multiset];
+
+(** Preservation of representing set `multiset' **)
+
+Goalw [multiset_def] "(%a. 0) : multiset";
+by(Simp_tac 1);
+qed "const0_in_multiset";
+Addsimps [const0_in_multiset];
+
+Goalw [multiset_def] "(%b. if b=a then 1 else 0) : multiset";
+by(Simp_tac 1);
+qed "only1_in_multiset";
+Addsimps [only1_in_multiset];
+
+Goalw [multiset_def]
+ "[| M : multiset; N : multiset |] ==> (%a. M a + N a) : multiset";
+by(Asm_full_simp_tac 1);
+bd finite_UnI 1;
+ba 1;
+by(asm_full_simp_tac (simpset() delsimps [finite_Un]addsimps [Un_def]) 1);
+qed "union_preserves_multiset";
+Addsimps [union_preserves_multiset];
+
+Goalw [multiset_def]
+ "[| M : multiset |] ==> (%a. M a - N a) : multiset";
+by(Asm_full_simp_tac 1);
+be (rotate_prems 1 finite_subset) 1;
+by(Auto_tac);
+qed "diff_preserves_multiset";
+Addsimps [diff_preserves_multiset];
+
+(** Injectivity of Rep_multiset **)
+
+Goal "(M = N) = (Rep_multiset M = Rep_multiset N)";
+br iffI 1;
+ by(Asm_simp_tac 1);
+by(dres_inst_tac [("f","Abs_multiset")] arg_cong 1);
+by(Asm_full_simp_tac 1);
+qed "multiset_eq_conv_Rep_eq";
+Addsimps [multiset_eq_conv_Rep_eq];
+Addsimps [expand_fun_eq];
+(*
+Goal
+ "[| f : multiset; g : multiset |] ==> \
+\ (Abs_multiset f = Abs_multiset g) = (!x. f x = g x)";
+br iffI 1;
+ by(dres_inst_tac [("f","Rep_multiset")] arg_cong 1);
+ by(Asm_full_simp_tac 1);
+by(subgoal_tac "f = g" 1);
+ by(Asm_simp_tac 1);
+br ext 1;
+by(Blast_tac 1);
+qed "Abs_multiset_eq";
+Addsimps [Abs_multiset_eq];
+*)
+
+(** Equations **)
+
+(* union *)
+
+Goalw [union_def,empty_def]
+ "M + {#} = M & {#} + M = M";
+by(Simp_tac 1);
+qed "union_empty";
+Addsimps [union_empty];
+
+Goalw [union_def]
+ "(M::'a multiset) + N = N + M";
+by(simp_tac (simpset() addsimps add_ac) 1);
+qed "union_comm";
+
+Goalw [union_def]
+ "((M::'a multiset)+N)+K = M+(N+K)";
+by(simp_tac (simpset() addsimps add_ac) 1);
+qed "union_assoc";
+
+qed_goal "union_lcomm" thy "M+(N+K) = N+((M+K)::'a multiset)"
+ (fn _ => [rtac (union_comm RS trans) 1, rtac (union_assoc RS trans) 1,
+           rtac (union_comm RS arg_cong) 1]);
+
+val union_ac = [union_assoc, union_comm, union_lcomm];
+
+(* diff *)
+
+Goalw [empty_def,diff_def]
+ "M-{#} = M & {#}-M = {#}";
+by(Simp_tac 1);
+qed "diff_empty";
+Addsimps [diff_empty];
+
+Goalw [union_def,diff_def]
+ "M+{#a#}-{#a#} = M";
+by(Simp_tac 1);
+qed "diff_union_inverse2";
+Addsimps [diff_union_inverse2];
+
+(* count *)
+
+Goalw [count_def,empty_def]
+ "count {#} a = 0";
+by(Simp_tac 1);
+qed "count_empty";
+Addsimps [count_empty];
+
+Goalw [count_def,single_def]
+ "count {#b#} a = (if b=a then 1 else 0)";
+by(Simp_tac 1);
+qed "count_single";
+Addsimps [count_single];
+
+Goalw [count_def,union_def]
+ "count (M+N) a = count M a + count N a";
+by(Simp_tac 1);
+qed "count_union";
+Addsimps [count_union];
+
+(* set_of *)
+
+Goalw [set_of_def] "set_of {#} = {}";
+by(Simp_tac 1);
+qed "set_of_empty";
+Addsimps [set_of_empty];
+
+Goalw [set_of_def]
+ "set_of {#b#} = {b}";
+by(Simp_tac 1);
+qed "set_of_single";
+Addsimps [set_of_single];
+
+Goalw [set_of_def]
+ "set_of(M+N) = set_of M Un set_of N";
+by(Auto_tac);
+qed "set_of_union";
+Addsimps [set_of_union];
+
+(* size *)
+
+Goalw [size_def] "size {#} = 0";
+by(Simp_tac 1);
+qed "size_empty";
+Addsimps [size_empty];
+
+Goalw [size_def]
+ "size {#b#} = 1";
+by(Simp_tac 1);
+qed "size_single";
+Addsimps [size_single];
+
+(* Some other day...
+Goalw [size_def]
+ "size (M+N::'a multiset) = size M + size N";
+*)
+
+(* equalities *)
+
+Goalw [single_def,empty_def] "{#a#} ~= {#}  &  {#} ~= {#a#}";
+by(Simp_tac 1);
+qed "single_not_empty";
+Addsimps [single_not_empty];
+
+Goalw [single_def] "({#a#}={#b#}) = (a=b)";
+by(Auto_tac);
+qed "single_eq_single";
+Addsimps [single_eq_single];
+
+Goalw [union_def,empty_def]
+ "(M+N = {#}) = (M = {#} & N = {#})";
+by(Simp_tac 1);
+by(Blast_tac 1);
+qed "union_eq_empty";
+AddIffs [union_eq_empty];
+
+Goalw [union_def,empty_def]
+ "({#} = M+N) = (M = {#} & N = {#})";
+by(Simp_tac 1);
+by(Blast_tac 1);
+qed "empty_eq_union";
+AddIffs [empty_eq_union];
+
+Goalw [union_def]
+ "(M+K = N+K) = (M=(N::'a multiset))";
+by(Simp_tac 1);
+qed "union_right_cancel";
+Addsimps [union_right_cancel];
+
+Goalw [union_def]
+ "(K+M = K+N) = (M=(N::'a multiset))";
+by(Simp_tac 1);
+qed "union_left_cancel";
+Addsimps [union_left_cancel];
+
+Goalw [empty_def,single_def,union_def]
+ "(M+N = {#a#}) = (M={#a#} & N={#} | M={#} & N={#a#})";
+by(simp_tac (simpset() addsimps [add_is_1]) 1);
+by(Blast_tac 1);
+qed "union_is_single";
+
+Goalw [empty_def,single_def,union_def]
+ "({#a#} = M+N) = ({#a#}=M & N={#} | M={#} & {#a#}=N)";
+by(simp_tac (simpset() addsimps [one_is_add]) 1);
+by(blast_tac (claset() addDs [sym]) 1);
+qed "single_is_union";
+
+Goalw [single_def,union_def,diff_def]
+ "(M+{#a#} = N+{#b#}) = (M=N & a=b | M = N-{#a#}+{#b#} & N = M-{#b#}+{#a#})";
+by(Simp_tac 1);
+br conjI 1;
+ by(Force_tac 1);
+by(Clarify_tac 1);
+br conjI 1;
+ by(Blast_tac 1);
+by(Clarify_tac 1);
+br iffI 1;
+ br conjI 1;
+ by(Clarify_tac 1);
+  br conjI 1;
+   by(asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
+(* PROOF FAILED:
+by(Blast_tac 1);
+*)
+  by(Fast_tac 1);
+ by(Asm_simp_tac 1);
+by(Force_tac 1);
+qed "add_eq_conv_diff";
+
+(* FIXME
+val prems = Goal
+ "[| !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> finite F --> P F";
+by(res_inst_tac [("a","F"),("f","%A. if finite A then card A else 0")]
+     measure_induct 1);
+by(Clarify_tac 1);
+brs prems 1;
+ ba 1;
+by(Clarify_tac 1);
+by(subgoal_tac "finite G" 1);
+ by(fast_tac (claset() addDs [finite_subset,order_less_le RS iffD1]) 2);
+be allE 1;
+be impE 1;
+ by(Blast_tac 2);
+by(asm_simp_tac (simpset() addsimps [psubset_card]) 1);
+val lemma = result();
+
+val prems = Goal
+ "[| finite F; !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> P F";
+br (lemma RS mp) 1;
+by (REPEAT(ares_tac prems 1));
+qed "finite_psubset_induct";
+
+Better: use wf_finite_psubset in WF_Rel
+*)
+
+(** Towards the induction rule **)
+
+Goal "finite F ==> (setsum f F = 0) = (!a:F. f a = 0)";
+be finite_induct 1;
+by(Auto_tac);
+qed "setsum_0";
+Addsimps [setsum_0];
+
+Goal "finite F ==> setsum f F = Suc n --> (? a:F. 0 < f a)";
+be finite_induct 1;
+by(Auto_tac);
+by(asm_full_simp_tac
+    (simpset() delsimps [setsum_0] addsimps [setsum_0 RS sym]) 1);
+val lemma = result();
+
+Goal "[| setsum f F = Suc n; finite F |] ==> ? a:F. 0 < f a";
+bd lemma 1;
+by(Fast_tac 1);
+qed "setsum_SucD";
+
+Goal "[| finite F; 0 < f a |] ==> \
+\     setsum (f(a:=f(a)-1)) F = (if a:F then setsum f F - 1 else setsum f F)";
+be finite_induct 1;
+by(Auto_tac);
+ by(asm_simp_tac (simpset() addsimps add_ac) 1);
+by(dres_inst_tac [("a","a")] mk_disjoint_insert 1);
+by(Auto_tac);
+qed "setsum_decr";
+
+val prems = Goalw [multiset_def]
+ "[| P(%a.0); \
+\    !!f b. [| f : multiset; P(f) |] ==> P(f(b:=f(b)+1)) |] \
+\  ==> !f. f : multiset --> setsum f {x. 0 < f x} = n --> P(f)";
+by(induct_tac "n" 1);
+ by(Asm_simp_tac 1);
+ by(Clarify_tac 1);
+ by(subgoal_tac "f = (%a.0)" 1);
+  by(Asm_simp_tac 1);
+  brs prems 1;
+ br ext 1;
+ by(Force_tac 1);
+by(Clarify_tac 1);
+by(forward_tac [setsum_SucD] 1);
+ ba 1;
+by(Clarify_tac 1);
+by(rename_tac "a" 1);
+by(subgoal_tac "finite{x. 0 < (f(a:=f(a)-1)) x}" 1);
+ be (rotate_prems 1 finite_subset) 2;
+ by(Simp_tac 2);
+ by(Blast_tac 2);
+by(subgoal_tac
+   "f = (f(a:=f(a)-1))(a:=(f(a:=f(a)-1))a+1)" 1);
+ br ext 2;
+ by(Asm_simp_tac 2);
+by(EVERY1[etac ssubst, resolve_tac prems]);
+ by(Blast_tac 1);
+by(EVERY[etac allE 1, etac impE 1, etac mp 2]);
+ by(Blast_tac 1);
+by(asm_simp_tac (simpset() addsimps [setsum_decr] delsimps [fun_upd_apply]) 1);
+by(subgoal_tac "{x. x ~= a --> 0 < f x} = {x. 0 < f x}" 1);
+ by(Blast_tac 2);
+by(subgoal_tac "{x. x ~= a & 0 < f x} = {x. 0 < f x} - {a}" 1);
+ by(Blast_tac 2);
+by(asm_simp_tac (simpset() addsimps [le_imp_diff_is_add,setsum_diff1]
+                           addcongs [conj_cong]
+                           addSolver cut_trans_tac) 1);
+val lemma = result();
+
+val major::prems = Goal
+ "[| f : multiset; \
+\    P(%a.0); \
+\    !!f b. [| f : multiset; P(f) |] ==> P(f(b:=f(b)+1)) |] ==> P(f)";
+by(rtac (major RSN (3, lemma RS spec RS mp RS mp)) 1);
+by(REPEAT(ares_tac (refl::prems) 1));
+qed "Rep_multiset_induct";
+
+val [prem1,prem2] = Goalw [union_def,single_def,empty_def]
+ "[| P({#}); !!M x. P(M) ==> P(M + {#x#}) |] ==> P(M)";
+by (rtac (Rep_multiset_inverse RS subst) 1);
+by (rtac (Rep_multiset RS Rep_multiset_induct) 1);
+ by(rtac prem1 1);
+by(Clarify_tac 1);
+by(subgoal_tac
+    "f(b := f b + 1) = (%a. f a + (if a = b then 1 else 0))" 1);
+ by(Simp_tac 2);
+be ssubst 1;
+by(etac (Abs_multiset_inverse RS subst) 1);
+by(etac(simplify (simpset()) prem2)1);
+qed "multiset_induct";
+
+Delsimps [multiset_eq_conv_Rep_eq, expand_fun_eq];
+Delsimps [Abs_multiset_inverse,Rep_multiset_inverse,Rep_multiset];
+
+Goal
+ "(M+{#a#} = N+{#b#}) = (M = N & a = b | (? K. M = K+{#b#} & N = K+{#a#}))";
+by(simp_tac (simpset() addsimps [add_eq_conv_diff]) 1);
+by(Auto_tac);
+qed "add_eq_conv_ex";
+
+(** order **)
+
+Goalw [mult1_def] "(M, {#}) ~: mult1(r)";
+by(Simp_tac 1);
+qed "not_less_empty";
+AddIffs [not_less_empty];
+
+Goalw [mult1_def]
+ "(N,M0 + {#a#}) : mult1(r) = \
+\ ((? M. (M,M0) : mult1(r) & N = M + {#a#}) | \
+\  (? K. (!b. elem K b --> (b,a) : r) & N = M0 + K))";
+br iffI 1;
+ by(asm_full_simp_tac (simpset() addsimps [add_eq_conv_ex]) 1);
+ by(Clarify_tac 1);
+ be disjE 1;
+  by(Blast_tac 1);
+ by(Clarify_tac 1);
+ by(res_inst_tac [("x","Ka+K")] exI 1);
+ by(simp_tac (simpset() addsimps union_ac) 1);
+ by(Blast_tac 1);
+be disjE 1;
+ by(Clarify_tac 1);
+ by(res_inst_tac [("x","aa")] exI 1);
+ by(res_inst_tac [("x","M0+{#a#}")] exI 1);
+ by(res_inst_tac [("x","K")] exI 1);
+ by(simp_tac (simpset() addsimps union_ac) 1);
+by(Blast_tac 1);
+qed "less_add_conv";
+
+Open_locale "MSOrd";
+
+val W_def = thm "W_def";
+
+Goalw [W_def]
+ "[| !b. (b,a) : r --> (!M : W. M+{#b#} : W); M0 : W; \
+\    !M. (M,M0) : mult1(r) --> M+{#a#} : W |] \
+\ ==> M0+{#a#} : W";
+br accI 1;
+by(rename_tac "N" 1);
+by(full_simp_tac (simpset() addsimps [less_add_conv]) 1);
+be disjE 1;
+ by(Blast_tac 1);
+by(Clarify_tac 1);
+by(rotate_tac ~1 1);
+be rev_mp 1;
+by(res_inst_tac [("M","K")] multiset_induct 1);
+ by(Asm_simp_tac 1);
+by(simp_tac (simpset() addsimps [union_assoc RS sym]) 1);
+by(Blast_tac 1);
+qed "lemma1";
+
+Goalw [W_def]
+ "[| !b. (b,a) : r --> (!M : W. M+{#b#} : W); M : W |] ==> M+{#a#} : W";
+be acc_induct 1;
+by(blast_tac (claset() addIs [export lemma1]) 1);
+qed "lemma2";
+
+Goalw [W_def]
+ "wf(r) ==> !M:W. M+{#a#} : W";
+by(eres_inst_tac [("a","a")] wf_induct 1);
+by(blast_tac (claset() addIs [export lemma2]) 1);
+qed "lemma3";
+
+Goalw [W_def] "wf(r) ==> M : W";
+by(res_inst_tac [("M","M")] multiset_induct 1);
+ br accI 1;
+ by(Asm_full_simp_tac 1);
+by(blast_tac (claset() addDs [export lemma3]) 1);
+qed "all_accessible";
+
+Close_locale();
+
+Goal "wf(r) ==> wf(mult1 r)";
+by(blast_tac (claset() addIs [acc_wfI, export all_accessible]) 1);
+qed "wf_mult1";
+
+Goalw [mult_def] "wf(r) ==> wf(mult r)";
+by(blast_tac (claset() addIs [wf_trancl,wf_mult1]) 1);
+qed "wf_mult";
+
+Goalw [mult_def,set_of_def]
+ "(M,N) : mult r = (? I J K. N = I+J & M = I+K & \
+\                            (!k : set_of K. ? j : set_of J. (k,j) : r))";
+br iffI 1;
+
+be trancl_induct 1;
+by(asm_full_simp_tac (simpset() addsimps [mult1_def]) 1);
+
+by(Clarify_tac 1);
+by(res_inst_tac [("x","M0")] exI 1);
+by(Simp_tac 1);
+
diff -r ac627075b808 -r 15b7f12ad919 src/HOL/Induct/Multiset.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Multiset.thy	Fri Oct 09 11:16:04 1998 +0200
@@ -0,0 +1,56 @@
+(*  Title:      HOL/Induct/Multiset.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+
+A definitional theory of multisets,
+including a wellfoundedness proof for the multiset order.
+use_thy"Multiset";
+
+*)
+
+Multiset = Multiset0 + Acc +
+
+typedef
+  'a multiset = "{f :: 'a => nat . finite{x . 0 < f x}}" (multiset_witness)
+
+instance multiset :: (term){ord,plus,minus}
+
+consts
+  "{#}"  :: 'a multiset                        ("{#}")
+  single :: 'a                => 'a multiset   ("{#_#}")
+  count  :: ['a multiset, 'a] => nat
+  set_of :: 'a multiset => 'a set
+
+syntax
+  elem   :: ['a multiset, 'a] => bool
+translations
+  "elem M a" == "0 < count M a"
+
+defs
+  count_def  "count == Rep_multiset"
+  empty_def  "{#}   == Abs_multiset(%a. 0)"
+  single_def "{#a#} == Abs_multiset(%b. if b=a then 1 else 0)"
+  union_def  "M+N   == Abs_multiset(%a. Rep_multiset M a + Rep_multiset N a)"
+  diff_def  "M-N    == Abs_multiset(%a. Rep_multiset M a - Rep_multiset N a)"
+  set_of_def "set_of M == {x. elem M x}"
+  size_def "size (M) == setsum (count M) (set_of M)"
+
+constdefs
+  mult1 :: "('a * 'a)set => ('a multiset * 'a multiset)set"
+ "mult1(r) == {(N,M) . ? a M0 K. M = M0 + {#a#} & N = M0 + K &
+                                 (!b. elem K b --> (b,a) : r)}"
+
+  mult :: "('a * 'a)set => ('a multiset * 'a multiset)set"
+ "mult(r) == (mult1 r)^+"
+
+locale MSOrd =
+  fixes
+    r :: "('a * 'a)set"
+    W :: "'a multiset set"
+
+  assumes
+
+  defines
+    W_def       "W == acc(mult1 r)"
+end
diff -r ac627075b808 -r 15b7f12ad919 src/HOL/Induct/Multiset0.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Multiset0.ML	Fri Oct 09 11:16:04 1998 +0200
@@ -0,0 +1,11 @@
+(*  Title:      HOL/Induct/Multiset0.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+
+This theory merely proves that the representation of multisets is nonempty.
+*)
+
+Goal "(%x.0) : {f. finite {x. 0 < f x}}";
+by(Simp_tac 1);
+qed "multiset_witness";
diff -r ac627075b808 -r 15b7f12ad919 src/HOL/Induct/Multiset0.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Multiset0.thy	Fri Oct 09 11:16:04 1998 +0200
@@ -0,0 +1,9 @@
+(*  Title:      HOL/Induct/Multiset0.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+
+This theory merely proves that the representation of multisets is nonempty.
+*)
+
+Multiset0 = Main
diff -r ac627075b808 -r 15b7f12ad919 src/HOL/Induct/Mutil.ML
--- a/src/HOL/Induct/Mutil.ML	Fri Oct 09 11:15:39 1998 +0200
+++ b/src/HOL/Induct/Mutil.ML	Fri Oct 09 11:16:04 1998 +0200
@@ -152,7 +152,7 @@
 (*Cardinality is smaller because of the two elements fewer*)
 by (rtac less_trans 1);
 by (REPEAT
-    (rtac card_Diff 1 
+    (rtac card_Diff1_less 1 
      THEN asm_simp_tac (simpset() addsimps [tiling_domino_finite]) 1 
      THEN asm_simp_tac (simpset() addsimps [mod_less, evnodd_iff]) 1));
 qed "mutil_not_tiling";
diff -r ac627075b808 -r 15b7f12ad919 src/HOL/Induct/ROOT.ML
--- a/src/HOL/Induct/ROOT.ML	Fri Oct 09 11:15:39 1998 +0200
+++ b/src/HOL/Induct/ROOT.ML	Fri Oct 09 11:16:04 1998 +0200
@@ -14,6 +14,7 @@
 time_use_thy "Comb";
 time_use_thy "Mutil";
 time_use_thy "Acc";
+time_use_thy "Multiset";
 time_use_thy "PropLog";
 time_use_thy "SList";
 time_use_thy "LFilter";