isabelle: src/HOLCF/FOCUS/Stream_adm.thy@e73f8140af78 (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
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	5	Admissibility for streams
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	6	*)
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	Stream_adm = Stream + Continuity +
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	9
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	10	consts
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	11
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	12	stream_monoP,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	13	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	14
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	15	defs
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	16
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	17	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	18	(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	19	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	20	(#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	21	(Fin i <= #x \\<longrightarrow> (\\<forall>y. x \\<sqsubseteq> y \\<longrightarrow>
11655 923e4d0d36d5 tuned parentheses in relational expressions; wenzelm parents: 11355 diff changeset	22	(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	23
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	24	constdefs
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	25	antitonP :: "'a set => bool"
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	26	"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	27
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	28	end

author	kleing
	Mon, 21 Jun 2004 10:25:57 +0200
changeset 14981	e73f8140af78
parent 11655	923e4d0d36d5
child 17293	ecf182ccc3ca
permissions	-rw-r--r--