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

2 
Author: Franz Regensburger 
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
40327
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 sums *} 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

7 

15577  8 
theory Ssum 
31115  9 
imports Tr 
15577  10 
begin 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

11 

36452  12 
default_sort pcpo 
16083
fca38c55c8fa
added defaultsort declaration, moved cpair_less to Cprod.thy
huffman
parents:
16070
diff
changeset

13 

15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

15 

45695  16 
definition 
17 
"ssum = 

18 
{p :: tr \<times> ('a \<times> 'b). p = \<bottom> \<or> 

19 
(fst p = TT \<and> fst (snd p) \<noteq> \<bottom> \<and> snd (snd p) = \<bottom>) \<or> 

20 
(fst p = FF \<and> fst (snd p) = \<bottom> \<and> snd (snd p) \<noteq> \<bottom>)}" 

21 

22 
pcpodef (open) ('a, 'b) ssum (infixr "++" 10) = "ssum :: (tr \<times> 'a \<times> 'b) set" 

23 
unfolding ssum_def by simp_all 

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

24 

35525  25 
instance ssum :: ("{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:
40092
diff
changeset

26 
by (rule typedef_chfin [OF type_definition_ssum below_ssum_def]) 
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25756
diff
changeset

27 

35427  28 
type_notation (xsymbols) 
35547  29 
ssum ("(_ \<oplus>/ _)" [21, 20] 20) 
35427  30 
type_notation (HTML output) 
35547  31 
ssum ("(_ \<oplus>/ _)" [21, 20] 20) 
32 

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

33 

16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

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

35 

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

36 
definition 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19440
diff
changeset

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

38 
"sinl = (\<Lambda> a. Abs_ssum (seq\<cdot>a\<cdot>TT, a, \<bottom>))" 
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

39 

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

40 
definition 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19440
diff
changeset

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

42 
"sinr = (\<Lambda> b. Abs_ssum (seq\<cdot>b\<cdot>FF, \<bottom>, b))" 
25740
de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

43 

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

44 
lemma sinl_ssum: "(seq\<cdot>a\<cdot>TT, a, \<bottom>) \<in> ssum" 
a3e505b236e7
rename function 'strict' to 'seq', which is its name in Haskell
huffman
parents:
40502
diff
changeset

45 
by (simp add: ssum_def seq_conv_if) 
25740
de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

46 

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

47 
lemma sinr_ssum: "(seq\<cdot>b\<cdot>FF, \<bottom>, b) \<in> ssum" 
a3e505b236e7
rename function 'strict' to 'seq', which is its name in Haskell
huffman
parents:
40502
diff
changeset

48 
by (simp add: ssum_def seq_conv_if) 
25740
de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

49 

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

50 
lemma Rep_ssum_sinl: "Rep_ssum (sinl\<cdot>a) = (seq\<cdot>a\<cdot>TT, a, \<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:
40092
diff
changeset

51 
by (simp add: sinl_def cont_Abs_ssum Abs_ssum_inverse sinl_ssum) 
25740
de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

52 

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

53 
lemma Rep_ssum_sinr: "Rep_ssum (sinr\<cdot>b) = (seq\<cdot>b\<cdot>FF, \<bottom>, 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:
40092
diff
changeset

54 
by (simp add: sinr_def cont_Abs_ssum Abs_ssum_inverse sinr_ssum) 
40092
baf5953615da
do proofs using Rep_Sprod_simps, Rep_Ssum_simps; remove unused lemmas
huffman
parents:
40089
diff
changeset

55 

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

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

57 
Rep_ssum_inject [symmetric] below_ssum_def 
44066
d74182c93f04
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman
parents:
42151
diff
changeset

58 
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:
40092
diff
changeset

59 
Rep_ssum_strict Rep_ssum_sinl Rep_ssum_sinr 
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

60 

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

61 
subsection {* Properties of \emph{sinl} and \emph{sinr} *} 
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

62 

25740
de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

63 
text {* Ordering *} 
de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

64 

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

65 
lemma sinl_below [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)" 
40767
a3e505b236e7
rename function 'strict' to 'seq', which is its name in Haskell
huffman
parents:
40502
diff
changeset

66 
by (simp add: Rep_ssum_simps seq_conv_if) 
25740
de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

67 

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

68 
lemma sinr_below [simp]: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)" 
40767
a3e505b236e7
rename function 'strict' to 'seq', which is its name in Haskell
huffman
parents:
40502
diff
changeset

69 
by (simp add: Rep_ssum_simps seq_conv_if) 
25740
de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

70 

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

71 
lemma sinl_below_sinr [simp]: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)" 
40767
a3e505b236e7
rename function 'strict' to 'seq', which is its name in Haskell
huffman
parents:
40502
diff
changeset

72 
by (simp add: Rep_ssum_simps seq_conv_if) 
25740
de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

73 

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

74 
lemma sinr_below_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)" 
40767
a3e505b236e7
rename function 'strict' to 'seq', which is its name in Haskell
huffman
parents:
40502
diff
changeset

75 
by (simp add: Rep_ssum_simps seq_conv_if) 
25740
de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

76 

de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

77 
text {* Equality *} 
de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

78 

de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

79 
lemma sinl_eq [simp]: "(sinl\<cdot>x = sinl\<cdot>y) = (x = y)" 
de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

80 
by (simp add: po_eq_conv) 
de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

81 

de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

82 
lemma sinr_eq [simp]: "(sinr\<cdot>x = sinr\<cdot>y) = (x = y)" 
de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

83 
by (simp add: po_eq_conv) 
de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

84 

de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

85 
lemma sinl_eq_sinr [simp]: "(sinl\<cdot>x = sinr\<cdot>y) = (x = \<bottom> \<and> y = \<bottom>)" 
de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

86 
by (subst po_eq_conv, simp) 
de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

87 

de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

88 
lemma sinr_eq_sinl [simp]: "(sinr\<cdot>x = sinl\<cdot>y) = (x = \<bottom> \<and> y = \<bottom>)" 
de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

89 
by (subst po_eq_conv, simp) 
de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

90 

de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

91 
lemma sinl_inject: "sinl\<cdot>x = sinl\<cdot>y \<Longrightarrow> x = y" 
de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

92 
by (rule sinl_eq [THEN iffD1]) 
de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

93 

de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

94 
lemma sinr_inject: "sinr\<cdot>x = sinr\<cdot>y \<Longrightarrow> x = y" 
de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

95 
by (rule sinr_eq [THEN iffD1]) 
de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

96 

de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

97 
text {* Strictness *} 
17837  98 

16211
faa9691da2bc
changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents:
16083
diff
changeset

99 
lemma sinl_strict [simp]: "sinl\<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:
40092
diff
changeset

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

101 

16211
faa9691da2bc
changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents:
16083
diff
changeset

102 
lemma sinr_strict [simp]: "sinr\<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:
40092
diff
changeset

103 
by (simp add: Rep_ssum_simps) 
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

104 

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

105 
lemma sinl_bottom_iff [simp]: "(sinl\<cdot>x = \<bottom>) = (x = \<bottom>)" 
40080  106 
using sinl_eq [of "x" "\<bottom>"] by simp 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

107 

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

108 
lemma sinr_bottom_iff [simp]: "(sinr\<cdot>x = \<bottom>) = (x = \<bottom>)" 
40080  109 
using sinr_eq [of "x" "\<bottom>"] by simp 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

110 

40081  111 
lemma sinl_defined: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>" 
16752
270ec60cc9e8
added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents:
16742
diff
changeset

112 
by simp 
270ec60cc9e8
added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents:
16742
diff
changeset

113 

40081  114 
lemma sinr_defined: "x \<noteq> \<bottom> \<Longrightarrow> sinr\<cdot>x \<noteq> \<bottom>" 
16752
270ec60cc9e8
added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents:
16742
diff
changeset

115 
by simp 
270ec60cc9e8
added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents:
16742
diff
changeset

116 

25882
c58e380d9f7d
new compactness lemmas; removed duplicated flat_less_iff
huffman
parents:
25827
diff
changeset

117 
text {* Compactness *} 
c58e380d9f7d
new compactness lemmas; removed duplicated flat_less_iff
huffman
parents:
25827
diff
changeset

118 

c58e380d9f7d
new compactness lemmas; removed duplicated flat_less_iff
huffman
parents:
25827
diff
changeset

119 
lemma compact_sinl: "compact x \<Longrightarrow> compact (sinl\<cdot>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:
40092
diff
changeset

120 
by (rule compact_ssum, simp add: Rep_ssum_sinl) 
25882
c58e380d9f7d
new compactness lemmas; removed duplicated flat_less_iff
huffman
parents:
25827
diff
changeset

121 

c58e380d9f7d
new compactness lemmas; removed duplicated flat_less_iff
huffman
parents:
25827
diff
changeset

122 
lemma compact_sinr: "compact x \<Longrightarrow> compact (sinr\<cdot>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:
40092
diff
changeset

123 
by (rule compact_ssum, simp add: Rep_ssum_sinr) 
25882
c58e380d9f7d
new compactness lemmas; removed duplicated flat_less_iff
huffman
parents:
25827
diff
changeset

124 

c58e380d9f7d
new compactness lemmas; removed duplicated flat_less_iff
huffman
parents:
25827
diff
changeset

125 
lemma compact_sinlD: "compact (sinl\<cdot>x) \<Longrightarrow> compact x" 
c58e380d9f7d
new compactness lemmas; removed duplicated flat_less_iff
huffman
parents:
25827
diff
changeset

126 
unfolding compact_def 
40327  127 
by (drule adm_subst [OF cont_Rep_cfun2 [where f=sinl]], simp) 
25882
c58e380d9f7d
new compactness lemmas; removed duplicated flat_less_iff
huffman
parents:
25827
diff
changeset

128 

c58e380d9f7d
new compactness lemmas; removed duplicated flat_less_iff
huffman
parents:
25827
diff
changeset

129 
lemma compact_sinrD: "compact (sinr\<cdot>x) \<Longrightarrow> compact x" 
c58e380d9f7d
new compactness lemmas; removed duplicated flat_less_iff
huffman
parents:
25827
diff
changeset

130 
unfolding compact_def 
40327  131 
by (drule adm_subst [OF cont_Rep_cfun2 [where f=sinr]], simp) 
25882
c58e380d9f7d
new compactness lemmas; removed duplicated flat_less_iff
huffman
parents:
25827
diff
changeset

132 

c58e380d9f7d
new compactness lemmas; removed duplicated flat_less_iff
huffman
parents:
25827
diff
changeset

133 
lemma compact_sinl_iff [simp]: "compact (sinl\<cdot>x) = compact x" 
c58e380d9f7d
new compactness lemmas; removed duplicated flat_less_iff
huffman
parents:
25827
diff
changeset

134 
by (safe elim!: compact_sinl compact_sinlD) 
c58e380d9f7d
new compactness lemmas; removed duplicated flat_less_iff
huffman
parents:
25827
diff
changeset

135 

c58e380d9f7d
new compactness lemmas; removed duplicated flat_less_iff
huffman
parents:
25827
diff
changeset

136 
lemma compact_sinr_iff [simp]: "compact (sinr\<cdot>x) = compact x" 
c58e380d9f7d
new compactness lemmas; removed duplicated flat_less_iff
huffman
parents:
25827
diff
changeset

137 
by (safe elim!: compact_sinr compact_sinrD) 
c58e380d9f7d
new compactness lemmas; removed duplicated flat_less_iff
huffman
parents:
25827
diff
changeset

138 

16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

139 
subsection {* Case analysis *} 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

140 

35783  141 
lemma ssumE [case_names bottom sinl sinr, cases type: ssum]: 
40080  142 
obtains "p = \<bottom>" 
143 
 x where "p = sinl\<cdot>x" and "x \<noteq> \<bottom>" 

144 
 y where "p = sinr\<cdot>y" 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:
40092
diff
changeset

145 
using Rep_ssum [of p] by (auto simp add: ssum_def Rep_ssum_simps) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

146 

35783  147 
lemma ssum_induct [case_names bottom sinl sinr, induct type: ssum]: 
25756  148 
"\<lbrakk>P \<bottom>; 
149 
\<And>x. x \<noteq> \<bottom> \<Longrightarrow> P (sinl\<cdot>x); 

150 
\<And>y. y \<noteq> \<bottom> \<Longrightarrow> P (sinr\<cdot>y)\<rbrakk> \<Longrightarrow> P x" 

151 
by (cases x, simp_all) 

152 

35783  153 
lemma ssumE2 [case_names sinl sinr]: 
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

154 
"\<lbrakk>\<And>x. p = sinl\<cdot>x \<Longrightarrow> Q; \<And>y. p = sinr\<cdot>y \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" 
25740
de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

155 
by (cases p, simp only: sinl_strict [symmetric], simp, simp) 
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

156 

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

157 
lemma below_sinlD: "p \<sqsubseteq> sinl\<cdot>x \<Longrightarrow> \<exists>y. p = sinl\<cdot>y \<and> y \<sqsubseteq> x" 
25740
de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

158 
by (cases p, rule_tac x="\<bottom>" in exI, simp_all) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

159 

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

160 
lemma below_sinrD: "p \<sqsubseteq> sinr\<cdot>x \<Longrightarrow> \<exists>y. p = sinr\<cdot>y \<and> y \<sqsubseteq> x" 
25740
de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

161 
by (cases p, rule_tac x="\<bottom>" in exI, simp_all) 
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

162 

25740
de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

163 
subsection {* Case analysis combinator *} 
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

164 

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

165 
definition 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19440
diff
changeset

166 
sscase :: "('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a ++ 'b) \<rightarrow> 'c" where 
40322
707eb30e8a53
make syntax of continuous ifthenelse consistent with HOL ifthenelse
huffman
parents:
40321
diff
changeset

167 
"sscase = (\<Lambda> f g s. (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y) (Rep_ssum s))" 
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

168 

833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

169 
translations 
26046  170 
"case s of XCONST sinl\<cdot>x \<Rightarrow> t1  XCONST sinr\<cdot>y \<Rightarrow> t2" == "CONST sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s" 
46125
00cd193a48dc
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
45695
diff
changeset

171 
"case s of (XCONST sinl :: 'a)\<cdot>x \<Rightarrow> t1  XCONST sinr\<cdot>y \<Rightarrow> t2" => "CONST sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s" 
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

172 

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

173 
translations 
26046  174 
"\<Lambda>(XCONST sinl\<cdot>x). t" == "CONST sscase\<cdot>(\<Lambda> x. t)\<cdot>\<bottom>" 
175 
"\<Lambda>(XCONST sinr\<cdot>y). t" == "CONST sscase\<cdot>\<bottom>\<cdot>(\<Lambda> y. t)" 

16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

176 

25740
de65baf89106
changed type definition to make Iwhen and reasoning about chains unnecessary;
huffman
parents:
25131
diff
changeset

177 
lemma beta_sscase: 
40322
707eb30e8a53
make syntax of continuous ifthenelse consistent with HOL ifthenelse
huffman
parents:
40321
diff
changeset

178 
"sscase\<cdot>f\<cdot>g\<cdot>s = (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y) (Rep_ssum s)" 
40834
a1249aeff5b6
change cpodefgenerated cont_Rep rules to cont2cont format
huffman
parents:
40774
diff
changeset

179 
unfolding sscase_def by (simp add: cont_Rep_ssum) 
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

180 

833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

181 
lemma sscase1 [simp]: "sscase\<cdot>f\<cdot>g\<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:
40092
diff
changeset

182 
unfolding beta_sscase by (simp add: Rep_ssum_strict) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

183 

16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

184 
lemma sscase2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> sscase\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = f\<cdot>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:
40092
diff
changeset

185 
unfolding beta_sscase by (simp add: Rep_ssum_sinl) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

186 

16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

187 
lemma sscase3 [simp]: "y \<noteq> \<bottom> \<Longrightarrow> sscase\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>y) = g\<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:
40092
diff
changeset

188 
unfolding beta_sscase by (simp add: Rep_ssum_sinr) 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

189 

16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

190 
lemma sscase4 [simp]: "sscase\<cdot>sinl\<cdot>sinr\<cdot>z = z" 
25756  191 
by (cases z, simp_all) 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

192 

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

193 
subsection {* Strict sum preserves flatness *} 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25756
diff
changeset

194 

35525  195 
instance ssum :: (flat, flat) flat 
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25756
diff
changeset

196 
apply (intro_classes, clarify) 
31115  197 
apply (case_tac x, simp) 
198 
apply (case_tac y, simp_all add: flat_below_iff) 

199 
apply (case_tac y, simp_all add: flat_below_iff) 

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

200 
done 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25756
diff
changeset

201 

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

202 
end 