header {* T12d: Pasos elementales *}
theory T12d_Pasos_elementales
imports Main
begin
text {* "thm" escribe el enunciado de los teoremas cuyos nombres se
indican. *}
thm conjI impI iffI notI
text{* Instanciación de teoremas con "of": *}
thm conjI
thm conjI[of "A" "B"]
thm conjI[of "A"]
thm conjI[of _ "B"]
text{* Instanciación de teoremas con "where": *}
thm conjI
thm conjI [where ?Q = "B"]
text {* Composición de teoremas con "OF": *}
thm refl
thm refl [of "a"]
thm conjI
thm conjI [OF refl [of "a"] refl [of "b"]]
thm conjI [OF refl [of "a"]]
thm conjI [OF _ refl [of "b"]]
text {* Una demostración por razonamiento hacia atrás: *}
lemma "⟦ A; B ⟧ ⟹ A ∧ B"
apply (rule conjI)
apply assumption
apply assumption
done
text {* Indicación de regla de introducción a "blast": *}
thm le_trans
lemma "⟦ (a::nat) ≤ b; b ≤ c; c ≤ d ⟧ ⟹ a ≤ d"
by (blast intro: le_trans)
end
