Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Rmap.thy Sprache: Isabelle

Original von: Isabelle^©

(*  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) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.