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)
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and