Re: [isabelle] Basic help with class and instantiation



On Fri, 17 Aug 2012, Yannick Duchêne (Hibou57) wrote:

The case is in the practical way solved, but something still holds mysterious things. With or without the “::int” annotation, at the beginning of the proof, there was this:

proof (state): step 1

goal (1 subgoal):
 1. cls1_f (cls1_g (0∷nat)) = cls1_g (0∷nat)
constants:
  […]
  cls1_g :: nat ⇒ int
  cls1_f :: int ⇒ int
  […]

Types are correctly inferred at the beginning, but later forgotten? That's strange. I will stay with this for now, but wish to understand it deeper a later time.

This is because there is no formal syntactic relationship between the goal state in the background and the Isar proof body in the foreground that is meant to address it (fix/assume/show clause). This principle allows to generalize what you are drafting in the proof text on the spot, without having your nose directly on the goal.


	Makarius


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