14151

1 
(* Title: FOL/ex/If.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1991 University of Cambridge

14957

5 
*)

14151

6 

14957

7 
header {* FirstOrder Logic: the 'if' example *}

14151

8 

16417

9 
theory If imports FOL begin

14151

10 


11 
constdefs

19796

12 
"if" :: "[o,o,o]=>o"


13 
"if(P,Q,R) == P&Q  ~P&R"

14151

14 


15 
lemma ifI:


16 
"[ P ==> Q; ~P ==> R ] ==> if(P,Q,R)"


17 
apply (simp add: if_def, blast)


18 
done


19 


20 
lemma ifE:


21 
"[ if(P,Q,R); [ P; Q ] ==> S; [ ~P; R ] ==> S ] ==> S"


22 
apply (simp add: if_def, blast)


23 
done


24 


25 
lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) <> if(Q, if(P,A,C), if(P,B,D))"


26 
apply (rule iffI)


27 
apply (erule ifE)


28 
apply (erule ifE)


29 
apply (rule ifI)


30 
apply (rule ifI)


31 
oops


32 


33 
text{*Trying again from the beginning in order to use @{text blast}*}


34 
declare ifI [intro!]


35 
declare ifE [elim!]


36 


37 
lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) <> if(Q, if(P,A,C), if(P,B,D))"


38 
by blast


39 


40 


41 
lemma "if(if(P,Q,R), A, B) <> if(P, if(Q,A,B), if(R,A,B))"


42 
by blast


43 


44 
text{*Trying again from the beginning in order to prove from the definitions*}


45 
lemma "if(if(P,Q,R), A, B) <> if(P, if(Q,A,B), if(R,A,B))"


46 
by (simp add: if_def, blast)


47 


48 


49 
text{*An invalid formula. Highlevel rules permit a simpler diagnosis*}


50 
lemma "if(if(P,Q,R), A, B) <> if(P, if(Q,A,B), if(R,B,A))"


51 
apply auto

14957

52 
 {*The next step will fail unless subgoals remain*}

14151

53 
apply (tactic all_tac)


54 
oops


55 


56 
text{*Trying again from the beginning in order to prove from the definitions*}


57 
lemma "if(if(P,Q,R), A, B) <> if(P, if(Q,A,B), if(R,B,A))"


58 
apply (simp add: if_def, auto)

14957

59 
 {*The next step will fail unless subgoals remain*}

14151

60 
apply (tactic all_tac)


61 
oops


62 

0

63 
end
