isabelle: src/HOLCF/FOCUS/FOCUS.ML@e135f6a1b76c (annotated)

17293 ecf182ccc3ca converted to Isar theory format; wenzelm parents: 15188 diff changeset	1	(* Title: HOLCF/FOCUS/FOCUS.ML
11355 778c369559d9 tuned wenzelm parents: 11350 diff changeset	2	ID: $Id$
17293 ecf182ccc3ca converted to Isar theory format; wenzelm parents: 15188 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: 15188 diff changeset	6	val ex_eqI = prove_goal (the_context ()) "? xx. x = xx" (K [Auto_tac]);
ecf182ccc3ca converted to Isar theory format; wenzelm parents: 15188 diff changeset	7	val ex2_eqI = prove_goal (the_context ()) "? xx yy. x = xx & y = yy" (K [Auto_tac]);
ecf182ccc3ca converted to Isar theory format; wenzelm parents: 15188 diff changeset	8	val eq_UU_symf = prove_goal (the_context ()) "(UU = f x) = (f x = UU)" (K [Auto_tac]);
11350 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	AddSIs [ex_eqI, ex2_eqI];
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	11	Addsimps[eq_UU_symf];
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	12	Goal "(#x ~= 0) = (? a y. x = a~> y)";
15188 9d57263faf9e integrated Streams with ex/Stream.; added FOCUS/Fstreams.thy oheimb* parents: 14981 diff changeset	13	by (simp_tac (simpset() addsimps [thm "slen_empty_eq", fstream_exhaust_eq]) 1);
11350 4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	14	qed "fstream_exhaust_slen_eq";
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	15
15188 9d57263faf9e integrated Streams with ex/Stream.; added FOCUS/Fstreams.thy oheimb* parents: 14981 diff changeset	16	Addsimps[thm "slen_less_1_eq", fstream_exhaust_slen_eq,
17293 ecf182ccc3ca converted to Isar theory format; wenzelm parents: 15188 diff changeset	17	thm "slen_fscons_eq", thm "slen_fscons_less_eq"];
11355 778c369559d9 tuned wenzelm parents: 11350 diff changeset	18	Addsimps[thm "Suc_ile_eq"];
11350 4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	19	AddEs [strictI];

author	wenzelm
	Tue, 10 Jan 2006 19:33:37 +0100
changeset 18638	e135f6a1b76c
parent 17293	ecf182ccc3ca
permissions	-rw-r--r--