77 where |
77 where |
78 "delete_raw [] x = []" |
78 "delete_raw [] x = []" |
79 | "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))" |
79 | "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))" |
80 |
80 |
81 lemma mem_delete_raw: |
81 lemma mem_delete_raw: |
82 "x mem (delete_raw A a) = (x mem A \<and> \<not>(x = a))" |
82 "x \<in> set (delete_raw A a) = (x \<in> set A \<and> \<not>(x = a))" |
83 by (induct A arbitrary: x a) (auto) |
83 by (induct A arbitrary: x a) (auto) |
84 |
84 |
85 lemma mem_delete_raw_ident: |
85 lemma mem_delete_raw_ident: |
86 "\<not>(a \<in> set (delete_raw A a))" |
86 "\<not>(a \<in> set (delete_raw A a))" |
87 by (induct A) (auto) |
87 by (induct A) (auto) |
95 apply(induct A arbitrary: B a) |
95 apply(induct A arbitrary: B a) |
96 apply(auto) |
96 apply(auto) |
97 sorry |
97 sorry |
98 |
98 |
99 lemma cons_delete_raw: |
99 lemma cons_delete_raw: |
100 "a # (delete_raw A a) \<approx> (if a mem A then A else (a # A))" |
100 "a # (delete_raw A a) \<approx> (if a \<in> set A then A else (a # A))" |
101 sorry |
101 sorry |
102 |
102 |
103 lemma mem_cons_delete_raw: |
103 lemma mem_cons_delete_raw: |
104 "a \<in> set A \<Longrightarrow> a # (delete_raw A a) \<approx> A" |
104 "a \<in> set A \<Longrightarrow> a # (delete_raw A a) \<approx> A" |
105 sorry |
105 sorry |
110 |
110 |
111 fun |
111 fun |
112 card_raw :: "'a list \<Rightarrow> nat" |
112 card_raw :: "'a list \<Rightarrow> nat" |
113 where |
113 where |
114 card_raw_nil: "card_raw [] = 0" |
114 card_raw_nil: "card_raw [] = 0" |
115 | card_raw_cons: "card_raw (x # xs) = (if x mem xs then card_raw xs else Suc (card_raw xs))" |
115 | card_raw_cons: "card_raw (x # xs) = (if x \<in> set xs then card_raw xs else Suc (card_raw xs))" |
116 |
116 |
117 lemma not_mem_card_raw: |
117 lemma not_mem_card_raw: |
118 fixes x :: "'a" |
118 fixes x :: "'a" |
119 fixes xs :: "'a list" |
119 fixes xs :: "'a list" |
120 shows "(\<not>(x mem xs)) = (card_raw (x # xs) = Suc (card_raw xs))" |
120 shows "(\<not>(x mem xs)) = (card_raw (x # xs) = Suc (card_raw xs))" |
121 sorry |
121 sorry |
122 |
122 |
123 lemma card_raw_suc: |
123 lemma card_raw_suc: |
124 fixes xs :: "'a list" |
|
125 fixes n :: "nat" |
|
126 assumes c: "card_raw xs = Suc n" |
124 assumes c: "card_raw xs = Suc n" |
127 shows "\<exists>a ys. \<not>(a mem ys) \<and> xs \<approx> (a # ys)" |
125 shows "\<exists>a ys. (a \<notin> set ys) \<and> xs \<approx> (a # ys)" |
128 using c |
126 using c apply(induct xs) |
129 apply(induct xs) |
127 apply(simp) |
130 (*apply(metis mem_delete_raw) |
128 sorry |
131 apply(metis mem_delete_raw) |
129 |
132 done*) |
130 lemma mem_card_raw_gt_0: |
133 sorry |
131 "a \<in> set A \<Longrightarrow> 0 < card_raw A" |
134 |
132 by (induct A) (auto) |
135 |
|
136 lemma mem_card_raw_not_0: |
|
137 "a mem A \<Longrightarrow> \<not>(card_raw A = 0)" |
|
138 sorry |
|
139 |
133 |
140 lemma card_raw_cons_gt_0: |
134 lemma card_raw_cons_gt_0: |
141 "0 < card_raw (a # A)" |
135 "0 < card_raw (a # A)" |
142 sorry |
136 by (induct A) (auto) |
143 |
137 |
144 lemma card_raw_delete_raw: |
138 lemma card_raw_delete_raw: |
145 "card_raw (delete_raw A a) = (if a mem A then card_raw A - 1 else card_raw A)" |
139 "card_raw (delete_raw A a) = (if a \<in> set A then card_raw A - 1 else card_raw A)" |
146 sorry |
140 sorry |
147 |
141 |
148 lemma card_raw_rsp_aux: |
142 lemma card_raw_rsp_aux: |
149 assumes e: "a \<approx> b" |
143 assumes e: "a \<approx> b" |
150 shows "card_raw a = card_raw b" |
144 shows "card_raw a = card_raw b" |
154 "(op \<approx> ===> op =) card_raw card_raw" |
148 "(op \<approx> ===> op =) card_raw card_raw" |
155 by (simp add: card_raw_rsp_aux) |
149 by (simp add: card_raw_rsp_aux) |
156 |
150 |
157 lemma card_raw_0: |
151 lemma card_raw_0: |
158 "(card_raw A = 0) = (A = [])" |
152 "(card_raw A = 0) = (A = [])" |
159 sorry |
153 by (induct A) (auto) |
160 |
154 |
161 lemma list2set_thm: |
155 lemma list2set_thm: |
162 shows "set [] = {}" |
156 shows "set [] = {}" |
163 and "set (h # t) = insert h (set t)" |
157 and "set (h # t) = insert h (set t)" |
164 sorry |
158 by (auto) |
165 |
159 |
166 lemma list2set_RSP: |
160 lemma list2set_RSP: |
167 "A \<approx> B \<Longrightarrow> set A = set B" |
161 "A \<approx> B \<Longrightarrow> set A = set B" |
168 sorry |
162 by auto |
169 |
163 |
170 definition |
164 definition |
171 rsp_fold |
165 rsp_fold |
172 where |
166 where |
173 "rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))" |
167 "rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))" |