merged
authorwenzelm
Thu, 04 Jun 2009 22:08:20 +0200
changeset 31442 b861e58086ab
parent 31441 428e4caf2299 (diff)
parent 31437 70309dc3deac (current diff)
child 31443 c23663825e23
merged
src/Pure/Concurrent/ROOT.ML
src/Pure/General/ROOT.ML
src/Pure/Isar/ROOT.ML
src/Pure/ML-Systems/install_pp_polyml-experimental.ML
src/Pure/ProofGeneral/ROOT.ML
src/Pure/Tools/ROOT.ML
--- a/src/HOL/Finite_Set.thy	Thu Jun 04 22:02:33 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Thu Jun 04 22:08:20 2009 +0200
@@ -457,6 +457,18 @@
 by(blast intro: finite_subset[OF subset_Pow_Union])
 
 
+lemma finite_subset_image:
+  assumes "finite B"
+  shows "B \<subseteq> f ` A \<Longrightarrow> \<exists>C\<subseteq>A. finite C \<and> B = f ` C"
+using assms proof(induct)
+  case empty thus ?case by simp
+next
+  case insert thus ?case
+    by (clarsimp simp del: image_insert simp add: image_insert[symmetric])
+       blast
+qed
+
+
 subsection {* Class @{text finite}  *}
 
 setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
@@ -1333,6 +1345,10 @@
 apply (auto simp add: insert_Diff_if add_ac)
 done
 
+lemma setsum_diff1_ring: assumes "finite A" "a \<in> A"
+  shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)"
+unfolding setsum_diff1'[OF assms] by auto
+
 (* By Jeremy Siek: *)
 
 lemma setsum_diff_nat: 
--- a/src/HOL/Fun.thy	Thu Jun 04 22:02:33 2009 +0200
+++ b/src/HOL/Fun.thy	Thu Jun 04 22:08:20 2009 +0200
@@ -250,6 +250,10 @@
 lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A"
 by (simp add: bij_betw_def)
 
+lemma bij_betw_trans:
+  "bij_betw f A B \<Longrightarrow> bij_betw g B C \<Longrightarrow> bij_betw (g o f) A C"
+by(auto simp add:bij_betw_def comp_inj_on)
+
 lemma bij_betw_inv: assumes "bij_betw f A B" shows "EX g. bij_betw g B A"
 proof -
   have i: "inj_on f A" and s: "f ` A = B"
@@ -300,6 +304,9 @@
 apply (blast del: subsetI intro: vimage_subsetI vimage_subsetD)
 done
 
+lemma inj_on_Un_image_eq_iff: "inj_on f (A \<union> B) \<Longrightarrow> f ` A = f ` B \<longleftrightarrow> A = B"
+by(blast dest: inj_onD)
+
 lemma inj_on_image_Int:
    "[| inj_on f C;  A<=C;  B<=C |] ==> f`(A Int B) = f`A Int f`B"
 apply (simp add: inj_on_def, blast)
--- a/src/HOL/Set.thy	Thu Jun 04 22:02:33 2009 +0200
+++ b/src/HOL/Set.thy	Thu Jun 04 22:08:20 2009 +0200
@@ -1344,13 +1344,16 @@
 by auto
 
 lemma image_image: "f ` (g ` A) = (\<lambda>x. f (g x)) ` A"
-  by blast
+by blast
 
 lemma insert_image [simp]: "x \<in> A ==> insert (f x) (f`A) = f`A"
-  by blast
+by blast
 
 lemma image_is_empty [iff]: "(f`A = {}) = (A = {})"
-  by blast
+by blast
+
+lemma empty_is_image[iff]: "({} = f ` A) = (A = {})"
+by blast
 
 
 lemma image_Collect [noatp]: "f ` {x. P x} = {f x | x. P x}"
--- a/src/HOL/SetInterval.thy	Thu Jun 04 22:02:33 2009 +0200
+++ b/src/HOL/SetInterval.thy	Thu Jun 04 22:08:20 2009 +0200
@@ -468,7 +468,6 @@
 lemma card_greaterThanLessThan [simp]: "card {l<..<u} = u - Suc l"
   by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp)
 
-
 lemma ex_bij_betw_nat_finite:
   "finite M \<Longrightarrow> \<exists>h. bij_betw h {0..<card M} M"
 apply(drule finite_imp_nat_seg_image_inj_on)
@@ -479,6 +478,17 @@
   "finite M \<Longrightarrow> \<exists>h. bij_betw h M {0..<card M}"
 by (blast dest: ex_bij_betw_nat_finite bij_betw_inv)
 
+lemma finite_same_card_bij:
+  "finite A \<Longrightarrow> finite B \<Longrightarrow> card A = card B \<Longrightarrow> EX h. bij_betw h A B"
+apply(drule ex_bij_betw_finite_nat)
+apply(drule ex_bij_betw_nat_finite)
+apply(auto intro!:bij_betw_trans)
+done
+
+lemma ex_bij_betw_nat_finite_1:
+  "finite M \<Longrightarrow> \<exists>h. bij_betw h {1 .. card M} M"
+by (rule finite_same_card_bij) auto
+
 
 subsection {* Intervals of integers *}
 
--- a/src/HOL/ex/predicate_compile.ML	Thu Jun 04 22:02:33 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Thu Jun 04 22:08:20 2009 +0200
@@ -143,7 +143,7 @@
                nparams = Symtab.empty};
   val copy = I;
   val extend = I;
-  fun merge _ r = {names = PredModetab.merge (op =) (pairself #names r),
+  fun merge _ (r : T * T) = {names = PredModetab.merge (op =) (pairself #names r),
                    modes = Symtab.merge (op =) (pairself #modes r),
                    function_defs = Symtab.merge Thm.eq_thm (pairself #function_defs r),
                    function_intros = Symtab.merge Thm.eq_thm (pairself #function_intros r),