On 23/06/11 21:00, Ahmadi Agra wrote: > 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.
Just one comment about notation. We use
[...] |- g
to refer to theorems. When you are talking about goal states (i.e., things
that are as yet unproven), our standard is to use the ?- "turnstile". Thus, I
would say that your first subgoal is
~(p \/ q) ?- ~q
> 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)].
I agree that this might appear confusing. As your experiments have revealed,
the first sub-goal does indeed get
[~q] |- ~q
as the extra theorem to use. This may appear invalid because ~q is not a
subset of the existing assumptions. However, the point is that invalidity is a
notion that is applied to all of the generated sub-goals and the way in which
the resulting theorems are combined, not a single sub-goal in isolation. In
this case, let's imagine you hadn't used DISCH_ALL. Then your subgoals would be
[~q, ~(p \/ q)] ?- ~p /\ ~q
and
[~(p \/ q)] ?- ~q
Let's also imagine that you successfully turned these goals into theorems:
[~q, ~(p \/ q)] |- ~p /\ ~q
and
[~(p \/ q)] |- ~q
The implementation of SUBGOAL_THEN then combines these theorems using PROVE_HYP
(the "cut" rule). The extra ~q assumption in the first theorem is eliminated,
and the resulting theorem is
[~(p \/ q)] |- ~p /\ ~q
as desired.
> 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?
Else :)
> 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.
Yes, using DISCH_ALL is probably a mistake in the context of tactics. In
particular, in this case you turn a useful assumption (~q) into a useless one
(~q ==> ~q).
If you want to use DISCH_ALL and similar functions, you should probably stick
to forward proof:
ASSUME ``~(p \/ q)``
|> NOT_ELIM
|> C MP (DISJ2 ``p:bool`` (ASSUME ``q:bool``))
|> DISCH ``q:bool``
|> NOT_INTRO
Of course, tactics are implemented in terms of forward proof underneath.
Moreover using DISCH_ALL "badly" will only give you the wrong theorems, or
unsolvable goals; it won't let you derive false theorems.
Michael
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ All the data continuously generated in your IT infrastructure contains a definitive record of customers, application performance, security threats, fraudulent activity and more. Splunk takes this data and makes sense of it. Business sense. IT sense. Common sense.. http://p.sf.net/sfu/splunk-d2d-c1
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
