Theory If
section ‹First-Order Logic: the 'if' example›
theory If
imports FOL
begin
definition "if" :: ‹[o,o,o]=>o›
where ‹if(P,Q,R) ≡ P ∧ Q ∨ ¬ P ∧ R›
lemma ifI: ‹⟦P ⟹ Q; ¬ P ⟹ R⟧ ⟹ if(P,Q,R)›
unfolding if_def by blast
lemma ifE: ‹⟦if(P,Q,R); ⟦P; Q⟧ ⟹ S; ⟦¬ P; R⟧ ⟹ S⟧ ⟹ S›
unfolding if_def by blast
lemma if_commute: ‹if(P, if(Q,A,B), if(Q,C,D)) ⟷ if(Q, if(P,A,C), if(P,B,D))›
apply (rule iffI)
apply (erule ifE)
apply (erule ifE)
apply (rule ifI)
apply (rule ifI)
oops
text‹Trying again from the beginning in order to use ‹blast››
declare ifI [intro!]
declare ifE [elim!]
lemma if_commute: ‹if(P, if(Q,A,B), if(Q,C,D)) ⟷ if(Q, if(P,A,C), if(P,B,D))›
by blast
lemma ‹if(if(P,Q,R), A, B) ⟷ if(P, if(Q,A,B), if(R,A,B))›
by blast
text‹Trying again from the beginning in order to prove from the definitions›
lemma ‹if(if(P,Q,R), A, B) ⟷ if(P, if(Q,A,B), if(R,A,B))›
unfolding if_def by blast
text ‹An invalid formula. High-level rules permit a simpler diagnosis.›
lemma ‹if(if(P,Q,R), A, B) ⟷ if(P, if(Q,A,B), if(R,B,A))›
apply auto
apply (tactic all_tac)
oops
text ‹Trying again from the beginning in order to prove from the definitions.›
lemma ‹if(if(P,Q,R), A, B) ⟷ if(P, if(Q,A,B), if(R,B,A))›
unfolding if_def
apply auto
apply (tactic all_tac)
oops
end