Dear HOL-info list,
I am new to HOL4 and to the list - apologies for any inherent mistakes
in my questions or examples.
I am trying to learn more on term substitution and SUBST in particular.
Based on pen and paper exercises from a format methods course, I wrote
the solutions in HOL4:
(* ================================================================== *)
(* Prove `|- (A ==> A)` *)
(* ================================================================== *)
(* ================================================================== *)
(* The 3 axioms introduced in the formal methods course *)
(* ================================================================== *)
val ax1 = new_axiom("ax1", Term `A ==> (B ==> A)`);
val ax2 = new_axiom("ax2", Term `(A ==> (B ==> C)) ==> ((A ==> B) ==> (A
==> C))`);
val ax3 = new_axiom("ax3", Term `(~A ==> ~B) ==> (B ==> A)`);
val subst_th1_1_B = new_axiom("subst_th1_1_B", Term `B = (B ==> A)`);
val b = Term `b`;
val th1_1 = SUBST [
inst [alpha |-> Type`:bool`] (b) |-> INST_TYPE [alpha |->
Type`:bool`] subst_th1_1_B
]
(* TODO: use "concl ax1" and replace B with b. How to do it? *)
(--`A ==> (b ==> A)`--)
(INST_TYPE [alpha |-> Type`:bool`] ax1);
val subst_th1_2_B = new_axiom("subst_th1_2_B", Term `B = (B ==> A)`);
val subst_th1_2_C = new_axiom("subst_th1_2_C", Term `C = A`);
val b = Term `b`;
val c = Term `c`;
val th1_2 = SUBST [
inst [alpha |-> Type`:bool`] (b) |-> INST_TYPE [alpha |->
Type`:bool`] subst_th1_2_B,
inst [alpha |-> Type`:bool`] (c) |-> INST_TYPE [alpha |->
Type`:bool`] subst_th1_2_C
]
(* TODO: use "concl ax2" and replace B with b and C with c. How to
do it? *)
(--`(A ==> (b ==> c)) ==> ((A ==> b) ==> (A ==> c))`--)
(INST_TYPE [alpha |-> Type`:bool`] ax2);
val th1_3 = MP th1_2 th1_1;
val th1_4 = ax1;
val th1_5 = MP th1_3 th1_4;
--------------------
a) Why SUBST cannot work on abstract types (e.g. 'a or alpha), but
requires explicit type instantiations, to :bool for example, even though
the result of the SUBST can still be of abstract type?
--------------------
b) How could the substitution theorem be written more elegantly without
using the new_axiom() "hack"? What is the proper/usual/recommended way
to supply such substitution theorems to the SUBST in a more complex
theory where dynamically generated substitutions might be necessary?
--------------------
c) What is a proper/usual/recommended way to write the template term
based on the axiom/theorem it is supposed to match against?
In current examples I hard-coded them manually (i.e. (--`A ==> (b ==>
A)`--) ). Most importantly it was possible to do that only because
knowing in advance the structure of the axiom/theorem to match (i.e.
ax1), so the template was merely a copy-paste.
The question of this point more relates to the more generic situation
where the axiom/theorem is a "dynamically generated" one, and where we
know that we might have a sub-term `A`, which we want to mark in the
template with `a` for being substituted - how can such templates be
generated?
My main thoughts are on the direction of using `concl thrm_to_match` and
`match_term` constructs, but I am still fuzzy.
--------------------
d) For the supplied example, which is forward-proof style, could someone
help with some hints towards tactics (like MP_TAC, SUBST_TAC,
REWRITE_TAC) and the way to use in order to goal-oriented prove the
theorem in the initial example?
--------------------
Thank you for any hints, suggestions and working examples.
PS: Apologies for the lengthy post.
Kind regards,
Andrei Costin
------------------------------------------------------------------------------
Precog is a next-generation analytics platform capable of advanced
analytics on semi-structured data. The platform includes APIs for building
apps and a phenomenal toolset for data science. Developers can use
our toolset for easy data analysis & visualization. Get a free account!
http://www2.precog.com/precogplatform/slashdotnewsletter
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
