[isabelle] Trivial lemma requires syntactic fiddling



Dear list,

It is a bit awkward to see that to prove a trivial lemma on natural numbers
requires syntactic fiddling on the notation of  sets. It looks like the
whole reasoning machinery behind assumes a certain syntactic notation for
sets.

For example the lemma in the sequel requires me to apply (**) twice as
substitution  just to get in a syntactic form where I can apply the
reasoning machinery provided by the library. Namely, it is awkward to see
that the notation {0..n::nat} is better than {na::nat. na ≤n} when proving
stuff on ∑ .
My question is why not just having the same syntactic sugar for both
notations? Any limitations to have an abbreviation of the form {na::nat. na
≤n} ==  {0..n::nat}? Or just because ∑ is too general? Is there an existing
AFP entry or an Isabelle theory that introduces these kind of abbreviations
when sets are specialized for natural numbers?

lemma "∑{na::nat. na ≤n} = ((n * (n +1)) div 2)"
proof -
  have **: "⋀n. {na::nat. na ≤n} = {0.. n}"
    by auto
  show ?thesis
  proof (induct n)
    case 0
    then show ?case by simp
  next
    case (Suc n)
    assume H1: "∑{na. na ≤ n} = n * (n + 1) div 2"
    have *:"∑{naa. naa ≤  Suc n} = ∑{naa. naa ≤  n} +  Suc n"
      apply (subst **)
      apply (subst **)
      using sum.atLeast0_atMost_Suc
      apply blast
      done
    show ?case
      apply (subst *)
      apply (subst H1)
      apply (simp)
      done
  qed
qed

Best wishes,

Yakoub.



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