| author | wenzelm |
| Thu, 18 Aug 2005 11:17:46 +0200 | |
| changeset 17111 | d2ea9c974570 |
| parent 15188 | 9d57263faf9e |
| child 17293 | ecf182ccc3ca |
| permissions | -rw-r--r-- |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
1 |
(* Title: HOLCF/FOCUS/FOCUS.ML |
| 11355 | 2 |
ID: $Id$ |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
3 |
Author: David von Oheimb, TU Muenchen |
|
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 |
|
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
6 |
val ex_eqI = prove_goal thy "? xx. x = xx" (K [Auto_tac]); |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
7 |
val ex2_eqI = prove_goal thy "? xx yy. x = xx & y = yy" (K [Auto_tac]); |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
8 |
val eq_UU_symf = prove_goal thy "(UU = f x) = (f x = UU)" (K [Auto_tac]); |
|
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, |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
14981
diff
changeset
|
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]; |