equal
deleted
inserted
replaced
56 "nz 0 = 0" |
56 "nz 0 = 0" |
57 "nz (Suc x) = nz (nz x)" |
57 "nz (Suc x) = nz (nz x)" |
58 by pat_completeness auto |
58 by pat_completeness auto |
59 |
59 |
60 lemma nz_is_zero: (* A lemma we need to prove termination *) |
60 lemma nz_is_zero: (* A lemma we need to prove termination *) |
61 assumes trm: "x \<in> nz.dom" |
61 assumes trm: "x \<in> nz_dom" |
62 shows "nz x = 0" |
62 shows "nz x = 0" |
63 using trm |
63 using trm |
64 by induct auto |
64 by induct auto |
65 |
65 |
66 termination nz |
66 termination nz |