equal
deleted
inserted
replaced
52 lemma cons_left_idem: |
52 lemma cons_left_idem: |
53 "x # x # A \<approx> x # A" |
53 "x # x # A \<approx> x # A" |
54 by auto |
54 by auto |
55 |
55 |
56 lemma finite_set_raw_strong_cases: |
56 lemma finite_set_raw_strong_cases: |
57 "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a mem Y) \<and> (X \<approx> a # Y)))" |
57 "(X = []) \<or> (\<exists>a Y. ((a \<notin> set Y) \<and> (X \<approx> a # Y)))" |
58 apply (induct X) |
58 apply (induct X) |
|
59 apply (simp) |
|
60 apply (rule disjI2) |
|
61 apply (erule disjE) |
|
62 apply (rule_tac x="a" in exI) |
|
63 apply (rule_tac x="[]" in exI) |
|
64 apply (simp) |
|
65 apply (erule exE)+ |
|
66 apply (case_tac "a = aa") |
|
67 apply (rule_tac x="a" in exI) |
|
68 apply (rule_tac x="Y" in exI) |
|
69 apply (simp) |
|
70 apply (rule_tac x="aa" in exI) |
|
71 apply (rule_tac x="a # Y" in exI) |
59 apply (auto) |
72 apply (auto) |
60 sorry |
73 done |
61 |
74 |
62 fun |
75 fun |
63 delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list" |
76 delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list" |
64 where |
77 where |
65 "delete_raw [] x = []" |
78 "delete_raw [] x = []" |