equal
deleted
inserted
replaced
35 intros |
35 intros |
36 Rec_zero: "NAT zero succ \<Longrightarrow> (zero, e) \<in> REC zero succ e r" |
36 Rec_zero: "NAT zero succ \<Longrightarrow> (zero, e) \<in> REC zero succ e r" |
37 Rec_succ: "NAT zero succ \<Longrightarrow> (m, n) \<in> REC zero succ e r \<Longrightarrow> |
37 Rec_succ: "NAT zero succ \<Longrightarrow> (m, n) \<in> REC zero succ e r \<Longrightarrow> |
38 (succ m, r m n) \<in> REC zero succ e r" |
38 (succ m, r m n) \<in> REC zero succ e r" |
39 |
39 |
40 abbreviation (in NAT) (output) |
40 abbreviation (in NAT) |
41 "Rec = REC zero succ" |
41 "Rec == REC zero succ" |
42 |
42 |
43 lemma (in NAT) Rec_functional: |
43 lemma (in NAT) Rec_functional: |
44 fixes x :: 'n |
44 fixes x :: 'n |
45 shows "\<exists>!y::'a. (x, y) \<in> Rec e r" (is "\<exists>!y::'a. _ \<in> ?Rec") |
45 shows "\<exists>!y::'a. (x, y) \<in> Rec e r" (is "\<exists>!y::'a. _ \<in> ?Rec") |
46 proof (induct x) |
46 proof (induct x) |