src/HOLCF/stream2.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 243 c22b85994e17
permissions -rw-r--r--
made tutorial first;
     1 (*  Title: 	HOLCF/stream2.ML
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Lemmas for theory Stream2.thy
     7 *)
     8 
     9 open Stream2;
    10 
    11 (* ------------------------------------------------------------------------- *)
    12 (* expand fixed point properties                                             *)
    13 (* ------------------------------------------------------------------------- *)
    14 
    15 val smap_def2 = fix_prover Stream2.thy smap_def 
    16 	"smap = (LAM f s. stream_when[LAM x l.scons[f[x]][smap[f][l]]][s])";
    17 
    18 
    19 (* ------------------------------------------------------------------------- *)
    20 (* recursive  properties                                                     *)
    21 (* ------------------------------------------------------------------------- *)
    22 
    23 
    24 val smap1 = prove_goal Stream2.thy "smap[f][UU] = UU"
    25  (fn prems =>
    26 	[
    27 	(rtac (smap_def2 RS ssubst) 1),
    28 	(simp_tac (HOLCF_ss addsimps stream_when) 1)
    29 	]);
    30 
    31 val smap2 = prove_goal Stream2.thy 
    32 	"x~=UU ==> smap[f][scons[x][xs]] = scons[f[x]][smap[f][xs]]"
    33  (fn prems =>
    34 	[
    35 	(cut_facts_tac prems 1),
    36 	(rtac trans 1),
    37 	(rtac (smap_def2 RS ssubst) 1),
    38 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
    39 	(rtac refl 1)
    40 	]);
    41 
    42 
    43 val stream2_rews = [smap1, smap2];