# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1254474573 -7200
# Node ID 4826ad24f772e270465730338a075bca5b07e4e0
# Parent  f2565006dc5afb10f0a0ec65b0edb2809d092016
First theorem with quantifiers. Learned how to use sledgehammer.

diff -r f2565006dc5a -r 4826ad24f772 QuotMain.thy
--- a/QuotMain.thy	Wed Sep 30 16:57:09 2009 +0200
+++ b/QuotMain.thy	Fri Oct 02 11:09:33 2009 +0200
@@ -702,6 +702,15 @@
   shows "(z # xs) \<approx> (z # ys)"
   using a by (rule QuotMain.list_eq.intros(5))
 
+lemma fs1_strong_cases:
+  fixes X :: "'a list"
+  shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a memb Y) \<and> (X \<approx> a # Y)))"
+  apply (induct X)
+  apply (simp)
+  apply (erule disjE)
+  apply (metis QuotMain.m1 list_eq_refl)
+  apply (metis QUOT_TYPE_I_fset.R_sym QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons)
+  done
 
 text {*
   Unlam_def converts a definition given as
@@ -1254,4 +1263,3 @@
 *)
 
 end
-