{"id":7190,"date":"2020-05-21T12:54:40","date_gmt":"2020-05-21T10:54:40","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7190"},"modified":"2020-05-21T12:54:40","modified_gmt":"2020-05-21T10:54:40","slug":"lmf2019-desarrollo-de-teorias-formalizadas-con-isabelle-hol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2019-desarrollo-de-teorias-formalizadas-con-isabelle-hol\/","title":{"rendered":"LMF2019: 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-19\">L\u00f3gica matem\u00e1tica y fundamentos<\/a> se ha estudiado c\u00f3mo desarrollar en Isabelle\/HOL teor\u00edas axiom\u00e1ticas usando entornos locales (&#8220;locales&#8221;) y clases de tipos (&#8220;class&#8221;). Se ha aplicado al desarrollo de las teor\u00edas de grupos y a las de \u00f3rdenes.  videoconferencia.<\/p>\n<p>La clase se ha dado mediante videoconferencia y los v\u00eddeos correspondientes son:<\/p>\n<ul>\n<li>Primera parte: <\/li>\n<\/ul>\n<p><iframe loading=\"lazy\" width=\"560\" height=\"315\" src=\"https:\/\/www.youtube.com\/embed\/LtiWoXdjiWs\" frameborder=\"0\" allow=\"accelerometer; autoplay; encrypted-media; gyroscope; picture-in-picture\" allowfullscreen><\/iframe><\/p>\n<ul>\n<li>Segunda parte:<\/li>\n<\/ul>\n<p><iframe loading=\"lazy\" width=\"560\" height=\"315\" src=\"https:\/\/www.youtube.com\/embed\/iUSfISnTfbM\" frameborder=\"0\" allow=\"accelerometer; autoplay; encrypted-media; gyroscope; picture-in-picture\" allowfullscreen><\/iframe><\/p>\n<p>La teor\u00eda con los ejemplos presentados en la clase es la siguiente:<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nchapter \u2039Desarrollo de teor\u00edas formalizadas\u203a\n\ntheory T11_Desarrollo_de_teorias_formalizadas\nimports Main\nbegin\n\nsection \u2039Desarrollo de la teor\u00eda de grupos\u203a\n\ntext \u2039El objetivo de este tema es mostrar c\u00f3mo se puede trabajar en\n  estructuras algebraicas por medio de locales. \n\n  Se usar\u00e1 como ejemplo la teor\u00eda de grupos.\u203a\n\ntext \u2039Ejemplo 1. Un grupo es una estructura (G,\u00b7,\ud835\udfed,^) tal que \n  * G es un conjunto, \n  * \u00b7 es una operaci\u00f3n binaria en G, \n  * \ud835\udfed es un elemento de G y \n  * ^ es una funci\u00f3n de G en G \n  tales que se cumplen las siguientes 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\n  Definir el entorno axiom\u00e1tico de los grupos.\u203a\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 \u2039Notas 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 pulsando 2 veces en ^.\u203a\n\ntext \u2039A continuaci\u00f3n se crea un contexto en el que se supone la \n  notaci\u00f3n y axiomas de grupos. \n\n  En el contexto se demuestran propiedades de los grupos.\u203a\n\ncontext grupo\nbegin\n\nthm neutro_i\n\ntext \u2039Ejemplo 2. En los grupos, x^ tambi\u00e9n es el inverso de x por la\n  derecha; es decir \n     x \u22c5 x^ = \ud835\udfed\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica (obtenida con Sledgehammer) es\u203a\nlemma \"x \u22c5 x^ = \ud835\udfed\"\n  (* sledgehammer *) \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^)\" \n    by (simp only: neutro_i)\n  also have \"\u2026 = (\ud835\udfed \u22c5 x) \u22c5 x^\" \n    by (simp only: asociativa)\n  also have \"\u2026 = (((x^)^ \u22c5 x^) \u22c5 x) \u22c5 x^\" \n    by (simp only: inverso_i)\n  also have \"\u2026 = ((x^)^ \u22c5 (x^ \u22c5 x)) \u22c5 x^\" \n    by (simp only: asociativa)\n  also have \"\u2026 = ((x^)^ \u22c5 \ud835\udfed) \u22c5 x^\" \n    by (simp only: inverso_i)\n  also have \"\u2026 = (x^)^ \u22c5 (\ud835\udfed \u22c5 x^)\" \n    by (simp only: asociativa)\n  also have \"\u2026 = (x^)^ \u22c5 x^\" \n    by (simp only: neutro_i)\n  also have \"\u2026 = \ud835\udfed\" \n    by (simp only: inverso_i)\n  finally show ?thesis \n    by this\nqed\n\ntext \u2039Ejemplo 2. En los grupos, \ud835\udfed tambi\u00e9n es el neutro por la derecha; \n  es decir \n     x \u22c5 \ud835\udfed = x\u203a\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)\" \n    by (simp only: inverso_i)\n  also have \"\u2026 = (x \u22c5 x^) \u22c5 x\"\n    by (simp only: asociativa)\n  also have \"\u2026 = \ud835\udfed \u22c5 x\" \n    by (simp only: inverso_d)\n  also have \"\u2026 = x\" \n    by (simp only: neutro_i)\n  finally show \"x \u22c5 \ud835\udfed = x\" \n    by this\nqed \n\ntext \u2039Ejemplo 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\u203a\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  then have \"x^ \u22c5 (x \u22c5 y) = x^ \u22c5 (x \u22c5 z)\"\n    (* thm arg_cong\n           arg_cong[of \"x \u22c5 y\"]\n           arg_cong[of \"x \u22c5 y\" \"x \u22c5 z\"] *)\n    by (simp only: arg_cong[of \"x \u22c5 y\" \"x \u22c5 z\"])\n  then have \"(x^ \u22c5 x) \u22c5 y = (x^ \u22c5 x) \u22c5 z\" \n    by (simp only: asociativa)\n  then have \"\ud835\udfed \u22c5 y = \ud835\udfed \u22c5 z\" \n    by (simp only: inverso_i)\n  thus \"y = z\" \n    by (simp only: neutro_i)\nnext\n  assume \"y = z\"\n  then show \"x \u22c5 y = x \u22c5 z\" \n    (* thm arg_cong \n           arg_cong [of \"y\" \"z\"]\n           arg_cong [of _ \"z\"] *)\n    by (simp only: arg_cong [of \"y\" \"z\"])\nqed\n\ntext \u2039Ejemplo 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.\u203a\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^\" \n    by (simp only: inverso_d)\n  also have \"... = (e \u22c5 x) \u22c5 x^\" \n    (* thm assms\n           assms[symmetric] *)\n    using assms [symmetric]\n    (* thm arg_cong\n           arg_cong [of \"x\" \"e \u22c5 x\" \"\u03bby. y \u22c5 x^\"] *)\n    by (rule arg_cong [of \"x\" \"e \u22c5 x\" \"\u03bby. y \u22c5 x^\"])\n  also have \"... = e \u22c5 (x \u22c5 x^)\" \n    by (simp only: asociativa)\n  also have \"... = e \u22c5 \ud835\udfed\" \n    by (simp only: inverso_d)\n  also have \"... = e\" \n    by (simp only: neutro_d)\n  finally show ?thesis \n    by this\nqed \n\ntext \u2039Ejemplo 5. En los grupos, los inversos por la izquierda son \n  \u00fanicos; es decir, si x' es un elemento tal que x' \u22c5 x = \ud835\udfed, entonces \n  x^ = x'.\u203a\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^\" \n    by (simp only: neutro_i)\n  also have \"... = (x' \u22c5 x) \u22c5 x^\" \n    using assms [symmetric] \n    by (simp only: arg_cong [of \"\ud835\udfed\" \"x' \u22c5 x\"])\n  also have \"... = x' \u22c5 (x \u22c5 x^)\" \n    by (simp only: asociativa)\n  also have \"... = x' \u22c5 \ud835\udfed\" \n    by (simp only: inverso_d)\n  also have \"... = x'\" \n    by (simp only: neutro_d)\n  finally show ?thesis \n    by this\nqed\n\ntext \u2039Ejemplo 6. En los grupos, es inverso de un producto es el \n  producto de los inversos cambiados de orden; es decir,\n     (x \u22c5 y)^ = y^ \u22c5 x^\u203a\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\" \n      by (simp only: inverso_i)\n    also have \"... = y^ \u22c5 y\" \n      by (simp only: neutro_d)\n    also have \"... = \ud835\udfed\" \n      by (simp only: inverso_i)\n    finally show ?thesis \n      by this\n  qed\nqed\n\ntext \u2039Ejemplo 7. En los grupos, el inverso del inverso es el propio\n  elemento; es decir, \n     (x^)^ = x\u203a\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\" \n    by (simp only: inverso_d)\nqed\n\ntext \u2039Ejemplo 8. En los grupos, la funci\u00f3n inversa es inyectiva; es \n  decir, si x e y tienen los mismos inversos, entonces son iguales.\u203a\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^)^\" \n    using assms \n    by (simp only: arg_cong [of \"x^\" \"y^\"])\n  then show \"x = y\" \n    by (simp only: inverso_inverso)\nqed\n\nthm neutro_i\nthm inversa_inyectiva\nend\n\nsection \u2039Teor\u00edas de \u00f3rdenes mediante clases\u203a\n\ntext \u2039El 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\u203a\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 \u2039Ha generado los teoremas correspondientes a los axiomas. Pueden \n  consultarse mediante thm como se muestra a continuaci\u00f3n.\u203a\n\nthm trans\n\ntext \u2039Se inicia el contexto orden en el que se van a realizar \n  definiciones y demostraciones.\u203a\n\ncontext orden\nbegin\n\ntext \u2039x es menor que y si x es menor o igual que y y no es menos o igual \n  que x.\u203a\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\nthm menor_def\n\ntext \u2039La relaci\u00f3n menor es irreflexiva.\u203a\n\nlemma irrefl: \"\u00ac x \u227a x\"\n  by (simp add: menor_def)\n\ntext \u2039La relaci\u00f3n menor es transitiva.\u203a\n\n(* Demostraci\u00f3n declarativa *)\nlemma \n  assumes \"x \u227a y\" \n          \"y \u227a z\"\n  shows   \"x \u227a z\"\nproof -\n  have 1: \"x \u227c y \u2227 \u00ac y \u227c x\"\n    using assms(1) by (simp add: menor_def)\n  have 2: \"y \u227c z \u2227 \u00ac z \u227c y\"\n    using assms(2) by (simp add: menor_def)\n  have \"x \u227c z\"\n  proof -\n    have \"x \u227c y\"\n      using 1 by (rule conjunct1)\n    moreover have \"y \u227c z\"\n      using 2 by (rule conjunct1)\n    ultimately show \"x \u227c z\"\n      by (rule trans)\n  qed\n  moreover have \"\u00ac z \u227c x\"\n  proof (rule notI)\n    assume \"z \u227c x\"\n    moreover have \"x \u227c y\"\n      using 1 by (rule conjunct1)\n    ultimately have \"z \u227c y\"\n      by (rule trans)\n    have \"\u00ac z \u227c y\"\n      using 2 by (rule conjunct2)\n    then show False \n      using \u2039z \u227c y\u203a by (rule notE)\n  qed\n  have \"x \u227c z \u2227 \u00ac z \u227c x\"\n    using \u2039x \u227c z\u203a \u2039\u00ac z \u227c x\u203a by (rule conjI)\n  then show \"x \u227a z\"\n    by (simp add: menor_def)\nqed \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 \u2039La relaci\u00f3n menor es asim\u00e9trica; es decir, si x \u227a y e y \u227a x, \n  entonces se verifica cualquier propiedad P. \u203a\n\nlemma asimetrica: \"x \u227a y \u27f9 y \u227a x \u27f9 P\"\n  by (simp add: menor_def)\n\nend\n\nsubsection \u2039Subclase\u203a\n\ntext \u2039Un orden lineal es un orden en que cada par de elementos son \n  comparables.\u203a\n\nclass ordenLineal = orden +\n  assumes lineal: \"x \u227c y \u2228 y \u227c x\"\nbegin\n\ntext \u2039En los \u00f3rdenes lineales se tiene que x \u227a y \u2228 x = y \u2228 y \u227a x.\u203a\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\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\nend\n\nsection \u2039Teor\u00eda de \u00f3rdenes mediante \u00e1mbitos (\"Locales\")\u203a\n\ntext \u2039Un orden es una estructura con una relaci\u00f3n reflexiva, \n  transitiva y antisim\u00e9trica.\u203a\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 \u2039Los teoremas se diferencian por el nombre y el \u00e1mbito. \n  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\u203a\n\nthm refl\nthm Orden.refl\nthm Orden_def\n\ntext \u2039Un orden lineal es un orden en el que todos los pares de elementos \n  son comparables.\u203a\n\nlocale OrdenLineal = Orden +\n  assumes lineal: \"x \u2291 y \u2228 y \u2291 x\"\n\ntext \u2039Los boooleanos est\u00e1 ordenados con el condicional.\u203a\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 \u2039Los naturales con la relaci\u00f3n de divisibilidad es un conjunto \n  ordenado.\u203a\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\"\n    using dvd_trans by blast \nnext\n  fix x y :: nat\n  show \"\u27e6x dvd y; y dvd x\u27e7 \u27f9 x = y\"\n    by (simp add: dvd_antisym) \nqed\n\nsection \u2039Bibliograf\u00eda\u203a\n\ntext \u2039\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\u203a\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 desarrollar en Isabelle\/HOL teor\u00edas axiom\u00e1ticas usando entornos locales (&#8220;locales&#8221;) y clases de tipos (&#8220;class&#8221;). Se ha aplicado al desarrollo de las teor\u00edas de grupos y a las de \u00f3rdenes. videoconferencia. La clase se ha dado mediante videoconferencia y los&#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":[334],"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\/7190"}],"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=7190"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7190\/revisions"}],"predecessor-version":[{"id":7191,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7190\/revisions\/7191"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7190"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7190"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7190"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}