src/HOL/ex/Reflected_Presburger.thy
author nipkow
Sat Jun 23 19:33:22 2007 +0200 (2007-06-23)
changeset 23477 f4b83f03cac9
parent 23315 df3a7e9ebadb
child 23515 3e7f62e68fe4
permissions -rw-r--r--
tuned and renamed group_eq_simps and ring_eq_simps
chaieb@17378
     1
theory Reflected_Presburger
nipkow@23477
     2
imports GCD Main EfficientNat
nipkow@23477
     3
uses ("coopereif.ML") ("coopertac.ML")
nipkow@23477
     4
begin
chaieb@17378
     5
chaieb@23274
     6
lemma allpairs_set: "set (allpairs Pair xs ys) = {(x,y). x\<in> set xs \<and> y \<in> set ys}"
chaieb@23274
     7
by (induct xs) auto
chaieb@17378
     8
chaieb@17378
     9
chaieb@23274
    10
  (* generate a list from i to j*)
chaieb@23274
    11
consts iupt :: "int \<times> int \<Rightarrow> int list"
chaieb@23274
    12
recdef iupt "measure (\<lambda> (i,j). nat (j-i +1))" 
chaieb@23274
    13
  "iupt (i,j) = (if j <i then [] else (i# iupt(i+1, j)))"
chaieb@17378
    14
chaieb@23274
    15
lemma iupt_set: "set (iupt(i,j)) = {i .. j}"
chaieb@23274
    16
proof(induct rule: iupt.induct)
chaieb@23274
    17
  case (1 a b)
chaieb@23274
    18
  show ?case
chaieb@23274
    19
    using prems by (simp add: simp_from_to)
chaieb@23274
    20
qed
chaieb@17378
    21
chaieb@17378
    22
lemma nth_pos2: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"
chaieb@17378
    23
using Nat.gr0_conv_Suc
chaieb@17378
    24
by clarsimp
chaieb@17378
    25
chaieb@23274
    26
chaieb@23274
    27
lemma myl: "\<forall> (a::'a::{pordered_ab_group_add}) (b::'a). (a \<le> b) = (0 \<le> b - a)" 
chaieb@23274
    28
proof(clarify)
chaieb@23274
    29
  fix x y ::"'a"
chaieb@23274
    30
  have "(x \<le> y) = (x - y \<le> 0)" by (simp only: le_iff_diff_le_0[where a="x" and b="y"])
chaieb@23274
    31
  also have "\<dots> = (- (y - x) \<le> 0)" by simp
chaieb@23274
    32
  also have "\<dots> = (0 \<le> y - x)" by (simp only: neg_le_0_iff_le[where a="y-x"])
chaieb@23274
    33
  finally show "(x \<le> y) = (0 \<le> y - x)" .
chaieb@23274
    34
qed
chaieb@17378
    35
chaieb@23274
    36
lemma myless: "\<forall> (a::'a::{pordered_ab_group_add}) (b::'a). (a < b) = (0 < b - a)" 
chaieb@23274
    37
proof(clarify)
chaieb@23274
    38
  fix x y ::"'a"
chaieb@23274
    39
  have "(x < y) = (x - y < 0)" by (simp only: less_iff_diff_less_0[where a="x" and b="y"])
chaieb@23274
    40
  also have "\<dots> = (- (y - x) < 0)" by simp
chaieb@23274
    41
  also have "\<dots> = (0 < y - x)" by (simp only: neg_less_0_iff_less[where a="y-x"])
chaieb@23274
    42
  finally show "(x < y) = (0 < y - x)" .
chaieb@23274
    43
qed
chaieb@23274
    44
chaieb@23274
    45
lemma myeq: "\<forall> (a::'a::{pordered_ab_group_add}) (b::'a). (a = b) = (0 = b - a)"
chaieb@23274
    46
  by auto
chaieb@17378
    47
chaieb@17378
    48
(* Periodicity of dvd *)
chaieb@23315
    49
chaieb@17378
    50
lemma dvd_period:
chaieb@17378
    51
  assumes advdd: "(a::int) dvd d"
chaieb@17378
    52
  shows "(a dvd (x + t)) = (a dvd ((x+ c*d) + t))"
chaieb@23274
    53
  using advdd  
chaieb@17378
    54
proof-
chaieb@23315
    55
  {fix x k
chaieb@23315
    56
    from inf_period(3)[OF advdd, rule_format, where x=x and k="-k"]  
chaieb@23315
    57
    have " ((a::int) dvd (x + t)) = (a dvd (x+k*d + t))" by simp}
chaieb@23315
    58
  hence "\<forall>x.\<forall>k. ((a::int) dvd (x + t)) = (a dvd (x+k*d + t))"  by simp
chaieb@17378
    59
  then show ?thesis by simp
chaieb@17378
    60
qed
chaieb@17378
    61
chaieb@23274
    62
  (*********************************************************************************)
chaieb@23274
    63
  (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
chaieb@23274
    64
  (*********************************************************************************)
chaieb@23274
    65
chaieb@23274
    66
datatype num = C int | Bound nat | CX int num | Neg num | Add num num| Sub num num 
chaieb@23274
    67
  | Mul int num
chaieb@23274
    68
chaieb@23274
    69
  (* A size for num to make inductive proofs simpler*)
chaieb@23274
    70
consts num_size :: "num \<Rightarrow> nat" 
chaieb@23274
    71
primrec 
chaieb@23274
    72
  "num_size (C c) = 1"
chaieb@23274
    73
  "num_size (Bound n) = 1"
chaieb@23274
    74
  "num_size (Neg a) = 1 + num_size a"
chaieb@23274
    75
  "num_size (Add a b) = 1 + num_size a + num_size b"
chaieb@23274
    76
  "num_size (Sub a b) = 3 + num_size a + num_size b"
chaieb@23274
    77
  "num_size (CX c a) = 4 + num_size a"
chaieb@23274
    78
  "num_size (Mul c a) = 1 + num_size a"
chaieb@17378
    79
chaieb@23274
    80
consts Inum :: "int list \<Rightarrow> num \<Rightarrow> int"
chaieb@23274
    81
primrec
chaieb@23274
    82
  "Inum bs (C c) = c"
chaieb@23274
    83
  "Inum bs (Bound n) = bs!n"
chaieb@23274
    84
  "Inum bs (CX c a) = c * (bs!0) + (Inum bs a)"
chaieb@23274
    85
  "Inum bs (Neg a) = -(Inum bs a)"
chaieb@23274
    86
  "Inum bs (Add a b) = Inum bs a + Inum bs b"
chaieb@23274
    87
  "Inum bs (Sub a b) = Inum bs a - Inum bs b"
chaieb@23274
    88
  "Inum bs (Mul c a) = c* Inum bs a"
chaieb@23274
    89
chaieb@23274
    90
datatype fm  = 
chaieb@23274
    91
  T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num|
chaieb@23274
    92
  NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm 
chaieb@23274
    93
  | Closed nat | NClosed nat
chaieb@23274
    94
chaieb@23274
    95
chaieb@23274
    96
  (* A size for fm *)
chaieb@23274
    97
consts fmsize :: "fm \<Rightarrow> nat"
chaieb@23274
    98
recdef fmsize "measure size"
chaieb@23274
    99
  "fmsize (NOT p) = 1 + fmsize p"
chaieb@23274
   100
  "fmsize (And p q) = 1 + fmsize p + fmsize q"
chaieb@23274
   101
  "fmsize (Or p q) = 1 + fmsize p + fmsize q"
chaieb@23274
   102
  "fmsize (Imp p q) = 3 + fmsize p + fmsize q"
chaieb@23274
   103
  "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)"
chaieb@23274
   104
  "fmsize (E p) = 1 + fmsize p"
chaieb@23274
   105
  "fmsize (A p) = 4+ fmsize p"
chaieb@23274
   106
  "fmsize (Dvd i t) = 2"
chaieb@23274
   107
  "fmsize (NDvd i t) = 2"
chaieb@23274
   108
  "fmsize p = 1"
chaieb@23274
   109
  (* several lemmas about fmsize *)
chaieb@23274
   110
lemma fmsize_pos: "fmsize p > 0"	
chaieb@23274
   111
by (induct p rule: fmsize.induct) simp_all
chaieb@17378
   112
chaieb@23274
   113
  (* Semantics of formulae (fm) *)
chaieb@23274
   114
consts Ifm ::"bool list \<Rightarrow> int list \<Rightarrow> fm \<Rightarrow> bool"
chaieb@23274
   115
primrec
chaieb@23274
   116
  "Ifm bbs bs T = True"
chaieb@23274
   117
  "Ifm bbs bs F = False"
chaieb@23274
   118
  "Ifm bbs bs (Lt a) = (Inum bs a < 0)"
chaieb@23274
   119
  "Ifm bbs bs (Gt a) = (Inum bs a > 0)"
chaieb@23274
   120
  "Ifm bbs bs (Le a) = (Inum bs a \<le> 0)"
chaieb@23274
   121
  "Ifm bbs bs (Ge a) = (Inum bs a \<ge> 0)"
chaieb@23274
   122
  "Ifm bbs bs (Eq a) = (Inum bs a = 0)"
chaieb@23274
   123
  "Ifm bbs bs (NEq a) = (Inum bs a \<noteq> 0)"
chaieb@23274
   124
  "Ifm bbs bs (Dvd i b) = (i dvd Inum bs b)"
chaieb@23274
   125
  "Ifm bbs bs (NDvd i b) = (\<not>(i dvd Inum bs b))"
chaieb@23274
   126
  "Ifm bbs bs (NOT p) = (\<not> (Ifm bbs bs p))"
chaieb@23274
   127
  "Ifm bbs bs (And p q) = (Ifm bbs bs p \<and> Ifm bbs bs q)"
chaieb@23274
   128
  "Ifm bbs bs (Or p q) = (Ifm bbs bs p \<or> Ifm bbs bs q)"
chaieb@23274
   129
  "Ifm bbs bs (Imp p q) = ((Ifm bbs bs p) \<longrightarrow> (Ifm bbs bs q))"
chaieb@23274
   130
  "Ifm bbs bs (Iff p q) = (Ifm bbs bs p = Ifm bbs bs q)"
chaieb@23274
   131
  "Ifm bbs bs (E p) = (\<exists> x. Ifm bbs (x#bs) p)"
chaieb@23274
   132
  "Ifm bbs bs (A p) = (\<forall> x. Ifm bbs (x#bs) p)"
chaieb@23274
   133
  "Ifm bbs bs (Closed n) = bbs!n"
chaieb@23274
   134
  "Ifm bbs bs (NClosed n) = (\<not> bbs!n)"
chaieb@23274
   135
chaieb@23274
   136
lemma "Ifm bbs [] (A(Imp (Gt (Sub (Bound 0) (C 8))) (E(E(Eq(Sub(Add (Mul 3 (Bound 0)) (Mul 5 (Bound 1))) (Bound 2))))))) = P"
chaieb@23274
   137
apply simp
chaieb@23274
   138
oops
chaieb@17378
   139
chaieb@23274
   140
consts prep :: "fm \<Rightarrow> fm"
chaieb@23274
   141
recdef prep "measure fmsize"
chaieb@23274
   142
  "prep (E T) = T"
chaieb@23274
   143
  "prep (E F) = F"
chaieb@23274
   144
  "prep (E (Or p q)) = Or (prep (E p)) (prep (E q))"
chaieb@23274
   145
  "prep (E (Imp p q)) = Or (prep (E (NOT p))) (prep (E q))"
chaieb@23274
   146
  "prep (E (Iff p q)) = Or (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))" 
chaieb@23274
   147
  "prep (E (NOT (And p q))) = Or (prep (E (NOT p))) (prep (E(NOT q)))"
chaieb@23274
   148
  "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))"
chaieb@23274
   149
  "prep (E (NOT (Iff p q))) = Or (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))"
chaieb@23274
   150
  "prep (E p) = E (prep p)"
chaieb@23274
   151
  "prep (A (And p q)) = And (prep (A p)) (prep (A q))"
chaieb@23274
   152
  "prep (A p) = prep (NOT (E (NOT p)))"
chaieb@23274
   153
  "prep (NOT (NOT p)) = prep p"
chaieb@23274
   154
  "prep (NOT (And p q)) = Or (prep (NOT p)) (prep (NOT q))"
chaieb@23274
   155
  "prep (NOT (A p)) = prep (E (NOT p))"
chaieb@23274
   156
  "prep (NOT (Or p q)) = And (prep (NOT p)) (prep (NOT q))"
chaieb@23274
   157
  "prep (NOT (Imp p q)) = And (prep p) (prep (NOT q))"
chaieb@23274
   158
  "prep (NOT (Iff p q)) = Or (prep (And p (NOT q))) (prep (And (NOT p) q))"
chaieb@23274
   159
  "prep (NOT p) = NOT (prep p)"
chaieb@23274
   160
  "prep (Or p q) = Or (prep p) (prep q)"
chaieb@23274
   161
  "prep (And p q) = And (prep p) (prep q)"
chaieb@23274
   162
  "prep (Imp p q) = prep (Or (NOT p) q)"
chaieb@23274
   163
  "prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))"
chaieb@23274
   164
  "prep p = p"
chaieb@23274
   165
(hints simp add: fmsize_pos)
chaieb@23274
   166
lemma prep: "Ifm bbs bs (prep p) = Ifm bbs bs p"
chaieb@23274
   167
by (induct p arbitrary: bs rule: prep.induct, auto)
chaieb@23274
   168
chaieb@17378
   169
chaieb@23274
   170
  (* Quantifier freeness *)
chaieb@23274
   171
consts qfree:: "fm \<Rightarrow> bool"
chaieb@23274
   172
recdef qfree "measure size"
chaieb@23274
   173
  "qfree (E p) = False"
chaieb@23274
   174
  "qfree (A p) = False"
chaieb@23274
   175
  "qfree (NOT p) = qfree p" 
chaieb@23274
   176
  "qfree (And p q) = (qfree p \<and> qfree q)" 
chaieb@23274
   177
  "qfree (Or  p q) = (qfree p \<and> qfree q)" 
chaieb@23274
   178
  "qfree (Imp p q) = (qfree p \<and> qfree q)" 
chaieb@23274
   179
  "qfree (Iff p q) = (qfree p \<and> qfree q)"
chaieb@23274
   180
  "qfree p = True"
chaieb@23274
   181
chaieb@23274
   182
  (* Boundedness and substitution *)
chaieb@23274
   183
consts 
chaieb@23274
   184
  numbound0:: "num \<Rightarrow> bool" (* a num is INDEPENDENT of Bound 0 *)
chaieb@23274
   185
  bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *)
chaieb@23274
   186
  numsubst0:: "num \<Rightarrow> num \<Rightarrow> num" (* substitute a num into a num for Bound 0 *)
chaieb@23274
   187
  subst0:: "num \<Rightarrow> fm \<Rightarrow> fm" (* substitue a num into a formula for Bound 0 *)
chaieb@23274
   188
primrec
chaieb@23274
   189
  "numbound0 (C c) = True"
chaieb@23274
   190
  "numbound0 (Bound n) = (n>0)"
chaieb@23274
   191
  "numbound0 (CX i a) = False"
chaieb@23274
   192
  "numbound0 (Neg a) = numbound0 a"
chaieb@23274
   193
  "numbound0 (Add a b) = (numbound0 a \<and> numbound0 b)"
chaieb@23274
   194
  "numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)" 
chaieb@23274
   195
  "numbound0 (Mul i a) = numbound0 a"
chaieb@23274
   196
chaieb@23274
   197
lemma numbound0_I:
chaieb@23274
   198
  assumes nb: "numbound0 a"
chaieb@23274
   199
  shows "Inum (b#bs) a = Inum (b'#bs) a"
chaieb@23274
   200
using nb
chaieb@23274
   201
by (induct a rule: numbound0.induct) (auto simp add: nth_pos2)
chaieb@17378
   202
chaieb@23274
   203
primrec
chaieb@23274
   204
  "bound0 T = True"
chaieb@23274
   205
  "bound0 F = True"
chaieb@23274
   206
  "bound0 (Lt a) = numbound0 a"
chaieb@23274
   207
  "bound0 (Le a) = numbound0 a"
chaieb@23274
   208
  "bound0 (Gt a) = numbound0 a"
chaieb@23274
   209
  "bound0 (Ge a) = numbound0 a"
chaieb@23274
   210
  "bound0 (Eq a) = numbound0 a"
chaieb@23274
   211
  "bound0 (NEq a) = numbound0 a"
chaieb@23274
   212
  "bound0 (Dvd i a) = numbound0 a"
chaieb@23274
   213
  "bound0 (NDvd i a) = numbound0 a"
chaieb@23274
   214
  "bound0 (NOT p) = bound0 p"
chaieb@23274
   215
  "bound0 (And p q) = (bound0 p \<and> bound0 q)"
chaieb@23274
   216
  "bound0 (Or p q) = (bound0 p \<and> bound0 q)"
chaieb@23274
   217
  "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"
chaieb@23274
   218
  "bound0 (Iff p q) = (bound0 p \<and> bound0 q)"
chaieb@23274
   219
  "bound0 (E p) = False"
chaieb@23274
   220
  "bound0 (A p) = False"
chaieb@23274
   221
  "bound0 (Closed P) = True"
chaieb@23274
   222
  "bound0 (NClosed P) = True"
chaieb@23274
   223
lemma bound0_I:
chaieb@23274
   224
  assumes bp: "bound0 p"
chaieb@23274
   225
  shows "Ifm bbs (b#bs) p = Ifm bbs (b'#bs) p"
chaieb@23274
   226
using bp numbound0_I[where b="b" and bs="bs" and b'="b'"]
chaieb@23274
   227
by (induct p rule: bound0.induct) (auto simp add: nth_pos2)
chaieb@23274
   228
chaieb@23274
   229
primrec
chaieb@23274
   230
  "numsubst0 t (C c) = (C c)"
chaieb@23274
   231
  "numsubst0 t (Bound n) = (if n=0 then t else Bound n)"
chaieb@23274
   232
  "numsubst0 t (CX i a) = Add (Mul i t) (numsubst0 t a)"
chaieb@23274
   233
  "numsubst0 t (Neg a) = Neg (numsubst0 t a)"
chaieb@23274
   234
  "numsubst0 t (Add a b) = Add (numsubst0 t a) (numsubst0 t b)"
chaieb@23274
   235
  "numsubst0 t (Sub a b) = Sub (numsubst0 t a) (numsubst0 t b)" 
chaieb@23274
   236
  "numsubst0 t (Mul i a) = Mul i (numsubst0 t a)"
chaieb@23274
   237
chaieb@23274
   238
lemma numsubst0_I:
chaieb@23274
   239
  shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t"
chaieb@23274
   240
  by (induct t) (simp_all add: nth_pos2)
chaieb@17378
   241
chaieb@23274
   242
lemma numsubst0_I':
chaieb@23274
   243
  assumes nb: "numbound0 a"
chaieb@23274
   244
  shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t"
chaieb@23274
   245
  by (induct t) (simp_all add: nth_pos2 numbound0_I[OF nb, where b="b" and b'="b'"])
chaieb@23274
   246
chaieb@23274
   247
chaieb@23274
   248
primrec
chaieb@23274
   249
  "subst0 t T = T"
chaieb@23274
   250
  "subst0 t F = F"
chaieb@23274
   251
  "subst0 t (Lt a) = Lt (numsubst0 t a)"
chaieb@23274
   252
  "subst0 t (Le a) = Le (numsubst0 t a)"
chaieb@23274
   253
  "subst0 t (Gt a) = Gt (numsubst0 t a)"
chaieb@23274
   254
  "subst0 t (Ge a) = Ge (numsubst0 t a)"
chaieb@23274
   255
  "subst0 t (Eq a) = Eq (numsubst0 t a)"
chaieb@23274
   256
  "subst0 t (NEq a) = NEq (numsubst0 t a)"
chaieb@23274
   257
  "subst0 t (Dvd i a) = Dvd i (numsubst0 t a)"
chaieb@23274
   258
  "subst0 t (NDvd i a) = NDvd i (numsubst0 t a)"
chaieb@23274
   259
  "subst0 t (NOT p) = NOT (subst0 t p)"
chaieb@23274
   260
  "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"
chaieb@23274
   261
  "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"
chaieb@23274
   262
  "subst0 t (Imp p q) = Imp (subst0 t p) (subst0 t q)"
chaieb@23274
   263
  "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
chaieb@23274
   264
  "subst0 t (Closed P) = (Closed P)"
chaieb@23274
   265
  "subst0 t (NClosed P) = (NClosed P)"
chaieb@23274
   266
chaieb@23274
   267
lemma subst0_I: assumes qfp: "qfree p"
chaieb@23274
   268
  shows "Ifm bbs (b#bs) (subst0 a p) = Ifm bbs ((Inum (b#bs) a)#bs) p"
chaieb@23274
   269
  using qfp numsubst0_I[where b="b" and bs="bs" and a="a"]
chaieb@23274
   270
  by (induct p) (simp_all add: nth_pos2 )
chaieb@23274
   271
chaieb@23274
   272
chaieb@23274
   273
consts 
chaieb@23274
   274
  decrnum:: "num \<Rightarrow> num" 
chaieb@23274
   275
  decr :: "fm \<Rightarrow> fm"
chaieb@23274
   276
chaieb@23274
   277
recdef decrnum "measure size"
chaieb@23274
   278
  "decrnum (Bound n) = Bound (n - 1)"
chaieb@23274
   279
  "decrnum (Neg a) = Neg (decrnum a)"
chaieb@23274
   280
  "decrnum (Add a b) = Add (decrnum a) (decrnum b)"
chaieb@23274
   281
  "decrnum (Sub a b) = Sub (decrnum a) (decrnum b)"
chaieb@23274
   282
  "decrnum (Mul c a) = Mul c (decrnum a)"
chaieb@23274
   283
  "decrnum a = a"
chaieb@17378
   284
chaieb@23274
   285
recdef decr "measure size"
chaieb@23274
   286
  "decr (Lt a) = Lt (decrnum a)"
chaieb@23274
   287
  "decr (Le a) = Le (decrnum a)"
chaieb@23274
   288
  "decr (Gt a) = Gt (decrnum a)"
chaieb@23274
   289
  "decr (Ge a) = Ge (decrnum a)"
chaieb@23274
   290
  "decr (Eq a) = Eq (decrnum a)"
chaieb@23274
   291
  "decr (NEq a) = NEq (decrnum a)"
chaieb@23274
   292
  "decr (Dvd i a) = Dvd i (decrnum a)"
chaieb@23274
   293
  "decr (NDvd i a) = NDvd i (decrnum a)"
chaieb@23274
   294
  "decr (NOT p) = NOT (decr p)" 
chaieb@23274
   295
  "decr (And p q) = And (decr p) (decr q)"
chaieb@23274
   296
  "decr (Or p q) = Or (decr p) (decr q)"
chaieb@23274
   297
  "decr (Imp p q) = Imp (decr p) (decr q)"
chaieb@23274
   298
  "decr (Iff p q) = Iff (decr p) (decr q)"
chaieb@23274
   299
  "decr p = p"
chaieb@23274
   300
chaieb@23274
   301
lemma decrnum: assumes nb: "numbound0 t"
chaieb@23274
   302
  shows "Inum (x#bs) t = Inum bs (decrnum t)"
chaieb@23274
   303
  using nb by (induct t rule: decrnum.induct, simp_all add: nth_pos2)
chaieb@23274
   304
chaieb@23274
   305
lemma decr: assumes nb: "bound0 p"
chaieb@23274
   306
  shows "Ifm bbs (x#bs) p = Ifm bbs bs (decr p)"
chaieb@23274
   307
  using nb 
chaieb@23274
   308
  by (induct p rule: decr.induct, simp_all add: nth_pos2 decrnum)
chaieb@23274
   309
chaieb@23274
   310
lemma decr_qf: "bound0 p \<Longrightarrow> qfree (decr p)"
chaieb@23274
   311
by (induct p, simp_all)
chaieb@23274
   312
chaieb@23274
   313
consts 
chaieb@23274
   314
  isatom :: "fm \<Rightarrow> bool" (* test for atomicity *)
chaieb@23274
   315
recdef isatom "measure size"
chaieb@23274
   316
  "isatom T = True"
chaieb@23274
   317
  "isatom F = True"
chaieb@23274
   318
  "isatom (Lt a) = True"
chaieb@23274
   319
  "isatom (Le a) = True"
chaieb@23274
   320
  "isatom (Gt a) = True"
chaieb@23274
   321
  "isatom (Ge a) = True"
chaieb@23274
   322
  "isatom (Eq a) = True"
chaieb@23274
   323
  "isatom (NEq a) = True"
chaieb@23274
   324
  "isatom (Dvd i b) = True"
chaieb@23274
   325
  "isatom (NDvd i b) = True"
chaieb@23274
   326
  "isatom (Closed P) = True"
chaieb@23274
   327
  "isatom (NClosed P) = True"
chaieb@23274
   328
  "isatom p = False"
chaieb@17378
   329
chaieb@23274
   330
lemma numsubst0_numbound0: assumes nb: "numbound0 t"
chaieb@23274
   331
  shows "numbound0 (numsubst0 t a)"
chaieb@23274
   332
using nb by (induct a rule: numsubst0.induct, auto)
chaieb@23274
   333
chaieb@23274
   334
lemma subst0_bound0: assumes qf: "qfree p" and nb: "numbound0 t"
chaieb@23274
   335
  shows "bound0 (subst0 t p)"
chaieb@23274
   336
using qf numsubst0_numbound0[OF nb] by (induct p  rule: subst0.induct, auto)
chaieb@23274
   337
chaieb@23274
   338
lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p"
chaieb@23274
   339
by (induct p, simp_all)
chaieb@23274
   340
chaieb@23274
   341
chaieb@23274
   342
constdefs djf:: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm"
chaieb@23274
   343
  "djf f p q \<equiv> (if q=T then T else if q=F then f p else 
chaieb@23274
   344
  (let fp = f p in case fp of T \<Rightarrow> T | F \<Rightarrow> q | _ \<Rightarrow> Or (f p) q))"
chaieb@23274
   345
constdefs evaldjf:: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm"
chaieb@23274
   346
  "evaldjf f ps \<equiv> foldr (djf f) ps F"
chaieb@23274
   347
chaieb@23274
   348
lemma djf_Or: "Ifm bbs bs (djf f p q) = Ifm bbs bs (Or (f p) q)"
chaieb@23274
   349
by (cases "q=T", simp add: djf_def,cases "q=F",simp add: djf_def) 
chaieb@23274
   350
(cases "f p", simp_all add: Let_def djf_def) 
chaieb@23274
   351
chaieb@23274
   352
lemma evaldjf_ex: "Ifm bbs bs (evaldjf f ps) = (\<exists> p \<in> set ps. Ifm bbs bs (f p))"
chaieb@23274
   353
  by(induct ps, simp_all add: evaldjf_def djf_Or)
chaieb@17378
   354
chaieb@23274
   355
lemma evaldjf_bound0: 
chaieb@23274
   356
  assumes nb: "\<forall> x\<in> set xs. bound0 (f x)"
chaieb@23274
   357
  shows "bound0 (evaldjf f xs)"
chaieb@23274
   358
  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto) 
chaieb@23274
   359
chaieb@23274
   360
lemma evaldjf_qf: 
chaieb@23274
   361
  assumes nb: "\<forall> x\<in> set xs. qfree (f x)"
chaieb@23274
   362
  shows "qfree (evaldjf f xs)"
chaieb@23274
   363
  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto) 
chaieb@17378
   364
chaieb@23274
   365
consts disjuncts :: "fm \<Rightarrow> fm list"
chaieb@23274
   366
recdef disjuncts "measure size"
chaieb@23274
   367
  "disjuncts (Or p q) = (disjuncts p) @ (disjuncts q)"
chaieb@23274
   368
  "disjuncts F = []"
chaieb@23274
   369
  "disjuncts p = [p]"
chaieb@23274
   370
chaieb@23274
   371
lemma disjuncts: "(\<exists> q\<in> set (disjuncts p). Ifm bbs bs q) = Ifm bbs bs p"
chaieb@23274
   372
by(induct p rule: disjuncts.induct, auto)
chaieb@23274
   373
chaieb@23274
   374
lemma disjuncts_nb: "bound0 p \<Longrightarrow> \<forall> q\<in> set (disjuncts p). bound0 q"
chaieb@17378
   375
proof-
chaieb@23274
   376
  assume nb: "bound0 p"
chaieb@23274
   377
  hence "list_all bound0 (disjuncts p)" by (induct p rule:disjuncts.induct,auto)
chaieb@23274
   378
  thus ?thesis by (simp only: list_all_iff)
chaieb@17378
   379
qed
chaieb@17378
   380
chaieb@23274
   381
lemma disjuncts_qf: "qfree p \<Longrightarrow> \<forall> q\<in> set (disjuncts p). qfree q"
chaieb@23274
   382
proof-
chaieb@23274
   383
  assume qf: "qfree p"
chaieb@23274
   384
  hence "list_all qfree (disjuncts p)"
chaieb@23274
   385
    by (induct p rule: disjuncts.induct, auto)
chaieb@23274
   386
  thus ?thesis by (simp only: list_all_iff)
chaieb@23274
   387
qed
chaieb@17378
   388
chaieb@23274
   389
constdefs DJ :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm"
chaieb@23274
   390
  "DJ f p \<equiv> evaldjf f (disjuncts p)"
chaieb@17378
   391
chaieb@23274
   392
lemma DJ: assumes fdj: "\<forall> p q. f (Or p q) = Or (f p) (f q)"
chaieb@23274
   393
  and fF: "f F = F"
chaieb@23274
   394
  shows "Ifm bbs bs (DJ f p) = Ifm bbs bs (f p)"
chaieb@23274
   395
proof-
chaieb@23274
   396
  have "Ifm bbs bs (DJ f p) = (\<exists> q \<in> set (disjuncts p). Ifm bbs bs (f q))"
chaieb@23274
   397
    by (simp add: DJ_def evaldjf_ex) 
chaieb@23274
   398
  also have "\<dots> = Ifm bbs bs (f p)" using fdj fF by (induct p rule: disjuncts.induct, auto)
chaieb@23274
   399
  finally show ?thesis .
chaieb@23274
   400
qed
chaieb@17378
   401
chaieb@23274
   402
lemma DJ_qf: assumes 
chaieb@23274
   403
  fqf: "\<forall> p. qfree p \<longrightarrow> qfree (f p)"
chaieb@23274
   404
  shows "\<forall>p. qfree p \<longrightarrow> qfree (DJ f p) "
chaieb@23274
   405
proof(clarify)
chaieb@23274
   406
  fix  p assume qf: "qfree p"
chaieb@23274
   407
  have th: "DJ f p = evaldjf f (disjuncts p)" by (simp add: DJ_def)
chaieb@23274
   408
  from disjuncts_qf[OF qf] have "\<forall> q\<in> set (disjuncts p). qfree q" .
chaieb@23274
   409
  with fqf have th':"\<forall> q\<in> set (disjuncts p). qfree (f q)" by blast
chaieb@23274
   410
  
chaieb@23274
   411
  from evaldjf_qf[OF th'] th show "qfree (DJ f p)" by simp
chaieb@17378
   412
qed
chaieb@17378
   413
chaieb@23274
   414
lemma DJ_qe: assumes qe: "\<forall> bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bbs bs (qe p) = Ifm bbs bs (E p))"
chaieb@23274
   415
  shows "\<forall> bs p. qfree p \<longrightarrow> qfree (DJ qe p) \<and> (Ifm bbs bs ((DJ qe p)) = Ifm bbs bs (E p))"
chaieb@23274
   416
proof(clarify)
chaieb@23274
   417
  fix p::fm and bs
chaieb@23274
   418
  assume qf: "qfree p"
chaieb@23274
   419
  from qe have qth: "\<forall> p. qfree p \<longrightarrow> qfree (qe p)" by blast
chaieb@23274
   420
  from DJ_qf[OF qth] qf have qfth:"qfree (DJ qe p)" by auto
chaieb@23274
   421
  have "Ifm bbs bs (DJ qe p) = (\<exists> q\<in> set (disjuncts p). Ifm bbs bs (qe q))"
chaieb@23274
   422
    by (simp add: DJ_def evaldjf_ex)
chaieb@23274
   423
  also have "\<dots> = (\<exists> q \<in> set(disjuncts p). Ifm bbs bs (E q))" using qe disjuncts_qf[OF qf] by auto
chaieb@23274
   424
  also have "\<dots> = Ifm bbs bs (E p)" by (induct p rule: disjuncts.induct, auto)
chaieb@23274
   425
  finally show "qfree (DJ qe p) \<and> Ifm bbs bs (DJ qe p) = Ifm bbs bs (E p)" using qfth by blast
chaieb@23274
   426
qed
chaieb@23274
   427
  (* Simplification *)
chaieb@23274
   428
chaieb@23274
   429
  (* Algebraic simplifications for nums *)
chaieb@23274
   430
consts bnds:: "num \<Rightarrow> nat list"
chaieb@23274
   431
  lex_ns:: "nat list \<times> nat list \<Rightarrow> bool"
chaieb@23274
   432
recdef bnds "measure size"
chaieb@23274
   433
  "bnds (Bound n) = [n]"
chaieb@23274
   434
  "bnds (CX c a) = 0#(bnds a)"
chaieb@23274
   435
  "bnds (Neg a) = bnds a"
chaieb@23274
   436
  "bnds (Add a b) = (bnds a)@(bnds b)"
chaieb@23274
   437
  "bnds (Sub a b) = (bnds a)@(bnds b)"
chaieb@23274
   438
  "bnds (Mul i a) = bnds a"
chaieb@23274
   439
  "bnds a = []"
chaieb@23274
   440
recdef lex_ns "measure (\<lambda> (xs,ys). length xs + length ys)"
chaieb@23274
   441
  "lex_ns ([], ms) = True"
chaieb@23274
   442
  "lex_ns (ns, []) = False"
chaieb@23274
   443
  "lex_ns (n#ns, m#ms) = (n<m \<or> ((n = m) \<and> lex_ns (ns,ms))) "
chaieb@23274
   444
constdefs lex_bnd :: "num \<Rightarrow> num \<Rightarrow> bool"
chaieb@23274
   445
  "lex_bnd t s \<equiv> lex_ns (bnds t, bnds s)"
chaieb@23274
   446
chaieb@23274
   447
consts simpnum:: "num \<Rightarrow> num"
chaieb@23274
   448
  numadd:: "num \<times> num \<Rightarrow> num"
chaieb@23274
   449
  nummul:: "num \<Rightarrow> int \<Rightarrow> num"
chaieb@23274
   450
  numfloor:: "num \<Rightarrow> num"
chaieb@23274
   451
recdef numadd "measure (\<lambda> (t,s). size t + size s)"
chaieb@23274
   452
  "numadd (Add (Mul c1 (Bound n1)) r1,Add (Mul c2 (Bound n2)) r2) =
chaieb@23274
   453
  (if n1=n2 then 
chaieb@23274
   454
  (let c = c1 + c2
chaieb@23274
   455
  in (if c=0 then numadd(r1,r2) else Add (Mul c (Bound n1)) (numadd (r1,r2))))
chaieb@23274
   456
  else if n1 \<le> n2 then (Add (Mul c1 (Bound n1)) (numadd (r1,Add (Mul c2 (Bound n2)) r2))) 
chaieb@23274
   457
  else (Add (Mul c2 (Bound n2)) (numadd (Add (Mul c1 (Bound n1)) r1,r2))))"
chaieb@23274
   458
  "numadd (Add (Mul c1 (Bound n1)) r1,t) = Add (Mul c1 (Bound n1)) (numadd (r1, t))"  
chaieb@23274
   459
  "numadd (t,Add (Mul c2 (Bound n2)) r2) = Add (Mul c2 (Bound n2)) (numadd (t,r2))" 
chaieb@23274
   460
  "numadd (C b1, C b2) = C (b1+b2)"
chaieb@23274
   461
  "numadd (a,b) = Add a b"
chaieb@23274
   462
chaieb@23274
   463
lemma numadd: "Inum bs (numadd (t,s)) = Inum bs (Add t s)"
chaieb@23274
   464
apply (induct t s rule: numadd.induct, simp_all add: Let_def)
chaieb@23274
   465
apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
nipkow@23477
   466
 apply (case_tac "n1 = n2")
nipkow@23477
   467
  apply(simp_all add: ring_simps)
nipkow@23477
   468
apply(simp add: left_distrib[symmetric])
nipkow@23477
   469
done
chaieb@23274
   470
chaieb@23274
   471
lemma numadd_nb: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
chaieb@23274
   472
by (induct t s rule: numadd.induct, auto simp add: Let_def)
chaieb@23274
   473
chaieb@23274
   474
recdef nummul "measure size"
chaieb@23274
   475
  "nummul (C j) = (\<lambda> i. C (i*j))"
chaieb@23274
   476
  "nummul (Add a b) = (\<lambda> i. numadd (nummul a i, nummul b i))"
chaieb@23274
   477
  "nummul (Mul c t) = (\<lambda> i. nummul t (i*c))"
chaieb@23274
   478
  "nummul t = (\<lambda> i. Mul i t)"
chaieb@23274
   479
chaieb@23274
   480
lemma nummul: "\<And> i. Inum bs (nummul t i) = Inum bs (Mul i t)"
nipkow@23477
   481
by (induct t rule: nummul.induct, auto simp add: ring_simps numadd)
chaieb@23274
   482
chaieb@23274
   483
lemma nummul_nb: "\<And> i. numbound0 t \<Longrightarrow> numbound0 (nummul t i)"
chaieb@23274
   484
by (induct t rule: nummul.induct, auto simp add: numadd_nb)
chaieb@23274
   485
chaieb@23274
   486
constdefs numneg :: "num \<Rightarrow> num"
chaieb@23274
   487
  "numneg t \<equiv> nummul t (- 1)"
chaieb@23274
   488
chaieb@23274
   489
constdefs numsub :: "num \<Rightarrow> num \<Rightarrow> num"
chaieb@23274
   490
  "numsub s t \<equiv> (if s = t then C 0 else numadd (s,numneg t))"
chaieb@23274
   491
chaieb@23274
   492
lemma numneg: "Inum bs (numneg t) = Inum bs (Neg t)"
chaieb@23274
   493
using numneg_def nummul by simp
chaieb@23274
   494
chaieb@23274
   495
lemma numneg_nb: "numbound0 t \<Longrightarrow> numbound0 (numneg t)"
chaieb@23274
   496
using numneg_def nummul_nb by simp
chaieb@23274
   497
chaieb@23274
   498
lemma numsub: "Inum bs (numsub a b) = Inum bs (Sub a b)"
chaieb@23274
   499
using numneg numadd numsub_def by simp
chaieb@23274
   500
chaieb@23274
   501
lemma numsub_nb: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numsub t s)"
chaieb@23274
   502
using numsub_def numadd_nb numneg_nb by simp
chaieb@23274
   503
chaieb@23274
   504
recdef simpnum "measure size"
chaieb@23274
   505
  "simpnum (C j) = C j"
chaieb@23274
   506
  "simpnum (Bound n) = Add (Mul 1 (Bound n)) (C 0)"
chaieb@23274
   507
  "simpnum (Neg t) = numneg (simpnum t)"
chaieb@23274
   508
  "simpnum (Add t s) = numadd (simpnum t,simpnum s)"
chaieb@23274
   509
  "simpnum (Sub t s) = numsub (simpnum t) (simpnum s)"
chaieb@23274
   510
  "simpnum (Mul i t) = (if i = 0 then (C 0) else nummul (simpnum t) i)"
chaieb@23274
   511
  "simpnum t = t"
chaieb@23274
   512
chaieb@23274
   513
lemma simpnum_ci: "Inum bs (simpnum t) = Inum bs t"
chaieb@23274
   514
by (induct t rule: simpnum.induct, auto simp add: numneg numadd numsub nummul)
chaieb@23274
   515
chaieb@23274
   516
lemma simpnum_numbound0: 
chaieb@23274
   517
  "numbound0 t \<Longrightarrow> numbound0 (simpnum t)"
chaieb@23274
   518
by (induct t rule: simpnum.induct, auto simp add: numadd_nb numsub_nb nummul_nb numneg_nb)
chaieb@23274
   519
chaieb@23274
   520
consts not:: "fm \<Rightarrow> fm"
chaieb@23274
   521
recdef not "measure size"
chaieb@23274
   522
  "not (NOT p) = p"
chaieb@23274
   523
  "not T = F"
chaieb@23274
   524
  "not F = T"
chaieb@23274
   525
  "not p = NOT p"
chaieb@23274
   526
lemma not: "Ifm bbs bs (not p) = Ifm bbs bs (NOT p)"
chaieb@23274
   527
by (cases p) auto
chaieb@23274
   528
lemma not_qf: "qfree p \<Longrightarrow> qfree (not p)"
chaieb@23274
   529
by (cases p, auto)
chaieb@23274
   530
lemma not_bn: "bound0 p \<Longrightarrow> bound0 (not p)"
chaieb@23274
   531
by (cases p, auto)
chaieb@23274
   532
chaieb@23274
   533
constdefs conj :: "fm \<Rightarrow> fm \<Rightarrow> fm"
chaieb@23274
   534
  "conj p q \<equiv> (if (p = F \<or> q=F) then F else if p=T then q else if q=T then p else And p q)"
chaieb@23274
   535
lemma conj: "Ifm bbs bs (conj p q) = Ifm bbs bs (And p q)"
chaieb@23274
   536
by (cases "p=F \<or> q=F",simp_all add: conj_def) (cases p,simp_all)
chaieb@23274
   537
chaieb@23274
   538
lemma conj_qf: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (conj p q)"
chaieb@23274
   539
using conj_def by auto 
chaieb@23274
   540
lemma conj_nb: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (conj p q)"
chaieb@23274
   541
using conj_def by auto 
chaieb@23274
   542
chaieb@23274
   543
constdefs disj :: "fm \<Rightarrow> fm \<Rightarrow> fm"
chaieb@23274
   544
  "disj p q \<equiv> (if (p = T \<or> q=T) then T else if p=F then q else if q=F then p else Or p q)"
chaieb@23274
   545
chaieb@23274
   546
lemma disj: "Ifm bbs bs (disj p q) = Ifm bbs bs (Or p q)"
chaieb@23274
   547
by (cases "p=T \<or> q=T",simp_all add: disj_def) (cases p,simp_all)
chaieb@23274
   548
lemma disj_qf: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (disj p q)"
chaieb@23274
   549
using disj_def by auto 
chaieb@23274
   550
lemma disj_nb: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (disj p q)"
chaieb@23274
   551
using disj_def by auto 
chaieb@23274
   552
chaieb@23274
   553
constdefs   imp :: "fm \<Rightarrow> fm \<Rightarrow> fm"
chaieb@23274
   554
  "imp p q \<equiv> (if (p = F \<or> q=T) then T else if p=T then q else if q=F then not p else Imp p q)"
chaieb@23274
   555
lemma imp: "Ifm bbs bs (imp p q) = Ifm bbs bs (Imp p q)"
chaieb@23274
   556
by (cases "p=F \<or> q=T",simp_all add: imp_def,cases p) (simp_all add: not)
chaieb@23274
   557
lemma imp_qf: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (imp p q)"
chaieb@23274
   558
using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def,cases p) (simp_all add: not_qf) 
chaieb@23274
   559
lemma imp_nb: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (imp p q)"
chaieb@23274
   560
using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def,cases p) simp_all
chaieb@23274
   561
chaieb@23274
   562
constdefs   iff :: "fm \<Rightarrow> fm \<Rightarrow> fm"
chaieb@23274
   563
  "iff p q \<equiv> (if (p = q) then T else if (p = not q \<or> not p = q) then F else 
chaieb@23274
   564
       if p=F then not q else if q=F then not p else if p=T then q else if q=T then p else 
chaieb@23274
   565
  Iff p q)"
chaieb@23274
   566
lemma iff: "Ifm bbs bs (iff p q) = Ifm bbs bs (Iff p q)"
chaieb@23274
   567
  by (unfold iff_def,cases "p=q", simp,cases "p=not q", simp add:not) 
chaieb@23274
   568
(cases "not p= q", auto simp add:not)
chaieb@23274
   569
lemma iff_qf: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (iff p q)"
chaieb@23274
   570
  by (unfold iff_def,cases "p=q", auto simp add: not_qf)
chaieb@23274
   571
lemma iff_nb: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (iff p q)"
chaieb@23274
   572
using iff_def by (unfold iff_def,cases "p=q", auto simp add: not_bn)
chaieb@23274
   573
chaieb@23274
   574
consts simpfm :: "fm \<Rightarrow> fm"
chaieb@23274
   575
recdef simpfm "measure fmsize"
chaieb@23274
   576
  "simpfm (And p q) = conj (simpfm p) (simpfm q)"
chaieb@23274
   577
  "simpfm (Or p q) = disj (simpfm p) (simpfm q)"
chaieb@23274
   578
  "simpfm (Imp p q) = imp (simpfm p) (simpfm q)"
chaieb@23274
   579
  "simpfm (Iff p q) = iff (simpfm p) (simpfm q)"
chaieb@23274
   580
  "simpfm (NOT p) = not (simpfm p)"
chaieb@23274
   581
  "simpfm (Lt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v < 0) then T else F 
chaieb@23274
   582
  | _ \<Rightarrow> Lt a')"
chaieb@23274
   583
  "simpfm (Le a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<le> 0)  then T else F | _ \<Rightarrow> Le a')"
chaieb@23274
   584
  "simpfm (Gt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v > 0)  then T else F | _ \<Rightarrow> Gt a')"
chaieb@23274
   585
  "simpfm (Ge a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<ge> 0)  then T else F | _ \<Rightarrow> Ge a')"
chaieb@23274
   586
  "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v = 0)  then T else F | _ \<Rightarrow> Eq a')"
chaieb@23274
   587
  "simpfm (NEq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<noteq> 0)  then T else F | _ \<Rightarrow> NEq a')"
chaieb@23274
   588
  "simpfm (Dvd i a) = (if i=0 then simpfm (Eq a)
chaieb@23274
   589
             else if (abs i = 1) then T
chaieb@23274
   590
             else let a' = simpnum a in case a' of C v \<Rightarrow> if (i dvd v)  then T else F | _ \<Rightarrow> Dvd i a')"
chaieb@23274
   591
  "simpfm (NDvd i a) = (if i=0 then simpfm (NEq a) 
chaieb@23274
   592
             else if (abs i = 1) then F
chaieb@23274
   593
             else let a' = simpnum a in case a' of C v \<Rightarrow> if (\<not>(i dvd v)) then T else F | _ \<Rightarrow> NDvd i a')"
chaieb@23274
   594
  "simpfm p = p"
chaieb@23274
   595
lemma simpfm: "Ifm bbs bs (simpfm p) = Ifm bbs bs p"
chaieb@23274
   596
proof(induct p rule: simpfm.induct)
chaieb@23274
   597
  case (6 a) let ?sa = "simpnum a" from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
chaieb@23274
   598
  {fix v assume "?sa = C v" hence ?case using sa by simp }
chaieb@23274
   599
  moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa 
chaieb@23274
   600
      by (cases ?sa, simp_all add: Let_def)}
chaieb@23274
   601
  ultimately show ?case by blast
chaieb@17378
   602
next
chaieb@23274
   603
  case (7 a)  let ?sa = "simpnum a" 
chaieb@23274
   604
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
chaieb@23274
   605
  {fix v assume "?sa = C v" hence ?case using sa by simp }
chaieb@23274
   606
  moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa 
chaieb@23274
   607
      by (cases ?sa, simp_all add: Let_def)}
chaieb@23274
   608
  ultimately show ?case by blast
chaieb@23274
   609
next
chaieb@23274
   610
  case (8 a)  let ?sa = "simpnum a" 
chaieb@23274
   611
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
chaieb@23274
   612
  {fix v assume "?sa = C v" hence ?case using sa by simp }
chaieb@23274
   613
  moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa 
chaieb@23274
   614
      by (cases ?sa, simp_all add: Let_def)}
chaieb@23274
   615
  ultimately show ?case by blast
chaieb@23274
   616
next
chaieb@23274
   617
  case (9 a)  let ?sa = "simpnum a" 
chaieb@23274
   618
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
chaieb@23274
   619
  {fix v assume "?sa = C v" hence ?case using sa by simp }
chaieb@23274
   620
  moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa 
chaieb@23274
   621
      by (cases ?sa, simp_all add: Let_def)}
chaieb@23274
   622
  ultimately show ?case by blast
chaieb@23274
   623
next
chaieb@23274
   624
  case (10 a)  let ?sa = "simpnum a" 
chaieb@23274
   625
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
chaieb@23274
   626
  {fix v assume "?sa = C v" hence ?case using sa by simp }
chaieb@23274
   627
  moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa 
chaieb@23274
   628
      by (cases ?sa, simp_all add: Let_def)}
chaieb@23274
   629
  ultimately show ?case by blast
chaieb@23274
   630
next
chaieb@23274
   631
  case (11 a)  let ?sa = "simpnum a" 
chaieb@23274
   632
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
chaieb@23274
   633
  {fix v assume "?sa = C v" hence ?case using sa by simp }
chaieb@23274
   634
  moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa 
chaieb@23274
   635
      by (cases ?sa, simp_all add: Let_def)}
chaieb@23274
   636
  ultimately show ?case by blast
chaieb@23274
   637
next
chaieb@23274
   638
  case (12 i a)  let ?sa = "simpnum a" from simpnum_ci 
chaieb@23274
   639
  have sa: "Inum bs ?sa = Inum bs a" by simp
chaieb@23274
   640
  have "i=0 \<or> abs i = 1 \<or> (i\<noteq>0 \<and> (abs i \<noteq> 1))" by auto
chaieb@23274
   641
  {assume "i=0" hence ?case using "12.hyps" by (simp add: dvd_def Let_def)}
chaieb@23274
   642
  moreover 
chaieb@23274
   643
  {assume i1: "abs i = 1"
chaieb@23274
   644
      from zdvd_1_left[where m = "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
chaieb@23315
   645
      have ?case using i1 apply (cases "i=0", simp_all add: Let_def) 
chaieb@23315
   646
	by (cases "i > 0", simp_all)}
chaieb@23274
   647
  moreover   
chaieb@23274
   648
  {assume inz: "i\<noteq>0" and cond: "abs i \<noteq> 1"
chaieb@23274
   649
    {fix v assume "?sa = C v" hence ?case using sa[symmetric] inz cond
chaieb@23274
   650
	by (cases "abs i = 1", auto) }
chaieb@23274
   651
    moreover {assume "\<not> (\<exists> v. ?sa = C v)" 
chaieb@23274
   652
      hence "simpfm (Dvd i a) = Dvd i ?sa" using inz cond 
chaieb@23274
   653
	by (cases ?sa, auto simp add: Let_def)
chaieb@23274
   654
      hence ?case using sa by simp}
chaieb@23274
   655
    ultimately have ?case by blast}
chaieb@23274
   656
  ultimately show ?case by blast
chaieb@23274
   657
next
chaieb@23274
   658
  case (13 i a)  let ?sa = "simpnum a" from simpnum_ci 
chaieb@23274
   659
  have sa: "Inum bs ?sa = Inum bs a" by simp
chaieb@23274
   660
  have "i=0 \<or> abs i = 1 \<or> (i\<noteq>0 \<and> (abs i \<noteq> 1))" by auto
chaieb@23274
   661
  {assume "i=0" hence ?case using "13.hyps" by (simp add: dvd_def Let_def)}
chaieb@23274
   662
  moreover 
chaieb@23274
   663
  {assume i1: "abs i = 1"
chaieb@23274
   664
      from zdvd_1_left[where m = "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
chaieb@23315
   665
      have ?case using i1 apply (cases "i=0", simp_all add: Let_def)
chaieb@23315
   666
      apply (cases "i > 0", simp_all) done}
chaieb@23274
   667
  moreover   
chaieb@23274
   668
  {assume inz: "i\<noteq>0" and cond: "abs i \<noteq> 1"
chaieb@23274
   669
    {fix v assume "?sa = C v" hence ?case using sa[symmetric] inz cond
chaieb@23274
   670
	by (cases "abs i = 1", auto) }
chaieb@23274
   671
    moreover {assume "\<not> (\<exists> v. ?sa = C v)" 
chaieb@23274
   672
      hence "simpfm (NDvd i a) = NDvd i ?sa" using inz cond 
chaieb@23274
   673
	by (cases ?sa, auto simp add: Let_def)
chaieb@23274
   674
      hence ?case using sa by simp}
chaieb@23274
   675
    ultimately have ?case by blast}
chaieb@23274
   676
  ultimately show ?case by blast
chaieb@23274
   677
qed (induct p rule: simpfm.induct, simp_all add: conj disj imp iff not)
chaieb@17378
   678
chaieb@23274
   679
lemma simpfm_bound0: "bound0 p \<Longrightarrow> bound0 (simpfm p)"
chaieb@23274
   680
proof(induct p rule: simpfm.induct)
chaieb@23274
   681
  case (6 a) hence nb: "numbound0 a" by simp
chaieb@23274
   682
  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
chaieb@23274
   683
  thus ?case by (cases "simpnum a", auto simp add: Let_def)
chaieb@23274
   684
next
chaieb@23274
   685
  case (7 a) hence nb: "numbound0 a" by simp
chaieb@23274
   686
  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
chaieb@23274
   687
  thus ?case by (cases "simpnum a", auto simp add: Let_def)
chaieb@23274
   688
next
chaieb@23274
   689
  case (8 a) hence nb: "numbound0 a" by simp
chaieb@23274
   690
  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
chaieb@23274
   691
  thus ?case by (cases "simpnum a", auto simp add: Let_def)
chaieb@23274
   692
next
chaieb@23274
   693
  case (9 a) hence nb: "numbound0 a" by simp
chaieb@23274
   694
  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
chaieb@23274
   695
  thus ?case by (cases "simpnum a", auto simp add: Let_def)
chaieb@23274
   696
next
chaieb@23274
   697
  case (10 a) hence nb: "numbound0 a" by simp
chaieb@23274
   698
  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
chaieb@23274
   699
  thus ?case by (cases "simpnum a", auto simp add: Let_def)
chaieb@23274
   700
next
chaieb@23274
   701
  case (11 a) hence nb: "numbound0 a" by simp
chaieb@23274
   702
  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
chaieb@23274
   703
  thus ?case by (cases "simpnum a", auto simp add: Let_def)
chaieb@23274
   704
next
chaieb@23274
   705
  case (12 i a) hence nb: "numbound0 a" by simp
chaieb@23274
   706
  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
chaieb@23274
   707
  thus ?case by (cases "simpnum a", auto simp add: Let_def)
chaieb@23274
   708
next
chaieb@23274
   709
  case (13 i a) hence nb: "numbound0 a" by simp
chaieb@23274
   710
  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
chaieb@23274
   711
  thus ?case by (cases "simpnum a", auto simp add: Let_def)
chaieb@23274
   712
qed(auto simp add: disj_def imp_def iff_def conj_def not_bn)
chaieb@17378
   713
chaieb@23274
   714
lemma simpfm_qf: "qfree p \<Longrightarrow> qfree (simpfm p)"
chaieb@23274
   715
by (induct p rule: simpfm.induct, auto simp add: disj_qf imp_qf iff_qf conj_qf not_qf Let_def)
chaieb@23274
   716
 (case_tac "simpnum a",auto)+
chaieb@23274
   717
chaieb@23274
   718
  (* Generic quantifier elimination *)
chaieb@23274
   719
consts qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
chaieb@23274
   720
recdef qelim "measure fmsize"
chaieb@23274
   721
  "qelim (E p) = (\<lambda> qe. DJ qe (qelim p qe))"
chaieb@23274
   722
  "qelim (A p) = (\<lambda> qe. not (qe ((qelim (NOT p) qe))))"
chaieb@23274
   723
  "qelim (NOT p) = (\<lambda> qe. not (qelim p qe))"
chaieb@23274
   724
  "qelim (And p q) = (\<lambda> qe. conj (qelim p qe) (qelim q qe))" 
chaieb@23274
   725
  "qelim (Or  p q) = (\<lambda> qe. disj (qelim p qe) (qelim q qe))" 
chaieb@23274
   726
  "qelim (Imp p q) = (\<lambda> qe. imp (qelim p qe) (qelim q qe))"
chaieb@23274
   727
  "qelim (Iff p q) = (\<lambda> qe. iff (qelim p qe) (qelim q qe))"
chaieb@23274
   728
  "qelim p = (\<lambda> y. simpfm p)"
chaieb@23274
   729
chaieb@23274
   730
lemma qelim_ci:
chaieb@23274
   731
  assumes qe_inv: "\<forall> bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bbs bs (qe p) = Ifm bbs bs (E p))"
chaieb@23274
   732
  shows "\<And> bs. qfree (qelim p qe) \<and> (Ifm bbs bs (qelim p qe) = Ifm bbs bs p)"
chaieb@23274
   733
using qe_inv DJ_qe[OF qe_inv] 
chaieb@23274
   734
by(induct p rule: qelim.induct) 
chaieb@23274
   735
(auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf 
chaieb@23274
   736
  simpfm simpfm_qf simp del: simpfm.simps)
chaieb@23274
   737
  (* Linearity for fm where Bound 0 ranges over \<int> *)
chaieb@23274
   738
consts
chaieb@23274
   739
  zsplit0 :: "num \<Rightarrow> int \<times> num" (* splits the bounded from the unbounded part*)
chaieb@23274
   740
recdef zsplit0 "measure size"
chaieb@23274
   741
  "zsplit0 (C c) = (0,C c)"
chaieb@23274
   742
  "zsplit0 (Bound n) = (if n=0 then (1, C 0) else (0,Bound n))"
chaieb@23274
   743
  "zsplit0 (CX i a) = (let (i',a') =  zsplit0 a in (i+i', a'))"
chaieb@23274
   744
  "zsplit0 (Neg a) = (let (i',a') =  zsplit0 a in (-i', Neg a'))"
chaieb@23274
   745
  "zsplit0 (Add a b) = (let (ia,a') =  zsplit0 a ; 
chaieb@23274
   746
                            (ib,b') =  zsplit0 b 
chaieb@23274
   747
                            in (ia+ib, Add a' b'))"
chaieb@23274
   748
  "zsplit0 (Sub a b) = (let (ia,a') =  zsplit0 a ; 
chaieb@23274
   749
                            (ib,b') =  zsplit0 b 
chaieb@23274
   750
                            in (ia-ib, Sub a' b'))"
chaieb@23274
   751
  "zsplit0 (Mul i a) = (let (i',a') =  zsplit0 a in (i*i', Mul i a'))"
chaieb@23274
   752
(hints simp add: Let_def)
chaieb@23274
   753
chaieb@23274
   754
lemma zsplit0_I:
chaieb@23274
   755
  shows "\<And> n a. zsplit0 t = (n,a) \<Longrightarrow> (Inum ((x::int) #bs) (CX n a) = Inum (x #bs) t) \<and> numbound0 a"
chaieb@23274
   756
  (is "\<And> n a. ?S t = (n,a) \<Longrightarrow> (?I x (CX n a) = ?I x t) \<and> ?N a")
chaieb@23274
   757
proof(induct t rule: zsplit0.induct)
chaieb@23274
   758
  case (1 c n a) thus ?case by auto 
chaieb@23274
   759
next
chaieb@23274
   760
  case (2 m n a) thus ?case by (cases "m=0") auto
chaieb@23274
   761
next
chaieb@23274
   762
  case (3 i a n a')
chaieb@23274
   763
  let ?j = "fst (zsplit0 a)"
chaieb@23274
   764
  let ?b = "snd (zsplit0 a)"
chaieb@23274
   765
  have abj: "zsplit0 a = (?j,?b)" by simp hence th: "a'=?b \<and> n=i+?j" using prems 
chaieb@23274
   766
    by (simp add: Let_def split_def)
chaieb@23274
   767
  from abj prems  have th2: "(?I x (CX ?j ?b) = ?I x a) \<and> ?N ?b" by blast
chaieb@23274
   768
  from th have "?I x (CX n a') = ?I x (CX (i+?j) ?b)" by simp
chaieb@23274
   769
  also from th2 have "\<dots> = ?I x (CX i (CX ?j ?b))" by (simp add: left_distrib)
chaieb@23274
   770
  finally have "?I x (CX n a') = ?I  x (CX i a)" using th2 by simp
chaieb@23274
   771
  with th2 th show ?case by blast
chaieb@23274
   772
next
chaieb@23274
   773
  case (4 t n a)
chaieb@23274
   774
  let ?nt = "fst (zsplit0 t)"
chaieb@23274
   775
  let ?at = "snd (zsplit0 t)"
chaieb@23274
   776
  have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Neg ?at \<and> n=-?nt" using prems 
chaieb@23274
   777
    by (simp add: Let_def split_def)
chaieb@23274
   778
  from abj prems  have th2: "(?I x (CX ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
chaieb@23274
   779
  from th2[simplified] th[simplified] show ?case by simp
chaieb@23274
   780
next
chaieb@23274
   781
  case (5 s t n a)
chaieb@23274
   782
  let ?ns = "fst (zsplit0 s)"
chaieb@23274
   783
  let ?as = "snd (zsplit0 s)"
chaieb@23274
   784
  let ?nt = "fst (zsplit0 t)"
chaieb@23274
   785
  let ?at = "snd (zsplit0 t)"
chaieb@23274
   786
  have abjs: "zsplit0 s = (?ns,?as)" by simp 
chaieb@23274
   787
  moreover have abjt:  "zsplit0 t = (?nt,?at)" by simp 
chaieb@23274
   788
  ultimately have th: "a=Add ?as ?at \<and> n=?ns + ?nt" using prems 
chaieb@23274
   789
    by (simp add: Let_def split_def)
chaieb@23274
   790
  from abjs[symmetric] have bluddy: "\<exists> x y. (x,y) = zsplit0 s" by blast
chaieb@23274
   791
  from prems have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CX xa xb) = Inum (x # bs) t \<and> numbound0 xb)" by simp
chaieb@23274
   792
  with bluddy abjt have th3: "(?I x (CX ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
chaieb@23274
   793
  from abjs prems  have th2: "(?I x (CX ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
chaieb@23274
   794
  from th3[simplified] th2[simplified] th[simplified] show ?case 
chaieb@23274
   795
    by (simp add: left_distrib)
chaieb@23274
   796
next
chaieb@23274
   797
  case (6 s t n a)
chaieb@23274
   798
  let ?ns = "fst (zsplit0 s)"
chaieb@23274
   799
  let ?as = "snd (zsplit0 s)"
chaieb@23274
   800
  let ?nt = "fst (zsplit0 t)"
chaieb@23274
   801
  let ?at = "snd (zsplit0 t)"
chaieb@23274
   802
  have abjs: "zsplit0 s = (?ns,?as)" by simp 
chaieb@23274
   803
  moreover have abjt:  "zsplit0 t = (?nt,?at)" by simp 
chaieb@23274
   804
  ultimately have th: "a=Sub ?as ?at \<and> n=?ns - ?nt" using prems 
chaieb@23274
   805
    by (simp add: Let_def split_def)
chaieb@23274
   806
  from abjs[symmetric] have bluddy: "\<exists> x y. (x,y) = zsplit0 s" by blast
chaieb@23274
   807
  from prems have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CX xa xb) = Inum (x # bs) t \<and> numbound0 xb)" by simp
chaieb@23274
   808
  with bluddy abjt have th3: "(?I x (CX ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
chaieb@23274
   809
  from abjs prems  have th2: "(?I x (CX ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
chaieb@23274
   810
  from th3[simplified] th2[simplified] th[simplified] show ?case 
chaieb@23274
   811
    by (simp add: left_diff_distrib)
chaieb@23274
   812
next
chaieb@23274
   813
  case (7 i t n a)
chaieb@23274
   814
  let ?nt = "fst (zsplit0 t)"
chaieb@23274
   815
  let ?at = "snd (zsplit0 t)"
chaieb@23274
   816
  have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Mul i ?at \<and> n=i*?nt" using prems 
chaieb@23274
   817
    by (simp add: Let_def split_def)
chaieb@23274
   818
  from abj prems  have th2: "(?I x (CX ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
chaieb@23274
   819
  hence " ?I x (Mul i t) = i * ?I x (CX ?nt ?at)" by simp
chaieb@23274
   820
  also have "\<dots> = ?I x (CX (i*?nt) (Mul i ?at))" by (simp add: right_distrib)
chaieb@23274
   821
  finally show ?case using th th2 by simp
chaieb@17378
   822
qed
chaieb@17378
   823
chaieb@23274
   824
consts
chaieb@23274
   825
  iszlfm :: "fm \<Rightarrow> bool"   (* Linearity test for fm *)
chaieb@23274
   826
  zlfm :: "fm \<Rightarrow> fm"       (* Linearity transformation for fm *)
chaieb@23274
   827
recdef iszlfm "measure size"
chaieb@23274
   828
  "iszlfm (And p q) = (iszlfm p \<and> iszlfm q)" 
chaieb@23274
   829
  "iszlfm (Or p q) = (iszlfm p \<and> iszlfm q)" 
chaieb@23274
   830
  "iszlfm (Eq  (CX c e)) = (c>0 \<and> numbound0 e)"
chaieb@23274
   831
  "iszlfm (NEq (CX c e)) = (c>0 \<and> numbound0 e)"
chaieb@23274
   832
  "iszlfm (Lt  (CX c e)) = (c>0 \<and> numbound0 e)"
chaieb@23274
   833
  "iszlfm (Le  (CX c e)) = (c>0 \<and> numbound0 e)"
chaieb@23274
   834
  "iszlfm (Gt  (CX c e)) = (c>0 \<and> numbound0 e)"
chaieb@23274
   835
  "iszlfm (Ge  (CX c e)) = ( c>0 \<and> numbound0 e)"
chaieb@23274
   836
  "iszlfm (Dvd i (CX c e)) = 
chaieb@23274
   837
                 (c>0 \<and> i>0 \<and> numbound0 e)"
chaieb@23274
   838
  "iszlfm (NDvd i (CX c e))= 
chaieb@23274
   839
                 (c>0 \<and> i>0 \<and> numbound0 e)"
chaieb@23274
   840
  "iszlfm p = (isatom p \<and> (bound0 p))"
chaieb@17378
   841
chaieb@23274
   842
lemma zlin_qfree: "iszlfm p \<Longrightarrow> qfree p"
chaieb@23274
   843
  by (induct p rule: iszlfm.induct) auto
chaieb@17378
   844
chaieb@17378
   845
chaieb@23274
   846
recdef zlfm "measure fmsize"
chaieb@23274
   847
  "zlfm (And p q) = And (zlfm p) (zlfm q)"
chaieb@23274
   848
  "zlfm (Or p q) = Or (zlfm p) (zlfm q)"
chaieb@23274
   849
  "zlfm (Imp p q) = Or (zlfm (NOT p)) (zlfm q)"
chaieb@23274
   850
  "zlfm (Iff p q) = Or (And (zlfm p) (zlfm q)) (And (zlfm (NOT p)) (zlfm (NOT q)))"
chaieb@23274
   851
  "zlfm (Lt a) = (let (c,r) = zsplit0 a in 
chaieb@23274
   852
     if c=0 then Lt r else 
chaieb@23274
   853
     if c>0 then (Lt (CX c r)) else (Gt (CX (- c) (Neg r))))"
chaieb@23274
   854
  "zlfm (Le a) = (let (c,r) = zsplit0 a in 
chaieb@23274
   855
     if c=0 then Le r else 
chaieb@23274
   856
     if c>0 then (Le (CX c r)) else (Ge (CX (- c) (Neg r))))"
chaieb@23274
   857
  "zlfm (Gt a) = (let (c,r) = zsplit0 a in 
chaieb@23274
   858
     if c=0 then Gt r else 
chaieb@23274
   859
     if c>0 then (Gt (CX c r)) else (Lt (CX (- c) (Neg r))))"
chaieb@23274
   860
  "zlfm (Ge a) = (let (c,r) = zsplit0 a in 
chaieb@23274
   861
     if c=0 then Ge r else 
chaieb@23274
   862
     if c>0 then (Ge (CX c r)) else (Le (CX (- c) (Neg r))))"
chaieb@23274
   863
  "zlfm (Eq a) = (let (c,r) = zsplit0 a in 
chaieb@23274
   864
     if c=0 then Eq r else 
chaieb@23274
   865
     if c>0 then (Eq (CX c r)) else (Eq (CX (- c) (Neg r))))"
chaieb@23274
   866
  "zlfm (NEq a) = (let (c,r) = zsplit0 a in 
chaieb@23274
   867
     if c=0 then NEq r else 
chaieb@23274
   868
     if c>0 then (NEq (CX c r)) else (NEq (CX (- c) (Neg r))))"
chaieb@23274
   869
  "zlfm (Dvd i a) = (if i=0 then zlfm (Eq a) 
chaieb@23274
   870
        else (let (c,r) = zsplit0 a in 
chaieb@23274
   871
              if c=0 then (Dvd (abs i) r) else 
chaieb@23274
   872
      if c>0 then (Dvd (abs i) (CX c r))
chaieb@23274
   873
      else (Dvd (abs i) (CX (- c) (Neg r)))))"
chaieb@23274
   874
  "zlfm (NDvd i a) = (if i=0 then zlfm (NEq a) 
chaieb@23274
   875
        else (let (c,r) = zsplit0 a in 
chaieb@23274
   876
              if c=0 then (NDvd (abs i) r) else 
chaieb@23274
   877
      if c>0 then (NDvd (abs i) (CX c r))
chaieb@23274
   878
      else (NDvd (abs i) (CX (- c) (Neg r)))))"
chaieb@23274
   879
  "zlfm (NOT (And p q)) = Or (zlfm (NOT p)) (zlfm (NOT q))"
chaieb@23274
   880
  "zlfm (NOT (Or p q)) = And (zlfm (NOT p)) (zlfm (NOT q))"
chaieb@23274
   881
  "zlfm (NOT (Imp p q)) = And (zlfm p) (zlfm (NOT q))"
chaieb@23274
   882
  "zlfm (NOT (Iff p q)) = Or (And(zlfm p) (zlfm(NOT q))) (And (zlfm(NOT p)) (zlfm q))"
chaieb@23274
   883
  "zlfm (NOT (NOT p)) = zlfm p"
chaieb@23274
   884
  "zlfm (NOT T) = F"
chaieb@23274
   885
  "zlfm (NOT F) = T"
chaieb@23274
   886
  "zlfm (NOT (Lt a)) = zlfm (Ge a)"
chaieb@23274
   887
  "zlfm (NOT (Le a)) = zlfm (Gt a)"
chaieb@23274
   888
  "zlfm (NOT (Gt a)) = zlfm (Le a)"
chaieb@23274
   889
  "zlfm (NOT (Ge a)) = zlfm (Lt a)"
chaieb@23274
   890
  "zlfm (NOT (Eq a)) = zlfm (NEq a)"
chaieb@23274
   891
  "zlfm (NOT (NEq a)) = zlfm (Eq a)"
chaieb@23274
   892
  "zlfm (NOT (Dvd i a)) = zlfm (NDvd i a)"
chaieb@23274
   893
  "zlfm (NOT (NDvd i a)) = zlfm (Dvd i a)"
chaieb@23274
   894
  "zlfm (NOT (Closed P)) = NClosed P"
chaieb@23274
   895
  "zlfm (NOT (NClosed P)) = Closed P"
chaieb@23274
   896
  "zlfm p = p" (hints simp add: fmsize_pos)
chaieb@23274
   897
chaieb@23274
   898
lemma zlfm_I:
chaieb@23274
   899
  assumes qfp: "qfree p"
chaieb@23274
   900
  shows "(Ifm bbs (i#bs) (zlfm p) = Ifm bbs (i# bs) p) \<and> iszlfm (zlfm p)"
chaieb@23274
   901
  (is "(?I (?l p) = ?I p) \<and> ?L (?l p)")
chaieb@23274
   902
using qfp
chaieb@23274
   903
proof(induct p rule: zlfm.induct)
chaieb@23274
   904
  case (5 a) 
chaieb@23274
   905
  let ?c = "fst (zsplit0 a)"
chaieb@23274
   906
  let ?r = "snd (zsplit0 a)"
chaieb@23274
   907
  have spl: "zsplit0 a = (?c,?r)" by simp
chaieb@23274
   908
  from zsplit0_I[OF spl, where x="i" and bs="bs"] 
chaieb@23274
   909
  have Ia:"Inum (i # bs) a = Inum (i #bs) (CX ?c ?r)" and nb: "numbound0 ?r" by auto 
chaieb@23274
   910
  let ?N = "\<lambda> t. Inum (i#bs) t"
chaieb@23274
   911
  from prems Ia nb  show ?case 
nipkow@23477
   912
    by (auto simp add: Let_def split_def ring_simps) (cases "?r",auto)
chaieb@23274
   913
next
chaieb@23274
   914
  case (6 a)  
chaieb@23274
   915
  let ?c = "fst (zsplit0 a)"
chaieb@23274
   916
  let ?r = "snd (zsplit0 a)"
chaieb@23274
   917
  have spl: "zsplit0 a = (?c,?r)" by simp
chaieb@23274
   918
  from zsplit0_I[OF spl, where x="i" and bs="bs"] 
chaieb@23274
   919
  have Ia:"Inum (i # bs) a = Inum (i #bs) (CX ?c ?r)" and nb: "numbound0 ?r" by auto 
chaieb@23274
   920
  let ?N = "\<lambda> t. Inum (i#bs) t"
chaieb@23274
   921
  from prems Ia nb  show ?case 
nipkow@23477
   922
    by (auto simp add: Let_def split_def ring_simps) (cases "?r",auto)
chaieb@23274
   923
next
chaieb@23274
   924
  case (7 a)  
chaieb@23274
   925
  let ?c = "fst (zsplit0 a)"
chaieb@23274
   926
  let ?r = "snd (zsplit0 a)"
chaieb@23274
   927
  have spl: "zsplit0 a = (?c,?r)" by simp
chaieb@23274
   928
  from zsplit0_I[OF spl, where x="i" and bs="bs"] 
chaieb@23274
   929
  have Ia:"Inum (i # bs) a = Inum (i #bs) (CX ?c ?r)" and nb: "numbound0 ?r" by auto 
chaieb@23274
   930
  let ?N = "\<lambda> t. Inum (i#bs) t"
chaieb@23274
   931
  from prems Ia nb  show ?case 
nipkow@23477
   932
    by (auto simp add: Let_def split_def ring_simps) (cases "?r",auto)
chaieb@23274
   933
next
chaieb@23274
   934
  case (8 a)  
chaieb@23274
   935
  let ?c = "fst (zsplit0 a)"
chaieb@23274
   936
  let ?r = "snd (zsplit0 a)"
chaieb@23274
   937
  have spl: "zsplit0 a = (?c,?r)" by simp
chaieb@23274
   938
  from zsplit0_I[OF spl, where x="i" and bs="bs"] 
chaieb@23274
   939
  have Ia:"Inum (i # bs) a = Inum (i #bs) (CX ?c ?r)" and nb: "numbound0 ?r" by auto 
chaieb@23274
   940
  let ?N = "\<lambda> t. Inum (i#bs) t"
chaieb@23274
   941
  from prems Ia nb  show ?case 
nipkow@23477
   942
    by (auto simp add: Let_def split_def ring_simps) (cases "?r",auto)
chaieb@23274
   943
next
chaieb@23274
   944
  case (9 a)  
chaieb@23274
   945
  let ?c = "fst (zsplit0 a)"
chaieb@23274
   946
  let ?r = "snd (zsplit0 a)"
chaieb@23274
   947
  have spl: "zsplit0 a = (?c,?r)" by simp
chaieb@23274
   948
  from zsplit0_I[OF spl, where x="i" and bs="bs"] 
chaieb@23274
   949
  have Ia:"Inum (i # bs) a = Inum (i #bs) (CX ?c ?r)" and nb: "numbound0 ?r" by auto 
chaieb@23274
   950
  let ?N = "\<lambda> t. Inum (i#bs) t"
chaieb@23274
   951
  from prems Ia nb  show ?case 
nipkow@23477
   952
    by (auto simp add: Let_def split_def ring_simps) (cases "?r",auto)
chaieb@23274
   953
next
chaieb@23274
   954
  case (10 a)  
chaieb@23274
   955
  let ?c = "fst (zsplit0 a)"
chaieb@23274
   956
  let ?r = "snd (zsplit0 a)"
chaieb@23274
   957
  have spl: "zsplit0 a = (?c,?r)" by simp
chaieb@23274
   958
  from zsplit0_I[OF spl, where x="i" and bs="bs"] 
chaieb@23274
   959
  have Ia:"Inum (i # bs) a = Inum (i #bs) (CX ?c ?r)" and nb: "numbound0 ?r" by auto 
chaieb@23274
   960
  let ?N = "\<lambda> t. Inum (i#bs) t"
chaieb@23274
   961
  from prems Ia nb  show ?case 
nipkow@23477
   962
    by (auto simp add: Let_def split_def ring_simps) (cases "?r",auto)
chaieb@17378
   963
next
chaieb@23274
   964
  case (11 j a)  
chaieb@23274
   965
  let ?c = "fst (zsplit0 a)"
chaieb@23274
   966
  let ?r = "snd (zsplit0 a)"
chaieb@23274
   967
  have spl: "zsplit0 a = (?c,?r)" by simp
chaieb@23274
   968
  from zsplit0_I[OF spl, where x="i" and bs="bs"] 
chaieb@23274
   969
  have Ia:"Inum (i # bs) a = Inum (i #bs) (CX ?c ?r)" and nb: "numbound0 ?r" by auto 
chaieb@23274
   970
  let ?N = "\<lambda> t. Inum (i#bs) t"
chaieb@23274
   971
  have "j=0 \<or> (j\<noteq>0 \<and> ?c = 0) \<or> (j\<noteq>0 \<and> ?c >0) \<or> (j\<noteq> 0 \<and> ?c<0)" by arith
chaieb@23274
   972
  moreover
chaieb@23274
   973
  {assume "j=0" hence z: "zlfm (Dvd j a) = (zlfm (Eq a))" by (simp add: Let_def) 
chaieb@23274
   974
    hence ?case using prems by (simp del: zlfm.simps add: zdvd_0_left)}
chaieb@23274
   975
  moreover
chaieb@23274
   976
  {assume "?c=0" and "j\<noteq>0" hence ?case 
chaieb@23274
   977
      using zsplit0_I[OF spl, where x="i" and bs="bs"] zdvd_abs1[where d="j"]
chaieb@23274
   978
      by (cases "?r", simp_all add: Let_def split_def)}
chaieb@23274
   979
  moreover
chaieb@23274
   980
  {assume cp: "?c > 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" 
chaieb@23274
   981
      by (simp add: nb Let_def split_def)
chaieb@23274
   982
    hence ?case using Ia cp jnz by (simp add: Let_def split_def 
chaieb@23274
   983
	zdvd_abs1[where d="j" and t="(?c*i) + ?N ?r", symmetric])}
chaieb@23274
   984
  moreover
chaieb@23274
   985
  {assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" 
chaieb@23274
   986
      by (simp add: nb Let_def split_def)
chaieb@23274
   987
    hence ?case using Ia cn jnz zdvd_zminus_iff[where m="abs j" and n="?c*i + ?N ?r" ]
chaieb@23274
   988
      by (simp add: Let_def split_def 
chaieb@23274
   989
      zdvd_abs1[where d="j" and t="(?c*i) + ?N ?r", symmetric])}
chaieb@23274
   990
  ultimately show ?case by blast
chaieb@17378
   991
next
chaieb@23274
   992
  case (12 j a) 
chaieb@23274
   993
  let ?c = "fst (zsplit0 a)"
chaieb@23274
   994
  let ?r = "snd (zsplit0 a)"
chaieb@23274
   995
  have spl: "zsplit0 a = (?c,?r)" by simp
chaieb@23274
   996
  from zsplit0_I[OF spl, where x="i" and bs="bs"] 
chaieb@23274
   997
  have Ia:"Inum (i # bs) a = Inum (i #bs) (CX ?c ?r)" and nb: "numbound0 ?r" by auto 
chaieb@23274
   998
  let ?N = "\<lambda> t. Inum (i#bs) t"
chaieb@23274
   999
  have "j=0 \<or> (j\<noteq>0 \<and> ?c = 0) \<or> (j\<noteq>0 \<and> ?c >0) \<or> (j\<noteq> 0 \<and> ?c<0)" by arith
chaieb@23274
  1000
  moreover
chaieb@23274
  1001
  {assume "j=0" hence z: "zlfm (NDvd j a) = (zlfm (NEq a))" by (simp add: Let_def) 
chaieb@23274
  1002
    hence ?case using prems by (simp del: zlfm.simps add: zdvd_0_left)}
chaieb@23274
  1003
  moreover
chaieb@23274
  1004
  {assume "?c=0" and "j\<noteq>0" hence ?case 
chaieb@23274
  1005
      using zsplit0_I[OF spl, where x="i" and bs="bs"] zdvd_abs1[where d="j"]
chaieb@23274
  1006
      by (cases "?r", simp_all add: Let_def split_def)}
chaieb@23274
  1007
  moreover
chaieb@23274
  1008
  {assume cp: "?c > 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" 
chaieb@23274
  1009
      by (simp add: nb Let_def split_def)
chaieb@23274
  1010
    hence ?case using Ia cp jnz by (simp add: Let_def split_def 
chaieb@23274
  1011
	zdvd_abs1[where d="j" and t="(?c*i) + ?N ?r", symmetric])}
chaieb@23274
  1012
  moreover
chaieb@23274
  1013
  {assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" 
chaieb@23274
  1014
      by (simp add: nb Let_def split_def)
chaieb@23274
  1015
    hence ?case using Ia cn jnz zdvd_zminus_iff[where m="abs j" and n="?c*i + ?N ?r" ]
chaieb@23274
  1016
      by (simp add: Let_def split_def 
chaieb@23274
  1017
      zdvd_abs1[where d="j" and t="(?c*i) + ?N ?r", symmetric])}
chaieb@23274
  1018
  ultimately show ?case by blast
chaieb@23274
  1019
qed auto
chaieb@23274
  1020
chaieb@23274
  1021
consts 
chaieb@23274
  1022
  plusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of +\<infinity>*)
chaieb@23274
  1023
  minusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of -\<infinity>*)
chaieb@23274
  1024
  \<delta> :: "fm \<Rightarrow> int" (* Compute lcm {d| N\<^isup>?\<^isup> Dvd c*x+t \<in> p}*)
chaieb@23274
  1025
  d\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* checks if a given l divides all the ds above*)
chaieb@23274
  1026
chaieb@23274
  1027
recdef minusinf "measure size"
chaieb@23274
  1028
  "minusinf (And p q) = And (minusinf p) (minusinf q)" 
chaieb@23274
  1029
  "minusinf (Or p q) = Or (minusinf p) (minusinf q)" 
chaieb@23274
  1030
  "minusinf (Eq  (CX c e)) = F"
chaieb@23274
  1031
  "minusinf (NEq (CX c e)) = T"
chaieb@23274
  1032
  "minusinf (Lt  (CX c e)) = T"
chaieb@23274
  1033
  "minusinf (Le  (CX c e)) = T"
chaieb@23274
  1034
  "minusinf (Gt  (CX c e)) = F"
chaieb@23274
  1035
  "minusinf (Ge  (CX c e)) = F"
chaieb@23274
  1036
  "minusinf p = p"
chaieb@23274
  1037
chaieb@23274
  1038
lemma minusinf_qfree: "qfree p \<Longrightarrow> qfree (minusinf p)"
chaieb@23274
  1039
  by (induct p rule: minusinf.induct, auto)
chaieb@23274
  1040
chaieb@23274
  1041
recdef plusinf "measure size"
chaieb@23274
  1042
  "plusinf (And p q) = And (plusinf p) (plusinf q)" 
chaieb@23274
  1043
  "plusinf (Or p q) = Or (plusinf p) (plusinf q)" 
chaieb@23274
  1044
  "plusinf (Eq  (CX c e)) = F"
chaieb@23274
  1045
  "plusinf (NEq (CX c e)) = T"
chaieb@23274
  1046
  "plusinf (Lt  (CX c e)) = F"
chaieb@23274
  1047
  "plusinf (Le  (CX c e)) = F"
chaieb@23274
  1048
  "plusinf (Gt  (CX c e)) = T"
chaieb@23274
  1049
  "plusinf (Ge  (CX c e)) = T"
chaieb@23274
  1050
  "plusinf p = p"
chaieb@23274
  1051
chaieb@23274
  1052
recdef \<delta> "measure size"
chaieb@23274
  1053
  "\<delta> (And p q) = ilcm (\<delta> p) (\<delta> q)" 
chaieb@23274
  1054
  "\<delta> (Or p q) = ilcm (\<delta> p) (\<delta> q)" 
chaieb@23274
  1055
  "\<delta> (Dvd i (CX c e)) = i"
chaieb@23274
  1056
  "\<delta> (NDvd i (CX c e)) = i"
chaieb@23274
  1057
  "\<delta> p = 1"
chaieb@23274
  1058
chaieb@23274
  1059
recdef d\<delta> "measure size"
chaieb@23274
  1060
  "d\<delta> (And p q) = (\<lambda> d. d\<delta> p d \<and> d\<delta> q d)" 
chaieb@23274
  1061
  "d\<delta> (Or p q) = (\<lambda> d. d\<delta> p d \<and> d\<delta> q d)" 
chaieb@23274
  1062
  "d\<delta> (Dvd i (CX c e)) = (\<lambda> d. i dvd d)"
chaieb@23274
  1063
  "d\<delta> (NDvd i (CX c e)) = (\<lambda> d. i dvd d)"
chaieb@23274
  1064
  "d\<delta> p = (\<lambda> d. True)"
chaieb@23274
  1065
chaieb@23274
  1066
lemma delta_mono: 
chaieb@23274
  1067
  assumes lin: "iszlfm p"
chaieb@23274
  1068
  and d: "d dvd d'"
chaieb@23274
  1069
  and ad: "d\<delta> p d"
chaieb@23274
  1070
  shows "d\<delta> p d'"
chaieb@23274
  1071
  using lin ad d
chaieb@23274
  1072
proof(induct p rule: iszlfm.induct)
chaieb@23274
  1073
  case (9 i c e)  thus ?case using d
chaieb@23274
  1074
    by (simp add: zdvd_trans[where m="i" and n="d" and k="d'"])
chaieb@17378
  1075
next
chaieb@23274
  1076
  case (10 i c e) thus ?case using d
chaieb@23274
  1077
    by (simp add: zdvd_trans[where m="i" and n="d" and k="d'"])
chaieb@23274
  1078
qed simp_all
chaieb@17378
  1079
chaieb@23274
  1080
lemma \<delta> : assumes lin:"iszlfm p"
chaieb@23274
  1081
  shows "d\<delta> p (\<delta> p) \<and> \<delta> p >0"
chaieb@23274
  1082
using lin
chaieb@23274
  1083
proof (induct p rule: iszlfm.induct)
chaieb@23274
  1084
  case (1 p q) 
chaieb@23274
  1085
  let ?d = "\<delta> (And p q)"
chaieb@23274
  1086
  from prems ilcm_pos have dp: "?d >0" by simp
chaieb@23274
  1087
  have d1: "\<delta> p dvd \<delta> (And p q)" using prems ilcm_dvd1 by simp 
chaieb@23274
  1088
   hence th: "d\<delta> p ?d" using delta_mono prems by auto
chaieb@23274
  1089
  have "\<delta> q dvd \<delta> (And p q)" using prems ilcm_dvd2 by simp 
chaieb@23274
  1090
  hence th': "d\<delta> q ?d" using delta_mono prems by auto
chaieb@23274
  1091
  from th th' dp show ?case by simp 
chaieb@23274
  1092
next
chaieb@23274
  1093
  case (2 p q)  
chaieb@23274
  1094
  let ?d = "\<delta> (And p q)"
chaieb@23274
  1095
  from prems ilcm_pos have dp: "?d >0" by simp
chaieb@23274
  1096
  have "\<delta> p dvd \<delta> (And p q)" using prems ilcm_dvd1 by simp hence th: "d\<delta> p ?d" using delta_mono prems by auto
chaieb@23274
  1097
  have "\<delta> q dvd \<delta> (And p q)" using prems ilcm_dvd2 by simp hence th': "d\<delta> q ?d" using delta_mono prems by auto
chaieb@23274
  1098
  from th th' dp show ?case by simp 
chaieb@17378
  1099
qed simp_all
chaieb@17378
  1100
chaieb@17378
  1101
chaieb@23274
  1102
consts 
chaieb@23274
  1103
  a\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" (* adjusts the coeffitients of a formula *)
chaieb@23274
  1104
  d\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* tests if all coeffs c of c divide a given l*)
chaieb@23274
  1105
  \<zeta>  :: "fm \<Rightarrow> int" (* computes the lcm of all coefficients of x*)
chaieb@23274
  1106
  \<beta> :: "fm \<Rightarrow> num list"
chaieb@23274
  1107
  \<alpha> :: "fm \<Rightarrow> num list"
chaieb@17378
  1108
chaieb@23274
  1109
recdef a\<beta> "measure size"
chaieb@23274
  1110
  "a\<beta> (And p q) = (\<lambda> k. And (a\<beta> p k) (a\<beta> q k))" 
chaieb@23274
  1111
  "a\<beta> (Or p q) = (\<lambda> k. Or (a\<beta> p k) (a\<beta> q k))" 
chaieb@23274
  1112
  "a\<beta> (Eq  (CX c e)) = (\<lambda> k. Eq (CX 1 (Mul (k div c) e)))"
chaieb@23274
  1113
  "a\<beta> (NEq (CX c e)) = (\<lambda> k. NEq (CX 1 (Mul (k div c) e)))"
chaieb@23274
  1114
  "a\<beta> (Lt  (CX c e)) = (\<lambda> k. Lt (CX 1 (Mul (k div c) e)))"
chaieb@23274
  1115
  "a\<beta> (Le  (CX c e)) = (\<lambda> k. Le (CX 1 (Mul (k div c) e)))"
chaieb@23274
  1116
  "a\<beta> (Gt  (CX c e)) = (\<lambda> k. Gt (CX 1 (Mul (k div c) e)))"
chaieb@23274
  1117
  "a\<beta> (Ge  (CX c e)) = (\<lambda> k. Ge (CX 1 (Mul (k div c) e)))"
chaieb@23274
  1118
  "a\<beta> (Dvd i (CX c e)) =(\<lambda> k. Dvd ((k div c)*i) (CX 1 (Mul (k div c) e)))"
chaieb@23274
  1119
  "a\<beta> (NDvd i (CX c e))=(\<lambda> k. NDvd ((k div c)*i) (CX 1 (Mul (k div c) e)))"
chaieb@23274
  1120
  "a\<beta> p = (\<lambda> k. p)"
chaieb@17378
  1121
chaieb@23274
  1122
recdef d\<beta> "measure size"
chaieb@23274
  1123
  "d\<beta> (And p q) = (\<lambda> k. (d\<beta> p k) \<and> (d\<beta> q k))" 
chaieb@23274
  1124
  "d\<beta> (Or p q) = (\<lambda> k. (d\<beta> p k) \<and> (d\<beta> q k))" 
chaieb@23274
  1125
  "d\<beta> (Eq  (CX c e)) = (\<lambda> k. c dvd k)"
chaieb@23274
  1126
  "d\<beta> (NEq (CX c e)) = (\<lambda> k. c dvd k)"
chaieb@23274
  1127
  "d\<beta> (Lt  (CX c e)) = (\<lambda> k. c dvd k)"
chaieb@23274
  1128
  "d\<beta> (Le  (CX c e)) = (\<lambda> k. c dvd k)"
chaieb@23274
  1129
  "d\<beta> (Gt  (CX c e)) = (\<lambda> k. c dvd k)"
chaieb@23274
  1130
  "d\<beta> (Ge  (CX c e)) = (\<lambda> k. c dvd k)"
chaieb@23274
  1131
  "d\<beta> (Dvd i (CX c e)) =(\<lambda> k. c dvd k)"
chaieb@23274
  1132
  "d\<beta> (NDvd i (CX c e))=(\<lambda> k. c dvd k)"
chaieb@23274
  1133
  "d\<beta> p = (\<lambda> k. True)"
chaieb@17378
  1134
chaieb@23274
  1135
recdef \<zeta> "measure size"
chaieb@23274
  1136
  "\<zeta> (And p q) = ilcm (\<zeta> p) (\<zeta> q)" 
chaieb@23274
  1137
  "\<zeta> (Or p q) = ilcm (\<zeta> p) (\<zeta> q)" 
chaieb@23274
  1138
  "\<zeta> (Eq  (CX c e)) = c"
chaieb@23274
  1139
  "\<zeta> (NEq (CX c e)) = c"
chaieb@23274
  1140
  "\<zeta> (Lt  (CX c e)) = c"
chaieb@23274
  1141
  "\<zeta> (Le  (CX c e)) = c"
chaieb@23274
  1142
  "\<zeta> (Gt  (CX c e)) = c"
chaieb@23274
  1143
  "\<zeta> (Ge  (CX c e)) = c"
chaieb@23274
  1144
  "\<zeta> (Dvd i (CX c e)) = c"
chaieb@23274
  1145
  "\<zeta> (NDvd i (CX c e))= c"
chaieb@23274
  1146
  "\<zeta> p = 1"
chaieb@17378
  1147
chaieb@23274
  1148
recdef \<beta> "measure size"
chaieb@23274
  1149
  "\<beta> (And p q) = (\<beta> p @ \<beta> q)" 
chaieb@23274
  1150
  "\<beta> (Or p q) = (\<beta> p @ \<beta> q)" 
chaieb@23274
  1151
  "\<beta> (Eq  (CX c e)) = [Sub (C -1) e]"
chaieb@23274
  1152
  "\<beta> (NEq (CX c e)) = [Neg e]"
chaieb@23274
  1153
  "\<beta> (Lt  (CX c e)) = []"
chaieb@23274
  1154
  "\<beta> (Le  (CX c e)) = []"
chaieb@23274
  1155
  "\<beta> (Gt  (CX c e)) = [Neg e]"
chaieb@23274
  1156
  "\<beta> (Ge  (CX c e)) = [Sub (C -1) e]"
chaieb@23274
  1157
  "\<beta> p = []"
wenzelm@19736
  1158
chaieb@23274
  1159
recdef \<alpha> "measure size"
chaieb@23274
  1160
  "\<alpha> (And p q) = (\<alpha> p @ \<alpha> q)" 
chaieb@23274
  1161
  "\<alpha> (Or p q) = (\<alpha> p @ \<alpha> q)" 
chaieb@23274
  1162
  "\<alpha> (Eq  (CX c e)) = [Add (C -1) e]"
chaieb@23274
  1163
  "\<alpha> (NEq (CX c e)) = [e]"
chaieb@23274
  1164
  "\<alpha> (Lt  (CX c e)) = [e]"
chaieb@23274
  1165
  "\<alpha> (Le  (CX c e)) = [Add (C -1) e]"
chaieb@23274
  1166
  "\<alpha> (Gt  (CX c e)) = []"
chaieb@23274
  1167
  "\<alpha> (Ge  (CX c e)) = []"
chaieb@23274
  1168
  "\<alpha> p = []"
chaieb@23274
  1169
consts mirror :: "fm \<Rightarrow> fm"
chaieb@23274
  1170
recdef mirror "measure size"
chaieb@23274
  1171
  "mirror (And p q) = And (mirror p) (mirror q)" 
chaieb@23274
  1172
  "mirror (Or p q) = Or (mirror p) (mirror q)" 
chaieb@23274
  1173
  "mirror (Eq  (CX c e)) = Eq (CX c (Neg e))"
chaieb@23274
  1174
  "mirror (NEq (CX c e)) = NEq (CX c (Neg e))"
chaieb@23274
  1175
  "mirror (Lt  (CX c e)) = Gt (CX c (Neg e))"
chaieb@23274
  1176
  "mirror (Le  (CX c e)) = Ge (CX c (Neg e))"
chaieb@23274
  1177
  "mirror (Gt  (CX c e)) = Lt (CX c (Neg e))"
chaieb@23274
  1178
  "mirror (Ge  (CX c e)) = Le (CX c (Neg e))"
chaieb@23274
  1179
  "mirror (Dvd i (CX c e)) = Dvd i (CX c (Neg e))"
chaieb@23274
  1180
  "mirror (NDvd i (CX c e)) = NDvd i (CX c (Neg e))"
chaieb@23274
  1181
  "mirror p = p"
chaieb@23274
  1182
    (* Lemmas for the correctness of \<sigma>\<rho> *)
chaieb@23274
  1183
lemma dvd1_eq1: "x >0 \<Longrightarrow> (x::int) dvd 1 = (x = 1)"
chaieb@23274
  1184
by auto
chaieb@17378
  1185
chaieb@23274
  1186
lemma minusinf_inf:
chaieb@23274
  1187
  assumes linp: "iszlfm p"
chaieb@23274
  1188
  and u: "d\<beta> p 1"
chaieb@23274
  1189
  shows "\<exists> (z::int). \<forall> x < z. Ifm bbs (x#bs) (minusinf p) = Ifm bbs (x#bs) p"
chaieb@23274
  1190
  (is "?P p" is "\<exists> (z::int). \<forall> x < z. ?I x (?M p) = ?I x p")
chaieb@23274
  1191
using linp u
chaieb@23274
  1192
proof (induct p rule: minusinf.induct)
chaieb@23274
  1193
  case (1 p q) thus ?case 
chaieb@23274
  1194
    by (auto simp add: dvd1_eq1) (rule_tac x="min z za" in exI,simp)
chaieb@23274
  1195
next
chaieb@23274
  1196
  case (2 p q) thus ?case 
chaieb@23274
  1197
    by (auto simp add: dvd1_eq1) (rule_tac x="min z za" in exI,simp)
chaieb@17378
  1198
next
chaieb@23274
  1199
  case (3 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
chaieb@23274
  1200
  hence "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<noteq> 0"
chaieb@23274
  1201
  proof(clarsimp)
chaieb@23274
  1202
    fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e = 0"
chaieb@23274
  1203
    with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
chaieb@23274
  1204
    show "False" by simp
chaieb@23274
  1205
  qed
chaieb@23274
  1206
  thus ?case by auto
chaieb@17378
  1207
next
chaieb@23274
  1208
  case (4 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
chaieb@23274
  1209
  hence "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<noteq> 0"
chaieb@23274
  1210
  proof(clarsimp)
chaieb@23274
  1211
    fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e = 0"
chaieb@23274
  1212
    with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
chaieb@23274
  1213
    show "False" by simp
chaieb@23274
  1214
  qed
chaieb@23274
  1215
  thus ?case by auto
chaieb@17378
  1216
next
chaieb@23274
  1217
  case (5 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
chaieb@23274
  1218
  hence "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e < 0"
chaieb@23274
  1219
  proof(clarsimp)
chaieb@23274
  1220
    fix x assume "x < (- Inum (a#bs) e)" 
chaieb@23274
  1221
    with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
chaieb@23274
  1222
    show "x + Inum (x#bs) e < 0" by simp
chaieb@23274
  1223
  qed
chaieb@23274
  1224
  thus ?case by auto
chaieb@23274
  1225
next
chaieb@23274
  1226
  case (6 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
chaieb@23274
  1227
  hence "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<le> 0"
chaieb@23274
  1228
  proof(clarsimp)
chaieb@23274
  1229
    fix x assume "x < (- Inum (a#bs) e)" 
chaieb@23274
  1230
    with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
chaieb@23274
  1231
    show "x + Inum (x#bs) e \<le> 0" by simp
chaieb@23274
  1232
  qed
chaieb@23274
  1233
  thus ?case by auto
chaieb@23274
  1234
next
chaieb@23274
  1235
  case (7 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
chaieb@23274
  1236
  hence "\<forall> x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e > 0)"
chaieb@23274
  1237
  proof(clarsimp)
chaieb@23274
  1238
    fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e > 0"
chaieb@23274
  1239
    with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
chaieb@23274
  1240
    show "False" by simp
chaieb@23274
  1241
  qed
chaieb@23274
  1242
  thus ?case by auto
chaieb@23274
  1243
next
chaieb@23274
  1244
  case (8 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
chaieb@23274
  1245
  hence "\<forall> x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e \<ge> 0)"
chaieb@23274
  1246
  proof(clarsimp)
chaieb@23274
  1247
    fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e \<ge> 0"
chaieb@23274
  1248
    with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
chaieb@23274
  1249
    show "False" by simp
chaieb@23274
  1250
  qed
chaieb@23274
  1251
  thus ?case by auto
chaieb@23274
  1252
qed auto
chaieb@17378
  1253
chaieb@23274
  1254
lemma minusinf_repeats:
chaieb@23274
  1255
  assumes d: "d\<delta> p d" and linp: "iszlfm p"
chaieb@23274
  1256
  shows "Ifm bbs ((x - k*d)#bs) (minusinf p) = Ifm bbs (x #bs) (minusinf p)"
chaieb@23274
  1257
using linp d
chaieb@23274
  1258
proof(induct p rule: iszlfm.induct) 
chaieb@23274
  1259
  case (9 i c e) hence nbe: "numbound0 e"  and id: "i dvd d" by simp+
chaieb@23274
  1260
    hence "\<exists> k. d=i*k" by (simp add: dvd_def)
chaieb@23274
  1261
    then obtain "di" where di_def: "d=i*di" by blast
chaieb@23274
  1262
    show ?case 
chaieb@23274
  1263
    proof(simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib, rule iffI)
chaieb@23274
  1264
      assume 
chaieb@23274
  1265
	"i dvd c * x - c*(k*d) + Inum (x # bs) e"
chaieb@23274
  1266
      (is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt")
chaieb@23274
  1267
      hence "\<exists> (l::int). ?rt = i * l" by (simp add: dvd_def)
chaieb@23274
  1268
      hence "\<exists> (l::int). c*x+ ?I x e = i*l+c*(k * i*di)" 
nipkow@23477
  1269
	by (simp add: ring_simps di_def)
chaieb@23274
  1270
      hence "\<exists> (l::int). c*x+ ?I x e = i*(l + c*k*di)"
nipkow@23477
  1271
	by (simp add: ring_simps)
chaieb@23274
  1272
      hence "\<exists> (l::int). c*x+ ?I x e = i*l" by blast
chaieb@23274
  1273
      thus "i dvd c*x + Inum (x # bs) e" by (simp add: dvd_def) 
chaieb@23274
  1274
    next
chaieb@23274
  1275
      assume 
chaieb@23274
  1276
	"i dvd c*x + Inum (x # bs) e" (is "?ri dvd ?rc*?rx+?e")
chaieb@23274
  1277
      hence "\<exists> (l::int). c*x+?e = i*l" by (simp add: dvd_def)
chaieb@23274
  1278
      hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp
chaieb@23274
  1279
      hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def)
nipkow@23477
  1280
      hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: ring_simps)
chaieb@23274
  1281
      hence "\<exists> (l::int). c*x - c * (k*d) +?e = i*l"
chaieb@23274
  1282
	by blast
chaieb@23274
  1283
      thus "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def)
chaieb@23274
  1284
    qed
chaieb@23274
  1285
next
chaieb@23274
  1286
  case (10 i c e)  hence nbe: "numbound0 e"  and id: "i dvd d" by simp+
chaieb@23274
  1287
    hence "\<exists> k. d=i*k" by (simp add: dvd_def)
chaieb@23274
  1288
    then obtain "di" where di_def: "d=i*di" by blast
chaieb@23274
  1289
    show ?case 
chaieb@23274
  1290
    proof(simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib, rule iffI)
chaieb@23274
  1291
      assume 
chaieb@23274
  1292
	"i dvd c * x - c*(k*d) + Inum (x # bs) e"
chaieb@23274
  1293
      (is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt")
chaieb@23274
  1294
      hence "\<exists> (l::int). ?rt = i * l" by (simp add: dvd_def)
chaieb@23274
  1295
      hence "\<exists> (l::int). c*x+ ?I x e = i*l+c*(k * i*di)" 
nipkow@23477
  1296
	by (simp add: ring_simps di_def)
chaieb@23274
  1297
      hence "\<exists> (l::int). c*x+ ?I x e = i*(l + c*k*di)"
nipkow@23477
  1298
	by (simp add: ring_simps)
chaieb@23274
  1299
      hence "\<exists> (l::int). c*x+ ?I x e = i*l" by blast
chaieb@23274
  1300
      thus "i dvd c*x + Inum (x # bs) e" by (simp add: dvd_def) 
chaieb@23274
  1301
    next
chaieb@23274
  1302
      assume 
chaieb@23274
  1303
	"i dvd c*x + Inum (x # bs) e" (is "?ri dvd ?rc*?rx+?e")
chaieb@23274
  1304
      hence "\<exists> (l::int). c*x+?e = i*l" by (simp add: dvd_def)
chaieb@23274
  1305
      hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp
chaieb@23274
  1306
      hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def)
nipkow@23477
  1307
      hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: ring_simps)
chaieb@23274
  1308
      hence "\<exists> (l::int). c*x - c * (k*d) +?e = i*l"
chaieb@23274
  1309
	by blast
chaieb@23274
  1310
      thus "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def)
chaieb@23274
  1311
    qed
chaieb@23274
  1312
qed (auto simp add: nth_pos2 numbound0_I[where bs="bs" and b="x - k*d" and b'="x"])
chaieb@17378
  1313
chaieb@23274
  1314
    (* Is'nt this beautiful?*)
chaieb@23274
  1315
lemma minusinf_ex:
chaieb@23274
  1316
  assumes lin: "iszlfm p" and u: "d\<beta> p 1"
chaieb@23274
  1317
  and exmi: "\<exists> (x::int). Ifm bbs (x#bs) (minusinf p)" (is "\<exists> x. ?P1 x")
chaieb@23274
  1318
  shows "\<exists> (x::int). Ifm bbs (x#bs) p" (is "\<exists> x. ?P x")
chaieb@17378
  1319
proof-
chaieb@23274
  1320
  let ?d = "\<delta> p"
chaieb@23274
  1321
  from \<delta> [OF lin] have dpos: "?d >0" by simp
chaieb@23274
  1322
  from \<delta> [OF lin] have alld: "d\<delta> p ?d" by simp
chaieb@23274
  1323
  from minusinf_repeats[OF alld lin] have th1:"\<forall> x k. ?P1 x = ?P1 (x - (k * ?d))" by simp
chaieb@23274
  1324
  from minusinf_inf[OF lin u] have th2:"\<exists> z. \<forall> x. x<z \<longrightarrow> (?P x = ?P1 x)" by blast
chaieb@23274
  1325
  from minusinfinity [OF dpos th1 th2] exmi show ?thesis by blast
chaieb@17378
  1326
qed
chaieb@17378
  1327
chaieb@23274
  1328
    (*	And This ???*)
chaieb@23274
  1329
lemma minusinf_bex:
chaieb@23274
  1330
  assumes lin: "iszlfm p"
chaieb@23274
  1331
  shows "(\<exists> (x::int). Ifm bbs (x#bs) (minusinf p)) = 
chaieb@23274
  1332
         (\<exists> (x::int)\<in> {1..\<delta> p}. Ifm bbs (x#bs) (minusinf p))"
chaieb@23274
  1333
  (is "(\<exists> x. ?P x) = _")
chaieb@17378
  1334
proof-
chaieb@23274
  1335
  let ?d = "\<delta> p"
chaieb@23274
  1336
  from \<delta> [OF lin] have dpos: "?d >0" by simp
chaieb@23274
  1337
  from \<delta> [OF lin] have alld: "d\<delta> p ?d" by simp
chaieb@23274
  1338
  from minusinf_repeats[OF alld lin] have th1:"\<forall> x k. ?P x = ?P (x - (k * ?d))" by simp
chaieb@23315
  1339
  from periodic_finite_ex[OF dpos th1] show ?thesis by blast
chaieb@17378
  1340
qed
chaieb@17378
  1341
chaieb@17378
  1342
chaieb@23274
  1343
lemma mirror\<alpha>\<beta>:
chaieb@23274
  1344
  assumes lp: "iszlfm p"
chaieb@23274
  1345
  shows "(Inum (i#bs)) ` set (\<alpha> p) = (Inum (i#bs)) ` set (\<beta> (mirror p))"
chaieb@23274
  1346
using lp
chaieb@23274
  1347
by (induct p rule: mirror.induct, auto)
chaieb@17378
  1348
chaieb@23274
  1349
lemma mirror: 
chaieb@23274
  1350
  assumes lp: "iszlfm p"
chaieb@23274
  1351
  shows "Ifm bbs (x#bs) (mirror p) = Ifm bbs ((- x)#bs) p" 
chaieb@23274
  1352
using lp
chaieb@23274
  1353
proof(induct p rule: iszlfm.induct)
chaieb@23274
  1354
  case (9 j c e) hence nb: "numbound0 e" by simp
chaieb@23274
  1355
  have "Ifm bbs (x#bs) (mirror (Dvd j (CX c e))) = (j dvd c*x - Inum (x#bs) e)" (is "_ = (j dvd c*x - ?e)") by simp
chaieb@23274
  1356
    also have "\<dots> = (j dvd (- (c*x - ?e)))"
chaieb@23274
  1357
    by (simp only: zdvd_zminus_iff)
chaieb@23274
  1358
  also have "\<dots> = (j dvd (c* (- x)) + ?e)"
chaieb@23274
  1359
    apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_def zadd_ac zminus_zadd_distrib)
nipkow@23477
  1360
    by (simp add: ring_simps)
chaieb@23274
  1361
  also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CX c e))"
chaieb@23274
  1362
    using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]
chaieb@23274
  1363
    by simp
chaieb@23274
  1364
  finally show ?case .
chaieb@23274
  1365
next
chaieb@23274
  1366
    case (10 j c e) hence nb: "numbound0 e" by simp
chaieb@23274
  1367
  have "Ifm bbs (x#bs) (mirror (Dvd j (CX c e))) = (j dvd c*x - Inum (x#bs) e)" (is "_ = (j dvd c*x - ?e)") by simp
chaieb@23274
  1368
    also have "\<dots> = (j dvd (- (c*x - ?e)))"
chaieb@23274
  1369
    by (simp only: zdvd_zminus_iff)
chaieb@23274
  1370
  also have "\<dots> = (j dvd (c* (- x)) + ?e)"
chaieb@23274
  1371
    apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_def zadd_ac zminus_zadd_distrib)
nipkow@23477
  1372
    by (simp add: ring_simps)
chaieb@23274
  1373
  also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CX c e))"
chaieb@23274
  1374
    using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]
chaieb@23274
  1375
    by simp
chaieb@23274
  1376
  finally show ?case by simp
chaieb@23274
  1377
qed (auto simp add: numbound0_I[where bs="bs" and b="x" and b'="- x"] nth_pos2)
chaieb@17378
  1378
chaieb@23274
  1379
lemma mirror_l: "iszlfm p \<and> d\<beta> p 1 
chaieb@23274
  1380
  \<Longrightarrow> iszlfm (mirror p) \<and> d\<beta> (mirror p) 1"
chaieb@23274
  1381
by (induct p rule: mirror.induct, auto)
chaieb@17378
  1382
chaieb@23274
  1383
lemma mirror_\<delta>: "iszlfm p \<Longrightarrow> \<delta> (mirror p) = \<delta> p"
chaieb@23274
  1384
by (induct p rule: mirror.induct,auto)
chaieb@23274
  1385
chaieb@23274
  1386
lemma \<beta>_numbound0: assumes lp: "iszlfm p"
chaieb@23274
  1387
  shows "\<forall> b\<in> set (\<beta> p). numbound0 b"
chaieb@23274
  1388
  using lp by (induct p rule: \<beta>.induct,auto)
chaieb@17378
  1389
chaieb@23274
  1390
lemma d\<beta>_mono: 
chaieb@23274
  1391
  assumes linp: "iszlfm p"
chaieb@23274
  1392
  and dr: "d\<beta> p l"
chaieb@23274
  1393
  and d: "l dvd l'"
chaieb@23274
  1394
  shows "d\<beta> p l'"
chaieb@23274
  1395
using dr linp zdvd_trans[where n="l" and k="l'", simplified d]
chaieb@23274
  1396
by (induct p rule: iszlfm.induct) simp_all
chaieb@23274
  1397
chaieb@23274
  1398
lemma \<alpha>_l: assumes lp: "iszlfm p"
chaieb@23274
  1399
  shows "\<forall> b\<in> set (\<alpha> p). numbound0 b"
chaieb@23274
  1400
using lp
chaieb@23274
  1401
by(induct p rule: \<alpha>.induct, auto)
chaieb@17378
  1402
chaieb@23274
  1403
lemma \<zeta>: 
chaieb@23274
  1404
  assumes linp: "iszlfm p"
chaieb@23274
  1405
  shows "\<zeta> p > 0 \<and> d\<beta> p (\<zeta> p)"
chaieb@23274
  1406
using linp
chaieb@23274
  1407
proof(induct p rule: iszlfm.induct)
chaieb@23274
  1408
  case (1 p q)
chaieb@23274
  1409
  from prems have dl1: "\<zeta> p dvd ilcm (\<zeta> p) (\<zeta> q)" 
chaieb@23274
  1410
    by (simp add: ilcm_dvd1[where a="\<zeta> p" and b="\<zeta> q"])
chaieb@23274
  1411
  from prems have dl2: "\<zeta> q dvd ilcm (\<zeta> p) (\<zeta> q)" 
chaieb@23274
  1412
    by (simp add: ilcm_dvd2[where a="\<zeta> p" and b="\<zeta> q"])
chaieb@23274
  1413
  from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="ilcm (\<zeta> p) (\<zeta> q)"] 
chaieb@23274
  1414
    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="ilcm (\<zeta> p) (\<zeta> q)"] 
chaieb@23274
  1415
    dl1 dl2 show ?case by (auto simp add: ilcm_pos)
chaieb@17378
  1416
next
chaieb@23274
  1417
  case (2 p q)
chaieb@23274
  1418
  from prems have dl1: "\<zeta> p dvd ilcm (\<zeta> p) (\<zeta> q)" 
chaieb@23274
  1419
    by (simp add: ilcm_dvd1[where a="\<zeta> p" and b="\<zeta> q"])
chaieb@23274
  1420
  from prems have dl2: "\<zeta> q dvd ilcm (\<zeta> p) (\<zeta> q)" 
chaieb@23274
  1421
    by (simp add: ilcm_dvd2[where a="\<zeta> p" and b="\<zeta> q"])
chaieb@23274
  1422
  from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="ilcm (\<zeta> p) (\<zeta> q)"] 
chaieb@23274
  1423
    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="ilcm (\<zeta> p) (\<zeta> q)"] 
chaieb@23274
  1424
    dl1 dl2 show ?case by (auto simp add: ilcm_pos)
chaieb@23274
  1425
qed (auto simp add: ilcm_pos)
chaieb@17378
  1426
chaieb@23274
  1427
lemma a\<beta>: assumes linp: "iszlfm p" and d: "d\<beta> p l" and lp: "l > 0"
chaieb@23274
  1428
  shows "iszlfm (a\<beta> p l) \<and> d\<beta> (a\<beta> p l) 1 \<and> (Ifm bbs (l*x #bs) (a\<beta> p l) = Ifm bbs (x#bs) p)"
chaieb@23274
  1429
using linp d
chaieb@23274
  1430
proof (induct p rule: iszlfm.induct)
chaieb@23274
  1431
  case (5 c e) hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp+
chaieb@23274
  1432
    from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
chaieb@23274
  1433
    from cp have cnz: "c \<noteq> 0" by simp
chaieb@23274
  1434
    have "c div c\<le> l div c"
chaieb@23274
  1435
      by (simp add: zdiv_mono1[OF clel cp])
chaieb@23274
  1436
    then have ldcp:"0 < l div c" 
chaieb@23274
  1437
      by (simp add: zdiv_self[OF cnz])
chaieb@23274
  1438
    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
chaieb@23274
  1439
    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
chaieb@23274
  1440
      by simp
chaieb@23274
  1441
    hence "(l*x + (l div c) * Inum (x # bs) e < 0) =
chaieb@23274
  1442
          ((c * (l div c)) * x + (l div c) * Inum (x # bs) e < 0)"
chaieb@23274
  1443
      by simp
nipkow@23477
  1444
    also have "\<dots> = ((l div c) * (c*x + Inum (x # bs) e) < (l div c) * 0)" by (simp add: ring_simps)
chaieb@23274
  1445
    also have "\<dots> = (c*x + Inum (x # bs) e < 0)"
chaieb@23274
  1446
    using mult_less_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp by simp
chaieb@23274
  1447
  finally show ?case using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be  by simp
chaieb@17378
  1448
next
chaieb@23274
  1449
  case (6 c e) hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp+
chaieb@23274
  1450
    from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
chaieb@23274
  1451
    from cp have cnz: "c \<noteq> 0" by simp
chaieb@23274
  1452
    have "c div c\<le> l div c"
chaieb@23274
  1453
      by (simp add: zdiv_mono1[OF clel cp])
chaieb@23274
  1454
    then have ldcp:"0 < l div c" 
chaieb@23274
  1455
      by (simp add: zdiv_self[OF cnz])
chaieb@23274
  1456
    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
chaieb@23274
  1457
    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
chaieb@17378
  1458
      by simp
chaieb@23274
  1459
    hence "(l*x + (l div c) * Inum (x# bs) e \<le> 0) =
chaieb@23274
  1460
          ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0)"
chaieb@23274
  1461
      by simp
nipkow@23477
  1462
    also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<le> ((l div c)) * 0)" by (simp add: ring_simps)
chaieb@23274
  1463
    also have "\<dots> = (c*x + Inum (x # bs) e \<le> 0)"
chaieb@23274
  1464
    using mult_le_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp by simp
chaieb@23274
  1465
  finally show ?case using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"]  be by simp
chaieb@17378
  1466
next
chaieb@23274
  1467
  case (7 c e) hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp+
chaieb@23274
  1468
    from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
chaieb@23274
  1469
    from cp have cnz: "c \<noteq> 0" by simp
chaieb@23274
  1470
    have "c div c\<le> l div c"
chaieb@23274
  1471
      by (simp add: zdiv_mono1[OF clel cp])
chaieb@23274
  1472
    then have ldcp:"0 < l div c" 
chaieb@23274
  1473
      by (simp add: zdiv_self[OF cnz])
chaieb@23274
  1474
    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
chaieb@23274
  1475
    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
chaieb@17378
  1476
      by simp
chaieb@23274
  1477
    hence "(l*x + (l div c)* Inum (x # bs) e > 0) =
chaieb@23274
  1478
          ((c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0)"
chaieb@17378
  1479
      by simp
nipkow@23477
  1480
    also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) > ((l div c)) * 0)" by (simp add: ring_simps)
chaieb@23274
  1481
    also have "\<dots> = (c * x + Inum (x # bs) e > 0)"
chaieb@23274
  1482
    using zero_less_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp
chaieb@23274
  1483
  finally show ?case using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"]  be  by simp
chaieb@17378
  1484
next
chaieb@23274
  1485
  case (8 c e) hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp+
chaieb@23274
  1486
    from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
chaieb@23274
  1487
    from cp have cnz: "c \<noteq> 0" by simp
chaieb@23274
  1488
    have "c div c\<le> l div c"
chaieb@23274
  1489
      by (simp add: zdiv_mono1[OF clel cp])
chaieb@23274
  1490
    then have ldcp:"0 < l div c" 
chaieb@23274
  1491
      by (simp add: zdiv_self[OF cnz])
chaieb@23274
  1492
    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
chaieb@23274
  1493
    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
chaieb@17378
  1494
      by simp
chaieb@23274
  1495
    hence "(l*x + (l div c)* Inum (x # bs) e \<ge> 0) =
chaieb@23274
  1496
          ((c*(l div c))*x + (l div c)* Inum (x # bs) e \<ge> 0)"
chaieb@23274
  1497
      by simp
chaieb@23274
  1498
    also have "\<dots> = ((l div c)*(c*x + Inum (x # bs) e) \<ge> ((l div c)) * 0)" 
nipkow@23477
  1499
      by (simp add: ring_simps)
chaieb@23274
  1500
    also have "\<dots> = (c*x + Inum (x # bs) e \<ge> 0)" using ldcp 
chaieb@23274
  1501
      zero_le_mult_iff [where a="l div c" and b="c*x + Inum (x # bs) e"] by simp
chaieb@23274
  1502
  finally show ?case using be numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"]  
chaieb@23274
  1503
    by simp
chaieb@17378
  1504
next
chaieb@23274
  1505
  case (3 c e) hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp+
chaieb@23274
  1506
    from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
chaieb@23274
  1507
    from cp have cnz: "c \<noteq> 0" by simp
chaieb@23274
  1508
    have "c div c\<le> l div c"
chaieb@23274
  1509
      by (simp add: zdiv_mono1[OF clel cp])
chaieb@23274
  1510
    then have ldcp:"0 < l div c" 
chaieb@23274
  1511
      by (simp add: zdiv_self[OF cnz])
chaieb@23274
  1512
    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
chaieb@23274
  1513
    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
chaieb@17378
  1514
      by simp
chaieb@23274
  1515
    hence "(l * x + (l div c) * Inum (x # bs) e = 0) =
chaieb@23274
  1516
          ((c * (l div c)) * x + (l div c) * Inum (x # bs) e = 0)"
chaieb@23274
  1517
      by simp
nipkow@23477
  1518
    also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) = ((l div c)) * 0)" by (simp add: ring_simps)
chaieb@23274
  1519
    also have "\<dots> = (c * x + Inum (x # bs) e = 0)"
chaieb@23274
  1520
    using mult_eq_0_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp
chaieb@23274
  1521
  finally show ?case using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"]  be  by simp
chaieb@17378
  1522
next
chaieb@23274
  1523
  case (4 c e) hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp+
chaieb@23274
  1524
    from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
chaieb@23274
  1525
    from cp have cnz: "c \<noteq> 0" by simp
chaieb@23274
  1526
    have "c div c\<le> l div c"
chaieb@23274
  1527
      by (simp add: zdiv_mono1[OF clel cp])
chaieb@23274
  1528
    then have ldcp:"0 < l div c" 
chaieb@23274
  1529
      by (simp add: zdiv_self[OF cnz])
chaieb@23274
  1530
    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
chaieb@23274
  1531
    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
chaieb@23274
  1532
      by simp
chaieb@23274
  1533
    hence "(l * x + (l div c) * Inum (x # bs) e \<noteq> 0) =
chaieb@23274
  1534
          ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<noteq> 0)"
chaieb@23274
  1535
      by simp
nipkow@23477
  1536
    also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<noteq> ((l div c)) * 0)" by (simp add: ring_simps)
chaieb@23274
  1537
    also have "\<dots> = (c * x + Inum (x # bs) e \<noteq> 0)"
chaieb@23274
  1538
    using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp
chaieb@23274
  1539
  finally show ?case using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"]  be  by simp
chaieb@17378
  1540
next
chaieb@23274
  1541
  case (9 j c e) hence cp: "c>0" and be: "numbound0 e" and jp: "j > 0" and d': "c dvd l" by simp+
chaieb@23274
  1542
    from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
chaieb@23274
  1543
    from cp have cnz: "c \<noteq> 0" by simp
chaieb@23274
  1544
    have "c div c\<le> l div c"
chaieb@23274
  1545
      by (simp add: zdiv_mono1[OF clel cp])
chaieb@23274
  1546
    then have ldcp:"0 < l div c" 
chaieb@23274
  1547
      by (simp add: zdiv_self[OF cnz])
chaieb@23274
  1548
    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
chaieb@23274
  1549
    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
chaieb@23274
  1550
      by simp
chaieb@23274
  1551
    hence "(\<exists> (k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = (\<exists> (k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"  by simp
nipkow@23477
  1552
    also have "\<dots> = (\<exists> (k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: ring_simps)
chaieb@23274
  1553
    also have "\<dots> = (\<exists> (k::int). c * x + Inum (x # bs) e - j * k = 0)"
chaieb@23274
  1554
    using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp by simp
chaieb@23274
  1555
  also have "\<dots> = (\<exists> (k::int). c * x + Inum (x # bs) e = j * k)" by simp
chaieb@23274
  1556
  finally show ?case using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be  mult_strict_mono[OF ldcp jp ldcp ] by (simp add: dvd_def)
chaieb@17378
  1557
next
chaieb@23274
  1558
  case (10 j c e) hence cp: "c>0" and be: "numbound0 e" and jp: "j > 0" and d': "c dvd l" by simp+
chaieb@23274
  1559
    from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
chaieb@23274
  1560
    from cp have cnz: "c \<noteq> 0" by simp
chaieb@23274
  1561
    have "c div c\<le> l div c"
chaieb@23274
  1562
      by (simp add: zdiv_mono1[OF clel cp])
chaieb@23274
  1563
    then have ldcp:"0 < l div c" 
chaieb@23274
  1564
      by (simp add: zdiv_self[OF cnz])
chaieb@23274
  1565
    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
chaieb@23274
  1566
    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
chaieb@23274
  1567
      by simp
chaieb@23274
  1568
    hence "(\<exists> (k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = (\<exists> (k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"  by simp
nipkow@23477
  1569
    also have "\<dots> = (\<exists> (k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: ring_simps)
chaieb@23274
  1570
    also have "\<dots> = (\<exists> (k::int). c * x + Inum (x # bs) e - j * k = 0)"
chaieb@23274
  1571
    using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp by simp
chaieb@23274
  1572
  also have "\<dots> = (\<exists> (k::int). c * x + Inum (x # bs) e = j * k)" by simp
chaieb@23274
  1573
  finally show ?case using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be  mult_strict_mono[OF ldcp jp ldcp ] by (simp add: dvd_def)
chaieb@23274
  1574
qed (simp_all add: nth_pos2 numbound0_I[where bs="bs" and b="(l * x)" and b'="x"])
chaieb@17378
  1575
chaieb@23274
  1576
lemma a\<beta>_ex: assumes linp: "iszlfm p" and d: "d\<beta> p l" and lp: "l>0"
chaieb@23274
  1577
  shows "(\<exists> x. l dvd x \<and> Ifm bbs (x #bs) (a\<beta> p l)) = (\<exists> (x::int). Ifm bbs (x#bs) p)"
chaieb@23274
  1578
  (is "(\<exists> x. l dvd x \<and> ?P x) = (\<exists> x. ?P' x)")
chaieb@23274
  1579
proof-
chaieb@23274
  1580
  have "(\<exists> x. l dvd x \<and> ?P x) = (\<exists> (x::int). ?P (l*x))"
chaieb@23274
  1581
    using unity_coeff_ex[where l="l" and P="?P", simplified] by simp
chaieb@23274
  1582
  also have "\<dots> = (\<exists> (x::int). ?P' x)" using a\<beta>[OF linp d lp] by simp
chaieb@23274
  1583
  finally show ?thesis  . 
chaieb@17378
  1584
qed
chaieb@17378
  1585
chaieb@23274
  1586
lemma \<beta>:
chaieb@23274
  1587
  assumes lp: "iszlfm p"
chaieb@23274
  1588
  and u: "d\<beta> p 1"
chaieb@23274
  1589
  and d: "d\<delta> p d"
chaieb@23274
  1590
  and dp: "d > 0"
chaieb@23274
  1591
  and nob: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists> b\<in> (Inum (a#bs)) ` set(\<beta> p). x = b + j)"
chaieb@23274
  1592
  and p: "Ifm bbs (x#bs) p" (is "?P x")
chaieb@23274
  1593
  shows "?P (x - d)"
chaieb@23274
  1594
using lp u d dp nob p
chaieb@23274
  1595
proof(induct p rule: iszlfm.induct)
chaieb@23274
  1596
  case (5 c e) hence c1: "c=1" and  bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
chaieb@23274
  1597
    with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] prems
chaieb@23274
  1598
    show ?case by simp
chaieb@23274
  1599
next
chaieb@23274
  1600
  case (6 c e)  hence c1: "c=1" and  bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
chaieb@23274
  1601
    with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] prems
chaieb@23274
  1602
    show ?case by simp
chaieb@23274
  1603
next
chaieb@23274
  1604
  case (7 c e) hence p: "Ifm bbs (x #bs) (Gt (CX c e))" and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
chaieb@23274
  1605
    let ?e = "Inum (x # bs) e"
chaieb@23274
  1606
    {assume "(x-d) +?e > 0" hence ?case using c1 
chaieb@23274
  1607
      numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp}
chaieb@23274
  1608
    moreover
chaieb@23274
  1609
    {assume H: "\<not> (x-d) + ?e > 0" 
chaieb@23274
  1610
      let ?v="Neg e"
chaieb@23274
  1611
      have vb: "?v \<in> set (\<beta> (Gt (CX c e)))" by simp
chaieb@23274
  1612
      from prems(11)[simplified simp_thms Inum.simps \<beta>.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]] 
chaieb@23274
  1613
      have nob: "\<not> (\<exists> j\<in> {1 ..d}. x =  - ?e + j)" by auto 
chaieb@23274
  1614
      from H p have "x + ?e > 0 \<and> x + ?e \<le> d" by (simp add: c1)
chaieb@23274
  1615
      hence "x + ?e \<ge> 1 \<and> x + ?e \<le> d"  by simp
chaieb@23274
  1616
      hence "\<exists> (j::int) \<in> {1 .. d}. j = x + ?e" by simp
chaieb@23274
  1617
      hence "\<exists> (j::int) \<in> {1 .. d}. x = (- ?e + j)" 
nipkow@23477
  1618
	by (simp add: ring_simps)
chaieb@23274
  1619
      with nob have ?case by auto}
chaieb@23274
  1620
    ultimately show ?case by blast
chaieb@23274
  1621
next
chaieb@23274
  1622
  case (8 c e) hence p: "Ifm bbs (x #bs) (Ge (CX c e))" and c1: "c=1" and bn:"numbound0 e" 
chaieb@23274
  1623
    using dvd1_eq1[where x="c"] by simp+
chaieb@23274
  1624
    let ?e = "Inum (x # bs) e"
chaieb@23274
  1625
    {assume "(x-d) +?e \<ge> 0" hence ?case using  c1 
chaieb@23274
  1626
      numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"]
chaieb@23274
  1627
	by simp}
chaieb@23274
  1628
    moreover
chaieb@23274
  1629
    {assume H: "\<not> (x-d) + ?e \<ge> 0" 
chaieb@23274
  1630
      let ?v="Sub (C -1) e"
chaieb@23274
  1631
      have vb: "?v \<in> set (\<beta> (Ge (CX c e)))" by simp
chaieb@23274
  1632
      from prems(11)[simplified simp_thms Inum.simps \<beta>.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]] 
chaieb@23274
  1633
      have nob: "\<not> (\<exists> j\<in> {1 ..d}. x =  - ?e - 1 + j)" by auto 
chaieb@23274
  1634
      from H p have "x + ?e \<ge> 0 \<and> x + ?e < d" by (simp add: c1)
chaieb@23274
  1635
      hence "x + ?e +1 \<ge> 1 \<and> x + ?e + 1 \<le> d"  by simp
chaieb@23274
  1636
      hence "\<exists> (j::int) \<in> {1 .. d}. j = x + ?e + 1" by simp
nipkow@23477
  1637
      hence "\<exists> (j::int) \<in> {1 .. d}. x= - ?e - 1 + j" by (simp add: ring_simps)
chaieb@23274
  1638
      with nob have ?case by simp }
chaieb@23274
  1639
    ultimately show ?case by blast
chaieb@23274
  1640
next
chaieb@23274
  1641
  case (3 c e) hence p: "Ifm bbs (x #bs) (Eq (CX c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
chaieb@23274
  1642
    let ?e = "Inum (x # bs) e"
chaieb@23274
  1643
    let ?v="(Sub (C -1) e)"
chaieb@23274
  1644
    have vb: "?v \<in> set (\<beta> (Eq (CX c e)))" by simp
chaieb@23274
  1645
    from p have "x= - ?e" by (simp add: c1) with prems(11) show ?case using dp
chaieb@23274
  1646
      by simp (erule ballE[where x="1"],
nipkow@23477
  1647
	simp_all add:ring_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"])
chaieb@23274
  1648
next
chaieb@23274
  1649
  case (4 c e)hence p: "Ifm bbs (x #bs) (NEq (CX c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
chaieb@23274
  1650
    let ?e = "Inum (x # bs) e"
chaieb@23274
  1651
    let ?v="Neg e"
chaieb@23274
  1652
    have vb: "?v \<in> set (\<beta> (NEq (CX c e)))" by simp
chaieb@23274
  1653
    {assume "x - d + Inum (((x -d)) # bs) e \<noteq> 0" 
chaieb@23274
  1654
      hence ?case by (simp add: c1)}
chaieb@23274
  1655
    moreover
chaieb@23274
  1656
    {assume H: "x - d + Inum (((x -d)) # bs) e = 0"
chaieb@23274
  1657
      hence "x = - Inum (((x -d)) # bs) e + d" by simp
chaieb@23274
  1658
      hence "x = - Inum (a # bs) e + d"
chaieb@23274
  1659
	by (simp add: numbound0_I[OF bn,where b="x - d"and b'="a"and bs="bs"])
chaieb@23274
  1660
       with prems(11) have ?case using dp by simp}
chaieb@23274
  1661
  ultimately show ?case by blast
chaieb@23274
  1662
next 
chaieb@23274
  1663
  case (9 j c e) hence p: "Ifm bbs (x #bs) (Dvd j (CX c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
chaieb@23274
  1664
    let ?e = "Inum (x # bs) e"
chaieb@23274
  1665
    from prems have id: "j dvd d" by simp
chaieb@23274
  1666
    from c1 have "?p x = (j dvd (x+ ?e))" by simp
chaieb@23274
  1667
    also have "\<dots> = (j dvd x - d + ?e)" 
chaieb@23274
  1668
      using dvd_period[OF id, where x="x" and c="-1" and t="?e"] by simp
chaieb@23274
  1669
    finally show ?case 
chaieb@23274
  1670
      using numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] c1 p by simp
chaieb@23274
  1671
next
chaieb@23274
  1672
  case (10 j c e) hence p: "Ifm bbs (x #bs) (NDvd j (CX c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
chaieb@23274
  1673
    let ?e = "Inum (x # bs) e"
chaieb@23274
  1674
    from prems have id: "j dvd d" by simp
chaieb@23274
  1675
    from c1 have "?p x = (\<not> j dvd (x+ ?e))" by simp
chaieb@23274
  1676
    also have "\<dots> = (\<not> j dvd x - d + ?e)" 
chaieb@23274
  1677
      using dvd_period[OF id, where x="x" and c="-1" and t="?e"] by simp
chaieb@23274
  1678
    finally show ?case using numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] c1 p by simp
chaieb@23274
  1679
qed (auto simp add: numbound0_I[where bs="bs" and b="(x - d)" and b'="x"] nth_pos2)
chaieb@17378
  1680
chaieb@23274
  1681
lemma \<beta>':   
chaieb@23274
  1682
  assumes lp: "iszlfm p"
chaieb@23274
  1683
  and u: "d\<beta> p 1"
chaieb@23274
  1684
  and d: "d\<delta> p d"
chaieb@23274
  1685
  and dp: "d > 0"
chaieb@23274
  1686
  shows "\<forall> x. \<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists> b\<in> set(\<beta> p). Ifm bbs ((Inum (a#bs) b + j) #bs) p) \<longrightarrow> Ifm bbs (x#bs) p \<longrightarrow> Ifm bbs ((x - d)#bs) p" (is "\<forall> x. ?b \<longrightarrow> ?P x \<longrightarrow> ?P (x - d)")
chaieb@23274
  1687
proof(clarify)
chaieb@23274
  1688
  fix x 
chaieb@23274
  1689
  assume nb:"?b" and px: "?P x" 
chaieb@23274
  1690
  hence nb2: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists> b\<in> (Inum (a#bs)) ` set(\<beta> p). x = b + j)"
chaieb@23274
  1691
    by auto
chaieb@23274
  1692
  from  \<beta>[OF lp u d dp nb2 px] show "?P (x -d )" .
chaieb@17378
  1693
qed
chaieb@23315
  1694
lemma cpmi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. x < z --> (P x = P1 x))
chaieb@23315
  1695
==> ALL x.~(EX (j::int) : {1..D}. EX (b::int) : B. P(b+j)) --> P (x) --> P (x - D) 
chaieb@23315
  1696
==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x-k*D))))
chaieb@23315
  1697
==> (EX (x::int). P(x)) = ((EX (j::int) : {1..D} . (P1(j))) | (EX (j::int) : {1..D}. EX (b::int) : B. P (b+j)))"
chaieb@23315
  1698
apply(rule iffI)
chaieb@23315
  1699
prefer 2
chaieb@23315
  1700
apply(drule minusinfinity)
chaieb@23315
  1701
apply assumption+
chaieb@23315
  1702
apply(fastsimp)
chaieb@23315
  1703
apply clarsimp
chaieb@23315
  1704
apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x - k*D)")
chaieb@23315
  1705
apply(frule_tac x = x and z=z in decr_lemma)
chaieb@23315
  1706
apply(subgoal_tac "P1(x - (\<bar>x - z\<bar> + 1) * D)")
chaieb@23315
  1707
prefer 2
chaieb@23315
  1708
apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)")
chaieb@23315
  1709
prefer 2 apply arith
chaieb@23315
  1710
 apply fastsimp
chaieb@23315
  1711
apply(drule (1)  periodic_finite_ex)
chaieb@23315
  1712
apply blast
chaieb@23315
  1713
apply(blast dest:decr_mult_lemma)
chaieb@23315
  1714
done
chaieb@17378
  1715
chaieb@23274
  1716
theorem cp_thm:
chaieb@23274
  1717
  assumes lp: "iszlfm p"
chaieb@23274
  1718
  and u: "d\<beta> p 1"
chaieb@23274
  1719
  and d: "d\<delta> p d"
chaieb@23274
  1720
  and dp: "d > 0"
chaieb@23274
  1721
  shows "(\<exists> (x::int). Ifm bbs (x #bs) p) = (\<exists> j\<in> {1.. d}. Ifm bbs (j #bs) (minusinf p) \<or> (\<exists> b \<in> set (\<beta> p). Ifm bbs ((Inum (i#bs) b + j) #bs) p))"
chaieb@23274
  1722
  (is "(\<exists> (x::int). ?P (x)) = (\<exists> j\<in> ?D. ?M j \<or> (\<exists> b\<in> ?B. ?P (?I b + j)))")
chaieb@17378
  1723
proof-
chaieb@23274
  1724
  from minusinf_inf[OF lp u] 
chaieb@23274
  1725
  have th: "\<exists>(z::int). \<forall>x<z. ?P (x) = ?M x" by blast
chaieb@23274
  1726
  let ?B' = "{?I b | b. b\<in> ?B}"
chaieb@23274
  1727
  have BB': "(\<exists>j\<in>?D. \<exists>b\<in> ?B. ?P (?I b +j)) = (\<exists> j \<in> ?D. \<exists> b \<in> ?B'. ?P (b + j))" by auto
chaieb@23274
  1728
  hence th2: "\<forall> x. \<not> (\<exists> j \<in> ?D. \<exists> b \<in> ?B'. ?P ((b + j))) \<longrightarrow> ?P (x) \<longrightarrow> ?P ((x - d))" 
chaieb@23274
  1729
    using \<beta>'[OF lp u d dp, where a="i" and bbs = "bbs"] by blast
chaieb@23274
  1730
  from minusinf_repeats[OF d lp]
chaieb@23274
  1731
  have th3: "\<forall> x k. ?M x = ?M (x-k*d)" by simp
chaieb@23274
  1732
  from cpmi_eq[OF dp th th2 th3] BB' show ?thesis by blast
chaieb@17378
  1733
qed
chaieb@17378
  1734
chaieb@23274
  1735
    (* Implement the right hand sides of Cooper's theorem and Ferrante and Rackoff. *)
chaieb@23274
  1736
lemma mirror_ex: 
chaieb@23274
  1737
  assumes lp: "iszlfm p"
chaieb@23274
  1738
  shows "(\<exists> x. Ifm bbs (x#bs) (mirror p)) = (\<exists> x. Ifm bbs (x#bs) p)"
chaieb@23274
  1739
  (is "(\<exists> x. ?I x ?mp) = (\<exists> x. ?I x p)")
chaieb@23274
  1740
proof(auto)
chaieb@23274
  1741
  fix x assume "?I x ?mp" hence "?I (- x) p" using mirror[OF lp] by blast
chaieb@23274
  1742
  thus "\<exists> x. ?I x p" by blast
chaieb@23274
  1743
next
chaieb@23274
  1744
  fix x assume "?I x p" hence "?I (- x) ?mp" 
chaieb@23274
  1745
    using mirror[OF lp, where x="- x", symmetric] by auto
chaieb@23274
  1746
  thus "\<exists> x. ?I x ?mp" by blast
chaieb@23274
  1747
qed
chaieb@23274
  1748
  
chaieb@23274
  1749
  
chaieb@23274
  1750
lemma cp_thm': 
chaieb@23274
  1751
  assumes lp: "iszlfm p"
chaieb@23274
  1752
  and up: "d\<beta> p 1" and dd: "d\<delta> p d" and dp: "d > 0"
chaieb@23274
  1753
  shows "(\<exists> x. Ifm bbs (x#bs) p) = ((\<exists> j\<in> {1 .. d}. Ifm bbs (j#bs) (minusinf p)) \<or> (\<exists> j\<in> {1.. d}. \<exists> b\<in> (Inum (i#bs)) ` set (\<beta> p). Ifm bbs ((b+j)#bs) p))"
chaieb@23274
  1754
  using cp_thm[OF lp up dd dp,where i="i"] by auto
chaieb@17378
  1755
chaieb@23274
  1756
constdefs unit:: "fm \<Rightarrow> fm \<times> num list \<times> int"
chaieb@23274
  1757
  "unit p \<equiv> (let p' = zlfm p ; l = \<zeta> p' ; q = And (Dvd l (CX 1 (C 0))) (a\<beta> p' l); d = \<delta> q;
chaieb@23274
  1758
             B = remdups (map simpnum (\<beta> q)) ; a = remdups (map simpnum (\<alpha> q))
chaieb@23274
  1759
             in if length B \<le> length a then (q,B,d) else (mirror q, a,d))"
chaieb@17378
  1760
chaieb@23274
  1761
lemma unit: assumes qf: "qfree p"
chaieb@23274
  1762
  shows "\<And> q B d. unit p = (q,B,d) \<Longrightarrow> ((\<exists> x. Ifm bbs (x#bs) p) = (\<exists> x. Ifm bbs (x#bs) q)) \<and> (Inum (i#bs)) ` set B = (Inum (i#bs)) ` set (\<beta> q) \<and> d\<beta> q 1 \<and> d\<delta> q d \<and> d >0 \<and> iszlfm q \<and> (\<forall> b\<in> set B. numbound0 b)"
chaieb@23274
  1763
proof-
chaieb@23274
  1764
  fix q B d 
chaieb@23274
  1765
  assume qBd: "unit p = (q,B,d)"
chaieb@23274
  1766
  let ?thes = "((\<exists> x. Ifm bbs (x#bs) p) = (\<exists> x. Ifm bbs (x#bs) q)) \<and>
chaieb@23274
  1767
    Inum (i#bs) ` set B = Inum (i#bs) ` set (\<beta> q) \<and>
chaieb@23274
  1768
    d\<beta> q 1 \<and> d\<delta> q d \<and> 0 < d \<and> iszlfm q \<and> (\<forall> b\<in> set B. numbound0 b)"
chaieb@23274
  1769
  let ?I = "\<lambda> x p. Ifm bbs (x#bs) p"
chaieb@23274
  1770
  let ?p' = "zlfm p"
chaieb@23274
  1771
  let ?l = "\<zeta> ?p'"
chaieb@23274
  1772
  let ?q = "And (Dvd ?l (CX 1 (C 0))) (a\<beta> ?p' ?l)"
chaieb@23274
  1773
  let ?d = "\<delta> ?q"
chaieb@23274
  1774
  let ?B = "set (\<beta> ?q)"
chaieb@23274
  1775
  let ?B'= "remdups (map simpnum (\<beta> ?q))"
chaieb@23274
  1776
  let ?A = "set (\<alpha> ?q)"
chaieb@23274
  1777
  let ?A'= "remdups (map simpnum (\<alpha> ?q))"
chaieb@23274
  1778
  from conjunct1[OF zlfm_I[OF qf, where bs="bs"]] 
chaieb@23274
  1779
  have pp': "\<forall> i. ?I i ?p' = ?I i p" by auto
chaieb@23274
  1780
  from conjunct2[OF zlfm_I[OF qf, where bs="bs" and i="i"]]
chaieb@23274
  1781
  have lp': "iszlfm ?p'" . 
chaieb@23274
  1782
  from lp' \<zeta>[where p="?p'"] have lp: "?l >0" and dl: "d\<beta> ?p' ?l" by auto
chaieb@23274
  1783
  from a\<beta>_ex[where p="?p'" and l="?l" and bs="bs", OF lp' dl lp] pp'
chaieb@23274
  1784
  have pq_ex:"(\<exists> (x::int). ?I x p) = (\<exists> x. ?I x ?q)" by simp 
chaieb@23274
  1785
  from lp' lp a\<beta>[OF lp' dl lp] have lq:"iszlfm ?q" and uq: "d\<beta> ?q 1"  by auto
chaieb@23274
  1786
  from \<delta>[OF lq] have dp:"?d >0" and dd: "d\<delta> ?q ?d" by blast+
chaieb@23274
  1787
  let ?N = "\<lambda> t. Inum (i#bs) t"
chaieb@23274
  1788
  have "?N ` set ?B' = ((?N o simpnum) ` ?B)" by auto 
chaieb@23274
  1789
  also have "\<dots> = ?N ` ?B" using simpnum_ci[where bs="i#bs"] by auto
chaieb@23274
  1790
  finally have BB': "?N ` set ?B' = ?N ` ?B" .
chaieb@23274
  1791
  have "?N ` set ?A' = ((?N o simpnum) ` ?A)" by auto 
chaieb@23274
  1792
  also have "\<dots> = ?N ` ?A" using simpnum_ci[where bs="i#bs"] by auto
chaieb@23274
  1793
  finally have AA': "?N ` set ?A' = ?N ` ?A" .
chaieb@23274
  1794
  from \<beta>_numbound0[OF lq] have B_nb:"\<forall> b\<in> set ?B'. numbound0 b"
chaieb@23274
  1795
    by (simp add: simpnum_numbound0)
chaieb@23274
  1796
  from \<alpha>_l[OF lq] have A_nb: "\<forall> b\<in> set ?A'. numbound0 b"
chaieb@23274
  1797
    by (simp add: simpnum_numbound0)
chaieb@23274
  1798
    {assume "length ?B' \<le> length ?A'"
chaieb@23274
  1799
    hence q:"q=?q" and "B = ?B'" and d:"d = ?d"
chaieb@23274
  1800
      using qBd by (auto simp add: Let_def unit_def)
chaieb@23274
  1801
    with BB' B_nb have b: "?N ` (set B) = ?N ` set (\<beta> q)" 
chaieb@23274
  1802
      and bn: "\<forall>b\<in> set B. numbound0 b" by simp+ 
chaieb@23274
  1803
  with pq_ex dp uq dd lq q d have ?thes by simp}
chaieb@23274
  1804
  moreover 
chaieb@23274
  1805
  {assume "\<not> (length ?B' \<le> length ?A')"
chaieb@23274
  1806
    hence q:"q=mirror ?q" and "B = ?A'" and d:"d = ?d"
chaieb@23274
  1807
      using qBd by (auto simp add: Let_def unit_def)
chaieb@23274
  1808
    with AA' mirror\<alpha>\<beta>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<beta> q)" 
chaieb@23274
  1809
      and bn: "\<forall>b\<in> set B. numbound0 b" by simp+
chaieb@23274
  1810
    from mirror_ex[OF lq] pq_ex q 
chaieb@23274
  1811
    have pqm_eq:"(\<exists> (x::int). ?I x p) = (\<exists> (x::int). ?I x q)" by simp
chaieb@23274
  1812
    from lq uq q mirror_l[where p="?q"]
chaieb@23274
  1813
    have lq': "iszlfm q" and uq: "d\<beta> q 1" by auto
chaieb@23274
  1814
    from \<delta>[OF lq'] mirror_\<delta>[OF lq] q d have dq:"d\<delta> q d " by auto
chaieb@23274
  1815
    from pqm_eq b bn uq lq' dp dq q dp d have ?thes by simp
chaieb@23274
  1816
  }
chaieb@23274
  1817
  ultimately show ?thes by blast
chaieb@23274
  1818
qed
chaieb@23274
  1819
    (* Cooper's Algorithm *)
chaieb@17378
  1820
chaieb@23274
  1821
constdefs cooper :: "fm \<Rightarrow> fm"
chaieb@23274
  1822
  "cooper p \<equiv> 
chaieb@23274
  1823
  (let (q,B,d) = unit p; js = iupt (1,d);
chaieb@23274
  1824
       mq = simpfm (minusinf q);
chaieb@23274
  1825
       md = evaldjf (\<lambda> j. simpfm (subst0 (C j) mq)) js
chaieb@23274
  1826
   in if md = T then T else
chaieb@23274
  1827
    (let qd = evaldjf (\<lambda> (b,j). simpfm (subst0 (Add b (C j)) q)) 
chaieb@23274
  1828
                               (allpairs Pair B js)
chaieb@23274
  1829
     in decr (disj md qd)))"
chaieb@23274
  1830
lemma cooper: assumes qf: "qfree p"
chaieb@23274
  1831
  shows "((\<exists> x. Ifm bbs (x#bs) p) = (Ifm bbs bs (cooper p))) \<and> qfree (cooper p)" 
chaieb@23274
  1832
  (is "(?lhs = ?rhs) \<and> _")
chaieb@23274
  1833
proof-
chaieb@17378
  1834
chaieb@23274
  1835
  let ?I = "\<lambda> x p. Ifm bbs (x#bs) p"
chaieb@23274
  1836
  let ?q = "fst (unit p)"
chaieb@23274
  1837
  let ?B = "fst (snd(unit p))"
chaieb@23274
  1838
  let ?d = "snd (snd (unit p))"
chaieb@23274
  1839
  let ?js = "iupt (1,?d)"
chaieb@23274
  1840
  let ?mq = "minusinf ?q"
chaieb@23274
  1841
  let ?smq = "simpfm ?mq"
chaieb@23274
  1842
  let ?md = "evaldjf (\<lambda> j. simpfm (subst0 (C j) ?smq)) ?js"
chaieb@23274
  1843
  let ?N = "\<lambda> t. Inum (i#bs) t"
chaieb@23274
  1844
  let ?qd = "evaldjf (\<lambda> (b,j). simpfm (subst0 (Add b (C j)) ?q)) (allpairs Pair ?B ?js)"
chaieb@23274
  1845
  have qbf:"unit p = (?q,?B,?d)" by simp
chaieb@23274
  1846
  from unit[OF qf qbf] have pq_ex: "(\<exists>(x::int). ?I x p) = (\<exists> (x::int). ?I x ?q)" and 
chaieb@23274
  1847
    B:"?N ` set ?B = ?N ` set (\<beta> ?q)" and 
chaieb@23274
  1848
    uq:"d\<beta> ?q 1" and dd: "d\<delta> ?q ?d" and dp: "?d > 0" and 
chaieb@23274
  1849
    lq: "iszlfm ?q" and 
chaieb@23274
  1850
    Bn: "\<forall> b\<in> set ?B. numbound0 b" by auto
chaieb@23274
  1851
  from zlin_qfree[OF lq] have qfq: "qfree ?q" .
chaieb@23274
  1852
  from simpfm_qf[OF minusinf_qfree[OF qfq]] have qfmq: "qfree ?smq".
chaieb@23274
  1853
  have jsnb: "\<forall> j \<in> set ?js. numbound0 (C j)" by simp
chaieb@23274
  1854
  hence "\<forall> j\<in> set ?js. bound0 (subst0 (C j) ?smq)" 
chaieb@23274
  1855
    by (auto simp only: subst0_bound0[OF qfmq])
chaieb@23274
  1856
  hence th: "\<forall> j\<in> set ?js. bound0 (simpfm (subst0 (C j) ?smq))"
chaieb@23274
  1857
    by (auto simp add: simpfm_bound0)
chaieb@23274
  1858
  from evaldjf_bound0[OF th] have mdb: "bound0 ?md" by simp 
chaieb@23274
  1859
  from Bn jsnb have "\<forall> (b,j) \<in> set (allpairs Pair ?B ?js). numbound0 (Add b (C j))"
chaieb@23274
  1860
    by (simp add: allpairs_set)
chaieb@23274
  1861
  hence "\<forall> (b,j) \<in> set (allpairs Pair ?B ?js). bound0 (subst0 (Add b (C j)) ?q)"
chaieb@23274
  1862
    using subst0_bound0[OF qfq] by blast
chaieb@23274
  1863
  hence "\<forall> (b,j) \<in> set (allpairs Pair ?B ?js). bound0 (simpfm (subst0 (Add b (C j)) ?q))"
chaieb@23274
  1864
    using simpfm_bound0  by blast
chaieb@23274
  1865
  hence th': "\<forall> x \<in> set (allpairs Pair ?B ?js). bound0 ((\<lambda> (b,j). simpfm (subst0 (Add b (C j)) ?q)) x)"
chaieb@23274
  1866
    by auto 
chaieb@23274
  1867
  from evaldjf_bound0 [OF th'] have qdb: "bound0 ?qd" by simp
chaieb@23274
  1868
  from mdb qdb 
chaieb@23274
  1869
  have mdqdb: "bound0 (disj ?md ?qd)" by (simp only: disj_def, cases "?md=T \<or> ?qd=T", simp_all)
chaieb@23274
  1870
  from trans [OF pq_ex cp_thm'[OF lq uq dd dp,where i="i"]] B
chaieb@23274
  1871
  have "?lhs = (\<exists> j\<in> {1.. ?d}. ?I j ?mq \<or> (\<exists> b\<in> ?N ` set ?B. Ifm bbs ((b+ j)#bs) ?q))" by auto
chaieb@23274
  1872
  also have "\<dots> = (\<exists> j\<in> {1.. ?d}. ?I j ?mq \<or> (\<exists> b\<in> set ?B. Ifm bbs ((?N b+ j)#bs) ?q))" by simp
chaieb@23274
  1873
  also have "\<dots> = ((\<exists> j\<in> {1.. ?d}. ?I j ?mq ) \<or> (\<exists> j\<in> {1.. ?d}. \<exists> b\<in> set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q))" by (simp only: Inum.simps) blast
chaieb@23274
  1874
  also have "\<dots> = ((\<exists> j\<in> {1.. ?d}. ?I j ?smq ) \<or> (\<exists> j\<in> {1.. ?d}. \<exists> b\<in> set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q))" by (simp add: simpfm) 
chaieb@23274
  1875
  also have "\<dots> = ((\<exists> j\<in> set ?js. (\<lambda> j. ?I i (simpfm (subst0 (C j) ?smq))) j) \<or> (\<exists> j\<in> set ?js. \<exists> b\<in> set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q))"
chaieb@23274
  1876
    by (simp only: simpfm subst0_I[OF qfmq] iupt_set) auto
chaieb@23274
  1877
  also have "\<dots> = (?I i (evaldjf (\<lambda> j. simpfm (subst0 (C j) ?smq)) ?js) \<or> (\<exists> j\<in> set ?js. \<exists> b\<in> set ?B. ?I i (subst0 (Add b (C j)) ?q)))" 
chaieb@23274
  1878
   by (simp only: evaldjf_ex subst0_I[OF qfq])
chaieb@23274
  1879
 also have "\<dots>= (?I i ?md \<or> (\<exists> (b,j) \<in> set (allpairs Pair ?B ?js). (\<lambda> (b,j). ?I i (simpfm (subst0 (Add b (C j)) ?q))) (b,j)))"
chaieb@23274
  1880
   by (simp only: simpfm allpairs_set) blast
chaieb@23274
  1881
 also have "\<dots> = (?I i ?md \<or> (?I i (evaldjf (\<lambda> (b,j). simpfm (subst0 (Add b (C j)) ?q)) (allpairs Pair ?B ?js))))"
chaieb@23274
  1882
   by (simp only: evaldjf_ex[where bs="i#bs" and f="\<lambda> (b,j). simpfm (subst0 (Add b (C j)) ?q)" and ps="allpairs Pair ?B ?js"]) (auto simp add: split_def) 
chaieb@23274
  1883
 finally have mdqd: "?lhs = (?I i ?md \<or> ?I i ?qd)" by simp  
chaieb@23274
  1884
  also have "\<dots> = (?I i (disj ?md ?qd))" by (simp add: disj)
chaieb@23274
  1885
  also have "\<dots> = (Ifm bbs bs (decr (disj ?md ?qd)))" by (simp only: decr [OF mdqdb]) 
chaieb@23274
  1886
  finally have mdqd2: "?lhs = (Ifm bbs bs (decr (disj ?md ?qd)))" . 
chaieb@23274
  1887
  {assume mdT: "?md = T"
chaieb@23274
  1888
    hence cT:"cooper p = T" 
chaieb@23274
  1889
      by (simp only: cooper_def unit_def split_def Let_def if_True) simp
chaieb@23274
  1890
    from mdT have lhs:"?lhs" using mdqd by simp 
chaieb@23274
  1891
    from mdT have "?rhs" by (simp add: cooper_def unit_def split_def)
chaieb@23274
  1892
    with lhs cT have ?thesis by simp }
chaieb@17378
  1893
  moreover
chaieb@23274
  1894
  {assume mdT: "?md \<noteq> T" hence "cooper p = decr (disj ?md ?qd)" 
chaieb@23274
  1895
      by (simp only: cooper_def unit_def split_def Let_def if_False) 
chaieb@23274
  1896
    with mdqd2 decr_qf[OF mdqdb] have ?thesis by simp }
chaieb@17378
  1897
  ultimately show ?thesis by blast
chaieb@17378
  1898
qed
chaieb@17378
  1899
chaieb@23274
  1900
constdefs pa:: "fm \<Rightarrow> fm"
chaieb@23274
  1901
  "pa \<equiv> (\<lambda> p. qelim (prep p) cooper)"
chaieb@17378
  1902
chaieb@23274
  1903
theorem mirqe: "(Ifm bbs bs (pa p) = Ifm bbs bs p) \<and> qfree (pa p)"
chaieb@23274
  1904
  using qelim_ci cooper prep by (auto simp add: pa_def)
chaieb@23315
  1905
declare zdvd_iff_zmod_eq_0 [code]
chaieb@17378
  1906
chaieb@23274
  1907
code_module GeneratedCooper
chaieb@23274
  1908
file "generated_cooper.ML"
chaieb@23274
  1909
contains pa = "pa"
chaieb@23274
  1910
test = "%x . pa (E(A(Imp (Ge (Sub (Bound 0) (Bound 1))) (E(E(Eq(Sub(Add(Mul 3 (Bound 1)) (Mul 5 (Bound 0))) (Bound 2))))))))"
chaieb@17378
  1911
chaieb@23274
  1912
ML{* use "generated_cooper.ML"; 
chaieb@23274
  1913
     GeneratedCooper.test (); *}
chaieb@23274
  1914
use "coopereif.ML"
chaieb@23274
  1915
oracle linzqe_oracle ("term") = Coopereif.cooper_oracle
chaieb@23274
  1916
use"coopertac.ML"
chaieb@23274
  1917
setup "LinZTac.setup"
chaieb@17378
  1918
chaieb@23274
  1919
  (* Tests *)
chaieb@23274
  1920
lemma "\<exists> (j::int). \<forall> x\<ge>j. (\<exists> a b. x = 3*a+5*b)"
chaieb@23274
  1921
by cooper
chaieb@17378
  1922
chaieb@23274
  1923
lemma "ALL (x::int) >=8. EX i j. 5*i + 3*j = x" by cooper
chaieb@23274
  1924
theorem "(\<forall>(y::int). 3 dvd y) ==> \<forall>(x::int). b < x --> a \<le> x"
chaieb@23274
  1925
  by cooper
chaieb@17378
  1926
chaieb@23274
  1927
theorem "!! (y::int) (z::int) (n::int). 3 dvd z ==> 2 dvd (y::int) ==>
chaieb@23274
  1928
  (\<exists>(x::int).  2*x =  y) & (\<exists>(k::int). 3*k = z)"
chaieb@23274
  1929
  by cooper
chaieb@23274
  1930
chaieb@23274
  1931
theorem "!! (y::int) (z::int) n. Suc(n::nat) < 6 ==>  3 dvd z ==>
chaieb@23274
  1932
  2 dvd (y::int) ==> (\<exists>(x::int).  2*x =  y) & (\<exists>(k::int). 3*k = z)"
chaieb@23274
  1933
  by cooper
chaieb@23274
  1934
chaieb@23274
  1935
theorem "\<forall>(x::nat). \<exists>(y::nat). (0::nat) \<le> 5 --> y = 5 + x "
chaieb@23274
  1936
  by cooper
chaieb@17378
  1937
chaieb@23274
  1938
lemma "ALL (x::int) >=8. EX i j. 5*i + 3*j = x" by cooper 
chaieb@23274
  1939
lemma "ALL (y::int) (z::int) (n::int). 3 dvd z --> 2 dvd (y::int) --> (EX (x::int).  2*x =  y) & (EX (k::int). 3*k = z)" by cooper
chaieb@23274
  1940
lemma "ALL(x::int) y. x < y --> 2 * x + 1 < 2 * y" by cooper
chaieb@23274
  1941
lemma "ALL(x::int) y. 2 * x + 1 ~= 2 * y" by cooper
chaieb@23274
  1942
lemma "EX(x::int) y. 0 < x  & 0 <= y  & 3 * x - 5 * y = 1" by cooper
chaieb@23274
  1943
lemma "~ (EX(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)" by cooper
chaieb@23274
  1944
lemma "ALL(x::int). (2 dvd x) --> (EX(y::int). x = 2*y)" by cooper
chaieb@23274
  1945
lemma "ALL(x::int). (2 dvd x) --> (EX(y::int). x = 2*y)" by cooper
chaieb@23274
  1946
lemma "ALL(x::int). (2 dvd x) = (EX(y::int). x = 2*y)" by cooper
chaieb@23274
  1947
lemma "ALL(x::int). ((2 dvd x) = (ALL(y::int). x ~= 2*y + 1))" by cooper
chaieb@23274
  1948
lemma "~ (ALL(x::int). ((2 dvd x) = (ALL(y::int). x ~= 2*y+1) | (EX(q::int) (u::int) i. 3*i + 2*q - u < 17) --> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))" by cooper
chaieb@23274
  1949
lemma "~ (ALL(i::int). 4 <= i --> (EX x y. 0 <= x & 0 <= y & 3 * x + 5 * y = i))" 
chaieb@23274
  1950
  by cooper
chaieb@23274
  1951
lemma "EX j. ALL (x::int) >= j. EX i j. 5*i + 3*j = x" by cooper
chaieb@17378
  1952
chaieb@23274
  1953
theorem "(\<forall>(y::int). 3 dvd y) ==> \<forall>(x::int). b < x --> a \<le> x"
chaieb@23274
  1954
  by cooper
chaieb@17378
  1955
chaieb@23274
  1956
theorem "!! (y::int) (z::int) (n::int). 3 dvd z ==> 2 dvd (y::int) ==>
chaieb@23274
  1957
  (\<exists>(x::int).  2*x =  y) & (\<exists>(k::int). 3*k = z)"
chaieb@23274
  1958
  by cooper
chaieb@17378
  1959
chaieb@23274
  1960
theorem "!! (y::int) (z::int) n. Suc(n::nat) < 6 ==>  3 dvd z ==>
chaieb@23274
  1961
  2 dvd (y::int) ==> (\<exists>(x::int).  2*x =  y) & (\<exists>(k::int). 3*k = z)"
chaieb@23274
  1962
  by cooper
chaieb@17378
  1963
chaieb@23274
  1964
theorem "\<forall>(x::nat). \<exists>(y::nat). (0::nat) \<le> 5 --> y = 5 + x "
chaieb@23274
  1965
  by cooper
chaieb@17378
  1966
chaieb@23274
  1967
theorem "\<forall>(x::nat). \<exists>(y::nat). y = 5 + x | x div 6 + 1= 2"
chaieb@23274
  1968
  by cooper
chaieb@17378
  1969
chaieb@23274
  1970
theorem "\<exists>(x::int). 0 < x"
chaieb@23274
  1971
  by cooper
chaieb@17378
  1972
chaieb@23274
  1973
theorem "\<forall>(x::int) y. x < y --> 2 * x + 1 < 2 * y"
chaieb@23274
  1974
  by cooper
chaieb@23274
  1975
 
chaieb@23274
  1976
theorem "\<forall>(x::int) y. 2 * x + 1 \<noteq> 2 * y"
chaieb@23274
  1977
  by cooper
chaieb@23274
  1978
 
chaieb@23274
  1979
theorem "\<exists>(x::int) y. 0 < x  & 0 \<le> y  & 3 * x - 5 * y = 1"
chaieb@23274
  1980
  by cooper
chaieb@17378
  1981
chaieb@23274
  1982
theorem "~ (\<exists>(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)"
chaieb@23274
  1983
  by cooper
chaieb@17378
  1984
chaieb@23274
  1985
theorem "~ (\<exists>(x::int). False)"
chaieb@23274
  1986
  by cooper
chaieb@17378
  1987
chaieb@23274
  1988
theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)"
chaieb@23274
  1989
  by cooper 
chaieb@23274
  1990
chaieb@23274
  1991
theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)"
chaieb@23274
  1992
  by cooper 
chaieb@17378
  1993
chaieb@23274
  1994
theorem "\<forall>(x::int). (2 dvd x) = (\<exists>(y::int). x = 2*y)"
chaieb@23274
  1995
  by cooper 
chaieb@17378
  1996
chaieb@23274
  1997
theorem "\<forall>(x::int). ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y + 1))"
chaieb@23274
  1998
  by cooper 
chaieb@17378
  1999
chaieb@23274
  2000
theorem "~ (\<forall>(x::int). 
chaieb@23274
  2001
            ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y+1) | 
chaieb@23274
  2002
             (\<exists>(q::int) (u::int) i. 3*i + 2*q - u < 17)
chaieb@23274
  2003
             --> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))"
chaieb@23274
  2004
  by cooper
chaieb@23274
  2005
 
chaieb@23274
  2006
theorem "~ (\<forall>(i::int). 4 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))"
chaieb@23274
  2007
  by cooper
chaieb@17378
  2008
chaieb@23274
  2009
theorem "\<forall>(i::int). 8 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i)"
chaieb@23274
  2010
  by cooper
chaieb@17378
  2011
chaieb@23274
  2012
theorem "\<exists>(j::int). \<forall>i. j \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i)"
chaieb@23274
  2013
  by cooper
chaieb@17378
  2014
chaieb@23274
  2015
theorem "~ (\<forall>j (i::int). j \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))"
chaieb@23274
  2016
  by cooper
chaieb@17378
  2017
chaieb@23274
  2018
theorem "(\<exists>m::nat. n = 2 * m) --> (n + 1) div 2 = n div 2"
chaieb@23274
  2019
  by cooper
wenzelm@17388
  2020
chaieb@17378
  2021
end