isabelle: src/HOL/HOLCF/Discrete.thy@f1c6e778e412 (annotated)

42151 4da4fc77664b tuned headers; wenzelm parents: 40774 diff changeset	1	(* Title: HOL/HOLCF/Discrete.thy
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	2	Author: Tobias Nipkow
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	3	*)
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	4
62175 8ffc4d0e652d isabelle update_cartouches -c -t; wenzelm parents: 61169 diff changeset	5	section \<open>Discrete cpo types\<close>
15578 d364491ba718 add header huffman parents: 15555 diff changeset	6
15555 9d4dbd18ff2d converted to new-style theory huffman parents: 14981 diff changeset	7	theory Discrete
67312 0d25e02759b7 misc tuning and modernization; wenzelm parents: 62175 diff changeset	8	imports Cont
15555 9d4dbd18ff2d converted to new-style theory huffman parents: 14981 diff changeset	9	begin
9d4dbd18ff2d converted to new-style theory huffman parents: 14981 diff changeset	10
58310 91ea607a34d8 updated news blanchet parents: 58249 diff changeset	11	datatype 'a discr = Discr "'a :: type"
15555 9d4dbd18ff2d converted to new-style theory huffman parents: 14981 diff changeset	12
62175 8ffc4d0e652d isabelle update_cartouches -c -t; wenzelm parents: 61169 diff changeset	13	subsection \<open>Discrete cpo class instance\<close>
15590 17f4f5afcd5f added subsection headings, cleaned up some proofs huffman parents: 15578 diff changeset	14
40434 f775e6e0dc99 remove unnecessary stuff from Discrete.thy huffman parents: 40091 diff changeset	15	instantiation discr :: (type) discrete_cpo
25902 c00823ce7288 new-style class instantiation huffman parents: 25827 diff changeset	16	begin
15555 9d4dbd18ff2d converted to new-style theory huffman parents: 14981 diff changeset	17
67399 eab6ce8368fa ran isabelle update_op on all sources nipkow parents: 67312 diff changeset	18	definition "((\<sqsubseteq>) :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (=)"
25902 c00823ce7288 new-style class instantiation huffman parents: 25827 diff changeset	19
40434 f775e6e0dc99 remove unnecessary stuff from Discrete.thy huffman parents: 40091 diff changeset	20	instance
61169 4de9ff3ea29a tuned proofs -- less legacy; wenzelm parents: 58880 diff changeset	21	by standard (simp add: below_discr_def)
15555 9d4dbd18ff2d converted to new-style theory huffman parents: 14981 diff changeset	22
40434 f775e6e0dc99 remove unnecessary stuff from Discrete.thy huffman parents: 40091 diff changeset	23	end
15555 9d4dbd18ff2d converted to new-style theory huffman parents: 14981 diff changeset	24
67312 0d25e02759b7 misc tuning and modernization; wenzelm parents: 62175 diff changeset	25
62175 8ffc4d0e652d isabelle update_cartouches -c -t; wenzelm parents: 61169 diff changeset	26	subsection \<open>\emph{undiscr}\<close>
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	27
67312 0d25e02759b7 misc tuning and modernization; wenzelm parents: 62175 diff changeset	28	definition undiscr :: "('a::type)discr \<Rightarrow> 'a"
0d25e02759b7 misc tuning and modernization; wenzelm parents: 62175 diff changeset	29	where "undiscr x = (case x of Discr y \<Rightarrow> y)"
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	30
26025 ca6876116bb4 instances for class discrete_cpo huffman parents: 25921 diff changeset	31	lemma undiscr_Discr [simp]: "undiscr (Discr x) = x"
67312 0d25e02759b7 misc tuning and modernization; wenzelm parents: 62175 diff changeset	32	by (simp add: undiscr_def)
15555 9d4dbd18ff2d converted to new-style theory huffman parents: 14981 diff changeset	33
26025 ca6876116bb4 instances for class discrete_cpo huffman parents: 25921 diff changeset	34	lemma Discr_undiscr [simp]: "Discr (undiscr y) = y"
67312 0d25e02759b7 misc tuning and modernization; wenzelm parents: 62175 diff changeset	35	by (induct y) simp
26025 ca6876116bb4 instances for class discrete_cpo huffman parents: 25921 diff changeset	36
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	37	end

author	wenzelm
	Sat, 12 Mar 2022 23:21:28 +0100
changeset 75273	f1c6e778e412
parent 67399	eab6ce8368fa
permissions	-rw-r--r--