42 nrecBSuc: "c(n,nrec(n,b,c)) : A ==> nrec(Suc(n),b,c) = c(n,nrec(n,b,c)) : A" |
42 nrecBSuc: "c(n,nrec(n,b,c)) : A ==> nrec(Suc(n),b,c) = c(n,nrec(n,b,c)) : A" |
43 |
43 |
44 |
44 |
45 subsection {* Proofs about the natural numbers *} |
45 subsection {* Proofs about the natural numbers *} |
46 |
46 |
47 lemma Suc_n_not_n: "?p : ~ (Suc(k) = k)" |
47 schematic_lemma Suc_n_not_n: "?p : ~ (Suc(k) = k)" |
48 apply (rule_tac n = k in induct) |
48 apply (rule_tac n = k in induct) |
49 apply (rule notI) |
49 apply (rule notI) |
50 apply (erule Suc_neq_0) |
50 apply (erule Suc_neq_0) |
51 apply (rule notI) |
51 apply (rule notI) |
52 apply (erule notE) |
52 apply (erule notE) |
53 apply (erule Suc_inject) |
53 apply (erule Suc_inject) |
54 done |
54 done |
55 |
55 |
56 lemma "?p : (k+m)+n = k+(m+n)" |
56 schematic_lemma "?p : (k+m)+n = k+(m+n)" |
57 apply (rule induct) |
57 apply (rule induct) |
58 back |
58 back |
59 back |
59 back |
60 back |
60 back |
61 back |
61 back |
62 back |
62 back |
63 back |
63 back |
64 oops |
64 oops |
65 |
65 |
66 lemma add_0 [simp]: "?p : 0+n = n" |
66 schematic_lemma add_0 [simp]: "?p : 0+n = n" |
67 apply (unfold add_def) |
67 apply (unfold add_def) |
68 apply (rule rec_0) |
68 apply (rule rec_0) |
69 done |
69 done |
70 |
70 |
71 lemma add_Suc [simp]: "?p : Suc(m)+n = Suc(m+n)" |
71 schematic_lemma add_Suc [simp]: "?p : Suc(m)+n = Suc(m+n)" |
72 apply (unfold add_def) |
72 apply (unfold add_def) |
73 apply (rule rec_Suc) |
73 apply (rule rec_Suc) |
74 done |
74 done |
75 |
75 |
76 |
76 |
77 lemma Suc_cong: "p : x = y \<Longrightarrow> ?p : Suc(x) = Suc(y)" |
77 schematic_lemma Suc_cong: "p : x = y \<Longrightarrow> ?p : Suc(x) = Suc(y)" |
78 apply (erule subst) |
78 apply (erule subst) |
79 apply (rule refl) |
79 apply (rule refl) |
80 done |
80 done |
81 |
81 |
82 lemma Plus_cong: "[| p : a = x; q: b = y |] ==> ?p : a + b = x + y" |
82 schematic_lemma Plus_cong: "[| p : a = x; q: b = y |] ==> ?p : a + b = x + y" |
83 apply (erule subst, erule subst, rule refl) |
83 apply (erule subst, erule subst, rule refl) |
84 done |
84 done |
85 |
85 |
86 lemmas nat_congs = Suc_cong Plus_cong |
86 lemmas nat_congs = Suc_cong Plus_cong |
87 |
87 |
88 ML {* |
88 ML {* |
89 val add_ss = FOLP_ss addcongs @{thms nat_congs} addrews [@{thm add_0}, @{thm add_Suc}] |
89 val add_ss = FOLP_ss addcongs @{thms nat_congs} addrews [@{thm add_0}, @{thm add_Suc}] |
90 *} |
90 *} |
91 |
91 |
92 lemma add_assoc: "?p : (k+m)+n = k+(m+n)" |
92 schematic_lemma add_assoc: "?p : (k+m)+n = k+(m+n)" |
93 apply (rule_tac n = k in induct) |
93 apply (rule_tac n = k in induct) |
94 apply (tactic {* SIMP_TAC add_ss 1 *}) |
94 apply (tactic {* SIMP_TAC add_ss 1 *}) |
95 apply (tactic {* ASM_SIMP_TAC add_ss 1 *}) |
95 apply (tactic {* ASM_SIMP_TAC add_ss 1 *}) |
96 done |
96 done |
97 |
97 |
98 lemma add_0_right: "?p : m+0 = m" |
98 schematic_lemma add_0_right: "?p : m+0 = m" |
99 apply (rule_tac n = m in induct) |
99 apply (rule_tac n = m in induct) |
100 apply (tactic {* SIMP_TAC add_ss 1 *}) |
100 apply (tactic {* SIMP_TAC add_ss 1 *}) |
101 apply (tactic {* ASM_SIMP_TAC add_ss 1 *}) |
101 apply (tactic {* ASM_SIMP_TAC add_ss 1 *}) |
102 done |
102 done |
103 |
103 |
104 lemma add_Suc_right: "?p : m+Suc(n) = Suc(m+n)" |
104 schematic_lemma add_Suc_right: "?p : m+Suc(n) = Suc(m+n)" |
105 apply (rule_tac n = m in induct) |
105 apply (rule_tac n = m in induct) |
106 apply (tactic {* ALLGOALS (ASM_SIMP_TAC add_ss) *}) |
106 apply (tactic {* ALLGOALS (ASM_SIMP_TAC add_ss) *}) |
107 done |
107 done |
108 |
108 |
109 (*mk_typed_congs appears not to work with FOLP's version of subst*) |
109 (*mk_typed_congs appears not to work with FOLP's version of subst*) |