src/HOLCF/stream2.ML

use HOLogic.Not;
export indexify_names;

(*  Title: 	HOLCF/stream2.ML
    ID:         $Id$
    Author: 	Franz Regensburger
    Copyright   1993 Technische Universitaet Muenchen

Lemmas for theory Stream2.thy
*)

open Stream2;

(* ------------------------------------------------------------------------- *)
(* expand fixed point properties                                             *)
(* ------------------------------------------------------------------------- *)

val smap_def2 = fix_prover Stream2.thy smap_def 
	"smap = (LAM f s. stream_when[LAM x l.scons[f[x]][smap[f][l]]][s])";


(* ------------------------------------------------------------------------- *)
(* recursive  properties                                                     *)
(* ------------------------------------------------------------------------- *)


val smap1 = prove_goal Stream2.thy "smap[f][UU] = UU"
 (fn prems =>
	[
	(rtac (smap_def2 RS ssubst) 1),
	(simp_tac (HOLCF_ss addsimps stream_when) 1)
	]);

val smap2 = prove_goal Stream2.thy 
	"x~=UU ==> smap[f][scons[x][xs]] = scons[f[x]][smap[f][xs]]"
 (fn prems =>
	[
	(cut_facts_tac prems 1),
	(rtac trans 1),
	(rtac (smap_def2 RS ssubst) 1),
	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
	(rtac refl 1)
	]);


val stream2_rews = [smap1, smap2];