--- a/Quot/Examples/IntEx.thy	Thu Dec 10 08:44:01 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Thu Dec 10 08:55:30 2009 +0100
@@ -113,6 +113,10 @@
   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
@@ -175,6 +179,27 @@
 apply(tactic {* clean_tac @{context} 1 *})
 done
 
+lemma int_induct_raw:
+  assumes a: "P (0::nat, 0)"
+  and     b: "\<And>i. P i \<Longrightarrow> P (my_plus i (1,0))"
+  and     c: "\<And>i. P i \<Longrightarrow> P (my_plus i (my_neg (1,0)))"
+  shows      "P x"
+  apply(case_tac x) apply(simp)
+  apply(rule_tac x="b" in spec)
+  apply(rule_tac Nat.induct)
+  apply(rule allI)
+  apply(rule_tac Nat.induct)
+  using a b c apply(auto)
+  done
+
+lemma int_induct:
+  assumes a: "P ZERO"
+  and     b: "\<And>i. P i \<Longrightarrow> P (PLUS i ONE)"
+  and     c: "\<And>i. P i \<Longrightarrow> P (PLUS i (NEG ONE))"
+  shows      "P x"
+  using a b c
+  by (lifting int_induct_raw)
+
 lemma ho_tst: "foldl my_plus x [] = x"
 apply simp
 done

--- a/Quot/Examples/IntEx2.thy	Thu Dec 10 08:44:01 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Thu Dec 10 08:55:30 2009 +0100
@@ -225,7 +225,7 @@
   shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"
 by (simp add: equivp_reflp[OF int_equivp])
 
-lemma int_def:
+lemma int_of_nat:
   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)
@@ -303,26 +303,6 @@
 apply(simp_all add: left_distrib add_strict_mono)
 done
 
-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"
-apply(case_tac x) apply(simp)
-apply(rule_tac x="b" in spec)
-apply(rule_tac Nat.induct)
-apply(rule allI)
-apply(rule_tac Nat.induct)
-using a b c apply(auto)
-done
-
-lemma int_induct:
-  assumes a: "P (0::int)"
-  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 by (lifting int_induct_raw)
-
 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)"
@@ -335,8 +315,8 @@
 
 lemma zero_le_imp_eq_int:
   fixes k::int
-  shows "0 < k \<Longrightarrow> \<exists>n > 0. k = int_of_nat n"
-  unfolding less_int_def 
+  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: 
@@ -346,7 +326,6 @@
 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