src/HOL/Decision_Procs/Cooper.thy
author wenzelm
Fri Mar 07 22:30:58 2014 +0100 (2014-03-07)
changeset 55990 41c6b99c5fb7
parent 55981 66739f41d5b2
child 55999 6477fc70cfa0
permissions -rw-r--r--
more antiquotations;
hoelzl@30439
     1
(*  Title:      HOL/Decision_Procs/Cooper.thy
haftmann@27456
     2
    Author:     Amine Chaieb
haftmann@27456
     3
*)
haftmann@27456
     4
haftmann@29788
     5
theory Cooper
wenzelm@55885
     6
imports
wenzelm@55885
     7
  Complex_Main
wenzelm@55885
     8
  "~~/src/HOL/Library/Code_Target_Numeral"
wenzelm@55885
     9
  "~~/src/HOL/Library/Old_Recdef"
nipkow@23477
    10
begin
chaieb@17378
    11
chaieb@17378
    12
(* Periodicity of dvd *)
chaieb@23315
    13
wenzelm@55885
    14
(*********************************************************************************)
wenzelm@55885
    15
(****                            SHADOW SYNTAX AND SEMANTICS                  ****)
wenzelm@55885
    16
(*********************************************************************************)
chaieb@23274
    17
wenzelm@50313
    18
datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
chaieb@23274
    19
  | Mul int num
chaieb@23274
    20
wenzelm@50313
    21
primrec num_size :: "num \<Rightarrow> nat" -- {* A size for num to make inductive proofs simpler *}
wenzelm@50313
    22
where
chaieb@23274
    23
  "num_size (C c) = 1"
haftmann@27456
    24
| "num_size (Bound n) = 1"
haftmann@27456
    25
| "num_size (Neg a) = 1 + num_size a"
haftmann@27456
    26
| "num_size (Add a b) = 1 + num_size a + num_size b"
haftmann@27456
    27
| "num_size (Sub a b) = 3 + num_size a + num_size b"
haftmann@27456
    28
| "num_size (CN n c a) = 4 + num_size a"
haftmann@27456
    29
| "num_size (Mul c a) = 1 + num_size a"
chaieb@17378
    30
wenzelm@55844
    31
primrec Inum :: "int list \<Rightarrow> num \<Rightarrow> int"
wenzelm@55844
    32
where
chaieb@23274
    33
  "Inum bs (C c) = c"
haftmann@27456
    34
| "Inum bs (Bound n) = bs!n"
haftmann@27456
    35
| "Inum bs (CN n c a) = c * (bs!n) + (Inum bs a)"
haftmann@27456
    36
| "Inum bs (Neg a) = -(Inum bs a)"
haftmann@27456
    37
| "Inum bs (Add a b) = Inum bs a + Inum bs b"
haftmann@27456
    38
| "Inum bs (Sub a b) = Inum bs a - Inum bs b"
haftmann@27456
    39
| "Inum bs (Mul c a) = c* Inum bs a"
chaieb@23274
    40
wenzelm@50313
    41
datatype fm  =
chaieb@23274
    42
  T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num|
wenzelm@50313
    43
  NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
chaieb@23274
    44
  | Closed nat | NClosed nat
chaieb@23274
    45
chaieb@23274
    46
wenzelm@50313
    47
fun fmsize :: "fm \<Rightarrow> nat"  -- {* A size for fm *}
wenzelm@50313
    48
where
chaieb@23274
    49
  "fmsize (NOT p) = 1 + fmsize p"
krauss@41837
    50
| "fmsize (And p q) = 1 + fmsize p + fmsize q"
krauss@41837
    51
| "fmsize (Or p q) = 1 + fmsize p + fmsize q"
krauss@41837
    52
| "fmsize (Imp p q) = 3 + fmsize p + fmsize q"
krauss@41837
    53
| "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)"
krauss@41837
    54
| "fmsize (E p) = 1 + fmsize p"
krauss@41837
    55
| "fmsize (A p) = 4+ fmsize p"
krauss@41837
    56
| "fmsize (Dvd i t) = 2"
krauss@41837
    57
| "fmsize (NDvd i t) = 2"
krauss@41837
    58
| "fmsize p = 1"
wenzelm@50313
    59
wenzelm@32960
    60
lemma fmsize_pos: "fmsize p > 0"
wenzelm@32960
    61
  by (induct p rule: fmsize.induct) simp_all
chaieb@17378
    62
wenzelm@50313
    63
primrec Ifm :: "bool list \<Rightarrow> int list \<Rightarrow> fm \<Rightarrow> bool"  -- {* Semantics of formulae (fm) *}
wenzelm@50313
    64
where
wenzelm@55981
    65
  "Ifm bbs bs T \<longleftrightarrow> True"
wenzelm@55981
    66
| "Ifm bbs bs F \<longleftrightarrow> False"
wenzelm@55981
    67
| "Ifm bbs bs (Lt a) \<longleftrightarrow> Inum bs a < 0"
wenzelm@55981
    68
| "Ifm bbs bs (Gt a) \<longleftrightarrow> Inum bs a > 0"
wenzelm@55981
    69
| "Ifm bbs bs (Le a) \<longleftrightarrow> Inum bs a \<le> 0"
wenzelm@55981
    70
| "Ifm bbs bs (Ge a) \<longleftrightarrow> Inum bs a \<ge> 0"
wenzelm@55981
    71
| "Ifm bbs bs (Eq a) \<longleftrightarrow> Inum bs a = 0"
wenzelm@55981
    72
| "Ifm bbs bs (NEq a) \<longleftrightarrow> Inum bs a \<noteq> 0"
wenzelm@55981
    73
| "Ifm bbs bs (Dvd i b) \<longleftrightarrow> i dvd Inum bs b"
wenzelm@55981
    74
| "Ifm bbs bs (NDvd i b) \<longleftrightarrow> \<not> i dvd Inum bs b"
wenzelm@55981
    75
| "Ifm bbs bs (NOT p) \<longleftrightarrow> \<not> Ifm bbs bs p"
wenzelm@55981
    76
| "Ifm bbs bs (And p q) \<longleftrightarrow> Ifm bbs bs p \<and> Ifm bbs bs q"
wenzelm@55981
    77
| "Ifm bbs bs (Or p q) \<longleftrightarrow> Ifm bbs bs p \<or> Ifm bbs bs q"
wenzelm@55981
    78
| "Ifm bbs bs (Imp p q) \<longleftrightarrow> (Ifm bbs bs p \<longrightarrow> Ifm bbs bs q)"
wenzelm@55981
    79
| "Ifm bbs bs (Iff p q) \<longleftrightarrow> Ifm bbs bs p = Ifm bbs bs q"
wenzelm@55981
    80
| "Ifm bbs bs (E p) \<longleftrightarrow> (\<exists>x. Ifm bbs (x # bs) p)"
wenzelm@55981
    81
| "Ifm bbs bs (A p) \<longleftrightarrow> (\<forall>x. Ifm bbs (x # bs) p)"
wenzelm@55981
    82
| "Ifm bbs bs (Closed n) \<longleftrightarrow> bbs!n"
wenzelm@55981
    83
| "Ifm bbs bs (NClosed n) \<longleftrightarrow> \<not> bbs!n"
chaieb@23274
    84
chaieb@23274
    85
consts prep :: "fm \<Rightarrow> fm"
chaieb@23274
    86
recdef prep "measure fmsize"
chaieb@23274
    87
  "prep (E T) = T"
chaieb@23274
    88
  "prep (E F) = F"
chaieb@23274
    89
  "prep (E (Or p q)) = Or (prep (E p)) (prep (E q))"
chaieb@23274
    90
  "prep (E (Imp p q)) = Or (prep (E (NOT p))) (prep (E q))"
wenzelm@50313
    91
  "prep (E (Iff p q)) = Or (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))"
chaieb@23274
    92
  "prep (E (NOT (And p q))) = Or (prep (E (NOT p))) (prep (E(NOT q)))"
chaieb@23274
    93
  "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))"
chaieb@23274
    94
  "prep (E (NOT (Iff p q))) = Or (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))"
chaieb@23274
    95
  "prep (E p) = E (prep p)"
chaieb@23274
    96
  "prep (A (And p q)) = And (prep (A p)) (prep (A q))"
chaieb@23274
    97
  "prep (A p) = prep (NOT (E (NOT p)))"
chaieb@23274
    98
  "prep (NOT (NOT p)) = prep p"
chaieb@23274
    99
  "prep (NOT (And p q)) = Or (prep (NOT p)) (prep (NOT q))"
chaieb@23274
   100
  "prep (NOT (A p)) = prep (E (NOT p))"
chaieb@23274
   101
  "prep (NOT (Or p q)) = And (prep (NOT p)) (prep (NOT q))"
chaieb@23274
   102
  "prep (NOT (Imp p q)) = And (prep p) (prep (NOT q))"
chaieb@23274
   103
  "prep (NOT (Iff p q)) = Or (prep (And p (NOT q))) (prep (And (NOT p) q))"
chaieb@23274
   104
  "prep (NOT p) = NOT (prep p)"
chaieb@23274
   105
  "prep (Or p q) = Or (prep p) (prep q)"
chaieb@23274
   106
  "prep (And p q) = And (prep p) (prep q)"
chaieb@23274
   107
  "prep (Imp p q) = prep (Or (NOT p) q)"
chaieb@23274
   108
  "prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))"
chaieb@23274
   109
  "prep p = p"
wenzelm@50313
   110
  (hints simp add: fmsize_pos)
wenzelm@50313
   111
chaieb@23274
   112
lemma prep: "Ifm bbs bs (prep p) = Ifm bbs bs p"
wenzelm@50313
   113
  by (induct p arbitrary: bs rule: prep.induct) auto
chaieb@23274
   114
chaieb@17378
   115
wenzelm@50313
   116
fun qfree :: "fm \<Rightarrow> bool"  -- {* Quantifier freeness *}
wenzelm@50313
   117
where
chaieb@23274
   118
  "qfree (E p) = False"
krauss@41837
   119
| "qfree (A p) = False"
wenzelm@50313
   120
| "qfree (NOT p) = qfree p"
wenzelm@50313
   121
| "qfree (And p q) = (qfree p \<and> qfree q)"
wenzelm@50313
   122
| "qfree (Or  p q) = (qfree p \<and> qfree q)"
wenzelm@50313
   123
| "qfree (Imp p q) = (qfree p \<and> qfree q)"
krauss@41837
   124
| "qfree (Iff p q) = (qfree p \<and> qfree q)"
krauss@41837
   125
| "qfree p = True"
chaieb@23274
   126
wenzelm@50313
   127
wenzelm@50313
   128
text {* Boundedness and substitution *}
wenzelm@50313
   129
wenzelm@50313
   130
primrec numbound0 :: "num \<Rightarrow> bool"  -- {* a num is INDEPENDENT of Bound 0 *}
wenzelm@50313
   131
where
wenzelm@55981
   132
  "numbound0 (C c) \<longleftrightarrow> True"
wenzelm@55981
   133
| "numbound0 (Bound n) \<longleftrightarrow> n > 0"
wenzelm@55981
   134
| "numbound0 (CN n i a) \<longleftrightarrow> n > 0 \<and> numbound0 a"
wenzelm@55981
   135
| "numbound0 (Neg a) \<longleftrightarrow> numbound0 a"
wenzelm@55981
   136
| "numbound0 (Add a b) \<longleftrightarrow> numbound0 a \<and> numbound0 b"
wenzelm@55981
   137
| "numbound0 (Sub a b) \<longleftrightarrow> numbound0 a \<and> numbound0 b"
wenzelm@55981
   138
| "numbound0 (Mul i a) \<longleftrightarrow> numbound0 a"
chaieb@23274
   139
chaieb@23274
   140
lemma numbound0_I:
chaieb@23274
   141
  assumes nb: "numbound0 a"
wenzelm@55981
   142
  shows "Inum (b # bs) a = Inum (b' # bs) a"
wenzelm@50313
   143
  using nb by (induct a rule: num.induct) (auto simp add: gr0_conv_Suc)
chaieb@17378
   144
wenzelm@50313
   145
primrec bound0 :: "fm \<Rightarrow> bool" -- {* A Formula is independent of Bound 0 *}
wenzelm@50313
   146
where
wenzelm@55981
   147
  "bound0 T \<longleftrightarrow> True"
wenzelm@55981
   148
| "bound0 F \<longleftrightarrow> True"
wenzelm@55981
   149
| "bound0 (Lt a) \<longleftrightarrow> numbound0 a"
wenzelm@55981
   150
| "bound0 (Le a) \<longleftrightarrow> numbound0 a"
wenzelm@55981
   151
| "bound0 (Gt a) \<longleftrightarrow> numbound0 a"
wenzelm@55981
   152
| "bound0 (Ge a) \<longleftrightarrow> numbound0 a"
wenzelm@55981
   153
| "bound0 (Eq a) \<longleftrightarrow> numbound0 a"
wenzelm@55981
   154
| "bound0 (NEq a) \<longleftrightarrow> numbound0 a"
wenzelm@55981
   155
| "bound0 (Dvd i a) \<longleftrightarrow> numbound0 a"
wenzelm@55981
   156
| "bound0 (NDvd i a) \<longleftrightarrow> numbound0 a"
wenzelm@55981
   157
| "bound0 (NOT p) \<longleftrightarrow> bound0 p"
wenzelm@55981
   158
| "bound0 (And p q) \<longleftrightarrow> bound0 p \<and> bound0 q"
wenzelm@55981
   159
| "bound0 (Or p q) \<longleftrightarrow> bound0 p \<and> bound0 q"
wenzelm@55981
   160
| "bound0 (Imp p q) \<longleftrightarrow> bound0 p \<and> bound0 q"
wenzelm@55981
   161
| "bound0 (Iff p q) \<longleftrightarrow> bound0 p \<and> bound0 q"
wenzelm@55981
   162
| "bound0 (E p) \<longleftrightarrow> False"
wenzelm@55981
   163
| "bound0 (A p) \<longleftrightarrow> False"
wenzelm@55981
   164
| "bound0 (Closed P) \<longleftrightarrow> True"
wenzelm@55981
   165
| "bound0 (NClosed P) \<longleftrightarrow> True"
wenzelm@50313
   166
chaieb@23274
   167
lemma bound0_I:
chaieb@23274
   168
  assumes bp: "bound0 p"
wenzelm@55981
   169
  shows "Ifm bbs (b # bs) p = Ifm bbs (b' # bs) p"
wenzelm@50313
   170
  using bp numbound0_I[where b="b" and bs="bs" and b'="b'"]
wenzelm@50313
   171
  by (induct p rule: fm.induct) (auto simp add: gr0_conv_Suc)
chaieb@23274
   172
wenzelm@50313
   173
fun numsubst0 :: "num \<Rightarrow> num \<Rightarrow> num"
wenzelm@50313
   174
where
chaieb@23274
   175
  "numsubst0 t (C c) = (C c)"
chaieb@23995
   176
| "numsubst0 t (Bound n) = (if n=0 then t else Bound n)"
chaieb@23995
   177
| "numsubst0 t (CN 0 i a) = Add (Mul i t) (numsubst0 t a)"
chaieb@23995
   178
| "numsubst0 t (CN n i a) = CN n i (numsubst0 t a)"
chaieb@23995
   179
| "numsubst0 t (Neg a) = Neg (numsubst0 t a)"
chaieb@23995
   180
| "numsubst0 t (Add a b) = Add (numsubst0 t a) (numsubst0 t b)"
wenzelm@50313
   181
| "numsubst0 t (Sub a b) = Sub (numsubst0 t a) (numsubst0 t b)"
chaieb@23995
   182
| "numsubst0 t (Mul i a) = Mul i (numsubst0 t a)"
chaieb@23274
   183
wenzelm@50313
   184
lemma numsubst0_I: "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t"
wenzelm@50313
   185
  by (induct t rule: numsubst0.induct) (auto simp: nth_Cons')
chaieb@17378
   186
chaieb@23274
   187
lemma numsubst0_I':
nipkow@25134
   188
  "numbound0 a \<Longrightarrow> Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t"
wenzelm@50313
   189
  by (induct t rule: numsubst0.induct) (auto simp: nth_Cons' numbound0_I[where b="b" and b'="b'"])
chaieb@23274
   190
wenzelm@50313
   191
primrec subst0:: "num \<Rightarrow> fm \<Rightarrow> fm"  -- {* substitue a num into a formula for Bound 0 *}
wenzelm@50313
   192
where
chaieb@23274
   193
  "subst0 t T = T"
haftmann@39246
   194
| "subst0 t F = F"
haftmann@39246
   195
| "subst0 t (Lt a) = Lt (numsubst0 t a)"
haftmann@39246
   196
| "subst0 t (Le a) = Le (numsubst0 t a)"
haftmann@39246
   197
| "subst0 t (Gt a) = Gt (numsubst0 t a)"
haftmann@39246
   198
| "subst0 t (Ge a) = Ge (numsubst0 t a)"
haftmann@39246
   199
| "subst0 t (Eq a) = Eq (numsubst0 t a)"
haftmann@39246
   200
| "subst0 t (NEq a) = NEq (numsubst0 t a)"
haftmann@39246
   201
| "subst0 t (Dvd i a) = Dvd i (numsubst0 t a)"
haftmann@39246
   202
| "subst0 t (NDvd i a) = NDvd i (numsubst0 t a)"
haftmann@39246
   203
| "subst0 t (NOT p) = NOT (subst0 t p)"
haftmann@39246
   204
| "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"
haftmann@39246
   205
| "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"
haftmann@39246
   206
| "subst0 t (Imp p q) = Imp (subst0 t p) (subst0 t q)"
haftmann@39246
   207
| "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
haftmann@39246
   208
| "subst0 t (Closed P) = (Closed P)"
haftmann@39246
   209
| "subst0 t (NClosed P) = (NClosed P)"
chaieb@23274
   210
wenzelm@50313
   211
lemma subst0_I:
wenzelm@50313
   212
  assumes qfp: "qfree p"
wenzelm@55885
   213
  shows "Ifm bbs (b # bs) (subst0 a p) = Ifm bbs (Inum (b # bs) a # bs) p"
chaieb@23274
   214
  using qfp numsubst0_I[where b="b" and bs="bs" and a="a"]
haftmann@23689
   215
  by (induct p) (simp_all add: gr0_conv_Suc)
chaieb@23274
   216
wenzelm@50313
   217
fun decrnum:: "num \<Rightarrow> num"
wenzelm@50313
   218
where
chaieb@23274
   219
  "decrnum (Bound n) = Bound (n - 1)"
krauss@41837
   220
| "decrnum (Neg a) = Neg (decrnum a)"
krauss@41837
   221
| "decrnum (Add a b) = Add (decrnum a) (decrnum b)"
krauss@41837
   222
| "decrnum (Sub a b) = Sub (decrnum a) (decrnum b)"
krauss@41837
   223
| "decrnum (Mul c a) = Mul c (decrnum a)"
krauss@41837
   224
| "decrnum (CN n i a) = (CN (n - 1) i (decrnum a))"
krauss@41837
   225
| "decrnum a = a"
chaieb@17378
   226
wenzelm@50313
   227
fun decr :: "fm \<Rightarrow> fm"
wenzelm@50313
   228
where
chaieb@23274
   229
  "decr (Lt a) = Lt (decrnum a)"
krauss@41837
   230
| "decr (Le a) = Le (decrnum a)"
krauss@41837
   231
| "decr (Gt a) = Gt (decrnum a)"
krauss@41837
   232
| "decr (Ge a) = Ge (decrnum a)"
krauss@41837
   233
| "decr (Eq a) = Eq (decrnum a)"
krauss@41837
   234
| "decr (NEq a) = NEq (decrnum a)"
krauss@41837
   235
| "decr (Dvd i a) = Dvd i (decrnum a)"
krauss@41837
   236
| "decr (NDvd i a) = NDvd i (decrnum a)"
wenzelm@50313
   237
| "decr (NOT p) = NOT (decr p)"
krauss@41837
   238
| "decr (And p q) = And (decr p) (decr q)"
krauss@41837
   239
| "decr (Or p q) = Or (decr p) (decr q)"
krauss@41837
   240
| "decr (Imp p q) = Imp (decr p) (decr q)"
krauss@41837
   241
| "decr (Iff p q) = Iff (decr p) (decr q)"
krauss@41837
   242
| "decr p = p"
chaieb@23274
   243
wenzelm@50313
   244
lemma decrnum:
wenzelm@50313
   245
  assumes nb: "numbound0 t"
wenzelm@55885
   246
  shows "Inum (x # bs) t = Inum bs (decrnum t)"
wenzelm@50313
   247
  using nb by (induct t rule: decrnum.induct) (auto simp add: gr0_conv_Suc)
chaieb@23274
   248
wenzelm@50313
   249
lemma decr:
wenzelm@50313
   250
  assumes nb: "bound0 p"
wenzelm@55885
   251
  shows "Ifm bbs (x # bs) p = Ifm bbs bs (decr p)"
wenzelm@50313
   252
  using nb by (induct p rule: decr.induct) (simp_all add: gr0_conv_Suc decrnum)
chaieb@23274
   253
chaieb@23274
   254
lemma decr_qf: "bound0 p \<Longrightarrow> qfree (decr p)"
wenzelm@50313
   255
  by (induct p) simp_all
chaieb@23274
   256
wenzelm@50313
   257
fun isatom :: "fm \<Rightarrow> bool"  -- {* test for atomicity *}
wenzelm@50313
   258
where
wenzelm@55981
   259
  "isatom T \<longleftrightarrow> True"
wenzelm@55981
   260
| "isatom F \<longleftrightarrow> True"
wenzelm@55981
   261
| "isatom (Lt a) \<longleftrightarrow> True"
wenzelm@55981
   262
| "isatom (Le a) \<longleftrightarrow> True"
wenzelm@55981
   263
| "isatom (Gt a) \<longleftrightarrow> True"
wenzelm@55981
   264
| "isatom (Ge a) \<longleftrightarrow> True"
wenzelm@55981
   265
| "isatom (Eq a) \<longleftrightarrow> True"
wenzelm@55981
   266
| "isatom (NEq a) \<longleftrightarrow> True"
wenzelm@55981
   267
| "isatom (Dvd i b) \<longleftrightarrow> True"
wenzelm@55981
   268
| "isatom (NDvd i b) \<longleftrightarrow> True"
wenzelm@55981
   269
| "isatom (Closed P) \<longleftrightarrow> True"
wenzelm@55981
   270
| "isatom (NClosed P) \<longleftrightarrow> True"
wenzelm@55981
   271
| "isatom p \<longleftrightarrow> False"
chaieb@17378
   272
wenzelm@50313
   273
lemma numsubst0_numbound0:
wenzelm@55844
   274
  assumes "numbound0 t"
chaieb@23274
   275
  shows "numbound0 (numsubst0 t a)"
wenzelm@55844
   276
  using assms
wenzelm@55844
   277
  apply (induct a)
wenzelm@50313
   278
  apply simp_all
wenzelm@55844
   279
  apply (case_tac nat)
wenzelm@55844
   280
  apply simp_all
wenzelm@50313
   281
  done
chaieb@23274
   282
wenzelm@50313
   283
lemma subst0_bound0:
wenzelm@55844
   284
  assumes qf: "qfree p"
wenzelm@55844
   285
    and nb: "numbound0 t"
chaieb@23274
   286
  shows "bound0 (subst0 t p)"
wenzelm@50313
   287
  using qf numsubst0_numbound0[OF nb] by (induct p) auto
chaieb@23274
   288
chaieb@23274
   289
lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p"
wenzelm@50313
   290
  by (induct p) simp_all
chaieb@23274
   291
chaieb@23274
   292
wenzelm@50313
   293
definition djf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm"
wenzelm@50313
   294
where
wenzelm@50313
   295
  "djf f p q =
wenzelm@55885
   296
   (if q = T then T
wenzelm@55885
   297
    else if q = F then f p
wenzelm@55885
   298
    else
wenzelm@55885
   299
      let fp = f p
wenzelm@55885
   300
      in case fp of T \<Rightarrow> T | F \<Rightarrow> q | _ \<Rightarrow> Or (f p) q)"
wenzelm@50313
   301
wenzelm@50313
   302
definition evaldjf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm"
wenzelm@50313
   303
  where "evaldjf f ps = foldr (djf f) ps F"
chaieb@23274
   304
chaieb@23274
   305
lemma djf_Or: "Ifm bbs bs (djf f p q) = Ifm bbs bs (Or (f p) q)"
wenzelm@55885
   306
  by (cases "q=T", simp add: djf_def, cases "q = F", simp add: djf_def)
wenzelm@50313
   307
    (cases "f p", simp_all add: Let_def djf_def)
chaieb@23274
   308
wenzelm@55885
   309
lemma evaldjf_ex: "Ifm bbs bs (evaldjf f ps) \<longleftrightarrow> (\<exists>p \<in> set ps. Ifm bbs bs (f p))"
wenzelm@50313
   310
  by (induct ps) (simp_all add: evaldjf_def djf_Or)
chaieb@17378
   311
wenzelm@50313
   312
lemma evaldjf_bound0:
wenzelm@50313
   313
  assumes nb: "\<forall>x\<in> set xs. bound0 (f x)"
chaieb@23274
   314
  shows "bound0 (evaldjf f xs)"
blanchet@55422
   315
  using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f a", auto)
chaieb@23274
   316
wenzelm@50313
   317
lemma evaldjf_qf:
wenzelm@50313
   318
  assumes nb: "\<forall>x\<in> set xs. qfree (f x)"
chaieb@23274
   319
  shows "qfree (evaldjf f xs)"
blanchet@55422
   320
  using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f a", auto)
chaieb@17378
   321
wenzelm@50313
   322
fun disjuncts :: "fm \<Rightarrow> fm list"
wenzelm@50313
   323
where
wenzelm@50313
   324
  "disjuncts (Or p q) = disjuncts p @ disjuncts q"
krauss@41837
   325
| "disjuncts F = []"
krauss@41837
   326
| "disjuncts p = [p]"
chaieb@23274
   327
wenzelm@55885
   328
lemma disjuncts: "(\<exists>q \<in> set (disjuncts p). Ifm bbs bs q) \<longleftrightarrow> Ifm bbs bs p"
wenzelm@55885
   329
  by (induct p rule: disjuncts.induct) auto
chaieb@23274
   330
wenzelm@50313
   331
lemma disjuncts_nb:
wenzelm@50313
   332
  assumes nb: "bound0 p"
wenzelm@50313
   333
  shows "\<forall>q \<in> set (disjuncts p). bound0 q"
wenzelm@50313
   334
proof -
wenzelm@50313
   335
  from nb have "list_all bound0 (disjuncts p)"
wenzelm@50313
   336
    by (induct p rule: disjuncts.induct) auto
wenzelm@55885
   337
  then show ?thesis by (simp only: list_all_iff)
chaieb@17378
   338
qed
chaieb@17378
   339
wenzelm@50313
   340
lemma disjuncts_qf:
wenzelm@50313
   341
  assumes qf: "qfree p"
wenzelm@50313
   342
  shows "\<forall>q \<in> set (disjuncts p). qfree q"
wenzelm@50313
   343
proof -
wenzelm@50313
   344
  from qf have "list_all qfree (disjuncts p)"
wenzelm@50313
   345
    by (induct p rule: disjuncts.induct) auto
wenzelm@55885
   346
  then show ?thesis by (simp only: list_all_iff)
chaieb@23274
   347
qed
chaieb@17378
   348
wenzelm@50313
   349
definition DJ :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm"
wenzelm@50313
   350
  where "DJ f p = evaldjf f (disjuncts p)"
chaieb@17378
   351
wenzelm@50313
   352
lemma DJ:
wenzelm@50313
   353
  assumes fdj: "\<forall>p q. f (Or p q) = Or (f p) (f q)"
wenzelm@50313
   354
    and fF: "f F = F"
chaieb@23274
   355
  shows "Ifm bbs bs (DJ f p) = Ifm bbs bs (f p)"
wenzelm@50313
   356
proof -
wenzelm@50313
   357
  have "Ifm bbs bs (DJ f p) = (\<exists>q \<in> set (disjuncts p). Ifm bbs bs (f q))"
wenzelm@50313
   358
    by (simp add: DJ_def evaldjf_ex)
wenzelm@50313
   359
  also have "\<dots> = Ifm bbs bs (f p)"
wenzelm@50313
   360
    using fdj fF by (induct p rule: disjuncts.induct) auto
chaieb@23274
   361
  finally show ?thesis .
chaieb@23274
   362
qed
chaieb@17378
   363
wenzelm@50313
   364
lemma DJ_qf:
wenzelm@50313
   365
  assumes fqf: "\<forall>p. qfree p \<longrightarrow> qfree (f p)"
chaieb@23274
   366
  shows "\<forall>p. qfree p \<longrightarrow> qfree (DJ f p) "
wenzelm@50313
   367
proof clarify
wenzelm@55844
   368
  fix p
wenzelm@55844
   369
  assume qf: "qfree p"
wenzelm@55844
   370
  have th: "DJ f p = evaldjf f (disjuncts p)"
wenzelm@55844
   371
    by (simp add: DJ_def)
wenzelm@55925
   372
  from disjuncts_qf[OF qf] have "\<forall>q \<in> set (disjuncts p). qfree q" .
wenzelm@55925
   373
  with fqf have th':"\<forall>q \<in> set (disjuncts p). qfree (f q)"
wenzelm@55844
   374
    by blast
wenzelm@55844
   375
  from evaldjf_qf[OF th'] th show "qfree (DJ f p)"
wenzelm@55844
   376
    by simp
chaieb@17378
   377
qed
chaieb@17378
   378
wenzelm@50313
   379
lemma DJ_qe:
wenzelm@55885
   380
  assumes qe: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> Ifm bbs bs (qe p) = Ifm bbs bs (E p)"
wenzelm@55885
   381
  shows "\<forall>bs p. qfree p \<longrightarrow> qfree (DJ qe p) \<and> Ifm bbs bs ((DJ qe p)) = Ifm bbs bs (E p)"
wenzelm@50313
   382
proof clarify
wenzelm@55844
   383
  fix p :: fm
wenzelm@55844
   384
  fix bs
chaieb@23274
   385
  assume qf: "qfree p"
wenzelm@55844
   386
  from qe have qth: "\<forall>p. qfree p \<longrightarrow> qfree (qe p)"
wenzelm@55844
   387
    by blast
wenzelm@55925
   388
  from DJ_qf[OF qth] qf have qfth: "qfree (DJ qe p)"
wenzelm@55844
   389
    by auto
wenzelm@50313
   390
  have "Ifm bbs bs (DJ qe p) = (\<exists>q\<in> set (disjuncts p). Ifm bbs bs (qe q))"
chaieb@23274
   391
    by (simp add: DJ_def evaldjf_ex)
wenzelm@55925
   392
  also have "\<dots> \<longleftrightarrow> (\<exists>q \<in> set(disjuncts p). Ifm bbs bs (E q))"
wenzelm@50313
   393
    using qe disjuncts_qf[OF qf] by auto
wenzelm@55925
   394
  also have "\<dots> \<longleftrightarrow> Ifm bbs bs (E p)"
wenzelm@50313
   395
    by (induct p rule: disjuncts.induct) auto
wenzelm@50313
   396
  finally show "qfree (DJ qe p) \<and> Ifm bbs bs (DJ qe p) = Ifm bbs bs (E p)"
wenzelm@50313
   397
    using qfth by blast
chaieb@23274
   398
qed
wenzelm@50313
   399
wenzelm@50313
   400
wenzelm@50313
   401
text {* Simplification *}
chaieb@23274
   402
wenzelm@50313
   403
text {* Algebraic simplifications for nums *}
krauss@41837
   404
wenzelm@50313
   405
fun bnds :: "num \<Rightarrow> nat list"
wenzelm@50313
   406
where
chaieb@23274
   407
  "bnds (Bound n) = [n]"
wenzelm@55921
   408
| "bnds (CN n c a) = n # bnds a"
krauss@41837
   409
| "bnds (Neg a) = bnds a"
wenzelm@55921
   410
| "bnds (Add a b) = bnds a @ bnds b"
wenzelm@55921
   411
| "bnds (Sub a b) =  bnds a @ bnds b"
krauss@41837
   412
| "bnds (Mul i a) = bnds a"
krauss@41837
   413
| "bnds a = []"
krauss@41837
   414
wenzelm@50313
   415
fun lex_ns:: "nat list \<Rightarrow> nat list \<Rightarrow> bool"
wenzelm@50313
   416
where
wenzelm@55844
   417
  "lex_ns [] ms \<longleftrightarrow> True"
wenzelm@55844
   418
| "lex_ns ns [] \<longleftrightarrow> False"
wenzelm@55844
   419
| "lex_ns (n # ns) (m # ms) \<longleftrightarrow> n < m \<or> (n = m \<and> lex_ns ns ms)"
chaieb@23274
   420
wenzelm@50313
   421
definition lex_bnd :: "num \<Rightarrow> num \<Rightarrow> bool"
wenzelm@50313
   422
  where "lex_bnd t s = lex_ns (bnds t) (bnds s)"
wenzelm@50313
   423
wenzelm@50313
   424
consts numadd:: "num \<times> num \<Rightarrow> num"
wenzelm@55921
   425
recdef numadd "measure (\<lambda>(t, s). num_size t + num_size s)"
wenzelm@55981
   426
  "numadd (CN n1 c1 r1, CN n2 c2 r2) =
wenzelm@50313
   427
    (if n1 = n2 then
wenzelm@55981
   428
       let c = c1 + c2
wenzelm@55981
   429
       in if c = 0 then numadd (r1, r2) else CN n1 c (numadd (r1, r2))
wenzelm@55921
   430
     else if n1 \<le> n2 then CN n1 c1 (numadd (r1, Add (Mul c2 (Bound n2)) r2))
wenzelm@50313
   431
     else CN n2 c2 (numadd (Add (Mul c1 (Bound n1)) r1, r2)))"
wenzelm@50313
   432
  "numadd (CN n1 c1 r1, t) = CN n1 c1 (numadd (r1, t))"
wenzelm@50313
   433
  "numadd (t, CN n2 c2 r2) = CN n2 c2 (numadd (t, r2))"
wenzelm@50313
   434
  "numadd (C b1, C b2) = C (b1 + b2)"
wenzelm@50313
   435
  "numadd (a, b) = Add a b"
chaieb@23274
   436
haftmann@23689
   437
(*function (sequential)
haftmann@23689
   438
  numadd :: "num \<Rightarrow> num \<Rightarrow> num"
haftmann@23689
   439
where
haftmann@23689
   440
  "numadd (Add (Mul c1 (Bound n1)) r1) (Add (Mul c2 (Bound n2)) r2) =
haftmann@23689
   441
      (if n1 = n2 then (let c = c1 + c2
haftmann@23689
   442
      in (if c = 0 then numadd r1 r2 else
haftmann@23689
   443
        Add (Mul c (Bound n1)) (numadd r1 r2)))
haftmann@23689
   444
      else if n1 \<le> n2 then
haftmann@23689
   445
        Add (Mul c1 (Bound n1)) (numadd r1 (Add (Mul c2 (Bound n2)) r2))
haftmann@23689
   446
      else
haftmann@23689
   447
        Add (Mul c2 (Bound n2)) (numadd (Add (Mul c1 (Bound n1)) r1) r2))"
haftmann@23689
   448
  | "numadd (Add (Mul c1 (Bound n1)) r1) t =
wenzelm@50313
   449
      Add (Mul c1 (Bound n1)) (numadd r1 t)"
haftmann@23689
   450
  | "numadd t (Add (Mul c2 (Bound n2)) r2) =
wenzelm@50313
   451
      Add (Mul c2 (Bound n2)) (numadd t r2)"
haftmann@23689
   452
  | "numadd (C b1) (C b2) = C (b1 + b2)"
haftmann@23689
   453
  | "numadd a b = Add a b"
haftmann@23689
   454
apply pat_completeness apply auto*)
wenzelm@50313
   455
chaieb@23274
   456
lemma numadd: "Inum bs (numadd (t,s)) = Inum bs (Add t s)"
wenzelm@55885
   457
  apply (induct t s rule: numadd.induct)
wenzelm@55885
   458
  apply (simp_all add: Let_def)
wenzelm@55844
   459
  apply (case_tac "c1 + c2 = 0")
wenzelm@55844
   460
  apply (case_tac "n1 \<le> n2")
wenzelm@55844
   461
  apply simp_all
wenzelm@50313
   462
   apply (case_tac "n1 = n2")
wenzelm@55844
   463
    apply (simp_all add: algebra_simps)
wenzelm@55844
   464
  apply (simp add: distrib_right[symmetric])
wenzelm@50313
   465
  done
chaieb@23274
   466
wenzelm@50313
   467
lemma numadd_nb: "numbound0 t \<Longrightarrow> numbound0 s \<Longrightarrow> numbound0 (numadd (t, s))"
wenzelm@50313
   468
  by (induct t s rule: numadd.induct) (auto simp add: Let_def)
chaieb@23274
   469
wenzelm@50313
   470
fun nummul :: "int \<Rightarrow> num \<Rightarrow> num"
wenzelm@50313
   471
where
haftmann@23689
   472
  "nummul i (C j) = C (i * j)"
wenzelm@55844
   473
| "nummul i (CN n c t) = CN n (c * i) (nummul i t)"
krauss@41837
   474
| "nummul i t = Mul i t"
chaieb@23274
   475
wenzelm@50313
   476
lemma nummul: "Inum bs (nummul i t) = Inum bs (Mul i t)"
wenzelm@50313
   477
  by (induct t arbitrary: i rule: nummul.induct) (auto simp add: algebra_simps numadd)
chaieb@23274
   478
wenzelm@50313
   479
lemma nummul_nb: "numbound0 t \<Longrightarrow> numbound0 (nummul i t)"
wenzelm@50313
   480
  by (induct t arbitrary: i rule: nummul.induct) (auto simp add: numadd_nb)
chaieb@23274
   481
wenzelm@50313
   482
definition numneg :: "num \<Rightarrow> num"
wenzelm@50313
   483
  where "numneg t = nummul (- 1) t"
chaieb@23274
   484
wenzelm@50313
   485
definition numsub :: "num \<Rightarrow> num \<Rightarrow> num"
wenzelm@50313
   486
  where "numsub s t = (if s = t then C 0 else numadd (s, numneg t))"
chaieb@23274
   487
chaieb@23274
   488
lemma numneg: "Inum bs (numneg t) = Inum bs (Neg t)"
wenzelm@50313
   489
  using numneg_def nummul by simp
chaieb@23274
   490
chaieb@23274
   491
lemma numneg_nb: "numbound0 t \<Longrightarrow> numbound0 (numneg t)"
wenzelm@50313
   492
  using numneg_def nummul_nb by simp
chaieb@23274
   493
chaieb@23274
   494
lemma numsub: "Inum bs (numsub a b) = Inum bs (Sub a b)"
wenzelm@50313
   495
  using numneg numadd numsub_def by simp
chaieb@23274
   496
wenzelm@50313
   497
lemma numsub_nb: "numbound0 t \<Longrightarrow> numbound0 s \<Longrightarrow> numbound0 (numsub t s)"
wenzelm@50313
   498
  using numsub_def numadd_nb numneg_nb by simp
chaieb@23274
   499
wenzelm@50313
   500
fun simpnum :: "num \<Rightarrow> num"
haftmann@23689
   501
where
chaieb@23274
   502
  "simpnum (C j) = C j"
wenzelm@50313
   503
| "simpnum (Bound n) = CN n 1 (C 0)"
wenzelm@50313
   504
| "simpnum (Neg t) = numneg (simpnum t)"
wenzelm@50313
   505
| "simpnum (Add t s) = numadd (simpnum t, simpnum s)"
wenzelm@50313
   506
| "simpnum (Sub t s) = numsub (simpnum t) (simpnum s)"
wenzelm@50313
   507
| "simpnum (Mul i t) = (if i = 0 then C 0 else nummul i (simpnum t))"
wenzelm@50313
   508
| "simpnum t = t"
chaieb@23274
   509
chaieb@23274
   510
lemma simpnum_ci: "Inum bs (simpnum t) = Inum bs t"
wenzelm@50313
   511
  by (induct t rule: simpnum.induct) (auto simp add: numneg numadd numsub nummul)
chaieb@23274
   512
wenzelm@50313
   513
lemma simpnum_numbound0: "numbound0 t \<Longrightarrow> numbound0 (simpnum t)"
wenzelm@50313
   514
  by (induct t rule: simpnum.induct) (auto simp add: numadd_nb numsub_nb nummul_nb numneg_nb)
chaieb@23274
   515
wenzelm@50313
   516
fun not :: "fm \<Rightarrow> fm"
haftmann@23689
   517
where
chaieb@23274
   518
  "not (NOT p) = p"
wenzelm@50313
   519
| "not T = F"
wenzelm@50313
   520
| "not F = T"
wenzelm@50313
   521
| "not p = NOT p"
wenzelm@50313
   522
chaieb@23274
   523
lemma not: "Ifm bbs bs (not p) = Ifm bbs bs (NOT p)"
wenzelm@41807
   524
  by (cases p) auto
wenzelm@50313
   525
chaieb@23274
   526
lemma not_qf: "qfree p \<Longrightarrow> qfree (not p)"
wenzelm@41807
   527
  by (cases p) auto
wenzelm@50313
   528
chaieb@23274
   529
lemma not_bn: "bound0 p \<Longrightarrow> bound0 (not p)"
wenzelm@41807
   530
  by (cases p) auto
chaieb@23274
   531
wenzelm@50313
   532
definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm"
wenzelm@50313
   533
  where
wenzelm@55844
   534
    "conj p q =
wenzelm@55844
   535
      (if p = F \<or> q = F then F
wenzelm@55844
   536
       else if p = T then q
wenzelm@55844
   537
       else if q = T then p
wenzelm@55844
   538
       else And p q)"
wenzelm@50313
   539
chaieb@23274
   540
lemma conj: "Ifm bbs bs (conj p q) = Ifm bbs bs (And p q)"
wenzelm@55844
   541
  by (cases "p = F \<or> q = F", simp_all add: conj_def) (cases p, simp_all)
chaieb@23274
   542
wenzelm@50313
   543
lemma conj_qf: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (conj p q)"
wenzelm@50313
   544
  using conj_def by auto
chaieb@23274
   545
wenzelm@50313
   546
lemma conj_nb: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (conj p q)"
wenzelm@50313
   547
  using conj_def by auto
wenzelm@50313
   548
wenzelm@50313
   549
definition disj :: "fm \<Rightarrow> fm \<Rightarrow> fm"
wenzelm@50313
   550
  where
wenzelm@50313
   551
    "disj p q =
wenzelm@55844
   552
      (if p = T \<or> q = T then T
wenzelm@55844
   553
       else if p = F then q
wenzelm@55844
   554
       else if q = F then p
wenzelm@55844
   555
       else Or p q)"
chaieb@23274
   556
chaieb@23274
   557
lemma disj: "Ifm bbs bs (disj p q) = Ifm bbs bs (Or p q)"
wenzelm@55885
   558
  by (cases "p = T \<or> q = T", simp_all add: disj_def) (cases p, simp_all)
wenzelm@50313
   559
wenzelm@55844
   560
lemma disj_qf: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (disj p q)"
wenzelm@50313
   561
  using disj_def by auto
wenzelm@50313
   562
wenzelm@55844
   563
lemma disj_nb: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (disj p q)"
wenzelm@50313
   564
  using disj_def by auto
chaieb@23274
   565
wenzelm@50313
   566
definition imp :: "fm \<Rightarrow> fm \<Rightarrow> fm"
wenzelm@50313
   567
  where
wenzelm@55844
   568
    "imp p q =
wenzelm@55844
   569
      (if p = F \<or> q = T then T
wenzelm@55844
   570
       else if p = T then q
wenzelm@55844
   571
       else if q = F then not p
wenzelm@55844
   572
       else Imp p q)"
wenzelm@50313
   573
chaieb@23274
   574
lemma imp: "Ifm bbs bs (imp p q) = Ifm bbs bs (Imp p q)"
wenzelm@55844
   575
  by (cases "p = F \<or> q = T", simp_all add: imp_def, cases p) (simp_all add: not)
wenzelm@50313
   576
wenzelm@50313
   577
lemma imp_qf: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (imp p q)"
wenzelm@55844
   578
  using imp_def by (cases "p = F \<or> q = T", simp_all add: imp_def, cases p) (simp_all add: not_qf)
wenzelm@50313
   579
wenzelm@50313
   580
lemma imp_nb: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (imp p q)"
wenzelm@55844
   581
  using imp_def by (cases "p = F \<or> q = T", simp_all add: imp_def, cases p) simp_all
chaieb@23274
   582
wenzelm@50313
   583
definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm"
wenzelm@55885
   584
where
wenzelm@55885
   585
  "iff p q =
wenzelm@55885
   586
    (if p = q then T
wenzelm@55885
   587
     else if p = not q \<or> not p = q then F
wenzelm@55885
   588
     else if p = F then not q
wenzelm@55885
   589
     else if q = F then not p
wenzelm@55885
   590
     else if p = T then q
wenzelm@55885
   591
     else if q = T then p
wenzelm@55885
   592
     else Iff p q)"
wenzelm@50313
   593
chaieb@23274
   594
lemma iff: "Ifm bbs bs (iff p q) = Ifm bbs bs (Iff p q)"
wenzelm@55885
   595
  by (unfold iff_def, cases "p = q", simp, cases "p = not q", simp add: not)
wenzelm@55885
   596
    (cases "not p = q", auto simp add: not)
wenzelm@50313
   597
wenzelm@55885
   598
lemma iff_qf: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (iff p q)"
wenzelm@55885
   599
  by (unfold iff_def, cases "p = q", auto simp add: not_qf)
chaieb@23274
   600
wenzelm@55885
   601
lemma iff_nb: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (iff p q)"
wenzelm@55885
   602
  using iff_def by (unfold iff_def, cases "p = q", auto simp add: not_bn)
wenzelm@50313
   603
wenzelm@50313
   604
function (sequential) simpfm :: "fm \<Rightarrow> fm"
haftmann@23689
   605
where
chaieb@23274
   606
  "simpfm (And p q) = conj (simpfm p) (simpfm q)"
wenzelm@50313
   607
| "simpfm (Or p q) = disj (simpfm p) (simpfm q)"
wenzelm@50313
   608
| "simpfm (Imp p q) = imp (simpfm p) (simpfm q)"
wenzelm@50313
   609
| "simpfm (Iff p q) = iff (simpfm p) (simpfm q)"
wenzelm@50313
   610
| "simpfm (NOT p) = not (simpfm p)"
wenzelm@55921
   611
| "simpfm (Lt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if v < 0 then T else F | _ \<Rightarrow> Lt a')"
wenzelm@55921
   612
| "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')"
wenzelm@55921
   613
| "simpfm (Gt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if v > 0 then T else F | _ \<Rightarrow> Gt a')"
wenzelm@55921
   614
| "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')"
wenzelm@55921
   615
| "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if v = 0 then T else F | _ \<Rightarrow> Eq a')"
wenzelm@55921
   616
| "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')"
wenzelm@50313
   617
| "simpfm (Dvd i a) =
wenzelm@55885
   618
    (if i = 0 then simpfm (Eq a)
wenzelm@55885
   619
     else if abs i = 1 then T
wenzelm@55921
   620
     else let a' = simpnum a in case a' of C v \<Rightarrow> if i dvd v then T else F | _ \<Rightarrow> Dvd i a')"
wenzelm@50313
   621
| "simpfm (NDvd i a) =
wenzelm@55885
   622
    (if i = 0 then simpfm (NEq a)
wenzelm@55885
   623
     else if abs i = 1 then F
wenzelm@55921
   624
     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')"
wenzelm@50313
   625
| "simpfm p = p"
wenzelm@50313
   626
  by pat_completeness auto
haftmann@23689
   627
termination by (relation "measure fmsize") auto
haftmann@23689
   628
chaieb@23274
   629
lemma simpfm: "Ifm bbs bs (simpfm p) = Ifm bbs bs p"
wenzelm@55844
   630
proof (induct p rule: simpfm.induct)
wenzelm@50313
   631
  case (6 a)
wenzelm@50313
   632
  let ?sa = "simpnum a"
wenzelm@55925
   633
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
wenzelm@55925
   634
    by simp
wenzelm@55925
   635
  {
wenzelm@55925
   636
    fix v
wenzelm@55925
   637
    assume "?sa = C v"
wenzelm@55925
   638
    then have ?case using sa
wenzelm@55925
   639
      by simp
wenzelm@55925
   640
  }
wenzelm@50313
   641
  moreover {
wenzelm@50313
   642
    assume "\<not> (\<exists>v. ?sa = C v)"
wenzelm@55925
   643
    then have ?case
wenzelm@55925
   644
      using sa by (cases ?sa) (simp_all add: Let_def)
wenzelm@50313
   645
  }
chaieb@23274
   646
  ultimately show ?case by blast
chaieb@17378
   647
next
wenzelm@50313
   648
  case (7 a)
wenzelm@50313
   649
  let ?sa = "simpnum a"
wenzelm@55925
   650
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
wenzelm@55925
   651
    by simp
wenzelm@55925
   652
  {
wenzelm@55925
   653
    fix v
wenzelm@55925
   654
    assume "?sa = C v"
wenzelm@55925
   655
    then have ?case using sa
wenzelm@55925
   656
      by simp
wenzelm@55925
   657
  }
wenzelm@50313
   658
  moreover {
wenzelm@50313
   659
    assume "\<not> (\<exists>v. ?sa = C v)"
wenzelm@55925
   660
    then have ?case
wenzelm@55925
   661
      using sa by (cases ?sa) (simp_all add: Let_def)
wenzelm@50313
   662
  }
chaieb@23274
   663
  ultimately show ?case by blast
chaieb@23274
   664
next
wenzelm@50313
   665
  case (8 a)
wenzelm@50313
   666
  let ?sa = "simpnum a"
wenzelm@55925
   667
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
wenzelm@55925
   668
    by simp
wenzelm@55925
   669
  {
wenzelm@55925
   670
    fix v
wenzelm@55925
   671
    assume "?sa = C v"
wenzelm@55925
   672
    then have ?case using sa
wenzelm@55925
   673
      by simp
wenzelm@55925
   674
  }
wenzelm@50313
   675
  moreover {
wenzelm@50313
   676
    assume "\<not> (\<exists>v. ?sa = C v)"
wenzelm@55925
   677
    then have ?case
wenzelm@55925
   678
      using sa by (cases ?sa) (simp_all add: Let_def)
wenzelm@50313
   679
  }
chaieb@23274
   680
  ultimately show ?case by blast
chaieb@23274
   681
next
wenzelm@50313
   682
  case (9 a)
wenzelm@50313
   683
  let ?sa = "simpnum a"
wenzelm@55925
   684
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
wenzelm@55925
   685
    by simp
wenzelm@55925
   686
  {
wenzelm@55925
   687
    fix v
wenzelm@55925
   688
    assume "?sa = C v"
wenzelm@55925
   689
    then have ?case using sa
wenzelm@55925
   690
      by simp
wenzelm@55925
   691
  }
wenzelm@50313
   692
  moreover {
wenzelm@50313
   693
    assume "\<not> (\<exists>v. ?sa = C v)"
wenzelm@55925
   694
    then have ?case using sa
wenzelm@55925
   695
      by (cases ?sa) (simp_all add: Let_def)
wenzelm@50313
   696
  }
chaieb@23274
   697
  ultimately show ?case by blast
chaieb@23274
   698
next
wenzelm@50313
   699
  case (10 a)
wenzelm@50313
   700
  let ?sa = "simpnum a"
wenzelm@55925
   701
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
wenzelm@55925
   702
    by simp
wenzelm@55925
   703
  {
wenzelm@55925
   704
    fix v
wenzelm@55925
   705
    assume "?sa = C v"
wenzelm@55925
   706
    then have ?case
wenzelm@55925
   707
      using sa by simp
wenzelm@55925
   708
  }
wenzelm@50313
   709
  moreover {
wenzelm@50313
   710
    assume "\<not> (\<exists>v. ?sa = C v)"
wenzelm@55925
   711
    then have ?case
wenzelm@55925
   712
      using sa by (cases ?sa) (simp_all add: Let_def)
wenzelm@50313
   713
  }
chaieb@23274
   714
  ultimately show ?case by blast
chaieb@23274
   715
next
wenzelm@50313
   716
  case (11 a)
wenzelm@50313
   717
  let ?sa = "simpnum a"
wenzelm@55925
   718
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
wenzelm@55925
   719
    by simp
wenzelm@55925
   720
  {
wenzelm@55925
   721
    fix v
wenzelm@55925
   722
    assume "?sa = C v"
wenzelm@55925
   723
    then have ?case using sa
wenzelm@55925
   724
      by simp
wenzelm@55925
   725
  }
wenzelm@50313
   726
  moreover {
wenzelm@50313
   727
    assume "\<not> (\<exists>v. ?sa = C v)"
wenzelm@55925
   728
    then have ?case
wenzelm@55925
   729
      using sa by (cases ?sa) (simp_all add: Let_def)
wenzelm@50313
   730
  }
chaieb@23274
   731
  ultimately show ?case by blast
chaieb@23274
   732
next
wenzelm@50313
   733
  case (12 i a)
wenzelm@50313
   734
  let ?sa = "simpnum a"
wenzelm@55925
   735
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
wenzelm@55925
   736
    by simp
wenzelm@55925
   737
  {
wenzelm@55925
   738
    assume "i = 0"
wenzelm@55925
   739
    then have ?case using "12.hyps"
wenzelm@55925
   740
      by (simp add: dvd_def Let_def)
wenzelm@55925
   741
  }
wenzelm@50313
   742
  moreover
wenzelm@55925
   743
  {
wenzelm@55925
   744
    assume i1: "abs i = 1"
wenzelm@50313
   745
    from one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
wenzelm@55925
   746
    have ?case
wenzelm@55925
   747
      using i1
wenzelm@55925
   748
      apply (cases "i = 0")
wenzelm@55925
   749
      apply (simp_all add: Let_def)
wenzelm@55925
   750
      apply (cases "i > 0")
wenzelm@55925
   751
      apply simp_all
wenzelm@50313
   752
      done
wenzelm@50313
   753
  }
wenzelm@50313
   754
  moreover
wenzelm@55925
   755
  {
wenzelm@55925
   756
    assume inz: "i \<noteq> 0" and cond: "abs i \<noteq> 1"
wenzelm@55925
   757
    {
wenzelm@55925
   758
      fix v
wenzelm@55925
   759
      assume "?sa = C v"
wenzelm@55925
   760
      then have ?case
wenzelm@55925
   761
        using sa[symmetric] inz cond
wenzelm@55925
   762
        by (cases "abs i = 1") auto
wenzelm@55925
   763
    }
wenzelm@55925
   764
    moreover
wenzelm@55925
   765
    {
wenzelm@50313
   766
      assume "\<not> (\<exists>v. ?sa = C v)"
wenzelm@55925
   767
      then have "simpfm (Dvd i a) = Dvd i ?sa"
wenzelm@55925
   768
        using inz cond by (cases ?sa) (auto simp add: Let_def)
wenzelm@55925
   769
      then have ?case
wenzelm@55925
   770
        using sa by simp
wenzelm@55925
   771
    }
wenzelm@55925
   772
    ultimately have ?case by blast
wenzelm@55925
   773
  }
wenzelm@50313
   774
  ultimately show ?case by blast
wenzelm@50313
   775
next
wenzelm@50313
   776
  case (13 i a)
wenzelm@55925
   777
  let ?sa = "simpnum a"
wenzelm@55925
   778
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
wenzelm@55925
   779
    by simp
wenzelm@55925
   780
  {
wenzelm@55925
   781
    assume "i = 0"
wenzelm@55925
   782
    then have ?case using "13.hyps"
wenzelm@55925
   783
      by (simp add: dvd_def Let_def)
wenzelm@55925
   784
  }
wenzelm@50313
   785
  moreover
wenzelm@55925
   786
  {
wenzelm@55925
   787
    assume i1: "abs i = 1"
wenzelm@50313
   788
    from one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
wenzelm@55925
   789
    have ?case
wenzelm@55925
   790
      using i1
wenzelm@55925
   791
      apply (cases "i = 0")
wenzelm@55925
   792
      apply (simp_all add: Let_def)
wenzelm@55925
   793
      apply (cases "i > 0")
wenzelm@55925
   794
      apply simp_all
wenzelm@50313
   795
      done
wenzelm@50313
   796
  }
wenzelm@50313
   797
  moreover
wenzelm@55925
   798
  {
wenzelm@55925
   799
    assume inz: "i \<noteq> 0" and cond: "abs i \<noteq> 1"
wenzelm@55925
   800
    {
wenzelm@55925
   801
      fix v
wenzelm@55925
   802
      assume "?sa = C v"
wenzelm@55925
   803
      then have ?case
wenzelm@55925
   804
        using sa[symmetric] inz cond by (cases "abs i = 1") auto
wenzelm@55925
   805
    }
wenzelm@55925
   806
    moreover
wenzelm@55925
   807
    {
wenzelm@50313
   808
      assume "\<not> (\<exists>v. ?sa = C v)"
wenzelm@55925
   809
      then have "simpfm (NDvd i a) = NDvd i ?sa"
wenzelm@55925
   810
        using inz cond by (cases ?sa) (auto simp add: Let_def)
wenzelm@55925
   811
      then have ?case using sa
wenzelm@55925
   812
        by simp
wenzelm@55925
   813
    }
wenzelm@55925
   814
    ultimately have ?case by blast
wenzelm@55925
   815
  }
chaieb@23274
   816
  ultimately show ?case by blast
wenzelm@50313
   817
qed (simp_all add: conj disj imp iff not)
chaieb@17378
   818
chaieb@23274
   819
lemma simpfm_bound0: "bound0 p \<Longrightarrow> bound0 (simpfm p)"
wenzelm@50313
   820
proof (induct p rule: simpfm.induct)
wenzelm@55925
   821
  case (6 a)
wenzelm@55925
   822
  then have nb: "numbound0 a" by simp
wenzelm@55885
   823
  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
wenzelm@55885
   824
  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
chaieb@23274
   825
next
wenzelm@55925
   826
  case (7 a)
wenzelm@55925
   827
  then have nb: "numbound0 a" by simp
wenzelm@55885
   828
  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
wenzelm@55885
   829
  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
chaieb@23274
   830
next
wenzelm@55925
   831
  case (8 a)
wenzelm@55925
   832
  then have nb: "numbound0 a" by simp
wenzelm@55885
   833
  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
wenzelm@55885
   834
  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
chaieb@23274
   835
next
wenzelm@55925
   836
  case (9 a)
wenzelm@55925
   837
  then have nb: "numbound0 a" by simp
wenzelm@55885
   838
  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
wenzelm@55885
   839
  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
chaieb@23274
   840
next
wenzelm@55925
   841
  case (10 a)
wenzelm@55925
   842
  then have nb: "numbound0 a" by simp
wenzelm@55885
   843
  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
wenzelm@55885
   844
  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
chaieb@23274
   845
next
wenzelm@55925
   846
  case (11 a)
wenzelm@55925
   847
  then have nb: "numbound0 a" by simp
wenzelm@55885
   848
  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
wenzelm@55885
   849
  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
chaieb@23274
   850
next
wenzelm@55925
   851
  case (12 i a)
wenzelm@55925
   852
  then have nb: "numbound0 a" by simp
wenzelm@55885
   853
  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
wenzelm@55885
   854
  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
chaieb@23274
   855
next
wenzelm@55925
   856
  case (13 i a)
wenzelm@55925
   857
  then have nb: "numbound0 a" by simp
wenzelm@55885
   858
  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
wenzelm@55885
   859
  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
wenzelm@50313
   860
qed (auto simp add: disj_def imp_def iff_def conj_def not_bn)
chaieb@17378
   861
chaieb@23274
   862
lemma simpfm_qf: "qfree p \<Longrightarrow> qfree (simpfm p)"
wenzelm@50313
   863
  by (induct p rule: simpfm.induct, auto simp add: disj_qf imp_qf iff_qf conj_qf not_qf Let_def)
wenzelm@50313
   864
    (case_tac "simpnum a", auto)+
chaieb@23274
   865
wenzelm@50313
   866
text {* Generic quantifier elimination *}
wenzelm@50313
   867
function (sequential) qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
wenzelm@50313
   868
where
wenzelm@50313
   869
  "qelim (E p) = (\<lambda>qe. DJ qe (qelim p qe))"
wenzelm@50313
   870
| "qelim (A p) = (\<lambda>qe. not (qe ((qelim (NOT p) qe))))"
wenzelm@50313
   871
| "qelim (NOT p) = (\<lambda>qe. not (qelim p qe))"
wenzelm@50313
   872
| "qelim (And p q) = (\<lambda>qe. conj (qelim p qe) (qelim q qe))"
wenzelm@50313
   873
| "qelim (Or  p q) = (\<lambda>qe. disj (qelim p qe) (qelim q qe))"
wenzelm@50313
   874
| "qelim (Imp p q) = (\<lambda>qe. imp (qelim p qe) (qelim q qe))"
wenzelm@50313
   875
| "qelim (Iff p q) = (\<lambda>qe. iff (qelim p qe) (qelim q qe))"
wenzelm@50313
   876
| "qelim p = (\<lambda>y. simpfm p)"
wenzelm@50313
   877
  by pat_completeness auto
krauss@41837
   878
termination by (relation "measure fmsize") auto
haftmann@23689
   879
chaieb@23274
   880
lemma qelim_ci:
wenzelm@55885
   881
  assumes qe_inv: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> Ifm bbs bs (qe p) = Ifm bbs bs (E p)"
wenzelm@55885
   882
  shows "\<And>bs. qfree (qelim p qe) \<and> Ifm bbs bs (qelim p qe) = Ifm bbs bs p"
wenzelm@50313
   883
  using qe_inv DJ_qe[OF qe_inv]
wenzelm@55964
   884
  by (induct p rule: qelim.induct)
wenzelm@55964
   885
    (auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf
wenzelm@55964
   886
      simpfm simpfm_qf simp del: simpfm.simps)
haftmann@23689
   887
wenzelm@50313
   888
text {* Linearity for fm where Bound 0 ranges over @{text "\<int>"} *}
wenzelm@50313
   889
wenzelm@50313
   890
fun zsplit0 :: "num \<Rightarrow> int \<times> num"  -- {* splits the bounded from the unbounded part *}
haftmann@23689
   891
where
wenzelm@55885
   892
  "zsplit0 (C c) = (0, C c)"
wenzelm@55885
   893
| "zsplit0 (Bound n) = (if n = 0 then (1, C 0) else (0, Bound n))"
wenzelm@50313
   894
| "zsplit0 (CN n i a) =
wenzelm@55885
   895
    (let (i', a') =  zsplit0 a
wenzelm@55885
   896
     in if n = 0 then (i + i', a') else (i', CN n i a'))"
wenzelm@55885
   897
| "zsplit0 (Neg a) = (let (i', a') = zsplit0 a in (-i', Neg a'))"
wenzelm@55885
   898
| "zsplit0 (Add a b) =
wenzelm@55885
   899
    (let
wenzelm@55885
   900
      (ia, a') = zsplit0 a;
wenzelm@55885
   901
      (ib, b') = zsplit0 b
wenzelm@55885
   902
     in (ia + ib, Add a' b'))"
wenzelm@55885
   903
| "zsplit0 (Sub a b) =
wenzelm@55885
   904
    (let
wenzelm@55885
   905
      (ia, a') = zsplit0 a;
wenzelm@55885
   906
      (ib, b') = zsplit0 b
wenzelm@55885
   907
     in (ia - ib, Sub a' b'))"
wenzelm@55885
   908
| "zsplit0 (Mul i a) = (let (i', a') = zsplit0 a in (i*i', Mul i a'))"
chaieb@23274
   909
chaieb@23274
   910
lemma zsplit0_I:
wenzelm@55964
   911
  "\<And>n a. zsplit0 t = (n, a) \<Longrightarrow>
wenzelm@55921
   912
    (Inum ((x::int) # bs) (CN 0 n a) = Inum (x # bs) t) \<and> numbound0 a"
wenzelm@50313
   913
  (is "\<And>n a. ?S t = (n,a) \<Longrightarrow> (?I x (CN 0 n a) = ?I x t) \<and> ?N a")
wenzelm@50313
   914
proof (induct t rule: zsplit0.induct)
wenzelm@55844
   915
  case (1 c n a)
wenzelm@55844
   916
  then show ?case by auto
chaieb@23274
   917
next
wenzelm@55844
   918
  case (2 m n a)
wenzelm@55844
   919
  then show ?case by (cases "m = 0") auto
chaieb@23274
   920
next
chaieb@23995
   921
  case (3 m i a n a')
chaieb@23274
   922
  let ?j = "fst (zsplit0 a)"
chaieb@23274
   923
  let ?b = "snd (zsplit0 a)"
wenzelm@55844
   924
  have abj: "zsplit0 a = (?j, ?b)" by simp
wenzelm@55844
   925
  {
wenzelm@55844
   926
    assume "m \<noteq> 0"
wenzelm@55844
   927
    with 3(1)[OF abj] 3(2) have ?case
wenzelm@55844
   928
      by (auto simp add: Let_def split_def)
wenzelm@55844
   929
  }
chaieb@23995
   930
  moreover
wenzelm@55844
   931
  {
wenzelm@55844
   932
    assume m0: "m = 0"
wenzelm@55964
   933
    with abj have th: "a' = ?b \<and> n = i + ?j"
wenzelm@55964
   934
      using 3 by (simp add: Let_def split_def)
wenzelm@55844
   935
    from abj 3 m0 have th2: "(?I x (CN 0 ?j ?b) = ?I x a) \<and> ?N ?b"
wenzelm@55844
   936
      by blast
wenzelm@55964
   937
    from th have "?I x (CN 0 n a') = ?I x (CN 0 (i + ?j) ?b)"
wenzelm@55844
   938
      by simp
wenzelm@55844
   939
    also from th2 have "\<dots> = ?I x (CN 0 i (CN 0 ?j ?b))"
wenzelm@55844
   940
      by (simp add: distrib_right)
wenzelm@55844
   941
    finally have "?I x (CN 0 n a') = ?I  x (CN 0 i a)"
wenzelm@55844
   942
      using th2 by simp
wenzelm@55844
   943
    with th2 th have ?case using m0
wenzelm@55844
   944
      by blast
wenzelm@55844
   945
  }
wenzelm@55844
   946
  ultimately show ?case by blast
chaieb@23274
   947
next
chaieb@23274
   948
  case (4 t n a)
chaieb@23274
   949
  let ?nt = "fst (zsplit0 t)"
chaieb@23274
   950
  let ?at = "snd (zsplit0 t)"
wenzelm@55964
   951
  have abj: "zsplit0 t = (?nt, ?at)"
wenzelm@55964
   952
    by simp
wenzelm@55964
   953
  then have th: "a = Neg ?at \<and> n = - ?nt"
wenzelm@55844
   954
    using 4 by (simp add: Let_def split_def)
wenzelm@55844
   955
  from abj 4 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at"
wenzelm@55844
   956
    by blast
wenzelm@55844
   957
  from th2[simplified] th[simplified] show ?case
wenzelm@55844
   958
    by simp
chaieb@23274
   959
next
chaieb@23274
   960
  case (5 s t n a)
chaieb@23274
   961
  let ?ns = "fst (zsplit0 s)"
chaieb@23274
   962
  let ?as = "snd (zsplit0 s)"
chaieb@23274
   963
  let ?nt = "fst (zsplit0 t)"
chaieb@23274
   964
  let ?at = "snd (zsplit0 t)"
wenzelm@55844
   965
  have abjs: "zsplit0 s = (?ns, ?as)"
wenzelm@55844
   966
    by simp
wenzelm@55844
   967
  moreover have abjt: "zsplit0 t = (?nt, ?at)"
wenzelm@55844
   968
    by simp
wenzelm@55964
   969
  ultimately have th: "a = Add ?as ?at \<and> n = ?ns + ?nt"
wenzelm@55844
   970
    using 5 by (simp add: Let_def split_def)
wenzelm@55964
   971
  from abjs[symmetric] have bluddy: "\<exists>x y. (x, y) = zsplit0 s"
wenzelm@55844
   972
    by blast
wenzelm@55844
   973
  from 5 have "(\<exists>x y. (x, y) = zsplit0 s) \<longrightarrow>
wenzelm@55844
   974
    (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)"
wenzelm@55844
   975
    by auto
wenzelm@55844
   976
  with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at"
wenzelm@55844
   977
    by blast
wenzelm@55844
   978
  from abjs 5 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as"
wenzelm@55844
   979
    by blast
wenzelm@50313
   980
  from th3[simplified] th2[simplified] th[simplified] show ?case
webertj@49962
   981
    by (simp add: distrib_right)
chaieb@23274
   982
next
chaieb@23274
   983
  case (6 s t n a)
chaieb@23274
   984
  let ?ns = "fst (zsplit0 s)"
chaieb@23274
   985
  let ?as = "snd (zsplit0 s)"
chaieb@23274
   986
  let ?nt = "fst (zsplit0 t)"
chaieb@23274
   987
  let ?at = "snd (zsplit0 t)"
wenzelm@55844
   988
  have abjs: "zsplit0 s = (?ns, ?as)"
wenzelm@55844
   989
    by simp
wenzelm@55844
   990
  moreover have abjt: "zsplit0 t = (?nt, ?at)"
wenzelm@55844
   991
    by simp
wenzelm@55964
   992
  ultimately have th: "a = Sub ?as ?at \<and> n = ?ns - ?nt"
wenzelm@55844
   993
    using 6 by (simp add: Let_def split_def)
wenzelm@55964
   994
  from abjs[symmetric] have bluddy: "\<exists>x y. (x, y) = zsplit0 s"
wenzelm@55844
   995
    by blast
wenzelm@50313
   996
  from 6 have "(\<exists>x y. (x,y) = zsplit0 s) \<longrightarrow>
wenzelm@50313
   997
    (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)"
wenzelm@50313
   998
    by auto
wenzelm@55844
   999
  with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at"
wenzelm@55844
  1000
    by blast
wenzelm@55844
  1001
  from abjs 6 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as"
wenzelm@55844
  1002
    by blast
wenzelm@50313
  1003
  from th3[simplified] th2[simplified] th[simplified] show ?case
chaieb@23274
  1004
    by (simp add: left_diff_distrib)
chaieb@23274
  1005
next
chaieb@23274
  1006
  case (7 i t n a)
chaieb@23274
  1007
  let ?nt = "fst (zsplit0 t)"
chaieb@23274
  1008
  let ?at = "snd (zsplit0 t)"
wenzelm@55844
  1009
  have abj: "zsplit0 t = (?nt,?at)"
wenzelm@55844
  1010
    by simp
wenzelm@55964
  1011
  then have th: "a = Mul i ?at \<and> n = i * ?nt"
wenzelm@55844
  1012
    using 7 by (simp add: Let_def split_def)
wenzelm@55844
  1013
  from abj 7 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at"
wenzelm@55844
  1014
    by blast
wenzelm@55844
  1015
  then have "?I x (Mul i t) = i * ?I x (CN 0 ?nt ?at)"
wenzelm@55844
  1016
    by simp
wenzelm@55844
  1017
  also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))"
wenzelm@55844
  1018
    by (simp add: distrib_left)
wenzelm@55844
  1019
  finally show ?case using th th2
wenzelm@55844
  1020
    by simp
chaieb@17378
  1021
qed
chaieb@17378
  1022
wenzelm@50313
  1023
consts iszlfm :: "fm \<Rightarrow> bool"  -- {* Linearity test for fm *}
chaieb@23274
  1024
recdef iszlfm "measure size"
wenzelm@55885
  1025
  "iszlfm (And p q) \<longleftrightarrow> iszlfm p \<and> iszlfm q"
wenzelm@55885
  1026
  "iszlfm (Or p q) \<longleftrightarrow> iszlfm p \<and> iszlfm q"
wenzelm@55885
  1027
  "iszlfm (Eq  (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
wenzelm@55885
  1028
  "iszlfm (NEq (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
wenzelm@55885
  1029
  "iszlfm (Lt  (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
wenzelm@55885
  1030
  "iszlfm (Le  (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
wenzelm@55885
  1031
  "iszlfm (Gt  (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
wenzelm@55885
  1032
  "iszlfm (Ge  (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
wenzelm@55885
  1033
  "iszlfm (Dvd i (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> i > 0 \<and> numbound0 e"
wenzelm@55885
  1034
  "iszlfm (NDvd i (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> i > 0 \<and> numbound0 e"
wenzelm@55885
  1035
  "iszlfm p \<longleftrightarrow> isatom p \<and> bound0 p"
chaieb@17378
  1036
chaieb@23274
  1037
lemma zlin_qfree: "iszlfm p \<Longrightarrow> qfree p"
chaieb@23274
  1038
  by (induct p rule: iszlfm.induct) auto
chaieb@17378
  1039
wenzelm@50313
  1040
consts zlfm :: "fm \<Rightarrow> fm"  -- {* Linearity transformation for fm *}
chaieb@23274
  1041
recdef zlfm "measure fmsize"
chaieb@23274
  1042
  "zlfm (And p q) = And (zlfm p) (zlfm q)"
chaieb@23274
  1043
  "zlfm (Or p q) = Or (zlfm p) (zlfm q)"
chaieb@23274
  1044
  "zlfm (Imp p q) = Or (zlfm (NOT p)) (zlfm q)"
chaieb@23274
  1045
  "zlfm (Iff p q) = Or (And (zlfm p) (zlfm q)) (And (zlfm (NOT p)) (zlfm (NOT q)))"
wenzelm@55964
  1046
  "zlfm (Lt a) =
wenzelm@55964
  1047
    (let (c, r) = zsplit0 a in
wenzelm@55964
  1048
      if c = 0 then Lt r else
wenzelm@55964
  1049
      if c > 0 then (Lt (CN 0 c r))
wenzelm@55964
  1050
      else Gt (CN 0 (- c) (Neg r)))"
wenzelm@55964
  1051
  "zlfm (Le a) =
wenzelm@55964
  1052
    (let (c, r) = zsplit0 a in
wenzelm@55964
  1053
      if c = 0 then Le r
wenzelm@55964
  1054
      else if c > 0 then Le (CN 0 c r)
wenzelm@55964
  1055
      else Ge (CN 0 (- c) (Neg r)))"
wenzelm@55964
  1056
  "zlfm (Gt a) =
wenzelm@55964
  1057
    (let (c, r) = zsplit0 a in
wenzelm@55964
  1058
      if c = 0 then Gt r else
wenzelm@55964
  1059
      if c > 0 then Gt (CN 0 c r)
wenzelm@55964
  1060
      else Lt (CN 0 (- c) (Neg r)))"
wenzelm@55964
  1061
  "zlfm (Ge a) =
wenzelm@55964
  1062
    (let (c, r) = zsplit0 a in
wenzelm@55964
  1063
      if c = 0 then Ge r
wenzelm@55964
  1064
      else if c > 0 then Ge (CN 0 c r)
wenzelm@55964
  1065
      else Le (CN 0 (- c) (Neg r)))"
wenzelm@55964
  1066
  "zlfm (Eq a) =
wenzelm@55964
  1067
    (let (c, r) = zsplit0 a in
wenzelm@55964
  1068
      if c = 0 then Eq r
wenzelm@55964
  1069
      else if c > 0 then Eq (CN 0 c r)
wenzelm@55964
  1070
      else Eq (CN 0 (- c) (Neg r)))"
wenzelm@55964
  1071
  "zlfm (NEq a) =
wenzelm@55964
  1072
    (let (c, r) = zsplit0 a in
wenzelm@55964
  1073
      if c = 0 then NEq r
wenzelm@55964
  1074
      else if c > 0 then NEq (CN 0 c r)
wenzelm@55964
  1075
      else NEq (CN 0 (- c) (Neg r)))"
wenzelm@55964
  1076
  "zlfm (Dvd i a) =
wenzelm@55964
  1077
    (if i = 0 then zlfm (Eq a)
wenzelm@55964
  1078
     else
wenzelm@55964
  1079
      let (c, r) = zsplit0 a in
wenzelm@55964
  1080
        if c = 0 then Dvd (abs i) r
wenzelm@55964
  1081
        else if c > 0 then Dvd (abs i) (CN 0 c r)
wenzelm@55964
  1082
        else Dvd (abs i) (CN 0 (- c) (Neg r)))"
wenzelm@55964
  1083
  "zlfm (NDvd i a) =
wenzelm@55964
  1084
    (if i = 0 then zlfm (NEq a)
wenzelm@55964
  1085
     else
wenzelm@55964
  1086
      let (c, r) = zsplit0 a in
wenzelm@55964
  1087
        if c = 0 then NDvd (abs i) r
wenzelm@55964
  1088
        else if c > 0 then NDvd (abs i) (CN 0 c r)
wenzelm@55964
  1089
        else NDvd (abs i) (CN 0 (- c) (Neg r)))"
chaieb@23274
  1090
  "zlfm (NOT (And p q)) = Or (zlfm (NOT p)) (zlfm (NOT q))"
chaieb@23274
  1091
  "zlfm (NOT (Or p q)) = And (zlfm (NOT p)) (zlfm (NOT q))"
chaieb@23274
  1092
  "zlfm (NOT (Imp p q)) = And (zlfm p) (zlfm (NOT q))"
chaieb@23274
  1093
  "zlfm (NOT (Iff p q)) = Or (And(zlfm p) (zlfm(NOT q))) (And (zlfm(NOT p)) (zlfm q))"
chaieb@23274
  1094
  "zlfm (NOT (NOT p)) = zlfm p"
chaieb@23274
  1095
  "zlfm (NOT T) = F"
chaieb@23274
  1096
  "zlfm (NOT F) = T"
chaieb@23274
  1097
  "zlfm (NOT (Lt a)) = zlfm (Ge a)"
chaieb@23274
  1098
  "zlfm (NOT (Le a)) = zlfm (Gt a)"
chaieb@23274
  1099
  "zlfm (NOT (Gt a)) = zlfm (Le a)"
chaieb@23274
  1100
  "zlfm (NOT (Ge a)) = zlfm (Lt a)"
chaieb@23274
  1101
  "zlfm (NOT (Eq a)) = zlfm (NEq a)"
chaieb@23274
  1102
  "zlfm (NOT (NEq a)) = zlfm (Eq a)"
chaieb@23274
  1103
  "zlfm (NOT (Dvd i a)) = zlfm (NDvd i a)"
chaieb@23274
  1104
  "zlfm (NOT (NDvd i a)) = zlfm (Dvd i a)"
chaieb@23274
  1105
  "zlfm (NOT (Closed P)) = NClosed P"
chaieb@23274
  1106
  "zlfm (NOT (NClosed P)) = Closed P"
chaieb@23274
  1107
  "zlfm p = p" (hints simp add: fmsize_pos)
chaieb@23274
  1108
chaieb@23274
  1109
lemma zlfm_I:
chaieb@23274
  1110
  assumes qfp: "qfree p"
wenzelm@55981
  1111
  shows "Ifm bbs (i # bs) (zlfm p) = Ifm bbs (i # bs) p \<and> iszlfm (zlfm p)"
wenzelm@55981
  1112
  (is "?I (?l p) = ?I p \<and> ?L (?l p)")
wenzelm@50313
  1113
  using qfp
wenzelm@50313
  1114
proof (induct p rule: zlfm.induct)
wenzelm@50313
  1115
  case (5 a)
chaieb@23274
  1116
  let ?c = "fst (zsplit0 a)"
chaieb@23274
  1117
  let ?r = "snd (zsplit0 a)"
wenzelm@55844
  1118
  have spl: "zsplit0 a = (?c, ?r)"
wenzelm@55844
  1119
    by simp
wenzelm@50313
  1120
  from zsplit0_I[OF spl, where x="i" and bs="bs"]
wenzelm@55964
  1121
  have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
wenzelm@55844
  1122
    by auto
wenzelm@55964
  1123
  let ?N = "\<lambda>t. Inum (i # bs) t"
wenzelm@55964
  1124
  from 5 Ia nb show ?case
wenzelm@50313
  1125
    apply (auto simp add: Let_def split_def algebra_simps)
wenzelm@55844
  1126
    apply (cases "?r")
wenzelm@55844
  1127
    apply auto
wenzelm@55844
  1128
    apply (case_tac nat)
wenzelm@55844
  1129
    apply auto
chaieb@23995
  1130
    done
chaieb@23274
  1131
next
wenzelm@50313
  1132
  case (6 a)
chaieb@23274
  1133
  let ?c = "fst (zsplit0 a)"
chaieb@23274
  1134
  let ?r = "snd (zsplit0 a)"
wenzelm@55844
  1135
  have spl: "zsplit0 a = (?c, ?r)"
wenzelm@55844
  1136
    by simp
wenzelm@50313
  1137
  from zsplit0_I[OF spl, where x="i" and bs="bs"]
wenzelm@55964
  1138
  have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
wenzelm@55844
  1139
    by auto
wenzelm@55964
  1140
  let ?N = "\<lambda>t. Inum (i # bs) t"
wenzelm@50313
  1141
  from 6 Ia nb show ?case
wenzelm@50313
  1142
    apply (auto simp add: Let_def split_def algebra_simps)
wenzelm@55844
  1143
    apply (cases "?r")
wenzelm@55844
  1144
    apply auto
wenzelm@55844
  1145
    apply (case_tac nat)
wenzelm@55844
  1146
    apply auto
chaieb@23995
  1147
    done
chaieb@23274
  1148
next
wenzelm@50313
  1149
  case (7 a)
chaieb@23274
  1150
  let ?c = "fst (zsplit0 a)"
chaieb@23274
  1151
  let ?r = "snd (zsplit0 a)"
wenzelm@55844
  1152
  have spl: "zsplit0 a = (?c, ?r)"
wenzelm@55844
  1153
    by simp
wenzelm@50313
  1154
  from zsplit0_I[OF spl, where x="i" and bs="bs"]
wenzelm@55844
  1155
  have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
wenzelm@55844
  1156
    by auto
wenzelm@55964
  1157
  let ?N = "\<lambda>t. Inum (i # bs) t"
wenzelm@50313
  1158
  from 7 Ia nb show ?case
wenzelm@50313
  1159
    apply (auto simp add: Let_def split_def algebra_simps)
wenzelm@55844
  1160
    apply (cases "?r")
wenzelm@55844
  1161
    apply auto
wenzelm@55844
  1162
    apply (case_tac nat)
wenzelm@55844
  1163
    apply auto
chaieb@23995
  1164
    done
chaieb@23274
  1165
next
wenzelm@50313
  1166
  case (8 a)
chaieb@23274
  1167
  let ?c = "fst (zsplit0 a)"
chaieb@23274
  1168
  let ?r = "snd (zsplit0 a)"
wenzelm@55844
  1169
  have spl: "zsplit0 a = (?c, ?r)"
wenzelm@55844
  1170
    by simp
wenzelm@50313
  1171
  from zsplit0_I[OF spl, where x="i" and bs="bs"]
wenzelm@55964
  1172
  have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
wenzelm@55844
  1173
    by auto
wenzelm@55964
  1174
  let ?N = "\<lambda>t. Inum (i # bs) t"
wenzelm@55844
  1175
  from 8 Ia nb show ?case
wenzelm@50313
  1176
    apply (auto simp add: Let_def split_def algebra_simps)
wenzelm@55844
  1177
    apply (cases "?r")
wenzelm@55844
  1178
    apply auto
wenzelm@55844
  1179
    apply (case_tac nat)
wenzelm@55844
  1180
    apply auto
chaieb@23995
  1181
    done
chaieb@23274
  1182
next
wenzelm@50313
  1183
  case (9 a)
chaieb@23274
  1184
  let ?c = "fst (zsplit0 a)"
chaieb@23274
  1185
  let ?r = "snd (zsplit0 a)"
wenzelm@55844
  1186
  have spl: "zsplit0 a = (?c, ?r)"
wenzelm@55844
  1187
    by simp
wenzelm@50313
  1188
  from zsplit0_I[OF spl, where x="i" and bs="bs"]
wenzelm@55844
  1189
  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
wenzelm@55844
  1190
    by auto
wenzelm@55964
  1191
  let ?N = "\<lambda>t. Inum (i # bs) t"
wenzelm@55844
  1192
  from 9 Ia nb show ?case
wenzelm@50313
  1193
    apply (auto simp add: Let_def split_def algebra_simps)
wenzelm@55844
  1194
    apply (cases "?r")
wenzelm@55844
  1195
    apply auto
wenzelm@55844
  1196
    apply (case_tac nat)
wenzelm@55844
  1197
    apply auto
chaieb@23995
  1198
    done
chaieb@23274
  1199
next
wenzelm@50313
  1200
  case (10 a)
chaieb@23274
  1201
  let ?c = "fst (zsplit0 a)"
chaieb@23274
  1202
  let ?r = "snd (zsplit0 a)"
wenzelm@55844
  1203
  have spl: "zsplit0 a = (?c, ?r)"
wenzelm@55844
  1204
    by simp
wenzelm@50313
  1205
  from zsplit0_I[OF spl, where x="i" and bs="bs"]
wenzelm@55844
  1206
  have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
wenzelm@55844
  1207
    by auto
wenzelm@55964
  1208
  let ?N = "\<lambda>t. Inum (i # bs) t"
wenzelm@55844
  1209
  from 10 Ia nb show ?case
wenzelm@50313
  1210
    apply (auto simp add: Let_def split_def algebra_simps)
wenzelm@55844
  1211
    apply (cases "?r")
wenzelm@55844
  1212
    apply auto
wenzelm@55844
  1213
    apply (case_tac nat)
wenzelm@55844
  1214
    apply auto
chaieb@23995
  1215
    done
chaieb@17378
  1216
next
wenzelm@50313
  1217
  case (11 j a)
chaieb@23274
  1218
  let ?c = "fst (zsplit0 a)"
chaieb@23274
  1219
  let ?r = "snd (zsplit0 a)"
wenzelm@55844
  1220
  have spl: "zsplit0 a = (?c,?r)"
wenzelm@55844
  1221
    by simp
wenzelm@50313
  1222
  from zsplit0_I[OF spl, where x="i" and bs="bs"]
wenzelm@55844
  1223
  have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
wenzelm@55844
  1224
    by auto
wenzelm@50313
  1225
  let ?N = "\<lambda>t. Inum (i#bs) t"
wenzelm@55844
  1226
  have "j = 0 \<or> (j \<noteq> 0 \<and> ?c = 0) \<or> (j \<noteq> 0 \<and> ?c > 0) \<or> (j \<noteq> 0 \<and> ?c < 0)"
wenzelm@55844
  1227
    by arith
chaieb@23274
  1228
  moreover
wenzelm@55844
  1229
  {
wenzelm@55844
  1230
    assume "j = 0"
wenzelm@55844
  1231
    then have z: "zlfm (Dvd j a) = (zlfm (Eq a))"
wenzelm@55844
  1232
      by (simp add: Let_def)
wenzelm@55844
  1233
    then have ?case using 11 `j = 0`
wenzelm@55844
  1234
      by (simp del: zlfm.simps)
wenzelm@55844
  1235
  }
chaieb@23274
  1236
  moreover
wenzelm@55844
  1237
  {
wenzelm@55844
  1238
    assume "?c = 0" and "j \<noteq> 0"
wenzelm@55844
  1239
    then have ?case
nipkow@29700
  1240
      using zsplit0_I[OF spl, where x="i" and bs="bs"]
wenzelm@50313
  1241
    apply (auto simp add: Let_def split_def algebra_simps)
wenzelm@55844
  1242
    apply (cases "?r")
wenzelm@55844
  1243
    apply auto
wenzelm@55844
  1244
    apply (case_tac nat)
wenzelm@55844
  1245
    apply auto
wenzelm@55844
  1246
    done
wenzelm@55844
  1247
  }
chaieb@23274
  1248
  moreover
wenzelm@55844
  1249
  {
wenzelm@55844
  1250
    assume cp: "?c > 0" and jnz: "j \<noteq> 0"
wenzelm@55844
  1251
    then have l: "?L (?l (Dvd j a))"
chaieb@23274
  1252
      by (simp add: nb Let_def split_def)
wenzelm@55844
  1253
    then have ?case
wenzelm@55844
  1254
      using Ia cp jnz by (simp add: Let_def split_def)
wenzelm@55844
  1255
  }
chaieb@23274
  1256
  moreover
wenzelm@55844
  1257
  { 
wenzelm@55844
  1258
    assume cn: "?c < 0" and jnz: "j \<noteq> 0"
wenzelm@55844
  1259
    then have l: "?L (?l (Dvd j a))"
chaieb@23274
  1260
      by (simp add: nb Let_def split_def)
wenzelm@55844
  1261
    then have ?case
wenzelm@55844
  1262
      using Ia cn jnz dvd_minus_iff[of "abs j" "?c*i + ?N ?r"]
wenzelm@55844
  1263
      by (simp add: Let_def split_def)
wenzelm@55844
  1264
  }
chaieb@23274
  1265
  ultimately show ?case by blast
chaieb@17378
  1266
next
wenzelm@50313
  1267
  case (12 j a)
chaieb@23274
  1268
  let ?c = "fst (zsplit0 a)"
chaieb@23274
  1269
  let ?r = "snd (zsplit0 a)"
wenzelm@55844
  1270
  have spl: "zsplit0 a = (?c, ?r)"
wenzelm@55844
  1271
    by simp
wenzelm@50313
  1272
  from zsplit0_I[OF spl, where x="i" and bs="bs"]
wenzelm@55844
  1273
  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
wenzelm@55844
  1274
    by auto
wenzelm@55964
  1275
  let ?N = "\<lambda>t. Inum (i # bs) t"
wenzelm@55844
  1276
  have "j = 0 \<or> (j \<noteq> 0 \<and> ?c = 0) \<or> (j \<noteq> 0 \<and> ?c > 0) \<or> (j \<noteq> 0 \<and> ?c < 0)"
wenzelm@55844
  1277
    by arith
chaieb@23274
  1278
  moreover
wenzelm@55844
  1279
  {
wenzelm@55844
  1280
    assume "j = 0"
wenzelm@55964
  1281
    then have z: "zlfm (NDvd j a) = zlfm (NEq a)"
wenzelm@55844
  1282
      by (simp add: Let_def)
wenzelm@55844
  1283
    then have ?case
wenzelm@55844
  1284
      using assms 12 `j = 0` by (simp del: zlfm.simps)
wenzelm@55844
  1285
  }
chaieb@23274
  1286
  moreover
wenzelm@55844
  1287
  {
wenzelm@55844
  1288
    assume "?c = 0" and "j \<noteq> 0"
wenzelm@55844
  1289
    then have ?case
nipkow@29700
  1290
      using zsplit0_I[OF spl, where x="i" and bs="bs"]
wenzelm@50313
  1291
    apply (auto simp add: Let_def split_def algebra_simps)
wenzelm@55844
  1292
    apply (cases "?r")
wenzelm@55844
  1293
    apply auto
wenzelm@55844
  1294
    apply (case_tac nat)
wenzelm@55844
  1295
    apply auto
wenzelm@55844
  1296
    done
wenzelm@55844
  1297
  }
chaieb@23274
  1298
  moreover
wenzelm@55844
  1299
  {
wenzelm@55844
  1300
    assume cp: "?c > 0" and jnz: "j \<noteq> 0"
wenzelm@55844
  1301
    then have l: "?L (?l (Dvd j a))"
chaieb@23274
  1302
      by (simp add: nb Let_def split_def)
wenzelm@55844
  1303
    then have ?case using Ia cp jnz
wenzelm@55844
  1304
      by (simp add: Let_def split_def)
wenzelm@55844
  1305
  }
chaieb@23274
  1306
  moreover
wenzelm@55844
  1307
  {
wenzelm@55844
  1308
    assume cn: "?c < 0" and jnz: "j \<noteq> 0"
wenzelm@55844
  1309
    then have l: "?L (?l (Dvd j a))"
chaieb@23274
  1310
      by (simp add: nb Let_def split_def)
wenzelm@55844
  1311
    then have ?case
wenzelm@55844
  1312
      using Ia cn jnz dvd_minus_iff[of "abs j" "?c*i + ?N ?r"]
wenzelm@55844
  1313
      by (simp add: Let_def split_def)
wenzelm@55844
  1314
  }
chaieb@23274
  1315
  ultimately show ?case by blast
chaieb@23274
  1316
qed auto
chaieb@23274
  1317
wenzelm@50313
  1318
consts minusinf :: "fm \<Rightarrow> fm" -- {* Virtual substitution of @{text "-\<infinity>"} *}
chaieb@23274
  1319
recdef minusinf "measure size"
wenzelm@50313
  1320
  "minusinf (And p q) = And (minusinf p) (minusinf q)"
wenzelm@50313
  1321
  "minusinf (Or p q) = Or (minusinf p) (minusinf q)"
chaieb@23995
  1322
  "minusinf (Eq  (CN 0 c e)) = F"
chaieb@23995
  1323
  "minusinf (NEq (CN 0 c e)) = T"
chaieb@23995
  1324
  "minusinf (Lt  (CN 0 c e)) = T"
chaieb@23995
  1325
  "minusinf (Le  (CN 0 c e)) = T"
chaieb@23995
  1326
  "minusinf (Gt  (CN 0 c e)) = F"
chaieb@23995
  1327
  "minusinf (Ge  (CN 0 c e)) = F"
chaieb@23274
  1328
  "minusinf p = p"
chaieb@23274
  1329
chaieb@23274
  1330
lemma minusinf_qfree: "qfree p \<Longrightarrow> qfree (minusinf p)"
wenzelm@50313
  1331
  by (induct p rule: minusinf.induct) auto
chaieb@23274
  1332
wenzelm@50313
  1333
consts plusinf :: "fm \<Rightarrow> fm"  -- {* Virtual substitution of @{text "+\<infinity>"} *}
chaieb@23274
  1334
recdef plusinf "measure size"
wenzelm@50313
  1335
  "plusinf (And p q) = And (plusinf p) (plusinf q)"
wenzelm@50313
  1336
  "plusinf (Or p q) = Or (plusinf p) (plusinf q)"
chaieb@23995
  1337
  "plusinf (Eq  (CN 0 c e)) = F"
chaieb@23995
  1338
  "plusinf (NEq (CN 0 c e)) = T"
chaieb@23995
  1339
  "plusinf (Lt  (CN 0 c e)) = F"
chaieb@23995
  1340
  "plusinf (Le  (CN 0 c e)) = F"
chaieb@23995
  1341
  "plusinf (Gt  (CN 0 c e)) = T"
chaieb@23995
  1342
  "plusinf (Ge  (CN 0 c e)) = T"
chaieb@23274
  1343
  "plusinf p = p"
chaieb@23274
  1344
wenzelm@53015
  1345
consts \<delta> :: "fm \<Rightarrow> int"  -- {* Compute @{text "lcm {d| N\<^sup>? Dvd c*x+t \<in> p}"} *}
chaieb@23274
  1346
recdef \<delta> "measure size"
wenzelm@50313
  1347
  "\<delta> (And p q) = lcm (\<delta> p) (\<delta> q)"
wenzelm@50313
  1348
  "\<delta> (Or p q) = lcm (\<delta> p) (\<delta> q)"
chaieb@23995
  1349
  "\<delta> (Dvd i (CN 0 c e)) = i"
chaieb@23995
  1350
  "\<delta> (NDvd i (CN 0 c e)) = i"
chaieb@23274
  1351
  "\<delta> p = 1"
chaieb@23274
  1352
wenzelm@50313
  1353
consts d_\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool"  -- {* check if a given l divides all the ds above *}
wenzelm@50252
  1354
recdef d_\<delta> "measure size"
wenzelm@50313
  1355
  "d_\<delta> (And p q) = (\<lambda>d. d_\<delta> p d \<and> d_\<delta> q d)"
wenzelm@50313
  1356
  "d_\<delta> (Or p q) = (\<lambda>d. d_\<delta> p d \<and> d_\<delta> q d)"
wenzelm@50313
  1357
  "d_\<delta> (Dvd i (CN 0 c e)) = (\<lambda>d. i dvd d)"
wenzelm@50313
  1358
  "d_\<delta> (NDvd i (CN 0 c e)) = (\<lambda>d. i dvd d)"
wenzelm@50313
  1359
  "d_\<delta> p = (\<lambda>d. True)"
chaieb@23274
  1360
wenzelm@50313
  1361
lemma delta_mono:
chaieb@23274
  1362
  assumes lin: "iszlfm p"
wenzelm@50313
  1363
    and d: "d dvd d'"
wenzelm@50313
  1364
    and ad: "d_\<delta> p d"
wenzelm@50252
  1365
  shows "d_\<delta> p d'"
chaieb@23274
  1366
  using lin ad d
wenzelm@50313
  1367
proof (induct p rule: iszlfm.induct)
wenzelm@55844
  1368
  case (9 i c e)
wenzelm@55844
  1369
  then show ?case using d
nipkow@30042
  1370
    by (simp add: dvd_trans[of "i" "d" "d'"])
chaieb@17378
  1371
next
wenzelm@55844
  1372
  case (10 i c e)
wenzelm@55844
  1373
  then show ?case using d
nipkow@30042
  1374
    by (simp add: dvd_trans[of "i" "d" "d'"])
chaieb@23274
  1375
qed simp_all
chaieb@17378
  1376
wenzelm@50313
  1377
lemma \<delta>:
wenzelm@55885
  1378
  assumes lin: "iszlfm p"
wenzelm@50252
  1379
  shows "d_\<delta> p (\<delta> p) \<and> \<delta> p >0"
wenzelm@50313
  1380
  using lin
chaieb@23274
  1381
proof (induct p rule: iszlfm.induct)
wenzelm@50313
  1382
  case (1 p q)
chaieb@23274
  1383
  let ?d = "\<delta> (And p q)"
wenzelm@55844
  1384
  from 1 lcm_pos_int have dp: "?d > 0"
wenzelm@55844
  1385
    by simp
wenzelm@55844
  1386
  have d1: "\<delta> p dvd \<delta> (And p q)"
wenzelm@55844
  1387
    using 1 by simp
wenzelm@55844
  1388
  then have th: "d_\<delta> p ?d"
wenzelm@55844
  1389
    using delta_mono 1(2,3) by (simp only: iszlfm.simps)
wenzelm@55844
  1390
  have "\<delta> q dvd \<delta> (And p q)"
wenzelm@55844
  1391
    using 1 by simp
wenzelm@55844
  1392
  then have th': "d_\<delta> q ?d"
wenzelm@55844
  1393
    using delta_mono 1 by (simp only: iszlfm.simps)
wenzelm@55844
  1394
  from th th' dp show ?case
wenzelm@55844
  1395
    by simp
chaieb@23274
  1396
next
wenzelm@50313
  1397
  case (2 p q)
chaieb@23274
  1398
  let ?d = "\<delta> (And p q)"
wenzelm@55844
  1399
  from 2 lcm_pos_int have dp: "?d > 0"
wenzelm@55844
  1400
    by simp
wenzelm@55844
  1401
  have "\<delta> p dvd \<delta> (And p q)"
wenzelm@55844
  1402
    using 2 by simp
wenzelm@55844
  1403
  then have th: "d_\<delta> p ?d"
wenzelm@55844
  1404
    using delta_mono 2 by (simp only: iszlfm.simps)
wenzelm@55844
  1405
  have "\<delta> q dvd \<delta> (And p q)"
wenzelm@55844
  1406
    using 2 by simp
wenzelm@55844
  1407
  then have th': "d_\<delta> q ?d"
wenzelm@55844
  1408
    using delta_mono 2 by (simp only: iszlfm.simps)
wenzelm@55844
  1409
  from th th' dp show ?case
wenzelm@55844
  1410
    by simp
chaieb@17378
  1411
qed simp_all
chaieb@17378
  1412
chaieb@17378
  1413
wenzelm@55921
  1414
consts a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm"  -- {* adjust the coefficients of a formula *}
wenzelm@50252
  1415
recdef a_\<beta> "measure size"
wenzelm@50313
  1416
  "a_\<beta> (And p q) = (\<lambda>k. And (a_\<beta> p k) (a_\<beta> q k))"
wenzelm@50313
  1417
  "a_\<beta> (Or p q) = (\<lambda>k. Or (a_\<beta> p k) (a_\<beta> q k))"
wenzelm@50313
  1418
  "a_\<beta> (Eq  (CN 0 c e)) = (\<lambda>k. Eq (CN 0 1 (Mul (k div c) e)))"
wenzelm@50313
  1419
  "a_\<beta> (NEq (CN 0 c e)) = (\<lambda>k. NEq (CN 0 1 (Mul (k div c) e)))"
wenzelm@50313
  1420
  "a_\<beta> (Lt  (CN 0 c e)) = (\<lambda>k. Lt (CN 0 1 (Mul (k div c) e)))"
wenzelm@50313
  1421
  "a_\<beta> (Le  (CN 0 c e)) = (\<lambda>k. Le (CN 0 1 (Mul (k div c) e)))"
wenzelm@50313
  1422
  "a_\<beta> (Gt  (CN 0 c e)) = (\<lambda>k. Gt (CN 0 1 (Mul (k div c) e)))"
wenzelm@50313
  1423
  "a_\<beta> (Ge  (CN 0 c e)) = (\<lambda>k. Ge (CN 0 1 (Mul (k div c) e)))"
wenzelm@50313
  1424
  "a_\<beta> (Dvd i (CN 0 c e)) =(\<lambda>k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
wenzelm@50313
  1425
  "a_\<beta> (NDvd i (CN 0 c e))=(\<lambda>k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
wenzelm@50313
  1426
  "a_\<beta> p = (\<lambda>k. p)"
chaieb@17378
  1427
wenzelm@50313
  1428
consts d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool"  -- {* test if all coeffs c of c divide a given l *}
wenzelm@50252
  1429
recdef d_\<beta> "measure size"
wenzelm@50313
  1430
  "d_\<beta> (And p q) = (\<lambda>k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
wenzelm@50313
  1431
  "d_\<beta> (Or p q) = (\<lambda>k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
wenzelm@50313
  1432
  "d_\<beta> (Eq  (CN 0 c e)) = (\<lambda>k. c dvd k)"
wenzelm@50313
  1433
  "d_\<beta> (NEq (CN 0 c e)) = (\<lambda>k. c dvd k)"
wenzelm@50313
  1434
  "d_\<beta> (Lt  (CN 0 c e)) = (\<lambda>k. c dvd k)"
wenzelm@50313
  1435
  "d_\<beta> (Le  (CN 0 c e)) = (\<lambda>k. c dvd k)"
wenzelm@50313
  1436
  "d_\<beta> (Gt  (CN 0 c e)) = (\<lambda>k. c dvd k)"
wenzelm@50313
  1437
  "d_\<beta> (Ge  (CN 0 c e)) = (\<lambda>k. c dvd k)"
wenzelm@50313
  1438
  "d_\<beta> (Dvd i (CN 0 c e)) =(\<lambda>k. c dvd k)"
wenzelm@50313
  1439
  "d_\<beta> (NDvd i (CN 0 c e))=(\<lambda>k. c dvd k)"
wenzelm@50313
  1440
  "d_\<beta> p = (\<lambda>k. True)"
chaieb@17378
  1441
wenzelm@50313
  1442
consts \<zeta> :: "fm \<Rightarrow> int"  -- {* computes the lcm of all coefficients of x *}
chaieb@23274
  1443
recdef \<zeta> "measure size"
wenzelm@50313
  1444
  "\<zeta> (And p q) = lcm (\<zeta> p) (\<zeta> q)"
wenzelm@50313
  1445
  "\<zeta> (Or p q) = lcm (\<zeta> p) (\<zeta> q)"
chaieb@23995
  1446
  "\<zeta> (Eq  (CN 0 c e)) = c"
chaieb@23995
  1447
  "\<zeta> (NEq (CN 0 c e)) = c"
chaieb@23995
  1448
  "\<zeta> (Lt  (CN 0 c e)) = c"
chaieb@23995
  1449
  "\<zeta> (Le  (CN 0 c e)) = c"
chaieb@23995
  1450
  "\<zeta> (Gt  (CN 0 c e)) = c"
chaieb@23995
  1451
  "\<zeta> (Ge  (CN 0 c e)) = c"
chaieb@23995
  1452
  "\<zeta> (Dvd i (CN 0 c e)) = c"
chaieb@23995
  1453
  "\<zeta> (NDvd i (CN 0 c e))= c"
chaieb@23274
  1454
  "\<zeta> p = 1"
chaieb@17378
  1455
wenzelm@50313
  1456
consts \<beta> :: "fm \<Rightarrow> num list"
chaieb@23274
  1457
recdef \<beta> "measure size"
wenzelm@50313
  1458
  "\<beta> (And p q) = (\<beta> p @ \<beta> q)"
wenzelm@50313
  1459
  "\<beta> (Or p q) = (\<beta> p @ \<beta> q)"
chaieb@23995
  1460
  "\<beta> (Eq  (CN 0 c e)) = [Sub (C -1) e]"
chaieb@23995
  1461
  "\<beta> (NEq (CN 0 c e)) = [Neg e]"
chaieb@23995
  1462
  "\<beta> (Lt  (CN 0 c e)) = []"
chaieb@23995
  1463
  "\<beta> (Le  (CN 0 c e)) = []"
chaieb@23995
  1464
  "\<beta> (Gt  (CN 0 c e)) = [Neg e]"
chaieb@23995
  1465
  "\<beta> (Ge  (CN 0 c e)) = [Sub (C -1) e]"
chaieb@23274
  1466
  "\<beta> p = []"
wenzelm@19736
  1467
wenzelm@50313
  1468
consts \<alpha> :: "fm \<Rightarrow> num list"
chaieb@23274
  1469
recdef \<alpha> "measure size"
wenzelm@50313
  1470
  "\<alpha> (And p q) = (\<alpha> p @ \<alpha> q)"
wenzelm@50313
  1471
  "\<alpha> (Or p q) = (\<alpha> p @ \<alpha> q)"
chaieb@23995
  1472
  "\<alpha> (Eq  (CN 0 c e)) = [Add (C -1) e]"
chaieb@23995
  1473
  "\<alpha> (NEq (CN 0 c e)) = [e]"
chaieb@23995
  1474
  "\<alpha> (Lt  (CN 0 c e)) = [e]"
chaieb@23995
  1475
  "\<alpha> (Le  (CN 0 c e)) = [Add (C -1) e]"
chaieb@23995
  1476
  "\<alpha> (Gt  (CN 0 c e)) = []"
chaieb@23995
  1477
  "\<alpha> (Ge  (CN 0 c e)) = []"
chaieb@23274
  1478
  "\<alpha> p = []"
wenzelm@50313
  1479
chaieb@23274
  1480
consts mirror :: "fm \<Rightarrow> fm"
chaieb@23274
  1481
recdef mirror "measure size"
wenzelm@50313
  1482
  "mirror (And p q) = And (mirror p) (mirror q)"
wenzelm@50313
  1483
  "mirror (Or p q) = Or (mirror p) (mirror q)"
chaieb@23995
  1484
  "mirror (Eq  (CN 0 c e)) = Eq (CN 0 c (Neg e))"
chaieb@23995
  1485
  "mirror (NEq (CN 0 c e)) = NEq (CN 0 c (Neg e))"
chaieb@23995
  1486
  "mirror (Lt  (CN 0 c e)) = Gt (CN 0 c (Neg e))"
chaieb@23995
  1487
  "mirror (Le  (CN 0 c e)) = Ge (CN 0 c (Neg e))"
chaieb@23995
  1488
  "mirror (Gt  (CN 0 c e)) = Lt (CN 0 c (Neg e))"
chaieb@23995
  1489
  "mirror (Ge  (CN 0 c e)) = Le (CN 0 c (Neg e))"
chaieb@23995
  1490
  "mirror (Dvd i (CN 0 c e)) = Dvd i (CN 0 c (Neg e))"
chaieb@23995
  1491
  "mirror (NDvd i (CN 0 c e)) = NDvd i (CN 0 c (Neg e))"
chaieb@23274
  1492
  "mirror p = p"
wenzelm@50313
  1493
wenzelm@50313
  1494
text {* Lemmas for the correctness of @{text "\<sigma>_\<rho>"} *}
wenzelm@50313
  1495
wenzelm@55844
  1496
lemma dvd1_eq1:
wenzelm@55844
  1497
  fixes x :: int
wenzelm@55844
  1498
  shows "x > 0 \<Longrightarrow> x dvd 1 \<longleftrightarrow> x = 1"
wenzelm@41807
  1499
  by simp
chaieb@17378
  1500
chaieb@23274
  1501
lemma minusinf_inf:
chaieb@23274
  1502
  assumes linp: "iszlfm p"
wenzelm@50313
  1503
    and u: "d_\<beta> p 1"
wenzelm@55964
  1504
  shows "\<exists>z::int. \<forall>x < z. Ifm bbs (x # bs) (minusinf p) = Ifm bbs (x # bs) p"
wenzelm@50313
  1505
  (is "?P p" is "\<exists>(z::int). \<forall>x < z. ?I x (?M p) = ?I x p")
wenzelm@50313
  1506
  using linp u
chaieb@23274
  1507
proof (induct p rule: minusinf.induct)
wenzelm@55844
  1508
  case (1 p q)
wenzelm@55844
  1509
  then show ?case
wenzelm@55964
  1510
    by auto (rule_tac x = "min z za" in exI, simp)
chaieb@23274
  1511
next
wenzelm@55844
  1512
  case (2 p q)
wenzelm@55844
  1513
  then show ?case
wenzelm@55964
  1514
    by auto (rule_tac x = "min z za" in exI, simp)
chaieb@17378
  1515
next
wenzelm@55844
  1516
  case (3 c e)
wenzelm@55844
  1517
  then have c1: "c = 1" and nb: "numbound0 e"
wenzelm@55844
  1518
    by simp_all
wenzelm@26934
  1519
  fix a
wenzelm@55844
  1520
  from 3 have "\<forall>x<(- Inum (a#bs) e). c * x + Inum (x # bs) e \<noteq> 0"
wenzelm@55844
  1521
  proof clarsimp
wenzelm@55844
  1522
    fix x
wenzelm@55844
  1523
    assume "x < (- Inum (a#bs) e)" and "x + Inum (x#bs) e = 0"
chaieb@23274
  1524
    with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
wenzelm@55844
  1525
    show False by simp
chaieb@23274
  1526
  qed
wenzelm@55844
  1527
  then show ?case by auto
chaieb@17378
  1528
next
wenzelm@55844
  1529
  case (4 c e)
wenzelm@55844
  1530
  then have c1: "c = 1" and nb: "numbound0 e"
wenzelm@55844
  1531
    by simp_all
wenzelm@26934
  1532
  fix a
wenzelm@55964
  1533
  from 4 have "\<forall>x < (- Inum (a # bs) e). c * x + Inum (x # bs) e \<noteq> 0"
wenzelm@55921
  1534
  proof clarsimp
wenzelm@55921
  1535
    fix x
wenzelm@55964
  1536
    assume "x < (- Inum (a # bs) e)" and "x + Inum (x # bs) e = 0"
chaieb@23274
  1537
    with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
chaieb@23274
  1538
    show "False" by simp
chaieb@23274
  1539
  qed
wenzelm@55885
  1540
  then show ?case by auto
chaieb@17378
  1541
next
wenzelm@55921
  1542
  case (5 c e)
wenzelm@55921
  1543
  then have c1: "c = 1" and nb: "numbound0 e"
wenzelm@55921
  1544
    by simp_all
wenzelm@26934
  1545
  fix a
wenzelm@55964
  1546
  from 5 have "\<forall>x<(- Inum (a # bs) e). c*x + Inum (x # bs) e < 0"
wenzelm@55921
  1547
  proof clarsimp
wenzelm@55921
  1548
    fix x
wenzelm@55964
  1549
    assume "x < (- Inum (a # bs) e)"
chaieb@23274
  1550
    with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
wenzelm@55921
  1551
    show "x + Inum (x # bs) e < 0"
wenzelm@55921
  1552
      by simp
chaieb@23274
  1553
  qed
wenzelm@55885
  1554
  then show ?case by auto
chaieb@23274
  1555
next
wenzelm@55921
  1556
  case (6 c e)
wenzelm@55921
  1557
  then have c1: "c = 1" and nb: "numbound0 e"
wenzelm@55921
  1558
    by simp_all
wenzelm@26934
  1559
  fix a
wenzelm@55964
  1560
  from 6 have "\<forall>x<(- Inum (a # bs) e). c * x + Inum (x # bs) e \<le> 0"
wenzelm@55921
  1561
  proof clarsimp
wenzelm@55921
  1562
    fix x
wenzelm@55964
  1563
    assume "x < (- Inum (a # bs) e)"
chaieb@23274
  1564
    with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
wenzelm@55964
  1565
    show "x + Inum (x # bs) e \<le> 0" by simp
chaieb@23274
  1566
  qed
wenzelm@55885
  1567
  then show ?case by auto
chaieb@23274
  1568
next
wenzelm@55921
  1569
  case (7 c e)
wenzelm@55921
  1570
  then have c1: "c = 1" and nb: "numbound0 e"
wenzelm@55921
  1571
    by simp_all
wenzelm@26934
  1572
  fix a
wenzelm@55964
  1573
  from 7 have "\<forall>x<(- Inum (a # bs) e). \<not> (c * x + Inum (x # bs) e > 0)"
wenzelm@55921
  1574
  proof clarsimp
wenzelm@55921
  1575
    fix x
wenzelm@55964
  1576
    assume "x < - Inum (a # bs) e" and "x + Inum (x # bs) e > 0"
chaieb@23274
  1577
    with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
wenzelm@55921
  1578
    show False by simp
chaieb@23274
  1579
  qed
wenzelm@55885
  1580
  then show ?case by auto
chaieb@23274
  1581
next
wenzelm@55921
  1582
  case (8 c e)
wenzelm@55921
  1583
  then have c1: "c = 1" and nb: "numbound0 e"
wenzelm@55921
  1584
    by simp_all
wenzelm@26934
  1585
  fix a
wenzelm@50313
  1586
  from 8 have "\<forall>x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e \<ge> 0)"
wenzelm@55921
  1587
  proof clarsimp
wenzelm@55921
  1588
    fix x
wenzelm@55921
  1589
    assume "x < (- Inum (a#bs) e)" and "x + Inum (x#bs) e \<ge> 0"
chaieb@23274
  1590
    with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
wenzelm@55921
  1591
    show False by simp
chaieb@23274
  1592
  qed
wenzelm@55885
  1593
  then show ?case by auto
chaieb@23274
  1594
qed auto
chaieb@17378
  1595
chaieb@23274
  1596
lemma minusinf_repeats:
wenzelm@55921
  1597
  assumes d: "d_\<delta> p d"
wenzelm@55921
  1598
    and linp: "iszlfm p"
wenzelm@55921
  1599
  shows "Ifm bbs ((x - k * d) # bs) (minusinf p) = Ifm bbs (x # bs) (minusinf p)"
wenzelm@50313
  1600
  using linp d
wenzelm@50313
  1601
proof (induct p rule: iszlfm.induct)
wenzelm@50313
  1602
  case (9 i c e)
wenzelm@55921
  1603
  then have nbe: "numbound0 e" and id: "i dvd d"
wenzelm@55921
  1604
    by simp_all
wenzelm@55921
  1605
  then have "\<exists>k. d = i * k"
wenzelm@55921
  1606
    by (simp add: dvd_def)
wenzelm@55921
  1607
  then obtain "di" where di_def: "d = i * di"
wenzelm@55921
  1608
    by blast
wenzelm@50313
  1609
  show ?case
wenzelm@50313
  1610
  proof (simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib,
wenzelm@50313
  1611
      rule iffI)
wenzelm@55921
  1612
    assume "i dvd c * x - c * (k * d) + Inum (x # bs) e"
chaieb@23274
  1613
      (is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt")
wenzelm@55921
  1614
    then have "\<exists>l::int. ?rt = i * l"
wenzelm@55921
  1615
      by (simp add: dvd_def)
wenzelm@55964
  1616
    then have "\<exists>l::int. c * x + ?I x e = i * l + c * (k * i * di)"
wenzelm@50313
  1617
      by (simp add: algebra_simps di_def)
wenzelm@55964
  1618
    then have "\<exists>l::int. c * x + ?I x e = i* (l + c * k * di)"
wenzelm@50313
  1619
      by (simp add: algebra_simps)
wenzelm@55921
  1620
    then have "\<exists>l::int. c * x + ?I x e = i * l"
wenzelm@55921
  1621
      by blast
wenzelm@55921
  1622
    then show "i dvd c * x + Inum (x # bs) e"
wenzelm@55921
  1623
      by (simp add: dvd_def)
wenzelm@50313
  1624
  next
wenzelm@55964
  1625
    assume "i dvd c * x + Inum (x # bs) e"  (is "?ri dvd ?rc * ?rx + ?e")
wenzelm@55921
  1626
    then have "\<exists>l::int. c * x + ?e = i * l"
wenzelm@55921
  1627
      by (simp add: dvd_def)
wenzelm@55921
  1628
    then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l - c * (k * d)"
wenzelm@55921
  1629
      by simp
wenzelm@55921
  1630
    then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l - c * (k * i * di)"
wenzelm@55921
  1631
      by (simp add: di_def)
wenzelm@55964
  1632
    then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * (l - c * k * di)"
wenzelm@55921
  1633
      by (simp add: algebra_simps)
wenzelm@55921
  1634
    then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l"
wenzelm@55921
  1635
      by blast
wenzelm@55921
  1636
    then show "i dvd c * x - c * (k * d) + Inum (x # bs) e"
wenzelm@55921
  1637
      by (simp add: dvd_def)
wenzelm@50313
  1638
  qed
chaieb@23274
  1639
next
wenzelm@50313
  1640
  case (10 i c e)
wenzelm@55921
  1641
  then have nbe: "numbound0 e" and id: "i dvd d"
wenzelm@55921
  1642
    by simp_all
wenzelm@55921
  1643
  then have "\<exists>k. d = i * k"
wenzelm@55921
  1644
    by (simp add: dvd_def)
wenzelm@55921
  1645
  then obtain di where di_def: "d = i * di"
wenzelm@55921
  1646
    by blast
wenzelm@50313
  1647
  show ?case
wenzelm@55921
  1648
  proof (simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib, rule iffI)
wenzelm@55921
  1649
    assume "i dvd c * x - c * (k * d) + Inum (x # bs) e"
chaieb@23274
  1650
      (is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt")
wenzelm@55921
  1651
    then have "\<exists>l::int. ?rt = i * l"
wenzelm@55921
  1652
      by (simp add: dvd_def)
wenzelm@55921
  1653
    then have "\<exists>l::int. c * x + ?I x e = i * l + c * (k * i * di)"
wenzelm@50313
  1654
      by (simp add: algebra_simps di_def)
wenzelm@55921
  1655
    then have "\<exists>l::int. c * x+ ?I x e = i * (l + c * k * di)"
wenzelm@50313
  1656
      by (simp add: algebra_simps)
wenzelm@55921
  1657
    then have "\<exists>l::int. c * x + ?I x e = i * l"
wenzelm@55921
  1658
      by blast
wenzelm@55921
  1659
    then show "i dvd c * x + Inum (x # bs) e"
wenzelm@55921
  1660
      by (simp add: dvd_def)
wenzelm@50313
  1661
  next
wenzelm@55921
  1662
    assume "i dvd c * x + Inum (x # bs) e" (is "?ri dvd ?rc * ?rx + ?e")
wenzelm@55921
  1663
    then have "\<exists>l::int. c * x + ?e = i * l"
wenzelm@55921
  1664
      by (simp add: dvd_def)
wenzelm@55921
  1665
    then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l - c * (k * d)"
wenzelm@55921
  1666
      by simp
wenzelm@55921
  1667
    then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l - c * (k * i * di)"
wenzelm@55921
  1668
      by (simp add: di_def)
wenzelm@55921
  1669
    then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * ((l - c * k * di))"
wenzelm@55921
  1670
      by (simp add: algebra_simps)
wenzelm@55921
  1671
    then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l"
wenzelm@50313
  1672
      by blast
wenzelm@55921
  1673
    then show "i dvd c * x - c * (k * d) + Inum (x # bs) e"
wenzelm@55921
  1674
      by (simp add: dvd_def)
wenzelm@50313
  1675
  qed
haftmann@23689
  1676
qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="x - k*d" and b'="x"])
chaieb@17378
  1677
wenzelm@50252
  1678
lemma mirror_\<alpha>_\<beta>:
chaieb@23274
  1679
  assumes lp: "iszlfm p"
wenzelm@55964
  1680
  shows "Inum (i # bs) ` set (\<alpha> p) = Inum (i # bs) ` set (\<beta> (mirror p))"
wenzelm@50313
  1681
  using lp by (induct p rule: mirror.induct) auto
chaieb@17378
  1682
wenzelm@50313
  1683
lemma mirror:
chaieb@23274
  1684
  assumes lp: "iszlfm p"
wenzelm@55921
  1685
  shows "Ifm bbs (x # bs) (mirror p) = Ifm bbs ((- x) # bs) p"
wenzelm@50313
  1686
  using lp
wenzelm@50313
  1687
proof (induct p rule: iszlfm.induct)
wenzelm@50313
  1688
  case (9 j c e)
wenzelm@55964
  1689
  then have nb: "numbound0 e"
wenzelm@55964
  1690
    by simp
wenzelm@55964
  1691
  have "Ifm bbs (x # bs) (mirror (Dvd j (CN 0 c e))) \<longleftrightarrow> j dvd c * x - Inum (x # bs) e"
wenzelm@50313
  1692
    (is "_ = (j dvd c*x - ?e)") by simp
wenzelm@55964
  1693
  also have "\<dots> \<longleftrightarrow> j dvd (- (c * x - ?e))"
nipkow@30042
  1694
    by (simp only: dvd_minus_iff)
wenzelm@55964
  1695
  also have "\<dots> \<longleftrightarrow> j dvd (c * (- x)) + ?e"
haftmann@54230
  1696
    by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] add_ac minus_add_distrib)
haftmann@54230
  1697
      (simp add: algebra_simps)
wenzelm@55964
  1698
  also have "\<dots> = Ifm bbs ((- x) # bs) (Dvd j (CN 0 c e))"
wenzelm@50313
  1699
    using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp
chaieb@23274
  1700
  finally show ?case .
chaieb@23274
  1701
next
wenzelm@55964
  1702
  case (10 j c e)
wenzelm@55964
  1703
  then have nb: "numbound0 e"
wenzelm@55964
  1704
    by simp
wenzelm@55964
  1705
  have "Ifm bbs (x # bs) (mirror (Dvd j (CN 0 c e))) \<longleftrightarrow> j dvd c * x - Inum (x # bs) e"
wenzelm@55964
  1706
    (is "_ = (j dvd c * x - ?e)") by simp
wenzelm@55964
  1707
  also have "\<dots> \<longleftrightarrow> j dvd (- (c * x - ?e))"
nipkow@30042
  1708
    by (simp only: dvd_minus_iff)
wenzelm@55964
  1709
  also have "\<dots> \<longleftrightarrow> j dvd (c * (- x)) + ?e"
haftmann@54230
  1710
    by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] add_ac minus_add_distrib)
haftmann@54230
  1711
      (simp add: algebra_simps)
wenzelm@55964
  1712
  also have "\<dots> \<longleftrightarrow> Ifm bbs ((- x) # bs) (Dvd j (CN 0 c e))"
wenzelm@50313
  1713
    using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp
chaieb@23274
  1714
  finally show ?case by simp
haftmann@23689
  1715
qed (auto simp add: numbound0_I[where bs="bs" and b="x" and b'="- x"] gr0_conv_Suc)
chaieb@17378
  1716
wenzelm@50313
  1717
lemma mirror_l: "iszlfm p \<and> d_\<beta> p 1 \<Longrightarrow> iszlfm (mirror p) \<and> d_\<beta> (mirror p) 1"
wenzelm@41807
  1718
  by (induct p rule: mirror.induct) auto
chaieb@17378
  1719
chaieb@23274
  1720
lemma mirror_\<delta>: "iszlfm p \<Longrightarrow> \<delta> (mirror p) = \<delta> p"
wenzelm@41807
  1721
  by (induct p rule: mirror.induct) auto
chaieb@23274
  1722
wenzelm@50313
  1723
lemma \<beta>_numbound0:
wenzelm@50313
  1724
  assumes lp: "iszlfm p"
wenzelm@55964
  1725
  shows "\<forall>b \<in> set (\<beta> p). numbound0 b"
wenzelm@41807
  1726
  using lp by (induct p rule: \<beta>.induct) auto
chaieb@17378
  1727
wenzelm@50313
  1728
lemma d_\<beta>_mono:
chaieb@23274
  1729
  assumes linp: "iszlfm p"
wenzelm@50313
  1730
    and dr: "d_\<beta> p l"
wenzelm@50313
  1731
    and d: "l dvd l'"
wenzelm@50252
  1732
  shows "d_\<beta> p l'"
wenzelm@50313
  1733
  using dr linp dvd_trans[of _ "l" "l'", simplified d]
wenzelm@41807
  1734
  by (induct p rule: iszlfm.induct) simp_all
chaieb@23274
  1735
wenzelm@50313
  1736
lemma \<alpha>_l:
wenzelm@50313
  1737
  assumes lp: "iszlfm p"
wenzelm@50313
  1738
  shows "\<forall>b \<in> set (\<alpha> p). numbound0 b"
wenzelm@50313
  1739
  using lp by (induct p rule: \<alpha>.induct) auto
chaieb@17378
  1740
wenzelm@50313
  1741
lemma \<zeta>:
chaieb@23274
  1742
  assumes linp: "iszlfm p"
wenzelm@50252
  1743
  shows "\<zeta> p > 0 \<and> d_\<beta> p (\<zeta> p)"
wenzelm@50313
  1744
  using linp
wenzelm@50313
  1745
proof (induct p rule: iszlfm.induct)
chaieb@23274
  1746
  case (1 p q)
wenzelm@55964
  1747
  from 1 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)"
wenzelm@55964
  1748
    by simp
wenzelm@55964
  1749
  from 1 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)"
wenzelm@55964
  1750
    by simp
wenzelm@50313
  1751
  from 1 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
wenzelm@55964
  1752
      d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
wenzelm@55964
  1753
      dl1 dl2
wenzelm@55964
  1754
  show ?case
wenzelm@55964
  1755
    by (auto simp add: lcm_pos_int)
chaieb@17378
  1756
next
chaieb@23274
  1757
  case (2 p q)
wenzelm@55964
  1758
  from 2 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)"
wenzelm@55964
  1759
    by simp
wenzelm@55964
  1760
  from 2 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)"
wenzelm@55964
  1761
    by simp
wenzelm@50313
  1762
  from 2 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
wenzelm@55964
  1763
      d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
wenzelm@55964
  1764
      dl1 dl2
wenzelm@55964
  1765
  show ?case
wenzelm@55964
  1766
    by (auto simp add: lcm_pos_int)
nipkow@31952
  1767
qed (auto simp add: lcm_pos_int)
chaieb@17378
  1768
wenzelm@50313
  1769
lemma a_\<beta>:
wenzelm@55921
  1770
  assumes linp: "iszlfm p"
wenzelm@55921
  1771
    and d: "d_\<beta> p l"
wenzelm@55921
  1772
    and lp: "l > 0"
wenzelm@55964
  1773
  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"
wenzelm@50313
  1774
  using linp d
chaieb@23274
  1775
proof (induct p rule: iszlfm.induct)
wenzelm@50313
  1776
  case (5 c e)
wenzelm@55964
  1777
  then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l"
wenzelm@55921
  1778
    by simp_all
wenzelm@55921
  1779
  from lp cp have clel: "c \<le> l"
wenzelm@55921
  1780
    by (simp add: zdvd_imp_le [OF d' lp])
wenzelm@55921
  1781
  from cp have cnz: "c \<noteq> 0"
wenzelm@55921
  1782
    by simp
wenzelm@55921
  1783
  have "c div c \<le> l div c"
wenzelm@50313
  1784
    by (simp add: zdiv_mono1[OF clel cp])
wenzelm@50313
  1785
  then have ldcp:"0 < l div c"
wenzelm@50313
  1786
    by (simp add: div_self[OF cnz])
wenzelm@55921
  1787
  have "c * (l div c) = c * (l div c) + l mod c"
wenzelm@55921
  1788
    using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
wenzelm@55921
  1789
  then have cl: "c * (l div c) =l"
wenzelm@55921
  1790
    using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
wenzelm@55964
  1791
  then have "(l * x + (l div c) * Inum (x # bs) e < 0) \<longleftrightarrow>
wenzelm@50313
  1792
      ((c * (l div c)) * x + (l div c) * Inum (x # bs) e < 0)"
wenzelm@50313
  1793
    by simp
wenzelm@55964
  1794
  also have "\<dots> \<longleftrightarrow> (l div c) * (c*x + Inum (x # bs) e) < (l div c) * 0"
wenzelm@50313
  1795
    by (simp add: algebra_simps)
wenzelm@55964
  1796
  also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e < 0"
wenzelm@55964
  1797
    using mult_less_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp
wenzelm@55964
  1798
    by simp
wenzelm@50313
  1799
  finally show ?case
wenzelm@55964
  1800
    using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be
wenzelm@55964
  1801
    by simp
chaieb@17378
  1802
next
wenzelm@50313
  1803
  case (6 c e)
wenzelm@55921
  1804
  then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l"
wenzelm@55921
  1805
    by simp_all
wenzelm@55921
  1806
  from lp cp have clel: "c \<le> l"
wenzelm@55921
  1807
    by (simp add: zdvd_imp_le [OF d' lp])
wenzelm@55921
  1808
  from cp have cnz: "c \<noteq> 0"
wenzelm@55921
  1809
    by simp
wenzelm@55964
  1810
  have "c div c \<le> l div c"
wenzelm@50313
  1811
    by (simp add: zdiv_mono1[OF clel cp])
wenzelm@50313
  1812
  then have ldcp:"0 < l div c"
wenzelm@50313
  1813
    by (simp add: div_self[OF cnz])
wenzelm@55964
  1814
  have "c * (l div c) = c * (l div c) + l mod c"
wenzelm@55921
  1815
    using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
wenzelm@55921
  1816
  then have cl: "c * (l div c) = l"
wenzelm@55921
  1817
    using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
wenzelm@55964
  1818
  then have "l * x + (l div c) * Inum (x # bs) e \<le> 0 \<longleftrightarrow>
wenzelm@55964
  1819
      (c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0"
wenzelm@50313
  1820
    by simp
wenzelm@55964
  1821
  also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) \<le> (l div c) * 0"
wenzelm@50313
  1822
    by (simp add: algebra_simps)
wenzelm@55964
  1823
  also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e \<le> 0"
chaieb@23274
  1824
    using mult_le_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp by simp
wenzelm@50313
  1825
  finally show ?case
wenzelm@50313
  1826
    using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be by simp
chaieb@17378
  1827
next
wenzelm@50313
  1828
  case (7 c e)
wenzelm@55921
  1829
  then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l"
wenzelm@55921
  1830
    by simp_all
wenzelm@55921
  1831
  from lp cp have clel: "c \<le> l"
wenzelm@55921
  1832
    by (simp add: zdvd_imp_le [OF d' lp])
wenzelm@55921
  1833
  from cp have cnz: "c \<noteq> 0"
wenzelm@55921
  1834
    by simp
wenzelm@55921
  1835
  have "c div c \<le> l div c"
wenzelm@55921
  1836
    by (simp add: zdiv_mono1[OF clel cp])
wenzelm@55964
  1837
  then have ldcp: "0 < l div c"
wenzelm@55921
  1838
    by (simp add: div_self[OF cnz])
wenzelm@55964
  1839
  have "c * (l div c) = c * (l div c) + l mod c"
wenzelm@55921
  1840
    using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
wenzelm@55964
  1841
  then have cl: "c * (l div c) = l"
wenzelm@55921
  1842
    using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
wenzelm@55964
  1843
  then have "l * x + (l div c) * Inum (x # bs) e > 0 \<longleftrightarrow>
wenzelm@55964
  1844
      (c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0"
wenzelm@55921
  1845
    by simp
wenzelm@55964
  1846
  also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) > (l div c) * 0"
wenzelm@55921
  1847
    by (simp add: algebra_simps)
wenzelm@55964
  1848
  also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e > 0"
wenzelm@55921
  1849
    using zero_less_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp
wenzelm@55921
  1850
    by simp
wenzelm@55921
  1851
  finally show ?case
wenzelm@55921
  1852
    using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be
wenzelm@55921
  1853
    by simp
wenzelm@55921
  1854
next
wenzelm@55921
  1855
  case (8 c e)
wenzelm@55921
  1856
  then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l"
wenzelm@55921
  1857
    by simp_all
wenzelm@55921
  1858
  from lp cp have clel: "c \<le> l"
wenzelm@55921
  1859
    by (simp add: zdvd_imp_le [OF d' lp])
wenzelm@55921
  1860
  from cp have cnz: "c \<noteq> 0"
wenzelm@55921
  1861
    by simp
wenzelm@55921
  1862
  have "c div c \<le> l div c"
wenzelm@55921
  1863
    by (simp add: zdiv_mono1[OF clel cp])
wenzelm@55921
  1864
  then have ldcp: "0 < l div c"
wenzelm@55921
  1865
    by (simp add: div_self[OF cnz])
wenzelm@55964
  1866
  have "c * (l div c) = c * (l div c) + l mod c"
wenzelm@55921
  1867
    using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
wenzelm@55921
  1868
  then have cl: "c * (l div c) =l"
wenzelm@55921
  1869
    using zmod_zdiv_equality[where a="l" and b="c", symmetric]
wenzelm@55921
  1870
    by simp
wenzelm@55964
  1871
  then have "l * x + (l div c) * Inum (x # bs) e \<ge> 0 \<longleftrightarrow>
wenzelm@55964
  1872
      (c * (l div c)) * x + (l div c) * Inum (x # bs) e \<ge> 0"
wenzelm@55921
  1873
    by simp
wenzelm@55964
  1874
  also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) \<ge> (l div c) * 0"
wenzelm@55921
  1875
    by (simp add: algebra_simps)
wenzelm@55964
  1876
  also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e \<ge> 0"
wenzelm@55921
  1877
    using ldcp zero_le_mult_iff [where a="l div c" and b="c*x + Inum (x # bs) e"]
wenzelm@55921
  1878
    by simp
wenzelm@55921
  1879
  finally show ?case
wenzelm@55921
  1880
    using be numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"]
wenzelm@55921
  1881
    by simp
wenzelm@55921
  1882
next
wenzelm@55921
  1883
  case (3 c e)
wenzelm@55921
  1884
  then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l"
wenzelm@55921
  1885
    by simp_all
wenzelm@55921
  1886
  from lp cp have clel: "c \<le> l"
wenzelm@55921
  1887
    by (simp add: zdvd_imp_le [OF d' lp])
wenzelm@55921
  1888
  from cp have cnz: "c \<noteq> 0"
wenzelm@55921
  1889
    by simp
wenzelm@55921
  1890
  have "c div c \<le> l div c"
wenzelm@50313
  1891
    by (simp add: zdiv_mono1[OF clel cp])
wenzelm@50313
  1892
  then have ldcp:"0 < l div c"
wenzelm@50313
  1893
    by (simp add: div_self[OF cnz])
wenzelm@55964
  1894
  have "c * (l div c) = c * (l div c) + l mod c"
wenzelm@50313
  1895
    using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
wenzelm@55885
  1896
  then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
wenzelm@50313
  1897
    by simp
wenzelm@55964
  1898
  then have "l * x + (l div c) * Inum (x # bs) e = 0 \<longleftrightarrow>
wenzelm@55964
  1899
      (c * (l div c)) * x + (l div c) * Inum (x # bs) e = 0"
chaieb@23274
  1900
    by simp
wenzelm@55964
  1901
  also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) = ((l div c)) * 0"
wenzelm@50313
  1902
    by (simp add: algebra_simps)
wenzelm@55964
  1903
  also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e = 0"
wenzelm@55921
  1904
    using mult_eq_0_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp
wenzelm@55921
  1905
    by simp
wenzelm@50313
  1906
  finally show ?case
wenzelm@55921
  1907
    using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be
wenzelm@55921
  1908
    by simp
chaieb@17378
  1909
next
wenzelm@50313
  1910
  case (4 c e)
wenzelm@55921
  1911
  then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l"
wenzelm@55921
  1912
    by simp_all
wenzelm@55921
  1913
  from lp cp have clel: "c \<le> l"
wenzelm@55921
  1914
    by (simp add: zdvd_imp_le [OF d' lp])
wenzelm@55921
  1915
  from cp have cnz: "c \<noteq> 0"
wenzelm@55921
  1916
    by simp
wenzelm@55921
  1917
  have "c div c \<le> l div c"
wenzelm@50313
  1918
    by (simp add: zdiv_mono1[OF clel cp])
wenzelm@50313
  1919
  then have ldcp:"0 < l div c"
wenzelm@50313
  1920
    by (simp add: div_self[OF cnz])
wenzelm@55964
  1921
  have "c * (l div c) = c * (l div c) + l mod c"
wenzelm@55921
  1922
    using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
wenzelm@55921
  1923
  then have cl: "c * (l div c) = l"
wenzelm@55921
  1924
    using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
wenzelm@55964
  1925
  then have "l * x + (l div c) * Inum (x # bs) e \<noteq> 0 \<longleftrightarrow>
wenzelm@55921
  1926
      (c * (l div c)) * x + (l div c) * Inum (x # bs) e \<noteq> 0"
wenzelm@50313
  1927
    by simp
wenzelm@55921
  1928
  also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) \<noteq> (l div c) * 0"
wenzelm@50313
  1929
    by (simp add: algebra_simps)
wenzelm@55921
  1930
  also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e \<noteq> 0"
wenzelm@55921
  1931
    using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp
wenzelm@55921
  1932
    by simp
wenzelm@50313
  1933
  finally show ?case
wenzelm@55921
  1934
    using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be
wenzelm@55921
  1935
    by simp
chaieb@17378
  1936
next
wenzelm@50313
  1937
  case (9 j c e)
wenzelm@55921
  1938
  then have cp: "c > 0" and be: "numbound0 e" and jp: "j > 0" and d': "c dvd l"
wenzelm@55921
  1939
    by simp_all
wenzelm@55921
  1940
  from lp cp have clel: "c \<le> l"
wenzelm@55921
  1941
    by (simp add: zdvd_imp_le [OF d' lp])
wenzelm@50313
  1942
  from cp have cnz: "c \<noteq> 0" by simp
wenzelm@50313
  1943
  have "c div c\<le> l div c"
wenzelm@50313
  1944
    by (simp add: zdiv_mono1[OF clel cp])
wenzelm@50313
  1945
  then have ldcp:"0 < l div c"
wenzelm@50313
  1946
    by (simp add: div_self[OF cnz])
wenzelm@55964
  1947
  have "c * (l div c) = c * (l div c) + l mod c"
wenzelm@55885
  1948
    using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
wenzelm@55921
  1949
  then have cl: "c * (l div c) = l"
wenzelm@55885
  1950
    using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
wenzelm@55921
  1951
  then have "(\<exists>k::int. l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) \<longleftrightarrow>
wenzelm@55964
  1952
      (\<exists>k::int. (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"
wenzelm@55921
  1953
    by simp
wenzelm@55964
  1954
  also have "\<dots> \<longleftrightarrow> (\<exists>k::int. (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c) * 0)"
wenzelm@55921
  1955
    by (simp add: algebra_simps)
wenzelm@55921
  1956
  also
wenzelm@55921
  1957
  fix k
wenzelm@55921
  1958
  have "\<dots> \<longleftrightarrow> (\<exists>k::int. c * x + Inum (x # bs) e - j * k = 0)"
wenzelm@55921
  1959
    using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp
wenzelm@55921
  1960
    by simp
wenzelm@55921
  1961
  also have "\<dots> \<longleftrightarrow> (\<exists>k::int. c * x + Inum (x # bs) e = j * k)"
wenzelm@55921
  1962
    by simp
wenzelm@55921
  1963
  finally show ?case
wenzelm@55921
  1964
    using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"]
wenzelm@55921
  1965
      be mult_strict_mono[OF ldcp jp ldcp ]
wenzelm@55921
  1966
    by (simp add: dvd_def)
wenzelm@55921
  1967
next
wenzelm@55921
  1968
  case (10 j c e)
wenzelm@55921
  1969
  then have cp: "c > 0" and be: "numbound0 e" and jp: "j > 0" and d': "c dvd l"
wenzelm@55921
  1970
    by simp_all
wenzelm@55921
  1971
  from lp cp have clel: "c \<le> l"
wenzelm@55921
  1972
    by (simp add: zdvd_imp_le [OF d' lp])
wenzelm@55921
  1973
  from cp have cnz: "c \<noteq> 0"
wenzelm@50313
  1974
    by simp
wenzelm@55921
  1975
  have "c div c \<le> l div c"
wenzelm@55921
  1976
    by (simp add: zdiv_mono1[OF clel cp])
wenzelm@55921
  1977
  then have ldcp: "0 < l div c"
wenzelm@55921
  1978
    by (simp add: div_self[OF cnz])
wenzelm@55921
  1979
  have "c * (l div c) = c* (l div c) + l mod c"
wenzelm@55921
  1980
    using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
wenzelm@55921
  1981
  then have cl:"c * (l div c) =l"
wenzelm@55921
  1982
    using zmod_zdiv_equality[where a="l" and b="c", symmetric]
wenzelm@55921
  1983
    by simp
wenzelm@55921
  1984
  then have "(\<exists>k::int. l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) \<longleftrightarrow>
wenzelm@55921
  1985
      (\<exists>k::int. (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"
wenzelm@55921
  1986
    by simp
wenzelm@55921
  1987
  also have "\<dots> \<longleftrightarrow> (\<exists>k::int. (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c) * 0)"
wenzelm@55921
  1988
    by (simp add: algebra_simps)
wenzelm@55921
  1989
  also
wenzelm@55921
  1990
  fix k
wenzelm@55964
  1991
  have "\<dots> \<longleftrightarrow> (\<exists>k::int. c * x + Inum (x # bs) e - j * k = 0)"
wenzelm@55921
  1992
    using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp
wenzelm@55921
  1993
    by simp
wenzelm@55964
  1994
  also have "\<dots> \<longleftrightarrow> (\<exists>k::int. c * x + Inum (x # bs) e = j * k)"
wenzelm@55921
  1995
    by simp
wenzelm@55921
  1996
  finally show ?case
wenzelm@55921
  1997
    using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be
wenzelm@55921
  1998
      mult_strict_mono[OF ldcp jp ldcp ]
wenzelm@55921
  1999
    by (simp add: dvd_def)
haftmann@23689
  2000
qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="(l * x)" and b'="x"])
chaieb@17378
  2001
wenzelm@55921
  2002
lemma a_\<beta>_ex:
wenzelm@55921
  2003
  assumes linp: "iszlfm p"
wenzelm@55921
  2004
    and d: "d_\<beta> p l"
wenzelm@55921
  2005
    and lp: "l > 0"
wenzelm@55921
  2006
  shows "(\<exists>x. l dvd x \<and> Ifm bbs (x #bs) (a_\<beta> p l)) \<longleftrightarrow> (\<exists>x::int. Ifm bbs (x#bs) p)"
wenzelm@55921
  2007
  (is "(\<exists>x. l dvd x \<and> ?P x) \<longleftrightarrow> (\<exists>x. ?P' x)")
chaieb@23274
  2008
proof-
wenzelm@55921
  2009
  have "(\<exists>x. l dvd x \<and> ?P x) \<longleftrightarrow> (\<exists>(x::int). ?P (l*x))"
chaieb@23274
  2010
    using unity_coeff_ex[where l="l" and P="?P", simplified] by simp
wenzelm@55921
  2011
  also have "\<dots> = (\<exists>x::int. ?P' x)"
wenzelm@55921
  2012
    using a_\<beta>[OF linp d lp] by simp
wenzelm@50313
  2013
  finally show ?thesis  .
chaieb@17378
  2014
qed
chaieb@17378
  2015
chaieb@23274
  2016
lemma \<beta>:
chaieb@23274
  2017
  assumes lp: "iszlfm p"
wenzelm@55885
  2018
    and u: "d_\<beta> p 1"
wenzelm@55885
  2019
    and d: "d_\<delta> p d"
wenzelm@55885
  2020
    and dp: "d > 0"
wenzelm@55964
  2021
    and nob: "\<not> (\<exists>j::int \<in> {1 .. d}. \<exists>b \<in> Inum (a # bs) ` set (\<beta> p). x = b + j)"
wenzelm@55964
  2022
    and p: "Ifm bbs (x # bs) p" (is "?P x")
chaieb@23274
  2023
  shows "?P (x - d)"
wenzelm@55885
  2024
  using lp u d dp nob p
wenzelm@55885
  2025
proof (induct p rule: iszlfm.induct)
wenzelm@55885
  2026
  case (5 c e)
wenzelm@55885
  2027
  then have c1: "c = 1" and  bn: "numbound0 e"
wenzelm@55885
  2028
    by simp_all
wenzelm@55964
  2029
  with dp p c1 numbound0_I[OF bn,where b = "(x - d)" and b' = "x" and bs = "bs"] 5
wenzelm@41807
  2030
  show ?case by simp
chaieb@23274
  2031
next
wenzelm@55885
  2032
  case (6 c e)
wenzelm@55885
  2033
  then have c1: "c = 1" and  bn: "numbound0 e"
wenzelm@55885
  2034
    by simp_all
wenzelm@41807
  2035
  with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] 6
wenzelm@41807
  2036
  show ?case by simp
chaieb@23274
  2037
next
wenzelm@55885
  2038
  case (7 c e)
wenzelm@55964
  2039
  then have p: "Ifm bbs (x # bs) (Gt (CN 0 c e))" and c1: "c=1" and bn: "numbound0 e"
wenzelm@55885
  2040
    by simp_all
wenzelm@41807
  2041
  let ?e = "Inum (x # bs) e"
wenzelm@55885
  2042
  {
wenzelm@55964
  2043
    assume "(x - d) + ?e > 0"
wenzelm@55885
  2044
    then have ?case
wenzelm@55885
  2045
      using c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp
wenzelm@55885
  2046
  }
wenzelm@41807
  2047
  moreover
wenzelm@55885
  2048
  {
wenzelm@55964
  2049
    assume H: "\<not> (x - d) + ?e > 0"
wenzelm@55964
  2050
    let ?v = "Neg e"
wenzelm@55964
  2051
    have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))"
wenzelm@55964
  2052
      by simp
blanchet@55584
  2053
    from 7(5)[simplified simp_thms Inum.simps \<beta>.simps set_simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
wenzelm@55964
  2054
    have nob: "\<not> (\<exists>j\<in> {1 ..d}. x = - ?e + j)"
wenzelm@55885
  2055
      by auto
wenzelm@55885
  2056
    from H p have "x + ?e > 0 \<and> x + ?e \<le> d"
wenzelm@55885
  2057
      by (simp add: c1)
wenzelm@55885
  2058
    then have "x + ?e \<ge> 1 \<and> x + ?e \<le> d"
wenzelm@55885
  2059
      by simp
wenzelm@55964
  2060
    then have "\<exists>j::int \<in> {1 .. d}. j = x + ?e"
wenzelm@55885
  2061
      by simp
wenzelm@55964
  2062
    then have "\<exists>j::int \<in> {1 .. d}. x = (- ?e + j)"
wenzelm@41807
  2063
      by (simp add: algebra_simps)
wenzelm@55885
  2064
    with nob have ?case
wenzelm@55885
  2065
      by auto
wenzelm@55885
  2066
  }
wenzelm@55885
  2067
  ultimately show ?case
wenzelm@55885
  2068
    by blast
chaieb@23274
  2069
next
wenzelm@55885
  2070
  case (8 c e)
wenzelm@55885
  2071
  then have p: "Ifm bbs (x # bs) (Ge (CN 0 c e))" and c1: "c = 1" and bn: "numbound0 e"
wenzelm@50313
  2072
    by simp_all
wenzelm@55885
  2073
  let ?e = "Inum (x # bs) e"
wenzelm@55885
  2074
  {
wenzelm@55885
  2075
    assume "(x - d) + ?e \<ge> 0"
wenzelm@55885
  2076
    then have ?case
wenzelm@55885
  2077
      using c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"]
wenzelm@55885
  2078
      by simp
wenzelm@55885
  2079
  }
wenzelm@55885
  2080
  moreover
wenzelm@55885
  2081
  {
wenzelm@55885
  2082
    assume H: "\<not> (x - d) + ?e \<ge> 0"
wenzelm@55885
  2083
    let ?v = "Sub (C -1) e"
wenzelm@55885
  2084
    have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))"
wenzelm@55885
  2085
      by simp
wenzelm@55885
  2086
    from 8(5)[simplified simp_thms Inum.simps \<beta>.simps set_simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
wenzelm@55885
  2087
    have nob: "\<not> (\<exists>j\<in> {1 ..d}. x =  - ?e - 1 + j)"
wenzelm@55885
  2088
      by auto
wenzelm@55885
  2089
    from H p have "x + ?e \<ge> 0 \<and> x + ?e < d"
wenzelm@55885
  2090
      by (simp add: c1)
wenzelm@55885
  2091
    then have "x + ?e +1 \<ge> 1 \<and> x + ?e + 1 \<le> d"
wenzelm@55885
  2092
      by simp
wenzelm@55964
  2093
    then have "\<exists>j::int \<in> {1 .. d}. j = x + ?e + 1"
wenzelm@55885
  2094
      by simp
wenzelm@55964
  2095
    then have "\<exists>j::int \<in> {1 .. d}. x= - ?e - 1 + j"
wenzelm@55885
  2096
      by (simp add: algebra_simps)
wenzelm@55885
  2097
    with nob have ?case
wenzelm@55885
  2098
      by simp
wenzelm@55885
  2099
  }
wenzelm@55885
  2100
  ultimately show ?case
wenzelm@55885
  2101
    by blast
chaieb@23274
  2102
next
wenzelm@55885
  2103
  case (3 c e)
wenzelm@55885
  2104
  then
wenzelm@55885
  2105
  have p: "Ifm bbs (x #bs) (Eq (CN 0 c e))" (is "?p x")
wenzelm@55964
  2106
    and c1: "c = 1"
wenzelm@55885
  2107
    and bn: "numbound0 e"
wenzelm@55885
  2108
    by simp_all
wenzelm@55885
  2109
  let ?e = "Inum (x # bs) e"
wenzelm@55885
  2110
  let ?v="(Sub (C -1) e)"
wenzelm@55885
  2111
  have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))"
wenzelm@55885
  2112
    by simp
wenzelm@55964
  2113
  from p have "x= - ?e"
wenzelm@55964
  2114
    by (simp add: c1) with 3(5)
wenzelm@55964
  2115
  show ?case
wenzelm@55885
  2116
    using dp
wenzelm@55885
  2117
    by simp (erule ballE[where x="1"],
wenzelm@55885
  2118
      simp_all add:algebra_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"])
chaieb@23274
  2119
next
wenzelm@55885
  2120
  case (4 c e)
wenzelm@55885
  2121
  then
wenzelm@55964
  2122
  have p: "Ifm bbs (x # bs) (NEq (CN 0 c e))" (is "?p x")
wenzelm@55885
  2123
    and c1: "c = 1"
wenzelm@55885
  2124
    and bn: "numbound0 e"
wenzelm@55885
  2125
    by simp_all
wenzelm@55885
  2126
  let ?e = "Inum (x # bs) e"
wenzelm@55885
  2127
  let ?v="Neg e"
wenzelm@55964
  2128
  have vb: "?v \<in> set (\<beta> (NEq (CN 0 c e)))"
wenzelm@55964
  2129
    by simp
wenzelm@55885
  2130
  {
wenzelm@55885
  2131
    assume "x - d + Inum (((x -d)) # bs) e \<noteq> 0"
wenzelm@55885
  2132
    then have ?case by (simp add: c1)
wenzelm@55885
  2133
  }
wenzelm@55885
  2134
  moreover
wenzelm@55885
  2135
  {
wenzelm@55964
  2136
    assume H: "x - d + Inum ((x - d) # bs) e = 0"
wenzelm@55964
  2137
    then have "x = - Inum ((x - d) # bs) e + d"
wenzelm@55885
  2138
      by simp
wenzelm@55885
  2139
    then have "x = - Inum (a # bs) e + d"
wenzelm@55885
  2140
      by (simp add: numbound0_I[OF bn,where b="x - d"and b'="a"and bs="bs"])
wenzelm@55885
  2141
     with 4(5) have ?case
wenzelm@55885
  2142
      using dp by simp
wenzelm@55885
  2143
  }
wenzelm@55885
  2144
  ultimately show ?case
wenzelm@55885
  2145
    by blast
wenzelm@50313
  2146
next
wenzelm@55885
  2147
  case (9 j c e)
wenzelm@55885
  2148
  then
wenzelm@55885
  2149
  have p: "Ifm bbs (x # bs) (Dvd j (CN 0 c e))" (is "?p x")
wenzelm@55885
  2150
    and c1: "c = 1"
wenzelm@55885
  2151
    and bn: "numbound0 e"
wenzelm@55885
  2152
    by simp_all
wenzelm@55885
  2153
  let ?e = "Inum (x # bs) e"
wenzelm@55885
  2154
  from 9 have id: "j dvd d"
wenzelm@55885
  2155
    by simp
wenzelm@55964
  2156
  from c1 have "?p x \<longleftrightarrow> j dvd (x + ?e)"
wenzelm@55885
  2157
    by simp
wenzelm@55964
  2158
  also have "\<dots> \<longleftrightarrow> j dvd x - d + ?e"
wenzelm@55885
  2159
    using zdvd_period[OF id, where x="x" and c="-1" and t="?e"]
wenzelm@55885
  2160
    by simp
wenzelm@55885
  2161
  finally show ?case
wenzelm@55885
  2162
    using numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] c1 p
wenzelm@55885
  2163
    by simp
chaieb@23274
  2164
next
wenzelm@55885
  2165
  case (10 j c e)
wenzelm@55885
  2166
  then
wenzelm@55964
  2167
  have p: "Ifm bbs (x # bs) (NDvd j (CN 0 c e))" (is "?p x")
wenzelm@55885
  2168
    and c1: "c = 1"
wenzelm@55885
  2169
    and bn: "numbound0 e"
wenzelm@55885
  2170
    by simp_all
wenzelm@55885
  2171
  let ?e = "Inum (x # bs) e"
wenzelm@55885
  2172
  from 10 have id: "j dvd d"
wenzelm@55885
  2173
    by simp
wenzelm@55964
  2174
  from c1 have "?p x \<longleftrightarrow> \<not> j dvd (x + ?e)"
wenzelm@55885
  2175
    by simp
wenzelm@55964
  2176
  also have "\<dots> \<longleftrightarrow> \<not> j dvd x - d + ?e"
wenzelm@55885
  2177
    using zdvd_period[OF id, where x="x" and c="-1" and t="?e"]
wenzelm@55885
  2178
    by simp
wenzelm@55885
  2179
  finally show ?case
wenzelm@55885
  2180
    using numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] c1 p
wenzelm@55885
  2181
    by simp
haftmann@23689
  2182
qed (auto simp add: numbound0_I[where bs="bs" and b="(x - d)" and b'="x"] gr0_conv_Suc)
chaieb@17378
  2183
wenzelm@50313
  2184
lemma \<beta>':
chaieb@23274
  2185
  assumes lp: "iszlfm p"
wenzelm@50252
  2186
  and u: "d_\<beta> p 1"
wenzelm@50252
  2187
  and d: "d_\<delta> p d"
chaieb@23274
  2188
  and dp: "d > 0"
wenzelm@55964
  2189
  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>
wenzelm@55964
  2190
    Ifm bbs (x # bs) p \<longrightarrow> Ifm bbs ((x - d) # bs) p" (is "\<forall>x. ?b \<longrightarrow> ?P x \<longrightarrow> ?P (x - d)")
wenzelm@55885
  2191
proof clarify
wenzelm@50313
  2192
  fix x
wenzelm@55885
  2193
  assume nb: "?b"
wenzelm@55885
  2194
    and px: "?P x"
wenzelm@55964
  2195
  then have nb2: "\<not> (\<exists>j::int \<in> {1 .. d}. \<exists>b \<in> Inum (a # bs) ` set (\<beta> p). x = b + j)"
chaieb@23274
  2196
    by auto
chaieb@23274
  2197
  from  \<beta>[OF lp u d dp nb2 px] show "?P (x -d )" .
chaieb@17378
  2198
qed
wenzelm@55885
  2199
wenzelm@55885
  2200
lemma cpmi_eq:
wenzelm@55885
  2201
  "0 < D \<Longrightarrow> (\<exists>z::int. \<forall>x. x < z \<longrightarrow> P x = P1 x)
wenzelm@55885
  2202
    \<Longrightarrow> \<forall>x. \<not>(\<exists>(j::int) \<in> {1..D}. \<exists>(b::int) \<in> B. P (b + j)) \<longrightarrow> P x \<longrightarrow> P (x - D)
wenzelm@55885
  2203
    \<Longrightarrow> (\<forall>(x::int). \<forall>(k::int). P1 x = (P1 (x - k * D)))
wenzelm@55885
  2204
    \<Longrightarrow> (\<exists>(x::int). P x) = ((\<exists>(j::int) \<in> {1..D}. P1 j) \<or> (\<exists>(j::int) \<in> {1..D}. \<exists>(b::int) \<in> B. P (b + j)))"
wenzelm@55885
  2205
  apply(rule iffI)
wenzelm@55885
  2206
  prefer 2
wenzelm@55981
  2207
  apply (drule minusinfinity)
wenzelm@55885
  2208
  apply assumption+
wenzelm@55981
  2209
  apply fastforce
wenzelm@55885
  2210
  apply clarsimp
wenzelm@55981
  2211
  apply (subgoal_tac "\<And>k. 0 \<le> k \<Longrightarrow> \<forall>x. P x \<longrightarrow> P (x - k * D)")
wenzelm@55981
  2212
  apply (frule_tac x = x and z=z in decr_lemma)
wenzelm@55981
  2213
  apply (subgoal_tac "P1 (x - (\<bar>x - z\<bar> + 1) * D)")
wenzelm@55885
  2214
  prefer 2
wenzelm@55981
  2215
  apply (subgoal_tac "0 \<le> \<bar>x - z\<bar> + 1")
wenzelm@55885
  2216
  prefer 2 apply arith
wenzelm@55885
  2217
   apply fastforce
wenzelm@55981
  2218
  apply (drule (1)  periodic_finite_ex)
wenzelm@55885
  2219
  apply blast
wenzelm@55981
  2220
  apply (blast dest: decr_mult_lemma)
wenzelm@55885
  2221
  done
chaieb@17378
  2222
chaieb@23274
  2223
theorem cp_thm:
chaieb@23274
  2224
  assumes lp: "iszlfm p"
wenzelm@55885
  2225
    and u: "d_\<beta> p 1"
wenzelm@55885
  2226
    and d: "d_\<delta> p d"
wenzelm@55885
  2227
    and dp: "d > 0"
wenzelm@55964
  2228
  shows "(\<exists>(x::int). Ifm bbs (x # bs) p) \<longleftrightarrow>
wenzelm@55964
  2229
    (\<exists>j \<in> {1.. d}. Ifm bbs (j # bs) (minusinf p) \<or>
wenzelm@55964
  2230
      (\<exists>b \<in> set (\<beta> p). Ifm bbs ((Inum (i # bs) b + j) # bs) p))"
wenzelm@50313
  2231
  (is "(\<exists>(x::int). ?P (x)) = (\<exists>j\<in> ?D. ?M j \<or> (\<exists>b\<in> ?B. ?P (?I b + j)))")
wenzelm@55885
  2232
proof -
wenzelm@50313
  2233
  from minusinf_inf[OF lp u]
wenzelm@55964
  2234
  have th: "\<exists>z::int. \<forall>x<z. ?P (x) = ?M x"
wenzelm@55885
  2235
    by blast
wenzelm@55964
  2236
  let ?B' = "{?I b | b. b \<in> ?B}"
wenzelm@55964
  2237
  have BB': "(\<exists>j\<in>?D. \<exists>b \<in> ?B. ?P (?I b + j)) \<longleftrightarrow> (\<exists>j \<in> ?D. \<exists>b \<in> ?B'. ?P (b + j))"
wenzelm@55885
  2238
    by auto
wenzelm@55964
  2239
  then have th2: "\<forall>x. \<not> (\<exists>j \<in> ?D. \<exists>b \<in> ?B'. ?P (b + j)) \<longrightarrow> ?P x \<longrightarrow> ?P (x - d)"
chaieb@23274
  2240
    using \<beta>'[OF lp u d dp, where a="i" and bbs = "bbs"] by blast
chaieb@23274
  2241
  from minusinf_repeats[OF d lp]
wenzelm@55885
  2242
  have th3: "\<forall>x k. ?M x = ?M (x-k*d)"
wenzelm@55885
  2243
    by simp
wenzelm@55885
  2244
  from cpmi_eq[OF dp th th2 th3] BB' show ?thesis
wenzelm@55885
  2245
    by blast
chaieb@17378
  2246
qed
chaieb@17378
  2247
wenzelm@55885
  2248
(* Implement the right hand sides of Cooper's theorem and Ferrante and Rackoff. *)
wenzelm@50313
  2249
lemma mirror_ex:
chaieb@23274
  2250
  assumes lp: "iszlfm p"
wenzelm@50313
  2251
  shows "(\<exists>x. Ifm bbs (x#bs) (mirror p)) = (\<exists>x. Ifm bbs (x#bs) p)"
wenzelm@50313
  2252
  (is "(\<exists>x. ?I x ?mp) = (\<exists>x. ?I x p)")
wenzelm@55964
  2253
proof auto
wenzelm@55964
  2254
  fix x
wenzelm@55964
  2255
  assume "?I x ?mp"
wenzelm@55964
  2256
  then have "?I (- x) p"
wenzelm@55964
  2257
    using mirror[OF lp] by blast
wenzelm@55964
  2258
  then show "\<exists>x. ?I x p"
wenzelm@55964
  2259
    by blast
chaieb@23274
  2260
next
wenzelm@55964
  2261
  fix x
wenzelm@55964
  2262
  assume "?I x p"
wenzelm@55964
  2263
  then have "?I (- x) ?mp"
chaieb@23274
  2264
    using mirror[OF lp, where x="- x", symmetric] by auto
wenzelm@55964
  2265
  then show "\<exists>x. ?I x ?mp"
wenzelm@55964
  2266
    by blast
chaieb@23274
  2267
qed
nipkow@24349
  2268
wenzelm@50313
  2269
lemma cp_thm':
chaieb@23274
  2270
  assumes lp: "iszlfm p"
wenzelm@55964
  2271
    and up: "d_\<beta> p 1"
wenzelm@55964
  2272
    and dd: "d_\<delta> p d"
wenzelm@55964
  2273
    and dp: "d > 0"
wenzelm@55964
  2274
  shows "(\<exists>x. Ifm bbs (x # bs) p) \<longleftrightarrow>
wenzelm@55964
  2275
    ((\<exists>j\<in> {1 .. d}. Ifm bbs (j#bs) (minusinf p)) \<or>
wenzelm@55964
  2276
      (\<exists>j\<in> {1.. d}. \<exists>b\<in> (Inum (i#bs)) ` set (\<beta> p). Ifm bbs ((b + j) # bs) p))"
chaieb@23274
  2277
  using cp_thm[OF lp up dd dp,where i="i"] by auto
chaieb@17378
  2278
wenzelm@50313
  2279
definition unit :: "fm \<Rightarrow> fm \<times> num list \<times> int"
wenzelm@50313
  2280
where
wenzelm@55964
  2281
  "unit p =
wenzelm@55964
  2282
     (let
wenzelm@55964
  2283
        p' = zlfm p;
wenzelm@55964
  2284
        l = \<zeta> p';
wenzelm@55964
  2285
        q = And (Dvd l (CN 0 1 (C 0))) (a_\<beta> p' l);
wenzelm@55964
  2286
        d = \<delta> q;
wenzelm@55964
  2287
        B = remdups (map simpnum (\<beta> q));
wenzelm@55964
  2288
        a = remdups (map simpnum (\<alpha> q))
wenzelm@55964
  2289
      in if length B \<le> length a then (q, B, d) else (mirror q, a, d))"
chaieb@17378
  2290
wenzelm@50313
  2291
lemma unit:
wenzelm@50313
  2292
  assumes qf: "qfree p"
wenzelm@55964
  2293
  shows "\<And>q B d. unit p = (q, B, d) \<Longrightarrow>
wenzelm@55964
  2294
    ((\<exists>x. Ifm bbs (x # bs) p) \<longleftrightarrow> (\<exists>x. Ifm bbs (x # bs) q)) \<and>
wenzelm@55964
  2295
    (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>
wenzelm@55964
  2296
    iszlfm q \<and> (\<forall>b\<in> set B. numbound0 b)"
wenzelm@50313
  2297
proof -
wenzelm@50313
  2298
  fix q B d
chaieb@23274
  2299
  assume qBd: "unit p = (q,B,d)"
wenzelm@55981
  2300
  let ?thes = "((\<exists>x. Ifm bbs (x#bs) p) \<longleftrightarrow> (\<exists>x. Ifm bbs (x#bs) q)) \<and>
chaieb@23274
  2301
    Inum (i#bs) ` set B = Inum (i#bs) ` set (\<beta> q) \<and>
wenzelm@50313
  2302
    d_\<beta> q 1 \<and> d_\<delta> q d \<and> 0 < d \<and> iszlfm q \<and> (\<forall>b\<in> set B. numbound0 b)"
wenzelm@50313
  2303
  let ?I = "\<lambda>x p. Ifm bbs (x#bs) p"
chaieb@23274
  2304
  let ?p' = "zlfm p"
chaieb@23274
  2305
  let ?l = "\<zeta> ?p'"
wenzelm@50252
  2306
  let ?q = "And (Dvd ?l (CN 0 1 (C 0))) (a_\<beta> ?p' ?l)"
chaieb@23274
  2307
  let ?d = "\<delta> ?q"
chaieb@23274
  2308
  let ?B = "set (\<beta> ?q)"
chaieb@23274
  2309
  let ?B'= "remdups (map simpnum (\<beta> ?q))"
chaieb@23274
  2310
  let ?A = "set (\<alpha> ?q)"
chaieb@23274
  2311
  let ?A'= "remdups (map simpnum (\<alpha> ?q))"
wenzelm@50313
  2312
  from conjunct1[OF zlfm_I[OF qf, where bs="bs"]]
wenzelm@50313
  2313
  have pp': "\<forall>i. ?I i ?p' = ?I i p" by auto
chaieb@23274
  2314
  from conjunct2[OF zlfm_I[OF qf, where bs="bs" and i="i"]]
wenzelm@50313
  2315
  have lp': "iszlfm ?p'" .
wenzelm@50252
  2316
  from lp' \<zeta>[where p="?p'"] have lp: "?l >0" and dl: "d_\<beta> ?p' ?l" by auto
wenzelm@50252
  2317
  from a_\<beta>_ex[where p="?p'" and l="?l" and bs="bs", OF lp' dl lp] pp'
wenzelm@50313
  2318
  have pq_ex:"(\<exists>(x::int). ?I x p) = (\<exists>x. ?I x ?q)" by simp
wenzelm@50252
  2319
  from lp' lp a_\<beta>[OF lp' dl lp] have lq:"iszlfm ?q" and uq: "d_\<beta> ?q 1"  by auto
wenzelm@50252
  2320
  from \<delta>[OF lq] have dp:"?d >0" and dd: "d_\<delta> ?q ?d" by blast+
wenzelm@50313
  2321
  let ?N = "\<lambda>t. Inum (i#bs) t"
wenzelm@55981
  2322
  have "?N ` set ?B' = ((?N \<circ> simpnum) ` ?B)"
wenzelm@55981
  2323
    by auto
wenzelm@55981
  2324
  also have "\<dots> = ?N ` ?B"
wenzelm@55981
  2325
    using simpnum_ci[where bs="i#bs"] by auto
chaieb@23274
  2326
  finally have BB': "?N ` set ?B' = ?N ` ?B" .
wenzelm@55981
  2327
  have "?N ` set ?A' = ((?N \<circ> simpnum) ` ?A)"
wenzelm@55981
  2328
    by auto
wenzelm@55981
  2329
  also have "\<dots> = ?N ` ?A"
wenzelm@55981
  2330
    using simpnum_ci[where bs="i#bs"] by auto
chaieb@23274
  2331
  finally have AA': "?N ` set ?A' = ?N ` ?A" .
wenzelm@50313
  2332
  from \<beta>_numbound0[OF lq] have B_nb:"\<forall>b\<in> set ?B'. numbound0 b"
chaieb@23274
  2333
    by (simp add: simpnum_numbound0)
wenzelm@50313
  2334
  from \<alpha>_l[OF lq] have A_nb: "\<forall>b\<in> set ?A'. numbound0 b"
chaieb@23274
  2335
    by (simp add: simpnum_numbound0)
wenzelm@55981
  2336
  {
wenzelm@55981
  2337
    assume "length ?B' \<le> length ?A'"
wenzelm@55981
  2338
    then have q: "q = ?q" and "B = ?B'" and d: "d = ?d"
chaieb@23274
  2339
      using qBd by (auto simp add: Let_def unit_def)
wenzelm@55981
  2340
    with BB' B_nb
wenzelm@55981
  2341
    have b: "?N ` (set B) = ?N ` set (\<beta> q)" and bn: "\<forall>b\<in> set B. numbound0 b"
wenzelm@55981
  2342
      by simp_all
wenzelm@55981
  2343
    with pq_ex dp uq dd lq q d have ?thes
wenzelm@55981
  2344
      by simp
wenzelm@55981
  2345
  }
wenzelm@50313
  2346
  moreover
wenzelm@55981
  2347
  {
wenzelm@55981
  2348
    assume "\<not> (length ?B' \<le> length ?A')"
wenzelm@55885
  2349
    then have q:"q=mirror ?q" and "B = ?A'" and d:"d = ?d"
chaieb@23274
  2350
      using qBd by (auto simp add: Let_def unit_def)
wenzelm@50313
  2351
    with AA' mirror_\<alpha>_\<beta>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<beta> q)"
wenzelm@50313
  2352
      and bn: "\<forall>b\<in> set B. numbound0 b" by simp_all
wenzelm@50313
  2353
    from mirror_ex[OF lq] pq_ex q
wenzelm@55981
  2354
    have pqm_eq:"(\<exists>(x::int). ?I x p) = (\<exists>(x::int). ?I x q)"
wenzelm@55981
  2355
      by simp
chaieb@23274
  2356
    from lq uq q mirror_l[where p="?q"]
wenzelm@55981
  2357
    have lq': "iszlfm q" and uq: "d_\<beta> q 1"
wenzelm@55981
  2358
      by auto
wenzelm@55981
  2359
    from \<delta>[OF lq'] mirror_\<delta>[OF lq] q d have dq: "d_\<delta> q d"
wenzelm@55981
  2360
      by auto
wenzelm@55981
  2361
    from pqm_eq b bn uq lq' dp dq q dp d have ?thes
wenzelm@55981
  2362
      by simp
chaieb@23274
  2363
  }
chaieb@23274
  2364
  ultimately show ?thes by blast
chaieb@23274
  2365
qed
wenzelm@50313
  2366
wenzelm@50313
  2367
wenzelm@50313
  2368
text {* Cooper's Algorithm *}
chaieb@17378
  2369
wenzelm@55981
  2370
definition cooper :: "fm \<Rightarrow> fm"
wenzelm@55981
  2371
where
wenzelm@50313
  2372
  "cooper p =
wenzelm@50313
  2373
    (let
wenzelm@50313
  2374
      (q, B, d) = unit p;
wenzelm@50313
  2375
      js = [1..d];
wenzelm@50313
  2376
      mq = simpfm (minusinf q);
wenzelm@50313
  2377
      md = evaldjf (\<lambda>j. simpfm (subst0 (C j) mq)) js
wenzelm@50313
  2378
     in
wenzelm@50313
  2379
      if md = T then T
wenzelm@50313
  2380
      else
wenzelm@50313
  2381
        (let
wenzelm@50313
  2382
          qd = evaldjf (\<lambda>(b, j). simpfm (subst0 (Add b (C j)) q)) [(b, j). b \<leftarrow> B, j \<leftarrow> js]
wenzelm@50313
  2383
         in decr (disj md qd)))"
wenzelm@50313
  2384
wenzelm@50313
  2385
lemma cooper:
wenzelm@50313
  2386
  assumes qf: "qfree p"
wenzelm@50313
  2387
  shows "((\<exists>x. Ifm bbs (x#bs) p) = (Ifm bbs bs (cooper p))) \<and> qfree (cooper p)"
chaieb@23274
  2388
  (is "(?lhs = ?rhs) \<and> _")
wenzelm@50313
  2389
proof -
wenzelm@50313
  2390
  let ?I = "\<lambda>x p. Ifm bbs (x#bs) p"
chaieb@23274
  2391
  let ?q = "fst (unit p)"
chaieb@23274
  2392
  let ?B = "fst (snd(unit p))"
chaieb@23274
  2393
  let ?d = "snd (snd (unit p))"
krauss@41836
  2394
  let ?js = "[1..?d]"
chaieb@23274
  2395
  let ?mq = "minusinf ?q"
chaieb@23274
  2396
  let ?smq = "simpfm ?mq"
wenzelm@50313
  2397
  let ?md = "evaldjf (\<lambda>j. simpfm (subst0 (C j) ?smq)) ?js"
wenzelm@26934
  2398
  fix i
wenzelm@50313
  2399
  let ?N = "\<lambda>t. Inum (i#bs) t"
nipkow@24336
  2400
  let ?Bjs = "[(b,j). b\<leftarrow>?B,j\<leftarrow>?js]"
wenzelm@50313
  2401
  let ?qd = "evaldjf (\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs"
chaieb@23274
  2402
  have qbf:"unit p = (?q,?B,?d)" by simp
wenzelm@55981
  2403
  from unit[OF qf qbf]
wenzelm@55981
  2404
  have pq_ex: "(\<exists>(x::int). ?I x p) \<longleftrightarrow> (\<exists>(x::int). ?I x ?q)"
wenzelm@55981
  2405
    and B: "?N ` set ?B = ?N ` set (\<beta> ?q)"
wenzelm@55981
  2406
    and uq: "d_\<beta> ?q 1"
wenzelm@55981
  2407
    and dd: "d_\<delta> ?q ?d"
wenzelm@55981
  2408
    and dp: "?d > 0"
wenzelm@55981
  2409
    and lq: "iszlfm ?q"
wenzelm@55981
  2410
    and Bn: "\<forall>b\<in> set ?B. numbound0 b"
wenzelm@55981
  2411
    by auto
chaieb@23274
  2412
  from zlin_qfree[OF lq] have qfq: "qfree ?q" .
wenzelm@55921
  2413
  from simpfm_qf[OF minusinf_qfree[OF qfq]] have qfmq: "qfree ?smq" .
wenzelm@55981
  2414
  have jsnb: "\<forall>j \<in> set ?js. numbound0 (C j)"
wenzelm@55981
  2415
    by simp
wenzelm@55885
  2416
  then have "\<forall>j\<in> set ?js. bound0 (subst0 (C j) ?smq)"
chaieb@23274
  2417
    by (auto simp only: subst0_bound0[OF qfmq])
wenzelm@55885
  2418
  then have th: "\<forall>j\<in> set ?js. bound0 (simpfm (subst0 (C j) ?smq))"
chaieb@23274
  2419
    by (auto simp add: simpfm_bound0)
wenzelm@55981
  2420
  from evaldjf_bound0[OF th] have mdb: "bound0 ?md"
wenzelm@55981
  2421
    by simp
wenzelm@50313
  2422
  from Bn jsnb have "\<forall>(b,j) \<in> set ?Bjs. numbound0 (Add b (C j))"
haftmann@23689
  2423
    by simp
wenzelm@55885
  2424
  then have "\<forall>(b,j) \<in> set ?Bjs. bound0 (subst0 (Add b (C j)) ?q)"
chaieb@23274
  2425
    using subst0_bound0[OF qfq] by blast
wenzelm@55885
  2426
  then have "\<forall>(b,j) \<in> set ?Bjs. bound0 (simpfm (subst0 (Add b (C j)) ?q))"
wenzelm@55981
  2427
    using simpfm_bound0 by blast
wenzelm@55885
  2428
  then have th': "\<forall>x \<in> set ?Bjs. bound0 ((\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)) x)"
wenzelm@50313
  2429
    by auto
wenzelm@55981
  2430
  from evaldjf_bound0 [OF th'] have qdb: "bound0 ?qd"
wenzelm@55981
  2431
    by simp
wenzelm@55981
  2432
  from mdb qdb have mdqdb: "bound0 (disj ?md ?qd)"
wenzelm@55981
  2433
    unfolding disj_def by (cases "?md = T \<or> ?qd = T") simp_all
chaieb@23274
  2434
  from trans [OF pq_ex cp_thm'[OF lq uq dd dp,where i="i"]] B
wenzelm@55981
  2435
  have "?lhs \<longleftrightarrow> (\<exists>j \<in> {1.. ?d}. ?I j ?mq \<or> (\<exists>b \<in> ?N ` set ?B. Ifm bbs ((b + j) # bs) ?q))"
wenzelm@55921
  2436
    by auto
wenzelm@55981
  2437
  also have "\<dots> \<longleftrightarrow> (\<exists>j \<in> {1.. ?d}. ?I j ?mq \<or> (\<exists>b \<in> set ?B. Ifm bbs ((?N b + j) # bs) ?q))"
wenzelm@55921
  2438
    by simp
wenzelm@55981
  2439
  also have "\<dots> \<longleftrightarrow> (\<exists>j \<in> {1.. ?d}. ?I j ?mq ) \<or>
wenzelm@55981
  2440
      (\<exists>j\<in> {1.. ?d}. \<exists>b \<in> set ?B. Ifm bbs ((?N (Add b (C j))) # bs) ?q)"
wenzelm@50313
  2441
    by (simp only: Inum.simps) blast
wenzelm@55981
  2442
  also have "\<dots> \<longleftrightarrow> (\<exists>j \<in> {1.. ?d}. ?I j ?smq) \<or>
wenzelm@55981
  2443
      (\<exists>j \<in> {1.. ?d}. \<exists>b \<in> set ?B. Ifm bbs ((?N (Add b (C j))) # bs) ?q)"
wenzelm@50313
  2444
    by (simp add: simpfm)
wenzelm@55981
  2445
  also have "\<dots> \<longleftrightarrow> (\<exists>j\<in> set ?js. (\<lambda>j. ?I i (simpfm (subst0 (C j) ?smq))) j) \<or>
wenzelm@55981
  2446
      (\<exists>j\<in> set ?js. \<exists>b\<in> set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q)"
krauss@41836
  2447
    by (simp only: simpfm subst0_I[OF qfmq] set_upto) auto
wenzelm@55981
  2448
  also have "\<dots> \<longleftrightarrow> ?I i (evaldjf (\<lambda>j. simpfm (subst0 (C j) ?smq)) ?js) \<or>
wenzelm@55981
  2449
      (\<exists>j\<in> set ?js. \<exists>b\<in> set ?B. ?I i (subst0 (Add b (C j)) ?q))"
wenzelm@50313
  2450
    by (simp only: evaldjf_ex subst0_I[OF qfq])
wenzelm@55981
  2451
  also have "\<dots> \<longleftrightarrow> ?I i ?md \<or>
wenzelm@55981
  2452
      (\<exists>(b,j) \<in> set ?Bjs. (\<lambda>(b,j). ?I i (simpfm (subst0 (Add b (C j)) ?q))) (b,j))"
wenzelm@50313
  2453
    by (simp only: simpfm set_concat set_map concat_map_singleton UN_simps) blast
wenzelm@55981
  2454
  also have "\<dots> \<longleftrightarrow> ?I i ?md \<or> ?I i (evaldjf (\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs)"
wenzelm@50313
  2455
    by (simp only: evaldjf_ex[where bs="i#bs" and f="\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)" and ps="?Bjs"])
wenzelm@50313
  2456
      (auto simp add: split_def)
wenzelm@55981
  2457
  finally have mdqd: "?lhs \<longleftrightarrow> ?I i ?md \<or> ?I i ?qd"
wenzelm@55921
  2458
    by simp
wenzelm@55981
  2459
  also have "\<dots> \<longleftrightarrow> ?I i (disj ?md ?qd)"
wenzelm@55921
  2460
    by (simp add: disj)
wenzelm@55981
  2461
  also have "\<dots> \<longleftrightarrow> Ifm bbs bs (decr (disj ?md ?qd))"
wenzelm@55921
  2462
    by (simp only: decr [OF mdqdb])
wenzelm@55981
  2463
  finally have mdqd2: "?lhs \<longleftrightarrow> Ifm bbs bs (decr (disj ?md ?qd))" .
wenzelm@55921
  2464
  {
wenzelm@55921
  2465
    assume mdT: "?md = T"
wenzelm@55921
  2466
    then have cT: "cooper p = T"
chaieb@23274
  2467
      by (simp only: cooper_def unit_def split_def Let_def if_True) simp
wenzelm@55921
  2468
    from mdT have lhs: "?lhs"
wenzelm@55921
  2469
      using mdqd by simp
wenzelm@55921
  2470
    from mdT have "?rhs"
wenzelm@55921
  2471
      by (simp add: cooper_def unit_def split_def)
wenzelm@55981
  2472
    with lhs cT have ?thesis
wenzelm@55981
  2473
      by simp
wenzelm@55921
  2474
  }
chaieb@17378
  2475
  moreover
wenzelm@55921
  2476
  {
wenzelm@55921
  2477
    assume mdT: "?md \<noteq> T"
wenzelm@55921
  2478
    then have "cooper p = decr (disj ?md ?qd)"
wenzelm@50313
  2479
      by (simp only: cooper_def unit_def split_def Let_def if_False)
wenzelm@55921
  2480
    with mdqd2 decr_qf[OF mdqdb] have ?thesis
wenzelm@55921
  2481
      by simp
wenzelm@55921
  2482
  }
chaieb@17378
  2483
  ultimately show ?thesis by blast
chaieb@17378
  2484
qed
chaieb@17378
  2485
wenzelm@55921
  2486
definition pa :: "fm \<Rightarrow> fm"
wenzelm@55921
  2487
  where "pa p = qelim (prep p) cooper"
chaieb@17378
  2488
wenzelm@55921
  2489
theorem mirqe: "Ifm bbs bs (pa p) = Ifm bbs bs p \<and> qfree (pa p)"
chaieb@23274
  2490
  using qelim_ci cooper prep by (auto simp add: pa_def)
chaieb@17378
  2491
wenzelm@50313
  2492
definition cooper_test :: "unit \<Rightarrow> fm"
wenzelm@50313
  2493
  where
wenzelm@50313
  2494
    "cooper_test u =
wenzelm@50313
  2495
      pa (E (A (Imp (Ge (Sub (Bound 0) (Bound 1)))
wenzelm@50313
  2496
        (E (E (Eq (Sub (Add (Mul 3 (Bound 1)) (Mul 5 (Bound 0))) (Bound 2))))))))"
chaieb@17378
  2497
wenzelm@51272
  2498
ML_val {* @{code cooper_test} () *}
haftmann@27456
  2499
haftmann@51143
  2500
(*code_reflect Cooper_Procedure
haftmann@55685
  2501
  functions pa T Bound nat_of_integer integer_of_nat int_of_integer integer_of_int
haftmann@51143
  2502
  file "~~/src/HOL/Tools/Qelim/cooper_procedure.ML"*)
haftmann@27456
  2503
wenzelm@28290
  2504
oracle linzqe_oracle = {*
haftmann@27456
  2505
let
haftmann@27456
  2506
wenzelm@55814
  2507
fun num_of_term vs (t as Free (xn, xT)) =
wenzelm@55814
  2508
      (case AList.lookup (op =) vs t of
wenzelm@55814
  2509
        NONE => error "Variable not found in the list!"
haftmann@51143
  2510
      | SOME n => @{code Bound} (@{code nat_of_integer} n))
haftmann@51143
  2511
  | num_of_term vs @{term "0::int"} = @{code C} (@{code int_of_integer} 0)
haftmann@51143
  2512
  | num_of_term vs @{term "1::int"} = @{code C} (@{code int_of_integer} 1)
haftmann@54489
  2513
  | num_of_term vs @{term "- 1::int"} = @{code C} (@{code int_of_integer} (~ 1))
haftmann@51143
  2514
  | num_of_term vs (@{term "numeral :: _ \<Rightarrow> int"} $ t) =
haftmann@51143
  2515
      @{code C} (@{code int_of_integer} (HOLogic.dest_num t))
haftmann@54489
  2516
  | num_of_term vs (@{term "- numeral :: _ \<Rightarrow> int"} $ t) =
haftmann@51143
  2517
      @{code C} (@{code int_of_integer} (~(HOLogic.dest_num t)))
haftmann@51143
  2518
  | num_of_term vs (Bound i) = @{code Bound} (@{code nat_of_integer} i)
haftmann@27456
  2519
  | num_of_term vs (@{term "uminus :: int \<Rightarrow> int"} $ t') = @{code Neg} (num_of_term vs t')
haftmann@27456
  2520
  | num_of_term vs (@{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) =
haftmann@27456
  2521
      @{code Add} (num_of_term vs t1, num_of_term vs t2)
haftmann@27456
  2522
  | num_of_term vs (@{term "op - :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) =
haftmann@27456
  2523
      @{code Sub} (num_of_term vs t1, num_of_term vs t2)
haftmann@27456
  2524
  | num_of_term vs (@{term "op * :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) =
wenzelm@55814
  2525
      (case try HOLogic.dest_number t1 of
wenzelm@55814
  2526
        SOME (_, i) => @{code Mul} (@{code int_of_integer} i, num_of_term vs t2)
wenzelm@55814
  2527
      | NONE =>
wenzelm@55814
  2528
          (case try HOLogic.dest_number t2 of
wenzelm@55814
  2529
            SOME (_, i) => @{code Mul} (@{code int_of_integer} i, num_of_term vs t1)
wenzelm@55814
  2530
          | NONE => error "num_of_term: unsupported multiplication"))
wenzelm@28264
  2531
  | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term @{context} t);
haftmann@27456
  2532
haftmann@27456
  2533
fun fm_of_term ps vs @{term True} = @{code T}
haftmann@27456
  2534
  | fm_of_term ps vs @{term False} = @{code F}
haftmann@27456
  2535
  | fm_of_term ps vs (@{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} $ t1 $ t2) =
haftmann@27456
  2536
      @{code Lt} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
haftmann@27456
  2537
  | fm_of_term ps vs (@{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"} $ t1 $ t2) =
haftmann@27456
  2538
      @{code Le} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
haftmann@27456
  2539
  | fm_of_term ps vs (@{term "op = :: int \<Rightarrow> int \<Rightarrow> bool"} $ t1 $ t2) =
wenzelm@50313
  2540
      @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
haftmann@27456
  2541
  | fm_of_term ps vs (@{term "op dvd :: int \<Rightarrow> int \<Rightarrow> bool"} $ t1 $ t2) =
wenzelm@55814
  2542
      (case try HOLogic.dest_number t1 of
wenzelm@55814
  2543
        SOME (_, i) => @{code Dvd} (@{code int_of_integer} i, num_of_term vs t2)
wenzelm@55814
  2544
      | NONE => error "num_of_term: unsupported dvd")
haftmann@27456
  2545
  | fm_of_term ps vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
haftmann@27456
  2546
      @{code Iff} (fm_of_term ps vs t1, fm_of_term ps vs t2)
haftmann@38795
  2547
  | fm_of_term ps vs (@{term HOL.conj} $ t1 $ t2) =
haftmann@27456
  2548
      @{code And} (fm_of_term ps vs t1, fm_of_term ps vs t2)
haftmann@38795
  2549
  | fm_of_term ps vs (@{term HOL.disj} $ t1 $ t2) =
haftmann@27456
  2550
      @{code Or} (fm_of_term ps vs t1, fm_of_term ps vs t2)
haftmann@38786
  2551
  | fm_of_term ps vs (@{term HOL.implies} $ t1 $ t2) =
haftmann@27456
  2552
      @{code Imp} (fm_of_term ps vs t1, fm_of_term ps vs t2)
haftmann@27456
  2553
  | fm_of_term ps vs (@{term "Not"} $ t') =
haftmann@27456
  2554
      @{code NOT} (fm_of_term ps vs t')
haftmann@38558
  2555
  | fm_of_term ps vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) =
haftmann@27456
  2556
      let
wenzelm@42284
  2557
        val (xn', p') = Syntax_Trans.variant_abs (xn, xT, p);  (* FIXME !? *)
haftmann@27456
  2558
        val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
haftmann@27456
  2559
      in @{code E} (fm_of_term ps vs' p) end
haftmann@38558
  2560
  | fm_of_term ps vs (Const (@{const_name All}, _) $ Abs (xn, xT, p)) =
haftmann@27456
  2561
      let
wenzelm@42284
  2562
        val (xn', p') = Syntax_Trans.variant_abs (xn, xT, p);  (* FIXME !? *)
haftmann@27456
  2563
        val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
haftmann@27456
  2564
      in @{code A} (fm_of_term ps vs' p) end
wenzelm@28264
  2565
  | fm_of_term ps vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t);
haftmann@23515
  2566
haftmann@51143
  2567
fun term_of_num vs (@{code C} i) = HOLogic.mk_number HOLogic.intT (@{code integer_of_int} i)
haftmann@51143
  2568
  | term_of_num vs (@{code Bound} n) =
haftmann@51143
  2569
      let
haftmann@51143
  2570
        val q = @{code integer_of_nat} n
haftmann@51143
  2571
      in fst (the (find_first (fn (_, m) => q = m) vs)) end
haftmann@27456
  2572
  | term_of_num vs (@{code Neg} t') = @{term "uminus :: int \<Rightarrow> int"} $ term_of_num vs t'
haftmann@27456
  2573
  | term_of_num vs (@{code Add} (t1, t2)) = @{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} $
haftmann@27456
  2574
      term_of_num vs t1 $ term_of_num vs t2