src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
author wenzelm
Wed, 26 Feb 2014 17:12:07 +0100
changeset 55768 72c6ce5aea2a
parent 55754 d14072d53c1e
child 56410 a14831ac3023
permissions -rw-r--r--
tuned specifications and proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
     1
(*  Title:      HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
     2
    Author:     Amine Chaieb
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
     3
*)
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
     4
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
     5
header{* A formalization of Ferrante and Rackoff's procedure with polynomial parameters, see Paper in CALCULEMUS 2008 *}
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
     6
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
     7
theory Parametric_Ferrante_Rackoff
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
     8
imports
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
     9
  Reflected_Multivariate_Polynomial
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    10
  Dense_Linear_Order
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    11
  DP_Library
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    12
  "~~/src/HOL/Library/Code_Target_Numeral"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    13
  "~~/src/HOL/Library/Old_Recdef"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
    14
begin
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
    15
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
    16
subsection {* Terms *}
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
    17
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    18
datatype tm = CP poly | Bound nat | Add tm tm | Mul poly tm
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
    19
  | Neg tm | Sub tm tm | CNP nat poly tm
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
    20
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    21
(* A size for poly to make inductive proofs simpler*)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    22
primrec tmsize :: "tm \<Rightarrow> nat"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    23
where
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
    24
  "tmsize (CP c) = polysize c"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
    25
| "tmsize (Bound n) = 1"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
    26
| "tmsize (Neg a) = 1 + tmsize a"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
    27
| "tmsize (Add a b) = 1 + tmsize a + tmsize b"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
    28
| "tmsize (Sub a b) = 3 + tmsize a + tmsize b"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
    29
| "tmsize (Mul c a) = 1 + polysize c + tmsize a"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
    30
| "tmsize (CNP n c a) = 3 + polysize c + tmsize a "
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
    31
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    32
(* Semantics of terms tm *)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    33
primrec Itm :: "'a::{field_char_0, field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    34
where
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
    35
  "Itm vs bs (CP c) = (Ipoly vs c)"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
    36
| "Itm vs bs (Bound n) = bs!n"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
    37
| "Itm vs bs (Neg a) = -(Itm vs bs a)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
    38
| "Itm vs bs (Add a b) = Itm vs bs a + Itm vs bs b"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
    39
| "Itm vs bs (Sub a b) = Itm vs bs a - Itm vs bs b"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
    40
| "Itm vs bs (Mul c a) = (Ipoly vs c) * Itm vs bs a"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    41
| "Itm vs bs (CNP n c t) = (Ipoly vs c)*(bs!n) + Itm vs bs t"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
    42
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    43
fun allpolys :: "(poly \<Rightarrow> bool) \<Rightarrow> tm \<Rightarrow> bool"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    44
where
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
    45
  "allpolys P (CP c) = P c"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
    46
| "allpolys P (CNP n c p) = (P c \<and> allpolys P p)"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
    47
| "allpolys P (Mul c p) = (P c \<and> allpolys P p)"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
    48
| "allpolys P (Neg p) = allpolys P p"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
    49
| "allpolys P (Add p q) = (allpolys P p \<and> allpolys P q)"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
    50
| "allpolys P (Sub p q) = (allpolys P p \<and> allpolys P q)"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
    51
| "allpolys P p = True"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
    52
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    53
primrec tmboundslt :: "nat \<Rightarrow> tm \<Rightarrow> bool"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    54
where
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
    55
  "tmboundslt n (CP c) = True"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
    56
| "tmboundslt n (Bound m) = (m < n)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
    57
| "tmboundslt n (CNP m c a) = (m < n \<and> tmboundslt n a)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
    58
| "tmboundslt n (Neg a) = tmboundslt n a"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
    59
| "tmboundslt n (Add a b) = (tmboundslt n a \<and> tmboundslt n b)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    60
| "tmboundslt n (Sub a b) = (tmboundslt n a \<and> tmboundslt n b)"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
    61
| "tmboundslt n (Mul i a) = tmboundslt n a"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
    62
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    63
primrec tmbound0 :: "tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound 0 *)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    64
where
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
    65
  "tmbound0 (CP c) = True"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
    66
| "tmbound0 (Bound n) = (n>0)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
    67
| "tmbound0 (CNP n c a) = (n\<noteq>0 \<and> tmbound0 a)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
    68
| "tmbound0 (Neg a) = tmbound0 a"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
    69
| "tmbound0 (Add a b) = (tmbound0 a \<and> tmbound0 b)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    70
| "tmbound0 (Sub a b) = (tmbound0 a \<and> tmbound0 b)"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
    71
| "tmbound0 (Mul i a) = tmbound0 a"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    72
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
    73
lemma tmbound0_I:
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
    74
  assumes nb: "tmbound0 a"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
    75
  shows "Itm vs (b#bs) a = Itm vs (b'#bs) a"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    76
  using nb
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    77
  by (induct a rule: tm.induct,auto)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
    78
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    79
primrec tmbound :: "nat \<Rightarrow> tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound n *)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    80
where
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
    81
  "tmbound n (CP c) = True"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
    82
| "tmbound n (Bound m) = (n \<noteq> m)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
    83
| "tmbound n (CNP m c a) = (n\<noteq>m \<and> tmbound n a)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
    84
| "tmbound n (Neg a) = tmbound n a"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
    85
| "tmbound n (Add a b) = (tmbound n a \<and> tmbound n b)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    86
| "tmbound n (Sub a b) = (tmbound n a \<and> tmbound n b)"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
    87
| "tmbound n (Mul i a) = tmbound n a"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    88
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    89
lemma tmbound0_tmbound_iff: "tmbound 0 t = tmbound0 t"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    90
  by (induct t) auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
    91
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    92
lemma tmbound_I:
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    93
  assumes bnd: "tmboundslt (length bs) t"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    94
    and nb: "tmbound n t"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    95
    and le: "n \<le> length bs"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
    96
  shows "Itm vs (bs[n:=x]) t = Itm vs bs t"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
    97
  using nb le bnd
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
    98
  by (induct t rule: tm.induct) auto
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
    99
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   100
fun decrtm0 :: "tm \<Rightarrow> tm"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   101
where
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   102
  "decrtm0 (Bound n) = Bound (n - 1)"
41821
c118ae98dfbf recdef -> fun
krauss
parents: 41816
diff changeset
   103
| "decrtm0 (Neg a) = Neg (decrtm0 a)"
c118ae98dfbf recdef -> fun
krauss
parents: 41816
diff changeset
   104
| "decrtm0 (Add a b) = Add (decrtm0 a) (decrtm0 b)"
c118ae98dfbf recdef -> fun
krauss
parents: 41816
diff changeset
   105
| "decrtm0 (Sub a b) = Sub (decrtm0 a) (decrtm0 b)"
c118ae98dfbf recdef -> fun
krauss
parents: 41816
diff changeset
   106
| "decrtm0 (Mul c a) = Mul c (decrtm0 a)"
c118ae98dfbf recdef -> fun
krauss
parents: 41816
diff changeset
   107
| "decrtm0 (CNP n c a) = CNP (n - 1) c (decrtm0 a)"
c118ae98dfbf recdef -> fun
krauss
parents: 41816
diff changeset
   108
| "decrtm0 a = a"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   109
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   110
fun incrtm0 :: "tm \<Rightarrow> tm"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   111
where
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   112
  "incrtm0 (Bound n) = Bound (n + 1)"
41821
c118ae98dfbf recdef -> fun
krauss
parents: 41816
diff changeset
   113
| "incrtm0 (Neg a) = Neg (incrtm0 a)"
c118ae98dfbf recdef -> fun
krauss
parents: 41816
diff changeset
   114
| "incrtm0 (Add a b) = Add (incrtm0 a) (incrtm0 b)"
c118ae98dfbf recdef -> fun
krauss
parents: 41816
diff changeset
   115
| "incrtm0 (Sub a b) = Sub (incrtm0 a) (incrtm0 b)"
c118ae98dfbf recdef -> fun
krauss
parents: 41816
diff changeset
   116
| "incrtm0 (Mul c a) = Mul c (incrtm0 a)"
c118ae98dfbf recdef -> fun
krauss
parents: 41816
diff changeset
   117
| "incrtm0 (CNP n c a) = CNP (n + 1) c (incrtm0 a)"
c118ae98dfbf recdef -> fun
krauss
parents: 41816
diff changeset
   118
| "incrtm0 a = a"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   119
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   120
lemma decrtm0:
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   121
  assumes nb: "tmbound0 t"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   122
  shows "Itm vs (x # bs) t = Itm vs bs (decrtm0 t)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   123
  using nb by (induct t rule: decrtm0.induct) simp_all
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   124
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   125
lemma incrtm0: "Itm vs (x#bs) (incrtm0 t) = Itm vs bs t"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   126
  by (induct t rule: decrtm0.induct) simp_all
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   127
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   128
primrec decrtm :: "nat \<Rightarrow> tm \<Rightarrow> tm"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   129
where
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   130
  "decrtm m (CP c) = (CP c)"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   131
| "decrtm m (Bound n) = (if n < m then Bound n else Bound (n - 1))"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   132
| "decrtm m (Neg a) = Neg (decrtm m a)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   133
| "decrtm m (Add a b) = Add (decrtm m a) (decrtm m b)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   134
| "decrtm m (Sub a b) = Sub (decrtm m a) (decrtm m b)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   135
| "decrtm m (Mul c a) = Mul c (decrtm m a)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   136
| "decrtm m (CNP n c a) = (if n < m then CNP n c (decrtm m a) else CNP (n - 1) c (decrtm m a))"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   137
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   138
primrec removen :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   139
where
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   140
  "removen n [] = []"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   141
| "removen n (x#xs) = (if n=0 then xs else (x#(removen (n - 1) xs)))"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   142
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   143
lemma removen_same: "n \<ge> length xs \<Longrightarrow> removen n xs = xs"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   144
  by (induct xs arbitrary: n) auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   145
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   146
lemma nth_length_exceeds: "n \<ge> length xs \<Longrightarrow> xs!n = []!(n - length xs)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   147
  by (induct xs arbitrary: n) auto
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   148
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   149
lemma removen_length:
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   150
  "length (removen n xs) = (if n \<ge> length xs then length xs else length xs - 1)"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   151
  by (induct xs arbitrary: n, auto)
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   152
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   153
lemma removen_nth:
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   154
  "(removen n xs)!m =
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   155
    (if n \<ge> length xs then xs!m
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   156
     else if m < n then xs!m
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   157
     else if m \<le> length xs then xs!(Suc m)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   158
     else []!(m - (length xs - 1)))"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   159
proof (induct xs arbitrary: n m)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   160
  case Nil
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   161
  then show ?case by simp
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   162
next
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   163
  case (Cons x xs n m)
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   164
  {
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   165
    assume nxs: "n \<ge> length (x#xs)"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   166
    then have ?case using removen_same[OF nxs] by simp
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   167
  }
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   168
  moreover
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   169
  {
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   170
    assume nxs: "\<not> (n \<ge> length (x#xs))"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   171
    {
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   172
      assume mln: "m < n"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   173
      then have ?case using Cons by (cases m) auto
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   174
    }
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   175
    moreover
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   176
    {
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   177
      assume mln: "\<not> (m < n)"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   178
      {
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   179
        assume mxs: "m \<le> length (x#xs)"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   180
        then have ?case using Cons by (cases m) auto
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   181
      }
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   182
      moreover
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   183
      {
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   184
        assume mxs: "\<not> (m \<le> length (x#xs))"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   185
        have th: "length (removen n (x#xs)) = length xs"
33268
02de0317f66f eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 33212
diff changeset
   186
          using removen_length[where n="n" and xs="x#xs"] nxs by simp
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   187
        with mxs have mxs':"m \<ge> length (removen n (x#xs))"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   188
          by auto
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   189
        then have "(removen n (x#xs))!m = [] ! (m - length xs)"
33268
02de0317f66f eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 33212
diff changeset
   190
          using th nth_length_exceeds[OF mxs'] by auto
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   191
        then have th: "(removen n (x#xs))!m = [] ! (m - (length (x#xs) - 1))"
33268
02de0317f66f eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 33212
diff changeset
   192
          by auto
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   193
        then have ?case
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   194
          using nxs mln mxs by auto
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   195
      }
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   196
      ultimately have ?case by blast
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   197
    }
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   198
    ultimately have ?case by blast
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   199
  }
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   200
  ultimately show ?case by blast
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   201
qed
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   202
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   203
lemma decrtm:
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   204
  assumes bnd: "tmboundslt (length bs) t"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   205
    and nb: "tmbound m t"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   206
    and nle: "m \<le> length bs"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   207
  shows "Itm vs (removen m bs) (decrtm m t) = Itm vs bs t"
41807
ab5d2d81f9fb tuned proofs -- eliminated prems;
wenzelm
parents: 41413
diff changeset
   208
  using bnd nb nle by (induct t rule: tm.induct) (auto simp add: removen_nth)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   209
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   210
primrec tmsubst0:: "tm \<Rightarrow> tm \<Rightarrow> tm"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   211
where
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   212
  "tmsubst0 t (CP c) = CP c"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   213
| "tmsubst0 t (Bound n) = (if n=0 then t else Bound n)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   214
| "tmsubst0 t (CNP n c a) = (if n=0 then Add (Mul c t) (tmsubst0 t a) else CNP n c (tmsubst0 t a))"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   215
| "tmsubst0 t (Neg a) = Neg (tmsubst0 t a)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   216
| "tmsubst0 t (Add a b) = Add (tmsubst0 t a) (tmsubst0 t b)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   217
| "tmsubst0 t (Sub a b) = Sub (tmsubst0 t a) (tmsubst0 t b)"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   218
| "tmsubst0 t (Mul i a) = Mul i (tmsubst0 t a)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   219
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   220
lemma tmsubst0: "Itm vs (x#bs) (tmsubst0 t a) = Itm vs ((Itm vs (x#bs) t)#bs) a"
41842
d8f76db6a207 added simp lemma nth_Cons_pos to List
nipkow
parents: 41838
diff changeset
   221
  by (induct a rule: tm.induct) auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   222
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   223
lemma tmsubst0_nb: "tmbound0 t \<Longrightarrow> tmbound0 (tmsubst0 t a)"
41842
d8f76db6a207 added simp lemma nth_Cons_pos to List
nipkow
parents: 41838
diff changeset
   224
  by (induct a rule: tm.induct) auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   225
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   226
primrec tmsubst:: "nat \<Rightarrow> tm \<Rightarrow> tm \<Rightarrow> tm"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   227
where
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   228
  "tmsubst n t (CP c) = CP c"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   229
| "tmsubst n t (Bound m) = (if n=m then t else Bound m)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   230
| "tmsubst n t (CNP m c a) =
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   231
    (if n = m then Add (Mul c t) (tmsubst n t a) else CNP m c (tmsubst n t a))"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   232
| "tmsubst n t (Neg a) = Neg (tmsubst n t a)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   233
| "tmsubst n t (Add a b) = Add (tmsubst n t a) (tmsubst n t b)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   234
| "tmsubst n t (Sub a b) = Sub (tmsubst n t a) (tmsubst n t b)"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   235
| "tmsubst n t (Mul i a) = Mul i (tmsubst n t a)"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   236
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   237
lemma tmsubst:
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   238
  assumes nb: "tmboundslt (length bs) a"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   239
    and nlt: "n \<le> length bs"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   240
  shows "Itm vs bs (tmsubst n t a) = Itm vs (bs[n:= Itm vs bs t]) a"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   241
  using nb nlt
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   242
  by (induct a rule: tm.induct) auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   243
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   244
lemma tmsubst_nb0:
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   245
  assumes tnb: "tmbound0 t"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   246
  shows "tmbound0 (tmsubst 0 t a)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   247
  using tnb
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   248
  by (induct a rule: tm.induct) auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   249
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   250
lemma tmsubst_nb:
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   251
  assumes tnb: "tmbound m t"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   252
  shows "tmbound m (tmsubst m t a)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   253
  using tnb
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   254
  by (induct a rule: tm.induct) auto
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   255
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   256
lemma incrtm0_tmbound: "tmbound n t \<Longrightarrow> tmbound (Suc n) (incrtm0 t)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   257
  by (induct t) auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   258
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   259
(* Simplification *)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   260
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   261
consts tmadd:: "tm \<times> tm \<Rightarrow> tm"
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   262
recdef tmadd "measure (\<lambda>(t,s). size t + size s)"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   263
  "tmadd (CNP n1 c1 r1,CNP n2 c2 r2) =
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   264
    (if n1 = n2 then
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   265
      let c = c1 +\<^sub>p c2
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   266
      in if c = 0\<^sub>p then tmadd(r1,r2) else CNP n1 c (tmadd (r1, r2))
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   267
    else if n1 \<le> n2 then (CNP n1 c1 (tmadd (r1,CNP n2 c2 r2)))
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   268
    else (CNP n2 c2 (tmadd (CNP n1 c1 r1, r2))))"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   269
  "tmadd (CNP n1 c1 r1, t) = CNP n1 c1 (tmadd (r1, t))"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   270
  "tmadd (t, CNP n2 c2 r2) = CNP n2 c2 (tmadd (t, r2))"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   271
  "tmadd (CP b1, CP b2) = CP (b1 +\<^sub>p b2)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   272
  "tmadd (a, b) = Add a b"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   273
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   274
lemma tmadd[simp]: "Itm vs bs (tmadd (t, s)) = Itm vs bs (Add t s)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   275
  apply (induct t s rule: tmadd.induct, simp_all add: Let_def)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   276
  apply (case_tac "c1 +\<^sub>p c2 = 0\<^sub>p",case_tac "n1 \<le> n2", simp_all)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   277
  apply (case_tac "n1 = n2", simp_all add: field_simps)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   278
  apply (simp only: distrib_left[symmetric])
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   279
  apply (auto simp del: polyadd simp add: polyadd[symmetric])
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   280
  done
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   281
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   282
lemma tmadd_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 s \<Longrightarrow> tmbound0 (tmadd (t, s))"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   283
  by (induct t s rule: tmadd.induct) (auto simp add: Let_def)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   284
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   285
lemma tmadd_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n s \<Longrightarrow> tmbound n (tmadd (t, s))"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   286
  by (induct t s rule: tmadd.induct) (auto simp add: Let_def)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   287
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   288
lemma tmadd_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n s \<Longrightarrow> tmboundslt n (tmadd (t, s))"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   289
  by (induct t s rule: tmadd.induct) (auto simp add: Let_def)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   290
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   291
lemma tmadd_allpolys_npoly[simp]:
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   292
  "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmadd(t, s))"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   293
  by (induct t s rule: tmadd.induct) (simp_all add: Let_def polyadd_norm)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   294
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   295
fun tmmul:: "tm \<Rightarrow> poly \<Rightarrow> tm"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   296
where
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   297
  "tmmul (CP j) = (\<lambda>i. CP (i *\<^sub>p j))"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   298
| "tmmul (CNP n c a) = (\<lambda>i. CNP n (i *\<^sub>p c) (tmmul a i))"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   299
| "tmmul t = (\<lambda>i. Mul i t)"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   300
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   301
lemma tmmul[simp]: "Itm vs bs (tmmul t i) = Itm vs bs (Mul i t)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   302
  by (induct t arbitrary: i rule: tmmul.induct) (simp_all add: field_simps)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   303
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   304
lemma tmmul_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 (tmmul t i)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   305
  by (induct t arbitrary: i rule: tmmul.induct) auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   306
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   307
lemma tmmul_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n (tmmul t i)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   308
  by (induct t arbitrary: n rule: tmmul.induct) auto
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   309
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   310
lemma tmmul_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n (tmmul t i)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   311
  by (induct t arbitrary: i rule: tmmul.induct) (auto simp add: Let_def)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   312
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   313
lemma tmmul_allpolys_npoly[simp]:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   314
  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   315
  shows "allpolys isnpoly t \<Longrightarrow> isnpoly c \<Longrightarrow> allpolys isnpoly (tmmul t c)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   316
  by (induct t rule: tmmul.induct) (simp_all add: Let_def polymul_norm)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   317
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   318
definition tmneg :: "tm \<Rightarrow> tm"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   319
  where "tmneg t \<equiv> tmmul t (C (- 1,1))"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   320
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   321
definition tmsub :: "tm \<Rightarrow> tm \<Rightarrow> tm"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   322
  where "tmsub s t \<equiv> (if s = t then CP 0\<^sub>p else tmadd (s, tmneg t))"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   323
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   324
lemma tmneg[simp]: "Itm vs bs (tmneg t) = Itm vs bs (Neg t)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   325
  using tmneg_def[of t] by simp
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   326
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   327
lemma tmneg_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 (tmneg t)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   328
  using tmneg_def by simp
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   329
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   330
lemma tmneg_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n (tmneg t)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   331
  using tmneg_def by simp
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   332
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   333
lemma tmneg_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n (tmneg t)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   334
  using tmneg_def by simp
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   335
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   336
lemma [simp]: "isnpoly (C (-1, 1))"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   337
  unfolding isnpoly_def by simp
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   338
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   339
lemma tmneg_allpolys_npoly[simp]:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   340
  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   341
  shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly (tmneg t)"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   342
  unfolding tmneg_def by auto
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   343
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   344
lemma tmsub[simp]: "Itm vs bs (tmsub a b) = Itm vs bs (Sub a b)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   345
  using tmsub_def by simp
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   346
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   347
lemma tmsub_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 s \<Longrightarrow> tmbound0 (tmsub t s)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   348
  using tmsub_def by simp
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   349
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   350
lemma tmsub_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n s \<Longrightarrow> tmbound n (tmsub t s)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   351
  using tmsub_def by simp
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   352
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   353
lemma tmsub_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n s \<Longrightarrow> tmboundslt n (tmsub t s)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   354
  using tmsub_def by simp
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   355
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   356
lemma tmsub_allpolys_npoly[simp]:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   357
  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   358
  shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmsub t s)"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   359
  unfolding tmsub_def by (simp add: isnpoly_def)
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   360
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   361
fun simptm :: "tm \<Rightarrow> tm"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   362
where
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   363
  "simptm (CP j) = CP (polynate j)"
50282
fe4d4bb9f4c2 more robust syntax that survives collapse of \<^isub> and \<^sub>;
wenzelm
parents: 50045
diff changeset
   364
| "simptm (Bound n) = CNP n (1)\<^sub>p (CP 0\<^sub>p)"
41821
c118ae98dfbf recdef -> fun
krauss
parents: 41816
diff changeset
   365
| "simptm (Neg t) = tmneg (simptm t)"
c118ae98dfbf recdef -> fun
krauss
parents: 41816
diff changeset
   366
| "simptm (Add t s) = tmadd (simptm t,simptm s)"
c118ae98dfbf recdef -> fun
krauss
parents: 41816
diff changeset
   367
| "simptm (Sub t s) = tmsub (simptm t) (simptm s)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   368
| "simptm (Mul i t) =
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   369
    (let i' = polynate i in if i' = 0\<^sub>p then CP 0\<^sub>p else tmmul (simptm t) i')"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   370
| "simptm (CNP n c t) =
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   371
    (let c' = polynate c in if c' = 0\<^sub>p then simptm t else tmadd (CNP n c' (CP 0\<^sub>p ), simptm t))"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   372
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   373
lemma polynate_stupid:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   374
  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
45499
849d697adf1e Parametric_Ferrante_Rackoff.thy: restrict to class number_ring, replace '1+1' with '2' everywhere
huffman
parents: 44064
diff changeset
   375
  shows "polynate t = 0\<^sub>p \<Longrightarrow> Ipoly bs t = (0::'a)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   376
  apply (subst polynate[symmetric])
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   377
  apply simp
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   378
  done
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   379
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   380
lemma simptm_ci[simp]: "Itm vs bs (simptm t) = Itm vs bs t"
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   381
  by (induct t rule: simptm.induct) (auto simp add: Let_def polynate_stupid)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   382
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   383
lemma simptm_tmbound0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 (simptm t)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   384
  by (induct t rule: simptm.induct) (auto simp add: Let_def)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   385
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   386
lemma simptm_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n (simptm t)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   387
  by (induct t rule: simptm.induct) (auto simp add: Let_def)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   388
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   389
lemma simptm_nlt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n (simptm t)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   390
  by (induct t rule: simptm.induct) (auto simp add: Let_def)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   391
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   392
lemma [simp]: "isnpoly 0\<^sub>p"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   393
  and [simp]: "isnpoly (C(1,1))"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   394
  by (simp_all add: isnpoly_def)
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   395
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   396
lemma simptm_allpolys_npoly[simp]:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   397
  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   398
  shows "allpolys isnpoly (simptm p)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   399
  by (induct p rule: simptm.induct) (auto simp add: Let_def)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   400
41822
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   401
declare let_cong[fundef_cong del]
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   402
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   403
fun split0 :: "tm \<Rightarrow> (poly \<times> tm)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   404
where
50282
fe4d4bb9f4c2 more robust syntax that survives collapse of \<^isub> and \<^sub>;
wenzelm
parents: 50045
diff changeset
   405
  "split0 (Bound 0) = ((1)\<^sub>p, CP 0\<^sub>p)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   406
| "split0 (CNP 0 c t) = (let (c', t') = split0 t in (c +\<^sub>p c', t'))"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   407
| "split0 (Neg t) = (let (c, t') = split0 t in (~\<^sub>p c, Neg t'))"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   408
| "split0 (CNP n c t) = (let (c', t') = split0 t in (c', CNP n c t'))"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   409
| "split0 (Add s t) = (let (c1, s') = split0 s; (c2, t') = split0 t in (c1 +\<^sub>p c2, Add s' t'))"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   410
| "split0 (Sub s t) = (let (c1, s') = split0 s; (c2, t') = split0 t in (c1 -\<^sub>p c2, Sub s' t'))"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   411
| "split0 (Mul c t) = (let (c', t') = split0 t in (c *\<^sub>p c', Mul c t'))"
41822
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   412
| "split0 t = (0\<^sub>p, t)"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   413
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   414
declare let_cong[fundef_cong]
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   415
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   416
lemma split0_stupid[simp]: "\<exists>x y. (x, y) = split0 p"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   417
  apply (rule exI[where x="fst (split0 p)"])
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   418
  apply (rule exI[where x="snd (split0 p)"])
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   419
  apply simp
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   420
  done
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   421
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   422
lemma split0:
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   423
  "tmbound 0 (snd (split0 t)) \<and> (Itm vs bs (CNP 0 (fst (split0 t)) (snd (split0 t))) = Itm vs bs t)"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   424
  apply (induct t rule: split0.induct)
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   425
  apply simp
36348
89c54f51f55a dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents: 35625
diff changeset
   426
  apply (simp add: Let_def split_def field_simps)
89c54f51f55a dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents: 35625
diff changeset
   427
  apply (simp add: Let_def split_def field_simps)
89c54f51f55a dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents: 35625
diff changeset
   428
  apply (simp add: Let_def split_def field_simps)
89c54f51f55a dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents: 35625
diff changeset
   429
  apply (simp add: Let_def split_def field_simps)
89c54f51f55a dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents: 35625
diff changeset
   430
  apply (simp add: Let_def split_def field_simps)
49962
a8cc904a6820 Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents: 48562
diff changeset
   431
  apply (simp add: Let_def split_def mult_assoc distrib_left[symmetric])
36348
89c54f51f55a dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents: 35625
diff changeset
   432
  apply (simp add: Let_def split_def field_simps)
89c54f51f55a dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents: 35625
diff changeset
   433
  apply (simp add: Let_def split_def field_simps)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   434
  done
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   435
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   436
lemma split0_ci: "split0 t = (c',t') \<Longrightarrow> Itm vs bs t = Itm vs bs (CNP 0 c' t')"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   437
proof -
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   438
  fix c' t'
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   439
  assume "split0 t = (c', t')"
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   440
  then have "c' = fst (split0 t)" and "t' = snd (split0 t)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   441
    by auto
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   442
  with split0[where t="t" and bs="bs"]
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   443
  show "Itm vs bs t = Itm vs bs (CNP 0 c' t')"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   444
    by simp
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   445
qed
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   446
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   447
lemma split0_nb0:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   448
  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   449
  shows "split0 t = (c',t') \<Longrightarrow>  tmbound 0 t'"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   450
proof -
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   451
  fix c' t'
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   452
  assume "split0 t = (c', t')"
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   453
  then have "c' = fst (split0 t)" and "t' = snd (split0 t)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   454
    by auto
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   455
  with conjunct1[OF split0[where t="t"]] show "tmbound 0 t'"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   456
    by simp
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   457
qed
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   458
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   459
lemma split0_nb0'[simp]:
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   460
  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   461
  shows "tmbound0 (snd (split0 t))"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   462
  using split0_nb0[of t "fst (split0 t)" "snd (split0 t)"]
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   463
  by (simp add: tmbound0_tmbound_iff)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   464
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   465
lemma split0_nb:
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   466
  assumes nb: "tmbound n t"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   467
  shows "tmbound n (snd (split0 t))"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   468
  using nb by (induct t rule: split0.induct) (auto simp add: Let_def split_def)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   469
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   470
lemma split0_blt:
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   471
  assumes nb: "tmboundslt n t"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   472
  shows "tmboundslt n (snd (split0 t))"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   473
  using nb by (induct t rule: split0.induct) (auto simp add: Let_def split_def)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   474
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   475
lemma tmbound_split0: "tmbound 0 t \<Longrightarrow> Ipoly vs (fst (split0 t)) = 0"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   476
  by (induct t rule: split0.induct) (auto simp add: Let_def split_def)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   477
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   478
lemma tmboundslt_split0: "tmboundslt n t \<Longrightarrow> Ipoly vs (fst (split0 t)) = 0 \<or> n > 0"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   479
  by (induct t rule: split0.induct) (auto simp add: Let_def split_def)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   480
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   481
lemma tmboundslt0_split0: "tmboundslt 0 t \<Longrightarrow> Ipoly vs (fst (split0 t)) = 0"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   482
  by (induct t rule: split0.induct) (auto simp add: Let_def split_def)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   483
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   484
lemma allpolys_split0: "allpolys isnpoly p \<Longrightarrow> allpolys isnpoly (snd (split0 p))"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   485
  by (induct p rule: split0.induct) (auto simp  add: isnpoly_def Let_def split_def)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   486
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   487
lemma isnpoly_fst_split0:
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   488
  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   489
  shows "allpolys isnpoly p \<Longrightarrow> isnpoly (fst (split0 p))"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   490
  by (induct p rule: split0.induct)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   491
    (auto simp  add: polyadd_norm polysub_norm polyneg_norm polymul_norm Let_def split_def)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   492
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   493
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   494
subsection{* Formulae *}
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   495
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   496
datatype fm  =  T| F| Le tm | Lt tm | Eq tm | NEq tm|
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   497
  NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   498
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   499
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   500
(* A size for fm *)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   501
fun fmsize :: "fm \<Rightarrow> nat"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   502
where
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   503
  "fmsize (NOT p) = 1 + fmsize p"
41822
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   504
| "fmsize (And p q) = 1 + fmsize p + fmsize q"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   505
| "fmsize (Or p q) = 1 + fmsize p + fmsize q"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   506
| "fmsize (Imp p q) = 3 + fmsize p + fmsize q"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   507
| "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   508
| "fmsize (E p) = 1 + fmsize p"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   509
| "fmsize (A p) = 4+ fmsize p"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   510
| "fmsize p = 1"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   511
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   512
(* several lemmas about fmsize *)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   513
lemma fmsize_pos[termination_simp]: "fmsize p > 0"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   514
  by (induct p rule: fmsize.induct) simp_all
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   515
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   516
  (* Semantics of formulae (fm) *)
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   517
primrec Ifm ::"'a::{linordered_field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   518
where
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   519
  "Ifm vs bs T = True"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   520
| "Ifm vs bs F = False"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   521
| "Ifm vs bs (Lt a) = (Itm vs bs a < 0)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   522
| "Ifm vs bs (Le a) = (Itm vs bs a \<le> 0)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   523
| "Ifm vs bs (Eq a) = (Itm vs bs a = 0)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   524
| "Ifm vs bs (NEq a) = (Itm vs bs a \<noteq> 0)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   525
| "Ifm vs bs (NOT p) = (\<not> (Ifm vs bs p))"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   526
| "Ifm vs bs (And p q) = (Ifm vs bs p \<and> Ifm vs bs q)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   527
| "Ifm vs bs (Or p q) = (Ifm vs bs p \<or> Ifm vs bs q)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   528
| "Ifm vs bs (Imp p q) = ((Ifm vs bs p) \<longrightarrow> (Ifm vs bs q))"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   529
| "Ifm vs bs (Iff p q) = (Ifm vs bs p = Ifm vs bs q)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   530
| "Ifm vs bs (E p) = (\<exists>x. Ifm vs (x#bs) p)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   531
| "Ifm vs bs (A p) = (\<forall>x. Ifm vs (x#bs) p)"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   532
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   533
fun not:: "fm \<Rightarrow> fm"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   534
where
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   535
  "not (NOT (NOT p)) = not p"
41822
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   536
| "not (NOT p) = p"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   537
| "not T = F"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   538
| "not F = T"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   539
| "not (Lt t) = Le (tmneg t)"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   540
| "not (Le t) = Lt (tmneg t)"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   541
| "not (Eq t) = NEq t"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   542
| "not (NEq t) = Eq t"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   543
| "not p = NOT p"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   544
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   545
lemma not[simp]: "Ifm vs bs (not p) = Ifm vs bs (NOT p)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   546
  by (induct p rule: not.induct) auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   547
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   548
definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   549
where
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   550
  "conj p q \<equiv>
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   551
    (if p = F \<or> q = F then F
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   552
     else if p = T then q
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   553
     else if q = T then p
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   554
     else if p = q then p
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   555
     else And p q)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   556
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   557
lemma conj[simp]: "Ifm vs bs (conj p q) = Ifm vs bs (And p q)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   558
  by (cases "p=F \<or> q=F", simp_all add: conj_def) (cases p, simp_all)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   559
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   560
definition disj :: "fm \<Rightarrow> fm \<Rightarrow> fm"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   561
where
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   562
  "disj p q \<equiv>
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   563
    (if (p = T \<or> q = T) then T
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   564
     else if p = F then q
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   565
     else if q = F then p
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   566
     else if p = q then p
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   567
     else Or p q)"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   568
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   569
lemma disj[simp]: "Ifm vs bs (disj p q) = Ifm vs bs (Or p q)"
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   570
  by (cases "p = T \<or> q = T", simp_all add: disj_def) (cases p, simp_all)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   571
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   572
definition imp :: "fm \<Rightarrow> fm \<Rightarrow> fm"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   573
where
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   574
  "imp p q \<equiv>
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   575
    (if p = F \<or> q = T \<or> p = q then T
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   576
     else if p = T then q
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   577
     else if q = F then not p
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   578
     else Imp p q)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   579
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   580
lemma imp[simp]: "Ifm vs bs (imp p q) = Ifm vs bs (Imp p q)"
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   581
  by (cases "p = F \<or> q = T") (simp_all add: imp_def)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   582
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   583
definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   584
where
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   585
  "iff p q \<equiv>
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   586
   (if p = q then T
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   587
    else if p = NOT q \<or> NOT p = q then F
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   588
    else if p = F then not q
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   589
    else if q = F then not p
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   590
    else if p = T then q
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   591
    else if q = T then p
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   592
    else Iff p q)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   593
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   594
lemma iff[simp]: "Ifm vs bs (iff p q) = Ifm vs bs (Iff p q)"
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   595
  by (unfold iff_def, cases "p = q", simp, cases "p = NOT q", simp) (cases "NOT p= q", auto)
41822
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   596
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   597
(* Quantifier freeness *)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   598
fun qfree:: "fm \<Rightarrow> bool"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   599
where
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   600
  "qfree (E p) = False"
41822
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   601
| "qfree (A p) = False"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   602
| "qfree (NOT p) = qfree p"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   603
| "qfree (And p q) = (qfree p \<and> qfree q)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   604
| "qfree (Or  p q) = (qfree p \<and> qfree q)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   605
| "qfree (Imp p q) = (qfree p \<and> qfree q)"
41822
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   606
| "qfree (Iff p q) = (qfree p \<and> qfree q)"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   607
| "qfree p = True"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   608
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   609
(* Boundedness and substitution *)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   610
primrec boundslt :: "nat \<Rightarrow> fm \<Rightarrow> bool"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   611
where
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   612
  "boundslt n T = True"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   613
| "boundslt n F = True"
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   614
| "boundslt n (Lt t) = tmboundslt n t"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   615
| "boundslt n (Le t) = tmboundslt n t"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   616
| "boundslt n (Eq t) = tmboundslt n t"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   617
| "boundslt n (NEq t) = tmboundslt n t"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   618
| "boundslt n (NOT p) = boundslt n p"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   619
| "boundslt n (And p q) = (boundslt n p \<and> boundslt n q)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   620
| "boundslt n (Or p q) = (boundslt n p \<and> boundslt n q)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   621
| "boundslt n (Imp p q) = ((boundslt n p) \<and> (boundslt n q))"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   622
| "boundslt n (Iff p q) = (boundslt n p \<and> boundslt n q)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   623
| "boundslt n (E p) = boundslt (Suc n) p"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   624
| "boundslt n (A p) = boundslt (Suc n) p"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   625
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   626
fun bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   627
where
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   628
  "bound0 T = True"
41822
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   629
| "bound0 F = True"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   630
| "bound0 (Lt a) = tmbound0 a"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   631
| "bound0 (Le a) = tmbound0 a"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   632
| "bound0 (Eq a) = tmbound0 a"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   633
| "bound0 (NEq a) = tmbound0 a"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   634
| "bound0 (NOT p) = bound0 p"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   635
| "bound0 (And p q) = (bound0 p \<and> bound0 q)"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   636
| "bound0 (Or p q) = (bound0 p \<and> bound0 q)"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   637
| "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   638
| "bound0 (Iff p q) = (bound0 p \<and> bound0 q)"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   639
| "bound0 p = False"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   640
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   641
lemma bound0_I:
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   642
  assumes bp: "bound0 p"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   643
  shows "Ifm vs (b#bs) p = Ifm vs (b'#bs) p"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   644
  using bp tmbound0_I[where b="b" and bs="bs" and b'="b'"]
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   645
  by (induct p rule: bound0.induct) auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   646
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   647
primrec bound:: "nat \<Rightarrow> fm \<Rightarrow> bool" (* A Formula is independent of Bound n *)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   648
where
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   649
  "bound m T = True"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   650
| "bound m F = True"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   651
| "bound m (Lt t) = tmbound m t"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   652
| "bound m (Le t) = tmbound m t"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   653
| "bound m (Eq t) = tmbound m t"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   654
| "bound m (NEq t) = tmbound m t"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   655
| "bound m (NOT p) = bound m p"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   656
| "bound m (And p q) = (bound m p \<and> bound m q)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   657
| "bound m (Or p q) = (bound m p \<and> bound m q)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   658
| "bound m (Imp p q) = ((bound m p) \<and> (bound m q))"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   659
| "bound m (Iff p q) = (bound m p \<and> bound m q)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   660
| "bound m (E p) = bound (Suc m) p"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   661
| "bound m (A p) = bound (Suc m) p"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   662
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   663
lemma bound_I:
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   664
  assumes bnd: "boundslt (length bs) p"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   665
    and nb: "bound n p"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   666
    and le: "n \<le> length bs"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   667
  shows "Ifm vs (bs[n:=x]) p = Ifm vs bs p"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   668
  using bnd nb le tmbound_I[where bs=bs and vs = vs]
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   669
proof (induct p arbitrary: bs n rule: fm.induct)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   670
  case (E p bs n)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   671
  {
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   672
    fix y
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   673
    from E have bnd: "boundslt (length (y#bs)) p"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   674
      and nb: "bound (Suc n) p" and le: "Suc n \<le> length (y#bs)" by simp+
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   675
    from E.hyps[OF bnd nb le tmbound_I] have "Ifm vs ((y#bs)[Suc n:=x]) p = Ifm vs (y#bs) p" .
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   676
  }
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   677
  then show ?case by simp
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   678
next
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   679
  case (A p bs n)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   680
  {
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   681
    fix y
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   682
    from A have bnd: "boundslt (length (y#bs)) p"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   683
      and nb: "bound (Suc n) p"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   684
      and le: "Suc n \<le> length (y#bs)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   685
      by simp_all
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   686
    from A.hyps[OF bnd nb le tmbound_I] have "Ifm vs ((y#bs)[Suc n:=x]) p = Ifm vs (y#bs) p" .
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   687
  }
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   688
  then show ?case by simp
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   689
qed auto
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   690
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   691
fun decr0 :: "fm \<Rightarrow> fm"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   692
where
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   693
  "decr0 (Lt a) = Lt (decrtm0 a)"
41822
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   694
| "decr0 (Le a) = Le (decrtm0 a)"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   695
| "decr0 (Eq a) = Eq (decrtm0 a)"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   696
| "decr0 (NEq a) = NEq (decrtm0 a)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   697
| "decr0 (NOT p) = NOT (decr0 p)"
41822
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   698
| "decr0 (And p q) = conj (decr0 p) (decr0 q)"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   699
| "decr0 (Or p q) = disj (decr0 p) (decr0 q)"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   700
| "decr0 (Imp p q) = imp (decr0 p) (decr0 q)"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   701
| "decr0 (Iff p q) = iff (decr0 p) (decr0 q)"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   702
| "decr0 p = p"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   703
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   704
lemma decr0:
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   705
  assumes nb: "bound0 p"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   706
  shows "Ifm vs (x#bs) p = Ifm vs bs (decr0 p)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   707
  using nb
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   708
  by (induct p rule: decr0.induct) (simp_all add: decrtm0)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   709
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   710
primrec decr :: "nat \<Rightarrow> fm \<Rightarrow> fm"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   711
where
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   712
  "decr m T = T"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   713
| "decr m F = F"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   714
| "decr m (Lt t) = (Lt (decrtm m t))"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   715
| "decr m (Le t) = (Le (decrtm m t))"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   716
| "decr m (Eq t) = (Eq (decrtm m t))"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   717
| "decr m (NEq t) = (NEq (decrtm m t))"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   718
| "decr m (NOT p) = NOT (decr m p)"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   719
| "decr m (And p q) = conj (decr m p) (decr m q)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   720
| "decr m (Or p q) = disj (decr m p) (decr m q)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   721
| "decr m (Imp p q) = imp (decr m p) (decr m q)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   722
| "decr m (Iff p q) = iff (decr m p) (decr m q)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   723
| "decr m (E p) = E (decr (Suc m) p)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   724
| "decr m (A p) = A (decr (Suc m) p)"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   725
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   726
lemma decr:
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   727
  assumes bnd: "boundslt (length bs) p"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   728
    and nb: "bound m p"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   729
    and nle: "m < length bs"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   730
  shows "Ifm vs (removen m bs) (decr m p) = Ifm vs bs p"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   731
  using bnd nb nle
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   732
proof (induct p arbitrary: bs m rule: fm.induct)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   733
  case (E p bs m)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   734
  { fix x
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   735
    from E
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   736
    have bnd: "boundslt (length (x#bs)) p"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   737
      and nb: "bound (Suc m) p"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   738
      and nle: "Suc m < length (x#bs)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   739
      by auto
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   740
    from E(1)[OF bnd nb nle]
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   741
    have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p" .
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   742
  }
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   743
  then show ?case by auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   744
next
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   745
  case (A p bs m)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   746
  { fix x
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   747
    from A
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   748
    have bnd: "boundslt (length (x#bs)) p"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   749
      and nb: "bound (Suc m) p"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   750
      and nle: "Suc m < length (x#bs)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   751
      by auto
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   752
    from A(1)[OF bnd nb nle]
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   753
    have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p" .
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   754
  }
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   755
  then show ?case by auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   756
qed (auto simp add: decrtm removen_nth)
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   757
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   758
primrec subst0 :: "tm \<Rightarrow> fm \<Rightarrow> fm"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   759
where
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   760
  "subst0 t T = T"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   761
| "subst0 t F = F"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   762
| "subst0 t (Lt a) = Lt (tmsubst0 t a)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   763
| "subst0 t (Le a) = Le (tmsubst0 t a)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   764
| "subst0 t (Eq a) = Eq (tmsubst0 t a)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   765
| "subst0 t (NEq a) = NEq (tmsubst0 t a)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   766
| "subst0 t (NOT p) = NOT (subst0 t p)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   767
| "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   768
| "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   769
| "subst0 t (Imp p q) = Imp (subst0 t p)  (subst0 t q)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   770
| "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   771
| "subst0 t (E p) = E p"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   772
| "subst0 t (A p) = A p"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   773
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   774
lemma subst0:
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   775
  assumes qf: "qfree p"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   776
  shows "Ifm vs (x # bs) (subst0 t p) = Ifm vs ((Itm vs (x # bs) t) # bs) p"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   777
  using qf tmsubst0[where x="x" and bs="bs" and t="t"]
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   778
  by (induct p rule: fm.induct) auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   779
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   780
lemma subst0_nb:
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   781
  assumes bp: "tmbound0 t"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   782
    and qf: "qfree p"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   783
  shows "bound0 (subst0 t p)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   784
  using qf tmsubst0_nb[OF bp] bp
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   785
  by (induct p rule: fm.induct) auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   786
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   787
primrec subst:: "nat \<Rightarrow> tm \<Rightarrow> fm \<Rightarrow> fm"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   788
where
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   789
  "subst n t T = T"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   790
| "subst n t F = F"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   791
| "subst n t (Lt a) = Lt (tmsubst n t a)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   792
| "subst n t (Le a) = Le (tmsubst n t a)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   793
| "subst n t (Eq a) = Eq (tmsubst n t a)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   794
| "subst n t (NEq a) = NEq (tmsubst n t a)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   795
| "subst n t (NOT p) = NOT (subst n t p)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   796
| "subst n t (And p q) = And (subst n t p) (subst n t q)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   797
| "subst n t (Or p q) = Or (subst n t p) (subst n t q)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   798
| "subst n t (Imp p q) = Imp (subst n t p)  (subst n t q)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   799
| "subst n t (Iff p q) = Iff (subst n t p) (subst n t q)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   800
| "subst n t (E p) = E (subst (Suc n) (incrtm0 t) p)"
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   801
| "subst n t (A p) = A (subst (Suc n) (incrtm0 t) p)"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   802
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   803
lemma subst:
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   804
  assumes nb: "boundslt (length bs) p"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   805
    and nlm: "n \<le> length bs"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   806
  shows "Ifm vs bs (subst n t p) = Ifm vs (bs[n:= Itm vs bs t]) p"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   807
  using nb nlm
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38864
diff changeset
   808
proof (induct p arbitrary: bs n t rule: fm.induct)
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   809
  case (E p bs n)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   810
  {
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   811
    fix x
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   812
    from E have bn: "boundslt (length (x#bs)) p"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   813
      by simp
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   814
    from E have nlm: "Suc n \<le> length (x#bs)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   815
      by simp
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   816
    from E(1)[OF bn nlm]
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   817
    have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) =
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   818
        Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   819
      by simp
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   820
    then have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) =
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   821
        Ifm vs (x#bs[n:= Itm vs bs t]) p"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   822
      by (simp add: incrtm0[where x="x" and bs="bs" and t="t"])
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   823
  }
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   824
  then show ?case by simp
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   825
next
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   826
  case (A p bs n)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   827
  {
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   828
    fix x
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   829
    from A have bn: "boundslt (length (x#bs)) p"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   830
      by simp
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   831
    from A have nlm: "Suc n \<le> length (x#bs)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   832
      by simp
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   833
    from A(1)[OF bn nlm]
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   834
    have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) =
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   835
        Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   836
      by simp
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   837
    then have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) =
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   838
        Ifm vs (x#bs[n:= Itm vs bs t]) p"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   839
      by (simp add: incrtm0[where x="x" and bs="bs" and t="t"])
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   840
  }
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   841
  then show ?case by simp
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   842
qed (auto simp add: tmsubst)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   843
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   844
lemma subst_nb:
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   845
  assumes tnb: "tmbound m t"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   846
  shows "bound m (subst m t p)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   847
  using tnb tmsubst_nb incrtm0_tmbound
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   848
  by (induct p arbitrary: m t rule: fm.induct) auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   849
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   850
lemma not_qf[simp]: "qfree p \<Longrightarrow> qfree (not p)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   851
  by (induct p rule: not.induct) auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   852
lemma not_bn0[simp]: "bound0 p \<Longrightarrow> bound0 (not p)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   853
  by (induct p rule: not.induct) auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   854
lemma not_nb[simp]: "bound n p \<Longrightarrow> bound n (not p)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   855
  by (induct p rule: not.induct) auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   856
lemma not_blt[simp]: "boundslt n p \<Longrightarrow> boundslt n (not p)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   857
  by (induct p rule: not.induct) auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   858
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   859
lemma conj_qf[simp]: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (conj p q)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   860
  using conj_def by auto
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   861
lemma conj_nb0[simp]: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (conj p q)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   862
  using conj_def by auto
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   863
lemma conj_nb[simp]: "bound n p \<Longrightarrow> bound n q \<Longrightarrow> bound n (conj p q)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   864
  using conj_def by auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   865
lemma conj_blt[simp]: "boundslt n p \<Longrightarrow> boundslt n q \<Longrightarrow> boundslt n (conj p q)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   866
  using conj_def by auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   867
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   868
lemma disj_qf[simp]: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (disj p q)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   869
  using disj_def by auto
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   870
lemma disj_nb0[simp]: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (disj p q)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   871
  using disj_def by auto
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   872
lemma disj_nb[simp]: "bound n p \<Longrightarrow> bound n q \<Longrightarrow> bound n (disj p q)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   873
  using disj_def by auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   874
lemma disj_blt[simp]: "boundslt n p \<Longrightarrow> boundslt n q \<Longrightarrow> boundslt n (disj p q)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   875
  using disj_def by auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   876
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   877
lemma imp_qf[simp]: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (imp p q)"
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   878
  using imp_def by (cases "p = F \<or> q = T") (simp_all add: imp_def)
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   879
lemma imp_nb0[simp]: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (imp p q)"
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   880
  using imp_def by (cases "p = F \<or> q = T \<or> p = q") (simp_all add: imp_def)
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   881
lemma imp_nb[simp]: "bound n p \<Longrightarrow> bound n q \<Longrightarrow> bound n (imp p q)"
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   882
  using imp_def by (cases "p = F \<or> q = T \<or> p = q") (simp_all add: imp_def)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   883
lemma imp_blt[simp]: "boundslt n p \<Longrightarrow> boundslt n q \<Longrightarrow> boundslt n (imp p q)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   884
  using imp_def by auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   885
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   886
lemma iff_qf[simp]: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (iff p q)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   887
  unfolding iff_def by (cases "p = q") auto
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   888
lemma iff_nb0[simp]: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (iff p q)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   889
  using iff_def unfolding iff_def by (cases "p = q") auto
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   890
lemma iff_nb[simp]: "bound n p \<Longrightarrow> bound n q \<Longrightarrow> bound n (iff p q)"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   891
  using iff_def unfolding iff_def by (cases "p = q") auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   892
lemma iff_blt[simp]: "boundslt n p \<Longrightarrow> boundslt n q \<Longrightarrow> boundslt n (iff p q)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   893
  using iff_def by auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   894
lemma decr0_qf: "bound0 p \<Longrightarrow> qfree (decr0 p)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   895
  by (induct p) simp_all
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   896
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   897
fun isatom :: "fm \<Rightarrow> bool" (* test for atomicity *)
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   898
where
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   899
  "isatom T = True"
41822
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   900
| "isatom F = True"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   901
| "isatom (Lt a) = True"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   902
| "isatom (Le a) = True"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   903
| "isatom (Eq a) = True"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   904
| "isatom (NEq a) = True"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   905
| "isatom p = False"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   906
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   907
lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   908
  by (induct p) simp_all
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   909
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   910
definition djf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   911
where
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   912
  "djf f p q \<equiv>
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   913
    (if q = T then T
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   914
     else if q = F then f p
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   915
     else (let fp = f p in case fp of T \<Rightarrow> T | F \<Rightarrow> q | _ \<Rightarrow> Or (f p) q))"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   916
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   917
definition evaldjf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   918
  where "evaldjf f ps \<equiv> foldr (djf f) ps F"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   919
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   920
lemma djf_Or: "Ifm vs bs (djf f p q) = Ifm vs bs (Or (f p) q)"
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   921
  by (cases "q=T", simp add: djf_def,cases "q=F", simp add: djf_def)
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   922
    (cases "f p", simp_all add: Let_def djf_def)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   923
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   924
lemma evaldjf_ex: "Ifm vs bs (evaldjf f ps) \<longleftrightarrow> (\<exists>p \<in> set ps. Ifm vs bs (f p))"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   925
  by (induct ps) (simp_all add: evaldjf_def djf_Or)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   926
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   927
lemma evaldjf_bound0:
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   928
  assumes nb: "\<forall>x\<in> set xs. bound0 (f x)"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   929
  shows "bound0 (evaldjf f xs)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   930
  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   931
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   932
lemma evaldjf_qf:
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   933
  assumes nb: "\<forall>x\<in> set xs. qfree (f x)"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   934
  shows "qfree (evaldjf f xs)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   935
  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   936
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   937
fun disjuncts :: "fm \<Rightarrow> fm list"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   938
where
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   939
  "disjuncts (Or p q) = disjuncts p @ disjuncts q"
41822
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   940
| "disjuncts F = []"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
   941
| "disjuncts p = [p]"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   942
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   943
lemma disjuncts: "(\<exists>q \<in> set (disjuncts p). Ifm vs bs q) = Ifm vs bs p"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   944
  by (induct p rule: disjuncts.induct) auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   945
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   946
lemma disjuncts_nb: "bound0 p \<Longrightarrow> \<forall>q \<in> set (disjuncts p). bound0 q"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   947
proof -
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   948
  assume nb: "bound0 p"
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   949
  then have "list_all bound0 (disjuncts p)"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   950
    by (induct p rule:disjuncts.induct) auto
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   951
  then show ?thesis
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   952
    by (simp only: list_all_iff)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   953
qed
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   954
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   955
lemma disjuncts_qf: "qfree p \<Longrightarrow> \<forall>q\<in> set (disjuncts p). qfree q"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   956
proof-
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   957
  assume qf: "qfree p"
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   958
  then have "list_all qfree (disjuncts p)"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   959
    by (induct p rule: disjuncts.induct) auto
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   960
  then show ?thesis by (simp only: list_all_iff)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   961
qed
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   962
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   963
definition DJ :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   964
  where "DJ f p \<equiv> evaldjf f (disjuncts p)"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   965
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   966
lemma DJ:
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   967
  assumes fdj: "\<forall>p q. Ifm vs bs (f (Or p q)) = Ifm vs bs (Or (f p) (f q))"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   968
    and fF: "f F = F"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   969
  shows "Ifm vs bs (DJ f p) = Ifm vs bs (f p)"
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   970
proof -
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   971
  have "Ifm vs bs (DJ f p) = (\<exists>q \<in> set (disjuncts p). Ifm vs bs (f q))"
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   972
    by (simp add: DJ_def evaldjf_ex)
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   973
  also have "\<dots> = Ifm vs bs (f p)"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   974
    using fdj fF by (induct p rule: disjuncts.induct) auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   975
  finally show ?thesis .
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   976
qed
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   977
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   978
lemma DJ_qf:
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   979
  assumes fqf: "\<forall>p. qfree p \<longrightarrow> qfree (f p)"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   980
  shows "\<forall>p. qfree p \<longrightarrow> qfree (DJ f p)"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   981
proof clarify
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   982
  fix  p
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   983
  assume qf: "qfree p"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   984
  have th: "DJ f p = evaldjf f (disjuncts p)"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   985
    by (simp add: DJ_def)
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   986
  from disjuncts_qf[OF qf] have "\<forall>q\<in> set (disjuncts p). qfree q" .
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   987
  with fqf have th':"\<forall>q\<in> set (disjuncts p). qfree (f q)"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   988
    by blast
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   989
  from evaldjf_qf[OF th'] th show "qfree (DJ f p)"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   990
    by simp
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   991
qed
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   992
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   993
lemma DJ_qe:
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   994
  assumes qe: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm vs bs (qe p) = Ifm vs bs (E p))"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
   995
  shows "\<forall>bs p. qfree p \<longrightarrow> qfree (DJ qe p) \<and> (Ifm vs bs ((DJ qe p)) = Ifm vs bs (E p))"
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   996
proof clarify
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   997
  fix p :: fm and bs
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
   998
  assume qf: "qfree p"
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
   999
  from qe have qth: "\<forall>p. qfree p \<longrightarrow> qfree (qe p)"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1000
    by blast
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1001
  from DJ_qf[OF qth] qf have qfth:"qfree (DJ qe p)"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1002
    by auto
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1003
  have "Ifm vs bs (DJ qe p) \<longleftrightarrow> (\<exists>q\<in> set (disjuncts p). Ifm vs bs (qe q))"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1004
    by (simp add: DJ_def evaldjf_ex)
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1005
  also have "\<dots> = (\<exists>q \<in> set(disjuncts p). Ifm vs bs (E q))"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1006
    using qe disjuncts_qf[OF qf] by auto
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1007
  also have "\<dots> = Ifm vs bs (E p)"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1008
    by (induct p rule: disjuncts.induct) auto
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1009
  finally show "qfree (DJ qe p) \<and> Ifm vs bs (DJ qe p) = Ifm vs bs (E p)"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1010
    using qfth by blast
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1011
qed
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1012
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1013
fun conjuncts :: "fm \<Rightarrow> fm list"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1014
where
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1015
  "conjuncts (And p q) = conjuncts p @ conjuncts q"
41822
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
  1016
| "conjuncts T = []"
27afef7d6c37 recdef -> fun
krauss
parents: 41821
diff changeset
  1017
| "conjuncts p = [p]"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1018
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1019
definition list_conj :: "fm list \<Rightarrow> fm"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1020
  where "list_conj ps \<equiv> foldr conj ps T"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1021
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1022
definition CJNB :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1023
where
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1024
  "CJNB f p \<equiv>
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1025
    (let cjs = conjuncts p;
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1026
      (yes, no) = partition bound0 cjs
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1027
     in conj (decr0 (list_conj yes)) (f (list_conj no)))"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1028
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
  1029
lemma conjuncts_qf: "qfree p \<Longrightarrow> \<forall>q\<in> set (conjuncts p). qfree q"
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1030
proof -
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1031
  assume qf: "qfree p"
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1032
  then have "list_all qfree (conjuncts p)"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1033
    by (induct p rule: conjuncts.induct) auto
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1034
  then show ?thesis
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1035
    by (simp only: list_all_iff)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1036
qed
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1037
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
  1038
lemma conjuncts: "(\<forall>q\<in> set (conjuncts p). Ifm vs bs q) = Ifm vs bs p"
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1039
  by (induct p rule: conjuncts.induct) auto
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1040
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
  1041
lemma conjuncts_nb: "bound0 p \<Longrightarrow> \<forall>q\<in> set (conjuncts p). bound0 q"
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1042
proof -
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1043
  assume nb: "bound0 p"
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1044
  then have "list_all bound0 (conjuncts p)"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1045
    by (induct p rule:conjuncts.induct) auto
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1046
  then show ?thesis
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1047
    by (simp only: list_all_iff)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1048
qed
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1049
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1050
fun islin :: "fm \<Rightarrow> bool"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1051
where
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1052
  "islin (And p q) = (islin p \<and> islin q \<and> p \<noteq> T \<and> p \<noteq> F \<and> q \<noteq> T \<and> q \<noteq> F)"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1053
| "islin (Or p q) = (islin p \<and> islin q \<and> p \<noteq> T \<and> p \<noteq> F \<and> q \<noteq> T \<and> q \<noteq> F)"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1054
| "islin (Eq (CNP 0 c s)) = (isnpoly c \<and> c \<noteq> 0\<^sub>p \<and> tmbound0 s \<and> allpolys isnpoly s)"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1055
| "islin (NEq (CNP 0 c s)) = (isnpoly c \<and> c \<noteq> 0\<^sub>p \<and> tmbound0 s \<and> allpolys isnpoly s)"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1056
| "islin (Lt (CNP 0 c s)) = (isnpoly c \<and> c \<noteq> 0\<^sub>p \<and> tmbound0 s \<and> allpolys isnpoly s)"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1057
| "islin (Le (CNP 0 c s)) = (isnpoly c \<and> c \<noteq> 0\<^sub>p \<and> tmbound0 s \<and> allpolys isnpoly s)"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1058
| "islin (NOT p) = False"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1059
| "islin (Imp p q) = False"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1060
| "islin (Iff p q) = False"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1061
| "islin p = bound0 p"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1062
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1063
lemma islin_stupid:
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1064
  assumes nb: "tmbound0 p"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1065
  shows "islin (Lt p)"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1066
    and "islin (Le p)"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1067
    and "islin (Eq p)"
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1068
    and "islin (NEq p)"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1069
  using nb by (cases p, auto, case_tac nat, auto)+
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1070
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1071
definition "lt p = (case p of CP (C c) \<Rightarrow> if 0>\<^sub>N c then T else F| _ \<Rightarrow> Lt p)"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1072
definition "le p = (case p of CP (C c) \<Rightarrow> if 0\<ge>\<^sub>N c then T else F | _ \<Rightarrow> Le p)"
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1073
definition "eq p = (case p of CP (C c) \<Rightarrow> if c = 0\<^sub>N then T else F | _ \<Rightarrow> Eq p)"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1074
definition "neq p = not (eq p)"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1075
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1076
lemma lt: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (lt p) = Ifm vs bs (Lt p)"
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1077
  apply (simp add: lt_def)
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1078
  apply (cases p)
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1079
  apply simp_all
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1080
  apply (case_tac poly)
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1081
  apply (simp_all add: isnpoly_def)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1082
  done
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1083
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1084
lemma le: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (le p) = Ifm vs bs (Le p)"
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1085
  apply (simp add: le_def)
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1086
  apply (cases p)
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1087
  apply simp_all
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1088
  apply (case_tac poly)
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1089
  apply (simp_all add: isnpoly_def)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1090
  done
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1091
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1092
lemma eq: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (eq p) = Ifm vs bs (Eq p)"
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1093
  apply (simp add: eq_def)
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1094
  apply (cases p)
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1095
  apply simp_all
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1096
  apply (case_tac poly)
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1097
  apply (simp_all add: isnpoly_def)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1098
  done
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1099
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1100
lemma neq: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (neq p) = Ifm vs bs (NEq p)"
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1101
  by (simp add: neq_def eq)
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1102
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1103
lemma lt_lin: "tmbound0 p \<Longrightarrow> islin (lt p)"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1104
  apply (simp add: lt_def)
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1105
  apply (cases p)
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1106
  apply simp_all
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1107
  apply (case_tac poly)
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1108
  apply simp_all
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1109
  apply (case_tac nat)
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1110
  apply simp_all
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1111
  done
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1112
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1113
lemma le_lin: "tmbound0 p \<Longrightarrow> islin (le p)"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1114
  apply (simp add: le_def)
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1115
  apply (cases p)
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1116
  apply simp_all
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1117
  apply (case_tac poly)
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1118
  apply simp_all
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1119
  apply (case_tac nat)
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1120
  apply simp_all
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1121
  done
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1122
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1123
lemma eq_lin: "tmbound0 p \<Longrightarrow> islin (eq p)"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1124
  apply (simp add: eq_def)
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1125
  apply (cases p)
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1126
  apply simp_all
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1127
  apply (case_tac poly)
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1128
  apply simp_all
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1129
  apply (case_tac nat)
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1130
  apply simp_all
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1131
  done
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1132
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1133
lemma neq_lin: "tmbound0 p \<Longrightarrow> islin (neq p)"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1134
  apply (simp add: neq_def eq_def)
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1135
  apply (cases p)
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1136
  apply simp_all
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1137
  apply (case_tac poly)
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1138
  apply simp_all
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1139
  apply (case_tac nat)
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1140
  apply simp_all
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1141
  done
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1142
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1143
definition "simplt t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then lt s else Lt (CNP 0 c s))"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1144
definition "simple t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then le s else Le (CNP 0 c s))"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1145
definition "simpeq t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then eq s else Eq (CNP 0 c s))"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1146
definition "simpneq t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then neq s else NEq (CNP 0 c s))"
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1147
55768
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1148
lemma simplt_islin[simp]:
72c6ce5aea2a tuned specifications and proofs;
wenzelm
parents: 55754
diff changeset
  1149
  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff changeset
  1150
  shows "islin (simplt t)"
55754
d14072d53c1e tuned specifications and proofs;
wenzelm
parents: 55422
diff changeset
  1151
  unfolding simplt_def
33152
241cfaed158f Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
pare