author  nipkow 
Fri, 05 Aug 2016 15:44:53 +0200  
changeset 63600  d0fa16751d14 
parent 62342  1cf129590be8 
child 64240  eabf80376aab 
permissions  rwrr 
30439  1 
(* Title: HOL/Decision_Procs/MIR.thy 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

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

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

4 

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

5 
theory MIR 
41849  6 
imports Complex_Main Dense_Linear_Order DP_Library 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50252
diff
changeset

7 
"~~/src/HOL/Library/Code_Target_Numeral" "~~/src/HOL/Library/Old_Recdef" 
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 

61586  10 
section \<open>Quantifier elimination for \<open>\<real> (0, 1, +, floor, <)\<close>\<close> 
27456  11 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

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

13 

51369  14 
lemma myle: 
15 
fixes a b :: "'a::{ordered_ab_group_add}" 

41849  16 
shows "(a \<le> b) = (0 \<le> b  a)" 
51369  17 
by (metis add_0_left add_le_cancel_right diff_add_cancel) 
18 

19 
lemma myless: 

20 
fixes a b :: "'a::{ordered_ab_group_add}" 

41849  21 
shows "(a < b) = (0 < b  a)" 
51369  22 
by (metis le_iff_diff_le_0 less_le_not_le myle) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

23 

324622260d29
Added 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 
(* Periodicity of dvd *) 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

25 
lemmas dvd_period = zdvd_period 
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

26 

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

27 
(* The Divisibility relation between reals *) 
51369  28 
definition rdvd:: "real \<Rightarrow> real \<Rightarrow> bool" (infixl "rdvd" 50) 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

29 
where "x rdvd y \<longleftrightarrow> (\<exists>k::int. y = x * real_of_int 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

30 

61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

31 
lemma int_rdvd_real: 
61942  32 
"real_of_int (i::int) rdvd x = (i dvd \<lfloor>x\<rfloor> \<and> real_of_int \<lfloor>x\<rfloor> = x)" (is "?l = ?r") 
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

33 
proof 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

34 
assume "?l" 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

35 
hence th: "\<exists> k. x=real_of_int (i*k)" by (simp add: rdvd_def) 
61942  36 
hence th': "real_of_int \<lfloor>x\<rfloor> = x" by (auto simp del: of_int_mult) 
37 
with th have "\<exists> k. real_of_int \<lfloor>x\<rfloor> = real_of_int (i*k)" by simp 

38 
hence "\<exists>k. \<lfloor>x\<rfloor> = i*k" by presburger 

39 
thus ?r using th' by (simp add: dvd_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

40 
next 
61076  41 
assume "?r" hence "(i::int) dvd \<lfloor>x::real\<rfloor>" .. 
61942  42 
hence "\<exists>k. real_of_int \<lfloor>x\<rfloor> = real_of_int (i*k)" 
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61610
diff
changeset

43 
by (metis (no_types) dvd_def) 
60533  44 
thus ?l using \<open>?r\<close> by (simp add: rdvd_def) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

45 
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

46 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

47 
lemma int_rdvd_iff: "(real_of_int (i::int) rdvd real_of_int t) = (i dvd t)" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

48 
by (auto simp add: rdvd_def dvd_def) (rule_tac x="k" in exI, simp only: of_int_mult[symmetric]) 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

49 

77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

50 

61945  51 
lemma rdvd_abs1: "(\<bar>real_of_int d\<bar> rdvd t) = (real_of_int (d ::int) rdvd 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

52 
proof 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

53 
assume d: "real_of_int d rdvd t" 
61942  54 
from d int_rdvd_real have d2: "d dvd \<lfloor>t\<rfloor>" and ti: "real_of_int \<lfloor>t\<rfloor> = t" 
51369  55 
by auto 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

56 

61945  57 
from iffD2[OF abs_dvd_iff] d2 have "\<bar>d\<bar> dvd \<lfloor>t\<rfloor>" by blast 
58 
with ti int_rdvd_real[symmetric] have "real_of_int \<bar>d\<bar> rdvd t" by blast 

59 
thus "\<bar>real_of_int d\<bar> rdvd 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

60 
next 
61945  61 
assume "\<bar>real_of_int d\<bar> rdvd t" hence "real_of_int \<bar>d\<bar> rdvd t" by simp 
62 
with int_rdvd_real[where i="\<bar>d\<bar>" and x="t"] 

63 
have d2: "\<bar>d\<bar> dvd \<lfloor>t\<rfloor>" and ti: "real_of_int \<lfloor>t\<rfloor> = t" 

51369  64 
by auto 
61942  65 
from iffD1[OF abs_dvd_iff] d2 have "d dvd \<lfloor>t\<rfloor>" by blast 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

66 
with ti int_rdvd_real[symmetric] show "real_of_int d rdvd 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

67 
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

68 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

69 
lemma rdvd_minus: "(real_of_int (d::int) rdvd t) = (real_of_int d rdvd 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

70 
apply (auto simp add: rdvd_def) 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

71 
apply (rule_tac x="k" in exI, 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

72 
apply (rule_tac x="k" in exI, simp) 
51369  73 
done 
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

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 rdvd_left_0_eq: "(0 rdvd t) = (t=0)" 
51369  76 
by (auto simp add: rdvd_def) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

77 

61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

78 
lemma rdvd_mult: 
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

79 
assumes knz: "k\<noteq>0" 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

80 
shows "(real_of_int (n::int) * real_of_int (k::int) rdvd x * real_of_int k) = (real_of_int n rdvd x)" 
51369  81 
using knz by (simp add: rdvd_def) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

82 

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

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

86 

61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

87 
datatype num = C int  Bound nat  CN nat int num  Neg num  Add num num Sub num num 
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

88 
 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

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

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

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

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

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

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

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

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

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

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

101 

324622260d29
Added 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 
(* Semantics of numeral terms (num) *) 
25765  103 
primrec Inum :: "real list \<Rightarrow> num \<Rightarrow> real" where 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

104 
"Inum bs (C c) = (real_of_int c)" 
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

105 
 "Inum bs (Bound n) = bs!n" 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

106 
 "Inum bs (CN n c a) = (real_of_int c) * (bs!n) + (Inum bs 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

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

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

109 
 "Inum bs (Sub a b) = Inum bs a  Inum bs b" 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

110 
 "Inum bs (Mul c a) = (real_of_int c) * Inum bs a" 
61942  111 
 "Inum bs (Floor a) = real_of_int \<lfloor>Inum bs a\<rfloor>" 
112 
 "Inum bs (CF c a b) = real_of_int c * real_of_int \<lfloor>Inum bs a\<rfloor> + Inum bs b" 

113 
definition "isint t bs \<equiv> real_of_int \<lfloor>Inum bs t\<rfloor> = Inum bs t" 

114 

115 
lemma isint_iff: "isint n bs = (real_of_int \<lfloor>Inum bs n\<rfloor> = Inum bs n)" 

51369  116 
by (simp add: isint_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

117 

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

119 
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

120 

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

122 
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

123 
let ?e = "Inum bs e" 
61942  124 
assume be: "isint e bs" hence efe:"real_of_int \<lfloor>?e\<rfloor> = ?e" by (simp add: isint_iff) 
125 
have "real_of_int \<lfloor>Inum bs (Mul c e)\<rfloor> = real_of_int \<lfloor>real_of_int (c * \<lfloor>?e\<rfloor>)\<rfloor>" 

126 
using efe by simp 

127 
also have "\<dots> = real_of_int (c* \<lfloor>?e\<rfloor>)" by (metis floor_of_int) 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

128 
also have "\<dots> = real_of_int c * ?e" using efe 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

129 
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

130 
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

131 

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

133 
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

134 
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

135 
assume ie: "isint e bs" 
61942  136 
hence th: "real_of_int \<lfloor>?I e\<rfloor> = ?I e" by (simp add: isint_def) 
137 
have "real_of_int \<lfloor>?I (Neg e)\<rfloor> = real_of_int \<lfloor> (real_of_int \<lfloor>?I e\<rfloor>)\<rfloor>" 

138 
by (simp add: th) 

139 
also have "\<dots> =  real_of_int \<lfloor>?I e\<rfloor>" 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

140 
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

141 
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

142 

61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

143 
lemma isint_sub: 
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

144 
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

145 
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

146 
let ?I = "\<lambda> t. Inum bs t" 
61942  147 
from ie have th: "real_of_int \<lfloor>?I e\<rfloor> = ?I e" by (simp add: isint_def) 
148 
have "real_of_int \<lfloor>?I (Sub (C c) e)\<rfloor> = real_of_int \<lfloor>real_of_int (c  \<lfloor>?I e\<rfloor>)\<rfloor>" 

149 
by (simp add: th) 

150 
also have "\<dots> = real_of_int (c  \<lfloor>?I e\<rfloor>)" 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

151 
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

152 
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

153 

51369  154 
lemma isint_add: 
155 
assumes ai: "isint a bs" and bi: "isint b bs" 

156 
shows "isint (Add a b) bs" 

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

157 
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

158 
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

159 
let ?b = "Inum bs b" 
61942  160 
from ai bi isint_iff have "real_of_int \<lfloor>?a + ?b\<rfloor> = real_of_int \<lfloor>real_of_int \<lfloor>?a\<rfloor> + real_of_int \<lfloor>?b\<rfloor>\<rfloor>" 
51369  161 
by simp 
61942  162 
also have "\<dots> = real_of_int \<lfloor>?a\<rfloor> + real_of_int \<lfloor>?b\<rfloor>" 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

163 
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

164 
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

165 
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

166 

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

168 
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

169 

324622260d29
Added 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 
(* FORMULAE *) 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

172 
datatype fm = 
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

173 
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

174 
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

175 

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

176 

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

178 
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

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

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

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

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

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

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

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

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

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

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

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

190 
lemma fmsize_pos: "fmsize p > 0" 
51369  191 
by (induct p rule: fmsize.induct) simp_all 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

192 

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

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

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

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

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

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

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

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

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

202 
 "Ifm bs (NEq a) = (Inum bs a \<noteq> 0)" 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

203 
 "Ifm bs (Dvd i b) = (real_of_int i rdvd Inum bs b)" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

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

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

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

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

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

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

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

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

212 

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

214 
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

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

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

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

218 
"prep (E (Imp p q)) = Or (prep (E (NOT p))) (prep (E q))" 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

219 
"prep (E (Iff p q)) = Or (prep (E (And p q))) (prep (E (And (NOT p) (NOT 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

237 
"prep p = p" 
25162  238 
(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

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

241 

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

324622260d29
Added 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 
(* Quantifier freeness *) 
25765  244 
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

245 
"qfree (E p) = False" 
25765  246 
 "qfree (A p) = False" 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

247 
 "qfree (NOT p) = qfree p" 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

248 
 "qfree (And p q) = (qfree p \<and> qfree q)" 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

249 
 "qfree (Or p q) = (qfree p \<and> qfree q)" 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

250 
 "qfree (Imp p q) = (qfree p \<and> qfree q)" 
25765  251 
 "qfree (Iff p q) = (qfree p \<and> qfree q)" 
252 
 "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

253 

324622260d29
Added 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 
(* Boundedness and substitution *) 
25765  255 
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

256 
"numbound0 (C c) = True" 
25765  257 
 "numbound0 (Bound n) = (n>0)" 
258 
 "numbound0 (CN n i a) = (n > 0 \<and> numbound0 a)" 

259 
 "numbound0 (Neg a) = numbound0 a" 

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

61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

261 
 "numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)" 
25765  262 
 "numbound0 (Mul i a) = numbound0 a" 
263 
 "numbound0 (Floor a) = numbound0 a" 

61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

264 
 "numbound0 (CF c a b) = (numbound0 a \<and> numbound0 b)" 
25765  265 

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

266 
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

267 
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

268 
shows "Inum (b#bs) a = Inum (b'#bs) a" 
41849  269 
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

270 

61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

271 
lemma numbound0_gen: 
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 
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

273 
shows "\<forall> y. isint t (y#bs)" 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

274 
using nb ti 
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

275 
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

276 
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

277 
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

278 
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

279 
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

280 
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

281 

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

283 
"bound0 T = True" 
25765  284 
 "bound0 F = True" 
285 
 "bound0 (Lt a) = numbound0 a" 

286 
 "bound0 (Le a) = numbound0 a" 

287 
 "bound0 (Gt a) = numbound0 a" 

288 
 "bound0 (Ge a) = numbound0 a" 

289 
 "bound0 (Eq a) = numbound0 a" 

290 
 "bound0 (NEq a) = numbound0 a" 

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

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

293 
 "bound0 (NOT p) = bound0 p" 

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

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

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

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

298 
 "bound0 (E p) = False" 

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

300 

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

302 
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

303 
shows "Ifm (b#bs) p = Ifm (b'#bs) p" 
51369  304 
using bp numbound0_I [where b="b" and bs="bs" and b'="b'"] 
41849  305 
by (induct p) auto 
25765  306 

307 
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

308 
"numsubst0 t (C c) = (C c)" 
25765  309 
 "numsubst0 t (Bound n) = (if n=0 then t else Bound n)" 
310 
 "numsubst0 t (CN n i a) = (if n=0 then Add (Mul i t) (numsubst0 t a) else CN n i (numsubst0 t a))" 

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

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

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

61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

314 
 "numsubst0 t (Sub a b) = Sub (numsubst0 t a) (numsubst0 t b)" 
25765  315 
 "numsubst0 t (Mul i a) = Mul i (numsubst0 t a)" 
316 
 "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

317 

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

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

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

321 

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

323 
"subst0 t T = T" 
25765  324 
 "subst0 t F = F" 
325 
 "subst0 t (Lt a) = Lt (numsubst0 t a)" 

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

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

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

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

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

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

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

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

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

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

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

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

338 

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

339 
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

340 
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

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

343 

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

345 
"decrnum (Bound n) = Bound (n  1)" 
41839  346 
 "decrnum (Neg a) = Neg (decrnum a)" 
347 
 "decrnum (Add a b) = Add (decrnum a) (decrnum b)" 

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

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

350 
 "decrnum (Floor a) = Floor (decrnum a)" 

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

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

353 
 "decrnum a = a" 

354 

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

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

356 
"decr (Lt a) = Lt (decrnum a)" 
41839  357 
 "decr (Le a) = Le (decrnum a)" 
358 
 "decr (Gt a) = Gt (decrnum a)" 

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

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

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

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

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

61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

364 
 "decr (NOT p) = NOT (decr p)" 
41839  365 
 "decr (And p q) = And (decr p) (decr q)" 
366 
 "decr (Or p q) = Or (decr p) (decr q)" 

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

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

369 
 "decr p = p" 

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

370 

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

371 
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

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

374 

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

375 
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

376 
shows "Ifm (x#bs) p = Ifm bs (decr p)" 
51369  377 
using nb by (induct p rule: decr.induct) (simp_all add: decrnum) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

378 

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

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

381 

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

383 
"isatom T = True" 
41839  384 
 "isatom F = True" 
385 
 "isatom (Lt a) = True" 

386 
 "isatom (Le a) = True" 

387 
 "isatom (Gt a) = True" 

388 
 "isatom (Ge a) = True" 

389 
 "isatom (Eq a) = True" 

390 
 "isatom (NEq a) = True" 

391 
 "isatom (Dvd i b) = True" 

392 
 "isatom (NDvd i b) = True" 

393 
 "isatom p = False" 

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

394 

51369  395 
lemma numsubst0_numbound0: 
396 
assumes nb: "numbound0 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

397 
shows "numbound0 (numsubst0 t a)" 
51369  398 
using nb by (induct a) auto 
399 

400 
lemma subst0_bound0: 

401 
assumes qf: "qfree p" and nb: "numbound0 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

402 
shows "bound0 (subst0 t p)" 
51369  403 
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

404 

324622260d29
Added 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 
lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p" 
51369  406 
by (induct p) simp_all 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

407 

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

408 

25765  409 
definition djf:: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm" where 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

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

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

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

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

415 

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

416 
lemma djf_Or: "Ifm bs (djf f p q) = Ifm bs (Or (f p) q)" 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

417 
by (cases "q=T", simp add: djf_def,cases "q=F",simp add: djf_def) 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

418 
(cases "f p", simp_all add: Let_def djf_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

419 

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

420 
lemma evaldjf_ex: "Ifm bs (evaldjf f ps) = (\<exists> p \<in> set ps. Ifm bs (f p))" 
51369  421 
by (induct ps) (simp_all add: evaldjf_def djf_Or) 
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

422 

61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

423 
lemma evaldjf_bound0: 
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 
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

425 
shows "bound0 (evaldjf f xs)" 
51369  426 
using nb 
427 
apply (induct xs) 

428 
apply (auto simp add: evaldjf_def djf_def Let_def) 

429 
apply (case_tac "f a") 

430 
apply auto 

431 
done 

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

432 

61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

433 
lemma evaldjf_qf: 
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

434 
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

435 
shows "qfree (evaldjf f xs)" 
51369  436 
using nb 
437 
apply (induct xs) 

438 
apply (auto simp add: evaldjf_def djf_def Let_def) 

439 
apply (case_tac "f a") 

440 
apply auto 

441 
done 

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

442 

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

444 
"disjuncts (Or p q) = (disjuncts p) @ (disjuncts q)" 
41839  445 
 "disjuncts F = []" 
446 
 "disjuncts p = [p]" 

447 

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

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

449 
"conjuncts (And p q) = (conjuncts p) @ (conjuncts q)" 
41839  450 
 "conjuncts T = []" 
451 
 "conjuncts p = [p]" 

452 

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

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

455 

324622260d29
Added 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 
lemma disjuncts_qf: "qfree p \<Longrightarrow> \<forall> q\<in> set (disjuncts p). qfree q" 
51369  457 
proof  
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

458 
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

459 
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

460 
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

461 
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

462 
qed 
51369  463 

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

464 
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

465 
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

466 
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

467 
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

468 
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

469 
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

470 
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

471 

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

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

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

474 

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

476 
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

477 
shows "Ifm bs (DJ f p) = Ifm bs (f p)" 
51369  478 
proof  
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

479 
have "Ifm bs (DJ f p) = (\<exists> q \<in> set (disjuncts p). Ifm bs (f q))" 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

480 
by (simp add: DJ_def evaldjf_ex) 
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

481 
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

482 
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

483 
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

484 

61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

485 
lemma DJ_qf: assumes 
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

486 
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

487 
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

488 
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

489 
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

490 
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

491 
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

492 
with fqf have th':"\<forall> q\<in> set (disjuncts p). qfree (f q)" by blast 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

493 

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

494 
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

495 
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

496 

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

498 
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

499 
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

500 
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

501 
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

502 
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

503 
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

504 
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

505 
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

506 
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

507 
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

508 
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

509 
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

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

511 

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

514 
"bnds (Bound n) = [n]" 
41839  515 
 "bnds (CN n c a) = n#(bnds a)" 
516 
 "bnds (Neg a) = bnds a" 

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

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

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

520 
 "bnds (Floor a) = bnds a" 

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

522 
 "bnds a = []" 

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

524 
"lex_ns [] ms = True" 

525 
 "lex_ns ns [] = False" 

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

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

527 
definition lex_bnd :: "num \<Rightarrow> num \<Rightarrow> bool" where 
41839  528 
"lex_bnd t s \<equiv> lex_ns (bnds t) (bnds s)" 
529 

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

61945  531 
"maxcoeff (C i) = \<bar>i\<bar>" 
532 
 "maxcoeff (CN n c t) = max \<bar>c\<bar> (maxcoeff t)" 

533 
 "maxcoeff (CF c t s) = max \<bar>c\<bar> (maxcoeff s)" 

41839  534 
 "maxcoeff t = 1" 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

535 

324622260d29
Added 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 maxcoeff_pos: "maxcoeff t \<ge> 0" 
51369  537 
by (induct t rule: maxcoeff.induct) auto 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

538 

41839  539 
fun numgcdh:: "num \<Rightarrow> int \<Rightarrow> int" where 
31706  540 
"numgcdh (C i) = (\<lambda>g. gcd i g)" 
41839  541 
 "numgcdh (CN n c t) = (\<lambda>g. gcd c (numgcdh t g))" 
542 
 "numgcdh (CF c s t) = (\<lambda>g. gcd c (numgcdh t g))" 

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

23858  544 

51369  545 
definition numgcd :: "num \<Rightarrow> int" 
546 
where "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

547 

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

549 
"reducecoeffh (C i) = (\<lambda> g. C (i div g))" 
41839  550 
 "reducecoeffh (CN n c t) = (\<lambda> g. CN n (c div g) (reducecoeffh t g))" 
551 
 "reducecoeffh (CF c s t) = (\<lambda> g. CF (c div g) s (reducecoeffh t g))" 

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

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

553 

51369  554 
definition reducecoeff :: "num \<Rightarrow> num" 
23858  555 
where 
51369  556 
"reducecoeff t = 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

557 
(let g = numgcd t in 
51369  558 
if g = 0 then C 0 else if g=1 then t else reducecoeffh 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

559 

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

561 
"dvdnumcoeff (C i) = (\<lambda> g. g dvd i)" 
41839  562 
 "dvdnumcoeff (CN n c t) = (\<lambda> g. g dvd c \<and> (dvdnumcoeff t g))" 
563 
 "dvdnumcoeff (CF c s t) = (\<lambda> g. g dvd c \<and> (dvdnumcoeff t g))" 

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

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

565 

61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

566 
lemma dvdnumcoeff_trans: 
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

567 
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

568 
shows "dvdnumcoeff t g" 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

569 
using dgt' gdg 
51369  570 
by (induct t rule: dvdnumcoeff.induct) (simp_all add: gdg dvd_trans[OF gdg]) 
30042  571 

572 
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

573 

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

575 
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

576 
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

577 
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

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

580 
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

581 
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

582 

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

583 
lemma numgcdh_pos: assumes gp: "g \<ge> 0" shows "numgcdh t g \<ge> 0" 
51369  584 
using gp by (induct t rule: numgcdh.induct) auto 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

585 

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

587 
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

588 

324622260d29
Added 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 
lemma reducecoeffh: 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

590 
assumes gt: "dvdnumcoeff t g" and gp: "g > 0" 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

591 
shows "real_of_int g *(Inum bs (reducecoeffh t g)) = Inum bs 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

592 
using gt 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

593 
proof(induct t rule: reducecoeffh.induct) 
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

594 
case (1 i) hence gd: "g dvd i" by simp 
46670  595 
from assms 1 show ?case by (simp add: real_of_int_div[OF gd]) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

596 
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

597 
case (2 n c t) hence gd: "g dvd c" by simp 
46670  598 
from assms 2 show ?case by (simp add: real_of_int_div[OF 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

599 
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

600 
case (3 c s t) hence gd: "g dvd c" by simp 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

601 
from assms 3 show ?case by (simp add: real_of_int_div[OF 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

602 
qed (auto simp add: numgcd_def gp) 
41807  603 

41839  604 
fun ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool" where 
61945  605 
"ismaxcoeff (C i) = (\<lambda> x. \<bar>i\<bar> \<le> x)" 
606 
 "ismaxcoeff (CN n c t) = (\<lambda>x. \<bar>c\<bar> \<le> x \<and> (ismaxcoeff t x))" 

607 
 "ismaxcoeff (CF c s t) = (\<lambda>x. \<bar>c\<bar> \<le> x \<and> (ismaxcoeff t x))" 

41839  608 
 "ismaxcoeff t = (\<lambda>x. True)" 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

609 

324622260d29
Added 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 
lemma ismaxcoeff_mono: "ismaxcoeff t c \<Longrightarrow> c \<le> c' \<Longrightarrow> ismaxcoeff t c'" 
51369  611 
by (induct t rule: ismaxcoeff.induct) auto 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

612 

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

614 
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

615 
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

616 
hence H:"ismaxcoeff t (maxcoeff t)" . 
61945  617 
have thh: "maxcoeff t \<le> max \<bar>c\<bar> (maxcoeff t)" by simp 
51369  618 
from ismaxcoeff_mono[OF H thh] show ?case by simp 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

619 
next 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

620 
case (3 c t s) 
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

621 
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

622 
have thh1: "maxcoeff s \<le> max \<bar>c\<bar> (maxcoeff s)" by (simp add: max_def) 
51369  623 
from ismaxcoeff_mono[OF H1 thh1] show ?case by simp 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

624 
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

625 

61945  626 
lemma zgcd_gt1: "gcd i j > (1::int) \<Longrightarrow> ((\<bar>i\<bar> > 1 \<and> \<bar>j\<bar> > 1) \<or> (\<bar>i\<bar> = 0 \<and> \<bar>j\<bar> > 1) \<or> (\<bar>i\<bar> > 1 \<and> \<bar>j\<bar> = 0))" 
31706  627 
apply (unfold gcd_int_def) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

628 
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

629 
apply (cases "j = 0", simp_all) 
61945  630 
apply (cases "\<bar>i\<bar> = 1", simp_all) 
631 
apply (cases "\<bar>j\<bar> = 1", simp_all) 

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

632 
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

633 
done 
51369  634 

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

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

637 

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

639 
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

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

642 
proof(induct t rule: numgcdh.induct) 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

643 
case (2 n c 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

644 
let ?g = "numgcdh t m" 
41807  645 
from 2 have th:"gcd c ?g > 1" by simp 
27556  646 
from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"] 
61945  647 
have "(\<bar>c\<bar> > 1 \<and> ?g > 1) \<or> (\<bar>c\<bar> = 0 \<and> ?g > 1) \<or> (\<bar>c\<bar> > 1 \<and> ?g = 0)" by simp 
648 
moreover {assume "\<bar>c\<bar> > 1" and gp: "?g > 1" with 2 

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

649 
have th: "dvdnumcoeff t ?g" by simp 
31706  650 
have th': "gcd c ?g dvd ?g" by simp 
651 
from dvdnumcoeff_trans[OF th' th] have ?case by simp } 

61945  652 
moreover {assume "\<bar>c\<bar> = 0 \<and> ?g > 1" 
41807  653 
with 2 have th: "dvdnumcoeff t ?g" by simp 
31706  654 
have th': "gcd c ?g dvd ?g" by simp 
655 
from dvdnumcoeff_trans[OF th' th] have ?case by simp 

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

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

659 
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

660 
next 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

661 
case (3 c s 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

662 
let ?g = "numgcdh t m" 
41807  663 
from 3 have th:"gcd c ?g > 1" by simp 
27556  664 
from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"] 
61945  665 
have "(\<bar>c\<bar> > 1 \<and> ?g > 1) \<or> (\<bar>c\<bar> = 0 \<and> ?g > 1) \<or> (\<bar>c\<bar> > 1 \<and> ?g = 0)" by simp 
666 
moreover {assume "\<bar>c\<bar> > 1" and gp: "?g > 1" with 3 

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

667 
have th: "dvdnumcoeff t ?g" by simp 
31706  668 
have th': "gcd c ?g dvd ?g" by simp 
669 
from dvdnumcoeff_trans[OF th' th] have ?case by simp } 

61945  670 
moreover {assume "\<bar>c\<bar> = 0 \<and> ?g > 1" 
41807  671 
with 3 have th: "dvdnumcoeff t ?g" by simp 
31706  672 
have th': "gcd c ?g dvd ?g" by simp 
673 
from dvdnumcoeff_trans[OF th' th] have ?case by simp 

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

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

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

679 

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

680 
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

681 
assumes "numgcd t > 1" shows "dvdnumcoeff t (numgcd t) \<and> numgcd t > 0" 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

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

683 
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

684 
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

685 
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

686 
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

687 
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

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

690 
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

691 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

692 
lemma reducecoeff: "real_of_int (numgcd t) * (Inum bs (reducecoeff t)) = Inum bs 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

693 
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

694 
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

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

696 
hence "?g = 0 \<or> ?g = 1 \<or> ?g > 1" by auto 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

697 
moreover {assume "?g = 0" hence ?thesis by (simp add: numgcd0)} 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

698 
moreover {assume "?g = 1" hence ?thesis by (simp add: reducecoeff_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

699 
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

700 
from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff t ?g" and g0: "?g > 0" by blast+ 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

701 
from reducecoeffh[OF th1 g0, where bs="bs"] g1 have ?thesis 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

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

703 
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

704 
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

705 

324622260d29
Added 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 
lemma reducecoeffh_numbound0: "numbound0 t \<Longrightarrow> numbound0 (reducecoeffh t g)" 
51369  707 
by (induct t rule: reducecoeffh.induct) auto 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

708 

324622260d29
Added 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 
lemma reducecoeff_numbound0: "numbound0 t \<Longrightarrow> numbound0 (reducecoeff t)" 
51369  710 
using reducecoeffh_numbound0 by (simp add: reducecoeff_def Let_def) 
711 

712 
consts numadd:: "num \<times> num \<Rightarrow> num" 

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

714 
"numadd (CN n1 c1 r1,CN n2 c2 r2) = 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

715 
(if n1=n2 then 
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

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

717 
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

718 
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

719 
else (CN n2 c2 (numadd (CN n1 c1 r1,r2))))" 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

720 
"numadd (CN n1 c1 r1,t) = CN n1 c1 (numadd (r1, t))" 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

721 
"numadd (t,CN n2 c2 r2) = CN n2 c2 (numadd (t,r2))" 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

722 
"numadd (CF c1 t1 r1,CF c2 t2 r2) = 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

723 
(if t1 = t2 then 
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

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

725 
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

726 
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

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

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

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

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

731 

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

733 
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

734 
apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all) 
29667  735 
apply (case_tac "n1 = n2", simp_all add: algebra_simps) 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
49069
diff
changeset

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

737 
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

738 
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

739 
apply (case_tac "c1+c2 = 0") 
51369  740 
apply (case_tac "t1 = t2") 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

741 
apply (simp_all add: algebra_simps distrib_right[symmetric] of_int_mult[symmetric] of_int_add[symmetric]del: of_int_mult of_int_add distrib_right) 
51369  742 
done 
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 

324622260d29
Added 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 
lemma numadd_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))" 
51369  745 
by (induct t s rule: numadd.induct) (auto simp add: Let_def) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

746 

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

748 
"nummul (C j) = (\<lambda> i. C (i*j))" 
41839  749 
 "nummul (CN n c t) = (\<lambda> i. CN n (c*i) (nummul t i))" 
750 
 "nummul (CF c t s) = (\<lambda> i. CF (c*i) t (nummul s i))" 

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

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

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

753 

324622260d29
Added 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 
lemma nummul[simp]: "\<And> i. Inum bs (nummul t i) = Inum bs (Mul i t)" 
51369  755 
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

756 

324622260d29
Added 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 
lemma nummul_nb[simp]: "\<And> i. numbound0 t \<Longrightarrow> numbound0 (nummul t i)" 
51369  758 
by (induct t rule: nummul.induct) auto 
759 

760 
definition numneg :: "num \<Rightarrow> num" 

761 
where "numneg t \<equiv> nummul t ( 1)" 

762 

763 
definition numsub :: "num \<Rightarrow> num \<Rightarrow> num" 

764 
where "numsub s t \<equiv> (if s = t then C 0 else numadd (s,numneg t))" 

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

765 

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

766 
lemma numneg[simp]: "Inum bs (numneg t) = Inum bs (Neg t)" 
51369  767 
using numneg_def nummul 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

768 

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

769 
lemma numneg_nb[simp]: "numbound0 t \<Longrightarrow> numbound0 (numneg t)" 
51369  770 
using numneg_def 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

771 

324622260d29
Added 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 
lemma numsub[simp]: "Inum bs (numsub a b) = Inum bs (Sub a b)" 
51369  773 
using numsub_def 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

774 

324622260d29
Added 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 
lemma numsub_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numsub t s)" 
51369  776 
using numsub_def 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

777 

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

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

779 
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

780 
have cti: "isint (Mul c (Floor t)) bs" by (simp add: isint_Mul isint_Floor) 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

781 

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

782 
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

783 
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

784 
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

785 
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

786 

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

788 
"split_int (C c) = (C 0, C c)" 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

789 
 "split_int (CN n c b) = 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

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

791 
in (CN n c bv, bi))" 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

792 
 "split_int (CF c a b) = 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

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

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

796 

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

798 
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

799 
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

800 
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

801 
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

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

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

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

806 
next 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

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

808 
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

809 
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

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

813 
by (simp add: Let_def split_def) 

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

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

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

817 

324622260d29
Added 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 
lemma split_int_nb: "numbound0 t \<Longrightarrow> numbound0 (fst (split_int t)) \<and> numbound0 (snd (split_int t)) " 
41807  819 
by (induct t rule: split_int.induct) (auto simp add: Let_def split_def) 
820 

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

23858  822 
where 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

823 
"numfloor t = (let (tv,ti) = split_int t in 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

824 
(case tv of C i \<Rightarrow> numadd (tv,ti) 
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

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

826 

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

828 
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

829 
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

830 
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

831 
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

832 
{assume H: "\<forall> v. ?tv \<noteq> C v" 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

833 
hence th1: "?n t = ?N (Add (Floor ?tv) ?ti)" 
51369  834 
by (cases ?tv) (auto simp add: numfloor_def Let_def split_def) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

835 
from split_int[OF tvti] have "?N (Floor t) = ?N (Floor(Add ?tv ?ti))" and tii:"isint ?ti bs" by simp+ 
61942  836 
hence "?N (Floor t) = real_of_int \<lfloor>?N (Add ?tv ?ti)\<rfloor>" by simp 
837 
also have "\<dots> = real_of_int (\<lfloor>?N ?tv\<rfloor> + \<lfloor>?N ?ti\<rfloor>)" 

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

838 
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

839 
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

840 
finally have ?thesis using th1 by simp} 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

841 
moreover {fix v assume H:"?tv = C v" 
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

842 
from split_int[OF tvti] have "?N (Floor t) = ?N (Floor(Add ?tv ?ti))" and tii:"isint ?ti bs" by simp+ 
61942  843 
hence "?N (Floor t) = real_of_int \<lfloor>?N (Add ?tv ?ti)\<rfloor>" by simp 
844 
also have "\<dots> = real_of_int (\<lfloor>?N ?tv\<rfloor> + \<lfloor>?N ?ti\<rfloor>)" 

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

845 
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

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

848 
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

849 
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

850 

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

852 
using split_int_nb[where t="t"] 
51369  853 
by (cases "fst (split_int t)") (auto simp add: numfloor_def Let_def split_def) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

854 

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

856 
"simpnum (C j) = C j" 
41839  857 
 "simpnum (Bound n) = CN n 1 (C 0)" 
858 
 "simpnum (Neg t) = numneg (simpnum t)" 

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

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

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

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

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

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

865 
by pat_completeness auto 

866 
termination by (relation "measure num_size") auto 

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

867 

324622260d29
Added 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 
lemma simpnum_ci[simp]: "Inum bs (simpnum t) = Inum bs t" 
51369  869 
by (induct t rule: simpnum.induct) auto 
870 

871 
lemma simpnum_numbound0[simp]: "numbound0 t \<Longrightarrow> numbound0 (simpnum t)" 

872 
by (induct t rule: simpnum.induct) auto 

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

873 

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

875 
"nozerocoeff (C c) = True" 
41839  876 
 "nozerocoeff (CN n c t) = (c\<noteq>0 \<and> nozerocoeff t)" 
877 
 "nozerocoeff (CF c s t) = (c \<noteq> 0 \<and> nozerocoeff t)" 

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

879 
 "nozerocoeff t = True" 

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

880 

324622260d29
Added 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 
lemma numadd_nz : "nozerocoeff a \<Longrightarrow> nozerocoeff b \<Longrightarrow> nozerocoeff (numadd (a,b))" 
51369  882 
by (induct a b rule: numadd.induct) (auto simp add: Let_def) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

883 

324622260d29
Added 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 
lemma nummul_nz : "\<And> i. i\<noteq>0 \<Longrightarrow> nozerocoeff a \<Longrightarrow> nozerocoeff (nummul a i)" 
51369  885 
by (induct a rule: nummul.induct) (auto simp add: Let_def numadd_nz) 
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

886 

324622260d29
Added 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 
lemma numneg_nz : "nozerocoeff a \<Longrightarrow> nozerocoeff (numneg a)" 
51369  888 
by (simp add: numneg_def nummul_nz) 
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

889 

324622260d29
Added 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 
lemma numsub_nz: "nozerocoeff a \<Longrightarrow> nozerocoeff b \<Longrightarrow> nozerocoeff (numsub a b)" 
51369  891 
by (simp add: numsub_def numneg_nz numadd_nz) 
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

892 

324622260d29
Added 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 
lemma split_int_nz: "nozerocoeff t \<Longrightarrow> nozerocoeff (fst (split_int t)) \<and> nozerocoeff (snd (split_int t))" 
51369  894 
by (induct t rule: split_int.induct) (auto simp add: Let_def split_def) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

895 

324622260d29
Added 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 
lemma numfloor_nz: "nozerocoeff t \<Longrightarrow> nozerocoeff (numfloor t)" 
51369  897 
by (simp add: numfloor_def Let_def split_def) 
898 
(cases "fst (split_int t)", simp_all add: split_int_nz numadd_nz) 

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

899 

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

900 
lemma simpnum_nz: "nozerocoeff (simpnum t)" 
51369  901 
by (induct t rule: simpnum.induct) 
902 
(auto simp add: numadd_nz numneg_nz numsub_nz nummul_nz numfloor_nz) 

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

903 

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

905 
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

906 
case (2 n c t) 
61945  907 
hence cnz: "c \<noteq>0" and mx: "max \<bar>c\<bar> (maxcoeff t) = 0" by simp+ 
908 
have "max \<bar>c\<bar> (maxcoeff t) \<ge> \<bar>c\<bar>" by simp 

909 
with cnz have "max \<bar>c\<bar> (maxcoeff t) > 0" by arith 

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

911 
next 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

912 
case (3 c s t) 
61945  913 
hence cnz: "c \<noteq>0" and mx: "max \<bar>c\<bar> (maxcoeff t) = 0" by simp+ 
914 
have "max \<bar>c\<bar> (maxcoeff t) \<ge> \<bar>c\<bar>" by simp 

915 
with cnz have "max \<bar>c\<bar> (maxcoeff t) > 0" by arith 

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

917 
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

918 

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

920 
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

921 
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

922 
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

923 
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

924 
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

925 

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

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

927 
"simp_num_pair \<equiv> (\<lambda> (t,n). (if n = 0 then (C 0, 0) else 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

928 
(let t' = simpnum t ; g = numgcd t' in 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

929 
if g > 1 then (let g' = gcd n g in 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

930 
if g' = 1 then (t',n) 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

931 
else (reducecoeffh t' g', n div 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

932 
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

933 

324622260d29
Added 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 
lemma simp_num_pair_ci: 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

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

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

937 
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

938 
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

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

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

942 
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

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

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

945 
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

946 
{assume g1:"?g>1" hence g0: "?g > 0" by simp 
31706  947 
from g1 nnz have gp0: "?g' \<noteq> 0" by simp 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31730
diff
changeset

948 
hence g'p: "?g' > 0" using gcd_ge_0_int[where x="n" and y="numgcd ?t'"] by arith 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

949 
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

950 
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

951 
moreover {assume g'1:"?g'>1" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

952 
from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff ?t' ?g" .. 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

953 
let ?tt = "reducecoeffh ?t' ?g'" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

954 
let ?t = "Inum bs ?tt" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

955 
have gpdg: "?g' dvd ?g" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

956 
have gpdd: "?g' dvd n" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

957 
have gpdgp: "?g' dvd ?g'" by simp 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

958 
from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

959 
have th2:"real_of_int ?g' * ?t = Inum bs ?t'" by simp 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

960 
from nnz g1 g'1 have "?lhs = ?t / real_of_int (n div ?g')" by (simp add: simp_num_pair_def Let_def) 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

961 
also have "\<dots> = (real_of_int ?g' * ?t) / (real_of_int ?g' * (real_of_int (n div ?g')))" by simp 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

962 
also have "\<dots> = (Inum bs ?t' / real_of_int n)" 
46670  963 
using real_of_int_div[OF gpdd] th2 gp0 by simp 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

964 
finally have "?lhs = Inum bs t / real_of_int n" by simp 
41807  965 
then have ?thesis using nnz g1 g'1 by (simp add: simp_num_pair_def) } 
966 
ultimately have ?thesis by blast } 

967 
ultimately have ?thesis by blast } 

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

968 
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

969 
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

970 

41807  971 
lemma simp_num_pair_l: 
972 
assumes tnb: "numbound0 t" and np: "n >0" and tn: "simp_num_pair (t,n) = (t',n')" 

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

973 
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

974 
proof 
41807  975 
let ?t' = "simpnum t" 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

976 
let ?g = "numgcd ?t'" 
31706  977 
let ?g' = "gcd n ?g" 
41807  978 
{ assume nz: "n = 0" hence ?thesis using assms by (simp add: Let_def simp_num_pair_def) } 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

979 
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

980 
{ assume nnz: "n \<noteq> 0" 
41807  981 
{assume "\<not> ?g > 1" hence ?thesis using assms by (auto simp add: Let_def simp_num_pair_def) } 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

982 
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

983 
{assume g1:"?g>1" hence g0: "?g > 0" by simp 
31706  984 
from g1 nnz have gp0: "?g' \<noteq> 0" by simp 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31730
diff
changeset

985 
hence g'p: "?g' > 0" using gcd_ge_0_int[where x="n" and y="numgcd ?t'"] by arith 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

986 
hence "?g'= 1 \<or> ?g' > 1" by arith 
41807  987 
moreover {assume "?g'=1" hence ?thesis using assms g1 g0 
988 
by (auto simp add: Let_def simp_num_pair_def) } 

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

989 
moreover {assume g'1:"?g'>1" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

990 
have gpdg: "?g' dvd ?g" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

991 
have gpdd: "?g' dvd n" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

992 
have gpdgp: "?g' dvd ?g'" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

993 
from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" . 
47142  994 
from zdiv_mono1[OF g'n g'p, simplified div_self[OF gp0]] 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

995 
have "n div ?g' >0" by simp 
41807  996 
hence ?thesis using assms g1 g'1 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

997 
by(auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0)} 
41807  998 
ultimately have ?thesis by blast } 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

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

1000 
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

1001 
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

1002 

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

1004 
"not (NOT p) = p" 
41839  1005 
 "not T = F" 
1006 
 "not F = T" 

1007 
 "not (Lt t) = Ge t" 

1008 
 "not (Le t) = Gt t" 

1009 
 "not (Gt t) = Le t" 

1010 
 "not (Ge t) = Lt t" 

1011 
 "not (Eq t) = NEq t" 

1012 
 "not (NEq t) = Eq t" 

1013 
 "not (Dvd i t) = NDvd i t" 

1014 
 "not (NDvd i t) = Dvd i t" 

1015 
 "not (And p q) = Or (not p) (not q)" 

1016 
 "not (Or p q) = And (not p) (not q)" 

1017 
 "not p = NOT p" 

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

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

1020 
lemma not_qf[simp]: "qfree p \<Longrightarrow> qfree (not p)" 
41807  1021 
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

1022 
lemma not_nb[simp]: "bound0 p \<Longrightarrow> bound0 (not p)" 
41807  1023 
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

1024 

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

1025 
definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

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

1027 
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

1028 
lemma conj[simp]: "Ifm bs (conj p q) = Ifm bs (And p q)" 
41807  1029 
by (cases "p=F \<or> q=F", simp_all add: conj_def) (cases p, simp_all) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1030 

324622260d29
Added 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 
lemma conj_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (conj p q)" 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

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

1033 
lemma conj_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (conj p q)" 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

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

1035 

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

1036 
definition disj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

1037 
"disj p q \<equiv> (if (p = T \<or> q=T) then T else if p=F then q else if q=F then p 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1038 
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

1039 

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

1040 
lemma disj[simp]: "Ifm bs (disj p q) = Ifm bs (Or p q)" 
41807  1041 
by (cases "p=T \<or> q=T",simp_all add: disj_def) (cases p,simp_all) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1042 
lemma disj_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (disj p q)" 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

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

1044 
lemma disj_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (disj p q)" 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

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

1046 

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

1047 
definition imp :: "fm \<Rightarrow> fm \<Rightarrow> fm" where 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

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

1049 
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

1050 
lemma imp[simp]: "Ifm bs (imp p q) = Ifm bs (Imp p q)" 
41807  1051 
by (cases "p=F \<or> q=T",simp_all add: imp_def) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1052 
lemma imp_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (imp p q)" 
41807  1053 
using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def) 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1054 

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

1055 
definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm" where 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

1056 
"iff p q \<equiv> (if (p = q) then T else if (p = not q \<or> not p = q) then F else 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

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

1058 
Iff p q)" 
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61610
diff
changeset

1059 

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

1060 
lemma iff[simp]: "Ifm bs (iff p q) = Ifm bs (Iff p q)" 
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61610
diff
changeset

1061 
by (unfold iff_def,cases "p=q", simp,cases "p=not q", simp) (cases "not p= q", auto simp add:not) 
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61610
diff
changeset

1062 

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

1063 
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

1064 
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

1065 

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

1067 
"check_int (C i) = True" 
41839  1068 
 "check_int (Floor t) = True" 
1069 
 "check_int (Mul i t) = check_int t" 

1070 
 "check_int (Add t s) = (check_int t \<and> check_int s)" 

1071 
 "check_int (Neg t) = check_int t" 

1072 
 "check_int (CF c t s) = check_int s" 

1073 
 "check_int t = False" 

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

1074 
lemma check_int: "check_int t \<Longrightarrow> isint t bs" 
51369  1075 
by (induct t) (auto simp add: isint_add isint_Floor isint_Mul isint_neg isint_c isint_CF) 
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

1076 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

1077 
lemma rdvd_left1_int: "real_of_int \<lfloor>t\<rfloor> = t \<Longrightarrow> 1 rdvd 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

1078 
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

1079 

61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

1080 
lemma rdvd_reduce: 
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

1081 
assumes gd:"g dvd d" and gc:"g dvd c" and gp: "g > 0" 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

1082 
shows "real_of_int (d::int) rdvd real_of_int (c::int)*t = (real_of_int (d div g) rdvd real_of_int (c div g)*t)" 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1083 
proof 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

1084 
assume d: "real_of_int d rdvd real_of_int c * t" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

1085 
from d rdvd_def obtain k where k_def: "real_of_int c * t = real_of_int d* real_of_int (k::int)" by auto 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1086 
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

1087 
from gc dvd_def obtain kc where kc_def: "c = g * kc" by auto 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

1088 
from k_def kd_def kc_def have "real_of_int g * real_of_int kc * t = real_of_int g * real_of_int kd * real_of_int k" by simp 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

1089 
hence "real_of_int kc * t = real_of_int kd * real_of_int k" using gp by simp 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

1090 
hence th:"real_of_int kd rdvd real_of_int kc * t" using rdvd_def 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

1091 
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

1092 
from kc_def gp have "kc = c div g" by simp 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

1093 
with th th' show "real_of_int (d div g) rdvd real_of_int (c div g) * 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

1094 
next 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

1095 
assume d: "real_of_int (d div g) rdvd real_of_int (c div g) * t" 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1096 
from gp have gnz: "g \<noteq> 0" by simp 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

1097 
thus "real_of_int d rdvd real_of_int c * t" using d rdvd_mult[OF gnz, where n="d div g" and x="real_of_int (c div g) * t"] real_of_int_div[OF gd] real_of_int_div[OF gc] 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

1098 
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

1099 

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

1100 
definition simpdvd :: "int \<Rightarrow> num \<Rightarrow> (int \<times> num)" where 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

1101 
"simpdvd d t \<equiv> 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

1102 
(let g = numgcd t in 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

1103 
if g > 1 then (let g' = gcd d g in 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

1104 
if g' = 1 then (d, t) 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

1105 
else (d div g',reducecoeffh 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

1106 
else (d, t))" 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

1107 
lemma simpdvd: 
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

1108 
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

1109 
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

1110 
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

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

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

1114 
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

1115 
{assume g1:"?g>1" hence g0: "?g > 0" by simp 
31706  1116 
from g1 dnz have gp0: "?g' \<noteq> 0" by simp 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31730
diff
changeset

1117 
hence g'p: "?g' > 0" using gcd_ge_0_int[where x="d" and y="numgcd t"] by arith 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1118 
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

1119 
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

1120 
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

1121 
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

1122 
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

1123 
let ?t = "Inum bs ?tt" 
31706  1124 
have gpdg: "?g' dvd ?g" by simp 
1125 
have gpdd: "?g' dvd d" by simp 

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

1126 
have gpdgp: "?g' dvd ?g'" by simp 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

1127 
from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

1128 
have th2:"real_of_int ?g' * ?t = Inum bs t" by simp 
41807  1129 
from assms g1 g0 g'1 
1130 
have "Ifm bs (Dvd (fst (simpdvd d t)) (snd(simpdvd d t))) = Ifm bs (Dvd (d div ?g') ?tt)" 

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

1131 
by (simp add: simpdvd_def Let_def) 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

1132 
also have "\<dots> = (real_of_int d rdvd (Inum bs t))" 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

1133 
using rdvd_reduce[OF gpdd gpdgp g'p, where t="?t", simplified div_self[OF gp0]] 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31952
diff
changeset

1134 
th2[symmetric] by simp 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1135 
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

1136 
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

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

1139 
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

1140 

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

1142 
"simpfm (And p q) = conj (simpfm p) (simpfm q)" 
41839  1143 
 "simpfm (Or p q) = disj (simpfm p) (simpfm q)" 
1144 
 "simpfm (Imp p q) = imp (simpfm p) (simpfm q)" 

1145 
 "simpfm (Iff p q) = iff (simpfm p) (simpfm q)" 

1146 
 "simpfm (NOT p) = not (simpfm p)" 

61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

1147 
 "simpfm (Lt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v < 0) then T else F 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1148 
 _ \<Rightarrow> Lt (reducecoeff a'))" 
41839  1149 
 "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'))" 
1150 
 "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'))" 

1151 
 "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'))" 

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

1153 
 "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'))" 

1154 
 "simpfm (Dvd i a) = (if i=0 then simpfm (Eq a) 

61945  1155 
else if (\<bar>i\<bar> = 1) \<and> check_int a then 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

1156 
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))" 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61652
diff
changeset

1157 
 "simpfm (NDvd i a) = (if i=0 then simpfm (NEq a) 
61945  1158 
else if (\<bar>i\<bar> = 1) \<and> check_int a then F 
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1159 
else let a' = simpnum a in case a' of C v \<Rightarrow> if (\<not>(i dvd v)) then T else F  _ \<Rightarrow> (let (d,t) = simpdvd i a' in NDvd d t))" 
41839  1160 
 "simpfm p = p" 
1161 
by pat_completeness auto 

1162 
termination by (relation "measure fmsize") auto 

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

1163 

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

1165 
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

1166 
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

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

1168 
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

1169 
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

1170 
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

1171 
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

1172 
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

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

1174 
with numgcd_pos[where t="?sa"] have "?g > 0" by (cases "?g=0", auto) 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

1175 
hence gp: "real_of_int ?g > 0" by simp 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

1176 
have "Inum bs ?sa = real_of_int ?g* ?r" by (simp add: reducecoeff) 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

1177 
with sa have "Inum bs a < 0 = (real_of_int ?g * ?r < real_of_int ?g * 0)" 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

1178 
also have "\<dots> = (?r < 0)" using gp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

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

1180 
finally have ?case using H by (cases "?sa" , simp_all add: Let_def)} 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1181 
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

1182 
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

1183 
case (7 a) let ?sa = "simpnum a" have sa: "Inum bs ?sa = Inum bs a" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

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

1185 
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

1186 
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

1187 
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

1188 
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

1189 
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

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

1191 
with numgcd_pos[where t="?sa"] have "?g > 0" by (cases "?g=0", auto) 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

1192 
hence gp: "real_of_int ?g > 0" by simp 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

1193 
have "Inum bs ?sa = real_of_int ?g* ?r" by (simp add: reducecoeff) 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

1194 
with sa have "Inum bs a \<le> 0 = (real_of_int ?g * ?r \<le> real_of_int ?g * 0)" 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

1195 
also have "\<dots> = (?r \<le> 0)" using gp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

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

1197 
finally have ?case using H by (cases "?sa" , simp_all add: Let_def)} 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

1198 
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

1199 
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

1200 
case (8 a) let ?sa = "simpnum a" have sa: "Inum bs ?sa = Inum bs a" by simp 
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset

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

1202 
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

1203 
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

1204 
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

1205 
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

1206 
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

1207 
{assume 