Up to index of Isabelle/HOL/HOL-Complex/transnumber
theory TransNumberModelheader {* A Model for Transarithmetic *} theory TransNumberModel imports TransNumberAxclass Real begin datatype 'a trans_number = P 'a | Infinity | MinusInfinity | Nullity lemma inv_R_R[simp]: "inv P (P x) = x"; by (rule inv_f_f, unfold inj_on_def, auto); consts primitive :: "'a trans_number => bool" primrec "primitive (P x) = True" "primitive Infinity = False" "primitive MinusInfinity = False" "primitive Nullity = False" lemma primitive_iff_exists: "primitive x = (∃ r. x = P r)"; by (case_tac x, auto); lemma primitiveD: "primitive x ==> ∃ r. x = P r"; by (simp add: primitive_iff_exists); instance trans_number :: (zero) zero .. instance trans_number ::(type) infinity .. instance trans_number ::(type) nullity .. instance trans_number :: (plus) plus .. instance trans_number :: (minus) minus .. defs (overloaded) trans_number_zero_def: "0 == P 0" trans_number_infinity_def: "∞ == Infinity" trans_number_nullity_def: "Φ == Nullity"; text {* Note type annotations below, and overloaded symbol awkwardness *} section{* A model for axiomatic class trans\_add *} primrec "P (x::'a::{plus,minus}) + y = ( if primitive y then P (x + inv P y) else if y = ∞ then ∞ else if y = -∞ then -∞ else Φ)" "Infinity + (y::'a::{plus,minus} trans_number) = (if primitive y ∨ y = ∞ then ∞ else Φ)" "MinusInfinity +(y::'a::{plus,minus} trans_number) = (if primitive y ∨ y = -∞ then -∞ else Φ)" Nullity_add_left: "Nullity +(y::'a::{plus,minus} trans_number) = Φ" ; primrec uminus_P: "- P x = P (- (x))" uminus_Infinity: "- Infinity = MinusInfinity" uminus_MinusInfinity: "- MinusInfinity = Infinity" uminus_Nullity: "- Nullity = Nullity"; text {* A6 *} defs (overloaded) trans_number_subtract_def: "!! (y::'a::{plus,minus} trans_number). x - y == x + (- y)" lemmas trans_number_defs = trans_number_zero_def trans_number_infinity_def trans_number_nullity_def trans_number_subtract_def; lemma trans_number_minus_infinity_sym_def: "MinusInfinity == -∞"; by (simp add: trans_number_defs); lemmas trans_number_sym_defs = trans_number_zero_def[symmetric] trans_number_infinity_def [symmetric] trans_number_minus_infinity_sym_def trans_number_nullity_def [symmetric] trans_number_subtract_def [symmetric] lemma primitive_zero[simp]: "primitive 0"; by (unfold trans_number_zero_def, simp); lemma not_primitive_simps[simp]: "¬ primitive (∞) ∧ ¬ primitive (-∞) ∧ ¬ primitive Φ"; by (unfold trans_number_defs, simp); lemma primitive_iff: "primitive x = (x ≠ ∞ ∧ x ≠ -∞ ∧ x ≠ Φ)"; by (case_tac x, simp_all add: trans_number_defs); subsection{*Distinctness of special values *} lemma P_neq_infinity[simp]: "P x ≠ ∞"; by (unfold trans_number_defs, simp); lemma P_neq_minus_infinity[simp]: "P x ≠ -∞"; by (unfold trans_number_defs, simp); lemma P_neq_nullity[simp]: "P x ≠ Φ"; by (unfold trans_number_defs, simp); lemma zero_neq_infinity[simp]: "(0::'a::zero trans_number) ≠ ∞"; by (unfold trans_number_defs, simp); lemma zero_neq_minus_infinity[simp]: "(0::'a::{zero,minus } trans_number) ≠ -∞"; by (unfold trans_number_defs, simp); lemma zero_neq_nullity[simp]: "(0::'a::{zero,minus } trans_number) ≠ Φ"; by (unfold trans_number_defs, simp); lemma infinity_neq_minus_infinity[simp]: "(∞::'a::minus trans_number) ≠ -∞"; by (unfold trans_number_defs, simp); lemma infinity_neq_nullity[simp]: "(∞::'a::minus trans_number) ≠ Φ"; by (unfold trans_number_defs, simp); lemma minus_infinity_neq_nullity[simp]: "(-∞::'a::minus trans_number) ≠ Φ"; by (unfold trans_number_defs, simp); declare P_neq_infinity [THEN not_sym,simp]; declare P_neq_minus_infinity [THEN not_sym,simp]; declare P_neq_nullity [THEN not_sym,simp]; declare zero_neq_infinity [THEN not_sym,simp]; declare zero_neq_minus_infinity [THEN not_sym,simp]; declare zero_neq_nullity [THEN not_sym,simp]; declare infinity_neq_minus_infinity [THEN not_sym,simp]; declare infinity_neq_nullity [THEN not_sym,simp]; declare minus_infinity_neq_nullity [THEN not_sym,simp]; lemma P_add_P[simp]: "P x + P y = P ((x ::'a::{plus,minus}) + y)"; by (simp add: trans_number_subtract_def); lemma P_add_non_primitive[simp]: "P x + ∞ = ∞ ∧ P x - ∞ = -∞ ∧ P x + Φ = Φ"; by (simp add: trans_number_subtract_def); lemma Infinity_add_left[simp]: "∞ + P x = (∞::'a::{plus,minus} trans_number) ∧ ∞ + ∞ = (∞::'a trans_number) ∧ ∞ - ∞ = (Φ ::'a trans_number) ∧ ∞ + Φ = (Φ ::'a trans_number)"; by (simp add: trans_number_defs); lemma MinusInfinity_add_left[simp]: "-∞ + P x = (-∞::'a::{plus,minus} trans_number) ∧ -∞ + ∞ = (Φ::'a trans_number) ∧ -∞ - ∞ = (-∞ ::'a trans_number) ∧ -∞ + Φ = (Φ ::'a trans_number)"; by (simp add: trans_number_defs); lemma uminus_simps[simp]: "- P x = (P (- x) ::'a::{minus} trans_number) ∧ - ( -∞) = (∞::'a trans_number) ∧ - Φ = (Φ ::'a trans_number)"; by (simp add: trans_number_defs); text {* A4 *} lemma nullity_add_left[simp]: "Φ + x = (Φ ::'a::{plus,minus} trans_number)"; by (simp add: trans_number_nullity_def); lemma nullity_subtract_left[simp]: "Φ - x = (Φ ::'a::{plus,minus} trans_number)"; by (simp add: trans_number_defs); text{* Axiom A5 *} lemma addition_infinity_not_null: "[| x≠-∞ ; x ≠ Φ |] ==> (x::'a::{plus,minus} trans_number) + ∞ = ∞"; by (case_tac x, simp_all add: trans_number_defs); text {* A1 *} lemma add_assoc: "((x::'a::ab_group_add trans_number) + y) + z = x + (y + z)"; apply (case_tac x, safe); apply (tactic "ALLGOALS (case_tac \"y\")", safe); apply (tactic "ALLGOALS (case_tac \"z\")", safe); by ( simp_all add: trans_number_sym_defs); text {* A2 *} lemma add_commute: "(x::'a::ab_group_add trans_number) + y = y + x"; apply (case_tac x, safe); apply (tactic "ALLGOALS (case_tac \"y\")"); by ( simp_all add: trans_number_sym_defs); lemma add_left_commute: "a + (b + c) = b + (a + (c::'a::ab_group_add trans_number))" by (rule mk_left_commute [of "op +", OF add_assoc add_commute]) theorems trans_add_ac = add_assoc add_commute add_left_commute; lemma nullity_add_right[simp]: "x + Φ = (Φ ::'a::ab_group_add trans_number)"; by (subst add_commute, simp add: trans_number_nullity_def); text {* A3 *} lemma add_identity[simp]: "0 + (x::'a::ab_group_add trans_number) = x"; apply (unfold trans_number_zero_def, case_tac x); by (simp_all, simp_all add: trans_number_defs); text {* A7 *} lemma bijectivity_of_uminus[simp]: "-(-(x::'a::ab_group_add trans_number)) = x"; by (case_tac x, simp_all add: trans_number_sym_defs); text {* A8 *} lemma additive_inverse[simp]: "!! (x::'a::ab_group_add trans_number). primitive x ==> x - x = 0"; apply (case_tac x); by ( simp_all add: trans_number_subtract_def trans_number_zero_def); text {* A9 *} lemma uminus_nullity: "- (Φ ::('a::minus) trans_number) = Φ"; by simp; text {* A10 *} lemma subtraction_infinity_not_null: "!! (x::'a::{plus,minus} trans_number). [| x ≠ ∞; x ≠ Φ |] ==> x - ∞ = -∞" by (case_tac x, simp_all add: trans_number_defs); instance trans_number :: (ab_group_add) trans_add apply (intro_classes, simp_all add:); apply (rule add_assoc [THEN sym]); apply (rule add_commute); apply (subst add_commute, erule addition_infinity_not_null, assumption); apply (simp add: trans_number_subtract_def); apply (rule additive_inverse, simp add: primitive_iff); by (erule subtraction_infinity_not_null, assumption); section{*Transnumber ordering *} instance trans_number :: (ord) ord ..; primrec P_less: "P x < y = (primitive y ∧ (x::'a::{minus,ord}) < inv P y | y = ∞)" Infinity_less: "(Infinity < (y::'a::{minus,ord} trans_number)) = False" MinusInfinity_less: "(MinusInfinity < y) = (y ≠ -∞ ∧ y ≠ (Φ::'a::{minus,ord} trans_number))" Nullity_less: "(Nullity < (y::'a::{minus,ord} trans_number)) = False" defs (overloaded) trans_number_le_def: "(x::'a::{minus,ord} trans_number) <= y == (x < y | x = y)" lemma P_less_P[simp]: "(P x < P y) = (x < (y::'a::{minus,order}))"; by (simp add: trans_number_defs); lemma P_less_non_primitive[simp]: "(P x < ∞) ∧ ¬ (P x < -∞) ∧ ¬ (P x < Φ)" by (simp add: trans_number_defs); lemma P_le[simp]: "(P x ≤ P y = (x ≤ (y::'a::{order,minus}))) ∧ (P x ≤ ∞) ∧ ¬ (P x ≤ -∞) ∧ ¬ (P x ≤ Φ)" by (simp add: trans_number_defs trans_number_le_def order_le_less); lemma not_infinity_less[simp]: "¬ ((∞::'a::{minus,ord} trans_number) < x)"; by (unfold trans_number_defs,simp); lemma infinity_le [simp]: "((∞::'a::{minus,ord} trans_number) ≤ x) = (x = ∞)"; by (auto simp: trans_number_le_def); lemma le_infinity[simp]: " x ≤ (∞::'a::{minus,ord} trans_number) = (x ≠ Φ)"; by (case_tac x, auto simp: trans_number_le_def trans_number_defs); lemma minus_infinity_less[simp]: "(-(∞::'a::{minus,ord} trans_number) < x) = (x ≠ -∞ ∧ x ≠ Φ)"; by (simp add: trans_number_defs); lemma minus_infinity_le[simp]: "(-(∞::'a::{minus,ord} trans_number) ≤ x) = (x ≠ Φ)"; by (auto simp: trans_number_le_def); lemma not_nullity_less[simp]: "¬ ((Φ::'a::{minus,ord} trans_number) < x)"; by (unfold trans_number_nullity_def, simp); lemma nullity_le[simp]: "((Φ::'a::{minus,ord} trans_number) ≤ x) = (x = Φ)"; by (auto simp: trans_number_le_def); lemma not_less_nullity[simp]: "¬ (x < (Φ::'a::{minus,ord} trans_number))"; by (case_tac x, simp_all); lemma le_nullity[simp]: "(x ≤ (Φ::'a::{minus,order} trans_number)) = (x = Φ)"; by (case_tac x, simp_all add: trans_number_sym_defs); lemma zero_less_P[simp]: "((0::'a::{minus,ord,zero} trans_number) < P x) = (0 < x)"; by (simp add: trans_number_zero_def); text{* A25 *} lemma zero_less_infinity[simp]: "((0::'a::{minus,ord,zero} trans_number) < ∞)"; by (simp add: trans_number_zero_def); lemma zero_not_less_minus_infinity[simp]: "¬ ((0::'a::{minus,ord,zero} trans_number) < -∞)"; by (simp add: trans_number_zero_def); lemma irreflexive_less[simp]: "¬ ((x::'a::{minus,order,zero} trans_number) < x)"; by (case_tac x, auto simp: trans_number_sym_defs); declare P_less[simp del]; text{* A26 *} lemma trans_number_ordering: "(x - y > 0) = (x > (y::'a::lordered_ab_group trans_number))"; apply (case_tac x); apply (tactic "ALLGOALS (case_tac \"y\")"); apply (simp_all add: trans_number_subtract_def); apply (unfold trans_number_sym_defs); by (simp_all add: compare_rls); text{* A27 holds trivially since gt is simply a syntactic abbreviation *} lemma less_than_gt_than_eq: "(x < y) = (y > x)"; by (rule refl); text{* A28 *} lemma quadrachotomoy: "!!x::'a::{ab_group_add,linorder} trans_number. xor [x < 0, x = 0, 0 < x, x= Φ]"; apply (case_tac x); apply (simp_all add: trans_number_sym_defs); apply (rule_tac x="a" and y ="0" in linorder_cases); by (auto simp: trans_number_zero_def); text{* A29 *} lemma pos_closure_add: "!! x::'a::{lordered_ab_group} trans_number. [| 0 < x ; 0 < y |] ==> 0 < x + y"; apply (case_tac x); apply (tactic "ALLGOALS (case_tac \"y\")"); apply (simp_all add: trans_number_sym_defs); by (erule add_pos_pos, assumption); lemma trans_number_order_refl: "(x::'a::{minus,order} trans_number) ≤ x"; apply (case_tac x); by (simp_all add: trans_number_sym_defs); lemma trans_number_order_trans: "[| (x::'a::{minus,order} trans_number) ≤ y; y ≤ z |] ==> x ≤ z"; apply (case_tac x); apply (tactic "ALLGOALS (case_tac \"y\")"); apply (tactic "ALLGOALS (case_tac \"z\")"); by (simp_all add: trans_number_sym_defs); lemma trans_number_order_antisym: "[| (x::'a::{minus,order} trans_number) ≤ y; y ≤ x |] ==> x = y"; apply (case_tac x); apply (tactic "ALLGOALS (case_tac \"y\")"); by (simp_all add: trans_number_sym_defs); lemma trans_number_less_le: "((x::'a::{minus,order} trans_number) < y) = (x ≤ y ∧ x ≠ y)"; apply (unfold trans_number_le_def, auto); by (case_tac y, simp_all add: trans_number_sym_defs); axclass minus_order ⊆ order, minus; instance pordered_ab_group_add ⊆ minus_order ..; instance trans_number :: (minus_order)order apply (intro_classes); apply (rule trans_number_order_refl); apply (erule trans_number_order_trans, assumption); apply (erule trans_number_order_antisym, assumption); by (rule trans_number_less_le); lemma ext_number_linear: "[| (x ::'a::{minus,linorder} trans_number) ≠ Φ; y ≠ Φ |] ==> x ≤ y | y ≤ x "; apply (case_tac x); apply (tactic "ALLGOALS (case_tac \"y\")"); by (simp_all add: trans_number_sym_defs linorder_linear); lemma not_elem_conv: "xs ⊆ {x. x ≠ a} = (a ∉ xs)"; by (unfold subset_def, auto); subsection{* Lattice-completeness of trans\_numbers *} text {* NOTE: cannot express l.-c. of transnumbers as instance rule *} lemma ext_number_complete_lattice: "lattice_complete {x :: real trans_number. x ≠ Φ}"; apply (unfold lattice_complete_def); apply (clarsimp simp: not_elem_conv); apply (case_tac "∃ a. ∀ x ∈ ys. x < P a"); apply (case_tac "∃ b. P b ∈ ys", safe); apply (cut_tac S = "inv P ` (ys - {-∞})" in reals_complete); apply (fastsimp); apply (rule_tac x="a" in exI); apply (unfold isUb_def setle_def isLub_def leastP_def setge_def, safe); apply (case_tac x, unfold trans_number_sym_defs); apply (fastsimp, fastsimp, fastsimp, fastsimp, fast); apply (clarsimp simp: isUb_def setle_def); apply (rule_tac x="P t" in exI, safe, simp_all); apply (case_tac y, unfold trans_number_sym_defs, simp); apply (erule_tac x = "P aa" in ballE); back; apply (simp+, force, fastsimp, fast); apply (case_tac "v", unfold trans_number_sym_defs); apply clarsimp; apply (erule_tac x = "aa" in allE, clarsimp); apply (case_tac y, unfold trans_number_sym_defs); apply (fastsimp, fastsimp, assumption, fastsimp, simp); apply (fastsimp, fastsimp) apply (rule_tac x="-∞" in exI, clarsimp); apply (case_tac y, unfold trans_number_sym_defs); apply ( fastsimp, fastsimp, simp, fastsimp); apply (rule_tac x = "∞" in exI, auto); apply (case_tac v, unfold trans_number_sym_defs); apply (auto); apply (erule_tac x = "a + 1" in allE, clarify); apply (erule_tac x = "x" in ballE); apply (auto simp: trans_number_less_le); apply (erule_tac notE, erule_tac trans_number_order_trans, simp); apply (erule_tac x = "1" in allE, auto); apply (erule_tac x = "x" in ballE); by (erule_tac notE, erule_tac trans_number_order_trans, fastsimp+); section {*A model for axiomatic class trans\_mult *} instance trans_number :: (one) one .. instance trans_number :: (inverse) inverse .. instance trans_number :: (times)times ..; defs (overloaded) trans_number_one_def: "1 == P 1" lemmas trans_number_defs = trans_number_zero_def trans_number_one_def trans_number_infinity_def trans_number_nullity_def trans_number_subtract_def; lemmas trans_number_sym_defs = trans_number_zero_def[symmetric] trans_number_one_def[symmetric] trans_number_infinity_def [symmetric] trans_number_minus_infinity_sym_def trans_number_nullity_def [symmetric] trans_number_subtract_def [symmetric] lemma primitive_one[simp]: "primitive 1"; by (unfold trans_number_one_def, simp); text{* Warning: simpsets contain different mult laws with special cases for RHS *} primrec trans_mult_P: "P (x::'a::{zero,times,minus,ord}) * y = ( if primitive y then P (x * inv P y) else if (y = ∞ ∧ x > 0) | (y = -∞ ∧ x < 0) then ∞ else if (y = ∞ ∧ x < 0) | (y = -∞ ∧ x > 0) then -∞ else Φ)" trans_mult_Infinity: "Infinity * (y::'a::{zero,times,minus,ord} trans_number) = (if (primitive y ∧ y > 0) | y = ∞ then ∞ else if (primitive y ∧ y < 0) | y = -∞ then -∞ else Φ)" trans_mult_MinusInfinity: "MinusInfinity * (y::'a::{zero,times,minus,ord} trans_number) = (if (primitive y ∧ y < 0) | y = -∞ then ∞ else if (primitive y ∧ y > 0) | y = ∞ then -∞ else Φ)" trans_mult_Nullity: "Nullity * (y::'a::{zero,times,minus,ord} trans_number) = Φ" ; lemma P_mult_P[simp]: "P x * P y = P ((x ::'a::{zero,times,minus,linorder}) * y)"; by auto; text {* A15 is first conjunct of mult\_nullity, see also trans\_mult\_nullity *} lemma mult_nullity[simp]: "(Φ ::'a ::ordered_idom trans_number) * x = Φ ∧ x * Φ = Φ"; apply (rule conjI); apply (simp add: trans_number_nullity_def); by (case_tac x, auto); text {* A16 is fourth conjunct of mult\_zero *} lemma mult_zero[simp]: "0 * P (x::'a::ordered_idom) = 0 ∧ P x * 0 = 0 ∧ (0 ::'a trans_number) * ∞ = Φ ∧ ∞ * (0 ::'a trans_number) = Φ ∧ (0 ::'a trans_number) * -∞ = Φ ∧ -∞ * (0 ::'a trans_number) = Φ ∧ ∞ * Φ = (Φ ::'a trans_number)"; by (simp add: trans_number_defs); lemma mult_infinity[simp]: "∞ * (∞::'a::ordered_idom trans_number) = ∞ ∧ (∞::'a trans_number) * -∞ = -∞ ∧ -∞ * (∞::'a trans_number) = -∞ ∧ -∞ * -∞ = (∞::'a trans_number)"; by (simp add: trans_number_defs); lemma P_mult_infinity_less_zero: "!! x ::('a::ordered_idom). x < 0 ==> P x * ∞ = - ∞ ∧ ∞ * P x = - ∞"; by (simp add: trans_number_defs); lemma P_mult_infinity_gt_zero: "!! x ::('a::ordered_idom). 0 < x ==> P x * ∞ = ∞ ∧ ∞ * P x = ∞"; by (simp add: trans_number_defs); lemma P_mult_MinusInfinity_less_zero: "!! x ::('a::ordered_idom). x < 0 ==> P x * -∞ = ∞ ∧ -∞ * P x = ∞"; by (simp add: trans_number_defs); lemma P_mult_MinusInfinity_gt_zero: "!! x ::('a::ordered_idom). 0 < x ==> P x * -∞ = -∞ ∧ -∞ * P x = -∞"; by (simp add: trans_number_defs); lemmas P_mult_infinities = P_mult_infinity_less_zero P_mult_infinity_gt_zero P_mult_MinusInfinity_less_zero P_mult_MinusInfinity_gt_zero; declare trans_mult_P [simp del] trans_mult_Infinity [simp del] trans_mult_MinusInfinity [simp del] trans_mult_Nullity [simp del]; text{* A13 *} lemma mult_commute: "(x::'a::ordered_idom trans_number) * y = y * x"; apply (case_tac x, safe); apply (tactic "ALLGOALS (case_tac \"y\")", safe); apply (simp_all add: trans_number_sym_defs mult_ac); by ((rule_tac x="a" and y ="0" in linorder_cases, (simp add: trans_number_zero_def [symmetric] P_mult_infinities)+)+); text{* A12 *} lemma mult_assoc: "((x::'a::ordered_idom trans_number) * y) * z = x * (y * z)"; apply (case_tac x, safe); apply (tactic "ALLGOALS (case_tac \"y\")", safe); apply (tactic "ALLGOALS (case_tac \"z\")", safe); apply (simp_all add: trans_number_sym_defs mult_ac); apply (tactic "ALLGOALS (case_tac \"a = 0\")"); apply (tactic "ALLGOALS (case_tac \"a < 0\")"); apply (simp_all add: trans_number_sym_defs P_mult_infinities mult_ac linorder_not_less order_le_less); apply (tactic "ALLGOALS(case_tac \"aa = 0\")"); apply (tactic "ALLGOALS(case_tac \"aa < 0\")"); by (simp_all add: trans_number_sym_defs P_mult_infinities mult_ac linorder_not_less order_le_less zero_less_mult_iff mult_less_0_iff); lemma mult_left_commute: "x * (y * z) = y * (x * (z::'a:: ordered_idom trans_number))"; by (rule mk_left_commute [of "op *", OF mult_assoc mult_commute]) lemmas trans_mult_ac = mult_assoc mult_commute mult_left_commute; text{* A14 *} lemma mult_one_left[simp]: "1 * x = (x::'a:: ordered_idom trans_number)"; apply (case_tac x); apply (simp_all add: trans_number_one_def); apply (simp add: P_mult_infinities trans_number_infinity_def[symmetric]); apply (simp add: P_mult_infinities uminus_Infinity [THEN sym] trans_number_infinity_def[symmetric]); by (simp add: trans_number_nullity_def [symmetric]); lemma mult_one_right[simp]: "x * 1 = (x::'a:: ordered_idom trans_number)"; by (subst mult_commute, rule mult_one_left); lemma not_primitive_mult_infinity[simp]: "¬ (primitive (P (x::'a::ordered_idom) * ∞))"; apply (case_tac "x < 0"); apply (simp add: P_mult_infinities); by (auto simp: linorder_not_less order_le_less P_mult_infinities trans_number_sym_defs); lemma not_primitive_mult_MinusInfinity[simp]: "¬ (primitive (P (x::'a::ordered_idom) * -∞))"; apply (case_tac "x < 0"); apply (simp add: P_mult_infinities); by (auto simp: linorder_not_less order_le_less P_mult_infinities trans_number_sym_defs); subsection{* Inverse and division *} primrec "inverse (P (x::'a::{inverse,zero})) = (if x = 0 then ∞ else P (inverse x))" "inverse (Infinity::('a::{inverse,zero}) trans_number) = 0" "inverse (MinusInfinity::('a::{inverse,zero}) trans_number) = 0" "inverse (Nullity::('a::{inverse,zero}) trans_number)= Φ"; text {* A17 *} defs (overloaded) trans_number_divison_def: "x / (y::'a::{times,inverse} trans_number) == x * inverse y" lemma inverse_Infinity[simp]: "inverse (∞ ::('a::{inverse,zero}) trans_number) = 0" by (simp add: trans_number_defs); lemma inverse_MinusInfinity[simp]: "inverse (-∞ ::('a::{inverse,zero,minus}) trans_number) = 0"; by (simp add: trans_number_defs); lemma inverse_nullity[simp]: "inverse (Φ ::('a::{inverse,zero}) trans_number)= Φ"; by (simp add: trans_number_defs); text{* A18 *} lemma multiplicative_inverse: "[| primitive (x::'a::ordered_field trans_number); x ≠ 0 |] ==> x / x = 1" apply (case_tac x, simp_all); by (auto simp: trans_number_divison_def trans_number_sym_defs); text{* A19 *} lemma bij_inverse: " (x::'a::ordered_field trans_number) ≠ - ∞ ==> inverse (inverse x) = x"; apply (case_tac x) apply (simp_all add: trans_number_defs nonzero_inverse_inverse_eq); by (fast intro: inverse_zero_imp_zero); text{* A20 *} lemma inverse_zero[simp]: "inverse (0::'a::ordered_field trans_number) = ∞"; by (simp add: trans_number_defs); text{* A21 *} lemma inverse_MinusInfinity[simp]: "inverse (-∞ ::'a::ordered_field trans_number) = 0"; by (simp add: trans_number_defs); text{* A22 *} lemma inverse_nullity[simp]: "inverse (Φ::'a::ordered_field trans_number) = Φ"; by (simp add: trans_number_defs); text{* A23 *} lemma positive_inf_mult: "(∞ * x = ∞) = (0 < (x::'a::ordered_field trans_number))" apply (case_tac x); apply (simp_all add: trans_number_sym_defs); apply(rule_tac x="a" and y ="0" in linorder_cases); apply (simp_all add: P_mult_infinities); by (simp add: trans_number_sym_defs); text{* A24 *} lemma negative_inf_mult: "(∞ * x = -∞) = (x < (0::'a::ordered_field trans_number))"; apply (case_tac x); apply (simp_all add: trans_number_sym_defs); apply (simp add: trans_number_zero_def); apply(rule_tac x="a" and y ="0" in linorder_cases); apply (simp_all add: P_mult_infinities); by (simp add: trans_number_sym_defs); instance trans_number :: (ordered_idom) sgn ..; defs (overloaded) trans_number_sgn_def: "sgn (a::'a::ordered_idom trans_number) == (if 0 < a then 1 else if 0 = a then 0 else if a < 0 then - 1 else (* a = Φ *) Φ)"; instance trans_number :: (ordered_idom) trans_sgn by (intro_classes, unfold trans_number_sgn_def, rule refl); lemma P_mult_infinity_neq_infinity_iff: "(P a * ∞ ≠ ∞) = (a ≤ (0::'a::ordered_idom))"; apply (case_tac "a< 0", simp add: P_mult_infinity_less_zero); by (auto simp: P_mult_infinity_gt_zero linorder_not_less order_le_less trans_number_sym_defs); lemma P_mult_infinity_neq_MinusInfinity_iff: "(P a * ∞ ≠ -∞) = (0 ≤ (a::'a::ordered_idom))"; apply (case_tac "a< 0", simp add: P_mult_infinity_less_zero); by (auto simp: P_mult_infinity_gt_zero linorder_not_less order_le_less trans_number_sym_defs); lemma P_mult_MinusInfinity_neq_MinusInfinity_iff: "(P a * -∞ ≠ -∞) = (a ≤ (0::'a::ordered_idom))"; apply (case_tac "0 < a", simp add: P_mult_MinusInfinity_gt_zero); by (auto simp: P_mult_MinusInfinity_less_zero linorder_not_less order_le_less trans_number_sym_defs); lemma P_mult_MinusInfinity_neq_infinity_iff: "(P a * -∞ ≠ ∞) = (0 ≤ (a::'a::ordered_idom))"; apply (case_tac "0< a", simp add: P_mult_MinusInfinity_gt_zero); by (auto simp: P_mult_MinusInfinity_less_zero linorder_not_less order_le_less trans_number_sym_defs); lemma sgn_P: "sgn (P (x::'a::ordered_idom)) = (if x < 0 then - 1 else if x = 0 then 0 else 1)"; apply (unfold trans_number_sgn_def, simp add: trans_number_sym_defs); by (safe, simp_all add: trans_number_zero_def); lemma uminus_eq_iff: "(-x = (x::'a::ordered_idom)) = (x = 0)"; by auto; (* Warning: need to avoid looping premise (-1) = 1 in next proof *) lemma sgn_P_eq_iff: "!! (x::'a::ordered_idom) (y::'a). (sgn (P x) = sgn (P y)) = (((x < 0) = (y < 0)) ∧ ((x = 0) = (y = 0)) ∧ ((0 < x) = (0 < (y::'a::ordered_idom))))"; apply (simp add: sgn_P, safe, simp_all); apply (simp add: trans_number_defs); apply (simp add: trans_number_defs); apply (simp add: trans_number_defs); apply (unfold trans_number_defs); apply (simp only: uminus_P trans_number.simps uminus_eq_iff); apply (simp); by (simp only: uminus_P trans_number.simps uminus_eq_iff); lemma sgn_zero[simp]: "sgn (0::('a::ordered_idom trans_number)) = 0"; by (simp add: trans_number_sgn_def); lemma sgn_infinity[simp]: "sgn (∞ ::('a::ordered_idom trans_number)) = 1"; by (simp add: trans_number_sgn_def); lemma sgn_minus_infinity[simp]: "sgn (-∞ ::('a::ordered_idom trans_number)) = - 1"; by (simp add: trans_number_sgn_def); lemma sgn_zero_iff[simp]: "(sgn (x::('a::ordered_idom trans_number)) = 0) = (x = 0)"; by (auto simp: trans_number_sgn_def, simp_all add: trans_number_defs); lemma sgn_P_one_iff[simp]: "(sgn (P (x::'a::ordered_idom)) = 1) = (0 < x)"; apply (simp add: trans_number_sgn_def, safe, simp); apply(unfold trans_number_defs); apply (simp only: uminus_P trans_number.simps uminus_eq_iff); by simp_all; lemma sgn_P_minus_one_iff[simp]: "(sgn (P (x::'a::ordered_idom)) = - 1) = (x < 0)"; apply (simp add: trans_number_sgn_def, safe, simp); apply(unfold trans_number_defs); apply (fast, simp, simp); apply (simp only: uminus_P trans_number.simps uminus_eq_iff); apply (blast intro: order_less_asym, simp); apply (simp only: uminus_P trans_number.simps uminus_eq_iff); apply (blast intro: order_less_asym, simp, simp); apply (simp only: uminus_P trans_number.simps uminus_eq_iff); apply (blast intro: order_less_asym); by (simp, simp); lemma P_eq_zero: "(P x = 0) = (x = 0)"; by (unfold trans_number_zero_def, auto); text{* A29 *} lemma distributivity: "!! a::('a::ordered_field trans_number). ¬ ((a = ∞ ∨ a = - ∞) ∧ sgn b ≠ sgn c ∧ (b + c ∉ {0,Φ})) ==> a * (b+c) = (a * b)+(a * c)" apply (case_tac a, tactic "ALLGOALS Clarsimp_tac"); apply (tactic "ALLGOALS (case_tac \"b\") THEN ALLGOALS Clarsimp_tac"); apply (tactic "ALLGOALS (case_tac \"c\") THEN ALLGOALS Clarsimp_tac"); apply (simp_all add: trans_number_sym_defs); apply (rule right_distrib, safe); apply (simp add: P_mult_infinities trans_number_sym_defs P_mult_infinity_neq_infinity_iff P_mult_infinity_neq_MinusInfinity_iff); apply (simp add: P_mult_infinities trans_number_sym_defs P_mult_MinusInfinity_neq_infinity_iff P_mult_MinusInfinity_neq_MinusInfinity_iff); apply (tactic "ALLGOALS (case_tac \"aa < 0\")"); apply (simp_all add: linorder_not_less order_le_less, safe); apply (simp_all add: trans_number_sym_defs P_mult_infinities sgn_P_eq_iff P_eq_zero); apply auto; apply (subst P_mult_infinity_less_zero [THEN conjunct2], simp, rule refl); apply (subst P_mult_infinity_gt_zero [THEN conjunct2], simp, rule refl); apply (drule sym); prefer 4; apply (drule sym); by (simp_all add: P_mult_infinities trans_number_sym_defs); instance trans_number :: (ordered_field) trans_mult; apply (intro_classes); prefer 17; apply (rule quadrachotomoy); (* avoid simplification of xor expression..*) apply (simp_all add: multiplicative_inverse primitive_iff bij_inverse positive_inf_mult negative_inf_mult trans_number_ordering); apply (rule mult_assoc [THEN sym]); apply (rule mult_commute); apply (simp add: trans_number_divison_def); apply (rule distributivity, simp); by (auto simp: order_le_less); end
lemma inv_R_R:
inv P (P x) = x
lemma primitive_iff_exists:
primitive x = (∃r. x = P r)
lemma primitiveD:
primitive x ==> ∃r. x = P r
lemmas trans_number_defs:
0 == P (0::'a)
∞ == Infinity
Φ == Nullity
x - y == x + - y
lemmas trans_number_defs:
0 == P (0::'a)
∞ == Infinity
Φ == Nullity
x - y == x + - y
lemma trans_number_minus_infinity_sym_def:
MinusInfinity == - ∞
lemmas trans_number_sym_defs:
P (0::'a1) == 0
Infinity == ∞
MinusInfinity == - ∞
Nullity == Φ
x1 + - y1 == x1 - y1
lemmas trans_number_sym_defs:
P (0::'a1) == 0
Infinity == ∞
MinusInfinity == - ∞
Nullity == Φ
x1 + - y1 == x1 - y1
lemma primitive_zero:
primitive 0
lemma not_primitive_simps:
¬ primitive (∞) ∧ ¬ primitive (- ∞) ∧ ¬ primitive Φ
lemma primitive_iff:
primitive x = (x ≠ ∞ ∧ x ≠ - ∞ ∧ x ≠ Φ)
lemma P_neq_infinity:
P x ≠ ∞
lemma P_neq_minus_infinity:
P x ≠ - ∞
lemma P_neq_nullity:
P x ≠ Φ
lemma zero_neq_infinity:
0 ≠ ∞
lemma zero_neq_minus_infinity:
0 ≠ - ∞
lemma zero_neq_nullity:
0 ≠ Φ
lemma infinity_neq_minus_infinity:
∞ ≠ - ∞
lemma infinity_neq_nullity:
∞ ≠ Φ
lemma minus_infinity_neq_nullity:
- ∞ ≠ Φ
lemma P_add_P:
P x + P y = P (x + y)
lemma P_add_non_primitive:
P x + ∞ = ∞ ∧ P x - ∞ = - ∞ ∧ P x + Φ = Φ
lemma Infinity_add_left:
∞ + P x = ∞ ∧ ∞ + ∞ = ∞ ∧ ∞ - ∞ = Φ ∧ ∞ + Φ = Φ
lemma MinusInfinity_add_left:
- ∞ + P x = - ∞ ∧ - ∞ + ∞ = Φ ∧ - ∞ - ∞ = - ∞ ∧ - ∞ + Φ = Φ
lemma uminus_simps:
- P x = P (- x) ∧ - (- ∞) = ∞ ∧ - Φ = Φ
lemma nullity_add_left:
Φ + x = Φ
lemma nullity_subtract_left:
Φ - x = Φ
lemma addition_infinity_not_null:
[| x ≠ - ∞; x ≠ Φ |] ==> x + ∞ = ∞
lemma add_assoc:
x + y + z = x + (y + z)
lemma add_commute:
x + y = y + x
lemma add_left_commute:
a + (b + c) = b + (a + c)
theorems trans_add_ac:
x + y + z = x + (y + z)
x + y = y + x
a + (b + c) = b + (a + c)
theorems trans_add_ac:
x + y + z = x + (y + z)
x + y = y + x
a + (b + c) = b + (a + c)
lemma nullity_add_right:
x + Φ = Φ
lemma add_identity:
0 + x = x
lemma bijectivity_of_uminus:
- (- x) = x
lemma additive_inverse:
primitive x ==> x - x = 0
lemma uminus_nullity:
- Φ = Φ
lemma subtraction_infinity_not_null:
[| x ≠ ∞; x ≠ Φ |] ==> x - ∞ = - ∞
lemma P_less_P:
(P x < P y) = (x < y)
lemma P_less_non_primitive:
P x < ∞ ∧ ¬ P x < - ∞ ∧ ¬ P x < Φ
lemma P_le:
(P x ≤ P y) = (x ≤ y) ∧ P x ≤ ∞ ∧ ¬ P x ≤ - ∞ ∧ ¬ P x ≤ Φ
lemma not_infinity_less:
¬ ∞ < x
lemma infinity_le:
(∞ ≤ x) = (x = ∞)
lemma le_infinity:
(x ≤ ∞) = (x ≠ Φ)
lemma minus_infinity_less:
(- ∞ < x) = (x ≠ - ∞ ∧ x ≠ Φ)
lemma minus_infinity_le:
(- ∞ ≤ x) = (x ≠ Φ)
lemma not_nullity_less:
¬ Φ < x
lemma nullity_le:
(Φ ≤ x) = (x = Φ)
lemma not_less_nullity:
¬ x < Φ
lemma le_nullity:
(x ≤ Φ) = (x = Φ)
lemma zero_less_P:
(0 < P x) = ((0::'a) < x)
lemma zero_less_infinity:
0 < ∞
lemma zero_not_less_minus_infinity:
¬ 0 < - ∞
lemma irreflexive_less:
¬ x < x
lemma trans_number_ordering:
(0 < x - y) = (y < x)
lemma less_than_gt_than_eq:
(x < y) = (x < y)
lemma quadrachotomoy:
xor [x < 0, x = 0, 0 < x, x = Φ]
lemma pos_closure_add:
[| 0 < x; 0 < y |] ==> 0 < x + y
lemma trans_number_order_refl:
x ≤ x
lemma trans_number_order_trans:
[| x ≤ y; y ≤ z |] ==> x ≤ z
lemma trans_number_order_antisym:
[| x ≤ y; y ≤ x |] ==> x = y
lemma trans_number_less_le:
(x < y) = (x ≤ y ∧ x ≠ y)
lemma ext_number_linear:
[| x ≠ Φ; y ≠ Φ |] ==> x ≤ y ∨ y ≤ x
lemma not_elem_conv:
(xs ⊆ {x. x ≠ a}) = (a ∉ xs)
lemma ext_number_complete_lattice:
lattice_complete {x. x ≠ Φ}
lemmas trans_number_defs:
0 == P (0::'a)
1 == P (1::'a)
∞ == Infinity
Φ == Nullity
x - y == x + - y
lemmas trans_number_defs:
0 == P (0::'a)
1 == P (1::'a)
∞ == Infinity
Φ == Nullity
x - y == x + - y
lemmas trans_number_sym_defs:
P (0::'a1) == 0
P (1::'a1) == 1
Infinity == ∞
MinusInfinity == - ∞
Nullity == Φ
x1 + - y1 == x1 - y1
lemmas trans_number_sym_defs:
P (0::'a1) == 0
P (1::'a1) == 1
Infinity == ∞
MinusInfinity == - ∞
Nullity == Φ
x1 + - y1 == x1 - y1
lemma primitive_one:
primitive 1
lemma P_mult_P:
P x * P y = P (x * y)
lemma mult_nullity:
Φ * x = Φ ∧ x * Φ = Φ
lemma mult_zero:
0 * P x = 0 ∧ P x * 0 = 0 ∧ 0 * ∞ = Φ ∧ ∞ * 0 = Φ ∧ 0 * - ∞ = Φ ∧ - ∞ * 0 = Φ ∧ ∞ * Φ = Φ
lemma mult_infinity:
∞ * ∞ = ∞ ∧ ∞ * - ∞ = - ∞ ∧ - ∞ * ∞ = - ∞ ∧ - ∞ * - ∞ = ∞
lemma P_mult_infinity_less_zero:
x < (0::'a) ==> P x * ∞ = - ∞ ∧ ∞ * P x = - ∞
lemma P_mult_infinity_gt_zero:
(0::'a) < x ==> P x * ∞ = ∞ ∧ ∞ * P x = ∞
lemma P_mult_MinusInfinity_less_zero:
x < (0::'a) ==> P x * - ∞ = ∞ ∧ - ∞ * P x = ∞
lemma P_mult_MinusInfinity_gt_zero:
(0::'a) < x ==> P x * - ∞ = - ∞ ∧ - ∞ * P x = - ∞
lemmas P_mult_infinities:
x < (0::'a) ==> P x * ∞ = - ∞ ∧ ∞ * P x = - ∞
(0::'a) < x ==> P x * ∞ = ∞ ∧ ∞ * P x = ∞
x < (0::'a) ==> P x * - ∞ = ∞ ∧ - ∞ * P x = ∞
(0::'a) < x ==> P x * - ∞ = - ∞ ∧ - ∞ * P x = - ∞
lemmas P_mult_infinities:
x < (0::'a) ==> P x * ∞ = - ∞ ∧ ∞ * P x = - ∞
(0::'a) < x ==> P x * ∞ = ∞ ∧ ∞ * P x = ∞
x < (0::'a) ==> P x * - ∞ = ∞ ∧ - ∞ * P x = ∞
(0::'a) < x ==> P x * - ∞ = - ∞ ∧ - ∞ * P x = - ∞
lemma mult_commute:
x * y = y * x
lemma mult_assoc:
x * y * z = x * (y * z)
lemma mult_left_commute:
x * (y * z) = y * (x * z)
lemmas trans_mult_ac:
x * y * z = x * (y * z)
x * y = y * x
x * (y * z) = y * (x * z)
lemmas trans_mult_ac:
x * y * z = x * (y * z)
x * y = y * x
x * (y * z) = y * (x * z)
lemma mult_one_left:
1 * x = x
lemma mult_one_right:
x * 1 = x
lemma not_primitive_mult_infinity:
¬ primitive (P x * ∞)
lemma not_primitive_mult_MinusInfinity:
¬ primitive (P x * - ∞)
lemma inverse_Infinity:
inverse (∞) = 0
lemma inverse_MinusInfinity:
inverse (- ∞) = 0
lemma inverse_nullity:
inverse Φ = Φ
lemma multiplicative_inverse:
[| primitive x; x ≠ 0 |] ==> x / x = 1
lemma bij_inverse:
x ≠ - ∞ ==> inverse (inverse x) = x
lemma inverse_zero:
inverse 0 = ∞
lemma inverse_MinusInfinity:
inverse (- ∞) = 0
lemma inverse_nullity:
inverse Φ = Φ
lemma positive_inf_mult:
(∞ * x = ∞) = (0 < x)
lemma negative_inf_mult:
(∞ * x = - ∞) = (x < 0)
lemma P_mult_infinity_neq_infinity_iff:
(P a * ∞ ≠ ∞) = (a ≤ (0::'a))
lemma P_mult_infinity_neq_MinusInfinity_iff:
(P a * ∞ ≠ - ∞) = ((0::'a) ≤ a)
lemma P_mult_MinusInfinity_neq_MinusInfinity_iff:
(P a * - ∞ ≠ - ∞) = (a ≤ (0::'a))
lemma P_mult_MinusInfinity_neq_infinity_iff:
(P a * - ∞ ≠ ∞) = ((0::'a) ≤ a)
lemma sgn_P:
sgn (P x) = (if x < (0::'a) then - 1 else if x = (0::'a) then 0 else 1)
lemma uminus_eq_iff:
(- x = x) = (x = (0::'a))
lemma sgn_P_eq_iff:
(sgn (P x) = sgn (P y)) = ((x < (0::'a)) = (y < (0::'a)) ∧ (x = (0::'a)) = (y = (0::'a)) ∧ ((0::'a) < x) = ((0::'a) < y))
lemma sgn_zero:
sgn 0 = 0
lemma sgn_infinity:
sgn (∞) = 1
lemma sgn_minus_infinity:
sgn (- ∞) = - 1
lemma sgn_zero_iff:
(sgn x = 0) = (x = 0)
lemma sgn_P_one_iff:
(sgn (P x) = 1) = ((0::'a) < x)
lemma sgn_P_minus_one_iff:
(sgn (P x) = - 1) = (x < (0::'a))
lemma P_eq_zero:
(P x = 0) = (x = (0::'a))
lemma distributivity:
¬ ((a = ∞ ∨ a = - ∞) ∧ sgn b ≠ sgn c ∧ b + c ∉ {0, Φ}) ==> a * (b + c) = a * b + a * c