author | huffman |
Tue, 02 Mar 2010 09:54:50 -0800 | |
changeset 35512 | d1ef88d7de5a |
parent 35174 | e15040ae75d7 |
permissions | -rw-r--r-- |
17293 | 1 |
(* Title: HOLCF/FOCUS/FOCUS.thy |
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 | 5 |
header {* Top level of FOCUS *} |
6 |
||
7 |
theory FOCUS |
|
8 |
imports Fstream |
|
9 |
begin |
|
10 |
||
19759 | 11 |
lemma ex_eqI [intro!]: "? xx. x = xx" |
12 |
by auto |
|
13 |
||
14 |
lemma ex2_eqI [intro!]: "? xx yy. x = xx & y = yy" |
|
15 |
by auto |
|
16 |
||
17 |
lemma eq_UU_symf: "(UU = f x) = (f x = UU)" |
|
18 |
by auto |
|
19 |
||
20 |
lemma fstream_exhaust_slen_eq: "(#x ~= 0) = (? a y. x = a~> y)" |
|
21 |
by (simp add: slen_empty_eq fstream_exhaust_eq) |
|
22 |
||
23 |
lemmas [simp] = |
|
24 |
slen_less_1_eq fstream_exhaust_slen_eq |
|
25 |
slen_fscons_eq slen_fscons_less_eq Suc_ile_eq |
|
26 |
||
27 |
declare strictI [elim] |
|
28 |
||
17293 | 29 |
end |