isabelle: src/HOL/HOLCF/FOCUS/FOCUS.thy@c7c85ff6de2a (annotated)

42151 4da4fc77664b tuned headers; wenzelm parents: 40774 diff changeset	1	(* Title: HOL/HOLCF/FOCUS/FOCUS.thy
17293 ecf182ccc3ca converted to Isar theory format; wenzelm parents: 14981 diff changeset	2	Author: David von Oheimb, TU Muenchen
11350 4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	3	*)
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	4
17293 ecf182ccc3ca converted to Isar theory format; wenzelm parents: 14981 diff changeset	5	header {* Top level of FOCUS *}
ecf182ccc3ca converted to Isar theory format; wenzelm parents: 14981 diff changeset	6
ecf182ccc3ca converted to Isar theory format; wenzelm parents: 14981 diff changeset	7	theory FOCUS
ecf182ccc3ca converted to Isar theory format; wenzelm parents: 14981 diff changeset	8	imports Fstream
ecf182ccc3ca converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	begin
ecf182ccc3ca converted to Isar theory format; wenzelm parents: 14981 diff changeset	10
19759 2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	11	lemma ex_eqI [intro!]: "? xx. x = xx"
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	12	by auto
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	13
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	14	lemma ex2_eqI [intro!]: "? xx yy. x = xx & y = yy"
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	15	by auto
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	16
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	17	lemma eq_UU_symf: "(UU = f x) = (f x = UU)"
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	18	by auto
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	19
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	20	lemma fstream_exhaust_slen_eq: "(#x ~= 0) = (? a y. x = a~> y)"
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	21	by (simp add: slen_empty_eq fstream_exhaust_eq)
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	22
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	23	lemmas [simp] =
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	24	slen_less_1_eq fstream_exhaust_slen_eq
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	25	slen_fscons_eq slen_fscons_less_eq Suc_ile_eq
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	26
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	27	declare strictI [elim]
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	28
17293 ecf182ccc3ca converted to Isar theory format; wenzelm parents: 14981 diff changeset	29	end

author	blanchet
	Tue, 14 Feb 2012 20:13:07 +0100
changeset 46481	c7c85ff6de2a
parent 42151	4da4fc77664b
child 58880	0baae4311a9f
permissions	-rw-r--r--