# HG changeset patch # User haftmann # Date 1184874465 -7200 # Node ID 5500610fe1e534b24e34596268dfa9fd9c2ea342 # Parent ad26287a9ccb25d2b37172a24c67b65ca27fb884 adapted to new code generator framework diff -r ad26287a9ccb -r 5500610fe1e5 src/HOL/Complex/ex/MIR.thy --- a/src/HOL/Complex/ex/MIR.thy Thu Jul 19 21:47:44 2007 +0200 +++ b/src/HOL/Complex/ex/MIR.thy Thu Jul 19 21:47:45 2007 +0200 @@ -5,7 +5,7 @@ header {* Quatifier elimination for R(0,1,+,floor,<) *} theory MIR - imports Real GCD + imports Real GCD Pretty_Int uses ("mireif.ML") ("mirtac.ML") begin @@ -106,8 +106,10 @@ qed (* The Divisibility relation between reals *) -consts rdvd:: "real \ real \ bool" (infixl 50) -defs rdvd_def: "x rdvd y \ \ (k::int). y=x*(real k)" +definition + rdvd:: "real \ real \ bool" (infixl "rdvd" 50) +where + rdvd_def: "x rdvd y \ (\k\int. y = x * real k)" lemma int_rdvd_real: shows "real (i::int) rdvd x = (i dvd (floor x) \ real (floor x) = x)" (is "?l = ?r") @@ -637,10 +639,8 @@ "lex_bnd t s \ lex_ns (bnds t, bnds s)" consts - numgcd :: "num \ int" numgcdh:: "num \ int \ int" reducecoeffh:: "num \ int \ num" - reducecoeff :: "num \ num" dvdnumcoeff:: "num \ int \ bool" consts maxcoeff:: "num \ int" recdef maxcoeff "measure size" @@ -658,7 +658,11 @@ "numgcdh (CN n c t) = (\g. igcd c (numgcdh t g))" "numgcdh (CF c s t) = (\g. igcd c (numgcdh t g))" "numgcdh t = (\g. 1)" -defs numgcd_def: "numgcd t \ numgcdh t (maxcoeff t)" + +definition + numgcd :: "num \ int" +where + numgcd_def: "numgcd t = numgcdh t (maxcoeff t)" recdef reducecoeffh "measure size" "reducecoeffh (C i) = (\ g. C (i div g))" @@ -666,7 +670,10 @@ "reducecoeffh (CF c s t) = (\ g. CF (c div g) s (reducecoeffh t g))" "reducecoeffh t = (\g. t)" -defs reducecoeff_def: "reducecoeff t \ +definition + reducecoeff :: "num \ num" +where + reducecoeff_def: "reducecoeff t = (let g = numgcd t in if g = 0 then C 0 else if g=1 then t else reducecoeffh t g)" @@ -832,7 +839,6 @@ simpnum:: "num \ num" numadd:: "num \ num \ num" nummul:: "num \ int \ num" - numfloor:: "num \ num" recdef numadd "measure (\ (t,s). size t + size s)" "numadd (CN n1 c1 r1,CN n2 c2 r2) = @@ -939,7 +945,10 @@ lemma split_int_nb: "numbound0 t \ numbound0 (fst (split_int t)) \ numbound0 (snd (split_int t)) " by (induct t rule: split_int.induct, auto simp add: Let_def split_def) -defs numfloor_def: "numfloor t \ (let (tv,ti) = split_int t in +definition + numfloor:: "num \ num" +where + numfloor_def: "numfloor t = (let (tv,ti) = split_int t in (case tv of C i \ numadd (tv,ti) | _ \ numadd(CF 1 tv (C 0),ti)))" @@ -3884,25 +3893,40 @@ with rsplit_ex fnsS fx show "?I x (rsplit f a)" by auto qed -consts +definition lt :: "int \ num \ fm" - le :: "int \ num \ fm" - gt :: "int \ num \ fm" - ge :: "int \ num \ fm" - eq :: "int \ num \ fm" - neq :: "int \ num \ fm" - -defs lt_def: "lt c t \ (if c = 0 then (Lt t) else if c > 0 then (Lt (CN 0 c t)) +where + lt_def: "lt c t = (if c = 0 then (Lt t) else if c > 0 then (Lt (CN 0 c t)) else (Gt (CN 0 (-c) (Neg t))))" -defs le_def: "le c t \ (if c = 0 then (Le t) else if c > 0 then (Le (CN 0 c t)) + +definition + le :: "int \ num \ fm" +where + le_def: "le c t = (if c = 0 then (Le t) else if c > 0 then (Le (CN 0 c t)) else (Ge (CN 0 (-c) (Neg t))))" -defs gt_def: "gt c t \ (if c = 0 then (Gt t) else if c > 0 then (Gt (CN 0 c t)) + +definition + gt :: "int \ num \ fm" +where + gt_def: "gt c t = (if c = 0 then (Gt t) else if c > 0 then (Gt (CN 0 c t)) else (Lt (CN 0 (-c) (Neg t))))" -defs ge_def: "ge c t \ (if c = 0 then (Ge t) else if c > 0 then (Ge (CN 0 c t)) + +definition + ge :: "int \ num \ fm" +where + ge_def: "ge c t = (if c = 0 then (Ge t) else if c > 0 then (Ge (CN 0 c t)) else (Le (CN 0 (-c) (Neg t))))" -defs eq_def: "eq c t \ (if c = 0 then (Eq t) else if c > 0 then (Eq (CN 0 c t)) + +definition + eq :: "int \ num \ fm" +where + eq_def: "eq c t = (if c = 0 then (Eq t) else if c > 0 then (Eq (CN 0 c t)) else (Eq (CN 0 (-c) (Neg t))))" -defs neq_def: "neq c t \ (if c = 0 then (NEq t) else if c > 0 then (NEq (CN 0 c t)) + +definition + neq :: "int \ num \ fm" +where + neq_def: "neq c t = (if c = 0 then (NEq t) else if c > 0 then (NEq (CN 0 c t)) else (NEq (CN 0 (-c) (Neg t))))" lemma lt_mono: "\ a n s. Inum (x#bs) a = Inum (x#bs) (CN 0 n s) \ numbound0 s \ Ifm (x#bs) (lt n s) = Ifm (x#bs) (Lt a)" @@ -3973,12 +3997,6 @@ by (rule rsplit_l[where f="neq" and a="a"], auto simp add: neq_def) (case_tac s, simp_all, case_tac"nat", simp_all) -consts - DVD :: "int \ int \ num \ fm" - DVDJ:: "int \ int \ num \ fm" - NDVD :: "int \ int \ num \ fm" - NDVDJ:: "int \ int \ num \ fm" - lemma small_le: assumes u0:"0 \ u" and u1: "u < 1" shows "(-u \ real (n::int)) = (0 \ n)" @@ -4017,8 +4035,15 @@ finally show ?thesis . qed -defs DVDJ_def: "DVDJ i n s \ (foldr disj (map (\ j. conj (Eq (CN 0 n (Add s (Sub (Floor (Neg s)) (C j))))) (Dvd i (Sub (C j) (Floor (Neg s))))) (iupt(0,n - 1))) F)" -defs NDVDJ_def: "NDVDJ i n s \ (foldr conj (map (\ j. disj (NEq (CN 0 n (Add s (Sub (Floor (Neg s)) (C j))))) (NDvd i (Sub (C j) (Floor (Neg s))))) (iupt(0,n - 1))) T)" +definition + DVDJ:: "int \ int \ num \ fm" +where + DVDJ_def: "DVDJ i n s = (foldr disj (map (\ j. conj (Eq (CN 0 n (Add s (Sub (Floor (Neg s)) (C j))))) (Dvd i (Sub (C j) (Floor (Neg s))))) (iupt(0,n - 1))) F)" + +definition + NDVDJ:: "int \ int \ num \ fm" +where + NDVDJ_def: "NDVDJ i n s = (foldr conj (map (\ j. disj (NEq (CN 0 n (Add s (Sub (Floor (Neg s)) (C j))))) (NDvd i (Sub (C j) (Floor (Neg s))))) (iupt(0,n - 1))) T)" lemma DVDJ_DVD: assumes xp:"x\ 0" and x1: "x < 1" and np:"real n > 0" @@ -4077,10 +4102,17 @@ from NDVDJ_def foldr_And_map_rlfm2[OF th] show ?thesis by auto qed -defs DVD_def: "DVD i c t \ +definition + DVD :: "int \ int \ num \ fm" +where + DVD_def: "DVD i c t = (if i=0 then eq c t else if c = 0 then (Dvd i t) else if c >0 then DVDJ (abs i) c t else DVDJ (abs i) (-c) (Neg t))" -defs NDVD_def: "NDVD i c t \ + +definition + NDVD :: "int \ int \ num \ fm" +where + "NDVD i c t = (if i=0 then neq c t else if c = 0 then (NDvd i t) else if c >0 then NDVDJ (abs i) c t else NDVDJ (abs i) (-c) (Neg t))" @@ -5750,32 +5782,42 @@ declare zdvd_iff_zmod_eq_0 [code] declare max_def [code unfold] -code_module Mir -file "mir.ML" -contains - mircfrqe = "mircfrqe" - mirlfrqe = "mirlfrqe" - test = "%x . mircfrqe (A (And (Le (Sub (Floor (Bound 0)) (Bound 0))) (Le (Add (Bound 0) (Floor (Neg (Bound 0)))))))" - test2 = "%x . mircfrqe (A (Iff (Eq (Add (Floor (Bound 0)) (Floor (Neg (Bound 0))))) (Eq (Sub (Floor (Bound 0)) (Bound 0)))))" - test' = "%x . mirlfrqe (A (And (Le (Sub (Floor (Bound 0)) (Bound 0))) (Le (Add (Bound 0) (Floor (Neg (Bound 0)))))))" - test2' = "%x . mirlfrqe (A (Iff (Eq (Add (Floor (Bound 0)) (Floor (Neg (Bound 0))))) (Eq (Sub (Floor (Bound 0)) (Bound 0)))))" -test3 = "%x .mircfrqe (A(E(And (Ge(Sub (Bound 1) (Bound 0))) (Eq (Add (Floor (Bound 1)) (Floor (Neg(Bound 0))))))))" - -ML {* use "mir.ML" *} +definition + "test1 (u\unit) = mircfrqe (A (And (Le (Sub (Floor (Bound 0)) (Bound 0))) (Le (Add (Bound 0) (Floor (Neg (Bound 0)))))))" + +definition + "test2 (u\unit) = mircfrqe (A (Iff (Eq (Add (Floor (Bound 0)) (Floor (Neg (Bound 0))))) (Eq (Sub (Floor (Bound 0)) (Bound 0)))))" + +definition + "test3 (u\unit) = mirlfrqe (A (And (Le (Sub (Floor (Bound 0)) (Bound 0))) (Le (Add (Bound 0) (Floor (Neg (Bound 0)))))))" + +definition + "test4 (u\unit) = mirlfrqe (A (Iff (Eq (Add (Floor (Bound 0)) (Floor (Neg (Bound 0))))) (Eq (Sub (Floor (Bound 0)) (Bound 0)))))" + +definition + "test5 (u\unit) = mircfrqe (A(E(And (Ge(Sub (Bound 1) (Bound 0))) (Eq (Add (Floor (Bound 1)) (Floor (Neg(Bound 0))))))))" + +code_gen mircfrqe mirlfrqe test1 test2 test3 test4 test5 + in SML to Mir + +code_gen mircfrqe mirlfrqe in SML to Mir file "raw_mir.ML" + ML "set Toplevel.timing" -ML "Mir.test ()" +ML "Mir.test1 ()" ML "Mir.test2 ()" -ML "Mir.test' ()" -ML "Mir.test2' ()" ML "Mir.test3 ()" +ML "Mir.test4 ()" +ML "Mir.test5 ()" +ML "reset Toplevel.timing" use "mireif.ML" oracle mircfr_oracle ("term") = ReflectedMir.mircfr_oracle oracle mirlfr_oracle ("term") = ReflectedMir.mirlfr_oracle -use"mirtac.ML" +use "mirtac.ML" setup "MirTac.setup" ML "set Toplevel.timing" + lemma "ALL (x::real). (\x\ = \x\ = (x = real \x\))" apply mir done @@ -5788,10 +5830,10 @@ apply mir done - lemma "ALL (x::real). \y \ x. (\x\ = \y\)" apply mir done + ML "reset Toplevel.timing" end diff -r ad26287a9ccb -r 5500610fe1e5 src/HOL/Complex/ex/mireif.ML --- a/src/HOL/Complex/ex/mireif.ML Thu Jul 19 21:47:44 2007 +0200 +++ b/src/HOL/Complex/ex/mireif.ML Thu Jul 19 21:47:45 2007 +0200 @@ -1,6 +1,9 @@ -(* - The oracle for Mixed Real-Integer auantifier elimination - based on the verified Code in ~/work/MIR/MIR.thy +(* 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 = @@ -10,20 +13,11 @@ exception MIR; -(* pseudo reification : term -> intterm *) -val iT = HOLogic.intT; -val rT = Type ("RealDef.real",[]); -val bT = HOLogic.boolT; -val realC = @{term "real :: int => _"}; -val floorC = @{term "floor"}; -val ceilC = @{term "ceiling"}; -val rzero = @{term "0::real"}; - 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) + 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 @@ -33,99 +27,99 @@ | 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") + (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 "Numeral.number_of"},_)$t' => C (HOLogic.dest_numeral t') | Const (@{const_name "Numeral.number_of"},_)$t' => C (HOLogic.dest_numeral t') | _ => error ("num_of_term: unknown term " ^ (Display.raw_string_of_term t)); - + (* pseudo reification : term -> fm *) fun fm_of_term vs t = case t of - Const("True",_) => T + Const("True",_) => T | Const("False",_) => F - | Const(@{const_name "Orderings.less"},_)$t1$t2 => Lt (Sub (num_of_term vs t1,num_of_term vs t2)) - | Const(@{const_name "Orderings.less_eq"},_)$t1$t2 => Le (Sub (num_of_term vs t1,num_of_term vs t2)) - | Const (@{const_name "MIR.op rdvd"},_)$(Const("RealDef.real",_)$(Const(@{const_name "Numeral.number_of"},_)$t1))$t2 => - Dvd(HOLogic.dest_numeral t1,num_of_term vs t2) + | Const(@{const_name "Orderings.less"},_)$t1$t2 => Lta (Sub (num_of_term vs t1,num_of_term vs t2)) + | Const(@{const_name "Orderings.less_eq"},_)$t1$t2 => Lea (Sub (num_of_term vs t1,num_of_term vs t2)) + | Const (@{const_name "MIR.rdvd"},_ )$ (Const("RealDef.real",_) $ (Const(@{const_name "Numeral.number_of"},_)$t1))$t2 => + Dvda (HOLogic.dest_numeral t1, num_of_term vs t2) | Const("op =",eqT)$t1$t2 => - if (domain_type eqT = rT) - 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') + if (domain_type eqT = @{typ real}) + then Eqa (Sub (num_of_term vs t1, num_of_term vs t2)) + else Iffa (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 => Impa (fm_of_term vs t1, fm_of_term vs t2) + | Const("Not",_)$t' => Nota (fm_of_term vs t') | Const("Ex",_)$Abs(xn,xT,p) => - E(fm_of_term (map (fn(v,n) => (v,Suc n)) vs) 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!" ^ (Display.raw_string_of_term t)); - -fun zip [] [] = [] - | zip (x::xs) (y::ys) = (x,y)::(zip xs ys); - + A (fm_of_term (map (fn(v, n) => (v, Suc n)) vs) p) + | _ => error ("fm_of_term : unknown term!" ^ Display.raw_string_of_term t); fun start_vs t = let val fs = term_frees t - in zip fs (map nat (0 upto (length fs - 1))) + 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 + [] => NONE | (x,v')::xs => if v = v' then SOME x - else myassoc2 xs v; + 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) + C i => realC $ (HOLogic.mk_number HOLogic.intT i) | Bound n => valOf (myassoc2 vs n) - | Neg (Floor (Neg t')) => realC $ (ceilC $ (term_of_num vs t')) + | 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 $ (floorC $ (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)); + | 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 + 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') + | Lta t => @{term "op <:: real => _"} $ term_of_num vs t $ rzero + | Lea t => @{term "op <=:: real => _"} $ term_of_num vs t $ rzero + | Gta t => @{term "op <:: real => _"}$ rzero $ term_of_num vs t + | Gea t => @{term "op <=:: real => _"} $ rzero $ term_of_num vs t + | Eqa t => @{term "op = :: real => _"}$ term_of_num vs t $ rzero + | NEq t => term_of_fm vs (Nota (Eqa t)) + | NDvd (i,t) => term_of_fm vs (Nota (Dvda (i,t))) + | Dvda (i,t) => @{term "op rdvd"} $ term_of_num vs (C i) $ term_of_num vs t + | Nota 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.eq_const bT $ term_of_fm vs t1 $ term_of_fm vs t2 + | Impa(t1,t2) => HOLogic.imp $ term_of_fm vs t1 $ term_of_fm vs t2 + | Iffa(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 + 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 + 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; diff -r ad26287a9ccb -r 5500610fe1e5 src/HOL/Complex/ex/mirtac.ML --- a/src/HOL/Complex/ex/mirtac.ML Thu Jul 19 21:47:44 2007 +0200 +++ b/src/HOL/Complex/ex/mirtac.ML Thu Jul 19 21:47:45 2007 +0200 @@ -1,3 +1,8 @@ +(* Title: HOL/Complex/ex/mirtac.ML + ID: $Id$ + Author: Amine Chaieb, TU Muenchen +*) + structure MirTac = struct