# Re: [isabelle] about free veriable

On Thu, 14 Apr 2011, 张欢欢 wrote:

`I am getting stuck in a proof. Besides other questions I am quite
``confused about this one:
`
lemma [simp]:"\<forall> f. set f \<subseteq> set (sweep h r f )"
apply(induct h)
...
proof-
fix a h assume IH:"\<forall> f . set
f
\<subseteq> set (sweep h r
f
)"
...
fix f from IH have "set
(a # f)
\<subseteq> set (sweep h r
(a # f)
)" sorry

`Why this step is wrong? I did use the \<forall> f? sweep is defined by
``primrec.
`

`It is not immediately clear what you are trying to do, but the approach
``looks a bit nonstandard. What is "..." after the initial
`"apply (induct h)".

`You should not do too many things at the same time, it will make the
``development of the proof difficult ("getting stuck") and confuse the
``reader of the result.
`
Here is a standard pattern for plain mathematical induction:
notepad
begin
fix n :: nat
have "P n"
proof (induct n) print_cases
case 0
show ?case sorry
next
case (Suc n)
thm Suc.hyps
show ?case sorry
qed
end

`The auxiliary print_cases gives an idea about the local contexts that are
``available in each branch of the proof -- that command can be deleted from
``the final version.
`

`Also note that auxiliary quantification of the statement is really
``ancient. The "induct" method already knows about "arbitrary" variables.
``See also ~~/src/HOL/Induct/Common_Patterns.thy for more advanced examples.
`
Makarius

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