doc-src/Logics/ZF-eg.txt
author paulson
Fri Feb 16 18:00:47 1996 +0100 (1996-02-16)
changeset 1512 ce37c64244c0
parent 115 745affa0262b
child 5151 1e944fe5ce96
permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
lcp@104
     1
(**** ZF examples ****)
lcp@104
     2
lcp@104
     3
Pretty.setmargin 72;  (*existing macros just allow this margin*)
lcp@104
     4
print_depth 0;
lcp@104
     5
lcp@104
     6
(*** Powerset example ***)
lcp@104
     7
lcp@115
     8
val [prem] = goal ZF.thy "A<=B  ==>  Pow(A) <= Pow(B)";
lcp@104
     9
by (resolve_tac [subsetI] 1);
lcp@104
    10
by (resolve_tac [PowI] 1);
lcp@104
    11
by (dresolve_tac [PowD] 1);
lcp@104
    12
by (eresolve_tac [subset_trans] 1);
lcp@104
    13
by (resolve_tac [prem] 1);
lcp@104
    14
val Pow_mono = result();
lcp@104
    15
lcp@115
    16
goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)";
lcp@104
    17
by (resolve_tac [equalityI] 1);
lcp@104
    18
by (resolve_tac [Int_greatest] 1);
lcp@104
    19
by (resolve_tac [Int_lower1 RS Pow_mono] 1);
lcp@104
    20
by (resolve_tac [Int_lower2 RS Pow_mono] 1);
lcp@104
    21
by (resolve_tac [subsetI] 1);
lcp@104
    22
by (eresolve_tac [IntE] 1);
lcp@104
    23
by (resolve_tac [PowI] 1);
lcp@104
    24
by (REPEAT (dresolve_tac [PowD] 1));
lcp@104
    25
by (resolve_tac [Int_greatest] 1);
lcp@104
    26
by (REPEAT (assume_tac 1));
lcp@104
    27
choplev 0;
lcp@104
    28
by (fast_tac (ZF_cs addIs [equalityI]) 1);
lcp@104
    29
lcp@115
    30
val [prem] = goal ZF.thy "C<=D ==> Union(C) <= Union(D)";
lcp@104
    31
by (resolve_tac [subsetI] 1);
lcp@104
    32
by (eresolve_tac [UnionE] 1);
lcp@104
    33
by (resolve_tac [UnionI] 1);
lcp@104
    34
by (resolve_tac [prem RS subsetD] 1);
lcp@104
    35
by (assume_tac 1);
lcp@104
    36
by (assume_tac 1);
lcp@104
    37
choplev 0;
lcp@104
    38
by (resolve_tac [Union_least] 1);
lcp@104
    39
by (resolve_tac [Union_upper] 1);
lcp@104
    40
by (eresolve_tac [prem RS subsetD] 1);
lcp@104
    41
lcp@104
    42
lcp@115
    43
val prems = goal ZF.thy
lcp@104
    44
    "[| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
lcp@104
    45
\    (f Un g)`a = f`a";
lcp@104
    46
by (resolve_tac [apply_equality] 1);
lcp@104
    47
by (resolve_tac [UnI1] 1);
lcp@104
    48
by (resolve_tac [apply_Pair] 1);
lcp@104
    49
by (resolve_tac prems 1);
lcp@104
    50
by (resolve_tac prems 1);
lcp@104
    51
by (resolve_tac [fun_disjoint_Un] 1);
lcp@104
    52
by (resolve_tac prems 1);
lcp@104
    53
by (resolve_tac prems 1);
lcp@104
    54
by (resolve_tac prems 1);
lcp@104
    55
lcp@104
    56
lcp@104
    57
lcp@104
    58
lcp@115
    59
goal ZF.thy "f``(UN x:A. B(x)) = (UN x:A. f``B(x))";
lcp@104
    60
by (resolve_tac [equalityI] 1);
lcp@104
    61
by (resolve_tac [subsetI] 1);
lcp@104
    62
fe imageE;
lcp@104
    63
lcp@104
    64
lcp@115
    65
goal ZF.thy "(UN x:C. A(x) Int B) = (UN x:C. A(x))  Int  B";
lcp@104
    66
by (resolve_tac [equalityI] 1);
lcp@104
    67
by (resolve_tac [Int_greatest] 1);
lcp@104
    68
fr UN_mono;
lcp@104
    69
by (resolve_tac [Int_lower1] 1);
lcp@104
    70
fr UN_least;
lcp@104
    71
????
lcp@104
    72
lcp@104
    73
lcp@115
    74
> goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)";
lcp@104
    75
Level 0
lcp@104
    76
Pow(A Int B) = Pow(A) Int Pow(B)
lcp@104
    77
 1. Pow(A Int B) = Pow(A) Int Pow(B)
lcp@104
    78
> by (resolve_tac [equalityI] 1);
lcp@104
    79
Level 1
lcp@104
    80
Pow(A Int B) = Pow(A) Int Pow(B)
lcp@104
    81
 1. Pow(A Int B) <= Pow(A) Int Pow(B)
lcp@104
    82
 2. Pow(A) Int Pow(B) <= Pow(A Int B)
lcp@104
    83
> by (resolve_tac [Int_greatest] 1);
lcp@104
    84
Level 2
lcp@104
    85
Pow(A Int B) = Pow(A) Int Pow(B)
lcp@104
    86
 1. Pow(A Int B) <= Pow(A)
lcp@104
    87
 2. Pow(A Int B) <= Pow(B)
lcp@104
    88
 3. Pow(A) Int Pow(B) <= Pow(A Int B)
lcp@104
    89
> by (resolve_tac [Int_lower1 RS Pow_mono] 1);
lcp@104
    90
Level 3
lcp@104
    91
Pow(A Int B) = Pow(A) Int Pow(B)
lcp@104
    92
 1. Pow(A Int B) <= Pow(B)
lcp@104
    93
 2. Pow(A) Int Pow(B) <= Pow(A Int B)
lcp@104
    94
> by (resolve_tac [Int_lower2 RS Pow_mono] 1);
lcp@104
    95
Level 4
lcp@104
    96
Pow(A Int B) = Pow(A) Int Pow(B)
lcp@104
    97
 1. Pow(A) Int Pow(B) <= Pow(A Int B)
lcp@104
    98
> by (resolve_tac [subsetI] 1);
lcp@104
    99
Level 5
lcp@104
   100
Pow(A Int B) = Pow(A) Int Pow(B)
lcp@104
   101
 1. !!x. x : Pow(A) Int Pow(B) ==> x : Pow(A Int B)
lcp@104
   102
> by (eresolve_tac [IntE] 1);
lcp@104
   103
Level 6
lcp@104
   104
Pow(A Int B) = Pow(A) Int Pow(B)
lcp@104
   105
 1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x : Pow(A Int B)
lcp@104
   106
> by (resolve_tac [PowI] 1);
lcp@104
   107
Level 7
lcp@104
   108
Pow(A Int B) = Pow(A) Int Pow(B)
lcp@104
   109
 1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x <= A Int B
lcp@104
   110
> by (REPEAT (dresolve_tac [PowD] 1));
lcp@104
   111
Level 8
lcp@104
   112
Pow(A Int B) = Pow(A) Int Pow(B)
lcp@104
   113
 1. !!x. [| x <= A; x <= B |] ==> x <= A Int B
lcp@104
   114
> by (resolve_tac [Int_greatest] 1);
lcp@104
   115
Level 9
lcp@104
   116
Pow(A Int B) = Pow(A) Int Pow(B)
lcp@104
   117
 1. !!x. [| x <= A; x <= B |] ==> x <= A
lcp@104
   118
 2. !!x. [| x <= A; x <= B |] ==> x <= B
lcp@104
   119
> by (REPEAT (assume_tac 1));
lcp@104
   120
Level 10
lcp@104
   121
Pow(A Int B) = Pow(A) Int Pow(B)
lcp@104
   122
No subgoals!
lcp@104
   123
> choplev 0;
lcp@104
   124
Level 0
lcp@104
   125
Pow(A Int B) = Pow(A) Int Pow(B)
lcp@104
   126
 1. Pow(A Int B) = Pow(A) Int Pow(B)
lcp@104
   127
> by (fast_tac (ZF_cs addIs [equalityI]) 1);
lcp@104
   128
Level 1
lcp@104
   129
Pow(A Int B) = Pow(A) Int Pow(B)
lcp@104
   130
No subgoals!
lcp@104
   131
lcp@104
   132
lcp@104
   133
lcp@104
   134
lcp@115
   135
> val [prem] = goal ZF.thy "C<=D ==> Union(C) <= Union(D)";
lcp@104
   136
Level 0
lcp@104
   137
Union(C) <= Union(D)
lcp@104
   138
 1. Union(C) <= Union(D)
lcp@104
   139
> by (resolve_tac [subsetI] 1);
lcp@104
   140
Level 1
lcp@104
   141
Union(C) <= Union(D)
lcp@104
   142
 1. !!x. x : Union(C) ==> x : Union(D)
lcp@104
   143
> by (eresolve_tac [UnionE] 1);
lcp@104
   144
Level 2
lcp@104
   145
Union(C) <= Union(D)
lcp@104
   146
 1. !!x B. [| x : B; B : C |] ==> x : Union(D)
lcp@104
   147
> by (resolve_tac [UnionI] 1);
lcp@104
   148
Level 3
lcp@104
   149
Union(C) <= Union(D)
lcp@104
   150
 1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : D
lcp@104
   151
 2. !!x B. [| x : B; B : C |] ==> x : ?B2(x,B)
lcp@104
   152
> by (resolve_tac [prem RS subsetD] 1);
lcp@104
   153
Level 4
lcp@104
   154
Union(C) <= Union(D)
lcp@104
   155
 1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : C
lcp@104
   156
 2. !!x B. [| x : B; B : C |] ==> x : ?B2(x,B)
lcp@104
   157
> by (assume_tac 1);
lcp@104
   158
Level 5
lcp@104
   159
Union(C) <= Union(D)
lcp@104
   160
 1. !!x B. [| x : B; B : C |] ==> x : B
lcp@104
   161
> by (assume_tac 1);
lcp@104
   162
Level 6
lcp@104
   163
Union(C) <= Union(D)
lcp@104
   164
No subgoals!
lcp@104
   165
lcp@104
   166
lcp@104
   167
lcp@115
   168
> val prems = goal ZF.thy
lcp@104
   169
#     "[| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
lcp@104
   170
# \    (f Un g)`a = f`a";
lcp@104
   171
Level 0
lcp@104
   172
(f Un g) ` a = f ` a
lcp@104
   173
 1. (f Un g) ` a = f ` a
lcp@104
   174
> by (resolve_tac [apply_equality] 1);
lcp@104
   175
Level 1
lcp@104
   176
(f Un g) ` a = f ` a
lcp@104
   177
 1. <a,f ` a> : f Un g
lcp@104
   178
 2. f Un g : (PROD x:?A. ?B(x))
lcp@104
   179
> by (resolve_tac [UnI1] 1);
lcp@104
   180
Level 2
lcp@104
   181
(f Un g) ` a = f ` a
lcp@104
   182
 1. <a,f ` a> : f
lcp@104
   183
 2. f Un g : (PROD x:?A. ?B(x))
lcp@104
   184
> by (resolve_tac [apply_Pair] 1);
lcp@104
   185
Level 3
lcp@104
   186
(f Un g) ` a = f ` a
lcp@104
   187
 1. f : (PROD x:?A2. ?B2(x))
lcp@104
   188
 2. a : ?A2
lcp@104
   189
 3. f Un g : (PROD x:?A. ?B(x))
lcp@104
   190
> by (resolve_tac prems 1);
lcp@104
   191
Level 4
lcp@104
   192
(f Un g) ` a = f ` a
lcp@104
   193
 1. a : A
lcp@104
   194
 2. f Un g : (PROD x:?A. ?B(x))
lcp@104
   195
> by (resolve_tac prems 1);
lcp@104
   196
Level 5
lcp@104
   197
(f Un g) ` a = f ` a
lcp@104
   198
 1. f Un g : (PROD x:?A. ?B(x))
lcp@104
   199
> by (resolve_tac [fun_disjoint_Un] 1);
lcp@104
   200
Level 6
lcp@104
   201
(f Un g) ` a = f ` a
lcp@104
   202
 1. f : ?A3 -> ?B3
lcp@104
   203
 2. g : ?C3 -> ?D3
lcp@104
   204
 3. ?A3 Int ?C3 = 0
lcp@104
   205
> by (resolve_tac prems 1);
lcp@104
   206
Level 7
lcp@104
   207
(f Un g) ` a = f ` a
lcp@104
   208
 1. g : ?C3 -> ?D3
lcp@104
   209
 2. A Int ?C3 = 0
lcp@104
   210
> by (resolve_tac prems 1);
lcp@104
   211
Level 8
lcp@104
   212
(f Un g) ` a = f ` a
lcp@104
   213
 1. A Int C = 0
lcp@104
   214
> by (resolve_tac prems 1);
lcp@104
   215
Level 9
lcp@104
   216
(f Un g) ` a = f ` a
lcp@104
   217
No subgoals!