src/ZF/Int_ZF.thy

 (*  Title:      ZF/Int_ZF.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 *)
 
-section{*The Integers as Equivalence Classes Over Pairs of Natural Numbers*}
+section\<open>The Integers as Equivalence Classes Over Pairs of Natural Numbers\<close>
 
 theory Int_ZF imports EquivClass ArithSimp begin
 
 definition
   intrel :: i  where

 definition
   int :: i  where
     "int == (nat*nat)//intrel"
 
 definition
-  int_of :: "i=>i" --{*coercion from nat to int*}    ("$# _" [80] 80)  where
+  int_of :: "i=>i" --\<open>coercion from nat to int\<close>    ("$# _" [80] 80)  where
     "$# m == intrel `` {<natify(m), 0>}"
 
 definition
-  intify :: "i=>i" --{*coercion from ANYTHING to int*}  where
+  intify :: "i=>i" --\<open>coercion from ANYTHING to int\<close>  where
     "intify(m) == if m \<in> int then m else $#0"
 
 definition
   raw_zminus :: "i=>i"  where
     "raw_zminus(z) == \<Union><x,y>\<in>z. intrel``{<y,x>}"

   nat_of  :: "i=>i"  where
   "nat_of(z) == raw_nat_of (intify(z))"
 
 definition
   zmagnitude  ::      "i=>i"  where
-  --{*could be replaced by an absolute value function from int to int?*}
+  --\<open>could be replaced by an absolute value function from int to int?\<close>
     "zmagnitude(z) ==
      THE m. m\<in>nat & ((~ znegative(z) & z = $# m) |
                        (znegative(z) & $- z = $# m))"
 
 definition

      "z1 $<= z2 == z1 $< z2 | intify(z1)=intify(z2)"
 
 
 notation (xsymbols)
   zmult  (infixl "$\<times>" 70) and
-  zle  (infixl "$\<le>" 50)  --{*less than or equals*}
+  zle  (infixl "$\<le>" 50)  --\<open>less than or equals\<close>
 
 notation (HTML output)
   zmult  (infixl "$\<times>" 70) and
   zle  (infixl "$\<le>" 50)
 
 
 declare quotientE [elim!]
 
-subsection{*Proving that @{term intrel} is an equivalence relation*}
+subsection\<open>Proving that @{term intrel} is an equivalence relation\<close>
 
 (** Natural deduction for intrel **)
 
 lemma intrel_iff [simp]:
     "<<x1,y1>,<x2,y2>>: intrel \<longleftrightarrow>

 
 lemma intify_ident [simp]: "n \<in> int ==> intify(n) = n"
 by (simp add: intify_def)
 
 
-subsection{*Collapsing rules: to remove @{term intify}
-            from arithmetic expressions*}
+subsection\<open>Collapsing rules: to remove @{term intify}
+            from arithmetic expressions\<close>
 
 lemma intify_idem [simp]: "intify(intify(x)) = intify(x)"
 by simp
 
 lemma int_of_natify [simp]: "$# (natify(m)) = $# m"

 
 lemma zle_intify2 [simp]:"x $<= intify(y) \<longleftrightarrow> x $<= y"
 by (simp add: zle_def)
 
 
-subsection{*@{term zminus}: unary negation on @{term int}*}
+subsection\<open>@{term zminus}: unary negation on @{term int}\<close>
 
 lemma zminus_congruent: "(%<x,y>. intrel``{<y,x>}) respects intrel"
 by (auto simp add: congruent_def add_ac)
 
 lemma raw_zminus_type: "z \<in> int ==> raw_zminus(z) \<in> int"

 
 lemma zminus_zminus: "z \<in> int ==> $- ($- z) = z"
 by simp
 
 
-subsection{*@{term znegative}: the test for negative integers*}
+subsection\<open>@{term znegative}: the test for negative integers\<close>
 
 lemma znegative: "[| x\<in>nat; y\<in>nat |] ==> znegative(intrel``{<x,y>}) \<longleftrightarrow> x<y"
 apply (cases "x<y")
 apply (auto simp add: znegative_def not_lt_iff_le)
 apply (subgoal_tac "y #+ x2 < x #+ y2", force)

 
 lemma not_znegative_imp_zero: "~ znegative($- $# n) ==> natify(n)=0"
 by (simp add: znegative int_of_def zminus Ord_0_lt_iff [THEN iff_sym])
 
 
-subsection{*@{term nat_of}: Coercion of an Integer to a Natural Number*}
+subsection\<open>@{term nat_of}: Coercion of an Integer to a Natural Number\<close>
 
 lemma nat_of_intify [simp]: "nat_of(intify(z)) = nat_of(z)"
 by (simp add: nat_of_def)
 
 lemma nat_of_congruent: "(\<lambda>x. (\<lambda>\<langle>x,y\<rangle>. x #- y)(x)) respects intrel"

 by (simp add: raw_nat_of_def)
 
 lemma nat_of_type [iff,TC]: "nat_of(z) \<in> nat"
 by (simp add: nat_of_def raw_nat_of_type)
 
-subsection{*zmagnitude: magnitide of an integer, as a natural number*}
+subsection\<open>zmagnitude: magnitide of an integer, as a natural number\<close>
 
 lemma zmagnitude_int_of [simp]: "zmagnitude($# n) = natify(n)"
 by (auto simp add: zmagnitude_def int_of_eq)
 
 lemma natify_int_of_eq: "natify(x)=n ==> $#x = $# n"

 apply (auto simp add: znegative nat_of_def raw_nat_of
             split add: nat_diff_split)
 done
 
 
-subsection{*@{term zadd}: addition on int*}
-
-text{*Congruence Property for Addition*}
+subsection\<open>@{term zadd}: addition on int\<close>
+
+text\<open>Congruence Property for Addition\<close>
 lemma zadd_congruent2:
     "(%z1 z2. let <x1,y1>=z1; <x2,y2>=z2
                             in intrel``{<x1#+x2, y1#+y2>})
      respects2 intrel"
 apply (simp add: congruent2_def)

 
 lemma zadd_int0_right: "z \<in> int ==> z $+ $#0 = z"
 by simp
 
 
-subsection{*@{term zmult}: Integer Multiplication*}
-
-text{*Congruence property for multiplication*}
+subsection\<open>@{term zmult}: Integer Multiplication\<close>
+
+text\<open>Congruence property for multiplication\<close>
 lemma zmult_congruent2:
     "(%p1 p2. split(%x1 y1. split(%x2 y2.
                     intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))
      respects2 intrel"
 apply (rule equiv_intrel [THEN congruent2_commuteI], auto)

 
 lemma zdiff_zadd_eq: "(x $- y) $+ z = (x $+ z) $- y"
 by (simp add: zdiff_def zadd_ac)
 
 
-subsection{*The "Less Than" Relation*}
+subsection\<open>The "Less Than" Relation\<close>
 
 (*"Less than" is a linear ordering*)
 lemma zless_linear_lemma:
      "[| z \<in> int; w \<in> int |] ==> z$<w | z=w | w$<z"
 apply (simp add: int_def zless_def znegative_def zdiff_def, auto)

 apply (simp add: zle_def)
 apply (cut_tac zless_linear, blast)
 done
 
 
-subsection{*Less Than or Equals*}
+subsection\<open>Less Than or Equals\<close>
 
 lemma zle_refl: "z $<= z"
 by (simp add: zle_def)
 
 lemma zle_eq_refl: "x=y ==> x $<= y"

 
 lemma not_zle_iff_zless: "~ (z $<= w) \<longleftrightarrow> (w $< z)"
 by (simp add: not_zless_iff_zle [THEN iff_sym])
 
 
-subsection{*More subtraction laws (for @{text zcompare_rls})*}
+subsection\<open>More subtraction laws (for @{text zcompare_rls})\<close>
 
 lemma zdiff_zdiff_eq: "(x $- y) $- z = x $- (y $+ z)"
 by (simp add: zdiff_def zadd_ac)
 
 lemma zdiff_zdiff_eq2: "x $- (y $- z) = (x $+ z) $- y"

 done
 
 lemma zle_zdiff_iff: "(x $<= z$-y) \<longleftrightarrow> (x $+ y $<= z)"
 by (cut_tac zle_zdiff_iff_lemma [ OF intify_in_int intify_in_int], simp)
 
-text{*This list of rewrites simplifies (in)equalities by bringing subtractions
+text\<open>This list of rewrites simplifies (in)equalities by bringing subtractions
   to the top and then moving negative terms to the other side.
-  Use with @{text zadd_ac}*}
+  Use with @{text zadd_ac}\<close>
 lemmas zcompare_rls =
      zdiff_def [symmetric]
      zadd_zdiff_eq zdiff_zadd_eq zdiff_zdiff_eq zdiff_zdiff_eq2
      zdiff_zless_iff zless_zdiff_iff zdiff_zle_iff zle_zdiff_iff
      zdiff_eq_iff eq_zdiff_iff
 
 
-subsection{*Monotonicity and Cancellation Results for Instantiation
-     of the CancelNumerals Simprocs*}
+subsection\<open>Monotonicity and Cancellation Results for Instantiation
+     of the CancelNumerals Simprocs\<close>
 
 lemma zadd_left_cancel:
      "[| w \<in> int; w': int |] ==> (z $+ w' = z $+ w) \<longleftrightarrow> (w' = w)"
 apply safe
 apply (drule_tac t = "%x. x $+ ($-z) " in subst_context)

 
 lemma zadd_zless_mono: "[| w' $< w; z' $<= z |] ==> w' $+ z' $< w $+ z"
 by (erule zadd_zless_mono1 [THEN zless_zle_trans], simp)
 
 
-subsection{*Comparison laws*}
+subsection\<open>Comparison laws\<close>
 
 lemma zminus_zless_zminus [simp]: "($- x $< $- y) \<longleftrightarrow> (y $< x)"
 by (simp add: zless_def zdiff_def zadd_ac)
 
 lemma zminus_zle_zminus [simp]: "($- x $<= $- y) \<longleftrightarrow> (y $<= x)"
 by (simp add: not_zless_iff_zle [THEN iff_sym])
 
-subsubsection{*More inequality lemmas*}
+subsubsection\<open>More inequality lemmas\<close>
 
 lemma equation_zminus: "[| x \<in> int;  y \<in> int |] ==> (x = $- y) \<longleftrightarrow> (y = $- x)"
 by auto
 
 lemma zminus_equation: "[| x \<in> int;  y \<in> int |] ==> ($- x = y) \<longleftrightarrow> ($- y = x)"

 apply (cut_tac x = "intify (x) " and y = "intify (y) " in zminus_equation)
 apply auto
 done
 
 
-subsubsection{*The next several equations are permutative: watch out!*}
+subsubsection\<open>The next several equations are permutative: watch out!\<close>
 
 lemma zless_zminus: "(x $< $- y) \<longleftrightarrow> (y $< $- x)"
 by (simp add: zless_def zdiff_def zadd_ac)
 
 lemma zminus_zless: "($- x $< y) \<longleftrightarrow> ($- y $< x)"