| author | wenzelm |
| Sat, 14 May 2011 16:27:47 +0200 | |
| changeset 42806 | 4b660cdab9b7 |
| parent 42151 | 4da4fc77664b |
| child 45788 | 9049b24959de |
| permissions | -rw-r--r-- |
| 42151 | 1 |
(* Title: HOL/HOLCF/ex/Letrec.thy |
| 35932 | 2 |
Author: Brian Huffman |
3 |
*) |
|
4 |
||
5 |
header {* Recursive let bindings *}
|
|
6 |
||
7 |
theory Letrec |
|
8 |
imports HOLCF |
|
9 |
begin |
|
10 |
||
| 36452 | 11 |
default_sort pcpo |
| 35932 | 12 |
|
13 |
definition |
|
14 |
CLetrec :: "('a \<rightarrow> 'a \<times> 'b) \<rightarrow> 'b" where
|
|
15 |
"CLetrec = (\<Lambda> F. snd (F\<cdot>(\<mu> x. fst (F\<cdot>x))))" |
|
16 |
||
|
41229
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
40774
diff
changeset
|
17 |
nonterminal recbinds and recbindt and recbind |
| 35932 | 18 |
|
19 |
syntax |
|
| 41479 | 20 |
"_recbind" :: "[logic, logic] \<Rightarrow> recbind" ("(2_ =/ _)" 10)
|
| 35932 | 21 |
"" :: "recbind \<Rightarrow> recbindt" ("_")
|
22 |
"_recbindt" :: "[recbind, recbindt] \<Rightarrow> recbindt" ("_,/ _")
|
|
23 |
"" :: "recbindt \<Rightarrow> recbinds" ("_")
|
|
24 |
"_recbinds" :: "[recbindt, recbinds] \<Rightarrow> recbinds" ("_;/ _")
|
|
| 41479 | 25 |
"_Letrec" :: "[recbinds, logic] \<Rightarrow> logic" ("(Letrec (_)/ in (_))" 10)
|
| 35932 | 26 |
|
27 |
translations |
|
28 |
(recbindt) "x = a, (y,ys) = (b,bs)" == (recbindt) "(x,y,ys) = (a,b,bs)" |
|
29 |
(recbindt) "x = a, y = b" == (recbindt) "(x,y) = (a,b)" |
|
30 |
||
31 |
translations |
|
32 |
"_Letrec (_recbinds b bs) e" == "_Letrec b (_Letrec bs e)" |
|
33 |
"Letrec xs = a in (e,es)" == "CONST CLetrec\<cdot>(\<Lambda> xs. (a,e,es))" |
|
34 |
"Letrec xs = a in e" == "CONST CLetrec\<cdot>(\<Lambda> xs. (a,e))" |
|
35 |
||
36 |
end |