--- a/src/HOL/Complex/ex/MIR.thy Thu Jul 03 11:16:09 2008 +0200
+++ b/src/HOL/Complex/ex/MIR.thy Thu Jul 03 11:16:33 2008 +0200
@@ -2,13 +2,13 @@
Author: Amine Chaieb
*)
-header {* Quatifier elimination for R(0,1,+,floor,<) *}
-
theory MIR
-imports List Real Code_Integer
-uses ("mireif.ML") ("mirtac.ML")
+imports List Real Code_Integer Efficient_Nat
+uses ("mirtac.ML")
begin
+section {* Quantifier elimination for @{text "\<real> (0, 1, +, floor, <)"} *}
+
declare real_of_int_floor_cancel [simp del]
primrec alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list" where
@@ -5721,12 +5721,11 @@
shows "qfree (exsplit p)"
using qf by (induct p rule: exsplit.induct, auto)
-constdefs mircfr :: "fm \<Rightarrow> fm"
-"mircfr \<equiv> (DJ cooper) o ferrack01 o simpfm o exsplit"
-
-constdefs mirlfr :: "fm \<Rightarrow> fm"
-"mirlfr \<equiv> (DJ redlove) o ferrack01 o simpfm o exsplit"
-
+definition mircfr :: "fm \<Rightarrow> fm" where
+ "mircfr = DJ cooper o ferrack01 o simpfm o exsplit"
+
+definition mirlfr :: "fm \<Rightarrow> fm" where
+ "mirlfr = DJ redlove o ferrack01 o simpfm o exsplit"
lemma mircfr: "\<forall> bs p. qfree p \<longrightarrow> qfree (mircfr p) \<and> Ifm bs (mircfr p) = Ifm bs (E p)"
proof(clarsimp simp del: Ifm.simps)
@@ -5756,11 +5755,11 @@
qed
qed
-constdefs mircfrqe:: "fm \<Rightarrow> fm"
- "mircfrqe \<equiv> (\<lambda> p. qelim (prep p) mircfr)"
-
-constdefs mirlfrqe:: "fm \<Rightarrow> fm"
- "mirlfrqe \<equiv> (\<lambda> p. qelim (prep p) mirlfr)"
+definition mircfrqe:: "fm \<Rightarrow> fm" where
+ "mircfrqe p = qelim (prep p) mircfr"
+
+definition mirlfrqe:: "fm \<Rightarrow> fm" where
+ "mirlfrqe p = qelim (prep p) mirlfr"
theorem mircfrqe: "(Ifm bs (mircfrqe p) = Ifm bs p) \<and> qfree (mircfrqe p)"
using qelim_ci[OF mircfr] prep by (auto simp add: mircfrqe_def)
@@ -5768,9 +5767,6 @@
theorem mirlfrqe: "(Ifm bs (mirlfrqe p) = Ifm bs p) \<and> qfree (mirlfrqe p)"
using qelim_ci[OF mirlfr] prep by (auto simp add: mirlfrqe_def)
-declare zdvd_iff_zmod_eq_0 [code]
-declare max_def [code unfold]
-
definition
"test1 (u\<Colon>unit) = mircfrqe (A (And (Le (Sub (Floor (Bound 0)) (Bound 0))) (Le (Add (Bound 0) (Floor (Neg (Bound 0)))))))"
@@ -5786,25 +5782,128 @@
definition
"test5 (u\<Colon>unit) = mircfrqe (A(E(And (Ge(Sub (Bound 1) (Bound 0))) (Eq (Add (Floor (Bound 1)) (Floor (Neg(Bound 0))))))))"
-export_code mircfrqe mirlfrqe test1 test2 test3 test4 test5
- in SML module_name Mir
+ML {* @{code test1} () *}
+ML {* @{code test2} () *}
+ML {* @{code test3} () *}
+ML {* @{code test4} () *}
+ML {* @{code test5} () *}
(*export_code mircfrqe mirlfrqe
in SML module_name Mir file "raw_mir.ML"*)
-ML "Mir.test1 ()"
-ML "Mir.test2 ()"
-ML "Mir.test3 ()"
-ML "Mir.test4 ()"
-ML "Mir.test5 ()"
-
-use "mireif.ML"
-oracle mircfr_oracle ("term") = ReflectedMir.mircfr_oracle
-oracle mirlfr_oracle ("term") = ReflectedMir.mirlfr_oracle
+oracle mirfr_oracle ("bool * term") = {*
+let
+
+fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t
+ of NONE => error "Variable not found in the list!"
+ | SOME n => @{code Bound} n)
+ | num_of_term vs @{term "real (0::int)"} = @{code C} 0
+ | num_of_term vs @{term "real (1::int)"} = @{code C} 1
+ | num_of_term vs @{term "0::real"} = @{code C} 0
+ | num_of_term vs @{term "1::real"} = @{code C} 1
+ | num_of_term vs (Bound i) = @{code Bound} i
+ | num_of_term vs (@{term "uminus :: real \<Rightarrow> real"} $ t') = @{code Neg} (num_of_term vs t')
+ | num_of_term vs (@{term "op + :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) =
+ @{code Add} (num_of_term vs t1, num_of_term vs t2)
+ | num_of_term vs (@{term "op - :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) =
+ @{code Sub} (num_of_term vs t1, num_of_term vs t2)
+ | num_of_term vs (@{term "op * :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) =
+ (case (num_of_term vs t1)
+ of @{code C} i => @{code Mul} (i, num_of_term vs t2)
+ | _ => error "num_of_term: unsupported Multiplication")
+ | num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "number_of :: int \<Rightarrow> int"} $ t')) =
+ @{code C} (HOLogic.dest_numeral t')
+ | num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "floor :: real \<Rightarrow> int"} $ t')) =
+ @{code Floor} (num_of_term vs t')
+ | num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "ceiling :: real \<Rightarrow> int"} $ t')) =
+ @{code Neg} (@{code Floor} (@{code Neg} (num_of_term vs t')))
+ | num_of_term vs (@{term "number_of :: int \<Rightarrow> real"} $ t') =
+ @{code C} (HOLogic.dest_numeral t')
+ | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term_global @{theory} t);
+
+fun fm_of_term vs @{term True} = @{code T}
+ | fm_of_term vs @{term False} = @{code F}
+ | fm_of_term vs (@{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) =
+ @{code Lt} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
+ | fm_of_term vs (@{term "op \<le> :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) =
+ @{code Le} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
+ | fm_of_term vs (@{term "op = :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) =
+ @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
+ | fm_of_term vs (@{term "op rdvd"} $ (@{term "real :: int \<Rightarrow> real"} $ (@{term "number_of :: int \<Rightarrow> int"} $ t1)) $ t2) =
+ @{code Dvd} (HOLogic.dest_numeral t1, num_of_term vs t2)
+ | fm_of_term vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
+ @{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
+ | fm_of_term vs (@{term "op &"} $ t1 $ t2) =
+ @{code And} (fm_of_term vs t1, fm_of_term vs t2)
+ | fm_of_term vs (@{term "op |"} $ t1 $ t2) =
+ @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
+ | fm_of_term vs (@{term "op -->"} $ t1 $ t2) =
+ @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
+ | fm_of_term vs (@{term "Not"} $ t') =
+ @{code NOT} (fm_of_term vs t')
+ | fm_of_term vs (Const ("Ex", _) $ Abs (xn, xT, p)) =
+ @{code E} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
+ | fm_of_term vs (Const ("All", _) $ Abs (xn, xT, p)) =
+ @{code A} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
+ | fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term_global @{theory} t);
+
+fun term_of_num vs (@{code C} i) = @{term "real :: int \<Rightarrow> real"} $ HOLogic.mk_number HOLogic.intT i
+ | term_of_num vs (@{code Bound} n) = fst (the (find_first (fn (_, m) => n = m) vs))
+ | term_of_num vs (@{code Neg} (@{code Floor} (@{code Neg} t'))) =
+ @{term "real :: int \<Rightarrow> real"} $ (@{term "ceiling :: real \<Rightarrow> int"} $ term_of_num vs t')
+ | term_of_num vs (@{code Neg} t') = @{term "uminus :: real \<Rightarrow> real"} $ term_of_num vs t'
+ | term_of_num vs (@{code Add} (t1, t2)) = @{term "op + :: real \<Rightarrow> real \<Rightarrow> real"} $
+ term_of_num vs t1 $ term_of_num vs t2
+ | term_of_num vs (@{code Sub} (t1, t2)) = @{term "op - :: real \<Rightarrow> real \<Rightarrow> real"} $
+ term_of_num vs t1 $ term_of_num vs t2
+ | term_of_num vs (@{code Mul} (i, t2)) = @{term "op * :: real \<Rightarrow> real \<Rightarrow> real"} $
+ term_of_num vs (@{code C} i) $ term_of_num vs t2
+ | term_of_num vs (@{code Floor} t) = @{term "real :: int \<Rightarrow> real"} $ (@{term "floor :: real \<Rightarrow> int"} $ term_of_num vs t)
+ | term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t))
+ | term_of_num vs (@{code CF} (c, t, s)) = term_of_num vs (@{code Add} (@{code Mul} (c, @{code Floor} t), s));
+
+fun term_of_fm vs @{code T} = HOLogic.true_const
+ | term_of_fm vs @{code F} = HOLogic.false_const
+ | term_of_fm vs (@{code Lt} t) =
+ @{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $ term_of_num vs t $ @{term "0::real"}
+ | term_of_fm vs (@{code Le} t) =
+ @{term "op \<le> :: real \<Rightarrow> real \<Rightarrow> bool"} $ term_of_num vs t $ @{term "0::real"}
+ | term_of_fm vs (@{code Gt} t) =
+ @{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $ @{term "0::real"} $ term_of_num vs t
+ | term_of_fm vs (@{code Ge} t) =
+ @{term "op \<le> :: real \<Rightarrow> real \<Rightarrow> bool"} $ @{term "0::real"} $ term_of_num vs t
+ | term_of_fm vs (@{code Eq} t) =
+ @{term "op = :: real \<Rightarrow> real \<Rightarrow> bool"} $ term_of_num vs t $ @{term "0::real"}
+ | term_of_fm vs (@{code NEq} t) =
+ term_of_fm vs (@{code NOT} (@{code Eq} t))
+ | term_of_fm vs (@{code Dvd} (i, t)) =
+ @{term "op rdvd"} $ term_of_num vs (@{code C} i) $ term_of_num vs t
+ | term_of_fm vs (@{code NDvd} (i, t)) =
+ term_of_fm vs (@{code NOT} (@{code Dvd} (i, t)))
+ | term_of_fm vs (@{code NOT} t') =
+ HOLogic.Not $ term_of_fm vs t'
+ | term_of_fm vs (@{code And} (t1, t2)) =
+ HOLogic.conj $ term_of_fm vs t1 $ term_of_fm vs t2
+ | term_of_fm vs (@{code Or} (t1, t2)) =
+ HOLogic.disj $ term_of_fm vs t1 $ term_of_fm vs t2
+ | term_of_fm vs (@{code Imp} (t1, t2)) =
+ HOLogic.imp $ term_of_fm vs t1 $ term_of_fm vs t2
+ | term_of_fm vs (@{code Iff} (t1, t2)) =
+ @{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ term_of_fm vs t1 $ term_of_fm vs t2;
+
+in fn thy => fn (proofs, t) =>
+ let
+ val fs = term_frees t;
+ val vs = fs ~~ (0 upto (length fs - 1));
+ val qe = if proofs then @{code mirlfrqe} else @{code mircfrqe};
+ val t' = (term_of_fm vs o qe o fm_of_term vs) t;
+ in (HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
+end;
+*}
+
use "mirtac.ML"
setup "MirTac.setup"
-
lemma "ALL (x::real). (\<lfloor>x\<rfloor> = \<lceil>x\<rceil> = (x = real \<lfloor>x\<rfloor>))"
apply mir
done
@@ -5821,9 +5920,8 @@
apply mir
done
-(*
lemma "ALL x y. \<lfloor>x\<rfloor> = \<lfloor>y\<rfloor> \<longrightarrow> 0 \<le> abs (y - x) \<and> abs (y - x) \<le> 1"
-by mir
-*)
+apply mir
+done
end
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy Thu Jul 03 11:16:09 2008 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy Thu Jul 03 11:16:33 2008 +0200
@@ -2,13 +2,12 @@
Author: Amine Chaieb
*)
-header {* Quatifier elimination for R(0,1,+,<) *}
-
theory ReflectedFerrack
imports Main GCD Real Efficient_Nat
uses ("linrtac.ML")
begin
+section {* Quantifier elimination for @{text "\<real> (0, 1, +, <)"} *}
(*********************************************************************************)
(* SOME GENERAL STUFF< HAS TO BE MOVED IN SOME LIB *)
@@ -1999,7 +1998,6 @@
ML {* @{code ferrack_test} () *}
oracle linr_oracle ("term") = {*
-
let
fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t
@@ -2009,7 +2007,7 @@
| num_of_term vs @{term "real (1::int)"} = @{code C} 1
| num_of_term vs @{term "0::real"} = @{code C} 0
| num_of_term vs @{term "1::real"} = @{code C} 1
- | num_of_term vs (Term.Bound i) = @{code Bound} i
+ | num_of_term vs (Bound i) = @{code Bound} i
| num_of_term vs (@{term "uminus :: real \<Rightarrow> real"} $ t') = @{code Neg} (num_of_term vs t')
| num_of_term vs (@{term "op + :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) = @{code Add} (num_of_term vs t1, num_of_term vs t2)
| num_of_term vs (@{term "op - :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) = @{code Sub} (num_of_term vs t1, num_of_term vs t2)
@@ -2017,22 +2015,22 @@
of @{code C} i => @{code Mul} (i, num_of_term vs t2)
| _ => error "num_of_term: unsupported Multiplication")
| num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "number_of :: int \<Rightarrow> int"} $ t')) = @{code C} (HOLogic.dest_numeral t')
- | num_of_term vs (@{term "number_of :: int \<Rightarrow> int"} $ t') = @{code C} (HOLogic.dest_numeral t')
+ | num_of_term vs (@{term "number_of :: int \<Rightarrow> real"} $ t') = @{code C} (HOLogic.dest_numeral t')
| num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term_global @{theory} t);
fun fm_of_term vs @{term True} = @{code T}
- | fm_of_term vs @{term False} = @{code T}
+ | fm_of_term vs @{term False} = @{code F}
| fm_of_term vs (@{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = @{code Lt} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
| fm_of_term vs (@{term "op \<le> :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = @{code Le} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
| fm_of_term vs (@{term "op = :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
- | fm_of_term vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) = @{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
+ | fm_of_term vs (@{term "op \<longleftrightarrow> :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) = @{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term "op &"} $ t1 $ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term "op |"} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term "op -->"} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term "Not"} $ t') = @{code NOT} (fm_of_term vs t')
- | fm_of_term vs (Const("Ex", _) $ Term.Abs (xn, xT, p)) =
+ | fm_of_term vs (Const ("Ex", _) $ Abs (xn, xT, p)) =
@{code E} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
- | fm_of_term vs (Const("All", _) $ Term.Abs(xn, xT, p)) =
+ | fm_of_term vs (Const ("All", _) $ Abs (xn, xT, p)) =
@{code A} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
| fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term_global @{theory} t);
@@ -2064,7 +2062,7 @@
| term_of_fm vs (@{code And} (t1, t2)) = HOLogic.conj $ term_of_fm vs t1 $ term_of_fm vs t2
| term_of_fm vs (@{code Or} (t1, t2)) = HOLogic.disj $ term_of_fm vs t1 $ term_of_fm vs t2
| term_of_fm vs (@{code Imp} (t1, t2)) = HOLogic.imp $ term_of_fm vs t1 $ term_of_fm vs t2
- | term_of_fm vs (@{code Iff} (t1, t2)) = @{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $
+ | term_of_fm vs (@{code Iff} (t1, t2)) = @{term "op \<longleftrightarrow> :: bool \<Rightarrow> bool \<Rightarrow> bool"} $
term_of_fm vs t1 $ term_of_fm vs t2
| term_of_fm vs _ = error "If this is raised, Isabelle/HOL or generate_code is inconsistent.";
@@ -2079,4 +2077,22 @@
use "linrtac.ML"
setup LinrTac.setup
+lemma
+ fixes x :: real
+ shows "2 * x \<le> 2 * x \<and> 2 * x \<le> 2 * x + 1"
+apply rferrack
+done
+
+lemma
+ fixes x :: real
+ shows "\<exists>y \<le> x. x = y + 1"
+apply rferrack
+done
+
+lemma
+ fixes x :: real
+ shows "\<not> (\<exists>z. x + z = x + z + 1)"
+apply rferrack
+done
+
end
--- a/src/HOL/Complex/ex/mireif.ML Thu Jul 03 11:16:09 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,125 +0,0 @@
-(* Title: HOL/Complex/ex/mireif.ML
- ID: $Id$
- Author: Amine Chaieb, TU Muenchen
-
-Oracle for Mixed Real-Integer auantifier elimination
-based on the verified code in HOL/Complex/ex/MIR.thy.
-*)
-
-structure ReflectedMir =
-struct
-
-open Mir;
-
-exception MIR;
-
-fun num_of_term vs t =
- case t of
- Free(xn,xT) => (case AList.lookup (op =) vs t of
- NONE => error "Variable not found in the list!"
- | SOME n => Bound n)
- | Const("RealDef.real",_)$ @{term "0::int"} => C 0
- | Const("RealDef.real",_)$ @{term "1::int"} => C 1
- | @{term "0::real"} => C 0
- | @{term "1::real"} => C 1
- | Term.Bound i => Bound (nat i)
- | Const(@{const_name "HOL.uminus"},_)$t' => Neg (num_of_term vs t')
- | Const (@{const_name "HOL.plus"},_)$t1$t2 => Add (num_of_term vs t1,num_of_term vs t2)
- | Const (@{const_name "HOL.minus"},_)$t1$t2 => Sub (num_of_term vs t1,num_of_term vs t2)
- | Const (@{const_name "HOL.times"},_)$t1$t2 =>
- (case (num_of_term vs t1) of C i =>
- Mul (i,num_of_term vs t2)
- | _ => error "num_of_term: unsupported Multiplication")
- | Const("RealDef.real",_)$ (Const (@{const_name "RComplete.floor"},_)$ t') => Floor (num_of_term vs t')
- | Const("RealDef.real",_)$ (Const (@{const_name "RComplete.ceiling"},_)$ t') => Neg(Floor (Neg (num_of_term vs t')))
- | Const("RealDef.real",_) $ Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
- | Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
- | _ => error ("num_of_term: unknown term " ^ Syntax.string_of_term_global Pure.thy t);
-
-
-(* pseudo reification : term -> fm *)
-fun fm_of_term vs t =
- case t of
- Const("True",_) => T
- | Const("False",_) => F
- | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (num_of_term vs t1,num_of_term vs t2))
- | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub (num_of_term vs t1,num_of_term vs t2))
- | Const (@{const_name "MIR.rdvd"},_ )$ (Const("RealDef.real",_) $ (Const(@{const_name "Int.number_of"},_)$t1))$t2 =>
- Dvd (HOLogic.dest_numeral t1, num_of_term vs t2)
- | Const("op =",eqT)$t1$t2 =>
- if (domain_type eqT = @{typ real})
- then Eq (Sub (num_of_term vs t1, num_of_term vs t2))
- else Iff (fm_of_term vs t1, fm_of_term vs t2)
- | Const("op &",_)$t1$t2 => And (fm_of_term vs t1, fm_of_term vs t2)
- | Const("op |",_)$t1$t2 => Or (fm_of_term vs t1, fm_of_term vs t2)
- | Const("op -->",_)$t1$t2 => Imp (fm_of_term vs t1, fm_of_term vs t2)
- | Const("Not",_)$t' => Not (fm_of_term vs t')
- | Const("Ex",_)$Abs(xn,xT,p) =>
- E (fm_of_term (map (fn (v, n) => (v, Suc n)) vs) p)
- | Const("All",_)$Abs(xn,xT,p) =>
- A (fm_of_term (map (fn(v, n) => (v, Suc n)) vs) p)
- | _ => error ("fm_of_term : unknown term!" ^ Syntax.string_of_term_global Pure.thy t);
-
-fun start_vs t =
- let val fs = term_frees t
- in fs ~~ map nat (0 upto (length fs - 1))
- end ;
-
-(* transform num and fm back to terms *)
-
-fun myassoc2 l v =
- case l of
- [] => NONE
- | (x,v')::xs => if v = v' then SOME x
- else myassoc2 xs v;
-
-val realC = @{term "real :: int => _"};
-val rzero = @{term "0::real"};
-
-fun term_of_num vs t =
- case t of
- C i => realC $ (HOLogic.mk_number HOLogic.intT i)
- | Bound n => valOf (myassoc2 vs n)
- | Neg (Floor (Neg t')) => realC $ (@{term "ceiling"} $ term_of_num vs t')
- | Neg t' => @{term "uminus:: real => _"} $ term_of_num vs t'
- | Add(t1,t2) => @{term "op +:: real => _"} $ term_of_num vs t1 $ term_of_num vs t2
- | Sub(t1,t2) => @{term "op -:: real => _"} $ term_of_num vs t1 $ term_of_num vs t2
- | Mul(i,t2) => @{term "op -:: real => _"} $ term_of_num vs (C i) $ term_of_num vs t2
- | Floor t => realC $ (@{term "floor"} $ term_of_num vs t)
- | Cn(n,i,t) => term_of_num vs (Add(Mul(i,Bound n),t))
- | Cf(c,t,s) => term_of_num vs (Add(Mul(c,Floor t),s));
-
-fun term_of_fm vs t =
- case t of
- T => HOLogic.true_const
- | F => HOLogic.false_const
- | Lt t => @{term "op <:: real => _"} $ term_of_num vs t $ rzero
- | Le t => @{term "op <=:: real => _"} $ term_of_num vs t $ rzero
- | Gt t => @{term "op <:: real => _"}$ rzero $ term_of_num vs t
- | Ge t => @{term "op <=:: real => _"} $ rzero $ term_of_num vs t
- | Eq t => @{term "op = :: real => _"}$ term_of_num vs t $ rzero
- | NEq t => term_of_fm vs (Not (Eq t))
- | NDvd (i,t) => term_of_fm vs (Not (Dvd (i,t)))
- | Dvd (i,t) => @{term "op rdvd"} $ term_of_num vs (C i) $ term_of_num vs t
- | Not t' => HOLogic.Not$(term_of_fm vs t')
- | And(t1,t2) => HOLogic.conj $ term_of_fm vs t1 $ term_of_fm vs t2
- | Or(t1,t2) => HOLogic.disj $ term_of_fm vs t1 $ term_of_fm vs t2
- | Imp(t1,t2) => HOLogic.imp $ term_of_fm vs t1 $ term_of_fm vs t2
- | Iff(t1,t2) => HOLogic.mk_eq (term_of_fm vs t1, term_of_fm vs t2)
- | _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
-
-(* The oracle *)
-
-fun mircfr_oracle thy t =
- let
- val vs = start_vs t
- in HOLogic.mk_Trueprop (HOLogic.mk_eq(t, term_of_fm vs (mircfrqe (fm_of_term vs t))))
- end;
-
-fun mirlfr_oracle thy t =
- let
- val vs = start_vs t
- in HOLogic.mk_Trueprop (HOLogic.mk_eq(t, term_of_fm vs (mirlfrqe (fm_of_term vs t))))
- end;
-
-end;
--- a/src/HOL/Complex/ex/mirtac.ML Thu Jul 03 11:16:09 2008 +0200
+++ b/src/HOL/Complex/ex/mirtac.ML Thu Jul 03 11:16:33 2008 +0200
@@ -58,7 +58,7 @@
val ZDIVISION_BY_ZERO_MOD = @{thm "DIVISION_BY_ZERO"} RS conjunct2;
val ZDIVISION_BY_ZERO_DIV = @{thm "DIVISION_BY_ZERO"} RS conjunct1;
-fun prepare_for_mir sg q fm =
+fun prepare_for_mir thy q fm =
let
val ps = Logic.strip_params fm
val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
@@ -92,9 +92,9 @@
THEN (fn st =>
let
val g = List.nth (prems_of st, i - 1)
- val sg = ProofContext.theory_of ctxt
+ val thy = ProofContext.theory_of ctxt
(* Transform the term*)
- val (t,np,nh) = prepare_for_mir sg q g
+ val (t,np,nh) = prepare_for_mir thy q g
(* Some simpsets for dealing with mod div abs and nat*)
val mod_div_simpset = HOL_basic_ss
addsimps [refl,nat_mod_add_eq,
@@ -121,7 +121,7 @@
@{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}]
addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
(* simp rules for elimination of abs *)
- val ct = cterm_of sg (HOLogic.mk_Trueprop t)
+ val ct = cterm_of thy (HOLogic.mk_Trueprop t)
(* Theorem for the nat --> int transformation *)
val pre_thm = Seq.hd (EVERY
[simp_tac mod_div_simpset 1, simp_tac simpset0 1,
@@ -134,8 +134,8 @@
let val pth =
(* If quick_and_dirty then run without proof generation as oracle*)
if !quick_and_dirty
- then mircfr_oracle sg (Pattern.eta_long [] t1)
- else mirlfr_oracle sg (Pattern.eta_long [] t1)
+ then mirfr_oracle thy (false, Pattern.eta_long [] t1)
+ else mirfr_oracle thy (true, Pattern.eta_long [] t1)
in
(trace_msg ("calling procedure with term:\n" ^
Syntax.string_of_term ctxt t1);
@@ -145,7 +145,7 @@
| _ => (pre_thm, assm_tac i)
in (rtac (((mp_step nh) o (spec_step np)) th) i
THEN tac) st
- end handle Subscript => no_tac st | ReflectedMir.MIR => no_tac st);
+ end handle Subscript => no_tac st);
fun mir_args meth =
let val parse_flag =
--- a/src/HOL/IsaMakefile Thu Jul 03 11:16:09 2008 +0200
+++ b/src/HOL/IsaMakefile Thu Jul 03 11:16:33 2008 +0200
@@ -782,7 +782,7 @@
ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy ex/Puzzle.thy \
ex/Quickcheck_Examples.thy ex/Reflection.thy ex/reflection_data.ML \
ex/ReflectionEx.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
- ex/Reflected_Presburger.thy ex/coopertac.ML ex/coopereif.ML \
+ ex/Reflected_Presburger.thy ex/coopertac.ML \
ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \
ex/Sudoku.thy ex/Tarski.thy ex/Unification.thy ex/document/root.bib \
ex/document/root.tex ex/Meson_Test.thy ex/reflection.ML ex/set.thy \
@@ -790,7 +790,7 @@
Complex/ex/BigO_Complex.thy Complex/ex/BinEx.thy \
Complex/ex/NSPrimes.thy Complex/ex/Sqrt.thy \
Complex/ex/Sqrt_Script.thy Complex/ex/MIR.thy Complex/ex/mirtac.ML \
- Complex/ex/mireif.ML Complex/ex/ReflectedFerrack.thy \
+ Complex/ex/ReflectedFerrack.thy \
Complex/ex/linrtac.ML
@$(ISATOOL) usedir $(OUT)/HOL ex
--- a/src/HOL/ex/Reflected_Presburger.thy Thu Jul 03 11:16:09 2008 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy Thu Jul 03 11:16:33 2008 +0200
@@ -1,6 +1,10 @@
+(* Title: HOL/ex/Reflected_Presburger.thy
+ Author: Amine Chaieb
+*)
+
theory Reflected_Presburger
imports Main GCD Efficient_Nat
-uses ("coopereif.ML") ("coopertac.ML")
+uses ("coopertac.ML")
begin
function
@@ -23,25 +27,23 @@
| Mul int num
(* A size for num to make inductive proofs simpler*)
-consts num_size :: "num \<Rightarrow> nat"
-primrec
+primrec num_size :: "num \<Rightarrow> nat" where
"num_size (C c) = 1"
- "num_size (Bound n) = 1"
- "num_size (Neg a) = 1 + num_size a"
- "num_size (Add a b) = 1 + num_size a + num_size b"
- "num_size (Sub a b) = 3 + num_size a + num_size b"
- "num_size (CN n c a) = 4 + num_size a"
- "num_size (Mul c a) = 1 + num_size a"
+| "num_size (Bound n) = 1"
+| "num_size (Neg a) = 1 + num_size a"
+| "num_size (Add a b) = 1 + num_size a + num_size b"
+| "num_size (Sub a b) = 3 + num_size a + num_size b"
+| "num_size (CN n c a) = 4 + num_size a"
+| "num_size (Mul c a) = 1 + num_size a"
-consts Inum :: "int list \<Rightarrow> num \<Rightarrow> int"
-primrec
+primrec Inum :: "int list \<Rightarrow> num \<Rightarrow> int" where
"Inum bs (C c) = c"
- "Inum bs (Bound n) = bs!n"
- "Inum bs (CN n c a) = c * (bs!n) + (Inum bs a)"
- "Inum bs (Neg a) = -(Inum bs a)"
- "Inum bs (Add a b) = Inum bs a + Inum bs b"
- "Inum bs (Sub a b) = Inum bs a - Inum bs b"
- "Inum bs (Mul c a) = c* Inum bs a"
+| "Inum bs (Bound n) = bs!n"
+| "Inum bs (CN n c a) = c * (bs!n) + (Inum bs a)"
+| "Inum bs (Neg a) = -(Inum bs a)"
+| "Inum bs (Add a b) = Inum bs a + Inum bs b"
+| "Inum bs (Sub a b) = Inum bs a - Inum bs b"
+| "Inum bs (Mul c a) = c* Inum bs a"
datatype fm =
T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num|
@@ -177,7 +179,7 @@
using bp numbound0_I[where b="b" and bs="bs" and b'="b'"]
by (induct p rule: bound0.induct) (auto simp add: gr0_conv_Suc)
-fun numsubst0:: "num \<Rightarrow> num \<Rightarrow> num" where
+fun numsubst0:: "num \<Rightarrow> num \<Rightarrow> num" where
"numsubst0 t (C c) = (C c)"
| "numsubst0 t (Bound n) = (if n=0 then t else Bound n)"
| "numsubst0 t (CN 0 i a) = Add (Mul i t) (numsubst0 t a)"
@@ -1898,8 +1900,8 @@
ultimately show ?thesis by blast
qed
-constdefs pa:: "fm \<Rightarrow> fm"
- "pa \<equiv> (\<lambda> p. qelim (prep p) cooper)"
+definition pa :: "fm \<Rightarrow> fm" where
+ "pa p = qelim (prep p) cooper"
theorem mirqe: "(Ifm bbs bs (pa p) = Ifm bbs bs p) \<and> qfree (pa p)"
using qelim_ci cooper prep by (auto simp add: pa_def)
@@ -1911,21 +1913,150 @@
(E (E (Eq (Sub (Add (Mul 3 (Bound 1)) (Mul 5 (Bound 0)))
(Bound 2))))))))"
+ML {* @{code cooper_test} () *}
+
+(*
code_reserved SML oo
-export_code pa cooper_test in SML module_name GeneratedCooper
-(*export_code pa in SML module_name GeneratedCooper file "~~/src/HOL/Tools/Qelim/raw_generated_cooper.ML"*)
+export_code pa in SML module_name GeneratedCooper file "~~/src/HOL/Tools/Qelim/raw_generated_cooper.ML"
+*)
+
+oracle linzqe_oracle ("term") = {*
+let
+
+fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t
+ of NONE => error "Variable not found in the list!"
+ | SOME n => @{code Bound} n)
+ | num_of_term vs @{term "0::int"} = @{code C} 0
+ | num_of_term vs @{term "1::int"} = @{code C} 1
+ | num_of_term vs (@{term "number_of :: int \<Rightarrow> int"} $ t) = @{code C} (HOLogic.dest_numeral t)
+ | num_of_term vs (Bound i) = @{code Bound} i
+ | num_of_term vs (@{term "uminus :: int \<Rightarrow> int"} $ t') = @{code Neg} (num_of_term vs t')
+ | num_of_term vs (@{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) =
+ @{code Add} (num_of_term vs t1, num_of_term vs t2)
+ | num_of_term vs (@{term "op - :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) =
+ @{code Sub} (num_of_term vs t1, num_of_term vs t2)
+ | num_of_term vs (@{term "op * :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) =
+ (case try HOLogic.dest_number t1
+ of SOME (_, i) => @{code Mul} (i, num_of_term vs t2)
+ | NONE => (case try HOLogic.dest_number t2
+ of SOME (_, i) => @{code Mul} (i, num_of_term vs t1)
+ | NONE => error "num_of_term: unsupported multiplication"))
+ | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term_global @{theory} t);
+
+fun fm_of_term ps vs @{term True} = @{code T}
+ | fm_of_term ps vs @{term False} = @{code F}
+ | fm_of_term ps vs (@{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} $ t1 $ t2) =
+ @{code Lt} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
+ | fm_of_term ps vs (@{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"} $ t1 $ t2) =
+ @{code Le} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
+ | fm_of_term ps vs (@{term "op = :: int \<Rightarrow> int \<Rightarrow> bool"} $ t1 $ t2) =
+ @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
+ | fm_of_term ps vs (@{term "op dvd :: int \<Rightarrow> int \<Rightarrow> bool"} $ t1 $ t2) =
+ (case try HOLogic.dest_number t1
+ of SOME (_, i) => @{code Dvd} (i, num_of_term vs t2)
+ | NONE => error "num_of_term: unsupported dvd")
+ | fm_of_term ps vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
+ @{code Iff} (fm_of_term ps vs t1, fm_of_term ps vs t2)
+ | fm_of_term ps vs (@{term "op &"} $ t1 $ t2) =
+ @{code And} (fm_of_term ps vs t1, fm_of_term ps vs t2)
+ | fm_of_term ps vs (@{term "op |"} $ t1 $ t2) =
+ @{code Or} (fm_of_term ps vs t1, fm_of_term ps vs t2)
+ | fm_of_term ps vs (@{term "op -->"} $ t1 $ t2) =
+ @{code Imp} (fm_of_term ps vs t1, fm_of_term ps vs t2)
+ | fm_of_term ps vs (@{term "Not"} $ t') =
+ @{code NOT} (fm_of_term ps vs t')
+ | fm_of_term ps vs (Const ("Ex", _) $ Abs (xn, xT, p)) =
+ let
+ val (xn', p') = variant_abs (xn, xT, p);
+ val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
+ in @{code E} (fm_of_term ps vs' p) end
+ | fm_of_term ps vs (Const ("All", _) $ Abs (xn, xT, p)) =
+ let
+ val (xn', p') = variant_abs (xn, xT, p);
+ val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
+ in @{code A} (fm_of_term ps vs' p) end
+ | fm_of_term ps vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term_global @{theory} t);
-ML {* GeneratedCooper.cooper_test () *}
-use "coopereif.ML"
-oracle linzqe_oracle ("term") = Coopereif.cooper_oracle
+fun term_of_num vs (@{code C} i) = HOLogic.mk_number HOLogic.intT i
+ | term_of_num vs (@{code Bound} n) = fst (the (find_first (fn (_, m) => n = m) vs))
+ | term_of_num vs (@{code Neg} t') = @{term "uminus :: int \<Rightarrow> int"} $ term_of_num vs t'
+ | term_of_num vs (@{code Add} (t1, t2)) = @{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} $
+ term_of_num vs t1 $ term_of_num vs t2
+ | term_of_num vs (@{code Sub} (t1, t2)) = @{term "op - :: int \<Rightarrow> int \<Rightarrow> int"} $
+ term_of_num vs t1 $ term_of_num vs t2
+ | term_of_num vs (@{code Mul} (i, t2)) = @{term "op * :: int \<Rightarrow> int \<Rightarrow> int"} $
+ term_of_num vs (@{code C} i) $ term_of_num vs t2
+ | term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t))
+
+fun term_of_fm ps vs @{code T} = HOLogic.true_const
+ | term_of_fm ps vs @{code F} = HOLogic.false_const
+ | term_of_fm ps vs (@{code Lt} t) =
+ @{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} $ term_of_num vs t $ @{term "0::int"}
+ | term_of_fm ps vs (@{code Le} t) =
+ @{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"} $ term_of_num vs t $ @{term "0::int"}
+ | term_of_fm ps vs (@{code Gt} t) =
+ @{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} $ @{term "0::int"} $ term_of_num vs t
+ | term_of_fm ps vs (@{code Ge} t) =
+ @{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"} $ @{term "0::int"} $ term_of_num vs t
+ | term_of_fm ps vs (@{code Eq} t) =
+ @{term "op = :: int \<Rightarrow> int \<Rightarrow> bool"} $ term_of_num vs t $ @{term "0::int"}
+ | term_of_fm ps vs (@{code NEq} t) =
+ term_of_fm ps vs (@{code NOT} (@{code Eq} t))
+ | term_of_fm ps vs (@{code Dvd} (i, t)) =
+ @{term "op dvd :: int \<Rightarrow> int \<Rightarrow> bool"} $ term_of_num vs (@{code C} i) $ term_of_num vs t
+ | term_of_fm ps vs (@{code NDvd} (i, t)) =
+ term_of_fm ps vs (@{code NOT} (@{code Dvd} (i, t)))
+ | term_of_fm ps vs (@{code NOT} t') =
+ HOLogic.Not $ term_of_fm ps vs t'
+ | term_of_fm ps vs (@{code And} (t1, t2)) =
+ HOLogic.conj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
+ | term_of_fm ps vs (@{code Or} (t1, t2)) =
+ HOLogic.disj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
+ | term_of_fm ps vs (@{code Imp} (t1, t2)) =
+ HOLogic.imp $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
+ | term_of_fm ps vs (@{code Iff} (t1, t2)) =
+ @{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
+ | term_of_fm ps vs (@{code Closed} n) = (fst o the) (find_first (fn (_, m) => m = n) ps)
+ | term_of_fm ps vs (@{code NClosed} n) = term_of_fm ps vs (@{code NOT} (@{code Closed} n))
+
+fun term_bools acc t =
+ let
+ val is_op = member (op =) [@{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
+ @{term "op = :: int => _"}, @{term "op < :: int => _"},
+ @{term "op <= :: int => _"}, @{term "Not"}, @{term "All :: (int => _) => _"},
+ @{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}]
+ fun is_ty t = not (fastype_of t = HOLogic.boolT)
+ in case t
+ of (l as f $ a) $ b => if is_ty t orelse is_op t then term_bools (term_bools acc l)b
+ else insert (op aconv) t acc
+ | f $ a => if is_ty t orelse is_op t then term_bools (term_bools acc f) a
+ else insert (op aconv) t acc
+ | Abs p => term_bools acc (snd (variant_abs p))
+ | _ => if is_ty t orelse is_op t then acc else insert (op aconv) t acc
+ end;
+
+in fn thy => fn t =>
+ let
+ val fs = term_frees t;
+ val bs = term_bools [] t;
+ val vs = fs ~~ (0 upto (length fs - 1))
+ val ps = bs ~~ (0 upto (length bs - 1))
+ val t' = (term_of_fm ps vs o @{code pa} o fm_of_term ps vs) t;
+ in (HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
+end;
+*}
+
use "coopertac.ML"
setup "LinZTac.setup"
- (* Tests *)
+text {* Tests *}
+
lemma "\<exists> (j::int). \<forall> x\<ge>j. (\<exists> a b. x = 3*a+5*b)"
-by cooper
+ by cooper
-lemma "ALL (x::int) >=8. EX i j. 5*i + 3*j = x" by cooper
+lemma "ALL (x::int) >=8. EX i j. 5*i + 3*j = x"
+ by cooper
+
theorem "(\<forall>(y::int). 3 dvd y) ==> \<forall>(x::int). b < x --> a \<le> x"
by cooper
@@ -1940,20 +2071,41 @@
theorem "\<forall>(x::nat). \<exists>(y::nat). (0::nat) \<le> 5 --> y = 5 + x "
by cooper
-lemma "ALL (x::int) >=8. EX i j. 5*i + 3*j = x" by cooper
-lemma "ALL (y::int) (z::int) (n::int). 3 dvd z --> 2 dvd (y::int) --> (EX (x::int). 2*x = y) & (EX (k::int). 3*k = z)" by cooper
-lemma "ALL(x::int) y. x < y --> 2 * x + 1 < 2 * y" by cooper
-lemma "ALL(x::int) y. 2 * x + 1 ~= 2 * y" by cooper
-lemma "EX(x::int) y. 0 < x & 0 <= y & 3 * x - 5 * y = 1" by cooper
-lemma "~ (EX(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)" by cooper
-lemma "ALL(x::int). (2 dvd x) --> (EX(y::int). x = 2*y)" by cooper
-lemma "ALL(x::int). (2 dvd x) --> (EX(y::int). x = 2*y)" by cooper
-lemma "ALL(x::int). (2 dvd x) = (EX(y::int). x = 2*y)" by cooper
-lemma "ALL(x::int). ((2 dvd x) = (ALL(y::int). x ~= 2*y + 1))" by cooper
-lemma "~ (ALL(x::int). ((2 dvd x) = (ALL(y::int). x ~= 2*y+1) | (EX(q::int) (u::int) i. 3*i + 2*q - u < 17) --> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))" by cooper
+lemma "ALL (x::int) >=8. EX i j. 5*i + 3*j = x"
+ by cooper
+
+lemma "ALL (y::int) (z::int) (n::int). 3 dvd z --> 2 dvd (y::int) --> (EX (x::int). 2*x = y) & (EX (k::int). 3*k = z)"
+ by cooper
+
+lemma "ALL(x::int) y. x < y --> 2 * x + 1 < 2 * y"
+ by cooper
+
+lemma "ALL(x::int) y. 2 * x + 1 ~= 2 * y"
+ by cooper
+
+lemma "EX(x::int) y. 0 < x & 0 <= y & 3 * x - 5 * y = 1"
+ by cooper
+
+lemma "~ (EX(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)"
+ by cooper
+
+lemma "ALL(x::int). (2 dvd x) --> (EX(y::int). x = 2*y)"
+ by cooper
+
+lemma "ALL(x::int). (2 dvd x) = (EX(y::int). x = 2*y)"
+ by cooper
+
+lemma "ALL(x::int). ((2 dvd x) = (ALL(y::int). x ~= 2*y + 1))"
+ by cooper
+
+lemma "~ (ALL(x::int). ((2 dvd x) = (ALL(y::int). x ~= 2*y+1) | (EX(q::int) (u::int) i. 3*i + 2*q - u < 17) --> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))"
+ by cooper
+
lemma "~ (ALL(i::int). 4 <= i --> (EX x y. 0 <= x & 0 <= y & 3 * x + 5 * y = i))"
by cooper
-lemma "EX j. ALL (x::int) >= j. EX i j. 5*i + 3*j = x" by cooper
+
+lemma "EX j. ALL (x::int) >= j. EX i j. 5*i + 3*j = x"
+ by cooper
theorem "(\<forall>(y::int). 3 dvd y) ==> \<forall>(x::int). b < x --> a \<le> x"
by cooper
--- a/src/HOL/ex/coopereif.ML Thu Jul 03 11:16:09 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,121 +0,0 @@
-(* ID: $Id$
- Author: Amine Chaieb, TU Muenchen
-
-Reification for the automatically generated oracle for Presburger arithmetic
-in HOL/ex/Reflected_Presburger.thy.
-*)
-
-structure Coopereif =
-struct
-
-open GeneratedCooper;
-
-fun i_of_term vs t = case t
- of Free(xn,xT) => (case AList.lookup (op aconv) vs t
- of NONE => error "Variable not found in the list!"
- | SOME n => Bound n)
- | @{term "0::int"} => C 0
- | @{term "1::int"} => C 1
- | Term.Bound i => Bound 0
- | Const(@{const_name "HOL.uminus"},_)$t' => Neg (i_of_term vs t')
- | Const(@{const_name "HOL.plus"},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
- | Const(@{const_name "HOL.minus"},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
- | Const(@{const_name "HOL.times"},_)$t1$t2 => (Mul (HOLogic.dest_number t1 |> snd,i_of_term vs t2)
- handle TERM _ =>
- (Mul (HOLogic.dest_number t2 |> snd,i_of_term vs t1)
- handle TERM _ => error "i_of_term: Unsupported kind of multiplication"))
- | _ => (C (HOLogic.dest_number t |> snd)
- handle TERM _ => error "i_of_term: unknown term");
-
-fun qf_of_term ps vs t = case t
- of Const("True",_) => T
- | Const("False",_) => F
- | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
- | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
- | Const(@{const_name "Divides.dvd"},_)$t1$t2 =>
- (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => error "qf_of_term: unsupported dvd")
- | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
- | @{term "op = :: bool => _ "}$t1$t2 => Iff(qf_of_term ps vs t1,qf_of_term ps vs t2)
- | Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2)
- | Const("op |",_)$t1$t2 => Or(qf_of_term ps vs t1,qf_of_term ps vs t2)
- | Const("op -->",_)$t1$t2 => Imp(qf_of_term ps vs t1,qf_of_term ps vs t2)
- | Const("Not",_)$t' => Not(qf_of_term ps vs t')
- | Const("Ex",_)$Abs(xn,xT,p) =>
- let val (xn',p') = variant_abs (xn,xT,p)
- val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1 + n)) vs)
- in E (qf_of_term ps vs' p')
- end
- | Const("All",_)$Abs(xn,xT,p) =>
- let val (xn',p') = variant_abs (xn,xT,p)
- val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1 + n)) vs)
- in A (qf_of_term ps vs' p')
- end
- | _ =>(case AList.lookup (op aconv) ps t of
- NONE => error "qf_of_term ps : unknown term!"
- | SOME n => Closed n);
-
-local
- val ops = [@{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
- @{term "op = :: int => _"}, @{term "op < :: int => _"},
- @{term "op <= :: int => _"}, @{term "Not"}, @{term "All:: (int => _) => _"},
- @{term "Ex:: (int => _) => _"}, @{term "True"}, @{term "False"}]
- fun ty t = Bool.not (fastype_of t = HOLogic.boolT)
-in
-
-fun term_bools acc t = case t
- of (l as f $ a) $ b => if ty t orelse f mem ops then term_bools (term_bools acc l)b
- else insert (op aconv) t acc
- | f $ a => if ty t orelse f mem ops then term_bools (term_bools acc f) a
- else insert (op aconv) t acc
- | Abs p => term_bools acc (snd (variant_abs p))
- | _ => if ty t orelse t mem ops then acc else insert (op aconv) t acc
-
-end;
-
-fun start_vs t =
- let
- val fs = term_frees t
- val ps = term_bools [] t
- in
- (fs ~~ (0 upto (length fs - 1)), ps ~~ (0 upto (length ps - 1)))
- end;
-
-fun term_of_i vs t = case t
- of C i => HOLogic.mk_number HOLogic.intT i
- | Bound n => (fst o the) (find_first (fn (_, m) => m = n) vs)
- | Neg t' => @{term "uminus :: int => _"} $ term_of_i vs t'
- | Add (t1, t2) => @{term "op +:: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
- | Sub (t1, t2) => Const (@{const_name "HOL.minus"}, HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $
- term_of_i vs t1 $ term_of_i vs t2
- | Mul (i, t2) => Const (@{const_name "HOL.times"}, HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $
- HOLogic.mk_number HOLogic.intT i $ term_of_i vs t2
- | Cn (n,i, t') => term_of_i vs (Add (Mul (i, Bound n), t'));
-
-fun term_of_qf ps vs t = case t
- of T => HOLogic.true_const
- | F => HOLogic.false_const
- | Lt t' => @{term "op < :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
- | Le t' => @{term "op <= :: int => _ "}$ term_of_i vs t' $ @{term "0::int"}
- | Gt t' => @{term "op < :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
- | Ge t' => @{term "op <= :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
- | Eq t' => @{term "op = :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
- | NEq t' => term_of_qf ps vs (Not(Eq t'))
- | Dvd(i,t') => @{term "op dvd :: int => _ "}$
- (HOLogic.mk_number HOLogic.intT i)$(term_of_i vs t')
- | NDvd(i,t')=> term_of_qf ps vs (Not(Dvd(i,t')))
- | Not t' => HOLogic.Not$(term_of_qf ps vs t')
- | And(t1,t2) => HOLogic.conj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
- | Or(t1,t2) => HOLogic.disj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
- | Imp(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
- | Iff(t1,t2) => HOLogic.eq_const HOLogic.boolT $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
- | Closed n => (fst o the) (find_first (fn (_, m) => m = n) ps)
- | NClosed n => term_of_qf ps vs (Not (Closed n))
- | _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
-
-(* The oracle *)
-fun cooper_oracle thy t =
- let
- val (vs, ps) = start_vs t;
- in HOLogic.mk_Trueprop (HOLogic.mk_eq (t, term_of_qf ps vs (pa (qf_of_term ps vs t)))) end;
-
-end;
\ No newline at end of file