# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260392711 -3600
# Node ID 217db3103f6a4e93a790b841652d13ea058d229e
# Parent  c636858377066d092379ef3898fc16b1250f9ba0
slightly more on IntEx2

diff -r c63685837706 -r 217db3103f6a Quot/Examples/IntEx2.thy
--- a/Quot/Examples/IntEx2.thy	Wed Dec 09 20:35:52 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Wed Dec 09 22:05:11 2009 +0100
@@ -24,8 +24,6 @@
 where
   "(0::nat, 0::nat)"
 
-thm zero_int_def
-
 quotient_def
   one_int::"1 :: int"
 where
@@ -172,15 +170,12 @@
   shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))"
   by simp
 
-text{*The integers form a @{text comm_ring_1}*}
+text{* The integers form a @{text comm_ring_1}*}
 
 ML {* qconsts_lookup @{theory} @{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} *}
-
 ML {* dest_Type (snd (dest_Const @{term "0 :: int"})) *}
 ML {* @{term "0 :: int"} *}
 
-thm plus_assoc_raw
-
 instance int :: comm_ring_1
 proof
   fix i j k :: int
@@ -206,15 +201,18 @@
     by (lifting one_zero_distinct)
 qed
 
-term of_nat
-thm of_nat_def
+
+lemma add:
+     "(ABS_int (x,y)) + (ABS_int (u,v)) =
+      (ABS_int (x+u, y+v))"
+apply(simp add: plus_int_def)
+sorry
 
 lemma int_def: "of_nat m = ABS_int (m, 0)"
 apply(induct m)
 apply(simp add: zero_int_def)
-apply(simp)
-apply(simp add: plus_int_def one_int_def)
-oops
+apply(simp add: one_int_def add)
+done
 
 lemma le_antisym_raw:
   shows "less_eq_raw i j \<Longrightarrow> less_eq_raw j i \<Longrightarrow> i \<approx> j"
@@ -275,11 +273,20 @@
     by (lifting le_plus_raw)
 qed
 
+abbreviation
+  "less_raw i j \<equiv> less_eq_raw i j \<and> \<not>(i \<approx> j)"
+
+
 lemma test:
-  "\<lbrakk>less_eq_raw i j \<and> \<not>i \<approx> j; less_eq_raw (0, 0) k \<and> \<not>(0, 0) \<approx> k\<rbrakk>
-    \<Longrightarrow> less_eq_raw (times_raw k i) (times_raw k j) \<and> \<not>times_raw k i \<approx> times_raw k j"
+  "\<lbrakk>less_raw i j; less_raw (0, 0) k\<rbrakk>
+    \<Longrightarrow> less_raw (times_raw k i) (times_raw k j)"
 apply(cases i, cases j, cases k)
-apply(auto simp add: algebra_simps)
+apply(simp only: less_eq_raw.simps times_raw.simps)
+apply(simp)
+apply(rename_tac u v w x y z)
+apply(rule conjI)
+apply(subgoal_tac "y*u + y*x \<le> y*w + y*v  &  z*v \<le> y*v")
+apply(simp add: )
 sorry