equal
deleted
inserted
replaced
20 l' = n + n |
20 l' = n + n |
21 in if j = 0 then l' else Suc l')" |
21 in if j = 0 then l' else Suc l')" |
22 proof - |
22 proof - |
23 have "2 = nat 2" by simp |
23 have "2 = nat 2" by simp |
24 show ?thesis |
24 show ?thesis |
25 apply (subst nat_mult_2 [symmetric]) |
25 apply (subst mult_2 [symmetric]) |
26 apply (auto simp add: Let_def divmod_int_mod_div not_le |
26 apply (auto simp add: Let_def divmod_int_mod_div not_le |
27 nat_div_distrib nat_mult_distrib mult_div_cancel mod_2_not_eq_zero_eq_one_int) |
27 nat_div_distrib nat_mult_distrib mult_div_cancel mod_2_not_eq_zero_eq_one_int) |
28 apply (unfold `2 = nat 2`) |
28 apply (unfold `2 = nat 2`) |
29 apply (subst nat_mod_distrib [symmetric]) |
29 apply (subst nat_mod_distrib [symmetric]) |
30 apply simp_all |
30 apply simp_all |