# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260588347 -3600
# Node ID 1a777307f57fdf9950d066a3fc19e43ef77bdcaf
# Parent  0d98a4c7f8dc138a11b6f7e8634a9f28a22e6ea0
A bracket was missing; with it proved the 'definitely false' lemma.

diff -r 0d98a4c7f8dc -r 1a777307f57f Quot/Examples/FSet3.thy
--- a/Quot/Examples/FSet3.thy	Sat Dec 12 01:44:56 2009 +0100
+++ b/Quot/Examples/FSet3.thy	Sat Dec 12 04:25:47 2009 +0100
@@ -65,13 +65,9 @@
   "delete_raw [] x = []"
 | "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))"
 
-(* definitely FALSE
 lemma mem_delete_raw:
-  "x mem (delete_raw A a) = x mem A \<and> \<not>(x = a)"
-apply(induct A arbitrary: x a)
-apply(auto)
-sorry
-*)
+  "x mem (delete_raw A a) = (x mem A \<and> \<not>(x = a))"
+  by (induct A arbitrary: x a) (auto)
 
 lemma mem_delete_raw_ident:
   "\<not>(a \<in> set (delete_raw A a))"
@@ -92,16 +88,12 @@
 sorry
 
 lemma mem_cons_delete_raw:
-    "a mem A \<Longrightarrow> a # (delete_raw A a) \<approx> A"
-sorry
-
-lemma finite_set_raw_delete_raw_cases1:
-    "X = [] \<or> (\<exists>a. X \<approx> a # delete_raw X a)"
+    "a \<in> set A \<Longrightarrow> a # (delete_raw A a) \<approx> A"
 sorry
 
 lemma finite_set_raw_delete_raw_cases:
     "X = [] \<or> (\<exists>a. a mem X \<and> X \<approx> a # delete_raw X a)"
-sorry
+  by (induct X) (auto)
 
 fun
   card_raw :: "'a list \<Rightarrow> nat"