Oops, sorry about that! Due to a combination of circumstances, somebody wrote a message to me personally to the isabelle-dev mailing list and I clicked "reply" and then this happened. Please ignore this.
Manuel On 20/11/2020 10:37, Manuel Eberl wrote: > Ich weiß nicht, wie die Policy auf der isabelle-users-Mailingliste ist. > Mir war zumindest nicht klar, dass man da subscribed sein muss, um > posten zu können. > > So oder so ist das aber kein Bug, sondern völlig erwartetes Verhalten, > und wie ich mir schon dachte liegt es an Polymorphismus: > > "to_bl (word_cat (y::4 word) (x::8 word)) = > to_bl (of_bl (to_bl y @ to_bl x))" > > Wenn man hier [[show_sorts]] anmacht (z.B. mit "declare [[show_sorts]]" > im theory toplevel oder mit "note [[show_sorts]]" im Isar-Beweis oder > mit "using [[show_sorts]]" im apply-Beweis) sieht man da folgendes: > > variables: > x :: 8 word > y :: 4 word > type variables: > 'a, 'b :: len0 > > Dass da zwei Typvariablen 'a und 'b sind (die für die Längen > irgendwelcher Wörter stehen) klingt schon einmal ungut. Man kann > Isabelle auch direkt fragen, warum die linke und rechte Seite nicht > gleich sind, indem man "rule refl" anwendet und unification tracing > anschaltet: > > using [[unify_trace_failure]] > apply (rule refl) > > Da bekommt man dann die Fehlermeldung > > The following types do not unify: > 'a::len0 word ⇒ bool list > 'b::len0 word ⇒ bool list > > Ich hab mir den Term dann etwas genauer angesehen und das Problem ist > die Funktion word_cat: > > word_cat :: "'a::len0 word ⇒ 'b::len0 word ⇒ 'c::len0 word" > > Diese Funktion macht aus zwei Wörtern beliebiger Länge ein Wort > beliebiger Länge. Gleichzeitig macht das "to_bl", das darauf dann > angewandt wird, aus einem Wort beliebiger Länge eine Liste von booleans. > Dadurch kann dann die Typinferenz von Isabelle nicht mehr herleiten, > dass die Wörter links und rechts von dem "=" gleiche Länge haben sollen. > > Also am besten das Ergebnis von "word_cat" immer mit einer Typannotation > versehen. (das gleiche gilt für of_bl, eigentlich alle Funktionen, deren > Rückgabetyp eine zusätzliche Typvariable enthält). > > Übermäßiger Polymorphismus ist manchmal etwas haarig, und da das > Typsystem von Isabelle relativ simpel ist sind manche Operationen leider > deutlich polymorpher als man sie gerne hätte… > > Viele Grüße > > Manuel > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev > _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
