src/ZF/ex/misc.ML
author paulson
Mon, 02 Feb 1998 12:57:20 +0100
changeset 4595 fa8cee619732
parent 4477 b3e5857d8d99
child 5068 fb28eaa07e01
permissions -rw-r--r--
New example, Pow_Sigma_bij
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1110
diff changeset
     1
(*  Title:      ZF/ex/misc
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1110
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Miscellaneous examples for Zermelo-Fraenkel Set Theory 
1646
f48fafc18a88 updated comments
paulson
parents: 1461
diff changeset
     7
Composition of homomorphisms, Pastre's examples, ...
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
writeln"ZF/ex/misc";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
3000
7ecb8b6a3d7f Moved blast_tac demo from ZF/func.ML to ZF/ex/misc.ML
paulson
parents: 2496
diff changeset
    12
(*Nice Blast_tac benchmark.  Proved in 0.3s; old tactics can't manage it!*)
7ecb8b6a3d7f Moved blast_tac demo from ZF/func.ML to ZF/ex/misc.ML
paulson
parents: 2496
diff changeset
    13
goal ZF.thy "!!S. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
7ecb8b6a3d7f Moved blast_tac demo from ZF/func.ML to ZF/ex/misc.ML
paulson
parents: 2496
diff changeset
    14
by (Blast_tac 1);
7ecb8b6a3d7f Moved blast_tac demo from ZF/func.ML to ZF/ex/misc.ML
paulson
parents: 2496
diff changeset
    15
result();
7ecb8b6a3d7f Moved blast_tac demo from ZF/func.ML to ZF/ex/misc.ML
paulson
parents: 2496
diff changeset
    16
4322
5f5df208b0e0 New example
paulson
parents: 4152
diff changeset
    17
(*variant of the benchmark above*)
5f5df208b0e0 New example
paulson
parents: 4152
diff changeset
    18
goal ZF.thy "!!S. ALL x:S. Union(S) <= x ==> EX z. S <= {z}";
5f5df208b0e0 New example
paulson
parents: 4152
diff changeset
    19
by (Blast_tac 1);
5f5df208b0e0 New example
paulson
parents: 4152
diff changeset
    20
result();
5f5df208b0e0 New example
paulson
parents: 4152
diff changeset
    21
4109
b131edcfeac3 isatool fixclasimp;
wenzelm
parents: 4091
diff changeset
    22
context Perm.thy;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
(*Example 12 (credited to Peter Andrews) from
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
 W. Bledsoe.  A Maximal Method for Set Variables in Automatic Theorem-proving.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
 In: J. Hayes and D. Michie and L. Mikulich, eds.  Machine Intelligence 9.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
 Ellis Horwood, 53-100 (1979). *)
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1782
diff changeset
    28
goal thy "(ALL F. {x}: F --> {y}:F) --> (ALL A. x:A --> y:A)";
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1782
diff changeset
    29
by (Best_tac 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
(*** Composition of homomorphisms is a homomorphism ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
(*Given as a challenge problem in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
  R. Boyer et al.,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
  Set Theory in First-Order Logic: Clauses for G\"odel's Axioms,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
  JAR 2 (1986), 287-327 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
7
268f93ab3bc4 Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents: 0
diff changeset
    41
(*collecting the relevant lemmas*)
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1782
diff changeset
    42
Addsimps [comp_fun, SigmaI, apply_funtype];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
736
a8d1758bb113 moved Cantors theorem to ZF/ZF.ML and ZF/Perm.ML
lcp
parents: 695
diff changeset
    44
(*This version uses a super application of simp_tac.  Needs setloop to help
a8d1758bb113 moved Cantors theorem to ZF/ZF.ML and ZF/Perm.ML
lcp
parents: 695
diff changeset
    45
  proving conditions of rewrites such as comp_fun_apply;
a8d1758bb113 moved Cantors theorem to ZF/ZF.ML and ZF/Perm.ML
lcp
parents: 695
diff changeset
    46
  rewriting does not instantiate Vars*)
7
268f93ab3bc4 Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents: 0
diff changeset
    47
goal Perm.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
    "(ALL A f B g. hom(A,f,B,g) = \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
\          {H: A->B. f:A*A->A & g:B*B->B & \
7
268f93ab3bc4 Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents: 0
diff changeset
    50
\                    (ALL x:A. ALL y:A. H`(f`<x,y>) = g`<H`x,H`y>)}) --> \
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
\    J : hom(A,f,B,g) & K : hom(B,g,C,h) -->  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
\    (K O J) : hom(A,f,C,h)";
4152
451104c223e2 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4109
diff changeset
    53
by (asm_simp_tac (simpset() setloop (K Safe_tac)) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
val comp_homs = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
7
268f93ab3bc4 Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents: 0
diff changeset
    56
(*This version uses meta-level rewriting, safe_tac and asm_simp_tac*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
val [hom_def] = goal Perm.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
    "(!! A f B g. hom(A,f,B,g) == \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
\          {H: A->B. f:A*A->A & g:B*B->B & \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
\                    (ALL x:A. ALL y:A. H`(f`<x,y>) = g`<H`x,H`y>)}) ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
\    J : hom(A,f,B,g) & K : hom(B,g,C,h) -->  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
\    (K O J) : hom(A,f,C,h)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
by (rewtac hom_def);
4152
451104c223e2 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4109
diff changeset
    64
by Safe_tac;
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1782
diff changeset
    65
by (Asm_simp_tac 1);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1782
diff changeset
    66
by (Asm_simp_tac 1);
782
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 736
diff changeset
    67
qed "comp_homs";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
(** A characterization of functions, suggested by Tobias Nipkow **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1782
diff changeset
    72
goalw thy [Pi_def, function_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
    "r: domain(r)->B  <->  r <= domain(r)*B & (ALL X. r `` (r -`` X) <= X)";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1782
diff changeset
    74
by (Best_tac 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
(**** From D Pastre.  Automatic theorem proving in set theory. 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
         Artificial Intelligence, 10:1--27, 1978.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
             These examples require forward reasoning! ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
(*reduce the clauses to units by type checking -- beware of nontermination*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
fun forw_typechk tyrls [] = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
  | forw_typechk tyrls clauses =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
    let val (units, others) = partition (has_fewer_prems 1) clauses
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
    in  gen_union eq_thm (units, forw_typechk tyrls (tyrls RL others))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
    end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
(*A crude form of forward reasoning*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
fun forw_iterate tyrls rls facts 0 = facts
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
  | forw_iterate tyrls rls facts n =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
      let val facts' = 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1110
diff changeset
    93
          gen_union eq_thm (forw_typechk (tyrls@facts) (facts RL rls), facts);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
      in  forw_iterate tyrls rls facts' (n-1)  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
val pastre_rls =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
    [comp_mem_injD1, comp_mem_surjD1, comp_mem_injD2, comp_mem_surjD2];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
fun pastre_facts (fact1::fact2::fact3::prems) = 
434
89d45187f04d Various updates and tidying
lcp
parents: 38
diff changeset
   100
    forw_iterate (prems @ [comp_surj, comp_inj, comp_fun])
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
               pastre_rls [fact1,fact2,fact3] 4;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
val prems = goalw Perm.thy [bij_def]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1110
diff changeset
   104
    "[| (h O g O f): inj(A,A);          \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1110
diff changeset
   105
\       (f O h O g): surj(B,B);         \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1110
diff changeset
   106
\       (g O f O h): surj(C,C);         \
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
782
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 736
diff changeset
   109
qed "pastre1";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
val prems = goalw Perm.thy [bij_def]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1110
diff changeset
   112
    "[| (h O g O f): surj(A,A);         \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1110
diff changeset
   113
\       (f O h O g): inj(B,B);          \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1110
diff changeset
   114
\       (g O f O h): surj(C,C);         \
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
782
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 736
diff changeset
   117
qed "pastre2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
val prems = goalw Perm.thy [bij_def]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1110
diff changeset
   120
    "[| (h O g O f): surj(A,A);         \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1110
diff changeset
   121
\       (f O h O g): surj(B,B);         \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1110
diff changeset
   122
\       (g O f O h): inj(C,C);          \
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
782
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 736
diff changeset
   125
qed "pastre3";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
val prems = goalw Perm.thy [bij_def]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1110
diff changeset
   128
    "[| (h O g O f): surj(A,A);         \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1110
diff changeset
   129
\       (f O h O g): inj(B,B);          \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1110
diff changeset
   130
\       (g O f O h): inj(C,C);          \
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
782
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 736
diff changeset
   133
qed "pastre4";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
val prems = goalw Perm.thy [bij_def]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1110
diff changeset
   136
    "[| (h O g O f): inj(A,A);          \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1110
diff changeset
   137
\       (f O h O g): surj(B,B);         \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1110
diff changeset
   138
\       (g O f O h): inj(C,C);          \
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
782
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 736
diff changeset
   141
qed "pastre5";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
val prems = goalw Perm.thy [bij_def]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1110
diff changeset
   144
    "[| (h O g O f): inj(A,A);          \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1110
diff changeset
   145
\       (f O h O g): inj(B,B);          \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1110
diff changeset
   146
\       (g O f O h): surj(C,C);         \
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
782
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 736
diff changeset
   149
qed "pastre6";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
7
268f93ab3bc4 Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents: 0
diff changeset
   151
(** Yet another example... **)
268f93ab3bc4 Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents: 0
diff changeset
   152
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1782
diff changeset
   153
goal Perm.thy
7
268f93ab3bc4 Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents: 0
diff changeset
   154
    "(lam Z:Pow(A+B). <{x:A. Inl(x):Z}, {y:B. Inr(y):Z}>) \
268f93ab3bc4 Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents: 0
diff changeset
   155
\    : bij(Pow(A+B), Pow(A)*Pow(B))";
1110
756aa2e81f6e Changed some definitions and proofs to use pattern-matching.
lcp
parents: 782
diff changeset
   156
by (res_inst_tac [("d", "%<X,Y>.{Inl(x).x:X} Un {Inr(y).y:Y}")] 
695
a1586fa1b755 ZF/ex/Ramsey,Rmap,misc.ML: modified for new definition of Pi(A,B)
lcp
parents: 434
diff changeset
   157
    lam_bijective 1);
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4322
diff changeset
   158
(*Auto_tac no longer proves it*)
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4322
diff changeset
   159
by (REPEAT (fast_tac (claset() addss (simpset())) 1));
4595
fa8cee619732 New example, Pow_Sigma_bij
paulson
parents: 4477
diff changeset
   160
qed "Pow_sum_bij";
fa8cee619732 New example, Pow_Sigma_bij
paulson
parents: 4477
diff changeset
   161
fa8cee619732 New example, Pow_Sigma_bij
paulson
parents: 4477
diff changeset
   162
(*As a special case, we have  bij(Pow(A*B), A -> Pow B)  *)
fa8cee619732 New example, Pow_Sigma_bij
paulson
parents: 4477
diff changeset
   163
goal Perm.thy
fa8cee619732 New example, Pow_Sigma_bij
paulson
parents: 4477
diff changeset
   164
    "(lam r:Pow(Sigma(A,B)). lam x:A. r``{x}) \
fa8cee619732 New example, Pow_Sigma_bij
paulson
parents: 4477
diff changeset
   165
\    : bij(Pow(Sigma(A,B)), PROD x:A. Pow(B(x)))";
fa8cee619732 New example, Pow_Sigma_bij
paulson
parents: 4477
diff changeset
   166
by (res_inst_tac [("d", "%f. UN x:A. UN y:f`x. {<x,y>}")] lam_bijective 1);
fa8cee619732 New example, Pow_Sigma_bij
paulson
parents: 4477
diff changeset
   167
by (blast_tac (claset() addDs [apply_type]) 2);
fa8cee619732 New example, Pow_Sigma_bij
paulson
parents: 4477
diff changeset
   168
by (blast_tac (claset() addIs [lam_type]) 1);
fa8cee619732 New example, Pow_Sigma_bij
paulson
parents: 4477
diff changeset
   169
by (ALLGOALS Asm_simp_tac);
fa8cee619732 New example, Pow_Sigma_bij
paulson
parents: 4477
diff changeset
   170
by (Fast_tac 1);
fa8cee619732 New example, Pow_Sigma_bij
paulson
parents: 4477
diff changeset
   171
by (rtac fun_extension 1);
fa8cee619732 New example, Pow_Sigma_bij
paulson
parents: 4477
diff changeset
   172
by (assume_tac 2);
fa8cee619732 New example, Pow_Sigma_bij
paulson
parents: 4477
diff changeset
   173
by (rtac (singletonI RS lam_type) 1);
fa8cee619732 New example, Pow_Sigma_bij
paulson
parents: 4477
diff changeset
   174
by (Asm_simp_tac 1);
fa8cee619732 New example, Pow_Sigma_bij
paulson
parents: 4477
diff changeset
   175
by (Blast_tac 1);
fa8cee619732 New example, Pow_Sigma_bij
paulson
parents: 4477
diff changeset
   176
qed "Pow_Sigma_bij";
7
268f93ab3bc4 Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents: 0
diff changeset
   177
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
writeln"Reached end of file.";