# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272467120 -7200
# Node ID 13298f4b212be1e1b2a53ff1702dcd318f001900
# Parent  fc5ce7f22b7400cce4f6dfb8ede0f5ee1889b156
Cleaning of Int and FSet Examples

diff -r fc5ce7f22b74 -r 13298f4b212b Attic/Quot/Examples/FSet.thy
--- a/Attic/Quot/Examples/FSet.thy	Wed Apr 28 08:32:33 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,433 +0,0 @@
-theory FSet
-imports "../Quotient" "../Quotient_List" "../Quotient_Product" List
-begin
-
-inductive
-  list_eq (infix "\<approx>" 50)
-where
-  "a#b#xs \<approx> b#a#xs"
-| "[] \<approx> []"
-| "xs \<approx> ys \<Longrightarrow> ys \<approx> xs"
-| "a#a#xs \<approx> a#xs"
-| "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys"
-| "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3"
-
-lemma list_eq_refl:
-  shows "xs \<approx> xs"
-  by (induct xs) (auto intro: list_eq.intros)
-
-lemma equivp_list_eq:
-  shows "equivp list_eq"
-  unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
-  apply(auto intro: list_eq.intros list_eq_refl)
-  done
-
-quotient_type 
-  'a fset = "'a list" / "list_eq"
-  by (rule equivp_list_eq)
-
-quotient_definition
-   "EMPTY :: 'a fset"
-is
-  "[]::'a list"
-
-quotient_definition
-   "INSERT :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-is
-  "op #"
-
-quotient_definition
-   "FUNION :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-is
-  "op @"
-
-fun
-  card1 :: "'a list \<Rightarrow> nat"
-where
-  card1_nil: "(card1 []) = 0"
-| card1_cons: "(card1 (x # xs)) = (if (x mem xs) then (card1 xs) else (Suc (card1 xs)))"
-
-quotient_definition
-   "CARD :: 'a fset \<Rightarrow> nat"
-is
-  "card1"
-
-quotient_definition
-  "fconcat :: ('a fset) fset \<Rightarrow> 'a fset"
-is
-  "concat"
-
-term concat
-term fconcat
-
-text {*
- Maybe make_const_def should require a theorem that says that the particular lifted function
- respects the relation. With it such a definition would be impossible:
- make_const_def CARD @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
-*}
-
-lemma card1_0:
-  fixes a :: "'a list"
-  shows "(card1 a = 0) = (a = [])"
-  by (induct a) auto
-
-lemma not_mem_card1:
-  fixes x :: "'a"
-  fixes xs :: "'a list"
-  shows "(~(x mem xs)) = (card1 (x # xs) = Suc (card1 xs))"
-  by auto
-
-lemma mem_cons:
-  fixes x :: "'a"
-  fixes xs :: "'a list"
-  assumes a : "x mem xs"
-  shows "x # xs \<approx> xs"
-  using a by (induct xs) (auto intro: list_eq.intros )
-
-lemma card1_suc:
-  fixes xs :: "'a list"
-  fixes n :: "nat"
-  assumes c: "card1 xs = Suc n"
-  shows "\<exists>a ys. ~(a mem ys) \<and> xs \<approx> (a # ys)"
-  using c
-apply(induct xs)
-apply (metis Suc_neq_Zero card1_0)
-apply (metis FSet.card1_cons list_eq.intros(6) list_eq_refl mem_cons)
-done
-
-definition
-  rsp_fold
-where
-  "rsp_fold f = ((!u v. (f u v = f v u)) \<and> (!u v w. ((f u (f v w) = f (f u v) w))))"
-
-primrec
-  fold1
-where
-  "fold1 f (g :: 'a \<Rightarrow> 'b) (z :: 'b) [] = z"
-| "fold1 f g z (a # A) =
-     (if rsp_fold f
-     then (
-       if (a mem A) then (fold1 f g z A) else (f (g a) (fold1 f g z A))
-     ) else z)"
-
-lemma fs1_strong_cases:
-  fixes X :: "'a list"
-  shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a mem Y) \<and> (X \<approx> a # Y)))"
-  apply (induct X)
-  apply (simp)
-  apply (metis List.member.simps(1) list_eq.intros(6) list_eq_refl mem_cons)
-  done
-
-quotient_definition
-   "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"
-is
-  "op mem"
-
-quotient_definition
-   "FOLD :: ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a"
-is
-  "fold1"
-
-quotient_definition
-  "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
-is
-  "map"
-
-lemma mem_rsp:
-  fixes z
-  assumes a: "x \<approx> y"
-  shows "(z mem x) = (z mem y)"
-  using a by induct auto
-
-lemma ho_memb_rsp[quot_respect]:
-  "(op = ===> (op \<approx> ===> op =)) (op mem) (op mem)"
-  by (simp add: mem_rsp)
-
-lemma card1_rsp:
-  fixes a b :: "'a list"
-  assumes e: "a \<approx> b"
-  shows "card1 a = card1 b"
-  using e by induct (simp_all add: mem_rsp)
-
-lemma ho_card1_rsp[quot_respect]: 
-  "(op \<approx> ===> op =) card1 card1"
-  by (simp add: card1_rsp)
-
-lemma cons_rsp:
-  fixes z
-  assumes a: "xs \<approx> ys"
-  shows "(z # xs) \<approx> (z # ys)"
-  using a by (rule list_eq.intros(5))
-
-lemma ho_cons_rsp[quot_respect]:
-  "(op = ===> op \<approx> ===> op \<approx>) op # op #"
-  by (simp add: cons_rsp)
-
-lemma append_rsp_aux1:
-  assumes a : "l2 \<approx> r2 "
-  shows "(h @ l2) \<approx> (h @ r2)"
-using a
-apply(induct h)
-apply(auto intro: list_eq.intros(5))
-done
-
-lemma append_rsp_aux2:
-  assumes a : "l1 \<approx> r1" "l2 \<approx> r2 "
-  shows "(l1 @ l2) \<approx> (r1 @ r2)"
-using a
-apply(induct arbitrary: l2 r2)
-apply(simp_all)
-apply(blast intro: list_eq.intros append_rsp_aux1)+
-done
-
-lemma append_rsp[quot_respect]:
-  "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
-  by (auto simp add: append_rsp_aux2)
-
-lemma map_rsp:
-  assumes a: "a \<approx> b"
-  shows "map f a \<approx> map f b"
-  using a
-  apply (induct)
-  apply(auto intro: list_eq.intros)
-  done
-
-lemma ho_map_rsp[quot_respect]:
-  "(op = ===> op \<approx> ===> op \<approx>) map map"
-  by (simp add: map_rsp)
-
-lemma map_append:
-  "(map f (a @ b)) \<approx> (map f a) @ (map f b)"
- by simp (rule list_eq_refl)
-
-lemma ho_fold_rsp[quot_respect]:
-  "(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1"
-  apply (auto)
-  apply (case_tac "rsp_fold x")
-  prefer 2
-  apply (erule_tac list_eq.induct)
-  apply (simp_all)
-  apply (erule_tac list_eq.induct)
-  apply (simp_all)
-  apply (auto simp add: mem_rsp rsp_fold_def)
-done
-
-lemma list_equiv_rsp[quot_respect]:
-  shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
-by (auto intro: list_eq.intros)
-
-lemma "IN x EMPTY = False"
-apply(lifting member.simps(1))
-done
-
-lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"
-apply (lifting member.simps(2))
-done
-
-lemma "INSERT a (INSERT a x) = INSERT a x"
-apply (lifting list_eq.intros(4))
-done
-
-lemma "x = xa \<Longrightarrow> INSERT a x = INSERT a xa"
-apply (lifting list_eq.intros(5))
-done
-
-lemma "CARD x = Suc n \<Longrightarrow> (\<exists>a b. \<not> IN a b & x = INSERT a b)"
-apply (lifting card1_suc)
-done
-
-lemma "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))"
-apply (lifting not_mem_card1)
-done
-
-lemma "FOLD f g (z::'b) (INSERT a x) =
-  (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"
-apply(lifting fold1.simps(2))
-done
-
-lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
-apply (lifting map_append)
-done
-
-lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"
-apply (lifting append_assoc)
-done
-
-
-lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
-apply(lifting list.induct)
-done
-
-lemma list_induct_part:
-  assumes a: "P (x :: 'a list) ([] :: 'c list)"
-  assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)"
-  shows "P x l"
-  apply (rule_tac P="P x" in list.induct)
-  apply (rule a)
-  apply (rule b)
-  apply (assumption)
-  done
-
-lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
-apply (lifting list_induct_part)
-done
-
-lemma "P (x :: 'a fset) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
-apply (lifting list_induct_part)
-done
-
-lemma "P (x :: 'a fset) ([] :: 'c list) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (e # t)) \<Longrightarrow> P x l"
-apply (lifting list_induct_part)
-done
-
-quotient_type 'a fset2 = "'a list" / "list_eq"
-  by (rule equivp_list_eq)
-
-quotient_definition
-   "EMPTY2 :: 'a fset2"
-is
-  "[]::'a list"
-
-quotient_definition
-   "INSERT2 :: 'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"
-is
-  "op #"
-
-lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
-apply (lifting list_induct_part)
-done
-
-lemma "P (x :: 'a fset) (EMPTY2 :: 'c fset2) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT2 e t)) \<Longrightarrow> P x l"
-apply (lifting list_induct_part)
-done
-
-quotient_definition
-  "fset_rec :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
-is
-  "list_rec"
-
-quotient_definition
-  "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
-is
-  "list_case"
-
-(* Probably not true without additional assumptions about the function *)
-lemma list_rec_rsp[quot_respect]:
-  "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"
-  apply (auto)
-  apply (erule_tac list_eq.induct)
-  apply (simp_all)
-  sorry
-
-lemma list_case_rsp[quot_respect]:
-  "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
-  apply (auto)
-  sorry
-
-lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
-apply (lifting list.recs(2))
-done
-
-lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa"
-apply (lifting list.cases(2))
-done
-
-lemma ttt: "((op @) x ((op #) e [])) = (((op #) e x))"
-sorry
-
-lemma "(FUNION x (INSERT e EMPTY)) = ((INSERT e x))"
-apply (lifting ttt)
-done
-
-
-lemma ttt2: "(\<lambda>e. ((op @) x ((op #) e []))) = (\<lambda>e. ((op #) e x))"
-sorry
-
-lemma "(\<lambda>e. (FUNION x (INSERT e EMPTY))) = (\<lambda>e. (INSERT e x))"
-apply(lifting ttt2)
-apply(regularize)
-apply(rule impI)
-apply(simp)
-apply(rule allI)
-apply(rule list_eq_refl)
-done
-
-lemma ttt3: "(\<lambda>x. ((op @) x (e # []))) = (op #) e"
-sorry
-
-lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = INSERT e"
-apply(lifting ttt3)
-apply(regularize)
-apply(auto simp add: cons_rsp)
-done
-lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))"
-sorry
-
-lemma eq_imp_rel:
-  shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
-  by (simp add: equivp_reflp)
-
-
-lemma hard_lift: "(\<lambda>P. \<lambda>Q. P (Q (x::'a fset))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a fset)))"
-apply(lifting hard)
-apply(regularize)
-apply(rule fun_rel_id_asm)
-apply(subst babs_simp)
-apply(tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
-apply(rule fun_rel_id_asm)
-apply(rule impI)
-apply(rule mp[OF eq_imp_rel[OF fset_equivp]])
-apply(drule fun_cong)
-apply(drule fun_cong)
-apply(assumption)
-done
-
-lemma test: "All (\<lambda>(x::'a list, y). x = y)"
-sorry
-
-lemma  "All (\<lambda>(x::'a fset, y). x = y)"
-apply(lifting test)
-done
-
-lemma test2: "Ex (\<lambda>(x::'a list, y). x = y)"
-sorry
-
-lemma  "Ex (\<lambda>(x::'a fset, y). x = y)"
-apply(lifting test2)
-done
-
-lemma test3: "All (\<lambda> (x :: 'a list, y, z). x = y \<and> y = z)"
-sorry
-
-lemma "All (\<lambda> (x :: 'a fset, y, z). x = y \<and> y = z)"
-apply(lifting test3)
-done
-
-lemma test4: "\<forall> (x :: 'a list, y, z) \<in> Respects(
-  prod_rel (op \<approx>) (prod_rel (op \<approx>) (op \<approx>))
-). x = y \<and> y = z"
-sorry
-
-lemma "All (\<lambda> (x :: 'a fset, y, z). x = y \<and> y = z)"
-apply (lifting test4)
-sorry
-
-lemma test5: "\<forall> (x :: 'a list \<Rightarrow> 'a list, y) \<in> Respects(
-  prod_rel (op \<approx> ===> op \<approx>) (op \<approx> ===> op \<approx>)
-). (op \<approx> ===> op \<approx>) x y"
-sorry
-
-lemma "All (\<lambda> (x :: 'a fset \<Rightarrow> 'a fset, y). x = y)"
-apply (lifting test5)
-done
-
-lemma test6: "\<forall> (x :: 'a list \<Rightarrow> 'a list, y, z) \<in> Respects(
-  prod_rel (op \<approx> ===> op \<approx>) (prod_rel (op \<approx> ===> op \<approx>) (op \<approx> ===> op \<approx>))
-). (op \<approx> ===> op \<approx>) x y \<and> (op \<approx> ===> op \<approx>) y z"
-sorry
-
-lemma "All (\<lambda> (x :: 'a fset \<Rightarrow> 'a fset, y, z). x = y \<and> y = z)"
-apply (lifting test6)
-done
-
-end
diff -r fc5ce7f22b74 -r 13298f4b212b Attic/Quot/Examples/FSet2.thy
--- a/Attic/Quot/Examples/FSet2.thy	Wed Apr 28 08:32:33 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,128 +0,0 @@
-theory FSet2
-imports "../Quotient" "../Quotient_List" List
-begin
-
-inductive
-  list_eq (infix "\<approx>" 50)
-where
-  "a#b#xs \<approx> b#a#xs"
-| "[] \<approx> []"
-| "xs \<approx> ys \<Longrightarrow> ys \<approx> xs"
-| "a#a#xs \<approx> a#xs"
-| "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys"
-| "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3"
-
-lemma list_eq_refl:
-  shows "xs \<approx> xs"
-by (induct xs) (auto intro: list_eq.intros)
-
-lemma equivp_list_eq:
-  shows "equivp list_eq"
-unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
-by (auto intro: list_eq.intros list_eq_refl)
-
-quotient_type
-  'a fset = "'a list" / "list_eq"
-  by (rule equivp_list_eq)
-
-quotient_definition
-  fempty ("{||}")
-where
-  "fempty :: 'a fset"
-is
-  "[]"
-
-quotient_definition
-  "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-is
-  "(op #)"
-
-lemma finsert_rsp[quot_respect]:
-  shows "(op = ===> op \<approx> ===> op \<approx>) (op #) (op #)"
-by (auto intro: list_eq.intros)
-
-quotient_definition
-  funion ("_ \<union>f _" [65,66] 65)
-where
-  "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-is
-  "(op @)"
-
-lemma append_rsp_aux1:
-  assumes a : "l2 \<approx> r2 "
-  shows "(h @ l2) \<approx> (h @ r2)"
-using a
-apply(induct h)
-apply(auto intro: list_eq.intros(5))
-done
-
-lemma append_rsp_aux2:
-  assumes a : "l1 \<approx> r1" "l2 \<approx> r2 "
-  shows "(l1 @ l2) \<approx> (r1 @ r2)"
-using a
-apply(induct arbitrary: l2 r2)
-apply(simp_all)
-apply(blast intro: list_eq.intros append_rsp_aux1)+
-done
-
-lemma append_rsp[quot_respect]:
-  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
-  by (auto simp add: append_rsp_aux2)
-
-
-quotient_definition
-  fmem ("_ \<in>f _" [50, 51] 50)
-where
-  "fmem :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"
-is
-  "(op mem)"
-
-lemma memb_rsp_aux:
-  assumes a: "x \<approx> y"
-  shows "(z mem x) = (z mem y)"
-  using a by induct auto
-
-lemma memb_rsp[quot_respect]:
-  shows "(op = ===> (op \<approx> ===> op =)) (op mem) (op mem)"
-  by (simp add: memb_rsp_aux)
-
-definition
-  fnot_mem :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<notin>f _" [50, 51] 50)
-where
-  "x \<notin>f S \<equiv> \<not>(x \<in>f S)"
-
-definition
-  "inter_list" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where
-  "inter_list X Y \<equiv> [x \<leftarrow> X. x\<in>set Y]"
-
-quotient_definition
-  finter ("_ \<inter>f _" [70, 71] 70)
-where
-  "finter::'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-is
-  "inter_list"
-
-no_syntax
-  "@Finset"     :: "args => 'a fset"                       ("{|(_)|}")
-syntax
-  "@Finfset"     :: "args => 'a fset"                       ("{|(_)|}")
-translations
-  "{|x, xs|}"     == "CONST finsert x {|xs|}"
-  "{|x|}"         == "CONST finsert x {||}"
-
-
-subsection {* Empty sets *}
-
-lemma test:
-  shows "\<not>(x # xs \<approx> [])"
-sorry
-
-lemma finsert_not_empty[simp]: 
-  shows "finsert x S \<noteq> {||}"
-  by (lifting test)
-
-
-
-
-end;
diff -r fc5ce7f22b74 -r 13298f4b212b Attic/Quot/Examples/IntEx.thy
--- a/Attic/Quot/Examples/IntEx.thy	Wed Apr 28 08:32:33 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,256 +0,0 @@
-theory IntEx
-imports "../Quotient_Product" "../Quotient_List"
-begin
-
-fun
-  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
-where
-  "intrel (x, y) (u, v) = (x + v = u + y)"
-
-quotient_type 
-  my_int = "nat \<times> nat" / intrel
-  apply(unfold equivp_def)
-  apply(auto simp add: mem_def expand_fun_eq)
-  done
-
-quotient_definition
-  "ZERO :: my_int"
-is
-  "(0::nat, 0::nat)"
-
-quotient_definition
-  "ONE :: my_int"
-is
-  "(1::nat, 0::nat)"
-
-fun
-  my_plus :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
-where
-  "my_plus (x, y) (u, v) = (x + u, y + v)"
-
-quotient_definition
-  "PLUS :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
-is
-  "my_plus"
-
-fun
-  my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
-where
-  "my_neg (x, y) = (y, x)"
-
-quotient_definition
-  "NEG :: my_int \<Rightarrow> my_int"
-is
-  "my_neg"
-
-definition
-  MINUS :: "my_int \<Rightarrow> my_int \<Rightarrow> my_int"
-where
-  "MINUS z w = PLUS z (NEG w)"
-
-fun
-  my_mult :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
-where
-  "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
-
-quotient_definition
-  "MULT :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
-is
-  "my_mult"
-
-
-(* NOT SURE WETHER THIS DEFINITION IS CORRECT *)
-fun
-  my_le :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
-where
-  "my_le (x, y) (u, v) = (x+v \<le> u+y)"
-
-quotient_definition
-   "LE :: my_int \<Rightarrow> my_int \<Rightarrow> bool"
-is
-  "my_le"
-
-term LE
-thm LE_def
-
-
-definition
-  LESS :: "my_int \<Rightarrow> my_int \<Rightarrow> bool"
-where
-  "LESS z w = (LE z w \<and> z \<noteq> w)"
-
-term LESS
-thm LESS_def
-
-definition
-  ABS :: "my_int \<Rightarrow> my_int"
-where
-  "ABS i = (if (LESS i ZERO) then (NEG i) else i)"
-
-definition
-  SIGN :: "my_int \<Rightarrow> my_int"
-where
- "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))"
-
-print_quotconsts
-
-lemma plus_sym_pre:
-  shows "my_plus a b \<approx> my_plus b a"
-  apply(cases a)
-  apply(cases b)
-  apply(auto)
-  done
-
-lemma plus_rsp[quot_respect]:
-  shows "(intrel ===> intrel ===> intrel) my_plus my_plus"
-by (simp)
-
-lemma neg_rsp[quot_respect]:
-  shows "(op \<approx> ===> op \<approx>) my_neg my_neg"
-by simp
-
-lemma test1: "my_plus a b = my_plus a b"
-apply(rule refl)
-done
-
-lemma "PLUS a b = PLUS a b"
-apply(lifting_setup test1)
-apply(regularize)
-apply(injection)
-apply(cleaning)
-done
-
-thm lambda_prs
-
-lemma test2: "my_plus a = my_plus a"
-apply(rule refl)
-done
-
-lemma "PLUS a = PLUS a"
-apply(lifting_setup test2)
-apply(rule impI)
-apply(rule ballI)
-apply(rule apply_rsp[OF Quotient_my_int plus_rsp])
-apply(simp only: in_respects)
-apply(injection)
-apply(cleaning)
-done
-
-lemma test3: "my_plus = my_plus"
-apply(rule refl)
-done
-
-lemma "PLUS = PLUS"
-apply(lifting_setup test3)
-apply(rule impI)
-apply(rule plus_rsp)
-apply(injection)
-apply(cleaning)
-done
-
-
-lemma "PLUS a b = PLUS b a"
-apply(lifting plus_sym_pre)
-done
-
-lemma plus_assoc_pre:
-  shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"
-  apply (cases i)
-  apply (cases j)
-  apply (cases k)
-  apply (simp)
-  done
-
-lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"
-apply(lifting plus_assoc_pre)
-done
-
-lemma ex1tst: "Bex1_rel (op \<approx>) (\<lambda>x :: nat \<times> nat. x \<approx> x)"
-sorry
-
-lemma ex1tst': "\<exists>!(x::my_int). x = x"
-apply(lifting ex1tst)
-done
-
-
-lemma ho_tst: "foldl my_plus x [] = x"
-apply simp
-done
-
-
-term foldl
-lemma "foldl PLUS x [] = x"
-apply(lifting ho_tst)
-done
-
-lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)"
-sorry
-
-lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)"
-apply(lifting ho_tst2)
-done
-
-lemma ho_tst3: "foldl f (s::nat \<times> nat) ([]::(nat \<times> nat) list) = s"
-by simp
-
-lemma "foldl f (x::my_int) ([]::my_int list) = x"
-apply(lifting ho_tst3)
-done
-
-lemma lam_tst: "(\<lambda>x. (x, x)) y = (y, (y :: nat \<times> nat))"
-by simp
-
-(* Don't know how to keep the goal non-contracted... *)
-lemma "(\<lambda>x. (x, x)) (y::my_int) = (y, y)"
-apply(lifting lam_tst)
-done
-
-lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)"
-by simp
-
-lemma
-  shows "equivp (op \<approx>)"
-  and "equivp ((op \<approx>) ===> (op \<approx>))"
-(* Nitpick finds a counterexample! *)
-oops
-
-lemma lam_tst3a: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)"
-by auto
-
-lemma id_rsp:
-  shows "(R ===> R) id id"
-by simp
-
-lemma lam_tst3a_reg: "(op \<approx> ===> op \<approx>) (Babs (Respects op \<approx>) (\<lambda>y. y)) (Babs (Respects op \<approx>) (\<lambda>x. x))"
-apply (rule babs_rsp[OF Quotient_my_int])
-apply (simp add: id_rsp)
-done
-
-lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"
-apply(lifting lam_tst3a)
-apply(rule impI)
-apply(rule lam_tst3a_reg)
-done
-
-lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)"
-by auto
-
-lemma "(\<lambda>(y :: my_int => my_int). y) = (\<lambda>(x :: my_int => my_int). x)"
-apply(lifting lam_tst3b)
-apply(rule impI)
-apply(rule babs_rsp[OF fun_quotient[OF Quotient_my_int Quotient_my_int]])
-apply(simp add: id_rsp)
-done
-
-lemma lam_tst4: "map (\<lambda>x. my_plus x (0,0)) l = l"
-apply (induct l)
-apply simp
-apply (case_tac a)
-apply simp
-done
-
-lemma "map (\<lambda>x. PLUS x ZERO) l = l"
-apply(lifting lam_tst4)
-done
-
-end
diff -r fc5ce7f22b74 -r 13298f4b212b Attic/Quot/Examples/IntEx2.thy
--- a/Attic/Quot/Examples/IntEx2.thy	Wed Apr 28 08:32:33 2010 +0200
+++ b/Attic/Quot/Examples/IntEx2.thy	Wed Apr 28 17:05:20 2010 +0200
@@ -1,361 +1,7 @@
 theory IntEx2
-imports "../Quotient" "../Quotient_Product" Nat
-(*uses
-  ("Tools/numeral.ML")
-  ("Tools/numeral_syntax.ML")
-  ("Tools/int_arith.ML")*)
-begin
-
-fun
-  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
-where
-  "intrel (x, y) (u, v) = (x + v = u + y)"
-
-quotient_type int = "nat \<times> nat" / intrel
-  unfolding equivp_def
-  by (auto simp add: mem_def expand_fun_eq)
-
-instantiation int :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}"
+imports "Quotient_Int"
 begin
 
-ML {* @{term "0 \<Colon> int"} *}
-
-quotient_definition
-  "0 \<Colon> int" is "(0\<Colon>nat, 0\<Colon>nat)"
-
-quotient_definition
-  "1 \<Colon> int" is "(1\<Colon>nat, 0\<Colon>nat)"
-
-fun
-  plus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
-where
-  "plus_raw (x, y) (u, v) = (x + u, y + v)"
-
-quotient_definition
-  "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" is "plus_raw"
-
-fun
-  uminus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
-where
-  "uminus_raw (x, y) = (y, x)"
-
-quotient_definition
-  "(uminus \<Colon> (int \<Rightarrow> int))" is "uminus_raw"
-
-definition
-  minus_int_def [code del]:  "z - w = z + (-w\<Colon>int)"
-
-fun
-  mult_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
-where
-  "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
-
-quotient_definition
-  mult_int_def: "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" is "mult_raw"
-
-fun
-  le_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
-where
-  "le_raw (x, y) (u, v) = (x+v \<le> u+y)"
-
-quotient_definition
-  le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_raw"
-
-definition
-  less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
-
-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 ..
-
-end
-
-lemma plus_raw_rsp[quot_respect]:
-  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw"
-  by auto
-
-lemma uminus_raw_rsp[quot_respect]:
-  shows "(op \<approx> ===> op \<approx>) uminus_raw uminus_raw"
-  by auto
-
-lemma mult_raw_fst:
-  assumes a: "x \<approx> z"
-  shows "mult_raw x y \<approx> mult_raw z y"
-  using a
-  apply(cases x, cases y, cases z)
-  apply(auto simp add: mult_raw.simps intrel.simps)
-  apply(rename_tac u v w x y z)
-  apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
-  apply(simp add: mult_ac)
-  apply(simp add: add_mult_distrib [symmetric])
-  done
-
-lemma mult_raw_snd:
-  assumes a: "x \<approx> z"
-  shows "mult_raw y x \<approx> mult_raw y z"
-  using a
-  apply(cases x, cases y, cases z)
-  apply(auto simp add: mult_raw.simps intrel.simps)
-  apply(rename_tac u v w x y z)
-  apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
-  apply(simp add: mult_ac)
-  apply(simp add: add_mult_distrib [symmetric])
-  done
-
-lemma mult_raw_rsp[quot_respect]:
-  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"
-  apply(simp only: fun_rel_def)
-  apply(rule allI | rule impI)+
-  apply(rule equivp_transp[OF int_equivp])
-  apply(rule mult_raw_fst)
-  apply(assumption)
-  apply(rule mult_raw_snd)
-  apply(assumption)
-  done
-
-lemma le_raw_rsp[quot_respect]:
-  shows "(op \<approx> ===> op \<approx> ===> op =) le_raw le_raw"
-  by auto
-
-lemma plus_assoc_raw:
-  shows "plus_raw (plus_raw i j) k \<approx> plus_raw i (plus_raw j k)"
-  by (cases i, cases j, cases k) (simp)
-
-lemma plus_sym_raw:
-  shows "plus_raw i j \<approx> plus_raw j i"
-  by (cases i, cases j) (simp)
-
-lemma plus_zero_raw:
-  shows "plus_raw  (0, 0) i \<approx> i"
-  by (cases i) (simp)
-
-lemma plus_minus_zero_raw:
-  shows "plus_raw (uminus_raw i) i \<approx> (0, 0)"
-  by (cases i) (simp)
-
-lemma times_assoc_raw:
-  shows "mult_raw (mult_raw i j) k \<approx> mult_raw i (mult_raw j k)"
-  by (cases i, cases j, cases k) 
-     (simp add: algebra_simps)
-
-lemma times_sym_raw:
-  shows "mult_raw i j \<approx> mult_raw j i"
-  by (cases i, cases j) (simp add: algebra_simps)
-
-lemma times_one_raw:
-  shows "mult_raw  (1, 0) i \<approx> i"
-  by (cases i) (simp)
-
-lemma times_plus_comm_raw:
-  shows "mult_raw (plus_raw i j) k \<approx> plus_raw (mult_raw i k) (mult_raw j k)"
-by (cases i, cases j, cases k) 
-   (simp add: algebra_simps)
-
-lemma one_zero_distinct:
-  shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))"
-  by simp
-
-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 (lifting plus_assoc_raw)
-  show "i + j = j + i" 
-    by (lifting plus_sym_raw)
-  show "0 + i = (i::int)"
-    by (lifting plus_zero_raw)
-  show "- i + i = 0"
-    by (lifting plus_minus_zero_raw)
-  show "i - j = i + - j"
-    by (simp add: minus_int_def)
-  show "(i * j) * k = i * (j * k)"
-    by (lifting times_assoc_raw)
-  show "i * j = j * i"
-    by (lifting times_sym_raw)
-  show "1 * i = i"
-    by (lifting times_one_raw)
-  show "(i + j) * k = i * k + j * k"
-    by (lifting times_plus_comm_raw)
-  show "0 \<noteq> (1::int)"
-    by (lifting one_zero_distinct)
-qed
-
-lemma plus_raw_rsp_aux:
-  assumes a: "a \<approx> b" "c \<approx> d"
-  shows "plus_raw a c \<approx> plus_raw b d"
-  using a
-  by (cases a, cases b, cases c, cases d)
-     (simp)
-
-lemma add:
-  "(abs_int (x,y)) + (abs_int (u,v)) =
-   (abs_int (x + u, y + v))"
-  apply(simp add: plus_int_def id_simps)
-  apply(fold plus_raw.simps)
-  apply(rule Quotient_rel_abs[OF Quotient_int])
-  apply(rule plus_raw_rsp_aux)
-  apply(simp_all add: rep_abs_rsp_left[OF Quotient_int])
-  done
-
-definition int_of_nat_raw: 
-  "int_of_nat_raw m = (m :: nat, 0 :: nat)"
-
-quotient_definition
-  "int_of_nat :: nat \<Rightarrow> int" is "int_of_nat_raw"
-
-lemma[quot_respect]: 
-  shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"
-  by (simp add: equivp_reflp[OF int_equivp])
-
-lemma int_of_nat:
-  shows "of_nat m = int_of_nat m"
-  by (induct m)
-    (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add)
-
-lemma le_antisym_raw:
-  shows "le_raw i j \<Longrightarrow> le_raw j i \<Longrightarrow> i \<approx> j"
-  by (cases i, cases j) (simp)
-
-lemma le_refl_raw:
-  shows "le_raw i i"
-  by (cases i) (simp)
-
-lemma le_trans_raw:
-  shows "le_raw i j \<Longrightarrow> le_raw j k \<Longrightarrow> le_raw i k"
-  by (cases i, cases j, cases k) (simp)
-
-lemma le_cases_raw:
-  shows "le_raw i j \<or> le_raw j i"
-  by (cases i, cases j)
-     (simp add: linorder_linear)
-
-instance int :: linorder
-proof
-  fix i j k :: int
-  show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
-    by (lifting le_antisym_raw)
-  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 (lifting le_refl_raw)
-  show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
-    by (lifting le_trans_raw)
-  show "i \<le> j \<or> j \<le> i"
-    by (lifting le_cases_raw)
-qed
-
-instantiation int :: distrib_lattice
-begin
-
-definition
-  "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
-
-definition
-  "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
-
-instance
-  by intro_classes
-    (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
-
-end
-
-lemma le_plus_raw:
-  shows "le_raw i j \<Longrightarrow> le_raw (plus_raw k i) (plus_raw k j)"
-  by (cases i, cases j, cases k) (simp)
-
-instance int :: ordered_cancel_ab_semigroup_add
-proof
-  fix i j k :: int
-  show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
-    by (lifting le_plus_raw)
-qed
-
-abbreviation
-  "less_raw i j \<equiv> le_raw i j \<and> \<not>(i \<approx> j)"
-
-lemma zmult_zless_mono2_lemma:
-  fixes i j::int
-  and   k::nat
-  shows "i < j \<Longrightarrow> 0 < k \<Longrightarrow> of_nat k * i < of_nat k * j"
-  apply(induct "k")
-  apply(simp)
-  apply(case_tac "k = 0")
-  apply(simp_all add: left_distrib add_strict_mono)
-  done
-
-lemma zero_le_imp_eq_int_raw:
-  fixes k::"(nat \<times> nat)"
-  shows "less_raw (0, 0) k \<Longrightarrow> (\<exists>n > 0. k \<approx> int_of_nat_raw n)"
-  apply(cases k)
-  apply(simp add:int_of_nat_raw)
-  apply(auto)
-  apply(rule_tac i="b" and j="a" in less_Suc_induct)
-  apply(auto)
-  done
-
-lemma zero_le_imp_eq_int:
-  fixes k::int
-  shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n"
-  unfolding less_int_def int_of_nat
-  by (lifting zero_le_imp_eq_int_raw)
-
-lemma zmult_zless_mono2: 
-  fixes i j k::int
-  assumes a: "i < j" "0 < k"
-  shows "k * i < k * j"
-  using a
-  by (drule_tac zero_le_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma)
-
-text{*The integers form an ordered integral domain*}
-instance int :: linordered_idom
-proof
-  fix i j k :: int
-  show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
-    by (rule zmult_zless_mono2)
-  show "\<bar>i\<bar> = (if i < 0 then -i else i)"
-    by (simp only: zabs_def)
-  show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
-    by (simp only: zsgn_def)
-qed
-
-lemmas int_distrib =
-  left_distrib [of "z1::int" "z2" "w", standard]
-  right_distrib [of "w::int" "z1" "z2", standard]
-  left_diff_distrib [of "z1::int" "z2" "w", standard]
-  right_diff_distrib [of "w::int" "z1" "z2", standard]
-
-lemma int_induct_raw:
-  assumes a: "P (0::nat, 0)"
-  and     b: "\<And>i. P i \<Longrightarrow> P (plus_raw i (1, 0))"
-  and     c: "\<And>i. P i \<Longrightarrow> P (plus_raw i (uminus_raw (1, 0)))"
-  shows      "P x"
-proof (cases x, clarify)
-  fix a b
-  show "P (a, b)"
-  proof (induct a arbitrary: b rule: Nat.induct)
-    case zero
-    show "P (0, b)" using assms by (induct b) auto
-  next
-    case (Suc n)
-    then show ?case using assms by auto
-  qed
-qed
-
-lemma int_induct:
-  fixes x :: int
-  assumes a: "P 0"
-  and     b: "\<And>i. P i \<Longrightarrow> P (i + 1)"
-  and     c: "\<And>i. P i \<Longrightarrow> P (i - 1)"
-  shows      "P x"
-  using a b c unfolding minus_int_def
-  by (lifting int_induct_raw)
-
 subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}
 
 (*
diff -r fc5ce7f22b74 -r 13298f4b212b Attic/Quot/Examples/Quotient_Int.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/Quot/Examples/Quotient_Int.thy	Wed Apr 28 17:05:20 2010 +0200
@@ -0,0 +1,379 @@
+(*  Title:      HOL/Quotient_Examples/Quotient_Int.thy
+    Author:     Cezary Kaliszyk
+    Author:     Christian Urban
+
+Integers based on Quotients.
+*)
+theory Quotient_Int
+imports Quotient_Product Nat
+begin
+
+fun
+  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
+where
+  "intrel (x, y) (u, v) = (x + v = u + y)"
+
+quotient_type int = "nat \<times> nat" / intrel
+  by (auto simp add: equivp_def expand_fun_eq)
+
+instantiation int :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}"
+begin
+
+quotient_definition
+  "0 \<Colon> int" is "(0\<Colon>nat, 0\<Colon>nat)"
+
+quotient_definition
+  "1 \<Colon> int" is "(1\<Colon>nat, 0\<Colon>nat)"
+
+fun
+  plus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+  "plus_int_raw (x, y) (u, v) = (x + u, y + v)"
+
+quotient_definition
+  "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" is "plus_int_raw"
+
+fun
+  uminus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+  "uminus_int_raw (x, y) = (y, x)"
+
+quotient_definition
+  "(uminus \<Colon> (int \<Rightarrow> int))" is "uminus_int_raw"
+
+definition
+  minus_int_def [code del]:  "z - w = z + (-w\<Colon>int)"
+
+fun
+  times_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+  "times_int_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
+
+quotient_definition
+  "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" is "times_int_raw"
+
+fun
+  le_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
+where
+  "le_int_raw (x, y) (u, v) = (x+v \<le> u+y)"
+
+quotient_definition
+  le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_int_raw"
+
+definition
+  less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
+
+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 ..
+
+end
+
+lemma [quot_respect]:
+  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_int_raw plus_int_raw"
+  and   "(op \<approx> ===> op \<approx>) uminus_int_raw uminus_int_raw"
+  and   "(op \<approx> ===> op \<approx> ===> op =) le_int_raw le_int_raw"
+  by auto
+
+lemma times_int_raw_fst:
+  assumes a: "x \<approx> z"
+  shows "times_int_raw x y \<approx> times_int_raw z y"
+  using a
+  apply(cases x, cases y, cases z)
+  apply(auto simp add: times_int_raw.simps intrel.simps)
+  apply(rename_tac u v w x y z)
+  apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
+  apply(simp add: mult_ac)
+  apply(simp add: add_mult_distrib [symmetric])
+  done
+
+lemma times_int_raw_snd:
+  assumes a: "x \<approx> z"
+  shows "times_int_raw y x \<approx> times_int_raw y z"
+  using a
+  apply(cases x, cases y, cases z)
+  apply(auto simp add: times_int_raw.simps intrel.simps)
+  apply(rename_tac u v w x y z)
+  apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
+  apply(simp add: mult_ac)
+  apply(simp add: add_mult_distrib [symmetric])
+  done
+
+lemma [quot_respect]:
+  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) times_int_raw times_int_raw"
+  apply(simp only: fun_rel_def)
+  apply(rule allI | rule impI)+
+  apply(rule equivp_transp[OF int_equivp])
+  apply(rule times_int_raw_fst)
+  apply(assumption)
+  apply(rule times_int_raw_snd)
+  apply(assumption)
+  done
+
+lemma plus_assoc_raw:
+  shows "plus_int_raw (plus_int_raw i j) k \<approx> plus_int_raw i (plus_int_raw j k)"
+  by (cases i, cases j, cases k) (simp)
+
+lemma plus_sym_raw:
+  shows "plus_int_raw i j \<approx> plus_int_raw j i"
+  by (cases i, cases j) (simp)
+
+lemma plus_zero_raw:
+  shows "plus_int_raw (0, 0) i \<approx> i"
+  by (cases i) (simp)
+
+lemma plus_minus_zero_raw:
+  shows "plus_int_raw (uminus_int_raw i) i \<approx> (0, 0)"
+  by (cases i) (simp)
+
+lemma times_assoc_raw:
+  shows "times_int_raw (times_int_raw i j) k \<approx> times_int_raw i (times_int_raw j k)"
+  by (cases i, cases j, cases k)
+     (simp add: algebra_simps)
+
+lemma times_sym_raw:
+  shows "times_int_raw i j \<approx> times_int_raw j i"
+  by (cases i, cases j) (simp add: algebra_simps)
+
+lemma times_one_raw:
+  shows "times_int_raw  (1, 0) i \<approx> i"
+  by (cases i) (simp)
+
+lemma times_plus_comm_raw:
+  shows "times_int_raw (plus_int_raw i j) k \<approx> plus_int_raw (times_int_raw i k) (times_int_raw j k)"
+by (cases i, cases j, cases k)
+   (simp add: algebra_simps)
+
+lemma one_zero_distinct:
+  shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))"
+  by simp
+
+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 (lifting plus_assoc_raw)
+  show "i + j = j + i"
+    by (lifting plus_sym_raw)
+  show "0 + i = (i::int)"
+    by (lifting plus_zero_raw)
+  show "- i + i = 0"
+    by (lifting plus_minus_zero_raw)
+  show "i - j = i + - j"
+    by (simp add: minus_int_def)
+  show "(i * j) * k = i * (j * k)"
+    by (lifting times_assoc_raw)
+  show "i * j = j * i"
+    by (lifting times_sym_raw)
+  show "1 * i = i"
+    by (lifting times_one_raw)
+  show "(i + j) * k = i * k + j * k"
+    by (lifting times_plus_comm_raw)
+  show "0 \<noteq> (1::int)"
+    by (lifting one_zero_distinct)
+qed
+
+lemma plus_int_raw_rsp_aux:
+  assumes a: "a \<approx> b" "c \<approx> d"
+  shows "plus_int_raw a c \<approx> plus_int_raw b d"
+  using a
+  by (cases a, cases b, cases c, cases d)
+     (simp)
+
+lemma add_abs_int:
+  "(abs_int (x,y)) + (abs_int (u,v)) =
+   (abs_int (x + u, y + v))"
+  apply(simp add: plus_int_def id_simps)
+  apply(fold plus_int_raw.simps)
+  apply(rule Quotient_rel_abs[OF Quotient_int])
+  apply(rule plus_int_raw_rsp_aux)
+  apply(simp_all add: rep_abs_rsp_left[OF Quotient_int])
+  done
+
+definition int_of_nat_raw:
+  "int_of_nat_raw m = (m :: nat, 0 :: nat)"
+
+quotient_definition
+  "int_of_nat :: nat \<Rightarrow> int" is "int_of_nat_raw"
+
+lemma[quot_respect]:
+  shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"
+  by (simp add: equivp_reflp[OF int_equivp])
+
+lemma int_of_nat:
+  shows "of_nat m = int_of_nat m"
+  by (induct m)
+     (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add_abs_int)
+
+lemma le_antisym_raw:
+  shows "le_int_raw i j \<Longrightarrow> le_int_raw j i \<Longrightarrow> i \<approx> j"
+  by (cases i, cases j) (simp)
+
+lemma le_refl_raw:
+  shows "le_int_raw i i"
+  by (cases i) (simp)
+
+lemma le_trans_raw:
+  shows "le_int_raw i j \<Longrightarrow> le_int_raw j k \<Longrightarrow> le_int_raw i k"
+  by (cases i, cases j, cases k) (simp)
+
+lemma le_cases_raw:
+  shows "le_int_raw i j \<or> le_int_raw j i"
+  by (cases i, cases j)
+     (simp add: linorder_linear)
+
+instance int :: linorder
+proof
+  fix i j k :: int
+  show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
+    by (lifting le_antisym_raw)
+  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 (lifting le_refl_raw)
+  show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
+    by (lifting le_trans_raw)
+  show "i \<le> j \<or> j \<le> i"
+    by (lifting le_cases_raw)
+qed
+
+instantiation int :: distrib_lattice
+begin
+
+definition
+  "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
+
+definition
+  "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
+
+instance
+  by intro_classes
+    (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
+
+end
+
+lemma le_plus_int_raw:
+  shows "le_int_raw i j \<Longrightarrow> le_int_raw (plus_int_raw k i) (plus_int_raw k j)"
+  by (cases i, cases j, cases k) (simp)
+
+instance int :: ordered_cancel_ab_semigroup_add
+proof
+  fix i j k :: int
+  show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
+    by (lifting le_plus_int_raw)
+qed
+
+abbreviation
+  "less_int_raw i j \<equiv> le_int_raw i j \<and> \<not>(i \<approx> j)"
+
+lemma zmult_zless_mono2_lemma:
+  fixes i j::int
+  and   k::nat
+  shows "i < j \<Longrightarrow> 0 < k \<Longrightarrow> of_nat k * i < of_nat k * j"
+  apply(induct "k")
+  apply(simp)
+  apply(case_tac "k = 0")
+  apply(simp_all add: left_distrib add_strict_mono)
+  done
+
+lemma zero_le_imp_eq_int_raw:
+  fixes k::"(nat \<times> nat)"
+  shows "less_int_raw (0, 0) k \<Longrightarrow> (\<exists>n > 0. k \<approx> int_of_nat_raw n)"
+  apply(cases k)
+  apply(simp add:int_of_nat_raw)
+  apply(auto)
+  apply(rule_tac i="b" and j="a" in less_Suc_induct)
+  apply(auto)
+  done
+
+lemma zero_le_imp_eq_int:
+  fixes k::int
+  shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n"
+  unfolding less_int_def int_of_nat
+  by (lifting zero_le_imp_eq_int_raw)
+
+lemma zmult_zless_mono2:
+  fixes i j k::int
+  assumes a: "i < j" "0 < k"
+  shows "k * i < k * j"
+  using a
+  by (drule_tac zero_le_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma)
+
+text{*The integers form an ordered integral domain*}
+instance int :: linordered_idom
+proof
+  fix i j k :: int
+  show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
+    by (rule zmult_zless_mono2)
+  show "\<bar>i\<bar> = (if i < 0 then -i else i)"
+    by (simp only: zabs_def)
+  show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
+    by (simp only: zsgn_def)
+qed
+
+lemmas int_distrib =
+  left_distrib [of "z1::int" "z2" "w", standard]
+  right_distrib [of "w::int" "z1" "z2", standard]
+  left_diff_distrib [of "z1::int" "z2" "w", standard]
+  right_diff_distrib [of "w::int" "z1" "z2", standard]
+  minus_add_distrib[of "z1::int" "z2", standard]
+
+lemma int_induct_raw:
+  assumes a: "P (0::nat, 0)"
+  and     b: "\<And>i. P i \<Longrightarrow> P (plus_int_raw i (1, 0))"
+  and     c: "\<And>i. P i \<Longrightarrow> P (plus_int_raw i (uminus_int_raw (1, 0)))"
+  shows      "P x"
+proof (cases x, clarify)
+  fix a b
+  show "P (a, b)"
+  proof (induct a arbitrary: b rule: Nat.induct)
+    case zero
+    show "P (0, b)" using assms by (induct b) auto
+  next
+    case (Suc n)
+    then show ?case using assms by auto
+  qed
+qed
+
+lemma int_induct:
+  fixes x :: int
+  assumes a: "P 0"
+  and     b: "\<And>i. P i \<Longrightarrow> P (i + 1)"
+  and     c: "\<And>i. P i \<Longrightarrow> P (i - 1)"
+  shows      "P x"
+  using a b c unfolding minus_int_def
+  by (lifting int_induct_raw)
+
+text {* Magnitide of an Integer, as a Natural Number: @{term nat} *}
+
+definition
+  "int_to_nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"
+
+quotient_definition
+  "int_to_nat::int \<Rightarrow> nat"
+is
+  "int_to_nat_raw"
+
+lemma [quot_respect]:
+  shows "(intrel ===> op =) int_to_nat_raw int_to_nat_raw"
+  by (auto iff: int_to_nat_raw_def)
+
+lemma nat_le_eq_zle_raw:
+  assumes a: "less_int_raw (0, 0) w \<or> le_int_raw (0, 0) z"
+  shows "(int_to_nat_raw w \<le> int_to_nat_raw z) = (le_int_raw w z)"
+  using a
+  by (cases w, cases z) (auto simp add: int_to_nat_raw_def)
+
+lemma nat_le_eq_zle:
+  fixes w z::"int"
+  shows "0 < w \<or> 0 \<le> z \<Longrightarrow> (int_to_nat w \<le> int_to_nat z) = (w \<le> z)"
+  unfolding less_int_def
+  by (lifting nat_le_eq_zle_raw)
+
+end