# HG changeset patch # User traytel # Date 1407746583 -7200 # Node ID 1e13f63fb452fefb0cdc950798b292d474775038 # Parent 049e13f616d408d2672559bc8c7c54b1886fbf37 use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed) diff -r 049e13f616d4 -r 1e13f63fb452 src/HOL/Tools/BNF/bnf_comp.ML --- 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 diff -r 049e13f616d4 -r 1e13f63fb452 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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; diff -r 049e13f616d4 -r 1e13f63fb452 src/HOL/Tools/BNF/bnf_lfp_size.ML --- 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 diff -r 049e13f616d4 -r 1e13f63fb452 src/HOL/Tools/Lifting/lifting_bnf.ML --- 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 diff -r 049e13f616d4 -r 1e13f63fb452 src/HOL/Tools/Transfer/transfer_bnf.ML --- 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