1.1 --- a/src/HOL/Equiv_Relations.thy Thu Aug 18 13:25:17 2011 +0200
1.2 +++ b/src/HOL/Equiv_Relations.thy Thu Aug 18 13:55:26 2011 +0200
1.3 @@ -164,7 +164,7 @@
1.4
1.5 text{*A congruence-preserving function*}
1.6
1.7 -definition congruent :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
1.8 +definition congruent :: "('a \<times> 'a) set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
1.9 "congruent r f \<longleftrightarrow> (\<forall>(y, z) \<in> r. f y = f z)"
1.10
1.11 lemma congruentI:
1.12 @@ -229,7 +229,7 @@
1.13
1.14 text{*A congruence-preserving function of two arguments*}
1.15
1.16 -definition congruent2 :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<times> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> bool" where
1.17 +definition congruent2 :: "('a \<times> 'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> bool" where
1.18 "congruent2 r1 r2 f \<longleftrightarrow> (\<forall>(y1, z1) \<in> r1. \<forall>(y2, z2) \<in> r2. f y1 y2 = f z1 z2)"
1.19
1.20 lemma congruent2I':
1.21 @@ -413,7 +413,7 @@
1.22
1.23 lemma equivpI:
1.24 "reflp R \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> equivp R"
1.25 - by (auto elim: reflpE sympE transpE simp add: equivp_def mem_def)
1.26 + by (auto simp add: mem_def elim: reflpE sympE transpE simp add: equivp_def)
1.27
1.28 lemma equivpE:
1.29 assumes "equivp R"
2.1 --- a/src/HOL/GCD.thy Thu Aug 18 13:25:17 2011 +0200
2.2 +++ b/src/HOL/GCD.thy Thu Aug 18 13:55:26 2011 +0200
2.3 @@ -531,11 +531,8 @@
2.4
2.5 lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = abs n"
2.6 apply(rule antisym)
2.7 - apply(rule Max_le_iff[THEN iffD2])
2.8 - apply simp
2.9 - apply fastsimp
2.10 - apply (metis Collect_def abs_ge_self dvd_imp_le_int mem_def zle_trans)
2.11 -apply simp
2.12 + apply(rule Max_le_iff [THEN iffD2])
2.13 + apply (auto intro: abs_le_D1 dvd_imp_le_int)
2.14 done
2.15
2.16 lemma gcd_is_Max_divisors_nat:
3.1 --- a/src/HOL/Nat.thy Thu Aug 18 13:25:17 2011 +0200
3.2 +++ b/src/HOL/Nat.thy Thu Aug 18 13:55:26 2011 +0200
3.3 @@ -39,11 +39,20 @@
3.4 Zero_RepI: "Nat Zero_Rep"
3.5 | Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)"
3.6
3.7 -typedef (open Nat) nat = Nat
3.8 - by (rule exI, unfold mem_def, rule Nat.Zero_RepI)
3.9 +typedef (open Nat) nat = "{n. Nat n}"
3.10 + using Nat.Zero_RepI by auto
3.11
3.12 -definition Suc :: "nat => nat" where
3.13 - "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
3.14 +lemma Nat_Rep_Nat:
3.15 + "Nat (Rep_Nat n)"
3.16 + using Rep_Nat by simp
3.17 +
3.18 +lemma Nat_Abs_Nat_inverse:
3.19 + "Nat n \<Longrightarrow> Rep_Nat (Abs_Nat n) = n"
3.20 + using Abs_Nat_inverse by simp
3.21 +
3.22 +lemma Nat_Abs_Nat_inject:
3.23 + "Nat n \<Longrightarrow> Nat m \<Longrightarrow> Abs_Nat n = Abs_Nat m \<longleftrightarrow> n = m"
3.24 + using Abs_Nat_inject by simp
3.25
3.26 instantiation nat :: zero
3.27 begin
3.28 @@ -55,9 +64,11 @@
3.29
3.30 end
3.31
3.32 +definition Suc :: "nat \<Rightarrow> nat" where
3.33 + "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
3.34 +
3.35 lemma Suc_not_Zero: "Suc m \<noteq> 0"
3.36 - by (simp add: Zero_nat_def Suc_def Abs_Nat_inject [unfolded mem_def]
3.37 - Rep_Nat [unfolded mem_def] Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def])
3.38 + by (simp add: Zero_nat_def Suc_def Suc_RepI Zero_RepI Nat_Abs_Nat_inject Suc_Rep_not_Zero_Rep Nat_Rep_Nat)
3.39
3.40 lemma Zero_not_Suc: "0 \<noteq> Suc m"
3.41 by (rule not_sym, rule Suc_not_Zero not_sym)
3.42 @@ -67,12 +78,12 @@
3.43
3.44 rep_datatype "0 \<Colon> nat" Suc
3.45 apply (unfold Zero_nat_def Suc_def)
3.46 - apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
3.47 - apply (erule Rep_Nat [unfolded mem_def, THEN Nat.induct])
3.48 - apply (iprover elim: Abs_Nat_inverse [unfolded mem_def, THEN subst])
3.49 - apply (simp_all add: Abs_Nat_inject [unfolded mem_def] Rep_Nat [unfolded mem_def]
3.50 - Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def]
3.51 - Suc_Rep_not_Zero_Rep [unfolded mem_def, symmetric]
3.52 + apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
3.53 + apply (erule Nat_Rep_Nat [THEN Nat.induct])
3.54 + apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
3.55 + apply (simp_all add: Nat_Abs_Nat_inject Nat_Rep_Nat
3.56 + Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep
3.57 + Suc_Rep_not_Zero_Rep [symmetric]
3.58 Suc_Rep_inject' Rep_Nat_inject)
3.59 done
3.60
4.1 --- a/src/HOL/Nitpick.thy Thu Aug 18 13:25:17 2011 +0200
4.2 +++ b/src/HOL/Nitpick.thy Thu Aug 18 13:55:26 2011 +0200
4.3 @@ -76,19 +76,19 @@
4.4 definition prod :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
4.5 "prod A B = {(a, b). a \<in> A \<and> b \<in> B}"
4.6
4.7 -definition refl' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
4.8 +definition refl' :: "('a \<times> 'a) set \<Rightarrow> bool" where
4.9 "refl' r \<equiv> \<forall>x. (x, x) \<in> r"
4.10
4.11 -definition wf' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
4.12 +definition wf' :: "('a \<times> 'a) set \<Rightarrow> bool" where
4.13 "wf' r \<equiv> acyclic r \<and> (finite r \<or> unknown)"
4.14
4.15 -definition card' :: "('a \<Rightarrow> bool) \<Rightarrow> nat" where
4.16 +definition card' :: "'a set \<Rightarrow> nat" where
4.17 "card' A \<equiv> if finite A then length (SOME xs. set xs = A \<and> distinct xs) else 0"
4.18
4.19 -definition setsum' :: "('a \<Rightarrow> 'b\<Colon>comm_monoid_add) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b" where
4.20 +definition setsum' :: "('a \<Rightarrow> 'b\<Colon>comm_monoid_add) \<Rightarrow> 'a set \<Rightarrow> 'b" where
4.21 "setsum' f A \<equiv> if finite A then listsum (map f (SOME xs. set xs = A \<and> distinct xs)) else 0"
4.22
4.23 -inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool" where
4.24 +inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool" where
4.25 "fold_graph' f z {} z" |
4.26 "\<lbrakk>x \<in> A; fold_graph' f z (A - {x}) y\<rbrakk> \<Longrightarrow> fold_graph' f z A (f x y)"
4.27
5.1 --- a/src/HOL/RealDef.thy Thu Aug 18 13:25:17 2011 +0200
5.2 +++ b/src/HOL/RealDef.thy Thu Aug 18 13:55:26 2011 +0200
5.3 @@ -121,7 +121,7 @@
5.4 subsection {* Cauchy sequences *}
5.5
5.6 definition
5.7 - cauchy :: "(nat \<Rightarrow> rat) set"
5.8 + cauchy :: "(nat \<Rightarrow> rat) \<Rightarrow> bool"
5.9 where
5.10 "cauchy X \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r)"
5.11
6.1 --- a/src/HOL/Relation.thy Thu Aug 18 13:25:17 2011 +0200
6.2 +++ b/src/HOL/Relation.thy Thu Aug 18 13:55:26 2011 +0200
6.3 @@ -133,9 +133,8 @@
6.4 by blast
6.5
6.6 lemma Id_on_def' [nitpick_unfold, code]:
6.7 - "(Id_on (A :: 'a => bool)) = (%(x, y). x = y \<and> A x)"
6.8 -by (auto simp add: fun_eq_iff
6.9 - elim: Id_onE[unfolded mem_def] intro: Id_onI[unfolded mem_def])
6.10 + "Id_on {x. A x} = Collect (\<lambda>(x, y). x = y \<and> A x)"
6.11 +by auto
6.12
6.13 lemma Id_on_subset_Times: "Id_on A \<subseteq> A \<times> A"
6.14 by blast
7.1 --- a/src/HOL/String.thy Thu Aug 18 13:25:17 2011 +0200
7.2 +++ b/src/HOL/String.thy Thu Aug 18 13:55:26 2011 +0200
7.3 @@ -155,7 +155,7 @@
7.4
7.5 subsection {* Strings as dedicated type *}
7.6
7.7 -typedef (open) literal = "UNIV :: string \<Rightarrow> bool"
7.8 +typedef (open) literal = "UNIV :: string set"
7.9 morphisms explode STR ..
7.10
7.11 instantiation literal :: size