use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed)
--- a/src/HOL/Tools/BNF/bnf_comp.ML Sun Aug 10 20:45:48 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Mon Aug 11 10:43:03 2014 +0200
@@ -203,7 +203,7 @@
fun tac {context = ctxt, prems = _} =
mk_simplified_set_tac ctxt (collect_set_map_of_bnf outer);
val set'_eq_set =
- Goal.prove names_lthy [] [] goal tac
+ Goal.prove (*no sorry*) names_lthy [] [] goal tac
|> Thm.close_derivation;
val set' = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of set'_eq_set)));
in
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sun Aug 10 20:45:48 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Aug 11 10:43:03 2014 +0200
@@ -1842,7 +1842,7 @@
(Proof_Context.export lthy' no_defs_lthy) lthy;
fun distinct_prems ctxt th =
- Goal.prove ctxt [] []
+ Goal.prove (*no sorry*) ctxt [] []
(th |> Thm.prop_of |> Logic.strip_horn |>> distinct (op aconv) |> Logic.list_implies)
(fn _ => HEADGOAL (cut_tac th THEN' atac) THEN ALLGOALS eq_assume_tac);
@@ -1852,7 +1852,7 @@
(map (unfold_thms ctxt @{thms atomize_imp[of _ "t = u" for t u]})
[thm, eq_ifIN ctxt thms]));
- val corec_code_thms = map (eq_ifIN lthy) corec_thmss
+ val corec_code_thms = map (eq_ifIN lthy) corec_thmss;
val sel_corec_thmss = map flat sel_corec_thmsss;
val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Sun Aug 10 20:45:48 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Mon Aug 11 10:43:03 2014 +0200
@@ -69,10 +69,11 @@
fun mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses
ctor_rec_o_map =
unfold_thms_tac ctxt [rec_def] THEN
- HEADGOAL (rtac (ctor_rec_o_map RS trans)) THEN
- PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion) THEN
- HEADGOAL (asm_simp_tac (ss_only (pre_map_defs @
- distinct Thm.eq_thm_prop (live_nesting_map_ident0s @ abs_inverses) @ rec_o_map_simp_thms) ctxt));
+ HEADGOAL (rtac (ctor_rec_o_map RS trans) THEN'
+ CONVERSION Thm.eta_long_conversion THEN'
+ asm_simp_tac (ss_only (pre_map_defs @
+ distinct Thm.eq_thm_prop (live_nesting_map_ident0s @ abs_inverses) @
+ rec_o_map_simp_thms) ctxt));
val size_o_map_simp_thms = @{thms prod_inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]};
@@ -303,7 +304,7 @@
curry HOLogic.mk_eq) rec_o_map_lhss rec_o_map_rhss;
val rec_o_map_thms =
map3 (fn goal => fn rec_def => fn ctor_rec_o_map =>
- Goal.prove lthy2 [] [] goal (fn {context = ctxt, ...} =>
+ Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} =>
mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses
ctor_rec_o_map)
|> Thm.close_derivation)
@@ -333,7 +334,7 @@
in terms of "map", which is not the end of the world. *)
val size_o_map_thmss =
map3 (fn goal => fn size_def => the_list o try (fn rec_o_map =>
- Goal.prove lthy2 [] [] goal (fn {context = ctxt, ...} =>
+ Goal.prove (*no sorry*) lthy2 [] [] goal (fn {context = ctxt, ...} =>
mk_size_o_map_tac ctxt size_def rec_o_map all_inj_maps nested_size_maps)
|> Thm.close_derivation))
size_o_map_goals size_defs rec_o_map_thms
--- a/src/HOL/Tools/Lifting/lifting_bnf.ML Sun Aug 10 20:45:48 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Mon Aug 11 10:43:03 2014 +0200
@@ -64,8 +64,9 @@
val T_rel = list_comb (mk_rel_of_bnf Ds As Bs bnf, nth argss' 3)
val concl = mk_Quotient [R_rel, Abs_map, Rep_map, T_rel] |> HOLogic.mk_Trueprop
val goal = Logic.list_implies (assms, concl)
- val thm = Goal.prove ctxt [] [] goal
+ val thm = Goal.prove_sorry ctxt [] [] goal
(fn {context = ctxt, prems = _} => Quotient_tac bnf ctxt 1)
+ |> Thm.close_derivation
in
Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
end
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML Sun Aug 10 20:45:48 2014 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Mon Aug 11 10:43:03 2014 +0200
@@ -112,8 +112,9 @@
let
val old_ctxt = ctxt
val (goal, ctxt) = generate_relation_constraint_goal ctxt bnf constraint_def
- val thm = Goal.prove ctxt [] [] goal
+ val thm = Goal.prove_sorry ctxt [] [] goal
(fn {context = ctxt, prems = _} => side_constraint_tac bnf [constraint_def] ctxt 1)
+ |> Thm.close_derivation
in
Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
end
@@ -122,8 +123,9 @@
let
val old_ctxt = ctxt
val (goal, ctxt) = generate_relation_constraint_goal ctxt bnf constraint_def
- val thm = Goal.prove ctxt [] [] goal
+ val thm = Goal.prove_sorry ctxt [] [] goal
(fn {context = ctxt, prems = _} => bi_constraint_tac constraint_def side_constraints ctxt 1)
+ |> Thm.close_derivation
in
Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
end
@@ -219,8 +221,9 @@
val lhs = mk_Domainp (list_comb (relator, args))
val rhs = mk_pred pred_def (map mk_Domainp args) T
val goal = HOLogic.mk_eq (lhs, rhs) |> HOLogic.mk_Trueprop
- val thm = Goal.prove ctxt [] [] goal
+ val thm = Goal.prove_sorry ctxt [] [] goal
(fn {context = ctxt, prems = _} => Domainp_tac bnf pred_def ctxt 1)
+ |> Thm.close_derivation
in
Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
end
@@ -244,8 +247,9 @@
val lhs = list_comb (relator, map mk_eq_onp args)
val rhs = mk_eq_onp (mk_pred pred_def args T)
val goal = HOLogic.mk_eq (lhs, rhs) |> HOLogic.mk_Trueprop
- val thm = Goal.prove ctxt [] [] goal
+ val thm = Goal.prove_sorry ctxt [] [] goal
(fn {context = ctxt, prems = _} => pred_eq_onp_tac bnf pred_def ctxt 1)
+ |> Thm.close_derivation
in
Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
end