src/ZF/ex/misc.ML
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 434 89d45187f04d
child 695 a1586fa1b755
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
clasohm@0
     1
(*  Title: 	ZF/ex/misc
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Miscellaneous examples for Zermelo-Fraenkel Set Theory 
clasohm@0
     7
Cantor's Theorem; Schroeder-Bernstein Theorem; Composition of homomorphisms...
clasohm@0
     8
*)
clasohm@0
     9
clasohm@0
    10
writeln"ZF/ex/misc";
clasohm@0
    11
clasohm@0
    12
clasohm@0
    13
(*Example 12 (credited to Peter Andrews) from
clasohm@0
    14
 W. Bledsoe.  A Maximal Method for Set Variables in Automatic Theorem-proving.
clasohm@0
    15
 In: J. Hayes and D. Michie and L. Mikulich, eds.  Machine Intelligence 9.
clasohm@0
    16
 Ellis Horwood, 53-100 (1979). *)
clasohm@0
    17
goal ZF.thy "(ALL F. {x}: F --> {y}:F) --> (ALL A. x:A --> y:A)";
clasohm@0
    18
by (best_tac ZF_cs 1);
clasohm@0
    19
result();
clasohm@0
    20
clasohm@0
    21
clasohm@0
    22
(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***)
clasohm@0
    23
clasohm@0
    24
val cantor_cs = FOL_cs   (*precisely the rules needed for the proof*)
clasohm@0
    25
  addSIs [ballI, CollectI, PowI, subsetI] addIs [bexI]
clasohm@0
    26
  addSEs [CollectE, equalityCE];
clasohm@0
    27
clasohm@0
    28
(*The search is undirected and similar proof attempts fail*)
lcp@38
    29
goal ZF.thy "ALL f: A->Pow(A). EX S: Pow(A). ALL x:A. f`x ~= S";
clasohm@0
    30
by (best_tac cantor_cs 1);
clasohm@0
    31
result();
clasohm@0
    32
lcp@38
    33
(*This form displays the diagonal term, {x: A . x ~: f`x} *)
clasohm@0
    34
val [prem] = goal ZF.thy
lcp@38
    35
    "f: A->Pow(A) ==> (ALL x:A. f`x ~= ?S) & ?S: Pow(A)";
clasohm@0
    36
by (best_tac cantor_cs 1);
clasohm@0
    37
result();
clasohm@0
    38
clasohm@0
    39
(*yet another version...*)
lcp@38
    40
goalw Perm.thy [surj_def] "f ~: surj(A,Pow(A))";
clasohm@0
    41
by (safe_tac ZF_cs);
clasohm@0
    42
by (etac ballE 1);
clasohm@0
    43
by (best_tac (cantor_cs addSEs [bexE]) 1);
clasohm@0
    44
by (fast_tac ZF_cs 1);
clasohm@0
    45
result();
clasohm@0
    46
clasohm@0
    47
clasohm@0
    48
(*** Composition of homomorphisms is a homomorphism ***)
clasohm@0
    49
clasohm@0
    50
(*Given as a challenge problem in
clasohm@0
    51
  R. Boyer et al.,
clasohm@0
    52
  Set Theory in First-Order Logic: Clauses for G\"odel's Axioms,
clasohm@0
    53
  JAR 2 (1986), 287-327 
clasohm@0
    54
*)
clasohm@0
    55
lcp@7
    56
(*collecting the relevant lemmas*)
lcp@434
    57
val hom_ss = ZF_ss addsimps [comp_fun,comp_fun_apply,SigmaI,apply_funtype];
clasohm@0
    58
lcp@434
    59
(*The problem below is proving conditions of rewrites such as comp_fun_apply;
lcp@7
    60
  rewriting does not instantiate Vars; we must prove the conditions
lcp@7
    61
  explicitly.*)
lcp@7
    62
fun hom_tac hyps =
lcp@7
    63
    resolve_tac (TrueI::refl::iff_refl::hyps) ORELSE' 
lcp@7
    64
    (cut_facts_tac hyps THEN' fast_tac prop_cs);
lcp@7
    65
lcp@7
    66
(*This version uses a super application of simp_tac*)
lcp@7
    67
goal Perm.thy
clasohm@0
    68
    "(ALL A f B g. hom(A,f,B,g) = \
clasohm@0
    69
\          {H: A->B. f:A*A->A & g:B*B->B & \
lcp@7
    70
\                    (ALL x:A. ALL y:A. H`(f`<x,y>) = g`<H`x,H`y>)}) --> \
clasohm@0
    71
\    J : hom(A,f,B,g) & K : hom(B,g,C,h) -->  \
clasohm@0
    72
\    (K O J) : hom(A,f,C,h)";
lcp@7
    73
by (simp_tac (hom_ss setsolver hom_tac) 1);
lcp@7
    74
(*Also works but slower:
lcp@7
    75
    by (asm_simp_tac (hom_ss setloop (K (safe_tac FOL_cs))) 1); *)
clasohm@0
    76
val comp_homs = result();
clasohm@0
    77
lcp@7
    78
(*This version uses meta-level rewriting, safe_tac and asm_simp_tac*)
clasohm@0
    79
val [hom_def] = goal Perm.thy
clasohm@0
    80
    "(!! A f B g. hom(A,f,B,g) == \
clasohm@0
    81
\          {H: A->B. f:A*A->A & g:B*B->B & \
clasohm@0
    82
\                    (ALL x:A. ALL y:A. H`(f`<x,y>) = g`<H`x,H`y>)}) ==> \
clasohm@0
    83
\    J : hom(A,f,B,g) & K : hom(B,g,C,h) -->  \
clasohm@0
    84
\    (K O J) : hom(A,f,C,h)";
clasohm@0
    85
by (rewtac hom_def);
clasohm@0
    86
by (safe_tac ZF_cs);
lcp@7
    87
by (asm_simp_tac hom_ss 1);
lcp@7
    88
by (asm_simp_tac hom_ss 1);
clasohm@0
    89
val comp_homs = result();
clasohm@0
    90
clasohm@0
    91
clasohm@0
    92
(** A characterization of functions, suggested by Tobias Nipkow **)
clasohm@0
    93
clasohm@0
    94
goalw ZF.thy [Pi_def]
clasohm@0
    95
    "r: domain(r)->B  <->  r <= domain(r)*B & (ALL X. r `` (r -`` X) <= X)";
clasohm@0
    96
by (safe_tac ZF_cs);
clasohm@0
    97
by (fast_tac (ZF_cs addSDs [bspec RS ex1_equalsE]) 1);
clasohm@0
    98
by (eres_inst_tac [("x", "{y}")] allE 1);
clasohm@0
    99
by (fast_tac ZF_cs 1);
clasohm@0
   100
result();
clasohm@0
   101
clasohm@0
   102
clasohm@0
   103
(**** From D Pastre.  Automatic theorem proving in set theory. 
clasohm@0
   104
         Artificial Intelligence, 10:1--27, 1978.
clasohm@0
   105
             These examples require forward reasoning! ****)
clasohm@0
   106
clasohm@0
   107
(*reduce the clauses to units by type checking -- beware of nontermination*)
clasohm@0
   108
fun forw_typechk tyrls [] = []
clasohm@0
   109
  | forw_typechk tyrls clauses =
clasohm@0
   110
    let val (units, others) = partition (has_fewer_prems 1) clauses
clasohm@0
   111
    in  gen_union eq_thm (units, forw_typechk tyrls (tyrls RL others))
clasohm@0
   112
    end;
clasohm@0
   113
clasohm@0
   114
(*A crude form of forward reasoning*)
clasohm@0
   115
fun forw_iterate tyrls rls facts 0 = facts
clasohm@0
   116
  | forw_iterate tyrls rls facts n =
clasohm@0
   117
      let val facts' = 
clasohm@0
   118
	  gen_union eq_thm (forw_typechk (tyrls@facts) (facts RL rls), facts);
clasohm@0
   119
      in  forw_iterate tyrls rls facts' (n-1)  end;
clasohm@0
   120
clasohm@0
   121
val pastre_rls =
clasohm@0
   122
    [comp_mem_injD1, comp_mem_surjD1, comp_mem_injD2, comp_mem_surjD2];
clasohm@0
   123
clasohm@0
   124
fun pastre_facts (fact1::fact2::fact3::prems) = 
lcp@434
   125
    forw_iterate (prems @ [comp_surj, comp_inj, comp_fun])
clasohm@0
   126
               pastre_rls [fact1,fact2,fact3] 4;
clasohm@0
   127
clasohm@0
   128
val prems = goalw Perm.thy [bij_def]
clasohm@0
   129
    "[| (h O g O f): inj(A,A);		\
clasohm@0
   130
\       (f O h O g): surj(B,B); 	\
clasohm@0
   131
\       (g O f O h): surj(C,C); 	\
clasohm@0
   132
\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
clasohm@0
   133
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
clasohm@0
   134
val pastre1 = result();
clasohm@0
   135
clasohm@0
   136
val prems = goalw Perm.thy [bij_def]
clasohm@0
   137
    "[| (h O g O f): surj(A,A);		\
clasohm@0
   138
\       (f O h O g): inj(B,B); 		\
clasohm@0
   139
\       (g O f O h): surj(C,C); 	\
clasohm@0
   140
\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
clasohm@0
   141
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
clasohm@0
   142
val pastre2 = result();
clasohm@0
   143
clasohm@0
   144
val prems = goalw Perm.thy [bij_def]
clasohm@0
   145
    "[| (h O g O f): surj(A,A);		\
clasohm@0
   146
\       (f O h O g): surj(B,B); 	\
clasohm@0
   147
\       (g O f O h): inj(C,C); 		\
clasohm@0
   148
\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
clasohm@0
   149
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
clasohm@0
   150
val pastre3 = result();
clasohm@0
   151
clasohm@0
   152
val prems = goalw Perm.thy [bij_def]
clasohm@0
   153
    "[| (h O g O f): surj(A,A);		\
clasohm@0
   154
\       (f O h O g): inj(B,B); 		\
clasohm@0
   155
\       (g O f O h): inj(C,C); 		\
clasohm@0
   156
\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
clasohm@0
   157
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
clasohm@0
   158
val pastre4 = result();
clasohm@0
   159
clasohm@0
   160
val prems = goalw Perm.thy [bij_def]
clasohm@0
   161
    "[| (h O g O f): inj(A,A);		\
clasohm@0
   162
\       (f O h O g): surj(B,B); 	\
clasohm@0
   163
\       (g O f O h): inj(C,C); 		\
clasohm@0
   164
\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
clasohm@0
   165
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
clasohm@0
   166
val pastre5 = result();
clasohm@0
   167
clasohm@0
   168
val prems = goalw Perm.thy [bij_def]
clasohm@0
   169
    "[| (h O g O f): inj(A,A);		\
clasohm@0
   170
\       (f O h O g): inj(B,B); 		\
clasohm@0
   171
\       (g O f O h): surj(C,C); 	\
clasohm@0
   172
\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
clasohm@0
   173
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
clasohm@0
   174
val pastre6 = result();
clasohm@0
   175
lcp@7
   176
(** Yet another example... **)
lcp@7
   177
lcp@7
   178
goalw (merge_theories(Sum.thy,Perm.thy)) [bij_def,inj_def,surj_def]
lcp@7
   179
    "(lam Z:Pow(A+B). <{x:A. Inl(x):Z}, {y:B. Inr(y):Z}>) \
lcp@7
   180
\    : bij(Pow(A+B), Pow(A)*Pow(B))";
lcp@7
   181
by (DO_GOAL
lcp@7
   182
      [rtac IntI,
lcp@7
   183
       DO_GOAL
lcp@7
   184
	 [rtac CollectI,
lcp@7
   185
	  fast_tac (ZF_cs addSIs [lam_type]),
lcp@7
   186
	  simp_tac ZF_ss,
lcp@7
   187
	  fast_tac (eq_cs addSEs [sumE]
lcp@7
   188
			  addEs  [equalityD1 RS subsetD RS CollectD2,
lcp@7
   189
				  equalityD2 RS subsetD RS CollectD2])],
lcp@7
   190
       DO_GOAL
lcp@7
   191
	 [rtac CollectI,
lcp@7
   192
	  fast_tac (ZF_cs addSIs [lam_type]),
lcp@7
   193
	  simp_tac ZF_ss,
lcp@7
   194
	  K(safe_tac ZF_cs),
lcp@7
   195
	  res_inst_tac [("x", "{Inl(u). u: ?U} Un {Inr(v). v: ?V}")] bexI,
lcp@7
   196
	  DO_GOAL
lcp@7
   197
	    [res_inst_tac [("t", "Pair")] subst_context2,
lcp@7
   198
	    fast_tac (sum_cs addSIs [equalityI]),
lcp@7
   199
	    fast_tac (sum_cs addSIs [equalityI])],
lcp@7
   200
	  DO_GOAL [fast_tac sum_cs]]] 1);
lcp@7
   201
val Pow_bij = result();
lcp@7
   202
clasohm@0
   203
writeln"Reached end of file.";