author  wenzelm 
Wed, 25 May 2005 09:44:34 +0200  
changeset 16070  4a83dd540b88 
parent 16057  e23a61b3406f 
child 16081  81a4b4a245b0 
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 

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

33 
subsection {* Ordering on @{typ "'a * 'b"} *} 
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) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

38 
less_cprod_def: "p1 << p2 == (fst p1<<fst p2 & snd p1 << snd p2)" 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

39 

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

40 
subsection {* Type @{typ "'a * 'b"} is a partial order *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

41 

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

42 
lemma refl_less_cprod: "(p::'a*'b) << p" 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

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

45 
done 
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 
lemma antisym_less_cprod: "[(p1::'a * 'b) << p2;p2 << p1] ==> p1=p2" 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

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

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

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

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

53 

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

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

55 
"[(p1::'a*'b) << p2;p2 << p3] ==> p1 << p3" 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

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

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

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

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

61 

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

62 
defaultsort pcpo 
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 
instance "*" :: (cpo, cpo) po 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

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

67 

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

68 
text {* for compatibility with old HOLCFVersion *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

69 
lemma inst_cprod_po: "(op <<)=(%x y. fst x<<fst y & snd x<<snd y)" 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

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

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

73 

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

74 
lemma less_cprod4c: "(x1,y1) << (x2,y2) ==> x1 << x2 & y1 << y2" 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

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

77 

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

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

79 

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

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

81 

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

82 
lemma monofun_pair1: "monofun Pair" 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

84 

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

85 
lemma monofun_pair2: "monofun(Pair x)" 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

87 

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

88 
lemma monofun_pair: "[x1<<x2; y1<<y2] ==> (x1::'a::cpo,y1::'b::cpo)<<(x2,y2)" 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

90 

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

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

92 

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

93 
lemma monofun_fst: "monofun fst" 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

95 

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

96 
lemma monofun_snd: "monofun snd" 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

98 

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

99 
subsection {* Type @{typ "'a * 'b"} is a cpo *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

100 

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

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

102 
"chain S ==> range S<<(lub(range(%i. fst(S i))),lub(range(%i. snd(S i))))" 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

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

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

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

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

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

109 
apply (rule is_ub_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 (rule_tac t = "u" in surjective_pairing [THEN ssubst]) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

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

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

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

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

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

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

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

120 

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

121 
lemmas thelub_cprod = lub_cprod [THEN thelubI, standard] 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

123 
"chain ?S1 ==> 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

124 
lub (range ?S1) = 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

125 
(lub (range (%i. fst (?S1 i))), lub (range (%i. snd (?S1 i))))" : thm 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

126 

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

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

128 

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

129 
lemma cpo_cprod: "chain(S::nat=>'a::cpo*'b::cpo)==>EX x. range S<< x" 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

131 

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

133 
by intro_classes (rule cpo_cprod) 
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 {* Type @{typ "'a * 'b"} is pointed *} 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

136 

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

137 
lemma minimal_cprod: "(UU,UU)<<p" 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

139 

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

140 
lemmas UU_cprod_def = minimal_cprod [THEN minimal2UU, symmetric, standard] 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

141 

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

142 
lemma least_cprod: "EX x::'a*'b. ALL y. x<<y" 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

143 
apply (rule_tac x = " (UU,UU) " in exI) 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

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

146 

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

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

149 

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

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

151 
lemma inst_cprod_pcpo: "UU = (UU,UU)" 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

152 
apply (simp add: UU_cprod_def[folded UU_def]) 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

154 

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

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

156 

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

157 
lemma contlub_pair1: "contlub(Pair)" 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

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

160 
apply (subst lub_fun [THEN thelubI]) 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

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

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

164 
apply (erule monofun_pair1 [THEN ch2ch_monofun]) 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

165 
apply (simp add: lub_const [THEN thelubI]) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

167 

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

168 
lemma contlub_pair2: "contlub(Pair(x))" 
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 (subst thelub_cprod) 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

171 
apply (erule monofun_pair2 [THEN ch2ch_monofun]) 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

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

174 

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

175 
lemma cont_pair1: "cont(Pair)" 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

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

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

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

180 

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

181 
lemma cont_pair2: "cont(Pair(x))" 
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_pair2) 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

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

186 

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

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

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

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

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

191 

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

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

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

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

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

196 

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

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

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

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

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

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

202 

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

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

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

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

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

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

208 

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

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

210 

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

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

212 
cpair :: "'a::cpo > 'b::cpo > ('a*'b)" (* continuous pairing *) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

213 
cfst :: "('a::cpo*'b::cpo)>'a" 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

214 
csnd :: "('a::cpo*'b::cpo)>'b" 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

215 
csplit :: "('a::cpo>'b::cpo>'c::cpo)>('a*'b)>'c" 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

216 

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

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

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

219 

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

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

221 
"<x, y, z>" == "<x, <y, z>>" 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

223 

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

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

225 
cpair_def: "cpair == (LAM x y.(x,y))" 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

226 
cfst_def: "cfst == (LAM p. fst(p))" 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

227 
csnd_def: "csnd == (LAM p. snd(p))" 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

228 
csplit_def: "csplit == (LAM f p. f$(cfst$p)$(csnd$p))" 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

229 

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

231 

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

233 

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

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

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

236 

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

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

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

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

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

241 

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

242 
syntax (xsymbols) 
15577  243 
"_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

244 

15609  245 
text {* syntax for Let *} 
246 

247 
constdefs 

248 
CLet :: "'a::cpo > ('a > 'b::cpo) > 'b" 

249 
"CLet == LAM s f. f$s" 

250 

251 
nonterminals 

252 
Cletbinds Cletbind 

253 

254 
syntax 

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

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

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

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

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

260 

261 
translations 

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

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

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

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

266 

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

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

268 

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

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

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

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

272 
apply (simp add: cont_pair1 cont_pair2 cont2cont_CF1L) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

273 
apply (subst beta_cfun) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

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

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

277 

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

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

279 
"<a,b> = <aa,ba> ==> a=aa & b=ba" 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

281 

16057
e23a61b3406f
added lemma cpair_eq, made cfst_strict and csnd_strict into simp rules
huffman
parents:
16008
diff
changeset

282 
lemma cpair_eq [iff]: "(<a, b> = <a', b'>) = (a = a' & b = b')" 
e23a61b3406f
added lemma cpair_eq, made cfst_strict and csnd_strict into simp rules
huffman
parents:
16008
diff
changeset

283 
by (blast dest!: inject_cpair) 
e23a61b3406f
added lemma cpair_eq, made cfst_strict and csnd_strict into simp rules
huffman
parents:
16008
diff
changeset

284 

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

285 
lemma inst_cprod_pcpo2: "UU = <UU,UU>" 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

287 

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

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

289 
"<a,b> = UU ==> a = UU & b = UU" 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

290 
apply (drule inst_cprod_pcpo2 [THEN subst]) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

291 
apply (erule inject_cpair) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

293 

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

294 
lemma Exh_Cprod2: "? a b. z=<a,b>" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

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

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

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

299 
apply (erule beta_cfun_cprod [THEN ssubst]) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

303 
assumes prems: "!!x y. [ p = <x,y> ] ==> Q" 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

304 
shows "Q" 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

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

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

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

309 

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

310 
lemma cfst2 [simp]: "cfst$<x,y> = x" 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

311 
by (simp add: cpair_def cfst_def beta_cfun_cprod cont_fst) 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

312 

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

313 
lemma csnd2 [simp]: "csnd$<x,y> = y" 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

314 
by (simp add: cpair_def csnd_def beta_cfun_cprod cont_snd) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

315 

16057
e23a61b3406f
added lemma cpair_eq, made cfst_strict and csnd_strict into simp rules
huffman
parents:
16008
diff
changeset

316 
lemma cfst_strict [simp]: "cfst$UU = UU" 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

318 

16057
e23a61b3406f
added lemma cpair_eq, made cfst_strict and csnd_strict into simp rules
huffman
parents:
16008
diff
changeset

319 
lemma csnd_strict [simp]: "csnd$UU = UU" 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

321 

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

322 
lemma surjective_pairing_Cprod2: "<cfst$p, csnd$p> = p" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

323 
apply (unfold cfst_def csnd_def cpair_def) 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

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

326 

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

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

328 
"<xa,ya> << <x,y> ==> xa<<x & ya << y" 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

329 
by (simp add: cpair_def beta_cfun_cprod inst_cprod_po) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

330 

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

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

332 
"[chain(S)] ==> range(S) << 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

333 
<(lub(range(%i. cfst$(S i)))) , lub(range(%i. csnd$(S i)))>" 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

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

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

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

338 

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

339 
lemmas thelub_cprod2 = lub_cprod2 [THEN thelubI, standard] 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

341 
chain ?S1 ==> 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

342 
lub (range ?S1) = 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

343 
<lub (range (%i. cfst$(?S1 i))), lub (range (%i. csnd$(?S1 i)))>" 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

345 

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

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

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

348 

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

349 
lemma csplit3: "csplit$cpair$z=z" 
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

351 

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

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

353 

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

354 
end 