635 by (asm_simp_tac |
635 by (asm_simp_tac |
636 (simpset() addsimps [restrict_apply1, compose_def, Inv_f_f]) 1); |
636 (simpset() addsimps [restrict_apply1, compose_def, Inv_f_f]) 1); |
637 qed "compose_Inv_id"; |
637 qed "compose_Inv_id"; |
638 |
638 |
639 |
639 |
640 (*** Pi and Applyall ***) |
640 (*** Pi ***) |
641 |
641 |
642 Goalw [Pi_def] "[| B(x) = {}; x: A |] ==> (PI x: A. B x) = {}"; |
642 Goalw [Pi_def] "[| B(x) = {}; x: A |] ==> (PI x: A. B x) = {}"; |
643 by Auto_tac; |
643 by Auto_tac; |
644 qed "Pi_eq_empty"; |
644 qed "Pi_eq_empty"; |
645 |
645 |
646 Goal "[| (PI x: A. B x) ~= {}; x: A |] ==> B(x) ~= {}"; |
646 Goal "[| (PI x: A. B x) ~= {}; x: A |] ==> B(x) ~= {}"; |
647 by (blast_tac (HOL_cs addIs [Pi_eq_empty]) 1); |
647 by (blast_tac (HOL_cs addIs [Pi_eq_empty]) 1); |
648 qed "Pi_total1"; |
648 qed "Pi_total1"; |
649 |
649 |
650 Goal "[| a : A; Pi A B ~= {} |] ==> Applyall (Pi A B) a = B a"; |
650 Goal "Pi {} B = { %x. @y. True }"; |
651 by (auto_tac (claset(), simpset() addsimps [Applyall_def, Pi_def])); |
|
652 by (rename_tac "g z" 1); |
|
653 by (res_inst_tac [("x","%y. if (y = a) then z else g y")] exI 1); |
|
654 by (auto_tac (claset(), simpset() addsimps [split_if_mem1, split_if_eq1])); |
|
655 qed "Applyall_beta"; |
|
656 |
|
657 Goal "Pi {} B = { (%x. @ y. True) }"; |
|
658 by (auto_tac (claset() addIs [ext], simpset() addsimps [Pi_def])); |
651 by (auto_tac (claset() addIs [ext], simpset() addsimps [Pi_def])); |
659 qed "Pi_empty"; |
652 qed "Pi_empty"; |
660 |
653 |
661 val [major] = Goalw [Pi_def] "(!!x. x: A ==> B x <= C x) ==> Pi A B <= Pi A C"; |
654 val [major] = Goalw [Pi_def] "(!!x. x: A ==> B x <= C x) ==> Pi A B <= Pi A C"; |
662 by (auto_tac (claset(), |
655 by (auto_tac (claset(), |