--- a/src/HOL/Tools/BNF/bnf_def.ML Tue Oct 06 11:50:23 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Tue Oct 06 12:01:07 2015 +0200
@@ -1420,14 +1420,7 @@
val in_rel = Lazy.lazy mk_in_rel;
fun mk_rel_flip () =
- let
- val rel_conversep_thm = Lazy.force rel_conversep;
- val cts = map (SOME o Thm.cterm_of lthy) Rs;
- val rel_conversep_thm' = infer_instantiate' lthy cts rel_conversep_thm;
- in
- unfold_thms lthy @{thms conversep_iff} (rel_conversep_thm' RS @{thm predicate2_eqD})
- |> singleton (Proof_Context.export names_lthy pre_names_lthy)
- end;
+ unfold_thms lthy @{thms conversep_iff} (Lazy.force rel_conversep RS @{thm predicate2_eqD});
val rel_flip = Lazy.lazy mk_rel_flip;
@@ -1469,11 +1462,11 @@
val eq = mk_Trueprop_eq (Term.list_comb (rel, Rs) $ x $ y,
Term.list_comb (rel, Rs_copy) $ x_copy $ y_copy);
in
- Goal.prove_sorry lthy [] (prem0 :: prem1 :: prems) eq
+ fold (Variable.add_free_names lthy) (eq :: prem0 :: prem1 :: prems) []
+ |> (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))
+ mk_rel_cong_tac ctxt (chop 2 prems) (Lazy.force rel_mono_strong)))
|> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val rel_cong = Lazy.lazy (mk_rel_cong Logic.mk_implies);
@@ -1524,13 +1517,13 @@
val Rs = map2 retype_const_or_free self_pred2RTs Rs;
val prems = map (HOLogic.mk_Trueprop o mk_prop) Rs;
val goal = HOLogic.mk_Trueprop (mk_prop (Term.list_comb (relAsAs, Rs)));
+ val vars = fold (Variable.add_free_names lthy) (goal :: prems) [];
in
- Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, goal))
+ Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, goal))
(fn {context = ctxt, prems = _} =>
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))
- |> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation
end;
@@ -1567,12 +1560,12 @@
(mk_rel_fun (Term.list_comb (mk_bnf_rel pred2RTsBsEs CB' CE', S_BsEs)) iff);
val goal =
HOLogic.mk_Trueprop (fold_rev mk_rel_fun prem_rels prem_elems $ rel $ relCsEs);
+ val vars = Variable.add_free_names lthy goal [];
in
- Goal.prove_sorry lthy [] [] goal
+ Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} =>
mk_rel_transfer_tac ctxt (Lazy.force in_rel) (Lazy.force rel_map)
(Lazy.force rel_mono_strong))
- |> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation
end;
@@ -1587,12 +1580,16 @@
in
if null goals then []
else
- Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
- (fn {context = ctxt, prems = _} =>
- mk_set_transfer_tac ctxt (Lazy.force in_rel) (map Lazy.force set_map))
- |> Thm.close_derivation
- |> Conjunction.elim_balanced (length goals)
- |> Proof_Context.export names_lthy lthy
+ let
+ val goal = Logic.mk_conjunction_balanced goals;
+ val vars = Variable.add_free_names lthy goal [];
+ in
+ 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
+ |> Conjunction.elim_balanced (length goals)
+ end
end;
val set_transfer = Lazy.lazy mk_set_transfer;
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Oct 06 11:50:23 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Oct 06 12:01:07 2015 +0200
@@ -142,7 +142,7 @@
thm -> thm list -> thm list -> thm list -> BNF_Def.bnf list -> typ list -> typ list ->
typ list -> typ list list list -> int list list -> int list list -> int list -> thm list ->
thm list -> (thm -> thm) -> thm list list -> Ctr_Sugar.ctr_sugar list -> term list ->
- thm list -> (thm list -> thm list) -> Proof.context -> gfp_sugar_thms
+ thm list -> Proof.context -> gfp_sugar_thms
val co_datatypes: BNF_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
@@ -685,13 +685,16 @@
map2 (fn thm => fn 0 => thm RS @{thm eq_True[THEN iffD2]} | _ => thm) rel_inject_thms ms;
val ctr_transfer_thms =
- let val goals = map2 (mk_parametricity_goal names_lthy Rs) ctrAs ctrBs in
- Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
+ let
+ val goals = map2 (mk_parametricity_goal names_lthy Rs) ctrAs ctrBs;
+ val goal = Logic.mk_conjunction_balanced goals;
+ val vars = Variable.add_free_names lthy goal [];
+ in
+ 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
|> Conjunction.elim_balanced (length goals)
- |> Proof_Context.export names_lthy lthy
end;
val (set_cases_thms, set_cases_attrss) =
@@ -741,10 +744,10 @@
end) args)
end) ctrAs;
val goal = Logic.mk_implies (mk_Trueprop_mem (elem, set $ ta), thesis);
+ val vars = Variable.add_free_names lthy goal [];
val thm =
- Goal.prove_sorry lthy [] (flat premss) goal (fn {context = ctxt, prems} =>
+ 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)
- |> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation
|> rotate_prems ~1;
@@ -779,7 +782,7 @@
end) (map (mk_set innerTs) (sets_of_bnf bnf)) ctxt))
| T => (if T = A then [mk_Trueprop_mem (t, setA $ ctr_args)] else [], ctxt));
- val (goalssss, names_lthy) =
+ val (goalssss, _) =
fold_map (fn set =>
let val A = HOLogic.dest_setT (range_type (fastype_of set)) in
fold_map (fn ctr => fn ctxt =>
@@ -792,11 +795,15 @@
`(fst o unflattt goalssss)
(if null goals then []
else
- Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
- (fn {context = ctxt, prems = _} => mk_set_intros_tac ctxt set0_thms)
- |> Thm.close_derivation
- |> Conjunction.elim_balanced (length goals)
- |> Proof_Context.export names_lthy lthy)
+ let
+ val goal = Logic.mk_conjunction_balanced goals;
+ val vars = Variable.add_free_names lthy goal [];
+ in
+ Goal.prove_sorry lthy vars [] goal
+ (fn {context = ctxt, prems = _} => mk_set_intros_tac ctxt set0_thms)
+ |> Thm.close_derivation
+ |> Conjunction.elim_balanced (length goals)
+ end)
end;
val rel_sel_thms =
@@ -820,10 +827,10 @@
| conjuncts => Library.foldr1 HOLogic.mk_conj conjuncts))];
fun prove goal =
- Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
+ Variable.add_free_names lthy goal []
+ |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
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)
- |> singleton (Proof_Context.export names_lthy lthy)
+ (flat sel_thmss) rel_inject_thms distincts rel_distinct_thms live_nesting_rel_eqs))
|> Thm.close_derivation;
in
map prove goals
@@ -851,13 +858,13 @@
names_ctxt)
end;
- val (assms, names_lthy) = @{fold_map 2} mk_assms ctrAs ctrBs names_lthy;
+ val (assms, _) = @{fold_map 2} mk_assms ctrAs ctrBs names_lthy;
val goal = Logic.list_implies (HOLogic.mk_Trueprop rel_Rs_a_b :: assms, thesis);
+ val vars = Variable.add_free_names lthy goal [];
val thm =
- Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
+ Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
mk_rel_cases_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;
val ctr_names = quasi_unambiguous_case_names (map name_of_ctr ctrAs);
@@ -870,14 +877,14 @@
val case_transfer_thm =
let
- val (S, names_lthy) = yield_singleton (mk_Frees "S") (mk_pred2T C E) names_lthy;
+ val (S, _) = yield_singleton (mk_Frees "S") (mk_pred2T C E) names_lthy;
val caseA = mk_case As C casex;
val caseB = mk_case Bs E casex;
val goal = mk_parametricity_goal names_lthy (S :: Rs) caseA caseB;
+ val vars = Variable.add_free_names lthy goal [];
in
- Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
+ Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
mk_case_transfer_tac ctxt rel_cases_thm case_thms)
- |> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation
end;
@@ -890,12 +897,16 @@
in
if null goals then []
else
- Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
- (fn {context = ctxt, prems = _} =>
- mk_sel_transfer_tac ctxt n sel_defs case_transfer_thm)
- |> Thm.close_derivation
- |> Conjunction.elim_balanced (length goals)
- |> Proof_Context.export names_lthy lthy
+ let
+ val goal = Logic.mk_conjunction_balanced goals;
+ val vars = Variable.add_free_names lthy goal [];
+ in
+ Goal.prove_sorry lthy vars [] goal
+ (fn {context = ctxt, prems = _} =>
+ mk_sel_transfer_tac ctxt n sel_defs case_transfer_thm)
+ |> Thm.close_derivation
+ |> Conjunction.elim_balanced (length goals)
+ end
end;
val disc_transfer_thms =
@@ -903,12 +914,16 @@
if null goals then
[]
else
- Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
- (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
- |> Conjunction.elim_balanced (length goals)
- |> Proof_Context.export names_lthy lthy
+ let
+ val goal = Logic.mk_conjunction_balanced goals;
+ val vars = Variable.add_free_names lthy goal [];
+ in
+ Goal.prove_sorry lthy vars [] goal
+ (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
+ |> Conjunction.elim_balanced (length goals)
+ end
end;
val map_disc_iff_thms =
@@ -927,12 +942,16 @@
if null goals then
[]
else
- Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
- (fn {context = ctxt, prems = _} =>
- mk_map_disc_iff_tac ctxt (Thm.cterm_of ctxt ta) exhaust (flat disc_thmss) map_thms)
- |> Thm.close_derivation
- |> Conjunction.elim_balanced (length goals)
- |> Proof_Context.export names_lthy lthy
+ let
+ val goal = Logic.mk_conjunction_balanced goals;
+ val vars = Variable.add_free_names lthy goal [];
+ in
+ Goal.prove_sorry lthy vars [] goal
+ (fn {context = ctxt, prems = _} =>
+ mk_map_disc_iff_tac ctxt (Thm.cterm_of ctxt ta) exhaust (flat disc_thmss) map_thms)
+ |> Thm.close_derivation
+ |> Conjunction.elim_balanced (length goals)
+ end
end;
val (map_sel_thmss, map_sel_thms) =
@@ -960,14 +979,18 @@
in
`(fst o unflat goalss)
(if null goals then []
- else
- Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
- (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
- |> Conjunction.elim_balanced (length goals)
- |> Proof_Context.export names_lthy lthy)
+ else
+ let
+ val goal = Logic.mk_conjunction_balanced goals;
+ val vars = Variable.add_free_names lthy goal [];
+ in
+ Goal.prove_sorry lthy vars [] goal
+ (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
+ |> Conjunction.elim_balanced (length goals)
+ end)
end;
val (set_sel_thmssss, set_sel_thms) =
@@ -1012,21 +1035,25 @@
([], ctxt)
end;
- val (goalssss, names_lthy) =
+ val (goalssss, _) =
fold_map (fn set => @{fold_map 2} (fold_map o mk_goal set) discAs selAss)
setAs names_lthy;
val goals = flat (flat (flat goalssss));
in
`(fst o unflattt goalssss)
(if null goals then []
- else
- Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
- (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
- |> Conjunction.elim_balanced (length goals)
- |> Proof_Context.export names_lthy lthy)
+ else
+ let
+ val goal = Logic.mk_conjunction_balanced goals;
+ val vars = Variable.add_free_names lthy goal [];
+ in
+ Goal.prove_sorry lthy vars [] goal
+ (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
+ |> Conjunction.elim_balanced (length goals)
+ end)
end;
val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
@@ -1309,12 +1336,12 @@
val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq
(map2 (build_the_rel [] lthy (Rs @ IRs) []) fpA_Ts fpB_Ts) IRs));
+ val vars = Variable.add_free_names lthy goal [];
val rel_induct0_thm =
- Goal.prove_sorry lthy [] prems goal (fn {context = ctxt, prems} =>
+ Goal.prove_sorry lthy 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)
- |> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation;
in
(postproc_co_induct lthy (length fpA_Ts) @{thm predicate2D} @{thm predicate2D_conj}
@@ -1407,16 +1434,17 @@
val goal =
Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss,
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry (op $)) ps us)));
+ val vars = Variable.add_free_names lthy goal [];
val kksss = map (map (map (fst o snd) o #2)) raw_premss;
val ctor_induct' = ctor_induct OF (map2 mk_absumprodE fp_type_definitions mss);
val thm =
- Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
+ Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} =>
mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' fp_abs_inverses
abs_inverses fp_nesting_set_maps pre_set_defss)
- |> singleton (Proof_Context.export names_lthy lthy);
+ |> Thm.close_derivation;
in
`(conj_dests nn) thm
end;
@@ -1515,7 +1543,7 @@
val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
val fpB_Ts = map B_ify_T fpA_Ts;
- val (Rs, IRs, fpAs, fpBs, names_lthy) =
+ val (Rs, IRs, fpAs, fpBs, _) =
let
val fp_names = map base_name_of_typ fpA_Ts;
val ((((Rs, IRs), fpAs_names), fpBs_names), names_lthy) = lthy
@@ -1567,14 +1595,14 @@
val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq
IRs (map2 (build_the_rel [] lthy (Rs @ IRs) []) fpA_Ts fpB_Ts)));
+ val vars = Variable.add_free_names lthy goal [];
val rel_coinduct0_thm =
- Goal.prove_sorry lthy [] prems goal (fn {context = ctxt, prems} =>
+ Goal.prove_sorry lthy vars prems goal (fn {context = ctxt, prems} =>
mk_rel_coinduct0_tac ctxt dtor_rel_coinduct (map (Thm.cterm_of ctxt) IRs) prems
(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)
- |> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation;
in
(postproc_co_induct lthy (length fpA_Ts) @{thm predicate2D} @{thm predicate2D_conj}
@@ -1651,12 +1679,12 @@
|>> apfst (apsnd (Library.foldr1 HOLogic.mk_conj))
|>> apsnd flat;
+ val vars = fold (Variable.add_free_names lthy) (concl :: prems) [];
val thm =
- Goal.prove_sorry lthy [] prems (HOLogic.mk_Trueprop concl)
+ Goal.prove_sorry lthy vars prems (HOLogic.mk_Trueprop concl)
(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)
- |> singleton (Proof_Context.export ctxt'' ctxt)
|> Thm.close_derivation;
val case_names_attr =
@@ -1694,7 +1722,7 @@
fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, (((pgss, _, _, _), cqgsss), _))
dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss
kss mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list)
- corecs corec_defs export_args lthy =
+ corecs corec_defs lthy =
let
fun mk_ctor_dtor_corec_thm dtor_inject dtor_ctor corec =
iffD1 OF [dtor_inject, trans OF [corec, dtor_ctor RS sym]];
@@ -1719,7 +1747,7 @@
val discIss = map #discIs ctr_sugars;
val sel_thmsss = map #sel_thmss ctr_sugars;
- val (((rs, us'), vs'), names_lthy) =
+ val (((rs, us'), vs'), _) =
lthy
|> mk_Frees "R" (map (fn T => mk_pred2T T T) fpTs)
||>> Variable.variant_fixes fp_b_names
@@ -1775,12 +1803,12 @@
ctrXs_Tsss, concl);
val goals = map mk_goal [rs, strong_rs];
-
- fun prove dtor_coinduct' goal =
- Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
+ val varss = map (fn goal => Variable.add_free_names lthy goal []) goals;
+
+ fun prove dtor_coinduct' goal vars =
+ Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} =>
mk_coinduct_tac ctxt live_nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs
fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss disc_thmsss sel_thmsss)
- |> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation;
val rel_eqs = map rel_eq_of_bnf pre_bnfs;
@@ -1788,7 +1816,7 @@
val dtor_coinducts =
[dtor_coinduct, mk_coinduct_strong_thm dtor_coinduct rel_eqs rel_monos mk_vimage2p lthy]
in
- map2 (postproc_co_induct lthy nn mp mp_conj oo prove) dtor_coinducts goals
+ @{map 3} (postproc_co_induct lthy nn mp mp_conj ooo prove) dtor_coinducts goals varss
end;
fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
@@ -1855,9 +1883,8 @@
val tacss = @{map 3} (map oo mk_corec_disc_iff_tac) case_splitss' corec_thmss disc_thmsss;
fun prove goal tac =
- Goal.prove_sorry lthy [] [] goal (tac o #context)
- |> singleton export_args
- |> singleton (Proof_Context.export names_lthy lthy)
+ Variable.add_free_names lthy goal []
+ |> (fn vars => Goal.prove_sorry lthy vars [] goal (tac o #context))
|> Thm.close_derivation;
fun proves [_] [_] = []
@@ -1923,7 +1950,7 @@
val set_boss = map (map fst o type_args_named_constrained_of_spec) specs;
val set_bss = map (map (the_default Binding.empty)) set_boss;
- val ((((Bs0, Cs), Es), Xs), names_no_defs_lthy) =
+ val ((((Bs0, Cs), Es), Xs), _) =
no_defs_lthy
|> fold (Variable.declare_typ o resort_tfree_or_tvar dummyS) unsorted_As
|> mk_TFrees num_As
@@ -2170,17 +2197,16 @@
val goal =
fold_rev Logic.all [w, u]
(mk_Trueprop_eq (HOLogic.mk_eq (u, ctor $ w), HOLogic.mk_eq (dtor $ u, w)));
+ val vars = Variable.add_free_names lthy goal [];
in
- Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
+ Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} =>
mk_ctor_iff_dtor_tac ctxt (map (SOME o Thm.ctyp_of lthy) [ctr_absT, fpT])
(Thm.cterm_of lthy ctor) (Thm.cterm_of lthy dtor) ctor_dtor dtor_ctor)
- |> Morphism.thm phi
|> Thm.close_derivation
end;
val sumEN_thm' =
- unfold_thms lthy @{thms unit_all_eq1} (mk_absumprodE type_definition ms)
- |> Morphism.thm phi;
+ unfold_thms lthy @{thms unit_all_eq1} (mk_absumprodE type_definition ms);
in
mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor_thm sumEN_thm'
end;
@@ -2261,14 +2287,17 @@
end;
fun derive_rec_transfer_thms lthy recs rec_defs (SOME (_, _, _, xsssss)) =
- let val (Rs, Ss, goals, names_lthy) = mk_co_rec_transfer_goals lthy recs in
- Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
+ let
+ val (Rs, Ss, goals, _) = mk_co_rec_transfer_goals lthy recs;
+ val goal = Logic.mk_conjunction_balanced goals;
+ val vars = Variable.add_free_names lthy goal [];
+ in
+ Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} =>
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
|> Conjunction.elim_balanced nn
- |> Proof_Context.export names_lthy lthy
end;
fun derive_rec_o_map_thmss lthy recs rec_defs =
@@ -2410,17 +2439,18 @@
fun derive_corec_transfer_thms lthy corecs corec_defs =
let
- val (Rs, Ss, goals, names_lthy) = mk_co_rec_transfer_goals lthy corecs;
+ val (Rs, Ss, goals, _) = mk_co_rec_transfer_goals lthy corecs;
val (_, _, _, (((pgss, pss, qssss, gssss), _), _)) = the corecs_args_types;
+ val goal = Logic.mk_conjunction_balanced goals;
+ val vars = Variable.add_free_names lthy goal [];
in
- Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
+ Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} =>
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
|> Conjunction.elim_balanced (length goals)
- |> Proof_Context.export names_lthy lthy
end;
fun derive_map_o_corec_thmss lthy0 lthy2 corecs corec_defs =
@@ -2495,8 +2525,7 @@
(corec_disc_iff_thmss, corec_disc_iff_attrs), (corec_sel_thmsss, corec_sel_attrs)) =
derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct
dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss
- ns abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs
- (Proof_Context.export lthy' names_no_defs_lthy) lthy;
+ ns abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs lthy;
fun distinct_prems ctxt thm =
Goal.prove (*no sorry*) ctxt [] []
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Tue Oct 06 11:50:23 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Tue Oct 06 12:01:07 2015 +0200
@@ -159,7 +159,7 @@
val unsortAT = Term.typ_subst_atomic (As ~~ unsorted_As);
val unsorted_fpTs = map unsortAT fpTs;
- val ((Cs, Xs), names_lthy) =
+ val ((Cs, Xs), _) =
no_defs_lthy
|> fold Variable.declare_typ As
|> mk_TFrees nn
@@ -281,15 +281,15 @@
derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types)
xtor_co_induct dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs
ctrXs_Tsss kss mss ns fp_abs_inverses abs_inverses
- (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss ctr_sugars co_recs co_rec_defs
- (Proof_Context.export lthy no_defs_lthy) lthy
+ (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss ctr_sugars co_recs co_rec_defs lthy
|> `(fn ((coinduct_thms_pairs, _), corec_thmss, corec_disc_thmss, _,
(corec_sel_thmsss, _)) =>
(map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, corec_thmss,
corec_disc_thmss, corec_sel_thmsss))
||> (fn info => (NONE, SOME info));
- val phi = Proof_Context.export_morphism names_lthy no_defs_lthy;
+ val names_lthy = lthy |> fold Variable.declare_typ (As @ Cs @ Xs);
+ val phi = Proof_Context.export_morphism names_lthy lthy;
fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec
co_rec_def map_thms co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML Tue Oct 06 11:50:23 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML Tue Oct 06 12:01:07 2015 +0200
@@ -116,18 +116,21 @@
val lfp_rec_sugar_transfer_interpretation = fp_rec_sugar_transfer_interpretation
(fn _ => fn _ => fn f => fn def => fn lthy =>
- let val (goal, names_lthy) = mk_goal lthy f in
- Goal.prove lthy [] [] goal (fn {context = ctxt, prems = _} =>
- mk_lfp_rec_sugar_transfer_tac ctxt def)
- |> singleton (Proof_Context.export names_lthy lthy)
- |> Thm.close_derivation
- end);
+ let
+ val (goal, _) = mk_goal lthy f;
+ val vars = Variable.add_free_names lthy goal [];
+ in
+ Goal.prove lthy vars [] goal (fn {context = ctxt, prems = _} =>
+ mk_lfp_rec_sugar_transfer_tac ctxt def)
+ |> Thm.close_derivation
+ end);
val gfp_rec_sugar_transfer_interpretation = fp_rec_sugar_transfer_interpretation
(fn kk => fn bnfs => fn f => fn def => fn lthy =>
let
val fp_sugars = map (the o fp_sugar_of_bnf lthy) bnfs;
- val (goal, names_lthy) = mk_goal lthy f;
+ val (goal, _) = mk_goal lthy f;
+ val vars = Variable.add_free_names lthy goal [];
val (disc_eq_cases, case_thms, case_distribs, case_congs) =
bnf_depth_first_traverse lthy (fn bnf =>
(case fp_sugar_of_bnf lthy bnf of
@@ -141,14 +144,13 @@
insert Thm.eq_thm case_cong case_congs0))))
(fastype_of f) ([], [], [], []);
in
- Goal.prove lthy [] [] goal (fn {context = ctxt, prems = _} =>
+ Goal.prove lthy vars [] goal (fn {context = ctxt, prems = _} =>
mk_gfp_rec_sugar_transfer_tac ctxt def
(#co_rec_def (#fp_co_induct_sugar (nth fp_sugars kk)))
(map (#type_definition o #absT_info) fp_sugars)
(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)
- |> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation
end);
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Tue Oct 06 11:50:23 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Tue Oct 06 12:01:07 2015 +0200
@@ -157,8 +157,7 @@
val sum_bdT = fst (dest_relT (fastype_of sum_bd));
val (sum_bdT_params, sum_bdT_params') = `(map TFree) (Term.add_tfreesT sum_bdT []);
- val ((((((((((zs, zs'), Bs), ss), fs), self_fs), all_gs), xFs), yFs), yFs_copy),
- names_lthy) =
+ val ((((((((((zs, zs'), Bs), ss), fs), self_fs), all_gs), xFs), yFs), yFs_copy), _) =
lthy
|> mk_Frees' "b" activeAs
||>> mk_Frees "B" BTs
@@ -214,11 +213,12 @@
(Term.list_comb (mapAsBs, passive_ids @ fs) $ x);
val rhs =
Term.list_comb (mapAsCs, take m all_gs @ map HOLogic.mk_comp (drop m all_gs ~~ fs)) $ x;
+ val goal = mk_Trueprop_eq (lhs, rhs);
+ val vars = Variable.add_free_names lthy goal [];
in
- Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (lhs, rhs))
+ Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => mk_map_comp_id_tac ctxt map_comp0)
|> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val map_comp_id_thms = @{map 5} mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps;
@@ -232,11 +232,11 @@
(mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z))));
val prems = @{map 4} mk_prem (drop m sets) self_fs zs zs';
val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x);
+ val vars = Variable.add_free_names lthy goal [];
in
- Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, goal))
+ 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
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val map_cong0L_thms = @{map 5} mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
@@ -253,10 +253,11 @@
val goals = map2 (fn prem => fn concl => Logic.mk_implies (prem, concl)) prems concls;
in
map (fn goal =>
- Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
- (hyp_subst_tac ctxt THEN' rtac ctxt refl) 1)
- |> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy)) goals
+ 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)
+ goals
end;
val timer = time (timer "Derived simple theorems");
@@ -297,7 +298,7 @@
Term.list_comb (Const (coalg, coalgT), args)
end;
- val((((((zs, zs'), Bs), B's), ss), s's), names_lthy) =
+ val((((((zs, zs'), Bs), B's), ss), s's), _) =
lthy
|> mk_Frees' "b" activeAs
||>> mk_Frees "B" BTs
@@ -322,24 +323,25 @@
Logic.list_implies (coalg_prem :: [prem], concl)) concls) prems conclss;
in
map (fn goals => map (fn goal =>
- Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
- mk_coalg_set_tac ctxt coalg_def)
- |> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy)) goals) goalss
+ 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)
+ goals) goalss
end;
fun mk_tcoalg BTs = mk_coalg (map HOLogic.mk_UNIV BTs);
val tcoalg_thm =
let
- val goal = HOLogic.mk_Trueprop (mk_tcoalg activeAs ss)
+ val goal = HOLogic.mk_Trueprop (mk_tcoalg activeAs ss);
+ val vars = Variable.add_free_names lthy goal [];
in
- Goal.prove_sorry lthy [] [] goal
+ Goal.prove_sorry lthy vars [] goal
(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
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val timer = time (timer "Coalgebra definition & thms");
@@ -386,7 +388,7 @@
end;
val (((((((((((((((zs, z's), Bs), Bs_copy), B's), B''s), ss), sum_ss), s's), s''s), fs),
- fs_copy), gs), RFs), Rs), names_lthy) =
+ fs_copy), gs), RFs), Rs), _) =
lthy
|> mk_Frees "b" activeAs
||>> mk_Frees "b" activeBs
@@ -417,10 +419,10 @@
mk_Trueprop_eq (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ x]), s' $ (f $ x)));
val elim_goals = @{map 6} mk_elim_goal Bs mapsAsBs fs ss s's zs;
fun prove goal =
- Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
- mk_mor_elim_tac ctxt mor_def)
- |> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy);
+ 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;
in
(map prove image_goals, map prove elim_goals)
end;
@@ -431,11 +433,11 @@
let
val prems = map2 (HOLogic.mk_Trueprop oo mk_leq) Bs Bs_copy;
val concl = HOLogic.mk_Trueprop (mk_mor Bs ss Bs_copy ss active_ids);
+ val vars = fold (Variable.add_free_names lthy) (concl :: prems) [];
in
- Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
+ 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
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val mor_id_thm = mor_incl_thm OF (replicate n subset_refl);
@@ -447,12 +449,12 @@
HOLogic.mk_Trueprop (mk_mor B's s's B''s s''s gs)];
val concl =
HOLogic.mk_Trueprop (mk_mor Bs ss B''s s''s (map2 (curry HOLogic.mk_comp) gs fs));
+ val vars = fold (Variable.add_free_names lthy) (concl :: prems) [];
in
- Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
+ 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
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val mor_cong_thm =
@@ -460,11 +462,11 @@
val prems = map HOLogic.mk_Trueprop
(map2 (curry HOLogic.mk_eq) fs_copy fs @ [mk_mor Bs ss B's s's fs])
val concl = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs_copy);
+ val vars = fold (Variable.add_free_names lthy) (concl :: prems) [];
in
- Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
+ 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
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val mor_UNIV_thm =
@@ -474,23 +476,23 @@
HOLogic.mk_comp (s', f));
val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs;
val rhs = Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct mapsAsBs fs ss s's);
+ val vars = fold (Variable.add_free_names lthy) [lhs, rhs] [];
in
- Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (lhs, rhs))
+ 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
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val mor_str_thm =
let
val maps = map2 (fn Ds => fn bnf => Term.list_comb
(mk_map_of_bnf Ds allAs (passiveAs @ FTsAs) bnf, passive_ids @ ss)) Dss bnfs;
+ val goal = HOLogic.mk_Trueprop (mk_mor active_UNIVs ss (map HOLogic.mk_UNIV FTsAs) maps ss);
+ val vars = Variable.add_free_names lthy goal [];
in
- Goal.prove_sorry lthy [] []
- (HOLogic.mk_Trueprop (mk_mor active_UNIVs ss (map HOLogic.mk_UNIV FTsAs) maps ss))
+ Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => mk_mor_str_tac ctxt ks mor_UNIV_thm)
|> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val mor_case_sum_thm =
@@ -498,12 +500,12 @@
val maps = @{map 3} (fn s => fn sum_s => fn mapx =>
mk_case_sum (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ Inls), s), sum_s))
s's sum_ss map_Inls;
+ val goal = HOLogic.mk_Trueprop (mk_mor (map HOLogic.mk_UNIV activeBs) s's sum_UNIVs maps Inls);
+ val vars = Variable.add_free_names lthy goal [];
in
- Goal.prove_sorry lthy [] []
- (HOLogic.mk_Trueprop (mk_mor (map HOLogic.mk_UNIV activeBs) s's sum_UNIVs maps Inls))
+ Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => mk_mor_case_sum_tac ctxt ks mor_UNIV_thm)
|> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val timer = time (timer "Morphism definition & thms");
@@ -555,7 +557,7 @@
end;
val (((((((((((((((((zs, z's), Bs), B's), B''s), ss), s's), s''s), fs), (Rtuple, Rtuple')), Rs),
- Rs_copy), R's), sRs), (idx, idx')), Idx), Ris), names_lthy) =
+ Rs_copy), R's), sRs), (idx, idx')), Idx), Ris), _) =
lthy
|> mk_Frees "b" activeAs
||>> mk_Frees "b" activeBs
@@ -580,11 +582,11 @@
val prems = map HOLogic.mk_Trueprop
(mk_bis Bs ss B's s's Rs :: map2 (curry HOLogic.mk_eq) Rs_copy Rs)
val concl = HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs_copy);
+ val vars = fold (Variable.add_free_names lthy) (concl :: prems) [];
in
- Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
+ 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
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val bis_rel_thm =
@@ -597,22 +599,26 @@
val rhs = HOLogic.mk_conj
(bis_le, Library.foldr1 HOLogic.mk_conj
(@{map 6} mk_conjunct Rs ss s's zs z's relsAsBs))
+ val goal = mk_Trueprop_eq (mk_bis Bs ss B's s's Rs, rhs);
+ val vars = Variable.add_free_names lthy goal [];
in
- Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (mk_bis Bs ss B's s's Rs, rhs))
+ 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
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val bis_converse_thm =
- Goal.prove_sorry lthy [] []
- (Logic.mk_implies (HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs),
- HOLogic.mk_Trueprop (mk_bis B's s's Bs ss (map mk_converse Rs))))
- (fn {context = ctxt, prems = _} => mk_bis_converse_tac ctxt m bis_rel_thm rel_congs
- rel_converseps)
- |> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy);
+ let
+ val goal = Logic.mk_implies (HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs),
+ HOLogic.mk_Trueprop (mk_bis B's s's Bs ss (map mk_converse Rs)));
+ val vars = Variable.add_free_names lthy goal [];
+ in
+ 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
+ end;
val bis_O_thm =
let
@@ -621,23 +627,22 @@
HOLogic.mk_Trueprop (mk_bis B's s's B''s s''s R's)];
val concl =
HOLogic.mk_Trueprop (mk_bis Bs ss B''s s''s (map2 (curry mk_rel_comp) Rs R's));
+ val vars = fold (Variable.add_free_names lthy) (concl :: prems) [];
in
- Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
+ 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
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val bis_Gr_thm =
let
- val concl =
- HOLogic.mk_Trueprop (mk_bis Bs ss B's s's (map2 mk_Gr Bs fs));
+ val concl = HOLogic.mk_Trueprop (mk_bis Bs ss B's s's (map2 mk_Gr Bs fs));
+ val vars = fold (Variable.add_free_names lthy) ([coalg_prem, mor_prem, concl]) [];
in
- Goal.prove_sorry lthy [] [] (Logic.list_implies ([coalg_prem, mor_prem], concl))
+ 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
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val bis_image2_thm = bis_cong_thm OF
@@ -654,11 +659,11 @@
(Term.absfree idx' (mk_bis Bs ss B's s's (map (fn R => R $ idx) Ris))));
val concl =
HOLogic.mk_Trueprop (mk_bis Bs ss B's s's (map (mk_UNION Idx) Ris));
+ val vars = fold (Variable.add_free_names lthy) [prem, concl] [];
in
- Goal.prove_sorry lthy [] [] (Logic.mk_implies (prem, concl))
+ 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
- |> singleton (Proof_Context.export names_lthy lthy)
end;
(* self-bisimulation *)
@@ -702,7 +707,7 @@
Term.list_comb (Const (nth lsbiss (i - 1), lsbisT), args)
end;
- val (((((zs, zs'), Bs), ss), sRs), names_lthy) =
+ val (((((zs, zs'), Bs), ss), sRs), _) =
lthy
|> mk_Frees' "b" activeAs
||>> mk_Frees "B" BTs
@@ -713,11 +718,15 @@
val coalg_prem = HOLogic.mk_Trueprop (mk_coalg Bs ss);
val sbis_lsbis_thm =
- Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (mk_sbis Bs ss (map (mk_lsbis Bs ss) ks)))
- (fn {context = ctxt, prems = _} =>
- mk_sbis_lsbis_tac ctxt lsbis_defs bis_Union_thm bis_cong_thm)
- |> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy);
+ let
+ val goal = HOLogic.mk_Trueprop (mk_sbis Bs ss (map (mk_lsbis Bs ss) ks));
+ val vars = Variable.add_free_names lthy goal [];
+ in
+ 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
+ end;
val lsbis_incl_thms = map (fn i => sbis_lsbis_thm RS
(bis_def RS iffD1 RS conjunct1 RS mk_conjunctN n i)) ks;
@@ -730,10 +739,11 @@
val goals = map2 (fn i => fn R => Logic.mk_implies (sbis_prem, mk_concl i R)) ks sRs;
in
@{map 3} (fn goal => fn i => fn def =>
- Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
- mk_incl_lsbis_tac ctxt n i def)
- |> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy)) goals ks lsbis_defs
+ 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)
+ goals ks lsbis_defs
end;
val equiv_lsbis_thms =
@@ -742,11 +752,11 @@
val goals = map2 (fn i => fn B => Logic.mk_implies (coalg_prem, mk_concl i B)) ks Bs;
in
@{map 3} (fn goal => fn l_incl => fn incl_l =>
- Goal.prove_sorry lthy [] [] goal
+ Variable.add_free_names lthy goal []
+ |> (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
- |> singleton (Proof_Context.export names_lthy lthy))
+ |> Thm.close_derivation))
goals lsbis_incl_thms incl_lsbis_thms
end;
@@ -1131,7 +1141,7 @@
Term.list_comb (Const (nth behs (i - 1), behT), ss)
end;
- val ((((((zs, zs_copy), zs_copy2), ss), (nat, nat')), (kl, kl')), names_lthy) =
+ val ((((((zs, zs_copy), zs_copy2), ss), (nat, nat')), (kl, kl')), _) =
lthy
|> mk_Frees "b" activeAs
||>> mk_Frees "b" activeAs
@@ -1146,14 +1156,14 @@
HOLogic.mk_eq (mk_size kl, nat));
val goal = list_all_free (kl :: zs)
(Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs));
+ val vars = Variable.add_free_names lthy goal [];
val cts = map (SOME o Thm.cterm_of lthy) [Term.absfree nat' goal, nat];
val length_Lev =
- Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
+ 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
- |> singleton (Proof_Context.export names_lthy lthy);
+ |> Thm.close_derivation;
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;
@@ -1163,11 +1173,13 @@
mk_Trueprop_mem (kl, mk_Lev ss (mk_size kl) i $ z));
val goals = map2 mk_goal ks zs;
- val length_Levs' = map2 (fn goal => fn length_Lev =>
- Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
- mk_length_Lev'_tac ctxt length_Lev)
- |> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy)) goals length_Levs;
+ val length_Levs' =
+ map2 (fn goal => fn length_Lev =>
+ 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)
+ goals length_Levs;
in
(length_Levs, length_Levs')
end;
@@ -1182,15 +1194,15 @@
(Library.foldr1 HOLogic.mk_conj (map2 (fn i => fn z =>
Library.foldr1 HOLogic.mk_conj
(map2 (mk_conjunct i z) ks zs_copy)) ks zs));
+ val vars = Variable.add_free_names lthy goal [];
val cTs = [SOME (Thm.ctyp_of lthy sum_sbdT)];
val cts = map (SOME o Thm.cterm_of lthy) [Term.absfree kl' goal, kl];
val rv_last =
- Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
+ 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
- |> singleton (Proof_Context.export names_lthy lthy);
+ |> Thm.close_derivation;
val rv_last' = mk_specN (n + 1) rv_last;
in
@@ -1220,15 +1232,15 @@
val goal = list_all_free (kl :: zs @ zs_copy @ zs_copy2)
(Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs));
+ val vars = Variable.add_free_names lthy goal [];
val cts = map (SOME o Thm.cterm_of lthy) [Term.absfree nat' goal, nat];
val set_Lev =
- Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
+ 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
- |> singleton (Proof_Context.export names_lthy lthy);
+ |> Thm.close_derivation;
val set_Lev' = mk_specN (3 * n + 1) set_Lev;
in
@@ -1260,16 +1272,16 @@
val goal = list_all_free (kl :: k :: zs @ zs_copy)
(Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs));
+ val vars = Variable.add_free_names lthy goal [];
val cts = map (SOME o Thm.cterm_of lthy) [Term.absfree nat' goal, nat];
val set_image_Lev =
- Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
+ Goal.prove_sorry lthy vars [] (HOLogic.mk_Trueprop goal)
(fn {context = ctxt, prems = _} =>
mk_set_image_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss
from_to_sbd_thmss to_sbd_inj_thmss)
- |> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy);
+ |> Thm.close_derivation;
val set_image_Lev' = mk_specN (2 * n + 2) set_image_Lev;
in
@@ -1280,15 +1292,18 @@
end;
val mor_beh_thm =
- Goal.prove_sorry lthy [] []
- (HOLogic.mk_Trueprop (mk_mor active_UNIVs ss carTAs strTAs (map (mk_beh ss) ks)))
- (fn {context = ctxt, prems = _} => mk_mor_beh_tac ctxt m mor_def mor_cong_thm
- beh_defs carT_defs strT_defs isNode_defs
- 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
- |> singleton (Proof_Context.export names_lthy lthy);
+ let
+ val goal = HOLogic.mk_Trueprop (mk_mor active_UNIVs ss carTAs strTAs (map (mk_beh ss) ks));
+ val vars = Variable.add_free_names lthy goal [];
+ in
+ Goal.prove_sorry lthy vars [] goal
+ (fn {context = ctxt, prems = _} => mk_mor_beh_tac ctxt m mor_def mor_cong_thm
+ beh_defs carT_defs strT_defs isNode_defs
+ 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
+ end;
val timer = time (timer "Behavioral morphism");
@@ -1455,7 +1470,7 @@
val unfold_defs = map (fn def =>
mk_unabs_def (n + 1) (Morphism.thm phi def RS meta_eq_to_obj_eq)) unfold_def_frees;
- val ((((ss, TRs), unfold_fs), corec_ss), names_lthy) =
+ val ((((ss, TRs), unfold_fs), corec_ss), _) =
lthy
|> mk_Frees "s" sTs
||>> mk_Frees "r" (map (mk_relT o `I) Ts)
@@ -1466,13 +1481,13 @@
let
val Abs_inverses' = map2 (curry op RS) in_car_final_thms Abs_inverses;
val morEs' = map (fn thm => (thm OF [mor_final_thm, UNIV_I]) RS sym) morE_thms;
+ val goal = HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors (map (mk_unfold Ts ss) ks));
+ val vars = Variable.add_free_names lthy goal [];
in
- Goal.prove_sorry lthy [] []
- (HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors (map (mk_unfold Ts ss) ks)))
+ 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
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val dtor_unfold_thms = map (fn thm => (thm OF [mor_unfold_thm, UNIV_I]) RS sym) morE_thms;
@@ -1481,13 +1496,13 @@
val prem = HOLogic.mk_Trueprop (mk_sbis UNIVs dtors TRs);
val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map2 (fn R => fn T => mk_leq R (Id_const T)) TRs Ts));
+ val vars = fold (Variable.add_free_names lthy) [prem, concl] [];
in
- `split_conj_thm (Goal.prove_sorry lthy [] [] (Logic.mk_implies (prem, concl))
+ `split_conj_thm (Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, concl))
(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
- |> singleton (Proof_Context.export names_lthy lthy))
+ |> Thm.close_derivation)
end;
val (unfold_unique_mor_thms, unfold_unique_mor_thm) =
@@ -1496,15 +1511,15 @@
fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_unfold Ts ss i);
val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map2 mk_fun_eq unfold_fs ks));
+ val vars = fold (Variable.add_free_names lthy) [prem, unique] [];
val bis_thm = tcoalg_thm RSN (2, tcoalg_thm RS bis_image2_thm);
val mor_thm = mor_comp_thm OF [mor_final_thm, mor_Abs_thm];
- val unique_mor = Goal.prove_sorry lthy [] [] (Logic.mk_implies (prem, unique))
+ 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
- |> singleton (Proof_Context.export names_lthy lthy);
+ |> Thm.close_derivation;
in
`split_conj_thm unique_mor
end;
@@ -1631,7 +1646,7 @@
val corec_defs = map (fn def =>
mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) corec_def_frees;
- val ((((((((zs, Jzs), Jzs_copy), Jzs1), Jzs2), unfold_fs), corec_ss), phis), names_lthy) =
+ val ((((((((zs, Jzs), Jzs_copy), Jzs1), Jzs2), unfold_fs), corec_ss), phis), _) =
lthy
|> mk_Frees "b" activeAs
||>> mk_Frees "z" Ts
@@ -1656,11 +1671,11 @@
val goals = @{map 5} mk_goal ks corec_ss corec_maps_rev dtors zs;
in
@{map 3} (fn goal => fn unfold => fn map_cong0 =>
- Goal.prove_sorry lthy [] [] goal
+ Variable.add_free_names lthy goal []
+ |> (fn vars => Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => mk_corec_tac ctxt m corec_defs unfold map_cong0
- corec_Inl_sum_thms)
- |> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy))
+ corec_Inl_sum_thms))
+ |> Thm.close_derivation)
goals dtor_unfold_thms map_cong0s
end;
@@ -1671,12 +1686,12 @@
fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_corec corec_ss i);
val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map2 mk_fun_eq unfold_fs ks));
+ val vars = fold (Variable.add_free_names lthy) [prem, unique] [];
in
- Goal.prove_sorry lthy [] [] (Logic.mk_implies (prem, unique))
+ Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, unique))
(fn {context = ctxt, prems = _} => mk_corec_unique_mor_tac ctxt corec_defs
corec_Inl_sum_thms unfold_unique_mor_thm)
|> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val map_id0s_o_id =
@@ -1714,11 +1729,11 @@
val dtor_coinduct_goal = Logic.list_implies (rel_prems, concl);
val dtor_coinduct =
- Goal.prove_sorry lthy [] [] dtor_coinduct_goal
+ Variable.add_free_names lthy dtor_coinduct_goal []
+ |> (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
- |> singleton (Proof_Context.export names_lthy lthy);
+ rel_congs))
+ |> Thm.close_derivation;
in
(rev (Term.add_tfrees dtor_coinduct_goal []), dtor_coinduct)
end;
@@ -1767,14 +1782,12 @@
val fTs = map2 (curry op -->) passiveAs passiveBs;
val gTs = map2 (curry op -->) passiveBs passiveCs;
val uTs = map2 (curry op -->) Ts Ts';
- val (((((((nat, nat'), (Jzs, Jzs')), (hrecs, hrecs')), (fs, fs')), fs_copy), gs), _) =
+ val (((((nat, nat'), (Jzs, Jzs')), (hrecs, hrecs')), (fs, fs')), _) =
lthy
|> yield_singleton (apfst (op ~~) oo mk_Frees' "n") HOLogic.natT
||>> mk_Frees' "z" Ts
||>> mk_Frees' "rec" hrecTs
- ||>> mk_Frees' "f" fTs
- ||>> mk_Frees "f" fTs
- ||>> mk_Frees "g" gTs;
+ ||>> mk_Frees' "f" fTs;
val map_FTFT's = map2 (fn Ds =>
mk_map_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
@@ -1910,11 +1923,11 @@
val goals = @{map 4} mk_goal fs_Jmaps map_FTFT's dtors dtor's;
val maps =
@{map 5} (fn goal => fn unfold => fn map_comp => fn map_cong0 => fn map_arg_cong =>
- Goal.prove_sorry lthy [] [] goal
+ Variable.add_free_names lthy goal []
+ |> (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
- |> singleton (Proof_Context.export names_lthy lthy))
+ mk_map_tac ctxt m n map_arg_cong unfold map_comp map_cong0))
+ |> Thm.close_derivation)
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
@@ -1929,12 +1942,12 @@
val goal =
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map2 (curry HOLogic.mk_eq) us fs_Jmaps));
+ val vars = fold (Variable.add_free_names lthy) (goal :: prems) [];
in
- `split_conj_thm (Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, goal))
+ `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
- |> singleton (Proof_Context.export names_lthy lthy))
+ |> Thm.close_derivation)
end;
val Jmap_comp0_thms =
@@ -1943,12 +1956,12 @@
(@{map 3} (fn fmap => fn gmap => fn fgmap =>
HOLogic.mk_eq (HOLogic.mk_comp (gmap, fmap), fgmap))
fs_Jmaps gs_Jmaps fgs_Jmaps))
+ val vars = Variable.add_free_names lthy goal [];
in
- split_conj_thm (Goal.prove_sorry lthy [] [] goal
+ 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
- |> singleton (Proof_Context.export names_lthy lthy))
+ |> Thm.close_derivation)
end;
val timer = time (timer "map functions for the new codatatypes");
@@ -1983,11 +1996,11 @@
map (fn phi => map (SOME o Thm.cterm_of lthy) [Term.absfree nat' phi, nat]) concls;
in
@{map 4} (fn goal => fn cts => fn col_0s => fn col_Sucs =>
- Goal.prove_sorry lthy [] [] goal
+ Variable.add_free_names lthy goal []
+ |> (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
- |> singleton (Proof_Context.export names_lthy lthy))
+ col_Sucs))
+ |> Thm.close_derivation)
goals ctss col_0ss' col_Sucss'
end;
@@ -1999,11 +2012,11 @@
Logic.list_implies (prems, HOLogic.mk_Trueprop concl)) premss concls;
in
map2 (fn goal => fn col_minimal =>
- Goal.prove_sorry lthy [] [] goal
+ Variable.add_free_names lthy goal []
+ |> (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
- |> singleton (Proof_Context.export names_lthy lthy))
+ mk_Jset_minimal_tac ctxt n col_minimal))
+ |> Thm.close_derivation)
goals col_minimal_thms
end;
@@ -2031,21 +2044,21 @@
in
(map2 (fn goals => fn rec_Sucs =>
map2 (fn goal => fn rec_Suc =>
- Goal.prove_sorry lthy [] [] goal
+ Variable.add_free_names lthy goal []
+ |> (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
- |> singleton (Proof_Context.export names_lthy lthy))
+ mk_set_incl_Jset_tac ctxt rec_Suc))
+ |> Thm.close_derivation)
goals rec_Sucs)
set_incl_Jset_goalss col_Sucss,
map2 (fn goalss => fn rec_Sucs =>
map2 (fn k => fn goals =>
map2 (fn goal => fn rec_Suc =>
- Goal.prove_sorry lthy [] [] goal
+ Variable.add_free_names lthy goal []
+ |> (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
- |> singleton (Proof_Context.export names_lthy lthy))
+ mk_set_Jset_incl_Jset_tac ctxt n rec_Suc k))
+ |> Thm.close_derivation)
goals rec_Sucs)
ks goalss)
set_Jset_incl_Jset_goalsss col_Sucss)
@@ -2100,21 +2113,21 @@
(mk_goals (uncurry mk_leq));
val set_le_thmss = map split_conj_thm
(@{map 4} (fn goal => fn Jset_minimal => fn set_Jsets => fn set_Jset_Jsetss =>
- Goal.prove_sorry lthy [] [] goal
+ Variable.add_free_names lthy goal []
+ |> (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
- |> singleton (Proof_Context.export names_lthy lthy))
+ mk_set_le_tac ctxt n Jset_minimal set_Jsets set_Jset_Jsetss))
+ |> Thm.close_derivation)
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));
val set_ge_thmss =
@{map 3} (@{map 3} (fn goal => fn set_incl_Jset => fn set_Jset_incl_Jsets =>
- Goal.prove_sorry lthy [] [] goal
+ Variable.add_free_names lthy goal []
+ |> (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
- |> singleton (Proof_Context.export names_lthy lthy)))
+ mk_set_ge_tac ctxt n set_incl_Jset set_Jset_incl_Jsets))
+ |> Thm.close_derivation))
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
@@ -2143,11 +2156,11 @@
val thms =
@{map 4} (fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
- Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
+ Variable.add_free_names lthy goal []
+ |> (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
- |> singleton (Proof_Context.export names_lthy lthy))
+ dtor_Jmap_thms set_mapss))
+ |> Thm.close_derivation)
goals ctss col_0ss' col_Sucss';
in
map (split_conj_thm o mk_specN n) thms
@@ -2167,11 +2180,11 @@
val thms =
@{map 5} (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
- Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
+ Variable.add_free_names lthy goal []
+ |> (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
- |> singleton (Proof_Context.export names_lthy lthy))
+ mk_col_bd_tac ctxt m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss))
+ |> Thm.close_derivation)
ls goals ctss col_0ss' col_Sucss';
in
map (split_conj_thm o mk_specN n) thms
@@ -2211,14 +2224,14 @@
val goal =
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(@{map 4} mk_map_cong0 Jsetss_by_bnf Jzs fs_Jmaps fs_copy_Jmaps));
+ val vars = Variable.add_free_names lthy goal [];
val thm =
- Goal.prove_sorry lthy [] [] goal
+ Goal.prove_sorry lthy vars [] goal
(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
- |> singleton (Proof_Context.export names_lthy lthy);
+ |> Thm.close_derivation;
in
split_conj_thm thm
end;
@@ -2243,12 +2256,12 @@
@{map 12} (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 =>
fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor =>
fn set_map0s => fn dtor_set_incls => fn dtor_set_set_inclss =>
- Goal.prove_sorry lthy [] [] goal
+ Variable.add_free_names lthy goal []
+ |> (fn vars => Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} =>
mk_dtor_rel_tac ctxt in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets
- dtor_inject dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss)
- |> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy))
+ dtor_inject dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss))
+ |> Thm.close_derivation)
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
@@ -2260,7 +2273,7 @@
val zipFTs = mk_FTs zip_ranTs;
val zipTs = @{map 3} (fn T => fn T' => fn FT => T --> T' --> FT) Ts Ts' zipFTs;
val zip_zTs = mk_Ts passiveABs;
- val (((zips, (abs, abs')), (zip_zs, zip_zs')), names_lthy) =
+ val (((zips, (abs, abs')), (zip_zs, zip_zs')), _) =
names_lthy
|> mk_Frees "zip" zipTs
||>> mk_Frees' "ab" passiveABs
@@ -2323,14 +2336,17 @@
(@{map 3} mk_helper_coind_concl Jz's Jz's_copy coind2_phis));
fun mk_helper_coind_thms fst concl cts =
- Goal.prove_sorry lthy [] [] (Logic.list_implies (helper_prems, concl))
- (fn {context = ctxt, prems = _} =>
- 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
- |> split_conj_thm
- |> Proof_Context.export names_lthy lthy;
+ let
+ val vars = fold (Variable.add_free_names lthy) (concl :: helper_prems) [];
+ in
+ Goal.prove_sorry lthy vars [] (Logic.list_implies (helper_prems, concl))
+ (fn {context = ctxt, prems = _} =>
+ 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
+ |> split_conj_thm
+ end;
val helper_coind1_thms = mk_helper_coind_thms true helper_coind1_concl cts1;
val helper_coind2_thms = mk_helper_coind_thms false helper_coind2_concl cts2;
@@ -2362,13 +2378,13 @@
val helper_ind_thmss = if m = 0 then replicate n [] else
@{map 4} (fn concl => fn j => fn set_induct => fn cts =>
- Goal.prove_sorry lthy [] [] (Logic.list_implies (helper_prems, concl))
+ fold (Variable.add_free_names lthy) (concl :: helper_prems) []
+ |> (fn vars => Goal.prove_sorry lthy vars [] (Logic.list_implies (helper_prems, concl))
(fn {context = ctxt, prems = _} =>
mk_rel_coinduct_ind_tac ctxt m ks
- dtor_unfold_thms set_mapss j (infer_instantiate' ctxt cts set_induct))
+ dtor_unfold_thms set_mapss j (infer_instantiate' ctxt cts set_induct)))
|> Thm.close_derivation
- |> split_conj_thm
- |> Proof_Context.export names_lthy lthy)
+ |> split_conj_thm)
mk_helper_ind_concls ls dtor_Jset_induct_thms ctss
|> transpose;
in
@@ -2387,11 +2403,11 @@
val goals = @{map 3} mk_le_Jrel_OO Jrelpsi1s Jrelpsi2s Jrelpsi12s;
val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals);
+ val vars = Variable.add_free_names lthy goal [];
in
- Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
+ 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
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val timer = time (timer "helpers for BNF properties");
@@ -2507,11 +2523,11 @@
val goals = @{map 5} mk_goal Jsetss_by_range ys ys_copy ys'_copy ls;
in
map2 (fn goal => fn induct =>
- Goal.prove_sorry lthy [] [] goal
+ Variable.add_free_names lthy goal []
+ |> (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
- |> singleton (Proof_Context.export names_lthy lthy))
+ (flat set_mapss) wit_thms))
+ |> Thm.close_derivation)
goals dtor_Jset_induct_thms
|> map split_conj_thm
|> transpose
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Oct 06 11:50:23 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Oct 06 12:01:07 2015 +0200
@@ -1107,7 +1107,7 @@
(ctr, map (K []) sels))) basic_ctr_specss);
val (corec_specs0, _, coinduct_thm, coinduct_strong_thm, coinduct_thms, coinduct_strong_thms,
- (coinduct_attrs, common_coinduct_attrs), n2m, lthy') =
+ (coinduct_attrs, common_coinduct_attrs), n2m, lthy) =
corec_specs_of bs arg_Ts res_Ts frees callssss lthy;
val corec_specs = take actual_nn corec_specs0;
val ctr_specss = map #ctr_specs corec_specs;
@@ -1144,7 +1144,7 @@
val disc_eqnss = @{map 6} mk_actual_disc_eqns bs arg_Tss exhaustives corec_specs sel_eqnss
disc_eqnss0;
val (defs, excludess') =
- build_defs lthy' bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss;
+ build_defs lthy bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss;
val tac_opts =
map (fn {code_rhs_opt, ...} :: _ =>
@@ -1558,7 +1558,7 @@
fun after_qed thmss' = fold_map Local_Theory.define defs #-> prove thmss';
in
- (goalss, after_qed, lthy')
+ (goalss, after_qed, lthy)
end;
fun primcorec_ursive_cmd auto opts (raw_fixes, raw_specs_of) lthy =
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Tue Oct 06 11:50:23 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Tue Oct 06 12:01:07 2015 +0200
@@ -117,7 +117,7 @@
bd0s Dss bnfs;
val witss = map wits_of_bnf bnfs;
- val ((((((((zs, zs'), Bs), ss), fs), self_fs), all_gs), (xFs, xFs')), names_lthy) =
+ val ((((((((zs, zs'), Bs), ss), fs), self_fs), all_gs), (xFs, xFs')), _) =
lthy
|> mk_Frees' "z" activeAs
||>> mk_Frees "B" BTs
@@ -192,11 +192,11 @@
(Term.list_comb (mapAsBs, passive_ids @ fs) $ x);
val rhs = Term.list_comb (mapAsCs,
take m all_gs @ map HOLogic.mk_comp (drop m all_gs ~~ fs)) $ x;
+ val vars = fold (Variable.add_free_names lthy) [lhs, rhs] [];
in
- Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (lhs, rhs))
+ 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
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val map_comp_id_thms = @{map 5} mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps;
@@ -209,11 +209,11 @@
(mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z))));
val prems = @{map 4} mk_prem (drop m sets) self_fs zs zs';
val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x);
+ val vars = fold (Variable.add_free_names lthy) (goal :: prems) [];
in
- Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, goal))
+ 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
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val map_cong0L_thms = @{map 5} mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
@@ -258,7 +258,7 @@
Term.list_comb (Const (alg, algT), args)
end;
- val ((((((((zs, zs'), Bs), B's), ss), s's), fs), (xFs, xFs')), names_lthy) =
+ val ((((((((zs, zs'), Bs), B's), ss), s's), fs), (xFs, xFs')), _) =
lthy
|> mk_Frees' "z" activeAs
||>> mk_Frees "B" BTs
@@ -279,10 +279,10 @@
Logic.list_implies (alg_prem :: prems, concl)) premss concls;
in
map (fn goal =>
- Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
- mk_alg_set_tac ctxt alg_def)
- |> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy))
+ 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)
goals
end;
@@ -297,11 +297,11 @@
map (fn concl => Logic.mk_implies (alg_prem, concl)) concls;
in
map2 (fn goal => fn alg_set =>
- Goal.prove_sorry lthy [] [] goal
+ Variable.add_free_names lthy goal []
+ |> (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
- |> singleton (Proof_Context.export names_lthy lthy))
+ mk_alg_not_empty_tac ctxt alg_set alg_set_thms wit_thms))
+ |> Thm.close_derivation)
goals alg_set_thms
end;
@@ -351,7 +351,7 @@
end;
val ((((((((((((Bs, Bs_copy), B's), B''s), ss), prod_ss), s's), s''s), fs), fs_copy), gs), xFs),
- names_lthy) =
+ _) =
lthy
|> mk_Frees "B" BTs
||>> mk_Frees "B" BTs
@@ -375,10 +375,11 @@
Logic.list_implies ([prem, mk_elim_prem sets x T],
mk_Trueprop_eq (f $ (s $ x), s' $ Term.list_comb (mapAsBs, passive_ids @ fs @ [x])));
val elim_goals = @{map 7} mk_elim_goal setssAs mapsAsBs fs ss s's xFs FTsAs;
- fun prove goal = Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
- mk_mor_elim_tac ctxt mor_def)
- |> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy);
+ fun prove goal =
+ 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;
in
map prove elim_goals
end;
@@ -387,11 +388,11 @@
let
val prems = map2 (HOLogic.mk_Trueprop oo mk_leq) Bs Bs_copy;
val concl = HOLogic.mk_Trueprop (mk_mor Bs ss Bs_copy ss active_ids);
+ val vars = fold (Variable.add_free_names lthy) (concl :: prems) [];
in
- Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
+ 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
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val mor_comp_thm =
@@ -401,11 +402,11 @@
HOLogic.mk_Trueprop (mk_mor B's s's B''s s''s gs)];
val concl =
HOLogic.mk_Trueprop (mk_mor Bs ss B''s s''s (map2 (curry HOLogic.mk_comp) gs fs));
+ val vars = fold (Variable.add_free_names lthy) (concl :: prems) [];
in
- Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
+ 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
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val mor_cong_thm =
@@ -413,24 +414,24 @@
val prems = map HOLogic.mk_Trueprop
(map2 (curry HOLogic.mk_eq) fs_copy fs @ [mk_mor Bs ss B's s's fs])
val concl = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs_copy);
+ val vars = fold (Variable.add_free_names lthy) (concl :: prems) [];
in
- Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
+ 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
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val mor_str_thm =
let
val maps = map2 (fn Ds => fn bnf => Term.list_comb
(mk_map_of_bnf Ds (passiveAs @ FTsAs) allAs bnf, passive_ids @ ss)) Dss bnfs;
+ val goal = HOLogic.mk_Trueprop
+ (mk_mor (map HOLogic.mk_UNIV FTsAs) maps active_UNIVs ss ss);
+ val vars = Variable.add_free_names lthy goal [];
in
- Goal.prove_sorry lthy [] []
- (HOLogic.mk_Trueprop
- (mk_mor (map HOLogic.mk_UNIV FTsAs) maps active_UNIVs ss ss))
+ Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => mk_mor_str_tac ctxt ks mor_def)
|> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val mor_convol_thm =
@@ -438,13 +439,13 @@
val maps = @{map 3} (fn s => fn prod_s => fn mapx =>
mk_convol (HOLogic.mk_comp (s, Term.list_comb (mapx, passive_ids @ fsts)), prod_s))
s's prod_ss map_fsts;
+ val goal = HOLogic.mk_Trueprop
+ (mk_mor prod_UNIVs maps (map HOLogic.mk_UNIV activeBs) s's fsts)
+ val vars = Variable.add_free_names lthy goal [];
in
- Goal.prove_sorry lthy [] []
- (HOLogic.mk_Trueprop
- (mk_mor prod_UNIVs maps (map HOLogic.mk_UNIV activeBs) s's fsts))
+ Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => mk_mor_convol_tac ctxt ks mor_def)
|> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val mor_UNIV_thm =
@@ -454,11 +455,11 @@
HOLogic.mk_comp (s', Term.list_comb (mapAsBs, passive_ids @ fs)));
val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs;
val rhs = Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct mapsAsBs fs ss s's);
+ val vars = fold (Variable.add_free_names lthy) [lhs, rhs] [];
in
- Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (lhs, rhs))
+ 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
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val timer = time (timer "Morphism definition & thms");
@@ -551,7 +552,7 @@
val II_sTs = map2 (fn Ds => fn bnf =>
mk_T_of_bnf Ds (passiveAs @ replicate n Asuc_bdT) bnf --> Asuc_bdT) Dss bnfs;
- val ((((((Bs, ss), idxs), Asi_name), (idx, idx')), (jdx, jdx')), names_lthy) =
+ val ((((((Bs, ss), idxs), Asi_name), (idx, idx')), (jdx, jdx')), _) =
lthy
|> mk_Frees "B" BTs
||>> mk_Frees "s" sTs
@@ -568,11 +569,11 @@
HOLogic.mk_mem (HOLogic.mk_prod (idx, jdx), suc_bd));
val concl = HOLogic.mk_Trueprop (mk_Bex field_suc_bd
(Term.absfree jdx' (Library.foldr1 HOLogic.mk_conj (map mk_conjunct idxs))));
+ val vars = fold (Variable.add_free_names lthy) [prem, concl] [];
in
- Goal.prove_sorry lthy [] [] (Logic.list_implies ([prem], concl))
+ 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
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val timer = time (timer "Bounds");
@@ -609,11 +610,11 @@
(HOLogic.mk_eq (min_algs $ idx, HOLogic.mk_tuple
(@{map 4} (mk_minH_component min_algs idx) setssAs FTsAs ss ks)));
val goal = Logic.mk_implies (HOLogic.mk_Trueprop i_field, concl);
+ val vars = Variable.add_free_names lthy goal [];
- val min_algs_thm = Goal.prove_sorry lthy [] [] goal
+ 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
- |> singleton (Proof_Context.export names_lthy lthy);
+ |> Thm.close_derivation;
val min_algs_thms = map (fn k => min_algs_thm RS mk_nthI n k) ks;
@@ -622,10 +623,10 @@
val monos =
map2 (fn goal => fn min_algs =>
- Goal.prove_sorry lthy [] [] goal
- (fn {context = ctxt, prems = _} => mk_min_algs_mono_tac ctxt min_algs)
- |> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy))
+ 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)
(map mk_mono_goal min_algss) min_algs_thms;
fun mk_card_conjunct min_alg = mk_ordLeq (mk_card_of min_alg) Asuc_bd;
@@ -634,14 +635,17 @@
val card_ct = Thm.cterm_of lthy (Term.absfree idx' card_conjunction);
val card_of =
- Goal.prove_sorry lthy [] []
- (HOLogic.mk_Trueprop (HOLogic.mk_imp (i_field, card_conjunction)))
- (fn {context = ctxt, prems = _} => mk_min_algs_card_of_tac ctxt card_cT card_ct
- 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
- |> singleton (Proof_Context.export names_lthy lthy);
+ let
+ val goal = HOLogic.mk_Trueprop (HOLogic.mk_imp (i_field, card_conjunction));
+ val vars = Variable.add_free_names lthy goal [];
+ in
+ Goal.prove_sorry lthy vars [] goal
+ (fn {context = ctxt, prems = _} => mk_min_algs_card_of_tac ctxt card_cT card_ct
+ 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
+ end;
val least_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
val least_conjunction = Library.foldr1 HOLogic.mk_conj (map2 mk_leq min_algss Bs);
@@ -649,13 +653,16 @@
val least_ct = Thm.cterm_of lthy (Term.absfree idx' least_conjunction);
val least =
- (Goal.prove_sorry lthy [] []
- (Logic.mk_implies (least_prem,
- HOLogic.mk_Trueprop (HOLogic.mk_imp (i_field, least_conjunction))))
- (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
- |> singleton (Proof_Context.export names_lthy lthy);
+ let
+ val goal = Logic.mk_implies (least_prem,
+ HOLogic.mk_Trueprop (HOLogic.mk_imp (i_field, least_conjunction)));
+ val vars = Variable.add_free_names lthy goal [];
+ in
+ 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
+ end;
in
(min_algs_thms, monos, card_of, least)
end;
@@ -698,43 +705,60 @@
val min_algs = map (mk_min_alg ss) ks;
- val ((Bs, ss), names_lthy) =
+ val ((Bs, ss), _) =
lthy
|> mk_Frees "B" BTs
||>> mk_Frees "s" sTs;
val (alg_min_alg_thm, card_of_min_alg_thms, least_min_alg_thms, mor_incl_min_alg_thm) =
let
- val goal = HOLogic.mk_Trueprop (mk_alg min_algs ss);
- val alg_min_alg = Goal.prove_sorry lthy [] [] 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
- |> singleton (Proof_Context.export names_lthy lthy);
+ val alg_min_alg =
+ let
+ val goal = HOLogic.mk_Trueprop (mk_alg min_algs ss);
+ val vars = Variable.add_free_names lthy goal [];
+ in
+ 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
+ end;
- fun mk_card_of_thm min_alg def = Goal.prove_sorry lthy [] []
- (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of min_alg) Asuc_bd))
- (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;
+ fun mk_card_of_thm min_alg def =
+ let
+ val goal = HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of min_alg) Asuc_bd);
+ val vars = Variable.add_free_names lthy goal [];
+ in
+ 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
+ end;
- val least_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
- fun mk_least_thm min_alg B def = Goal.prove_sorry lthy [] []
- (Logic.mk_implies (least_prem, HOLogic.mk_Trueprop (mk_leq min_alg B)))
- (fn {context = ctxt, prems = _} => mk_least_min_alg_tac ctxt def least_min_algs_thm)
- |> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy);
+ fun mk_least_thm min_alg B def =
+ let
+ val prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
+ val goal = Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_leq min_alg B));
+ val vars = Variable.add_free_names lthy goal [];
+ 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
+ end;
val leasts = @{map 3} mk_least_thm min_algs Bs min_alg_defs;
- val incl_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
- val incl = Goal.prove_sorry lthy [] []
- (Logic.mk_implies (incl_prem,
- HOLogic.mk_Trueprop (mk_mor min_algs ss Bs ss active_ids)))
- (fn {context = ctxt, prems = _} =>
- EVERY' (rtac ctxt mor_incl_thm :: map (etac ctxt) leasts) 1)
- |> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy);
+ val incl =
+ let
+ val prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
+ val goal = Logic.mk_implies (prem,
+ HOLogic.mk_Trueprop (mk_mor min_algs ss Bs ss active_ids));
+ val vars = Variable.add_free_names lthy goal [];
+ in
+ Goal.prove_sorry lthy vars [] goal
+ (fn {context = ctxt, prems = _} =>
+ EVERY' (rtac ctxt mor_incl_thm :: map (etac ctxt) leasts) 1)
+ |> Thm.close_derivation
+ end;
in
(alg_min_alg, map2 mk_card_of_thm min_algs min_alg_defs, leasts, incl)
end;
@@ -809,7 +833,7 @@
val car_inits = map (mk_min_alg str_inits) ks;
val (((((((((Bs, ss), Asuc_fs), (iidx, iidx')), init_xs), (init_xFs, init_xFs')), init_fs),
- init_fs_copy), init_phis), names_lthy) =
+ init_fs_copy), init_phis), _) =
lthy
|> mk_Frees "B" BTs
||>> mk_Frees "s" sTs
@@ -838,13 +862,13 @@
val concl = HOLogic.mk_Trueprop
(mk_mor car_inits str_inits active_UNIVs ss
(map (fn f => HOLogic.mk_comp (f, mk_rapp iidx Asuc_bdT)) Asuc_fs));
+ val vars = fold (Variable.add_free_names lthy) (concl :: prems) [];
in
- Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
+ Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
(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
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val init_unique_mor_thms =
@@ -857,12 +881,13 @@
val unique = HOLogic.mk_Trueprop
(Library.foldr1 HOLogic.mk_conj (@{map 3} mk_fun_eq init_fs init_fs_copy init_xs));
val cts = map (Thm.cterm_of lthy) ss;
+ val all_prems = prems @ mor_prems;
+ val vars = fold (Variable.add_free_names lthy) (unique :: all_prems) [];
val unique_mor =
- Goal.prove_sorry lthy [] [] (Logic.list_implies (prems @ mor_prems, unique))
+ 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
- |> singleton (Proof_Context.export names_lthy lthy);
+ |> Thm.close_derivation;
in
split_conj_thm unique_mor
end;
@@ -891,12 +916,12 @@
val prem = HOLogic.mk_Trueprop (mk_closed init_phis);
val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map2 mk_Ball car_inits init_phis));
+ val vars = fold (Variable.add_free_names lthy) [concl, prem] [];
in
- Goal.prove_sorry lthy [] [] (Logic.mk_implies (prem, concl))
+ 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
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val timer = time (timer "Initiality definition & thms");
@@ -1028,7 +1053,7 @@
(* algebra copies *)
- val (((((((Bs, B's), ss), s's), inv_fs), fs), rec_ss), names_lthy) =
+ val (((((((Bs, B's), ss), s's), inv_fs), fs), rec_ss), _) =
lthy
|> mk_Frees "B" BTs
||>> mk_Frees "B'" B'Ts
@@ -1044,25 +1069,25 @@
@{map 3} (HOLogic.mk_Trueprop ooo mk_bij_betw) inv_fs B's Bs;
val concl = HOLogic.mk_Trueprop (list_exists_free s's
(HOLogic.mk_conj (mk_alg B's s's, mk_mor B's s's Bs ss inv_fs)));
+ val vars = fold (Variable.add_free_names lthy) (concl :: prems) [];
in
- Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
+ 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
- |> singleton (Proof_Context.export names_lthy lthy)
+ |> Thm.close_derivation
end;
val init_ex_mor_thm =
let
val goal = HOLogic.mk_Trueprop
(list_exists_free fs (mk_mor UNIVs ctors active_UNIVs ss fs));
+ val vars = Variable.add_free_names lthy goal [];
in
- Goal.prove_sorry lthy [] [] goal
+ Goal.prove_sorry lthy vars [] goal
(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
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val mor_fold_thm =
@@ -1070,13 +1095,13 @@
val mor_cong = mor_cong_thm OF (map (mk_nth_conv n) ks);
val cT = Thm.ctyp_of lthy foldT;
val ct = Thm.cterm_of lthy fold_fun
+ val goal = HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss (map (mk_fold Ts ss) ks));
+ val vars = Variable.add_free_names lthy goal [];
in
- Goal.prove_sorry lthy [] []
- (HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss (map (mk_fold Ts ss) ks)))
+ 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
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val ctor_fold_thms = map (fn morE => rule_by_tactic lthy
@@ -1088,11 +1113,11 @@
val prem = HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss fs);
fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_fold Ts ss i);
val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_fun_eq fs ks));
- val unique_mor = Goal.prove_sorry lthy [] [] (Logic.mk_implies (prem, unique))
+ val vars = fold (Variable.add_free_names lthy) [prem, unique] [];
+ 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
- |> singleton (Proof_Context.export names_lthy lthy);
+ |> Thm.close_derivation;
in
`split_conj_thm unique_mor
end;
@@ -1220,8 +1245,7 @@
val rec_defs = map (fn def =>
mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) rec_def_frees;
- val (((((((((Izs, (Izs1, Izs1'))), (Izs2, Izs2')), xFs), yFs), fs), rec_ss), init_phis),
- names_lthy) =
+ val (((((((((Izs, (Izs1, Izs1'))), (Izs2, Izs2')), xFs), yFs), fs), rec_ss), init_phis), _) =
lthy
|> mk_Frees "z" Ts
||>> mk_Frees' "z1" Ts
@@ -1248,10 +1272,10 @@
val goals = @{map 5} mk_goal ks rec_ss rec_maps_rev ctors xFs;
in
map2 (fn goal => fn foldx =>
- Goal.prove_sorry lthy [] [] goal
- (fn {context = ctxt, prems = _} => mk_rec_tac ctxt rec_defs foldx fst_rec_pair_thms)
- |> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy))
+ Variable.add_free_names lthy goal []
+ |> (fn vars => Goal.prove_sorry lthy vars [] goal
+ (fn {context = ctxt, prems = _} => mk_rec_tac ctxt rec_defs foldx fst_rec_pair_thms))
+ |> Thm.close_derivation)
goals ctor_fold_thms
end;
@@ -1261,12 +1285,12 @@
val prem = HOLogic.mk_Trueprop (mk_mor UNIVs ctors rec_UNIVs (mk_rec_strs rec_ss) id_fs);
fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_rec rec_ss i);
val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_fun_eq fs ks));
+ val vars = fold (Variable.add_free_names lthy) [prem, unique] [];
in
- Goal.prove_sorry lthy [] [] (Logic.mk_implies (prem, unique))
+ Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, unique))
(fn {context = ctxt, prems = _} => mk_rec_unique_mor_tac ctxt rec_defs fst_rec_pair_thms
fold_unique_mor_thm)
|> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val (ctor_rec_unique_thms, ctor_rec_unique_thm) =
@@ -1301,13 +1325,13 @@
val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_concl phis Izs));
val goal = Logic.list_implies (prems, concl);
+ val vars = Variable.add_free_names lthy goal [];
in
- (Goal.prove_sorry lthy [] [] goal
+ (Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} =>
mk_ctor_induct_tac ctxt m set_mapss init_induct_thm morE_thms mor_Abs_thm
Rep_inverses Abs_inverses Reps)
- |> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy),
+ |> Thm.close_derivation,
rev (Term.add_tfrees goal []))
end;
@@ -1345,12 +1369,12 @@
Term.absfree z1' (HOLogic.mk_all (fst z2', snd z2', phi $ z1 $ z2));
val cts = @{map 3} (SOME o Thm.cterm_of lthy ooo mk_t) phi2s (Izs1 ~~ Izs1') (Izs2 ~~ Izs2');
val goal = Logic.list_implies (prems, concl);
+ val vars = Variable.add_free_names lthy goal [];
in
- (Goal.prove_sorry lthy [] [] goal
+ (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
- |> singleton (Proof_Context.export names_lthy lthy),
+ |> Thm.close_derivation,
rev (Term.add_tfrees goal []))
end;
@@ -1510,7 +1534,7 @@
bs map_bs rel_bs set_bss fs_maps setss_by_bnf ctor_witss Ts lthy;
val ((((((((((((((Izs, (Izs1, Izs1')), (Izs2, Izs2')), xFs), yFs))), Iphis), Ipsi1s),
- Ipsi2s), fs), fs_copy), us), (ys, ys')), names_lthy) =
+ Ipsi2s), fs), fs_copy), us), (ys, ys')), _) =
lthy
|> mk_Frees "z" Ts
||>> mk_Frees' "z1" Ts
@@ -1558,11 +1582,11 @@
val goals = @{map 4} mk_goal fs_Imaps map_FTFT's ctors ctor's;
val maps =
@{map 4} (fn goal => fn foldx => fn map_comp_id => fn map_cong0 =>
- Goal.prove_sorry lthy [] [] goal
+ Variable.add_free_names lthy goal []
+ |> (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
- |> singleton (Proof_Context.export names_lthy lthy))
+ mk_map_tac ctxt m n foldx map_comp_id map_cong0))
+ |> Thm.close_derivation)
goals ctor_fold_thms map_comp_id_thms map_cong0s;
in
`(map (fn thm => thm RS @{thm comp_eq_dest})) maps
@@ -1577,11 +1601,11 @@
val goal =
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map2 (curry HOLogic.mk_eq) us fs_Imaps));
- val unique = Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, goal))
+ val vars = fold (Variable.add_free_names lthy) (goal :: prems) [];
+ 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
- |> singleton (Proof_Context.export names_lthy lthy);
+ |> Thm.close_derivation;
in
`split_conj_thm unique
end;
@@ -1613,11 +1637,11 @@
ls Isetss_by_range;
val ctor_setss = @{map 3} (fn i => @{map 3} (fn set_nats => fn goal => fn set =>
- Goal.prove_sorry lthy [] [] goal
+ Variable.add_free_names lthy goal []
+ |> (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
- |> singleton (Proof_Context.export names_lthy lthy))
+ mk_ctor_set_tac ctxt set (nth set_nats (i - 1)) (drop m set_nats)))
+ |> Thm.close_derivation)
set_mapss) ls simp_goalss setss;
in
ctor_setss
@@ -1661,10 +1685,10 @@
fun mk_tac ctxt induct = mk_set_nat_tac ctxt m (rtac ctxt induct) set_mapss ctor_Imap_thms;
val thms =
@{map 5} (fn goal => fn csets => fn ctor_sets => fn induct => fn i =>
- Goal.prove_sorry lthy [] [] goal
- (fn {context = ctxt, prems = _} => mk_tac ctxt induct csets ctor_sets i)
- |> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy))
+ 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)
goals csetss ctor_Iset_thmss inducts ls;
in
map split_conj_thm thms
@@ -1689,11 +1713,11 @@
fun mk_tac ctxt induct = mk_set_bd_tac ctxt m (rtac ctxt induct) sbd0_Cinfinite set_sbd0ss;
val thms =
@{map 4} (fn goal => fn ctor_sets => fn induct => fn i =>
- Goal.prove_sorry lthy [] [] goal
+ Variable.add_free_names lthy goal []
+ |> (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
- |> singleton (Proof_Context.export names_lthy lthy))
+ mk_tac ctxt induct ctor_sets i))
+ |> Thm.close_derivation)
goals ctor_Iset_thmss inducts ls;
in
map split_conj_thm thms
@@ -1719,12 +1743,12 @@
val goal =
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(@{map 4} mk_map_cong0 Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps));
+ val vars = Variable.add_free_names lthy goal [];
- val thm = Goal.prove_sorry lthy [] [] goal
+ 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
- |> singleton (Proof_Context.export names_lthy lthy);
+ |> Thm.close_derivation;
in
split_conj_thm thm
end;
@@ -1754,12 +1778,12 @@
@{map 12} (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 =>
fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor =>
fn set_map0s => fn ctor_set_incls => fn ctor_set_set_inclss =>
- Goal.prove_sorry lthy [] [] goal
+ Variable.add_free_names lthy goal []
+ |> (fn vars => Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} =>
mk_ctor_rel_tac ctxt in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets
- ctor_inject ctor_dtor set_map0s ctor_set_incls ctor_set_set_inclss)
- |> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy))
+ ctor_inject ctor_dtor set_map0s ctor_set_incls ctor_set_set_inclss))
+ |> Thm.close_derivation)
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
@@ -1779,12 +1803,12 @@
val induct = Thm.instantiate' cTs (cphis @ cxs) ctor_induct2_thm;
val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals);
+ val vars = Variable.add_free_names lthy goal [];
in
- Goal.prove_sorry lthy [] [] goal
+ 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
- |> singleton (Proof_Context.export names_lthy lthy)
end;
val timer = time (timer "helpers for BNF properties");
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Oct 06 11:50:23 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Oct 06 12:01:07 2015 +0200
@@ -269,15 +269,15 @@
if exists rhs_is_zero size_thms then []
else
let
- val (xs, names_lthy2) = mk_Frees "x" (binder_types (fastype_of size)) lthy2;
+ val (xs, _) = mk_Frees "x" (binder_types (fastype_of size)) lthy2;
val goal =
HOLogic.mk_Trueprop (BNF_LFP_Util.mk_not_eq (list_comb (size, xs)) HOLogic.zero);
+ val vars = Variable.add_free_names lthy2 goal [];
val thm =
- Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} =>
+ Goal.prove_sorry lthy2 vars [] goal (fn {context = ctxt, ...} =>
mk_size_neq ctxt (map (Thm.cterm_of lthy2) xs)
(#exhaust (#ctr_sugar (#fp_ctr_sugar fp_sugar))) size_thms)
|> single
- |> Proof_Context.export names_lthy2 lthy2
|> map Thm.close_derivation;
in thm end) fp_sugars overloaded_size_consts overloaded_size_simpss
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Tue Oct 06 11:50:23 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Tue Oct 06 12:01:07 2015 +0200
@@ -357,8 +357,8 @@
val n = length card_of_min_algs;
in
EVERY' [Method.insert_tac (map (fn thm => thm RS @{thm ex_bij_betw}) card_of_min_algs),
- REPEAT_DETERM o etac ctxt exE, rtac ctxt rev_mp, rtac ctxt copy,
- REPEAT_DETERM_N n o assume_tac ctxt,
+ REPEAT_DETERM o dtac ctxt meta_spec, REPEAT_DETERM o etac ctxt exE, rtac ctxt rev_mp,
+ rtac ctxt copy, REPEAT_DETERM_N n o assume_tac ctxt,
rtac ctxt impI, REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], REPEAT_DETERM_N n o rtac ctxt exI,
rtac ctxt mor_comp, rtac ctxt mor_Rep, rtac ctxt mor_select, rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI,
rtac ctxt conjI, rtac ctxt refl, assume_tac ctxt,
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Tue Oct 06 11:50:23 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Tue Oct 06 12:01:07 2015 +0200
@@ -673,7 +673,7 @@
fun after_qed ([exhaust_thm] :: thmss) lthy =
let
- val ((((((((xss, xss'), fs), gs), h), (u, u')), v), p), names_lthy) =
+ val ((((((((xss, xss'), fs), gs), h), (u, u')), v), p), _) =
lthy
|> mk_Freess' "x" ctr_Tss
||>> mk_Frees "f" case_Ts
@@ -754,12 +754,14 @@
Logic.list_implies (uv_eq :: @{map 4} mk_prem xctrs xss xfs xgs,
mk_Trueprop_eq (eta_ufcase, eta_vgcase));
val weak_goal = Logic.mk_implies (uv_eq, mk_Trueprop_eq (ufcase, vfcase));
+ val vars = Variable.add_free_names lthy goal [];
+ val weak_vars = Variable.add_free_names lthy weak_goal [];
in
- (Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
+ (Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
mk_case_cong_tac ctxt uexhaust_thm case_thms),
- Goal.prove_sorry lthy [] [] weak_goal (fn {context = ctxt, prems = _} =>
+ Goal.prove_sorry lthy weak_vars [] weak_goal (fn {context = ctxt, prems = _} =>
etac ctxt arg_cong 1))
- |> apply2 (Thm.close_derivation #> singleton (Proof_Context.export names_lthy lthy))
+ |> apply2 (Thm.close_derivation)
end;
val split_lhs = q $ ufcase;
@@ -778,15 +780,15 @@
(@{map 3} mk_split_disjunct xctrs xss xfs)));
fun prove_split selss goal =
- Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
- mk_split_tac ctxt ms uexhaust_thm case_thms selss inject_thmss distinct_thmsss)
- |> singleton (Proof_Context.export names_lthy lthy)
+ Variable.add_free_names lthy goal []
+ |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
+ mk_split_tac ctxt ms uexhaust_thm case_thms selss inject_thmss distinct_thmsss))
|> Thm.close_derivation;
fun prove_split_asm asm_goal split_thm =
- Goal.prove_sorry lthy [] [] asm_goal (fn {context = ctxt, ...} =>
- mk_split_asm_tac ctxt split_thm)
- |> singleton (Proof_Context.export names_lthy lthy)
+ 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;
val (split_thm, split_asm_thm) =
@@ -842,10 +844,10 @@
let
val m = the_single ms;
val goal = mk_Trueprop_eq (mk_uu_eq (), the_single exist_xs_u_eq_ctrs);
+ val vars = Variable.add_free_names lthy goal [];
in
- Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
+ Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
mk_unique_disc_def_tac ctxt m uexhaust_thm)
- |> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation
end;
@@ -854,11 +856,11 @@
val goal =
mk_Trueprop_eq (alternate_disc_lhs (K (nth udiscs)) (3 - k),
nth exist_xs_u_eq_ctrs (k - 1));
+ val vars = Variable.add_free_names lthy goal [];
in
- Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
+ 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)
- |> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation
end;
@@ -991,12 +993,12 @@
(@{map 5} mk_prems ks udiscs uselss vdiscs vselss, uv_eq);
val uncollapse_thms =
map2 (fn thm => fn [] => thm | _ => thm RS sym) all_collapse_thms uselss;
+ val vars = Variable.add_free_names lthy goal [];
in
- Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
+ Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
mk_expand_tac ctxt n ms (inst_thm u exhaust_disc_thm)
(inst_thm v exhaust_disc_thm) uncollapse_thms distinct_disc_thmsss
distinct_disc_thmsss')
- |> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation
end;
@@ -1015,10 +1017,10 @@
val case_eq_if_thm =
let
val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs usel_fs);
+ val vars = Variable.add_free_names lthy goal [];
in
- Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
+ Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} =>
mk_case_eq_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)
- |> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation
end;
@@ -1029,13 +1031,14 @@
fold_rev Term.absdummy argTs (const_of_bool (n = k))) ctr_Tss;
val goals = map_index (fn (n, udisc) =>
mk_Trueprop_eq (udisc, list_comb (casexBool, mk_case_args n) $ u)) udiscs;
+ val goal = Logic.mk_conjunction_balanced goals;
+ val vars = Variable.add_free_names lthy goal [];
in
- Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
+ 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
|> Conjunction.elim_balanced (length goals)
- |> Proof_Context.export names_lthy lthy
end;
in
(sel_defs, all_sel_thms, sel_thmss, disc_defs, disc_thmss, nontriv_disc_thmss,
@@ -1052,10 +1055,10 @@
fold_rev Term.lambda args (h $ list_comb (f, args))
end) fs ctr_Tss;
val goal = mk_Trueprop_eq (h $ ufcase, list_comb (casexC, args) $ u);
+ val vars = Variable.add_free_names lthy goal [];
in
- Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
+ Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} =>
mk_case_distrib_tac ctxt (Thm.cterm_of ctxt u) exhaust_thm case_thms)
- |> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation
end;