--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Thu Sep 26 15:50:33 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Thu Sep 26 16:50:40 2013 +0200
@@ -252,16 +252,20 @@
(case ctr_sugar_of ctxt s of
SOME {casex = Const (case_name, _), discs = discs0, selss = selss0, ...} =>
if case_name = c then
- let
- val n = length discs0;
- val (branches, obj :: leftovers) = chop n args;
- val discs = map (mk_disc_or_sel Ts) discs0;
- val selss = map (map (mk_disc_or_sel Ts)) selss0;
- val conds = map (rapp obj) discs;
- val branch_argss = map (fn sels => map (rapp obj) sels @ leftovers) selss;
- val branches' = map2 (curry Term.betapplys) branches branch_argss;
- in
- SOME (conds, branches')
+ let val n = length discs0 in
+ if n < length args then
+ let
+ val (branches, obj :: leftovers) = chop n args;
+ val discs = map (mk_disc_or_sel Ts) discs0;
+ val selss = map (map (mk_disc_or_sel Ts)) selss0;
+ val conds = map (rapp obj) discs;
+ val branch_argss = map (fn sels => map (rapp obj) sels @ leftovers) selss;
+ val branches' = map2 (curry Term.betapplys) branches branch_argss;
+ in
+ SOME (conds, branches')
+ end
+ else
+ NONE
end
else
NONE
@@ -310,12 +314,10 @@
val raw_disc_bindings' = pad_list Binding.empty n raw_disc_bindings;
- fun can_definitely_rely_on_disc k =
- not (Binding.is_empty (nth raw_disc_bindings' (k - 1)));
+ fun can_definitely_rely_on_disc k = not (Binding.is_empty (nth raw_disc_bindings' (k - 1)));
fun can_rely_on_disc k =
can_definitely_rely_on_disc k orelse (k = 1 andalso not (can_definitely_rely_on_disc 2));
- fun should_omit_disc_binding k =
- n = 1 orelse (n = 2 andalso can_rely_on_disc (3 - k));
+ fun should_omit_disc_binding k = n = 1 orelse (n = 2 andalso can_rely_on_disc (3 - k));
fun is_disc_binding_valid b =
not (Binding.is_empty b orelse Binding.eq_name (b, equal_binding));
@@ -384,10 +386,9 @@
fun mk_case_disj xctr xf xs =
list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (u, xctr), HOLogic.mk_eq (w, xf)));
- val case_rhs =
- fold_rev (fold_rev Term.lambda) [fs, [u]]
- (Const (@{const_name The}, (B --> HOLogic.boolT) --> B) $
- Term.lambda w (Library.foldr1 HOLogic.mk_disj (map3 mk_case_disj xctrs xfs xss)));
+ val case_rhs = fold_rev (fold_rev Term.lambda) [fs, [u]]
+ (Const (@{const_name The}, (B --> HOLogic.boolT) --> B) $
+ Term.lambda w (Library.foldr1 HOLogic.mk_disj (map3 mk_case_disj xctrs xfs xss)));
val ((raw_case, (_, raw_case_def)), (lthy', lthy)) = no_defs_lthy
|> Local_Theory.define ((case_binding, NoSyn), ((Thm.def_binding case_binding, []), case_rhs))
@@ -811,7 +812,7 @@
|> Thm.close_derivation
end;
- val expand_thms =
+ val expand_thm =
let
fun mk_prems k udisc usels vdisc vsels =
(if k = n then [] else [mk_Trueprop_eq (udisc, vdisc)]) @
@@ -829,12 +830,12 @@
val uncollapse_thms =
map2 (fn thm => fn [] => thm | _ => thm RS sym) all_collapse_thms uselss;
in
- [Goal.prove_sorry lthy [] [] goal (fn _ =>
- mk_expand_tac lthy n ms (inst_thm u disc_exhaust_thm)
- (inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss
- disc_exclude_thmsss')]
- |> map Thm.close_derivation
- |> Proof_Context.export names_lthy lthy
+ Goal.prove_sorry lthy [] [] goal (fn _ =>
+ mk_expand_tac lthy n ms (inst_thm u disc_exhaust_thm)
+ (inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss
+ disc_exclude_thmsss')
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
val (sel_split_thm, sel_split_asm_thm) =
@@ -849,20 +850,20 @@
(thm, asm_thm)
end;
- val case_conv_if_thms =
+ val case_conv_if_thm =
let
val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs usel_fs);
in
- [Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
- mk_case_conv_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)]
- |> map Thm.close_derivation
- |> Proof_Context.export names_lthy lthy
+ Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
+ mk_case_conv_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
in
(all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms,
nontriv_discI_thms, disc_exclude_thms, [disc_exhaust_thm], [sel_exhaust_thm],
- all_collapse_thms, safe_collapse_thms, expand_thms, [sel_split_thm],
- [sel_split_asm_thm], case_conv_if_thms)
+ all_collapse_thms, safe_collapse_thms, [expand_thm], [sel_split_thm],
+ [sel_split_asm_thm], [case_conv_if_thm])
end;
val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML Thu Sep 26 15:50:33 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML Thu Sep 26 16:50:40 2013 +0200
@@ -65,8 +65,8 @@
val mk_disc_exhaust_tac = mk_disc_or_sel_exhaust_tac;
fun mk_sel_exhaust_tac n disc_exhaust collapses =
- if n = 1 then HEADGOAL (etac meta_mp THEN' resolve_tac collapses)
- else mk_disc_or_sel_exhaust_tac n disc_exhaust collapses;
+ mk_disc_or_sel_exhaust_tac n disc_exhaust collapses ORELSE
+ HEADGOAL (etac meta_mp THEN' resolve_tac collapses);
fun mk_collapse_tac ctxt m discD sels =
HEADGOAL (dtac discD THEN'
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Thu Sep 26 15:50:33 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Thu Sep 26 16:50:40 2013 +0200
@@ -734,7 +734,7 @@
val (defs, exclss') =
co_build_defs lthy' bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss;
- fun prove_excl_tac (c, c', a) =
+ fun excl_tac (c, c', a) =
if a orelse c = c' orelse sequential then SOME (K (mk_primcorec_assumption_tac lthy []))
else if simple then SOME (K (auto_tac lthy))
else NONE;
@@ -745,7 +745,7 @@
*)
val exclss'' = exclss' |> map (map (fn (idx, t) =>
- (idx, (Option.map (Goal.prove lthy [] [] t) (prove_excl_tac idx), t))));
+ (idx, (Option.map (Goal.prove lthy [] [] t) (excl_tac idx), t))));
val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) exclss'';
val (obligation_idxss, obligationss) = exclss''
|> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd))
@@ -800,7 +800,7 @@
|> HOLogic.mk_Trueprop o HOLogic.mk_eq
|> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
|> curry Logic.list_all (map dest_Free fun_args);
- val (distincts, _, _, sel_splits, sel_split_asms) = case_thms_of_term lthy [] rhs_term;
+ val (distincts, _, sel_splits, sel_split_asms) = case_thms_of_term lthy [] rhs_term;
in
mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms nested_maps
nested_map_idents nested_map_comps sel_corec k m exclsss
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Thu Sep 26 15:50:33 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Thu Sep 26 16:50:40 2013 +0200
@@ -9,8 +9,8 @@
sig
val mk_primcorec_assumption_tac: Proof.context -> thm list -> tactic
val mk_primcorec_code_of_ctr_tac: Proof.context -> thm list -> thm list -> thm list -> thm list ->
- thm list -> int list -> thm list -> tactic
- val mk_primcorec_code_of_raw_tac: thm list -> thm list -> thm -> thm list -> tactic
+ int list -> thm list -> tactic
+ val mk_primcorec_code_of_raw_tac: thm list -> 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
@@ -40,7 +40,7 @@
fun mk_primcorec_assumption_tac ctxt discIs =
HEADGOAL (SELECT_GOAL (unfold_thms_tac ctxt
@{thms not_not not_False_eq_True de_Morgan_conj de_Morgan_disj} THEN
- SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE'
+ SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE' etac conjE ORELSE'
resolve_tac @{thms TrueI conjI disjI1 disjI2} ORELSE'
dresolve_tac discIs THEN' atac)))));
@@ -49,7 +49,7 @@
else REPEAT_DETERM_N (m - 1) o (rtac conjI THEN' atac) THEN' atac);
fun mk_primcorec_different_case_tac ctxt excl =
- unfold_thms_tac ctxt @{thms not_not not_False_eq_True} THEN
+ unfold_thms_tac ctxt @{thms not_not not_False_eq_True not_True_eq_False} THEN
HEADGOAL (rtac excl THEN_ALL_NEW SELECT_GOAL (mk_primcorec_assumption_tac ctxt []));
fun mk_primcorec_cases_tac ctxt k m exclsss =
@@ -83,33 +83,31 @@
(the_default (K all_tac) (Option.map rtac maybe_disc_f)) THEN' REPEAT_DETERM_N m o atac) THEN
unfold_thms_tac ctxt sel_fs THEN HEADGOAL (rtac refl);
-(* TODO: do we need "collapses"? *)
(* TODO: reduce code duplication with selector tactic above *)
-fun mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs collapses splits split_asms m f_ctr =
+fun mk_primcorec_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
mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN
REPEAT_DETERM_N m (mk_primcorec_assumption_tac ctxt discIs) THEN
HEADGOAL (SELECT_GOAL (HEADGOAL (REPEAT_DETERM o
(rtac refl ORELSE' atac ORELSE'
- eresolve_tac (falseEs @ map (fn thm => thm RS trans) collapses) ORELSE'
resolve_tac split_connectI ORELSE'
Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE'
Splitter.split_tac (split_if :: splits) ORELSE'
eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
(TRY o dresolve_tac discIs) THEN' etac notE THEN' atac))));
-fun mk_primcorec_code_of_ctr_tac ctxt distincts discIs collapses splits split_asms ms ctr_thms =
- EVERY (map2 (mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs collapses splits
- split_asms) ms ctr_thms);
+fun mk_primcorec_code_of_ctr_tac ctxt distincts discIs splits split_asms ms ctr_thms =
+ EVERY (map2 (mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs splits split_asms)
+ ms ctr_thms);
-fun mk_primcorec_code_of_raw_tac splits disc_excludes raw collapses =
+fun mk_primcorec_code_of_raw_tac splits disc_excludes raw =
HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN' REPEAT_DETERM o
(rtac refl ORELSE'
(TRY o rtac sym) THEN' atac ORELSE'
resolve_tac split_connectI ORELSE'
Splitter.split_tac (split_if :: splits) ORELSE'
etac notE THEN' atac ORELSE'
- dresolve_tac disc_excludes THEN' etac notE THEN' atac ORELSE'
- eresolve_tac (maps (fn thm => [thm, thm RS sym]) collapses)));
+ (TRY o dresolve_tac disc_excludes) THEN' etac notE THEN' atac));
+
end;
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Thu Sep 26 15:50:33 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Thu Sep 26 16:50:40 2013 +0200
@@ -70,7 +70,7 @@
val fold_rev_corec_code_rhs: Proof.context -> (term list -> term -> term list -> 'a -> 'a) ->
typ list -> term -> 'a -> 'a
val case_thms_of_term: Proof.context -> typ list -> term ->
- thm list * thm list * thm list * thm list * thm list
+ thm list * thm list * thm list * thm list
val rec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->
((term * term list list) list) list -> local_theory ->
@@ -234,7 +234,7 @@
o fld (conds @ s_not_disj cond) else_branch
| (Const (c, _), args as _ :: _ :: _) =>
let val n = num_binder_types (Sign.the_const_type thy c) - 1 in
- if length args > n then
+ if n >= 0 andalso n < length args then
(case fastype_of1 (bound_Ts, nth args n) of
Type (s, Ts) =>
(case dest_case ctxt s Ts t of
@@ -276,7 +276,7 @@
val (gen_branch_Ts, gen_body_fun_T) = strip_fun_type gen_T;
val n = length gen_branch_Ts;
in
- if length args > n then
+ if n < length args then
(case gen_body_fun_T of
Type (_, [Type (T_name, _), _]) =>
if case_of ctxt T_name = SOME c then
@@ -397,8 +397,8 @@
val (caseT_names, _) = fold_rev_let_if_case ctxt (K (K I)) bound_Ts t ();
val ctr_sugars = map (the o ctr_sugar_of ctxt) caseT_names;
in
- (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #collapses ctr_sugars,
- maps #sel_splits ctr_sugars, maps #sel_split_asms ctr_sugars)
+ (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #sel_splits ctr_sugars,
+ maps #sel_split_asms ctr_sugars)
end;
fun indexed xs h = let val h' = h + length xs in (h upto h' - 1, h') end;