# HG changeset patch # User traytel # Date 1444125667 -7200 # Node ID 8d40ddaa427f3fa0d711e16aeb42fe853c046bd5 # Parent 24b5e7579fdd87c8c8704c077e300bbc15c4b160 collect the names from goals in favor of fragile exports diff -r 24b5e7579fdd -r 8d40ddaa427f src/HOL/Tools/BNF/bnf_def.ML --- 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; diff -r 24b5e7579fdd -r 8d40ddaa427f src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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 [] [] diff -r 24b5e7579fdd -r 8d40ddaa427f src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- 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 diff -r 24b5e7579fdd -r 8d40ddaa427f src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML --- 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); diff -r 24b5e7579fdd -r 8d40ddaa427f src/HOL/Tools/BNF/bnf_gfp.ML --- 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 diff -r 24b5e7579fdd -r 8d40ddaa427f src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- 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 = diff -r 24b5e7579fdd -r 8d40ddaa427f src/HOL/Tools/BNF/bnf_lfp.ML --- 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"); diff -r 24b5e7579fdd -r 8d40ddaa427f src/HOL/Tools/BNF/bnf_lfp_size.ML --- 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 diff -r 24b5e7579fdd -r 8d40ddaa427f src/HOL/Tools/BNF/bnf_lfp_tactics.ML --- 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, diff -r 24b5e7579fdd -r 8d40ddaa427f src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- 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;