author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45695  b108b3d7c49e 
child 49759  ecf1d5d87e5e 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/Sprod.thy 
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
40436
diff
changeset

2 
Author: Franz Regensburger 
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
40436
diff
changeset

3 
Author: Brian Huffman 
15576
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 

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

6 
header {* The type of strict products *} 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

7 

15577  8 
theory Sprod 
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
40436
diff
changeset

9 
imports Cfun 
15577  10 
begin 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

11 

36452  12 
default_sort pcpo 
16082  13 

15591
50c3384ca6c4
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

14 
subsection {* Definition of strict product type *} 
50c3384ca6c4
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

15 

45695  16 
definition "sprod = {p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}" 
17 

18 
pcpodef (open) ('a, 'b) sprod (infixr "**" 20) = "sprod :: ('a \<times> 'b) set" 

19 
unfolding sprod_def by simp_all 

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

20 

35525  21 
instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin 
40098
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset

22 
by (rule typedef_chfin [OF type_definition_sprod below_sprod_def]) 
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25757
diff
changeset

23 

35427  24 
type_notation (xsymbols) 
35547  25 
sprod ("(_ \<otimes>/ _)" [21,20] 20) 
35427  26 
type_notation (HTML output) 
35547  27 
sprod ("(_ \<otimes>/ _)" [21,20] 20) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

28 

16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset

29 
subsection {* Definitions of constants *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

30 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

31 
definition 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

32 
sfst :: "('a ** 'b) \<rightarrow> 'a" where 
40098
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset

33 
"sfst = (\<Lambda> p. fst (Rep_sprod p))" 
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

34 

4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

35 
definition 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

36 
ssnd :: "('a ** 'b) \<rightarrow> 'b" where 
40098
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset

37 
"ssnd = (\<Lambda> p. snd (Rep_sprod p))" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

38 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

39 
definition 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

40 
spair :: "'a \<rightarrow> 'b \<rightarrow> ('a ** 'b)" where 
40767
a3e505b236e7
rename function 'strict' to 'seq', which is its name in Haskell
huffman
parents:
40502
diff
changeset

41 
"spair = (\<Lambda> a b. Abs_sprod (seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b))" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

42 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

43 
definition 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

44 
ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c" where 
40767
a3e505b236e7
rename function 'strict' to 'seq', which is its name in Haskell
huffman
parents:
40502
diff
changeset

45 
"ssplit = (\<Lambda> f p. seq\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))" 
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

46 

4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

47 
syntax 
41479  48 
"_stuple" :: "[logic, args] \<Rightarrow> logic" ("(1'(:_,/ _:'))") 
49 

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

50 
translations 
18078
20e5a6440790
change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
huffman
parents:
17837
diff
changeset

51 
"(:x, y, z:)" == "(:x, (:y, z:):)" 
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18078
diff
changeset

52 
"(:x, y:)" == "CONST spair\<cdot>x\<cdot>y" 
18078
20e5a6440790
change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
huffman
parents:
17837
diff
changeset

53 

20e5a6440790
change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
huffman
parents:
17837
diff
changeset

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

55 
"\<Lambda>(CONST spair\<cdot>x\<cdot>y). t" == "CONST ssplit\<cdot>(\<Lambda> x y. t)" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

56 

16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset

57 
subsection {* Case analysis *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

58 

40767
a3e505b236e7
rename function 'strict' to 'seq', which is its name in Haskell
huffman
parents:
40502
diff
changeset

59 
lemma spair_sprod: "(seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b) \<in> sprod" 
a3e505b236e7
rename function 'strict' to 'seq', which is its name in Haskell
huffman
parents:
40502
diff
changeset

60 
by (simp add: sprod_def seq_conv_if) 
40083  61 

40767
a3e505b236e7
rename function 'strict' to 'seq', which is its name in Haskell
huffman
parents:
40502
diff
changeset

62 
lemma Rep_sprod_spair: "Rep_sprod (:a, b:) = (seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b)" 
40098
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset

63 
by (simp add: spair_def cont_Abs_sprod Abs_sprod_inverse spair_sprod) 
40080  64 

40098
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset

65 
lemmas Rep_sprod_simps = 
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset

66 
Rep_sprod_inject [symmetric] below_sprod_def 
44066
d74182c93f04
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman
parents:
42151
diff
changeset

67 
prod_eq_iff below_prod_def 
40098
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset

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

69 

35783  70 
lemma sprodE [case_names bottom spair, cases type: sprod]: 
40080  71 
obtains "p = \<bottom>"  x y where "p = (:x, y:)" and "x \<noteq> \<bottom>" and "y \<noteq> \<bottom>" 
40098
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset

72 
using Rep_sprod [of p] by (auto simp add: sprod_def Rep_sprod_simps) 
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset

73 

35783  74 
lemma sprod_induct [case_names bottom spair, induct type: sprod]: 
25757
5957e3d72fec
declare sprodE as cases rule; new induction rule sprod_induct
huffman
parents:
25135
diff
changeset

75 
"\<lbrakk>P \<bottom>; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> P (:x, y:)\<rbrakk> \<Longrightarrow> P x" 
5957e3d72fec
declare sprodE as cases rule; new induction rule sprod_induct
huffman
parents:
25135
diff
changeset

76 
by (cases x, simp_all) 
5957e3d72fec
declare sprodE as cases rule; new induction rule sprod_induct
huffman
parents:
25135
diff
changeset

77 

35900
aa5dfb03eb1e
remove LaTeX hyperref warnings by avoiding antiquotations within section headings
huffman
parents:
35783
diff
changeset

78 
subsection {* Properties of \emph{spair} *} 
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset

79 

16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset

80 
lemma spair_strict1 [simp]: "(:\<bottom>, y:) = \<bottom>" 
40098
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset

81 
by (simp add: Rep_sprod_simps) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

82 

16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset

83 
lemma spair_strict2 [simp]: "(:x, \<bottom>:) = \<bottom>" 
40098
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset

84 
by (simp add: Rep_sprod_simps) 
25914  85 

40321
d065b195ec89
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents:
40098
diff
changeset

86 
lemma spair_bottom_iff [simp]: "((:x, y:) = \<bottom>) = (x = \<bottom> \<or> y = \<bottom>)" 
40767
a3e505b236e7
rename function 'strict' to 'seq', which is its name in Haskell
huffman
parents:
40502
diff
changeset

87 
by (simp add: Rep_sprod_simps seq_conv_if) 
25914  88 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

89 
lemma spair_below_iff: 
25914  90 
"((:a, b:) \<sqsubseteq> (:c, d:)) = (a = \<bottom> \<or> b = \<bottom> \<or> (a \<sqsubseteq> c \<and> b \<sqsubseteq> d))" 
40767
a3e505b236e7
rename function 'strict' to 'seq', which is its name in Haskell
huffman
parents:
40502
diff
changeset

91 
by (simp add: Rep_sprod_simps seq_conv_if) 
25914  92 

93 
lemma spair_eq_iff: 

94 
"((:a, b:) = (:c, d:)) = 

95 
(a = c \<and> b = d \<or> (a = \<bottom> \<or> b = \<bottom>) \<and> (c = \<bottom> \<or> d = \<bottom>))" 

40767
a3e505b236e7
rename function 'strict' to 'seq', which is its name in Haskell
huffman
parents:
40502
diff
changeset

96 
by (simp add: Rep_sprod_simps seq_conv_if) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

97 

16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset

98 
lemma spair_strict: "x = \<bottom> \<or> y = \<bottom> \<Longrightarrow> (:x, y:) = \<bottom>" 
25914  99 
by simp 
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset

100 

16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset

101 
lemma spair_strict_rev: "(:x, y:) \<noteq> \<bottom> \<Longrightarrow> x \<noteq> \<bottom> \<and> y \<noteq> \<bottom>" 
25914  102 
by simp 
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset

103 

25914  104 
lemma spair_defined: "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<noteq> \<bottom>" 
105 
by simp 

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

106 

16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset

107 
lemma spair_defined_rev: "(:x, y:) = \<bottom> \<Longrightarrow> x = \<bottom> \<or> y = \<bottom>" 
25914  108 
by simp 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

109 

40095  110 
lemma spair_below: 
111 
"\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<sqsubseteq> (:a, b:) = (x \<sqsubseteq> a \<and> y \<sqsubseteq> b)" 

112 
by (simp add: spair_below_iff) 

113 

16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset

114 
lemma spair_eq: 
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset

115 
"\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> ((:x, y:) = (:a, b:)) = (x = a \<and> y = b)" 
25914  116 
by (simp add: spair_eq_iff) 
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset

117 

16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset

118 
lemma spair_inject: 
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset

119 
"\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>; (:x, y:) = (:a, b:)\<rbrakk> \<Longrightarrow> x = a \<and> y = b" 
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset

120 
by (rule spair_eq [THEN iffD1]) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

121 

41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
40774
diff
changeset

122 
lemma inst_sprod_pcpo2: "\<bottom> = (:\<bottom>, \<bottom>:)" 
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset

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

124 

33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
32960
diff
changeset

125 
lemma sprodE2: "(\<And>x y. p = (:x, y:) \<Longrightarrow> Q) \<Longrightarrow> Q" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
32960
diff
changeset

126 
by (cases p, simp only: inst_sprod_pcpo2, simp) 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
32960
diff
changeset

127 

35900
aa5dfb03eb1e
remove LaTeX hyperref warnings by avoiding antiquotations within section headings
huffman
parents:
35783
diff
changeset

128 
subsection {* Properties of \emph{sfst} and \emph{ssnd} *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

129 

16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset

130 
lemma sfst_strict [simp]: "sfst\<cdot>\<bottom> = \<bottom>" 
40098
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset

131 
by (simp add: sfst_def cont_Rep_sprod Rep_sprod_strict) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

132 

16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset

133 
lemma ssnd_strict [simp]: "ssnd\<cdot>\<bottom> = \<bottom>" 
40098
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset

134 
by (simp add: ssnd_def cont_Rep_sprod Rep_sprod_strict) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

135 

16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset

136 
lemma sfst_spair [simp]: "y \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>(:x, y:) = x" 
40098
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset

137 
by (simp add: sfst_def cont_Rep_sprod Rep_sprod_spair) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

138 

16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset

139 
lemma ssnd_spair [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>(:x, y:) = y" 
40098
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset

140 
by (simp add: ssnd_def cont_Rep_sprod Rep_sprod_spair) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

141 

40321
d065b195ec89
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents:
40098
diff
changeset

142 
lemma sfst_bottom_iff [simp]: "(sfst\<cdot>p = \<bottom>) = (p = \<bottom>)" 
25757
5957e3d72fec
declare sprodE as cases rule; new induction rule sprod_induct
huffman
parents:
25135
diff
changeset

143 
by (cases p, simp_all) 
16777
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16751
diff
changeset

144 

40321
d065b195ec89
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents:
40098
diff
changeset

145 
lemma ssnd_bottom_iff [simp]: "(ssnd\<cdot>p = \<bottom>) = (p = \<bottom>)" 
25757
5957e3d72fec
declare sprodE as cases rule; new induction rule sprod_induct
huffman
parents:
25135
diff
changeset

146 
by (cases p, simp_all) 
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset

147 

16777
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16751
diff
changeset

148 
lemma sfst_defined: "p \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>p \<noteq> \<bottom>" 
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16751
diff
changeset

149 
by simp 
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16751
diff
changeset

150 

555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16751
diff
changeset

151 
lemma ssnd_defined: "p \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>p \<noteq> \<bottom>" 
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16751
diff
changeset

152 
by simp 
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16751
diff
changeset

153 

40094
0295606b6a36
rename lemma surjective_pairing_Sprod2 to spair_sfst_ssnd
huffman
parents:
40093
diff
changeset

154 
lemma spair_sfst_ssnd: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p" 
25757
5957e3d72fec
declare sprodE as cases rule; new induction rule sprod_induct
huffman
parents:
25135
diff
changeset

155 
by (cases p, simp_all) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

156 

40436  157 
lemma below_sprod: "(x \<sqsubseteq> y) = (sfst\<cdot>x \<sqsubseteq> sfst\<cdot>y \<and> ssnd\<cdot>x \<sqsubseteq> ssnd\<cdot>y)" 
40098
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset

158 
by (simp add: Rep_sprod_simps sfst_def ssnd_def cont_Rep_sprod) 
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset

159 

16751  160 
lemma eq_sprod: "(x = y) = (sfst\<cdot>x = sfst\<cdot>y \<and> ssnd\<cdot>x = ssnd\<cdot>y)" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

161 
by (auto simp add: po_eq_conv below_sprod) 
16751  162 

40436  163 
lemma sfst_below_iff: "sfst\<cdot>x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (:y, ssnd\<cdot>x:)" 
25881  164 
apply (cases "x = \<bottom>", simp, cases "y = \<bottom>", simp) 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

165 
apply (simp add: below_sprod) 
25881  166 
done 
167 

40436  168 
lemma ssnd_below_iff: "ssnd\<cdot>x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (:sfst\<cdot>x, y:)" 
25881  169 
apply (cases "x = \<bottom>", simp, cases "y = \<bottom>", simp) 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

170 
apply (simp add: below_sprod) 
25881  171 
done 
172 

173 
subsection {* Compactness *} 

174 

175 
lemma compact_sfst: "compact x \<Longrightarrow> compact (sfst\<cdot>x)" 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

176 
by (rule compactI, simp add: sfst_below_iff) 
25881  177 

178 
lemma compact_ssnd: "compact x \<Longrightarrow> compact (ssnd\<cdot>x)" 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

179 
by (rule compactI, simp add: ssnd_below_iff) 
25881  180 

181 
lemma compact_spair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (:x, y:)" 

40767
a3e505b236e7
rename function 'strict' to 'seq', which is its name in Haskell
huffman
parents:
40502
diff
changeset

182 
by (rule compact_sprod, simp add: Rep_sprod_spair seq_conv_if) 
25881  183 

184 
lemma compact_spair_iff: 

185 
"compact (:x, y:) = (x = \<bottom> \<or> y = \<bottom> \<or> (compact x \<and> compact y))" 

186 
apply (safe elim!: compact_spair) 

187 
apply (drule compact_sfst, simp) 

188 
apply (drule compact_ssnd, simp) 

189 
apply simp 

190 
apply simp 

191 
done 

192 

35900
aa5dfb03eb1e
remove LaTeX hyperref warnings by avoiding antiquotations within section headings
huffman
parents:
35783
diff
changeset

193 
subsection {* Properties of \emph{ssplit} *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

194 

16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset

195 
lemma ssplit1 [simp]: "ssplit\<cdot>f\<cdot>\<bottom> = \<bottom>" 
15591
50c3384ca6c4
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

196 
by (simp add: ssplit_def) 
50c3384ca6c4
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

197 

16920  198 
lemma ssplit2 [simp]: "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> ssplit\<cdot>f\<cdot>(:x, y:) = f\<cdot>x\<cdot>y" 
15591
50c3384ca6c4
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

199 
by (simp add: ssplit_def) 
50c3384ca6c4
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

200 

16553  201 
lemma ssplit3 [simp]: "ssplit\<cdot>spair\<cdot>z = z" 
25757
5957e3d72fec
declare sprodE as cases rule; new induction rule sprod_induct
huffman
parents:
25135
diff
changeset

202 
by (cases z, simp_all) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

203 

25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25757
diff
changeset

204 
subsection {* Strict product preserves flatness *} 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25757
diff
changeset

205 

35525  206 
instance sprod :: (flat, flat) flat 
27310  207 
proof 
208 
fix x y :: "'a \<otimes> 'b" 

209 
assume "x \<sqsubseteq> y" thus "x = \<bottom> \<or> x = y" 

210 
apply (induct x, simp) 

211 
apply (induct y, simp) 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

212 
apply (simp add: spair_below_iff flat_below_iff) 
27310  213 
done 
214 
qed 

25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25757
diff
changeset

215 

26962
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
25914
diff
changeset

216 
end 