Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma

Benutzer


products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Zippy/document/ Datei vom 29.4.2026 mit Größe 536 B

Quellcode-Bibliothek Map_Extra.thy

Sprache: Isabelle

(******************************************************************************)
(* Project: Isabelle/UTP Toolkit                                              *)
(* File: Map_Extra.thy                                                        *)
(* Authors: Simon Foster and Frank Zeyda                                      *)
(* Emails: simon.foster@york.ac.uk and frank.zeyda@york.ac.uk                 *)
(******************************************************************************)

section ‹

Map_Extra
imports
"HOL-Library.Countable_Set"
"HOL-Library.Monad_Syntax"

‹ Functional Relations ›

functional :: "('a * 'b) set ==> bool" where
functional g = inj_on fst g"

functional_list :: "('a * 'b) list ==> bool" where
functional_list xs = (∀ x y z. ListMem (x,y) xs ∧ ListMem (x,z) xs ⟶ y = z)"

functional_insert [simp]: "functional (insert (x,y) g) ⟷ (g``{x} ⊆ {y} ∧ functional g)"
by (auto simp add:functional_def inj_on_def image_def)

functional_list_nil[simp]: "functional_list []"
by (simp add:functional_list_def ListMem_iff)

functional_list: "functional_list xs ⟷ functional (set xs)"
apply (induct xs)
apply (simp add:functional_def)
apply (simp add:functional_def functional_list_def ListMem_iff)
apply (safe)
apply (force)
apply (force)
apply (force)
apply (force)
apply (force)
apply (force)
apply (force)
apply (force)
done

‹ Graphing Maps ›

map_graph :: "('a ⇀ 'b) ==> ('a * 'b) set" where
map_graph f = {(x,y) | x y. f x = Some y}"

graph_map :: "('a * 'b) set ==> ('a ⇀ 'b)" where
graph_map g = (λ x. if (x ∈ fst ` g) then Some (SOME y. (x,y) ∈ g) else None)"

graph_map' :: "('a × 'b) set ⇀ ('a ⇀ 'b)" where
graph_map' R = (if (functional R) then Some (graph_map R) else None)"

map_graph_mem_equiv: "(x, y) ∈ map_graph f ⟷ f(x) = Some y"
by (simp add: map_graph_def)

map_graph_functional[simp]: "functional (map_graph f)"
by (simp add:functional_def map_graph_def inj_on_def)

map_graph_countable [simp]: "countable (dom f) ==> countable (map_graph f)"
apply (auto simp add:map_graph_def countable_def)
apply (rename_tac f')
apply (rule_tac x="f' ∘ fst" in exI)
apply (auto simp add:inj_on_def dom_def)
apply fastforce
done

map_graph_inv [simp]: "graph_map (map_graph f) = f"
by (auto intro!:ext simp add:map_graph_def graph_map_def image_def)

graph_map_empty[simp]: "graph_map {} = Map.empty"
by (simp add:graph_map_def)

graph_map_insert [simp]: "[functional g; g``{x} ⊆ {y}] ==> graph_map (insert (x,y) g) = (graph_map g)(x ↦ y)"
by (rule ext, auto simp add:graph_map_def)

dom_map_graph: "dom f = Domain(map_graph f)"
by (simp add: map_graph_def dom_def image_def)

ran_map_graph: "ran f = Range(map_graph f)"
by (simp add: map_graph_def ran_def image_def)

ran_map_add_subset:
"ran (x ++ y) ⊆ (ran x) ∪ (ran y)"
by (auto simp add:ran_def)

finite_dom_graph: "finite (dom f) ==> finite (map_graph f)"
by (metis dom_map_graph finite_imageD fst_eq_Domain functional_def map_graph_functional)

finite_dom_ran [simp]: "finite (dom f) ==> finite (ran f)"
by (metis finite_Range finite_dom_graph ran_map_graph)

graph_map_inv [simp]: "functional g ==> map_graph (graph_map g) = g"
apply (auto simp add:map_graph_def graph_map_def functional_def)
apply (metis (lifting, no_types) image_iff option.distinct(1) option.inject someI surjective_pairing)
apply (simp add:inj_on_def)
apply (metis fst_conv snd_conv some_equality)
apply (metis (lifting) fst_conv image_iff)
done

graph_map_dom: "dom (graph_map R) = fst ` R"
by (simp add: graph_map_def dom_def)

graph_map_countable_dom: "countable R ==> countable (dom (graph_map R))"
by (simp add: graph_map_dom)

countable_ran:
assumes "countable (dom f)"
shows "countable (ran f)"
-
have "countable (map_graph f)"
by (simp add: assms)
then have "countable (Range(map_graph f))"
by (simp add: Range_snd)
thus ?thesis
by (simp add: ran_map_graph)

map_graph_inv' [simp]:
"graph_map' (map_graph f) = Some f"
by (simp add: graph_map'_def)

map_graph_inj:
"inj map_graph"
by (metis injI map_graph_inv)

map_eq_graph: "f = g ⟷ map_graph f = map_graph g"
by (auto simp add: inj_eq map_graph_inj)

map_le_graph: "f ⊆_m g ⟷ map_graph f ⊆ map_graph g"
by (force simp add: map_le_def map_graph_def)

map_graph_comp: "map_graph (g ∘_m f) = (map_graph f) O (map_graph g)"
apply (auto simp add: map_comp_def map_graph_def relcomp_unfold)
apply (rename_tac a b)
apply (case_tac "f a", auto)
done

‹ Map Application ›

map_apply :: "('a ⇀ 'b) ==> 'a ==> 'b" (‹_'(_')_m› [999,0] 999) where
map_apply = (λ f x. the (f x))"

‹ Map Membership ›

map_member :: "'a × 'b ==> ('a ⇀ 'b) ==> bool" (infix ‹∈_m› 50) where
(k, v) ∈_m m ⟷ m(k) = Some(v)"

map_ext:
"[ ∧ x y. (x, y) ∈_m A ⟷ (x, y) ∈_m B ] ==> A = B"
by (rule ext, auto, metis not_Some_eq)

map_member_alt_def:
"(x, y) ∈_m A ⟷ (x ∈ dom A ∧ A(x)_m = y)"
by (auto simp add: map_apply_def)

map_le_member:
"f ⊆_m g ⟷ (∀ x y. (x,y) ∈_m f ⟶ (x,y) ∈_m g)"
by (force simp add: map_le_def)

‹ Preimage ›

preimage :: "('a ⇀ 'b) ==> 'b set ==> 'a set" where
preimage f B = {x ∈ dom(f). the(f(x)) ∈ B}"

preimage_range: "preimage f (ran f) = dom f"
by (auto simp add: preimage_def ran_def)

dom_preimage: "dom (m ∘_m f) = preimage f (dom m)"
apply (auto simp add: dom_def preimage_def)
apply (meson map_comp_Some_iff)
apply (metis map_comp_def option.case_eq_if option.distinct(1))
done

countable_preimage:
"[ countable A; inj_on f (preimage f A) ] ==> countable (preimage f A)"
apply (auto simp add: countable_def)
apply (rename_tac g)
apply (rule_tac x="g ∘ the ∘ f" in exI)
apply (rule inj_onI)
apply (drule inj_onD)
apply (auto simp add: preimage_def inj_onD)
done

‹ Minus operation for maps ›

map_minus :: "('a ⇀ 'b) ==> ('a ⇀ 'b) ==> ('a ⇀ 'b)" (infixl ‹--› 100)
"map_minus f g = (λ x. if (f x = g x) then None else f x)"

map_minus_apply [simp]: "y ∈ dom(f -- g) ==> (f -- g)(y)_m = f(y)_m"
by (auto simp add: map_minus_def dom_def map_apply_def)

map_member_plus:
"(x, y) ∈_m f ++ g ⟷ ((x ∉ dom(g) ∧ (x, y) ∈_m f) ∨ (x, y) ∈_m g)"
by (auto simp add: map_add_Some_iff)

map_member_minus:
"(x, y) ∈_m f -- g ⟷ (x, y) ∈_m f ∧ (¬ (x, y) ∈_m g)"
by (auto simp add: map_minus_def)

map_minus_plus_commute:
"dom(g) ∩ dom(h) = {} ==> (f -- g) ++ h = (f ++ h) -- g"
apply (rule map_ext)
apply (auto simp add: map_member_plus map_member_minus simp del: map_member.simps)
apply (auto simp add: map_member_alt_def)
done

map_graph_minus: "map_graph (f -- g) = map_graph f - map_graph g"
by (auto simp add: map_minus_def map_graph_def, (meson option.distinct(1))+)

map_minus_common_subset:
"[ h ⊆_m f; h ⊆_m g ] ==> (f -- h = g -- h) = (f = g)"
by (auto simp add: map_eq_graph map_graph_minus map_le_graph)

‹ Map Bind ›

‹ Create some extra intro/elim rules to help dealing with proof about option bind. ›

option_bindSomeE [elim!]:
"[ X >>= F = Some(v); ∧ x. [ X = Some(x); F(x) = Some(v) ] ==> P ] ==> P"
by (case_tac X, auto)

option_bindSomeI [intro]:
"[ X = Some(x); F(x) = Some(y) ] ==> X >>= F = Some(y)"
by (simp)

ifSomeE [elim]: "[ (if c then Some(x) else None) = Some(y); [ c; x = y ] ==> P ] ==> P"
by (case_tac c, auto)

‹ Range Restriction ›

‹A range restriction operator; only domain restriction is provided in HOL.›

ran_restrict_map :: "('a ⇀ 'b) ==> 'b set ==> 'a ⇀ 'b" (‹_↿› [111,110] 110) where
ran_restrict_map f B = (λx. do { v <- f(x); if (v ∈ B) then Some(v) else None })"

ran_restrict_empty [simp]: "f↿_} = Map.empty"
by (simp add:ran_restrict_map_def)

ran_restrict_ran [simp]: "f↿_(f) = f"
apply (auto simp add:ran_restrict_map_def ran_def)
apply (rule ext)
apply (case_tac "f(x)", auto)
done

ran_ran_restrict [simp]: "ran(f↿) = ran(f) ∩ B"
by (auto intro!:option_bindSomeI simp add:ran_restrict_map_def ran_def)

dom_ran_restrict: "dom(f↿) ⊆ dom(f)"
by (auto simp add:ran_restrict_map_def dom_def)

ran_restrict_finite_dom [intro]:
"finite(dom(f)) ==> finite(dom(f↿))"
by (metis finite_subset dom_ran_restrict)

dom_Some [simp]: "dom (Some ∘ f) = UNIV"
by (auto)

dom_left_map_add [simp]: "x ∈ dom g ==> (f ++ g) x = g x"
by (auto simp add:map_add_def dom_def)

dom_right_map_add [simp]: "[ x ∉ dom g; x ∈ dom f ] ==> (f ++ g) x = f x"
by (auto simp add:map_add_def dom_def)

map_add_restrict:
"f ++ g = (f |` (- dom g)) ++ g"
by (rule ext, auto simp add: map_add_def restrict_map_def)

‹ Map Inverse and Identity ›

map_inv :: "('a ⇀ 'b) ==> ('b ⇀ 'a)" where
map_inv f ≡ λ y. if (y ∈ ran f) then Some (SOME x. f x = Some y) else None"

map_id_on :: "'a set ==> ('a ⇀ 'a)" where
map_id_on xs ≡ λ x. if (x ∈ xs) then Some x else None"

map_id_on_in [simp]:
"x ∈ xs ==> map_id_on xs x = Some x"
by (simp add:map_id_on_def)

map_id_on_out [simp]:
"x ∉ xs ==> map_id_on xs x = None"
by (simp add:map_id_on_def)

map_id_dom [simp]: "dom (map_id_on xs) = xs"
by (simp add:dom_def map_id_on_def)

map_id_ran [simp]: "ran (map_id_on xs) = xs"
by (force simp add:ran_def map_id_on_def)

map_id_on_UNIV[simp]: "map_id_on UNIV = Some"
by (simp add:map_id_on_def)

map_id_on_inj [simp]:
"inj_on (map_id_on xs) xs"
by (simp add:inj_on_def)

map_inv_empty [simp]: "map_inv Map.empty = Map.empty"
by (simp add:map_inv_def)

map_inv_id [simp]:
"map_inv (map_id_on xs) = map_id_on xs"
by (force simp add:map_inv_def map_id_on_def ran_def)

map_inv_Some [simp]: "map_inv Some = Some"
by (simp add:map_inv_def ran_def)

map_inv_f_f [simp]:
"[ inj_on f (dom f); f x = Some y ] ==> map_inv f y = Some x"
apply (auto simp add: map_inv_def)
apply (rule some_equality)
apply (auto simp add:inj_on_def dom_def ran_def)
done

dom_map_inv [simp]:
"dom (map_inv f) = ran f"
by (auto simp add:map_inv_def)

ran_map_inv [simp]:
"inj_on f (dom f) ==> ran (map_inv f) = dom f"
apply (auto simp add:map_inv_def ran_def)
apply (rename_tac a b)
apply (rule_tac x="a" in exI)
apply (force intro:someI)
apply (rename_tac x y)
apply (rule_tac x="y" in exI)
apply (auto)
apply (rule some_equality, simp_all)
apply (auto simp add:inj_on_def dom_def)
done

dom_image_ran: "f ` dom f = Some ` ran f"
by (auto simp add:dom_def ran_def image_def)

inj_map_inv [intro]:
"inj_on f (dom f) ==> inj_on (map_inv f) (ran f)"
apply (auto simp add:map_inv_def inj_on_def dom_def ran_def)
apply (rename_tac x y u v)
apply (frule_tac P="λ xa. f xa = Some x" in some_equality)
apply (auto)
apply (metis (mono_tags) option.sel someI)
done

inj_map_bij: "inj_on f (dom f) ==> bij_betw f (dom f) (Some ` ran f)"
by (auto simp add:inj_on_def dom_def ran_def image_def bij_betw_def)

map_inv_map_inv [simp]:
assumes "inj_on f (dom f)"
shows "map_inv (map_inv f) = f"
-

from assms have "inj_on (map_inv f) (ran f)"
by auto

thus ?thesis
apply (rule_tac ext)
apply (rename_tac x)
apply (case_tac "∃ y. map_inv f y = Some x")
apply (auto)[1]
apply (simp add:map_inv_def)
apply (rename_tac x y)
apply (case_tac "y ∈ ran f", simp_all)
apply (auto)
apply (rule someI2_ex)
apply (simp add:ran_def)
apply (simp)
apply (metis assms dom_image_ran dom_map_inv image_iff map_add_dom_app_simps(2) map_add_dom_app_simps(3) ran_map_inv)
done

map_self_adjoin_complete [intro]:
assumes "dom f ∩ ran f = {}" "inj_on f (dom f)"
shows "inj_on (map_inv f ++ f) (dom f ∪ ran f)"
apply (rule inj_onI)
apply (insert assms)
apply (rename_tac x y)
apply (case_tac "x ∈ dom f")
apply (simp)
apply (case_tac "y ∈ dom f")
apply (simp add:inj_on_def)
apply (case_tac "y ∈ ran f")
apply (subgoal_tac "y ∈ dom (map_inv f)")
apply (simp)
apply (metis Int_iff domD empty_iff ranI ran_map_inv)
apply (simp)
apply (simp)
apply (simp)
apply (case_tac "y ∈ dom f")
apply (simp)
apply (case_tac "y ∈ ran f")
apply (subgoal_tac "y ∈ dom (map_inv f)")
apply (simp)
apply (metis Int_iff empty_iff)
apply (simp)
apply (metis Int_iff domD empty_iff ranI ran_map_inv)
apply (simp)
apply (metis (lifting) inj_map_inv inj_on_contraD)
done

inj_completed_map [intro]:
"[ dom f = ran f; inj_on f (dom f) ] ==> inj (Some ++ f)"
apply (drule inj_map_bij)
apply (auto simp add:bij_betw_def)
apply (auto simp add:inj_on_def)[1]
apply (rename_tac x y)
apply (case_tac "x ∈ dom f")
apply (simp)
apply (case_tac "y ∈ dom f")
apply (simp)
apply (simp add:ran_def)
apply (case_tac "y ∈ dom f")
apply (auto intro:ranI)
done

bij_completed_map [intro]:
"[ dom f = ran f; inj_on f (dom f) ] ==>
bij_betw (Some ++ f) UNIV (range Some)"
apply (auto simp add:bij_betw_def)
apply (rename_tac x)
apply (case_tac "x ∈ dom f")
apply (simp)
apply (metis domD rangeI)
apply (simp)
apply (simp add:image_def)
apply (metis (full_types) dom_image_ran dom_left_map_add image_iff map_add_dom_app_simps(3))
done

bij_map_Some:
"bij_betw f a (Some ` b) ==> bij_betw (the ∘ f) a b"
apply (simp add:bij_betw_def)
apply (safe)
apply (metis (opaque_lifting, no_types) comp_inj_on_iff f_the_inv_into_f inj_on_inverseI option.sel)
apply (metis (opaque_lifting, no_types) image_iff option.sel)
apply (metis Option.these_def Some_image_these_eq image_image these_image_Some_eq)
done

ran_map_add [simp]:
"m`(dom m ∩ dom n) = n`(dom m ∩ dom n) ==>
ran(m++n) = ran n ∪ ran m"
apply (auto simp add:ran_def)
apply (metis map_add_find_right)
apply (rename_tac x a)
apply (case_tac "a ∈ dom n")
apply (subgoal_tac "∃ b. n b = Some x")
apply (auto)
apply (rename_tac x a b y)
apply (rule_tac x="b" in exI)
apply (simp)
apply (metis (opaque_lifting, no_types) IntI domI image_iff)
apply (metis (full_types) map_add_None map_add_dom_app_simps(1) map_add_dom_app_simps(3) not_None_eq)
done

ran_maplets [simp]:
"[ length xs = length ys; distinct xs ] ==> ran [xs [↦] ys] = set ys"
by (induct rule:list_induct2, simp_all)

inj_map_add:
"[ inj_on f (dom f); inj_on g (dom g); ran f ∩ ran g = {} ] ==>
inj_on (f ++ g) (dom f ∪ dom g)"
apply (auto simp add:inj_on_def)
apply (metis (full_types) disjoint_iff_not_equal domI dom_left_map_add map_add_dom_app_simps(3) ranI)
apply (metis domI)
apply (metis disjoint_iff_not_equal ranI)
apply (metis disjoint_iff_not_equal domIff map_add_Some_iff ranI)
apply (metis domI)
done

map_inv_add [simp]:
assumes "inj_on f (dom f)" "inj_on g (dom g)"
"dom f ∩ dom g = {}" "ran f ∩ ran g = {}"
shows "map_inv (f ++ g) = map_inv f ++ map_inv g"
(rule ext)

from assms have minj: "inj_on (f ++ g) (dom (f ++ g))"
by (simp, metis inj_map_add sup_commute)

fix x
have "x ∈ ran g ==> map_inv (f ++ g) x = (map_inv f ++ map_inv g) x"
proof -
assume ran:"x ∈ ran g"
then obtain y where dom:"g y = Some x" "y ∈ dom g"
by (auto simp add:ran_def)

hence "(f ++ g) y = Some x"
by simp

with assms minj ran dom show "map_inv (f ++ g) x = (map_inv f ++ map_inv g) x"
by simp
qed

moreover have "[ x ∉ ran g; x ∈ ran f ] ==> map_inv (f ++ g) x = (map_inv f ++ map_inv g) x"
proof -
assume ran:"x ∉ ran g" "x ∈ ran f"
with assms obtain y where dom:"f y = Some x" "y ∈ dom f" "y ∉ dom g"
by (auto simp add:ran_def)

with ran have "(f ++ g) y = Some x"
by (simp)

with assms minj ran dom show "map_inv (f ++ g) x = (map_inv f ++ map_inv g) x"
by simp
qed

moreover from assms minj have "[ x ∉ ran g; x ∉ ran f ] ==> map_inv (f ++ g) x = (map_inv f ++ map_inv g) x"
apply (auto simp add:map_inv_def ran_def map_add_def)
apply (metis dom_left_map_add map_add_def map_add_dom_app_simps(3))
done

ultimately show "map_inv (f ++ g) x = (map_inv f ++ map_inv g) x"
apply (case_tac "x ∈ ran g")
apply (simp)
apply (case_tac "x ∈ ran f")
apply (simp_all)
done

map_add_lookup [simp]:
"x ∉ dom f ==> ([x ↦ y] ++ f) x = Some y"
by (simp add:map_add_def dom_def)

map_add_Some: "Some ++ f = map_id_on (- dom f) ++ f"
apply (rule ext)
apply (rename_tac x)
apply (case_tac "x ∈ dom f")
apply (simp_all)
done

distinct_map_dom:
"x ∉ set xs ==> x ∉ dom [xs [↦] ys]"
by (simp add:dom_def)

distinct_map_ran:
"[ distinct xs; y ∉ set ys; length xs = length ys ] ==>
y ∉ ran ([xs [↦] ys])"
apply (simp add:map_upds_def)
apply (subgoal_tac "distinct (map fst (rev (zip xs ys)))")
apply (simp add:ran_distinct)
apply (metis (opaque_lifting, no_types) image_iff set_zip_rightD surjective_pairing)
apply (simp add:zip_rev[THEN sym])

maplets_lookup[rule_format,dest]:
"[ length xs = length ys; distinct xs ] ==>
∀ y. [xs [↦] ys] x = Some y ⟶ y ∈ set ys"
by (induct rule:list_induct2, auto)

maplets_distinct_inj [intro]:
"[ length xs = length ys; distinct xs; distinct ys; set xs ∩ set ys = {} ] ==>
inj_on [xs [↦] ys] (set xs)"
apply (induct rule:list_induct2)
apply (simp_all)
apply (rule conjI)
apply (rule inj_onI)
apply (rename_tac x xs y ys xa ya)
apply (case_tac "xa = x")
apply (simp)
apply (case_tac "xa = y")
apply (simp)
apply (simp)
apply (case_tac "ya = x")
apply (simp)
apply (simp add:inj_on_def)
apply (auto)
apply (rename_tac x xs y ys xa)
apply (case_tac "xa = y")
apply (simp)
apply (metis maplets_lookup)
done

map_inv_maplet[simp]: "map_inv [x ↦ y] = [y ↦ x]"
by (auto simp add:map_inv_def)

map_inv_maplets [simp]:
"[ length xs = length ys; distinct xs; distinct ys; set xs ∩ set ys = {} ] ==>
map_inv [xs [↦] ys] = [ys [↦] xs]"
apply (induct rule:list_induct2)
apply (simp_all)
apply (rename_tac x xs y ys)
apply (subgoal_tac "map_inv ([xs [↦] ys] ++ [x ↦ y]) = map_inv [xs [↦] ys] ++ map_inv [x ↦ y]")
apply (simp)
apply (rule map_inv_add)
apply (auto)
done

maplets_lookup_nth [rule_format,simp]:
"[ length xs = length ys; distinct xs ] ==>
∀ i < length ys. [xs [↦] ys] (xs ! i) = Some (ys ! i)"
apply (induct rule:list_induct2)
apply (auto)
apply (rename_tac x xs y ys i)
apply (case_tac i)
apply (simp_all)
apply (metis nth_mem)
apply (rename_tac x xs y ys i)
apply (case_tac i)
apply (auto)
done

inv_map_inv:
"[ inj_on f (dom f); ran f = dom f ]
==> inv (the ∘ (Some ++ f)) = the ∘ map_inv (Some ++ f)"
apply (rule ext)
apply (simp add:map_add_Some)
apply (simp add:inv_def)
apply (rename_tac x)
apply (case_tac "∃ y. f y = Some x")
apply (erule exE)
apply (rename_tac x y)
apply (subgoal_tac "x ∈ ran f")
apply (subgoal_tac "y ∈ dom f")
apply (simp)
apply (rule some_equality)
apply (simp)
apply (metis (opaque_lifting, mono_tags) domD domI dom_left_map_add inj_on_contraD map_add_Some map_add_dom_app_simps(3) option.sel)
apply (simp add:dom_def)
apply (metis ranI)
apply (simp)
apply (rename_tac x)
apply (subgoal_tac "x ∉ ran f")
apply (simp)
apply (rule some_equality)
apply (simp)
apply (metis domD dom_left_map_add map_add_Some map_add_dom_app_simps(3) option.sel)
apply (metis dom_image_ran image_iff)
done

map_comp_dom: "dom (g ∘_m f) ⊆ dom f"
by (metis (lifting, full_types) Collect_mono dom_def map_comp_simps(1))

map_comp_assoc: "f ∘_m (g ∘_m h) = f ∘_m g ∘_m h"

fix x
show "(f ∘_m (g ∘_m h)) x = (f ∘_m g ∘_m h) x"
proof (cases "h x")
case None thus ?thesis
by (auto simp add: map_comp_def)
next
case (Some y) thus ?thesis
by (auto simp add: map_comp_def)
qed

map_comp_runit [simp]: "f ∘_m Some = f"
by (simp add: map_comp_def)

map_comp_lunit [simp]: "Some ∘_m f = f"

fix x
show "(Some ∘_m f) x = f x"
proof (cases "f x")
case None thus ?thesis
by (simp add: map_comp_def)
next
case (Some y) thus ?thesis
by (simp add: map_comp_def)
qed

map_comp_apply [simp]: "(f ∘_m g) x = g(x) >>= f"
by (auto simp add: map_comp_def option.case_eq_if)

‹ Merging of compatible maps ›

comp_map :: "('a ⇀ 'b) ==> ('a ⇀ 'b) ==> bool" (infixl ‹∥_m› 60) where
comp_map f g = (∀ x ∈ dom(f) ∩ dom(g). the(f(x)) = the(g(x)))"

comp_map_unit: "Map.empty ∥_m f"
by (simp add: comp_map_def)

comp_map_refl: "f ∥_m f"
by (simp add: comp_map_def)

comp_map_sym: "f ∥_m g ==> g ∥_m f"
by (simp add: comp_map_def)

merge :: "('a ⇀ 'b) set ==> 'a ⇀ 'b" where
merge fs =
(λ x. if (∃ f ∈ fs. x ∈ dom(f)) then (THE y. ∀ f ∈ fs. x ∈ dom(f) ⟶ f(x) = y) else None)"

merge_empty: "merge {} = Map.empty"
by (simp add: merge_def)

merge_singleton: "merge {f} = f"
apply (auto intro!: ext simp add: merge_def)
using option.collapse apply fastforce
done

‹ Conversion between lists and maps ›

map_of_list :: "'a list ==> (nat ⇀ 'a)" where
map_of_list xs = (λ i. if (i < length xs) then Some (xs!i) else None)"

map_of_list_nil [simp]: "map_of_list [] = Map.empty"
by (simp add: map_of_list_def)

dom_map_of_list [simp]: "dom (map_of_list xs) = {0..<length xs}"
by (auto simp add: map_of_list_def dom_def)

ran_map_of_list [simp]: "ran (map_of_list xs) = set xs"
apply (simp add: ran_def map_of_list_def)
apply (safe)
apply (force)
apply (meson in_set_conv_nth)
done

list_of_map :: "(nat ⇀ 'a) ==> 'a list" where
list_of_map f = (if (f = Map.empty) then [] else map (the ∘ f) [0 ..< Suc(GREATEST x. x ∈ dom f)])"

list_of_map_empty [simp]: "list_of_map Map.empty = []"
by (simp add: list_of_map_def)

list_of_map' :: "(nat ⇀ 'a) ⇀ 'a list" where
list_of_map' f = (if (∃ n. dom f = {0..<n}) then Some (list_of_map f) else None)"

map_of_list_inv [simp]: "list_of_map (map_of_list xs) = xs"
(cases "xs = []")
case True thus ?thesis by (simp)

case False
moreover hence "(GREATEST x. x ∈ dom (map_of_list xs)) = length xs - 1"
by (auto intro: Greatest_equality)
moreover from False have "map_of_list xs ≠ Map.empty"
by (metis ran_empty ran_map_of_list set_empty)
ultimately show ?thesis
by (auto simp add: list_of_map_def map_of_list_def intro: nth_equalityI)

‹ Map Comprehension ›

‹ Map comprehension simply converts a relation built through set comprehension into a map. ›

"_Mapcompr" :: "'a ==> 'b ==> idts ==> bool ==> 'a ⇀ 'b" (‹(1[_ ↦ _ |/_./ _])›)

"_Mapcompr" == graph_map

"_Mapcompr F G xs P" == "CONST graph_map {(F, G) | xs. P}"

map_compr_eta:
"[x ↦ y | x y. (x, y) ∈_m f] = f"
apply (rule ext)
apply (auto simp add: graph_map_def)
apply (metis (mono_tags, lifting) Domain.DomainI fst_eq_Domain mem_Collect_eq old.prod.case option.distinct(1) option.expand option.sel)
done

map_compr_simple:
"[x ↦ F x y | x y. (x, y) ∈_m f] = (λ x. do { y ← f(x); Some(F x y) })"
apply (rule ext)
apply (auto simp add: graph_map_def image_Collect)
done

map_compr_dom_simple [simp]:
"dom [x ↦ f x | x. P x] = {x. P x}"
by (force simp add: graph_map_dom image_Collect)

map_compr_ran_simple [simp]:
"ran [x ↦ f x | x. P x] = {f x | x. P x}"
apply (auto simp add: graph_map_def ran_def)
apply (metis (mono_tags, lifting) fst_eqD image_eqI mem_Collect_eq someI)
done

map_compr_eval_simple [simp]:
"[x ↦ f x | x. P x] x = (if (P x) then Some (f x) else None)"
by (auto simp add: graph_map_def image_Collect)

‹ Sorted lists from maps ›

sorted_list_of_map :: "('a::linorder ⇀ 'b) ==> ('a × 'b) list" where
sorted_list_of_map f = map (λ k. (k, the (f k))) (sorted_list_of_set(dom(f)))"

sorted_list_of_map_empty [simp]:
"sorted_list_of_map Map.empty = []"
by (simp add: sorted_list_of_map_def)

sorted_list_of_map_inv:
assumes "finite(dom(f))"
shows "map_of (sorted_list_of_map f) = f"
-
obtain A where "finite A" "A = dom(f)"
by (simp add: assms)
thus ?thesis
proof (induct A rule: finite_induct)
case empty thus ?thesis
by (simp add: sorted_list_of_map_def, metis dom_empty empty_iff map_le_antisym map_le_def)
next
case (insert x A) thus ?thesis
by (simp add: assms sorted_list_of_map_def map_of_map_keys)
qed

map_member.simps [simp del]

‹ Extra map lemmas ›

map_eqI:
"[ dom f = dom g; ∀ x∈dom(f). the(f x) = the(g x) ] ==> f = g"
by (metis domIff map_le_antisym map_le_def option.expand)

map_restrict_dom [simp]: "f |` dom f = f"
by (simp add: map_eqI)

map_restrict_dom_compl: "f |` (- dom f) = Map.empty"
by (metis dom_eq_empty_conv dom_restrict inf_compl_bot)

restrict_map_neg_disj:
"dom(f) ∩ A = {} ==> f |` (- A) = f"
by (auto simp add: restrict_map_def, rule ext, auto, metis disjoint_iff_not_equal domIff)

map_plus_restrict_dist: "(f ++ g) |` A = (f |` A) ++ (g |` A)"
by (auto simp add: restrict_map_def map_add_def)

map_plus_eq_left:
assumes "f ++ h = g ++ h"
shows "(f |` (- dom h)) = (g |` (- dom h))"
-
have "h |` (- dom h) = Map.empty"
by (metis Compl_disjoint dom_eq_empty_conv dom_restrict)
then have f2: "f |` (- dom h) = (f ++ h) |` (- dom h)"
by (simp add: map_plus_restrict_dist)
have "h |` (- dom h) = Map.empty"
by (metis (no_types) Compl_disjoint dom_eq_empty_conv dom_restrict)
then show ?thesis
using f2 assms by (simp add: map_plus_restrict_dist)

map_add_split:
"dom(f) = A ∪ B ==> (f |` A) ++ (f |` B) = f"
by (rule ext, auto simp add: map_add_def restrict_map_def option.case_eq_if)

map_le_via_restrict:
"f ⊆_m g ⟷ g |` dom(f) = f"
by (auto simp add: map_le_def restrict_map_def dom_def fun_eq_iff)

map_add_cancel:
"f ⊆_m g ==> f ++ (g -- f) = g"
by (auto simp add: map_le_def map_add_def map_minus_def fun_eq_iff option.case_eq_if)
(metis domIff)

map_le_iff_add: "f ⊆_m g ⟷ (∃ h. dom(f) ∩ dom(h) = {} ∧ f ++ h = g)"
apply (auto)
apply (rule_tac x="g -- f" in exI)
apply (metis (no_types, lifting) Int_emptyI domIff map_add_cancel map_le_def map_minus_def)
apply (simp add: map_add_comm)
done

map_add_comm_weak: "(∀ k ∈ dom m1 ∩ dom m2. m1(k) = m2(k)) ==> m1 ++ m2 = m2 ++ m1"
by (auto simp add: map_add_def option.case_eq_if fun_eq_iff)
(metis IntI domI option.inject)

Messung V0.5 in Prozent

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.35Bemerkung: ¤

*Bot Zugriff

Wurzel

Suchen

NIST Cobol Testsuite

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.