isabelle: src/HOL/HOLCF/FOCUS/FOCUS.thy@e4fae2227594 (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
62175 8ffc4d0e652d isabelle update_cartouches -c -t; wenzelm parents: 58880 diff changeset	5	section \<open>Top level of FOCUS\<close>
17293 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
67613 ce654b0e6d69 more symbols; wenzelm parents: 62175 diff changeset	11	lemma ex_eqI [intro!]: "\<exists>xx. x = xx"
19759 2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	12	by auto
2d0896653e7a removed legacy ML scripts huffman parents: 17293 diff changeset	13
67613 ce654b0e6d69 more symbols; wenzelm parents: 62175 diff changeset	14	lemma ex2_eqI [intro!]: "\<exists>xx yy. x = xx & y = yy"
19759 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
67613 ce654b0e6d69 more symbols; wenzelm parents: 62175 diff changeset	20	lemma fstream_exhaust_slen_eq: "(#x \<noteq> 0) = (\<exists>a y. x = a~> y)"
19759 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	haftmann
	Sun, 27 Jul 2025 17:52:06 +0200
changeset 82909	e4fae2227594
parent 67613	ce654b0e6d69
permissions	-rw-r--r--