# HG changeset patch # User traytel # Date 1443214891 -7200 # Node ID 0478ba10152a2ae19fa33954945ae90924eee676 # Parent 28eb608b9b5902e36a7b134118fba9b5ff4f76a7 more canonical context threading diff -r 28eb608b9b59 -r 0478ba10152a src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Fri Sep 25 23:41:24 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_def.ML Fri Sep 25 23:01:31 2015 +0200 @@ -1258,8 +1258,9 @@ val goal = fold_rev Logic.all (x :: x_copy :: fs @ fs_copy) (Logic.list_implies (prem0 :: prems, eq)); in - Goal.prove_sorry lthy [] [] goal (K (unfold_thms_tac lthy @{thms simp_implies_def} THEN - mk_map_cong_tac lthy (#map_cong0 axioms))) + Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => + unfold_thms_tac ctxt @{thms simp_implies_def} THEN + mk_map_cong_tac ctxt (#map_cong0 axioms)) |> Thm.close_derivation end; diff -r 28eb608b9b59 -r 0478ba10152a src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Fri Sep 25 23:41:24 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Fri Sep 25 23:01:31 2015 +0200 @@ -445,7 +445,8 @@ HOLogic.mk_Trueprop (mk_mor Bs ss B''s s''s (map2 (curry HOLogic.mk_comp) gs fs)); in Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl)) - (K (mk_mor_comp_tac lthy mor_def mor_image'_thms morE_thms map_comp_id_thms)) + (fn {context = ctxt, prems = _} => + mk_mor_comp_tac ctxt mor_def mor_image'_thms morE_thms map_comp_id_thms) |> Thm.close_derivation |> singleton (Proof_Context.export names_lthy lthy) end; @@ -457,7 +458,7 @@ val concl = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs_copy); in Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl)) - (K ((hyp_subst_tac lthy THEN' assume_tac lthy) 1)) + (fn {context = ctxt, prems = _} => (hyp_subst_tac ctxt THEN' assume_tac ctxt) 1) |> Thm.close_derivation |> singleton (Proof_Context.export names_lthy lthy) end; @@ -597,7 +598,7 @@ HOLogic.mk_Trueprop (mk_bis Bs ss B''s s''s (map2 (curry mk_rel_comp) Rs R's)); in Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl)) - (K (mk_bis_O_tac lthy m bis_rel_thm rel_congs le_rel_OOs)) + (fn {context = ctxt, prems = _} => mk_bis_O_tac ctxt m bis_rel_thm rel_congs le_rel_OOs) |> Thm.close_derivation |> singleton (Proof_Context.export names_lthy lthy) end; @@ -680,7 +681,8 @@ val sbis_lsbis_thm = Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (mk_sbis Bs ss (map (mk_lsbis Bs ss) ks))) - (K (mk_sbis_lsbis_tac lthy lsbis_defs bis_Union_thm bis_cong_thm)) + (fn {context = ctxt, prems = _} => + mk_sbis_lsbis_tac ctxt lsbis_defs bis_Union_thm bis_cong_thm) |> Thm.close_derivation |> singleton (Proof_Context.export names_lthy lthy); @@ -1102,7 +1104,7 @@ val length_Lev = Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal) - (K (mk_length_Lev_tac lthy cts Lev_0s Lev_Sucs)) + (fn {context = ctxt, prems = _} => mk_length_Lev_tac ctxt cts Lev_0s Lev_Sucs) |> Thm.close_derivation |> singleton (Proof_Context.export names_lthy lthy); @@ -1176,7 +1178,8 @@ val set_Lev = Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal) - (K (mk_set_Lev_tac lthy cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbd_thmss)) + (fn {context = ctxt, prems = _} => + mk_set_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbd_thmss) |> Thm.close_derivation |> singleton (Proof_Context.export names_lthy lthy); @@ -1215,8 +1218,9 @@ val set_image_Lev = Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal) - (K (mk_set_image_Lev_tac lthy cts Lev_0s Lev_Sucs rv_Nils rv_Conss - from_to_sbd_thmss to_sbd_inj_thmss)) + (fn {context = ctxt, prems = _} => + mk_set_image_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss + from_to_sbd_thmss to_sbd_inj_thmss) |> Thm.close_derivation |> singleton (Proof_Context.export names_lthy lthy); @@ -2161,8 +2165,9 @@ fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor => fn set_map0s => fn dtor_set_incls => fn dtor_set_set_inclss => Goal.prove_sorry lthy [] [] goal - (K (mk_dtor_rel_tac lthy in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets - dtor_inject dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss)) + (fn {context = ctxt, prems = _} => + mk_dtor_rel_tac ctxt in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets + dtor_inject dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss) |> Thm.close_derivation |> singleton (Proof_Context.export names_lthy lthy)) ks goals in_rels map_comps map_cong0s dtor_Jmap_thms dtor_Jset_thmss' diff -r 28eb608b9b59 -r 0478ba10152a src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Sep 25 23:41:24 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Sep 25 23:01:31 2015 +0200 @@ -1148,7 +1148,7 @@ fun exclude_tac tac_opt sequential (c, c', a) = if a orelse c = c' orelse sequential then - SOME (K (HEADGOAL (mk_primcorec_assumption_tac lthy []))) + SOME (fn {context = ctxt, prems = _} => HEADGOAL (mk_primcorec_assumption_tac ctxt [])) else tac_opt; @@ -1233,9 +1233,11 @@ |> list_all_fun_args ps |> @{map 3} (fn disc_eqns as {fun_args, ...} :: _ => fn [] => K [] | [nchotomy_thm] => fn [goal] => - [mk_primcorec_exhaust_tac lthy ("" (* for "P" *) :: map (fst o dest_Free) fun_args) - (length disc_eqns) nchotomy_thm - |> K |> Goal.prove_sorry lthy [] [] goal + [Goal.prove_sorry lthy [] [] goal + (fn {context = ctxt, prems = _} => + mk_primcorec_exhaust_tac ctxt + ("" (* for "P" *) :: map (fst o dest_Free) fun_args) + (length disc_eqns) nchotomy_thm) |> Thm.close_derivation]) disc_eqnss nchotomy_thmss; val nontriv_exhaust_thmss = map (filter_out is_trivial_implies) exhaust_thmss; @@ -1267,8 +1269,9 @@ if prems = [@{term False}] then [] else - mk_primcorec_disc_tac lthy def_thms corec_disc k m excludesss - |> K |> Goal.prove_sorry lthy [] [] goal + Goal.prove_sorry lthy [] [] goal + (fn {context = ctxt, prems = _} => + mk_primcorec_disc_tac ctxt def_thms corec_disc k m excludesss) |> Thm.close_derivation |> pair (#disc (nth ctr_specs ctr_no)) |> pair eqn_pos @@ -1297,9 +1300,10 @@ |> curry Logic.list_all (map dest_Free fun_args); val (distincts, _, _, split_sels, split_sel_asms) = case_thms_of_term lthy rhs_term; in - mk_primcorec_sel_tac lthy def_thms distincts split_sels split_sel_asms fp_nesting_maps - fp_nesting_map_ident0s fp_nesting_map_comps corec_sel k m excludesss - |> K |> Goal.prove_sorry lthy [] [] goal + Goal.prove_sorry lthy [] [] goal + (fn {context = ctxt, prems = _} => + mk_primcorec_sel_tac ctxt def_thms distincts split_sels split_sel_asms + fp_nesting_maps fp_nesting_map_ident0s fp_nesting_map_comps corec_sel k m excludesss) |> Thm.close_derivation |> `(is_some code_rhs_opt ? fold_thms lthy sel_defs) (*mildly too aggressive*) |> pair sel @@ -1346,8 +1350,9 @@ if prems = [@{term False}] then [] else - mk_primcorec_ctr_tac lthy m collapse disc_thm_opt sel_thms - |> K |> Goal.prove_sorry lthy [] [] goal + Goal.prove_sorry lthy [] [] goal + (fn {context = ctxt, prems = _} => + mk_primcorec_ctr_tac ctxt m collapse disc_thm_opt sel_thms) |> is_some code_rhs_opt ? fold_thms lthy sel_defs (*mildly too aggressive*) |> Thm.close_derivation |> pair ctr @@ -1431,14 +1436,16 @@ val (distincts, discIs, _, split_sels, split_sel_asms) = case_thms_of_term lthy raw_rhs; - val raw_code_thm = mk_primcorec_raw_code_tac lthy distincts discIs split_sels - split_sel_asms ms ctr_thms - (if exhaustive_code then try the_single nchotomys else NONE) - |> K |> Goal.prove_sorry lthy [] [] raw_goal + val raw_code_thm = + Goal.prove_sorry lthy [] [] raw_goal + (fn {context = ctxt, prems = _} => + mk_primcorec_raw_code_tac ctxt distincts discIs split_sels split_sel_asms + ms ctr_thms (if exhaustive_code then try the_single nchotomys else NONE)) |> Thm.close_derivation; in - mk_primcorec_code_tac lthy distincts split_sels raw_code_thm - |> K |> Goal.prove_sorry lthy [] [] goal + Goal.prove_sorry lthy [] [] goal + (fn {context = ctxt, prems = _} => + mk_primcorec_code_tac ctxt distincts split_sels raw_code_thm) |> Thm.close_derivation |> single end) @@ -1465,9 +1472,10 @@ mk_conjs prems) |> curry Logic.list_all (map dest_Free fun_args); in - mk_primcorec_disc_iff_tac lthy (map (fst o dest_Free) exhaust_fun_args) - (the_single exhaust_thms) disc_thms disc_thmss' (flat distinct_discss) - |> K |> Goal.prove_sorry lthy [] [] goal + Goal.prove_sorry lthy [] [] goal + (fn {context = ctxt, prems = _} => + mk_primcorec_disc_iff_tac ctxt (map (fst o dest_Free) exhaust_fun_args) + (the_single exhaust_thms) disc_thms disc_thmss' (flat distinct_discss)) |> Thm.close_derivation |> fold (fn rule => perhaps (try (fn thm => Meson.first_order_resolve lthy thm rule))) @{thms eqTrueE eq_False[THEN iffD1] notnotD} diff -r 28eb608b9b59 -r 0478ba10152a src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Fri Sep 25 23:41:24 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Fri Sep 25 23:01:31 2015 +0200 @@ -298,7 +298,8 @@ in map2 (fn goal => fn alg_set => Goal.prove_sorry lthy [] [] goal - (K (mk_alg_not_empty_tac lthy alg_set alg_set_thms wit_thms)) + (fn {context = ctxt, prems = _} => + mk_alg_not_empty_tac ctxt alg_set alg_set_thms wit_thms) |> Thm.close_derivation |> singleton (Proof_Context.export names_lthy lthy)) goals alg_set_thms @@ -606,7 +607,8 @@ val monos = map2 (fn goal => fn min_algs => - Goal.prove_sorry lthy [] [] goal (K (mk_min_algs_mono_tac lthy min_algs)) + Goal.prove_sorry lthy [] [] goal + (fn {context = ctxt, prems = _} => mk_min_algs_mono_tac ctxt min_algs) |> Thm.close_derivation |> singleton (Proof_Context.export names_lthy lthy)) (map mk_mono_goal min_algss) min_algs_thms; @@ -1255,8 +1257,9 @@ val goal = Logic.list_implies (prems, concl); in (Goal.prove_sorry lthy [] [] goal - (K (mk_ctor_induct_tac lthy m set_mapss init_induct_thm morE_thms mor_Abs_thm - Rep_inverses Abs_inverses Reps)) + (fn {context = ctxt, prems = _} => + mk_ctor_induct_tac ctxt m set_mapss init_induct_thm morE_thms mor_Abs_thm + Rep_inverses Abs_inverses Reps) |> Thm.close_derivation |> singleton (Proof_Context.export names_lthy lthy), rev (Term.add_tfrees goal [])) @@ -1696,8 +1699,9 @@ fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor => fn set_map0s => fn ctor_set_incls => fn ctor_set_set_inclss => Goal.prove_sorry lthy [] [] goal - (K (mk_ctor_rel_tac lthy in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets - ctor_inject ctor_dtor set_map0s ctor_set_incls ctor_set_set_inclss)) + (fn {context = ctxt, prems = _} => + mk_ctor_rel_tac ctxt in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets + ctor_inject ctor_dtor set_map0s ctor_set_incls ctor_set_set_inclss) |> Thm.close_derivation |> singleton (Proof_Context.export names_lthy lthy)) ks goals in_rels map_comps map_cong0s ctor_Imap_thms ctor_Iset_thmss' diff -r 28eb608b9b59 -r 0478ba10152a src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Fri Sep 25 23:41:24 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Fri Sep 25 23:01:31 2015 +0200 @@ -552,9 +552,10 @@ |> map_filter (try (fn (x, [y]) => (#user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y))) |> map (fn (user_eqn, num_extra_args, rec_thm) => - mk_primrec_tac lthy' num_extra_args fp_nesting_map_ident0s fp_nesting_map_comps - def_thms rec_thm - |> K |> Goal.prove_sorry lthy' [] [] user_eqn + Goal.prove_sorry lthy' [] [] user_eqn + (fn {context = ctxt, prems = _} => + mk_primrec_tac ctxt num_extra_args fp_nesting_map_ident0s fp_nesting_map_comps + def_thms rec_thm) |> Thm.close_derivation); in ((js, simps), lthy') diff -r 28eb608b9b59 -r 0478ba10152a src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Sep 25 23:41:24 2015 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Sep 25 23:01:31 2015 +0200 @@ -739,7 +739,8 @@ mk_Trueprop_eq (eta_ufcase, eta_vgcase)); val weak_goal = Logic.mk_implies (uv_eq, mk_Trueprop_eq (ufcase, vfcase)); in - (Goal.prove_sorry lthy [] [] goal (fn _ => mk_case_cong_tac lthy uexhaust_thm case_thms), + (Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => + mk_case_cong_tac ctxt uexhaust_thm case_thms), Goal.prove_sorry lthy [] [] weak_goal (fn {context = ctxt, prems = _} => etac ctxt arg_cong 1)) |> apply2 (singleton (Proof_Context.export names_lthy lthy) #> @@ -762,8 +763,8 @@ (@{map 3} mk_split_disjunct xctrs xss xfs))); fun prove_split selss goal = - Goal.prove_sorry lthy [] [] goal (fn _ => - mk_split_tac lthy ms uexhaust_thm case_thms selss inject_thmss distinct_thmsss) + Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => + mk_split_tac ctxt ms uexhaust_thm case_thms selss inject_thmss distinct_thmsss) |> singleton (Proof_Context.export names_lthy lthy) |> Thm.close_derivation; @@ -976,8 +977,8 @@ val uncollapse_thms = map2 (fn thm => fn [] => thm | _ => thm RS sym) all_collapse_thms uselss; in - Goal.prove_sorry lthy [] [] goal (fn _ => - mk_expand_tac lthy n ms (inst_thm u exhaust_disc_thm) + Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => + mk_expand_tac ctxt n ms (inst_thm u exhaust_disc_thm) (inst_thm v exhaust_disc_thm) uncollapse_thms distinct_disc_thmsss distinct_disc_thmsss') |> singleton (Proof_Context.export names_lthy lthy)