author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 18289  56ddf617d6e8 
child 25131  2c8caac48ade 
permissions  rwrr 
15600  1 
(* Title: HOLCF/Cprod.thy 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

2 
ID: $Id$ 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

3 
Author: Franz Regensburger 
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:
16057
diff
changeset

5 
Partial ordering for cartesian product of HOL products. 
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 cpo of cartesian products *} 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

9 

15577  10 
theory Cprod 
11 
imports Cfun 

12 
begin 

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

13 

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

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

15 

16008  16 
subsection {* Type @{typ unit} is a pcpo *} 
17 

18 
instance unit :: sq_ord .. 

19 

20 
defs (overloaded) 

21 
less_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<equiv> True" 

22 

23 
instance unit :: po 

24 
by intro_classes simp_all 

25 

26 
instance unit :: cpo 

27 
by intro_classes (simp add: is_lub_def is_ub_def) 

28 

29 
instance unit :: pcpo 

30 
by intro_classes simp 

31 

18289  32 
constdefs 
33 
unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a" 

34 
"unit_when \<equiv> \<Lambda> a _. a" 

16008  35 

18289  36 
translations 
37 
"\<Lambda>(). t" == "unit_when\<cdot>t" 

38 

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

40 
by (simp add: unit_when_def) 

41 

42 

43 
subsection {* Product type is a partial order *} 

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

44 

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

45 
instance "*" :: (sq_ord, sq_ord) sq_ord .. 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

46 

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

47 
defs (overloaded) 
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

48 
less_cprod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

49 

16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

50 
lemma refl_less_cprod: "(p::'a * 'b) \<sqsubseteq> p" 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

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

52 

16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

53 
lemma antisym_less_cprod: "\<lbrakk>(p1::'a * 'b) \<sqsubseteq> p2; p2 \<sqsubseteq> p1\<rbrakk> \<Longrightarrow> p1 = p2" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

54 
apply (unfold less_cprod_def) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

55 
apply (rule injective_fst_snd) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

56 
apply (fast intro: antisym_less) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

57 
apply (fast intro: antisym_less) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

59 

16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

60 
lemma trans_less_cprod: "\<lbrakk>(p1::'a*'b) \<sqsubseteq> p2; p2 \<sqsubseteq> p3\<rbrakk> \<Longrightarrow> p1 \<sqsubseteq> p3" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

61 
apply (unfold less_cprod_def) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

62 
apply (fast intro: trans_less) 
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 

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

65 
instance "*" :: (cpo, cpo) po 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

67 
(assumption  rule refl_less_cprod antisym_less_cprod trans_less_cprod)+ 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

68 

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

69 

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

70 
subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

71 

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

72 
text {* Pair @{text "(_,_)"} is monotone in both arguments *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

73 

16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

74 
lemma monofun_pair1: "monofun (\<lambda>x. (x, y))" 
16210
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset

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

76 

16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

77 
lemma monofun_pair2: "monofun (\<lambda>y. (x, y))" 
16210
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset

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

79 

16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

80 
lemma monofun_pair: 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

81 
"\<lbrakk>x1 \<sqsubseteq> x2; y1 \<sqsubseteq> y2\<rbrakk> \<Longrightarrow> (x1, y1) \<sqsubseteq> (x2, y2)" 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

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

83 

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

84 
text {* @{term fst} and @{term snd} are monotone *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

85 

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

86 
lemma monofun_fst: "monofun fst" 
16210
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset

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

88 

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

89 
lemma monofun_snd: "monofun snd" 
16210
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset

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

91 

18289  92 
subsection {* Product type is a cpo *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

93 

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

94 
lemma lub_cprod: 
16210
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset

95 
"chain S \<Longrightarrow> range S << (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

96 
apply (rule is_lubI) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

97 
apply (rule ub_rangeI) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

98 
apply (rule_tac t = "S i" in surjective_pairing [THEN ssubst]) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

99 
apply (rule monofun_pair) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

100 
apply (rule is_ub_thelub) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

101 
apply (erule monofun_fst [THEN ch2ch_monofun]) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

102 
apply (rule is_ub_thelub) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

103 
apply (erule monofun_snd [THEN ch2ch_monofun]) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

104 
apply (rule_tac t = "u" in surjective_pairing [THEN ssubst]) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

105 
apply (rule monofun_pair) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

106 
apply (rule is_lub_thelub) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

107 
apply (erule monofun_fst [THEN ch2ch_monofun]) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

108 
apply (erule monofun_fst [THEN ub2ub_monofun]) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

109 
apply (rule is_lub_thelub) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

110 
apply (erule monofun_snd [THEN ch2ch_monofun]) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

111 
apply (erule monofun_snd [THEN ub2ub_monofun]) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

113 

16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

114 
lemma thelub_cprod: 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

115 
"chain S \<Longrightarrow> lub (range S) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

116 
by (rule lub_cprod [THEN thelubI]) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

117 

16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

118 
lemma cpo_cprod: 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

119 
"chain (S::nat \<Rightarrow> 'a::cpo * 'b::cpo) \<Longrightarrow> \<exists>x. range S << x" 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

120 
by (rule exI, erule lub_cprod) 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

121 

15609  122 
instance "*" :: (cpo, cpo) cpo 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

123 
by intro_classes (rule cpo_cprod) 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

124 

18289  125 
subsection {* Product type is pointed *} 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

126 

16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

127 
lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p" 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

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

129 

16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

130 
lemma least_cprod: "EX x::'a::pcpo * 'b::pcpo. ALL y. x \<sqsubseteq> y" 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

131 
apply (rule_tac x = "(\<bottom>, \<bottom>)" in exI) 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

132 
apply (rule minimal_cprod [THEN allI]) 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

134 

15609  135 
instance "*" :: (pcpo, pcpo) pcpo 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

136 
by intro_classes (rule least_cprod) 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

137 

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

138 
text {* for compatibility with old HOLCFVersion *} 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

139 
lemma inst_cprod_pcpo: "UU = (UU,UU)" 
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

140 
by (rule minimal_cprod [THEN UU_I, symmetric]) 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

141 

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

142 

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

143 
subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *} 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

144 

16916  145 
lemma contlub_pair1: "contlub (\<lambda>x. (x, y))" 
16210
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset

146 
apply (rule contlubI) 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

147 
apply (subst thelub_cprod) 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

148 
apply (erule monofun_pair1 [THEN ch2ch_monofun]) 
18077
f1f4f951ec8d
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
huffman
parents:
17837
diff
changeset

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

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

151 

16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

152 
lemma contlub_pair2: "contlub (\<lambda>y. (x, y))" 
16210
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset

153 
apply (rule contlubI) 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

154 
apply (subst thelub_cprod) 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

155 
apply (erule monofun_pair2 [THEN ch2ch_monofun]) 
18077
f1f4f951ec8d
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
huffman
parents:
17837
diff
changeset

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

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

158 

16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

159 
lemma cont_pair1: "cont (\<lambda>x. (x, y))" 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

160 
apply (rule monocontlub2cont) 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

161 
apply (rule monofun_pair1) 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

162 
apply (rule contlub_pair1) 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

164 

16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

165 
lemma cont_pair2: "cont (\<lambda>y. (x, y))" 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

166 
apply (rule monocontlub2cont) 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

167 
apply (rule monofun_pair2) 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

168 
apply (rule contlub_pair2) 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

170 

16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

171 
lemma contlub_fst: "contlub fst" 
16210
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset

172 
apply (rule contlubI) 
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset

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

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

175 

16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

176 
lemma contlub_snd: "contlub snd" 
16210
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset

177 
apply (rule contlubI) 
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset

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

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

180 

16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

181 
lemma cont_fst: "cont fst" 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

182 
apply (rule monocontlub2cont) 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

183 
apply (rule monofun_fst) 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

184 
apply (rule contlub_fst) 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

186 

16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

187 
lemma cont_snd: "cont snd" 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

188 
apply (rule monocontlub2cont) 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

189 
apply (rule monofun_snd) 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

190 
apply (rule contlub_snd) 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

192 

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

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

194 

17834  195 
constdefs 
196 
cpair :: "'a \<rightarrow> 'b \<rightarrow> ('a * 'b)" (* continuous pairing *) 

197 
"cpair \<equiv> (\<Lambda> x y. (x, y))" 

198 

199 
cfst :: "('a * 'b) \<rightarrow> 'a" 

200 
"cfst \<equiv> (\<Lambda> p. fst p)" 

201 

202 
csnd :: "('a * 'b) \<rightarrow> 'b" 

203 
"csnd \<equiv> (\<Lambda> p. snd p)" 

204 

16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

205 
csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a * 'b) \<rightarrow> 'c" 
17834  206 
"csplit \<equiv> (\<Lambda> f p. f\<cdot>(cfst\<cdot>p)\<cdot>(csnd\<cdot>p))" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

207 

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

208 
syntax 
17834  209 
"_ctuple" :: "['a, args] \<Rightarrow> 'a * 'b" ("(1<_,/ _>)") 
210 

211 
syntax (xsymbols) 

212 
"_ctuple" :: "['a, args] \<Rightarrow> 'a * 'b" ("(1\<langle>_,/ _\<rangle>)") 

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

213 

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

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

215 
"\<langle>x, y, z\<rangle>" == "\<langle>x, \<langle>y, z\<rangle>\<rangle>" 
20e5a6440790
change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
huffman
parents:
18077
diff
changeset

216 
"\<langle>x, y\<rangle>" == "cpair\<cdot>x\<cdot>y" 
17834  217 

17816
9942c5ed866a
new syntax translations for continuous lambda abstraction
huffman
parents:
16916
diff
changeset

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

219 
"\<Lambda>(cpair\<cdot>x\<cdot>y). t" == "csplit\<cdot>(\<Lambda> x y. t)" 
17816
9942c5ed866a
new syntax translations for continuous lambda abstraction
huffman
parents:
16916
diff
changeset

220 

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

221 

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

222 
subsection {* Convert all lemmas to the continuous versions *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

223 

16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

224 
lemma cpair_eq_pair: "<x, y> = (x, y)" 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

225 
by (simp add: cpair_def cont_pair1 cont_pair2) 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

226 

81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

227 
lemma inject_cpair: "<a,b> = <aa,ba> \<Longrightarrow> a = aa \<and> b = ba" 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

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

229 

16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

230 
lemma cpair_eq [iff]: "(<a, b> = <a', b'>) = (a = a' \<and> b = b')" 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

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

232 

18077
f1f4f951ec8d
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
huffman
parents:
17837
diff
changeset

233 
lemma cpair_less [iff]: "(<a, b> \<sqsubseteq> <a', b'>) = (a \<sqsubseteq> a' \<and> b \<sqsubseteq> b')" 
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

234 
by (simp add: cpair_eq_pair less_cprod_def) 
16057
e23a61b3406f
added lemma cpair_eq, made cfst_strict and csnd_strict into simp rules
huffman
parents:
16008
diff
changeset

235 

18077
f1f4f951ec8d
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
huffman
parents:
17837
diff
changeset

236 
lemma cpair_defined_iff [iff]: "(<x, y> = \<bottom>) = (x = \<bottom> \<and> y = \<bottom>)" 
16916  237 
by (simp add: inst_cprod_pcpo cpair_eq_pair) 
238 

16210
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset

239 
lemma cpair_strict: "<\<bottom>, \<bottom>> = \<bottom>" 
18077
f1f4f951ec8d
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
huffman
parents:
17837
diff
changeset

240 
by simp 
16210
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset

241 

16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

242 
lemma inst_cprod_pcpo2: "\<bottom> = <\<bottom>, \<bottom>>" 
16916  243 
by (rule cpair_strict [symmetric]) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

244 

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

245 
lemma defined_cpair_rev: 
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

246 
"<a,b> = \<bottom> \<Longrightarrow> a = \<bottom> \<and> b = \<bottom>" 
18077
f1f4f951ec8d
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
huffman
parents:
17837
diff
changeset

247 
by simp 
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

248 

81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

249 
lemma Exh_Cprod2: "\<exists>a b. z = <a, b>" 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

250 
by (simp add: cpair_eq_pair) 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

251 

81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

252 
lemma cprodE: "\<lbrakk>\<And>x y. p = <x, y> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

253 
by (cut_tac Exh_Cprod2, auto) 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

254 

16210
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset

255 
lemma cfst_cpair [simp]: "cfst\<cdot><x, y> = x" 
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

256 
by (simp add: cpair_eq_pair cfst_def cont_fst) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

257 

16210
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset

258 
lemma csnd_cpair [simp]: "csnd\<cdot><x, y> = y" 
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

259 
by (simp add: cpair_eq_pair csnd_def cont_snd) 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

260 

81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

261 
lemma cfst_strict [simp]: "cfst\<cdot>\<bottom> = \<bottom>" 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

262 
by (simp add: inst_cprod_pcpo2) 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

263 

81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

264 
lemma csnd_strict [simp]: "csnd\<cdot>\<bottom> = \<bottom>" 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

265 
by (simp add: inst_cprod_pcpo2) 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

266 

81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

267 
lemma surjective_pairing_Cprod2: "<cfst\<cdot>p, csnd\<cdot>p> = p" 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

268 
apply (unfold cfst_def csnd_def) 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

269 
apply (simp add: cont_fst cont_snd cpair_eq_pair) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

271 

16750  272 
lemma less_cprod: "x \<sqsubseteq> y = (cfst\<cdot>x \<sqsubseteq> cfst\<cdot>y \<and> csnd\<cdot>x \<sqsubseteq> csnd\<cdot>y)" 
16315  273 
by (simp add: less_cprod_def cfst_def csnd_def cont_fst cont_snd) 
274 

16750  275 
lemma eq_cprod: "(x = y) = (cfst\<cdot>x = cfst\<cdot>y \<and> csnd\<cdot>x = csnd\<cdot>y)" 
276 
by (auto simp add: po_eq_conv less_cprod) 

277 

17837  278 
lemma compact_cpair [simp]: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact <x, y>" 
279 
by (rule compactI, simp add: less_cprod) 

280 

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

281 
lemma lub_cprod2: 
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

282 
"chain S \<Longrightarrow> range S << <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>" 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

283 
apply (simp add: cpair_eq_pair cfst_def csnd_def cont_fst cont_snd) 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

284 
apply (erule lub_cprod) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

286 

16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

287 
lemma thelub_cprod2: 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

288 
"chain S \<Longrightarrow> lub (range S) = <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>" 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

289 
by (rule lub_cprod2 [THEN thelubI]) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

290 

18077
f1f4f951ec8d
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
huffman
parents:
17837
diff
changeset

291 
lemma csplit1 [simp]: "csplit\<cdot>f\<cdot>\<bottom> = f\<cdot>\<bottom>\<cdot>\<bottom>" 
f1f4f951ec8d
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
huffman
parents:
17837
diff
changeset

292 
by (simp add: csplit_def) 
f1f4f951ec8d
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
huffman
parents:
17837
diff
changeset

293 

16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

294 
lemma csplit2 [simp]: "csplit\<cdot>f\<cdot><x,y> = f\<cdot>x\<cdot>y" 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

296 

16553  297 
lemma csplit3 [simp]: "csplit\<cdot>cpair\<cdot>z = z" 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

299 

16210
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset

300 
lemmas Cprod_rews = cfst_cpair csnd_cpair csplit2 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

301 

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

302 
end 