observe distinction between sets and predicates more properly
authorhaftmann
Thu Aug 18 13:55:26 2011 +0200 (2011-08-18)
changeset 442781220ecb81e8f
parent 44277 bcb696533579
child 44279 7496258e44e4
observe distinction between sets and predicates more properly
src/HOL/Equiv_Relations.thy
src/HOL/GCD.thy
src/HOL/Nat.thy
src/HOL/Nitpick.thy
src/HOL/RealDef.thy
src/HOL/Relation.thy
src/HOL/String.thy
     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 +lemma Nat_Rep_Nat:
    3.13 +  "Nat (Rep_Nat n)"
    3.14 +  using Rep_Nat by simp
    3.15  
    3.16 -definition Suc :: "nat => nat" where
    3.17 -  "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
    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