# HG changeset patch # User Andreas Lochbihler # Date 1380207040 -7200 # Node ID 2e75da4fe4b6e9188d3e1f4022c9c61d273b53c3 # Parent abe2b313f0e5caa66614dbe8bf210e36946228b3# Parent 9fc9a59ad579a039ae80256bd5b3e8f302de403f merged diff -r abe2b313f0e5 -r 2e75da4fe4b6 src/HOL/BNF/Tools/bnf_ctr_sugar.ML --- 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)); diff -r abe2b313f0e5 -r 2e75da4fe4b6 src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML --- 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' diff -r abe2b313f0e5 -r 2e75da4fe4b6 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML --- 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 diff -r abe2b313f0e5 -r 2e75da4fe4b6 src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML --- 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; diff -r abe2b313f0e5 -r 2e75da4fe4b6 src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML --- 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;