5250

1 
(* Title: HOL/ex/PiSets.thy


2 
ID: $Id$


3 
Author: Florian Kammueller, University of Cambridge


4 


5 
Pi sets and their application.


6 
*)


7 

5845

8 
(*** > and Pi ***)

5250

9 


10 

5845

11 
val prems = Goalw [Pi_def]


12 
"[ !!x. x: A ==> f x: B x; !!x. x ~: A ==> f(x) = (@ y. True)] \


13 
\ ==> f: Pi A B";


14 
by (auto_tac (claset(), simpset() addsimps prems));


15 
qed "Pi_I";


16 


17 
val prems = Goal


18 
"[ !!x. x: A ==> f x: B; !!x. x ~: A ==> f(x) = (@ y. True)] ==> f: A > B";


19 
by (blast_tac (claset() addIs Pi_I::prems) 1);


20 
qed "funcsetI";

5250

21 

5845

22 
Goalw [Pi_def] "[f: Pi A B; x: A] ==> f x: B x";


23 
by Auto_tac;


24 
qed "Pi_mem";


25 


26 
Goalw [Pi_def] "[f: A > B; x: A] ==> f x: B";


27 
by Auto_tac;


28 
qed "funcset_mem";


29 


30 
Goalw [Pi_def] "[f: Pi A B; x~: A] ==> f x = (@ y. True)";


31 
by Auto_tac;


32 
qed "apply_arb";

5250

33 

5845

34 
Goalw [Pi_def] "[ f: Pi A B; g: Pi A B; ! x: A. f x = g x ] ==> f = g";


35 
by (rtac ext 1);


36 
by Auto_tac;


37 
val Pi_extensionality = ballI RSN (3, result());

5250

38 

5845

39 
(*** compose ***)


40 


41 
Goalw [Pi_def, compose_def, restrict_def]


42 
"[ f: A > B; g: B > C ]==> compose A g f: A > C";


43 
by Auto_tac;


44 
qed "funcset_compose";

5250

45 

5845

46 
Goal "[ f: A > B; g: B > C; h: C > D ]\


47 
\ ==> compose A h (compose A g f) = compose A (compose B h g) f";


48 
by (res_inst_tac [("A","A")] Pi_extensionality 1);


49 
by (blast_tac (claset() addIs [funcset_compose]) 1);


50 
by (blast_tac (claset() addIs [funcset_compose]) 1);


51 
by (rewrite_goals_tac [Pi_def, compose_def, restrict_def]);


52 
by Auto_tac;


53 
qed "compose_assoc";

5250

54 

5845

55 
Goal "[ f: A > B; g: B > C; x: A ]==> compose A g f x = g(f(x))";


56 
by (asm_full_simp_tac (simpset() addsimps [compose_def, restrict_def]) 1);


57 
qed "compose_eq";

5250

58 

5845

59 
Goal "[ f : A > B; f `` A = B; g: B > C; g `` B = C ]\


60 
\ ==> compose A g f `` A = C";


61 
by (auto_tac (claset(),


62 
simpset() addsimps [image_def, compose_eq]));


63 
qed "surj_compose";

5250

64 


65 

5845

66 
Goal "[ f : A > B; g: B > C; f `` A = B; inj_on f A; inj_on g B ]\


67 
\ ==> inj_on (compose A g f) A";


68 
by (auto_tac (claset(),


69 
simpset() addsimps [inj_on_def, compose_eq]));


70 
qed "inj_on_compose";

5250

71 


72 

5845

73 
(*** restrict / lam ***)


74 
Goal "[ f `` A <= B ] ==> (lam x: A. f x) : A > B";


75 
by (auto_tac (claset(),


76 
simpset() addsimps [restrict_def, Pi_def]));


77 
qed "restrict_in_funcset";


78 


79 
val prems = Goalw [restrict_def, Pi_def]


80 
"(!!x. x: A ==> f x: B x) ==> (lam x: A. f x) : Pi A B";


81 
by (asm_simp_tac (simpset() addsimps prems) 1);


82 
qed "restrictI";

5250

83 


84 

5845

85 
Goal "x: A ==> (lam y: A. f y) x = f x";


86 
by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);


87 
qed "restrict_apply1";

5250

88 

5845

89 
Goal "[ x: A; f : A > B ] ==> (lam y: A. f y) x : B";


90 
by (asm_full_simp_tac (simpset() addsimps [restrict_apply1,Pi_def]) 1);


91 
qed "restrict_apply1_mem";

5250

92 

5845

93 
Goal "x ~: A ==> (lam y: A. f y) x = (@ y. True)";


94 
by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);


95 
qed "restrict_apply2";

5250

96 


97 

5845

98 
val prems = Goal


99 
"(!!x. x: A ==> f x = g x) ==> (lam x: A. f x) = (lam x: A. g x)";


100 
by (rtac ext 1);


101 
by (auto_tac (claset(),


102 
simpset() addsimps prems@[restrict_def, Pi_def]));


103 
qed "restrict_ext";

5250

104 


105 

5845

106 
(*** Inverse ***)

5250

107 

5845

108 
Goal "[f `` A = B; x: B ] ==> ? y: A. f y = x";


109 
by (Blast_tac 1);


110 
qed "surj_image";

5250

111 

5845

112 
Goalw [Inv_def] "[ f `` A = B; f : A > B ] \


113 
\ ==> (lam x: B. (Inv A f) x) : B > A";


114 
by (fast_tac (claset() addIs [restrict_in_funcset, selectI2]) 1);


115 
qed "Inv_funcset";

5250

116 


117 

5845

118 
Goal "[ f: A > B; inj_on f A; f `` A = B; x: A ] \


119 
\ ==> (lam y: B. (Inv A f) y) (f x) = x";


120 
by (asm_simp_tac (simpset() addsimps [restrict_apply1, funcset_mem]) 1);


121 
by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1);


122 
by (rtac selectI2 1);


123 
by Auto_tac;


124 
qed "Inv_f_f";

5250

125 

5845

126 
Goal "[ f: A > B; f `` A = B; x: B ] \


127 
\ ==> f ((lam y: B. (Inv A f y)) x) = x";


128 
by (asm_simp_tac (simpset() addsimps [Inv_def, restrict_apply1]) 1);


129 
by (fast_tac (claset() addIs [selectI2]) 1);


130 
qed "f_Inv_f";

5250

131 

5845

132 
Goal "[ f: A > B; inj_on f A; f `` A = B ]\


133 
\ ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)";


134 
by (rtac Pi_extensionality 1);


135 
by (blast_tac (claset() addIs [funcset_compose, Inv_funcset]) 1);


136 
by (blast_tac (claset() addIs [restrict_in_funcset]) 1);


137 
by (asm_simp_tac


138 
(simpset() addsimps [restrict_apply1, compose_def, Inv_f_f]) 1);


139 
qed "compose_Inv_id";

5250

140 


141 

5845

142 
(*** Pi and its application @@ ***)

5250

143 

5845

144 
Goalw [Pi_def] "[ B(x) = {}; x: A ] ==> (PI x: A. B x) = {}";


145 
by Auto_tac;


146 
qed "Pi_eq_empty";

5250

147 

5845

148 
Goal "[ (PI x: A. B x) ~= {}; x: A ] ==> B(x) ~= {}";


149 
by (blast_tac (HOL_cs addIs [Pi_eq_empty]) 1);


150 
qed "Pi_total1";

5250

151 

5845

152 
Goal "[ a : A; Pi A B ~= {} ] ==> (Pi A B) @@ a = B(a)";


153 
by (auto_tac (claset(), simpset() addsimps [Fset_apply_def, Pi_def]));


154 
by (rename_tac "g z" 1);


155 
by (res_inst_tac [("x","%y. if (y = a) then z else g y")] exI 1);


156 
by (auto_tac (claset(), simpset() addsimps [split_if_mem1, split_if_eq1]));


157 
qed "Fset_beta";


158 

5250

159 

5845

160 
(*** Bijection between Pi in terms of => and Pi in terms of Sigma ***)


161 
Goal "f: Pi A B ==> PiBij A B f <= Sigma A B";


162 
by (auto_tac (claset(),


163 
simpset() addsimps [PiBij_def,Pi_def,restrict_apply1]));


164 
qed "PiBij_subset_Sigma";

5250

165 

5845

166 
Goal "f: Pi A B ==> (! x: A. (?! y. (x, y): (PiBij A B f)))";


167 
by (auto_tac (claset(),


168 
simpset() addsimps [PiBij_def,restrict_apply1]));


169 
qed "PiBij_unique";

5250

170 

5845

171 
Goal "f: Pi A B ==> PiBij A B f : Graph A B";


172 
by (asm_simp_tac (simpset() addsimps [Graph_def,PiBij_unique,


173 
PiBij_subset_Sigma]) 1);


174 
qed "PiBij_in_Graph";

5250

175 

5845

176 
Goalw [PiBij_def, Graph_def] "PiBij A B: Pi A B > Graph A B";

5318

177 
by (rtac restrictI 1);

5845

178 
by (auto_tac (claset(), simpset() addsimps [Pi_def]));


179 
qed "PiBij_func";

5250

180 

5845

181 
Goal "inj_on (PiBij A B) (Pi A B)";

5318

182 
by (rtac inj_onI 1);


183 
by (rtac Pi_extensionality 1);


184 
by (assume_tac 1);


185 
by (assume_tac 1);

5845

186 
by (rotate_tac 1 1);


187 
by (asm_full_simp_tac (simpset() addsimps [PiBij_def,restrict_apply1]) 1);


188 
by (blast_tac (claset() addEs [equalityE]) 1);


189 
qed "inj_PiBij";

5250

190 

5845

191 

5250

192 

5845

193 
Goal "PiBij A B `` (Pi A B) = Graph A B";

5318

194 
by (rtac equalityI 1);

5521

195 
by (force_tac (claset(), simpset() addsimps [image_def,PiBij_in_Graph]) 1);

5318

196 
by (rtac subsetI 1);

5845

197 
by (asm_full_simp_tac (simpset() addsimps [image_def]) 1);

5250

198 
by (res_inst_tac [("x","lam a: A. @ y. (a, y): x")] bexI 1);

5845

199 
by (rtac restrictI 2);


200 
by (res_inst_tac [("P", "%xa. (a, xa) : x")] ex1E 2);


201 
by (force_tac (claset(), simpset() addsimps [Graph_def]) 2);


202 
by (full_simp_tac (simpset() addsimps [Graph_def]) 2);


203 
by (stac select_equality 2);

5521

204 
by (assume_tac 2);


205 
by (Blast_tac 2);


206 
by (Blast_tac 2);

5250

207 
(* x = PiBij A B (lam a:A. @ y. (a, y) : x) *)

5845

208 
by (full_simp_tac (simpset() addsimps [PiBij_def,Graph_def]) 1);


209 
by (stac restrict_apply1 1);


210 
by (rtac restrictI 1);


211 
by (blast_tac (claset() addSDs [[select_eq_Ex, ex1_implies_ex] MRS iffD2]) 1);


212 
(** LEVEL 17 **)

5318

213 
by (rtac equalityI 1);


214 
by (rtac subsetI 1);

5845

215 
by (split_all_tac 1);


216 
by (subgoal_tac "a: A" 1);


217 
by (Blast_tac 2);


218 
by (asm_full_simp_tac (simpset() addsimps [restrict_apply1]) 1);


219 
(*Blast_tac: PROOF FAILED for depth 5*)


220 
by (fast_tac (claset() addSIs [select1_equality RS sym]) 1);

5250

221 
(* {(xa,y). xa : A & y = (lam a:A. @ y. (a, y) : x) xa} <= x *)

5845

222 
by (Clarify_tac 1);


223 
by (asm_full_simp_tac (simpset() addsimps [restrict_apply1]) 1);


224 
by (fast_tac (claset() addIs [selectI2]) 1);


225 
qed "surj_PiBij";

5250

226 

5845

227 
Goal "f: Pi A B ==> \


228 
\ (lam y: Graph A B. (Inv (Pi A B)(PiBij A B)) y)(PiBij A B f) = f";


229 
by (asm_simp_tac


230 
(simpset() addsimps [Inv_f_f, PiBij_func, inj_PiBij, surj_PiBij]) 1);


231 
qed "PiBij_bij1";

5250

232 

5845

233 
Goal "[ f: Graph A B ] ==> \

5250

234 
\ (PiBij A B) ((lam y: (Graph A B). (Inv (Pi A B)(PiBij A B)) y) f) = f";

5845

235 
by (rtac (PiBij_func RS f_Inv_f) 1);


236 
by (asm_full_simp_tac (simpset() addsimps [surj_PiBij]) 1);

5318

237 
by (assume_tac 1);

5845

238 
qed "PiBij_bij2";

5250

239 

5845

240 
Goal "Pi {} B = {f. !x. f x = (@ y. True)}";


241 
by (asm_full_simp_tac (simpset() addsimps [Pi_def]) 1);


242 
qed "empty_Pi";

5250

243 

5845

244 
Goal "(% x. (@ y. True)) : Pi {} B";


245 
by (simp_tac (simpset() addsimps [empty_Pi]) 1);


246 
qed "empty_Pi_func";

5250

247 

5845

248 
val [major] = Goalw [Pi_def] "(!!x. x: A ==> B x <= C x) ==> Pi A B <= Pi A C";


249 
by (auto_tac (claset(),


250 
simpset() addsimps [impOfSubs major]));


251 
qed "Pi_mono";
