src/HOL/Decision_Procs/ferrante_rackoff.ML
changeset 51717 9e7d1c139569
parent 46497 89ccf66aa73d
child 54742 7a86358a3c0b
     1.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4    funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE)
     1.5      (funpow 2 Thm.dest_arg (cprop_of th)) |> Thm.dest_arg
     1.6  
     1.7 -fun ferrack_conv
     1.8 +fun ferrack_conv ctxt
     1.9     (entr as ({minf = minf, pinf = pinf, nmi = nmi, npi = npi,
    1.10                ld = ld, qe = qe, atoms = atoms},
    1.11               {isolate_conv = icv, whatis = wi, simpset = simpset}):entry) =
    1.12 @@ -163,7 +163,7 @@
    1.13                          qe))
    1.14                    [fU, ld_th, nmi_th, npi_th, minf_th, pinf_th]
    1.15      val bex_conv =
    1.16 -      Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms bex_simps(1-5)})
    1.17 +      Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms bex_simps(1-5)})
    1.18      val result_th = fconv_rule (arg_conv bex_conv) (Thm.transitive enth qe_th)
    1.19     in result_th
    1.20     end
    1.21 @@ -196,22 +196,21 @@
    1.22     in h (bounds + 1) b' end;
    1.23  in h end;
    1.24  
    1.25 -fun raw_ferrack_qe_conv ctxt (thy, {isolate_conv, whatis, simpset}) tm =
    1.26 +fun raw_ferrack_qe_conv ctxt (thy, {isolate_conv, whatis, simpset = ss}) tm =
    1.27   let
    1.28 -   val ss = simpset
    1.29     val ss' =
    1.30 -     merge_ss (HOL_basic_ss addsimps @{thms simp_thms ex_simps all_simps
    1.31 -                not_all all_not_ex ex_disj_distrib}, ss)
    1.32 -     |> Simplifier.inherit_context ss
    1.33 -   val pcv = Simplifier.rewrite ss'     
    1.34 -   val postcv = Simplifier.rewrite ss
    1.35 -   val nnf = K (nnf_conv then_conv postcv)
    1.36 +     merge_ss (simpset_of
    1.37 +      (put_simpset HOL_basic_ss ctxt addsimps
    1.38 +        @{thms simp_thms ex_simps all_simps not_all all_not_ex ex_disj_distrib}), ss);
    1.39 +   val pcv = Simplifier.rewrite (put_simpset ss' ctxt);
    1.40 +   val postcv = Simplifier.rewrite (put_simpset ss ctxt);
    1.41 +   val nnf = K (nnf_conv ctxt then_conv postcv)
    1.42     val qe_conv = Qelim.gen_qelim_conv pcv postcv pcv cons (Thm.add_cterm_frees tm [])
    1.43                    (isolate_conv ctxt) nnf
    1.44 -                  (fn vs => ferrack_conv (thy,{isolate_conv = isolate_conv ctxt,
    1.45 -                                               whatis = whatis, simpset = simpset}) vs
    1.46 +                  (fn vs => ferrack_conv ctxt (thy,{isolate_conv = isolate_conv ctxt,
    1.47 +                                               whatis = whatis, simpset = ss}) vs
    1.48                     then_conv postcv)
    1.49 - in (Simplifier.rewrite ss then_conv qe_conv) tm end;
    1.50 + in (Simplifier.rewrite (put_simpset ss ctxt) then_conv qe_conv) tm end;
    1.51  
    1.52  fun dlo_instance ctxt tm =
    1.53    Ferrante_Rackoff_Data.match ctxt (grab_atom_bop 0 tm);
    1.54 @@ -226,8 +225,8 @@
    1.55      NONE => no_tac
    1.56    | SOME instance =>
    1.57        Object_Logic.full_atomize_tac i THEN
    1.58 -      simp_tac (#simpset (snd instance)) i THEN  (* FIXME already part of raw_ferrack_qe_conv? *)
    1.59 +      simp_tac (put_simpset (#simpset (snd instance)) ctxt) i THEN  (* FIXME already part of raw_ferrack_qe_conv? *)
    1.60        CONVERSION (Object_Logic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN
    1.61 -      simp_tac (simpset_of ctxt) i));  (* FIXME really? *)
    1.62 +      simp_tac ctxt i));  (* FIXME really? *)
    1.63  
    1.64  end;