equal
deleted
inserted
replaced
63 delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list" |
63 delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list" |
64 where |
64 where |
65 "delete_raw [] x = []" |
65 "delete_raw [] x = []" |
66 | "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))" |
66 | "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))" |
67 |
67 |
68 (* definitely FALSE |
|
69 lemma mem_delete_raw: |
68 lemma mem_delete_raw: |
70 "x mem (delete_raw A a) = x mem A \<and> \<not>(x = a)" |
69 "x mem (delete_raw A a) = (x mem A \<and> \<not>(x = a))" |
71 apply(induct A arbitrary: x a) |
70 by (induct A arbitrary: x a) (auto) |
72 apply(auto) |
|
73 sorry |
|
74 *) |
|
75 |
71 |
76 lemma mem_delete_raw_ident: |
72 lemma mem_delete_raw_ident: |
77 "\<not>(a \<in> set (delete_raw A a))" |
73 "\<not>(a \<in> set (delete_raw A a))" |
78 by (induct A) (auto) |
74 by (induct A) (auto) |
79 |
75 |
90 lemma cons_delete_raw: |
86 lemma cons_delete_raw: |
91 "a # (delete_raw A a) \<approx> (if a mem A then A else (a # A))" |
87 "a # (delete_raw A a) \<approx> (if a mem A then A else (a # A))" |
92 sorry |
88 sorry |
93 |
89 |
94 lemma mem_cons_delete_raw: |
90 lemma mem_cons_delete_raw: |
95 "a mem A \<Longrightarrow> a # (delete_raw A a) \<approx> A" |
91 "a \<in> set A \<Longrightarrow> a # (delete_raw A a) \<approx> A" |
96 sorry |
|
97 |
|
98 lemma finite_set_raw_delete_raw_cases1: |
|
99 "X = [] \<or> (\<exists>a. X \<approx> a # delete_raw X a)" |
|
100 sorry |
92 sorry |
101 |
93 |
102 lemma finite_set_raw_delete_raw_cases: |
94 lemma finite_set_raw_delete_raw_cases: |
103 "X = [] \<or> (\<exists>a. a mem X \<and> X \<approx> a # delete_raw X a)" |
95 "X = [] \<or> (\<exists>a. a mem X \<and> X \<approx> a # delete_raw X a)" |
104 sorry |
96 by (induct X) (auto) |
105 |
97 |
106 fun |
98 fun |
107 card_raw :: "'a list \<Rightarrow> nat" |
99 card_raw :: "'a list \<Rightarrow> nat" |
108 where |
100 where |
109 card_raw_nil: "card_raw [] = 0" |
101 card_raw_nil: "card_raw [] = 0" |