author wenzelm
Mon, 29 Jan 2001 14:14:03 +0100
changeset 10991 2e59c831cf07
parent 10941 6c09cae3b4ad
child 13447 3470596f3cd5
permissions -rw-r--r--
*** empty log message ***

Isabelle BUGS -- history of reported faults

1.  Symptom: hyp_subst_tac does nothing if the selected equality involves type
    unknowns.  Cause: it uses the simplifier, which ignores such equalities.
    Fix: check for type unknowns in hypsubst/inspect_pair;  change interface
    function dest_eq to return the type of the equality. (lcp, 5/11/97)

2.  Symptom: read_instantiate_sg has problems instantiating types in some
    simultaneous instantiations (Message-id: <199710301432.PAA20594@sirius.Informatik.Uni-Bremen.DE> on isabelle-users)

- res_inst_tac bug:
val [p1, p2] = Goalw [o_def]
     "[| f : Funs (range g); !!h. f = g o h ==> P |] ==> P";
by (res_inst_tac [("h", "%x. @y. f x = g y")] p2 1);
by (res_inst_tac [("h", "%x. @y. (f x::'b) = g y")] p2 1);
                                      ^^^^ required!
Problem: lift_inst_rule only refers to syntactic context of current
dynamic proof state; old-style goal initially does not contain hyps

Fix: either make assumptions statically scoped (included as hyps in
goal), or pass additional environment to lift_inst_rule (this would
improve upon Isar's res_inst_tac as well);

- type infer / inst bug:
Goal "x = (x::?'a)";
by (cut_inst_tac [("t", "x")] refl 1);

- bug in prove_goal (!?):
forall_elim: Variable ?uu has two distinct types
*** The exception above was raised for
*** (!!uu uua. PROP P (uu, uua)) ==> PROP P xa