Admin/BUGS
author paulson
Wed, 25 Jul 2001 18:21:01 +0200
changeset 11455 e07927b980ec
parent 10991 2e59c831cf07
child 13447 3470596f3cd5
permissions -rw-r--r--
defer_recdef (lazyR_def) now looks for theorem Hilbert_Choice.tfl_some dynamically, so recdef no longer needs to import Hilbert_Choice.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4382
c1536da54f52 Comprehensive (??) list of bugs, fixed or not
paulson
parents:
diff changeset
     1
c1536da54f52 Comprehensive (??) list of bugs, fixed or not
paulson
parents:
diff changeset
     2
Isabelle BUGS -- history of reported faults
c1536da54f52 Comprehensive (??) list of bugs, fixed or not
paulson
parents:
diff changeset
     3
===========================================
c1536da54f52 Comprehensive (??) list of bugs, fixed or not
paulson
parents:
diff changeset
     4
c1536da54f52 Comprehensive (??) list of bugs, fixed or not
paulson
parents:
diff changeset
     5
1.  Symptom: hyp_subst_tac does nothing if the selected equality involves type
c1536da54f52 Comprehensive (??) list of bugs, fixed or not
paulson
parents:
diff changeset
     6
    unknowns.  Cause: it uses the simplifier, which ignores such equalities.
c1536da54f52 Comprehensive (??) list of bugs, fixed or not
paulson
parents:
diff changeset
     7
    Fix: check for type unknowns in hypsubst/inspect_pair;  change interface
c1536da54f52 Comprehensive (??) list of bugs, fixed or not
paulson
parents:
diff changeset
     8
    function dest_eq to return the type of the equality. (lcp, 5/11/97)
c1536da54f52 Comprehensive (??) list of bugs, fixed or not
paulson
parents:
diff changeset
     9
c1536da54f52 Comprehensive (??) list of bugs, fixed or not
paulson
parents:
diff changeset
    10
2.  Symptom: read_instantiate_sg has problems instantiating types in some
c1536da54f52 Comprehensive (??) list of bugs, fixed or not
paulson
parents:
diff changeset
    11
    simultaneous instantiations (Message-id: <199710301432.PAA20594@sirius.Informatik.Uni-Bremen.DE> on isabelle-users)
10941
6c09cae3b4ad more bugs;
wenzelm
parents: 4382
diff changeset
    12
6c09cae3b4ad more bugs;
wenzelm
parents: 4382
diff changeset
    13
6c09cae3b4ad more bugs;
wenzelm
parents: 4382
diff changeset
    14
- res_inst_tac bug:
6c09cae3b4ad more bugs;
wenzelm
parents: 4382
diff changeset
    15
val [p1, p2] = Goalw [o_def]
6c09cae3b4ad more bugs;
wenzelm
parents: 4382
diff changeset
    16
     "[| f : Funs (range g); !!h. f = g o h ==> P |] ==> P";
6c09cae3b4ad more bugs;
wenzelm
parents: 4382
diff changeset
    17
by (res_inst_tac [("h", "%x. @y. f x = g y")] p2 1);
6c09cae3b4ad more bugs;
wenzelm
parents: 4382
diff changeset
    18
by (res_inst_tac [("h", "%x. @y. (f x::'b) = g y")] p2 1);
6c09cae3b4ad more bugs;
wenzelm
parents: 4382
diff changeset
    19
                                      ^^^^ required!
6c09cae3b4ad more bugs;
wenzelm
parents: 4382
diff changeset
    20
Problem: lift_inst_rule only refers to syntactic context of current
6c09cae3b4ad more bugs;
wenzelm
parents: 4382
diff changeset
    21
dynamic proof state; old-style goal initially does not contain hyps
6c09cae3b4ad more bugs;
wenzelm
parents: 4382
diff changeset
    22
(!!);
6c09cae3b4ad more bugs;
wenzelm
parents: 4382
diff changeset
    23
6c09cae3b4ad more bugs;
wenzelm
parents: 4382
diff changeset
    24
Fix: either make assumptions statically scoped (included as hyps in
6c09cae3b4ad more bugs;
wenzelm
parents: 4382
diff changeset
    25
goal), or pass additional environment to lift_inst_rule (this would
6c09cae3b4ad more bugs;
wenzelm
parents: 4382
diff changeset
    26
improve upon Isar's res_inst_tac as well);
6c09cae3b4ad more bugs;
wenzelm
parents: 4382
diff changeset
    27
6c09cae3b4ad more bugs;
wenzelm
parents: 4382
diff changeset
    28
- type infer / inst bug:
6c09cae3b4ad more bugs;
wenzelm
parents: 4382
diff changeset
    29
Goal "x = (x::?'a)";
6c09cae3b4ad more bugs;
wenzelm
parents: 4382
diff changeset
    30
by (cut_inst_tac [("t", "x")] refl 1);
6c09cae3b4ad more bugs;
wenzelm
parents: 4382
diff changeset
    31
6c09cae3b4ad more bugs;
wenzelm
parents: 4382
diff changeset
    32
- bug in prove_goal (!?):
6c09cae3b4ad more bugs;
wenzelm
parents: 4382
diff changeset
    33
forall_elim: Variable ?uu has two distinct types
6c09cae3b4ad more bugs;
wenzelm
parents: 4382
diff changeset
    34
'a
6c09cae3b4ad more bugs;
wenzelm
parents: 4382
diff changeset
    35
'b
6c09cae3b4ad more bugs;
wenzelm
parents: 4382
diff changeset
    36
*** The exception above was raised for
6c09cae3b4ad more bugs;
wenzelm
parents: 4382
diff changeset
    37
*** (!!uu uua. PROP P (uu, uua)) ==> PROP P xa