author  wenzelm 
Sat, 16 Apr 2011 20:49:48 +0200  
changeset 42368  3b8498ac2314 
parent 42364  8c674b3b8e44 
child 42814  5af15f1e2ef6 
permissions  rwrr 
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 
41849  8 
imports Reflected_Multivariate_Polynomial Dense_Linear_Order DP_Library 
41413
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
39246
diff
changeset

9 
"~~/src/HOL/Library/Efficient_Nat" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

10 
begin 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

11 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

12 
subsection {* Terms *} 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

13 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

14 
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

15 
 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

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

17 

39246  18 
primrec tmsize :: "tm \<Rightarrow> nat" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

19 
"tmsize (CP c) = polysize c" 
39246  20 
 "tmsize (Bound n) = 1" 
21 
 "tmsize (Neg a) = 1 + tmsize a" 

22 
 "tmsize (Add a b) = 1 + tmsize a + tmsize b" 

23 
 "tmsize (Sub a b) = 3 + tmsize a + tmsize b" 

24 
 "tmsize (Mul c a) = 1 + polysize c + tmsize a" 

25 
 "tmsize (CNP n c a) = 3 + polysize c + tmsize a " 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

26 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

27 
(* Semantics of terms tm *) 
39246  28 
primrec Itm :: "'a::{field_char_0, field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

29 
"Itm vs bs (CP c) = (Ipoly vs c)" 
39246  30 
 "Itm vs bs (Bound n) = bs!n" 
31 
 "Itm vs bs (Neg a) = (Itm vs bs a)" 

32 
 "Itm vs bs (Add a b) = Itm vs bs a + Itm vs bs b" 

33 
 "Itm vs bs (Sub a b) = Itm vs bs a  Itm vs bs b" 

34 
 "Itm vs bs (Mul c a) = (Ipoly vs c) * Itm vs bs a" 

35 
 "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

36 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

37 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

38 
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

39 
"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

40 
 "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

41 
 "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

42 
 "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

43 
 "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

44 
 "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

45 
 "allpolys P p = True" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

46 

39246  47 
primrec tmboundslt:: "nat \<Rightarrow> tm \<Rightarrow> bool" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

48 
"tmboundslt n (CP c) = True" 
39246  49 
 "tmboundslt n (Bound m) = (m < n)" 
50 
 "tmboundslt n (CNP m c a) = (m < n \<and> tmboundslt n a)" 

51 
 "tmboundslt n (Neg a) = tmboundslt n a" 

52 
 "tmboundslt n (Add a b) = (tmboundslt n a \<and> tmboundslt n b)" 

53 
 "tmboundslt n (Sub a b) = (tmboundslt n a \<and> tmboundslt n b)" 

54 
 "tmboundslt n (Mul i a) = tmboundslt n a" 

55 

56 
primrec tmbound0:: "tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound 0 *) where 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

57 
"tmbound0 (CP c) = True" 
39246  58 
 "tmbound0 (Bound n) = (n>0)" 
59 
 "tmbound0 (CNP n c a) = (n\<noteq>0 \<and> tmbound0 a)" 

60 
 "tmbound0 (Neg a) = tmbound0 a" 

61 
 "tmbound0 (Add a b) = (tmbound0 a \<and> tmbound0 b)" 

62 
 "tmbound0 (Sub a b) = (tmbound0 a \<and> tmbound0 b)" 

63 
 "tmbound0 (Mul i a) = tmbound0 a" 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

64 
lemma tmbound0_I: 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

65 
assumes nb: "tmbound0 a" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

66 
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

67 
using nb 
41842  68 
by (induct a rule: tm.induct,auto) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

69 

39246  70 
primrec tmbound:: "nat \<Rightarrow> tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound n *) where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

71 
"tmbound n (CP c) = True" 
39246  72 
 "tmbound n (Bound m) = (n \<noteq> m)" 
73 
 "tmbound n (CNP m c a) = (n\<noteq>m \<and> tmbound n a)" 

74 
 "tmbound n (Neg a) = tmbound n a" 

75 
 "tmbound n (Add a b) = (tmbound n a \<and> tmbound n b)" 

76 
 "tmbound n (Sub a b) = (tmbound n a \<and> tmbound n b)" 

77 
 "tmbound n (Mul i a) = tmbound n a" 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

78 
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

79 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

80 
lemma tmbound_I: 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

81 
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

82 
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

83 
using nb le bnd 
39246  84 
by (induct t rule: tm.induct , auto) 
85 

41821  86 
fun decrtm0:: "tm \<Rightarrow> tm" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

87 
"decrtm0 (Bound n) = Bound (n  1)" 
41821  88 
 "decrtm0 (Neg a) = Neg (decrtm0 a)" 
89 
 "decrtm0 (Add a b) = Add (decrtm0 a) (decrtm0 b)" 

90 
 "decrtm0 (Sub a b) = Sub (decrtm0 a) (decrtm0 b)" 

91 
 "decrtm0 (Mul c a) = Mul c (decrtm0 a)" 

92 
 "decrtm0 (CNP n c a) = CNP (n  1) c (decrtm0 a)" 

93 
 "decrtm0 a = a" 

39246  94 

41821  95 
fun incrtm0:: "tm \<Rightarrow> tm" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

96 
"incrtm0 (Bound n) = Bound (n + 1)" 
41821  97 
 "incrtm0 (Neg a) = Neg (incrtm0 a)" 
98 
 "incrtm0 (Add a b) = Add (incrtm0 a) (incrtm0 b)" 

99 
 "incrtm0 (Sub a b) = Sub (incrtm0 a) (incrtm0 b)" 

100 
 "incrtm0 (Mul c a) = Mul c (incrtm0 a)" 

101 
 "incrtm0 (CNP n c a) = CNP (n + 1) c (incrtm0 a)" 

102 
 "incrtm0 a = a" 

39246  103 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

104 
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

105 
shows "Itm vs (x#bs) t = Itm vs bs (decrtm0 t)" 
41842  106 
using nb by (induct t rule: decrtm0.induct, simp_all) 
39246  107 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

108 
lemma incrtm0: "Itm vs (x#bs) (incrtm0 t) = Itm vs bs t" 
41842  109 
by (induct t rule: decrtm0.induct, simp_all) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

110 

39246  111 
primrec decrtm:: "nat \<Rightarrow> tm \<Rightarrow> tm" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

112 
"decrtm m (CP c) = (CP c)" 
39246  113 
 "decrtm m (Bound n) = (if n < m then Bound n else Bound (n  1))" 
114 
 "decrtm m (Neg a) = Neg (decrtm m a)" 

115 
 "decrtm m (Add a b) = Add (decrtm m a) (decrtm m b)" 

116 
 "decrtm m (Sub a b) = Sub (decrtm m a) (decrtm m b)" 

117 
 "decrtm m (Mul c a) = Mul c (decrtm m a)" 

118 
 "decrtm m (CNP n c a) = (if n < m then CNP n c (decrtm m a) else CNP (n  1) c (decrtm m a))" 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

119 

39246  120 
primrec removen:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

121 
"removen n [] = []" 
39246  122 
 "removen n (x#xs) = (if n=0 then xs else (x#(removen (n  1) xs)))" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

123 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

124 
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

125 
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

126 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

127 
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

128 
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

129 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

130 
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

131 
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

132 
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

133 
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

134 
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

135 
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

136 
next 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

137 
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

138 
{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

139 
moreover 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

140 
{assume nxs: "\<not> (n \<ge> length (x#xs))" 
41807  141 
{assume mln: "m < n" hence ?case using Cons by (cases m, auto)} 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

142 
moreover 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

143 
{assume mln: "\<not> (m < n)" 
41807  144 
{assume mxs: "m \<le> length (x#xs)" hence ?case using Cons by (cases m, auto)} 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

145 
moreover 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

146 
{assume mxs: "\<not> (m \<le> length (x#xs))" 
33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33212
diff
changeset

147 
have th: "length (removen n (x#xs)) = length xs" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33212
diff
changeset

148 
using removen_length[where n="n" and xs="x#xs"] nxs by simp 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33212
diff
changeset

149 
with mxs have mxs':"m \<ge> length (removen n (x#xs))" by auto 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33212
diff
changeset

150 
hence "(removen n (x#xs))!m = [] ! (m  length xs)" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33212
diff
changeset

151 
using th nth_length_exceeds[OF mxs'] by auto 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33212
diff
changeset

152 
hence th: "(removen n (x#xs))!m = [] ! (m  (length (x#xs)  1))" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33212
diff
changeset

153 
by auto 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33212
diff
changeset

154 
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

155 
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

156 
} 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

157 
ultimately have ?case by blast 
41807  158 
} ultimately show ?case by blast 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

159 
qed 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

160 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

161 
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

162 
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

163 
shows "Itm vs (removen m bs) (decrtm m t) = Itm vs bs t" 
41807  164 
using bnd nb nle by (induct t rule: tm.induct) (auto simp add: removen_nth) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

165 

39246  166 
primrec tmsubst0:: "tm \<Rightarrow> tm \<Rightarrow> tm" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

167 
"tmsubst0 t (CP c) = CP c" 
39246  168 
 "tmsubst0 t (Bound n) = (if n=0 then t else Bound n)" 
169 
 "tmsubst0 t (CNP n c a) = (if n=0 then Add (Mul c t) (tmsubst0 t a) else CNP n c (tmsubst0 t a))" 

170 
 "tmsubst0 t (Neg a) = Neg (tmsubst0 t a)" 

171 
 "tmsubst0 t (Add a b) = Add (tmsubst0 t a) (tmsubst0 t b)" 

172 
 "tmsubst0 t (Sub a b) = Sub (tmsubst0 t a) (tmsubst0 t b)" 

173 
 "tmsubst0 t (Mul i a) = Mul i (tmsubst0 t a)" 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

174 
lemma tmsubst0: 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

175 
shows "Itm vs (x#bs) (tmsubst0 t a) = Itm vs ((Itm vs (x#bs) t)#bs) a" 
41842  176 
by (induct a rule: tm.induct) auto 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

177 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

178 
lemma tmsubst0_nb: "tmbound0 t \<Longrightarrow> tmbound0 (tmsubst0 t a)" 
41842  179 
by (induct a rule: tm.induct) auto 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

180 

39246  181 
primrec tmsubst:: "nat \<Rightarrow> tm \<Rightarrow> tm \<Rightarrow> tm" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

182 
"tmsubst n t (CP c) = CP c" 
39246  183 
 "tmsubst n t (Bound m) = (if n=m then t else Bound m)" 
184 
 "tmsubst n t (CNP m c a) = (if n=m then Add (Mul c t) (tmsubst n t a) 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

185 
else CNP m c (tmsubst n t a))" 
39246  186 
 "tmsubst n t (Neg a) = Neg (tmsubst n t a)" 
187 
 "tmsubst n t (Add a b) = Add (tmsubst n t a) (tmsubst n t b)" 

188 
 "tmsubst n t (Sub a b) = Sub (tmsubst n t a) (tmsubst n t b)" 

189 
 "tmsubst n t (Mul i a) = Mul i (tmsubst n t a)" 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

190 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

191 
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

192 
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

193 
using nb nlt 
41842  194 
by (induct a rule: tm.induct,auto) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

195 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

196 
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

197 
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

198 
using tnb 
39246  199 
by (induct a rule: tm.induct, auto) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

200 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

201 
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

202 
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

203 
using tnb 
39246  204 
by (induct a rule: tm.induct, auto) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

205 
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

206 
by (induct t, auto) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

207 
(* Simplification *) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

208 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

209 
consts 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

210 
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

211 
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

212 
"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

213 
(if n1=n2 then 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

215 
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

216 
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

217 
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

218 
"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

219 
"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

220 
"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

221 
"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

222 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

223 
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

224 
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

225 
apply (case_tac "c1 +\<^sub>p c2 = 0\<^sub>p",case_tac "n1 \<le> n2", simp_all) 
36348
89c54f51f55a
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents:
35625
diff
changeset

226 
apply (case_tac "n1 = n2", simp_all add: field_simps) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

227 
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

228 
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

229 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

230 
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

231 
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

232 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

233 
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

234 
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

235 
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

236 
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

237 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

238 
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

239 

41821  240 
fun tmmul:: "tm \<Rightarrow> poly \<Rightarrow> tm" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

241 
"tmmul (CP j) = (\<lambda> i. CP (i *\<^sub>p j))" 
41821  242 
 "tmmul (CNP n c a) = (\<lambda> i. CNP n (i *\<^sub>p c) (tmmul a i))" 
243 
 "tmmul t = (\<lambda> i. Mul i t)" 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

244 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

245 
lemma tmmul[simp]: "Itm vs bs (tmmul t i) = Itm vs bs (Mul i t)" 
36348
89c54f51f55a
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents:
35625
diff
changeset

246 
by (induct t arbitrary: i rule: tmmul.induct, simp_all add: field_simps) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

247 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

248 
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

249 
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

250 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

251 
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

252 
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

253 
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

254 
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

255 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

256 
lemma tmmul_allpolys_npoly[simp]: 
36409  257 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

258 
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

259 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35267
diff
changeset

260 
definition tmneg :: "tm \<Rightarrow> tm" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

261 
"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

262 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35267
diff
changeset

263 
definition tmsub :: "tm \<Rightarrow> tm \<Rightarrow> tm" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

264 
"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

265 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

266 
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

267 
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

268 
apply simp 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

269 
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

270 
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

271 
apply simp 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

272 
done 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

273 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

274 
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

275 
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

276 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

277 
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

278 
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

279 
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

280 
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

281 
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

282 
lemma tmneg_allpolys_npoly[simp]: 
36409  283 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

284 
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

285 
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

286 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

287 
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

288 
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

289 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

290 
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

291 
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

292 
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

293 
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

294 
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

295 
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

296 
lemma tmsub_allpolys_npoly[simp]: 
36409  297 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

298 
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

299 
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

300 

41821  301 
fun simptm:: "tm \<Rightarrow> tm" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

302 
"simptm (CP j) = CP (polynate j)" 
41821  303 
 "simptm (Bound n) = CNP n 1\<^sub>p (CP 0\<^sub>p)" 
304 
 "simptm (Neg t) = tmneg (simptm t)" 

305 
 "simptm (Add t s) = tmadd (simptm t,simptm s)" 

306 
 "simptm (Sub t s) = tmsub (simptm t) (simptm s)" 

307 
 "simptm (Mul i t) = (let i' = polynate i in if i' = 0\<^sub>p then CP 0\<^sub>p else tmmul (simptm t) i')" 

308 
 "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))" 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

309 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

310 
lemma polynate_stupid: 
36409  311 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
312 
shows "polynate t = 0\<^sub>p \<Longrightarrow> Ipoly bs t = (0::'a::{field_char_0, field_inverse_zero})" 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

313 
apply (subst polynate[symmetric]) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

314 
apply simp 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

315 
done 
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 
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

318 
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

319 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

320 
lemma simptm_tmbound0[simp]: 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

321 
"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

322 
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

323 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

324 
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

325 
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

326 
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

327 
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

328 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

329 
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

330 
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

331 
lemma simptm_allpolys_npoly[simp]: 
36409  332 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

333 
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

334 
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

335 

41822  336 
declare let_cong[fundef_cong del] 
337 

338 
fun split0 :: "tm \<Rightarrow> (poly \<times> tm)" where 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

339 
"split0 (Bound 0) = (1\<^sub>p, CP 0\<^sub>p)" 
41822  340 
 "split0 (CNP 0 c t) = (let (c',t') = split0 t in (c +\<^sub>p c',t'))" 
341 
 "split0 (Neg t) = (let (c,t') = split0 t in (~\<^sub>p c,Neg t'))" 

342 
 "split0 (CNP n c t) = (let (c',t') = split0 t in (c',CNP n c t'))" 

343 
 "split0 (Add s t) = (let (c1,s') = split0 s ; (c2,t') = split0 t in (c1 +\<^sub>p c2, Add s' t'))" 

344 
 "split0 (Sub s t) = (let (c1,s') = split0 s ; (c2,t') = split0 t in (c1 \<^sub>p c2, Sub s' t'))" 

345 
 "split0 (Mul c t) = (let (c',t') = split0 t in (c *\<^sub>p c', Mul c t'))" 

346 
 "split0 t = (0\<^sub>p, t)" 

347 

348 
declare let_cong[fundef_cong] 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

349 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

350 
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

351 
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

352 
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

353 
by simp 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

354 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

355 
lemma split0: 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

356 
"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

357 
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

358 
apply simp 
36348
89c54f51f55a
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents:
35625
diff
changeset

359 
apply (simp add: Let_def split_def field_simps) 
89c54f51f55a
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents:
35625
diff
changeset

360 
apply (simp add: Let_def split_def field_simps) 
89c54f51f55a
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents:
35625
diff
changeset

361 
apply (simp add: Let_def split_def field_simps) 
89c54f51f55a
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents:
35625
diff
changeset

362 
apply (simp add: Let_def split_def field_simps) 
89c54f51f55a
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents:
35625
diff
changeset

363 
apply (simp add: Let_def split_def field_simps) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

364 
apply (simp add: Let_def split_def mult_assoc right_distrib[symmetric]) 
36348
89c54f51f55a
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents:
35625
diff
changeset

365 
apply (simp add: Let_def split_def field_simps) 
89c54f51f55a
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents:
35625
diff
changeset

366 
apply (simp add: Let_def split_def field_simps) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

367 
done 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

368 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

369 
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

370 
proof 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

371 
fix c' t' 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

372 
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

373 
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

374 
qed 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

375 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

376 
lemma split0_nb0: 
36409  377 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

378 
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

379 
proof 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

380 
fix c' t' 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

381 
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

382 
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

383 
qed 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

384 

36409  385 
lemma split0_nb0'[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

386 
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

387 
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

388 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

389 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

390 
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

391 
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

392 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

393 
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

394 
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

395 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

396 
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

397 
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

398 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

399 
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

400 
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

401 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

402 
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

403 
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

404 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

405 
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

406 
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

407 

36409  408 
lemma isnpoly_fst_split0: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

409 
shows 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

410 
"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

411 
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

412 
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

413 
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 
subsection{* Formulae *} 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

416 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

417 
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

418 
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

419 

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 
(* A size for fm *) 
41822  422 
fun fmsize :: "fm \<Rightarrow> nat" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

423 
"fmsize (NOT p) = 1 + fmsize p" 
41822  424 
 "fmsize (And p q) = 1 + fmsize p + fmsize q" 
425 
 "fmsize (Or p q) = 1 + fmsize p + fmsize q" 

426 
 "fmsize (Imp p q) = 3 + fmsize p + fmsize q" 

427 
 "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)" 

428 
 "fmsize (E p) = 1 + fmsize p" 

429 
 "fmsize (A p) = 4+ fmsize p" 

430 
 "fmsize p = 1" 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

431 
(* several lemmas about fmsize *) 
41822  432 
lemma fmsize_pos[termination_simp]: "fmsize p > 0" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

433 
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

434 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

435 
(* Semantics of formulae (fm) *) 
39246  436 
primrec Ifm ::"'a::{linordered_field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

437 
"Ifm vs bs T = True" 
39246  438 
 "Ifm vs bs F = False" 
439 
 "Ifm vs bs (Lt a) = (Itm vs bs a < 0)" 

440 
 "Ifm vs bs (Le a) = (Itm vs bs a \<le> 0)" 

441 
 "Ifm vs bs (Eq a) = (Itm vs bs a = 0)" 

442 
 "Ifm vs bs (NEq a) = (Itm vs bs a \<noteq> 0)" 

443 
 "Ifm vs bs (NOT p) = (\<not> (Ifm vs bs p))" 

444 
 "Ifm vs bs (And p q) = (Ifm vs bs p \<and> Ifm vs bs q)" 

445 
 "Ifm vs bs (Or p q) = (Ifm vs bs p \<or> Ifm vs bs q)" 

446 
 "Ifm vs bs (Imp p q) = ((Ifm vs bs p) \<longrightarrow> (Ifm vs bs q))" 

447 
 "Ifm vs bs (Iff p q) = (Ifm vs bs p = Ifm vs bs q)" 

448 
 "Ifm vs bs (E p) = (\<exists> x. Ifm vs (x#bs) p)" 

449 
 "Ifm vs bs (A p) = (\<forall> x. Ifm vs (x#bs) p)" 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

450 

41822  451 
fun not:: "fm \<Rightarrow> fm" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

452 
"not (NOT (NOT p)) = not p" 
41822  453 
 "not (NOT p) = p" 
454 
 "not T = F" 

455 
 "not F = T" 

456 
 "not (Lt t) = Le (tmneg t)" 

457 
 "not (Le t) = Lt (tmneg t)" 

458 
 "not (Eq t) = NEq t" 

459 
 "not (NEq t) = Eq t" 

460 
 "not p = NOT p" 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

461 
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

462 
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

463 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35267
diff
changeset

464 
definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

465 
"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

466 
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

467 
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

468 
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

469 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35267
diff
changeset

470 
definition disj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

471 
"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

472 
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

473 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

474 
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

475 
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

476 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35267
diff
changeset

477 
definition imp :: "fm \<Rightarrow> fm \<Rightarrow> fm" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

478 
"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

479 
else Imp p q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

480 
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

481 
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

482 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35267
diff
changeset

483 
definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

484 
"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

485 
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

486 
Iff p q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

487 
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

488 
by (unfold iff_def,cases "p=q", simp,cases "p=NOT q", simp) (cases "NOT p= q", auto) 
41822  489 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

490 
(* Quantifier freeness *) 
41822  491 
fun qfree:: "fm \<Rightarrow> bool" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

492 
"qfree (E p) = False" 
41822  493 
 "qfree (A p) = False" 
494 
 "qfree (NOT p) = qfree p" 

495 
 "qfree (And p q) = (qfree p \<and> qfree q)" 

496 
 "qfree (Or p q) = (qfree p \<and> qfree q)" 

497 
 "qfree (Imp p q) = (qfree p \<and> qfree q)" 

498 
 "qfree (Iff p q) = (qfree p \<and> qfree q)" 

499 
 "qfree p = True" 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

500 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

501 
(* Boundedness and substitution *) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

502 

39246  503 
primrec boundslt :: "nat \<Rightarrow> fm \<Rightarrow> bool" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

504 
"boundslt n T = True" 
39246  505 
 "boundslt n F = True" 
506 
 "boundslt n (Lt t) = (tmboundslt n t)" 

507 
 "boundslt n (Le t) = (tmboundslt n t)" 

508 
 "boundslt n (Eq t) = (tmboundslt n t)" 

509 
 "boundslt n (NEq t) = (tmboundslt n t)" 

510 
 "boundslt n (NOT p) = boundslt n p" 

511 
 "boundslt n (And p q) = (boundslt n p \<and> boundslt n q)" 

512 
 "boundslt n (Or p q) = (boundslt n p \<and> boundslt n q)" 

513 
 "boundslt n (Imp p q) = ((boundslt n p) \<and> (boundslt n q))" 

514 
 "boundslt n (Iff p q) = (boundslt n p \<and> boundslt n q)" 

515 
 "boundslt n (E p) = boundslt (Suc n) p" 

516 
 "boundslt n (A p) = boundslt (Suc n) p" 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

517 

41822  518 
fun bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *) where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

519 
"bound0 T = True" 
41822  520 
 "bound0 F = True" 
521 
 "bound0 (Lt a) = tmbound0 a" 

522 
 "bound0 (Le a) = tmbound0 a" 

523 
 "bound0 (Eq a) = tmbound0 a" 

524 
 "bound0 (NEq a) = tmbound0 a" 

525 
 "bound0 (NOT p) = bound0 p" 

526 
 "bound0 (And p q) = (bound0 p \<and> bound0 q)" 

527 
 "bound0 (Or p q) = (bound0 p \<and> bound0 q)" 

528 
 "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))" 

529 
 "bound0 (Iff p q) = (bound0 p \<and> bound0 q)" 

530 
 "bound0 p = False" 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

531 
lemma bound0_I: 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

532 
assumes bp: "bound0 p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

533 
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

534 
using bp tmbound0_I[where b="b" and bs="bs" and b'="b'"] 
41842  535 
by (induct p rule: bound0.induct,auto) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

536 

39246  537 
primrec bound:: "nat \<Rightarrow> fm \<Rightarrow> bool" (* A Formula is independent of Bound n *) where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

538 
"bound m T = True" 
39246  539 
 "bound m F = True" 
540 
 "bound m (Lt t) = tmbound m t" 

541 
 "bound m (Le t) = tmbound m t" 

542 
 "bound m (Eq t) = tmbound m t" 

543 
 "bound m (NEq t) = tmbound m t" 

544 
 "bound m (NOT p) = bound m p" 

545 
 "bound m (And p q) = (bound m p \<and> bound m q)" 

546 
 "bound m (Or p q) = (bound m p \<and> bound m q)" 

547 
 "bound m (Imp p q) = ((bound m p) \<and> (bound m q))" 

548 
 "bound m (Iff p q) = (bound m p \<and> bound m q)" 

549 
 "bound m (E p) = bound (Suc m) p" 

550 
 "bound m (A p) = bound (Suc m) p" 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

551 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

552 
lemma bound_I: 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

553 
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

554 
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

555 
using bnd nb le tmbound_I[where bs=bs and vs = vs] 
39246  556 
proof(induct p arbitrary: bs n rule: fm.induct) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

557 
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

558 
{fix y 
41807  559 
from E have bnd: "boundslt (length (y#bs)) p" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

560 
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

561 
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

562 
thus ?case by simp 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

563 
next 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

564 
case (A p bs n) {fix y 
41807  565 
from A have bnd: "boundslt (length (y#bs)) p" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

566 
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

567 
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

568 
thus ?case by simp 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

569 
qed auto 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

570 

41822  571 
fun decr0 :: "fm \<Rightarrow> fm" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

572 
"decr0 (Lt a) = Lt (decrtm0 a)" 
41822  573 
 "decr0 (Le a) = Le (decrtm0 a)" 
574 
 "decr0 (Eq a) = Eq (decrtm0 a)" 

575 
 "decr0 (NEq a) = NEq (decrtm0 a)" 

576 
 "decr0 (NOT p) = NOT (decr0 p)" 

577 
 "decr0 (And p q) = conj (decr0 p) (decr0 q)" 

578 
 "decr0 (Or p q) = disj (decr0 p) (decr0 q)" 

579 
 "decr0 (Imp p q) = imp (decr0 p) (decr0 q)" 

580 
 "decr0 (Iff p q) = iff (decr0 p) (decr0 q)" 

581 
 "decr0 p = p" 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

582 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

583 
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

584 
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

585 
using nb 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

586 
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

587 

39246  588 
primrec decr :: "nat \<Rightarrow> fm \<Rightarrow> fm" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

589 
"decr m T = T" 
39246  590 
 "decr m F = F" 
591 
 "decr m (Lt t) = (Lt (decrtm m t))" 

592 
 "decr m (Le t) = (Le (decrtm m t))" 

593 
 "decr m (Eq t) = (Eq (decrtm m t))" 

594 
 "decr m (NEq t) = (NEq (decrtm m t))" 

595 
 "decr m (NOT p) = NOT (decr m p)" 

596 
 "decr m (And p q) = conj (decr m p) (decr m q)" 

597 
 "decr m (Or p q) = disj (decr m p) (decr m q)" 

598 
 "decr m (Imp p q) = imp (decr m p) (decr m q)" 

599 
 "decr m (Iff p q) = iff (decr m p) (decr m q)" 

600 
 "decr m (E p) = E (decr (Suc m) p)" 

601 
 "decr m (A p) = A (decr (Suc m) p)" 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

602 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

603 
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

604 
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

605 
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

606 
using bnd nb nle 
39246  607 
proof(induct p arbitrary: bs m rule: fm.induct) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

608 
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

609 
{fix x 
41807  610 
from E have bnd: "boundslt (length (x#bs)) p" and nb: "bound (Suc m) p" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

611 
and nle: "Suc m < length (x#bs)" by auto 
41807  612 
from E(1)[OF bnd nb nle] have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p". 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

613 
} thus ?case by auto 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

614 
next 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

615 
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

616 
{fix x 
41807  617 
from A have bnd: "boundslt (length (x#bs)) p" and nb: "bound (Suc m) p" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

618 
and nle: "Suc m < length (x#bs)" by auto 
41807  619 
from A(1)[OF bnd nb nle] have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p". 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

620 
} thus ?case by auto 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

621 
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

622 

39246  623 
primrec subst0:: "tm \<Rightarrow> fm \<Rightarrow> fm" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

624 
"subst0 t T = T" 
39246  625 
 "subst0 t F = F" 
626 
 "subst0 t (Lt a) = Lt (tmsubst0 t a)" 

627 
 "subst0 t (Le a) = Le (tmsubst0 t a)" 

628 
 "subst0 t (Eq a) = Eq (tmsubst0 t a)" 

629 
 "subst0 t (NEq a) = NEq (tmsubst0 t a)" 

630 
 "subst0 t (NOT p) = NOT (subst0 t p)" 

631 
 "subst0 t (And p q) = And (subst0 t p) (subst0 t q)" 

632 
 "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)" 

633 
 "subst0 t (Imp p q) = Imp (subst0 t p) (subst0 t q)" 

634 
 "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)" 

635 
 "subst0 t (E p) = E p" 

636 
 "subst0 t (A p) = A p" 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

637 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

638 
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

639 
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

640 
using qf tmsubst0[where x="x" and bs="bs" and t="t"] 
39246  641 
by (induct p rule: fm.induct, auto) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

642 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

643 
lemma subst0_nb: 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

644 
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

645 
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

646 
using qf tmsubst0_nb[OF bp] bp 
39246  647 
by (induct p rule: fm.induct, auto) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

648 

39246  649 
primrec subst:: "nat \<Rightarrow> tm \<Rightarrow> fm \<Rightarrow> fm" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

650 
"subst n t T = T" 
39246  651 
 "subst n t F = F" 
652 
 "subst n t (Lt a) = Lt (tmsubst n t a)" 

653 
 "subst n t (Le a) = Le (tmsubst n t a)" 

654 
 "subst n t (Eq a) = Eq (tmsubst n t a)" 

655 
 "subst n t (NEq a) = NEq (tmsubst n t a)" 

656 
 "subst n t (NOT p) = NOT (subst n t p)" 

657 
 "subst n t (And p q) = And (subst n t p) (subst n t q)" 

658 
 "subst n t (Or p q) = Or (subst n t p) (subst n t q)" 

659 
 "subst n t (Imp p q) = Imp (subst n t p) (subst n t q)" 

660 
 "subst n t (Iff p q) = Iff (subst n t p) (subst n t q)" 

661 
 "subst n t (E p) = E (subst (Suc n) (incrtm0 t) p)" 

662 
 "subst n t (A p) = A (subst (Suc n) (incrtm0 t) p)" 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

663 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

664 
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

665 
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

666 
using nb nlm 
39246  667 
proof (induct p arbitrary: bs n t rule: fm.induct) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

668 
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

669 
{fix x 
41807  670 
from E have bn: "boundslt (length (x#bs)) p" by simp 
671 
from E have nlm: "Suc n \<le> length (x#bs)" by simp 

672 
from E(1)[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 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

673 
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

674 
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

675 
thus ?case by simp 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

676 
next 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

677 
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

678 
{fix x 
41807  679 
from A have bn: "boundslt (length (x#bs)) p" by simp 
680 
from A have nlm: "Suc n \<le> length (x#bs)" by simp 

681 
from A(1)[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 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

682 
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

683 
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

684 
thus ?case by simp 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

685 
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

686 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

687 
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

688 
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

689 
using tnb tmsubst_nb incrtm0_tmbound 
39246  690 
by (induct p arbitrary: m t rule: fm.induct, auto) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

691 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

692 
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

693 
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

694 
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

695 
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

696 
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

697 
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

698 
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

699 
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

700 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

701 
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

702 
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

703 
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

704 
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

705 
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

706 
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

707 
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

708 
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

709 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

710 
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

711 
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

712 
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

713 
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

714 
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

715 
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

716 
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

717 
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

718 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

719 
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

720 
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

721 
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

722 
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

723 
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

724 
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

725 
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

726 
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

727 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

728 
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

729 
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

730 
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

731 
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

732 
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

733 
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

734 
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

735 
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

736 
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

737 
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

738 

41822  739 
fun isatom :: "fm \<Rightarrow> bool" (* test for atomicity *) where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

740 
"isatom T = True" 
41822  741 
 "isatom F = True" 
742 
 "isatom (Lt a) = True" 

743 
 "isatom (Le a) = True" 

744 
 "isatom (Eq a) = True" 

745 
 "isatom (NEq a) = True" 

746 
 "isatom p = False" 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

747 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

748 
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

749 
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

750 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35267
diff
changeset

751 
definition djf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

752 
"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

753 
(let fp = f p in case fp of T \<Rightarrow> T  F \<Rightarrow> q  _ \<Rightarrow> Or (f p) q))" 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35267
diff
changeset

754 
definition evaldjf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

755 
"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

756 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

757 
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

758 
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

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

760 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

761 
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

762 
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

763 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

764 
lemma evaldjf_bound0: 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

765 
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

766 
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

767 
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

768 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

769 
lemma evaldjf_qf: 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

770 
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

771 
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

772 
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

773 

41822  774 
fun disjuncts :: "fm \<Rightarrow> fm list" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

775 
"disjuncts (Or p q) = (disjuncts p) @ (disjuncts q)" 
41822  776 
 "disjuncts F = []" 
777 
 "disjuncts p = [p]" 

33152
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 
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

780 
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

781 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

782 
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

783 
proof 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

784 
assume nb: "bound0 p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

785 
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

786 
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

787 
qed 
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 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

790 
proof 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

791 
assume qf: "qfree p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

792 
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

793 
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

794 
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

795 
qed 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

796 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35267
diff
changeset

797 
definition DJ :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

798 
"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

799 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

800 
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

801 
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

802 
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

803 
proof 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

804 
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

805 
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

806 
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

807 
finally show ?thesis . 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

808 
qed 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

809 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

810 
lemma DJ_qf: assumes 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

811 
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

812 
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

813 
proof(clarify) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

814 
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

815 
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

816 
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

817 
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

818 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

819 
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

820 
qed 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

821 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

822 
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

823 
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

824 
proof(clarify) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

825 
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

826 
assume qf: "qfree p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

827 
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

828 
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

829 
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

830 
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

831 
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

832 
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

833 
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

834 
qed 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

835 

41822  836 
fun conjuncts :: "fm \<Rightarrow> fm list" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

837 
"conjuncts (And p q) = (conjuncts p) @ (conjuncts q)" 
41822  838 
 "conjuncts T = []" 
839 
 "conjuncts p = [p]" 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

840 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35267
diff
changeset

841 
definition list_conj :: "fm list \<Rightarrow> fm" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

842 
"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

843 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35267
diff
changeset

844 
definition CJNB :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

845 
"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

846 
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

847 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

848 
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

849 
proof 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

850 
assume qf: "qfree p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

851 
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

852 
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

853 
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

854 
qed 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

855 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

856 
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

857 
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

858 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

859 
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

860 
proof 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

861 
assume nb: "bound0 p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

862 
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

863 
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

864 
qed 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

865 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

866 
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

867 
"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

868 
 "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

869 
 "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

870 
 "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

871 
 "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

872 
 "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

873 
 "islin (NOT p) = False" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

874 
 "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

875 
 "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

876 
 "islin p = bound0 p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

877 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

878 
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

879 
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

880 
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

881 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

882 
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

883 
definition "le p = (case p of CP (C c) \<Rightarrow> if 0\<ge>\<^sub>N c then T else F  _ \<Rightarrow> Le p)" 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset

884 
definition eq where "eq p = (case p of CP (C c) \<Rightarrow> if c = 0\<^sub>N then T else F  _ \<Rightarrow> Eq p)" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

885 
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

886 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

887 
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

888 
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

889 
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

890 
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

891 
done 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

892 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

893 
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

894 
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

895 
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

896 
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

897 
done 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

898 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

899 
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

900 
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

901 
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

902 
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

903 
done 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

904 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

905 
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

906 
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

907 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

908 
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

909 
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

910 
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

911 
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

912 
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

913 
done 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

914 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

915 
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

916 
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

917 
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

918 
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

919 
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

920 
done 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

921 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

922 
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

923 
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

924 
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

925 
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

926 
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

927 
done 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

928 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

929 
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

930 
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

931 
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

932 
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

933 
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

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

937 
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

938 
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

939 
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

940 

36409  941 
lemma simplt_islin[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

942 
shows "islin (simplt t)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

943 
unfolding simplt_def 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

944 
using split0_nb0' 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

945 
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

946 

36409  947 
lemma simple_islin[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

948 
shows "islin (simple t)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

949 
unfolding simple_def 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

950 
using split0_nb0' 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

951 
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) 
36409  952 
lemma simpeq_islin[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

953 
shows "islin (simpeq t)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

954 
unfolding simpeq_def 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

955 
using split0_nb0' 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

956 
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

957 

36409  958 
lemma simpneq_islin[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

959 
shows "islin (simpneq t)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

960 
unfolding simpneq_def 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

961 
using split0_nb0' 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

962 
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

963 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

964 
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

965 
by (cases "split0 s", auto) 
36409  966 
lemma split0_npoly: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

967 
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

968 
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

969 
using n 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

970 
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

971 
lemma simplt[simp]: 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

972 
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

973 
proof 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

974 
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

975 
let ?t = "simptm t" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

976 
{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

977 
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

978 
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

979 
moreover 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

980 
{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

981 
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

982 
} 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

983 
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

984 
qed 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

985 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

986 
lemma simple[simp]: 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

987 
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

988 
proof 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

989 
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

990 
let ?t = "simptm t" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

991 
{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

992 
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

993 
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

994 
moreover 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

995 
{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

996 
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

997 
} 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

998 
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

999 
qed 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1000 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1001 
lemma simpeq[simp]: 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1002 
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

1003 
proof 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1004 
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

1005 
let ?t = "simptm t" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1006 
{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

1007 
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

1008 
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

1009 
moreover 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1010 
{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

1011 
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

1012 
} 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1013 
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

1014 
qed 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1015 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1016 
lemma simpneq[simp]: 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1017 
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

1018 
proof 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1019 
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

1020 
let ?t = "simptm t" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1021 
{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

1022 
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

1023 
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

1024 
moreover 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1025 
{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

1026 
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

1027 
} 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1028 
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

1029 
qed 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1030 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1031 
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

1032 
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

1033 
apply (cases t, auto) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1034 
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

1035 
done 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1036 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1037 
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

1038 
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

1039 
apply (cases t, auto) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1040 
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

1041 
done 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1042 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1043 
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

1044 
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

1045 
apply (cases t, auto) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1046 
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

1047 
done 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1048 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1049 
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

1050 
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

1051 
apply (cases t, auto) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1052 
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

1053 
done 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1054 

36409  1055 
lemma simplt_nb[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1056 
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

1057 
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

1058 
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

1059 
assume nb: "tmbound0 t" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1060 
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

1061 
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

1062 
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

1063 
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

1064 
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

1065 
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

1066 
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

1067 
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

1068 
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

1069 
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

1070 
qed 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1071 

36409  1072 
lemma simple_nb[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1073 
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

1074 
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

1075 
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

1076 
assume nb: "tmbound0 t" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1077 
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

1078 
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

1079 
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

1080 
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

1081 
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

1082 
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

1083 
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

1084 
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

1085 
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

1086 
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

1087 
qed 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1088 

36409  1089 
lemma simpeq_nb[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1090 
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

1091 
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

1092 
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

1093 
assume nb: "tmbound0 t" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1094 
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

1095 
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

1096 
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

1097 
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

1098 
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

1099 
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

1100 
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

1101 
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

1102 
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

1103 
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

1104 
qed 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1105 

36409  1106 
lemma simpneq_nb[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1107 
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

1108 
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

1109 
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

1110 
assume nb: "tmbound0 t" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1111 
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

1112 
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

1113 
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

1114 
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

1115 
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

1116 
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

1117 
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

1118 
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

1119 
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

1120 
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

1121 
qed 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1122 

41822  1123 
fun conjs :: "fm \<Rightarrow> fm list" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1124 
"conjs (And p q) = (conjs p)@(conjs q)" 
41822  1125 
 "conjs T = []" 
1126 
 "conjs p = [p]" 

33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1127 
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

1128 
by (induct p rule: conjs.induct, auto) 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35267
diff
changeset

1129 
definition list_disj :: "fm list \<Rightarrow> fm" where 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1130 
"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

1131 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1132 
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

1133 
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

1134 
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

1135 
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

1136 
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

1137 
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

1138 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1139 
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

1140 
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

1141 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1142 
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

1143 
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

1144 
apply (unfold conjs.simps) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1145 
apply (unfold set_append) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1146 
apply (unfold ball_Un) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1147 
apply (unfold bound.simps) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1148 
apply auto 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1149 
done 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1150 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1151 
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

1152 
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

1153 
apply (unfold conjs.simps) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1154 
apply (unfold set_append) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1155 
apply (unfold ball_Un) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1156 
apply (unfold boundslt.simps) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1157 
apply blast 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1158 
by simp_all 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1159 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1160 
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

1161 
unfolding list_conj_def 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1162 
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

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_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

1165 
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

1166 
using bnd 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1167 
unfolding list_conj_def 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1168 
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

1169 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1170 
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

1171 
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

1172 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1173 
lemma CJNB_qe: 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1174 
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

1175 
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

1176 
proof(clarify) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1177 
fix bs p 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1178 
assume qfp: "qfree p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1179 
let ?cjs = "conjuncts p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1180 
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

1181 
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

1182 
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

1183 
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

1184 
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

1185 
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

1186 
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

1187 
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

1188 
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

1189 
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

1190 
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

1191 
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

1192 
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

1193 
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

1194 
by (simp add: CJNB_def Let_def conj_qf split_def) 