{"id":6698,"date":"2019-05-23T19:01:01","date_gmt":"2019-05-23T17:01:01","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6698"},"modified":"2019-05-25T19:01:31","modified_gmt":"2019-05-25T17:01:31","slug":"lmf2018-desarrollo-de-teorias-formalizadas-con-isabelle-hol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2018-desarrollo-de-teorias-formalizadas-con-isabelle-hol\/","title":{"rendered":"LMF2018: Desarrollo de teor\u00edas formalizadas con Isabelle\/HOL"},"content":{"rendered":"<p>En la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-18\">L\u00f3gica matem\u00e1tica y fundamentos<\/a> se ha estudiado c\u00f3mo definir desarrollar en Isabelle\/HOL teor\u00edas axiom\u00e1ticas como las de monoides, semigrupos, grupos, \u00f3rdenes y \u00f3rdenes lineales.<\/p>\n<p>La clase se ha basado en la siguiente teor\u00eda Isabelle<br \/>\n<!-- more --><\/p>\n<pre lang=\"isar\">\nchapter {* T11: Desarrollo de teor\u00edas formalizadas *}\n\ntheory T11_Desarrollo_de_teorias_formalizadas\nimports Main\nbegin\n\nsection {* Desarrollo de la teor\u00eda de grupos*}\n\ntext {*\n  El objetivo de este tema es mostrar c\u00f3mo se puede trabajar en\n  estructuras algebraicas por medio de locales. Se usar\u00e1 como ejemplo la\n  teor\u00eda de grupos. *}\n\ntext {*\n  Ejemplo 1. Un grupo es una estructura (G,\u00b7,\ud835\udfed,^) tal que G es un\n  conjunto, \u00b7 es una operaci\u00f3n binaria en G, \ud835\udfed es un elemento de G y ^\n  es una funci\u00f3n de G en G tales que se cumplen las siguientes\n  propiedades:\n  * asociativa: \u2200x y z. x \u22c5 (y \u22c5 z) = (x \u22c5 y) \u22c5 z\n  * neutro por la izquierda: \u2200x. \ud835\udfed \u22c5 x = x\n  * inverso por la izquierda: \u2200x. x^ \u22c5 x = \ud835\udfed \n  Definir el entorno axiom\u00e1tico de los grupos. *}\n\nlocale grupo = \n  fixes prod :: \"['a, 'a] \u21d2 'a\" (infixl \"\u22c5\" 70)\n    and neutro (\"\ud835\udfed\") \n    and inverso (\"_^\" [100] 100)\n  assumes asociativa: \"(x \u22c5 y) \u22c5 z = x \u22c5 (y \u22c5 z)\"\n      and neutro_i:   \"\ud835\udfed \u22c5 x = x\"\n      and inverso_i:  \"x^ \u22c5 x = \ud835\udfed\"\n\ntext {*\n  Notas sobre notaci\u00f3n:\n  * El producto es \u22c5 y se escribe con \\ cdot (sin espacio entre ellos). \n  * El neutro es \ud835\udfed y se escribe con \\ y <one> (sin espacio entre ellos).\n  * El inverso de x es x^ y se escribe con pulsando 2 veces en ^. *}\n\ntext {*\n  A continuaci\u00f3n se crea un contexto en el que se supone la notaci\u00f3n y\n  axiomas de grupos. En el contexto se demuestran propiedades de los\n  grupos. *}\n\ncontext grupo\nbegin\n\ntext {*\n  Ejemplo 2. En los grupos, x^ tambi\u00e9n es el inverso de x por la\n  derecha; es decir \n     x \u22c5 x^ = \ud835\udfed   *}\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica (obtenida con Sledgehammer) es\u203a\nlemma \"x \u22c5 x^ = \ud835\udfed\"\n  by (metis asociativa inverso_i neutro_i)\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma inverso_d: \n  \"x \u22c5 x^ = \ud835\udfed\"\nproof -\n  have \"x \u22c5 x^ = \ud835\udfed \u22c5 (x \u22c5 x^)\" by (simp only: neutro_i)\n  also have \"\u2026 = (\ud835\udfed \u22c5 x) \u22c5 x^\" by (simp only: asociativa)\n  also have \"\u2026 = (((x^)^ \u22c5 x^) \u22c5 x) \u22c5 x^\" by (simp only: inverso_i)\n  also have \"\u2026 = ((x^)^ \u22c5 (x^ \u22c5 x)) \u22c5 x^\" by (simp only: asociativa)\n  also have \"\u2026 = ((x^)^ \u22c5 \ud835\udfed) \u22c5 x^\" by (simp only: inverso_i)\n  also have \"\u2026 = (x^)^ \u22c5 (\ud835\udfed \u22c5 x^)\" by (simp only: asociativa)\n  also have \"\u2026 = (x^)^ \u22c5 x^\" by (simp only: neutro_i)\n  also have \"\u2026 = \ud835\udfed\" by (simp only: inverso_i)\n  finally show ?thesis .\nqed\n\ntext {*\n  Ejemplo 2. En los grupos, \ud835\udfed tambi\u00e9n es el neutro por la derecha; es decir \n     x \u22c5 \ud835\udfed = x   *}\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica (obtenida con Sledgehammer) es\u203a\nlemma \"x \u22c5 \ud835\udfed = x\"\n  by (metis asociativa inverso_i neutro_i)\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma neutro_d: \n  \"x \u22c5 \ud835\udfed = x\"\nproof -\n  have \"x \u22c5 \ud835\udfed = x \u22c5 (x^ \u22c5 x)\" by (simp only: inverso_i)\n  also have \"\u2026 = (x \u22c5 x^) \u22c5 x\" by (simp only: asociativa)\n  also have \"\u2026 = \ud835\udfed \u22c5 x\" by (simp only: inverso_d)\n  also have \"\u2026 = x\" by (simp only: neutro_i)\n  finally show \"x \u22c5 \ud835\udfed = x\" .\nqed \n\ntext {*\n  Ejemplo 3. En los grupos, se tiene la propiedad cancelativa por la\n  izquierda; es decir,\n     x \u22c5 y = x \u22c5 z syss y = z   *}\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica (obtenida con Sledgehammer) es\u203a\nlemma \"(x \u22c5 y = x \u22c5 z) = (y = z)\"\n  by (metis asociativa inverso_i neutro_i)\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma cancelativa_i: \n  \"(x \u22c5 y = x \u22c5 z) = (y = z)\"\nproof\n  assume \"x \u22c5 y = x \u22c5 z\"\n  hence \"x^ \u22c5 (x \u22c5 y) = x^ \u22c5 (x \u22c5 z)\" by simp\n  hence \"(x^ \u22c5 x) \u22c5 y = (x^ \u22c5 x) \u22c5 z\" by (simp only: asociativa)\n  hence \"\ud835\udfed \u22c5 y = \ud835\udfed \u22c5 z\" by (simp only: inverso_i)\n  thus \"y = z\" by (simp only: neutro_i)\nnext\n  assume \"y = z\"\n  then show \"x \u22c5 y = x \u22c5 z\" by simp\nqed\n\ntext {*\n  Ejemplo 4. En los grupos, el elemento neutro por la izquierda es\n  \u00fanico; es decir, si e es un elemento tal que para todo x se tiene que \n  e \u22c5 x = x, entonces e = \ud835\udfed. *}\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es (obtenida con Sledgehammer) es\u203a\nlemma \n  assumes \"e \u22c5 x = x\"\n  shows \"\ud835\udfed = e\"\n  using assms\n  by (metis asociativa inverso_d neutro_d)\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma unicidad_neutro_i:\n  assumes \"e \u22c5 x = x\"\n  shows \"\ud835\udfed = e\"\nproof -\n  have \"\ud835\udfed = x \u22c5 x^\" by (simp only: inverso_d)\n  also have \"... = (e \u22c5 x) \u22c5 x^\" using assms by simp\n  also have \"... = e \u22c5 (x \u22c5 x^)\" by (simp only: asociativa)\n  also have \"... = e \u22c5 \ud835\udfed\" by (simp only: inverso_d)\n  also have \"... = e\" by (simp only: neutro_d)\n  finally show ?thesis .\nqed \n\ntext {*\n  Ejemplo 5. En los grupos, los inversos por la izquierda son \u00fanicos; es\n  decir, si x' es un elemento tal que x' \u22c5 x = \ud835\udfed, entonces x^ x'. *}\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica (obtenida con Sledgehammer) es\u203a\nlemma \n  assumes \"x' \u22c5 x = \ud835\udfed\"\n  shows \"x^ = x'\"\n  using assms\n  by (metis asociativa inverso_i neutro_i)\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma unicidad_inverso_i:\n  assumes \"x' \u22c5 x = \ud835\udfed\"\n  shows \"x^ = x'\"\nproof -\n  have \"x^ = \ud835\udfed \u22c5 x^\" by (simp only: neutro_i)\n  also have \"... = (x' \u22c5 x) \u22c5 x^\" using assms by simp\n  also have \"... = x' \u22c5 (x \u22c5 x^)\" by (simp only: asociativa)\n  also have \"... = x' \u22c5 \ud835\udfed\" by (simp only: inverso_d)\n  also have \"... = x'\" by (simp only: neutro_d)\n  finally show ?thesis .\nqed\n\ntext {*\n  Ejemplo 6. En los grupos, es inverso de un producto es el producto de\n  los inversos cambiados de orden; es decir,\n     (x \u22c5 y)^ = y^ \u22c5 x^    *}\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica (obtenida con Sledgehammer) es\u203a\nlemma \"(x \u22c5 y)^ = y^ \u22c5 x^\"\n  by (metis asociativa inverso_d neutro_d)\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma inversa_producto:\n  \"(x \u22c5 y)^ = y^ \u22c5 x^\"\nproof (rule unicidad_inverso_i)\n  show \"(y^ \u22c5 x^) \u22c5 (x \u22c5 y) = \ud835\udfed\"\n  proof -\n    have \"(y^ \u22c5 x^) \u22c5 (x \u22c5 y) = (y^ \u22c5 (x^ \u22c5 x)) \u22c5 y\" \n      by (simp only: asociativa)\n    also have \"... = (y^ \u22c5 \ud835\udfed) \u22c5 y\" by (simp only: inverso_i)\n    also have \"... = y^ \u22c5 y\" by (simp only: neutro_d)\n    also have \"... = \ud835\udfed\" by (simp only: inverso_i)\n    finally show ?thesis .\n  qed\nqed\n\ntext {*\n  Ejemplo 7. En los grupos, el inverso del inverso es el propio\n  elemento; es decir, \n     (x^)^ = x    *}\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica (obtenida con Sledgehammer) es\u203a\nlemma \"(x^)^ = x\"\n  using inverso_d unicidad_inverso_i by blast\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma inverso_inverso: \n  \"(x^)^ = x\"\nproof (rule unicidad_inverso_i)\n  show \"x \u22c5 x^ = \ud835\udfed\" by (simp only: inverso_d)\nqed\n\ntext {*\n  Ejemplo 8. En los grupos, la funci\u00f3n inversa es inyectiva; es decir,\n  si x e y tienen los mismos inversos, entonces son iguales. *}\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es (obtenida con Sledgehammer) es\u203a\nlemma \n  assumes \"x^ = y^\"\n  shows \"x = y\"\n  using assms\n  by (metis inverso_inverso)\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica estructurada es\u203a\nlemma inversa_inyectiva:\n  assumes \"x^ = y^\"\n  shows \"x = y\"\nproof -\n  have \"(x^)^ = (y^)^\" using assms by simp\n  thus \"x = y\" by (simp only: inverso_inverso)\nqed\n\nend\n\nsection {* Teor\u00edas de \u00f3rdenes mediante clases *}\n\ntext {*\n  El tutorial sobre clases est\u00e1 en la teor\u00eda Clases.thy.\n  \n  La clase de los \u00f3rdenes es la colecci\u00f3n de los tipos que poseen una\n  relaci\u00f3n \u227c verificando las siguientes propiedades\n  \u00b7 reflexiva: x \u227c x\n  \u00b7 transitiva: \u27e6x \u227c y; y \u227c z\u27e7 \u27f9 x \u227c z\n  \u00b7 antisim\u00e9trica: \u27e6x \u227c y; y \u227c x\u27e7 \u27f9 x = y\n*}\n\nclass orden = \n  fixes menor_ig :: \"'a \u21d2 'a \u21d2 bool\"  (infix \"\u227c\" 50)\n  assumes refl: \"x \u227c x\"\n      and trans: \"\u27e6x \u227c y; y \u227c z\u27e7 \u27f9 x \u227c z\"\n      and antisim: \"\u27e6x \u227c y; y \u227c x\u27e7 \u27f9 x = y\"\n\ntext {*\n  Ha generado los teoremas correspondientes a los axiomas. Pueden \n  consultarse mediante thm como se muestra a continuaci\u00f3n.\n*}\n\nthm trans\n\ntext {*\n  Se inicia el contexto orden en el que se van a realizar definiciones y\n  demostraciones. \n*}\n\ncontext orden\nbegin\n\ntext {*\n  x es menor que y si x es menor o igual que y y no son iguales.\n*}\n\ndefinition menor :: \"'a \u21d2 'a \u21d2 bool\"  (infix \"\u227a\" 50)\n  where \"x \u227a y \u27f7 x \u227c y \u2227 \u00ac y \u227c x\"\n\ntext {*\n    La relaci\u00f3n menor es irreflexiva.\n*}\n\nlemma irrefl: \"\u00ac x \u227a x\"\n  by (auto simp: menor_def)\n\ntext {*\n  La relaci\u00f3n menor es transitiva.\n*}\n\n(* Demostraci\u00f3n aplicativa *)\nlemma \"\u27e6x \u227a y; y \u227a z\u27e7 \u27f9 x \u227a z\"\n  apply (unfold menor_def)\n    (* \u27e6x \u227c y \u2227 \u00ac y \u227c x; y \u227c z \u2227 \u00ac z \u227c y\u27e7 \u27f9 x \u227c z \u2227 \u00ac z \u227c x *)\n  apply (auto intro: trans)\n    (* *)\n  done\n\n(* Demostraci\u00f3n autom\u00e1tica *)\nlemma menor_trans: \"\u27e6x \u227a y; y \u227a z\u27e7 \u27f9 x \u227a z\"\n  by (auto simp: menor_def intro: trans)\n\ntext {*\n  La relaci\u00f3n menor es asim\u00e9trica; es decir, si x \u227a y e y \u227a x, entonces\n  se verifica cualquier propiedad P. \n*}\n\nlemma asimetrica: \"x \u227a y \u27f9 y \u227a x \u27f9 P\"\n  by (simp add: menor_def)\n\nend\n\nsubsection {* Subclase *}\n\ntext {*\n  Un orden lineal es un orden en que cada par de elementos son comparables.\n*}\n\nclass ordenLineal = orden +\n  assumes lineal: \"x \u227c y \u2228 y \u227c x\"\nbegin\n\ntext {*\n  En los \u00f3rdenes lineales se tiene que x \u227a y \u2228 x = y \u2228 y \u227a x.\n*}\n\n(* Demostraci\u00f3n aplicativa *)\nlemma \"x \u227a y \u2228 x = y \u2228 y \u227a x\"\n  apply (unfold menor_def)\n      (* (x \u227c y \u2227 \u00ac y \u227c x) \u2228 x = y \u2228 (y \u227c x \u2227 \u00ac x \u227c y) *)\n  apply auto\n      (*  1. \u27e6x \u2260 y; \u00ac x \u227c y\u27e7 \u27f9 y \u227c x\n          2. \u27e6x \u2260 y; y \u227c x; x \u227c y\u27e7 \u27f9 False *)\n   apply (cut_tac x=x and y=y in lineal)\n      (* 1. \u27e6x \u2260 y; \u00ac x \u227c y; x \u227c y \u2228 y \u227c x\u27e7 \u27f9 y \u227c x\n         2. \u27e6x \u2260 y; y \u227c x; x \u227c y\u27e7 \u27f9 False *)\n   apply (erule disjE)\n      (* 1. \u27e6x \u2260 y; \u00ac x \u227c y; x \u227c y\u27e7 \u27f9 y \u227c x\n         2. \u27e6x \u2260 y; \u00ac x \u227c y; y \u227c x\u27e7 \u27f9 y \u227c x\n         3. \u27e6x \u2260 y; y \u227c x; x \u227c y\u27e7 \u27f9 False *)\n    apply (erule_tac P=\"x \u227c y\" in notE)\n      (* 1. \u27e6x \u2260 y; x \u227c y\u27e7 \u27f9 x \u227c y\n         2. \u27e6x \u2260 y; \u00ac x \u227c y; y \u227c x\u27e7 \u27f9 y \u227c x\n         3. \u27e6x \u2260 y; y \u227c x; x \u227c y\u27e7 \u27f9 False *)\n    apply assumption\n      (* 1. \u27e6x \u2260 y; \u00ac x \u227c y; y \u227c x\u27e7 \u27f9 y \u227c x\n         2. \u27e6x \u2260 y; y \u227c x; x \u227c y\u27e7 \u27f9 False *)\n   apply assumption\n      (* 1. \u27e6x \u2260 y; y \u227c x; x \u227c y\u27e7 \u27f9 False *)\n  apply (drule antisim)\n      (* 1. \u27e6x \u2260 y; x \u227c y\u27e7 \u27f9 x \u227c y\n         2. \u27e6x \u2260 y; x \u227c y; y = x\u27e7 \u27f9 False *)\n   apply assumption\n      (* 1. \u27e6x \u2260 y; x \u227c y; y = x\u27e7 \u27f9 False *)\n  apply (erule notE)\n      (* 1. \u27e6x \u227c y; y = x\u27e7 \u27f9 x = y *)\n  apply (erule sym)\n      (* *)\n  done\n\n(* Demostraci\u00f3n autom\u00e1tica *)\nlemma \"x \u227a y \u2228 x = y \u2228 y \u227a x\"\n  using antisim lineal menor_def by auto\n\nend\n\nsection {* Teor\u00eda de \u00f3rdenes mediante \u00e1mbitos (\"Locales\") *}\n\ntext {*\n  Un orden es una estructura con una relaci\u00f3n reflexiva, transitiva y\n  antisim\u00e9trica. \n*}\n\nlocale Orden =\n  fixes menor_ig :: \"'a \u21d2 'a \u21d2 bool\"  (infix \"\u2291\" 50)\n  assumes refl:    \"x \u2291 x\"\n      and trans:   \"\u27e6x \u2291 y; y \u2291 z\u27e7 \u27f9 x \u2291 z\"\n      and antisim: \"\u27e6x \u2291 y; y \u2291 x\u27e7 \u27f9 x = y\"\n\ntext {*\n    Los teoremas se diferencian por el nombre y el \u00e1mbito. Por ejemplo,\n    refl: ?x \u227c ?x\n    Orden.refl: Orden ?menor_ig \u27f9 ?menor_ig ?x ?x\n    Orden_def: Orden ?menor_ig \u2261\n               (\u2200x. ?menor_ig x x) \u2227\n               (\u2200x y z. ?menor_ig x y \u27f6 ?menor_ig y z \u27f6 ?menor_ig x z) \u2227\n               (\u2200x y. ?menor_ig x y \u27f6 ?menor_ig y x \u27f6 x = y)\n*}\n\nthm refl\nthm Orden.refl\nthm Orden_def\n\ntext {*\n  Un orden lineal es un orden en el que todos los pares de elementos son \n  comparables. \n*}\n\nlocale OrdenLineal = Orden +\n  assumes lineal: \"x \u2291 y \u2228 y \u2291 x\"\n\ntext {*\n  Los boooleanos est\u00e1 ordenados con el condicional.\n*}\n\ninterpretation Orden_imp: Orden \"\u03bbx y. x \u27f6 y\"\nproof\n  fix P show \"P \u27f6 P\" by simp\nnext\n  fix P Q R show \"P \u27f6 Q \u27f9 Q \u27f6 R \u27f9 P \u27f6 R\" by simp\nnext\n  fix P Q show \"P \u27f6 Q \u27f9 Q \u27f6 P \u27f9 P = Q\" by blast\nqed\n\ntext {*\n  Los naturales con la relaci\u00f3n de divisibilidad es un conjunto ordenado.\n*}\n\ninterpretation Orden_dvd: Orden \"(dvd) :: nat \u21d2 nat \u21d2 bool\"\nproof \n  fix x :: nat\n  show \"x dvd x\" by simp\nnext\n  fix x y z :: nat\n  show \"\u27e6x dvd y; y dvd z\u27e7 \u27f9 x dvd z\" by auto \nnext\n  fix x y :: nat\n  show \"\u27e6x dvd y; y dvd x\u27e7 \u27f9 x = y\" by auto\nqed\n\ntext {*\n  \u00c1mbito de las funciones mon\u00f3tonas (ver la p\u00e1gina 12 del tutorial de\n  locales). \n*}\n\nlocale Mono =\n  le1: Orden le1 +\n  le2: Orden le2 \n    for le1 (infix \"\u2291\u21e91\" 50) and le2 (infix \"\u2291\u21e92\" 50) +\n  fixes f :: \"'a \u21d2 'b\"\n  assumes mono: \"x \u2291\u21e91 y \u27f9 f(x) \u2291\u21e92 f(y)\"\n\ntext {*\n  Si f es mon\u00f3tona, x \u2291_1 y e y \u2291_1 z, entonces f(x) \u2291_2 f(z).\n*}\n\nlemma (in Mono) mono_trans: \n  assumes \"x \u2291\u21e91 y\" and \"y \u2291\u21e91 z\" \n  shows \"f(x) \u2291\u21e92 f(z)\"\nproof -\n  have \"x \u2291\u21e91 z\" using assms and le1.trans by blast\n  then show \"f(x) \u2291\u21e92 f(z)\" using mono by simp\nqed\n\ntext {*\n  El teorema generado se llama Mono.mono_trans.\n*}\n\nthm Mono.mono_trans\n\ntext {*\n  En el contexto Mono el nombre es mono_trans.\n*}\n\ncontext Mono \nbegin \nthm mono_trans \nend\n\ntext {*\n  El predicado `ser par' es un operador mon\u00f3tono entre los naturales con la\n  relaci\u00f3n de divisibilidad y los booleanos con el condicional; es decir, \n     x dvd y \u27f9 even x \u27f6 even y\n*}\n\ninterpretation Mono \"(dvd)\" \"(\u27f6)\" \"\u03bbn::nat. 2 dvd n\"\nproof\n  fix x y :: nat \n  show \"x dvd y \u27f9 even x \u27f6 even y\"\n    proof \n      assume \"x dvd y\" and \"even x\"\n      then show \"even y\" \n        using  Rings.comm_monoid_mult_class.dvd_trans by auto\n    qed\nqed\n\nsection {* Semigrupos, monoides y grupos *}\n\nsubsection {* Definici\u00f3n de clases *}\n\ntext {*\n  Un semigrupo es una estructura compuesta por un conjunto A y una\n  operaci\u00f3n binaria en A.\n*}\n\nclass semigrupo =\n  fixes mult :: \"'a \u21d2 'a \u21d2 'a\" (infixl \"\u2297\" 70) \n  assumes asoc: \"(x \u2297 y) \u2297 z = x \u2297 (y \u2297 z )\"\n\nsubsection {* Instanciaci\u00f3n de clases *}\n\ntext {*\n  Los enteros con la suma forman un semigrupo.\n*}\n\ninstantiation int :: semigrupo \nbegin \ndefinition \n  mult_int_def: \"i \u2297 j = i + (j ::int)\" \n\ninstance proof \n  fix i j k :: \"int\" \n  have \"(i + j ) + k = i + (j + k)\" by simp \n  then show \"(i \u2297 j ) \u2297 k = i \u2297 (j \u2297 k)\" unfolding mult_int_def . \nqed \nend \n\ntext {*\n  Los naturales con la suma forman un semigrupo.\n*}\n\ninstantiation nat :: semigrupo \nbegin \nprimrec mult_nat where \n  \"(0::nat) \u2297 n = n\" \n| \"Suc m \u2297 n = Suc (m \u2297 n)\" \n\ninstance proof \n  fix m n q :: \"nat\" \n  show \"m \u2297 n \u2297 q = m \u2297 (n \u2297 q)\" \n    by (induct m) auto\nqed \nend\n\nsubsection {* Instancias recursivas *}\n\ntext {*\n  Si (A,\u2297) y (B,\u2297) son semigrupos, entonces ((A\u00d7B,\u2297), donde el producto\n  se define por \n     (x,y)\u2297(x',y') = (x\u2297x',y\u2297y'),\n  es un semigrupo.\n*}\n \ninstantiation prod :: (semigrupo, semigrupo) semigrupo \nbegin \n\ndefinition \n  mult_prod_def : \"p1 \u2297 p2 = (fst p1 \u2297 fst p2, snd p1 \u2297 snd p2)\" \n\ninstance proof \n  fix p1 p2 p3 :: \"'a::semigrupo \u00d7 'b::semigrupo\" \n  show \"(p1 \u2297 p2) \u2297 p3 = p1 \u2297 (p2 \u2297 p3)\" \n    unfolding mult_prod_def by (simp add: asoc) \nqed \nend\n\nsubsection {* Subclases *}\n\ntext {*\n  Un monoide izquierdo es un semigrupo con elemento neutro por la izquierda. \n*}\n\nclass monoideI = semigrupo + \n  fixes neutro :: \"'a\" (\"\ud835\udfed\") \n  assumes neutroI: \"\ud835\udfed \u2297 x = x\"\n\ntext {*\n  Los naturales y los enteros con la suma forman monoides por la izquierda.\n*}\n\ninstantiation nat and int :: monoideI \nbegin \n\ndefinition \n  neutro_nat_def : \"\ud835\udfed = (0::nat)\" \n\ndefinition \n  neutro_int_def : \"\ud835\udfed = (0::int)\" \n\ninstance proof \n  fix n :: nat \n  show \"\ud835\udfed \u2297 n = n\" unfolding neutro_nat_def by simp\nnext \n  fix k :: int \n  show \"\ud835\udfed \u2297 k = k\" unfolding neutro_int_def mult_int_def by simp \nqed \nend\n\ntext {*\n  El producto de dos monoides por la izquierda es un monoide por la\n  izquierda, donde el neutro es el par formado por los elementos neutros.\n*}\n\ninstantiation prod :: (monoideI , monoideI) monoideI \nbegin \n\ndefinition \n  neutro_prod_def : \"\ud835\udfed = (\ud835\udfed, \ud835\udfed)\" \n\ninstance proof \n  fix p :: \"'a::monoideI \u00d7 'b::monoideI\" \n  show \"\ud835\udfed \u2297 p = p\" \n    unfolding neutro_prod_def mult_prod_def by (simp add: neutroI) \nqed \nend\n\ntext {*\n  Un monoide es un monoide por la izquierda cuyo elemento neutro por la\n  izquierda lo es tambi\u00e9n por la derecha.\n*}\n\nclass monoide = monoideI + \n  assumes neutro: \"x \u2297 \ud835\udfed = x\" \n\ntext {*\n  Los naturales y los enteros con la suma son monoides.\n*}\n\ninstantiation nat and int :: monoide \nbegin \n\ninstance proof \n  fix n :: nat \n  show \"n \u2297 \ud835\udfed = n\" \n    unfolding neutro_nat_def by (induct n) simp_all \nnext \n  fix k :: int \n  show \"k \u2297 \ud835\udfed = k\" \n    unfolding neutro_int_def mult_int_def by simp \nqed\nend\n\ntext {*\n  El producto de dos monoides es un monoide.\n*}\n\ninstantiation prod :: (monoide, monoide) monoide \nbegin \n\ninstance proof \n  fix p :: \"'a::monoide \u00d7 'b::monoide\" \n  show \"p \u2297 \ud835\udfed = p\" \n    unfolding neutro_prod_def mult_prod_def by (simp add: neutro) \nqed \nend\n\ntext {*\n  Un grupo es un monoide por la izquierda tal que todo elemento posee un\n  inverso por la izquierda.\n*}\n\nclass grupo2 = monoideI + \n  fixes inverso :: \"'a \u21d2 'a\" (\"(_\u21e7-\u21e71)\" [1000] 999)\n  assumes inversoI: \"x\u21e7-\u21e71 \u2297 x = \ud835\udfed\" \n\ntext {*\n  Los enteros con la suma forman un grupo.\n*}\n\ninstantiation int :: grupo2 \nbegin \n\ndefinition\n  inverso_int_def: \"i\u21e7-\u21e71 = -(i::int)\"\n\ninstance proof \n  fix i :: \"int\" \n  have \"-i + i = 0\" by simp \n  then show \"i\u21e7-\u21e71 \u2297 i = \ud835\udfed\" \n    unfolding mult_int_def neutro_int_def inverso_int_def . \nqed \nend\n\nsubsection {* Razonamiento abstracto *}\n\ntext {*\n  En los grupos se verifica la propiedad cancelativa por la izquierda, i.e.\n     x \u2297 y = x \u2297 z \u27f7 y = z\n*}\n\nlemma (in grupo2) cancelativa_izq: \"x \u2297 y = x \u2297 z \u27f7 y = z\" \nproof \n  assume \"x \u2297 y = x \u2297 z\"\n  hence \"x\u21e7-\u21e71 \u2297 (x \u2297 y) = x\u21e7-\u21e71 \u2297 (x \u2297 z)\" by simp \n  hence \"(x\u21e7-\u21e71 \u2297 x) \u2297 y = (x\u21e7-\u21e71 \u2297 x) \u2297 z\" using asoc by simp \n  then show \"y = z\" using neutroI and inversoI by simp\nnext \n  assume \"y = z\" \n  then show \"x \u2297 y = x \u2297 z\" by simp\nqed\n\nthm grupo2.cancelativa_izq\n\ntext {*\n  Se genera el teorema grupo.cancelativa_izq\n     class.grupo2 ?mult ?neutro ?inverso \u27f9 \n     (?mult ?x ?y = ?mult ?x ?z) = (?y = ?z)\n\n  El teorema se aplica autom\u00e1ticamente a todas las instancias de la clase\n  grupo. Por ejemplo, a los enteros.\n*}\n\nsubsection {* Definiciones derivadas *}\n\ntext {*\n  En los monoides se define la potencia natural por\n  \u00b7 x^0     = 1\n  \u00b7 x^{n+1} = x*x^n\n*}\n\nfun (in monoide) potencia_nat :: \"nat \u21d2 'a \u21d2 'a\" where \n  \"potencia_nat 0 x       = \ud835\udfed\"  \n| \"potencia_nat (Suc n) x = x \u2297 potencia_nat n x\"\n\nsubsection {* Analog\u00eda entre clases y functores *}\n\ntext {*\n  Las listas con la operaci\u00f3n de concatenaci\u00f3n y la lista vac\u00eda como elemento\n  neutro forman un monoide.\n*}\n\ninterpretation list_monoide: monoide \"append\" \"[]\"\nproof \n  show \"\u22c0x y z. (x @ y) @ z = x @ (y @ z)\" by simp\nnext\n  show \"\u22c0x. [] @ x = x\" by simp\nnext\n  show \"\u22c0x. x @ [] = x\" by simp\nqed\n\ntext {*\n  Se pueden aplicar propiedades de los monides a las listas. Por ejemplo,\n*}\n\nlemma \"append [] xs = xs\"\n  by simp\n\ntext {*\n  (repite n xs) es la lista obtenida concatenando n veces la lista xs. \n*}\n\nfun repite :: \"nat \u21d2 'a list \u21d2 'a list\" where \n  \"repite 0 _        = []\"\n| \"repite (Suc n) xs = xs @ repite n xs\"\n\ntext {*\n  Las listas con la operaci\u00f3n de concatenaci\u00f3n y la lista vac\u00eda como elemento\n  neutro forman un monoide. Adem\u00e1s, la potencia natural se intepreta como\n  repite. \n*}\n\ninterpretation list_monoide: monoide \"append\" \"[]\" rewrites\n  \"monoide.potencia_nat append [] = repite\" \nproof -\n  interpret monoide \"append\" \"[]\" .. \n  show \"monoide.potencia_nat append [] = repite\" \n  proof \n    fix n \n    show \"monoide.potencia_nat append [] n = repite n\"\n      by (induct n) auto \n  qed \nqed intro_locales\n\nsubsection {* Relaciones de subclase adicionales *}\n\ntext {*\n  Los grupos son monoides.\n*}\n\nsubclass (in grupo2) monoide \nproof \n  fix x \n  have \"x\u21e7-\u21e71 \u2297 (x \u2297 \ud835\udfed) = x\u21e7-\u21e71 \u2297 (x \u2297 (x\u21e7-\u21e71 \u2297 x))\" using inversoI by simp\n  also have \"\u2026 = (x\u21e7-\u21e71 \u2297 x) \u2297 (x\u21e7-\u21e71 \u2297 x)\" using asoc [symmetric] by simp\n  also have \"\u2026 = \ud835\udfed \u2297 (x\u21e7-\u21e71 \u2297 x)\" using inversoI by simp\n  also have \"\u2026 = x\u21e7-\u21e71 \u2297 x\" using neutroI by simp\n  finally have \"x\u21e7-\u21e71 \u2297 (x \u2297 \ud835\udfed) = x\u21e7-\u21e71 \u2297 x\" . \n  then show \"x \u2297 \ud835\udfed = x\" using cancelativa_izq by simp\nqed\n\ntext {*\n  La potencia entera en los grupos se define a partir de la potencia natural\n  como sigue:\n  \u00b7 x^k = x^k si k \u2265 0\n  \u00b7 x^k = (x^{-k})^{-1}, en caso contrario.\n*}\n\ndefinition (in grupo2) potencia_entera :: \"int \u21d2 'a \u21d2 'a\" where \n  \"potencia_entera k x = \n   (if k >= 0 \n    then potencia_nat (nat k) x \n    else (potencia_nat (nat (- k)) x)\u21e7-\u21e71)\"\n\nsection {* Bibliograf\u00eda *}\ntext {* \n  + \"Haskell-style type classes with Isabelle\/Isar\" ~ F. Haftmann.\n    http:\/\/bit.ly\/2E55pAJ\n  + \"Tutorial to locales and locale interpretation\" ~ C. Ballarin.\n    http:\/\/bit.ly\/2E3ozXB  \n*}\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso de L\u00f3gica matem\u00e1tica y fundamentos se ha estudiado c\u00f3mo definir desarrollar en Isabelle\/HOL teor\u00edas axiom\u00e1ticas como las de monoides, semigrupos, grupos, \u00f3rdenes y \u00f3rdenes lineales. La clase se ha basado en la siguiente teor\u00eda Isabelle chapter {* T11: Desarrollo de teor\u00edas formalizadas *} theory T11_Desarrollo_de_teorias_formalizadas imports Main begin&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[268],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6698"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=6698"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6698\/revisions"}],"predecessor-version":[{"id":6699,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6698\/revisions\/6699"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6698"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6698"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6698"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}