author | wenzelm |
Wed, 12 Oct 2011 20:16:48 +0200 | |
changeset 45129 | 1fce03e3e8ad |
parent 44512 | 5e0f9e0e32fb |
child 45343 | 873e9c0ca37d |
permissions | -rw-r--r-- |
36524
3909002beca5
Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36465
diff
changeset
|
1 |
(* Title: HOL/Quotient_Examples/FSet.thy |
36465 | 2 |
Author: Cezary Kaliszyk, TU Munich |
3 |
Author: Christian Urban, TU Munich |
|
36280 | 4 |
|
41467 | 5 |
Type of finite sets. |
36280 | 6 |
*) |
36465 | 7 |
|
36280 | 8 |
theory FSet |
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
41071
diff
changeset
|
9 |
imports "~~/src/HOL/Library/Quotient_List" "~~/src/HOL/Library/More_List" |
36280 | 10 |
begin |
11 |
||
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
12 |
text {* |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
13 |
The type of finite sets is created by a quotient construction |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
14 |
over lists. The definition of the equivalence: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
15 |
*} |
36280 | 16 |
|
40467
dc0439fdd7c5
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
40034
diff
changeset
|
17 |
definition |
36280 | 18 |
list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50) |
19 |
where |
|
40952 | 20 |
[simp]: "xs \<approx> ys \<longleftrightarrow> set xs = set ys" |
36280 | 21 |
|
40822 | 22 |
lemma list_eq_reflp: |
23 |
"reflp list_eq" |
|
24 |
by (auto intro: reflpI) |
|
25 |
||
26 |
lemma list_eq_symp: |
|
27 |
"symp list_eq" |
|
28 |
by (auto intro: sympI) |
|
29 |
||
30 |
lemma list_eq_transp: |
|
31 |
"transp list_eq" |
|
32 |
by (auto intro: transpI) |
|
33 |
||
36280 | 34 |
lemma list_eq_equivp: |
40822 | 35 |
"equivp list_eq" |
36 |
by (auto intro: equivpI list_eq_reflp list_eq_symp list_eq_transp) |
|
36280 | 37 |
|
40688
a961ec75fc29
corrected abd4e7358847 where SOMEthing went utterly wrong
haftmann
parents:
40672
diff
changeset
|
38 |
text {* The @{text fset} type *} |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
39 |
|
36280 | 40 |
quotient_type |
41 |
'a fset = "'a list" / "list_eq" |
|
42 |
by (rule list_eq_equivp) |
|
43 |
||
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
44 |
text {* |
40953 | 45 |
Definitions for sublist, cardinality, |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
46 |
intersection, difference and respectful fold over |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
47 |
lists. |
39994
7bd8013b903f
FSet: give names to respectfulness theorems, rename list_all2_refl to avoid clash
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
48 |
*} |
36280 | 49 |
|
40953 | 50 |
declare List.member_def [simp] |
36280 | 51 |
|
40034 | 52 |
definition |
36280 | 53 |
sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
54 |
where |
40034 | 55 |
[simp]: "sub_list xs ys \<longleftrightarrow> set xs \<subseteq> set ys" |
36280 | 56 |
|
40034 | 57 |
definition |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
58 |
card_list :: "'a list \<Rightarrow> nat" |
36280 | 59 |
where |
40034 | 60 |
[simp]: "card_list xs = card (set xs)" |
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
61 |
|
40034 | 62 |
definition |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
63 |
inter_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
64 |
where |
40034 | 65 |
[simp]: "inter_list xs ys = [x \<leftarrow> xs. x \<in> set xs \<and> x \<in> set ys]" |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
66 |
|
40034 | 67 |
definition |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
68 |
diff_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
69 |
where |
40034 | 70 |
[simp]: "diff_list xs ys = [x \<leftarrow> xs. x \<notin> set ys]" |
36280 | 71 |
|
72 |
definition |
|
40954
ecca598474dd
conventional point-free characterization of rsp_fold
haftmann
parents:
40953
diff
changeset
|
73 |
rsp_fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool" |
36280 | 74 |
where |
40954
ecca598474dd
conventional point-free characterization of rsp_fold
haftmann
parents:
40953
diff
changeset
|
75 |
"rsp_fold f \<longleftrightarrow> (\<forall>u v. f u \<circ> f v = f v \<circ> f u)" |
36280 | 76 |
|
40961 | 77 |
lemma rsp_foldI: |
78 |
"(\<And>u v. f u \<circ> f v = f v \<circ> f u) \<Longrightarrow> rsp_fold f" |
|
79 |
by (simp add: rsp_fold_def) |
|
80 |
||
81 |
lemma rsp_foldE: |
|
82 |
assumes "rsp_fold f" |
|
83 |
obtains "f u \<circ> f v = f v \<circ> f u" |
|
84 |
using assms by (simp add: rsp_fold_def) |
|
85 |
||
40962
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
86 |
definition |
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
87 |
fold_once :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" |
36280 | 88 |
where |
40962
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
89 |
"fold_once f xs = (if rsp_fold f then fold f (remdups xs) else id)" |
36280 | 90 |
|
40962
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
91 |
lemma fold_once_default [simp]: |
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
92 |
"\<not> rsp_fold f \<Longrightarrow> fold_once f xs = id" |
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
93 |
by (simp add: fold_once_def) |
40961 | 94 |
|
40962
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
95 |
lemma fold_once_fold_remdups: |
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
96 |
"rsp_fold f \<Longrightarrow> fold_once f xs = fold f (remdups xs)" |
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
97 |
by (simp add: fold_once_def) |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
98 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
99 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
100 |
section {* Quotient composition lemmas *} |
36280 | 101 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
102 |
lemma list_all2_refl': |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
103 |
assumes q: "equivp R" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
104 |
shows "(list_all2 R) r r" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
105 |
by (rule list_all2_refl) (metis equivp_def q) |
36280 | 106 |
|
107 |
lemma compose_list_refl: |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
108 |
assumes q: "equivp R" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
109 |
shows "(list_all2 R OOO op \<approx>) r r" |
36280 | 110 |
proof |
36465 | 111 |
have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp]) |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
112 |
show "list_all2 R r r" by (rule list_all2_refl'[OF q]) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
113 |
with * show "(op \<approx> OO list_all2 R) r r" .. |
36280 | 114 |
qed |
115 |
||
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
116 |
lemma map_list_eq_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba" |
40467
dc0439fdd7c5
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
40034
diff
changeset
|
117 |
by (simp only: list_eq_def set_map) |
36280 | 118 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
119 |
lemma quotient_compose_list_g: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
120 |
assumes q: "Quotient R Abs Rep" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
121 |
and e: "equivp R" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
122 |
shows "Quotient ((list_all2 R) OOO (op \<approx>)) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
123 |
(abs_fset \<circ> (map Abs)) ((map Rep) \<circ> rep_fset)" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
124 |
unfolding Quotient_def comp_def |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
125 |
proof (intro conjI allI) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
126 |
fix a r s |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
127 |
show "abs_fset (map Abs (map Rep (rep_fset a))) = a" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
128 |
by (simp add: abs_o_rep[OF q] Quotient_abs_rep[OF Quotient_fset] map_id) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
129 |
have b: "list_all2 R (map Rep (rep_fset a)) (map Rep (rep_fset a))" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
130 |
by (rule list_all2_refl'[OF e]) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
131 |
have c: "(op \<approx> OO list_all2 R) (map Rep (rep_fset a)) (map Rep (rep_fset a))" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
132 |
by (rule, rule equivp_reflp[OF fset_equivp]) (rule b) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
133 |
show "(list_all2 R OOO op \<approx>) (map Rep (rep_fset a)) (map Rep (rep_fset a))" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
134 |
by (rule, rule list_all2_refl'[OF e]) (rule c) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
135 |
show "(list_all2 R OOO op \<approx>) r s = ((list_all2 R OOO op \<approx>) r r \<and> |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
136 |
(list_all2 R OOO op \<approx>) s s \<and> abs_fset (map Abs r) = abs_fset (map Abs s))" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
137 |
proof (intro iffI conjI) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
138 |
show "(list_all2 R OOO op \<approx>) r r" by (rule compose_list_refl[OF e]) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
139 |
show "(list_all2 R OOO op \<approx>) s s" by (rule compose_list_refl[OF e]) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
140 |
next |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
141 |
assume a: "(list_all2 R OOO op \<approx>) r s" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
142 |
then have b: "map Abs r \<approx> map Abs s" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
143 |
proof (elim pred_compE) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
144 |
fix b ba |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
145 |
assume c: "list_all2 R r b" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
146 |
assume d: "b \<approx> ba" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
147 |
assume e: "list_all2 R ba s" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
148 |
have f: "map Abs r = map Abs b" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
149 |
using Quotient_rel[OF list_quotient[OF q]] c by blast |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
150 |
have "map Abs ba = map Abs s" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
151 |
using Quotient_rel[OF list_quotient[OF q]] e by blast |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
152 |
then have g: "map Abs s = map Abs ba" by simp |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
153 |
then show "map Abs r \<approx> map Abs s" using d f map_list_eq_cong by simp |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
154 |
qed |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
155 |
then show "abs_fset (map Abs r) = abs_fset (map Abs s)" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
156 |
using Quotient_rel[OF Quotient_fset] by blast |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
157 |
next |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
158 |
assume a: "(list_all2 R OOO op \<approx>) r r \<and> (list_all2 R OOO op \<approx>) s s |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
159 |
\<and> abs_fset (map Abs r) = abs_fset (map Abs s)" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
160 |
then have s: "(list_all2 R OOO op \<approx>) s s" by simp |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
161 |
have d: "map Abs r \<approx> map Abs s" |
40822 | 162 |
by (subst Quotient_rel [OF Quotient_fset, symmetric]) (simp add: a) |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
163 |
have b: "map Rep (map Abs r) \<approx> map Rep (map Abs s)" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
164 |
by (rule map_list_eq_cong[OF d]) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
165 |
have y: "list_all2 R (map Rep (map Abs s)) s" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
166 |
by (fact rep_abs_rsp_left[OF list_quotient[OF q], OF list_all2_refl'[OF e, of s]]) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
167 |
have c: "(op \<approx> OO list_all2 R) (map Rep (map Abs r)) s" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
168 |
by (rule pred_compI) (rule b, rule y) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
169 |
have z: "list_all2 R r (map Rep (map Abs r))" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
170 |
by (fact rep_abs_rsp[OF list_quotient[OF q], OF list_all2_refl'[OF e, of r]]) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
171 |
then show "(list_all2 R OOO op \<approx>) r s" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
172 |
using a c pred_compI by simp |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
173 |
qed |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
174 |
qed |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
175 |
|
36280 | 176 |
lemma quotient_compose_list[quot_thm]: |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
177 |
shows "Quotient ((list_all2 op \<approx>) OOO (op \<approx>)) |
36280 | 178 |
(abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)" |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
179 |
by (rule quotient_compose_list_g, rule Quotient_fset, rule list_eq_equivp) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
180 |
|
36280 | 181 |
|
39996
c02078ff8691
FSet: definition changes propagated from Nominal and more use of 'descending' tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39995
diff
changeset
|
182 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
183 |
subsection {* Respectfulness lemmas for list operations *} |
39996
c02078ff8691
FSet: definition changes propagated from Nominal and more use of 'descending' tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39995
diff
changeset
|
184 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
185 |
lemma list_equiv_rsp [quot_respect]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
186 |
shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>" |
40467
dc0439fdd7c5
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
40034
diff
changeset
|
187 |
by (auto intro!: fun_relI) |
39996
c02078ff8691
FSet: definition changes propagated from Nominal and more use of 'descending' tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39995
diff
changeset
|
188 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
189 |
lemma append_rsp [quot_respect]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
190 |
shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append" |
40467
dc0439fdd7c5
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
40034
diff
changeset
|
191 |
by (auto intro!: fun_relI) |
36280 | 192 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
193 |
lemma sub_list_rsp [quot_respect]: |
36280 | 194 |
shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list" |
40467
dc0439fdd7c5
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
40034
diff
changeset
|
195 |
by (auto intro!: fun_relI) |
36280 | 196 |
|
40953 | 197 |
lemma member_rsp [quot_respect]: |
198 |
shows "(op \<approx> ===> op =) List.member List.member" |
|
44512
5e0f9e0e32fb
FSet: Explicit proof without mem_def
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
44204
diff
changeset
|
199 |
proof |
5e0f9e0e32fb
FSet: Explicit proof without mem_def
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
44204
diff
changeset
|
200 |
fix x y assume "x \<approx> y" |
5e0f9e0e32fb
FSet: Explicit proof without mem_def
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
44204
diff
changeset
|
201 |
then show "List.member x = List.member y" |
5e0f9e0e32fb
FSet: Explicit proof without mem_def
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
44204
diff
changeset
|
202 |
unfolding fun_eq_iff by simp |
5e0f9e0e32fb
FSet: Explicit proof without mem_def
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
44204
diff
changeset
|
203 |
qed |
36280 | 204 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
205 |
lemma nil_rsp [quot_respect]: |
39994
7bd8013b903f
FSet: give names to respectfulness theorems, rename list_all2_refl to avoid clash
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
206 |
shows "(op \<approx>) Nil Nil" |
36280 | 207 |
by simp |
208 |
||
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
209 |
lemma cons_rsp [quot_respect]: |
39994
7bd8013b903f
FSet: give names to respectfulness theorems, rename list_all2_refl to avoid clash
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
210 |
shows "(op = ===> op \<approx> ===> op \<approx>) Cons Cons" |
40467
dc0439fdd7c5
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
40034
diff
changeset
|
211 |
by (auto intro!: fun_relI) |
36280 | 212 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
213 |
lemma map_rsp [quot_respect]: |
36280 | 214 |
shows "(op = ===> op \<approx> ===> op \<approx>) map map" |
40467
dc0439fdd7c5
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
40034
diff
changeset
|
215 |
by (auto intro!: fun_relI) |
36280 | 216 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
217 |
lemma set_rsp [quot_respect]: |
36280 | 218 |
"(op \<approx> ===> op =) set set" |
40467
dc0439fdd7c5
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
40034
diff
changeset
|
219 |
by (auto intro!: fun_relI) |
36280 | 220 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
221 |
lemma inter_list_rsp [quot_respect]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
222 |
shows "(op \<approx> ===> op \<approx> ===> op \<approx>) inter_list inter_list" |
40467
dc0439fdd7c5
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
40034
diff
changeset
|
223 |
by (auto intro!: fun_relI) |
39996
c02078ff8691
FSet: definition changes propagated from Nominal and more use of 'descending' tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39995
diff
changeset
|
224 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
225 |
lemma removeAll_rsp [quot_respect]: |
39996
c02078ff8691
FSet: definition changes propagated from Nominal and more use of 'descending' tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39995
diff
changeset
|
226 |
shows "(op = ===> op \<approx> ===> op \<approx>) removeAll removeAll" |
40467
dc0439fdd7c5
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
40034
diff
changeset
|
227 |
by (auto intro!: fun_relI) |
39996
c02078ff8691
FSet: definition changes propagated from Nominal and more use of 'descending' tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39995
diff
changeset
|
228 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
229 |
lemma diff_list_rsp [quot_respect]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
230 |
shows "(op \<approx> ===> op \<approx> ===> op \<approx>) diff_list diff_list" |
40467
dc0439fdd7c5
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
40034
diff
changeset
|
231 |
by (auto intro!: fun_relI) |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
232 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
233 |
lemma card_list_rsp [quot_respect]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
234 |
shows "(op \<approx> ===> op =) card_list card_list" |
40467
dc0439fdd7c5
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
40034
diff
changeset
|
235 |
by (auto intro!: fun_relI) |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
236 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
237 |
lemma filter_rsp [quot_respect]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
238 |
shows "(op = ===> op \<approx> ===> op \<approx>) filter filter" |
40467
dc0439fdd7c5
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
40034
diff
changeset
|
239 |
by (auto intro!: fun_relI) |
39996
c02078ff8691
FSet: definition changes propagated from Nominal and more use of 'descending' tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39995
diff
changeset
|
240 |
|
40962
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
241 |
lemma remdups_removeAll: (*FIXME move*) |
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
242 |
"remdups (removeAll x xs) = remove1 x (remdups xs)" |
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
243 |
by (induct xs) auto |
36280 | 244 |
|
40962
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
245 |
lemma member_commute_fold_once: |
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
246 |
assumes "rsp_fold f" |
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
247 |
and "x \<in> set xs" |
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
248 |
shows "fold_once f xs = fold_once f (removeAll x xs) \<circ> f x" |
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
249 |
proof - |
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
250 |
from assms have "More_List.fold f (remdups xs) = More_List.fold f (remove1 x (remdups xs)) \<circ> f x" |
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
251 |
by (auto intro!: fold_remove1_split elim: rsp_foldE) |
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
252 |
then show ?thesis using `rsp_fold f` by (simp add: fold_once_fold_remdups remdups_removeAll) |
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
253 |
qed |
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
254 |
|
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
255 |
lemma fold_once_set_equiv: |
40961 | 256 |
assumes "xs \<approx> ys" |
40962
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
257 |
shows "fold_once f xs = fold_once f ys" |
40961 | 258 |
proof (cases "rsp_fold f") |
259 |
case False then show ?thesis by simp |
|
260 |
next |
|
261 |
case True |
|
262 |
then have "\<And>x y. x \<in> set (remdups xs) \<Longrightarrow> y \<in> set (remdups xs) \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" |
|
263 |
by (rule rsp_foldE) |
|
264 |
moreover from assms have "multiset_of (remdups xs) = multiset_of (remdups ys)" |
|
265 |
by (simp add: set_eq_iff_multiset_of_remdups_eq) |
|
266 |
ultimately have "fold f (remdups xs) = fold f (remdups ys)" |
|
267 |
by (rule fold_multiset_equiv) |
|
40962
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
268 |
with True show ?thesis by (simp add: fold_once_fold_remdups) |
40961 | 269 |
qed |
36280 | 270 |
|
40962
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
271 |
lemma fold_once_rsp [quot_respect]: |
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
272 |
shows "(op = ===> op \<approx> ===> op =) fold_once fold_once" |
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
273 |
unfolding fun_rel_def by (auto intro: fold_once_set_equiv) |
36280 | 274 |
|
275 |
lemma concat_rsp_pre: |
|
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
276 |
assumes a: "list_all2 op \<approx> x x'" |
36280 | 277 |
and b: "x' \<approx> y'" |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
278 |
and c: "list_all2 op \<approx> y' y" |
36280 | 279 |
and d: "\<exists>x\<in>set x. xa \<in> set x" |
280 |
shows "\<exists>x\<in>set y. xa \<in> set x" |
|
281 |
proof - |
|
282 |
obtain xb where e: "xb \<in> set x" and f: "xa \<in> set xb" using d by auto |
|
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
283 |
have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_all2_find_element[OF e a]) |
36280 | 284 |
then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto |
36465 | 285 |
have "ya \<in> set y'" using b h by simp |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
286 |
then have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" using c by (rule list_all2_find_element) |
36280 | 287 |
then show ?thesis using f i by auto |
288 |
qed |
|
289 |
||
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
290 |
lemma concat_rsp [quot_respect]: |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
291 |
shows "(list_all2 op \<approx> OOO op \<approx> ===> op \<approx>) concat concat" |
36280 | 292 |
proof (rule fun_relI, elim pred_compE) |
293 |
fix a b ba bb |
|
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
294 |
assume a: "list_all2 op \<approx> a ba" |
40822 | 295 |
with list_symp [OF list_eq_symp] have a': "list_all2 op \<approx> ba a" by (rule sympE) |
36280 | 296 |
assume b: "ba \<approx> bb" |
40822 | 297 |
with list_eq_symp have b': "bb \<approx> ba" by (rule sympE) |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
298 |
assume c: "list_all2 op \<approx> bb b" |
40822 | 299 |
with list_symp [OF list_eq_symp] have c': "list_all2 op \<approx> b bb" by (rule sympE) |
39996
c02078ff8691
FSet: definition changes propagated from Nominal and more use of 'descending' tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39995
diff
changeset
|
300 |
have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" |
c02078ff8691
FSet: definition changes propagated from Nominal and more use of 'descending' tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39995
diff
changeset
|
301 |
proof |
36280 | 302 |
fix x |
39996
c02078ff8691
FSet: definition changes propagated from Nominal and more use of 'descending' tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39995
diff
changeset
|
303 |
show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" |
c02078ff8691
FSet: definition changes propagated from Nominal and more use of 'descending' tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39995
diff
changeset
|
304 |
proof |
36280 | 305 |
assume d: "\<exists>xa\<in>set a. x \<in> set xa" |
306 |
show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d]) |
|
307 |
next |
|
308 |
assume e: "\<exists>xa\<in>set b. x \<in> set xa" |
|
309 |
show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e]) |
|
310 |
qed |
|
311 |
qed |
|
39996
c02078ff8691
FSet: definition changes propagated from Nominal and more use of 'descending' tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39995
diff
changeset
|
312 |
then show "concat a \<approx> concat b" by auto |
36280 | 313 |
qed |
314 |
||
36639
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
315 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
316 |
section {* Quotient definitions for fsets *} |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
317 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
318 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
319 |
subsection {* Finite sets are a bounded, distributive lattice with minus *} |
36280 | 320 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
321 |
instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}" |
36280 | 322 |
begin |
323 |
||
324 |
quotient_definition |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
325 |
"bot :: 'a fset" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
326 |
is "Nil :: 'a list" |
36280 | 327 |
|
328 |
abbreviation |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
329 |
empty_fset ("{||}") |
36280 | 330 |
where |
331 |
"{||} \<equiv> bot :: 'a fset" |
|
332 |
||
333 |
quotient_definition |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
334 |
"less_eq_fset :: ('a fset \<Rightarrow> 'a fset \<Rightarrow> bool)" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
335 |
is "sub_list :: ('a list \<Rightarrow> 'a list \<Rightarrow> bool)" |
36280 | 336 |
|
337 |
abbreviation |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
338 |
subset_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subseteq>|" 50) |
36280 | 339 |
where |
340 |
"xs |\<subseteq>| ys \<equiv> xs \<le> ys" |
|
341 |
||
342 |
definition |
|
39995 | 343 |
less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" |
344 |
where |
|
345 |
"xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a fset)" |
|
36280 | 346 |
|
347 |
abbreviation |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
348 |
psubset_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subset>|" 50) |
36280 | 349 |
where |
350 |
"xs |\<subset>| ys \<equiv> xs < ys" |
|
351 |
||
352 |
quotient_definition |
|
39995 | 353 |
"sup :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
354 |
is "append :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
36280 | 355 |
|
356 |
abbreviation |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
357 |
union_fset (infixl "|\<union>|" 65) |
36280 | 358 |
where |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
359 |
"xs |\<union>| ys \<equiv> sup xs (ys::'a fset)" |
36280 | 360 |
|
361 |
quotient_definition |
|
39995 | 362 |
"inf :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
363 |
is "inter_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
36280 | 364 |
|
365 |
abbreviation |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
366 |
inter_fset (infixl "|\<inter>|" 65) |
36280 | 367 |
where |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
368 |
"xs |\<inter>| ys \<equiv> inf xs (ys::'a fset)" |
36280 | 369 |
|
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
370 |
quotient_definition |
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
371 |
"minus :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
372 |
is "diff_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
373 |
|
36280 | 374 |
instance |
375 |
proof |
|
376 |
fix x y z :: "'a fset" |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
377 |
show "x |\<subset>| y \<longleftrightarrow> x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x" |
40467
dc0439fdd7c5
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
40034
diff
changeset
|
378 |
by (unfold less_fset_def, descending) auto |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
379 |
show "x |\<subseteq>| x" by (descending) (simp) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
380 |
show "{||} |\<subseteq>| x" by (descending) (simp) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
381 |
show "x |\<subseteq>| x |\<union>| y" by (descending) (simp) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
382 |
show "y |\<subseteq>| x |\<union>| y" by (descending) (simp) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
383 |
show "x |\<inter>| y |\<subseteq>| x" by (descending) (auto) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
384 |
show "x |\<inter>| y |\<subseteq>| y" by (descending) (auto) |
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
385 |
show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)" |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
386 |
by (descending) (auto) |
36280 | 387 |
next |
388 |
fix x y z :: "'a fset" |
|
389 |
assume a: "x |\<subseteq>| y" |
|
390 |
assume b: "y |\<subseteq>| z" |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
391 |
show "x |\<subseteq>| z" using a b by (descending) (simp) |
36280 | 392 |
next |
393 |
fix x y :: "'a fset" |
|
394 |
assume a: "x |\<subseteq>| y" |
|
395 |
assume b: "y |\<subseteq>| x" |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
396 |
show "x = y" using a b by (descending) (auto) |
36280 | 397 |
next |
398 |
fix x y z :: "'a fset" |
|
399 |
assume a: "y |\<subseteq>| x" |
|
400 |
assume b: "z |\<subseteq>| x" |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
401 |
show "y |\<union>| z |\<subseteq>| x" using a b by (descending) (simp) |
36280 | 402 |
next |
403 |
fix x y z :: "'a fset" |
|
404 |
assume a: "x |\<subseteq>| y" |
|
405 |
assume b: "x |\<subseteq>| z" |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
406 |
show "x |\<subseteq>| y |\<inter>| z" using a b by (descending) (auto) |
36280 | 407 |
qed |
408 |
||
409 |
end |
|
410 |
||
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
411 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
412 |
subsection {* Other constants for fsets *} |
36280 | 413 |
|
414 |
quotient_definition |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
415 |
"insert_fset :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
416 |
is "Cons" |
36280 | 417 |
|
418 |
syntax |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
419 |
"@Insert_fset" :: "args => 'a fset" ("{|(_)|}") |
36280 | 420 |
|
421 |
translations |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
422 |
"{|x, xs|}" == "CONST insert_fset x {|xs|}" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
423 |
"{|x|}" == "CONST insert_fset x {||}" |
36280 | 424 |
|
425 |
quotient_definition |
|
40953 | 426 |
fset_member |
36280 | 427 |
where |
40953 | 428 |
"fset_member :: 'a fset \<Rightarrow> 'a \<Rightarrow> bool" is "List.member" |
429 |
||
430 |
abbreviation |
|
431 |
in_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) |
|
432 |
where |
|
433 |
"x |\<in>| S \<equiv> fset_member S x" |
|
36280 | 434 |
|
435 |
abbreviation |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
436 |
notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) |
36280 | 437 |
where |
438 |
"x |\<notin>| S \<equiv> \<not> (x |\<in>| S)" |
|
439 |
||
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
440 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
441 |
subsection {* Other constants on the Quotient Type *} |
36280 | 442 |
|
443 |
quotient_definition |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
444 |
"card_fset :: 'a fset \<Rightarrow> nat" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
445 |
is card_list |
36280 | 446 |
|
447 |
quotient_definition |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
448 |
"map_fset :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
449 |
is map |
36280 | 450 |
|
451 |
quotient_definition |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
452 |
"remove_fset :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
39996
c02078ff8691
FSet: definition changes propagated from Nominal and more use of 'descending' tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39995
diff
changeset
|
453 |
is removeAll |
36280 | 454 |
|
455 |
quotient_definition |
|
39996
c02078ff8691
FSet: definition changes propagated from Nominal and more use of 'descending' tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39995
diff
changeset
|
456 |
"fset :: 'a fset \<Rightarrow> 'a set" |
36280 | 457 |
is "set" |
458 |
||
459 |
quotient_definition |
|
40961 | 460 |
"fold_fset :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b \<Rightarrow> 'b" |
40962
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
461 |
is fold_once |
36280 | 462 |
|
463 |
quotient_definition |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
464 |
"concat_fset :: ('a fset) fset \<Rightarrow> 'a fset" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
465 |
is concat |
36280 | 466 |
|
36639
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
467 |
quotient_definition |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
468 |
"filter_fset :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
469 |
is filter |
36639
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
470 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
471 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
472 |
subsection {* Compositional respectfulness and preservation lemmas *} |
36280 | 473 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
474 |
lemma Nil_rsp2 [quot_respect]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
475 |
shows "(list_all2 op \<approx> OOO op \<approx>) Nil Nil" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
476 |
by (rule compose_list_refl, rule list_eq_equivp) |
36280 | 477 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
478 |
lemma Cons_rsp2 [quot_respect]: |
39994
7bd8013b903f
FSet: give names to respectfulness theorems, rename list_all2_refl to avoid clash
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset
|
479 |
shows "(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) Cons Cons" |
40467
dc0439fdd7c5
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
40034
diff
changeset
|
480 |
apply (auto intro!: fun_relI) |
36280 | 481 |
apply (rule_tac b="x # b" in pred_compI) |
482 |
apply auto |
|
483 |
apply (rule_tac b="x # ba" in pred_compI) |
|
484 |
apply auto |
|
485 |
done |
|
486 |
||
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
487 |
lemma map_prs [quot_preserve]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
488 |
shows "(abs_fset \<circ> map f) [] = abs_fset []" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
489 |
by simp |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
490 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
491 |
lemma insert_fset_rsp [quot_preserve]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
492 |
"(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) Cons = insert_fset" |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
493 |
by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset] |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
494 |
abs_o_rep[OF Quotient_fset] map_id insert_fset_def) |
36280 | 495 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
496 |
lemma union_fset_rsp [quot_preserve]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
497 |
"((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
498 |
append = union_fset" |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
499 |
by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset] |
36280 | 500 |
abs_o_rep[OF Quotient_fset] map_id sup_fset_def) |
501 |
||
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
502 |
lemma list_all2_app_l: |
36280 | 503 |
assumes a: "reflp R" |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
504 |
and b: "list_all2 R l r" |
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
505 |
shows "list_all2 R (z @ l) (z @ r)" |
40822 | 506 |
using a b by (induct z) (auto elim: reflpE) |
36280 | 507 |
|
508 |
lemma append_rsp2_pre0: |
|
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
509 |
assumes a:"list_all2 op \<approx> x x'" |
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
510 |
shows "list_all2 op \<approx> (x @ z) (x' @ z)" |
36280 | 511 |
using a apply (induct x x' rule: list_induct2') |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
512 |
by simp_all (rule list_all2_refl'[OF list_eq_equivp]) |
36280 | 513 |
|
514 |
lemma append_rsp2_pre1: |
|
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
515 |
assumes a:"list_all2 op \<approx> x x'" |
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
516 |
shows "list_all2 op \<approx> (z @ x) (z @ x')" |
36280 | 517 |
using a apply (induct x x' arbitrary: z rule: list_induct2') |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
518 |
apply (rule list_all2_refl'[OF list_eq_equivp]) |
40467
dc0439fdd7c5
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
40034
diff
changeset
|
519 |
apply (simp_all del: list_eq_def) |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
520 |
apply (rule list_all2_app_l) |
40822 | 521 |
apply (simp_all add: reflpI) |
36280 | 522 |
done |
523 |
||
524 |
lemma append_rsp2_pre: |
|
40822 | 525 |
assumes "list_all2 op \<approx> x x'" |
526 |
and "list_all2 op \<approx> z z'" |
|
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
527 |
shows "list_all2 op \<approx> (x @ z) (x' @ z')" |
40822 | 528 |
using assms by (rule list_all2_appendI) |
36280 | 529 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
530 |
lemma append_rsp2 [quot_respect]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
531 |
"(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append" |
36280 | 532 |
proof (intro fun_relI, elim pred_compE) |
533 |
fix x y z w x' z' y' w' :: "'a list list" |
|
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
534 |
assume a:"list_all2 op \<approx> x x'" |
36280 | 535 |
and b: "x' \<approx> y'" |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
536 |
and c: "list_all2 op \<approx> y' y" |
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
537 |
assume aa: "list_all2 op \<approx> z z'" |
36280 | 538 |
and bb: "z' \<approx> w'" |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
539 |
and cc: "list_all2 op \<approx> w' w" |
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
540 |
have a': "list_all2 op \<approx> (x @ z) (x' @ z')" using a aa append_rsp2_pre by auto |
36280 | 541 |
have b': "x' @ z' \<approx> y' @ w'" using b bb by simp |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
542 |
have c': "list_all2 op \<approx> (y' @ w') (y @ w)" using c cc append_rsp2_pre by auto |
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
543 |
have d': "(op \<approx> OO list_all2 op \<approx>) (x' @ z') (y @ w)" |
36280 | 544 |
by (rule pred_compI) (rule b', rule c') |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
545 |
show "(list_all2 op \<approx> OOO op \<approx>) (x @ z) (y @ w)" |
36280 | 546 |
by (rule pred_compI) (rule a', rule d') |
547 |
qed |
|
548 |
||
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
549 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
550 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
551 |
section {* Lifted theorems *} |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
552 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
553 |
subsection {* fset *} |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
554 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
555 |
lemma fset_simps [simp]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
556 |
shows "fset {||} = {}" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
557 |
and "fset (insert_fset x S) = insert x (fset S)" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
558 |
by (descending, simp)+ |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
559 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
560 |
lemma finite_fset [simp]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
561 |
shows "finite (fset S)" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
562 |
by (descending) (simp) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
563 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
564 |
lemma fset_cong: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
565 |
shows "fset S = fset T \<longleftrightarrow> S = T" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
566 |
by (descending) (simp) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
567 |
|
44204
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
41467
diff
changeset
|
568 |
lemma filter_fset [simp]: |
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
41467
diff
changeset
|
569 |
shows "fset (filter_fset P xs) = Collect P \<inter> fset xs" |
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
41467
diff
changeset
|
570 |
by (descending) (auto) |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
571 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
572 |
lemma remove_fset [simp]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
573 |
shows "fset (remove_fset x xs) = fset xs - {x}" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
574 |
by (descending) (simp) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
575 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
576 |
lemma inter_fset [simp]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
577 |
shows "fset (xs |\<inter>| ys) = fset xs \<inter> fset ys" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
578 |
by (descending) (auto) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
579 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
580 |
lemma union_fset [simp]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
581 |
shows "fset (xs |\<union>| ys) = fset xs \<union> fset ys" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
582 |
by (lifting set_append) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
583 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
584 |
lemma minus_fset [simp]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
585 |
shows "fset (xs - ys) = fset xs - fset ys" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
586 |
by (descending) (auto) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
587 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
588 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
589 |
subsection {* in_fset *} |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
590 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
591 |
lemma in_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
592 |
shows "x |\<in>| S \<longleftrightarrow> x \<in> fset S" |
40953 | 593 |
by descending simp |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
594 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
595 |
lemma notin_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
596 |
shows "x |\<notin>| S \<longleftrightarrow> x \<notin> fset S" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
597 |
by (simp add: in_fset) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
598 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
599 |
lemma notin_empty_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
600 |
shows "x |\<notin>| {||}" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
601 |
by (simp add: in_fset) |
36280 | 602 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
603 |
lemma fset_eq_iff: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
604 |
shows "S = T \<longleftrightarrow> (\<forall>x. (x |\<in>| S) = (x |\<in>| T))" |
40953 | 605 |
by descending auto |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
606 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
607 |
lemma none_in_empty_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
608 |
shows "(\<forall>x. x |\<notin>| S) \<longleftrightarrow> S = {||}" |
40953 | 609 |
by descending simp |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
610 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
611 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
612 |
subsection {* insert_fset *} |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
613 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
614 |
lemma in_insert_fset_iff [simp]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
615 |
shows "x |\<in>| insert_fset y S \<longleftrightarrow> x = y \<or> x |\<in>| S" |
40953 | 616 |
by descending simp |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
617 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
618 |
lemma |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
619 |
shows insert_fsetI1: "x |\<in>| insert_fset x S" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
620 |
and insert_fsetI2: "x |\<in>| S \<Longrightarrow> x |\<in>| insert_fset y S" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
621 |
by simp_all |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
622 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
623 |
lemma insert_absorb_fset [simp]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
624 |
shows "x |\<in>| S \<Longrightarrow> insert_fset x S = S" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
625 |
by (descending) (auto) |
36280 | 626 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
627 |
lemma empty_not_insert_fset[simp]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
628 |
shows "{||} \<noteq> insert_fset x S" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
629 |
and "insert_fset x S \<noteq> {||}" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
630 |
by (descending, simp)+ |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
631 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
632 |
lemma insert_fset_left_comm: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
633 |
shows "insert_fset x (insert_fset y S) = insert_fset y (insert_fset x S)" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
634 |
by (descending) (auto) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
635 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
636 |
lemma insert_fset_left_idem: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
637 |
shows "insert_fset x (insert_fset x S) = insert_fset x S" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
638 |
by (descending) (auto) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
639 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
640 |
lemma singleton_fset_eq[simp]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
641 |
shows "{|x|} = {|y|} \<longleftrightarrow> x = y" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
642 |
by (descending) (auto) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
643 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
644 |
lemma in_fset_mdef: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
645 |
shows "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = insert_fset x (F - {|x|})" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
646 |
by (descending) (auto) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
647 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
648 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
649 |
subsection {* union_fset *} |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
650 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
651 |
lemmas [simp] = |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
652 |
sup_bot_left[where 'a="'a fset", standard] |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
653 |
sup_bot_right[where 'a="'a fset", standard] |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
654 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
655 |
lemma union_insert_fset [simp]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
656 |
shows "insert_fset x S |\<union>| T = insert_fset x (S |\<union>| T)" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
657 |
by (lifting append.simps(2)) |
36280 | 658 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
659 |
lemma singleton_union_fset_left: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
660 |
shows "{|a|} |\<union>| S = insert_fset a S" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
661 |
by simp |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
662 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
663 |
lemma singleton_union_fset_right: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
664 |
shows "S |\<union>| {|a|} = insert_fset a S" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
665 |
by (subst sup.commute) simp |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
666 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
667 |
lemma in_union_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
668 |
shows "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
669 |
by (descending) (simp) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
670 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
671 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
672 |
subsection {* minus_fset *} |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
673 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
674 |
lemma minus_in_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
675 |
shows "x |\<in>| (xs - ys) \<longleftrightarrow> x |\<in>| xs \<and> x |\<notin>| ys" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
676 |
by (descending) (simp) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
677 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
678 |
lemma minus_insert_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
679 |
shows "insert_fset x xs - ys = (if x |\<in>| ys then xs - ys else insert_fset x (xs - ys))" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
680 |
by (descending) (auto) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
681 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
682 |
lemma minus_insert_in_fset[simp]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
683 |
shows "x |\<in>| ys \<Longrightarrow> insert_fset x xs - ys = xs - ys" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
684 |
by (simp add: minus_insert_fset) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
685 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
686 |
lemma minus_insert_notin_fset[simp]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
687 |
shows "x |\<notin>| ys \<Longrightarrow> insert_fset x xs - ys = insert_fset x (xs - ys)" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
688 |
by (simp add: minus_insert_fset) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
689 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
690 |
lemma in_minus_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
691 |
shows "x |\<in>| F - S \<Longrightarrow> x |\<notin>| S" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
692 |
unfolding in_fset minus_fset |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
693 |
by blast |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
694 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
695 |
lemma notin_minus_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
696 |
shows "x |\<in>| S \<Longrightarrow> x |\<notin>| F - S" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
697 |
unfolding in_fset minus_fset |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
698 |
by blast |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
699 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
700 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
701 |
subsection {* remove_fset *} |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
702 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
703 |
lemma in_remove_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
704 |
shows "x |\<in>| remove_fset y S \<longleftrightarrow> x |\<in>| S \<and> x \<noteq> y" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
705 |
by (descending) (simp) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
706 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
707 |
lemma notin_remove_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
708 |
shows "x |\<notin>| remove_fset x S" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
709 |
by (descending) (simp) |
36280 | 710 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
711 |
lemma notin_remove_ident_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
712 |
shows "x |\<notin>| S \<Longrightarrow> remove_fset x S = S" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
713 |
by (descending) (simp) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
714 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
715 |
lemma remove_fset_cases: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
716 |
shows "S = {||} \<or> (\<exists>x. x |\<in>| S \<and> S = insert_fset x (remove_fset x S))" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
717 |
by (descending) (auto simp add: insert_absorb) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
718 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
719 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
720 |
subsection {* inter_fset *} |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
721 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
722 |
lemma inter_empty_fset_l: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
723 |
shows "{||} |\<inter>| S = {||}" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
724 |
by simp |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
725 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
726 |
lemma inter_empty_fset_r: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
727 |
shows "S |\<inter>| {||} = {||}" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
728 |
by simp |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
729 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
730 |
lemma inter_insert_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
731 |
shows "insert_fset x S |\<inter>| T = (if x |\<in>| T then insert_fset x (S |\<inter>| T) else S |\<inter>| T)" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
732 |
by (descending) (auto) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
733 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
734 |
lemma in_inter_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
735 |
shows "x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
736 |
by (descending) (simp) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
737 |
|
36280 | 738 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
739 |
subsection {* subset_fset and psubset_fset *} |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
740 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
741 |
lemma subset_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
742 |
shows "xs |\<subseteq>| ys \<longleftrightarrow> fset xs \<subseteq> fset ys" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
743 |
by (descending) (simp) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
744 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
745 |
lemma psubset_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
746 |
shows "xs |\<subset>| ys \<longleftrightarrow> fset xs \<subset> fset ys" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
747 |
unfolding less_fset_def |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
748 |
by (descending) (auto) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
749 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
750 |
lemma subset_insert_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
751 |
shows "(insert_fset x xs) |\<subseteq>| ys \<longleftrightarrow> x |\<in>| ys \<and> xs |\<subseteq>| ys" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
752 |
by (descending) (simp) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
753 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
754 |
lemma subset_in_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
755 |
shows "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
756 |
by (descending) (auto) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
757 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
758 |
lemma subset_empty_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
759 |
shows "xs |\<subseteq>| {||} \<longleftrightarrow> xs = {||}" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
760 |
by (descending) (simp) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
761 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
762 |
lemma not_psubset_empty_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
763 |
shows "\<not> xs |\<subset>| {||}" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
764 |
by (metis fset_simps(1) psubset_fset not_psubset_empty) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
765 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
766 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
767 |
subsection {* map_fset *} |
36280 | 768 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
769 |
lemma map_fset_simps [simp]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
770 |
shows "map_fset f {||} = {||}" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
771 |
and "map_fset f (insert_fset x S) = insert_fset (f x) (map_fset f S)" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
772 |
by (descending, simp)+ |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
773 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
774 |
lemma map_fset_image [simp]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
775 |
shows "fset (map_fset f S) = f ` (fset S)" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
776 |
by (descending) (simp) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
777 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
778 |
lemma inj_map_fset_cong: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
779 |
shows "inj f \<Longrightarrow> map_fset f S = map_fset f T \<longleftrightarrow> S = T" |
40467
dc0439fdd7c5
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
40034
diff
changeset
|
780 |
by (descending) (metis inj_vimage_image_eq list_eq_def set_map) |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
781 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
782 |
lemma map_union_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
783 |
shows "map_fset f (S |\<union>| T) = map_fset f S |\<union>| map_fset f T" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
784 |
by (descending) (simp) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
785 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
786 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
787 |
subsection {* card_fset *} |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
788 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
789 |
lemma card_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
790 |
shows "card_fset xs = card (fset xs)" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
791 |
by (descending) (simp) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
792 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
793 |
lemma card_insert_fset_iff [simp]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
794 |
shows "card_fset (insert_fset x S) = (if x |\<in>| S then card_fset S else Suc (card_fset S))" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
795 |
by (descending) (simp add: insert_absorb) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
796 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
797 |
lemma card_fset_0[simp]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
798 |
shows "card_fset S = 0 \<longleftrightarrow> S = {||}" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
799 |
by (descending) (simp) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
800 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
801 |
lemma card_empty_fset[simp]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
802 |
shows "card_fset {||} = 0" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
803 |
by (simp add: card_fset) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
804 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
805 |
lemma card_fset_1: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
806 |
shows "card_fset S = 1 \<longleftrightarrow> (\<exists>x. S = {|x|})" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
807 |
by (descending) (auto simp add: card_Suc_eq) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
808 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
809 |
lemma card_fset_gt_0: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
810 |
shows "x \<in> fset S \<Longrightarrow> 0 < card_fset S" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
811 |
by (descending) (auto simp add: card_gt_0_iff) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
812 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
813 |
lemma card_notin_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
814 |
shows "(x |\<notin>| S) = (card_fset (insert_fset x S) = Suc (card_fset S))" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
815 |
by simp |
36280 | 816 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
817 |
lemma card_fset_Suc: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
818 |
shows "card_fset S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = insert_fset x T \<and> card_fset T = n" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
819 |
apply(descending) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
820 |
apply(auto dest!: card_eq_SucD) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
821 |
by (metis Diff_insert_absorb set_removeAll) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
822 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
823 |
lemma card_remove_fset_iff [simp]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
824 |
shows "card_fset (remove_fset y S) = (if y |\<in>| S then card_fset S - 1 else card_fset S)" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
825 |
by (descending) (simp) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
826 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
827 |
lemma card_Suc_exists_in_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
828 |
shows "card_fset S = Suc n \<Longrightarrow> \<exists>a. a |\<in>| S" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
829 |
by (drule card_fset_Suc) (auto) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
830 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
831 |
lemma in_card_fset_not_0: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
832 |
shows "a |\<in>| A \<Longrightarrow> card_fset A \<noteq> 0" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
833 |
by (descending) (auto) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
834 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
835 |
lemma card_fset_mono: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
836 |
shows "xs |\<subseteq>| ys \<Longrightarrow> card_fset xs \<le> card_fset ys" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
837 |
unfolding card_fset psubset_fset |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
838 |
by (simp add: card_mono subset_fset) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
839 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
840 |
lemma card_subset_fset_eq: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
841 |
shows "xs |\<subseteq>| ys \<Longrightarrow> card_fset ys \<le> card_fset xs \<Longrightarrow> xs = ys" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
842 |
unfolding card_fset subset_fset |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
843 |
by (auto dest: card_seteq[OF finite_fset] simp add: fset_cong) |
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
844 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
845 |
lemma psubset_card_fset_mono: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
846 |
shows "xs |\<subset>| ys \<Longrightarrow> card_fset xs < card_fset ys" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
847 |
unfolding card_fset subset_fset |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
848 |
by (metis finite_fset psubset_fset psubset_card_mono) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
849 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
850 |
lemma card_union_inter_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
851 |
shows "card_fset xs + card_fset ys = card_fset (xs |\<union>| ys) + card_fset (xs |\<inter>| ys)" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
852 |
unfolding card_fset union_fset inter_fset |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
853 |
by (rule card_Un_Int[OF finite_fset finite_fset]) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
854 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
855 |
lemma card_union_disjoint_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
856 |
shows "xs |\<inter>| ys = {||} \<Longrightarrow> card_fset (xs |\<union>| ys) = card_fset xs + card_fset ys" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
857 |
unfolding card_fset union_fset |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
858 |
apply (rule card_Un_disjoint[OF finite_fset finite_fset]) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
859 |
by (metis inter_fset fset_simps(1)) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
860 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
861 |
lemma card_remove_fset_less1: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
862 |
shows "x |\<in>| xs \<Longrightarrow> card_fset (remove_fset x xs) < card_fset xs" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
863 |
unfolding card_fset in_fset remove_fset |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
864 |
by (rule card_Diff1_less[OF finite_fset]) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
865 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
866 |
lemma card_remove_fset_less2: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
867 |
shows "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> card_fset (remove_fset y (remove_fset x xs)) < card_fset xs" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
868 |
unfolding card_fset remove_fset in_fset |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
869 |
by (rule card_Diff2_less[OF finite_fset]) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
870 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
871 |
lemma card_remove_fset_le1: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
872 |
shows "card_fset (remove_fset x xs) \<le> card_fset xs" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
873 |
unfolding remove_fset card_fset |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
874 |
by (rule card_Diff1_le[OF finite_fset]) |
36280 | 875 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
876 |
lemma card_psubset_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
877 |
shows "ys |\<subseteq>| xs \<Longrightarrow> card_fset ys < card_fset xs \<Longrightarrow> ys |\<subset>| xs" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
878 |
unfolding card_fset psubset_fset subset_fset |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
879 |
by (rule card_psubset[OF finite_fset]) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
880 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
881 |
lemma card_map_fset_le: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
882 |
shows "card_fset (map_fset f xs) \<le> card_fset xs" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
883 |
unfolding card_fset map_fset_image |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
884 |
by (rule card_image_le[OF finite_fset]) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
885 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
886 |
lemma card_minus_insert_fset[simp]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
887 |
assumes "a |\<in>| A" and "a |\<notin>| B" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
888 |
shows "card_fset (A - insert_fset a B) = card_fset (A - B) - 1" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
889 |
using assms |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
890 |
unfolding in_fset card_fset minus_fset |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
891 |
by (simp add: card_Diff_insert[OF finite_fset]) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
892 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
893 |
lemma card_minus_subset_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
894 |
assumes "B |\<subseteq>| A" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
895 |
shows "card_fset (A - B) = card_fset A - card_fset B" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
896 |
using assms |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
897 |
unfolding subset_fset card_fset minus_fset |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
898 |
by (rule card_Diff_subset[OF finite_fset]) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
899 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
900 |
lemma card_minus_fset: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
901 |
shows "card_fset (A - B) = card_fset A - card_fset (A |\<inter>| B)" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
902 |
unfolding inter_fset card_fset minus_fset |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
903 |
by (rule card_Diff_subset_Int) (simp) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
904 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
905 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
906 |
subsection {* concat_fset *} |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
907 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
908 |
lemma concat_empty_fset [simp]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
909 |
shows "concat_fset {||} = {||}" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
910 |
by (lifting concat.simps(1)) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
911 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
912 |
lemma concat_insert_fset [simp]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
913 |
shows "concat_fset (insert_fset x S) = x |\<union>| concat_fset S" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
914 |
by (lifting concat.simps(2)) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
915 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
916 |
lemma concat_inter_fset [simp]: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
917 |
shows "concat_fset (xs |\<union>| ys) = concat_fset xs |\<union>| concat_fset ys" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
918 |
by (lifting concat_append) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
919 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
920 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
921 |
subsection {* filter_fset *} |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
922 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
923 |
lemma subset_filter_fset: |
40961 | 924 |
"filter_fset P xs |\<subseteq>| filter_fset Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)" |
925 |
by descending auto |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
926 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
927 |
lemma eq_filter_fset: |
40961 | 928 |
"(filter_fset P xs = filter_fset Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)" |
929 |
by descending auto |
|
36280 | 930 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
931 |
lemma psubset_filter_fset: |
40961 | 932 |
"(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
933 |
filter_fset P xs |\<subset>| filter_fset Q xs" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
934 |
unfolding less_fset_def by (auto simp add: subset_filter_fset eq_filter_fset) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
935 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
936 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
937 |
subsection {* fold_fset *} |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
938 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
939 |
lemma fold_empty_fset: |
40961 | 940 |
"fold_fset f {||} = id" |
40962
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
941 |
by descending (simp add: fold_once_def) |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
942 |
|
40961 | 943 |
lemma fold_insert_fset: "fold_fset f (insert_fset a A) = |
40962
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
944 |
(if rsp_fold f then if a |\<in>| A then fold_fset f A else fold_fset f A \<circ> f a else id)" |
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
945 |
by descending (simp add: fold_once_fold_remdups) |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
946 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
947 |
lemma in_commute_fold_fset: |
40962
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
948 |
"rsp_fold f \<Longrightarrow> h |\<in>| b \<Longrightarrow> fold_fset f b = fold_fset f (remove_fset h b) \<circ> f h" |
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
949 |
by descending (simp add: member_commute_fold_once) |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
950 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
951 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
952 |
subsection {* Choice in fsets *} |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
953 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
954 |
lemma fset_choice: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
955 |
assumes a: "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y)" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
956 |
shows "\<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
957 |
using a |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
958 |
apply(descending) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
959 |
using finite_set_choice |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
960 |
by (auto simp add: Ball_def) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
961 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
962 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
963 |
section {* Induction and Cases rules for fsets *} |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
964 |
|
41070 | 965 |
lemma fset_exhaust [case_names empty insert, cases type: fset]: |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
966 |
assumes empty_fset_case: "S = {||} \<Longrightarrow> P" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
967 |
and insert_fset_case: "\<And>x S'. S = insert_fset x S' \<Longrightarrow> P" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
968 |
shows "P" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
969 |
using assms by (lifting list.exhaust) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
970 |
|
41070 | 971 |
lemma fset_induct [case_names empty insert]: |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
972 |
assumes empty_fset_case: "P {||}" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
973 |
and insert_fset_case: "\<And>x S. P S \<Longrightarrow> P (insert_fset x S)" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
974 |
shows "P S" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
975 |
using assms |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
976 |
by (descending) (blast intro: list.induct) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
977 |
|
41070 | 978 |
lemma fset_induct_stronger [case_names empty insert, induct type: fset]: |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
979 |
assumes empty_fset_case: "P {||}" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
980 |
and insert_fset_case: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (insert_fset x S)" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
981 |
shows "P S" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
982 |
proof(induct S rule: fset_induct) |
41070 | 983 |
case empty |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
984 |
show "P {||}" using empty_fset_case by simp |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
985 |
next |
41070 | 986 |
case (insert x S) |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
987 |
have "P S" by fact |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
988 |
then show "P (insert_fset x S)" using insert_fset_case |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
989 |
by (cases "x |\<in>| S") (simp_all) |
36280 | 990 |
qed |
991 |
||
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
992 |
lemma fset_card_induct: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
993 |
assumes empty_fset_case: "P {||}" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
994 |
and card_fset_Suc_case: "\<And>S T. Suc (card_fset S) = (card_fset T) \<Longrightarrow> P S \<Longrightarrow> P T" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
995 |
shows "P S" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
996 |
proof (induct S) |
41070 | 997 |
case empty |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
998 |
show "P {||}" by (rule empty_fset_case) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
999 |
next |
41070 | 1000 |
case (insert x S) |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1001 |
have h: "P S" by fact |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1002 |
have "x |\<notin>| S" by fact |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1003 |
then have "Suc (card_fset S) = card_fset (insert_fset x S)" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1004 |
using card_fset_Suc by auto |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1005 |
then show "P (insert_fset x S)" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1006 |
using h card_fset_Suc_case by simp |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1007 |
qed |
36280 | 1008 |
|
1009 |
lemma fset_raw_strong_cases: |
|
36465 | 1010 |
obtains "xs = []" |
40953 | 1011 |
| ys x where "\<not> List.member ys x" and "xs \<approx> x # ys" |
45129
1fce03e3e8ad
tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
wenzelm
parents:
44512
diff
changeset
|
1012 |
proof (induct xs) |
36465 | 1013 |
case Nil |
1014 |
then show thesis by simp |
|
1015 |
next |
|
1016 |
case (Cons a xs) |
|
40953 | 1017 |
have a: "\<lbrakk>xs = [] \<Longrightarrow> thesis; \<And>x ys. \<lbrakk>\<not> List.member ys x; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis" |
1018 |
by (rule Cons(1)) |
|
1019 |
have b: "\<And>x' ys'. \<lbrakk>\<not> List.member ys' x'; a # xs \<approx> x' # ys'\<rbrakk> \<Longrightarrow> thesis" by fact |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1020 |
have c: "xs = [] \<Longrightarrow> thesis" using b |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1021 |
apply(simp) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1022 |
by (metis List.set.simps(1) emptyE empty_subsetI) |
40953 | 1023 |
have "\<And>x ys. \<lbrakk>\<not> List.member ys x; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis" |
36465 | 1024 |
proof - |
1025 |
fix x :: 'a |
|
1026 |
fix ys :: "'a list" |
|
40953 | 1027 |
assume d:"\<not> List.member ys x" |
36465 | 1028 |
assume e:"xs \<approx> x # ys" |
1029 |
show thesis |
|
1030 |
proof (cases "x = a") |
|
1031 |
assume h: "x = a" |
|
40953 | 1032 |
then have f: "\<not> List.member ys a" using d by simp |
36465 | 1033 |
have g: "a # xs \<approx> a # ys" using e h by auto |
1034 |
show thesis using b f g by simp |
|
1035 |
next |
|
1036 |
assume h: "x \<noteq> a" |
|
40953 | 1037 |
then have f: "\<not> List.member (a # ys) x" using d by auto |
36465 | 1038 |
have g: "a # xs \<approx> x # (a # ys)" using e h by auto |
40953 | 1039 |
show thesis using b f g by (simp del: List.member_def) |
36465 | 1040 |
qed |
1041 |
qed |
|
1042 |
then show thesis using a c by blast |
|
1043 |
qed |
|
36280 | 1044 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1045 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1046 |
lemma fset_strong_cases: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1047 |
obtains "xs = {||}" |
40953 | 1048 |
| ys x where "x |\<notin>| ys" and "xs = insert_fset x ys" |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1049 |
by (lifting fset_raw_strong_cases) |
36280 | 1050 |
|
39996
c02078ff8691
FSet: definition changes propagated from Nominal and more use of 'descending' tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39995
diff
changeset
|
1051 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1052 |
lemma fset_induct2: |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1053 |
"P {||} {||} \<Longrightarrow> |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1054 |
(\<And>x xs. x |\<notin>| xs \<Longrightarrow> P (insert_fset x xs) {||}) \<Longrightarrow> |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1055 |
(\<And>y ys. y |\<notin>| ys \<Longrightarrow> P {||} (insert_fset y ys)) \<Longrightarrow> |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1056 |
(\<And>x xs y ys. \<lbrakk>P xs ys; x |\<notin>| xs; y |\<notin>| ys\<rbrakk> \<Longrightarrow> P (insert_fset x xs) (insert_fset y ys)) \<Longrightarrow> |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1057 |
P xsa ysa" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1058 |
apply (induct xsa arbitrary: ysa) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1059 |
apply (induct_tac x rule: fset_induct_stronger) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1060 |
apply simp_all |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1061 |
apply (induct_tac xa rule: fset_induct_stronger) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1062 |
apply simp_all |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1063 |
done |
36280 | 1064 |
|
41070 | 1065 |
text {* Extensionality *} |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1066 |
|
41070 | 1067 |
lemma fset_eqI: |
1068 |
assumes "\<And>x. x \<in> fset A \<longleftrightarrow> x \<in> fset B" |
|
1069 |
shows "A = B" |
|
1070 |
using assms proof (induct A arbitrary: B) |
|
1071 |
case empty then show ?case |
|
1072 |
by (auto simp add: in_fset none_in_empty_fset [symmetric] sym) |
|
1073 |
next |
|
1074 |
case (insert x A) |
|
1075 |
from insert.prems insert.hyps(1) have "\<And>z. z \<in> fset A \<longleftrightarrow> z \<in> fset (B - {|x|})" |
|
1076 |
by (auto simp add: in_fset) |
|
1077 |
then have "A = B - {|x|}" by (rule insert.hyps(2)) |
|
1078 |
moreover with insert.prems [symmetric, of x] have "x |\<in>| B" by (simp add: in_fset) |
|
1079 |
ultimately show ?case by (metis in_fset_mdef) |
|
1080 |
qed |
|
36280 | 1081 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1082 |
subsection {* alternate formulation with a different decomposition principle |
36280 | 1083 |
and a proof of equivalence *} |
1084 |
||
1085 |
inductive |
|
40952 | 1086 |
list_eq2 :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<approx>2 _") |
36280 | 1087 |
where |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1088 |
"(a # b # xs) \<approx>2 (b # a # xs)" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1089 |
| "[] \<approx>2 []" |
40952 | 1090 |
| "xs \<approx>2 ys \<Longrightarrow> ys \<approx>2 xs" |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1091 |
| "(a # a # xs) \<approx>2 (a # xs)" |
40952 | 1092 |
| "xs \<approx>2 ys \<Longrightarrow> (a # xs) \<approx>2 (a # ys)" |
1093 |
| "xs1 \<approx>2 xs2 \<Longrightarrow> xs2 \<approx>2 xs3 \<Longrightarrow> xs1 \<approx>2 xs3" |
|
36280 | 1094 |
|
1095 |
lemma list_eq2_refl: |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1096 |
shows "xs \<approx>2 xs" |
36280 | 1097 |
by (induct xs) (auto intro: list_eq2.intros) |
1098 |
||
1099 |
lemma cons_delete_list_eq2: |
|
40953 | 1100 |
shows "(a # (removeAll a A)) \<approx>2 (if List.member A a then A else a # A)" |
36280 | 1101 |
apply (induct A) |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1102 |
apply (simp add: list_eq2_refl) |
40953 | 1103 |
apply (case_tac "List.member (aa # A) a") |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1104 |
apply (simp_all) |
36280 | 1105 |
apply (case_tac [!] "a = aa") |
1106 |
apply (simp_all) |
|
40953 | 1107 |
apply (case_tac "List.member A a") |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1108 |
apply (auto)[2] |
36280 | 1109 |
apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6)) |
1110 |
apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6)) |
|
40953 | 1111 |
apply (auto simp add: list_eq2_refl) |
36280 | 1112 |
done |
1113 |
||
40953 | 1114 |
lemma member_delete_list_eq2: |
1115 |
assumes a: "List.member r e" |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1116 |
shows "(e # removeAll e r) \<approx>2 r" |
36280 | 1117 |
using a cons_delete_list_eq2[of e r] |
1118 |
by simp |
|
1119 |
||
1120 |
lemma list_eq2_equiv: |
|
1121 |
"(l \<approx> r) \<longleftrightarrow> (list_eq2 l r)" |
|
1122 |
proof |
|
1123 |
show "list_eq2 l r \<Longrightarrow> l \<approx> r" by (induct rule: list_eq2.induct) auto |
|
1124 |
next |
|
1125 |
{ |
|
1126 |
fix n |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1127 |
assume a: "card_list l = n" and b: "l \<approx> r" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1128 |
have "l \<approx>2 r" |
36280 | 1129 |
using a b |
1130 |
proof (induct n arbitrary: l r) |
|
1131 |
case 0 |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1132 |
have "card_list l = 0" by fact |
40953 | 1133 |
then have "\<forall>x. \<not> List.member l x" by auto |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1134 |
then have z: "l = []" by auto |
36280 | 1135 |
then have "r = []" using `l \<approx> r` by simp |
1136 |
then show ?case using z list_eq2_refl by simp |
|
1137 |
next |
|
1138 |
case (Suc m) |
|
1139 |
have b: "l \<approx> r" by fact |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1140 |
have d: "card_list l = Suc m" by fact |
40953 | 1141 |
then have "\<exists>a. List.member l a" |
41067 | 1142 |
apply(simp) |
1143 |
apply(drule card_eq_SucD) |
|
1144 |
apply(blast) |
|
1145 |
done |
|
40953 | 1146 |
then obtain a where e: "List.member l a" by auto |
1147 |
then have e': "List.member r a" using list_eq_def [simplified List.member_def [symmetric], of l r] b |
|
41067 | 1148 |
by auto |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1149 |
have f: "card_list (removeAll a l) = m" using e d by (simp) |
39996
c02078ff8691
FSet: definition changes propagated from Nominal and more use of 'descending' tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39995
diff
changeset
|
1150 |
have g: "removeAll a l \<approx> removeAll a r" using removeAll_rsp b by simp |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1151 |
have "(removeAll a l) \<approx>2 (removeAll a r)" by (rule Suc.hyps[OF f g]) |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1152 |
then have h: "(a # removeAll a l) \<approx>2 (a # removeAll a r)" by (rule list_eq2.intros(5)) |
41067 | 1153 |
have i: "l \<approx>2 (a # removeAll a l)" |
40953 | 1154 |
by (rule list_eq2.intros(3)[OF member_delete_list_eq2[OF e]]) |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1155 |
have "l \<approx>2 (a # removeAll a r)" by (rule list_eq2.intros(6)[OF i h]) |
40953 | 1156 |
then show ?case using list_eq2.intros(6)[OF _ member_delete_list_eq2[OF e']] by simp |
36280 | 1157 |
qed |
1158 |
} |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1159 |
then show "l \<approx> r \<Longrightarrow> l \<approx>2 r" by blast |
36280 | 1160 |
qed |
1161 |
||
1162 |
||
1163 |
(* We cannot write it as "assumes .. shows" since Isabelle changes |
|
1164 |
the quantifiers to schematic variables and reintroduces them in |
|
1165 |
a different order *) |
|
1166 |
lemma fset_eq_cases: |
|
1167 |
"\<lbrakk>a1 = a2; |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1168 |
\<And>a b xs. \<lbrakk>a1 = insert_fset a (insert_fset b xs); a2 = insert_fset b (insert_fset a xs)\<rbrakk> \<Longrightarrow> P; |
36280 | 1169 |
\<lbrakk>a1 = {||}; a2 = {||}\<rbrakk> \<Longrightarrow> P; \<And>xs ys. \<lbrakk>a1 = ys; a2 = xs; xs = ys\<rbrakk> \<Longrightarrow> P; |
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1170 |
\<And>a xs. \<lbrakk>a1 = insert_fset a (insert_fset a xs); a2 = insert_fset a xs\<rbrakk> \<Longrightarrow> P; |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1171 |
\<And>xs ys a. \<lbrakk>a1 = insert_fset a xs; a2 = insert_fset a ys; xs = ys\<rbrakk> \<Longrightarrow> P; |
36280 | 1172 |
\<And>xs1 xs2 xs3. \<lbrakk>a1 = xs1; a2 = xs3; xs1 = xs2; xs2 = xs3\<rbrakk> \<Longrightarrow> P\<rbrakk> |
1173 |
\<Longrightarrow> P" |
|
1174 |
by (lifting list_eq2.cases[simplified list_eq2_equiv[symmetric]]) |
|
1175 |
||
1176 |
lemma fset_eq_induct: |
|
1177 |
assumes "x1 = x2" |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1178 |
and "\<And>a b xs. P (insert_fset a (insert_fset b xs)) (insert_fset b (insert_fset a xs))" |
36280 | 1179 |
and "P {||} {||}" |
1180 |
and "\<And>xs ys. \<lbrakk>xs = ys; P xs ys\<rbrakk> \<Longrightarrow> P ys xs" |
|
40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1181 |
and "\<And>a xs. P (insert_fset a (insert_fset a xs)) (insert_fset a xs)" |
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1182 |
and "\<And>xs ys a. \<lbrakk>xs = ys; P xs ys\<rbrakk> \<Longrightarrow> P (insert_fset a xs) (insert_fset a ys)" |
36280 | 1183 |
and "\<And>xs1 xs2 xs3. \<lbrakk>xs1 = xs2; P xs1 xs2; xs2 = xs3; P xs2 xs3\<rbrakk> \<Longrightarrow> P xs1 xs3" |
1184 |
shows "P x1 x2" |
|
1185 |
using assms |
|
1186 |
by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]]) |
|
1187 |
||
1188 |
ML {* |
|
36465 | 1189 |
fun dest_fsetT (Type (@{type_name fset}, [T])) = T |
36280 | 1190 |
| dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
1191 |
*} |
|
1192 |
||
1193 |
no_notation |
|
40034 | 1194 |
list_eq (infix "\<approx>" 50) and |
1195 |
list_eq2 (infix "\<approx>2" 50) |
|
36280 | 1196 |
|
1197 |
end |