# 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 \ _) \ is_pideal I" + assumes pid_ax: "is_ideal (I :: ('a::domain) set) \ 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 \ string list" where - "show S = filter S letters" + "show S = filter (\x. x \ 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 \ 'a Heap \ bool" where "Heap_ord = img_ord execute (fun_ord option_ord)" -definition Heap_lub :: "('a Heap \ bool) \ 'a Heap" where +definition Heap_lub :: "'a Heap set \ '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]: "((\x x' y y'. ((x, x'), (y, y')) \ R) <= (\x x' y y'. ((x, x'), (y, y')) \ 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]: "((\x x' y. ((x, x'), y) \ R) <= (\x x' y. ((x, x'), y) \ 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 "\ = n" using i by (simp add: setsum_delta) finally - have "?xs \ natpermute n (k+1)" using xsl unfolding natpermute_def Collect_def mem_def + have "?xs \ natpermute n (k+1)" using xsl unfolding natpermute_def mem_Collect_eq by blast then have "?xs \ ?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 \ nat \ 'a" -definition nonzero_positions :: "(nat \ nat \ 'a::zero) \ nat \ nat \ bool" where +definition nonzero_positions :: "(nat \ nat \ 'a::zero) \ (nat \ nat) set" where "nonzero_positions A = {pos. A (fst pos) (snd pos) ~= 0}" typedef 'a matrix = "{(f::(nat \ nat \ '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: "\l. l \ dom (Mapping.lookup m)" by (auto simp add: is_empty_def fun_eq_iff mem_def keys_def) + then have l: "\l. l \ dom (Mapping.lookup m)" by (auto simp add: is_empty_def keys_def) then have "(let l = SOME l. l \ dom (Mapping.lookup m) in the (Mapping.lookup m l) + (\k \ dom (Mapping.lookup m) - {l}. the (Mapping.lookup m k))) = (\k \ dom (Mapping.lookup m). the (Mapping.lookup m k))"