proper context;
authorwenzelm
Fri Mar 06 20:08:45 2015 +0100 (2015-03-06)
changeset 59625aacdce52b2fc
parent 59624 6c0e70b01111
child 59626 a6e977d8b070
proper context;
src/HOL/Library/Multiset.thy
src/HOL/Tools/Function/function_lib.ML
src/HOL/Tools/Function/scnp_reconstruct.ML
src/HOL/Tools/Function/termination.ML
     1.1 --- a/src/HOL/Library/Multiset.thy	Fri Mar 06 18:21:32 2015 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Fri Mar 06 20:08:45 2015 +0100
     1.3 @@ -1917,9 +1917,9 @@
     1.4    val mset_nonempty_tac =
     1.5        rtac @{thm nonempty_plus} ORELSE' rtac @{thm nonempty_single}
     1.6  
     1.7 -  val regroup_munion_conv =
     1.8 -      Function_Lib.regroup_conv @{const_abbrev Mempty} @{const_name plus}
     1.9 -        (map (fn t => t RS eq_reflection) (@{thms ac_simps} @ @{thms empty_neutral}))
    1.10 +  fun regroup_munion_conv ctxt =
    1.11 +    Function_Lib.regroup_conv ctxt @{const_abbrev Mempty} @{const_name plus}
    1.12 +      (map (fn t => t RS eq_reflection) (@{thms ac_simps} @ @{thms empty_neutral}))
    1.13  
    1.14    fun unfold_pwleq_tac i =
    1.15      (rtac @{thm pw_leq_step} i THEN (fn st => unfold_pwleq_tac (i + 1) st))
     2.1 --- a/src/HOL/Tools/Function/function_lib.ML	Fri Mar 06 18:21:32 2015 +0100
     2.2 +++ b/src/HOL/Tools/Function/function_lib.ML	Fri Mar 06 20:08:45 2015 +0100
     2.3 @@ -21,8 +21,8 @@
     2.4    val try_proof: cterm -> tactic -> proof_attempt
     2.5  
     2.6    val dest_binop_list: string -> term -> term list
     2.7 -  val regroup_conv: string -> string -> thm list -> int list -> conv
     2.8 -  val regroup_union_conv: int list -> conv
     2.9 +  val regroup_conv: Proof.context -> string -> string -> thm list -> int list -> conv
    2.10 +  val regroup_union_conv: Proof.context -> int list -> conv
    2.11  
    2.12    val inst_constrs_of: Proof.context -> typ -> term list
    2.13  end
    2.14 @@ -93,11 +93,8 @@
    2.15          (e.g. [0,1,3] in the above example)
    2.16  *)
    2.17  
    2.18 -fun regroup_conv neu cn ac is ct =
    2.19 +fun regroup_conv ctxt neu cn ac is ct =
    2.20   let
    2.21 -   val thy = Thm.theory_of_cterm ct
    2.22 -   val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
    2.23 -
    2.24     val mk = HOLogic.mk_binop cn
    2.25     val t = Thm.term_of ct
    2.26     val xs = dest_binop_list cn t
    2.27 @@ -117,8 +114,8 @@
    2.28   end
    2.29  
    2.30  (* instance for unions *)
    2.31 -val regroup_union_conv =
    2.32 -  regroup_conv @{const_abbrev Set.empty} @{const_name Lattices.sup}
    2.33 +fun regroup_union_conv ctxt =
    2.34 +  regroup_conv ctxt @{const_abbrev Set.empty} @{const_name Lattices.sup}
    2.35      (map (fn t => t RS eq_reflection)
    2.36        (@{thms Un_ac} @ @{thms Un_empty_right} @ @{thms Un_empty_left}))
    2.37  
     3.1 --- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Fri Mar 06 18:21:32 2015 +0100
     3.2 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Fri Mar 06 20:08:45 2015 +0100
     3.3 @@ -16,7 +16,7 @@
     3.4      {
     3.5       msetT : typ -> typ,
     3.6       mk_mset : typ -> term list -> term,
     3.7 -     mset_regroup_conv : int list -> conv,
     3.8 +     mset_regroup_conv : Proof.context -> int list -> conv,
     3.9       mset_member_tac : int -> int -> tactic,
    3.10       mset_nonempty_tac : int -> tactic,
    3.11       mset_pwleq_tac : int -> tactic,
    3.12 @@ -48,7 +48,7 @@
    3.13    {
    3.14     msetT : typ -> typ,
    3.15     mk_mset : typ -> term list -> term,
    3.16 -   mset_regroup_conv : int list -> conv,
    3.17 +   mset_regroup_conv : Proof.context -> int list -> conv,
    3.18     mset_member_tac : int -> int -> tactic,
    3.19     mset_nonempty_tac : int -> tactic,
    3.20     mset_pwleq_tac : int -> tactic,
    3.21 @@ -71,7 +71,7 @@
    3.22  
    3.23  fun undef _ = error "undef"
    3.24  
    3.25 -fun get_multiset_setup thy = Multiset_Setup.get thy
    3.26 +fun get_multiset_setup ctxt = Multiset_Setup.get (Proof_Context.theory_of ctxt)
    3.27    |> the_default (Multiset
    3.28      { msetT = undef, mk_mset=undef,
    3.29        mset_regroup_conv=undef, mset_member_tac = undef,
    3.30 @@ -145,12 +145,11 @@
    3.31  
    3.32  fun reconstruct_tac ctxt D cs (GP (_, gs)) certificate =
    3.33    let
    3.34 -    val thy = Proof_Context.theory_of ctxt
    3.35      val Multiset
    3.36            { msetT, mk_mset,
    3.37              mset_regroup_conv, mset_pwleq_tac, set_of_simps,
    3.38              smsI', wmsI2'', wmsI1, reduction_pair=ms_rp, ...}
    3.39 -        = get_multiset_setup thy
    3.40 +        = get_multiset_setup ctxt
    3.41  
    3.42      fun measure_fn p = nth (Termination.get_measures D p)
    3.43  
    3.44 @@ -239,8 +238,8 @@
    3.45                  fun t_conv a C =
    3.46                    params_conv ~1 (K ((concl_conv ~1 o arg_conv o arg1_conv o a) C)) ctxt
    3.47                  val goal_rewrite =
    3.48 -                    t_conv arg1_conv (mset_regroup_conv iqs)
    3.49 -                    then_conv t_conv arg_conv (mset_regroup_conv ips)
    3.50 +                    t_conv arg1_conv (mset_regroup_conv ctxt iqs)
    3.51 +                    then_conv t_conv arg_conv (mset_regroup_conv ctxt ips)
    3.52                  end
    3.53                in
    3.54                  CONVERSION goal_rewrite 1
    3.55 @@ -275,7 +274,7 @@
    3.56          |> Thm.cterm_of ctxt
    3.57      in
    3.58        PROFILE "Proof Reconstruction"
    3.59 -        (CONVERSION (Conv.arg_conv (Conv.arg_conv (Function_Lib.regroup_union_conv sl))) 1
    3.60 +        (CONVERSION (Conv.arg_conv (Conv.arg_conv (Function_Lib.regroup_union_conv ctxt sl))) 1
    3.61           THEN (rtac @{thm reduction_pair_lemma} 1)
    3.62           THEN (rtac @{thm rp_inv_image_rp} 1)
    3.63           THEN (rtac (order_rpair ms_rp label) 1)
     4.1 --- a/src/HOL/Tools/Function/termination.ML	Fri Mar 06 18:21:32 2015 +0100
     4.2 +++ b/src/HOL/Tools/Function/termination.ML	Fri Mar 06 20:08:45 2015 +0100
     4.3 @@ -331,7 +331,7 @@
     4.4     val is = map (fn c => find_index (curry op aconv c) cs') cs
     4.5   in
     4.6     CONVERSION (Conv.arg_conv (Conv.arg_conv
     4.7 -     (Function_Lib.regroup_union_conv is))) i
     4.8 +     (Function_Lib.regroup_union_conv ctxt is))) i
     4.9   end)
    4.10  
    4.11