(**** ZF examples ****) Pretty.setmargin 72; (*existing macros just allow this margin*) print_depth 0; (*** Powerset example ***) val [prem] = goal ZF.thy "A<=B ==> Pow(A) <= Pow(B)"; by (resolve_tac [subsetI] 1); by (resolve_tac [PowI] 1); by (dresolve_tac [PowD] 1); by (eresolve_tac [subset_trans] 1); by (resolve_tac [prem] 1); val Pow_mono = result(); goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)"; by (resolve_tac [equalityI] 1); by (resolve_tac [Int_greatest] 1); by (resolve_tac [Int_lower1 RS Pow_mono] 1); by (resolve_tac [Int_lower2 RS Pow_mono] 1); by (resolve_tac [subsetI] 1); by (eresolve_tac [IntE] 1); by (resolve_tac [PowI] 1); by (REPEAT (dresolve_tac [PowD] 1)); by (resolve_tac [Int_greatest] 1); by (REPEAT (assume_tac 1)); choplev 0; by (fast_tac (ZF_cs addIs [equalityI]) 1); Goal "C<=D ==> Union(C) <= Union(D)"; by (resolve_tac [subsetI] 1); by (eresolve_tac [UnionE] 1); by (resolve_tac [UnionI] 1); by (eresolve_tac [subsetD] 1); by (assume_tac 1); by (assume_tac 1); choplev 0; by (resolve_tac [Union_least] 1); by (resolve_tac [Union_upper] 1); by (eresolve_tac [subsetD] 1); val prems = goal ZF.thy "[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \ \ (f Un g)`a = f`a"; by (resolve_tac [apply_equality] 1); by (resolve_tac [UnI1] 1); by (resolve_tac [apply_Pair] 1); by (resolve_tac prems 1); by (resolve_tac prems 1); by (resolve_tac [fun_disjoint_Un] 1); by (resolve_tac prems 1); by (resolve_tac prems 1); by (resolve_tac prems 1); Goal "[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \ \ (f Un g)`a = f`a"; by (resolve_tac [apply_equality] 1); by (resolve_tac [UnI1] 1); by (resolve_tac [apply_Pair] 1); by (assume_tac 1); by (assume_tac 1); by (resolve_tac [fun_disjoint_Un] 1); by (assume_tac 1); by (assume_tac 1); by (assume_tac 1); goal ZF.thy "f``(UN x:A. B(x)) = (UN x:A. f``B(x))"; by (resolve_tac [equalityI] 1); by (resolve_tac [subsetI] 1); fe imageE; goal ZF.thy "(UN x:C. A(x) Int B) = (UN x:C. A(x)) Int B"; by (resolve_tac [equalityI] 1); by (resolve_tac [Int_greatest] 1); fr UN_mono; by (resolve_tac [Int_lower1] 1); fr UN_least; ???? > goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)"; Level 0 Pow(A Int B) = Pow(A) Int Pow(B) 1. Pow(A Int B) = Pow(A) Int Pow(B) > by (resolve_tac [equalityI] 1); Level 1 Pow(A Int B) = Pow(A) Int Pow(B) 1. Pow(A Int B) <= Pow(A) Int Pow(B) 2. Pow(A) Int Pow(B) <= Pow(A Int B) > by (resolve_tac [Int_greatest] 1); Level 2 Pow(A Int B) = Pow(A) Int Pow(B) 1. Pow(A Int B) <= Pow(A) 2. Pow(A Int B) <= Pow(B) 3. Pow(A) Int Pow(B) <= Pow(A Int B) > by (resolve_tac [Int_lower1 RS Pow_mono] 1); Level 3 Pow(A Int B) = Pow(A) Int Pow(B) 1. Pow(A Int B) <= Pow(B) 2. Pow(A) Int Pow(B) <= Pow(A Int B) > by (resolve_tac [Int_lower2 RS Pow_mono] 1); Level 4 Pow(A Int B) = Pow(A) Int Pow(B) 1. Pow(A) Int Pow(B) <= Pow(A Int B) > by (resolve_tac [subsetI] 1); Level 5 Pow(A Int B) = Pow(A) Int Pow(B) 1. !!x. x : Pow(A) Int Pow(B) ==> x : Pow(A Int B) > by (eresolve_tac [IntE] 1); Level 6 Pow(A Int B) = Pow(A) Int Pow(B) 1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x : Pow(A Int B) > by (resolve_tac [PowI] 1); Level 7 Pow(A Int B) = Pow(A) Int Pow(B) 1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x <= A Int B > by (REPEAT (dresolve_tac [PowD] 1)); Level 8 Pow(A Int B) = Pow(A) Int Pow(B) 1. !!x. [| x <= A; x <= B |] ==> x <= A Int B > by (resolve_tac [Int_greatest] 1); Level 9 Pow(A Int B) = Pow(A) Int Pow(B) 1. !!x. [| x <= A; x <= B |] ==> x <= A 2. !!x. [| x <= A; x <= B |] ==> x <= B > by (REPEAT (assume_tac 1)); Level 10 Pow(A Int B) = Pow(A) Int Pow(B) No subgoals! > choplev 0; Level 0 Pow(A Int B) = Pow(A) Int Pow(B) 1. Pow(A Int B) = Pow(A) Int Pow(B) > by (fast_tac (ZF_cs addIs [equalityI]) 1); Level 1 Pow(A Int B) = Pow(A) Int Pow(B) No subgoals! > val [prem] = goal ZF.thy "C<=D ==> Union(C) <= Union(D)"; Level 0 Union(C) <= Union(D) 1. Union(C) <= Union(D) > by (resolve_tac [subsetI] 1); Level 1 Union(C) <= Union(D) 1. !!x. x : Union(C) ==> x : Union(D) > by (eresolve_tac [UnionE] 1); Level 2 Union(C) <= Union(D) 1. !!x B. [| x : B; B : C |] ==> x : Union(D) > by (resolve_tac [UnionI] 1); Level 3 Union(C) <= Union(D) 1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : D 2. !!x B. [| x : B; B : C |] ==> x : ?B2(x,B) > by (resolve_tac [prem RS subsetD] 1); Level 4 Union(C) <= Union(D) 1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : C 2. !!x B. [| x : B; B : C |] ==> x : ?B2(x,B) > by (assume_tac 1); Level 5 Union(C) <= Union(D) 1. !!x B. [| x : B; B : C |] ==> x : B > by (assume_tac 1); Level 6 Union(C) <= Union(D) No subgoals! > val prems = goal ZF.thy # "[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \ # \ (f Un g)`a = f`a"; Level 0 (f Un g) ` a = f ` a 1. (f Un g) ` a = f ` a > by (resolve_tac [apply_equality] 1); Level 1 (f Un g) ` a = f ` a 1. : f Un g 2. f Un g : (PROD x:?A. ?B(x)) > by (resolve_tac [UnI1] 1); Level 2 (f Un g) ` a = f ` a 1. : f 2. f Un g : (PROD x:?A. ?B(x)) > by (resolve_tac [apply_Pair] 1); Level 3 (f Un g) ` a = f ` a 1. f : (PROD x:?A2. ?B2(x)) 2. a : ?A2 3. f Un g : (PROD x:?A. ?B(x)) > by (resolve_tac prems 1); Level 4 (f Un g) ` a = f ` a 1. a : A 2. f Un g : (PROD x:?A. ?B(x)) > by (resolve_tac prems 1); Level 5 (f Un g) ` a = f ` a 1. f Un g : (PROD x:?A. ?B(x)) > by (resolve_tac [fun_disjoint_Un] 1); Level 6 (f Un g) ` a = f ` a 1. f : ?A3 -> ?B3 2. g : ?C3 -> ?D3 3. ?A3 Int ?C3 = 0 > by (resolve_tac prems 1); Level 7 (f Un g) ` a = f ` a 1. g : ?C3 -> ?D3 2. A Int ?C3 = 0 > by (resolve_tac prems 1); Level 8 (f Un g) ` a = f ` a 1. A Int C = 0 > by (resolve_tac prems 1); Level 9 (f Un g) ` a = f ` a No subgoals!