author | huffman |
Fri, 20 Jun 2008 23:01:09 +0200 | |
changeset 27310 | d0229bc6c461 |
parent 19759 | 2d0896653e7a |
child 35174 | e15040ae75d7 |
permissions | -rw-r--r-- |
17293 | 1 |
(* Title: HOLCF/FOCUS/FOCUS.thy |
11355 | 2 |
ID: $Id$ |
17293 | 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 | 6 |
header {* Top level of FOCUS *} |
7 |
||
8 |
theory FOCUS |
|
9 |
imports Fstream |
|
10 |
begin |
|
11 |
||
19759 | 12 |
lemma ex_eqI [intro!]: "? xx. x = xx" |
13 |
by auto |
|
14 |
||
15 |
lemma ex2_eqI [intro!]: "? xx yy. x = xx & y = yy" |
|
16 |
by auto |
|
17 |
||
18 |
lemma eq_UU_symf: "(UU = f x) = (f x = UU)" |
|
19 |
by auto |
|
20 |
||
21 |
lemma fstream_exhaust_slen_eq: "(#x ~= 0) = (? a y. x = a~> y)" |
|
22 |
by (simp add: slen_empty_eq fstream_exhaust_eq) |
|
23 |
||
24 |
lemmas [simp] = |
|
25 |
slen_less_1_eq fstream_exhaust_slen_eq |
|
26 |
slen_fscons_eq slen_fscons_less_eq Suc_ile_eq |
|
27 |
||
28 |
declare strictI [elim] |
|
29 |
||
17293 | 30 |
end |