| author | kleing |
| Tue, 13 May 2003 08:59:21 +0200 | |
| changeset 14024 | 213dcc39358f |
| parent 12039 | ef2a6fdd3564 |
| child 14981 | e73f8140af78 |
| 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 |
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
|
8 |
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
|
9 |
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
|
10 |
|
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
11 |
AddSIs [ex_eqI, ex2_eqI]; |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
12 |
Addsimps[eq_UU_symf]; |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
13 |
Goal "(#x ~= 0) = (? a y. x = a~> y)"; |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
14 |
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
|
15 |
qed "fstream_exhaust_slen_eq"; |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
16 |
|
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
17 |
Addsimps[slen_less_1_eq, fstream_exhaust_slen_eq, |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
18 |
slen_fscons_eq, slen_fscons_less_eq]; |
| 11355 | 19 |
Addsimps[thm "Suc_ile_eq"]; |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
20 |
AddEs [strictI]; |