[isabelle] about free veriable



Hi all:

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.

Thanks

Huanhuan Zhang



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