11 (** Conversion into rewrite rules **) |
11 (** Conversion into rewrite rules **) |
12 |
12 |
13 (*Make atomic rewrite rules*) |
13 (*Make atomic rewrite rules*) |
14 fun atomize r = |
14 fun atomize r = |
15 case concl_of r of |
15 case concl_of r of |
16 Const("Trueprop",_) $ Abs(_,_,a) $ Abs(_,_,c) => |
16 Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) => |
17 (case (forms_of_seq a, forms_of_seq c) of |
17 (case (forms_of_seq a, forms_of_seq c) of |
18 ([], [p]) => |
18 ([], [p]) => |
19 (case p of |
19 (case p of |
20 Const("imp",_)$_$_ => atomize(r RS @{thm mp_R}) |
20 Const(@{const_name imp},_)$_$_ => atomize(r RS @{thm mp_R}) |
21 | Const("conj",_)$_$_ => atomize(r RS @{thm conjunct1}) @ |
21 | Const(@{const_name conj},_)$_$_ => atomize(r RS @{thm conjunct1}) @ |
22 atomize(r RS @{thm conjunct2}) |
22 atomize(r RS @{thm conjunct2}) |
23 | Const("All",_)$_ => atomize(r RS @{thm spec}) |
23 | Const(@{const_name All},_)$_ => atomize(r RS @{thm spec}) |
24 | Const("True",_) => [] (*True is DELETED*) |
24 | Const(@{const_name True},_) => [] (*True is DELETED*) |
25 | Const("False",_) => [] (*should False do something?*) |
25 | Const(@{const_name False},_) => [] (*should False do something?*) |
26 | _ => [r]) |
26 | _ => [r]) |
27 | _ => []) (*ignore theorem unless it has precisely one conclusion*) |
27 | _ => []) (*ignore theorem unless it has precisely one conclusion*) |
28 | _ => [r]; |
28 | _ => [r]; |
29 |
29 |
30 (*Make meta-equalities.*) |
30 (*Make meta-equalities.*) |
31 fun mk_meta_eq th = case concl_of th of |
31 fun mk_meta_eq th = case concl_of th of |
32 Const("==",_)$_$_ => th |
32 Const("==",_)$_$_ => th |
33 | Const("Trueprop",_) $ Abs(_,_,a) $ Abs(_,_,c) => |
33 | Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) => |
34 (case (forms_of_seq a, forms_of_seq c) of |
34 (case (forms_of_seq a, forms_of_seq c) of |
35 ([], [p]) => |
35 ([], [p]) => |
36 (case p of |
36 (case p of |
37 (Const("equal",_)$_$_) => th RS @{thm eq_reflection} |
37 (Const(@{const_name equal},_)$_$_) => th RS @{thm eq_reflection} |
38 | (Const("iff",_)$_$_) => th RS @{thm iff_reflection} |
38 | (Const(@{const_name iff},_)$_$_) => th RS @{thm iff_reflection} |
39 | (Const("Not",_)$_) => th RS @{thm iff_reflection_F} |
39 | (Const(@{const_name Not},_)$_) => th RS @{thm iff_reflection_F} |
40 | _ => th RS @{thm iff_reflection_T}) |
40 | _ => th RS @{thm iff_reflection_T}) |
41 | _ => error ("addsimps: unable to use theorem\n" ^ |
41 | _ => error ("addsimps: unable to use theorem\n" ^ |
42 Display.string_of_thm_without_context th)); |
42 Display.string_of_thm_without_context th)); |
43 |
43 |
44 (*Replace premises x=y, X<->Y by X==Y*) |
44 (*Replace premises x=y, X<->Y by X==Y*) |