author | wenzelm |
Mon, 03 Nov 1997 12:24:13 +0100 | |
changeset 4091 | 771b1f6422a8 |
parent 3141 | 2791aa6dc1bd |
child 5050 | e925308df78b |
permissions | -rw-r--r-- |
1459 | 1 |
(* Title: FOL/ex/if |
0 | 2 |
ID: $Id$ |
1459 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1991 University of Cambridge |
5 |
||
3141 | 6 |
First-Order Logic: the 'if' example |
0 | 7 |
*) |
8 |
||
9 |
open If; |
|
2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2486
diff
changeset
|
10 |
open Cla; (*in case structure IntPr is open!*) |
0 | 11 |
|
12 |
val prems = goalw If.thy [if_def] |
|
13 |
"[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)"; |
|
4091 | 14 |
by (blast_tac (claset() addIs prems) 1); |
725 | 15 |
qed "ifI"; |
0 | 16 |
|
17 |
val major::prems = goalw If.thy [if_def] |
|
18 |
"[| if(P,Q,R); [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S"; |
|
19 |
by (cut_facts_tac [major] 1); |
|
4091 | 20 |
by (blast_tac (claset() addIs prems) 1); |
725 | 21 |
qed "ifE"; |
0 | 22 |
|
23 |
||
24 |
goal If.thy |
|
25 |
"if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"; |
|
1459 | 26 |
by (rtac iffI 1); |
27 |
by (etac ifE 1); |
|
28 |
by (etac ifE 1); |
|
29 |
by (rtac ifI 1); |
|
30 |
by (rtac ifI 1); |
|
0 | 31 |
|
32 |
choplev 0; |
|
2469 | 33 |
AddSIs [ifI]; |
34 |
AddSEs [ifE]; |
|
3141 | 35 |
by (Blast_tac 1); |
755 | 36 |
qed "if_commute"; |
0 | 37 |
|
38 |
||
39 |
goal If.thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"; |
|
3141 | 40 |
by (Blast_tac 1); |
755 | 41 |
qed "nested_ifs"; |
0 | 42 |
|
43 |
choplev 0; |
|
1459 | 44 |
by (rewtac if_def); |
3141 | 45 |
by (blast_tac FOL_cs 1); |
0 | 46 |
result(); |
47 |
||
48 |
||
49 |
(*An invalid formula. High-level rules permit a simpler diagnosis*) |
|
50 |
goal If.thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))"; |
|
3141 | 51 |
by (Blast_tac 1) handle ERROR => writeln"Failed, as expected"; |
0 | 52 |
(*Check that subgoals remain: proof failed.*) |
53 |
getgoal 1; |
|
2469 | 54 |
by (REPEAT (Step_tac 1)); |
0 | 55 |
|
56 |
choplev 0; |
|
1459 | 57 |
by (rewtac if_def); |
3141 | 58 |
by (blast_tac FOL_cs 1) handle ERROR => writeln"Failed, as expected"; |
0 | 59 |
(*Check that subgoals remain: proof failed.*) |
60 |
getgoal 1; |
|
61 |
by (REPEAT (step_tac FOL_cs 1)); |
|
62 |
||
63 |
||
64 |
||
65 |
writeln"Reached end of file."; |