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