isabelle: src/HOLCF/FOCUS/FOCUS.thy@033ce4cafba6 (annotated)

17293 ecf182ccc3ca converted to Isar theory format; wenzelm parents: 14981 diff changeset	1	(* Title: HOLCF/FOCUS/FOCUS.thy
11355 778c369559d9 tuned wenzelm parents: 11350 diff changeset	2	ID: $Id$
17293 ecf182ccc3ca converted to Isar theory format; wenzelm parents: 14981 diff changeset	3	Author: David von Oheimb, TU Muenchen
11350 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
17293 ecf182ccc3ca converted to Isar theory format; wenzelm parents: 14981 diff changeset	6	header {* Top level of FOCUS *}
ecf182ccc3ca converted to Isar theory format; wenzelm parents: 14981 diff changeset	7
ecf182ccc3ca converted to Isar theory format; wenzelm parents: 14981 diff changeset	8	theory FOCUS
ecf182ccc3ca converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	imports Fstream
ecf182ccc3ca converted to Isar theory format; wenzelm parents: 14981 diff changeset	10	begin
ecf182ccc3ca converted to Isar theory format; wenzelm parents: 14981 diff changeset	11
19759 2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	12	lemma ex_eqI [intro!]: "? xx. x = xx"
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	13	by auto
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	14
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	15	lemma ex2_eqI [intro!]: "? xx yy. x = xx & y = yy"
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	16	by auto
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	17
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	18	lemma eq_UU_symf: "(UU = f x) = (f x = UU)"
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	19	by auto
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	20
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	21	lemma fstream_exhaust_slen_eq: "(#x ~= 0) = (? a y. x = a~> y)"
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	22	by (simp add: slen_empty_eq fstream_exhaust_eq)
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	23
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	24	lemmas [simp] =
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	25	slen_less_1_eq fstream_exhaust_slen_eq
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	26	slen_fscons_eq slen_fscons_less_eq Suc_ile_eq
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	27
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	28	declare strictI [elim]
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	29
17293 ecf182ccc3ca converted to Isar theory format; wenzelm parents: 14981 diff changeset	30	end

author	krauss
	Mon, 23 Nov 2009 15:11:21 +0100
changeset 33859	033ce4cafba6
parent 19759	2d0896653e7a
child 35174	e15040ae75d7
permissions	-rw-r--r--