# Re: [isabelle] Tactic for Eliminating Parameters Wanted ...

```Hi Burkhart,

```
If I wanted to do this in Isabelle 2005, I'd just try rewriting with the following:
```
triv_forall_equality ;
val it = "(!!x. PROP ?V) == PROP ?V" : Thm.thm

```
Of course, I've no idea whether this is still available in the current versions
```
Cheers,

Jeremy

On 26/02/15 22:55, Burkhart Wolff wrote:
```
```Dear all,

is there any way to actually eliminate a parameter or a goal ?

After case-splits, parameters are often no longer of relevance.

MY PROBLEM:
============

I have something like:

"âS. PUT (S::(...) actionâiâpâc)â

which I reduce via case-splitting to:

"(âS ipc_stage ipc_direction. PUT (IPC ipc_stage ipc_direction)) â (âS. PUT S)â

which I would like to reduce to:

"(â ipc_stage ipc_direction. PUT (IPC ipc_stage ipc_direction)) â (âS. PUT S)â

(so canceling the parameter S irrelevant in the goal).

SOME ELEMENTS OF A SOLUTION:
I cooked up some sketch of a tactics which does nearly what I want:

ML{* val XX = Unsynchronized.ref(@{thm impI})
fun PEEK st = (XX:=st; all_tac st)
*}
lemma "âS. PUT (S::(...) actionâiâpâc)"
apply(tactic "Induct_Tacs.case_tac @{context} \"S\" 1", hypsubst)
apply(tactic "PEEK")
oops
ML{* val st = !XX;
val thy = #thy (rep_thm (st));
val _ \$ (_ \$ Abs(x,ty,t))  = concl_of(st);
val cFree = cterm_of thy (Free(x,ty))
*}
ML{* val _ \$ Abs(ss,_,T) = term_of (cprem_of (st) 1) ;
val T' =  cterm_of thy (subst_bounds([Bound 0],T)) *}

ML{* val Q  = Thm.assume T'*}
ML{* val Q' = Thm.forall_intr cFree  (Q) ; *}
ML{* val Q'' = Thm.implies_intr T' Q'*}
ML{* val Q''' = Q'' RS (st)*}

Unfortunately, the very last composition step fails:
exception THM 1 raised (line 332 of "drule.ML"):
RSN: no unifiers
(âipc_stage ipc_direction. PUT (IPC ipc_stage ipc_direction)) â
(âS ipc_stage ipc_direction. PUT (IPC ipc_stage ipc_direction))
(âS ipc_stage ipc_direction. PUT (IPC ipc_stage ipc_direction)) â (âS. PUT S)

which looks bizarre. The types and class types are confrom.

Any ideas ?

Best

bu

```
```

```

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