diff -r c663e675e177 -r b8ef7afe3a6b src/ZF/Arith.thy --- a/src/ZF/Arith.thy Sun Oct 07 15:49:25 2007 +0200 +++ b/src/ZF/Arith.thy Sun Oct 07 21:19:31 2007 +0200 @@ -17,11 +17,12 @@ text{*Proofs about elementary arithmetic: addition, multiplication, etc.*} -constdefs - pred :: "i=>i" (*inverse of succ*) +definition + pred :: "i=>i" (*inverse of succ*) where "pred(y) == nat_case(0, %x. x, y)" - natify :: "i=>i" (*coerces non-nats to nats*) +definition + natify :: "i=>i" (*coerces non-nats to nats*) where "natify == Vrecursor(%f a. if a = succ(pred(a)) then succ(f`pred(a)) else 0)" @@ -43,36 +44,41 @@ "raw_mult(0, n) = 0" "raw_mult(succ(m), n) = raw_add (n, raw_mult(m, n))" -constdefs - add :: "[i,i]=>i" (infixl "#+" 65) +definition + add :: "[i,i]=>i" (infixl "#+" 65) where "m #+ n == raw_add (natify(m), natify(n))" - diff :: "[i,i]=>i" (infixl "#-" 65) +definition + diff :: "[i,i]=>i" (infixl "#-" 65) where "m #- n == raw_diff (natify(m), natify(n))" - mult :: "[i,i]=>i" (infixl "#*" 70) +definition + mult :: "[i,i]=>i" (infixl "#*" 70) where "m #* n == raw_mult (natify(m), natify(n))" - raw_div :: "[i,i]=>i" +definition + raw_div :: "[i,i]=>i" where "raw_div (m, n) == transrec(m, %j f. if ji" +definition + raw_mod :: "[i,i]=>i" where "raw_mod (m, n) == transrec(m, %j f. if ji" (infixl "div" 70) +definition + div :: "[i,i]=>i" (infixl "div" 70) where "m div n == raw_div (natify(m), natify(n))" - mod :: "[i,i]=>i" (infixl "mod" 70) +definition + mod :: "[i,i]=>i" (infixl "mod" 70) where "m mod n == raw_mod (natify(m), natify(n))" -syntax (xsymbols) - "mult" :: "[i,i] => i" (infixr "#\" 70) +notation (xsymbols) + mult (infixr "#\" 70) -syntax (HTML output) - "mult" :: "[i, i] => i" (infixr "#\" 70) - +notation (HTML output) + mult (infixr "#\" 70) declare rec_type [simp] nat_0_le [simp] @@ -548,94 +554,4 @@ lemmas nat_typechecks = rec_type nat_0I nat_1I nat_succI Ord_nat -ML -{* -val pred_def = thm "pred_def"; -val raw_div_def = thm "raw_div_def"; -val raw_mod_def = thm "raw_mod_def"; -val div_def = thm "div_def"; -val mod_def = thm "mod_def"; - -val zero_lt_natE = thm "zero_lt_natE"; -val pred_succ_eq = thm "pred_succ_eq"; -val natify_succ = thm "natify_succ"; -val natify_0 = thm "natify_0"; -val natify_non_succ = thm "natify_non_succ"; -val natify_in_nat = thm "natify_in_nat"; -val natify_ident = thm "natify_ident"; -val natify_eqE = thm "natify_eqE"; -val natify_idem = thm "natify_idem"; -val add_natify1 = thm "add_natify1"; -val add_natify2 = thm "add_natify2"; -val mult_natify1 = thm "mult_natify1"; -val mult_natify2 = thm "mult_natify2"; -val diff_natify1 = thm "diff_natify1"; -val diff_natify2 = thm "diff_natify2"; -val mod_natify1 = thm "mod_natify1"; -val mod_natify2 = thm "mod_natify2"; -val div_natify1 = thm "div_natify1"; -val div_natify2 = thm "div_natify2"; -val raw_add_type = thm "raw_add_type"; -val add_type = thm "add_type"; -val raw_mult_type = thm "raw_mult_type"; -val mult_type = thm "mult_type"; -val raw_diff_type = thm "raw_diff_type"; -val diff_type = thm "diff_type"; -val diff_0_eq_0 = thm "diff_0_eq_0"; -val diff_succ_succ = thm "diff_succ_succ"; -val diff_0 = thm "diff_0"; -val diff_le_self = thm "diff_le_self"; -val add_0_natify = thm "add_0_natify"; -val add_succ = thm "add_succ"; -val add_0 = thm "add_0"; -val add_assoc = thm "add_assoc"; -val add_0_right_natify = thm "add_0_right_natify"; -val add_succ_right = thm "add_succ_right"; -val add_0_right = thm "add_0_right"; -val add_commute = thm "add_commute"; -val add_left_commute = thm "add_left_commute"; -val raw_add_left_cancel = thm "raw_add_left_cancel"; -val add_left_cancel_natify = thm "add_left_cancel_natify"; -val add_left_cancel = thm "add_left_cancel"; -val add_le_elim1_natify = thm "add_le_elim1_natify"; -val add_le_elim1 = thm "add_le_elim1"; -val add_lt_elim1_natify = thm "add_lt_elim1_natify"; -val add_lt_elim1 = thm "add_lt_elim1"; -val add_lt_mono1 = thm "add_lt_mono1"; -val add_lt_mono2 = thm "add_lt_mono2"; -val add_lt_mono = thm "add_lt_mono"; -val Ord_lt_mono_imp_le_mono = thm "Ord_lt_mono_imp_le_mono"; -val add_le_mono1 = thm "add_le_mono1"; -val add_le_mono = thm "add_le_mono"; -val diff_add_inverse = thm "diff_add_inverse"; -val diff_add_inverse2 = thm "diff_add_inverse2"; -val diff_cancel = thm "diff_cancel"; -val diff_cancel2 = thm "diff_cancel2"; -val diff_add_0 = thm "diff_add_0"; -val eq_add_iff = thm "eq_add_iff"; -val less_add_iff = thm "less_add_iff"; -val diff_add_eq = thm "diff_add_eq"; -val eq_cong2 = thm "eq_cong2"; -val iff_cong2 = thm "iff_cong2"; -val mult_0 = thm "mult_0"; -val mult_succ = thm "mult_succ"; -val mult_0_right = thm "mult_0_right"; -val mult_succ_right = thm "mult_succ_right"; -val mult_1_natify = thm "mult_1_natify"; -val mult_1_right_natify = thm "mult_1_right_natify"; -val mult_1 = thm "mult_1"; -val mult_1_right = thm "mult_1_right"; -val mult_commute = thm "mult_commute"; -val add_mult_distrib = thm "add_mult_distrib"; -val add_mult_distrib_left = thm "add_mult_distrib_left"; -val mult_assoc = thm "mult_assoc"; -val mult_left_commute = thm "mult_left_commute"; -val lt_succ_eq_0_disj = thm "lt_succ_eq_0_disj"; -val less_diff_conv = thm "less_diff_conv"; - -val add_ac = thms "add_ac"; -val mult_ac = thms "mult_ac"; -val nat_typechecks = thms "nat_typechecks"; -*} - end