src/HOL/Library/AList_Mapping.thy
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 63649 e690d6f2185b
permissions -rw-r--r--
tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
     1
(*  Title:      HOL/Library/AList_Mapping.thy
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
     2
    Author:     Florian Haftmann, TU Muenchen
44897
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
     3
*)
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
     4
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 59487
diff changeset
     5
section \<open>Implementation of mappings with Association Lists\<close>
44897
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
     6
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
     7
theory AList_Mapping
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
     8
  imports AList Mapping
44897
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
     9
begin
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    10
49929
70300f1b6835 update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents: 46238
diff changeset
    11
lift_definition Mapping :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) mapping" is map_of .
44897
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    12
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    13
code_datatype Mapping
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    14
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    15
lemma lookup_Mapping [simp, code]: "Mapping.lookup (Mapping xs) = map_of xs"
49929
70300f1b6835 update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents: 46238
diff changeset
    16
  by transfer rule
44897
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    17
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    18
lemma keys_Mapping [simp, code]: "Mapping.keys (Mapping xs) = set (map fst xs)"
49929
70300f1b6835 update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents: 46238
diff changeset
    19
  by transfer (simp add: dom_map_of_conv_image_fst)
44897
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    20
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    21
lemma empty_Mapping [code]: "Mapping.empty = Mapping []"
49929
70300f1b6835 update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents: 46238
diff changeset
    22
  by transfer simp
44897
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    23
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    24
lemma is_empty_Mapping [code]: "Mapping.is_empty (Mapping xs) \<longleftrightarrow> List.null xs"
63649
e690d6f2185b tuned proofs;
wenzelm
parents: 63476
diff changeset
    25
  by (cases xs) (simp_all add: is_empty_def null_def)
44897
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    26
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    27
lemma update_Mapping [code]: "Mapping.update k v (Mapping xs) = Mapping (AList.update k v xs)"
49929
70300f1b6835 update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents: 46238
diff changeset
    28
  by transfer (simp add: update_conv')
44897
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    29
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    30
lemma delete_Mapping [code]: "Mapping.delete k (Mapping xs) = Mapping (AList.delete k xs)"
49929
70300f1b6835 update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents: 46238
diff changeset
    31
  by transfer (simp add: delete_conv')
44897
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    32
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    33
lemma ordered_keys_Mapping [code]:
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    34
  "Mapping.ordered_keys (Mapping xs) = sort (remdups (map fst xs))"
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    35
  by (simp only: ordered_keys_def keys_Mapping sorted_list_of_set_sort_remdups) simp
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    36
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    37
lemma size_Mapping [code]: "Mapping.size (Mapping xs) = length (remdups (map fst xs))"
44897
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    38
  by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst)
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    39
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    40
lemma tabulate_Mapping [code]: "Mapping.tabulate ks f = Mapping (map (\<lambda>k. (k, f k)) ks)"
49929
70300f1b6835 update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents: 46238
diff changeset
    41
  by transfer (simp add: map_of_map_restrict)
44897
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    42
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    43
lemma bulkload_Mapping [code]:
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    44
  "Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
49929
70300f1b6835 update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents: 46238
diff changeset
    45
  by transfer (simp add: map_of_map_restrict fun_eq_iff)
44897
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    46
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    47
lemma equal_Mapping [code]:
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    48
  "HOL.equal (Mapping xs) (Mapping ys) \<longleftrightarrow>
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    49
    (let ks = map fst xs; ls = map fst ys
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    50
     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))"
44897
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    51
proof -
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    52
  have *: "(a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs" for a b xs
44897
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    53
    by (auto simp add: image_def intro!: bexI)
63476
wenzelm
parents: 63462
diff changeset
    54
  show ?thesis
wenzelm
parents: 63462
diff changeset
    55
    apply transfer
wenzelm
parents: 63462
diff changeset
    56
    apply (auto intro!: map_of_eqI)
wenzelm
parents: 63462
diff changeset
    57
     apply (auto dest!: map_of_eq_dom intro: *)
wenzelm
parents: 63462
diff changeset
    58
    done
44897
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    59
qed
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    60
63194
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 60500
diff changeset
    61
lemma map_values_Mapping [code]:
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    62
  "Mapping.map_values f (Mapping xs) = Mapping (map (\<lambda>(x,y). (x, f x y)) xs)"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    63
  for f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b" and xs :: "('c \<times> 'a) list"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    64
  apply transfer
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    65
  apply (rule ext)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    66
  subgoal for f xs x by (induct xs) auto
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    67
  done
63194
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 60500
diff changeset
    68
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    69
lemma combine_with_key_code [code]:
63195
f3f08c0d4aaf Tuned code equations for mappings and PMFs
eberlm
parents: 63194
diff changeset
    70
  "Mapping.combine_with_key f (Mapping xs) (Mapping ys) =
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    71
     Mapping.tabulate (remdups (map fst xs @ map fst ys))
63195
f3f08c0d4aaf Tuned code equations for mappings and PMFs
eberlm
parents: 63194
diff changeset
    72
       (\<lambda>x. the (combine_options (f x) (map_of xs x) (map_of ys x)))"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    73
  apply transfer
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    74
  apply (rule ext)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    75
  apply (rule sym)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    76
  subgoal for f xs ys x
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    77
    apply (cases "map_of xs x"; cases "map_of ys x"; simp)
63476
wenzelm
parents: 63462
diff changeset
    78
       apply (force simp: map_of_eq_None_iff combine_options_def option.the_def o_def image_iff
wenzelm
parents: 63462
diff changeset
    79
        dest: map_of_SomeD split: option.splits)+
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    80
    done
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    81
  done
63195
f3f08c0d4aaf Tuned code equations for mappings and PMFs
eberlm
parents: 63194
diff changeset
    82
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    83
lemma combine_code [code]:
63194
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 60500
diff changeset
    84
  "Mapping.combine f (Mapping xs) (Mapping ys) =
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    85
     Mapping.tabulate (remdups (map fst xs @ map fst ys))
63194
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 60500
diff changeset
    86
       (\<lambda>x. the (combine_options f (map_of xs x) (map_of ys x)))"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    87
  apply transfer
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    88
  apply (rule ext)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    89
  apply (rule sym)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    90
  subgoal for f xs ys x
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    91
    apply (cases "map_of xs x"; cases "map_of ys x"; simp)
63476
wenzelm
parents: 63462
diff changeset
    92
       apply (force simp: map_of_eq_None_iff combine_options_def option.the_def o_def image_iff
wenzelm
parents: 63462
diff changeset
    93
        dest: map_of_SomeD split: option.splits)+
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    94
    done
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    95
  done
63194
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 60500
diff changeset
    96
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    97
lemma map_of_filter_distinct:  (* TODO: move? *)
63194
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 60500
diff changeset
    98
  assumes "distinct (map fst xs)"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
    99
  shows "map_of (filter P xs) x =
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
   100
    (case map_of xs x of
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
   101
      None \<Rightarrow> None
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
   102
    | Some y \<Rightarrow> if P (x,y) then Some y else None)"
63194
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 60500
diff changeset
   103
  using assms
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 60500
diff changeset
   104
  by (auto simp: map_of_eq_None_iff filter_map distinct_map_filter dest: map_of_SomeD
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
   105
      simp del: map_of_eq_Some_iff intro!: map_of_is_SomeI split: option.splits)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
   106
63194
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 60500
diff changeset
   107
lemma filter_Mapping [code]:
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 60500
diff changeset
   108
  "Mapping.filter P (Mapping xs) = Mapping (filter (\<lambda>(k,v). P k v) (AList.clearjunk xs))"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
   109
  apply transfer
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
   110
  apply (rule ext)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
   111
  apply (subst map_of_filter_distinct)
63476
wenzelm
parents: 63462
diff changeset
   112
   apply (simp_all add: map_of_clearjunk split: option.split)
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
   113
  done
63194
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 60500
diff changeset
   114
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 63195
diff changeset
   115
lemma [code nbe]: "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True"
44897
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
   116
  by (fact equal_refl)
59487
adaa430fc0f7 default abstypes and default abstract equations make technical (no_code) annotation superfluous
haftmann
parents: 58881
diff changeset
   117
44913
48240fb48980 correcting theory name and dependencies
bulwahn
parents: 44897
diff changeset
   118
end