isabelle: src/HOL/HOLCF/ex/Letrec.thy@6d736d983d5c (annotated)

35932 86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	1	(* Title: HOLCF/ex/Letrec.thy
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	2	Author: Brian Huffman
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	3	*)
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	4
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	5	header {* Recursive let bindings *}
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	6
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	7	theory Letrec
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	8	imports HOLCF
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	9	begin
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	10
36452 d37c6eed8117 renamed command 'defaultsort' to 'default_sort'; wenzelm parents: 35932 diff changeset	11	default_sort pcpo
35932 86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	12
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	13	definition
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	14	CLetrec :: "('a \<rightarrow> 'a \<times> 'b) \<rightarrow> 'b" where
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	15	"CLetrec = (\<Lambda> F. snd (F\<cdot>(\<mu> x. fst (F\<cdot>x))))"
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	16
41229 d797baa3d57c replaced command 'nonterminals' by slightly modernized version 'nonterminal'; wenzelm parents: 40774 diff changeset	17	nonterminal recbinds and recbindt and recbind
35932 86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	18
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	19	syntax
41479 655f583840d0 use proper syntactic types for 'syntax' commands huffman parents: 41229 diff changeset	20	"_recbind" :: "[logic, logic] \<Rightarrow> recbind" ("(2_ =/ _)" 10)
35932 86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	21	"" :: "recbind \<Rightarrow> recbindt" ("_")
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	22	"_recbindt" :: "[recbind, recbindt] \<Rightarrow> recbindt" ("_,/ _")
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	23	"" :: "recbindt \<Rightarrow> recbinds" ("_")
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	24	"_recbinds" :: "[recbindt, recbinds] \<Rightarrow> recbinds" ("_;/ _")
41479 655f583840d0 use proper syntactic types for 'syntax' commands huffman parents: 41229 diff changeset	25	"_Letrec" :: "[recbinds, logic] \<Rightarrow> logic" ("(Letrec (_)/ in (_))" 10)
35932 86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	26
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	27	translations
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	28	(recbindt) "x = a, (y,ys) = (b,bs)" == (recbindt) "(x,y,ys) = (a,b,bs)"
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	29	(recbindt) "x = a, y = b" == (recbindt) "(x,y) = (a,b)"
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	30
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	31	translations
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	32	"_Letrec (_recbinds b bs) e" == "_Letrec b (_Letrec bs e)"
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	33	"Letrec xs = a in (e,es)" == "CONST CLetrec\<cdot>(\<Lambda> xs. (a,e,es))"
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	34	"Letrec xs = a in e" == "CONST CLetrec\<cdot>(\<Lambda> xs. (a,e))"
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	35
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	36	end

author	wenzelm
	Sun, 30 Jan 2011 13:02:18 +0100
changeset 41648	6d736d983d5c
parent 41479	655f583840d0
child 42151	4da4fc77664b
permissions	-rw-r--r--