1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Mar 22 08:30:13 2010 +0100
1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Mar 22 08:30:13 2010 +0100
1.3 @@ -17,8 +17,8 @@
1.4 val is_registered : theory -> string -> bool
1.5 val function_name_of : Predicate_Compile_Aux.compilation -> theory
1.6 -> string -> bool * Predicate_Compile_Aux.mode -> string
1.7 - val predfun_intro_of: theory -> string -> Predicate_Compile_Aux.mode -> thm
1.8 - val predfun_elim_of: theory -> string -> Predicate_Compile_Aux.mode -> thm
1.9 + val predfun_intro_of: Proof.context -> string -> Predicate_Compile_Aux.mode -> thm
1.10 + val predfun_elim_of: Proof.context -> string -> Predicate_Compile_Aux.mode -> thm
1.11 val all_preds_of : theory -> string list
1.12 val modes_of: Predicate_Compile_Aux.compilation
1.13 -> theory -> string -> Predicate_Compile_Aux.mode list
1.14 @@ -244,7 +244,7 @@
1.15
1.16 fun the_elim_of thy name = case #elim (the_pred_data thy name)
1.17 of NONE => error ("No elimination rule for predicate " ^ quote name)
1.18 - | SOME thm => Thm.transfer thy thm
1.19 + | SOME thm => Thm.transfer thy thm
1.20
1.21 val has_elim = is_some o #elim oo the_pred_data;
1.22
1.23 @@ -282,13 +282,13 @@
1.24 " of predicate " ^ name)
1.25 | SOME data => data;
1.26
1.27 -val predfun_definition_of = #definition ooo the_predfun_data
1.28 +val predfun_definition_of = #definition ooo the_predfun_data o ProofContext.theory_of
1.29
1.30 -val predfun_intro_of = #intro ooo the_predfun_data
1.31 +val predfun_intro_of = #intro ooo the_predfun_data o ProofContext.theory_of
1.32
1.33 -val predfun_elim_of = #elim ooo the_predfun_data
1.34 +val predfun_elim_of = #elim ooo the_predfun_data o ProofContext.theory_of
1.35
1.36 -val predfun_neg_intro_of = #neg_intro ooo the_predfun_data
1.37 +val predfun_neg_intro_of = #neg_intro ooo the_predfun_data o ProofContext.theory_of
1.38
1.39 (* diagnostic display functions *)
1.40
1.41 @@ -1900,7 +1900,7 @@
1.42 (* MAJOR FIXME: prove_params should be simple
1.43 - different form of introrule for parameters ? *)
1.44
1.45 -fun prove_param options thy nargs t deriv =
1.46 +fun prove_param options ctxt nargs t deriv =
1.47 let
1.48 val (f, args) = strip_comb (Envir.eta_contract t)
1.49 val mode = head_mode_of deriv
1.50 @@ -1908,20 +1908,17 @@
1.51 val ho_args = ho_args_of mode args
1.52 val f_tac = case f of
1.53 Const (name, T) => simp_tac (HOL_basic_ss addsimps
1.54 - [@{thm eval_pred}, predfun_definition_of thy name mode,
1.55 + [@{thm eval_pred}, predfun_definition_of ctxt name mode,
1.56 @{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
1.57 @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
1.58 | Free _ =>
1.59 - (* rewrite with parameter equation *)
1.60 - (* test: *)
1.61 - Subgoal.FOCUS_PREMS (fn {context = ctxt, params = params, prems = prems,
1.62 - asms = a, concl = concl, schematics = s} =>
1.63 + Subgoal.FOCUS_PREMS (fn {context = ctxt, params = params, prems, asms, concl, schematics} =>
1.64 let
1.65 val prems' = maps dest_conjunct_prem (take nargs prems)
1.66 in
1.67 MetaSimplifier.rewrite_goal_tac
1.68 (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
1.69 - end) (ProofContext.init thy) 1 (* FIXME: proper context handling *)
1.70 + end) ctxt 1
1.71 | Abs _ => raise Fail "prove_param: No valid parameter term"
1.72 in
1.73 REPEAT_DETERM (rtac @{thm ext} 1)
1.74 @@ -1929,16 +1926,16 @@
1.75 THEN f_tac
1.76 THEN print_tac options "after prove_param"
1.77 THEN (REPEAT_DETERM (atac 1))
1.78 - THEN (EVERY (map2 (prove_param options thy nargs) ho_args param_derivations))
1.79 + THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations))
1.80 THEN REPEAT_DETERM (rtac @{thm refl} 1)
1.81 end
1.82
1.83 -fun prove_expr options thy nargs (premposition : int) (t, deriv) =
1.84 +fun prove_expr options ctxt nargs (premposition : int) (t, deriv) =
1.85 case strip_comb t of
1.86 (Const (name, T), args) =>
1.87 let
1.88 val mode = head_mode_of deriv
1.89 - val introrule = predfun_intro_of thy name mode
1.90 + val introrule = predfun_intro_of ctxt name mode
1.91 val param_derivations = param_derivations_of deriv
1.92 val ho_args = ho_args_of mode args
1.93 in
1.94 @@ -1950,13 +1947,12 @@
1.95 THEN atac 1
1.96 THEN print_tac options "parameter goal"
1.97 (* work with parameter arguments *)
1.98 - THEN (EVERY (map2 (prove_param options thy nargs) ho_args param_derivations))
1.99 + THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations))
1.100 THEN (REPEAT_DETERM (atac 1))
1.101 end
1.102 | (Free _, _) =>
1.103 print_tac options "proving parameter call.."
1.104 - THEN Subgoal.FOCUS_PREMS (fn {context = ctxt, params = params, prems = prems,
1.105 - asms = a, concl = cl, schematics = s} =>
1.106 + THEN Subgoal.FOCUS_PREMS (fn {context = ctxt, params, prems, asms, concl, schematics} =>
1.107 let
1.108 val param_prem = nth prems premposition
1.109 val (param, _) = strip_comb (HOLogic.dest_Trueprop (prop_of param_prem))
1.110 @@ -1970,14 +1966,14 @@
1.111 param_prem
1.112 in
1.113 rtac param_prem' 1
1.114 - end) (ProofContext.init thy) 1 (* FIXME: proper context handling *)
1.115 + end) ctxt 1
1.116 THEN print_tac options "after prove parameter call"
1.117
1.118 fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st;
1.119
1.120 fun SOLVEDALL tac st = FILTER (fn st' => nprems_of st' = 0) tac st
1.121
1.122 -fun check_format thy st =
1.123 +fun check_format ctxt st =
1.124 let
1.125 val concl' = Logic.strip_assums_concl (hd (prems_of st))
1.126 val concl = HOLogic.dest_Trueprop concl'
1.127 @@ -1992,8 +1988,9 @@
1.128 ((*tracing "expression is not valid";*) Seq.empty) (*error "check_format: wrong format"*)
1.129 end
1.130
1.131 -fun prove_match options thy (out_ts : term list) =
1.132 +fun prove_match options ctxt out_ts =
1.133 let
1.134 + val thy = ProofContext.theory_of ctxt
1.135 fun get_case_rewrite t =
1.136 if (is_constructor thy t) then let
1.137 val case_rewrites = (#case_rewrites (Datatype.the_info thy
1.138 @@ -2006,7 +2003,7 @@
1.139 (* make this simpset better! *)
1.140 asm_full_simp_tac (HOL_basic_ss' addsimps simprules) 1
1.141 THEN print_tac options "after prove_match:"
1.142 - THEN (DETERM (TRY (EqSubst.eqsubst_tac (ProofContext.init thy) [0] [@{thm HOL.if_P}] 1
1.143 + THEN (DETERM (TRY (EqSubst.eqsubst_tac ctxt [0] [@{thm HOL.if_P}] 1
1.144 THEN (REPEAT_DETERM (rtac @{thm conjI} 1 THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1))))
1.145 THEN print_tac options "if condition to be solved:"
1.146 THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1 THEN print_tac options "after if simp; in SOLVED:"))
1.147 @@ -2017,8 +2014,9 @@
1.148
1.149 (* corresponds to compile_fun -- maybe call that also compile_sidecond? *)
1.150
1.151 -fun prove_sidecond thy t =
1.152 +fun prove_sidecond ctxt t =
1.153 let
1.154 + val thy = ProofContext.theory_of ctxt
1.155 fun preds_of t nameTs = case strip_comb t of
1.156 (f as Const (name, T), args) =>
1.157 if is_registered thy name then (name, T) :: nameTs
1.158 @@ -2026,7 +2024,7 @@
1.159 | _ => nameTs
1.160 val preds = preds_of t []
1.161 val defs = map
1.162 - (fn (pred, T) => predfun_definition_of thy pred
1.163 + (fn (pred, T) => predfun_definition_of ctxt pred
1.164 (all_input_of T))
1.165 preds
1.166 in
1.167 @@ -2036,11 +2034,11 @@
1.168 (* need better control here! *)
1.169 end
1.170
1.171 -fun prove_clause options thy nargs mode (_, clauses) (ts, moded_ps) =
1.172 +fun prove_clause options ctxt nargs mode (_, clauses) (ts, moded_ps) =
1.173 let
1.174 val (in_ts, clause_out_ts) = split_mode mode ts;
1.175 fun prove_prems out_ts [] =
1.176 - (prove_match options thy out_ts)
1.177 + (prove_match options ctxt out_ts)
1.178 THEN print_tac options "before simplifying assumptions"
1.179 THEN asm_full_simp_tac HOL_basic_ss' 1
1.180 THEN print_tac options "before single intro rule"
1.181 @@ -2060,7 +2058,7 @@
1.182 print_tac options "before clause:"
1.183 (*THEN asm_simp_tac HOL_basic_ss 1*)
1.184 THEN print_tac options "before prove_expr:"
1.185 - THEN prove_expr options thy nargs premposition (t, deriv)
1.186 + THEN prove_expr options ctxt nargs premposition (t, deriv)
1.187 THEN print_tac options "after prove_expr:"
1.188 THEN rec_tac
1.189 end
1.190 @@ -2071,7 +2069,8 @@
1.191 val rec_tac = prove_prems out_ts''' ps
1.192 val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
1.193 val neg_intro_rule =
1.194 - Option.map (fn name => the (predfun_neg_intro_of thy name mode)) name
1.195 + Option.map (fn name =>
1.196 + the (predfun_neg_intro_of ctxt name mode)) name
1.197 val param_derivations = param_derivations_of deriv
1.198 val params = ho_args_of mode args
1.199 in
1.200 @@ -2085,7 +2084,7 @@
1.201 THEN etac (the neg_intro_rule) 1
1.202 THEN rotate_tac (~premposition) 1
1.203 THEN print_tac options "after applying not introduction rule"
1.204 - THEN (EVERY (map2 (prove_param options thy nargs) params param_derivations))
1.205 + THEN (EVERY (map2 (prove_param options ctxt nargs) params param_derivations))
1.206 THEN (REPEAT_DETERM (atac 1))
1.207 else
1.208 rtac @{thm not_predI'} 1
1.209 @@ -2098,10 +2097,10 @@
1.210 | Sidecond t =>
1.211 rtac @{thm if_predI} 1
1.212 THEN print_tac options "before sidecond:"
1.213 - THEN prove_sidecond thy t
1.214 + THEN prove_sidecond ctxt t
1.215 THEN print_tac options "after sidecond:"
1.216 THEN prove_prems [] ps)
1.217 - in (prove_match options thy out_ts)
1.218 + in (prove_match options ctxt out_ts)
1.219 THEN rest_tac
1.220 end;
1.221 val prems_tac = prove_prems in_ts moded_ps
1.222 @@ -2116,51 +2115,55 @@
1.223 | select_sup _ 1 = [rtac @{thm supI1}]
1.224 | select_sup n i = (rtac @{thm supI2})::(select_sup (n - 1) (i - 1));
1.225
1.226 -fun prove_one_direction options thy clauses preds pred mode moded_clauses =
1.227 +fun prove_one_direction options ctxt clauses preds pred mode moded_clauses =
1.228 let
1.229 + val thy = ProofContext.theory_of ctxt
1.230 val T = the (AList.lookup (op =) preds pred)
1.231 val nargs = length (binder_types T)
1.232 val pred_case_rule = the_elim_of thy pred
1.233 in
1.234 REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"}))
1.235 THEN print_tac options "before applying elim rule"
1.236 - THEN etac (predfun_elim_of thy pred mode) 1
1.237 + THEN etac (predfun_elim_of ctxt pred mode) 1
1.238 THEN etac pred_case_rule 1
1.239 THEN print_tac options "after applying elim rule"
1.240 THEN (EVERY (map
1.241 (fn i => EVERY' (select_sup (length moded_clauses) i) i)
1.242 (1 upto (length moded_clauses))))
1.243 - THEN (EVERY (map2 (prove_clause options thy nargs mode) clauses moded_clauses))
1.244 + THEN (EVERY (map2 (prove_clause options ctxt nargs mode) clauses moded_clauses))
1.245 THEN print_tac options "proved one direction"
1.246 end;
1.247
1.248 (** Proof in the other direction **)
1.249
1.250 -fun prove_match2 options thy out_ts = let
1.251 - fun split_term_tac (Free _) = all_tac
1.252 - | split_term_tac t =
1.253 - if (is_constructor thy t) then let
1.254 - val info = Datatype.the_info thy ((fst o dest_Type o fastype_of) t)
1.255 - val num_of_constrs = length (#case_rewrites info)
1.256 - (* special treatment of pairs -- because of fishing *)
1.257 - val split_rules = case (fst o dest_Type o fastype_of) t of
1.258 - "*" => [@{thm prod.split_asm}]
1.259 - | _ => PureThy.get_thms thy (((fst o dest_Type o fastype_of) t) ^ ".split_asm")
1.260 - val (_, ts) = strip_comb t
1.261 - in
1.262 - (print_tac options ("Term " ^ (Syntax.string_of_term_global thy t) ^
1.263 - "splitting with rules \n" ^
1.264 - commas (map (Display.string_of_thm_global thy) split_rules)))
1.265 - THEN TRY ((Splitter.split_asm_tac split_rules 1)
1.266 - THEN (print_tac options "after splitting with split_asm rules")
1.267 - (* THEN (Simplifier.asm_full_simp_tac HOL_basic_ss 1)
1.268 - THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*)
1.269 - THEN (REPEAT_DETERM_N (num_of_constrs - 1)
1.270 - (etac @{thm botE} 1 ORELSE etac @{thm botE} 2)))
1.271 - THEN (assert_tac (Max_number_of_subgoals 2))
1.272 - THEN (EVERY (map split_term_tac ts))
1.273 - end
1.274 - else all_tac
1.275 +fun prove_match2 options ctxt out_ts =
1.276 + let
1.277 + val thy = ProofContext.theory_of ctxt
1.278 + fun split_term_tac (Free _) = all_tac
1.279 + | split_term_tac t =
1.280 + if (is_constructor thy t) then
1.281 + let
1.282 + val info = Datatype.the_info thy ((fst o dest_Type o fastype_of) t)
1.283 + val num_of_constrs = length (#case_rewrites info)
1.284 + (* special treatment of pairs -- because of fishing *)
1.285 + val split_rules = case (fst o dest_Type o fastype_of) t of
1.286 + "*" => [@{thm prod.split_asm}]
1.287 + | _ => PureThy.get_thms thy (((fst o dest_Type o fastype_of) t) ^ ".split_asm")
1.288 + val (_, ts) = strip_comb t
1.289 + in
1.290 + (print_tac options ("Term " ^ (Syntax.string_of_term ctxt t) ^
1.291 + "splitting with rules \n" ^
1.292 + commas (map (Display.string_of_thm ctxt) split_rules)))
1.293 + THEN TRY ((Splitter.split_asm_tac split_rules 1)
1.294 + THEN (print_tac options "after splitting with split_asm rules")
1.295 + (* THEN (Simplifier.asm_full_simp_tac HOL_basic_ss 1)
1.296 + THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*)
1.297 + THEN (REPEAT_DETERM_N (num_of_constrs - 1)
1.298 + (etac @{thm botE} 1 ORELSE etac @{thm botE} 2)))
1.299 + THEN (assert_tac (Max_number_of_subgoals 2))
1.300 + THEN (EVERY (map split_term_tac ts))
1.301 + end
1.302 + else all_tac
1.303 in
1.304 split_term_tac (HOLogic.mk_tuple out_ts)
1.305 THEN (DETERM (TRY ((Splitter.split_asm_tac [@{thm "split_if_asm"}] 1)
1.306 @@ -2172,7 +2175,7 @@
1.307 *)
1.308 (* TODO: remove function *)
1.309
1.310 -fun prove_param2 options thy t deriv =
1.311 +fun prove_param2 options ctxt t deriv =
1.312 let
1.313 val (f, args) = strip_comb (Envir.eta_contract t)
1.314 val mode = head_mode_of deriv
1.315 @@ -2180,7 +2183,7 @@
1.316 val ho_args = ho_args_of mode args
1.317 val f_tac = case f of
1.318 Const (name, T) => full_simp_tac (HOL_basic_ss addsimps
1.319 - (@{thm eval_pred}::(predfun_definition_of thy name mode)
1.320 + (@{thm eval_pred}::(predfun_definition_of ctxt name mode)
1.321 :: @{thm "Product_Type.split_conv"}::[])) 1
1.322 | Free _ => all_tac
1.323 | _ => error "prove_param2: illegal parameter term"
1.324 @@ -2188,10 +2191,10 @@
1.325 print_tac options "before simplification in prove_args:"
1.326 THEN f_tac
1.327 THEN print_tac options "after simplification in prove_args"
1.328 - THEN EVERY (map2 (prove_param2 options thy) ho_args param_derivations)
1.329 + THEN EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations)
1.330 end
1.331
1.332 -fun prove_expr2 options thy (t, deriv) =
1.333 +fun prove_expr2 options ctxt (t, deriv) =
1.334 (case strip_comb t of
1.335 (Const (name, T), args) =>
1.336 let
1.337 @@ -2202,25 +2205,22 @@
1.338 etac @{thm bindE} 1
1.339 THEN (REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"})))
1.340 THEN print_tac options "prove_expr2-before"
1.341 - THEN etac (predfun_elim_of thy name mode) 1
1.342 + THEN etac (predfun_elim_of ctxt name mode) 1
1.343 THEN print_tac options "prove_expr2"
1.344 - THEN (EVERY (map2 (prove_param2 options thy) ho_args param_derivations))
1.345 + THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations))
1.346 THEN print_tac options "finished prove_expr2"
1.347 end
1.348 | _ => etac @{thm bindE} 1)
1.349
1.350 -(* FIXME: what is this for? *)
1.351 -(* replace defined by has_mode thy pred *)
1.352 -(* TODO: rewrite function *)
1.353 -fun prove_sidecond2 options thy t = let
1.354 +fun prove_sidecond2 options ctxt t = let
1.355 fun preds_of t nameTs = case strip_comb t of
1.356 (f as Const (name, T), args) =>
1.357 - if is_registered thy name then (name, T) :: nameTs
1.358 + if is_registered (ProofContext.theory_of ctxt) name then (name, T) :: nameTs
1.359 else fold preds_of args nameTs
1.360 | _ => nameTs
1.361 val preds = preds_of t []
1.362 val defs = map
1.363 - (fn (pred, T) => predfun_definition_of thy pred
1.364 + (fn (pred, T) => predfun_definition_of ctxt pred
1.365 (all_input_of T))
1.366 preds
1.367 in
1.368 @@ -2230,13 +2230,13 @@
1.369 THEN print_tac options "after sidecond2 simplification"
1.370 end
1.371
1.372 -fun prove_clause2 options thy pred mode (ts, ps) i =
1.373 +fun prove_clause2 options ctxt pred mode (ts, ps) i =
1.374 let
1.375 - val pred_intro_rule = nth (intros_of thy pred) (i - 1)
1.376 + val pred_intro_rule = nth (intros_of (ProofContext.theory_of ctxt) pred) (i - 1)
1.377 val (in_ts, clause_out_ts) = split_mode mode ts;
1.378 fun prove_prems2 out_ts [] =
1.379 print_tac options "before prove_match2 - last call:"
1.380 - THEN prove_match2 options thy out_ts
1.381 + THEN prove_match2 options ctxt out_ts
1.382 THEN print_tac options "after prove_match2 - last call:"
1.383 THEN (etac @{thm singleE} 1)
1.384 THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
1.385 @@ -2262,7 +2262,7 @@
1.386 val (_, out_ts''') = split_mode mode us
1.387 val rec_tac = prove_prems2 out_ts''' ps
1.388 in
1.389 - (prove_expr2 options thy (t, deriv)) THEN rec_tac
1.390 + (prove_expr2 options ctxt (t, deriv)) THEN rec_tac
1.391 end
1.392 | Negprem t =>
1.393 let
1.394 @@ -2277,10 +2277,10 @@
1.395 THEN etac @{thm bindE} 1
1.396 THEN (if is_some name then
1.397 full_simp_tac (HOL_basic_ss addsimps
1.398 - [predfun_definition_of thy (the name) mode]) 1
1.399 + [predfun_definition_of ctxt (the name) mode]) 1
1.400 THEN etac @{thm not_predE} 1
1.401 THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
1.402 - THEN (EVERY (map2 (prove_param2 options thy) ho_args param_derivations))
1.403 + THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations))
1.404 else
1.405 etac @{thm not_predE'} 1)
1.406 THEN rec_tac
1.407 @@ -2288,10 +2288,10 @@
1.408 | Sidecond t =>
1.409 etac @{thm bindE} 1
1.410 THEN etac @{thm if_predE} 1
1.411 - THEN prove_sidecond2 options thy t
1.412 + THEN prove_sidecond2 options ctxt t
1.413 THEN prove_prems2 [] ps)
1.414 in print_tac options "before prove_match2:"
1.415 - THEN prove_match2 options thy out_ts
1.416 + THEN prove_match2 options ctxt out_ts
1.417 THEN print_tac options "after prove_match2:"
1.418 THEN rest_tac
1.419 end;
1.420 @@ -2305,15 +2305,15 @@
1.421 THEN prems_tac
1.422 end;
1.423
1.424 -fun prove_other_direction options thy pred mode moded_clauses =
1.425 +fun prove_other_direction options ctxt pred mode moded_clauses =
1.426 let
1.427 fun prove_clause clause i =
1.428 (if i < length moded_clauses then etac @{thm supE} 1 else all_tac)
1.429 - THEN (prove_clause2 options thy pred mode clause i)
1.430 + THEN (prove_clause2 options ctxt pred mode clause i)
1.431 in
1.432 (DETERM (TRY (rtac @{thm unit.induct} 1)))
1.433 THEN (REPEAT_DETERM (CHANGED (rewtac @{thm split_paired_all})))
1.434 - THEN (rtac (predfun_intro_of thy pred mode) 1)
1.435 + THEN (rtac (predfun_intro_of ctxt pred mode) 1)
1.436 THEN (REPEAT_DETERM (rtac @{thm refl} 2))
1.437 THEN (if null moded_clauses then
1.438 etac @{thm botE} 1
1.439 @@ -2332,9 +2332,9 @@
1.440 (fn _ =>
1.441 rtac @{thm pred_iffI} 1
1.442 THEN print_tac options "after pred_iffI"
1.443 - THEN prove_one_direction options thy clauses preds pred mode moded_clauses
1.444 + THEN prove_one_direction options ctxt clauses preds pred mode moded_clauses
1.445 THEN print_tac options "proved one direction"
1.446 - THEN prove_other_direction options thy pred mode moded_clauses
1.447 + THEN prove_other_direction options ctxt pred mode moded_clauses
1.448 THEN print_tac options "proved other direction")
1.449 else (fn _ => Skip_Proof.cheat_tac thy))
1.450 end;
1.451 @@ -2478,6 +2478,7 @@
1.452
1.453 fun add_code_equations thy preds result_thmss =
1.454 let
1.455 + val ctxt = ProofContext.init thy
1.456 fun add_code_equation (predname, T) (pred, result_thms) =
1.457 let
1.458 val full_mode = fold_rev (curry Fun) (map (K Input) (binder_types T)) Bool
1.459 @@ -2493,10 +2494,10 @@
1.460 val rhs = @{term Predicate.holds} $ (list_comb (predfun, args))
1.461 val eq_term = HOLogic.mk_Trueprop
1.462 (HOLogic.mk_eq (list_comb (Const (predname, T), args), rhs))
1.463 - val def = predfun_definition_of thy predname full_mode
1.464 + val def = predfun_definition_of ctxt predname full_mode
1.465 val tac = fn _ => Simplifier.simp_tac
1.466 (HOL_basic_ss addsimps [def, @{thm holds_eq}, @{thm eval_pred}]) 1
1.467 - val eq = Goal.prove (ProofContext.init thy) arg_names [] eq_term tac
1.468 + val eq = Goal.prove ctxt arg_names [] eq_term tac
1.469 in
1.470 (pred, result_thms @ [eq])
1.471 end