clarified context;
authorwenzelm
Fri Mar 06 23:33:25 2015 +0100 (2015-03-06)
changeset 596290d77c51b5040
parent 59628 2b15625b85fc
child 59630 c9aa1c90796f
clarified context;
src/HOL/Decision_Procs/approximation_generator.ML
src/HOL/Decision_Procs/commutative_ring_tac.ML
src/HOL/Decision_Procs/cooper_tac.ML
src/HOL/Decision_Procs/ferrack_tac.ML
src/HOL/Decision_Procs/mir_tac.ML
     1.1 --- a/src/HOL/Decision_Procs/approximation_generator.ML	Fri Mar 06 23:14:41 2015 +0100
     1.2 +++ b/src/HOL/Decision_Procs/approximation_generator.ML	Fri Mar 06 23:33:25 2015 +0100
     1.3 @@ -117,7 +117,7 @@
     1.4    }
     1.5  
     1.6  fun rewrite_with ctxt thms = Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps thms)
     1.7 -fun conv_term thy conv r = Thm.global_cterm_of thy r |> conv |> Thm.prop_of |> Logic.dest_equals |> snd
     1.8 +fun conv_term ctxt conv r = Thm.cterm_of ctxt r |> conv |> Thm.prop_of |> Logic.dest_equals |> snd
     1.9  
    1.10  fun approx_random ctxt prec eps frees e xs genuine_only size seed =
    1.11    let
    1.12 @@ -138,7 +138,7 @@
    1.13            (AList.lookup op = (map dest_Free xs ~~ ts)
    1.14              #> the_default Term.dummy
    1.15              #> curry op $ @{term "real::float\<Rightarrow>_"}
    1.16 -            #> conv_term (Proof_Context.theory_of ctxt) (rewrite_with ctxt postproc_form_eqs))
    1.17 +            #> conv_term ctxt (rewrite_with ctxt postproc_form_eqs))
    1.18            frees
    1.19        in
    1.20          if approximate ctxt (mk_approx_form e ts) |> is_True
    1.21 @@ -159,13 +159,12 @@
    1.22      "\<not> (p \<and> q) \<longleftrightarrow> \<not> p \<or> \<not> q"
    1.23      "\<not> (p \<or> q) \<longleftrightarrow> \<not> p \<and> \<not> q"
    1.24      "\<not> \<not> q \<longleftrightarrow> q"
    1.25 -    by auto
    1.26 -  }
    1.27 +    by auto}
    1.28  
    1.29  fun reify_goal ctxt t =
    1.30    HOLogic.mk_not t
    1.31 -    |> conv_term (Proof_Context.theory_of ctxt) (rewrite_with ctxt preproc_form_eqs)
    1.32 -    |> conv_term (Proof_Context.theory_of ctxt) (Reification.conv ctxt form_equations)
    1.33 +    |> conv_term ctxt (rewrite_with ctxt preproc_form_eqs)
    1.34 +    |> conv_term ctxt (Reification.conv ctxt form_equations)
    1.35      |> dest_interpret_form
    1.36      ||> HOLogic.dest_list
    1.37  
     2.1 --- a/src/HOL/Decision_Procs/commutative_ring_tac.ML	Fri Mar 06 23:14:41 2015 +0100
     2.2 +++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML	Fri Mar 06 23:33:25 2015 +0100
     2.3 @@ -76,12 +76,11 @@
     2.4  fun reif_eq ctxt (eq as Const (@{const_name HOL.eq}, Type (@{type_name fun}, [T, _])) $ lhs $ rhs) =
     2.5        if Sign.of_sort (Proof_Context.theory_of ctxt) (T, cr_sort) then
     2.6          let
     2.7 -          val thy = Proof_Context.theory_of ctxt;
     2.8            val fs = Misc_Legacy.term_frees eq;
     2.9 -          val cvs = Thm.global_cterm_of thy (HOLogic.mk_list T fs);
    2.10 -          val clhs = Thm.global_cterm_of thy (reif_polex T fs lhs);
    2.11 -          val crhs = Thm.global_cterm_of thy (reif_polex T fs rhs);
    2.12 -          val ca = Thm.global_ctyp_of thy T;
    2.13 +          val cvs = Thm.cterm_of ctxt (HOLogic.mk_list T fs);
    2.14 +          val clhs = Thm.cterm_of ctxt (reif_polex T fs lhs);
    2.15 +          val crhs = Thm.cterm_of ctxt (reif_polex T fs rhs);
    2.16 +          val ca = Thm.ctyp_of ctxt T;
    2.17          in (ca, cvs, clhs, crhs) end
    2.18        else error ("reif_eq: not an equation over " ^ Syntax.string_of_sort ctxt cr_sort)
    2.19    | reif_eq _ _ = error "reif_eq: not an equation";
     3.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Fri Mar 06 23:14:41 2015 +0100
     3.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Fri Mar 06 23:33:25 2015 +0100
     3.3 @@ -40,7 +40,6 @@
     3.4  
     3.5  fun linz_tac ctxt q = Object_Logic.atomize_prems_tac ctxt THEN' SUBGOAL (fn (g, i) =>
     3.6    let
     3.7 -    val thy = Proof_Context.theory_of ctxt;
     3.8      (* Transform the term*)
     3.9      val (t, np, nh) = prepare_for_linz q g;
    3.10      (* Some simpsets for dealing with mod div abs and nat*)
    3.11 @@ -73,7 +72,7 @@
    3.12        |> fold Simplifier.add_cong @{thms conj_le_cong imp_le_cong}
    3.13      (* simp rules for elimination of abs *)
    3.14      val simpset3 = put_simpset HOL_basic_ss ctxt |> Splitter.add_split @{thm abs_split}
    3.15 -    val ct = Thm.global_cterm_of thy (HOLogic.mk_Trueprop t)
    3.16 +    val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t)
    3.17      (* Theorem for the nat --> int transformation *)
    3.18      val pre_thm = Seq.hd (EVERY
    3.19        [simp_tac mod_div_simpset 1, simp_tac simpset0 1,
    3.20 @@ -86,7 +85,7 @@
    3.21        (case Thm.prop_of pre_thm of
    3.22          Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
    3.23            let
    3.24 -            val pth = linzqe_oracle (Thm.global_cterm_of thy (Envir.eta_long [] t1))
    3.25 +            val pth = linzqe_oracle (Thm.cterm_of ctxt (Envir.eta_long [] t1))
    3.26            in
    3.27              ((pth RS iffD2) RS pre_thm,
    3.28                assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
     4.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Fri Mar 06 23:14:41 2015 +0100
     4.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Fri Mar 06 23:33:25 2015 +0100
     4.3 @@ -50,12 +50,11 @@
     4.4          THEN' (REPEAT_DETERM o split_tac ctxt [@{thm split_min}, @{thm split_max}, @{thm abs_split}])
     4.5          THEN' SUBGOAL (fn (g, i) =>
     4.6    let
     4.7 -    val thy = Proof_Context.theory_of ctxt
     4.8      (* Transform the term*)
     4.9      val (t,np,nh) = prepare_for_linr q g
    4.10      (* Some simpsets for dealing with mod div abs and nat*)
    4.11      val simpset0 = put_simpset HOL_basic_ss ctxt addsimps comp_arith
    4.12 -    val ct = Thm.global_cterm_of thy (HOLogic.mk_Trueprop t)
    4.13 +    val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t)
    4.14      (* Theorem for the nat --> int transformation *)
    4.15     val pre_thm = Seq.hd (EVERY
    4.16        [simp_tac simpset0 1,
     5.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Fri Mar 06 23:14:41 2015 +0100
     5.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Fri Mar 06 23:33:25 2015 +0100
     5.3 @@ -70,7 +70,6 @@
     5.4          THEN' (REPEAT_DETERM o split_tac ctxt [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}])
     5.5          THEN' SUBGOAL (fn (g, i) =>
     5.6    let
     5.7 -    val thy = Proof_Context.theory_of ctxt
     5.8      (* Transform the term*)
     5.9      val (t,np,nh) = prepare_for_mir q g
    5.10      (* Some simpsets for dealing with mod div abs and nat*)
    5.11 @@ -101,7 +100,7 @@
    5.12                  @{thm "int_0"}, @{thm "int_1"}]
    5.13        |> fold Simplifier.add_cong [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
    5.14      (* simp rules for elimination of abs *)
    5.15 -    val ct = Thm.global_cterm_of thy (HOLogic.mk_Trueprop t)
    5.16 +    val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t)
    5.17      (* Theorem for the nat --> int transformation *)
    5.18      val pre_thm = Seq.hd (EVERY
    5.19        [simp_tac mod_div_simpset 1, simp_tac simpset0 1,
    5.20 @@ -116,8 +115,8 @@
    5.21      let val pth =
    5.22            (* If quick_and_dirty then run without proof generation as oracle*)
    5.23               if Config.get ctxt quick_and_dirty
    5.24 -             then mirfr_oracle (false, Thm.global_cterm_of thy (Envir.eta_long [] t1))
    5.25 -             else mirfr_oracle (true, Thm.global_cterm_of thy (Envir.eta_long [] t1))
    5.26 +             then mirfr_oracle (false, Thm.cterm_of ctxt (Envir.eta_long [] t1))
    5.27 +             else mirfr_oracle (true, Thm.cterm_of ctxt (Envir.eta_long [] t1))
    5.28      in 
    5.29         ((pth RS iffD2) RS pre_thm,
    5.30          assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))