author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47308  9caab698dbe4 
child 47435  e1b761c216ac 
permissions  rwrr 
47308  1 
(* Title: HOL/Quotient3_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 
45994  9 
imports "~~/src/HOL/Library/Multiset" "~~/src/HOL/Library/Quotient_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 pointfree 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 pointfree 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: 
47308  120 
assumes q: "Quotient3 R Abs Rep" 
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

121 
and e: "equivp R" 
47308  122 
shows "Quotient3 ((list_all2 R) OOO (op \<approx>)) 
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

123 
(abs_fset \<circ> (map Abs)) ((map Rep) \<circ> rep_fset)" 
47308  124 
unfolding Quotient3_def comp_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

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" 
47308  128 
by (simp add: abs_o_rep[OF q] Quotient3_abs_rep[OF Quotient3_fset] List.map.id) 
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

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" 
47308  149 
using Quotient3_rel[OF list_quotient3[OF q]] c by blast 
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

150 
have "map Abs ba = map Abs s" 
47308  151 
using Quotient3_rel[OF list_quotient3[OF q]] e by blast 
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

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)" 
47308  156 
using Quotient3_rel[OF Quotient3_fset] by blast 
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

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" 
47308  162 
by (subst Quotient3_rel [OF Quotient3_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" 
47308  166 
by (fact rep_abs_rsp_left[OF list_quotient3[OF q], OF list_all2_refl'[OF e, of 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

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))" 
47308  170 
by (fact rep_abs_rsp[OF list_quotient3[OF q], OF list_all2_refl'[OF e, of r]]) 
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

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]: 
47308  177 
shows "Quotient3 ((list_all2 op \<approx>) OOO (op \<approx>)) 
36280  178 
(abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)" 
47308  179 
by (rule quotient_compose_list_g, rule Quotient3_fset, rule list_eq_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

180 

36280  181 

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

182 
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

183 

9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset

184 

9f8dcf6ef563
reorganisation of 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 
subsection {* Finite sets are a bounded, distributive lattice with minus *} 
36280  186 

37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset

187 
instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}" 
36280  188 
begin 
189 

190 
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

191 
"bot :: 'a fset" 
47092  192 
is "Nil :: 'a list" done 
36280  193 

194 
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

195 
empty_fset ("{}") 
36280  196 
where 
197 
"{} \<equiv> bot :: 'a fset" 

198 

199 
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

200 
"less_eq_fset :: ('a fset \<Rightarrow> 'a fset \<Rightarrow> bool)" 
47092  201 
is "sub_list :: ('a list \<Rightarrow> 'a list \<Rightarrow> bool)" by simp 
36280  202 

203 
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

204 
subset_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "\<subseteq>" 50) 
36280  205 
where 
206 
"xs \<subseteq> ys \<equiv> xs \<le> ys" 

207 

208 
definition 

39995  209 
less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" 
210 
where 

211 
"xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a fset)" 

36280  212 

213 
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

214 
psubset_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "\<subset>" 50) 
36280  215 
where 
216 
"xs \<subset> ys \<equiv> xs < ys" 

217 

218 
quotient_definition 

39995  219 
"sup :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" 
47092  220 
is "append :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" by simp 
36280  221 

222 
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

223 
union_fset (infixl "\<union>" 65) 
36280  224 
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

225 
"xs \<union> ys \<equiv> sup xs (ys::'a fset)" 
36280  226 

227 
quotient_definition 

39995  228 
"inf :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" 
47092  229 
is "inter_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" by simp 
36280  230 

231 
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

232 
inter_fset (infixl "\<inter>" 65) 
36280  233 
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

234 
"xs \<inter> ys \<equiv> inf xs (ys::'a fset)" 
36280  235 

36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset

236 
quotient_definition 
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset

237 
"minus :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" 
47092  238 
is "diff_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" by fastforce 
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

239 

36280  240 
instance 
241 
proof 

242 
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

243 
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

244 
by (unfold less_fset_def, descending) auto 
46441
992a1688303f
Generalize the compositional preservation theorems
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46416
diff
changeset

245 
show "x \<subseteq> x" 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

246 
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

247 
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

248 
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

249 
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

250 
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

251 
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

252 
by (descending) (auto) 
36280  253 
next 
254 
fix x y z :: "'a fset" 

255 
assume a: "x \<subseteq> y" 

256 
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

257 
show "x \<subseteq> z" using a b by (descending) (simp) 
36280  258 
next 
259 
fix x y :: "'a fset" 

260 
assume a: "x \<subseteq> y" 

261 
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

262 
show "x = y" using a b by (descending) (auto) 
36280  263 
next 
264 
fix x y z :: "'a fset" 

265 
assume a: "y \<subseteq> x" 

266 
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

267 
show "y \<union> z \<subseteq> x" using a b by (descending) (simp) 
36280  268 
next 
269 
fix x y z :: "'a fset" 

270 
assume a: "x \<subseteq> y" 

271 
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

272 
show "x \<subseteq> y \<inter> z" using a b by (descending) (auto) 
36280  273 
qed 
274 

275 
end 

276 

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

277 

9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset

278 
subsection {* Other constants for fsets *} 
36280  279 

280 
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

281 
"insert_fset :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" 
47092  282 
is "Cons" by auto 
36280  283 

284 
syntax 

45343  285 
"_insert_fset" :: "args => 'a fset" ("{(_)}") 
36280  286 

287 
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

288 
"{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

289 
"{x}" == "CONST insert_fset x {}" 
36280  290 

291 
quotient_definition 

40953  292 
fset_member 
36280  293 
where 
47092  294 
"fset_member :: 'a fset \<Rightarrow> 'a \<Rightarrow> bool" is "List.member" by fastforce 
40953  295 

296 
abbreviation 

297 
in_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "\<in>" 50) 

298 
where 

299 
"x \<in> S \<equiv> fset_member S x" 

36280  300 

301 
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

302 
notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "\<notin>" 50) 
36280  303 
where 
304 
"x \<notin> S \<equiv> \<not> (x \<in> S)" 

305 

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

306 

9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset

307 
subsection {* Other constants on the Quotient Type *} 
36280  308 

309 
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

310 
"card_fset :: 'a fset \<Rightarrow> nat" 
47092  311 
is card_list by simp 
36280  312 

313 
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

314 
"map_fset :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" 
47092  315 
is map by simp 
36280  316 

317 
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

318 
"remove_fset :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" 
47092  319 
is removeAll by simp 
36280  320 

321 
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

322 
"fset :: 'a fset \<Rightarrow> 'a set" 
47092  323 
is "set" by simp 
324 

325 
lemma fold_once_set_equiv: 

326 
assumes "xs \<approx> ys" 

327 
shows "fold_once f xs = fold_once f ys" 

328 
proof (cases "rsp_fold f") 

329 
case False then show ?thesis by simp 

330 
next 

331 
case True 

332 
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" 

333 
by (rule rsp_foldE) 

334 
moreover from assms have "multiset_of (remdups xs) = multiset_of (remdups ys)" 

335 
by (simp add: set_eq_iff_multiset_of_remdups_eq) 

336 
ultimately have "fold f (remdups xs) = fold f (remdups ys)" 

337 
by (rule fold_multiset_equiv) 

338 
with True show ?thesis by (simp add: fold_once_fold_remdups) 

339 
qed 

36280  340 

341 
quotient_definition 

40961  342 
"fold_fset :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b \<Rightarrow> 'b" 
47092  343 
is fold_once by (rule fold_once_set_equiv) 
344 

345 
lemma concat_rsp_pre: 

346 
assumes a: "list_all2 op \<approx> x x'" 

347 
and b: "x' \<approx> y'" 

348 
and c: "list_all2 op \<approx> y' y" 

349 
and d: "\<exists>x\<in>set x. xa \<in> set x" 

350 
shows "\<exists>x\<in>set y. xa \<in> set x" 

351 
proof  

352 
obtain xb where e: "xb \<in> set x" and f: "xa \<in> set xb" using d by auto 

353 
have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_all2_find_element[OF e a]) 

354 
then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto 

355 
have "ya \<in> set y'" using b h by simp 

356 
then have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" using c by (rule list_all2_find_element) 

357 
then show ?thesis using f i by auto 

358 
qed 

36280  359 

360 
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

361 
"concat_fset :: ('a fset) fset \<Rightarrow> 'a fset" 
47092  362 
is concat 
363 
proof (elim pred_compE) 

364 
fix a b ba bb 

365 
assume a: "list_all2 op \<approx> a ba" 

366 
with list_symp [OF list_eq_symp] have a': "list_all2 op \<approx> ba a" by (rule sympE) 

367 
assume b: "ba \<approx> bb" 

368 
with list_eq_symp have b': "bb \<approx> ba" by (rule sympE) 

369 
assume c: "list_all2 op \<approx> bb b" 

370 
with list_symp [OF list_eq_symp] have c': "list_all2 op \<approx> b bb" by (rule sympE) 

371 
have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" 

372 
proof 

373 
fix x 

374 
show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" 

375 
proof 

376 
assume d: "\<exists>xa\<in>set a. x \<in> set xa" 

377 
show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d]) 

378 
next 

379 
assume e: "\<exists>xa\<in>set b. x \<in> set xa" 

380 
show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e]) 

381 
qed 

382 
qed 

383 
then show "concat a \<approx> concat b" by auto 

384 
qed 

36280  385 

36639
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset

386 
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

387 
"filter_fset :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" 
47092  388 
is filter by force 
36639
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset

389 

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

390 

9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset

391 
subsection {* Compositional respectfulness and preservation lemmas *} 
36280  392 

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

393 
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

394 
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

395 
by (rule compose_list_refl, rule list_eq_equivp) 
36280  396 

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 
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

398 
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

399 
apply (auto intro!: fun_relI) 
36280  400 
apply (rule_tac b="x # b" in pred_compI) 
401 
apply auto 

402 
apply (rule_tac b="x # ba" in pred_compI) 

403 
apply auto 

404 
done 

405 

46441
992a1688303f
Generalize the compositional preservation theorems
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46416
diff
changeset

406 
lemma Nil_prs2 [quot_preserve]: 
47308  407 
assumes "Quotient3 R Abs Rep" 
46441
992a1688303f
Generalize the compositional preservation theorems
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46416
diff
changeset

408 
shows "(Abs \<circ> map f) [] = Abs []" 
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

409 
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

410 

46441
992a1688303f
Generalize the compositional preservation theorems
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46416
diff
changeset

411 
lemma Cons_prs2 [quot_preserve]: 
47308  412 
assumes q: "Quotient3 R1 Abs1 Rep1" 
413 
and r: "Quotient3 R2 Abs2 Rep2" 

46441
992a1688303f
Generalize the compositional preservation theorems
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46416
diff
changeset

414 
shows "(Rep1 > (map Rep1 \<circ> Rep2) > (Abs2 \<circ> map Abs1)) (op #) = (id > Rep2 > Abs2) (op #)" 
47308  415 
by (auto simp add: fun_eq_iff comp_def Quotient3_abs_rep [OF q]) 
36280  416 

46441
992a1688303f
Generalize the compositional preservation theorems
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46416
diff
changeset

417 
lemma append_prs2 [quot_preserve]: 
47308  418 
assumes q: "Quotient3 R1 Abs1 Rep1" 
419 
and r: "Quotient3 R2 Abs2 Rep2" 

46441
992a1688303f
Generalize the compositional preservation theorems
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46416
diff
changeset

420 
shows "((map Rep1 \<circ> Rep2) > (map Rep1 \<circ> Rep2) > (Abs2 \<circ> map Abs1)) op @ = 
992a1688303f
Generalize the compositional preservation theorems
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46416
diff
changeset

421 
(Rep2 > Rep2 > Abs2) op @" 
46663  422 
by (simp add: fun_eq_iff abs_o_rep[OF q] List.map.id) 
36280  423 

37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset

424 
lemma list_all2_app_l: 
36280  425 
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

426 
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

427 
shows "list_all2 R (z @ l) (z @ r)" 
40822  428 
using a b by (induct z) (auto elim: reflpE) 
36280  429 

430 
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

431 
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

432 
shows "list_all2 op \<approx> (x @ z) (x' @ z)" 
36280  433 
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

434 
by simp_all (rule list_all2_refl'[OF list_eq_equivp]) 
36280  435 

436 
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

437 
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

438 
shows "list_all2 op \<approx> (z @ x) (z @ x')" 
36280  439 
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

440 
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

441 
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

442 
apply (rule list_all2_app_l) 
40822  443 
apply (simp_all add: reflpI) 
36280  444 
done 
445 

446 
lemma append_rsp2_pre: 

40822  447 
assumes "list_all2 op \<approx> x x'" 
448 
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

449 
shows "list_all2 op \<approx> (x @ z) (x' @ z')" 
40822  450 
using assms by (rule list_all2_appendI) 
36280  451 

46441
992a1688303f
Generalize the compositional preservation theorems
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46416
diff
changeset

452 
lemma compositional_rsp3: 
992a1688303f
Generalize the compositional preservation theorems
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46416
diff
changeset

453 
assumes "(R1 ===> R2 ===> R3) C C" and "(R4 ===> R5 ===> R6) C C" 
992a1688303f
Generalize the compositional preservation theorems
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46416
diff
changeset

454 
shows "(R1 OOO R4 ===> R2 OOO R5 ===> R3 OOO R6) C C" 
992a1688303f
Generalize the compositional preservation theorems
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46416
diff
changeset

455 
by (auto intro!: fun_relI) 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46663
diff
changeset

456 
(metis (full_types) assms fun_relE pred_compI) 
46441
992a1688303f
Generalize the compositional preservation theorems
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46416
diff
changeset

457 

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

458 
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

459 
"(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append" 
47092  460 
by (intro compositional_rsp3) 
46441
992a1688303f
Generalize the compositional preservation theorems
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46416
diff
changeset

461 
(auto intro!: fun_relI simp add: append_rsp2_pre) 
36280  462 

46404
7736068b9f56
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46133
diff
changeset

463 
lemma map_rsp2 [quot_respect]: 
7736068b9f56
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46133
diff
changeset

464 
"((op \<approx> ===> op \<approx>) ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) map map" 
7736068b9f56
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46133
diff
changeset

465 
proof (auto intro!: fun_relI) 
7736068b9f56
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46133
diff
changeset

466 
fix f f' :: "'a list \<Rightarrow> 'b list" 
7736068b9f56
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46133
diff
changeset

467 
fix xa ya x y :: "'a list list" 
7736068b9f56
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46133
diff
changeset

468 
assume fs: "(op \<approx> ===> op \<approx>) f f'" and x: "list_all2 op \<approx> xa x" and xy: "set x = set y" and y: "list_all2 op \<approx> y ya" 
7736068b9f56
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46133
diff
changeset

469 
have a: "(list_all2 op \<approx>) (map f xa) (map f x)" 
7736068b9f56
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46133
diff
changeset

470 
using x 
7736068b9f56
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46133
diff
changeset

471 
by (induct xa x rule: list_induct2') 
7736068b9f56
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46133
diff
changeset

472 
(simp_all, metis fs fun_relE list_eq_def) 
7736068b9f56
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46133
diff
changeset

473 
have b: "set (map f x) = set (map f y)" 
7736068b9f56
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46133
diff
changeset

474 
using xy fs 
7736068b9f56
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46133
diff
changeset

475 
by (induct x y rule: list_induct2') 
7736068b9f56
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46133
diff
changeset

476 
(simp_all, metis image_insert) 
7736068b9f56
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46133
diff
changeset

477 
have c: "(list_all2 op \<approx>) (map f y) (map f' ya)" 
7736068b9f56
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46133
diff
changeset

478 
using y fs 
7736068b9f56
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46133
diff
changeset

479 
by (induct y ya rule: list_induct2') 
7736068b9f56
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46133
diff
changeset

480 
(simp_all, metis apply_rsp' list_eq_def) 
7736068b9f56
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46133
diff
changeset

481 
show "(list_all2 op \<approx> OOO op \<approx>) (map f xa) (map f' ya)" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46663
diff
changeset

482 
by (metis a b c list_eq_def pred_compI) 
46404
7736068b9f56
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46133
diff
changeset

483 
qed 
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

484 

46404
7736068b9f56
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46133
diff
changeset

485 
lemma map_prs2 [quot_preserve]: 
46441
992a1688303f
Generalize the compositional preservation theorems
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46416
diff
changeset

486 
shows "((abs_fset > rep_fset) > (map rep_fset \<circ> rep_fset) > abs_fset \<circ> map abs_fset) map = (id > rep_fset > abs_fset) map" 
992a1688303f
Generalize the compositional preservation theorems
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46416
diff
changeset

487 
by (auto simp add: fun_eq_iff) 
47308  488 
(simp only: map_map[symmetric] map_prs_aux[OF Quotient3_fset Quotient3_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

489 

9f8dcf6ef563
reorganisation of 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 
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

491 

9f8dcf6ef563
reorganisation of 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 
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

493 

9f8dcf6ef563
reorganisation of 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 
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

495 
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

496 
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

497 
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

498 

9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset

499 
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

500 
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

501 
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

502 

9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset

503 
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

504 
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

505 
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

506 

44204
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
41467
diff
changeset

507 
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

508 
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

509 
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

510 

9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset

511 
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

512 
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

513 
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

514 

9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset

515 
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

516 
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

517 
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

518 

9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset

519 
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

520 
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

521 
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

522 

9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset

523 
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

524 
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

525 
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

526 

9f8dcf6ef563
reorganisation of 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 

9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset

528 
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

529 

9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset

530 
lemma 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

531 
shows "x \<in> S \<longleftrightarrow> x \<in> fset S" 
40953  532 
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

533 

9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset

534 
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

535 
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

536 
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

537 

9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset

538 
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

539 
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

540 
by (simp add: in_fset) 
36280  541 

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

542 
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

543 
shows "S = T \<longleftrightarrow> (\<forall>x. (x \<in> S) = (x \<in> T))" 
40953  544 
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

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 
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

547 
shows "(\<forall>x. x \<notin> S) \<longleftrightarrow> S = {}" 
40953  548 
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

549 

9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset

550 

9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset

551 
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

552 

9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset

553 
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

554 
shows "x \<in> insert_fset y S \<longleftrightarrow> x = y \<or> x \<in> S" 
40953  555 
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

556 

9f8dcf6ef563
reorganisation of 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 
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

558 
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

559 
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

560 
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

561 

9f8dcf6ef563
reorganisation of 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 
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

563 
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

564 
by (descending) (auto) 
36280  565 

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

566 
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

567 
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

568 
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

569 
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

570 

9f8dcf6ef563
reorganisation of 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 
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

572 
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

573 
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

574 

9f8dcf6ef563
reorganisation of 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 
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

576 
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

577 
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

578 

9f8dcf6ef563
reorganisation of 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 
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

580 
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

581 
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

582 

9f8dcf6ef563
reorganisation of 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 
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

584 
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

585 
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

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 

9f8dcf6ef563
reorganisation of 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 
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

589 

9f8dcf6ef563
reorganisation of 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 
lemmas [simp] = 
45605  591 
sup_bot_left[where 'a="'a fset"] 
592 
sup_bot_right[where 'a="'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

593 

9f8dcf6ef563
reorganisation of 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 
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

595 
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

596 
by (lifting append.simps(2)) 
36280  597 

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

598 
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

599 
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

600 
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

601 

9f8dcf6ef563
reorganisation of 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 
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

603 
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

604 
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

605 

9f8dcf6ef563
reorganisation of 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 
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

607 
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

608 
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

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 

9f8dcf6ef563
reorganisation of 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 
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

612 

9f8dcf6ef563
reorganisation of 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 
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

614 
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

615 
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

616 

9f8dcf6ef563
reorganisation of 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 
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

618 
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

619 
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

620 

9f8dcf6ef563
reorganisation of 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 
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

622 
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

623 
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

624 

9f8dcf6ef563
reorganisation of 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 
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

626 
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

627 
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

628 

9f8dcf6ef563
reorganisation of 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 
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

630 
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

631 
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

632 
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

633 

9f8dcf6ef563
reorganisation of 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 
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

635 
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

636 
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

637 
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

638 

9f8dcf6ef563
reorganisation of 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 
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

641 

9f8dcf6ef563
reorganisation of 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 
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

643 
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

644 
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

645 

9f8dcf6ef563
reorganisation of 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 
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

647 
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

648 
by (descending) (simp) 
36280  649 

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

650 
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

651 
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

652 
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

653 

9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset

654 
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

655 
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

656 
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

657 

9f8dcf6ef563
reorganisation of 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 
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

660 

9f8dcf6ef563
reorganisation of 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 
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

662 
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

663 
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

664 

9f8dcf6ef563
reorganisation of 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 
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

666 
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

667 
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

668 

9f8dcf6ef563
reorganisation of 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 
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

670 
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

671 
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

672 

9f8dcf6ef563
reorganisation of 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 
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

674 
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

675 
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

676 

36280  677 

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

678 
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

679 

9f8dcf6ef563
reorganisation of 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 
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

681 
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

682 
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

683 

9f8dcf6ef563
reorganisation of 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 
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

685 
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

686 
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

687 
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

688 

9f8dcf6ef563
reorganisation of 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 
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

690 
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

691 
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

692 

9f8dcf6ef563
reorganisation of 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 
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

694 
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

695 
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

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 
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

698 
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

699 
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

700 

9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset

701 
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

702 
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

703 
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

704 

9f8dcf6ef563
reorganisation of 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 

9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset

706 
subsection {* map_fset *} 
36280  707 

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

708 
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

709 
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

710 
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

711 
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

712 

9f8dcf6ef563
reorganisation of 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 
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

714 
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

715 
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

716 

9f8dcf6ef563
reorganisation of 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 
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

718 
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

719 
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

720 

9f8dcf6ef563
reorganisation of 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 
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

722 
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

723 
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

724 

9f8dcf6ef563
reorganisation of 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 
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

727 

9f8dcf6ef563
reorganisation of 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 
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

729 
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

730 
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

731 

9f8dcf6ef563
reorganisation of 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 
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

733 
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

734 
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

735 

9f8dcf6ef563
reorganisation of 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 
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

737 
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

738 
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

739 

9f8dcf6ef563
reorganisation of 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 
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

741 
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

742 
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

743 

9f8dcf6ef563
reorganisation of 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 
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

745 
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

746 
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

747 

9f8dcf6ef563
reorganisation of 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 
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

749 
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

750 
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

751 

9f8dcf6ef563
reorganisation of 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 
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

753 
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

754 
by simp 
36280  755 

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

756 
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

757 
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

758 
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

759 
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

760 
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

761 

9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset

762 
lemma 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

763 
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

764 
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

765 

9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset

766 
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

767 
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

768 
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

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 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

771 
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

772 
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

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 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

775 
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

776 
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

777 
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

778 

9f8dcf6ef563
reorganisation of 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 
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

780 
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

781 
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

782 
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

783 

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

784 
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

785 
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

786 
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

787 
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

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_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

790 
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

791 
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

792 
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

793 

9f8dcf6ef563
reorganisation of 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 
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

795 
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

796 
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

797 
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

798 
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

799 

9f8dcf6ef563
reorganisation of 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 
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

801 
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

802 
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

803 
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

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_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

806 
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

807 
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

808 
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

809 

9f8dcf6ef563
reorganisation of 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 
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

811 
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

812 
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

813 
by (rule card_Diff1_le[OF finite_fset]) 
36280  814 

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

815 
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

816 
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

817 
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

818 
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

819 

9f8dcf6ef563
reorganisation of 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 
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

821 
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

822 
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

823 
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

824 

9f8dcf6ef563
reorganisation of 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 
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

826 
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

827 
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

828 
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

829 
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

830 
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

831 

9f8dcf6ef563
reorganisation of 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 
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

833 
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

834 
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

835 
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

836 
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

837 
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

838 

9f8dcf6ef563
reorganisation of 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 
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

840 
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

841 
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

842 
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

843 

9f8dcf6ef563
reorganisation of 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 

9f8dcf6ef563
reorganisation of 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 
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

846 

9f8dcf6ef563
reorganisation of 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 
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

848 
shows "concat_fset {} = {}" 
46416
5f5665a0b973
Make automatic derivation of raw/quotient types more greedy to allow descending and quot_lifted for compound quotients.
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46404
diff
changeset

849 
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

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 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

852 
shows "concat_fset (insert_fset x S) = x \<union> concat_fset S" 
46416
5f5665a0b973
Make automatic derivation of raw/quotient types more greedy to allow descending and quot_lifted for compound quotients.
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46404
diff
changeset

853 
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

854 

46441
992a1688303f
Generalize the compositional preservation theorems
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46416
diff
changeset

855 
lemma concat_union_fset [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

856 
shows "concat_fset (xs \<union> ys) = concat_fset xs \<union> concat_fset ys" 
46416
5f5665a0b973
Make automatic derivation of raw/quotient types more greedy to allow descending and quot_lifted for compound quotients.
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46404
diff
changeset

857 
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

858 

46404
7736068b9f56
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46133
diff
changeset

859 
lemma map_concat_fset: 
7736068b9f56
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46133
diff
changeset

860 
shows "map_fset f (concat_fset xs) = concat_fset (map_fset (map_fset f) xs)" 
7736068b9f56
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
46133
diff
changeset

861 
by (lifting map_concat) 
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

862 

9f8dcf6ef563
reorganisation of 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 
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

864 

9f8dcf6ef563
reorganisation of 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 
lemma subset_filter_fset: 
40961  866 
"filter_fset P xs \<subseteq> filter_fset Q xs = (\<forall> x. x \<in> xs \<longrightarrow> P x \<longrightarrow> Q x)" 
867 
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

868 

9f8dcf6ef563
reorganisation of 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 
lemma eq_filter_fset: 
40961  870 
"(filter_fset P xs = filter_fset Q xs) = (\<forall>x. x \<in> xs \<longrightarrow> P x = Q x)" 
871 
by descending auto 

36280  872 

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

873 
lemma psubset_filter_fset: 
40961  874 
"(\<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

875 
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

876 
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

877 

9f8dcf6ef563
reorganisation of 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 

9f8dcf6ef563
reorganisation of 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 
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

880 

9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset

881 
lemma fold_empty_fset: 
40961  882 
"fold_fset f {} = id" 
40962
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset

883 
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

884 

40961  885 
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

886 
(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

887 
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

888 

47092  889 
lemma remdups_removeAll: 
890 
"remdups (removeAll x xs) = remove1 x (remdups xs)" 

891 
by (induct xs) auto 

892 

893 
lemma member_commute_fold_once: 

894 
assumes "rsp_fold f" 

895 
and "x \<in> set xs" 

896 
shows "fold_once f xs = fold_once f (removeAll x xs) \<circ> f x" 

897 
proof  

898 
from assms have "fold f (remdups xs) = fold f (remove1 x (remdups xs)) \<circ> f x" 

899 
by (auto intro!: fold_remove1_split elim: rsp_foldE) 

900 
then show ?thesis using `rsp_fold f` by (simp add: fold_once_fold_remdups remdups_removeAll) 

901 
qed 

902 

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

903 
lemma in_commute_fold_fset: 
40962
069cd1c1f39b
more intimate definition of fold_list / fold_once in terms of fold
haftmann
parents:
40961
diff
changeset

904 
"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

905 
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

906 

9f8dcf6ef563
reorganisation of 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 
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

909 

9f8dcf6ef563
reorganisation of 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 
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

911 
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

912 
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

913 
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

914 
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

915 
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

916 
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

917 

9f8dcf6ef563
reorganisation of 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 
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

920 

41070  921 
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

922 
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

923 
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

924 
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

925 
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

926 

41070  927 
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

928 
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

929 
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

930 
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

931 
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

932 
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

933 

41070  934 
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

935 
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

936 
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

937 
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

938 
proof(induct S rule: fset_induct) 
41070  939 
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

940 
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

941 
next 
41070  942 
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

943 
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

944 
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

945 
by (cases "x \<in> S") (simp_all) 
36280  946 
qed 
947 

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

948 
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

949 
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

950 
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

951 
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

952 
proof (induct S) 
41070  953 
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

954 
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

955 
next 
41070  956 
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

957 
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

958 
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

959 
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

960 
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

961 
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

962 
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

963 
qed 
36280  964 

965 
lemma fset_raw_strong_cases: 

36465  966 
obtains "xs = []" 
40953  967 
 ys x where "\<not> List.member ys x" and "xs \<approx> x # ys" 
45129
1fce03e3e8ad
tuned proofs  eliminated vacuous "induct arbitrary: ..." situations;
wenzelm
parents:
44512
diff
changeset

968 
proof (induct xs) 
36465  969 
case Nil 
970 
then show thesis by simp 

971 
next 

972 
case (Cons a xs) 

40953  973 
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" 
974 
by (rule Cons(1)) 

975 
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

976 
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

977 
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

978 
by (metis List.set.simps(1) emptyE empty_subsetI) 
40953  979 
have "\<And>x ys. \<lbrakk>\<not> List.member ys x; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis" 
36465  980 
proof  
981 
fix x :: 'a 

982 
fix ys :: "'a list" 

40953  983 
assume d:"\<not> List.member ys x" 
36465  984 
assume e:"xs \<approx> x # ys" 
985 
show thesis 

986 
proof (cases "x = a") 

987 
assume h: "x = a" 

40953  988 
then have f: "\<not> List.member ys a" using d by simp 
36465  989 
have g: "a # xs \<approx> a # ys" using e h by auto 
990 
show thesis using b f g by simp 

991 
next 

992 
assume h: "x \<noteq> a" 

40953  993 
then have f: "\<not> List.member (a # ys) x" using d by auto 
36465  994 
have g: "a # xs \<approx> x # (a # ys)" using e h by auto 
40953  995 
show thesis using b f g by (simp del: List.member_def) 
36465  996 
qed 
997 
qed 

998 
then show thesis using a c by blast 

999 
qed 

36280  1000 

40030
9f8dcf6ef563
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Christian Urban <urbanc@in.tum.de>
parents:
39996
diff
changeset

1001 

9f8dcf6ef563
reorganisation of 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 
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

1003 
obtains "xs = {}" 
40953  1004 
 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

1005 
by (lifting fset_raw_strong_cases) 
36280  1006 

39996
c02078ff8691
FSet: definition changes propagated from Nominal and more use of 'descending' tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39995
diff
changeset

1007 

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

1008 
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

1009 
"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

1010 
(\<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

1011 
(\<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

1012 
(\<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

1013 
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

1014 
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

1015 
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

1016 
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

1017 
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

1018 
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

1019 
done 
36280  1020 

41070  1021 
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

1022 

41070  1023 
lemma fset_eqI: 
1024 
assumes "\<And>x. x \<in> fset A \<longleftrightarrow> x \<in> fset B" 

1025 
shows "A = B" 

1026 
using assms proof (induct A arbitrary: B) 

1027 
case empty then show ?case 

1028 
by (auto simp add: in_fset none_in_empty_fset [symmetric] sym) 

1029 
next 

1030 
case (insert x A) 

1031 
from insert.prems insert.hyps(1) have "\<And>z. z \<in> fset A \<longleftrightarrow> z \<in> fset (B  {x})" 

1032 
by (auto simp add: in_fset) 

1033 
then have "A = B  {x}" by (rule insert.hyps(2)) 

1034 
moreover with insert.prems [symmetric, of x] have "x \<in> B" by (simp add: in_fset) 

1035 
ultimately show ?case by (metis in_fset_mdef) 

1036 
qed 

36280  1037 

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

1038 
subsection {* alternate formulation with a different decomposition principle 
36280  1039 
and a proof of equivalence *} 
1040 

1041 
inductive 

40952  1042 
list_eq2 :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<approx>2 _") 
36280  1043 
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

1044 
"(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

1045 
 "[] \<approx>2 []" 
40952  1046 
 "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

1047 
 "(a # a # xs) \<approx>2 (a # xs)" 
40952  1048 
 "xs \<approx>2 ys \<Longrightarrow> (a # xs) \<approx>2 (a # ys)" 
1049 
 "xs1 \<approx>2 xs2 \<Longrightarrow> xs2 \<approx>2 xs3 \<Longrightarrow> xs1 \<approx>2 xs3" 

36280  1050 

1051 
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

1052 
shows "xs \<approx>2 xs" 
36280  1053 
by (induct xs) (auto intro: list_eq2.intros) 
1054 

1055 
lemma cons_delete_list_eq2: 

40953  1056 
shows "(a # (removeAll a A)) \<approx>2 (if List.member A a then A else a # A)" 
36280  1057 
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

1058 
apply (simp add: list_eq2_refl) 
40953  1059 
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

1060 
apply (simp_all) 
36280  1061 
apply (case_tac [!] "a = aa") 
1062 
apply (simp_all) 

40953  1063 
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

1064 
apply (auto)[2] 
36280  1065 
apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6)) 