# HG changeset patch # User blanchet # Date 1389366661 -3600 # Node ID afc156c7e4f7bf100f0d722a9e540cfc87019c5e # Parent 63a5e0d8ce3bdd071dd8e6b9891e0991296033db cope gracefully with missing ctr equations by plugging in 'False ==> ...' diff -r 63a5e0d8ce3b -r afc156c7e4f7 src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Fri Jan 10 15:48:13 2014 +0100 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Fri Jan 10 16:11:01 2014 +0100 @@ -1172,7 +1172,8 @@ val raw_rhs = expand_corec_code_rhs lthy has_call bound_Ts rhs; val cond_ctrs = fold_rev_corec_code_rhs lthy (K oo (cons oo pair)) bound_Ts raw_rhs []; - val ctr_thms = map (the o AList.lookup (op =) ctr_alist o snd) cond_ctrs; + val ctr_thms = + map (the_default FalseE o AList.lookup (op =) ctr_alist o snd) cond_ctrs; in SOME (false, rhs, raw_rhs, ctr_thms) end | NONE => let @@ -1221,13 +1222,13 @@ val (distincts, discIs, sel_splits, sel_split_asms) = case_thms_of_term lthy bound_Ts raw_rhs; - val raw_code_thm = mk_primcorec_raw_code_of_ctr_tac lthy distincts discIs - sel_splits sel_split_asms ms ctr_thms + val raw_code_thm = mk_primcorec_raw_code_tac lthy distincts discIs sel_splits + sel_split_asms ms ctr_thms (if exhaustive_code then try the_single nchotomys else NONE) |> K |> Goal.prove_sorry lthy [] [] raw_goal |> Thm.close_derivation; in - mk_primcorec_code_of_raw_code_tac lthy distincts sel_splits raw_code_thm + mk_primcorec_code_tac lthy distincts sel_splits raw_code_thm |> K |> Goal.prove_sorry lthy [] [] goal |> Thm.close_derivation |> single diff -r 63a5e0d8ce3b -r afc156c7e4f7 src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Fri Jan 10 15:48:13 2014 +0100 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Fri Jan 10 16:11:01 2014 +0100 @@ -8,7 +8,7 @@ signature BNF_GFP_REC_SUGAR_TACTICS = sig val mk_primcorec_assumption_tac: Proof.context -> thm list -> int -> tactic - val mk_primcorec_code_of_raw_code_tac: Proof.context -> thm list -> thm list -> thm -> tactic + val mk_primcorec_code_tac: Proof.context -> thm list -> thm list -> thm -> tactic val mk_primcorec_ctr_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 @@ -16,8 +16,8 @@ thm list -> tactic val mk_primcorec_exhaust_tac: Proof.context -> string list -> int -> thm -> tactic val mk_primcorec_nchotomy_tac: Proof.context -> thm list -> tactic - val mk_primcorec_raw_code_of_ctr_tac: Proof.context -> thm list -> thm list -> thm list -> - thm list -> int list -> thm list -> thm option -> tactic + val mk_primcorec_raw_code_tac: Proof.context -> thm list -> thm list -> thm list -> thm list -> + int list -> thm list -> thm option -> tactic val mk_primcorec_sel_tac: Proof.context -> thm list -> thm list -> thm list -> thm list -> thm list -> thm list -> thm list -> thm -> int -> int -> thm list list list -> tactic end; @@ -157,7 +157,7 @@ end | _ => split); -fun raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m fun_ctr = +fun raw_code_single_tac ctxt distincts discIs splits split_asms m fun_ctr = let val splits' = map (fn th => th RS iffD2) (@{thm split_if_eq2} :: map (inst_split_eq ctxt) splits) @@ -177,8 +177,7 @@ fun rulify_nchotomy n = funpow (n - 1) (fn thm => thm RS @{thm Meson.make_pos_rule'}); -fun mk_primcorec_raw_code_of_ctr_tac ctxt distincts discIs splits split_asms ms fun_ctrs - nchotomy_opt = +fun mk_primcorec_raw_code_tac ctxt distincts discIs splits split_asms ms fun_ctrs nchotomy_opt = let val n = length ms; val (ms', fun_ctrs') = @@ -192,13 +191,12 @@ ||> (fn thm => [rulify_nchotomy n nchotomy RS thm] handle THM _ => [thm]) |> op @)); in - EVERY (map2 (raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms) - ms' fun_ctrs') THEN + EVERY (map2 (raw_code_single_tac ctxt distincts discIs splits split_asms) ms' fun_ctrs') THEN IF_UNSOLVED (unfold_thms_tac ctxt @{thms Code.abort_def} THEN HEADGOAL (REPEAT_DETERM o resolve_tac (refl :: split_connectI))) end; -fun mk_primcorec_code_of_raw_code_tac ctxt distincts splits raw = +fun mk_primcorec_code_tac ctxt distincts splits raw = HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN' SELECT_GOAL (unfold_thms_tac ctxt unfold_lets) THEN' REPEAT_DETERM o (rtac refl ORELSE' atac ORELSE'