Quelle ArithSimp.thy Sprache: Isabelle

(*  Title:      ZF/ArithSimp.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   2000  University of Cambridge
*)

section\<open>Arithmetic with simplification\<close>

theory ArithSimp
imports Arith
begin

subsection \<open>Arithmetic simplification\<close>

ML_file \<open>~~/src/Provers/Arith/cancel_numerals.ML\<close>
ML_file \<open>~~/src/Provers/Arith/combine_numerals.ML\<close>
ML_file \<open>arith_data.ML\<close>

simproc_setup nateq_cancel_numerals
  ("l #+ m = n" | "l = m #+ n" | "l #* m = n" | "l = m #* n" | "succ(m) = n" | "m = succ(n)") =
  \<open>K ArithData.nateq_cancel_numerals_proc\<close>

simproc_setup natless_cancel_numerals
  ("l #+ m < n" | "l < m #+ n" | "l #* m < n" | "l < m #* n" | "succ(m) < n" | "m < succ(n)") =
  \<open>K ArithData.natless_cancel_numerals_proc\<close>

simproc_setup natdiff_cancel_numerals
  ("(l #+ m) #- n" | "l #- (m #+ n)" | "(l #* m) #- n" | "l #- (m #* n)" |
    "succ(m) #- n" | "m #- succ(n)") =
  \<open>K ArithData.natdiff_cancel_numerals_proc\<close>

subsubsection \<open>Examples\<close>

lemma "x #+ y = x #+ z" apply simp oops
lemma "y #+ x = x #+ z" apply simp oops
lemma "x #+ y #+ z = x #+ z" apply simp oops
lemma "y #+ (z #+ x) = z #+ x" apply simp oops
lemma "x #+ y #+ z = (z #+ y) #+ (x #+ w)" apply simp oops
lemma "x#*y #+ z = (z #+ y) #+ (y#*x #+ w)" apply simp oops

lemma "x #+ succ(y) = x #+ z" apply simp oops
lemma "x #+ succ(y) = succ(z #+ x)" apply simp oops
lemma "succ(x) #+ succ(y) #+ z = succ(z #+ y) #+ succ(x #+ w)" apply simp oops

lemma "(x #+ y) #- (x #+ z) = w" apply simp oops
lemma "(y #+ x) #- (x #+ z) = dd" apply simp oops
lemma "(x #+ y #+ z) #- (x #+ z) = dd" apply simp oops
lemma "(y #+ (z #+ x)) #- (z #+ x) = dd" apply simp oops
lemma "(x #+ y #+ z) #- ((z #+ y) #+ (x #+ w)) = dd" apply simp oops
lemma "(x#*y #+ z) #- ((z #+ y) #+ (y#*x #+ w)) = dd" apply simp oops

(*BAD occurrence of natify*)
lemma "(x #+ succ(y)) #- (x #+ z) = dd" apply simp oops

lemma "x #* y2 #+ y #* x2 = y #* x2 #+ x #* y2" apply simp oops

lemma "(x #+ succ(y)) #- (succ(z #+ x)) = dd" apply simp oops
lemma "(succ(x) #+ succ(y) #+ z) #- (succ(z #+ y) #+ succ(x #+ w)) = dd" apply simp oops

(*use of typing information*)
lemma "x : nat ==> x #+ y = x" apply simp oops
lemma "x : nat --> x #+ y = x" apply simp oops
lemma "x : nat ==> x #+ y < x" apply simp oops
lemma "x : nat ==> x < y#+x" apply simp oops
lemma "x : nat ==> x \ succ(x)" apply simp oops

(*fails: no typing information isn't visible*)
lemma "x #+ y = x" apply simp? oops

lemma "x #+ y < x #+ z" apply simp oops
lemma "y #+ x < x #+ z" apply simp oops
lemma "x #+ y #+ z < x #+ z" apply simp oops
lemma "y #+ z #+ x < x #+ z" apply simp oops
lemma "y #+ (z #+ x) < z #+ x" apply simp oops
lemma "x #+ y #+ z < (z #+ y) #+ (x #+ w)" apply simp oops
lemma "x#*y #+ z < (z #+ y) #+ (y#*x #+ w)" apply simp oops

lemma "x #+ succ(y) < x #+ z" apply simp oops
lemma "x #+ succ(y) < succ(z #+ x)" apply simp oops
lemma "succ(x) #+ succ(y) #+ z < succ(z #+ y) #+ succ(x #+ w)" apply simp oops

lemma "x #+ succ(y) \ succ(z #+ x)" apply simp oops

subsection\<open>Difference\<close>

lemma diff_self_eq_0 [simp]: "m #- m = 0"
apply (subgoal_tac "natify (m) #- natify (m) = 0")
apply (rule_tac [2] natify_in_nat [THEN nat_induct], auto)
done

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

(*We need m:nat even if we replace the RHS by natify(m), for consider e.g.
  n=2, m=omega; then n + (m-n) = 2 + (0-2) = 2 \<noteq> 0 = natify(m).*)
lemma add_diff_inverse: "\n \ m; m:nat\ \ n #+ (m#-n) = m"
apply (frule lt_nat_in_nat, erule nat_succI)
apply (erule rev_mp)
apply (rule_tac m = m and n = n in diff_induct, auto)
done

lemma add_diff_inverse2: "\n \ m; m:nat\ \ (m#-n) #+ n = m"
apply (frule lt_nat_in_nat, erule nat_succI)
apply (simp (no_asm_simp) add: add_commute add_diff_inverse)
done

(*Proof is IDENTICAL to that of add_diff_inverse*)
lemma diff_succ: "\n \ m; m:nat\ \ succ(m) #- n = succ(m#-n)"
apply (frule lt_nat_in_nat, erule nat_succI)
apply (erule rev_mp)
apply (rule_tac m = m and n = n in diff_induct)
apply (simp_all (no_asm_simp))
done

lemma zero_less_diff [simp]:
     "\m: nat; n: nat\ \ 0 < (n #- m) \ m
apply (rule_tac m = m and n = n in diff_induct)
apply (simp_all (no_asm_simp))
done

(** Difference distributes over multiplication **)

lemma diff_mult_distrib: "(m #- n) #* k = (m #* k) #- (n #* k)"
apply (subgoal_tac " (natify (m) #- natify (n)) #* natify (k) = (natify (m) #* natify (k)) #- (natify (n) #* natify (k))")
apply (rule_tac [2] m = "natify (m) " and n = "natify (n) " in diff_induct)
apply (simp_all add: diff_cancel)
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

subsection\<open>Remainder\<close>

(*We need m:nat even with natify*)
lemma div_termination: "\0 m; m:nat\ \ m #- n < m"
apply (frule lt_nat_in_nat, erule nat_succI)
apply (erule rev_mp)
apply (erule rev_mp)
apply (rule_tac m = m and n = n in diff_induct)
apply (simp_all (no_asm_simp) add: diff_le_self)
done

(*for mod and div*)
lemmas div_rls =
    nat_typechecks Ord_transrec_type apply_funtype
    div_termination [THEN ltD]
    nat_into_Ord not_lt_iff_le [THEN iffD1]

lemma raw_mod_type: "\m:nat; n:nat\ \ raw_mod (m, n) \ nat"
  unfolding raw_mod_def
apply (rule Ord_transrec_type)
apply (auto simp add: nat_into_Ord [THEN Ord_0_lt_iff])
apply (blast intro: div_rls)
done

lemma mod_type [TC,iff]: "m mod n \ nat"
  unfolding mod_def
apply (simp (no_asm) add: mod_def raw_mod_type)
done

(** Aribtrary definitions for division by zero.  Useful to simplify
    certain equations **)

lemma DIVISION_BY_ZERO_DIV: "a div 0 = 0"
  unfolding div_def
apply (rule raw_div_def [THEN def_transrec, THEN trans])
apply (simp (no_asm_simp))
done  (*NOT for adding to default simpset*)

lemma DIVISION_BY_ZERO_MOD: "a mod 0 = natify(a)"
  unfolding mod_def
apply (rule raw_mod_def [THEN def_transrec, THEN trans])
apply (simp (no_asm_simp))
done  (*NOT for adding to default simpset*)

lemma raw_mod_less: "m raw_mod (m,n) = m"
apply (rule raw_mod_def [THEN def_transrec, THEN trans])
apply (simp (no_asm_simp) add: div_termination [THEN ltD])
done

lemma mod_less [simp]: "\m nat\ \ m mod n = m"
apply (frule lt_nat_in_nat, assumption)
apply (simp (no_asm_simp) add: mod_def raw_mod_less)
done

lemma raw_mod_geq:
     "\0 m; m:nat\ \ raw_mod (m, n) = raw_mod (m#-n, n)"
apply (frule lt_nat_in_nat, erule nat_succI)
apply (rule raw_mod_def [THEN def_transrec, THEN trans])
apply (simp (no_asm_simp) add: div_termination [THEN ltD] not_lt_iff_le [THEN iffD2], blast)
done

lemma mod_geq: "\n \ m; m:nat\ \ m mod n = (m#-n) mod n"
apply (frule lt_nat_in_nat, erule nat_succI)
apply (case_tac "n=0")
apply (simp add: DIVISION_BY_ZERO_MOD)
apply (simp add: mod_def raw_mod_geq nat_into_Ord [THEN Ord_0_lt_iff])
done

subsection\<open>Division\<close>

lemma raw_div_type: "\m:nat; n:nat\ \ raw_div (m, n) \ nat"
  unfolding raw_div_def
apply (rule Ord_transrec_type)
apply (auto simp add: nat_into_Ord [THEN Ord_0_lt_iff])
apply (blast intro: div_rls)
done

lemma div_type [TC,iff]: "m div n \ nat"
  unfolding div_def
apply (simp (no_asm) add: div_def raw_div_type)
done

lemma raw_div_less: "m raw_div (m,n) = 0"
apply (rule raw_div_def [THEN def_transrec, THEN trans])
apply (simp (no_asm_simp) add: div_termination [THEN ltD])
done

lemma div_less [simp]: "\m nat\ \ m div n = 0"
apply (frule lt_nat_in_nat, assumption)
apply (simp (no_asm_simp) add: div_def raw_div_less)
done

lemma raw_div_geq: "\0 m; m:nat\ \ raw_div(m,n) = succ(raw_div(m#-n, n))"
apply (subgoal_tac "n \ 0")
prefer 2 apply blast
apply (frule lt_nat_in_nat, erule nat_succI)
apply (rule raw_div_def [THEN def_transrec, THEN trans])
apply (simp (no_asm_simp) add: div_termination [THEN ltD] not_lt_iff_le [THEN iffD2] )
done

lemma div_geq [simp]:
     "\0 m; m:nat\ \ m div n = succ ((m#-n) div n)"
apply (frule lt_nat_in_nat, erule nat_succI)
apply (simp (no_asm_simp) add: div_def raw_div_geq)
done

declare div_less [simp] div_geq [simp]

(*A key result*)
lemma mod_div_lemma: "\m: nat; n: nat\ \ (m div n)#*n #+ m mod n = m"
apply (case_tac "n=0")
apply (simp add: DIVISION_BY_ZERO_MOD)
apply (simp add: nat_into_Ord [THEN Ord_0_lt_iff])
apply (erule complete_induct)
apply (case_tac "x)
txt\<open>case x<n\<close>
apply (simp (no_asm_simp))
txt\<open>case \<^term>\<open>n \<le> x\<close>\<close>
apply (simp add: not_lt_iff_le add_assoc mod_geq div_termination [THEN ltD] add_diff_inverse)
done

lemma mod_div_equality_natify: "(m div n)#*n #+ m mod n = natify(m)"
apply (subgoal_tac " (natify (m) div natify (n))#*natify (n) #+ natify (m) mod natify (n) = natify (m) ")
apply force
apply (subst mod_div_lemma, auto)
done

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

subsection\<open>Further Facts about Remainder\<close>

text\<open>(mainly for mutilated chess board)\<close>

lemma mod_succ_lemma:
     "\0
      \<Longrightarrow> succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))"
apply (erule complete_induct)
apply (case_tac "succ (x) )
txt\<open>case succ(x) < n\<close>
apply (simp (no_asm_simp) add: nat_le_refl [THEN lt_trans] succ_neq_self)
apply (simp add: ltD [THEN mem_imp_not_eq])
txt\<open>case \<^term>\<open>n \<le> succ(x)\<close>\<close>
apply (simp add: mod_geq not_lt_iff_le)
apply (erule leE)
apply (simp (no_asm_simp) add: mod_geq div_termination [THEN ltD] diff_succ)
txt\<open>equality case\<close>
apply (simp add: diff_self_eq_0)
done

lemma mod_succ:
  "n:nat \ succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))"
apply (case_tac "n=0")
apply (simp (no_asm_simp) add: natify_succ DIVISION_BY_ZERO_MOD)
apply (subgoal_tac "natify (succ (m)) mod n = (if succ (natify (m) mod n) = n then 0 else succ (natify (m) mod n))")
prefer 2
apply (subst natify_succ)
apply (rule mod_succ_lemma)
  apply (auto simp del: natify_succ simp add: nat_into_Ord [THEN Ord_0_lt_iff])
done

lemma mod_less_divisor: "\0 \ m mod n < n"
apply (subgoal_tac "natify (m) mod n < n")
apply (rule_tac [2] i = "natify (m) " in complete_induct)
apply (case_tac [3] "x, auto)
txt\<open>case \<^term>\<open>n \<le> x\<close>\<close>
apply (simp add: mod_geq not_lt_iff_le div_termination [THEN ltD])
done

lemma mod_1_eq [simp]: "m mod 1 = 0"
by (cut_tac n = 1 in mod_less_divisor, auto)

lemma mod2_cases: "b<2 \ k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)"
apply (subgoal_tac "k mod 2: 2")
prefer 2 apply (simp add: mod_less_divisor [THEN ltD])
apply (drule ltD, auto)
done

lemma mod2_succ_succ [simp]: "succ(succ(m)) mod 2 = m mod 2"
apply (subgoal_tac "m mod 2: 2")
prefer 2 apply (simp add: mod_less_divisor [THEN ltD])
apply (auto simp add: mod_succ)
done

lemma mod2_add_more [simp]: "(m#+m#+n) mod 2 = n mod 2"
apply (subgoal_tac " (natify (m) #+natify (m) #+n) mod 2 = n mod 2")
apply (rule_tac [2] n = "natify (m) " in nat_induct)
apply auto
done

lemma mod2_add_self [simp]: "(m#+m) mod 2 = 0"
by (cut_tac n = 0 in mod2_add_more, auto)

subsection\<open>Additional theorems about \<open>\<le>\<close>\<close>

lemma add_le_self: "m:nat \ m \ (m #+ n)"
apply (simp (no_asm_simp))
done

lemma add_le_self2: "m:nat \ m \ (n #+ m)"
apply (simp (no_asm_simp))
done

(*** Monotonicity of Multiplication ***)

lemma mult_le_mono1: "\i \ j; j:nat\ \ (i#*k) \ (j#*k)"
apply (subgoal_tac "natify (i) #*natify (k) \ j#*natify (k) ")
apply (frule_tac [2] lt_nat_in_nat)
apply (rule_tac [3] n = "natify (k) " in nat_induct)
apply (simp_all add: add_le_mono)
done

(* @{text"\<le>"} monotonicity, BOTH arguments*)
lemma mult_le_mono: "\i \ j; k \ l; j:nat; l:nat\ \ i#*k \ j#*l"
apply (rule mult_le_mono1 [THEN le_trans], assumption+)
apply (subst mult_commute, subst mult_commute, rule mult_le_mono1, assumption+)
done

(*strict, in 1st argument; proof is by induction on k>0.
  I can't see how to relax the typing conditions.*)
lemma mult_lt_mono2: "\i \ k#*i < k#*j"
apply (erule zero_lt_natE)
apply (frule_tac [2] lt_nat_in_nat)
apply (simp_all (no_asm_simp))
apply (induct_tac "x")
apply (simp_all (no_asm_simp) add: add_lt_mono)
done

lemma mult_lt_mono1: "\i \ i#*k < j#*k"
apply (simp (no_asm_simp) add: mult_lt_mono2 mult_commute [of _ k])
done

lemma add_eq_0_iff [iff]: "m#+n = 0 \ natify(m)=0 \ natify(n)=0"
apply (subgoal_tac "natify (m) #+ natify (n) = 0 \ natify (m) =0 \ natify (n) =0")
apply (rule_tac [2] n = "natify (m) " in natE)
apply (rule_tac [4] n = "natify (n) " in natE)
apply auto
done

lemma zero_lt_mult_iff [iff]: "0 < m#*n \ 0 < natify(m) \ 0 < natify(n)"
apply (subgoal_tac "0 < natify (m) #*natify (n) \ 0 < natify (m) \ 0 < natify (n) ")
apply (rule_tac [2] n = "natify (m) " in natE)
apply (rule_tac [4] n = "natify (n) " in natE)
  apply (rule_tac [3] n = "natify (n) " in natE)
apply auto
done

lemma mult_eq_1_iff [iff]: "m#*n = 1 \ natify(m)=1 \ natify(n)=1"
apply (subgoal_tac "natify (m) #* natify (n) = 1 \ natify (m) =1 \ natify (n) =1")
apply (rule_tac [2] n = "natify (m) " in natE)
apply (rule_tac [4] n = "natify (n) " in natE)
apply auto
done

lemma mult_is_zero: "\m: nat; n: nat\ \ (m #* n = 0) \ (m = 0 | n = 0)"
apply auto
apply (erule natE)
apply (erule_tac [2] natE, auto)
done

lemma mult_is_zero_natify [iff]:
     "(m #* n = 0) \ (natify(m) = 0 | natify(n) = 0)"
apply (cut_tac m = "natify (m) " and n = "natify (n) " in mult_is_zero)
apply auto
done

subsection\<open>Cancellation Laws for Common Factors in Comparisons\<close>

lemma mult_less_cancel_lemma:
     "\k: nat; m: nat; n: nat\ \ (m#*k < n#*k) \ (0 m
apply (safe intro!: mult_lt_mono1)
apply (erule natE, auto)
apply (rule not_le_iff_lt [THEN iffD1])
apply (drule_tac [3] not_le_iff_lt [THEN [2] rev_iffD2])
prefer 5 apply (blast intro: mult_le_mono1, auto)
done

lemma mult_less_cancel2 [simp]:
     "(m#*k < n#*k) \ (0 < natify(k) \ natify(m) < natify(n))"
apply (rule iff_trans)
apply (rule_tac [2] mult_less_cancel_lemma, auto)
done

lemma mult_less_cancel1 [simp]:
     "(k#*m < k#*n) \ (0 < natify(k) \ natify(m) < natify(n))"
apply (simp (no_asm) add: mult_less_cancel2 mult_commute [of k])
done

lemma mult_le_cancel2 [simp]: "(m#*k \ n#*k) \ (0 < natify(k) \ natify(m) \ natify(n))"
apply (simp (no_asm_simp) add: not_lt_iff_le [THEN iff_sym])
apply auto
done

lemma mult_le_cancel1 [simp]: "(k#*m \ k#*n) \ (0 < natify(k) \ natify(m) \ natify(n))"
apply (simp (no_asm_simp) add: not_lt_iff_le [THEN iff_sym])
apply auto
done

lemma mult_le_cancel_le1: "k \ nat \ k #* m \ k \ (0 < k \ natify(m) \ 1)"
by (cut_tac k = k and m = m and n = 1 in mult_le_cancel1, auto)

lemma Ord_eq_iff_le: "\Ord(m); Ord(n)\ \ m=n \ (m \ n \ n \ m)"
by (blast intro: le_anti_sym)

lemma mult_cancel2_lemma:
     "\k: nat; m: nat; n: nat\ \ (m#*k = n#*k) \ (m=n | k=0)"
apply (simp (no_asm_simp) add: Ord_eq_iff_le [of "m#*k"] Ord_eq_iff_le [of m])
apply (auto simp add: Ord_0_lt_iff)
done

lemma mult_cancel2 [simp]:
     "(m#*k = n#*k) \ (natify(m) = natify(n) | natify(k) = 0)"
apply (rule iff_trans)
apply (rule_tac [2] mult_cancel2_lemma, auto)
done

lemma mult_cancel1 [simp]:
     "(k#*m = k#*n) \ (natify(m) = natify(n) | natify(k) = 0)"
apply (simp (no_asm) add: mult_cancel2 mult_commute [of k])
done

(** Cancellation law for division **)

lemma div_cancel_raw:
     "\0 \ (k#*m) div (k#*n) = m div n"
apply (erule_tac i = m in complete_induct)
apply (case_tac "x)
apply (simp add: div_less zero_lt_mult_iff mult_lt_mono2)
apply (simp add: not_lt_iff_le zero_lt_mult_iff le_refl [THEN mult_le_mono]
          div_geq diff_mult_distrib2 [symmetric] div_termination [THEN ltD])
done

lemma div_cancel:
     "\0 < natify(n); 0 < natify(k)\ \ (k#*m) div (k#*n) = m div n"
apply (cut_tac k = "natify (k) " and m = "natify (m)" and n = "natify (n)"
       in div_cancel_raw)
apply auto
done

subsection\<open>More Lemmas about Remainder\<close>

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)
apply (case_tac "n=0")
apply (simp add: DIVISION_BY_ZERO_MOD)
apply (simp add: nat_into_Ord [THEN Ord_0_lt_iff])
apply (erule_tac i = m in complete_induct)
apply (case_tac "x)
apply (simp (no_asm_simp) add: mod_less zero_lt_mult_iff mult_lt_mono2)
apply (simp add: not_lt_iff_le zero_lt_mult_iff le_refl [THEN mult_le_mono]
         mod_geq diff_mult_distrib2 [symmetric] div_termination [THEN ltD])
done

lemma mod_mult_distrib2: "k #* (m mod n) = (k#*m) mod (k#*n)"
apply (cut_tac k = "natify (k) " and m = "natify (m)" and n = "natify (n)"
       in mult_mod_distrib_raw)
apply auto
done

lemma mult_mod_distrib: "(m mod n) #* k = (m#*k) mod (n#*k)"
apply (simp (no_asm) add: mult_commute mod_mult_distrib2)
done

lemma mod_add_self2_raw: "n \ nat \ (m #+ n) mod n = m mod n"
apply (subgoal_tac " (n #+ m) mod n = (n #+ m #- n) mod n")
apply (simp add: add_commute)
apply (subst mod_geq [symmetric], auto)
done

lemma mod_add_self2 [simp]: "(m #+ n) mod n = m mod n"
apply (cut_tac n = "natify (n) " in mod_add_self2_raw)
apply auto
done

lemma mod_add_self1 [simp]: "(n#+m) mod n = m mod n"
apply (simp (no_asm_simp) add: add_commute mod_add_self2)
done

lemma mod_mult_self1_raw: "k \ nat \ (m #+ k#*n) mod n = m mod n"
apply (erule nat_induct)
apply (simp_all (no_asm_simp) add: add_left_commute [of _ n])
done

lemma mod_mult_self1 [simp]: "(m #+ k#*n) mod n = m mod n"
apply (cut_tac k = "natify (k) " in mod_mult_self1_raw)
apply auto
done

lemma mod_mult_self2 [simp]: "(m #+ n#*k) mod n = m mod n"
apply (simp (no_asm) add: mult_commute mod_mult_self1)
done

(*Lemma for gcd*)
lemma mult_eq_self_implies_10: "m = m#*n \ natify(n)=1 | m=0"
apply (subgoal_tac "m: nat")
prefer 2
apply (erule ssubst)
apply simp
apply (rule disjCI)
apply (drule sym)
apply (rule Ord_linear_lt [of "natify(n)" 1])
apply simp_all
apply (subgoal_tac "m #* n = 0", simp)
apply (subst mult_natify2 [symmetric])
apply (simp del: mult_natify2)
apply (drule nat_into_Ord [THEN Ord_0_lt, THEN [2] mult_lt_mono2], auto)
done

lemma less_imp_succ_add [rule_format]:
     "\m \ \k\nat. n = succ(m#+k)"
apply (frule lt_nat_in_nat, assumption)
apply (erule rev_mp)
apply (induct_tac "n")
apply (simp_all (no_asm) add: le_iff)
apply (blast elim!: leE intro!: add_0_right [symmetric] add_succ_right [symmetric])
done

lemma less_iff_succ_add:
     "\m: nat; n: nat\ \ (m (\k\nat. n = succ(m#+k))"
by (auto intro: less_imp_succ_add)

lemma add_lt_elim2:
     "\a #+ d = b #+ c; a < b; b \ nat; c \ nat; d \ nat\ \ c < d"
by (drule less_imp_succ_add, auto)

lemma add_le_elim2:
     "\a #+ d = b #+ c; a \ b; b \ nat; c \ nat; d \ nat\ \ c \ d"
by (drule less_imp_succ_add, auto)

subsubsection\<open>More Lemmas About Difference\<close>

lemma diff_is_0_lemma:
     "\m: nat; n: nat\ \ m #- n = 0 \ m \ n"
apply (rule_tac m = m and n = n in diff_induct, simp_all)
done

lemma diff_is_0_iff: "m #- n = 0 \ natify(m) \ natify(n)"
by (simp add: diff_is_0_lemma [symmetric])

lemma nat_lt_imp_diff_eq_0:
     "\a:nat; b:nat; a \ a #- b = 0"
by (simp add: diff_is_0_iff le_iff)

lemma raw_nat_diff_split:
     "\a:nat; b:nat\ \
      (P(a #- b)) \<longleftrightarrow> ((a < b \<longrightarrow>P(0)) \<and> (\<forall>d\<in>nat. a = b #+ d \<longrightarrow> P(d)))"
apply (case_tac "a < b")
apply (force simp add: nat_lt_imp_diff_eq_0)
apply (rule iffI, force, simp)
apply (drule_tac x="a#-b" in bspec)
apply (simp_all add: Ordinal.not_lt_iff_le add_diff_inverse)
done

lemma nat_diff_split:
   "(P(a #- b)) \
    (natify(a) < natify(b) \<longrightarrow>P(0)) \<and> (\<forall>d\<in>nat. natify(a) = b #+ d \<longrightarrow> P(d))"
apply (cut_tac P=P and a="natify(a)" and b="natify(b)" in raw_nat_diff_split)
apply simp_all
done

text\<open>Difference and less-than\<close>

lemma diff_lt_imp_lt: "\(k#-i) < (k#-j); i\nat; j\nat; k\nat\ \ j
apply (erule rev_mp)
apply (simp split: nat_diff_split, auto)
apply (blast intro: add_le_self lt_trans1)
apply (rule not_le_iff_lt [THEN iffD1], auto)
apply (subgoal_tac "i #+ da < j #+ d", force)
apply (blast intro: add_le_lt_mono)
done

lemma lt_imp_diff_lt: "\jk; k\nat\ \ (k#-i) < (k#-j)"
apply (frule le_in_nat, assumption)
apply (frule lt_nat_in_nat, assumption)
apply (simp split: nat_diff_split, auto)
  apply (blast intro: lt_asym lt_trans2)
apply (blast intro: lt_irrefl lt_trans2)
apply (rule not_le_iff_lt [THEN iffD1], auto)
apply (subgoal_tac "j #+ d < i #+ da", force)
apply (blast intro: add_lt_le_mono)
done

lemma diff_lt_iff_lt: "\i\k; j\nat; k\nat\ \ (k#-i) < (k#-j) \ j
apply (frule le_in_nat, assumption)
apply (blast intro: lt_imp_diff_lt diff_lt_imp_lt)
done

end

quality100%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.18Bemerkung: (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.