isabelle: src/HOLCF/FOCUS/Stream_adm.thy@213dcc39358f (annotated)

11350 4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	1	(* Title: HOLCF/ex/Stream_adm.thy
11355 778c369559d9 tuned wenzelm parents: 11350 diff changeset	2	ID: $Id$
11350 4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	3	Author: David von Oheimb, TU Muenchen
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	4	License: GPL (GNU GENERAL PUBLIC LICENSE)
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	5
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	6	Admissibility for streams
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	7	*)
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	8
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	9	Stream_adm = Stream + Continuity +
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	10
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	11	consts
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	12
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	13	stream_monoP,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	14	stream_antiP :: "(('a stream) set \\<Rightarrow> ('a stream) set) \\<Rightarrow> bool"
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	15
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	16	defs
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	17
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	18	stream_monoP_def "stream_monoP F \\<equiv> \\<exists>Q i. \\<forall>P s. Fin i \\<le> #s \\<longrightarrow>
11655 923e4d0d36d5 tuned parentheses in relational expressions; wenzelm parents: 11355 diff changeset	19	(s \\<in> F P) = (stream_take i\\<cdot>s \\<in> Q \\<and> iterate i rt s \\<in> P)"
11350 4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	20	stream_antiP_def "stream_antiP F \\<equiv> \\<forall>P x. \\<exists>Q i.
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	21	(#x < Fin i \\<longrightarrow> (\\<forall>y. x \\<sqsubseteq> y \\<longrightarrow> y \\<in> F P \\<longrightarrow> x \\<in> F P)) \\<and>
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	22	(Fin i <= #x \\<longrightarrow> (\\<forall>y. x \\<sqsubseteq> y \\<longrightarrow>
11655 923e4d0d36d5 tuned parentheses in relational expressions; wenzelm parents: 11355 diff changeset	23	(y \\<in> F P) = (stream_take i\\<cdot>y \\<in> Q \\<and> iterate i rt y \\<in> P)))"
11350 4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	24
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	25	constdefs
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	26	antitonP :: "'a set => bool"
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	27	"antitonP P \\<equiv> \\<forall>x y. x \\<sqsubseteq> y \\<longrightarrow> y\\<in>P \\<longrightarrow> x\\<in>P"
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	28
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	29	end

author	kleing
	Tue, 13 May 2003 08:59:21 +0200
changeset 14024	213dcc39358f
parent 11655	923e4d0d36d5
child 14981	e73f8140af78
permissions	-rw-r--r--