author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45786  3f07a7a91180 
child 58880  0baae4311a9f 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/Cprod.thy 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

2 
Author: Franz Regensburger 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

3 
*) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

4 

efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

5 
header {* The cpo of cartesian products *} 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

6 

15577  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  9 
begin 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

10 

36452  11 
default_sort cpo 
15576
efb95d0d01f7
converted to newstyle 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  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  18 

18289  19 
translations 
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18289
diff
changeset

20 
"\<Lambda>(). t" == "CONST unit_when\<cdot>t" 
18289  21 

22 
lemma unit_when [simp]: "unit_when\<cdot>a\<cdot>u = a" 

23 
by (simp add: unit_when_def) 

24 

35926  25 
subsection {* Continuous version of split function *} 
17834  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  29 
"csplit = (\<Lambda> f p. f\<cdot>(fst p)\<cdot>(snd p))" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

30 

efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

31 
translations 
35926  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 newstyle 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 newstyle 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  47 
lemma csplit_Pair [simp]: "csplit\<cdot>f\<cdot>(x, y) = f\<cdot>x\<cdot>y" 
35922  48 
by (simp add: csplit_def) 
33399  49 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

50 
end 