# Theory Rmap

Up to index of Isabelle/ZF/Induct

theory Rmap
imports Main
begin

    (*  Title:      ZF/Induct/Rmap.thy
        ID:         $Id: Rmap.thy,v 1.4 2005/06/17 14:15:11 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1994  University of Cambridge
    *)

    header {* An operator to ``map'' a relation over a list *}

    theory Rmap imports Main begin

    consts
      rmap :: "i=>i"

    inductive
      domains "rmap(r)" ⊆ "list(domain(r)) × list(range(r))"
      intros
        NilI:  "<Nil,Nil> ∈ rmap(r)"

        ConsI: "[| <x,y>: r;  <xs,ys> ∈ rmap(r) |]
                ==> <Cons(x,xs), Cons(y,ys)> ∈ 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!]: "<Nil,zs> ∈ rmap(r)"
      and Cons_rmap_case [elim!]: "<Cons(x,xs),zs> ∈ 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 {*
      \medskip If @{text f} is a function then @{text "rmap(f)"} behaves
      as expected.
    *}

    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

lemma rmap_mono:

      r ⊆ s ==> rmap(r) ⊆ rmap(s)

lemmas Nil_rmap_case:

      [| ⟨[], zs⟩ ∈ rmap(r); zs = [] ==> Q |] ==> Q

and Cons_rmap_case:

      [| ⟨Cons(x, xs), zs⟩ ∈ rmap(r);
         !!y ys. [| ⟨x, y⟩ ∈ r; ⟨xs, ys⟩ ∈ rmap(r); zs = Cons(y, ys) |] ==> Q |]
      ==> Q

lemma rmap_rel_type:

      r ⊆ A × B ==> rmap(r) ⊆ list(A) × list(B)

lemma rmap_total:

      A ⊆ domain(r) ==> list(A) ⊆ domain(rmap(r))

lemma rmap_functional:

      function(r) ==> function(rmap(r))

lemma rmap_fun_type:

      f ∈ A -> B ==> rmap(f) ∈ list(A) -> list(B)

lemma rmap_Nil:

      rmap(f) ` [] = []

lemma rmap_Cons:

      [| f ∈ A -> B; x ∈ A; xs ∈ list(A) |]
      ==> rmap(f) ` Cons(x, xs) = Cons(f ` x, rmap(f) ` xs)