# HG changeset patch
# User wenzelm
# Date 1375966501 -7200
# Node ID 66cc4ed9a1f2d7259fd405930f0722fba42bd12f
# Parent  ba514b5aa809b9d8edf3af81813639093d15a7d2# Parent  3461985dcbc3257cb86e48ea003265fe224f6ac8
merged

diff -r 3461985dcbc3 -r 66cc4ed9a1f2 src/HOL/BNF/Examples/Stream.thy
--- a/src/HOL/BNF/Examples/Stream.thy	Thu Aug 08 14:24:21 2013 +0200
+++ b/src/HOL/BNF/Examples/Stream.thy	Thu Aug 08 14:55:01 2013 +0200
@@ -239,6 +239,17 @@
   qed (metis comp_apply sdrop.simps(1) sdrop_while.simps snth.simps(1))
 qed
 
+definition "sfilter P = stream_unfold (shd o sdrop_while (Not o P)) (stl o sdrop_while (Not o P))"
+
+lemma sfilter_Stream: "sfilter P (x ## s) = (if P x then x ## sfilter P s else sfilter P s)"
+proof (cases "P x")
+  case True thus ?thesis unfolding sfilter_def
+    by (subst stream.unfold) (simp add: sdrop_while_Stream)
+next
+  case False thus ?thesis unfolding sfilter_def
+    by (subst (1 2) stream.unfold) (simp add: sdrop_while_Stream)
+qed
+
 
 subsection {* unary predicates lifted to streams *}
 
diff -r 3461985dcbc3 -r 66cc4ed9a1f2 src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Aug 08 14:24:21 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Aug 08 14:55:01 2013 +0200
@@ -326,7 +326,7 @@
     val coalg_prem = HOLogic.mk_Trueprop (mk_coalg As Bs ss);
 
     val coalg_in_thms = map (fn i =>
-      coalg_def RS @{thm subst[of _ _ "%x. x"]} RS mk_conjunctN n i RS bspec) ks
+      coalg_def RS iffD1 RS mk_conjunctN n i RS bspec) ks
 
     val coalg_set_thmss =
       let
@@ -922,9 +922,9 @@
       |> Thm.close_derivation;
 
     val lsbis_incl_thms = map (fn i => sbis_lsbis_thm RS
-      (bis_def RS @{thm subst[of _ _ "%x. x"]} RS conjunct1 RS mk_conjunctN n i)) ks;
+      (bis_def RS iffD1 RS conjunct1 RS mk_conjunctN n i)) ks;
     val lsbisE_thms = map (fn i => (mk_specN 2 (sbis_lsbis_thm RS
-      (bis_def RS @{thm subst[of _ _ "%x. x"]} RS conjunct2 RS mk_conjunctN n i))) RS mp) ks;
+      (bis_def RS iffD1 RS conjunct2 RS mk_conjunctN n i))) RS mp) ks;
 
     val incl_lsbis_thms =
       let
@@ -1482,8 +1482,8 @@
         map (fn i => map (fn i' =>
           split_conj_thm (if n = 1 then set_rv_Lev' RS mk_conjunctN n i RS mp
             else set_rv_Lev' RS mk_conjunctN n i RS mp RSN
-              (2, @{thm sum_case_weak_cong} RS @{thm subst[of _ _ "%x. x"]}) RS
-              (mk_sum_casesN n i' RS @{thm subst[of _ _ "%x. x"]}))) ks) ks
+              (2, @{thm sum_case_weak_cong} RS iffD1) RS
+              (mk_sum_casesN n i' RS iffD1))) ks) ks
       end;
 
     val set_Lev_thmsss =
@@ -1838,7 +1838,7 @@
       end;
 
     val (dtor_unfold_unique_thms, dtor_unfold_unique_thm) = `split_conj_thm (split_conj_prems n
-      (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS unfold_unique_mor_thm));
+      (mor_UNIV_thm RS iffD2 RS unfold_unique_mor_thm));
 
     val unfold_dtor_thms = map (fn thm => mor_id_thm RS thm RS sym) unfold_unique_mor_thms;
 
@@ -2005,7 +2005,7 @@
 
     val dtor_corec_unique_thms =
       split_conj_thm (split_conj_prems n
-        (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS corec_unique_mor_thm)
+        (mor_UNIV_thm RS iffD2 RS corec_unique_mor_thm)
         |> Local_Defs.unfold lthy (@{thms o_sum_case o_id id_o o_assoc sum_case_o_inj(1)} @
            map_ids @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]});
 
diff -r 3461985dcbc3 -r 66cc4ed9a1f2 src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Aug 08 14:24:21 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Aug 08 14:55:01 2013 +0200
@@ -1135,7 +1135,7 @@
 
     val ctor_fold_unique_thms =
       split_conj_thm (mk_conjIN n RS
-        (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS fold_unique_mor_thm))
+        (mor_UNIV_thm RS iffD2 RS fold_unique_mor_thm))
 
     val fold_ctor_thms =
       map (fn thm => (mor_incl_thm OF replicate n @{thm subset_UNIV}) RS thm RS sym)
@@ -1296,7 +1296,7 @@
 
     val ctor_rec_unique_thms =
       split_conj_thm (split_conj_prems n
-        (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS rec_unique_mor_thm)
+        (mor_UNIV_thm RS iffD2 RS rec_unique_mor_thm)
         |> Local_Defs.unfold lthy (@{thms convol_o o_id id_o o_assoc[symmetric] fst_convol} @
            map_ids @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ convol, OF refl]});
 
diff -r 3461985dcbc3 -r 66cc4ed9a1f2 src/HOL/BNF/Tools/bnf_lfp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Thu Aug 08 14:24:21 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Thu Aug 08 14:55:01 2013 +0200
@@ -245,7 +245,7 @@
           REPEAT_DETERM o rtac subset_UNIV, REPEAT_DETERM_N n o (set_tac thms)])
       (set_map's ~~ alg_sets);
   in
-    (rtac (iso_alt RS @{thm ssubst[of _ _ "%x. x"]}) THEN'
+    (rtac (iso_alt RS iffD2) THEN'
     etac copy_str THEN' REPEAT_DETERM o atac THEN'
     rtac conjI THEN' stac mor_def THEN' rtac conjI THEN' fbetw_tac THEN' mor_tac THEN'
     CONJ_WRAP' (K atac) alg_sets) 1
@@ -372,7 +372,7 @@
             etac @{thm underS_I}, atac, atac]]))
           set_bds];
   in
-    (rtac (alg_def RS @{thm ssubst[of _ _ "%x. x"]}) THEN'
+    (rtac (alg_def RS iffD2) THEN'
     CONJ_WRAP' mk_conjunct_tac (set_bdss ~~ (min_algs ~~ min_alg_defs))) 1
   end;
 
diff -r 3461985dcbc3 -r 66cc4ed9a1f2 src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Thu Aug 08 14:24:21 2013 +0200
+++ b/src/HOL/IMP/Compiler.thy	Thu Aug 08 14:55:01 2013 +0200
@@ -34,14 +34,11 @@
 
 subsection "Instructions and Stack Machine"
 
+text_raw{*\snip{instrdef}{0}{1}{% *}
 datatype instr = 
-  LOADI int |
-  LOAD vname |
-  ADD |
-  STORE vname |
-  JMP int |
-  JMPLESS int |
-  JMPGE int
+  LOADI int | LOAD vname | ADD | STORE vname |
+  JMP int | JMPLESS int | JMPGE int
+text_raw{*}%endsnip*}
 
 type_synonym stack = "val list"
 type_synonym config = "int \<times> state \<times> stack"