This issue seems to be related to the fact that we had
val EXCLUDED_MIDDLE = save_thm(
"EXCLUDED_MIDDLE”, ...)
followed by
val _ = save_thm("EXCLUDED_MIDDLE",EXCLUDED_MIDDLE)
in boolScript.sml.
This meant that the saved theorem “EXCLUDED_MIDDLE” (id 30) depended on an
unsaved/overwritten theorem (id 29). NOT_CLAUSES also depended on id 29, so a
lookup failed because this theorem wasn’t being saved with the theory. (The
same sort of thing was happening throughout boolTheory.)
I’ve updated the script file to avoid instances of “val _ = save_thm”. This
means that we now get
> boolTheory.NOT_CLAUSES |> Thm.tag |> Tag.dep_of |> Dep.depidl_of;
val it =
[("bool", 25), ("bool", 26), ("bool", 27), ("bool", 29), ("bool", 46),
("bool", 47)]: Dep.depid list
> List.map hhWriter.thm_of_depid it
val it =
[("TRUTH", |- T),
("IMP_ANTISYM_AX",
|- ∀t1 t2. (t1 ⇒ t2) ⇒ (t2 ⇒ t1) ⇒ (t1 ⇔ t2)),
("FALSITY", |- ∀t. F ⇒ t),
("EXCLUDED_MIDDLE", |- ∀t. t ∨ ¬t),
("IMP_F", |- ∀t. (t ⇒ F) ⇒ ¬t),
("F_IMP", |- ∀t. ¬t ⇒ t ⇒ F)]:
(string * thm) list
I’m not sure if it makes sense to think about exporting the theory in such a
way that references to unsaved theorems are eliminated. Thibault Gauthier is
better placed to discuss this issue.
Anthony
> On 6 Dec 2015, at 14:51, Andrea Condoluci <[email protected]> wrote:
>
> I now have a problem w/ dependencies: some theorems depend on things that do
> not appear to exist (?)
> For example:
> - boolTheory.NOT_CLAUSES |> Thm.tag |> Tag.dep_of |> Dep.depidl_of;
> > val it = [("bool", 0), ("bool", 6), ("bool", 26), ("bool", 27), ("bool",
> > 29)]
> - hhWriter.thm_of_depid ("bool", 29);
> ! Uncaught exception:
> ! HOL_ERR
>
> Why this?
>
> Andrea
>
------------------------------------------------------------------------------
Go from Idea to Many App Stores Faster with Intel(R) XDK
Give your users amazing mobile app experiences with Intel(R) XDK.
Use one codebase in this all-in-one HTML5 development environment.
Design, debug & build mobile apps & 2D/3D high-impact games for multiple OSs.
http://pubads.g.doubleclick.net/gampad/clk?id=254741911&iu=/4140
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
