# HG changeset patch # User haftmann # Date 1273597216 -7200 # Node ID 9628f969d8432d4f369d6c56b5757540661edadc # Parent e6078ef937df2de6e25df67c622faff4cee70580 represent de-Bruin indices simply by position in list diff -r e6078ef937df -r 9628f969d843 src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Tue May 11 18:46:03 2010 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Tue May 11 19:00:16 2010 +0200 @@ -585,12 +585,11 @@ fun descend vs (abs as (_, xT, _)) = let val (xn', p') = variant_abs abs; - val vs' = ((xn', xT), 0) :: (map o apsnd) (fn n => n + 1) vs; - in (vs', p') end; + in ((xn', xT) :: vs, p') end; local structure Proc = Cooper_Procedure in -fun num_of_term vs (Free vT) = Proc.Bound (the (AList.lookup (op =) vs vT)) +fun num_of_term vs (Free vT) = Proc.Bound (find_index (fn vT' => vT' = vT) vs) | num_of_term vs (Term.Bound i) = Proc.Bound i | num_of_term vs @{term "0::int"} = Proc.C 0 | num_of_term vs @{term "1::int"} = Proc.C 1 @@ -636,13 +635,11 @@ (case perhaps_number t1 of SOME n => Proc.Dvd (n, num_of_term vs t2) | NONE => raise COOPER "reification: unsupported dvd") - | fm_of_term ps vs t = - (case AList.lookup (op aconv) ps t - of SOME n => Proc.Closed n - | NONE => raise COOPER "reification: unknown term"); + | fm_of_term ps vs t = let val n = find_index (fn t' => t aconv t') ps + in if n > 0 then Proc.Closed n else raise COOPER "reification: unknown term" end; fun term_of_num vs (Proc.C i) = HOLogic.mk_number HOLogic.intT i - | term_of_num vs (Proc.Bound n) = Free (the (AList.lookup (op =) vs n)) + | term_of_num vs (Proc.Bound n) = Free (nth vs n) | term_of_num vs (Proc.Neg t') = @{term "uminus :: int => _"} $ term_of_num vs t' | term_of_num vs (Proc.Add (t1, t2)) = @@ -670,23 +667,20 @@ | term_of_fm ps vs (Proc.Dvd (i, t')) = @{term "op dvd :: int => _ "} $ HOLogic.mk_number HOLogic.intT i $ term_of_num vs t' | term_of_fm ps vs (Proc.NDvd (i, t')) = term_of_fm ps vs (Proc.Not (Proc.Dvd (i, t'))) - | term_of_fm ps vs (Proc.Closed n) = the (AList.lookup (op =) ps n) + | term_of_fm ps vs (Proc.Closed n) = nth ps n | term_of_fm ps vs (Proc.NClosed n) = term_of_fm ps vs (Proc.Not (Proc.Closed n)); -fun invoke t = +fun procedure t = let - 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_fm (map swap ps) (map swap vs) (Proc.pa (fm_of_term ps vs t)))) - end; + val vs = Term.add_frees t []; + val ps = add_bools t []; + in (term_of_fm ps vs o Proc.pa o fm_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))))); +val (_, oracle) = Context.>>> (Context.map_theory_result (Thm.add_oracle (Binding.name "cooper", + (fn (ctxt, t) => (Thm.cterm_of (ProofContext.theory_of ctxt) o Logic.mk_equals o pairself HOLogic.mk_Trueprop) + (t, procedure t))))); val comp_ss = HOL_ss addsimps @{thms semiring_norm};