[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.