author  huffman 
Sat, 04 Jun 2005 00:22:08 +0200  
changeset 16221  879400e029bf 
parent 16210  5d1b752cacc1 
child 16315  bfb2f513916a 
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 (fast intro: trans_less) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

54 

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

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

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

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

58 

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

59 

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

60 
subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *} 
15576
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 
text {* Pair @{text "(_,_)"} is monotone in both arguments *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

63 

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

64 
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

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

66 

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

67 
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

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

69 

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

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

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

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

73 

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

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

75 

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

76 
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

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

78 

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

79 
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

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

81 

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

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

83 

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

84 
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

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

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

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

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

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

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

91 
apply (erule monofun_fst [THEN ch2ch_monofun]) 
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_snd [THEN ch2ch_monofun]) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

103 

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

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

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

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

107 

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

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

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

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

111 

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

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

114 

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

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

116 

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

117 
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

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

119 

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

120 
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

121 
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

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

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

124 

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

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

127 

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

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

129 
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

130 
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

131 

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

132 

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

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

134 

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

135 
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

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

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

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

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

141 

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

142 
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

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

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

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

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

148 

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

149 
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

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

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

152 
apply (rule contlub_pair1) 
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 

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

155 
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

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

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

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

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

160 

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

161 
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

162 
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

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

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

165 

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

166 
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

167 
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

168 
apply (simp add: thelub_cprod) 
15593
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 cont_fst: "cont fst" 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

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

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

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

176 

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

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

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

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

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

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

182 

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

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

184 

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

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

186 
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

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

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

189 
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

190 

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

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

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

193 

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

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

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

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

197 

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

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

199 
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

200 
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

201 
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

202 
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

203 

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

205 

15609  206 
text {* syntax for @{text "LAM <x,y,z>.e"} *} 
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 
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

209 
"_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

210 

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

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

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

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

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

215 

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

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

217 
"_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

218 

15609  219 
text {* syntax for Let *} 
220 

221 
constdefs 

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

222 
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

223 
"CLet \<equiv> \<Lambda> s f. f\<cdot>s" 
15609  224 

225 
nonterminals 

226 
Cletbinds Cletbind 

227 

228 
syntax 

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

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

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

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

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

234 

235 
translations 

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

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

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

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

240 

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

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

242 

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

243 
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

244 
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

245 

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

246 
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

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

248 

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

249 
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

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

251 

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

252 
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

253 
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

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 cpair_strict: "<\<bottom>, \<bottom>> = \<bottom>" 
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

256 
by (simp add: cpair_eq_pair inst_cprod_pcpo) 
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

257 

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

258 
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

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

260 

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

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

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

263 
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

264 

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

265 
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

266 
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

267 

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

268 
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

269 
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

270 

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

271 
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

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

273 

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

274 
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

275 
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

276 

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

277 
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

278 
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

279 

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

280 
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

281 
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

282 

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

283 
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

284 
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

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

286 
done 
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 lub_cprod2: 
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset

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

290 
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

291 
apply (erule lub_cprod) 
15576
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 

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

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

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

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

297 

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

298 
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

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

300 

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

301 
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

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

303 

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

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

305 

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

306 
end 