# HG changeset patch
# User huffman
# Date 1313185550 25200
# Node ID d1d79f0e1ea6db45c296e9c29cb26e8ea975b149
# Parent  75ea0e390a92799a31dfb4073e0dc41930301de2
make more HOL theories work with separate set type

diff -r 75ea0e390a92 -r d1d79f0e1ea6 src/HOL/Algebra/abstract/Ideal2.thy
--- a/src/HOL/Algebra/abstract/Ideal2.thy	Fri Aug 12 09:17:30 2011 -0700
+++ b/src/HOL/Algebra/abstract/Ideal2.thy	Fri Aug 12 14:45:50 2011 -0700
@@ -25,7 +25,7 @@
 text {* Principle ideal domains *}
 
 class pid =
-  assumes pid_ax: "is_ideal (I :: 'a::domain \<Rightarrow> _) \<Longrightarrow> is_pideal I"
+  assumes pid_ax: "is_ideal (I :: ('a::domain) set) \<Longrightarrow> is_pideal I"
 
 (* is_ideal *)
 
diff -r 75ea0e390a92 -r d1d79f0e1ea6 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Fri Aug 12 09:17:30 2011 -0700
+++ b/src/HOL/Auth/Message.thy	Fri Aug 12 14:45:50 2011 -0700
@@ -841,7 +841,7 @@
 apply (erule analz.induct, auto)
 apply (blast dest:parts.Body)
 apply (blast dest: parts.Body)
-apply (metis Un_absorb2 keyfree_KeyE mem_def parts_Un parts_keyfree sup1I2)
+apply (metis Un_absorb2 keyfree_KeyE parts_Un parts_keyfree UnI2)
 done
 
 subsection{*Tactics useful for many protocol proofs*}
diff -r 75ea0e390a92 -r d1d79f0e1ea6 src/HOL/IMP/Util.thy
--- a/src/HOL/IMP/Util.thy	Fri Aug 12 09:17:30 2011 -0700
+++ b/src/HOL/IMP/Util.thy	Fri Aug 12 14:45:50 2011 -0700
@@ -22,7 +22,7 @@
 
 definition 
   "show" :: "string set \<Rightarrow> string list" where
-  "show S = filter S letters" 
+  "show S = filter (\<lambda>x. x \<in> S) letters" 
 
 value "show {''x'', ''z''}"
 
diff -r 75ea0e390a92 -r d1d79f0e1ea6 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Aug 12 09:17:30 2011 -0700
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Aug 12 14:45:50 2011 -0700
@@ -411,7 +411,7 @@
 definition Heap_ord :: "'a Heap \<Rightarrow> 'a Heap \<Rightarrow> bool" where
   "Heap_ord = img_ord execute (fun_ord option_ord)"
 
-definition Heap_lub :: "('a Heap \<Rightarrow> bool) \<Rightarrow> 'a Heap" where
+definition Heap_lub :: "'a Heap set \<Rightarrow> 'a Heap" where
   "Heap_lub = img_lub execute Heap (fun_lub (flat_lub None))"
 
 interpretation heap!: partial_function_definitions Heap_ord Heap_lub
diff -r 75ea0e390a92 -r d1d79f0e1ea6 src/HOL/Induct/Com.thy
--- a/src/HOL/Induct/Com.thy	Fri Aug 12 09:17:30 2011 -0700
+++ b/src/HOL/Induct/Com.thy	Fri Aug 12 14:45:50 2011 -0700
@@ -84,11 +84,13 @@
 
 lemma [pred_set_conv]:
   "((\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> R) <= (\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> S)) = (R <= S)"
-  by (auto simp add: le_fun_def le_bool_def mem_def)
+  unfolding subset_eq
+  by (auto simp add: le_fun_def le_bool_def)
 
 lemma [pred_set_conv]:
   "((\<lambda>x x' y. ((x, x'), y) \<in> R) <= (\<lambda>x x' y. ((x, x'), y) \<in> S)) = (R <= S)"
-  by (auto simp add: le_fun_def le_bool_def mem_def)
+  unfolding subset_eq
+  by (auto simp add: le_fun_def le_bool_def)
 
 text{*Command execution is functional (deterministic) provided evaluation is*}
 theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)"
diff -r 75ea0e390a92 -r d1d79f0e1ea6 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Fri Aug 12 09:17:30 2011 -0700
+++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Aug 12 14:45:50 2011 -0700
@@ -1436,7 +1436,7 @@
       apply (rule setsum_cong2) by (simp del: replicate.simps)
     also have "\<dots> = n" using i by (simp add: setsum_delta)
     finally
-    have "?xs \<in> natpermute n (k+1)" using xsl unfolding natpermute_def Collect_def mem_def
+    have "?xs \<in> natpermute n (k+1)" using xsl unfolding natpermute_def mem_Collect_eq
       by blast
     then have "?xs \<in> ?A"  using nxs  by blast}
   ultimately show ?thesis by auto
diff -r 75ea0e390a92 -r d1d79f0e1ea6 src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Fri Aug 12 09:17:30 2011 -0700
+++ b/src/HOL/Matrix/Matrix.thy	Fri Aug 12 14:45:50 2011 -0700
@@ -8,7 +8,7 @@
 
 type_synonym 'a infmatrix = "nat \<Rightarrow> nat \<Rightarrow> 'a"
 
-definition nonzero_positions :: "(nat \<Rightarrow> nat \<Rightarrow> 'a::zero) \<Rightarrow> nat \<times> nat \<Rightarrow> bool" where
+definition nonzero_positions :: "(nat \<Rightarrow> nat \<Rightarrow> 'a::zero) \<Rightarrow> (nat \<times> nat) set" where
   "nonzero_positions A = {pos. A (fst pos) (snd pos) ~= 0}"
 
 typedef 'a matrix = "{(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
diff -r 75ea0e390a92 -r d1d79f0e1ea6 src/HOL/ex/Execute_Choice.thy
--- a/src/HOL/ex/Execute_Choice.thy	Fri Aug 12 09:17:30 2011 -0700
+++ b/src/HOL/ex/Execute_Choice.thy	Fri Aug 12 14:45:50 2011 -0700
@@ -26,7 +26,7 @@
   case True then show ?thesis by (simp add: is_empty_def keys_def valuesum_def)
 next
   case False
-  then have l: "\<exists>l. l \<in> dom (Mapping.lookup m)" by (auto simp add: is_empty_def fun_eq_iff mem_def keys_def)
+  then have l: "\<exists>l. l \<in> dom (Mapping.lookup m)" by (auto simp add: is_empty_def keys_def)
   then have "(let l = SOME l. l \<in> dom (Mapping.lookup m) in
      the (Mapping.lookup m l) + (\<Sum>k \<in> dom (Mapping.lookup m) - {l}. the (Mapping.lookup m k))) =
        (\<Sum>k \<in> dom (Mapping.lookup m). the (Mapping.lookup m k))"