author  hoelzl 
Wed, 11 Mar 2009 10:58:18 +0100  
changeset 30439  57c68b3af2ea 
parent 30242  aea5d7fa7ef5 
child 30649  57753e0ec1d4 
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 
29811
026b0f9f579f
fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library
chaieb@chaieblaptop
parents:
29788
diff
changeset

6 
imports Complex_Main Dense_Linear_Order Efficient_Nat 
29788  7 
uses ("mir_tac.ML") 
27368  8 
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

9 

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

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

12 
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

13 

25765  14 
primrec alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) 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

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

16 
 "alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs 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

17 

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

18 
lemma alluopairs_set1: "set (alluopairs xs) \<le> {(x,y). x\<in> set xs \<and> y\<in> set 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

19 
by (induct xs, 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

20 

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

21 
lemma alluopairs_set: 
324622260d29
Added 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 
"\<lbrakk>x\<in> set xs ; y \<in> set xs\<rbrakk> \<Longrightarrow> (x,y) \<in> set (alluopairs xs) \<or> (y,x) \<in> set (alluopairs 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

23 
by (induct xs, 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

24 

324622260d29
Added 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 
lemma alluopairs_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

26 
assumes Pc: "\<forall> x y. P x y = P y 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 
shows "(\<exists> x \<in> set xs. \<exists> y \<in> set xs. P x y) = (\<exists> (x,y) \<in> set (alluopairs xs). P x 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

28 
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

29 
assume "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x 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

30 
then obtain x y where x: "x \<in> set xs" and y:"y \<in> set xs" and P: "P x y" 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

31 
from alluopairs_set[OF x y] P Pc show"\<exists>(x, y)\<in>set (alluopairs xs). P x 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

32 
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

33 
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

34 
assume "\<exists>(x, y)\<in>set (alluopairs xs). P x 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

35 
then obtain "x" and "y" where xy:"(x,y) \<in> set (alluopairs xs)" and P: "P x y" 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

36 
from xy have "x \<in> set xs \<and> y\<in> set xs" using alluopairs_set1 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

37 
with P show "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y" 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

38 
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

39 

324622260d29
Added 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 
(* generate a list from i to j*) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

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

42 
recdef iupt "measure (\<lambda> (i,j). nat (ji +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

43 
"iupt (i,j) = (if j <i then [] else (i# iupt(i+1, j)))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

44 

324622260d29
Added 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 
lemma iupt_set: "set (iupt(i,j)) = {i .. j}" 
324622260d29
Added 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 
proof(induct rule: iupt.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

47 
case (1 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

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

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

50 
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

51 

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

52 
lemma nth_pos2: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (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

53 
using Nat.gr0_conv_Suc 
324622260d29
Added 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 
by clarsimp 
324622260d29
Added 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 

324622260d29
Added 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 

324622260d29
Added 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 
lemma myl: "\<forall> (a::'a::{pordered_ab_group_add}) (b::'a). (a \<le> b) = (0 \<le> b  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

58 
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

59 
fix x y ::"'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

60 
have "(x \<le> y) = (x  y \<le> 0)" by (simp only: le_iff_diff_le_0[where a="x" and b="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

61 
also have "\<dots> = ( (y  x) \<le> 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

62 
also have "\<dots> = (0 \<le> y  x)" by (simp only: neg_le_0_iff_le[where a="yx"]) 
324622260d29
Added 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 
finally show "(x \<le> y) = (0 \<le> y  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

64 
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

65 

324622260d29
Added 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 
lemma myless: "\<forall> (a::'a::{pordered_ab_group_add}) (b::'a). (a < b) = (0 < b  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

67 
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

68 
fix x y ::"'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

69 
have "(x < y) = (x  y < 0)" by (simp only: less_iff_diff_less_0[where a="x" and b="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

70 
also have "\<dots> = ( (y  x) < 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

71 
also have "\<dots> = (0 < y  x)" by (simp only: neg_less_0_iff_less[where a="yx"]) 
324622260d29
Added 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 
finally show "(x < y) = (0 < y  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

73 
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

74 

324622260d29
Added 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 
lemma myeq: "\<forall> (a::'a::{pordered_ab_group_add}) (b::'a). (a = b) = (0 = b  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

76 
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

77 

324622260d29
Added 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 
(* 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

79 
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

80 
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

81 
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

82 
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

83 
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

84 
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

85 
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

86 
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

87 
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

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

91 
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

92 
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

93 
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

94 
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

95 
proof 
23316  96 
{fix x k 
97 
from inf_period(3)[OF advdd, rule_format, where x=x and k="k"] 

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

99 
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

100 
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

101 
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

102 

324622260d29
Added 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 
(* The Divisibility relation between reals *) 
23858  104 
definition 
105 
rdvd:: "real \<Rightarrow> real \<Rightarrow> bool" (infixl "rdvd" 50) 

106 
where 

107 
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

108 

324622260d29
Added 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 
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

110 
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

111 
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

112 
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

113 
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

114 
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

115 
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

116 
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

117 
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

118 
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

119 
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

120 
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

121 
by (simp only: real_of_int_inject) (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

122 
thus ?l using prems 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

123 
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

124 

324622260d29
Added 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 
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

126 
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

127 

324622260d29
Added 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 

324622260d29
Added 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 
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

130 
"(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

131 
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

132 
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

133 
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

134 

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

136 
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

137 
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

138 
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

139 
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

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

142 
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

143 
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

144 

324622260d29
Added 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 
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

146 
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

147 
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

148 
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

149 
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

150 

324622260d29
Added 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 
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

152 
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

153 

324622260d29
Added 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 
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

155 
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

156 
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

157 
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

158 

324622260d29
Added 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 
lemma rdvd_trans: assumes mn:"m rdvd n" and nk:"n rdvd 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

160 
shows "m rdvd 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

161 
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

162 
from rdvd_def mn obtain c where nmc:"n = m * real (c::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

163 
from rdvd_def nk obtain c' where nkc:"k = n * real (c'::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

164 
hence "k = m * real (c * c')" using nmc 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

165 
thus ?thesis 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

166 
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

167 

324622260d29
Added 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 
(*********************************************************************************) 
324622260d29
Added 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 
(**** 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

170 
(*********************************************************************************) 
324622260d29
Added 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 

324622260d29
Added 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 
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

173 
 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

174 

324622260d29
Added 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 
(* A size for num to make inductive proofs simpler*) 
25765  176 
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

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

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

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

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

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

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

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

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

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

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 
(* Semantics of numeral terms (num) *) 
25765  188 
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

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

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

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

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

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

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

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

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

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

198 
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

199 

324622260d29
Added 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 
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

201 
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

202 

324622260d29
Added 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 
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

204 
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

205 

324622260d29
Added 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 
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

207 
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

208 
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

209 
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

210 
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

211 
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

212 
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

213 
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

214 
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

215 
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

216 

324622260d29
Added 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 
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

218 
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

219 
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

220 
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

221 
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

222 
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

223 
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

224 
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

225 
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

226 

324622260d29
Added 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 
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

228 
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

229 
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

230 
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

231 
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

232 
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

233 
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

234 
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

235 
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

236 

324622260d29
Added 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 
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

238 
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

239 
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

240 
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

241 
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

242 
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

243 
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

244 
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

245 
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

246 
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

247 

324622260d29
Added 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 
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

249 
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

250 

324622260d29
Added 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 

324622260d29
Added 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 
(* 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

253 
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

254 
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

255 
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

256 

324622260d29
Added 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 

324622260d29
Added 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 
(* 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

259 
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

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

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

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

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

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

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

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

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

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

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

270 
(* several lemmas about fmsize *) 
25162  271 
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

272 
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

273 

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

274 
(* Semantics of formulae (fm) *) 
25765  275 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

293 

324622260d29
Added 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 
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

295 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

318 
"prep p = p" 
25162  319 
(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

320 
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

321 
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

322 

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

323 

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

324 
(* Quantifier freeness *) 
25765  325 
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

326 
"qfree (E p) = False" 
25765  327 
 "qfree (A p) = False" 
328 
 "qfree (NOT p) = qfree p" 

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

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

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

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

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

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 
(* Boundedness and substitution *) 
25765  336 
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

337 
"numbound0 (C c) = True" 
25765  338 
 "numbound0 (Bound n) = (n>0)" 
339 
 "numbound0 (CN n i a) = (n > 0 \<and> numbound0 a)" 

340 
 "numbound0 (Neg a) = numbound0 a" 

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

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

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

344 
 "numbound0 (Floor a) = numbound0 a" 

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

346 

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

347 
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

348 
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

349 
shows "Inum (b#bs) a = Inum (b'#bs) a" 
25765  350 
using nb by (induct a) (auto simp add: nth_pos2) 
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

351 

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

352 
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

353 
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

354 
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

355 
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

356 
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

357 
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

358 
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

359 
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

360 
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

361 
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

362 

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

364 
"bound0 T = True" 
25765  365 
 "bound0 F = True" 
366 
 "bound0 (Lt a) = numbound0 a" 

367 
 "bound0 (Le a) = numbound0 a" 

368 
 "bound0 (Gt a) = numbound0 a" 

369 
 "bound0 (Ge a) = numbound0 a" 

370 
 "bound0 (Eq a) = numbound0 a" 

371 
 "bound0 (NEq a) = numbound0 a" 

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

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

374 
 "bound0 (NOT p) = bound0 p" 

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

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

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

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

379 
 "bound0 (E p) = False" 

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

381 

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

382 
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

383 
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

384 
shows "Ifm (b#bs) p = Ifm (b'#bs) p" 
25765  385 
using bp numbound0_I [where b="b" and bs="bs" and b'="b'"] 
386 
by (induct p) (auto simp add: nth_pos2) 

387 

388 
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

389 
"numsubst0 t (C c) = (C c)" 
25765  390 
 "numsubst0 t (Bound n) = (if n=0 then t else Bound n)" 
391 
 "numsubst0 t (CN n i a) = (if n=0 then Add (Mul i t) (numsubst0 t a) else CN n i (numsubst0 t a))" 

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

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

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

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

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

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

398 

324622260d29
Added 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 
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

400 
shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#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

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

402 

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

403 
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

404 
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

405 
shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#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

406 
by (induct t) (simp_all add: nth_pos2 numbound0_I[OF nb, where b="b" and b'="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

407 

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

409 
"subst0 t T = T" 
25765  410 
 "subst0 t F = F" 
411 
 "subst0 t (Lt a) = Lt (numsubst0 t a)" 

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

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

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

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

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

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

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

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

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

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

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

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

424 

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

425 
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

426 
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

427 
using qfp numsubst0_I[where b="b" and bs="bs" and a="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

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

429 

25765  430 
consts 
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 
decrnum:: "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

432 
decr :: "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

433 

324622260d29
Added 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 
recdef decrnum "measure size" 
324622260d29
Added 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 
"decrnum (Bound n) = 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

436 
"decrnum (Neg a) = Neg (decrnum 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

437 
"decrnum (Add a b) = Add (decrnum a) (decrnum 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

438 
"decrnum (Sub a b) = Sub (decrnum a) (decrnum 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

439 
"decrnum (Mul c a) = Mul c (decrnum 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

440 
"decrnum (Floor a) = Floor (decrnum 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

441 
"decrnum (CN n c a) = CN (n  1) c (decrnum 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

442 
"decrnum (CF c a b) = CF c (decrnum a) (decrnum 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

443 
"decrnum a = 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

444 

324622260d29
Added 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 
recdef decr "measure size" 
324622260d29
Added 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 
"decr (Lt a) = Lt (decrnum 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

447 
"decr (Le a) = Le (decrnum 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

448 
"decr (Gt a) = Gt (decrnum 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

449 
"decr (Ge a) = Ge (decrnum 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

450 
"decr (Eq a) = Eq (decrnum 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

451 
"decr (NEq a) = NEq (decrnum 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

452 
"decr (Dvd i a) = Dvd i (decrnum 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

453 
"decr (NDvd i a) = NDvd i (decrnum 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

454 
"decr (NOT p) = NOT (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

455 
"decr (And p q) = And (decr p) (decr 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

456 
"decr (Or p q) = Or (decr p) (decr 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

457 
"decr (Imp p q) = Imp (decr p) (decr 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

458 
"decr (Iff p q) = Iff (decr p) (decr 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

459 
"decr p = 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 

324622260d29
Added 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 
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

462 
shows "Inum (x#bs) t = Inum bs (decrnum 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

463 
using nb by (induct t rule: decrnum.induct, simp_all add: nth_pos2) 
324622260d29
Added 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 

324622260d29
Added 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 
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

466 
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

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

468 
by (induct p rule: decr.induct, simp_all add: nth_pos2 decrnum) 
324622260d29
Added 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 

324622260d29
Added 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 
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

471 
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

472 

324622260d29
Added 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 
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

474 
isatom :: "fm \<Rightarrow> bool" (* test for atomicity *) 
324622260d29
Added 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 
recdef isatom "measure size" 
324622260d29
Added 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 
"isatom 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

477 
"isatom F = 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

478 
"isatom (Lt a) = 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

479 
"isatom (Le a) = 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

480 
"isatom (Gt a) = 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

481 
"isatom (Ge a) = 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

482 
"isatom (Eq a) = 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

483 
"isatom (NEq a) = 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

484 
"isatom (Dvd i b) = 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

485 
"isatom (NDvd i b) = 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

486 
"isatom p = 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

487 

324622260d29
Added 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 
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

489 
shows "numbound0 (numsubst0 t a)" 
25765  490 
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

491 

324622260d29
Added 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 
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

493 
shows "bound0 (subst0 t p)" 
25765  494 
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

495 

324622260d29
Added 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 
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

497 
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

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 

25765  500 
definition djf:: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm" where 
501 
"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

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

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

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

506 

324622260d29
Added 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 
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

508 
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

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

510 

324622260d29
Added 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 
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

512 
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

513 

324622260d29
Added 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 
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

515 
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

516 
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

517 
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

518 

324622260d29
Added 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 
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

520 
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

521 
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

522 
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

523 

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

524 
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

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

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

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

528 
"disjuncts (Or p q) = (disjuncts p) @ (disjuncts 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

529 
"disjuncts 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

530 
"disjuncts p = [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

531 

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

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

533 
"conjuncts (And p q) = (conjuncts p) @ (conjuncts 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

534 
"conjuncts 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

535 
"conjuncts p = [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

536 
lemma disjuncts: "(\<exists> q\<in> set (disjuncts 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

537 
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

538 
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

539 
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

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 disjuncts_nb: "bound0 p \<Longrightarrow> \<forall> q\<in> set (disjuncts p). bound0 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

542 
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

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

544 
hence "list_all bound0 (disjuncts 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

545 
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

546 
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

547 
lemma conjuncts_nb: "bound0 p \<Longrightarrow> \<forall> q\<in> set (conjuncts p). bound0 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

548 
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

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

550 
hence "list_all bound0 (conjuncts p)" 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

551 
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

552 
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

553 

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

554 
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

555 
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

556 
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

557 
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

558 
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

559 
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

560 
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

561 
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

562 
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

563 
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

564 
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

565 
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

566 
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

567 
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

568 

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

569 
constdefs DJ :: "(fm \<Rightarrow> fm) \<Rightarrow> 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

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

571 

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

572 
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

573 
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

574 
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

575 
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

576 
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

577 
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

578 
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

579 
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

580 
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

581 

324622260d29
Added 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 
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

583 
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

584 
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

585 
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

586 
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

587 
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

588 
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

589 
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

590 

324622260d29
Added 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 
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

592 
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

593 

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

594 
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

595 
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

596 
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

597 
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

598 
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

599 
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

600 
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

601 
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

602 
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

603 
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

604 
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

605 
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

606 
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

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

608 

324622260d29
Added 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 
(* Algebraic simplifications for nums *) 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

610 
consts bnds:: "num \<Rightarrow> nat list" 
324622260d29
Added 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 
lex_ns:: "nat list \<times> nat list \<Rightarrow> bool" 
324622260d29
Added 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 
recdef bnds "measure size" 
324622260d29
Added 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 
"bnds (Bound n) = [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

614 
"bnds (CN n c a) = n#(bnds 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

615 
"bnds (Neg a) = bnds 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

616 
"bnds (Add a b) = (bnds a)@(bnds 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

617 
"bnds (Sub a b) = (bnds a)@(bnds 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

618 
"bnds (Mul i a) = bnds 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

619 
"bnds (Floor a) = bnds 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

620 
"bnds (CF c a b) = (bnds a)@(bnds 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

621 
"bnds 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

622 
recdef lex_ns "measure (\<lambda> (xs,ys). length xs + length ys)" 
324622260d29
Added 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 
"lex_ns ([], ms) = 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

624 
"lex_ns (ns, []) = 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

625 
"lex_ns (n#ns, m#ms) = (n<m \<or> ((n = m) \<and> lex_ns (ns,ms))) " 
324622260d29
Added 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 
constdefs lex_bnd :: "num \<Rightarrow> num \<Rightarrow> bool" 
324622260d29
Added 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 
"lex_bnd t s \<equiv> lex_ns (bnds t, bnds 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

628 

324622260d29
Added 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 
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

630 
numgcdh:: "num \<Rightarrow> int \<Rightarrow> 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

631 
reducecoeffh:: "num \<Rightarrow> int \<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

632 
dvdnumcoeff:: "num \<Rightarrow> int \<Rightarrow> bool" 
324622260d29
Added 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 
consts maxcoeff:: "num \<Rightarrow> 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

634 
recdef maxcoeff "measure size" 
324622260d29
Added 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 
"maxcoeff (C i) = abs 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

636 
"maxcoeff (CN n c t) = max (abs c) (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

637 
"maxcoeff (CF c t s) = max (abs c) (maxcoeff 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

638 
"maxcoeff 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

639 

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

640 
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

641 
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

642 
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

643 

324622260d29
Added 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 
recdef numgcdh "measure size" 
27556  645 
"numgcdh (C i) = (\<lambda>g. zgcd i g)" 
646 
"numgcdh (CN n c t) = (\<lambda>g. zgcd c (numgcdh t g))" 

647 
"numgcdh (CF c s t) = (\<lambda>g. zgcd c (numgcdh 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

648 
"numgcdh t = (\<lambda>g. 1)" 
23858  649 

650 
definition 

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

652 
where 

653 
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

654 

324622260d29
Added 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 
recdef reducecoeffh "measure size" 
324622260d29
Added 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 
"reducecoeffh (C i) = (\<lambda> g. C (i 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

657 
"reducecoeffh (CN n c t) = (\<lambda> g. CN n (c 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

658 
"reducecoeffh (CF c s t) = (\<lambda> g. CF (c div g) s (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

659 
"reducecoeffh t = (\<lambda>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

660 

23858  661 
definition 
662 
reducecoeff :: "num \<Rightarrow> num" 

663 
where 

664 
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

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

666 
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

667 

324622260d29
Added 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 
recdef dvdnumcoeff "measure size" 
324622260d29
Added 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 
"dvdnumcoeff (C i) = (\<lambda> g. g dvd 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

670 
"dvdnumcoeff (CN n c t) = (\<lambda> g. g dvd c \<and> (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

671 
"dvdnumcoeff (CF c s t) = (\<lambda> g. g dvd c \<and> (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

672 
"dvdnumcoeff t = (\<lambda>g. 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

673 

324622260d29
Added 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 
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

675 
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

676 
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

677 
using dgt' gdg 
30042  678 
by (induct t rule: dvdnumcoeff.induct, simp_all add: gdg dvd_trans[OF gdg]) 
679 

680 
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

681 

324622260d29
Added 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 
lemma natabs0: "(nat (abs x) = 0) = (x = 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

683 
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

684 

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

685 
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

686 
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

687 
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

688 
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

689 
have "\<And>x. numgcdh t x= 0 \<Longrightarrow> Inum bs t = 0" 
27556  690 
by (induct t rule: numgcdh.induct, auto simp add: zgcd_def gcd_zero natabs0 max_def maxcoeff_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

691 
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

692 
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

693 

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

694 
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

695 
using gp 
27556  696 
by (induct t rule: numgcdh.induct, auto simp add: zgcd_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

697 

324622260d29
Added 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 
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

699 
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

700 

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

701 
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

702 
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

703 
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

704 
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

705 
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

706 
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

707 
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

708 
from prems show ?case by (simp add: real_of_int_div[OF gnz gd]) 
324622260d29
Added 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 
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

710 
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

711 
from gp have gnz: "g \<noteq> 0" by simp 
29667  712 
from prems 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

713 
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

714 
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

715 
from gp have gnz: "g \<noteq> 0" by simp 
29667  716 
from prems 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

717 
qed (auto simp add: numgcd_def 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

718 
consts ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool" 
324622260d29
Added 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 
recdef ismaxcoeff "measure size" 
324622260d29
Added 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 
"ismaxcoeff (C i) = (\<lambda> x. abs i \<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

721 
"ismaxcoeff (CN n c t) = (\<lambda>x. abs c \<le> x \<and> (ismaxcoeff t 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

722 
"ismaxcoeff (CF c s t) = (\<lambda>x. abs c \<le> x \<and> (ismaxcoeff t 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

723 
"ismaxcoeff t = (\<lambda>x. 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

724 

324622260d29
Added 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 
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

726 
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

727 

324622260d29
Added 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 
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

729 
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

730 
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

731 
hence H:"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

732 
have thh: "maxcoeff t \<le> max (abs c) (maxcoeff t)" by (simp add: le_maxI2) 
324622260d29
Added 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 
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

734 
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

735 
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

736 
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

737 
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

738 
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

739 
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

740 

27556  741 
lemma zgcd_gt1: "zgcd i j > 1 \<Longrightarrow> ((abs i > 1 \<and> abs j > 1) \<or> (abs i = 0 \<and> abs j > 1) \<or> (abs i > 1 \<and> abs j = 0))" 
742 
apply (unfold zgcd_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

743 
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

744 
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

745 
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

746 
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

747 
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

748 
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

749 
lemma numgcdh0:"numgcdh t m = 0 \<Longrightarrow> m =0" 
27556  750 
by (induct t rule: numgcdh.induct, auto simp add:zgcd0) 
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

751 

324622260d29
Added 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 
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

753 
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

754 
shows "dvdnumcoeff t (numgcdh t m)" 
324622260d29
Added 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 
using prems 
324622260d29
Added 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 
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

757 
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

758 
let ?g = "numgcdh t m" 
27556  759 
from prems have th:"zgcd c ?g > 1" by simp 
760 
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

761 
have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?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

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

763 
have th: "dvdnumcoeff t ?g" by simp 
27567  764 
have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2) 
765 
from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)} 

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

766 
moreover {assume "abs c = 0 \<and> ?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

767 
with prems have th: "dvdnumcoeff t ?g" by simp 
27567  768 
have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2) 
769 
from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1) 

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

770 
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

771 
moreover {assume "abs c > 1" and g0:"?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

772 
from numgcdh0[OF g0] have "m=0". with prems have ?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

773 
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

774 
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

775 
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

776 
let ?g = "numgcdh t m" 
27556  777 
from prems have th:"zgcd c ?g > 1" by simp 
778 
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

779 
have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?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

780 
moreover {assume "abs c > 1" and gp: "?g > 1" with prems 
324622260d29
Added 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 
have th: "dvdnumcoeff t ?g" by simp 
27567  782 
have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2) 
783 
from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)} 

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

784 
moreover {assume "abs c = 0 \<and> ?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

785 
with prems have th: "dvdnumcoeff t ?g" by simp 
27567  786 
have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2) 
787 
from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1) 

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

788 
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

789 
moreover {assume "abs c > 1" and g0:"?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

790 
from numgcdh0[OF g0] have "m=0". with prems have ?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

791 
ultimately show ?case by blast 
27567  792 
qed(auto simp add: zgcd_zdvd1) 
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

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

795 
assumes "numgcd t > 1" shows "dvdnumcoeff t (numgcd t) \<and> 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

796 
using prems 
324622260d29
Added 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 
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

798 
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

799 
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

800 
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

801 
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

802 
assume H: "numgcdh t ?mc > 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

803 
from dvdnumcoeff_aux[OF th1 th2 H] show "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

804 
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

805 

324622260d29
Added 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 
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

807 
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

808 
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

809 
have "?g \<ge> 0" by (simp add: numgcd_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

810 
hence "?g = 0 \<or> ?g = 1 \<or> ?g > 1" 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

811 
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

812 
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

813 
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

814 
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

815 
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

816 
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

817 
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

818 
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

819 

324622260d29
Added 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 
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

821 
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

822 

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

823 
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

824 
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

825 

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

826 
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

827 
simpnum:: "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

828 
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

829 
nummul:: "num \<Rightarrow> int \<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

830 

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

831 
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

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

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

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

835 
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

836 
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

837 
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

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

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

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

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

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

843 
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

844 
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

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

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

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

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

849 

324622260d29
Added 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 
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

851 
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

852 
apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all) 
29667  853 
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

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

855 
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

856 
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

857 
apply (case_tac "c1+c2 = 0") 
29667  858 
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

859 

324622260d29
Added 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 
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

861 
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

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 
recdef nummul "measure size" 
324622260d29
Added 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 
"nummul (C j) = (\<lambda> i. C (i*j))" 
324622260d29
Added 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 
"nummul (CN n c t) = (\<lambda> i. CN n (c*i) (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

866 
"nummul (CF c t s) = (\<lambda> i. CF (c*i) t (nummul s 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

867 
"nummul (Mul c t) = (\<lambda> i. nummul t (i*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

868 
"nummul t = (\<lambda> i. Mul i 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

869 

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

870 
lemma nummul[simp]: "\<And> i. Inum bs (nummul t i) = Inum bs (Mul i t)" 
29667  871 
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

872 

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

873 
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

874 
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

875 

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

876 
constdefs numneg :: "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

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

878 

324622260d29
Added 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 
constdefs numsub :: "num \<Rightarrow> 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

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

881 

324622260d29
Added 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 
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

883 
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

884 

324622260d29
Added 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 
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

886 
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

887 

324622260d29
Added 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 
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

889 
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

890 

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

891 
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

892 
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

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

895 
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

896 
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

897 

324622260d29
Added 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 
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

899 
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

900 
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

901 
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

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 
consts split_int:: "num \<Rightarrow> num\<times>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

904 
recdef split_int "measure num_size" 
324622260d29
Added 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 
"split_int (C c) = (C 0, 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

906 
"split_int (CN n c 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

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

908 
in (CN n c bv, bi))" 
324622260d29
Added 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 
"split_int (CF c 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

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

911 
in (bv, CF c a bi))" 
324622260d29
Added 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 
"split_int a = (a,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

913 

324622260d29
Added 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 
lemma split_int:"\<And> tv ti. split_int t = (tv,ti) \<Longrightarrow> (Inum bs (Add tv ti) = Inum bs t) \<and> isint ti 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

915 
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

916 
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

917 
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

918 
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

919 
have "split_int b = (?bv,?bi)" 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 
with prems(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" 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

921 
from prems(2) have tibi: "ti = ?bi" by (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

922 
from prems(2) b[symmetric] bii show ?case by (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

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

925 
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

926 
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

927 
have "split_int b = (?bv,?bi)" 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

928 
with prems(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" 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

929 
from prems(2) have tibi: "ti = CF c a ?bi" by (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

930 
from prems(2) b[symmetric] bii show ?case by (auto simp add: Let_def split_def isint_Floor isint_add isint_Mul isint_CF) 
29667  931 
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

932 

324622260d29
Added 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 
lemma split_int_nb: "numbound0 t \<Longrightarrow> numbound0 (fst (split_int t)) \<and> numbound0 (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

934 
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

935 

23858  936 
definition 
937 
numfloor:: "num \<Rightarrow> num" 

938 
where 

939 
numfloor_def: "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

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

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

942 

324622260d29
Added 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 
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

944 
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

945 
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

946 
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

947 
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

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

949 
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

950 
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

951 
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

952 
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

953 
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

954 
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

955 
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

956 
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

957 
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

958 
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

959 
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

960 
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

961 
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

962 
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

963 
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

964 
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

965 
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

966 

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

967 
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

968 
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

969 
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

970 

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

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

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

973 
"simpnum (Bound n) = CN n 1 (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

974 
"simpnum (Neg t) = numneg (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

975 
"simpnum (Add t s) = numadd (simpnum t,simpnum 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

976 
"simpnum (Sub t s) = numsub (simpnum t) (simpnum 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

977 
"simpnum (Mul i t) = (if i = 0 then (C 0) else nummul (simpnum 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

978 
"simpnum (Floor t) = numfloor (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

979 
"simpnum (CN n c t) = (if c=0 then simpnum t else CN n c (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

980 
"simpnum (CF c t s) = simpnum(Add (Mul c (Floor 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

981 

324622260d29
Added 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 
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

983 
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

984 

324622260d29
Added 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 
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

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

987 
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

988 

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

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

990 
recdef nozerocoeff "measure size" 
324622260d29
Added 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 
"nozerocoeff (C c) = 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

992 
"nozerocoeff (CN n c t) = (c\<noteq>0 \<and> nozerocoeff 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

993 
"nozerocoeff (CF c s t) = (c \<noteq> 0 \<and> nozerocoeff 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

994 
"nozerocoeff (Mul c t) = (c\<noteq>0 \<and> nozerocoeff 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

995 
"nozerocoeff 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

996 

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

997 
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

998 
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

999 

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

1000 
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

1001 
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

1002 

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

1003 
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

1004 
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

1005 

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

1006 
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

1007 
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

1008 

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

1009 
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

1010 
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

1011 

324622260d29
Added 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 
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

1013 
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

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

1015 

324622260d29
Added 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 
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

1017 
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

1018 

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

1019 
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

1020 
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

1021 
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

1022 
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

1023 
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

1024 
with cnz have "max (abs c) (maxcoeff t) > 0" 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

1025 
with prems show ?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

1026 
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

1027 
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

1028 
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

1029 
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

1030 
with cnz have "max (abs c) (maxcoeff t) > 0" 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

1031 
with prems show ?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

1032 
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

1033 

324622260d29
Added 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 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

1035 
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

1036 
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

1037 
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

1038 
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

1039 
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

1040 

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

1041 
constdefs simp_num_pair:: "(num \<times> int) \<Rightarrow> num \<times> 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

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

1043 
(let t' = simpnum t ; g = numgcd t' in 
27556  1044 
if g > 1 then (let g' = zgcd 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

1045 
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

1046 
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

1047 
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

1048 

324622260d29
Added 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 
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

1050 
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

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

1052 
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

1053 
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

1054 
let ?g = "numgcd ?t'" 
27556  1055 
let ?g' = "zgcd 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

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

1057 
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

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

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

1060 
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

1061 
{assume g1:"?g>1" hence g0: "?g > 0" by simp 
27556  1062 
from zgcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp 
1063 
hence g'p: "?g' > 0" using zgcd_pos[where i="n" and j="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

1064 
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

1065 
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

1066 
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

1067 
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

1068 
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

1069 
let ?t = "Inum bs ?tt" 
27567  1070 
have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2) 
1071 
have gpdd: "?g' dvd n" by (simp add: zgcd_zdvd1) 

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

1072 
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

1073 
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

1074 
have th2:"real ?g' * ?t = Inum bs ?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

1075 
from prems have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_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

1076 
also have "\<dots> = (real ?g' * ?t) / (real ?g' * (real (n 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

1077 
also have "\<dots> = (Inum bs ?t' / real 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

1078 
using real_of_int_div[OF gp0 gpdd] th2 gp0 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

1079 
finally have "?lhs = Inum bs t / real 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

1080 
then have ?thesis using prems by (simp add: 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

1081 
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

1082 
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

1083 
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

1084 
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

1085 

324622260d29
Added 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 
lemma simp_num_pair_l: assumes tnb: "numbound0 t" and np: "n >0" and tn: "simp_num_pair (t,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

1087 
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

1088 
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

1089 
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

1090 
let ?g = "numgcd ?t'" 
27556  1091 
let ?g' = "zgcd 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

1092 
{assume nz: "n = 0" hence ?thesis using prems 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

1093 
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

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

1095 
{assume "\<not> ?g > 1" hence ?thesis using prems by (auto 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

1096 
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

1097 
{assume g1:"?g>1" hence g0: "?g > 0" by simp 
27556  1098 
from zgcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp 
1099 
hence g'p: "?g' > 0" using zgcd_pos[where i="n" and j="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

1100 
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

1101 
moreover {assume "?g'=1" hence ?thesis using prems 
324622260d29
Added 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 
by (auto 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

1103 
moreover {assume g'1:"?g'>1" 
27567  1104 
have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2) 
1105 
have gpdd: "?g' dvd n" by (simp add: zgcd_zdvd1) 

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

1106 
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

1107 
from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> 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

1108 
from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]] 
324622260d29
Added 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 
have "n div ?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

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

1111 
by(auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0)} 
324622260d29
Added 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 
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

1113 
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

1114 
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

1115 
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

1116 

324622260d29
Added 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 
consts not:: "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

1118 
recdef not "measure size" 
324622260d29
Added 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 
"not (NOT p) = 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

1120 
"not T = 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

1121 
"not F = 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

1122 
"not (Lt t) = Ge 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

1123 
"not (Le t) = Gt 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

1124 
"not (Gt t) = Le 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

1125 
"not (Ge t) = Lt 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

1126 
"not (Eq t) = NEq 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

1127 
"not (NEq t) = Eq 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

1128 
"not (Dvd i t) = NDvd i 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

1129 
"not (NDvd i t) = Dvd i 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

1130 
"not (And p q) = Or (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

1131 
"not (Or p q) = 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

1132 
"not p = 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

1133 
lemma not[simp]: "Ifm bs (not p) = Ifm bs (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

1134 
by (induct p) 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

1135 
lemma not_qf[simp]: "qfree p \<Longrightarrow> qfree (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

1136 
by (induct p, 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

1137 
lemma not_nb[simp]: "bound0 p \<Longrightarrow> bound0 (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

1138 
by (induct p, 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

1139 

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

1140 
constdefs conj :: "fm \<Rightarrow> 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

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

1142 
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

1143 
lemma conj[simp]: "Ifm bs (conj p q) = Ifm bs (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

1144 
by (cases "p=F \<or> q=F",simp_all add: conj_def) (cases 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

1145 

324622260d29
Added 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 
lemma conj_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (conj 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

1147 
using conj_def 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

1148 
lemma conj_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (conj 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

1149 
using conj_def 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

1150 

324622260d29
Added 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 
constdefs disj :: "fm \<Rightarrow> 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

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

1153 
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

1154 

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

1155 
lemma disj[simp]: "Ifm bs (disj p q) = Ifm bs (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

1156 
by (cases "p=T \<or> q=T",simp_all add: disj_def) (cases 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

1157 
lemma disj_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (disj 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

1158 
using disj_def 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

1159 
lemma disj_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (disj 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

1160 
using disj_def 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

1161 

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

1162 
constdefs imp :: "fm \<Rightarrow> 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

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

1164 
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

1165 
lemma imp[simp]: "Ifm bs (imp p q) = Ifm bs (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

1166 
by (cases "p=F \<or> q=T",simp_all add: imp_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

1167 
lemma imp_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (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

1168 
using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_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

1169 
lemma imp_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (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

1170 
using imp_def by (cases "p=F \<or> q=T \<or> p=q",simp_all add: imp_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

1171 

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

1172 
constdefs iff :: "fm \<Rightarrow> 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

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

1174 
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

1175 
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

1176 
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

1177 
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

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

1179 
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

1180 
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

1181 
lemma iff_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (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

1182 
using iff_def 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

1183 

324622260d29
Added 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 
consts check_int:: "num \<Rightarrow> bool" 
324622260d29
Added 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 
recdef check_int "measure size" 
324622260d29
Added 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 
"check_int (C i) = 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

1187 
"check_int (Floor 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

1188 
"check_int (Mul i t) = check_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

1189 
"check_int (Add t s) = (check_int t \<and> check_int 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

1190 
"check_int (Neg t) = check_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

1191 
"check_int (CF c t s) = check_int 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

1192 
"check_int t = 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

1193 
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

1194 
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

1195 

324622260d29
Added 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 
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

1197 
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

1198 

324622260d29
Added 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 
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

1200 
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

1201 
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

1202 
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

1203 
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

1204 
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

1205 
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

1206 
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

1207 
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

1208 
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

1209 
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

1210 
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

1211 
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

1212 
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

1213 
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

1214 
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

1215 
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

1216 
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

1217 
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

1218 

324622260d29
Added 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 
constdefs simpdvd:: "int \<Rightarrow> num \<Rightarrow> (int \<times> 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

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

1221 
(let g = numgcd t in 
27556  1222 
if g > 1 then (let g' = zgcd 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

1223 
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

1224 
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

1225 
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

1226 
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

1227 
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

1228 
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

1229 
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

1230 
let ?g = "numgcd t" 
27556  1231 
let ?g' = "zgcd 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

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

1233 
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

1234 
{assume g1:"?g>1" hence g0: "?g > 0" by simp 
27556  1235 
from zgcd0 g1 dnz have gp0: "?g' \<noteq> 0" by simp 
1236 
hence g'p: "?g' > 0" using zgcd_pos[where i="d" and j="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

1237 
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

1238 
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

1239 
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

1240 
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

1241 
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

1242 
let ?t = "Inum bs ?tt" 
27567  1243 
have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2) 
1244 
have gpdd: "?g' dvd d" by (simp add: zgcd_zdvd1) 

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

1245 
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

1246 
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

1247 
have th2:"real ?g' * ?t = Inum bs 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

1248 
from prems have "Ifm bs (Dvd (fst (simpdvd d t)) (snd(simpdvd d t))) = Ifm bs (Dvd (d div ?g') ?tt)" 
324622260d29
Added 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 
by (simp add: simpdvd_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

1250 
also have "\<dots> = (real d rdvd (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

1251 
using rdvd_reduce[OF gpdd gpdgp g'p, where t="?t", simplified zdiv_self[OF gp0]] 
324622260d29
Added 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 
th2[symmetric] 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

1253 
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

1254 
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

1255 
} 
324622260d29
Added 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 
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

1257 
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

1258 

324622260d29
Added 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 
consts simpfm :: "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

1260 
recdef simpfm "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

1261 
"simpfm (And p q) = conj (simpfm p) (simpfm 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

1262 
"simpfm (Or p q) = disj (simpfm p) (simpfm 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

1263 
"simpfm (Imp p q) = imp (simpfm p) (simpfm 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

1264 
"simpfm (Iff p q) = iff (simpfm p) (simpfm 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

1265 
"simpfm (NOT p) = not (simpfm 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

1266 
"simpfm (Lt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v < 0) then T else 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

1267 
 _ \<Rightarrow> Lt (reducecoeff 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

1268 
"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'))" 
324622260d29
Added 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 
"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'))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1270 
"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'))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1271 
"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'))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1272 
"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'))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1273 
"simpfm (Dvd i a) = (if i=0 then simpfm (Eq 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

1274 
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

1275 
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))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1276 
"simpfm (NDvd i a) = (if i=0 then simpfm (NEq 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

1277 
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

1278 
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))" 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1279 
"simpfm p = 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

1280 

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

1281 
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

1282 
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

1283 
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

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

1285 
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

1286 
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

1287 
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

1288 
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

1289 
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

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

1291 
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

1292 
hence gp: "real ?g > 0 