src/HOL/Library/Finite_Map.thy
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 64267 b9a1486e79be
child 66267 04b626416eae
permissions -rw-r--r--
tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     1
(*  Title:      HOL/Library/Finite_Map.thy
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     2
    Author:     Lars Hupel, TU M√ľnchen
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     3
*)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     4
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     5
section \<open>Type of finite maps defined as a subtype of maps\<close>
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     6
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     7
theory Finite_Map
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     8
  imports FSet AList
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     9
begin
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    10
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    11
subsection \<open>Auxiliary constants and lemmas over @{type map}\<close>
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    12
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    13
context includes lifting_syntax begin
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    14
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    15
abbreviation rel_map :: "('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'c) \<Rightarrow> bool" where
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    16
"rel_map f \<equiv> op = ===> rel_option f"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    17
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    18
lemma map_empty_transfer[transfer_rule]: "rel_map A Map.empty Map.empty"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    19
by transfer_prover
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    20
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    21
lemma ran_transfer[transfer_rule]: "(rel_map A ===> rel_set A) ran ran"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    22
proof
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    23
  fix m n
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    24
  assume "rel_map A m n"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    25
  show "rel_set A (ran m) (ran n)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    26
    proof (rule rel_setI)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    27
      fix x
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    28
      assume "x \<in> ran m"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    29
      then obtain a where "m a = Some x"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    30
        unfolding ran_def by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    31
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    32
      have "rel_option A (m a) (n a)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    33
        using \<open>rel_map A m n\<close>
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    34
        by (auto dest: rel_funD)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    35
      then obtain y where "n a = Some y" "A x y"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    36
        unfolding \<open>m a = _\<close>
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    37
        by cases auto
64180
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
    38
      then show "\<exists>y \<in> ran n. A x y"
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    39
        unfolding ran_def by blast
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    40
    next
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    41
      fix y
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    42
      assume "y \<in> ran n"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    43
      then obtain a where "n a = Some y"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    44
        unfolding ran_def by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    45
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    46
      have "rel_option A (m a) (n a)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    47
        using \<open>rel_map A m n\<close>
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    48
        by (auto dest: rel_funD)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    49
      then obtain x where "m a = Some x" "A x y"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    50
        unfolding \<open>n a = _\<close>
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    51
        by cases auto
64180
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
    52
      then show "\<exists>x \<in> ran m. A x y"
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    53
        unfolding ran_def by blast
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    54
    qed
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    55
qed
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    56
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    57
lemma ran_alt_def: "ran m = (the \<circ> m) ` dom m"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    58
unfolding ran_def dom_def by force
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    59
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    60
lemma dom_transfer[transfer_rule]: "(rel_map A ===> op =) dom dom"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    61
proof
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    62
  fix m n
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    63
  assume "rel_map A m n"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    64
  have "m a \<noteq> None \<longleftrightarrow> n a \<noteq> None" for a
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    65
    proof -
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    66
      from \<open>rel_map A m n\<close> have "rel_option A (m a) (n a)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    67
        unfolding rel_fun_def by auto
64180
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
    68
      then show ?thesis
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    69
        by cases auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    70
    qed
64180
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
    71
  then show "dom m = dom n"
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    72
    by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    73
qed
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    74
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    75
definition map_upd :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    76
"map_upd k v m = m(k \<mapsto> v)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    77
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    78
lemma map_upd_transfer[transfer_rule]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    79
  "(op = ===> A ===> rel_map A ===> rel_map A) map_upd map_upd"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    80
unfolding map_upd_def[abs_def]
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    81
by transfer_prover
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    82
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    83
definition map_filter :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    84
"map_filter P m = (\<lambda>x. if P x then m x else None)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    85
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    86
lemma map_filter_map_of[simp]: "map_filter P (map_of m) = map_of [(k, _) \<leftarrow> m. P k]"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    87
proof
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    88
  fix x
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    89
  show "map_filter P (map_of m) x = map_of [(k, _) \<leftarrow> m. P k] x"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    90
    by (induct m) (auto simp: map_filter_def)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    91
qed
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    92
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    93
lemma map_filter_transfer[transfer_rule]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    94
  "(op = ===> rel_map A ===> rel_map A) map_filter map_filter"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    95
unfolding map_filter_def[abs_def]
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    96
by transfer_prover
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    97
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    98
lemma map_filter_finite[intro]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    99
  assumes "finite (dom m)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   100
  shows "finite (dom (map_filter P m))"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   101
proof -
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   102
  have "dom (map_filter P m) = Set.filter P (dom m)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   103
    unfolding map_filter_def Set.filter_def dom_def
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   104
    by auto
64180
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   105
  then show ?thesis
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   106
    using assms
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   107
    by (simp add: Set.filter_def)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   108
qed
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   109
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   110
definition map_drop :: "'a \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   111
"map_drop a = map_filter (\<lambda>a'. a' \<noteq> a)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   112
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   113
lemma map_drop_transfer[transfer_rule]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   114
  "(op = ===> rel_map A ===> rel_map A) map_drop map_drop"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   115
unfolding map_drop_def[abs_def]
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   116
by transfer_prover
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   117
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   118
definition map_drop_set :: "'a set \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   119
"map_drop_set A = map_filter (\<lambda>a. a \<notin> A)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   120
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   121
lemma map_drop_set_transfer[transfer_rule]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   122
  "(op = ===> rel_map A ===> rel_map A) map_drop_set map_drop_set"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   123
unfolding map_drop_set_def[abs_def]
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   124
by transfer_prover
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   125
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   126
definition map_restrict_set :: "'a set \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   127
"map_restrict_set A = map_filter (\<lambda>a. a \<in> A)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   128
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   129
lemma map_restrict_set_transfer[transfer_rule]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   130
  "(op = ===> rel_map A ===> rel_map A) map_restrict_set map_restrict_set"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   131
unfolding map_restrict_set_def[abs_def]
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   132
by transfer_prover
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   133
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   134
lemma map_add_transfer[transfer_rule]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   135
  "(rel_map A ===> rel_map A ===> rel_map A) op ++ op ++"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   136
unfolding map_add_def[abs_def]
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   137
by transfer_prover
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   138
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   139
definition map_pred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> bool" where
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   140
"map_pred P m \<longleftrightarrow> (\<forall>x. case m x of None \<Rightarrow> True | Some y \<Rightarrow> P x y)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   141
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   142
lemma map_pred_transfer[transfer_rule]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   143
  "((op = ===> A ===> op =) ===> rel_map A ===> op =) map_pred map_pred"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   144
unfolding map_pred_def[abs_def]
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   145
by transfer_prover
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   146
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   147
definition rel_map_on_set :: "'a set \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'c) \<Rightarrow> bool" where
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   148
"rel_map_on_set S P = eq_onp (\<lambda>x. x \<in> S) ===> rel_option P"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   149
  
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   150
lemma map_of_transfer[transfer_rule]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   151
  includes lifting_syntax
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   152
  shows "(list_all2 (rel_prod op = A) ===> rel_map A) map_of map_of"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   153
unfolding map_of_def by transfer_prover
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   154
  
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   155
end
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   156
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   157
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   158
subsection \<open>Abstract characterisation\<close>
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   159
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   160
typedef ('a, 'b) fmap = "{m. finite (dom m)} :: ('a \<rightharpoonup> 'b) set"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   161
  morphisms fmlookup Abs_fmap
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   162
proof
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   163
  show "Map.empty \<in> {m. finite (dom m)}"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   164
    by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   165
qed
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   166
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   167
setup_lifting type_definition_fmap
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   168
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   169
lemma fmlookup_finite[intro, simp]: "finite (dom (fmlookup m))"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   170
using fmap.fmlookup by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   171
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   172
lemma fmap_ext:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   173
  assumes "\<And>x. fmlookup m x = fmlookup n x"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   174
  shows "m = n"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   175
using assms
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   176
by transfer' auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   177
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   178
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   179
subsection \<open>Operations\<close>
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   180
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   181
context
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   182
  includes fset.lifting
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   183
begin
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   184
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   185
lift_definition fmran :: "('a, 'b) fmap \<Rightarrow> 'b fset"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   186
  is ran
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   187
  parametric ran_transfer
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   188
unfolding ran_alt_def by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   189
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   190
lemma fmranI: "fmlookup m x = Some y \<Longrightarrow> y |\<in>| fmran m" by transfer' (auto simp: ran_def)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   191
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   192
lift_definition fmdom :: "('a, 'b) fmap \<Rightarrow> 'a fset"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   193
  is dom
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   194
  parametric dom_transfer
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   195
.
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   196
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   197
lemma fmdom_notI: "fmlookup m x = None \<Longrightarrow> x |\<notin>| fmdom m" by transfer' auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   198
lemma fmdomI: "fmlookup m x = Some y \<Longrightarrow> x |\<in>| fmdom m" by transfer' auto
63900
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   199
lemma fmdom_notD: "x |\<notin>| fmdom m \<Longrightarrow> fmlookup m x = None" by transfer' auto
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   200
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   201
lift_definition fmdom' :: "('a, 'b) fmap \<Rightarrow> 'a set"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   202
  is dom
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   203
  parametric dom_transfer
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   204
.
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   205
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   206
lemma fmdom'_notI: "fmlookup m x = None \<Longrightarrow> x \<notin> fmdom' m" by transfer' auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   207
lemma fmdom'I: "fmlookup m x = Some y \<Longrightarrow> x \<in> fmdom' m" by transfer' auto
63900
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   208
lemma fmdom'_notD: "x \<notin> fmdom' m \<Longrightarrow> fmlookup m x = None" by transfer' auto
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   209
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   210
lemma fmdom'_alt_def: "fmdom' = fset \<circ> fmdom"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   211
by transfer' force
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   212
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   213
lemma fmlookup_dom_iff: "x |\<in>| fmdom m \<longleftrightarrow> (\<exists>a. fmlookup m x = Some a)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   214
by transfer' auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   215
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   216
lift_definition fmempty :: "('a, 'b) fmap"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   217
  is Map.empty
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   218
  parametric map_empty_transfer
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   219
by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   220
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   221
lemma fmempty_lookup[simp]: "fmlookup fmempty x = None"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   222
by transfer' simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   223
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   224
lemma fmdom_empty[simp]: "fmdom fmempty = {||}" by transfer' simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   225
lemma fmdom'_empty[simp]: "fmdom' fmempty = {}" by transfer' simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   226
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   227
lift_definition fmupd :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   228
  is map_upd
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   229
  parametric map_upd_transfer
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   230
unfolding map_upd_def[abs_def]
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   231
by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   232
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   233
lemma fmupd_lookup[simp]: "fmlookup (fmupd a b m) a' = (if a = a' then Some b else fmlookup m a')"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   234
by transfer' (auto simp: map_upd_def)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   235
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   236
lemma fmdom_fmupd[simp]: "fmdom (fmupd a b m) = finsert a (fmdom m)" by transfer (simp add: map_upd_def)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   237
lemma fmdom'_fmupd[simp]: "fmdom' (fmupd a b m) = insert a (fmdom' m)" by transfer (simp add: map_upd_def)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   238
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   239
lift_definition fmfilter :: "('a \<Rightarrow> bool) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   240
  is map_filter
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   241
  parametric map_filter_transfer
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   242
by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   243
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   244
lemma fmdom_filter[simp]: "fmdom (fmfilter P m) = ffilter P (fmdom m)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   245
by transfer' (auto simp: map_filter_def Set.filter_def split: if_splits)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   246
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   247
lemma fmdom'_filter[simp]: "fmdom' (fmfilter P m) = Set.filter P (fmdom' m)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   248
by transfer' (auto simp: map_filter_def Set.filter_def split: if_splits)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   249
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   250
lemma fmlookup_filter[simp]: "fmlookup (fmfilter P m) x = (if P x then fmlookup m x else None)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   251
by transfer' (auto simp: map_filter_def)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   252
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   253
lemma fmfilter_empty[simp]: "fmfilter P fmempty = fmempty"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   254
by transfer' (auto simp: map_filter_def)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   255
63900
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   256
lemma fmfilter_true[simp]:
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   257
  assumes "\<And>x. x |\<in>| fmdom m \<Longrightarrow> P x"
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   258
  shows "fmfilter P m = m"
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   259
proof (rule fmap_ext)
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   260
  fix x
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   261
  have "fmlookup m x = None" if "\<not> P x"
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   262
    using that assms
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   263
    unfolding fmlookup_dom_iff by fastforce
64180
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   264
  then show "fmlookup (fmfilter P m) x = fmlookup m x"
63900
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   265
    by simp
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   266
qed
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   267
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   268
lemma fmfilter_false[simp]: "(\<And>x. x |\<in>| fmdom m \<Longrightarrow> \<not> P x) \<Longrightarrow> fmfilter P m = fmempty"
63900
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   269
by transfer' (auto simp: map_filter_def fun_eq_iff)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   270
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   271
lemma fmfilter_comp[simp]: "fmfilter P (fmfilter Q m) = fmfilter (\<lambda>x. P x \<and> Q x) m"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   272
by transfer' (auto simp: map_filter_def)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   273
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   274
lemma fmfilter_comm: "fmfilter P (fmfilter Q m) = fmfilter Q (fmfilter P m)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   275
unfolding fmfilter_comp by meson
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   276
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   277
lemma fmfilter_cong[cong]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   278
  assumes "\<And>x. x |\<in>| fmdom m \<Longrightarrow> P x = Q x"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   279
  shows "fmfilter P m = fmfilter Q m"
63900
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   280
proof (rule fmap_ext)
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   281
  fix x
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   282
  have "fmlookup m x = None" if "P x \<noteq> Q x"
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   283
    using that assms
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   284
    unfolding fmlookup_dom_iff by fastforce
64180
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   285
  then show "fmlookup (fmfilter P m) x = fmlookup (fmfilter Q m) x"
63900
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   286
    by auto
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   287
qed
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   288
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   289
lemma fmfilter_cong'[fundef_cong]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   290
  assumes "\<And>x. x \<in> fmdom' m \<Longrightarrow> P x = Q x"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   291
  shows "fmfilter P m = fmfilter Q m"
63900
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   292
proof (rule fmfilter_cong)
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   293
  fix x
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   294
  assume "x |\<in>| fmdom m"
64180
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   295
  then show "P x = Q x"
63900
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   296
    using assms
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   297
    unfolding fmdom'_alt_def fmember.rep_eq
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   298
    by auto
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   299
qed
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   300
63900
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   301
lemma fmfilter_upd[simp]:
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   302
  "fmfilter P (fmupd x y m) = (if P x then fmupd x y (fmfilter P m) else fmfilter P m)"
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   303
by transfer' (auto simp: map_upd_def map_filter_def)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   304
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   305
lift_definition fmdrop :: "'a \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   306
  is map_drop
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   307
  parametric map_drop_transfer
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   308
unfolding map_drop_def by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   309
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   310
lemma fmdrop_lookup[simp]: "fmlookup (fmdrop a m) a = None"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   311
by transfer' (auto simp: map_drop_def map_filter_def)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   312
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   313
lift_definition fmdrop_set :: "'a set \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   314
  is map_drop_set
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   315
  parametric map_drop_set_transfer
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   316
unfolding map_drop_set_def by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   317
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   318
lift_definition fmdrop_fset :: "'a fset \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   319
  is map_drop_set
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   320
  parametric map_drop_set_transfer
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   321
unfolding map_drop_set_def by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   322
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   323
lift_definition fmrestrict_set :: "'a set \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   324
  is map_restrict_set
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   325
  parametric map_restrict_set_transfer
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   326
unfolding map_restrict_set_def by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   327
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   328
lift_definition fmrestrict_fset :: "'a fset \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   329
  is map_restrict_set
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   330
  parametric map_restrict_set_transfer
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   331
unfolding map_restrict_set_def by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   332
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   333
lemma fmfilter_alt_defs:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   334
  "fmdrop a = fmfilter (\<lambda>a'. a' \<noteq> a)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   335
  "fmdrop_set A = fmfilter (\<lambda>a. a \<notin> A)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   336
  "fmdrop_fset B = fmfilter (\<lambda>a. a |\<notin>| B)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   337
  "fmrestrict_set A = fmfilter (\<lambda>a. a \<in> A)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   338
  "fmrestrict_fset B = fmfilter (\<lambda>a. a |\<in>| B)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   339
by (transfer'; simp add: map_drop_def map_drop_set_def map_restrict_set_def)+
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   340
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   341
lemma fmdom_drop[simp]: "fmdom (fmdrop a m) = fmdom m - {|a|}" unfolding fmfilter_alt_defs by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   342
lemma fmdom'_drop[simp]: "fmdom' (fmdrop a m) = fmdom' m - {a}" unfolding fmfilter_alt_defs by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   343
lemma fmdom'_drop_set[simp]: "fmdom' (fmdrop_set A m) = fmdom' m - A" unfolding fmfilter_alt_defs by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   344
lemma fmdom_drop_fset[simp]: "fmdom (fmdrop_fset A m) = fmdom m - A" unfolding fmfilter_alt_defs by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   345
lemma fmdom'_restrict_set: "fmdom' (fmrestrict_set A m) \<subseteq> A" unfolding fmfilter_alt_defs by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   346
lemma fmdom_restrict_fset: "fmdom (fmrestrict_fset A m) |\<subseteq>| A" unfolding fmfilter_alt_defs by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   347
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   348
lemma fmdom'_drop_fset[simp]: "fmdom' (fmdrop_fset A m) = fmdom' m - fset A"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   349
unfolding fmfilter_alt_defs by transfer' (auto simp: map_filter_def split: if_splits)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   350
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   351
lemma fmdom'_restrict_fset: "fmdom' (fmrestrict_fset A m) \<subseteq> fset A"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   352
unfolding fmfilter_alt_defs by transfer' (auto simp: map_filter_def)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   353
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   354
lemma fmlookup_drop[simp]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   355
  "fmlookup (fmdrop a m) x = (if x \<noteq> a then fmlookup m x else None)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   356
unfolding fmfilter_alt_defs by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   357
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   358
lemma fmlookup_drop_set[simp]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   359
  "fmlookup (fmdrop_set A m) x = (if x \<notin> A then fmlookup m x else None)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   360
unfolding fmfilter_alt_defs by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   361
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   362
lemma fmlookup_drop_fset[simp]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   363
  "fmlookup (fmdrop_fset A m) x = (if x |\<notin>| A then fmlookup m x else None)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   364
unfolding fmfilter_alt_defs by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   365
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   366
lemma fmlookup_restrict_set[simp]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   367
  "fmlookup (fmrestrict_set A m) x = (if x \<in> A then fmlookup m x else None)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   368
unfolding fmfilter_alt_defs by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   369
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   370
lemma fmlookup_restrict_fset[simp]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   371
  "fmlookup (fmrestrict_fset A m) x = (if x |\<in>| A then fmlookup m x else None)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   372
unfolding fmfilter_alt_defs by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   373
63900
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   374
lemma fmrestrict_set_dom[simp]: "fmrestrict_set (fmdom' m) m = m"
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   375
  by (rule fmap_ext) (auto dest: fmdom'_notD)
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   376
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   377
lemma fmrestrict_fset_dom[simp]: "fmrestrict_fset (fmdom m) m = m"
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   378
  by (rule fmap_ext) (auto dest: fmdom_notD)
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   379
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   380
lemma fmdrop_empty[simp]: "fmdrop a fmempty = fmempty"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   381
  unfolding fmfilter_alt_defs by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   382
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   383
lemma fmdrop_set_empty[simp]: "fmdrop_set A fmempty = fmempty"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   384
  unfolding fmfilter_alt_defs by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   385
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   386
lemma fmdrop_fset_empty[simp]: "fmdrop_fset A fmempty = fmempty"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   387
  unfolding fmfilter_alt_defs by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   388
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   389
lemma fmrestrict_set_empty[simp]: "fmrestrict_set A fmempty = fmempty"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   390
  unfolding fmfilter_alt_defs by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   391
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   392
lemma fmrestrict_fset_empty[simp]: "fmrestrict_fset A fmempty = fmempty"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   393
  unfolding fmfilter_alt_defs by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   394
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   395
lemma fmdrop_set_single[simp]: "fmdrop_set {a} m = fmdrop a m"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   396
  unfolding fmfilter_alt_defs by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   397
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   398
lemma fmdrop_fset_single[simp]: "fmdrop_fset {|a|} m = fmdrop a m"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   399
  unfolding fmfilter_alt_defs by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   400
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   401
lemma fmrestrict_set_null[simp]: "fmrestrict_set {} m = fmempty"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   402
  unfolding fmfilter_alt_defs by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   403
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   404
lemma fmrestrict_fset_null[simp]: "fmrestrict_fset {||} m = fmempty"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   405
  unfolding fmfilter_alt_defs by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   406
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   407
lemma fmdrop_comm: "fmdrop a (fmdrop b m) = fmdrop b (fmdrop a m)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   408
unfolding fmfilter_alt_defs by (rule fmfilter_comm)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   409
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   410
lift_definition fmadd :: "('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap" (infixl "++\<^sub>f" 100)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   411
  is map_add
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   412
  parametric map_add_transfer
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   413
by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   414
63900
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   415
lemma fmlookup_add[simp]:
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   416
  "fmlookup (m ++\<^sub>f n) x = (if x |\<in>| fmdom n then fmlookup n x else fmlookup m x)"
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   417
  by transfer' (auto simp: map_add_def split: option.splits)
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   418
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   419
lemma fmdom_add[simp]: "fmdom (m ++\<^sub>f n) = fmdom m |\<union>| fmdom n" by transfer' auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   420
lemma fmdom'_add[simp]: "fmdom' (m ++\<^sub>f n) = fmdom' m \<union> fmdom' n" by transfer' auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   421
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   422
lemma fmadd_drop_left_dom: "fmdrop_fset (fmdom n) m ++\<^sub>f n = m ++\<^sub>f n"
63900
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   423
  by (rule fmap_ext) auto
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   424
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   425
lemma fmadd_restrict_right_dom: "fmrestrict_fset (fmdom n) (m ++\<^sub>f n) = n"
63900
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   426
  by (rule fmap_ext) (auto dest: fmdom_notD)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   427
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   428
lemma fmfilter_add_distrib[simp]: "fmfilter P (m ++\<^sub>f n) = fmfilter P m ++\<^sub>f fmfilter P n"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   429
by transfer' (auto simp: map_filter_def map_add_def)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   430
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   431
lemma fmdrop_add_distrib[simp]: "fmdrop a (m ++\<^sub>f n) = fmdrop a m ++\<^sub>f fmdrop a n"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   432
  unfolding fmfilter_alt_defs by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   433
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   434
lemma fmdrop_set_add_distrib[simp]: "fmdrop_set A (m ++\<^sub>f n) = fmdrop_set A m ++\<^sub>f fmdrop_set A n"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   435
  unfolding fmfilter_alt_defs by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   436
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   437
lemma fmdrop_fset_add_distrib[simp]: "fmdrop_fset A (m ++\<^sub>f n) = fmdrop_fset A m ++\<^sub>f fmdrop_fset A n"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   438
  unfolding fmfilter_alt_defs by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   439
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   440
lemma fmrestrict_set_add_distrib[simp]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   441
  "fmrestrict_set A (m ++\<^sub>f n) = fmrestrict_set A m ++\<^sub>f fmrestrict_set A n"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   442
  unfolding fmfilter_alt_defs by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   443
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   444
lemma fmrestrict_fset_add_distrib[simp]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   445
  "fmrestrict_fset A (m ++\<^sub>f n) = fmrestrict_fset A m ++\<^sub>f fmrestrict_fset A n"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   446
  unfolding fmfilter_alt_defs by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   447
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   448
lemma fmadd_empty[simp]: "fmempty ++\<^sub>f m = m" "m ++\<^sub>f fmempty = m"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   449
by (transfer'; auto)+
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   450
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   451
lemma fmadd_idempotent[simp]: "m ++\<^sub>f m = m"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   452
by transfer' (auto simp: map_add_def split: option.splits)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   453
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   454
lemma fmadd_assoc[simp]: "m ++\<^sub>f (n ++\<^sub>f p) = m ++\<^sub>f n ++\<^sub>f p"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   455
by transfer' simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   456
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   457
lift_definition fmpred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> bool"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   458
  is map_pred
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   459
  parametric map_pred_transfer
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   460
.
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   461
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   462
lemma fmpredI[intro]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   463
  assumes "\<And>x y. fmlookup m x = Some y \<Longrightarrow> P x y"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   464
  shows "fmpred P m"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   465
using assms
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   466
by transfer' (auto simp: map_pred_def split: option.splits)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   467
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   468
lemma fmpredD[dest]: "fmpred P m \<Longrightarrow> fmlookup m x = Some y \<Longrightarrow> P x y" 
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   469
by transfer' (auto simp: map_pred_def split: option.split_asm)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   470
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   471
lemma fmpred_iff: "fmpred P m \<longleftrightarrow> (\<forall>x y. fmlookup m x = Some y \<longrightarrow> P x y)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   472
by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   473
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   474
lemma fmpred_alt_def: "fmpred P m \<longleftrightarrow> fBall (fmdom m) (\<lambda>x. P x (the (fmlookup m x)))"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   475
unfolding fmpred_iff
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   476
apply auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   477
apply (subst (asm) fmlookup_dom_iff)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   478
apply simp
63900
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   479
apply (rename_tac x y)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   480
apply (erule_tac x = x in fBallE)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   481
apply simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   482
by (simp add: fmlookup_dom_iff)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   483
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   484
lemma fmpred_empty[intro!, simp]: "fmpred P fmempty"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   485
by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   486
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   487
lemma fmpred_upd[intro]: "fmpred P m \<Longrightarrow> P x y \<Longrightarrow> fmpred P (fmupd x y m)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   488
by transfer' (auto simp: map_pred_def map_upd_def)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   489
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   490
lemma fmpred_updD[dest]: "fmpred P (fmupd x y m) \<Longrightarrow> P x y"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   491
by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   492
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   493
lemma fmpred_add[intro]: "fmpred P m \<Longrightarrow> fmpred P n \<Longrightarrow> fmpred P (m ++\<^sub>f n)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   494
by transfer' (auto simp: map_pred_def map_add_def split: option.splits)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   495
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   496
lemma fmpred_filter[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmfilter Q m)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   497
by transfer' (auto simp: map_pred_def map_filter_def)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   498
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   499
lemma fmpred_drop[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop a m)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   500
  by (auto simp: fmfilter_alt_defs)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   501
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   502
lemma fmpred_drop_set[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop_set A m)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   503
  by (auto simp: fmfilter_alt_defs)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   504
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   505
lemma fmpred_drop_fset[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop_fset A m)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   506
  by (auto simp: fmfilter_alt_defs)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   507
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   508
lemma fmpred_restrict_set[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmrestrict_set A m)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   509
  by (auto simp: fmfilter_alt_defs)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   510
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   511
lemma fmpred_restrict_fset[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmrestrict_fset A m)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   512
  by (auto simp: fmfilter_alt_defs)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   513
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   514
lemma fmpred_cases[consumes 1]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   515
  assumes "fmpred P m"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   516
  obtains (none) "fmlookup m x = None" | (some) y where "fmlookup m x = Some y" "P x y"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   517
using assms by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   518
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   519
lift_definition fmsubset :: "('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap \<Rightarrow> bool" (infix "\<subseteq>\<^sub>f" 50)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   520
  is map_le
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   521
.
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   522
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   523
lemma fmsubset_alt_def: "m \<subseteq>\<^sub>f n \<longleftrightarrow> fmpred (\<lambda>k v. fmlookup n k = Some v) m"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   524
by transfer' (auto simp: map_pred_def map_le_def dom_def split: option.splits)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   525
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   526
lemma fmsubset_pred: "fmpred P m \<Longrightarrow> n \<subseteq>\<^sub>f m \<Longrightarrow> fmpred P n"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   527
unfolding fmsubset_alt_def fmpred_iff
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   528
by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   529
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   530
lemma fmsubset_filter_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmfilter P m \<subseteq>\<^sub>f fmfilter P n"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   531
unfolding fmsubset_alt_def fmpred_iff
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   532
by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   533
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   534
lemma fmsubset_drop_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmdrop a m \<subseteq>\<^sub>f fmdrop a n"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   535
unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   536
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   537
lemma fmsubset_drop_set_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmdrop_set A m \<subseteq>\<^sub>f fmdrop_set A n"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   538
unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   539
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   540
lemma fmsubset_drop_fset_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmdrop_fset A m \<subseteq>\<^sub>f fmdrop_fset A n"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   541
unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   542
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   543
lemma fmsubset_restrict_set_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmrestrict_set A m \<subseteq>\<^sub>f fmrestrict_set A n"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   544
unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   545
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   546
lemma fmsubset_restrict_fset_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmrestrict_fset A m \<subseteq>\<^sub>f fmrestrict_fset A n"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   547
unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   548
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   549
lift_definition fmap_of_list :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) fmap"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   550
  is map_of
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   551
  parametric map_of_transfer
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   552
by (rule finite_dom_map_of)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   553
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   554
lemma fmap_of_list_simps[simp]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   555
  "fmap_of_list [] = fmempty"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   556
  "fmap_of_list ((k, v) # kvs) = fmupd k v (fmap_of_list kvs)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   557
by (transfer, simp add: map_upd_def)+
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   558
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   559
lemma fmap_of_list_app[simp]: "fmap_of_list (xs @ ys) = fmap_of_list ys ++\<^sub>f fmap_of_list xs"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   560
by transfer' simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   561
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   562
lemma fmupd_alt_def: "fmupd k v m = m ++\<^sub>f fmap_of_list [(k, v)]"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   563
by transfer' (auto simp: map_upd_def)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   564
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   565
lemma fmpred_of_list[intro]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   566
  assumes "\<And>k v. (k, v) \<in> set xs \<Longrightarrow> P k v"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   567
  shows "fmpred P (fmap_of_list xs)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   568
using assms
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   569
by (induction xs) (transfer'; auto simp: map_pred_def)+
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   570
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   571
lemma fmap_of_list_SomeD: "fmlookup (fmap_of_list xs) k = Some v \<Longrightarrow> (k, v) \<in> set xs"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   572
by transfer' (auto dest: map_of_SomeD)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   573
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   574
lift_definition fmrel_on_set :: "'a set \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'c) fmap \<Rightarrow> bool"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   575
  is rel_map_on_set
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   576
.
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   577
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   578
lift_definition fmrel_on_fset :: "'a fset \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'c) fmap \<Rightarrow> bool"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   579
  is rel_map_on_set
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   580
.
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   581
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   582
lemma fmrel_on_fset_alt_def: "fmrel_on_fset S P m n \<longleftrightarrow> fBall S (\<lambda>x. rel_option P (fmlookup m x) (fmlookup n x))"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   583
by transfer' (auto simp: rel_map_on_set_def eq_onp_def rel_fun_def)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   584
64181
4d1d2de432fa renamed lemma to a more consistent name
Lars Hupel <lars.hupel@mytum.de>
parents: 64180
diff changeset
   585
lemma fmrel_on_fsetI[intro]:
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   586
  assumes "\<And>x. x |\<in>| S \<Longrightarrow> rel_option P (fmlookup m x) (fmlookup n x)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   587
  shows "fmrel_on_fset S P m n"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   588
using assms
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   589
unfolding fmrel_on_fset_alt_def by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   590
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   591
lemma fmrel_on_fset_mono[mono]: "R \<le> Q \<Longrightarrow> fmrel_on_fset S R \<le> fmrel_on_fset S Q"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   592
unfolding fmrel_on_fset_alt_def[abs_def]
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   593
apply (intro le_funI fBall_mono)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   594
using option.rel_mono by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   595
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   596
lemma fmrel_on_fsetD: "x |\<in>| S \<Longrightarrow> fmrel_on_fset S P m n \<Longrightarrow> rel_option P (fmlookup m x) (fmlookup n x)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   597
unfolding fmrel_on_fset_alt_def
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   598
by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   599
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   600
lemma fmrel_on_fsubset: "fmrel_on_fset S R m n \<Longrightarrow> T |\<subseteq>| S \<Longrightarrow> fmrel_on_fset T R m n"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   601
unfolding fmrel_on_fset_alt_def
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   602
by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   603
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   604
end
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   605
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   606
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   607
subsection \<open>BNF setup\<close>
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   608
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   609
lift_bnf ('a, fmran': 'b) fmap [wits: Map.empty]
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   610
  for map: fmmap
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   611
      rel: fmrel
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   612
  by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   613
64180
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   614
text \<open>
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   615
  Unfortunately, @{command lift_bnf} doesn't register the definitional theorems. We're doing it
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   616
  manually below.
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   617
\<close>
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   618
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   619
local_setup \<open>fn lthy =>
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   620
  let
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   621
    val SOME bnf = BNF_Def.bnf_of lthy @{type_name fmap}
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   622
  in
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   623
    lthy
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   624
    |> Local_Theory.note ((@{binding fmmap_def}, []), [BNF_Def.map_def_of_bnf bnf]) |> #2
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   625
    |> Local_Theory.note ((@{binding fmran'_def}, []), BNF_Def.set_defs_of_bnf bnf) |> #2
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   626
    |> Local_Theory.note ((@{binding fmrel_def}, []), [BNF_Def.rel_def_of_bnf bnf]) |> #2
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   627
  end
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   628
\<close>
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   629
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   630
context includes lifting_syntax begin
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   631
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   632
lemma fmmap_transfer[transfer_rule]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   633
  "(op = ===> pcr_fmap op = op = ===> pcr_fmap op = op =) (\<lambda>f. op \<circ> (map_option f)) fmmap"
64180
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   634
  unfolding fmmap_def
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   635
  by (rule rel_funI ext)+ (auto simp: fmap.Abs_fmap_inverse fmap.pcr_cr_eq cr_fmap_def)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   636
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   637
lemma fmran'_transfer[transfer_rule]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   638
  "(pcr_fmap op = op = ===> op =) (\<lambda>x. UNION (range x) set_option) fmran'"
64180
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   639
  unfolding fmran'_def fmap.pcr_cr_eq cr_fmap_def by fastforce
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   640
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   641
lemma fmrel_transfer[transfer_rule]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   642
  "(op = ===> pcr_fmap op = op = ===> pcr_fmap op = op = ===> op =) rel_map fmrel"
64180
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   643
  unfolding fmrel_def fmap.pcr_cr_eq cr_fmap_def vimage2p_def by fastforce
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   644
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   645
end
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   646
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   647
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   648
lemma fmran'_alt_def: "fmran' = fset \<circ> fmran"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   649
including fset.lifting
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   650
by transfer' (auto simp: ran_def fun_eq_iff)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   651
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   652
lemma fmran'I: "fmlookup m x = Some y \<Longrightarrow> y \<in> fmran' m"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   653
by transfer' auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   654
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   655
lemma fmrel_iff: "fmrel R m n \<longleftrightarrow> (\<forall>x. rel_option R (fmlookup m x) (fmlookup n x))"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   656
by transfer' (auto simp: rel_fun_def)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   657
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   658
lemma fmrelI[intro]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   659
  assumes "\<And>x. rel_option R (fmlookup m x) (fmlookup n x)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   660
  shows "fmrel R m n"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   661
using assms
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   662
by transfer' auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   663
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   664
lemma fmempty_transfer[simp, intro, transfer_rule]: "fmrel P fmempty fmempty"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   665
by transfer auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   666
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   667
lemma fmrel_upd[intro]: "fmrel P m n \<Longrightarrow> P x y \<Longrightarrow> fmrel P (fmupd k x m) (fmupd k y n)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   668
by transfer' (auto simp: map_upd_def rel_fun_def)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   669
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   670
lemma fmrelD[dest]: "fmrel P m n \<Longrightarrow> rel_option P (fmlookup m x) (fmlookup n x)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   671
by transfer' (auto simp: rel_fun_def)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   672
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   673
lemma fmrel_addI[intro]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   674
  assumes "fmrel P m n" "fmrel P a b"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   675
  shows "fmrel P (m ++\<^sub>f a) (n ++\<^sub>f b)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   676
using assms
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   677
apply transfer'
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   678
apply (auto simp: rel_fun_def map_add_def)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   679
by (metis option.case_eq_if option.collapse option.rel_sel)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   680
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   681
lemma fmrel_cases[consumes 1]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   682
  assumes "fmrel P m n"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   683
  obtains (none) "fmlookup m x = None" "fmlookup n x = None"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   684
        | (some) a b where "fmlookup m x = Some a" "fmlookup n x = Some b" "P a b"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   685
proof -
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   686
  from assms have "rel_option P (fmlookup m x) (fmlookup n x)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   687
    by auto
64180
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   688
  then show thesis
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   689
    using none some
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   690
    by (cases rule: option.rel_cases) auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   691
qed
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   692
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   693
lemma fmrel_filter[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmfilter Q m) (fmfilter Q n)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   694
unfolding fmrel_iff by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   695
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   696
lemma fmrel_drop[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmdrop a m) (fmdrop a n)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   697
  unfolding fmfilter_alt_defs by blast
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   698
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   699
lemma fmrel_drop_set[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmdrop_set A m) (fmdrop_set A n)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   700
  unfolding fmfilter_alt_defs by blast
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   701
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   702
lemma fmrel_drop_fset[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmdrop_fset A m) (fmdrop_fset A n)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   703
  unfolding fmfilter_alt_defs by blast
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   704
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   705
lemma fmrel_restrict_set[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmrestrict_set A m) (fmrestrict_set A n)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   706
  unfolding fmfilter_alt_defs by blast
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   707
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   708
lemma fmrel_restrict_fset[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmrestrict_fset A m) (fmrestrict_fset A n)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   709
  unfolding fmfilter_alt_defs by blast
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   710
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   711
lemma pred_fmap_fmpred[simp]: "pred_fmap P = fmpred (\<lambda>_. P)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   712
unfolding fmap.pred_set fmran'_alt_def
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   713
including fset.lifting
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   714
apply transfer'
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   715
apply (rule ext)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   716
apply (auto simp: map_pred_def ran_def split: option.splits dest: )
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   717
done
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   718
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   719
lemma pred_fmap_id[simp]: "pred_fmap id (fmmap f m) \<longleftrightarrow> pred_fmap f m"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   720
unfolding fmap.pred_set fmap.set_map
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   721
by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   722
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   723
lemma fmlookup_map[simp]: "fmlookup (fmmap f m) x = map_option f (fmlookup m x)"
64180
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   724
by transfer' auto
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   725
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   726
lemma fmpred_map[simp]: "fmpred P (fmmap f m) \<longleftrightarrow> fmpred (\<lambda>k v. P k (f v)) m"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   727
unfolding fmpred_iff pred_fmap_def fmap.set_map
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   728
by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   729
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   730
lemma fmpred_id[simp]: "fmpred (\<lambda>_. id) (fmmap f m) \<longleftrightarrow> fmpred (\<lambda>_. f) m"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   731
by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   732
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   733
lemma fmmap_add[simp]: "fmmap f (m ++\<^sub>f n) = fmmap f m ++\<^sub>f fmmap f n"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   734
by transfer' (auto simp: map_add_def fun_eq_iff split: option.splits)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   735
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   736
lemma fmmap_empty[simp]: "fmmap f fmempty = fmempty"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   737
by transfer auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   738
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   739
lemma fmdom_map[simp]: "fmdom (fmmap f m) = fmdom m"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   740
including fset.lifting
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   741
by transfer' simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   742
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   743
lemma fmdom'_map[simp]: "fmdom' (fmmap f m) = fmdom' m"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   744
by transfer' simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   745
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   746
lemma fmfilter_fmmap[simp]: "fmfilter P (fmmap f m) = fmmap f (fmfilter P m)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   747
by transfer' (auto simp: map_filter_def)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   748
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   749
lemma fmdrop_fmmap[simp]: "fmdrop a (fmmap f m) = fmmap f (fmdrop a m)" unfolding fmfilter_alt_defs by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   750
lemma fmdrop_set_fmmap[simp]: "fmdrop_set A (fmmap f m) = fmmap f (fmdrop_set A m)" unfolding fmfilter_alt_defs by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   751
lemma fmdrop_fset_fmmap[simp]: "fmdrop_fset A (fmmap f m) = fmmap f (fmdrop_fset A m)" unfolding fmfilter_alt_defs by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   752
lemma fmrestrict_set_fmmap[simp]: "fmrestrict_set A (fmmap f m) = fmmap f (fmrestrict_set A m)" unfolding fmfilter_alt_defs by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   753
lemma fmrestrict_fset_fmmap[simp]: "fmrestrict_fset A (fmmap f m) = fmmap f (fmrestrict_fset A m)" unfolding fmfilter_alt_defs by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   754
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   755
lemma fmmap_subset[intro]: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmmap f m \<subseteq>\<^sub>f fmmap f n"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   756
by transfer' (auto simp: map_le_def)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   757
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   758
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   759
subsection \<open>Code setup\<close>
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   760
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   761
instantiation fmap :: (type, equal) equal begin
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   762
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   763
definition "equal_fmap \<equiv> fmrel HOL.equal"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   764
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   765
instance proof
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   766
  fix m n :: "('a, 'b) fmap"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   767
  have "fmrel op = m n \<longleftrightarrow> (m = n)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   768
    by transfer' (simp add: option.rel_eq rel_fun_eq)
64180
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   769
  then show "equal_class.equal m n \<longleftrightarrow> (m = n)"
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   770
    unfolding equal_fmap_def
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   771
    by (simp add: equal_eq[abs_def])
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   772
qed
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   773
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   774
end
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   775
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   776
lemma fBall_alt_def: "fBall S P \<longleftrightarrow> (\<forall>x. x |\<in>| S \<longrightarrow> P x)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   777
by force
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   778
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   779
lemma fmrel_code:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   780
  "fmrel R m n \<longleftrightarrow>
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   781
    fBall (fmdom m) (\<lambda>x. rel_option R (fmlookup m x) (fmlookup n x)) \<and>
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   782
    fBall (fmdom n) (\<lambda>x. rel_option R (fmlookup m x) (fmlookup n x))"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   783
unfolding fmrel_iff fmlookup_dom_iff fBall_alt_def
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   784
by (metis option.collapse option.rel_sel)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   785
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   786
lemmas fmap_generic_code =
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   787
  fmrel_code
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   788
  fmran'_alt_def
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   789
  fmdom'_alt_def
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   790
  fmfilter_alt_defs
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   791
  pred_fmap_fmpred
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   792
  fmsubset_alt_def
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   793
  fmupd_alt_def
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   794
  fmrel_on_fset_alt_def
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   795
  fmpred_alt_def
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   796
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   797
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   798
code_datatype fmap_of_list
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   799
quickcheck_generator fmap constructors: fmap_of_list
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   800
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   801
context includes fset.lifting begin
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   802
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   803
lemma [code]: "fmlookup (fmap_of_list m) = map_of m"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   804
by transfer simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   805
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   806
lemma [code]: "fmempty = fmap_of_list []"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   807
by transfer simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   808
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   809
lemma [code]: "fmran (fmap_of_list m) = snd |`| fset_of_list (AList.clearjunk m)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   810
by transfer (auto simp: ran_map_of)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   811
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   812
lemma [code]: "fmdom (fmap_of_list m) = fst |`| fset_of_list m"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   813
by transfer (auto simp: dom_map_of_conv_image_fst)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   814
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   815
lemma [code]: "fmfilter P (fmap_of_list m) = fmap_of_list (filter (\<lambda>(k, _). P k) m)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   816
by transfer' auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   817
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   818
lemma [code]: "fmap_of_list m ++\<^sub>f fmap_of_list n = fmap_of_list (AList.merge m n)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   819
by transfer (simp add: merge_conv')
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   820
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   821
lemma [code]: "fmmap f (fmap_of_list m) = fmap_of_list (map (apsnd f) m)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   822
apply transfer
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   823
apply (subst map_of_map[symmetric])
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   824
apply (auto simp: apsnd_def map_prod_def)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   825
done
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   826
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   827
end
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   828
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   829
declare fmap_generic_code[code]
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   830
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   831
lifting_update fmap.lifting
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   832
lifting_forget fmap.lifting
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   833
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64181
diff changeset
   834
end