equal
deleted
inserted
replaced
20 shows "equivp list_eq" |
20 shows "equivp list_eq" |
21 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def |
21 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def |
22 apply(auto intro: list_eq.intros list_eq_refl) |
22 apply(auto intro: list_eq.intros list_eq_refl) |
23 done |
23 done |
24 |
24 |
25 quotient fset = "'a list" / "list_eq" |
25 quotient_type |
26 apply(rule equivp_list_eq) |
26 fset = "'a list" / "list_eq" |
27 done |
27 by (rule equivp_list_eq) |
28 |
28 |
29 quotient_def |
29 quotient_def |
30 "EMPTY :: 'a fset" |
30 "EMPTY :: 'a fset" |
31 as |
31 as |
32 "[]::'a list" |
32 "[]::'a list" |
269 |
269 |
270 lemma "P (x :: 'a fset) ([] :: 'c list) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (e # t)) \<Longrightarrow> P x l" |
270 lemma "P (x :: 'a fset) ([] :: 'c list) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (e # t)) \<Longrightarrow> P x l" |
271 apply (lifting list_induct_part) |
271 apply (lifting list_induct_part) |
272 done |
272 done |
273 |
273 |
274 quotient fset2 = "'a list" / "list_eq" |
274 quotient_type fset2 = "'a list" / "list_eq" |
275 by (rule equivp_list_eq) |
275 by (rule equivp_list_eq) |
276 |
276 |
277 quotient_def |
277 quotient_def |
278 "EMPTY2 :: 'a fset2" |
278 "EMPTY2 :: 'a fset2" |
279 as |
279 as |