--- a/src/HOL/Tools/Qelim/cooper.ML Tue May 11 08:52:22 2010 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML Tue May 11 18:31:36 2010 +0200
@@ -77,7 +77,9 @@
val iT = HOLogic.intT
val bT = HOLogic.boolT;
-val dest_numeral = HOLogic.dest_number #> snd;
+val dest_number = HOLogic.dest_number #> snd;
+val perhaps_number = try dest_number;
+val is_number = can dest_number;
val [miconj, midisj, mieq, mineq, milt, mile, migt, mige, midvd, mindvd, miP] =
map(instantiate' [SOME @{ctyp "int"}] []) @{thms "minf"};
@@ -171,10 +173,8 @@
val [addC, mulC, subC] = map term_of [cadd, cmulC, cminus]
val [zero, one] = [@{term "0 :: int"}, @{term "1 :: int"}];
-val is_numeral = can dest_numeral;
-
-fun numeral1 f n = HOLogic.mk_number iT (f (dest_numeral n));
-fun numeral2 f m n = HOLogic.mk_number iT (f (dest_numeral m) (dest_numeral n));
+fun numeral1 f n = HOLogic.mk_number iT (f (dest_number n));
+fun numeral2 f m n = HOLogic.mk_number iT (f (dest_number m) (dest_number n));
val [minus1,plus1] =
map (fn c => fn t => Thm.capply (Thm.capply c t) cone) [cminus,cadd];
@@ -253,16 +253,16 @@
exception COOPER of string;
-fun lint vars tm = if is_numeral tm then tm else case tm of
+fun lint vars tm = if is_number tm then tm else case tm of
Const (@{const_name Groups.uminus}, _) $ t => linear_neg (lint vars t)
| Const (@{const_name Groups.plus}, _) $ s $ t => linear_add vars (lint vars s) (lint vars t)
| Const (@{const_name Groups.minus}, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t)
| Const (@{const_name Groups.times}, _) $ s $ t =>
let val s' = lint vars s
val t' = lint vars t
- in if is_numeral s' then (linear_cmul (dest_numeral s') t')
- else if is_numeral t' then (linear_cmul (dest_numeral t') s')
- else raise COOPER "lint: not linear"
+ in case perhaps_number s' of SOME n => linear_cmul n t'
+ | NONE => (case perhaps_number t' of SOME n => linear_cmul n s'
+ | NONE => raise COOPER "lint: not linear")
end
| _ => addC $ (mulC $ one $ tm) $ zero;
@@ -277,14 +277,14 @@
(case lint vs (subC$t$s) of
(t as a$(m$c$y)$r) =>
if x <> y then b$zero$t
- else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r
+ else if dest_number c < 0 then b$(m$(numeral1 ~ c)$y)$r
else b$(m$c$y)$(linear_neg r)
| t => b$zero$t)
| lin (vs as x::_) (b$s$t) =
(case lint vs (subC$t$s) of
(t as a$(m$c$y)$r) =>
if x <> y then b$zero$t
- else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r
+ else if dest_number c < 0 then b$(m$(numeral1 ~ c)$y)$r
else b$(linear_neg r)$(m$c$y)
| t => b$zero$t)
| lin vs fm = fm;
@@ -307,12 +307,12 @@
val th = Conv.binop_conv (lint_conv ctxt vs) ct
val (d',t') = Thm.dest_binop (Thm.rhs_of th)
val (dt',tt') = (term_of d', term_of t')
- in if is_numeral dt' andalso is_numeral tt'
+ in if is_number dt' andalso is_number tt'
then Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite presburger_ss)) th
else
let
val dth =
- ((if dest_numeral (term_of d') < 0 then
+ ((if dest_number (term_of d') < 0 then
Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (lint_conv ctxt vs)))
(Thm.transitive th (inst' [d',t'] dvd_uminus))
else th) handle TERM _ => th)
@@ -320,7 +320,7 @@
in
case tt' of
Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$_)$_ =>
- let val x = dest_numeral c
+ let val x = dest_number c
in if x < 0 then Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (lint_conv ctxt vs)))
(Thm.transitive dth (inst' [d'',t'] dvd_uminus'))
else dth end
@@ -345,13 +345,13 @@
Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
if x aconv y andalso member (op =)
["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
- then (ins (dest_numeral c) acc,dacc) else (acc,dacc)
+ then (ins (dest_number c) acc,dacc) else (acc,dacc)
| Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
if x aconv y andalso member (op =)
[@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
- then (ins (dest_numeral c) acc, dacc) else (acc,dacc)
+ then (ins (dest_number c) acc, dacc) else (acc,dacc)
| Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_) =>
- if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc)
+ if x aconv y then (acc,ins (dest_number c) dacc) else (acc,dacc)
| Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
| Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
| Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t)
@@ -374,7 +374,7 @@
let val tab = fold Inttab.update
(ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty
in
- fn ct => the (Inttab.lookup tab (ct |> term_of |> dest_numeral))
+ fn ct => the (Inttab.lookup tab (ct |> term_of |> dest_number))
handle Option =>
(writeln ("noz: Theorems-Table contains no entry for " ^
Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option)
@@ -387,15 +387,15 @@
| Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
if x=y andalso member (op =)
["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
- then cv (l div dest_numeral c) t else Thm.reflexive t
+ then cv (l div dest_number c) t else Thm.reflexive t
| Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
if x=y andalso member (op =)
[@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
- then cv (l div dest_numeral c) t else Thm.reflexive t
+ then cv (l div dest_number c) t else Thm.reflexive t
| Const(@{const_name Rings.dvd},_)$d$(r as (Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_)) =>
if x=y then
let
- val k = l div dest_numeral c
+ val k = l div dest_number c
val kt = HOLogic.mk_number iT k
val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t]
((Thm.dest_arg t |> funpow 2 Thm.dest_arg1 |> notz) RS zdvd_mono)
@@ -447,8 +447,8 @@
| Le t => (bacc, ins (plus1 t) aacc,dacc)
| Gt t => (ins t bacc, aacc,dacc)
| Ge t => (ins (minus1 t) bacc, aacc,dacc)
- | Dvd (d,_) => (bacc,aacc,insert (op =) (term_of d |> dest_numeral) dacc)
- | NDvd (d,_) => (bacc,aacc,insert (op =) (term_of d|> dest_numeral) dacc)
+ | Dvd (d,_) => (bacc,aacc,insert (op =) (term_of d |> dest_number) dacc)
+ | NDvd (d,_) => (bacc,aacc,insert (op =) (term_of d|> dest_number) dacc)
| _ => (bacc, aacc, dacc)
val (b0,a0,ds) = h p ([],[],[])
val d = Integer.lcms ds
@@ -462,7 +462,7 @@
in equal_elim (Thm.symmetric th) TrueI end;
val dvd =
let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in
- fn ct => the (Inttab.lookup tab (term_of ct |> dest_numeral))
+ fn ct => the (Inttab.lookup tab (term_of ct |> dest_number))
handle Option =>
(writeln ("dvd: Theorems-Table contains no entry for" ^
Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option)
@@ -554,125 +554,121 @@
fun integer_nnf_conv ctxt env =
nnf_conv then_conv literals_conv [HOLogic.conj, HOLogic.disj] [] env (linearize_conv ctxt);
-local
- val pcv = Simplifier.rewrite
- (HOL_basic_ss addsimps (@{thms simp_thms} @ List.take(@{thms ex_simps}, 4)
- @ [not_all, all_not_ex, @{thm ex_disj_distrib}]))
- val postcv = Simplifier.rewrite presburger_ss
- fun conv ctxt p =
- let val _ = ()
- in
- Qelim.gen_qelim_conv pcv postcv pcv (cons o term_of)
- (OldTerm.term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt)
- (cooperex_conv ctxt) p
- end
- handle CTERM s => raise COOPER "bad cterm"
- | THM s => raise COOPER "bad thm"
- | TYPE s => raise COOPER "bad type"
-in val conv = conv
-end;
+val conv_ss = HOL_basic_ss addsimps
+ (@{thms simp_thms} @ take 4 @{thms ex_simps} @ [not_all, all_not_ex, @{thm ex_disj_distrib}]);
+
+fun conv ctxt p =
+ Qelim.gen_qelim_conv (Simplifier.rewrite conv_ss) (Simplifier.rewrite presburger_ss) (Simplifier.rewrite conv_ss)
+ (cons o term_of) (OldTerm.term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt)
+ (cooperex_conv ctxt) p
+ handle CTERM s => raise COOPER "bad cterm"
+ | THM s => raise COOPER "bad thm"
+ | TYPE s => raise COOPER "bad type"
-fun term_bools acc t =
+fun add_bools t =
let
- 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 = not (fastype_of t = HOLogic.boolT)
+ val ops = [@{term "op = :: int => _"}, @{term "op < :: int => _"}, @{term "op <= :: int => _"},
+ @{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
+ @{term "Not"}, @{term "All :: (int => _) => _"},
+ @{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}];
+ val is_op = member (op =) ops;
+ val skip = not (fastype_of t = HOLogic.boolT)
in case t of
- (l as f $ a) $ b => if ty t orelse member (op =) ops f then term_bools (term_bools acc l)b
- else insert (op aconv) t acc
- | f $ a => if ty t orelse member (op =) ops f 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 member (op =) ops t then acc else insert (op aconv) t acc
+ (l as f $ a) $ b => if skip orelse is_op f then add_bools b o add_bools l
+ else insert (op aconv) t
+ | f $ a => if skip orelse is_op f then add_bools a o add_bools f
+ else insert (op aconv) t
+ | Abs p => add_bools (snd (variant_abs p))
+ | _ => if skip orelse is_op t then I else insert (op aconv) t
end;
-fun i_of_term vs t = case t
- of Free (xn, xT) => (case AList.lookup (op aconv) vs t
- of NONE => raise COOPER "reification: variable not found in list"
- | SOME n => Cooper_Procedure.Bound n)
- | @{term "0::int"} => Cooper_Procedure.C 0
- | @{term "1::int"} => Cooper_Procedure.C 1
- | Term.Bound i => Cooper_Procedure.Bound i
- | Const(@{const_name Groups.uminus},_)$t' => Cooper_Procedure.Neg (i_of_term vs t')
- | Const(@{const_name Groups.plus},_)$t1$t2 => Cooper_Procedure.Add (i_of_term vs t1,i_of_term vs t2)
- | Const(@{const_name Groups.minus},_)$t1$t2 => Cooper_Procedure.Sub (i_of_term vs t1,i_of_term vs t2)
- | Const(@{const_name Groups.times},_)$t1$t2 =>
- (Cooper_Procedure.Mul (HOLogic.dest_number t1 |> snd, i_of_term vs t2)
- handle TERM _ =>
- (Cooper_Procedure.Mul (HOLogic.dest_number t2 |> snd, i_of_term vs t1)
- handle TERM _ => raise COOPER "reification: unsupported kind of multiplication"))
- | _ => (Cooper_Procedure.C (HOLogic.dest_number t |> snd)
- handle TERM _ => raise COOPER "reification: unknown term");
+local structure Proc = Cooper_Procedure in
+
+fun i_of_term vs (Free vT) = Proc.Bound (the (AList.lookup (op =) vs vT))
+ | i_of_term vs (Term.Bound i) = Proc.Bound i
+ | i_of_term vs @{term "0::int"} = Proc.C 0
+ | i_of_term vs @{term "1::int"} = Proc.C 1
+ | i_of_term vs (t as Const (@{const_name number_of}, _) $ _) = Proc.C (dest_number t)
+ | i_of_term vs (Const (@{const_name Groups.uminus}, _) $ t') = Proc.Neg (i_of_term vs t')
+ | i_of_term vs (Const (@{const_name Groups.plus}, _) $ t1 $ t2) = Proc.Add (i_of_term vs t1, i_of_term vs t2)
+ | i_of_term vs (Const (@{const_name Groups.minus}, _) $ t1 $ t2) = Proc.Sub (i_of_term vs t1, i_of_term vs t2)
+ | i_of_term vs (Const (@{const_name Groups.times}, _) $ t1 $ t2) = (case perhaps_number t1
+ of SOME n => Proc.Mul (n, i_of_term vs t2)
+ | NONE => (case perhaps_number t2
+ of SOME n => Proc.Mul (n, i_of_term vs t1)
+ | NONE => raise COOPER "reification: unsupported kind of multiplication"))
+ | i_of_term _ _ = raise COOPER "reification: unknown term";
-fun qf_of_term ps vs t = case t
- of Const("True",_) => Cooper_Procedure.T
- | Const("False",_) => Cooper_Procedure.F
- | Const(@{const_name Orderings.less},_)$t1$t2 => Cooper_Procedure.Lt (Cooper_Procedure.Sub (i_of_term vs t1,i_of_term vs t2))
- | Const(@{const_name Orderings.less_eq},_)$t1$t2 => Cooper_Procedure.Le (Cooper_Procedure.Sub(i_of_term vs t1,i_of_term vs t2))
- | Const(@{const_name Rings.dvd},_)$t1$t2 =>
- (Cooper_Procedure.Dvd (HOLogic.dest_number t1 |> snd, i_of_term vs t2)
+fun qf_of_term ps vs t = case t
+ of Const (@{const_name True}, _) => Proc.T
+ | Const (@{const_name False}, _) => Proc.F
+ | Const (@{const_name Orderings.less}, _) $ t1 $ t2 => Proc.Lt (Proc.Sub (i_of_term vs t1, i_of_term vs t2))
+ | Const (@{const_name Orderings.less_eq}, _) $ t1 $ t2 => Proc.Le (Proc.Sub(i_of_term vs t1, i_of_term vs t2))
+ | Const (@{const_name Rings.dvd}, _) $ t1 $ t2 =>
+ (Proc.Dvd (dest_number t1, i_of_term vs t2)
handle TERM _ => raise COOPER "reification: unsupported dvd")
- | @{term "op = :: int => _"}$t1$t2 => Cooper_Procedure.Eq (Cooper_Procedure.Sub (i_of_term vs t1,i_of_term vs t2))
- | @{term "op = :: bool => _ "}$t1$t2 => Cooper_Procedure.Iff(qf_of_term ps vs t1,qf_of_term ps vs t2)
- | Const("op &",_)$t1$t2 => Cooper_Procedure.And(qf_of_term ps vs t1,qf_of_term ps vs t2)
- | Const("op |",_)$t1$t2 => Cooper_Procedure.Or(qf_of_term ps vs t1,qf_of_term ps vs t2)
- | Const("op -->",_)$t1$t2 => Cooper_Procedure.Imp(qf_of_term ps vs t1,qf_of_term ps vs t2)
- | Const (@{const_name Not},_)$t' => Cooper_Procedure.Not(qf_of_term ps vs t')
- | Const("Ex",_)$Abs(xn,xT,p) =>
+ | @{term "op = :: int => _"} $ t1 $ t2 => Proc.Eq (Proc.Sub (i_of_term vs t1, i_of_term vs t2))
+ | @{term "op = :: bool => _ "} $ t1 $ t2 => Proc.Iff (qf_of_term ps vs t1, qf_of_term ps vs t2)
+ | Const ("op &", _) $ t1 $t2 => Proc.And (qf_of_term ps vs t1, qf_of_term ps vs t2)
+ | Const ("op |", _) $ t1 $ t2 => Proc.Or (qf_of_term ps vs t1, qf_of_term ps vs t2)
+ | Const ("op -->", _) $ t1 $t2 => Proc.Imp (qf_of_term ps vs t1, qf_of_term ps vs t2)
+ | Const (@{const_name Not}, _) $ t' => Proc.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 Cooper_Procedure.E (qf_of_term ps vs' p')
+ val vs' = ((xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
+ in Proc.E (qf_of_term ps vs' p')
end
- | Const("All",_)$Abs(xn,xT,p) =>
+ | 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 Cooper_Procedure.A (qf_of_term ps vs' p')
+ val vs' = ((xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
+ in Proc.A (qf_of_term ps vs' p')
end
| _ =>(case AList.lookup (op aconv) ps t of
NONE => raise COOPER "reification: unknown term"
- | SOME n => Cooper_Procedure.Closed n);
+ | SOME n => Proc.Closed n);
fun term_of_i vs t = case t
- of Cooper_Procedure.C i => HOLogic.mk_number HOLogic.intT i
- | Cooper_Procedure.Bound n => the (AList.lookup (op =) vs n)
- | Cooper_Procedure.Neg t' => @{term "uminus :: int => _"} $ term_of_i vs t'
- | Cooper_Procedure.Add (t1, t2) => @{term "op + :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
- | Cooper_Procedure.Sub (t1, t2) => @{term "op - :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
- | Cooper_Procedure.Mul (i, t2) => @{term "op * :: int => _"} $
+ of Proc.C i => HOLogic.mk_number HOLogic.intT i
+ | Proc.Bound n => Free (the (AList.lookup (op =) vs n))
+ | Proc.Neg t' => @{term "uminus :: int => _"} $ term_of_i vs t'
+ | Proc.Add (t1, t2) => @{term "op + :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
+ | Proc.Sub (t1, t2) => @{term "op - :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
+ | Proc.Mul (i, t2) => @{term "op * :: int => _"} $
HOLogic.mk_number HOLogic.intT i $ term_of_i vs t2
- | Cooper_Procedure.Cn (n, i, t') => term_of_i vs (Cooper_Procedure.Add (Cooper_Procedure.Mul (i, Cooper_Procedure.Bound n), t'));
+ | Proc.Cn (n, i, t') => term_of_i vs (Proc.Add (Proc.Mul (i, Proc.Bound n), t'));
fun term_of_qf ps vs t =
case t of
- Cooper_Procedure.T => HOLogic.true_const
- | Cooper_Procedure.F => HOLogic.false_const
- | Cooper_Procedure.Lt t' => @{term "op < :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
- | Cooper_Procedure.Le t' => @{term "op <= :: int => _ "}$ term_of_i vs t' $ @{term "0::int"}
- | Cooper_Procedure.Gt t' => @{term "op < :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
- | Cooper_Procedure.Ge t' => @{term "op <= :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
- | Cooper_Procedure.Eq t' => @{term "op = :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
- | Cooper_Procedure.NEq t' => term_of_qf ps vs (Cooper_Procedure.Not (Cooper_Procedure.Eq t'))
- | Cooper_Procedure.Dvd(i,t') => @{term "op dvd :: int => _ "} $
+ Proc.T => HOLogic.true_const
+ | Proc.F => HOLogic.false_const
+ | Proc.Lt t' => @{term "op < :: int => _ "} $ term_of_i vs t' $ @{term "0::int"}
+ | Proc.Le t' => @{term "op <= :: int => _ "} $ term_of_i vs t' $ @{term "0::int"}
+ | Proc.Gt t' => @{term "op < :: int => _ "} $ @{term "0::int"} $ term_of_i vs t'
+ | Proc.Ge t' => @{term "op <= :: int => _ "} $ @{term "0::int"} $ term_of_i vs t'
+ | Proc.Eq t' => @{term "op = :: int => _ "} $ term_of_i vs t'$ @{term "0::int"}
+ | Proc.NEq t' => term_of_qf ps vs (Proc.Not (Proc.Eq t'))
+ | Proc.Dvd (i, t') => @{term "op dvd :: int => _ "} $
HOLogic.mk_number HOLogic.intT i $ term_of_i vs t'
- | Cooper_Procedure.NDvd(i,t')=> term_of_qf ps vs (Cooper_Procedure.Not(Cooper_Procedure.Dvd(i,t')))
- | Cooper_Procedure.Not t' => HOLogic.Not$(term_of_qf ps vs t')
- | Cooper_Procedure.And(t1,t2) => HOLogic.conj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
- | Cooper_Procedure.Or(t1,t2) => HOLogic.disj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
- | Cooper_Procedure.Imp(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
- | Cooper_Procedure.Iff(t1,t2) => @{term "op = :: bool => _"} $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
- | Cooper_Procedure.Closed n => the (AList.lookup (op =) ps n)
- | Cooper_Procedure.NClosed n => term_of_qf ps vs (Cooper_Procedure.Not (Cooper_Procedure.Closed n));
+ | Proc.NDvd (i, t')=> term_of_qf ps vs (Proc.Not (Proc.Dvd (i, t')))
+ | Proc.Not t' => HOLogic.Not $ term_of_qf ps vs t'
+ | Proc.And (t1, t2) => HOLogic.conj $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
+ | Proc.Or (t1, t2) => HOLogic.disj $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
+ | Proc.Imp (t1, t2) => HOLogic.imp $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
+ | Proc.Iff (t1, t2) => @{term "op = :: bool => _"} $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
+ | Proc.Closed n => the (AList.lookup (op =) ps n)
+ | Proc.NClosed n => term_of_qf ps vs (Proc.Not (Proc.Closed n));
fun invoke t =
let
- val (vs, ps) = pairself (map_index swap) (OldTerm.term_frees t, term_bools [] t);
+ val vs = map_index swap (Term.add_frees t []);
+ val ps = map_index swap (add_bools t []);
in
Logic.mk_equals (HOLogic.mk_Trueprop t,
- HOLogic.mk_Trueprop (term_of_qf (map swap ps) (map swap vs) (Cooper_Procedure.pa (qf_of_term ps vs t))))
+ HOLogic.mk_Trueprop (term_of_qf (map swap ps) (map swap vs) (Proc.pa (qf_of_term ps vs t))))
end;
+end;
+
val (_, oracle) = Context.>>> (Context.map_theory_result
(Thm.add_oracle (Binding.name "cooper",
(fn (ctxt, t) => Thm.cterm_of (ProofContext.theory_of ctxt) (invoke t)))));
@@ -730,7 +726,7 @@
| Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r
| Const(@{const_name Divides.mod},_)$l$r => isnum l andalso isnum r
| Const(@{const_name Divides.div},_)$l$r => isnum l andalso isnum r
- | _ => can HOLogic.dest_number t orelse can HOLogic.dest_nat t
+ | _ => is_number t orelse can HOLogic.dest_nat t
fun ty cts t =
if not (member (op =) [HOLogic.intT, HOLogic.natT, HOLogic.boolT] (typ_of (ctyp_of_term t))) then false