Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: AList_Mapping.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Library/AList_Mapping.thy
    Author:     Florian Haftmann, TU Muenchen
*)

section \<open>Implementation of mappings with Association Lists\<close>

theory AList_Mapping
  imports AList Mapping
begin

lift_definition Mapping :: "('a \ 'b) list \ ('a, 'b) mapping" is map_of .

code_datatype Mapping

lemma lookup_Mapping [simp, code]: "Mapping.lookup (Mapping xs) = map_of xs"
  by transfer rule

lemma keys_Mapping [simp, code]: "Mapping.keys (Mapping xs) = set (map fst xs)"
  by transfer (simp add: dom_map_of_conv_image_fst)

lemma empty_Mapping [code]: "Mapping.empty = Mapping []"
  by transfer simp

lemma is_empty_Mapping [code]: "Mapping.is_empty (Mapping xs) \ List.null xs"
  by (cases xs) (simp_all add: is_empty_def null_def)

lemma update_Mapping [code]: "Mapping.update k v (Mapping xs) = Mapping (AList.update k v xs)"
  by transfer (simp add: update_conv')

lemma delete_Mapping [code]: "Mapping.delete k (Mapping xs) = Mapping (AList.delete k xs)"
  by transfer (simp add: delete_conv')

lemma ordered_keys_Mapping [code]:
  "Mapping.ordered_keys (Mapping xs) = sort (remdups (map fst xs))"
  by (simp only: ordered_keys_def keys_Mapping sorted_list_of_set_sort_remdups) simp

lemma size_Mapping [code]: "Mapping.size (Mapping xs) = length (remdups (map fst xs))"
  by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst)

lemma tabulate_Mapping [code]: "Mapping.tabulate ks f = Mapping (map (\k. (k, f k)) ks)"
  by transfer (simp add: map_of_map_restrict)

lemma bulkload_Mapping [code]:
  "Mapping.bulkload vs = Mapping (map (\n. (n, vs ! n)) [0..
  by transfer (simp add: map_of_map_restrict fun_eq_iff)

lemma equal_Mapping [code]:
  "HOL.equal (Mapping xs) (Mapping ys) \
    (let ks = map fst xs; ls = map fst ys
     in (\<forall>l\<in>set ls. l \<in> set ks) \<and> (\<forall>k\<in>set ks. k \<in> set ls \<and> map_of xs k = map_of ys k))"
proof -
  have *: "(a, b) \ set xs \ a \ fst ` set xs" for a b xs
    by (auto simp add: image_def intro!: bexI)
  show ?thesis
    apply transfer
    apply (auto intro!: map_of_eqI)
     apply (auto dest!: map_of_eq_dom intro: *)
    done
qed

lemma map_values_Mapping [code]:
  "Mapping.map_values f (Mapping xs) = Mapping (map (\(x,y). (x, f x y)) xs)"
  for f :: "'c \ 'a \ 'b" and xs :: "('c \ 'a) list"
  apply transfer
  apply (rule ext)
  subgoal for f xs x by (induct xs) auto
  done

lemma combine_with_key_code [code]:
  "Mapping.combine_with_key f (Mapping xs) (Mapping ys) =
     Mapping.tabulate (remdups (map fst xs @ map fst ys))
       (\<lambda>x. the (combine_options (f x) (map_of xs x) (map_of ys x)))"
  apply transfer
  apply (rule ext)
  apply (rule sym)
  subgoal for f xs ys x
    apply (cases "map_of xs x"; cases "map_of ys x"; simp)
       apply (force simp: map_of_eq_None_iff combine_options_def option.the_def o_def image_iff
        dest: map_of_SomeD split: option.splits)+
    done
  done

lemma combine_code [code]:
  "Mapping.combine f (Mapping xs) (Mapping ys) =
     Mapping.tabulate (remdups (map fst xs @ map fst ys))
       (\<lambda>x. the (combine_options f (map_of xs x) (map_of ys x)))"
  apply transfer
  apply (rule ext)
  apply (rule sym)
  subgoal for f xs ys x
    apply (cases "map_of xs x"; cases "map_of ys x"; simp)
       apply (force simp: map_of_eq_None_iff combine_options_def option.the_def o_def image_iff
        dest: map_of_SomeD split: option.splits)+
    done
  done

lemma map_of_filter_distinct:  (* TODO: move? *)
  assumes "distinct (map fst xs)"
  shows "map_of (filter P xs) x =
    (case map_of xs x of
      None \<Rightarrow> None
    | Some y \<Rightarrow> if P (x,y) then Some y else None)"
  using assms
  by (auto simp: map_of_eq_None_iff filter_map distinct_map_filter dest: map_of_SomeD
      simp del: map_of_eq_Some_iff intro!: map_of_is_SomeI split: option.splits)

lemma filter_Mapping [code]:
  "Mapping.filter P (Mapping xs) = Mapping (filter (\(k,v). P k v) (AList.clearjunk xs))"
  apply transfer
  apply (rule ext)
  apply (subst map_of_filter_distinct)
   apply (simp_all add: map_of_clearjunk split: option.split)
  done

lemma [code nbe]: "HOL.equal (x :: ('a, 'b) mapping) x \ True"
  by (fact equal_refl)

end

¤ Dauer der Verarbeitung: 0.16 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.