equal
deleted
inserted
replaced
7 |
7 |
8 theory FSet |
8 theory FSet |
9 imports Quotient_List |
9 imports Quotient_List |
10 begin |
10 begin |
11 |
11 |
12 text {* Definiton of the equivalence relation over lists *} |
12 text {* Definition of the equivalence relation over lists *} |
13 |
13 |
14 fun |
14 fun |
15 list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50) |
15 list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50) |
16 where |
16 where |
17 "list_eq xs ys = (set xs = set ys)" |
17 "list_eq xs ys = (set xs = set ys)" |
521 section {* Lifted theorems *} |
521 section {* Lifted theorems *} |
522 |
522 |
523 subsection {* fset *} |
523 subsection {* fset *} |
524 |
524 |
525 lemma fset_simps [simp]: |
525 lemma fset_simps [simp]: |
526 "fset {||} = ({} :: 'a set)" |
526 shows "fset {||} = {}" |
527 "fset (insert_fset (x :: 'a) S) = insert x (fset S)" |
527 and "fset (insert_fset x S) = insert x (fset S)" |
528 by (lifting set.simps) |
528 by (descending, simp)+ |
529 |
529 |
530 lemma finite_fset [simp]: |
530 lemma finite_fset [simp]: |
531 shows "finite (fset S)" |
531 shows "finite (fset S)" |
532 by (descending) (simp) |
532 by (descending) (simp) |
533 |
533 |