# HG changeset patch
# User Andreas Lochbihler
# Date 1338532346 -7200
# Node ID 60bcc6cf17d6cacc73f3662b2c3e9879c680a0a5
# Parent  9bc78a08ff0a3e7c03d073f5e889feda7a1b570e# Parent  72acba14c12bab6359b7650d22e71d6a7dde9079
merged

diff -r 9bc78a08ff0a -r 60bcc6cf17d6 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu May 31 17:10:43 2012 +0200
+++ b/src/HOL/Int.thy	Fri Jun 01 08:32:26 2012 +0200
@@ -6,193 +6,106 @@
 header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} 
 
 theory Int
-imports Equiv_Relations Wellfounded
+imports Equiv_Relations Wellfounded Quotient
 uses
   ("Tools/int_arith.ML")
 begin
 
-subsection {* The equivalence relation underlying the integers *}
+subsection {* Definition of integers as a quotient type *}
 
-definition intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set" where
-  "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
+definition intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" where
+  "intrel = (\<lambda>(x, y) (u, v). x + v = u + y)"
+
+lemma intrel_iff [simp]: "intrel (x, y) (u, v) \<longleftrightarrow> x + v = u + y"
+  by (simp add: intrel_def)
 
-definition "Integ = UNIV//intrel"
-
-typedef (open) int = Integ
+quotient_type int = "nat \<times> nat" / "intrel"
   morphisms Rep_Integ Abs_Integ
-  unfolding Integ_def by (auto simp add: quotient_def)
+proof (rule equivpI)
+  show "reflp intrel"
+    unfolding reflp_def by auto
+  show "symp intrel"
+    unfolding symp_def by auto
+  show "transp intrel"
+    unfolding transp_def by auto
+qed
 
-instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
+lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]:
+     "(!!x y. z = Abs_Integ (x, y) ==> P) ==> P"
+by (induct z) auto
+
+subsection {* Integers form a commutative ring *}
+
+instantiation int :: comm_ring_1
 begin
 
-definition
-  Zero_int_def: "0 = Abs_Integ (intrel `` {(0, 0)})"
+lift_definition zero_int :: "int" is "(0, 0)"
+  by simp
 
-definition
-  One_int_def: "1 = Abs_Integ (intrel `` {(1, 0)})"
+lift_definition one_int :: "int" is "(1, 0)"
+  by simp
 
-definition
-  add_int_def: "z + w = Abs_Integ
-    (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u, v) \<in> Rep_Integ w.
-      intrel `` {(x + u, y + v)})"
+lift_definition plus_int :: "int \<Rightarrow> int \<Rightarrow> int"
+  is "\<lambda>(x, y) (u, v). (x + u, y + v)"
+  by clarsimp
 
-definition
-  minus_int_def:
-    "- z = Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"
-
-definition
-  diff_int_def:  "z - w = z + (-w \<Colon> int)"
+lift_definition uminus_int :: "int \<Rightarrow> int"
+  is "\<lambda>(x, y). (y, x)"
+  by clarsimp
 
-definition
-  mult_int_def: "z * w = Abs_Integ
-    (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u,v ) \<in> Rep_Integ w.
-      intrel `` {(x*u + y*v, x*v + y*u)})"
-
-definition
-  le_int_def:
-   "z \<le> w \<longleftrightarrow> (\<exists>x y u v. x+v \<le> u+y \<and> (x, y) \<in> Rep_Integ z \<and> (u, v) \<in> Rep_Integ w)"
+lift_definition minus_int :: "int \<Rightarrow> int \<Rightarrow> int"
+  is "\<lambda>(x, y) (u, v). (x + v, y + u)"
+  by clarsimp
 
-definition
-  less_int_def: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
+lift_definition times_int :: "int \<Rightarrow> int \<Rightarrow> int"
+  is "\<lambda>(x, y) (u, v). (x*u + y*v, x*v + y*u)"
+proof (clarsimp)
+  fix s t u v w x y z :: nat
+  assume "s + v = u + t" and "w + z = y + x"
+  hence "(s + v) * w + (u + t) * x + u * (w + z) + v * (y + x)
+       = (u + t) * w + (s + v) * x + u * (y + x) + v * (w + z)"
+    by simp
+  thus "(s * w + t * x) + (u * z + v * y) = (u * y + v * z) + (s * x + t * w)"
+    by (simp add: algebra_simps)
+qed
 
-definition
-  zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
-
-definition
-  zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
-
-instance ..
+instance
+  by default (transfer, clarsimp simp: algebra_simps)+
 
 end
 
-
-subsection{*Construction of the Integers*}
-
-lemma intrel_iff [simp]: "(((x,y),(u,v)) \<in> intrel) = (x+v = u+y)"
-by (simp add: intrel_def)
-
-lemma equiv_intrel: "equiv UNIV intrel"
-by (simp add: intrel_def equiv_def refl_on_def sym_def trans_def)
-
-text{*Reduces equality of equivalence classes to the @{term intrel} relation:
-  @{term "(intrel `` {x} = intrel `` {y}) = ((x,y) \<in> intrel)"} *}
-lemmas equiv_intrel_iff [simp] = eq_equiv_class_iff [OF equiv_intrel UNIV_I UNIV_I]
-
-text{*All equivalence classes belong to set of representatives*}
-lemma [simp]: "intrel``{(x,y)} \<in> Integ"
-by (auto simp add: Integ_def intrel_def quotient_def)
-
-text{*Reduces equality on abstractions to equality on representatives:
-  @{prop "\<lbrakk>x \<in> Integ; y \<in> Integ\<rbrakk> \<Longrightarrow> (Abs_Integ x = Abs_Integ y) = (x=y)"} *}
-declare Abs_Integ_inject [simp,no_atp]  Abs_Integ_inverse [simp,no_atp]
-
-text{*Case analysis on the representation of an integer as an equivalence
-      class of pairs of naturals.*}
-lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]:
-     "(!!x y. z = Abs_Integ(intrel``{(x,y)}) ==> P) ==> P"
-apply (rule Abs_Integ_cases [of z]) 
-apply (auto simp add: Integ_def quotient_def) 
-done
-
-
-subsection {* Arithmetic Operations *}
-
-lemma minus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})"
-proof -
-  have "(\<lambda>(x,y). intrel``{(y,x)}) respects intrel"
-    by (auto simp add: congruent_def)
-  thus ?thesis
-    by (simp add: minus_int_def UN_equiv_class [OF equiv_intrel])
-qed
-
-lemma add:
-     "Abs_Integ (intrel``{(x,y)}) + Abs_Integ (intrel``{(u,v)}) =
-      Abs_Integ (intrel``{(x+u, y+v)})"
-proof -
-  have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). intrel `` {(x+u, y+v)}) w) z) 
-        respects2 intrel"
-    by (auto simp add: congruent2_def)
-  thus ?thesis
-    by (simp add: add_int_def UN_UN_split_split_eq
-                  UN_equiv_class2 [OF equiv_intrel equiv_intrel])
-qed
-
-text{*Congruence property for multiplication*}
-lemma mult_congruent2:
-     "(%p1 p2. (%(x,y). (%(u,v). intrel``{(x*u + y*v, x*v + y*u)}) p2) p1)
-      respects2 intrel"
-apply (rule equiv_intrel [THEN congruent2_commuteI])
- apply (force simp add: mult_ac, clarify) 
-apply (simp add: congruent_def mult_ac)  
-apply (rename_tac u v w x y z)
-apply (subgoal_tac "u*y + x*y = w*y + v*y  &  u*z + x*z = w*z + v*z")
-apply (simp add: mult_ac)
-apply (simp add: add_mult_distrib [symmetric])
-done
-
-lemma mult:
-     "Abs_Integ((intrel``{(x,y)})) * Abs_Integ((intrel``{(u,v)})) =
-      Abs_Integ(intrel `` {(x*u + y*v, x*v + y*u)})"
-by (simp add: mult_int_def UN_UN_split_split_eq mult_congruent2
-              UN_equiv_class2 [OF equiv_intrel equiv_intrel])
-
-text{*The integers form a @{text comm_ring_1}*}
-instance int :: comm_ring_1
-proof
-  fix i j k :: int
-  show "(i + j) + k = i + (j + k)"
-    by (cases i, cases j, cases k) (simp add: add add_assoc)
-  show "i + j = j + i" 
-    by (cases i, cases j) (simp add: add_ac add)
-  show "0 + i = i"
-    by (cases i) (simp add: Zero_int_def add)
-  show "- i + i = 0"
-    by (cases i) (simp add: Zero_int_def minus add)
-  show "i - j = i + - j"
-    by (simp add: diff_int_def)
-  show "(i * j) * k = i * (j * k)"
-    by (cases i, cases j, cases k) (simp add: mult algebra_simps)
-  show "i * j = j * i"
-    by (cases i, cases j) (simp add: mult algebra_simps)
-  show "1 * i = i"
-    by (cases i) (simp add: One_int_def mult)
-  show "(i + j) * k = i * k + j * k"
-    by (cases i, cases j, cases k) (simp add: add mult algebra_simps)
-  show "0 \<noteq> (1::int)"
-    by (simp add: Zero_int_def One_int_def)
-qed
-
 abbreviation int :: "nat \<Rightarrow> int" where
   "int \<equiv> of_nat"
 
-lemma int_def: "int m = Abs_Integ (intrel `` {(m, 0)})"
-by (induct m) (simp_all add: Zero_int_def One_int_def add)
-
-
-subsection {* The @{text "\<le>"} Ordering *}
+lemma int_def: "int n = Abs_Integ (n, 0)"
+  by (induct n, simp add: zero_int.abs_eq,
+    simp add: one_int.abs_eq plus_int.abs_eq)
 
-lemma le:
-  "(Abs_Integ(intrel``{(x,y)}) \<le> Abs_Integ(intrel``{(u,v)})) = (x+v \<le> u+y)"
-by (force simp add: le_int_def)
+lemma int_transfer [transfer_rule]:
+  "(fun_rel (op =) cr_int) (\<lambda>n. (n, 0)) int"
+  unfolding fun_rel_def cr_int_def int_def by simp
 
-lemma less:
-  "(Abs_Integ(intrel``{(x,y)}) < Abs_Integ(intrel``{(u,v)})) = (x+v < u+y)"
-by (simp add: less_int_def le order_less_le)
+lemma int_diff_cases:
+  obtains (diff) m n where "z = int m - int n"
+  by transfer clarsimp
+
+subsection {* Integers are totally ordered *}
 
-instance int :: linorder
-proof
-  fix i j k :: int
-  show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
-    by (cases i, cases j) (simp add: le)
-  show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
-    by (auto simp add: less_int_def dest: antisym) 
-  show "i \<le> i"
-    by (cases i) (simp add: le)
-  show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
-    by (cases i, cases j, cases k) (simp add: le)
-  show "i \<le> j \<or> j \<le> i"
-    by (cases i, cases j) (simp add: le linorder_linear)
-qed
+instantiation int :: linorder
+begin
+
+lift_definition less_eq_int :: "int \<Rightarrow> int \<Rightarrow> bool"
+  is "\<lambda>(x, y) (u, v). x + v \<le> u + y"
+  by auto
+
+lift_definition less_int :: "int \<Rightarrow> int \<Rightarrow> bool"
+  is "\<lambda>(x, y) (u, v). x + v < u + y"
+  by auto
+
+instance
+  by default (transfer, force)+
+
+end
 
 instantiation int :: distrib_lattice
 begin
@@ -209,14 +122,15 @@
 
 end
 
+subsection {* Ordering properties of arithmetic operations *}
+
 instance int :: ordered_cancel_ab_semigroup_add
 proof
   fix i j k :: int
   show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
-    by (cases i, cases j, cases k) (simp add: le add)
+    by transfer clarsimp
 qed
 
-
 text{*Strict Monotonicity of Multiplication*}
 
 text{*strict, in 1st argument; proof is by induction on k>0*}
@@ -230,15 +144,15 @@
 done
 
 lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = int n"
-apply (cases k)
-apply (auto simp add: le add int_def Zero_int_def)
-apply (rule_tac x="x-y" in exI, simp)
+apply transfer
+apply clarsimp
+apply (rule_tac x="a - b" in exI, simp)
 done
 
 lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = int n"
-apply (cases k)
-apply (simp add: less int_def Zero_int_def)
-apply (rule_tac x="x-y" in exI, simp)
+apply transfer
+apply clarsimp
+apply (rule_tac x="a - b" in exI, simp)
 done
 
 lemma zmult_zless_mono2: "[| i<j;  (0::int) < k |] ==> k*i < k*j"
@@ -247,8 +161,16 @@
 done
 
 text{*The integers form an ordered integral domain*}
-instance int :: linordered_idom
-proof
+instantiation int :: linordered_idom
+begin
+
+definition
+  zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
+
+definition
+  zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
+
+instance proof
   fix i j k :: int
   show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
     by (rule zmult_zless_mono2)
@@ -258,17 +180,17 @@
     by (simp only: zsgn_def)
 qed
 
+end
+
 lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + (1\<Colon>int) \<le> z"
-apply (cases w, cases z) 
-apply (simp add: less le add One_int_def)
-done
+  by transfer clarsimp
 
 lemma zless_iff_Suc_zadd:
   "(w \<Colon> int) < z \<longleftrightarrow> (\<exists>n. z = w + int (Suc n))"
-apply (cases z, cases w)
-apply (auto simp add: less add int_def)
-apply (rename_tac a b c d) 
-apply (rule_tac x="a+d - Suc(c+b)" in exI) 
+apply transfer
+apply auto
+apply (rename_tac a b c d)
+apply (rule_tac x="c+b - Suc(a+d)" in exI)
 apply arith
 done
 
@@ -285,37 +207,30 @@
 context ring_1
 begin
 
-definition of_int :: "int \<Rightarrow> 'a" where
-  "of_int z = the_elem (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
-
-lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
-proof -
-  have "(\<lambda>(i,j). { of_nat i - (of_nat j :: 'a) }) respects intrel"
-    by (auto simp add: congruent_def) (simp add: algebra_simps of_nat_add [symmetric]
-            del: of_nat_add) 
-  thus ?thesis
-    by (simp add: of_int_def UN_equiv_class [OF equiv_intrel])
-qed
+lift_definition of_int :: "int \<Rightarrow> 'a" is "\<lambda>(i, j). of_nat i - of_nat j"
+  by (clarsimp simp add: diff_eq_eq eq_diff_eq diff_add_eq
+    of_nat_add [symmetric] simp del: of_nat_add)
 
 lemma of_int_0 [simp]: "of_int 0 = 0"
-by (simp add: of_int Zero_int_def)
+by (simp add: of_int.abs_eq zero_int.abs_eq) (* FIXME: transfer *)
 
 lemma of_int_1 [simp]: "of_int 1 = 1"
-by (simp add: of_int One_int_def)
+by (simp add: of_int.abs_eq one_int.abs_eq) (* FIXME: transfer *)
 
 lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z"
-by (cases w, cases z) (simp add: algebra_simps of_int add)
+(* FIXME: transfer *)
+by (cases w, cases z) (simp add: algebra_simps of_int.abs_eq plus_int.abs_eq)
 
 lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)"
-by (cases z) (simp add: algebra_simps of_int minus)
+(* FIXME: transfer *)
+by (cases z) (simp add: algebra_simps of_int.abs_eq uminus_int.abs_eq)
 
 lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z"
 by (simp add: diff_minus Groups.diff_minus)
 
 lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
-apply (cases w, cases z)
-apply (simp add: algebra_simps of_int mult of_nat_mult)
-done
+by (cases w, cases z, (* FIXME: transfer *)
+  simp add: algebra_simps of_int.abs_eq times_int.abs_eq of_nat_mult)
 
 text{*Collapse nested embeddings*}
 lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n"
@@ -339,8 +254,9 @@
 
 lemma of_int_eq_iff [simp]:
    "of_int w = of_int z \<longleftrightarrow> w = z"
+(* FIXME: transfer *)
 apply (cases w, cases z)
-apply (simp add: of_int)
+apply (simp add: of_int.abs_eq int.abs_eq_iff)
 apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq)
 apply (simp only: of_nat_add [symmetric] of_nat_eq_iff)
 done
@@ -364,8 +280,9 @@
 
 lemma of_int_le_iff [simp]:
   "of_int w \<le> of_int z \<longleftrightarrow> w \<le> z"
-  by (cases w, cases z)
-    (simp add: of_int le minus algebra_simps of_nat_add [symmetric] del: of_nat_add)
+  by (cases w, cases z) (* FIXME: transfer *)
+    (simp add: of_int.abs_eq less_eq_int.abs_eq
+      algebra_simps of_nat_add [symmetric] del: of_nat_add)
 
 lemma of_int_less_iff [simp]:
   "of_int w < of_int z \<longleftrightarrow> w < z"
@@ -392,39 +309,29 @@
 lemma of_int_eq_id [simp]: "of_int = id"
 proof
   fix z show "of_int z = id z"
-    by (cases z) (simp add: of_int add minus int_def diff_minus)
+    by (cases z rule: int_diff_cases, simp)
 qed
 
 
 subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *}
 
-definition nat :: "int \<Rightarrow> nat" where
-  "nat z = the_elem (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
-
-lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
-proof -
-  have "(\<lambda>(x,y). {x-y}) respects intrel"
-    by (auto simp add: congruent_def)
-  thus ?thesis
-    by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
-qed
+lift_definition nat :: "int \<Rightarrow> nat" is "\<lambda>(x, y). x - y"
+  by auto
 
 lemma nat_int [simp]: "nat (int n) = n"
-by (simp add: nat int_def)
+  by transfer simp
 
 lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
-by (cases z) (simp add: nat le int_def Zero_int_def)
+  by transfer clarsimp
 
 corollary nat_0_le: "0 \<le> z ==> int (nat z) = z"
 by simp
 
 lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
-by (cases z) (simp add: nat le Zero_int_def)
+  by transfer clarsimp
 
 lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
-apply (cases w, cases z) 
-apply (simp add: nat le linorder_not_le [symmetric] Zero_int_def, arith)
-done
+  by transfer (clarsimp, arith)
 
 text{*An alternative condition is @{term "0 \<le> w"} *}
 corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
@@ -434,9 +341,7 @@
 by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 
 
 lemma zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < z)"
-apply (cases w, cases z) 
-apply (simp add: nat le Zero_int_def linorder_not_le [symmetric], arith)
-done
+  by transfer (clarsimp, arith)
 
 lemma nonneg_eq_int:
   fixes z :: int
@@ -445,24 +350,22 @@
   using assms by (blast dest: nat_0_le sym)
 
 lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"
-by (cases w) (simp add: nat le int_def Zero_int_def, arith)
+  by transfer (clarsimp simp add: le_imp_diff_is_add)
 
 corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"
 by (simp only: eq_commute [of m] nat_eq_iff)
 
 lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"
-apply (cases w)
-apply (simp add: nat le int_def Zero_int_def linorder_not_le[symmetric], arith)
-done
+  by transfer (clarsimp, arith)
 
 lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> int n"
-  by (cases x, simp add: nat le int_def le_diff_conv)
+  by transfer (clarsimp simp add: le_diff_conv)
 
 lemma nat_mono: "x \<le> y \<Longrightarrow> nat x \<le> nat y"
-  by (cases x, cases y, simp add: nat le)
+  by transfer auto
 
 lemma nat_0_iff[simp]: "nat(i::int) = 0 \<longleftrightarrow> i\<le>0"
-by(simp add: nat_eq_iff) arith
+  by transfer clarsimp
 
 lemma int_eq_iff: "(of_nat m = z) = (m = nat z & 0 \<le> z)"
 by (auto simp add: nat_eq_iff2)
@@ -472,25 +375,24 @@
 
 lemma nat_add_distrib:
      "[| (0::int) \<le> z;  0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
-by (cases z, cases z') (simp add: nat add le Zero_int_def)
+  by transfer clarsimp
 
 lemma nat_diff_distrib:
      "[| (0::int) \<le> z';  z' \<le> z |] ==> nat (z-z') = nat z - nat z'"
-by (cases z, cases z')
-  (simp add: nat add minus diff_minus le Zero_int_def)
+  by transfer clarsimp
 
 lemma nat_zminus_int [simp]: "nat (- int n) = 0"
-by (simp add: int_def minus nat Zero_int_def) 
+  by transfer simp
 
 lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
-by (cases z) (simp add: nat less int_def, arith)
+  by transfer (clarsimp simp add: less_diff_conv)
 
 context ring_1
 begin
 
 lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z"
-  by (cases z rule: eq_Abs_Integ)
-   (simp add: nat le of_int Zero_int_def of_nat_diff)
+  by (cases z rule: eq_Abs_Integ) (* FIXME: transfer *)
+   (simp add: nat.abs_eq less_eq_int.abs_eq of_int.abs_eq zero_int.abs_eq of_nat_diff)
 
 end
 
@@ -516,7 +418,7 @@
 by (subst le_minus_iff, simp del: of_nat_Suc)
 
 lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
-by (simp add: int_def le minus Zero_int_def)
+  by transfer simp
 
 lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
 by (simp add: linorder_not_less)
@@ -550,9 +452,9 @@
 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
 
 lemma negD: "x < 0 \<Longrightarrow> \<exists>n. x = - (int (Suc n))"
-apply (cases x)
-apply (auto simp add: le minus Zero_int_def int_def order_less_le)
-apply (rule_tac x="y - Suc x" in exI, arith)
+apply transfer
+apply clarsimp
+apply (rule_tac x="b - Suc a" in exI, arith)
 done
 
 
@@ -578,14 +480,6 @@
   assumes "0 \<le> k" obtains n where "k = int n"
   using assms by (cases k, simp, simp del: of_nat_Suc)
 
-text{*Contributed by Brian Huffman*}
-theorem int_diff_cases:
-  obtains (diff) m n where "z = int m - int n"
-apply (cases z rule: eq_Abs_Integ)
-apply (rule_tac m=x and n=y in diff)
-apply (simp add: int_def minus add diff_minus)
-done
-
 lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
   -- {* Unfold all @{text let}s involving constants *}
   unfolding Let_def ..
@@ -870,12 +764,8 @@
 
 subsection{*The functions @{term nat} and @{term int}*}
 
-text{*Simplify the terms @{term "int 0"}, @{term "int(Suc 0)"} and
-  @{term "w + - z"}*}
-declare Zero_int_def [symmetric, simp]
-declare One_int_def [symmetric, simp]
-
-lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp]
+text{*Simplify the term @{term "w + - z"}*}
+lemmas diff_int_def_symmetric = diff_def [where 'a=int, symmetric, simp]
 
 lemma nat_0 [simp]: "nat 0 = 0"
 by (simp add: nat_eq_iff)
@@ -1771,4 +1661,14 @@
 
 lemmas zpower_int = int_power [symmetric]
 
+text {* De-register @{text "int"} as a quotient type: *}
+
+lemmas [transfer_rule del] =
+  int.id_abs_transfer int.rel_eq_transfer zero_int.transfer one_int.transfer
+  plus_int.transfer uminus_int.transfer minus_int.transfer times_int.transfer
+  int_transfer less_eq_int.transfer less_int.transfer of_int.transfer
+  nat.transfer
+
+declare Quotient_int [quot_del]
+
 end
diff -r 9bc78a08ff0a -r 60bcc6cf17d6 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu May 31 17:10:43 2012 +0200
+++ b/src/HOL/IsaMakefile	Fri Jun 01 08:32:26 2012 +0200
@@ -1034,14 +1034,16 @@
   ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy				\
   ex/Quicksort.thy ex/ROOT.ML						\
   ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy		\
-  ex/SAT_Examples.thy ex/Serbian.thy ex/Set_Theory.thy			\
-  ex/Simproc_Tests.thy ex/SVC_Oracle.thy		\
-  ex/Seq.thy ex/Sqrt.thy ex/Sqrt_Script.thy 	\
+  ex/SAT_Examples.thy ex/Serbian.thy 					\
+  ex/Set_Comprehension_Pointfree_Tests.thy ex/Set_Theory.thy		\
+  ex/Simproc_Tests.thy ex/SVC_Oracle.thy				\
+  ex/Seq.thy ex/Sqrt.thy ex/Sqrt_Script.thy 				\
   ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy	\
   ex/Transfer_Int_Nat.thy						\
   ex/Tree23.thy	ex/Unification.thy ex/While_Combinator_Example.thy	\
   ex/document/root.bib ex/document/root.tex ex/svc_funcs.ML		\
-  ex/svc_test.thy ../Tools/interpretation_with_defs.ML
+  ex/svc_test.thy ../Tools/interpretation_with_defs.ML			\
+  ex/set_comprehension_pointfree.ML
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
 
 
diff -r 9bc78a08ff0a -r 60bcc6cf17d6 src/HOL/Metis_Examples/Sets.thy
--- a/src/HOL/Metis_Examples/Sets.thy	Thu May 31 17:10:43 2012 +0200
+++ b/src/HOL/Metis_Examples/Sets.thy	Fri Jun 01 08:32:26 2012 +0200
@@ -195,7 +195,7 @@
        apply (metis all_not_in_conv)
       apply (metis all_not_in_conv)
      apply (metis mem_Collect_eq)
-    apply (metis less_int_def singleton_iff)
+    apply (metis less_le singleton_iff)
    apply (metis mem_Collect_eq)
   apply (metis mem_Collect_eq)
  apply (metis all_not_in_conv)
diff -r 9bc78a08ff0a -r 60bcc6cf17d6 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu May 31 17:10:43 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jun 01 08:32:26 2012 +0200
@@ -1760,7 +1760,7 @@
     hence "norm (a + x) \<le> b + norm a" using norm_triangle_ineq[of a x] b by auto
   }
   thus ?thesis unfolding bounded_pos using norm_ge_zero[of a] b(1) using add_strict_increasing[of b 0 "norm a"]
-    by (auto intro!: add exI[of _ "b + norm a"])
+    by (auto intro!: exI[of _ "b + norm a"])
 qed
 
 
diff -r 9bc78a08ff0a -r 60bcc6cf17d6 src/HOL/Nitpick_Examples/Integer_Nits.thy
--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy	Thu May 31 17:10:43 2012 +0200
+++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy	Fri Jun 01 08:32:26 2012 +0200
@@ -95,6 +95,9 @@
 nitpick [binary_ints, bits = 9, expect = genuine]
 oops
 
+(* FIXME
+*** Invalid intermediate term ("Nitpick_Nut.the_name"): (ConstName Nitpick.sel0$Nitpick.Quot int \<Rightarrow> nat X).
+
 lemma "nat (of_nat n) = n"
 nitpick [unary_ints, expect = none]
 nitpick [binary_ints, expect = none]
@@ -205,6 +208,7 @@
 nitpick [unary_ints, expect = none]
 nitpick [binary_ints, expect = none]
 sorry
+*)
 
 datatype tree = Null | Node nat tree tree
 
diff -r 9bc78a08ff0a -r 60bcc6cf17d6 src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Thu May 31 17:10:43 2012 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Jun 01 08:32:26 2012 +0200
@@ -64,8 +64,10 @@
 subsection {* 2.5. Natural Numbers and Integers *}
 
 lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
+(* FIXME
 nitpick [expect = genuine]
 nitpick [binary_ints, bits = 16, expect = genuine]
+*)
 oops
 
 lemma "\<forall>n. Suc n \<noteq> n \<Longrightarrow> P"
@@ -141,11 +143,15 @@
   Ycoord :: int
 
 lemma "Xcoord (p\<Colon>point) = Xcoord (q\<Colon>point)"
+(* FIXME: Invalid intermediate term
 nitpick [show_datatypes, expect = genuine]
+*)
 oops
 
 lemma "4 * x + 3 * (y\<Colon>real) \<noteq> 1 / 2"
+(* FIXME: Invalid intermediate term
 nitpick [show_datatypes, expect = genuine]
+*)
 oops
 
 subsection {* 2.8. Inductive and Coinductive Predicates *}
diff -r 9bc78a08ff0a -r 60bcc6cf17d6 src/HOL/Nitpick_Examples/Record_Nits.thy
--- a/src/HOL/Nitpick_Examples/Record_Nits.thy	Thu May 31 17:10:43 2012 +0200
+++ b/src/HOL/Nitpick_Examples/Record_Nits.thy	Fri Jun 01 08:32:26 2012 +0200
@@ -18,6 +18,7 @@
   xc :: int
   yc :: int
 
+(* FIXME: Invalid intermediate term
 lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x, yc := y\<rparr>"
 nitpick [expect = none]
 sorry
@@ -83,5 +84,6 @@
 lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> = p"
 nitpick [expect = genuine]
 oops
+*)
 
 end
diff -r 9bc78a08ff0a -r 60bcc6cf17d6 src/HOL/Nitpick_Examples/Typedef_Nits.thy
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Thu May 31 17:10:43 2012 +0200
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Fri Jun 01 08:32:26 2012 +0200
@@ -171,6 +171,7 @@
   Xcoord :: int
   Ycoord :: int
 
+(* FIXME: Invalid intermediate term
 lemma "Abs_point_ext (Rep_point_ext a) = a"
 nitpick [expect = none]
 by (fact Rep_point_ext_inverse)
@@ -182,5 +183,6 @@
 lemma "Abs_rat (Rep_rat a) = a"
 nitpick [card = 1, expect = none]
 by (rule Rep_rat_inverse)
+*)
 
 end
diff -r 9bc78a08ff0a -r 60bcc6cf17d6 src/HOL/Quotient_Examples/Quotient_Rat.thy
--- a/src/HOL/Quotient_Examples/Quotient_Rat.thy	Thu May 31 17:10:43 2012 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy	Fri Jun 01 08:32:26 2012 +0200
@@ -114,6 +114,8 @@
 
 lemmas [simp] = Respects_def
 
+(* FIXME: (partiality_)descending raises exception TYPE_MATCH
+
 instantiation rat :: comm_ring_1
 begin
 
@@ -260,5 +262,6 @@
     then show "\<exists>z\<Colon>int. a * b \<le> z * b * b" by auto
   qed
 qed
+*)
 
 end
diff -r 9bc78a08ff0a -r 60bcc6cf17d6 src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Thu May 31 17:10:43 2012 +0200
+++ b/src/HOL/Tools/SMT/smt_config.ML	Fri Jun 01 08:32:26 2012 +0200
@@ -9,7 +9,7 @@
   (*solver*)
   type solver_info = {
     name: string,
-    class: SMT_Utils.class,
+    class: Proof.context -> SMT_Utils.class,
     avail: unit -> bool,
     options: Proof.context -> string list }
   val add_solver: solver_info -> Context.generic -> Context.generic
@@ -61,7 +61,7 @@
 
 type solver_info = {
   name: string,
-  class: SMT_Utils.class,
+  class: Proof.context -> SMT_Utils.class,
   avail: unit -> bool,
   options: Proof.context -> string list }
 
@@ -131,7 +131,8 @@
   | (_, NONE) => default ())
 
 fun solver_class_of ctxt =
-  solver_info_of no_solver_err (#class o fst o the) ctxt
+  let fun class_of ({class, ...}: solver_info, _) = class ctxt
+  in solver_info_of no_solver_err (class_of o the) ctxt end
 
 fun solver_options_of ctxt =
   let
diff -r 9bc78a08ff0a -r 60bcc6cf17d6 src/HOL/Tools/SMT/smt_setup_solvers.ML
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Thu May 31 17:10:43 2012 +0200
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Fri Jun 01 08:32:26 2012 +0200
@@ -63,7 +63,7 @@
 
   fun mk is_remote = {
     name = make_name is_remote "cvc3",
-    class = SMTLIB_Interface.smtlibC,
+    class = K SMTLIB_Interface.smtlibC,
     avail = make_avail is_remote "CVC3",
     command = make_command is_remote "CVC3",
     options = cvc3_options,
@@ -85,7 +85,7 @@
 
 fun yices () = {
   name = "yices",
-  class = SMTLIB_Interface.smtlibC,
+  class = K SMTLIB_Interface.smtlibC,
   avail = make_local_avail "YICES",
   command = make_local_command "YICES",
   options = (fn ctxt => [
@@ -163,9 +163,16 @@
       handle SMT_Failure.SMT _ => outcome (swap o split_last)
     end
 
+  val with_extensions =
+    Attrib.setup_config_bool @{binding z3_with_extensions} (K true)
+
+  fun select_class ctxt =
+    if Config.get ctxt with_extensions then Z3_Interface.smtlib_z3C
+    else SMTLIB_Interface.smtlibC
+
   fun mk is_remote = {
     name = make_name is_remote "z3",
-    class = Z3_Interface.smtlib_z3C,
+    class = select_class,
     avail = make_avail is_remote "Z3",
     command = z3_make_command is_remote "Z3",
     options = z3_options,
diff -r 9bc78a08ff0a -r 60bcc6cf17d6 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Thu May 31 17:10:43 2012 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Fri Jun 01 08:32:26 2012 +0200
@@ -10,7 +10,7 @@
   datatype outcome = Unsat | Sat | Unknown
   type solver_config = {
     name: string,
-    class: SMT_Utils.class,
+    class: Proof.context -> SMT_Utils.class,
     avail: unit -> bool,
     command: unit -> string list,
     options: Proof.context -> string list,
@@ -146,7 +146,7 @@
 
 type solver_config = {
   name: string,
-  class: SMT_Utils.class,
+  class: Proof.context -> SMT_Utils.class,
   avail: unit -> bool,
   command: unit -> string list,
   options: Proof.context -> string list,
diff -r 9bc78a08ff0a -r 60bcc6cf17d6 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Thu May 31 17:10:43 2012 +0200
+++ b/src/HOL/ex/ROOT.ML	Fri Jun 01 08:32:26 2012 +0200
@@ -72,7 +72,8 @@
   "Seq",
   "Simproc_Tests",
   "Executable_Relation",
-  "FinFunPred"
+  "FinFunPred",
+  "Set_Comprehension_Pointfree_Tests"
 ];
 
 use_thy "SVC_Oracle";
diff -r 9bc78a08ff0a -r 60bcc6cf17d6 src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy	Fri Jun 01 08:32:26 2012 +0200
@@ -0,0 +1,45 @@
+(*  Title:      HOL/ex/Set_Comprehension_Pointfree_Tests.thy
+    Author:     Lukas Bulwahn
+    Copyright   2012 TU Muenchen
+*)
+
+header {* Tests for the set comprehension to pointfree simproc *}
+
+theory Set_Comprehension_Pointfree_Tests
+imports Main
+uses "~~/src/HOL/ex/set_comprehension_pointfree.ML"
+begin
+
+simproc_setup finite_Collect ("finite (Collect P)") = {* Set_Comprehension_Pointfree.simproc *}
+
+lemma
+  "finite {f a b| a b. a : A \<and> b : B}"
+apply simp (* works :) *)
+oops
+
+lemma
+  "finite {f a b| a b. a : A \<and> a : A' \<and> b : B}"
+(* apply simp -- does not terminate *)
+oops
+
+lemma
+  "finite {f a b| a b. a : A \<and> b : B \<and> b : B'}"
+(* apply simp -- does not terminate *)
+oops
+
+lemma
+  "finite {f a b c| a b c. a : A \<and> b : B \<and> c : C}"
+(* apply simp -- failed *) 
+oops
+
+lemma
+  "finite {f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D}"
+(* apply simp -- failed *)
+oops
+
+lemma
+  "finite {f a b c d e | a b c d e. a : A \<and> b : B \<and> c : C \<and> d : D \<and> e : E}"
+(* apply simp -- failed *)
+oops
+
+end
diff -r 9bc78a08ff0a -r 60bcc6cf17d6 src/HOL/ex/set_comprehension_pointfree.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/set_comprehension_pointfree.ML	Fri Jun 01 08:32:26 2012 +0200
@@ -0,0 +1,120 @@
+(*  Title:      HOL/Tools/set_comprehension_pointfree.ML
+    Author:     Felix Kuperjans, Lukas Bulwahn, TU Muenchen
+
+Simproc for rewriting set comprehensions to pointfree expressions.
+*)
+
+signature SET_COMPREHENSION_POINTFREE =
+sig
+  val simproc : morphism -> simpset -> cterm -> thm option
+end
+
+structure Set_Comprehension_Pointfree : SET_COMPREHENSION_POINTFREE =
+struct
+
+(* syntactic operations *)
+
+fun mk_inf (t1, t2) =
+  let
+    val T = fastype_of t1
+  in
+    Const (@{const_name Lattices.inf_class.inf}, T --> T --> T) $ t1 $ t2
+  end
+
+fun mk_image t1 t2 =
+  let
+    val T as Type (@{type_name fun}, [_ , R]) = fastype_of t1
+  in
+    Const (@{const_name image}, T --> fastype_of t2 --> HOLogic.mk_setT R) $ t1 $ t2
+  end;
+
+fun mk_sigma (t1, t2) =
+  let
+    val T1 = fastype_of t1
+    val T2 = fastype_of t2
+    val setT = HOLogic.dest_setT T1
+    val resultT = HOLogic.mk_setT (HOLogic.mk_prodT (setT, HOLogic.dest_setT T2))
+  in
+    Const (@{const_name Sigma}, T1 --> (setT --> T2) --> resultT) $ t1 $ absdummy setT t2
+  end;
+
+fun dest_Bound (Bound x) = x
+  | dest_Bound t = raise TERM("dest_Bound", [t]);
+
+fun dest_Collect (Const (@{const_name Collect}, _) $ Abs (_, _, t)) = t
+  | dest_Collect t = raise TERM ("dest_Collect", [t])
+
+(* Copied from predicate_compile_aux.ML *)
+fun strip_ex (Const (@{const_name Ex}, _) $ Abs (x, T, t)) =
+  let
+    val (xTs, t') = strip_ex t
+  in
+    ((x, T) :: xTs, t')
+  end
+  | strip_ex t = ([], t)
+
+fun list_tupled_abs [] f = f
+  | list_tupled_abs [(n, T)] f = (Abs (n, T, f))
+  | list_tupled_abs ((n, T)::v::vs) f = HOLogic.mk_split (Abs (n, T, list_tupled_abs (v::vs) f))
+  
+fun mk_pointfree_expr t =
+  let
+    val (vs, t'') = strip_ex (dest_Collect t)
+    val (eq::conjs) = HOLogic.dest_conj t''
+    val f = if fst (HOLogic.dest_eq eq) = Bound (length vs)
+            then snd (HOLogic.dest_eq eq)
+            else raise TERM("mk_pointfree_expr", [t]);
+    val mems = map (apfst dest_Bound o HOLogic.dest_mem) conjs
+    val grouped_mems = AList.group (op =) mems
+    fun mk_grouped_unions (i, T) =
+      case AList.lookup (op =) grouped_mems i of
+        SOME ts => foldr1 mk_inf ts
+      | NONE => HOLogic.mk_UNIV T
+    val complete_sets = map mk_grouped_unions ((length vs - 1) downto 0 ~~ map snd vs)
+  in
+    mk_image (list_tupled_abs vs f) (foldr1 mk_sigma complete_sets)
+  end;
+
+(* proof tactic *)
+
+(* This tactic is terribly incomplete *) 
+
+val goal1_tac_part2 = REPEAT_ALL_NEW (CHANGED o (atac ORELSE' rtac @{thm SigmaI}))
+
+val goal1_tac = etac @{thm CollectE}
+  THEN' REPEAT1 o CHANGED o etac @{thm exE}
+  THEN' REPEAT1 o CHANGED o etac @{thm conjE}
+  THEN' rtac @{thm image_eqI}
+  THEN' RANGE [(REPEAT o CHANGED o stac @{thm split}) THEN' goal1_tac_part2, goal1_tac_part2]
+
+val goal2_tac = etac @{thm imageE}
+  THEN' rtac @{thm CollectI}
+  THEN' REPEAT o CHANGED o etac @{thm SigmaE}
+  THEN' REPEAT o CHANGED o rtac @{thm exI}
+  THEN' REPEAT_ALL_NEW (rtac @{thm conjI})
+  THEN_ALL_NEW
+    (atac ORELSE'
+    (asm_full_simp_tac HOL_basic_ss THEN' stac @{thm split} THEN' rtac @{thm refl}))
+
+val tac =
+  rtac @{thm set_eqI} 1
+  THEN rtac @{thm iffI} 1
+  THEN goal1_tac 1
+  THEN goal2_tac 1
+
+(* simproc *)
+
+fun simproc _ ss redex =
+  let
+    val ctxt = Simplifier.the_context ss
+    val _ $ set_compr = term_of redex
+  in
+    case try mk_pointfree_expr set_compr of
+      NONE => NONE
+    | SOME pointfree_expr =>
+        SOME (Goal.prove ctxt [] []
+          (HOLogic.mk_Trueprop (HOLogic.mk_eq (set_compr, pointfree_expr))) (K tac)
+        RS @{thm arg_cong[of _ _ finite]} RS @{thm eq_reflection})
+  end
+
+end;