src/ZF/ex/Rmap.ML
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 515 abcc438e7c27
child 694 c7d592f6312a
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
     1 (*  Title: 	ZF/ex/Rmap
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Inductive definition of an operator to "map" a relation over a list
     7 *)
     8 
     9 open Rmap;
    10 
    11 goalw Rmap.thy rmap.defs "!!r s. r<=s ==> rmap(r) <= rmap(s)";
    12 by (rtac lfp_mono 1);
    13 by (REPEAT (rtac rmap.bnd_mono 1));
    14 by (REPEAT (ares_tac ([Sigma_mono, list_mono, domain_mono, range_mono] @ 
    15 		      basic_monos) 1));
    16 val rmap_mono = result();
    17 
    18 val rmap_induct = standard 
    19     (rmap.mutual_induct RS spec RS spec RSN (2,rev_mp));
    20 
    21 val Nil_rmap_case = rmap.mk_cases list.con_defs "<Nil,zs> : rmap(r)"
    22 and Cons_rmap_case = rmap.mk_cases list.con_defs "<Cons(x,xs),zs> : rmap(r)";
    23 
    24 val rmap_cs = ZF_cs addIs  rmap.intrs
    25 		    addSEs [Nil_rmap_case, Cons_rmap_case];
    26 
    27 goal Rmap.thy "!!r. r <= A*B ==> rmap(r) <= list(A)*list(B)";
    28 by (rtac (rmap.dom_subset RS subset_trans) 1);
    29 by (REPEAT (ares_tac [domain_rel_subset, range_rel_subset,
    30 		      Sigma_mono, list_mono] 1));
    31 val rmap_rel_type = result();
    32 
    33 goal Rmap.thy
    34     "!!r. [| ALL x:A. EX y. <x,y>: r;  xs: list(A) |] ==> \
    35 \         EX y. <xs, y> : rmap(r)";
    36 by (etac list.induct 1);
    37 by (ALLGOALS (fast_tac rmap_cs));
    38 val rmap_total = result();
    39 
    40 goal Rmap.thy
    41     "!!r. [| ALL x y z. <x,y>: r --> <x,z>: r --> y=z;    \
    42 \            <xs, ys> : rmap(r) |] ==>                    \
    43 \          ALL zs. <xs, zs> : rmap(r) --> ys=zs";
    44 by (etac rmap_induct 1);
    45 by (ALLGOALS (fast_tac rmap_cs));
    46 val rmap_functional_lemma = result();
    47 val rmap_functional = standard (rmap_functional_lemma RS spec RS mp);
    48 
    49 (** If f is a function then rmap(f) behaves as expected. **)
    50 
    51 goal Rmap.thy "!!f. f: A->B ==> rmap(f): list(A)->list(B)";
    52 by (etac PiE 1);
    53 by (rtac PiI 1);
    54 by (etac rmap_rel_type 1);
    55 by (rtac (rmap_total RS ex_ex1I) 1);
    56 by (assume_tac 2);
    57 by (fast_tac (ZF_cs addSEs [bspec RS ex1E]) 1);
    58 by (rtac rmap_functional 1);
    59 by (REPEAT (assume_tac 2));
    60 by (fast_tac (ZF_cs addSEs [bspec RS ex1_equalsE]) 1);
    61 val rmap_fun_type = result();
    62 
    63 goalw Rmap.thy [apply_def] "rmap(f)`Nil = Nil";
    64 by (fast_tac (rmap_cs addIs [the_equality]) 1);
    65 val rmap_Nil = result();
    66 
    67 goal Rmap.thy "!!f. [| f: A->B;  x: A;  xs: list(A) |] ==> \
    68 \                   rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)";
    69 by (rtac apply_equality 1);
    70 by (REPEAT (ares_tac ([apply_Pair, rmap_fun_type] @ rmap.intrs) 1));
    71 val rmap_Cons = result();