RA2018: Conjuntos, funciones y relaciones en Isabelle/HOL

En la segunda parte de la clase de hoy del curso de Razonamiento automático se ha estudiado cómo trabajar en Isabelle/HOL con conjuntos, funciones y relaciones.

La clase se ha basado en la siguiente teoría Isabelle/HOL

chapter {* Tema 12: Conjuntos, funciones y relaciones *}

theory T12_Conjuntos_funciones_y_relaciones
imports Main 
begin

section {* Conjuntos *}

subsection {* Operaciones con conjuntos *}

text {*
  Nota. La teoría elemental de conjuntos es HOL/Set.thy.

  Nota. En un conjunto todos los elemento son del mismo tipo (por
  ejemplo, del tipo τ) y el conjunto tiene tipo (en el ejemplo, "τ set"). 

  Reglas de la intersección:
  · IntI:  ⟦c ∈ A; c ∈ B⟧ ⟹ c ∈ A ∩ B
  · IntD1: c ∈ A ∩ B ⟹ c ∈ A
  · IntD2: c ∈ A ∩ B ⟹ c ∈ B

  Nota. Propiedades del complementario:
  · Compl_iff: (c ∈ - A) = (c ∉ A)
  · Compl_Un:  - (A ∪ B) = - A ∩ - B

  Nota. El conjunto vacío se representa por {} y el universal por UNIV. 

  Nota. Propiedades de la diferencia y del complementario:
  · Diff_disjoint:   A ∩ (B - A) = {}
  · Compl_partition: A ∪ - A = UNIV

  Nota. Reglas de la relación de subconjunto:
  · subsetI: (⋀x. x ∈ A ⟹ x ∈ B) ⟹ A ⊆ B
  · subsetD: ⟦A ⊆ B; c ∈ A⟧ ⟹ c ∈ B   
*}

text {*
  Ejemplo: A ∪ B ⊆ C syss A ⊆ C ∧ B ⊆ C.   
*}

lemma "(A ∪ B ⊆ C) = (A ⊆ C ∧ B ⊆ C)"
by blast

text {* 
  Ejemplo: A ⊆ -B syss B ⊆ -A.   
*}

lemma "(A ⊆ -B) = (B ⊆ -A)"
by blast

text {*
  Principio de extensionalidad de conjuntos:
  · set_eqI: (⋀x. (x ∈ A) = (x ∈ B)) ⟹ A = B

  Reglas de la igualdad de conjuntos:
  · equalityI:  ⟦A ⊆ B; B ⊆ A⟧ ⟹ A = B
  · equalityD1: A = B ⟹ A ⊆ B
  · equalityD2: A = B ⟹ B ⊆ A 
  · equalityE:  ⟦A = B; ⟦A ⊆ B; B ⊆ A⟧ ⟹ P⟧ ⟹ P   
*}

text {*
  Lema. [Analogía entre intersección y conjunción]
  "x ∈ A ∩ B" syss "x ∈ A" y "x ∈ B". 
*}

lemma "(x ∈ A ∩ B) = (x ∈ A ∧ x ∈ B)" 
by simp

text {*
  Lema. [Analogía entre unión y disyunción]
  x ∈ A ∪ B syss x ∈ A ó x ∈ B.   
*}

lemma "(x ∈ A ∪ B) = (x ∈ A ∨ x ∈ B)" 
by simp

text {*
  Lema. [Analogía entre subconjunto e implicación]
  A ⊆ B syss para todo x, si x ∈ A entonces x ∈ B.   
*}

lemma "(A ⊆ B) = (∀ x. x ∈ A ⟶ x ∈ B)" 
by auto

text {*
  Lema. [Analogía entre complementario y negación]
  x pertenece al complementario de A syss x no pertenece a A.   
*}

lemma "(x ∈ -A) = (x ∉ A)" 
by simp

subsection {* Notación de conjuntos finitos *}

text {*
  Nota. La teoría de conjuntos finitos es HOL/Finite_Set.thy.

  Nota. Los conjuntos finitos se definen por inducción a partir de las
  siguientes reglas inductivas:
  · El conjunto vacío es un conjunto finito.
    · emptyI: "finite {}"
  · Si se le añade un elemento a un conjunto finito se obtiene otro
    conjunto finito. 
    · insertI: "finite A ⟹ finite (insert a A)" 

  A continuación se muestran ejemplos de conjuntos finitos.   
*}

lemma 
  "insert 2 {} = {2} ∧
   insert 3 {2} = {2,3} ∧
   insert 2 {2,3} = {2,3} ∧
   {2,3} = {3,2,3,2,2}"
by auto

text {*
  Nota. Los conjuntos finitos se representan con la notación conjuntista
  habitual: los elementos entre llaves y separados por comas. 
*}

text {*
  Ejemplo: {a,b} ∪ {c,d} = {a,b,c,d}   
*}

lemma "{a,b} ∪ {c,d} = {a,b,c,d}" 
by blast

text {*
  Ejemplo de conjetura falsa y su refutación. 
*}

lemma "{a,b} ∩ {b,c} = {b}" 
oops

text {*
  Ejemplo con la conjetura corregida.   
*}

lemma "{a,b} ∩ {b,c} = (if a = c then {a,b} else {b})"
by auto

text {*
  Sumas de conjuntos finitos:
  · ∑A es la suma de los elementos del conjunto finito A. Por ejemplo, 
      value "∑{1,2,3}::int" -- "= 6"
  · (setsum f A) es la suma de la aplicación de f a los elementos del
    conjunto finito A,  Por ejemplo,
       value "setsum (λx. x*x) {1,2,3}::int" -- "= 14"
*}

text {*
  Ejemplos de definiciones recursivas sobre conjuntos finitos: 
  Sea A un conjunto finito de números naturales.
  · sumaConj A es la suma de los elementos A.
  · sumaCuadradosConj A es la suma de los cuadrados de los elementos A. 
*}

definition sumaConj :: "nat set ⇒ nat" where
  "sumaConj S ≡ ∑S"

value "sumaConj {2,5,3}" ― ‹= 10›

value "∑{2::nat,5,3}" ― ‹= 10›

definition sumaCuadradosConj :: "nat set ⇒ nat" where
  "sumaCuadradosConj S ≡ ∑x∈S. x*x"

value "sumaCuadradosConj {2,5,3}" ― ‹= 38›

text {*
  Nota. Para simplificar lo que sigue, declaramos las anteriores
  definiciones como reglas de simplificación.   
*}

declare sumaConj_def [simp]
declare sumaCuadradosConj_def [simp]

text {*
  Ejemplos de evaluación de las anteriores definiciones recursivas.   
*}

lemma 
  "sumaConj {1,2,3,4} = 10 ∧
   sumaCuadradosConj {1,2,3,4} = 30"
by simp

text {*
  Inducción sobre conjuntos finitos: Para demostrar que todos los
  conjuntos finitos tienen una propiedad P basta probar que
  · El conjunto vacío tiene la propiedad P.
  · Si a un conjunto finito que tiene la propiedad P se le añade un
    nuevo elemento, el conjunto obtenido sigue teniendo la propiedad P. 
  En forma de regla
  · finite_induct: ⟦finite F; 
                    P {}; 
                    ⋀x F. ⟦finite F; x ∉ F; P F⟧ ⟹ P ({x} ∪ F)⟧ 
                   ⟹ P F   
*}

text {* 
  Ejemplo de inducción sobre conjuntos finitos: Sea S un conjunto finito
  de números naturales. Entonces todos los elementos de S son menores o
  iguales que la suma de los elementos de S. 
*}

― ‹La demostración automática es›
lemma "finite S ⟹ ∀x∈S. x ≤ sumaConj S"
by (induct rule: finite_induct) auto

― ‹La demostración estructurada es›
lemma sumaConj_acota: 
  "finite S ⟹ ∀x∈S. x ≤ sumaConj S"
proof (induct rule: finite_induct)
  show "∀x ∈ {}. x ≤ sumaConj {}" by simp
next
  fix x and F
  assume fF: "finite F" 
     and xF: "x ∉ F" 
     and HI: "∀ x∈F. x ≤ sumaConj F"
  show "∀y ∈ insert x F. y ≤ sumaConj (insert x F)"
  proof 
    fix y 
    assume "y ∈ insert x F"
    show "y ≤ sumaConj (insert x F)"
    proof (cases "y = x")
      assume "y = x"
      then have "y ≤ x + (sumaConj F)" by simp
      also have "… = sumaConj (insert x F)" using fF xF by simp
      finally show ?thesis .
    next
      assume "y ≠ x"
      then have "y ∈ F" using `y ∈ insert x F` by simp
      then have "y ≤ sumaConj F" using HI by blast
      also have "… ≤ x + (sumaConj F)" by simp
      also have "… = sumaConj (insert x F)" using fF xF by simp
      finally show ?thesis .
    qed
  qed
qed

subsection {* Definiciones por comprensión *}

text {*
  El conjunto de los elementos que cumple la propiedad P se representa
  por {x. P}. 

  Reglas de comprensión (relación entre colección y pertenencia):
  · mem_Collect_eq: (a ∈ {x. P x}) = P a
  · Collect_mem_eq: {x. x ∈ A} = A   
*}

text {*
  Ejemplo de comprensión: {x. P x ∨ x ∈ A} = {x. P x} ∪ A   
*}

lemma "{x. P x ∨ x ∈ A} = {x. P x} ∪ A"
by blast

text {*
  Ejemplo de comprensión: {x. P x ⟶ Q x} = -{x. P x} ∪ {x. Q x}   
*}

lemma "{x. P x ⟶ Q x} = -{x. P x} ∪ {x. Q x}"
by blast

text {*
  Ejemplo con la sintaxis general de comprensión.   
     {p*q | p q. p ∈ prime ∧ q ∈ prime} = 
     {z. ∃p q. z = p*q ∧ p ∈ prime ∧ q ∈ prime}   
*}

lemma 
  "{p*q | p q. p ∈ prime ∧ q ∈ prime} = 
   {z. ∃p q. z = p*q ∧ p ∈ prime ∧ q ∈ prime}"
by blast

text {*
   En HOL, la notación conjuntista es azúcar sintáctica:
   · x ∈ A  es equivalente a A(x).
   · {x. P} es equivalente a λx. P.
*}

text {*
  Ejemplo de definición por comprensión: El conjunto de los pares es el
  de los números n para los que existe un m tal que n = 2*m.
*}

definition Pares :: "nat set" where
  "Pares ≡ {n. ∃m. n = 2*m }"

text {*
  Ejemplo. Los números 2 y 34 son pares.
*}

lemma 
  "2 ∈ Pares ∧
   34 ∈ Pares" 
by (simp add: Pares_def)

text {*
  Definición. El conjunto de los impares es el de los números n para los
  que existe un m tal que n = 2*m + 1.
*}

definition Impares :: "nat set" where
  "Impares ≡ {n. ∃m. n = 2*m + 1}"

text {*
  Ejemplo con las reglas de intersección y comprensión: El conjunto de
  los pares es disjunto con el de los impares. 
*}

― ‹La demostración detallada es›
lemma "x ∉ (Pares ∩ Impares)"
proof 
  fix x assume S: "x ∈ (Pares ∩ Impares)"
  then have "x ∈ Pares" by (rule IntD1)
  then have "∃m. x = 2 * m" by (simp only: Pares_def mem_Collect_eq)
  then obtain p where p: "x = 2 * p" .. 
  from S have "x ∈ Impares" by (rule IntD2)
  then have "∃ m. x = 2 * m + 1" by (simp only: Impares_def mem_Collect_eq)
  then obtain q where q: "x = 2 * q + 1" .. 
  from p and q show "False" by arith
qed

― ‹La demostración estructurada es›
lemma "x ∉ (Pares ∩ Impares)"
proof 
  fix x assume S: "x ∈ (Pares ∩ Impares)"
  then have "x ∈ Pares" ..
  then have "∃m. x = 2 * m" by (simp only: Pares_def mem_Collect_eq)
  then obtain p where p: "x = 2 * p" .. 
  from S have "x ∈ Impares" ..
  then have "∃ m. x = 2 * m + 1" by (simp only: Impares_def mem_Collect_eq)
  then obtain q where q: "x = 2 * q + 1" .. 
  from p and q show "False" by arith
qed

― ‹La demostración automática es›
lemma "x ∉ (Pares ∩ Impares)"
by (auto simp add: Pares_def Impares_def, arith)

subsection {* Cuantificadores acotados *}

text {*
  Reglas de cuantificador universal acotado ("bounded"):
  · ballI: (⋀x. x ∈ A ⟹ P x) ⟹ ∀x∈A. P x
  · bspec: ⟦∀x∈A. P x; x ∈ A⟧ ⟹ P x

  Reglas de cuantificador existencial acotado ("bounded"):
  · bexI: ⟦P x; x ∈ A⟧ ⟹ ∃x∈A. P x
  · bexE: ⟦∃x∈A. P x; ⋀x. ⟦x ∈ A; P x⟧ ⟹ Q⟧ ⟹ Q

  Reglas de la unión indexada:
  · UN_iff: (b ∈ (⋃x∈A. B x)) = (∃x∈A. b ∈ B x)
  · UN_I:   ⟦a ∈ A; b ∈ B a⟧ ⟹ b ∈ (⋃x∈A. B x)
  · UN_E:   ⟦b ∈ (⋃x∈A. B x); ⋀x. ⟦x ∈ A; b ∈ B x⟧ ⟹ R⟧ ⟹ R

  Reglas de la unión de una familia:
  · Union_def: ⋃S = (⋃x∈S. x)
  · Union_iff: (A ∈ ⋃C) = (∃X∈C. A ∈ X)

  Reglas de la intersección indexada:
  · INT_iff: (b ∈ (⋂x∈A. B x)) = (∀x∈A. b ∈ B x)
  · INT_I:   (⋀x. x ∈ A ⟹ b ∈ B x) ⟹ b ∈ (⋂x∈A. B x)
  · INT_E:   ⟦b ∈ (⋂x∈A. B x); b ∈ B a ⟹ R; a ∉ A ⟹ R⟧ ⟹ R

  Reglas de la intersección de una familia:
  · Inter_def: ⋂S = (⋂x∈S. x)
  · Inter_iff: (A ∈ ⋂C) = (∀X∈C. A ∈ X)

  Abreviaturas:
  · "Collect P" es lo mismo que "{x. P}".
  · "All P"     es lo mismo que "∀x. P x".
  · "Ex P"      es lo mismo que "∃x. P x".
  · "Ball A P"  es lo mismo que "∀x∈A. P x".
  · "Bex A P"   es lo mismo que "∃x∈A. P x".
*}

subsection {* Conjuntos finitos y cardinalidad *}

text {*
  El número de elementos de un conjunto finito A es el cardinal de A y
  se representa por "card A".
*}

text {*
  Ejemplos de cardinales de conjuntos finitos.
*}

lemma 
  "card {} = 0 ∧
   card {4} = 1 ∧
   card {4,1} = 2 ∧
   x ≠ y ⟹ card {x,y} = 2" 
by simp

text {* 
  Propiedades de cardinales:
  · Cardinal de la unión de conjuntos finitos:
    card_Un_Int: ⟦finite A; finite B⟧ 
                 ⟹ card A + card B = card (A ∪ B) + card (A ∩ B)" 
  · Cardinal del conjunto potencia: 
    card_Pow: finite A ⟹ card (Pow A) = 2 ^ card A
*}

section {* Funciones *}

text {* 
  La teoría de funciones es HOL/Fun.thy. 
*}

subsection {* Nociones básicas de funciones *}

text {*
  Principio de extensionalidad para funciones:
  · ext: (⋀x. f x = g x) ⟹ f = g

  Actualización de funciones  
  · fun_upd_apply: (f(x := y)) z = (if z = x then y else f z)
  · fun_upd_upd:   f(x := y, x := z) = f(x := z)

  Función identidad
  · id_def: id ≡ λx. x

  Composición de funciones:
  · o_def: f ∘ g = (λx. f (g x))

  Asociatividad de la composición:
  · o_assoc: f ∘ (g ∘ h) = (f ∘ g) ∘ h
*}

subsection {* Funciones inyectivas, suprayectivas y biyectivas *}

text {*
  Función inyectiva sobre A:
  · inj_on_def: inj_on f A ≡ ∀x∈A. ∀y∈A. f x = f y ⟶ x = y

  Nota. "inj f" es una abreviatura de "inj_on f UNIV".

  Función suprayectiva:
  · surj_def: surj f ≡ ∀y. ∃x. y = f x

  Función biyectiva:
  · bij_def: bij f ≡ inj f ∧ surj f

  Propiedades de las funciones inversas:
  · inv_f_f:      inj f  ⟹ inv f (f x) = x
  · surj_f_inv_f: surj f ⟹ f (inv f y) = y
  · inv_inv_eq:   bij f  ⟹ inv (inv f) = f

  Igualdad de funciones (por extensionalidad):
  · fun_eq_iff: (f = g) = (∀x. f x = g x)
*}

text {*
  Ejemplo de lema de demostración de propiedades de funciones: Una
  función inyectiva puede cancelarse en el lado izquierdo de la
  composición de funciones. 
*}

― ‹La demostración detallada es›
lemma 
  assumes "inj f"
  shows "(f ∘ g = f ∘ h) = (g = h)"
proof 
  assume "f ∘ g = f ∘ h"
  show "g = h"
  proof
    fix x
    have "(f ∘ g)(x) = (f ∘ h)(x)" using `f ∘ g = f ∘ h` by simp
    then have "f(g(x)) = f(h(x))" by simp
    then show "g(x) = h(x)" using `inj f` by (simp add:inj_on_def)
  qed
next
  assume "g = h"
  show "f ∘ g = f ∘ h"
  proof
    fix x
    have "(f ∘ g) x = f(g(x))" by simp
    also have "… = f(h(x))" using `g = h` by simp
    also have "… = (f ∘ h) x" by simp
    finally show "(f ∘ g) x = (f ∘ h) x" by simp
  qed
qed

― ‹La demostración estructurada es›
lemma 
  assumes "inj f"
  shows "(f ∘ g = f ∘ h) = (g = h)"
proof 
  assume "f ∘ g = f ∘ h" 
  then show "g = h" using `inj f` by (simp add: inj_on_def fun_eq_iff) 
next
  assume "g = h" 
  then show "f ∘ g = f ∘ h" by auto
qed

― ‹La demostración automática es›
lemma 
  assumes "inj f"
  shows "(f ∘ g = f ∘ h) = (g = h)"
using assms
by (auto simp add: inj_on_def fun_eq_iff) 

subsubsection {* Función imagen *}

text {*
  Imagen de un conjunto mediante una función:
  · image_def: f ` A = {y. (∃x∈A. y = f x)}

  Propiedades de la imagen:
  · image_compose: (f ∘ g)`r = f`g`r
  · image_Un:      f`(A ∪ B) = f`A ∪ f`B 
  · image_Int:     inj f ⟹ f`(A ∩ B) = f`A ∩ f`B" 
*}

text {*
  Ejemplo de demostración de propiedades de la imagen:
     f`A ∪ g`A = (⋃x∈A. {f x, g x})
*}

lemma "f`A ∪ g`A = (⋃x∈A. {f x, g x})"
by auto

text {*
  Ejemplo de demostración de propiedades de la imagen:
     f`{(x,y). P x y} = {f(x,y) | x y. P x y}
*}

lemma "f`{(x,y). P x y} = {f(x,y) | x y. P x y}"
by auto

text {*
  El rango de una función ("range f") es la imagen del universo 
  ("f`UNIV"). 

  Imagen inversa de un conjunto:
  · vimage_def: f -` B ≡ {x. f x ∈ B}

  Propiedad de la imagen inversa de un conjunto:
  · vimage_Compl: f -` (-A) = -(f -` A)
*}

section {* Relaciones *}

subsection {* Relaciones básicas *}

text {*
  La teoría de relaciones es HOL/Relation.thy.

  Las relaciones son conjuntos de pares.

  Relación identidad:
  · Id_def: Id ≡ {p. ∃x. p = (x,x)}

  Composición de relaciones:
  · rel_comp_def: r O s ≡ {(x,z). ∃y. (x, y) ∈ r ∧ (y, z) ∈ s}

  Propiedades:
  · R_O_Id:        R O Id = R
  · rel_comp_mono: ⟦r' ⊆ r; s' ⊆ s⟧ ⟹ (r' O s') ⊆ (r O s)

  Imagen inversa de una relación:
  · converse_iff: ((a,b) ∈ r^-1) = ((b,a) ∈ r)

  Propiedad de la imagen inversa de una relación:
  · converse_rel_comp: (r O s)^-1 = s^-1 O r^-1

  Imagen de un conjunto mediante una relación:
  · Image_iff: (b ∈ r``A) = (∃x:A. (x, b) ∈ r)

  Dominio de una relación:
  · Domain_iff: (a ∈ Domain r) = (∃y. (a, y) ∈ r)

  Rango de una relación:
  · Range_iff: (a ∈ Range r) = (∃y. (y,a) ∈ r)
*}

end

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

158

159

160

161

162

163

164

165

166

167

168

169

170

171

172

173

174

175

176

177

178

179

180

181

182

183

184

185

186

187

188

189

190

191

192

193

194

195

196

197

198

199

200

201

202

203

204

205

206

207

208

209

210

211

212

213

214

215

216

217

218

219

220

221

222

223

224

225

226

227

228

229

230

231

232

233

234

235

236

237

238

239

240

241

242

243

244

245

246

247

248

249

250

251

252

253

254

255

256

257

258

259

260

261

262

263

264

265

266

267

268

269

270

271

272

273

274

275

276

277

278

279

280

281

282

283

284

285

286

287

288

289

290

291

292

293

294

295

296

297

298

299

300

301

302

303

304

305

306

307

308

309

310

311

312

313

314

315

316

317

318

319

320

321

322

323

324

325

326

327

328

329

330

331

332

333

334

335

336

337

338

339

340

341

342

343

344

345

346

347

348

349

350

351

352

353

354

355

356

357

358

359

360

361

362

363

364

365

366

367

368

369

370

371

372

373

374

375

376

377

378

379

380

381

382

383

384

385

386

387

388

389

390

391

392

393

394

395

396

397

398

399

400

401

402

403

404

405

406

407

408

409

410

411

412

413

414

415

416

417

418

419

420

421

422

423

424

425

426

427

428

429

430

431

432

433

434

435

436

437

438

439

440

441

442

443

444

445

446

447

448

449

450

451

452

453

454

455

456

457

458

459

460

461

462

463

464

465

466

467

468

469

470

471

472

473

474

475

476

477

478

479

480

481

482

483

484

485

486

487

488

489

490

491

492

493

494

495

496

497

498

499

500

501

502

503

504

505

506

507

508

509

510

511

512

513

514

515

516

517

518

519

520

521

522

523

524

525

526

527

528

529

530

531

532

533

534

535

536

537

538

539

540

541

542

543

544

545

546

547

548

549

550

551

552

553

554

555

556

557

558

559

560

561

562

563

564

565

566

567

568

569

570

571

572

573

574

575

576

577

578

579

580

581

chapter {* Tema 12: Conjuntos, funciones y relaciones *}

theory T12_Conjuntos_funciones_y_relaciones

imports Main

begin

section {* Conjuntos *}

subsection {* Operaciones con conjuntos *}

text {*

Nota. La teoría elemental de conjuntos es HOL/Set.thy.

Nota. En un conjunto todos los elemento son del mismo tipo (por

ejemplo, del tipo τ) y el conjunto tiene tipo (en el ejemplo, "τ set").

Reglas de la intersección:

· IntI: ⟦c ∈ A; c ∈ B⟧ ⟹ c ∈ A ∩ B

· IntD1: c ∈ A ∩ B ⟹ c ∈ A

· IntD2: c ∈ A ∩ B ⟹ c ∈ B

Nota. Propiedades del complementario:

· Compl_iff: (c ∈ - A) = (c ∉ A)

· Compl_Un: - (A ∪ B) = - A ∩ - B

Nota. El conjunto vacío se representa por {} y el universal por UNIV.

Nota. Propiedades de la diferencia y del complementario:

· Diff_disjoint: A ∩ (B - A) = {}

· Compl_partition: A ∪ - A = UNIV

Nota. Reglas de la relación de subconjunto:

· subsetI: (⋀x. x ∈ A ⟹ x ∈ B) ⟹ A ⊆ B

· subsetD: ⟦A ⊆ B; c ∈ A⟧ ⟹ c ∈ B

text {*

Ejemplo: A ∪ B ⊆ C syss A ⊆ C ∧ B ⊆ C.

lemma "(A ∪ B ⊆ C) = (A ⊆ C ∧ B ⊆ C)"

by blast

text {*

Ejemplo: A ⊆ -B syss B ⊆ -A.

lemma "(A ⊆ -B) = (B ⊆ -A)"

by blast

text {*

Principio de extensionalidad de conjuntos:

· set_eqI: (⋀x. (x ∈ A) = (x ∈ B)) ⟹ A = B

Reglas de la igualdad de conjuntos:

· equalityI: ⟦A ⊆ B; B ⊆ A⟧ ⟹ A = B

· equalityD1: A = B ⟹ A ⊆ B

· equalityD2: A = B ⟹ B ⊆ A

· equalityE: ⟦A = B; ⟦A ⊆ B; B ⊆ A⟧ ⟹ P⟧ ⟹ P

text {*

Lema. [Analogía entre intersección y conjunción]

"x ∈ A ∩ B" syss "x ∈ A" y "x ∈ B".

lemma "(x ∈ A ∩ B) = (x ∈ A ∧ x ∈ B)"

by simp

text {*

Lema. [Analogía entre unión y disyunción]

x ∈ A ∪ B syss x ∈ A ó x ∈ B.

lemma "(x ∈ A ∪ B) = (x ∈ A ∨ x ∈ B)"

by simp

text {*

Lema. [Analogía entre subconjunto e implicación]

A ⊆ B syss para todo x, si x ∈ A entonces x ∈ B.

lemma "(A ⊆ B) = (∀ x. x ∈ A ⟶ x ∈ B)"

by auto

text {*

Lema. [Analogía entre complementario y negación]

x pertenece al complementario de A syss x no pertenece a A.

lemma "(x ∈ -A) = (x ∉ A)"

by simp

subsection {* Notación de conjuntos finitos *}

text {*

Nota. La teoría de conjuntos finitos es HOL/Finite_Set.thy.

Nota. Los conjuntos finitos se definen por inducción a partir de las

siguientes reglas inductivas:

· El conjunto vacío es un conjunto finito.

· emptyI: "finite {}"

· Si se le añade un elemento a un conjunto finito se obtiene otro

conjunto finito.

· insertI: "finite A ⟹ finite (insert a A)"

A continuación se muestran ejemplos de conjuntos finitos.

lemma

"insert 2 {} = {2} ∧

insert 3 {2} = {2,3} ∧

insert 2 {2,3} = {2,3} ∧

{2,3} = {3,2,3,2,2}"

by auto

text {*

Nota. Los conjuntos finitos se representan con la notación conjuntista

habitual: los elementos entre llaves y separados por comas.

text {*

Ejemplo: {a,b} ∪ {c,d} = {a,b,c,d}

lemma "{a,b} ∪ {c,d} = {a,b,c,d}"

by blast

text {*

Ejemplo de conjetura falsa y su refutación.

lemma "{a,b} ∩ {b,c} = {b}"

oops

text {*

Ejemplo con la conjetura corregida.

lemma "{a,b} ∩ {b,c} = (if a = c then {a,b} else {b})"

by auto

text {*

Sumas de conjuntos finitos:

· ∑A es la suma de los elementos del conjunto finito A. Por ejemplo,

value "∑{1,2,3}::int" -- "= 6"

· (setsum f A) es la suma de la aplicación de f a los elementos del

conjunto finito A, Por ejemplo,

value "setsum (λx. x*x) {1,2,3}::int" -- "= 14"

text {*

Ejemplos de definiciones recursivas sobre conjuntos finitos:

Sea A un conjunto finito de números naturales.

· sumaConj A es la suma de los elementos A.

· sumaCuadradosConj A es la suma de los cuadrados de los elementos A.

definition sumaConj :: "nat set ⇒ nat" where

"sumaConj S ≡ ∑S"

value "sumaConj {2,5,3}" ― ‹= 10›

value "∑{2::nat,5,3}" ― ‹= 10›

definition sumaCuadradosConj :: "nat set ⇒ nat" where

"sumaCuadradosConj S ≡ ∑x∈S. x*x"

value "sumaCuadradosConj {2,5,3}" ― ‹= 38›

text {*

Nota. Para simplificar lo que sigue, declaramos las anteriores

definiciones como reglas de simplificación.

declare sumaConj_def [simp]

declare sumaCuadradosConj_def [simp]

text {*

Ejemplos de evaluación de las anteriores definiciones recursivas.

lemma

"sumaConj {1,2,3,4} = 10 ∧

sumaCuadradosConj {1,2,3,4} = 30"

by simp

text {*

Inducción sobre conjuntos finitos: Para demostrar que todos los

conjuntos finitos tienen una propiedad P basta probar que

· El conjunto vacío tiene la propiedad P.

· Si a un conjunto finito que tiene la propiedad P se le añade un

nuevo elemento, el conjunto obtenido sigue teniendo la propiedad P.

En forma de regla

· finite_induct: ⟦finite F;

P {};

⋀x F. ⟦finite F; x ∉ F; P F⟧ ⟹ P ({x} ∪ F)⟧

⟹ P F

text {*

Ejemplo de inducción sobre conjuntos finitos: Sea S un conjunto finito

de números naturales. Entonces todos los elementos de S son menores o

iguales que la suma de los elementos de S.

― ‹La demostración automática es›

lemma "finite S ⟹ ∀x∈S. x ≤ sumaConj S"

by (induct rule: finite_induct) auto

― ‹La demostración estructurada es›

lemma sumaConj_acota:

"finite S ⟹ ∀x∈S. x ≤ sumaConj S"

proof (induct rule: finite_induct)

show "∀x ∈ {}. x ≤ sumaConj {}" by simp

fix x and F

assume fF: "finite F"

and xF: "x ∉ F"

and HI: "∀ x∈F. x ≤ sumaConj F"

show "∀y ∈ insert x F. y ≤ sumaConj (insert x F)"

proof

fix y

assume "y ∈ insert x F"

show "y ≤ sumaConj (insert x F)"

proof (cases "y = x")

assume "y = x"

then have "y ≤ x + (sumaConj F)" by simp

also have "… = sumaConj (insert x F)" using fF xF by simp

finally show ?thesis .

assume "y ≠ x"

then have "y ∈ F" using `y ∈ insert x F` by simp

then have "y ≤ sumaConj F" using HI by blast

also have "… ≤ x + (sumaConj F)" by simp

also have "… = sumaConj (insert x F)" using fF xF by simp

finally show ?thesis .

qed

subsection {* Definiciones por comprensión *}

text {*

El conjunto de los elementos que cumple la propiedad P se representa

por {x. P}.

Reglas de comprensión (relación entre colección y pertenencia):

· mem_Collect_eq: (a ∈ {x. P x}) = P a

· Collect_mem_eq: {x. x ∈ A} = A

text {*

Ejemplo de comprensión: {x. P x ∨ x ∈ A} = {x. P x} ∪ A

lemma "{x. P x ∨ x ∈ A} = {x. P x} ∪ A"

by blast

text {*

Ejemplo de comprensión: {x. P x ⟶ Q x} = -{x. P x} ∪ {x. Q x}

lemma "{x. P x ⟶ Q x} = -{x. P x} ∪ {x. Q x}"

by blast

text {*

Ejemplo con la sintaxis general de comprensión.

{p*q | p q. p ∈ prime ∧ q ∈ prime} =

{z. ∃p q. z = p*q ∧ p ∈ prime ∧ q ∈ prime}

lemma

"{p*q | p q. p ∈ prime ∧ q ∈ prime} =

{z. ∃p q. z = p*q ∧ p ∈ prime ∧ q ∈ prime}"

by blast

text {*

En HOL, la notación conjuntista es azúcar sintáctica:

· x ∈ A es equivalente a A(x).

· {x. P} es equivalente a λx. P.

text {*

Ejemplo de definición por comprensión: El conjunto de los pares es el

de los números n para los que existe un m tal que n = 2*m.

definition Pares :: "nat set" where

"Pares ≡ {n. ∃m. n = 2*m }"

text {*

Ejemplo. Los números 2 y 34 son pares.

lemma

"2 ∈ Pares ∧

34 ∈ Pares"

by (simp add: Pares_def)

text {*

Definición. El conjunto de los impares es el de los números n para los

que existe un m tal que n = 2*m + 1.

definition Impares :: "nat set" where

"Impares ≡ {n. ∃m. n = 2*m + 1}"

text {*

Ejemplo con las reglas de intersección y comprensión: El conjunto de

los pares es disjunto con el de los impares.

― ‹La demostración detallada es›

lemma "x ∉ (Pares ∩ Impares)"

proof

fix x assume S: "x ∈ (Pares ∩ Impares)"

then have "x ∈ Pares" by (rule IntD1)

then have "∃m. x = 2 * m" by (simp only: Pares_def mem_Collect_eq)

then obtain p where p: "x = 2 * p" ..

from S have "x ∈ Impares" by (rule IntD2)

then have "∃ m. x = 2 * m + 1" by (simp only: Impares_def mem_Collect_eq)

then obtain q where q: "x = 2 * q + 1" ..

from p and q show "False" by arith

qed

― ‹La demostración estructurada es›

lemma "x ∉ (Pares ∩ Impares)"

proof

fix x assume S: "x ∈ (Pares ∩ Impares)"

then have "x ∈ Pares" ..

then have "∃m. x = 2 * m" by (simp only: Pares_def mem_Collect_eq)

then obtain p where p: "x = 2 * p" ..

from S have "x ∈ Impares" ..

then have "∃ m. x = 2 * m + 1" by (simp only: Impares_def mem_Collect_eq)

then obtain q where q: "x = 2 * q + 1" ..

from p and q show "False" by arith

qed

― ‹La demostración automática es›

lemma "x ∉ (Pares ∩ Impares)"

by (auto simp add: Pares_def Impares_def, arith)

subsection {* Cuantificadores acotados *}

text {*

Reglas de cuantificador universal acotado ("bounded"):

· ballI: (⋀x. x ∈ A ⟹ P x) ⟹ ∀x∈A. P x

· bspec: ⟦∀x∈A. P x; x ∈ A⟧ ⟹ P x

Reglas de cuantificador existencial acotado ("bounded"):

· bexI: ⟦P x; x ∈ A⟧ ⟹ ∃x∈A. P x

· bexE: ⟦∃x∈A. P x; ⋀x. ⟦x ∈ A; P x⟧ ⟹ Q⟧ ⟹ Q

Reglas de la unión indexada:

· UN_iff: (b ∈ (⋃x∈A. B x)) = (∃x∈A. b ∈ B x)

· UN_I: ⟦a ∈ A; b ∈ B a⟧ ⟹ b ∈ (⋃x∈A. B x)

· UN_E: ⟦b ∈ (⋃x∈A. B x); ⋀x. ⟦x ∈ A; b ∈ B x⟧ ⟹ R⟧ ⟹ R

Reglas de la unión de una familia:

· Union_def: ⋃S = (⋃x∈S. x)

· Union_iff: (A ∈ ⋃C) = (∃X∈C. A ∈ X)

Reglas de la intersección indexada:

· INT_iff: (b ∈ (⋂x∈A. B x)) = (∀x∈A. b ∈ B x)

· INT_I: (⋀x. x ∈ A ⟹ b ∈ B x) ⟹ b ∈ (⋂x∈A. B x)

· INT_E: ⟦b ∈ (⋂x∈A. B x); b ∈ B a ⟹ R; a ∉ A ⟹ R⟧ ⟹ R

Reglas de la intersección de una familia:

· Inter_def: ⋂S = (⋂x∈S. x)

· Inter_iff: (A ∈ ⋂C) = (∀X∈C. A ∈ X)

Abreviaturas:

· "Collect P" es lo mismo que "{x. P}".

· "All P" es lo mismo que "∀x. P x".

· "Ex P" es lo mismo que "∃x. P x".

· "Ball A P" es lo mismo que "∀x∈A. P x".

· "Bex A P" es lo mismo que "∃x∈A. P x".

subsection {* Conjuntos finitos y cardinalidad *}

text {*

El número de elementos de un conjunto finito A es el cardinal de A y

se representa por "card A".

text {*

Ejemplos de cardinales de conjuntos finitos.

lemma

"card {} = 0 ∧

card {4} = 1 ∧

card {4,1} = 2 ∧

x ≠ y ⟹ card {x,y} = 2"

by simp

text {*

Propiedades de cardinales:

· Cardinal de la unión de conjuntos finitos:

card_Un_Int: ⟦finite A; finite B⟧

⟹ card A + card B = card (A ∪ B) + card (A ∩ B)"

· Cardinal del conjunto potencia:

card_Pow: finite A ⟹ card (Pow A) = 2 ^ card A

section {* Funciones *}

text {*

La teoría de funciones es HOL/Fun.thy.

subsection {* Nociones básicas de funciones *}

text {*

Principio de extensionalidad para funciones:

· ext: (⋀x. f x = g x) ⟹ f = g

Actualización de funciones

· fun_upd_apply: (f(x := y)) z = (if z = x then y else f z)

· fun_upd_upd: f(x := y, x := z) = f(x := z)

Función identidad

· id_def: id ≡ λx. x

Composición de funciones:

· o_def: f ∘ g = (λx. f (g x))

Asociatividad de la composición:

· o_assoc: f ∘ (g ∘ h) = (f ∘ g) ∘ h

subsection {* Funciones inyectivas, suprayectivas y biyectivas *}

text {*

Función inyectiva sobre A:

· inj_on_def: inj_on f A ≡ ∀x∈A. ∀y∈A. f x = f y ⟶ x = y

Nota. "inj f" es una abreviatura de "inj_on f UNIV".

Función suprayectiva:

· surj_def: surj f ≡ ∀y. ∃x. y = f x

Función biyectiva:

· bij_def: bij f ≡ inj f ∧ surj f

Propiedades de las funciones inversas:

· inv_f_f: inj f ⟹ inv f (f x) = x

· surj_f_inv_f: surj f ⟹ f (inv f y) = y

· inv_inv_eq: bij f ⟹ inv (inv f) = f

Igualdad de funciones (por extensionalidad):

· fun_eq_iff: (f = g) = (∀x. f x = g x)

text {*

Ejemplo de lema de demostración de propiedades de funciones: Una

función inyectiva puede cancelarse en el lado izquierdo de la

composición de funciones.

― ‹La demostración detallada es›

lemma

assumes "inj f"

shows "(f ∘ g = f ∘ h) = (g = h)"

proof

assume "f ∘ g = f ∘ h"

show "g = h"

proof

fix x

have "(f ∘ g)(x) = (f ∘ h)(x)" using `f ∘ g = f ∘ h` by simp

then have "f(g(x)) = f(h(x))" by simp

then show "g(x) = h(x)" using `inj f` by (simp add:inj_on_def)

qed

assume "g = h"

show "f ∘ g = f ∘ h"

proof

fix x

have "(f ∘ g) x = f(g(x))" by simp

also have "… = f(h(x))" using `g = h` by simp

also have "… = (f ∘ h) x" by simp

finally show "(f ∘ g) x = (f ∘ h) x" by simp

qed

― ‹La demostración estructurada es›

lemma

assumes "inj f"

shows "(f ∘ g = f ∘ h) = (g = h)"

proof

assume "f ∘ g = f ∘ h"

then show "g = h" using `inj f` by (simp add: inj_on_def fun_eq_iff)

assume "g = h"

then show "f ∘ g = f ∘ h" by auto

qed

― ‹La demostración automática es›

lemma

assumes "inj f"

shows "(f ∘ g = f ∘ h) = (g = h)"

using assms

by (auto simp add: inj_on_def fun_eq_iff)

subsubsection {* Función imagen *}

text {*

Imagen de un conjunto mediante una función:

· image_def: f ` A = {y. (∃x∈A. y = f x)}

Propiedades de la imagen:

· image_compose: (f ∘ g)`r = f`g`r

· image_Un: f`(A ∪ B) = f`A ∪ f`B

· image_Int: inj f ⟹ f`(A ∩ B) = f`A ∩ f`B"

text {*

Ejemplo de demostración de propiedades de la imagen:

f`A ∪ g`A = (⋃x∈A. {f x, g x})

lemma "f`A ∪ g`A = (⋃x∈A. {f x, g x})"

by auto

text {*

Ejemplo de demostración de propiedades de la imagen:

f`{(x,y). P x y} = {f(x,y) | x y. P x y}

lemma "f`{(x,y). P x y} = {f(x,y) | x y. P x y}"

by auto

text {*

El rango de una función ("range f") es la imagen del universo

("f`UNIV").

Imagen inversa de un conjunto:

· vimage_def: f -` B ≡ {x. f x ∈ B}

Propiedad de la imagen inversa de un conjunto:

· vimage_Compl: f -` (-A) = -(f -` A)

section {* Relaciones *}

subsection {* Relaciones básicas *}

text {*

La teoría de relaciones es HOL/Relation.thy.

Las relaciones son conjuntos de pares.

Relación identidad:

· Id_def: Id ≡ {p. ∃x. p = (x,x)}

Composición de relaciones:

· rel_comp_def: r O s ≡ {(x,z). ∃y. (x, y) ∈ r ∧ (y, z) ∈ s}

Propiedades:

· R_O_Id: R O Id = R

· rel_comp_mono: ⟦r' ⊆ r; s' ⊆ s⟧ ⟹ (r' O s') ⊆ (r O s)

Imagen inversa de una relación:

· converse_iff: ((a,b) ∈ r^-1) = ((b,a) ∈ r)

Propiedad de la imagen inversa de una relación:

· converse_rel_comp: (r O s)^-1 = s^-1 O r^-1

Imagen de un conjunto mediante una relación:

· Image_iff: (b ∈ r``A) = (∃x:A. (x, b) ∈ r)

Dominio de una relación:

· Domain_iff: (a ∈ Domain r) = (∃y. (a, y) ∈ r)

Rango de una relación:

· Range_iff: (a ∈ Range r) = (∃y. (y,a) ∈ r)

end

Se puede imprimir o compartir con