author  wenzelm 
Wed, 26 Feb 2014 17:12:07 +0100  
changeset 55768  72c6ce5aea2a 
parent 55754  d14072d53c1e 
child 56410  a14831ac3023 
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 
55754  8 
imports 
9 
Reflected_Multivariate_Polynomial 

10 
Dense_Linear_Order 

11 
DP_Library 

12 
"~~/src/HOL/Library/Code_Target_Numeral" 

13 
"~~/src/HOL/Library/Old_Recdef" 

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

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

15 

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

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

17 

55754  18 
datatype tm = CP poly  Bound nat  Add tm tm  Mul poly tm 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

19 
 Neg tm  Sub tm tm  CNP nat poly tm 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

20 

55754  21 
(* A size for poly to make inductive proofs simpler*) 
22 
primrec tmsize :: "tm \<Rightarrow> nat" 

23 
where 

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

24 
"tmsize (CP c) = polysize c" 
39246  25 
 "tmsize (Bound n) = 1" 
26 
 "tmsize (Neg a) = 1 + tmsize a" 

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

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

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

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

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

31 

55754  32 
(* Semantics of terms tm *) 
33 
primrec Itm :: "'a::{field_char_0, field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a" 

34 
where 

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

35 
"Itm vs bs (CP c) = (Ipoly vs c)" 
39246  36 
 "Itm vs bs (Bound n) = bs!n" 
37 
 "Itm vs bs (Neg a) = (Itm vs bs a)" 

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

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

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

55754  41 
 "Itm vs bs (CNP n c t) = (Ipoly vs c)*(bs!n) + Itm vs bs t" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

42 

55754  43 
fun allpolys :: "(poly \<Rightarrow> bool) \<Rightarrow> tm \<Rightarrow> bool" 
44 
where 

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

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

46 
 "allpolys P (CNP n c p) = (P c \<and> allpolys P p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

47 
 "allpolys P (Mul c p) = (P c \<and> allpolys P p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

49 
 "allpolys P (Add p q) = (allpolys P p \<and> allpolys P q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

50 
 "allpolys P (Sub p q) = (allpolys P p \<and> allpolys P q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

52 

55754  53 
primrec tmboundslt :: "nat \<Rightarrow> tm \<Rightarrow> bool" 
54 
where 

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

55 
"tmboundslt n (CP c) = True" 
39246  56 
 "tmboundslt n (Bound m) = (m < n)" 
57 
 "tmboundslt n (CNP m c a) = (m < n \<and> tmboundslt n a)" 

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

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

55754  60 
 "tmboundslt n (Sub a b) = (tmboundslt n a \<and> tmboundslt n b)" 
39246  61 
 "tmboundslt n (Mul i a) = tmboundslt n a" 
62 

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

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

65 
"tmbound0 (CP c) = True" 
39246  66 
 "tmbound0 (Bound n) = (n>0)" 
67 
 "tmbound0 (CNP n c a) = (n\<noteq>0 \<and> tmbound0 a)" 

68 
 "tmbound0 (Neg a) = tmbound0 a" 

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

55754  70 
 "tmbound0 (Sub a b) = (tmbound0 a \<and> tmbound0 b)" 
39246  71 
 "tmbound0 (Mul i a) = tmbound0 a" 
55754  72 

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

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

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

75 
shows "Itm vs (b#bs) a = Itm vs (b'#bs) a" 
55754  76 
using nb 
77 
by (induct a rule: tm.induct,auto) 

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

78 

55754  79 
primrec tmbound :: "nat \<Rightarrow> tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound n *) 
80 
where 

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

81 
"tmbound n (CP c) = True" 
39246  82 
 "tmbound n (Bound m) = (n \<noteq> m)" 
83 
 "tmbound n (CNP m c a) = (n\<noteq>m \<and> tmbound n a)" 

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

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

55754  86 
 "tmbound n (Sub a b) = (tmbound n a \<and> tmbound n b)" 
39246  87 
 "tmbound n (Mul i a) = tmbound n a" 
55754  88 

89 
lemma tmbound0_tmbound_iff: "tmbound 0 t = tmbound0 t" 

90 
by (induct t) auto 

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

91 

55754  92 
lemma tmbound_I: 
93 
assumes bnd: "tmboundslt (length bs) t" 

94 
and nb: "tmbound n t" 

95 
and le: "n \<le> length bs" 

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

96 
shows "Itm vs (bs[n:=x]) t = Itm vs bs t" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

97 
using nb le bnd 
55754  98 
by (induct t rule: tm.induct) auto 
39246  99 

55754  100 
fun decrtm0 :: "tm \<Rightarrow> tm" 
101 
where 

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

102 
"decrtm0 (Bound n) = Bound (n  1)" 
41821  103 
 "decrtm0 (Neg a) = Neg (decrtm0 a)" 
104 
 "decrtm0 (Add a b) = Add (decrtm0 a) (decrtm0 b)" 

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

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

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

108 
 "decrtm0 a = a" 

39246  109 

55754  110 
fun incrtm0 :: "tm \<Rightarrow> tm" 
111 
where 

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

112 
"incrtm0 (Bound n) = Bound (n + 1)" 
41821  113 
 "incrtm0 (Neg a) = Neg (incrtm0 a)" 
114 
 "incrtm0 (Add a b) = Add (incrtm0 a) (incrtm0 b)" 

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

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

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

118 
 "incrtm0 a = a" 

39246  119 

55754  120 
lemma decrtm0: 
121 
assumes nb: "tmbound0 t" 

122 
shows "Itm vs (x # bs) t = Itm vs bs (decrtm0 t)" 

123 
using nb by (induct t rule: decrtm0.induct) simp_all 

39246  124 

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

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

127 

55754  128 
primrec decrtm :: "nat \<Rightarrow> tm \<Rightarrow> tm" 
129 
where 

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

130 
"decrtm m (CP c) = (CP c)" 
39246  131 
 "decrtm m (Bound n) = (if n < m then Bound n else Bound (n  1))" 
132 
 "decrtm m (Neg a) = Neg (decrtm m a)" 

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

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

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

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

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

137 

55754  138 
primrec removen :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" 
139 
where 

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

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

142 

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

143 
lemma removen_same: "n \<ge> length xs \<Longrightarrow> removen n xs = xs" 
55754  144 
by (induct xs arbitrary: n) auto 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

145 

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

146 
lemma nth_length_exceeds: "n \<ge> length xs \<Longrightarrow> xs!n = []!(n  length xs)" 
55754  147 
by (induct xs arbitrary: n) auto 
148 

149 
lemma removen_length: 

150 
"length (removen n xs) = (if n \<ge> length xs then length xs else length xs  1)" 

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

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

152 

55754  153 
lemma removen_nth: 
154 
"(removen n xs)!m = 

155 
(if n \<ge> length xs then xs!m 

156 
else if m < n then xs!m 

157 
else if m \<le> length xs then xs!(Suc m) 

158 
else []!(m  (length xs  1)))" 

159 
proof (induct xs arbitrary: n m) 

160 
case Nil 

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

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

163 
case (Cons x xs n m) 
55768  164 
{ 
165 
assume nxs: "n \<ge> length (x#xs)" 

166 
then have ?case using removen_same[OF nxs] by simp 

167 
} 

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

168 
moreover 
55768  169 
{ 
170 
assume nxs: "\<not> (n \<ge> length (x#xs))" 

171 
{ 

172 
assume mln: "m < n" 

173 
then have ?case using Cons by (cases m) auto 

174 
} 

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

175 
moreover 
55768  176 
{ 
177 
assume mln: "\<not> (m < n)" 

178 
{ 

179 
assume mxs: "m \<le> length (x#xs)" 

180 
then have ?case using Cons by (cases m) auto 

181 
} 

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

182 
moreover 
55768  183 
{ 
184 
assume mxs: "\<not> (m \<le> length (x#xs))" 

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

186 
using removen_length[where n="n" and xs="x#xs"] nxs by simp 
55768  187 
with mxs have mxs':"m \<ge> length (removen n (x#xs))" 
188 
by auto 

189 
then have "(removen n (x#xs))!m = [] ! (m  length xs)" 

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

190 
using th nth_length_exceeds[OF mxs'] by auto 
55768  191 
then have th: "(removen n (x#xs))!m = [] ! (m  (length (x#xs)  1))" 
33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33212
diff
changeset

192 
by auto 
55768  193 
then have ?case 
194 
using nxs mln mxs by auto 

195 
} 

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

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

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

198 
ultimately have ?case by blast 
55768  199 
} 
200 
ultimately show ?case by blast 

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

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

202 

55754  203 
lemma decrtm: 
204 
assumes bnd: "tmboundslt (length bs) t" 

205 
and nb: "tmbound m t" 

206 
and nle: "m \<le> length bs" 

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

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

209 

55754  210 
primrec tmsubst0:: "tm \<Rightarrow> tm \<Rightarrow> tm" 
211 
where 

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

212 
"tmsubst0 t (CP c) = CP c" 
39246  213 
 "tmsubst0 t (Bound n) = (if n=0 then t else Bound n)" 
214 
 "tmsubst0 t (CNP n c a) = (if n=0 then Add (Mul c t) (tmsubst0 t a) else CNP n c (tmsubst0 t a))" 

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

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

55754  217 
 "tmsubst0 t (Sub a b) = Sub (tmsubst0 t a) (tmsubst0 t b)" 
39246  218 
 "tmsubst0 t (Mul i a) = Mul i (tmsubst0 t a)" 
55754  219 

220 
lemma tmsubst0: "Itm vs (x#bs) (tmsubst0 t a) = Itm vs ((Itm vs (x#bs) t)#bs) a" 

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

222 

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

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

225 

55754  226 
primrec tmsubst:: "nat \<Rightarrow> tm \<Rightarrow> tm \<Rightarrow> tm" 
227 
where 

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

228 
"tmsubst n t (CP c) = CP c" 
39246  229 
 "tmsubst n t (Bound m) = (if n=m then t else Bound m)" 
55754  230 
 "tmsubst n t (CNP m c a) = 
231 
(if n = m then Add (Mul c t) (tmsubst n t a) else CNP m c (tmsubst n t a))" 

39246  232 
 "tmsubst n t (Neg a) = Neg (tmsubst n t a)" 
233 
 "tmsubst n t (Add a b) = Add (tmsubst n t a) (tmsubst n t b)" 

55754  234 
 "tmsubst n t (Sub a b) = Sub (tmsubst n t a) (tmsubst n t b)" 
39246  235 
 "tmsubst n t (Mul i a) = Mul i (tmsubst n t a)" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

236 

55754  237 
lemma tmsubst: 
238 
assumes nb: "tmboundslt (length bs) a" 

239 
and nlt: "n \<le> length bs" 

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

240 
shows "Itm vs bs (tmsubst n t a) = Itm vs (bs[n:= Itm vs bs t]) a" 
55754  241 
using nb nlt 
242 
by (induct a rule: tm.induct) auto 

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

243 

55754  244 
lemma tmsubst_nb0: 
245 
assumes tnb: "tmbound0 t" 

246 
shows "tmbound0 (tmsubst 0 t a)" 

247 
using tnb 

248 
by (induct a rule: tm.induct) auto 

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

249 

55754  250 
lemma tmsubst_nb: 
251 
assumes tnb: "tmbound m t" 

252 
shows "tmbound m (tmsubst m t a)" 

253 
using tnb 

254 
by (induct a rule: tm.induct) auto 

255 

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

256 
lemma incrtm0_tmbound: "tmbound n t \<Longrightarrow> tmbound (Suc n) (incrtm0 t)" 
55754  257 
by (induct t) auto 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

258 

55754  259 
(* Simplification *) 
260 

261 
consts tmadd:: "tm \<times> tm \<Rightarrow> tm" 

55768  262 
recdef tmadd "measure (\<lambda>(t,s). size t + size s)" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

263 
"tmadd (CNP n1 c1 r1,CNP n2 c2 r2) = 
55754  264 
(if n1 = n2 then 
265 
let c = c1 +\<^sub>p c2 

266 
in if c = 0\<^sub>p then tmadd(r1,r2) else CNP n1 c (tmadd (r1, r2)) 

267 
else if n1 \<le> n2 then (CNP n1 c1 (tmadd (r1,CNP n2 c2 r2))) 

268 
else (CNP n2 c2 (tmadd (CNP n1 c1 r1, r2))))" 

269 
"tmadd (CNP n1 c1 r1, t) = CNP n1 c1 (tmadd (r1, t))" 

270 
"tmadd (t, CNP n2 c2 r2) = CNP n2 c2 (tmadd (t, r2))" 

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

271 
"tmadd (CP b1, CP b2) = CP (b1 +\<^sub>p b2)" 
55754  272 
"tmadd (a, b) = Add a b" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

273 

55754  274 
lemma tmadd[simp]: "Itm vs bs (tmadd (t, s)) = Itm vs bs (Add t s)" 
275 
apply (induct t s rule: tmadd.induct, simp_all add: Let_def) 

276 
apply (case_tac "c1 +\<^sub>p c2 = 0\<^sub>p",case_tac "n1 \<le> n2", simp_all) 

277 
apply (case_tac "n1 = n2", simp_all add: field_simps) 

278 
apply (simp only: distrib_left[symmetric]) 

279 
apply (auto simp del: polyadd simp add: polyadd[symmetric]) 

280 
done 

281 

282 
lemma tmadd_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 s \<Longrightarrow> tmbound0 (tmadd (t, s))" 

283 
by (induct t s rule: tmadd.induct) (auto simp add: Let_def) 

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

284 

55754  285 
lemma tmadd_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n s \<Longrightarrow> tmbound n (tmadd (t, s))" 
286 
by (induct t s rule: tmadd.induct) (auto simp add: Let_def) 

287 

288 
lemma tmadd_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n s \<Longrightarrow> tmboundslt n (tmadd (t, s))" 

289 
by (induct t s rule: tmadd.induct) (auto simp add: Let_def) 

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

290 

55754  291 
lemma tmadd_allpolys_npoly[simp]: 
292 
"allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmadd(t, s))" 

293 
by (induct t s rule: tmadd.induct) (simp_all add: Let_def polyadd_norm) 

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

294 

55754  295 
fun tmmul:: "tm \<Rightarrow> poly \<Rightarrow> tm" 
296 
where 

55768  297 
"tmmul (CP j) = (\<lambda>i. CP (i *\<^sub>p j))" 
298 
 "tmmul (CNP n c a) = (\<lambda>i. CNP n (i *\<^sub>p c) (tmmul a i))" 

299 
 "tmmul t = (\<lambda>i. Mul i t)" 

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

300 

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

301 
lemma tmmul[simp]: "Itm vs bs (tmmul t i) = Itm vs bs (Mul i t)" 
55754  302 
by (induct t arbitrary: i rule: tmmul.induct) (simp_all add: field_simps) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

303 

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

304 
lemma tmmul_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 (tmmul t i)" 
55754  305 
by (induct t arbitrary: i rule: tmmul.induct) auto 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

306 

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

307 
lemma tmmul_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n (tmmul t i)" 
55754  308 
by (induct t arbitrary: n rule: tmmul.induct) auto 
309 

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

310 
lemma tmmul_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n (tmmul t i)" 
55754  311 
by (induct t arbitrary: i rule: tmmul.induct) (auto simp add: Let_def) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

312 

55754  313 
lemma tmmul_allpolys_npoly[simp]: 
36409  314 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
55754  315 
shows "allpolys isnpoly t \<Longrightarrow> isnpoly c \<Longrightarrow> allpolys isnpoly (tmmul t c)" 
316 
by (induct t rule: tmmul.induct) (simp_all add: Let_def polymul_norm) 

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

317 

55754  318 
definition tmneg :: "tm \<Rightarrow> tm" 
319 
where "tmneg t \<equiv> tmmul t (C ( 1,1))" 

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

320 

55754  321 
definition tmsub :: "tm \<Rightarrow> tm \<Rightarrow> tm" 
322 
where "tmsub s t \<equiv> (if s = t then CP 0\<^sub>p else tmadd (s, tmneg t))" 

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

323 

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

324 
lemma tmneg[simp]: "Itm vs bs (tmneg t) = Itm vs bs (Neg t)" 
55754  325 
using tmneg_def[of t] by simp 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

326 

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

327 
lemma tmneg_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 (tmneg t)" 
55754  328 
using tmneg_def by simp 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

329 

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

330 
lemma tmneg_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n (tmneg t)" 
55754  331 
using tmneg_def by simp 
332 

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

333 
lemma tmneg_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n (tmneg t)" 
55754  334 
using tmneg_def by simp 
335 

336 
lemma [simp]: "isnpoly (C (1, 1))" 

337 
unfolding isnpoly_def by simp 

338 

339 
lemma tmneg_allpolys_npoly[simp]: 

36409  340 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
55754  341 
shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly (tmneg t)" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

343 

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

344 
lemma tmsub[simp]: "Itm vs bs (tmsub a b) = Itm vs bs (Sub a b)" 
55754  345 
using tmsub_def by simp 
346 

347 
lemma tmsub_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 s \<Longrightarrow> tmbound0 (tmsub t s)" 

348 
using tmsub_def by simp 

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

349 

55754  350 
lemma tmsub_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n s \<Longrightarrow> tmbound n (tmsub t s)" 
351 
using tmsub_def by simp 

352 

353 
lemma tmsub_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n s \<Longrightarrow> tmboundslt n (tmsub t s)" 

354 
using tmsub_def by simp 

355 

356 
lemma tmsub_allpolys_npoly[simp]: 

36409  357 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
55754  358 
shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmsub t s)" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

360 

55754  361 
fun simptm :: "tm \<Rightarrow> tm" 
362 
where 

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

363 
"simptm (CP j) = CP (polynate j)" 
50282
fe4d4bb9f4c2
more robust syntax that survives collapse of \<^isub> and \<^sub>;
wenzelm
parents:
50045
diff
changeset

364 
 "simptm (Bound n) = CNP n (1)\<^sub>p (CP 0\<^sub>p)" 
41821  365 
 "simptm (Neg t) = tmneg (simptm t)" 
366 
 "simptm (Add t s) = tmadd (simptm t,simptm s)" 

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

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

370 
 "simptm (CNP n c t) = 

371 
(let c' = polynate c in if c' = 0\<^sub>p then simptm t else tmadd (CNP n c' (CP 0\<^sub>p ), simptm t))" 

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

372 

55754  373 
lemma polynate_stupid: 
36409  374 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
45499
849d697adf1e
Parametric_Ferrante_Rackoff.thy: restrict to class number_ring, replace '1+1' with '2' everywhere
huffman
parents:
44064
diff
changeset

375 
shows "polynate t = 0\<^sub>p \<Longrightarrow> Ipoly bs t = (0::'a)" 
55754  376 
apply (subst polynate[symmetric]) 
377 
apply simp 

378 
done 

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

379 

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

380 
lemma simptm_ci[simp]: "Itm vs bs (simptm t) = Itm vs bs t" 
55768  381 
by (induct t rule: simptm.induct) (auto simp add: Let_def polynate_stupid) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

382 

55754  383 
lemma simptm_tmbound0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 (simptm t)" 
384 
by (induct t rule: simptm.induct) (auto simp add: Let_def) 

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

385 

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

386 
lemma simptm_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n (simptm t)" 
55754  387 
by (induct t rule: simptm.induct) (auto simp add: Let_def) 
388 

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

389 
lemma simptm_nlt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n (simptm t)" 
55754  390 
by (induct t rule: simptm.induct) (auto simp add: Let_def) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

391 

55754  392 
lemma [simp]: "isnpoly 0\<^sub>p" 
393 
and [simp]: "isnpoly (C(1,1))" 

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

394 
by (simp_all add: isnpoly_def) 
55754  395 

396 
lemma simptm_allpolys_npoly[simp]: 

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

398 
shows "allpolys isnpoly (simptm p)" 
55754  399 
by (induct p rule: simptm.induct) (auto simp add: Let_def) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

400 

41822  401 
declare let_cong[fundef_cong del] 
402 

55754  403 
fun split0 :: "tm \<Rightarrow> (poly \<times> tm)" 
404 
where 

50282
fe4d4bb9f4c2
more robust syntax that survives collapse of \<^isub> and \<^sub>;
wenzelm
parents:
50045
diff
changeset

405 
"split0 (Bound 0) = ((1)\<^sub>p, CP 0\<^sub>p)" 
55754  406 
 "split0 (CNP 0 c t) = (let (c', t') = split0 t in (c +\<^sub>p c', t'))" 
407 
 "split0 (Neg t) = (let (c, t') = split0 t in (~\<^sub>p c, Neg t'))" 

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

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

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

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

41822  412 
 "split0 t = (0\<^sub>p, t)" 
413 

414 
declare let_cong[fundef_cong] 

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

415 

55754  416 
lemma split0_stupid[simp]: "\<exists>x y. (x, y) = split0 p" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

417 
apply (rule exI[where x="fst (split0 p)"]) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

418 
apply (rule exI[where x="snd (split0 p)"]) 
55754  419 
apply simp 
420 
done 

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

421 

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

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

423 
"tmbound 0 (snd (split0 t)) \<and> (Itm vs bs (CNP 0 (fst (split0 t)) (snd (split0 t))) = Itm vs bs t)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

424 
apply (induct t rule: split0.induct) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

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

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

430 
apply (simp add: Let_def split_def field_simps) 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
48562
diff
changeset

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

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

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

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

435 

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

436 
lemma split0_ci: "split0 t = (c',t') \<Longrightarrow> Itm vs bs t = Itm vs bs (CNP 0 c' t')" 
55754  437 
proof  
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

438 
fix c' t' 
55754  439 
assume "split0 t = (c', t')" 
55768  440 
then have "c' = fst (split0 t)" and "t' = snd (split0 t)" 
55754  441 
by auto 
55768  442 
with split0[where t="t" and bs="bs"] 
443 
show "Itm vs bs t = Itm vs bs (CNP 0 c' t')" 

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

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

446 

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

449 
shows "split0 t = (c',t') \<Longrightarrow> tmbound 0 t'" 
55754  450 
proof  
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

451 
fix c' t' 
55754  452 
assume "split0 t = (c', t')" 
55768  453 
then have "c' = fst (split0 t)" and "t' = snd (split0 t)" 
55754  454 
by auto 
455 
with conjunct1[OF split0[where t="t"]] show "tmbound 0 t'" 

456 
by simp 

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

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

458 

55754  459 
lemma split0_nb0'[simp]: 
460 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 

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

461 
shows "tmbound0 (snd (split0 t))" 
55754  462 
using split0_nb0[of t "fst (split0 t)" "snd (split0 t)"] 
463 
by (simp add: tmbound0_tmbound_iff) 

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

464 

55754  465 
lemma split0_nb: 
466 
assumes nb: "tmbound n t" 

467 
shows "tmbound n (snd (split0 t))" 

468 
using nb by (induct t rule: split0.induct) (auto simp add: Let_def split_def) 

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

469 

55754  470 
lemma split0_blt: 
471 
assumes nb: "tmboundslt n t" 

472 
shows "tmboundslt n (snd (split0 t))" 

473 
using nb by (induct t rule: split0.induct) (auto simp add: Let_def split_def) 

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

474 

55754  475 
lemma tmbound_split0: "tmbound 0 t \<Longrightarrow> Ipoly vs (fst (split0 t)) = 0" 
476 
by (induct t rule: split0.induct) (auto simp add: Let_def split_def) 

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

477 

55754  478 
lemma tmboundslt_split0: "tmboundslt n t \<Longrightarrow> Ipoly vs (fst (split0 t)) = 0 \<or> n > 0" 
479 
by (induct t rule: split0.induct) (auto simp add: Let_def split_def) 

480 

481 
lemma tmboundslt0_split0: "tmboundslt 0 t \<Longrightarrow> Ipoly vs (fst (split0 t)) = 0" 

482 
by (induct t rule: split0.induct) (auto simp add: Let_def split_def) 

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

483 

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

484 
lemma allpolys_split0: "allpolys isnpoly p \<Longrightarrow> allpolys isnpoly (snd (split0 p))" 
55754  485 
by (induct p rule: split0.induct) (auto simp add: isnpoly_def Let_def split_def) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

486 

55754  487 
lemma isnpoly_fst_split0: 
488 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 

489 
shows "allpolys isnpoly p \<Longrightarrow> isnpoly (fst (split0 p))" 

490 
by (induct p rule: split0.induct) 

491 
(auto simp add: polyadd_norm polysub_norm polyneg_norm polymul_norm Let_def split_def) 

492 

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

493 

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

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

495 

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

496 
datatype fm = T F Le tm  Lt tm  Eq tm  NEq tm 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

497 
NOT fm And fm fm Or fm fm Imp fm fm Iff fm fm E fm A fm 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

498 

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

499 

55754  500 
(* A size for fm *) 
501 
fun fmsize :: "fm \<Rightarrow> nat" 

502 
where 

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

503 
"fmsize (NOT p) = 1 + fmsize p" 
41822  504 
 "fmsize (And p q) = 1 + fmsize p + fmsize q" 
505 
 "fmsize (Or p q) = 1 + fmsize p + fmsize q" 

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

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

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

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

510 
 "fmsize p = 1" 

55754  511 

512 
(* several lemmas about fmsize *) 

513 
lemma fmsize_pos[termination_simp]: "fmsize p > 0" 

514 
by (induct p rule: fmsize.induct) simp_all 

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

515 

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

516 
(* Semantics of formulae (fm) *) 
55768  517 
primrec Ifm ::"'a::{linordered_field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool" 
518 
where 

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

519 
"Ifm vs bs T = True" 
39246  520 
 "Ifm vs bs F = False" 
521 
 "Ifm vs bs (Lt a) = (Itm vs bs a < 0)" 

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

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

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

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

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

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

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

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

55754  530 
 "Ifm vs bs (E p) = (\<exists>x. Ifm vs (x#bs) p)" 
531 
 "Ifm vs bs (A p) = (\<forall>x. Ifm vs (x#bs) p)" 

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

532 

55768  533 
fun not:: "fm \<Rightarrow> fm" 
534 
where 

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

535 
"not (NOT (NOT p)) = not p" 
41822  536 
 "not (NOT p) = p" 
537 
 "not T = F" 

538 
 "not F = T" 

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

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

541 
 "not (Eq t) = NEq t" 

542 
 "not (NEq t) = Eq t" 

543 
 "not p = NOT p" 

55754  544 

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

545 
lemma not[simp]: "Ifm vs bs (not p) = Ifm vs bs (NOT p)" 
55754  546 
by (induct p rule: not.induct) auto 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

547 

55754  548 
definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm" 
549 
where 

550 
"conj p q \<equiv> 

551 
(if p = F \<or> q = F then F 

552 
else if p = T then q 

553 
else if q = T then p 

554 
else if p = q then p 

555 
else And p q)" 

556 

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

557 
lemma conj[simp]: "Ifm vs bs (conj p q) = Ifm vs bs (And p q)" 
55754  558 
by (cases "p=F \<or> q=F", simp_all add: conj_def) (cases p, simp_all) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

559 

55754  560 
definition disj :: "fm \<Rightarrow> fm \<Rightarrow> fm" 
561 
where 

562 
"disj p q \<equiv> 

563 
(if (p = T \<or> q = T) then T 

564 
else if p = F then q 

565 
else if q = F then p 

566 
else if p = q then p 

567 
else Or p q)" 

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

568 

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

569 
lemma disj[simp]: "Ifm vs bs (disj p q) = Ifm vs bs (Or p q)" 
55768  570 
by (cases "p = T \<or> q = T", simp_all add: disj_def) (cases p, simp_all) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

571 

55754  572 
definition imp :: "fm \<Rightarrow> fm \<Rightarrow> fm" 
573 
where 

574 
"imp p q \<equiv> 

575 
(if p = F \<or> q = T \<or> p = q then T 

576 
else if p = T then q 

577 
else if q = F then not p 

578 
else Imp p q)" 

579 

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

580 
lemma imp[simp]: "Ifm vs bs (imp p q) = Ifm vs bs (Imp p q)" 
55768  581 
by (cases "p = F \<or> q = T") (simp_all add: imp_def) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

582 

55754  583 
definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm" 
584 
where 

585 
"iff p q \<equiv> 

586 
(if p = q then T 

587 
else if p = NOT q \<or> NOT p = q then F 

588 
else if p = F then not q 

589 
else if q = F then not p 

590 
else if p = T then q 

591 
else if q = T then p 

592 
else Iff p q)" 

593 

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

594 
lemma iff[simp]: "Ifm vs bs (iff p q) = Ifm vs bs (Iff p q)" 
55768  595 
by (unfold iff_def, cases "p = q", simp, cases "p = NOT q", simp) (cases "NOT p= q", auto) 
41822  596 

55754  597 
(* Quantifier freeness *) 
598 
fun qfree:: "fm \<Rightarrow> bool" 

599 
where 

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

600 
"qfree (E p) = False" 
41822  601 
 "qfree (A p) = False" 
55754  602 
 "qfree (NOT p) = qfree p" 
603 
 "qfree (And p q) = (qfree p \<and> qfree q)" 

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

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

41822  606 
 "qfree (Iff p q) = (qfree p \<and> qfree q)" 
607 
 "qfree p = True" 

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

608 

55754  609 
(* Boundedness and substitution *) 
610 
primrec boundslt :: "nat \<Rightarrow> fm \<Rightarrow> bool" 

611 
where 

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

612 
"boundslt n T = True" 
39246  613 
 "boundslt n F = True" 
55768  614 
 "boundslt n (Lt t) = tmboundslt n t" 
615 
 "boundslt n (Le t) = tmboundslt n t" 

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

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

39246  618 
 "boundslt n (NOT p) = boundslt n p" 
619 
 "boundslt n (And p q) = (boundslt n p \<and> boundslt n q)" 

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

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

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

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

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

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

625 

55754  626 
fun bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *) 
627 
where 

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

628 
"bound0 T = True" 
41822  629 
 "bound0 F = True" 
630 
 "bound0 (Lt a) = tmbound0 a" 

631 
 "bound0 (Le a) = tmbound0 a" 

632 
 "bound0 (Eq a) = tmbound0 a" 

633 
 "bound0 (NEq a) = tmbound0 a" 

634 
 "bound0 (NOT p) = bound0 p" 

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

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

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

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

639 
 "bound0 p = False" 

55754  640 

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

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

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

643 
shows "Ifm vs (b#bs) p = Ifm vs (b'#bs) p" 
55754  644 
using bp tmbound0_I[where b="b" and bs="bs" and b'="b'"] 
645 
by (induct p rule: bound0.induct) auto 

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

646 

55754  647 
primrec bound:: "nat \<Rightarrow> fm \<Rightarrow> bool" (* A Formula is independent of Bound n *) 
648 
where 

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

649 
"bound m T = True" 
39246  650 
 "bound m F = True" 
651 
 "bound m (Lt t) = tmbound m t" 

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

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

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

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

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

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

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

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

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

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

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

662 

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

663 
lemma bound_I: 
55754  664 
assumes bnd: "boundslt (length bs) p" 
665 
and nb: "bound n p" 

666 
and le: "n \<le> length bs" 

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

667 
shows "Ifm vs (bs[n:=x]) p = Ifm vs bs p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

668 
using bnd nb le tmbound_I[where bs=bs and vs = vs] 
55754  669 
proof (induct p arbitrary: bs n rule: fm.induct) 
670 
case (E p bs n) 

671 
{ 

672 
fix y 

673 
from E have bnd: "boundslt (length (y#bs)) p" 

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

674 
and nb: "bound (Suc n) p" and le: "Suc n \<le> length (y#bs)" by simp+ 
55754  675 
from E.hyps[OF bnd nb le tmbound_I] have "Ifm vs ((y#bs)[Suc n:=x]) p = Ifm vs (y#bs) p" . 
676 
} 

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

678 
next 
55754  679 
case (A p bs n) 
680 
{ 

681 
fix y 

682 
from A have bnd: "boundslt (length (y#bs)) p" 

683 
and nb: "bound (Suc n) p" 

684 
and le: "Suc n \<le> length (y#bs)" 

685 
by simp_all 

686 
from A.hyps[OF bnd nb le tmbound_I] have "Ifm vs ((y#bs)[Suc n:=x]) p = Ifm vs (y#bs) p" . 

687 
} 

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

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

690 

55768  691 
fun decr0 :: "fm \<Rightarrow> fm" 
692 
where 

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

693 
"decr0 (Lt a) = Lt (decrtm0 a)" 
41822  694 
 "decr0 (Le a) = Le (decrtm0 a)" 
695 
 "decr0 (Eq a) = Eq (decrtm0 a)" 

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

55754  697 
 "decr0 (NOT p) = NOT (decr0 p)" 
41822  698 
 "decr0 (And p q) = conj (decr0 p) (decr0 q)" 
699 
 "decr0 (Or p q) = disj (decr0 p) (decr0 q)" 

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

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

702 
 "decr0 p = p" 

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

703 

55754  704 
lemma decr0: 
705 
assumes nb: "bound0 p" 

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

706 
shows "Ifm vs (x#bs) p = Ifm vs bs (decr0 p)" 
55754  707 
using nb 
708 
by (induct p rule: decr0.induct) (simp_all add: decrtm0) 

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

709 

55754  710 
primrec decr :: "nat \<Rightarrow> fm \<Rightarrow> fm" 
711 
where 

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

712 
"decr m T = T" 
39246  713 
 "decr m F = F" 
714 
 "decr m (Lt t) = (Lt (decrtm m t))" 

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

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

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

55754  718 
 "decr m (NOT p) = NOT (decr m p)" 
39246  719 
 "decr m (And p q) = conj (decr m p) (decr m q)" 
720 
 "decr m (Or p q) = disj (decr m p) (decr m q)" 

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

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

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

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

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

725 

55754  726 
lemma decr: 
727 
assumes bnd: "boundslt (length bs) p" 

728 
and nb: "bound m p" 

729 
and nle: "m < length bs" 

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

730 
shows "Ifm vs (removen m bs) (decr m p) = Ifm vs bs p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

731 
using bnd nb nle 
55754  732 
proof (induct p arbitrary: bs m rule: fm.induct) 
733 
case (E p bs m) 

734 
{ fix x 

735 
from E 

736 
have bnd: "boundslt (length (x#bs)) p" 

737 
and nb: "bound (Suc m) p" 

738 
and nle: "Suc m < length (x#bs)" 

739 
by auto 

740 
from E(1)[OF bnd nb nle] 

741 
have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p" . 

742 
} 

55768  743 
then show ?case by auto 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

744 
next 
55754  745 
case (A p bs m) 
746 
{ fix x 

747 
from A 

748 
have bnd: "boundslt (length (x#bs)) p" 

749 
and nb: "bound (Suc m) p" 

750 
and nle: "Suc m < length (x#bs)" 

751 
by auto 

752 
from A(1)[OF bnd nb nle] 

753 
have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p" . 

754 
} 

55768  755 
then show ?case by auto 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

757 

55754  758 
primrec subst0 :: "tm \<Rightarrow> fm \<Rightarrow> fm" 
759 
where 

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

760 
"subst0 t T = T" 
39246  761 
 "subst0 t F = F" 
762 
 "subst0 t (Lt a) = Lt (tmsubst0 t a)" 

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

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

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

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

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

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

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

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

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

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

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

773 

55754  774 
lemma subst0: 
775 
assumes qf: "qfree p" 

776 
shows "Ifm vs (x # bs) (subst0 t p) = Ifm vs ((Itm vs (x # bs) t) # bs) p" 

777 
using qf tmsubst0[where x="x" and bs="bs" and t="t"] 

778 
by (induct p rule: fm.induct) auto 

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

779 

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

780 
lemma subst0_nb: 
55754  781 
assumes bp: "tmbound0 t" 
782 
and qf: "qfree p" 

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

783 
shows "bound0 (subst0 t p)" 
55754  784 
using qf tmsubst0_nb[OF bp] bp 
785 
by (induct p rule: fm.induct) auto 

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

786 

55754  787 
primrec subst:: "nat \<Rightarrow> tm \<Rightarrow> fm \<Rightarrow> fm" 
788 
where 

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

789 
"subst n t T = T" 
39246  790 
 "subst n t F = F" 
791 
 "subst n t (Lt a) = Lt (tmsubst n t a)" 

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

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

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

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

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

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

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

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

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

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

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

802 

55754  803 
lemma subst: 
804 
assumes nb: "boundslt (length bs) p" 

805 
and nlm: "n \<le> length bs" 

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

806 
shows "Ifm vs bs (subst n t p) = Ifm vs (bs[n:= Itm vs bs t]) p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

807 
using nb nlm 
39246  808 
proof (induct p arbitrary: bs n t rule: fm.induct) 
55754  809 
case (E p bs n) 
810 
{ 

811 
fix x 

812 
from E have bn: "boundslt (length (x#bs)) p" 

813 
by simp 

814 
from E have nlm: "Suc n \<le> length (x#bs)" 

815 
by simp 

816 
from E(1)[OF bn nlm] 

55768  817 
have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = 
818 
Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p" 

55754  819 
by simp 
55768  820 
then have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = 
821 
Ifm vs (x#bs[n:= Itm vs bs t]) p" 

55754  822 
by (simp add: incrtm0[where x="x" and bs="bs" and t="t"]) 
823 
} 

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

825 
next 
55754  826 
case (A p bs n) 
827 
{ 

828 
fix x 

829 
from A have bn: "boundslt (length (x#bs)) p" 

830 
by simp 

831 
from A have nlm: "Suc n \<le> length (x#bs)" 

832 
by simp 

833 
from A(1)[OF bn nlm] 

55768  834 
have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = 
835 
Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p" 

55754  836 
by simp 
55768  837 
then have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = 
838 
Ifm vs (x#bs[n:= Itm vs bs t]) p" 

55754  839 
by (simp add: incrtm0[where x="x" and bs="bs" and t="t"]) 
840 
} 

55768  841 
then show ?case by simp 
55754  842 
qed (auto simp add: tmsubst) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

843 

55754  844 
lemma subst_nb: 
845 
assumes tnb: "tmbound m t" 

846 
shows "bound m (subst m t p)" 

847 
using tnb tmsubst_nb incrtm0_tmbound 

848 
by (induct p arbitrary: m t rule: fm.induct) auto 

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

849 

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

850 
lemma not_qf[simp]: "qfree p \<Longrightarrow> qfree (not p)" 
55754  851 
by (induct p rule: not.induct) auto 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

852 
lemma not_bn0[simp]: "bound0 p \<Longrightarrow> bound0 (not p)" 
55754  853 
by (induct p rule: not.induct) auto 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

854 
lemma not_nb[simp]: "bound n p \<Longrightarrow> bound n (not p)" 
55754  855 
by (induct p rule: not.induct) auto 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

856 
lemma not_blt[simp]: "boundslt n p \<Longrightarrow> boundslt n (not p)" 
55754  857 
by (induct p rule: not.induct) auto 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

858 

55754  859 
lemma conj_qf[simp]: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (conj p q)" 
860 
using conj_def by auto 

861 
lemma conj_nb0[simp]: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (conj p q)" 

862 
using conj_def by auto 

863 
lemma conj_nb[simp]: "bound n p \<Longrightarrow> bound n q \<Longrightarrow> bound n (conj p q)" 

864 
using conj_def by auto 

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

865 
lemma conj_blt[simp]: "boundslt n p \<Longrightarrow> boundslt n q \<Longrightarrow> boundslt n (conj p q)" 
55754  866 
using conj_def by auto 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

867 

55754  868 
lemma disj_qf[simp]: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (disj p q)" 
869 
using disj_def by auto 

870 
lemma disj_nb0[simp]: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (disj p q)" 

871 
using disj_def by auto 

872 
lemma disj_nb[simp]: "bound n p \<Longrightarrow> bound n q \<Longrightarrow> bound n (disj p q)" 

873 
using disj_def by auto 

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

874 
lemma disj_blt[simp]: "boundslt n p \<Longrightarrow> boundslt n q \<Longrightarrow> boundslt n (disj p q)" 
55754  875 
using disj_def by auto 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

876 

55754  877 
lemma imp_qf[simp]: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (imp p q)" 
55768  878 
using imp_def by (cases "p = F \<or> q = T") (simp_all add: imp_def) 
55754  879 
lemma imp_nb0[simp]: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (imp p q)" 
55768  880 
using imp_def by (cases "p = F \<or> q = T \<or> p = q") (simp_all add: imp_def) 
55754  881 
lemma imp_nb[simp]: "bound n p \<Longrightarrow> bound n q \<Longrightarrow> bound n (imp p q)" 
55768  882 
using imp_def by (cases "p = F \<or> q = T \<or> p = q") (simp_all add: imp_def) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

883 
lemma imp_blt[simp]: "boundslt n p \<Longrightarrow> boundslt n q \<Longrightarrow> boundslt n (imp p q)" 
55754  884 
using imp_def by auto 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

885 

55754  886 
lemma iff_qf[simp]: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (iff p q)" 
887 
unfolding iff_def by (cases "p = q") auto 

888 
lemma iff_nb0[simp]: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (iff p q)" 

889 
using iff_def unfolding iff_def by (cases "p = q") auto 

890 
lemma iff_nb[simp]: "bound n p \<Longrightarrow> bound n q \<Longrightarrow> bound n (iff p q)" 

891 
using iff_def unfolding iff_def by (cases "p = q") auto 

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

892 
lemma iff_blt[simp]: "boundslt n p \<Longrightarrow> boundslt n q \<Longrightarrow> boundslt n (iff p q)" 
55754  893 
using iff_def by auto 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

894 
lemma decr0_qf: "bound0 p \<Longrightarrow> qfree (decr0 p)" 
55754  895 
by (induct p) simp_all 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

896 

55754  897 
fun isatom :: "fm \<Rightarrow> bool" (* test for atomicity *) 
898 
where 

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

899 
"isatom T = True" 
41822  900 
 "isatom F = True" 
901 
 "isatom (Lt a) = True" 

902 
 "isatom (Le a) = True" 

903 
 "isatom (Eq a) = True" 

904 
 "isatom (NEq a) = True" 

905 
 "isatom p = False" 

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

906 

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

907 
lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p" 
55754  908 
by (induct p) simp_all 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

909 

55754  910 
definition djf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm" 
911 
where 

912 
"djf f p q \<equiv> 

913 
(if q = T then T 

914 
else if q = F then f p 

915 
else (let fp = f p in case fp of T \<Rightarrow> T  F \<Rightarrow> q  _ \<Rightarrow> Or (f p) q))" 

916 

917 
definition evaldjf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm" 

918 
where "evaldjf f ps \<equiv> foldr (djf f) ps F" 

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

919 

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

920 
lemma djf_Or: "Ifm vs bs (djf f p q) = Ifm vs bs (Or (f p) q)" 
55768  921 
by (cases "q=T", simp add: djf_def,cases "q=F", simp add: djf_def) 
55754  922 
(cases "f p", simp_all add: Let_def djf_def) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

923 

55754  924 
lemma evaldjf_ex: "Ifm vs bs (evaldjf f ps) \<longleftrightarrow> (\<exists>p \<in> set ps. Ifm vs bs (f p))" 
925 
by (induct ps) (simp_all add: evaldjf_def djf_Or) 

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

926 

55754  927 
lemma evaldjf_bound0: 
928 
assumes nb: "\<forall>x\<in> set xs. bound0 (f x)" 

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

929 
shows "bound0 (evaldjf f xs)" 
55754  930 
using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

931 

55754  932 
lemma evaldjf_qf: 
933 
assumes nb: "\<forall>x\<in> set xs. qfree (f x)" 

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

934 
shows "qfree (evaldjf f xs)" 
55754  935 
using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

936 

55754  937 
fun disjuncts :: "fm \<Rightarrow> fm list" 
938 
where 

939 
"disjuncts (Or p q) = disjuncts p @ disjuncts q" 

41822  940 
 "disjuncts F = []" 
941 
 "disjuncts p = [p]" 

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

942 

55754  943 
lemma disjuncts: "(\<exists>q \<in> set (disjuncts p). Ifm vs bs q) = Ifm vs bs p" 
944 
by (induct p rule: disjuncts.induct) auto 

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

945 

55754  946 
lemma disjuncts_nb: "bound0 p \<Longrightarrow> \<forall>q \<in> set (disjuncts p). bound0 q" 
947 
proof  

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

948 
assume nb: "bound0 p" 
55768  949 
then have "list_all bound0 (disjuncts p)" 
950 
by (induct p rule:disjuncts.induct) auto 

951 
then show ?thesis 

952 
by (simp only: list_all_iff) 

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

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

954 

55754  955 
lemma disjuncts_qf: "qfree p \<Longrightarrow> \<forall>q\<in> set (disjuncts p). qfree q" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

957 
assume qf: "qfree p" 
55768  958 
then have "list_all qfree (disjuncts p)" 
959 
by (induct p rule: disjuncts.induct) auto 

960 
then show ?thesis by (simp only: list_all_iff) 

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

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

962 

55768  963 
definition DJ :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm" 
964 
where "DJ f p \<equiv> evaldjf f (disjuncts p)" 

965 

966 
lemma DJ: 

967 
assumes fdj: "\<forall>p q. Ifm vs bs (f (Or p q)) = Ifm vs bs (Or (f p) (f q))" 

968 
and fF: "f F = F" 

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

969 
shows "Ifm vs bs (DJ f p) = Ifm vs bs (f p)" 
55768  970 
proof  
55754  971 
have "Ifm vs bs (DJ f p) = (\<exists>q \<in> set (disjuncts p). Ifm vs bs (f q))" 
972 
by (simp add: DJ_def evaldjf_ex) 

55768  973 
also have "\<dots> = Ifm vs bs (f p)" 
974 
using fdj fF by (induct p rule: disjuncts.induct) auto 

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

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

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

977 

55768  978 
lemma DJ_qf: 
979 
assumes fqf: "\<forall>p. qfree p \<longrightarrow> qfree (f p)" 

980 
shows "\<forall>p. qfree p \<longrightarrow> qfree (DJ f p)" 

981 
proof clarify 

982 
fix p 

983 
assume qf: "qfree p" 

984 
have th: "DJ f p = evaldjf f (disjuncts p)" 

985 
by (simp add: DJ_def) 

55754  986 
from disjuncts_qf[OF qf] have "\<forall>q\<in> set (disjuncts p). qfree q" . 
55768  987 
with fqf have th':"\<forall>q\<in> set (disjuncts p). qfree (f q)" 
988 
by blast 

989 
from evaldjf_qf[OF th'] th show "qfree (DJ f p)" 

990 
by simp 

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

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

992 

55768  993 
lemma DJ_qe: 
994 
assumes qe: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm vs bs (qe p) = Ifm vs bs (E p))" 

55754  995 
shows "\<forall>bs p. qfree p \<longrightarrow> qfree (DJ qe p) \<and> (Ifm vs bs ((DJ qe p)) = Ifm vs bs (E p))" 
55768  996 
proof clarify 
997 
fix p :: fm and bs 

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

998 
assume qf: "qfree p" 
55768  999 
from qe have qth: "\<forall>p. qfree p \<longrightarrow> qfree (qe p)" 
1000 
by blast 

1001 
from DJ_qf[OF qth] qf have qfth:"qfree (DJ qe p)" 

1002 
by auto 

1003 
have "Ifm vs bs (DJ qe p) \<longleftrightarrow> (\<exists>q\<in> set (disjuncts p). Ifm vs bs (qe q))" 

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

1004 
by (simp add: DJ_def evaldjf_ex) 
55768  1005 
also have "\<dots> = (\<exists>q \<in> set(disjuncts p). Ifm vs bs (E q))" 
1006 
using qe disjuncts_qf[OF qf] by auto 

1007 
also have "\<dots> = Ifm vs bs (E p)" 

1008 
by (induct p rule: disjuncts.induct) auto 

1009 
finally show "qfree (DJ qe p) \<and> Ifm vs bs (DJ qe p) = Ifm vs bs (E p)" 

1010 
using qfth by blast 

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

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

1012 

55768  1013 
fun conjuncts :: "fm \<Rightarrow> fm list" 
1014 
where 

1015 
"conjuncts (And p q) = conjuncts p @ conjuncts q" 

41822  1016 
 "conjuncts T = []" 
1017 
 "conjuncts p = [p]" 

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

1018 

55768  1019 
definition list_conj :: "fm list \<Rightarrow> fm" 
1020 
where "list_conj ps \<equiv> foldr conj ps T" 

1021 

1022 
definition CJNB :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm" 

1023 
where 

1024 
"CJNB f p \<equiv> 

1025 
(let cjs = conjuncts p; 

1026 
(yes, no) = partition bound0 cjs 

1027 
in conj (decr0 (list_conj yes)) (f (list_conj no)))" 

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

1028 

55754  1029 
lemma conjuncts_qf: "qfree p \<Longrightarrow> \<forall>q\<in> set (conjuncts p). qfree q" 
55768  1030 
proof  
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1031 
assume qf: "qfree p" 
55768  1032 
then have "list_all qfree (conjuncts p)" 
1033 
by (induct p rule: conjuncts.induct) auto 

1034 
then show ?thesis 

1035 
by (simp only: list_all_iff) 

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

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

1037 

55754  1038 
lemma conjuncts: "(\<forall>q\<in> set (conjuncts p). Ifm vs bs q) = Ifm vs bs p" 
55768  1039 
by (induct p rule: conjuncts.induct) auto 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1040 

55754  1041 
lemma conjuncts_nb: "bound0 p \<Longrightarrow> \<forall>q\<in> set (conjuncts p). bound0 q" 
55768  1042 
proof  
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1043 
assume nb: "bound0 p" 
55768  1044 
then have "list_all bound0 (conjuncts p)" 
1045 
by (induct p rule:conjuncts.induct) auto 

1046 
then show ?thesis 

1047 
by (simp only: list_all_iff) 

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

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

1049 

55768  1050 
fun islin :: "fm \<Rightarrow> bool" 
1051 
where 

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

1052 
"islin (And p q) = (islin p \<and> islin q \<and> p \<noteq> T \<and> p \<noteq> F \<and> q \<noteq> T \<and> q \<noteq> F)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1053 
 "islin (Or p q) = (islin p \<and> islin q \<and> p \<noteq> T \<and> p \<noteq> F \<and> q \<noteq> T \<and> q \<noteq> F)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1054 
 "islin (Eq (CNP 0 c s)) = (isnpoly c \<and> c \<noteq> 0\<^sub>p \<and> tmbound0 s \<and> allpolys isnpoly s)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1055 
 "islin (NEq (CNP 0 c s)) = (isnpoly c \<and> c \<noteq> 0\<^sub>p \<and> tmbound0 s \<and> allpolys isnpoly s)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1056 
 "islin (Lt (CNP 0 c s)) = (isnpoly c \<and> c \<noteq> 0\<^sub>p \<and> tmbound0 s \<and> allpolys isnpoly s)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1057 
 "islin (Le (CNP 0 c s)) = (isnpoly c \<and> c \<noteq> 0\<^sub>p \<and> tmbound0 s \<and> allpolys isnpoly s)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

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

1062 

55768  1063 
lemma islin_stupid: 
1064 
assumes nb: "tmbound0 p" 

1065 
shows "islin (Lt p)" 

1066 
and "islin (Le p)" 

1067 
and "islin (Eq p)" 

1068 
and "islin (NEq p)" 

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

1069 
using nb by (cases p, auto, case_tac nat, auto)+ 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1070 

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

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

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

1074 
definition "neq p = not (eq p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1075 

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

1076 
lemma lt: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (lt p) = Ifm vs bs (Lt p)" 
55768  1077 
apply (simp add: lt_def) 
1078 
apply (cases p) 

1079 
apply simp_all 

1080 
apply (case_tac poly) 

1081 
apply (simp_all add: isnpoly_def) 

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

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

1083 

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

1084 
lemma le: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (le p) = Ifm vs bs (Le p)" 
55768  1085 
apply (simp add: le_def) 
1086 
apply (cases p) 

1087 
apply simp_all 

1088 
apply (case_tac poly) 

1089 
apply (simp_all add: isnpoly_def) 

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

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

1091 

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

1092 
lemma eq: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (eq p) = Ifm vs bs (Eq p)" 
55768  1093 
apply (simp add: eq_def) 
1094 
apply (cases p) 

1095 
apply simp_all 

1096 
apply (case_tac poly) 

1097 
apply (simp_all add: isnpoly_def) 

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

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

1099 

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

1100 
lemma neq: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (neq p) = Ifm vs bs (NEq p)" 
55768  1101 
by (simp add: neq_def eq) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1102 

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

1103 
lemma lt_lin: "tmbound0 p \<Longrightarrow> islin (lt p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1104 
apply (simp add: lt_def) 
55768  1105 
apply (cases p) 
1106 
apply simp_all 

1107 
apply (case_tac poly) 

1108 
apply simp_all 

1109 
apply (case_tac nat) 

1110 
apply simp_all 

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

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

1112 

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

1113 
lemma le_lin: "tmbound0 p \<Longrightarrow> islin (le p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1114 
apply (simp add: le_def) 
55768  1115 
apply (cases p) 
1116 
apply simp_all 

1117 
apply (case_tac poly) 

1118 
apply simp_all 

1119 
apply (case_tac nat) 

1120 
apply simp_all 

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

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

1122 

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

1123 
lemma eq_lin: "tmbound0 p \<Longrightarrow> islin (eq p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1124 
apply (simp add: eq_def) 
55768  1125 
apply (cases p) 
1126 
apply simp_all 

1127 
apply (case_tac poly) 

1128 
apply simp_all 

1129 
apply (case_tac nat) 

1130 
apply simp_all 

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

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

1132 

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

1133 
lemma neq_lin: "tmbound0 p \<Longrightarrow> islin (neq p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1134 
apply (simp add: neq_def eq_def) 
55768  1135 
apply (cases p) 
1136 
apply simp_all 

1137 
apply (case_tac poly) 

1138 
apply simp_all 

1139 
apply (case_tac nat) 

1140 
apply simp_all 

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

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

1142 

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

1143 
definition "simplt t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then lt s else Lt (CNP 0 c s))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1144 
definition "simple t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then le s else Le (CNP 0 c s))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1145 
definition "simpeq t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then eq s else Eq (CNP 0 c s))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1146 
definition "simpneq t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then neq s else NEq (CNP 0 c s))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1147 

55768  1148 
lemma simplt_islin[simp]: 
1149 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 

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

1150 
shows "islin (simplt t)" 
55754  1151 
unfolding simplt_def 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
pare 