# 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:

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.