Quelle  Dense_Linear_Order_Ex.thy   Sprache: Isabelle

(* Author:     Amine Chaieb, TU Muenchen *)

section ‹Examples for Ferrante and Rackoff's quantifier elimination procedure\

theory Dense_Linear_Order_Ex
imports "../Dense_Linear_Order"
begin

lemma "\(y::'a::linordered_field) < 2. x + 3* y < 0 \ x - y > 0"
  by ferrack

lemma "\ (\x (y::'a::linordered_field). x < y \ 10 * x < 11 * y)"
  by ferrack

lemma "\(x::'a::linordered_field) y. x < y \ 10 * (x + 5 * y + -1) < 60 * y"
  by ferrack

lemma "\(x::'a::linordered_field) y. x \ y \ x < y"
  by ferrack

lemma "\(x::'a::linordered_field) y. x \ y \ 10 * x \ 9 * y \ 10 * x < y \ x < y"
  by ferrack

lemma "\(x::'a::linordered_field) y. x \ y \ 5 * x \ y \ 500 * x \ 100 * y"
  by ferrack

lemma "\x::'a::linordered_field. \y::'a::linordered_field. 4 * x + 3 * y \ 0 \ 4 * x + 3 * y \ -1"
  by ferrack

lemma "\(x::'a::linordered_field) < 0. \(y::'a::linordered_field) > 0. 7 * x + y > 0 \ x - y \ 9"
  by ferrack

lemma "\x::'a::linordered_field. 0 < x \ x < 1 \ (\y > 1. x + y \ 1)"
  by ferrack

lemma "\x. \y::'a::linordered_field. y < 2 \ 2 * (y - x) \ 0"
  by ferrack

lemma "\x::'a::linordered_field. x < 10 \ x > 20 \ (\y. y \ 0 \ y \ 10 \ x + y = 20)"
  by ferrack

lemma "\(x::'a::linordered_field) y z. x + y < z \ y \ z \ x < 0"
  by ferrack

lemma "\(x::'a::linordered_field) y z. x + 7 * y < 5 * z \ 5 * y \ 7 * z \ x < 0"
  by ferrack

lemma "\(x::'a::linordered_field) y z. \x + y\ \ z \ \z\ = z"
  by ferrack

lemma "\(x::'a::linordered_field) y z. x + 7 * y - 5 * z < 0 \ 5 * y + 7 * z + 3 * x < 0"
  by ferrack

lemma "\(x::'a::linordered_field) y z.
  (∣5 * x + 3 * y + z∣ ≤ 5 * x + 3 * y + z ∧ ∣5 * x + 3 * y + z∣ ≥ - (5 * x + 3 * y + z)) ∨
  (∣5 * x + 3 * y + z∣ ≥ 5 * x + 3 * y + z ∧ ∣5 * x + 3 * y + z∣ ≤ - (5 * x + 3 * y + z))"
  by ferrack

lemma "\(x::'a::linordered_field) y. x < y \ (\z>0. x + z = y)"
  by ferrack

lemma "\(x::'a::linordered_field) y. x < y \ (\z>0. x + z = y)"
  by ferrack

lemma "\(x::'a::linordered_field) y. \z>0. \x - y\ \ z"
  by ferrack

lemma "\(x::'a::linordered_field) y. \z<0. (z < x \ z \ y) \ (z > y \ z \ x)"
  by ferrack

lemma "\(x::'a::linordered_field) y. \z\0. \3 * x + 7 * y\ \ 2 * z + 1"
  by ferrack

lemma "\(x::'a::linordered_field) y. \z<0. (z < x \ z \ y) \ (z > y \ z \ x)"
  by ferrack

lemma "\(x::'a::linordered_field) > 0. \y. \z. 13 * \z\ \ \12 * y - x\ \ 5 * x - 3 * \y\ \ 7 * z"
  by ferrack

lemma "\x::'a::linordered_field.
  ∣4 * x + 17∣ < 4 ∧ (∀y. ∣x * 34 - 34 * y - 9∣ ≠ 0 ⟶ (∃z. 5 * x - 3 * ∣y∣ ≤ 7 * z))"
  by ferrack

lemma "\x::'a::linordered_field. \y > \23 * x - 9\. \z > \3 * y - 19 * \x\\. x + z > 2 * y"
  by ferrack

lemma "\x::'a::linordered_field.
  ∃y < ∣3 * x - 1∣. ∀z ≥ 3 * ∣x∣ - 1. ∣12 * x - 13 * y + 19 * z∣ > ∣23 * x∣"
  by ferrack

lemma "\x::'a::linordered_field. \x\ < 100 \ (\y > x. (\z < 2 * y - x. 5 * x - 3 * y \ 7 * z))"
  by ferrack

lemma "\(x::'a::linordered_field) y z w.
  7 * x < 3 * y ⟶ 5 * y < 7 * z ⟶ z < 2 * w ⟶ 7 * (2 * w - x) > 2 * y"
  by ferrack

lemma "\(x::'a::linordered_field) y z w. 5 * x + 3 * z - 17 * w + \y - 8 * x + z\ \ 89"
  by ferrack

lemma "\(x::'a::linordered_field) y z w.
  5 * x + 3 * z - 17 * w + 7 * (y - 8 * x + z) ≤ max y (7 * z - x + w)"
  by ferrack

lemma "\(x::'a::linordered_field) y z w.
  min (5 * x + 3 * z) (17 * w) + 5 * ∣y - 8 * x + z∣ ≤ max y (7 * z - x + w)"
  by ferrack

lemma "\(x::'a::linordered_field) y z. \w \ x + y + z. w \ \x\ + \y\ + \z\"
  by ferrack

lemma "\ (\x::'a::linordered_field. \y z w.
  3 * x + z * 4 = 3 * y ∧ x + y < z ∧ x > w ∧ 3 * x < w + y)"
  by ferrack

lemma "\(x::'a::linordered_field) y. \z w. \x - y\ = z - w \ z * 1234 < 233 * x \ w \ y"
  by ferrack

lemma "\x::'a::linordered_field. \y z w.
  min (5 * x + 3 * z) (17 * w) + 5 * ∣y - 8 * x + z∣ ≤ max y (7 * z - x + w)"
  by ferrack

lemma "\(x::'a::linordered_field) y z. \w \ \x + y + z\. w \ \x\ + \y\ + \z\"
  by ferrack

lemma "\z. \(x::'a::linordered_field) y. \w \ x + y + z. w \ \x\ + \y\ + \z\"
  by ferrack

lemma "\z. \(x::'a::linordered_field) < \z\. \y w. x < y \ x < z \ x > w \ 3 * x < w + y"
  by ferrack

lemma "\(x::'a::linordered_field) y. \z. \w. \x - y\ = \z - w\ \ z < x \ w \ y"
  by ferrack

lemma "\y. \x::'a::linordered_field. \z w.
  min (5 * x + 3 * z) (17 * w) + 5 * ∣y - 8 * x + z∣ ≤ max y (7 * z - x + w)"
  by ferrack

lemma "\(x::'a::linordered_field) z. \w \ 13 * x - 4 * z. \y. w \ \x\ + \y\ + z"
  by ferrack

lemma "\x::'a::linordered_field. \y < x. \z > x + y.
  ∀w. 5 * w + 10 * x - z ≥ y ⟶ w + 7 * x + 3 * z ≥ 2 * y"
  by ferrack

lemma "\x::'a::linordered_field. \y. \z > y.
  ∀w. w < 13 ⟶ w + 10 * x - z ≥ y ⟶ 5 * w + 7 * x + 13 * z ≥ 2 * y"
  by ferrack

lemma "\(x::'a::linordered_field) y z w.
  min (5 * x + 3 * z) (17 * w) + 5 * ∣y - 8 * x + z∣ ≤ max y (7 * z - x + w)"
  by ferrack

lemma "\x::'a::linordered_field. \y. \z>19. y \ x + z \ (\w. \y - x\ < w)"
  by ferrack

lemma "\x::'a::linordered_field. \y. \z>19. y \ x + z \ (\w. \x + z\ < w - y)"
  by ferrack

lemma "\x::'a::linordered_field. \y.
  ∣y∣ ≠ ∣x∣ ∧ (∀z > max x y. ∃w. w ≠ y ∧ w ≠ z ∧ 3 * w - z ≥ x + y)"
  by ferrack

end