src/ZF/AC.ML
 changeset 1461 6bcb44e4d6e5 parent 1074 d60f203eeddf child 2469 b50b8c0eec01
equal inserted replaced
1460:5a6f2aabd538 1461:6bcb44e4d6e5
`     1 (*  Title: 	ZF/AC.ML`
`     1 (*  Title:      ZF/AC.ML`
`     2     ID:         \$Id\$`
`     2     ID:         \$Id\$`
`     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory`
`     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory`
`     4     Copyright   1994  University of Cambridge`
`     4     Copyright   1994  University of Cambridge`
`     5 `
`     5 `
`     6 For AC.thy.  The Axiom of Choice`
`     6 For AC.thy.  The Axiom of Choice`
`     7 *)`
`     7 *)`
`     8 `
`     8 `
`    17 by (fast_tac (eq_cs addIs [AC, nonempty]) 1);`
`    17 by (fast_tac (eq_cs addIs [AC, nonempty]) 1);`
`    18 qed "AC_Pi";`
`    18 qed "AC_Pi";`
`    19 `
`    19 `
`    20 (*Using dtac, this has the advantage of DELETING the universal quantifier*)`
`    20 (*Using dtac, this has the advantage of DELETING the universal quantifier*)`
`    21 goal AC.thy "!!A B. ALL x:A. EX y. y:B(x) ==> EX y. y : Pi(A,B)";`
`    21 goal AC.thy "!!A B. ALL x:A. EX y. y:B(x) ==> EX y. y : Pi(A,B)";`
`    22 by (resolve_tac [AC_Pi] 1);`
`    22 by (rtac AC_Pi 1);`
`    23 by (eresolve_tac [bspec] 1);`
`    23 by (etac bspec 1);`
`    24 by (assume_tac 1);`
`    24 by (assume_tac 1);`
`    25 qed "AC_ball_Pi";`
`    25 qed "AC_ball_Pi";`
`    26 `
`    26 `
`    27 goal AC.thy "EX f. f: (PROD X: Pow(C)-{0}. X)";`
`    27 goal AC.thy "EX f. f: (PROD X: Pow(C)-{0}. X)";`
`    28 by (res_inst_tac [("B1", "%x.x")] (AC_Pi RS exE) 1);`
`    28 by (res_inst_tac [("B1", "%x.x")] (AC_Pi RS exE) 1);`
`    29 by (etac exI 2);`
`    29 by (etac exI 2);`
`    30 by (fast_tac eq_cs 1);`
`    30 by (fast_tac eq_cs 1);`
`    31 qed "AC_Pi_Pow";`
`    31 qed "AC_Pi_Pow";`
`    32 `
`    32 `
`    33 val [nonempty] = goal AC.thy`
`    33 val [nonempty] = goal AC.thy`
`    34      "[| !!x. x:A ==> (EX y. y:x)	\`
`    34      "[| !!x. x:A ==> (EX y. y:x)       \`
`    35 \     |] ==> EX f: A->Union(A). ALL x:A. f`x : x";`
`    35 \     |] ==> EX f: A->Union(A). ALL x:A. f`x : x";`
`    36 by (res_inst_tac [("B1", "%x.x")] (AC_Pi RS exE) 1);`
`    36 by (res_inst_tac [("B1", "%x.x")] (AC_Pi RS exE) 1);`
`    37 by (etac nonempty 1);`
`    37 by (etac nonempty 1);`
`    38 by (fast_tac (ZF_cs addDs [apply_type] addIs [Pi_type]) 1);`
`    38 by (fast_tac (ZF_cs addDs [apply_type] addIs [Pi_type]) 1);`
`    39 qed "AC_func";`
`    39 qed "AC_func";`
`    50 `
`    50 `
`    51 goal AC.thy "EX f: (Pow(C)-{0}) -> C. ALL x:(Pow(C)-{0}). f`x : x";`
`    51 goal AC.thy "EX f: (Pow(C)-{0}) -> C. ALL x:(Pow(C)-{0}). f`x : x";`
`    52 by (resolve_tac [AC_func0 RS bexE] 1);`
`    52 by (resolve_tac [AC_func0 RS bexE] 1);`
`    53 by (rtac bexI 2);`
`    53 by (rtac bexI 2);`
`    54 by (assume_tac 2);`
`    54 by (assume_tac 2);`
`    55 by (eresolve_tac [fun_weaken_type] 2);`
`    55 by (etac fun_weaken_type 2);`
`    56 by (ALLGOALS (fast_tac ZF_cs));`
`    56 by (ALLGOALS (fast_tac ZF_cs));`
`    57 qed "AC_func_Pow";`
`    57 qed "AC_func_Pow";`
`    58 `
`    58 `
`    59 goal AC.thy "!!A. 0 ~: A ==> EX f. f: (PROD x:A. x)";`
`    59 goal AC.thy "!!A. 0 ~: A ==> EX f. f: (PROD x:A. x)";`
`    60 by (rtac AC_Pi 1);`
`    60 by (rtac AC_Pi 1);`