equal
deleted
inserted
replaced
82 assumes c: "card1 xs = Suc n" |
82 assumes c: "card1 xs = Suc n" |
83 shows "\<exists>a ys. ~(a mem ys) \<and> xs \<approx> (a # ys)" |
83 shows "\<exists>a ys. ~(a mem ys) \<and> xs \<approx> (a # ys)" |
84 using c |
84 using c |
85 apply(induct xs) |
85 apply(induct xs) |
86 apply (metis Suc_neq_Zero card1_0) |
86 apply (metis Suc_neq_Zero card1_0) |
87 apply (metis QUOT_TYPE_I_fset.R_trans card1_cons list_eq_refl mem_cons) |
87 apply (metis FSet.card1_cons list_eq.intros(6) list_eq_refl mem_cons) |
88 done |
88 done |
89 |
89 |
90 definition |
90 definition |
91 rsp_fold |
91 rsp_fold |
92 where |
92 where |
105 lemma fs1_strong_cases: |
105 lemma fs1_strong_cases: |
106 fixes X :: "'a list" |
106 fixes X :: "'a list" |
107 shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a mem Y) \<and> (X \<approx> a # Y)))" |
107 shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a mem Y) \<and> (X \<approx> a # Y)))" |
108 apply (induct X) |
108 apply (induct X) |
109 apply (simp) |
109 apply (simp) |
110 apply (metis List.member.simps(1) QUOT_TYPE_I_fset.R_trans list_eq_refl mem_cons) |
110 apply (metis List.member.simps(1) list_eq.intros(6) list_eq_refl mem_cons) |
111 done |
111 done |
112 |
112 |
113 quotient_def |
113 quotient_def |
114 IN :: "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" |
114 IN :: "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" |
115 where |
115 where |