9548

1 
(* Title: ZF/ArithSimp.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 2000 University of Cambridge


5 


6 
*)


7 

13328

8 
header{*Arithmetic with simplification*}


9 

9548

10 
theory ArithSimp = Arith


11 
files "arith_data.ML":

13259

12 


13 
(*** Difference ***)


14 


15 
lemma diff_self_eq_0: "m # m = 0"


16 
apply (subgoal_tac "natify (m) # natify (m) = 0")


17 
apply (rule_tac [2] natify_in_nat [THEN nat_induct], auto)


18 
done


19 


20 
(**Addition is the inverse of subtraction**)


21 


22 
(*We need m:nat even if we replace the RHS by natify(m), for consider e.g.


23 
n=2, m=omega; then n + (mn) = 2 + (02) = 2 ~= 0 = natify(m).*)


24 
lemma add_diff_inverse: "[ n le m; m:nat ] ==> n #+ (m#n) = m"


25 
apply (frule lt_nat_in_nat, erule nat_succI)


26 
apply (erule rev_mp)


27 
apply (rule_tac m = "m" and n = "n" in diff_induct, auto)


28 
done


29 


30 
lemma add_diff_inverse2: "[ n le m; m:nat ] ==> (m#n) #+ n = m"


31 
apply (frule lt_nat_in_nat, erule nat_succI)


32 
apply (simp (no_asm_simp) add: add_commute add_diff_inverse)


33 
done


34 


35 
(*Proof is IDENTICAL to that of add_diff_inverse*)


36 
lemma diff_succ: "[ n le m; m:nat ] ==> succ(m) # n = succ(m#n)"


37 
apply (frule lt_nat_in_nat, erule nat_succI)


38 
apply (erule rev_mp)


39 
apply (rule_tac m = "m" and n = "n" in diff_induct)


40 
apply (simp_all (no_asm_simp))


41 
done


42 


43 
lemma zero_less_diff [simp]:


44 
"[ m: nat; n: nat ] ==> 0 < (n # m) <> m<n"


45 
apply (rule_tac m = "m" and n = "n" in diff_induct)


46 
apply (simp_all (no_asm_simp))


47 
done


48 


49 


50 
(** Difference distributes over multiplication **)


51 


52 
lemma diff_mult_distrib: "(m # n) #* k = (m #* k) # (n #* k)"


53 
apply (subgoal_tac " (natify (m) # natify (n)) #* natify (k) = (natify (m) #* natify (k)) # (natify (n) #* natify (k))")


54 
apply (rule_tac [2] m = "natify (m) " and n = "natify (n) " in diff_induct)


55 
apply (simp_all add: diff_cancel)


56 
done


57 


58 
lemma diff_mult_distrib2: "k #* (m # n) = (k #* m) # (k #* n)"


59 
apply (simp (no_asm) add: mult_commute [of k] diff_mult_distrib)


60 
done


61 


62 


63 
(*** Remainder ***)


64 


65 
(*We need m:nat even with natify*)


66 
lemma div_termination: "[ 0<n; n le m; m:nat ] ==> m # n < m"


67 
apply (frule lt_nat_in_nat, erule nat_succI)


68 
apply (erule rev_mp)


69 
apply (erule rev_mp)


70 
apply (rule_tac m = "m" and n = "n" in diff_induct)


71 
apply (simp_all (no_asm_simp) add: diff_le_self)


72 
done


73 


74 
(*for mod and div*)


75 
lemmas div_rls =


76 
nat_typechecks Ord_transrec_type apply_funtype


77 
div_termination [THEN ltD]


78 
nat_into_Ord not_lt_iff_le [THEN iffD1]


79 


80 
lemma raw_mod_type: "[ m:nat; n:nat ] ==> raw_mod (m, n) : nat"


81 
apply (unfold raw_mod_def)


82 
apply (rule Ord_transrec_type)


83 
apply (auto simp add: nat_into_Ord [THEN Ord_0_lt_iff])


84 
apply (blast intro: div_rls)


85 
done


86 


87 
lemma mod_type [TC,iff]: "m mod n : nat"


88 
apply (unfold mod_def)


89 
apply (simp (no_asm) add: mod_def raw_mod_type)


90 
done


91 


92 


93 
(** Aribtrary definitions for division by zero. Useful to simplify


94 
certain equations **)


95 


96 
lemma DIVISION_BY_ZERO_DIV: "a div 0 = 0"


97 
apply (unfold div_def)


98 
apply (rule raw_div_def [THEN def_transrec, THEN trans])


99 
apply (simp (no_asm_simp))


100 
done (*NOT for adding to default simpset*)


101 


102 
lemma DIVISION_BY_ZERO_MOD: "a mod 0 = natify(a)"


103 
apply (unfold mod_def)


104 
apply (rule raw_mod_def [THEN def_transrec, THEN trans])


105 
apply (simp (no_asm_simp))


106 
done (*NOT for adding to default simpset*)


107 


108 
lemma raw_mod_less: "m<n ==> raw_mod (m,n) = m"


109 
apply (rule raw_mod_def [THEN def_transrec, THEN trans])


110 
apply (simp (no_asm_simp) add: div_termination [THEN ltD])


111 
done


112 


113 
lemma mod_less [simp]: "[ m<n; n : nat ] ==> m mod n = m"


114 
apply (frule lt_nat_in_nat, assumption)


115 
apply (simp (no_asm_simp) add: mod_def raw_mod_less)


116 
done


117 


118 
lemma raw_mod_geq:


119 
"[ 0<n; n le m; m:nat ] ==> raw_mod (m, n) = raw_mod (m#n, n)"


120 
apply (frule lt_nat_in_nat, erule nat_succI)


121 
apply (rule raw_mod_def [THEN def_transrec, THEN trans])


122 
apply (simp add: div_termination [THEN ltD] not_lt_iff_le [THEN iffD2], blast)


123 
done


124 


125 


126 
lemma mod_geq: "[ n le m; m:nat ] ==> m mod n = (m#n) mod n"


127 
apply (frule lt_nat_in_nat, erule nat_succI)


128 
apply (case_tac "n=0")


129 
apply (simp add: DIVISION_BY_ZERO_MOD)


130 
apply (simp add: mod_def raw_mod_geq nat_into_Ord [THEN Ord_0_lt_iff])


131 
done


132 


133 


134 
(*** Division ***)


135 


136 
lemma raw_div_type: "[ m:nat; n:nat ] ==> raw_div (m, n) : nat"


137 
apply (unfold raw_div_def)


138 
apply (rule Ord_transrec_type)


139 
apply (auto simp add: nat_into_Ord [THEN Ord_0_lt_iff])


140 
apply (blast intro: div_rls)


141 
done


142 


143 
lemma div_type [TC,iff]: "m div n : nat"


144 
apply (unfold div_def)


145 
apply (simp (no_asm) add: div_def raw_div_type)


146 
done


147 


148 
lemma raw_div_less: "m<n ==> raw_div (m,n) = 0"


149 
apply (rule raw_div_def [THEN def_transrec, THEN trans])


150 
apply (simp (no_asm_simp) add: div_termination [THEN ltD])


151 
done


152 


153 
lemma div_less [simp]: "[ m<n; n : nat ] ==> m div n = 0"


154 
apply (frule lt_nat_in_nat, assumption)


155 
apply (simp (no_asm_simp) add: div_def raw_div_less)


156 
done


157 


158 
lemma raw_div_geq: "[ 0<n; n le m; m:nat ] ==> raw_div(m,n) = succ(raw_div(m#n, n))"


159 
apply (subgoal_tac "n ~= 0")


160 
prefer 2 apply blast


161 
apply (frule lt_nat_in_nat, erule nat_succI)


162 
apply (rule raw_div_def [THEN def_transrec, THEN trans])


163 
apply (simp add: div_termination [THEN ltD] not_lt_iff_le [THEN iffD2] )


164 
done


165 


166 
lemma div_geq [simp]:


167 
"[ 0<n; n le m; m:nat ] ==> m div n = succ ((m#n) div n)"


168 
apply (frule lt_nat_in_nat, erule nat_succI)


169 
apply (simp (no_asm_simp) add: div_def raw_div_geq)


170 
done


171 


172 
declare div_less [simp] div_geq [simp]


173 


174 


175 
(*A key result*)


176 
lemma mod_div_lemma: "[ m: nat; n: nat ] ==> (m div n)#*n #+ m mod n = m"


177 
apply (case_tac "n=0")


178 
apply (simp add: DIVISION_BY_ZERO_MOD)


179 
apply (simp add: nat_into_Ord [THEN Ord_0_lt_iff])


180 
apply (erule complete_induct)


181 
apply (case_tac "x<n")


182 
txt{*case x<n*}


183 
apply (simp (no_asm_simp))


184 
txt{*case n le x*}


185 
apply (simp add: not_lt_iff_le add_assoc mod_geq div_termination [THEN ltD] add_diff_inverse)


186 
done


187 


188 
lemma mod_div_equality_natify: "(m div n)#*n #+ m mod n = natify(m)"


189 
apply (subgoal_tac " (natify (m) div natify (n))#*natify (n) #+ natify (m) mod natify (n) = natify (m) ")


190 
apply force


191 
apply (subst mod_div_lemma, auto)


192 
done


193 


194 
lemma mod_div_equality: "m: nat ==> (m div n)#*n #+ m mod n = m"


195 
apply (simp (no_asm_simp) add: mod_div_equality_natify)


196 
done


197 


198 


199 
(*** Further facts about mod (mainly for mutilated chess board) ***)


200 


201 
lemma mod_succ_lemma:


202 
"[ 0<n; m:nat; n:nat ]


203 
==> succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))"


204 
apply (erule complete_induct)


205 
apply (case_tac "succ (x) <n")


206 
txt{* case succ(x) < n *}


207 
apply (simp (no_asm_simp) add: nat_le_refl [THEN lt_trans] succ_neq_self)


208 
apply (simp add: ltD [THEN mem_imp_not_eq])


209 
txt{* case n le succ(x) *}


210 
apply (simp add: mod_geq not_lt_iff_le)


211 
apply (erule leE)


212 
apply (simp (no_asm_simp) add: mod_geq div_termination [THEN ltD] diff_succ)


213 
txt{*equality case*}


214 
apply (simp add: diff_self_eq_0)


215 
done


216 


217 
lemma mod_succ:


218 
"n:nat ==> succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))"


219 
apply (case_tac "n=0")


220 
apply (simp (no_asm_simp) add: natify_succ DIVISION_BY_ZERO_MOD)


221 
apply (subgoal_tac "natify (succ (m)) mod n = (if succ (natify (m) mod n) = n then 0 else succ (natify (m) mod n))")


222 
prefer 2


223 
apply (subst natify_succ)


224 
apply (rule mod_succ_lemma)


225 
apply (auto simp del: natify_succ simp add: nat_into_Ord [THEN Ord_0_lt_iff])


226 
done


227 


228 
lemma mod_less_divisor: "[ 0<n; n:nat ] ==> m mod n < n"


229 
apply (subgoal_tac "natify (m) mod n < n")


230 
apply (rule_tac [2] i = "natify (m) " in complete_induct)


231 
apply (case_tac [3] "x<n", auto)


232 
txt{* case n le x*}


233 
apply (simp add: mod_geq not_lt_iff_le div_termination [THEN ltD])


234 
done


235 


236 
lemma mod_1_eq [simp]: "m mod 1 = 0"


237 
by (cut_tac n = "1" in mod_less_divisor, auto)


238 


239 
lemma mod2_cases: "b<2 ==> k mod 2 = b  k mod 2 = (if b=1 then 0 else 1)"


240 
apply (subgoal_tac "k mod 2: 2")


241 
prefer 2 apply (simp add: mod_less_divisor [THEN ltD])


242 
apply (drule ltD, auto)


243 
done


244 


245 
lemma mod2_succ_succ [simp]: "succ(succ(m)) mod 2 = m mod 2"


246 
apply (subgoal_tac "m mod 2: 2")


247 
prefer 2 apply (simp add: mod_less_divisor [THEN ltD])


248 
apply (auto simp add: mod_succ)


249 
done


250 


251 
lemma mod2_add_more [simp]: "(m#+m#+n) mod 2 = n mod 2"


252 
apply (subgoal_tac " (natify (m) #+natify (m) #+n) mod 2 = n mod 2")


253 
apply (rule_tac [2] n = "natify (m) " in nat_induct)


254 
apply auto


255 
done


256 


257 
lemma mod2_add_self [simp]: "(m#+m) mod 2 = 0"


258 
by (cut_tac n = "0" in mod2_add_more, auto)


259 


260 


261 
(**** Additional theorems about "le" ****)


262 


263 
lemma add_le_self: "m:nat ==> m le (m #+ n)"


264 
apply (simp (no_asm_simp))


265 
done


266 


267 
lemma add_le_self2: "m:nat ==> m le (n #+ m)"


268 
apply (simp (no_asm_simp))


269 
done


270 


271 
(*** Monotonicity of Multiplication ***)


272 


273 
lemma mult_le_mono1: "[ i le j; j:nat ] ==> (i#*k) le (j#*k)"


274 
apply (subgoal_tac "natify (i) #*natify (k) le j#*natify (k) ")


275 
apply (frule_tac [2] lt_nat_in_nat)


276 
apply (rule_tac [3] n = "natify (k) " in nat_induct)


277 
apply (simp_all add: add_le_mono)


278 
done


279 


280 
(* le monotonicity, BOTH arguments*)


281 
lemma mult_le_mono: "[ i le j; k le l; j:nat; l:nat ] ==> i#*k le j#*l"


282 
apply (rule mult_le_mono1 [THEN le_trans], assumption+)


283 
apply (subst mult_commute, subst mult_commute, rule mult_le_mono1, assumption+)


284 
done


285 


286 
(*strict, in 1st argument; proof is by induction on k>0.


287 
I can't see how to relax the typing conditions.*)


288 
lemma mult_lt_mono2: "[ i<j; 0<k; j:nat; k:nat ] ==> k#*i < k#*j"


289 
apply (erule zero_lt_natE)


290 
apply (frule_tac [2] lt_nat_in_nat)


291 
apply (simp_all (no_asm_simp))


292 
apply (induct_tac "x")


293 
apply (simp_all (no_asm_simp) add: add_lt_mono)


294 
done


295 


296 
lemma mult_lt_mono1: "[ i<j; 0<k; j:nat; k:nat ] ==> i#*k < j#*k"


297 
apply (simp (no_asm_simp) add: mult_lt_mono2 mult_commute [of _ k])


298 
done


299 


300 
lemma add_eq_0_iff [iff]: "m#+n = 0 <> natify(m)=0 & natify(n)=0"


301 
apply (subgoal_tac "natify (m) #+ natify (n) = 0 <> natify (m) =0 & natify (n) =0")


302 
apply (rule_tac [2] n = "natify (m) " in natE)


303 
apply (rule_tac [4] n = "natify (n) " in natE)


304 
apply auto


305 
done


306 


307 
lemma zero_lt_mult_iff [iff]: "0 < m#*n <> 0 < natify(m) & 0 < natify(n)"


308 
apply (subgoal_tac "0 < natify (m) #*natify (n) <> 0 < natify (m) & 0 < natify (n) ")


309 
apply (rule_tac [2] n = "natify (m) " in natE)


310 
apply (rule_tac [4] n = "natify (n) " in natE)


311 
apply (rule_tac [3] n = "natify (n) " in natE)


312 
apply auto


313 
done


314 


315 
lemma mult_eq_1_iff [iff]: "m#*n = 1 <> natify(m)=1 & natify(n)=1"


316 
apply (subgoal_tac "natify (m) #* natify (n) = 1 <> natify (m) =1 & natify (n) =1")


317 
apply (rule_tac [2] n = "natify (m) " in natE)


318 
apply (rule_tac [4] n = "natify (n) " in natE)


319 
apply auto


320 
done


321 


322 


323 
lemma mult_is_zero: "[m: nat; n: nat] ==> (m #* n = 0) <> (m = 0  n = 0)"


324 
apply auto


325 
apply (erule natE)


326 
apply (erule_tac [2] natE, auto)


327 
done


328 


329 
lemma mult_is_zero_natify [iff]:


330 
"(m #* n = 0) <> (natify(m) = 0  natify(n) = 0)"


331 
apply (cut_tac m = "natify (m) " and n = "natify (n) " in mult_is_zero)


332 
apply auto


333 
done


334 


335 


336 
(** Cancellation laws for common factors in comparisons **)


337 


338 
lemma mult_less_cancel_lemma:


339 
"[ k: nat; m: nat; n: nat ] ==> (m#*k < n#*k) <> (0<k & m<n)"


340 
apply (safe intro!: mult_lt_mono1)


341 
apply (erule natE, auto)


342 
apply (rule not_le_iff_lt [THEN iffD1])


343 
apply (drule_tac [3] not_le_iff_lt [THEN [2] rev_iffD2])


344 
prefer 5 apply (blast intro: mult_le_mono1, auto)


345 
done


346 


347 
lemma mult_less_cancel2 [simp]:


348 
"(m#*k < n#*k) <> (0 < natify(k) & natify(m) < natify(n))"


349 
apply (rule iff_trans)


350 
apply (rule_tac [2] mult_less_cancel_lemma, auto)


351 
done


352 


353 
lemma mult_less_cancel1 [simp]:


354 
"(k#*m < k#*n) <> (0 < natify(k) & natify(m) < natify(n))"


355 
apply (simp (no_asm) add: mult_less_cancel2 mult_commute [of k])


356 
done


357 


358 
lemma mult_le_cancel2 [simp]: "(m#*k le n#*k) <> (0 < natify(k) > natify(m) le natify(n))"


359 
apply (simp (no_asm_simp) add: not_lt_iff_le [THEN iff_sym])


360 
apply auto


361 
done


362 


363 
lemma mult_le_cancel1 [simp]: "(k#*m le k#*n) <> (0 < natify(k) > natify(m) le natify(n))"


364 
apply (simp (no_asm_simp) add: not_lt_iff_le [THEN iff_sym])


365 
apply auto


366 
done


367 


368 
lemma mult_le_cancel_le1: "k : nat ==> k #* m le k \<longleftrightarrow> (0 < k \<longrightarrow> natify(m) le 1)"


369 
by (cut_tac k = "k" and m = "m" and n = "1" in mult_le_cancel1, auto)


370 


371 
lemma Ord_eq_iff_le: "[ Ord(m); Ord(n) ] ==> m=n <> (m le n & n le m)"


372 
by (blast intro: le_anti_sym)


373 


374 
lemma mult_cancel2_lemma:


375 
"[ k: nat; m: nat; n: nat ] ==> (m#*k = n#*k) <> (m=n  k=0)"


376 
apply (simp (no_asm_simp) add: Ord_eq_iff_le [of "m#*k"] Ord_eq_iff_le [of m])


377 
apply (auto simp add: Ord_0_lt_iff)


378 
done


379 


380 
lemma mult_cancel2 [simp]:


381 
"(m#*k = n#*k) <> (natify(m) = natify(n)  natify(k) = 0)"


382 
apply (rule iff_trans)


383 
apply (rule_tac [2] mult_cancel2_lemma, auto)


384 
done


385 


386 
lemma mult_cancel1 [simp]:


387 
"(k#*m = k#*n) <> (natify(m) = natify(n)  natify(k) = 0)"


388 
apply (simp (no_asm) add: mult_cancel2 mult_commute [of k])


389 
done


390 


391 


392 
(** Cancellation law for division **)


393 


394 
lemma div_cancel_raw:


395 
"[ 0<n; 0<k; k:nat; m:nat; n:nat ] ==> (k#*m) div (k#*n) = m div n"


396 
apply (erule_tac i = "m" in complete_induct)


397 
apply (case_tac "x<n")


398 
apply (simp add: div_less zero_lt_mult_iff mult_lt_mono2)


399 
apply (simp add: not_lt_iff_le zero_lt_mult_iff le_refl [THEN mult_le_mono]


400 
div_geq diff_mult_distrib2 [symmetric] div_termination [THEN ltD])


401 
done


402 


403 
lemma div_cancel:


404 
"[ 0 < natify(n); 0 < natify(k) ] ==> (k#*m) div (k#*n) = m div n"


405 
apply (cut_tac k = "natify (k) " and m = "natify (m)" and n = "natify (n)"


406 
in div_cancel_raw)


407 
apply auto


408 
done


409 


410 


411 
(** Distributive law for remainder (mod) **)


412 


413 
lemma mult_mod_distrib_raw:


414 
"[ k:nat; m:nat; n:nat ] ==> (k#*m) mod (k#*n) = k #* (m mod n)"


415 
apply (case_tac "k=0")


416 
apply (simp add: DIVISION_BY_ZERO_MOD)


417 
apply (case_tac "n=0")


418 
apply (simp add: DIVISION_BY_ZERO_MOD)


419 
apply (simp add: nat_into_Ord [THEN Ord_0_lt_iff])


420 
apply (erule_tac i = "m" in complete_induct)


421 
apply (case_tac "x<n")


422 
apply (simp (no_asm_simp) add: mod_less zero_lt_mult_iff mult_lt_mono2)


423 
apply (simp add: not_lt_iff_le zero_lt_mult_iff le_refl [THEN mult_le_mono]


424 
mod_geq diff_mult_distrib2 [symmetric] div_termination [THEN ltD])


425 
done


426 


427 
lemma mod_mult_distrib2: "k #* (m mod n) = (k#*m) mod (k#*n)"


428 
apply (cut_tac k = "natify (k) " and m = "natify (m)" and n = "natify (n)"


429 
in mult_mod_distrib_raw)


430 
apply auto


431 
done


432 


433 
lemma mult_mod_distrib: "(m mod n) #* k = (m#*k) mod (n#*k)"


434 
apply (simp (no_asm) add: mult_commute mod_mult_distrib2)


435 
done


436 


437 
lemma mod_add_self2_raw: "n \<in> nat ==> (m #+ n) mod n = m mod n"


438 
apply (subgoal_tac " (n #+ m) mod n = (n #+ m # n) mod n")


439 
apply (simp add: add_commute)


440 
apply (subst mod_geq [symmetric], auto)


441 
done


442 


443 
lemma mod_add_self2 [simp]: "(m #+ n) mod n = m mod n"


444 
apply (cut_tac n = "natify (n) " in mod_add_self2_raw)


445 
apply auto


446 
done


447 


448 
lemma mod_add_self1 [simp]: "(n#+m) mod n = m mod n"


449 
apply (simp (no_asm_simp) add: add_commute mod_add_self2)


450 
done


451 


452 
lemma mod_mult_self1_raw: "k \<in> nat ==> (m #+ k#*n) mod n = m mod n"


453 
apply (erule nat_induct)


454 
apply (simp_all (no_asm_simp) add: add_left_commute [of _ n])


455 
done


456 


457 
lemma mod_mult_self1 [simp]: "(m #+ k#*n) mod n = m mod n"


458 
apply (cut_tac k = "natify (k) " in mod_mult_self1_raw)


459 
apply auto


460 
done


461 


462 
lemma mod_mult_self2 [simp]: "(m #+ n#*k) mod n = m mod n"


463 
apply (simp (no_asm) add: mult_commute mod_mult_self1)


464 
done


465 


466 
(*Lemma for gcd*)


467 
lemma mult_eq_self_implies_10: "m = m#*n ==> natify(n)=1  m=0"


468 
apply (subgoal_tac "m: nat")


469 
prefer 2


470 
apply (erule ssubst)


471 
apply simp


472 
apply (rule disjCI)


473 
apply (drule sym)


474 
apply (rule Ord_linear_lt [of "natify(n)" 1])


475 
apply simp_all


476 
apply (subgoal_tac "m #* n = 0", simp)


477 
apply (subst mult_natify2 [symmetric])


478 
apply (simp del: mult_natify2)


479 
apply (drule nat_into_Ord [THEN Ord_0_lt, THEN [2] mult_lt_mono2], auto)


480 
done


481 


482 
lemma less_imp_succ_add [rule_format]:


483 
"[ m<n; n: nat ] ==> EX k: nat. n = succ(m#+k)"


484 
apply (frule lt_nat_in_nat, assumption)


485 
apply (erule rev_mp)


486 
apply (induct_tac "n")


487 
apply (simp_all (no_asm) add: le_iff)


488 
apply (blast elim!: leE intro!: add_0_right [symmetric] add_succ_right [symmetric])


489 
done


490 


491 
lemma less_iff_succ_add:


492 
"[ m: nat; n: nat ] ==> (m<n) <> (EX k: nat. n = succ(m#+k))"


493 
by (auto intro: less_imp_succ_add)


494 


495 
(* on nat *)


496 


497 
lemma diff_is_0_lemma:


498 
"[ m: nat; n: nat ] ==> m # n = 0 <> m le n"


499 
apply (rule_tac m = "m" and n = "n" in diff_induct, simp_all)


500 
done


501 


502 
lemma diff_is_0_iff: "m # n = 0 <> natify(m) le natify(n)"


503 
by (simp add: diff_is_0_lemma [symmetric])


504 


505 
lemma nat_lt_imp_diff_eq_0:


506 
"[ a:nat; b:nat; a<b ] ==> a # b = 0"


507 
by (simp add: diff_is_0_iff le_iff)


508 


509 
lemma nat_diff_split:


510 
"[ a:nat; b:nat ] ==>


511 
(P(a # b)) <> ((a < b >P(0)) & (ALL d:nat. a = b #+ d > P(d)))"


512 
apply (case_tac "a < b")


513 
apply (force simp add: nat_lt_imp_diff_eq_0)


514 
apply (rule iffI, simp_all)


515 
apply clarify


516 
apply (rotate_tac 1)


517 
apply simp


518 
apply (drule_tac x="a#b" in bspec)


519 
apply (simp_all add: Ordinal.not_lt_iff_le add_diff_inverse)


520 
done


521 


522 
ML


523 
{*


524 
val diff_self_eq_0 = thm "diff_self_eq_0";


525 
val add_diff_inverse = thm "add_diff_inverse";


526 
val add_diff_inverse2 = thm "add_diff_inverse2";


527 
val diff_succ = thm "diff_succ";


528 
val zero_less_diff = thm "zero_less_diff";


529 
val diff_mult_distrib = thm "diff_mult_distrib";


530 
val diff_mult_distrib2 = thm "diff_mult_distrib2";


531 
val div_termination = thm "div_termination";


532 
val raw_mod_type = thm "raw_mod_type";


533 
val mod_type = thm "mod_type";


534 
val DIVISION_BY_ZERO_DIV = thm "DIVISION_BY_ZERO_DIV";


535 
val DIVISION_BY_ZERO_MOD = thm "DIVISION_BY_ZERO_MOD";


536 
val raw_mod_less = thm "raw_mod_less";


537 
val mod_less = thm "mod_less";


538 
val raw_mod_geq = thm "raw_mod_geq";


539 
val mod_geq = thm "mod_geq";


540 
val raw_div_type = thm "raw_div_type";


541 
val div_type = thm "div_type";


542 
val raw_div_less = thm "raw_div_less";


543 
val div_less = thm "div_less";


544 
val raw_div_geq = thm "raw_div_geq";


545 
val div_geq = thm "div_geq";


546 
val mod_div_equality_natify = thm "mod_div_equality_natify";


547 
val mod_div_equality = thm "mod_div_equality";


548 
val mod_succ = thm "mod_succ";


549 
val mod_less_divisor = thm "mod_less_divisor";


550 
val mod_1_eq = thm "mod_1_eq";


551 
val mod2_cases = thm "mod2_cases";


552 
val mod2_succ_succ = thm "mod2_succ_succ";


553 
val mod2_add_more = thm "mod2_add_more";


554 
val mod2_add_self = thm "mod2_add_self";


555 
val add_le_self = thm "add_le_self";


556 
val add_le_self2 = thm "add_le_self2";


557 
val mult_le_mono1 = thm "mult_le_mono1";


558 
val mult_le_mono = thm "mult_le_mono";


559 
val mult_lt_mono2 = thm "mult_lt_mono2";


560 
val mult_lt_mono1 = thm "mult_lt_mono1";


561 
val add_eq_0_iff = thm "add_eq_0_iff";


562 
val zero_lt_mult_iff = thm "zero_lt_mult_iff";


563 
val mult_eq_1_iff = thm "mult_eq_1_iff";


564 
val mult_is_zero = thm "mult_is_zero";


565 
val mult_is_zero_natify = thm "mult_is_zero_natify";


566 
val mult_less_cancel2 = thm "mult_less_cancel2";


567 
val mult_less_cancel1 = thm "mult_less_cancel1";


568 
val mult_le_cancel2 = thm "mult_le_cancel2";


569 
val mult_le_cancel1 = thm "mult_le_cancel1";


570 
val mult_le_cancel_le1 = thm "mult_le_cancel_le1";


571 
val Ord_eq_iff_le = thm "Ord_eq_iff_le";


572 
val mult_cancel2 = thm "mult_cancel2";


573 
val mult_cancel1 = thm "mult_cancel1";


574 
val div_cancel_raw = thm "div_cancel_raw";


575 
val div_cancel = thm "div_cancel";


576 
val mult_mod_distrib_raw = thm "mult_mod_distrib_raw";


577 
val mod_mult_distrib2 = thm "mod_mult_distrib2";


578 
val mult_mod_distrib = thm "mult_mod_distrib";


579 
val mod_add_self2_raw = thm "mod_add_self2_raw";


580 
val mod_add_self2 = thm "mod_add_self2";


581 
val mod_add_self1 = thm "mod_add_self1";


582 
val mod_mult_self1_raw = thm "mod_mult_self1_raw";


583 
val mod_mult_self1 = thm "mod_mult_self1";


584 
val mod_mult_self2 = thm "mod_mult_self2";


585 
val mult_eq_self_implies_10 = thm "mult_eq_self_implies_10";


586 
val less_imp_succ_add = thm "less_imp_succ_add";


587 
val less_iff_succ_add = thm "less_iff_succ_add";


588 
val diff_is_0_iff = thm "diff_is_0_iff";


589 
val nat_lt_imp_diff_eq_0 = thm "nat_lt_imp_diff_eq_0";


590 
val nat_diff_split = thm "nat_diff_split";


591 
*}


592 

9548

593 
end
