# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272010894 -7200
# Node ID 19f296e757c55e2de4772fe44cc920cfb10e523a
# Parent  3641d055b260dfb4af798644d543996ec8ac0a1f
Minor cleaning of IntEx

diff -r 3641d055b260 -r 19f296e757c5 Attic/Quot/Examples/IntEx.thy
--- a/Attic/Quot/Examples/IntEx.thy	Fri Apr 23 09:54:42 2010 +0200
+++ b/Attic/Quot/Examples/IntEx.thy	Fri Apr 23 10:21:34 2010 +0200
@@ -165,27 +165,6 @@
 apply(lifting plus_assoc_pre)
 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 ex1tst: "Bex1_rel (op \<approx>) (\<lambda>x :: nat \<times> nat. x \<approx> x)"
 sorry
 
diff -r 3641d055b260 -r 19f296e757c5 Attic/Quot/Examples/IntEx2.thy
--- a/Attic/Quot/Examples/IntEx2.thy	Fri Apr 23 09:54:42 2010 +0200
+++ b/Attic/Quot/Examples/IntEx2.thy	Fri Apr 23 10:21:34 2010 +0200
@@ -76,7 +76,7 @@
 
 lemma plus_raw_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw"
-by auto
+  by auto
 
 lemma uminus_raw_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx>) uminus_raw uminus_raw"
@@ -85,70 +85,70 @@
 lemma mult_raw_fst:
   assumes a: "x \<approx> z"
   shows "mult_raw x y \<approx> mult_raw z y"
-using a
-apply(cases x, cases y, cases z)
-apply(auto simp add: mult_raw.simps intrel.simps)
-apply(rename_tac u v w x y z)
-apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
-apply(simp add: mult_ac)
-apply(simp add: add_mult_distrib [symmetric])
-done
+  using a
+  apply(cases x, cases y, cases z)
+  apply(auto simp add: mult_raw.simps intrel.simps)
+  apply(rename_tac u v w x y z)
+  apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
+  apply(simp add: mult_ac)
+  apply(simp add: add_mult_distrib [symmetric])
+  done
 
 lemma mult_raw_snd:
   assumes a: "x \<approx> z"
   shows "mult_raw y x \<approx> mult_raw y z"
-using a
-apply(cases x, cases y, cases z)
-apply(auto simp add: mult_raw.simps intrel.simps)
-apply(rename_tac u v w x y z)
-apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
-apply(simp add: mult_ac)
-apply(simp add: add_mult_distrib [symmetric])
-done
+  using a
+  apply(cases x, cases y, cases z)
+  apply(auto simp add: mult_raw.simps intrel.simps)
+  apply(rename_tac u v w x y z)
+  apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
+  apply(simp add: mult_ac)
+  apply(simp add: add_mult_distrib [symmetric])
+  done
 
 lemma mult_raw_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"
-apply(simp only: fun_rel_def)
-apply(rule allI | rule impI)+
-apply(rule equivp_transp[OF int_equivp])
-apply(rule mult_raw_fst)
-apply(assumption)
-apply(rule mult_raw_snd)
-apply(assumption)
-done
+  apply(simp only: fun_rel_def)
+  apply(rule allI | rule impI)+
+  apply(rule equivp_transp[OF int_equivp])
+  apply(rule mult_raw_fst)
+  apply(assumption)
+  apply(rule mult_raw_snd)
+  apply(assumption)
+  done
 
 lemma le_raw_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op =) le_raw le_raw"
-by auto
+  by auto
 
 lemma plus_assoc_raw:
   shows "plus_raw (plus_raw i j) k \<approx> plus_raw i (plus_raw j k)"
-by (cases i, cases j, cases k) (simp)
+  by (cases i, cases j, cases k) (simp)
 
 lemma plus_sym_raw:
   shows "plus_raw i j \<approx> plus_raw j i"
-by (cases i, cases j) (simp)
+  by (cases i, cases j) (simp)
 
 lemma plus_zero_raw:
   shows "plus_raw  (0, 0) i \<approx> i"
-by (cases i) (simp)
+  by (cases i) (simp)
 
 lemma plus_minus_zero_raw:
   shows "plus_raw (uminus_raw i) i \<approx> (0, 0)"
-by (cases i) (simp)
+  by (cases i) (simp)
 
 lemma times_assoc_raw:
   shows "mult_raw (mult_raw i j) k \<approx> mult_raw i (mult_raw j k)"
-by (cases i, cases j, cases k) 
-   (simp add: algebra_simps)
+  by (cases i, cases j, cases k) 
+     (simp add: algebra_simps)
 
 lemma times_sym_raw:
   shows "mult_raw i j \<approx> mult_raw j i"
-by (cases i, cases j) (simp add: algebra_simps)
+  by (cases i, cases j) (simp add: algebra_simps)
 
 lemma times_one_raw:
   shows "mult_raw  (1, 0) i \<approx> i"
-by (cases i) (simp)
+  by (cases i) (simp)
 
 lemma times_plus_comm_raw:
   shows "mult_raw (plus_raw i j) k \<approx> plus_raw (mult_raw i k) (mult_raw j k)"
@@ -189,19 +189,19 @@
 lemma plus_raw_rsp_aux:
   assumes a: "a \<approx> b" "c \<approx> d"
   shows "plus_raw a c \<approx> plus_raw b d"
-using a
-by (cases a, cases b, cases c, cases d) 
-   (simp)
+  using a
+  by (cases a, cases b, cases c, cases d)
+     (simp)
 
 lemma add:
-     "(abs_int (x,y)) + (abs_int (u,v)) =
-      (abs_int (x + u, y + v))"
-apply(simp add: plus_int_def id_simps)
-apply(fold plus_raw.simps)
-apply(rule Quotient_rel_abs[OF Quotient_int])
-apply(rule plus_raw_rsp_aux)
-apply(simp_all add: rep_abs_rsp_left[OF Quotient_int])
-done
+  "(abs_int (x,y)) + (abs_int (u,v)) =
+   (abs_int (x + u, y + v))"
+  apply(simp add: plus_int_def id_simps)
+  apply(fold plus_raw.simps)
+  apply(rule Quotient_rel_abs[OF Quotient_int])
+  apply(rule plus_raw_rsp_aux)
+  apply(simp_all add: rep_abs_rsp_left[OF Quotient_int])
+  done
 
 definition int_of_nat_raw: 
   "int_of_nat_raw m = (m :: nat, 0 :: nat)"
@@ -211,30 +211,29 @@
 
 lemma[quot_respect]: 
   shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"
-by (simp add: equivp_reflp[OF int_equivp])
+  by (simp add: equivp_reflp[OF int_equivp])
 
 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)
-done
+  by (induct m)
+    (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add)
 
 lemma le_antisym_raw:
   shows "le_raw i j \<Longrightarrow> le_raw j i \<Longrightarrow> i \<approx> j"
-by (cases i, cases j) (simp)
+  by (cases i, cases j) (simp)
 
 lemma le_refl_raw:
   shows "le_raw i i"
-by (cases i) (simp)
+  by (cases i) (simp)
 
 lemma le_trans_raw:
   shows "le_raw i j \<Longrightarrow> le_raw j k \<Longrightarrow> le_raw i k"
-by (cases i, cases j, cases k) (simp)
+  by (cases i, cases j, cases k) (simp)
 
 lemma le_cases_raw:
   shows "le_raw i j \<or> le_raw j i"
-by (cases i, cases j) 
-   (simp add: linorder_linear)
+  by (cases i, cases j)
+     (simp add: linorder_linear)
 
 instance int :: linorder
 proof
@@ -268,8 +267,7 @@
 
 lemma le_plus_raw:
   shows "le_raw i j \<Longrightarrow> le_raw (plus_raw k i) (plus_raw k j)"
-by (cases i, cases j, cases k) (simp)
-
+  by (cases i, cases j, cases k) (simp)
 
 instance int :: ordered_cancel_ab_semigroup_add
 proof
@@ -285,21 +283,21 @@
   fixes i j::int
   and   k::nat
   shows "i < j \<Longrightarrow> 0 < k \<Longrightarrow> of_nat k * i < of_nat k * j"
-apply(induct "k")
-apply(simp)
-apply(case_tac "k = 0")
-apply(simp_all add: left_distrib add_strict_mono)
-done
+  apply(induct "k")
+  apply(simp)
+  apply(case_tac "k = 0")
+  apply(simp_all add: left_distrib add_strict_mono)
+  done
 
 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
+  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
@@ -311,11 +309,8 @@
   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(auto simp add: zmult_zless_mono2_lemma)
-done
+  using a
+  by (drule_tac zero_le_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma)
 
 text{*The integers form an ordered integral domain*}
 instance int :: linordered_idom
@@ -335,6 +330,31 @@
   left_diff_distrib [of "z1::int" "z2" "w", standard]
   right_diff_distrib [of "w::int" "z1" "z2", standard]
 
+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"
+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_induct:
+  fixes x :: 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)
 
 subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}