src/ZF/ex/misc.ML
author clasohm
Thu, 16 Sep 1993 12:20:38 +0200
changeset 0 a5a9c433f639
child 7 268f93ab3bc4
permissions -rw-r--r--
Initial revision
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/ex/misc
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
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 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
Cantor's Theorem; Schroeder-Bernstein Theorem; Composition of homomorphisms...
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
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
(*Example 12 (credited to Peter Andrews) from
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
 W. Bledsoe.  A Maximal Method for Set Variables in Automatic Theorem-proving.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
 In: J. Hayes and D. Michie and L. Mikulich, eds.  Machine Intelligence 9.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
 Ellis Horwood, 53-100 (1979). *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
goal ZF.thy "(ALL F. {x}: F --> {y}:F) --> (ALL A. x:A --> y:A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
by (best_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
val cantor_cs = FOL_cs   (*precisely the rules needed for the proof*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
  addSIs [ballI, CollectI, PowI, subsetI] addIs [bexI]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
  addSEs [CollectE, equalityCE];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
(*The search is undirected and similar proof attempts fail*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
goal ZF.thy "ALL f: A->Pow(A). EX S: Pow(A). ALL x:A. ~ f`x = S";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
by (best_tac cantor_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
(*This form displays the diagonal term, {x: A . ~ x: f`x} *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
val [prem] = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
    "f: A->Pow(A) ==> (ALL x:A. ~ f`x = ?S) & ?S: Pow(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
by (best_tac cantor_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
(*yet another version...*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
goalw Perm.thy [surj_def] "~ f : surj(A,Pow(A))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
by (safe_tac ZF_cs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
by (etac ballE 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
by (best_tac (cantor_cs addSEs [bexE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
(**** The Schroeder-Bernstein Theorem -- see Davey & Priestly, page 106 ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
val SB_thy = merge_theories (Fixedpt.thy, Perm.thy);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
(** Lemma: Banach's Decomposition Theorem **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
goal SB_thy "bnd_mono(X, %W. X - g``(Y - f``W))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
by (rtac bnd_monoI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
by (REPEAT (ares_tac [Diff_subset, subset_refl, Diff_mono, image_mono] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
val decomp_bnd_mono = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
val [gfun] = goal SB_thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
    "g: Y->X ==>   					\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
\    g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) = 	\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
\    X - lfp(X, %W. X - g``(Y - f``W)) ";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
by (res_inst_tac [("P", "%u. ?v = X-u")] 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
     (decomp_bnd_mono RS lfp_Tarski RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
by (SIMP_TAC (ZF_ss addrews [subset_refl, double_complement, Diff_subset,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
			     gfun RS fun_is_rel RS image_subset]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
val Banach_last_equation = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
val prems = goal SB_thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
    "[| f: X->Y;  g: Y->X |] ==>   \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
\    EX XA XB YA YB. (XA Int XB = 0) & (XA Un XB = X) &    \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
\                    (YA Int YB = 0) & (YA Un YB = Y) &    \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
\                    f``XA=YA & g``YB=XB";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
by (REPEAT 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
    (FIRSTGOAL
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
     (resolve_tac [refl, exI, conjI, Diff_disjoint, Diff_partition])));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
by (rtac Banach_last_equation 3);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
by (REPEAT (resolve_tac (prems@[fun_is_rel, image_subset, lfp_subset]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
val decomposition = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
val prems = goal SB_thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
    "[| f: inj(X,Y);  g: inj(Y,X) |] ==> EX h. h: bij(X,Y)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
by (cut_facts_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
by (cut_facts_tac [(prems RL [inj_is_fun]) MRS decomposition] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
by (fast_tac (ZF_cs addSIs [restrict_bij,bij_disjoint_Un]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
                    addIs [bij_converse_bij]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
(* The instantiation of exI to "restrict(f,XA) Un converse(restrict(g,YB))"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
   is forced by the context!! *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
val schroeder_bernstein = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
(*** Composition of homomorphisms is a homomorphism ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
(*Given as a challenge problem in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
  R. Boyer et al.,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
  Set Theory in First-Order Logic: Clauses for G\"odel's Axioms,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
  JAR 2 (1986), 287-327 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
val hom_ss =   (*collecting the relevant lemmas*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
  ZF_ss addrews [comp_func,comp_func_apply,SigmaI,apply_type]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
   	addcongs (mk_congs Perm.thy ["op O"]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
(*This version uses a super application of SIMP_TAC;  it is SLOW
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
  Expressing the goal by --> instead of ==> would make it slower still*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
val [hom_eq] = goal Perm.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
    "(ALL A f B g. hom(A,f,B,g) = \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
\          {H: A->B. f:A*A->A & g:B*B->B & \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
\                    (ALL x:A. ALL y:A. H`(f`<x,y>) = g`<H`x,H`y>)}) ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
\    J : hom(A,f,B,g) & K : hom(B,g,C,h) -->  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
\    (K O J) : hom(A,f,C,h)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
by (SIMP_TAC (hom_ss setauto K(fast_tac prop_cs) addrews [hom_eq]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
val comp_homs = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
(*This version uses meta-level rewriting, safe_tac and ASM_SIMP_TAC*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
val [hom_def] = goal Perm.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
    "(!! A f B g. hom(A,f,B,g) == \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
\          {H: A->B. f:A*A->A & g:B*B->B & \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
\                    (ALL x:A. ALL y:A. H`(f`<x,y>) = g`<H`x,H`y>)}) ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
\    J : hom(A,f,B,g) & K : hom(B,g,C,h) -->  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
\    (K O J) : hom(A,f,C,h)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
by (rewtac hom_def);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
by (safe_tac ZF_cs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
by (ASM_SIMP_TAC hom_ss 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
by (ASM_SIMP_TAC hom_ss 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
val comp_homs = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
(** A characterization of functions, suggested by Tobias Nipkow **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
goalw ZF.thy [Pi_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
    "r: domain(r)->B  <->  r <= domain(r)*B & (ALL X. r `` (r -`` X) <= X)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
by (safe_tac ZF_cs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
by (fast_tac (ZF_cs addSDs [bspec RS ex1_equalsE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
by (eres_inst_tac [("x", "{y}")] allE 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
(**** From D Pastre.  Automatic theorem proving in set theory. 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
         Artificial Intelligence, 10:1--27, 1978.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
             These examples require forward reasoning! ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
(*reduce the clauses to units by type checking -- beware of nontermination*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
fun forw_typechk tyrls [] = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
  | forw_typechk tyrls clauses =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
    let val (units, others) = partition (has_fewer_prems 1) clauses
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
    in  gen_union eq_thm (units, forw_typechk tyrls (tyrls RL others))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
    end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
(*A crude form of forward reasoning*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
fun forw_iterate tyrls rls facts 0 = facts
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
  | forw_iterate tyrls rls facts n =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
      let val facts' = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
	  gen_union eq_thm (forw_typechk (tyrls@facts) (facts RL rls), facts);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
      in  forw_iterate tyrls rls facts' (n-1)  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
val pastre_rls =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
    [comp_mem_injD1, comp_mem_surjD1, comp_mem_injD2, comp_mem_surjD2];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
fun pastre_facts (fact1::fact2::fact3::prems) = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
    forw_iterate (prems @ [comp_surj, comp_inj, comp_func])
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
               pastre_rls [fact1,fact2,fact3] 4;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
val prems = goalw Perm.thy [bij_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
    "[| (h O g O f): inj(A,A);		\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
\       (f O h O g): surj(B,B); 	\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
\       (g O f O h): surj(C,C); 	\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
val pastre1 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
val prems = goalw Perm.thy [bij_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
    "[| (h O g O f): surj(A,A);		\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
\       (f O h O g): inj(B,B); 		\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
\       (g O f O h): surj(C,C); 	\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
val pastre2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
val prems = goalw Perm.thy [bij_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
    "[| (h O g O f): surj(A,A);		\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
\       (f O h O g): surj(B,B); 	\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
\       (g O f O h): inj(C,C); 		\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
val pastre3 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
val prems = goalw Perm.thy [bij_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
    "[| (h O g O f): surj(A,A);		\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
\       (f O h O g): inj(B,B); 		\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
\       (g O f O h): inj(C,C); 		\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
val pastre4 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
val prems = goalw Perm.thy [bij_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
    "[| (h O g O f): inj(A,A);		\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
\       (f O h O g): surj(B,B); 	\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
\       (g O f O h): inj(C,C); 		\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
val pastre5 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
val prems = goalw Perm.thy [bij_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
    "[| (h O g O f): inj(A,A);		\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
\       (f O h O g): inj(B,B); 		\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
\       (g O f O h): surj(C,C); 	\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
val pastre6 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
writeln"Reached end of file.";