# HG changeset patch
# User blanchet
# Date 1376343403 -7200
# Node ID abd760a19e22ac49a06ac664738b45cd942ab604
# Parent  633ccbcd8d8c2d649a8c951a33ac699527f7d198
fixed "sorry"d proofs

diff -r 633ccbcd8d8c -r abd760a19e22 src/HOL/BNF/Examples/Koenig.thy
--- 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
diff -r 633ccbcd8d8c -r abd760a19e22 src/HOL/BNF/Examples/TreeFI.thy
--- 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)"