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)
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.

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:


  fix n :: nat
  have "P n"
  proof (induct n) print_cases
    case 0
    show ?case sorry
    case (Suc n)
    thm Suc.hyps
    show ?case sorry


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.


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