author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 19440  b2877e230b07 
child 25131  2c8caac48ade 
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 

17817  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 

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

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

29 

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

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

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

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

33 

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

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

35 
"sinr \<equiv> \<Lambda> b. Abs_Ssum <\<bottom>, b>" 
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 
subsection {* Properties of @{term sinl} and @{term sinr} *} 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

38 

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

39 
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

40 
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

41 

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

42 
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

43 
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

44 

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

45 
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

46 
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

47 

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

48 
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

49 
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

50 

17837  51 
lemma compact_sinl [simp]: "compact x \<Longrightarrow> compact (sinl\<cdot>x)" 
52 
by (rule compact_Ssum, simp add: Rep_Ssum_sinl) 

53 

54 
lemma compact_sinr [simp]: "compact x \<Longrightarrow> compact (sinr\<cdot>x)" 

55 
by (rule compact_Ssum, simp add: Rep_Ssum_sinr) 

56 

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

57 
lemma sinl_strict [simp]: "sinl\<cdot>\<bottom> = \<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

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

59 

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

60 
lemma sinr_strict [simp]: "sinr\<cdot>\<bottom> = \<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

61 
by (simp add: sinr_Abs_Ssum Abs_Ssum_strict cpair_strict) 
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

62 

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

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

64 
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

65 

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

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

67 
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

68 

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

69 
lemma sinl_inject: "sinl\<cdot>x = sinl\<cdot>y \<Longrightarrow> x = y" 
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

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

71 

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

72 
lemma sinr_inject: "sinr\<cdot>x = sinr\<cdot>y \<Longrightarrow> x = y" 
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

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

74 

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

75 
lemma sinl_defined_iff [simp]: "(sinl\<cdot>x = \<bottom>) = (x = \<bottom>)" 
17837  76 
by (cut_tac sinl_eq [of "x" "\<bottom>"], simp) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

77 

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

78 
lemma sinr_defined_iff [simp]: "(sinr\<cdot>x = \<bottom>) = (x = \<bottom>)" 
17837  79 
by (cut_tac sinr_eq [of "x" "\<bottom>"], simp) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

80 

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

81 
lemma sinl_defined [intro!]: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>" 
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

82 
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

83 

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

84 
lemma sinr_defined [intro!]: "x \<noteq> \<bottom> \<Longrightarrow> sinr\<cdot>x \<noteq> \<bottom>" 
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

85 
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

86 

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

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

88 

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

90 
"z = \<bottom> \<or> (\<exists>a. z = sinl\<cdot>a \<and> a \<noteq> \<bottom>) \<or> (\<exists>b. z = sinr\<cdot>b \<and> b \<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

91 
apply (rule_tac x=z in Abs_Ssum_induct) 
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

92 
apply (rule_tac p=y in cprodE) 
16921  93 
apply (simp add: sinl_Abs_Ssum sinr_Abs_Ssum) 
94 
apply (simp add: Abs_Ssum_inject Ssum_def) 

95 
apply (auto simp add: cpair_strict Abs_Ssum_strict) 

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

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

97 

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

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

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

100 
\<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

101 
\<And>y. \<lbrakk>p = sinr\<cdot>y; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" 
16921  102 
by (cut_tac z=p in Exh_Ssum, auto) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

103 

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

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

105 
"\<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

106 
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

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

108 
apply simp 
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 
done 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

111 

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

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

113 

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

114 
lemma sinl_less [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> 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

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

116 

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

117 
lemma sinr_less [simp]: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> 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

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

119 

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

120 
lemma sinl_less_sinr [simp]: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)" 
19440  121 
by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr) 
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

122 

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

123 
lemma sinr_less_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)" 
19440  124 
by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

125 

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

126 
lemma sinl_eq_sinr [simp]: "(sinl\<cdot>x = sinr\<cdot>y) = (x = \<bottom> \<and> y = \<bottom>)" 
19440  127 
by (subst po_eq_conv, simp) 
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

128 

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

129 
lemma sinr_eq_sinl [simp]: "(sinr\<cdot>x = sinl\<cdot>y) = (x = \<bottom> \<and> y = \<bottom>)" 
19440  130 
by (subst po_eq_conv, simp) 
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

131 

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

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

133 

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

134 
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

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

136 
apply (rule_tac x="\<bottom>" in exI, simp) 
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

137 
apply 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

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

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

140 

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

141 
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

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

143 
apply (rule_tac x="\<bottom>" in exI, simp) 
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

144 
apply 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

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

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

147 

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

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

149 
"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

150 
(\<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

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

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

153 
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

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

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

157 
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

158 
apply (drule less_sinlD, clarify) 
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

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

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

161 
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

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

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

165 
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

166 
apply (drule less_sinrD, clarify) 
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

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

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

169 

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

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

171 

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

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

173 
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

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

175 
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

176 
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

177 

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

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

179 

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

180 
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

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

182 

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

183 
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

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

185 

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

186 
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

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

188 

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

189 
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

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

191 

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

192 
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

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

194 

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

195 
subsection {* Continuity of @{term Iwhen} *} 
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 
text {* @{term Iwhen} is continuous in all arguments *} 
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

198 

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

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

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

201 

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

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

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

204 

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

205 
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

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

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

208 
apply (simp add: contlub_cfun_arg [symmetric]) 
16823  209 
apply (simp add: Iwhen4 cont_cfun_arg) 
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset

210 
apply (simp add: contlub_cfun_arg [symmetric]) 
16823  211 
apply (simp add: Iwhen5 cont_cfun_arg) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

213 

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

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

215 

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

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

217 
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

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

219 

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

220 
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

221 
"case s of sinl\<cdot>x \<Rightarrow> t1  sinr\<cdot>y \<Rightarrow> t2" == "sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s" 
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

222 

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

223 
translations 
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

224 
"\<Lambda>(sinl\<cdot>x). t" == "sscase\<cdot>(\<Lambda> x. t)\<cdot>\<bottom>" 
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

225 
"\<Lambda>(sinr\<cdot>y). t" == "sscase\<cdot>\<bottom>\<cdot>(\<Lambda> y. t)" 
16060
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 
text {* continuous versions of lemmas for @{term sscase} *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

228 

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

229 
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

230 
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

231 

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

232 
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

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

234 

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

235 
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

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

237 

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

238 
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

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

240 

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

241 
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

242 
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

243 

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

244 
end 