# HG changeset patch
# User huffman
# Date 1321442990 -3600
# Node ID 726b743855ea7506bf9b2ad0fca05b005487fc15
# Parent  dc452a1a46e55e133e6f7389ddd8420d80c5005f
simplify proof of word_of_int; remove several now-unused lemmas about Rep_Integ

diff -r dc452a1a46e5 -r 726b743855ea src/HOL/Word/Misc_Numeric.thy
--- a/src/HOL/Word/Misc_Numeric.thy	Tue Nov 15 12:51:14 2011 +0100
+++ b/src/HOL/Word/Misc_Numeric.thy	Wed Nov 16 12:29:50 2011 +0100
@@ -247,58 +247,6 @@
   apply (simp add: zmde ring_distribs)
   done
 
-(** Rep_Integ **)
-lemma eqne: "equiv A r ==> X : A // r ==> X ~= {}"
-  unfolding equiv_def refl_on_def quotient_def Image_def by auto
-
-lemmas Rep_Integ_ne = Integ.Rep_Integ 
-  [THEN equiv_intrel [THEN eqne, simplified Integ_def [symmetric]], standard]
-
-lemmas riq = Integ.Rep_Integ [simplified Integ_def]
-lemmas intrel_refl = refl [THEN equiv_intrel_iff [THEN iffD1], standard]
-lemmas Rep_Integ_equiv = quotient_eq_iff
-  [OF equiv_intrel riq riq, simplified Integ.Rep_Integ_inject, standard]
-lemmas Rep_Integ_same = 
-  Rep_Integ_equiv [THEN intrel_refl [THEN rev_iffD2], standard]
-
-lemma RI_int: "(a, 0) : Rep_Integ (int a)"
-  unfolding int_def by auto
-
-lemmas RI_intrel [simp] = UNIV_I [THEN quotientI,
-  THEN Integ.Abs_Integ_inverse [simplified Integ_def], standard]
-
-lemma RI_minus: "(a, b) : Rep_Integ x ==> (b, a) : Rep_Integ (- x)"
-  apply (rule_tac z=x in eq_Abs_Integ)
-  apply (clarsimp simp: minus)
-  done
-
-lemma RI_add: 
-  "(a, b) : Rep_Integ x ==> (c, d) : Rep_Integ y ==> 
-   (a + c, b + d) : Rep_Integ (x + y)"
-  apply (rule_tac z=x in eq_Abs_Integ)
-  apply (rule_tac z=y in eq_Abs_Integ) 
-  apply (clarsimp simp: add)
-  done
-
-lemma mem_same: "a : S ==> a = b ==> b : S"
-  by fast
-
-(* two alternative proofs of this *)
-lemma RI_eq_diff': "(a, b) : Rep_Integ (int a - int b)"
-  apply (unfold diff_minus)
-  apply (rule mem_same)
-   apply (rule RI_minus RI_add RI_int)+
-  apply simp
-  done
-
-lemma RI_eq_diff: "((a, b) : Rep_Integ x) = (int a - int b = x)"
-  apply safe
-   apply (rule Rep_Integ_same)
-    prefer 2
-    apply (erule asm_rl)
-   apply (rule RI_eq_diff')+
-  done
-
 lemma mod_power_lem:
   "a > 1 ==> a ^ n mod a ^ m = (if m <= n then 0 else (a :: int) ^ n)"
   apply clarsimp
diff -r dc452a1a46e5 -r 726b743855ea src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Tue Nov 15 12:51:14 2011 +0100
+++ b/src/HOL/Word/Word.thy	Wed Nov 16 12:29:50 2011 +0100
@@ -1769,16 +1769,8 @@
 
 lemma word_of_int: "of_int = word_of_int"
   apply (rule ext)
-  apply (unfold of_int_def)
-  apply (rule the_elemI)
-  apply safe
-  apply (simp_all add: word_of_nat word_of_int_homs)
-   defer
-   apply (rule Rep_Integ_ne [THEN nonemptyE])
-   apply (rule bexI)
-    prefer 2
-    apply assumption
-   apply (auto simp add: RI_eq_diff)
+  apply (case_tac x rule: int_diff_cases)
+  apply (simp add: word_of_nat word_of_int_sub_hom)
   done
 
 lemma word_of_int_nat: