src/HOL/HOLCF/FOCUS/FOCUS.thy
author huffman
Sat Nov 27 16:08:10 2010 -0800 (2010-11-27)
changeset 40774 0437dbc127b3
parent 35174 src/HOLCF/FOCUS/FOCUS.thy@e15040ae75d7
child 42151 4da4fc77664b
permissions -rw-r--r--
moved directory src/HOLCF to src/HOL/HOLCF;
added HOLCF theories to src/HOL/IsaMakefile;
     1 (*  Title:      HOLCF/FOCUS/FOCUS.thy
     2     Author:     David von Oheimb, TU Muenchen
     3 *)
     4 
     5 header {* Top level of FOCUS *}
     6 
     7 theory FOCUS
     8 imports Fstream
     9 begin
    10 
    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 
    29 end