author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 47101  ded5cc757bc9 
child 58871  c399ae4b836f 
permissions  rwrr 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24893
diff
changeset

1 
(* Title: ZF/Perm.thy 
1478  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  3 
Copyright 1991 University of Cambridge 
4 

5 
The theory underlying permutation groups 

6 
 Composition of relations, the identity relation 

7 
 Injections, surjections, bijections 

8 
 Lemmas for the SchroederBernstein Theorem 

9 
*) 

10 

13356  11 
header{*Injections, Surjections, Bijections, Composition*} 
12 

16417  13 
theory Perm imports func begin 
0  14 

24893  15 
definition 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

16 
(*composition of relations and functions; NOT Suppes's relative product*) 
24893  17 
comp :: "[i,i]=>i" (infixr "O" 60) where 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

18 
"r O s == {xz \<in> domain(s)*range(r) . 
46820  19 
\<exists>x y z. xz=<x,z> & <x,y>:s & <y,z>:r}" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

20 

24893  21 
definition 
1806  22 
(*the identity function for A*) 
24893  23 
id :: "i=>i" where 
46820  24 
"id(A) == (\<lambda>x\<in>A. x)" 
0  25 

24893  26 
definition 
1806  27 
(*onetoone functions from A to B*) 
24893  28 
inj :: "[i,i]=>i" where 
46953  29 
"inj(A,B) == { f \<in> A>B. \<forall>w\<in>A. \<forall>x\<in>A. f`w=f`x \<longrightarrow> w=x}" 
0  30 

24893  31 
definition 
1806  32 
(*onto functions from A to B*) 
24893  33 
surj :: "[i,i]=>i" where 
46953  34 
"surj(A,B) == { f \<in> A>B . \<forall>y\<in>B. \<exists>x\<in>A. f`x=y}" 
0  35 

24893  36 
definition 
1806  37 
(*onetoone and onto functions*) 
24893  38 
bij :: "[i,i]=>i" where 
46820  39 
"bij(A,B) == inj(A,B) \<inter> surj(A,B)" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

40 

312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

41 

41160
be34449f6cba
Added two theorems about the concept of range. Tidied up the comments.
paulson
parents:
32960
diff
changeset

42 
subsection{*Surjective Function Space*} 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

43 

46953  44 
lemma surj_is_fun: "f \<in> surj(A,B) ==> f \<in> A>B" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

45 
apply (unfold surj_def) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

46 
apply (erule CollectD1) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

47 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

48 

46953  49 
lemma fun_is_surj: "f \<in> Pi(A,B) ==> f \<in> surj(A,range(f))" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

50 
apply (unfold surj_def) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

51 
apply (blast intro: apply_equality range_of_fun domain_type) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

52 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

53 

46953  54 
lemma surj_range: "f \<in> surj(A,B) ==> range(f)=B" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

55 
apply (unfold surj_def) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

56 
apply (best intro: apply_Pair elim: range_type) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

57 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

58 

41160
be34449f6cba
Added two theorems about the concept of range. Tidied up the comments.
paulson
parents:
32960
diff
changeset

59 
text{* A function with a right inverse is a surjection *} 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

60 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

61 
lemma f_imp_surjective: 
46953  62 
"[ f \<in> A>B; !!y. y \<in> B ==> d(y): A; !!y. y \<in> B ==> f`d(y) = y ] 
63 
==> f \<in> surj(A,B)" 

41160
be34449f6cba
Added two theorems about the concept of range. Tidied up the comments.
paulson
parents:
32960
diff
changeset

64 
by (simp add: surj_def, blast) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

65 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

66 
lemma lam_surjective: 
46953  67 
"[ !!x. x \<in> A ==> c(x): B; 
68 
!!y. y \<in> B ==> d(y): A; 

69 
!!y. y \<in> B ==> c(d(y)) = y 

46820  70 
] ==> (\<lambda>x\<in>A. c(x)) \<in> surj(A,B)" 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

71 
apply (rule_tac d = d in f_imp_surjective) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

72 
apply (simp_all add: lam_type) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

73 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

74 

41160
be34449f6cba
Added two theorems about the concept of range. Tidied up the comments.
paulson
parents:
32960
diff
changeset

75 
text{*Cantor's theorem revisited*} 
46820  76 
lemma cantor_surj: "f \<notin> surj(A,Pow(A))" 
13180  77 
apply (unfold surj_def, safe) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

78 
apply (cut_tac cantor) 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

79 
apply (best del: subsetI) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

80 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

81 

312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

82 

41160
be34449f6cba
Added two theorems about the concept of range. Tidied up the comments.
paulson
parents:
32960
diff
changeset

83 
subsection{*Injective Function Space*} 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

84 

46953  85 
lemma inj_is_fun: "f \<in> inj(A,B) ==> f \<in> A>B" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

86 
apply (unfold inj_def) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

87 
apply (erule CollectD1) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

88 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

89 

41160
be34449f6cba
Added two theorems about the concept of range. Tidied up the comments.
paulson
parents:
32960
diff
changeset

90 
text{*Good for dealing with sets of pairs, but a bit ugly in use [used in AC]*} 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

91 
lemma inj_equality: 
46953  92 
"[ <a,b>:f; <c,b>:f; f \<in> inj(A,B) ] ==> a=c" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

93 
apply (unfold inj_def) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

94 
apply (blast dest: Pair_mem_PiD) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

95 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

96 

46953  97 
lemma inj_apply_equality: "[ f \<in> inj(A,B); f`a=f`b; a \<in> A; b \<in> A ] ==> a=b" 
13180  98 
by (unfold inj_def, blast) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

99 

41160
be34449f6cba
Added two theorems about the concept of range. Tidied up the comments.
paulson
parents:
32960
diff
changeset

100 
text{* A function with a left inverse is an injection *} 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

101 

46953  102 
lemma f_imp_injective: "[ f \<in> A>B; \<forall>x\<in>A. d(f`x)=x ] ==> f \<in> inj(A,B)" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

103 
apply (simp (no_asm_simp) add: inj_def) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

104 
apply (blast intro: subst_context [THEN box_equals]) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

105 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

106 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

107 
lemma lam_injective: 
46953  108 
"[ !!x. x \<in> A ==> c(x): B; 
109 
!!x. x \<in> A ==> d(c(x)) = x ] 

46820  110 
==> (\<lambda>x\<in>A. c(x)) \<in> inj(A,B)" 
13784  111 
apply (rule_tac d = d in f_imp_injective) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

112 
apply (simp_all add: lam_type) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

113 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

114 

13356  115 
subsection{*Bijections*} 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

116 

46953  117 
lemma bij_is_inj: "f \<in> bij(A,B) ==> f \<in> inj(A,B)" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

118 
apply (unfold bij_def) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

119 
apply (erule IntD1) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

120 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

121 

46953  122 
lemma bij_is_surj: "f \<in> bij(A,B) ==> f \<in> surj(A,B)" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

123 
apply (unfold bij_def) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

124 
apply (erule IntD2) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

125 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

126 

46953  127 
lemma bij_is_fun: "f \<in> bij(A,B) ==> f \<in> A>B" 
128 
by (rule bij_is_inj [THEN inj_is_fun]) 

13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

129 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

130 
lemma lam_bijective: 
46953  131 
"[ !!x. x \<in> A ==> c(x): B; 
132 
!!y. y \<in> B ==> d(y): A; 

133 
!!x. x \<in> A ==> d(c(x)) = x; 

134 
!!y. y \<in> B ==> c(d(y)) = y 

46820  135 
] ==> (\<lambda>x\<in>A. c(x)) \<in> bij(A,B)" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

136 
apply (unfold bij_def) 
13180  137 
apply (blast intro!: lam_injective lam_surjective) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

138 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

139 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

140 
lemma RepFun_bijective: "(\<forall>y\<in>x. EX! y'. f(y') = f(y)) 
46953  141 
==> (\<lambda>z\<in>{f(y). y \<in> x}. THE y. f(y) = z) \<in> bij({f(y). y \<in> x}, x)" 
13784  142 
apply (rule_tac d = f in lam_bijective) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

143 
apply (auto simp add: the_equality2) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

144 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

145 

312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

146 

13356  147 
subsection{*Identity Function*} 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

148 

46953  149 
lemma idI [intro!]: "a \<in> A ==> <a,a> \<in> id(A)" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

150 
apply (unfold id_def) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

151 
apply (erule lamI) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

152 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

153 

46953  154 
lemma idE [elim!]: "[ p \<in> id(A); !!x.[ x \<in> A; p=<x,x> ] ==> P ] ==> P" 
13180  155 
by (simp add: id_def lam_def, blast) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

156 

46820  157 
lemma id_type: "id(A) \<in> A>A" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

158 
apply (unfold id_def) 
13180  159 
apply (rule lam_type, assumption) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

160 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

161 

46953  162 
lemma id_conv [simp]: "x \<in> A ==> id(A)`x = x" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

163 
apply (unfold id_def) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

164 
apply (simp (no_asm_simp)) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

165 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

166 

46820  167 
lemma id_mono: "A<=B ==> id(A) \<subseteq> id(B)" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

168 
apply (unfold id_def) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

169 
apply (erule lam_mono) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

170 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

171 

312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

172 
lemma id_subset_inj: "A<=B ==> id(A): inj(A,B)" 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

173 
apply (simp add: inj_def id_def) 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

174 
apply (blast intro: lam_type) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

175 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

176 

45602  177 
lemmas id_inj = subset_refl [THEN id_subset_inj] 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

178 

312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

179 
lemma id_surj: "id(A): surj(A,A)" 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

180 
apply (unfold id_def surj_def) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

181 
apply (simp (no_asm_simp)) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

182 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

183 

312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

184 
lemma id_bij: "id(A): bij(A,A)" 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

185 
apply (unfold bij_def) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

186 
apply (blast intro: id_inj id_surj) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

187 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

188 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

189 
lemma subset_iff_id: "A \<subseteq> B \<longleftrightarrow> id(A) \<in> A>B" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

190 
apply (unfold id_def) 
13180  191 
apply (force intro!: lam_type dest: apply_type) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

192 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

193 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
13784
diff
changeset

194 
text{*@{term id} as the identity relation*} 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

195 
lemma id_iff [simp]: "<x,y> \<in> id(A) \<longleftrightarrow> x=y & y \<in> A" 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
13784
diff
changeset

196 
by auto 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

197 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
13784
diff
changeset

198 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
13784
diff
changeset

199 
subsection{*Converse of a Function*} 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

200 

46953  201 
lemma inj_converse_fun: "f \<in> inj(A,B) ==> converse(f) \<in> range(f)>A" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

202 
apply (unfold inj_def) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

203 
apply (simp (no_asm_simp) add: Pi_iff function_def) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

204 
apply (erule CollectE) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

205 
apply (simp (no_asm_simp) add: apply_iff) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

206 
apply (blast dest: fun_is_rel) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

207 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

208 

41160
be34449f6cba
Added two theorems about the concept of range. Tidied up the comments.
paulson
parents:
32960
diff
changeset

209 
text{* Equations for converse(f) *} 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

210 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
13784
diff
changeset

211 
text{*The premises are equivalent to saying that f is injective...*} 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

212 
lemma left_inverse_lemma: 
46953  213 
"[ f \<in> A>B; converse(f): C>A; a \<in> A ] ==> converse(f)`(f`a) = a" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

214 
by (blast intro: apply_Pair apply_equality converseI) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

215 

46953  216 
lemma left_inverse [simp]: "[ f \<in> inj(A,B); a \<in> A ] ==> converse(f)`(f`a) = a" 
13180  217 
by (blast intro: left_inverse_lemma inj_converse_fun inj_is_fun) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

218 

14883  219 
lemma left_inverse_eq: 
220 
"[f \<in> inj(A,B); f ` x = y; x \<in> A] ==> converse(f) ` y = x" 

221 
by auto 

222 

45602  223 
lemmas left_inverse_bij = bij_is_inj [THEN left_inverse] 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

224 

312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

225 
lemma right_inverse_lemma: 
46953  226 
"[ f \<in> A>B; converse(f): C>A; b \<in> C ] ==> f`(converse(f)`b) = b" 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

227 
by (rule apply_Pair [THEN converseD [THEN apply_equality]], auto) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

228 

46953  229 
(*Should the premises be f \<in> surj(A,B), b \<in> B for symmetry with left_inverse? 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

230 
No: they would not imply that converse(f) was a function! *) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

231 
lemma right_inverse [simp]: 
46953  232 
"[ f \<in> inj(A,B); b \<in> range(f) ] ==> f`(converse(f)`b) = b" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

233 
by (blast intro: right_inverse_lemma inj_converse_fun inj_is_fun) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

234 

46953  235 
lemma right_inverse_bij: "[ f \<in> bij(A,B); b \<in> B ] ==> f`(converse(f)`b) = b" 
13180  236 
by (force simp add: bij_def surj_range) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

237 

13356  238 
subsection{*Converses of Injections, Surjections, Bijections*} 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

239 

46953  240 
lemma inj_converse_inj: "f \<in> inj(A,B) ==> converse(f): inj(range(f), A)" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

241 
apply (rule f_imp_injective) 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

242 
apply (erule inj_converse_fun, clarify) 
13180  243 
apply (rule right_inverse) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

244 
apply assumption 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

245 
apply blast 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

246 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

247 

46953  248 
lemma inj_converse_surj: "f \<in> inj(A,B) ==> converse(f): surj(range(f), A)" 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

249 
by (blast intro: f_imp_surjective inj_converse_fun left_inverse inj_is_fun 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

250 
range_of_fun [THEN apply_type]) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

251 

41160
be34449f6cba
Added two theorems about the concept of range. Tidied up the comments.
paulson
parents:
32960
diff
changeset

252 
text{*Adding this as an intro! rule seems to cause looping*} 
46953  253 
lemma bij_converse_bij [TC]: "f \<in> bij(A,B) ==> converse(f): bij(B,A)" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

254 
apply (unfold bij_def) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

255 
apply (fast elim: surj_range [THEN subst] inj_converse_inj inj_converse_surj) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

256 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

257 

312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

258 

312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

259 

13356  260 
subsection{*Composition of Two Relations*} 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

261 

46820  262 
text{*The inductive definition package could derive these theorems for @{term"r O s"}*} 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

263 

46820  264 
lemma compI [intro]: "[ <a,b>:s; <b,c>:r ] ==> <a,c> \<in> r O s" 
13180  265 
by (unfold comp_def, blast) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

266 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

267 
lemma compE [elim!]: 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

268 
"[ xz \<in> r O s; 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

269 
!!x y z. [ xz=<x,z>; <x,y>:s; <y,z>:r ] ==> P ] 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

270 
==> P" 
13180  271 
by (unfold comp_def, blast) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

272 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

273 
lemma compEpair: 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

274 
"[ <a,c> \<in> r O s; 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

275 
!!y. [ <a,y>:s; <y,c>:r ] ==> P ] 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

276 
==> P" 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

277 
by (erule compE, simp) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

278 

312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

279 
lemma converse_comp: "converse(R O S) = converse(S) O converse(R)" 
13180  280 
by blast 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

281 

312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

282 

13356  283 
subsection{*Domain and Range  see Suppes, Section 3.1*} 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

284 

41160
be34449f6cba
Added two theorems about the concept of range. Tidied up the comments.
paulson
parents:
32960
diff
changeset

285 
text{*Boyer et al., Set Theory in FirstOrder Logic, JAR 2 (1986), 287327*} 
46820  286 
lemma range_comp: "range(r O s) \<subseteq> range(r)" 
13180  287 
by blast 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

288 

46820  289 
lemma range_comp_eq: "domain(r) \<subseteq> range(s) ==> range(r O s) = range(r)" 
13180  290 
by (rule range_comp [THEN equalityI], blast) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

291 

46820  292 
lemma domain_comp: "domain(r O s) \<subseteq> domain(s)" 
13180  293 
by blast 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

294 

46820  295 
lemma domain_comp_eq: "range(s) \<subseteq> domain(r) ==> domain(r O s) = domain(s)" 
13180  296 
by (rule domain_comp [THEN equalityI], blast) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

297 

312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

298 
lemma image_comp: "(r O s)``A = r``(s``A)" 
13180  299 
by blast 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

300 

46953  301 
lemma inj_inj_range: "f \<in> inj(A,B) ==> f \<in> inj(A,range(f))" 
41160
be34449f6cba
Added two theorems about the concept of range. Tidied up the comments.
paulson
parents:
32960
diff
changeset

302 
by (auto simp add: inj_def Pi_iff function_def) 
be34449f6cba
Added two theorems about the concept of range. Tidied up the comments.
paulson
parents:
32960
diff
changeset

303 

46953  304 
lemma inj_bij_range: "f \<in> inj(A,B) ==> f \<in> bij(A,range(f))" 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

305 
by (auto simp add: bij_def intro: inj_inj_range inj_is_fun fun_is_surj) 
41160
be34449f6cba
Added two theorems about the concept of range. Tidied up the comments.
paulson
parents:
32960
diff
changeset

306 

13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

307 

13356  308 
subsection{*Other Results*} 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

309 

46820  310 
lemma comp_mono: "[ r'<=r; s'<=s ] ==> (r' O s') \<subseteq> (r O s)" 
13180  311 
by blast 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

312 

41160
be34449f6cba
Added two theorems about the concept of range. Tidied up the comments.
paulson
parents:
32960
diff
changeset

313 
text{*composition preserves relations*} 
46820  314 
lemma comp_rel: "[ s<=A*B; r<=B*C ] ==> (r O s) \<subseteq> A*C" 
13180  315 
by blast 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

316 

41160
be34449f6cba
Added two theorems about the concept of range. Tidied up the comments.
paulson
parents:
32960
diff
changeset

317 
text{*associative law for composition*} 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

318 
lemma comp_assoc: "(r O s) O t = r O (s O t)" 
13180  319 
by blast 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

320 

312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

321 
(*left identity of composition; provable inclusions are 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

322 
id(A) O r \<subseteq> r 
46820  323 
and [ r<=A*B; B<=C ] ==> r \<subseteq> id(C) O r *) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

324 
lemma left_comp_id: "r<=A*B ==> id(B) O r = r" 
13180  325 
by blast 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

326 

312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

327 
(*right identity of composition; provable inclusions are 
46820  328 
r O id(A) \<subseteq> r 
329 
and [ r<=A*B; A<=C ] ==> r \<subseteq> r O id(C) *) 

13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

330 
lemma right_comp_id: "r<=A*B ==> r O id(A) = r" 
13180  331 
by blast 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

332 

312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

333 

13356  334 
subsection{*Composition Preserves Functions, Injections, and Surjections*} 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

335 

13180  336 
lemma comp_function: "[ function(g); function(f) ] ==> function(f O g)" 
337 
by (unfold function_def, blast) 

13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

338 

41160
be34449f6cba
Added two theorems about the concept of range. Tidied up the comments.
paulson
parents:
32960
diff
changeset

339 
text{*Don't think the premises can be weakened much*} 
46953  340 
lemma comp_fun: "[ g \<in> A>B; f \<in> B>C ] ==> (f O g) \<in> A>C" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

341 
apply (auto simp add: Pi_def comp_function Pow_iff comp_rel) 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

342 
apply (subst range_rel_subset [THEN domain_comp_eq], auto) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

343 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

344 

46953  345 
(*Thanks to the new definition of "apply", the premise f \<in> B>C is gone!*) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

346 
lemma comp_fun_apply [simp]: 
46953  347 
"[ g \<in> A>B; a \<in> A ] ==> (f O g)`a = f`(g`a)" 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

348 
apply (frule apply_Pair, assumption) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

349 
apply (simp add: apply_def image_comp) 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

350 
apply (blast dest: apply_equality) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

351 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

352 

41160
be34449f6cba
Added two theorems about the concept of range. Tidied up the comments.
paulson
parents:
32960
diff
changeset

353 
text{*Simplifies compositions of lambdaabstractions*} 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

354 
lemma comp_lam: 
46953  355 
"[ !!x. x \<in> A ==> b(x): B ] 
46820  356 
==> (\<lambda>y\<in>B. c(y)) O (\<lambda>x\<in>A. b(x)) = (\<lambda>x\<in>A. c(b(x)))" 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

357 
apply (subgoal_tac "(\<lambda>x\<in>A. b(x)) \<in> A > B") 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

358 
apply (rule fun_extension) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

359 
apply (blast intro: comp_fun lam_funtype) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

360 
apply (rule lam_funtype) 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

361 
apply simp 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

362 
apply (simp add: lam_type) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

363 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

364 

312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

365 
lemma comp_inj: 
46953  366 
"[ g \<in> inj(A,B); f \<in> inj(B,C) ] ==> (f O g) \<in> inj(A,C)" 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

367 
apply (frule inj_is_fun [of g]) 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

368 
apply (frule inj_is_fun [of f]) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

369 
apply (rule_tac d = "%y. converse (g) ` (converse (f) ` y)" in f_imp_injective) 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

370 
apply (blast intro: comp_fun, simp) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

371 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

372 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

373 
lemma comp_surj: 
46953  374 
"[ g \<in> surj(A,B); f \<in> surj(B,C) ] ==> (f O g) \<in> surj(A,C)" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

375 
apply (unfold surj_def) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

376 
apply (blast intro!: comp_fun comp_fun_apply) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

377 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

378 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

379 
lemma comp_bij: 
46953  380 
"[ g \<in> bij(A,B); f \<in> bij(B,C) ] ==> (f O g) \<in> bij(A,C)" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

381 
apply (unfold bij_def) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

382 
apply (blast intro: comp_inj comp_surj) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

383 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

384 

312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

385 

13356  386 
subsection{*Dual Properties of @{term inj} and @{term surj}*} 
387 

388 
text{*Useful for proofs from 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

389 
D Pastre. Automatic theorem proving in set theory. 
13356  390 
Artificial Intelligence, 10:127, 1978.*} 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

391 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

392 
lemma comp_mem_injD1: 
46953  393 
"[ (f O g): inj(A,C); g \<in> A>B; f \<in> B>C ] ==> g \<in> inj(A,B)" 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

394 
by (unfold inj_def, force) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

395 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

396 
lemma comp_mem_injD2: 
46953  397 
"[ (f O g): inj(A,C); g \<in> surj(A,B); f \<in> B>C ] ==> f \<in> inj(B,C)" 
13180  398 
apply (unfold inj_def surj_def, safe) 
13784  399 
apply (rule_tac x1 = x in bspec [THEN bexE]) 
400 
apply (erule_tac [3] x1 = w in bspec [THEN bexE], assumption+, safe) 

13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

401 
apply (rule_tac t = "op ` (g) " in subst_context) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

402 
apply (erule asm_rl bspec [THEN bspec, THEN mp])+ 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

403 
apply (simp (no_asm_simp)) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

404 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

405 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

406 
lemma comp_mem_surjD1: 
46953  407 
"[ (f O g): surj(A,C); g \<in> A>B; f \<in> B>C ] ==> f \<in> surj(B,C)" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

408 
apply (unfold surj_def) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

409 
apply (blast intro!: comp_fun_apply [symmetric] apply_funtype) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

410 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

411 

312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

412 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

413 
lemma comp_mem_surjD2: 
46953  414 
"[ (f O g): surj(A,C); g \<in> A>B; f \<in> inj(B,C) ] ==> g \<in> surj(A,B)" 
13180  415 
apply (unfold inj_def surj_def, safe) 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

416 
apply (drule_tac x = "f`y" in bspec, auto) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

417 
apply (blast intro: apply_funtype) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

418 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

419 

13356  420 
subsubsection{*Inverses of Composition*} 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

421 

41160
be34449f6cba
Added two theorems about the concept of range. Tidied up the comments.
paulson
parents:
32960
diff
changeset

422 
text{*left inverse of composition; one inclusion is 
46953  423 
@{term "f \<in> A>B ==> id(A) \<subseteq> converse(f) O f"} *} 
424 
lemma left_comp_inverse: "f \<in> inj(A,B) ==> converse(f) O f = id(A)" 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

425 
apply (unfold inj_def, clarify) 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

426 
apply (rule equalityI) 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

427 
apply (auto simp add: apply_iff, blast) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

428 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

429 

41160
be34449f6cba
Added two theorems about the concept of range. Tidied up the comments.
paulson
parents:
32960
diff
changeset

430 
text{*right inverse of composition; one inclusion is 
46953  431 
@{term "f \<in> A>B ==> f O converse(f) \<subseteq> id(B)"} *} 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

432 
lemma right_comp_inverse: 
46953  433 
"f \<in> surj(A,B) ==> f O converse(f) = id(B)" 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

434 
apply (simp add: surj_def, clarify) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

435 
apply (rule equalityI) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

436 
apply (best elim: domain_type range_type dest: apply_equality2) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

437 
apply (blast intro: apply_Pair) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

438 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

439 

312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

440 

13356  441 
subsubsection{*Proving that a Function is a Bijection*} 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

442 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

443 
lemma comp_eq_id_iff: 
46953  444 
"[ f \<in> A>B; g \<in> B>A ] ==> f O g = id(B) \<longleftrightarrow> (\<forall>y\<in>B. f`(g`y)=y)" 
13180  445 
apply (unfold id_def, safe) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

446 
apply (drule_tac t = "%h. h`y " in subst_context) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

447 
apply simp 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

448 
apply (rule fun_extension) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

449 
apply (blast intro: comp_fun lam_type) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

450 
apply auto 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

451 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

452 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

453 
lemma fg_imp_bijective: 
46953  454 
"[ f \<in> A>B; g \<in> B>A; f O g = id(B); g O f = id(A) ] ==> f \<in> bij(A,B)" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

455 
apply (unfold bij_def) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

456 
apply (simp add: comp_eq_id_iff) 
13180  457 
apply (blast intro: f_imp_injective f_imp_surjective apply_funtype) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

458 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

459 

46953  460 
lemma nilpotent_imp_bijective: "[ f \<in> A>A; f O f = id(A) ] ==> f \<in> bij(A,A)" 
13180  461 
by (blast intro: fg_imp_bijective) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

462 

13180  463 
lemma invertible_imp_bijective: 
46953  464 
"[ converse(f): B>A; f \<in> A>B ] ==> f \<in> bij(A,B)" 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

465 
by (simp add: fg_imp_bijective comp_eq_id_iff 
13180  466 
left_inverse_lemma right_inverse_lemma) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

467 

13356  468 
subsubsection{*Unions of Functions*} 
469 

470 
text{*See similar theorems in func.thy*} 

13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

471 

41160
be34449f6cba
Added two theorems about the concept of range. Tidied up the comments.
paulson
parents:
32960
diff
changeset

472 
text{*Theorem by KG, proof by LCP*} 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

473 
lemma inj_disjoint_Un: 
46953  474 
"[ f \<in> inj(A,B); g \<in> inj(C,D); B \<inter> D = 0 ] 
475 
==> (\<lambda>a\<in>A \<union> C. if a \<in> A then f`a else g`a) \<in> inj(A \<union> C, B \<union> D)" 

476 
apply (rule_tac d = "%z. if z \<in> B then converse (f) `z else converse (g) `z" 

13180  477 
in lam_injective) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

478 
apply (auto simp add: inj_is_fun [THEN apply_type]) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

479 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

480 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

481 
lemma surj_disjoint_Un: 
46953  482 
"[ f \<in> surj(A,B); g \<in> surj(C,D); A \<inter> C = 0 ] 
46820  483 
==> (f \<union> g) \<in> surj(A \<union> C, B \<union> D)" 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

484 
apply (simp add: surj_def fun_disjoint_Un) 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

485 
apply (blast dest!: domain_of_fun 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24893
diff
changeset

486 
intro!: fun_disjoint_apply1 fun_disjoint_apply2) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

487 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

488 

41160
be34449f6cba
Added two theorems about the concept of range. Tidied up the comments.
paulson
parents:
32960
diff
changeset

489 
text{*A simple, highlevel proof; the version for injections follows from it, 
46953  490 
using @{term "f \<in> inj(A,B) \<longleftrightarrow> f \<in> bij(A,range(f))"} *} 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

491 
lemma bij_disjoint_Un: 
46953  492 
"[ f \<in> bij(A,B); g \<in> bij(C,D); A \<inter> C = 0; B \<inter> D = 0 ] 
46820  493 
==> (f \<union> g) \<in> bij(A \<union> C, B \<union> D)" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

494 
apply (rule invertible_imp_bijective) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

495 
apply (subst converse_Un) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

496 
apply (auto intro: fun_disjoint_Un bij_is_fun bij_converse_bij) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

497 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

498 

312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

499 

13356  500 
subsubsection{*Restrictions as Surjections and Bijections*} 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

501 

312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

502 
lemma surj_image: 
46953  503 
"f \<in> Pi(A,B) ==> f \<in> surj(A, f``A)" 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

504 
apply (simp add: surj_def) 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

505 
apply (blast intro: apply_equality apply_Pair Pi_type) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

506 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

507 

47101  508 
lemma surj_image_eq: "f \<in> surj(A, B) ==> f``A = B" 
509 
by (auto simp add: surj_def image_fun) (blast dest: apply_type) 

510 

46820  511 
lemma restrict_image [simp]: "restrict(f,A) `` B = f `` (A \<inter> B)" 
13180  512 
by (auto simp add: restrict_def) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

513 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

514 
lemma restrict_inj: 
46953  515 
"[ f \<in> inj(A,B); C<=A ] ==> restrict(f,C): inj(C,B)" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

516 
apply (unfold inj_def) 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

517 
apply (safe elim!: restrict_type2, auto) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

518 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

519 

46953  520 
lemma restrict_surj: "[ f \<in> Pi(A,B); C<=A ] ==> restrict(f,C): surj(C, f``C)" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

521 
apply (insert restrict_type2 [THEN surj_image]) 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

522 
apply (simp add: restrict_image) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

523 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

524 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

525 
lemma restrict_bij: 
46953  526 
"[ f \<in> inj(A,B); C<=A ] ==> restrict(f,C): bij(C, f``C)" 
13180  527 
apply (simp add: inj_def bij_def) 
528 
apply (blast intro: restrict_surj surj_is_fun) 

13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

529 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

530 

312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

531 

13356  532 
subsubsection{*Lemmas for Ramsey's Theorem*} 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

533 

46953  534 
lemma inj_weaken_type: "[ f \<in> inj(A,B); B<=D ] ==> f \<in> inj(A,D)" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

535 
apply (unfold inj_def) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

536 
apply (blast intro: fun_weaken_type) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

537 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

538 

312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

539 
lemma inj_succ_restrict: 
46953  540 
"[ f \<in> inj(succ(m), A) ] ==> restrict(f,m) \<in> inj(m, A{f`m})" 
13269  541 
apply (rule restrict_bij [THEN bij_is_inj, THEN inj_weaken_type], assumption, blast) 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

542 
apply (unfold inj_def) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

543 
apply (fast elim: range_type mem_irrefl dest: apply_equality) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

544 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

545 

312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

546 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

547 
lemma inj_extend: 
46953  548 
"[ f \<in> inj(A,B); a\<notin>A; b\<notin>B ] 
46820  549 
==> cons(<a,b>,f) \<in> inj(cons(a,A), cons(b,B))" 
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

550 
apply (unfold inj_def) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

551 
apply (force intro: apply_type simp add: fun_extend) 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

552 
done 
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset

553 

0  554 
end 