header {* T12b: Razonamiento modular mediante entornos locales *}
theory T12b_Razonamiento_modular
imports Main
begin
text {*
Basado en
http://www.cse.unsw.edu.au/~kleing/teaching/thprv-04/slides/Demo14.thy
*}
section {* Ejemplo 1 *}
locale semi =
fixes prod :: "['a, 'a] => 'a" (infixl "⋅" 70)
assumes assoc: "(x ⋅ y) ⋅ z = x ⋅ (y ⋅ z)"
locale group = semi +
fixes one ("𝟭") and inv ("_⇧-" [100] 100)
assumes l_one: "𝟭 ⋅ x = x"
assumes l_inv: "x⇧-⋅ x = 𝟭"
lemma (in group) r_inv:
"x ⋅ x⇧- = 𝟭"
proof -
have "x ⋅ x⇧- = 𝟭 ⋅ (x ⋅ x⇧-)" by (simp only: l_one)
also have "… = (𝟭 ⋅ x) ⋅ x⇧-" by (simp only: assoc)
also have "… = (((x⇧-)⇧- ⋅ x⇧-) ⋅ x) ⋅ x⇧-" by (simp only: l_inv)
also have "… = ((x⇧-)⇧- ⋅ (x⇧- ⋅ x)) ⋅ x⇧-" by (simp only: assoc)
also have "… = ((x⇧-)⇧- ⋅ 𝟭) ⋅ x⇧-" by (simp only: l_inv)
also have "… = (x⇧-)⇧- ⋅ (𝟭 ⋅ x⇧-)" by (simp only: assoc)
also have "… = (x⇧-)⇧- ⋅ x⇧-" by (simp only: l_one)
also have "… = 𝟭" by (simp only: l_inv)
finally show ?thesis .
qed
lemma (in group) r_one:
"x ⋅ 𝟭 = x"
proof -
have "x ⋅ 𝟭 = x ⋅ (x⇧- ⋅ x)" by (simp only: l_inv)
also have "… = (x ⋅ x⇧-) ⋅ x" by (simp only: assoc)
also have "… = 𝟭 ⋅ x" by (simp only: r_inv)
also have "… = x" by (simp only: l_one)
finally show "x ⋅ 𝟭 = x" .
qed
lemma (in group) l_cancel [simp]:
"(x ⋅ y = x ⋅ z) = (y = z)"
proof
assume "x ⋅ y = x ⋅ z"
then have "(x⇧- ⋅ x) ⋅ y = (x⇧- ⋅ x) ⋅ z" by (simp add: assoc)
then show "y = z" by (simp add: l_inv l_one)
next
assume "y = z"
then show "x ⋅ y = x ⋅ z" by simp
qed
subsection {* Exportación *}
thm semi.assoc group.l_cancel
subsection {* Definiciones *}
locale semi2 = semi +
fixes rprod (infixl "⊙" 70)
defines rprod_def: "rprod x y ≡ y ⋅ x "
lemma (in semi2) r_assoc:
"(x ⊙ y) ⊙ z = x ⊙ (y ⊙ z)"
by (simp only: rprod_def assoc)
thm semi2.r_assoc
end
