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

42151 4da4fc77664b tuned headers; wenzelm parents: 41479 diff changeset	1	(* Title: HOL/HOLCF/ex/Letrec.thy
35932 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
62175 8ffc4d0e652d isabelle update_cartouches -c -t; wenzelm parents: 58880 diff changeset	5	section \<open>Recursive let bindings\<close>
35932 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
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	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 86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	13	"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	14
41229 d797baa3d57c replaced command 'nonterminals' by slightly modernized version 'nonterminal'; wenzelm parents: 40774 diff changeset	15	nonterminal recbinds and recbindt and recbind
35932 86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	16
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	17	syntax
81095 49c04500c5f9 more inner syntax markup: HOLCF; wenzelm parents: 80914 diff changeset	18	"_recbind" :: "[logic, logic] \<Rightarrow> recbind" (\<open>(\<open>indent=2 notation=\<open>mixfix Letrec binding\<close>\<close>_ =/ _)\<close> 10)
80914 d97fdabd9e2b standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing; wenzelm parents: 80768 diff changeset	19	"" :: "recbind \<Rightarrow> recbindt" (\<open>_\<close>)
d97fdabd9e2b standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing; wenzelm parents: 80768 diff changeset	20	"_recbindt" :: "[recbind, recbindt] \<Rightarrow> recbindt" (\<open>_,/ _\<close>)
d97fdabd9e2b standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing; wenzelm parents: 80768 diff changeset	21	"" :: "recbindt \<Rightarrow> recbinds" (\<open>_\<close>)
d97fdabd9e2b standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing; wenzelm parents: 80768 diff changeset	22	"_recbinds" :: "[recbindt, recbinds] \<Rightarrow> recbinds" (\<open>_;/ _\<close>)
81095 49c04500c5f9 more inner syntax markup: HOLCF; wenzelm parents: 80914 diff changeset	23	"_Letrec" :: "[recbinds, logic] \<Rightarrow> logic" (\<open>(\<open>notation=\<open>mixfix Letrec expression\<close>\<close>Letrec (_)/ in (_))\<close> 10)
80768 c7723cc15de8 more markup for syntax consts; wenzelm parents: 62175 diff changeset	24
81182 fc5066122e68 more inner-syntax markup; wenzelm parents: 81095 diff changeset	25	syntax_consts
fc5066122e68 more inner-syntax markup; wenzelm parents: 81095 diff changeset	26	"_Letrec" \<rightleftharpoons> CLetrec
fc5066122e68 more inner-syntax markup; wenzelm parents: 81095 diff changeset	27
35932 86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	28	translations
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	29	(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	30	(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	31
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	32	translations
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	33	"_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	34	"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	35	"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	36
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: diff changeset	37	end

author	wenzelm
	Tue, 22 Jul 2025 12:02:53 +0200
changeset 82894	a8e47bd31965
parent 81182	fc5066122e68
permissions	-rw-r--r--