# HG changeset patch # User blanchet # Date 1381735024 -7200 # Node ID 94f2dc9aea7a28496b14ad33beecf16dedd93f11 # Parent 6fefbaeccb63dd7c65f6b4edb311fe68a695618f strengthened tactic w.r.t. "let" diff -r 6fefbaeccb63 -r 94f2dc9aea7a src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Sun Oct 13 21:36:26 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Mon Oct 14 09:17:04 2013 +0200 @@ -1015,14 +1015,11 @@ val raw_code_thm = mk_primcorec_raw_code_of_ctr_tac lthy distincts discIs sel_splits sel_split_asms ms ctr_thms |> K |> Goal.prove lthy [] [] raw_t; -val _ = tracing ("raw code theorem: " ^ Syntax.string_of_term lthy (prop_of raw_code_thm)); in - mk_primcorec_code_of_raw_code_tac sel_splits raw_code_thm + mk_primcorec_code_of_raw_code_tac lthy sel_splits raw_code_thm |> K |> Goal.prove lthy [] [] t -|> tap (tracing o curry (op ^) "code theorem: " o Syntax.string_of_term lthy o prop_of) |> single end -handle ERROR s => (warning s; []) (*###*) end; val disc_alists = map3 (maps oo prove_disc) corec_specs exclssss disc_eqnss; diff -r 6fefbaeccb63 -r 94f2dc9aea7a src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Sun Oct 13 21:36:26 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Mon Oct 14 09:17:04 2013 +0200 @@ -8,7 +8,7 @@ signature BNF_FP_REC_SUGAR_TACTICS = sig val mk_primcorec_assumption_tac: Proof.context -> thm list -> int -> tactic - val mk_primcorec_code_of_raw_code_tac: thm list -> thm -> tactic + val mk_primcorec_code_of_raw_code_tac: Proof.context -> thm list -> thm -> tactic val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list -> tactic @@ -89,7 +89,8 @@ (* TODO: reduce code duplication with selector tactic above *) fun mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m f_ctr = - HEADGOAL (REPEAT o (resolve_tac split_connectI ORELSE' split_tac (split_if :: splits))) THEN + HEADGOAL (REPEAT o (resolve_tac split_connectI ORELSE' + Splitter.split_tac (split_if :: splits))) THEN mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN HEADGOAL ((REPEAT_DETERM_N m o mk_primcorec_assumption_tac ctxt discIs) THEN' SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o @@ -105,8 +106,9 @@ EVERY (map2 (mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms) ms ctr_thms); -fun mk_primcorec_code_of_raw_code_tac splits raw = - HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN' REPEAT_DETERM o +fun mk_primcorec_code_of_raw_code_tac ctxt splits raw = + HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN' + SELECT_GOAL (unfold_thms_tac ctxt @{thms Let_def}) THEN' REPEAT_DETERM o (rtac refl ORELSE' (TRY o rtac sym) THEN' atac ORELSE' resolve_tac split_connectI ORELSE'