isabelle: src/HOL/HOLCF/Discrete.thy@180f1b3508ed (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
15578 d364491ba718 add header huffman parents: 15555 diff changeset	5	header {* Discrete cpo types *}
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
58249 180f1b3508ed use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries blanchet parents: 42151 diff changeset	11	datatype_new 'a discr = Discr "'a :: type"
15555 9d4dbd18ff2d converted to new-style theory huffman parents: 14981 diff changeset	12
40434 f775e6e0dc99 remove unnecessary stuff from Discrete.thy huffman parents: 40091 diff changeset	13	subsection {* Discrete cpo class instance *}
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
f775e6e0dc99 remove unnecessary stuff from Discrete.thy huffman parents: 40091 diff changeset	22	by default (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
35900 aa5dfb03eb1e remove LaTeX hyperref warnings by avoiding antiquotations within section headings huffman parents: 31076 diff changeset	26	subsection {* \emph{undiscr} *}
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
	Tue, 09 Sep 2014 20:51:36 +0200
changeset 58249	180f1b3508ed
parent 42151	4da4fc77664b
child 58310	91ea607a34d8
permissions	-rw-r--r--