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

author | wenzelm |

Sat, 31 Dec 2005 21:49:35 +0100 | |

changeset 18528 | 85e7f80023fc |

parent 18527 | 88abdee3e23f |

child 18529 | 540da2415751 |

obsolete, see classical_rule in Provers/classical.ML;

src/Provers/make_elim.ML | file | annotate | diff | comparison | revisions |

--- a/src/Provers/make_elim.ML Sat Dec 31 13:03:55 2005 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,38 +0,0 @@ -(* Title: Provers/make_elim.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 2000 University of Cambridge - -Classical version of Tactic.make_elim - -In classical logic, we can make stronger elimination rules using this version. -For instance, the HOL rule injD is transformed into - [| inj ?f; ~ ?W ==> ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W -while Tactic.make_elim would yield the weaker rule - [| inj ?f; ?f ?x = ?f ?y; ?x = ?y ==> PROP ?W |] ==> PROP ?W -Such rules can cause Fast_tac to fail and Blast_tac to report "PROOF FAILED" -*) - -signature MAKE_ELIM_DATA = -sig - val cla_dist_concl: thm (*"[| ~Z ==> PROP X; PROP Y ==> Z; PROP X ==> PROP Y |] ==> Z"*) -end; - -functor Make_Elim_Fun(Data: MAKE_ELIM_DATA) = -struct - -fun make_elim rl = - let - fun compose_extra nsubgoal (tha,i,thb) = - Seq.list_of (bicompose false (false,tha,nsubgoal) i thb) - val revcut_rl' = Drule.incr_indexes rl revcut_rl - - fun making (i,rl) = - case compose_extra 2 (Data.cla_dist_concl,i,rl) of - [] => rl (*terminates by clash of variables!*) - | rl'::_ => making (i+1,rl') - in making (2, hd (compose_extra 1 (rl, 1, revcut_rl'))) end - handle (*in default, use the previous version, which never fails*) - THM _ => Tactic.make_elim rl | Empty => Tactic.make_elim rl; - -end;