author  boehmes 
Tue, 07 Dec 2010 15:44:38 +0100  
changeset 41064  0c447a17770a 
parent 35416  d8d7d1b785af 
child 42637  381fdcab0f36 
permissions  rwrr 
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 

16417  9 
theory If imports FOL begin 
14205  10 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
19792
diff
changeset

11 
definition "if" :: "[o,o,o]=>o" where 
19792  12 
"if(P,Q,R) == P&Q  ~P&R" 
14205  13 

14 
lemma ifI: 

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

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

17 
apply (simp add: if_def) 

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

19 
apply blast 

20 
done 

21 

22 
lemma ifE: 

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

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

25 
apply (simp add: if_def) 

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

27 
apply blast 

28 
done 

29 

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

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

32 
apply (rule iffI) 

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

34 
apply (erule ifE) 

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

36 
apply (erule ifE) 

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

38 
apply (rule ifI) 

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

40 
apply (rule ifI) 

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

42 
oops 

43 

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

45 
declare ifI [intro!] 

46 
declare ifE [elim!] 

47 

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

49 
by blast 

50 

51 

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

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

54 
by blast 

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,A,B))" 

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

59 
apply (simp add: if_def) 

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

61 
apply blast 

62 
done 

63 

64 

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

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

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

68 
apply auto 

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

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

71 
apply (tactic all_tac) 

72 
oops 

73 

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

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

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

77 
apply (simp add: if_def) 

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

79 
apply (auto) 

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

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

82 
apply (tactic all_tac) 

83 
oops 

84 

85 

86 
end 