equal
deleted
inserted
replaced
33 P (\<Squnion>i. iterate i F \<bottom>)" |
33 P (\<Squnion>i. iterate i F \<bottom>)" |
34 |
34 |
35 subsection {* Binder syntax for @{term fix} *} |
35 subsection {* Binder syntax for @{term fix} *} |
36 |
36 |
37 syntax |
37 syntax |
38 "@FIX" :: "('a => 'a) => 'a" (binder "FIX " 10) |
38 "_FIX" :: "[pttrn, 'a] => 'a" ("(3FIX _./ _)" [0, 10] 10) |
39 "@FIXP" :: "[patterns, 'a] => 'a" ("(3FIX <_>./ _)" [0, 10] 10) |
|
40 |
39 |
41 syntax (xsymbols) |
40 syntax (xsymbols) |
42 "FIX " :: "[idt, 'a] => 'a" ("(3\<mu>_./ _)" [0, 10] 10) |
41 "_FIX" :: "[pttrn, 'a] => 'a" ("(3\<mu>_./ _)" [0, 10] 10) |
43 "@FIXP" :: "[patterns, 'a] => 'a" ("(3\<mu>()<_>./ _)" [0, 10] 10) |
|
44 |
42 |
45 translations |
43 translations |
46 "FIX x. LAM y. t" == "fix\<cdot>(LAM x y. t)" |
44 "FIX x. t" == "fix$(LAM x. t)" |
47 "FIX x. t" == "fix\<cdot>(LAM x. t)" |
|
48 "FIX <xs>. t" == "fix\<cdot>(LAM <xs>. t)" |
|
49 |
45 |
50 subsection {* Properties of @{term iterate} and @{term fix} *} |
46 subsection {* Properties of @{term iterate} and @{term fix} *} |
51 |
47 |
52 text {* derive inductive properties of iterate from primitive recursion *} |
48 text {* derive inductive properties of iterate from primitive recursion *} |
53 |
49 |