author  blanchet 
Fri, 14 Feb 2014 07:53:46 +0100  
changeset 55469  b19dd108f0c2 
parent 55468  98b25c51e9e5 
child 55534  b18bdcbda41b 
permissions  rwrr 
10213  1 
(* Title: HOL/Sum_Type.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

3 
Copyright 1992 University of Cambridge 

4 
*) 

5 

15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

6 
header{*The Disjoint Sum of Two Types*} 
10213  7 

15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

8 
theory Sum_Type 
33961  9 
imports Typedef Inductive Fun 
15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

10 
begin 
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

11 

33962  12 
subsection {* Construction of the sum type and its basic abstract operations *} 
10213  13 

33962  14 
definition Inl_Rep :: "'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" where 
15 
"Inl_Rep a x y p \<longleftrightarrow> x = a \<and> p" 

10213  16 

33962  17 
definition Inr_Rep :: "'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" where 
18 
"Inr_Rep b x y p \<longleftrightarrow> y = b \<and> \<not> p" 

15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

19 

45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45204
diff
changeset

20 
definition "sum = {f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}" 
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45204
diff
changeset

21 

49834  22 
typedef ('a, 'b) sum (infixr "+" 10) = "sum :: ('a => 'b => bool => bool) set" 
45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45204
diff
changeset

23 
unfolding sum_def by auto 
10213  24 

37388  25 
lemma Inl_RepI: "Inl_Rep a \<in> sum" 
26 
by (auto simp add: sum_def) 

15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

27 

37388  28 
lemma Inr_RepI: "Inr_Rep b \<in> sum" 
29 
by (auto simp add: sum_def) 

15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

30 

37388  31 
lemma inj_on_Abs_sum: "A \<subseteq> sum \<Longrightarrow> inj_on Abs_sum A" 
32 
by (rule inj_on_inverseI, rule Abs_sum_inverse) auto 

15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

33 

33962  34 
lemma Inl_Rep_inject: "inj_on Inl_Rep A" 
35 
proof (rule inj_onI) 

36 
show "\<And>a c. Inl_Rep a = Inl_Rep c \<Longrightarrow> a = c" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

37 
by (auto simp add: Inl_Rep_def fun_eq_iff) 
33962  38 
qed 
15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

39 

33962  40 
lemma Inr_Rep_inject: "inj_on Inr_Rep A" 
41 
proof (rule inj_onI) 

42 
show "\<And>b d. Inr_Rep b = Inr_Rep d \<Longrightarrow> b = d" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

43 
by (auto simp add: Inr_Rep_def fun_eq_iff) 
33962  44 
qed 
15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

45 

33962  46 
lemma Inl_Rep_not_Inr_Rep: "Inl_Rep a \<noteq> Inr_Rep b" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

47 
by (auto simp add: Inl_Rep_def Inr_Rep_def fun_eq_iff) 
15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

48 

33962  49 
definition Inl :: "'a \<Rightarrow> 'a + 'b" where 
37388  50 
"Inl = Abs_sum \<circ> Inl_Rep" 
15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

51 

33962  52 
definition Inr :: "'b \<Rightarrow> 'a + 'b" where 
37388  53 
"Inr = Abs_sum \<circ> Inr_Rep" 
15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

54 

29025
8c8859c0d734
move lemmas from Numeral_Type.thy to other theories
huffman
parents:
28524
diff
changeset

55 
lemma inj_Inl [simp]: "inj_on Inl A" 
37388  56 
by (auto simp add: Inl_def intro!: comp_inj_on Inl_Rep_inject inj_on_Abs_sum Inl_RepI) 
29025
8c8859c0d734
move lemmas from Numeral_Type.thy to other theories
huffman
parents:
28524
diff
changeset

57 

33962  58 
lemma Inl_inject: "Inl x = Inl y \<Longrightarrow> x = y" 
59 
using inj_Inl by (rule injD) 

15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

60 

29025
8c8859c0d734
move lemmas from Numeral_Type.thy to other theories
huffman
parents:
28524
diff
changeset

61 
lemma inj_Inr [simp]: "inj_on Inr A" 
37388  62 
by (auto simp add: Inr_def intro!: comp_inj_on Inr_Rep_inject inj_on_Abs_sum Inr_RepI) 
15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

63 

33962  64 
lemma Inr_inject: "Inr x = Inr y \<Longrightarrow> x = y" 
65 
using inj_Inr by (rule injD) 

15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

66 

33962  67 
lemma Inl_not_Inr: "Inl a \<noteq> Inr b" 
68 
proof  

37388  69 
from Inl_RepI [of a] Inr_RepI [of b] have "{Inl_Rep a, Inr_Rep b} \<subseteq> sum" by auto 
70 
with inj_on_Abs_sum have "inj_on Abs_sum {Inl_Rep a, Inr_Rep b}" . 

71 
with Inl_Rep_not_Inr_Rep [of a b] inj_on_contraD have "Abs_sum (Inl_Rep a) \<noteq> Abs_sum (Inr_Rep b)" by auto 

33962  72 
then show ?thesis by (simp add: Inl_def Inr_def) 
73 
qed 

15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

74 

33962  75 
lemma Inr_not_Inl: "Inr b \<noteq> Inl a" 
76 
using Inl_not_Inr by (rule not_sym) 

15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

77 

797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset

78 
lemma sumE: 
33962  79 
assumes "\<And>x::'a. s = Inl x \<Longrightarrow> P" 
80 
and "\<And>y::'b. s = Inr y \<Longrightarrow> P" 

81 
shows P 

37388  82 
proof (rule Abs_sum_cases [of s]) 
33962  83 
fix f 
37388  84 
assume "s = Abs_sum f" and "f \<in> sum" 
85 
with assms show P by (auto simp add: sum_def Inl_def Inr_def) 

33962  86 
qed 
33961  87 

55469
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

88 
free_constructors case_sum for 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

89 
isl: Inl projl 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

90 
 Inr projr 
55393
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset

91 
by (erule sumE, assumption) (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr) 
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset

92 

55442  93 
text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *} 
94 

55393
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset

95 
setup {* Sign.mandatory_path "old" *} 
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset

96 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37388
diff
changeset

97 
rep_datatype Inl Inr 
33961  98 
proof  
99 
fix P 

100 
fix s :: "'a + 'b" 

101 
assume x: "\<And>x\<Colon>'a. P (Inl x)" and y: "\<And>y\<Colon>'b. P (Inr y)" 

102 
then show "P s" by (auto intro: sumE [of s]) 

33962  103 
qed (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr) 
104 

55393
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset

105 
setup {* Sign.parent_path *} 
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset

106 

55468
98b25c51e9e5
renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)
blanchet
parents:
55467
diff
changeset

107 
text {* But erase the prefix for properties that are not generated by @{text free_constructors}. *} 
55442  108 

55393
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset

109 
setup {* Sign.mandatory_path "sum" *} 
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset

110 

ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset

111 
declare 
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset

112 
old.sum.inject[iff del] 
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset

113 
old.sum.distinct(1)[simp del, induct_simp del] 
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset

114 

ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset

115 
lemmas induct = old.sum.induct 
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset

116 
lemmas inducts = old.sum.inducts 
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset

117 
lemmas recs = old.sum.recs 
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset

118 
lemmas cases = sum.case 
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset

119 
lemmas simps = sum.inject sum.distinct sum.case old.sum.recs 
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset

120 

ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset

121 
setup {* Sign.parent_path *} 
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset

122 

40610  123 
primrec sum_map :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd" where 
124 
"sum_map f1 f2 (Inl a) = Inl (f1 a)" 

125 
 "sum_map f1 f2 (Inr a) = Inr (f2 a)" 

126 

55467
a5c9002bc54d
renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
blanchet
parents:
55442
diff
changeset

127 
functor sum_map: sum_map proof  
41372  128 
fix f g h i 
129 
show "sum_map f g \<circ> sum_map h i = sum_map (f \<circ> h) (g \<circ> i)" 

130 
proof 

131 
fix s 

132 
show "(sum_map f g \<circ> sum_map h i) s = sum_map (f \<circ> h) (g \<circ> i) s" 

133 
by (cases s) simp_all 

134 
qed 

40610  135 
next 
136 
fix s 

41372  137 
show "sum_map id id = id" 
138 
proof 

139 
fix s 

140 
show "sum_map id id s = id s" 

141 
by (cases s) simp_all 

142 
qed 

40610  143 
qed 
144 

53010  145 
lemma split_sum_all: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))" 
146 
by (auto intro: sum.induct) 

147 

148 
lemma split_sum_ex: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P (Inl x)) \<or> (\<exists>x. P (Inr x))" 

149 
using split_sum_all[of "\<lambda>x. \<not>P x"] by blast 

33961  150 

33962  151 
subsection {* Projections *} 
152 

55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55403
diff
changeset

153 
lemma case_sum_KK [simp]: "case_sum (\<lambda>x. a) (\<lambda>x. a) = (\<lambda>x. a)" 
33961  154 
by (rule ext) (simp split: sum.split) 
155 

55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55403
diff
changeset

156 
lemma surjective_sum: "case_sum (\<lambda>x::'a. f (Inl x)) (\<lambda>y::'b. f (Inr y)) = f" 
33962  157 
proof 
158 
fix s :: "'a + 'b" 

159 
show "(case s of Inl (x\<Colon>'a) \<Rightarrow> f (Inl x)  Inr (y\<Colon>'b) \<Rightarrow> f (Inr y)) = f s" 

160 
by (cases s) simp_all 

161 
qed 

33961  162 

55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55403
diff
changeset

163 
lemma case_sum_inject: 
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55403
diff
changeset

164 
assumes a: "case_sum f1 f2 = case_sum g1 g2" 
33962  165 
assumes r: "f1 = g1 \<Longrightarrow> f2 = g2 \<Longrightarrow> P" 
166 
shows P 

167 
proof (rule r) 

168 
show "f1 = g1" proof 

169 
fix x :: 'a 

55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55403
diff
changeset

170 
from a have "case_sum f1 f2 (Inl x) = case_sum g1 g2 (Inl x)" by simp 
33962  171 
then show "f1 x = g1 x" by simp 
172 
qed 

173 
show "f2 = g2" proof 

174 
fix y :: 'b 

55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55403
diff
changeset

175 
from a have "case_sum f1 f2 (Inr y) = case_sum g1 g2 (Inr y)" by simp 
33962  176 
then show "f2 y = g2 y" by simp 
177 
qed 

178 
qed 

179 

180 
primrec Suml :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where 

181 
"Suml f (Inl x) = f x" 

182 

183 
primrec Sumr :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where 

184 
"Sumr f (Inr x) = f x" 

185 

186 
lemma Suml_inject: 

187 
assumes "Suml f = Suml g" shows "f = g" 

188 
proof 

189 
fix x :: 'a 

190 
let ?s = "Inl x \<Colon> 'a + 'b" 

191 
from assms have "Suml f ?s = Suml g ?s" by simp 

192 
then show "f x = g x" by simp 

33961  193 
qed 
194 

33962  195 
lemma Sumr_inject: 
196 
assumes "Sumr f = Sumr g" shows "f = g" 

197 
proof 

198 
fix x :: 'b 

199 
let ?s = "Inr x \<Colon> 'a + 'b" 

200 
from assms have "Sumr f ?s = Sumr g ?s" by simp 

201 
then show "f x = g x" by simp 

202 
qed 

33961  203 

33995  204 

33962  205 
subsection {* The Disjoint Sum of Sets *} 
33961  206 

33962  207 
definition Plus :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a + 'b) set" (infixr "<+>" 65) where 
208 
"A <+> B = Inl ` A \<union> Inr ` B" 

209 

40271  210 
hide_const (open) Plus "Valuable identifier" 
211 

33962  212 
lemma InlI [intro!]: "a \<in> A \<Longrightarrow> Inl a \<in> A <+> B" 
213 
by (simp add: Plus_def) 

33961  214 

33962  215 
lemma InrI [intro!]: "b \<in> B \<Longrightarrow> Inr b \<in> A <+> B" 
216 
by (simp add: Plus_def) 

33961  217 

33962  218 
text {* Exhaustion rule for sums, a degenerate form of induction *} 
219 

220 
lemma PlusE [elim!]: 

221 
"u \<in> A <+> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> u = Inl x \<Longrightarrow> P) \<Longrightarrow> (\<And>y. y \<in> B \<Longrightarrow> u = Inr y \<Longrightarrow> P) \<Longrightarrow> P" 

222 
by (auto simp add: Plus_def) 

33961  223 

33962  224 
lemma Plus_eq_empty_conv [simp]: "A <+> B = {} \<longleftrightarrow> A = {} \<and> B = {}" 
225 
by auto 

33961  226 

33962  227 
lemma UNIV_Plus_UNIV [simp]: "UNIV <+> UNIV = UNIV" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

228 
proof (rule set_eqI) 
33962  229 
fix u :: "'a + 'b" 
230 
show "u \<in> UNIV <+> UNIV \<longleftrightarrow> u \<in> UNIV" by (cases u) auto 

231 
qed 

33961  232 

49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49834
diff
changeset

233 
lemma UNIV_sum: 
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49834
diff
changeset

234 
"UNIV = Inl ` UNIV \<union> Inr ` UNIV" 
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49834
diff
changeset

235 
proof  
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49834
diff
changeset

236 
{ fix x :: "'a + 'b" 
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49834
diff
changeset

237 
assume "x \<notin> range Inr" 
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49834
diff
changeset

238 
then have "x \<in> range Inl" 
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49834
diff
changeset

239 
by (cases x) simp_all 
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49834
diff
changeset

240 
} then show ?thesis by auto 
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49834
diff
changeset

241 
qed 
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49834
diff
changeset

242 

55393
ce5cebfaedda
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents:
53010
diff
changeset

243 
hide_const (open) Suml Sumr sum 
45204
5e4a1270c000
hide typedefgenerated constants Product_Type.prod and Sum_Type.sum
huffman
parents:
41505
diff
changeset

244 

10213  245 
end 