--- a/src/HOL/BNF/Examples/Koenig.thy Mon Aug 12 23:21:06 2013 +0200
+++ b/src/HOL/BNF/Examples/Koenig.thy Mon Aug 12 23:36:43 2013 +0200
@@ -14,10 +14,14 @@
(* selectors for streams *)
lemma shd_def': "shd as = fst (stream_dtor as)"
-unfolding shd_def stream_case_def fst_def by (rule refl)
+apply (case_tac as)
+apply (auto simp add: shd_def)
+by (simp add: Stream_def stream.dtor_ctor)
lemma stl_def': "stl as = snd (stream_dtor as)"
-unfolding stl_def stream_case_def snd_def by (rule refl)
+apply (case_tac as)
+apply (auto simp add: stl_def)
+by (simp add: Stream_def stream.dtor_ctor)
lemma unfold_pair_fun_shd[simp]: "shd (stream_dtor_unfold (f \<odot> g) t) = f t"
unfolding shd_def' pair_fun_def stream.dtor_unfold by simp
--- a/src/HOL/BNF/Examples/TreeFI.thy Mon Aug 12 23:21:06 2013 +0200
+++ b/src/HOL/BNF/Examples/TreeFI.thy Mon Aug 12 23:36:43 2013 +0200
@@ -19,11 +19,7 @@
by (auto simp add: listF.set_map')
lemma dtor[simp]: "treeFI_dtor tr = (lab tr, sub tr)"
-unfolding lab_def sub_def treeFI_case_def
-(*
-by (metis fst_def pair_collapse snd_def)
-*)
-sorry
+by (metis Tree_def treeFI.collapse treeFI.dtor_ctor)
definition pair_fun (infixr "\<odot>" 50) where
"f \<odot> g \<equiv> \<lambda>x. (f x, g x)"