isabelle: src/HOL/HOLCF/Discrete.thy@6d83841134f8 (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
19105 3aabd46340e0 use minimal imports huffman parents: 16213 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
25902 c00823ce7288 new-style class instantiation huffman parents: 25827 diff changeset	18	definition
40434 f775e6e0dc99 remove unnecessary stuff from Discrete.thy huffman parents: 40091 diff changeset	19	"(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)"
25902 c00823ce7288 new-style class instantiation huffman parents: 25827 diff changeset	20
40434 f775e6e0dc99 remove unnecessary stuff from Discrete.thy huffman parents: 40091 diff changeset	21	instance
61169 4de9ff3ea29a tuned proofs -- less legacy; wenzelm parents: 58880 diff changeset	22	by standard (simp add: below_discr_def)
15555 9d4dbd18ff2d converted to new-style theory huffman parents: 14981 diff changeset	23
40434 f775e6e0dc99 remove unnecessary stuff from Discrete.thy huffman parents: 40091 diff changeset	24	end
15555 9d4dbd18ff2d converted to new-style theory huffman parents: 14981 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
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19105 diff changeset	28	definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19105 diff changeset	29	undiscr :: "('a::type)discr => 'a" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19105 diff changeset	30	"undiscr x = (case x of Discr y => y)"
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	31
26025 ca6876116bb4 instances for class discrete_cpo huffman parents: 25921 diff changeset	32	lemma undiscr_Discr [simp]: "undiscr (Discr x) = x"
15590 17f4f5afcd5f added subsection headings, cleaned up some proofs huffman parents: 15578 diff changeset	33	by (simp add: undiscr_def)
15555 9d4dbd18ff2d converted to new-style theory huffman parents: 14981 diff changeset	34
26025 ca6876116bb4 instances for class discrete_cpo huffman parents: 25921 diff changeset	35	lemma Discr_undiscr [simp]: "Discr (undiscr y) = y"
ca6876116bb4 instances for class discrete_cpo huffman parents: 25921 diff changeset	36	by (induct y) simp
ca6876116bb4 instances for class discrete_cpo huffman parents: 25921 diff changeset	37
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: diff changeset	38	end

author	blanchet
	Wed, 07 Sep 2016 13:53:16 +0200
changeset 63816	6d83841134f8
parent 62175	8ffc4d0e652d
child 67312	0d25e02759b7
permissions	-rw-r--r--