author | wenzelm |
Sat, 20 Aug 2011 23:36:18 +0200 | |
changeset 44339 | eda6aef75939 |
parent 44204 | 3cdc4176638c |
child 44512 | 5e0f9e0e32fb |
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" |
|
199 |
by (auto intro!: fun_relI simp add: mem_def) |
|
36280 | 200 |
|
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
|
201 |
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
|
202 |
shows "(op \<approx>) Nil Nil" |
36280 | 203 |
by simp |
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 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
|
206 |
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
|
207 |
by (auto intro!: fun_relI) |
36280 | 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 map_rsp [quot_respect]: |
36280 | 210 |
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
|
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 set_rsp [quot_respect]: |
36280 | 214 |
"(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
|
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 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
|
218 |
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
|
219 |
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
|
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 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
|
222 |
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
|
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 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
|
226 |
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
|
227 |
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
|
228 |
|
9f8dcf6ef563
reorganisation of 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 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
|
230 |
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
|
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 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
|
234 |
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
|
235 |
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
|
236 |
|
40962
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
237 |
lemma remdups_removeAll: (*FIXME move*) |
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
238 |
"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
|
239 |
by (induct xs) auto |
36280 | 240 |
|
40962
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
241 |
lemma member_commute_fold_once: |
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
242 |
assumes "rsp_fold f" |
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
243 |
and "x \<in> set xs" |
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
244 |
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
|
245 |
proof - |
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
246 |
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
|
247 |
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
|
248 |
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
|
249 |
qed |
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
250 |
|
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
251 |
lemma fold_once_set_equiv: |
40961 | 252 |
assumes "xs \<approx> ys" |
40962
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
253 |
shows "fold_once f xs = fold_once f ys" |
40961 | 254 |
proof (cases "rsp_fold f") |
255 |
case False then show ?thesis by simp |
|
256 |
next |
|
257 |
case True |
|
258 |
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" |
|
259 |
by (rule rsp_foldE) |
|
260 |
moreover from assms have "multiset_of (remdups xs) = multiset_of (remdups ys)" |
|
261 |
by (simp add: set_eq_iff_multiset_of_remdups_eq) |
|
262 |
ultimately have "fold f (remdups xs) = fold f (remdups ys)" |
|
263 |
by (rule fold_multiset_equiv) |
|
40962
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
264 |
with True show ?thesis by (simp add: fold_once_fold_remdups) |
40961 | 265 |
qed |
36280 | 266 |
|
40962
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
267 |
lemma fold_once_rsp [quot_respect]: |
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
268 |
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
|
269 |
unfolding fun_rel_def by (auto intro: fold_once_set_equiv) |
36280 | 270 |
|
271 |
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
|
272 |
assumes a: "list_all2 op \<approx> x x'" |
36280 | 273 |
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
|
274 |
and c: "list_all2 op \<approx> y' y" |
36280 | 275 |
and d: "\<exists>x\<in>set x. xa \<in> set x" |
276 |
shows "\<exists>x\<in>set y. xa \<in> set x" |
|
277 |
proof - |
|
278 |
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
|
279 |
have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_all2_find_element[OF e a]) |
36280 | 280 |
then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto |
36465 | 281 |
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
|
282 |
then have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" using c by (rule list_all2_find_element) |
36280 | 283 |
then show ?thesis using f i by auto |
284 |
qed |
|
285 |
||
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
|
286 |
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
|
287 |
shows "(list_all2 op \<approx> OOO op \<approx> ===> op \<approx>) concat concat" |
36280 | 288 |
proof (rule fun_relI, elim pred_compE) |
289 |
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
|
290 |
assume a: "list_all2 op \<approx> a ba" |
40822 | 291 |
with list_symp [OF list_eq_symp] have a': "list_all2 op \<approx> ba a" by (rule sympE) |
36280 | 292 |
assume b: "ba \<approx> bb" |
40822 | 293 |
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
|
294 |
assume c: "list_all2 op \<approx> bb b" |
40822 | 295 |
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
|
296 |
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
|
297 |
proof |
36280 | 298 |
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
|
299 |
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
|
300 |
proof |
36280 | 301 |
assume d: "\<exists>xa\<in>set a. x \<in> set xa" |
302 |
show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d]) |
|
303 |
next |
|
304 |
assume e: "\<exists>xa\<in>set b. x \<in> set xa" |
|
305 |
show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e]) |
|
306 |
qed |
|
307 |
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
|
308 |
then show "concat a \<approx> concat b" by auto |
36280 | 309 |
qed |
310 |
||
36639
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
311 |
|
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
|
312 |
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
|
313 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
314 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
315 |
subsection {* Finite sets are a bounded, distributive lattice with minus *} |
36280 | 316 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
317 |
instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}" |
36280 | 318 |
begin |
319 |
||
320 |
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
|
321 |
"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
|
322 |
is "Nil :: 'a list" |
36280 | 323 |
|
324 |
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
|
325 |
empty_fset ("{||}") |
36280 | 326 |
where |
327 |
"{||} \<equiv> bot :: 'a fset" |
|
328 |
||
329 |
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
|
330 |
"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
|
331 |
is "sub_list :: ('a list \<Rightarrow> 'a list \<Rightarrow> bool)" |
36280 | 332 |
|
333 |
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
|
334 |
subset_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subseteq>|" 50) |
36280 | 335 |
where |
336 |
"xs |\<subseteq>| ys \<equiv> xs \<le> ys" |
|
337 |
||
338 |
definition |
|
39995 | 339 |
less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" |
340 |
where |
|
341 |
"xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a fset)" |
|
36280 | 342 |
|
343 |
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
|
344 |
psubset_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subset>|" 50) |
36280 | 345 |
where |
346 |
"xs |\<subset>| ys \<equiv> xs < ys" |
|
347 |
||
348 |
quotient_definition |
|
39995 | 349 |
"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
|
350 |
is "append :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
36280 | 351 |
|
352 |
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
|
353 |
union_fset (infixl "|\<union>|" 65) |
36280 | 354 |
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
|
355 |
"xs |\<union>| ys \<equiv> sup xs (ys::'a fset)" |
36280 | 356 |
|
357 |
quotient_definition |
|
39995 | 358 |
"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
|
359 |
is "inter_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
36280 | 360 |
|
361 |
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
|
362 |
inter_fset (infixl "|\<inter>|" 65) |
36280 | 363 |
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
|
364 |
"xs |\<inter>| ys \<equiv> inf xs (ys::'a fset)" |
36280 | 365 |
|
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
366 |
quotient_definition |
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
367 |
"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
|
368 |
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
|
369 |
|
36280 | 370 |
instance |
371 |
proof |
|
372 |
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
|
373 |
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
|
374 |
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
|
375 |
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
|
376 |
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
|
377 |
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
|
378 |
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
|
379 |
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
|
380 |
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
|
381 |
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
|
382 |
by (descending) (auto) |
36280 | 383 |
next |
384 |
fix x y z :: "'a fset" |
|
385 |
assume a: "x |\<subseteq>| y" |
|
386 |
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
|
387 |
show "x |\<subseteq>| z" using a b by (descending) (simp) |
36280 | 388 |
next |
389 |
fix x y :: "'a fset" |
|
390 |
assume a: "x |\<subseteq>| y" |
|
391 |
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
|
392 |
show "x = y" using a b by (descending) (auto) |
36280 | 393 |
next |
394 |
fix x y z :: "'a fset" |
|
395 |
assume a: "y |\<subseteq>| x" |
|
396 |
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
|
397 |
show "y |\<union>| z |\<subseteq>| x" using a b by (descending) (simp) |
36280 | 398 |
next |
399 |
fix x y z :: "'a fset" |
|
400 |
assume a: "x |\<subseteq>| y" |
|
401 |
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
|
402 |
show "x |\<subseteq>| y |\<inter>| z" using a b by (descending) (auto) |
36280 | 403 |
qed |
404 |
||
405 |
end |
|
406 |
||
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
|
407 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
408 |
subsection {* Other constants for fsets *} |
36280 | 409 |
|
410 |
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
|
411 |
"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
|
412 |
is "Cons" |
36280 | 413 |
|
414 |
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
|
415 |
"@Insert_fset" :: "args => 'a fset" ("{|(_)|}") |
36280 | 416 |
|
417 |
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
|
418 |
"{|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
|
419 |
"{|x|}" == "CONST insert_fset x {||}" |
36280 | 420 |
|
421 |
quotient_definition |
|
40953 | 422 |
fset_member |
36280 | 423 |
where |
40953 | 424 |
"fset_member :: 'a fset \<Rightarrow> 'a \<Rightarrow> bool" is "List.member" |
425 |
||
426 |
abbreviation |
|
427 |
in_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) |
|
428 |
where |
|
429 |
"x |\<in>| S \<equiv> fset_member S x" |
|
36280 | 430 |
|
431 |
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
|
432 |
notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) |
36280 | 433 |
where |
434 |
"x |\<notin>| S \<equiv> \<not> (x |\<in>| S)" |
|
435 |
||
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 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
437 |
subsection {* Other constants on the Quotient Type *} |
36280 | 438 |
|
439 |
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
|
440 |
"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
|
441 |
is card_list |
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 |
"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
|
445 |
is map |
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 |
"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
|
449 |
is removeAll |
36280 | 450 |
|
451 |
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
|
452 |
"fset :: 'a fset \<Rightarrow> 'a set" |
36280 | 453 |
is "set" |
454 |
||
455 |
quotient_definition |
|
40961 | 456 |
"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
|
457 |
is fold_once |
36280 | 458 |
|
459 |
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
|
460 |
"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
|
461 |
is concat |
36280 | 462 |
|
36639
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
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 |
"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
|
465 |
is filter |
36639
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
466 |
|
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
|
467 |
|
9f8dcf6ef563
reorganisation of 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 |
subsection {* Compositional respectfulness and preservation lemmas *} |
36280 | 469 |
|
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
|
470 |
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
|
471 |
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
|
472 |
by (rule compose_list_refl, rule list_eq_equivp) |
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 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
|
475 |
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
|
476 |
apply (auto intro!: fun_relI) |
36280 | 477 |
apply (rule_tac b="x # b" in pred_compI) |
478 |
apply auto |
|
479 |
apply (rule_tac b="x # ba" in pred_compI) |
|
480 |
apply auto |
|
481 |
done |
|
482 |
||
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
|
483 |
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
|
484 |
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
|
485 |
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
|
486 |
|
9f8dcf6ef563
reorganisation of 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 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
|
488 |
"(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
|
489 |
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
|
490 |
abs_o_rep[OF Quotient_fset] map_id insert_fset_def) |
36280 | 491 |
|
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
|
492 |
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
|
493 |
"((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
|
494 |
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
|
495 |
by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset] |
36280 | 496 |
abs_o_rep[OF Quotient_fset] map_id sup_fset_def) |
497 |
||
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
498 |
lemma list_all2_app_l: |
36280 | 499 |
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
|
500 |
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
|
501 |
shows "list_all2 R (z @ l) (z @ r)" |
40822 | 502 |
using a b by (induct z) (auto elim: reflpE) |
36280 | 503 |
|
504 |
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
|
505 |
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
|
506 |
shows "list_all2 op \<approx> (x @ z) (x' @ z)" |
36280 | 507 |
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
|
508 |
by simp_all (rule list_all2_refl'[OF list_eq_equivp]) |
36280 | 509 |
|
510 |
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
|
511 |
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
|
512 |
shows "list_all2 op \<approx> (z @ x) (z @ x')" |
36280 | 513 |
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
|
514 |
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
|
515 |
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
|
516 |
apply (rule list_all2_app_l) |
40822 | 517 |
apply (simp_all add: reflpI) |
36280 | 518 |
done |
519 |
||
520 |
lemma append_rsp2_pre: |
|
40822 | 521 |
assumes "list_all2 op \<approx> x x'" |
522 |
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
|
523 |
shows "list_all2 op \<approx> (x @ z) (x' @ z')" |
40822 | 524 |
using assms by (rule list_all2_appendI) |
36280 | 525 |
|
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
|
526 |
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
|
527 |
"(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append" |
36280 | 528 |
proof (intro fun_relI, elim pred_compE) |
529 |
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
|
530 |
assume a:"list_all2 op \<approx> x x'" |
36280 | 531 |
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
|
532 |
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
|
533 |
assume aa: "list_all2 op \<approx> z z'" |
36280 | 534 |
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
|
535 |
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
|
536 |
have a': "list_all2 op \<approx> (x @ z) (x' @ z')" using a aa append_rsp2_pre by auto |
36280 | 537 |
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
|
538 |
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
|
539 |
have d': "(op \<approx> OO list_all2 op \<approx>) (x' @ z') (y @ w)" |
36280 | 540 |
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
|
541 |
show "(list_all2 op \<approx> OOO op \<approx>) (x @ z) (y @ w)" |
36280 | 542 |
by (rule pred_compI) (rule a', rule d') |
543 |
qed |
|
544 |
||
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
|
545 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
546 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
547 |
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
|
548 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
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 |
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
|
552 |
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
|
553 |
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
|
554 |
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
|
555 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
557 |
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
|
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 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
|
561 |
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
|
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 |
|
44204
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
41467
diff
changeset
|
564 |
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
|
565 |
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
|
566 |
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
|
567 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
568 |
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
|
569 |
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
|
570 |
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
|
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 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
|
573 |
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
|
574 |
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
|
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 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
|
577 |
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
|
578 |
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
|
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 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
|
581 |
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
|
582 |
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
|
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 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
586 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
588 |
shows "x |\<in>| S \<longleftrightarrow> x \<in> fset S" |
40953 | 589 |
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
|
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 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
|
592 |
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
|
593 |
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
|
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_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
|
596 |
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
|
597 |
by (simp add: in_fset) |
36280 | 598 |
|
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
|
599 |
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
|
600 |
shows "S = T \<longleftrightarrow> (\<forall>x. (x |\<in>| S) = (x |\<in>| T))" |
40953 | 601 |
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
|
602 |
|
9f8dcf6ef563
reorganisation of 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 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
|
604 |
shows "(\<forall>x. x |\<notin>| S) \<longleftrightarrow> S = {||}" |
40953 | 605 |
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
|
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 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
609 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
611 |
shows "x |\<in>| insert_fset y S \<longleftrightarrow> x = y \<or> x |\<in>| S" |
40953 | 612 |
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
|
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 |
9f8dcf6ef563
reorganisation of 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 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
|
616 |
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
|
617 |
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
|
618 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
620 |
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
|
621 |
by (descending) (auto) |
36280 | 622 |
|
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
|
623 |
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
|
624 |
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
|
625 |
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
|
626 |
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
|
627 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
629 |
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
|
630 |
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
|
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_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
|
633 |
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
|
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 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
|
637 |
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
|
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 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
|
641 |
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
|
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 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
646 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
648 |
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
|
649 |
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
|
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 |
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
|
652 |
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
|
653 |
by (lifting append.simps(2)) |
36280 | 654 |
|
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
|
655 |
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
|
656 |
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
|
657 |
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
|
658 |
|
9f8dcf6ef563
reorganisation of 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_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
|
660 |
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
|
661 |
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
|
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 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
|
664 |
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
|
665 |
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
|
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 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
669 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
671 |
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
|
672 |
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
|
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_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
|
675 |
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
|
676 |
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
|
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_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
|
679 |
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
|
680 |
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
|
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_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
|
683 |
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
|
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 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
|
687 |
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
|
688 |
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
|
689 |
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
|
690 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
692 |
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
|
693 |
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
|
694 |
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
|
695 |
|
9f8dcf6ef563
reorganisation of 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 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
698 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
700 |
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
|
701 |
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
|
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 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
|
704 |
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
|
705 |
by (descending) (simp) |
36280 | 706 |
|
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
|
707 |
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
|
708 |
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
|
709 |
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
|
710 |
|
9f8dcf6ef563
reorganisation of 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 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
|
712 |
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
|
713 |
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
|
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 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
717 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
719 |
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
|
720 |
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
|
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_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
|
723 |
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
|
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_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
|
727 |
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
|
728 |
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
|
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 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
|
731 |
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
|
732 |
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
|
733 |
|
36280 | 734 |
|
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
|
735 |
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
|
736 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
738 |
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
|
739 |
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
|
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 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
|
742 |
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
|
743 |
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
|
744 |
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
|
745 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
747 |
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
|
748 |
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
|
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_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
|
751 |
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
|
752 |
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
|
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_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
|
755 |
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
|
756 |
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
|
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 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
|
759 |
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
|
760 |
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
|
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 |
|
9f8dcf6ef563
reorganisation of 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 |
subsection {* map_fset *} |
36280 | 764 |
|
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
|
765 |
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
|
766 |
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
|
767 |
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
|
768 |
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
|
769 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
771 |
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
|
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 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
|
775 |
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
|
776 |
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
|
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 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
|
779 |
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
|
780 |
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
|
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 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
784 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
786 |
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
|
787 |
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
|
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_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
|
790 |
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
|
791 |
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
|
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_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
|
794 |
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
|
795 |
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
|
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_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
|
798 |
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
|
799 |
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
|
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_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
|
802 |
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
|
803 |
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
|
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_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
|
806 |
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
|
807 |
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
|
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_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
|
810 |
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
|
811 |
by simp |
36280 | 812 |
|
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
|
813 |
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
|
814 |
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
|
815 |
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
|
816 |
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
|
817 |
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
|
818 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
820 |
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
|
821 |
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
|
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_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
|
824 |
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
|
825 |
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
|
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 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
|
828 |
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
|
829 |
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
|
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 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
|
832 |
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
|
833 |
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
|
834 |
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
|
835 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
837 |
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
|
838 |
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
|
839 |
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
|
840 |
|
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
|
841 |
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
|
842 |
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
|
843 |
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
|
844 |
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
|
845 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
847 |
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
|
848 |
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
|
849 |
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
|
850 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
852 |
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
|
853 |
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
|
854 |
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
|
855 |
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
|
856 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
858 |
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
|
859 |
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
|
860 |
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
|
861 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
863 |
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
|
864 |
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
|
865 |
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
|
866 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
868 |
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
|
869 |
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
|
870 |
by (rule card_Diff1_le[OF finite_fset]) |
36280 | 871 |
|
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
|
872 |
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
|
873 |
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
|
874 |
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
|
875 |
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
|
876 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
878 |
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
|
879 |
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
|
880 |
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
|
881 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
883 |
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
|
884 |
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
|
885 |
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
|
886 |
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
|
887 |
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
|
888 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
890 |
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
|
891 |
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
|
892 |
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
|
893 |
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
|
894 |
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
|
895 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
897 |
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
|
898 |
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
|
899 |
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
|
900 |
|
9f8dcf6ef563
reorganisation of 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 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
903 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
905 |
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
|
906 |
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
|
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_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
|
909 |
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
|
910 |
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
|
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_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
|
913 |
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
|
914 |
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
|
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 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
918 |
|
9f8dcf6ef563
reorganisation of 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 |
lemma subset_filter_fset: |
40961 | 920 |
"filter_fset P xs |\<subseteq>| filter_fset Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)" |
921 |
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
|
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 eq_filter_fset: |
40961 | 924 |
"(filter_fset P xs = filter_fset Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)" |
925 |
by descending auto |
|
36280 | 926 |
|
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
|
927 |
lemma psubset_filter_fset: |
40961 | 928 |
"(\<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
|
929 |
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
|
930 |
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
|
931 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
932 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
934 |
|
9f8dcf6ef563
reorganisation of 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 |
lemma fold_empty_fset: |
40961 | 936 |
"fold_fset f {||} = id" |
40962
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
937 |
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
|
938 |
|
40961 | 939 |
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
|
940 |
(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
|
941 |
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
|
942 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
943 |
lemma in_commute_fold_fset: |
40962
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset
|
944 |
"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
|
945 |
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
|
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 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
948 |
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
|
949 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
951 |
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
|
952 |
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
|
953 |
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
|
954 |
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
|
955 |
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
|
956 |
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
|
957 |
|
9f8dcf6ef563
reorganisation of 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 |
|
9f8dcf6ef563
reorganisation of 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 |
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
|
960 |
|
41070 | 961 |
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
|
962 |
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
|
963 |
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
|
964 |
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
|
965 |
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
|
966 |
|
41070 | 967 |
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
|
968 |
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
|
969 |
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
|
970 |
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
|
971 |
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
|
972 |
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
|
973 |
|
41070 | 974 |
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
|
975 |
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
|
976 |
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
|
977 |
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
|
978 |
proof(induct S rule: fset_induct) |
41070 | 979 |
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
|
980 |
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
|
981 |
next |
41070 | 982 |
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
|
983 |
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
|
984 |
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
|
985 |
by (cases "x |\<in>| S") (simp_all) |
36280 | 986 |
qed |
987 |
||
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
|
988 |
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
|
989 |
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
|
990 |
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
|
991 |
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
|
992 |
proof (induct S) |
41070 | 993 |
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
|
994 |
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
|
995 |
next |
41070 | 996 |
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
|
997 |
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
|
998 |
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
|
999 |
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
|
1000 |
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
|
1001 |
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
|
1002 |
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
|
1003 |
qed |
36280 | 1004 |
|
1005 |
lemma fset_raw_strong_cases: |
|
36465 | 1006 |
obtains "xs = []" |
40953 | 1007 |
| ys x where "\<not> List.member ys x" and "xs \<approx> x # ys" |
36465 | 1008 |
proof (induct xs arbitrary: x ys) |
1009 |
case Nil |
|
1010 |
then show thesis by simp |
|
1011 |
next |
|
1012 |
case (Cons a xs) |
|
40953 | 1013 |
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" |
1014 |
by (rule Cons(1)) |
|
1015 |
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
|
1016 |
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
|
1017 |
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
|
1018 |
by (metis List.set.simps(1) emptyE empty_subsetI) |
40953 | 1019 |
have "\<And>x ys. \<lbrakk>\<not> List.member ys x; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis" |
36465 | 1020 |
proof - |
1021 |
fix x :: 'a |
|
1022 |
fix ys :: "'a list" |
|
40953 | 1023 |
assume d:"\<not> List.member ys x" |
36465 | 1024 |
assume e:"xs \<approx> x # ys" |
1025 |
show thesis |
|
1026 |
proof (cases "x = a") |
|
1027 |
assume h: "x = a" |
|
40953 | 1028 |
then have f: "\<not> List.member ys a" using d by simp |
36465 | 1029 |
have g: "a # xs \<approx> a # ys" using e h by auto |
1030 |
show thesis using b f g by simp |
|
1031 |
next |
|
1032 |
assume h: "x \<noteq> a" |
|
40953 | 1033 |
then have f: "\<not> List.member (a # ys) x" using d by auto |
36465 | 1034 |
have g: "a # xs \<approx> x # (a # ys)" using e h by auto |
40953 | 1035 |
show thesis using b f g by (simp del: List.member_def) |
36465 | 1036 |
qed |
1037 |
qed |
|
1038 |
then show thesis using a c by blast |
|
1039 |
qed |
|
36280 | 1040 |
|
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
|
1041 |
|
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset
|
1042 |
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
|
1043 |
obtains "xs = {||}" |
40953 | 1044 |
| 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
|
1045 |
by (lifting fset_raw_strong_cases) |
36280 | 1046 |
|
39996
c02078ff8691
FSet: definition changes propagated from Nominal and more use of 'descending' tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39995
diff
changeset
|
1047 |
|
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
|
1048 |
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
|
1049 |
"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
|
1050 |
(\<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
|
1051 |
(\<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
|
1052 |
(\<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
|
1053 |
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
|
1054 |
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
|
1055 |
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
|
1056 |
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
|
1057 |
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
|
1058 |
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
|
1059 |
done |
36280 | 1060 |
|
41070 | 1061 |
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
|
1062 |
|
41070 | 1063 |
lemma fset_eqI: |
1064 |
assumes "\<And>x. x \<in> fset A \<longleftrightarrow> x \<in> fset B" |
|
1065 |
shows "A = B" |
|
1066 |
using assms proof (induct A arbitrary: B) |
|
1067 |
case empty then show ?case |
|
1068 |
by (auto simp add: in_fset none_in_empty_fset [symmetric] sym) |
|
1069 |
next |
|
1070 |
case (insert x A) |
|
1071 |
from insert.prems insert.hyps(1) have "\<And>z. z \<in> fset A \<longleftrightarrow> z \<in> fset (B - {|x|})" |
|
1072 |
by (auto simp add: in_fset) |
|
1073 |
then have "A = B - {|x|}" by (rule insert.hyps(2)) |
|
1074 |
moreover with insert.prems [symmetric, of x] have "x |\<in>| B" by (simp add: in_fset) |
|
1075 |
ultimately show ?case by (metis in_fset_mdef) |
|
1076 |
qed |
|
36280 | 1077 |
|
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
|
1078 |
subsection {* alternate formulation with a different decomposition principle |
36280 | 1079 |
and a proof of equivalence *} |
1080 |
||
1081 |
inductive |
|
40952 | 1082 |
list_eq2 :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<approx>2 _") |
36280 | 1083 |
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
|
1084 |
"(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
|
1085 |
| "[] \<approx>2 []" |
40952 | 1086 |
| "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
|
1087 |
| "(a # a # xs) \<approx>2 (a # xs)" |
40952 | 1088 |
| "xs \<approx>2 ys \<Longrightarrow> (a # xs) \<approx>2 (a # ys)" |
1089 |
| "xs1 \<approx>2 xs2 \<Longrightarrow> xs2 \<approx>2 xs3 \<Longrightarrow> xs1 \<approx>2 xs3" |
|
36280 | 1090 |
|
1091 |
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
|
1092 |
shows "xs \<approx>2 xs" |
36280 | 1093 |
by (induct xs) (auto intro: list_eq2.intros) |
1094 |
||
1095 |
lemma cons_delete_list_eq2: |
|
40953 | 1096 |
shows "(a # (removeAll a A)) \<approx>2 (if List.member A a then A else a # A)" |
36280 | 1097 |
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
|
1098 |
apply (simp add: list_eq2_refl) |
40953 | 1099 |
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
|
1100 |
apply (simp_all) |
36280 | 1101 |
apply (case_tac [!] "a = aa") |
1102 |
apply (simp_all) |
|
40953 | 1103 |
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
|
1104 |
apply (auto)[2] |
36280 | 1105 |
apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6)) |
1106 |
apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6)) |
|
40953 | 1107 |
apply (auto simp add: list_eq2_refl) |
36280 | 1108 |
done |
1109 |
||
40953 | 1110 |
lemma member_delete_list_eq2: |
1111 |
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
|
1112 |
shows "(e # removeAll e r) \<approx>2 r" |
36280 | 1113 |
using a cons_delete_list_eq2[of e r] |
1114 |
by simp |
|
1115 |
||
1116 |
lemma list_eq2_equiv: |
|
1117 |
"(l \<approx> r) \<longleftrightarrow> (list_eq2 l r)" |
|
1118 |
proof |
|
1119 |
show "list_eq2 l r \<Longrightarrow> l \<approx> r" by (induct rule: list_eq2.induct) auto |
|
1120 |
next |
|
1121 |
{ |
|
1122 |
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
|
1123 |
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
|
1124 |
have "l \<approx>2 r" |
36280 | 1125 |
using a b |
1126 |
proof (induct n arbitrary: l r) |
|
1127 |
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
|
1128 |
have "card_list l = 0" by fact |
40953 | 1129 |
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
|
1130 |
then have z: "l = []" by auto |
36280 | 1131 |
then have "r = []" using `l \<approx> r` by simp |
1132 |
then show ?case using z list_eq2_refl by simp |
|
1133 |
next |
|
1134 |
case (Suc m) |
|
1135 |
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
|
1136 |
have d: "card_list l = Suc m" by fact |
40953 | 1137 |
then have "\<exists>a. List.member l a" |
41067 | 1138 |
apply(simp) |
1139 |
apply(drule card_eq_SucD) |
|
1140 |
apply(blast) |
|
1141 |
done |
|
40953 | 1142 |
then obtain a where e: "List.member l a" by auto |
1143 |
then have e': "List.member r a" using list_eq_def [simplified List.member_def [symmetric], of l r] b |
|
41067 | 1144 |
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
|
1145 |
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
|
1146 |
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
|
1147 |
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
|
1148 |
then have h: "(a # removeAll a l) \<approx>2 (a # removeAll a r)" by (rule list_eq2.intros(5)) |
41067 | 1149 |
have i: "l \<approx>2 (a # removeAll a l)" |
40953 | 1150 |
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
|
1151 |
have "l \<approx>2 (a # removeAll a r)" by (rule list_eq2.intros(6)[OF i h]) |
40953 | 1152 |
then show ?case using list_eq2.intros(6)[OF _ member_delete_list_eq2[OF e']] by simp |
36280 | 1153 |
qed |
1154 |
} |
|
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 |
then show "l \<approx> r \<Longrightarrow> l \<approx>2 r" by blast |
36280 | 1156 |
qed |
1157 |
||
1158 |
||
1159 |
(* We cannot write it as "assumes .. shows" since Isabelle changes |
|
1160 |
the quantifiers to schematic variables and reintroduces them in |
|
1161 |
a different order *) |
|
1162 |
lemma fset_eq_cases: |
|
1163 |
"\<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
|
1164 |
\<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 | 1165 |
\<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
|
1166 |
\<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
|
1167 |
\<And>xs ys a. \<lbrakk>a1 = insert_fset a xs; a2 = insert_fset a ys; xs = ys\<rbrakk> \<Longrightarrow> P; |
36280 | 1168 |
\<And>xs1 xs2 xs3. \<lbrakk>a1 = xs1; a2 = xs3; xs1 = xs2; xs2 = xs3\<rbrakk> \<Longrightarrow> P\<rbrakk> |
1169 |
\<Longrightarrow> P" |
|
1170 |
by (lifting list_eq2.cases[simplified list_eq2_equiv[symmetric]]) |
|
1171 |
||
1172 |
lemma fset_eq_induct: |
|
1173 |
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
|
1174 |
and "\<And>a b xs. P (insert_fset a (insert_fset b xs)) (insert_fset b (insert_fset a xs))" |
36280 | 1175 |
and "P {||} {||}" |
1176 |
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
|
1177 |
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
|
1178 |
and "\<And>xs ys a. \<lbrakk>xs = ys; P xs ys\<rbrakk> \<Longrightarrow> P (insert_fset a xs) (insert_fset a ys)" |
36280 | 1179 |
and "\<And>xs1 xs2 xs3. \<lbrakk>xs1 = xs2; P xs1 xs2; xs2 = xs3; P xs2 xs3\<rbrakk> \<Longrightarrow> P xs1 xs3" |
1180 |
shows "P x1 x2" |
|
1181 |
using assms |
|
1182 |
by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]]) |
|
1183 |
||
1184 |
ML {* |
|
36465 | 1185 |
fun dest_fsetT (Type (@{type_name fset}, [T])) = T |
36280 | 1186 |
| dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
1187 |
*} |
|
1188 |
||
1189 |
no_notation |
|
40034 | 1190 |
list_eq (infix "\<approx>" 50) and |
1191 |
list_eq2 (infix "\<approx>2" 50) |
|
36280 | 1192 |
|
1193 |
end |