equal
deleted
inserted
replaced
37 "Z=Arg+n = (%Z s. Z = s<Arg>+n)" |
37 "Z=Arg+n = (%Z s. Z = s<Arg>+n)" |
38 |
38 |
39 definition |
39 definition |
40 Res_ok :: "nat assn" where |
40 Res_ok :: "nat assn" where |
41 "Res_ok = (%Z s. even Z = (s<Res> = 0))" |
41 "Res_ok = (%Z s. even Z = (s<Res> = 0))" |
42 |
|
43 |
|
44 subsection "even" |
|
45 |
|
46 lemma not_even_1 [simp]: "even (Suc 0) = False" |
|
47 apply (unfold even_def) |
|
48 apply simp |
|
49 done |
|
50 |
|
51 lemma even_step [simp]: "even (Suc (Suc n)) = even n" |
|
52 apply (unfold even_def) |
|
53 apply (subgoal_tac "Suc (Suc n) = n+2") |
|
54 prefer 2 |
|
55 apply simp |
|
56 apply (erule ssubst) |
|
57 apply (rule dvd_reduce) |
|
58 done |
|
59 |
42 |
60 |
43 |
61 subsection "Arg, Res" |
44 subsection "Arg, Res" |
62 |
45 |
63 declare Arg_neq_Res [simp] Arg_neq_Res [THEN not_sym, simp] |
46 declare Arg_neq_Res [simp] Arg_neq_Res [THEN not_sym, simp] |