# HG changeset patch # User huffman # Date 1332781457 -7200 # Node ID a3a64240cd98e1385833260f62afc5a3fc624643 # Parent 960f0a4404c71e04ba5119292ec175dd04846d4c code lemma for function 'nat' that doesn't go into an infinite loop (fixes problem with non-terminating HOL-Proofs-Lambda) diff -r 960f0a4404c7 -r a3a64240cd98 src/HOL/Library/Code_Integer.thy --- a/src/HOL/Library/Code_Integer.thy Mon Mar 26 19:03:27 2012 +0200 +++ b/src/HOL/Library/Code_Integer.thy Mon Mar 26 19:04:17 2012 +0200 @@ -16,11 +16,13 @@ "nat k = (if k \ 0 then 0 else let (l, j) = divmod_int k 2; - l' = 2 * nat l + n = nat l; + l' = n + n in if j = 0 then l' else Suc l')" proof - have "2 = nat 2" by simp show ?thesis + apply (subst nat_mult_2 [symmetric]) apply (auto simp add: Let_def divmod_int_mod_div not_le nat_div_distrib nat_mult_distrib mult_div_cancel mod_2_not_eq_zero_eq_one_int) apply (unfold `2 = nat 2`)