# HG changeset patch # User blanchet # Date 1388652622 -3600 # Node ID 2fdec6c29eb79c097d3eef51c7cc78474c0388b4 # Parent 5d965f17b0e4233718b5405edc5a5ad867b116a4 don't generate any proof obligation for implicit (de facto) exclusiveness diff -r 5d965f17b0e4 -r 2fdec6c29eb7 src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Thu Jan 02 09:50:22 2014 +0100 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Thu Jan 02 09:50:22 2014 +0100 @@ -21,6 +21,7 @@ structure BNF_GFP_Rec_Sugar : BNF_GFP_REC_SUGAR = struct +open Ctr_Sugar_General_Tactics open Ctr_Sugar open BNF_Util open BNF_Def @@ -532,15 +533,15 @@ val catch_all = try (fst o dest_Free o the_single) prems' = SOME Name.uu_; val matchedss = AList.lookup (op =) matchedsss fun_name |> the_default []; val prems = map (abstract (List.rev fun_args)) prems'; - val real_prems = + val actual_prems = (if catch_all orelse sequential then maps s_not_conj matchedss else []) @ (if catch_all then [] else prems); val matchedsss' = AList.delete (op =) fun_name matchedsss - |> cons (fun_name, if sequential then matchedss @ [prems] else matchedss @ [real_prems]); + |> cons (fun_name, if sequential then matchedss @ [prems] else matchedss @ [actual_prems]); val user_eqn = - (real_prems, concl) + (actual_prems, concl) |>> map HOLogic.mk_Trueprop ||> HOLogic.mk_Trueprop o abstract (List.rev fun_args) |> curry Logic.list_all (map dest_Free fun_args) o Logic.list_implies; in @@ -551,7 +552,7 @@ ctr = ctr, ctr_no = ctr_no, disc = disc, - prems = real_prems, + prems = actual_prems, auto_gen = catch_all, maybe_ctr_rhs = maybe_ctr_rhs, maybe_code_rhs = maybe_code_rhs, @@ -807,9 +808,11 @@ |> rpair excludess' end; -fun mk_real_disc_eqns fun_binding arg_Ts ({ctr_specs, ...} : corec_spec) +fun mk_actual_disc_eqns fun_binding arg_Ts exhaustive ({ctr_specs, ...} : corec_spec) (sel_eqns : coeqn_data_sel list) (disc_eqns : coeqn_data_disc list) = - if length disc_eqns <> length ctr_specs - 1 then disc_eqns else + if exhaustive orelse length disc_eqns <> length ctr_specs - 1 then + disc_eqns + else let val n = 0 upto length ctr_specs |> the o find_first (fn idx => not (exists (equal idx o #ctr_no) disc_eqns)); @@ -903,7 +906,8 @@ |> map (flat o snd); val arg_Tss = map (binder_types o snd o fst) fixes; - val disc_eqnss = map5 mk_real_disc_eqns bs arg_Tss corec_specs sel_eqnss disc_eqnss'; + val disc_eqnss = map6 mk_actual_disc_eqns bs arg_Tss exhaustives corec_specs sel_eqnss + disc_eqnss'; val (defs, excludess') = build_codefs lthy' bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss; @@ -927,26 +931,39 @@ |> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd)) |> split_list o map split_list; - val de_facto_exhaustives = - map2 (fn exhaustive => fn disc_eqns => - exhaustive orelse forall (null o #prems) disc_eqns orelse exists #auto_gen disc_eqns) - exhaustives disc_eqnss; - val list_all_fun_args = map2 ((fn {fun_args, ...} => map (curry Logic.list_all (map dest_Free fun_args))) o hd) disc_eqnss; + val syntactic_exhaustives = + map (fn disc_eqns => forall (null o #prems) disc_eqns orelse exists #auto_gen disc_eqns) + disc_eqnss; + val de_facto_exhaustives = + map2 (fn b => fn b' => b orelse b') exhaustives syntactic_exhaustives; + + fun map_prove_with_tac tac = + map (fn goal => Goal.prove lthy [] [] goal tac |> Thm.close_derivation); + val nchotomy_goalss = map2 (fn false => K [] | true => single o HOLogic.mk_Trueprop o mk_dnf o map #prems) de_facto_exhaustives disc_eqnss |> list_all_fun_args val nchotomy_taut_thmss = - (case maybe_tac of - SOME tac => map (map (fn goal => Goal.prove lthy [] [] goal tac |> Thm.close_derivation)) - nchotomy_goalss - | NONE => []); + map2 (fn syntactic_exhaustive => + (case maybe_tac of + SOME tac => map_prove_with_tac tac + | NONE => + if syntactic_exhaustive then + map_prove_with_tac (fn {context = ctxt, ...} => HEADGOAL (clean_blast_tac ctxt)) + else + K [])) + syntactic_exhaustives nchotomy_goalss; val goalss = goalss' - |> (if is_none maybe_tac then append (map (map (rpair [])) nchotomy_goalss) else I); + |> (if is_none maybe_tac then + append (map2 (fn true => K [] | false => map (rpair [])) syntactic_exhaustives + nchotomy_goalss) + else + I); val p = Var (("P", 0), HOLogic.boolT); (* safe since there are no other variables around *) @@ -956,8 +973,8 @@ let val def_thms = map (snd o snd) def_thms'; - val nchotomy_thmss = - if is_none maybe_tac then take actual_nn thmss'' else nchotomy_taut_thmss; + val nchotomy_thmss = nchotomy_taut_thmss + |> (if is_none maybe_tac then map2 append (take actual_nn thmss'') else I); val exclude_thmss = thmss'' |> is_none maybe_tac ? drop actual_nn; val exhaust_thmss = @@ -1074,7 +1091,7 @@ |> single end; - fun prove_code de_facto_exhaustive disc_eqns sel_eqns nchotomys ctr_alist ctr_specs = + fun prove_code exhaustive disc_eqns sel_eqns nchotomys ctr_alist ctr_specs = let val maybe_fun_data = (find_first (member (op =) (map #ctr ctr_specs) o #ctr) disc_eqns, @@ -1098,7 +1115,7 @@ 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; - in SOME (rhs, raw_rhs, ctr_thms) end + in SOME (false, rhs, raw_rhs, ctr_thms) end | NONE => let fun prove_code_ctr {ctr, sels, ...} = @@ -1116,24 +1133,28 @@ SOME (prems, t) end; val maybe_ctr_conds_argss = map prove_code_ctr ctr_specs; + val exhaustive_code = + exhaustive + orelse forall null (map_filter (try (fst o the)) maybe_ctr_conds_argss) + orelse forall is_some maybe_ctr_conds_argss + andalso exists #auto_gen disc_eqns; + val rhs = + (if exhaustive_code then + split_last (map_filter I maybe_ctr_conds_argss) ||> snd + else + Const (@{const_name Code.abort}, @{typ String.literal} --> + (@{typ unit} --> body_type fun_T) --> body_type fun_T) $ + HOLogic.mk_literal fun_name $ + absdummy @{typ unit} (incr_boundvars 1 lhs) + |> pair (map_filter I maybe_ctr_conds_argss)) + |-> fold_rev (fn (prems, u) => mk_If (s_conjs prems) u) in - let - val rhs = - (if de_facto_exhaustive then - split_last (map_filter I maybe_ctr_conds_argss) ||> snd - else - Const (@{const_name Code.abort}, @{typ String.literal} --> - (@{typ unit} --> body_type fun_T) --> body_type fun_T) $ - HOLogic.mk_literal fun_name $ - absdummy @{typ unit} (incr_boundvars 1 lhs) - |> pair (map_filter I maybe_ctr_conds_argss)) - |-> fold_rev (fn (prems, u) => mk_If (s_conjs prems) u) - in SOME (rhs, rhs, map snd ctr_alist) end + SOME (exhaustive_code, rhs, rhs, map snd ctr_alist) end); in (case maybe_rhs_info of NONE => [] - | SOME (rhs, raw_rhs, ctr_thms) => + | SOME (exhaustive_code, rhs, raw_rhs, ctr_thms) => let val ms = map (Logic.count_prems o prop_of) ctr_thms; val (raw_goal, goal) = (raw_rhs, rhs) @@ -1143,7 +1164,8 @@ 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 (try the_single nchotomys) + sel_splits sel_split_asms ms ctr_thms + (if exhaustive_code then try the_single nchotomys else NONE) |> K |> Goal.prove lthy [] [] raw_goal |> Thm.close_derivation; in @@ -1167,7 +1189,6 @@ else let val {disc, disc_excludess, ...} = nth ctr_specs ctr_no; - val m = length prems; val goal = mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args |> curry betapply disc, mk_conjs prems) @@ -1190,8 +1211,8 @@ ctr_specss; val ctr_thmss = map (map snd) ctr_alists; - val code_thmss = map6 prove_code de_facto_exhaustives disc_eqnss sel_eqnss nchotomy_thmss - ctr_alists ctr_specss; + val code_thmss = map6 prove_code exhaustives disc_eqnss sel_eqnss nchotomy_thmss ctr_alists + ctr_specss; val simp_thmss = map2 append disc_thmss sel_thmss diff -r 5d965f17b0e4 -r 2fdec6c29eb7 src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Thu Jan 02 09:50:22 2014 +0100 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Thu Jan 02 09:50:22 2014 +0100 @@ -36,12 +36,13 @@ fun mk_primcorec_exhaust_tac n nchotomy = let val ks = 1 upto n in - HEADGOAL (cut_tac nchotomy THEN' - EVERY' (map (fn k => - (if k < n then etac disjE else K all_tac) THEN' - REPEAT o (etac conjE THEN' dtac meta_mp THEN' atac) THEN' - dtac meta_mp THEN' atac THEN' atac) - ks)) + HEADGOAL (atac ORELSE' + cut_tac nchotomy THEN' + EVERY' (map (fn k => + (if k < n then etac disjE else K all_tac) THEN' + REPEAT o (etac conjE THEN' dtac meta_mp THEN' atac) THEN' + dtac meta_mp THEN' atac THEN' atac) + ks)) end; fun mk_primcorec_assumption_tac ctxt discIs = diff -r 5d965f17b0e4 -r 2fdec6c29eb7 src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML Thu Jan 02 09:50:22 2014 +0100 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML Thu Jan 02 09:50:22 2014 +0100 @@ -7,6 +7,7 @@ signature CTR_SUGAR_GENERAL_TACTICS = sig + val clean_blast_tac: Proof.context -> int -> tactic val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic val unfold_thms_tac: Proof.context -> thm list -> tactic end; @@ -41,6 +42,8 @@ val meta_mp = @{thm meta_mp}; +fun clean_blast_tac ctxt = blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt); + fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl, tac, REPEAT_DETERM_N (n - k) o etac thin_rl]); @@ -157,7 +160,7 @@ ALLGOALS (fn k => (hyp_subst_tac ctxt THEN' simp_tac (ss_only (@{thms simp_thms} @ cases @ nth selss (k - 1) @ nth injectss (k - 1) @ flat (nth distinctsss (k - 1))) ctxt)) k) THEN - ALLGOALS (blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt)); + ALLGOALS (clean_blast_tac ctxt); val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};