Dear HOL-info,
I want to prove in HOL-4 Kananaskis 6, one de Morgan law:
[~(p \/ q)] |- ~p /\ ~q
After initialization, I use SUBGOAL_THEN (term -> thm_tactic -> tactic) to
introduce lemma lm1, [~(p \/ q)] |- ~q, as a first subgoal. I used to think
that
a theorem achieved by lm1 is used as an argument for thm_tactic come later. So,
if one expand current goal with
e(SUBGOAL_THEN (Term `~q`) (fn th => ASSUME_TAC th))
then I used to think that it is [~(p \/ q)] |- ~q which is supplied to
ASSUME_TAC, not [] |- ~q or [~q] |- q. (We all know that ASSUME_TAC A' |- v is
invalid unless A' is a subset for assumption of the goal it is try to expand).
But, when one execute
- e(SUBGOAL_THEN (Term `~q`)(fn th => ASSUME_TAC (DISCH_ALL th)));
OK..
2 subgoals:
> val it =
~p /\ ~q
------------------------------------
0. ~(p \/ q)
1. ~q ==> ~q
~q
------------------------------------
~(p \/ q)
: proof
It could be elicited that it is [~q] |- ~q which is actually supplied to
thm_tactic. It is confusing me since [~q], AFAIK, could not be viewed as a
subset for [~(p \/ q)].
When one try to expand initial goal by (for testing purpose)
-b();
.
.
- val qThm = ASSUME ``~q``;
> qThm = [~q] |- ~q : thm
- e(ASSUME_TAC qThm);
OK..
Exception raised at Tactical.VALID:
Invalid tactic
! Uncaught exception:
! HOL_ERR
,
it raises an exception. Hence, it is true that [~q] |- q should not be used
with
ASSUME_TAC in this case.
One might think there is something with DISCH_ALL rule, but when we define a
new
theorem (again, for testing purpose)
- prove (``~(p \/ q) ==> ~q``, RW_TAC bool_ss[]);
> val it = [] |- ~(p \/ q) ==> ~q : thm
- val iThm = UNDISCH it;
> val iThm = [~(p \/ q)] |- ~q : thm
and experiment with ASSUME_TAC-DISCH_ALL
> val it =
Initial goal:
~p /\ ~q
------------------------------------
~(p \/ q)
: proof
- e(ASSUME_TAC (DISCH_ALL iThm));
OK..
1 subgoal:
> val it =
~p /\ ~q
------------------------------------
0. ~(p \/ q)
1. ~(p \/ q) ==> ~q
: proof
What does actually happen? Is ASSUME_TAC, and generally all tactics, has
different behaviour when it comes to SUBGOAL_THEN, and generally all tacticals?
Or is it because the system does some kind of adjusment when printing response
with SUBGOAL_THEN? Or else?
Regards,
Ahmadi
NB: I hope nothing's wrong with DISCH_ALL trick, because I try DISCH_ALL to
make
theorem's argument explicit from another tactical (PAT_ASSUM), too.------------------------------------------------------------------------------
Simplify data backup and recovery for your virtual environment with vRanger.
Installation's a snap, and flexible recovery options mean your data is safe,
secure and there when you need it. Data protection magic?
Nope - It's vRanger. Get your free trial download today.
http://p.sf.net/sfu/quest-sfdev2dev
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
