--- 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) = (\<lambda>g. igcd i g)"
"numgcdh (CN n c t) = (\<lambda>g. igcd c (numgcdh t g))"
"numgcdh t = (\<lambda>g. 1)"
-defs numgcd_def: "numgcd t \<equiv> numgcdh t (maxcoeff t)"
+defs numgcd_def [code func]: "numgcd t \<equiv> numgcdh t (maxcoeff t)"
recdef reducecoeffh "measure size"
"reducecoeffh (C i) = (\<lambda> 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 \<Rightarrow> num \<Rightarrow> 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 \<Rightarrow> num \<Rightarrow> 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 \<Rightarrow> num \<Rightarrow> fm"
- ge :: "int \<Rightarrow> num \<Rightarrow> fm"
- eq :: "int \<Rightarrow> num \<Rightarrow> fm"
- neq :: "int \<Rightarrow> num \<Rightarrow> 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 \<equiv> (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 \<equiv> (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 \<equiv> (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 \<equiv> (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 \<equiv> (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 \<equiv> (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 \<Rightarrow> num \<Rightarrow> 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 \<Rightarrow> num \<Rightarrow> 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 \<Rightarrow> num \<Rightarrow> 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 \<Longrightarrow> Ifm bs (split lt (rsplit0 t)) = Ifm bs (Lt t) \<and> 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 \<Rightarrow> 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"
--- 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;
--- 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) \<and> 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 \<Rightarrow> 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 *)
--- 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