1(*  Title:      ZF/Induct/Rmap.thy
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1994  University of Cambridge
4*)
5
6section \<open>An operator to ``map'' a relation over a list\<close>
7
8theory Rmap imports ZF begin
9
10consts
11  rmap :: "i=>i"
12
13inductive
14  domains "rmap(r)" \<subseteq> "list(domain(r)) \<times> list(range(r))"
15  intros
16    NilI:  "<Nil,Nil> \<in> rmap(r)"
17
18    ConsI: "[| <x,y>: r;  <xs,ys> \<in> rmap(r) |]
19            ==> <Cons(x,xs), Cons(y,ys)> \<in> rmap(r)"
20
21  type_intros domainI rangeI list.intros
22
23lemma rmap_mono: "r \<subseteq> s ==> rmap(r) \<subseteq> rmap(s)"
24  apply (unfold rmap.defs)
25  apply (rule lfp_mono)
26    apply (rule rmap.bnd_mono)+
27  apply (assumption | rule Sigma_mono list_mono domain_mono range_mono basic_monos)+
28  done
29
30inductive_cases
31      Nil_rmap_case [elim!]: "<Nil,zs> \<in> rmap(r)"
32  and Cons_rmap_case [elim!]: "<Cons(x,xs),zs> \<in> rmap(r)"
33
34declare rmap.intros [intro]
35
36lemma rmap_rel_type: "r \<subseteq> A \<times> B ==> rmap(r) \<subseteq> list(A) \<times> list(B)"
37  apply (rule rmap.dom_subset [THEN subset_trans])
38  apply (assumption |
39    rule domain_rel_subset range_rel_subset Sigma_mono list_mono)+
40  done
41
42lemma rmap_total: "A \<subseteq> domain(r) ==> list(A) \<subseteq> domain(rmap(r))"
43  apply (rule subsetI)
44  apply (erule list.induct)
45   apply blast+
46  done
47
48lemma rmap_functional: "function(r) ==> function(rmap(r))"
49  apply (unfold function_def)
50  apply (rule impI [THEN allI, THEN allI])
51  apply (erule rmap.induct)
52   apply blast+
53  done
54
55text \<open>
56  \medskip If \<open>f\<close> is a function then \<open>rmap(f)\<close> behaves
57  as expected.
58\<close>
59
60lemma rmap_fun_type: "f \<in> A->B ==> rmap(f): list(A)->list(B)"
61  by (simp add: Pi_iff rmap_rel_type rmap_functional rmap_total)
62
63lemma rmap_Nil: "rmap(f)`Nil = Nil"
64  by (unfold apply_def) blast
65
66lemma rmap_Cons: "[| f \<in> A->B;  x \<in> A;  xs: list(A) |]
67      ==> rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)"
68  by (blast intro: apply_equality apply_Pair rmap_fun_type rmap.intros)
69
70end
71