# HG changeset patch # User haftmann # Date 1313668526 -7200 # Node ID 1220ecb81e8fd59c9fd3d04970fc93a4ad2e4d91 # Parent bcb69653357960b71ae26cedae2913ac1b454d66 observe distinction between sets and predicates more properly diff -r bcb696533579 -r 1220ecb81e8f src/HOL/Equiv_Relations.thy --- a/src/HOL/Equiv_Relations.thy Thu Aug 18 13:25:17 2011 +0200 +++ b/src/HOL/Equiv_Relations.thy Thu Aug 18 13:55:26 2011 +0200 @@ -164,7 +164,7 @@ text{*A congruence-preserving function*} -definition congruent :: "('a \ 'a \ bool) \ ('a \ 'b) \ bool" where +definition congruent :: "('a \ 'a) set \ ('a \ 'b) \ bool" where "congruent r f \ (\(y, z) \ r. f y = f z)" lemma congruentI: @@ -229,7 +229,7 @@ text{*A congruence-preserving function of two arguments*} -definition congruent2 :: "('a \ 'a \ bool) \ ('b \ 'b \ bool) \ ('a \ 'b \ 'c) \ bool" where +definition congruent2 :: "('a \ 'a) set \ ('b \ 'b) set \ ('a \ 'b \ 'c) \ bool" where "congruent2 r1 r2 f \ (\(y1, z1) \ r1. \(y2, z2) \ r2. f y1 y2 = f z1 z2)" lemma congruent2I': @@ -413,7 +413,7 @@ lemma equivpI: "reflp R \ symp R \ transp R \ equivp R" - by (auto elim: reflpE sympE transpE simp add: equivp_def mem_def) + by (auto simp add: mem_def elim: reflpE sympE transpE simp add: equivp_def) lemma equivpE: assumes "equivp R" diff -r bcb696533579 -r 1220ecb81e8f src/HOL/GCD.thy --- a/src/HOL/GCD.thy Thu Aug 18 13:25:17 2011 +0200 +++ b/src/HOL/GCD.thy Thu Aug 18 13:55:26 2011 +0200 @@ -531,11 +531,8 @@ lemma Max_divisors_self_int[simp]: "n\0 \ Max{d::int. d dvd n} = abs n" apply(rule antisym) - apply(rule Max_le_iff[THEN iffD2]) - apply simp - apply fastsimp - apply (metis Collect_def abs_ge_self dvd_imp_le_int mem_def zle_trans) -apply simp + apply(rule Max_le_iff [THEN iffD2]) + apply (auto intro: abs_le_D1 dvd_imp_le_int) done lemma gcd_is_Max_divisors_nat: diff -r bcb696533579 -r 1220ecb81e8f src/HOL/Nat.thy --- a/src/HOL/Nat.thy Thu Aug 18 13:25:17 2011 +0200 +++ b/src/HOL/Nat.thy Thu Aug 18 13:55:26 2011 +0200 @@ -39,11 +39,20 @@ Zero_RepI: "Nat Zero_Rep" | Suc_RepI: "Nat i \ Nat (Suc_Rep i)" -typedef (open Nat) nat = Nat - by (rule exI, unfold mem_def, rule Nat.Zero_RepI) +typedef (open Nat) nat = "{n. Nat n}" + using Nat.Zero_RepI by auto + +lemma Nat_Rep_Nat: + "Nat (Rep_Nat n)" + using Rep_Nat by simp -definition Suc :: "nat => nat" where - "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))" +lemma Nat_Abs_Nat_inverse: + "Nat n \ Rep_Nat (Abs_Nat n) = n" + using Abs_Nat_inverse by simp + +lemma Nat_Abs_Nat_inject: + "Nat n \ Nat m \ Abs_Nat n = Abs_Nat m \ n = m" + using Abs_Nat_inject by simp instantiation nat :: zero begin @@ -55,9 +64,11 @@ end +definition Suc :: "nat \ nat" where + "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))" + lemma Suc_not_Zero: "Suc m \ 0" - by (simp add: Zero_nat_def Suc_def Abs_Nat_inject [unfolded mem_def] - Rep_Nat [unfolded mem_def] Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def]) + by (simp add: Zero_nat_def Suc_def Suc_RepI Zero_RepI Nat_Abs_Nat_inject Suc_Rep_not_Zero_Rep Nat_Rep_Nat) lemma Zero_not_Suc: "0 \ Suc m" by (rule not_sym, rule Suc_not_Zero not_sym) @@ -67,12 +78,12 @@ rep_datatype "0 \ nat" Suc apply (unfold Zero_nat_def Suc_def) - apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *} - apply (erule Rep_Nat [unfolded mem_def, THEN Nat.induct]) - apply (iprover elim: Abs_Nat_inverse [unfolded mem_def, THEN subst]) - apply (simp_all add: Abs_Nat_inject [unfolded mem_def] Rep_Nat [unfolded mem_def] - Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def] - Suc_Rep_not_Zero_Rep [unfolded mem_def, symmetric] + apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *} + apply (erule Nat_Rep_Nat [THEN Nat.induct]) + apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst]) + apply (simp_all add: Nat_Abs_Nat_inject Nat_Rep_Nat + Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep + Suc_Rep_not_Zero_Rep [symmetric] Suc_Rep_inject' Rep_Nat_inject) done diff -r bcb696533579 -r 1220ecb81e8f src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Thu Aug 18 13:25:17 2011 +0200 +++ b/src/HOL/Nitpick.thy Thu Aug 18 13:55:26 2011 +0200 @@ -76,19 +76,19 @@ definition prod :: "'a set \ 'b set \ ('a \ 'b) set" where "prod A B = {(a, b). a \ A \ b \ B}" -definition refl' :: "('a \ 'a \ bool) \ bool" where +definition refl' :: "('a \ 'a) set \ bool" where "refl' r \ \x. (x, x) \ r" -definition wf' :: "('a \ 'a \ bool) \ bool" where +definition wf' :: "('a \ 'a) set \ bool" where "wf' r \ acyclic r \ (finite r \ unknown)" -definition card' :: "('a \ bool) \ nat" where +definition card' :: "'a set \ nat" where "card' A \ if finite A then length (SOME xs. set xs = A \ distinct xs) else 0" -definition setsum' :: "('a \ 'b\comm_monoid_add) \ ('a \ bool) \ 'b" where +definition setsum' :: "('a \ 'b\comm_monoid_add) \ 'a set \ 'b" where "setsum' f A \ if finite A then listsum (map f (SOME xs. set xs = A \ distinct xs)) else 0" -inductive fold_graph' :: "('a \ 'b \ 'b) \ 'b \ ('a \ bool) \ 'b \ bool" where +inductive fold_graph' :: "('a \ 'b \ 'b) \ 'b \ 'a set \ 'b \ bool" where "fold_graph' f z {} z" | "\x \ A; fold_graph' f z (A - {x}) y\ \ fold_graph' f z A (f x y)" diff -r bcb696533579 -r 1220ecb81e8f src/HOL/RealDef.thy --- a/src/HOL/RealDef.thy Thu Aug 18 13:25:17 2011 +0200 +++ b/src/HOL/RealDef.thy Thu Aug 18 13:55:26 2011 +0200 @@ -121,7 +121,7 @@ subsection {* Cauchy sequences *} definition - cauchy :: "(nat \ rat) set" + cauchy :: "(nat \ rat) \ bool" where "cauchy X \ (\r>0. \k. \m\k. \n\k. \X m - X n\ < r)" diff -r bcb696533579 -r 1220ecb81e8f src/HOL/Relation.thy --- a/src/HOL/Relation.thy Thu Aug 18 13:25:17 2011 +0200 +++ b/src/HOL/Relation.thy Thu Aug 18 13:55:26 2011 +0200 @@ -133,9 +133,8 @@ by blast lemma Id_on_def' [nitpick_unfold, code]: - "(Id_on (A :: 'a => bool)) = (%(x, y). x = y \ A x)" -by (auto simp add: fun_eq_iff - elim: Id_onE[unfolded mem_def] intro: Id_onI[unfolded mem_def]) + "Id_on {x. A x} = Collect (\(x, y). x = y \ A x)" +by auto lemma Id_on_subset_Times: "Id_on A \ A \ A" by blast diff -r bcb696533579 -r 1220ecb81e8f src/HOL/String.thy --- a/src/HOL/String.thy Thu Aug 18 13:25:17 2011 +0200 +++ b/src/HOL/String.thy Thu Aug 18 13:55:26 2011 +0200 @@ -155,7 +155,7 @@ subsection {* Strings as dedicated type *} -typedef (open) literal = "UNIV :: string \ bool" +typedef (open) literal = "UNIV :: string set" morphisms explode STR .. instantiation literal :: size