isabelle

6calore

1risposta

Invocazione di Nitpick e Sledgehammer insieme in Isabelle

Quando dichiaro un lemma in Isabelle, spesso digito nitpick e, se questo non mi dà un controesempio. Quindi digitare sledgehammer per provare a trovare automaticamente una prova. mi chiedo: è possibil

11calore

3risposta

Isabelle/HOL fondazioni

Ho visto molta documentazione sulla sintassi e le strategie di prova di Isabelle, ma non ho trovato nulla sulle sue basi. Ho alcune domande che sarei molto grato se qualcuno potesse prendere il tempo

6calore

4risposta

applicare un metodo se e solo se si risolve l'obiettivo attuale

A volte, quando sto scrivendo prove applicare in stile, ho voluto un modo per modificare un metodo di prova per foo Prova foo al primo obbiettivo. Se risolve l'obiettivo, bene; se lo fa, non lo risolv

5calore

2risposta

cadere una premessa in un obiettivo in applicare stile

supponiamo che voglio mostrare il seguente lemma lemma "⟦ A; B; C ⟧ ⟹ D" ho l'obiettivo 1. A ⟹ B ⟹ C ⟹ D Tuttavia, non ho bisogno di B. Come posso trasferire il mio obiettivo a qualcosa di simile

7calore

3risposta

Quale regola usa "regola" o "prova"?

Quando uso apply (rule) in uno script di applicazione, in genere è selezionata una regola appropriata. Lo stesso vale per proof in prove strutturate. Dove posso imparare/cercare il nome della regola c

7calore

2risposta

Prova idiomatica per contraddizione in Isabelle?

Finora ho scritto dimostrazioni per assurdo nello stile seguito a Isabelle (utilizzando un modello da Jeremy Siek): lemma "<expression>" proof - { assume "¬ <expression>" then have Fal

10calore

1risposta

Come posso generare LaTeX da Isabelle/HOL?

Come posso utilizzare Isabelle/HOL per generare automaticamente LaTeX dai miei file di teoria dei sorgenti? Isabelle/HOL's tutorial.pdf è molto bello. Ho intenzione di scrivere un articolo su LaTeX co

5calore

2risposta

Definizione delle costanti sovraccariche in Isabelle

Come si può definire una funzione in Isabelle che ha una definizione diversa a seconda del tipo di argomento o del tipo di contesto in cui viene utilizzata? Ad esempio, potrei voler definire una funzi