src/HOLCF/explicit_domains/Stream2.ML
changeset 2679 3eac428cdd1b
parent 2678 d5fe793293ac
child 2680 20fa49e610ca
     1.1 --- a/src/HOLCF/explicit_domains/Stream2.ML	Mon Feb 24 09:46:12 1997 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,43 +0,0 @@
     1.4 -(*
     1.5 -    ID:         $Id$
     1.6 -    Author:     Franz Regensburger
     1.7 -    Copyright   1993 Technische Universitaet Muenchen
     1.8 -
     1.9 -Lemmas for theory Stream2.thy
    1.10 -*)
    1.11 -
    1.12 -open Stream2;
    1.13 -
    1.14 -(* ------------------------------------------------------------------------- *)
    1.15 -(* expand fixed point properties                                             *)
    1.16 -(* ------------------------------------------------------------------------- *)
    1.17 -
    1.18 -val smap_def2 = fix_prover2 Stream2.thy smap_def 
    1.19 -        "smap = (LAM f s. stream_when`(LAM x l.scons`(f`x) `(smap`f`l)) `s)";
    1.20 -
    1.21 -
    1.22 -(* ------------------------------------------------------------------------- *)
    1.23 -(* recursive  properties                                                     *)
    1.24 -(* ------------------------------------------------------------------------- *)
    1.25 -
    1.26 -
    1.27 -qed_goal "smap1" Stream2.thy "smap`f`UU = UU"
    1.28 - (fn prems =>
    1.29 -        [
    1.30 -        (stac smap_def2 1),
    1.31 -        (simp_tac (!simpset addsimps stream_when) 1)
    1.32 -        ]);
    1.33 -
    1.34 -qed_goal "smap2" Stream2.thy 
    1.35 -        "x~=UU ==> smap`f`(scons`x`xs) = scons `(f`x) `(smap`f`xs)"
    1.36 - (fn prems =>
    1.37 -        [
    1.38 -        (cut_facts_tac prems 1),
    1.39 -        (rtac trans 1),
    1.40 -        (stac smap_def2 1),
    1.41 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
    1.42 -        (rtac refl 1)
    1.43 -        ]);
    1.44 -
    1.45 -
    1.46 -val stream2_rews = [smap1, smap2];