@pepelluba

"Supongamos que tengo 'p'". Metes 'p' en tu mochila temporalmente. Es una hipótesis que podrás usar más tarde como ingrediente.

"Hago una pausa para fabricar 'q'". Es una mini-meta. Te inventas un paso intermedio que necesitas para más adelante. Tienes que demostrarlo ahí mismo.

"Con esto demuestro mi meta actual". Es el golpe final. Lo que pongas en un show tiene que coincidir exactamente con lo que Isabelle te está pidiendo en ese momento.

"Usando estos ingredientes…". Le pasas datos de tu mochila (hipótesis o resultados previos) a una regla para que pueda ejecutarse.

"Voy a resolver esta meta abriendo la estructura con la regla X". Aplica la regla principal y genera las sub-metas correspondientes.

"No apliques ninguna regla automática todavía. Voy a preparar mis ingredientes en la mesa primero". Útil cuando necesitas montar piezas antes de cerrar.

El separador de universos paralelos. Cierra un caso y resetea la mochila para empezar el siguiente. Imprescindible en pruebas por casos o conjunciones divididas.

Para fabricar un billete de 'p' a 'q', asumo que estoy en 'p' y trato de demostrar que puedo llegar a 'q'. proof (rule impI)
  assume "p"
  show "q" ...

Tienes p → q (el billete) y tienes p (estás en la ciudad). Como tengo el billete y estoy en el origen, llego al destino. have "q" using `p → q` `p` by (rule mp)

Tienes una bolsa p & q. Rompes la bolsa y te quedas con lo de la izquierda (conjunct1) o con lo de la derecha (conjunct2). have "p" using `p & q` by (rule conjunct1)

Tienes 'p' suelta y tienes 'q' suelta. Les pones pegamento y las metes en una bolsa juntas. Si haces proof (rule conjI) sin ingredientes, Isabelle te divide en dos sub-tareas. show "p & q" using `p` `q` by (rule conjI)

Ya sabes que 'p' es verdad de forma segura. Como tienes 'p', te puedes inventar cualquier alternativa a su lado. show "p | q" using `p` by (rule disjI1)
show "p | q" using `q` by (rule disjI2)

Tienes p | q pero tu meta es r. Como no sabes si es 'p' o 'q', exploras ambos universos. Demuestras 'r' asumiendo 'p', y luego demuestras 'r' asumiendo 'q'. show "r" using `p | q`
proof (rule disjE)
  assume "p"
  show "r" ...
next
  assume "q"
  show "r" ...
qed

Para demostrar que 'p' es mentira, asumo que es verdad. Al asumir 'p', si llego a una contradicción absurda (False), entonces era mentira. proof (rule notI)
  assume "p"
  show False ...

Tienes algo afirmado (p) y lo mismo negado (~p). Tengo un choque frontal. Se lo doy a 'notE', el sistema se rompe, y como premio me regala la meta que yo quiera. show "Z" using `~p` `p` by (rule notE)

Ya tienes la palabra False en tu mochila. Como ya has demostrado el absurdo, puedes concluir cualquier cosa. show "Z" using `False` by (rule FalseE)

Estás atascado en tu meta p. Asumes que tu meta entera es mentira (~p). Si usando eso logras crear un cortocircuito (False), entonces tu meta original era verdad. proof (rule ccontr)
  assume "~p"
  show False ...