|
4382
|
1 |
|
|
|
2 |
Isabelle BUGS -- history of reported faults
|
|
|
3 |
===========================================
|
|
|
4 |
|
|
|
5 |
1. Symptom: hyp_subst_tac does nothing if the selected equality involves type
|
|
|
6 |
unknowns. Cause: it uses the simplifier, which ignores such equalities.
|
|
|
7 |
Fix: check for type unknowns in hypsubst/inspect_pair; change interface
|
|
|
8 |
function dest_eq to return the type of the equality. (lcp, 5/11/97)
|
|
|
9 |
|
|
|
10 |
2. Symptom: read_instantiate_sg has problems instantiating types in some
|
|
|
11 |
simultaneous instantiations (Message-id: <199710301432.PAA20594@sirius.Informatik.Uni-Bremen.DE> on isabelle-users)
|
|
10941
|
12 |
|
|
|
13 |
|
|
|
14 |
- res_inst_tac bug:
|
|
|
15 |
val [p1, p2] = Goalw [o_def]
|
|
|
16 |
"[| f : Funs (range g); !!h. f = g o h ==> P |] ==> P";
|
|
|
17 |
by (res_inst_tac [("h", "%x. @y. f x = g y")] p2 1);
|
|
|
18 |
by (res_inst_tac [("h", "%x. @y. (f x::'b) = g y")] p2 1);
|
|
|
19 |
^^^^ required!
|
|
|
20 |
Problem: lift_inst_rule only refers to syntactic context of current
|
|
|
21 |
dynamic proof state; old-style goal initially does not contain hyps
|
|
|
22 |
(!!);
|
|
|
23 |
|
|
|
24 |
Fix: either make assumptions statically scoped (included as hyps in
|
|
|
25 |
goal), or pass additional environment to lift_inst_rule (this would
|
|
|
26 |
improve upon Isar's res_inst_tac as well);
|
|
|
27 |
|
|
|
28 |
- type infer / inst bug:
|
|
|
29 |
Goal "x = (x::?'a)";
|
|
|
30 |
by (cut_inst_tac [("t", "x")] refl 1);
|
|
|
31 |
|
|
|
32 |
- bug in prove_goal (!?):
|
|
|
33 |
forall_elim: Variable ?uu has two distinct types
|
|
|
34 |
'a
|
|
|
35 |
'b
|
|
|
36 |
*** The exception above was raised for
|
|
|
37 |
*** (!!uu uua. PROP P (uu, uua)) ==> PROP P xa
|