| author | oheimb |
| Thu, 30 Aug 2001 15:47:30 +0200 | |
| changeset 11507 | 4b32a46ffd29 |
| parent 11355 | 778c369559d9 |
| child 12039 | ef2a6fdd3564 |
| 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 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
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 |
|
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
7 |
open FOCUS; |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
8 |
|
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
9 |
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
|
10 |
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
|
11 |
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
|
12 |
|
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
13 |
AddSIs [ex_eqI, ex2_eqI]; |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
14 |
Addsimps[eq_UU_symf]; |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
15 |
Goal "(#x ~= 0) = (? a y. x = a~> y)"; |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
16 |
by (simp_tac (simpset() addsimps [slen_empty_eq, fstream_exhaust_eq]) 1); |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
17 |
qed "fstream_exhaust_slen_eq"; |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
18 |
|
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
19 |
Addsimps[slen_less_1_eq, fstream_exhaust_slen_eq, |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
20 |
slen_fscons_eq, slen_fscons_less_eq]; |
| 11355 | 21 |
Addsimps[thm "Suc_ile_eq"]; |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
22 |
AddEs [strictI]; |