author  wenzelm 
Sat, 05 Apr 2014 15:03:40 +0200  
changeset 56421  1ffd7eaa778b 
parent 50530  6266e44b3396 
permissions  rwrr 
50530  1 
(* Title: Doc/ZF/If.thy 
14205  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
3 
Copyright 1991 University of Cambridge 

4 

5 
FirstOrder Logic: the 'if' example. 

6 
*) 

7 

48517  8 
theory If imports "~~/src/FOL/FOL" begin 
14205  9 

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

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

13 
lemma ifI: 

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

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

16 
apply (simp add: if_def) 

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

18 
apply blast 

19 
done 

20 

21 
lemma ifE: 

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

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

24 
apply (simp add: if_def) 

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

26 
apply blast 

27 
done 

28 

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

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

31 
apply (rule iffI) 

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

33 
apply (erule ifE) 

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

35 
apply (erule ifE) 

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

37 
apply (rule ifI) 

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

39 
apply (rule ifI) 

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

41 
oops 

42 

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

44 
declare ifI [intro!] 

45 
declare ifE [elim!] 

46 

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

48 
by blast 

49 

50 

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

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

53 
by blast 

54 

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

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

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

58 
apply (simp add: if_def) 

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

60 
apply blast 

61 
done 

62 

63 

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

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

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

67 
apply auto 

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

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

70 
apply (tactic all_tac) 

71 
oops 

72 

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

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

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

76 
apply (simp add: if_def) 

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

78 
apply (auto) 

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

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

81 
apply (tactic all_tac) 

82 
oops 

83 

84 

85 
end 