38 |
38 |
39 lemma sub_list_rsp2: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list zs xs = sub_list zs ys" |
39 lemma sub_list_rsp2: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list zs xs = sub_list zs ys" |
40 by (simp add: sub_list_def) |
40 by (simp add: sub_list_def) |
41 |
41 |
42 lemma [quot_respect]: |
42 lemma [quot_respect]: |
43 "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list" |
43 shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list" |
44 by (auto simp only: fun_rel_def sub_list_rsp1 sub_list_rsp2) |
44 by (auto simp only: fun_rel_def sub_list_rsp1 sub_list_rsp2) |
|
45 |
|
46 lemma [quot_respect]: |
|
47 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @" |
|
48 by auto |
45 |
49 |
46 lemma sub_list_not_eq: |
50 lemma sub_list_not_eq: |
47 "(sub_list x y \<and> \<not> list_eq x y) = (sub_list x y \<and> \<not> sub_list y x)" |
51 "(sub_list x y \<and> \<not> list_eq x y) = (sub_list x y \<and> \<not> sub_list y x)" |
48 by (auto simp add: sub_list_def) |
52 by (auto simp add: sub_list_def) |
49 |
53 |
100 fix x y z :: "'a fset" |
104 fix x y z :: "'a fset" |
101 assume a: "x |\<subseteq>| y" |
105 assume a: "x |\<subseteq>| y" |
102 assume b: "y |\<subseteq>| z" |
106 assume b: "y |\<subseteq>| z" |
103 show "x |\<subseteq>| z" using a b by (lifting sub_list_trans) |
107 show "x |\<subseteq>| z" using a b by (lifting sub_list_trans) |
104 qed |
108 qed |
105 |
109 end |
|
110 |
|
111 lemma sub_list_append_left: |
|
112 "sub_list x (x @ y)" |
|
113 by (simp add: sub_list_def) |
|
114 |
|
115 lemma sub_list_append_right: |
|
116 "sub_list y (x @ y)" |
|
117 by (simp add: sub_list_def) |
|
118 |
|
119 lemma sub_list_list_eq: |
|
120 "sub_list x y \<Longrightarrow> sub_list y x \<Longrightarrow> list_eq x y" |
|
121 unfolding sub_list_def list_eq.simps by blast |
|
122 |
|
123 lemma sub_list_append: |
|
124 "sub_list y x \<Longrightarrow> sub_list z x \<Longrightarrow> sub_list (y @ z) x" |
|
125 unfolding sub_list_def by auto |
|
126 |
|
127 instantiation fset :: (type) "semilattice_sup" |
|
128 begin |
|
129 |
|
130 quotient_definition |
|
131 "sup \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)" |
|
132 is |
|
133 "(op @) \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)" |
|
134 |
|
135 abbreviation |
|
136 funion (infixl "|\<union>|" 65) |
|
137 where |
|
138 "xs |\<union>| ys \<equiv> sup (xs :: 'a fset) ys" |
|
139 |
|
140 instance |
|
141 proof |
|
142 fix x y :: "'a fset" |
|
143 show "x |\<subseteq>| x |\<union>| y" by (lifting sub_list_append_left) |
|
144 show "y |\<subseteq>| x |\<union>| y" by (lifting sub_list_append_right) |
|
145 next |
|
146 fix x y :: "'a fset" |
|
147 assume a: "x |\<subseteq>| y" |
|
148 assume b: "y |\<subseteq>| x" |
|
149 show "x = y" using a b by (lifting sub_list_list_eq) |
|
150 next |
|
151 fix x y z :: "'a fset" |
|
152 assume a: "y |\<subseteq>| x" |
|
153 assume b: "z |\<subseteq>| x" |
|
154 show "y |\<union>| z |\<subseteq>| x" using a b by (lifting sub_list_append) |
|
155 qed |
106 end |
156 end |
107 |
157 |
108 section {* Empty fset, Finsert and Membership *} |
158 section {* Empty fset, Finsert and Membership *} |
109 |
159 |
110 quotient_definition |
160 quotient_definition |
178 section {* Singletons *} |
228 section {* Singletons *} |
179 |
229 |
180 lemma singleton_list_eq: |
230 lemma singleton_list_eq: |
181 shows "[x] \<approx> [y] \<longleftrightarrow> x = y" |
231 shows "[x] \<approx> [y] \<longleftrightarrow> x = y" |
182 by (simp add: id_simps) auto |
232 by (simp add: id_simps) auto |
183 |
|
184 section {* Unions *} |
|
185 |
|
186 quotient_definition |
|
187 funion (infixl "|\<union>|" 65) |
|
188 where |
|
189 "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
|
190 is |
|
191 "op @" |
|
192 |
233 |
193 section {* sub_list *} |
234 section {* sub_list *} |
194 |
235 |
195 lemma sub_list_cons: |
236 lemma sub_list_cons: |
196 "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)" |
237 "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)" |
495 |
536 |
496 lemma funion_sym_pre: |
537 lemma funion_sym_pre: |
497 "xs @ ys \<approx> ys @ xs" |
538 "xs @ ys \<approx> ys @ xs" |
498 by auto |
539 by auto |
499 |
540 |
500 lemma append_rsp[quot_respect]: |
|
501 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @" |
|
502 by auto |
|
503 |
|
504 lemma set_cong: |
541 lemma set_cong: |
505 shows "(set x = set y) = (x \<approx> y)" |
542 shows "(set x = set y) = (x \<approx> y)" |
506 by auto |
543 by auto |
507 |
544 |
508 lemma inj_map_eq_iff: |
545 lemma inj_map_eq_iff: |
544 apply (case_tac [!] "a = aa") |
581 apply (case_tac [!] "a = aa") |
545 apply (simp_all add: delete_raw.simps) |
582 apply (simp_all add: delete_raw.simps) |
546 apply (case_tac "memb a A") |
583 apply (case_tac "memb a A") |
547 apply (auto simp add: memb_def)[2] |
584 apply (auto simp add: memb_def)[2] |
548 apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6)) |
585 apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6)) |
549 apply (metis delete_raw.simps(2) list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6)) |
586 apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6)) |
550 apply (auto simp add: list_eq2_refl not_memb_delete_raw_ident) |
587 apply (auto simp add: list_eq2_refl not_memb_delete_raw_ident) |
551 done |
588 done |
552 |
589 |
553 lemma memb_delete_list_eq2: |
590 lemma memb_delete_list_eq2: |
554 assumes a: "memb e r" |
591 assumes a: "memb e r" |