[isabelle] how is one supposed to get !!x. p(x) from p(?x)



Ok, so I have a kind of "two-dimensional" induction that I'm trying to
do. Here is a stripped-down example that illustrates the difficulty:

consts p :: "nat => nat => bool"

lemma base: "(p 0 y)"
sorry (* lemma base: p 0 ?y *)

lemma meta: "(p row col) ==> (p (row + 1) any_col)"
sorry (* lemma meta: p ?row ?col ==> p (?row + 1) ?any_col *)

lemma half: "(!!col. (p row col)) ==> (p (row + 1) any_col)"
sorry (* lemma half: (!!col. p ?row col) ==> p (?row + 1) ?any_col *)

lemma desired: "(p row col)"

The base cases and inductive steps are simply "provided" using "sorry"
to keep the example simple. meta and half are basically the same thing
except in meta "col" is a meta-whatsitcalled or maybe
schematic-whatsitcalled. Now, after 3 hours of trial and error, I have
succeeded in providing the desired lemma:

lemma helper: "!!row. (!!col. p row col) ==> p (Suc row) col"
apply(drule half[where any_col=col])
apply(simp)
done (* lemma helper: (!!col. p ?row col) ==> p (Suc ?row) ?col *)

lemma desired: "(p row col)"
apply(induct row arbitrary: col)
apply(simp add: base)
apply(simp add: helper)
done (* lemma desired: p ?row ?col *)

So, how is this kind of thing -supposed- to be done? Is there a way to
apply something in the main proof to get this done without a helper
lemma? I was thinking the obvious thing is change it to subgoal_tac,
but so far all my attempts have been unsuccessful. Plus, it seems like
there should be an even better way.

Thanks,
-Andrei





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