(* Создано 2014-03-01 или 2014-03-02 *) (* Этот файл является моим знанием *) theory "theory-[hol-based-theory]" imports HOL (* Приблизительно: HOL - это Pure (т. е. только металогика) плюс \, = и т. д. *) begin (* class - это тип типа. Это как классы типов в Haskell. Например, есть тип "действительные числа", он принадлежит классам "поле", "упорядоченное множество". Локаль - это почти тоже самое, что и класс, но со следующими отличиями: * Локаль может описывать свойства сразу несколько типов. Т. е. например, мы можем создать локаль "векторное пространство" и в ней описать, что значит "тип 'a является векторным пространством над полем 'b" (при описании класса типа или локали тип, который мы описываем, заменяется переменной вида 'a) * После определения класса можно в последующем ссылаться на этот класс и говорить "a::b", что означает "тип a принадлежит классу b" * После определения класса все определённые константы (функции тоже являются константами; это как в математической логике, только наоборот; в мат. логике можно константы сигнатуры считать функциями от нуля переменных, в Isabelle функции - это константы типа, скажем, 'a \ 'a) приобретают тип, скажем, 'a::c, где c - нужный класс. Т. е. если определена константа e, то e::('a::c). Далее можно использовать эти константы, и Isabelle будет знать их тип. Можно формулировать теоремы про эти константы, не указывая, что мы находимся в контексте этого класса. Это как классы типов в Haskell: мы определили класс и мы определили функции. Глобально. И теперь этим везде можно пользоваться. Локаль - это локаль. Она локальна. Всё, определённое в ней, определено только в ней Я решил для себя, что для простоты не буду пользоваться реальными типами и классами, а буду пользоваться только локалями. *) section {* Определим группы тремя способами для демонстрации этих способов *} subsection {* axiomatization *} typedecl tg1 (* test group 1 *) axiomatization tg1e :: tg1 and tg1op :: "[tg1, tg1] \ tg1" (infixl "\" 70) and tg1i :: "tg1 \ tg1" where tg1aa: "\ a . \ b . \ c . (a \ b) \ c = a \ (b \ c)" and tg1ae: "\ a . (tg1e \ a = a \ a \ tg1e = a)" and tg1ai: "\ a . (a \ tg1i a = tg1e \ tg1i a \ a = tg1e)" lemma "a \ tg1e = a" using tg1ae by auto subsection {* class *} (* По всей видимости, class - самый подходящий способ для описания структур с перегруженными операторами. Например, есть стандартный класс times для структур с операцией times ( * ) *) class tg2 = fixes tg2e :: "'a" fixes tg2op :: "['a, 'a] \ 'a" fixes tg2i :: "'a \ 'a" assumes tg2aa: "\ a . \ b . \ c . tg2op (tg2op a b) c = tg2op a (tg2op b c)" assumes tg2ae: "\ a . (tg2op tg2e a = a \ tg2op a tg2e = a)" assumes tg2ai: "\ a . (tg2op a (tg2i a) = tg2e \ tg2op (tg2i a) a = tg2e)" (* begin *) (* begin и end можно не ставить. Видимо, потому что tg2op уже говорит о том, что мы говорим про класс tg2. Но тогда нужен blast *) lemma "\ a . tg2op a tg2e = a" using tg2ae by blast (* end *) subsection {* locale *} locale tg3 = fixes tg3e :: "'a" fixes tg3op :: "['a, 'a] \ 'a" fixes tg3i :: "'a \ 'a" assumes tg3aa: "\ a . \ b . \ c . tg3op (tg3op a b) c = tg3op a (tg3op b c)" assumes tg3ae: "\ a . (tg3op tg3e a = a \ tg3op a tg3e = a)" assumes tg3ai: "\ a . (tg3op a (tg3i a) = tg3e \ tg3op (tg3i a) a = tg3e)" begin (* А вот здесь обязательно нужен begin (т. е. лемма должна быть внутри контекста локали) *) lemma "\ a . tg3op a tg3e = a" using tg3ae by auto end section {* Алгебра *} locale one = fixes times :: "['a, 'a] \ 'a" (infixl "*" 70) fixes one :: 'a ("1") assumes neutral: "a * 1 = a \ 1 * a = a" locale comm_struct = fixes times :: "['a, 'a] \ 'a" (infixl "*" 70) assumes commute: "a * b = b * a" locale semigroup = fixes times :: "['a, 'a] \ 'a" (infixl "*" 70) assumes assoc: "(a * b) * c = a * (b * c)" (* Определяем моноид, т. к. поле - это моноид по умножению, но не группа, из-за нуля *) locale monoid = semigroup + one begin (* У одного элемента не может быть двух обратных. blast не справляется :( *) theorem assumes "a * b = 1 \ b * a = 1 \ a * c = 1 \ c * a = 1" shows "b = c" proof - have "(b * a) * c = 1 * c" using assms by auto (* hence = from this have *) hence "b * (a * c) = c" using assoc and neutral by auto (* thus = from this show *) (* show аннигилирует сейчас доказываемый факт с целью *) thus "b = c" using assms and neutral by auto qed end locale group = monoid + fixes inverse :: "'a \ 'a" assumes inverse_ax: "a * inverse a = 1 \ inverse a * a = 1" begin theorem about_inv: assumes "b * a = a \ a * b = a" shows "b = 1" proof - { assume "b * a = a" hence "(b * a) * inverse a = a * inverse a" by auto hence "b * (a * inverse a) = a * inverse a" using assoc by auto hence "b * (a * inverse a) = 1" using inverse_ax by auto hence "b = 1" using inverse_ax and neutral by auto } moreover { assume "a * b = a" hence "inverse a * (a * b) = inverse a * a" by auto hence "(inverse a * a) * b = inverse a * a" using assoc by auto hence "(inverse a * a) * b = 1" using inverse_ax by auto hence "b = 1" using inverse_ax and neutral by auto } ultimately show ?thesis using assms by auto qed end locale abel_group = group + comm_struct locale add_group = abel_group plus zero uminus for plus :: "['a, 'a] \ 'a" (infixl "+" 65) and zero :: 'a ("0") and uminus :: "'a \ 'a" ("- _" [81] 80) locale ring = add!: add_group + fixes times :: "['a, 'a] \ 'a" (infixl "*" 70) assumes dist: "x * (a + b) = x * a + x * b \ (a + b) * x = a * x + b * x" begin theorem times0: "a * 0 = 0" and "0 * a = 0" proof - have "a * (0 + 0) = a * 0 + a * 0" using dist by auto hence "a * 0 = a * 0 + a * 0" using add.neutral by auto hence "a * 0 + a * 0 = a * 0" by auto thus "a * 0 = 0" using add.about_inv by auto have "(0 + 0) * a = 0 * a + 0 * a" using dist by auto hence "0 * a = 0 * a + 0 * a" using add.neutral by auto hence "0 * a + 0 * a = 0 * a" by auto thus "0 * a = 0" using add.about_inv by auto qed end locale ring1 = ring + mult!: one locale assoc_ring = ring + mult!: semigroup locale assoc_ring1 = ring1 + mult!: semigroup locale comm_ring = ring + mult!: comm_struct locale comm_ring1 = ring1 + mult!: comm_struct locale assoc_comm_ring = assoc_ring + mult!: comm_struct locale assoc_comm_ring1 = assoc_ring1 + mult!: comm_struct sublocale assoc_ring1 < assoc_ring by unfold_locales sublocale comm_ring1 < comm_ring by unfold_locales sublocale assoc_comm_ring < comm_ring by unfold_locales sublocale assoc_comm_ring1 < comm_ring1 by unfold_locales sublocale assoc_comm_ring1 < assoc_comm_ring by unfold_locales sublocale assoc_ring1 < mult!: monoid by unfold_locales locale field = assoc_comm_ring1 + assumes mult_inverse: "\ a . (a \ 0 \ (\ b . a * b = 1 \ b * a = 1))" and not_eq01: "0 \ 1" begin (* Нет делителей нуля *) theorem no_0_divisors: assumes "a * b = 0" shows "a = 0 \ b = 0" proof - { assume "a \ 0" then obtain c where "c * a = 1" using mult_inverse by auto moreover have "c * (a * b) = c * 0" using assms by auto ultimately have "1 * b = 0" using mult.assoc and times0 by auto hence "b = 0" using mult.neutral by auto } thus ?thesis by auto qed end (* Все объявленные в локали константы (включая функции, но не типы) являются её параметрами. При создании локали на основе существующих можно к этим существующим локалям указывать параметры. Указывать их нужно в том порядке, в котором они в этой существующей локали объявлены. Более подробно: сперва идут (рекурсивно) все параметры, объявленные в локалях-предках, затем объявленные в for и assume в том порядке, в котором они объявлены. Как наследовать локали: locale parent = fixes par1 :: 'a fixes par2 :: 'a locale child = parent _ par3 + parent par1 par3 for par3 :: 'a Нужно указать после имени родительской локали параметры к ней, а затем обязательно их объявить в for, как это сделано с par3. Имя параметра может не совпадать с оригинальным (как здесь с par2 и par3). Потом можно использовать этот параметр снова, но объявить его всё равно нужно только один раз. Можно поставить вместо параметра _, тогда берётся уже существующий параметр с его именем. В этом случае объявлять его уже нельзя, и затем его можно использовать в качестве параметра снова, но опять-таки, объявлять его по-прежнему нельзя, как это сделано с par1. parent эквивалентно parent _ _. Параметры, которые нужно объявить в for, объявить нужно. Которые нельзя - нельзя. Т. е. список параметров, которые нужно объявить в for, определён однозначно.*) (* 'v - vector, 's - scalar *) locale vector_space = scalar!: field _ _ _ _ one + vadd!: add_group vplus vzero vuminus for one :: 's ("1") and vplus :: "['v, 'v] \ 'v" (infixl "[+]" 65) and vzero :: 'v ("[0]") and vuminus :: "'v \ 'v" ("[-] _" [81] 80) + fixes svtimes :: "['s, 'v] \ 'v" (infixl "[*]" 70) assumes svdist: "(k + l)[*]a = k[*]a [+] l[*]a \ k[*](a [+] b) = k[*]a [+] k[*]b" assumes svone: "1[*]a = a" assumes ssvassoc: "(k * l)[*]a = k[*](l[*]a)" end