# HG changeset patch # User haftmann # Date 1183050578 -7200 # Node ID 3e7f62e68fe43337f7753f7d827f608158590d50 # Parent 25e69e56355d83feebf6a7814f3fd3e0bbead3f2 new code generator framework diff -r 25e69e56355d -r 3e7f62e68fe4 src/HOL/Complex/ex/ReflectedFerrack.thy --- a/src/HOL/Complex/ex/ReflectedFerrack.thy Thu Jun 28 19:09:36 2007 +0200 +++ b/src/HOL/Complex/ex/ReflectedFerrack.thy Thu Jun 28 19:09:38 2007 +0200 @@ -482,7 +482,7 @@ "numgcdh (C i) = (\g. igcd i g)" "numgcdh (CN n c t) = (\g. igcd c (numgcdh t g))" "numgcdh t = (\g. 1)" -defs numgcd_def: "numgcd t \ numgcdh t (maxcoeff t)" +defs numgcd_def [code func]: "numgcd t \ numgcdh t (maxcoeff t)" recdef reducecoeffh "measure size" "reducecoeffh (C i) = (\ g. C (i div g))" @@ -1008,26 +1008,41 @@ qed(auto simp add: Let_def split_def ring_simps , simp add: right_distrib[symmetric]) (* Linearize a formula*) -consts +definition lt :: "int \ num \ fm" +where + "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))))" + +definition le :: "int \ num \ fm" +where + "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))))" + +definition gt :: "int \ num \ fm" - ge :: "int \ num \ fm" - eq :: "int \ num \ fm" - neq :: "int \ num \ fm" +where + "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 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)) - 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)) - 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)) - 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)) - 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)) - else (NEq (CN 0 (-c) (Neg t))))" +definition + ge :: "int \ num \ fm" +where + "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))))" + +definition + eq :: "int \ num \ fm" +where + "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))))" + +definition + neq :: "int \ num \ fm" +where + "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: "numnoabs t \ Ifm bs (split lt (rsplit0 t)) = Ifm bs (Lt t) \ isrlfm (split lt (rsplit0 t))" using rsplit0[where bs = "bs" and t="t"] @@ -1972,17 +1987,26 @@ using ferrack qelim_ci prep unfolding linrqe_def by auto -code_module Ferrack -file "generated_ferrack.ML" -contains linrqe = "linrqe" -test = "%x . linrqe (A(A(Imp (Lt(Sub (Bound 1) (Bound 0))) (E(Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))" +definition + ferrack_test :: "unit \ fm" +where + "ferrack_test u = linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0))) + (E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))" + +code_gen linrqe ferrack_test in SML -ML{* use "generated_ferrack.ML"*} -ML "Ferrack.test ()" +ML {* structure Ferrack = struct open ROOT end *} +(*code_module Ferrack + contains + linrqe = linrqe + test = ferrack_test*) + +ML {* Ferrack.ReflectedFerrack.ferrack_test () *} + +code_gen linrqe ferrack_test in SML file "~~/../../gen_code/ferrack.ML" use "linreif.ML" oracle linr_oracle ("term") = ReflectedFerrack.linrqe_oracle - use"linrtac.ML" setup "LinrTac.setup" diff -r 25e69e56355d -r 3e7f62e68fe4 src/HOL/Complex/ex/linreif.ML --- a/src/HOL/Complex/ex/linreif.ML Thu Jun 28 19:09:36 2007 +0200 +++ b/src/HOL/Complex/ex/linreif.ML Thu Jun 28 19:09:38 2007 +0200 @@ -1,12 +1,15 @@ -(* - The oracle for Mixed Real-Integer auantifier elimination - based on the verified Code in ~/work/MIR/MIR.thy +(* ID: $Id$ + Author: Amine Chaieb, TU Muenchen + +The oracle for Mixed Real-Integer auantifier elimination +based on the verified Code in ~/work/MIR/MIR.thy. *) structure ReflectedFerrack = struct open Ferrack; +open ReflectedFerrack exception LINR; @@ -20,13 +23,13 @@ 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!!" + 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 "0::real"} => C 1 - | Term.Bound i => Bound (nat i) + | Term.Bound i => Bound (Integer.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) @@ -44,16 +47,16 @@ case t of 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 "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("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) + 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 => Imp(fm_of_term vs t1,fm_of_term vs t2) - | Const("Not",_)$t' => NOT(fm_of_term vs t') + | 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",_)$Term.Abs(xn,xT,p) => E(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p) | Const("All",_)$Term.Abs(xn,xT,p) => @@ -66,7 +69,7 @@ fun start_vs t = let val fs = term_frees t - in zip fs (map nat (0 upto (length fs - 1))) + in zip fs (map Integer.nat (0 upto (length fs - 1))) end ; (* transform num and fm back to terms *) @@ -88,28 +91,28 @@ (term_of_num vs t1)$(term_of_num vs t2) | Mul(i,t2) => Const(@{const_name "HOL.times"},[rT,rT] ---> rT)$ (term_of_num vs (C i))$(term_of_num vs t2) - | CN(n,i,t) => term_of_num vs (Add (Mul(i,Bound n),t)); + | Cn(n,i,t) => term_of_num vs (Add (Mul(i,Bound n),t)); fun term_of_fm vs t = case t of T => HOLogic.true_const | F => HOLogic.false_const - | Lt t => Const(@{const_name "Orderings.less"},[rT,rT] ---> bT)$ + | Lta t => Const(@{const_name "Orderings.less"},[rT,rT] ---> bT)$ (term_of_num vs t)$ rzero - | Le t => Const(@{const_name "Orderings.less_eq"},[rT,rT] ---> bT)$ + | Lea t => Const(@{const_name "Orderings.less_eq"},[rT,rT] ---> bT)$ (term_of_num vs t)$ rzero - | Gt t => Const(@{const_name "Orderings.less"},[rT,rT] ---> bT)$ + | Gta t => Const(@{const_name "Orderings.less"},[rT,rT] ---> bT)$ rzero $(term_of_num vs t) - | Ge t => Const(@{const_name "Orderings.less_eq"},[rT,rT] ---> bT)$ + | Gea t => Const(@{const_name "Orderings.less_eq"},[rT,rT] ---> bT)$ rzero $(term_of_num vs t) - | Eq t => Const("op =",[rT,rT] ---> bT)$ + | Eqa t => Const("op =",[rT,rT] ---> bT)$ (term_of_num vs t)$ rzero - | NEq t => term_of_fm vs (NOT (Eq t)) - | NOT t' => HOLogic.Not$(term_of_fm vs t') + | NEq t => term_of_fm vs (Nota (Eqa 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)$ + | Impa(t1,t2) => HOLogic.imp$(term_of_fm vs t1)$(term_of_fm vs t2) + | Iffa(t1,t2) => (HOLogic.eq_const bT)$(term_of_fm vs t1)$ (term_of_fm vs t2) | _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!"; @@ -120,4 +123,5 @@ val vs = start_vs t in HOLogic.mk_Trueprop (HOLogic.mk_eq(t, term_of_fm vs (linrqe (fm_of_term vs t)))) end; + end; diff -r 25e69e56355d -r 3e7f62e68fe4 src/HOL/ex/Reflected_Presburger.thy --- a/src/HOL/ex/Reflected_Presburger.thy Thu Jun 28 19:09:36 2007 +0200 +++ b/src/HOL/ex/Reflected_Presburger.thy Thu Jun 28 19:09:38 2007 +0200 @@ -1,5 +1,5 @@ theory Reflected_Presburger -imports GCD Main EfficientNat +imports GCD EfficientNat uses ("coopereif.ML") ("coopertac.ML") begin @@ -1902,18 +1902,21 @@ theorem mirqe: "(Ifm bbs bs (pa p) = Ifm bbs bs p) \ qfree (pa p)" using qelim_ci cooper prep by (auto simp add: pa_def) -declare zdvd_iff_zmod_eq_0 [code] -code_module GeneratedCooper -file "generated_cooper.ML" -contains pa = "pa" -test = "%x . pa (E(A(Imp (Ge (Sub (Bound 0) (Bound 1))) (E(E(Eq(Sub(Add(Mul 3 (Bound 1)) (Mul 5 (Bound 0))) (Bound 2))))))))" +definition + cooper_test :: "unit \ fm" +where + "cooper_test u = pa (E (A (Imp (Ge (Sub (Bound 0) (Bound 1))) + (E (E (Eq (Sub (Add (Mul 3 (Bound 1)) (Mul 5 (Bound 0))) + (Bound 2))))))))" -ML{* use "generated_cooper.ML"; - GeneratedCooper.test (); *} +code_gen pa cooper_test in SML + +ML {* structure GeneratedCooper = struct open ROOT end *} +ML {* GeneratedCooper.Reflected_Presburger.cooper_test () *} use "coopereif.ML" oracle linzqe_oracle ("term") = Coopereif.cooper_oracle -use"coopertac.ML" +use "coopertac.ML" setup "LinZTac.setup" (* Tests *) diff -r 25e69e56355d -r 3e7f62e68fe4 src/HOL/ex/coopereif.ML --- a/src/HOL/ex/coopereif.ML Thu Jun 28 19:09:36 2007 +0200 +++ b/src/HOL/ex/coopereif.ML Thu Jun 28 19:09:38 2007 +0200 @@ -1,56 +1,54 @@ -(* $Id$ *) +(* ID: $Id$ + Author: Amine Chaieb, TU Muenchen -(* Reification for the autimatically generated oracle for Presburger arithmetic - in HOL/ex/Reflected_Presburger.thy - Author : Amine Chaieb +Reification for the automatically generated oracle for Presburger arithmetic +in HOL/ex/Reflected_Presburger.thy. *) structure Coopereif = struct open GeneratedCooper; +open Reflected_Presburger; -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 (nat i) - | 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) +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 (Integer.nat i) + | 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 + | _ => (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 "Orderings.less"},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2)) | Const(@{const_name "Orderings.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") + (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) + | @{term "op = :: bool => _ "}$t1$t2 => Iffa(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("op -->",_)$t1$t2 => Impa(qf_of_term ps vs t1,qf_of_term ps vs t2) + | Const("Not",_)$t' => Nota(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), nat 0) :: (map (fn(v,n) => (v,1 + n)) vs) + val vs' = (Free (xn',xT), Integer.nat 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), nat 0) :: (map (fn(v,n) => (v,1 + n)) vs) + val vs' = (Free (xn',xT), Integer.nat 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 @@ -58,77 +56,68 @@ | 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) + 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 + +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 + 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 ~~ (map nat (0 upto (length fs - 1))), - ps ~~ (map nat (0 upto (length ps - 1)))) -end ; + let + val fs = term_frees t + val ps = term_bools [] t + in + (fs ~~ (map Integer.nat (0 upto (length fs - 1))), + ps ~~ (map Integer.nat (0 upto (length ps - 1)))) + end; -val iT = HOLogic.intT; -val bT = HOLogic.boolT; -fun myassoc2 l v = - case l of - [] => NONE - | (x,v')::xs => if v = v' then SOME x - else myassoc2 xs v; +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 + | Cx (i, t') => term_of_i vs (Add (Mul (i, Bound (Integer.nat 0)), t')); -fun term_of_i vs t = - case t of - C i => HOLogic.mk_number HOLogic.intT i - | Bound n => valOf (myassoc2 vs n) - | 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"},[iT,iT] ---> iT)$ - (term_of_i vs t1)$(term_of_i vs t2) - | Mul(i,t2) => Const(@{const_name "HOL.times"},[iT,iT] ---> iT)$ - (HOLogic.mk_number HOLogic.intT i)$(term_of_i vs t2) - | CX(i,t')=> term_of_i vs (Add(Mul (i,Bound (nat 0)),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 bT)$(term_of_qf ps vs t1)$ (term_of_qf ps vs t2) - | Closed n => valOf (myassoc2 ps n) - | NClosed n => term_of_qf ps vs (NOT (Closed n)) - | _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!"; +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 (Nota(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 (Nota(Dvd(i,t'))) + | Nota 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) + | Impa(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2) + | Iffa(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 (Nota (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; + 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