# [isabelle] Fix-assume in Eisbach or Isabelle/ML method?

```Dear Eisbach/Isabelle/ML experts,

```
I have a repetitive structured proof whose functionality I would like to encapsulate as a method.
```For example:

```
assume *: "&#928;x:A. &#928;y: B x. &#928;z: C x y. D x y z : U"
```
have 0: "A : U" using * by rule

-- {* "B: A -> U" abbreviates "!!x. x : A ==> B x : U" *}
have 1: "B: A -> U"
proof -
fix x assume "x : A"
```
with * have **: "&#928;y: B x. &#928;z: C x y. D x y z : U" by rule
```  then show "B x : U" by rule
qed

have 2: "!!x. x : A ==> C x : B x -> U"
proof -
fix x assume "x : A"
```
with * have **: "&#928;y: B x. &#928;z: C x y. D x y z : U" by rule
```  fix y assume "y : B x"
with ** have "&#928;z: C x y. D x y z : U" by rule
then show "C x y : U" by rule
qed

```
have 3: "!!x y. [| x : A; y : B x |] ==> D x y : C x y -> U"
```proof -
fix x assume "x : A"
```
with * have **: "&#928;y: B x. &#928;z: C x y. D x y z : U" by rule
```  fix y assume "y : B x"
with ** have "&#928;z: C x y. D x y z : U" by rule
then show "D x y: C x y -> U" by rule
qed

end

```
In the above proofs, "rule" is applying one or the other of two rules previously declared as [elim]: Prod_form_cond1 [elim]: "!!A B. (&#928;x:A. B x : U) ==> A : U" Prod_form_cond2 [elim]: "!!A B. (&#928;x:A. B x : U) ==> B: A -> U"
```
```
Given "&#928;x:T. S x : U", the basic proof pattern is then: Fix x, assume "x : T", and derive either "T: U" or "S x : U" by rule. Recurse, essentially performing a breadth-first search over a binary tree.
```
```
I have tried and failed at automating this proof with Eisbach, my difficulty is in getting it to perform the "fix...assume" steps to instantiate a "scope" for the variable and introduce the typing assumption. Is there any method that emulates this? If not, how does one go about implementing such functionality in an Isabelle/ML tactic?
```
Thanks very much! :)

```

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