src/ZF/ex/Rmap.ML

-(*  Title: 	ZF/ex/rmap
+(*  Title: 	ZF/ex/Rmap
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
+    Copyright   1994  University of Cambridge
 
 Inductive definition of an operator to "map" a relation over a list
 *)
 
-structure Rmap = Inductive_Fun
- (val thy 	 = List.thy |> add_consts [("rmap","i=>i",NoSyn)];
-  val thy_name	 = "Rmap";
-  val rec_doms	 = [("rmap", "list(domain(r))*list(range(r))")];
-  val sintrs	 = 
-      ["<Nil,Nil> : rmap(r)",
+open Rmap;
 
-       "[| <x,y>: r;  <xs,ys> : rmap(r) |] ==> \
-\       <Cons(x,xs), Cons(y,ys)> : rmap(r)"];
-  val monos	 = [];
-  val con_defs	 = [];
-  val type_intrs = [domainI,rangeI] @ List.intrs
-  val type_elims = []);
-
-goalw Rmap.thy Rmap.defs "!!r s. r<=s ==> rmap(r) <= rmap(s)";
+goalw Rmap.thy rmap.defs "!!r s. r<=s ==> rmap(r) <= rmap(s)";
 by (rtac lfp_mono 1);
-by (REPEAT (rtac Rmap.bnd_mono 1));
+by (REPEAT (rtac rmap.bnd_mono 1));
 by (REPEAT (ares_tac ([Sigma_mono, list_mono, domain_mono, range_mono] @ 
 		      basic_monos) 1));
 val rmap_mono = result();
 
 val rmap_induct = standard 
-    (Rmap.mutual_induct RS spec RS spec RSN (2,rev_mp));
+    (rmap.mutual_induct RS spec RS spec RSN (2,rev_mp));
 
-val Nil_rmap_case = Rmap.mk_cases List.con_defs "<Nil,zs> : rmap(r)"
-and Cons_rmap_case = Rmap.mk_cases List.con_defs "<Cons(x,xs),zs> : rmap(r)";
+val Nil_rmap_case = rmap.mk_cases list.con_defs "<Nil,zs> : rmap(r)"
+and Cons_rmap_case = rmap.mk_cases list.con_defs "<Cons(x,xs),zs> : rmap(r)";
 
-val rmap_cs = ZF_cs addIs  Rmap.intrs
+val rmap_cs = ZF_cs addIs  rmap.intrs
 		    addSEs [Nil_rmap_case, Cons_rmap_case];
 
 goal Rmap.thy "!!r. r <= A*B ==> rmap(r) <= list(A)*list(B)";
-by (rtac (Rmap.dom_subset RS subset_trans) 1);
+by (rtac (rmap.dom_subset RS subset_trans) 1);
 by (REPEAT (ares_tac [domain_rel_subset, range_rel_subset,
 		      Sigma_mono, list_mono] 1));
 val rmap_rel_type = result();
 
 goal Rmap.thy
     "!!r. [| ALL x:A. EX y. <x,y>: r;  xs: list(A) |] ==> \
 \         EX y. <xs, y> : rmap(r)";
-by (etac List.induct 1);
+by (etac list.induct 1);
 by (ALLGOALS (fast_tac rmap_cs));
 val rmap_total = result();
 
 goal Rmap.thy
     "!!r. [| ALL x y z. <x,y>: r --> <x,z>: r --> y=z;    \

 val rmap_Nil = result();
 
 goal Rmap.thy "!!f. [| f: A->B;  x: A;  xs: list(A) |] ==> \
 \                   rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)";
 by (rtac apply_equality 1);
-by (REPEAT (ares_tac ([apply_Pair, rmap_fun_type] @ Rmap.intrs) 1));
+by (REPEAT (ares_tac ([apply_Pair, rmap_fun_type] @ rmap.intrs) 1));
 val rmap_Cons = result();