Prova idiomatica per contraddizione in Isabelle?

Question

Finora ho scritto dimostrazioni per assurdo nello stile seguito a Isabelle (utilizzando un modello da Jeremy Siek):

lemma "<expression>" 
proof - 
    { 
    assume "¬ <expression>" 
    then have False sorry 
    } 
    then show ?thesis by blast 
qed 

C'è un modo che funziona senza la prova grezzo nidificato bloccare { ... }?

Answer 1

V'è la regola ccontr per le classiche prove per assurdo:

have "<expression>" 
proof (rule ccontr) 
    assume "¬ <expression>" 
    then show False sorry 
qed 

A volte può aiutare a utilizzare by contradiction per provare l'ultimo passo.

V'è anche la regola classical (che sembra meno intuitivo):

have "<expression>" 
proof (rule classical) 
    assume "¬ <expression>" 
    then show "<expression>" sorry 
qed 

Per ulteriori esempi che utilizzano classical, vedere $ISABELLE_HOME/src/HOL/Isar_Examples/Drinker.thy

Answer 2

Per una migliore comprensione della regola classical può essere stampata in stile strutturato Isar In questo modo:

print_statement classical 

Uscita:

theorem classical: 
    obtains "¬ thesis" 

Così il male puro intuizionisti appare un po 'più intuitivo: per dimostrare qualche tesi arbitraria, possiamo supporre che la sua negazione contiene.

Il modello di prova canonica corrispondente è questo:

notepad 
begin 
    have A 
    proof (rule classical) 
    assume "¬ ?thesis" 
    then show ?thesis sorry 
    qed 
end 

Qui ?thesis è la tesi concreta l'affermazione sopra di A, che può essere una dichiarazione arbitrariamente complessa. Questa quasi astrazione tramite l'abbreviazione ?thesis è tipica dell'idioma idiota, per enfatizzare la struttura del ragionamento.