src/ZF/ex/misc.ML
author paulson
Wed Dec 24 10:02:30 1997 +0100 (1997-12-24 ago)
changeset 4477 b3e5857d8d99
parent 4322 5f5df208b0e0
child 4595 fa8cee619732
permissions -rw-r--r--
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
clasohm@1461
     1
(*  Title:      ZF/ex/misc
clasohm@0
     2
    ID:         $Id$
clasohm@1461
     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 
paulson@1646
     7
Composition of homomorphisms, Pastre's examples, ...
clasohm@0
     8
*)
clasohm@0
     9
clasohm@0
    10
writeln"ZF/ex/misc";
clasohm@0
    11
paulson@3000
    12
(*Nice Blast_tac benchmark.  Proved in 0.3s; old tactics can't manage it!*)
paulson@3000
    13
goal ZF.thy "!!S. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
paulson@3000
    14
by (Blast_tac 1);
paulson@3000
    15
result();
paulson@3000
    16
paulson@4322
    17
(*variant of the benchmark above*)
paulson@4322
    18
goal ZF.thy "!!S. ALL x:S. Union(S) <= x ==> EX z. S <= {z}";
paulson@4322
    19
by (Blast_tac 1);
paulson@4322
    20
result();
paulson@4322
    21
wenzelm@4109
    22
context Perm.thy;
clasohm@0
    23
clasohm@0
    24
(*Example 12 (credited to Peter Andrews) from
clasohm@0
    25
 W. Bledsoe.  A Maximal Method for Set Variables in Automatic Theorem-proving.
clasohm@0
    26
 In: J. Hayes and D. Michie and L. Mikulich, eds.  Machine Intelligence 9.
clasohm@0
    27
 Ellis Horwood, 53-100 (1979). *)
paulson@2469
    28
goal thy "(ALL F. {x}: F --> {y}:F) --> (ALL A. x:A --> y:A)";
paulson@2469
    29
by (Best_tac 1);
clasohm@0
    30
result();
clasohm@0
    31
clasohm@0
    32
clasohm@0
    33
(*** Composition of homomorphisms is a homomorphism ***)
clasohm@0
    34
clasohm@0
    35
(*Given as a challenge problem in
clasohm@0
    36
  R. Boyer et al.,
clasohm@0
    37
  Set Theory in First-Order Logic: Clauses for G\"odel's Axioms,
clasohm@0
    38
  JAR 2 (1986), 287-327 
clasohm@0
    39
*)
clasohm@0
    40
lcp@7
    41
(*collecting the relevant lemmas*)
paulson@2469
    42
Addsimps [comp_fun, SigmaI, apply_funtype];
clasohm@0
    43
lcp@736
    44
(*This version uses a super application of simp_tac.  Needs setloop to help
lcp@736
    45
  proving conditions of rewrites such as comp_fun_apply;
lcp@736
    46
  rewriting does not instantiate Vars*)
lcp@7
    47
goal Perm.thy
clasohm@0
    48
    "(ALL A f B g. hom(A,f,B,g) = \
clasohm@0
    49
\          {H: A->B. f:A*A->A & g:B*B->B & \
lcp@7
    50
\                    (ALL x:A. ALL y:A. H`(f`<x,y>) = g`<H`x,H`y>)}) --> \
clasohm@0
    51
\    J : hom(A,f,B,g) & K : hom(B,g,C,h) -->  \
clasohm@0
    52
\    (K O J) : hom(A,f,C,h)";
paulson@4152
    53
by (asm_simp_tac (simpset() setloop (K Safe_tac)) 1);
clasohm@0
    54
val comp_homs = result();
clasohm@0
    55
lcp@7
    56
(*This version uses meta-level rewriting, safe_tac and asm_simp_tac*)
clasohm@0
    57
val [hom_def] = goal Perm.thy
clasohm@0
    58
    "(!! A f B g. hom(A,f,B,g) == \
clasohm@0
    59
\          {H: A->B. f:A*A->A & g:B*B->B & \
clasohm@0
    60
\                    (ALL x:A. ALL y:A. H`(f`<x,y>) = g`<H`x,H`y>)}) ==> \
clasohm@0
    61
\    J : hom(A,f,B,g) & K : hom(B,g,C,h) -->  \
clasohm@0
    62
\    (K O J) : hom(A,f,C,h)";
clasohm@0
    63
by (rewtac hom_def);
paulson@4152
    64
by Safe_tac;
paulson@2469
    65
by (Asm_simp_tac 1);
paulson@2469
    66
by (Asm_simp_tac 1);
clasohm@782
    67
qed "comp_homs";
clasohm@0
    68
clasohm@0
    69
clasohm@0
    70
(** A characterization of functions, suggested by Tobias Nipkow **)
clasohm@0
    71
paulson@2469
    72
goalw thy [Pi_def, function_def]
clasohm@0
    73
    "r: domain(r)->B  <->  r <= domain(r)*B & (ALL X. r `` (r -`` X) <= X)";
paulson@2469
    74
by (Best_tac 1);
clasohm@0
    75
result();
clasohm@0
    76
clasohm@0
    77
clasohm@0
    78
(**** From D Pastre.  Automatic theorem proving in set theory. 
clasohm@0
    79
         Artificial Intelligence, 10:1--27, 1978.
clasohm@0
    80
             These examples require forward reasoning! ****)
clasohm@0
    81
clasohm@0
    82
(*reduce the clauses to units by type checking -- beware of nontermination*)
clasohm@0
    83
fun forw_typechk tyrls [] = []
clasohm@0
    84
  | forw_typechk tyrls clauses =
clasohm@0
    85
    let val (units, others) = partition (has_fewer_prems 1) clauses
clasohm@0
    86
    in  gen_union eq_thm (units, forw_typechk tyrls (tyrls RL others))
clasohm@0
    87
    end;
clasohm@0
    88
clasohm@0
    89
(*A crude form of forward reasoning*)
clasohm@0
    90
fun forw_iterate tyrls rls facts 0 = facts
clasohm@0
    91
  | forw_iterate tyrls rls facts n =
clasohm@0
    92
      let val facts' = 
clasohm@1461
    93
          gen_union eq_thm (forw_typechk (tyrls@facts) (facts RL rls), facts);
clasohm@0
    94
      in  forw_iterate tyrls rls facts' (n-1)  end;
clasohm@0
    95
clasohm@0
    96
val pastre_rls =
clasohm@0
    97
    [comp_mem_injD1, comp_mem_surjD1, comp_mem_injD2, comp_mem_surjD2];
clasohm@0
    98
clasohm@0
    99
fun pastre_facts (fact1::fact2::fact3::prems) = 
lcp@434
   100
    forw_iterate (prems @ [comp_surj, comp_inj, comp_fun])
clasohm@0
   101
               pastre_rls [fact1,fact2,fact3] 4;
clasohm@0
   102
clasohm@0
   103
val prems = goalw Perm.thy [bij_def]
clasohm@1461
   104
    "[| (h O g O f): inj(A,A);          \
clasohm@1461
   105
\       (f O h O g): surj(B,B);         \
clasohm@1461
   106
\       (g O f O h): surj(C,C);         \
clasohm@0
   107
\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
clasohm@0
   108
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
clasohm@782
   109
qed "pastre1";
clasohm@0
   110
clasohm@0
   111
val prems = goalw Perm.thy [bij_def]
clasohm@1461
   112
    "[| (h O g O f): surj(A,A);         \
clasohm@1461
   113
\       (f O h O g): inj(B,B);          \
clasohm@1461
   114
\       (g O f O h): surj(C,C);         \
clasohm@0
   115
\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
clasohm@0
   116
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
clasohm@782
   117
qed "pastre2";
clasohm@0
   118
clasohm@0
   119
val prems = goalw Perm.thy [bij_def]
clasohm@1461
   120
    "[| (h O g O f): surj(A,A);         \
clasohm@1461
   121
\       (f O h O g): surj(B,B);         \
clasohm@1461
   122
\       (g O f O h): inj(C,C);          \
clasohm@0
   123
\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
clasohm@0
   124
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
clasohm@782
   125
qed "pastre3";
clasohm@0
   126
clasohm@0
   127
val prems = goalw Perm.thy [bij_def]
clasohm@1461
   128
    "[| (h O g O f): surj(A,A);         \
clasohm@1461
   129
\       (f O h O g): inj(B,B);          \
clasohm@1461
   130
\       (g O f O h): inj(C,C);          \
clasohm@0
   131
\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
clasohm@0
   132
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
clasohm@782
   133
qed "pastre4";
clasohm@0
   134
clasohm@0
   135
val prems = goalw Perm.thy [bij_def]
clasohm@1461
   136
    "[| (h O g O f): inj(A,A);          \
clasohm@1461
   137
\       (f O h O g): surj(B,B);         \
clasohm@1461
   138
\       (g O f O h): inj(C,C);          \
clasohm@0
   139
\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
clasohm@0
   140
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
clasohm@782
   141
qed "pastre5";
clasohm@0
   142
clasohm@0
   143
val prems = goalw Perm.thy [bij_def]
clasohm@1461
   144
    "[| (h O g O f): inj(A,A);          \
clasohm@1461
   145
\       (f O h O g): inj(B,B);          \
clasohm@1461
   146
\       (g O f O h): surj(C,C);         \
clasohm@0
   147
\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
clasohm@0
   148
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
clasohm@782
   149
qed "pastre6";
clasohm@0
   150
lcp@7
   151
(** Yet another example... **)
lcp@7
   152
paulson@2469
   153
goal Perm.thy
lcp@7
   154
    "(lam Z:Pow(A+B). <{x:A. Inl(x):Z}, {y:B. Inr(y):Z}>) \
lcp@7
   155
\    : bij(Pow(A+B), Pow(A)*Pow(B))";
lcp@1110
   156
by (res_inst_tac [("d", "%<X,Y>.{Inl(x).x:X} Un {Inr(y).y:Y}")] 
lcp@695
   157
    lam_bijective 1);
paulson@4477
   158
(*Auto_tac no longer proves it*)
paulson@4477
   159
by (REPEAT (fast_tac (claset() addss (simpset())) 1));
paulson@4477
   160
qed "Pow_bij";
lcp@7
   161
clasohm@0
   162
writeln"Reached end of file.";