tuned proofs

--- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Mon Apr 02 18:12:53 2012 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Mon Apr 02 21:26:07 2012 +0100
@@ -255,31 +255,25 @@
   minus_add_distrib[of z1 z2]
   for z1 z2 w :: int
 
-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_induct2:
+  assumes "P 0 0"
+  and     "\<And>n m. P n m \<Longrightarrow> P (Suc n) m"
+  and     "\<And>n m. P n m \<Longrightarrow> P n (Suc m)"
+  shows   "P n m"
+using assms
+by (induction_schema) (pat_completeness, lexicographic_order)
+
 
 lemma int_induct:
-  fixes x :: int
+  fixes j :: 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)
+  and     b: "\<And>i::int. P i \<Longrightarrow> P (i + 1)"
+  and     c: "\<And>i::int. P i \<Longrightarrow> P (i - 1)"
+  shows      "P j"
+using a b c 
+unfolding minus_int_def
+by (descending) (auto intro: int_induct2)
+  
 
 text {* Magnitide of an Integer, as a Natural Number: @{term nat} *}
 
@@ -289,7 +283,8 @@
 quotient_definition
   "int_to_nat::int \<Rightarrow> nat"
 is
-  "int_to_nat_raw" unfolding int_to_nat_raw_def by force
+  "int_to_nat_raw" 
+unfolding int_to_nat_raw_def by auto 
 
 lemma nat_le_eq_zle:
   fixes w z::"int"

--- a/src/HOL/Quotient_Examples/Quotient_Message.thy	Mon Apr 02 18:12:53 2012 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Message.thy	Mon Apr 02 21:26:07 2012 +0100
@@ -307,20 +307,15 @@
   thus "Decrypt K X = Decrypt K X'" by simp
 qed
 
-lemma msg_induct_aux:
-  shows "\<lbrakk>\<And>N. P (Nonce N);
-          \<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y);
-          \<And>K X. P X \<Longrightarrow> P (Crypt K X);
-          \<And>K X. P X \<Longrightarrow> P (Decrypt K X)\<rbrakk> \<Longrightarrow> P msg"
-  by (lifting freemsg.induct)
-
 lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:
   assumes N: "\<And>N. P (Nonce N)"
       and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)"
       and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
       and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"
   shows "P msg"
-  using N M C D by (rule msg_induct_aux)
+  using N M C D 
+  by (descending) (auto intro: freemsg.induct)
+
 
 subsection{*The Abstract Discriminator*}