# 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 \<times> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"  where
+definition congruent :: "('a \<times> 'a) set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"  where
   "congruent r f \<longleftrightarrow> (\<forall>(y, z) \<in> r. f y = f z)"
 
 lemma congruentI:
@@ -229,7 +229,7 @@
 
 text{*A congruence-preserving function of two arguments*}
 
-definition congruent2 :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<times> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> bool" where
+definition congruent2 :: "('a \<times> 'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> bool" where
   "congruent2 r1 r2 f \<longleftrightarrow> (\<forall>(y1, z1) \<in> r1. \<forall>(y2, z2) \<in> r2. f y1 y2 = f z1 z2)"
 
 lemma congruent2I':
@@ -413,7 +413,7 @@
 
 lemma equivpI:
   "reflp R \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> 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\<noteq>0 \<Longrightarrow> 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 \<Longrightarrow> 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
 
-definition Suc :: "nat => nat" where
-  "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
+lemma Nat_Rep_Nat:
+  "Nat (Rep_Nat n)"
+  using Rep_Nat by simp
+
+lemma Nat_Abs_Nat_inverse:
+  "Nat n \<Longrightarrow> Rep_Nat (Abs_Nat n) = n"
+  using Abs_Nat_inverse by simp
+
+lemma Nat_Abs_Nat_inject:
+  "Nat n \<Longrightarrow> Nat m \<Longrightarrow> Abs_Nat n = Abs_Nat m \<longleftrightarrow> n = m"
+  using Abs_Nat_inject by simp
 
 instantiation nat :: zero
 begin
@@ -55,9 +64,11 @@
 
 end
 
+definition Suc :: "nat \<Rightarrow> nat" where
+  "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
+
 lemma Suc_not_Zero: "Suc m \<noteq> 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 \<noteq> Suc m"
   by (rule not_sym, rule Suc_not_Zero not_sym)
@@ -67,12 +78,12 @@
 
 rep_datatype "0 \<Colon> 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 \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
 "prod A B = {(a, b). a \<in> A \<and> b \<in> B}"
 
-definition refl' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+definition refl' :: "('a \<times> 'a) set \<Rightarrow> bool" where
 "refl' r \<equiv> \<forall>x. (x, x) \<in> r"
 
-definition wf' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+definition wf' :: "('a \<times> 'a) set \<Rightarrow> bool" where
 "wf' r \<equiv> acyclic r \<and> (finite r \<or> unknown)"
 
-definition card' :: "('a \<Rightarrow> bool) \<Rightarrow> nat" where
+definition card' :: "'a set \<Rightarrow> nat" where
 "card' A \<equiv> if finite A then length (SOME xs. set xs = A \<and> distinct xs) else 0"
 
-definition setsum' :: "('a \<Rightarrow> 'b\<Colon>comm_monoid_add) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b" where
+definition setsum' :: "('a \<Rightarrow> 'b\<Colon>comm_monoid_add) \<Rightarrow> 'a set \<Rightarrow> 'b" where
 "setsum' f A \<equiv> if finite A then listsum (map f (SOME xs. set xs = A \<and> distinct xs)) else 0"
 
-inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool" where
+inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool" where
 "fold_graph' f z {} z" |
 "\<lbrakk>x \<in> A; fold_graph' f z (A - {x}) y\<rbrakk> \<Longrightarrow> 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 \<Rightarrow> rat) set"
+  cauchy :: "(nat \<Rightarrow> rat) \<Rightarrow> bool"
 where
   "cauchy X \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < 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 \<and> 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 (\<lambda>(x, y). x = y \<and> A x)"
+by auto
 
 lemma Id_on_subset_Times: "Id_on A \<subseteq> A \<times> 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 \<Rightarrow> bool"
+typedef (open) literal = "UNIV :: string set"
   morphisms explode STR ..
 
 instantiation literal :: size