author  huffman 
Fri, 27 May 2005 00:16:18 +0200  
changeset 16093  cdcbf5a7f38d 
parent 16081  81a4b4a245b0 
child 16210  5d1b752cacc1 
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 

32 

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

33 
subsection {* Type @{typ "'a * 'b"} is a partial order *} 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

34 

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

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

36 

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

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

38 
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

39 

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

40 
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

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

42 

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

43 
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

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

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

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

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

48 
done 
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 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

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

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

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

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

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

56 

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

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

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

59 
(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

60 

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

61 

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

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

63 

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

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

65 

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

66 
lemma monofun_pair1: "monofun (\<lambda>x. (x, y))" 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

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

68 

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

69 
lemma monofun_pair2: "monofun (\<lambda>y. (x, y))" 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

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

71 

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

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

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

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

75 

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

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

77 

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

78 
lemma monofun_fst: "monofun fst" 
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

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

80 

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

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

82 
by (simp add: monofun 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 
subsection {* Type @{typ "'a * 'b"} is a cpo *} 
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 lub_cprod: 
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

105 

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

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

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

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

109 

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

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

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

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

113 

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

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

116 

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

117 
subsection {* Type @{typ "'a * 'b"} is pointed *} 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

118 

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

119 
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

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

121 

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

122 
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

123 
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

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

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

126 

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

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

129 

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

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

131 
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

132 
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

133 

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

134 

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

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

136 

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

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

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

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

140 
apply (erule monofun_pair1 [THEN ch2ch_monofun]) 
16093  141 
apply (simp add: thelub_const) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

143 

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

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

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

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

147 
apply (erule monofun_pair2 [THEN ch2ch_monofun]) 
16093  148 
apply (simp add: thelub_const) 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

150 

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

151 
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

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

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

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

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

156 

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

157 
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

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

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

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

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

162 

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

163 
lemma contlub_fst: "contlub fst" 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

165 
apply (simp add: lub_cprod [THEN thelubI]) 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

167 

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

168 
lemma contlub_snd: "contlub snd" 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

170 
apply (simp add: lub_cprod [THEN thelubI]) 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

172 

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

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

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

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

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

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

178 

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

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

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

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

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

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

184 

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

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

186 

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

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

188 
cpair :: "'a \<rightarrow> 'b \<rightarrow> ('a * 'b)" (* continuous pairing *) 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

189 
cfst :: "('a * 'b) \<rightarrow> 'a" 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

190 
csnd :: "('a * 'b) \<rightarrow> 'b" 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

191 
csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a * 'b) \<rightarrow> 'c" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

192 

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

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

194 
"@ctuple" :: "['a, args] \<Rightarrow> 'a * 'b" ("(1<_,/ _>)") 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

195 

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

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

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

198 
"<x, y>" == "cpair$x$y" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

199 

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

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

201 
cpair_def: "cpair \<equiv> (\<Lambda> x y. (x, y))" 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

202 
cfst_def: "cfst \<equiv> (\<Lambda> p. fst p)" 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

203 
csnd_def: "csnd \<equiv> (\<Lambda> p. snd p)" 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

204 
csplit_def: "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

205 

15609  206 
subsection {* Syntax *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

207 

15609  208 
text {* syntax for @{text "LAM <x,y,z>.e"} *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

209 

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

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

211 
"_LAM" :: "[patterns, 'a \<Rightarrow> 'b] \<Rightarrow> ('a \<rightarrow> 'b)" ("(3LAM <_>./ _)" [0, 10] 10) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

212 

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

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

214 
"LAM <x,y,zs>. b" == "csplit$(LAM x. LAM <y,zs>. b)" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

215 
"LAM <x,y>. LAM zs. b" <= "csplit$(LAM x y zs. b)" 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

216 
"LAM <x,y>.b" == "csplit$(LAM x y. b)" 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

217 

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

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

219 
"_LAM" :: "[patterns, 'a => 'b] => ('a > 'b)" ("(3\<Lambda>()<_>./ _)" [0, 10] 10) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

220 

15609  221 
text {* syntax for Let *} 
222 

223 
constdefs 

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

224 
CLet :: "'a \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'b" 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

225 
"CLet \<equiv> \<Lambda> s f. f\<cdot>s" 
15609  226 

227 
nonterminals 

228 
Cletbinds Cletbind 

229 

230 
syntax 

231 
"_Cbind" :: "[pttrn, 'a] => Cletbind" ("(2_ =/ _)" 10) 

232 
"_Cbindp" :: "[patterns, 'a] => Cletbind" ("(2<_> =/ _)" 10) 

233 
"" :: "Cletbind => Cletbinds" ("_") 

234 
"_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds" ("_;/ _") 

235 
"_CLet" :: "[Cletbinds, 'a] => 'a" ("(Let (_)/ in (_))" 10) 

236 

237 
translations 

238 
"_CLet (_Cbinds b bs) e" == "_CLet b (_CLet bs e)" 

239 
"Let x = a in LAM ys. e" == "CLet$a$(LAM x ys. e)" 

240 
"Let x = a in e" == "CLet$a$(LAM x. e)" 

241 
"Let <xs> = a in e" == "CLet$a$(LAM <xs>. e)" 

242 

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

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

244 

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

245 
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

246 
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

247 

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

248 
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

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

250 

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

251 
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

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

253 

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

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

255 
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

256 

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

257 
lemma inst_cprod_pcpo2: "\<bottom> = <\<bottom>, \<bottom>>" 
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

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

259 

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

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

261 
"<a,b> = \<bottom> \<Longrightarrow> a = \<bottom> \<and> b = \<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_pcpo cpair_eq_pair) 
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 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

265 
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

266 

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

267 
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

268 
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

269 

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

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

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

272 

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

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

274 
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

275 

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

276 
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

277 
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

278 

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

279 
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

280 
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

281 

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

282 
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

283 
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

284 
apply (simp add: cont_fst cont_snd cpair_eq_pair) 
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 

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

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

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

289 
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

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

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

292 

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

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

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

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

296 

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

297 
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

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

299 

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

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

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

302 

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

303 
lemmas Cprod_rews = cfst2 csnd2 csplit2 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

304 

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

305 
end 