40 FUNION :: "FUNION :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
40 FUNION :: "FUNION :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
41 where |
41 where |
42 "op @" |
42 "op @" |
43 |
43 |
44 fun |
44 fun |
45 membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infix "memb" 100) |
|
46 where |
|
47 m1: "(x memb []) = False" |
|
48 | m2: "(x memb (y#xs)) = ((x=y) \<or> (x memb xs))" |
|
49 |
|
50 fun |
|
51 card1 :: "'a list \<Rightarrow> nat" |
45 card1 :: "'a list \<Rightarrow> nat" |
52 where |
46 where |
53 card1_nil: "(card1 []) = 0" |
47 card1_nil: "(card1 []) = 0" |
54 | card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))" |
48 | card1_cons: "(card1 (x # xs)) = (if (x mem xs) then (card1 xs) else (Suc (card1 xs)))" |
55 |
49 |
56 quotient_def |
50 quotient_def |
57 CARD :: "CARD :: 'a fset \<Rightarrow> nat" |
51 CARD :: "CARD :: 'a fset \<Rightarrow> nat" |
58 where |
52 where |
59 "card1" |
53 "card1" |
70 by (induct a) auto |
64 by (induct a) auto |
71 |
65 |
72 lemma not_mem_card1: |
66 lemma not_mem_card1: |
73 fixes x :: "'a" |
67 fixes x :: "'a" |
74 fixes xs :: "'a list" |
68 fixes xs :: "'a list" |
75 shows "(~(x memb xs)) = (card1 (x # xs) = Suc (card1 xs))" |
69 shows "(~(x mem xs)) = (card1 (x # xs) = Suc (card1 xs))" |
76 by auto |
70 by auto |
77 |
71 |
78 lemma mem_cons: |
72 lemma mem_cons: |
79 fixes x :: "'a" |
73 fixes x :: "'a" |
80 fixes xs :: "'a list" |
74 fixes xs :: "'a list" |
81 assumes a : "x memb xs" |
75 assumes a : "x mem xs" |
82 shows "x # xs \<approx> xs" |
76 shows "x # xs \<approx> xs" |
83 using a by (induct xs) (auto intro: list_eq.intros ) |
77 using a by (induct xs) (auto intro: list_eq.intros ) |
84 |
78 |
85 lemma card1_suc: |
79 lemma card1_suc: |
86 fixes xs :: "'a list" |
80 fixes xs :: "'a list" |
87 fixes n :: "nat" |
81 fixes n :: "nat" |
88 assumes c: "card1 xs = Suc n" |
82 assumes c: "card1 xs = Suc n" |
89 shows "\<exists>a ys. ~(a memb ys) \<and> xs \<approx> (a # ys)" |
83 shows "\<exists>a ys. ~(a mem ys) \<and> xs \<approx> (a # ys)" |
90 using c |
84 using c |
91 apply(induct xs) |
85 apply(induct xs) |
92 apply (metis Suc_neq_Zero card1_0) |
86 apply (metis Suc_neq_Zero card1_0) |
93 apply (metis QUOT_TYPE_I_fset.R_trans card1_cons list_eq_refl mem_cons) |
87 apply (metis QUOT_TYPE_I_fset.R_trans card1_cons list_eq_refl mem_cons) |
94 done |
88 done |
103 where |
97 where |
104 "fold1 f (g :: 'a \<Rightarrow> 'b) (z :: 'b) [] = z" |
98 "fold1 f (g :: 'a \<Rightarrow> 'b) (z :: 'b) [] = z" |
105 | "fold1 f g z (a # A) = |
99 | "fold1 f g z (a # A) = |
106 (if rsp_fold f |
100 (if rsp_fold f |
107 then ( |
101 then ( |
108 if (a memb A) then (fold1 f g z A) else (f (g a) (fold1 f g z A)) |
102 if (a mem A) then (fold1 f g z A) else (f (g a) (fold1 f g z A)) |
109 ) else z)" |
103 ) else z)" |
110 |
104 |
111 lemma fs1_strong_cases: |
105 lemma fs1_strong_cases: |
112 fixes X :: "'a list" |
106 fixes X :: "'a list" |
113 shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a memb Y) \<and> (X \<approx> a # Y)))" |
107 shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a mem Y) \<and> (X \<approx> a # Y)))" |
114 apply (induct X) |
108 apply (induct X) |
115 apply (simp) |
109 apply (simp) |
116 apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons m1) |
110 apply (metis List.member.simps(1) QUOT_TYPE_I_fset.R_trans list_eq_refl mem_cons) |
117 done |
111 done |
118 |
112 |
119 quotient_def |
113 quotient_def |
120 IN :: "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" |
114 IN :: "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" |
121 where |
115 where |
122 "membship" |
116 "op mem" |
123 |
117 |
124 quotient_def |
118 quotient_def |
125 FOLD :: "FOLD :: ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a" |
119 FOLD :: "FOLD :: ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a" |
126 where |
120 where |
127 "fold1" |
121 "fold1" |
129 quotient_def |
123 quotient_def |
130 fmap::"fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
124 fmap::"fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
131 where |
125 where |
132 "map" |
126 "map" |
133 |
127 |
134 lemma memb_rsp: |
128 lemma mem_rsp: |
135 fixes z |
129 fixes z |
136 assumes a: "x \<approx> y" |
130 assumes a: "x \<approx> y" |
137 shows "(z memb x) = (z memb y)" |
131 shows "(z mem x) = (z mem y)" |
138 using a by induct auto |
132 using a by induct auto |
139 |
133 |
140 lemma ho_memb_rsp[quot_respect]: |
134 lemma ho_memb_rsp[quot_respect]: |
141 "(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)" |
135 "(op = ===> (op \<approx> ===> op =)) (op mem) (op mem)" |
142 by (simp add: memb_rsp) |
136 by (simp add: mem_rsp) |
143 |
137 |
144 lemma card1_rsp: |
138 lemma card1_rsp: |
145 fixes a b :: "'a list" |
139 fixes a b :: "'a list" |
146 assumes e: "a \<approx> b" |
140 assumes e: "a \<approx> b" |
147 shows "card1 a = card1 b" |
141 shows "card1 a = card1 b" |
148 using e by induct (simp_all add:memb_rsp) |
142 using e by induct (simp_all add: mem_rsp) |
149 |
143 |
150 lemma ho_card1_rsp[quot_respect]: |
144 lemma ho_card1_rsp[quot_respect]: |
151 "(op \<approx> ===> op =) card1 card1" |
145 "(op \<approx> ===> op =) card1 card1" |
152 by (simp add: card1_rsp) |
146 by (simp add: card1_rsp) |
153 |
147 |
205 prefer 2 |
199 prefer 2 |
206 apply (erule_tac list_eq.induct) |
200 apply (erule_tac list_eq.induct) |
207 apply (simp_all) |
201 apply (simp_all) |
208 apply (erule_tac list_eq.induct) |
202 apply (erule_tac list_eq.induct) |
209 apply (simp_all) |
203 apply (simp_all) |
210 apply (auto simp add: memb_rsp rsp_fold_def) |
204 apply (auto simp add: mem_rsp rsp_fold_def) |
211 done |
205 done |
212 |
206 |
213 lemma list_equiv_rsp[quot_respect]: |
207 lemma list_equiv_rsp[quot_respect]: |
214 shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>" |
208 shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>" |
215 by (auto intro: list_eq.intros) |
209 by (auto intro: list_eq.intros) |
216 |
210 |
217 |
|
218 lemma "IN x EMPTY = False" |
211 lemma "IN x EMPTY = False" |
219 apply(lifting m1) |
212 apply(lifting member.simps(1)) |
220 done |
213 done |
221 |
214 |
222 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)" |
215 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)" |
223 by (lifting m2) |
216 by (lifting member.simps(2)) |
224 |
217 |
225 lemma "INSERT a (INSERT a x) = INSERT a x" |
218 lemma "INSERT a (INSERT a x) = INSERT a x" |
226 apply (lifting list_eq.intros(4)) |
219 apply (lifting list_eq.intros(4)) |
227 done |
220 done |
228 |
221 |