Up to index of Isabelle/HOL/HOL-Complex/transnumber
theory TransNumberAxclassheader {* Transarithmetic: Axiomatic Classes *} theory TransNumberAxclass imports Main Real begin subsection{*New constants: xor, infinity, sgn *} text{* Note: This "list" xor is different from binary xor when there are three or more arguments. *} consts xor :: "bool list => bool" primrec "xor [] = False" "xor (a # x) = ((xor x ∧ ¬ a) | (¬ (list_ex id x) ∧ a))"; lemma xor_singleton: "xor [b] = b"; by simp; lemma xor_pair: "xor [a,b] = (a ≠ b)"; by auto; lemma xor_triple: "xor [a,b,c] = ((a ∧ ¬ b ∧ ¬c) ∨ (¬ a ∧ b ∧ ¬c) ∨ (¬ a ∧ ¬ b ∧ c))"; by auto; axclass infinity < type text{* Note: there is no separate constant minus-infinity *} consts infinity :: "'a::infinity" ("∞" 100) axclass nullity < type consts nullity:: "'a ::nullity" ("Φ") axclass sgn < zero,one,minus, ord consts sgn :: "'a :: sgn => 'a" axclass trans_sgn < sgn, nullity trans_sgn: "sgn a = (if 0 < a then 1 else if 0 = a then 0 else if a < 0 then - 1 else (* a = Φ *) Φ)" subsection{* Axiomatic class trans\_add *} axclass trans_add < zero, infinity, nullity, plus, minus A1: "a + (b + c) = (a + b) + c" (* add assoc *) A2: "a + b = b + a" (* add commute *) A3: "0 + a = a" (* add null *) A4: "Φ + a = Φ" (* add nullity *) A5: "[| a ≠ -∞; a ≠ Φ |] ==> ∞ + a = ∞ " (* add infinity *) A6: "a - b = a + (-b)" (* subtraction *) A7: "-(-a) = a" (* uminus\_uminus *) A8: "[| a ≠ ∞; a ≠ -∞; a ≠ Φ |] ==> a - a = 0" (* add inverse *) A9: " -Φ = Φ" (* uminus nullity *) A10: "[| a ≠ ∞; a ≠ Φ |] ==> a - ∞ = - ∞ " (* real substract infinity, needed??? *) A11: "∞ - ∞ = Φ " (* infinity minus infinity *) instance trans_add ⊆ comm_monoid_add apply (intro_classes) apply (rule A1 [THEN sym]); by ( rule A2, rule A3); subsection {* Axiomatic class trans\_mult (Axioms A12-A28) *} axclass trans_mult < trans_add, trans_sgn, one, times, inverse, ord A12: "a * (b * c)= (a * b) * c " (* mult assoc *) A13: "a * b = b * a" (* mult commute *) A14: "1 * a = a" (* one mult *) A15: "Φ * a = Φ" (* nullity mult *) A16: "∞ * 0 = Φ" (* infinity mult zero *) A17: " a / b = a * inverse b" (* division defintion *) A18: "[| a ≠ 0; a ≠ ∞; a ≠ -∞; a ≠ Φ |] ==> a / a = 1" (* mult inverse *) A19: "a ≠ -∞ ==> inverse (inverse a) = a" (* inverse of inverse *) A20: "inverse 0 = ∞" (* inverse of zero !!! *) A21: "inverse (-∞) = 0" (* inverse of minus infinity *) A22: "inverse Φ = Φ" (* inverse of nullity *) A23: "(∞ * a = ∞) = (0 < a )" (* positive *) A24: "(∞ * a = -∞) = (a < 0)" (* negative *) A25: "0 < ∞" (* infinity is positive *) A26: " (0 < a - b) = (b < a) " (* ordering positive *) A27: "(a > b) = (b < a)" (* less than, trivial by translation rule for > *) A28: "xor [a < 0, a = 0, 0 < a, a = Φ]" (* quadrachotomy *) A29: "¬ ((a = ∞ ∨ a = - ∞) ∧ sgn b ≠ sgn c ∧ (b + c ∉ {0,Φ})) ==> a * (b+c) = (a * b)+(a * c)" (* distributivity *) A30: "a ≤ b = (a = b ∨ a < b)" (* definition of le *) instance trans_mult ⊆ comm_monoid_mult by (intro_classes, rule A12 [THEN sym], rule A13, rule A14); subsection{* Axiomatic classes trans\_complete and trans\_reals *} constdefs lattice_complete :: "('a::ord) set => bool" "lattice_complete xs == ∀ ys. ys ⊆ xs --> (∃ u ∈ xs. (∀ y ∈ ys. y ≤ u) ∧ (∀ v ∈ xs. (∀ y ∈ ys. y ≤ v) --> u ≤ v))" axclass trans_complete < trans_add, one, times, inverse, ord A31: "lattice_complete {x. x ≠ Φ}" axclass trans_reals < trans_mult, trans_complete ; text{* TODO: validate definition by proving lattice-completeness of [0..1] *} end
lemma xor_singleton:
xor [b] = b
lemma xor_pair:
xor [a, b] = (a ≠ b)
lemma xor_triple:
xor [a, b, c] = (a ∧ ¬ b ∧ ¬ c ∨ ¬ a ∧ b ∧ ¬ c ∨ ¬ a ∧ ¬ b ∧ c)