equal
deleted
inserted
replaced
24 |
24 |
25 quotient_type |
25 quotient_type |
26 'a fset = "'a list" / "list_eq" |
26 'a fset = "'a list" / "list_eq" |
27 by (rule list_eq_equivp) |
27 by (rule list_eq_equivp) |
28 |
28 |
29 text {* Raw definitions *} |
29 text {* Raw definitions of membership, sublist, cardinality, |
|
30 intersection |
|
31 *} |
30 |
32 |
31 definition |
33 definition |
32 memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" |
34 memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" |
33 where |
35 where |
34 "memb x xs \<equiv> x \<in> set xs" |
36 "memb x xs \<equiv> x \<in> set xs" |
40 |
42 |
41 fun |
43 fun |
42 fcard_raw :: "'a list \<Rightarrow> nat" |
44 fcard_raw :: "'a list \<Rightarrow> nat" |
43 where |
45 where |
44 fcard_raw_nil: "fcard_raw [] = 0" |
46 fcard_raw_nil: "fcard_raw [] = 0" |
45 | fcard_raw_cons: "fcard_raw (x # xs) = (if memb x xs then fcard_raw xs else Suc (fcard_raw xs))" |
47 | fcard_raw_cons: "fcard_raw (x # xs) = |
|
48 (if memb x xs then fcard_raw xs else Suc (fcard_raw xs))" |
46 |
49 |
47 primrec |
50 primrec |
48 finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
51 finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
49 where |
52 where |
50 "finter_raw [] l = []" |
53 "finter_raw [] l = []" |
51 | "finter_raw (h # t) l = |
54 | "finter_raw (h # t) l = |
52 (if memb h l then h # (finter_raw t l) else finter_raw t l)" |
55 (if memb h l then h # (finter_raw t l) else finter_raw t l)" |
53 |
56 |
54 primrec |
57 primrec |
55 delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list" |
58 delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list" |
56 where |
59 where |
57 "delete_raw [] x = []" |
60 "delete_raw [] x = []" |
58 | "delete_raw (a # xs) x = (if (a = x) then delete_raw xs x else a # (delete_raw xs x))" |
61 | "delete_raw (a # xs) x = |
|
62 (if (a = x) then delete_raw xs x else a # (delete_raw xs x))" |
59 |
63 |
60 primrec |
64 primrec |
61 fminus_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
65 fminus_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
62 where |
66 where |
63 "fminus_raw l [] = l" |
67 "fminus_raw l [] = l" |