| author | wenzelm |
| Sat, 03 May 2014 20:31:29 +0200 | |
| changeset 56842 | b6e266574b26 |
| 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 |