# [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:
notepad begin

`assume *: "Πx:A. Πy: B x. Π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 **: "Πy: B x. Π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 **: "Πy: B x. Πz: C x y. D x y z
``: U" by rule
` fix y assume "y : B x"
with ** have "Π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 **: "Πy: B x. Πz: C x y. D x y z
``: U" by rule
` fix y assume "y : B x"
with ** have "Π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. (Πx:A. B x : U) ==> A
``: U"
``Prod_form_cond2 [elim]: "!!A B. (Πx:A. B x : U) ==>
``B: A -> U"
`

`Given "Π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.*