(* Title: ZF/Induct/Rmap.thy Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge \<open>An operator to ``map'' a relation over a list\<close> theory Rmap imports ZF begin consts "i\i" inductive "rmap(r)" \<subseteq> "list(domain(r)) \<times> list(range(r))" intros "\Nil,Nil\ \ rmap(r)" "\\x,y\: r; \xs,ys\ \ rmap(r)\ \<Longrightarrow> <Cons(x,xs), Cons(y,ys)> \<in> rmap(r)" intros lemma rmap_mono: "r \ s \ rmap(r) \ rmap(s)" unfolding 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,zs\ \ 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 |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))" unfolding function_defapply (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 \<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) blastlemma rmap_Cons: "\f \ A->B; x \ A; xs: list(A)\ \<Longrightarrow> rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)" by (blast intro: apply_equality apply_Pair rmap_fun_type rmap.intros )end quality 93%
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
