# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260406075 -3600
# Node ID 35fbace8d48d8399d9f0c4be68b97ecccc3dee60
# Parent  94d6d29459c9c99bff094a2fc910976d7ae908ac
naming in this file cannot be made to agree to the original (PROBLEM?)

diff -r 94d6d29459c9 -r 35fbace8d48d Quot/Examples/IntEx2.thy
--- a/Quot/Examples/IntEx2.thy	Wed Dec 09 23:32:16 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Thu Dec 10 01:47:55 2009 +0100
@@ -12,9 +12,8 @@
   "intrel (x, y) (u, v) = (x + v = u + y)"
 
 quotient int = "nat \<times> nat" / intrel
-  apply(unfold equivp_def)
-  apply(auto simp add: mem_def expand_fun_eq)
-  done
+  unfolding equivp_def
+  by (auto simp add: mem_def expand_fun_eq)
 
 instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
 begin
@@ -40,14 +39,14 @@
   "plus_raw"
 
 fun
-  minus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+  uminus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
 where
-  "minus_raw (x, y) = (y, x)"
+  "uminus_raw (x, y) = (y, x)"
 
 quotient_def
   uminus_int::"(uminus :: (int \<Rightarrow> int))"
 where
-  "minus_raw"
+  "uminus_raw"
 
 definition
   minus_int_def [code del]:  "z - w = z + (-w::int)"
@@ -62,6 +61,7 @@
 where
   "times_raw"
 
+(* PROBLEM: this should be called le_int and le_raw / or odd *)
 fun
   less_eq_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
 where
@@ -90,7 +90,7 @@
 by auto
 
 lemma minus_raw_rsp[quot_respect]:
-  shows "(op \<approx> ===> op \<approx>) minus_raw minus_raw"
+  shows "(op \<approx> ===> op \<approx>) uminus_raw uminus_raw"
   by auto
 
 lemma times_raw_fst:
@@ -117,7 +117,7 @@
 apply(simp add: add_mult_distrib [symmetric])
 done
 
-lemma mult_raw_rsp[quot_respect]:
+lemma times_raw_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) times_raw times_raw"
 apply(simp only: fun_rel.simps)
 apply(rule allI | rule impI)+
@@ -145,7 +145,7 @@
 by (cases i) (simp)
 
 lemma plus_minus_zero_raw:
-  shows "plus_raw (minus_raw i) i \<approx> (0, 0)"
+  shows "plus_raw (uminus_raw i) i \<approx> (0, 0)"
 by (cases i) (simp)
 
 lemma times_assoc_raw: