Thanks for the help Anthony!
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
Il giorno ven 4 dic 2015 alle ore 17:26 Anthony Fox <[email protected]> ha
scritto:
> 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
