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