equal
deleted
inserted
replaced
29 (We simulate a localized version of the inductive packages using |
29 (We simulate a localized version of the inductive packages using |
30 explicit premises + parameters, and an abbreviation.) *} |
30 explicit premises + parameters, and an abbreviation.) *} |
31 |
31 |
32 consts |
32 consts |
33 REC :: "'n \<Rightarrow> ('n \<Rightarrow> 'n) \<Rightarrow> 'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('n * 'a) set" |
33 REC :: "'n \<Rightarrow> ('n \<Rightarrow> 'n) \<Rightarrow> 'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('n * 'a) set" |
34 inductive "REC zero succ e r" |
34 inductive "REC zer succ e r" |
35 intros |
35 intros |
36 Rec_zero: "NAT zero succ \<Longrightarrow> (zero, e) \<in> REC zero succ e r" |
36 Rec_zero: "NAT zer succ \<Longrightarrow> (zer, e) \<in> REC zer succ e r" |
37 Rec_succ: "NAT zero succ \<Longrightarrow> (m, n) \<in> REC zero succ e r \<Longrightarrow> |
37 Rec_succ: "NAT zer succ \<Longrightarrow> (m, n) \<in> REC zer succ e r \<Longrightarrow> |
38 (succ m, r m n) \<in> REC zero succ e r" |
38 (succ m, r m n) \<in> REC zer succ e r" |
39 |
39 |
40 abbreviation (in NAT) |
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: |