27 definition |
27 definition |
28 sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
28 sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
29 where |
29 where |
30 "sub_list xs ys \<equiv> (\<forall>x. x \<in> set xs \<longrightarrow> x \<in> set ys)" |
30 "sub_list xs ys \<equiv> (\<forall>x. x \<in> set xs \<longrightarrow> x \<in> set ys)" |
31 |
31 |
|
32 quotient_type |
|
33 'a fset = "'a list" / "list_eq" |
|
34 by (rule list_eq_equivp) |
|
35 |
|
36 section {* Empty fset, Finsert and Membership *} |
|
37 |
|
38 quotient_definition |
|
39 fempty ("{||}") |
|
40 where |
|
41 "fempty :: 'a fset" |
|
42 is "[]::'a list" |
|
43 |
|
44 quotient_definition |
|
45 "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
|
46 is "op #" |
|
47 |
|
48 syntax |
|
49 "@Finset" :: "args => 'a fset" ("{|(_)|}") |
|
50 |
|
51 translations |
|
52 "{|x, xs|}" == "CONST finsert x {|xs|}" |
|
53 "{|x|}" == "CONST finsert x {||}" |
|
54 |
|
55 quotient_definition |
|
56 fin ("_ |\<in>| _" [50, 51] 50) |
|
57 where |
|
58 "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb" |
|
59 |
|
60 abbreviation |
|
61 fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50) |
|
62 where |
|
63 "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)" |
|
64 |
|
65 lemma memb_rsp[quot_respect]: |
|
66 shows "(op = ===> op \<approx> ===> op =) memb memb" |
|
67 by (auto simp add: memb_def) |
|
68 |
|
69 lemma nil_rsp[quot_respect]: |
|
70 shows "[] \<approx> []" |
|
71 by simp |
|
72 |
|
73 lemma cons_rsp[quot_respect]: |
|
74 shows "(op = ===> op \<approx> ===> op \<approx>) op # op #" |
|
75 by simp |
|
76 |
|
77 section {* Augmenting an fset -- @{const finsert} *} |
|
78 |
|
79 lemma nil_not_cons: |
|
80 shows "\<not> ([] \<approx> x # xs)" |
|
81 and "\<not> (x # xs \<approx> [])" |
|
82 by auto |
|
83 |
|
84 lemma not_memb_nil: |
|
85 shows "\<not> memb x []" |
|
86 by (simp add: memb_def) |
|
87 |
|
88 lemma no_memb_nil: |
|
89 "(\<forall>x. \<not> memb x xs) = (xs = [])" |
|
90 by (simp add: memb_def) |
|
91 |
|
92 lemma none_memb_nil: |
|
93 "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])" |
|
94 by (simp add: memb_def) |
|
95 |
|
96 lemma memb_cons_iff: |
|
97 shows "memb x (y # xs) = (x = y \<or> memb x xs)" |
|
98 by (induct xs) (auto simp add: memb_def) |
|
99 |
|
100 lemma memb_consI1: |
|
101 shows "memb x (x # xs)" |
|
102 by (simp add: memb_def) |
|
103 |
|
104 lemma memb_consI2: |
|
105 shows "memb x xs \<Longrightarrow> memb x (y # xs)" |
|
106 by (simp add: memb_def) |
|
107 |
|
108 lemma memb_absorb: |
|
109 shows "memb x xs \<Longrightarrow> x # xs \<approx> xs" |
|
110 by (induct xs) (auto simp add: memb_def id_simps) |
|
111 |
|
112 section {* Singletons *} |
|
113 |
|
114 lemma singleton_list_eq: |
|
115 shows "[x] \<approx> [y] \<longleftrightarrow> x = y" |
|
116 by (simp add: id_simps) auto |
|
117 |
|
118 section {* Unions *} |
|
119 |
|
120 quotient_definition |
|
121 funion (infixl "|\<union>|" 65) |
|
122 where |
|
123 "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
|
124 is |
|
125 "op @" |
|
126 |
|
127 section {* sub_list *} |
|
128 |
32 lemma sub_list_cons: |
129 lemma sub_list_cons: |
33 "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)" |
130 "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)" |
34 by (auto simp add: memb_def sub_list_def) |
131 by (auto simp add: memb_def sub_list_def) |
35 |
132 |
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" |
133 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) |
134 by (simp add: sub_list_def) |
43 |
135 |
44 lemma sub_list_rsp2: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list zs xs = sub_list zs ys" |
136 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) |
137 by (simp add: sub_list_def) |
46 |
138 |
47 lemma [quot_respect]: |
139 lemma [quot_respect]: |
48 "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list" |
140 "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list" |
49 by (auto simp only: fun_rel_def sub_list_rsp1 sub_list_rsp2) |
141 by (auto simp only: fun_rel_def sub_list_rsp1 sub_list_rsp2) |
50 |
|
51 quotient_type |
|
52 'a fset = "'a list" / "list_eq" |
|
53 by (rule list_eq_equivp) |
|
54 |
|
55 section {* Empty fset, Finsert and Membership *} |
|
56 |
|
57 quotient_definition |
|
58 fempty ("{||}") |
|
59 where |
|
60 "fempty :: 'a fset" |
|
61 is "[]::'a list" |
|
62 |
|
63 quotient_definition |
|
64 "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
|
65 is "op #" |
|
66 |
|
67 syntax |
|
68 "@Finset" :: "args => 'a fset" ("{|(_)|}") |
|
69 |
|
70 translations |
|
71 "{|x, xs|}" == "CONST finsert x {|xs|}" |
|
72 "{|x|}" == "CONST finsert x {||}" |
|
73 |
|
74 quotient_definition |
|
75 fin ("_ |\<in>| _" [50, 51] 50) |
|
76 where |
|
77 "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb" |
|
78 |
|
79 abbreviation |
|
80 fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50) |
|
81 where |
|
82 "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)" |
|
83 |
|
84 lemma memb_rsp[quot_respect]: |
|
85 shows "(op = ===> op \<approx> ===> op =) memb memb" |
|
86 by (auto simp add: memb_def) |
|
87 |
|
88 lemma nil_rsp[quot_respect]: |
|
89 shows "[] \<approx> []" |
|
90 by simp |
|
91 |
|
92 lemma cons_rsp[quot_respect]: |
|
93 shows "(op = ===> op \<approx> ===> op \<approx>) op # op #" |
|
94 by simp |
|
95 |
|
96 section {* Augmenting an fset -- @{const finsert} *} |
|
97 |
|
98 lemma not_memb_nil: |
|
99 shows "\<not> memb x []" |
|
100 by (simp add: memb_def) |
|
101 |
|
102 lemma no_memb_nil: |
|
103 "(\<forall>x. \<not> memb x xs) = (xs = [])" |
|
104 by (simp add: memb_def) |
|
105 |
|
106 lemma none_memb_nil: |
|
107 "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])" |
|
108 by (simp add: memb_def) |
|
109 |
|
110 lemma memb_cons_iff: |
|
111 shows "memb x (y # xs) = (x = y \<or> memb x xs)" |
|
112 by (induct xs) (auto simp add: memb_def) |
|
113 |
|
114 lemma memb_consI1: |
|
115 shows "memb x (x # xs)" |
|
116 by (simp add: memb_def) |
|
117 |
|
118 lemma memb_consI2: |
|
119 shows "memb x xs \<Longrightarrow> memb x (y # xs)" |
|
120 by (simp add: memb_def) |
|
121 |
|
122 lemma memb_absorb: |
|
123 shows "memb x xs \<Longrightarrow> x # xs \<approx> xs" |
|
124 by (induct xs) (auto simp add: memb_def id_simps) |
|
125 |
|
126 section {* Singletons *} |
|
127 |
|
128 lemma singleton_list_eq: |
|
129 shows "[x] \<approx> [y] \<longleftrightarrow> x = y" |
|
130 by (simp add: id_simps) auto |
|
131 |
|
132 section {* Unions *} |
|
133 |
|
134 quotient_definition |
|
135 funion (infixl "|\<union>|" 65) |
|
136 where |
|
137 "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
|
138 is |
|
139 "op @" |
|
140 |
142 |
141 section {* Cardinality of finite sets *} |
143 section {* Cardinality of finite sets *} |
142 |
144 |
143 fun |
145 fun |
144 fcard_raw :: "'a list \<Rightarrow> nat" |
146 fcard_raw :: "'a list \<Rightarrow> nat" |