src/ZF/OrderArith.ML
changeset 835 313ac9b513f1
parent 815 de2d8a63256d
child 859 bc5f424c8c04
equal deleted inserted replaced
834:ad1d0eb0ee82 835:313ac9b513f1
   202 by (rtac Collect_subset 1);
   202 by (rtac Collect_subset 1);
   203 qed "rvimage_type";
   203 qed "rvimage_type";
   204 
   204 
   205 bind_thm ("field_rvimage", (rvimage_type RS field_rel_subset));
   205 bind_thm ("field_rvimage", (rvimage_type RS field_rel_subset));
   206 
   206 
       
   207 goalw OrderArith.thy [rvimage_def] 
       
   208     "rvimage(A,f, converse(r)) = converse(rvimage(A,f,r))";
       
   209 by (fast_tac eq_cs 1);
       
   210 qed "rvimage_converse";
       
   211 
       
   212 
       
   213 (** Partial Ordering Properties **)
       
   214 
       
   215 goalw OrderArith.thy [irrefl_def, rvimage_def]
       
   216     "!!A B. [| f: inj(A,B);  irrefl(B,r) |] ==> irrefl(A, rvimage(A,f,r))";
       
   217 by (fast_tac (ZF_cs addIs [inj_is_fun RS apply_type]) 1);
       
   218 qed "irrefl_rvimage";
       
   219 
       
   220 goalw OrderArith.thy [trans_on_def, rvimage_def] 
       
   221     "!!A B. [| f: inj(A,B);  trans[B](r) |] ==> trans[A](rvimage(A,f,r))";
       
   222 by (fast_tac (ZF_cs addIs [inj_is_fun RS apply_type]) 1);
       
   223 qed "trans_on_rvimage";
       
   224 
       
   225 goalw OrderArith.thy [part_ord_def]
       
   226     "!!A B. [| f: inj(A,B);  part_ord(B,r) |] ==> part_ord(A, rvimage(A,f,r))";
       
   227 by (fast_tac (ZF_cs addSIs [irrefl_rvimage, trans_on_rvimage]) 1);
       
   228 qed "part_ord_rvimage";
   207 
   229 
   208 (** Linearity **)
   230 (** Linearity **)
   209 
   231 
   210 val [finj,lin] = goalw OrderArith.thy [inj_def]
   232 val [finj,lin] = goalw OrderArith.thy [inj_def]
   211     "[| f: inj(A,B);  linear(B,r) |] ==> linear(A,rvimage(A,f,r))";
   233     "[| f: inj(A,B);  linear(B,r) |] ==> linear(A,rvimage(A,f,r))";
   215 by (cut_facts_tac [finj] 1);
   237 by (cut_facts_tac [finj] 1);
   216 by (res_inst_tac [("x","f`x"), ("y","f`y")] (lin RS linearE) 1);
   238 by (res_inst_tac [("x","f`x"), ("y","f`y")] (lin RS linearE) 1);
   217 by (REPEAT_SOME (fast_tac (ZF_cs addSIs [apply_type])));
   239 by (REPEAT_SOME (fast_tac (ZF_cs addSIs [apply_type])));
   218 qed "linear_rvimage";
   240 qed "linear_rvimage";
   219 
   241 
       
   242 goalw OrderArith.thy [tot_ord_def] 
       
   243     "!!A B. [| f: inj(A,B);  tot_ord(B,r) |] ==> tot_ord(A, rvimage(A,f,r))";
       
   244 by (fast_tac (ZF_cs addSIs [part_ord_rvimage, linear_rvimage]) 1);
       
   245 qed "tot_ord_rvimage";
       
   246 
   220 
   247 
   221 (** Well-foundedness **)
   248 (** Well-foundedness **)
   222 
   249 
   223 goal OrderArith.thy
   250 goal OrderArith.thy
   224     "!!r. [| f: A->B;  wf[B](r) |] ==> wf[A](rvimage(A,f,r))";
   251     "!!r. [| f: A->B;  wf[B](r) |] ==> wf[A](rvimage(A,f,r))";
   228 by (eres_inst_tac [("a","f`y")] wf_on_induct 1);
   255 by (eres_inst_tac [("a","f`y")] wf_on_induct 1);
   229 by (fast_tac (ZF_cs addSIs [apply_type]) 1);
   256 by (fast_tac (ZF_cs addSIs [apply_type]) 1);
   230 by (best_tac (ZF_cs addSIs [apply_type] addSDs [rvimage_iff RS iffD1]) 1);
   257 by (best_tac (ZF_cs addSIs [apply_type] addSDs [rvimage_iff RS iffD1]) 1);
   231 qed "wf_on_rvimage";
   258 qed "wf_on_rvimage";
   232 
   259 
       
   260 (*Note that we need only wf[A](...) and linear(A,...) to get the result!*)
   233 goal OrderArith.thy 
   261 goal OrderArith.thy 
   234     "!!r. [| f: inj(A,B);  well_ord(B,r) |] ==> well_ord(A, rvimage(A,f,r))";
   262     "!!r. [| f: inj(A,B);  well_ord(B,r) |] ==> well_ord(A, rvimage(A,f,r))";
   235 by (rtac well_ordI 1);
   263 by (rtac well_ordI 1);
   236 by (rewrite_goals_tac [well_ord_def, tot_ord_def]);
   264 by (rewrite_goals_tac [well_ord_def, tot_ord_def]);
   237 by (fast_tac (ZF_cs addSIs [wf_on_rvimage, inj_is_fun]) 1);
   265 by (fast_tac (ZF_cs addSIs [wf_on_rvimage, inj_is_fun]) 1);
   240 
   268 
   241 goalw OrderArith.thy [ord_iso_def]
   269 goalw OrderArith.thy [ord_iso_def]
   242     "!!A B. f: bij(A,B) ==> f: ord_iso(A, rvimage(A,f,s), B, s)";
   270     "!!A B. f: bij(A,B) ==> f: ord_iso(A, rvimage(A,f,s), B, s)";
   243 by (asm_full_simp_tac (ZF_ss addsimps [rvimage_iff]) 1);
   271 by (asm_full_simp_tac (ZF_ss addsimps [rvimage_iff]) 1);
   244 qed "ord_iso_rvimage";
   272 qed "ord_iso_rvimage";
       
   273 
       
   274 goalw OrderArith.thy [ord_iso_def, rvimage_def]
       
   275     "!!A B. f: ord_iso(A,r, B,s) ==> rvimage(A,f,s) = r Int A*A";
       
   276 by (fast_tac eq_cs 1);
       
   277 qed "ord_iso_rvimage_eq";