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

Question

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 risolve, ripristina lo stato originale e fallisce.

Questo si avvicinò nel codice seguente:

qed (subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)+ 

Dopo qualche cambiamento più in alto, la chiamata a simp non risolverebbe completamente un obiettivo più, e allora questo ciclo. Se avessi potuto specificato qualcosa di simile

qed (solve_goal(subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail))+ 

o (in alternativa suggerita synatx)

qed ((subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)!)+ 

o (forse anche la sintassi più bello)

qed ((subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)[1!])+ 

sarebbe fermato al primo obiettivo che non è stato risolvibile da questo script.

Answer 1

Dal momento che l'avvento del Eisbach proof script language, questo è ora supportato . Dopo l'importazione "~~/src/HOL/Eisbach/Eisbach", si può sostituire

apply foo 

con

apply (solves ‹foo›) 

e la linea non riuscirà se solves produce eventuali nuovi obiettivi. Questo può essere combinato con [1] come in

apply (solves ‹(auto)[1]›) 

se desiderato.

La definizione di solves è in realtà abbastanza semplice:

method solves methods m = (m; fail) 

Answer 2

Isabelle non ha un tale combinatore, che è qualcosa che mi manca anche. Spesso, posso evitare la necessità di un tale combinatore se sostituisco le chiamate auto o simp da fastforce o force (che hanno il comportamento di risolvere o fallire).

Quindi, se il simp nel tuo esempio si suppone per risolvere l'obiettivo (senza loop),

qed (subst fibs.simps, (subst fib.simps)?, fastforce simp: nth_zipWith nth_tail)+ 

potrebbe essere una variante più robusta.

Answer 3

La lingua Isar di Isabelle non fornisce questa caratteristica; questo è intenzionale e non un bug, come spiegato on the isabelle developer list:

Il metodo di prova di lingua Isar è stato progettato in un certo modo, per arrivare a "stilizzato" le specifiche di alcuni aspetti operativi nel testo di prova. Ha escluso qualsiasi tipo di programmazione o controllo sofisticato strutture appositamente.

Answer 4

Mentre non v'è nessuna tattica o combinatore built-in disponibili, è possibile implementare uno voi stessi come segue:

ML {* 
fun solved_tac thm = 
    if nprems_of thm = 0 then Seq.single thm else Seq.empty 
*} 

method_setup solved = {* 
    Scan.succeed (K (SIMPLE_METHOD solved_tac)) 
*} 

Questo crea un nuovo metodo solved che avrà successo se l'obiettivo attuale è stato completamente risolto , o fallire se vi sono ancora uno o più sotto-obiettivi.

Può essere utilizzato, ad esempio, come segue:

lemma "a ∨ ¬ a " 
    apply ((rule disjI1, solved) | (simp, solved)) 
    done 

senza la clausola solved, Isabelle selezionerà il lato rule disjI1 del passo apply, lasciando con un obiettivo irrisolvibile.Con la clausola solved su ciascun lato, Isabelle tenta di utilizzare rule disjI1 e, quando non riesce a risolvere l'obiettivo, passa allo simp, che ha quindi esito positivo.

Questo può essere utilizzato per risolvere singoli obiettivi utilizzando la sintassi (...)[1] di Isabelle. Ad esempio, la seguente dichiarazione tenterà di risolvere il maggior numero di sotto-obiettivi possibili utilizzando simp, ma lascerà un sotto-obiettivo invariato se simp non riesce a risolvere completamente:

apply ((simp, solved)[1])+