--- a/src/HOL/HOLCF/Tools/cont_proc.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/HOLCF/Tools/cont_proc.ML Fri Aug 09 17:14:49 2019 +0200
@@ -57,7 +57,7 @@
let
(* should use "close_derivation" for thms that are used multiple times *)
(* it seems to allow for sharing in explicit proof objects *)
- val x' = Thm.close_derivation (k x)
+ val x' = Thm.close_derivation \<^here> (k x)
val Lx = x' RS cont_L
in (map (fn y => SOME (k y RS Lx)) ys, x') end
--- a/src/HOL/Tools/BNF/bnf_axiomatization.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_axiomatization.ML Fri Aug 09 17:14:49 2019 +0200
@@ -89,7 +89,7 @@
fun mk_wit_thms set_maps =
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
(fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> Conjunction.elim_balanced (length wit_goals)
|> map2 (Conjunction.elim_balanced o length) wit_goalss
|> (map o map) (Thm.forall_elim_vars 0);
--- a/src/HOL/Tools/BNF/bnf_comp.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Fri Aug 09 17:14:49 2019 +0200
@@ -252,7 +252,7 @@
mk_simplified_set_tac ctxt (collect_set_map_of_bnf outer);
val set'_eq_set =
Goal.prove (*no sorry*) names_lthy [] [] goal tac
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
val set' = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of set'_eq_set)));
in
(set', set'_eq_set)
@@ -274,7 +274,7 @@
val goal = mk_Trueprop_mem (bd_bd', ordIso);
in
(bd', SOME (Goal.prove_sorry lthy [] [] goal (bd_ordIso_natLeq_tac o #context)
- |> Thm.close_derivation))
+ |> Thm.close_derivation \<^here>))
end
else
(bd, NONE);
@@ -308,7 +308,7 @@
Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} =>
mk_comp_set_alt_tac ctxt (collect_set_map_of_bnf outer))
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
(map2 (curry mk_Trueprop_eq) sets sets_alt);
fun map_cong0_tac ctxt =
@@ -342,7 +342,7 @@
in
Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} => mk_comp_in_alt_tac ctxt set_alt_thms)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun le_rel_OO_tac ctxt = mk_le_rel_OO_tac ctxt (le_rel_OO_of_bnf outer) (rel_mono_of_bnf outer)
@@ -465,7 +465,7 @@
val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
in
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
- kill_in_alt_tac ctxt) |> Thm.close_derivation
+ kill_in_alt_tac ctxt) |> Thm.close_derivation \<^here>
end;
fun le_rel_OO_tac ctxt =
@@ -579,7 +579,7 @@
val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
in
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => lift_in_alt_tac ctxt)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun le_rel_OO_tac ctxt = rtac ctxt (le_rel_OO_of_bnf bnf) 1;
@@ -667,7 +667,7 @@
in
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
mk_permute_in_alt_tac ctxt src dest)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun le_rel_OO_tac ctxt = rtac ctxt (le_rel_OO_of_bnf bnf) 1;
--- a/src/HOL/Tools/BNF/bnf_def.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Fri Aug 09 17:14:49 2019 +0200
@@ -1449,7 +1449,7 @@
in
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
mk_collect_set_map_tac ctxt (#set_map0 axioms))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val collect_set_map = Lazy.lazy mk_collect_set_map;
@@ -1464,7 +1464,7 @@
in
Goal.prove_sorry lthy [] [] in_mono_goal (fn {context = ctxt, prems = _} =>
mk_in_mono_tac ctxt live)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val in_mono = Lazy.lazy mk_in_mono;
@@ -1479,7 +1479,7 @@
in
Goal.prove_sorry lthy [] [] in_cong_goal
(fn {context = ctxt, prems = _} => (TRY o hyp_subst_tac ctxt THEN' rtac ctxt refl) 1)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val in_cong = Lazy.lazy mk_in_cong;
@@ -1501,7 +1501,7 @@
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
+ |> Thm.close_derivation \<^here>
end;
val map_cong = Lazy.lazy (mk_map_cong Logic.mk_implies);
@@ -1516,7 +1516,7 @@
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
mk_inj_map_tac ctxt live (Lazy.force map_id) (Lazy.force map_comp) (#map_cong0 axioms)
(Lazy.force map_cong))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val inj_map = Lazy.lazy mk_inj_map;
@@ -1560,7 +1560,7 @@
(Lazy.force map_comp) (Lazy.force map_id) (#map_cong0 axioms)
(map Lazy.force set_map) (#set_bd axioms) (#bd_card_order axioms)
bd_Card_order bd_Cinfinite bd_Cnotzero)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val in_bd = Lazy.lazy mk_in_bd;
@@ -1578,7 +1578,7 @@
(fn {context = ctxt, prems = _} => mk_rel_Grp_tac ctxt rel_OO_Grps (#map_id0 axioms)
(#map_cong0 axioms) (Lazy.force map_id) (Lazy.force map_comp)
(map Lazy.force set_map))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val rel_Grp = Lazy.lazy mk_rel_Grp;
@@ -1596,7 +1596,7 @@
(fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (mono_prems, mono_concl)))
(fn {context = ctxt, prems = _} =>
mk_rel_mono_tac ctxt rel_OO_Grps (Lazy.force in_mono))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun mk_rel_cong0 () =
@@ -1607,7 +1607,7 @@
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (cong_prems, cong_concl)))
(fn {context = ctxt, prems = _} => (TRY o hyp_subst_tac ctxt THEN' rtac ctxt refl) 1)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val rel_mono = Lazy.lazy mk_rel_mono;
@@ -1619,7 +1619,7 @@
HOLogic.eq_const CA'))
(fn {context = ctxt, prems = _} =>
mk_rel_eq_tac ctxt live (Lazy.force rel_Grp) (Lazy.force rel_cong0) (#map_id0 axioms))
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
val rel_eq = Lazy.lazy mk_rel_eq;
@@ -1633,13 +1633,13 @@
(fn {context = ctxt, prems = _} => mk_rel_conversep_le_tac ctxt rel_OO_Grps
(Lazy.force rel_eq) (#map_cong0 axioms) (Lazy.force map_comp)
(map Lazy.force set_map))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
val goal = fold_rev Logic.all Rs (mk_Trueprop_eq (lhs, rhs));
in
Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} =>
mk_rel_conversep_tac ctxt le_thm (Lazy.force rel_mono))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val rel_conversep = Lazy.lazy mk_rel_conversep;
@@ -1649,7 +1649,7 @@
(fold_rev Logic.all (Rs @ Ss) (HOLogic.mk_Trueprop (mk_leq rel_OO_lhs rel_OO_rhs)))
(fn {context = ctxt, prems = _} => mk_rel_OO_le_tac ctxt rel_OO_Grps (Lazy.force rel_eq)
(#map_cong0 axioms) (Lazy.force map_comp) (map Lazy.force set_map))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> (fn thm => @{thm antisym} OF [thm, #le_rel_OO axioms]);
val rel_OO = Lazy.lazy mk_rel_OO;
@@ -1679,7 +1679,7 @@
(fold_rev Logic.all (x :: y :: Rs @ Rs_copy) (Logic.list_implies (prems, concl)))
(fn {context = ctxt, prems = _} => mk_rel_mono_strong0_tac ctxt (Lazy.force in_rel)
(map Lazy.force set_map))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val rel_mono_strong0 = Lazy.lazy mk_rel_mono_strong0;
@@ -1704,7 +1704,7 @@
|> (fn vars => Goal.prove_sorry lthy vars (prem0 :: prem1 :: prems) eq
(fn {context = ctxt, prems} =>
mk_rel_cong_tac ctxt (chop 2 prems) (Lazy.force rel_mono_strong)))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val rel_cong = Lazy.lazy (mk_rel_cong Logic.mk_implies);
@@ -1722,7 +1722,7 @@
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (Ps @ Ps_copy) (Logic.list_implies (cong_prems, cong_concl)))
(fn {context = ctxt, prems = _} => (TRY o hyp_subst_tac ctxt THEN' rtac ctxt refl) 1)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val pred_cong0 = Lazy.lazy mk_pred_cong0;
@@ -1735,7 +1735,7 @@
Goal.prove_sorry lthy (map fst Ps') [] (mk_Trueprop_eq (lhs, rhs))
(fn {context = ctxt, prems = _} =>
mk_rel_eq_onp_tac ctxt (#pred_set axioms) (#map_id0 axioms) (Lazy.force rel_Grp))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val rel_eq_onp = Lazy.lazy mk_rel_eq_onp;
@@ -1754,7 +1754,7 @@
(fold_rev Logic.all (x :: Ps @ Ps_copy) (Logic.list_implies (prems, concl)))
(fn {context = ctxt, prems = _} =>
mk_pred_mono_strong0_tac ctxt (Lazy.force pred_rel) (Lazy.force rel_mono_strong0))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val pred_mono_strong0 = Lazy.lazy mk_pred_mono_strong0;
@@ -1770,7 +1770,7 @@
(fold_rev Logic.all (Ps @ Ps_copy) (Logic.list_implies (mono_prems, mono_concl)))
(fn {context = ctxt, prems = _} =>
mk_pred_mono_tac ctxt (Lazy.force rel_eq_onp) (Lazy.force rel_mono))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val pred_mono = Lazy.lazy mk_pred_mono;
@@ -1790,7 +1790,7 @@
|> (fn vars => Goal.prove_sorry lthy vars (prem0 :: prems) eq
(fn {context = ctxt, prems} =>
mk_rel_cong_tac ctxt (chop 1 prems) (Lazy.force pred_mono_strong)))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val pred_cong = Lazy.lazy (mk_pred_cong Logic.mk_implies);
@@ -1812,7 +1812,7 @@
HEADGOAL (EVERY' [REPEAT_DETERM o etac ctxt conjE,
etac ctxt (Lazy.force map_cong) THEN_ALL_NEW
(etac ctxt @{thm bspec} THEN' assume_tac ctxt)]))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val map_cong_pred = Lazy.lazy mk_map_cong_pred;
@@ -1839,7 +1839,7 @@
(Lazy.force rel_Grp) (Lazy.force map_id)))
|> map (unfold_thms lthy @{thms vimage2p_def[of id, simplified id_apply]
vimage2p_def[of _ id, simplified id_apply]})
- |> map Thm.close_derivation
+ |> map (Thm.close_derivation \<^here>)
end;
val rel_map = Lazy.lazy mk_rel_map;
@@ -1869,7 +1869,7 @@
unfold_thms_tac ctxt [prop_conv_thm] THEN
HEADGOAL (rtac ctxt (Lazy.force thm RS sym RS @{thm ord_eq_le_trans})
THEN' rtac ctxt (Lazy.force rel_mono) THEN_ALL_NEW assume_tac ctxt))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val rel_reflp = Lazy.lazy (mk_rel_preserves mk_reflp @{thm reflp_eq} rel_eq);
@@ -1888,7 +1888,7 @@
Lazy.force rel_cong0 RS fun_cong RS fun_cong RS trans OF
replicate live @{thm eq_onp_True},
Lazy.force rel_eq RS fun_cong RS fun_cong RS trans, @{thm eqTrueI[OF refl]}])))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val pred_True = Lazy.lazy mk_pred_True;
@@ -1907,7 +1907,7 @@
unfold_thms_tac ctxt
(@{thms Ball_image_comp ball_empty} @ map Lazy.force set_map) THEN
HEADGOAL (rtac ctxt refl))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val pred_map = Lazy.lazy mk_pred_map;
@@ -1926,7 +1926,7 @@
(fn {context = ctxt, prems = _} => mk_map_transfer_tac ctxt (Lazy.force rel_mono)
(Lazy.force in_rel) (map Lazy.force set_map) (#map_cong0 axioms)
(Lazy.force map_comp))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val map_transfer = Lazy.lazy mk_map_transfer;
@@ -1943,7 +1943,7 @@
Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
mk_pred_transfer_tac ctxt live (Lazy.force in_rel) (Lazy.force pred_map)
(Lazy.force pred_cong))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val pred_transfer = Lazy.lazy mk_pred_transfer;
@@ -1964,7 +1964,7 @@
(fn {context = ctxt, prems = _} =>
mk_rel_transfer_tac ctxt (Lazy.force in_rel) (Lazy.force rel_map)
(Lazy.force rel_mono_strong))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val rel_transfer = Lazy.lazy mk_rel_transfer;
@@ -1985,7 +1985,7 @@
Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} =>
mk_set_transfer_tac ctxt (Lazy.force in_rel) (map Lazy.force set_map))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> Conjunction.elim_balanced (length goals)
end
end;
@@ -2011,7 +2011,7 @@
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
mk_inj_map_strong_tac ctxt (Lazy.force rel_eq) (Lazy.force rel_map)
(Lazy.force rel_mono_strong))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val inj_map_strong = Lazy.lazy mk_inj_map_strong;
@@ -2074,12 +2074,12 @@
fun mk_wit_thms set_maps =
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
(fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> Conjunction.elim_balanced (length wit_goals)
|> map2 (Conjunction.elim_balanced o length) wit_goalss
|> (map o map) (Thm.forall_elim_vars 0);
in
- map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])
+ map2 (Thm.close_derivation \<^here> oo Goal.prove_sorry lthy [] [])
goals (map (fn tac => fn {context = ctxt, prems = _} =>
unfold_thms_tac ctxt one_step_defs THEN tac ctxt) tacs)
|> (fn thms => after_qed mk_wit_thms (map single thms) lthy)
@@ -2094,7 +2094,7 @@
fun mk_triv_wit_thms tac set_maps =
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
(fn {context = ctxt, prems = _} => TRYALL Goal.conjunction_tac THEN tac ctxt set_maps)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> Conjunction.elim_balanced (length wit_goals)
|> map2 (Conjunction.elim_balanced o length) wit_goalss
|> (map o map) (Thm.forall_elim_vars 0);
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Aug 09 17:14:49 2019 +0200
@@ -655,7 +655,7 @@
Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} =>
mk_ctor_iff_dtor_tac ctxt (map (SOME o Thm.ctyp_of lthy) [ctor_absT, fpT])
(Thm.cterm_of lthy ctor) (Thm.cterm_of lthy dtor) ctor_dtor dtor_ctor)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val ctr_rhss =
@@ -784,7 +784,7 @@
mk_rel_case_tac ctxt (Thm.cterm_of ctxt ta) (Thm.cterm_of ctxt tb) exhaust injects
rel_inject_thms distincts rel_distinct_thms live_nesting_rel_eqs)
|> singleton (Proof_Context.export names_lthy lthy)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_case_transfer rel_case_thm =
@@ -797,7 +797,7 @@
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
mk_case_transfer_tac ctxt rel_case_thm case_thms)
|> singleton (Proof_Context.export names_lthy lthy)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
in
if live = 0 then
@@ -877,7 +877,7 @@
Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
mk_map_tac ctxt abs_inverses pre_map_def map_ctor_thm live_nesting_map_id0s ctr_defs'
extra_unfolds_map)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> Conjunction.elim_balanced (length goals)
end;
@@ -906,7 +906,7 @@
Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
mk_set0_tac ctxt abs_inverses pre_set_defs dtor_ctor fp_set_thms
fp_nesting_set_maps live_nesting_set_maps ctr_defs' extra_unfolds_set)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> Conjunction.elim_balanced (length goals)
end
end;
@@ -953,7 +953,7 @@
Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
mk_rel_tac ctxt abs_inverses pre_rel_def rel_ctor_thm live_nesting_rel_eqs ctr_defs'
extra_unfolds_rel)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> Conjunction.elim_balanced (length goals)
end;
@@ -979,7 +979,7 @@
Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
mk_rel_tac ctxt abs_inverses pre_rel_def rel_ctor_thm live_nesting_rel_eqs
ctr_defs' extra_unfolds_rel)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> Conjunction.elim_balanced (length goals)
end)
end;
@@ -1012,7 +1012,7 @@
Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} =>
mk_ctr_transfer_tac ctxt rel_intro_thms live_nesting_rel_eqs)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> Conjunction.elim_balanced (length goals)
end;
@@ -1066,7 +1066,7 @@
val thm =
Goal.prove_sorry lthy vars (flat premss) goal (fn {context = ctxt, prems} =>
mk_set_cases_tac ctxt (Thm.cterm_of ctxt ta) prems exhaust set_thms)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> rotate_prems ~1;
val cases_set_attr =
@@ -1117,7 +1117,7 @@
in
Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => mk_set_intros_tac ctxt set0_thms)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> Conjunction.elim_balanced (length goals)
end)
end;
@@ -1150,7 +1150,7 @@
mk_rel_sel_tac ctxt (Thm.cterm_of ctxt ta) (Thm.cterm_of ctxt tb) exhaust
(flat disc_thmss) (flat sel_thmss) rel_inject_thms distincts rel_distinct_thms
live_nesting_rel_eqs))
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
in
map prove goals
end;
@@ -1183,7 +1183,7 @@
Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} =>
mk_sel_transfer_tac ctxt n sel_defs case_transfer_thm)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> Conjunction.elim_balanced (length goals)
end
end;
@@ -1201,7 +1201,7 @@
(fn {context = ctxt, prems = _} => mk_disc_transfer_tac ctxt
(the_single rel_sel_thms) (the_single exhaust_discs)
(flat (flat distinct_discsss)))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> Conjunction.elim_balanced (length goals)
end
end;
@@ -1230,7 +1230,7 @@
(fn {context = ctxt, prems = _} =>
mk_map_disc_iff_tac ctxt (Thm.cterm_of ctxt ta) exhaust (flat disc_thmss)
map_thms)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> Conjunction.elim_balanced (length goals)
end
end;
@@ -1270,7 +1270,7 @@
(fn {context = ctxt, prems = _} =>
mk_map_sel_tac ctxt (Thm.cterm_of ctxt ta) exhaust (flat disc_thmss)
map_thms (flat sel_thmss) live_nesting_map_id0s)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> Conjunction.elim_balanced (length goals)
end)
end;
@@ -1334,7 +1334,7 @@
(fn {context = ctxt, prems = _} =>
mk_set_sel_tac ctxt (Thm.cterm_of ctxt ta) exhaust (flat disc_thmss)
(flat sel_thmss) set0_thms)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> Conjunction.elim_balanced (length goals)
end)
end;
@@ -1744,7 +1744,7 @@
Goal.prove_sorry ctxt vars prems goal (fn {context = ctxt, prems} =>
mk_rel_induct0_tac ctxt ctor_rel_induct prems (map (Thm.cterm_of ctxt) IRs) exhausts
ctor_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs)
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
in
(postproc_co_induct ctxt nn @{thm predicate2D} @{thm predicate2D_conj} rel_induct0_thm,
mk_induct_attrs ctrAss)
@@ -1796,7 +1796,7 @@
Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, ...} =>
mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' pre_abs_inverses
abs_inverses fp_nesting_set_maps pre_set_defss)
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
in
`(conj_dests nn) thm
end;
@@ -1838,7 +1838,7 @@
fun prove goal tac =
Goal.prove_sorry ctxt [] [] goal (tac o #context)
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
in
map2 (map2 prove) goalss tacss
end;
@@ -1947,7 +1947,7 @@
(map #exhaust ctr_sugars) (map (flat o #disc_thmss) ctr_sugars)
(map (flat o #sel_thmss) ctr_sugars) ctor_defss dtor_ctors ctor_injects abs_injects
rel_pre_defs abs_inverses live_nesting_rel_eqs)
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
in
(postproc_co_induct ctxt nn @{thm predicate2D} @{thm predicate2D_conj} rel_coinduct0_thm,
mk_coinduct_attrs fpA_Ts (map #ctrs ctr_sugars) (map #discs ctr_sugars) mss)
@@ -2028,7 +2028,7 @@
(fn {context = ctxt, prems} =>
mk_set_induct0_tac ctxt (map (Thm.cterm_of ctxt'') Ps) prems dtor_set_inducts
exhausts set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses)
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
val case_names_attr = Attrib.case_names (quasi_unambiguous_case_names case_names);
val induct_set_attrs = map (Attrib.internal o K o Induct.induct_pred o name_of_set) sets;
@@ -2115,7 +2115,7 @@
|> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, ...} =>
mk_coinduct_tac ctxt live_nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs pre_abs_inverses
abs_inverses dtor_ctors exhausts ctr_defss disc_thmsss sel_thmsss))
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
val rel_eqs = map rel_eq_of_bnf pre_bnfs;
val rel_monos = map rel_mono_of_bnf pre_bnfs;
@@ -2202,7 +2202,7 @@
fun prove goal tac =
Goal.prove_sorry ctxt [] [] goal (tac o #context)
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
in
map2 (map2 prove) goalss tacss
|> map (map (unfold_thms ctxt @{thms case_sum_if}))
@@ -2226,7 +2226,7 @@
fun prove goal tac =
Variable.add_free_names ctxt goal []
|> (fn vars => Goal.prove_sorry ctxt vars [] goal (tac o #context))
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
fun proves [_] [_] = []
| proves goals tacs = map2 prove goals tacs;
@@ -2565,7 +2565,7 @@
mk_rec_transfer_tac ctxt nn ns (map (Thm.cterm_of ctxt) Ss)
(map (Thm.cterm_of ctxt) Rs) xsssss rec_defs xtor_co_rec_transfers pre_rel_defs
live_nesting_rel_eqs)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> Conjunction.elim_balanced nn
end;
@@ -2626,7 +2626,7 @@
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
mk_co_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s
abs_inverses ctor_rec_o_map)
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
rec_o_map_goals rec_defs xtor_co_rec_o_maps;
in
map single rec_o_map_thms
@@ -2717,7 +2717,7 @@
mk_corec_transfer_tac ctxt (map (Thm.cterm_of ctxt) Ss) (map (Thm.cterm_of ctxt) Rs)
type_definitions corec_defs xtor_co_rec_transfers pre_rel_defs
live_nesting_rel_eqs (flat pgss) pss qssss gssss)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> Conjunction.elim_balanced (length goals)
end;
@@ -2773,7 +2773,7 @@
Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} =>
mk_co_rec_o_map_tac ctxt corec_def pre_map_defs live_nesting_map_ident0s
abs_inverses dtor_map_o_corec)
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
map_o_corec_goals corec_defs xtor_co_rec_o_maps;
in
map single map_o_corec_thms
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Fri Aug 09 17:14:49 2019 +0200
@@ -36,7 +36,7 @@
in
Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
HEADGOAL (hyp_subst_tac ctxt THEN' rtac ctxt refl))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val cacheN = "cache"
@@ -473,7 +473,7 @@
|> HOLogic.mk_Trueprop
|> (fn goal => Goal.prove_sorry raw_lthy [] [] goal
(fn {context = ctxt, prems = _} => mk_xtor_un_fold_tac ctxt n simps cache_defs))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> Morphism.thm phi
|> split_conj_thm
|> map (fn thm => thm RS @{thm comp_eq_dest})
@@ -512,7 +512,7 @@
Goal.prove_sorry raw_lthy vars prems concl
(mk_xtor_un_fold_unique_tac fp un_fold_defs map_arg_congs xtor_un_fold_o_maps
Rep_o_Abss fp_un_fold_uniques simp_thms map_thms map_defs cache_defs)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> case_fp fp I (fn thm => thm OF replicate n sym)
|> Morphism.thm phi
end;
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML Fri Aug 09 17:14:49 2019 +0200
@@ -133,7 +133,7 @@
in
Goal.prove lthy vars [] goal (fn {context = ctxt, prems = _} =>
mk_lfp_rec_sugar_transfer_tac ctxt def)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end);
val gfp_rec_sugar_transfer_interpretation = fp_rec_sugar_transfer_interpretation
@@ -162,7 +162,7 @@
(maps (#xtor_co_rec_transfers o #fp_res) fp_sugars)
(map (rel_def_of_bnf o #pre_bnf) fp_sugars)
disc_eq_cases case_thms case_distribs case_congs)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end);
val _ = Theory.setup (lfp_rec_sugar_interpretation transfer_plugin
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Aug 09 17:14:49 2019 +0200
@@ -567,7 +567,7 @@
(map2 (flip mk_leq) relphis pre_phis));
in
Goal.prove_sorry lthy (map (fst o dest_Free) (phis @ pre_phis)) prems concl tac
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> (fn thm => thm OF (replicate (length pre_rels) @{thm allI[OF allI[OF impI]]}))
end;
@@ -586,7 +586,7 @@
(HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj transfers));
in
Goal.prove_sorry lthy [] [] goal tac
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> split_conj_thm
end;
@@ -796,7 +796,7 @@
Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => mk_xtor_co_rec_id_tac ctxt xtor_un_fold_xtor_thms
xtor_un_fold_unique xtor_un_folds map_comps)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> split_conj_thm
end;
@@ -825,7 +825,7 @@
|> (fn vars => Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} =>
mk_xtor_co_rec_tac ctxt un_fold co_rec_defs co_rec_expand_thms))
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
goals xtor_un_folds
end;
@@ -856,7 +856,7 @@
Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => mk_xtor_co_rec_unique_tac ctxt fp co_rec_defs
co_rec_expand'_thms xtor_un_fold_unique map_id0s sym_map_comp0s inverses)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val xtor_co_rec_o_map_thms = if forall is_none absT_info_opts
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Fri Aug 09 17:14:49 2019 +0200
@@ -213,7 +213,7 @@
in
Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => mk_map_comp_id_tac ctxt map_comp0)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val map_comp_id_thms = @{map 5} mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps;
@@ -231,7 +231,7 @@
in
Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, goal))
(fn {context = ctxt, prems = _} => mk_map_cong0L_tac ctxt m map_cong0 map_id)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val map_cong0L_thms = @{map 5} mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
@@ -251,7 +251,7 @@
Variable.add_free_names lthy goal []
|> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
(hyp_subst_tac ctxt THEN' rtac ctxt refl) 1))
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
goals
end;
@@ -321,7 +321,7 @@
Variable.add_free_names lthy goal []
|> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
mk_coalg_set_tac ctxt coalg_def))
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
goals) goalss
end;
@@ -336,7 +336,7 @@
(fn {context = ctxt, prems = _} => (rtac ctxt (coalg_def RS iffD2) 1 THEN CONJ_WRAP
(K (EVERY' [rtac ctxt ballI, rtac ctxt CollectI,
CONJ_WRAP' (K (EVERY' [rtac ctxt @{thm subset_UNIV}])) allAs] 1)) ss))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val timer = time (timer "Coalgebra definition & thms");
@@ -416,7 +416,7 @@
Variable.add_free_names lthy goal []
|> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
mk_mor_elim_tac ctxt mor_def))
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
in
(map prove image_goals, map prove elim_goals)
end;
@@ -431,7 +431,7 @@
in
Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
(fn {context = ctxt, prems = _} => mk_mor_incl_tac ctxt mor_def map_ids)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val mor_id_thm = mor_incl_thm OF (replicate n subset_refl);
@@ -448,7 +448,7 @@
Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
(fn {context = ctxt, prems = _} =>
mk_mor_comp_tac ctxt mor_def mor_image'_thms morE_thms map_comp_id_thms)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val mor_cong_thm =
@@ -460,7 +460,7 @@
in
Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
(fn {context = ctxt, prems = _} => (hyp_subst_tac ctxt THEN' assume_tac ctxt) 1)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val mor_UNIV_thm =
@@ -474,7 +474,7 @@
in
Goal.prove_sorry lthy vars [] (mk_Trueprop_eq (lhs, rhs))
(fn {context = ctxt, prems = _} => mk_mor_UNIV_tac ctxt morE_thms mor_def)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val mor_str_thm =
@@ -486,7 +486,7 @@
in
Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => mk_mor_str_tac ctxt ks mor_UNIV_thm)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val timer = time (timer "Morphism definition & thms");
@@ -567,7 +567,7 @@
in
Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
(fn {context = ctxt, prems = _} => (hyp_subst_tac ctxt THEN' assume_tac ctxt) 1)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val bis_rel_thm =
@@ -586,7 +586,7 @@
Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => mk_bis_rel_tac ctxt m bis_def in_rels map_comps
map_cong0s set_mapss)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val bis_converse_thm =
@@ -598,7 +598,7 @@
Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => mk_bis_converse_tac ctxt m bis_rel_thm rel_congs
rel_converseps)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val bis_O_thm =
@@ -612,7 +612,7 @@
in
Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
(fn {context = ctxt, prems = _} => mk_bis_O_tac ctxt m bis_rel_thm rel_congs le_rel_OOs)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val bis_Gr_thm =
@@ -623,7 +623,7 @@
Goal.prove_sorry lthy vars [] (Logic.list_implies ([coalg_prem, mor_prem], concl))
(fn {context = ctxt, prems = _} => mk_bis_Gr_tac ctxt bis_rel_thm rel_Grps mor_image_thms
morE_thms coalg_in_thms)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val bis_image2_thm = bis_cong_thm OF
@@ -644,7 +644,7 @@
in
Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, concl))
(fn {context = ctxt, prems = _} => mk_bis_Union_tac ctxt bis_def in_mono'_thms)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
(* self-bisimulation *)
@@ -706,7 +706,7 @@
Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} =>
mk_sbis_lsbis_tac ctxt lsbis_defs bis_Union_thm bis_cong_thm)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val lsbis_incl_thms = map (fn i => sbis_lsbis_thm RS
@@ -723,7 +723,7 @@
Variable.add_free_names lthy goal []
|> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
mk_incl_lsbis_tac ctxt n i def))
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
goals ks lsbis_defs
end;
@@ -737,7 +737,7 @@
|> (fn vars => Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => mk_equiv_lsbis_tac ctxt sbis_lsbis_thm l_incl incl_l
bis_Id_on_thm bis_converse_thm bis_O_thm)
- |> Thm.close_derivation))
+ |> Thm.close_derivation \<^here>))
goals lsbis_incl_thms incl_lsbis_thms
end;
@@ -968,7 +968,7 @@
Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (mk_coalg carTAs strTAs))
(fn {context = ctxt, prems = _} => mk_coalgT_tac ctxt m
(coalg_def :: isNode_defs @ carT_defs) strT_defs set_mapss)
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
val timer = time (timer "Tree coalgebra");
@@ -1144,7 +1144,7 @@
val length_Lev =
Goal.prove_sorry lthy vars [] (HOLogic.mk_Trueprop goal)
(fn {context = ctxt, prems = _} => mk_length_Lev_tac ctxt cts Lev_0s Lev_Sucs)
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
val length_Lev' = mk_specN (n + 1) length_Lev;
val length_Levs = map (fn i => length_Lev' RS mk_conjunctN n i RS mp) ks;
@@ -1159,7 +1159,7 @@
Variable.add_free_names lthy goal []
|> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
mk_length_Lev'_tac ctxt length_Lev))
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
goals length_Levs;
in
(length_Levs, length_Levs')
@@ -1183,7 +1183,7 @@
val rv_last =
Goal.prove_sorry lthy vars [] (HOLogic.mk_Trueprop goal)
(fn {context = ctxt, prems = _} => mk_rv_last_tac ctxt cTs cts rv_Nils rv_Conss)
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
val rv_last' = mk_specN (n + 1) rv_last;
in
@@ -1221,7 +1221,7 @@
Goal.prove_sorry lthy vars [] (HOLogic.mk_Trueprop goal)
(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;
+ |> Thm.close_derivation \<^here>;
val set_Lev' = mk_specN (3 * n + 1) set_Lev;
in
@@ -1262,7 +1262,7 @@
(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;
+ |> Thm.close_derivation \<^here>;
val set_image_Lev' = mk_specN (2 * n + 2) set_image_Lev;
in
@@ -1283,7 +1283,7 @@
to_sbd_inj_thmss from_to_sbd_thmss Lev_0s Lev_Sucs rv_Nils rv_Conss
length_Lev_thms length_Lev'_thms rv_last_thmss set_Lev_thmsss
set_image_Lev_thmsss set_mapss map_comp_id_thms map_cong0s)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val timer = time (timer "Behavioral morphism");
@@ -1312,7 +1312,7 @@
Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} => mk_congruent_str_final_tac ctxt m lsbisE map_comp_id
map_cong0 equiv_LSBIS_thms)
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
goals lsbisE_thms map_comp_id_thms map_cong0s
end;
@@ -1320,13 +1320,13 @@
(HOLogic.mk_Trueprop (mk_coalg car_finals str_finals))
(fn {context = ctxt, prems = _} => mk_coalg_final_tac ctxt m coalg_def
congruent_str_final_thms equiv_LSBIS_thms set_mapss coalgT_set_thmss)
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
val mor_T_final_thm = Goal.prove_sorry lthy [] []
(HOLogic.mk_Trueprop (mk_mor carTAs strTAs car_finals str_finals (map mk_proj lsbisAs)))
(fn {context = ctxt, prems = _} => mk_mor_T_final_tac ctxt mor_def congruent_str_final_thms
equiv_LSBIS_thms)
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
val mor_final_thm = mor_comp_thm OF [mor_beh_thm, mor_T_final_thm];
val in_car_final_thms = map (fn thm => thm OF [mor_final_thm, UNIV_I]) mor_image'_thms;
@@ -1404,14 +1404,14 @@
(HOLogic.mk_Trueprop (mk_mor UNIVs dtors car_finals str_finals Rep_Ts))
(fn {context = ctxt, prems = _} => mk_mor_Rep_tac ctxt (mor_def :: dtor_defs) Reps
Abs_inverses coalg_final_set_thmss map_comp_id_thms map_cong0L_thms)
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
val mor_Abs =
Goal.prove_sorry lthy [] []
(HOLogic.mk_Trueprop (mk_mor car_finals str_finals UNIVs dtors Abs_Ts))
(fn {context = ctxt, prems = _} => mk_mor_Abs_tac ctxt (mor_def :: dtor_defs)
Abs_inverses)
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
in
(mor_Rep, mor_Abs)
end;
@@ -1462,7 +1462,7 @@
Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => mk_mor_unfold_tac ctxt m mor_UNIV_thm dtor_defs
unfold_defs Abs_inverses' morEs' map_comp_id_thms map_cong0s)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val dtor_unfold_thms = map (fn thm => (thm OF [mor_unfold_thm, UNIV_I]) RS sym) morE_thms;
@@ -1477,7 +1477,7 @@
(fn {context = ctxt, prems = _} => mk_raw_coind_tac ctxt bis_def bis_cong_thm bis_O_thm
bis_converse_thm bis_Gr_thm tcoalg_thm coalgT_thm mor_T_final_thm sbis_lsbis_thm
lsbis_incl_thms incl_lsbis_thms equiv_LSBIS_thms mor_Rep_thm Rep_injects)
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
end;
val (unfold_unique_mor_thms, unfold_unique_mor_thm) =
@@ -1494,7 +1494,7 @@
val unique_mor = Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, unique))
(fn {context = ctxt, prems = _} => mk_unfold_unique_mor_tac ctxt raw_coind_thms
bis_thm mor_thm unfold_defs)
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
in
`split_conj_thm unique_mor
end;
@@ -1550,7 +1550,7 @@
Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} => mk_dtor_o_ctor_tac ctxt ctor_def unfold map_comp_id
map_cong0L unfold_o_dtor_thms)
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
goals ctor_defs dtor_unfold_thms map_comp_id_thms map_cong0L_thms
end;
@@ -1608,7 +1608,7 @@
|> (fn vars => Goal.prove_sorry lthy vars [] dtor_coinduct_goal
(fn {context = ctxt, prems = _} => mk_dtor_coinduct_tac ctxt m raw_coind_thm bis_rel_thm
rel_congs))
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
in
(rev (Term.add_tfrees dtor_coinduct_goal []), dtor_coinduct)
end;
@@ -1834,7 +1834,7 @@
|> (fn vars => Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN
mk_map_tac ctxt m n map_arg_cong unfold map_comp map_cong0))
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
goals dtor_unfold_thms map_comps map_cong0s map_arg_cong_thms;
in
map_split (fn thm => (thm RS @{thm comp_eq_dest}, thm)) maps
@@ -1854,7 +1854,7 @@
`split_conj_thm (Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, goal))
(fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN
mk_dtor_map_unique_tac ctxt dtor_unfold_unique_thm sym_map_comps)
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
end;
val Jmap_comp0_thms =
@@ -1868,7 +1868,7 @@
split_conj_thm (Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} =>
mk_map_comp0_tac ctxt Jmap_thms map_comp0s dtor_Jmap_unique_thm)
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
end;
val timer = time (timer "map functions for the new codatatypes");
@@ -1907,7 +1907,7 @@
|> (fn vars => Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => mk_col_minimal_tac ctxt m cts col_0s
col_Sucs))
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
goals ctss col_0ss' col_Sucss'
end;
@@ -1923,7 +1923,7 @@
|> (fn vars => Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
mk_Jset_minimal_tac ctxt n col_minimal))
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
goals col_minimal_thms
end;
@@ -1955,7 +1955,7 @@
|> (fn vars => Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
mk_set_incl_Jset_tac ctxt rec_Suc))
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
goals rec_Sucs)
set_incl_Jset_goalss col_Sucss,
map2 (fn goalss => fn rec_Sucs =>
@@ -1965,7 +1965,7 @@
|> (fn vars => Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
mk_set_Jset_incl_Jset_tac ctxt n rec_Suc k))
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
goals rec_Sucs)
ks goalss)
set_Jset_incl_Jset_goalsss col_Sucss)
@@ -2024,7 +2024,7 @@
|> (fn vars => Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} =>
mk_set_le_tac ctxt n Jset_minimal set_Jsets set_Jset_Jsetss))
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
le_goals Jset_minimal_thms set_Jset_thmss' set_Jset_Jset_thmsss');
val ge_goalss = map (map HOLogic.mk_Trueprop) (mk_goals (uncurry mk_leq o swap));
@@ -2034,7 +2034,7 @@
|> (fn vars => Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} =>
mk_set_ge_tac ctxt n set_incl_Jset set_Jset_incl_Jsets))
- |> Thm.close_derivation))
+ |> Thm.close_derivation \<^here>))
ge_goalss set_incl_Jset_thmss' set_Jset_incl_Jset_thmsss'
in
map2 (map2 (fn le => fn ge => equalityI OF [le, ge])) set_le_thmss set_ge_thmss
@@ -2067,7 +2067,7 @@
|> (fn vars => Goal.prove_sorry lthy vars [] (HOLogic.mk_Trueprop goal)
(fn {context = ctxt, prems = _} => mk_col_natural_tac ctxt cts rec_0s rec_Sucs
dtor_Jmap_thms set_mapss))
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
goals ctss col_0ss' col_Sucss';
in
map (split_conj_thm o mk_specN n) thms
@@ -2091,7 +2091,7 @@
|> (fn vars => Goal.prove_sorry lthy vars [] (HOLogic.mk_Trueprop goal)
(fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jbd_defs THEN
mk_col_bd_tac ctxt m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss))
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
ls goals ctss col_0ss' col_Sucss';
in
map (split_conj_thm o mk_specN n) thms
@@ -2138,7 +2138,7 @@
(fn {context = ctxt, prems = _} => mk_mcong_tac ctxt m (rtac ctxt coinduct) map_comps
dtor_Jmap_thms map_cong0s
set_mapss set_Jset_thmss set_Jset_Jset_thmsss in_rels)
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
in
split_conj_thm thm
end;
@@ -2169,7 +2169,7 @@
(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)
+ |> Thm.close_derivation \<^here>)
ks goals in_rels map_comps map_cong0s dtor_Jmap_thms dtor_Jset_thmss'
dtor_inject_thms dtor_ctor_thms set_mapss dtor_Jset_incl_thmss
dtor_set_Jset_incl_thmsss
@@ -2252,7 +2252,7 @@
mk_rel_coinduct_coind_tac ctxt fst m
(infer_instantiate' ctxt cts dtor_coinduct_thm) ks map_comps map_cong0s
map_arg_cong_thms set_mapss dtor_unfold_thms dtor_Jmap_thms in_rels)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> split_conj_thm
end;
@@ -2291,7 +2291,7 @@
(fn {context = ctxt, prems = _} =>
mk_rel_coinduct_ind_tac ctxt m ks
dtor_unfold_thms set_mapss j (infer_instantiate' ctxt cts set_induct)))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> split_conj_thm)
mk_helper_ind_concls ls dtor_Jset_induct_thms ctss
|> transpose;
@@ -2315,7 +2315,7 @@
in
Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
mk_le_rel_OO_tac ctxt Jrel_coinduct_thm dtor_Jrel_thms le_rel_OOs)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val timer = time (timer "helpers for BNF properties");
@@ -2435,7 +2435,7 @@
|> (fn vars => Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => mk_coind_wit_tac ctxt induct dtor_unfold_thms
(flat set_mapss) wit_thms))
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
goals dtor_Jset_induct_thms
|> map split_conj_thm
|> transpose
--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Fri Aug 09 17:14:49 2019 +0200
@@ -881,7 +881,7 @@
Variable.add_free_names ctxt goal []
|> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_sig_transfer_tac ctxt pre_rel_def preT_rel_eqs transfer_thm))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_transfer_by_transfer_prover ctxt live_AsBs Rs R const const_defs rel_eqs transfers =
@@ -893,7 +893,7 @@
|> (fn vars => Goal.prove (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_transfer_by_transfer_prover_tac ctxt (const_defs @ map (fn thm => thm RS sym) rel_eqs)
rel_eqs transfers))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_dtor_transfer ctxt live_EsFs Y Z pre_rel fp_rel Rs dtor dtor_rel_thm =
@@ -911,7 +911,7 @@
Variable.add_free_names ctxt goal []
|> (fn vars => Goal.prove (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_dtor_transfer_tac ctxt dtor_rel_thm))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_Lam_or_eval_core_transfer ctxt live_AsBs Y Z preT ssig_T Rs R pre_rel sig_or_ssig_rel
@@ -936,7 +936,7 @@
Variable.add_free_names ctxt goal []
|> (fn vars => Goal.prove (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_transfer_by_transfer_prover_tac ctxt [const_def] rel_eqs transfers))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_proto_sctr_transfer_step_or_merge ctxt Y Z R dead_pre_rel dead_sig_rel proto_sctr
@@ -949,7 +949,7 @@
Variable.add_free_names ctxt goal []
|> (fn vars => Goal.prove (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_transfer_by_transfer_prover_tac ctxt [proto_sctr_def] fp_k_T_rel_eqs transfers))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_sctr_transfer ctxt live_AsBs Y Z ssig_T Rs R pre_rel ssig_rel sctr sctr_def
@@ -967,7 +967,7 @@
Variable.add_free_names ctxt goal []
|> (fn vars => Goal.prove (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_transfer_by_transfer_prover_tac ctxt [sctr_def] fp_k_T_rel_eqs transfers))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_corecUU_transfer ctxt live_AsBs Y Z Rs R preT ssig_T pre_rel fp_rel ssig_rel corecUU
@@ -993,7 +993,7 @@
|> (fn vars => Goal.prove (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_transfer_by_transfer_prover_tac ctxt [cutSsig_def, corecU_def, corecUU_def] fp_k_T_rel_eqs
transfers))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun mk_natural_goal ctxt simple_T_mapfs fs t u =
@@ -1021,7 +1021,7 @@
Variable.add_free_names ctxt goal []
|> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_natural_by_unfolding_tac ctxt map_thms))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_natural_from_transfer ctxt live_AsBs simple_T_mapfs fs f const transfer bnfs subst_bnfs =
@@ -1035,7 +1035,7 @@
|> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_natural_from_transfer_tac ctxt m (replicate m true) transfer [] (map rel_Grp_of_bnf bnfs)
(map rel_Grp_of_bnf subst_bnfs)))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_natural_from_transfer_with_pre_type ctxt live_AsBs Y Z preT ssig_T pre_map ssig_map fs
@@ -1077,7 +1077,7 @@
|> (fn vars => Goal.prove_sorry ctxt vars [] goal
(fn {context = ctxt, prems = _} => mk_Lam_Inl_Inr_tac ctxt unsig_thm Lam_def))
|> Conjunction.elim_balanced (length goals)
- |> map Thm.close_derivation
+ |> map (Thm.close_derivation \<^here>)
end;
fun derive_flat_VLeaf ctxt Y Z ssig_T x VLeaf dead_ssig_map flat ssig_induct fp_map_id sig_map_cong
@@ -1095,7 +1095,7 @@
mk_flat_VLeaf_or_flat_tac ctxt ssig_induct' sig_map_cong
(fp_map_id :: sig_map_ident :: sig_map_comp :: ssig_map_thms @ flat_simps @
@{thms o_apply id_apply id_def[symmetric]})))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_flat_flat ctxt Y Z ssig_T x dead_ssig_map flat ssig_induct fp_map_id sig_map_cong
@@ -1116,7 +1116,7 @@
|> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_flat_VLeaf_or_flat_tac ctxt ssig_induct' sig_map_cong
(o_apply :: fp_map_id :: sig_map_comp :: ssig_map_thms @ flat_simps)))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_eval_core_flat ctxt Y Z preT ssig_T dead_pre_map dead_ssig_map flat eval_core x
@@ -1148,7 +1148,7 @@
mk_eval_core_flat_tac ctxt ssig_induct' dead_pre_map_id dead_pre_map_comp0 dead_pre_map_comp
fp_map_id sig_map_comp sig_map_cong ssig_map_thms ssig_map_comp flat_simps
flat_pointful_natural flat_flat Lam_pointful_natural eval_core_simps))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_eval_thm ctxt dtor_inject dtor_unfold_thm eval_def =
@@ -1177,7 +1177,7 @@
|> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_eval_flat_tac ctxt dead_pre_map_comp0 ssig_map_id ssig_map_comp flat_pointful_natural
eval_core_pointful_natural eval_core_flat eval_thm cond_eval_o_flat))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_eval_Oper ctxt live Y Z fpT sig_T ssig_T dead_sig_map Oper eval algLam x sig_map_ident
@@ -1196,7 +1196,7 @@
|> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_eval_Oper_tac ctxt live sig_map_ident sig_map_comp0 sig_map_comp Oper_natural_pointful
VLeaf_natural flat_simps eval_flat algLam_def))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_eval_V_or_CLeaf ctxt Y fpT V_or_CLeaf eval x dead_pre_map_id dead_pre_map_comp fp_map_id
@@ -1211,7 +1211,7 @@
|> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_eval_V_or_CLeaf_tac ctxt dead_pre_map_id dead_pre_map_comp fp_map_id dtor_unfold_unique
V_or_CLeaf_map_thm eval_core_simps eval_thm))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_extdd_mor ctxt Y Z preT fpT ssig_T dead_pre_map dtor extdd cutSsig f g dead_pre_map_comp0
@@ -1235,7 +1235,7 @@
mk_extdd_mor_tac ctxt dead_pre_map_comp0 dead_pre_map_comp VLeaf_map_thm ssig_map_comp
flat_pointful_natural eval_core_pointful_natural eval_thm eval_flat eval_VLeaf cutSsig_def
prem))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_mor_cutSsig_flat ctxt Y Z preT fpT ssig_T dead_pre_map dead_ssig_map dtor flat eval_core
@@ -1271,7 +1271,7 @@
dead_pre_map_cong dtor_unfold_unique dead_ssig_map_comp0 ssig_map_comp flat_simps
flat_pointful_natural eval_core_pointful_natural flat_flat flat_VLeaf eval_core_flat
cutSsig_def cutSsig_def_pointful_natural eval_thm prem))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_extdd_o_VLeaf ctxt Y Z preT fpT ssig_T dead_pre_map dtor VLeaf extdd f g
@@ -1295,7 +1295,7 @@
|> (fn vars => Goal.prove_sorry ctxt vars [prem] goal (fn {context = ctxt, prems = [prem]} =>
mk_extdd_o_VLeaf_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_inject ssig_map_thms
eval_core_simps eval_thm eval_VLeaf prem))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_corecU_pointfree ctxt Y Z preT fpT ssig_T dead_pre_map dtor extdd corecU g
@@ -1318,7 +1318,7 @@
mk_corecU_pointfree_tac ctxt dead_pre_map_comp dtor_unfold_thm ssig_map_thms
dead_ssig_map_comp0 flat_simps flat_VLeaf eval_core_simps cutSsig_def mor_cutSsig_flat
corecU_def))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_corecU_ctor_unique ctxt Y Z preT fpT ssig_T dead_pre_map ctor dtor VLeaf extdd corecU f g
@@ -1386,7 +1386,7 @@
mk_dtor_algLam_tac ctxt pre_map_comp dead_pre_map_id dead_pre_map_comp0 dead_pre_map_comp
sig_map_comp Oper_pointful_natural ssig_map_thms dead_ssig_map_comp0 Lam_pointful_natural
eval_core_simps eval_thm eval_flat eval_VLeaf algLam_def))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_algLam_base ctxt Y Z preT fpT dead_pre_map ctor dtor algLam proto_sctr dead_pre_map_id
@@ -1407,7 +1407,7 @@
mk_algLam_base_tac ctxt dead_pre_map_dtor dead_pre_map_id dead_pre_map_comp ctor_dtor
dtor_ctor dtor_unfold_unique unsig_thm Sig_pointful_natural ssig_map_thms Lam_def flat_simps
eval_core_simps eval_thm algLam_def))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_flat_embL ctxt Y Z old_ssig_T ssig_T dead_old_ssig_map embL old_flat flat x
@@ -1431,7 +1431,7 @@
|> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_flat_embL_tac ctxt old_ssig_induct' fp_map_id Sig_pointful_natural old_sig_map_comp
old_sig_map_cong old_ssig_map_thms old_flat_simps flat_simps embL_simps))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_eval_core_embL ctxt Y Z preT old_ssig_T ssig_T dead_pre_map embL old_eval_core eval_core
@@ -1457,7 +1457,7 @@
mk_eval_core_embL_tac ctxt old_ssig_induct' dead_pre_map_comp0 dead_pre_map_comp
Sig_pointful_natural unsig_thm old_sig_map_comp old_sig_map_cong old_Lam_pointful_natural
Lam_def flat_embL old_eval_core_simps eval_core_simps embL_simps embL_pointful_natural))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_eval_embL ctxt Y fpT embL old_eval eval dead_pre_map_comp0 dtor_unfold_unique
@@ -1470,7 +1470,7 @@
|> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_eval_embL_tac ctxt dead_pre_map_comp0 dtor_unfold_unique embL_pointful_natural
eval_core_embL old_eval_thm eval_thm))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_algLam_algLam ctxt Inx_const Y fpT Sig old_algLam algLam dead_pre_map_comp dtor_inject
@@ -1486,7 +1486,7 @@
|> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_algLam_algLam_tac ctxt dead_pre_map_comp dtor_inject unsig_thm sig_map_thm Lam_def
eval_embL old_dtor_algLam dtor_algLam))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_eval_core_k_as_ssig ctxt Y preT k_T rho eval_core k_as_ssig x pre_map_comp
@@ -1505,7 +1505,7 @@
|> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_eval_core_k_as_ssig_tac ctxt pre_map_comp dead_pre_map_id sig_map_comp ssig_map_thms
Lam_natural_pointful Lam_Inr flat_VLeaf eval_core_simps))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_algLam_algrho ctxt Y fpT Sig algLam algrho algLam_def algrho_def =
@@ -1519,7 +1519,7 @@
Variable.add_free_names ctxt goal []
|> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_algLam_algrho_tac ctxt algLam_def algrho_def))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_dtor_algrho ctxt Y Z preT fpT k_T ssig_T dead_pre_map dead_k_map dtor rho eval algrho x
@@ -1543,7 +1543,7 @@
Variable.add_free_names ctxt goal []
|> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_dtor_algrho_tac ctxt eval_thm k_as_ssig_natural_pointful eval_core_k_as_ssig algrho_def))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_algLam_step_or_merge ctxt Y fpT ctor proto_sctr algLam proto_sctr_def old_algLam_pointful
@@ -1557,7 +1557,7 @@
Variable.add_free_names ctxt goal []
|> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_algLam_step_tac ctxt proto_sctr_def old_algLam_pointful algLam_algLam_pointful))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_eval_sctr ctxt Y Z fpT ssig_T dead_pre_map ctor eval sctr proto_sctr_pointful_natural
@@ -1574,7 +1574,7 @@
Variable.add_free_names ctxt goal []
|> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_eval_sctr_tac ctxt proto_sctr_pointful_natural eval_Oper algLam_thm sctr_def))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_corecUU_pointfree_unique ctxt Y Z preT fpT ssig_T dead_pre_map ctor dead_ssig_map eval
@@ -1609,7 +1609,7 @@
mk_corecUU_pointfree_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor dtor_inject
ssig_map_comp flat_pointful_natural eval_core_pointful_natural eval_thm eval_flat
corecU_ctor sctr_pointful_natural eval_sctr_pointful corecUU_def))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val corecUU_unique =
@@ -1623,7 +1623,7 @@
mk_corecUU_unique_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor
ssig_map_comp flat_pointful_natural eval_core_pointful_natural eval_thm eval_flat
corecU_unique sctr_pointful_natural eval_sctr_pointful corecUU_def prem))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
in
(corecUU_pointfree, corecUU_unique)
@@ -1858,7 +1858,7 @@
|> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_equivp_Retr_tac ctxt dead_pre_rel_refl_thm dead_pre_rel_flip_thm dead_pre_rel_mono_thm
dead_pre_rel_compp_thm))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_Retr_coinduct ctxt fpT Retr R dtor_rel_coinduct_thm rel_eq_thm =
@@ -1868,7 +1868,7 @@
in
Goal.prove_sorry ctxt [] [] goal (fn {context = ctxt, prems = _} =>
mk_Retr_coinduct_tac ctxt dtor_rel_coinduct_thm rel_eq_thm)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_Retr fp_sugar fpT dead_pre_bnf ctor dtor names_lthy lthy =
@@ -1904,7 +1904,7 @@
in
Variable.add_free_names ctxt goal []
|> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} => tac ctxt))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_cong_general fp_b version fpT dead_ssig_bnf dead_pre_bnf eval Retr equivp_Retr
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Fri Aug 09 17:14:49 2019 +0200
@@ -247,7 +247,7 @@
in
Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_case_dtor_tac ctxt u abs_inverse dtor_ctor ctr_defs exhaust case_thms)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_case_trivial ctxt fpT_name =
@@ -269,7 +269,7 @@
Goal.prove_sorry ctxt [var_name] [] goal (fn {context = ctxt, prems = _} =>
HEADGOAL (rtac ctxt exhaust') THEN ALLGOALS (hyp_subst_tac ctxt) THEN
unfold_thms_tac ctxt case_thms THEN ALLGOALS (rtac ctxt refl))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun mk_abs_rep_transfers ctxt fpT_name =
@@ -351,7 +351,7 @@
live_nesting_map_ident0s fp_map_ident case_trivial ctr_defs case_eq_ifs corecUU_thm
all_sig_map_thms ssig_map_thms all_algLam_alg_pointfuls (all_algrho_eqs_of ctxt) eval_simps
inner_fp_simps fun_def))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_unique ctxt phi code_goal
@@ -410,7 +410,7 @@
live_nesting_map_ident0s fp_map_ident case_trivial ctr_defs case_eq_ifs all_sig_map_thms
ssig_map_thms all_algLam_alg_pointfuls (all_algrho_eqs_of ctxt) eval_simps corecUU_unique
eq_corecUU)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_last_disc ctxt fcT_name =
@@ -428,7 +428,7 @@
in
Goal.prove_sorry ctxt [fst (dest_Free u)] [] goal (fn {context = ctxt, prems = _} =>
mk_last_disc_tac ctxt u exhaust (flat disc_thmss))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_eq_algrho ctxt {sig_fp_sugars, ssig_fp_sugar, eval, eval_simps, all_algLam_algs,
@@ -522,7 +522,7 @@
disc_sel_eq_cases case_dtor case_eq_ifs const_pointful_naturals
fp_nesting_k_map_disc_sels' rho_def dtor_algrho corecUU_unique eq_corecUU all_sig_map_thms
ssig_map_thms all_algLam_alg_pointfuls (all_algrho_eqs_of ctxt) eval_simps)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
handle e as ERROR _ =>
(case filter (is_none o snd) (const_transfers ~~ const_pointful_natural_opts) of
[] => Exn.reraise e
@@ -549,7 +549,7 @@
Variable.add_free_names ctxt goal []
|> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
unfold_thms_tac ctxt simps THEN HEADGOAL (rtac ctxt rho_transfer')))
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
val goal' = Raw_Simplifier.rewrite_term thy simps [] goal;
in
@@ -567,7 +567,7 @@
mk_rho_transfer_tac ctxt (null abs_rep_transfers) (rel_def_of_bnf pre_bnf)
const_transfers))
|> unfold_thms ctxt [rho_def RS @{thm symmetric}]
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun mk_cong_intro_ctr_or_friend_goal ctxt fpT Rcong alg =
@@ -606,7 +606,7 @@
Variable.add_free_names ctxt goal []
|> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_cong_intro_ctr_or_friend_tac ctxt ctr_def [pre_rel_def, abs_inverse] cong_ctor_intro))
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
val goals = map (mk_cong_intro_ctr_or_friend_goal ctxt fpT Rcong) ctrs;
in
@@ -635,7 +635,7 @@
Variable.add_free_names ctxt goal []
|> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_cong_intro_ctr_or_friend_tac ctxt eq_algrho [] cong_algrho_intro))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_cong_intros lthy ctr_names friend_names
@@ -1912,7 +1912,7 @@
live_nesting_map_ident0s fp_map_ident case_trivial ctr_defs case_eq_ifs all_sig_map_thms
ssig_map_thms all_algLam_alg_pointfuls (all_algrho_eqs_of ctxt) eval_simps corecUU_unique
fun_code)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun derive_coinduct_cong_intros
@@ -2167,7 +2167,7 @@
Variable.add_free_names ctxt goal []
|> (fn vars => Goal.prove (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
HEADGOAL (Transfer.transfer_prover_tac ctxt)))
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
fun maybe_prove_transfer_goal ctxt goal =
(case try (prove_transfer_goal ctxt) goal of
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML Fri Aug 09 17:14:49 2019 +0200
@@ -101,7 +101,7 @@
rtac ctxt refl);
in
Goal.prove_sorry ctxt [] [] goal (fn {context = ctxt, ...} => mk_tac ctxt)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val num_curry_uncurryN_balanced_precomp = 8;
@@ -239,7 +239,7 @@
Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_natural_from_transfer_tac ctxt m (replicate n true) transfer A_nesting_map_ids
A_nesting_rel_Grps [])
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
type s_parse_info =
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Aug 09 17:14:49 2019 +0200
@@ -1147,7 +1147,7 @@
tac_opt;
val excludess'' = @{map 3} (fn tac_opt => fn sequential => map (fn (j, goal) =>
- (j, (Option.map (Goal.prove (*no sorry*) lthy [] [] goal #> Thm.close_derivation)
+ (j, (Option.map (Goal.prove (*no sorry*) lthy [] [] goal #> Thm.close_derivation \<^here>)
(exclude_tac tac_opt sequential j), goal))))
tac_opts sequentials excludess'
handle ERROR _ => use_primcorecursive ();
@@ -1183,12 +1183,12 @@
in
[Goal.prove (*no sorry*) lthy [] [] goal (fn {context = ctxt, ...} =>
mk_primcorec_nchotomy_tac ctxt (res_exhaust_discs @ arg_exhaust_discs))
- |> Thm.close_derivation]
+ |> Thm.close_derivation \<^here>]
handle ERROR _ => use_primcorecursive ()
end
| false =>
(case tac_opt of
- SOME tac => [Goal.prove_sorry lthy [] [] goal tac |> Thm.close_derivation]
+ SOME tac => [Goal.prove_sorry lthy [] [] goal tac |> Thm.close_derivation \<^here>]
| NONE => []))
tac_opts corec_specs disc_eqnss nchotomy_goalss syntactic_exhaustives;
@@ -1232,7 +1232,7 @@
mk_primcorec_exhaust_tac ctxt
("" (* for "P" *) :: map (fst o dest_Free) fun_args)
(length disc_eqns) nchotomy_thm)
- |> Thm.close_derivation])
+ |> Thm.close_derivation \<^here>])
disc_eqnss nchotomy_thmss;
val nontriv_exhaust_thmss = map (filter_out is_trivial_implies) exhaust_thmss;
@@ -1266,7 +1266,7 @@
Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} =>
mk_primcorec_disc_tac ctxt def_thms corec_disc k m excludesss)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> pair (#disc (nth ctr_specs ctr_no))
|> pair eqn_pos
|> single
@@ -1299,7 +1299,7 @@
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
+ |> Thm.close_derivation \<^here>
|> `(is_some code_rhs_opt ? Local_Defs.fold lthy sel_defs) (*mildly too aggressive*)
|> pair sel
|> pair eqn_pos
@@ -1349,7 +1349,7 @@
(fn {context = ctxt, prems = _} =>
mk_primcorec_ctr_tac ctxt m collapse disc_thm_opt sel_thms)
|> is_some code_rhs_opt ? Local_Defs.fold lthy sel_defs (*mildly too aggressive*)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> pair ctr
|> pair eqn_pos
|> single
@@ -1438,12 +1438,12 @@
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;
+ |> Thm.close_derivation \<^here>;
in
Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} =>
mk_primcorec_code_tac ctxt distincts split_sels raw_code_thm)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> single
end)
end)
@@ -1473,7 +1473,7 @@
(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
+ |> Thm.close_derivation \<^here>
|> fold (fn rule => perhaps (try (fn thm => Meson.first_order_resolve lthy thm rule)))
@{thms eqTrueE eq_False[THEN iffD1] notnotD}
|> pair eqn_pos
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Fri Aug 09 17:14:49 2019 +0200
@@ -191,7 +191,7 @@
in
Goal.prove_sorry lthy vars [] (mk_Trueprop_eq (lhs, rhs))
(fn {context = ctxt, prems = _} => mk_map_comp_id_tac ctxt map_comp0)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val map_comp_id_thms = @{map 5} mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps;
@@ -208,7 +208,7 @@
in
Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, goal))
(fn {context = ctxt, prems = _} => mk_map_cong0L_tac ctxt m map_cong0 map_id)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val map_cong0L_thms = @{map 5} mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
@@ -277,7 +277,7 @@
Variable.add_free_names lthy goal []
|> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
mk_alg_set_tac ctxt alg_def))
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
goals
end;
@@ -296,7 +296,7 @@
|> (fn vars => Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} =>
mk_alg_not_empty_tac ctxt alg_set alg_set_thms wit_thms))
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
goals alg_set_thms
end;
@@ -372,7 +372,7 @@
Variable.add_free_names lthy goal []
|> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
mk_mor_elim_tac ctxt mor_def))
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
in
map prove elim_goals
end;
@@ -385,7 +385,7 @@
in
Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
(fn {context = ctxt, prems = _} => mk_mor_incl_tac ctxt mor_def map_ids)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val mor_comp_thm =
@@ -399,7 +399,7 @@
in
Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
(fn {context = ctxt, prems = _} => mk_mor_comp_tac ctxt mor_def set_mapss map_comp_id_thms)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val mor_cong_thm =
@@ -411,7 +411,7 @@
in
Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
(fn {context = ctxt, prems = _} => (hyp_subst_tac ctxt THEN' assume_tac ctxt) 1)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val mor_str_thm =
@@ -424,7 +424,7 @@
in
Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => mk_mor_str_tac ctxt ks mor_def)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val mor_UNIV_thm =
@@ -438,7 +438,7 @@
in
Goal.prove_sorry lthy vars [] (mk_Trueprop_eq (lhs, rhs))
(fn {context = ctxt, prems = _} => mk_mor_UNIV_tac ctxt m morE_thms mor_def)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val timer = time (timer "Morphism definition & thms");
@@ -552,7 +552,7 @@
in
Goal.prove_sorry lthy vars [] (Logic.list_implies ([prem], concl))
(fn {context = ctxt, prems = _} => mk_bd_limit_tac ctxt n suc_bd_Cinfinite)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val timer = time (timer "Bounds");
@@ -592,7 +592,7 @@
val min_algs_thm = Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => mk_min_algs_tac ctxt suc_bd_worel in_cong'_thms)
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
val min_algs_thms = map (fn k => min_algs_thm RS mk_nthI n k) ks;
@@ -604,7 +604,7 @@
Variable.add_free_names lthy goal []
|> (fn vars => Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => mk_min_algs_mono_tac ctxt min_algs))
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
(map mk_mono_goal min_algss) min_algs_thms;
fun mk_card_conjunct min_alg = mk_ordLeq (mk_card_of min_alg) Asuc_bd;
@@ -622,7 +622,7 @@
m suc_bd_worel min_algs_thms in_sbds
sbd_Card_order sbd_Cnotzero suc_bd_Card_order suc_bd_Cinfinite suc_bd_Cnotzero
suc_bd_Asuc_bd Asuc_bd_Cinfinite)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val least_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
@@ -639,7 +639,7 @@
Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => mk_min_algs_least_tac ctxt least_cT least_ct
suc_bd_worel min_algs_thms alg_set_thms)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
in
(min_algs_thms, monos, card_of, least)
@@ -698,7 +698,7 @@
Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => mk_alg_min_alg_tac ctxt m alg_def min_alg_defs
suc_bd_limit_thm sbd_Cinfinite set_sbdss min_algs_thms min_algs_mono_thms)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun mk_card_of_thm min_alg def =
@@ -709,7 +709,7 @@
Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => mk_card_of_min_alg_tac ctxt def card_of_min_algs_thm
suc_bd_Card_order suc_bd_Asuc_bd Asuc_bd_Cinfinite)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun mk_least_thm min_alg B def =
@@ -720,7 +720,7 @@
in
Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => mk_least_min_alg_tac ctxt def least_min_algs_thm)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val leasts = @{map 3} mk_least_thm min_algs Bs min_alg_defs;
@@ -735,7 +735,7 @@
Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} =>
EVERY' (rtac ctxt mor_incl_thm :: map (etac ctxt) leasts) 1)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
in
(alg_min_alg, map2 mk_card_of_thm min_algs min_alg_defs, leasts, incl)
@@ -830,7 +830,7 @@
(HOLogic.mk_Trueprop (mk_Ball II
(Term.absfree iidx' (mk_alg select_Bs select_ss))))
(fn {context = ctxt, prems = _} => mk_alg_select_tac ctxt Abs_IIT_inverse_thm)
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
val mor_select_thm =
let
@@ -846,7 +846,7 @@
(fn {context = ctxt, prems = _} => mk_mor_select_tac ctxt mor_def mor_cong_thm
mor_comp_thm mor_incl_min_alg_thm alg_def alg_select_thm alg_set_thms set_mapss
str_init_defs)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val init_unique_mor_thms =
@@ -865,7 +865,7 @@
Goal.prove_sorry lthy vars [] (Logic.list_implies (all_prems, unique))
(fn {context = ctxt, prems = _} => mk_init_unique_mor_tac ctxt cts m alg_def
alg_init_thm least_min_alg_thms in_mono'_thms alg_set_thms morE_thms map_cong0s)
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
in
split_conj_thm unique_mor
end;
@@ -899,7 +899,7 @@
Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, concl))
(fn {context = ctxt, prems = _} => mk_init_induct_tac ctxt m alg_def alg_init_thm
least_min_alg_thms alg_set_thms)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val timer = time (timer "Initiality definition & thms");
@@ -977,7 +977,7 @@
(HOLogic.mk_Trueprop (mk_mor UNIVs ctors car_inits str_inits Rep_Ts))
(fn {context = ctxt, prems = _} => mk_mor_Rep_tac ctxt m defs Reps Abs_inverses
alg_min_alg_thm alg_set_thms set_mapss)
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
fun mk_ct initFT str abs = Term.absdummy initFT (abs $ (str $ Bound 0))
val cts = @{map 3} (Thm.cterm_of lthy ooo mk_ct) init_FTs str_inits Abs_Ts;
@@ -987,7 +987,7 @@
(HOLogic.mk_Trueprop (mk_mor car_inits str_inits UNIVs ctors Abs_Ts))
(fn {context = ctxt, prems = _} => mk_mor_Abs_tac ctxt cts defs Abs_inverses
map_comp_id_thms map_cong0L_thms)
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
in
(mor_Rep, mor_Abs)
end;
@@ -1046,7 +1046,7 @@
Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
(fn {context = ctxt, prems = _} => mk_copy_tac ctxt m alg_def mor_def alg_set_thms
set_mapss)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val init_ex_mor_thm =
@@ -1059,7 +1059,7 @@
(fn {context = ctxt, prems = _} =>
mk_init_ex_mor_tac ctxt Abs_IIT_inverse_thm (alg_min_alg_thm RS copy_thm)
card_of_min_alg_thms mor_Rep_thm mor_comp_thm mor_select_thm mor_incl_thm)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val mor_fold_thm =
@@ -1073,7 +1073,7 @@
Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, ...} =>
mk_mor_fold_tac ctxt cT ct fold_defs init_ex_mor_thm mor_cong)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val ctor_fold_thms = map (fn morE => rule_by_tactic lthy
@@ -1089,7 +1089,7 @@
val unique_mor = Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, unique))
(fn {context = ctxt, prems = _} => mk_fold_unique_mor_tac ctxt type_defs
init_unique_mor_thms Reps mor_comp_thm mor_Abs_thm mor_fold_thm)
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
in
`split_conj_thm unique_mor
end;
@@ -1148,7 +1148,7 @@
Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} => mk_dtor_o_ctor_tac ctxt dtor_def foldx map_comp_id
map_cong0L ctor_o_fold_thms)
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
goals dtor_defs ctor_fold_thms map_comp_id_thms map_cong0L_thms
end;
@@ -1215,7 +1215,7 @@
(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,
+ |> Thm.close_derivation \<^here>,
rev (Term.add_tfrees goal []))
end;
@@ -1258,7 +1258,7 @@
(Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => mk_ctor_induct2_tac ctxt cTs cts ctor_induct_thm
weak_ctor_induct_thms)
- |> Thm.close_derivation,
+ |> Thm.close_derivation \<^here>,
rev (Term.add_tfrees goal []))
end;
@@ -1495,7 +1495,7 @@
|> (fn vars => Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Imap_defs THEN
mk_map_tac ctxt m n foldx map_comp_id map_cong0))
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
goals ctor_fold_thms map_comp_id_thms map_cong0s;
in
`(map (fn thm => thm RS @{thm comp_eq_dest})) maps
@@ -1514,7 +1514,7 @@
val unique = Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, goal))
(fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Imap_defs THEN
mk_ctor_map_unique_tac ctxt ctor_fold_unique_thm sym_map_comps)
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
in
`split_conj_thm unique
end;
@@ -1532,7 +1532,7 @@
val setss = map (map2 (fn foldx => fn goal =>
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
unfold_thms_tac ctxt Iset_defs THEN mk_set_tac ctxt foldx)
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
ctor_fold_thms) goalss;
fun mk_simp_goal pas_set act_sets sets ctor z set =
@@ -1550,7 +1550,7 @@
|> (fn vars => Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} =>
mk_ctor_set_tac ctxt set (nth set_nats (i - 1)) (drop m set_nats)))
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
set_mapss) ls simp_goalss setss;
in
ctor_setss
@@ -1597,7 +1597,7 @@
Variable.add_free_names lthy goal []
|> (fn vars => Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => mk_tac ctxt induct csets ctor_sets i))
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
goals csetss ctor_Iset_thmss inducts ls;
in
map split_conj_thm thms
@@ -1626,7 +1626,7 @@
|> (fn vars => Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Ibd_defs THEN
mk_tac ctxt induct ctor_sets i))
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
goals ctor_Iset_thmss inducts ls;
in
map split_conj_thm thms
@@ -1657,7 +1657,7 @@
val thm = Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => mk_mcong_tac ctxt (rtac ctxt induct) set_Iset_thmsss
map_cong0s ctor_Imap_thms)
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
in
split_conj_thm thm
end;
@@ -1693,7 +1693,7 @@
(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)
+ |> Thm.close_derivation \<^here>)
ks goals in_rels map_comps map_cong0s ctor_Imap_thms ctor_Iset_thmss'
ctor_inject_thms ctor_dtor_thms set_mapss ctor_Iset_incl_thmss
ctor_set_Iset_incl_thmsss
@@ -1718,7 +1718,7 @@
Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => mk_le_rel_OO_tac ctxt m induct ctor_nchotomy_thms
ctor_Irel_thms rel_mono_strong0s le_rel_OOs)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val timer = time (timer "helpers for BNF properties");
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Fri Aug 09 17:14:49 2019 +0200
@@ -158,7 +158,7 @@
fun prove goal =
Goal.prove_sorry ctxt [] [] goal (tac o #context)
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
in
map (map prove) goalss
end;
--- a/src/HOL/Tools/BNF/bnf_lfp_countable.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_countable.ML Fri Aug 09 17:14:49 2019 +0200
@@ -178,7 +178,7 @@
inj_map_strongs')
|> HOLogic.conj_elims ctxt
|> Proof_Context.export names_ctxt ctxt
- |> map Thm.close_derivation
+ |> map (Thm.close_derivation \<^here>)
end;
fun get_countable_goal_type_name (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>Ex\<close>, _)
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Fri Aug 09 17:14:49 2019 +0200
@@ -557,7 +557,7 @@
(fn {context = ctxt, prems = _} =>
mk_primrec_tac ctxt num_extra_args fp_nesting_map_ident0s fp_nesting_map_comps
fp_nesting_pred_maps def_thms rec_thm)
- |> Thm.close_derivation);
+ |> Thm.close_derivation \<^here>);
in
((js, simps), lthy')
end;
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Aug 09 17:14:49 2019 +0200
@@ -300,7 +300,7 @@
mk_size_neq ctxt (map (Thm.cterm_of lthy2) xs)
(#exhaust (#ctr_sugar (#fp_ctr_sugar fp_sugar))) size_thms)
|> single
- |> map Thm.close_derivation;
+ |> map (Thm.close_derivation \<^here>);
in thm end) fp_sugars overloaded_size_consts overloaded_size_simpss;
val ABs = As ~~ Bs;
@@ -347,7 +347,7 @@
@{map 3} (fn goal => fn size_def => fn rec_o_map =>
Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} =>
mk_size_gen_o_map_tac ctxt size_def rec_o_map all_inj_maps nested_size_maps)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> single)
size_gen_o_map_goals size_defs rec_o_maps
else
--- a/src/HOL/Tools/BNF/bnf_tactics.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_tactics.ML Fri Aug 09 17:14:49 2019 +0200
@@ -59,7 +59,7 @@
(K (rtac ctxt ext 1 THEN
unfold_thms_tac ctxt ([o_apply, unfold_thms ctxt [o_apply] (mk_sym thm)]) THEN
rtac ctxt refl 1)))
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
(* Theorems for open typedefs with UNIV as representing set *)
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Aug 09 17:14:49 2019 +0200
@@ -731,7 +731,7 @@
in
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
mk_nchotomy_tac ctxt n exhaust_thm)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val case_thms =
@@ -743,7 +743,7 @@
@{map 4} (fn k => fn goal => fn injects => fn distinctss =>
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
mk_case_tac ctxt n k case_def injects distinctss)
- |> Thm.close_derivation)
+ |> Thm.close_derivation \<^here>)
ks goals inject_thmss distinct_thmsss
end;
@@ -764,7 +764,7 @@
mk_case_cong_tac ctxt uexhaust_thm case_thms),
Goal.prove_sorry lthy weak_vars [] weak_goal (fn {context = ctxt, prems = _} =>
etac ctxt arg_cong 1))
- |> apply2 (Thm.close_derivation)
+ |> apply2 (Thm.close_derivation \<^here>)
end;
val split_lhs = q $ ufcase;
@@ -786,13 +786,13 @@
Variable.add_free_names lthy goal []
|> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
mk_split_tac ctxt uexhaust_thm case_thms selss inject_thmss distinct_thmsss))
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
fun prove_split_asm asm_goal split_thm =
Variable.add_free_names lthy asm_goal []
|> (fn vars => Goal.prove_sorry lthy vars [] asm_goal (fn {context = ctxt, ...} =>
mk_split_asm_tac ctxt split_thm))
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
val (split_thm, split_asm_thm) =
let
@@ -851,7 +851,7 @@
in
Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
mk_unique_disc_def_tac ctxt m uexhaust_thm)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
fun mk_alternate_disc_def k =
@@ -864,7 +864,7 @@
Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} =>
mk_alternate_disc_def_tac ctxt k (nth disc_defs (2 - k))
(nth distinct_thms (2 - k)) uexhaust_thm)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val has_alternate_disc_def =
@@ -917,7 +917,7 @@
fun prove tac goal =
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => tac ctxt)
- |> Thm.close_derivation;
+ |> Thm.close_derivation \<^here>;
val half_pairss = mk_half_pairss (`I (ms ~~ discD_thms ~~ udiscs));
@@ -945,7 +945,7 @@
in
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
mk_exhaust_disc_tac ctxt n exhaust_thm discI_thms)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val (safe_collapse_thms, all_collapse_thms) =
@@ -962,7 +962,7 @@
@{map 5} (fn m => fn discD => fn sel_thms => fn triv => fn goal =>
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
mk_collapse_tac ctxt m discD sel_thms ORELSE HEADGOAL (assume_tac ctxt))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> not triv ? perhaps (try (fn thm => refl RS thm)))
ms discD_thms sel_thmss trivs goals;
in
@@ -980,7 +980,7 @@
in
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
mk_exhaust_sel_tac ctxt n exhaust_disc_thm swapped_all_collapse_thms)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val expand_thm =
@@ -1006,7 +1006,7 @@
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')
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val (split_sel_thm, split_sel_asm_thm) =
@@ -1028,7 +1028,7 @@
in
Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} =>
mk_case_eq_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val disc_eq_case_thms =
@@ -1044,7 +1044,7 @@
Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, ...} => mk_disc_eq_case_tac ctxt (Thm.cterm_of ctxt u)
exhaust_thm (flat nontriv_disc_thmss) distinct_thms case_thms)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> Conjunction.elim_balanced (length goals)
end;
in
@@ -1066,7 +1066,7 @@
in
Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} =>
mk_case_distrib_tac ctxt (Thm.cterm_of ctxt u) exhaust_thm case_thms)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
end;
val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
@@ -1151,7 +1151,7 @@
end;
fun free_constructors kind tacss = (fn (goalss, after_qed, lthy) =>
- map2 (map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])) goalss tacss
+ map2 (map2 (Thm.close_derivation \<^here> oo Goal.prove_sorry lthy [] [])) goalss tacss
|> (fn thms => after_qed thms lthy)) oo prepare_free_constructors kind (K I) (K I);
fun free_constructors_cmd kind = (fn (goalss, after_qed, lthy) =>
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Fri Aug 09 17:14:49 2019 +0200
@@ -76,7 +76,7 @@
fun proves goals = goals
|> Logic.mk_conjunction_balanced
|> prove
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> Conjunction.elim_balanced (length goals)
|> map Simpdata.mk_eq;
in
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Fri Aug 09 17:14:49 2019 +0200
@@ -221,11 +221,13 @@
fun name_noted_thms _ _ [] = []
| name_noted_thms qualifier base ((local_name, thms) :: noted) =
if Long_Name.base_name local_name = base then
- (local_name,
- map_index (uncurry (fn j => Thm.name_derivation (Long_Name.append qualifier base ^
- (if can the_single thms then "" else "_" ^ string_of_int (j + 1))))) thms) :: noted
- else
- ((local_name, thms) :: name_noted_thms qualifier base noted);
+ let
+ val thms' = thms |> map_index (uncurry (fn j =>
+ Thm.name_derivation
+ (((Long_Name.append qualifier base ^
+ (if can the_single thms then "" else "_" ^ string_of_int (j + 1))), Position.none))))
+ in (local_name, thms') :: noted end
+ else ((local_name, thms) :: name_noted_thms qualifier base noted);
fun substitute_noted_thm noted =
let val tab = fold (fold (Termtab.default o `Thm.full_prop_of) o snd) noted Termtab.empty in
--- a/src/HOL/Tools/Function/function.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/Function/function.ML Fri Aug 09 17:14:49 2019 +0200
@@ -90,7 +90,7 @@
fun afterqed [[proof]] lthy =
let
- val result = cont lthy (Thm.close_derivation proof)
+ val result = cont lthy (Thm.close_derivation \<^here> proof)
val FunctionResult {fs, R, dom, psimps, simple_pinducts,
termination, domintros, cases, ...} = result
@@ -185,7 +185,7 @@
val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
fun afterqed [[totality]] lthy =
let
- val totality = Thm.close_derivation totality
+ val totality = Thm.close_derivation \<^here> totality
val remove_domain_condition =
full_simplify (put_simpset HOL_basic_ss lthy
addsimps [totality, @{thm True_implies_equals}])
--- a/src/HOL/Tools/Function/function_core.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/Function/function_core.ML Fri Aug 09 17:14:49 2019 +0200
@@ -275,7 +275,7 @@
|> fold_rev (Thm.implies_intr o Thm.cprop_of) h_assums
|> fold_rev (Thm.implies_intr o Thm.cprop_of) ags
|> fold_rev Thm.forall_intr cqs
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
in
replace_lemma
end
@@ -426,7 +426,7 @@
(Term.add_vars (Thm.prop_of it) []) it)
val goalstate = Conjunction.intr graph_is_function complete
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> Goal.protect 0
|> fold_rev (Thm.implies_intr o Thm.cprop_of) compat
|> Thm.implies_intr (Thm.cprop_of complete)
--- a/src/HOL/Tools/Lifting/lifting_bnf.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Fri Aug 09 17:14:49 2019 +0200
@@ -67,7 +67,7 @@
in
Goal.prove_sorry ctxt'' [] [] goal
(fn {context = goal_ctxt, ...} => Quotient_tac bnf goal_ctxt 1)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> singleton (Variable.export ctxt'' ctxt)
|> Drule.zero_var_indexes
end
--- a/src/HOL/Tools/Lifting/lifting_def.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Fri Aug 09 17:14:49 2019 +0200
@@ -664,7 +664,7 @@
let
val rsp_thm =
Goal.prove_sorry lthy [] [] goal (tac o #context)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
in
after_qed rsp_thm lthy
end
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Fri Aug 09 17:14:49 2019 +0200
@@ -288,7 +288,7 @@
val f'_rsp = Goal.prove_sorry lthy3 [] [] f'_rsp_goal
(fn {context = ctxt, prems = _} =>
HEADGOAL (CONVERSION (rel_eq_onps_conv) THEN' rtac ctxt rsp_norm))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
val (f'_lift_def, lthy4) = add_lift_def ld_no_notes f'_var f'_qty rhs f'_rsp [] lthy3
val f'_lift_def = inst_of_lift_def lthy4 f'_qty f'_lift_def
val f'_lift_const = mk_lift_const_of_lift_def f'_qty f'_lift_def
@@ -306,7 +306,7 @@
val f_alt_def =
Goal.prove_sorry transfer_ctxt [] [] f_alt_def_goal
(fn {context = goal_ctxt, ...} => HEADGOAL (f_alt_def_tac goal_ctxt))
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> singleton (Variable.export transfer_ctxt lthy4)
val lthy5 = lthy4
|> Local_Theory.note ((Binding.empty, @{attributes [code]}), [f_alt_def])
@@ -458,7 +458,7 @@
val quot_thm_isom =
Goal.prove_sorry transfer_ctxt [] [] typedef_goal
(fn {context = goal_ctxt, ...} => typ_isom_tac goal_ctxt 1)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> singleton (Variable.export transfer_ctxt lthy6)
|> (fn thm => @{thm UNIV_typedef_to_Quotient} OF [thm, @{thm reflexive}])
val qty_isom_name = Tname qty_isom;
@@ -540,7 +540,7 @@
val rep_isom_code =
Goal.prove_sorry x_ctxt [] [] rep_isom_code_goal
(fn {context = goal_ctxt, ...} => rep_isom_code_tac ctr_sugar goal_ctxt 1)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> singleton(Variable.export x_ctxt lthy6)
in
lthy6
--- a/src/HOL/Tools/Meson/meson_clausify.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Fri Aug 09 17:14:49 2019 +0200
@@ -384,7 +384,7 @@
#> (case opt of SOME (_, ct) => intr_imp ct | NONE => I))
|> Variable.export ctxt2 ctxt0
|> finish_cnf
- |> map Thm.close_derivation)
+ |> map (Thm.close_derivation \<^here>))
end
handle THM _ => (NONE, [])
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Fri Aug 09 17:14:49 2019 +0200
@@ -93,7 +93,7 @@
in
Goal.prove_sorry ctxt' [] [] goal (fn {context = goal_ctxt, ...} =>
side_constraint_tac bnf [constraint_def] goal_ctxt 1)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> singleton (Variable.export ctxt' ctxt)
|> Drule.zero_var_indexes
end
@@ -104,7 +104,7 @@
in
Goal.prove_sorry ctxt' [] [] goal (fn {context = goal_ctxt, ...} =>
bi_constraint_tac constraint_def side_constraints goal_ctxt 1)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> singleton (Variable.export ctxt' ctxt)
|> Drule.zero_var_indexes
end
@@ -189,7 +189,7 @@
in
Goal.prove_sorry ctxt'' [] [] goal (fn {context = goal_ctxt, ...} =>
Domainp_tac bnf pred_def goal_ctxt 1)
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> singleton (Variable.export ctxt'' ctxt)
|> Drule.zero_var_indexes
end
--- a/src/Pure/General/binding.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/Pure/General/binding.ML Fri Aug 09 17:14:49 2019 +0200
@@ -18,6 +18,7 @@
val set_pos: Position.T -> binding -> binding
val reset_pos: binding -> binding
val default_pos: binding -> binding
+ val default_pos_of: binding -> Position.T
val name: bstring -> binding
val name_of: binding -> bstring
val map_name: (bstring -> bstring) -> binding -> binding
@@ -95,6 +96,10 @@
fun default_pos b =
if pos_of b = Position.none then set_pos (Position.thread_data ()) b else b;
+fun default_pos_of b =
+ let val pos = pos_of b
+ in if pos = Position.none then Position.thread_data () else pos end;
+
(* name *)
--- a/src/Pure/Isar/code.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/Pure/Isar/code.ML Fri Aug 09 17:14:49 2019 +0200
@@ -90,11 +90,6 @@
(** auxiliary **)
-(* close theorem for storage *)
-
-val close = Thm.trim_context o Thm.close_derivation;
-
-
(* printing *)
fun string_of_typ thy =
@@ -1012,13 +1007,13 @@
Abstract (snd (constrain_thm thy (fst (typscheme_abs thy abs_thm)) sorts abs_thm), tyco);
fun conclude_cert (Nothing cert_thm) =
- Nothing (Thm.close_derivation cert_thm)
+ Nothing (Thm.close_derivation \<^here> cert_thm)
| conclude_cert (Equations (cert_thm, propers)) =
- Equations (Thm.close_derivation cert_thm, propers)
+ Equations (Thm.close_derivation \<^here> cert_thm, propers)
| conclude_cert (cert as Projection _) =
cert
| conclude_cert (Abstract (abs_thm, tyco)) =
- Abstract (Thm.close_derivation abs_thm, tyco);
+ Abstract (Thm.close_derivation \<^here> abs_thm, tyco);
fun typscheme_of_cert thy (Nothing cert_thm) =
fst (get_head thy cert_thm)
@@ -1403,7 +1398,7 @@
(if verbose then warning ("Code generator: dropping subsumed code equation\n" ^
Thm.string_of_thm_global thy thm') else (); true)
else false;
- in (close thm, proper) :: filter_out drop eqns end;
+ in (thm |> Thm.close_derivation \<^here> |> Thm.trim_context, proper) :: filter_out drop eqns end;
fun add_eqn_for (c, eqn) thy =
thy |> modify_specs (modify_pending_eqns c (subsumptive_add thy true eqn));
@@ -1419,7 +1414,7 @@
else specs);
fun add_abstract_for (c, (thm, tyco_abs as (tyco, _))) =
- modify_specs (register_fun_spec c (Abstr (Thm.close_derivation thm, tyco_abs))
+ modify_specs (register_fun_spec c (Abstr (Thm.close_derivation \<^here> thm, tyco_abs))
#> map_types (History.modify_entry tyco (add_abstract_function c)))
in
--- a/src/Pure/Isar/element.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/Pure/Isar/element.ML Fri Aug 09 17:14:49 2019 +0200
@@ -273,7 +273,7 @@
fun prove_witness ctxt t tac =
Witness (t,
- Thm.close_derivation
+ Thm.close_derivation \<^here>
(Goal.prove ctxt [] [] (mark_witness t)
(fn _ => resolve_tac ctxt [Drule.protectI] 1 THEN tac)));
@@ -290,7 +290,7 @@
(map o map) (fn prop => (mark_witness prop, [])) wit_propss @
[map (rpair []) eq_props];
fun after_qed' thmss =
- let val (wits, eqs) = split_last ((map o map) Thm.close_derivation thmss);
+ let val (wits, eqs) = split_last ((map o map) (Thm.close_derivation \<^here>) thmss);
in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
in proof after_qed' propss #> refine_witness end;
@@ -322,7 +322,7 @@
end;
fun conclude_witness ctxt (Witness (_, th)) =
- Thm.close_derivation (Raw_Simplifier.norm_hhf_protect ctxt (Goal.conclude th));
+ Thm.close_derivation \<^here> (Raw_Simplifier.norm_hhf_protect ctxt (Goal.conclude th));
fun pretty_witness ctxt witn =
let val prt_term = Pretty.quote o Syntax.pretty_term ctxt in
--- a/src/Pure/Isar/generic_target.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/Pure/Isar/generic_target.ML Fri Aug 09 17:14:49 2019 +0200
@@ -303,13 +303,16 @@
in (result'', result) end;
+fun bind_name lthy b =
+ (Local_Theory.full_name lthy b, Binding.default_pos_of b);
+
in
fun notes target_notes kind facts lthy =
let
val facts' = facts
- |> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi
- (Local_Theory.full_name lthy (fst a))) bs))
+ |> map (fn (a, bs) =>
+ (a, Global_Theory.burrow_fact (Global_Theory.name_multi (bind_name lthy (fst a))) bs))
|> Global_Theory.map_facts (import_export_proof lthy);
val local_facts = Global_Theory.map_facts #1 facts';
val global_facts = Global_Theory.map_facts #2 facts';
--- a/src/Pure/Isar/proof.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/Pure/Isar/proof.ML Fri Aug 09 17:14:49 2019 +0200
@@ -497,7 +497,7 @@
fun err_lost () = error ("Lost goal structure:\n" ^ Thm.string_of_thm ctxt goal);
val th =
- (Goal.conclude (Thm.close_derivation goal) handle THM _ => err_lost ())
+ (Goal.conclude (Thm.close_derivation \<^here> goal) handle THM _ => err_lost ())
|> Drule.flexflex_unique (SOME ctxt)
|> Thm.check_shyps ctxt
|> Thm.check_hyps (Context.Proof ctxt);
--- a/src/Pure/Isar/proof_context.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/Pure/Isar/proof_context.ML Fri Aug 09 17:14:49 2019 +0200
@@ -1074,27 +1074,29 @@
fun update_facts flags (b, SOME ths) ctxt = ctxt |> add_facts flags (b, Lazy.value ths) |> #2
| update_facts _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b));
+fun bind_name ctxt b = (full_name ctxt b, Binding.default_pos_of b);
+
in
fun add_thms_lazy kind (b, ths) ctxt =
let
- val name = full_name ctxt b;
+ val name_pos = bind_name ctxt b;
val ths' =
Global_Theory.check_thms_lazy ths
|> Lazy.map_finished
- (Global_Theory.name_thms Global_Theory.unofficial1 name #> map (Thm.kind_rule kind));
+ (Global_Theory.name_thms Global_Theory.unofficial1 name_pos #> map (Thm.kind_rule kind));
val (_, ctxt') = add_facts {index = is_stmt ctxt} (b, ths') ctxt;
in ctxt' end;
fun note_thms kind ((b, more_atts), facts) ctxt =
let
- val name = full_name ctxt b;
+ val (name, pos) = bind_name ctxt b;
val facts' = facts
- |> Global_Theory.burrow_fact (Global_Theory.name_thms Global_Theory.unofficial1 name);
+ |> Global_Theory.burrow_fact (Global_Theory.name_thms Global_Theory.unofficial1 (name, pos));
fun app (ths, atts) =
fold_map (Thm.proof_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths;
val (res, ctxt') = fold_map app facts' ctxt;
- val thms = Global_Theory.name_thms Global_Theory.unofficial2 name (flat res);
+ val thms = Global_Theory.name_thms Global_Theory.unofficial2 (name, pos) (flat res);
val (_, ctxt'') = ctxt' |> add_facts {index = is_stmt ctxt} (b, Lazy.value thms);
in ((name, thms), ctxt'') end;
--- a/src/Pure/ML/ml_thms.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/Pure/ML/ml_thms.ML Fri Aug 09 17:14:49 2019 +0200
@@ -91,7 +91,7 @@
val _ = Context_Position.reports ctxt reports;
val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
- val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation;
+ val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation \<^here>;
fun after_qed res goal_ctxt =
Proof_Context.put_thms false (Auto_Bind.thisN,
SOME (map prep_result (Proof_Context.export goal_ctxt ctxt (flat res)))) goal_ctxt;
--- a/src/Pure/Proof/extraction.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/Pure/Proof/extraction.ML Fri Aug 09 17:14:49 2019 +0200
@@ -595,8 +595,9 @@
(corr_prf1 % u %% corr_prf2, defs2)
end
- | corr d vs ts Ts hs cs _ (prf0 as PThm ({name, prop, types = SOME Ts', ...}, thm_body)) _ defs =
+ | corr d vs ts Ts hs cs _ (prf0 as PThm (thm_header as {types = SOME Ts', ...}, thm_body)) _ defs =
let
+ val {pos, name, prop, ...} = thm_header;
val prf = Proofterm.thm_body_proof_open thm_body;
val (vs', tye) = find_inst prop Ts ts vs;
val shyps = mk_shyps tye;
@@ -621,7 +622,7 @@
val corr_prf = mkabsp shyps corr_prf0;
val corr_prop = Proofterm.prop_of corr_prf;
val corr_header =
- Proofterm.thm_header (Proofterm.proof_serial ()) (corr_name name vs')
+ Proofterm.thm_header (Proofterm.proof_serial ()) pos (corr_name name vs')
corr_prop (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
val corr_body =
Proofterm.thm_body I (Future.value (Proofterm.approximate_proof_body corr_prf));
@@ -696,8 +697,9 @@
in (f $ t, defs'') end
end
- | extr d vs ts Ts hs (prf0 as PThm ({name = s, prop, types = SOME Ts', ...}, thm_body)) defs =
+ | extr d vs ts Ts hs (prf0 as PThm (thm_header as {types = SOME Ts', ...}, thm_body)) defs =
let
+ val {pos, name = s, prop, ...} = thm_header;
val prf = Proofterm.thm_body_proof_open thm_body;
val (vs', tye) = find_inst prop Ts ts vs;
val shyps = mk_shyps tye;
@@ -741,7 +743,7 @@
SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf);
val corr_prop = Proofterm.prop_of corr_prf';
val corr_header =
- Proofterm.thm_header (Proofterm.proof_serial ()) (corr_name s vs')
+ Proofterm.thm_header (Proofterm.proof_serial ()) pos (corr_name s vs')
corr_prop (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
val corr_body =
Proofterm.thm_body I
--- a/src/Pure/drule.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/Pure/drule.ML Fri Aug 09 17:14:49 2019 +0200
@@ -256,7 +256,7 @@
val export_without_context =
flexflex_unique NONE
#> export_without_context_open
- #> Thm.close_derivation;
+ #> Thm.close_derivation \<^here>;
(*Rotates a rule's premises to the left by k*)
--- a/src/Pure/global_theory.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/Pure/global_theory.ML Fri Aug 09 17:14:49 2019 +0200
@@ -20,15 +20,15 @@
val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list
val burrow_facts: ('a list -> 'b list) ->
('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
- val name_multi: string -> 'a list -> (string * 'a) list
+ val name_multi: string * Position.T -> 'a list -> ((string * Position.T) * 'a) list
type name_flags
val unnamed: name_flags
val official1: name_flags
val official2: name_flags
val unofficial1: name_flags
val unofficial2: name_flags
- val name_thm: name_flags -> string -> thm -> thm
- val name_thms: name_flags -> string -> thm list -> thm list
+ val name_thm: name_flags -> string * Position.T -> thm -> thm
+ val name_thms: name_flags -> string * Position.T -> thm list -> thm list
val check_thms_lazy: thm list lazy -> thm list lazy
val add_thms_lazy: string -> (binding * thm list lazy) -> theory -> theory
val store_thm: binding * thm -> theory -> thm * theory
@@ -122,35 +122,39 @@
val unofficial1 = Name_Flags {pre = true, official = false};
val unofficial2 = Name_Flags {pre = false, official = false};
-fun name_thm name_flags name =
+fun name_thm name_flags (name, pos) =
Thm.solve_constraints #> (fn thm =>
(case name_flags of
No_Name_Flags => thm
| Name_Flags {pre, official} =>
thm
|> (official andalso (not pre orelse Thm.derivation_name thm = "")) ?
- Thm.name_derivation name
+ Thm.name_derivation (name, pos)
|> (name <> "" andalso (not pre orelse not (Thm.has_name_hint thm))) ?
Thm.put_name_hint name));
end;
-fun name_multi name [x] = [(name, x)]
- | name_multi "" xs = map (pair "") xs
- | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs;
+fun name_multi (name, pos: Position.T) xs =
+ (case xs of
+ [x] => [((name, pos), x)]
+ | _ =>
+ if name = "" then map (pair ("", pos)) xs
+ else map_index (fn (i, x) => ((name ^ "_" ^ string_of_int (i + 1), pos), x)) xs);
-fun name_thms name_flags name thms =
- map (uncurry (name_thm name_flags)) (name_multi name thms);
+fun name_thms name_flags name_pos thms =
+ map (uncurry (name_thm name_flags)) (name_multi name_pos thms);
(* apply theorems and attributes *)
fun register_proofs thms thy = (thms, Thm.register_proofs (Lazy.value thms) thy);
+fun bind_name thy b = (Sign.full_name thy b, Binding.default_pos_of b);
+
fun add_facts (b, fact) thy =
let
- val full_name = Sign.full_name thy b;
- val pos = Binding.pos_of b;
+ val (full_name, pos) = bind_name thy b;
fun check fact =
fact |> map_index (fn (i, thm) =>
let
@@ -183,10 +187,10 @@
if Binding.is_empty b then Thm.register_proofs (check_thms_lazy thms) thy
else
let
- val name = Sign.full_name thy b;
+ val name_pos = bind_name thy b;
val thms' =
check_thms_lazy thms
- |> Lazy.map_finished (name_thms official1 name #> map (Thm.kind_rule kind));
+ |> Lazy.map_finished (name_thms official1 name_pos #> map (Thm.kind_rule kind));
in thy |> Thm.register_proofs thms' |> add_facts (b, thms') end;
val app_facts =
@@ -196,10 +200,10 @@
if Binding.is_empty b then app_facts facts thy |-> register_proofs
else
let
- val name = Sign.full_name thy b;
+ val name_pos= bind_name thy b;
val (thms', thy') = thy
- |> app_facts (map (apfst (name_thms name_flags1 name)) facts)
- |>> name_thms name_flags2 name |-> register_proofs;
+ |> app_facts (map (apfst (name_thms name_flags1 name_pos)) facts)
+ |>> name_thms name_flags2 name_pos |-> register_proofs;
val thy'' = thy' |> add_facts (b, Lazy.value thms');
in (map (Thm.transfer thy'') thms', thy'') end;
--- a/src/Pure/goal.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/Pure/goal.ML Fri Aug 09 17:14:49 2019 +0200
@@ -136,7 +136,7 @@
Thm.solve_constraints);
val local_result =
Thm.future global_result global_prop
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> Thm.instantiate (instT, [])
|> Drule.forall_elim_list fixes
|> fold (Thm.elim_implies o Thm.assume) assms
@@ -220,7 +220,7 @@
(Thm.term_of stmt);
in
res
- |> Thm.close_derivation
+ |> Thm.close_derivation \<^here>
|> Conjunction.elim_balanced (length props)
|> map (Assumption.export false ctxt' ctxt)
|> Variable.export ctxt' ctxt
--- a/src/Pure/proofterm.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/Pure/proofterm.ML Fri Aug 09 17:14:49 2019 +0200
@@ -11,7 +11,7 @@
type thm_node
type proof_serial = int
type thm_header =
- {serial: proof_serial, name: string, prop: term, types: typ list option}
+ {serial: proof_serial, pos: Position.T, name: string, prop: term, types: typ list option}
type thm_body
datatype proof =
MinProof
@@ -40,7 +40,7 @@
type oracle = string * term
val proof_of: proof_body -> proof
val map_proof_of: (proof -> proof) -> proof_body -> proof_body
- val thm_header: proof_serial -> string -> term -> typ list option -> thm_header
+ val thm_header: proof_serial -> Position.T -> string -> term -> typ list option -> thm_header
val thm_body: (proof -> proof) -> proof_body future -> thm_body
val thm_body_proof_raw: thm_body -> proof
val thm_body_proof_open: thm_body -> proof
@@ -165,8 +165,8 @@
val proof_serial: unit -> proof_serial
val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
val thm_proof: theory -> (class * class -> proof) ->
- (string * class list list * class -> proof) -> string -> sort list -> term list -> term ->
- (serial * proof_body future) list -> proof_body -> pthm * proof
+ (string * class list list * class -> proof) -> string * Position.T -> sort list ->
+ term list -> term -> (serial * proof_body future) list -> proof_body -> pthm * proof
val unconstrain_thm_proof: theory -> (class * class -> proof) ->
(string * class list list * class -> proof) -> sort list -> term ->
(serial * proof_body future) list -> proof_body -> pthm * proof
@@ -181,7 +181,7 @@
type proof_serial = int;
type thm_header =
- {serial: proof_serial, name: string, prop: term, types: typ list option};
+ {serial: proof_serial, pos: Position.T, name: string, prop: term, types: typ list option};
datatype proof =
MinProof
@@ -213,8 +213,8 @@
fun map_proof_of f (PBody {oracles, thms, proof}) =
PBody {oracles = oracles, thms = thms, proof = f proof};
-fun thm_header serial name prop types : thm_header =
- {serial = serial, name = name, prop = prop, types = types};
+fun thm_header serial pos name prop types : thm_header =
+ {serial = serial, pos = pos, name = name, prop = prop, types = types};
fun thm_body open_proof body =
Thm_Body {open_proof = open_proof, body = body};
@@ -369,9 +369,10 @@
fn PAxm (a, b, c) => ([a], pair term (option (list typ)) (b, c)),
fn OfClass (a, b) => ([b], typ a),
fn Oracle (a, b, c) => ([a], pair term (option (list typ)) (b, c)),
- fn PThm ({serial, name, prop, types}, Thm_Body {open_proof, body}) =>
- ([int_atom serial, name], triple term (option (list typ)) proof_body
- (prop, types, map_proof_of open_proof (Future.join body)))]
+ fn PThm ({serial, pos, name, prop, types}, Thm_Body {open_proof, body}) =>
+ ([int_atom serial, name],
+ pair properties (pair term (pair (option (list typ)) proof_body))
+ (Position.properties_of pos, (prop, (types, map_proof_of open_proof (Future.join body)))))]
and proof_body (PBody {oracles, thms, proof = prf}) =
triple (list (pair string term)) (list pthm) proof (oracles, thms, prf)
and pthm (a, thm_node) =
@@ -404,8 +405,8 @@
fn ([b], a) => OfClass (typ a, b),
fn ([a], b) => let val (c, d) = pair term (option (list typ)) b in Oracle (a, c, d) end,
fn ([a, b], c) =>
- let val (d, e, f) = triple term (option (list typ)) proof_body c
- in PThm (thm_header (int_atom a) b d e, thm_body I (Future.value f)) end]
+ let val ((d, (e, (f, g)))) = pair properties (pair term (pair (option (list typ)) proof_body)) c
+ in PThm (thm_header (int_atom a) (Position.of_properties d) b e f, thm_body I (Future.value g)) end]
and proof_body x =
let val (a, b, c) = triple (list (pair string term)) (list pthm) proof x
in PBody {oracles = a, thms = b, proof = c} end
@@ -479,8 +480,8 @@
| proof (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (typs Ts))
| proof (OfClass T_c) = ofclass T_c
| proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts))
- | proof (PThm ({serial, name, prop, types = SOME Ts}, thm_body)) =
- PThm (thm_header serial name prop (SOME (typs Ts)), thm_body)
+ | proof (PThm ({serial, pos, name, prop, types = SOME Ts}, thm_body)) =
+ PThm (thm_header serial pos name prop (SOME (typs Ts)), thm_body)
| proof _ = raise Same.SAME;
in proof end;
@@ -519,8 +520,8 @@
fun change_types types (PAxm (name, prop, _)) = PAxm (name, prop, types)
| change_types (SOME [T]) (OfClass (_, c)) = OfClass (T, c)
| change_types types (Oracle (name, prop, _)) = Oracle (name, prop, types)
- | change_types types (PThm ({serial, name, prop, ...}, thm_body)) =
- PThm (thm_header serial name prop types, thm_body)
+ | change_types types (PThm ({serial, pos, name, prop, types = _}, thm_body)) =
+ PThm (thm_header serial pos name prop types, thm_body)
| change_types _ prf = prf;
@@ -667,8 +668,8 @@
OfClass (htypeT Envir.norm_type_same T, c)
| norm (Oracle (s, prop, Ts)) =
Oracle (s, prop, Same.map_option (htypeTs Envir.norm_types_same) Ts)
- | norm (PThm ({serial = i, name = a, prop = t, types = Ts}, thm_body)) =
- PThm (thm_header i a t (Same.map_option (htypeTs Envir.norm_types_same) Ts), thm_body)
+ | norm (PThm ({serial = i, pos = p, name = a, prop = t, types = Ts}, thm_body)) =
+ PThm (thm_header i p a t (Same.map_option (htypeTs Envir.norm_types_same) Ts), thm_body)
| norm _ = raise Same.SAME;
in Same.commit norm end;
@@ -992,8 +993,8 @@
OfClass (Logic.incr_tvar_same inc T, c)
| lift' _ _ (Oracle (s, prop, Ts)) =
Oracle (s, prop, (Same.map_option o Same.map) (Logic.incr_tvar_same inc) Ts)
- | lift' _ _ (PThm ({serial = i, name = s, prop, types = Ts}, thm_body)) =
- PThm (thm_header i s prop ((Same.map_option o Same.map) (Logic.incr_tvar inc) Ts),
+ | lift' _ _ (PThm ({serial = i, pos = p, name = s, prop, types = Ts}, thm_body)) =
+ PThm (thm_header i p s prop ((Same.map_option o Same.map) (Logic.incr_tvar inc) Ts),
thm_body)
| lift' _ _ _ = raise Same.SAME
and lifth' Us Ts prf = (lift' Us Ts prf handle Same.SAME => prf);
@@ -1423,8 +1424,8 @@
| subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Same.map_option substTs Ts)
| subst _ _ (OfClass (T, c)) = OfClass (substT T, c)
| subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Same.map_option substTs Ts)
- | subst _ _ (PThm ({serial = i, name = id, prop, types}, thm_body)) =
- PThm (thm_header i id prop (Same.map_option substTs types), thm_body)
+ | subst _ _ (PThm ({serial = i, pos = p, name = id, prop, types}, thm_body)) =
+ PThm (thm_header i p id prop (Same.map_option substTs types), thm_body)
| subst _ _ _ = raise Same.SAME;
in fn t => subst 0 0 t handle Same.SAME => t end;
@@ -2038,7 +2039,7 @@
else proof;
fun prepare_thm_proof unconstrain thy classrel_proof arity_proof
- name shyps hyps concl promises body =
+ (name, pos) shyps hyps concl promises body =
let
val named = name <> "";
@@ -2067,7 +2068,7 @@
val (i, body') =
(*non-deterministic, depends on unknown promises*)
(case strip_combt (fst (strip_combP prf)) of
- (PThm ({serial = i, name = a, prop = prop', types = NONE}, thm_body'), args') =>
+ (PThm ({serial = i, name = a, prop = prop', types = NONE, ...}, thm_body'), args') =>
if (a = "" orelse a = name) andalso prop' = prop1 andalso args' = args then
let val Thm_Body {body = body', ...} = thm_body';
in (i, body' |> (a = "" andalso named) ? Future.map (publish i)) end
@@ -2076,7 +2077,7 @@
val pthm = (i, make_thm_node name prop1 body');
- val head = PThm (thm_header i name prop1 NONE, thm_body open_proof body');
+ val head = PThm (thm_header i pos name prop1 NONE, thm_body open_proof body');
val proof =
if unconstrain then
proof_combt' (head, (map o Option.map o Term.map_types) (#map_atyps ucontext) args)
@@ -2090,7 +2091,8 @@
val thm_proof = prepare_thm_proof false;
fun unconstrain_thm_proof thy classrel_proof arity_proof shyps concl promises body =
- prepare_thm_proof true thy classrel_proof arity_proof "" shyps [] concl promises body;
+ prepare_thm_proof true thy classrel_proof arity_proof ("", Position.none)
+ shyps [] concl promises body;
end;
--- a/src/Pure/thm.ML Fri Aug 09 15:58:26 2019 +0200
+++ b/src/Pure/thm.ML Fri Aug 09 17:14:49 2019 +0200
@@ -106,8 +106,8 @@
val future: thm future -> cterm -> thm
val derivation_closed: thm -> bool
val derivation_name: thm -> string
- val name_derivation: string -> thm -> thm
- val close_derivation: thm -> thm
+ val name_derivation: string * Position.T -> thm -> thm
+ val close_derivation: Position.T -> thm -> thm
val trim_context: thm -> thm
val axiom: theory -> string -> thm
val axioms_of: theory -> (string * thm) list
@@ -1000,7 +1000,7 @@
fun derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
Proofterm.get_name shyps hyps prop (Proofterm.proof_of body);
-fun name_derivation name =
+fun name_derivation name_pos =
solve_constraints #> (fn thm as Thm (der, args) =>
let
val thy = theory_of_thm thm;
@@ -1013,13 +1013,14 @@
val ps = map (apsnd (Future.map fulfill_body)) promises;
val (pthm, proof) =
- Proofterm.thm_proof thy (classrel_proof thy) (arity_proof thy) name shyps hyps prop ps body;
+ Proofterm.thm_proof thy (classrel_proof thy) (arity_proof thy)
+ name_pos shyps hyps prop ps body;
val der' = make_deriv [] [] [pthm] proof;
in Thm (der', args) end);
-val close_derivation =
+fun close_derivation pos =
solve_constraints #> (fn thm =>
- if derivation_closed thm then thm else name_derivation "" thm);
+ if derivation_closed thm then thm else name_derivation ("", pos) thm);
val trim_context = solve_constraints #> trim_context_thm;
@@ -1688,7 +1689,8 @@
val ps = map (apsnd (Future.map fulfill_body)) promises;
val (pthm, proof) =
- Proofterm.unconstrain_thm_proof thy (classrel_proof thy) (arity_proof thy) shyps prop ps body;
+ Proofterm.unconstrain_thm_proof thy (classrel_proof thy) (arity_proof thy)
+ shyps prop ps body;
val der' = make_deriv [] [] [pthm] proof;
val prop' = Proofterm.thm_node_prop (#2 pthm);
in
@@ -2207,7 +2209,7 @@
|> (map_classrels o Symreltab.update) ((c1, c2),
(the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2))
|> standard_tvars
- |> close_derivation
+ |> close_derivation \<^here>
|> trim_context));
val proven = is_classrel thy1;
@@ -2240,7 +2242,7 @@
val th1 =
(th RS the_classrel thy (c, c1))
|> standard_tvars
- |> close_derivation
+ |> close_derivation \<^here>
|> trim_context;
in SOME ((t, Ss, c1), (th1, thy_name, ser)) end);
val finished' = finished andalso null completions;