author  huffman 
Thu, 07 Jul 2005 18:38:00 +0200  
changeset 16742  d1641dba61e5 
parent 16699  24b494ff8f0f 
child 16752  270ec60cc9e8 
permissions  rwrr 
15600  1 
(* Title: HOLCF/Ssum.thy 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

3 
Author: Franz Regensburger and Brian Huffman 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

4 

16070
4a83dd540b88
removed LICENCE note  everything is subject to Isabelle licence as
wenzelm
parents:
16060
diff
changeset

5 
Strict sum with typedef. 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

7 

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

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

9 

15577  10 
theory Ssum 
16699  11 
imports Cprod 
15577  12 
begin 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

13 

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

14 
defaultsort pcpo 
fca38c55c8fa
added defaultsort declaration, moved cpair_less to Cprod.thy
huffman
parents:
16070
diff
changeset

15 

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

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

17 

16699  18 
pcpodef (Ssum) ('a, 'b) "++" (infixr 10) = 
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

19 
"{p::'a \<times> 'b. cfst\<cdot>p = \<bottom> \<or> csnd\<cdot>p = \<bottom>}" 
16699  20 
by simp 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

21 

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

22 
syntax (xsymbols) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

23 
"++" :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

24 
syntax (HTML output) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

25 
"++" :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

26 

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

27 
lemma UU_Abs_Ssum: "\<bottom> = Abs_Ssum <\<bottom>, \<bottom>>" 
16211
faa9691da2bc
changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents:
16083
diff
changeset

28 
by (simp add: Abs_Ssum_strict inst_cprod_pcpo2 [symmetric]) 
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

29 

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

30 

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

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

32 

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

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

34 
sinl :: "'a \<rightarrow> ('a ++ 'b)" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

35 
"sinl \<equiv> \<Lambda> a. Abs_Ssum <a, \<bottom>>" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

36 

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

37 
sinr :: "'b \<rightarrow> ('a ++ 'b)" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

38 
"sinr \<equiv> \<Lambda> b. Abs_Ssum <\<bottom>, b>" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

39 

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

40 
subsection {* Properties of @{term sinl} and @{term sinr} *} 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

41 

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

42 
lemma sinl_Abs_Ssum: "sinl\<cdot>a = Abs_Ssum <a, \<bottom>>" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

43 
by (unfold sinl_def, simp add: cont_Abs_Ssum Ssum_def) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

44 

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

45 
lemma sinr_Abs_Ssum: "sinr\<cdot>b = Abs_Ssum <\<bottom>, b>" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

46 
by (unfold sinr_def, simp add: cont_Abs_Ssum Ssum_def) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

47 

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

48 
lemma Rep_Ssum_sinl: "Rep_Ssum (sinl\<cdot>a) = <a, \<bottom>>" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

49 
by (unfold sinl_def, simp add: cont_Abs_Ssum Abs_Ssum_inverse Ssum_def) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

50 

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

51 
lemma Rep_Ssum_sinr: "Rep_Ssum (sinr\<cdot>b) = <\<bottom>, b>" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

52 
by (unfold sinr_def, simp add: cont_Abs_Ssum Abs_Ssum_inverse Ssum_def) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

53 

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

54 
lemma sinl_strict [simp]: "sinl\<cdot>\<bottom> = \<bottom>" 
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

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

56 

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

57 
lemma sinr_strict [simp]: "sinr\<cdot>\<bottom> = \<bottom>" 
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

58 
by (simp add: sinr_Abs_Ssum UU_Abs_Ssum) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

59 

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

60 
lemma noteq_sinlsinr: "sinl\<cdot>a = sinr\<cdot>b \<Longrightarrow> a = \<bottom> \<and> b = \<bottom>" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

61 
apply (simp add: sinl_Abs_Ssum sinr_Abs_Ssum) 
15606
95617b30514b
simplified some definitions, many proofs are much shorter
huffman
parents:
15600
diff
changeset

62 
apply (simp add: Abs_Ssum_inject Ssum_def) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

64 

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

65 
lemma sinl_inject: "sinl\<cdot>x = sinl\<cdot>y \<Longrightarrow> x = y" 
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

66 
by (simp add: sinl_Abs_Ssum Abs_Ssum_inject Ssum_def) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

67 

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

68 
lemma sinr_inject: "sinr\<cdot>x = sinr\<cdot>y \<Longrightarrow> x = y" 
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

69 
by (simp add: sinr_Abs_Ssum Abs_Ssum_inject Ssum_def) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

70 

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

71 
lemma sinl_eq: "(sinl\<cdot>x = sinl\<cdot>y) = (x = y)" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

72 
by (simp add: sinl_Abs_Ssum Abs_Ssum_inject Ssum_def) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

73 

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

74 
lemma sinr_eq: "(sinr\<cdot>x = sinr\<cdot>y) = (x = y)" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

75 
by (simp add: sinr_Abs_Ssum Abs_Ssum_inject Ssum_def) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

76 

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

77 
lemma sinl_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

78 
apply (erule contrapos_nn) 
16211
faa9691da2bc
changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents:
16083
diff
changeset

79 
apply (rule sinl_inject) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

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

82 

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

83 
lemma sinr_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> sinr\<cdot>x \<noteq> \<bottom>" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

84 
apply (erule contrapos_nn) 
16211
faa9691da2bc
changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents:
16083
diff
changeset

85 
apply (rule sinr_inject) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

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

88 

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

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

90 

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

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

92 
"z = \<bottom> \<or> (\<exists>a. z = sinl\<cdot>a \<and> a \<noteq> \<bottom>) \<or> (\<exists>b. z = sinr\<cdot>b \<and> b \<noteq> \<bottom>)" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

93 
apply (simp add: sinl_Abs_Ssum sinr_Abs_Ssum UU_Abs_Ssum) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

94 
apply (rule_tac x=z in Abs_Ssum_cases) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

95 
apply (rule_tac p=y in cprodE) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

96 
apply (auto simp add: Ssum_def) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

98 

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

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

100 
"\<lbrakk>p = \<bottom> \<Longrightarrow> Q; 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

101 
\<And>x. \<lbrakk>p = sinl\<cdot>x; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q; 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

102 
\<And>y. \<lbrakk>p = sinr\<cdot>y; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

103 
by (cut_tac z=p in Exh_Ssum1, auto) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

104 

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

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

106 
"\<lbrakk>\<And>x. p = sinl\<cdot>x \<Longrightarrow> Q; \<And>y. p = sinr\<cdot>y \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

107 
apply (rule_tac p=p in ssumE) 
16211
faa9691da2bc
changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents:
16083
diff
changeset

108 
apply (simp only: sinl_strict [symmetric]) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

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

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

112 

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

113 
subsection {* Ordering properties of @{term sinl} and @{term sinr} *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

114 

16316
17db5df51a35
renamed theorems less_ssum4a,b,c,d to more meaningful names
huffman
parents:
16211
diff
changeset

115 
lemma sinl_less: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)" 
16699  116 
by (simp add: less_Ssum_def Rep_Ssum_sinl cpair_less) 
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

117 

16316
17db5df51a35
renamed theorems less_ssum4a,b,c,d to more meaningful names
huffman
parents:
16211
diff
changeset

118 
lemma sinr_less: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)" 
16699  119 
by (simp add: less_Ssum_def Rep_Ssum_sinr cpair_less) 
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

120 

16316
17db5df51a35
renamed theorems less_ssum4a,b,c,d to more meaningful names
huffman
parents:
16211
diff
changeset

121 
lemma sinl_less_sinr: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)" 
16699  122 
by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

123 

16316
17db5df51a35
renamed theorems less_ssum4a,b,c,d to more meaningful names
huffman
parents:
16211
diff
changeset

124 
lemma sinr_less_sinl: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)" 
16699  125 
by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff) 
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

126 

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

127 
subsection {* Chains of strict sums *} 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

128 

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

129 
lemma less_sinlD: "p \<sqsubseteq> sinl\<cdot>x \<Longrightarrow> \<exists>y. p = sinl\<cdot>y \<and> y \<sqsubseteq> x" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

130 
apply (rule_tac p=p in ssumE) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

131 
apply (rule_tac x="\<bottom>" in exI, simp) 
16316
17db5df51a35
renamed theorems less_ssum4a,b,c,d to more meaningful names
huffman
parents:
16211
diff
changeset

132 
apply (simp add: sinl_less sinl_eq) 
17db5df51a35
renamed theorems less_ssum4a,b,c,d to more meaningful names
huffman
parents:
16211
diff
changeset

133 
apply (simp add: sinr_less_sinl) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

135 

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

136 
lemma less_sinrD: "p \<sqsubseteq> sinr\<cdot>x \<Longrightarrow> \<exists>y. p = sinr\<cdot>y \<and> y \<sqsubseteq> x" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

137 
apply (rule_tac p=p in ssumE) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

138 
apply (rule_tac x="\<bottom>" in exI, simp) 
16316
17db5df51a35
renamed theorems less_ssum4a,b,c,d to more meaningful names
huffman
parents:
16211
diff
changeset

139 
apply (simp add: sinl_less_sinr) 
17db5df51a35
renamed theorems less_ssum4a,b,c,d to more meaningful names
huffman
parents:
16211
diff
changeset

140 
apply (simp add: sinr_less sinr_eq) 
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

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

142 

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

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

144 
"chain Y \<Longrightarrow> (\<exists>A. chain A \<and> Y = (\<lambda>i. sinl\<cdot>(A i))) \<or> 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

145 
(\<exists>B. chain B \<and> Y = (\<lambda>i. sinr\<cdot>(B i)))" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

146 
apply (rule_tac p="lub (range Y)" in ssumE2) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

147 
apply (rule disjI1) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

148 
apply (rule_tac x="\<lambda>i. cfst\<cdot>(Rep_Ssum (Y i))" in exI) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

149 
apply (rule conjI) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

150 
apply (rule chain_monofun) 
16742  151 
apply (erule cont_Rep_Ssum [THEN ch2ch_cont]) 
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

152 
apply (rule ext, drule_tac x=i in is_ub_thelub, simp) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

153 
apply (drule less_sinlD, clarify) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

154 
apply (simp add: sinl_eq Rep_Ssum_sinl) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

155 
apply (rule disjI2) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

156 
apply (rule_tac x="\<lambda>i. csnd\<cdot>(Rep_Ssum (Y i))" in exI) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

157 
apply (rule conjI) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

158 
apply (rule chain_monofun) 
16742  159 
apply (erule cont_Rep_Ssum [THEN ch2ch_cont]) 
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

160 
apply (rule ext, drule_tac x=i in is_ub_thelub, simp) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

161 
apply (drule less_sinrD, clarify) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

162 
apply (simp add: sinr_eq Rep_Ssum_sinr) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

164 

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

165 
subsection {* Definitions of constants *} 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

166 

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

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

168 
Iwhen :: "['a \<rightarrow> 'c, 'b \<rightarrow> 'c, 'a ++ 'b] \<Rightarrow> 'c" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

169 
"Iwhen \<equiv> \<lambda>f g s. 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

170 
if cfst\<cdot>(Rep_Ssum s) \<noteq> \<bottom> then f\<cdot>(cfst\<cdot>(Rep_Ssum s)) else 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

171 
if csnd\<cdot>(Rep_Ssum s) \<noteq> \<bottom> then g\<cdot>(csnd\<cdot>(Rep_Ssum s)) else \<bottom>" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

172 

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

173 
text {* rewrites for @{term Iwhen} *} 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

174 

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

175 
lemma Iwhen1 [simp]: "Iwhen f g \<bottom> = \<bottom>" 
16211
faa9691da2bc
changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents:
16083
diff
changeset

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

177 

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

178 
lemma Iwhen2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> Iwhen f g (sinl\<cdot>x) = f\<cdot>x" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

179 
by (simp add: Iwhen_def Rep_Ssum_sinl) 
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 Iwhen3 [simp]: "y \<noteq> \<bottom> \<Longrightarrow> Iwhen f g (sinr\<cdot>y) = g\<cdot>y" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

182 
by (simp add: Iwhen_def Rep_Ssum_sinr) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

183 

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

184 
lemma Iwhen4: "Iwhen f g (sinl\<cdot>x) = strictify\<cdot>f\<cdot>x" 
16211
faa9691da2bc
changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents:
16083
diff
changeset

185 
by (simp add: strictify_conv_if) 
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 Iwhen5: "Iwhen f g (sinr\<cdot>y) = strictify\<cdot>g\<cdot>y" 
16211
faa9691da2bc
changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents:
16083
diff
changeset

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

189 

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

190 
subsection {* Continuity of @{term Iwhen} *} 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

191 

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

192 
text {* @{term Iwhen} is continuous in all arguments *} 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

193 

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

194 
lemma cont_Iwhen1: "cont (\<lambda>f. Iwhen f g s)" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

195 
by (rule_tac p=s in ssumE, simp_all) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

196 

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

197 
lemma cont_Iwhen2: "cont (\<lambda>g. Iwhen f g s)" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

198 
by (rule_tac p=s in ssumE, simp_all) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

199 

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

200 
lemma cont_Iwhen3: "cont (\<lambda>s. Iwhen f g s)" 
16211
faa9691da2bc
changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents:
16083
diff
changeset

201 
apply (rule contI) 
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

202 
apply (drule ssum_chain_lemma, safe) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

203 
apply (simp add: contlub_cfun_arg [symmetric]) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

204 
apply (simp add: Iwhen4) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

205 
apply (simp add: contlub_cfun_arg) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

206 
apply (simp add: thelubE chain_monofun) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

207 
apply (simp add: contlub_cfun_arg [symmetric]) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

208 
apply (simp add: Iwhen5) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

209 
apply (simp add: contlub_cfun_arg) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

210 
apply (simp add: thelubE chain_monofun) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

212 

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

213 
subsection {* Continuous versions of constants *} 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

214 

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

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

216 
sscase :: "('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a ++ 'b) \<rightarrow> 'c" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

217 
"sscase \<equiv> \<Lambda> f g s. Iwhen f g s" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

218 

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

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

220 
"case s of sinl$x => t1  sinr$y => t2" == "sscase$(LAM x. t1)$(LAM y. t2)$s" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

221 

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

222 
text {* continuous versions of lemmas for @{term sscase} *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

223 

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

224 
lemma beta_sscase: "sscase\<cdot>f\<cdot>g\<cdot>s = Iwhen f g s" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

225 
by (simp add: sscase_def cont_Iwhen1 cont_Iwhen2 cont_Iwhen3) 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

226 

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

227 
lemma sscase1 [simp]: "sscase\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

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

229 

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

230 
lemma sscase2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> sscase\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = f\<cdot>x" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

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

232 

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

233 
lemma sscase3 [simp]: "y \<noteq> \<bottom> \<Longrightarrow> sscase\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>y) = g\<cdot>y" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

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

235 

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

236 
lemma sscase4 [simp]: "sscase\<cdot>sinl\<cdot>sinr\<cdot>z = z" 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

237 
by (rule_tac p=z in ssumE, simp_all) 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

238 

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

239 
end 