src/ZF/IntDiv_ZF.thy

                        else
                           if 0<b then negDivAlg (a,b)
                           else        negateSnd (posDivAlg (~a,~b));
 *)
 
-section{*The Division Operators Div and Mod*}
+section\<open>The Division Operators Div and Mod\<close>
 
 theory IntDiv_ZF
 imports Bin OrderArith
 begin
 

 lemma zmult_cancel1 [simp]:
      "(k$*m = k$*n) \<longleftrightarrow> (intify(k) = #0 | intify(m) = intify(n))"
 by (simp add: zmult_commute [of k] zmult_cancel2)
 
 
-subsection{* Uniqueness and monotonicity of quotients and remainders *}
+subsection\<open>Uniqueness and monotonicity of quotients and remainders\<close>
 
 lemma unique_quotient_lemma:
      "[| b$*q' $+ r' $<= b$*q $+ r;  #0 $<= r';  #0 $< b;  r $< b |]
       ==> q' $<= q"
 apply (subgoal_tac "r' $+ b $* (q'$-q) $<= r")

  prefer 2 apply (blast intro: unique_quotient)
 apply (simp add: quorem_def)
 done
 
 
-subsection{*Correctness of posDivAlg,
-           the Division Algorithm for @{text "a\<ge>0"} and @{text "b>0"} *}
+subsection\<open>Correctness of posDivAlg,
+           the Division Algorithm for @{text "a\<ge>0"} and @{text "b>0"}\<close>
 
 lemma adjust_eq [simp]:
      "adjust(b, <q,r>) = (let diff = r$-b in
                           if #0 $<= diff then <#2$*q $+ #1,diff>
                                          else <#2$*q,r>)"

     then this rewrite can work for all constants!!*)
 lemma intify_eq_0_iff_zle: "intify(m) = #0 \<longleftrightarrow> (m $<= #0 & #0 $<= m)"
   by (simp add: int_eq_iff_zle)
 
 
-subsection{* Some convenient biconditionals for products of signs *}
+subsection\<open>Some convenient biconditionals for products of signs\<close>
 
 lemma zmult_pos: "[| #0 $< i; #0 $< j |] ==> #0 $< i $* j"
   by (drule zmult_zless_mono1, auto)
 
 lemma zmult_neg: "[| i $< #0; j $< #0 |] ==> #0 $< i $* j"

      "[| a \<in> int; b \<in> int |]
       ==> #0 $<= a \<longrightarrow> #0 $< b \<longrightarrow> quorem (<a,b>, posDivAlg(<a,b>))"
 apply (rule_tac u = "a" and v = "b" in posDivAlg_induct)
 apply auto
    apply (simp_all add: quorem_def)
-   txt{*base case: a<b*}
+   txt\<open>base case: a<b\<close>
    apply (simp add: posDivAlg_eqn)
   apply (simp add: not_zless_iff_zle [THEN iff_sym])
  apply (simp add: int_0_less_mult_iff)
-txt{*main argument*}
+txt\<open>main argument\<close>
 apply (subst posDivAlg_eqn)
 apply (simp_all (no_asm_simp))
 apply (erule splitE)
 apply (rule posDivAlg_type)
 apply (simp_all add: int_0_less_mult_iff)
 apply (auto simp add: zadd_zmult_distrib2 Let_def)
-txt{*now just linear arithmetic*}
+txt\<open>now just linear arithmetic\<close>
 apply (simp add: not_zle_iff_zless zdiff_zless_iff)
 done
 
 
-subsection{*Correctness of negDivAlg, the division algorithm for a<0 and b>0*}
+subsection\<open>Correctness of negDivAlg, the division algorithm for a<0 and b>0\<close>
 
 lemma negDivAlg_termination:
      "[| #0 $< b; a $+ b $< #0 |]
       ==> nat_of($- a $- #2 $* b) < nat_of($- a $- b)"
 apply (simp (no_asm) add: zless_nat_conj)

      "[| a \<in> int; b \<in> int |]
       ==> a $< #0 \<longrightarrow> #0 $< b \<longrightarrow> quorem (<a,b>, negDivAlg(<a,b>))"
 apply (rule_tac u = "a" and v = "b" in negDivAlg_induct)
   apply auto
    apply (simp_all add: quorem_def)
-   txt{*base case: @{term "0$<=a$+b"}*}
+   txt\<open>base case: @{term "0$<=a$+b"}\<close>
    apply (simp add: negDivAlg_eqn)
   apply (simp add: not_zless_iff_zle [THEN iff_sym])
  apply (simp add: int_0_less_mult_iff)
-txt{*main argument*}
+txt\<open>main argument\<close>
 apply (subst negDivAlg_eqn)
 apply (simp_all (no_asm_simp))
 apply (erule splitE)
 apply (rule negDivAlg_type)
 apply (simp_all add: int_0_less_mult_iff)
 apply (auto simp add: zadd_zmult_distrib2 Let_def)
-txt{*now just linear arithmetic*}
+txt\<open>now just linear arithmetic\<close>
 apply (simp add: not_zle_iff_zless zdiff_zless_iff)
 done
 
 
-subsection{* Existence shown by proving the division algorithm to be correct *}
+subsection\<open>Existence shown by proving the division algorithm to be correct\<close>
 
 (*the case a=0*)
 lemma quorem_0: "[|b \<noteq> #0;  b \<in> int|] ==> quorem (<#0,b>, <#0,#0>)"
 by (force simp add: quorem_def neq_iff_zless)
 

 lemma quorem_neg:
      "[|quorem (<$-a,$-b>, qr);  a \<in> int;  b \<in> int;  qr \<in> int * int|]
       ==> quorem (<a,b>, negateSnd(qr))"
 apply clarify
 apply (auto elim: zless_asym simp add: quorem_def zless_zminus)
-txt{*linear arithmetic from here on*}
+txt\<open>linear arithmetic from here on\<close>
 apply (simp_all add: zminus_equation [of a] zminus_zless)
 apply (cut_tac [2] z = "b" and w = "#0" in zless_linear)
 apply (cut_tac [1] z = "b" and w = "#0" in zless_linear)
 apply auto
 apply (blast dest: zle_zless_trans)+

      "[|b \<noteq> #0;  a \<in> int;  b \<in> int|] ==> quorem (<a,b>, divAlg(<a,b>))"
 apply (auto simp add: quorem_0 divAlg_def)
 apply (safe intro!: quorem_neg posDivAlg_correct negDivAlg_correct
                     posDivAlg_type negDivAlg_type)
 apply (auto simp add: quorem_def neq_iff_zless)
-txt{*linear arithmetic from here on*}
+txt\<open>linear arithmetic from here on\<close>
 apply (auto simp add: zle_def)
 done
 
 lemma divAlg_type: "[|a \<in> int;  b \<in> int|] ==> divAlg(<a,b>) \<in> int * int"
 apply (auto simp add: divAlg_def)

 apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_zminus_zminus_raw)
 apply auto
 done
 
 
-subsection{* division of a number by itself *}
+subsection\<open>division of a number by itself\<close>
 
 lemma self_quotient_aux1: "[| #0 $< a; a = r $+ a$*q; r $< a |] ==> #1 $<= q"
 apply (subgoal_tac "#0 $< a$*q")
 apply (cut_tac w = "#0" and z = "q" in add1_zle_iff)
 apply (simp add: int_0_less_mult_iff)

 apply (cut_tac a = "intify (a)" in zmod_self_raw)
 apply auto
 done
 
 
-subsection{* Computation of division and remainder *}
+subsection\<open>Computation of division and remainder\<close>
 
 lemma zdiv_zero [simp]: "#0 zdiv b = #0"
   by (simp add: zdiv_def divAlg_def)
 
 lemma zdiv_eq_minus1: "#0 $< b ==> #-1 zdiv b = #-1"

 apply auto
 done
 declare zdiv_minus1_right [simp]
 
 
-subsection{* Monotonicity in the first argument (divisor) *}
+subsection\<open>Monotonicity in the first argument (divisor)\<close>
 
 lemma zdiv_mono1: "[| a $<= a';  #0 $< b |] ==> a zdiv b $<= a' zdiv b"
 apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
 apply (cut_tac a = "a'" and b = "b" in zmod_zdiv_equality)
 apply (rule unique_quotient_lemma)

 apply (erule subst)
 apply (simp_all (no_asm_simp) add: neg_mod_sign neg_mod_bound)
 done
 
 
-subsection{* Monotonicity in the second argument (dividend) *}
+subsection\<open>Monotonicity in the second argument (dividend)\<close>
 
 lemma q_pos_lemma:
      "[| #0 $<= b'$*q' $+ r'; r' $< b';  #0 $< b' |] ==> #0 $<= q'"
 apply (subgoal_tac "#0 $< b'$* (q' $+ #1)")
  apply (simp add: int_0_less_mult_iff)

 apply auto
 done
 
 
 
-subsection{* More algebraic laws for zdiv and zmod *}
+subsection\<open>More algebraic laws for zdiv and zmod\<close>
 
 (** proving (a*b) zdiv c = a $* (b zdiv c) $+ a * (b zmod c) **)
 
 lemma zmult1_lemma:
      "[| quorem(<b,c>, <q,r>);  c \<in> int;  c \<noteq> #0 |]

  apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
 apply (simp (no_asm_simp) add: zmod_zadd1_eq)
 done
 
 
-subsection{* proving  a zdiv (b*c) = (a zdiv b) zdiv c *}
+subsection\<open>proving  a zdiv (b*c) = (a zdiv b) zdiv c\<close>
 
 (*The condition c>0 seems necessary.  Consider that 7 zdiv ~6 = ~2 but
   7 zdiv 2 zdiv ~3 = 3 zdiv ~3 = ~1.  The subcase (a zdiv b) zmod c = 0 seems
   to cause particular problems.*)
 

      "#0 $< c ==> a zmod (b$*c) = b$*(a zdiv b zmod c) $+ a zmod b"
 apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_zmult2_eq_raw)
 apply auto
 done
 
-subsection{* Cancellation of common factors in "zdiv" *}
+subsection\<open>Cancellation of common factors in "zdiv"\<close>
 
 lemma zdiv_zmult_zmult1_aux1:
      "[| #0 $< b;  intify(c) \<noteq> #0 |] ==> (c$*a) zdiv (c$*b) = a zdiv b"
 apply (subst zdiv_zmult2_eq)
 apply auto

 apply (drule zdiv_zmult_zmult1)
 apply (auto simp add: zmult_commute)
 done
 
 
-subsection{* Distribution of factors over "zmod" *}
+subsection\<open>Distribution of factors over "zmod"\<close>
 
 lemma zmod_zmult_zmult1_aux1:
      "[| #0 $< b;  intify(c) \<noteq> #0 |]
       ==> (c$*a) zmod (c$*b) = c $* (a zmod b)"
 apply (subst zmod_zmult2_eq)