src/HOL/ex/Reflected_Presburger.thy
author chaieb
Wed Sep 14 17:25:52 2005 +0200 (2005-09-14)
changeset 17378 105519771c67
child 17381 ec9997d0a3ff
permissions -rw-r--r--
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
comm_ring : a reflected Method for proving equalities in a commutative ring
chaieb@17378
     1
(* A formalization of quantifier elimination for Presburger arithmetic*)
chaieb@17378
     2
(* based on a generic quantifier elimination algorithm and 
chaieb@17378
     3
   cooper's methos to eliminate on \<exists> *)
chaieb@17378
     4
chaieb@17378
     5
theory Reflected_Presburger
chaieb@17378
     6
imports Main
chaieb@17378
     7
uses ("rcooper.ML") ("rpresbtac.ML")
chaieb@17378
     8
begin
chaieb@17378
     9
chaieb@17378
    10
(* Shadow syntax for integer terms *)
chaieb@17378
    11
datatype intterm =
chaieb@17378
    12
    Cst int
chaieb@17378
    13
  | Var nat
chaieb@17378
    14
  | Neg intterm
chaieb@17378
    15
  | Add intterm intterm 
chaieb@17378
    16
  | Sub intterm intterm
chaieb@17378
    17
  | Mult intterm intterm
chaieb@17378
    18
chaieb@17378
    19
(* interpretatation of intterms , takes bound variables and free variables *)
chaieb@17378
    20
consts I_intterm :: "int list \<Rightarrow> intterm \<Rightarrow> int"
chaieb@17378
    21
primrec 
chaieb@17378
    22
"I_intterm ats (Cst b) = b"
chaieb@17378
    23
"I_intterm ats (Var n) = (ats!n)"
chaieb@17378
    24
"I_intterm ats (Neg it) = -(I_intterm ats it)"
chaieb@17378
    25
"I_intterm ats (Add it1 it2) = (I_intterm ats it1) + (I_intterm ats it2)" 
chaieb@17378
    26
"I_intterm ats (Sub it1 it2) = (I_intterm ats it1) - (I_intterm ats it2)"
chaieb@17378
    27
"I_intterm ats (Mult it1 it2) = (I_intterm ats it1) * (I_intterm ats it2)"
chaieb@17378
    28
chaieb@17378
    29
(*Shadow syntax for Presburger formulae *)
chaieb@17378
    30
datatype QF = 
chaieb@17378
    31
   Lt intterm intterm
chaieb@17378
    32
  |Gt intterm intterm
chaieb@17378
    33
  |Le intterm intterm
chaieb@17378
    34
  |Ge intterm intterm
chaieb@17378
    35
  |Eq intterm intterm
chaieb@17378
    36
  |Divides intterm intterm
chaieb@17378
    37
  |T
chaieb@17378
    38
  |F
chaieb@17378
    39
  |NOT QF
chaieb@17378
    40
  |And QF QF
chaieb@17378
    41
  |Or QF QF
chaieb@17378
    42
  |Imp QF QF
chaieb@17378
    43
  |Equ QF QF
chaieb@17378
    44
  |QAll QF
chaieb@17378
    45
  |QEx QF
chaieb@17378
    46
chaieb@17378
    47
(* Interpretation of Presburger  formulae *)
chaieb@17378
    48
consts qinterp :: "int list \<Rightarrow> QF \<Rightarrow> bool"
chaieb@17378
    49
primrec
chaieb@17378
    50
"qinterp ats (Lt it1 it2) = (I_intterm ats it1 < I_intterm ats it2)"
chaieb@17378
    51
"qinterp ats (Gt it1 it2) = (I_intterm ats it1 > I_intterm ats it2)"
chaieb@17378
    52
"qinterp ats (Le it1 it2) = (I_intterm ats it1 \<le> I_intterm ats it2)"
chaieb@17378
    53
"qinterp ats (Ge it1 it2) = (I_intterm ats it1 \<ge> I_intterm ats it2)"
chaieb@17378
    54
"qinterp ats (Divides it1 it2) = (I_intterm ats it1 dvd I_intterm ats it2)"
chaieb@17378
    55
"qinterp ats (Eq it1 it2) = (I_intterm ats it1 = I_intterm ats it2)"
chaieb@17378
    56
"qinterp ats T = True"
chaieb@17378
    57
"qinterp ats F = False"
chaieb@17378
    58
"qinterp ats (NOT p) = (\<not>(qinterp ats p))"
chaieb@17378
    59
"qinterp ats (And p q) = (qinterp ats p \<and> qinterp ats q)"
chaieb@17378
    60
"qinterp ats (Or p q) = (qinterp ats p \<or> qinterp ats q)"
chaieb@17378
    61
"qinterp ats (Imp p q) = (qinterp ats p \<longrightarrow> qinterp ats q)"
chaieb@17378
    62
"qinterp ats (Equ p q) = (qinterp ats p = qinterp ats q)"
chaieb@17378
    63
"qinterp ats (QAll p) = (\<forall>x. qinterp (x#ats) p)"
chaieb@17378
    64
"qinterp ats (QEx p) = (\<exists>x. qinterp (x#ats) p)"
chaieb@17378
    65
chaieb@17378
    66
(* quantifier elimination based on qe, quantifier elimination for an
chaieb@17378
    67
   existential formula, with quantifier free body 
chaieb@17378
    68
   Since quantifier elimination for one formula is allowed to fail, 
chaieb@17378
    69
   the reult is of type QF option *)
chaieb@17378
    70
chaieb@17378
    71
consts lift_bin:: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<times> 'a option \<times> 'a option \<Rightarrow> 'b option"
chaieb@17378
    72
recdef lift_bin "measure (\<lambda>(c,a,b). size a)"
chaieb@17378
    73
"lift_bin (c,Some a,Some b) = Some (c a b)"
chaieb@17378
    74
"lift_bin (c,x, y)  = None"
chaieb@17378
    75
chaieb@17378
    76
lemma lift_bin_Some:
chaieb@17378
    77
  assumes ls: "lift_bin (c,x,y) = Some t"
chaieb@17378
    78
  shows "(\<exists>a. x = Some a) \<and> (\<exists>b. y = Some b)"
chaieb@17378
    79
  using ls 
chaieb@17378
    80
  by (cases "x", auto) (cases "y", auto)+
chaieb@17378
    81
chaieb@17378
    82
consts lift_un:: "('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"
chaieb@17378
    83
primrec
chaieb@17378
    84
"lift_un c None = None"
chaieb@17378
    85
"lift_un c (Some p) = Some (c p)"
chaieb@17378
    86
chaieb@17378
    87
consts lift_qe:: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a option \<Rightarrow> 'b option"
chaieb@17378
    88
primrec
chaieb@17378
    89
"lift_qe qe None = None"
chaieb@17378
    90
"lift_qe qe (Some p) = qe p"
chaieb@17378
    91
chaieb@17378
    92
(* generic quantifier elimination *)
chaieb@17378
    93
consts qelim :: "(QF \<Rightarrow> QF option) \<times> QF \<Rightarrow> QF option"
chaieb@17378
    94
recdef qelim "measure (\<lambda>(qe,p). size p)"
chaieb@17378
    95
"qelim (qe, (QAll p)) = lift_un NOT (lift_qe qe (lift_un NOT (qelim (qe ,p))))"
chaieb@17378
    96
"qelim (qe, (QEx p)) = lift_qe qe (qelim (qe,p))"
chaieb@17378
    97
"qelim (qe, (And p q)) = lift_bin (And, (qelim (qe, p)), (qelim (qe, q)))"
chaieb@17378
    98
"qelim (qe, (Or p q)) = lift_bin (Or, (qelim (qe, p)), (qelim (qe, q)))"
chaieb@17378
    99
"qelim (qe, (Imp p q)) = lift_bin (Imp, (qelim (qe, p)), (qelim (qe, q)))"
chaieb@17378
   100
"qelim (qe, (Equ p q)) = lift_bin (Equ, (qelim (qe, p)), (qelim (qe, q)))"
chaieb@17378
   101
"qelim (qe,NOT p) = lift_un NOT (qelim (qe,p))"
chaieb@17378
   102
"qelim (qe, p) = Some p"
chaieb@17378
   103
chaieb@17378
   104
(* quantifier free-ness *)
chaieb@17378
   105
consts isqfree :: "QF \<Rightarrow> bool"
chaieb@17378
   106
recdef isqfree "measure size"
chaieb@17378
   107
"isqfree (QAll p) = False"
chaieb@17378
   108
"isqfree (QEx p) = False"
chaieb@17378
   109
"isqfree (And p q) = (isqfree p \<and> isqfree q)"
chaieb@17378
   110
"isqfree (Or p q) = (isqfree p \<and> isqfree q)"
chaieb@17378
   111
"isqfree (Imp p q) = (isqfree p \<and> isqfree q)"
chaieb@17378
   112
"isqfree (Equ p q) = (isqfree p \<and> isqfree q)"
chaieb@17378
   113
"isqfree (NOT p) = isqfree p"
chaieb@17378
   114
"isqfree p = True"
chaieb@17378
   115
chaieb@17378
   116
(* qelim lifts quantifierfreeness*)
chaieb@17378
   117
lemma qelim_qfree: 
chaieb@17378
   118
  assumes qeqf: "(\<And> q q'. \<lbrakk>isqfree q ; qe q = Some q'\<rbrakk> \<Longrightarrow>  isqfree q')"
chaieb@17378
   119
  shows qff:"\<And> p'. qelim (qe, p) = Some p' \<Longrightarrow> isqfree p'"
chaieb@17378
   120
  using qeqf
chaieb@17378
   121
proof (induct p)
chaieb@17378
   122
  case (Lt a b)
chaieb@17378
   123
  have "qelim (qe, Lt a b) = Some (Lt a b)" by simp
chaieb@17378
   124
  moreover have "qelim (qe,Lt a b) = Some p'" . 
chaieb@17378
   125
  ultimately have "p' = Lt a b" by simp
chaieb@17378
   126
  moreover have "isqfree (Lt a b)" by simp
chaieb@17378
   127
  ultimately 
chaieb@17378
   128
  show ?case  by simp
chaieb@17378
   129
next  
chaieb@17378
   130
  case (Gt a b)
chaieb@17378
   131
  have "qelim (qe, Gt a b) = Some (Gt a b)" by simp
chaieb@17378
   132
  moreover have "qelim (qe,Gt a b) = Some p'" . 
chaieb@17378
   133
  ultimately have "p' = Gt a b" by simp
chaieb@17378
   134
  moreover have "isqfree (Gt a b)" by simp
chaieb@17378
   135
  ultimately 
chaieb@17378
   136
  show ?case  by simp
chaieb@17378
   137
next  
chaieb@17378
   138
  case (Le a b)
chaieb@17378
   139
  have "qelim (qe, Le a b) = Some (Le a b)" by simp
chaieb@17378
   140
  moreover have "qelim (qe,Le a b) = Some p'" . 
chaieb@17378
   141
  ultimately have "p' = Le a b" by simp
chaieb@17378
   142
  moreover have "isqfree (Le a b)" by simp
chaieb@17378
   143
  ultimately 
chaieb@17378
   144
  show ?case  by simp
chaieb@17378
   145
next  
chaieb@17378
   146
  case (Ge a b)
chaieb@17378
   147
  have "qelim (qe, Ge a b) = Some (Ge a b)" by simp
chaieb@17378
   148
  moreover have "qelim (qe,Ge a b) = Some p'" . 
chaieb@17378
   149
  ultimately have "p' = Ge a b" by simp
chaieb@17378
   150
  moreover have "isqfree (Ge a b)" by simp
chaieb@17378
   151
  ultimately 
chaieb@17378
   152
  show ?case  by simp
chaieb@17378
   153
next  
chaieb@17378
   154
  case (Eq a b)
chaieb@17378
   155
  have "qelim (qe, Eq a b) = Some (Eq a b)" by simp
chaieb@17378
   156
  moreover have "qelim (qe,Eq a b) = Some p'" . 
chaieb@17378
   157
  ultimately have "p' = Eq a b" by simp
chaieb@17378
   158
  moreover have "isqfree (Eq a b)" by simp
chaieb@17378
   159
  ultimately 
chaieb@17378
   160
  show ?case  by simp
chaieb@17378
   161
next  
chaieb@17378
   162
  case (Divides a b)
chaieb@17378
   163
  have "qelim (qe, Divides a b) = Some (Divides a b)" by simp
chaieb@17378
   164
  moreover have "qelim (qe,Divides a b) = Some p'" . 
chaieb@17378
   165
  ultimately have "p' = Divides a b" by simp
chaieb@17378
   166
  moreover have "isqfree (Divides a b)" by simp
chaieb@17378
   167
  ultimately 
chaieb@17378
   168
  show ?case  by simp
chaieb@17378
   169
next  
chaieb@17378
   170
  case T 
chaieb@17378
   171
  have "qelim(qe,T) = Some T" by simp
chaieb@17378
   172
  moreover have "qelim(qe,T) = Some p'" .
chaieb@17378
   173
  ultimately have "p' = T" by simp
chaieb@17378
   174
  moreover have "isqfree T" by simp
chaieb@17378
   175
  ultimately show ?case by simp
chaieb@17378
   176
next  
chaieb@17378
   177
  case F
chaieb@17378
   178
  have "qelim(qe,F) = Some F" by simp
chaieb@17378
   179
  moreover have "qelim(qe,F) = Some p'" .
chaieb@17378
   180
  ultimately have "p' = F" by simp
chaieb@17378
   181
  moreover have "isqfree F" by simp
chaieb@17378
   182
  ultimately show ?case by simp
chaieb@17378
   183
next  
chaieb@17378
   184
  case (NOT p)
chaieb@17378
   185
  from "NOT.prems" have "\<exists> p1. qelim(qe,p) = Some p1"
chaieb@17378
   186
    by  (cases "qelim(qe,p)") simp_all
chaieb@17378
   187
  then obtain "p1" where p1_def: "qelim(qe,p) = Some p1" by blast
chaieb@17378
   188
  from "NOT.prems" have "\<And>q q'. \<lbrakk>isqfree q; qe q = Some q'\<rbrakk> \<Longrightarrow> isqfree q'" 
chaieb@17378
   189
    by blast
chaieb@17378
   190
  with "NOT.hyps" p1_def have p1qf: "isqfree p1" by blast
chaieb@17378
   191
  then have "p' = NOT p1" using "NOT.prems" p1_def
chaieb@17378
   192
    by (cases "qelim(qe,NOT p)") simp_all
chaieb@17378
   193
  then show ?case using p1qf by simp
chaieb@17378
   194
next  
chaieb@17378
   195
  case (And p q) 
chaieb@17378
   196
  from "And.prems" have p1q1: "(\<exists>p1. qelim(qe,p) = Some p1) \<and> 
chaieb@17378
   197
    (\<exists>q1. qelim(qe,q) = Some q1)" using lift_bin_Some[where c="And"] by simp
chaieb@17378
   198
  from p1q1 obtain "p1" and "q1" 
chaieb@17378
   199
    where p1_def: "qelim(qe,p) = Some p1" 
chaieb@17378
   200
    and q1_def: "qelim(qe,q) = Some q1" by blast
chaieb@17378
   201
  from prems have qf1:"isqfree p1"
chaieb@17378
   202
    using p1_def by blast
chaieb@17378
   203
  from prems have qf2:"isqfree q1"
chaieb@17378
   204
    using q1_def by blast
chaieb@17378
   205
  from "And.prems" have "qelim(qe,And p q) = Some p'" by blast
chaieb@17378
   206
  then have "p' = And p1 q1" using p1_def q1_def by simp
chaieb@17378
   207
  then 
chaieb@17378
   208
  show ?case using qf1 qf2 by simp
chaieb@17378
   209
next  
chaieb@17378
   210
  case (Or p q)
chaieb@17378
   211
  from "Or.prems" have p1q1: "(\<exists>p1. qelim(qe,p) = Some p1) \<and> 
chaieb@17378
   212
    (\<exists>q1. qelim(qe,q) = Some q1)" using lift_bin_Some[where c="Or"] by simp
chaieb@17378
   213
  from p1q1 obtain "p1" and "q1" 
chaieb@17378
   214
    where p1_def: "qelim(qe,p) = Some p1" 
chaieb@17378
   215
    and q1_def: "qelim(qe,q) = Some q1" by blast
chaieb@17378
   216
  from prems have qf1:"isqfree p1"
chaieb@17378
   217
    using p1_def by blast
chaieb@17378
   218
  from prems have qf2:"isqfree q1"
chaieb@17378
   219
    using q1_def by blast
chaieb@17378
   220
  from "Or.prems" have "qelim(qe,Or p q) = Some p'" by blast
chaieb@17378
   221
  then have "p' = Or p1 q1" using p1_def q1_def by simp
chaieb@17378
   222
  then 
chaieb@17378
   223
  show ?case using qf1 qf2 by simp
chaieb@17378
   224
next  
chaieb@17378
   225
  case (Imp p q)
chaieb@17378
   226
  from "Imp.prems" have p1q1: "(\<exists>p1. qelim(qe,p) = Some p1) \<and> 
chaieb@17378
   227
    (\<exists>q1. qelim(qe,q) = Some q1)" using lift_bin_Some[where c="Imp"] by simp
chaieb@17378
   228
  from p1q1 obtain "p1" and "q1" 
chaieb@17378
   229
    where p1_def: "qelim(qe,p) = Some p1" 
chaieb@17378
   230
    and q1_def: "qelim(qe,q) = Some q1" by blast
chaieb@17378
   231
  from prems have qf1:"isqfree p1"
chaieb@17378
   232
    using p1_def by blast
chaieb@17378
   233
  from prems have qf2:"isqfree q1"
chaieb@17378
   234
    using q1_def by blast
chaieb@17378
   235
  from "Imp.prems" have "qelim(qe,Imp p q) = Some p'" by blast
chaieb@17378
   236
  then have "p' = Imp p1 q1" using p1_def q1_def by simp
chaieb@17378
   237
  then 
chaieb@17378
   238
  show ?case using qf1 qf2 by simp
chaieb@17378
   239
next  
chaieb@17378
   240
  case (Equ p q)
chaieb@17378
   241
  from "Equ.prems" have p1q1: "(\<exists>p1. qelim(qe,p) = Some p1) \<and> 
chaieb@17378
   242
    (\<exists>q1. qelim(qe,q) = Some q1)" using lift_bin_Some[where c="Equ"] by simp
chaieb@17378
   243
  from p1q1 obtain "p1" and "q1" 
chaieb@17378
   244
    where p1_def: "qelim(qe,p) = Some p1" 
chaieb@17378
   245
    and q1_def: "qelim(qe,q) = Some q1" by blast
chaieb@17378
   246
  from prems have qf1:"isqfree p1"
chaieb@17378
   247
    using p1_def by blast
chaieb@17378
   248
  from prems have qf2:"isqfree q1"
chaieb@17378
   249
    using q1_def by blast
chaieb@17378
   250
  from "Equ.prems" have "qelim(qe,Equ p q) = Some p'" by blast
chaieb@17378
   251
  then have "p' = Equ p1 q1" using p1_def q1_def by simp
chaieb@17378
   252
  then 
chaieb@17378
   253
  show ?case using qf1 qf2 by simp
chaieb@17378
   254
next 
chaieb@17378
   255
  case (QEx p)
chaieb@17378
   256
  from "QEx.prems" have "\<exists> p1. qelim(qe,p) = Some p1"
chaieb@17378
   257
    by  (cases "qelim(qe,p)") simp_all
chaieb@17378
   258
  then obtain "p1" where p1_def: "qelim(qe,p) = Some p1" by blast
chaieb@17378
   259
  from "QEx.prems" have "\<And>q q'. \<lbrakk>isqfree q; qe q = Some q'\<rbrakk> \<Longrightarrow> isqfree q'" 
chaieb@17378
   260
    by blast
chaieb@17378
   261
  with "QEx.hyps" p1_def have p1qf: "isqfree p1" by blast
chaieb@17378
   262
  from "QEx.prems" have "qe p1 = Some p'" using p1_def by simp
chaieb@17378
   263
  with "QEx.prems" show ?case  using p1qf 
chaieb@17378
   264
    by simp
chaieb@17378
   265
next 
chaieb@17378
   266
  case (QAll p) 
chaieb@17378
   267
  from "QAll.prems"
chaieb@17378
   268
  have "\<exists> p1. lift_qe qe (lift_un NOT (qelim (qe ,p))) = Some p1" 
chaieb@17378
   269
    by (cases "lift_qe qe (lift_un NOT (qelim (qe ,p)))") simp_all
chaieb@17378
   270
  then obtain "p1" where 
chaieb@17378
   271
    p1_def:"lift_qe qe (lift_un NOT (qelim (qe ,p))) = Some p1" by blast
chaieb@17378
   272
  then have "\<exists> p2. lift_un NOT (qelim (qe ,p)) = Some p2"
chaieb@17378
   273
    by (cases "qelim (qe ,p)") simp_all
chaieb@17378
   274
  then obtain "p2" 
chaieb@17378
   275
    where p2_def:"lift_un NOT (qelim (qe ,p)) = Some p2" by blast
chaieb@17378
   276
  then have "\<exists> p3. qelim(qe,p) = Some p3" by (cases "qelim(qe,p)") simp_all
chaieb@17378
   277
  then obtain "p3" where p3_def: "qelim(qe,p) = Some p3" by blast
chaieb@17378
   278
  with prems have qf3: "isqfree p3" by blast
chaieb@17378
   279
  have p2_def2: "p2 = NOT p3" using p2_def p3_def by simp
chaieb@17378
   280
  then have qf2: "isqfree p2" using qf3 by simp
chaieb@17378
   281
  have p1_edf2: "qe p2 = Some p1" using p1_def p2_def by simp
chaieb@17378
   282
  with "QAll.prems" have qf1: "isqfree p1" using qf2 by blast
chaieb@17378
   283
  from "QAll.prems" have "p' = NOT p1" using p1_def by simp
chaieb@17378
   284
  with qf1 show ?case by simp
chaieb@17378
   285
qed
chaieb@17378
   286
chaieb@17378
   287
(* qelim lifts semantical equivalence *)
chaieb@17378
   288
lemma qelim_corr: 
chaieb@17378
   289
  assumes qecorr: "(\<And> q q' ats. \<lbrakk>isqfree q ; qe q = Some q'\<rbrakk> \<Longrightarrow>  (qinterp ats (QEx q)) = (qinterp ats q'))"
chaieb@17378
   290
  and qeqf: "(\<And> q q'. \<lbrakk>isqfree q ; qe q = Some q'\<rbrakk> \<Longrightarrow>  isqfree q')"
chaieb@17378
   291
  shows qff:"\<And> p' ats. qelim (qe, p) = Some p' \<Longrightarrow> (qinterp ats p = qinterp ats p')" (is "\<And> p' ats. ?Qe p p' \<Longrightarrow> (?F ats p = ?F ats p')")
chaieb@17378
   292
  using qeqf qecorr
chaieb@17378
   293
proof (induct p)
chaieb@17378
   294
  case (NOT f)  
chaieb@17378
   295
  from "NOT.prems" have "\<exists>f'. ?Qe f f' " by (cases "qelim(qe,f)") simp_all
chaieb@17378
   296
  then obtain "f'" where df': "?Qe f f'" by blast
chaieb@17378
   297
  with prems have feqf': "?F ats f = ?F ats f'" by blast
chaieb@17378
   298
  from "NOT.prems" df' have "p' = NOT f'" by simp
chaieb@17378
   299
  with feqf' show ?case by simp
chaieb@17378
   300
chaieb@17378
   301
next
chaieb@17378
   302
  case (And f g) 
chaieb@17378
   303
  from "And.prems" have f1g1: "(\<exists>f1. qelim(qe,f) = Some f1) \<and> 
chaieb@17378
   304
    (\<exists>g1. qelim(qe,g) = Some g1)" using lift_bin_Some[where c="And"] by simp
chaieb@17378
   305
  from f1g1 obtain "f1" and "g1" 
chaieb@17378
   306
    where f1_def: "qelim(qe, f) = Some f1" 
chaieb@17378
   307
    and g1_def: "qelim(qe,g) = Some g1" by blast
chaieb@17378
   308
  from prems f1_def have feqf1: "?F ats f = ?F ats f1" by blast
chaieb@17378
   309
  from prems g1_def have geqg1: "?F ats g = ?F ats g1" by blast
chaieb@17378
   310
  from "And.prems" f1_def g1_def have "p' = And f1 g1" by simp
chaieb@17378
   311
  with feqf1 geqg1 show ?case by simp
chaieb@17378
   312
chaieb@17378
   313
next
chaieb@17378
   314
  case (Or f g) 
chaieb@17378
   315
  from "Or.prems" have f1g1: "(\<exists>f1. qelim(qe,f) = Some f1) \<and> 
chaieb@17378
   316
    (\<exists>g1. qelim(qe,g) = Some g1)" using lift_bin_Some[where c="Or"] by simp
chaieb@17378
   317
  from f1g1 obtain "f1" and "g1" 
chaieb@17378
   318
    where f1_def: "qelim(qe, f) = Some f1" 
chaieb@17378
   319
    and g1_def: "qelim(qe,g) = Some g1" by blast
chaieb@17378
   320
  from prems f1_def have feqf1: "?F ats f = ?F ats  f1" by blast
chaieb@17378
   321
  from prems g1_def have geqg1: "?F ats g = ?F ats g1" by blast
chaieb@17378
   322
  from "Or.prems" f1_def g1_def have "p' = Or f1 g1" by simp
chaieb@17378
   323
  with feqf1 geqg1 show ?case by simp
chaieb@17378
   324
next
chaieb@17378
   325
  case (Imp f g)
chaieb@17378
   326
  from "Imp.prems" have f1g1: "(\<exists>f1. qelim(qe,f) = Some f1) \<and> 
chaieb@17378
   327
    (\<exists>g1. qelim(qe,g) = Some g1)" using lift_bin_Some[where c="Imp"] by simp
chaieb@17378
   328
  from f1g1 obtain "f1" and "g1" 
chaieb@17378
   329
    where f1_def: "qelim(qe, f) = Some f1" 
chaieb@17378
   330
    and g1_def: "qelim(qe,g) = Some g1" by blast
chaieb@17378
   331
  from prems f1_def have feqf1: "?F ats f = ?F ats f1" by blast
chaieb@17378
   332
  from prems g1_def have geqg1: "?F ats g = ?F ats g1" by blast
chaieb@17378
   333
  from "Imp.prems" f1_def g1_def have "p' = Imp f1 g1" by simp
chaieb@17378
   334
  with feqf1 geqg1 show ?case by simp
chaieb@17378
   335
next
chaieb@17378
   336
  case (Equ f g)
chaieb@17378
   337
  from "Equ.prems" have f1g1: "(\<exists>f1. qelim(qe,f) = Some f1) \<and> 
chaieb@17378
   338
    (\<exists>g1. qelim(qe,g) = Some g1)" using lift_bin_Some[where c="Equ"] by simp
chaieb@17378
   339
  from f1g1 obtain "f1" and "g1" 
chaieb@17378
   340
    where f1_def: "qelim(qe, f) = Some f1" 
chaieb@17378
   341
    and g1_def: "qelim(qe,g) = Some g1" by blast
chaieb@17378
   342
  from prems f1_def have feqf1: "?F ats f = ?F ats f1" by blast
chaieb@17378
   343
  from prems g1_def have geqg1: "?F ats g = ?F ats g1" by blast
chaieb@17378
   344
  from "Equ.prems" f1_def g1_def have "p' = Equ f1 g1" by simp
chaieb@17378
   345
  with feqf1 geqg1 show ?case by simp
chaieb@17378
   346
next
chaieb@17378
   347
  case (QEx f) 
chaieb@17378
   348
    from "QEx.prems" have "\<exists> f1. ?Qe f f1"
chaieb@17378
   349
    by  (cases "qelim(qe,f)") simp_all
chaieb@17378
   350
  then obtain "f1" where f1_def: "qelim(qe,f) = Some f1" by blast
chaieb@17378
   351
  from prems have qf1:"isqfree f1" using qelim_qfree by blast
chaieb@17378
   352
  from prems have feqf1: "\<forall> ats. qinterp ats f = qinterp ats f1"
chaieb@17378
   353
    using f1_def qf1 by blast
chaieb@17378
   354
  then  have "?F ats (QEx f) = ?F ats (QEx f1)" 
chaieb@17378
   355
    by simp 
chaieb@17378
   356
  from prems have "qelim (qe,QEx f) = Some p'" by blast
chaieb@17378
   357
  then  have "\<exists> f'. qe f1 = Some f'" using f1_def by simp
chaieb@17378
   358
  then obtain "f'" where fdef': "qe f1 = Some f'" by blast
chaieb@17378
   359
  with prems have exf1: "?F ats (QEx f1) = ?F ats f'" using qf1 by blast
chaieb@17378
   360
  have fp: "?Qe (QEx f) f'" using f1_def fdef' by simp
chaieb@17378
   361
  from prems have "?Qe (QEx f) p'" by blast 
chaieb@17378
   362
  then have "p' = f'" using fp by simp
chaieb@17378
   363
  then show ?case using feqf1 exf1 by simp
chaieb@17378
   364
next
chaieb@17378
   365
  case (QAll f)
chaieb@17378
   366
  from "QAll.prems"
chaieb@17378
   367
  have "\<exists> f0. lift_un NOT (lift_qe qe (lift_un NOT (qelim (qe ,f)))) = 
chaieb@17378
   368
    Some f0"
chaieb@17378
   369
    by (cases "lift_un NOT (lift_qe qe (lift_un NOT (qelim (qe ,f))))") 
chaieb@17378
   370
      simp_all
chaieb@17378
   371
  then obtain "f0" 
chaieb@17378
   372
    where f0_def: "lift_un NOT (lift_qe qe (lift_un NOT (qelim (qe ,f)))) = 
chaieb@17378
   373
    Some f0" by blast
chaieb@17378
   374
  then have "\<exists> f1. lift_qe qe (lift_un NOT (qelim (qe ,f))) = Some f1" 
chaieb@17378
   375
    by (cases "lift_qe qe (lift_un NOT (qelim (qe ,f)))") simp_all
chaieb@17378
   376
  then obtain "f1" where 
chaieb@17378
   377
    f1_def:"lift_qe qe (lift_un NOT (qelim (qe ,f))) = Some f1" by blast
chaieb@17378
   378
  then have "\<exists> f2. lift_un NOT (qelim (qe ,f)) = Some f2"
chaieb@17378
   379
    by (cases "qelim (qe ,f)") simp_all
chaieb@17378
   380
  then obtain "f2" 
chaieb@17378
   381
    where f2_def:"lift_un NOT (qelim (qe ,f)) = Some f2" by blast
chaieb@17378
   382
  then have "\<exists> f3. qelim(qe,f) = Some f3" by (cases "qelim(qe,f)") simp_all
chaieb@17378
   383
  then obtain "f3" where f3_def: "qelim(qe,f) = Some f3" by blast
chaieb@17378
   384
  from prems have qf3:"isqfree f3" using qelim_qfree by blast
chaieb@17378
   385
  from prems have feqf3: "\<forall> ats. qinterp ats f = qinterp ats f3"
chaieb@17378
   386
    using f3_def qf3 by blast
chaieb@17378
   387
  have f23:"f2 = NOT f3" using f2_def f3_def by simp
chaieb@17378
   388
  then have feqf2: "\<forall> ats. qinterp ats f = qinterp ats (NOT f2)"
chaieb@17378
   389
    using feqf3 by simp
chaieb@17378
   390
  have qf2: "isqfree f2" using f23 qf3 by simp
chaieb@17378
   391
  have "qe f2 = Some f1" using f1_def f2_def f23 by simp
chaieb@17378
   392
  with prems have exf2eqf1: "?F ats (QEx f2) = ?F ats f1" using qf2 by blast
chaieb@17378
   393
  have "f0 = NOT f1" using f0_def f1_def by simp
chaieb@17378
   394
  then have f0eqf1: "?F ats f0 = ?F ats (NOT f1)" by simp
chaieb@17378
   395
  from prems have "qelim (qe, QAll f) = Some p'" by blast
chaieb@17378
   396
  then have f0eqp': "p' = f0" using f0_def by simp
chaieb@17378
   397
  have "?F ats (QAll f) = (\<forall>x. ?F (x#ats) f)" by simp
chaieb@17378
   398
  also have "\<dots> = (\<not> (\<exists> x. ?F (x#ats) (NOT f)))" by simp
chaieb@17378
   399
  also have "\<dots> = (\<not> (\<exists> x. ?F (x#ats) (NOT (NOT f2))))" using feqf2
chaieb@17378
   400
    by auto
chaieb@17378
   401
  also have "\<dots> = (\<not> (\<exists> x. ?F (x#ats) f2))" by simp
chaieb@17378
   402
  also have "\<dots> = (\<not> (?F ats f1))" using exf2eqf1 by simp
chaieb@17378
   403
  finally show ?case using f0eqp' f0eqf1 by simp
chaieb@17378
   404
qed simp_all
chaieb@17378
   405
chaieb@17378
   406
(* Cooper's algorithm *)
chaieb@17378
   407
chaieb@17378
   408
chaieb@17378
   409
(* Transform an intform into NNF *)
chaieb@17378
   410
consts lgth :: "QF \<Rightarrow> nat"
chaieb@17378
   411
       nnf :: "QF \<Rightarrow> QF"    
chaieb@17378
   412
primrec
chaieb@17378
   413
"lgth (Lt it1 it2) = 1"
chaieb@17378
   414
"lgth (Gt it1 it2) = 1"
chaieb@17378
   415
"lgth (Le it1 it2) = 1"
chaieb@17378
   416
"lgth (Ge it1 it2) = 1"
chaieb@17378
   417
"lgth (Eq it1 it2) = 1"
chaieb@17378
   418
"lgth (Divides it1 it2) = 1"
chaieb@17378
   419
"lgth T = 1"
chaieb@17378
   420
"lgth F = 1"
chaieb@17378
   421
"lgth (NOT p) = 1 + lgth p"
chaieb@17378
   422
"lgth (And p q) = 1 + lgth p + lgth q"
chaieb@17378
   423
"lgth (Or p q) = 1 + lgth p + lgth q"
chaieb@17378
   424
"lgth (Imp p q) = 1 + lgth p + lgth q"
chaieb@17378
   425
"lgth (Equ p q) = 1 + lgth p + lgth q" 
chaieb@17378
   426
"lgth (QAll p) = 1 + lgth p" 
chaieb@17378
   427
"lgth (QEx p) = 1 + lgth p" 
chaieb@17378
   428
chaieb@17378
   429
lemma [simp] :"0 < lgth q"
chaieb@17378
   430
apply (induct_tac q)
chaieb@17378
   431
apply(auto)
chaieb@17378
   432
done
chaieb@17378
   433
chaieb@17378
   434
(* NNF *)
chaieb@17378
   435
recdef nnf "measure (\<lambda>p. lgth p)"
chaieb@17378
   436
  "nnf (Lt it1 it2) = Le (Sub it1 it2) (Cst (- 1))"
chaieb@17378
   437
  "nnf (Gt it1 it2) = Le (Sub it2 it1) (Cst (- 1))"
chaieb@17378
   438
  "nnf (Le it1 it2) = Le it1 it2 "
chaieb@17378
   439
  "nnf (Ge it1 it2) = Le it2 it1"
chaieb@17378
   440
  "nnf (Eq it1 it2) = Eq it2 it1"
chaieb@17378
   441
  "nnf (Divides d t) = Divides d t"
chaieb@17378
   442
  "nnf T = T"
chaieb@17378
   443
  "nnf F = F"
chaieb@17378
   444
  "nnf (And p q) = And (nnf p) (nnf q)"
chaieb@17378
   445
  "nnf (Or p q) = Or (nnf p) (nnf q)"
chaieb@17378
   446
  "nnf (Imp p q) = Or (nnf (NOT p)) (nnf q)"
chaieb@17378
   447
  "nnf (Equ p q) = Or (And (nnf p) (nnf q)) 
chaieb@17378
   448
  (And (nnf (NOT p)) (nnf (NOT q)))"
chaieb@17378
   449
  "nnf (NOT (Lt it1 it2)) = (Le it2 it1)"
chaieb@17378
   450
  "nnf (NOT (Gt it1 it2))  = (Le it1 it2)"
chaieb@17378
   451
  "nnf (NOT (Le it1 it2)) = (Le (Sub it2 it1) (Cst (- 1)))"
chaieb@17378
   452
  "nnf (NOT (Ge it1 it2)) = (Le (Sub it1 it2) (Cst (- 1)))"
chaieb@17378
   453
  "nnf (NOT (Eq it1 it2)) = (NOT (Eq it1 it2))"
chaieb@17378
   454
  "nnf (NOT (Divides d t)) = (NOT (Divides d t))"
chaieb@17378
   455
  "nnf (NOT T) = F"
chaieb@17378
   456
  "nnf (NOT F) = T"
chaieb@17378
   457
  "nnf (NOT (NOT p)) = (nnf p)"
chaieb@17378
   458
  "nnf (NOT (And p q)) = (Or (nnf (NOT p)) (nnf (NOT q)))"
chaieb@17378
   459
  "nnf (NOT (Or p q)) = (And (nnf (NOT p)) (nnf (NOT q)))"
chaieb@17378
   460
  "nnf (NOT (Imp p q)) = (And (nnf p) (nnf (NOT q)))"
chaieb@17378
   461
  "nnf (NOT (Equ p q)) = (Or (And (nnf p) (nnf (NOT q))) (And (nnf (NOT p)) (nnf q)))"
chaieb@17378
   462
chaieb@17378
   463
consts isnnf :: "QF \<Rightarrow> bool"
chaieb@17378
   464
recdef isnnf "measure (\<lambda>p. lgth p)"
chaieb@17378
   465
  "isnnf (Le it1 it2) = True"
chaieb@17378
   466
  "isnnf (Eq it1 it2) = True"
chaieb@17378
   467
  "isnnf (Divides d t) = True"
chaieb@17378
   468
  "isnnf T = True"
chaieb@17378
   469
  "isnnf F = True"
chaieb@17378
   470
  "isnnf (And p q) = (isnnf p \<and> isnnf q)"
chaieb@17378
   471
  "isnnf (Or p q) = (isnnf p \<and> isnnf q)"
chaieb@17378
   472
  "isnnf (NOT (Divides d t)) = True" 
chaieb@17378
   473
  "isnnf (NOT (Eq it1 it2)) = True" 
chaieb@17378
   474
  "isnnf p = False"
chaieb@17378
   475
chaieb@17378
   476
(* nnf preserves semantics *)
chaieb@17378
   477
lemma nnf_corr: "isqfree p \<Longrightarrow> qinterp ats p = qinterp ats (nnf p)"
chaieb@17378
   478
by (induct p rule: nnf.induct,simp_all) 
chaieb@17378
   479
(arith, arith, arith, arith, arith, arith, arith, arith, arith, blast)
chaieb@17378
   480
chaieb@17378
   481
chaieb@17378
   482
(* the result of nnf is in NNF *)
chaieb@17378
   483
lemma nnf_isnnf : "isqfree p \<Longrightarrow> isnnf (nnf p)"
chaieb@17378
   484
by (induct p rule: nnf.induct, auto)
chaieb@17378
   485
chaieb@17378
   486
lemma nnf_isqfree: "isnnf p \<Longrightarrow> isqfree p"
chaieb@17378
   487
by (induct p rule: isnnf.induct) auto
chaieb@17378
   488
chaieb@17378
   489
(* nnf preserves quantifier freeness *)
chaieb@17378
   490
lemma nnf_qfree: "isqfree p \<Longrightarrow> isqfree(nnf p)"
chaieb@17378
   491
  using nnf_isqfree nnf_isnnf by simp
chaieb@17378
   492
chaieb@17378
   493
(* Linearization and normalization of formulae *)
chaieb@17378
   494
(* Definition of linearity of an intterm *)
chaieb@17378
   495
chaieb@17378
   496
consts islinintterm :: "intterm \<Rightarrow> bool"
chaieb@17378
   497
recdef islinintterm "measure size"
chaieb@17378
   498
"islinintterm (Cst i) = True"
chaieb@17378
   499
"islinintterm (Add (Mult (Cst i) (Var n)) (Cst i')) = (i \<noteq> 0)"
chaieb@17378
   500
"islinintterm (Add (Mult (Cst i) (Var n)) (Add (Mult (Cst i') (Var n')) r)) = ( i \<noteq> 0 \<and> i' \<noteq> 0 \<and> n < n' \<and> islinintterm  (Add (Mult (Cst i') (Var n')) r))"
chaieb@17378
   501
"islinintterm i = False"
chaieb@17378
   502
chaieb@17378
   503
(* subterms of linear terms are linear *)
chaieb@17378
   504
lemma islinintterm_subt:
chaieb@17378
   505
  assumes lr: "islinintterm (Add (Mult (Cst i) (Var n)) r)"
chaieb@17378
   506
  shows "islinintterm r"
chaieb@17378
   507
using lr
chaieb@17378
   508
by (induct r rule: islinintterm.induct) auto
chaieb@17378
   509
chaieb@17378
   510
(* c \<noteq> 0 for linear term c.n + r*)
chaieb@17378
   511
lemma islinintterm_cnz:
chaieb@17378
   512
  assumes lr: "islinintterm (Add (Mult (Cst i) (Var n)) r)"
chaieb@17378
   513
  shows "i \<noteq> 0"
chaieb@17378
   514
using lr
chaieb@17378
   515
by (induct r rule: islinintterm.induct) auto
chaieb@17378
   516
chaieb@17378
   517
lemma islininttermc0r: "islinintterm (Add (Mult (Cst c) (Var n)) r) \<Longrightarrow> (c \<noteq> 0 \<and> islinintterm r)"
chaieb@17378
   518
by (induct r rule: islinintterm.induct, simp_all)
chaieb@17378
   519
chaieb@17378
   520
(* An alternative linearity definition *)
chaieb@17378
   521
consts islintn :: "(nat \<times> intterm) \<Rightarrow> bool"
chaieb@17378
   522
recdef islintn "measure (\<lambda> (n,t). (size t))"
chaieb@17378
   523
"islintn (n0, Cst i) = True"
chaieb@17378
   524
"islintn (n0, Add (Mult (Cst i) (Var n)) r) = (i \<noteq> 0 \<and> n0 \<le> n \<and> islintn (n+1,r))"
chaieb@17378
   525
"islintn (n0, t) = False"
chaieb@17378
   526
chaieb@17378
   527
constdefs islint :: "intterm \<Rightarrow> bool"
chaieb@17378
   528
  "islint t \<equiv> islintn(0,t)"
chaieb@17378
   529
chaieb@17378
   530
(* And the equivalence to the first definition *)
chaieb@17378
   531
lemma islinintterm_eq_islint: "islinintterm t = islint t"
chaieb@17378
   532
  using islint_def
chaieb@17378
   533
by (induct t rule: islinintterm.induct) auto
chaieb@17378
   534
chaieb@17378
   535
(* monotony *)
chaieb@17378
   536
lemma islintn_mon:
chaieb@17378
   537
  assumes lin: "islintn (n,t)"
chaieb@17378
   538
  and mgen: "m \<le> n"
chaieb@17378
   539
  shows "islintn(m,t)"
chaieb@17378
   540
  using lin mgen 
chaieb@17378
   541
by (induct t rule: islintn.induct) auto
chaieb@17378
   542
chaieb@17378
   543
lemma islintn_subt:
chaieb@17378
   544
  assumes lint: "islintn(n,Add (Mult (Cst i) (Var m)) r)"
chaieb@17378
   545
  shows "islintn (m+1,r)"
chaieb@17378
   546
using lint
chaieb@17378
   547
by auto
chaieb@17378
   548
chaieb@17378
   549
(* List indexin for n > 0 *)
chaieb@17378
   550
lemma nth_pos: "0 < n \<longrightarrow> (x#xs) ! n = (y#xs) ! n"
chaieb@17378
   551
using Nat.gr0_conv_Suc 
chaieb@17378
   552
by clarsimp 
chaieb@17378
   553
chaieb@17378
   554
lemma nth_pos2: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"
chaieb@17378
   555
using Nat.gr0_conv_Suc
chaieb@17378
   556
by clarsimp
chaieb@17378
   557
chaieb@17378
   558
lemma intterm_novar0: 
chaieb@17378
   559
  assumes lin: "islinintterm (Add (Mult (Cst i) (Var n)) r)"
chaieb@17378
   560
  shows "I_intterm (x#ats) r = I_intterm (y#ats) r"
chaieb@17378
   561
using lin
chaieb@17378
   562
by (induct r rule: islinintterm.induct) (simp_all add: nth_pos2)
chaieb@17378
   563
(* a simple version of a general theorem: Interpretation doese not depend 
chaieb@17378
   564
   on the first variable if it doese not occur in the term *)
chaieb@17378
   565
chaieb@17378
   566
lemma linterm_novar0:
chaieb@17378
   567
  assumes lin: "islintn (n,t)"
chaieb@17378
   568
  and npos: "0 < n"
chaieb@17378
   569
  shows "I_intterm (x#ats) t = I_intterm (y#ats) t"
chaieb@17378
   570
using lin npos
chaieb@17378
   571
by (induct n t rule: islintn.induct) (simp_all add: nth_pos2)
chaieb@17378
   572
chaieb@17378
   573
(* Periodicity of dvd *)
chaieb@17378
   574
lemma dvd_period:
chaieb@17378
   575
  assumes advdd: "(a::int) dvd d"
chaieb@17378
   576
  shows "(a dvd (x + t)) = (a dvd ((x+ c*d) + t))"
chaieb@17378
   577
using advdd  
chaieb@17378
   578
proof-
chaieb@17378
   579
  from advdd  have "\<forall>x.\<forall>k. (((a::int) dvd (x + t)) = (a dvd
chaieb@17378
   580
 (x+k*d + t)))" by (rule dvd_modd_pinf)
chaieb@17378
   581
  then show ?thesis by simp
chaieb@17378
   582
qed
chaieb@17378
   583
chaieb@17378
   584
(* lin_ad adds two linear terms*)
chaieb@17378
   585
consts lin_add :: "intterm \<times> intterm \<Rightarrow> intterm"
chaieb@17378
   586
recdef lin_add "measure (\<lambda>(x,y). ((size x) + (size y)))"
chaieb@17378
   587
"lin_add (Add (Mult (Cst c1) (Var n1)) (r1),Add (Mult (Cst c2) (Var n2)) (r2)) =
chaieb@17378
   588
  (if n1=n2 then 
chaieb@17378
   589
  (let c = Cst (c1 + c2) 
chaieb@17378
   590
   in (if c1+c2=0 then lin_add(r1,r2) else Add (Mult c (Var n1)) (lin_add (r1,r2))))
chaieb@17378
   591
  else if n1 \<le> n2 then (Add (Mult (Cst c1) (Var n1)) (lin_add (r1,Add (Mult (Cst c2) (Var n2)) (r2)))) 
chaieb@17378
   592
  else (Add (Mult (Cst c2) (Var n2)) (lin_add (Add (Mult (Cst c1) (Var n1)) r1,r2))))"
chaieb@17378
   593
"lin_add (Add (Mult (Cst c1) (Var n1)) (r1),Cst b) = 
chaieb@17378
   594
  (Add (Mult (Cst c1) (Var n1)) (lin_add (r1, Cst b)))"  
chaieb@17378
   595
"lin_add (Cst x,Add (Mult (Cst c2) (Var n2)) (r2)) = 
chaieb@17378
   596
  Add (Mult (Cst c2) (Var n2)) (lin_add (Cst x,r2))" 
chaieb@17378
   597
"lin_add (Cst b1, Cst b2) = Cst (b1+b2)"
chaieb@17378
   598
chaieb@17378
   599
lemma lin_add_cst_corr: 
chaieb@17378
   600
  assumes blin : "islintn(n0,b)"
chaieb@17378
   601
  shows "I_intterm ats (lin_add (Cst a,b)) = (I_intterm ats (Add (Cst a) b))"
chaieb@17378
   602
using blin
chaieb@17378
   603
by (induct n0 b rule: islintn.induct) auto
chaieb@17378
   604
chaieb@17378
   605
lemma lin_add_cst_corr2: 
chaieb@17378
   606
  assumes blin : "islintn(n0,b)"
chaieb@17378
   607
  shows "I_intterm ats (lin_add (b,Cst a)) = (I_intterm ats (Add b (Cst a)))"
chaieb@17378
   608
using blin
chaieb@17378
   609
by (induct n0 b rule: islintn.induct) auto
chaieb@17378
   610
chaieb@17378
   611
lemma lin_add_corrh: "\<And> n01 n02. \<lbrakk> islintn (n01,a) ; islintn (n02,b)\<rbrakk> 
chaieb@17378
   612
  \<Longrightarrow> I_intterm ats (lin_add(a,b)) = I_intterm ats (Add a b)"
chaieb@17378
   613
proof(induct a b rule: lin_add.induct)
chaieb@17378
   614
  case (58 i n r j m s) 
chaieb@17378
   615
  have "(n = m \<and> i+j = 0) \<or> (n = m \<and> i+j \<noteq> 0) \<or> n < m \<or> m < n " by arith
chaieb@17378
   616
  moreover
chaieb@17378
   617
  {assume "n=m\<and>i+j=0" hence ?case using prems by (auto simp add: sym[OF zadd_zmult_distrib]) }
chaieb@17378
   618
  moreover
chaieb@17378
   619
  {assume "n=m\<and>i+j\<noteq>0" hence ?case using prems by (auto simp add: Let_def zadd_zmult_distrib)}
chaieb@17378
   620
  moreover
chaieb@17378
   621
  {assume "n < m" hence ?case using prems by auto }
chaieb@17378
   622
  moreover
chaieb@17378
   623
  {assume "n > m" hence ?case using prems by auto }
chaieb@17378
   624
  ultimately show ?case by blast
chaieb@17378
   625
qed (auto simp add: lin_add_cst_corr lin_add_cst_corr2 Let_def)
chaieb@17378
   626
chaieb@17378
   627
(* lin_add has the semantics of Add*)
chaieb@17378
   628
lemma lin_add_corr:
chaieb@17378
   629
  assumes lina: "islinintterm a"
chaieb@17378
   630
  and linb: "islinintterm b"
chaieb@17378
   631
  shows "I_intterm ats (lin_add (a,b)) = (I_intterm ats (Add a b))"
chaieb@17378
   632
using lina linb islinintterm_eq_islint islint_def lin_add_corrh
chaieb@17378
   633
by blast
chaieb@17378
   634
chaieb@17378
   635
lemma lin_add_cst_lint:
chaieb@17378
   636
  assumes lin: "islintn (n0,b)"
chaieb@17378
   637
  shows "islintn (n0, lin_add (Cst i, b))"
chaieb@17378
   638
using lin
chaieb@17378
   639
by (induct n0 b rule: islintn.induct) auto
chaieb@17378
   640
chaieb@17378
   641
lemma lin_add_cst_lint2:
chaieb@17378
   642
  assumes lin: "islintn (n0,b)"
chaieb@17378
   643
  shows "islintn (n0, lin_add (b,Cst i))"
chaieb@17378
   644
using lin
chaieb@17378
   645
by (induct n0 b rule: islintn.induct) auto
chaieb@17378
   646
chaieb@17378
   647
(* lin_add preserves linearity..*)
chaieb@17378
   648
lemma lin_add_lint: "\<And> n0 n01 n02. \<lbrakk> islintn (n01,a) ; islintn (n02,b); n0 \<le>  min n01 n02 \<rbrakk> 
chaieb@17378
   649
  \<Longrightarrow> islintn (n0, lin_add (a,b))"
chaieb@17378
   650
proof (induct a b rule: lin_add.induct)
chaieb@17378
   651
  case (58 i n r j m s)
chaieb@17378
   652
  have "(n =m \<and> i + j = 0) \<or> (n = m \<and> i+j \<noteq> 0) \<or> n <m \<or> m < n" by arith
chaieb@17378
   653
  moreover 
chaieb@17378
   654
  { assume "n = m"
chaieb@17378
   655
      and  "i+j = 0"
chaieb@17378
   656
    hence ?case using "58" islintn_mon[where m = "n01" and n = "Suc m"]
chaieb@17378
   657
      islintn_mon[where m = "n02" and n = "Suc m"] by auto }
chaieb@17378
   658
  moreover 
chaieb@17378
   659
  { assume  "n = m"
chaieb@17378
   660
      and "i+j \<noteq> 0"
chaieb@17378
   661
    hence ?case using "58" islintn_mon[where m = "n01" and n = "Suc m"]
chaieb@17378
   662
      islintn_mon[where m = "n02" and n = "Suc m"] by (auto simp add: Let_def) }
chaieb@17378
   663
  moreover
chaieb@17378
   664
  { assume "n < m" hence ?case using 58 by force }
chaieb@17378
   665
moreover
chaieb@17378
   666
  { assume "m < n"
chaieb@17378
   667
    hence ?case using 58 
chaieb@17378
   668
      apply (auto simp add: Let_def) 
chaieb@17378
   669
      apply (erule allE[where x = "Suc m" ] )
chaieb@17378
   670
      by (erule allE[where x = "Suc m" ] ) simp }
chaieb@17378
   671
  ultimately show ?case by blast
chaieb@17378
   672
qed(simp_all add: Let_def lin_add_cst_lint lin_add_cst_lint2)
chaieb@17378
   673
chaieb@17378
   674
lemma lin_add_lin:
chaieb@17378
   675
  assumes lina: "islinintterm a"
chaieb@17378
   676
  and linb: "islinintterm b"
chaieb@17378
   677
  shows "islinintterm (lin_add (a,b))"
chaieb@17378
   678
using islinintterm_eq_islint islint_def lin_add_lint lina linb by auto
chaieb@17378
   679
chaieb@17378
   680
(* lin_mul multiplies a linear term by a constant *)
chaieb@17378
   681
consts lin_mul :: "int \<times> intterm \<Rightarrow> intterm"
chaieb@17378
   682
recdef lin_mul "measure (\<lambda>(c,t). size t)"
chaieb@17378
   683
"lin_mul (c,Cst i) = (Cst (c*i))"
chaieb@17378
   684
"lin_mul (c,Add (Mult (Cst c') (Var n)) r)  = 
chaieb@17378
   685
  (if c = 0 then (Cst 0) else
chaieb@17378
   686
  (Add (Mult (Cst (c*c')) (Var n)) (lin_mul (c,r))))"
chaieb@17378
   687
chaieb@17378
   688
lemma zmult_zadd_distrib[simp]: "(a::int) * (b+c) = a*b + a*c"
chaieb@17378
   689
proof-
chaieb@17378
   690
  have "a*(b+c) = (b+c)*a" by simp
chaieb@17378
   691
  moreover have "(b+c)*a = b*a + c*a" by (simp add: zadd_zmult_distrib)
chaieb@17378
   692
  ultimately show ?thesis by simp
chaieb@17378
   693
qed
chaieb@17378
   694
chaieb@17378
   695
(* lin_mul has the semantics of Mult *)
chaieb@17378
   696
lemma lin_mul_corr: 
chaieb@17378
   697
  assumes lint: "islinintterm  t"
chaieb@17378
   698
  shows "I_intterm ats (lin_mul (c,t)) = I_intterm ats (Mult (Cst c) t)"
chaieb@17378
   699
using lint
chaieb@17378
   700
proof (induct c t rule: lin_mul.induct)
chaieb@17378
   701
  case (21 c c' n r)
chaieb@17378
   702
  have "islinintterm (Add (Mult (Cst c') (Var n)) r)" .
chaieb@17378
   703
  then have "islinintterm r" 
chaieb@17378
   704
    by (rule islinintterm_subt[of "c'" "n" "r"])
chaieb@17378
   705
  then show ?case  using "21.hyps" "21.prems" by simp
chaieb@17378
   706
qed(auto)
chaieb@17378
   707
chaieb@17378
   708
(* lin_mul preserves linearity *)
chaieb@17378
   709
lemma lin_mul_lin:
chaieb@17378
   710
  assumes lint: "islinintterm t"
chaieb@17378
   711
  shows "islinintterm (lin_mul(c,t))"
chaieb@17378
   712
using lint
chaieb@17378
   713
by (induct t rule: islinintterm.induct) auto
chaieb@17378
   714
chaieb@17378
   715
lemma lin_mul0:
chaieb@17378
   716
  assumes lint: "islinintterm t"
chaieb@17378
   717
  shows "lin_mul(0,t) = Cst 0"
chaieb@17378
   718
  using lint
chaieb@17378
   719
  by (induct t rule: islinintterm.induct) auto
chaieb@17378
   720
chaieb@17378
   721
lemma lin_mul_lintn:
chaieb@17378
   722
  "\<And> m. islintn(m,t) \<Longrightarrow> islintn(m,lin_mul(l,t))"
chaieb@17378
   723
  by (induct l t rule: lin_mul.induct) simp_all
chaieb@17378
   724
chaieb@17378
   725
(* lin_neg neagtes a linear term *)
chaieb@17378
   726
constdefs lin_neg :: "intterm \<Rightarrow> intterm"
chaieb@17378
   727
"lin_neg i == lin_mul ((-1::int),i)"
chaieb@17378
   728
chaieb@17378
   729
(* lin_neg has the semantics of Neg *)
chaieb@17378
   730
lemma lin_neg_corr:
chaieb@17378
   731
  assumes lint: "islinintterm  t"
chaieb@17378
   732
  shows "I_intterm ats (lin_neg t) = I_intterm ats (Neg t)"
chaieb@17378
   733
  using lint lin_mul_corr
chaieb@17378
   734
  by (simp add: lin_neg_def lin_mul_corr)
chaieb@17378
   735
chaieb@17378
   736
(* lin_neg preserves linearity *)
chaieb@17378
   737
lemma lin_neg_lin:
chaieb@17378
   738
  assumes lint: "islinintterm  t"
chaieb@17378
   739
  shows "islinintterm (lin_neg t)"
chaieb@17378
   740
using lint
chaieb@17378
   741
by (simp add: lin_mul_lin lin_neg_def)
chaieb@17378
   742
chaieb@17378
   743
(* Some properties about lin_add and lin-neg should be moved above *)
chaieb@17378
   744
chaieb@17378
   745
lemma lin_neg_idemp: 
chaieb@17378
   746
  assumes lini: "islinintterm i"
chaieb@17378
   747
  shows "lin_neg (lin_neg i) = i"
chaieb@17378
   748
using lini
chaieb@17378
   749
by (induct i rule: islinintterm.induct) (auto simp add: lin_neg_def)
chaieb@17378
   750
chaieb@17378
   751
lemma lin_neg_lin_add_distrib:
chaieb@17378
   752
  assumes lina : "islinintterm a"
chaieb@17378
   753
  and linb :"islinintterm b"
chaieb@17378
   754
  shows "lin_neg (lin_add(a,b)) = lin_add (lin_neg a, lin_neg b)"
chaieb@17378
   755
using lina linb
chaieb@17378
   756
proof (induct a b rule: lin_add.induct)
chaieb@17378
   757
  case (58 c1 n1 r1 c2 n2 r2)
chaieb@17378
   758
  from prems have lincnr1:"islinintterm (Add (Mult (Cst c1) (Var n1)) r1)" by simp
chaieb@17378
   759
  have linr1: "islinintterm r1" by (rule islinintterm_subt[OF lincnr1])
chaieb@17378
   760
  from prems have lincnr2: "islinintterm (Add (Mult (Cst c2) (Var n2)) r2)" by simp
chaieb@17378
   761
  have linr2: "islinintterm r2" by (rule islinintterm_subt[OF lincnr2])
chaieb@17378
   762
  have "n1 = n2 \<or> n1 < n2 \<or> n1 > n2" by arith
chaieb@17378
   763
  show ?case using prems linr1 linr2 by (simp_all add: lin_neg_def Let_def)
chaieb@17378
   764
next
chaieb@17378
   765
  case (59 c n r b) 
chaieb@17378
   766
  from prems have lincnr: "islinintterm (Add (Mult (Cst c) (Var n)) r)" by simp
chaieb@17378
   767
  have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
chaieb@17378
   768
  show ?case using prems linr by (simp add: lin_neg_def Let_def)
chaieb@17378
   769
next
chaieb@17378
   770
  case (60 b c n r)
chaieb@17378
   771
  from prems have lincnr: "islinintterm (Add (Mult (Cst c) (Var n)) r)" by simp
chaieb@17378
   772
  have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
chaieb@17378
   773
  show ?case  using prems linr by (simp add: lin_neg_def Let_def)
chaieb@17378
   774
qed (simp_all add: lin_neg_def)
chaieb@17378
   775
chaieb@17378
   776
(* linearize tries to linearize a term *)
chaieb@17378
   777
consts linearize :: "intterm \<Rightarrow> intterm option"
chaieb@17378
   778
recdef linearize "measure (\<lambda>t. size t)"
chaieb@17378
   779
"linearize (Cst b) = Some (Cst b)"
chaieb@17378
   780
"linearize (Var n) = Some (Add (Mult (Cst 1) (Var n)) (Cst 0))"
chaieb@17378
   781
"linearize (Neg i) = lift_un lin_neg (linearize i)"
chaieb@17378
   782
 "linearize (Add i j) = lift_bin(\<lambda> x. \<lambda> y. lin_add(x,y), linearize i, linearize j)"
chaieb@17378
   783
"linearize (Sub i j) = 
chaieb@17378
   784
  lift_bin(\<lambda> x. \<lambda> y. lin_add(x,lin_neg y), linearize i, linearize j)"
chaieb@17378
   785
"linearize (Mult i j) = 
chaieb@17378
   786
  (case linearize i of
chaieb@17378
   787
  None \<Rightarrow> None
chaieb@17378
   788
  | Some li \<Rightarrow> (case li of 
chaieb@17378
   789
     Cst b \<Rightarrow> (case linearize j of
chaieb@17378
   790
      None \<Rightarrow> None
chaieb@17378
   791
     | (Some lj) \<Rightarrow> Some (lin_mul(b,lj)))
chaieb@17378
   792
  | _ \<Rightarrow> (case linearize j of
chaieb@17378
   793
      None \<Rightarrow> None
chaieb@17378
   794
    | (Some lj) \<Rightarrow> (case lj of 
chaieb@17378
   795
        Cst b \<Rightarrow> Some (lin_mul (b,li))
chaieb@17378
   796
      | _ \<Rightarrow> None))))"
chaieb@17378
   797
chaieb@17378
   798
lemma linearize_linear1:
chaieb@17378
   799
  assumes lin: "linearize t \<noteq> None"
chaieb@17378
   800
  shows "islinintterm (the (linearize t))"
chaieb@17378
   801
using lin
chaieb@17378
   802
proof (induct t rule: linearize.induct)
chaieb@17378
   803
  case (1 b) show ?case by simp  
chaieb@17378
   804
next 
chaieb@17378
   805
  case (2 n) show ?case by simp 
chaieb@17378
   806
next 
chaieb@17378
   807
  case (3 i) show ?case 
chaieb@17378
   808
    proof-
chaieb@17378
   809
    have "(linearize i = None) \<or> (\<exists>li. linearize i = Some li)" by auto
chaieb@17378
   810
    moreover 
chaieb@17378
   811
    { assume "linearize i = None" with prems have ?thesis by auto}
chaieb@17378
   812
    moreover 
chaieb@17378
   813
    { assume lini: "\<exists>li. linearize i = Some li"
chaieb@17378
   814
      from lini obtain "li" where  "linearize i = Some li" by blast
chaieb@17378
   815
      have linli: "islinintterm li" by (simp!)
chaieb@17378
   816
      moreover have "linearize (Neg i) = Some (lin_neg li)" using prems by simp
chaieb@17378
   817
      moreover from linli have "islinintterm(lin_neg li)" by (simp add: lin_neg_lin)
chaieb@17378
   818
      ultimately have ?thesis by simp
chaieb@17378
   819
    }
chaieb@17378
   820
    ultimately show ?thesis by blast
chaieb@17378
   821
  qed
chaieb@17378
   822
next 
chaieb@17378
   823
  case (4 i j) show ?case 
chaieb@17378
   824
    proof-
chaieb@17378
   825
    have "(linearize i = None) \<or> ((\<exists> li. linearize i = Some li) \<and> linearize j = None) \<or> ((\<exists> li. linearize i = Some li) \<and> (\<exists> lj. linearize j = Some lj))" by auto 
chaieb@17378
   826
    moreover 
chaieb@17378
   827
    {
chaieb@17378
   828
      assume nlini: "linearize i = None"
chaieb@17378
   829
      from nlini have "linearize (Add i j) = None" 
chaieb@17378
   830
	by (simp add: Let_def measure_def inv_image_def) then have ?thesis using prems by auto}
chaieb@17378
   831
    moreover 
chaieb@17378
   832
    { assume nlinj: "linearize j = None"
chaieb@17378
   833
	and lini: "\<exists> li. linearize i = Some li"
chaieb@17378
   834
      from nlinj lini have "linearize (Add i j) = None" 
chaieb@17378
   835
	by (simp add: Let_def measure_def inv_image_def, auto) with prems  have ?thesis by auto}
chaieb@17378
   836
    moreover 
chaieb@17378
   837
    { assume lini: "\<exists>li. linearize i = Some li"
chaieb@17378
   838
	and linj: "\<exists>lj. linearize j = Some lj"
chaieb@17378
   839
      from lini obtain "li" where  "linearize i = Some li" by blast
chaieb@17378
   840
      have linli: "islinintterm li" by (simp!)
chaieb@17378
   841
      from linj obtain "lj" where  "linearize j = Some lj" by blast
chaieb@17378
   842
      have linlj: "islinintterm lj" by (simp!)
chaieb@17378
   843
      moreover from lini linj have "linearize (Add i j) = Some (lin_add (li,lj))" 
chaieb@17378
   844
	by (simp add: measure_def inv_image_def, auto!)
chaieb@17378
   845
      moreover from linli linlj have "islinintterm(lin_add (li,lj))" by (simp add: lin_add_lin)
chaieb@17378
   846
      ultimately have ?thesis by simp  }
chaieb@17378
   847
    ultimately show ?thesis by blast
chaieb@17378
   848
  qed
chaieb@17378
   849
next 
chaieb@17378
   850
  case (5 i j)show ?case 
chaieb@17378
   851
    proof-
chaieb@17378
   852
    have "(linearize i = None) \<or> ((\<exists> li. linearize i = Some li) \<and> linearize j = None) \<or> ((\<exists> li. linearize i = Some li) \<and> (\<exists> lj. linearize j = Some lj))" by auto 
chaieb@17378
   853
    moreover 
chaieb@17378
   854
    {
chaieb@17378
   855
      assume nlini: "linearize i = None"
chaieb@17378
   856
      from nlini have "linearize (Sub i j) = None" by (simp add: Let_def measure_def inv_image_def) then have ?thesis by (auto!)
chaieb@17378
   857
    }
chaieb@17378
   858
    moreover 
chaieb@17378
   859
    {
chaieb@17378
   860
      assume lini: "\<exists> li. linearize i = Some li"
chaieb@17378
   861
	and nlinj: "linearize j = None"
chaieb@17378
   862
      from nlinj lini have "linearize (Sub i j) = None" 
chaieb@17378
   863
	by (simp add: Let_def measure_def inv_image_def, auto) then have ?thesis by (auto!)
chaieb@17378
   864
    }
chaieb@17378
   865
    moreover 
chaieb@17378
   866
    {
chaieb@17378
   867
      assume lini: "\<exists>li. linearize i = Some li"
chaieb@17378
   868
	and linj: "\<exists>lj. linearize j = Some lj"
chaieb@17378
   869
      from lini obtain "li" where  "linearize i = Some li" by blast
chaieb@17378
   870
      have linli: "islinintterm li" by (simp!)
chaieb@17378
   871
      from linj obtain "lj" where  "linearize j = Some lj" by blast
chaieb@17378
   872
      have linlj: "islinintterm lj" by (simp!)
chaieb@17378
   873
      moreover from lini linj have "linearize (Sub i j) = Some (lin_add (li,lin_neg lj))" 
chaieb@17378
   874
	by (simp add: measure_def inv_image_def, auto!)
chaieb@17378
   875
      moreover from linli linlj have "islinintterm(lin_add (li,lin_neg lj))" by (simp add: lin_add_lin lin_neg_lin)
chaieb@17378
   876
      ultimately have ?thesis by simp
chaieb@17378
   877
    }
chaieb@17378
   878
    ultimately show ?thesis by blast
chaieb@17378
   879
  qed
chaieb@17378
   880
next
chaieb@17378
   881
  case (6 i j)show ?case 
chaieb@17378
   882
    proof-
chaieb@17378
   883
      have cses: "(linearize i = None) \<or> 
chaieb@17378
   884
	((\<exists> li. linearize i = Some li) \<and> linearize j = None) \<or> 
chaieb@17378
   885
	((\<exists> li. linearize i = Some li) \<and> (\<exists> bj. linearize j = Some (Cst bj)))
chaieb@17378
   886
	\<or> ((\<exists> bi. linearize i = Some (Cst bi)) \<and> (\<exists> lj. linearize j = Some lj))
chaieb@17378
   887
	\<or> ((\<exists> li. linearize i = Some li \<and> \<not> (\<exists> bi. li = Cst bi)) \<and> (\<exists> lj. linearize j = Some lj \<and> \<not> (\<exists> bj. lj = Cst bj)))" by auto 
chaieb@17378
   888
    moreover 
chaieb@17378
   889
    {
chaieb@17378
   890
      assume nlini: "linearize i = None"
chaieb@17378
   891
      from nlini have "linearize (Mult i j) = None" 
chaieb@17378
   892
	by (simp add: Let_def measure_def inv_image_def)  
chaieb@17378
   893
      with prems have ?thesis by auto }
chaieb@17378
   894
    moreover 
chaieb@17378
   895
    {  assume lini: "\<exists> li. linearize i = Some li"
chaieb@17378
   896
	and nlinj: "linearize j = None"
chaieb@17378
   897
      from lini obtain "li" where "linearize i = Some li" by blast 
chaieb@17378
   898
      moreover from nlinj lini have "linearize (Mult i j) = None"
chaieb@17378
   899
	using prems
chaieb@17378
   900
	by (cases li ) (auto simp add: Let_def measure_def inv_image_def)
chaieb@17378
   901
      with prems have ?thesis by auto}
chaieb@17378
   902
    moreover 
chaieb@17378
   903
    { assume lini: "\<exists>li. linearize i = Some li"
chaieb@17378
   904
	and linj: "\<exists>bj. linearize j = Some (Cst bj)"
chaieb@17378
   905
      from lini obtain "li" where  li_def: "linearize i = Some li" by blast
chaieb@17378
   906
      from prems have linli: "islinintterm li" by simp
chaieb@17378
   907
      moreover 
chaieb@17378
   908
      from linj  obtain "bj" where  bj_def: "linearize j = Some (Cst bj)" by blast
chaieb@17378
   909
      have linlj: "islinintterm (Cst bj)" by simp 
chaieb@17378
   910
      moreover from lini linj prems 
chaieb@17378
   911
      have "linearize (Mult i j) = Some (lin_mul (bj,li))"
chaieb@17378
   912
	by (cases li) (auto simp add: measure_def inv_image_def)
chaieb@17378
   913
      moreover from linli linlj have "islinintterm(lin_mul (bj,li))" by (simp add: lin_mul_lin)
chaieb@17378
   914
      ultimately have ?thesis by simp  }
chaieb@17378
   915
    moreover 
chaieb@17378
   916
    { assume lini: "\<exists>bi. linearize i = Some (Cst bi)"
chaieb@17378
   917
	and linj: "\<exists>lj. linearize j = Some lj"
chaieb@17378
   918
      from lini obtain "bi" where  "linearize i = Some (Cst bi)" by blast
chaieb@17378
   919
      from prems have linli: "islinintterm (Cst bi)" by simp
chaieb@17378
   920
      moreover 
chaieb@17378
   921
      from linj  obtain "lj" where  "linearize j = Some lj" by blast
chaieb@17378
   922
      from prems have linlj: "islinintterm lj" by simp
chaieb@17378
   923
      moreover from lini linj prems have "linearize (Mult i j) = Some (lin_mul (bi,lj))" 
chaieb@17378
   924
	by (simp add: measure_def inv_image_def) 
chaieb@17378
   925
      moreover from linli linlj have "islinintterm(lin_mul (bi,lj))" by (simp add: lin_mul_lin)
chaieb@17378
   926
      ultimately have ?thesis by simp }
chaieb@17378
   927
    moreover 
chaieb@17378
   928
    { assume linc: "\<exists> li. linearize i = Some li \<and> \<not> (\<exists> bi. li = Cst bi)"
chaieb@17378
   929
	and ljnc: "\<exists> lj. linearize j = Some lj \<and> \<not> (\<exists> bj. lj = Cst bj)"
chaieb@17378
   930
      from linc obtain "li" where "linearize i = Some li \<and> \<not> (\<exists> bi. li = Cst bi)" by blast
chaieb@17378
   931
      moreover 
chaieb@17378
   932
      from ljnc obtain "lj" where "linearize j = Some lj \<and> \<not> (\<exists> bj. lj = Cst bj)" by blast
chaieb@17378
   933
      ultimately have "linearize (Mult i j) = None"
chaieb@17378
   934
	by (cases li, auto simp add: measure_def inv_image_def) (cases lj, auto)+
chaieb@17378
   935
      with prems have ?thesis by simp }
chaieb@17378
   936
    ultimately show ?thesis by blast
chaieb@17378
   937
  qed
chaieb@17378
   938
qed  
chaieb@17378
   939
chaieb@17378
   940
(* the result of linearize, when successful, is a linear term*)
chaieb@17378
   941
lemma linearize_linear: "\<And> t'. linearize t = Some t' \<Longrightarrow> islinintterm t'"
chaieb@17378
   942
proof-
chaieb@17378
   943
  fix t'
chaieb@17378
   944
  assume lint: "linearize t = Some t'"
chaieb@17378
   945
  from lint have lt: "linearize t \<noteq> None" by auto
chaieb@17378
   946
  then have "islinintterm (the (linearize t))" by (rule_tac  linearize_linear1[OF lt])
chaieb@17378
   947
  with lint show "islinintterm t'" by simp
chaieb@17378
   948
qed
chaieb@17378
   949
chaieb@17378
   950
lemma linearize_corr1: 
chaieb@17378
   951
  assumes lin: "linearize t \<noteq> None"
chaieb@17378
   952
  shows "I_intterm ats t = I_intterm ats (the (linearize t))"
chaieb@17378
   953
using lin
chaieb@17378
   954
proof (induct t rule: linearize.induct)
chaieb@17378
   955
  case (3 i) show ?case 
chaieb@17378
   956
    proof-
chaieb@17378
   957
    have "(linearize i = None) \<or> (\<exists>li. linearize i = Some li)" by auto
chaieb@17378
   958
    moreover 
chaieb@17378
   959
    {
chaieb@17378
   960
      assume "linearize i = None"
chaieb@17378
   961
      have ?thesis using prems by simp
chaieb@17378
   962
    }
chaieb@17378
   963
    moreover 
chaieb@17378
   964
    {
chaieb@17378
   965
      assume lini: "\<exists>li. linearize i = Some li"
chaieb@17378
   966
      from lini have lini2: "linearize i \<noteq> None" by simp
chaieb@17378
   967
      from lini obtain "li" where  "linearize i = Some li" by blast
chaieb@17378
   968
      from lini2 lini have "islinintterm (the (linearize i))"
chaieb@17378
   969
	by (simp add: linearize_linear1[OF lini2])
chaieb@17378
   970
      then have linli: "islinintterm li" using prems by simp
chaieb@17378
   971
      have ieqli: "I_intterm ats i = I_intterm ats li" using prems by simp
chaieb@17378
   972
      moreover have "linearize (Neg i) = Some (lin_neg li)" using prems by simp
chaieb@17378
   973
      moreover from ieqli linli have "I_intterm ats (Neg i) = I_intterm ats (lin_neg li)" by (simp add: lin_neg_corr[OF linli])
chaieb@17378
   974
      ultimately have ?thesis using prems by (simp add: lin_neg_corr)
chaieb@17378
   975
    }
chaieb@17378
   976
    ultimately show ?thesis by blast
chaieb@17378
   977
  qed
chaieb@17378
   978
next 
chaieb@17378
   979
  case (4 i j) show ?case 
chaieb@17378
   980
    proof-
chaieb@17378
   981
    have "(linearize i = None) \<or> ((\<exists> li. linearize i = Some li) \<and> linearize j = None) \<or> ((\<exists> li. linearize i = Some li) \<and> (\<exists> lj. linearize j = Some lj))" by auto 
chaieb@17378
   982
    moreover 
chaieb@17378
   983
    {
chaieb@17378
   984
      assume nlini: "linearize i = None"
chaieb@17378
   985
      from nlini have "linearize (Add i j) = None" by (simp add: Let_def measure_def inv_image_def) then have ?thesis using prems by auto
chaieb@17378
   986
    }
chaieb@17378
   987
    moreover 
chaieb@17378
   988
    {
chaieb@17378
   989
      assume nlinj: "linearize j = None"
chaieb@17378
   990
	and lini: "\<exists> li. linearize i = Some li"
chaieb@17378
   991
      from nlinj lini have "linearize (Add i j) = None" 
chaieb@17378
   992
	by (simp add: Let_def measure_def inv_image_def, auto) 
chaieb@17378
   993
      then have ?thesis using prems by auto
chaieb@17378
   994
    }
chaieb@17378
   995
    moreover 
chaieb@17378
   996
    {
chaieb@17378
   997
      assume lini: "\<exists>li. linearize i = Some li"
chaieb@17378
   998
	and linj: "\<exists>lj. linearize j = Some lj"
chaieb@17378
   999
      from lini have lini2: "linearize i \<noteq> None" by simp
chaieb@17378
  1000
      from linj have linj2: "linearize j \<noteq> None" by simp
chaieb@17378
  1001
      from lini obtain "li" where  "linearize i = Some li" by blast
chaieb@17378
  1002
      from lini2 have "islinintterm (the (linearize i))" by (simp add: linearize_linear1)
chaieb@17378
  1003
      then have linli: "islinintterm li" using prems by simp
chaieb@17378
  1004
      from linj obtain "lj" where  "linearize j = Some lj" by blast
chaieb@17378
  1005
      from linj2 have "islinintterm (the (linearize j))" by (simp add: linearize_linear1)
chaieb@17378
  1006
      then have linlj: "islinintterm lj" using prems by simp
chaieb@17378
  1007
      moreover from lini linj have "linearize (Add i j) = Some (lin_add (li,lj))"
chaieb@17378
  1008
	using prems by (simp add: measure_def inv_image_def)
chaieb@17378
  1009
      moreover from linli linlj have "I_intterm ats (lin_add (li,lj)) = I_intterm ats (Add li lj)" by (simp add: lin_add_corr)
chaieb@17378
  1010
      ultimately have ?thesis using prems by simp
chaieb@17378
  1011
    }
chaieb@17378
  1012
    ultimately show ?thesis by blast
chaieb@17378
  1013
  qed
chaieb@17378
  1014
next 
chaieb@17378
  1015
  case (5 i j)show ?case 
chaieb@17378
  1016
    proof-
chaieb@17378
  1017
    have "(linearize i = None) \<or> ((\<exists> li. linearize i = Some li) \<and> linearize j = None) \<or> ((\<exists> li. linearize i = Some li) \<and> (\<exists> lj. linearize j = Some lj))" by auto 
chaieb@17378
  1018
    moreover 
chaieb@17378
  1019
    {
chaieb@17378
  1020
      assume nlini: "linearize i = None"
chaieb@17378
  1021
      from nlini have "linearize (Sub i j) = None" by (simp add: Let_def measure_def inv_image_def) then have ?thesis using prems by auto
chaieb@17378
  1022
    }
chaieb@17378
  1023
    moreover 
chaieb@17378
  1024
    {
chaieb@17378
  1025
      assume lini: "\<exists> li. linearize i = Some li"
chaieb@17378
  1026
	and nlinj: "linearize j = None"
chaieb@17378
  1027
      from nlinj lini have "linearize (Sub i j) = None" 
chaieb@17378
  1028
	by (simp add: Let_def measure_def inv_image_def, auto) with prems have ?thesis by auto
chaieb@17378
  1029
    }
chaieb@17378
  1030
    moreover 
chaieb@17378
  1031
    {
chaieb@17378
  1032
      assume lini: "\<exists>li. linearize i = Some li"
chaieb@17378
  1033
	and linj: "\<exists>lj. linearize j = Some lj"
chaieb@17378
  1034
      from lini have lini2: "linearize i \<noteq> None" by simp
chaieb@17378
  1035
      from linj have linj2: "linearize j \<noteq> None" by simp
chaieb@17378
  1036
      from lini obtain "li" where  "linearize i = Some li" by blast
chaieb@17378
  1037
      from lini2 have "islinintterm (the (linearize i))" by (simp add: linearize_linear1)
chaieb@17378
  1038
      with prems have linli: "islinintterm li" by simp
chaieb@17378
  1039
      from linj obtain "lj" where  "linearize j = Some lj" by blast
chaieb@17378
  1040
      from linj2 have "islinintterm (the (linearize j))" by (simp add: linearize_linear1)
chaieb@17378
  1041
      with prems have linlj: "islinintterm lj" by simp
chaieb@17378
  1042
      moreover from prems have "linearize (Sub i j) = Some (lin_add (li,lin_neg lj))" 
chaieb@17378
  1043
	by (simp add: measure_def inv_image_def)
chaieb@17378
  1044
      moreover from linlj have linnlj:"islinintterm (lin_neg lj)" by (simp add: lin_neg_lin)
chaieb@17378
  1045
      moreover from linli linnlj have "I_intterm ats (lin_add (li,lin_neg lj)) = I_intterm ats (Add li (lin_neg lj))" by (simp only: lin_add_corr[OF linli linnlj])
chaieb@17378
  1046
      moreover from linli linlj linnlj have "I_intterm ats (Add li (lin_neg lj)) = I_intterm ats (Sub li lj)" 
chaieb@17378
  1047
	by (simp add: lin_neg_corr)
chaieb@17378
  1048
      ultimately have ?thesis using prems by simp    
chaieb@17378
  1049
    }
chaieb@17378
  1050
    ultimately show ?thesis by blast
chaieb@17378
  1051
  qed
chaieb@17378
  1052
next
chaieb@17378
  1053
  case (6 i j)show ?case 
chaieb@17378
  1054
    proof-
chaieb@17378
  1055
      have cses: "(linearize i = None) \<or> 
chaieb@17378
  1056
	((\<exists> li. linearize i = Some li) \<and> linearize j = None) \<or> 
chaieb@17378
  1057
	((\<exists> li. linearize i = Some li) \<and> (\<exists> bj. linearize j = Some (Cst bj)))
chaieb@17378
  1058
	\<or> ((\<exists> bi. linearize i = Some (Cst bi)) \<and> (\<exists> lj. linearize j = Some lj))
chaieb@17378
  1059
	\<or> ((\<exists> li. linearize i = Some li \<and> \<not> (\<exists> bi. li = Cst bi)) \<and> (\<exists> lj. linearize j = Some lj \<and> \<not> (\<exists> bj. lj = Cst bj)))" by auto 
chaieb@17378
  1060
    moreover 
chaieb@17378
  1061
    {
chaieb@17378
  1062
      assume nlini: "linearize i = None"
chaieb@17378
  1063
      from nlini have "linearize (Mult i j) = None" by (simp add: Let_def measure_def inv_image_def) with prems  have ?thesis by auto
chaieb@17378
  1064
    }
chaieb@17378
  1065
    moreover 
chaieb@17378
  1066
    {
chaieb@17378
  1067
      assume lini: "\<exists> li. linearize i = Some li"
chaieb@17378
  1068
	and nlinj: "linearize j = None"
chaieb@17378
  1069
chaieb@17378
  1070
      from lini obtain "li" where "linearize i = Some li" by blast 
chaieb@17378
  1071
      moreover from prems have "linearize (Mult i j) = None" 
chaieb@17378
  1072
	by (cases li) (simp_all add: Let_def measure_def inv_image_def)
chaieb@17378
  1073
      with prems have ?thesis by auto
chaieb@17378
  1074
    }
chaieb@17378
  1075
    moreover 
chaieb@17378
  1076
    {
chaieb@17378
  1077
      assume lini: "\<exists>li. linearize i = Some li"
chaieb@17378
  1078
	and linj: "\<exists>bj. linearize j = Some (Cst bj)"
chaieb@17378
  1079
      from lini have lini2: "linearize i \<noteq> None" by simp
chaieb@17378
  1080
      from linj have linj2: "linearize j \<noteq> None" by auto
chaieb@17378
  1081
      from lini obtain "li" where  "linearize i = Some li" by blast
chaieb@17378
  1082
      from lini2 have "islinintterm (the (linearize i))" by (simp add: linearize_linear1)
chaieb@17378
  1083
      with prems  have linli: "islinintterm li" by simp
chaieb@17378
  1084
      moreover 
chaieb@17378
  1085
      from linj  obtain "bj" where  "linearize j = Some (Cst bj)" by blast
chaieb@17378
  1086
      have linlj: "islinintterm (Cst bj)" by simp
chaieb@17378
  1087
      moreover from prems have "linearize (Mult i j) = Some (lin_mul (bj,li))"
chaieb@17378
  1088
 	by (cases li) (auto simp add: measure_def inv_image_def) 
chaieb@17378
  1089
      then have lm1: "I_intterm ats (the(linearize (Mult i j))) = I_intterm ats (lin_mul (bj,li))" by simp
chaieb@17378
  1090
      moreover from linli linlj have "I_intterm ats (lin_mul(bj,li)) = I_intterm ats (Mult li (Cst bj))" by (simp add: lin_mul_corr)
chaieb@17378
  1091
      with prems 
chaieb@17378
  1092
      have "I_intterm ats (lin_mul(bj,li)) = I_intterm ats (Mult li (the (linearize j)))" 
chaieb@17378
  1093
	by auto
chaieb@17378
  1094
      moreover have "I_intterm ats (Mult li (the (linearize j))) = I_intterm ats (Mult i (the (linearize j)))" using prems  by simp
chaieb@17378
  1095
      moreover have "I_intterm ats i = I_intterm ats (the (linearize i))"  
chaieb@17378
  1096
	using lini2 lini "6.hyps" by simp
chaieb@17378
  1097
	moreover have "I_intterm ats j = I_intterm ats (the (linearize j))"
chaieb@17378
  1098
	  using prems by (cases li) (auto simp add: measure_def inv_image_def)
chaieb@17378
  1099
      ultimately have ?thesis by auto }
chaieb@17378
  1100
    moreover 
chaieb@17378
  1101
    { assume lini: "\<exists>bi. linearize i = Some (Cst bi)"
chaieb@17378
  1102
	and linj: "\<exists>lj. linearize j = Some lj"
chaieb@17378
  1103
      from lini have lini2 : "linearize i \<noteq> None" by auto
chaieb@17378
  1104
      from linj have linj2 : "linearize j \<noteq> None" by auto      
chaieb@17378
  1105
      from lini obtain "bi" where  "linearize i = Some (Cst bi)" by blast
chaieb@17378
  1106
      have linli: "islinintterm (Cst bi)" using prems by simp
chaieb@17378
  1107
      moreover 
chaieb@17378
  1108
      from linj  obtain "lj" where  "linearize j = Some lj" by blast
chaieb@17378
  1109
      from linj2 have "islinintterm (the (linearize j))" by (simp add: linearize_linear1) 
chaieb@17378
  1110
      then have linlj: "islinintterm lj" by (simp!)
chaieb@17378
  1111
      moreover from linli lini linj have "linearize (Mult i j) = Some (lin_mul (bi,lj))" 	apply (simp add: measure_def inv_image_def) 
chaieb@17378
  1112
	apply auto by (case_tac "li::intterm",auto!)
chaieb@17378
  1113
      then have lm1: "I_intterm ats (the(linearize (Mult i j))) = I_intterm ats (lin_mul (bi,lj))" by simp
chaieb@17378
  1114
      moreover from linli linlj have "I_intterm ats (lin_mul(bi,lj)) = I_intterm ats (Mult (Cst bi) lj)" by (simp add: lin_mul_corr)
chaieb@17378
  1115
      then have "I_intterm ats (lin_mul(bi,lj)) = I_intterm ats (Mult (the (linearize i)) lj)" by (auto!)
chaieb@17378
  1116
      moreover have "I_intterm ats (Mult (the (linearize i)) lj) = I_intterm ats (Mult (the (linearize i)) j)" using lini lini2  by (simp!)
chaieb@17378
  1117
      moreover have "I_intterm ats i = I_intterm ats (the (linearize i))"  
chaieb@17378
  1118
	using lini2 lini "6.hyps" by simp
chaieb@17378
  1119
	moreover have "I_intterm ats j = I_intterm ats (the (linearize j))"
chaieb@17378
  1120
	  using linj linj2 lini lini2 linli linlj "6.hyps" by (auto!)
chaieb@17378
  1121
chaieb@17378
  1122
      ultimately have ?thesis by auto }
chaieb@17378
  1123
    moreover 
chaieb@17378
  1124
    { assume linc: "\<exists> li. linearize i = Some li \<and> \<not> (\<exists> bi. li = Cst bi)"
chaieb@17378
  1125
	and ljnc: "\<exists> lj. linearize j = Some lj \<and> \<not> (\<exists> bj. lj = Cst bj)"
chaieb@17378
  1126
      from linc obtain "li" where "\<exists> li. linearize i = Some li \<and> \<not> (\<exists> bi. li = Cst bi)" by blast
chaieb@17378
  1127
      moreover 
chaieb@17378
  1128
      from ljnc obtain "lj" where "\<exists> lj. linearize j = Some lj \<and> \<not> (\<exists> bj. lj = Cst bj)" by blast
chaieb@17378
  1129
      ultimately have "linearize (Mult i j) = None"
chaieb@17378
  1130
	apply (simp add: measure_def inv_image_def)
chaieb@17378
  1131
	apply (case_tac "linearize i", auto)
chaieb@17378
  1132
	apply (case_tac a)
chaieb@17378
  1133
	apply (auto!)
chaieb@17378
  1134
	by (case_tac "lj",auto)+
chaieb@17378
  1135
      then have ?thesis by (simp!) }
chaieb@17378
  1136
    ultimately show ?thesis by blast
chaieb@17378
  1137
  qed
chaieb@17378
  1138
qed  simp_all
chaieb@17378
  1139
chaieb@17378
  1140
chaieb@17378
  1141
(* linearize, when successfull, preserves semantics *)
chaieb@17378
  1142
lemma linearize_corr: "\<And> t'. linearize t = Some t' \<Longrightarrow> I_intterm ats t = I_intterm ats t' "
chaieb@17378
  1143
proof-
chaieb@17378
  1144
  fix t'
chaieb@17378
  1145
  assume lint: "linearize t = Some t'"
chaieb@17378
  1146
  show  "I_intterm ats t = I_intterm ats t'"
chaieb@17378
  1147
  proof-
chaieb@17378
  1148
    from lint have lt: "linearize t \<noteq> None" by simp 
chaieb@17378
  1149
    then have "I_intterm ats t = I_intterm ats (the (linearize t))" 
chaieb@17378
  1150
      by (rule_tac linearize_corr1[OF lt])
chaieb@17378
  1151
    with lint show ?thesis by simp
chaieb@17378
  1152
  qed
chaieb@17378
  1153
qed
chaieb@17378
  1154
chaieb@17378
  1155
(* tries to linearize a formula *)
chaieb@17378
  1156
consts linform :: "QF \<Rightarrow> QF option"
chaieb@17378
  1157
primrec
chaieb@17378
  1158
"linform (Le it1 it2) =  
chaieb@17378
  1159
  lift_bin(\<lambda>x. \<lambda>y. Le (lin_add(x,lin_neg y)) (Cst 0),linearize it1, linearize it2)"
chaieb@17378
  1160
"linform (Eq it1 it2) =  
chaieb@17378
  1161
  lift_bin(\<lambda>x. \<lambda>y. Eq (lin_add(x,lin_neg y)) (Cst 0),linearize it1, linearize it2)"
chaieb@17378
  1162
"linform (Divides d t) =  
chaieb@17378
  1163
  (case linearize d of
chaieb@17378
  1164
    None \<Rightarrow> None
chaieb@17378
  1165
   | Some ld \<Rightarrow> (case ld of
chaieb@17378
  1166
          Cst b \<Rightarrow> 
chaieb@17378
  1167
               (if (b=0) then None
chaieb@17378
  1168
               else 
chaieb@17378
  1169
                (case linearize t of 
chaieb@17378
  1170
                 None \<Rightarrow> None
chaieb@17378
  1171
               | Some lt \<Rightarrow> Some (Divides ld lt)))
chaieb@17378
  1172
         | _ \<Rightarrow> None))"
chaieb@17378
  1173
"linform  T = Some T"
chaieb@17378
  1174
"linform  F = Some F"
chaieb@17378
  1175
"linform (NOT p) = lift_un NOT (linform p)"
chaieb@17378
  1176
"linform (And p q)= lift_bin(\<lambda>f. \<lambda>g. And f g, linform p, linform q)"
chaieb@17378
  1177
"linform (Or p q) = lift_bin(\<lambda>f. \<lambda>g. Or f g, linform p, linform q)"
chaieb@17378
  1178
chaieb@17378
  1179
(* linearity of formulae *)
chaieb@17378
  1180
consts islinform :: "QF \<Rightarrow> bool"
chaieb@17378
  1181
recdef islinform "measure size"
chaieb@17378
  1182
"islinform (Le it (Cst i)) = (i=0 \<and> islinintterm it )"
chaieb@17378
  1183
"islinform (Eq it (Cst i)) = (i=0 \<and> islinintterm it)"
chaieb@17378
  1184
"islinform (Divides (Cst d) t) = (d \<noteq> 0 \<and> islinintterm t)"
chaieb@17378
  1185
"islinform  T = True"
chaieb@17378
  1186
"islinform  F = True"
chaieb@17378
  1187
"islinform (NOT (Divides (Cst d) t)) = (d \<noteq> 0 \<and> islinintterm t)"
chaieb@17378
  1188
"islinform (NOT (Eq it (Cst i))) = (i=0 \<and> islinintterm it)"
chaieb@17378
  1189
"islinform (And p q)= ((islinform p) \<and> (islinform q))"
chaieb@17378
  1190
"islinform (Or p q) = ((islinform p) \<and> (islinform q))"
chaieb@17378
  1191
"islinform p = False"
chaieb@17378
  1192
chaieb@17378
  1193
(* linform preserves nnf, if successful *)
chaieb@17378
  1194
lemma linform_nnf: 
chaieb@17378
  1195
  assumes nnfp: "isnnf p" 
chaieb@17378
  1196
  shows "\<And> p'. \<lbrakk>linform p = Some p'\<rbrakk> \<Longrightarrow> isnnf p'"
chaieb@17378
  1197
using nnfp
chaieb@17378
  1198
proof (induct p rule: isnnf.induct, simp_all)
chaieb@17378
  1199
  case (goal1 a b p')
chaieb@17378
  1200
  show ?case 
chaieb@17378
  1201
    using prems 
chaieb@17378
  1202
    by (cases "linearize a", auto) (cases "linearize b", auto)
chaieb@17378
  1203
next 
chaieb@17378
  1204
  case (goal2 a b p')
chaieb@17378
  1205
  show ?case 
chaieb@17378
  1206
    using prems 
chaieb@17378
  1207
    by (cases "linearize a", auto) (cases "linearize b", auto)
chaieb@17378
  1208
next 
chaieb@17378
  1209
  case (goal3 d t p')
chaieb@17378
  1210
  show ?case 
chaieb@17378
  1211
    using prems
chaieb@17378
  1212
    apply (cases "linearize d", auto)
chaieb@17378
  1213
    apply (case_tac "a",auto)
chaieb@17378
  1214
    apply (case_tac "int=0",auto)
chaieb@17378
  1215
    by (cases "linearize t",auto)
chaieb@17378
  1216
next
chaieb@17378
  1217
  case (goal4 f g p') show ?case 
chaieb@17378
  1218
    using prems
chaieb@17378
  1219
    by (cases "linform f", auto) (cases "linform g", auto)
chaieb@17378
  1220
next
chaieb@17378
  1221
  case (goal5 f g p') show ?case 
chaieb@17378
  1222
    using prems
chaieb@17378
  1223
    by (cases "linform f", auto) (cases "linform g", auto)
chaieb@17378
  1224
next
chaieb@17378
  1225
  case (goal6 d t p') show ?case 
chaieb@17378
  1226
    using prems
chaieb@17378
  1227
    apply (cases "linearize d", auto)
chaieb@17378
  1228
    apply (case_tac "a", auto)
chaieb@17378
  1229
    apply (case_tac "int = 0",auto)
chaieb@17378
  1230
    by (cases "linearize t", auto)
chaieb@17378
  1231
next 
chaieb@17378
  1232
  case (goal7 a b p')
chaieb@17378
  1233
  show ?case 
chaieb@17378
  1234
    using prems 
chaieb@17378
  1235
    by (cases "linearize a", auto) (cases "linearize b", auto)
chaieb@17378
  1236
chaieb@17378
  1237
chaieb@17378
  1238
qed
chaieb@17378
  1239
chaieb@17378
  1240
chaieb@17378
  1241
lemma linform_corr: "\<And> lp. \<lbrakk> isnnf p ; linform p = Some lp \<rbrakk> \<Longrightarrow> 
chaieb@17378
  1242
                     (qinterp ats p = qinterp ats lp)"
chaieb@17378
  1243
proof (induct p rule: linform.induct)
chaieb@17378
  1244
  case (Le x y)
chaieb@17378
  1245
  show ?case
chaieb@17378
  1246
    using "Le.prems"
chaieb@17378
  1247
  proof-
chaieb@17378
  1248
    have "(\<exists> lx ly. linearize x = Some lx \<and> linearize y = Some ly) \<or> 
chaieb@17378
  1249
      (linearize x = None) \<or> (linearize y = None)"by auto
chaieb@17378
  1250
    moreover 
chaieb@17378
  1251
    {
chaieb@17378
  1252
      assume linxy: "\<exists> lx ly. linearize x = Some lx \<and> linearize y = Some ly"
chaieb@17378
  1253
      from linxy obtain "lx" "ly" 
chaieb@17378
  1254
	where lxly:"linearize x = Some lx \<and> linearize y = Some ly" by blast
chaieb@17378
  1255
      then 
chaieb@17378
  1256
      have lxeqx: "I_intterm ats x = I_intterm ats lx" 
chaieb@17378
  1257
	by (simp add: linearize_corr)
chaieb@17378
  1258
      from lxly have lxlin: "islinintterm lx" 
chaieb@17378
  1259
	by (auto simp add: linearize_linear)
chaieb@17378
  1260
      from lxly have lyeqy: "I_intterm ats y = I_intterm ats ly"
chaieb@17378
  1261
	by (simp add: linearize_corr)
chaieb@17378
  1262
      from lxly have lylin: "islinintterm ly" 
chaieb@17378
  1263
	by (auto simp add: linearize_linear)
chaieb@17378
  1264
      from "prems"
chaieb@17378
  1265
      have lpeqle: "lp =  (Le (lin_add(lx,lin_neg ly)) (Cst 0))"
chaieb@17378
  1266
	by auto
chaieb@17378
  1267
      moreover
chaieb@17378
  1268
      have lin1: "islinintterm (Cst 1)" by simp
chaieb@17378
  1269
      then
chaieb@17378
  1270
      have ?thesis  
chaieb@17378
  1271
	using lxlin lylin lin1 lin_add_lin lin_neg_lin "prems" lxly lpeqle
chaieb@17378
  1272
	by (simp add: lin_add_corr lin_neg_corr lxeqx lyeqy)
chaieb@17378
  1273
      
chaieb@17378
  1274
    }
chaieb@17378
  1275
    
chaieb@17378
  1276
    moreover
chaieb@17378
  1277
    {
chaieb@17378
  1278
      assume "linearize x = None"
chaieb@17378
  1279
      have ?thesis using "prems" by simp
chaieb@17378
  1280
    }
chaieb@17378
  1281
    
chaieb@17378
  1282
    moreover
chaieb@17378
  1283
    {
chaieb@17378
  1284
      assume "linearize y = None"
chaieb@17378
  1285
      then have ?thesis using "prems"
chaieb@17378
  1286
	by (case_tac "linearize x", auto)
chaieb@17378
  1287
    }
chaieb@17378
  1288
    ultimately show ?thesis by blast
chaieb@17378
  1289
  qed
chaieb@17378
  1290
  
chaieb@17378
  1291
next 
chaieb@17378
  1292
  case (Eq x y)
chaieb@17378
  1293
  show ?case
chaieb@17378
  1294
    using "Eq.prems"
chaieb@17378
  1295
  proof-
chaieb@17378
  1296
    have "(\<exists> lx ly. linearize x = Some lx \<and> linearize y = Some ly) \<or> 
chaieb@17378
  1297
      (linearize x = None) \<or> (linearize y = None)"by auto
chaieb@17378
  1298
    moreover 
chaieb@17378
  1299
    {
chaieb@17378
  1300
      assume linxy: "\<exists> lx ly. linearize x = Some lx \<and> linearize y = Some ly"
chaieb@17378
  1301
      from linxy obtain "lx" "ly" 
chaieb@17378
  1302
	where lxly:"linearize x = Some lx \<and> linearize y = Some ly" by blast
chaieb@17378
  1303
      then 
chaieb@17378
  1304
      have lxeqx: "I_intterm ats x = I_intterm ats lx" 
chaieb@17378
  1305
	by (simp add: linearize_corr)
chaieb@17378
  1306
      from lxly have lxlin: "islinintterm lx" 
chaieb@17378
  1307
	by (auto simp add: linearize_linear)
chaieb@17378
  1308
      from lxly have lyeqy: "I_intterm ats y = I_intterm ats ly"
chaieb@17378
  1309
	by (simp add: linearize_corr)
chaieb@17378
  1310
      from lxly have lylin: "islinintterm ly" 
chaieb@17378
  1311
	by (auto simp add: linearize_linear)
chaieb@17378
  1312
      from "prems"
chaieb@17378
  1313
      have lpeqle: "lp =  (Eq (lin_add(lx,lin_neg ly)) (Cst 0))"
chaieb@17378
  1314
	by auto
chaieb@17378
  1315
      moreover
chaieb@17378
  1316
      have lin1: "islinintterm (Cst 1)" by simp
chaieb@17378
  1317
      then
chaieb@17378
  1318
      have ?thesis  
chaieb@17378
  1319
	using lxlin lylin lin1 lin_add_lin lin_neg_lin "prems" lxly lpeqle
chaieb@17378
  1320
	by (simp add: lin_add_corr lin_neg_corr lxeqx lyeqy)
chaieb@17378
  1321
      
chaieb@17378
  1322
    }
chaieb@17378
  1323
    
chaieb@17378
  1324
    moreover
chaieb@17378
  1325
    {
chaieb@17378
  1326
      assume "linearize x = None"
chaieb@17378
  1327
      have ?thesis using "prems" by simp
chaieb@17378
  1328
    }
chaieb@17378
  1329
    
chaieb@17378
  1330
    moreover
chaieb@17378
  1331
    {
chaieb@17378
  1332
      assume "linearize y = None"
chaieb@17378
  1333
      then have ?thesis using "prems"
chaieb@17378
  1334
	by (case_tac "linearize x", auto)
chaieb@17378
  1335
    }
chaieb@17378
  1336
    ultimately show ?thesis by blast
chaieb@17378
  1337
  qed
chaieb@17378
  1338
  
chaieb@17378
  1339
next 
chaieb@17378
  1340
  case (Divides d t)
chaieb@17378
  1341
  show ?case
chaieb@17378
  1342
    using "Divides.prems"
chaieb@17378
  1343
    apply (case_tac "linearize d",auto)
chaieb@17378
  1344
    apply (case_tac a, auto)
chaieb@17378
  1345
    apply (case_tac "int = 0", auto)
chaieb@17378
  1346
    apply (case_tac "linearize t", auto)
chaieb@17378
  1347
    apply (simp add: linearize_corr)
chaieb@17378
  1348
    apply (case_tac a, auto)
chaieb@17378
  1349
    apply (case_tac "int = 0", auto)
chaieb@17378
  1350
    by (case_tac "linearize t", auto simp add: linearize_corr)
chaieb@17378
  1351
next
chaieb@17378
  1352
  case (NOT f) show ?case
chaieb@17378
  1353
    using "prems"
chaieb@17378
  1354
  proof-
chaieb@17378
  1355
    have "(\<exists> lf. linform f = Some lf) \<or> (linform f = None)" by auto
chaieb@17378
  1356
    moreover 
chaieb@17378
  1357
    {
chaieb@17378
  1358
      assume linf: "\<exists> lf. linform f = Some lf"
chaieb@17378
  1359
      from prems have "isnnf (NOT f)" by simp
chaieb@17378
  1360
      then have fnnf: "isnnf f" by (cases f) auto
chaieb@17378
  1361
      from linf obtain "lf" where lf: "linform f = Some lf" by blast
chaieb@17378
  1362
      then have "lp = NOT lf" using "prems" by auto
chaieb@17378
  1363
      with "NOT.prems" "NOT.hyps" lf fnnf
chaieb@17378
  1364
      have ?case by simp
chaieb@17378
  1365
    }
chaieb@17378
  1366
    moreover 
chaieb@17378
  1367
    {
chaieb@17378
  1368
      assume "linform f = None"
chaieb@17378
  1369
      then 
chaieb@17378
  1370
      have "linform (NOT f) = None" by simp
chaieb@17378
  1371
      then 
chaieb@17378
  1372
      have ?thesis  using "NOT.prems" by simp
chaieb@17378
  1373
    }
chaieb@17378
  1374
    ultimately show ?thesis by blast
chaieb@17378
  1375
  qed
chaieb@17378
  1376
next
chaieb@17378
  1377
  case (Or f g) 
chaieb@17378
  1378
  show ?case using "Or.hyps"
chaieb@17378
  1379
  proof -
chaieb@17378
  1380
    have "((\<exists> lf. linform f = Some lf ) \<and> (\<exists> lg. linform g = Some lg)) \<or> 
chaieb@17378
  1381
      (linform f = None) \<or> (linform g = None)" by auto
chaieb@17378
  1382
    moreover
chaieb@17378
  1383
    {
chaieb@17378
  1384
      assume linf: "\<exists> lf. linform f = Some lf"
chaieb@17378
  1385
	and ling: "\<exists> lg. linform g = Some lg"
chaieb@17378
  1386
      from linf obtain "lf" where lf: "linform f = Some lf" by blast
chaieb@17378
  1387
      from ling obtain "lg" where lg: "linform g = Some lg" by blast
chaieb@17378
  1388
      from lf lg have "linform (Or f g) = Some (Or lf lg)" by simp
chaieb@17378
  1389
      then have "lp = Or lf lg" using lf lg "prems"  by simp
chaieb@17378
  1390
      with lf lg "prems" have ?thesis by simp
chaieb@17378
  1391
    }
chaieb@17378
  1392
    moreover
chaieb@17378
  1393
    {
chaieb@17378
  1394
      assume "linform f = None"
chaieb@17378
  1395
      then have ?thesis using "Or.prems"  by auto
chaieb@17378
  1396
    }
chaieb@17378
  1397
    moreover
chaieb@17378
  1398
    {
chaieb@17378
  1399
      assume "linform g = None"
chaieb@17378
  1400
      then have ?thesis using "Or.prems"  by (case_tac "linform f", auto)
chaieb@17378
  1401
      
chaieb@17378
  1402
    }
chaieb@17378
  1403
    ultimately show ?thesis by blast
chaieb@17378
  1404
  qed
chaieb@17378
  1405
next
chaieb@17378
  1406
  case (And f g) 
chaieb@17378
  1407
  show ?case using "And.hyps"
chaieb@17378
  1408
  proof -
chaieb@17378
  1409
    have "((\<exists> lf. linform f = Some lf ) \<and> (\<exists> lg. linform g = Some lg)) \<or> 
chaieb@17378
  1410
      (linform f = None) \<or> (linform g = None)" by auto
chaieb@17378
  1411
    moreover
chaieb@17378
  1412
    {
chaieb@17378
  1413
      assume linf: "\<exists> lf. linform f = Some lf"
chaieb@17378
  1414
	and ling: "\<exists> lg. linform g = Some lg"
chaieb@17378
  1415
      from linf obtain "lf" where lf: "linform f = Some lf" by blast
chaieb@17378
  1416
      from ling obtain "lg" where lg: "linform g = Some lg" by blast
chaieb@17378
  1417
      from lf lg have "linform (And f g) = Some (And lf lg)" by simp
chaieb@17378
  1418
      then have "lp = And lf lg" using lf lg "prems"  by simp
chaieb@17378
  1419
      with lf lg "prems" have ?thesis by simp
chaieb@17378
  1420
    }
chaieb@17378
  1421
    moreover
chaieb@17378
  1422
    {
chaieb@17378
  1423
      assume "linform f = None"
chaieb@17378
  1424
      then have ?thesis using "And.prems"  by auto
chaieb@17378
  1425
    }
chaieb@17378
  1426
    moreover
chaieb@17378
  1427
    {
chaieb@17378
  1428
      assume "linform g = None"
chaieb@17378
  1429
      then have ?thesis using "And.prems"  by (case_tac "linform f", auto)
chaieb@17378
  1430
      
chaieb@17378
  1431
    }
chaieb@17378
  1432
    ultimately show ?thesis by blast
chaieb@17378
  1433
  qed
chaieb@17378
  1434
chaieb@17378
  1435
qed simp_all
chaieb@17378
  1436
chaieb@17378
  1437
chaieb@17378
  1438
(* the result of linform is a linear formula *)
chaieb@17378
  1439
lemma linform_lin: "\<And> lp. \<lbrakk> isnnf p ; linform p = Some lp\<rbrakk> \<Longrightarrow> islinform lp"
chaieb@17378
  1440
proof (induct p rule: linform.induct)
chaieb@17378
  1441
   case (Le x y)
chaieb@17378
  1442
  have "((\<exists> lx. linearize x = Some lx) \<and> (\<exists> ly. linearize y = Some ly)) \<or> 
chaieb@17378
  1443
    (linearize x = None) \<or> (linearize y = None) " by clarsimp
chaieb@17378
  1444
  moreover 
chaieb@17378
  1445
  {
chaieb@17378
  1446
    assume linx: "\<exists> lx. linearize x = Some lx"
chaieb@17378
  1447
      and liny: "\<exists> ly. linearize y = Some ly"
chaieb@17378
  1448
    from linx obtain "lx" where lx: "linearize x = Some lx" by blast
chaieb@17378
  1449
    from liny obtain "ly" where ly: "linearize y = Some ly" by blast
chaieb@17378
  1450
    from lx have lxlin: "islinintterm lx" by (simp add: linearize_linear)
chaieb@17378
  1451
    from ly have lylin: "islinintterm ly" by (simp add: linearize_linear)    
chaieb@17378
  1452
    have lin1:"islinintterm (Cst 1)" by simp
chaieb@17378
  1453
    have lin0: "islinintterm (Cst 0)" by simp
chaieb@17378
  1454
    from "prems"  have "lp = Le (lin_add(lx,lin_neg ly)) (Cst 0)"
chaieb@17378
  1455
      by auto
chaieb@17378
  1456
    with lin0 lin1 lxlin lylin "prems" 
chaieb@17378
  1457
    have ?case by (simp add: lin_add_lin lin_neg_lin)
chaieb@17378
  1458
    
chaieb@17378
  1459
  }
chaieb@17378
  1460
chaieb@17378
  1461
  moreover 
chaieb@17378
  1462
  {
chaieb@17378
  1463
    assume "linearize x = None"
chaieb@17378
  1464
    then have ?case using "prems" by simp
chaieb@17378
  1465
  }
chaieb@17378
  1466
  moreover 
chaieb@17378
  1467
  {
chaieb@17378
  1468
    assume "linearize y = None"
chaieb@17378
  1469
    then have ?case using "prems" by (case_tac "linearize x",simp_all)
chaieb@17378
  1470
  }
chaieb@17378
  1471
  ultimately show ?case by blast
chaieb@17378
  1472
next
chaieb@17378
  1473
   case (Eq x y)
chaieb@17378
  1474
  have "((\<exists> lx. linearize x = Some lx) \<and> (\<exists> ly. linearize y = Some ly)) \<or> 
chaieb@17378
  1475
    (linearize x = None) \<or> (linearize y = None) " by clarsimp
chaieb@17378
  1476
  moreover 
chaieb@17378
  1477
  {
chaieb@17378
  1478
    assume linx: "\<exists> lx. linearize x = Some lx"
chaieb@17378
  1479
      and liny: "\<exists> ly. linearize y = Some ly"
chaieb@17378
  1480
    from linx obtain "lx" where lx: "linearize x = Some lx" by blast
chaieb@17378
  1481
    from liny obtain "ly" where ly: "linearize y = Some ly" by blast
chaieb@17378
  1482
    from lx have lxlin: "islinintterm lx" by (simp add: linearize_linear)
chaieb@17378
  1483
    from ly have lylin: "islinintterm ly" by (simp add: linearize_linear)    
chaieb@17378
  1484
    have lin1:"islinintterm (Cst 1)" by simp
chaieb@17378
  1485
    have lin0: "islinintterm (Cst 0)" by simp
chaieb@17378
  1486
    from "prems"  have "lp = Eq (lin_add(lx,lin_neg ly)) (Cst 0)"
chaieb@17378
  1487
      by auto
chaieb@17378
  1488
    with lin0 lin1 lxlin lylin "prems" 
chaieb@17378
  1489
    have ?case by (simp add: lin_add_lin lin_neg_lin)
chaieb@17378
  1490
    
chaieb@17378
  1491
  }
chaieb@17378
  1492
chaieb@17378
  1493
  moreover 
chaieb@17378
  1494
  {
chaieb@17378
  1495
    assume "linearize x = None"
chaieb@17378
  1496
    then have ?case using "prems" by simp
chaieb@17378
  1497
  }
chaieb@17378
  1498
  moreover 
chaieb@17378
  1499
  {
chaieb@17378
  1500
    assume "linearize y = None"
chaieb@17378
  1501
    then have ?case using "prems" by (case_tac "linearize x",simp_all)
chaieb@17378
  1502
  }
chaieb@17378
  1503
  ultimately show ?case by blast
chaieb@17378
  1504
next
chaieb@17378
  1505
   case (Divides d t)
chaieb@17378
  1506
   show ?case 
chaieb@17378
  1507
     using prems
chaieb@17378
  1508
     apply (case_tac "linearize d", auto)
chaieb@17378
  1509
     apply (case_tac a, auto)
chaieb@17378
  1510
     apply (case_tac "int = 0", auto)
chaieb@17378
  1511
chaieb@17378
  1512
     by (case_tac "linearize t",auto simp add: linearize_linear)
chaieb@17378
  1513
next
chaieb@17378
  1514
  case (Or f g)
chaieb@17378
  1515
 show ?case using "Or.hyps"
chaieb@17378
  1516
  proof -
chaieb@17378
  1517
    have "((\<exists> lf. linform f = Some lf ) \<and> (\<exists> lg. linform g = Some lg)) \<or> 
chaieb@17378
  1518
      (linform f = None) \<or> (linform g = None)" by auto
chaieb@17378
  1519
    moreover
chaieb@17378
  1520
    {
chaieb@17378
  1521
      assume linf: "\<exists> lf. linform f = Some lf"
chaieb@17378
  1522
	and ling: "\<exists> lg. linform g = Some lg"
chaieb@17378
  1523
      from linf obtain "lf" where lf: "linform f = Some lf" by blast
chaieb@17378
  1524
      from ling obtain "lg" where lg: "linform g = Some lg" by blast
chaieb@17378
  1525
      from lf lg have "linform (Or f g) = Some (Or lf lg)" by simp
chaieb@17378
  1526
      then have "lp = Or lf lg" using lf lg "prems"  by simp
chaieb@17378
  1527
      with lf lg "prems" have ?thesis by simp
chaieb@17378
  1528
    }
chaieb@17378
  1529
    moreover
chaieb@17378
  1530
    {
chaieb@17378
  1531
      assume "linform f = None"
chaieb@17378
  1532
      then have ?thesis using "Or.prems"  by auto
chaieb@17378
  1533
    }
chaieb@17378
  1534
    moreover
chaieb@17378
  1535
    {
chaieb@17378
  1536
      assume "linform g = None"
chaieb@17378
  1537
      then have ?thesis using "Or.prems"  by (case_tac "linform f", auto)
chaieb@17378
  1538
      
chaieb@17378
  1539
    }
chaieb@17378
  1540
    ultimately show ?thesis by blast
chaieb@17378
  1541
  qed
chaieb@17378
  1542
next
chaieb@17378
  1543
  case (And f g) 
chaieb@17378
  1544
  show ?case using "And.hyps"
chaieb@17378
  1545
  proof -
chaieb@17378
  1546
    have "((\<exists> lf. linform f = Some lf ) \<and> (\<exists> lg. linform g = Some lg)) \<or> 
chaieb@17378
  1547
      (linform f = None) \<or> (linform g = None)" by auto
chaieb@17378
  1548
    moreover
chaieb@17378
  1549
    {
chaieb@17378
  1550
      assume linf: "\<exists> lf. linform f = Some lf"
chaieb@17378
  1551
	and ling: "\<exists> lg. linform g = Some lg"
chaieb@17378
  1552
      from linf obtain "lf" where lf: "linform f = Some lf" by blast
chaieb@17378
  1553
      from ling obtain "lg" where lg: "linform g = Some lg" by blast
chaieb@17378
  1554
      from lf lg have "linform (And f g) = Some (And lf lg)" by simp
chaieb@17378
  1555
      then have "lp = And lf lg" using lf lg "prems"  by simp
chaieb@17378
  1556
      with lf lg "prems" have ?thesis by simp
chaieb@17378
  1557
    }
chaieb@17378
  1558
    moreover
chaieb@17378
  1559
    {
chaieb@17378
  1560
      assume "linform f = None"
chaieb@17378
  1561
      then have ?thesis using "And.prems"  by auto
chaieb@17378
  1562
    }
chaieb@17378
  1563
    moreover
chaieb@17378
  1564
    {
chaieb@17378
  1565
      assume "linform g = None"
chaieb@17378
  1566
      then have ?thesis using "And.prems"  by (case_tac "linform f", auto)
chaieb@17378
  1567
      
chaieb@17378
  1568
    }
chaieb@17378
  1569
    ultimately show ?thesis by blast
chaieb@17378
  1570
  qed
chaieb@17378
  1571
next
chaieb@17378
  1572
  case (NOT f) show ?case
chaieb@17378
  1573
    using "prems"
chaieb@17378
  1574
  proof-
chaieb@17378
  1575
    have "(\<exists> lf. linform f = Some lf) \<or> (linform f = None)" by auto
chaieb@17378
  1576
    moreover 
chaieb@17378
  1577
    {
chaieb@17378
  1578
      assume linf: "\<exists> lf. linform f = Some lf"
chaieb@17378
  1579
      from prems have "isnnf (NOT f)" by simp
chaieb@17378
  1580
      then have fnnf: "isnnf f" by (cases f) auto
chaieb@17378
  1581
      from linf obtain "lf" where lf: "linform f = Some lf" by blast
chaieb@17378
  1582
      then have "lp = NOT lf" using "prems" by auto
chaieb@17378
  1583
      with "NOT.prems" "NOT.hyps" lf fnnf
chaieb@17378
  1584
      have ?thesis 
chaieb@17378
  1585
	using fnnf
chaieb@17378
  1586
	apply (cases f, auto) 
chaieb@17378
  1587
	prefer 2
chaieb@17378
  1588
	apply (case_tac "linearize intterm1",auto)
chaieb@17378
  1589
	apply (case_tac a, auto)
chaieb@17378
  1590
	apply (case_tac "int = 0", auto)
chaieb@17378
  1591
	apply (case_tac "linearize intterm2") 
chaieb@17378
  1592
	apply (auto simp add: linearize_linear)
chaieb@17378
  1593
	apply (case_tac "linearize intterm1",auto)
chaieb@17378
  1594
	by (case_tac "linearize intterm2") 
chaieb@17378
  1595
      (auto simp add: linearize_linear lin_add_lin lin_neg_lin)
chaieb@17378
  1596
    }
chaieb@17378
  1597
    moreover 
chaieb@17378
  1598
    {
chaieb@17378
  1599
      assume "linform f = None"
chaieb@17378
  1600
      then 
chaieb@17378
  1601
      have "linform (NOT f) = None" by simp
chaieb@17378
  1602
      then 
chaieb@17378
  1603
      have ?thesis  using "NOT.prems" by simp
chaieb@17378
  1604
    }
chaieb@17378
  1605
    ultimately show ?thesis by blast
chaieb@17378
  1606
  qed
chaieb@17378
  1607
qed (simp_all)
chaieb@17378
  1608
chaieb@17378
  1609
chaieb@17378
  1610
(* linform, if successfull, preserves quantifier freeness *)
chaieb@17378
  1611
lemma linform_isnnf: "islinform p \<Longrightarrow> isnnf p"
chaieb@17378
  1612
by (induct p rule: islinform.induct) auto
chaieb@17378
  1613
chaieb@17378
  1614
lemma linform_isqfree: "islinform p \<Longrightarrow> isqfree p"
chaieb@17378
  1615
using linform_isnnf nnf_isqfree by simp
chaieb@17378
  1616
chaieb@17378
  1617
lemma linform_qfree: "\<And> p'. \<lbrakk> isnnf p ; linform p = Some p'\<rbrakk> \<Longrightarrow> isqfree p'"
chaieb@17378
  1618
using linform_isqfree linform_lin 
chaieb@17378
  1619
by simp
chaieb@17378
  1620
chaieb@17378
  1621
(* Definitions and lemmas about gcd and lcm *)
chaieb@17378
  1622
constdefs lcm :: "nat \<times> nat \<Rightarrow> nat"
chaieb@17378
  1623
  "lcm \<equiv> (\<lambda>(m,n). m*n div gcd(m,n))"
chaieb@17378
  1624
chaieb@17378
  1625
constdefs ilcm :: "int \<Rightarrow> int \<Rightarrow> int"
chaieb@17378
  1626
  "ilcm \<equiv> \<lambda>i.\<lambda>j. int (lcm(nat(abs i),nat(abs j)))"
chaieb@17378
  1627
chaieb@17378
  1628
(* ilcm_dvd12 are needed later *)
chaieb@17378
  1629
lemma lcm_dvd1: 
chaieb@17378
  1630
  assumes mpos: " m >0"
chaieb@17378
  1631
  and npos: "n>0"
chaieb@17378
  1632
  shows "m dvd (lcm(m,n))"
chaieb@17378
  1633
proof-
chaieb@17378
  1634
  have "gcd(m,n) dvd n" by simp
chaieb@17378
  1635
  then obtain "k" where "n = gcd(m,n) * k" using dvd_def by auto
chaieb@17378
  1636
  then have "m*n div gcd(m,n) = m*(gcd(m,n)*k) div gcd(m,n)" by (simp add: mult_ac)
chaieb@17378
  1637
  also have "\<dots> = m*k" using mpos npos gcd_zero by simp
chaieb@17378
  1638
  finally show ?thesis by (simp add: lcm_def)
chaieb@17378
  1639
qed
chaieb@17378
  1640
chaieb@17378
  1641
lemma lcm_dvd2: 
chaieb@17378
  1642
  assumes mpos: " m >0"
chaieb@17378
  1643
  and npos: "n>0"
chaieb@17378
  1644
  shows "n dvd (lcm(m,n))"
chaieb@17378
  1645
proof-
chaieb@17378
  1646
  have "gcd(m,n) dvd m" by simp
chaieb@17378
  1647
  then obtain "k" where "m = gcd(m,n) * k" using dvd_def by auto
chaieb@17378
  1648
  then have "m*n div gcd(m,n) = (gcd(m,n)*k)*n div gcd(m,n)" by (simp add: mult_ac)
chaieb@17378
  1649
  also have "\<dots> = n*k" using mpos npos gcd_zero by simp
chaieb@17378
  1650
  finally show ?thesis by (simp add: lcm_def)
chaieb@17378
  1651
qed
chaieb@17378
  1652
chaieb@17378
  1653
lemma ilcm_dvd1: 
chaieb@17378
  1654
assumes anz: "a \<noteq> 0" 
chaieb@17378
  1655
  and bnz: "b \<noteq> 0"
chaieb@17378
  1656
  shows "a dvd (ilcm a b)"
chaieb@17378
  1657
proof-
chaieb@17378
  1658
  let ?na = "nat (abs a)"
chaieb@17378
  1659
  let ?nb = "nat (abs b)"
chaieb@17378
  1660
  have nap: "?na >0" using anz by simp
chaieb@17378
  1661
  have nbp: "?nb >0" using bnz by simp
chaieb@17378
  1662
  from nap nbp have "?na dvd lcm(?na,?nb)" using lcm_dvd1 by simp
chaieb@17378
  1663
  thus ?thesis by (simp add: ilcm_def dvd_int_iff)
chaieb@17378
  1664
qed
chaieb@17378
  1665
chaieb@17378
  1666
chaieb@17378
  1667
lemma ilcm_dvd2: 
chaieb@17378
  1668
assumes anz: "a \<noteq> 0" 
chaieb@17378
  1669
  and bnz: "b \<noteq> 0"
chaieb@17378
  1670
  shows "b dvd (ilcm a b)"
chaieb@17378
  1671
proof-
chaieb@17378
  1672
  let ?na = "nat (abs a)"
chaieb@17378
  1673
  let ?nb = "nat (abs b)"
chaieb@17378
  1674
  have nap: "?na >0" using anz by simp
chaieb@17378
  1675
  have nbp: "?nb >0" using bnz by simp
chaieb@17378
  1676
  from nap nbp have "?nb dvd lcm(?na,?nb)" using lcm_dvd2 by simp
chaieb@17378
  1677
  thus ?thesis by (simp add: ilcm_def dvd_int_iff)
chaieb@17378
  1678
qed
chaieb@17378
  1679
chaieb@17378
  1680
lemma zdvd_self_abs1: "(d::int) dvd (abs d)"
chaieb@17378
  1681
by (case_tac "d <0", simp_all)
chaieb@17378
  1682
chaieb@17378
  1683
lemma zdvd_self_abs2: "(abs (d::int)) dvd d"
chaieb@17378
  1684
by (case_tac "d<0", simp_all)
chaieb@17378
  1685
chaieb@17378
  1686
(* lcm a b is positive for positive a and b *)
chaieb@17378
  1687
chaieb@17378
  1688
lemma lcm_pos: 
chaieb@17378
  1689
  assumes mpos: "m > 0"
chaieb@17378
  1690
  and npos: "n>0"
chaieb@17378
  1691
  shows "lcm (m,n) > 0"
chaieb@17378
  1692
chaieb@17378
  1693
proof(rule ccontr, simp add: lcm_def gcd_zero)
chaieb@17378
  1694
assume h:"m*n div gcd(m,n) = 0"
chaieb@17378
  1695
from mpos npos have "gcd (m,n) \<noteq> 0" using gcd_zero by simp
chaieb@17378
  1696
hence gcdp: "gcd(m,n) > 0" by simp
chaieb@17378
  1697
with h
chaieb@17378
  1698
have "m*n < gcd(m,n)"
chaieb@17378
  1699
  by (cases "m * n < gcd (m, n)") (auto simp add: div_if[OF gcdp, where m="m*n"])
chaieb@17378
  1700
moreover 
chaieb@17378
  1701
have "gcd(m,n) dvd m" by simp
chaieb@17378
  1702
 with mpos dvd_imp_le have t1:"gcd(m,n) \<le> m" by simp
chaieb@17378
  1703
 with npos have t1:"gcd(m,n)*n \<le> m*n" by simp
chaieb@17378
  1704
 have "gcd(m,n) \<le> gcd(m,n)*n" using npos by simp
chaieb@17378
  1705
 with t1 have "gcd(m,n) \<le> m*n" by arith
chaieb@17378
  1706
ultimately show "False" by simp
chaieb@17378
  1707
qed
chaieb@17378
  1708
chaieb@17378
  1709
lemma ilcm_pos: 
chaieb@17378
  1710
  assumes apos: " 0 < a"
chaieb@17378
  1711
  and bpos: "0 < b" 
chaieb@17378
  1712
  shows "0 < ilcm  a b"
chaieb@17378
  1713
proof-
chaieb@17378
  1714
  let ?na = "nat (abs a)"
chaieb@17378
  1715
  let ?nb = "nat (abs b)"
chaieb@17378
  1716
  have nap: "?na >0" using apos by simp
chaieb@17378
  1717
  have nbp: "?nb >0" using bpos by simp
chaieb@17378
  1718
  have "0 < lcm (?na,?nb)" by (rule lcm_pos[OF nap nbp])
chaieb@17378
  1719
  thus ?thesis by (simp add: ilcm_def)
chaieb@17378
  1720
qed
chaieb@17378
  1721
chaieb@17378
  1722
(* fomlcm computes the lcm of all c, where c is the coeffitient of Var 0 *)
chaieb@17378
  1723
consts formlcm :: &q