src/HOL/Decision_Procs/Cooper.thy
author hoelzl
Wed, 11 Mar 2009 10:58:18 +0100
changeset 30439 57c68b3af2ea
parent 30042 31039ee583fa
child 31715 2eb55a82acd9
permissions -rw-r--r--
Updated paths in Decision_Procs comments and NEWS
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30439
57c68b3af2ea Updated paths in Decision_Procs comments and NEWS
hoelzl
parents: 30042
diff changeset
     1
(*  Title:      HOL/Decision_Procs/Cooper.thy
27456
52c7c42e7e27 code antiquotation roaring ahead
haftmann
parents: 26934
diff changeset
     2
    Author:     Amine Chaieb
52c7c42e7e27 code antiquotation roaring ahead
haftmann
parents: 26934
diff changeset
     3
*)
52c7c42e7e27 code antiquotation roaring ahead
haftmann
parents: 26934
diff changeset
     4
29788
1b80ebe713a4 established session HOL-Reflection
haftmann
parents: 29700
diff changeset
     5
theory Cooper
1b80ebe713a4 established session HOL-Reflection
haftmann
parents: 29700
diff changeset
     6
imports Complex_Main Efficient_Nat
1b80ebe713a4 established session HOL-Reflection
haftmann
parents: 29700
diff changeset
     7
uses ("cooper_tac.ML")
23477
f4b83f03cac9 tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents: 23315
diff changeset
     8
begin
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
     9
29788
1b80ebe713a4 established session HOL-Reflection
haftmann
parents: 29700
diff changeset
    10
function iupt :: "int \<Rightarrow> int \<Rightarrow> int list" where
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
    11
  "iupt i j = (if j < i then [] else i # iupt (i+1) j)"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
    12
by pat_completeness auto
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
    13
termination by (relation "measure (\<lambda> (i, j). nat (j-i+1))") auto
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    14
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
    15
lemma iupt_set: "set (iupt i j) = {i..j}"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
    16
  by (induct rule: iupt.induct) (simp add: simp_from_to)
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
    17
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
    18
(* Periodicity of dvd *)
23315
df3a7e9ebadb tuned Proof
chaieb
parents: 23274
diff changeset
    19
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    20
  (*********************************************************************************)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    21
  (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    22
  (*********************************************************************************)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    23
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
    24
datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num 
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    25
  | Mul int num
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    26
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    27
  (* A size for num to make inductive proofs simpler*)
27456
52c7c42e7e27 code antiquotation roaring ahead
haftmann
parents: 26934
diff changeset
    28
primrec num_size :: "num \<Rightarrow> nat" where
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    29
  "num_size (C c) = 1"
27456
52c7c42e7e27 code antiquotation roaring ahead
haftmann
parents: 26934
diff changeset
    30
| "num_size (Bound n) = 1"
52c7c42e7e27 code antiquotation roaring ahead
haftmann
parents: 26934
diff changeset
    31
| "num_size (Neg a) = 1 + num_size a"
52c7c42e7e27 code antiquotation roaring ahead
haftmann
parents: 26934
diff changeset
    32
| "num_size (Add a b) = 1 + num_size a + num_size b"
52c7c42e7e27 code antiquotation roaring ahead
haftmann
parents: 26934
diff changeset
    33
| "num_size (Sub a b) = 3 + num_size a + num_size b"
52c7c42e7e27 code antiquotation roaring ahead
haftmann
parents: 26934
diff changeset
    34
| "num_size (CN n c a) = 4 + num_size a"
52c7c42e7e27 code antiquotation roaring ahead
haftmann
parents: 26934
diff changeset
    35
| "num_size (Mul c a) = 1 + num_size a"
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
    36
27456
52c7c42e7e27 code antiquotation roaring ahead
haftmann
parents: 26934
diff changeset
    37
primrec Inum :: "int list \<Rightarrow> num \<Rightarrow> int" where
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    38
  "Inum bs (C c) = c"
27456
52c7c42e7e27 code antiquotation roaring ahead
haftmann
parents: 26934
diff changeset
    39
| "Inum bs (Bound n) = bs!n"
52c7c42e7e27 code antiquotation roaring ahead
haftmann
parents: 26934
diff changeset
    40
| "Inum bs (CN n c a) = c * (bs!n) + (Inum bs a)"
52c7c42e7e27 code antiquotation roaring ahead
haftmann
parents: 26934
diff changeset
    41
| "Inum bs (Neg a) = -(Inum bs a)"
52c7c42e7e27 code antiquotation roaring ahead
haftmann
parents: 26934
diff changeset
    42
| "Inum bs (Add a b) = Inum bs a + Inum bs b"
52c7c42e7e27 code antiquotation roaring ahead
haftmann
parents: 26934
diff changeset
    43
| "Inum bs (Sub a b) = Inum bs a - Inum bs b"
52c7c42e7e27 code antiquotation roaring ahead
haftmann
parents: 26934
diff changeset
    44
| "Inum bs (Mul c a) = c* Inum bs a"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    45
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    46
datatype fm  = 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    47
  T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num|
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    48
  NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    49
  | Closed nat | NClosed nat
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    50
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    51
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    52
  (* A size for fm *)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    53
consts fmsize :: "fm \<Rightarrow> nat"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    54
recdef fmsize "measure size"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    55
  "fmsize (NOT p) = 1 + fmsize p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    56
  "fmsize (And p q) = 1 + fmsize p + fmsize q"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    57
  "fmsize (Or p q) = 1 + fmsize p + fmsize q"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    58
  "fmsize (Imp p q) = 3 + fmsize p + fmsize q"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    59
  "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    60
  "fmsize (E p) = 1 + fmsize p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    61
  "fmsize (A p) = 4+ fmsize p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    62
  "fmsize (Dvd i t) = 2"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    63
  "fmsize (NDvd i t) = 2"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    64
  "fmsize p = 1"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    65
  (* several lemmas about fmsize *)
25162
ad4d5365d9d8 went back to >0
nipkow
parents: 25134
diff changeset
    66
lemma fmsize_pos: "fmsize p > 0"	
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    67
by (induct p rule: fmsize.induct) simp_all
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
    68
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    69
  (* Semantics of formulae (fm) *)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    70
consts Ifm ::"bool list \<Rightarrow> int list \<Rightarrow> fm \<Rightarrow> bool"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    71
primrec
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    72
  "Ifm bbs bs T = True"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    73
  "Ifm bbs bs F = False"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    74
  "Ifm bbs bs (Lt a) = (Inum bs a < 0)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    75
  "Ifm bbs bs (Gt a) = (Inum bs a > 0)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    76
  "Ifm bbs bs (Le a) = (Inum bs a \<le> 0)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    77
  "Ifm bbs bs (Ge a) = (Inum bs a \<ge> 0)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    78
  "Ifm bbs bs (Eq a) = (Inum bs a = 0)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    79
  "Ifm bbs bs (NEq a) = (Inum bs a \<noteq> 0)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    80
  "Ifm bbs bs (Dvd i b) = (i dvd Inum bs b)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    81
  "Ifm bbs bs (NDvd i b) = (\<not>(i dvd Inum bs b))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    82
  "Ifm bbs bs (NOT p) = (\<not> (Ifm bbs bs p))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    83
  "Ifm bbs bs (And p q) = (Ifm bbs bs p \<and> Ifm bbs bs q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    84
  "Ifm bbs bs (Or p q) = (Ifm bbs bs p \<or> Ifm bbs bs q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    85
  "Ifm bbs bs (Imp p q) = ((Ifm bbs bs p) \<longrightarrow> (Ifm bbs bs q))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    86
  "Ifm bbs bs (Iff p q) = (Ifm bbs bs p = Ifm bbs bs q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    87
  "Ifm bbs bs (E p) = (\<exists> x. Ifm bbs (x#bs) p)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    88
  "Ifm bbs bs (A p) = (\<forall> x. Ifm bbs (x#bs) p)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    89
  "Ifm bbs bs (Closed n) = bbs!n"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    90
  "Ifm bbs bs (NClosed n) = (\<not> bbs!n)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    91
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    92
consts prep :: "fm \<Rightarrow> fm"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    93
recdef prep "measure fmsize"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    94
  "prep (E T) = T"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    95
  "prep (E F) = F"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    96
  "prep (E (Or p q)) = Or (prep (E p)) (prep (E q))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    97
  "prep (E (Imp p q)) = Or (prep (E (NOT p))) (prep (E q))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    98
  "prep (E (Iff p q)) = Or (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
    99
  "prep (E (NOT (And p q))) = Or (prep (E (NOT p))) (prep (E(NOT q)))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   100
  "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   101
  "prep (E (NOT (Iff p q))) = Or (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   102
  "prep (E p) = E (prep p)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   103
  "prep (A (And p q)) = And (prep (A p)) (prep (A q))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   104
  "prep (A p) = prep (NOT (E (NOT p)))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   105
  "prep (NOT (NOT p)) = prep p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   106
  "prep (NOT (And p q)) = Or (prep (NOT p)) (prep (NOT q))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   107
  "prep (NOT (A p)) = prep (E (NOT p))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   108
  "prep (NOT (Or p q)) = And (prep (NOT p)) (prep (NOT q))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   109
  "prep (NOT (Imp p q)) = And (prep p) (prep (NOT q))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   110
  "prep (NOT (Iff p q)) = Or (prep (And p (NOT q))) (prep (And (NOT p) q))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   111
  "prep (NOT p) = NOT (prep p)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   112
  "prep (Or p q) = Or (prep p) (prep q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   113
  "prep (And p q) = And (prep p) (prep q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   114
  "prep (Imp p q) = prep (Or (NOT p) q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   115
  "prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   116
  "prep p = p"
25162
ad4d5365d9d8 went back to >0
nipkow
parents: 25134
diff changeset
   117
(hints simp add: fmsize_pos)
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   118
lemma prep: "Ifm bbs bs (prep p) = Ifm bbs bs p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   119
by (induct p arbitrary: bs rule: prep.induct, auto)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   120
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
   121
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   122
  (* Quantifier freeness *)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   123
consts qfree:: "fm \<Rightarrow> bool"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   124
recdef qfree "measure size"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   125
  "qfree (E p) = False"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   126
  "qfree (A p) = False"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   127
  "qfree (NOT p) = qfree p" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   128
  "qfree (And p q) = (qfree p \<and> qfree q)" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   129
  "qfree (Or  p q) = (qfree p \<and> qfree q)" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   130
  "qfree (Imp p q) = (qfree p \<and> qfree q)" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   131
  "qfree (Iff p q) = (qfree p \<and> qfree q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   132
  "qfree p = True"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   133
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   134
  (* Boundedness and substitution *)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   135
consts 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   136
  numbound0:: "num \<Rightarrow> bool" (* a num is INDEPENDENT of Bound 0 *)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   137
  bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   138
  subst0:: "num \<Rightarrow> fm \<Rightarrow> fm" (* substitue a num into a formula for Bound 0 *)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   139
primrec
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   140
  "numbound0 (C c) = True"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   141
  "numbound0 (Bound n) = (n>0)"
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   142
  "numbound0 (CN n i a) = (n >0 \<and> numbound0 a)"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   143
  "numbound0 (Neg a) = numbound0 a"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   144
  "numbound0 (Add a b) = (numbound0 a \<and> numbound0 b)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   145
  "numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   146
  "numbound0 (Mul i a) = numbound0 a"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   147
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   148
lemma numbound0_I:
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   149
  assumes nb: "numbound0 a"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   150
  shows "Inum (b#bs) a = Inum (b'#bs) a"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   151
using nb
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   152
by (induct a rule: numbound0.induct) (auto simp add: gr0_conv_Suc)
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
   153
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   154
primrec
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   155
  "bound0 T = True"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   156
  "bound0 F = True"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   157
  "bound0 (Lt a) = numbound0 a"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   158
  "bound0 (Le a) = numbound0 a"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   159
  "bound0 (Gt a) = numbound0 a"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   160
  "bound0 (Ge a) = numbound0 a"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   161
  "bound0 (Eq a) = numbound0 a"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   162
  "bound0 (NEq a) = numbound0 a"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   163
  "bound0 (Dvd i a) = numbound0 a"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   164
  "bound0 (NDvd i a) = numbound0 a"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   165
  "bound0 (NOT p) = bound0 p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   166
  "bound0 (And p q) = (bound0 p \<and> bound0 q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   167
  "bound0 (Or p q) = (bound0 p \<and> bound0 q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   168
  "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   169
  "bound0 (Iff p q) = (bound0 p \<and> bound0 q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   170
  "bound0 (E p) = False"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   171
  "bound0 (A p) = False"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   172
  "bound0 (Closed P) = True"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   173
  "bound0 (NClosed P) = True"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   174
lemma bound0_I:
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   175
  assumes bp: "bound0 p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   176
  shows "Ifm bbs (b#bs) p = Ifm bbs (b'#bs) p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   177
using bp numbound0_I[where b="b" and bs="bs" and b'="b'"]
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   178
by (induct p rule: bound0.induct) (auto simp add: gr0_conv_Suc)
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   179
27456
52c7c42e7e27 code antiquotation roaring ahead
haftmann
parents: 26934
diff changeset
   180
fun numsubst0:: "num \<Rightarrow> num \<Rightarrow> num" where
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   181
  "numsubst0 t (C c) = (C c)"
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   182
| "numsubst0 t (Bound n) = (if n=0 then t else Bound n)"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   183
| "numsubst0 t (CN 0 i a) = Add (Mul i t) (numsubst0 t a)"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   184
| "numsubst0 t (CN n i a) = CN n i (numsubst0 t a)"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   185
| "numsubst0 t (Neg a) = Neg (numsubst0 t a)"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   186
| "numsubst0 t (Add a b) = Add (numsubst0 t a) (numsubst0 t b)"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   187
| "numsubst0 t (Sub a b) = Sub (numsubst0 t a) (numsubst0 t b)" 
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   188
| "numsubst0 t (Mul i a) = Mul i (numsubst0 t a)"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   189
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   190
lemma numsubst0_I:
25134
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
   191
  "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t"
25162
ad4d5365d9d8 went back to >0
nipkow
parents: 25134
diff changeset
   192
by (induct t rule: numsubst0.induct,auto simp:nth_Cons')
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
   193
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   194
lemma numsubst0_I':
25134
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
   195
  "numbound0 a \<Longrightarrow> Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t"
25162
ad4d5365d9d8 went back to >0
nipkow
parents: 25134
diff changeset
   196
by (induct t rule: numsubst0.induct, auto simp: nth_Cons' numbound0_I[where b="b" and b'="b'"])
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   197
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   198
primrec
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   199
  "subst0 t T = T"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   200
  "subst0 t F = F"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   201
  "subst0 t (Lt a) = Lt (numsubst0 t a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   202
  "subst0 t (Le a) = Le (numsubst0 t a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   203
  "subst0 t (Gt a) = Gt (numsubst0 t a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   204
  "subst0 t (Ge a) = Ge (numsubst0 t a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   205
  "subst0 t (Eq a) = Eq (numsubst0 t a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   206
  "subst0 t (NEq a) = NEq (numsubst0 t a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   207
  "subst0 t (Dvd i a) = Dvd i (numsubst0 t a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   208
  "subst0 t (NDvd i a) = NDvd i (numsubst0 t a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   209
  "subst0 t (NOT p) = NOT (subst0 t p)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   210
  "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   211
  "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   212
  "subst0 t (Imp p q) = Imp (subst0 t p) (subst0 t q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   213
  "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   214
  "subst0 t (Closed P) = (Closed P)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   215
  "subst0 t (NClosed P) = (NClosed P)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   216
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   217
lemma subst0_I: assumes qfp: "qfree p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   218
  shows "Ifm bbs (b#bs) (subst0 a p) = Ifm bbs ((Inum (b#bs) a)#bs) p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   219
  using qfp numsubst0_I[where b="b" and bs="bs" and a="a"]
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   220
  by (induct p) (simp_all add: gr0_conv_Suc)
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   221
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   222
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   223
consts 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   224
  decrnum:: "num \<Rightarrow> num" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   225
  decr :: "fm \<Rightarrow> fm"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   226
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   227
recdef decrnum "measure size"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   228
  "decrnum (Bound n) = Bound (n - 1)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   229
  "decrnum (Neg a) = Neg (decrnum a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   230
  "decrnum (Add a b) = Add (decrnum a) (decrnum b)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   231
  "decrnum (Sub a b) = Sub (decrnum a) (decrnum b)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   232
  "decrnum (Mul c a) = Mul c (decrnum a)"
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   233
  "decrnum (CN n i a) = (CN (n - 1) i (decrnum a))"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   234
  "decrnum a = a"
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
   235
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   236
recdef decr "measure size"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   237
  "decr (Lt a) = Lt (decrnum a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   238
  "decr (Le a) = Le (decrnum a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   239
  "decr (Gt a) = Gt (decrnum a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   240
  "decr (Ge a) = Ge (decrnum a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   241
  "decr (Eq a) = Eq (decrnum a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   242
  "decr (NEq a) = NEq (decrnum a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   243
  "decr (Dvd i a) = Dvd i (decrnum a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   244
  "decr (NDvd i a) = NDvd i (decrnum a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   245
  "decr (NOT p) = NOT (decr p)" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   246
  "decr (And p q) = And (decr p) (decr q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   247
  "decr (Or p q) = Or (decr p) (decr q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   248
  "decr (Imp p q) = Imp (decr p) (decr q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   249
  "decr (Iff p q) = Iff (decr p) (decr q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   250
  "decr p = p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   251
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   252
lemma decrnum: assumes nb: "numbound0 t"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   253
  shows "Inum (x#bs) t = Inum bs (decrnum t)"
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   254
  using nb by (induct t rule: decrnum.induct, auto simp add: gr0_conv_Suc)
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   255
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   256
lemma decr: assumes nb: "bound0 p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   257
  shows "Ifm bbs (x#bs) p = Ifm bbs bs (decr p)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   258
  using nb 
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   259
  by (induct p rule: decr.induct, simp_all add: gr0_conv_Suc decrnum)
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   260
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   261
lemma decr_qf: "bound0 p \<Longrightarrow> qfree (decr p)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   262
by (induct p, simp_all)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   263
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   264
consts 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   265
  isatom :: "fm \<Rightarrow> bool" (* test for atomicity *)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   266
recdef isatom "measure size"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   267
  "isatom T = True"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   268
  "isatom F = True"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   269
  "isatom (Lt a) = True"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   270
  "isatom (Le a) = True"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   271
  "isatom (Gt a) = True"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   272
  "isatom (Ge a) = True"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   273
  "isatom (Eq a) = True"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   274
  "isatom (NEq a) = True"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   275
  "isatom (Dvd i b) = True"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   276
  "isatom (NDvd i b) = True"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   277
  "isatom (Closed P) = True"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   278
  "isatom (NClosed P) = True"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   279
  "isatom p = False"
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
   280
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   281
lemma numsubst0_numbound0: assumes nb: "numbound0 t"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   282
  shows "numbound0 (numsubst0 t a)"
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   283
using nb apply (induct a rule: numbound0.induct)
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   284
apply simp_all
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   285
apply (case_tac n, simp_all)
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   286
done
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   287
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   288
lemma subst0_bound0: assumes qf: "qfree p" and nb: "numbound0 t"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   289
  shows "bound0 (subst0 t p)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   290
using qf numsubst0_numbound0[OF nb] by (induct p  rule: subst0.induct, auto)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   291
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   292
lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   293
by (induct p, simp_all)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   294
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   295
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   296
constdefs djf:: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   297
  "djf f p q \<equiv> (if q=T then T else if q=F then f p else 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   298
  (let fp = f p in case fp of T \<Rightarrow> T | F \<Rightarrow> q | _ \<Rightarrow> Or (f p) q))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   299
constdefs evaldjf:: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   300
  "evaldjf f ps \<equiv> foldr (djf f) ps F"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   301
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   302
lemma djf_Or: "Ifm bbs bs (djf f p q) = Ifm bbs bs (Or (f p) q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   303
by (cases "q=T", simp add: djf_def,cases "q=F",simp add: djf_def) 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   304
(cases "f p", simp_all add: Let_def djf_def) 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   305
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   306
lemma evaldjf_ex: "Ifm bbs bs (evaldjf f ps) = (\<exists> p \<in> set ps. Ifm bbs bs (f p))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   307
  by(induct ps, simp_all add: evaldjf_def djf_Or)
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
   308
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   309
lemma evaldjf_bound0: 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   310
  assumes nb: "\<forall> x\<in> set xs. bound0 (f x)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   311
  shows "bound0 (evaldjf f xs)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   312
  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto) 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   313
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   314
lemma evaldjf_qf: 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   315
  assumes nb: "\<forall> x\<in> set xs. qfree (f x)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   316
  shows "qfree (evaldjf f xs)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   317
  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto) 
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
   318
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   319
consts disjuncts :: "fm \<Rightarrow> fm list"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   320
recdef disjuncts "measure size"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   321
  "disjuncts (Or p q) = (disjuncts p) @ (disjuncts q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   322
  "disjuncts F = []"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   323
  "disjuncts p = [p]"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   324
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   325
lemma disjuncts: "(\<exists> q\<in> set (disjuncts p). Ifm bbs bs q) = Ifm bbs bs p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   326
by(induct p rule: disjuncts.induct, auto)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   327
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   328
lemma disjuncts_nb: "bound0 p \<Longrightarrow> \<forall> q\<in> set (disjuncts p). bound0 q"
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
   329
proof-
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   330
  assume nb: "bound0 p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   331
  hence "list_all bound0 (disjuncts p)" by (induct p rule:disjuncts.induct,auto)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   332
  thus ?thesis by (simp only: list_all_iff)
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
   333
qed
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
   334
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   335
lemma disjuncts_qf: "qfree p \<Longrightarrow> \<forall> q\<in> set (disjuncts p). qfree q"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   336
proof-
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   337
  assume qf: "qfree p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   338
  hence "list_all qfree (disjuncts p)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   339
    by (induct p rule: disjuncts.induct, auto)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   340
  thus ?thesis by (simp only: list_all_iff)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   341
qed
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
   342
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   343
constdefs DJ :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   344
  "DJ f p \<equiv> evaldjf f (disjuncts p)"
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
   345
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   346
lemma DJ: assumes fdj: "\<forall> p q. f (Or p q) = Or (f p) (f q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   347
  and fF: "f F = F"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   348
  shows "Ifm bbs bs (DJ f p) = Ifm bbs bs (f p)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   349
proof-
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   350
  have "Ifm bbs bs (DJ f p) = (\<exists> q \<in> set (disjuncts p). Ifm bbs bs (f q))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   351
    by (simp add: DJ_def evaldjf_ex) 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   352
  also have "\<dots> = Ifm bbs bs (f p)" using fdj fF by (induct p rule: disjuncts.induct, auto)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   353
  finally show ?thesis .
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   354
qed
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
   355
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   356
lemma DJ_qf: assumes 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   357
  fqf: "\<forall> p. qfree p \<longrightarrow> qfree (f p)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   358
  shows "\<forall>p. qfree p \<longrightarrow> qfree (DJ f p) "
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   359
proof(clarify)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   360
  fix  p assume qf: "qfree p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   361
  have th: "DJ f p = evaldjf f (disjuncts p)" by (simp add: DJ_def)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   362
  from disjuncts_qf[OF qf] have "\<forall> q\<in> set (disjuncts p). qfree q" .
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   363
  with fqf have th':"\<forall> q\<in> set (disjuncts p). qfree (f q)" by blast
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   364
  
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   365
  from evaldjf_qf[OF th'] th show "qfree (DJ f p)" by simp
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
   366
qed
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
   367
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   368
lemma DJ_qe: assumes qe: "\<forall> bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bbs bs (qe p) = Ifm bbs bs (E p))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   369
  shows "\<forall> bs p. qfree p \<longrightarrow> qfree (DJ qe p) \<and> (Ifm bbs bs ((DJ qe p)) = Ifm bbs bs (E p))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   370
proof(clarify)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   371
  fix p::fm and bs
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   372
  assume qf: "qfree p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   373
  from qe have qth: "\<forall> p. qfree p \<longrightarrow> qfree (qe p)" by blast
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   374
  from DJ_qf[OF qth] qf have qfth:"qfree (DJ qe p)" by auto
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   375
  have "Ifm bbs bs (DJ qe p) = (\<exists> q\<in> set (disjuncts p). Ifm bbs bs (qe q))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   376
    by (simp add: DJ_def evaldjf_ex)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   377
  also have "\<dots> = (\<exists> q \<in> set(disjuncts p). Ifm bbs bs (E q))" using qe disjuncts_qf[OF qf] by auto
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   378
  also have "\<dots> = Ifm bbs bs (E p)" by (induct p rule: disjuncts.induct, auto)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   379
  finally show "qfree (DJ qe p) \<and> Ifm bbs bs (DJ qe p) = Ifm bbs bs (E p)" using qfth by blast
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   380
qed
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   381
  (* Simplification *)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   382
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   383
  (* Algebraic simplifications for nums *)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   384
consts bnds:: "num \<Rightarrow> nat list"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   385
  lex_ns:: "nat list \<times> nat list \<Rightarrow> bool"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   386
recdef bnds "measure size"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   387
  "bnds (Bound n) = [n]"
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   388
  "bnds (CN n c a) = n#(bnds a)"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   389
  "bnds (Neg a) = bnds a"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   390
  "bnds (Add a b) = (bnds a)@(bnds b)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   391
  "bnds (Sub a b) = (bnds a)@(bnds b)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   392
  "bnds (Mul i a) = bnds a"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   393
  "bnds a = []"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   394
recdef lex_ns "measure (\<lambda> (xs,ys). length xs + length ys)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   395
  "lex_ns ([], ms) = True"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   396
  "lex_ns (ns, []) = False"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   397
  "lex_ns (n#ns, m#ms) = (n<m \<or> ((n = m) \<and> lex_ns (ns,ms))) "
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   398
constdefs lex_bnd :: "num \<Rightarrow> num \<Rightarrow> bool"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   399
  "lex_bnd t s \<equiv> lex_ns (bnds t, bnds s)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   400
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   401
consts
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   402
  numadd:: "num \<times> num \<Rightarrow> num"
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   403
recdef numadd "measure (\<lambda> (t,s). num_size t + num_size s)"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   404
  "numadd (CN n1 c1 r1 ,CN n2 c2 r2) =
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   405
  (if n1=n2 then 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   406
  (let c = c1 + c2
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   407
  in (if c=0 then numadd(r1,r2) else CN n1 c (numadd (r1,r2))))
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   408
  else if n1 \<le> n2 then CN n1 c1 (numadd (r1,Add (Mul c2 (Bound n2)) r2))
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   409
  else CN n2 c2 (numadd (Add (Mul c1 (Bound n1)) r1,r2)))"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   410
  "numadd (CN n1 c1 r1, t) = CN n1 c1 (numadd (r1, t))"  
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   411
  "numadd (t,CN n2 c2 r2) = CN n2 c2 (numadd (t,r2))" 
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   412
  "numadd (C b1, C b2) = C (b1+b2)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   413
  "numadd (a,b) = Add a b"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   414
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   415
(*function (sequential)
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   416
  numadd :: "num \<Rightarrow> num \<Rightarrow> num"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   417
where
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   418
  "numadd (Add (Mul c1 (Bound n1)) r1) (Add (Mul c2 (Bound n2)) r2) =
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   419
      (if n1 = n2 then (let c = c1 + c2
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   420
      in (if c = 0 then numadd r1 r2 else
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   421
        Add (Mul c (Bound n1)) (numadd r1 r2)))
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   422
      else if n1 \<le> n2 then
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   423
        Add (Mul c1 (Bound n1)) (numadd r1 (Add (Mul c2 (Bound n2)) r2))
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   424
      else
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   425
        Add (Mul c2 (Bound n2)) (numadd (Add (Mul c1 (Bound n1)) r1) r2))"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   426
  | "numadd (Add (Mul c1 (Bound n1)) r1) t =
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   427
      Add (Mul c1 (Bound n1)) (numadd r1 t)"  
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   428
  | "numadd t (Add (Mul c2 (Bound n2)) r2) =
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   429
      Add (Mul c2 (Bound n2)) (numadd t r2)" 
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   430
  | "numadd (C b1) (C b2) = C (b1 + b2)"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   431
  | "numadd a b = Add a b"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   432
apply pat_completeness apply auto*)
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   433
  
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   434
lemma numadd: "Inum bs (numadd (t,s)) = Inum bs (Add t s)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   435
apply (induct t s rule: numadd.induct, simp_all add: Let_def)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   436
apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
23477
f4b83f03cac9 tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents: 23315
diff changeset
   437
 apply (case_tac "n1 = n2")
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29265
diff changeset
   438
  apply(simp_all add: algebra_simps)
23477
f4b83f03cac9 tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents: 23315
diff changeset
   439
apply(simp add: left_distrib[symmetric])
f4b83f03cac9 tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents: 23315
diff changeset
   440
done
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   441
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   442
lemma numadd_nb: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   443
by (induct t s rule: numadd.induct, auto simp add: Let_def)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   444
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   445
fun
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   446
  nummul :: "int \<Rightarrow> num \<Rightarrow> num"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   447
where
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   448
  "nummul i (C j) = C (i * j)"
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   449
  | "nummul i (CN n c t) = CN n (c*i) (nummul i t)"
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   450
  | "nummul i t = Mul i t"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   451
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   452
lemma nummul: "\<And> i. Inum bs (nummul i t) = Inum bs (Mul i t)"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29265
diff changeset
   453
by (induct t rule: nummul.induct, auto simp add: algebra_simps numadd)
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   454
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   455
lemma nummul_nb: "\<And> i. numbound0 t \<Longrightarrow> numbound0 (nummul i t)"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   456
by (induct t rule: nummul.induct, auto simp add: numadd_nb)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   457
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   458
constdefs numneg :: "num \<Rightarrow> num"
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   459
  "numneg t \<equiv> nummul (- 1) t"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   460
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   461
constdefs numsub :: "num \<Rightarrow> num \<Rightarrow> num"
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   462
  "numsub s t \<equiv> (if s = t then C 0 else numadd (s, numneg t))"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   463
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   464
lemma numneg: "Inum bs (numneg t) = Inum bs (Neg t)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   465
using numneg_def nummul by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   466
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   467
lemma numneg_nb: "numbound0 t \<Longrightarrow> numbound0 (numneg t)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   468
using numneg_def nummul_nb by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   469
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   470
lemma numsub: "Inum bs (numsub a b) = Inum bs (Sub a b)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   471
using numneg numadd numsub_def by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   472
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   473
lemma numsub_nb: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numsub t s)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   474
using numsub_def numadd_nb numneg_nb by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   475
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   476
fun
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   477
  simpnum :: "num \<Rightarrow> num"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   478
where
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   479
  "simpnum (C j) = C j"
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   480
  | "simpnum (Bound n) = CN n 1 (C 0)"
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   481
  | "simpnum (Neg t) = numneg (simpnum t)"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   482
  | "simpnum (Add t s) = numadd (simpnum t, simpnum s)"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   483
  | "simpnum (Sub t s) = numsub (simpnum t) (simpnum s)"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   484
  | "simpnum (Mul i t) = (if i = 0 then C 0 else nummul i (simpnum t))"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   485
  | "simpnum t = t"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   486
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   487
lemma simpnum_ci: "Inum bs (simpnum t) = Inum bs t"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   488
by (induct t rule: simpnum.induct, auto simp add: numneg numadd numsub nummul)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   489
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   490
lemma simpnum_numbound0: 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   491
  "numbound0 t \<Longrightarrow> numbound0 (simpnum t)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   492
by (induct t rule: simpnum.induct, auto simp add: numadd_nb numsub_nb nummul_nb numneg_nb)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   493
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   494
fun
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   495
  not :: "fm \<Rightarrow> fm"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   496
where
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   497
  "not (NOT p) = p"
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   498
  | "not T = F"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   499
  | "not F = T"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   500
  | "not p = NOT p"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   501
lemma not: "Ifm bbs bs (not p) = Ifm bbs bs (NOT p)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   502
by (cases p) auto
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   503
lemma not_qf: "qfree p \<Longrightarrow> qfree (not p)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   504
by (cases p, auto)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   505
lemma not_bn: "bound0 p \<Longrightarrow> bound0 (not p)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   506
by (cases p, auto)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   507
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   508
constdefs conj :: "fm \<Rightarrow> fm \<Rightarrow> fm"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   509
  "conj p q \<equiv> (if (p = F \<or> q=F) then F else if p=T then q else if q=T then p else And p q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   510
lemma conj: "Ifm bbs bs (conj p q) = Ifm bbs bs (And p q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   511
by (cases "p=F \<or> q=F",simp_all add: conj_def) (cases p,simp_all)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   512
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   513
lemma conj_qf: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (conj p q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   514
using conj_def by auto 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   515
lemma conj_nb: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (conj p q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   516
using conj_def by auto 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   517
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   518
constdefs disj :: "fm \<Rightarrow> fm \<Rightarrow> fm"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   519
  "disj p q \<equiv> (if (p = T \<or> q=T) then T else if p=F then q else if q=F then p else Or p q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   520
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   521
lemma disj: "Ifm bbs bs (disj p q) = Ifm bbs bs (Or p q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   522
by (cases "p=T \<or> q=T",simp_all add: disj_def) (cases p,simp_all)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   523
lemma disj_qf: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (disj p q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   524
using disj_def by auto 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   525
lemma disj_nb: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (disj p q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   526
using disj_def by auto 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   527
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   528
constdefs   imp :: "fm \<Rightarrow> fm \<Rightarrow> fm"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   529
  "imp p q \<equiv> (if (p = F \<or> q=T) then T else if p=T then q else if q=F then not p else Imp p q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   530
lemma imp: "Ifm bbs bs (imp p q) = Ifm bbs bs (Imp p q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   531
by (cases "p=F \<or> q=T",simp_all add: imp_def,cases p) (simp_all add: not)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   532
lemma imp_qf: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (imp p q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   533
using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def,cases p) (simp_all add: not_qf) 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   534
lemma imp_nb: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (imp p q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   535
using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def,cases p) simp_all
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   536
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   537
constdefs   iff :: "fm \<Rightarrow> fm \<Rightarrow> fm"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   538
  "iff p q \<equiv> (if (p = q) then T else if (p = not q \<or> not p = q) then F else 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   539
       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 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   540
  Iff p q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   541
lemma iff: "Ifm bbs bs (iff p q) = Ifm bbs bs (Iff p q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   542
  by (unfold iff_def,cases "p=q", simp,cases "p=not q", simp add:not) 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   543
(cases "not p= q", auto simp add:not)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   544
lemma iff_qf: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (iff p q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   545
  by (unfold iff_def,cases "p=q", auto simp add: not_qf)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   546
lemma iff_nb: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (iff p q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   547
using iff_def by (unfold iff_def,cases "p=q", auto simp add: not_bn)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   548
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   549
function (sequential)
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   550
  simpfm :: "fm \<Rightarrow> fm"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   551
where
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   552
  "simpfm (And p q) = conj (simpfm p) (simpfm q)"
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   553
  | "simpfm (Or p q) = disj (simpfm p) (simpfm q)"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   554
  | "simpfm (Imp p q) = imp (simpfm p) (simpfm q)"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   555
  | "simpfm (Iff p q) = iff (simpfm p) (simpfm q)"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   556
  | "simpfm (NOT p) = not (simpfm p)"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   557
  | "simpfm (Lt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v < 0) then T else F 
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   558
      | _ \<Rightarrow> Lt a')"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   559
  | "simpfm (Le a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<le> 0)  then T else F | _ \<Rightarrow> Le a')"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   560
  | "simpfm (Gt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v > 0)  then T else F | _ \<Rightarrow> Gt a')"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   561
  | "simpfm (Ge a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<ge> 0)  then T else F | _ \<Rightarrow> Ge a')"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   562
  | "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v = 0)  then T else F | _ \<Rightarrow> Eq a')"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   563
  | "simpfm (NEq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<noteq> 0)  then T else F | _ \<Rightarrow> NEq a')"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   564
  | "simpfm (Dvd i a) = (if i=0 then simpfm (Eq a)
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   565
             else if (abs i = 1) then T
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   566
             else let a' = simpnum a in case a' of C v \<Rightarrow> if (i dvd v)  then T else F | _ \<Rightarrow> Dvd i a')"
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   567
  | "simpfm (NDvd i a) = (if i=0 then simpfm (NEq a) 
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   568
             else if (abs i = 1) then F
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   569
             else let a' = simpnum a in case a' of C v \<Rightarrow> if (\<not>(i dvd v)) then T else F | _ \<Rightarrow> NDvd i a')"
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   570
  | "simpfm p = p"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   571
by pat_completeness auto
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   572
termination by (relation "measure fmsize") auto
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   573
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   574
lemma simpfm: "Ifm bbs bs (simpfm p) = Ifm bbs bs p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   575
proof(induct p rule: simpfm.induct)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   576
  case (6 a) let ?sa = "simpnum a" from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   577
  {fix v assume "?sa = C v" hence ?case using sa by simp }
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   578
  moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   579
      by (cases ?sa, simp_all add: Let_def)}
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   580
  ultimately show ?case by blast
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
   581
next
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   582
  case (7 a)  let ?sa = "simpnum a" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   583
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   584
  {fix v assume "?sa = C v" hence ?case using sa by simp }
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   585
  moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   586
      by (cases ?sa, simp_all add: Let_def)}
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   587
  ultimately show ?case by blast
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   588
next
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   589
  case (8 a)  let ?sa = "simpnum a" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   590
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   591
  {fix v assume "?sa = C v" hence ?case using sa by simp }
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   592
  moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   593
      by (cases ?sa, simp_all add: Let_def)}
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   594
  ultimately show ?case by blast
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   595
next
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   596
  case (9 a)  let ?sa = "simpnum a" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   597
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   598
  {fix v assume "?sa = C v" hence ?case using sa by simp }
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   599
  moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   600
      by (cases ?sa, simp_all add: Let_def)}
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   601
  ultimately show ?case by blast
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   602
next
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   603
  case (10 a)  let ?sa = "simpnum a" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   604
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   605
  {fix v assume "?sa = C v" hence ?case using sa by simp }
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   606
  moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   607
      by (cases ?sa, simp_all add: Let_def)}
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   608
  ultimately show ?case by blast
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   609
next
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   610
  case (11 a)  let ?sa = "simpnum a" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   611
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   612
  {fix v assume "?sa = C v" hence ?case using sa by simp }
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   613
  moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   614
      by (cases ?sa, simp_all add: Let_def)}
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   615
  ultimately show ?case by blast
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   616
next
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   617
  case (12 i a)  let ?sa = "simpnum a" from simpnum_ci 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   618
  have sa: "Inum bs ?sa = Inum bs a" by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   619
  have "i=0 \<or> abs i = 1 \<or> (i\<noteq>0 \<and> (abs i \<noteq> 1))" by auto
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   620
  {assume "i=0" hence ?case using "12.hyps" by (simp add: dvd_def Let_def)}
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   621
  moreover 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   622
  {assume i1: "abs i = 1"
30042
31039ee583fa Removed subsumed lemmas
nipkow
parents: 29823
diff changeset
   623
      from one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
23315
df3a7e9ebadb tuned Proof
chaieb
parents: 23274
diff changeset
   624
      have ?case using i1 apply (cases "i=0", simp_all add: Let_def) 
df3a7e9ebadb tuned Proof
chaieb
parents: 23274
diff changeset
   625
	by (cases "i > 0", simp_all)}
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   626
  moreover   
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   627
  {assume inz: "i\<noteq>0" and cond: "abs i \<noteq> 1"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   628
    {fix v assume "?sa = C v" hence ?case using sa[symmetric] inz cond
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   629
	by (cases "abs i = 1", auto) }
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   630
    moreover {assume "\<not> (\<exists> v. ?sa = C v)" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   631
      hence "simpfm (Dvd i a) = Dvd i ?sa" using inz cond 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   632
	by (cases ?sa, auto simp add: Let_def)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   633
      hence ?case using sa by simp}
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   634
    ultimately have ?case by blast}
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   635
  ultimately show ?case by blast
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   636
next
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   637
  case (13 i a)  let ?sa = "simpnum a" from simpnum_ci 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   638
  have sa: "Inum bs ?sa = Inum bs a" by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   639
  have "i=0 \<or> abs i = 1 \<or> (i\<noteq>0 \<and> (abs i \<noteq> 1))" by auto
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   640
  {assume "i=0" hence ?case using "13.hyps" by (simp add: dvd_def Let_def)}
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   641
  moreover 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   642
  {assume i1: "abs i = 1"
30042
31039ee583fa Removed subsumed lemmas
nipkow
parents: 29823
diff changeset
   643
      from one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
23315
df3a7e9ebadb tuned Proof
chaieb
parents: 23274
diff changeset
   644
      have ?case using i1 apply (cases "i=0", simp_all add: Let_def)
df3a7e9ebadb tuned Proof
chaieb
parents: 23274
diff changeset
   645
      apply (cases "i > 0", simp_all) done}
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   646
  moreover   
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   647
  {assume inz: "i\<noteq>0" and cond: "abs i \<noteq> 1"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   648
    {fix v assume "?sa = C v" hence ?case using sa[symmetric] inz cond
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   649
	by (cases "abs i = 1", auto) }
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   650
    moreover {assume "\<not> (\<exists> v. ?sa = C v)" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   651
      hence "simpfm (NDvd i a) = NDvd i ?sa" using inz cond 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   652
	by (cases ?sa, auto simp add: Let_def)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   653
      hence ?case using sa by simp}
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   654
    ultimately have ?case by blast}
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   655
  ultimately show ?case by blast
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   656
qed (induct p rule: simpfm.induct, simp_all add: conj disj imp iff not)
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
   657
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   658
lemma simpfm_bound0: "bound0 p \<Longrightarrow> bound0 (simpfm p)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   659
proof(induct p rule: simpfm.induct)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   660
  case (6 a) hence nb: "numbound0 a" by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   661
  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   662
  thus ?case by (cases "simpnum a", auto simp add: Let_def)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   663
next
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   664
  case (7 a) hence nb: "numbound0 a" by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   665
  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   666
  thus ?case by (cases "simpnum a", auto simp add: Let_def)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   667
next
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   668
  case (8 a) hence nb: "numbound0 a" by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   669
  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   670
  thus ?case by (cases "simpnum a", auto simp add: Let_def)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   671
next
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   672
  case (9 a) hence nb: "numbound0 a" by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   673
  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   674
  thus ?case by (cases "simpnum a", auto simp add: Let_def)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   675
next
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   676
  case (10 a) hence nb: "numbound0 a" by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   677
  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   678
  thus ?case by (cases "simpnum a", auto simp add: Let_def)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   679
next
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   680
  case (11 a) hence nb: "numbound0 a" by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   681
  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   682
  thus ?case by (cases "simpnum a", auto simp add: Let_def)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   683
next
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   684
  case (12 i a) hence nb: "numbound0 a" by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   685
  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   686
  thus ?case by (cases "simpnum a", auto simp add: Let_def)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   687
next
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   688
  case (13 i a) hence nb: "numbound0 a" by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   689
  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   690
  thus ?case by (cases "simpnum a", auto simp add: Let_def)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   691
qed(auto simp add: disj_def imp_def iff_def conj_def not_bn)
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
   692
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   693
lemma simpfm_qf: "qfree p \<Longrightarrow> qfree (simpfm p)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   694
by (induct p rule: simpfm.induct, auto simp add: disj_qf imp_qf iff_qf conj_qf not_qf Let_def)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   695
 (case_tac "simpnum a",auto)+
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   696
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   697
  (* Generic quantifier elimination *)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   698
consts qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   699
recdef qelim "measure fmsize"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   700
  "qelim (E p) = (\<lambda> qe. DJ qe (qelim p qe))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   701
  "qelim (A p) = (\<lambda> qe. not (qe ((qelim (NOT p) qe))))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   702
  "qelim (NOT p) = (\<lambda> qe. not (qelim p qe))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   703
  "qelim (And p q) = (\<lambda> qe. conj (qelim p qe) (qelim q qe))" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   704
  "qelim (Or  p q) = (\<lambda> qe. disj (qelim p qe) (qelim q qe))" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   705
  "qelim (Imp p q) = (\<lambda> qe. imp (qelim p qe) (qelim q qe))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   706
  "qelim (Iff p q) = (\<lambda> qe. iff (qelim p qe) (qelim q qe))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   707
  "qelim p = (\<lambda> y. simpfm p)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   708
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   709
(*function (sequential)
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   710
  qelim :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   711
where
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   712
  "qelim qe (E p) = DJ qe (qelim qe p)"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   713
  | "qelim qe (A p) = not (qe ((qelim qe (NOT p))))"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   714
  | "qelim qe (NOT p) = not (qelim qe p)"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   715
  | "qelim qe (And p q) = conj (qelim qe p) (qelim qe q)" 
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   716
  | "qelim qe (Or  p q) = disj (qelim qe p) (qelim qe q)" 
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   717
  | "qelim qe (Imp p q) = imp (qelim qe p) (qelim qe q)"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   718
  | "qelim qe (Iff p q) = iff (qelim qe p) (qelim qe q)"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   719
  | "qelim qe p = simpfm p"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   720
by pat_completeness auto
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   721
termination by (relation "measure (fmsize o snd)") auto*)
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   722
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   723
lemma qelim_ci:
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   724
  assumes qe_inv: "\<forall> bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bbs bs (qe p) = Ifm bbs bs (E p))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   725
  shows "\<And> bs. qfree (qelim p qe) \<and> (Ifm bbs bs (qelim p qe) = Ifm bbs bs p)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   726
using qe_inv DJ_qe[OF qe_inv] 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   727
by(induct p rule: qelim.induct) 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   728
(auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   729
  simpfm simpfm_qf simp del: simpfm.simps)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   730
  (* Linearity for fm where Bound 0 ranges over \<int> *)
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   731
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   732
fun
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   733
  zsplit0 :: "num \<Rightarrow> int \<times> num" (* splits the bounded from the unbounded part*)
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   734
where
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   735
  "zsplit0 (C c) = (0,C c)"
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   736
  | "zsplit0 (Bound n) = (if n=0 then (1, C 0) else (0,Bound n))"
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   737
  | "zsplit0 (CN n i a) = 
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   738
      (let (i',a') =  zsplit0 a 
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   739
       in if n=0 then (i+i', a') else (i',CN n i a'))"
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   740
  | "zsplit0 (Neg a) = (let (i',a') =  zsplit0 a in (-i', Neg a'))"
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   741
  | "zsplit0 (Add a b) = (let (ia,a') =  zsplit0 a ; 
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   742
                            (ib,b') =  zsplit0 b 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   743
                            in (ia+ib, Add a' b'))"
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   744
  | "zsplit0 (Sub a b) = (let (ia,a') =  zsplit0 a ; 
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   745
                            (ib,b') =  zsplit0 b 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   746
                            in (ia-ib, Sub a' b'))"
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   747
  | "zsplit0 (Mul i a) = (let (i',a') =  zsplit0 a in (i*i', Mul i a'))"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   748
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   749
lemma zsplit0_I:
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   750
  shows "\<And> n a. zsplit0 t = (n,a) \<Longrightarrow> (Inum ((x::int) #bs) (CN 0 n a) = Inum (x #bs) t) \<and> numbound0 a"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   751
  (is "\<And> n a. ?S t = (n,a) \<Longrightarrow> (?I x (CN 0 n a) = ?I x t) \<and> ?N a")
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   752
proof(induct t rule: zsplit0.induct)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   753
  case (1 c n a) thus ?case by auto 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   754
next
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   755
  case (2 m n a) thus ?case by (cases "m=0") auto
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   756
next
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   757
  case (3 m i a n a')
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   758
  let ?j = "fst (zsplit0 a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   759
  let ?b = "snd (zsplit0 a)"
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   760
  have abj: "zsplit0 a = (?j,?b)" by simp 
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   761
  {assume "m\<noteq>0" 
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   762
    with prems(1)[OF abj] prems(2) have ?case by (auto simp add: Let_def split_def)}
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   763
  moreover
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   764
  {assume m0: "m =0"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   765
    from abj have th: "a'=?b \<and> n=i+?j" using prems 
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   766
      by (simp add: Let_def split_def)
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   767
    from abj prems  have th2: "(?I x (CN 0 ?j ?b) = ?I x a) \<and> ?N ?b" by blast
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   768
    from th have "?I x (CN 0 n a') = ?I x (CN 0 (i+?j) ?b)" by simp
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   769
    also from th2 have "\<dots> = ?I x (CN 0 i (CN 0 ?j ?b))" by (simp add: left_distrib)
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   770
  finally have "?I x (CN 0 n a') = ?I  x (CN 0 i a)" using th2 by simp
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   771
  with th2 th have ?case using m0 by blast} 
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   772
ultimately show ?case by blast
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   773
next
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   774
  case (4 t n a)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   775
  let ?nt = "fst (zsplit0 t)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   776
  let ?at = "snd (zsplit0 t)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   777
  have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Neg ?at \<and> n=-?nt" using prems 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   778
    by (simp add: Let_def split_def)
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   779
  from abj prems  have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   780
  from th2[simplified] th[simplified] show ?case by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   781
next
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   782
  case (5 s t n a)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   783
  let ?ns = "fst (zsplit0 s)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   784
  let ?as = "snd (zsplit0 s)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   785
  let ?nt = "fst (zsplit0 t)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   786
  let ?at = "snd (zsplit0 t)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   787
  have abjs: "zsplit0 s = (?ns,?as)" by simp 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   788
  moreover have abjt:  "zsplit0 t = (?nt,?at)" by simp 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   789
  ultimately have th: "a=Add ?as ?at \<and> n=?ns + ?nt" using prems 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   790
    by (simp add: Let_def split_def)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   791
  from abjs[symmetric] have bluddy: "\<exists> x y. (x,y) = zsplit0 s" by blast
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   792
  from prems have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)" by auto
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   793
  with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   794
  from abjs prems  have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   795
  from th3[simplified] th2[simplified] th[simplified] show ?case 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   796
    by (simp add: left_distrib)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   797
next
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   798
  case (6 s t n a)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   799
  let ?ns = "fst (zsplit0 s)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   800
  let ?as = "snd (zsplit0 s)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   801
  let ?nt = "fst (zsplit0 t)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   802
  let ?at = "snd (zsplit0 t)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   803
  have abjs: "zsplit0 s = (?ns,?as)" by simp 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   804
  moreover have abjt:  "zsplit0 t = (?nt,?at)" by simp 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   805
  ultimately have th: "a=Sub ?as ?at \<and> n=?ns - ?nt" using prems 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   806
    by (simp add: Let_def split_def)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   807
  from abjs[symmetric] have bluddy: "\<exists> x y. (x,y) = zsplit0 s" by blast
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   808
  from prems have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)" by auto
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   809
  with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   810
  from abjs prems  have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   811
  from th3[simplified] th2[simplified] th[simplified] show ?case 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   812
    by (simp add: left_diff_distrib)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   813
next
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   814
  case (7 i t n a)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   815
  let ?nt = "fst (zsplit0 t)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   816
  let ?at = "snd (zsplit0 t)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   817
  have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Mul i ?at \<and> n=i*?nt" using prems 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   818
    by (simp add: Let_def split_def)
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   819
  from abj prems  have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   820
  hence " ?I x (Mul i t) = i * ?I x (CN 0 ?nt ?at)" by simp
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   821
  also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: right_distrib)
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   822
  finally show ?case using th th2 by simp
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
   823
qed
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
   824
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   825
consts
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   826
  iszlfm :: "fm \<Rightarrow> bool"   (* Linearity test for fm *)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   827
recdef iszlfm "measure size"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   828
  "iszlfm (And p q) = (iszlfm p \<and> iszlfm q)" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   829
  "iszlfm (Or p q) = (iszlfm p \<and> iszlfm q)" 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   830
  "iszlfm (Eq  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   831
  "iszlfm (NEq (CN 0 c e)) = (c>0 \<and> numbound0 e)"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   832
  "iszlfm (Lt  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   833
  "iszlfm (Le  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   834
  "iszlfm (Gt  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   835
  "iszlfm (Ge  (CN 0 c e)) = ( c>0 \<and> numbound0 e)"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   836
  "iszlfm (Dvd i (CN 0 c e)) = 
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   837
                 (c>0 \<and> i>0 \<and> numbound0 e)"
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   838
  "iszlfm (NDvd i (CN 0 c e))= 
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   839
                 (c>0 \<and> i>0 \<and> numbound0 e)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   840
  "iszlfm p = (isatom p \<and> (bound0 p))"
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
   841
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   842
lemma zlin_qfree: "iszlfm p \<Longrightarrow> qfree p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   843
  by (induct p rule: iszlfm.induct) auto
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
   844
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   845
consts
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23515
diff changeset
   846
  zlfm :: "fm \<Rightarrow> fm"       (* Linearity transformation for fm *)
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   847
recdef zlfm "measure fmsize"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   848
  "zlfm (And p q) = And (zlfm p) (zlfm q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   849
  "zlfm (Or p q) = Or (zlfm p) (zlfm q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   850
  "zlfm (Imp p q) = Or (zlfm (NOT p)) (zlfm q)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   851
  "zlfm (Iff p q) = Or (And (zlfm p) (zlfm q)) (And (zlfm (NOT p)) (zlfm (NOT q)))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   852
  "zlfm (Lt a) = (let (c,r) = zsplit0 a in 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   853
     if c=0 then Lt r else 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   854
     if c>0 then (Lt (CN 0 c r)) else (Gt (CN 0 (- c) (Neg r))))"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   855
  "zlfm (Le a) = (let (c,r) = zsplit0 a in 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   856
     if c=0 then Le r else 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   857
     if c>0 then (Le (CN 0 c r)) else (Ge (CN 0 (- c) (Neg r))))"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   858
  "zlfm (Gt a) = (let (c,r) = zsplit0 a in 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   859
     if c=0 then Gt r else 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   860
     if c>0 then (Gt (CN 0 c r)) else (Lt (CN 0 (- c) (Neg r))))"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   861
  "zlfm (Ge a) = (let (c,r) = zsplit0 a in 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   862
     if c=0 then Ge r else 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   863
     if c>0 then (Ge (CN 0 c r)) else (Le (CN 0 (- c) (Neg r))))"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   864
  "zlfm (Eq a) = (let (c,r) = zsplit0 a in 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   865
     if c=0 then Eq r else 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   866
     if c>0 then (Eq (CN 0 c r)) else (Eq (CN 0 (- c) (Neg r))))"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   867
  "zlfm (NEq a) = (let (c,r) = zsplit0 a in 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   868
     if c=0 then NEq r else 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   869
     if c>0 then (NEq (CN 0 c r)) else (NEq (CN 0 (- c) (Neg r))))"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   870
  "zlfm (Dvd i a) = (if i=0 then zlfm (Eq a) 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   871
        else (let (c,r) = zsplit0 a in 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   872
              if c=0 then (Dvd (abs i) r) else 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   873
      if c>0 then (Dvd (abs i) (CN 0 c r))
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   874
      else (Dvd (abs i) (CN 0 (- c) (Neg r)))))"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   875
  "zlfm (NDvd i a) = (if i=0 then zlfm (NEq a) 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   876
        else (let (c,r) = zsplit0 a in 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   877
              if c=0 then (NDvd (abs i) r) else 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   878
      if c>0 then (NDvd (abs i) (CN 0 c r))
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   879
      else (NDvd (abs i) (CN 0 (- c) (Neg r)))))"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   880
  "zlfm (NOT (And p q)) = Or (zlfm (NOT p)) (zlfm (NOT q))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   881
  "zlfm (NOT (Or p q)) = And (zlfm (NOT p)) (zlfm (NOT q))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   882
  "zlfm (NOT (Imp p q)) = And (zlfm p) (zlfm (NOT q))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   883
  "zlfm (NOT (Iff p q)) = Or (And(zlfm p) (zlfm(NOT q))) (And (zlfm(NOT p)) (zlfm q))"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   884
  "zlfm (NOT (NOT p)) = zlfm p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   885
  "zlfm (NOT T) = F"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   886
  "zlfm (NOT F) = T"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   887
  "zlfm (NOT (Lt a)) = zlfm (Ge a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   888
  "zlfm (NOT (Le a)) = zlfm (Gt a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   889
  "zlfm (NOT (Gt a)) = zlfm (Le a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   890
  "zlfm (NOT (Ge a)) = zlfm (Lt a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   891
  "zlfm (NOT (Eq a)) = zlfm (NEq a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   892
  "zlfm (NOT (NEq a)) = zlfm (Eq a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   893
  "zlfm (NOT (Dvd i a)) = zlfm (NDvd i a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   894
  "zlfm (NOT (NDvd i a)) = zlfm (Dvd i a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   895
  "zlfm (NOT (Closed P)) = NClosed P"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   896
  "zlfm (NOT (NClosed P)) = Closed P"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   897
  "zlfm p = p" (hints simp add: fmsize_pos)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   898
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   899
lemma zlfm_I:
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   900
  assumes qfp: "qfree p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   901
  shows "(Ifm bbs (i#bs) (zlfm p) = Ifm bbs (i# bs) p) \<and> iszlfm (zlfm p)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   902
  (is "(?I (?l p) = ?I p) \<and> ?L (?l p)")
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   903
using qfp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   904
proof(induct p rule: zlfm.induct)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   905
  case (5 a) 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   906
  let ?c = "fst (zsplit0 a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   907
  let ?r = "snd (zsplit0 a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   908
  have spl: "zsplit0 a = (?c,?r)" by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   909
  from zsplit0_I[OF spl, where x="i" and bs="bs"] 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   910
  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   911
  let ?N = "\<lambda> t. Inum (i#bs) t"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   912
  from prems Ia nb  show ?case 
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29265
diff changeset
   913
    apply (auto simp add: Let_def split_def algebra_simps) 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   914
    apply (cases "?r",auto)
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   915
    apply (case_tac nat, auto)
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   916
    done
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   917
next
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   918
  case (6 a)  
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   919
  let ?c = "fst (zsplit0 a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   920
  let ?r = "snd (zsplit0 a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   921
  have spl: "zsplit0 a = (?c,?r)" by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   922
  from zsplit0_I[OF spl, where x="i" and bs="bs"] 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   923
  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   924
  let ?N = "\<lambda> t. Inum (i#bs) t"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   925
  from prems Ia nb  show ?case 
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29265
diff changeset
   926
    apply (auto simp add: Let_def split_def algebra_simps) 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   927
    apply (cases "?r",auto)
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   928
    apply (case_tac nat, auto)
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   929
    done
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   930
next
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   931
  case (7 a)  
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   932
  let ?c = "fst (zsplit0 a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   933
  let ?r = "snd (zsplit0 a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   934
  have spl: "zsplit0 a = (?c,?r)" by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   935
  from zsplit0_I[OF spl, where x="i" and bs="bs"] 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   936
  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   937
  let ?N = "\<lambda> t. Inum (i#bs) t"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   938
  from prems Ia nb  show ?case 
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29265
diff changeset
   939
    apply (auto simp add: Let_def split_def algebra_simps) 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   940
    apply (cases "?r",auto)
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   941
    apply (case_tac nat, auto)
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   942
    done
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   943
next
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   944
  case (8 a)  
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   945
  let ?c = "fst (zsplit0 a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   946
  let ?r = "snd (zsplit0 a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   947
  have spl: "zsplit0 a = (?c,?r)" by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   948
  from zsplit0_I[OF spl, where x="i" and bs="bs"] 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   949
  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   950
  let ?N = "\<lambda> t. Inum (i#bs) t"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   951
  from prems Ia nb  show ?case 
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29265
diff changeset
   952
    apply (auto simp add: Let_def split_def algebra_simps) 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   953
    apply (cases "?r",auto)
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   954
    apply (case_tac nat, auto)
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   955
    done
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   956
next
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   957
  case (9 a)  
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   958
  let ?c = "fst (zsplit0 a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   959
  let ?r = "snd (zsplit0 a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   960
  have spl: "zsplit0 a = (?c,?r)" by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   961
  from zsplit0_I[OF spl, where x="i" and bs="bs"] 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   962
  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   963
  let ?N = "\<lambda> t. Inum (i#bs) t"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   964
  from prems Ia nb  show ?case 
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29265
diff changeset
   965
    apply (auto simp add: Let_def split_def algebra_simps) 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   966
    apply (cases "?r",auto)
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   967
    apply (case_tac nat, auto)
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   968
    done
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   969
next
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   970
  case (10 a)  
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   971
  let ?c = "fst (zsplit0 a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   972
  let ?r = "snd (zsplit0 a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   973
  have spl: "zsplit0 a = (?c,?r)" by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   974
  from zsplit0_I[OF spl, where x="i" and bs="bs"] 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   975
  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   976
  let ?N = "\<lambda> t. Inum (i#bs) t"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   977
  from prems Ia nb  show ?case 
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29265
diff changeset
   978
    apply (auto simp add: Let_def split_def algebra_simps) 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   979
    apply (cases "?r",auto)
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   980
    apply (case_tac nat, auto)
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   981
    done
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
   982
next
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   983
  case (11 j a)  
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   984
  let ?c = "fst (zsplit0 a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   985
  let ?r = "snd (zsplit0 a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   986
  have spl: "zsplit0 a = (?c,?r)" by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   987
  from zsplit0_I[OF spl, where x="i" and bs="bs"] 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   988
  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   989
  let ?N = "\<lambda> t. Inum (i#bs) t"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   990
  have "j=0 \<or> (j\<noteq>0 \<and> ?c = 0) \<or> (j\<noteq>0 \<and> ?c >0) \<or> (j\<noteq> 0 \<and> ?c<0)" by arith
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   991
  moreover
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   992
  {assume "j=0" hence z: "zlfm (Dvd j a) = (zlfm (Eq a))" by (simp add: Let_def) 
30042
31039ee583fa Removed subsumed lemmas
nipkow
parents: 29823
diff changeset
   993
    hence ?case using prems by (simp del: zlfm.simps)}
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   994
  moreover
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
   995
  {assume "?c=0" and "j\<noteq>0" hence ?case 
29700
22faf21db3df added some simp rules
nipkow
parents: 29667
diff changeset
   996
      using zsplit0_I[OF spl, where x="i" and bs="bs"]
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29265
diff changeset
   997
    apply (auto simp add: Let_def split_def algebra_simps) 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   998
    apply (cases "?r",auto)
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
   999
    apply (case_tac nat, auto)
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1000
    done}
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1001
  moreover
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1002
  {assume cp: "?c > 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1003
      by (simp add: nb Let_def split_def)
29700
22faf21db3df added some simp rules
nipkow
parents: 29667
diff changeset
  1004
    hence ?case using Ia cp jnz by (simp add: Let_def split_def)}
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1005
  moreover
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1006
  {assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1007
      by (simp add: nb Let_def split_def)
30042
31039ee583fa Removed subsumed lemmas
nipkow
parents: 29823
diff changeset
  1008
    hence ?case using Ia cn jnz dvd_minus_iff[of "abs j" "?c*i + ?N ?r" ]
29700
22faf21db3df added some simp rules
nipkow
parents: 29667
diff changeset
  1009
      by (simp add: Let_def split_def) }
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1010
  ultimately show ?case by blast
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
  1011
next
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1012
  case (12 j a) 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1013
  let ?c = "fst (zsplit0 a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1014
  let ?r = "snd (zsplit0 a)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1015
  have spl: "zsplit0 a = (?c,?r)" by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1016
  from zsplit0_I[OF spl, where x="i" and bs="bs"] 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1017
  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1018
  let ?N = "\<lambda> t. Inum (i#bs) t"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1019
  have "j=0 \<or> (j\<noteq>0 \<and> ?c = 0) \<or> (j\<noteq>0 \<and> ?c >0) \<or> (j\<noteq> 0 \<and> ?c<0)" by arith
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1020
  moreover
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1021
  {assume "j=0" hence z: "zlfm (NDvd j a) = (zlfm (NEq a))" by (simp add: Let_def) 
30042
31039ee583fa Removed subsumed lemmas
nipkow
parents: 29823
diff changeset
  1022
    hence ?case using prems by (simp del: zlfm.simps)}
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1023
  moreover
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1024
  {assume "?c=0" and "j\<noteq>0" hence ?case 
29700
22faf21db3df added some simp rules
nipkow
parents: 29667
diff changeset
  1025
      using zsplit0_I[OF spl, where x="i" and bs="bs"]
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29265
diff changeset
  1026
    apply (auto simp add: Let_def split_def algebra_simps) 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1027
    apply (cases "?r",auto)
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1028
    apply (case_tac nat, auto)
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1029
    done}
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1030
  moreover
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1031
  {assume cp: "?c > 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1032
      by (simp add: nb Let_def split_def)
29700
22faf21db3df added some simp rules
nipkow
parents: 29667
diff changeset
  1033
    hence ?case using Ia cp jnz by (simp add: Let_def split_def) }
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1034
  moreover
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1035
  {assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1036
      by (simp add: nb Let_def split_def)
30042
31039ee583fa Removed subsumed lemmas
nipkow
parents: 29823
diff changeset
  1037
    hence ?case using Ia cn jnz dvd_minus_iff[of "abs j" "?c*i + ?N ?r"]
29700
22faf21db3df added some simp rules
nipkow
parents: 29667
diff changeset
  1038
      by (simp add: Let_def split_def)}
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1039
  ultimately show ?case by blast
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1040
qed auto
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1041
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1042
consts 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1043
  plusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of +\<infinity>*)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1044
  minusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of -\<infinity>*)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1045
  \<delta> :: "fm \<Rightarrow> int" (* Compute lcm {d| N\<^isup>?\<^isup> Dvd c*x+t \<in> p}*)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1046
  d\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* checks if a given l divides all the ds above*)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1047
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1048
recdef minusinf "measure size"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1049
  "minusinf (And p q) = And (minusinf p) (minusinf q)" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1050
  "minusinf (Or p q) = Or (minusinf p) (minusinf q)" 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1051
  "minusinf (Eq  (CN 0 c e)) = F"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1052
  "minusinf (NEq (CN 0 c e)) = T"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1053
  "minusinf (Lt  (CN 0 c e)) = T"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1054
  "minusinf (Le  (CN 0 c e)) = T"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1055
  "minusinf (Gt  (CN 0 c e)) = F"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1056
  "minusinf (Ge  (CN 0 c e)) = F"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1057
  "minusinf p = p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1058
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1059
lemma minusinf_qfree: "qfree p \<Longrightarrow> qfree (minusinf p)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1060
  by (induct p rule: minusinf.induct, auto)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1061
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1062
recdef plusinf "measure size"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1063
  "plusinf (And p q) = And (plusinf p) (plusinf q)" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1064
  "plusinf (Or p q) = Or (plusinf p) (plusinf q)" 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1065
  "plusinf (Eq  (CN 0 c e)) = F"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1066
  "plusinf (NEq (CN 0 c e)) = T"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1067
  "plusinf (Lt  (CN 0 c e)) = F"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1068
  "plusinf (Le  (CN 0 c e)) = F"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1069
  "plusinf (Gt  (CN 0 c e)) = T"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1070
  "plusinf (Ge  (CN 0 c e)) = T"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1071
  "plusinf p = p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1072
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1073
recdef \<delta> "measure size"
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27456
diff changeset
  1074
  "\<delta> (And p q) = zlcm (\<delta> p) (\<delta> q)" 
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27456
diff changeset
  1075
  "\<delta> (Or p q) = zlcm (\<delta> p) (\<delta> q)" 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1076
  "\<delta> (Dvd i (CN 0 c e)) = i"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1077
  "\<delta> (NDvd i (CN 0 c e)) = i"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1078
  "\<delta> p = 1"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1079
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1080
recdef d\<delta> "measure size"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1081
  "d\<delta> (And p q) = (\<lambda> d. d\<delta> p d \<and> d\<delta> q d)" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1082
  "d\<delta> (Or p q) = (\<lambda> d. d\<delta> p d \<and> d\<delta> q d)" 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1083
  "d\<delta> (Dvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1084
  "d\<delta> (NDvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1085
  "d\<delta> p = (\<lambda> d. True)"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1086
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1087
lemma delta_mono: 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1088
  assumes lin: "iszlfm p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1089
  and d: "d dvd d'"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1090
  and ad: "d\<delta> p d"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1091
  shows "d\<delta> p d'"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1092
  using lin ad d
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1093
proof(induct p rule: iszlfm.induct)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1094
  case (9 i c e)  thus ?case using d
30042
31039ee583fa Removed subsumed lemmas
nipkow
parents: 29823
diff changeset
  1095
    by (simp add: dvd_trans[of "i" "d" "d'"])
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
  1096
next
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1097
  case (10 i c e) thus ?case using d
30042
31039ee583fa Removed subsumed lemmas
nipkow
parents: 29823
diff changeset
  1098
    by (simp add: dvd_trans[of "i" "d" "d'"])
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1099
qed simp_all
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
  1100
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1101
lemma \<delta> : assumes lin:"iszlfm p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1102
  shows "d\<delta> p (\<delta> p) \<and> \<delta> p >0"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1103
using lin
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1104
proof (induct p rule: iszlfm.induct)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1105
  case (1 p q) 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1106
  let ?d = "\<delta> (And p q)"
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27456
diff changeset
  1107
  from prems zlcm_pos have dp: "?d >0" by simp
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1108
  have d1: "\<delta> p dvd \<delta> (And p q)" using prems by simp
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27456
diff changeset
  1109
  hence th: "d\<delta> p ?d" using delta_mono prems(3-4) by(simp del:dvd_zlcm_self1)
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1110
  have "\<delta> q dvd \<delta> (And p q)" using prems by simp
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27456
diff changeset
  1111
  hence th': "d\<delta> q ?d" using delta_mono prems by(simp del:dvd_zlcm_self2)
23984
aaff3bc5ec28 fixed broken proof
nipkow
parents: 23854
diff changeset
  1112
  from th th' dp show ?case by simp
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1113
next
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1114
  case (2 p q)  
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1115
  let ?d = "\<delta> (And p q)"
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27456
diff changeset
  1116
  from prems zlcm_pos have dp: "?d >0" by simp
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1117
  have "\<delta> p dvd \<delta> (And p q)" using prems by simp
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27456
diff changeset
  1118
  hence th: "d\<delta> p ?d" using delta_mono prems by(simp del:dvd_zlcm_self1)
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1119
  have "\<delta> q dvd \<delta> (And p q)" using prems by simp
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27456
diff changeset
  1120
  hence th': "d\<delta> q ?d" using delta_mono prems by(simp del:dvd_zlcm_self2)
23984
aaff3bc5ec28 fixed broken proof
nipkow
parents: 23854
diff changeset
  1121
  from th th' dp show ?case by simp
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
  1122
qed simp_all
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
  1123
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
  1124
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1125
consts 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1126
  a\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" (* adjusts the coeffitients of a formula *)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1127
  d\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* tests if all coeffs c of c divide a given l*)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1128
  \<zeta>  :: "fm \<Rightarrow> int" (* computes the lcm of all coefficients of x*)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1129
  \<beta> :: "fm \<Rightarrow> num list"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1130
  \<alpha> :: "fm \<Rightarrow> num list"
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
  1131
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1132
recdef a\<beta> "measure size"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1133
  "a\<beta> (And p q) = (\<lambda> k. And (a\<beta> p k) (a\<beta> q k))" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1134
  "a\<beta> (Or p q) = (\<lambda> k. Or (a\<beta> p k) (a\<beta> q k))" 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1135
  "a\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. Eq (CN 0 1 (Mul (k div c) e)))"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1136
  "a\<beta> (NEq (CN 0 c e)) = (\<lambda> k. NEq (CN 0 1 (Mul (k div c) e)))"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1137
  "a\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. Lt (CN 0 1 (Mul (k div c) e)))"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1138
  "a\<beta> (Le  (CN 0 c e)) = (\<lambda> k. Le (CN 0 1 (Mul (k div c) e)))"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1139
  "a\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. Gt (CN 0 1 (Mul (k div c) e)))"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1140
  "a\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. Ge (CN 0 1 (Mul (k div c) e)))"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1141
  "a\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1142
  "a\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1143
  "a\<beta> p = (\<lambda> k. p)"
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
  1144
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1145
recdef d\<beta> "measure size"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1146
  "d\<beta> (And p q) = (\<lambda> k. (d\<beta> p k) \<and> (d\<beta> q k))" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1147
  "d\<beta> (Or p q) = (\<lambda> k. (d\<beta> p k) \<and> (d\<beta> q k))" 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1148
  "d\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. c dvd k)"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1149
  "d\<beta> (NEq (CN 0 c e)) = (\<lambda> k. c dvd k)"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1150
  "d\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1151
  "d\<beta> (Le  (CN 0 c e)) = (\<lambda> k. c dvd k)"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1152
  "d\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1153
  "d\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. c dvd k)"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1154
  "d\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. c dvd k)"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1155
  "d\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. c dvd k)"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1156
  "d\<beta> p = (\<lambda> k. True)"
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
  1157
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1158
recdef \<zeta> "measure size"
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27456
diff changeset
  1159
  "\<zeta> (And p q) = zlcm (\<zeta> p) (\<zeta> q)" 
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27456
diff changeset
  1160
  "\<zeta> (Or p q) = zlcm (\<zeta> p) (\<zeta> q)" 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1161
  "\<zeta> (Eq  (CN 0 c e)) = c"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1162
  "\<zeta> (NEq (CN 0 c e)) = c"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1163
  "\<zeta> (Lt  (CN 0 c e)) = c"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1164
  "\<zeta> (Le  (CN 0 c e)) = c"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1165
  "\<zeta> (Gt  (CN 0 c e)) = c"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1166
  "\<zeta> (Ge  (CN 0 c e)) = c"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1167
  "\<zeta> (Dvd i (CN 0 c e)) = c"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1168
  "\<zeta> (NDvd i (CN 0 c e))= c"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1169
  "\<zeta> p = 1"
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
  1170
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1171
recdef \<beta> "measure size"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1172
  "\<beta> (And p q) = (\<beta> p @ \<beta> q)" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1173
  "\<beta> (Or p q) = (\<beta> p @ \<beta> q)" 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1174
  "\<beta> (Eq  (CN 0 c e)) = [Sub (C -1) e]"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1175
  "\<beta> (NEq (CN 0 c e)) = [Neg e]"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1176
  "\<beta> (Lt  (CN 0 c e)) = []"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1177
  "\<beta> (Le  (CN 0 c e)) = []"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1178
  "\<beta> (Gt  (CN 0 c e)) = [Neg e]"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1179
  "\<beta> (Ge  (CN 0 c e)) = [Sub (C -1) e]"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1180
  "\<beta> p = []"
19736
wenzelm
parents: 19623
diff changeset
  1181
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1182
recdef \<alpha> "measure size"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1183
  "\<alpha> (And p q) = (\<alpha> p @ \<alpha> q)" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1184
  "\<alpha> (Or p q) = (\<alpha> p @ \<alpha> q)" 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1185
  "\<alpha> (Eq  (CN 0 c e)) = [Add (C -1) e]"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1186
  "\<alpha> (NEq (CN 0 c e)) = [e]"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1187
  "\<alpha> (Lt  (CN 0 c e)) = [e]"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1188
  "\<alpha> (Le  (CN 0 c e)) = [Add (C -1) e]"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1189
  "\<alpha> (Gt  (CN 0 c e)) = []"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1190
  "\<alpha> (Ge  (CN 0 c e)) = []"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1191
  "\<alpha> p = []"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1192
consts mirror :: "fm \<Rightarrow> fm"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1193
recdef mirror "measure size"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1194
  "mirror (And p q) = And (mirror p) (mirror q)" 
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1195
  "mirror (Or p q) = Or (mirror p) (mirror q)" 
23995
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1196
  "mirror (Eq  (CN 0 c e)) = Eq (CN 0 c (Neg e))"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1197
  "mirror (NEq (CN 0 c e)) = NEq (CN 0 c (Neg e))"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1198
  "mirror (Lt  (CN 0 c e)) = Gt (CN 0 c (Neg e))"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1199
  "mirror (Le  (CN 0 c e)) = Ge (CN 0 c (Neg e))"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1200
  "mirror (Gt  (CN 0 c e)) = Lt (CN 0 c (Neg e))"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1201
  "mirror (Ge  (CN 0 c e)) = Le (CN 0 c (Neg e))"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1202
  "mirror (Dvd i (CN 0 c e)) = Dvd i (CN 0 c (Neg e))"
c34490f1e0ff Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents: 23984
diff changeset
  1203
  "mirror (NDvd i (CN 0 c e)) = NDvd i (CN 0 c (Neg e))"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1204
  "mirror p = p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1205
    (* Lemmas for the correctness of \<sigma>\<rho> *)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1206
lemma dvd1_eq1: "x >0 \<Longrightarrow> (x::int) dvd 1 = (x = 1)"
29700
22faf21db3df added some simp rules
nipkow
parents: 29667
diff changeset
  1207
by simp
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
  1208
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1209
lemma minusinf_inf:
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1210
  assumes linp: "iszlfm p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1211
  and u: "d\<beta> p 1"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1212
  shows "\<exists> (z::int). \<forall> x < z. Ifm bbs (x#bs) (minusinf p) = Ifm bbs (x#bs) p"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1213
  (is "?P p" is "\<exists> (z::int). \<forall> x < z. ?I x (?M p) = ?I x p")
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1214
using linp u
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1215
proof (induct p rule: minusinf.induct)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1216
  case (1 p q) thus ?case 
29700
22faf21db3df added some simp rules
nipkow
parents: 29667
diff changeset
  1217
    by auto (rule_tac x="min z za" in exI,simp)
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1218
next
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1219
  case (2 p q) thus ?case 
29700
22faf21db3df added some simp rules
nipkow
parents: 29667
diff changeset
  1220
    by auto (rule_tac x="min z za" in exI,simp)
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
  1221
next
29700
22faf21db3df added some simp rules
nipkow
parents: 29667
diff changeset
  1222
  case (3 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
26934
c1ae80a58341 avoid undeclared variables within proofs;
wenzelm
parents: 25592
diff changeset
  1223
  fix a
c1ae80a58341 avoid undeclared variables within proofs;
wenzelm
parents: 25592
diff changeset
  1224
  from 3 have "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<noteq> 0"
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1225
  proof(clarsimp)
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1226
    fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e = 0"
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1227
    with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1228
    show "False" by simp
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1229
  qed
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 21404
diff changeset
  1230
  thus ?case by auto
17378
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff changeset
  1231
next
29700
22faf21db3df added some simp rules
nipkow
parents: 29667
diff changeset
  1232
  case (4 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
26934
c1ae80a58341 avoid undeclared variables within proofs;
wenzelm
parents: 25592
diff changeset
  1233
  fix a
c1ae80a58341 avoid undeclared variables within proofs;
wenzelm
parents: 25592
diff changeset
  1234</