# HG changeset patch
# User traytel
# Date 1393537589 -3600
# Node ID 341fbb9bdda1286fa27ff0be19797b0e7ac76b7e
# Parent  74d3fe9031d8fac3a856fe7a034484b825177f08
adapt examples to new intermediate typedef

diff -r 74d3fe9031d8 -r 341fbb9bdda1 src/HOL/BNF_Examples/Stream.thy
--- a/src/HOL/BNF_Examples/Stream.thy	Tue Feb 25 18:14:26 2014 +0100
+++ b/src/HOL/BNF_Examples/Stream.thy	Thu Feb 27 22:46:29 2014 +0100
@@ -26,12 +26,25 @@
 
 (* TODO: Provide by the package*)
 theorem sset_induct:
-  "\<lbrakk>\<And>s. P (shd s) s; \<And>s y. \<lbrakk>y \<in> sset (stl s); P y (stl s)\<rbrakk> \<Longrightarrow> P y s\<rbrakk> \<Longrightarrow>
-    \<forall>y \<in> sset s. P y s"
-  apply (rule stream.dtor_set_induct)
-  apply (auto simp add: shd_def stl_def fsts_def snds_def split_beta)
-  apply (metis SCons_def fst_conv stream.case stream.dtor_ctor stream.exhaust)
-  by (metis SCons_def sndI stl_def stream.collapse stream.dtor_ctor)
+  assumes Base: "\<And>s. P (shd s) s" and Step: "\<And>s y. \<lbrakk>y \<in> sset (stl s); P y (stl s)\<rbrakk> \<Longrightarrow> P y s"
+  shows "\<forall>y \<in> sset s. P y s"
+proof (rule stream.dtor_set_induct)
+  fix a :: 'a and s :: "'a stream"
+  assume "a \<in> set1_pre_stream (dtor_stream s)"
+  then have "a = shd s"
+    by (cases "dtor_stream s")
+      (auto simp: shd_def fsts_def set1_pre_stream_def stream.dtor_ctor SCons_def
+        Abs_stream_pre_stream_inverse Abs_stream_pre_stream_inject split: stream.splits)
+  with Base show "P a s" by simp
+next
+  fix a :: 'a and s' :: "'a stream"  and s :: "'a stream"
+  assume "s' \<in> set2_pre_stream (dtor_stream s)" and prems: "a \<in> sset s'" "P a s'"
+  then have "s' = stl s"
+    by (cases "dtor_stream s")
+      (auto simp: stl_def snds_def set2_pre_stream_def stream.dtor_ctor SCons_def
+        Abs_stream_pre_stream_inverse Abs_stream_pre_stream_inject split: stream.splits)
+  with Step prems show "P a s" by simp
+qed
 
 lemma smap_simps[simp]:
   "shd (smap f s) = f (shd s)" "stl (smap f s) = smap f (stl s)"
diff -r 74d3fe9031d8 -r 341fbb9bdda1 src/HOL/BNF_Examples/Stream_Processor.thy
--- a/src/HOL/BNF_Examples/Stream_Processor.thy	Tue Feb 25 18:14:26 2014 +0100
+++ b/src/HOL/BNF_Examples/Stream_Processor.thy	Thu Feb 27 22:46:29 2014 +0100
@@ -126,7 +126,7 @@
 (*will be provided by the package*)
 lemma sp\<^sub>\<mu>_rel_map_map[unfolded vimage2p_def, simp]:
   "rel_sp\<^sub>\<mu> R1 R2 (map_sp\<^sub>\<mu> f1 f2 sp) (map_sp\<^sub>\<mu> g1 g2 sp') =
-  rel_sp\<^sub>\<mu> (BNF_Def.vimage2p f1 g1 R1) (BNF_Def.vimage2p f2 g2 R2) sp sp'"
+  rel_sp\<^sub>\<mu> (BNF_Util.vimage2p f1 g1 R1) (BNF_Util.vimage2p f2 g2 R2) sp sp'"
 by (tactic {*
   let val ks = 1 upto 2;
   in