equal
deleted
inserted
replaced
41 "memb x xs \<equiv> x \<in> set xs" |
41 "memb x xs \<equiv> x \<in> set xs" |
42 |
42 |
43 quotient_definition |
43 quotient_definition |
44 fin ("_ |\<in>| _" [50, 51] 50) |
44 fin ("_ |\<in>| _" [50, 51] 50) |
45 where |
45 where |
46 "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" |
46 "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb" |
47 is "memb" |
|
48 |
47 |
49 abbreviation |
48 abbreviation |
50 fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50) |
49 fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50) |
51 where |
50 where |
52 "a |\<notin>| S \<equiv> \<not>(a |\<in>| S)" |
51 "a |\<notin>| S \<equiv> \<not>(a |\<in>| S)" |
61 |
60 |
62 lemma cons_rsp[quot_respect]: |
61 lemma cons_rsp[quot_respect]: |
63 shows "(op = ===> op \<approx> ===> op \<approx>) op # op #" |
62 shows "(op = ===> op \<approx> ===> op \<approx>) op # op #" |
64 by simp |
63 by simp |
65 |
64 |
66 section {* Augmenting a set -- @{const finsert} *} |
65 section {* Augmenting an fset -- @{const finsert} *} |
67 |
66 |
68 lemma nil_not_cons: |
67 lemma nil_not_cons: |
69 shows |
68 shows |
70 "\<not>[] \<approx> x # xs" |
69 "\<not>[] \<approx> x # xs" |
71 "\<not>x # xs \<approx> []" |
70 "\<not>x # xs \<approx> []" |