13 where |
13 where |
14 "list_eq xs ys = (\<forall>x. x \<in> set xs \<longleftrightarrow> x \<in> set ys)" |
14 "list_eq xs ys = (\<forall>x. x \<in> set xs \<longleftrightarrow> x \<in> set ys)" |
15 |
15 |
16 lemma list_eq_equivp: |
16 lemma list_eq_equivp: |
17 shows "equivp list_eq" |
17 shows "equivp list_eq" |
18 unfolding equivp_reflp_symp_transp |
18 unfolding equivp_reflp_symp_transp |
19 unfolding reflp_def symp_def transp_def |
19 unfolding reflp_def symp_def transp_def |
20 by auto |
20 by auto |
|
21 |
|
22 definition |
|
23 memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" |
|
24 where |
|
25 "memb x xs \<equiv> x \<in> set xs" |
|
26 |
|
27 definition |
|
28 sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
|
29 where |
|
30 "sub_list xs ys \<equiv> (\<forall>x. x \<in> set xs \<longrightarrow> x \<in> set ys)" |
|
31 |
|
32 lemma sub_list_cons: |
|
33 "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)" |
|
34 by (auto simp add: memb_def sub_list_def) |
|
35 |
|
36 lemma nil_not_cons: |
|
37 shows "\<not> ([] \<approx> x # xs)" |
|
38 and "\<not> (x # xs \<approx> [])" |
|
39 by auto |
|
40 |
|
41 lemma sub_list_rsp1: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list xs zs = sub_list ys zs" |
|
42 by (simp add: sub_list_def) |
|
43 |
|
44 lemma sub_list_rsp2: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list zs xs = sub_list zs ys" |
|
45 by (simp add: sub_list_def) |
|
46 |
|
47 lemma [quot_respect]: |
|
48 "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list" |
|
49 by (auto simp only: fun_rel_def sub_list_rsp1 sub_list_rsp2) |
21 |
50 |
22 quotient_type |
51 quotient_type |
23 'a fset = "'a list" / "list_eq" |
52 'a fset = "'a list" / "list_eq" |
24 by (rule list_eq_equivp) |
53 by (rule list_eq_equivp) |
25 |
54 |
40 |
69 |
41 translations |
70 translations |
42 "{|x, xs|}" == "CONST finsert x {|xs|}" |
71 "{|x, xs|}" == "CONST finsert x {|xs|}" |
43 "{|x|}" == "CONST finsert x {||}" |
72 "{|x|}" == "CONST finsert x {||}" |
44 |
73 |
45 definition |
|
46 memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" |
|
47 where |
|
48 "memb x xs \<equiv> x \<in> set xs" |
|
49 |
|
50 quotient_definition |
74 quotient_definition |
51 fin ("_ |\<in>| _" [50, 51] 50) |
75 fin ("_ |\<in>| _" [50, 51] 50) |
52 where |
76 where |
53 "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb" |
77 "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb" |
54 |
78 |
68 lemma cons_rsp[quot_respect]: |
92 lemma cons_rsp[quot_respect]: |
69 shows "(op = ===> op \<approx> ===> op \<approx>) op # op #" |
93 shows "(op = ===> op \<approx> ===> op \<approx>) op # op #" |
70 by simp |
94 by simp |
71 |
95 |
72 section {* Augmenting an fset -- @{const finsert} *} |
96 section {* Augmenting an fset -- @{const finsert} *} |
73 |
|
74 lemma nil_not_cons: |
|
75 shows "\<not> ([] \<approx> x # xs)" |
|
76 and "\<not> (x # xs \<approx> [])" |
|
77 by auto |
|
78 |
97 |
79 lemma not_memb_nil: |
98 lemma not_memb_nil: |
80 shows "\<not> memb x []" |
99 shows "\<not> memb x []" |
81 by (simp add: memb_def) |
100 by (simp add: memb_def) |
82 |
101 |
485 shows "list_eq2 l r" |
504 shows "list_eq2 l r" |
486 using a b |
505 using a b |
487 proof (induct n arbitrary: l r) |
506 proof (induct n arbitrary: l r) |
488 case 0 |
507 case 0 |
489 have "fcard_raw l = 0" by fact |
508 have "fcard_raw l = 0" by fact |
490 then have "\<forall>x. \<not> memb x l" using mem_card_not_0[of _ l] by auto |
509 then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto |
491 then have z: "l = []" using no_memb_nil by auto |
510 then have z: "l = []" using no_memb_nil by auto |
492 then have "r = []" sorry |
511 then have "r = []" sorry |
493 then show ?case using z list_eq2_refl by simp |
512 then show ?case using z list_eq2_refl by simp |
494 next |
513 next |
495 case (Suc m) |
514 case (Suc m) |