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