isabelle: src/HOL/HOLCF/Cprod.thy@62f794b9e9cc (annotated)

42151 4da4fc77664b tuned headers; wenzelm parents: 40774 diff changeset	1	(* Title: HOL/HOLCF/Cprod.thy
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	2	Author: Franz Regensburger
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	3	*)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	4
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	5	header {* The cpo of cartesian products *}
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	6
15577 e16da3068ad6 fix headers huffman parents: 15576 diff changeset	7	theory Cprod
40502 8e92772bc0e8 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF huffman parents: 40002 diff changeset	8	imports Cfun
15577 e16da3068ad6 fix headers huffman parents: 15576 diff changeset	9	begin
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	10
36452 d37c6eed8117 renamed command 'defaultsort' to 'default_sort'; wenzelm parents: 35926 diff changeset	11	default_sort cpo
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	12
35900 aa5dfb03eb1e remove LaTeX hyperref warnings by avoiding antiquotations within section headings huffman parents: 33399 diff changeset	13	subsection {* Continuous case function for unit type *}
16008 861a255cf1e7 pcpo instance for type unit huffman parents: 15609 diff changeset	14
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 18289 diff changeset	15	definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 18289 diff changeset	16	unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 18289 diff changeset	17	"unit_when = (\<Lambda> a _. a)"
16008 861a255cf1e7 pcpo instance for type unit huffman parents: 15609 diff changeset	18
18289 56ddf617d6e8 add constant unit_when huffman parents: 18078 diff changeset	19	translations
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 18289 diff changeset	20	"\<Lambda>(). t" == "CONST unit_when\<cdot>t"
18289 56ddf617d6e8 add constant unit_when huffman parents: 18078 diff changeset	21
56ddf617d6e8 add constant unit_when huffman parents: 18078 diff changeset	22	lemma unit_when [simp]: "unit_when\<cdot>a\<cdot>u = a"
56ddf617d6e8 add constant unit_when huffman parents: 18078 diff changeset	23	by (simp add: unit_when_def)
56ddf617d6e8 add constant unit_when huffman parents: 18078 diff changeset	24
35926 e6aec5d665f0 completely remove constants cpair, cfst, csnd huffman parents: 35922 diff changeset	25	subsection {* Continuous version of split function *}
17834 28414668b43d added xsymbols syntax for pairs; cleaned up huffman parents: 17816 diff changeset	26
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 18289 diff changeset	27	definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 18289 diff changeset	28	csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a * 'b) \<rightarrow> 'c" where
35922 bfa52a972745 define csplit using fst, snd huffman parents: 35900 diff changeset	29	"csplit = (\<Lambda> f p. f\<cdot>(fst p)\<cdot>(snd p))"
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	30
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	31	translations
35926 e6aec5d665f0 completely remove constants cpair, cfst, csnd huffman parents: 35922 diff changeset	32	"\<Lambda>(CONST Pair x y). t" == "CONST csplit\<cdot>(\<Lambda> x y. t)"
17816 9942c5ed866a new syntax translations for continuous lambda abstraction huffman parents: 16916 diff changeset	33
45786 3f07a7a91180 reinstate old functions cfst and csnd as abbreviations huffman parents: 42151 diff changeset	34	abbreviation
3f07a7a91180 reinstate old functions cfst and csnd as abbreviations huffman parents: 42151 diff changeset	35	cfst :: "'a \<times> 'b \<rightarrow> 'a" where
3f07a7a91180 reinstate old functions cfst and csnd as abbreviations huffman parents: 42151 diff changeset	36	"cfst \<equiv> Abs_cfun fst"
3f07a7a91180 reinstate old functions cfst and csnd as abbreviations huffman parents: 42151 diff changeset	37
3f07a7a91180 reinstate old functions cfst and csnd as abbreviations huffman parents: 42151 diff changeset	38	abbreviation
3f07a7a91180 reinstate old functions cfst and csnd as abbreviations huffman parents: 42151 diff changeset	39	csnd :: "'a \<times> 'b \<rightarrow> 'b" where
3f07a7a91180 reinstate old functions cfst and csnd as abbreviations huffman parents: 42151 diff changeset	40	"csnd \<equiv> Abs_cfun snd"
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	41
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	42	subsection {* Convert all lemmas to the continuous versions *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	43
18077 f1f4f951ec8d make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1 huffman parents: 17837 diff changeset	44	lemma csplit1 [simp]: "csplit\<cdot>f\<cdot>\<bottom> = f\<cdot>\<bottom>\<cdot>\<bottom>"
f1f4f951ec8d make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1 huffman parents: 17837 diff changeset	45	by (simp add: csplit_def)
f1f4f951ec8d make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1 huffman parents: 17837 diff changeset	46
33399 768b2bb9e66a add (LAM (x, y). t) syntax and lemma csplit_Pair huffman parents: 31113 diff changeset	47	lemma csplit_Pair [simp]: "csplit\<cdot>f\<cdot>(x, y) = f\<cdot>x\<cdot>y"
35922 bfa52a972745 define csplit using fst, snd huffman parents: 35900 diff changeset	48	by (simp add: csplit_def)
33399 768b2bb9e66a add (LAM (x, y). t) syntax and lemma csplit_Pair huffman parents: 31113 diff changeset	49
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	50	end

author	blanchet
	Thu, 06 Jun 2013 11:41:19 +0200
changeset 52313	62f794b9e9cc
parent 45786	3f07a7a91180
child 58880	0baae4311a9f
permissions	-rw-r--r--