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