author | wenzelm |
Wed, 13 Jan 2016 23:07:06 +0100 | |
changeset 62175 | 8ffc4d0e652d |
parent 58880 | 0baae4311a9f |
child 67613 | ce654b0e6d69 |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/FOCUS/FOCUS.thy |
17293 | 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 | 5 |
section \<open>Top level of FOCUS\<close> |
17293 | 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 |