CODEWITHSUNDEEP
logicisabelle
IIM
IIM

Reputation: 533

Using an 'if and only if' rule to prove an 'if' statement (in Isabelle)

I am trying to use a limited set of rules to prove a lemma in Isabelle using the apply method. This set of rules contains disj_not1 which is (P --> Q) = (\<not> P \/ Q).

I had the subgoal (P --> Q) ==> (\<not> P \/ Q), so I thought 'Aha! Here is a place for me to use my rule disj_not1'. But unfortunately, disj_not1 is an 'if and only if' rule not an 'if' rule, and Isabelle objects. Yet the 'if and only if' rule should be enough to prove it (more than enough really). Is this possible, and if so, how can it be done?

Upvotes: 1

Views: 282

Answers (2)

chris
chris

Reputation: 5018

What I sometimes do in such situations is to create the required rule in an ad hoc fashion as follows:

apply (rule disj_not1 [THEN iffD1])

where iffD1 is the fact

?Q = ?P ⟹ ?Q ⟹ ?P

If you need the direction from right to left, you can use iffD2 instead.

Upvotes: 1

Manuel Eberl
Manuel Eberl

Reputation: 8248

There is the subst method. apply (subst foo) will apply an equational rule by rewriting the first instance of the left-hand side of the rule in the goal with the corresponding instance of the right-hand side. You can specify other occurrences with subst (2 3) e.g. to rewrite the second and third occurrence. In order to rewrite in the assumptions of the current goal, you need to do subst (asm). To rewrite the second occurrence in an assumption, write subst (asm) (2).

Upvotes: 3

Related Questions