15 intros |
15 intros |
16 LeafI: "Leaf(a) \<in> sexp" |
16 LeafI: "Leaf(a) \<in> sexp" |
17 NumbI: "Numb(i) \<in> sexp" |
17 NumbI: "Numb(i) \<in> sexp" |
18 SconsI: "[| M \<in> sexp; N \<in> sexp |] ==> Scons M N \<in> sexp" |
18 SconsI: "[| M \<in> sexp; N \<in> sexp |] ==> Scons M N \<in> sexp" |
19 |
19 |
20 constdefs |
20 definition |
21 |
21 |
22 sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, |
22 sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, |
23 'a item] => 'b" |
23 'a item] => 'b" |
24 "sexp_case c d e M == THE z. (EX x. M=Leaf(x) & z=c(x)) |
24 "sexp_case c d e M = (THE z. (EX x. M=Leaf(x) & z=c(x)) |
25 | (EX k. M=Numb(k) & z=d(k)) |
25 | (EX k. M=Numb(k) & z=d(k)) |
26 | (EX N1 N2. M = Scons N1 N2 & z=e N1 N2)" |
26 | (EX N1 N2. M = Scons N1 N2 & z=e N1 N2))" |
27 |
27 |
28 pred_sexp :: "('a item * 'a item)set" |
28 pred_sexp :: "('a item * 'a item)set" |
29 "pred_sexp == \<Union>M \<in> sexp. \<Union>N \<in> sexp. {(M, Scons M N), (N, Scons M N)}" |
29 "pred_sexp = (\<Union>M \<in> sexp. \<Union>N \<in> sexp. {(M, Scons M N), (N, Scons M N)})" |
30 |
30 |
31 sexp_rec :: "['a item, 'a=>'b, nat=>'b, |
31 sexp_rec :: "['a item, 'a=>'b, nat=>'b, |
32 ['a item, 'a item, 'b, 'b]=>'b] => 'b" |
32 ['a item, 'a item, 'b, 'b]=>'b] => 'b" |
33 "sexp_rec M c d e == wfrec pred_sexp |
33 "sexp_rec M c d e = wfrec pred_sexp |
34 (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2))) M" |
34 (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2))) M" |
35 |
35 |
36 |
36 |
37 (** sexp_case **) |
37 (** sexp_case **) |
38 |
38 |