Quelle  Dense_Linear_Order_Ex.thy

(* 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