src/HOL/HOLCF/FOCUS/FOCUS.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 42151 4da4fc77664b
child 58880 0baae4311a9f
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42151
4da4fc77664b tuned headers;
wenzelm
parents: 40774
diff changeset
     1
(*  Title:      HOL/HOLCF/FOCUS/FOCUS.thy
17293
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     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
17293
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     5
header {* Top level of FOCUS *}
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     6
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     7
theory FOCUS
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     8
imports Fstream
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     9
begin
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    10
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    11
lemma ex_eqI [intro!]: "? xx. x = xx"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    12
by auto
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    13
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    14
lemma ex2_eqI [intro!]: "? xx yy. x = xx & y = yy"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    15
by auto
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    16
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    17
lemma eq_UU_symf: "(UU = f x) = (f x = UU)"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    18
by auto
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    19
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    20
lemma fstream_exhaust_slen_eq: "(#x ~= 0) = (? a y. x = a~> y)"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    21
by (simp add: slen_empty_eq fstream_exhaust_eq)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    22
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    23
lemmas [simp] =
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    24
  slen_less_1_eq fstream_exhaust_slen_eq
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    25
  slen_fscons_eq slen_fscons_less_eq Suc_ile_eq
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    26
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    27
declare strictI [elim]
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    28
17293
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    29
end