equal
deleted
inserted
replaced
475 lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z" |
475 lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z" |
476 by (cases z rule: eq_Abs_Integ) |
476 by (cases z rule: eq_Abs_Integ) |
477 (simp add: nat le of_int Zero_int_def of_nat_diff) |
477 (simp add: nat le of_int Zero_int_def of_nat_diff) |
478 |
478 |
479 end |
479 end |
|
480 |
|
481 text {* For termination proofs: *} |
|
482 lemma measure_function_int[measure_function]: "is_measure (nat o abs)" .. |
480 |
483 |
481 |
484 |
482 subsection{*Lemmas about the Function @{term of_nat} and Orderings*} |
485 subsection{*Lemmas about the Function @{term of_nat} and Orderings*} |
483 |
486 |
484 lemma negative_zless_0: "- (of_nat (Suc n)) < (0 \<Colon> int)" |
487 lemma negative_zless_0: "- (of_nat (Suc n)) < (0 \<Colon> int)" |