author  wenzelm 
Tue, 25 Feb 2014 23:12:48 +0100  
changeset 55754  d14072d53c1e 
parent 55422  6445a05a1234 
child 55768  72c6ce5aea2a 
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 

161 
thus ?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) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

164 
{assume nxs: "n \<ge> length (x#xs)" hence ?case using removen_same[OF nxs] by simp} 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

171 
moreover 
55754  172 
{assume mxs: "\<not> (m \<le> length (x#xs))" 
173 
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

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

175 
with mxs have mxs':"m \<ge> length (removen n (x#xs))" by auto 
55754  176 
hence "(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

177 
using th nth_length_exceeds[OF mxs'] by auto 
55754  178 
hence 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

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

180 
hence ?case using nxs mln mxs by auto } 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

181 
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

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

183 
ultimately have ?case by blast 
41807  184 
} 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

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

186 

55754  187 
lemma decrtm: 
188 
assumes bnd: "tmboundslt (length bs) t" 

189 
and nb: "tmbound m t" 

190 
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

191 
shows "Itm vs (removen m bs) (decrtm m t) = Itm vs bs t" 
41807  192 
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

193 

55754  194 
primrec tmsubst0:: "tm \<Rightarrow> tm \<Rightarrow> tm" 
195 
where 

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

196 
"tmsubst0 t (CP c) = CP c" 
39246  197 
 "tmsubst0 t (Bound n) = (if n=0 then t else Bound n)" 
198 
 "tmsubst0 t (CNP n c a) = (if n=0 then Add (Mul c t) (tmsubst0 t a) else CNP n c (tmsubst0 t a))" 

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

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

55754  201 
 "tmsubst0 t (Sub a b) = Sub (tmsubst0 t a) (tmsubst0 t b)" 
39246  202 
 "tmsubst0 t (Mul i a) = Mul i (tmsubst0 t a)" 
55754  203 

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

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

206 

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

207 
lemma tmsubst0_nb: "tmbound0 t \<Longrightarrow> tmbound0 (tmsubst0 t a)" 
41842  208 
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

209 

55754  210 
primrec tmsubst:: "nat \<Rightarrow> 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 
"tmsubst n t (CP c) = CP c" 
39246  213 
 "tmsubst n t (Bound m) = (if n=m then t else Bound m)" 
55754  214 
 "tmsubst n t (CNP m c a) = 
215 
(if n = m then Add (Mul c t) (tmsubst n t a) else CNP m c (tmsubst n t a))" 

39246  216 
 "tmsubst n t (Neg a) = Neg (tmsubst n t a)" 
217 
 "tmsubst n t (Add a b) = Add (tmsubst n t a) (tmsubst n t b)" 

55754  218 
 "tmsubst n t (Sub a b) = Sub (tmsubst n t a) (tmsubst n t b)" 
39246  219 
 "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

220 

55754  221 
lemma tmsubst: 
222 
assumes nb: "tmboundslt (length bs) a" 

223 
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

224 
shows "Itm vs bs (tmsubst n t a) = Itm vs (bs[n:= Itm vs bs t]) a" 
55754  225 
using nb nlt 
226 
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

227 

55754  228 
lemma tmsubst_nb0: 
229 
assumes tnb: "tmbound0 t" 

230 
shows "tmbound0 (tmsubst 0 t a)" 

231 
using tnb 

232 
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

233 

55754  234 
lemma tmsubst_nb: 
235 
assumes tnb: "tmbound m t" 

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

237 
using tnb 

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

239 

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

240 
lemma incrtm0_tmbound: "tmbound n t \<Longrightarrow> tmbound (Suc n) (incrtm0 t)" 
55754  241 
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

242 

55754  243 
(* Simplification *) 
244 

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

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

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

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

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

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

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

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

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

255 
"tmadd (CP b1, CP b2) = CP (b1 +\<^sub>p b2)" 
55754  256 
"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

257 

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

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

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

262 
apply (simp only: distrib_left[symmetric]) 

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

264 
done 

265 

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

267 
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

268 

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

271 

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

273 
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

274 

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

277 
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

278 

55754  279 
fun tmmul:: "tm \<Rightarrow> poly \<Rightarrow> tm" 
280 
where 

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

281 
"tmmul (CP j) = (\<lambda> i. CP (i *\<^sub>p j))" 
41821  282 
 "tmmul (CNP n c a) = (\<lambda> i. CNP n (i *\<^sub>p c) (tmmul a i))" 
283 
 "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

284 

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

285 
lemma tmmul[simp]: "Itm vs bs (tmmul t i) = Itm vs bs (Mul i t)" 
55754  286 
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

287 

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

288 
lemma tmmul_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 (tmmul t i)" 
55754  289 
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

290 

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

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

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

294 
lemma tmmul_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n (tmmul t i)" 
55754  295 
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

296 

55754  297 
lemma tmmul_allpolys_npoly[simp]: 
36409  298 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
55754  299 
shows "allpolys isnpoly t \<Longrightarrow> isnpoly c \<Longrightarrow> allpolys isnpoly (tmmul t c)" 
300 
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

301 

55754  302 
definition tmneg :: "tm \<Rightarrow> tm" 
303 
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

304 

55754  305 
definition tmsub :: "tm \<Rightarrow> tm \<Rightarrow> tm" 
306 
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

307 

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

308 
lemma tmneg[simp]: "Itm vs bs (tmneg t) = Itm vs bs (Neg t)" 
55754  309 
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

310 

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

311 
lemma tmneg_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 (tmneg t)" 
55754  312 
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

313 

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

314 
lemma tmneg_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n (tmneg t)" 
55754  315 
using tmneg_def by simp 
316 

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

317 
lemma tmneg_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n (tmneg t)" 
55754  318 
using tmneg_def by simp 
319 

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

321 
unfolding isnpoly_def by simp 

322 

323 
lemma tmneg_allpolys_npoly[simp]: 

36409  324 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
55754  325 
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

326 
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

327 

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

328 
lemma tmsub[simp]: "Itm vs bs (tmsub a b) = Itm vs bs (Sub a b)" 
55754  329 
using tmsub_def by simp 
330 

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

332 
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

333 

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

336 

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

338 
using tmsub_def by simp 

339 

340 
lemma tmsub_allpolys_npoly[simp]: 

36409  341 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
55754  342 
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

343 
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

344 

55754  345 
fun simptm :: "tm \<Rightarrow> tm" 
346 
where 

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

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

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

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

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

354 
 "simptm (CNP n c t) = 

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

356 

55754  357 
lemma polynate_stupid: 
36409  358 
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

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

362 
done 

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

363 

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

364 
lemma simptm_ci[simp]: "Itm vs bs (simptm t) = Itm vs bs t" 
55754  365 
by (induct t rule: simptm.induct) 
366 
(auto simp add: tmneg tmadd tmsub tmmul 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

367 

55754  368 
lemma simptm_tmbound0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 (simptm t)" 
369 
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

370 

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

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

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

374 
lemma simptm_nlt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n (simptm t)" 
55754  375 
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

376 

55754  377 
lemma [simp]: "isnpoly 0\<^sub>p" 
378 
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

379 
by (simp_all add: isnpoly_def) 
55754  380 

381 
lemma simptm_allpolys_npoly[simp]: 

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

383 
shows "allpolys isnpoly (simptm p)" 
55754  384 
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

385 

41822  386 
declare let_cong[fundef_cong del] 
387 

55754  388 
fun split0 :: "tm \<Rightarrow> (poly \<times> tm)" 
389 
where 

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

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

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

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

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

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

41822  397 
 "split0 t = (0\<^sub>p, t)" 
398 

399 
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

400 

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

402 
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

403 
apply (rule exI[where x="snd (split0 p)"]) 
55754  404 
apply simp 
405 
done 

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

406 

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

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

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

409 
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

410 
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

411 
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

412 
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

413 
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

414 
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

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

416 
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

417 
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

418 
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

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

420 

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

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

423 
fix c' t' 
55754  424 
assume "split0 t = (c', t')" 
425 
hence "c' = fst (split0 t)" and "t' = snd (split0 t)" 

426 
by auto 

427 
with split0[where t="t" and bs="bs"] show "Itm vs bs t = Itm vs bs (CNP 0 c' t')" 

428 
by simp 

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

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

430 

55754  431 
lemma split0_nb0: 
36409  432 
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

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

435 
fix c' t' 
55754  436 
assume "split0 t = (c', t')" 
437 
hence "c' = fst (split0 t)" and "t' = snd (split0 t)" 

438 
by auto 

439 
with conjunct1[OF split0[where t="t"]] show "tmbound 0 t'" 

440 
by simp 

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

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

442 

55754  443 
lemma split0_nb0'[simp]: 
444 
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

445 
shows "tmbound0 (snd (split0 t))" 
55754  446 
using split0_nb0[of t "fst (split0 t)" "snd (split0 t)"] 
447 
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

448 

55754  449 
lemma split0_nb: 
450 
assumes nb: "tmbound n t" 

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

452 
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

453 

55754  454 
lemma split0_blt: 
455 
assumes nb: "tmboundslt n t" 

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

457 
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

458 

55754  459 
lemma tmbound_split0: "tmbound 0 t \<Longrightarrow> Ipoly vs (fst (split0 t)) = 0" 
460 
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

461 

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

464 

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

466 
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

467 

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

468 
lemma allpolys_split0: "allpolys isnpoly p \<Longrightarrow> allpolys isnpoly (snd (split0 p))" 
55754  469 
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

470 

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

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

474 
by (induct p rule: split0.induct) 

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

476 

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

477 

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

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

479 

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

480 
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

481 
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

482 

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

483 

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

486 
where 

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

487 
"fmsize (NOT p) = 1 + fmsize p" 
41822  488 
 "fmsize (And p q) = 1 + fmsize p + fmsize q" 
489 
 "fmsize (Or p q) = 1 + fmsize p + fmsize q" 

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

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

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

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

494 
 "fmsize p = 1" 

55754  495 

496 
(* several lemmas about fmsize *) 

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

498 
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

499 

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

500 
(* Semantics of formulae (fm) *) 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45499
diff
changeset

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

502 
"Ifm vs bs T = True" 
39246  503 
 "Ifm vs bs F = False" 
504 
 "Ifm vs bs (Lt a) = (Itm vs bs a < 0)" 

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

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

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

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

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

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

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

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

55754  513 
 "Ifm vs bs (E p) = (\<exists>x. Ifm vs (x#bs) p)" 
514 
 "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

515 

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

517 
"not (NOT (NOT p)) = not p" 
41822  518 
 "not (NOT p) = p" 
519 
 "not T = F" 

520 
 "not F = T" 

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

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

523 
 "not (Eq t) = NEq t" 

524 
 "not (NEq t) = Eq t" 

525 
 "not p = NOT p" 

55754  526 

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

527 
lemma not[simp]: "Ifm vs bs (not p) = Ifm vs bs (NOT p)" 
55754  528 
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

529 

55754  530 
definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm" 
531 
where 

532 
"conj p q \<equiv> 

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

534 
else if p = T then q 

535 
else if q = T then p 

536 
else if p = q then p 

537 
else And p q)" 

538 

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

539 
lemma conj[simp]: "Ifm vs bs (conj p q) = Ifm vs bs (And p q)" 
55754  540 
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

541 

55754  542 
definition disj :: "fm \<Rightarrow> fm \<Rightarrow> fm" 
543 
where 

544 
"disj p q \<equiv> 

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

546 
else if p = F then q 

547 
else if q = F then p 

548 
else if p = q then p 

549 
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

550 

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

551 
lemma disj[simp]: "Ifm vs bs (disj p q) = Ifm vs bs (Or p q)" 
55754  552 
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

553 

55754  554 
definition imp :: "fm \<Rightarrow> fm \<Rightarrow> fm" 
555 
where 

556 
"imp p q \<equiv> 

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

558 
else if p = T then q 

559 
else if q = F then not p 

560 
else Imp p q)" 

561 

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

562 
lemma imp[simp]: "Ifm vs bs (imp p q) = Ifm vs bs (Imp p q)" 
55754  563 
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

564 

55754  565 
definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm" 
566 
where 

567 
"iff p q \<equiv> 

568 
(if p = q then T 

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

570 
else if p = F then not q 

571 
else if q = F then not p 

572 
else if p = T then q 

573 
else if q = T then p 

574 
else Iff p q)" 

575 

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

576 
lemma iff[simp]: "Ifm vs bs (iff p q) = Ifm vs bs (Iff p q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

577 
by (unfold iff_def,cases "p=q", simp,cases "p=NOT q", simp) (cases "NOT p= q", auto) 
41822  578 

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

581 
where 

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

582 
"qfree (E p) = False" 
41822  583 
 "qfree (A p) = False" 
55754  584 
 "qfree (NOT p) = qfree p" 
585 
 "qfree (And p q) = (qfree p \<and> qfree q)" 

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

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

41822  588 
 "qfree (Iff p q) = (qfree p \<and> qfree q)" 
589 
 "qfree p = True" 

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

590 

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

593 
where 

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

594 
"boundslt n T = True" 
39246  595 
 "boundslt n F = True" 
596 
 "boundslt n (Lt t) = (tmboundslt n t)" 

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

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

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

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

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

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

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

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

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

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

607 

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

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

610 
"bound0 T = True" 
41822  611 
 "bound0 F = True" 
612 
 "bound0 (Lt a) = tmbound0 a" 

613 
 "bound0 (Le a) = tmbound0 a" 

614 
 "bound0 (Eq a) = tmbound0 a" 

615 
 "bound0 (NEq a) = tmbound0 a" 

616 
 "bound0 (NOT p) = bound0 p" 

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

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

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

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

621 
 "bound0 p = False" 

55754  622 

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

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

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

625 
shows "Ifm vs (b#bs) p = Ifm vs (b'#bs) p" 
55754  626 
using bp tmbound0_I[where b="b" and bs="bs" and b'="b'"] 
627 
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

628 

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

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

631 
"bound m T = True" 
39246  632 
 "bound m F = True" 
633 
 "bound m (Lt t) = tmbound m t" 

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

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

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

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

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

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

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

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

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

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

644 

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

645 
lemma bound_I: 
55754  646 
assumes bnd: "boundslt (length bs) p" 
647 
and nb: "bound n p" 

648 
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

649 
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

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

653 
{ 

654 
fix y 

655 
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

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

659 
thus ?case by simp 

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

660 
next 
55754  661 
case (A p bs n) 
662 
{ 

663 
fix y 

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

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

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

667 
by simp_all 

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

669 
} 

670 
thus ?case by simp 

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

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

672 

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

674 
"decr0 (Lt a) = Lt (decrtm0 a)" 
41822  675 
 "decr0 (Le a) = Le (decrtm0 a)" 
676 
 "decr0 (Eq a) = Eq (decrtm0 a)" 

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

55754  678 
 "decr0 (NOT p) = NOT (decr0 p)" 
41822  679 
 "decr0 (And p q) = conj (decr0 p) (decr0 q)" 
680 
 "decr0 (Or p q) = disj (decr0 p) (decr0 q)" 

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

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

683 
 "decr0 p = p" 

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

684 

55754  685 
lemma decr0: 
686 
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

687 
shows "Ifm vs (x#bs) p = Ifm vs bs (decr0 p)" 
55754  688 
using nb 
689 
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

690 

55754  691 
primrec decr :: "nat \<Rightarrow> 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 
"decr m T = T" 
39246  694 
 "decr m F = F" 
695 
 "decr m (Lt t) = (Lt (decrtm m t))" 

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

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

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

55754  699 
 "decr m (NOT p) = NOT (decr m p)" 
39246  700 
 "decr m (And p q) = conj (decr m p) (decr m q)" 
701 
 "decr m (Or p q) = disj (decr m p) (decr m q)" 

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

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

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

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

706 

55754  707 
lemma decr: 
708 
assumes bnd: "boundslt (length bs) p" 

709 
and nb: "bound m p" 

710 
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

711 
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

712 
using bnd nb nle 
55754  713 
proof (induct p arbitrary: bs m rule: fm.induct) 
714 
case (E p bs m) 

715 
{ fix x 

716 
from E 

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

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

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

720 
by auto 

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

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

723 
} 

724 
thus ?case by auto 

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

725 
next 
55754  726 
case (A p bs m) 
727 
{ fix x 

728 
from A 

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

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

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

732 
by auto 

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

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

735 
} 

736 
thus ?case by auto 

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

737 
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

738 

55754  739 
primrec subst0 :: "tm \<Rightarrow> fm \<Rightarrow> fm" 
740 
where 

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

741 
"subst0 t T = T" 
39246  742 
 "subst0 t F = F" 
743 
 "subst0 t (Lt a) = Lt (tmsubst0 t a)" 

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

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

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

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

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

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

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

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

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

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

754 

55754  755 
lemma subst0: 
756 
assumes qf: "qfree p" 

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

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

759 
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

760 

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

761 
lemma subst0_nb: 
55754  762 
assumes bp: "tmbound0 t" 
763 
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

764 
shows "bound0 (subst0 t p)" 
55754  765 
using qf tmsubst0_nb[OF bp] bp 
766 
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

767 

55754  768 
primrec subst:: "nat \<Rightarrow> tm \<Rightarrow> fm \<Rightarrow> fm" 
769 
where 

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

770 
"subst n t T = T" 
39246  771 
 "subst n t F = F" 
772 
 "subst n t (Lt a) = Lt (tmsubst n t a)" 

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

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

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

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

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

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

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

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

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

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

783 

55754  784 
lemma subst: 
785 
assumes nb: "boundslt (length bs) p" 

786 
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

787 
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

788 
using nb nlm 
39246  789 
proof (induct p arbitrary: bs n t rule: fm.induct) 
55754  790 
case (E p bs n) 
791 
{ 

792 
fix x 

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

794 
by simp 

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

796 
by simp 

797 
from E(1)[OF bn nlm] 

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

799 
by simp 

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

800 
hence "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs (x#bs[n:= Itm vs bs t]) p" 
55754  801 
by (simp add: incrtm0[where x="x" and bs="bs" and t="t"]) 
802 
} 

803 
thus ?case by simp 

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

804 
next 
55754  805 
case (A p bs n) 
806 
{ 

807 
fix x 

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

809 
by simp 

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

811 
by simp 

812 
from A(1)[OF bn nlm] 

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

814 
by simp 

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

815 
hence "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs (x#bs[n:= Itm vs bs t]) p" 
55754  816 
by (simp add: incrtm0[where x="x" and bs="bs" and t="t"]) 
817 
} 

818 
thus ?case by simp 

819 
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

820 

55754  821 
lemma subst_nb: 
822 
assumes tnb: "tmbound m t" 

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

824 
using tnb tmsubst_nb incrtm0_tmbound 

825 
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

826 

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

827 
lemma not_qf[simp]: "qfree p \<Longrightarrow> qfree (not p)" 
55754  828 
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

829 
lemma not_bn0[simp]: "bound0 p \<Longrightarrow> bound0 (not p)" 
55754  830 
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

831 
lemma not_nb[simp]: "bound n p \<Longrightarrow> bound n (not p)" 
55754  832 
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

833 
lemma not_blt[simp]: "boundslt n p \<Longrightarrow> boundslt n (not p)" 
55754  834 
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

835 

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

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

839 
using conj_def by auto 

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

841 
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

842 
lemma conj_blt[simp]: "boundslt n p \<Longrightarrow> boundslt n q \<Longrightarrow> boundslt n (conj p q)" 
55754  843 
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

844 

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

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

848 
using disj_def by auto 

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

850 
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

851 
lemma disj_blt[simp]: "boundslt n p \<Longrightarrow> boundslt n q \<Longrightarrow> boundslt n (disj p q)" 
55754  852 
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

853 

55754  854 
lemma imp_qf[simp]: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (imp p q)" 
855 
using imp_def by (cases "p=F \<or> q=T") (simp_all add: imp_def) 

856 
lemma imp_nb0[simp]: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (imp p q)" 

857 
using imp_def by (cases "p=F \<or> q=T \<or> p=q") (simp_all add: imp_def) 

858 
lemma imp_nb[simp]: "bound n p \<Longrightarrow> bound n q \<Longrightarrow> bound n (imp p q)" 

859 
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

860 
lemma imp_blt[simp]: "boundslt n p \<Longrightarrow> boundslt n q \<Longrightarrow> boundslt n (imp p q)" 
55754  861 
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

862 

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

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

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

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

868 
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

869 
lemma iff_blt[simp]: "boundslt n p \<Longrightarrow> boundslt n q \<Longrightarrow> boundslt n (iff p q)" 
55754  870 
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

871 
lemma decr0_qf: "bound0 p \<Longrightarrow> qfree (decr0 p)" 
55754  872 
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

873 

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

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

876 
"isatom T = True" 
41822  877 
 "isatom F = True" 
878 
 "isatom (Lt a) = True" 

879 
 "isatom (Le a) = True" 

880 
 "isatom (Eq a) = True" 

881 
 "isatom (NEq a) = True" 

882 
 "isatom p = False" 

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

883 

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

884 
lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p" 
55754  885 
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

886 

55754  887 
definition djf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm" 
888 
where 

889 
"djf f p q \<equiv> 

890 
(if q = T then T 

891 
else if q = F then f p 

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

893 

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

895 
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

896 

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

897 
lemma djf_Or: "Ifm vs bs (djf f p q) = Ifm vs bs (Or (f p) q)" 
55754  898 
by (cases "q=T", simp add: djf_def,cases "q=F",simp add: djf_def) 
899 
(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

900 

55754  901 
lemma evaldjf_ex: "Ifm vs bs (evaldjf f ps) \<longleftrightarrow> (\<exists>p \<in> set ps. Ifm vs bs (f p))" 
902 
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

903 

55754  904 
lemma evaldjf_bound0: 
905 
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

906 
shows "bound0 (evaldjf f xs)" 
55754  907 
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

908 

55754  909 
lemma evaldjf_qf: 
910 
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

911 
shows "qfree (evaldjf f xs)" 
55754  912 
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

913 

55754  914 
fun disjuncts :: "fm \<Rightarrow> fm list" 
915 
where 

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

41822  917 
 "disjuncts F = []" 
918 
 "disjuncts p = [p]" 

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

919 

55754  920 
lemma disjuncts: "(\<exists>q \<in> set (disjuncts p). Ifm vs bs q) = Ifm vs bs p" 
921 
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

922 

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

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

925 
assume nb: "bound0 p" 
55754  926 
hence "list_all bound0 (disjuncts p)" 
927 
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

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

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

930 

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

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

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

934 
hence "list_all qfree (disjuncts p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

938 

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

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

940 
"DJ f p \<equiv> evaldjf f (disjuncts p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

941 

55754  942 
lemma DJ: assumes fdj: "\<forall>p q. Ifm vs bs (f (Or p q)) = Ifm vs bs (Or (f p) (f q))" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

943 
and fF: "f F = F" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

945 
proof 
55754  946 
have "Ifm vs bs (DJ f p) = (\<exists>q \<in> set (disjuncts p). Ifm vs bs (f q))" 
947 
by (simp add: DJ_def evaldjf_ex) 

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

948 
also have "\<dots> = Ifm vs bs (f p)" using fdj fF by (induct p rule: disjuncts.induct, auto) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

951 

55754  952 
lemma DJ_qf: assumes 
953 
fqf: "\<forall>p. qfree p \<longrightarrow> qfree (f p)" 

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

954 
shows "\<forall>p. qfree p \<longrightarrow> qfree (DJ f p) " 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

957 
have th: "DJ f p = evaldjf f (disjuncts p)" by (simp add: DJ_def) 
55754  958 
from disjuncts_qf[OF qf] have "\<forall>q\<in> set (disjuncts p). qfree q" . 
959 
with fqf have th':"\<forall>q\<in> set (disjuncts p). qfree (f q)" by blast 

960 

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

961 
from evaldjf_qf[OF th'] th show "qfree (DJ f p)" by simp 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

963 

55754  964 
lemma DJ_qe: assumes qe: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm vs bs (qe p) = Ifm vs bs (E p))" 
965 
shows "\<forall>bs p. qfree p \<longrightarrow> qfree (DJ qe p) \<and> (Ifm vs bs ((DJ qe p)) = Ifm vs bs (E p))" 

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

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

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

968 
assume qf: "qfree p" 
55754  969 
from qe have qth: "\<forall>p. qfree p \<longrightarrow> qfree (qe p)" by blast 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

970 
from DJ_qf[OF qth] qf have qfth:"qfree (DJ qe p)" by auto 
55754  971 
have "Ifm vs bs (DJ qe p) = (\<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

972 
by (simp add: DJ_def evaldjf_ex) 
55754  973 
also have "\<dots> = (\<exists>q \<in> set(disjuncts p). Ifm vs bs (E q))" using qe disjuncts_qf[OF qf] by auto 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

974 
also have "\<dots> = Ifm vs bs (E p)" by (induct p rule: disjuncts.induct, auto) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

975 
finally show "qfree (DJ qe p) \<and> Ifm vs bs (DJ qe p) = Ifm vs bs (E p)" using qfth by blast 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

977 

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

979 
"conjuncts (And p q) = (conjuncts p) @ (conjuncts q)" 
41822  980 
 "conjuncts T = []" 
981 
 "conjuncts p = [p]" 

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

982 

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

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

984 
"list_conj ps \<equiv> foldr conj ps T" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

985 

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

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

987 
"CJNB f p \<equiv> (let cjs = conjuncts p ; (yes,no) = partition bound0 cjs 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

988 
in conj (decr0 (list_conj yes)) (f (list_conj no)))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

989 

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

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

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

993 
hence "list_all qfree (conjuncts p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

997 

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

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

1000 

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

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

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

1004 
hence "list_all bound0 (conjuncts p)" by (induct p rule:conjuncts.induct,auto) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

1007 

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

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

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

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

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

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

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

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

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

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

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

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

1019 

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

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

1021 
shows "islin (Lt p)" and "islin (Le p)" and "islin (Eq p)" and "islin (NEq p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1022 
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

1023 

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

1024 
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

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

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

1027 
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

1028 

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

1029 
lemma lt: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (lt p) = Ifm vs bs (Lt p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

1032 
apply (case_tac poly, simp_all add: isnpoly_def) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

1034 

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

1035 
lemma le: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (le p) = Ifm vs bs (Le p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

1038 
apply (case_tac poly, simp_all add: isnpoly_def) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

1040 

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

1041 
lemma eq: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (eq p) = Ifm vs bs (Eq p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

1044 
apply (case_tac poly, simp_all add: isnpoly_def) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

1046 

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

1047 
lemma neq: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (neq p) = Ifm vs bs (NEq p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

1049 

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

1050 
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

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

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

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

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

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

1056 

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

1057 
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

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

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

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

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

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

1063 

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

1064 
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

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

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

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

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

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

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

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

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

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

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

1077 

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

1078 
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

1079 
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

1080 
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

1081 
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

1082 

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

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

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

1087 
by (auto simp add: lt_lin Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly] islin_stupid allpolys_split0[OF simptm_allpolys_npoly]) 
55754  1088 

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

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

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

1093 
by (auto simp add: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly] islin_stupid allpolys_split0[OF simptm_allpolys_npoly] le_lin) 
36409  1094 
lemma simpeq_islin[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

1098 
by (auto simp add: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly] islin_stupid allpolys_split0[OF simptm_allpolys_npoly] eq_lin) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1099 

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

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

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

1104 
by (auto simp add: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly] islin_stupid allpolys_split0[OF simptm_allpolys_npoly] neq_lin) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1105 

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

1106 
lemma really_stupid: "\<not> (\<forall>c1 s'. (c1, s') \<noteq> split0 s)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

1109 
and n: "allpolys isnpoly t" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1110 
shows "isnpoly (fst (split0 t))" and "allpolys isnpoly (snd (split0 t))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

1112 
by (induct t rule: split0.induct, auto simp add: Let_def split_def polyadd_norm polymul_norm polyneg_norm polysub_norm really_stupid) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

1114 
shows "Ifm vs bs (simplt t) = Ifm vs bs (Lt t)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

1116 
have n: "allpolys isnpoly (simptm t)" by simp 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

1118 
{assume "fst (split0 ?t) = 0\<^sub>p" hence ?thesis 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1119 
using split0[of "simptm t" vs bs] lt[OF split0_npoly(2)[OF n], of vs bs] 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1120 
by (simp add: simplt_def Let_def split_def lt)} 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

1122 
{assume "fst (split0 ?t) \<noteq> 0\<^sub>p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1123 
hence ?thesis using split0[of "simptm t" vs bs] by (simp add: simplt_def Let_def split_def) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

1127 

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

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

1129 
shows "Ifm vs bs (simple t) = Ifm vs bs (Le t)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

1131 
have n: "allpolys isnpoly (simptm t)" by simp 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

1133 
{assume "fst (split0 ?t) = 0\<^sub>p" hence ?thesis 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1134 
using split0[of "simptm t" vs bs] le[OF split0_npoly(2)[OF n], of vs bs] 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1135 
by (simp add: simple_def Let_def split_def le)} 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

1137 
{assume "fst (split0 ?t) \<noteq> 0\<^sub>p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1138 
hence ?thesis using split0[of "simptm t" vs bs] by (simp add: simple_def Let_def split_def) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

1141 
qed 
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 
lemma simpeq[simp]: 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1144 
shows "Ifm vs bs (simpeq t) = Ifm vs bs (Eq t)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

1146 
have n: "allpolys isnpoly (simptm t)" by simp 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

1148 
{assume "fst (split0 ?t) = 0\<^sub>p" hence ?thesis 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1149 
using split0[of "simptm t" vs bs] eq[OF split0_npoly(2)[OF n], of vs bs] 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1150 
by (simp add: simpeq_def Let_def split_def)} 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

1152 
{assume "fst (split0 ?t) \<noteq> 0\<^sub>p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1153 
hence ?thesis using split0[of "simptm t" vs bs] by (simp add: simpeq_def Let_def split_def) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

1155 
ultimately show ?thesis by blast 