Czy nie można importować żadnej teorii w Isabelle?

Question

Chcę zdefiniować własny typ listy w teorii o nazwie List, ale istnieje już teoria o tej nazwie. Czy istnieje bardziej lekka teoria niż Main?

Answer 1

Nie można importować niczego w Isabelle (ponieważ import jest niezbędny nawet dla podstawowej logiki). Wdrożenie HOL w Isabelle ma trzy obsługiwane punkty wejścia: Main, Complex_Main (co jest Main plus niektóre analizy) i Plain, ale tylko pierwsze dwa są zamierzone do regularnego użytkowania.

Zwykły już zawiera podstawową logikę, ale prawie nic pod względem standardowej biblioteki (np. Bez list). Ale brakuje również ważnych narzędzi, takich jak QuickCheck, Sledgehammer i generator kodu. Co więcej, jeśli zaczniesz od Plain, aby móc nazwać swoją własną Listę Teorii, bądź świadomy, że twoja teoria będzie niezgodna z jakimkolwiek budowaniem pracy na Main (która jest prawie wszystkim).

Tak więc, jeśli nie masz naprawdę dobrych powodów, proponuję śledzić komentarz Raphaela i podać twojej liście teorii inne imię.

Answer 2

Można importować tylko HOL, jak w

theory Test_Theory 
imports HOL 
begin 
    … 
end 

ja często go do testowania i badania o Isabelle.

Jednakże, będziesz brakuje definicji typu danych, a prawdopodobnie trzeba będzie importować Datatype (a może być nawet Record), a także, aby móc napisać swoją teorię List.

theory Test_Theory 
imports HOL Datatype Record 
begin 
    … 
end 

W obu Datatype i Record importu HOL, można po prostu:

theory Test_Theory 
imports Datatype Record 
begin 
    … 
end 

To nie jest łatwe do zrobienia bez teorii Main, ale nie niemożliwe. Po prostu pamiętaj, że będziesz musiał obyć się bez wielu powszechnie używanych twierdzeń i być może będziesz musiał napisać i udowodnić swoje własne.

Answer 3

Zauważ, że $ISABELLE_HOME/src/HOL/ex/Seq.thy daje minimalny przykład zdefiniowania własnego typu danych na liście do eksperymentowania, bez wdawania się w delikatne pytanie, jak pracować z systemem poniżej jego punktu wejścia Main. (Początkujący wpadają w zakłopotanie, a eksperci tego nie robią.)

Teoretycznie najbardziej prymitywną teorią, którą można zaimportować, jest Pure, ale jest to po prostu szkielet logiczny, bez logiki obiektowej, takiej jak HOL. Tylko dla ciekawości, możesz spojrzeć na $ISABELLE_HOME/src/HOL/ex/Higher_Order_Logic.thy, która zaczyna się od Pure i definiuje minimalną wersję H.O.L. na dodatek bez zaawansowanych teorii i narzędzi, których można oczekiwać od pełnej wersji Isabelle/HOL.