author | wenzelm |
Tue, 06 Sep 2005 21:51:17 +0200 | |
changeset 17293 | ecf182ccc3ca |
parent 15188 | 9d57263faf9e |
permissions | -rw-r--r-- |
17293 | 1 |
(* Title: HOLCF/FOCUS/FOCUS.ML |
11355 | 2 |
ID: $Id$ |
17293 | 3 |
Author: David von Oheimb, TU Muenchen |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
4 |
*) |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
5 |
|
17293 | 6 |
val ex_eqI = prove_goal (the_context ()) "? xx. x = xx" (K [Auto_tac]); |
7 |
val ex2_eqI = prove_goal (the_context ()) "? xx yy. x = xx & y = yy" (K [Auto_tac]); |
|
8 |
val eq_UU_symf = prove_goal (the_context ()) "(UU = f x) = (f x = UU)" (K [Auto_tac]); |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
9 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
10 |
AddSIs [ex_eqI, ex2_eqI]; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
11 |
Addsimps[eq_UU_symf]; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
12 |
Goal "(#x ~= 0) = (? a y. x = a~> y)"; |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
14981
diff
changeset
|
13 |
by (simp_tac (simpset() addsimps [thm "slen_empty_eq", fstream_exhaust_eq]) 1); |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
14 |
qed "fstream_exhaust_slen_eq"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
15 |
|
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
14981
diff
changeset
|
16 |
Addsimps[thm "slen_less_1_eq", fstream_exhaust_slen_eq, |
17293 | 17 |
thm "slen_fscons_eq", thm "slen_fscons_less_eq"]; |
11355 | 18 |
Addsimps[thm "Suc_ile_eq"]; |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
19 |
AddEs [strictI]; |