|
(* Title: ZF/Induct/Rmap.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
*)
section \<open>An operator to ``map'' a relation over a list\<close>
theory Rmap imports ZF begin
consts
rmap :: "i=>i"
inductive
domains "rmap(r)" \<subseteq> "list(domain(r)) \<times> list(range(r))"
intros
NilI: " \ rmap(r)"
ConsI: "[| : r; \ rmap(r) |]
==> <Cons(x,xs), Cons(y,ys)> \<in> rmap(r)"
type_intros domainI rangeI list.intros
lemma rmap_mono: "r \ s ==> rmap(r) \ rmap(s)"
apply (unfold rmap.defs)
apply (rule lfp_mono)
apply (rule rmap.bnd_mono)+
apply (assumption | rule Sigma_mono list_mono domain_mono range_mono basic_monos)+
done
inductive_cases
Nil_rmap_case [elim!]: " \ rmap(r)"
and Cons_rmap_case [elim!]: " \ rmap(r)"
declare rmap.intros [intro]
lemma rmap_rel_type: "r \ A \ B ==> rmap(r) \ list(A) \ list(B)"
apply (rule rmap.dom_subset [THEN subset_trans])
apply (assumption |
rule domain_rel_subset range_rel_subset Sigma_mono list_mono)+
done
lemma rmap_total: "A \ domain(r) ==> list(A) \ domain(rmap(r))"
apply (rule subsetI)
apply (erule list.induct)
apply blast+
done
lemma rmap_functional: "function(r) ==> function(rmap(r))"
apply (unfold function_def)
apply (rule impI [THEN allI, THEN allI])
apply (erule rmap.induct)
apply blast+
done
text \<open>
\medskip If \<open>f\<close> is a function then \<open>rmap(f)\<close> behaves
as expected.
\<close>
lemma rmap_fun_type: "f \ A->B ==> rmap(f): list(A)->list(B)"
by (simp add: Pi_iff rmap_rel_type rmap_functional rmap_total)
lemma rmap_Nil: "rmap(f)`Nil = Nil"
by (unfold apply_def) blast
lemma rmap_Cons: "[| f \ A->B; x \ A; xs: list(A) |]
==> rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)"
by (blast intro: apply_equality apply_Pair rmap_fun_type rmap.intros)
end
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
