(* Title: HOL/ex/PresburgerEx.thy
ID: $Id$
Author: Amine Chaieb, TU Muenchen
A formalization of quantifier elimination for Presburger arithmetic
based on a generic quantifier elimination algorithm and Cooper's
method to eliminate on \<exists>. *)
header {* Quantifier elimination for Presburger arithmetic *}
theory Reflected_Presburger
imports Main GCD
begin
(* Shadow syntax for integer terms *)
datatype intterm =
Cst int
| Var nat
| Neg intterm
| Add intterm intterm
| Sub intterm intterm
| Mult intterm intterm
(* interpretation of intterms, takes bound variables and free variables *)
consts I_intterm :: "int list \<Rightarrow> intterm \<Rightarrow> int"
primrec
"I_intterm ats (Cst b) = b"
"I_intterm ats (Var n) = (ats!n)"
"I_intterm ats (Neg it) = -(I_intterm ats it)"
"I_intterm ats (Add it1 it2) = (I_intterm ats it1) + (I_intterm ats it2)"
"I_intterm ats (Sub it1 it2) = (I_intterm ats it1) - (I_intterm ats it2)"
"I_intterm ats (Mult it1 it2) = (I_intterm ats it1) * (I_intterm ats it2)"
(* Shadow syntax for Presburger formulae *)
datatype QF =
Lt intterm intterm
|Gt intterm intterm
|Le intterm intterm
|Ge intterm intterm
|Eq intterm intterm
|Divides intterm intterm
|T
|F
|NOT QF
|And QF QF
|Or QF QF
|Imp QF QF
|Equ QF QF
|QAll QF
|QEx QF
(* Interpretation of Presburger formulae *)
consts qinterp :: "int list \<Rightarrow> QF \<Rightarrow> bool"
primrec
"qinterp ats (Lt it1 it2) = (I_intterm ats it1 < I_intterm ats it2)"
"qinterp ats (Gt it1 it2) = (I_intterm ats it1 > I_intterm ats it2)"
"qinterp ats (Le it1 it2) = (I_intterm ats it1 \<le> I_intterm ats it2)"
"qinterp ats (Ge it1 it2) = (I_intterm ats it1 \<ge> I_intterm ats it2)"
"qinterp ats (Divides it1 it2) = (I_intterm ats it1 dvd I_intterm ats it2)"
"qinterp ats (Eq it1 it2) = (I_intterm ats it1 = I_intterm ats it2)"
"qinterp ats T = True"
"qinterp ats F = False"
"qinterp ats (NOT p) = (\<not>(qinterp ats p))"
"qinterp ats (And p q) = (qinterp ats p \<and> qinterp ats q)"
"qinterp ats (Or p q) = (qinterp ats p \<or> qinterp ats q)"
"qinterp ats (Imp p q) = (qinterp ats p \<longrightarrow> qinterp ats q)"
"qinterp ats (Equ p q) = (qinterp ats p = qinterp ats q)"
"qinterp ats (QAll p) = (\<forall>x. qinterp (x#ats) p)"
"qinterp ats (QEx p) = (\<exists>x. qinterp (x#ats) p)"
(* quantifier elimination based on qe, quantifier elimination for an
existential formula, with quantifier free body
Since quantifier elimination for one formula is allowed to fail,
the result is of type QF option *)
consts lift_bin:: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<times> 'a option \<times> 'a option \<Rightarrow> 'b option"
recdef lift_bin "measure (\<lambda>(c,a,b). size a)"
"lift_bin (c,Some a,Some b) = Some (c a b)"
"lift_bin (c,x, y) = None"
lemma lift_bin_Some:
assumes ls: "lift_bin (c,x,y) = Some t"
shows "(\<exists>a. x = Some a) \<and> (\<exists>b. y = Some b)"
using ls
by (cases "x", auto) (cases "y", auto)+
consts lift_un:: "('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"
primrec
"lift_un c None = None"
"lift_un c (Some p) = Some (c p)"
consts lift_qe:: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a option \<Rightarrow> 'b option"
primrec
"lift_qe qe None = None"
"lift_qe qe (Some p) = qe p"
(* generic quantifier elimination *)
consts qelim :: "(QF \<Rightarrow> QF option) \<times> QF \<Rightarrow> QF option"
recdef qelim "measure (\<lambda>(qe,p). size p)"
"qelim (qe, (QAll p)) = lift_un NOT (lift_qe qe (lift_un NOT (qelim (qe ,p))))"
"qelim (qe, (QEx p)) = lift_qe qe (qelim (qe,p))"
"qelim (qe, (And p q)) = lift_bin (And, (qelim (qe, p)), (qelim (qe, q)))"
"qelim (qe, (Or p q)) = lift_bin (Or, (qelim (qe, p)), (qelim (qe, q)))"
"qelim (qe, (Imp p q)) = lift_bin (Imp, (qelim (qe, p)), (qelim (qe, q)))"
"qelim (qe, (Equ p q)) = lift_bin (Equ, (qelim (qe, p)), (qelim (qe, q)))"
"qelim (qe,NOT p) = lift_un NOT (qelim (qe,p))"
"qelim (qe, p) = Some p"
(* quantifier free-ness *)
consts isqfree :: "QF \<Rightarrow> bool"
recdef isqfree "measure size"
"isqfree (QAll p) = False"
"isqfree (QEx p) = False"
"isqfree (And p q) = (isqfree p \<and> isqfree q)"
"isqfree (Or p q) = (isqfree p \<and> isqfree q)"
"isqfree (Imp p q) = (isqfree p \<and> isqfree q)"
"isqfree (Equ p q) = (isqfree p \<and> isqfree q)"
"isqfree (NOT p) = isqfree p"
"isqfree p = True"
(* qelim lifts quantifierfreeness*)
lemma qelim_qfree:
assumes qeqf: "(\<And> q q'. \<lbrakk>isqfree q ; qe q = Some q'\<rbrakk> \<Longrightarrow> isqfree q')"
shows qff:"\<And> p'. qelim (qe, p) = Some p' \<Longrightarrow> isqfree p'"
using qeqf
proof (induct p)
case (Lt a b)
have "qelim (qe, Lt a b) = Some (Lt a b)" by simp
moreover have "qelim (qe,Lt a b) = Some p'" .
ultimately have "p' = Lt a b" by simp
moreover have "isqfree (Lt a b)" by simp
ultimately
show ?case by simp
next
case (Gt a b)
have "qelim (qe, Gt a b) = Some (Gt a b)" by simp
moreover have "qelim (qe,Gt a b) = Some p'" .
ultimately have "p' = Gt a b" by simp
moreover have "isqfree (Gt a b)" by simp
ultimately
show ?case by simp
next
case (Le a b)
have "qelim (qe, Le a b) = Some (Le a b)" by simp
moreover have "qelim (qe,Le a b) = Some p'" .
ultimately have "p' = Le a b" by simp
moreover have "isqfree (Le a b)" by simp
ultimately
show ?case by simp
next
case (Ge a b)
have "qelim (qe, Ge a b) = Some (Ge a b)" by simp
moreover have "qelim (qe,Ge a b) = Some p'" .
ultimately have "p' = Ge a b" by simp
moreover have "isqfree (Ge a b)" by simp
ultimately
show ?case by simp
next
case (Eq a b)
have "qelim (qe, Eq a b) = Some (Eq a b)" by simp
moreover have "qelim (qe,Eq a b) = Some p'" .
ultimately have "p' = Eq a b" by simp
moreover have "isqfree (Eq a b)" by simp
ultimately
show ?case by simp
next
case (Divides a b)
have "qelim (qe, Divides a b) = Some (Divides a b)" by simp
moreover have "qelim (qe,Divides a b) = Some p'" .
ultimately have "p' = Divides a b" by simp
moreover have "isqfree (Divides a b)" by simp
ultimately
show ?case by simp
next
case T
have "qelim(qe,T) = Some T" by simp
moreover have "qelim(qe,T) = Some p'" .
ultimately have "p' = T" by simp
moreover have "isqfree T" by simp
ultimately show ?case by simp
next
case F
have "qelim(qe,F) = Some F" by simp
moreover have "qelim(qe,F) = Some p'" .
ultimately have "p' = F" by simp
moreover have "isqfree F" by simp
ultimately show ?case by simp
next
case (NOT p)
from "NOT.prems" have "\<exists> p1. qelim(qe,p) = Some p1"
by (cases "qelim(qe,p)") simp_all
then obtain "p1" where p1_def: "qelim(qe,p) = Some p1" by blast
from "NOT.prems" have "\<And>q q'. \<lbrakk>isqfree q; qe q = Some q'\<rbrakk> \<Longrightarrow> isqfree q'"
by blast
with "NOT.hyps" p1_def have p1qf: "isqfree p1" by blast
then have "p' = NOT p1" using "NOT.prems" p1_def
by (cases "qelim(qe,NOT p)") simp_all
then show ?case using p1qf by simp
next
case (And p q)
from "And.prems" have p1q1: "(\<exists>p1. qelim(qe,p) = Some p1) \<and>
(\<exists>q1. qelim(qe,q) = Some q1)" using lift_bin_Some[where c="And"] by simp
from p1q1 obtain "p1" and "q1"
where p1_def: "qelim(qe,p) = Some p1"
and q1_def: "qelim(qe,q) = Some q1" by blast
from prems have qf1:"isqfree p1"
using p1_def by blast
from prems have qf2:"isqfree q1"
using q1_def by blast
from "And.prems" have "qelim(qe,And p q) = Some p'" by blast
then have "p' = And p1 q1" using p1_def q1_def by simp
then
show ?case using qf1 qf2 by simp
next
case (Or p q)
from "Or.prems" have p1q1: "(\<exists>p1. qelim(qe,p) = Some p1) \<and>
(\<exists>q1. qelim(qe,q) = Some q1)" using lift_bin_Some[where c="Or"] by simp
from p1q1 obtain "p1" and "q1"
where p1_def: "qelim(qe,p) = Some p1"
and q1_def: "qelim(qe,q) = Some q1" by blast
from prems have qf1:"isqfree p1"
using p1_def by blast
from prems have qf2:"isqfree q1"
using q1_def by blast
from "Or.prems" have "qelim(qe,Or p q) = Some p'" by blast
then have "p' = Or p1 q1" using p1_def q1_def by simp
then
show ?case using qf1 qf2 by simp
next
case (Imp p q)
from "Imp.prems" have p1q1: "(\<exists>p1. qelim(qe,p) = Some p1) \<and>
(\<exists>q1. qelim(qe,q) = Some q1)" using lift_bin_Some[where c="Imp"] by simp
from p1q1 obtain "p1" and "q1"
where p1_def: "qelim(qe,p) = Some p1"
and q1_def: "qelim(qe,q) = Some q1" by blast
from prems have qf1:"isqfree p1"
using p1_def by blast
from prems have qf2:"isqfree q1"
using q1_def by blast
from "Imp.prems" have "qelim(qe,Imp p q) = Some p'" by blast
then have "p' = Imp p1 q1" using p1_def q1_def by simp
then
show ?case using qf1 qf2 by simp
next
case (Equ p q)
from "Equ.prems" have p1q1: "(\<exists>p1. qelim(qe,p) = Some p1) \<and>
(\<exists>q1. qelim(qe,q) = Some q1)" using lift_bin_Some[where c="Equ"] by simp
from p1q1 obtain "p1" and "q1"
where p1_def: "qelim(qe,p) = Some p1"
and q1_def: "qelim(qe,q) = Some q1" by blast
from prems have qf1:"isqfree p1"
using p1_def by blast
from prems have qf2:"isqfree q1"
using q1_def by blast
from "Equ.prems" have "qelim(qe,Equ p q) = Some p'" by blast
then have "p' = Equ p1 q1" using p1_def q1_def by simp
then
show ?case using qf1 qf2 by simp
next
case (QEx p)
from "QEx.prems" have "\<exists> p1. qelim(qe,p) = Some p1"
by (cases "qelim(qe,p)") simp_all
then obtain "p1" where p1_def: "qelim(qe,p) = Some p1" by blast
from "QEx.prems" have "\<And>q q'. \<lbrakk>isqfree q; qe q = Some q'\<rbrakk> \<Longrightarrow> isqfree q'"
by blast
with "QEx.hyps" p1_def have p1qf: "isqfree p1" by blast
from "QEx.prems" have "qe p1 = Some p'" using p1_def by simp
with "QEx.prems" show ?case using p1qf
by simp
next
case (QAll p)
from "QAll.prems"
have "\<exists> p1. lift_qe qe (lift_un NOT (qelim (qe ,p))) = Some p1"
by (cases "lift_qe qe (lift_un NOT (qelim (qe ,p)))") simp_all
then obtain "p1" where
p1_def:"lift_qe qe (lift_un NOT (qelim (qe ,p))) = Some p1" by blast
then have "\<exists> p2. lift_un NOT (qelim (qe ,p)) = Some p2"
by (cases "qelim (qe ,p)") simp_all
then obtain "p2"
where p2_def:"lift_un NOT (qelim (qe ,p)) = Some p2" by blast
then have "\<exists> p3. qelim(qe,p) = Some p3" by (cases "qelim(qe,p)") simp_all
then obtain "p3" where p3_def: "qelim(qe,p) = Some p3" by blast
with prems have qf3: "isqfree p3" by blast
have p2_def2: "p2 = NOT p3" using p2_def p3_def by simp
then have qf2: "isqfree p2" using qf3 by simp
have p1_edf2: "qe p2 = Some p1" using p1_def p2_def by simp
with "QAll.prems" have qf1: "isqfree p1" using qf2 by blast
from "QAll.prems" have "p' = NOT p1" using p1_def by simp
with qf1 show ?case by simp
qed
(* qelim lifts semantical equivalence *)
lemma qelim_corr:
assumes qecorr: "(\<And> q q' ats. \<lbrakk>isqfree q ; qe q = Some q'\<rbrakk> \<Longrightarrow> (qinterp ats (QEx q)) = (qinterp ats q'))"
and qeqf: "(\<And> q q'. \<lbrakk>isqfree q ; qe q = Some q'\<rbrakk> \<Longrightarrow> isqfree q')"
shows qff:"\<And> p' ats. qelim (qe, p) = Some p' \<Longrightarrow> (qinterp ats p = qinterp ats p')" (is "\<And> p' ats. ?Qe p p' \<Longrightarrow> (?F ats p = ?F ats p')")
using qeqf qecorr
proof (induct p)
case (NOT f)
from "NOT.prems" have "\<exists>f'. ?Qe f f' " by (cases "qelim(qe,f)") simp_all
then obtain "f'" where df': "?Qe f f'" by blast
with prems have feqf': "?F ats f = ?F ats f'" by blast
from "NOT.prems" df' have "p' = NOT f'" by simp
with feqf' show ?case by simp
next
case (And f g)
from "And.prems" have f1g1: "(\<exists>f1. qelim(qe,f) = Some f1) \<and>
(\<exists>g1. qelim(qe,g) = Some g1)" using lift_bin_Some[where c="And"] by simp
from f1g1 obtain "f1" and "g1"
where f1_def: "qelim(qe, f) = Some f1"
and g1_def: "qelim(qe,g) = Some g1" by blast
from prems f1_def have feqf1: "?F ats f = ?F ats f1" by blast
from prems g1_def have geqg1: "?F ats g = ?F ats g1" by blast
from "And.prems" f1_def g1_def have "p' = And f1 g1" by simp
with feqf1 geqg1 show ?case by simp
next
case (Or f g)
from "Or.prems" have f1g1: "(\<exists>f1. qelim(qe,f) = Some f1) \<and>
(\<exists>g1. qelim(qe,g) = Some g1)" using lift_bin_Some[where c="Or"] by simp
from f1g1 obtain "f1" and "g1"
where f1_def: "qelim(qe, f) = Some f1"
and g1_def: "qelim(qe,g) = Some g1" by blast
from prems f1_def have feqf1: "?F ats f = ?F ats f1" by blast
from prems g1_def have geqg1: "?F ats g = ?F ats g1" by blast
from "Or.prems" f1_def g1_def have "p' = Or f1 g1" by simp
with feqf1 geqg1 show ?case by simp
next
case (Imp f g)
from "Imp.prems" have f1g1: "(\<exists>f1. qelim(qe,f) = Some f1) \<and>
(\<exists>g1. qelim(qe,g) = Some g1)" using lift_bin_Some[where c="Imp"] by simp
from f1g1 obtain "f1" and "g1"
where f1_def: "qelim(qe, f) = Some f1"
and g1_def: "qelim(qe,g) = Some g1" by blast
from prems f1_def have feqf1: "?F ats f = ?F ats f1" by blast
from prems g1_def have geqg1: "?F ats g = ?F ats g1" by blast
from "Imp.prems" f1_def g1_def have "p' = Imp f1 g1" by simp
with feqf1 geqg1 show ?case by simp
next
case (Equ f g)
from "Equ.prems" have f1g1: "(\<exists>f1. qelim(qe,f) = Some f1) \<and>
(\<exists>g1. qelim(qe,g) = Some g1)" using lift_bin_Some[where c="Equ"] by simp
from f1g1 obtain "f1" and "g1"
where f1_def: "qelim(qe, f) = Some f1"
and g1_def: "qelim(qe,g) = Some g1" by blast
from prems f1_def have feqf1: "?F ats f = ?F ats f1" by blast
from prems g1_def have geqg1: "?F ats g = ?F ats g1" by blast
from "Equ.prems" f1_def g1_def have "p' = Equ f1 g1" by simp
with feqf1 geqg1 show ?case by simp
next
case (QEx f)
from "QEx.prems" have "\<exists> f1. ?Qe f f1"
by (cases "qelim(qe,f)") simp_all
then obtain "f1" where f1_def: "qelim(qe,f) = Some f1" by blast
from prems have qf1:"isqfree f1" using qelim_qfree by blast
from prems have feqf1: "\<forall> ats. qinterp ats f = qinterp ats f1"
using f1_def qf1 by blast
then have "?F ats (QEx f) = ?F ats (QEx f1)"
by simp
from prems have "qelim (qe,QEx f) = Some p'" by blast
then have "\<exists> f'. qe f1 = Some f'" using f1_def by simp
then obtain "f'" where fdef': "qe f1 = Some f'" by blast
with prems have exf1: "?F ats (QEx f1) = ?F ats f'" using qf1 by blast
have fp: "?Qe (QEx f) f'" using f1_def fdef' by simp
from prems have "?Qe (QEx f) p'" by blast
then have "p' = f'" using fp by simp
then show ?case using feqf1 exf1 by simp
next
case (QAll f)
from "QAll.prems"
have "\<exists> f0. lift_un NOT (lift_qe qe (lift_un NOT (qelim (qe ,f)))) =
Some f0"
by (cases "lift_un NOT (lift_qe qe (lift_un NOT (qelim (qe ,f))))")
simp_all
then obtain "f0"
where f0_def: "lift_un NOT (lift_qe qe (lift_un NOT (qelim (qe ,f)))) =
Some f0" by blast
then have "\<exists> f1. lift_qe qe (lift_un NOT (qelim (qe ,f))) = Some f1"
by (cases "lift_qe qe (lift_un NOT (qelim (qe ,f)))") simp_all
then obtain "f1" where
f1_def:"lift_qe qe (lift_un NOT (qelim (qe ,f))) = Some f1" by blast
then have "\<exists> f2. lift_un NOT (qelim (qe ,f)) = Some f2"
by (cases "qelim (qe ,f)") simp_all
then obtain "f2"
where f2_def:"lift_un NOT (qelim (qe ,f)) = Some f2" by blast
then have "\<exists> f3. qelim(qe,f) = Some f3" by (cases "qelim(qe,f)") simp_all
then obtain "f3" where f3_def: "qelim(qe,f) = Some f3" by blast
from prems have qf3:"isqfree f3" using qelim_qfree by blast
from prems have feqf3: "\<forall> ats. qinterp ats f = qinterp ats f3"
using f3_def qf3 by blast
have f23:"f2 = NOT f3" using f2_def f3_def by simp
then have feqf2: "\<forall> ats. qinterp ats f = qinterp ats (NOT f2)"
using feqf3 by simp
have qf2: "isqfree f2" using f23 qf3 by simp
have "qe f2 = Some f1" using f1_def f2_def f23 by simp
with prems have exf2eqf1: "?F ats (QEx f2) = ?F ats f1" using qf2 by blast
have "f0 = NOT f1" using f0_def f1_def by simp
then have f0eqf1: "?F ats f0 = ?F ats (NOT f1)" by simp
from prems have "qelim (qe, QAll f) = Some p'" by blast
then have f0eqp': "p' = f0" using f0_def by simp
have "?F ats (QAll f) = (\<forall>x. ?F (x#ats) f)" by simp
also have "\<dots> = (\<not> (\<exists> x. ?F (x#ats) (NOT f)))" by simp
also have "\<dots> = (\<not> (\<exists> x. ?F (x#ats) (NOT (NOT f2))))" using feqf2
by auto
also have "\<dots> = (\<not> (\<exists> x. ?F (x#ats) f2))" by simp
also have "\<dots> = (\<not> (?F ats f1))" using exf2eqf1 by simp
finally show ?case using f0eqp' f0eqf1 by simp
qed simp_all
(* Cooper's algorithm *)
(* Transform an intform into NNF *)
consts lgth :: "QF \<Rightarrow> nat"
nnf :: "QF \<Rightarrow> QF"
primrec
"lgth (Lt it1 it2) = 1"
"lgth (Gt it1 it2) = 1"
"lgth (Le it1 it2) = 1"
"lgth (Ge it1 it2) = 1"
"lgth (Eq it1 it2) = 1"
"lgth (Divides it1 it2) = 1"
"lgth T = 1"
"lgth F = 1"
"lgth (NOT p) = 1 + lgth p"
"lgth (And p q) = 1 + lgth p + lgth q"
"lgth (Or p q) = 1 + lgth p + lgth q"
"lgth (Imp p q) = 1 + lgth p + lgth q"
"lgth (Equ p q) = 1 + lgth p + lgth q"
"lgth (QAll p) = 1 + lgth p"
"lgth (QEx p) = 1 + lgth p"
lemma [simp] :"0 < lgth q"
apply (induct_tac q)
apply(auto)
done
(* NNF *)
recdef nnf "measure (\<lambda>p. lgth p)"
"nnf (Lt it1 it2) = Le (Sub it1 it2) (Cst (- 1))"
"nnf (Gt it1 it2) = Le (Sub it2 it1) (Cst (- 1))"
"nnf (Le it1 it2) = Le it1 it2 "
"nnf (Ge it1 it2) = Le it2 it1"
"nnf (Eq it1 it2) = Eq it2 it1"
"nnf (Divides d t) = Divides d t"
"nnf T = T"
"nnf F = F"
"nnf (And p q) = And (nnf p) (nnf q)"
"nnf (Or p q) = Or (nnf p) (nnf q)"
"nnf (Imp p q) = Or (nnf (NOT p)) (nnf q)"
"nnf (Equ p q) = Or (And (nnf p) (nnf q))
(And (nnf (NOT p)) (nnf (NOT q)))"
"nnf (NOT (Lt it1 it2)) = (Le it2 it1)"
"nnf (NOT (Gt it1 it2)) = (Le it1 it2)"
"nnf (NOT (Le it1 it2)) = (Le (Sub it2 it1) (Cst (- 1)))"
"nnf (NOT (Ge it1 it2)) = (Le (Sub it1 it2) (Cst (- 1)))"
"nnf (NOT (Eq it1 it2)) = (NOT (Eq it1 it2))"
"nnf (NOT (Divides d t)) = (NOT (Divides d t))"
"nnf (NOT T) = F"
"nnf (NOT F) = T"
"nnf (NOT (NOT p)) = (nnf p)"
"nnf (NOT (And p q)) = (Or (nnf (NOT p)) (nnf (NOT q)))"
"nnf (NOT (Or p q)) = (And (nnf (NOT p)) (nnf (NOT q)))"
"nnf (NOT (Imp p q)) = (And (nnf p) (nnf (NOT q)))"
"nnf (NOT (Equ p q)) = (Or (And (nnf p) (nnf (NOT q))) (And (nnf (NOT p)) (nnf q)))"
consts isnnf :: "QF \<Rightarrow> bool"
recdef isnnf "measure (\<lambda>p. lgth p)"
"isnnf (Le it1 it2) = True"
"isnnf (Eq it1 it2) = True"
"isnnf (Divides d t) = True"
"isnnf T = True"
"isnnf F = True"
"isnnf (And p q) = (isnnf p \<and> isnnf q)"
"isnnf (Or p q) = (isnnf p \<and> isnnf q)"
"isnnf (NOT (Divides d t)) = True"
"isnnf (NOT (Eq it1 it2)) = True"
"isnnf p = False"
(* nnf preserves semantics *)
lemma nnf_corr: "isqfree p \<Longrightarrow> qinterp ats p = qinterp ats (nnf p)"
by (induct p rule: nnf.induct,simp_all)
(arith, arith, arith, arith, arith, arith, arith, arith, arith, blast)
(* the result of nnf is in NNF *)
lemma nnf_isnnf : "isqfree p \<Longrightarrow> isnnf (nnf p)"
by (induct p rule: nnf.induct, auto)
lemma nnf_isqfree: "isnnf p \<Longrightarrow> isqfree p"
by (induct p rule: isnnf.induct) auto
(* nnf preserves quantifier freeness *)
lemma nnf_qfree: "isqfree p \<Longrightarrow> isqfree(nnf p)"
using nnf_isqfree nnf_isnnf by simp
(* Linearization and normalization of formulae *)
(* Definition of linearity of an intterm *)
consts islinintterm :: "intterm \<Rightarrow> bool"
recdef islinintterm "measure size"
"islinintterm (Cst i) = True"
"islinintterm (Add (Mult (Cst i) (Var n)) (Cst i')) = (i \<noteq> 0)"
"islinintterm (Add (Mult (Cst i) (Var n)) (Add (Mult (Cst i') (Var n')) r)) = ( i \<noteq> 0 \<and> i' \<noteq> 0 \<and> n < n' \<and> islinintterm (Add (Mult (Cst i') (Var n')) r))"
"islinintterm i = False"
(* subterms of linear terms are linear *)
lemma islinintterm_subt:
assumes lr: "islinintterm (Add (Mult (Cst i) (Var n)) r)"
shows "islinintterm r"
using lr
by (induct r rule: islinintterm.induct) auto
(* c \<noteq> 0 for linear term c.n + r*)
lemma islinintterm_cnz:
assumes lr: "islinintterm (Add (Mult (Cst i) (Var n)) r)"
shows "i \<noteq> 0"
using lr
by (induct r rule: islinintterm.induct) auto
lemma islininttermc0r: "islinintterm (Add (Mult (Cst c) (Var n)) r) \<Longrightarrow> (c \<noteq> 0 \<and> islinintterm r)"
by (induct r rule: islinintterm.induct, simp_all)
(* An alternative linearity definition *)
consts islintn :: "(nat \<times> intterm) \<Rightarrow> bool"
recdef islintn "measure (\<lambda> (n,t). (size t))"
"islintn (n0, Cst i) = True"
"islintn (n0, Add (Mult (Cst i) (Var n)) r) = (i \<noteq> 0 \<and> n0 \<le> n \<and> islintn (n+1,r))"
"islintn (n0, t) = False"
definition
islint :: "intterm \<Rightarrow> bool"
"islint t = islintn(0,t)"
(* And the equivalence to the first definition *)
lemma islinintterm_eq_islint: "islinintterm t = islint t"
using islint_def
by (induct t rule: islinintterm.induct) auto
(* monotony *)
lemma islintn_mon:
assumes lin: "islintn (n,t)"
and mgen: "m \<le> n"
shows "islintn(m,t)"
using lin mgen
by (induct t rule: islintn.induct) auto
lemma islintn_subt:
assumes lint: "islintn(n,Add (Mult (Cst i) (Var m)) r)"
shows "islintn (m+1,r)"
using lint
by auto
(* List indexin for n > 0 *)
lemma nth_pos: "0 < n \<longrightarrow> (x#xs) ! n = (y#xs) ! n"
using Nat.gr0_conv_Suc
by clarsimp
lemma nth_pos2: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"
using Nat.gr0_conv_Suc
by clarsimp
lemma intterm_novar0:
assumes lin: "islinintterm (Add (Mult (Cst i) (Var n)) r)"
shows "I_intterm (x#ats) r = I_intterm (y#ats) r"
using lin
by (induct r rule: islinintterm.induct) (simp_all add: nth_pos2)
(* a simple version of a general theorem: Interpretation does not depend
on the first variable if it does not occur in the term *)
lemma linterm_novar0:
assumes lin: "islintn (n,t)"
and npos: "0 < n"
shows "I_intterm (x#ats) t = I_intterm (y#ats) t"
using lin npos
by (induct n t rule: islintn.induct) (simp_all add: nth_pos2)
(* Periodicity of dvd *)
lemma dvd_period:
assumes advdd: "(a::int) dvd d"
shows "(a dvd (x + t)) = (a dvd ((x+ c*d) + t))"
using advdd
proof-
from advdd have "\<forall>x.\<forall>k. (((a::int) dvd (x + t)) = (a dvd
(x+k*d + t)))" by (rule dvd_modd_pinf)
then show ?thesis by simp
qed
(* lin_ad adds two linear terms*)
consts lin_add :: "intterm \<times> intterm \<Rightarrow> intterm"
recdef lin_add "measure (\<lambda>(x,y). ((size x) + (size y)))"
"lin_add (Add (Mult (Cst c1) (Var n1)) (r1),Add (Mult (Cst c2) (Var n2)) (r2)) =
(if n1=n2 then
(let c = Cst (c1 + c2)
in (if c1+c2=0 then lin_add(r1,r2) else Add (Mult c (Var n1)) (lin_add (r1,r2))))
else if n1 \<le> n2 then (Add (Mult (Cst c1) (Var n1)) (lin_add (r1,Add (Mult (Cst c2) (Var n2)) (r2))))
else (Add (Mult (Cst c2) (Var n2)) (lin_add (Add (Mult (Cst c1) (Var n1)) r1,r2))))"
"lin_add (Add (Mult (Cst c1) (Var n1)) (r1),Cst b) =
(Add (Mult (Cst c1) (Var n1)) (lin_add (r1, Cst b)))"
"lin_add (Cst x,Add (Mult (Cst c2) (Var n2)) (r2)) =
Add (Mult (Cst c2) (Var n2)) (lin_add (Cst x,r2))"
"lin_add (Cst b1, Cst b2) = Cst (b1+b2)"
lemma lin_add_cst_corr:
assumes blin : "islintn(n0,b)"
shows "I_intterm ats (lin_add (Cst a,b)) = (I_intterm ats (Add (Cst a) b))"
using blin
by (induct n0 b rule: islintn.induct) auto
lemma lin_add_cst_corr2:
assumes blin : "islintn(n0,b)"
shows "I_intterm ats (lin_add (b,Cst a)) = (I_intterm ats (Add b (Cst a)))"
using blin
by (induct n0 b rule: islintn.induct) auto
lemma lin_add_corrh: "\<And> n01 n02. \<lbrakk> islintn (n01,a) ; islintn (n02,b)\<rbrakk>
\<Longrightarrow> I_intterm ats (lin_add(a,b)) = I_intterm ats (Add a b)"
proof(induct a b rule: lin_add.induct)
case (58 i n r j m s)
have "(n = m \<and> i+j = 0) \<or> (n = m \<and> i+j \<noteq> 0) \<or> n < m \<or> m < n " by arith
moreover
{assume "n=m\<and>i+j=0" hence ?case using prems by (auto simp add: sym[OF zadd_zmult_distrib]) }
moreover
{assume "n=m\<and>i+j\<noteq>0" hence ?case using prems by (auto simp add: Let_def zadd_zmult_distrib)}
moreover
{assume "n < m" hence ?case using prems by auto }
moreover
{assume "n > m" hence ?case using prems by auto }
ultimately show ?case by blast
qed (auto simp add: lin_add_cst_corr lin_add_cst_corr2 Let_def)
(* lin_add has the semantics of Add*)
lemma lin_add_corr:
assumes lina: "islinintterm a"
and linb: "islinintterm b"
shows "I_intterm ats (lin_add (a,b)) = (I_intterm ats (Add a b))"
using lina linb islinintterm_eq_islint islint_def lin_add_corrh
by blast
lemma lin_add_cst_lint:
assumes lin: "islintn (n0,b)"
shows "islintn (n0, lin_add (Cst i, b))"
using lin
by (induct n0 b rule: islintn.induct) auto
lemma lin_add_cst_lint2:
assumes lin: "islintn (n0,b)"
shows "islintn (n0, lin_add (b,Cst i))"
using lin
by (induct n0 b rule: islintn.induct) auto
(* lin_add preserves linearity..*)
lemma lin_add_lint: "\<And> n0 n01 n02. \<lbrakk> islintn (n01,a) ; islintn (n02,b); n0 \<le> min n01 n02 \<rbrakk>
\<Longrightarrow> islintn (n0, lin_add (a,b))"
proof (induct a b rule: lin_add.induct)
case (58 i n r j m s)
have "(n =m \<and> i + j = 0) \<or> (n = m \<and> i+j \<noteq> 0) \<or> n <m \<or> m < n" by arith
moreover
{ assume "n = m"
and "i+j = 0"
hence ?case using "58" islintn_mon[where m = "n01" and n = "Suc m"]
islintn_mon[where m = "n02" and n = "Suc m"] by auto }
moreover
{ assume "n = m"
and "i+j \<noteq> 0"
hence ?case using "58" islintn_mon[where m = "n01" and n = "Suc m"]
islintn_mon[where m = "n02" and n = "Suc m"] by (auto simp add: Let_def) }
moreover
{ assume "n < m" hence ?case using 58 by force }
moreover
{ assume "m < n"
hence ?case using 58
apply (auto simp add: Let_def)
apply (erule allE[where x = "Suc m" ] )
by (erule allE[where x = "Suc m" ] ) simp }
ultimately show ?case by blast
qed(simp_all add: Let_def lin_add_cst_lint lin_add_cst_lint2)
lemma lin_add_lin:
assumes lina: "islinintterm a"
and linb: "islinintterm b"
shows "islinintterm (lin_add (a,b))"
using islinintterm_eq_islint islint_def lin_add_lint lina linb by auto
(* lin_mul multiplies a linear term by a constant *)
consts lin_mul :: "int \<times> intterm \<Rightarrow> intterm"
recdef lin_mul "measure (\<lambda>(c,t). size t)"
"lin_mul (c,Cst i) = (Cst (c*i))"
"lin_mul (c,Add (Mult (Cst c') (Var n)) r) =
(if c = 0 then (Cst 0) else
(Add (Mult (Cst (c*c')) (Var n)) (lin_mul (c,r))))"
lemma zmult_zadd_distrib[simp]: "(a::int) * (b+c) = a*b + a*c"
proof-
have "a*(b+c) = (b+c)*a" by simp
moreover have "(b+c)*a = b*a + c*a" by (simp add: zadd_zmult_distrib)
ultimately show ?thesis by simp
qed
(* lin_mul has the semantics of Mult *)
lemma lin_mul_corr:
assumes lint: "islinintterm t"
shows "I_intterm ats (lin_mul (c,t)) = I_intterm ats (Mult (Cst c) t)"
using lint
proof (induct c t rule: lin_mul.induct)
case (21 c c' n r)
have "islinintterm (Add (Mult (Cst c') (Var n)) r)" .
then have "islinintterm r"
by (rule islinintterm_subt[of "c'" "n" "r"])
then show ?case using "21.hyps" "21.prems" by simp
qed(auto)
(* lin_mul preserves linearity *)
lemma lin_mul_lin:
assumes lint: "islinintterm t"
shows "islinintterm (lin_mul(c,t))"
using lint
by (induct t rule: islinintterm.induct) auto
lemma lin_mul0:
assumes lint: "islinintterm t"
shows "lin_mul(0,t) = Cst 0"
using lint
by (induct t rule: islinintterm.induct) auto
lemma lin_mul_lintn:
"\<And> m. islintn(m,t) \<Longrightarrow> islintn(m,lin_mul(l,t))"
by (induct l t rule: lin_mul.induct) simp_all
(* lin_neg neagtes a linear term *)
definition
lin_neg :: "intterm \<Rightarrow> intterm"
"lin_neg i = lin_mul ((-1::int),i)"
(* lin_neg has the semantics of Neg *)
lemma lin_neg_corr:
assumes lint: "islinintterm t"
shows "I_intterm ats (lin_neg t) = I_intterm ats (Neg t)"
using lint lin_mul_corr
by (simp add: lin_neg_def lin_mul_corr)
(* lin_neg preserves linearity *)
lemma lin_neg_lin:
assumes lint: "islinintterm t"
shows "islinintterm (lin_neg t)"
using lint
by (simp add: lin_mul_lin lin_neg_def)
(* Some properties about lin_add and lin-neg should be moved above *)
lemma lin_neg_idemp:
assumes lini: "islinintterm i"
shows "lin_neg (lin_neg i) = i"
using lini
by (induct i rule: islinintterm.induct) (auto simp add: lin_neg_def)
lemma lin_neg_lin_add_distrib:
assumes lina : "islinintterm a"
and linb :"islinintterm b"
shows "lin_neg (lin_add(a,b)) = lin_add (lin_neg a, lin_neg b)"
using lina linb
proof (induct a b rule: lin_add.induct)
case (58 c1 n1 r1 c2 n2 r2)
from prems have lincnr1:"islinintterm (Add (Mult (Cst c1) (Var n1)) r1)" by simp
have linr1: "islinintterm r1" by (rule islinintterm_subt[OF lincnr1])
from prems have lincnr2: "islinintterm (Add (Mult (Cst c2) (Var n2)) r2)" by simp
have linr2: "islinintterm r2" by (rule islinintterm_subt[OF lincnr2])
have "n1 = n2 \<or> n1 < n2 \<or> n1 > n2" by arith
show ?case using prems linr1 linr2 by (simp_all add: lin_neg_def Let_def)
next
case (59 c n r b)
from prems have lincnr: "islinintterm (Add (Mult (Cst c) (Var n)) r)" by simp
have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
show ?case using prems linr by (simp add: lin_neg_def Let_def)
next
case (60 b c n r)
from prems have lincnr: "islinintterm (Add (Mult (Cst c) (Var n)) r)" by simp
have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
show ?case using prems linr by (simp add: lin_neg_def Let_def)
qed (simp_all add: lin_neg_def)
(* linearize tries to linearize a term *)
consts linearize :: "intterm \<Rightarrow> intterm option"
recdef linearize "measure (\<lambda>t. size t)"
"linearize (Cst b) = Some (Cst b)"
"linearize (Var n) = Some (Add (Mult (Cst 1) (Var n)) (Cst 0))"
"linearize (Neg i) = lift_un lin_neg (linearize i)"
"linearize (Add i j) = lift_bin(\<lambda> x. \<lambda> y. lin_add(x,y), linearize i, linearize j)"
"linearize (Sub i j) =
lift_bin(\<lambda> x. \<lambda> y. lin_add(x,lin_neg y), linearize i, linearize j)"
"linearize (Mult i j) =
(case linearize i of
None \<Rightarrow> None
| Some li \<Rightarrow> (case li of
Cst b \<Rightarrow> (case linearize j of
None \<Rightarrow> None
| (Some lj) \<Rightarrow> Some (lin_mul(b,lj)))
| _ \<Rightarrow> (case linearize j of
None \<Rightarrow> None
| (Some lj) \<Rightarrow> (case lj of
Cst b \<Rightarrow> Some (lin_mul (b,li))
| _ \<Rightarrow> None))))"
lemma linearize_linear1:
assumes lin: "linearize t \<noteq> None"
shows "islinintterm (the (linearize t))"
using lin
proof (induct t rule: linearize.induct)
case (1 b) show ?case by simp
next
case (2 n) show ?case by simp
next
case (3 i) show ?case
proof-
have "(linearize i = None) \<or> (\<exists>li. linearize i = Some li)" by auto
moreover
{ assume "linearize i = None" with prems have ?thesis by auto}
moreover
{ assume lini: "\<exists>li. linearize i = Some li"
from lini obtain "li" where "linearize i = Some li" by blast
have linli: "islinintterm li" by (simp!)
moreover have "linearize (Neg i) = Some (lin_neg li)" using prems by simp
moreover from linli have "islinintterm(lin_neg li)" by (simp add: lin_neg_lin)
ultimately have ?thesis by simp
}
ultimately show ?thesis by blast
qed
next
case (4 i j) show ?case
proof-
have "(linearize i = None) \<or> ((\<exists> li. linearize i = Some li) \<and> linearize j = None) \<or> ((\<exists> li. linearize i = Some li) \<and> (\<exists> lj. linearize j = Some lj))" by auto
moreover
{
assume nlini: "linearize i = None"
from nlini have "linearize (Add i j) = None"
by simp then have ?thesis using prems by auto}
moreover
{ assume nlinj: "linearize j = None"
and lini: "\<exists> li. linearize i = Some li"
from nlinj lini have "linearize (Add i j) = None"
by auto with prems have ?thesis by auto}
moreover
{ assume lini: "\<exists>li. linearize i = Some li"
and linj: "\<exists>lj. linearize j = Some lj"
from lini obtain "li" where "linearize i = Some li" by blast
have linli: "islinintterm li" by (simp!)
from linj obtain "lj" where "linearize j = Some lj" by blast
have linlj: "islinintterm lj" by (simp!)
moreover from lini linj have "linearize (Add i j) = Some (lin_add (li,lj))"
by (auto!)
moreover from linli linlj have "islinintterm(lin_add (li,lj))" by (simp add: lin_add_lin)
ultimately have ?thesis by simp }
ultimately show ?thesis by blast
qed
next
case (5 i j)show ?case
proof-
have "(linearize i = None) \<or> ((\<exists> li. linearize i = Some li) \<and> linearize j = None) \<or> ((\<exists> li. linearize i = Some li) \<and> (\<exists> lj. linearize j = Some lj))" by auto
moreover
{
assume nlini: "linearize i = None"
from nlini have "linearize (Sub i j) = None" by simp then have ?thesis by (auto!)
}
moreover
{
assume lini: "\<exists> li. linearize i = Some li"
and nlinj: "linearize j = None"
from nlinj lini have "linearize (Sub i j) = None"
by auto then have ?thesis by (auto!)
}
moreover
{
assume lini: "\<exists>li. linearize i = Some li"
and linj: "\<exists>lj. linearize j = Some lj"
from lini obtain "li" where "linearize i = Some li" by blast
have linli: "islinintterm li" by (simp!)
from linj obtain "lj" where "linearize j = Some lj" by blast
have linlj: "islinintterm lj" by (simp!)
moreover from lini linj have "linearize (Sub i j) = Some (lin_add (li,lin_neg lj))"
by (auto!)
moreover from linli linlj have "islinintterm(lin_add (li,lin_neg lj))" by (simp add: lin_add_lin lin_neg_lin)
ultimately have ?thesis by simp
}
ultimately show ?thesis by blast
qed
next
case (6 i j)show ?case
proof-
have cses: "(linearize i = None) \<or>
((\<exists> li. linearize i = Some li) \<and> linearize j = None) \<or>
((\<exists> li. linearize i = Some li) \<and> (\<exists> bj. linearize j = Some (Cst bj)))
\<or> ((\<exists> bi. linearize i = Some (Cst bi)) \<and> (\<exists> lj. linearize j = Some lj))
\<or> ((\<exists> li. linearize i = Some li \<and> \<not> (\<exists> bi. li = Cst bi)) \<and> (\<exists> lj. linearize j = Some lj \<and> \<not> (\<exists> bj. lj = Cst bj)))" by auto
moreover
{
assume nlini: "linearize i = None"
from nlini have "linearize (Mult i j) = None" by (simp)
with prems have ?thesis by auto }
moreover
{ assume lini: "\<exists> li. linearize i = Some li"
and nlinj: "linearize j = None"
from lini obtain "li" where "linearize i = Some li" by blast
moreover from nlinj lini have "linearize (Mult i j) = None"
using prems
by (cases li) (auto)
with prems have ?thesis by auto}
moreover
{ assume lini: "\<exists>li. linearize i = Some li"
and linj: "\<exists>bj. linearize j = Some (Cst bj)"
from lini obtain "li" where li_def: "linearize i = Some li" by blast
from prems have linli: "islinintterm li" by simp
moreover
from linj obtain "bj" where bj_def: "linearize j = Some (Cst bj)" by blast
have linlj: "islinintterm (Cst bj)" by simp
moreover from lini linj prems
have "linearize (Mult i j) = Some (lin_mul (bj,li))"
by (cases li) auto
moreover from linli linlj have "islinintterm(lin_mul (bj,li))" by (simp add: lin_mul_lin)
ultimately have ?thesis by simp }
moreover
{ assume lini: "\<exists>bi. linearize i = Some (Cst bi)"
and linj: "\<exists>lj. linearize j = Some lj"
from lini obtain "bi" where "linearize i = Some (Cst bi)" by blast
from prems have linli: "islinintterm (Cst bi)" by simp
moreover
from linj obtain "lj" where "linearize j = Some lj" by blast
from prems have linlj: "islinintterm lj" by simp
moreover from lini linj prems have "linearize (Mult i j) = Some (lin_mul (bi,lj))"
by simp
moreover from linli linlj have "islinintterm(lin_mul (bi,lj))" by (simp add: lin_mul_lin)
ultimately have ?thesis by simp }
moreover
{ assume linc: "\<exists> li. linearize i = Some li \<and> \<not> (\<exists> bi. li = Cst bi)"
and ljnc: "\<exists> lj. linearize j = Some lj \<and> \<not> (\<exists> bj. lj = Cst bj)"
from linc obtain "li" where "linearize i = Some li \<and> \<not> (\<exists> bi. li = Cst bi)" by blast
moreover
from ljnc obtain "lj" where "linearize j = Some lj \<and> \<not> (\<exists> bj. lj = Cst bj)" by blast
ultimately have "linearize (Mult i j) = None"
by (cases li, auto) (cases lj, auto)+
with prems have ?thesis by simp }
ultimately show ?thesis by blast
qed
qed
(* the result of linearize, when successful, is a linear term*)
lemma linearize_linear: "\<And> t'. linearize t = Some t' \<Longrightarrow> islinintterm t'"
proof-
fix t'
assume lint: "linearize t = Some t'"
from lint have lt: "linearize t \<noteq> None" by auto
then have "islinintterm (the (linearize t))" by (rule_tac linearize_linear1[OF lt])
with lint show "islinintterm t'" by simp
qed
lemma linearize_corr1:
assumes lin: "linearize t \<noteq> None"
shows "I_intterm ats t = I_intterm ats (the (linearize t))"
using lin
proof (induct t rule: linearize.induct)
case (3 i) show ?case
proof-
have "(linearize i = None) \<or> (\<exists>li. linearize i = Some li)" by auto
moreover
{
assume "linearize i = None"
have ?thesis using prems by simp
}
moreover
{
assume lini: "\<exists>li. linearize i = Some li"
from lini have lini2: "linearize i \<noteq> None" by auto
from lini obtain "li" where "linearize i = Some li" by blast
from lini2 lini have "islinintterm (the (linearize i))"
by (simp add: linearize_linear1[OF lini2])
then have linli: "islinintterm li" using prems by simp
have ieqli: "I_intterm ats i = I_intterm ats li" using prems by simp
moreover have "linearize (Neg i) = Some (lin_neg li)" using prems by simp
moreover from ieqli linli have "I_intterm ats (Neg i) = I_intterm ats (lin_neg li)" by (simp add: lin_neg_corr[OF linli])
ultimately have ?thesis using prems by (simp add: lin_neg_corr)
}
ultimately show ?thesis by blast
qed
next
case (4 i j) show ?case
proof-
have "(linearize i = None) \<or> ((\<exists> li. linearize i = Some li) \<and> linearize j = None) \<or> ((\<exists> li. linearize i = Some li) \<and> (\<exists> lj. linearize j = Some lj))" by auto
moreover
{
assume nlini: "linearize i = None"
from nlini have "linearize (Add i j) = None" by simp then have ?thesis using prems by auto
}
moreover
{
assume nlinj: "linearize j = None"
and lini: "\<exists> li. linearize i = Some li"
from nlinj lini have "linearize (Add i j) = None" by auto
then have ?thesis using prems by auto
}
moreover
{
assume lini: "\<exists>li. linearize i = Some li"
and linj: "\<exists>lj. linearize j = Some lj"
from lini have lini2: "linearize i \<noteq> None" by auto
from linj have linj2: "linearize j \<noteq> None" by auto
from lini obtain "li" where "linearize i = Some li" by blast
from lini2 have "islinintterm (the (linearize i))" by (simp add: linearize_linear1)
then have linli: "islinintterm li" using prems by simp
from linj obtain "lj" where "linearize j = Some lj" by blast
from linj2 have "islinintterm (the (linearize j))" by (simp add: linearize_linear1)
then have linlj: "islinintterm lj" using prems by simp
moreover from lini linj have "linearize (Add i j) = Some (lin_add (li,lj))"
using prems by simp
moreover from linli linlj have "I_intterm ats (lin_add (li,lj)) = I_intterm ats (Add li lj)" by (simp add: lin_add_corr)
ultimately have ?thesis using prems by simp
}
ultimately show ?thesis by blast
qed
next
case (5 i j)show ?case
proof-
have "(linearize i = None) \<or> ((\<exists> li. linearize i = Some li) \<and> linearize j = None) \<or> ((\<exists> li. linearize i = Some li) \<and> (\<exists> lj. linearize j = Some lj))" by auto
moreover
{
assume nlini: "linearize i = None"
from nlini have "linearize (Sub i j) = None" by simp then have ?thesis using prems by auto
}
moreover
{
assume lini: "\<exists> li. linearize i = Some li"
and nlinj: "linearize j = None"
from nlinj lini have "linearize (Sub i j) = None"
by auto with prems have ?thesis by auto
}
moreover
{
assume lini: "\<exists>li. linearize i = Some li"
and linj: "\<exists>lj. linearize j = Some lj"
from lini have lini2: "linearize i \<noteq> None" by auto
from linj have linj2: "linearize j \<noteq> None" by auto
from lini obtain "li" where "linearize i = Some li" by blast
from lini2 have "islinintterm (the (linearize i))" by (simp add: linearize_linear1)
with prems have linli: "islinintterm li" by simp
from linj obtain "lj" where "linearize j = Some lj" by blast
from linj2 have "islinintterm (the (linearize j))" by (simp add: linearize_linear1)
with prems have linlj: "islinintterm lj" by simp
moreover from prems have "linearize (Sub i j) = Some (lin_add (li,lin_neg lj))"
by simp
moreover from linlj have linnlj:"islinintterm (lin_neg lj)" by (simp add: lin_neg_lin)
moreover from linli linnlj have "I_intterm ats (lin_add (li,lin_neg lj)) = I_intterm ats (Add li (lin_neg lj))" by (simp only: lin_add_corr[OF linli linnlj])
moreover from linli linlj linnlj have "I_intterm ats (Add li (lin_neg lj)) = I_intterm ats (Sub li lj)"
by (simp add: lin_neg_corr)
ultimately have ?thesis using prems by simp
}
ultimately show ?thesis by blast
qed
next
case (6 i j)show ?case
proof-
have cses: "(linearize i = None) \<or>
((\<exists> li. linearize i = Some li) \<and> linearize j = None) \<or>
((\<exists> li. linearize i = Some li) \<and> (\<exists> bj. linearize j = Some (Cst bj)))
\<or> ((\<exists> bi. linearize i = Some (Cst bi)) \<and> (\<exists> lj. linearize j = Some lj))
\<or> ((\<exists> li. linearize i = Some li \<and> \<not> (\<exists> bi. li = Cst bi)) \<and> (\<exists> lj. linearize j = Some lj \<and> \<not> (\<exists> bj. lj = Cst bj)))" by auto
moreover
{
assume nlini: "linearize i = None"
from nlini have "linearize (Mult i j) = None" by simp with prems have ?thesis by auto
}
moreover
{
assume lini: "\<exists> li. linearize i = Some li"
and nlinj: "linearize j = None"
from lini obtain "li" where "linearize i = Some li" by blast
moreover from prems have "linearize (Mult i j) = None"
by (cases li) simp_all
with prems have ?thesis by auto
}
moreover
{
assume lini: "\<exists>li. linearize i = Some li"
and linj: "\<exists>bj. linearize j = Some (Cst bj)"
from lini have lini2: "linearize i \<noteq> None" by auto
from linj have linj2: "linearize j \<noteq> None" by auto
from lini obtain "li" where "linearize i = Some li" by blast
from lini2 have "islinintterm (the (linearize i))" by (simp add: linearize_linear1)
with prems have linli: "islinintterm li" by simp
moreover
from linj obtain "bj" where "linearize j = Some (Cst bj)" by blast
have linlj: "islinintterm (Cst bj)" by simp
moreover from prems have "linearize (Mult i j) = Some (lin_mul (bj,li))"
by (cases li) auto
then have lm1: "I_intterm ats (the(linearize (Mult i j))) = I_intterm ats (lin_mul (bj,li))" by simp
moreover from linli linlj have "I_intterm ats (lin_mul(bj,li)) = I_intterm ats (Mult li (Cst bj))" by (simp add: lin_mul_corr)
with prems
have "I_intterm ats (lin_mul(bj,li)) = I_intterm ats (Mult li (the (linearize j)))"
by auto
moreover have "I_intterm ats (Mult li (the (linearize j))) = I_intterm ats (Mult i (the (linearize j)))" using prems by simp
moreover have "I_intterm ats i = I_intterm ats (the (linearize i))"
using lini2 lini "6.hyps" by simp
moreover have "I_intterm ats j = I_intterm ats (the (linearize j))"
using prems by (cases li) auto
ultimately have ?thesis by auto }
moreover
{ assume lini: "\<exists>bi. linearize i = Some (Cst bi)"
and linj: "\<exists>lj. linearize j = Some lj"
from lini have lini2 : "linearize i \<noteq> None" by auto
from linj have linj2 : "linearize j \<noteq> None" by auto
from lini obtain "bi" where "linearize i = Some (Cst bi)" by blast
have linli: "islinintterm (Cst bi)" using prems by simp
moreover
from linj obtain "lj" where "linearize j = Some lj" by blast
from linj2 have "islinintterm (the (linearize j))" by (simp add: linearize_linear1)
then have linlj: "islinintterm lj" by (simp!)
moreover from linli lini linj have "linearize (Mult i j) = Some (lin_mul (bi,lj))"
by (case_tac "li::intterm",auto!)
then have lm1: "I_intterm ats (the(linearize (Mult i j))) = I_intterm ats (lin_mul (bi,lj))" by simp
moreover from linli linlj have "I_intterm ats (lin_mul(bi,lj)) = I_intterm ats (Mult (Cst bi) lj)" by (simp add: lin_mul_corr)
then have "I_intterm ats (lin_mul(bi,lj)) = I_intterm ats (Mult (the (linearize i)) lj)" by (auto!)
moreover have "I_intterm ats (Mult (the (linearize i)) lj) = I_intterm ats (Mult (the (linearize i)) j)" using lini lini2 by (simp!)
moreover have "I_intterm ats i = I_intterm ats (the (linearize i))"
using lini2 lini "6.hyps" by simp
moreover have "I_intterm ats j = I_intterm ats (the (linearize j))"
using linj linj2 lini lini2 linli linlj "6.hyps" by (auto!)
ultimately have ?thesis by auto }
moreover
{ assume linc: "\<exists> li. linearize i = Some li \<and> \<not> (\<exists> bi. li = Cst bi)"
and ljnc: "\<exists> lj. linearize j = Some lj \<and> \<not> (\<exists> bj. lj = Cst bj)"
from linc obtain "li" where "\<exists> li. linearize i = Some li \<and> \<not> (\<exists> bi. li = Cst bi)" by blast
moreover
from ljnc obtain "lj" where "\<exists> lj. linearize j = Some lj \<and> \<not> (\<exists> bj. lj = Cst bj)" by blast
ultimately have "linearize (Mult i j) = None"
apply simp
apply (case_tac "linearize i", auto)
apply (case_tac a)
apply (auto!)
by (case_tac "lj",auto)+
then have ?thesis by (simp!) }
ultimately show ?thesis by blast
qed
qed simp_all
(* linearize, when successful, preserves semantics *)
lemma linearize_corr: "\<And> t'. linearize t = Some t' \<Longrightarrow> I_intterm ats t = I_intterm ats t' "
proof-
fix t'
assume lint: "linearize t = Some t'"
show "I_intterm ats t = I_intterm ats t'"
proof-
from lint have lt: "linearize t \<noteq> None" by simp
then have "I_intterm ats t = I_intterm ats (the (linearize t))"
by (rule_tac linearize_corr1[OF lt])
with lint show ?thesis by simp
qed
qed
(* tries to linearize a formula *)
consts linform :: "QF \<Rightarrow> QF option"
primrec
"linform (Le it1 it2) =
lift_bin(\<lambda>x. \<lambda>y. Le (lin_add(x,lin_neg y)) (Cst 0),linearize it1, linearize it2)"
"linform (Eq it1 it2) =
lift_bin(\<lambda>x. \<lambda>y. Eq (lin_add(x,lin_neg y)) (Cst 0),linearize it1, linearize it2)"
"linform (Divides d t) =
(case linearize d of
None \<Rightarrow> None
| Some ld \<Rightarrow> (case ld of
Cst b \<Rightarrow>
(if (b=0) then None
else
(case linearize t of
None \<Rightarrow> None
| Some lt \<Rightarrow> Some (Divides ld lt)))
| _ \<Rightarrow> None))"
"linform T = Some T"
"linform F = Some F"
"linform (NOT p) = lift_un NOT (linform p)"
"linform (And p q)= lift_bin(\<lambda>f. \<lambda>g. And f g, linform p, linform q)"
"linform (Or p q) = lift_bin(\<lambda>f. \<lambda>g. Or f g, linform p, linform q)"
(* linearity of formulae *)
consts islinform :: "QF \<Rightarrow> bool"
recdef islinform "measure size"
"islinform (Le it (Cst i)) = (i=0 \<and> islinintterm it )"
"islinform (Eq it (Cst i)) = (i=0 \<and> islinintterm it)"
"islinform (Divides (Cst d) t) = (d \<noteq> 0 \<and> islinintterm t)"
"islinform T = True"
"islinform F = True"
"islinform (NOT (Divides (Cst d) t)) = (d \<noteq> 0 \<and> islinintterm t)"
"islinform (NOT (Eq it (Cst i))) = (i=0 \<and> islinintterm it)"
"islinform (And p q)= ((islinform p) \<and> (islinform q))"
"islinform (Or p q) = ((islinform p) \<and> (islinform q))"
"islinform p = False"
(* linform preserves nnf, if successful *)
lemma linform_nnf:
assumes nnfp: "isnnf p"
shows "\<And> p'. \<lbrakk>linform p = Some p'\<rbrakk> \<Longrightarrow> isnnf p'"
using nnfp
proof (induct p rule: isnnf.induct, simp_all)
case (goal1 a b p')
show ?case
using prems
by (cases "linearize a", auto) (cases "linearize b", auto)
next
case (goal2 a b p')
show ?case
using prems
by (cases "linearize a", auto) (cases "linearize b", auto)
next
case (goal3 d t p')
show ?case
using prems
apply (cases "linearize d", auto)
apply (case_tac "a",auto)
apply (case_tac "int=0",auto)
by (cases "linearize t",auto)
next
case (goal4 f g p') show ?case
using prems
by (cases "linform f", auto) (cases "linform g", auto)
next
case (goal5 f g p') show ?case
using prems
by (cases "linform f", auto) (cases "linform g", auto)
next
case (goal6 d t p') show ?case
using prems
apply (cases "linearize d", auto)
apply (case_tac "a", auto)
apply (case_tac "int = 0",auto)
by (cases "linearize t", auto)
next
case (goal7 a b p')
show ?case
using prems
by (cases "linearize a", auto) (cases "linearize b", auto)
qed
lemma linform_corr: "\<And> lp. \<lbrakk> isnnf p ; linform p = Some lp \<rbrakk> \<Longrightarrow>
(qinterp ats p = qinterp ats lp)"
proof (induct p rule: linform.induct)
case (Le x y)
show ?case
using "Le.prems"
proof-
have "(\<exists> lx ly. linearize x = Some lx \<and> linearize y = Some ly) \<or>
(linearize x = None) \<or> (linearize y = None)"by auto
moreover
{
assume linxy: "\<exists> lx ly. linearize x = Some lx \<and> linearize y = Some ly"
from linxy obtain "lx" "ly"
where lxly:"linearize x = Some lx \<and> linearize y = Some ly" by blast
then
have lxeqx: "I_intterm ats x = I_intterm ats lx"
by (simp add: linearize_corr)
from lxly have lxlin: "islinintterm lx"
by (auto simp add: linearize_linear)
from lxly have lyeqy: "I_intterm ats y = I_intterm ats ly"
by (simp add: linearize_corr)
from lxly have lylin: "islinintterm ly"
by (auto simp add: linearize_linear)
from "prems"
have lpeqle: "lp = (Le (lin_add(lx,lin_neg ly)) (Cst 0))"
by auto
moreover
have lin1: "islinintterm (Cst 1)" by simp
then
have ?thesis
using lxlin lylin lin1 lin_add_lin lin_neg_lin "prems" lxly lpeqle
by (simp add: lin_add_corr lin_neg_corr lxeqx lyeqy)
}
moreover
{
assume "linearize x = None"
have ?thesis using "prems" by simp
}
moreover
{
assume "linearize y = None"
then have ?thesis using "prems"
by (case_tac "linearize x", auto)
}
ultimately show ?thesis by blast
qed
next
case (Eq x y)
show ?case
using "Eq.prems"
proof-
have "(\<exists> lx ly. linearize x = Some lx \<and> linearize y = Some ly) \<or>
(linearize x = None) \<or> (linearize y = None)"by auto
moreover
{
assume linxy: "\<exists> lx ly. linearize x = Some lx \<and> linearize y = Some ly"
from linxy obtain "lx" "ly"
where lxly:"linearize x = Some lx \<and> linearize y = Some ly" by blast
then
have lxeqx: "I_intterm ats x = I_intterm ats lx"
by (simp add: linearize_corr)
from lxly have lxlin: "islinintterm lx"
by (auto simp add: linearize_linear)
from lxly have lyeqy: "I_intterm ats y = I_intterm ats ly"
by (simp add: linearize_corr)
from lxly have lylin: "islinintterm ly"
by (auto simp add: linearize_linear)
from "prems"
have lpeqle: "lp = (Eq (lin_add(lx,lin_neg ly)) (Cst 0))"
by auto
moreover
have lin1: "islinintterm (Cst 1)" by simp
then
have ?thesis
using lxlin lylin lin1 lin_add_lin lin_neg_lin "prems" lxly lpeqle
by (simp add: lin_add_corr lin_neg_corr lxeqx lyeqy)
}
moreover
{
assume "linearize x = None"
have ?thesis using "prems" by simp
}
moreover
{
assume "linearize y = None"
then have ?thesis using "prems"
by (case_tac "linearize x", auto)
}
ultimately show ?thesis by blast
qed
next
case (Divides d t)
show ?case
using "Divides.prems"
apply (case_tac "linearize d",auto)
apply (case_tac a, auto)
apply (case_tac "int = 0", auto)
apply (case_tac "linearize t", auto)
apply (simp add: linearize_corr)
apply (case_tac a, auto)
apply (case_tac "int = 0", auto)
by (case_tac "linearize t", auto simp add: linearize_corr)
next
case (NOT f) show ?case
using "prems"
proof-
have "(\<exists> lf. linform f = Some lf) \<or> (linform f = None)" by auto
moreover
{
assume linf: "\<exists> lf. linform f = Some lf"
from prems have "isnnf (NOT f)" by simp
then have fnnf: "isnnf f" by (cases f) auto
from linf obtain "lf" where lf: "linform f = Some lf" by blast
then have "lp = NOT lf" using "prems" by auto
with "NOT.prems" "NOT.hyps" lf fnnf
have ?case by simp
}
moreover
{
assume "linform f = None"
then
have "linform (NOT f) = None" by simp
then
have ?thesis using "NOT.prems" by simp
}
ultimately show ?thesis by blast
qed
next
case (Or f g)
show ?case using "Or.hyps"
proof -
have "((\<exists> lf. linform f = Some lf ) \<and> (\<exists> lg. linform g = Some lg)) \<or>
(linform f = None) \<or> (linform g = None)" by auto
moreover
{
assume linf: "\<exists> lf. linform f = Some lf"
and ling: "\<exists> lg. linform g = Some lg"
from linf obtain "lf" where lf: "linform f = Some lf" by blast
from ling obtain "lg" where lg: "linform g = Some lg" by blast
from lf lg have "linform (Or f g) = Some (Or lf lg)" by simp
then have "lp = Or lf lg" using lf lg "prems" by simp
with lf lg "prems" have ?thesis by simp
}
moreover
{
assume "linform f = None"
then have ?thesis using "Or.prems" by auto
}
moreover
{
assume "linform g = None"
then have ?thesis using "Or.prems" by (case_tac "linform f", auto)
}
ultimately show ?thesis by blast
qed
next
case (And f g)
show ?case using "And.hyps"
proof -
have "((\<exists> lf. linform f = Some lf ) \<and> (\<exists> lg. linform g = Some lg)) \<or>
(linform f = None) \<or> (linform g = None)" by auto
moreover
{
assume linf: "\<exists> lf. linform f = Some lf"
and ling: "\<exists> lg. linform g = Some lg"
from linf obtain "lf" where lf: "linform f = Some lf" by blast
from ling obtain "lg" where lg: "linform g = Some lg" by blast
from lf lg have "linform (And f g) = Some (And lf lg)" by simp
then have "lp = And lf lg" using lf lg "prems" by simp
with lf lg "prems" have ?thesis by simp
}
moreover
{
assume "linform f = None"
then have ?thesis using "And.prems" by auto
}
moreover
{
assume "linform g = None"
then have ?thesis using "And.prems" by (case_tac "linform f", auto)
}
ultimately show ?thesis by blast
qed
qed simp_all
(* the result of linform is a linear formula *)
lemma linform_lin: "\<And> lp. \<lbrakk> isnnf p ; linform p = Some lp\<rbrakk> \<Longrightarrow> islinform lp"
proof (induct p rule: linform.induct)
case (Le x y)
have "((\<exists> lx. linearize x = Some lx) \<and> (\<exists> ly. linearize y = Some ly)) \<or>
(linearize x = None) \<or> (linearize y = None) " by clarsimp
moreover
{
assume linx: "\<exists> lx. linearize x = Some lx"
and liny: "\<exists> ly. linearize y = Some ly"
from linx obtain "lx" where lx: "linearize x = Some lx" by blast
from liny obtain "ly" where ly: "linearize y = Some ly" by blast
from lx have lxlin: "islinintterm lx" by (simp add: linearize_linear)
from ly have lylin: "islinintterm ly" by (simp add: linearize_linear)
have lin1:"islinintterm (Cst 1)" by simp
have lin0: "islinintterm (Cst 0)" by simp
from "prems" have "lp = Le (lin_add(lx,lin_neg ly)) (Cst 0)"
by auto
with lin0 lin1 lxlin lylin "prems"
have ?case by (simp add: lin_add_lin lin_neg_lin)
}
moreover
{
assume "linearize x = None"
then have ?case using "prems" by simp
}
moreover
{
assume "linearize y = None"
then have ?case using "prems" by (case_tac "linearize x",simp_all)
}
ultimately show ?case by blast
next
case (Eq x y)
have "((\<exists> lx. linearize x = Some lx) \<and> (\<exists> ly. linearize y = Some ly)) \<or>
(linearize x = None) \<or> (linearize y = None) " by clarsimp
moreover
{
assume linx: "\<exists> lx. linearize x = Some lx"
and liny: "\<exists> ly. linearize y = Some ly"
from linx obtain "lx" where lx: "linearize x = Some lx" by blast
from liny obtain "ly" where ly: "linearize y = Some ly" by blast
from lx have lxlin: "islinintterm lx" by (simp add: linearize_linear)
from ly have lylin: "islinintterm ly" by (simp add: linearize_linear)
have lin1:"islinintterm (Cst 1)" by simp
have lin0: "islinintterm (Cst 0)" by simp
from "prems" have "lp = Eq (lin_add(lx,lin_neg ly)) (Cst 0)"
by auto
with lin0 lin1 lxlin lylin "prems"
have ?case by (simp add: lin_add_lin lin_neg_lin)
}
moreover
{
assume "linearize x = None"
then have ?case using "prems" by simp
}
moreover
{
assume "linearize y = None"
then have ?case using "prems" by (case_tac "linearize x",simp_all)
}
ultimately show ?case by blast
next
case (Divides d t)
show ?case
using prems
apply (case_tac "linearize d", auto)
apply (case_tac a, auto)
apply (case_tac "int = 0", auto)
by (case_tac "linearize t",auto simp add: linearize_linear)
next
case (Or f g)
show ?case using "Or.hyps"
proof -
have "((\<exists> lf. linform f = Some lf ) \<and> (\<exists> lg. linform g = Some lg)) \<or>
(linform f = None) \<or> (linform g = None)" by auto
moreover
{
assume linf: "\<exists> lf. linform f = Some lf"
and ling: "\<exists> lg. linform g = Some lg"
from linf obtain "lf" where lf: "linform f = Some lf" by blast
from ling obtain "lg" where lg: "linform g = Some lg" by blast
from lf lg have "linform (Or f g) = Some (Or lf lg)" by simp
then have "lp = Or lf lg" using lf lg "prems" by simp
with lf lg "prems" have ?thesis by simp
}
moreover
{
assume "linform f = None"
then have ?thesis using "Or.prems" by auto
}
moreover
{
assume "linform g = None"
then have ?thesis using "Or.prems" by (case_tac "linform f", auto)
}
ultimately show ?thesis by blast
qed
next
case (And f g)
show ?case using "And.hyps"
proof -
have "((\<exists> lf. linform f = Some lf ) \<and> (\<exists> lg. linform g = Some lg)) \<or>
(linform f = None) \<or> (linform g = None)" by auto
moreover
{
assume linf: "\<exists> lf. linform f = Some lf"
and ling: "\<exists> lg. linform g = Some lg"
from linf obtain "lf" where lf: "linform f = Some lf" by blast
from ling obtain "lg" where lg: "linform g = Some lg" by blast
from lf lg have "linform (And f g) = Some (And lf lg)" by simp
then have "lp = And lf lg" using lf lg "prems" by simp
with lf lg "prems" have ?thesis by simp
}
moreover
{
assume "linform f = None"
then have ?thesis using "And.prems" by auto
}
moreover
{
assume "linform g = None"
then have ?thesis using "And.prems" by (case_tac "linform f", auto)
}
ultimately show ?thesis by blast
qed
next
case (NOT f) show ?case
using "prems"
proof-
have "(\<exists> lf. linform f = Some lf) \<or> (linform f = None)" by auto
moreover
{
assume linf: "\<exists> lf. linform f = Some lf"
from prems have "isnnf (NOT f)" by simp
then have fnnf: "isnnf f" by (cases f) auto
from linf obtain "lf" where lf: "linform f = Some lf" by blast
then have "lp = NOT lf" using "prems" by auto
with "NOT.prems" "NOT.hyps" lf fnnf
have ?thesis
using fnnf
apply (cases f, auto)
prefer 2
apply (case_tac "linearize intterm1",auto)
apply (case_tac a, auto)
apply (case_tac "int = 0", auto)
apply (case_tac "linearize intterm2")
apply (auto simp add: linearize_linear)
apply (case_tac "linearize intterm1",auto)
by (case_tac "linearize intterm2")
(auto simp add: linearize_linear lin_add_lin lin_neg_lin)
}
moreover
{
assume "linform f = None"
then
have "linform (NOT f) = None" by simp
then
have ?thesis using "NOT.prems" by simp
}
ultimately show ?thesis by blast
qed
qed (simp_all)
(* linform, if successful, preserves quantifier freeness *)
lemma linform_isnnf: "islinform p \<Longrightarrow> isnnf p"
by (induct p rule: islinform.induct) auto
lemma linform_isqfree: "islinform p \<Longrightarrow> isqfree p"
using linform_isnnf nnf_isqfree by simp
lemma linform_qfree: "\<And> p'. \<lbrakk> isnnf p ; linform p = Some p'\<rbrakk> \<Longrightarrow> isqfree p'"
using linform_isqfree linform_lin
by simp
(* Definitions and lemmas about gcd and lcm *)
definition
lcm :: "nat \<times> nat \<Rightarrow> nat"
"lcm = (\<lambda>(m,n). m*n div gcd(m,n))"
definition
ilcm :: "int \<Rightarrow> int \<Rightarrow> int"
"ilcm = (\<lambda>i.\<lambda>j. int (lcm(nat(abs i),nat(abs j))))"
(* ilcm_dvd12 are needed later *)
lemma lcm_dvd1:
assumes mpos: " m >0"
and npos: "n>0"
shows "m dvd (lcm(m,n))"
proof-
have "gcd(m,n) dvd n" by simp
then obtain "k" where "n = gcd(m,n) * k" using dvd_def by auto
then have "m*n div gcd(m,n) = m*(gcd(m,n)*k) div gcd(m,n)" by (simp add: mult_ac)
also have "\<dots> = m*k" using mpos npos gcd_zero by simp
finally show ?thesis by (simp add: lcm_def)
qed
lemma lcm_dvd2:
assumes mpos: " m >0"
and npos: "n>0"
shows "n dvd (lcm(m,n))"
proof-
have "gcd(m,n) dvd m" by simp
then obtain "k" where "m = gcd(m,n) * k" using dvd_def by auto
then have "m*n div gcd(m,n) = (gcd(m,n)*k)*n div gcd(m,n)" by (simp add: mult_ac)
also have "\<dots> = n*k" using mpos npos gcd_zero by simp
finally show ?thesis by (simp add: lcm_def)
qed
lemma ilcm_dvd1:
assumes anz: "a \<noteq> 0"
and bnz: "b \<noteq> 0"
shows "a dvd (ilcm a b)"
proof-
let ?na = "nat (abs a)"
let ?nb = "nat (abs b)"
have nap: "?na >0" using anz by simp
have nbp: "?nb >0" using bnz by simp
from nap nbp have "?na dvd lcm(?na,?nb)" using lcm_dvd1 by simp
thus ?thesis by (simp add: ilcm_def dvd_int_iff)
qed
lemma ilcm_dvd2:
assumes anz: "a \<noteq> 0"
and bnz: "b \<noteq> 0"
shows "b dvd (ilcm a b)"
proof-
let ?na = "nat (abs a)"
let ?nb = "nat (abs b)"
have nap: "?na >0" using anz by simp
have nbp: "?nb >0" using bnz by simp
from nap nbp have "?nb dvd lcm(?na,?nb)" using lcm_dvd2 by simp
thus ?thesis by (simp add: ilcm_def dvd_int_iff)
qed
lemma zdvd_self_abs1: "(d::int) dvd (abs d)"
by (case_tac "d <0", simp_all)
lemma zdvd_self_abs2: "(abs (d::int)) dvd d"
by (case_tac "d<0", simp_all)
(* lcm a b is positive for positive a and b *)
lemma lcm_pos:
assumes mpos: "m > 0"
and npos: "n>0"
shows "lcm (m,n) > 0"
proof(rule ccontr, simp add: lcm_def gcd_zero)
assume h:"m*n div gcd(m,n) = 0"
from mpos npos have "gcd (m,n) \<noteq> 0" using gcd_zero by simp
hence gcdp: "gcd(m,n) > 0" by simp
with h
have "m*n < gcd(m,n)"
by (cases "m * n < gcd (m, n)") (auto simp add: div_if[OF gcdp, where m="m*n"])
moreover
have "gcd(m,n) dvd m" by simp
with mpos dvd_imp_le have t1:"gcd(m,n) \<le> m" by simp
with npos have t1:"gcd(m,n)*n \<le> m*n" by simp
have "gcd(m,n) \<le> gcd(m,n)*n" using npos by simp
with t1 have "gcd(m,n) \<le> m*n" by arith
ultimately show "False" by simp
qed
lemma ilcm_pos:
assumes apos: " 0 < a"
and bpos: "0 < b"
shows "0 < ilcm a b"
proof-
let ?na = "nat (abs a)"
let ?nb = "nat (abs b)"
have nap: "?na >0" using apos by simp
have nbp: "?nb >0" using bpos by simp
have "0 < lcm (?na,?nb)" by (rule lcm_pos[OF nap nbp])
thus ?thesis by (simp add: ilcm_def)
qed
(* fomlcm computes the lcm of all c, where c is the coeffitient of Var 0 *)
consts formlcm :: "QF \<Rightarrow> int"
recdef formlcm "measure size"
"formlcm (Le (Add (Mult (Cst c) (Var 0)) r) (Cst i)) = abs c "
"formlcm (Eq (Add (Mult (Cst c) (Var 0)) r) (Cst i)) = abs c "
"formlcm (Divides (Cst d) (Add (Mult (Cst c) (Var 0)) r)) = abs c"
"formlcm (NOT p) = formlcm p"
"formlcm (And p q)= ilcm (formlcm p) (formlcm q)"
"formlcm (Or p q) = ilcm (formlcm p) (formlcm q)"
"formlcm p = 1"
(* the property that formlcm should fullfill *)
consts divideallc:: "int \<times> QF \<Rightarrow> bool"
recdef divideallc "measure (\<lambda>(i,p). size p)"
"divideallc (l,Le (Add (Mult (Cst c) (Var 0)) r) (Cst i)) = (c dvd l)"
"divideallc (l,Eq (Add (Mult (Cst c) (Var 0)) r) (Cst i)) = (c dvd l)"
"divideallc(l,Divides (Cst d) (Add (Mult (Cst c) (Var 0)) r)) = (c dvd l)"
"divideallc (l,NOT p) = divideallc(l,p)"
"divideallc (l,And p q) = (divideallc (l,p) \<and> divideallc (l,q))"
"divideallc (l,Or p q) = (divideallc (l,p) \<and> divideallc (l,q))"
"divideallc p = True"
(* formlcm retuns a positive integer *)
lemma formlcm_pos:
assumes linp: "islinform p"
shows "0 < formlcm p"
using linp
proof (induct p rule: formlcm.induct, simp_all add: ilcm_pos)
case (goal1 c r i)
have "i=0 \<or> i \<noteq> 0" by simp
moreover
{
assume "i \<noteq> 0" then have ?case using prems by simp
}
moreover
{
assume iz: "i = 0"
then have "islinintterm (Add (Mult (Cst c) (Var 0)) r)" using prems by simp
then have "c\<noteq>0"
using prems
by (simp add: islininttermc0r[where c="c" and n="0" and r="r"])
then have ?case by simp
}
ultimately
show ?case by blast
next
case (goal2 c r i)
have "i=0 \<or> i \<noteq> 0" by simp
moreover
{
assume "i \<noteq> 0" then have ?case using prems by simp
}
moreover
{
assume iz: "i = 0"
then have "islinintterm (Add (Mult (Cst c) (Var 0)) r)" using prems by simp
then have "c\<noteq>0"
using prems
by (simp add: islininttermc0r[where c="c" and n="0" and r="r"])
then have ?case by simp
}
ultimately
show ?case by blast
next
case (goal3 d c r)
show ?case using prems by (simp add: islininttermc0r[where c="c" and n="0" and r="r"])
next
case (goal4 f)
show ?case using prems
by (cases f,auto) (case_tac "intterm2", auto,case_tac "intterm1", auto)
qed
lemma divideallc_mono: "\<And> c. \<lbrakk> divideallc(c,p) ; c dvd d\<rbrakk> \<Longrightarrow> divideallc (d,p)"
proof (induct d p rule: divideallc.induct, simp_all)
case (goal1 l a b) show ?case by ( rule zdvd_trans [where m="a" and n="b" and k="l"])
next
case (goal2 l a b) show ?case by ( rule zdvd_trans [where m="a" and n="b" and k="l"])
next
case (goal3 l a b) show ?case by ( rule zdvd_trans [where m="a" and n="b" and k="l"])
next
case (goal4 l f g k)
have "divideallc (l,g)" using prems by clarsimp
moreover have "divideallc (l,f)" using prems by clarsimp
ultimately
show ?case by simp
next
case (goal5 l f g k)
have "divideallc (l,g)" using prems by clarsimp
moreover have "divideallc (l,f)" using prems by clarsimp
ultimately
show ?case by simp
qed
(* fomlcm retuns a number all coeffitients of Var 0 divide *)
lemma formlcm_divideallc:
assumes linp: "islinform p"
shows "divideallc(formlcm p, p)"
using linp
proof (induct p rule: formlcm.induct, simp_all add: zdvd_self_abs1)
case (goal1 f)
show ?case using prems
by (cases f,auto) (case_tac "intterm2", auto, case_tac "intterm1",auto)
next
case (goal2 f g)
have "formlcm f >0" using formlcm_pos prems by simp
hence "formlcm f \<noteq> 0" by simp
moreover have "formlcm g > 0" using formlcm_pos prems by simp
hence "formlcm g \<noteq> 0" by simp
ultimately
show ?case using prems formlcm_pos
by (simp add: ilcm_dvd1 ilcm_dvd2
divideallc_mono[where c="formlcm f" and d="ilcm (formlcm f) (formlcm g)"]
divideallc_mono[where c="formlcm g" and d="ilcm (formlcm f) (formlcm g)"])
next
case (goal3 f g)
have "formlcm f >0" using formlcm_pos prems by simp
hence "formlcm f \<noteq> 0" by simp
moreover have "formlcm g > 0" using formlcm_pos prems by simp
hence "formlcm g \<noteq> 0" by simp
ultimately
show ?case using prems
by (simp add: ilcm_dvd1 ilcm_dvd2
divideallc_mono[where c="formlcm f" and d="ilcm (formlcm f) (formlcm g)"]
divideallc_mono[where c="formlcm g" and d="ilcm (formlcm f) (formlcm g)"])
qed
(* adjustcoeff transforms the formula given an l , look at correctness thm*)
consts adjustcoeff :: "int \<times> QF \<Rightarrow> QF"
recdef adjustcoeff "measure (\<lambda>(l,p). size p)"
"adjustcoeff (l,(Le (Add (Mult (Cst c) (Var 0)) r) (Cst i))) =
(if c\<le>0 then
Le (Add (Mult (Cst -1) (Var 0)) (lin_mul (- (l div c), r))) (Cst (0::int))
else
Le (Add (Mult (Cst 1) (Var 0)) (lin_mul (l div c, r))) (Cst (0::int)))"
"adjustcoeff (l,(Eq (Add (Mult (Cst c) (Var 0)) r) (Cst i))) =
(Eq (Add (Mult (Cst 1) (Var 0)) (lin_mul (l div c, r))) (Cst (0::int)))"
"adjustcoeff (l,Divides (Cst d) (Add (Mult (Cst c) (Var 0)) r)) =
Divides (Cst ((l div c) * d))
(Add (Mult (Cst 1) (Var 0)) (lin_mul (l div c, r)))"
"adjustcoeff (l,NOT (Divides (Cst d) (Add (Mult (Cst c) (Var 0)) r))) = NOT (Divides (Cst ((l div c) * d))
(Add (Mult (Cst 1) (Var 0)) (lin_mul (l div c, r))))"
"adjustcoeff (l,(NOT(Eq (Add (Mult (Cst c) (Var 0)) r) (Cst i)))) =
(NOT(Eq (Add (Mult (Cst 1) (Var 0)) (lin_mul (l div c, r))) (Cst (0::int))))"
"adjustcoeff (l,And p q) = And (adjustcoeff (l,p)) (adjustcoeff(l,q))"
"adjustcoeff (l,Or p q) = Or (adjustcoeff (l,p)) (adjustcoeff(l,q))"
"adjustcoeff (l,p) = p"
(* unitycoeff expects a quantifier free formula an transforms it to an equivalent formula where the bound variable occurs only with coeffitient 1 or -1 *)
definition
unitycoeff :: "QF \<Rightarrow> QF"
"unitycoeff p =
(let l = formlcm p;
p' = adjustcoeff (l,p)
in (if l=1 then p' else
(And (Divides (Cst l) (Add (Mult (Cst 1) (Var 0)) (Cst 0))) p')))"
(* what is a unified formula *)
consts isunified :: "QF \<Rightarrow> bool"
recdef isunified "measure size"
"isunified (Le (Add (Mult (Cst i) (Var 0)) r) (Cst z)) =
((abs i) = 1 \<and> (islinform(Le (Add (Mult (Cst i) (Var 0)) r) (Cst z))))"
"isunified (Eq (Add (Mult (Cst i) (Var 0)) r) (Cst z)) =
((abs i) = 1 \<and> (islinform(Le (Add (Mult (Cst i) (Var 0)) r) (Cst z))))"
"isunified (NOT(Eq (Add (Mult (Cst i) (Var 0)) r) (Cst z))) =
((abs i) = 1 \<and> (islinform(Le (Add (Mult (Cst i) (Var 0)) r) (Cst z))))"
"isunified (Divides (Cst d) (Add (Mult (Cst i) (Var 0)) r)) =
((abs i) = 1 \<and> (islinform(Divides (Cst d) (Add (Mult (Cst i) (Var 0)) r))))"
"isunified (NOT(Divides (Cst d) (Add (Mult (Cst i) (Var 0)) r))) =
((abs i) = 1 \<and> (islinform(NOT(Divides (Cst d) (Add (Mult (Cst i) (Var 0)) r)))))"
"isunified (And p q) = (isunified p \<and> isunified q)"
"isunified (Or p q) = (isunified p \<and> isunified q)"
"isunified p = islinform p"
lemma unified_islinform: "isunified p \<Longrightarrow> islinform p"
by (induct p rule: isunified.induct) auto
lemma adjustcoeff_lenpos:
"0 < n \<Longrightarrow> adjustcoeff (l, Le (Add (Mult (Cst i) (Var n)) r) (Cst c)) =
Le (Add (Mult (Cst i) (Var n)) r) (Cst c)"
by (cases n, auto)
lemma adjustcoeff_eqnpos:
"0 < n \<Longrightarrow> adjustcoeff (l, Eq (Add (Mult (Cst i) (Var n)) r) (Cst c)) =
Eq (Add (Mult (Cst i) (Var n)) r) (Cst c)"
by (cases n, auto)
(* Properties of adjustcoeff and unitycoeff *)
(* Some simple lemmas used afterwards *)
lemma zmult_zle_mono: "(i::int) \<le> j \<Longrightarrow> 0 \<le> k \<Longrightarrow> k * i \<le> k * j"
apply (erule order_le_less [THEN iffD1, THEN disjE, of "0::int"])
apply (erule order_le_less [THEN iffD1, THEN disjE])
apply (rule order_less_imp_le)
apply (rule zmult_zless_mono2)
apply simp_all
done
lemma zmult_zle_mono_eq:
assumes kpos: "0 < k"
shows "((i::int) \<le> j) = (k*i \<le> k*j)" (is "?P = ?Q")
proof
assume P: ?P
from kpos have kge0: "0 \<le> k" by simp
show ?Q
by (rule zmult_zle_mono[OF P kge0])
next
assume ?Q
then have "k*i - k*j \<le> 0" by simp
then have le1: "k*(i-j) \<le> k*0"
by (simp add: zdiff_zmult_distrib2)
have "i -j \<le> 0"
by (rule mult_left_le_imp_le[OF le1 kpos])
then
show ?P by simp
qed
lemma adjustcoeff_le_corr:
assumes lpos: "0 < l"
and ipos: "0 < (i::int)"
and dvd: "i dvd l"
shows "(i*x + r \<le> 0) = (l*x + ((l div i)*r) \<le> 0)"
proof-
from lpos ipos have ilel: "i\<le>l" by (simp add: zdvd_imp_le [OF dvd lpos])
from ipos have inz: "i \<noteq> 0" by simp
have "i div i\<le> l div i"
by (simp add: zdiv_mono1[OF ilel ipos])
then have ldivipos:"0 < l div i"
by (simp add: zdiv_self[OF inz])
from dvd have "\<exists>i'. i*i' = l" by (auto simp add: dvd_def)
then obtain "i'" where ii'eql: "i*i' = l" by blast
have "(i * x + r \<le> 0) = (l div i * (i * x + r) \<le> l div i * 0)"
by (rule zmult_zle_mono_eq[OF ldivipos, where i="i*x + r" and j="0"])
also
have "(l div i * (i * x + r) \<le> l div i * 0) = ((l div i * i) * x + ((l div i)*r) \<le> 0)"
by (simp add: mult_ac)
also have "((l div i * i) * x + ((l div i)*r) \<le> 0) = (l*x + ((l div i)*r) \<le> 0)"
using sym[OF ii'eql] inz
by (simp add: zmult_ac)
finally
show ?thesis
by simp
qed
lemma adjustcoeff_le_corr2:
assumes lpos: "0 < l"
and ineg: "(i::int) < 0"
and dvd: "i dvd l"
shows "(i*x + r \<le> 0) = ((-l)*x + ((-(l div i))*r) \<le> 0)"
proof-
from dvd have midvdl: "-i dvd l" by simp
from ineg have mipos: "0 < -i" by simp
from lpos ineg have milel: "-i\<le>l" by (simp add: zdvd_imp_le [OF midvdl lpos])
from ineg have inz: "i \<noteq> 0" by simp
have "l div i\<le> -i div i"
by (simp add: zdiv_mono1_neg[OF milel ineg])
then have "l div i \<le> -1"
apply (simp add: zdiv_zminus1_eq_if[OF inz, where a="i"])
by (simp add: zdiv_self[OF inz])
then have ldivineg: "l div i < 0" by simp
then have mldivipos: "0 < - (l div i)" by simp
from dvd have "\<exists>i'. i*i' = l" by (auto simp add: dvd_def)
then obtain "i'" where ii'eql: "i*i' = l" by blast
have "(i * x + r \<le> 0) = (- (l div i) * (i * x + r) \<le> - (l div i) * 0)"
by (rule zmult_zle_mono_eq[OF mldivipos, where i="i*x + r" and j="0"])
also
have "(- (l div i) * (i * x + r) \<le> - (l div i) * 0) = (-((l div i) * i) * x \<le> (l div i)*r)"
by (simp add: mult_ac)
also have " (-((l div i) * i) * x \<le> (l div i)*r) = (- (l*x) \<le> (l div i)*r)"
using sym[OF ii'eql] inz
by (simp add: zmult_ac)
finally
show ?thesis
by simp
qed
(* FIXME : Move this theorem above, it simplifies the 2 theorems above : adjustcoeff_le_corr1,2 *)
lemma dvd_div_pos:
assumes bpos: "0 < (b::int)"
and anz: "a\<noteq>0"
and dvd: "a dvd b"
shows "(b div a)*a = b"
proof-
from anz have "0 < a \<or> a < 0" by arith
moreover
{
assume apos: "0 < a"
from bpos apos have aleb: "a\<le>b" by (simp add: zdvd_imp_le [OF dvd bpos])
have "a div a\<le> b div a"
by (simp add: zdiv_mono1[OF aleb apos])
then have bdivapos:"0 < b div a"
by (simp add: zdiv_self[OF anz])
from dvd have "\<exists>a'. a*a' = b" by (auto simp add: dvd_def)
then obtain "a'" where aa'eqb: "a*a' = b" by blast
then have ?thesis using anz sym[OF aa'eqb] by simp
}
moreover
{
assume aneg: "a < 0"
from dvd have midvdb: "-a dvd b" by simp
from aneg have mapos: "0 < -a" by simp
from bpos aneg have maleb: "-a\<le>b" by (simp add: zdvd_imp_le [OF midvdb bpos])
from aneg have anz: "a \<noteq> 0" by simp
have "b div a\<le> -a div a"
by (simp add: zdiv_mono1_neg[OF maleb aneg])
then have "b div a \<le> -1"
apply (simp add: zdiv_zminus1_eq_if[OF anz, where a="a"])
by (simp add: zdiv_self[OF anz])
then have bdivaneg: "b div a < 0" by simp
then have mbdivapos: "0 < - (b div a)" by simp
from dvd have "\<exists>a'. a*a' = b" by (auto simp add: dvd_def)
then obtain "a'" where aa'eqb: "a*a' = b" by blast
then have ?thesis using anz sym[OF aa'eqb] by (simp)
}
ultimately show ?thesis by blast
qed
lemma adjustcoeff_eq_corr:
assumes lpos: "(0::int) < l"
and inz: "i \<noteq> 0"
and dvd: "i dvd l"
shows "(i*x + r = 0) = (l*x + ((l div i)*r) = 0)"
proof-
have ldvdii: "(l div i)*i = l" by (rule dvd_div_pos[OF lpos inz dvd])
have ldivinz: "l div i \<noteq> 0" using inz ldvdii lpos by auto
have "(i*x + r = 0) = ((l div i)*(i*x + r) = (l div i)*0)"
using ldivinz by arith
also have "\<dots> = (((l div i)*i)*x + (l div i)*r = 0)"
by (simp add: zmult_ac)
finally show ?thesis using ldvdii by simp
qed
(* Correctness theorem for adjustcoeff *)
lemma adjustcoeff_corr:
assumes linp: "islinform p"
and alldvd: "divideallc (l,p)"
and lpos: "0 < l"
shows "qinterp (a#ats) p = qinterp ((a*l)#ats) (adjustcoeff(l, p))"
using linp alldvd
proof (induct p rule: islinform.induct,simp_all)
case (goal1 t c)
from prems have cz: "c=0" by simp
then have ?case
using prems
proof(induct t rule: islinintterm.induct)
case (2 i n i') show ?case using prems
proof-
from prems have "i\<noteq>0" by simp
then
have "(n=0 \<and> i < 0) \<or> (n=0 \<and> i > 0) \<or> n\<noteq>0" by arith
moreover
{
assume "n\<noteq>0" then have ?thesis
by (simp add: nth_pos2 adjustcoeff_lenpos)
}
moreover
{
assume nz: "n=0"
and ipos: "0 < i"
from prems nz have idvdl: "i dvd l" by simp
have "(i*a + i' \<le> 0) = (l*a+ ((l div i)*i') \<le> 0)"
by (rule adjustcoeff_le_corr[OF lpos ipos idvdl])
then
have ?thesis using prems by (simp add: mult_ac)
}
moreover
{
assume nz: "n=0"
and ineg: "i < 0"
from prems nz have idvdl: "i dvd l" by simp
have "(i*a+i' \<le> 0) = (-l*a + (-(l div i) * i') \<le> 0)"
by (rule adjustcoeff_le_corr2[OF lpos ineg idvdl])
then
have ?thesis using prems
by (simp add: zmult_ac)
}
ultimately show ?thesis by blast
qed
next
case (3 i n i' n' r) show ?case using prems
proof-
from prems
have lininrp: "islinintterm (Add (Mult (Cst i') (Var n')) r)"
by simp
then
have "islint (Add (Mult (Cst i') (Var n')) (r))"
by (simp add: islinintterm_eq_islint)
then have linr: "islintn(Suc n',r)"
by (simp add: islinintterm_subt[OF lininrp] islinintterm_eq_islint islint_def)
from lininrp have linr2: "islinintterm r"
by (simp add: islinintterm_subt[OF lininrp])
from prems have "n < n'" by simp
then have nppos: "0 < n'" by simp
from prems have "i\<noteq>0" by simp
then
have "(n=0 \<and> i < 0) \<or> (n=0 \<and> i > 0) \<or> n\<noteq>0" by arith
moreover
{
assume nnz: "n\<noteq>0"
from linr have ?thesis using nppos nnz intterm_novar0[OF lininrp] prems
apply (simp add: adjustcoeff_lenpos linterm_novar0[OF linr, where x="a" and y="a*l"])
by (simp add: nth_pos2)
}
moreover
{
assume nz: "n=0"
and ipos: "0 < i"
from prems nz have idvdl: "i dvd l" by simp
have "(i * a + (i' * (a # ats) ! n' + I_intterm (a # ats) r) \<le> 0) =
(l * a + l div i * (i' * (a # ats) ! n' + I_intterm (a # ats) r) \<le> 0)"
by (rule adjustcoeff_le_corr[OF lpos ipos idvdl])
then
have ?thesis using prems linr linr2
by (simp add: mult_ac nth_pos2 lin_mul_corr
linterm_novar0[OF linr, where x="a" and y="a*l"])
}
moreover
{
assume nz: "n=0"
and ineg: "i < 0"
from prems nz have idvdl: "i dvd l" by simp
have "(i * a + (i' * (a # ats) ! n' + I_intterm (a # ats) r) \<le> 0) =
(- l * a + - (l div i) * (i' * (a # ats) ! n' + I_intterm (a # ats) r) \<le> 0)"
by (rule adjustcoeff_le_corr2[OF lpos ineg idvdl, where x="a" and r="(i'* (a#ats) ! n' + I_intterm (a#ats) r )"])
then
have ?thesis using prems linr linr2
by (simp add: zmult_ac nth_pos2 lin_mul_corr
linterm_novar0[OF linr, where x="a" and y="a*l"] )
}
ultimately show ?thesis by blast
qed
qed simp_all
then show ?case by simp
next
case (goal2 t c)
from prems have cz: "c=0" by simp
then have ?case
using prems
proof(induct t rule: islinintterm.induct)
case (2 i n i') show ?case using prems
proof-
from prems have inz: "i\<noteq>0" by simp
then
have "n=0 \<or> n\<noteq>0" by arith
moreover
{
assume "n\<noteq>0" then have ?thesis
by (simp add: nth_pos2 adjustcoeff_eqnpos)
}
moreover
{
assume nz: "n=0"
from prems nz have idvdl: "i dvd l" by simp
have "(i*a + i' = 0) = (l*a+ ((l div i)*i') = 0)"
by (rule adjustcoeff_eq_corr[OF lpos inz idvdl])
then
have ?thesis using prems by (simp add: mult_ac)
}
ultimately show ?thesis by blast
qed
next
case (3 i n i' n' r) show ?case using prems
proof-
from prems
have lininrp: "islinintterm (Add (Mult (Cst i') (Var n')) r)"
by simp
then
have "islint (Add (Mult (Cst i') (Var n')) (r))"
by (simp add: islinintterm_eq_islint)
then have linr: "islintn(Suc n',r)"
by (simp add: islinintterm_subt[OF lininrp] islinintterm_eq_islint islint_def)
from lininrp have linr2: "islinintterm r"
by (simp add: islinintterm_subt[OF lininrp])
from prems have "n < n'" by simp
then have nppos: "0 < n'" by simp
from prems have "i\<noteq>0" by simp
then
have "n=0 \<or> n\<noteq>0" by arith
moreover
{
assume nnz: "n\<noteq>0"
from linr have ?thesis using nppos nnz intterm_novar0[OF lininrp] prems
apply (simp add: adjustcoeff_eqnpos linterm_novar0[OF linr, where x="a" and y="a*l"])
by (simp add: nth_pos2)
}
moreover
{
assume nz: "n=0"
from prems have inz: "i \<noteq> 0" by auto
from prems nz have idvdl: "i dvd l" by simp
have "(i * a + (i' * (a # ats) ! n' + I_intterm (a # ats) r) = 0) =
(l * a + l div i * (i' * (a # ats) ! n' + I_intterm (a # ats) r) = 0)"
by (rule adjustcoeff_eq_corr[OF lpos inz idvdl])
then
have ?thesis using prems linr linr2
by (simp add: mult_ac nth_pos2 lin_mul_corr
linterm_novar0[OF linr, where x="a" and y="a*l"])
}
ultimately show ?thesis by blast
qed
qed simp_all
then show ?case by simp
next
case (goal3 d t) show ?case
using prems
proof (induct t rule: islinintterm.induct)
case (2 i n i')
have "n=0 \<or> (\<exists>m. (n = Suc m))" by arith
moreover
{
assume "\<exists>m. n = Suc m"
then have ?case using prems by auto
}
moreover
{
assume nz: "n=0"
from prems have inz: "i\<noteq>0" by simp
from prems have idvdl: "i dvd l" by simp
have ldiviieql: "l div i * i = l" by (rule dvd_div_pos[OF lpos inz idvdl])
with lpos have ldivinz: "0 \<noteq> l div i" by auto
then have ?case using prems
apply simp
apply (simp add:
ac_dvd_eq[OF ldivinz, where m="d" and c="i" and n="a" and t="i'"]
ldiviieql)
by (simp add: zmult_commute)
}
ultimately show ?case by blast
next
case (3 i n i' n' r)
from prems
have lininrp: "islinintterm (Add (Mult (Cst i') (Var n')) r)"
by simp
then
have "islint (Add (Mult (Cst i') (Var n')) (r))"
by (simp add: islinintterm_eq_islint)
then have linr: "islintn(Suc n',r)"
by (simp add: islinintterm_subt[OF lininrp] islinintterm_eq_islint islint_def)
from lininrp have linr2: "islinintterm r"
by (simp add: islinintterm_subt[OF lininrp])
from prems have "n < n'" by simp
then have nppos: "0 < n'" by simp
from prems have inz: "i\<noteq>0" by simp
have "n=0 \<or> (\<exists>m. (n = Suc m))" by arith
moreover
{
assume "\<exists>m. n = Suc m"
then have npos: "0 < n" by arith
have ?case using nppos intterm_novar0[OF lininrp] prems
apply (auto simp add: linterm_novar0[OF linr, where x="a" and y="a*l"])
by (simp_all add: nth_pos2)
}
moreover
{
assume nz: "n=0"
from prems have idvdl: "i dvd l" by simp
have ldiviieql: "l div i * i = l" by (rule dvd_div_pos[OF lpos inz idvdl])
with lpos have ldivinz: "0 \<noteq> l div i" by auto
then have ?case using prems linr2 linr
apply (simp add: nth_pos2 lin_mul_corr linterm_novar0)
apply (simp add: ac_dvd_eq[OF ldivinz, where m="d" and c="i" and n="a" and t="(i' * ats ! (n' - Suc 0) + I_intterm (a # ats) r)"] ldiviieql)
by (simp add: zmult_ac linterm_novar0[OF linr, where x="a" and y="a*l"])
}
ultimately show ?case by blast
qed simp_all
next
case (goal4 d t) show ?case
using prems
proof (induct t rule: islinintterm.induct)
case (2 i n i')
have "n=0 \<or> (\<exists>m. (n = Suc m))" by arith
moreover
{
assume "\<exists>m. n = Suc m"
then have ?case using prems by auto
}
moreover
{
assume nz: "n=0"
from prems have inz: "i\<noteq>0" by simp
from prems have idvdl: "i dvd l" by simp
have ldiviieql: "l div i * i = l" by (rule dvd_div_pos[OF lpos inz idvdl])
with lpos have ldivinz: "0 \<noteq> l div i" by auto
then have ?case using prems
apply simp
apply (simp add:
ac_dvd_eq[OF ldivinz, where m="d" and c="i" and n="a" and t="i'"]
ldiviieql)
by (simp add: zmult_commute)
}
ultimately show ?case by blast
next
case (3 i n i' n' r)
from prems
have lininrp: "islinintterm (Add (Mult (Cst i') (Var n')) r)"
by simp
then
have "islint (Add (Mult (Cst i') (Var n')) (r))"
by (simp add: islinintterm_eq_islint)
then have linr: "islintn(Suc n',r)"
by (simp add: islinintterm_subt[OF lininrp] islinintterm_eq_islint islint_def)
from lininrp have linr2: "islinintterm r"
by (simp add: islinintterm_subt[OF lininrp])
from prems have "n < n'" by simp
then have nppos: "0 < n'" by simp
from prems have inz: "i\<noteq>0" by simp
have "n=0 \<or> (\<exists>m. (n = Suc m))" by arith
moreover
{
assume "\<exists>m. n = Suc m"
then have npos: "0 < n" by arith
have ?case using nppos intterm_novar0[OF lininrp] prems
apply (auto simp add: linterm_novar0[OF linr, where x="a" and y="a*l"])
by (simp_all add: nth_pos2)
}
moreover
{
assume nz: "n=0"
from prems have idvdl: "i dvd l" by simp
have ldiviieql: "l div i * i = l" by (rule dvd_div_pos[OF lpos inz idvdl])
with lpos have ldivinz: "0 \<noteq> l div i" by auto
then have ?case using prems linr2 linr
apply (simp add: nth_pos2 lin_mul_corr linterm_novar0)
apply (simp add: ac_dvd_eq[OF ldivinz, where m="d" and c="i" and n="a" and t="(i' * ats ! (n' - Suc 0) + I_intterm (a # ats) r)"] ldiviieql)
by (simp add: zmult_ac linterm_novar0[OF linr, where x="a" and y="a*l"])
}
ultimately show ?case by blast
qed simp_all
next
case (goal5 t c)
from prems have cz: "c=0" by simp
then have ?case
using prems
proof(induct t rule: islinintterm.induct)
case (2 i n i') show ?case using prems
proof-
from prems have inz: "i\<noteq>0" by simp
then
have "n=0 \<or> n\<noteq>0" by arith
moreover
{
assume "n\<noteq>0" then have ?thesis
using prems
by (cases n, simp_all)
}
moreover
{
assume nz: "n=0"
from prems nz have idvdl: "i dvd l" by simp
have "(i*a + i' = 0) = (l*a+ ((l div i)*i') = 0)"
by (rule adjustcoeff_eq_corr[OF lpos inz idvdl])
then
have ?thesis using prems by (simp add: mult_ac)
}
ultimately show ?thesis by blast
qed
next
case (3 i n i' n' r) show ?case using prems
proof-
from prems
have lininrp: "islinintterm (Add (Mult (Cst i') (Var n')) r)"
by simp
then
have "islint (Add (Mult (Cst i') (Var n')) (r))"
by (simp add: islinintterm_eq_islint)
then have linr: "islintn(Suc n',r)"
by (simp add: islinintterm_subt[OF lininrp] islinintterm_eq_islint islint_def)
from lininrp have linr2: "islinintterm r"
by (simp add: islinintterm_subt[OF lininrp])
from prems have "n < n'" by simp
then have nppos: "0 < n'" by simp
from prems have "i\<noteq>0" by simp
then
have "n=0 \<or> n\<noteq>0" by arith
moreover
{
assume nnz: "n\<noteq>0"
then have ?thesis using prems linr nppos nnz intterm_novar0[OF lininrp]
by (cases n, simp_all)
(simp add: nth_pos2 linterm_novar0[OF linr, where x="a" and y="a*l"])
}
moreover
{
assume nz: "n=0"
from prems have inz: "i \<noteq> 0" by auto
from prems nz have idvdl: "i dvd l" by simp
have "(i * a + (i' * (a # ats) ! n' + I_intterm (a # ats) r) = 0) =
(l * a + l div i * (i' * (a # ats) ! n' + I_intterm (a # ats) r) = 0)"
by (rule adjustcoeff_eq_corr[OF lpos inz idvdl])
then
have ?thesis using prems linr linr2
by (simp add: mult_ac nth_pos2 lin_mul_corr
linterm_novar0[OF linr, where x="a" and y="a*l"])
}
ultimately show ?thesis by blast
qed
qed simp_all
then show ?case by simp
qed
(* unitycoeff preserves semantics *)
lemma unitycoeff_corr:
assumes linp: "islinform p"
shows "qinterp ats (QEx p) = qinterp ats (QEx (unitycoeff p))"
proof-
have lpos: "0 < formlcm p" by (rule formlcm_pos[OF linp])
have dvd : "divideallc (formlcm p, p)" by (rule formlcm_divideallc[OF linp])
show ?thesis using prems lpos dvd
proof (simp add: unitycoeff_def Let_def,case_tac "formlcm p = 1",
simp_all add: adjustcoeff_corr)
show "(\<exists>x. qinterp (x * formlcm p # ats) (adjustcoeff (formlcm p, p))) =
(\<exists>x. formlcm p dvd x \<and>
qinterp (x # ats) (adjustcoeff (formlcm p, p)))"
(is "(\<exists>x. ?P(x* (formlcm p))) = (\<exists>x. formlcm p dvd x \<and> ?P x)")
proof-
have "(\<exists>x. ?P(x* (formlcm p))) = (\<exists>x. ?P((formlcm p)*x))"
by (simp add: mult_commute)
also have "(\<exists>x. ?P((formlcm p)*x)) = (\<exists>x. (formlcm p dvd x) \<and> ?P x)"
by (simp add: unity_coeff_ex[where P="?P"])
finally show ?thesis by simp
qed
qed
qed
(* the resul of adjustcoeff is unified for all l with divideallc (l,p) *)
lemma adjustcoeff_unified:
assumes linp: "islinform p"
and dvdc: "divideallc(l,p)"
and lpos: "l > 0"
shows "isunified (adjustcoeff(l, p))"
using linp dvdc lpos
proof(induct l p rule: adjustcoeff.induct,simp_all add: lin_mul_lintn islinintterm_eq_islint islint_def)
case (goal1 l d c r)
from prems have "c >0 \<or> c < 0" by auto
moreover {
assume cpos: "c > 0 "
from prems have lp: "l > 0" by simp
from prems have cdvdl: "c dvd l" by simp
have clel: "c \<le> l" by (rule zdvd_imp_le[OF cdvdl lp])
have "c div c \<le> l div c" by (rule zdiv_mono1[OF clel cpos])
then have ?case using cpos by (simp add: zdiv_self)
}
moreover {
assume cneg: "c < 0"
have mcpos: "-c > 0" by simp
then have mcnz: "-c \<noteq> 0" by simp
from prems have mcdvdl: "-c dvd l"
by simp
then have l1:"l mod -c = 0" by (simp add: zdvd_iff_zmod_eq_0)
from prems have lp: "l >0" by simp
have mclel: "-c \<le> l" by (rule zdvd_imp_le[OF mcdvdl lp])
have "l div c = (-l div -c)" by simp
also have "\<dots> = - (l div -c)" using l1
by (simp only: zdiv_zminus1_eq_if[OF mcnz, where a="l"]) simp
finally have diveq: "l div c = - (l div -c)" by simp
have "-c div -c \<le> l div -c" by (rule zdiv_mono1[OF mclel mcpos])
then have "0 < l div -c" using cneg
by (simp add: zdiv_self)
then have ?case using diveq by simp
}
ultimately show ?case by blast
next
case (goal2 l p) from prems have "c >0 \<or> c < 0" by auto
moreover {
assume cpos: "c > 0 "
from prems have lp: "l > 0" by simp
from prems have cdvdl: "c dvd l" by simp
have clel: "c \<le> l" by (rule zdvd_imp_le[OF cdvdl lp])
have "c div c \<le> l div c" by (rule zdiv_mono1[OF clel cpos])
then have ?case using cpos by (simp add: zdiv_self)
}
moreover {
assume cneg: "c < 0"
have mcpos: "-c > 0" by simp
then have mcnz: "-c \<noteq> 0" by simp
from prems have mcdvdl: "-c dvd l"
by simp
then have l1:"l mod -c = 0" by (simp add: zdvd_iff_zmod_eq_0)
from prems have lp: "l >0" by simp
have mclel: "-c \<le> l" by (rule zdvd_imp_le[OF mcdvdl lp])
have "l div c = (-l div -c)" by simp
also have "\<dots> = - (l div -c)" using l1
by (simp only: zdiv_zminus1_eq_if[OF mcnz, where a="l"]) simp
finally have diveq: "l div c = - (l div -c)" by simp
have "-c div -c \<le> l div -c" by (rule zdiv_mono1[OF mclel mcpos])
then have "0 < l div -c" using cneg
by (simp add: zdiv_self)
then have ?case using diveq by simp
}
ultimately show ?case by blast
qed
lemma adjustcoeff_lcm_unified:
assumes linp: "islinform p"
shows "isunified (adjustcoeff(formlcm p, p))"
using linp adjustcoeff_unified formlcm_pos formlcm_divideallc
by simp
(* the result of unitycoeff is unified *)
lemma unitycoeff_unified:
assumes linp: "islinform p"
shows "isunified (unitycoeff p)"
using linp formlcm_pos[OF linp]
proof (auto simp add: unitycoeff_def Let_def adjustcoeff_lcm_unified)
assume f1: "formlcm p = 1"
have "isunified (adjustcoeff(formlcm p, p))"
by (rule adjustcoeff_lcm_unified[OF linp])
with f1
show "isunified (adjustcoeff(1,p))" by simp
qed
lemma unified_isnnf:
assumes unifp: "isunified p"
shows "isnnf p"
using unified_islinform[OF unifp] linform_isnnf
by simp
lemma unified_isqfree: "isunified p\<Longrightarrow> isqfree p"
using unified_islinform linform_isqfree
by auto
(* Plus/Minus infinity , B and A set definitions *)
consts minusinf :: "QF \<Rightarrow> QF"
plusinf :: "QF \<Rightarrow> QF"
aset :: "QF \<Rightarrow> intterm list"
bset :: "QF \<Rightarrow> intterm list"
recdef minusinf "measure size"
"minusinf (Le (Add (Mult (Cst c) (Var 0)) r) z) =
(if c < 0 then F else T)"
"minusinf (Eq (Add (Mult (Cst c) (Var 0)) r) z) = F"
"minusinf (NOT(Eq (Add (Mult (Cst c) (Var 0)) r) z)) = T"
"minusinf (And p q) = And (minusinf p) (minusinf q)"
"minusinf (Or p q) = Or (minusinf p) (minusinf q)"
"minusinf p = p"
recdef plusinf "measure size"
"plusinf (Le (Add (Mult (Cst c) (Var 0)) r) z) =
(if c < 0 then T else F)"
"plusinf (Eq (Add (Mult (Cst c) (Var 0)) r) z) = F"
"plusinf (NOT (Eq (Add (Mult (Cst c) (Var 0)) r) z)) = T"
"plusinf (And p q) = And (plusinf p) (plusinf q)"
"plusinf (Or p q) = Or (plusinf p) (plusinf q)"
"plusinf p = p"
recdef bset "measure size"
"bset (Le (Add (Mult (Cst c) (Var 0)) r) z) =
(if c < 0 then [lin_add(r,(Cst -1)), r]
else [lin_add(lin_neg r,(Cst -1))])"
"bset (Eq (Add (Mult (Cst c) (Var 0)) r) z) =
(if c < 0 then [lin_add(r,(Cst -1))]
else [lin_add(lin_neg r,(Cst -1))])"
"bset (NOT(Eq (Add (Mult (Cst c) (Var 0)) r) z)) =
(if c < 0 then [r]
else [lin_neg r])"
"bset (And p q) = (bset p) @ (bset q)"
"bset (Or p q) = (bset p) @ (bset q)"
"bset p = []"
recdef aset "measure size"
"aset (Le (Add (Mult (Cst c) (Var 0)) r) z) =
(if c < 0 then [lin_add (r, Cst 1)]
else [lin_add (lin_neg r, Cst 1), lin_neg r])"
"aset (Eq (Add (Mult (Cst c) (Var 0)) r) z) =
(if c < 0 then [lin_add(r,(Cst 1))]
else [lin_add(lin_neg r,(Cst 1))])"
"aset (NOT(Eq (Add (Mult (Cst c) (Var 0)) r) z)) =
(if c < 0 then [r]
else [lin_neg r])"
"aset (And p q) = (aset p) @ (aset q)"
"aset (Or p q) = (aset p) @ (aset q)"
"aset p = []"
(* divlcm computes \<delta> = lcm d , where d | x +t occurs in p *)
consts divlcm :: "QF \<Rightarrow> int"
recdef divlcm "measure size"
"divlcm (Divides (Cst d) (Add (Mult (Cst c) (Var 0)) r)) = (abs d)"
"divlcm (NOT p) = divlcm p"
"divlcm (And p q)= ilcm (divlcm p) (divlcm q)"
"divlcm (Or p q) = ilcm (divlcm p) (divlcm q)"
"divlcm p = 1"
(* the preoperty of \<delta> *)
consts alldivide :: "int \<times> QF \<Rightarrow> bool"
recdef alldivide "measure (%(d,p). size p)"
"alldivide (d,(Divides (Cst d') (Add (Mult (Cst c) (Var 0)) r))) =
(d' dvd d)"
"alldivide (d,(NOT p)) = alldivide (d,p)"
"alldivide (d,(And p q)) = (alldivide (d,p) \<and> alldivide (d,q))"
"alldivide (d,(Or p q)) = ((alldivide (d,p)) \<and> (alldivide (d,q)))"
"alldivide (d,p) = True"
(* alldivide is monotone *)
lemma alldivide_mono: "\<And> d'. \<lbrakk> alldivide (d,p) ; d dvd d'\<rbrakk> \<Longrightarrow> alldivide (d',p)"
proof(induct d p rule: alldivide.induct, simp_all add: ilcm_dvd1 ilcm_dvd2)
fix "d1" "d2" "d3"
assume th1:"d2 dvd (d1::int)"
and th2: "d1 dvd d3"
show "d2 dvd d3" by (rule zdvd_trans[OF th1 th2])
qed
(* Some simple lemmas *)
lemma zdvd_eq_zdvd_abs: " (d::int) dvd d' = (d dvd (abs d')) "
proof-
have "d' < 0 \<or> d' \<ge> 0" by arith
moreover
{
assume dn': "d' < 0"
then have "abs d' = - d'" by simp
then
have ?thesis by (simp)
}
moreover
{
assume dp': "d' \<ge> 0"
then have "abs d' = d'" by simp
then have ?thesis by simp
}
ultimately show ?thesis by blast
qed
lemma zdvd_refl_abs: "(d::int) dvd (abs d)"
proof-
have "d dvd d" by simp
then show ?thesis by (simp add: iffD1 [OF zdvd_eq_zdvd_abs [where d = "d" and d'="d"]])
qed
(* \<delta> > 0*)
lemma divlcm_pos:
assumes
linp: "islinform p"
shows "0 < divlcm p"
using linp
proof (induct p rule: divlcm.induct,simp_all add: ilcm_pos)
case (goal1 f) show ?case
using prems
by (cases f, auto) (case_tac "intterm1", auto)
qed
lemma nz_le: "(x::int) > 0 \<Longrightarrow> x \<noteq> 0" by auto
(* divlcm is correct *)
lemma divlcm_corr:
assumes
linp: "islinform p"
shows "alldivide (divlcm p,p)"
using linp divlcm_pos
proof (induct p rule: divlcm.induct,simp_all add: zdvd_refl_abs,clarsimp simp add: Nat.gr0_conv_Suc)
case (goal1 f)
have "islinform f" using prems
by (cases f, auto) (case_tac "intterm2", auto,case_tac "intterm1", auto)
then have "alldivide (divlcm f, f)" using prems by simp
moreover have "divlcm (NOT f) = divlcm f" by simp
moreover have "alldivide (x,f) = alldivide (x,NOT f)" by simp
ultimately show ?case by simp
next
case (goal2 f g)
have dvd1: "(divlcm f) dvd (ilcm (divlcm f) (divlcm g))"
using prems by(simp add: ilcm_dvd1 nz_le)
have dvd2: "(divlcm g) dvd (ilcm (divlcm f) (divlcm g))"
using prems by (simp add: ilcm_dvd2 nz_le)
from dvd1 prems
have "alldivide (ilcm (divlcm f) (divlcm g), f)"
by (simp add: alldivide_mono[where d= "divlcm f" and p="f" and d' ="ilcm (divlcm f) (divlcm g)"])
moreover from dvd2 prems
have "alldivide (ilcm (divlcm f) (divlcm g), g)"
by (simp add: alldivide_mono[where d= "divlcm g" and p="g" and d' ="ilcm (divlcm f) (divlcm g)"])
ultimately show ?case by simp
next
case (goal3 f g)
have dvd1: "(divlcm f) dvd (ilcm (divlcm f) (divlcm g))"
using prems by (simp add: nz_le ilcm_dvd1)
have dvd2: "(divlcm g) dvd (ilcm (divlcm f) (divlcm g))"
using prems by (simp add: nz_le ilcm_dvd2)
from dvd1 prems
have "alldivide (ilcm (divlcm f) (divlcm g), f)"
by (simp add: alldivide_mono[where d= "divlcm f" and p="f" and d' ="ilcm (divlcm f) (divlcm g)"])
moreover from dvd2 prems
have "alldivide (ilcm (divlcm f) (divlcm g), g)"
by (simp add: alldivide_mono[where d= "divlcm g" and p="g" and d' ="ilcm (divlcm f) (divlcm g)"])
ultimately show ?case by simp
qed
(* Properties of minusinf and plusinf*)
(* minusinf p and p are the same for minusinfity \<dots> *)
lemma minusinf_eq:
assumes unifp: "isunified p"
shows "\<exists> z. \<forall> x. x < z \<longrightarrow> (qinterp (x#ats) p = qinterp (x#ats) (minusinf p))"
using unifp unified_islinform[OF unifp]
proof (induct p rule: minusinf.induct)
case (1 c r z)
have "c <0 \<or> 0 \<le> c" by arith
moreover
{
assume cneg: " c < 0"
from prems have z0: "z= Cst 0"
by (cases z,auto)
with prems have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)"
by simp
from prems z0 have ?case
proof-
show ?thesis
using prems z0
apply auto
apply (rule exI[where x="I_intterm (a # ats) r"])
apply (rule allI)
proof-
fix x
show "x < I_intterm (a # ats) r \<longrightarrow> \<not> - x + I_intterm (x # ats) r \<le> 0"
by (simp add: intterm_novar0[OF lincnr, where x="a" and y="x"])
qed
qed
}
moreover
{
assume cpos: "0 \<le> c"
from prems have z0: "z= Cst 0"
by (cases z) auto
with prems have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)"
by simp
from prems z0 have ?case
proof-
show ?thesis
using prems z0
apply auto
apply (rule exI[where x="-(I_intterm (a # ats) r)"])
apply (rule allI)
proof-
fix x
show "x < - I_intterm (a # ats) r \<longrightarrow> x + I_intterm (x # ats) r \<le> 0"
by (simp add: intterm_novar0[OF lincnr, where x="a" and y="x"])
qed
qed
}
ultimately show ?case by blast
next
case (2 c r z)
from prems have z0: "z= Cst 0"
by (cases z,auto)
with prems have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)"
by simp
have "c <0 \<or> 0 \<le> c" by arith
moreover
{
assume cneg: " c < 0"
from prems z0 have ?case
proof-
show ?thesis
using prems z0
apply auto
apply (rule exI[where x="I_intterm (a # ats) r"])
apply (rule allI)
proof-
fix x
show "x < I_intterm (a # ats) r \<longrightarrow> \<not> - x + I_intterm (x # ats) r = 0"
by (simp add: intterm_novar0[OF lincnr, where x="a" and y="x"])
qed
qed
}
moreover
{
assume cpos: "0 \<le> c"
from prems z0 have ?case
proof-
show ?thesis
using prems z0
apply auto
apply (rule exI[where x="-(I_intterm (a # ats) r)"])
apply (rule allI)
proof-
fix x
show "x < - I_intterm (a # ats) r \<longrightarrow> x + I_intterm (x # ats) r \<noteq> 0"
by (simp add: intterm_novar0[OF lincnr, where x="a" and y="x"])
qed
qed
}
ultimately show ?case by blast
next
case (3 c r z)
from prems have z0: "z= Cst 0"
by (cases z,auto)
with prems have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)"
by simp
have "c <0 \<or> 0 \<le> c" by arith
moreover
{
assume cneg: " c < 0"
from prems z0 have ?case
proof-
show ?thesis
using prems z0
apply auto
apply (rule exI[where x="I_intterm (a # ats) r"])
apply (rule allI)
proof-
fix x
show "x < I_intterm (a # ats) r \<longrightarrow> \<not> - x + I_intterm (x # ats) r = 0"
by (simp add: intterm_novar0[OF lincnr, where x="a" and y="x"])
qed
qed
}
moreover
{
assume cpos: "0 \<le> c"
from prems z0 have ?case
proof-
show ?thesis
using prems z0
apply auto
apply (rule exI[where x="-(I_intterm (a # ats) r)"])
apply (rule allI)
proof-
fix x
show "x < - I_intterm (a # ats) r \<longrightarrow> x + I_intterm (x # ats) r \<noteq> 0"
by (simp add: intterm_novar0[OF lincnr, where x="a" and y="x"])
qed
qed
}
ultimately show ?case by blast
next
case (4 f g)
from prems obtain "zf" where
zf:"\<forall>x<zf. qinterp (x # ats) f = qinterp (x # ats) (minusinf f)" by auto
from prems obtain "zg" where
zg:"\<forall>x<zg. qinterp (x # ats) g = qinterp (x # ats) (minusinf g)" by auto
from zf zg show ?case
apply auto
apply (rule exI[where x="min zf zg"])
by simp
next case (5 f g)
from prems obtain "zf" where
zf:"\<forall>x<zf. qinterp (x # ats) f = qinterp (x # ats) (minusinf f)" by auto
from prems obtain "zg" where
zg:"\<forall>x<zg. qinterp (x # ats) g = qinterp (x # ats) (minusinf g)" by auto
from zf zg show ?case
apply auto
apply (rule exI[where x="min zf zg"])
by simp
qed simp_all
(* miusinf p behaves periodically*)
lemma minusinf_repeats:
assumes alldvd: "alldivide (d,p)"
and unity: "isunified p"
shows "qinterp (x#ats) (minusinf p) = qinterp ((x + c*d)#ats) (minusinf p)"
using alldvd unity unified_islinform[OF unity]
proof(induct p rule: islinform.induct, simp_all)
case (goal1 t a)
show ?case
using prems
apply (cases t, simp_all add: nth_pos2)
apply (case_tac "intterm1", simp_all)
apply (case_tac "intterm1a",simp_all)
by (case_tac "intterm2a",simp_all)
(case_tac "nat",simp_all add: nth_pos2 intterm_novar0[where x="x" and y="x+c*d"])
next
case (goal2 t a)
show ?case
using prems
apply (cases t, simp_all add: nth_pos2)
apply (case_tac "intterm1", simp_all)
apply (case_tac "intterm1a",simp_all)
by (case_tac "intterm2a",simp_all)
(case_tac "nat",simp_all add: nth_pos2 intterm_novar0[where x="x" and y="x+c*d"])
next
case (goal3 a t)
show ?case using prems
proof(induct t rule: islinintterm.induct, simp_all add: nth_pos2)
case (goal1 i n i')
show ?case
using prems
proof(cases n, simp_all, case_tac "i=1", simp,
simp add: dvd_period[where a="a" and d="d" and x="x" and c="c"])
case goal1
from prems have "(abs i = 1) \<and> i \<noteq> 1" by auto
then have im1: "i=-1" by arith
then have "(a dvd i*x + i') = (a dvd x + (-i'))"
by (simp add: uminus_dvd_conv'[where d="a" and t="-x +i'"])
moreover
from im1 have "(a dvd i*x + (i*(c * d)) + i') = (a dvd (x + c*d - i'))"
apply simp
apply (simp add: uminus_dvd_conv'[where d="a" and t="-x - c * d + i'"])
by (simp add: zadd_ac)
ultimately
have eq1:"((a dvd i*x + i') = (a dvd i*x + (i*(c * d)) + i')) =
((a dvd x + (-i')) = (a dvd (x + c*d - i')))" by simp
moreover
have dvd2: "(a dvd x + (-i')) = (a dvd x + c * d + (-i'))"
by (rule dvd_period[where a="a" and d="d" and x="x" and c="c"], assumption)
ultimately show ?case by simp
qed
next
case (goal2 i n i' n' r)
have "n = 0 \<or> 0 < n" by arith
moreover
{
assume npos: "0 < n"
from prems have "n < n'" by simp then have "0 < n'" by simp
moreover from prems
have linr: "islinintterm (Add (Mult (Cst i') (Var n')) r)" by simp
ultimately have ?case
using prems npos
by (simp add: nth_pos2 intterm_novar0[OF linr,where x="x" and y="x + c*d"])
}
moreover
{
assume n0: "n=0"
from prems have lin2: "islinintterm (Add (Mult (Cst i') (Var n')) r)" by simp
from prems have "n < n'" by simp then have npos': "0 < n'" by simp
with prems have ?case
proof(simp add: intterm_novar0[OF lin2, where x="x" and y="x+c*d"]
nth_pos2 dvd_period,case_tac "i=1",
simp add: dvd_period[where a="a" and d="d" and x="x" and c="c"], simp)
case goal1
from prems have "abs i = 1 \<and> i\<noteq>1" by auto
then have mi: "i = -1" by arith
have "(a dvd -x + (i' * ats ! (n' - Suc 0) + I_intterm ((x + c * d) # ats) r)) =
(a dvd x + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r))"
by (simp add:
uminus_dvd_conv'[where d="a" and
t="-x + (i' * ats ! (n' - Suc 0) + I_intterm ((x + c * d) # ats) r)"])
also
have "(a dvd x + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r)) =
(a dvd x +c*d + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r))"
by (rule dvd_period[where a="a" and d="d" and x="x" and c="c"], assumption)
also
have "(a dvd x +c*d +
(-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r)) =
(a dvd -(x +c*d +
(-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r)))"
by (rule uminus_dvd_conv'[where d="a" and
t="x +c*d + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r)"])
also
have "(a dvd -(x +c*d +
(-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r)))
= (a dvd
- x - c * d + (i' * ats ! (n' - Suc 0) + I_intterm ((x + c * d) # ats) r))"
by (auto,simp_all add: zadd_ac)
finally show ?case using mi by auto
qed
}
ultimately show ?case by blast
qed
next
case (goal4 a t)
show ?case using prems
proof(induct t rule: islinintterm.induct, simp_all,case_tac "n=0",
simp_all add: nth_pos2)
case (goal1 i n i')
show ?case
using prems
proof(case_tac "i=1", simp,
simp add: dvd_period[where a="a" and d="d" and x="x" and c="c"])
case goal1
from prems have "abs i = 1 \<and> i\<noteq>1" by auto
then have im1: "i=-1" by arith
then have "(a dvd i*x + i') = (a dvd x + (-i'))"
by (simp add: uminus_dvd_conv'[where d="a" and t="-x +i'"])
moreover
from im1 have "(a dvd i*x + (i*(c * d)) + i') = (a dvd (x + c*d - i'))"
apply simp
apply (simp add: uminus_dvd_conv'[where d="a" and t="-x - c * d + i'"])
by (simp add: zadd_ac)
ultimately
have eq1:"((a dvd i*x + i') = (a dvd i*x + (i*(c * d)) + i')) =
((a dvd x + (-i')) = (a dvd (x + c*d - i')))" by simp
moreover
have dvd2: "(a dvd x + (-i')) = (a dvd x + c * d + (-i'))"
by (rule dvd_period[where a="a" and d="d" and x="x" and c="c"], assumption)
ultimately show ?thesis by simp
qed
next
case (goal2 i n i' n' r)
have "n = 0 \<or> 0 < n" by arith
moreover
{
assume npos: "0 < n"
from prems have "n < n'" by simp then have "0 < n'" by simp
moreover from prems
have linr: "islinintterm (Add (Mult (Cst i') (Var n')) r)" by simp
ultimately have ?case
using prems npos
by (simp add: nth_pos2 intterm_novar0[OF linr,where x="x" and y="x + c*d"])
}
moreover
{
assume n0: "n=0"
from prems have lin2: "islinintterm (Add (Mult (Cst i') (Var n')) r)" by simp
from prems have "n < n'" by simp then have npos': "0 < n'" by simp
with prems have ?case
proof(simp add: intterm_novar0[OF lin2, where x="x" and y="x+c*d"]
nth_pos2 dvd_period,case_tac "i=1",
simp add: dvd_period[where a="a" and d="d" and x="x" and c="c"], simp)
case goal1
from prems have "abs i = 1 \<and> i\<noteq>1" by auto
then have mi: "i = -1" by arith
have "(a dvd -x + (i' * ats ! (n' - Suc 0) + I_intterm ((x + c * d) # ats) r)) =
(a dvd x + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r))"
by (simp add:
uminus_dvd_conv'[where d="a" and
t="-x + (i' * ats ! (n' - Suc 0) + I_intterm ((x + c * d) # ats) r)"])
also
have "(a dvd x + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r)) =
(a dvd x +c*d + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r))"
by (rule dvd_period[where a="a" and d="d" and x="x" and c="c"], assumption)
also
have "(a dvd x +c*d +
(-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r)) =
(a dvd -(x +c*d +
(-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r)))"
by (rule uminus_dvd_conv'[where d="a" and
t="x +c*d + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r)"])
also
have "(a dvd -(x +c*d +
(-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r)))
= (a dvd
- x - c * d + (i' * ats ! (n' - Suc 0) + I_intterm ((x + c * d) # ats) r))"
by (auto,simp_all add: zadd_ac)
finally show ?case using mi by auto
qed
}
ultimately show ?case by blast
qed
next
case (goal5 t a)
show ?case
using prems
apply (cases t, simp_all add: nth_pos2)
apply (case_tac "intterm1", simp_all)
apply (case_tac "intterm1a",simp_all)
by (case_tac "intterm2a",simp_all)
(case_tac "nat",simp_all add: nth_pos2 intterm_novar0[where x="x" and y="x+c*d"])
qed
lemma minusinf_repeats2:
assumes alldvd: "alldivide (d,p)"
and unity: "isunified p"
shows "\<forall> x k. (qinterp (x#ats) (minusinf p) = qinterp ((x - k*d)#ats) (minusinf p))"
(is "\<forall> x k. ?P x = ?P (x - k*d)")
proof(rule allI, rule allI)
fix x k
show "?P x = ?P (x - k*d)"
proof-
have "?P x = ?P (x + (-k)*d)" by (rule minusinf_repeats[OF alldvd unity])
then have "?P x = ?P (x - (k*d))" by simp
then show ?thesis by blast
qed
qed
(* existence for minusinf p is existence for p *)
lemma minusinf_lemma:
assumes unifp: "isunified p"
and exminf: "\<exists> j \<in> {1 ..d}. qinterp (j#ats) (minusinf p)" (is "\<exists> j \<in> {1 .. d}. ?P1 j")
shows "\<exists> x. qinterp (x#ats) p" (is "\<exists> x. ?P x")
proof-
from exminf obtain "j" where P1j: "?P1 j" by blast
have ePeqP1: "\<exists>z. \<forall> x. x < z \<longrightarrow> (?P x = ?P1 x)"
by (rule minusinf_eq[OF unifp])
then obtain "z" where P1eqP : "\<forall> x. x < z \<longrightarrow> (?P x = ?P1 x)" by blast
let ?d = "divlcm p"
have alldvd: "alldivide (?d,p)" using unified_islinform[OF unifp] divlcm_corr
by auto
have dpos: "0 < ?d" using unified_islinform[OF unifp] divlcm_pos
by simp
have P1eqP1 : "\<forall> x k. ?P1 x = ?P1 (x - k*(?d))"
by (rule minusinf_repeats2[OF alldvd unifp])
let ?w = "j - (abs (j-z) +1)* ?d"
show "\<exists> x. ?P x"
proof
have w: "?w < z"
by (rule decr_lemma[OF dpos])
have "?P1 j = ?P1 ?w" using P1eqP1 by blast
also have "\<dots> = ?P ?w" using w P1eqP by blast
finally show "?P ?w" using P1j by blast
qed
qed
(* limited search for the withness for minusinf p, due to peridicity *)
lemma minusinf_disj:
assumes unifp: "isunified p"
shows "(\<exists> x. qinterp (x#ats) (minusinf p)) =
(\<exists> j \<in> { 1.. divlcm p}. qinterp (j#ats) (minusinf p))"
(is "(\<exists> x. ?P x) = (\<exists> j \<in> { 1.. ?d}. ?P j)")
proof
have linp: "islinform p" by (rule unified_islinform[OF unifp])
have dpos: "0 < ?d" by (rule divlcm_pos[OF linp])
have alldvd: "alldivide(?d,p)" by (rule divlcm_corr[OF linp])
{
assume "\<exists> j\<in> {1 .. ?d}. ?P j"
then show "\<exists> x. ?P x" using dpos by auto
next
assume "\<exists> x. ?P x"
then obtain "x" where P: "?P x" by blast
have modd: "\<forall>x k. ?P x = ?P (x - k*?d)"
by (rule minusinf_repeats2[OF alldvd unifp])
have "x mod ?d = x - (x div ?d)*?d"
by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq)
hence Pmod: "?P x = ?P (x mod ?d)" using modd by simp
show "\<exists> j\<in> {1 .. ?d}. ?P j"
proof (cases)
assume "x mod ?d = 0"
hence "?P 0" using P Pmod by simp
moreover have "?P 0 = ?P (0 - (-1)*?d)" using modd by blast
ultimately have "?P ?d" by simp
moreover have "?d \<in> {1 .. ?d}" using dpos
by (simp add:atLeastAtMost_iff)
ultimately show "\<exists> j\<in> {1 .. ?d}. ?P j" ..
next
assume not0: "x mod ?d \<noteq> 0"
have "?P(x mod ?d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound)
moreover have "x mod ?d : {1 .. ?d}"
proof -
have "0 \<le> x mod ?d" by(rule pos_mod_sign[OF dpos])
moreover have "x mod ?d < ?d" by(rule pos_mod_bound[OF dpos])
ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff)
qed
ultimately show "\<exists> j\<in> {1 .. ?d}. ?P j" ..
qed
}
qed
lemma minusinf_qfree:
assumes linp : "islinform p"
shows "isqfree (minusinf p)"
using linp
by (induct p rule: minusinf.induct) auto
(* Properties of bset and a set *)
(* The elements of a bset are linear *)
lemma bset_lin:
assumes unifp: "isunified p"
shows "\<forall> b \<in> set (bset p). islinintterm b"
using unifp unified_islinform[OF unifp]
proof (induct p rule: bset.induct, auto)
case (goal1 c r z)
from prems have "z = Cst 0" by (cases z, simp_all)
then have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" using prems by simp
have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
have "islinintterm (Cst -1)" by simp
then show ?case using linr lin_add_lin by simp
next
case (goal2 c r z)
from prems have "z = Cst 0" by (cases z, simp_all)
then have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" using prems by simp
have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
show ?case by (rule linr)
next
case (goal3 c r z)
from prems have "z = Cst 0" by (cases z, simp_all)
then have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" using prems by simp
have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
have "islinintterm (Cst -1)" by simp
then show ?case using linr lin_add_lin lin_neg_lin by simp
next
case (goal4 c r z)
from prems have "z = Cst 0" by (cases z, simp_all)
then have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" using prems by simp
have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
have "islinintterm (Cst -1)" by simp
then show ?case using linr lin_add_lin lin_neg_lin by simp
next
case (goal5 c r z)
from prems have "z = Cst 0" by (cases z, simp_all)
then have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" using prems by simp
have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
have "islinintterm (Cst -1)" by simp
then show ?case using linr lin_add_lin lin_neg_lin by simp
next
case (goal6 c r z)
from prems have "z = Cst 0" by (cases z, simp_all)
then have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" using prems by simp
have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
have "islinintterm (Cst -1)" by simp
then show ?case using linr lin_add_lin lin_neg_lin by simp
next
case (goal7 c r z)
from prems have "z = Cst 0" by (cases z, simp_all)
then have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" using prems by simp
have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
have "islinintterm (Cst -1)" by simp
then show ?case using linr lin_add_lin lin_neg_lin by simp
qed
(* The third lemma in Norrisch's Paper *)
lemma bset_disj_repeat:
assumes unifp: "isunified p"
and alldvd: "alldivide (d,p)"
and dpos: "0 < d"
and nob: "(qinterp (x#ats) q) \<and> \<not>(\<exists>j\<in> {1 .. d}. \<exists> b \<in> set (bset p). (qinterp (((I_intterm (a#ats) b) + j)#ats) q)) \<and>(qinterp (x#ats) p)"
(is "?Q x \<and> \<not>(\<exists> j\<in> {1.. d}. \<exists> b\<in> ?B. ?Q (?I a b + j)) \<and> ?P x")
shows "?P (x -d)"
using unifp nob alldvd unified_islinform[OF unifp]
proof (induct p rule: islinform.induct,auto)
case (goal1 t)
from prems
have lint: "islinintterm t" by simp
then have "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
by (induct t rule: islinintterm.induct) auto
moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
moreover
{ assume "\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r"
then obtain "i" "n" "r" where
inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
by blast
with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
by simp
have linr: "islinintterm r"
by (rule islinintterm_subt[OF lininr])
have "n=0 \<or> n>0" by arith
moreover {assume "n>0" then have ?case
using prems
by (simp add: nth_pos2
intterm_novar0[OF lininr, where x="x" and y="x-d"]) }
moreover
{assume nz: "n = 0"
from prems have "abs i = 1" by auto
then have "i = -1 \<or> i =1" by arith
moreover
{
assume i1: "i=1"
have ?case using dpos prems
by (auto simp add: intterm_novar0[OF lininr, where x="x" and y="x - d"])
}
moreover
{
assume im1: "i = -1"
have ?case
using prems
proof(auto simp add: intterm_novar0[OF lininr, where x="x - d" and y="x"], cases)
assume "- x + d + ?I x r \<le> 0"
then show "- x + d + ?I x r \<le> 0" .
next
assume np: "\<not> - x + d + ?I x r \<le> 0"
then have ltd:"x - ?I x r \<le> d - 1" by simp
from prems have "-x + ?I x r \<le> 0" by simp
then have ge0: "x - ?I x r \<ge> 0"
by simp
from ltd ge0 have "x - ?I x r = 0 \<or> (1 \<le> x - ?I x r \<and> x - ?I x r \<le> d - 1) " by arith
moreover
{
assume "x - ?I x r = 0"
then have xeqr: "x = ?I x r" by simp
from prems have "?Q x" by simp
with xeqr have qr:"?Q (?I x r)" by simp
from prems have lininr: "islinintterm (Add (Mult (Cst i) (Var 0)) r)" by simp
have "islinintterm r" by (rule islinintterm_subt[OF lininr])
from prems
have "\<forall>j\<in>{1..d}. \<not> ?Q (?I a r + -1 + j)"
using linr by (auto simp add: lin_add_corr)
moreover from dpos have "1 \<in> {1..d}" by simp
ultimately have " \<not> ?Q (?I a r + -1 + 1)" by blast
with dpos linr have "\<not> ?Q (?I x r)"
by (simp add: intterm_novar0[OF lininr, where x="x" and y="a"] lin_add_corr)
with qr have "- x + d + ?I x r \<le> 0" by simp
}
moreover
{
assume gt0: "1 \<le> x - ?I x r \<and> x - ?I x r \<le> d - 1"
then have "\<exists> j\<in> {1 .. d - 1}. x - ?I x r = j" by simp
then have "\<exists> j\<in> {1 .. d}. x - ?I x r = j" by auto
then obtain "j" where con: "1\<le>j \<and> j \<le> d \<and> x - ?I x r = j" by auto
then have xeqr: "x = ?I x r + j" by auto
with prems have "?Q (?I x r + j)" by simp
with con have qrpj: "\<exists> j\<in> {1 .. d}. ?Q (?I x r + j)" by auto
from prems have "\<forall>j\<in>{1..d}. \<not> ?Q (?I a r + j)" by auto
then have "\<not> (\<exists> j\<in>{1..d}. ?Q (?I x r + j))"
by (simp add: intterm_novar0[OF lininr, where x="x" and y="a"])
with qrpj prems have "- x + d + ?I x r \<le> 0" by simp
}
ultimately show "- x + d + ?I x r \<le> 0" by blast
qed
}
ultimately have ?case by blast
}
ultimately have ?case by blast
}
ultimately show ?case by blast
next
case (goal3 a t)
from prems
have lint: "islinintterm t" by simp
then have "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
by (induct t rule: islinintterm.induct) auto
moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
moreover
{ assume "\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r"
then obtain "i" "n" "r" where
inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
by blast
with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
by simp
have linr: "islinintterm r"
by (rule islinintterm_subt[OF lininr])
have "n=0 \<or> n>0" by arith
moreover {assume "n>0" then have ?case using prems
by (simp add: nth_pos2
intterm_novar0[OF lininr, where x="x" and y="x-d"]) }
moreover {
assume nz: "n=0"
from prems have "abs i = 1" by auto
then have ipm: "i=1 \<or> i = -1" by arith
from nz prems have advdixr: "a dvd (i * x) + I_intterm (x # ats) r"
by simp
from prems have "a dvd d" by simp
then have advdid: "a dvd i*d" using ipm by auto
have ?case
using prems ipm
by (auto simp add: intterm_novar0[OF lininr, where x="x-d" and y="x"] dvd_period[OF advdid, where x="i*x" and c="-1"])
}
ultimately have ?case by blast
} ultimately show ?case by blast
next
case (goal4 a t)
from prems
have lint: "islinintterm t" by simp
then have "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
by (induct t rule: islinintterm.induct) auto
moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
moreover
{ assume "\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r"
then obtain "i" "n" "r" where
inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
by blast
with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
by simp
have linr: "islinintterm r"
by (rule islinintterm_subt[OF lininr])
have "n=0 \<or> n>0" by arith
moreover {assume "n>0" then have ?case using prems
by (simp add: nth_pos2
intterm_novar0[OF lininr, where x="x" and y="x-d"]) }
moreover {
assume nz: "n=0"
from prems have "abs i = 1" by auto
then have ipm: "i =1 \<or> i = -1" by arith
from nz prems have advdixr: "\<not> (a dvd (i * x) + I_intterm (x # ats) r)"
by simp
from prems have "a dvd d" by simp
then have advdid: "a dvd i*d" using ipm by auto
have ?case
using prems ipm
by (auto simp add: intterm_novar0[OF lininr, where x="x-d" and y="x"] dvd_period[OF advdid, where x="i*x" and c="-1"])
}
ultimately have ?case by blast
} ultimately show ?case by blast
next
case (goal2 t)
from prems
have lint: "islinintterm t" by simp
then have "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
by (induct t rule: islinintterm.induct) auto
moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
moreover
{ assume "\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r"
then obtain "i" "n" "r" where
inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
by blast
with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
by simp
have linr: "islinintterm r"
by (rule islinintterm_subt[OF lininr])
have "n=0 \<or> n>0" by arith
moreover {assume "n>0" then have ?case
using prems
by (simp add: nth_pos2
intterm_novar0[OF lininr, where x="x" and y="x-d"]) }
moreover
{assume nz: "n = 0"
from prems have "abs i = 1" by auto
then have "i = -1 \<or> i =1" by arith
moreover
{
assume i1: "i=1"
with prems have px: "x + ?I x r = 0" by simp
then have "x = (- ?I x r - 1) + 1" by simp
hence q1: "?Q ((- ?I x r - 1) + 1)" by simp
from prems have "\<not> (?Q ((?I a (lin_add(lin_neg r, Cst -1))) + 1))"
by auto
hence "\<not> (?Q ((- ?I a r - 1) + 1))"
using lin_add_corr lin_neg_corr linr lin_neg_lin
by simp
hence "\<not> (?Q ((- ?I x r - 1) + 1))"
using intterm_novar0[OF lininr, where x="x" and y="a"]
by simp
with q1 have ?case by simp
}
moreover
{
assume im1: "i = -1"
with prems have px: "-x + ?I x r = 0" by simp
then have "x = ?I x r" by simp
hence q1: "?Q (?I x r)" by simp
from prems have "\<not> (?Q ((?I a (lin_add(r, Cst -1))) + 1))"
by auto
hence "\<not> (?Q (?I a r))"
using lin_add_corr lin_neg_corr linr lin_neg_lin
by simp
hence "\<not> (?Q (?I x r ))"
using intterm_novar0[OF lininr, where x="x" and y="a"]
by simp
with q1 have ?case by simp
}
ultimately have ?case by blast
}
ultimately have ?case by blast
}
ultimately show ?case by blast
next
case (goal5 t)
from prems
have lint: "islinintterm t" by simp
then have "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
by (induct t rule: islinintterm.induct) auto
moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
moreover
{ assume "\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r"
then obtain "i" "n" "r" where
inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
by blast
with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
by simp
have linr: "islinintterm r"
by (rule islinintterm_subt[OF lininr])
have "n=0 \<or> n>0" by arith
moreover {assume "n>0" then have ?case
using prems
by (simp add: nth_pos2
intterm_novar0[OF lininr, where x="x" and y="x-d"]) }
moreover
{assume nz: "n = 0"
from prems have "abs i = 1" by auto
then have "i = -1 \<or> i =1" by arith
moreover
{
assume i1: "i=1"
with prems have px: "x -d + ?I (x-d) r = 0" by simp
hence "x = (- ?I x r) + d"
using intterm_novar0[OF lininr, where x="x" and y="x-d"]
by simp
hence q1: "?Q (- ?I x r + d)" by simp
from prems have "\<not> (?Q ((?I a (lin_neg r)) + d))"
by auto
hence "\<not> (?Q (- ?I a r + d))"
using lin_neg_corr linr by simp
hence "\<not> (?Q ((- ?I x r + d)))"
using intterm_novar0[OF lininr, where x="x" and y="a"]
by simp
with q1 have ?case by simp
}
moreover
{
assume im1: "i = -1"
with prems have px: "- (x -d) + ?I (x - d) r = 0" by simp
then have "x = ?I x r + d "
using intterm_novar0[OF lininr, where x="x" and y="x-d"]
by simp
hence q1: "?Q (?I x r + d)" by simp
from prems have "\<not> (?Q ((?I a r) + d))"
by auto
hence "\<not> (?Q (?I x r + d))"
using intterm_novar0[OF lininr, where x="x" and y="a"]
by simp
with q1 have ?case by simp
}
ultimately have ?case by blast
}
ultimately have ?case by blast
}
ultimately show ?case by blast
qed
lemma bset_disj_repeat2:
assumes unifp: "isunified p"
shows "\<forall> x. \<not>(\<exists>j\<in> {1 .. (divlcm p)}. \<exists> b \<in> set (bset p).
(qinterp (((I_intterm (a#ats) b) + j)#ats) p))
\<longrightarrow> (qinterp (x#ats) p) \<longrightarrow> (qinterp ((x - (divlcm p))#ats) p)"
(is "\<forall> x. \<not>(\<exists> j\<in> {1 .. ?d}. \<exists> b\<in> ?B. ?P (?I a b + j)) \<longrightarrow> ?P x \<longrightarrow> ?P (x - ?d)")
proof
fix x
have linp: "islinform p" by (rule unified_islinform[OF unifp])
have dpos: "?d > 0" by (rule divlcm_pos[OF linp])
have alldvd: "alldivide(?d,p)" by (rule divlcm_corr[OF linp])
show "\<not>(\<exists> j\<in> {1 .. ?d}. \<exists> b\<in> ?B. ?P (?I a b + j)) \<longrightarrow> ?P x \<longrightarrow> ?P (x - ?d)"
using prems bset_disj_repeat[OF unifp alldvd dpos]
by blast
qed
(* Cooper's theorem in the minusinfinity version *)
lemma cooper_mi_eq:
assumes unifp : "isunified p"
shows "(\<exists> x. qinterp (x#ats) p) =
((\<exists> j \<in> {1 .. (divlcm p)}. qinterp (j#ats) (minusinf p)) \<or>
(\<exists> j \<in> {1 .. (divlcm p)}. \<exists> b \<in> set (bset p).
qinterp (((I_intterm (a#ats) b) + j)#ats) p))"
(is "(\<exists> x. ?P x) = ((\<exists> j\<in> {1 .. ?d}. ?MP j) \<or> (\<exists> j \<in> ?D. \<exists> b\<in> ?B. ?P (?I a b + j)))")
proof-
have linp :"islinform p" by (rule unified_islinform[OF unifp])
have dpos: "?d > 0" by (rule divlcm_pos[OF linp])
have alldvd: "alldivide(?d,p)" by (rule divlcm_corr[OF linp])
have eMPimpeP: "(\<exists>j \<in> ?D. ?MP j) \<longrightarrow> (\<exists>x. ?P x)"
by (simp add: minusinf_lemma[OF unifp, where d="?d" and ats="ats"])
have ePimpeP: "(\<exists> j \<in> ?D. \<exists> b\<in> ?B. ?P (?I a b + j)) \<longrightarrow> (\<exists> x. ?P x)"
by blast
have bst_rep: "\<forall> x. \<not> (\<exists> j \<in> ?D. \<exists> b \<in> ?B. ?P (?I a b + j)) \<longrightarrow> ?P x \<longrightarrow> ?P (x - ?d)"
by (rule bset_disj_repeat2[OF unifp])
have MPrep: "\<forall> x k. ?MP x = ?MP (x- k*?d)"
by (rule minusinf_repeats2[OF alldvd unifp])
have MPeqP: "\<exists> z. \<forall> x < z. ?P x = ?MP x"
by (rule minusinf_eq[OF unifp])
let ?B'= "{?I a b| b. b\<in> ?B}"
from bst_rep have bst_rep2: "\<forall>x. \<not> (\<exists>j\<in>?D. \<exists>b\<in> ?B'. ?P (b+j)) \<longrightarrow> ?P x \<longrightarrow> ?P (x - ?d)"
by auto
show ?thesis
using cpmi_eq[OF dpos MPeqP bst_rep2 MPrep]
by auto
qed
(* A formalized analogy between aset, bset, plusinfinity and minusinfinity *)
consts mirror:: "QF \<Rightarrow> QF"
recdef mirror "measure size"
"mirror (Le (Add (Mult (Cst c) (Var 0)) r) z) =
(Le (Add (Mult (Cst (- c)) (Var 0)) r) z)"
"mirror (Eq (Add (Mult (Cst c) (Var 0)) r) z) =
(Eq (Add (Mult (Cst (- c)) (Var 0)) r) z)"
"mirror (Divides (Cst d) (Add (Mult (Cst c) (Var 0)) r)) =
(Divides (Cst d) (Add (Mult (Cst (- c)) (Var 0)) r))"
"mirror (NOT(Divides (Cst d) (Add (Mult (Cst c) (Var 0)) r))) =
(NOT(Divides (Cst d) (Add (Mult (Cst (- c)) (Var 0)) r)))"
"mirror (NOT(Eq (Add (Mult (Cst c) (Var 0)) r) z)) =
(NOT(Eq (Add (Mult (Cst (- c)) (Var 0)) r) z))"
"mirror (And p q) = And (mirror p) (mirror q)"
"mirror (Or p q) = Or (mirror p) (mirror q)"
"mirror p = p"
(* mirror preserves unifiedness *)
lemma[simp]: "(abs (i::int) = 1) = (i =1 \<or> i = -1)" by arith
lemma mirror_unified:
assumes unif: "isunified p"
shows "isunified (mirror p)"
using unif
proof (induct p rule: mirror.induct, simp_all)
case (goal1 c r z)
from prems have zz: "z = Cst 0" by (cases z, simp_all)
then show ?case using prems
by (auto simp add: islinintterm_eq_islint islint_def)
next
case (goal2 c r z)
from prems have zz: "z = Cst 0" by (cases z, simp_all)
then show ?case using prems
by (auto simp add: islinintterm_eq_islint islint_def)
next
case (goal3 d c r) show ?case using prems by (auto simp add: islinintterm_eq_islint islint_def)
next
case (goal4 d c r) show ?case using prems by (auto simp add: islinintterm_eq_islint islint_def)
next
case (goal5 c r z)
from prems have zz: "z = Cst 0" by (cases z, simp_all)
then show ?case using prems
by (auto simp add: islinintterm_eq_islint islint_def)
qed
(* relationship between plusinf and minusinf *)
lemma plusinf_eq_minusinf_mirror:
assumes unifp: "isunified p"
shows "(qinterp (x#ats) (plusinf p)) = (qinterp ((- x)#ats) (minusinf (mirror p)))"
using unifp unified_islinform[OF unifp]
proof (induct p rule: islinform.induct, simp_all)
case (goal1 t z)
from prems
have lint: "islinintterm t" by simp
then have "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
by (induct t rule: islinintterm.induct) auto
moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
moreover
{ assume "\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r"
then obtain "i" "n" "r" where
inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
by blast
with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
by simp
have linr: "islinintterm r"
by (rule islinintterm_subt[OF lininr])
have ?case using prems
by (cases n, auto simp add: nth_pos2
intterm_novar0[OF lininr, where x="x" and y="-x"] )}
ultimately show ?case by blast
next
case (goal2 t z)
from prems
have lint: "islinintterm t" by simp
then have "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
by (induct t rule: islinintterm.induct) auto
moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
moreover
{ assume "\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r"
then obtain "i" "n" "r" where
inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
by blast
with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
by simp
have linr: "islinintterm r"
by (rule islinintterm_subt[OF lininr])
have ?case using prems
by (cases n, auto simp add: nth_pos2
intterm_novar0[OF lininr, where x="x" and y="-x"] )}
ultimately show ?case by blast
next
case (goal3 d t)
from prems
have lint: "islinintterm t" by simp
then have "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
by (induct t rule: islinintterm.induct) auto
moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
moreover
{ assume "\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r"
then obtain "i" "n" "r" where
inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
by blast
with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
by simp
have linr: "islinintterm r"
by (rule islinintterm_subt[OF lininr])
have ?case using prems
by (cases n, simp_all add: nth_pos2
intterm_novar0[OF lininr, where x="x" and y="-x"] )}
ultimately show ?case by blast
next
case (goal4 d t)
from prems
have lint: "islinintterm t" by simp
then have "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
by (induct t rule: islinintterm.induct) auto
moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
moreover
{ assume "\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r"
then obtain "i" "n" "r" where
inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
by blast
with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
by simp
have linr: "islinintterm r"
by (rule islinintterm_subt[OF lininr])
have ?case using prems
by (cases n, simp_all add: nth_pos2
intterm_novar0[OF lininr, where x="x" and y="-x"] )}
ultimately show ?case by blast
next
case (goal5 t z)
from prems
have lint: "islinintterm t" by simp
then have "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
by (induct t rule: islinintterm.induct) auto
moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
moreover
{ assume "\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r"
then obtain "i" "n" "r" where
inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
by blast
with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
by simp
have linr: "islinintterm r"
by (rule islinintterm_subt[OF lininr])
have ?case using prems
by (cases n, auto simp add: nth_pos2
intterm_novar0[OF lininr, where x="x" and y="-x"] )}
ultimately show ?case by blast
qed
(* relationship between aset abd bset *)
lemma aset_eq_bset_mirror:
assumes unifp: "isunified p"
shows "set (aset p) = set (map lin_neg (bset (mirror p)))"
using unifp
proof(induct p rule: mirror.induct)
case (1 c r z)
from prems have zz: "z = Cst 0"
by (cases z, auto)
from prems zz have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" by simp
have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
have neg1eqm1: "Cst 1 = lin_neg (Cst -1)" by (simp add: lin_neg_def)
have negm1eq1: "Cst -1 = lin_neg (Cst 1)" by (simp add: lin_neg_def)
show ?case using prems linr zz apply (auto simp add: lin_neg_lin_add_distrib lin_neg_idemp neg1eqm1)
by (simp add: negm1eq1 lin_neg_idemp sym[OF lin_neg_lin_add_distrib] lin_add_lin)
next
case (2 c r z) from prems have zz: "z = Cst 0"
by (cases z, auto)
from prems zz have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" by simp
have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
have neg1eqm1: "Cst 1 = lin_neg (Cst -1)" by (simp add: lin_neg_def)
have negm1eq1: "Cst -1 = lin_neg (Cst 1)" by (simp add: lin_neg_def)
show ?case using prems linr zz
by (auto simp add: lin_neg_lin_add_distrib lin_neg_idemp neg1eqm1)
(simp add: negm1eq1 lin_neg_idemp sym[OF lin_neg_lin_add_distrib] lin_add_lin lin_neg_lin)
next
case (5 c r z) from prems have zz: "z = Cst 0"
by (cases z, auto)
from prems zz have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" by simp
have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
have neg1eqm1: "Cst 1 = lin_neg (Cst -1)" by (simp add: lin_neg_def)
have negm1eq1: "Cst -1 = lin_neg (Cst 1)" by (simp add: lin_neg_def)
show ?case using prems linr zz
by(auto simp add: lin_neg_lin_add_distrib lin_neg_idemp neg1eqm1)
qed simp_all
(* relationship between aset abd bset 2*)
lemma aset_eq_bset_mirror2:
assumes unifp: "isunified p"
shows "aset p = map lin_neg (bset (mirror p))"
using unifp
proof(induct p rule: mirror.induct)
case (1 c r z)
from prems have zz: "z = Cst 0"
by (cases z, auto)
from prems zz have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" by simp
have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
have neg1eqm1: "Cst 1 = lin_neg (Cst -1)" by (simp add: lin_neg_def)
have negm1eq1: "Cst -1 = lin_neg (Cst 1)" by (simp add: lin_neg_def)
show ?case using prems linr zz
apply (simp add: lin_neg_lin_add_distrib lin_neg_idemp neg1eqm1)
apply (simp add: negm1eq1 lin_neg_idemp sym[OF lin_neg_lin_add_distrib] lin_add_lin)
by arith
next
case (2 c r z) from prems have zz: "z = Cst 0"
by (cases z, auto)
from prems zz have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" by simp
have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
have neg1eqm1: "Cst 1 = lin_neg (Cst -1)" by (simp add: lin_neg_def)
have negm1eq1: "Cst -1 = lin_neg (Cst 1)" by (simp add: lin_neg_def)
show ?case using prems linr zz
by(auto simp add: lin_neg_lin_add_distrib lin_neg_idemp neg1eqm1)
(simp add: negm1eq1 lin_neg_idemp sym[OF lin_neg_lin_add_distrib] lin_add_lin lin_neg_lin)
next
case (5 c r z) from prems have zz: "z = Cst 0"
by (cases z, auto)
from prems zz have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" by simp
have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
have neg1eqm1: "Cst 1 = lin_neg (Cst -1)" by (simp add: lin_neg_def)
have negm1eq1: "Cst -1 = lin_neg (Cst 1)" by (simp add: lin_neg_def)
show ?case using prems linr zz
by(auto simp add: lin_neg_lin_add_distrib lin_neg_idemp neg1eqm1)
qed simp_all
(* mirror preserves divlcm *)
lemma divlcm_mirror_eq:
assumes unifp: "isunified p"
shows "divlcm p = divlcm (mirror p)"
using unifp
by (induct p rule: mirror.induct) auto
(* mirror almost preserves semantics *)
lemma mirror_interp:
assumes unifp: "isunified p"
shows "(qinterp (x#ats) p) = (qinterp ((- x)#ats) (mirror p))" (is "?P x = ?MP (-x)")
using unifp unified_islinform[OF unifp]
proof (induct p rule: islinform.induct)
case (1 t z)
from prems have zz: "z = 0" by simp
from prems
have lint: "islinintterm t" by simp
then have "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
by (induct t rule: islinintterm.induct) auto
moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
moreover
{ assume "\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r"
then obtain "i" "n" "r" where
inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
by blast
with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
by simp
have linr: "islinintterm r"
by (rule islinintterm_subt[OF lininr])
have ?case using prems zz
by (cases n) (simp_all add: nth_pos2
intterm_novar0[OF lininr, where x="x" and y="-x"])
}
ultimately show ?case by blast
next
case (2 t z)
from prems have zz: "z = 0" by simp
from prems
have lint: "islinintterm t" by simp
then have "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
by (induct t rule: islinintterm.induct) auto
moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
moreover
{ assume "\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r"
then obtain "i" "n" "r" where
inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
by blast
with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
by simp
have linr: "islinintterm r"
by (rule islinintterm_subt[OF lininr])
have ?case using prems zz
by (cases n) (simp_all add: nth_pos2
intterm_novar0[OF lininr, where x="x" and y="-x"])
}
ultimately show ?case by blast
next
case (3 d t)
from prems
have lint: "islinintterm t" by simp
then have "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
by (induct t rule: islinintterm.induct) auto
moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
moreover
{ assume "\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r"
then obtain "i" "n" "r" where
inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
by blast
with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
by simp
have linr: "islinintterm r"
by (rule islinintterm_subt[OF lininr])
have ?case
using prems linr
by (cases n) (simp_all add: nth_pos2
intterm_novar0[OF lininr, where x="x" and y="-x"])
}
ultimately show ?case by blast
next
case (6 d t)
from prems
have lint: "islinintterm t" by simp
then have "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
by (induct t rule: islinintterm.induct) auto
moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
moreover
{ assume "\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r"
then obtain "i" "n" "r" where
inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
by blast
with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
by simp
have linr: "islinintterm r"
by (rule islinintterm_subt[OF lininr])
have ?case
using prems linr
by (cases n) (simp_all add: nth_pos2
intterm_novar0[OF lininr, where x="x" and y="-x"])
}
ultimately show ?case by blast
next
case (7 t z)
from prems have zz: "z = 0" by simp
from prems
have lint: "islinintterm t" by simp
then have "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
by (induct t rule: islinintterm.induct) auto
moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
moreover
{ assume "\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r"
then obtain "i" "n" "r" where
inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
by blast
with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
by simp
have linr: "islinintterm r"
by (rule islinintterm_subt[OF lininr])
have ?case using prems zz
by (cases n) (simp_all add: nth_pos2
intterm_novar0[OF lininr, where x="x" and y="-x"])
}
ultimately show ?case by blast
qed simp_all
lemma mirror_interp2:
assumes unifp: "islinform p"
shows "(qinterp (x#ats) p) = (qinterp ((- x)#ats) (mirror p))" (is "?P x = ?MP (-x)")
using unifp
proof (induct p rule: islinform.induct)
case (1 t z)
from prems have zz: "z = 0" by simp
from prems
have lint: "islinintterm t" by simp
then have "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
by (induct t rule: islinintterm.induct) auto
moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
moreover
{ assume "\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r"
then obtain "i" "n" "r" where
inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
by blast
with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
by simp
have linr: "islinintterm r"
by (rule islinintterm_subt[OF lininr])
have ?case using prems zz
by (cases n) (simp_all add: nth_pos2
intterm_novar0[OF lininr, where x="x" and y="-x"])
}
ultimately show ?case by blast
next
case (2 t z)
from prems have zz: "z = 0" by simp
from prems
have lint: "islinintterm t" by simp
then have "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
by (induct t rule: islinintterm.induct) auto
moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
moreover
{ assume "\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r"
then obtain "i" "n" "r" where
inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
by blast
with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
by simp
have linr: "islinintterm r"
by (rule islinintterm_subt[OF lininr])
have ?case using prems zz
by (cases n) (simp_all add: nth_pos2
intterm_novar0[OF lininr, where x="x" and y="-x"])
}
ultimately show ?case by blast
next
case (3 d t)
from prems
have lint: "islinintterm t" by simp
then have "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
by (induct t rule: islinintterm.induct) auto
moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
moreover
{ assume "\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r"
then obtain "i" "n" "r" where
inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
by blast
with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
by simp
have linr: "islinintterm r"
by (rule islinintterm_subt[OF lininr])
have ?case
using prems linr
by (cases n) (simp_all add: nth_pos2
intterm_novar0[OF lininr, where x="x" and y="-x"])
}
ultimately show ?case by blast
next
case (6 d t)
from prems
have lint: "islinintterm t" by simp
then have "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
by (induct t rule: islinintterm.induct) auto
moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
moreover
{ assume "\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r"
then obtain "i" "n" "r" where
inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
by blast
with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
by simp
have linr: "islinintterm r"
by (rule islinintterm_subt[OF lininr])
have ?case
using prems linr
by (cases n) (simp_all add: nth_pos2
intterm_novar0[OF lininr, where x="x" and y="-x"])
}
ultimately show ?case by blast
next
case (7 t z)
from prems have zz: "z = 0" by simp
from prems
have lint: "islinintterm t" by simp
then have "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
by (induct t rule: islinintterm.induct) auto
moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
moreover
{ assume "\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r"
then obtain "i" "n" "r" where
inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
by blast
with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
by simp
have linr: "islinintterm r"
by (rule islinintterm_subt[OF lininr])
have ?case using prems zz
by (cases n) (simp_all add: nth_pos2
intterm_novar0[OF lininr, where x="x" and y="-x"])
}
ultimately show ?case by blast
qed simp_all
(* mirror preserves existence *)
lemma mirror_ex:
assumes unifp: "isunified p"
shows "(\<exists> x. (qinterp (x#ats) p)) = (\<exists> y. (qinterp (y#ats) (mirror p)))"
(is "(\<exists> x. ?P x) = (\<exists> y. ?MP y)")
proof
assume "\<exists> x. ?P x"
then obtain "x" where px:"?P x" by blast
have "?MP (-x)"
using px
by(simp add: mirror_interp[OF unifp, where x="x"])
then show "\<exists> y. ?MP y" by blast
next
assume "\<exists> y. ?MP y"
then obtain "y" where mpy: "?MP y" by blast
have "?P (-y)"
using mpy
by (simp add: mirror_interp[OF unifp, where x="-y"])
then show "\<exists> x. ?P x" by blast
qed
lemma mirror_ex2:
assumes unifp: "isunified p"
shows "qinterp ats (QEx p) = qinterp ats (QEx (mirror p))"
using mirror_ex[OF unifp] by simp
(* Cooper's theorem in its plusinfinity version *)
lemma cooper_pi_eq:
assumes unifp : "isunified p"
shows "(\<exists> x. qinterp (x#ats) p) =
((\<exists> j \<in> {1 .. (divlcm p)}. qinterp (-j#ats) (plusinf p)) \<or>
(\<exists> j \<in> {1 .. (divlcm p)}. \<exists> b \<in> set (aset p).
qinterp (((I_intterm (a#ats) b) - j)#ats) p))"
(is "(\<exists> x. ?P x) = ((\<exists> j\<in> {1 .. ?d}. ?PP (-j)) \<or> (\<exists> j \<in> ?D. \<exists> b\<in> ?A. ?P (?I a b - j)))")
proof-
have unifmp: "isunified (mirror p)" by (rule mirror_unified[OF unifp])
have th1:
"(\<exists> j\<in> {1 .. ?d}. ?PP (-j)) = (\<exists> j\<in> {1..?d}. qinterp (j # ats) (minusinf (mirror p)))"
by (simp add: plusinf_eq_minusinf_mirror[OF unifp])
have dth: "?d = divlcm (mirror p)"
by (rule divlcm_mirror_eq[OF unifp])
have "(\<exists> j \<in> ?D. \<exists> b\<in> ?A. ?P (?I a b - j)) =
(\<exists> j\<in> ?D. \<exists> b \<in> set (map lin_neg (bset (mirror p))). ?P (?I a b - j))"
by (simp only: aset_eq_bset_mirror[OF unifp])
also have "\<dots> = (\<exists> j\<in> ?D. \<exists> b \<in> set (bset (mirror p)). ?P (?I a (lin_neg b) - j))"
by simp
also have "\<dots> = (\<exists> j\<in> ?D. \<exists> b \<in> set (bset (mirror p)). ?P (-(?I a b + j)))"
proof
assume "\<exists>j\<in>{1..divlcm p}.
\<exists>b\<in>set (bset (mirror p)). qinterp ((I_intterm (a # ats) (lin_neg b) - j) # ats) p"
then
obtain "j" and "b" where
pbmj: "j\<in> ?D \<and> b\<in> set (bset (mirror p)) \<and> ?P (?I a (lin_neg b) - j)" by blast
then have linb: "islinintterm b"
by (auto simp add:bset_lin[OF unifmp])
from linb pbmj have "?P (-(?I a b + j))" by (simp add: lin_neg_corr)
then show "\<exists> j\<in> ?D. \<exists> b \<in> set (bset (mirror p)). ?P (-(?I a b + j))"
using pbmj
by auto
next
assume "\<exists> j\<in> ?D. \<exists> b \<in> set (bset (mirror p)). ?P (-(?I a b + j))"
then obtain "j" and "b" where
pbmj: "j\<in> ?D \<and> b\<in> set (bset (mirror p)) \<and> ?P (-(?I a b + j))"
by blast
then have linb: "islinintterm b"
by (auto simp add:bset_lin[OF unifmp])
from linb pbmj have "?P (?I a (lin_neg b) - j)"
by (simp add: lin_neg_corr)
then show "\<exists> j\<in> ?D. \<exists> b \<in> set (bset (mirror p)). ?P (?I a (lin_neg b) - j)"
using pbmj by auto
qed
finally
have bth: "(\<exists> j\<in> ?D. \<exists> b\<in> ?A. ?P (?I a b - j)) =
(\<exists>j\<in> ?D. \<exists> b\<in>set (bset (mirror p)).
qinterp ((I_intterm (a # ats) b + j) # ats) (mirror p))"
by (simp add: mirror_interp[OF unifp] zadd_ac)
from bth dth th1
have "(\<exists> x. ?P x) = (\<exists> x. qinterp (x#ats) (mirror p))"
by (simp add: mirror_ex[OF unifp])
also have "\<dots> = ((\<exists>j\<in>{1..divlcm (mirror p)}. qinterp (j # ats) (minusinf (mirror p))) \<or>
(\<exists>j\<in>{1..divlcm (mirror p)}.
\<exists>b\<in>set (bset (mirror p)). qinterp ((I_intterm (a # ats) b + j) # ats) (mirror p)))"
(is "(\<exists> x. ?MP x) = ((\<exists> j\<in> ?DM. ?MPM j) \<or> (\<exists> j \<in> ?DM. \<exists> b\<in> ?BM. ?MP (?I a b + j)))")
by (rule cooper_mi_eq[OF unifmp])
also
have "\<dots> = ((\<exists> j\<in> ?D. ?PP (-j)) \<or> (\<exists> j \<in> ?D. \<exists> b\<in> ?BM. ?MP (?I a b + j)))"
using bth th1 dth by simp
finally show ?thesis using sym[OF bth] by simp
qed
(* substitution of a term into a Qfree formula, substitution of Bound 0 by i*)
consts subst_it:: "intterm \<Rightarrow> intterm \<Rightarrow> intterm"
primrec
"subst_it i (Cst b) = Cst b"
"subst_it i (Var n) = (if n = 0 then i else Var n)"
"subst_it i (Neg it) = Neg (subst_it i it)"
"subst_it i (Add it1 it2) = Add (subst_it i it1) (subst_it i it2)"
"subst_it i (Sub it1 it2) = Sub (subst_it i it1) (subst_it i it2)"
"subst_it i (Mult it1 it2) = Mult (subst_it i it1) (subst_it i it2)"
(* subst_it preserves semantics *)
lemma subst_it_corr:
"I_intterm (a#ats) (subst_it i t) = I_intterm ((I_intterm (a#ats) i)#ats) t"
by (induct t rule: subst_it.induct, simp_all add: nth_pos2)
consts subst_p:: "intterm \<Rightarrow> QF \<Rightarrow> QF"
primrec
"subst_p i (Le it1 it2) = Le (subst_it i it1) (subst_it i it2)"
"subst_p i (Lt it1 it2) = Lt (subst_it i it1) (subst_it i it2)"
"subst_p i (Ge it1 it2) = Ge (subst_it i it1) (subst_it i it2)"
"subst_p i (Gt it1 it2) = Gt (subst_it i it1) (subst_it i it2)"
"subst_p i (Eq it1 it2) = Eq (subst_it i it1) (subst_it i it2)"
"subst_p i (Divides d t) = Divides (subst_it i d) (subst_it i t)"
"subst_p i T = T"
"subst_p i F = F"
"subst_p i (And p q) = And (subst_p i p) (subst_p i q)"
"subst_p i (Or p q) = Or (subst_p i p) (subst_p i q)"
"subst_p i (Imp p q) = Imp (subst_p i p) (subst_p i q)"
"subst_p i (Equ p q) = Equ (subst_p i p) (subst_p i q)"
"subst_p i (NOT p) = (NOT (subst_p i p))"
(* subs_p preserves correctness *)
lemma subst_p_corr:
assumes qf: "isqfree p"
shows "qinterp (a # ats) (subst_p i p) = qinterp ((I_intterm (a#ats) i)#ats) p "
using qf
by (induct p rule: subst_p.induct) (simp_all add: subst_it_corr)
(* novar0 p is true if the fomula doese not depend on the quantified variable*)
consts novar0I:: "intterm \<Rightarrow> bool"
primrec
"novar0I (Cst i) = True"
"novar0I (Var n) = (n > 0)"
"novar0I (Neg a) = (novar0I a)"
"novar0I (Add a b) = (novar0I a \<and> novar0I b)"
"novar0I (Sub a b) = (novar0I a \<and> novar0I b)"
"novar0I (Mult a b) = (novar0I a \<and> novar0I b)"
consts novar0:: "QF \<Rightarrow> bool"
recdef novar0 "measure size"
"novar0 (Lt a b) = (novar0I a \<and> novar0I b)"
"novar0 (Gt a b) = (novar0I a \<and> novar0I b)"
"novar0 (Le a b) = (novar0I a \<and> novar0I b)"
"novar0 (Ge a b) = (novar0I a \<and> novar0I b)"
"novar0 (Eq a b) = (novar0I a \<and> novar0I b)"
"novar0 (Divides a b) = (novar0I a \<and> novar0I b)"
"novar0 T = True"
"novar0 F = True"
"novar0 (NOT p) = novar0 p"
"novar0 (And p q) = (novar0 p \<and> novar0 q)"
"novar0 (Or p q) = (novar0 p \<and> novar0 q)"
"novar0 (Imp p q) = (novar0 p \<and> novar0 q)"
"novar0 (Equ p q) = (novar0 p \<and> novar0 q)"
"novar0 p = False"
(* Interpretation of terms, that doese not depend on Var 0 *)
lemma I_intterm_novar0:
assumes nov0: "novar0I x"
shows "I_intterm (a#ats) x = I_intterm (b#ats) x"
using nov0
by (induct x) (auto simp add: nth_pos2)
(* substition is meaningless for term independent of Var 0*)
lemma subst_p_novar0_corr:
assumes qfp: "isqfree p"
and nov0: "novar0I i"
shows "qinterp (a#ats) (subst_p i p) = qinterp (I_intterm (b#ats) i#ats) p"
proof-
have "qinterp (a#ats) (subst_p i p) = qinterp (I_intterm (a#ats) i#ats) p"
by (rule subst_p_corr[OF qfp])
moreover have "I_intterm (a#ats) i#ats = I_intterm (b#ats) i#ats"
by (simp add: I_intterm_novar0[OF nov0, where a="a" and b="b"])
ultimately show ?thesis by simp
qed
(* linearity and independence on Var 0*)
lemma lin_novar0:
assumes linx: "islinintterm x"
and nov0: "novar0I x"
shows "\<exists> n > 0. islintn(n,x)"
using linx nov0
by (induct x rule: islinintterm.induct) auto
lemma lintnpos_novar0:
assumes npos: "n > 0"
and linx: "islintn(n,x)"
shows "novar0I x"
using npos linx
by (induct n x rule: islintn.induct) auto
(* lin_add preserves independence on Var 0*)
lemma lin_add_novar0:
assumes nov0a: "novar0I a"
and nov0b : "novar0I b"
and lina : "islinintterm a"
and linb: "islinintterm b"
shows "novar0I (lin_add (a,b))"
proof-
have "\<exists> na > 0. islintn(na, a)" by (rule lin_novar0[OF lina nov0a])
then obtain "na" where na: "na > 0 \<and> islintn(na,a)" by blast
have "\<exists> nb > 0. islintn(nb, b)" by (rule lin_novar0[OF linb nov0b])
then obtain "nb" where nb: "nb > 0 \<and> islintn(nb,b)" by blast
from na have napos: "na > 0" by simp
from na have linna: "islintn(na,a)" by simp
from nb have nbpos: "nb > 0" by simp
from nb have linnb: "islintn(nb,b)" by simp
have "min na nb \<le> min na nb" by simp
then have "islintn (min na nb, lin_add(a,b))" by (simp add: lin_add_lint[OF linna linnb])
moreover have "min na nb > 0" using napos nbpos by (simp add: min_def)
ultimately show ?thesis by (simp only: lintnpos_novar0)
qed
(* lin__mul preserves independence on Var 0*)
lemma lin_mul_novar0:
assumes linx: "islinintterm x"
and nov0: "novar0I x"
shows "novar0I (lin_mul(i,x))"
using linx nov0
proof (induct i x rule: lin_mul.induct, auto)
case (goal1 c c' n r)
from prems have lincnr: "islinintterm (Add (Mult (Cst c') (Var n)) r)" by simp
have "islinintterm r" by (rule islinintterm_subt[OF lincnr])
then show ?case using prems by simp
qed
(* lin_neg preserves indepenednce on Var 0*)
lemma lin_neg_novar0:
assumes linx: "islinintterm x"
and nov0: "novar0I x"
shows "novar0I (lin_neg x)"
by (auto simp add: lin_mul_novar0 linx nov0 lin_neg_def)
(* subterms of linear terms are independent on Var 0*)
lemma intterm_subt_novar0:
assumes lincnr: "islinintterm (Add (Mult (Cst c) (Var n)) r)"
shows "novar0I r"
proof-
have cnz: "c \<noteq> 0" by (rule islinintterm_cnz[OF lincnr])
have "islintn(0,Add (Mult (Cst c) (Var n)) r)" using lincnr
by (simp only: islinintterm_eq_islint islint_def)
then have "islintn (n+1,r)" by auto
moreover have "n+1 >0 " by arith
ultimately show ?thesis
using lintnpos_novar0
by auto
qed
(* decrease the De-Bruijn indices*)
consts decrvarsI:: "intterm \<Rightarrow> intterm"
primrec
"decrvarsI (Cst i) = (Cst i)"
"decrvarsI (Var n) = (Var (n - 1))"
"decrvarsI (Neg a) = (Neg (decrvarsI a))"
"decrvarsI (Add a b) = (Add (decrvarsI a) (decrvarsI b))"
"decrvarsI (Sub a b) = (Sub (decrvarsI a) (decrvarsI b))"
"decrvarsI (Mult a b) = (Mult (decrvarsI a) (decrvarsI b))"
(* One can decrease the indics for terms and formulae independent on Var 0*)
lemma intterm_decrvarsI:
assumes nov0: "novar0I t"
shows "I_intterm (a#ats) t = I_intterm ats (decrvarsI t)"
using nov0
by (induct t) (auto simp add: nth_pos2)
consts decrvars:: "QF \<Rightarrow> QF"
primrec
"decrvars (Lt a b) = (Lt (decrvarsI a) (decrvarsI b))"
"decrvars (Gt a b) = (Gt (decrvarsI a) (decrvarsI b))"
"decrvars (Le a b) = (Le (decrvarsI a) (decrvarsI b))"
"decrvars (Ge a b) = (Ge (decrvarsI a) (decrvarsI b))"
"decrvars (Eq a b) = (Eq (decrvarsI a) (decrvarsI b))"
"decrvars (Divides a b) = (Divides (decrvarsI a) (decrvarsI b))"
"decrvars T = T"
"decrvars F = F"
"decrvars (NOT p) = (NOT (decrvars p))"
"decrvars (And p q) = (And (decrvars p) (decrvars q))"
"decrvars (Or p q) = (Or (decrvars p) (decrvars q))"
"decrvars (Imp p q) = (Imp (decrvars p) (decrvars q))"
"decrvars (Equ p q) = (Equ (decrvars p) (decrvars q))"
(* decrvars preserves quantifier freeness*)
lemma decrvars_qfree: "isqfree p \<Longrightarrow> isqfree (decrvars p)"
by (induct p rule: isqfree.induct, auto)
lemma novar0_qfree: "novar0 p \<Longrightarrow> isqfree p"
by (induct p) auto
lemma qinterp_novar0:
assumes nov0: "novar0 p"
shows "qinterp (a#ats) p = qinterp ats (decrvars p)"
using nov0
by(induct p) (simp_all add: intterm_decrvarsI)
(* All elements of bset p doese not depend on Var 0*)
lemma bset_novar0:
assumes unifp: "isunified p"
shows "\<forall> b\<in> set (bset p). novar0I b "
using unifp
proof(induct p rule: bset.induct)
case (1 c r z)
from prems have zz: "z = Cst 0" by (cases "z", auto)
from prems zz have lincnr: "islinintterm(Add (Mult (Cst c) (Var 0)) r)" by simp
have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
have novar0r: "novar0I r" by (rule intterm_subt_novar0[OF lincnr])
from prems zz have "c = 1 \<or> c = -1" by auto
moreover
{
assume c1: "c=1"
have lin1: "islinintterm (Cst 1)" by simp
have novar01: "novar0I (Cst 1)" by simp
then have ?case
using prems zz novar0r lin1 novar01
by (auto simp add: lin_add_novar0 lin_neg_novar0 linr lin_neg_lin)
}
moreover
{
assume c1: "c= -1"
have lin1: "islinintterm (Cst -1)" by simp
have novar01: "novar0I (Cst -1)" by simp
then have ?case
using prems zz novar0r lin1 novar01
by (auto simp add: lin_add_novar0 lin_neg_novar0 linr lin_neg_lin)
}
ultimately show ?case by blast
next
case (2 c r z)
from prems have zz: "z = Cst 0" by (cases "z", auto)
from prems zz have lincnr: "islinintterm(Add (Mult (Cst c) (Var 0)) r)" by simp
have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
have novar0r: "novar0I r" by (rule intterm_subt_novar0[OF lincnr])
from prems zz have "c = 1 \<or> c = -1" by auto
moreover
{
assume c1: "c=1"
have lin1: "islinintterm (Cst 1)" by simp
have novar01: "novar0I (Cst 1)" by simp
then have ?case
using prems zz novar0r lin1 novar01
by (auto simp add: lin_add_novar0 lin_neg_novar0 linr lin_neg_lin)
}
moreover
{
assume c1: "c= -1"
have lin1: "islinintterm (Cst -1)" by simp
have novar01: "novar0I (Cst -1)" by simp
then have ?case
using prems zz novar0r lin1 novar01
by (auto simp add: lin_add_novar0 lin_neg_novar0 linr lin_neg_lin)
}
ultimately show ?case by blast
next
case (3 c r z)
from prems have zz: "z = Cst 0" by (cases "z", auto)
from prems zz have lincnr: "islinintterm(Add (Mult (Cst c) (Var 0)) r)" by simp
have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
have novar0r: "novar0I r" by (rule intterm_subt_novar0[OF lincnr])
from prems zz have "c = 1 \<or> c = -1" by auto
moreover
{
assume c1: "c=1"
have lin1: "islinintterm (Cst 1)" by simp
have novar01: "novar0I (Cst 1)" by simp
then have ?case
using prems zz novar0r lin1 novar01
by (auto simp add: lin_add_novar0 lin_neg_novar0 linr lin_neg_lin)
}
moreover
{
assume c1: "c= -1"
have lin1: "islinintterm (Cst -1)" by simp
have novar01: "novar0I (Cst -1)" by simp
then have ?case
using prems zz novar0r lin1 novar01
by (auto simp add: lin_add_novar0 lin_neg_novar0 linr lin_neg_lin)
}
ultimately show ?case by blast
qed auto
(* substitution preserves independence on Var 0*)
lemma subst_it_novar0:
assumes nov0x: "novar0I x"
shows "novar0I (subst_it x t)"
using nov0x
by (induct t) auto
lemma subst_p_novar0:
assumes nov0x:"novar0I x"
and qfp: "isqfree p"
shows "novar0 (subst_p x p)"
using nov0x qfp
by (induct p rule: novar0.induct) (simp_all add: subst_it_novar0)
(* linearize preserves independence on Var 0 *)
lemma linearize_novar0:
assumes nov0t: "novar0I t "
shows "\<And> t'. linearize t = Some t' \<Longrightarrow> novar0I t'"
using nov0t
proof(induct t rule: novar0I.induct)
case (Neg a)
let ?la = "linearize a"
from prems have "\<exists> a'. ?la = Some a'" by (cases ?la, auto)
then obtain "a'" where "?la = Some a'" by blast
with prems have nv0a':"novar0I a'" by simp
have "islinintterm a'" using prems by (simp add: linearize_linear)
with nv0a' have "novar0I (lin_neg a')"
by (simp add: lin_neg_novar0)
then
show ?case using prems by simp
next
case (Add a b)
let ?la = "linearize a"
let ?lb = "linearize b"
from prems have linab: "linearize (Add a b) = Some t'" by simp
then have "\<exists> a'. ?la = Some a'" by (cases ?la) auto
then obtain "a'" where "?la = Some a'" by blast
with prems have nv0a':"novar0I a'" by simp
have lina': "islinintterm a'" using prems by (simp add: linearize_linear)
from linab have "\<exists> b'. ?lb = Some b'"
by (cases ?la, auto) (cases ?lb, auto)
then obtain "b'" where "?lb = Some b'" by blast
with prems have nv0b':"novar0I b'" by simp
have linb': "islinintterm b'" using prems by (simp add: linearize_linear)
then show ?case using prems lina' linb' nv0a' nv0b'
by (auto simp add: lin_add_novar0)
next
case (Sub a b)
let ?la = "linearize a"
let ?lb = "linearize b"
from prems have linab: "linearize (Sub a b) = Some t'" by simp
then have "\<exists> a'. ?la = Some a'" by (cases ?la) auto
then obtain "a'" where "?la = Some a'" by blast
with prems have nv0a':"novar0I a'" by simp
have lina': "islinintterm a'" using prems by (simp add: linearize_linear)
from linab have "\<exists> b'. ?lb = Some b'"
by (cases ?la, auto) (cases ?lb, auto)
then obtain "b'" where "?lb = Some b'" by blast
with prems have nv0b':"novar0I b'" by simp
have linb': "islinintterm b'" using prems by (simp add: linearize_linear)
then show ?case using prems lina' linb' nv0a' nv0b'
by (auto simp add: lin_add_novar0 lin_neg_novar0 lin_neg_lin)
next
case (Mult a b)
let ?la = "linearize a"
let ?lb = "linearize b"
from prems have linab: "linearize (Mult a b) = Some t'" by simp
then have "\<exists> a'. ?la = Some a'" by (cases ?la, auto)
then obtain "a'" where "?la = Some a'" by blast
with prems have nv0a':"novar0I a'" by simp
have lina': "islinintterm a'" using prems by (simp add: linearize_linear)
from prems linab have "\<exists> b'. ?lb = Some b'"
apply (cases ?la, auto)
by (cases "a'",auto) (cases ?lb, auto)+
then obtain "b'" where "?lb = Some b'" by blast
with prems have nv0b':"novar0I b'" by simp
have linb': "islinintterm b'" using prems by (simp add: linearize_linear)
then show ?case using prems lina' linb' nv0a' nv0b'
by (cases "a'",auto simp add: lin_mul_novar0)
(cases "b'",auto simp add: lin_mul_novar0)
qed auto
(* simplification of formulae *)
consts psimpl :: "QF \<Rightarrow> QF"
recdef psimpl "measure size"
"psimpl (Le l r) =
(case (linearize (Sub l r)) of
None \<Rightarrow> Le l r
| Some x \<Rightarrow> (case x of
Cst i \<Rightarrow> (if i \<le> 0 then T else F)
| _ \<Rightarrow> (Le x (Cst 0))))"
"psimpl (Eq l r) =
(case (linearize (Sub l r)) of
None \<Rightarrow> Eq l r
| Some x \<Rightarrow> (case x of
Cst i \<Rightarrow> (if i = 0 then T else F)
| _ \<Rightarrow> (Eq x (Cst 0))))"
"psimpl (Divides (Cst d) t) =
(case (linearize t) of
None \<Rightarrow> (Divides (Cst d) t)
| Some c \<Rightarrow> (case c of
Cst i \<Rightarrow> (if d dvd i then T else F)
| _ \<Rightarrow> (Divides (Cst d) c)))"
"psimpl (And p q) =
(let p'= psimpl p
in (case p' of
F \<Rightarrow> F
|T \<Rightarrow> psimpl q
| _ \<Rightarrow> let q' = psimpl q
in (case q' of
F \<Rightarrow> F
| T \<Rightarrow> p'
| _ \<Rightarrow> (And p' q'))))"
"psimpl (Or p q) =
(let p'= psimpl p
in (case p' of
T \<Rightarrow> T
| F \<Rightarrow> psimpl q
| _ \<Rightarrow> let q' = psimpl q
in (case q' of
T \<Rightarrow> T
| F \<Rightarrow> p'
| _ \<Rightarrow> (Or p' q'))))"
"psimpl (Imp p q) =
(let p'= psimpl p
in (case p' of
F \<Rightarrow> T
|T \<Rightarrow> psimpl q
| NOT p1 \<Rightarrow> let q' = psimpl q
in (case q' of
F \<Rightarrow> p1
| T \<Rightarrow> T
| _ \<Rightarrow> (Or p1 q'))
| _ \<Rightarrow> let q' = psimpl q
in (case q' of
F \<Rightarrow> NOT p'
| T \<Rightarrow> T
| _ \<Rightarrow> (Imp p' q'))))"
"psimpl (Equ p q) =
(let p'= psimpl p ; q' = psimpl q
in (case p' of
T \<Rightarrow> q'
| F \<Rightarrow> (case q' of
T \<Rightarrow> F
| F \<Rightarrow> T
| NOT q1 \<Rightarrow> q1
| _ \<Rightarrow> NOT q')
| NOT p1 \<Rightarrow> (case q' of
T \<Rightarrow> p'
| F \<Rightarrow> p1
| NOT q1 \<Rightarrow> (Equ p1 q1)
| _ \<Rightarrow> (Equ p' q'))
| _ \<Rightarrow> (case q' of
T \<Rightarrow> p'
| F \<Rightarrow> NOT p'
| _ \<Rightarrow> (Equ p' q'))))"
"psimpl (NOT p) =
(let p' = psimpl p
in ( case p' of
F \<Rightarrow> T
| T \<Rightarrow> F
| NOT p1 \<Rightarrow> p1
| _ \<Rightarrow> (NOT p')))"
"psimpl p = p"
(* psimpl preserves semantics *)
lemma psimpl_corr: "qinterp ats p = qinterp ats (psimpl p)"
proof(induct p rule: psimpl.induct)
case (1 l r)
have "(\<exists> lx. linearize (Sub l r) = Some lx) \<or> (linearize (Sub l r) = None)" by auto
moreover
{
assume lin: "\<exists> lx. linearize (Sub l r) = Some lx"
from lin obtain "lx" where lx: "linearize (Sub l r) = Some lx" by blast
from lx have "I_intterm ats (Sub l r) = I_intterm ats lx"
by (rule linearize_corr[where t="Sub l r" and t'= "lx"])
then have feq: "qinterp ats (Le l r) = qinterp ats (Le lx (Cst 0))" by (simp , arith)
from lx have lxlin: "islinintterm lx" by (rule linearize_linear)
from lxlin feq have ?case
proof-
have "(\<exists> i. lx = Cst i) \<or> (\<not> (\<exists> i. lx = Cst i))" by blast
moreover
{
assume lxcst: "\<exists> i. lx = Cst i"
from lxcst obtain "i" where lxi: "lx = Cst i" by blast
with feq have "qinterp ats (Le l r) = (i \<le> 0)" by simp
then have ?case using prems by simp
}
moreover
{
assume "(\<not> (\<exists> i. lx = Cst i))"
then have "(case lx of
Cst i \<Rightarrow> (if i \<le> 0 then T else F)
| _ \<Rightarrow> (Le lx (Cst 0))) = (Le lx (Cst 0))"
by (case_tac "lx::intterm", auto)
with prems lxlin feq have ?case by auto
}
ultimately show ?thesis by blast
qed
}
moreover
{
assume "linearize (Sub l r) = None"
then have ?case using prems by simp
}
ultimately show ?case by blast
next
case (2 l r)
have "(\<exists> lx. linearize (Sub l r) = Some lx) \<or> (linearize (Sub l r) = None)" by auto
moreover
{
assume lin: "\<exists> lx. linearize (Sub l r) = Some lx"
from lin obtain "lx" where lx: "linearize (Sub l r) = Some lx" by blast
from lx have "I_intterm ats (Sub l r) = I_intterm ats lx"
by (rule linearize_corr[where t="Sub l r" and t'= "lx"])
then have feq: "qinterp ats (Eq l r) = qinterp ats (Eq lx (Cst 0))" by (simp , arith)
from lx have lxlin: "islinintterm lx" by (rule linearize_linear)
from lxlin feq have ?case
proof-
have "(\<exists> i. lx = Cst i) \<or> (\<not> (\<exists> i. lx = Cst i))" by blast
moreover
{
assume lxcst: "\<exists> i. lx = Cst i"
from lxcst obtain "i" where lxi: "lx = Cst i" by blast
with feq have "qinterp ats (Eq l r) = (i = 0)" by simp
then have ?case using prems by simp
}
moreover
{
assume "(\<not> (\<exists> i. lx = Cst i))"
then have "(case lx of
Cst i \<Rightarrow> (if i = 0 then T else F)
| _ \<Rightarrow> (Eq lx (Cst 0))) = (Eq lx (Cst 0))"
by (case_tac "lx::intterm", auto)
with prems lxlin feq have ?case by auto
}
ultimately show ?thesis by blast
qed
}
moreover
{
assume "linearize (Sub l r) = None"
then have ?case using prems by simp
}
ultimately show ?case by blast
next
case (3 d t)
have "(\<exists> lt. linearize t = Some lt) \<or> (linearize t = None)" by auto
moreover
{
assume lin: "\<exists> lt. linearize t = Some lt"
from lin obtain "lt" where lt: "linearize t = Some lt" by blast
from lt have "I_intterm ats t = I_intterm ats lt"
by (rule linearize_corr[where t="t" and t'= "lt"])
then have feq: "qinterp ats (Divides (Cst d) t) = qinterp ats (Divides (Cst d) lt)" by (simp)
from lt have ltlin: "islinintterm lt" by (rule linearize_linear)
from ltlin feq have ?case using prems apply simp by (case_tac "lt::intterm", simp_all)
}
moreover
{
assume "linearize t = None"
then have ?case using prems by simp
}
ultimately show ?case by blast
next
case (4 f g)
let ?sf = "psimpl f"
let ?sg = "psimpl g"
show ?case using prems
by (cases ?sf, simp_all add: Let_def) (cases ?sg, simp_all)+
next
case (5 f g)
let ?sf = "psimpl f"
let ?sg = "psimpl g"
show ?case using prems
apply (cases ?sf, simp_all add: Let_def)
apply (cases ?sg, simp_all)
apply (cases ?sg, simp_all)
apply (cases ?sg, simp_all)
apply (cases ?sg, simp_all)
apply (cases ?sg, simp_all)
apply (cases ?sg, simp_all)
apply (cases ?sg, simp_all)
apply blast
apply (cases ?sg, simp_all)
apply (cases ?sg, simp_all)
apply (cases ?sg, simp_all)
apply blast
apply (cases ?sg, simp_all)
by (cases ?sg, simp_all) (cases ?sg, simp_all)
next
case (6 f g)
let ?sf = "psimpl f"
let ?sg = "psimpl g"
show ?case using prems
apply(simp add: Let_def)
apply(cases ?sf,simp_all)
apply (simp_all add: Let_def)
apply(cases ?sg, simp_all)
apply(cases ?sg, simp_all)
apply(cases ?sg, simp_all)
apply(cases ?sg, simp_all)
apply(cases ?sg, simp_all)
apply(cases ?sg, simp_all)
apply(cases ?sg, simp_all)
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply(cases ?sg, simp_all)
apply(cases ?sg, simp_all)
apply(cases ?sg, simp_all)
apply(cases ?sg, simp_all)
apply(cases ?sg, simp_all)
apply(cases ?sg, simp_all)
done
next
case (7 f g)
let ?sf = "psimpl f"
let ?sg = "psimpl g"
show ?case
using prems
by (cases ?sf, simp_all add: Let_def) (cases ?sg, simp_all)+
next
case (8 f) show ?case
using prems
apply (simp add: Let_def)
by (case_tac "psimpl f", simp_all)
qed simp_all
(* psimpl preserves independence on Var 0*)
lemma psimpl_novar0:
assumes nov0p: "novar0 p"
shows "novar0 (psimpl p)"
using nov0p
proof (induct p rule: psimpl.induct)
case (1 l r)
let ?ls = "linearize (Sub l r)"
have "?ls = None \<or> (\<exists> x. ?ls = Some x)" by auto
moreover
{
assume "?ls = None" then have ?case using prems by simp
}
moreover {
assume "\<exists> x. ?ls = Some x"
then obtain "x" where ls_d: "?ls = Some x" by blast
from prems have "novar0I l" by simp
moreover from prems have "novar0I r" by simp
ultimately have nv0s: "novar0I (Sub l r)" by simp
from prems have "novar0I x"
by (simp add: linearize_novar0[OF nv0s, where t'="x"])
then have ?case
using prems
by (cases "x") auto
}
ultimately show ?case by blast
next
case (2 l r)
let ?ls = "linearize (Sub l r)"
have "?ls = None \<or> (\<exists> x. ?ls = Some x)" by auto
moreover
{
assume "?ls = None" then have ?case using prems by simp
}
moreover {
assume "\<exists> x. ?ls = Some x"
then obtain "x" where ls_d: "?ls = Some x" by blast
from prems have "novar0I l" by simp
moreover from prems have "novar0I r" by simp
ultimately have nv0s: "novar0I (Sub l r)" by simp
from prems have "novar0I x"
by (simp add: linearize_novar0[OF nv0s, where t'="x"])
then have ?case using prems by (cases "x") auto
}
ultimately show ?case by blast
next
case (3 d t)
let ?lt = "linearize t"
have "?lt = None \<or> (\<exists> x. ?lt = Some x)" by auto
moreover
{ assume "?lt = None" then have ?case using prems by simp }
moreover {
assume "\<exists>x. ?lt = Some x"
then obtain "x" where x_d: "?lt = Some x" by blast
from prems have nv0t: "novar0I t" by simp
with x_d have "novar0I x"
by (simp add: linearize_novar0[OF nv0t])
with prems have ?case
by (cases "x") simp_all
}
ultimately show ?case by blast
next
case (4 f g)
let ?sf = "psimpl f"
let ?sg = "psimpl g"
show ?case using prems
by (cases ?sf, simp_all add: Let_def) (cases ?sg,simp_all)+
next
case (5 f g)
let ?sf = "psimpl f"
let ?sg = "psimpl g"
show ?case using prems
by (cases ?sf, simp_all add: Let_def) (cases ?sg,simp_all)+
next
case (6 f g)
let ?sf = "psimpl f"
let ?sg = "psimpl g"
show ?case using prems
by (cases ?sf, simp_all add: Let_def) (cases ?sg,simp_all)+
next
case (7 f g)
let ?sf = "psimpl f"
let ?sg = "psimpl g"
show ?case using prems
by (cases ?sf, simp_all add: Let_def) (cases ?sg,simp_all)+
next
case (8 f)
let ?sf = "psimpl f"
from prems have nv0sf:"novar0 ?sf" by simp
show ?case using prems nv0sf by (cases ?sf, auto simp add: Let_def)
qed simp_all
(* implements a disj of p applied to all elements of the list*)
consts explode_disj :: "(intterm list \<times> QF) \<Rightarrow> QF"
recdef explode_disj "measure (\<lambda>(is,p). length is)"
"explode_disj ([],p) = F"
"explode_disj (i#is,p) =
(let pi = psimpl (subst_p i p)
in ( case pi of
T \<Rightarrow> T
| F \<Rightarrow> explode_disj (is,p)
| _ \<Rightarrow> (let r = explode_disj (is,p)
in (case r of
T \<Rightarrow> T
| F \<Rightarrow> pi
| _ \<Rightarrow> Or pi r))))"
(* correctness theorem for one iteration of explode_disj *)
lemma explode_disj_disj:
assumes qfp: "isqfree p"
shows "(qinterp (x#xs) (explode_disj(i#is,p))) =
(qinterp (x#xs) (subst_p i p) \<or> (qinterp (x#xs) (explode_disj(is,p))))"
using qfp
proof-
let ?pi = "psimpl (subst_p i p)"
have pi: "qinterp (x#xs) ?pi = qinterp (x#xs) (subst_p i p)"
by (simp add: psimpl_corr[where p="(subst_p i p)"])
let ?dp = "explode_disj(is,p)"
show ?thesis using pi
proof (cases)
assume "?pi= T \<or> ?pi = F"
then show ?thesis using pi by (case_tac "?pi::QF", auto)
next
assume notTF: "\<not> (?pi = T \<or> ?pi = F)"
let ?dp = "explode_disj(is,p)"
have dp_cases: "explode_disj(i#is,p) =
(case (explode_disj(is,p)) of
T \<Rightarrow> T
| F \<Rightarrow> psimpl (subst_p i p)
| _ \<Rightarrow> Or (psimpl (subst_p i p)) (explode_disj(is,p)))" using notTF
by (cases "?pi")
(simp_all add: Let_def cong del: QF.weak_case_cong)
show ?thesis using pi dp_cases notTF
proof(cases)
assume "?dp = T \<or> ?dp = F"
then show ?thesis
using pi dp_cases
by (cases "?dp") auto
next
assume "\<not> (?dp = T \<or> ?dp = F)"
then show ?thesis using pi dp_cases notTF
by (cases ?dp) auto
qed
qed
qed
(* correctness theorem for explode_disj *)
lemma explode_disj_corr:
assumes qfp: "isqfree p"
shows "(\<exists> x \<in> set xs. qinterp (a#ats) (subst_p x p)) =
(qinterp (a#ats) (explode_disj(xs,p)))" (is "(\<exists> x \<in> set xs. ?P x) = (?DP a xs )")
using qfp
proof (induct xs)
case Nil show ?case by simp
next
case (Cons y ys)
have "(\<exists> x \<in> set (y#ys). ?P x) = (?P y \<or> (\<exists> x\<in> set ys. ?P x))"
by auto
also have "\<dots> = (?P y \<or> ?DP a ys)" using "Cons.hyps" qfp by auto
also have "\<dots> = ?DP a (y#ys)" using explode_disj_disj[OF qfp] by auto
finally show ?case by simp
qed
(* explode_disj preserves independence on Var 0*)
lemma explode_disj_novar0:
assumes nov0xs: "\<forall>x \<in> set xs. novar0I x"
and qfp: "isqfree p"
shows "novar0 (explode_disj (xs,p))"
using nov0xs qfp
proof (induct xs, auto simp add: Let_def)
case (goal1 a as)
let ?q = "subst_p a p"
let ?qs = "psimpl ?q"
have "?qs = T \<or> ?qs = F \<or> (?qs \<noteq> T \<or> ?qs \<noteq> F)" by simp
moreover
{ assume "?qs = T" then have ?case by simp }
moreover
{ assume "?qs = F" then have ?case by simp }
moreover
{
assume qsnTF: "?qs \<noteq> T \<and> ?qs \<noteq> F"
let ?r = "explode_disj (as,p)"
have nov0qs: "novar0 ?qs"
using prems
by (auto simp add: psimpl_novar0 subst_p_novar0)
have "?r = T \<or> ?r = F \<or> (?r \<noteq> T \<or> ?r \<noteq> F)" by simp
moreover
{ assume "?r = T" then have ?case by (cases ?qs) auto }
moreover
{ assume "?r = F" then have ?case using nov0qs by (cases ?qs, auto) }
moreover
{ assume "?r \<noteq> T \<and> ?r \<noteq> F" then have ?case using nov0qs prems qsnTF
by (cases ?qs, auto simp add: Let_def) (cases ?r,auto)+
}
ultimately have ?case by blast
}
ultimately show ?case by blast
qed
(* Some simple lemmas used for technical reasons *)
lemma eval_Or_cases:
"qinterp (a#ats) (case f of
T \<Rightarrow> T
| F \<Rightarrow> g
| _ \<Rightarrow> (case g of
T \<Rightarrow> T
| F \<Rightarrow> f
| _ \<Rightarrow> Or f g)) = (qinterp (a#ats) f \<or> qinterp (a#ats) g)"
proof-
let ?result = "
(case f of
T \<Rightarrow> T
| F \<Rightarrow> g
| _ \<Rightarrow> (case g of
T \<Rightarrow> T
| F \<Rightarrow> f
| _ \<Rightarrow> Or f g))"
have "f = T \<or> f = F \<or> (f \<noteq> T \<and> f\<noteq> F)" by auto
moreover
{
assume fT: "f = T"
then have ?thesis by auto
}
moreover
{
assume "f=F"
then have ?thesis by auto
}
moreover
{
assume fnT: "f\<noteq>T"
and fnF: "f\<noteq>F"
have "g = T \<or> g = F \<or> (g \<noteq> T \<and> g\<noteq> F)" by auto
moreover
{
assume "g=T"
then have ?thesis using fnT fnF by (cases f, auto)
}
moreover
{
assume "g=F"
then have ?thesis using fnT fnF by (cases f, auto)
}
moreover
{
assume gnT: "g\<noteq>T"
and gnF: "g\<noteq>F"
then have "?result = (case g of
T \<Rightarrow> T
| F \<Rightarrow> f
| _ \<Rightarrow> Or f g)"
using fnT fnF
by (cases f, auto)
also have "\<dots> = Or f g"
using gnT gnF
by (cases g, auto)
finally have "?result = Or f g" by simp
then
have ?thesis by simp
}
ultimately have ?thesis by blast
}
ultimately show ?thesis by blast
qed
lemma or_case_novar0:
assumes fnTF: "f \<noteq> T \<and> f \<noteq> F"
and gnTF: "g \<noteq> T \<and> g \<noteq> F"
and f0: "novar0 f"
and g0: "novar0 g"
shows "novar0
(case f of T \<Rightarrow> T | F \<Rightarrow> g
| _ \<Rightarrow> (case g of T \<Rightarrow> T | F \<Rightarrow> f | _ \<Rightarrow> Or f g))"
using fnTF gnTF f0 g0
by (cases f, auto) (cases g, auto)+
(* An implementation of sets trough lists *)
definition
list_insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
"list_insert x xs = (if x mem xs then xs else x#xs)"
lemma list_insert_set: "set (list_insert x xs) = set (x#xs)"
by(induct xs) (auto simp add: list_insert_def)
consts list_union :: "('a list \<times> 'a list) \<Rightarrow> 'a list"
recdef list_union "measure (\<lambda>(xs,ys). length xs)"
"list_union ([], ys) = ys"
"list_union (xs, []) = xs"
"list_union (x#xs,ys) = list_insert x (list_union (xs,ys))"
lemma list_union_set: "set (list_union(xs,ys)) = set (xs@ys)"
by(induct xs ys rule: list_union.induct, auto simp add:list_insert_set)
consts list_set ::"'a list \<Rightarrow> 'a list"
primrec
"list_set [] = []"
"list_set (x#xs) = list_insert x (list_set xs)"
lemma list_set_set: "set xs = set (list_set xs)"
by (induct xs) (auto simp add: list_insert_set)
consts iupto :: "int \<times> int \<Rightarrow> int list"
recdef iupto "measure (\<lambda> (i,j). nat (j - i +1))"
"iupto(i,j) = (if j<i then [] else (i#(iupto(i+1,j))))"
(* correctness theorem for iupto *)
lemma iupto_set: "set (iupto(i,j)) = {i .. j}"
proof(induct rule: iupto.induct)
case (1 a b)
show ?case
using prems by (simp add: simp_from_to)
qed
consts all_sums :: "int \<times> intterm list \<Rightarrow> intterm list"
recdef all_sums "measure (\<lambda>(i,is). length is)"
"all_sums (j,[]) = []"
"all_sums (j,i#is) = (map (\<lambda>x. lin_add (i,(Cst x))) (iupto(1,j))@(all_sums (j,is)))"
(* all_sums preserves independence on Var 0*)
lemma all_sums_novar0:
assumes nov0xs: "\<forall> x\<in> set xs. novar0I x"
and linxs: "\<forall> x\<in> set xs. islinintterm x "
shows "\<forall> x\<in> set (all_sums (d,xs)). novar0I x"
using nov0xs linxs
proof(induct d xs rule: all_sums.induct)
case 1 show ?case by simp
next
case (2 j a as)
have lina: "islinintterm a" using "2.prems" by auto
have nov0a: "novar0I a" using "2.prems" by auto
let ?ys = "map (\<lambda>x. lin_add (a,(Cst x))) (iupto(1,j))"
have nov0ys: "\<forall> y\<in> set ?ys. novar0I y"
proof-
have linx: "\<forall> x \<in> set (iupto(1,j)). islinintterm (Cst x)" by simp
have nov0x: "\<forall> x \<in> set (iupto(1,j)). novar0I (Cst x)" by simp
with nov0a lina linx have "\<forall> x\<in> set (iupto(1,j)). novar0I (lin_add (a,Cst x))"
by (simp add: lin_add_novar0)
then show ?thesis by auto
qed
from "2.prems"
have linas: "\<forall>u\<in>set as. islinintterm u" by auto
from "2.prems" have nov0as: "\<forall>u\<in>set as. novar0I u" by auto
from "2.hyps" linas nov0as have nov0alls: "\<forall>u\<in>set (all_sums (j, as)). novar0I u" by simp
from nov0alls nov0ys have
cs: "(\<forall> u\<in> set (?ys@ (all_sums (j,as))). novar0I u)"
by (simp only: sym[OF list_all_iff]) auto
have "all_sums(j,a#as) = ?ys@(all_sums(j,as))"
by simp
then
have "?case = (\<forall> x\<in> set (?ys@ (all_sums (j,as))). novar0I x)"
by auto
with cs show ?case by blast
qed
(* correctness theorem for all_sums*)
lemma all_sums_ex:
"(\<exists> j\<in> {1..d}. \<exists> b\<in> (set xs). P (lin_add(b,Cst j))) =
(\<exists> x\<in> set (all_sums (d,xs)). P x)"
proof(induct d xs rule: all_sums.induct)
case (1 a) show ?case by simp
next
case (2 a y ys)
have "(\<exists> x\<in> set (map (\<lambda>x. lin_add (y,(Cst x))) (iupto(1,a))) . P x) =
(\<exists> j\<in> set (iupto(1,a)). P (lin_add(y,Cst j)))"
by auto
also have "\<dots> = (\<exists> j\<in> {1..a}. P (lin_add(y,Cst j)))"
by (simp only : iupto_set)
finally
have dsj1:"(\<exists>j\<in>{1..a}. P (lin_add (y, Cst j))) = (\<exists>x\<in>set (map (\<lambda>x. lin_add (y, Cst x)) (iupto (1, a))). P x)" by simp
from prems have "(\<exists> j\<in> {1..a}. \<exists> b\<in> (set (y#ys)). P (lin_add(b,Cst j))) =
((\<exists> j\<in> {1..a}. P (lin_add(y,Cst j))) \<or> (\<exists> j\<in> {1..a}. \<exists> b \<in> set ys. P (lin_add(b,Cst j))))" by auto
also
have " \<dots> = ((\<exists> j\<in> {1..a}. P (lin_add(y,Cst j))) \<or> (\<exists> x\<in> set (all_sums(a, ys)). P x))" using prems by simp
also have "\<dots> = ((\<exists>x\<in>set (map (\<lambda>x. lin_add (y, Cst x)) (iupto (1, a))). P x) \<or> (\<exists>x\<in>set (all_sums (a, ys)). P x))" using dsj1 by simp
also have "\<dots> = (\<exists> x\<in> (set (map (\<lambda>x. lin_add (y, Cst x)) (iupto (1, a)))) \<union> (set (all_sums(a, ys))). P x)" by blast
finally show ?case by simp
qed
(* explode_minf (p,B) assumes that p is unified and B = bset p, it computes the rhs of cooper_mi_eq*)
consts explode_minf :: "(QF \<times> intterm list) \<Rightarrow> QF"
recdef explode_minf "measure size"
"explode_minf (q,B) =
(let d = divlcm q;
pm = minusinf q;
dj1 = explode_disj ((map Cst (iupto (1, d))),pm)
in (case dj1 of
T \<Rightarrow> T
| F \<Rightarrow> explode_disj (all_sums (d,B),q)
| _ \<Rightarrow> (let dj2 = explode_disj (all_sums (d,B),q)
in ( case dj2 of
T \<Rightarrow> T
| F \<Rightarrow> dj1
| _ \<Rightarrow> Or dj1 dj2))))"
(* The result of the rhs of cooper's theorem doese not depend on Var 0*)
lemma explode_minf_novar0:
assumes unifp : "isunified p"
and bst: "set (bset p) = set B"
shows "novar0 (explode_minf (p,B))"
proof-
let ?d = "divlcm p"
let ?pm = "minusinf p"
let ?dj1 = "explode_disj (map Cst (iupto(1,?d)),?pm)"
have qfpm: "isqfree ?pm" using unified_islinform[OF unifp] minusinf_qfree by simp
have dpos: "?d >0" using unified_islinform[OF unifp] divlcm_pos by simp
have "\<forall> x\<in> set (map Cst (iupto(1,?d))). novar0I x" by auto
then have dj1_nov0: "novar0 ?dj1" using qfpm explode_disj_novar0 by simp
let ?dj2 = "explode_disj (all_sums (?d,B),p)"
have
bstlin: "\<forall>b\<in>set B. islinintterm b"
using bset_lin[OF unifp] bst
by simp
have bstnov0: "\<forall>b\<in>set B. novar0I b"
using bst bset_novar0[OF unifp] by simp
have allsnov0: "\<forall>x\<in>set (all_sums(?d,B)). novar0I x "
by (simp add:all_sums_novar0[OF bstnov0 bstlin] )
then have dj2_nov0: "novar0 ?dj2"
using explode_disj_novar0 unified_isqfree[OF unifp] bst by simp
have "?dj1 = T \<or> ?dj1 = F \<or> (?dj1 \<noteq> T \<and> ?dj1 \<noteq> F)" by auto
moreover
{ assume "?dj1 = T" then have ?thesis by simp }
moreover
{ assume "?dj1 = F" then have ?thesis using bst dj2_nov0 by (simp add: Let_def)}
moreover
{
assume dj1nFT:"?dj1 \<noteq> T \<and> ?dj1 \<noteq> F"
have "?dj2 = T \<or> ?dj2 = F \<or> (?dj2 \<noteq> T \<and> ?dj2 \<noteq> F)" by auto
moreover
{ assume "?dj2 = T" then have ?thesis by (cases ?dj1) simp_all }
moreover
{ assume "?dj2 = F" then have ?thesis using dj1_nov0 bst
by (cases ?dj1) (simp_all add: Let_def)}
moreover
{
assume dj2_nTF:"?dj2 \<noteq> T \<and> ?dj2 \<noteq> F"
let ?res = "\<lambda>f. \<lambda>g. (case f of T \<Rightarrow> T | F \<Rightarrow> g
| _ \<Rightarrow> (case g of T \<Rightarrow> T| F \<Rightarrow> f| _ \<Rightarrow> Or f g))"
have expth: "explode_minf (p,B) = ?res ?dj1 ?dj2"
by (simp add: Let_def del: iupto.simps split del: split_if
cong del: QF.weak_case_cong)
then have ?thesis
using prems or_case_novar0 [OF dj1nFT dj2_nTF dj1_nov0 dj2_nov0]
by (simp add: Let_def del: iupto.simps cong del: QF.weak_case_cong)
}
ultimately have ?thesis by blast
}
ultimately show ?thesis by blast
qed
(* explode_minf computes the rhs of cooper's thm*)
lemma explode_minf_corr:
assumes unifp : "isunified p"
and bst: "set (bset p) = set B"
shows "(\<exists> x . qinterp (x#ats) p) = (qinterp (a#ats) (explode_minf (p,B)))"
(is "(\<exists> x. ?P x) = (?EXP a p)")
proof-
let ?d = "divlcm p"
let ?pm = "minusinf p"
let ?dj1 = "explode_disj (map Cst (iupto(1,?d)),?pm)"
have qfpm: "isqfree ?pm" using unified_islinform[OF unifp] minusinf_qfree by simp
have nnfp: "isnnf p" by (rule unified_isnnf[OF unifp])
have "(\<exists>j\<in>{1..?d}. qinterp (j # ats) (minusinf p))
= (\<exists>j\<in> set (iupto(1,?d)). qinterp (j#ats) (minusinf p))"
(is "(\<exists> j\<in> {1..?d}. ?QM j) = \<dots>")
by (simp add: sym[OF iupto_set] )
also
have "\<dots> =(\<exists>j\<in> set (iupto(1,?d)). qinterp ((I_intterm (a#ats) (Cst j))#ats) (minusinf p))"
by simp
also have
"\<dots> = (\<exists>j\<in> set (map Cst (iupto(1,?d))). qinterp ((I_intterm (a#ats) j)#ats) (minusinf p))" by simp
also have
"\<dots> =
(\<exists>j\<in> set (map Cst (iupto(1,?d))). qinterp (a#ats) (subst_p j (minusinf p)))"
by (simp add: subst_p_corr[OF qfpm])
finally have dj1_thm:
"(\<exists> j\<in> {1..?d}. ?QM j) = (qinterp (a#ats) ?dj1)"
by (simp only: explode_disj_corr[OF qfpm])
let ?dj2 = "explode_disj (all_sums (?d,B),p)"
have
bstlin: "\<forall>b\<in>set B. islinintterm b"
using bst by (simp add: bset_lin[OF unifp])
have bstnov0: "\<forall>b\<in>set B. novar0I b"
using bst by (simp add: bset_novar0[OF unifp])
have allsnov0: "\<forall>x\<in>set (all_sums(?d,B)). novar0I x "
by (simp add:all_sums_novar0[OF bstnov0 bstlin] )
have "(\<exists> j\<in> {1..?d}. \<exists> b\<in> set B. ?P (I_intterm (a#ats) b + j)) =
(\<exists> j\<in> {1..?d}. \<exists> b\<in> set B. ?P (I_intterm (a#ats) (lin_add(b,Cst j))))"
using bst by (auto simp add: lin_add_corr bset_lin[OF unifp])
also have "\<dots> = (\<exists> x \<in> set (all_sums (?d, B)). ?P (I_intterm (a#ats) x))"
by (simp add: all_sums_ex[where P="\<lambda> t. ?P (I_intterm (a#ats) t)"])
finally
have "(\<exists> j\<in> {1..?d}. \<exists> b\<in> set B. ?P (I_intterm (a#ats) b + j)) =
(\<exists> x \<in> set (all_sums (?d, B)). qinterp (a#ats) (subst_p x p))"
using allsnov0 prems linform_isqfree unified_islinform[OF unifp]
by (simp add: all_sums_ex subst_p_corr)
also have "\<dots> = (qinterp (a#ats) ?dj2)"
using linform_isqfree unified_islinform[OF unifp]
by (simp add: explode_disj_corr)
finally have dj2th:
"(\<exists> j\<in> {1..?d}. \<exists> b\<in> set B. ?P (I_intterm (a#ats) b + j)) =
(qinterp (a#ats) ?dj2)" by simp
let ?result = "\<lambda>f. \<lambda>g.
(case f of
T \<Rightarrow> T
| F \<Rightarrow> g
| _ \<Rightarrow> (case g of
T \<Rightarrow> T
| F \<Rightarrow> f
| _ \<Rightarrow> Or f g))"
have "?EXP a p = qinterp (a#ats) (?result ?dj1 ?dj2)"
by (simp only: explode_minf.simps Let_def)
also
have "\<dots> = (qinterp (a#ats) ?dj1 \<or> qinterp (a#ats) ?dj2)"
by (rule eval_Or_cases[where f="?dj1" and g="?dj2" and a="a" and ats="ats"])
also
have "\<dots> = ((\<exists> j\<in> {1..?d}. ?QM j) \<or>
(\<exists> j\<in> {1..?d}. \<exists> b\<in> set B. ?P (I_intterm (a#ats) b + j)))"
by (simp add: dj1_thm dj2th)
also
have "\<dots> = (\<exists> x. ?P x)"
using bst sym[OF cooper_mi_eq[OF unifp]] by simp
finally show ?thesis by simp
qed
lemma explode_minf_corr2:
assumes unifp : "isunified p"
and bst: "set (bset p) = set B"
shows "(qinterp ats (QEx p)) = (qinterp ats (decrvars(explode_minf (p,B))))"
(is "?P = (?Qe p)")
proof-
have "?P = (\<exists>x. qinterp (x#ats) p)" by simp
also have "\<dots> = (qinterp (a # ats) (explode_minf (p,B)))"
using unifp bst explode_minf_corr by simp
finally have ex: "?P = (qinterp (a # ats) (explode_minf (p,B)))" .
have nv0: "novar0 (explode_minf (p,B))"
by (rule explode_minf_novar0[OF unifp])
show ?thesis
using qinterp_novar0[OF nv0] ex by simp
qed
(* An implementation of cooper's method for both plus/minus/infinity *)
(* unify the formula *)
definition unify:: "QF \<Rightarrow> (QF \<times> intterm list)"
"unify p =
(let q = unitycoeff p;
B = list_set(bset q);
A = list_set (aset q)
in
if (length B \<le> length A)
then (q,B)
else (mirror q, map lin_neg A))"
(* unify behaves like unitycoeff *)
lemma unify_ex:
assumes linp: "islinform p"
shows "qinterp ats (QEx p) = qinterp ats (QEx (fst (unify p)))"
proof-
have "length (list_set(bset (unitycoeff p))) \<le> length (list_set (aset (unitycoeff p))) \<or> length (list_set(bset (unitycoeff p))) > length (list_set (aset (unitycoeff p)))" by arith
moreover
{
assume "length (list_set(bset (unitycoeff p))) \<le> length (list_set (aset (unitycoeff p)))"
then have "fst (unify p) = unitycoeff p" using unify_def by (simp add: Let_def)
then have ?thesis using unitycoeff_corr[OF linp]
by simp
}
moreover
{
assume "length (list_set(bset (unitycoeff p))) > length (list_set (aset (unitycoeff p)))"
then have unif: "fst(unify p) = mirror (unitycoeff p)"
using unify_def by (simp add: Let_def)
let ?q ="unitycoeff p"
have unifq: "isunified ?q" by(rule unitycoeff_unified[OF linp])
have linq: "islinform ?q" by (rule unified_islinform[OF unifq])
have "qinterp ats (QEx ?q) = qinterp ats (QEx (mirror ?q))"
by (rule mirror_ex2[OF unifq])
moreover have "qinterp ats (QEx p) = qinterp ats (QEx ?q)"
using unitycoeff_corr linp by simp
ultimately have ?thesis using prems unif by simp
}
ultimately show ?thesis by blast
qed
(* unify's result is a unified formula *)
lemma unify_unified:
assumes linp: "islinform p"
shows "isunified (fst (unify p))"
using linp unitycoeff_unified mirror_unified unify_def unified_islinform
by (auto simp add: Let_def)
(* unify preserves quantifier-freeness*)
lemma unify_qfree:
assumes linp: "islinform p"
shows "isqfree (fst(unify p))"
using linp unify_unified unified_isqfree by simp
lemma unify_bst:
assumes linp: " islinform p"
and unif: "unify p = (q,B)"
shows "set B = set (bset q)"
proof-
let ?q = "unitycoeff p"
let ?a = "aset ?q"
let ?b = "bset ?q"
let ?la = "list_set ?a"
let ?lb = "list_set ?b"
have " length ?lb \<le> length ?la \<or> length ?lb > length ?la" by arith
moreover
{
assume "length ?lb \<le> length ?la"
then
have "unify p = (?q,?lb)"using unify_def prems by (simp add: Let_def)
then
have ?thesis using prems by (simp add: sym[OF list_set_set])
}
moreover
{ assume "length ?lb > length ?la"
have r: "unify p = (mirror ?q,map lin_neg ?la)"using unify_def prems by (simp add: Let_def)
have lin: "\<forall> x\<in> set (bset (mirror ?q)). islinintterm x"
using bset_lin mirror_unified unitycoeff_unified[OF linp] by auto
with r prems aset_eq_bset_mirror lin_neg_idemp unitycoeff_unified linp
have "set B = set (map lin_neg (map lin_neg (bset (mirror (unitycoeff p)))))"
by (simp add: sym[OF list_set_set])
also have "\<dots> = set (map (\<lambda>x. lin_neg (lin_neg x)) (bset (mirror (unitycoeff p))))"
by auto
also have "\<dots> = set (bset (mirror (unitycoeff p)))"
using lin lin_neg_idemp by (auto simp add: map_idI)
finally
have ?thesis using r prems aset_eq_bset_mirror lin_neg_idemp unitycoeff_unified linp
by (simp add: sym[OF list_set_set])}
ultimately show ?thesis by blast
qed
lemma explode_minf_unify_novar0:
assumes linp: "islinform p"
shows "novar0 (explode_minf (unify p))"
proof-
have "\<exists> q B. unify p = (q,B)" by simp
then obtain "q" "B" where qB_def: "unify p = (q,B)" by blast
have unifq: "isunified q" using unify_unified[OF linp] qB_def by simp
have bst: "set B = set (bset q)" using unify_bst linp qB_def by simp
from unifq bst explode_minf_novar0 show ?thesis
using qB_def by simp
qed
lemma explode_minf_unify_corr2:
assumes linp: "islinform p"
shows "qinterp ats (QEx p) = qinterp ats (decrvars(explode_minf(unify p)))"
proof-
have "\<exists> q B. unify p = (q,B)" by simp
then obtain "q" "B" where qB_def: "unify p = (q,B)" by blast
have unifq: "isunified q" using unify_unified[OF linp] qB_def by simp
have bst: "set (bset q) = set B" using unify_bst linp qB_def by simp
from explode_minf_corr2[OF unifq bst] unify_ex[OF linp] show ?thesis
using qB_def by simp
qed
(* An implementation of cooper's method *)
definition
cooper:: "QF \<Rightarrow> QF option"
"cooper p = lift_un (\<lambda>q. decrvars(explode_minf (unify q))) (linform (nnf p))"
(* cooper eliminates quantifiers *)
lemma cooper_qfree: "(\<And> q q'. \<lbrakk>isqfree q ; cooper q = Some q'\<rbrakk> \<Longrightarrow> isqfree q')"
proof-
fix "q" "q'"
assume qfq: "isqfree q"
and qeq: "cooper q = Some q'"
from qeq have "\<exists>p. linform (nnf q) = Some p"
by (cases "linform (nnf q)") (simp_all add: cooper_def)
then obtain "p" where p_def: "linform (nnf q) = Some p" by blast
have linp: "islinform p" using p_def linform_lin nnf_isnnf qfq
by auto
have nnfq: "isnnf (nnf q)" using nnf_isnnf qfq by simp
then have nnfp: "isnnf p" using linform_nnf[OF nnfq] p_def by auto
have qfp: "isqfree p" using linp linform_isqfree by simp
have "cooper q = Some (decrvars(explode_minf (unify p)))" using p_def
by (simp add: cooper_def del: explode_minf.simps)
then have "q' = decrvars (explode_minf (unify p))" using qeq by simp
with linp qfp nnfp unify_unified unify_qfree unified_islinform
show "isqfree q'"
using novar0_qfree explode_minf_unify_novar0 decrvars_qfree
by simp
qed
(* cooper preserves semantics *)
lemma cooper_corr: "(\<And> q q' ats. \<lbrakk>isqfree q ; cooper q = Some q'\<rbrakk> \<Longrightarrow> (qinterp ats (QEx q)) = (qinterp ats q'))" (is "\<And> q q' ats. \<lbrakk> _ ; _ \<rbrakk> \<Longrightarrow> (?P ats (QEx q) = ?P ats q')")
proof-
fix "q" "q'" "ats"
assume qfq: "isqfree q"
and qeq: "cooper q = Some q'"
from qeq have "\<exists>p. linform (nnf q) = Some p"
by (cases "linform (nnf q)") (simp_all add: cooper_def)
then obtain "p" where p_def: "linform (nnf q) = Some p" by blast
have linp: "islinform p" using p_def linform_lin nnf_isnnf qfq by auto
have qfp: "isqfree p" using linp linform_isqfree by simp
have nnfq: "isnnf (nnf q)" using nnf_isnnf qfq by simp
then have nnfp: "isnnf p" using linform_nnf[OF nnfq] p_def by auto
have "\<forall> ats. ?P ats q = ?P ats (nnf q)" using nnf_corr qfq by auto
then have qeqp: "\<forall> ats. ?P ats q = ?P ats p"
using linform_corr p_def nnf_isnnf qfq
by auto
have "cooper q = Some (decrvars (explode_minf (unify p)))" using p_def
by (simp add: cooper_def del: explode_minf.simps)
then have decr: "q' = decrvars(explode_minf (unify p))" using qeq by simp
have eqq:"?P ats (QEx q) = ?P ats (QEx p)" using qeqp by auto
with decr explode_minf_unify_corr2 unified_islinform unify_unified linp
show "?P ats (QEx q) = ?P ats q'" by simp
qed
(* A decision procedure for Presburger Arithmetics *)
definition
pa:: "QF \<Rightarrow> QF option"
"pa p \<equiv> lift_un psimpl (qelim(cooper, p))"
lemma psimpl_qfree: "isqfree p \<Longrightarrow> isqfree (psimpl p)"
apply(induct p rule: isqfree.induct)
apply(auto simp add: Let_def)
apply (simp_all cong del: QF.weak_case_cong add: Let_def)
apply (case_tac "psimpl p", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl p", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl p", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl p", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl q", auto)
apply (case_tac "psimpl p", auto)
apply (case_tac "lift_bin (\<lambda>x y. lin_add (x, lin_neg y), linearize y,
linearize z)", auto)
apply (case_tac "a",auto)
apply (case_tac "lift_bin (\<lambda>x y. lin_add (x, lin_neg y), linearize ac,
linearize ad)", auto)
apply (case_tac "a",auto)
apply (case_tac "ae", auto)
apply (case_tac "linearize af", auto)
by (case_tac "a", auto)
(* pa eliminates quantifiers *)
theorem pa_qfree: "\<And> p'. pa p = Some p' \<Longrightarrow> isqfree p'"
proof(simp only: pa_def)
fix "p'"
assume qep: "lift_un psimpl (qelim (cooper, p)) = Some p'"
then have "\<exists> q. qelim (cooper, p) = Some q"
by (cases "qelim(cooper, p)") auto
then obtain "q" where q_def: "qelim (cooper, p) = Some q" by blast
have "\<And>q q'. \<lbrakk>isqfree q; cooper q = Some q'\<rbrakk> \<Longrightarrow> isqfree q'" using cooper_qfree by blast
with q_def
have "isqfree q" using qelim_qfree by blast
then have "isqfree (psimpl q)" using psimpl_qfree
by auto
then show "isqfree p'"
using prems
by simp
qed
(* pa preserves semantics *)
theorem pa_corr:
"\<And> p'. pa p = Some p' \<Longrightarrow> (qinterp ats p = qinterp ats p')"
proof(simp only: pa_def)
fix "p'"
assume qep: "lift_un psimpl (qelim(cooper, p)) = Some p'"
then have "\<exists> q. qelim (cooper, p) = Some q"
by (cases "qelim(cooper, p)") auto
then obtain "q" where q_def: "qelim (cooper, p) = Some q" by blast
have cp1:"\<And>q q' ats.
\<lbrakk>isqfree q; cooper q = Some q'\<rbrakk> \<Longrightarrow> qinterp ats (QEx q) = qinterp ats q'"
using cooper_corr by blast
moreover have cp2: "\<And>q q'. \<lbrakk>isqfree q; cooper q = Some q'\<rbrakk> \<Longrightarrow> isqfree q'"
using cooper_qfree by blast
ultimately have "qinterp ats p = qinterp ats q" using qelim_corr qep psimpl_corr q_def
by blast
then have "qinterp ats p = qinterp ats (psimpl q)" using psimpl_corr q_def
by auto
then show "qinterp ats p = qinterp ats p'" using prems
by simp
qed
lemma [code]: "linearize (Mult i j) =
(case linearize i of
None \<Rightarrow> None
| Some li \<Rightarrow> (case li of
Cst b \<Rightarrow> (case linearize j of
None \<Rightarrow> None
| (Some lj) \<Rightarrow> Some (lin_mul(b,lj)))
| _ \<Rightarrow> (case linearize j of
None \<Rightarrow> None
| (Some lj) \<Rightarrow> (case lj of
Cst b \<Rightarrow> Some (lin_mul (b,li))
| _ \<Rightarrow> None))))"
by simp
lemma [code]: "psimpl (And p q) =
(let p'= psimpl p
in (case p' of
F \<Rightarrow> F
|T \<Rightarrow> psimpl q
| _ \<Rightarrow> let q' = psimpl q
in (case q' of
F \<Rightarrow> F
| T \<Rightarrow> p'
| _ \<Rightarrow> (And p' q'))))"
by simp
lemma [code]: "psimpl (Or p q) =
(let p'= psimpl p
in (case p' of
T \<Rightarrow> T
| F \<Rightarrow> psimpl q
| _ \<Rightarrow> let q' = psimpl q
in (case q' of
T \<Rightarrow> T
| F \<Rightarrow> p'
| _ \<Rightarrow> (Or p' q'))))"
by simp
lemma [code]: "psimpl (Imp p q) =
(let p'= psimpl p
in (case p' of
F \<Rightarrow> T
|T \<Rightarrow> psimpl q
| NOT p1 \<Rightarrow> let q' = psimpl q
in (case q' of
F \<Rightarrow> p1
| T \<Rightarrow> T
| _ \<Rightarrow> (Or p1 q'))
| _ \<Rightarrow> let q' = psimpl q
in (case q' of
F \<Rightarrow> NOT p'
| T \<Rightarrow> T
| _ \<Rightarrow> (Imp p' q'))))"
by simp
declare zdvd_iff_zmod_eq_0 [code]
(*
generate_code ("presburger.ML") test = "pa"
use "rcooper.ML"
oracle rpresburger_oracle ("term") = RCooper.rpresburger_oracle
use "rpresbtac.ML"
setup RPresburger.setup
*)
end