src/HOL/ex/PiSets.ML
changeset 5865 2303f5a3036d
parent 5856 5fb5a626f3b9
child 9190 b86ff604729f
equal deleted inserted replaced
5864:30b6a3251813 5865:2303f5a3036d
    83 by (rtac (PiBij_func RS f_Inv_f) 1);
    83 by (rtac (PiBij_func RS f_Inv_f) 1);
    84 by (asm_full_simp_tac (simpset() addsimps [surj_PiBij]) 1);
    84 by (asm_full_simp_tac (simpset() addsimps [surj_PiBij]) 1);
    85 by (assume_tac 1);
    85 by (assume_tac 1);
    86 qed "PiBij_bij2";
    86 qed "PiBij_bij2";
    87 
    87 
    88 Goal "Pi {} B = {f. !x. f x = (@ y. True)}";
       
    89 by (asm_full_simp_tac (simpset() addsimps [Pi_def]) 1);
       
    90 qed "empty_Pi";
       
    91 
       
    92 Goal "(% x. (@ y. True)) : Pi {} B";
       
    93 by (simp_tac (simpset() addsimps [empty_Pi]) 1);
       
    94 qed "empty_Pi_func";
       
    95 
       
    96 val [major] = Goalw [Pi_def] "(!!x. x: A ==> B x <= C x) ==> Pi A B <= Pi A C";
       
    97 by (auto_tac (claset(),
       
    98 	      simpset() addsimps [impOfSubs major]));
       
    99 qed "Pi_mono";