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