# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260411942 -3600
# Node ID 8aa67d037b3cd14c8e040156449baaf0e000b3d6
# Parent  3c6419a5a7fc9f8780313fbd85358b36f53175fa# Parent  fe64784b38c3c8f4d84f15631913a1886f591877
merged

diff -r 3c6419a5a7fc -r 8aa67d037b3c Quot/Examples/IntEx2.thy
--- a/Quot/Examples/IntEx2.thy	Thu Dec 10 03:11:19 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Thu Dec 10 03:25:42 2009 +0100
@@ -218,9 +218,22 @@
 apply(simp_all add: rep_abs_rsp_left[OF Quotient_int])
 done
 
-lemma int_def: 
-  shows "of_nat m = ABS_int (m, 0)"
-by (induct m) (simp_all add: zero_int_def one_int_def add)
+definition int_of_nat_raw: 
+  "int_of_nat_raw m = (m :: nat, 0 :: nat)"
+
+quotient_def
+  int_of_nat :: "int_of_nat :: nat \<Rightarrow> int" 
+where "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_def:
+  shows "of_nat m = int_of_nat m"
+apply (induct m)
+apply (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add)
+done
 
 lemma le_antisym_raw:
   shows "less_eq_raw i j \<Longrightarrow> less_eq_raw j i \<Longrightarrow> i \<approx> j"
@@ -297,7 +310,7 @@
 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 (minus_raw (1,0)))"
+  and     c: "\<And>i. P i \<Longrightarrow> P (plus_raw i (uminus_raw (1,0)))"
   shows      "P x"
 apply(case_tac x) apply(simp)
 apply(rule_tac x="b" in spec)
@@ -314,17 +327,30 @@
   shows      "P x"
 using a b c by (lifting int_induct_raw)
 
-lemma zero_le_imp_eq_int: 
+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"
-sorry
+  shows "0 < k \<Longrightarrow> \<exists>n > 0. k = int_of_nat n"
+  unfolding less_int_def 
+  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
+using a
 apply(drule_tac zero_le_imp_eq_int)
+apply(fold int_def)
 apply(auto simp add: zmult_zless_mono2_lemma)
 done