Theory HypNat

(*  Title:      HOL/Nat.thy
    ID:         $Id: Nat.thy,v 1.43 2004/01/09 09:46:19 paulson Exp $
    Author:     Tobias Nipkow and Lawrence C Paulson

Type "nat" is a linear order, and a datatype; arithmetic operators + -
and * (for div, mod and dvd, see theory Divides).
*)

header {* Hyper-Natural numbers *}

theory HypNat
imports StarClasses
begin

syntax hSuc :: "nat star => nat star"
translations "hSuc" \<rightleftharpoons> "Ifun_of Suc"

lemma star_of_Suc: "star_of (Suc n) = hSuc (star_of n)"
  by transfer simp


text {* Distinctness of constructors *}

lemma hSuc_not_Zero [iff]: "!!m. hSuc m ≠ 0"
  by transfer (rule Suc_not_Zero)

lemma Zero_not_hSuc [iff]: "!!m. 0 ≠ hSuc m"
  by transfer (rule Zero_not_Suc)

lemma hSuc_neq_Zero: "!!m. hSuc m = 0 ==> R"
  by transfer (rule Suc_neq_Zero)

lemma Zero_neq_hSuc: "!!m. 0 = hSuc m ==> R"
  by transfer (rule Zero_neq_Suc)

text {* Injectiveness of @{term Suc} *}

(* belongs in Fun.thy *)
lemma inj_def: "inj f ≡ ∀x y. f x = f y --> x = y"
by (simp add: inj_on_def)

lemma inj_hSuc: "inj hSuc"
  by (transfer inj_def, rule inj_Suc)

lemma hSuc_inject: "!!x y. hSuc x = hSuc y ==> x = y"
  by transfer (rule Suc_inject)

lemma hSuc_hSuc_eq [iff]: "!!m n. (hSuc m = hSuc n) = (m = n)"
  by transfer (rule Suc_Suc_eq)

lemma hypnat_not_singleton: "(∀x. x = (0::nat star)) = False"
  by transfer (rule nat_not_singleton)

lemma n_not_hSuc_n: "!!n. n ≠ hSuc n"
  by transfer (rule n_not_Suc_n)

lemma hSuc_n_not_n: "!!t. hSuc t ≠ t"
  by transfer (rule Suc_n_not_n)

subsubsection {* Introduction properties *}

(* less_trans is instance of order_less_trans *)

lemma star_lessI [iff]: "!!n. n < hSuc n"
  by transfer (rule lessI)

lemma less_hSucI: "!!i j. i < j ==> i < hSuc j"
  by transfer (rule less_SucI)

lemma zero_less_hSuc [iff]: "!!n. 0 < hSuc n"
  by transfer (rule zero_less_Suc)

subsubsection {* Elimination properties *}

(* less_not_sym instance of order_less_imp_not_less *)

(* less_asym instance of order_less_asym *)

(* less_not_refl instance of order_less_irrefl *)

(* less_irrefl comes from order class *)
(* less_not_refl2 *)
(* less_not_refl3 *)

lemma star_lessE:
  "!!i k. [|i < k; k = hSuc i ==> P; !!j. [|i < j; k = hSuc j|] ==> P|] ==> P"
  by transfer (erule lessE, fast, fast)

lemma star_not_less0 [iff]: "!!n. ~ n < (0::nat star)"
  by transfer (rule not_less0)

lemma star_less_zeroE: "!!n. (n::nat star) < 0 ==> R"
  by transfer (rule less_zeroE)

lemma less_hSucE:
  "!!m n. [|m < hSuc n; m < n ==> P; m = n ==> P|] ==> P"
  by transfer (erule less_SucE, fast, fast)

lemma less_hSuc_eq: "!!m n. (m < hSuc n) = (m < n | m = n)"
  by transfer (rule less_Suc_eq)

lemma star_less_one [iff]: "!!n. (n < (1::nat star)) = (n = 0)"
  by transfer (rule less_one)

lemma less_hSuc0 [iff]: "!!n. (n < hSuc 0) = (n = 0)"
  by transfer (rule less_Suc0)

lemma hSuc_mono: "!!m n. m < n ==> hSuc m < hSuc n"
  by transfer (rule Suc_mono)

text {* "Less than" is antisymmetric, sort of *}
lemma star_less_antisym: "!!m n. [|¬ n < m; n < hSuc m|] ==> m = n"
  by transfer (rule less_antisym)

(* nat_neq_iff instance of linorder_neq_iff *)

(* nat_less_cases instance of linorder_cases *)


subsubsection {* Inductive (?) properties *}

lemma hSuc_lessI: "!!m n. m < n ==> hSuc m ≠ n ==> hSuc m < n"
  by transfer (rule Suc_lessI)

lemma hSuc_lessD: "!!m n. hSuc m < n ==> m < n"
  by transfer (rule Suc_lessD)

lemma hSuc_lessE:
  "!!i k. [|hSuc i < k; !!j. i < j ==> k = hSuc j ==> P|] ==> P"
  by transfer (erule Suc_lessE, fast)

lemma hSuc_less_hSucD: "!!m n. hSuc m < hSuc n ==> m < n"
  by transfer (rule Suc_less_SucD)

lemma hSuc_less_eq [iff]: "!!m n. (hSuc m < hSuc n) = (m < n)"
  by transfer (rule Suc_less_eq)

lemma less_trans_hSuc: "!!i j k. i < j ==> j < k ==> hSuc i < k"
  by transfer (rule less_trans_Suc)

text {* Can be used with @{text less_hSuc_eq} to get @{term "n = m | n < m"} *}
lemma star_not_less_eq: "!!m n. (~ m < n) = (n < hSuc m)"
  by transfer (rule not_less_eq)

subsection {* Properties of "less than or equal" *}

text {* Was @{text le_eq_less_hSuc}, but this orientation is more useful *}
lemma less_hSuc_eq_le: "!!m n. (m < hSuc n) = (m ≤ n)"
  by transfer (rule less_Suc_eq_le)

lemma le_imp_less_hSuc: "!!m n. m ≤ n ==> m < hSuc n"
  by transfer (rule le_imp_less_Suc)

lemma star_le0 [iff]: "!!n. (0::nat star) ≤ n"
  by transfer (rule le0)

lemma hSuc_n_not_le_n: "!!n. ~ hSuc n ≤ n"
  by transfer (rule Suc_n_not_le_n)

lemma star_le_0_eq [iff]: "!!i. ((i::nat star) ≤ 0) = (i = 0)"
  by transfer (rule le_0_eq)

lemma le_hSuc_eq: "!!m n. (m ≤ hSuc n) = (m ≤ n | m = hSuc n)"
  by transfer (rule le_Suc_eq)

lemma le_hSucE:
  "!!m n. m ≤ hSuc n ==> (m ≤ n ==> R) ==> (m = hSuc n ==> R) ==> R"
  by transfer (erule le_SucE, fast, fast)

lemma star_leI: "!!m n. ~ n < m ==> m ≤ (n::nat star)"
  by transfer (rule leI)

lemma star_leD: "!!m n. m ≤ n ==> ~ n < (m::nat star)"
  by transfer (rule leD)

lemmas star_leE = star_leD [elim_format]

(* not_less_iff_le instance of linorder_not_less *)

(* not_leE instance of linorder_not_le[THEN iffD1] *)

(* not_le_iff_less instance of linorder_not_le *)

lemma hSuc_leI: "!!m n. m < n ==> hSuc(m) ≤ n"
  by transfer (rule Suc_leI)

lemma hSuc_leD: "!!m n. hSuc(m) ≤ n ==> m ≤ n"
  by transfer (rule Suc_leD)

text {* Stronger version of @{text hSuc_leD} *}
lemma hSuc_le_lessD: "!!m n. hSuc m ≤ n ==> m < n"
  by transfer (rule Suc_le_lessD)

lemma hSuc_le_eq: "!!m n. (hSuc m ≤ n) = (m < n)"
  by transfer (rule Suc_le_eq)

lemma le_hSucI: "!!m n. m ≤ n ==> m ≤ hSuc n"
  by transfer (rule le_SucI)

(* less_imp_le instance of order_less_imp_le *)

text {* For instance, @{text "(hSuc m < hSuc n) = (hSuc m ≤ n) = (m < n)"} *}
lemmas star_le_simps = order_less_imp_le less_hSuc_eq_le hSuc_le_eq


text {* Equivalence of @{term "m ≤ n"} and @{term "m < n | m = n"} *}

(* le_imp_less_or_eq instance of order_le_imp_less_or_eq *)

(* less_or_eq_imp_le instance of order_le_less[THEN iffD2] *)

(* le_eq_less_or_eq instance of order_le_less *)

(* eq_imp_le from order class *)

(* le_refl instance of order_refl *)

(* le_less_trans instance of order_le_less_trans *)

(* less_le_trans instance of order_less_le_trans *)

(* le_trans instance of order_trans *)

(* le_anti_sym instance of order_antisym *)

lemma hSuc_le_mono [iff]: "!!m n. (hSuc n ≤ hSuc m) = (n ≤ m)"
  by transfer (rule Suc_le_mono)

(* nat_less_le instance of order_less_le *)

(* le_neq_implies_less from order class *)

(* nat_le_linear instance of linorder_linear *)

lemma not_less_less_hSuc_eq: "!!m n. ~ n < m ==> (n < hSuc m) = (n = m)"
  by transfer (rule not_less_less_Suc_eq)

lemma le_less_hSuc_eq: "!!m n. m ≤ n ==> (n < hSuc m) = (n = m)"
  by transfer (rule le_less_Suc_eq)

lemmas star_not_less_simps = not_less_less_hSuc_eq le_less_hSuc_eq


subsection {* Arithmetic operators *}

(* add_0 instance of comm_monoid_add.add_0 *)

lemma add_hSuc [simp]: "!!m n. hSuc m + n = hSuc (m + n)"
  by transfer (rule add_Suc)

lemma star_diff_0 [simp]: "!!m. m - 0 = (m::nat star)"
  by transfer (rule diff_0)

(* TODO: hnat_case *)
(* lemma diff_hSuc: "m - hSuc n = (case m - n of 0 => 0 | hSuc k => k)" *)

(* mult_0 instance of mult_zero_left *)

lemma mult_hSuc [simp]: "!!m n. hSuc m * n = n + (m * n)"
  by transfer (rule mult_Suc)

lemma not0_implies_hSuc: "!!n. n ≠ 0 ==> ∃m. n = hSuc m"
  by transfer (rule not0_implies_Suc)

lemma star_gr_implies_not0: "!!m n::nat star. m<n ==> n ≠ 0"
  by transfer (rule gr_implies_not0)

lemma star_neq0_conv [iff]: "!!n::nat star. (n ≠ 0) = (0 < n)"
  by transfer (rule neq0_conv)

text {* This theorem is useful with @{text blast} *}
lemma star_gr0I: "!!n. ((n::nat star) = 0 ==> False) ==> 0 < n"
  by transfer (rule gr0I, fast)

lemma gr0_conv_hSuc: "!!n. (0 < n) = (∃m. n = hSuc m)"
  by transfer (rule gr0_conv_Suc)

lemma star_not_gr0 [iff]: "!!n::nat star. (~ (0 < n)) = (n = 0)"
  by transfer (rule not_gr0)

lemma hSuc_le_D: "!!n m'. (hSuc n ≤ m') ==> (? m. m' = hSuc m)"
  by transfer (rule Suc_le_D)

text {* Useful in certain inductive arguments *}
lemma less_hSuc_eq_0_disj:
  "!!m n. (m < hSuc n) = (m = 0 | (∃j. m = hSuc j & j < n))"
  by transfer (rule less_Suc_eq_0_disj)


subsection {* @{term min} and @{term max} *}

lemma star_min_0L [simp]: "!!n. min 0 n = (0::nat star)"
  by (transfer min_def, rule min_0L)

lemma star_min_0R [simp]: "!!n. min n 0 = (0::nat star)"
  by (transfer min_def, rule min_0R)

lemma min_hSuc_hSuc [simp]: "!!m n. min (hSuc m) (hSuc n) = hSuc (min m n)"
  by (transfer min_def, rule min_Suc_Suc)

lemma star_max_0L [simp]: "!!n. max 0 n = (n::nat star)"
  by (transfer max_def, rule max_0L)

lemma star_max_0R [simp]: "!!n. max n 0 = (n::nat star)"
  by (transfer max_def, rule max_0R)

lemma max_hSuc_hSuc [simp]: "!!m n. max (hSuc m) (hSuc n) = hSuc(max m n)"
  by (transfer max_def, rule max_Suc_Suc)


subsection {* Basic rewrite rules for the arithmetic operators *}

text {* Difference *}

lemma star_diff_0_eq_0 [simp]: "!!n. 0 - n = (0::nat star)"
  by transfer (rule diff_0_eq_0)

lemma diff_hSuc_hSuc [simp]: "!!m n. hSuc(m) - hSuc(n) = m - n"
  by transfer (rule diff_Suc_Suc)


text {*
  Could be (and is, below) generalized in various ways
  However, none of the generalizations are currently in the simpset,
  and I dread to think what happens if I put them in
*}
lemma hSuc_pred [simp]: "!!n. 0 < n ==> hSuc (n - hSuc 0) = n"
  by transfer (rule Suc_pred)

(* declare diff_hSuc [simp del, code del] *)


subsection {* Addition *}

(* add_0_right is instance of comm_monoid_add.add_0_right *)

lemma add_hSuc_right [simp]: "!!m n. m + hSuc n = hSuc (m + n)"
  by transfer (rule add_Suc_right)

(* nat_add_assoc instance of add_assoc *)

(* nat_add_commute instance of add_commute *)

(* nat_add_left_commute instance of add_left_commute *)

(* nat_add_left_cancel instance of add_left_cancel *)

(* nat_add_right_cancel instance of add_right_cancel *)

(* nat_add_left_cancel_le instance of add_le_cancel_left *)

(* nat_add_left_cancel_less instance of add_less_cancel_left *)

text {* Reasoning about @{text "m + 0 = 0"}, etc. *}

lemma star_add_is_0 [iff]: "!!m n::nat star. (m + n = 0) = (m = 0 & n = 0)"
  by transfer (rule add_is_0)

lemma star_add_is_1:
  "!!m n. (m+n= hSuc 0) = (m= hSuc 0 & n=0 | m=0 & n= hSuc 0)"
  by transfer (rule add_is_1)

lemma star_one_is_add:
  "!!m n. (hSuc 0 = m + n) = (m = hSuc 0 & n = 0 | m = 0 & n = hSuc 0)"
  by transfer (rule one_is_add)

lemma star_add_gr_0 [iff]: "!!m n::nat star. (0 < m + n) = (0 < m | 0 < n)"
  by transfer (rule add_gr_0)

lemma star_add_eq_self_zero: "!!m n::nat star. m + n = m ==> n = 0"
  by transfer (rule add_eq_self_zero)


subsection {* Multiplication *}

(* mult_0_right instance of mult_zero_right *)

lemma mult_hSuc_right [simp]: "!!m n. m * hSuc n = m + (m * n)"
  by transfer (rule mult_Suc_right)

(* nat_mult_commute instance of mult_commute *)

(* add_mult_distrib instance of left_distrib *)

(* add_mult_distrib2 instance of right_distrib *)

(* nat_mult_assoc instance of mult_assoc *)

lemma star_mult_is_0 [simp]: "!!m n. ((m::nat star) * n = 0) = (m=0 | n=0)"
  by transfer (rule mult_is_0)

subsection {* Monotonicity of Addition *}

(* add_less_mono1 instance of add_strict_right_mono *)

(* add_less_mono instance of add_strict_mono *)

lemma less_imp_hSuc_add: "!!m n. m < n ==> (∃k. n = hSuc (m + k))"
  by transfer (rule less_imp_Suc_add)

(* mult_less_mono2 instance of mult_strict_left_mono *)

(* nat_mult_1 instance of mult_1_left *)

(* nat_mult_1_right instance of mult_1_right *)


subsection {* Additional theorems about "less than" *}

(* TODO: should be generalized in Nat.thy *)
text {* A [clumsy] way of lifting @{text "<"}
  monotonicity to @{text "≤"} monotonicity *}
lemma order_less_mono_imp_le_mono:
  assumes lt_mono: "!!i j::'a::order. i < j ==> f i < f j"
  and le: "i ≤ j" shows "f i ≤ ((f j)::'b::order)" using le
  apply (simp add: order_le_less)
  apply (blast intro!: lt_mono)
  done

(* add_le_mono1 instance of add_right_mono *)

(* add_le_mono instance of add_mono *)

lemma star_le_add2: "!!m n. n ≤ ((m + n)::nat star)"
  by transfer (rule le_add2)

lemma star_le_add1: "!!m n. n ≤ ((n + m)::nat star)"
  by transfer (rule le_add1)

lemma less_add_hSuc1: "!!i m. i < hSuc (i + m)"
  by transfer (rule less_add_Suc1)

lemma less_add_hSuc2: "!!i m. i < hSuc (m + i)"
  by transfer (rule less_add_Suc2)

lemma less_iff_hSuc_add: "!!m n. (m < n) = (∃k. n = hSuc (m + k))"
  by transfer (rule less_iff_Suc_add)

lemma star_trans_le_add1: "!!i j m. (i::nat star) ≤ j ==> i ≤ j + m"
  by transfer (rule trans_le_add1)

lemma star_trans_le_add2: "!!i j m. (i::nat star) ≤ j ==> i ≤ m + j"
  by transfer (rule trans_le_add2)

lemma star_trans_less_add1: "!!i j m. (i::nat star) < j ==> i < j + m"
  by transfer (rule trans_less_add1)

lemma star_trans_less_add2: "!!i j m. (i::nat star) < j ==> i < m + j"
  by transfer (rule trans_less_add2)

lemma star_add_lessD1: "!!i j k. i + j < (k::nat star) ==> i < k"
  by transfer (rule add_lessD1)

lemma star_not_add_less1 [iff]: "!!i j. ~ (i + j < (i::nat star))"
  by transfer (rule not_add_less1)

lemma star_not_add_less2 [iff]: "!!i j. ~ (j + i < (i::nat star))"
  by transfer (rule not_add_less2)

lemma star_add_leD1: "!!k m n. m + k ≤ n ==> m ≤ (n::nat star)"
  by transfer (rule add_leD1)

lemma star_add_leD2: "!!k m n. m + k ≤ n ==> k ≤ (n::nat star)"
  by transfer (rule add_leD2)

lemma star_add_leE:
  "!!k m n. (m::nat star) + k ≤ n ==> (m ≤ n ==> k ≤ n ==> R) ==> R"
  by transfer (erule add_leE, fast)

text {* needs @{text "!!k"} for @{text add_ac} to work *}
lemma star_less_add_eq_less:
  "!!k l m n::nat star. k < l ==> m + l = k + n ==> m < n"
  by transfer (rule less_add_eq_less)


subsection {* Difference *}

lemma star_diff_self_eq_0 [simp]: "!!m. (m::nat star) - m = 0"
  by transfer (rule diff_self_eq_0)

text {* Addition is the inverse of subtraction:
  if @{term "n ≤ m"} then @{term "n + (m - n) = m"}. *}
lemma star_add_diff_inverse: "!!m n. ~  m < n ==> n + (m - n) = (m::nat star)"
  by transfer (rule add_diff_inverse)

lemma star_le_add_diff_inverse [simp]:
  "!!m n. n ≤ m ==> n + (m - n) = (m::nat star)"
  by transfer (rule le_add_diff_inverse)

lemma star_le_add_diff_inverse2 [simp]:
  "!!m n. n ≤ m ==> (m - n) + n = (m::nat star)"
  by transfer (rule le_add_diff_inverse2)


subsection {* More results about difference *}

lemma hSuc_diff_le: "!!m n. n ≤ m ==> hSuc m - n = hSuc (m - n)"
  by transfer (rule Suc_diff_le)

lemma diff_less_hSuc: "!!m n. m - n < hSuc m"
  by transfer (rule diff_less_Suc)

lemma star_diff_le_self [simp]: "!!m n. m - n ≤ (m::nat star)"
  by transfer (rule diff_le_self)

lemma star_less_imp_diff_less: "!!j k n. (j::nat star) < k ==> j - n < k"
  by transfer (rule less_imp_diff_less)

lemma star_diff_diff_left: "!!i j k. (i::nat star) - j - k = i - (j + k)"
  by transfer (rule diff_diff_left)

lemma hSuc_diff_diff [simp]: "!!m n k. (hSuc m - n) - hSuc k = m - n - k"
  by transfer (rule Suc_diff_diff)

lemma diff_hSuc_less [simp]: "!!n i. 0<n ==> n - hSuc i < n"
  by transfer (rule diff_Suc_less)

text {* This and the next few suggested by Florian Kammueller *}
lemma star_diff_commute: "!!i j k. (i::nat star) - j - k = i - k - j"
  by transfer (rule diff_commute)

lemma star_diff_add_assoc:
  "!!i j k. k ≤ (j::nat star) ==> (i + j) - k = i + (j - k)"
  by transfer (rule diff_add_assoc)

lemma star_diff_add_assoc2:
  "!!i j k. k ≤ (j::nat star) ==> (j + i) - k = (j - k) + i"
  by transfer (rule diff_add_assoc2)

lemma star_diff_add_inverse: "!!m n. (n + m) - n = (m::nat star)"
  by transfer (rule diff_add_inverse)

lemma star_diff_add_inverse2: "!!m n. (m + n) - n = (m::nat star)"
  by transfer (rule diff_add_inverse2)

lemma star_le_imp_diff_is_add:
  "!!i j k. i ≤ (j::nat star) ==> (j - i = k) = (j = k + i)"
  by transfer (rule le_imp_diff_is_add)

lemma star_diff_is_0_eq [simp]: "!!m n. ((m::nat star) - n = 0) = (m ≤ n)"
  by transfer (rule diff_is_0_eq)

lemma star_diff_is_0_eq' [simp]: "!!m n. m ≤ n ==> (m::nat star) - n = 0"
  by transfer (rule diff_is_0_eq')

lemma star_zero_less_diff [simp]: "!!m n. (0 < n - (m::nat star)) = (m < n)"
  by transfer (rule zero_less_diff)

lemma star_less_imp_add_positive:
  "!!i j. i < j  ==> ∃k::nat star. 0 < k & i + k = j"
  by transfer (rule less_imp_add_positive)

lemma star_diff_cancel: "!!k m n. (k + m) - (k + n) = m - (n::nat star)"
  by transfer (rule diff_cancel)

lemma star_diff_cancel2: "!!k m n. (m + k) - (n + k) = m - (n::nat star)"
  by transfer (rule diff_cancel2)

lemma star_diff_add_0: "!!m n. n - (n + m) = (0::nat star)"
  by transfer (rule diff_add_0)


text {* Difference distributes over multiplication *}

lemma star_diff_mult_distrib:
  "!!k m n. ((m::nat star) - n) * k = (m * k) - (n * k)"
  by transfer (rule diff_mult_distrib)

lemma star_diff_mult_distrib2:
  "!!k m n. k * ((m::nat star) - n) = (k * m) - (k * n)"
  by transfer (rule diff_mult_distrib2)

lemmas star_nat_distrib =
  left_distrib right_distrib star_diff_mult_distrib star_diff_mult_distrib2


subsection {* Monotonicity of Multiplication *}

lemma star_mult_le_mono1: "!!i j k. i ≤ (j::nat star) ==> i * k ≤ j * k"
  by transfer (rule mult_le_mono1)

lemma star_mult_le_mono2: "!!i j k. i ≤ (j::nat star) ==> k * i ≤ k * j"
  by transfer (rule mult_le_mono2)

text {* @{text "≤"} monotonicity, BOTH arguments *}
lemma star_mult_le_mono:
  "!!i j k l. i ≤ (j::nat star) ==> k ≤ l ==> i * k ≤ j * l"
  by transfer (rule mult_le_mono)

lemma star_mult_less_mono1:
  "!!i j k. (i::nat star) < j ==> 0 < k ==> i * k < j * k"
  by transfer (rule mult_less_mono1)

text{*Differs from the standard @{text zero_less_mult_iff} in that
      there are no negative numbers.*}
lemma star_nat_0_less_mult_iff [simp]:
  "!!m n. (0 < (m::nat star) * n) = (0 < m & 0 < n)"
  by transfer (rule nat_0_less_mult_iff)

lemma star_one_le_mult_iff [simp]: "!!m n. (hSuc 0 ≤ m * n) = (1 ≤ m & 1 ≤ n)"
  by transfer (rule one_le_mult_iff)

lemma star_mult_eq_1_iff [simp]: "!!m n. (m * n = hSuc 0) = (m = 1 & n = 1)"
  by transfer (rule mult_eq_1_iff)

lemma star_one_eq_mult_iff [simp]: "!!m n. (hSuc 0 = m * n) = (m = 1 & n = 1)"
  by transfer (rule one_eq_mult_iff)

lemma star_mult_less_cancel2 [simp]:
  "!!k m n. ((m::nat star) * k < n * k) = (0 < k & m < n)"
  by transfer (rule mult_less_cancel2)

lemma star_mult_less_cancel1 [simp]:
  "!!k m n. (k * (m::nat star) < k * n) = (0 < k & m < n)"
  by transfer (rule mult_less_cancel1)

lemma star_mult_le_cancel1 [simp]:
  "!!k m n. (k * (m::nat star) ≤ k * n) = (0 < k --> m ≤ n)"
  by transfer (rule mult_le_cancel1)

lemma star_mult_le_cancel2 [simp]:
  "!!k m n. ((m::nat star) * k ≤ n * k) = (0 < k --> m ≤ n)" 
  by transfer (rule mult_le_cancel2)

lemma star_mult_cancel2 [simp]:
  "!!k m n. (m * k = n * k) = (m = n | (k = (0::nat star)))"
  by transfer (rule mult_cancel2)

lemma star_mult_cancel1 [simp]:
  "!!k m n. (k * m = k * n) = (m = n | (k = (0::nat star)))"
  by transfer (rule mult_cancel1)

lemma hSuc_mult_less_cancel1: "!!k m n. (hSuc k * m < hSuc k * n) = (m < n)"
  by transfer (rule Suc_mult_less_cancel1)

lemma hSuc_mult_le_cancel1: "!!k m n. (hSuc k * m ≤ hSuc k * n) = (m ≤ n)"
  by transfer (rule Suc_mult_le_cancel1)

lemma hSuc_mult_cancel1: "!!k m n. (hSuc k * m = hSuc k * n) = (m = n)"
  by transfer (rule Suc_mult_cancel1)

text {* Lemma for @{text gcd} *}
lemma star_mult_eq_self_implies_10:
  "!!m n. (m::nat star) = m * n ==> n = 1 | m = 0"
  by transfer (rule mult_eq_self_implies_10)

end