src/ZF/Induct/Rmap.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Induct/Rmap.ML	Wed Nov 07 12:29:07 2001 +0100
@@ -0,0 +1,56 @@
+(*  Title:      ZF/ex/Rmap
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Inductive definition of an operator to "map" a relation over a list
+*)
+
+Goalw rmap.defs "r \\<subseteq> s ==> rmap(r) \\<subseteq> rmap(s)";
+by (rtac lfp_mono 1);
+by (REPEAT (rtac rmap.bnd_mono 1));
+by (REPEAT (ares_tac ([Sigma_mono, list_mono, domain_mono, range_mono] @ 
+                      basic_monos) 1));
+qed "rmap_mono";
+
+val Nil_rmap_case  = rmap.mk_cases "<Nil,zs> \\<in> rmap(r)"
+and Cons_rmap_case = rmap.mk_cases "<Cons(x,xs),zs> \\<in> rmap(r)";
+
+AddIs  rmap.intrs;
+AddSEs [Nil_rmap_case, Cons_rmap_case];
+
+Goal "r \\<subseteq> A*B ==> rmap(r) \\<subseteq> list(A)*list(B)";
+by (rtac (rmap.dom_subset RS subset_trans) 1);
+by (REPEAT (ares_tac [domain_rel_subset, range_rel_subset,
+                      Sigma_mono, list_mono] 1));
+qed "rmap_rel_type";
+
+Goal "A \\<subseteq> domain(r) ==> list(A) \\<subseteq> domain(rmap(r))";
+by (rtac subsetI 1);
+by (etac list.induct 1);
+by (ALLGOALS Fast_tac);
+qed "rmap_total";
+
+Goalw [function_def] "function(r) ==> function(rmap(r))";
+by (rtac (impI RS allI RS allI) 1);
+by (etac rmap.induct 1);
+by (ALLGOALS Fast_tac);
+qed "rmap_functional";
+
+
+(** If f is a function then rmap(f) behaves as expected. **)
+
+Goal "f \\<in> A->B ==> rmap(f): list(A)->list(B)";
+by (asm_full_simp_tac (simpset() addsimps [Pi_iff, rmap_rel_type,
+					   rmap_functional, rmap_total]) 1);
+qed "rmap_fun_type";
+
+Goalw [apply_def] "rmap(f)`Nil = Nil";
+by (Blast_tac 1);
+qed "rmap_Nil";
+
+Goal "[| f \\<in> A->B;  x \\<in> 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));
+qed "rmap_Cons";