[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)
fix a h assume IH:"\<forall> f . set
  \<subseteq> set (sweep h  r 

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.


Huanhuan Zhang

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