(* Title: HOL/HOLCF/FOCUS/FOCUS.thy Author: David von Oheimb, TU Muenchen *) section ‹Top level of FOCUS› theory FOCUS imports Fstream begin lemma ex_eqI [intro!]: "∃xx. x = xx" by auto lemma ex2_eqI [intro!]: "∃xx yy. x = xx & y = yy" by auto lemma eq_UU_symf: "(UU = f x) = (f x = UU)" by auto lemma fstream_exhaust_slen_eq: "(#x ≠ 0) = (∃a y. x = a~> y)" by (simp add: slen_empty_eq fstream_exhaust_eq) lemmas [simp] = slen_less_1_eq fstream_exhaust_slen_eq slen_fscons_eq slen_fscons_less_eq Suc_ile_eq declare strictI [elim] end