# HG changeset patch
# User huffman
# Date 1320391164 -3600
# Node ID f502f439305435023f77dac7e0b8b993ffda8f60
# Parent  a68ce51de69a66e0f0d004c9966ceea9eaad818f
ex/Tree23.thy: automate proof of gfull_add

diff -r a68ce51de69a -r f502f4393054 src/HOL/ex/Tree23.thy
--- a/src/HOL/ex/Tree23.thy	Fri Nov 04 08:00:48 2011 +0100
+++ b/src/HOL/ex/Tree23.thy	Fri Nov 04 08:19:24 2011 +0100
@@ -218,28 +218,7 @@
 "gfull n (Sprout l p r) \<longleftrightarrow> full n l \<and> full n r"
 
 lemma gfull_add: "full n t \<Longrightarrow> gfull n (add k y t)"
- apply (induct set: full)
-   apply simp
-  apply clarsimp
-  apply (case_tac "ord k a")
-    apply simp
-    apply (case_tac "add k y l", simp, simp)
-   apply simp
-  apply simp
-  apply (case_tac "add k y r", simp, simp)
- apply clarsimp
- apply (case_tac "ord k a")
-   apply simp
-   apply (case_tac "add k y l", simp, simp)
-  apply simp
- apply simp
- apply (case_tac "ord k aa")
-   apply simp
-   apply (case_tac "add k y m", simp, simp)
-  apply simp
- apply simp
- apply (case_tac "add k y r", simp, simp)
-done
+by (induct set: full, auto split: ord.split growth.split)
 
 text {* The @{term "add0"} operation preserves balance. *}
 
@@ -373,6 +352,8 @@
       apply (simp split: ord.split)
      apply simp
      apply (subst del_extra_simps, force)
+     (* This should work, but it is way too slow!
+     apply (force split: ord.split option.split bool.split tree23.split) *)
      apply (simp | rule dfull_case_intros)+
      done
   } note A = this