| author | wenzelm |
| Tue, 31 Mar 2015 22:31:05 +0200 | |
| changeset 59886 | e0dc738eb08c |
| parent 59720 | f893472fff31 |
| child 66453 | cc19f7ca2ed6 |
| permissions | -rw-r--r-- |
| 59720 | 1 |
(* Title: Doc/Logics_ZF/If.thy |
| 14205 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 |
Copyright 1991 University of Cambridge |
|
4 |
||
5 |
First-Order 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. High-level 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 |