14205

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


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1991 University of Cambridge


5 


6 
FirstOrder Logic: the 'if' example.


7 
*)


8 


9 
theory If = FOL:


10 


11 
constdefs


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


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


14 


15 
lemma ifI:


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


17 
{* @{subgoals[display,indent=0,margin=65]} *}


18 
apply (simp add: if_def)


19 
{* @{subgoals[display,indent=0,margin=65]} *}


20 
apply blast


21 
done


22 


23 
lemma ifE:


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


25 
{* @{subgoals[display,indent=0,margin=65]} *}


26 
apply (simp add: if_def)


27 
{* @{subgoals[display,indent=0,margin=65]} *}


28 
apply blast


29 
done


30 


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


32 
{* @{subgoals[display,indent=0,margin=65]} *}


33 
apply (rule iffI)


34 
{* @{subgoals[display,indent=0,margin=65]} *}


35 
apply (erule ifE)


36 
{* @{subgoals[display,indent=0,margin=65]} *}


37 
apply (erule ifE)


38 
{* @{subgoals[display,indent=0,margin=65]} *}


39 
apply (rule ifI)


40 
{* @{subgoals[display,indent=0,margin=65]} *}


41 
apply (rule ifI)


42 
{* @{subgoals[display,indent=0,margin=65]} *}


43 
oops


44 


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


46 
declare ifI [intro!]


47 
declare ifE [elim!]


48 


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


50 
by blast


51 


52 


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


54 
{* @{subgoals[display,indent=0,margin=65]} *}


55 
by blast


56 


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


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


59 
{* @{subgoals[display,indent=0,margin=65]} *}


60 
apply (simp add: if_def)


61 
{* @{subgoals[display,indent=0,margin=65]} *}


62 
apply blast


63 
done


64 


65 


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


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


68 
{* @{subgoals[display,indent=0,margin=65]} *}


69 
apply auto


70 
{* @{subgoals[display,indent=0,margin=65]} *}


71 
(*The next step will fail unless subgoals remain*)


72 
apply (tactic all_tac)


73 
oops


74 


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


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


77 
{* @{subgoals[display,indent=0,margin=65]} *}


78 
apply (simp add: if_def)


79 
{* @{subgoals[display,indent=0,margin=65]} *}


80 
apply (auto)


81 
{* @{subgoals[display,indent=0,margin=65]} *}


82 
(*The next step will fail unless subgoals remain*)


83 
apply (tactic all_tac)


84 
oops


85 


86 


87 
end
