src/HOL/Library/Finite_Map.thy
author wenzelm
Fri, 21 Mar 2025 22:26:18 +0100
changeset 82317 231b6d8231c6
parent 81113 6fefd6c602fa
permissions -rw-r--r--
more uniform Proof_Display.print_results for theory and proof output --- avoid loss of information seen in src/Doc/JEdit/document/output-and-state.png (the first bad changeset is f8c412a45af8, see also 53b59fa42696);
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
68462
8d1bf38c6fe6 simplify parametricity proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 68386
diff changeset
     8
  imports FSet AList Conditional_Parametricity
67780
7655e6369c9f more abbrevs -- this makes "(=" ambiguous and thus simplifies input of "(=)" (within the context of Main HOL);
wenzelm
parents: 67485
diff changeset
     9
  abbrevs "(=" = "\<subseteq>\<^sub>f"
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    10
begin
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    11
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69313
diff changeset
    12
subsection \<open>Auxiliary constants and lemmas over \<^type>\<open>map\<close>\<close>
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    13
68462
8d1bf38c6fe6 simplify parametricity proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 68386
diff changeset
    14
parametric_constant map_add_transfer[transfer_rule]: map_add_def
8d1bf38c6fe6 simplify parametricity proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 68386
diff changeset
    15
parametric_constant map_of_transfer[transfer_rule]: map_of_def
8d1bf38c6fe6 simplify parametricity proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 68386
diff changeset
    16
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    17
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
    18
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    19
abbreviation rel_map :: "('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'c) \<Rightarrow> bool" where
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 66398
diff changeset
    20
"rel_map f \<equiv> (=) ===> rel_option f"
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    21
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    22
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
    23
proof
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    24
  fix m n
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    25
  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
    26
  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
    27
    proof (rule rel_setI)
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    28
      fix x
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    29
      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
    30
      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
    31
        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
    32
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    33
      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
    34
        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
    35
        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
    36
      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
    37
        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
    38
        by cases auto
64180
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
    39
      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
    40
        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
    41
    next
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    42
      fix y
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    43
      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
    44
      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
    45
        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
    46
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    47
      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
    48
        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
    49
        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
    50
      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
    51
        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
    52
        by cases auto
64180
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
    53
      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
    54
        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
    55
    qed
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    56
qed
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    57
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    58
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
    59
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
    60
68462
8d1bf38c6fe6 simplify parametricity proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 68386
diff changeset
    61
parametric_constant dom_transfer[transfer_rule]: dom_def
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    62
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    63
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
    64
"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
    65
68462
8d1bf38c6fe6 simplify parametricity proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 68386
diff changeset
    66
parametric_constant map_upd_transfer[transfer_rule]: map_upd_def
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    67
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    68
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
    69
"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
    70
68462
8d1bf38c6fe6 simplify parametricity proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 68386
diff changeset
    71
parametric_constant map_filter_transfer[transfer_rule]: map_filter_def
8d1bf38c6fe6 simplify parametricity proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 68386
diff changeset
    72
68386
98cf1c823c48 Keep filter input syntax
nipkow
parents: 68249
diff changeset
    73
lemma map_filter_map_of[simp]: "map_filter P (map_of m) = map_of [(k, _) \<leftarrow> m. P k]"
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    74
proof
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    75
  fix x
68386
98cf1c823c48 Keep filter input syntax
nipkow
parents: 68249
diff changeset
    76
  show "map_filter P (map_of m) x = map_of [(k, _) \<leftarrow> m. P k] x"
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    77
    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
    78
qed
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    79
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    80
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
    81
  assumes "finite (dom m)"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    82
  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
    83
proof -
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    84
  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
    85
    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
    86
    by auto
64180
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
    87
  then show ?thesis
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    88
    using assms
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    89
    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
    90
qed
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    91
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    92
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
    93
"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
    94
68462
8d1bf38c6fe6 simplify parametricity proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 68386
diff changeset
    95
parametric_constant map_drop_transfer[transfer_rule]: map_drop_def
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    96
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    97
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
    98
"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
    99
68462
8d1bf38c6fe6 simplify parametricity proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 68386
diff changeset
   100
parametric_constant map_drop_set_transfer[transfer_rule]: map_drop_set_def
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   101
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   102
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
   103
"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
   104
68462
8d1bf38c6fe6 simplify parametricity proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 68386
diff changeset
   105
parametric_constant map_restrict_set_transfer[transfer_rule]: map_restrict_set_def
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   106
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   107
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
   108
"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
   109
68462
8d1bf38c6fe6 simplify parametricity proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 68386
diff changeset
   110
parametric_constant map_pred_transfer[transfer_rule]: map_pred_def
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   111
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   112
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
   113
"rel_map_on_set S P = eq_onp (\<lambda>x. x \<in> S) ===> rel_option P"
66267
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
   114
66282
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
   115
definition set_of_map :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<times> 'b) set" where
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
   116
"set_of_map m = {(k, v)|k v. m k = Some v}"
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
   117
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
   118
lemma set_of_map_alt_def: "set_of_map m = (\<lambda>k. (k, the (m k))) ` dom m"
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
   119
unfolding set_of_map_def dom_def
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
   120
by auto
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
   121
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
   122
lemma set_of_map_finite: "finite (dom m) \<Longrightarrow> finite (set_of_map m)"
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
   123
unfolding set_of_map_alt_def
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
   124
by auto
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
   125
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
   126
lemma set_of_map_inj: "inj set_of_map"
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
   127
proof
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
   128
  fix x y
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
   129
  assume "set_of_map x = set_of_map y"
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
   130
  hence "(x a = Some b) = (y a = Some b)" for a b
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
   131
    unfolding set_of_map_def by auto
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
   132
  hence "x k = y k" for k
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
   133
    by (metis not_None_eq)
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
   134
  thus "x = y" ..
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
   135
qed
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
   136
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   137
lemma dom_comp: "dom (m \<circ>\<^sub>m n) \<subseteq> dom n"
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   138
unfolding map_comp_def dom_def
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   139
by (auto split: option.splits)
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   140
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   141
lemma dom_comp_finite: "finite (dom n) \<Longrightarrow> finite (dom (map_comp m n))"
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   142
by (metis finite_subset dom_comp)
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   143
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   144
parametric_constant map_comp_transfer[transfer_rule]: map_comp_def
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   145
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   146
end
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   147
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   148
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   149
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
   150
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   151
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
   152
  morphisms fmlookup Abs_fmap
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   153
proof
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   154
  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
   155
    by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   156
qed
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
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
   159
69142
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   160
lemma dom_fmlookup_finite[intro, simp]: "finite (dom (fmlookup m))"
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   161
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
   162
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   163
lemma fmap_ext:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   164
  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
   165
  shows "m = n"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   166
using assms
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   167
by transfer' auto
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
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   170
subsection \<open>Operations\<close>
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
context
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   173
  includes fset.lifting
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   174
begin
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   175
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   176
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
   177
  is ran
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   178
  parametric ran_transfer
68462
8d1bf38c6fe6 simplify parametricity proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 68386
diff changeset
   179
by (rule finite_ran)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   180
66268
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   181
lemma fmlookup_ran_iff: "y |\<in>| fmran m \<longleftrightarrow> (\<exists>x. fmlookup m x = Some y)"
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   182
by transfer' (auto simp: ran_def)
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   183
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   184
lemma fmranI: "fmlookup m x = Some y \<Longrightarrow> y |\<in>| fmran m" by (auto simp: fmlookup_ran_iff)
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   185
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   186
lemma fmranE[elim]:
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   187
  assumes "y |\<in>| fmran m"
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   188
  obtains x where "fmlookup m x = Some y"
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   189
using assms by (auto simp: fmlookup_ran_iff)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   190
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   191
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
   192
  is dom
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   193
  parametric dom_transfer
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   194
.
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   195
66268
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   196
lemma fmlookup_dom_iff: "x |\<in>| fmdom m \<longleftrightarrow> (\<exists>a. fmlookup m x = Some a)"
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   197
by transfer' auto
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   198
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   199
lemma fmdom_notI: "fmlookup m x = None \<Longrightarrow> x |\<notin>| fmdom m" by (simp add: fmlookup_dom_iff)
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   200
lemma fmdomI: "fmlookup m x = Some y \<Longrightarrow> x |\<in>| fmdom m" by (simp add: fmlookup_dom_iff)
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   201
lemma fmdom_notD[dest]: "x |\<notin>| fmdom m \<Longrightarrow> fmlookup m x = None" by (simp add: fmlookup_dom_iff)
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   202
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   203
lemma fmdomE[elim]:
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   204
  assumes "x |\<in>| fmdom m"
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   205
  obtains y where "fmlookup m x = Some y"
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   206
using assms by (auto simp: fmlookup_dom_iff)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   207
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   208
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
   209
  is dom
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   210
  parametric dom_transfer
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   211
.
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   212
66268
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   213
lemma fmlookup_dom'_iff: "x \<in> fmdom' m \<longleftrightarrow> (\<exists>a. fmlookup m x = Some a)"
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   214
by transfer' auto
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   215
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   216
lemma fmdom'_notI: "fmlookup m x = None \<Longrightarrow> x \<notin> fmdom' m" by (simp add: fmlookup_dom'_iff)
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   217
lemma fmdom'I: "fmlookup m x = Some y \<Longrightarrow> x \<in> fmdom' m" by (simp add: fmlookup_dom'_iff)
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   218
lemma fmdom'_notD[dest]: "x \<notin> fmdom' m \<Longrightarrow> fmlookup m x = None" by (simp add: fmlookup_dom'_iff)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   219
66268
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   220
lemma fmdom'E[elim]:
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   221
  assumes "x \<in> fmdom' m"
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   222
  obtains x y where "fmlookup m x = Some y"
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   223
using assms by (auto simp: fmlookup_dom'_iff)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   224
66268
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   225
lemma fmdom'_alt_def: "fmdom' m = fset (fmdom m)"
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   226
by transfer' force
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   227
69142
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   228
lemma finite_fmdom'[simp]: "finite (fmdom' m)"
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   229
unfolding fmdom'_alt_def by simp
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   230
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   231
lemma dom_fmlookup[simp]: "dom (fmlookup m) = fmdom' m"
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   232
by transfer' simp
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   233
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   234
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
   235
  is Map.empty
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   236
by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   237
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   238
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
   239
by transfer' simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   240
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   241
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
   242
lemma fmdom'_empty[simp]: "fmdom' fmempty = {}" by transfer' simp
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
   243
lemma fmran_empty[simp]: "fmran fmempty = fempty" by transfer' (auto simp: ran_def map_filter_def)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   244
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   245
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
   246
  is map_upd
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   247
  parametric map_upd_transfer
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   248
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
   249
by simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   250
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   251
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
   252
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
   253
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   254
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
   255
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
   256
70277
ac24aaf84a36 Finite_Map: move lemmas from LambdaAuth AFP entry
Lars Hupel <lars.hupel@mytum.de>
parents: 69700
diff changeset
   257
lemma fmupd_reorder_neq:
ac24aaf84a36 Finite_Map: move lemmas from LambdaAuth AFP entry
Lars Hupel <lars.hupel@mytum.de>
parents: 69700
diff changeset
   258
  assumes "a \<noteq> b"
ac24aaf84a36 Finite_Map: move lemmas from LambdaAuth AFP entry
Lars Hupel <lars.hupel@mytum.de>
parents: 69700
diff changeset
   259
  shows "fmupd a x (fmupd b y m) = fmupd b y (fmupd a x m)"
ac24aaf84a36 Finite_Map: move lemmas from LambdaAuth AFP entry
Lars Hupel <lars.hupel@mytum.de>
parents: 69700
diff changeset
   260
using assms
ac24aaf84a36 Finite_Map: move lemmas from LambdaAuth AFP entry
Lars Hupel <lars.hupel@mytum.de>
parents: 69700
diff changeset
   261
by transfer' (auto simp: map_upd_def)
ac24aaf84a36 Finite_Map: move lemmas from LambdaAuth AFP entry
Lars Hupel <lars.hupel@mytum.de>
parents: 69700
diff changeset
   262
ac24aaf84a36 Finite_Map: move lemmas from LambdaAuth AFP entry
Lars Hupel <lars.hupel@mytum.de>
parents: 69700
diff changeset
   263
lemma fmupd_idem[simp]: "fmupd a x (fmupd a y m) = fmupd a x m"
ac24aaf84a36 Finite_Map: move lemmas from LambdaAuth AFP entry
Lars Hupel <lars.hupel@mytum.de>
parents: 69700
diff changeset
   264
by transfer' (auto simp: map_upd_def)
ac24aaf84a36 Finite_Map: move lemmas from LambdaAuth AFP entry
Lars Hupel <lars.hupel@mytum.de>
parents: 69700
diff changeset
   265
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   266
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
   267
  is map_filter
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   268
  parametric map_filter_transfer
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   269
by auto
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 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
   272
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
   273
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   274
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
   275
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
   276
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   277
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
   278
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
   279
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   280
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
   281
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
   282
63900
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   283
lemma fmfilter_true[simp]:
66268
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   284
  assumes "\<And>x y. fmlookup m x = Some y \<Longrightarrow> P x"
63900
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   285
  shows "fmfilter P m = m"
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   286
proof (rule fmap_ext)
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   287
  fix x
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   288
  have "fmlookup m x = None" if "\<not> P x"
66268
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   289
    using that assms by fastforce
64180
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   290
  then show "fmlookup (fmfilter P m) x = fmlookup m x"
63900
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   291
    by simp
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   292
qed
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   293
66268
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   294
lemma fmfilter_false[simp]:
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   295
  assumes "\<And>x y. fmlookup m x = Some y \<Longrightarrow> \<not> P x"
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   296
  shows "fmfilter P m = fmempty"
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   297
using assms by transfer' (fastforce simp: map_filter_def)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   298
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   299
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
   300
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
   301
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   302
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
   303
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
   304
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   305
lemma fmfilter_cong[cong]:
66268
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   306
  assumes "\<And>x y. fmlookup m x = Some y \<Longrightarrow> P x = Q x"
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   307
  shows "fmfilter P m = fmfilter Q m"
63900
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   308
proof (rule fmap_ext)
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   309
  fix x
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   310
  have "fmlookup m x = None" if "P x \<noteq> Q x"
66268
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   311
    using that assms by fastforce
64180
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   312
  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
   313
    by auto
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   314
qed
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   315
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   316
lemma fmfilter_cong'[fundef_cong]:
67485
89f5d876a656 repair malformed fundef_cong rule
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   317
  assumes "m = n" "\<And>x. x \<in> fmdom' m \<Longrightarrow> P x = Q x"
89f5d876a656 repair malformed fundef_cong rule
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   318
  shows "fmfilter P m = fmfilter Q n"
89f5d876a656 repair malformed fundef_cong rule
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   319
using assms(2) unfolding assms(1)
66268
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   320
by (rule fmfilter_cong) (metis fmdom'I)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   321
63900
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   322
lemma fmfilter_upd[simp]:
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   323
  "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
   324
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
   325
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   326
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
   327
  is map_drop
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   328
  parametric map_drop_transfer
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   329
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
   330
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   331
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
   332
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
   333
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   334
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
   335
  is map_drop_set
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   336
  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
   337
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
   338
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   339
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
   340
  is map_drop_set
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   341
  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
   342
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
   343
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   344
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
   345
  is map_restrict_set
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   346
  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
   347
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
   348
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   349
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
   350
  is map_restrict_set
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   351
  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
   352
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
   353
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   354
lemma fmfilter_alt_defs:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   355
  "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
   356
  "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
   357
  "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
   358
  "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
   359
  "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
   360
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
   361
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   362
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
   363
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
   364
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
   365
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
   366
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
   367
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
   368
70277
ac24aaf84a36 Finite_Map: move lemmas from LambdaAuth AFP entry
Lars Hupel <lars.hupel@mytum.de>
parents: 69700
diff changeset
   369
lemma fmdrop_fmupd: "fmdrop x (fmupd y z m) = (if x = y then fmdrop x m else fmupd y z (fmdrop x m))"
ac24aaf84a36 Finite_Map: move lemmas from LambdaAuth AFP entry
Lars Hupel <lars.hupel@mytum.de>
parents: 69700
diff changeset
   370
by transfer' (auto simp: map_drop_def map_filter_def map_upd_def)
ac24aaf84a36 Finite_Map: move lemmas from LambdaAuth AFP entry
Lars Hupel <lars.hupel@mytum.de>
parents: 69700
diff changeset
   371
ac24aaf84a36 Finite_Map: move lemmas from LambdaAuth AFP entry
Lars Hupel <lars.hupel@mytum.de>
parents: 69700
diff changeset
   372
lemma fmdrop_idle: "x |\<notin>| fmdom B \<Longrightarrow> fmdrop x B = B"
ac24aaf84a36 Finite_Map: move lemmas from LambdaAuth AFP entry
Lars Hupel <lars.hupel@mytum.de>
parents: 69700
diff changeset
   373
by transfer' (auto simp: map_drop_def map_filter_def)
ac24aaf84a36 Finite_Map: move lemmas from LambdaAuth AFP entry
Lars Hupel <lars.hupel@mytum.de>
parents: 69700
diff changeset
   374
ac24aaf84a36 Finite_Map: move lemmas from LambdaAuth AFP entry
Lars Hupel <lars.hupel@mytum.de>
parents: 69700
diff changeset
   375
lemma fmdrop_idle': "x \<notin> fmdom' B \<Longrightarrow> fmdrop x B = B"
ac24aaf84a36 Finite_Map: move lemmas from LambdaAuth AFP entry
Lars Hupel <lars.hupel@mytum.de>
parents: 69700
diff changeset
   376
by transfer' (auto simp: map_drop_def map_filter_def)
ac24aaf84a36 Finite_Map: move lemmas from LambdaAuth AFP entry
Lars Hupel <lars.hupel@mytum.de>
parents: 69700
diff changeset
   377
ac24aaf84a36 Finite_Map: move lemmas from LambdaAuth AFP entry
Lars Hupel <lars.hupel@mytum.de>
parents: 69700
diff changeset
   378
lemma fmdrop_fmupd_same: "fmdrop x (fmupd x y m) = fmdrop x m"
ac24aaf84a36 Finite_Map: move lemmas from LambdaAuth AFP entry
Lars Hupel <lars.hupel@mytum.de>
parents: 69700
diff changeset
   379
by transfer' (auto simp: map_drop_def map_filter_def map_upd_def)
ac24aaf84a36 Finite_Map: move lemmas from LambdaAuth AFP entry
Lars Hupel <lars.hupel@mytum.de>
parents: 69700
diff changeset
   380
69142
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   381
lemma fmdom'_restrict_set_precise: "fmdom' (fmrestrict_set A m) = fmdom' m \<inter> A"
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   382
unfolding fmfilter_alt_defs by auto
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   383
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   384
lemma fmdom'_restrict_fset_precise: "fmdom (fmrestrict_fset A m) = fmdom m |\<inter>| A"
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   385
unfolding fmfilter_alt_defs by auto
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   386
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   387
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
   388
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
   389
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   390
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
   391
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
   392
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   393
lemma fmlookup_drop[simp]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   394
  "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
   395
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
   396
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   397
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
   398
  "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
   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 fmlookup_drop_fset[simp]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   402
  "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
   403
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
   404
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   405
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
   406
  "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
   407
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
   408
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   409
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
   410
  "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
   411
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
   412
63900
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   413
lemma fmrestrict_set_dom[simp]: "fmrestrict_set (fmdom' m) m = m"
68909
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
   414
by (rule fmap_ext) auto
63900
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   415
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   416
lemma fmrestrict_fset_dom[simp]: "fmrestrict_fset (fmdom m) m = m"
68909
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
   417
by (rule fmap_ext) auto
63900
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 fmdrop_empty[simp]: "fmdrop a fmempty = fmempty"
68909
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
   420
unfolding fmfilter_alt_defs by simp
63885
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 fmdrop_set_empty[simp]: "fmdrop_set A fmempty = fmempty"
68909
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
   423
unfolding fmfilter_alt_defs by simp
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 fmdrop_fset_empty[simp]: "fmdrop_fset A fmempty = fmempty"
68909
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
   426
unfolding fmfilter_alt_defs by simp
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   427
70277
ac24aaf84a36 Finite_Map: move lemmas from LambdaAuth AFP entry
Lars Hupel <lars.hupel@mytum.de>
parents: 69700
diff changeset
   428
lemma fmdrop_fset_fmdom[simp]: "fmdrop_fset (fmdom A) A = fmempty"
ac24aaf84a36 Finite_Map: move lemmas from LambdaAuth AFP entry
Lars Hupel <lars.hupel@mytum.de>
parents: 69700
diff changeset
   429
by transfer' (auto simp: map_drop_set_def map_filter_def)
ac24aaf84a36 Finite_Map: move lemmas from LambdaAuth AFP entry
Lars Hupel <lars.hupel@mytum.de>
parents: 69700
diff changeset
   430
ac24aaf84a36 Finite_Map: move lemmas from LambdaAuth AFP entry
Lars Hupel <lars.hupel@mytum.de>
parents: 69700
diff changeset
   431
lemma fmdrop_set_fmdom[simp]: "fmdrop_set (fmdom' A) A = fmempty"
ac24aaf84a36 Finite_Map: move lemmas from LambdaAuth AFP entry
Lars Hupel <lars.hupel@mytum.de>
parents: 69700
diff changeset
   432
by transfer' (auto simp: map_drop_set_def map_filter_def)
ac24aaf84a36 Finite_Map: move lemmas from LambdaAuth AFP entry
Lars Hupel <lars.hupel@mytum.de>
parents: 69700
diff changeset
   433
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   434
lemma fmrestrict_set_empty[simp]: "fmrestrict_set A fmempty = fmempty"
68909
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
   435
unfolding fmfilter_alt_defs by simp
63885
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 fmrestrict_fset_empty[simp]: "fmrestrict_fset A fmempty = fmempty"
68909
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
   438
unfolding fmfilter_alt_defs by simp
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   439
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
   440
lemma fmdrop_set_null[simp]: "fmdrop_set {} m = m"
68909
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
   441
by (rule fmap_ext) auto
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
   442
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
   443
lemma fmdrop_fset_null[simp]: "fmdrop_fset {||} m = m"
68909
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
   444
by (rule fmap_ext) auto
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
   445
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   446
lemma fmdrop_set_single[simp]: "fmdrop_set {a} m = fmdrop a m"
68909
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
   447
unfolding fmfilter_alt_defs by simp
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   448
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   449
lemma fmdrop_fset_single[simp]: "fmdrop_fset {|a|} m = fmdrop a m"
68909
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
   450
unfolding fmfilter_alt_defs by simp
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   451
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   452
lemma fmrestrict_set_null[simp]: "fmrestrict_set {} m = fmempty"
68909
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
   453
unfolding fmfilter_alt_defs by simp
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   454
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   455
lemma fmrestrict_fset_null[simp]: "fmrestrict_fset {||} m = fmempty"
68909
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
   456
unfolding fmfilter_alt_defs by simp
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   457
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   458
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
   459
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
   460
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
   461
lemma fmdrop_set_insert[simp]: "fmdrop_set (insert x S) m = fmdrop x (fmdrop_set S m)"
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
   462
by (rule fmap_ext) auto
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
   463
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
   464
lemma fmdrop_fset_insert[simp]: "fmdrop_fset (finsert x S) m = fmdrop x (fmdrop_fset S m)"
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
   465
by (rule fmap_ext) auto
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
   466
69142
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   467
lemma fmrestrict_set_twice[simp]: "fmrestrict_set S (fmrestrict_set T m) = fmrestrict_set (S \<inter> T) m"
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   468
unfolding fmfilter_alt_defs by auto
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   469
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   470
lemma fmrestrict_fset_twice[simp]: "fmrestrict_fset S (fmrestrict_fset T m) = fmrestrict_fset (S |\<inter>| T) m"
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   471
unfolding fmfilter_alt_defs by auto
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   472
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   473
lemma fmrestrict_set_drop[simp]: "fmrestrict_set S (fmdrop b m) = fmrestrict_set (S - {b}) m"
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   474
unfolding fmfilter_alt_defs by auto
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   475
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   476
lemma fmrestrict_fset_drop[simp]: "fmrestrict_fset S (fmdrop b m) = fmrestrict_fset (S - {| b |}) m"
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   477
unfolding fmfilter_alt_defs by auto
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   478
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   479
lemma fmdrop_fmrestrict_set[simp]: "fmdrop b (fmrestrict_set S m) = fmrestrict_set (S - {b}) m"
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   480
by (rule fmap_ext) auto
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   481
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   482
lemma fmdrop_fmrestrict_fset[simp]: "fmdrop b (fmrestrict_fset S m) = fmrestrict_fset (S - {| b |}) m"
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   483
by (rule fmap_ext) auto
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   484
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   485
lemma fmdrop_idem[simp]: "fmdrop a (fmdrop a m) = fmdrop a m"
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   486
unfolding fmfilter_alt_defs by auto
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   487
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   488
lemma fmdrop_set_twice[simp]: "fmdrop_set S (fmdrop_set T m) = fmdrop_set (S \<union> T) m"
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   489
unfolding fmfilter_alt_defs by auto
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   490
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   491
lemma fmdrop_fset_twice[simp]: "fmdrop_fset S (fmdrop_fset T m) = fmdrop_fset (S |\<union>| T) m"
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   492
unfolding fmfilter_alt_defs by auto
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   493
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   494
lemma fmdrop_set_fmdrop[simp]: "fmdrop_set S (fmdrop b m) = fmdrop_set (insert b S) m"
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   495
by (rule fmap_ext) auto
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   496
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   497
lemma fmdrop_fset_fmdrop[simp]: "fmdrop_fset S (fmdrop b m) = fmdrop_fset (finsert b S) m"
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   498
by (rule fmap_ext) auto
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   499
80914
d97fdabd9e2b standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing;
wenzelm
parents: 80777
diff changeset
   500
lift_definition fmadd :: "('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap" (infixl \<open>++\<^sub>f\<close> 100)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   501
  is map_add
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   502
  parametric map_add_transfer
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   503
  by simp
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   504
63900
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   505
lemma fmlookup_add[simp]:
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   506
  "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
   507
  by transfer' (auto simp: map_add_def split: option.splits)
2359e9952641 tuned proofs
Lars Hupel <lars.hupel@mytum.de>
parents: 63885
diff changeset
   508
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   509
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
   510
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
   511
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   512
lemma fmadd_drop_left_dom: "fmdrop_fset (fmdom n) m ++\<^sub>f n = m ++\<^sub>f n"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   513
  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
   514
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   515
lemma fmadd_restrict_right_dom: "fmrestrict_fset (fmdom n) (m ++\<^sub>f n) = n"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   516
  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
   517
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   518
lemma fmfilter_add_distrib[simp]: "fmfilter P (m ++\<^sub>f n) = fmfilter P m ++\<^sub>f fmfilter P n"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   519
  by transfer' (auto simp: map_filter_def map_add_def)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   520
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   521
lemma fmdrop_add_distrib[simp]: "fmdrop a (m ++\<^sub>f n) = fmdrop a m ++\<^sub>f fmdrop a n"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   522
  unfolding fmfilter_alt_defs by simp
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   523
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   524
lemma fmdrop_set_add_distrib[simp]: "fmdrop_set A (m ++\<^sub>f n) = fmdrop_set A m ++\<^sub>f fmdrop_set A n"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   525
  unfolding fmfilter_alt_defs by simp
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   526
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   527
lemma fmdrop_fset_add_distrib[simp]: "fmdrop_fset A (m ++\<^sub>f n) = fmdrop_fset A m ++\<^sub>f fmdrop_fset A n"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   528
  unfolding fmfilter_alt_defs by simp
63885
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 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
   531
  "fmrestrict_set A (m ++\<^sub>f n) = fmrestrict_set A m ++\<^sub>f fmrestrict_set A n"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   532
  unfolding fmfilter_alt_defs by simp
63885
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 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
   535
  "fmrestrict_fset A (m ++\<^sub>f n) = fmrestrict_fset A m ++\<^sub>f fmrestrict_fset A n"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   536
  unfolding fmfilter_alt_defs by simp
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   537
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   538
lemma fmadd_empty[simp]: "fmempty ++\<^sub>f m = m" "m ++\<^sub>f fmempty = m"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   539
  by (transfer'; auto)+
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   540
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   541
lemma fmadd_idempotent[simp]: "m ++\<^sub>f m = m"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   542
  by transfer' (auto simp: map_add_def split: option.splits)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   543
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   544
lemma fmadd_assoc[simp]: "m ++\<^sub>f (n ++\<^sub>f p) = m ++\<^sub>f n ++\<^sub>f p"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   545
  by transfer' simp
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   546
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
   547
lemma fmadd_fmupd[simp]: "m ++\<^sub>f fmupd a b n = fmupd a b (m ++\<^sub>f n)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   548
  by (rule fmap_ext) simp
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
   549
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   550
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
   551
  is map_pred
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   552
  parametric map_pred_transfer
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   553
  .
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   554
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   555
lemma fmpredI[intro]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   556
  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
   557
  shows "fmpred P m"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   558
  using assms
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   559
  by transfer' (auto simp: map_pred_def split: option.splits)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   560
66267
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
   561
lemma fmpredD[dest]: "fmpred P m \<Longrightarrow> fmlookup m x = Some y \<Longrightarrow> P x y"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   562
  by transfer' (auto simp: map_pred_def split: option.split_asm)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   563
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   564
lemma fmpred_iff: "fmpred P m \<longleftrightarrow> (\<forall>x y. fmlookup m x = Some y \<longrightarrow> P x y)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   565
  by auto
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   566
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   567
lemma fmpred_alt_def: "fmpred P m \<longleftrightarrow> fBall (fmdom m) (\<lambda>x. P x (the (fmlookup m x)))"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   568
  unfolding fmpred_iff
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   569
  using fmdomI by fastforce
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   570
68757
e7e3776385ba Finite_Map: monotonicity
Lars Hupel <lars.hupel@mytum.de>
parents: 68463
diff changeset
   571
lemma fmpred_mono_strong:
e7e3776385ba Finite_Map: monotonicity
Lars Hupel <lars.hupel@mytum.de>
parents: 68463
diff changeset
   572
  assumes "\<And>x y. fmlookup m x = Some y \<Longrightarrow> P x y \<Longrightarrow> Q x y"
e7e3776385ba Finite_Map: monotonicity
Lars Hupel <lars.hupel@mytum.de>
parents: 68463
diff changeset
   573
  shows "fmpred P m \<Longrightarrow> fmpred Q m"
e7e3776385ba Finite_Map: monotonicity
Lars Hupel <lars.hupel@mytum.de>
parents: 68463
diff changeset
   574
using assms unfolding fmpred_iff by auto
e7e3776385ba Finite_Map: monotonicity
Lars Hupel <lars.hupel@mytum.de>
parents: 68463
diff changeset
   575
e7e3776385ba Finite_Map: monotonicity
Lars Hupel <lars.hupel@mytum.de>
parents: 68463
diff changeset
   576
lemma fmpred_mono[mono]: "P \<le> Q \<Longrightarrow> fmpred P \<le> fmpred Q"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   577
  by auto
68757
e7e3776385ba Finite_Map: monotonicity
Lars Hupel <lars.hupel@mytum.de>
parents: 68463
diff changeset
   578
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   579
lemma fmpred_empty[intro!, simp]: "fmpred P fmempty"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   580
  by auto
63885
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 fmpred_upd[intro]: "fmpred P m \<Longrightarrow> P x y \<Longrightarrow> fmpred P (fmupd x y m)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   583
  by transfer' (auto simp: map_pred_def map_upd_def)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   584
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   585
lemma fmpred_updD[dest]: "fmpred P (fmupd x y m) \<Longrightarrow> P x y"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   586
  by auto
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   587
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   588
lemma fmpred_add[intro]: "fmpred P m \<Longrightarrow> fmpred P n \<Longrightarrow> fmpred P (m ++\<^sub>f n)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   589
  by transfer' (auto simp: map_pred_def map_add_def split: option.splits)
63885
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 fmpred_filter[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmfilter Q m)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   592
  by transfer' (auto simp: map_pred_def map_filter_def)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   593
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   594
lemma fmpred_drop[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop a m)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   595
  by (auto simp: fmfilter_alt_defs)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   596
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   597
lemma fmpred_drop_set[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop_set A m)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   598
  by (auto simp: fmfilter_alt_defs)
63885
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 fmpred_drop_fset[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop_fset A m)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   601
  by (auto simp: fmfilter_alt_defs)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   602
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   603
lemma fmpred_restrict_set[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmrestrict_set A m)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   604
  by (auto simp: fmfilter_alt_defs)
63885
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
lemma fmpred_restrict_fset[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmrestrict_fset A m)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   607
  by (auto simp: fmfilter_alt_defs)
63885
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
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
   610
  assumes "fmpred P m"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   611
  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
   612
using assms by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   613
80914
d97fdabd9e2b standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing;
wenzelm
parents: 80777
diff changeset
   614
lift_definition fmsubset :: "('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap \<Rightarrow> bool" (infix \<open>\<subseteq>\<^sub>f\<close> 50)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   615
  is map_le
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   616
.
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   617
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   618
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
   619
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
   620
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   621
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
   622
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
   623
by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   624
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   625
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
   626
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
   627
by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   628
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   629
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
   630
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
   631
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   632
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
   633
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
   634
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   635
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
   636
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
   637
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   638
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
   639
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
   640
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   641
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
   642
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
   643
69142
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   644
lemma fmfilter_subset[simp]: "fmfilter P m \<subseteq>\<^sub>f m"
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   645
unfolding fmsubset_alt_def fmpred_iff by auto
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   646
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   647
lemma fmsubset_drop[simp]: "fmdrop a m \<subseteq>\<^sub>f m"
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   648
unfolding fmfilter_alt_defs by (rule fmfilter_subset)
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   649
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   650
lemma fmsubset_drop_set[simp]: "fmdrop_set S m \<subseteq>\<^sub>f m"
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   651
unfolding fmfilter_alt_defs by (rule fmfilter_subset)
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   652
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   653
lemma fmsubset_drop_fset[simp]: "fmdrop_fset S m \<subseteq>\<^sub>f m"
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   654
unfolding fmfilter_alt_defs by (rule fmfilter_subset)
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   655
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   656
lemma fmsubset_restrict_set[simp]: "fmrestrict_set S m \<subseteq>\<^sub>f m"
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   657
unfolding fmfilter_alt_defs by (rule fmfilter_subset)
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   658
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   659
lemma fmsubset_restrict_fset[simp]: "fmrestrict_fset S m \<subseteq>\<^sub>f m"
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   660
unfolding fmfilter_alt_defs by (rule fmfilter_subset)
c5e3212455ed more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68909
diff changeset
   661
66282
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
   662
lift_definition fset_of_fmap :: "('a, 'b) fmap \<Rightarrow> ('a \<times> 'b) fset" is set_of_map
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   663
  by (rule set_of_map_finite)
66282
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
   664
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
   665
lemma fset_of_fmap_inj[intro, simp]: "inj fset_of_fmap"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   666
  apply rule
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   667
  apply transfer'
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   668
  using set_of_map_inj unfolding inj_def by auto
66282
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
   669
66398
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
   670
lemma fset_of_fmap_iff[simp]: "(a, b) |\<in>| fset_of_fmap m \<longleftrightarrow> fmlookup m a = Some b"
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
   671
by transfer' (auto simp: set_of_map_def)
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
   672
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   673
lemma fset_of_fmap_iff': "(a, b) \<in> fset (fset_of_fmap m) \<longleftrightarrow> fmlookup m a = Some b"
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   674
  by simp
66398
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
   675
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   676
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
   677
  is map_of
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   678
  parametric map_of_transfer
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   679
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
   680
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   681
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
   682
  "fmap_of_list [] = fmempty"
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   683
  "fmap_of_list ((k, v) # kvs) = fmupd k v (fmap_of_list kvs)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   684
  by (transfer, simp add: map_upd_def)+
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   685
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   686
lemma fmap_of_list_app[simp]: "fmap_of_list (xs @ ys) = fmap_of_list ys ++\<^sub>f fmap_of_list xs"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   687
  by transfer' simp
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   688
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   689
lemma fmupd_alt_def: "fmupd k v m = m ++\<^sub>f fmap_of_list [(k, v)]"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   690
  by simp
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   691
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   692
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
   693
  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
   694
  shows "fmpred P (fmap_of_list xs)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   695
  using assms
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   696
  by (induction xs) (transfer'; auto simp: map_pred_def)+
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   697
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   698
lemma fmap_of_list_SomeD: "fmlookup (fmap_of_list xs) k = Some v \<Longrightarrow> (k, v) \<in> set xs"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   699
  by transfer' (auto dest: map_of_SomeD)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   700
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
   701
lemma fmdom_fmap_of_list[simp]: "fmdom (fmap_of_list xs) = fset_of_list (map fst xs)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   702
  by transfer' (simp add: dom_map_of_conv_image_fst)
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
   703
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   704
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
   705
  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
   706
.
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_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
   709
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
   710
64181
4d1d2de432fa renamed lemma to a more consistent name
Lars Hupel <lars.hupel@mytum.de>
parents: 64180
diff changeset
   711
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
   712
  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
   713
  shows "fmrel_on_fset S P m n"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   714
  by (simp add: assms fmrel_on_fset_alt_def)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   715
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   716
lemma fmrel_on_fset_mono[mono]: "R \<le> Q \<Longrightarrow> fmrel_on_fset S R \<le> fmrel_on_fset S Q"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   717
  unfolding fmrel_on_fset_alt_def[abs_def]
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   718
  using option.rel_mono by blast
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   719
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   720
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)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   721
  unfolding fmrel_on_fset_alt_def
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   722
  by auto
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   723
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   724
lemma fmrel_on_fsubset: "fmrel_on_fset S R m n \<Longrightarrow> T |\<subseteq>| S \<Longrightarrow> fmrel_on_fset T R m n"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   725
  unfolding fmrel_on_fset_alt_def
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   726
  by auto
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   727
66274
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   728
lemma fmrel_on_fset_unionI:
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   729
  "fmrel_on_fset A R m n \<Longrightarrow> fmrel_on_fset B R m n \<Longrightarrow> fmrel_on_fset (A |\<union>| B) R m n"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   730
  unfolding fmrel_on_fset_alt_def
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   731
  by auto
66274
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   732
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   733
lemma fmrel_on_fset_updateI:
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   734
  assumes "fmrel_on_fset S P m n" "P v\<^sub>1 v\<^sub>2"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   735
  shows "fmrel_on_fset (finsert k S) P (fmupd k v\<^sub>1 m) (fmupd k v\<^sub>2 n)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   736
  using assms
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   737
  unfolding fmrel_on_fset_alt_def
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   738
  by auto
66274
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   739
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   740
lift_definition fmimage :: "('a, 'b) fmap \<Rightarrow> 'a fset \<Rightarrow> 'b fset" is "\<lambda>m S. {b|a b. m a = Some b \<and> a \<in> S}"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   741
  by (smt (verit, del_insts) Collect_mono_iff finite_surj ran_alt_def ran_def)
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   742
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   743
lemma fmimage_alt_def: "fmimage m S = fmran (fmrestrict_fset S m)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   744
  by transfer' (auto simp: ran_def map_restrict_set_def map_filter_def)
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   745
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   746
lemma fmimage_empty[simp]: "fmimage m fempty = fempty"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   747
  by transfer' auto
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   748
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   749
lemma fmimage_subset_ran[simp]: "fmimage m S |\<subseteq>| fmran m"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   750
  by transfer' (auto simp: ran_def)
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   751
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   752
lemma fmimage_dom[simp]: "fmimage m (fmdom m) = fmran m"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   753
  by transfer' (auto simp: ran_def)
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   754
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   755
lemma fmimage_inter: "fmimage m (A |\<inter>| B) |\<subseteq>| fmimage m A |\<inter>| fmimage m B"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   756
  by transfer' auto
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   757
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   758
lemma fimage_inter_dom[simp]:
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   759
  "fmimage m (fmdom m |\<inter>| A) = fmimage m A"
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   760
  "fmimage m (A |\<inter>| fmdom m) = fmimage m A"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   761
  by (transfer'; auto)+
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   762
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   763
lemma fmimage_union[simp]: "fmimage m (A |\<union>| B) = fmimage m A |\<union>| fmimage m B"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   764
  by transfer' auto
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   765
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   766
lemma fmimage_Union[simp]: "fmimage m (ffUnion A) = ffUnion (fmimage m |`| A)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   767
  by transfer' auto
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   768
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   769
lemma fmimage_filter[simp]: "fmimage (fmfilter P m) A = fmimage m (ffilter P A)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   770
  by transfer' (auto simp: map_filter_def)
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   771
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   772
lemma fmimage_drop[simp]: "fmimage (fmdrop a m) A = fmimage m (A - {|a|})"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   773
  by (simp add: fmimage_alt_def)
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   774
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   775
lemma fmimage_drop_fset[simp]: "fmimage (fmdrop_fset B m) A = fmimage m (A - B)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   776
  by transfer' (auto simp: map_filter_def map_drop_set_def)
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   777
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   778
lemma fmimage_restrict_fset[simp]: "fmimage (fmrestrict_fset B m) A = fmimage m (A |\<inter>| B)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   779
  by transfer' (auto simp: map_filter_def map_restrict_set_def)
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   780
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   781
lemma fmfilter_ran[simp]: "fmran (fmfilter P m) = fmimage m (ffilter P (fmdom m))"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   782
  by transfer' (auto simp: ran_def map_filter_def)
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   783
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   784
lemma fmran_drop[simp]: "fmran (fmdrop a m) = fmimage m (fmdom m - {|a|})"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   785
  by transfer' (auto simp: ran_def map_drop_def map_filter_def)
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   786
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   787
lemma fmran_drop_fset[simp]: "fmran (fmdrop_fset A m) = fmimage m (fmdom m - A)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   788
  by transfer' (auto simp: ran_def map_drop_set_def map_filter_def)
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   789
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   790
lemma fmran_restrict_fset: "fmran (fmrestrict_fset A m) = fmimage m (fmdom m |\<inter>| A)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   791
  by transfer' (auto simp: ran_def map_restrict_set_def map_filter_def)
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   792
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   793
lemma fmlookup_image_iff: "y |\<in>| fmimage m A \<longleftrightarrow> (\<exists>x. fmlookup m x = Some y \<and> x |\<in>| A)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   794
  by transfer' (auto simp: ran_def)
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   795
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   796
lemma fmimageI: "fmlookup m x = Some y \<Longrightarrow> x |\<in>| A \<Longrightarrow> y |\<in>| fmimage m A"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   797
  by (auto simp: fmlookup_image_iff)
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   798
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   799
lemma fmimageE[elim]:
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   800
  assumes "y |\<in>| fmimage m A"
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   801
  obtains x where "fmlookup m x = Some y" "x |\<in>| A"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   802
  using assms by (auto simp: fmlookup_image_iff)
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   803
80914
d97fdabd9e2b standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing;
wenzelm
parents: 80777
diff changeset
   804
lift_definition fmcomp :: "('b, 'c) fmap \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'c) fmap" (infixl \<open>\<circ>\<^sub>f\<close> 55)
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   805
  is map_comp
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   806
  parametric map_comp_transfer
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   807
  by (rule dom_comp_finite)
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   808
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   809
lemma fmlookup_comp[simp]: "fmlookup (m \<circ>\<^sub>f n) x = Option.bind (fmlookup n x) (fmlookup m)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   810
  by transfer' (auto simp: map_comp_def split: option.splits)
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
   811
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   812
end
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   813
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
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
   816
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   817
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
   818
  for map: fmmap
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   819
      rel: fmrel
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   820
  by auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   821
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
   822
declare fmap.pred_mono[mono]
66268
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   823
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   824
66268
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   825
lemma fmran'_alt_def: "fmran' m = fset (fmran m)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   826
  including fset.lifting
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   827
  by transfer' (auto simp: ran_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
   828
66268
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   829
lemma fmlookup_ran'_iff: "y \<in> fmran' m \<longleftrightarrow> (\<exists>x. fmlookup m x = Some y)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   830
  by transfer' (auto simp: ran_def)
66268
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   831
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   832
lemma fmran'I: "fmlookup m x = Some y \<Longrightarrow> y \<in> fmran' m" 
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   833
  by (auto simp: fmlookup_ran'_iff)
66268
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   834
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   835
lemma fmran'E[elim]:
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   836
  assumes "y \<in> fmran' m"
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   837
  obtains x where "fmlookup m x = Some y"
e4b98cad5ab4 canonical representation for fmaps is fmlookup
Lars Hupel <lars.hupel@mytum.de>
parents: 66267
diff changeset
   838
using assms by (auto simp: fmlookup_ran'_iff)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   839
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   840
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
   841
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
   842
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   843
lemma fmrelI[intro]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   844
  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
   845
  shows "fmrel R m n"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   846
  using assms
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   847
  by transfer' auto
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   848
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   849
lemma fmrel_upd[intro]: "fmrel P m n \<Longrightarrow> P x y \<Longrightarrow> fmrel P (fmupd k x m) (fmupd k y n)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   850
  by transfer' (auto simp: map_upd_def rel_fun_def)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   851
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   852
lemma fmrelD[dest]: "fmrel P m n \<Longrightarrow> rel_option P (fmlookup m x) (fmlookup n x)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   853
  by transfer' (auto simp: rel_fun_def)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   854
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   855
lemma fmrel_addI[intro]:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   856
  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
   857
  shows "fmrel P (m ++\<^sub>f a) (n ++\<^sub>f b)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   858
  by (smt (verit, del_insts) assms domIff fmdom.rep_eq fmlookup_add fmrel_iff option.rel_sel)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   859
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   860
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
   861
  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
   862
  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
   863
        | (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
   864
proof -
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   865
  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
   866
    by auto
64180
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
   867
  then show thesis
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   868
    using none some
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   869
    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
   870
qed
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   871
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   872
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
   873
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
   874
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   875
lemma fmrel_drop[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmdrop a m) (fmdrop a n)"
68909
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
   876
unfolding fmfilter_alt_defs by blast
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   877
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   878
lemma fmrel_drop_set[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmdrop_set A m) (fmdrop_set A n)"
68909
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
   879
unfolding fmfilter_alt_defs by blast
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   880
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   881
lemma fmrel_drop_fset[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmdrop_fset A m) (fmdrop_fset A n)"
68909
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
   882
unfolding fmfilter_alt_defs by blast
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   883
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   884
lemma fmrel_restrict_set[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmrestrict_set A m) (fmrestrict_set A n)"
68909
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
   885
unfolding fmfilter_alt_defs by blast
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   886
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   887
lemma fmrel_restrict_fset[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmrestrict_fset A m) (fmrestrict_fset A n)"
68909
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
   888
unfolding fmfilter_alt_defs by blast
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   889
66274
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   890
lemma fmrel_on_fset_fmrel_restrict:
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   891
  "fmrel_on_fset S P m n \<longleftrightarrow> fmrel P (fmrestrict_fset S m) (fmrestrict_fset S n)"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   892
unfolding fmrel_on_fset_alt_def fmrel_iff
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   893
by auto
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   894
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   895
lemma fmrel_on_fset_refl_strong:
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   896
  assumes "\<And>x y. x |\<in>| S \<Longrightarrow> fmlookup m x = Some y \<Longrightarrow> P y y"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   897
  shows "fmrel_on_fset S P m m"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   898
unfolding fmrel_on_fset_fmrel_restrict fmrel_iff
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   899
using assms
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   900
by (simp add: option.rel_sel)
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   901
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   902
lemma fmrel_on_fset_addI:
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   903
  assumes "fmrel_on_fset S P m n" "fmrel_on_fset S P a b"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   904
  shows "fmrel_on_fset S P (m ++\<^sub>f a) (n ++\<^sub>f b)"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   905
using assms
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   906
unfolding fmrel_on_fset_fmrel_restrict
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   907
by auto
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   908
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   909
lemma fmrel_fmdom_eq:
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   910
  assumes "fmrel P x y"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   911
  shows "fmdom x = fmdom y"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   912
proof -
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   913
  have "a |\<in>| fmdom x \<longleftrightarrow> a |\<in>| fmdom y" for a
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   914
    proof -
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   915
      have "rel_option P (fmlookup x a) (fmlookup y a)"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   916
        using assms by (simp add: fmrel_iff)
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   917
      thus ?thesis
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   918
        by cases (auto intro: fmdomI)
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   919
    qed
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   920
  thus ?thesis
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   921
    by auto
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   922
qed
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   923
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   924
lemma fmrel_fmdom'_eq: "fmrel P x y \<Longrightarrow> fmdom' x = fmdom' y"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   925
unfolding fmdom'_alt_def
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   926
by (metis fmrel_fmdom_eq)
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   927
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   928
lemma fmrel_rel_fmran:
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   929
  assumes "fmrel P x y"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   930
  shows "rel_fset P (fmran x) (fmran y)"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   931
proof -
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   932
  {
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   933
    fix b
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   934
    assume "b |\<in>| fmran x"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   935
    then obtain a where "fmlookup x a = Some b"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   936
      by auto
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   937
    moreover have "rel_option P (fmlookup x a) (fmlookup y a)"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   938
      using assms by auto
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   939
    ultimately have "\<exists>b'. b' |\<in>| fmran y \<and> P b b'"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   940
      by (metis option_rel_Some1 fmranI)
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   941
  }
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   942
  moreover
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   943
  {
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   944
    fix b
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   945
    assume "b |\<in>| fmran y"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   946
    then obtain a where "fmlookup y a = Some b"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   947
      by auto
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   948
    moreover have "rel_option P (fmlookup x a) (fmlookup y a)"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   949
      using assms by auto
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   950
    ultimately have "\<exists>b'. b' |\<in>| fmran x \<and> P b' b"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   951
      by (metis option_rel_Some2 fmranI)
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   952
  }
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   953
  ultimately show ?thesis
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   954
    unfolding rel_fset_alt_def
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   955
    by auto
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   956
qed
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   957
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   958
lemma fmrel_rel_fmran': "fmrel P x y \<Longrightarrow> rel_set P (fmran' x) (fmran' y)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   959
  unfolding fmran'_alt_def
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   960
  by (metis fmrel_rel_fmran rel_fset_fset)
66274
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   961
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   962
lemma pred_fmap_fmpred[simp]: "pred_fmap P = fmpred (\<lambda>_. P)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   963
  unfolding fmap.pred_set fmran'_alt_def
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   964
  using fmranI by fastforce
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   965
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   966
lemma pred_fmap_id[simp]: "pred_fmap id (fmmap f m) \<longleftrightarrow> pred_fmap f m"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   967
  unfolding fmap.pred_set fmap.set_map
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   968
  by simp
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   969
66274
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   970
lemma pred_fmapD: "pred_fmap P m \<Longrightarrow> x |\<in>| fmran m \<Longrightarrow> P x"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   971
  by auto
66274
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
   972
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   973
lemma fmlookup_map[simp]: "fmlookup (fmmap f m) x = map_option f (fmlookup m x)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   974
  by transfer' auto
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   975
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   976
lemma fmpred_map[simp]: "fmpred P (fmmap f m) \<longleftrightarrow> fmpred (\<lambda>k v. P k (f v)) m"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   977
  unfolding fmpred_iff pred_fmap_def fmap.set_map
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   978
  by auto
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   979
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   980
lemma fmpred_id[simp]: "fmpred (\<lambda>_. id) (fmmap f m) \<longleftrightarrow> fmpred (\<lambda>_. f) m"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   981
  by simp
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   982
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   983
lemma fmmap_add[simp]: "fmmap f (m ++\<^sub>f n) = fmmap f m ++\<^sub>f fmmap f n"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   984
  by transfer' (auto simp: map_add_def fun_eq_iff split: option.splits)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   985
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   986
lemma fmmap_empty[simp]: "fmmap f fmempty = fmempty"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   987
  by transfer auto
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   988
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   989
lemma fmdom_map[simp]: "fmdom (fmmap f m) = fmdom m"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   990
  including fset.lifting
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   991
  by transfer' simp
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   992
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   993
lemma fmdom'_map[simp]: "fmdom' (fmmap f m) = fmdom' m"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   994
  by transfer' simp
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   995
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
   996
lemma fmran_fmmap[simp]: "fmran (fmmap f m) = f |`| fmran m"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   997
  including fset.lifting
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
   998
  by transfer' (auto simp: ran_def)
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
   999
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1000
lemma fmran'_fmmap[simp]: "fmran' (fmmap f m) = f ` fmran' m"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1001
  by transfer' (auto simp: ran_def)
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1002
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1003
lemma fmfilter_fmmap[simp]: "fmfilter P (fmmap f m) = fmmap f (fmfilter P m)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1004
  by transfer' (auto simp: map_filter_def)
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1005
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1006
lemma fmdrop_fmmap[simp]: "fmdrop a (fmmap f m) = fmmap f (fmdrop a m)" 
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1007
  unfolding fmfilter_alt_defs by simp
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1008
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1009
lemma fmdrop_set_fmmap[simp]: "fmdrop_set A (fmmap f m) = fmmap f (fmdrop_set A m)"
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1010
  unfolding fmfilter_alt_defs by simp
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1011
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1012
lemma fmdrop_fset_fmmap[simp]: "fmdrop_fset A (fmmap f m) = fmmap f (fmdrop_fset A m)"
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1013
  unfolding fmfilter_alt_defs by simp
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1014
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1015
lemma fmrestrict_set_fmmap[simp]: "fmrestrict_set A (fmmap f m) = fmmap f (fmrestrict_set A m)"
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1016
  unfolding fmfilter_alt_defs by simp
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1017
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1018
lemma fmrestrict_fset_fmmap[simp]: "fmrestrict_fset A (fmmap f m) = fmmap f (fmrestrict_fset A m)"
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1019
  unfolding fmfilter_alt_defs by simp
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1020
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1021
lemma fmmap_subset[intro]: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmmap f m \<subseteq>\<^sub>f fmmap f n"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1022
  by transfer' (auto simp: map_le_def)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1023
66398
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
  1024
lemma fmmap_fset_of_fmap: "fset_of_fmap (fmmap f m) = (\<lambda>(k, v). (k, f v)) |`| fset_of_fmap m"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1025
  including fset.lifting
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1026
  by transfer' (auto simp: set_of_map_def)
66398
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
  1027
70277
ac24aaf84a36 Finite_Map: move lemmas from LambdaAuth AFP entry
Lars Hupel <lars.hupel@mytum.de>
parents: 69700
diff changeset
  1028
lemma fmmap_fmupd: "fmmap f (fmupd x y m) = fmupd x (f y) (fmmap f m)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1029
  by transfer' (auto simp: fun_eq_iff map_upd_def)
66398
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
  1030
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69313
diff changeset
  1031
subsection \<open>\<^const>\<open>size\<close> setup\<close>
66398
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
  1032
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
  1033
definition size_fmap :: "('a \<Rightarrow> nat) \<Rightarrow> ('b \<Rightarrow> nat) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> nat" where
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
  1034
[simp]: "size_fmap f g m = size_fset (\<lambda>(a, b). f a + g b) (fset_of_fmap m)"
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
  1035
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
  1036
instantiation fmap :: (type, type) size begin
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
  1037
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
  1038
definition size_fmap where
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
  1039
size_fmap_overloaded_def: "size_fmap = Finite_Map.size_fmap (\<lambda>_. 0) (\<lambda>_. 0)"
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
  1040
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
  1041
instance ..
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
  1042
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
  1043
end
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
  1044
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
  1045
lemma size_fmap_overloaded_simps[simp]: "size x = size (fset_of_fmap x)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1046
  unfolding size_fmap_overloaded_def
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1047
  by simp
66398
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
  1048
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1049
lemma fmap_size_o_map: "size_fmap f g \<circ> fmmap h = size_fmap f (g \<circ> h)"
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1050
proof -
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1051
  have inj: "inj_on (\<lambda>(k, v). (k, h v)) (fset (fset_of_fmap m))" for m
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1052
    using inj_on_def by force
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1053
  show ?thesis
66398
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
  1054
  unfolding size_fmap_def
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1055
  apply (clarsimp simp: fun_eq_iff fmmap_fset_of_fmap sum.reindex [OF inj])
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1056
  by (rule sum.cong) (auto split: prod.splits)
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1057
qed
66398
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
  1058
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
  1059
setup \<open>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69313
diff changeset
  1060
BNF_LFP_Size.register_size_global \<^type_name>\<open>fmap\<close> \<^const_name>\<open>size_fmap\<close>
66398
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
  1061
  @{thm size_fmap_overloaded_def} @{thms size_fmap_def size_fmap_overloaded_simps}
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
  1062
  @{thms fmap_size_o_map}
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
  1063
\<close>
4d2ce596f505 fmap :: size
Lars Hupel <lars.hupel@mytum.de>
parents: 66291
diff changeset
  1064
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1065
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1066
subsection \<open>Additional operations\<close>
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1067
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1068
lift_definition fmmap_keys :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'c) fmap" is
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1069
  "\<lambda>f m a. map_option (f a) (m a)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1070
  unfolding dom_def
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1071
  by simp
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1072
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1073
lemma fmpred_fmmap_keys[simp]: "fmpred P (fmmap_keys f m) = fmpred (\<lambda>a b. P a (f a b)) m"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1074
  by transfer' (auto simp: map_pred_def split: option.splits)
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1075
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1076
lemma fmdom_fmmap_keys[simp]: "fmdom (fmmap_keys f m) = fmdom m"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1077
  including fset.lifting
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1078
  by transfer' auto
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1079
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1080
lemma fmlookup_fmmap_keys[simp]: "fmlookup (fmmap_keys f m) x = map_option (f x) (fmlookup m x)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1081
  by transfer' simp
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1082
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1083
lemma fmfilter_fmmap_keys[simp]: "fmfilter P (fmmap_keys f m) = fmmap_keys f (fmfilter P m)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1084
  by transfer' (auto simp: map_filter_def)
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1085
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1086
lemma fmdrop_fmmap_keys[simp]: "fmdrop a (fmmap_keys f m) = fmmap_keys f (fmdrop a m)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1087
  unfolding fmfilter_alt_defs by simp
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1088
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1089
lemma fmdrop_set_fmmap_keys[simp]: "fmdrop_set A (fmmap_keys f m) = fmmap_keys f (fmdrop_set A m)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1090
  unfolding fmfilter_alt_defs by simp
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1091
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1092
lemma fmdrop_fset_fmmap_keys[simp]: "fmdrop_fset A (fmmap_keys f m) = fmmap_keys f (fmdrop_fset A m)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1093
  unfolding fmfilter_alt_defs by simp
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1094
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1095
lemma fmrestrict_set_fmmap_keys[simp]: "fmrestrict_set A (fmmap_keys f m) = fmmap_keys f (fmrestrict_set A m)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1096
  unfolding fmfilter_alt_defs by simp
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1097
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1098
lemma fmrestrict_fset_fmmap_keys[simp]: "fmrestrict_fset A (fmmap_keys f m) = fmmap_keys f (fmrestrict_fset A m)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1099
  unfolding fmfilter_alt_defs by simp
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1100
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1101
lemma fmmap_keys_subset[intro]: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmmap_keys f m \<subseteq>\<^sub>f fmmap_keys f n"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1102
  by transfer' (auto simp: map_le_def dom_def)
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1103
68463
410818a69ee3 material on finite sets and maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68462
diff changeset
  1104
definition sorted_list_of_fmap :: "('a::linorder, 'b) fmap \<Rightarrow> ('a \<times> 'b) list" where
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1105
  "sorted_list_of_fmap m = map (\<lambda>k. (k, the (fmlookup m k))) (sorted_list_of_fset (fmdom m))"
68463
410818a69ee3 material on finite sets and maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68462
diff changeset
  1106
410818a69ee3 material on finite sets and maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68462
diff changeset
  1107
lemma list_all_sorted_list[simp]: "list_all P (sorted_list_of_fmap m) = fmpred (curry P) m"
410818a69ee3 material on finite sets and maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68462
diff changeset
  1108
unfolding sorted_list_of_fmap_def curry_def list.pred_map
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1109
  by (smt (verit, best) Ball_set comp_def fmpred_alt_def sorted_list_of_fset_simps(1))
68463
410818a69ee3 material on finite sets and maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68462
diff changeset
  1110
410818a69ee3 material on finite sets and maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68462
diff changeset
  1111
lemma map_of_sorted_list[simp]: "map_of (sorted_list_of_fmap m) = fmlookup m"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1112
  unfolding sorted_list_of_fmap_def
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1113
  including fset.lifting
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1114
  by transfer (simp add: map_of_map_keys)
68463
410818a69ee3 material on finite sets and maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68462
diff changeset
  1115
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1116
68909
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1117
subsection \<open>Additional properties\<close>
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1118
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1119
lemma fmchoice':
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1120
  assumes "finite S" "\<forall>x \<in> S. \<exists>y. Q x y"
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1121
  shows "\<exists>m. fmdom' m = S \<and> fmpred Q m"
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1122
proof -
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1123
  obtain f where f: "Q x (f x)" if "x \<in> S" for x
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1124
    using assms by metis
68909
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1125
  define f' where "f' x = (if x \<in> S then Some (f x) else None)" for x
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1126
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1127
  have "eq_onp (\<lambda>m. finite (dom m)) f' f'"
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1128
    unfolding eq_onp_def f'_def dom_def using assms by auto
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1129
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1130
  show ?thesis
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1131
    apply (rule exI[where x = "Abs_fmap f'"])
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1132
    apply (subst fmpred.abs_eq, fact)
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1133
    apply (subst fmdom'.abs_eq, fact)
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1134
    unfolding f'_def dom_def map_pred_def using f
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1135
    by auto
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1136
qed
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1137
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1138
subsection \<open>Lifting/transfer setup\<close>
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1139
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1140
context includes lifting_syntax begin
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1141
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1142
lemma fmempty_transfer[simp, intro, transfer_rule]: "fmrel P fmempty fmempty"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1143
  by transfer auto
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1144
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1145
lemma fmadd_transfer[transfer_rule]:
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1146
  "(fmrel P ===> fmrel P ===> fmrel P) fmadd fmadd"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1147
  by (intro fmrel_addI rel_funI)
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1148
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1149
lemma fmupd_transfer[transfer_rule]:
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 66398
diff changeset
  1150
  "((=) ===> P ===> fmrel P ===> fmrel P) fmupd fmupd"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1151
  by auto
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1152
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1153
end
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1154
68909
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1155
lemma Quotient_fmap_bnf[quot_map]:
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1156
  assumes "Quotient R Abs Rep T"
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1157
  shows "Quotient (fmrel R) (fmmap Abs) (fmmap Rep) (fmrel T)"
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1158
unfolding Quotient_alt_def4 proof safe
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1159
  fix m n
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1160
  assume "fmrel T m n"
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1161
  then have "fmlookup (fmmap Abs m) x = fmlookup n x" for x
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1162
    using assms unfolding Quotient_alt_def 
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1163
      by (cases rule: fmrel_cases[where x = x]) auto
68909
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1164
  then show "fmmap Abs m = n"
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1165
    by (rule fmap_ext)
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1166
next
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1167
  fix m
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1168
  show "fmrel T (fmmap Rep m) m"
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1169
    unfolding fmap.rel_map
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1170
    by (metis (mono_tags) Quotient_alt_def assms fmap.rel_refl)
68909
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1171
next
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1172
  from assms have "R = T OO T\<inverse>\<inverse>"
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1173
    unfolding Quotient_alt_def4 by simp
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1174
  then show "fmrel R = fmrel T OO (fmrel T)\<inverse>\<inverse>"
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1175
    by (simp add: fmap.rel_compp fmap.rel_conversep)
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1176
qed
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1177
66274
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1178
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1179
subsection \<open>View as datatype\<close>
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1180
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1181
lemma fmap_distinct[simp]:
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1182
  "fmempty \<noteq> fmupd k v m"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1183
  "fmupd k v m \<noteq> fmempty"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1184
  by (transfer'; auto simp: map_upd_def fun_eq_iff)+
66274
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1185
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1186
lifting_update fmap.lifting
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1187
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
  1188
lemma fmap_exhaust[cases type: fmap]:
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
  1189
  obtains (fmempty) "m = fmempty"
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
  1190
        | (fmupd) x y m' where "m = fmupd x y m'" "x |\<notin>| fmdom m'"
81113
6fefd6c602fa clarified syntax for opening bundles;
wenzelm
parents: 80914
diff changeset
  1191
using that including fmap.lifting and fset.lifting
66274
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1192
proof transfer
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1193
  fix m P
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1194
  assume "finite (dom m)"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1195
  assume empty: P if "m = Map.empty"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1196
  assume map_upd: P if "finite (dom m')" "m = map_upd x y m'" "x \<notin> dom m'" for x y m'
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1197
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1198
  show P
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1199
    proof (cases "m = Map.empty")
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1200
      case True thus ?thesis using empty by simp
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1201
    next
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1202
      case False
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1203
      hence "dom m \<noteq> {}" by simp
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1204
      then obtain x where "x \<in> dom m" by blast
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1205
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1206
      let ?m' = "map_drop x m"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1207
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1208
      show ?thesis
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1209
        proof (rule map_upd)
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1210
          show "finite (dom ?m')"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1211
            using \<open>finite (dom m)\<close>
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1212
            unfolding map_drop_def
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1213
            by auto
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1214
        next
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1215
          show "m = map_upd x (the (m x)) ?m'"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1216
            using \<open>x \<in> dom m\<close> unfolding map_drop_def map_filter_def map_upd_def
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1217
            by auto
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1218
        next
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1219
          show "x \<notin> dom ?m'"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1220
            unfolding map_drop_def map_filter_def
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1221
            by auto
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1222
        qed
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1223
    qed
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1224
qed
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1225
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1226
lemma fmap_induct[case_names fmempty fmupd, induct type: fmap]:
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1227
  assumes "P fmempty"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1228
  assumes "(\<And>x y m. P m \<Longrightarrow> fmlookup m x = None \<Longrightarrow> P (fmupd x y m))"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1229
  shows "P m"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1230
proof (induction "fmdom m" arbitrary: m rule: fset_induct_stronger)
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1231
  case empty
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1232
  hence "m = fmempty"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1233
    by (metis fmrestrict_fset_dom fmrestrict_fset_null)
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1234
  with assms show ?case
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1235
    by simp
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1236
next
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1237
  case (insert x S)
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1238
  hence "S = fmdom (fmdrop x m)"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1239
    by auto
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1240
  with insert have "P (fmdrop x m)"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1241
    by auto
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1242
  moreover
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1243
  obtain y where "fmlookup m x = Some y"
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1244
    using insert.hyps by force
66274
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1245
  hence "m = fmupd x y (fmdrop x m)"
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1246
    by (auto intro: fmap_ext)
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1247
  ultimately show ?case
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1248
    by (metis assms(2) fmdrop_lookup)
66274
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1249
qed
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1250
be8d3819c21c more material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 66273
diff changeset
  1251
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1252
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
  1253
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1254
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
  1255
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1256
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
  1257
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1258
instance proof
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1259
  fix m n :: "('a, 'b) fmap"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 66398
diff changeset
  1260
  have "fmrel (=) 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
  1261
    by transfer' (simp add: option.rel_eq rel_fun_eq)
64180
Lars Hupel <lars.hupel@mytum.de>
parents: 64179
diff changeset
  1262
  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
  1263
    unfolding equal_fmap_def
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1264
    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
  1265
qed
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1266
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1267
end
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1268
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1269
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
  1270
by force
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1271
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1272
lemma fmrel_code:
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1273
  "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
  1274
    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
  1275
    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
  1276
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
  1277
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
  1278
66291
f32968e099d5 tuned code setup
Lars Hupel <lars.hupel@mytum.de>
parents: 66282
diff changeset
  1279
lemmas [code] =
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1280
  fmrel_code
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1281
  fmran'_alt_def
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1282
  fmdom'_alt_def
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1283
  fmfilter_alt_defs
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1284
  pred_fmap_fmpred
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1285
  fmsubset_alt_def
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1286
  fmupd_alt_def
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1287
  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
  1288
  fmpred_alt_def
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1289
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1290
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1291
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
  1292
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
  1293
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1294
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
  1295
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1296
lemma fmlookup_of_list[code]: "fmlookup (fmap_of_list m) = map_of m"
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1297
by transfer simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1298
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1299
lemma fmempty_of_list[code]: "fmempty = fmap_of_list []"
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1300
by transfer simp
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1301
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1302
lemma fmran_of_list[code]: "fmran (fmap_of_list m) = snd |`| fset_of_list (AList.clearjunk m)"
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1303
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
  1304
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1305
lemma fmdom_of_list[code]: "fmdom (fmap_of_list m) = fst |`| fset_of_list m"
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1306
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
  1307
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1308
lemma fmfilter_of_list[code]: "fmfilter P (fmap_of_list m) = fmap_of_list (filter (\<lambda>(k, _). P k) m)"
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1309
by transfer' auto
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1310
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1311
lemma fmadd_of_list[code]: "fmap_of_list m ++\<^sub>f fmap_of_list n = fmap_of_list (AList.merge m n)"
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1312
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
  1313
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1314
lemma fmmap_of_list[code]: "fmmap f (fmap_of_list m) = fmap_of_list (map (apsnd f) m)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1315
  apply transfer
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1316
  by (metis (no_types, lifting) apsnd_conv map_eq_conv map_of_map old.prod.case old.prod.exhaust)
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1317
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
  1318
lemma fmmap_keys_of_list[code]:
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
  1319
  "fmmap_keys f (fmap_of_list m) = fmap_of_list (map (\<lambda>(a, b). (a, f a b)) m)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1320
  apply transfer
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1321
  subgoal for f m by (induction m) (auto simp: apsnd_def map_prod_def fun_eq_iff)
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1322
  done
66269
0820c8368320 more material on fmaps
Lars Hupel <lars.hupel@mytum.de>
parents: 66268
diff changeset
  1323
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
  1324
lemma fmimage_of_list[code]:
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
  1325
  "fmimage (fmap_of_list m) A = fset_of_list (map snd (filter (\<lambda>(k, _). k |\<in>| A) (AList.clearjunk m)))"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1326
  apply (subst fmimage_alt_def)
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1327
  apply (subst fmfilter_alt_defs)
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1328
  apply (subst fmfilter_of_list)
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1329
  apply (subst fmran_of_list)
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1330
  apply transfer'
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1331
  by (metis AList.restrict_eq clearjunk_restrict list.set_map)
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
  1332
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
  1333
lemma fmcomp_list[code]:
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
  1334
  "fmap_of_list m \<circ>\<^sub>f fmap_of_list n = fmap_of_list (AList.compose n m)"
80777
623d46973cbe More tidying of old proofs
paulson <lp15@cam.ac.uk>
parents: 78117
diff changeset
  1335
  by (rule fmap_ext) (simp add: fmlookup_of_list compose_conv map_comp_def split: option.splits)
68810
db97c1ed115e material on finite maps
Lars Hupel <lars.hupel@mytum.de>
parents: 68757
diff changeset
  1336
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1337
end
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1338
66267
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1339
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1340
subsection \<open>Instances\<close>
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1341
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1342
lemma exists_map_of:
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1343
  assumes "finite (dom m)" shows "\<exists>xs. map_of xs = m"
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1344
  using assms
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1345
proof (induction "dom m" arbitrary: m)
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1346
  case empty
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1347
  hence "m = Map.empty"
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1348
    by auto
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1349
  moreover have "map_of [] = Map.empty"
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1350
    by simp
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1351
  ultimately show ?case
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1352
    by blast
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1353
next
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1354
  case (insert x F)
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1355
  hence "F = dom (map_drop x m)"
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1356
    unfolding map_drop_def map_filter_def dom_def by auto
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1357
  with insert have "\<exists>xs'. map_of xs' = map_drop x m"
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1358
    by auto
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1359
  then obtain xs' where "map_of xs' = map_drop x m"
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1360
    ..
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1361
  moreover obtain y where "m x = Some y"
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1362
    using insert unfolding dom_def by blast
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1363
  ultimately have "map_of ((x, y) # xs') = m"
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1364
    using \<open>insert x F = dom m\<close>
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1365
    unfolding map_drop_def map_filter_def
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1366
    by auto
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1367
  thus ?case
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1368
    ..
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1369
qed
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1370
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1371
lemma exists_fmap_of_list: "\<exists>xs. fmap_of_list xs = m"
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1372
by transfer (rule exists_map_of)
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1373
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1374
lemma fmap_of_list_surj[simp, intro]: "surj fmap_of_list"
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1375
proof -
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1376
  have "x \<in> range fmap_of_list" for x :: "('a, 'b) fmap"
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1377
    unfolding image_iff
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1378
    using exists_fmap_of_list by (metis UNIV_I)
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1379
  thus ?thesis by auto
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1380
qed
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1381
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1382
instance fmap :: (countable, countable) countable
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1383
proof
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1384
  obtain to_nat :: "('a \<times> 'b) list \<Rightarrow> nat" where "inj to_nat"
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1385
    by (metis ex_inj)
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1386
  moreover have "inj (inv fmap_of_list)"
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1387
    using fmap_of_list_surj by (rule surj_imp_inj_inv)
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1388
  ultimately have "inj (to_nat \<circ> inv fmap_of_list)"
69700
7a92cbec7030 new material about summations and powers, along with some tweaks
paulson <lp15@cam.ac.uk>
parents: 69593
diff changeset
  1389
    by (rule inj_compose)
66267
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1390
  thus "\<exists>to_nat::('a, 'b) fmap \<Rightarrow> nat. inj to_nat"
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1391
    by auto
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1392
qed
04b626416eae fmaps are countable
Lars Hupel <lars.hupel@mytum.de>
parents: 64267
diff changeset
  1393
66282
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
  1394
instance fmap :: (finite, finite) finite
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
  1395
proof
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
  1396
  show "finite (UNIV :: ('a, 'b) fmap set)"
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
  1397
    by (rule finite_imageD) auto
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
  1398
qed
e5ba49a72ab9 fmap is finite
Lars Hupel <lars.hupel@mytum.de>
parents: 66274
diff changeset
  1399
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1400
lifting_update fmap.lifting
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1401
lifting_forget fmap.lifting
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
  1402
68909
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1403
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1404
subsection \<open>Tests\<close>
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1405
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1406
\<comment> \<open>Code generation\<close>
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1407
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1408
export_code
78117
7735645667f0 redefined FSet.fBall and FSet.fBex as abbreviations based on Set.Ball and Set.Bex
desharna
parents: 71262
diff changeset
  1409
  Ball fset fmrel fmran fmran' fmdom fmdom' fmpred pred_fmap fmsubset fmupd fmrel_on_fset
68909
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1410
  fmdrop fmdrop_set fmdrop_fset fmrestrict_set fmrestrict_fset fmimage fmlookup fmempty
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1411
  fmfilter fmadd fmmap fmmap_keys fmcomp
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1412
  checking SML Scala Haskell? OCaml?
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1413
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69313
diff changeset
  1414
\<comment> \<open>\<open>lifting\<close> through \<^type>\<open>fmap\<close>\<close>
68909
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1415
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1416
experiment begin
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1417
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1418
context includes fset.lifting begin
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1419
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1420
lift_definition test1 :: "('a, 'b fset) fmap" is "fmempty :: ('a, 'b set) fmap"
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1421
  by auto
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1422
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1423
lift_definition test2 :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b fset) fmap" is "\<lambda>a b. fmupd a {b} fmempty"
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1424
  by auto
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1425
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1426
end
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1427
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1428
end
34e777447ed5 material on finite sets
Lars Hupel <lars.hupel@mytum.de>
parents: 68810
diff changeset
  1429
67485
89f5d876a656 repair malformed fundef_cong rule
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
  1430
end