Hi,
I could not believe that recdef could not be replaced by fun, so here is
the patch that removes usages of recdef from Decision_Procs. The proof
rules that come out of the function package are fine (one just needs a
few split_format (complete) attributes in a few places).
I'm not sure if this is something for the repository though, since it
has a factor of >2 impact on the build-time:
recdef: Finished HOL-Decision_Procs (0:03:53 elapsed time, 0:13:26 cpu
time, factor 3.45)
fun : Finished HOL-Decision_Procs (0:08:24 elapsed time, 0:28:10 cpu
time, factor 3.35)
On the other hand 8 minutes is still not much. The longest fun
invocation (numadd in MIR) takes about 2 minutes, other are all below 20
seconds.
Dmitriy
On 07.06.2015 07:18, Amine Chaieb wrote:
I remember trying to convert Cooper's as well as other Decision proc's
recdefs to fun, also with the help of Alex but gave up at some point.
I think the killer at the time was rather the induction principle and
not the simp rules. The one derived by recdef really fits the
definition and "spirit" of development. Also runtime at the time was
not acceptable. I also remember havin the runtime problem with fun vs.
primrec (so we left those there too).
Context: Deep embedding of datatype + normal form on this data type
+ set of recursive functions on syntax preserving normal form. The
normal Form has conditions on nested patterns --> introduce new
constructor for these common nested patterns in normal form.
We had combinatorial explosion due to the depth of the patterns (which
is the main reason to introduce special constructors in the datatype,
to reduce deep patterns).
The induction priciples with recdef really fitted, i.e. induct auto
with spice did the job for lemmas you do not expect to spend time
thinking as a software developer.
One could argue that one should introduce a new data type for
normalized syntactic elements and perform such computations as needed.
I dismissed this idea and did not explore it, since it comes with a
high price. Perhaps there are better ways to do the formalization.
Amine.
On 06/06/2015 08:37 PM, Tobias Nipkow wrote:
On 06/06/2015 20:11, Larry Paulson wrote:
Pattern matching is a convenience, and can always be eliminated
manually. Is there really no reasonable way to re-express the
definitions in Cooper.thy?
You can always turn all patterns of the lhs into cases on the rhs and
derive the individual equations as lemmas. You also need to derive an
induction principle. I would rather keep recdef than do all that by
hand.
Tobias
Larry
On 6 Jun 2015, at 16:11, Florian Haftmann
<florian.haftm...@informatik.tu-muenchen.de> wrote:
The reason for the continued existence of recdef is that function can
cause a combinatorial explosion the way it compiles pattern
matches. I
just tried Cooper.thy and changing one of the recdefs to function
makes
Isabelle go blue (purple) in the face until one gives up. Hardware
alone
will not solve that one.
Now one could argue that since we need recdef, we should also keep
the
special variant defer_recdef, but if nobody speaks up for it, we
don't
have a proof that we really need it and it should go.
At the time of their writing the recdef examples in (nowadays)
src/HOL/Decision_Procs were the power applications of their times.
Since then power applications have grown bigger and bigger and
fun/function have been used widespread. It seems strange to me
that no
application since then had never hit the same concrete wall again.
So are there any experience reports that the combinatorial
explosion in
pattern matching in fun/function had to be worked around somehow?
Or do
we have to conclude that the pattern complexity of the applications in
src/HOL/Decision_Procs is indeed domain-specific?
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
# HG changeset patch
# User traytel
# Date 1433658664 -7200
# So Jun 07 08:31:04 2015 +0200
# Node ID 03ef7232e0f060ed68756b902bd55ec9a51ed9b7
# Parent 392402362c3e01d9556b59674ce2d4f38903bd0b
get rid of recdef from Decision_Procs
diff -r 392402362c3e -r 03ef7232e0f0 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy Fr Jun 05 09:15:37 2015 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy So Jun 07 08:31:04 2015 +0200
@@ -6,7 +6,6 @@
imports
Complex_Main
"~~/src/HOL/Library/Code_Target_Numeral"
- "~~/src/HOL/Library/Old_Recdef"
begin
(* Periodicity of dvd *)
@@ -82,32 +81,32 @@
| "Ifm bbs bs (Closed n) \<longleftrightarrow> bbs!n"
| "Ifm bbs bs (NClosed n) \<longleftrightarrow> \<not> bbs!n"
-consts prep :: "fm \<Rightarrow> fm"
-recdef prep "measure fmsize"
+function (sequential) prep :: "fm \<Rightarrow> fm" where
"prep (E T) = T"
- "prep (E F) = F"
- "prep (E (Or p q)) = Or (prep (E p)) (prep (E q))"
- "prep (E (Imp p q)) = Or (prep (E (NOT p))) (prep (E q))"
- "prep (E (Iff p q)) = Or (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))"
- "prep (E (NOT (And p q))) = Or (prep (E (NOT p))) (prep (E(NOT q)))"
- "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))"
- "prep (E (NOT (Iff p q))) = Or (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))"
- "prep (E p) = E (prep p)"
- "prep (A (And p q)) = And (prep (A p)) (prep (A q))"
- "prep (A p) = prep (NOT (E (NOT p)))"
- "prep (NOT (NOT p)) = prep p"
- "prep (NOT (And p q)) = Or (prep (NOT p)) (prep (NOT q))"
- "prep (NOT (A p)) = prep (E (NOT p))"
- "prep (NOT (Or p q)) = And (prep (NOT p)) (prep (NOT q))"
- "prep (NOT (Imp p q)) = And (prep p) (prep (NOT q))"
- "prep (NOT (Iff p q)) = Or (prep (And p (NOT q))) (prep (And (NOT p) q))"
- "prep (NOT p) = NOT (prep p)"
- "prep (Or p q) = Or (prep p) (prep q)"
- "prep (And p q) = And (prep p) (prep q)"
- "prep (Imp p q) = prep (Or (NOT p) q)"
- "prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))"
- "prep p = p"
- (hints simp add: fmsize_pos)
+| "prep (E F) = F"
+| "prep (E (Or p q)) = Or (prep (E p)) (prep (E q))"
+| "prep (E (Imp p q)) = Or (prep (E (NOT p))) (prep (E q))"
+| "prep (E (Iff p q)) = Or (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))"
+| "prep (E (NOT (And p q))) = Or (prep (E (NOT p))) (prep (E(NOT q)))"
+| "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))"
+| "prep (E (NOT (Iff p q))) = Or (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))"
+| "prep (E p) = E (prep p)"
+| "prep (A (And p q)) = And (prep (A p)) (prep (A q))"
+| "prep (A p) = prep (NOT (E (NOT p)))"
+| "prep (NOT (NOT p)) = prep p"
+| "prep (NOT (And p q)) = Or (prep (NOT p)) (prep (NOT q))"
+| "prep (NOT (A p)) = prep (E (NOT p))"
+| "prep (NOT (Or p q)) = And (prep (NOT p)) (prep (NOT q))"
+| "prep (NOT (Imp p q)) = And (prep p) (prep (NOT q))"
+| "prep (NOT (Iff p q)) = Or (prep (And p (NOT q))) (prep (And (NOT p) q))"
+| "prep (NOT p) = NOT (prep p)"
+| "prep (Or p q) = Or (prep p) (prep q)"
+| "prep (And p q) = And (prep p) (prep q)"
+| "prep (Imp p q) = prep (Or (NOT p) q)"
+| "prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))"
+| "prep p = p"
+ by pat_completeness auto
+termination by (relation "measure fmsize") (auto simp: fmsize_pos)
lemma prep: "Ifm bbs bs (prep p) = Ifm bbs bs p"
by (induct p arbitrary: bs rule: prep.induct) auto
@@ -422,20 +421,22 @@
definition lex_bnd :: "num \<Rightarrow> num \<Rightarrow> bool"
where "lex_bnd t s = lex_ns (bnds t) (bnds s)"
-consts numadd:: "num \<times> num \<Rightarrow> num"
-recdef numadd "measure (\<lambda>(t, s). num_size t + num_size s)"
+function (sequential) numadd:: "num \<times> num \<Rightarrow> num" where
"numadd (CN n1 c1 r1, CN n2 c2 r2) =
(if n1 = n2 then
let c = c1 + c2
in if c = 0 then numadd (r1, r2) else CN n1 c (numadd (r1, r2))
else if n1 \<le> n2 then CN n1 c1 (numadd (r1, Add (Mul c2 (Bound n2)) r2))
else CN n2 c2 (numadd (Add (Mul c1 (Bound n1)) r1, r2)))"
- "numadd (CN n1 c1 r1, t) = CN n1 c1 (numadd (r1, t))"
- "numadd (t, CN n2 c2 r2) = CN n2 c2 (numadd (t, r2))"
- "numadd (C b1, C b2) = C (b1 + b2)"
- "numadd (a, b) = Add a b"
+| "numadd (CN n1 c1 r1, t) = CN n1 c1 (numadd (r1, t))"
+| "numadd (t, CN n2 c2 r2) = CN n2 c2 (numadd (t, r2))"
+| "numadd (C b1, C b2) = C (b1 + b2)"
+| "numadd (a, b) = Add a b"
+ by pat_completeness auto
+termination by size_change
-(*function (sequential)
+(*
+function (sequential)
numadd :: "num \<Rightarrow> num \<Rightarrow> num"
where
"numadd (Add (Mul c1 (Bound n1)) r1) (Add (Mul c2 (Bound n2)) r2) =
@@ -455,7 +456,7 @@
apply pat_completeness apply auto*)
lemma numadd: "Inum bs (numadd (t,s)) = Inum bs (Add t s)"
- apply (induct t s rule: numadd.induct)
+ apply (induct t s rule: numadd.induct[split_format (complete)])
apply (simp_all add: Let_def)
apply (case_tac "c1 + c2 = 0")
apply (case_tac "n1 \<le> n2")
@@ -466,7 +467,7 @@
done
lemma numadd_nb: "numbound0 t \<Longrightarrow> numbound0 s \<Longrightarrow> numbound0 (numadd (t, s))"
- by (induct t s rule: numadd.induct) (auto simp add: Let_def)
+ by (induct t s rule: numadd.induct[split_format (complete)]) (auto simp add: Let_def)
fun nummul :: "int \<Rightarrow> num \<Rightarrow> num"
where
@@ -1021,91 +1022,91 @@
by simp
qed
-consts iszlfm :: "fm \<Rightarrow> bool" -- {* Linearity test for fm *}
-recdef iszlfm "measure size"
+fun iszlfm :: "fm \<Rightarrow> bool" where -- {* Linearity test for fm *}
"iszlfm (And p q) \<longleftrightarrow> iszlfm p \<and> iszlfm q"
- "iszlfm (Or p q) \<longleftrightarrow> iszlfm p \<and> iszlfm q"
- "iszlfm (Eq (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
- "iszlfm (NEq (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
- "iszlfm (Lt (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
- "iszlfm (Le (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
- "iszlfm (Gt (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
- "iszlfm (Ge (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
- "iszlfm (Dvd i (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> i > 0 \<and> numbound0 e"
- "iszlfm (NDvd i (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> i > 0 \<and> numbound0 e"
- "iszlfm p \<longleftrightarrow> isatom p \<and> bound0 p"
+| "iszlfm (Or p q) \<longleftrightarrow> iszlfm p \<and> iszlfm q"
+| "iszlfm (Eq (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
+| "iszlfm (NEq (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
+| "iszlfm (Lt (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
+| "iszlfm (Le (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
+| "iszlfm (Gt (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
+| "iszlfm (Ge (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
+| "iszlfm (Dvd i (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> i > 0 \<and> numbound0 e"
+| "iszlfm (NDvd i (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> i > 0 \<and> numbound0 e"
+| "iszlfm p \<longleftrightarrow> isatom p \<and> bound0 p"
lemma zlin_qfree: "iszlfm p \<Longrightarrow> qfree p"
by (induct p rule: iszlfm.induct) auto
-consts zlfm :: "fm \<Rightarrow> fm" -- {* Linearity transformation for fm *}
-recdef zlfm "measure fmsize"
+function (sequential) zlfm :: "fm \<Rightarrow> fm" where -- {* Linearity transformation for fm *}
"zlfm (And p q) = And (zlfm p) (zlfm q)"
- "zlfm (Or p q) = Or (zlfm p) (zlfm q)"
- "zlfm (Imp p q) = Or (zlfm (NOT p)) (zlfm q)"
- "zlfm (Iff p q) = Or (And (zlfm p) (zlfm q)) (And (zlfm (NOT p)) (zlfm (NOT q)))"
- "zlfm (Lt a) =
+| "zlfm (Or p q) = Or (zlfm p) (zlfm q)"
+| "zlfm (Imp p q) = Or (zlfm (NOT p)) (zlfm q)"
+| "zlfm (Iff p q) = Or (And (zlfm p) (zlfm q)) (And (zlfm (NOT p)) (zlfm (NOT q)))"
+| "zlfm (Lt a) =
(let (c, r) = zsplit0 a in
if c = 0 then Lt r else
if c > 0 then (Lt (CN 0 c r))
else Gt (CN 0 (- c) (Neg r)))"
- "zlfm (Le a) =
+| "zlfm (Le a) =
(let (c, r) = zsplit0 a in
if c = 0 then Le r
else if c > 0 then Le (CN 0 c r)
else Ge (CN 0 (- c) (Neg r)))"
- "zlfm (Gt a) =
+| "zlfm (Gt a) =
(let (c, r) = zsplit0 a in
if c = 0 then Gt r else
if c > 0 then Gt (CN 0 c r)
else Lt (CN 0 (- c) (Neg r)))"
- "zlfm (Ge a) =
+| "zlfm (Ge a) =
(let (c, r) = zsplit0 a in
if c = 0 then Ge r
else if c > 0 then Ge (CN 0 c r)
else Le (CN 0 (- c) (Neg r)))"
- "zlfm (Eq a) =
+| "zlfm (Eq a) =
(let (c, r) = zsplit0 a in
if c = 0 then Eq r
else if c > 0 then Eq (CN 0 c r)
else Eq (CN 0 (- c) (Neg r)))"
- "zlfm (NEq a) =
+| "zlfm (NEq a) =
(let (c, r) = zsplit0 a in
if c = 0 then NEq r
else if c > 0 then NEq (CN 0 c r)
else NEq (CN 0 (- c) (Neg r)))"
- "zlfm (Dvd i a) =
+| "zlfm (Dvd i a) =
(if i = 0 then zlfm (Eq a)
else
let (c, r) = zsplit0 a in
if c = 0 then Dvd (abs i) r
else if c > 0 then Dvd (abs i) (CN 0 c r)
else Dvd (abs i) (CN 0 (- c) (Neg r)))"
- "zlfm (NDvd i a) =
+| "zlfm (NDvd i a) =
(if i = 0 then zlfm (NEq a)
else
let (c, r) = zsplit0 a in
if c = 0 then NDvd (abs i) r
else if c > 0 then NDvd (abs i) (CN 0 c r)
else NDvd (abs i) (CN 0 (- c) (Neg r)))"
- "zlfm (NOT (And p q)) = Or (zlfm (NOT p)) (zlfm (NOT q))"
- "zlfm (NOT (Or p q)) = And (zlfm (NOT p)) (zlfm (NOT q))"
- "zlfm (NOT (Imp p q)) = And (zlfm p) (zlfm (NOT q))"
- "zlfm (NOT (Iff p q)) = Or (And(zlfm p) (zlfm(NOT q))) (And (zlfm(NOT p)) (zlfm q))"
- "zlfm (NOT (NOT p)) = zlfm p"
- "zlfm (NOT T) = F"
- "zlfm (NOT F) = T"
- "zlfm (NOT (Lt a)) = zlfm (Ge a)"
- "zlfm (NOT (Le a)) = zlfm (Gt a)"
- "zlfm (NOT (Gt a)) = zlfm (Le a)"
- "zlfm (NOT (Ge a)) = zlfm (Lt a)"
- "zlfm (NOT (Eq a)) = zlfm (NEq a)"
- "zlfm (NOT (NEq a)) = zlfm (Eq a)"
- "zlfm (NOT (Dvd i a)) = zlfm (NDvd i a)"
- "zlfm (NOT (NDvd i a)) = zlfm (Dvd i a)"
- "zlfm (NOT (Closed P)) = NClosed P"
- "zlfm (NOT (NClosed P)) = Closed P"
- "zlfm p = p" (hints simp add: fmsize_pos)
+| "zlfm (NOT (And p q)) = Or (zlfm (NOT p)) (zlfm (NOT q))"
+| "zlfm (NOT (Or p q)) = And (zlfm (NOT p)) (zlfm (NOT q))"
+| "zlfm (NOT (Imp p q)) = And (zlfm p) (zlfm (NOT q))"
+| "zlfm (NOT (Iff p q)) = Or (And(zlfm p) (zlfm(NOT q))) (And (zlfm(NOT p)) (zlfm q))"
+| "zlfm (NOT (NOT p)) = zlfm p"
+| "zlfm (NOT T) = F"
+| "zlfm (NOT F) = T"
+| "zlfm (NOT (Lt a)) = zlfm (Ge a)"
+| "zlfm (NOT (Le a)) = zlfm (Gt a)"
+| "zlfm (NOT (Gt a)) = zlfm (Le a)"
+| "zlfm (NOT (Ge a)) = zlfm (Lt a)"
+| "zlfm (NOT (Eq a)) = zlfm (NEq a)"
+| "zlfm (NOT (NEq a)) = zlfm (Eq a)"
+| "zlfm (NOT (Dvd i a)) = zlfm (NDvd i a)"
+| "zlfm (NOT (NDvd i a)) = zlfm (Dvd i a)"
+| "zlfm (NOT (Closed P)) = NClosed P"
+| "zlfm (NOT (NClosed P)) = Closed P"
+| "zlfm p = p"
+ by pat_completeness auto
+termination by (relation "measure fmsize") auto
lemma zlfm_I:
assumes qfp: "qfree p"
@@ -1316,48 +1317,44 @@
ultimately show ?case by blast
qed auto
-consts minusinf :: "fm \<Rightarrow> fm" -- {* Virtual substitution of @{text "-\<infinity>"} *}
-recdef minusinf "measure size"
+fun minusinf :: "fm \<Rightarrow> fm" where -- {* Virtual substitution of @{text "-\<infinity>"} *}
"minusinf (And p q) = And (minusinf p) (minusinf q)"
- "minusinf (Or p q) = Or (minusinf p) (minusinf q)"
- "minusinf (Eq (CN 0 c e)) = F"
- "minusinf (NEq (CN 0 c e)) = T"
- "minusinf (Lt (CN 0 c e)) = T"
- "minusinf (Le (CN 0 c e)) = T"
- "minusinf (Gt (CN 0 c e)) = F"
- "minusinf (Ge (CN 0 c e)) = F"
- "minusinf p = p"
+| "minusinf (Or p q) = Or (minusinf p) (minusinf q)"
+| "minusinf (Eq (CN 0 c e)) = F"
+| "minusinf (NEq (CN 0 c e)) = T"
+| "minusinf (Lt (CN 0 c e)) = T"
+| "minusinf (Le (CN 0 c e)) = T"
+| "minusinf (Gt (CN 0 c e)) = F"
+| "minusinf (Ge (CN 0 c e)) = F"
+| "minusinf p = p"
lemma minusinf_qfree: "qfree p \<Longrightarrow> qfree (minusinf p)"
by (induct p rule: minusinf.induct) auto
-consts plusinf :: "fm \<Rightarrow> fm" -- {* Virtual substitution of @{text "+\<infinity>"} *}
-recdef plusinf "measure size"
+fun plusinf :: "fm \<Rightarrow> fm" where -- {* Virtual substitution of @{text "+\<infinity>"} *}
"plusinf (And p q) = And (plusinf p) (plusinf q)"
- "plusinf (Or p q) = Or (plusinf p) (plusinf q)"
- "plusinf (Eq (CN 0 c e)) = F"
- "plusinf (NEq (CN 0 c e)) = T"
- "plusinf (Lt (CN 0 c e)) = F"
- "plusinf (Le (CN 0 c e)) = F"
- "plusinf (Gt (CN 0 c e)) = T"
- "plusinf (Ge (CN 0 c e)) = T"
- "plusinf p = p"
+| "plusinf (Or p q) = Or (plusinf p) (plusinf q)"
+| "plusinf (Eq (CN 0 c e)) = F"
+| "plusinf (NEq (CN 0 c e)) = T"
+| "plusinf (Lt (CN 0 c e)) = F"
+| "plusinf (Le (CN 0 c e)) = F"
+| "plusinf (Gt (CN 0 c e)) = T"
+| "plusinf (Ge (CN 0 c e)) = T"
+| "plusinf p = p"
-consts \<delta> :: "fm \<Rightarrow> int" -- {* Compute @{text "lcm {d| N\<^sup>? Dvd c*x+t \<in> p}"} *}
-recdef \<delta> "measure size"
+fun \<delta> :: "fm \<Rightarrow> int" where -- {* Compute @{text "lcm {d| N\<^sup>? Dvd c*x+t \<in> p}"} *}
"\<delta> (And p q) = lcm (\<delta> p) (\<delta> q)"
- "\<delta> (Or p q) = lcm (\<delta> p) (\<delta> q)"
- "\<delta> (Dvd i (CN 0 c e)) = i"
- "\<delta> (NDvd i (CN 0 c e)) = i"
- "\<delta> p = 1"
+| "\<delta> (Or p q) = lcm (\<delta> p) (\<delta> q)"
+| "\<delta> (Dvd i (CN 0 c e)) = i"
+| "\<delta> (NDvd i (CN 0 c e)) = i"
+| "\<delta> p = 1"
-consts d_\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool" -- {* check if a given l divides all the ds above *}
-recdef d_\<delta> "measure size"
+fun d_\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool" where -- {* check if a given l divides all the ds above *}
"d_\<delta> (And p q) = (\<lambda>d. d_\<delta> p d \<and> d_\<delta> q d)"
- "d_\<delta> (Or p q) = (\<lambda>d. d_\<delta> p d \<and> d_\<delta> q d)"
- "d_\<delta> (Dvd i (CN 0 c e)) = (\<lambda>d. i dvd d)"
- "d_\<delta> (NDvd i (CN 0 c e)) = (\<lambda>d. i dvd d)"
- "d_\<delta> p = (\<lambda>d. True)"
+| "d_\<delta> (Or p q) = (\<lambda>d. d_\<delta> p d \<and> d_\<delta> q d)"
+| "d_\<delta> (Dvd i (CN 0 c e)) = (\<lambda>d. i dvd d)"
+| "d_\<delta> (NDvd i (CN 0 c e)) = (\<lambda>d. i dvd d)"
+| "d_\<delta> p = (\<lambda>d. True)"
lemma delta_mono:
assumes lin: "iszlfm p"
@@ -1387,7 +1384,7 @@
have d1: "\<delta> p dvd \<delta> (And p q)"
using 1 by simp
then have th: "d_\<delta> p ?d"
- using delta_mono 1(2,3) by (simp only: iszlfm.simps)
+ using delta_mono 1(1,3) by (simp only: iszlfm.simps)
have "\<delta> q dvd \<delta> (And p q)"
using 1 by simp
then have th': "d_\<delta> q ?d"
@@ -1412,85 +1409,79 @@
qed simp_all
-consts a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" -- {* adjust the coefficients of a formula *}
-recdef a_\<beta> "measure size"
+fun a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" where -- {* adjust the coefficients of a formula *}
"a_\<beta> (And p q) = (\<lambda>k. And (a_\<beta> p k) (a_\<beta> q k))"
- "a_\<beta> (Or p q) = (\<lambda>k. Or (a_\<beta> p k) (a_\<beta> q k))"
- "a_\<beta> (Eq (CN 0 c e)) = (\<lambda>k. Eq (CN 0 1 (Mul (k div c) e)))"
- "a_\<beta> (NEq (CN 0 c e)) = (\<lambda>k. NEq (CN 0 1 (Mul (k div c) e)))"
- "a_\<beta> (Lt (CN 0 c e)) = (\<lambda>k. Lt (CN 0 1 (Mul (k div c) e)))"
- "a_\<beta> (Le (CN 0 c e)) = (\<lambda>k. Le (CN 0 1 (Mul (k div c) e)))"
- "a_\<beta> (Gt (CN 0 c e)) = (\<lambda>k. Gt (CN 0 1 (Mul (k div c) e)))"
- "a_\<beta> (Ge (CN 0 c e)) = (\<lambda>k. Ge (CN 0 1 (Mul (k div c) e)))"
- "a_\<beta> (Dvd i (CN 0 c e)) =(\<lambda>k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
- "a_\<beta> (NDvd i (CN 0 c e))=(\<lambda>k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
- "a_\<beta> p = (\<lambda>k. p)"
+| "a_\<beta> (Or p q) = (\<lambda>k. Or (a_\<beta> p k) (a_\<beta> q k))"
+| "a_\<beta> (Eq (CN 0 c e)) = (\<lambda>k. Eq (CN 0 1 (Mul (k div c) e)))"
+| "a_\<beta> (NEq (CN 0 c e)) = (\<lambda>k. NEq (CN 0 1 (Mul (k div c) e)))"
+| "a_\<beta> (Lt (CN 0 c e)) = (\<lambda>k. Lt (CN 0 1 (Mul (k div c) e)))"
+| "a_\<beta> (Le (CN 0 c e)) = (\<lambda>k. Le (CN 0 1 (Mul (k div c) e)))"
+| "a_\<beta> (Gt (CN 0 c e)) = (\<lambda>k. Gt (CN 0 1 (Mul (k div c) e)))"
+| "a_\<beta> (Ge (CN 0 c e)) = (\<lambda>k. Ge (CN 0 1 (Mul (k div c) e)))"
+| "a_\<beta> (Dvd i (CN 0 c e)) =(\<lambda>k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
+| "a_\<beta> (NDvd i (CN 0 c e))=(\<lambda>k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
+| "a_\<beta> p = (\<lambda>k. p)"
-consts d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" -- {* test if all coeffs c of c divide a given l *}
-recdef d_\<beta> "measure size"
+fun d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" where -- {* test if all coeffs c of c divide a given l *}
"d_\<beta> (And p q) = (\<lambda>k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
- "d_\<beta> (Or p q) = (\<lambda>k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
- "d_\<beta> (Eq (CN 0 c e)) = (\<lambda>k. c dvd k)"
- "d_\<beta> (NEq (CN 0 c e)) = (\<lambda>k. c dvd k)"
- "d_\<beta> (Lt (CN 0 c e)) = (\<lambda>k. c dvd k)"
- "d_\<beta> (Le (CN 0 c e)) = (\<lambda>k. c dvd k)"
- "d_\<beta> (Gt (CN 0 c e)) = (\<lambda>k. c dvd k)"
- "d_\<beta> (Ge (CN 0 c e)) = (\<lambda>k. c dvd k)"
- "d_\<beta> (Dvd i (CN 0 c e)) =(\<lambda>k. c dvd k)"
- "d_\<beta> (NDvd i (CN 0 c e))=(\<lambda>k. c dvd k)"
- "d_\<beta> p = (\<lambda>k. True)"
+| "d_\<beta> (Or p q) = (\<lambda>k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
+| "d_\<beta> (Eq (CN 0 c e)) = (\<lambda>k. c dvd k)"
+| "d_\<beta> (NEq (CN 0 c e)) = (\<lambda>k. c dvd k)"
+| "d_\<beta> (Lt (CN 0 c e)) = (\<lambda>k. c dvd k)"
+| "d_\<beta> (Le (CN 0 c e)) = (\<lambda>k. c dvd k)"
+| "d_\<beta> (Gt (CN 0 c e)) = (\<lambda>k. c dvd k)"
+| "d_\<beta> (Ge (CN 0 c e)) = (\<lambda>k. c dvd k)"
+| "d_\<beta> (Dvd i (CN 0 c e)) =(\<lambda>k. c dvd k)"
+| "d_\<beta> (NDvd i (CN 0 c e))=(\<lambda>k. c dvd k)"
+| "d_\<beta> p = (\<lambda>k. True)"
-consts \<zeta> :: "fm \<Rightarrow> int" -- {* computes the lcm of all coefficients of x *}
-recdef \<zeta> "measure size"
+fun \<zeta> :: "fm \<Rightarrow> int" where -- {* computes the lcm of all coefficients of x *}
"\<zeta> (And p q) = lcm (\<zeta> p) (\<zeta> q)"
- "\<zeta> (Or p q) = lcm (\<zeta> p) (\<zeta> q)"
- "\<zeta> (Eq (CN 0 c e)) = c"
- "\<zeta> (NEq (CN 0 c e)) = c"
- "\<zeta> (Lt (CN 0 c e)) = c"
- "\<zeta> (Le (CN 0 c e)) = c"
- "\<zeta> (Gt (CN 0 c e)) = c"
- "\<zeta> (Ge (CN 0 c e)) = c"
- "\<zeta> (Dvd i (CN 0 c e)) = c"
- "\<zeta> (NDvd i (CN 0 c e))= c"
- "\<zeta> p = 1"
+| "\<zeta> (Or p q) = lcm (\<zeta> p) (\<zeta> q)"
+| "\<zeta> (Eq (CN 0 c e)) = c"
+| "\<zeta> (NEq (CN 0 c e)) = c"
+| "\<zeta> (Lt (CN 0 c e)) = c"
+| "\<zeta> (Le (CN 0 c e)) = c"
+| "\<zeta> (Gt (CN 0 c e)) = c"
+| "\<zeta> (Ge (CN 0 c e)) = c"
+| "\<zeta> (Dvd i (CN 0 c e)) = c"
+| "\<zeta> (NDvd i (CN 0 c e))= c"
+| "\<zeta> p = 1"
-consts \<beta> :: "fm \<Rightarrow> num list"
-recdef \<beta> "measure size"
+fun \<beta> :: "fm \<Rightarrow> num list" where
"\<beta> (And p q) = (\<beta> p @ \<beta> q)"
- "\<beta> (Or p q) = (\<beta> p @ \<beta> q)"
- "\<beta> (Eq (CN 0 c e)) = [Sub (C (- 1)) e]"
- "\<beta> (NEq (CN 0 c e)) = [Neg e]"
- "\<beta> (Lt (CN 0 c e)) = []"
- "\<beta> (Le (CN 0 c e)) = []"
- "\<beta> (Gt (CN 0 c e)) = [Neg e]"
- "\<beta> (Ge (CN 0 c e)) = [Sub (C (- 1)) e]"
- "\<beta> p = []"
+| "\<beta> (Or p q) = (\<beta> p @ \<beta> q)"
+| "\<beta> (Eq (CN 0 c e)) = [Sub (C (- 1)) e]"
+| "\<beta> (NEq (CN 0 c e)) = [Neg e]"
+| "\<beta> (Lt (CN 0 c e)) = []"
+| "\<beta> (Le (CN 0 c e)) = []"
+| "\<beta> (Gt (CN 0 c e)) = [Neg e]"
+| "\<beta> (Ge (CN 0 c e)) = [Sub (C (- 1)) e]"
+| "\<beta> p = []"
-consts \<alpha> :: "fm \<Rightarrow> num list"
-recdef \<alpha> "measure size"
+fun \<alpha> :: "fm \<Rightarrow> num list" where
"\<alpha> (And p q) = \<alpha> p @ \<alpha> q"
- "\<alpha> (Or p q) = \<alpha> p @ \<alpha> q"
- "\<alpha> (Eq (CN 0 c e)) = [Add (C (- 1)) e]"
- "\<alpha> (NEq (CN 0 c e)) = [e]"
- "\<alpha> (Lt (CN 0 c e)) = [e]"
- "\<alpha> (Le (CN 0 c e)) = [Add (C (- 1)) e]"
- "\<alpha> (Gt (CN 0 c e)) = []"
- "\<alpha> (Ge (CN 0 c e)) = []"
- "\<alpha> p = []"
+| "\<alpha> (Or p q) = \<alpha> p @ \<alpha> q"
+| "\<alpha> (Eq (CN 0 c e)) = [Add (C (- 1)) e]"
+| "\<alpha> (NEq (CN 0 c e)) = [e]"
+| "\<alpha> (Lt (CN 0 c e)) = [e]"
+| "\<alpha> (Le (CN 0 c e)) = [Add (C (- 1)) e]"
+| "\<alpha> (Gt (CN 0 c e)) = []"
+| "\<alpha> (Ge (CN 0 c e)) = []"
+| "\<alpha> p = []"
-consts mirror :: "fm \<Rightarrow> fm"
-recdef mirror "measure size"
+fun mirror :: "fm \<Rightarrow> fm" where
"mirror (And p q) = And (mirror p) (mirror q)"
- "mirror (Or p q) = Or (mirror p) (mirror q)"
- "mirror (Eq (CN 0 c e)) = Eq (CN 0 c (Neg e))"
- "mirror (NEq (CN 0 c e)) = NEq (CN 0 c (Neg e))"
- "mirror (Lt (CN 0 c e)) = Gt (CN 0 c (Neg e))"
- "mirror (Le (CN 0 c e)) = Ge (CN 0 c (Neg e))"
- "mirror (Gt (CN 0 c e)) = Lt (CN 0 c (Neg e))"
- "mirror (Ge (CN 0 c e)) = Le (CN 0 c (Neg e))"
- "mirror (Dvd i (CN 0 c e)) = Dvd i (CN 0 c (Neg e))"
- "mirror (NDvd i (CN 0 c e)) = NDvd i (CN 0 c (Neg e))"
- "mirror p = p"
+| "mirror (Or p q) = Or (mirror p) (mirror q)"
+| "mirror (Eq (CN 0 c e)) = Eq (CN 0 c (Neg e))"
+| "mirror (NEq (CN 0 c e)) = NEq (CN 0 c (Neg e))"
+| "mirror (Lt (CN 0 c e)) = Gt (CN 0 c (Neg e))"
+| "mirror (Le (CN 0 c e)) = Ge (CN 0 c (Neg e))"
+| "mirror (Gt (CN 0 c e)) = Lt (CN 0 c (Neg e))"
+| "mirror (Ge (CN 0 c e)) = Le (CN 0 c (Neg e))"
+| "mirror (Dvd i (CN 0 c e)) = Dvd i (CN 0 c (Neg e))"
+| "mirror (NDvd i (CN 0 c e)) = NDvd i (CN 0 c (Neg e))"
+| "mirror p = p"
text {* Lemmas for the correctness of @{text "\<sigma>_\<rho>"} *}
diff -r 392402362c3e -r 03ef7232e0f0 src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy Fr Jun 05 09:15:37 2015 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy So Jun 07 08:31:04 2015 +0200
@@ -4,7 +4,7 @@
theory Ferrack
imports Complex_Main Dense_Linear_Order DP_Library
- "~~/src/HOL/Library/Code_Target_Numeral" "~~/src/HOL/Library/Old_Recdef"
+ "~~/src/HOL/Library/Code_Target_Numeral"
begin
section {* Quantifier elimination for @{text "\<real> (0, 1, +, <)"} *}
@@ -550,29 +550,26 @@
lemma reducecoeff_numbound0: "numbound0 t \<Longrightarrow> numbound0 (reducecoeff t)"
using reducecoeffh_numbound0 by (simp add: reducecoeff_def Let_def)
-consts
- numadd:: "num \<times> num \<Rightarrow> num"
-
-recdef numadd "measure (\<lambda> (t,s). size t + size s)"
+fun numadd:: "num \<times> num \<Rightarrow> num" where
"numadd (CN n1 c1 r1,CN n2 c2 r2) =
(if n1=n2 then
(let c = c1 + c2
in (if c=0 then numadd(r1,r2) else CN n1 c (numadd (r1,r2))))
else if n1 \<le> n2 then (CN n1 c1 (numadd (r1,CN n2 c2 r2)))
else (CN n2 c2 (numadd (CN n1 c1 r1,r2))))"
- "numadd (CN n1 c1 r1,t) = CN n1 c1 (numadd (r1, t))"
- "numadd (t,CN n2 c2 r2) = CN n2 c2 (numadd (t,r2))"
- "numadd (C b1, C b2) = C (b1+b2)"
- "numadd (a,b) = Add a b"
+| "numadd (CN n1 c1 r1,t) = CN n1 c1 (numadd (r1, t))"
+| "numadd (t,CN n2 c2 r2) = CN n2 c2 (numadd (t,r2))"
+| "numadd (C b1, C b2) = C (b1+b2)"
+| "numadd (a,b) = Add a b"
lemma numadd[simp]: "Inum bs (numadd (t,s)) = Inum bs (Add t s)"
-apply (induct t s rule: numadd.induct, simp_all add: Let_def)
+apply (induct t s rule: numadd.induct[split_format (complete)], simp_all add: Let_def)
apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
apply (case_tac "n1 = n2", simp_all add: algebra_simps)
by (simp only: distrib_right[symmetric],simp)
lemma numadd_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
-by (induct t s rule: numadd.induct, auto simp add: Let_def)
+by (induct t s rule: numadd.induct[split_format (complete)], auto simp add: Let_def)
fun nummul:: "num \<Rightarrow> int \<Rightarrow> num" where
"nummul (C j) = (\<lambda> i. C (i*j))"
@@ -625,7 +622,7 @@
| "nozerocoeff t = True"
lemma numadd_nz : "nozerocoeff a \<Longrightarrow> nozerocoeff b \<Longrightarrow> nozerocoeff (numadd (a,b))"
-by (induct a b rule: numadd.induct,auto simp add: Let_def)
+by (induct a b rule: numadd.induct[split_format (complete)],auto simp add: Let_def)
lemma nummul_nz : "\<And> i. i\<noteq>0 \<Longrightarrow> nozerocoeff a \<Longrightarrow> nozerocoeff (nummul a i)"
by (induct a rule: nummul.induct,auto simp add: Let_def numadd_nz)
@@ -826,32 +823,33 @@
apply (case_tac "simpnum a", auto)+
done
-consts prep :: "fm \<Rightarrow> fm"
-recdef prep "measure fmsize"
+function (sequential) prep :: "fm \<Rightarrow> fm" where
"prep (E T) = T"
- "prep (E F) = F"
- "prep (E (Or p q)) = disj (prep (E p)) (prep (E q))"
- "prep (E (Imp p q)) = disj (prep (E (NOT p))) (prep (E q))"
- "prep (E (Iff p q)) = disj (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))"
- "prep (E (NOT (And p q))) = disj (prep (E (NOT p))) (prep (E(NOT q)))"
- "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))"
- "prep (E (NOT (Iff p q))) = disj (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))"
- "prep (E p) = E (prep p)"
- "prep (A (And p q)) = conj (prep (A p)) (prep (A q))"
- "prep (A p) = prep (NOT (E (NOT p)))"
- "prep (NOT (NOT p)) = prep p"
- "prep (NOT (And p q)) = disj (prep (NOT p)) (prep (NOT q))"
- "prep (NOT (A p)) = prep (E (NOT p))"
- "prep (NOT (Or p q)) = conj (prep (NOT p)) (prep (NOT q))"
- "prep (NOT (Imp p q)) = conj (prep p) (prep (NOT q))"
- "prep (NOT (Iff p q)) = disj (prep (And p (NOT q))) (prep (And (NOT p) q))"
- "prep (NOT p) = not (prep p)"
- "prep (Or p q) = disj (prep p) (prep q)"
- "prep (And p q) = conj (prep p) (prep q)"
- "prep (Imp p q) = prep (Or (NOT p) q)"
- "prep (Iff p q) = disj (prep (And p q)) (prep (And (NOT p) (NOT q)))"
- "prep p = p"
-(hints simp add: fmsize_pos)
+| "prep (E F) = F"
+| "prep (E (Or p q)) = disj (prep (E p)) (prep (E q))"
+| "prep (E (Imp p q)) = disj (prep (E (NOT p))) (prep (E q))"
+| "prep (E (Iff p q)) = disj (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))"
+| "prep (E (NOT (And p q))) = disj (prep (E (NOT p))) (prep (E(NOT q)))"
+| "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))"
+| "prep (E (NOT (Iff p q))) = disj (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))"
+| "prep (E p) = E (prep p)"
+| "prep (A (And p q)) = conj (prep (A p)) (prep (A q))"
+| "prep (A p) = prep (NOT (E (NOT p)))"
+| "prep (NOT (NOT p)) = prep p"
+| "prep (NOT (And p q)) = disj (prep (NOT p)) (prep (NOT q))"
+| "prep (NOT (A p)) = prep (E (NOT p))"
+| "prep (NOT (Or p q)) = conj (prep (NOT p)) (prep (NOT q))"
+| "prep (NOT (Imp p q)) = conj (prep p) (prep (NOT q))"
+| "prep (NOT (Iff p q)) = disj (prep (And p (NOT q))) (prep (And (NOT p) q))"
+| "prep (NOT p) = not (prep p)"
+| "prep (Or p q) = disj (prep p) (prep q)"
+| "prep (And p q) = conj (prep p) (prep q)"
+| "prep (Imp p q) = prep (Or (NOT p) q)"
+| "prep (Iff p q) = disj (prep (And p q)) (prep (And (NOT p) (NOT q)))"
+| "prep p = p"
+ by pat_completeness auto
+termination by (relation "measure fmsize") (auto simp: fmsize_pos)
+
lemma prep: "\<And> bs. Ifm bs (prep p) = Ifm bs p"
by (induct p rule: prep.induct) auto
@@ -1005,32 +1003,33 @@
lemma disj_lin: "isrlfm p \<Longrightarrow> isrlfm q \<Longrightarrow> isrlfm (disj p q)"
by (auto simp add: disj_def)
-consts rlfm :: "fm \<Rightarrow> fm"
-recdef rlfm "measure fmsize"
+function (sequential) rlfm :: "fm \<Rightarrow> fm" where
"rlfm (And p q) = conj (rlfm p) (rlfm q)"
- "rlfm (Or p q) = disj (rlfm p) (rlfm q)"
- "rlfm (Imp p q) = disj (rlfm (NOT p)) (rlfm q)"
- "rlfm (Iff p q) = disj (conj (rlfm p) (rlfm q)) (conj (rlfm (NOT p)) (rlfm (NOT q)))"
- "rlfm (Lt a) = split lt (rsplit0 a)"
- "rlfm (Le a) = split le (rsplit0 a)"
- "rlfm (Gt a) = split gt (rsplit0 a)"
- "rlfm (Ge a) = split ge (rsplit0 a)"
- "rlfm (Eq a) = split eq (rsplit0 a)"
- "rlfm (NEq a) = split neq (rsplit0 a)"
- "rlfm (NOT (And p q)) = disj (rlfm (NOT p)) (rlfm (NOT q))"
- "rlfm (NOT (Or p q)) = conj (rlfm (NOT p)) (rlfm (NOT q))"
- "rlfm (NOT (Imp p q)) = conj (rlfm p) (rlfm (NOT q))"
- "rlfm (NOT (Iff p q)) = disj (conj(rlfm p) (rlfm(NOT q))) (conj(rlfm(NOT p)) (rlfm q))"
- "rlfm (NOT (NOT p)) = rlfm p"
- "rlfm (NOT T) = F"
- "rlfm (NOT F) = T"
- "rlfm (NOT (Lt a)) = rlfm (Ge a)"
- "rlfm (NOT (Le a)) = rlfm (Gt a)"
- "rlfm (NOT (Gt a)) = rlfm (Le a)"
- "rlfm (NOT (Ge a)) = rlfm (Lt a)"
- "rlfm (NOT (Eq a)) = rlfm (NEq a)"
- "rlfm (NOT (NEq a)) = rlfm (Eq a)"
- "rlfm p = p" (hints simp add: fmsize_pos)
+| "rlfm (Or p q) = disj (rlfm p) (rlfm q)"
+| "rlfm (Imp p q) = disj (rlfm (NOT p)) (rlfm q)"
+| "rlfm (Iff p q) = disj (conj (rlfm p) (rlfm q)) (conj (rlfm (NOT p)) (rlfm (NOT q)))"
+| "rlfm (Lt a) = split lt (rsplit0 a)"
+| "rlfm (Le a) = split le (rsplit0 a)"
+| "rlfm (Gt a) = split gt (rsplit0 a)"
+| "rlfm (Ge a) = split ge (rsplit0 a)"
+| "rlfm (Eq a) = split eq (rsplit0 a)"
+| "rlfm (NEq a) = split neq (rsplit0 a)"
+| "rlfm (NOT (And p q)) = disj (rlfm (NOT p)) (rlfm (NOT q))"
+| "rlfm (NOT (Or p q)) = conj (rlfm (NOT p)) (rlfm (NOT q))"
+| "rlfm (NOT (Imp p q)) = conj (rlfm p) (rlfm (NOT q))"
+| "rlfm (NOT (Iff p q)) = disj (conj(rlfm p) (rlfm(NOT q))) (conj(rlfm(NOT p)) (rlfm q))"
+| "rlfm (NOT (NOT p)) = rlfm p"
+| "rlfm (NOT T) = F"
+| "rlfm (NOT F) = T"
+| "rlfm (NOT (Lt a)) = rlfm (Ge a)"
+| "rlfm (NOT (Le a)) = rlfm (Gt a)"
+| "rlfm (NOT (Gt a)) = rlfm (Le a)"
+| "rlfm (NOT (Ge a)) = rlfm (Lt a)"
+| "rlfm (NOT (Eq a)) = rlfm (NEq a)"
+| "rlfm (NOT (NEq a)) = rlfm (Eq a)"
+| "rlfm p = p"
+ by pat_completeness auto
+termination by (relation "measure fmsize") auto
lemma rlfm_I:
assumes qfp: "qfree p"
@@ -1297,29 +1296,27 @@
ultimately show ?thesis using z_def by auto
qed
-consts
- uset:: "fm \<Rightarrow> (num \<times> int) list"
- usubst :: "fm \<Rightarrow> (num \<times> int) \<Rightarrow> fm "
-recdef uset "measure size"
+fun uset:: "fm \<Rightarrow> (num \<times> int) list" where
"uset (And p q) = (uset p @ uset q)"
- "uset (Or p q) = (uset p @ uset q)"
- "uset (Eq (CN 0 c e)) = [(Neg e,c)]"
- "uset (NEq (CN 0 c e)) = [(Neg e,c)]"
- "uset (Lt (CN 0 c e)) = [(Neg e,c)]"
- "uset (Le (CN 0 c e)) = [(Neg e,c)]"
- "uset (Gt (CN 0 c e)) = [(Neg e,c)]"
- "uset (Ge (CN 0 c e)) = [(Neg e,c)]"
- "uset p = []"
-recdef usubst "measure size"
+| "uset (Or p q) = (uset p @ uset q)"
+| "uset (Eq (CN 0 c e)) = [(Neg e,c)]"
+| "uset (NEq (CN 0 c e)) = [(Neg e,c)]"
+| "uset (Lt (CN 0 c e)) = [(Neg e,c)]"
+| "uset (Le (CN 0 c e)) = [(Neg e,c)]"
+| "uset (Gt (CN 0 c e)) = [(Neg e,c)]"
+| "uset (Ge (CN 0 c e)) = [(Neg e,c)]"
+| "uset p = []"
+
+fun usubst :: "fm \<Rightarrow> (num \<times> int) \<Rightarrow> fm" where
"usubst (And p q) = (\<lambda> (t,n). And (usubst p (t,n)) (usubst q (t,n)))"
- "usubst (Or p q) = (\<lambda> (t,n). Or (usubst p (t,n)) (usubst q (t,n)))"
- "usubst (Eq (CN 0 c e)) = (\<lambda> (t,n). Eq (Add (Mul c t) (Mul n e)))"
- "usubst (NEq (CN 0 c e)) = (\<lambda> (t,n). NEq (Add (Mul c t) (Mul n e)))"
- "usubst (Lt (CN 0 c e)) = (\<lambda> (t,n). Lt (Add (Mul c t) (Mul n e)))"
- "usubst (Le (CN 0 c e)) = (\<lambda> (t,n). Le (Add (Mul c t) (Mul n e)))"
- "usubst (Gt (CN 0 c e)) = (\<lambda> (t,n). Gt (Add (Mul c t) (Mul n e)))"
- "usubst (Ge (CN 0 c e)) = (\<lambda> (t,n). Ge (Add (Mul c t) (Mul n e)))"
- "usubst p = (\<lambda> (t,n). p)"
+| "usubst (Or p q) = (\<lambda> (t,n). Or (usubst p (t,n)) (usubst q (t,n)))"
+| "usubst (Eq (CN 0 c e)) = (\<lambda> (t,n). Eq (Add (Mul c t) (Mul n e)))"
+| "usubst (NEq (CN 0 c e)) = (\<lambda> (t,n). NEq (Add (Mul c t) (Mul n e)))"
+| "usubst (Lt (CN 0 c e)) = (\<lambda> (t,n). Lt (Add (Mul c t) (Mul n e)))"
+| "usubst (Le (CN 0 c e)) = (\<lambda> (t,n). Le (Add (Mul c t) (Mul n e)))"
+| "usubst (Gt (CN 0 c e)) = (\<lambda> (t,n). Gt (Add (Mul c t) (Mul n e)))"
+| "usubst (Ge (CN 0 c e)) = (\<lambda> (t,n). Ge (Add (Mul c t) (Mul n e)))"
+| "usubst p = (\<lambda> (t,n). p)"
lemma usubst_I: assumes lp: "isrlfm p"
and np: "real n > 0" and nbt: "numbound0 t"
diff -r 392402362c3e -r 03ef7232e0f0 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy Fr Jun 05 09:15:37 2015 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy So Jun 07 08:31:04 2015 +0200
@@ -4,7 +4,7 @@
theory MIR
imports Complex_Main Dense_Linear_Order DP_Library
- "~~/src/HOL/Library/Code_Target_Numeral" "~~/src/HOL/Library/Old_Recdef"
+ "~~/src/HOL/Library/Code_Target_Numeral"
begin
section {* Quantifier elimination for @{text "\<real> (0, 1, +, floor, <)"} *}
@@ -229,36 +229,36 @@
| "Ifm bs (E p) = (\<exists> x. Ifm (x#bs) p)"
| "Ifm bs (A p) = (\<forall> x. Ifm (x#bs) p)"
-consts prep :: "fm \<Rightarrow> fm"
-recdef prep "measure fmsize"
+function (sequential) prep :: "fm \<Rightarrow> fm" where
"prep (E T) = T"
- "prep (E F) = F"
- "prep (E (Or p q)) = Or (prep (E p)) (prep (E q))"
- "prep (E (Imp p q)) = Or (prep (E (NOT p))) (prep (E q))"
- "prep (E (Iff p q)) = Or (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))"
- "prep (E (NOT (And p q))) = Or (prep (E (NOT p))) (prep (E(NOT q)))"
- "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))"
- "prep (E (NOT (Iff p q))) = Or (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))"
- "prep (E p) = E (prep p)"
- "prep (A (And p q)) = And (prep (A p)) (prep (A q))"
- "prep (A p) = prep (NOT (E (NOT p)))"
- "prep (NOT (NOT p)) = prep p"
- "prep (NOT (And p q)) = Or (prep (NOT p)) (prep (NOT q))"
- "prep (NOT (A p)) = prep (E (NOT p))"
- "prep (NOT (Or p q)) = And (prep (NOT p)) (prep (NOT q))"
- "prep (NOT (Imp p q)) = And (prep p) (prep (NOT q))"
- "prep (NOT (Iff p q)) = Or (prep (And p (NOT q))) (prep (And (NOT p) q))"
- "prep (NOT p) = NOT (prep p)"
- "prep (Or p q) = Or (prep p) (prep q)"
- "prep (And p q) = And (prep p) (prep q)"
- "prep (Imp p q) = prep (Or (NOT p) q)"
- "prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))"
- "prep p = p"
-(hints simp add: fmsize_pos)
+| "prep (E F) = F"
+| "prep (E (Or p q)) = Or (prep (E p)) (prep (E q))"
+| "prep (E (Imp p q)) = Or (prep (E (NOT p))) (prep (E q))"
+| "prep (E (Iff p q)) = Or (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))"
+| "prep (E (NOT (And p q))) = Or (prep (E (NOT p))) (prep (E(NOT q)))"
+| "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))"
+| "prep (E (NOT (Iff p q))) = Or (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))"
+| "prep (E p) = E (prep p)"
+| "prep (A (And p q)) = And (prep (A p)) (prep (A q))"
+| "prep (A p) = prep (NOT (E (NOT p)))"
+| "prep (NOT (NOT p)) = prep p"
+| "prep (NOT (And p q)) = Or (prep (NOT p)) (prep (NOT q))"
+| "prep (NOT (A p)) = prep (E (NOT p))"
+| "prep (NOT (Or p q)) = And (prep (NOT p)) (prep (NOT q))"
+| "prep (NOT (Imp p q)) = And (prep p) (prep (NOT q))"
+| "prep (NOT (Iff p q)) = Or (prep (And p (NOT q))) (prep (And (NOT p) q))"
+| "prep (NOT p) = NOT (prep p)"
+| "prep (Or p q) = Or (prep p) (prep q)"
+| "prep (And p q) = And (prep p) (prep q)"
+| "prep (Imp p q) = prep (Or (NOT p) q)"
+| "prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))"
+| "prep p = p"
+ by pat_completeness auto
+termination by (relation "measure fmsize") (auto simp: fmsize_pos)
+
lemma prep: "\<And> bs. Ifm bs (prep p) = Ifm bs p"
by (induct p rule: prep.induct) auto
-
(* Quantifier freeness *)
fun qfree:: "fm \<Rightarrow> bool" where
"qfree (E p) = False"
@@ -728,28 +728,27 @@
lemma reducecoeff_numbound0: "numbound0 t \<Longrightarrow> numbound0 (reducecoeff t)"
using reducecoeffh_numbound0 by (simp add: reducecoeff_def Let_def)
-consts numadd:: "num \<times> num \<Rightarrow> num"
-recdef numadd "measure (\<lambda> (t,s). size t + size s)"
+fun numadd:: "num \<times> num \<Rightarrow> num" where
"numadd (CN n1 c1 r1,CN n2 c2 r2) =
(if n1=n2 then
(let c = c1 + c2
in (if c=0 then numadd(r1,r2) else CN n1 c (numadd (r1,r2))))
else if n1 \<le> n2 then CN n1 c1 (numadd (r1,CN n2 c2 r2))
else (CN n2 c2 (numadd (CN n1 c1 r1,r2))))"
- "numadd (CN n1 c1 r1,t) = CN n1 c1 (numadd (r1, t))"
- "numadd (t,CN n2 c2 r2) = CN n2 c2 (numadd (t,r2))"
- "numadd (CF c1 t1 r1,CF c2 t2 r2) =
+| "numadd (CN n1 c1 r1,t) = CN n1 c1 (numadd (r1, t))"
+| "numadd (t,CN n2 c2 r2) = CN n2 c2 (numadd (t,r2))"
+| "numadd (CF c1 t1 r1,CF c2 t2 r2) =
(if t1 = t2 then
(let c=c1+c2; s= numadd(r1,r2) in (if c=0 then s else CF c t1 s))
else if lex_bnd t1 t2 then CF c1 t1 (numadd(r1,CF c2 t2 r2))
else CF c2 t2 (numadd(CF c1 t1 r1,r2)))"
- "numadd (CF c1 t1 r1,C c) = CF c1 t1 (numadd (r1, C c))"
- "numadd (C c,CF c1 t1 r1) = CF c1 t1 (numadd (r1, C c))"
- "numadd (C b1, C b2) = C (b1+b2)"
- "numadd (a,b) = Add a b"
+| "numadd (CF c1 t1 r1,C c) = CF c1 t1 (numadd (r1, C c))"
+| "numadd (C c,CF c1 t1 r1) = CF c1 t1 (numadd (r1, C c))"
+| "numadd (C b1, C b2) = C (b1+b2)"
+| "numadd (a,b) = Add a b"
lemma numadd[simp]: "Inum bs (numadd (t,s)) = Inum bs (Add t s)"
-apply (induct t s rule: numadd.induct, simp_all add: Let_def)
+apply (induct t s rule: numadd.induct[split_format (complete)], simp_all add: Let_def)
apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
apply (case_tac "n1 = n2", simp_all add: algebra_simps)
apply (simp only: distrib_right[symmetric])
@@ -761,7 +760,7 @@
done
lemma numadd_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
- by (induct t s rule: numadd.induct) (auto simp add: Let_def)
+ by (induct t s rule: numadd.induct[split_format (complete)]) (auto simp add: Let_def)
fun nummul:: "num \<Rightarrow> int \<Rightarrow> num" where
"nummul (C j) = (\<lambda> i. C (i*j))"
@@ -898,7 +897,7 @@
| "nozerocoeff t = True"
lemma numadd_nz : "nozerocoeff a \<Longrightarrow> nozerocoeff b \<Longrightarrow> nozerocoeff (numadd (a,b))"
- by (induct a b rule: numadd.induct) (auto simp add: Let_def)
+ by (induct a b rule: numadd.induct[split_format (complete)]) (auto simp add: Let_def)
lemma nummul_nz : "\<And> i. i\<noteq>0 \<Longrightarrow> nozerocoeff a \<Longrightarrow> nozerocoeff (nummul a i)"
by (induct a rule: nummul.induct) (auto simp add: Let_def numadd_nz)
@@ -1550,23 +1549,20 @@
with na show ?case by simp
qed
-consts
- iszlfm :: "fm \<Rightarrow> real list \<Rightarrow> bool" (* Linearity test for fm *)
- zlfm :: "fm \<Rightarrow> fm" (* Linearity transformation for fm *)
-recdef iszlfm "measure size"
+fun iszlfm :: "fm \<Rightarrow> real list \<Rightarrow> bool" where (* Linearity test for fm *)
"iszlfm (And p q) = (\<lambda> bs. iszlfm p bs \<and> iszlfm q bs)"
- "iszlfm (Or p q) = (\<lambda> bs. iszlfm p bs \<and> iszlfm q bs)"
- "iszlfm (Eq (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
- "iszlfm (NEq (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
- "iszlfm (Lt (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
- "iszlfm (Le (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
- "iszlfm (Gt (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
- "iszlfm (Ge (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
- "iszlfm (Dvd i (CN 0 c e)) =
+| "iszlfm (Or p q) = (\<lambda> bs. iszlfm p bs \<and> iszlfm q bs)"
+| "iszlfm (Eq (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
+| "iszlfm (NEq (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
+| "iszlfm (Lt (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
+| "iszlfm (Le (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
+| "iszlfm (Gt (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
+| "iszlfm (Ge (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
+| "iszlfm (Dvd i (CN 0 c e)) =
(\<lambda> bs. c>0 \<and> i>0 \<and> numbound0 e \<and> isint e bs)"
- "iszlfm (NDvd i (CN 0 c e))=
+| "iszlfm (NDvd i (CN 0 c e))=
(\<lambda> bs. c>0 \<and> i>0 \<and> numbound0 e \<and> isint e bs)"
- "iszlfm p = (\<lambda> bs. isatom p \<and> (bound0 p))"
+| "iszlfm p = (\<lambda> bs. isatom p \<and> (bound0 p))"
lemma zlin_qfree: "iszlfm p bs \<Longrightarrow> qfree p"
by (induct p rule: iszlfm.induct) auto
@@ -1586,61 +1582,63 @@
lemma disj_zl[simp]: "iszlfm p bs \<Longrightarrow> iszlfm q bs \<Longrightarrow> iszlfm (disj p q) bs"
using disj_def by (cases p,auto)
-recdef zlfm "measure fmsize"
+function (sequential) zlfm :: "fm \<Rightarrow> fm" where (* Linearity transformation for fm *)
"zlfm (And p q) = conj (zlfm p) (zlfm q)"
- "zlfm (Or p q) = disj (zlfm p) (zlfm q)"
- "zlfm (Imp p q) = disj (zlfm (NOT p)) (zlfm q)"
- "zlfm (Iff p q) = disj (conj (zlfm p) (zlfm q)) (conj (zlfm (NOT p)) (zlfm (NOT q)))"
- "zlfm (Lt a) = (let (c,r) = zsplit0 a in
+| "zlfm (Or p q) = disj (zlfm p) (zlfm q)"
+| "zlfm (Imp p q) = disj (zlfm (NOT p)) (zlfm q)"
+| "zlfm (Iff p q) = disj (conj (zlfm p) (zlfm q)) (conj (zlfm (NOT p)) (zlfm (NOT q)))"
+| "zlfm (Lt a) = (let (c,r) = zsplit0 a in
if c=0 then Lt r else
if c>0 then Or (Lt (CN 0 c (Neg (Floor (Neg r))))) (And (Eq (CN 0 c (Neg (Floor (Neg r))))) (Lt (Add (Floor (Neg r)) r)))
else Or (Gt (CN 0 (-c) (Floor(Neg r)))) (And (Eq(CN 0 (-c) (Floor(Neg r)))) (Lt (Add (Floor (Neg r)) r))))"
- "zlfm (Le a) = (let (c,r) = zsplit0 a in
+| "zlfm (Le a) = (let (c,r) = zsplit0 a in
if c=0 then Le r else
if c>0 then Or (Le (CN 0 c (Neg (Floor (Neg r))))) (And (Eq (CN 0 c (Neg (Floor (Neg r))))) (Lt (Add (Floor (Neg r)) r)))
else Or (Ge (CN 0 (-c) (Floor(Neg r)))) (And (Eq(CN 0 (-c) (Floor(Neg r)))) (Lt (Add (Floor (Neg r)) r))))"
- "zlfm (Gt a) = (let (c,r) = zsplit0 a in
+| "zlfm (Gt a) = (let (c,r) = zsplit0 a in
if c=0 then Gt r else
if c>0 then Or (Gt (CN 0 c (Floor r))) (And (Eq (CN 0 c (Floor r))) (Lt (Sub (Floor r) r)))
else Or (Lt (CN 0 (-c) (Neg (Floor r)))) (And (Eq(CN 0 (-c) (Neg (Floor r)))) (Lt (Sub (Floor r) r))))"
- "zlfm (Ge a) = (let (c,r) = zsplit0 a in
+| "zlfm (Ge a) = (let (c,r) = zsplit0 a in
if c=0 then Ge r else
if c>0 then Or (Ge (CN 0 c (Floor r))) (And (Eq (CN 0 c (Floor r))) (Lt (Sub (Floor r) r)))
else Or (Le (CN 0 (-c) (Neg (Floor r)))) (And (Eq(CN 0 (-c) (Neg (Floor r)))) (Lt (Sub (Floor r) r))))"
- "zlfm (Eq a) = (let (c,r) = zsplit0 a in
+| "zlfm (Eq a) = (let (c,r) = zsplit0 a in
if c=0 then Eq r else
if c>0 then (And (Eq (CN 0 c (Neg (Floor (Neg r))))) (Eq (Add (Floor (Neg r)) r)))
else (And (Eq (CN 0 (-c) (Floor (Neg r)))) (Eq (Add (Floor (Neg r)) r))))"
- "zlfm (NEq a) = (let (c,r) = zsplit0 a in
+| "zlfm (NEq a) = (let (c,r) = zsplit0 a in
if c=0 then NEq r else
if c>0 then (Or (NEq (CN 0 c (Neg (Floor (Neg r))))) (NEq (Add (Floor (Neg r)) r)))
else (Or (NEq (CN 0 (-c) (Floor (Neg r)))) (NEq (Add (Floor (Neg r)) r))))"
- "zlfm (Dvd i a) = (if i=0 then zlfm (Eq a)
+| "zlfm (Dvd i a) = (if i=0 then zlfm (Eq a)
else (let (c,r) = zsplit0 a in
if c=0 then Dvd (abs i) r else
if c>0 then And (Eq (Sub (Floor r) r)) (Dvd (abs i) (CN 0 c (Floor r)))
else And (Eq (Sub (Floor r) r)) (Dvd (abs i) (CN 0 (-c) (Neg (Floor r))))))"
- "zlfm (NDvd i a) = (if i=0 then zlfm (NEq a)
+| "zlfm (NDvd i a) = (if i=0 then zlfm (NEq a)
else (let (c,r) = zsplit0 a in
if c=0 then NDvd (abs i) r else
if c>0 then Or (NEq (Sub (Floor r) r)) (NDvd (abs i) (CN 0 c (Floor r)))
else Or (NEq (Sub (Floor r) r)) (NDvd (abs i) (CN 0 (-c) (Neg (Floor r))))))"
- "zlfm (NOT (And p q)) = disj (zlfm (NOT p)) (zlfm (NOT q))"
- "zlfm (NOT (Or p q)) = conj (zlfm (NOT p)) (zlfm (NOT q))"
- "zlfm (NOT (Imp p q)) = conj (zlfm p) (zlfm (NOT q))"
- "zlfm (NOT (Iff p q)) = disj (conj(zlfm p) (zlfm(NOT q))) (conj (zlfm(NOT p)) (zlfm q))"
- "zlfm (NOT (NOT p)) = zlfm p"
- "zlfm (NOT T) = F"
- "zlfm (NOT F) = T"
- "zlfm (NOT (Lt a)) = zlfm (Ge a)"
- "zlfm (NOT (Le a)) = zlfm (Gt a)"
- "zlfm (NOT (Gt a)) = zlfm (Le a)"
- "zlfm (NOT (Ge a)) = zlfm (Lt a)"
- "zlfm (NOT (Eq a)) = zlfm (NEq a)"
- "zlfm (NOT (NEq a)) = zlfm (Eq a)"
- "zlfm (NOT (Dvd i a)) = zlfm (NDvd i a)"
- "zlfm (NOT (NDvd i a)) = zlfm (Dvd i a)"
- "zlfm p = p" (hints simp add: fmsize_pos)
+| "zlfm (NOT (And p q)) = disj (zlfm (NOT p)) (zlfm (NOT q))"
+| "zlfm (NOT (Or p q)) = conj (zlfm (NOT p)) (zlfm (NOT q))"
+| "zlfm (NOT (Imp p q)) = conj (zlfm p) (zlfm (NOT q))"
+| "zlfm (NOT (Iff p q)) = disj (conj(zlfm p) (zlfm(NOT q))) (conj (zlfm(NOT p)) (zlfm q))"
+| "zlfm (NOT (NOT p)) = zlfm p"
+| "zlfm (NOT T) = F"
+| "zlfm (NOT F) = T"
+| "zlfm (NOT (Lt a)) = zlfm (Ge a)"
+| "zlfm (NOT (Le a)) = zlfm (Gt a)"
+| "zlfm (NOT (Gt a)) = zlfm (Le a)"
+| "zlfm (NOT (Ge a)) = zlfm (Lt a)"
+| "zlfm (NOT (Eq a)) = zlfm (NEq a)"
+| "zlfm (NOT (NEq a)) = zlfm (Eq a)"
+| "zlfm (NOT (Dvd i a)) = zlfm (NDvd i a)"
+| "zlfm (NOT (NDvd i a)) = zlfm (Dvd i a)"
+| "zlfm p = p"
+ by pat_completeness auto
+termination by (relation "measure fmsize") auto
lemma split_int_less_real:
"(real (a::int) < b) = (a < floor b \<or> (a = floor b \<and> real (floor b) < b))"
@@ -2255,86 +2253,79 @@
lemma dvd1_eq1: "x >0 \<Longrightarrow> (x::int) dvd 1 = (x = 1)" by auto
-consts
- a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" (* adjusts the coeffitients of a formula *)
- d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* tests if all coeffs c of c divide a given l*)
- \<zeta> :: "fm \<Rightarrow> int" (* computes the lcm of all coefficients of x*)
- \<beta> :: "fm \<Rightarrow> num list"
- \<alpha> :: "fm \<Rightarrow> num list"
-
-recdef a_\<beta> "measure size"
+fun a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" where (* adjusts the coeffitients of a formula *)
"a_\<beta> (And p q) = (\<lambda> k. And (a_\<beta> p k) (a_\<beta> q k))"
- "a_\<beta> (Or p q) = (\<lambda> k. Or (a_\<beta> p k) (a_\<beta> q k))"
- "a_\<beta> (Eq (CN 0 c e)) = (\<lambda> k. Eq (CN 0 1 (Mul (k div c) e)))"
- "a_\<beta> (NEq (CN 0 c e)) = (\<lambda> k. NEq (CN 0 1 (Mul (k div c) e)))"
- "a_\<beta> (Lt (CN 0 c e)) = (\<lambda> k. Lt (CN 0 1 (Mul (k div c) e)))"
- "a_\<beta> (Le (CN 0 c e)) = (\<lambda> k. Le (CN 0 1 (Mul (k div c) e)))"
- "a_\<beta> (Gt (CN 0 c e)) = (\<lambda> k. Gt (CN 0 1 (Mul (k div c) e)))"
- "a_\<beta> (Ge (CN 0 c e)) = (\<lambda> k. Ge (CN 0 1 (Mul (k div c) e)))"
- "a_\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
- "a_\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
- "a_\<beta> p = (\<lambda> k. p)"
-
-recdef d_\<beta> "measure size"
+| "a_\<beta> (Or p q) = (\<lambda> k. Or (a_\<beta> p k) (a_\<beta> q k))"
+| "a_\<beta> (Eq (CN 0 c e)) = (\<lambda> k. Eq (CN 0 1 (Mul (k div c) e)))"
+| "a_\<beta> (NEq (CN 0 c e)) = (\<lambda> k. NEq (CN 0 1 (Mul (k div c) e)))"
+| "a_\<beta> (Lt (CN 0 c e)) = (\<lambda> k. Lt (CN 0 1 (Mul (k div c) e)))"
+| "a_\<beta> (Le (CN 0 c e)) = (\<lambda> k. Le (CN 0 1 (Mul (k div c) e)))"
+| "a_\<beta> (Gt (CN 0 c e)) = (\<lambda> k. Gt (CN 0 1 (Mul (k div c) e)))"
+| "a_\<beta> (Ge (CN 0 c e)) = (\<lambda> k. Ge (CN 0 1 (Mul (k div c) e)))"
+| "a_\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
+| "a_\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
+| "a_\<beta> p = (\<lambda> k. p)"
+
+fun d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" where (* tests if all coeffs c of c divide a given l*)
"d_\<beta> (And p q) = (\<lambda> k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
- "d_\<beta> (Or p q) = (\<lambda> k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
- "d_\<beta> (Eq (CN 0 c e)) = (\<lambda> k. c dvd k)"
- "d_\<beta> (NEq (CN 0 c e)) = (\<lambda> k. c dvd k)"
- "d_\<beta> (Lt (CN 0 c e)) = (\<lambda> k. c dvd k)"
- "d_\<beta> (Le (CN 0 c e)) = (\<lambda> k. c dvd k)"
- "d_\<beta> (Gt (CN 0 c e)) = (\<lambda> k. c dvd k)"
- "d_\<beta> (Ge (CN 0 c e)) = (\<lambda> k. c dvd k)"
- "d_\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. c dvd k)"
- "d_\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. c dvd k)"
- "d_\<beta> p = (\<lambda> k. True)"
-
-recdef \<zeta> "measure size"
+| "d_\<beta> (Or p q) = (\<lambda> k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
+| "d_\<beta> (Eq (CN 0 c e)) = (\<lambda> k. c dvd k)"
+| "d_\<beta> (NEq (CN 0 c e)) = (\<lambda> k. c dvd k)"
+| "d_\<beta> (Lt (CN 0 c e)) = (\<lambda> k. c dvd k)"
+| "d_\<beta> (Le (CN 0 c e)) = (\<lambda> k. c dvd k)"
+| "d_\<beta> (Gt (CN 0 c e)) = (\<lambda> k. c dvd k)"
+| "d_\<beta> (Ge (CN 0 c e)) = (\<lambda> k. c dvd k)"
+| "d_\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. c dvd k)"
+| "d_\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. c dvd k)"
+| "d_\<beta> p = (\<lambda> k. True)"
+
+fun \<zeta> :: "fm \<Rightarrow> int" where (* computes the lcm of all coefficients of x*)
"\<zeta> (And p q) = lcm (\<zeta> p) (\<zeta> q)"
- "\<zeta> (Or p q) = lcm (\<zeta> p) (\<zeta> q)"
- "\<zeta> (Eq (CN 0 c e)) = c"
- "\<zeta> (NEq (CN 0 c e)) = c"
- "\<zeta> (Lt (CN 0 c e)) = c"
- "\<zeta> (Le (CN 0 c e)) = c"
- "\<zeta> (Gt (CN 0 c e)) = c"
- "\<zeta> (Ge (CN 0 c e)) = c"
- "\<zeta> (Dvd i (CN 0 c e)) = c"
- "\<zeta> (NDvd i (CN 0 c e))= c"
- "\<zeta> p = 1"
-
-recdef \<beta> "measure size"
+| "\<zeta> (Or p q) = lcm (\<zeta> p) (\<zeta> q)"
+| "\<zeta> (Eq (CN 0 c e)) = c"
+| "\<zeta> (NEq (CN 0 c e)) = c"
+| "\<zeta> (Lt (CN 0 c e)) = c"
+| "\<zeta> (Le (CN 0 c e)) = c"
+| "\<zeta> (Gt (CN 0 c e)) = c"
+| "\<zeta> (Ge (CN 0 c e)) = c"
+| "\<zeta> (Dvd i (CN 0 c e)) = c"
+| "\<zeta> (NDvd i (CN 0 c e))= c"
+| "\<zeta> p = 1"
+
+fun \<beta> :: "fm \<Rightarrow> num list" where
"\<beta> (And p q) = (\<beta> p @ \<beta> q)"
- "\<beta> (Or p q) = (\<beta> p @ \<beta> q)"
- "\<beta> (Eq (CN 0 c e)) = [Sub (C (- 1)) e]"
- "\<beta> (NEq (CN 0 c e)) = [Neg e]"
- "\<beta> (Lt (CN 0 c e)) = []"
- "\<beta> (Le (CN 0 c e)) = []"
- "\<beta> (Gt (CN 0 c e)) = [Neg e]"
- "\<beta> (Ge (CN 0 c e)) = [Sub (C (- 1)) e]"
- "\<beta> p = []"
-
-recdef \<alpha> "measure size"
+| "\<beta> (Or p q) = (\<beta> p @ \<beta> q)"
+| "\<beta> (Eq (CN 0 c e)) = [Sub (C (- 1)) e]"
+| "\<beta> (NEq (CN 0 c e)) = [Neg e]"
+| "\<beta> (Lt (CN 0 c e)) = []"
+| "\<beta> (Le (CN 0 c e)) = []"
+| "\<beta> (Gt (CN 0 c e)) = [Neg e]"
+| "\<beta> (Ge (CN 0 c e)) = [Sub (C (- 1)) e]"
+| "\<beta> p = []"
+
+fun \<alpha> :: "fm \<Rightarrow> num list" where
"\<alpha> (And p q) = (\<alpha> p @ \<alpha> q)"
- "\<alpha> (Or p q) = (\<alpha> p @ \<alpha> q)"
- "\<alpha> (Eq (CN 0 c e)) = [Add (C (- 1)) e]"
- "\<alpha> (NEq (CN 0 c e)) = [e]"
- "\<alpha> (Lt (CN 0 c e)) = [e]"
- "\<alpha> (Le (CN 0 c e)) = [Add (C (- 1)) e]"
- "\<alpha> (Gt (CN 0 c e)) = []"
- "\<alpha> (Ge (CN 0 c e)) = []"
- "\<alpha> p = []"
-consts mirror :: "fm \<Rightarrow> fm"
-recdef mirror "measure size"
+| "\<alpha> (Or p q) = (\<alpha> p @ \<alpha> q)"
+| "\<alpha> (Eq (CN 0 c e)) = [Add (C (- 1)) e]"
+| "\<alpha> (NEq (CN 0 c e)) = [e]"
+| "\<alpha> (Lt (CN 0 c e)) = [e]"
+| "\<alpha> (Le (CN 0 c e)) = [Add (C (- 1)) e]"
+| "\<alpha> (Gt (CN 0 c e)) = []"
+| "\<alpha> (Ge (CN 0 c e)) = []"
+| "\<alpha> p = []"
+
+fun mirror :: "fm \<Rightarrow> fm" where
"mirror (And p q) = And (mirror p) (mirror q)"
- "mirror (Or p q) = Or (mirror p) (mirror q)"
- "mirror (Eq (CN 0 c e)) = Eq (CN 0 c (Neg e))"
- "mirror (NEq (CN 0 c e)) = NEq (CN 0 c (Neg e))"
- "mirror (Lt (CN 0 c e)) = Gt (CN 0 c (Neg e))"
- "mirror (Le (CN 0 c e)) = Ge (CN 0 c (Neg e))"
- "mirror (Gt (CN 0 c e)) = Lt (CN 0 c (Neg e))"
- "mirror (Ge (CN 0 c e)) = Le (CN 0 c (Neg e))"
- "mirror (Dvd i (CN 0 c e)) = Dvd i (CN 0 c (Neg e))"
- "mirror (NDvd i (CN 0 c e)) = NDvd i (CN 0 c (Neg e))"
- "mirror p = p"
+| "mirror (Or p q) = Or (mirror p) (mirror q)"
+| "mirror (Eq (CN 0 c e)) = Eq (CN 0 c (Neg e))"
+| "mirror (NEq (CN 0 c e)) = NEq (CN 0 c (Neg e))"
+| "mirror (Lt (CN 0 c e)) = Gt (CN 0 c (Neg e))"
+| "mirror (Le (CN 0 c e)) = Ge (CN 0 c (Neg e))"
+| "mirror (Gt (CN 0 c e)) = Lt (CN 0 c (Neg e))"
+| "mirror (Ge (CN 0 c e)) = Le (CN 0 c (Neg e))"
+| "mirror (Dvd i (CN 0 c e)) = Dvd i (CN 0 c (Neg e))"
+| "mirror (NDvd i (CN 0 c e)) = NDvd i (CN 0 c (Neg e))"
+| "mirror p = p"
lemma mirror_\<alpha>_\<beta>:
assumes lp: "iszlfm p (a#bs)"
@@ -2787,52 +2778,46 @@
(* Reddy and Loveland *)
-
-consts
- \<rho> :: "fm \<Rightarrow> (num \<times> int) list" (* Compute the Reddy and Loveland Bset*)
- \<sigma>_\<rho>:: "fm \<Rightarrow> num \<times> int \<Rightarrow> fm" (* Performs the modified substitution of Reddy and Loveland*)
- \<alpha>_\<rho> :: "fm \<Rightarrow> (num\<times>int) list"
- a_\<rho> :: "fm \<Rightarrow> int \<Rightarrow> fm"
-recdef \<rho> "measure size"
+fun \<rho> :: "fm \<Rightarrow> (num \<times> int) list" where (* Compute the Reddy and Loveland Bset*)
"\<rho> (And p q) = (\<rho> p @ \<rho> q)"
- "\<rho> (Or p q) = (\<rho> p @ \<rho> q)"
- "\<rho> (Eq (CN 0 c e)) = [(Sub (C (- 1)) e,c)]"
- "\<rho> (NEq (CN 0 c e)) = [(Neg e,c)]"
- "\<rho> (Lt (CN 0 c e)) = []"
- "\<rho> (Le (CN 0 c e)) = []"
- "\<rho> (Gt (CN 0 c e)) = [(Neg e, c)]"
- "\<rho> (Ge (CN 0 c e)) = [(Sub (C (-1)) e, c)]"
- "\<rho> p = []"
-
-recdef \<sigma>_\<rho> "measure size"
+| "\<rho> (Or p q) = (\<rho> p @ \<rho> q)"
+| "\<rho> (Eq (CN 0 c e)) = [(Sub (C (- 1)) e,c)]"
+| "\<rho> (NEq (CN 0 c e)) = [(Neg e,c)]"
+| "\<rho> (Lt (CN 0 c e)) = []"
+| "\<rho> (Le (CN 0 c e)) = []"
+| "\<rho> (Gt (CN 0 c e)) = [(Neg e, c)]"
+| "\<rho> (Ge (CN 0 c e)) = [(Sub (C (-1)) e, c)]"
+| "\<rho> p = []"
+
+fun \<sigma>_\<rho>:: "fm \<Rightarrow> num \<times> int \<Rightarrow> fm" where (* Performs the modified substitution of Reddy and Loveland*)
"\<sigma>_\<rho> (And p q) = (\<lambda> (t,k). And (\<sigma>_\<rho> p (t,k)) (\<sigma>_\<rho> q (t,k)))"
- "\<sigma>_\<rho> (Or p q) = (\<lambda> (t,k). Or (\<sigma>_\<rho> p (t,k)) (\<sigma>_\<rho> q (t,k)))"
- "\<sigma>_\<rho> (Eq (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Eq (Add (Mul (c div k) t) e))
+| "\<sigma>_\<rho> (Or p q) = (\<lambda> (t,k). Or (\<sigma>_\<rho> p (t,k)) (\<sigma>_\<rho> q (t,k)))"
+| "\<sigma>_\<rho> (Eq (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Eq (Add (Mul (c div k) t) e))
else (Eq (Add (Mul c t) (Mul k e))))"
- "\<sigma>_\<rho> (NEq (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (NEq (Add (Mul (c div k) t) e))
+| "\<sigma>_\<rho> (NEq (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (NEq (Add (Mul (c div k) t) e))
else (NEq (Add (Mul c t) (Mul k e))))"
- "\<sigma>_\<rho> (Lt (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Lt (Add (Mul (c div k) t) e))
+| "\<sigma>_\<rho> (Lt (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Lt (Add (Mul (c div k) t) e))
else (Lt (Add (Mul c t) (Mul k e))))"
- "\<sigma>_\<rho> (Le (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Le (Add (Mul (c div k) t) e))
+| "\<sigma>_\<rho> (Le (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Le (Add (Mul (c div k) t) e))
else (Le (Add (Mul c t) (Mul k e))))"
- "\<sigma>_\<rho> (Gt (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Gt (Add (Mul (c div k) t) e))
+| "\<sigma>_\<rho> (Gt (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Gt (Add (Mul (c div k) t) e))
else (Gt (Add (Mul c t) (Mul k e))))"
- "\<sigma>_\<rho> (Ge (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Ge (Add (Mul (c div k) t) e))
+| "\<sigma>_\<rho> (Ge (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Ge (Add (Mul (c div k) t) e))
else (Ge (Add (Mul c t) (Mul k e))))"
- "\<sigma>_\<rho> (Dvd i (CN 0 c e)) =(\<lambda> (t,k). if k dvd c then (Dvd i (Add (Mul (c div k) t) e))
+| "\<sigma>_\<rho> (Dvd i (CN 0 c e)) =(\<lambda> (t,k). if k dvd c then (Dvd i (Add (Mul (c div k) t) e))
else (Dvd (i*k) (Add (Mul c t) (Mul k e))))"
- "\<sigma>_\<rho> (NDvd i (CN 0 c e))=(\<lambda> (t,k). if k dvd c then (NDvd i (Add (Mul (c div k) t) e))
+| "\<sigma>_\<rho> (NDvd i (CN 0 c e))=(\<lambda> (t,k). if k dvd c then (NDvd i (Add (Mul (c div k) t) e))
else (NDvd (i*k) (Add (Mul c t) (Mul k e))))"
- "\<sigma>_\<rho> p = (\<lambda> (t,k). p)"
-
-recdef \<alpha>_\<rho> "measure size"
+| "\<sigma>_\<rho> p = (\<lambda> (t,k). p)"
+
+fun \<alpha>_\<rho> :: "fm \<Rightarrow> (num\<times>int) list" where
"\<alpha>_\<rho> (And p q) = (\<alpha>_\<rho> p @ \<alpha>_\<rho> q)"
- "\<alpha>_\<rho> (Or p q) = (\<alpha>_\<rho> p @ \<alpha>_\<rho> q)"
- "\<alpha>_\<rho> (Eq (CN 0 c e)) = [(Add (C (- 1)) e,c)]"
- "\<alpha>_\<rho> (NEq (CN 0 c e)) = [(e,c)]"
- "\<alpha>_\<rho> (Lt (CN 0 c e)) = [(e,c)]"
- "\<alpha>_\<rho> (Le (CN 0 c e)) = [(Add (C (- 1)) e,c)]"
- "\<alpha>_\<rho> p = []"
+| "\<alpha>_\<rho> (Or p q) = (\<alpha>_\<rho> p @ \<alpha>_\<rho> q)"
+| "\<alpha>_\<rho> (Eq (CN 0 c e)) = [(Add (C (- 1)) e,c)]"
+| "\<alpha>_\<rho> (NEq (CN 0 c e)) = [(e,c)]"
+| "\<alpha>_\<rho> (Lt (CN 0 c e)) = [(e,c)]"
+| "\<alpha>_\<rho> (Le (CN 0 c e)) = [(Add (C (- 1)) e,c)]"
+| "\<alpha>_\<rho> p = []"
(* Simulates normal substituion by modifying the formula see correctness theorem *)
@@ -3297,18 +3282,16 @@
text {* The @{text "\<real>"} part*}
text{* Linearity for fm where Bound 0 ranges over @{text "\<real>"}*}
-consts
- isrlfm :: "fm \<Rightarrow> bool" (* Linearity test for fm *)
-recdef isrlfm "measure size"
+fun isrlfm :: "fm \<Rightarrow> bool" where (* Linearity test for fm *)
"isrlfm (And p q) = (isrlfm p \<and> isrlfm q)"
- "isrlfm (Or p q) = (isrlfm p \<and> isrlfm q)"
- "isrlfm (Eq (CN 0 c e)) = (c>0 \<and> numbound0 e)"
- "isrlfm (NEq (CN 0 c e)) = (c>0 \<and> numbound0 e)"
- "isrlfm (Lt (CN 0 c e)) = (c>0 \<and> numbound0 e)"
- "isrlfm (Le (CN 0 c e)) = (c>0 \<and> numbound0 e)"
- "isrlfm (Gt (CN 0 c e)) = (c>0 \<and> numbound0 e)"
- "isrlfm (Ge (CN 0 c e)) = (c>0 \<and> numbound0 e)"
- "isrlfm p = (isatom p \<and> (bound0 p))"
+| "isrlfm (Or p q) = (isrlfm p \<and> isrlfm q)"
+| "isrlfm (Eq (CN 0 c e)) = (c>0 \<and> numbound0 e)"
+| "isrlfm (NEq (CN 0 c e)) = (c>0 \<and> numbound0 e)"
+| "isrlfm (Lt (CN 0 c e)) = (c>0 \<and> numbound0 e)"
+| "isrlfm (Le (CN 0 c e)) = (c>0 \<and> numbound0 e)"
+| "isrlfm (Gt (CN 0 c e)) = (c>0 \<and> numbound0 e)"
+| "isrlfm (Ge (CN 0 c e)) = (c>0 \<and> numbound0 e)"
+| "isrlfm p = (isatom p \<and> (bound0 p))"
definition fp :: "fm \<Rightarrow> int \<Rightarrow> num \<Rightarrow> int \<Rightarrow> fm" where
"fp p n s j \<equiv> (if n > 0 then
@@ -3934,36 +3917,37 @@
by (rule rsplit_l[where f="NDVD i" and a="a"], auto simp add: NDVD_def neq_def NDVDJ_l)
(case_tac s, simp_all, rename_tac nat a b, case_tac "nat", simp_all)
-consts rlfm :: "fm \<Rightarrow> fm"
-recdef rlfm "measure fmsize"
+function (sequential) rlfm :: "fm \<Rightarrow> fm" where
"rlfm (And p q) = conj (rlfm p) (rlfm q)"
- "rlfm (Or p q) = disj (rlfm p) (rlfm q)"
- "rlfm (Imp p q) = disj (rlfm (NOT p)) (rlfm q)"
- "rlfm (Iff p q) = disj (conj(rlfm p) (rlfm q)) (conj(rlfm (NOT p)) (rlfm (NOT q)))"
- "rlfm (Lt a) = rsplit lt a"
- "rlfm (Le a) = rsplit le a"
- "rlfm (Gt a) = rsplit gt a"
- "rlfm (Ge a) = rsplit ge a"
- "rlfm (Eq a) = rsplit eq a"
- "rlfm (NEq a) = rsplit neq a"
- "rlfm (Dvd i a) = rsplit (\<lambda> t. DVD i t) a"
- "rlfm (NDvd i a) = rsplit (\<lambda> t. NDVD i t) a"
- "rlfm (NOT (And p q)) = disj (rlfm (NOT p)) (rlfm (NOT q))"
- "rlfm (NOT (Or p q)) = conj (rlfm (NOT p)) (rlfm (NOT q))"
- "rlfm (NOT (Imp p q)) = conj (rlfm p) (rlfm (NOT q))"
- "rlfm (NOT (Iff p q)) = disj (conj(rlfm p) (rlfm(NOT q))) (conj(rlfm(NOT p)) (rlfm q))"
- "rlfm (NOT (NOT p)) = rlfm p"
- "rlfm (NOT T) = F"
- "rlfm (NOT F) = T"
- "rlfm (NOT (Lt a)) = simpfm (rlfm (Ge a))"
- "rlfm (NOT (Le a)) = simpfm (rlfm (Gt a))"
- "rlfm (NOT (Gt a)) = simpfm (rlfm (Le a))"
- "rlfm (NOT (Ge a)) = simpfm (rlfm (Lt a))"
- "rlfm (NOT (Eq a)) = simpfm (rlfm (NEq a))"
- "rlfm (NOT (NEq a)) = simpfm (rlfm (Eq a))"
- "rlfm (NOT (Dvd i a)) = simpfm (rlfm (NDvd i a))"
- "rlfm (NOT (NDvd i a)) = simpfm (rlfm (Dvd i a))"
- "rlfm p = p" (hints simp add: fmsize_pos)
+| "rlfm (Or p q) = disj (rlfm p) (rlfm q)"
+| "rlfm (Imp p q) = disj (rlfm (NOT p)) (rlfm q)"
+| "rlfm (Iff p q) = disj (conj(rlfm p) (rlfm q)) (conj(rlfm (NOT p)) (rlfm (NOT q)))"
+| "rlfm (Lt a) = rsplit lt a"
+| "rlfm (Le a) = rsplit le a"
+| "rlfm (Gt a) = rsplit gt a"
+| "rlfm (Ge a) = rsplit ge a"
+| "rlfm (Eq a) = rsplit eq a"
+| "rlfm (NEq a) = rsplit neq a"
+| "rlfm (Dvd i a) = rsplit (\<lambda> t. DVD i t) a"
+| "rlfm (NDvd i a) = rsplit (\<lambda> t. NDVD i t) a"
+| "rlfm (NOT (And p q)) = disj (rlfm (NOT p)) (rlfm (NOT q))"
+| "rlfm (NOT (Or p q)) = conj (rlfm (NOT p)) (rlfm (NOT q))"
+| "rlfm (NOT (Imp p q)) = conj (rlfm p) (rlfm (NOT q))"
+| "rlfm (NOT (Iff p q)) = disj (conj(rlfm p) (rlfm(NOT q))) (conj(rlfm(NOT p)) (rlfm q))"
+| "rlfm (NOT (NOT p)) = rlfm p"
+| "rlfm (NOT T) = F"
+| "rlfm (NOT F) = T"
+| "rlfm (NOT (Lt a)) = simpfm (rlfm (Ge a))"
+| "rlfm (NOT (Le a)) = simpfm (rlfm (Gt a))"
+| "rlfm (NOT (Gt a)) = simpfm (rlfm (Le a))"
+| "rlfm (NOT (Ge a)) = simpfm (rlfm (Lt a))"
+| "rlfm (NOT (Eq a)) = simpfm (rlfm (NEq a))"
+| "rlfm (NOT (NEq a)) = simpfm (rlfm (Eq a))"
+| "rlfm (NOT (Dvd i a)) = simpfm (rlfm (NDvd i a))"
+| "rlfm (NOT (NDvd i a)) = simpfm (rlfm (Dvd i a))"
+| "rlfm p = p"
+ by pat_completeness auto
+termination by (relation "measure fmsize") auto
lemma bound0at_l : "\<lbrakk>isatom p ; bound0 p\<rbrakk> \<Longrightarrow> isrlfm p"
by (induct p rule: isrlfm.induct, auto)
@@ -4397,30 +4381,27 @@
ultimately show ?thesis using z_def by auto
qed
-consts
- \<Upsilon>:: "fm \<Rightarrow> (num \<times> int) list"
- \<upsilon> :: "fm \<Rightarrow> (num \<times> int) \<Rightarrow> fm "
-recdef \<Upsilon> "measure size"
+fun \<Upsilon>:: "fm \<Rightarrow> (num \<times> int) list" where
"\<Upsilon> (And p q) = (\<Upsilon> p @ \<Upsilon> q)"
- "\<Upsilon> (Or p q) = (\<Upsilon> p @ \<Upsilon> q)"
- "\<Upsilon> (Eq (CN 0 c e)) = [(Neg e,c)]"
- "\<Upsilon> (NEq (CN 0 c e)) = [(Neg e,c)]"
- "\<Upsilon> (Lt (CN 0 c e)) = [(Neg e,c)]"
- "\<Upsilon> (Le (CN 0 c e)) = [(Neg e,c)]"
- "\<Upsilon> (Gt (CN 0 c e)) = [(Neg e,c)]"
- "\<Upsilon> (Ge (CN 0 c e)) = [(Neg e,c)]"
- "\<Upsilon> p = []"
-
-recdef \<upsilon> "measure size"
+| "\<Upsilon> (Or p q) = (\<Upsilon> p @ \<Upsilon> q)"
+| "\<Upsilon> (Eq (CN 0 c e)) = [(Neg e,c)]"
+| "\<Upsilon> (NEq (CN 0 c e)) = [(Neg e,c)]"
+| "\<Upsilon> (Lt (CN 0 c e)) = [(Neg e,c)]"
+| "\<Upsilon> (Le (CN 0 c e)) = [(Neg e,c)]"
+| "\<Upsilon> (Gt (CN 0 c e)) = [(Neg e,c)]"
+| "\<Upsilon> (Ge (CN 0 c e)) = [(Neg e,c)]"
+| "\<Upsilon> p = []"
+
+fun \<upsilon> :: "fm \<Rightarrow> (num \<times> int) \<Rightarrow> fm" where
"\<upsilon> (And p q) = (\<lambda> (t,n). And (\<upsilon> p (t,n)) (\<upsilon> q (t,n)))"
- "\<upsilon> (Or p q) = (\<lambda> (t,n). Or (\<upsilon> p (t,n)) (\<upsilon> q (t,n)))"
- "\<upsilon> (Eq (CN 0 c e)) = (\<lambda> (t,n). Eq (Add (Mul c t) (Mul n e)))"
- "\<upsilon> (NEq (CN 0 c e)) = (\<lambda> (t,n). NEq (Add (Mul c t) (Mul n e)))"
- "\<upsilon> (Lt (CN 0 c e)) = (\<lambda> (t,n). Lt (Add (Mul c t) (Mul n e)))"
- "\<upsilon> (Le (CN 0 c e)) = (\<lambda> (t,n). Le (Add (Mul c t) (Mul n e)))"
- "\<upsilon> (Gt (CN 0 c e)) = (\<lambda> (t,n). Gt (Add (Mul c t) (Mul n e)))"
- "\<upsilon> (Ge (CN 0 c e)) = (\<lambda> (t,n). Ge (Add (Mul c t) (Mul n e)))"
- "\<upsilon> p = (\<lambda> (t,n). p)"
+| "\<upsilon> (Or p q) = (\<lambda> (t,n). Or (\<upsilon> p (t,n)) (\<upsilon> q (t,n)))"
+| "\<upsilon> (Eq (CN 0 c e)) = (\<lambda> (t,n). Eq (Add (Mul c t) (Mul n e)))"
+| "\<upsilon> (NEq (CN 0 c e)) = (\<lambda> (t,n). NEq (Add (Mul c t) (Mul n e)))"
+| "\<upsilon> (Lt (CN 0 c e)) = (\<lambda> (t,n). Lt (Add (Mul c t) (Mul n e)))"
+| "\<upsilon> (Le (CN 0 c e)) = (\<lambda> (t,n). Le (Add (Mul c t) (Mul n e)))"
+| "\<upsilon> (Gt (CN 0 c e)) = (\<lambda> (t,n). Gt (Add (Mul c t) (Mul n e)))"
+| "\<upsilon> (Ge (CN 0 c e)) = (\<lambda> (t,n). Ge (Add (Mul c t) (Mul n e)))"
+| "\<upsilon> p = (\<lambda> (t,n). p)"
lemma \<upsilon>_I: assumes lp: "isrlfm p"
and np: "real n > 0" and nbt: "numbound0 t"
diff -r 392402362c3e -r 03ef7232e0f0 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fr Jun 05 09:15:37 2015 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy So Jun 07 08:31:04 2015 +0200
@@ -10,7 +10,6 @@
Dense_Linear_Order
DP_Library
"~~/src/HOL/Library/Code_Target_Numeral"
- "~~/src/HOL/Library/Old_Recdef"
begin
subsection {* Terms *}
@@ -258,21 +257,20 @@
(* Simplification *)
-consts tmadd:: "tm \<times> tm \<Rightarrow> tm"
-recdef tmadd "measure (\<lambda>(t,s). size t + size s)"
+fun tmadd:: "tm \<times> tm \<Rightarrow> tm" where
"tmadd (CNP n1 c1 r1,CNP n2 c2 r2) =
(if n1 = n2 then
let c = c1 +\<^sub>p c2
in if c = 0\<^sub>p then tmadd(r1,r2) else CNP n1 c (tmadd (r1, r2))
else if n1 \<le> n2 then (CNP n1 c1 (tmadd (r1,CNP n2 c2 r2)))
else (CNP n2 c2 (tmadd (CNP n1 c1 r1, r2))))"
- "tmadd (CNP n1 c1 r1, t) = CNP n1 c1 (tmadd (r1, t))"
- "tmadd (t, CNP n2 c2 r2) = CNP n2 c2 (tmadd (t, r2))"
- "tmadd (CP b1, CP b2) = CP (b1 +\<^sub>p b2)"
- "tmadd (a, b) = Add a b"
+| "tmadd (CNP n1 c1 r1, t) = CNP n1 c1 (tmadd (r1, t))"
+| "tmadd (t, CNP n2 c2 r2) = CNP n2 c2 (tmadd (t, r2))"
+| "tmadd (CP b1, CP b2) = CP (b1 +\<^sub>p b2)"
+| "tmadd (a, b) = Add a b"
lemma tmadd[simp]: "Itm vs bs (tmadd (t, s)) = Itm vs bs (Add t s)"
- apply (induct t s rule: tmadd.induct, simp_all add: Let_def)
+ apply (induct t s rule: tmadd.induct[split_format (complete)], simp_all add: Let_def)
apply (case_tac "c1 +\<^sub>p c2 = 0\<^sub>p",case_tac "n1 \<le> n2", simp_all)
apply (case_tac "n1 = n2", simp_all add: field_simps)
apply (simp only: distrib_left[symmetric])
@@ -280,17 +278,17 @@
done
lemma tmadd_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 s \<Longrightarrow> tmbound0 (tmadd (t, s))"
- by (induct t s rule: tmadd.induct) (auto simp add: Let_def)
+ by (induct t s rule: tmadd.induct[split_format (complete)]) (auto simp add: Let_def)
lemma tmadd_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n s \<Longrightarrow> tmbound n (tmadd (t, s))"
- by (induct t s rule: tmadd.induct) (auto simp add: Let_def)
+ by (induct t s rule: tmadd.induct[split_format (complete)]) (auto simp add: Let_def)
lemma tmadd_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n s \<Longrightarrow> tmboundslt n (tmadd (t, s))"
- by (induct t s rule: tmadd.induct) (auto simp add: Let_def)
+ by (induct t s rule: tmadd.induct[split_format (complete)]) (auto simp add: Let_def)
lemma tmadd_allpolys_npoly[simp]:
"allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmadd(t, s))"
- by (induct t s rule: tmadd.induct) (simp_all add: Let_def polyadd_norm)
+ by (induct t s rule: tmadd.induct[split_format (complete)]) (simp_all add: Let_def polyadd_norm)
fun tmmul:: "tm \<Rightarrow> poly \<Rightarrow> tm"
where
@@ -1497,30 +1495,31 @@
by blast
qed
-consts simpfm :: "fm \<Rightarrow> fm"
-recdef simpfm "measure fmsize"
+function (sequential) simpfm :: "fm \<Rightarrow> fm" where
"simpfm (Lt t) = simplt (simptm t)"
- "simpfm (Le t) = simple (simptm t)"
- "simpfm (Eq t) = simpeq(simptm t)"
- "simpfm (NEq t) = simpneq(simptm t)"
- "simpfm (And p q) = conj (simpfm p) (simpfm q)"
- "simpfm (Or p q) = disj (simpfm p) (simpfm q)"
- "simpfm (Imp p q) = disj (simpfm (NOT p)) (simpfm q)"
- "simpfm (Iff p q) =
+| "simpfm (Le t) = simple (simptm t)"
+| "simpfm (Eq t) = simpeq(simptm t)"
+| "simpfm (NEq t) = simpneq(simptm t)"
+| "simpfm (And p q) = conj (simpfm p) (simpfm q)"
+| "simpfm (Or p q) = disj (simpfm p) (simpfm q)"
+| "simpfm (Imp p q) = disj (simpfm (NOT p)) (simpfm q)"
+| "simpfm (Iff p q) =
disj (conj (simpfm p) (simpfm q)) (conj (simpfm (NOT p)) (simpfm (NOT q)))"
- "simpfm (NOT (And p q)) = disj (simpfm (NOT p)) (simpfm (NOT q))"
- "simpfm (NOT (Or p q)) = conj (simpfm (NOT p)) (simpfm (NOT q))"
- "simpfm (NOT (Imp p q)) = conj (simpfm p) (simpfm (NOT q))"
- "simpfm (NOT (Iff p q)) =
+| "simpfm (NOT (And p q)) = disj (simpfm (NOT p)) (simpfm (NOT q))"
+| "simpfm (NOT (Or p q)) = conj (simpfm (NOT p)) (simpfm (NOT q))"
+| "simpfm (NOT (Imp p q)) = conj (simpfm p) (simpfm (NOT q))"
+| "simpfm (NOT (Iff p q)) =
disj (conj (simpfm p) (simpfm (NOT q))) (conj (simpfm (NOT p)) (simpfm q))"
- "simpfm (NOT (Eq t)) = simpneq t"
- "simpfm (NOT (NEq t)) = simpeq t"
- "simpfm (NOT (Le t)) = simplt (Neg t)"
- "simpfm (NOT (Lt t)) = simple (Neg t)"
- "simpfm (NOT (NOT p)) = simpfm p"
- "simpfm (NOT T) = F"
- "simpfm (NOT F) = T"
- "simpfm p = p"
+| "simpfm (NOT (Eq t)) = simpneq t"
+| "simpfm (NOT (NEq t)) = simpeq t"
+| "simpfm (NOT (Le t)) = simplt (Neg t)"
+| "simpfm (NOT (Lt t)) = simple (Neg t)"
+| "simpfm (NOT (NOT p)) = simpfm p"
+| "simpfm (NOT T) = F"
+| "simpfm (NOT F) = T"
+| "simpfm p = p"
+ by pat_completeness auto
+termination by (relation "measure fmsize") auto
lemma simpfm[simp]: "Ifm vs bs (simpfm p) = Ifm vs bs p"
by (induct p arbitrary: bs rule: simpfm.induct) auto
@@ -1571,32 +1570,32 @@
shows "qfree p \<Longrightarrow> islin (simpfm p)"
by (induct p rule: simpfm.induct) (simp_all add: conj_lin disj_lin)
-consts prep :: "fm \<Rightarrow> fm"
-recdef prep "measure fmsize"
+function (sequential) prep :: "fm \<Rightarrow> fm" where
"prep (E T) = T"
- "prep (E F) = F"
- "prep (E (Or p q)) = disj (prep (E p)) (prep (E q))"
- "prep (E (Imp p q)) = disj (prep (E (NOT p))) (prep (E q))"
- "prep (E (Iff p q)) = disj (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))"
- "prep (E (NOT (And p q))) = disj (prep (E (NOT p))) (prep (E(NOT q)))"
- "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))"
- "prep (E (NOT (Iff p q))) = disj (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))"
- "prep (E p) = E (prep p)"
- "prep (A (And p q)) = conj (prep (A p)) (prep (A q))"
- "prep (A p) = prep (NOT (E (NOT p)))"
- "prep (NOT (NOT p)) = prep p"
- "prep (NOT (And p q)) = disj (prep (NOT p)) (prep (NOT q))"
- "prep (NOT (A p)) = prep (E (NOT p))"
- "prep (NOT (Or p q)) = conj (prep (NOT p)) (prep (NOT q))"
- "prep (NOT (Imp p q)) = conj (prep p) (prep (NOT q))"
- "prep (NOT (Iff p q)) = disj (prep (And p (NOT q))) (prep (And (NOT p) q))"
- "prep (NOT p) = not (prep p)"
- "prep (Or p q) = disj (prep p) (prep q)"
- "prep (And p q) = conj (prep p) (prep q)"
- "prep (Imp p q) = prep (Or (NOT p) q)"
- "prep (Iff p q) = disj (prep (And p q)) (prep (And (NOT p) (NOT q)))"
- "prep p = p"
-(hints simp add: fmsize_pos)
+| "prep (E F) = F"
+| "prep (E (Or p q)) = disj (prep (E p)) (prep (E q))"
+| "prep (E (Imp p q)) = disj (prep (E (NOT p))) (prep (E q))"
+| "prep (E (Iff p q)) = disj (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))"
+| "prep (E (NOT (And p q))) = disj (prep (E (NOT p))) (prep (E(NOT q)))"
+| "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))"
+| "prep (E (NOT (Iff p q))) = disj (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))"
+| "prep (E p) = E (prep p)"
+| "prep (A (And p q)) = conj (prep (A p)) (prep (A q))"
+| "prep (A p) = prep (NOT (E (NOT p)))"
+| "prep (NOT (NOT p)) = prep p"
+| "prep (NOT (And p q)) = disj (prep (NOT p)) (prep (NOT q))"
+| "prep (NOT (A p)) = prep (E (NOT p))"
+| "prep (NOT (Or p q)) = conj (prep (NOT p)) (prep (NOT q))"
+| "prep (NOT (Imp p q)) = conj (prep p) (prep (NOT q))"
+| "prep (NOT (Iff p q)) = disj (prep (And p (NOT q))) (prep (And (NOT p) q))"
+| "prep (NOT p) = not (prep p)"
+| "prep (Or p q) = disj (prep p) (prep q)"
+| "prep (And p q) = conj (prep p) (prep q)"
+| "prep (Imp p q) = prep (Or (NOT p) q)"
+| "prep (Iff p q) = disj (prep (And p q)) (prep (And (NOT p) (NOT q)))"
+| "prep p = p"
+ by pat_completeness auto
+termination by (relation "measure fmsize") (auto simp: fmsize_pos)
lemma prep: "Ifm vs bs (prep p) = Ifm vs bs p"
by (induct p arbitrary: bs rule: prep.induct) auto
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
