Równoważność między stylami Apply i Isar w Isabelle

Question 1

Czy Apply style i Isar-proof są odpowiednikami? To jest pytanie, nad którym zastanawiałem się od jakiegoś czasu. Oczywiście, Isar-dowody są znacznie bardziej czytelne, łatwe w utrzymaniu i łatwe do napisania (?), ale moje pytanie brzmi, czy można udowodnić dokładnie to samo w obu stylach.

Na przykład obecnie pracuję nad dowodem, w którym muszę wyjść:

apply(simp split: prod.splits) 
using some_lemma by fastforce

Jaka jest równoważna forma tych poleceń w stylu Apply i Isar? Właściwie bardziej interesuje mnie styl Isar, ponieważ powiedziano mi, że mieszanie stylów jest złym stylem.

isabelle

2

Rodrigo 10 listopad 2018, 02:03

Answer

Odpowiednikiem stylu Isar byłoby:

have "P"
  using some_lemma by fastforce
then have "Q"
  by (simp split: prod.splits)

Gdzie „P” oznacza pośredni stan celu po pierwszym apply.

Ogólnie rzecz biorąc, wszystko, co można udowodnić, można udowodnić zarówno w stylu Isar, jak iw stylu apply; obaj mają swoje mocne i słabe strony.

Osobiście używam stylu, w którym staram się ustrukturyzować moje dowody na zewnątrz: na zewnątrz (jak indukcja) Isar i jeśli to konieczne, wewnątrz (jak uproszczenie, rzeczy na niskim poziomie) z apply.

Generalnie jednak polecam pobyt w Isar jak najdłużej.

3

larsrh 10 listopad 2018, 02:24

Question 2