src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy
 author nipkow Tue Feb 23 16:25:08 2016 +0100 (2016-02-23) changeset 62390 842917225d56 parent 60540 b7b71952c194 permissions -rw-r--r--
more canonical names
```     1 (* Author:     Amine Chaieb, TU Muenchen *)
```
```     2
```
```     3 section \<open>Examples for Ferrante and Rackoff's quantifier elimination procedure\<close>
```
```     4
```
```     5 theory Dense_Linear_Order_Ex
```
```     6 imports "../Dense_Linear_Order"
```
```     7 begin
```
```     8
```
```     9 lemma "\<exists>(y::'a::linordered_field) < 2. x + 3* y < 0 \<and> x - y > 0"
```
```    10   by ferrack
```
```    11
```
```    12 lemma "\<not> (\<forall>x (y::'a::linordered_field). x < y \<longrightarrow> 10 * x < 11 * y)"
```
```    13   by ferrack
```
```    14
```
```    15 lemma "\<forall>(x::'a::linordered_field) y. x < y \<longrightarrow> 10 * (x + 5 * y + -1) < 60 * y"
```
```    16   by ferrack
```
```    17
```
```    18 lemma "\<exists>(x::'a::linordered_field) y. x \<noteq> y \<longrightarrow> x < y"
```
```    19   by ferrack
```
```    20
```
```    21 lemma "\<exists>(x::'a::linordered_field) y. x \<noteq> y \<and> 10 * x \<noteq> 9 * y \<and> 10 * x < y \<longrightarrow> x < y"
```
```    22   by ferrack
```
```    23
```
```    24 lemma "\<forall>(x::'a::linordered_field) y. x \<noteq> y \<and> 5 * x \<le> y \<longrightarrow> 500 * x \<le> 100 * y"
```
```    25   by ferrack
```
```    26
```
```    27 lemma "\<forall>x::'a::linordered_field. \<exists>y::'a::linordered_field. 4 * x + 3 * y \<le> 0 \<and> 4 * x + 3 * y \<ge> -1"
```
```    28   by ferrack
```
```    29
```
```    30 lemma "\<forall>(x::'a::linordered_field) < 0. \<exists>(y::'a::linordered_field) > 0. 7 * x + y > 0 \<and> x - y \<le> 9"
```
```    31   by ferrack
```
```    32
```
```    33 lemma "\<exists>x::'a::linordered_field. 0 < x \<and> x < 1 \<longrightarrow> (\<forall>y > 1. x + y \<noteq> 1)"
```
```    34   by ferrack
```
```    35
```
```    36 lemma "\<exists>x. \<forall>y::'a::linordered_field. y < 2 \<longrightarrow> 2 * (y - x) \<le> 0"
```
```    37   by ferrack
```
```    38
```
```    39 lemma "\<forall>x::'a::linordered_field. x < 10 \<or> x > 20 \<or> (\<exists>y. y \<ge> 0 \<and> y \<le> 10 \<and> x + y = 20)"
```
```    40   by ferrack
```
```    41
```
```    42 lemma "\<forall>(x::'a::linordered_field) y z. x + y < z \<longrightarrow> y \<ge> z \<longrightarrow> x < 0"
```
```    43   by ferrack
```
```    44
```
```    45 lemma "\<exists>(x::'a::linordered_field) y z. x + 7 * y < 5 * z \<and> 5 * y \<ge> 7 * z \<and> x < 0"
```
```    46   by ferrack
```
```    47
```
```    48 lemma "\<forall>(x::'a::linordered_field) y z. \<bar>x + y\<bar> \<le> z \<longrightarrow> \<bar>z\<bar> = z"
```
```    49   by ferrack
```
```    50
```
```    51 lemma "\<exists>(x::'a::linordered_field) y z. x + 7 * y - 5 * z < 0 \<and> 5 * y + 7 * z + 3 * x < 0"
```
```    52   by ferrack
```
```    53
```
```    54 lemma "\<forall>(x::'a::linordered_field) y z.
```
```    55   (\<bar>5 * x + 3 * y + z\<bar> \<le> 5 * x + 3 * y + z \<and> \<bar>5 * x + 3 * y + z\<bar> \<ge> - (5 * x + 3 * y + z)) \<or>
```
```    56   (\<bar>5 * x + 3 * y + z\<bar> \<ge> 5 * x + 3 * y + z \<and> \<bar>5 * x + 3 * y + z\<bar> \<le> - (5 * x + 3 * y + z))"
```
```    57   by ferrack
```
```    58
```
```    59 lemma "\<forall>(x::'a::linordered_field) y. x < y \<longrightarrow> (\<exists>z>0. x + z = y)"
```
```    60   by ferrack
```
```    61
```
```    62 lemma "\<forall>(x::'a::linordered_field) y. x < y \<longrightarrow> (\<exists>z>0. x + z = y)"
```
```    63   by ferrack
```
```    64
```
```    65 lemma "\<forall>(x::'a::linordered_field) y. \<exists>z>0. \<bar>x - y\<bar> \<le> z"
```
```    66   by ferrack
```
```    67
```
```    68 lemma "\<exists>(x::'a::linordered_field) y. \<forall>z<0. (z < x \<longrightarrow> z \<le> y) \<and> (z > y \<longrightarrow> z \<ge> x)"
```
```    69   by ferrack
```
```    70
```
```    71 lemma "\<exists>(x::'a::linordered_field) y. \<forall>z\<ge>0. \<bar>3 * x + 7 * y\<bar> \<le> 2 * z + 1"
```
```    72   by ferrack
```
```    73
```
```    74 lemma "\<exists>(x::'a::linordered_field) y. \<forall>z<0. (z < x \<longrightarrow> z \<le> y) \<and> (z > y \<longrightarrow> z \<ge> x)"
```
```    75   by ferrack
```
```    76
```
```    77 lemma "\<exists>(x::'a::linordered_field) > 0. \<forall>y. \<exists>z. 13 * \<bar>z\<bar> \<noteq> \<bar>12 * y - x\<bar> \<and> 5 * x - 3 * \<bar>y\<bar> \<le> 7 * z"
```
```    78   by ferrack
```
```    79
```
```    80 lemma "\<exists>x::'a::linordered_field.
```
```    81   \<bar>4 * x + 17\<bar> < 4 \<and> (\<forall>y. \<bar>x * 34 - 34 * y - 9\<bar> \<noteq> 0 \<longrightarrow> (\<exists>z. 5 * x - 3 * \<bar>y\<bar> \<le> 7 * z))"
```
```    82   by ferrack
```
```    83
```
```    84 lemma "\<forall>x::'a::linordered_field. \<exists>y > \<bar>23 * x - 9\<bar>. \<forall>z > \<bar>3 * y - 19 * \<bar>x\<bar>\<bar>. x + z > 2 * y"
```
```    85   by ferrack
```
```    86
```
```    87 lemma "\<forall>x::'a::linordered_field.
```
```    88   \<exists>y < \<bar>3 * x - 1\<bar>. \<forall>z \<ge> 3 * \<bar>x\<bar> - 1. \<bar>12 * x - 13 * y + 19 * z\<bar> > \<bar>23 * x\<bar>"
```
```    89   by ferrack
```
```    90
```
```    91 lemma "\<exists>x::'a::linordered_field. \<bar>x\<bar> < 100 \<and> (\<forall>y > x. (\<exists>z < 2 * y - x. 5 * x - 3 * y \<le> 7 * z))"
```
```    92   by ferrack
```
```    93
```
```    94 lemma "\<forall>(x::'a::linordered_field) y z w.
```
```    95   7 * x < 3 * y \<longrightarrow> 5 * y < 7 * z \<longrightarrow> z < 2 * w \<longrightarrow> 7 * (2 * w - x) > 2 * y"
```
```    96   by ferrack
```
```    97
```
```    98 lemma "\<exists>(x::'a::linordered_field) y z w. 5 * x + 3 * z - 17 * w + \<bar>y - 8 * x + z\<bar> \<le> 89"
```
```    99   by ferrack
```
```   100
```
```   101 lemma "\<exists>(x::'a::linordered_field) y z w.
```
```   102   5 * x + 3 * z - 17 * w + 7 * (y - 8 * x + z) \<le> max y (7 * z - x + w)"
```
```   103   by ferrack
```
```   104
```
```   105 lemma "\<exists>(x::'a::linordered_field) y z w.
```
```   106   min (5 * x + 3 * z) (17 * w) + 5 * \<bar>y - 8 * x + z\<bar> \<le> max y (7 * z - x + w)"
```
```   107   by ferrack
```
```   108
```
```   109 lemma "\<forall>(x::'a::linordered_field) y z. \<exists>w \<ge> x + y + z. w \<le> \<bar>x\<bar> + \<bar>y\<bar> + \<bar>z\<bar>"
```
```   110   by ferrack
```
```   111
```
```   112 lemma "\<not> (\<forall>x::'a::linordered_field. \<exists>y z w.
```
```   113   3 * x + z * 4 = 3 * y \<and> x + y < z \<and> x > w \<and> 3 * x < w + y)"
```
```   114   by ferrack
```
```   115
```
```   116 lemma "\<forall>(x::'a::linordered_field) y. \<exists>z w. \<bar>x - y\<bar> = z - w \<and> z * 1234 < 233 * x \<and> w \<noteq> y"
```
```   117   by ferrack
```
```   118
```
```   119 lemma "\<forall>x::'a::linordered_field. \<exists>y z w.
```
```   120   min (5 * x + 3 * z) (17 * w) + 5 * \<bar>y - 8 * x + z\<bar> \<le> max y (7 * z - x + w)"
```
```   121   by ferrack
```
```   122
```
```   123 lemma "\<exists>(x::'a::linordered_field) y z. \<forall>w \<ge> \<bar>x + y + z\<bar>. w \<ge> \<bar>x\<bar> + \<bar>y\<bar> + \<bar>z\<bar>"
```
```   124   by ferrack
```
```   125
```
```   126 lemma "\<exists>z. \<forall>(x::'a::linordered_field) y. \<exists>w \<ge> x + y + z. w \<le> \<bar>x\<bar> + \<bar>y\<bar> + \<bar>z\<bar>"
```
```   127   by ferrack
```
```   128
```
```   129 lemma "\<exists>z. \<forall>(x::'a::linordered_field) < \<bar>z\<bar>. \<exists>y w. x < y \<and> x < z \<and> x > w \<and> 3 * x < w + y"
```
```   130   by ferrack
```
```   131
```
```   132 lemma "\<forall>(x::'a::linordered_field) y. \<exists>z. \<forall>w. \<bar>x - y\<bar> = \<bar>z - w\<bar> \<longrightarrow> z < x \<and> w \<noteq> y"
```
```   133   by ferrack
```
```   134
```
```   135 lemma "\<exists>y. \<forall>x::'a::linordered_field. \<exists>z w.
```
```   136   min (5 * x + 3 * z) (17 * w) + 5 * \<bar>y - 8 * x + z\<bar> \<le> max y (7 * z - x + w)"
```
```   137   by ferrack
```
```   138
```
```   139 lemma "\<exists>(x::'a::linordered_field) z. \<forall>w \<ge> 13 * x - 4 * z. \<exists>y. w \<ge> \<bar>x\<bar> + \<bar>y\<bar> + z"
```
```   140   by ferrack
```
```   141
```
```   142 lemma "\<exists>x::'a::linordered_field. \<forall>y < x. \<exists>z > x + y.
```
```   143   \<forall>w. 5 * w + 10 * x - z \<ge> y \<longrightarrow> w + 7 * x + 3 * z \<ge> 2 * y"
```
```   144   by ferrack
```
```   145
```
```   146 lemma "\<exists>x::'a::linordered_field. \<forall>y. \<exists>z > y.
```
```   147   \<forall>w. w < 13 \<longrightarrow> w + 10 * x - z \<ge> y \<longrightarrow> 5 * w + 7 * x + 13 * z \<ge> 2 * y"
```
```   148   by ferrack
```
```   149
```
```   150 lemma "\<exists>(x::'a::linordered_field) y z w.
```
```   151   min (5 * x + 3 * z) (17 * w) + 5 * \<bar>y - 8 * x + z\<bar> \<le> max y (7 * z - x + w)"
```
```   152   by ferrack
```
```   153
```
```   154 lemma "\<forall>x::'a::linordered_field. \<exists>y. \<forall>z>19. y \<le> x + z \<and> (\<exists>w. \<bar>y - x\<bar> < w)"
```
```   155   by ferrack
```
```   156
```
```   157 lemma "\<forall>x::'a::linordered_field. \<exists>y. \<forall>z>19. y \<le> x + z \<and> (\<exists>w. \<bar>x + z\<bar> < w - y)"
```
```   158   by ferrack
```
```   159
```
```   160 lemma "\<forall>x::'a::linordered_field. \<exists>y.
```
```   161   \<bar>y\<bar> \<noteq> \<bar>x\<bar> \<and> (\<forall>z > max x y. \<exists>w. w \<noteq> y \<and> w \<noteq> z \<and> 3 * w - z \<ge> x + y)"
```
```   162   by ferrack
```
```   163
```
```   164 end
```