387 by (etac (major RS apply_rangeI) 1); |
387 by (etac (major RS apply_rangeI) 1); |
388 qed "range_of_fun"; |
388 qed "range_of_fun"; |
389 |
389 |
390 (*** Extensions of functions ***) |
390 (*** Extensions of functions ***) |
391 |
391 |
392 goal ZF.thy |
392 Goal "[| f: A->B; c~:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)"; |
393 "!!f A B. [| f: A->B; c~:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)"; |
|
394 by (forward_tac [singleton_fun RS fun_disjoint_Un] 1); |
393 by (forward_tac [singleton_fun RS fun_disjoint_Un] 1); |
395 by (asm_full_simp_tac (FOL_ss addsimps [cons_eq]) 2); |
394 by (asm_full_simp_tac (FOL_ss addsimps [cons_eq]) 2); |
396 by (Blast_tac 1); |
395 by (Blast_tac 1); |
397 qed "fun_extend"; |
396 qed "fun_extend"; |
398 |
397 |
399 goal ZF.thy |
398 Goal "[| f: A->B; c~:A; b: B |] ==> cons(<c,b>,f) : cons(c,A) -> B"; |
400 "!!f A B. [| f: A->B; c~:A; b: B |] ==> cons(<c,b>,f) : cons(c,A) -> B"; |
|
401 by (blast_tac (claset() addIs [fun_extend RS fun_weaken_type]) 1); |
399 by (blast_tac (claset() addIs [fun_extend RS fun_weaken_type]) 1); |
402 qed "fun_extend3"; |
400 qed "fun_extend3"; |
403 |
401 |
404 goal ZF.thy "!!f A B. [| f: A->B; a:A; c~:A |] ==> cons(<c,b>,f)`a = f`a"; |
402 Goal "[| f: A->B; a:A; c~:A |] ==> cons(<c,b>,f)`a = f`a"; |
405 by (rtac (apply_Pair RS consI2 RS apply_equality) 1); |
403 by (rtac (apply_Pair RS consI2 RS apply_equality) 1); |
406 by (rtac fun_extend 3); |
404 by (rtac fun_extend 3); |
407 by (REPEAT (assume_tac 1)); |
405 by (REPEAT (assume_tac 1)); |
408 qed "fun_extend_apply1"; |
406 qed "fun_extend_apply1"; |
409 |
407 |
410 goal ZF.thy "!!f A B. [| f: A->B; c~:A |] ==> cons(<c,b>,f)`c = b"; |
408 Goal "[| f: A->B; c~:A |] ==> cons(<c,b>,f)`c = b"; |
411 by (rtac (consI1 RS apply_equality) 1); |
409 by (rtac (consI1 RS apply_equality) 1); |
412 by (rtac fun_extend 1); |
410 by (rtac fun_extend 1); |
413 by (REPEAT (assume_tac 1)); |
411 by (REPEAT (assume_tac 1)); |
414 qed "fun_extend_apply2"; |
412 qed "fun_extend_apply2"; |
415 |
413 |
416 bind_thm ("singleton_apply", [singletonI, singleton_fun] MRS apply_equality); |
414 bind_thm ("singleton_apply", [singletonI, singleton_fun] MRS apply_equality); |
417 Addsimps [singleton_apply]; |
415 Addsimps [singleton_apply]; |
418 |
416 |
419 (*For Finite.ML. Inclusion of right into left is easy*) |
417 (*For Finite.ML. Inclusion of right into left is easy*) |
420 goal ZF.thy |
418 Goal "c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})"; |
421 "!!c. c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})"; |
|
422 by (rtac equalityI 1); |
419 by (rtac equalityI 1); |
423 by (safe_tac (claset() addSEs [fun_extend3])); |
420 by (safe_tac (claset() addSEs [fun_extend3])); |
424 (*Inclusion of left into right*) |
421 (*Inclusion of left into right*) |
425 by (subgoal_tac "restrict(x, A) : A -> B" 1); |
422 by (subgoal_tac "restrict(x, A) : A -> B" 1); |
426 by (blast_tac (claset() addIs [restrict_type2]) 2); |
423 by (blast_tac (claset() addIs [restrict_type2]) 2); |