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