The axiom tag list only contains axioms that have been introduced within the
“current theory segment”. All theorems from other theory segments (i.e. those
previously stored to “disk”) will have an empty list of axioms, since they
cannot have been derived using axioms from the current theory segment.
You can list all axioms introduced in ancestor theories with
List.map DB.axioms (Theory.ancestry "-“)
By contrast, oracle tags are sticky. The DISK_THM tag is used to show that a
theorem has come from a stored theory, i.e. via export_theory.
So, if you have
val name = Theory.new_axiom (“name", ..)
in the current theory segment then (while that segment is still active) the
“name” axiom tag will appear in all theorems derived using this axiom. However,
once this theory is stored, only the existence of the axiom is recorded.
If you have
val name = Thm.mk_oracle_thm “name” (.., ..)
then the “name” oracle tag will always appear in the tags of all theorems
derived with this theorem (even after storing the theorems to disk).
Things have recently become a bit more complicated with holyhammer, which uses
special tags to keep track of all theorem dependencies. However, this
information is not printed when showing the normal tags. For your example, you
can see the connection with
> Tag.dep_of (Thm.tag boolTheory.AND_CLAUSES);
val it = DEP_SAVED (("bool", 51), [("bool", [0, 3, 26, 27, 39])]): Dep.dep
> Tag.dep_of (Thm.tag IMP_ANTISYM_AX);
val it = DEP_SAVED (("bool", 26), [("bool", [0, 4, 5, 13])]): Dep.dep
> Tag.dep_of (Thm.tag boolTheory.BOOL_CASES_AX);
val it = DEP_SAVED (("bool", 13), []): Dep.dep
>
i.e. theorem 51 (AND_CLAUSES) depends on theorem 26 (MP_ANTISYM_AX), which in
turn depends on theorem 13 (BOOL_CASES_AX).
Anthony
> On 4 Dec 2015, at 13:44, Andrea Condoluci <[email protected]> wrote:
>
> Hi all,
>
> Let's consider any theorem that depends on the BOOL_CASES_AX. For example,
> from the HOL Reference:
>
> > [AND_CLAUSES] Theorem
> >
> > [oracles: ] [axioms: BOOL_CASES_AX] []
> > |- !t.
> > (T /\ t <=> t) /\ (t /\ T <=> t) /\ (F /\ t <=> F) /\
> > (t /\ F <=> F) /\ (t /\ t <=> t)
>
> But if now I display in my HOL system the theorem, with the option "show_tags
> := true", this is what I get:
>
> > val it =
> > [oracles: DISK_THM] [axioms: ] []
> > |- ∀t.
> > (T ∧ t ⇔ t) ∧ (t ∧ T ⇔ t) ∧ (F ∧ t ⇔ F) ∧ (t ∧ F ⇔ F) ∧ (t ∧ t ⇔ t)
>
> How comes the axiom is not displayed, and there is a "DISK_THM" oracle
> instead?
>
> Thank you,
> 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
