73326
|
1 |
(* Title: HOL/Library/Disjoint_FSets.thy
|
|
2 |
Author: Lars Hupel, TU München
|
|
3 |
*)
|
|
4 |
|
|
5 |
section \<open>Disjoint FSets\<close>
|
|
6 |
|
|
7 |
theory Disjoint_FSets
|
|
8 |
imports
|
|
9 |
"HOL-Library.Finite_Map"
|
|
10 |
"HOL-Library.Disjoint_Sets"
|
|
11 |
begin
|
|
12 |
|
|
13 |
context
|
|
14 |
includes fset.lifting
|
|
15 |
begin
|
|
16 |
|
|
17 |
lift_definition fdisjnt :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" is disjnt .
|
|
18 |
|
|
19 |
lemma fdisjnt_alt_def: "fdisjnt M N \<longleftrightarrow> (M |\<inter>| N = {||})"
|
|
20 |
by transfer (simp add: disjnt_def)
|
|
21 |
|
|
22 |
lemma fdisjnt_insert: "x |\<notin>| N \<Longrightarrow> fdisjnt M N \<Longrightarrow> fdisjnt (finsert x M) N"
|
|
23 |
by transfer' (rule disjnt_insert)
|
|
24 |
|
|
25 |
lemma fdisjnt_subset_right: "N' |\<subseteq>| N \<Longrightarrow> fdisjnt M N \<Longrightarrow> fdisjnt M N'"
|
|
26 |
unfolding fdisjnt_alt_def by auto
|
|
27 |
|
|
28 |
lemma fdisjnt_subset_left: "N' |\<subseteq>| N \<Longrightarrow> fdisjnt N M \<Longrightarrow> fdisjnt N' M"
|
|
29 |
unfolding fdisjnt_alt_def by auto
|
|
30 |
|
|
31 |
lemma fdisjnt_union_right: "fdisjnt M A \<Longrightarrow> fdisjnt M B \<Longrightarrow> fdisjnt M (A |\<union>| B)"
|
|
32 |
unfolding fdisjnt_alt_def by auto
|
|
33 |
|
|
34 |
lemma fdisjnt_union_left: "fdisjnt A M \<Longrightarrow> fdisjnt B M \<Longrightarrow> fdisjnt (A |\<union>| B) M"
|
|
35 |
unfolding fdisjnt_alt_def by auto
|
|
36 |
|
|
37 |
lemma fdisjnt_swap: "fdisjnt M N \<Longrightarrow> fdisjnt N M"
|
|
38 |
including fset.lifting by transfer' (auto simp: disjnt_def)
|
|
39 |
|
|
40 |
lemma distinct_append_fset:
|
|
41 |
assumes "distinct xs" "distinct ys" "fdisjnt (fset_of_list xs) (fset_of_list ys)"
|
|
42 |
shows "distinct (xs @ ys)"
|
|
43 |
using assms
|
|
44 |
by transfer' (simp add: disjnt_def)
|
|
45 |
|
|
46 |
lemma fdisjnt_contrI:
|
|
47 |
assumes "\<And>x. x |\<in>| M \<Longrightarrow> x |\<in>| N \<Longrightarrow> False"
|
|
48 |
shows "fdisjnt M N"
|
|
49 |
using assms
|
|
50 |
by transfer' (auto simp: disjnt_def)
|
|
51 |
|
|
52 |
lemma fdisjnt_Union_left: "fdisjnt (ffUnion S) T \<longleftrightarrow> fBall S (\<lambda>S. fdisjnt S T)"
|
|
53 |
by transfer' (auto simp: disjnt_def)
|
|
54 |
|
|
55 |
lemma fdisjnt_Union_right: "fdisjnt T (ffUnion S) \<longleftrightarrow> fBall S (\<lambda>S. fdisjnt T S)"
|
|
56 |
by transfer' (auto simp: disjnt_def)
|
|
57 |
|
|
58 |
lemma fdisjnt_ge_max: "fBall X (\<lambda>x. x > fMax Y) \<Longrightarrow> fdisjnt X Y"
|
|
59 |
by transfer (auto intro: disjnt_ge_max)
|
|
60 |
|
|
61 |
end
|
|
62 |
|
|
63 |
(* FIXME should be provable without lifting *)
|
|
64 |
lemma fmadd_disjnt: "fdisjnt (fmdom m) (fmdom n) \<Longrightarrow> m ++\<^sub>f n = n ++\<^sub>f m"
|
|
65 |
unfolding fdisjnt_alt_def
|
|
66 |
including fset.lifting fmap.lifting
|
|
67 |
apply transfer
|
|
68 |
apply (rule ext)
|
|
69 |
apply (auto simp: map_add_def split: option.splits)
|
|
70 |
done
|
|
71 |
|
|
72 |
end
|