src/HOL/HOLCF/FOCUS/FOCUS.thy
author wenzelm
Sun Sep 18 20:33:48 2016 +0200 (2016-09-18)
changeset 63915 bab633745c7f
parent 62175 8ffc4d0e652d
child 67613 ce654b0e6d69
permissions -rw-r--r--
tuned proofs;
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/FOCUS/FOCUS.thy
wenzelm@17293
     2
    Author:     David von Oheimb, TU Muenchen
oheimb@11350
     3
*)
oheimb@11350
     4
wenzelm@62175
     5
section \<open>Top level of FOCUS\<close>
wenzelm@17293
     6
wenzelm@17293
     7
theory FOCUS
wenzelm@17293
     8
imports Fstream
wenzelm@17293
     9
begin
wenzelm@17293
    10
huffman@19759
    11
lemma ex_eqI [intro!]: "? xx. x = xx"
huffman@19759
    12
by auto
huffman@19759
    13
huffman@19759
    14
lemma ex2_eqI [intro!]: "? xx yy. x = xx & y = yy"
huffman@19759
    15
by auto
huffman@19759
    16
huffman@19759
    17
lemma eq_UU_symf: "(UU = f x) = (f x = UU)"
huffman@19759
    18
by auto
huffman@19759
    19
huffman@19759
    20
lemma fstream_exhaust_slen_eq: "(#x ~= 0) = (? a y. x = a~> y)"
huffman@19759
    21
by (simp add: slen_empty_eq fstream_exhaust_eq)
huffman@19759
    22
huffman@19759
    23
lemmas [simp] =
huffman@19759
    24
  slen_less_1_eq fstream_exhaust_slen_eq
huffman@19759
    25
  slen_fscons_eq slen_fscons_less_eq Suc_ile_eq
huffman@19759
    26
huffman@19759
    27
declare strictI [elim]
huffman@19759
    28
wenzelm@17293
    29
end