|
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 |
First-Order Logic: the 'if' example.
|
|
|
7 |
*)
|
|
|
8 |
|
|
16417
|
9 |
theory If imports FOL begin
|
|
14205
|
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. High-level 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
|