(**** 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. <a,f ` a> : 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. <a,f ` a> : 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!