src/HOL/HOLCF/FOCUS/FOCUS.thy
author wenzelm
Thu Feb 15 12:11:00 2018 +0100 (2018-02-15)
changeset 67613 ce654b0e6d69
parent 62175 8ffc4d0e652d
permissions -rw-r--r--
more symbols;
     1 (*  Title:      HOL/HOLCF/FOCUS/FOCUS.thy
     2     Author:     David von Oheimb, TU Muenchen
     3 *)
     4 
     5 section \<open>Top level of FOCUS\<close>
     6 
     7 theory FOCUS
     8 imports Fstream
     9 begin
    10 
    11 lemma ex_eqI [intro!]: "\<exists>xx. x = xx"
    12 by auto
    13 
    14 lemma ex2_eqI [intro!]: "\<exists>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 \<noteq> 0) = (\<exists>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 
    29 end