summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Thu, 19 Sep 2002 16:00:27 +0200 | |

changeset 13568 | 6b12df05f358 |

parent 13567 | 7f5bf04095bd |

child 13569 | 69a6b3aa0f38 |

preserve names of rewrite rules when transforming them

--- a/src/HOL/simpdata.ML Wed Sep 18 18:19:43 2002 +0200 +++ b/src/HOL/simpdata.ML Thu Sep 19 16:00:27 2002 +0200 @@ -136,18 +136,18 @@ (*Make meta-equalities. The operator below is Trueprop*) -fun mk_meta_eq r = r RS eq_reflection; +fun mk_meta_eq r = r nRS eq_reflection; fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r; fun mk_eq th = case concl_of th of Const("==",_)$_$_ => th | _$(Const("op =",_)$_$_) => mk_meta_eq th - | _$(Const("Not",_)$_) => th RS Eq_FalseI - | _ => th RS Eq_TrueI; -(* last 2 lines requires all formulae to be of the from Trueprop(.) *) + | _$(Const("Not",_)$_) => th nRS Eq_FalseI + | _ => th nRS Eq_TrueI; +(* Expects Trueprop(.) if not == *) fun mk_eq_True r = - Some (r RS meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => None; + Some (r nRS meta_eq_to_obj_eq nRS Eq_TrueI) handle Thm.THM _ => None; (*Congruence rules for = (instead of ==)*) fun mk_meta_cong rl = @@ -188,21 +188,15 @@ val Addsplits = Splitter.Addsplits; val Delsplits = Splitter.Delsplits; -(*In general it seems wrong to add distributive laws by default: they - might cause exponential blow-up. But imp_disjL has been in for a while - and cannot be removed without affecting existing proofs. Moreover, - rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the - grounds that it allows simplification of R in the two cases.*) - val mksimps_pairs = [("op -->", [mp]), ("op &", [conjunct1,conjunct2]), ("All", [spec]), ("True", []), ("False", []), ("If", [if_bool_eq_conj RS iffD1])]; -(* ###FIXME: move to Provers/simplifier.ML +(* val mk_atomize: (string * thm list) list -> thm -> thm list +looks too specific to move it somewhere else *) -(* ###FIXME: move to Provers/simplifier.ML *) fun mk_atomize pairs = let fun atoms th = (case concl_of th of @@ -210,7 +204,7 @@ (case head_of p of Const(a,_) => (case assoc(pairs,a) of - Some(rls) => flat (map atoms ([th] RL rls)) + Some(rls) => flat (map atoms (map (apl(th,op nRS)) rls)) | None => [th]) | _ => [th]) | _ => [th]) @@ -237,6 +231,12 @@ setmkeqTrue mk_eq_True setmkcong mk_meta_cong; +(*In general it seems wrong to add distributive laws by default: they + might cause exponential blow-up. But imp_disjL has been in for a while + and cannot be removed without affecting existing proofs. Moreover, + rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the + grounds that it allows simplification of R in the two cases.*) + val HOL_ss = HOL_basic_ss addsimps ([triv_forall_equality, (* prunes params *)