# Re: [isabelle] Generalized elimination rule?

```Peter Lammich wrote:
```
```Hi Brian,

Many thanks you for your answer.

```
I adopted your proposal for my needs. However, I ran into a problem that should also be imminent in your proposal (?). If there are premises of the form !!x. _==>_, they are counted in nhyps, however dtac keepI will not unify against them, thus
```  val ktac = EVERY' (replicate nhyps (dtac keepI)) : int -> tactic ;
produces premises that are doubly-wrapped into keep.

What's the best way around?
Only counting "plain" premises? (How?)
Can keepI be defined to also wrap higher-order premises?

Best,
Peter

```
```Dear Peter,

I'm not quite sure if I understand you correctly.

```
Are you talking about the situation where there is a premise (among the list of premises of a subgoal) of the form !!x. _==>_ ?
```(Isn't this rather unusual - could I see an example of how this arises ?)

Certainly, keep, as I defined it, won't wrap around a premise of the form
```
!!x. _==>_ because such a premise is of type prop, not bool. Isabelle generally - I think - wasn't intended to work very much with meta-level stuff, and previously I have found that playing around with meta-level props instead of object level bools doesn't seem to work as expected. However to my surprise the attached does seem to work - try it out and see if it works on your problem example.
```
Regards,

Jeremy

```
```consts
meta_keep     :: "bool => prop => prop"

defs
meta_keep_def : "meta_keep b f == f"

val meta_iffD2 = prove_goal ProtoPure.thy
"[| PROP P==PROP Q; PROP Q |] ==> PROP P"
(fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]);

val meta_iffD1 = symmetric_thm RS meta_iffD2;
val meta_iffDs = [meta_iffD1, meta_iffD2] ;

val _ = ListPair.app bind_thm (["meta_keepD", "meta_keepI"],
[meta_keep_def] RL meta_iffDs) ;
val _ = bind_thm ("meta_keepTD",
read_instantiate [("b", "True")] meta_keepD) ;
val _ = bind_thm ("meta_keepFD",
read_instantiate [("b", "False")] meta_keepD) ;
val _ = bind_thm ("meta_keepF_thin", meta_keepFD RS thin_rl) ;

(* meta_fetac : thm -> int -> int -> tactic
like fatac n but also deletes hypotheses matched *)
fun meta_fetac th n sg st =
let val fth = thin_rl RS (replicate n meta_keepFD MRS th) : thm ;
val subgoal = List.nth (prems_of st, sg - 1) : term ;
(* turn all subgoal hypotheses H into meta_keep ?b H *)
val nhyps = length (Logic.strip_assums_hyp subgoal) ;
val ktac = EVERY' (replicate nhyps (dtac meta_keepI)) : int -> tactic ;
(* then apply ftac fth - see later *)
(* then apply atac n times,
which marks the hypotheses to be deleted with meta_keep False *)
val atacs = EVERY' (replicate n atac) ;
(* treat other instances of meta_keep ?b as meta_keep True, and erase *)
val ekttac = REPEAT o dtac meta_keepTD : int -> tactic ;
(* delete hypotheses which are (meta_keep False ...) *)
val ekftac = REPEAT o etac meta_keepF_thin : int -> tactic ;
(* combine all the above *)
val ctac = EVERY' [ktac, ftac fth, atacs] THEN_ALL_NEW
(ekttac THEN' ekftac) : int -> tactic ;
in ctac sg st end ;

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.