summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/Provers/make_elim.ML

author | nipkow |

Fri May 17 11:25:07 2002 +0200 (2002-05-17 ago) | |

changeset 13157 | 4a4599f78f18 |

parent 12605 | c198367640f6 |

child 15570 | 8d8c70b41bab |

permissions | -rw-r--r-- |

allowed more general split rules to cope with div/mod 2

1 (* Title: Provers/make_elim.ML

2 ID: $Id$

3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory

4 Copyright 2000 University of Cambridge

6 Classical version of Tactic.make_elim

8 In classical logic, we can make stronger elimination rules using this version.

9 For instance, the HOL rule injD is transformed into

10 [| inj ?f; ~ ?W ==> ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W

11 while Tactic.make_elim would yield the weaker rule

12 [| inj ?f; ?f ?x = ?f ?y; ?x = ?y ==> PROP ?W |] ==> PROP ?W

13 Such rules can cause Fast_tac to fail and Blast_tac to report "PROOF FAILED"

14 *)

16 signature MAKE_ELIM_DATA =

17 sig

18 val classical : thm (* (~P ==> P) ==> P *)

19 end;

21 functor Make_Elim_Fun(Data: MAKE_ELIM_DATA) =

22 struct

24 local

25 val cla_dist_concl = prove_goal (the_context ())

26 "[| ~Z_ ==> PROP X_; PROP Y_ ==> Z_; PROP X_ ==> PROP Y_ |] ==> Z_"

27 (fn [premx,premz,premy] =>

28 ([(rtac Data.classical 1),

29 (etac (premx RS premy RS premz) 1)]))

31 fun compose_extra nsubgoal (tha,i,thb) =

32 Seq.list_of (bicompose false (false,tha,nsubgoal) i thb)

34 in

36 fun make_elim rl =

37 let val revcut_rl' = incr_indexes_wrt [] [] [] [rl] revcut_rl

38 fun making (i,rl) =

39 case compose_extra 2 (cla_dist_concl,i,rl) of

40 [] => rl (*terminates by clash of variables!*)

41 | rl'::_ => making (i+1,rl')

42 in making (2, hd (compose_extra 1 (rl, 1, revcut_rl'))) end

43 handle (*in default, use the previous version, which never fails*)

44 THM _ => Tactic.make_elim rl | LIST _ => Tactic.make_elim rl;

46 end

48 end;