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