author  wenzelm 
Thu, 03 Mar 2011 15:19:20 +0100  
changeset 41882  ae8d62656392 
parent 41849  1a65b780bd56 
child 41891  d37babdf5cae 
permissions  rwrr 
30439  1 
(* Title: HOL/Decision_Procs/MIR.thy 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

2 
Author: Amine Chaieb 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

3 
*) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

4 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

5 
theory MIR 
41849  6 
imports Complex_Main Dense_Linear_Order DP_Library 
7 
"~~/src/HOL/Library/Efficient_Nat" 

29788  8 
uses ("mir_tac.ML") 
27368  9 
begin 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

10 

27456  11 
section {* Quantifier elimination for @{text "\<real> (0, 1, +, floor, <)"} *} 
12 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

13 
declare real_of_int_floor_cancel [simp del] 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

14 

41849  15 
lemma myle: fixes a b :: "'a::{ordered_ab_group_add}" 
16 
shows "(a \<le> b) = (0 \<le> b  a)" 

17 
by (metis add_0_left add_le_cancel_right diff_add_cancel) 

18 

19 
lemma myless: fixes a b :: "'a::{ordered_ab_group_add}" 

20 
shows "(a < b) = (0 < b  a)" 

21 
by (metis le_iff_diff_le_0 less_le_not_le myle) 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

22 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

23 
(* Maybe should be added to the library \<dots> *) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

24 
lemma floor_int_eq: "(real n\<le> x \<and> x < real (n+1)) = (floor x = n)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

25 
proof( auto) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

26 
assume lb: "real n \<le> x" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

27 
and ub: "x < real n + 1" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

28 
have "real (floor x) \<le> x" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

29 
hence "real (floor x) < real (n + 1) " using ub by arith 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

30 
hence "floor x < n+1" by simp 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30042
diff
changeset

31 
moreover from lb have "n \<le> floor x" using floor_mono[where x="real n" and y="x"] 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

32 
by simp ultimately show "floor x = n" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

33 
qed 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

34 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

35 
(* Periodicity of dvd *) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

36 
lemma dvd_period: 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

37 
assumes advdd: "(a::int) dvd d" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

38 
shows "(a dvd (x + t)) = (a dvd ((x+ c*d) + t))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

39 
using advdd 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

40 
proof 
23316  41 
{fix x k 
42 
from inf_period(3)[OF advdd, rule_format, where x=x and k="k"] 

43 
have " ((a::int) dvd (x + t)) = (a dvd (x+k*d + t))" by simp} 

44 
hence "\<forall>x.\<forall>k. ((a::int) dvd (x + t)) = (a dvd (x+k*d + t))" by simp 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

45 
then show ?thesis by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

46 
qed 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

47 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

48 
(* The Divisibility relation between reals *) 
23858  49 
definition 
50 
rdvd:: "real \<Rightarrow> real \<Rightarrow> bool" (infixl "rdvd" 50) 

51 
where 

52 
rdvd_def: "x rdvd y \<longleftrightarrow> (\<exists>k\<Colon>int. y = x * real k)" 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

53 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

54 
lemma int_rdvd_real: 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

55 
shows "real (i::int) rdvd x = (i dvd (floor x) \<and> real (floor x) = x)" (is "?l = ?r") 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

56 
proof 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

57 
assume "?l" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

58 
hence th: "\<exists> k. x=real (i*k)" by (simp add: rdvd_def) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

59 
hence th': "real (floor x) = x" by (auto simp del: real_of_int_mult) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

60 
with th have "\<exists> k. real (floor x) = real (i*k)" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

61 
hence "\<exists> k. floor x = i*k" by (simp only: real_of_int_inject) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

62 
thus ?r using th' by (simp add: dvd_def) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

63 
next 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

64 
assume "?r" hence "(i\<Colon>int) dvd \<lfloor>x\<Colon>real\<rfloor>" .. 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

65 
hence "\<exists> k. real (floor x) = real (i*k)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

66 
by (simp only: real_of_int_inject) (simp add: dvd_def) 
41807  67 
thus ?l using `?r` by (simp add: rdvd_def) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

68 
qed 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

69 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

70 
lemma int_rdvd_iff: "(real (i::int) rdvd real t) = (i dvd t)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

71 
by (auto simp add: rdvd_def dvd_def) (rule_tac x="k" in exI, simp only :real_of_int_mult[symmetric]) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

72 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

73 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

74 
lemma rdvd_abs1: 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

75 
"(abs (real d) rdvd t) = (real (d ::int) rdvd t)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

76 
proof 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

77 
assume d: "real d rdvd t" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

78 
from d int_rdvd_real have d2: "d dvd (floor t)" and ti: "real (floor t) = t" by auto 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

79 

30042  80 
from iffD2[OF abs_dvd_iff] d2 have "(abs d) dvd (floor t)" by blast 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

81 
with ti int_rdvd_real[symmetric] have "real (abs d) rdvd t" by blast 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

82 
thus "abs (real d) rdvd t" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

83 
next 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

84 
assume "abs (real d) rdvd t" hence "real (abs d) rdvd t" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

85 
with int_rdvd_real[where i="abs d" and x="t"] have d2: "abs d dvd floor t" and ti: "real (floor t) =t" by auto 
30042  86 
from iffD1[OF abs_dvd_iff] d2 have "d dvd floor t" by blast 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

87 
with ti int_rdvd_real[symmetric] show "real d rdvd t" by blast 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

88 
qed 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

89 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

90 
lemma rdvd_minus: "(real (d::int) rdvd t) = (real d rdvd t)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

91 
apply (auto simp add: rdvd_def) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

92 
apply (rule_tac x="k" in exI, simp) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

93 
apply (rule_tac x="k" in exI, simp) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

94 
done 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

95 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

96 
lemma rdvd_left_0_eq: "(0 rdvd t) = (t=0)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

97 
by (auto simp add: rdvd_def) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

98 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

99 
lemma rdvd_mult: 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

100 
assumes knz: "k\<noteq>0" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

101 
shows "(real (n::int) * real (k::int) rdvd x * real k) = (real n rdvd x)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

102 
using knz by (simp add:rdvd_def) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

103 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

104 
(*********************************************************************************) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

105 
(**** SHADOW SYNTAX AND SEMANTICS ****) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

106 
(*********************************************************************************) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

107 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

108 
datatype num = C int  Bound nat  CN nat int num  Neg num  Add num num Sub num num 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

109 
 Mul int num  Floor num CF int num num 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

110 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

111 
(* A size for num to make inductive proofs simpler*) 
25765  112 
primrec num_size :: "num \<Rightarrow> nat" where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

113 
"num_size (C c) = 1" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

114 
 "num_size (Bound n) = 1" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

115 
 "num_size (Neg a) = 1 + num_size a" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

116 
 "num_size (Add a b) = 1 + num_size a + num_size b" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

117 
 "num_size (Sub a b) = 3 + num_size a + num_size b" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

118 
 "num_size (CN n c a) = 4 + num_size a " 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

119 
 "num_size (CF c a b) = 4 + num_size a + num_size b" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

120 
 "num_size (Mul c a) = 1 + num_size a" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

121 
 "num_size (Floor a) = 1 + num_size a" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

122 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

123 
(* Semantics of numeral terms (num) *) 
25765  124 
primrec Inum :: "real list \<Rightarrow> num \<Rightarrow> real" where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

125 
"Inum bs (C c) = (real c)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

126 
 "Inum bs (Bound n) = bs!n" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

127 
 "Inum bs (CN n c a) = (real c) * (bs!n) + (Inum bs a)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

128 
 "Inum bs (Neg a) = (Inum bs a)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

129 
 "Inum bs (Add a b) = Inum bs a + Inum bs b" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

130 
 "Inum bs (Sub a b) = Inum bs a  Inum bs b" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

131 
 "Inum bs (Mul c a) = (real c) * Inum bs a" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

132 
 "Inum bs (Floor a) = real (floor (Inum bs a))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

133 
 "Inum bs (CF c a b) = real c * real (floor (Inum bs a)) + Inum bs b" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

134 
definition "isint t bs \<equiv> real (floor (Inum bs t)) = Inum bs t" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

135 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

136 
lemma isint_iff: "isint n bs = (real (floor (Inum bs n)) = Inum bs n)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

137 
by (simp add: isint_def) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

138 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

139 
lemma isint_Floor: "isint (Floor n) bs" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

140 
by (simp add: isint_iff) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

141 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

142 
lemma isint_Mul: "isint e bs \<Longrightarrow> isint (Mul c e) bs" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

143 
proof 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

144 
let ?e = "Inum bs e" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

145 
let ?fe = "floor ?e" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

146 
assume be: "isint e bs" hence efe:"real ?fe = ?e" by (simp add: isint_iff) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

147 
have "real ((floor (Inum bs (Mul c e)))) = real (floor (real (c * ?fe)))" using efe by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

148 
also have "\<dots> = real (c* ?fe)" by (simp only: floor_real_of_int) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

149 
also have "\<dots> = real c * ?e" using efe by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

150 
finally show ?thesis using isint_iff by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

151 
qed 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

152 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

153 
lemma isint_neg: "isint e bs \<Longrightarrow> isint (Neg e) bs" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

154 
proof 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

155 
let ?I = "\<lambda> t. Inum bs t" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

156 
assume ie: "isint e bs" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

157 
hence th: "real (floor (?I e)) = ?I e" by (simp add: isint_def) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

158 
have "real (floor (?I (Neg e))) = real (floor ( (real (floor (?I e)))))" by (simp add: th) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

159 
also have "\<dots> =  real (floor (?I e))" by(simp add: floor_minus_real_of_int) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

160 
finally show "isint (Neg e) bs" by (simp add: isint_def th) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

161 
qed 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

162 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

163 
lemma isint_sub: 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

164 
assumes ie: "isint e bs" shows "isint (Sub (C c) e) bs" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

165 
proof 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

166 
let ?I = "\<lambda> t. Inum bs t" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

167 
from ie have th: "real (floor (?I e)) = ?I e" by (simp add: isint_def) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

168 
have "real (floor (?I (Sub (C c) e))) = real (floor ((real (c floor (?I e)))))" by (simp add: th) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

169 
also have "\<dots> = real (c floor (?I e))" by(simp add: floor_minus_real_of_int) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

170 
finally show "isint (Sub (C c) e) bs" by (simp add: isint_def th) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

171 
qed 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

172 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

173 
lemma isint_add: assumes 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

174 
ai:"isint a bs" and bi: "isint b bs" shows "isint (Add a b) bs" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

175 
proof 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

176 
let ?a = "Inum bs a" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

177 
let ?b = "Inum bs b" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

178 
from ai bi isint_iff have "real (floor (?a + ?b)) = real (floor (real (floor ?a) + real (floor ?b)))" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

179 
also have "\<dots> = real (floor ?a) + real (floor ?b)" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

180 
also have "\<dots> = ?a + ?b" using ai bi isint_iff by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

181 
finally show "isint (Add a b) bs" by (simp add: isint_iff) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

182 
qed 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

183 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

184 
lemma isint_c: "isint (C j) bs" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

185 
by (simp add: isint_iff) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

186 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

187 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

188 
(* FORMULAE *) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

189 
datatype fm = 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

190 
T F Lt num Le num Gt num Ge num Eq num NEq num Dvd int num NDvd int num 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

191 
NOT fm And fm fm Or fm fm Imp fm fm Iff fm fm E fm A fm 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

192 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

193 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

194 
(* A size for fm *) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

195 
fun fmsize :: "fm \<Rightarrow> nat" where 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

196 
"fmsize (NOT p) = 1 + fmsize p" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

197 
 "fmsize (And p q) = 1 + fmsize p + fmsize q" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

198 
 "fmsize (Or p q) = 1 + fmsize p + fmsize q" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

199 
 "fmsize (Imp p q) = 3 + fmsize p + fmsize q" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

200 
 "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

201 
 "fmsize (E p) = 1 + fmsize p" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

202 
 "fmsize (A p) = 4+ fmsize p" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

203 
 "fmsize (Dvd i t) = 2" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

204 
 "fmsize (NDvd i t) = 2" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

205 
 "fmsize p = 1" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

206 
(* several lemmas about fmsize *) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

207 
lemma fmsize_pos: "fmsize p > 0" 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

208 
by (induct p rule: fmsize.induct) simp_all 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

209 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

210 
(* Semantics of formulae (fm) *) 
25765  211 
primrec Ifm ::"real list \<Rightarrow> fm \<Rightarrow> bool" where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

212 
"Ifm bs T = True" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

213 
 "Ifm bs F = False" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

214 
 "Ifm bs (Lt a) = (Inum bs a < 0)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

215 
 "Ifm bs (Gt a) = (Inum bs a > 0)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

216 
 "Ifm bs (Le a) = (Inum bs a \<le> 0)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

217 
 "Ifm bs (Ge a) = (Inum bs a \<ge> 0)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

218 
 "Ifm bs (Eq a) = (Inum bs a = 0)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

219 
 "Ifm bs (NEq a) = (Inum bs a \<noteq> 0)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

220 
 "Ifm bs (Dvd i b) = (real i rdvd Inum bs b)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

221 
 "Ifm bs (NDvd i b) = (\<not>(real i rdvd Inum bs b))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

222 
 "Ifm bs (NOT p) = (\<not> (Ifm bs p))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

223 
 "Ifm bs (And p q) = (Ifm bs p \<and> Ifm bs q)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

224 
 "Ifm bs (Or p q) = (Ifm bs p \<or> Ifm bs q)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

225 
 "Ifm bs (Imp p q) = ((Ifm bs p) \<longrightarrow> (Ifm bs q))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

226 
 "Ifm bs (Iff p q) = (Ifm bs p = Ifm bs q)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

227 
 "Ifm bs (E p) = (\<exists> x. Ifm (x#bs) p)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

228 
 "Ifm bs (A p) = (\<forall> x. Ifm (x#bs) p)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

229 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

230 
consts prep :: "fm \<Rightarrow> fm" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

231 
recdef prep "measure fmsize" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

232 
"prep (E T) = T" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

233 
"prep (E F) = F" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

234 
"prep (E (Or p q)) = Or (prep (E p)) (prep (E q))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

235 
"prep (E (Imp p q)) = Or (prep (E (NOT p))) (prep (E q))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

236 
"prep (E (Iff p q)) = Or (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

237 
"prep (E (NOT (And p q))) = Or (prep (E (NOT p))) (prep (E(NOT q)))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

238 
"prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

239 
"prep (E (NOT (Iff p q))) = Or (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

240 
"prep (E p) = E (prep p)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

241 
"prep (A (And p q)) = And (prep (A p)) (prep (A q))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

242 
"prep (A p) = prep (NOT (E (NOT p)))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

243 
"prep (NOT (NOT p)) = prep p" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

244 
"prep (NOT (And p q)) = Or (prep (NOT p)) (prep (NOT q))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

245 
"prep (NOT (A p)) = prep (E (NOT p))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

246 
"prep (NOT (Or p q)) = And (prep (NOT p)) (prep (NOT q))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

247 
"prep (NOT (Imp p q)) = And (prep p) (prep (NOT q))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

248 
"prep (NOT (Iff p q)) = Or (prep (And p (NOT q))) (prep (And (NOT p) q))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

249 
"prep (NOT p) = NOT (prep p)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

250 
"prep (Or p q) = Or (prep p) (prep q)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

251 
"prep (And p q) = And (prep p) (prep q)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

252 
"prep (Imp p q) = prep (Or (NOT p) q)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

253 
"prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

254 
"prep p = p" 
25162  255 
(hints simp add: fmsize_pos) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

256 
lemma prep: "\<And> bs. Ifm bs (prep p) = Ifm bs p" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

257 
by (induct p rule: prep.induct, auto) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

258 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

259 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

260 
(* Quantifier freeness *) 
25765  261 
fun qfree:: "fm \<Rightarrow> bool" where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

262 
"qfree (E p) = False" 
25765  263 
 "qfree (A p) = False" 
264 
 "qfree (NOT p) = qfree p" 

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

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

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

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

269 
 "qfree p = True" 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

270 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

271 
(* Boundedness and substitution *) 
25765  272 
primrec numbound0 :: "num \<Rightarrow> bool" (* a num is INDEPENDENT of Bound 0 *) where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

273 
"numbound0 (C c) = True" 
25765  274 
 "numbound0 (Bound n) = (n>0)" 
275 
 "numbound0 (CN n i a) = (n > 0 \<and> numbound0 a)" 

276 
 "numbound0 (Neg a) = numbound0 a" 

277 
 "numbound0 (Add a b) = (numbound0 a \<and> numbound0 b)" 

278 
 "numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)" 

279 
 "numbound0 (Mul i a) = numbound0 a" 

280 
 "numbound0 (Floor a) = numbound0 a" 

281 
 "numbound0 (CF c a b) = (numbound0 a \<and> numbound0 b)" 

282 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

283 
lemma numbound0_I: 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

284 
assumes nb: "numbound0 a" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

285 
shows "Inum (b#bs) a = Inum (b'#bs) a" 
41849  286 
using nb by (induct a) auto 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

287 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

288 
lemma numbound0_gen: 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

289 
assumes nb: "numbound0 t" and ti: "isint t (x#bs)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

290 
shows "\<forall> y. isint t (y#bs)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

291 
using nb ti 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

292 
proof(clarify) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

293 
fix y 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

294 
from numbound0_I[OF nb, where bs="bs" and b="y" and b'="x"] ti[simplified isint_def] 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

295 
show "isint t (y#bs)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

296 
by (simp add: isint_def) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

297 
qed 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

298 

25765  299 
primrec bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *) where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

300 
"bound0 T = True" 
25765  301 
 "bound0 F = True" 
302 
 "bound0 (Lt a) = numbound0 a" 

303 
 "bound0 (Le a) = numbound0 a" 

304 
 "bound0 (Gt a) = numbound0 a" 

305 
 "bound0 (Ge a) = numbound0 a" 

306 
 "bound0 (Eq a) = numbound0 a" 

307 
 "bound0 (NEq a) = numbound0 a" 

308 
 "bound0 (Dvd i a) = numbound0 a" 

309 
 "bound0 (NDvd i a) = numbound0 a" 

310 
 "bound0 (NOT p) = bound0 p" 

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

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

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

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

315 
 "bound0 (E p) = False" 

316 
 "bound0 (A p) = False" 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

317 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

318 
lemma bound0_I: 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

319 
assumes bp: "bound0 p" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

320 
shows "Ifm (b#bs) p = Ifm (b'#bs) p" 
25765  321 
using bp numbound0_I [where b="b" and bs="bs" and b'="b'"] 
41849  322 
by (induct p) auto 
25765  323 

324 
primrec numsubst0:: "num \<Rightarrow> num \<Rightarrow> num" (* substitute a num into a num for Bound 0 *) where 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

325 
"numsubst0 t (C c) = (C c)" 
25765  326 
 "numsubst0 t (Bound n) = (if n=0 then t else Bound n)" 
327 
 "numsubst0 t (CN n i a) = (if n=0 then Add (Mul i t) (numsubst0 t a) else CN n i (numsubst0 t a))" 

328 
 "numsubst0 t (CF i a b) = CF i (numsubst0 t a) (numsubst0 t b)" 

329 
 "numsubst0 t (Neg a) = Neg (numsubst0 t a)" 

330 
 "numsubst0 t (Add a b) = Add (numsubst0 t a) (numsubst0 t b)" 

331 
 "numsubst0 t (Sub a b) = Sub (numsubst0 t a) (numsubst0 t b)" 

332 
 "numsubst0 t (Mul i a) = Mul i (numsubst0 t a)" 

333 
 "numsubst0 t (Floor a) = Floor (numsubst0 t a)" 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

334 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

335 
lemma numsubst0_I: 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

336 
shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t" 
41849  337 
by (induct t) simp_all 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

338 

25765  339 
primrec subst0:: "num \<Rightarrow> fm \<Rightarrow> fm" (* substitue a num into a formula for Bound 0 *) where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

340 
"subst0 t T = T" 
25765  341 
 "subst0 t F = F" 
342 
 "subst0 t (Lt a) = Lt (numsubst0 t a)" 

343 
 "subst0 t (Le a) = Le (numsubst0 t a)" 

344 
 "subst0 t (Gt a) = Gt (numsubst0 t a)" 

345 
 "subst0 t (Ge a) = Ge (numsubst0 t a)" 

346 
 "subst0 t (Eq a) = Eq (numsubst0 t a)" 

347 
 "subst0 t (NEq a) = NEq (numsubst0 t a)" 

348 
 "subst0 t (Dvd i a) = Dvd i (numsubst0 t a)" 

349 
 "subst0 t (NDvd i a) = NDvd i (numsubst0 t a)" 

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

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

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

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

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

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

355 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

356 
lemma subst0_I: assumes qfp: "qfree p" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

357 
shows "Ifm (b#bs) (subst0 a p) = Ifm ((Inum (b#bs) a)#bs) p" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

358 
using qfp numsubst0_I[where b="b" and bs="bs" and a="a"] 
41849  359 
by (induct p) simp_all 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

360 

41839  361 
fun decrnum:: "num \<Rightarrow> num" where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

362 
"decrnum (Bound n) = Bound (n  1)" 
41839  363 
 "decrnum (Neg a) = Neg (decrnum a)" 
364 
 "decrnum (Add a b) = Add (decrnum a) (decrnum b)" 

365 
 "decrnum (Sub a b) = Sub (decrnum a) (decrnum b)" 

366 
 "decrnum (Mul c a) = Mul c (decrnum a)" 

367 
 "decrnum (Floor a) = Floor (decrnum a)" 

368 
 "decrnum (CN n c a) = CN (n  1) c (decrnum a)" 

369 
 "decrnum (CF c a b) = CF c (decrnum a) (decrnum b)" 

370 
 "decrnum a = a" 

371 

372 
fun decr :: "fm \<Rightarrow> fm" where 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

373 
"decr (Lt a) = Lt (decrnum a)" 
41839  374 
 "decr (Le a) = Le (decrnum a)" 
375 
 "decr (Gt a) = Gt (decrnum a)" 

376 
 "decr (Ge a) = Ge (decrnum a)" 

377 
 "decr (Eq a) = Eq (decrnum a)" 

378 
 "decr (NEq a) = NEq (decrnum a)" 

379 
 "decr (Dvd i a) = Dvd i (decrnum a)" 

380 
 "decr (NDvd i a) = NDvd i (decrnum a)" 

381 
 "decr (NOT p) = NOT (decr p)" 

382 
 "decr (And p q) = And (decr p) (decr q)" 

383 
 "decr (Or p q) = Or (decr p) (decr q)" 

384 
 "decr (Imp p q) = Imp (decr p) (decr q)" 

385 
 "decr (Iff p q) = Iff (decr p) (decr q)" 

386 
 "decr p = p" 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

387 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

388 
lemma decrnum: assumes nb: "numbound0 t" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

389 
shows "Inum (x#bs) t = Inum bs (decrnum t)" 
41849  390 
using nb by (induct t rule: decrnum.induct, simp_all) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

391 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

392 
lemma decr: assumes nb: "bound0 p" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

393 
shows "Ifm (x#bs) p = Ifm bs (decr p)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

394 
using nb 
41849  395 
by (induct p rule: decr.induct, simp_all add: decrnum) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

396 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

397 
lemma decr_qf: "bound0 p \<Longrightarrow> qfree (decr p)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

398 
by (induct p, simp_all) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

399 

41839  400 
fun isatom :: "fm \<Rightarrow> bool" (* test for atomicity *) where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

401 
"isatom T = True" 
41839  402 
 "isatom F = True" 
403 
 "isatom (Lt a) = True" 

404 
 "isatom (Le a) = True" 

405 
 "isatom (Gt a) = True" 

406 
 "isatom (Ge a) = True" 

407 
 "isatom (Eq a) = True" 

408 
 "isatom (NEq a) = True" 

409 
 "isatom (Dvd i b) = True" 

410 
 "isatom (NDvd i b) = True" 

411 
 "isatom p = False" 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

412 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

413 
lemma numsubst0_numbound0: assumes nb: "numbound0 t" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

414 
shows "numbound0 (numsubst0 t a)" 
25765  415 
using nb by (induct a, auto) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

416 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

417 
lemma subst0_bound0: assumes qf: "qfree p" and nb: "numbound0 t" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

418 
shows "bound0 (subst0 t p)" 
25765  419 
using qf numsubst0_numbound0[OF nb] by (induct p, auto) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

420 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

421 
lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

422 
by (induct p, simp_all) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

423 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

424 

25765  425 
definition djf:: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm" where 
426 
"djf f p q = (if q=T then T else if q=F then f p else 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

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

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

430 
"evaldjf f ps = foldr (djf f) ps F" 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

431 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

432 
lemma djf_Or: "Ifm bs (djf f p q) = Ifm bs (Or (f p) q)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

433 
by (cases "q=T", simp add: djf_def,cases "q=F",simp add: djf_def) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

434 
(cases "f p", simp_all add: Let_def djf_def) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

435 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

436 
lemma evaldjf_ex: "Ifm bs (evaldjf f ps) = (\<exists> p \<in> set ps. Ifm bs (f p))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

437 
by(induct ps, simp_all add: evaldjf_def djf_Or) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

438 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

439 
lemma evaldjf_bound0: 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

440 
assumes nb: "\<forall> x\<in> set xs. bound0 (f x)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

441 
shows "bound0 (evaldjf f xs)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

442 
using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

443 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

444 
lemma evaldjf_qf: 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

445 
assumes nb: "\<forall> x\<in> set xs. qfree (f x)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

446 
shows "qfree (evaldjf f xs)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

447 
using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

448 

41839  449 
fun disjuncts :: "fm \<Rightarrow> fm list" where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

450 
"disjuncts (Or p q) = (disjuncts p) @ (disjuncts q)" 
41839  451 
 "disjuncts F = []" 
452 
 "disjuncts p = [p]" 

453 

454 
fun conjuncts :: "fm \<Rightarrow> fm list" where 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

455 
"conjuncts (And p q) = (conjuncts p) @ (conjuncts q)" 
41839  456 
 "conjuncts T = []" 
457 
 "conjuncts p = [p]" 

458 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

459 
lemma conjuncts: "(\<forall> q\<in> set (conjuncts p). Ifm bs q) = Ifm bs p" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

460 
by(induct p rule: conjuncts.induct, auto) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

461 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

462 
lemma disjuncts_qf: "qfree p \<Longrightarrow> \<forall> q\<in> set (disjuncts p). qfree q" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

463 
proof 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

464 
assume qf: "qfree p" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

465 
hence "list_all qfree (disjuncts p)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

466 
by (induct p rule: disjuncts.induct, auto) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

467 
thus ?thesis by (simp only: list_all_iff) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

468 
qed 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

469 
lemma conjuncts_qf: "qfree p \<Longrightarrow> \<forall> q\<in> set (conjuncts p). qfree q" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

470 
proof 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

471 
assume qf: "qfree p" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

472 
hence "list_all qfree (conjuncts p)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

473 
by (induct p rule: conjuncts.induct, auto) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

474 
thus ?thesis by (simp only: list_all_iff) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

475 
qed 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

476 

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

477 
definition DJ :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm" where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

478 
"DJ f p \<equiv> evaldjf f (disjuncts p)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

479 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

480 
lemma DJ: assumes fdj: "\<forall> p q. f (Or p q) = Or (f p) (f q)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

481 
and fF: "f F = F" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

482 
shows "Ifm bs (DJ f p) = Ifm bs (f p)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

483 
proof 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

484 
have "Ifm bs (DJ f p) = (\<exists> q \<in> set (disjuncts p). Ifm bs (f q))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

485 
by (simp add: DJ_def evaldjf_ex) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

486 
also have "\<dots> = Ifm bs (f p)" using fdj fF by (induct p rule: disjuncts.induct, auto) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

487 
finally show ?thesis . 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

488 
qed 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

489 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

490 
lemma DJ_qf: assumes 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

491 
fqf: "\<forall> p. qfree p \<longrightarrow> qfree (f p)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

492 
shows "\<forall>p. qfree p \<longrightarrow> qfree (DJ f p) " 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

493 
proof(clarify) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

494 
fix p assume qf: "qfree p" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

495 
have th: "DJ f p = evaldjf f (disjuncts p)" by (simp add: DJ_def) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

496 
from disjuncts_qf[OF qf] have "\<forall> q\<in> set (disjuncts p). qfree q" . 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

497 
with fqf have th':"\<forall> q\<in> set (disjuncts p). qfree (f q)" by blast 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

498 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

499 
from evaldjf_qf[OF th'] th show "qfree (DJ f p)" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

500 
qed 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

501 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

502 
lemma DJ_qe: assumes qe: "\<forall> bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bs (qe p) = Ifm bs (E p))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

503 
shows "\<forall> bs p. qfree p \<longrightarrow> qfree (DJ qe p) \<and> (Ifm bs ((DJ qe p)) = Ifm bs (E p))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

504 
proof(clarify) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

505 
fix p::fm and bs 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

506 
assume qf: "qfree p" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

507 
from qe have qth: "\<forall> p. qfree p \<longrightarrow> qfree (qe p)" by blast 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

508 
from DJ_qf[OF qth] qf have qfth:"qfree (DJ qe p)" by auto 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

509 
have "Ifm bs (DJ qe p) = (\<exists> q\<in> set (disjuncts p). Ifm bs (qe q))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

510 
by (simp add: DJ_def evaldjf_ex) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

511 
also have "\<dots> = (\<exists> q \<in> set(disjuncts p). Ifm bs (E q))" using qe disjuncts_qf[OF qf] by auto 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

512 
also have "\<dots> = Ifm bs (E p)" by (induct p rule: disjuncts.induct, auto) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

513 
finally show "qfree (DJ qe p) \<and> Ifm bs (DJ qe p) = Ifm bs (E p)" using qfth by blast 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

514 
qed 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

515 
(* Simplification *) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

516 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

517 
(* Algebraic simplifications for nums *) 
41839  518 
fun bnds:: "num \<Rightarrow> nat list" where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

519 
"bnds (Bound n) = [n]" 
41839  520 
 "bnds (CN n c a) = n#(bnds a)" 
521 
 "bnds (Neg a) = bnds a" 

522 
 "bnds (Add a b) = (bnds a)@(bnds b)" 

523 
 "bnds (Sub a b) = (bnds a)@(bnds b)" 

524 
 "bnds (Mul i a) = bnds a" 

525 
 "bnds (Floor a) = bnds a" 

526 
 "bnds (CF c a b) = (bnds a)@(bnds b)" 

527 
 "bnds a = []" 

528 
fun lex_ns:: "nat list \<Rightarrow> nat list \<Rightarrow> bool" where 

529 
"lex_ns [] ms = True" 

530 
 "lex_ns ns [] = False" 

531 
 "lex_ns (n#ns) (m#ms) = (n<m \<or> ((n = m) \<and> lex_ns ns ms)) " 

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

532 
definition lex_bnd :: "num \<Rightarrow> num \<Rightarrow> bool" where 
41839  533 
"lex_bnd t s \<equiv> lex_ns (bnds t) (bnds s)" 
534 

535 
fun maxcoeff:: "num \<Rightarrow> int" where 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

536 
"maxcoeff (C i) = abs i" 
41839  537 
 "maxcoeff (CN n c t) = max (abs c) (maxcoeff t)" 
538 
 "maxcoeff (CF c t s) = max (abs c) (maxcoeff s)" 

539 
 "maxcoeff t = 1" 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

540 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

541 
lemma maxcoeff_pos: "maxcoeff t \<ge> 0" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

542 
apply (induct t rule: maxcoeff.induct, auto) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

543 
done 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

544 

41839  545 
fun numgcdh:: "num \<Rightarrow> int \<Rightarrow> int" where 
31706  546 
"numgcdh (C i) = (\<lambda>g. gcd i g)" 
41839  547 
 "numgcdh (CN n c t) = (\<lambda>g. gcd c (numgcdh t g))" 
548 
 "numgcdh (CF c s t) = (\<lambda>g. gcd c (numgcdh t g))" 

549 
 "numgcdh t = (\<lambda>g. 1)" 

23858  550 

551 
definition 

552 
numgcd :: "num \<Rightarrow> int" 

553 
where 

554 
numgcd_def: "numgcd t = numgcdh t (maxcoeff t)" 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

555 

41839  556 
fun reducecoeffh:: "num \<Rightarrow> int \<Rightarrow> num" where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

557 
"reducecoeffh (C i) = (\<lambda> g. C (i div g))" 
41839  558 
 "reducecoeffh (CN n c t) = (\<lambda> g. CN n (c div g) (reducecoeffh t g))" 
559 
 "reducecoeffh (CF c s t) = (\<lambda> g. CF (c div g) s (reducecoeffh t g))" 

560 
 "reducecoeffh t = (\<lambda>g. t)" 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

561 

23858  562 
definition 
563 
reducecoeff :: "num \<Rightarrow> num" 

564 
where 

565 
reducecoeff_def: "reducecoeff t = 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

566 
(let g = numgcd t in 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

567 
if g = 0 then C 0 else if g=1 then t else reducecoeffh t g)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

568 

41839  569 
fun dvdnumcoeff:: "num \<Rightarrow> int \<Rightarrow> bool" where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

570 
"dvdnumcoeff (C i) = (\<lambda> g. g dvd i)" 
41839  571 
 "dvdnumcoeff (CN n c t) = (\<lambda> g. g dvd c \<and> (dvdnumcoeff t g))" 
572 
 "dvdnumcoeff (CF c s t) = (\<lambda> g. g dvd c \<and> (dvdnumcoeff t g))" 

573 
 "dvdnumcoeff t = (\<lambda>g. False)" 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

574 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

575 
lemma dvdnumcoeff_trans: 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

576 
assumes gdg: "g dvd g'" and dgt':"dvdnumcoeff t g'" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

577 
shows "dvdnumcoeff t g" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

578 
using dgt' gdg 
30042  579 
by (induct t rule: dvdnumcoeff.induct, simp_all add: gdg dvd_trans[OF gdg]) 
580 

581 
declare dvd_trans [trans add] 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

582 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

583 
lemma numgcd0: 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

584 
assumes g0: "numgcd t = 0" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

585 
shows "Inum bs t = 0" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

586 
proof 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

587 
have "\<And>x. numgcdh t x= 0 \<Longrightarrow> Inum bs t = 0" 
31706  588 
by (induct t rule: numgcdh.induct, auto) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

589 
thus ?thesis using g0[simplified numgcd_def] by blast 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

590 
qed 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

591 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

592 
lemma numgcdh_pos: assumes gp: "g \<ge> 0" shows "numgcdh t g \<ge> 0" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

593 
using gp 
31706  594 
by (induct t rule: numgcdh.induct, auto) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

595 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

596 
lemma numgcd_pos: "numgcd t \<ge>0" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

597 
by (simp add: numgcd_def numgcdh_pos maxcoeff_pos) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

598 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

599 
lemma reducecoeffh: 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

600 
assumes gt: "dvdnumcoeff t g" and gp: "g > 0" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

601 
shows "real g *(Inum bs (reducecoeffh t g)) = Inum bs t" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

602 
using gt 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

603 
proof(induct t rule: reducecoeffh.induct) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

604 
case (1 i) hence gd: "g dvd i" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

605 
from gp have gnz: "g \<noteq> 0" by simp 
41807  606 
from assms 1 show ?case by (simp add: real_of_int_div[OF gnz gd]) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

607 
next 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

608 
case (2 n c t) hence gd: "g dvd c" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

609 
from gp have gnz: "g \<noteq> 0" by simp 
41807  610 
from assms 2 show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

611 
next 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

612 
case (3 c s t) hence gd: "g dvd c" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

613 
from gp have gnz: "g \<noteq> 0" by simp 
41807  614 
from assms 3 show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

615 
qed (auto simp add: numgcd_def gp) 
41807  616 

41839  617 
fun ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool" where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

618 
"ismaxcoeff (C i) = (\<lambda> x. abs i \<le> x)" 
41839  619 
 "ismaxcoeff (CN n c t) = (\<lambda>x. abs c \<le> x \<and> (ismaxcoeff t x))" 
620 
 "ismaxcoeff (CF c s t) = (\<lambda>x. abs c \<le> x \<and> (ismaxcoeff t x))" 

621 
 "ismaxcoeff t = (\<lambda>x. True)" 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

622 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

623 
lemma ismaxcoeff_mono: "ismaxcoeff t c \<Longrightarrow> c \<le> c' \<Longrightarrow> ismaxcoeff t c'" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

624 
by (induct t rule: ismaxcoeff.induct, auto) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

625 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

626 
lemma maxcoeff_ismaxcoeff: "ismaxcoeff t (maxcoeff t)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

627 
proof (induct t rule: maxcoeff.induct) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

628 
case (2 n c t) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

629 
hence H:"ismaxcoeff t (maxcoeff t)" . 
41807  630 
have thh: "maxcoeff t \<le> max (abs c) (maxcoeff t)" by simp 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

631 
from ismaxcoeff_mono[OF H thh] show ?case by (simp add: le_maxI1) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

632 
next 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

633 
case (3 c t s) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

634 
hence H1:"ismaxcoeff s (maxcoeff s)" by auto 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

635 
have thh1: "maxcoeff s \<le> max \<bar>c\<bar> (maxcoeff s)" by (simp add: max_def) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

636 
from ismaxcoeff_mono[OF H1 thh1] show ?case by (simp add: le_maxI1) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

637 
qed simp_all 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

638 

31706  639 
lemma zgcd_gt1: "gcd i j > (1::int) \<Longrightarrow> ((abs i > 1 \<and> abs j > 1) \<or> (abs i = 0 \<and> abs j > 1) \<or> (abs i > 1 \<and> abs j = 0))" 
640 
apply (unfold gcd_int_def) 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

641 
apply (cases "i = 0", simp_all) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

642 
apply (cases "j = 0", simp_all) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

643 
apply (cases "abs i = 1", simp_all) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

644 
apply (cases "abs j = 1", simp_all) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

645 
apply auto 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

646 
done 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

647 
lemma numgcdh0:"numgcdh t m = 0 \<Longrightarrow> m =0" 
41807  648 
by (induct t rule: numgcdh.induct) auto 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

649 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

650 
lemma dvdnumcoeff_aux: 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

651 
assumes "ismaxcoeff t m" and mp:"m \<ge> 0" and "numgcdh t m > 1" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

652 
shows "dvdnumcoeff t (numgcdh t m)" 
41807  653 
using assms 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

654 
proof(induct t rule: numgcdh.induct) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

655 
case (2 n c t) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

656 
let ?g = "numgcdh t m" 
41807  657 
from 2 have th:"gcd c ?g > 1" by simp 
27556  658 
from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"] 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

659 
have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp 
41807  660 
moreover {assume "abs c > 1" and gp: "?g > 1" with 2 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

661 
have th: "dvdnumcoeff t ?g" by simp 
31706  662 
have th': "gcd c ?g dvd ?g" by simp 
663 
from dvdnumcoeff_trans[OF th' th] have ?case by simp } 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

664 
moreover {assume "abs c = 0 \<and> ?g > 1" 
41807  665 
with 2 have th: "dvdnumcoeff t ?g" by simp 
31706  666 
have th': "gcd c ?g dvd ?g" by simp 
667 
from dvdnumcoeff_trans[OF th' th] have ?case by simp 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

668 
hence ?case by simp } 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

669 
moreover {assume "abs c > 1" and g0:"?g = 0" 
41807  670 
from numgcdh0[OF g0] have "m=0". with 2 g0 have ?case by simp } 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

671 
ultimately show ?case by blast 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

672 
next 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

673 
case (3 c s t) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

674 
let ?g = "numgcdh t m" 
41807  675 
from 3 have th:"gcd c ?g > 1" by simp 
27556  676 
from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"] 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

677 
have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp 
41807  678 
moreover {assume "abs c > 1" and gp: "?g > 1" with 3 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

679 
have th: "dvdnumcoeff t ?g" by simp 
31706  680 
have th': "gcd c ?g dvd ?g" by simp 
681 
from dvdnumcoeff_trans[OF th' th] have ?case by simp } 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

682 
moreover {assume "abs c = 0 \<and> ?g > 1" 
41807  683 
with 3 have th: "dvdnumcoeff t ?g" by simp 
31706  684 
have th': "gcd c ?g dvd ?g" by simp 
685 
from dvdnumcoeff_trans[OF th' th] have ?case by simp 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

686 
hence ?case by simp } 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

687 
moreover {assume "abs c > 1" and g0:"?g = 0" 
41807  688 
from numgcdh0[OF g0] have "m=0". with 3 g0 have ?case by simp } 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

689 
ultimately show ?case by blast 
31706  690 
qed auto 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

691 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

692 
lemma dvdnumcoeff_aux2: 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

693 
assumes "numgcd t > 1" shows "dvdnumcoeff t (numgcd t) \<and> numgcd t > 0" 
41807  694 
using assms 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

695 
proof (simp add: numgcd_def) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

696 
let ?mc = "maxcoeff t" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

697 
let ?g = "numgcdh t ?mc" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

698 
have th1: "ismaxcoeff t ?mc" by (rule maxcoeff_ismaxcoeff) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

699 
have th2: "?mc \<ge> 0" by (rule maxcoeff_pos) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

700 
assume H: "numgcdh t ?mc > 1" 
41807  701 
from dvdnumcoeff_aux[OF th1 th2 H] show "dvdnumcoeff t ?g" . 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

702 
qed 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

703 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

704 
lemma reducecoeff: "real (numgcd t) * (Inum bs (reducecoeff t)) = Inum bs t" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

705 
proof 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

706 
let ?g = "numgcd t" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

707 
have "?g \<ge> 0" by (simp add: numgcd_pos) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

708 
hence "?g = 0 \<or> ?g = 1 \<or> ?g > 1" by auto 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

709 
moreover {assume "?g = 0" hence ?thesis by (simp add: numgcd0)} 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

710 
moreover {assume "?g = 1" hence ?thesis by (simp add: reducecoeff_def)} 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

711 
moreover { assume g1:"?g > 1" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

712 
from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff t ?g" and g0: "?g > 0" by blast+ 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

713 
from reducecoeffh[OF th1 g0, where bs="bs"] g1 have ?thesis 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

714 
by (simp add: reducecoeff_def Let_def)} 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

715 
ultimately show ?thesis by blast 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

716 
qed 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

717 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

718 
lemma reducecoeffh_numbound0: "numbound0 t \<Longrightarrow> numbound0 (reducecoeffh t g)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

719 
by (induct t rule: reducecoeffh.induct, auto) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

720 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

721 
lemma reducecoeff_numbound0: "numbound0 t \<Longrightarrow> numbound0 (reducecoeff t)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

722 
using reducecoeffh_numbound0 by (simp add: reducecoeff_def Let_def) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

723 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

724 
consts 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

725 
numadd:: "num \<times> num \<Rightarrow> num" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

726 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

727 
recdef numadd "measure (\<lambda> (t,s). size t + size s)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

728 
"numadd (CN n1 c1 r1,CN n2 c2 r2) = 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

729 
(if n1=n2 then 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

730 
(let c = c1 + c2 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

731 
in (if c=0 then numadd(r1,r2) else CN n1 c (numadd (r1,r2)))) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

732 
else if n1 \<le> n2 then CN n1 c1 (numadd (r1,CN n2 c2 r2)) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

733 
else (CN n2 c2 (numadd (CN n1 c1 r1,r2))))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

734 
"numadd (CN n1 c1 r1,t) = CN n1 c1 (numadd (r1, t))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

735 
"numadd (t,CN n2 c2 r2) = CN n2 c2 (numadd (t,r2))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

736 
"numadd (CF c1 t1 r1,CF c2 t2 r2) = 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

737 
(if t1 = t2 then 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

738 
(let c=c1+c2; s= numadd(r1,r2) in (if c=0 then s else CF c t1 s)) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

739 
else if lex_bnd t1 t2 then CF c1 t1 (numadd(r1,CF c2 t2 r2)) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

740 
else CF c2 t2 (numadd(CF c1 t1 r1,r2)))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

741 
"numadd (CF c1 t1 r1,C c) = CF c1 t1 (numadd (r1, C c))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

742 
"numadd (C c,CF c1 t1 r1) = CF c1 t1 (numadd (r1, C c))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

743 
"numadd (C b1, C b2) = C (b1+b2)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

744 
"numadd (a,b) = Add a b" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

745 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

746 
lemma numadd[simp]: "Inum bs (numadd (t,s)) = Inum bs (Add t s)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

747 
apply (induct t s rule: numadd.induct, simp_all add: Let_def) 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23464
diff
changeset

748 
apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all) 
29667  749 
apply (case_tac "n1 = n2", simp_all add: algebra_simps) 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23464
diff
changeset

750 
apply (simp only: left_distrib[symmetric]) 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23464
diff
changeset

751 
apply simp 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

752 
apply (case_tac "lex_bnd t1 t2", simp_all) 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23464
diff
changeset

753 
apply (case_tac "c1+c2 = 0") 
29667  754 
by (case_tac "t1 = t2", simp_all add: algebra_simps left_distrib[symmetric] real_of_int_mult[symmetric] real_of_int_add[symmetric]del: real_of_int_mult real_of_int_add left_distrib) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

755 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

756 
lemma numadd_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

757 
by (induct t s rule: numadd.induct, auto simp add: Let_def) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

758 

41839  759 
fun nummul:: "num \<Rightarrow> int \<Rightarrow> num" where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

760 
"nummul (C j) = (\<lambda> i. C (i*j))" 
41839  761 
 "nummul (CN n c t) = (\<lambda> i. CN n (c*i) (nummul t i))" 
762 
 "nummul (CF c t s) = (\<lambda> i. CF (c*i) t (nummul s i))" 

763 
 "nummul (Mul c t) = (\<lambda> i. nummul t (i*c))" 

764 
 "nummul t = (\<lambda> i. Mul i t)" 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

765 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

766 
lemma nummul[simp]: "\<And> i. Inum bs (nummul t i) = Inum bs (Mul i t)" 
29667  767 
by (induct t rule: nummul.induct, auto simp add: algebra_simps) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

768 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

769 
lemma nummul_nb[simp]: "\<And> i. numbound0 t \<Longrightarrow> numbound0 (nummul t i)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

770 
by (induct t rule: nummul.induct, auto) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

771 

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

772 
definition numneg :: "num \<Rightarrow> num" where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

773 
"numneg t \<equiv> nummul t ( 1)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

774 

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

775 
definition numsub :: "num \<Rightarrow> num \<Rightarrow> num" where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

776 
"numsub s t \<equiv> (if s = t then C 0 else numadd (s,numneg t))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

777 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

778 
lemma numneg[simp]: "Inum bs (numneg t) = Inum bs (Neg t)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

779 
using numneg_def nummul by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

780 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

781 
lemma numneg_nb[simp]: "numbound0 t \<Longrightarrow> numbound0 (numneg t)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

782 
using numneg_def by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

783 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

784 
lemma numsub[simp]: "Inum bs (numsub a b) = Inum bs (Sub a b)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

785 
using numsub_def by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

786 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

787 
lemma numsub_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numsub t s)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

788 
using numsub_def by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

789 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

790 
lemma isint_CF: assumes si: "isint s bs" shows "isint (CF c t s) bs" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

791 
proof 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

792 
have cti: "isint (Mul c (Floor t)) bs" by (simp add: isint_Mul isint_Floor) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

793 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

794 
have "?thesis = isint (Add (Mul c (Floor t)) s) bs" by (simp add: isint_def) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

795 
also have "\<dots>" by (simp add: isint_add cti si) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

796 
finally show ?thesis . 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

797 
qed 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

798 

41839  799 
fun split_int:: "num \<Rightarrow> num \<times> num" where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

800 
"split_int (C c) = (C 0, C c)" 
41839  801 
 "split_int (CN n c b) = 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

802 
(let (bv,bi) = split_int b 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

803 
in (CN n c bv, bi))" 
41839  804 
 "split_int (CF c a b) = 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

805 
(let (bv,bi) = split_int b 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

806 
in (bv, CF c a bi))" 
41839  807 
 "split_int a = (a,C 0)" 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

808 

41807  809 
lemma split_int: "\<And>tv ti. split_int t = (tv,ti) \<Longrightarrow> (Inum bs (Add tv ti) = Inum bs t) \<and> isint ti bs" 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

810 
proof (induct t rule: split_int.induct) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

811 
case (2 c n b tv ti) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

812 
let ?bv = "fst (split_int b)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

813 
let ?bi = "snd (split_int b)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

814 
have "split_int b = (?bv,?bi)" by simp 
41807  815 
with 2(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" by blast+ 
816 
from 2(2) have tibi: "ti = ?bi" by (simp add: Let_def split_def) 

817 
from 2(2) b[symmetric] bii show ?case by (auto simp add: Let_def split_def) 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

818 
next 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

819 
case (3 c a b tv ti) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

820 
let ?bv = "fst (split_int b)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

821 
let ?bi = "snd (split_int b)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

822 
have "split_int b = (?bv,?bi)" by simp 
41807  823 
with 3(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" by blast+ 
824 
from 3(2) have tibi: "ti = CF c a ?bi" 

825 
by (simp add: Let_def split_def) 

826 
from 3(2) b[symmetric] bii show ?case 

827 
by (auto simp add: Let_def split_def isint_Floor isint_add isint_Mul isint_CF) 

29667  828 
qed (auto simp add: Let_def isint_iff isint_Floor isint_add isint_Mul split_def algebra_simps) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

829 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

830 
lemma split_int_nb: "numbound0 t \<Longrightarrow> numbound0 (fst (split_int t)) \<and> numbound0 (snd (split_int t)) " 
41807  831 
by (induct t rule: split_int.induct) (auto simp add: Let_def split_def) 
832 

833 
definition numfloor:: "num \<Rightarrow> num" 

23858  834 
where 
41807  835 
"numfloor t = (let (tv,ti) = split_int t in 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

836 
(case tv of C i \<Rightarrow> numadd (tv,ti) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

837 
 _ \<Rightarrow> numadd(CF 1 tv (C 0),ti)))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

838 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

839 
lemma numfloor[simp]: "Inum bs (numfloor t) = Inum bs (Floor t)" (is "?n t = ?N (Floor t)") 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

840 
proof 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

841 
let ?tv = "fst (split_int t)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

842 
let ?ti = "snd (split_int t)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

843 
have tvti:"split_int t = (?tv,?ti)" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

844 
{assume H: "\<forall> v. ?tv \<noteq> C v" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

845 
hence th1: "?n t = ?N (Add (Floor ?tv) ?ti)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

846 
by (cases ?tv, auto simp add: numfloor_def Let_def split_def numadd) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

847 
from split_int[OF tvti] have "?N (Floor t) = ?N (Floor(Add ?tv ?ti))" and tii:"isint ?ti bs" by simp+ 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

848 
hence "?N (Floor t) = real (floor (?N (Add ?tv ?ti)))" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

849 
also have "\<dots> = real (floor (?N ?tv) + (floor (?N ?ti)))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

850 
by (simp,subst tii[simplified isint_iff, symmetric]) simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

851 
also have "\<dots> = ?N (Add (Floor ?tv) ?ti)" by (simp add: tii[simplified isint_iff]) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

852 
finally have ?thesis using th1 by simp} 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

853 
moreover {fix v assume H:"?tv = C v" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

854 
from split_int[OF tvti] have "?N (Floor t) = ?N (Floor(Add ?tv ?ti))" and tii:"isint ?ti bs" by simp+ 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

855 
hence "?N (Floor t) = real (floor (?N (Add ?tv ?ti)))" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

856 
also have "\<dots> = real (floor (?N ?tv) + (floor (?N ?ti)))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

857 
by (simp,subst tii[simplified isint_iff, symmetric]) simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

858 
also have "\<dots> = ?N (Add (Floor ?tv) ?ti)" by (simp add: tii[simplified isint_iff]) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

859 
finally have ?thesis by (simp add: H numfloor_def Let_def split_def numadd) } 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

860 
ultimately show ?thesis by auto 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

861 
qed 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

862 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

863 
lemma numfloor_nb[simp]: "numbound0 t \<Longrightarrow> numbound0 (numfloor t)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

864 
using split_int_nb[where t="t"] 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

865 
by (cases "fst(split_int t)" , auto simp add: numfloor_def Let_def split_def numadd_nb) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

866 

41839  867 
function simpnum:: "num \<Rightarrow> num" where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

868 
"simpnum (C j) = C j" 
41839  869 
 "simpnum (Bound n) = CN n 1 (C 0)" 
870 
 "simpnum (Neg t) = numneg (simpnum t)" 

871 
 "simpnum (Add t s) = numadd (simpnum t,simpnum s)" 

872 
 "simpnum (Sub t s) = numsub (simpnum t) (simpnum s)" 

873 
 "simpnum (Mul i t) = (if i = 0 then (C 0) else nummul (simpnum t) i)" 

874 
 "simpnum (Floor t) = numfloor (simpnum t)" 

875 
 "simpnum (CN n c t) = (if c=0 then simpnum t else CN n c (simpnum t))" 

876 
 "simpnum (CF c t s) = simpnum(Add (Mul c (Floor t)) s)" 

877 
by pat_completeness auto 

878 
termination by (relation "measure num_size") auto 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

879 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

880 
lemma simpnum_ci[simp]: "Inum bs (simpnum t) = Inum bs t" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

881 
by (induct t rule: simpnum.induct, auto) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

882 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

883 
lemma simpnum_numbound0[simp]: 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

884 
"numbound0 t \<Longrightarrow> numbound0 (simpnum t)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

885 
by (induct t rule: simpnum.induct, auto) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

886 

41839  887 
fun nozerocoeff:: "num \<Rightarrow> bool" where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

888 
"nozerocoeff (C c) = True" 
41839  889 
 "nozerocoeff (CN n c t) = (c\<noteq>0 \<and> nozerocoeff t)" 
890 
 "nozerocoeff (CF c s t) = (c \<noteq> 0 \<and> nozerocoeff t)" 

891 
 "nozerocoeff (Mul c t) = (c\<noteq>0 \<and> nozerocoeff t)" 

892 
 "nozerocoeff t = True" 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

893 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

894 
lemma numadd_nz : "nozerocoeff a \<Longrightarrow> nozerocoeff b \<Longrightarrow> nozerocoeff (numadd (a,b))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

895 
by (induct a b rule: numadd.induct,auto simp add: Let_def) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

896 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

897 
lemma nummul_nz : "\<And> i. i\<noteq>0 \<Longrightarrow> nozerocoeff a \<Longrightarrow> nozerocoeff (nummul a i)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

898 
by (induct a rule: nummul.induct,auto simp add: Let_def numadd_nz) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

899 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

900 
lemma numneg_nz : "nozerocoeff a \<Longrightarrow> nozerocoeff (numneg a)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

901 
by (simp add: numneg_def nummul_nz) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

902 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

903 
lemma numsub_nz: "nozerocoeff a \<Longrightarrow> nozerocoeff b \<Longrightarrow> nozerocoeff (numsub a b)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

904 
by (simp add: numsub_def numneg_nz numadd_nz) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

905 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

906 
lemma split_int_nz: "nozerocoeff t \<Longrightarrow> nozerocoeff (fst (split_int t)) \<and> nozerocoeff (snd (split_int t))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

907 
by (induct t rule: split_int.induct,auto simp add: Let_def split_def) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

908 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

909 
lemma numfloor_nz: "nozerocoeff t \<Longrightarrow> nozerocoeff (numfloor t)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

910 
by (simp add: numfloor_def Let_def split_def) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

911 
(cases "fst (split_int t)", simp_all add: split_int_nz numadd_nz) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

912 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

913 
lemma simpnum_nz: "nozerocoeff (simpnum t)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

914 
by(induct t rule: simpnum.induct, auto simp add: numadd_nz numneg_nz numsub_nz nummul_nz numfloor_nz) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

915 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

916 
lemma maxcoeff_nz: "nozerocoeff t \<Longrightarrow> maxcoeff t = 0 \<Longrightarrow> t = C 0" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

917 
proof (induct t rule: maxcoeff.induct) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

918 
case (2 n c t) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

919 
hence cnz: "c \<noteq>0" and mx: "max (abs c) (maxcoeff t) = 0" by simp+ 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

920 
have "max (abs c) (maxcoeff t) \<ge> abs c" by (simp add: le_maxI1) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

921 
with cnz have "max (abs c) (maxcoeff t) > 0" by arith 
41807  922 
with 2 show ?case by simp 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

923 
next 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

924 
case (3 c s t) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

925 
hence cnz: "c \<noteq>0" and mx: "max (abs c) (maxcoeff t) = 0" by simp+ 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

926 
have "max (abs c) (maxcoeff t) \<ge> abs c" by (simp add: le_maxI1) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

927 
with cnz have "max (abs c) (maxcoeff t) > 0" by arith 
41807  928 
with 3 show ?case by simp 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

929 
qed auto 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

930 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

931 
lemma numgcd_nz: assumes nz: "nozerocoeff t" and g0: "numgcd t = 0" shows "t = C 0" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

932 
proof 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

933 
from g0 have th:"numgcdh t (maxcoeff t) = 0" by (simp add: numgcd_def) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

934 
from numgcdh0[OF th] have th:"maxcoeff t = 0" . 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

935 
from maxcoeff_nz[OF nz th] show ?thesis . 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

936 
qed 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

937 

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

938 
definition simp_num_pair :: "(num \<times> int) \<Rightarrow> num \<times> int" where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

939 
"simp_num_pair \<equiv> (\<lambda> (t,n). (if n = 0 then (C 0, 0) else 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

940 
(let t' = simpnum t ; g = numgcd t' in 
31706  941 
if g > 1 then (let g' = gcd n g in 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

942 
if g' = 1 then (t',n) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

943 
else (reducecoeffh t' g', n div g')) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

944 
else (t',n))))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

945 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

946 
lemma simp_num_pair_ci: 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

947 
shows "((\<lambda> (t,n). Inum bs t / real n) (simp_num_pair (t,n))) = ((\<lambda> (t,n). Inum bs t / real n) (t,n))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

948 
(is "?lhs = ?rhs") 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

949 
proof 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

950 
let ?t' = "simpnum t" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

951 
let ?g = "numgcd ?t'" 
31706  952 
let ?g' = "gcd n ?g" 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

953 
{assume nz: "n = 0" hence ?thesis by (simp add: Let_def simp_num_pair_def)} 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

954 
moreover 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

955 
{ assume nnz: "n \<noteq> 0" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

956 
{assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simp_num_pair_def)} 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

957 
moreover 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

958 
{assume g1:"?g>1" hence g0: "?g > 0" by simp 
31706  959 
from g1 nnz have gp0: "?g' \<noteq> 0" by simp 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31730
diff
changeset

960 
hence g'p: "?g' > 0" using gcd_ge_0_int[where x="n" and y="numgcd ?t'"] by arith 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

961 
hence "?g'= 1 \<or> ?g' > 1" by arith 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

962 
moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simp_num_pair_def)} 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

963 
moreover {assume g'1:"?g'>1" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

964 
from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff ?t' ?g" .. 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

965 
let ?tt = "reducecoeffh ?t' ?g'" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

966 
let ?t = "Inum bs ?tt" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

967 
have gpdg: "?g' dvd ?g" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

968 
have gpdd: "?g' dvd n" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

969 
have gpdgp: "?g' dvd ?g'" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

970 
from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

971 
have th2:"real ?g' * ?t = Inum bs ?t'" by simp 
41807  972 
from nnz g1 g'1 have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_def Let_def) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

973 
also have "\<dots> = (real ?g' * ?t) / (real ?g' * (real (n div ?g')))" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

974 
also have "\<dots> = (Inum bs ?t' / real n)" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

975 
using real_of_int_div[OF gp0 gpdd] th2 gp0 by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

976 
finally have "?lhs = Inum bs t / real n" by simp 
41807  977 
then have ?thesis using nnz g1 g'1 by (simp add: simp_num_pair_def) } 
978 
ultimately have ?thesis by blast } 

979 
ultimately have ?thesis by blast } 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

980 
ultimately show ?thesis by blast 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

981 
qed 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

982 

41807  983 
lemma simp_num_pair_l: 
984 
assumes tnb: "numbound0 t" and np: "n >0" and tn: "simp_num_pair (t,n) = (t',n')" 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

985 
shows "numbound0 t' \<and> n' >0" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

986 
proof 
41807  987 
let ?t' = "simpnum t" 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

988 
let ?g = "numgcd ?t'" 
31706  989 
let ?g' = "gcd n ?g" 
41807  990 
{ assume nz: "n = 0" hence ?thesis using assms by (simp add: Let_def simp_num_pair_def) } 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

991 
moreover 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

992 
{ assume nnz: "n \<noteq> 0" 
41807  993 
{assume "\<not> ?g > 1" hence ?thesis using assms by (auto simp add: Let_def simp_num_pair_def) } 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

994 
moreover 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

995 
{assume g1:"?g>1" hence g0: "?g > 0" by simp 
31706  996 
from g1 nnz have gp0: "?g' \<noteq> 0" by simp 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31730
diff
changeset

997 
hence g'p: "?g' > 0" using gcd_ge_0_int[where x="n" and y="numgcd ?t'"] by arith 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

998 
hence "?g'= 1 \<or> ?g' > 1" by arith 
41807  999 
moreover {assume "?g'=1" hence ?thesis using assms g1 g0 
1000 
by (auto simp add: Let_def simp_num_pair_def) } 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1001 
moreover {assume g'1:"?g'>1" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

1002 
have gpdg: "?g' dvd ?g" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

1003 
have gpdd: "?g' dvd n" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

1004 
have gpdgp: "?g' dvd ?g'" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

1005 
from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" . 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

1006 
from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]] 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

1007 
have "n div ?g' >0" by simp 
41807  1008 
hence ?thesis using assms g1 g'1 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

1009 
by(auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0)} 
41807  1010 
ultimately have ?thesis by blast } 
1011 
ultimately have ?thesis by blast } 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1012 
ultimately show ?thesis by blast 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1013 
qed 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1014 

41839  1015 
fun not:: "fm \<Rightarrow> fm" where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1016 
"not (NOT p) = p" 
41839  1017 
 "not T = F" 
1018 
 "not F = T" 

1019 
 "not (Lt t) = Ge t" 

1020 
 "not (Le t) = Gt t" 

1021 
 "not (Gt t) = Le t" 

1022 
 "not (Ge t) = Lt t" 

1023 
 "not (Eq t) = NEq t" 

1024 
 "not (NEq t) = Eq t" 

1025 
 "not (Dvd i t) = NDvd i t" 

1026 
 "not (NDvd i t) = Dvd i t" 

1027 
 "not (And p q) = Or (not p) (not q)" 

1028 
 "not (Or p q) = And (not p) (not q)" 

1029 
 "not p = NOT p" 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1030 
lemma not[simp]: "Ifm bs (not p) = Ifm bs (NOT p)" 
41807  1031 
by (induct p) auto 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1032 
lemma not_qf[simp]: "qfree p \<Longrightarrow> qfree (not p)" 
41807  1033 
by (induct p) auto 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1034 
lemma not_nb[simp]: "bound0 p \<Longrightarrow> bound0 (not p)" 
41807  1035 
by (induct p) auto 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1036 

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

1037 
definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1038 
"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 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1039 
if p = q then p else And p q)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1040 
lemma conj[simp]: "Ifm bs (conj p q) = Ifm bs (And p q)" 
41807  1041 
by (cases "p=F \<or> q=F", simp_all add: conj_def) (cases p, simp_all) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1042 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1043 
lemma conj_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (conj p q)" 
41807  1044 
using conj_def by auto 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1045 
lemma conj_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (conj p q)" 
41807  1046 
using conj_def by auto 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1047 

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

1048 
definition disj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1049 
"disj p q \<equiv> (if (p = T \<or> q=T) then T else if p=F then q else if q=F then p 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1050 
else if p=q then p else Or p q)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1051 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1052 
lemma disj[simp]: "Ifm bs (disj p q) = Ifm bs (Or p q)" 
41807  1053 
by (cases "p=T \<or> q=T",simp_all add: disj_def) (cases p,simp_all) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1054 
lemma disj_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (disj p q)" 
41807  1055 
using disj_def by auto 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1056 
lemma disj_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (disj p q)" 
41807  1057 
using disj_def by auto 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1058 

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

1059 
definition imp :: "fm \<Rightarrow> fm \<Rightarrow> fm" where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1060 
"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 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1061 
else Imp p q)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1062 
lemma imp[simp]: "Ifm bs (imp p q) = Ifm bs (Imp p q)" 
41807  1063 
by (cases "p=F \<or> q=T",simp_all add: imp_def) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1064 
lemma imp_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (imp p q)" 
41807  1065 
using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1066 

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

1067 
definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm" where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1068 
"iff p q \<equiv> (if (p = q) then T else if (p = not q \<or> not p = q) then F else 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1069 
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 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1070 
Iff p q)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1071 
lemma iff[simp]: "Ifm bs (iff p q) = Ifm bs (Iff p q)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1072 
by (unfold iff_def,cases "p=q", simp,cases "p=not q", simp add:not) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1073 
(cases "not p= q", auto simp add:not) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1074 
lemma iff_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (iff p q)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1075 
by (unfold iff_def,cases "p=q", auto) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1076 

41839  1077 
fun check_int:: "num \<Rightarrow> bool" where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1078 
"check_int (C i) = True" 
41839  1079 
 "check_int (Floor t) = True" 
1080 
 "check_int (Mul i t) = check_int t" 

1081 
 "check_int (Add t s) = (check_int t \<and> check_int s)" 

1082 
 "check_int (Neg t) = check_int t" 

1083 
 "check_int (CF c t s) = check_int s" 

1084 
 "check_int t = False" 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1085 
lemma check_int: "check_int t \<Longrightarrow> isint t bs" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1086 
by (induct t, auto simp add: isint_add isint_Floor isint_Mul isint_neg isint_c isint_CF) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1087 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1088 
lemma rdvd_left1_int: "real \<lfloor>t\<rfloor> = t \<Longrightarrow> 1 rdvd t" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1089 
by (simp add: rdvd_def,rule_tac x="\<lfloor>t\<rfloor>" in exI) simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1090 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1091 
lemma rdvd_reduce: 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1092 
assumes gd:"g dvd d" and gc:"g dvd c" and gp: "g > 0" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1093 
shows "real (d::int) rdvd real (c::int)*t = (real (d div g) rdvd real (c div g)*t)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1094 
proof 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1095 
assume d: "real d rdvd real c * t" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1096 
from d rdvd_def obtain k where k_def: "real c * t = real d* real (k::int)" by auto 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1097 
from gd dvd_def obtain kd where kd_def: "d = g * kd" by auto 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1098 
from gc dvd_def obtain kc where kc_def: "c = g * kc" by auto 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1099 
from k_def kd_def kc_def have "real g * real kc * t = real g * real kd * real k" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1100 
hence "real kc * t = real kd * real k" using gp by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1101 
hence th:"real kd rdvd real kc * t" using rdvd_def by blast 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1102 
from kd_def gp have th':"kd = d div g" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1103 
from kc_def gp have "kc = c div g" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1104 
with th th' show "real (d div g) rdvd real (c div g) * t" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1105 
next 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1106 
assume d: "real (d div g) rdvd real (c div g) * t" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1107 
from gp have gnz: "g \<noteq> 0" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1108 
thus "real d rdvd real c * t" using d rdvd_mult[OF gnz, where n="d div g" and x="real (c div g) * t"] real_of_int_div[OF gnz gd] real_of_int_div[OF gnz gc] by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1109 
qed 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1110 

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

1111 
definition simpdvd :: "int \<Rightarrow> num \<Rightarrow> (int \<times> num)" where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1112 
"simpdvd d t \<equiv> 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1113 
(let g = numgcd t in 
31706  1114 
if g > 1 then (let g' = gcd d g in 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1115 
if g' = 1 then (d, t) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1116 
else (d div g',reducecoeffh t g')) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1117 
else (d, t))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1118 
lemma simpdvd: 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1119 
assumes tnz: "nozerocoeff t" and dnz: "d \<noteq> 0" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1120 
shows "Ifm bs (Dvd (fst (simpdvd d t)) (snd (simpdvd d t))) = Ifm bs (Dvd d t)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1121 
proof 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1122 
let ?g = "numgcd t" 
31706  1123 
let ?g' = "gcd d ?g" 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1124 
{assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simpdvd_def)} 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1125 
moreover 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1126 
{assume g1:"?g>1" hence g0: "?g > 0" by simp 
31706  1127 
from g1 dnz have gp0: "?g' \<noteq> 0" by simp 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31730
diff
changeset

1128 
hence g'p: "?g' > 0" using gcd_ge_0_int[where x="d" and y="numgcd t"] by arith 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1129 
hence "?g'= 1 \<or> ?g' > 1" by arith 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1130 
moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simpdvd_def)} 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1131 
moreover {assume g'1:"?g'>1" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1132 
from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff t ?g" .. 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1133 
let ?tt = "reducecoeffh t ?g'" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1134 
let ?t = "Inum bs ?tt" 
31706  1135 
have gpdg: "?g' dvd ?g" by simp 
1136 
have gpdd: "?g' dvd d" by simp 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1137 
have gpdgp: "?g' dvd ?g'" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1138 
from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1139 
have th2:"real ?g' * ?t = Inum bs t" by simp 
41807  1140 
from assms g1 g0 g'1 
1141 
have "Ifm bs (Dvd (fst (simpdvd d t)) (snd(simpdvd d t))) = Ifm bs (Dvd (d div ?g') ?tt)" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

1142 
by (simp add: simpdvd_def Let_def) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1143 
also have "\<dots> = (real d rdvd (Inum bs t))" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

1144 
using rdvd_reduce[OF gpdd gpdgp g'p, where t="?t", simplified zdiv_self[OF gp0]] 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

1145 
th2[symmetric] by simp 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1146 
finally have ?thesis by simp } 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1147 
ultimately have ?thesis by blast 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1148 
} 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1149 
ultimately show ?thesis by blast 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1150 
qed 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1151 

41839  1152 
function (sequential) simpfm :: "fm \<Rightarrow> fm" where 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1153 
"simpfm (And p q) = conj (simpfm p) (simpfm q)" 
41839  1154 
 "simpfm (Or p q) = disj (simpfm p) (simpfm q)" 
1155 
 "simpfm (Imp p q) = imp (simpfm p) (simpfm q)" 

1156 
 "simpfm (Iff p q) = iff (simpfm p) (simpfm q)" 

1157 
 "simpfm (NOT p) = not (simpfm p)" 

1158 
 "simpfm (Lt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v < 0) then T else F 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1159 
 _ \<Rightarrow> Lt (reducecoeff a'))" 
41839  1160 
 "simpfm (Le a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<le> 0) then T else F  _ \<Rightarrow> Le (reducecoeff a'))" 
1161 
 "simpfm (Gt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v > 0) then T else F  _ \<Rightarrow> Gt (reducecoeff a'))" 

1162 
 "simpfm (Ge a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<ge> 0) then T else F  _ \<Rightarrow> Ge (reducecoeff a'))" 

1163 
 "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v = 0) then T else F  _ \<Rightarrow> Eq (reducecoeff a'))" 

1164 
 "simpfm (NEq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<noteq> 0) then T else F  _ \<Rightarrow> NEq (reducecoeff a'))" 

1165 
 "simpfm (Dvd i a) = (if i=0 then simpfm (Eq a) 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1166 
else if (abs i = 1) \<and> check_int a then T 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1167 
else let a' = simpnum a in case a' of C v \<Rightarrow> if (i dvd v) then T else F  _ \<Rightarrow> (let (d,t) = simpdvd i a' in Dvd d t))" 
41839  1168 
 "simpfm (NDvd i a) = (if i=0 then simpfm (NEq a) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1169 
else if (abs i = 1) \<and> check_int a then F 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1170 
else let a' = simpnum a in case a' of C v \<Rightarrow> if (\<not>(i dvd v)) then T else F  _ \<Rightarrow> (let (d,t) = simpdvd i a' in NDvd d t))" 
41839  1171 
 "simpfm p = p" 
1172 
by pat_completeness auto 

1173 
termination by (relation "measure fmsize") auto 

23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1174 

324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1175 
lemma simpfm[simp]: "Ifm bs (simpfm p) = Ifm bs p" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1176 
proof(induct p rule: simpfm.induct) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1177 
case (6 a) let ?sa = "simpnum a" have sa: "Inum bs ?sa = Inum bs a" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1178 
{fix v assume "?sa = C v" hence ?case using sa by simp } 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1179 
moreover {assume H:"\<not> (\<exists> v. ?sa = C v)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1180 
let ?g = "numgcd ?sa" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1181 
let ?rsa = "reducecoeff ?sa" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1182 
let ?r = "Inum bs ?rsa" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1183 
have sa_nz: "nozerocoeff ?sa" by (rule simpnum_nz) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1184 
{assume gz: "?g=0" from numgcd_nz[OF sa_nz gz] H have "False" by auto} 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1185 
with numgcd_pos[where t="?sa"] have "?g > 0" by (cases "?g=0", auto) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1186 
hence gp: "real ?g > 0" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1187 
have "Inum bs ?sa = real ?g* ?r" by (simp add: reducecoeff) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1188 
with sa have "Inum bs a < 0 = (real ?g * ?r < real ?g * 0)" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1189 
also have "\<dots> = (?r < 0)" using gp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1190 
by (simp only: mult_less_cancel_left) simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1191 
finally have ?case using H by (cases "?sa" , simp_all add: Let_def)} 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1192 
ultimately show ?case by blast 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1193 
next 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1194 
case (7 a) let ?sa = "simpnum a" have sa: "Inum bs ?sa = Inum bs a" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1195 
{fix v assume "?sa = C v" hence ?case using sa by simp } 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1196 
moreover {assume H:"\<not> (\<exists> v. ?sa = C v)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1197 
let ?g = "numgcd ?sa" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1198 
let ?rsa = "reducecoeff ?sa" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1199 
let ?r = "Inum bs ?rsa" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1200 
have sa_nz: "nozerocoeff ?sa" by (rule simpnum_nz) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1201 
{assume gz: "?g=0" from numgcd_nz[OF sa_nz gz] H have "False" by auto} 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1202 
with numgcd_pos[where t="?sa"] have "?g > 0" by (cases "?g=0", auto) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1203 
hence gp: "real ?g > 0" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1204 
have "Inum bs ?sa = real ?g* ?r" by (simp add: reducecoeff) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1205 
with sa have "Inum bs a \<le> 0 = (real ?g * ?r \<le> real ?g * 0)" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1206 
also have "\<dots> = (?r \<le> 0)" using gp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1207 
by (simp only: mult_le_cancel_left) simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1208 
finally have ?case using H by (cases "?sa" , simp_all add: Let_def)} 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1209 
ultimately show ?case by blast 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1210 
next 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1211 
case (8 a) let ?sa = "simpnum a" have sa: "Inum bs ?sa = Inum bs a" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1212 
{fix v assume "?sa = C v" hence ?case using sa by simp } 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1213 
moreover {assume H:"\<not> (\<exists> v. ?sa = C v)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1214 
let ?g = "numgcd ?sa" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1215 
let ?rsa = "reducecoeff ?sa" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1216 
let ?r = "Inum bs ?rsa" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1217 
have sa_nz: "nozerocoeff ?sa" by (rule simpnum_nz) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1218 
{assume gz: "?g=0" from numgcd_nz[OF sa_nz gz] H have "False" by auto} 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1219 
with numgcd_pos[where t="?sa"] have "?g > 0" by (cases "?g=0", auto) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1220 
hence gp: "real ?g > 0" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1221 
have "Inum bs ?sa = real ?g* ?r" by (simp add: reducecoeff) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1222 
with sa have "Inum bs a > 0 = (real ?g * ?r > real ?g * 0)" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1223 
also have "\<dots> = (?r > 0)" using gp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1224 
by (simp only: mult_less_cancel_left) simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1225 
finally have ?case using H by (cases "?sa" , simp_all add: Let_def)} 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1226 
ultimately show ?case by blast 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1227 
next 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1228 
case (9 a) let ?sa = "simpnum a" have sa: "Inum bs ?sa = Inum bs a" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1229 
{fix v assume "?sa = C v" hence ?case using sa by simp } 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1230 
moreover {assume H:"\<not> (\<exists> v. ?sa = C v)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1231 
let ?g = "numgcd ?sa" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1232 
let ?rsa = "reducecoeff ?sa" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1233 
let ?r = "Inum bs ?rsa" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1234 
have sa_nz: "nozerocoeff ?sa" by (rule simpnum_nz) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1235 
{assume gz: "?g=0" from numgcd_nz[OF sa_nz gz] H have "False" by auto} 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1236 
with numgcd_pos[where t="?sa"] have "?g > 0" by (cases "?g=0", auto) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1237 
hence gp: "real ?g > 0" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1238 
have "Inum bs ?sa = real ?g* ?r" by (simp add: reducecoeff) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1239 
with sa have "Inum bs a \<ge> 0 = (real ?g * ?r \<ge> real ?g * 0)" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1240 
also have "\<dots> = (?r \<ge> 0)" using gp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1241 
by (simp only: mult_le_cancel_left) simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1242 
finally have ?case using H by (cases "?sa" , simp_all add: Let_def)} 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1243 
ultimately show ?case by blast 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1244 
next 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1245 
case (10 a) let ?sa = "simpnum a" have sa: "Inum bs ?sa = Inum bs a" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1246 
{fix v assume "?sa = C v" hence ?case using sa by simp } 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1247 
moreover {assume H:"\<not> (\<exists> v. ?sa = C v)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1248 
let ?g = "numgcd ?sa" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1249 
let ?rsa = "reducecoeff ?sa" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1250 
let ?r = "Inum bs ?rsa" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1251 
have sa_nz: "nozerocoeff ?sa" by (rule simpnum_nz) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1252 
{assume gz: "?g=0" from numgcd_nz[OF sa_nz gz] H have "False" by auto} 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1253 
with numgcd_pos[where t="?sa"] have "?g > 0" by (cases "?g=0", auto) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1254 
hence gp: "real ?g > 0" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1255 
have "Inum bs ?sa = real ?g* ?r" by (simp add: reducecoeff) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1256 
with sa have "Inum bs a = 0 = (real ?g * ?r = 0)" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1257 
also have "\<dots> = (?r = 0)" using gp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1258 
by (simp add: mult_eq_0_iff) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1259 
finally have ?case using H by (cases "?sa" , simp_all add: Let_def)} 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1260 
ultimately show ?case by blast 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1261 
next 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1262 
case (11 a) let ?sa = "simpnum a" have sa: "Inum bs ?sa = Inum bs a" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1263 
{fix v assume "?sa = C v" hence ?case using sa by simp } 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1264 
moreover {assume H:"\<not> (\<exists> v. ?sa = C v)" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1265 
let ?g = "numgcd ?sa" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1266 
let ?rsa = "reducecoeff ?sa" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1267 
let ?r = "Inum bs ?rsa" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1268 
have sa_nz: "nozerocoeff ?sa" by (rule simpnum_nz) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1269 
{assume gz: "?g=0" from numgcd_nz[OF sa_nz gz] H have "False" by auto} 
