author | wenzelm |
Sat, 07 Apr 2012 16:41:59 +0200 | |
changeset 47389 | e8552cba702d |
parent 45788 | 9049b24959de |
child 58880 | 0baae4311a9f |
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 |
||
11 |
definition |
|
45788
9049b24959de
HOLCF/ex/Letrec.thy: keep class 'domain' as default sort
huffman
parents:
42151
diff
changeset
|
12 |
CLetrec :: "('a::pcpo \<rightarrow> 'a \<times> 'b::pcpo) \<rightarrow> 'b" where |
35932 | 13 |
"CLetrec = (\<Lambda> F. snd (F\<cdot>(\<mu> x. fst (F\<cdot>x))))" |
14 |
||
41229
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
40774
diff
changeset
|
15 |
nonterminal recbinds and recbindt and recbind |
35932 | 16 |
|
17 |
syntax |
|
41479 | 18 |
"_recbind" :: "[logic, logic] \<Rightarrow> recbind" ("(2_ =/ _)" 10) |
35932 | 19 |
"" :: "recbind \<Rightarrow> recbindt" ("_") |
20 |
"_recbindt" :: "[recbind, recbindt] \<Rightarrow> recbindt" ("_,/ _") |
|
21 |
"" :: "recbindt \<Rightarrow> recbinds" ("_") |
|
22 |
"_recbinds" :: "[recbindt, recbinds] \<Rightarrow> recbinds" ("_;/ _") |
|
41479 | 23 |
"_Letrec" :: "[recbinds, logic] \<Rightarrow> logic" ("(Letrec (_)/ in (_))" 10) |
35932 | 24 |
|
25 |
translations |
|
26 |
(recbindt) "x = a, (y,ys) = (b,bs)" == (recbindt) "(x,y,ys) = (a,b,bs)" |
|
27 |
(recbindt) "x = a, y = b" == (recbindt) "(x,y) = (a,b)" |
|
28 |
||
29 |
translations |
|
30 |
"_Letrec (_recbinds b bs) e" == "_Letrec b (_Letrec bs e)" |
|
31 |
"Letrec xs = a in (e,es)" == "CONST CLetrec\<cdot>(\<Lambda> xs. (a,e,es))" |
|
32 |
"Letrec xs = a in e" == "CONST CLetrec\<cdot>(\<Lambda> xs. (a,e))" |
|
33 |
||
34 |
end |