src/ZF/ex/Rmap.ML
author lcp
Thu Nov 03 16:05:22 1994 +0100 (1994-11-03)
changeset 694 c7d592f6312a
parent 515 abcc438e7c27
child 782 200a16083201
permissions -rw-r--r--
ZF/ex/Ramsey,Rmap,misc.ML: modified for new definition of Pi(A,B)
lcp@515
     1
(*  Title: 	ZF/ex/Rmap
lcp@16
     2
    ID:         $Id$
lcp@16
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@515
     4
    Copyright   1994  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@515
     9
open Rmap;
lcp@16
    10
lcp@515
    11
goalw Rmap.thy rmap.defs "!!r s. r<=s ==> rmap(r) <= rmap(s)";
lcp@16
    12
by (rtac lfp_mono 1);
lcp@515
    13
by (REPEAT (rtac rmap.bnd_mono 1));
lcp@16
    14
by (REPEAT (ares_tac ([Sigma_mono, list_mono, domain_mono, range_mono] @ 
lcp@16
    15
		      basic_monos) 1));
lcp@16
    16
val rmap_mono = result();
lcp@16
    17
lcp@16
    18
val rmap_induct = standard 
lcp@515
    19
    (rmap.mutual_induct RS spec RS spec RSN (2,rev_mp));
lcp@16
    20
lcp@515
    21
val Nil_rmap_case = rmap.mk_cases list.con_defs "<Nil,zs> : rmap(r)"
lcp@515
    22
and Cons_rmap_case = rmap.mk_cases list.con_defs "<Cons(x,xs),zs> : rmap(r)";
lcp@16
    23
lcp@515
    24
val rmap_cs = ZF_cs addIs  rmap.intrs
lcp@16
    25
		    addSEs [Nil_rmap_case, Cons_rmap_case];
lcp@16
    26
lcp@16
    27
goal Rmap.thy "!!r. r <= A*B ==> rmap(r) <= list(A)*list(B)";
lcp@515
    28
by (rtac (rmap.dom_subset RS subset_trans) 1);
lcp@16
    29
by (REPEAT (ares_tac [domain_rel_subset, range_rel_subset,
lcp@16
    30
		      Sigma_mono, list_mono] 1));
lcp@16
    31
val rmap_rel_type = result();
lcp@16
    32
lcp@16
    33
goal Rmap.thy
lcp@694
    34
    "!!r. A <= domain(r) ==> list(A) <= domain(rmap(r))";
lcp@694
    35
by (resolve_tac [subsetI] 1);
lcp@515
    36
by (etac list.induct 1);
lcp@16
    37
by (ALLGOALS (fast_tac rmap_cs));
lcp@16
    38
val rmap_total = result();
lcp@16
    39
lcp@694
    40
goalw Rmap.thy [function_def] "!!r. function(r) ==> function(rmap(r))";
lcp@694
    41
by (rtac (impI RS allI RS allI) 1);
lcp@16
    42
by (etac rmap_induct 1);
lcp@16
    43
by (ALLGOALS (fast_tac rmap_cs));
lcp@694
    44
val rmap_functional = result();
lcp@694
    45
lcp@16
    46
lcp@16
    47
(** If f is a function then rmap(f) behaves as expected. **)
lcp@16
    48
lcp@16
    49
goal Rmap.thy "!!f. f: A->B ==> rmap(f): list(A)->list(B)";
lcp@694
    50
by (asm_full_simp_tac 
lcp@694
    51
    (ZF_ss addsimps [Pi_iff, rmap_rel_type, rmap_functional, rmap_total]) 1);
lcp@16
    52
val rmap_fun_type = result();
lcp@16
    53
lcp@16
    54
goalw Rmap.thy [apply_def] "rmap(f)`Nil = Nil";
lcp@16
    55
by (fast_tac (rmap_cs addIs [the_equality]) 1);
lcp@16
    56
val rmap_Nil = result();
lcp@16
    57
lcp@16
    58
goal Rmap.thy "!!f. [| f: A->B;  x: A;  xs: list(A) |] ==> \
lcp@16
    59
\                   rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)";
lcp@16
    60
by (rtac apply_equality 1);
lcp@515
    61
by (REPEAT (ares_tac ([apply_Pair, rmap_fun_type] @ rmap.intrs) 1));
lcp@16
    62
val rmap_Cons = result();