|
|
| (No se muestran 2 ediciones intermedias del mismo usuario) |
| Línea 1: |
Línea 1: |
| − | == RA_Relacion_1 ==
| |
| − | <source lang="isar">
| |
| − | theory Relacion_1
| |
| − | imports Main
| |
| − | begin
| |
| | | | |
| − | (* Demostrar los siguientes lemas usando sólo las reglas básicas de deducción
| |
| − | natural de la lógica proposicional. *)
| |
| − |
| |
| − | lemma I: "A ⟶ A"
| |
| − | proof
| |
| − | assume 1: "A"
| |
| − | qed
| |
| − |
| |
| − | lemma 0: "A ∧ B ⟶ B ∧ A"
| |
| − | proof
| |
| − | assume 1: "A ∧ B"
| |
| − | from 1 have 2: "A" by (rule conjunct1)
| |
| − | from 1 have 3: "B" by (rule conjunct2)
| |
| − | from 3 and 2 show "B ∧ A" by (rule conjI)
| |
| − | qed
| |
| − |
| |
| − | lemma "A ∧ B ⟶ A ∨ B"
| |
| − | proof
| |
| − | assume 1: "A ∧ B"
| |
| − | from 1 have 2: "A" by (rule conjunct1)
| |
| − | from 1 have 3: "B" by (rule conjunct2)
| |
| − | from 2 show "A ∨ B" by (rule disjI1)
| |
| − | qed
| |
| − |
| |
| − | lemma "(A ∨ B) ∨ C ⟶ A ∨ (B ∨ C)"
| |
| − | proof
| |
| − | assume 1: "(A ∨ B) ∨ C"
| |
| − | show "A ∨ (B ∨ C)"
| |
| − | proof -
| |
| − | note 1
| |
| − | moreover{
| |
| − | assume 2: "A ∨ B"
| |
| − | have "A ∨ (B ∨ C)"
| |
| − | proof -
| |
| − | note 2
| |
| − | moreover{
| |
| − | assume 3: "A"
| |
| − | from 3 have 4:"A ∨ (B ∨ C)" by (rule disjI1)
| |
| − | }
| |
| − | moreover{
| |
| − | assume 5:"B"
| |
| − | from 5 have 6: "B ∨ C" by (rule disjI1)
| |
| − | from 6 have 7: "A ∨ (B ∨ C)" by (rule disjI2)
| |
| − | }
| |
| − | ultimately show "A ∨ (B ∨ C)" by (rule disjE)
| |
| − | qed
| |
| − | }
| |
| − | moreover{
| |
| − | assume 8: "C"
| |
| − | from 8 have 9: "B ∨ C" by (rule disjI2)
| |
| − | from 9 have "A ∨ (B ∨ C)" by (rule disjI2)
| |
| − | }
| |
| − | ultimately show "A ∨ (B ∨ C)" by (rule disjE)
| |
| − | qed
| |
| − | qed
| |
| − |
| |
| − | lemma Aux:
| |
| − | assumes "A"
| |
| − | shows "B ⟶ A"
| |
| − | using assms by simp
| |
| − |
| |
| − | lemma K: "A ⟶ (B ⟶ A)"
| |
| − | proof
| |
| − | assume 1: "A"
| |
| − | from 1 show "B ⟶ A" by (rule Aux)
| |
| − | qed
| |
| − |
| |
| − |
| |
| − | lemma S: "(A ⟶ (B ⟶ C)) ⟶ ((A ⟶ B) ⟶ (A ⟶ C))"
| |
| − | proof
| |
| − | assume 1: "(A ⟶ (B ⟶ C))"
| |
| − | show "(A ⟶ B) ⟶ (A ⟶ C)"
| |
| − | proof
| |
| − | assume 2: "A ⟶ B"
| |
| − | show "A ⟶ C"
| |
| − | proof
| |
| − | assume 3: "A"
| |
| − | from 2 and 3 have 4: "B" by (rule mp)
| |
| − | from 1 and 3 have 5: "B ⟶ C" by (rule mp)
| |
| − | from 5 and 4 show 6: "C" by (rule mp)
| |
| − | qed
| |
| − | qed
| |
| − | qed
| |
| − |
| |
| − | lemma "(A ⟶ B) ⟶ ((B ⟶ C) ⟶ (A ⟶ C))"
| |
| − | proof
| |
| − | assume 1: "A ⟶ B"
| |
| − | show "(B ⟶ C) ⟶ (A ⟶ C)"
| |
| − | proof
| |
| − | assume 2: "B ⟶ C"
| |
| − | show "A ⟶ C"
| |
| − | proof
| |
| − | assume 3: "A"
| |
| − | from 1 and 3 have 4: "B" by (rule mp)
| |
| − | from 2 and 4 show 5: "C" by (rule mp)
| |
| − | qed
| |
| − | qed
| |
| − | qed
| |
| − |
| |
| − |
| |
| − | lemma "¬¬A ⟶ A"
| |
| − | proof
| |
| − | assume 1: "¬¬A"
| |
| − | from 1 show "A" by (rule notnotD)
| |
| − | qed
| |
| − |
| |
| − | lemma "A ⟶ ¬¬A"
| |
| − | proof
| |
| − | assume 1: "A"
| |
| − | from 1 show "¬¬A" by (rule contrapos_pn)
| |
| − | qed
| |
| − |
| |
| − | lemma MT:
| |
| − | assumes 1: "F ⟶ G" and
| |
| − | 2: "¬G"
| |
| − | shows "¬F"
| |
| − | proof (rule notI)
| |
| − | assume 3: "F"
| |
| − | from 1 and 3 have 4: "G" by (rule mp)
| |
| − | from 2 and 4 show False by (rule notE)
| |
| − | qed
| |
| − |
| |
| − | lemma "(¬A ⟶ B) ⟶ (¬B ⟶ A)"
| |
| − | proof
| |
| − | assume 1: "¬A ⟶ B"
| |
| − | show "¬B ⟶ A"
| |
| − | proof
| |
| − | assume 2: "¬B"
| |
| − | from 1 and 2 have 3:"¬¬A" by (rule MT)
| |
| − | from 3 show "A" by (rule notnotD)
| |
| − | qed
| |
| − | qed
| |
| − |
| |
| − | lemma "((A ⟶ B) ⟶ A) ⟶ A"
| |
| − | proof
| |
| − | assume 1: "(A ⟶ B) ⟶ A"
| |
| − | have 8: "¬¬A"
| |
| − | proof (rule notI)
| |
| − | assume 2: "¬A"
| |
| − | have 3: "A ⟶ B"
| |
| − | proof (rule impI)
| |
| − | assume 4: "A"
| |
| − | from 2 and 4 show "B" by (rule notE)
| |
| − | qed
| |
| − | from 1 and 3 have 5: "A" by (rule mp)
| |
| − | from 2 and 5 show False by (rule notE)
| |
| − | qed
| |
| − | from 8 show "A" by (rule notnotD)
| |
| − | qed
| |
| − |
| |
| − | lemma "A ∨ ¬A"
| |
| − | proof cases
| |
| − | assume "A" thus ?thesis ..
| |
| − | next
| |
| − | assume "¬A" thus ?thesis ..
| |
| − | qed
| |
| − |
| |
| − |
| |
| − | lemma "(¬(A ∧ B)) = (¬A ∨ ¬B)"
| |
| − | proof
| |
| − | {
| |
| − | assume 1: "¬(A ∧ B)"
| |
| − | have 2: "¬A ∨ A" by (rule excluded_middle)
| |
| − | thus "¬A ∨ ¬B"
| |
| − | proof (rule disjE)
| |
| − | { assume 3: "¬A"
| |
| − | thus "¬A ∨ ¬B" by (rule disjI1) }
| |
| − | next
| |
| − | { assume 4: "A"
| |
| − | have 5: "¬B ∨ B" by (rule excluded_middle)
| |
| − | thus "¬A ∨ ¬B"
| |
| − | proof (rule disjE)
| |
| − | {assume 6: "¬B"
| |
| − | thus "¬A ∨ ¬B" by (rule disjI2) }
| |
| − | next
| |
| − | {assume 7: "B"
| |
| − | from 4 and 7 have 8: "A ∧ B" by (rule conjI)
| |
| − | from 1 and 8 show "¬A ∨ ¬B" by (rule notE) }
| |
| − | qed
| |
| − | }
| |
| − | qed
| |
| − | }
| |
| − | next
| |
| − | { assume 1: "¬A ∨ ¬B"
| |
| − | show "¬(A ∧ B)"
| |
| − | proof (rule notI)
| |
| − | assume 2: "A ∧ B"
| |
| − | from 1 have 3:"¬A ∨ ¬B" .
| |
| − | moreover
| |
| − | { assume 4: "¬A"
| |
| − | from 2 have 5:"A" by (rule conjunct1)
| |
| − | from 4 and 5 have False by (rule notE) }
| |
| − | moreover
| |
| − | { assume 6: "¬B"
| |
| − | from 2 have 7: "B" by (rule conjunct2)
| |
| − | from 6 and 7 have False by (rule notE) }
| |
| − | ultimately show False by (rule disjE)
| |
| − | qed
| |
| − |
| |
| − | }
| |
| − | qed
| |
| − |
| |
| − | end
| |
| − |
| |
| − | </source>
| |
| − |
| |
| − | == RA_Relacion_2 ==
| |
| − | <source lang="isar">
| |
| − |
| |
| − | theory Relacion_2
| |
| − | imports Main
| |
| − | begin
| |
| − |
| |
| − | (* Demostrar o refutar los siguientes lemas usando sólo las reglas básicas
| |
| − | de deducción natural de la lógica proposicional y de la lógica de
| |
| − | predicados (allI, allE, exI y exE). *)
| |
| − |
| |
| − |
| |
| − | lemma "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
| |
| − | proof (rule impI)
| |
| − | assume 1: "(∃x. ∀y. P x y)"
| |
| − | show "(∀y. ∃x. P x y)"
| |
| − | proof (rule allI)
| |
| − | from 1 obtain x where 2: "∀y. P x y" by (rule exE)
| |
| − | fix y
| |
| − | from 2 have 3: "P x y" by (rule allE)
| |
| − | from 3 show 4: "∃x. P x y" by (rule exI)
| |
| − | qed
| |
| − | qed
| |
| − |
| |
| − | lemma "(∀x. P x ⟶ Q) = ((∃x. P x) ⟶ Q)"
| |
| − | proof
| |
| − | { assume 1: "∀x. P x ⟶ Q"
| |
| − | show "(∃x. P x) ⟶ Q"
| |
| − | proof
| |
| − | assume "∃x. P x"
| |
| − | then obtain a where "P a" by (rule exE)
| |
| − | have "P a ⟶ Q" using 1 by (rule allE)
| |
| − | thus "Q" using `P a` by (rule mp)
| |
| − | qed }
| |
| − | next
| |
| − | { assume 2: "(∃x. P x) ⟶ Q"
| |
| − | show "∀x. P x ⟶ Q"
| |
| − | proof
| |
| − | fix a
| |
| − | show "P a ⟶ Q"
| |
| − | proof
| |
| − | assume "P a"
| |
| − | hence 3: "∃x. P x" by (rule exI)
| |
| − | from 2 and 3 show "Q" by (rule mp)
| |
| − | qed
| |
| − | qed }
| |
| − | qed
| |
| − |
| |
| − | lemma "((∀ x. P x) ∧ (∀ x. Q x)) = (∀ x. (P x ∧ Q x))"
| |
| − | proof
| |
| − | {
| |
| − | assume 1: "(∀ x. P x) ∧ (∀ x. Q x)"
| |
| − | show "(∀ x. (P x ∧ Q x))"
| |
| − | proof (rule allI)
| |
| − | from 1 have 2: "(∀ x. P x)" by (rule conjE)
| |
| − | from 1 have 3: "(∀ x. Q x)" by (rule conjE)
| |
| − | fix a
| |
| − | from 2 have 4: "P a" by (rule allE)
| |
| − | from 3 have 5: "Q a" by (rule allE)
| |
| − | from 4 and 5 show 6: "(P a) ∧ (Q a)" by (rule conjI)
| |
| − | qed
| |
| − | }
| |
| − | next
| |
| − | {
| |
| − | assume 7: "∀ x. (P x ∧ Q x)"
| |
| − | show "(∀ x. P x) ∧ (∀ x. Q x)"
| |
| − | proof
| |
| − | fix a
| |
| − | from 7 have 8: "P a ∧ Q a" by (rule allE)
| |
| − | from 8 have 9: "P a" by (rule conjE)
| |
| − | (* seguir... *)
| |
| − | from 8 have 11: "Q a" by (rule allE)
| |
| − | (* seguir... *)
| |
| − | qed
| |
| − | }
| |
| − | qed
| |
| − |
| |
| − | oops
| |
| − |
| |
| − | lemma "((∀ x. P x) ∨ (∀ x. Q x)) = (∀ x. (P x ∨ Q x))"
| |
| − | oops
| |
| − |
| |
| − | lemma "((∃ x. P x) ∨ (∃ x. Q x)) = (∃ x. (P x ∨ Q x))"
| |
| − | oops
| |
| − |
| |
| − | lemma "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
| |
| − | oops
| |
| − | (*
| |
| − | proof (rule impI)
| |
| − | assume 1: "∀x. ∃y. P x y"
| |
| − | show "∃y. ∀x. P x y"
| |
| − | proof (rule exI)
| |
| − | show " ∀x. P x y"
| |
| − | proof (rule allI)
| |
| − | fix x
| |
| − | from 1 have 2: "∃y. P x y" by (rule allE)
| |
| − | from 2 obtain y where 3: "P x y" by (rule exE)
| |
| − | thus ?thesis ..
| |
| − | qed
| |
| − | *)
| |
| − |
| |
| − | lemma "(¬ (∀ x. P x)) = (∃ x. ¬ P x)"
| |
| − | proof
| |
| − | {
| |
| − | assume 1: "¬ (∀ x. P x)"
| |
| − | show "∃ x. ¬ P x"
| |
| − | proof
| |
| − |
| |
| − |
| |
| − | qed
| |
| − | }
| |
| − | next
| |
| − | {
| |
| − | assume 2: "∃ x. ¬ P x"
| |
| − | show "¬ (∀ x. P x)"
| |
| − | proof
| |
| − |
| |
| − | qed
| |
| − | }
| |
| − | qed
| |
| − |
| |
| − | end
| |
| − |
| |
| − | </source>
| |
