author  haftmann 
Fri, 05 Feb 2010 14:33:50 +0100  
changeset 35028  108662d50512 
parent 34974  18b41bba42b5 
child 35033  e47934673b74 
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 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

11 

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

12 

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

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

14 

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

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

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

17 
(* A size for poly to make inductive proofs simpler*) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

18 

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

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

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

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

22 
"tmsize (Bound n) = 1" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

23 
"tmsize (Neg a) = 1 + tmsize a" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

24 
"tmsize (Add a b) = 1 + tmsize a + tmsize b" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

25 
"tmsize (Sub a b) = 3 + tmsize a + tmsize b" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

26 
"tmsize (Mul c a) = 1 + polysize c + tmsize a" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

27 
"tmsize (CNP n c a) = 3 + polysize c + tmsize a " 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

28 

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

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

30 
consts Itm :: "'a::{ring_char_0,division_by_zero,field} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

32 
"Itm vs bs (CP c) = (Ipoly vs c)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

33 
"Itm vs bs (Bound n) = bs!n" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

34 
"Itm vs bs (Neg a) = (Itm vs bs a)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

35 
"Itm vs bs (Add a b) = Itm vs bs a + Itm vs bs b" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

36 
"Itm vs bs (Sub a b) = Itm vs bs a  Itm vs bs b" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

37 
"Itm vs bs (Mul c a) = (Ipoly vs c) * Itm vs bs a" 
33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33212
diff
changeset

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

39 

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

40 

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

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

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

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

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

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

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

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

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

49 

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

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

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

52 
tmbound0:: "tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound 0 *) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

55 
incrtm:: "nat \<Rightarrow> tm \<Rightarrow> tm" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

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

60 
"tmboundslt n (Bound m) = (m < n)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

63 
"tmboundslt n (Add a b) = (tmboundslt n a \<and> tmboundslt n b)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

64 
"tmboundslt n (Sub a b) = (tmboundslt n a \<and> tmboundslt n b)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

65 
"tmboundslt n (Mul i a) = tmboundslt n a" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

68 
"tmbound0 (Bound n) = (n>0)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

71 
"tmbound0 (Add a b) = (tmbound0 a \<and> tmbound0 b)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

72 
"tmbound0 (Sub a b) = (tmbound0 a \<and> tmbound0 b)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

76 
shows "Itm vs (b#bs) a = Itm vs (b'#bs) a" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

78 
by (induct a rule: tmbound0.induct,auto simp add: nth_pos2) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

79 

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

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

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

82 
"tmbound n (Bound m) = (n \<noteq> m)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

85 
"tmbound n (Add a b) = (tmbound n a \<and> tmbound n b)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

86 
"tmbound n (Sub a b) = (tmbound n a \<and> tmbound n b)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

87 
"tmbound n (Mul i a) = tmbound n a" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

88 
lemma tmbound0_tmbound_iff: "tmbound 0 t = tmbound0 t" by (induct t, auto) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

89 

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

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

91 
assumes bnd: "tmboundslt (length bs) t" and nb: "tmbound n t" and le: "n \<le> length bs" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

95 

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

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

97 
"decrtm0 (Bound n) = Bound (n  1)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

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

102 
"decrtm0 (CNP n c a) = CNP (n  1) c (decrtm0 a)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

105 
"incrtm0 (Bound n) = Bound (n + 1)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

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

110 
"incrtm0 (CNP n c a) = CNP (n + 1) c (incrtm0 a)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

114 
using nb by (induct t rule: decrtm0.induct, simp_all add: nth_pos2) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

115 
lemma incrtm0: "Itm vs (x#bs) (incrtm0 t) = Itm vs bs t" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

116 
by (induct t rule: decrtm0.induct, simp_all add: nth_pos2) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

117 

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

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

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

120 
"decrtm m (Bound n) = (if n < m then Bound n else Bound (n  1))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

123 
"decrtm m (Sub a b) = Sub (decrtm m a) (decrtm m b)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

124 
"decrtm m (Mul c a) = Mul c (decrtm m a)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

125 
"decrtm m (CNP n c a) = (if n < m then CNP n c (decrtm m a) else CNP (n  1) c (decrtm m a))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

126 

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

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

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

129 
"removen n [] = []" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

131 

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

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

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

134 

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

135 
lemma nth_length_exceeds: "n \<ge> length xs \<Longrightarrow> xs!n = []!(n  length xs)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

137 

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

138 
lemma removen_length: "length (removen n xs) = (if n \<ge> length xs then length xs else length xs  1)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

140 
lemma removen_nth: "(removen n xs)!m = (if n \<ge> length xs then xs!m 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

141 
else if m < n then xs!m else if m \<le> length xs then xs!(Suc m) else []!(m  (length xs  1)))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

145 
case (Cons x xs n m) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

148 
{assume nxs: "\<not> (n \<ge> length (x#xs))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

149 
{assume mln: "m < n" hence ?case using prems by (cases m, auto)} 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

151 
{assume mln: "\<not> (m < n)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

152 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

167 

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

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

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

170 

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

171 
lemma decrtm: assumes bnd: "tmboundslt (length bs) t" and nb: "tmbound m t" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

172 
and nle: "m \<le> length bs" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

173 
shows "Itm vs (removen m bs) (decrtm m t) = Itm vs bs t" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

175 
by (induct t rule: decrtm.induct, auto simp add: removen_nth) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

176 

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

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

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

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

180 
"tmsubst0 t (Bound n) = (if n=0 then t else Bound n)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

181 
"tmsubst0 t (CNP n c a) = (if n=0 then Add (Mul c t) (tmsubst0 t a) else CNP n c (tmsubst0 t a))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

184 
"tmsubst0 t (Sub a b) = Sub (tmsubst0 t a) (tmsubst0 t b)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

185 
"tmsubst0 t (Mul i a) = Mul i (tmsubst0 t a)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

188 
by (induct a rule: tmsubst0.induct,auto simp add: nth_pos2) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

189 

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

190 
lemma tmsubst0_nb: "tmbound0 t \<Longrightarrow> tmbound0 (tmsubst0 t a)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

191 
by (induct a rule: tmsubst0.induct,auto simp add: nth_pos2) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

192 

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

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

194 

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

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

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

197 
"tmsubst n t (Bound m) = (if n=m then t else Bound m)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

198 
"tmsubst n t (CNP m c a) = (if n=m then Add (Mul c t) (tmsubst n t a) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

199 
else CNP m c (tmsubst n t a))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

200 
"tmsubst n t (Neg a) = Neg (tmsubst n t a)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

201 
"tmsubst n t (Add a b) = Add (tmsubst n t a) (tmsubst n t b)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

202 
"tmsubst n t (Sub a b) = Sub (tmsubst n t a) (tmsubst n t b)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

203 
"tmsubst n t (Mul i a) = Mul i (tmsubst n t a)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

204 

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

205 
lemma tmsubst: assumes nb: "tmboundslt (length bs) a" and nlt: "n \<le> length bs" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

208 
by (induct a rule: tmsubst0.induct,auto simp add: nth_pos2) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

209 

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

210 
lemma tmsubst_nb0: assumes tnb: "tmbound0 t" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

211 
shows "tmbound0 (tmsubst 0 t a)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

214 

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

215 
lemma tmsubst_nb: assumes tnb: "tmbound m t" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

216 
shows "tmbound m (tmsubst m t a)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

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

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

222 

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

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

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

225 
tmadd:: "tm \<times> tm \<Rightarrow> tm" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

228 
"tmadd (CNP n1 c1 r1,CNP n2 c2 r2) = 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

230 
(let c = c1 +\<^sub>p c2 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

231 
in if c = 0\<^sub>p then tmadd(r1,r2) else CNP n1 c (tmadd (r1,r2))) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

232 
else if n1 \<le> n2 then (CNP n1 c1 (tmadd (r1,CNP n2 c2 r2))) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

233 
else (CNP n2 c2 (tmadd (CNP n1 c1 r1,r2))))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

234 
"tmadd (CNP n1 c1 r1,t) = CNP n1 c1 (tmadd (r1, t))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

235 
"tmadd (t,CNP n2 c2 r2) = CNP n2 c2 (tmadd (t,r2))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

238 

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

239 
lemma tmadd[simp]: "Itm vs bs (tmadd (t,s)) = Itm vs bs (Add t s)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

240 
apply (induct t s rule: tmadd.induct, simp_all add: Let_def) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

241 
apply (case_tac "c1 +\<^sub>p c2 = 0\<^sub>p",case_tac "n1 \<le> n2", simp_all) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

244 
by (auto simp del: polyadd simp add: polyadd[symmetric]) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

245 

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

246 
lemma tmadd_nb0[simp]: "\<lbrakk> tmbound0 t ; tmbound0 s\<rbrakk> \<Longrightarrow> tmbound0 (tmadd (t,s))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

247 
by (induct t s rule: tmadd.induct, auto simp add: Let_def) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

248 

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

249 
lemma tmadd_nb[simp]: "\<lbrakk> tmbound n t ; tmbound n s\<rbrakk> \<Longrightarrow> tmbound n (tmadd (t,s))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

250 
by (induct t s rule: tmadd.induct, auto simp add: Let_def) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

251 
lemma tmadd_blt[simp]: "\<lbrakk>tmboundslt n t ; tmboundslt n s\<rbrakk> \<Longrightarrow> tmboundslt n (tmadd (t,s))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

252 
by (induct t s rule: tmadd.induct, auto simp add: Let_def) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

253 

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

254 
lemma tmadd_allpolys_npoly[simp]: "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmadd(t,s))" by (induct t s rule: tmadd.induct, simp_all add: Let_def polyadd_norm) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

255 

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

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

257 
"tmmul (CP j) = (\<lambda> i. CP (i *\<^sub>p j))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

258 
"tmmul (CNP n c a) = (\<lambda> i. CNP n (i *\<^sub>p c) (tmmul a i))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

259 
"tmmul t = (\<lambda> i. Mul i t)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

260 

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

261 
lemma tmmul[simp]: "Itm vs bs (tmmul t i) = Itm vs bs (Mul i t)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

263 

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

264 
lemma tmmul_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 (tmmul t i)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

266 

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

267 
lemma tmmul_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n (tmmul t i)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

269 
lemma tmmul_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n (tmmul t i)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

271 

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

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

273 
assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero, field})" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

274 
shows "allpolys isnpoly t \<Longrightarrow> isnpoly c \<Longrightarrow> allpolys isnpoly (tmmul t c)" by (induct t rule: tmmul.induct, simp_all add: Let_def polymul_norm) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

275 

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

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

277 
"tmneg t \<equiv> tmmul t (C ( 1,1))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

278 

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

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

280 
"tmsub s t \<equiv> (if s = t then CP 0\<^sub>p else tmadd (s,tmneg t))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

281 

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

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

283 
using tmneg_def[of t] 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

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

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

289 

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

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

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

292 

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

293 
lemma tmneg_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n (tmneg t)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

295 
lemma tmneg_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n (tmneg t)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

297 
lemma [simp]: "isnpoly (C (1,1))" unfolding isnpoly_def by simp 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

299 
assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero, field})" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

300 
shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly (tmneg t)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

302 

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

303 
lemma tmsub[simp]: "Itm vs bs (tmsub a b) = Itm vs bs (Sub a b)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

305 

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

306 
lemma tmsub_nb0[simp]: "\<lbrakk> tmbound0 t ; tmbound0 s\<rbrakk> \<Longrightarrow> tmbound0 (tmsub t s)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

308 
lemma tmsub_nb[simp]: "\<lbrakk> tmbound n t ; tmbound n s\<rbrakk> \<Longrightarrow> tmbound n (tmsub t s)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

310 
lemma tmsub_blt[simp]: "\<lbrakk>tmboundslt n t ; tmboundslt n s\<rbrakk> \<Longrightarrow> tmboundslt n (tmsub t s )" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

313 
assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero, field})" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

314 
shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmsub t s)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

316 

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

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

318 
"simptm (CP j) = CP (polynate j)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

319 
"simptm (Bound n) = CNP n 1\<^sub>p (CP 0\<^sub>p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

323 
"simptm (Mul i t) = (let i' = polynate i in if i' = 0\<^sub>p then CP 0\<^sub>p else tmmul (simptm t) i')" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

324 
"simptm (CNP n c t) = (let c' = polynate c in if c' = 0\<^sub>p then simptm t else tmadd (CNP n c' (CP 0\<^sub>p ), simptm t))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

325 

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

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

327 
assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero, field})" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

328 
shows "polynate t = 0\<^sub>p \<Longrightarrow> Ipoly bs t = (0::'a::{ring_char_0,division_by_zero, field})" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

332 

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

333 
lemma simptm_ci[simp]: "Itm vs bs (simptm t) = Itm vs bs t" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

334 
by (induct t rule: simptm.induct, auto simp add: tmneg tmadd tmsub tmmul Let_def polynate_stupid) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

335 

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

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

337 
"tmbound0 t \<Longrightarrow> tmbound0 (simptm t)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

338 
by (induct t rule: simptm.induct, auto simp add: Let_def) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

339 

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

340 
lemma simptm_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n (simptm t)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

341 
by (induct t rule: simptm.induct, auto simp add: Let_def) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

342 
lemma simptm_nlt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n (simptm t)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

343 
by (induct t rule: simptm.induct, auto simp add: Let_def) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

344 

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

345 
lemma [simp]: "isnpoly 0\<^sub>p" and [simp]: "isnpoly (C(1,1))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

348 
assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero, field})" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

349 
shows "allpolys isnpoly (simptm p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

351 

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

352 
consts split0 :: "tm \<Rightarrow> (poly \<times> tm)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

354 
"split0 (Bound 0) = (1\<^sub>p, CP 0\<^sub>p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

355 
"split0 (CNP 0 c t) = (let (c',t') = split0 t in (c +\<^sub>p c',t'))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

356 
"split0 (Neg t) = (let (c,t') = split0 t in (~\<^sub>p c,Neg t'))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

357 
"split0 (CNP n c t) = (let (c',t') = split0 t in (c',CNP n c t'))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

358 
"split0 (Add s t) = (let (c1,s') = split0 s ; (c2,t') = split0 t in (c1 +\<^sub>p c2, Add s' t'))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

359 
"split0 (Sub s t) = (let (c1,s') = split0 s ; (c2,t') = split0 t in (c1 \<^sub>p c2, Sub s' t'))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

360 
"split0 (Mul c t) = (let (c',t') = split0 t in (c *\<^sub>p c', Mul c t'))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

361 
"split0 t = (0\<^sub>p, t)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

362 

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

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

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

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

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

367 

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

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

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

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

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

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

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

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

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

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

377 
apply (simp add: Let_def split_def mult_assoc right_distrib[symmetric]) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

381 

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

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

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

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

385 
assume "split0 t = (c', t')" hence "c' = fst (split0 t)" and "t' = snd (split0 t)" by auto 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

386 
with split0[where t="t" and bs="bs"] show "Itm vs bs t = Itm vs bs (CNP 0 c' t')" by simp 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

388 

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

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

390 
assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero, field})" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

394 
assume "split0 t = (c', t')" hence "c' = fst (split0 t)" and "t' = snd (split0 t)" by auto 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

395 
with conjunct1[OF split0[where t="t"]] show "tmbound 0 t'" by simp 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

397 

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

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

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

400 
using split0_nb0[of t "fst (split0 t)" "snd (split0 t)"] by (simp add: tmbound0_tmbound_iff) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

401 

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

402 

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

403 
lemma split0_nb: assumes nb:"tmbound n t" shows "tmbound n (snd (split0 t))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

404 
using nb by (induct t rule: split0.induct, auto simp add: Let_def split_def split0_stupid) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

405 

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

406 
lemma split0_blt: assumes nb:"tmboundslt n t" shows "tmboundslt n (snd (split0 t))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

407 
using nb by (induct t rule: split0.induct, auto simp add: Let_def split_def split0_stupid) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

408 

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

409 
lemma tmbound_split0: "tmbound 0 t \<Longrightarrow> Ipoly vs (fst(split0 t)) = 0" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

411 

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

412 
lemma tmboundslt_split0: "tmboundslt n t \<Longrightarrow> Ipoly vs (fst(split0 t)) = 0 \<or> n > 0" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

414 

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

415 
lemma tmboundslt0_split0: "tmboundslt 0 t \<Longrightarrow> Ipoly vs (fst(split0 t)) = 0" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

417 

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

418 
lemma allpolys_split0: "allpolys isnpoly p \<Longrightarrow> allpolys isnpoly (snd (split0 p))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

419 
by (induct p rule: split0.induct, auto simp add: isnpoly_def Let_def split_def split0_stupid) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

420 

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

421 
lemma isnpoly_fst_split0: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero, field})" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

423 
"allpolys isnpoly p \<Longrightarrow> isnpoly (fst (split0 p))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

425 
auto simp add: polyadd_norm polysub_norm polyneg_norm polymul_norm 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

427 

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

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

429 

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

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

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

432 

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

433 

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

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

435 
consts fmsize :: "fm \<Rightarrow> nat" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

438 
"fmsize (And p q) = 1 + fmsize p + fmsize q" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

439 
"fmsize (Or p q) = 1 + fmsize p + fmsize q" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

441 
"fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

442 
"fmsize (E p) = 1 + fmsize p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

443 
"fmsize (A p) = 4+ fmsize p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

445 
(* several lemmas about fmsize *) 
33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33212
diff
changeset

446 
lemma fmsize_pos: "fmsize p > 0" 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

448 

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

449 
(* Semantics of formulae (fm) *) 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34974
diff
changeset

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

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

452 
"Ifm vs bs T = True" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

453 
"Ifm vs bs F = False" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

454 
"Ifm vs bs (Lt a) = (Itm vs bs a < 0)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

455 
"Ifm vs bs (Le a) = (Itm vs bs a \<le> 0)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

457 
"Ifm vs bs (NEq a) = (Itm vs bs a \<noteq> 0)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

458 
"Ifm vs bs (NOT p) = (\<not> (Ifm vs bs p))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

460 
"Ifm vs bs (Or p q) = (Ifm vs bs p \<or> Ifm vs bs q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

461 
"Ifm vs bs (Imp p q) = ((Ifm vs bs p) \<longrightarrow> (Ifm vs bs q))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

463 
"Ifm vs bs (E p) = (\<exists> x. Ifm vs (x#bs) p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

464 
"Ifm vs bs (A p) = (\<forall> x. Ifm vs (x#bs) p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

465 

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

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

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

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

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

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

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

472 
"not (Lt t) = Le (tmneg t)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

473 
"not (Le t) = Lt (tmneg t)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

474 
"not (Eq t) = NEq t" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

475 
"not (NEq t) = Eq t" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

479 

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

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

481 
"conj p q \<equiv> (if (p = F \<or> q=F) then F else if p=T then q else if q=T then p else 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

484 
by (cases "p=F \<or> q=F",simp_all add: conj_def) (cases p,simp_all) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

485 

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

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

487 
"disj p q \<equiv> (if (p = T \<or> q=T) then T else if p=F then q else if q=F then p 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

489 

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

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

491 
by (cases "p=T \<or> q=T",simp_all add: disj_def) (cases p,simp_all) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

492 

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

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

494 
"imp p q \<equiv> (if (p = F \<or> q=T \<or> p=q) then T else if p=T then q else if q=F then not p 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

497 
by (cases "p=F \<or> q=T",simp_all add: imp_def) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

498 

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

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

500 
"iff p q \<equiv> (if (p = q) then T else if (p = NOT q \<or> NOT p = q) then F else 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

501 
if p=F then not q else if q=F then not p else if p=T then q else if q=T then p else 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

504 
by (unfold iff_def,cases "p=q", simp,cases "p=NOT q", simp) (cases "NOT p= q", auto) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

516 

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

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

518 

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

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

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

521 
"boundslt n T = True" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

522 
"boundslt n F = True" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

523 
"boundslt n (Lt t) = (tmboundslt n t)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

524 
"boundslt n (Le t) = (tmboundslt n t)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

525 
"boundslt n (Eq t) = (tmboundslt n t)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

526 
"boundslt n (NEq t) = (tmboundslt n t)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

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

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

532 
"boundslt n (E p) = boundslt (Suc n) p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

533 
"boundslt n (A p) = boundslt (Suc n) p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

534 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

556 
using bp tmbound0_I[where b="b" and bs="bs" and b'="b'"] 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

558 

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

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

560 
"bound m T = True" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

561 
"bound m F = True" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

562 
"bound m (Lt t) = tmbound m t" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

563 
"bound m (Le t) = tmbound m t" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

564 
"bound m (Eq t) = tmbound m t" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

565 
"bound m (NEq t) = tmbound m t" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

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

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

571 
"bound m (E p) = bound (Suc m) p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

572 
"bound m (A p) = bound (Suc m) p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

573 

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

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

575 
assumes bnd: "boundslt (length bs) p" and nb: "bound n p" and le: "n \<le> length bs" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

577 
using bnd nb le tmbound_I[where bs=bs and vs = vs] 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

578 
proof(induct p arbitrary: bs n rule: bound.induct) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

581 
from prems have bnd: "boundslt (length (y#bs)) p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

582 
and nb: "bound (Suc n) p" and le: "Suc n \<le> length (y#bs)" by simp+ 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

583 
from E.hyps[OF bnd nb le tmbound_I] have "Ifm vs ((y#bs)[Suc n:=x]) p = Ifm vs (y#bs) p" . } 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

586 
case (A p bs n) {fix y 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

587 
from prems have bnd: "boundslt (length (y#bs)) p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

588 
and nb: "bound (Suc n) p" and le: "Suc n \<le> length (y#bs)" by simp+ 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

589 
from A.hyps[OF bnd nb le tmbound_I] have "Ifm vs ((y#bs)[Suc n:=x]) p = Ifm vs (y#bs) p" . } 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

592 

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

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

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

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

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

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

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

599 
"decr0 (And p q) = conj (decr0 p) (decr0 q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

600 
"decr0 (Or p q) = disj (decr0 p) (decr0 q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

604 

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

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

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

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

608 
by (induct p rule: decr0.induct, simp_all add: decrtm0) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

609 

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

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

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

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

613 
"decr m (Lt t) = (Lt (decrtm m t))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

614 
"decr m (Le t) = (Le (decrtm m t))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

615 
"decr m (Eq t) = (Eq (decrtm m t))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

616 
"decr m (NEq t) = (NEq (decrtm m t))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

618 
"decr m (And p q) = conj (decr m p) (decr m q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

619 
"decr m (Or p q) = disj (decr m p) (decr m q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

622 
"decr m (E p) = E (decr (Suc m) p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

623 
"decr m (A p) = A (decr (Suc m) p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

624 

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

625 
lemma decr: assumes bnd: "boundslt (length bs) p" and nb: "bound m p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

626 
and nle: "m < length bs" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

629 
proof(induct p arbitrary: bs m rule: decr.induct) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

633 
and nle: "Suc m < length (x#bs)" by auto 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

634 
from prems(4)[OF bnd nb nle] have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p". 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

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

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

640 
and nle: "Suc m < length (x#bs)" by auto 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

641 
from prems(4)[OF bnd nb nle] have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p". 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

644 

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

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

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

647 

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

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

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

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

651 
"subst0 t (Lt a) = Lt (tmsubst0 t a)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

652 
"subst0 t (Le a) = Le (tmsubst0 t a)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

653 
"subst0 t (Eq a) = Eq (tmsubst0 t a)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

654 
"subst0 t (NEq a) = NEq (tmsubst0 t a)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

656 
"subst0 t (And p q) = And (subst0 t p) (subst0 t q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

657 
"subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

660 
"subst0 t (E p) = E p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

661 
"subst0 t (A p) = A p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

662 

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

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

664 
shows "Ifm vs (x#bs) (subst0 t p) = Ifm vs ((Itm vs (x#bs) t)#bs) p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

665 
using qf tmsubst0[where x="x" and bs="bs" and t="t"] 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

667 

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

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

669 
assumes bp: "tmbound0 t" and qf: "qfree p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

670 
shows "bound0 (subst0 t p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

671 
using qf tmsubst0_nb[OF bp] bp 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

673 

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

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

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

676 
"subst n t T = T" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

677 
"subst n t F = F" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

678 
"subst n t (Lt a) = Lt (tmsubst n t a)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

679 
"subst n t (Le a) = Le (tmsubst n t a)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

680 
"subst n t (Eq a) = Eq (tmsubst n t a)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

681 
"subst n t (NEq a) = NEq (tmsubst n t a)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

683 
"subst n t (And p q) = And (subst n t p) (subst n t q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

684 
"subst n t (Or p q) = Or (subst n t p) (subst n t q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

687 
"subst n t (E p) = E (subst (Suc n) (incrtm0 t) p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

688 
"subst n t (A p) = A (subst (Suc n) (incrtm0 t) p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

689 

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

690 
lemma subst: assumes nb: "boundslt (length bs) p" and nlm: "n \<le> length bs" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

693 
proof (induct p arbitrary: bs n t rule: subst0.induct) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

696 
from prems have bn: "boundslt (length (x#bs)) p" by simp 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

697 
from prems have nlm: "Suc n \<le> length (x#bs)" by simp 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

698 
from prems(3)[OF bn nlm] have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p" by simp 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

700 
by (simp add: incrtm0[where x="x" and bs="bs" and t="t"]) } 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

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

705 
from prems have bn: "boundslt (length (x#bs)) p" by simp 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

706 
from prems have nlm: "Suc n \<le> length (x#bs)" by simp 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

707 
from prems(3)[OF bn nlm] have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p" by simp 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

709 
by (simp add: incrtm0[where x="x" and bs="bs" and t="t"]) } 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

712 

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

713 
lemma subst_nb: assumes tnb: "tmbound m t" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

714 
shows "bound m (subst m t p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

717 

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

718 
lemma not_qf[simp]: "qfree p \<Longrightarrow> qfree (not p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

720 
lemma not_bn0[simp]: "bound0 p \<Longrightarrow> bound0 (not p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

722 
lemma not_nb[simp]: "bound n p \<Longrightarrow> bound n (not p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

724 
lemma not_blt[simp]: "boundslt n p \<Longrightarrow> boundslt n (not p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

726 

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

727 
lemma conj_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (conj p q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

729 
lemma conj_nb0[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (conj p q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

731 
lemma conj_nb[simp]: "\<lbrakk>bound n p ; bound n q\<rbrakk> \<Longrightarrow> bound n (conj p q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

735 

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

736 
lemma disj_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (disj p q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

738 
lemma disj_nb0[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (disj p q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

740 
lemma disj_nb[simp]: "\<lbrakk>bound n p ; bound n q\<rbrakk> \<Longrightarrow> bound n (disj p q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

744 

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

745 
lemma imp_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (imp p q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

746 
using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

747 
lemma imp_nb0[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (imp p q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

748 
using imp_def by (cases "p=F \<or> q=T \<or> p=q",simp_all add: imp_def) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

749 
lemma imp_nb[simp]: "\<lbrakk>bound n p ; bound n q\<rbrakk> \<Longrightarrow> bound n (imp p q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

750 
using imp_def by (cases "p=F \<or> q=T \<or> p=q",simp_all add: imp_def) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

753 

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

754 
lemma iff_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (iff p q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

755 
by (unfold iff_def,cases "p=q", auto) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

756 
lemma iff_nb0[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (iff p q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

757 
using iff_def by (unfold iff_def,cases "p=q", auto) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

758 
lemma iff_nb[simp]: "\<lbrakk>bound n p ; bound n q\<rbrakk> \<Longrightarrow> bound n (iff p q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

759 
using iff_def by (unfold iff_def,cases "p=q", auto) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

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

764 

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

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

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

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

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

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

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

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

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

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

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

775 

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

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

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

778 

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

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

780 
"djf f p q \<equiv> (if q=T then T else if q=F then f p else 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

781 
(let fp = f p in case fp of T \<Rightarrow> T  F \<Rightarrow> q  _ \<Rightarrow> Or (f p) q))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

783 
"evaldjf f ps \<equiv> foldr (djf f) ps F" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

784 

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

785 
lemma djf_Or: "Ifm vs bs (djf f p q) = Ifm vs bs (Or (f p) q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

786 
by (cases "q=T", simp add: djf_def,cases "q=F",simp add: djf_def) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

787 
(cases "f p", simp_all add: Let_def djf_def) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

788 

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

789 
lemma evaldjf_ex: "Ifm vs bs (evaldjf f ps) = (\<exists> p \<in> set ps. Ifm vs bs (f p))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

790 
by(induct ps, simp_all add: evaldjf_def djf_Or) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

791 

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

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

793 
assumes nb: "\<forall> x\<in> set xs. bound0 (f x)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

794 
shows "bound0 (evaldjf f xs)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

796 

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

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

798 
assumes nb: "\<forall> x\<in> set xs. qfree (f x)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

799 
shows "qfree (evaldjf f xs)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

801 

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

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

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

804 
"disjuncts (Or p q) = (disjuncts p) @ (disjuncts q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

805 
"disjuncts F = []" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

806 
"disjuncts p = [p]" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

807 

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

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

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

810 

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

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

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

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

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

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

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

817 

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

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

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

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

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

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

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

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

825 

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

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

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

828 

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

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

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

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

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

833 
have "Ifm vs bs (DJ f p) = (\<exists> q \<in> set (disjuncts p). Ifm vs bs (f q))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

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

838 

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

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

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

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

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

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

844 
have th: "DJ f p = evaldjf f (disjuncts p)" by (simp add: DJ_def) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

845 
from disjuncts_qf[OF qf] have "\<forall> q\<in> set (disjuncts p). qfree q" . 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

846 
with fqf have th':"\<forall> q\<in> set (disjuncts p). qfree (f q)" by blast 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

847 

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

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

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

850 

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

851 
lemma DJ_qe: assumes qe: "\<forall> bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm vs bs (qe p) = Ifm vs bs (E p))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

852 
shows "\<forall> bs p. qfree p \<longrightarrow> qfree (DJ qe p) \<and> (Ifm vs bs ((DJ qe p)) = Ifm vs bs (E p))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

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

857 
from DJ_qf[OF qth] qf have qfth:"qfree (DJ qe p)" by auto 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

858 
have "Ifm vs bs (DJ qe p) = (\<exists> q\<in> set (disjuncts p). Ifm vs bs (qe q))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

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

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

864 

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

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

866 

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

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

868 
"conjuncts (And p q) = (conjuncts p) @ (conjuncts q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

869 
"conjuncts T = []" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

871 

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

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

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

874 

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

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

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

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

878 

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

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

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

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

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

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

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

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

886 

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

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

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

889 

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

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

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

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

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

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

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

896 

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

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

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

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

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

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

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

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

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

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

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

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

908 

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

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

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

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

912 

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

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

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

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

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

917 

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

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

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

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

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

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

923 

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

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

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

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

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

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

929 

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

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

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

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

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

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

935 

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

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

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

938 

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

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

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

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

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

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

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

945 

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

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

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

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

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

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

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

952 

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

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

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

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

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

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

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

959 

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

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

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

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

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

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

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

966 

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

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

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

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

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

971 

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

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

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

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

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

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

977 

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

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

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

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

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

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

983 
lemma simpeq_islin[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

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

988 

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

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

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

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

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

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

994 

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

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

996 
by (cases "split0 s", auto) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

997 
lemma split0_npoly: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1016 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1031 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1046 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1061 

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

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

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

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

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

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

1067 

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

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

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

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

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

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

1073 

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

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

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

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

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

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

1079 

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

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

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

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

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

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

1085 

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

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

1087 
shows "tmbound0 t \<Longrightarrow> bound0 (simplt t)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

1091 
hence nb': "tmbound0 (simptm t)" by simp 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

1093 
from tmbound_split0[OF nb'[unfolded tmbound0_tmbound_iff[symmetric]]] 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1094 
have th: "\<forall>bs. Ipoly bs ?c = Ipoly bs 0\<^sub>p" by auto 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1095 
from isnpoly_fst_split0[OF simptm_allpolys_npoly[of t]] 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1096 
have ths: "isnpolyh ?c 0" "isnpolyh 0\<^sub>p 0" by (simp_all add: isnpoly_def) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1097 
from iffD1[OF isnpolyh_unique[OF ths] th] 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1098 
have "fst (split0 (simptm t)) = 0\<^sub>p" . 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1099 
thus "(fst (split0 (simptm t)) = 0\<^sub>p \<longrightarrow> bound0 (lt (snd (split0 (simptm t))))) \<and> 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1100 
fst (split0 (simptm t)) = 0\<^sub>p" by (simp add: simplt_def Let_def split_def lt_nb) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

1102 

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

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

1104 
shows "tmbound0 t \<Longrightarrow> bound0 (simple t)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

1108 
hence nb': "tmbound0 (simptm t)" by simp 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

1110 
from tmbound_split0[OF nb'[unfolded tmbound0_tmbound_iff[symmetric]]] 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1111 
have th: "\<forall>bs. Ipoly bs ?c = Ipoly bs 0\<^sub>p" by auto 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1112 
from isnpoly_fst_split0[OF simptm_allpolys_npoly[of t]] 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1113 
have ths: "isnpolyh ?c 0" "isnpolyh 0\<^sub>p 0" by (simp_all add: isnpoly_def) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1114 
from iffD1[OF isnpolyh_unique[OF ths] th] 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1115 
have "fst (split0 (simptm t)) = 0\<^sub>p" . 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1116 
thus "(fst (split0 (simptm t)) = 0\<^sub>p \<longrightarrow> bound0 (le (snd (split0 (simptm t))))) \<and> 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1117 
fst (split0 (simptm t)) = 0\<^sub>p" by (simp add: simplt_def Let_def split_def le_nb) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

1119 

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

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

1121 
shows "tmbound0 t \<Longrightarrow> bound0 (simpeq t)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

1125 
hence nb': "tmbound0 (simptm t)" by simp 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

1127 
from tmbound_split0[OF nb'[unfolded tmbound0_tmbound_iff[symmetric]]] 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1128 
have th: "\<forall>bs. Ipoly bs ?c = Ipoly bs 0\<^sub>p" by auto 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1129 
from isnpoly_fst_split0[OF simptm_allpolys_npoly[of t]] 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1130 
have ths: "isnpolyh ?c 0" "isnpolyh 0\<^sub>p 0" by (simp_all add: isnpoly_def) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1131 
from iffD1[OF isnpolyh_unique[OF ths] th] 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1132 
have "fst (split0 (simptm t)) = 0\<^sub>p" . 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1133 
thus "(fst (split0 (simptm t)) = 0\<^sub>p \<longrightarrow> bound0 (eq (snd (split0 (simptm t))))) \<and> 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1134 
fst (split0 (simptm t)) = 0\<^sub>p" by (simp add: simpeq_def Let_def split_def eq_nb) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

1136 

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

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

1138 
shows "tmbound0 t \<Longrightarrow> bound0 (simpneq t)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

1142 
hence nb': "tmbound0 (simptm t)" by simp 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

1144 
from tmbound_split0[OF nb'[unfolded tmbound0_tmbound_iff[symmetric]]] 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1145 
have th: "\<forall>bs. Ipoly bs ?c = Ipoly bs 0\<^sub>p" by auto 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1146 
from isnpoly_fst_split0[OF simptm_allpolys_npoly[of t]] 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1147 
have ths: "isnpolyh ?c 0" "isnpolyh 0\<^sub>p 0" by (simp_all add: isnpoly_def) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1148 
from iffD1[OF isnpolyh_unique[OF ths] th] 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1149 
have "fst (split0 (simptm t)) = 0\<^sub>p" . 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1150 
thus "(fst (split0 (simptm t)) = 0\<^sub>p \<longrightarrow> bound0 (neq (snd (split0 (simptm t))))) \<and> 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1151 
fst (split0 (simptm t)) = 0\<^sub>p" by (simp add: simpneq_def Let_def split_def neq_nb) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

1153 

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

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

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

1156 
"conjs (And p q) = (conjs p)@(conjs q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1157 
"conjs T = []" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1158 
"conjs p = [p]" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

1162 
"list_disj ps \<equiv> foldr disj ps F" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1163 

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

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

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

1166 
lemma list_conj_qf: " \<forall>p\<in> set ps. qfree p \<Longrightarrow> qfree (list_conj ps)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1167 
by (induct ps, auto simp add: list_conj_def conj_qf) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1168 
lemma list_disj: "Ifm vs bs (list_disj ps) = (\<exists>p\<in> set ps. Ifm vs bs p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

1170 

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

1171 
lemma conj_boundslt: "boundslt n p \<Longrightarrow> boundslt n q \<Longrightarrow> boundslt n (conj p q)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

1173 

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

1174 
lemma conjs_nb: "bound n p \<Longrightarrow> \<forall>q\<in> set (conjs p). bound n q" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

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

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

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

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

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

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

1181 
done 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1182 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1183 
lemma conjs_boundslt: "boundslt n p \<Longrightarrow> \<forall>q\<in> set (conjs p). boundslt n q" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1184 
apply (induct p rule: conjs.induct) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1185 
apply (unfold conjs.simps) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1186 
apply (unfold set_append) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1187 
apply (unfold ball_Un) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1188 
apply (unfold boundslt.simps) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1189 
apply blast 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1190 
by simp_all 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1191 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1192 
lemma list_conj_boundslt: " \<forall>p\<in> set ps. boundslt n p \<Longrightarrow> boundslt n (list_conj ps)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1193 
unfolding list_conj_def 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1194 
by (induct ps, auto simp add: conj_boundslt) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1195 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1196 
lemma list_conj_nb: assumes bnd: "\<forall>p\<in> set ps. bound n p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1197 
shows "bound n (list_conj ps)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1198 
using bnd 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1199 
unfolding list_conj_def 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1200 
by (induct ps, auto simp add: conj_nb) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1201 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1202 
lemma list_conj_nb': "\<forall>p\<in>set ps. bound0 p \<Longrightarrow> bound0 (list_conj ps)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1203 
unfolding list_conj_def by (induct ps , auto) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1204 

241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1205 
lemma CJNB_qe: 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1206 
assumes qe: "\<forall> bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm vs bs (qe p) = Ifm vs bs (E p))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1207 
shows "\<forall> bs p. qfree p \<longrightarrow> qfree (CJNB qe p) \<and> (Ifm vs bs ((CJNB qe p)) = Ifm vs bs (E p))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1208 
proof(clarify) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1209 
fix bs p 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1210 
assume qfp: "qfree p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1211 
let ?cjs = "conjuncts p" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1212 
let ?yes = "fst (partition bound0 ?cjs)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1213 
let ?no = "snd (partition bound0 ?cjs)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1214 
let ?cno = "list_conj ?no" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1215 
let ?cyes = "list_conj ?yes" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1216 
have part: "partition bound0 ?cjs = (?yes,?no)" by simp 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1217 
from partition_P[OF part] have "\<forall> q\<in> set ?yes. bound0 q" by blast 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1218 
hence yes_nb: "bound0 ?cyes" by (simp add: list_conj_nb') 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1219 
hence yes_qf: "qfree (decr0 ?cyes )" by (simp add: decr0_qf) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1220 
from conjuncts_qf[OF qfp] partition_set[OF part] 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1221 
have " \<forall>q\<in> set ?no. qfree q" by auto 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1222 
hence no_qf: "qfree ?cno"by (simp add: list_conj_qf) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1223 
with qe have cno_qf:"qfree (qe ?cno )" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1224 
and noE: "Ifm vs bs (qe ?cno) = Ifm vs bs (E ?cno)" by blast+ 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1225 
from cno_qf yes_qf have qf: "qfree (CJNB qe p)" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1226 
by (simp add: CJNB_def Let_def conj_qf split_def) 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1227 
{fix bs 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1228 
from conjuncts have "Ifm vs bs p = (\<forall>q\<in> set ?cjs. Ifm vs bs q)" by blast 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1229 
also have "\<dots> = ((\<forall>q\<in> set ?yes. Ifm vs bs q) \<and> (\<forall>q\<in> set ?no. Ifm vs bs q))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1230 
using partition_set[OF part] by auto 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1231 
finally have "Ifm vs bs p = ((Ifm vs bs ?cyes) \<and> (Ifm vs bs ?cno))" using list_conj[of vs bs] by simp} 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1232 
hence "Ifm vs bs (E p) = (\<exists>x. (Ifm vs (x#bs) ?cyes) \<and> (Ifm vs (x#bs) ?cno))" by simp 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1233 
also have "\<dots> = (\<exists>x. (Ifm vs (y#bs) ?cyes) \<and> (Ifm vs (x#bs) ?cno))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1234 
using bound0_I[OF yes_nb, where bs="bs" and b'="y"] by blast 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1235 
also have "\<dots> = (Ifm vs bs (decr0 ?cyes) \<and> Ifm vs bs (E ?cno))" 
33639
603320b93668
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
hoelzl
parents:
33268
diff
changeset

1236 
by (auto simp add: decr0[OF yes_nb] simp del: partition_filter_conv) 
33152
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
diff
changeset

1237 
also have "\<dots> = (Ifm vs bs (conj (decr0 ?cyes) (qe ?cno)))" 
241cfaed158f
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
chaieb
parents:
