--- a/Attic/Quot/Examples/IntEx2.thy	Sat May 12 21:05:59 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,111 +0,0 @@
-theory IntEx2
-imports "Quotient_Int"
-begin
-
-subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}
-
-(*
-context ring_1
-begin
-
- 
-definition 
-  of_int :: "int \<Rightarrow> 'a" 
-where
-  "of_int 
-*)
-
-
-subsection {* Binary representation *}
-
-text {*
-  This formalization defines binary arithmetic in terms of the integers
-  rather than using a datatype. This avoids multiple representations (leading
-  zeroes, etc.)  See @{text "ZF/Tools/twos-compl.ML"}, function @{text
-  int_of_binary}, for the numerical interpretation.
-
-  The representation expects that @{text "(m mod 2)"} is 0 or 1,
-  even if m is negative;
-  For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
-  @{text "-5 = (-3)*2 + 1"}.
-  
-  This two's complement binary representation derives from the paper 
-  "An Efficient Representation of Arithmetic for Term Rewriting" by
-  Dave Cohen and Phil Watson, Rewriting Techniques and Applications,
-  Springer LNCS 488 (240-251), 1991.
-*}
-
-subsubsection {* The constructors @{term Bit0}, @{term Bit1}, @{term Pls} and @{term Min} *}
-
-definition
-  Pls :: int where
-  [code del]: "Pls = 0"
-
-definition
-  Min :: int where
-  [code del]: "Min = - 1"
-
-definition
-  Bit0 :: "int \<Rightarrow> int" where
-  [code del]: "Bit0 k = k + k"
-
-definition
-  Bit1 :: "int \<Rightarrow> int" where
-  [code del]: "Bit1 k = 1 + k + k"
-
-class number = -- {* for numeric types: nat, int, real, \dots *}
-  fixes number_of :: "int \<Rightarrow> 'a"
-
-(*use "~~/src/HOL/Tools/numeral.ML"
-
-syntax
-  "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
-
-use "~~/src/HOL/Tools/numeral_syntax.ML"
-
-setup NumeralSyntax.setup
-
-abbreviation
-  "Numeral0 \<equiv> number_of Pls"
-
-abbreviation
-  "Numeral1 \<equiv> number_of (Bit1 Pls)"
-
-lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"
-  -- {* Unfold all @{text let}s involving constants *}
-  unfolding Let_def ..
-
-definition
-  succ :: "int \<Rightarrow> int" where
-  [code del]: "succ k = k + 1"
-
-definition
-  pred :: "int \<Rightarrow> int" where
-  [code del]: "pred k = k - 1"
-
-lemmas
-  max_number_of [simp] = max_def
-    [of "number_of u" "number_of v", standard, simp]
-and
-  min_number_of [simp] = min_def 
-    [of "number_of u" "number_of v", standard, simp]
-  -- {* unfolding @{text minx} and @{text max} on numerals *}
-
-lemmas numeral_simps = 
-  succ_def pred_def Pls_def Min_def Bit0_def Bit1_def
-
-text {* Removal of leading zeroes *}
-
-lemma Bit0_Pls [simp, code_post]:
-  "Bit0 Pls = Pls"
-  unfolding numeral_simps by simp
-
-lemma Bit1_Min [simp, code_post]:
-  "Bit1 Min = Min"
-  unfolding numeral_simps by simp
-
-lemmas normalize_bin_simps =
-  Bit0_Pls Bit1_Min
-*)
-
-end