3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 |
5 |
6 Simplification data for FOL |
6 Simplification data for FOL |
7 *) |
7 *) |
|
8 |
|
9 (*** Addition of rules to simpsets and clasets simultaneously ***) (* FIXME move to Provers/clasimp.ML? *) |
|
10 |
|
11 infix 4 addIffs delIffs; |
|
12 |
|
13 (*Takes UNCONDITIONAL theorems of the form A<->B to |
|
14 the Safe Intr rule B==>A and |
|
15 the Safe Destruct rule A==>B. |
|
16 Also ~A goes to the Safe Elim rule A ==> ?R |
|
17 Failing other cases, A is added as a Safe Intr rule*) |
|
18 local |
|
19 fun addIff ((cla, simp), th) = |
|
20 (case FOLogic.dest_Trueprop (#prop (rep_thm th)) of |
|
21 (Const("Not", _) $ A) => |
|
22 cla addSEs [zero_var_indexes (th RS notE)] |
|
23 | (Const("op <->", _) $ _ $ _) => |
|
24 cla addSIs [zero_var_indexes (th RS iffD2)] |
|
25 addSDs [zero_var_indexes (th RS iffD1)] |
|
26 | _ => cla addSIs [th], |
|
27 simp addsimps [th]) |
|
28 handle TERM _ => error ("AddIffs: theorem must be unconditional\n" ^ |
|
29 string_of_thm th); |
|
30 |
|
31 fun delIff ((cla, simp), th) = |
|
32 (case FOLogic.dest_Trueprop (#prop (rep_thm th)) of |
|
33 (Const ("Not", _) $ A) => |
|
34 cla delrules [zero_var_indexes (th RS notE)] |
|
35 | (Const("op <->", _) $ _ $ _) => |
|
36 cla delrules [zero_var_indexes (th RS iffD2), |
|
37 cla_make_elim (zero_var_indexes (th RS iffD1))] |
|
38 | _ => cla delrules [th], |
|
39 simp delsimps [th]) |
|
40 handle TERM _ => (warning("DelIffs: ignoring conditional theorem\n" ^ |
|
41 string_of_thm th); (cla, simp)); |
|
42 |
|
43 fun store_clasimp (cla, simp) = (claset_ref () := cla; simpset_ref () := simp) |
|
44 in |
|
45 val op addIffs = foldl addIff; |
|
46 val op delIffs = foldl delIff; |
|
47 fun AddIffs thms = store_clasimp ((claset (), simpset ()) addIffs thms); |
|
48 fun DelIffs thms = store_clasimp ((claset (), simpset ()) delIffs thms); |
|
49 end; |
|
50 |
|
51 |
8 |
52 |
9 (* Elimination of True from asumptions: *) |
53 (* Elimination of True from asumptions: *) |
10 |
54 |
11 val True_implies_equals = prove_goal IFOL.thy |
55 val True_implies_equals = prove_goal IFOL.thy |
12 "(True ==> PROP P) == PROP P" |
56 "(True ==> PROP P) == PROP P" |