src/ZF/ArithSimp.thy

 header{*Arithmetic with simplification*}
 
 theory ArithSimp = Arith
 files "arith_data.ML":
 
-(*** Difference ***)
+subsection{*Difference*}
 
 lemma diff_self_eq_0: "m #- m = 0"
 apply (subgoal_tac "natify (m) #- natify (m) = 0")
 apply (rule_tac [2] natify_in_nat [THEN nat_induct], auto)
 done

 lemma diff_mult_distrib2: "k #* (m #- n) = (k #* m) #- (k #* n)"
 apply (simp (no_asm) add: mult_commute [of k] diff_mult_distrib)
 done
 
 
-(*** Remainder ***)
+subsection{*Remainder*}
 
 (*We need m:nat even with natify*)
 lemma div_termination: "[| 0<n;  n le m;  m:nat |] ==> m #- n < m"
 apply (frule lt_nat_in_nat, erule nat_succI)
 apply (erule rev_mp)

  apply (simp add: DIVISION_BY_ZERO_MOD)
 apply (simp add: mod_def raw_mod_geq nat_into_Ord [THEN Ord_0_lt_iff])
 done
 
 
-(*** Division ***)
+subsection{*Division*}
 
 lemma raw_div_type: "[| m:nat;  n:nat |] ==> raw_div (m, n) : nat"
 apply (unfold raw_div_def)
 apply (rule Ord_transrec_type)
 apply (auto simp add: nat_into_Ord [THEN Ord_0_lt_iff])

 lemma mod_div_equality: "m: nat ==> (m div n)#*n #+ m mod n = m"
 apply (simp (no_asm_simp) add: mod_div_equality_natify)
 done
 
 
-(*** Further facts about mod (mainly for mutilated chess board) ***)
+subsection{*Further Facts about Remainder*}
+
+text{*(mainly for mutilated chess board)*}
 
 lemma mod_succ_lemma:
      "[| 0<n;  m:nat;  n:nat |]  
       ==> succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))"
 apply (erule complete_induct)

 
 lemma mod2_add_self [simp]: "(m#+m) mod 2 = 0"
 by (cut_tac n = "0" in mod2_add_more, auto)
 
 
-(**** Additional theorems about "le" ****)
+subsection{*Additional theorems about @{text "\<le>"}*}
 
 lemma add_le_self: "m:nat ==> m le (m #+ n)"
 apply (simp (no_asm_simp))
 done
 

 apply (cut_tac m = "natify (m) " and n = "natify (n) " in mult_is_zero)
 apply auto
 done
 
 
-(** Cancellation laws for common factors in comparisons **)
+subsection{*Cancellation Laws for Common Factors in Comparisons*}
 
 lemma mult_less_cancel_lemma:
      "[| k: nat; m: nat; n: nat |] ==> (m#*k < n#*k) <-> (0<k & m<n)"
 apply (safe intro!: mult_lt_mono1)
 apply (erule natE, auto)

        in div_cancel_raw)
 apply auto
 done
 
 
-(** Distributive law for remainder (mod) **)
+subsection{*More Lemmas about Remainder*}
 
 lemma mult_mod_distrib_raw:
      "[| k:nat; m:nat; n:nat |] ==> (k#*m) mod (k#*n) = k #* (m mod n)"
 apply (case_tac "k=0")
  apply (simp add: DIVISION_BY_ZERO_MOD)

 
 lemma less_iff_succ_add:
      "[| m: nat; n: nat |] ==> (m<n) <-> (EX k: nat. n = succ(m#+k))"
 by (auto intro: less_imp_succ_add)
 
-(* on nat *)
+
+subsubsection{*More Lemmas About Difference*}
 
 lemma diff_is_0_lemma:
      "[| m: nat; n: nat |] ==> m #- n = 0 <-> m le n"
 apply (rule_tac m = "m" and n = "n" in diff_induct, simp_all)
 done