make more HOL theories work with separate set type
authorhuffman
Fri Aug 12 14:45:50 2011 -0700 (2011-08-12)
changeset 44174d1d79f0e1ea6
parent 44171 75ea0e390a92
child 44175 28cdf93076f4
make more HOL theories work with separate set type
src/HOL/Algebra/abstract/Ideal2.thy
src/HOL/Auth/Message.thy
src/HOL/IMP/Util.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Induct/Com.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Matrix/Matrix.thy
src/HOL/ex/Execute_Choice.thy
     1.1 --- a/src/HOL/Algebra/abstract/Ideal2.thy	Fri Aug 12 09:17:30 2011 -0700
     1.2 +++ b/src/HOL/Algebra/abstract/Ideal2.thy	Fri Aug 12 14:45:50 2011 -0700
     1.3 @@ -25,7 +25,7 @@
     1.4  text {* Principle ideal domains *}
     1.5  
     1.6  class pid =
     1.7 -  assumes pid_ax: "is_ideal (I :: 'a::domain \<Rightarrow> _) \<Longrightarrow> is_pideal I"
     1.8 +  assumes pid_ax: "is_ideal (I :: ('a::domain) set) \<Longrightarrow> is_pideal I"
     1.9  
    1.10  (* is_ideal *)
    1.11  
     2.1 --- a/src/HOL/Auth/Message.thy	Fri Aug 12 09:17:30 2011 -0700
     2.2 +++ b/src/HOL/Auth/Message.thy	Fri Aug 12 14:45:50 2011 -0700
     2.3 @@ -841,7 +841,7 @@
     2.4  apply (erule analz.induct, auto)
     2.5  apply (blast dest:parts.Body)
     2.6  apply (blast dest: parts.Body)
     2.7 -apply (metis Un_absorb2 keyfree_KeyE mem_def parts_Un parts_keyfree sup1I2)
     2.8 +apply (metis Un_absorb2 keyfree_KeyE parts_Un parts_keyfree UnI2)
     2.9  done
    2.10  
    2.11  subsection{*Tactics useful for many protocol proofs*}
     3.1 --- a/src/HOL/IMP/Util.thy	Fri Aug 12 09:17:30 2011 -0700
     3.2 +++ b/src/HOL/IMP/Util.thy	Fri Aug 12 14:45:50 2011 -0700
     3.3 @@ -22,7 +22,7 @@
     3.4  
     3.5  definition 
     3.6    "show" :: "string set \<Rightarrow> string list" where
     3.7 -  "show S = filter S letters" 
     3.8 +  "show S = filter (\<lambda>x. x \<in> S) letters" 
     3.9  
    3.10  value "show {''x'', ''z''}"
    3.11  
     4.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Aug 12 09:17:30 2011 -0700
     4.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Aug 12 14:45:50 2011 -0700
     4.3 @@ -411,7 +411,7 @@
     4.4  definition Heap_ord :: "'a Heap \<Rightarrow> 'a Heap \<Rightarrow> bool" where
     4.5    "Heap_ord = img_ord execute (fun_ord option_ord)"
     4.6  
     4.7 -definition Heap_lub :: "('a Heap \<Rightarrow> bool) \<Rightarrow> 'a Heap" where
     4.8 +definition Heap_lub :: "'a Heap set \<Rightarrow> 'a Heap" where
     4.9    "Heap_lub = img_lub execute Heap (fun_lub (flat_lub None))"
    4.10  
    4.11  interpretation heap!: partial_function_definitions Heap_ord Heap_lub
     5.1 --- a/src/HOL/Induct/Com.thy	Fri Aug 12 09:17:30 2011 -0700
     5.2 +++ b/src/HOL/Induct/Com.thy	Fri Aug 12 14:45:50 2011 -0700
     5.3 @@ -84,11 +84,13 @@
     5.4  
     5.5  lemma [pred_set_conv]:
     5.6    "((\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> R) <= (\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> S)) = (R <= S)"
     5.7 -  by (auto simp add: le_fun_def le_bool_def mem_def)
     5.8 +  unfolding subset_eq
     5.9 +  by (auto simp add: le_fun_def le_bool_def)
    5.10  
    5.11  lemma [pred_set_conv]:
    5.12    "((\<lambda>x x' y. ((x, x'), y) \<in> R) <= (\<lambda>x x' y. ((x, x'), y) \<in> S)) = (R <= S)"
    5.13 -  by (auto simp add: le_fun_def le_bool_def mem_def)
    5.14 +  unfolding subset_eq
    5.15 +  by (auto simp add: le_fun_def le_bool_def)
    5.16  
    5.17  text{*Command execution is functional (deterministic) provided evaluation is*}
    5.18  theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)"
     6.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Fri Aug 12 09:17:30 2011 -0700
     6.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Aug 12 14:45:50 2011 -0700
     6.3 @@ -1436,7 +1436,7 @@
     6.4        apply (rule setsum_cong2) by (simp del: replicate.simps)
     6.5      also have "\<dots> = n" using i by (simp add: setsum_delta)
     6.6      finally
     6.7 -    have "?xs \<in> natpermute n (k+1)" using xsl unfolding natpermute_def Collect_def mem_def
     6.8 +    have "?xs \<in> natpermute n (k+1)" using xsl unfolding natpermute_def mem_Collect_eq
     6.9        by blast
    6.10      then have "?xs \<in> ?A"  using nxs  by blast}
    6.11    ultimately show ?thesis by auto
     7.1 --- a/src/HOL/Matrix/Matrix.thy	Fri Aug 12 09:17:30 2011 -0700
     7.2 +++ b/src/HOL/Matrix/Matrix.thy	Fri Aug 12 14:45:50 2011 -0700
     7.3 @@ -8,7 +8,7 @@
     7.4  
     7.5  type_synonym 'a infmatrix = "nat \<Rightarrow> nat \<Rightarrow> 'a"
     7.6  
     7.7 -definition nonzero_positions :: "(nat \<Rightarrow> nat \<Rightarrow> 'a::zero) \<Rightarrow> nat \<times> nat \<Rightarrow> bool" where
     7.8 +definition nonzero_positions :: "(nat \<Rightarrow> nat \<Rightarrow> 'a::zero) \<Rightarrow> (nat \<times> nat) set" where
     7.9    "nonzero_positions A = {pos. A (fst pos) (snd pos) ~= 0}"
    7.10  
    7.11  typedef 'a matrix = "{(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
     8.1 --- a/src/HOL/ex/Execute_Choice.thy	Fri Aug 12 09:17:30 2011 -0700
     8.2 +++ b/src/HOL/ex/Execute_Choice.thy	Fri Aug 12 14:45:50 2011 -0700
     8.3 @@ -26,7 +26,7 @@
     8.4    case True then show ?thesis by (simp add: is_empty_def keys_def valuesum_def)
     8.5  next
     8.6    case False
     8.7 -  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)
     8.8 +  then have l: "\<exists>l. l \<in> dom (Mapping.lookup m)" by (auto simp add: is_empty_def keys_def)
     8.9    then have "(let l = SOME l. l \<in> dom (Mapping.lookup m) in
    8.10       the (Mapping.lookup m l) + (\<Sum>k \<in> dom (Mapping.lookup m) - {l}. the (Mapping.lookup m k))) =
    8.11         (\<Sum>k \<in> dom (Mapping.lookup m). the (Mapping.lookup m k))"