# HG changeset patch # User blanchet # Date 1448971660 -3600 # Node ID 1647bb48952239c72fe5e493f7452242caf64562 # Parent 49353865e5395827a6b0d6d38509abd9bf3204ef tuned whitespace diff -r 49353865e539 -r 1647bb489522 src/HOL/Tools/BNF/bnf_comp.ML --- a/src/HOL/Tools/BNF/bnf_comp.ML Mon Nov 30 19:12:08 2015 +0100 +++ b/src/HOL/Tools/BNF/bnf_comp.ML Tue Dec 01 13:07:40 2015 +0100 @@ -181,7 +181,8 @@ val CCA = mk_T_of_bnf oDs CAs outer; val CBs = @{map 3} mk_T_of_bnf Dss Bss_repl inners; val outer_sets = mk_sets_of_bnf (replicate olive oDs) (replicate olive CAs) outer; - val inner_setss = @{map 3} mk_sets_of_bnf (map (replicate ilive) Dss) (replicate olive Ass) inners; + val inner_setss = + @{map 3} mk_sets_of_bnf (map (replicate ilive) Dss) (replicate olive Ass) inners; val inner_bds = @{map 3} mk_bd_of_bnf Dss Ass_repl inners; val outer_bd = mk_bd_of_bnf oDs CAs outer; @@ -692,7 +693,8 @@ val ((kill_poss, As), (inners', ((cache', unfold_set'), lthy'))) = normalize_bnfs qualify Ass Ds flatten_tyargs inners accum; - val Ds = oDs @ flat (@{map 3} (uncurry append oo curry swap oo map o nth) tfreess kill_poss Dss); + val Ds = + oDs @ flat (@{map 3} (uncurry append oo curry swap oo map o nth) tfreess kill_poss Dss); val As = map TFree As; in apfst (rpair (Ds, As)) diff -r 49353865e539 -r 1647bb489522 src/HOL/Tools/BNF/bnf_comp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML Mon Nov 30 19:12:08 2015 +0100 +++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML Tue Dec 01 13:07:40 2015 +0100 @@ -74,14 +74,16 @@ map (fn thm => rtac ctxt (thm RS fun_cong)) set_map0s @ [rtac ctxt (Gset_map0 RS comp_eq_dest_lhs), rtac ctxt sym, rtac ctxt trans_o_apply, rtac ctxt trans_image_cong_o_apply, rtac ctxt trans_image_cong_o_apply, - rtac ctxt (@{thm image_cong} OF [Gset_map0 RS comp_eq_dest_lhs RS arg_cong_Union, refl] RS trans), + rtac ctxt (@{thm image_cong} OF [Gset_map0 RS comp_eq_dest_lhs RS arg_cong_Union, refl] + RS trans), rtac ctxt @{thm trans[OF comp_eq_dest[OF Union_natural[symmetric]]]}, rtac ctxt arg_cong_Union, rtac ctxt @{thm trans[OF comp_eq_dest_lhs[OF image_o_collect[symmetric]]]}, rtac ctxt @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @ [REPEAT_DETERM_N (length set_map0s) o EVERY' [rtac ctxt @{thm trans[OF image_insert]}, - rtac ctxt @{thm arg_cong2[of _ _ _ _ insert]}, rtac ctxt @{thm ext}, rtac ctxt trans_o_apply, - rtac ctxt trans_image_cong_o_apply, rtac ctxt @{thm trans[OF image_image]}, - rtac ctxt @{thm sym[OF trans[OF o_apply]]}, rtac ctxt @{thm image_cong[OF refl o_apply]}], + rtac ctxt @{thm arg_cong2[of _ _ _ _ insert]}, rtac ctxt @{thm ext}, + rtac ctxt trans_o_apply, rtac ctxt trans_image_cong_o_apply, + rtac ctxt @{thm trans[OF image_image]}, rtac ctxt @{thm sym[OF trans[OF o_apply]]}, + rtac ctxt @{thm image_cong[OF refl o_apply]}], rtac ctxt @{thm image_empty}]) 1; fun mk_comp_map_cong0_tac ctxt set'_eq_sets comp_set_alts map_cong0 map_cong0s = @@ -96,9 +98,9 @@ EVERY' [select_prem_tac ctxt n (dtac ctxt @{thm meta_spec}) (k + 1), etac ctxt meta_mp, rtac ctxt (equalityD2 RS set_mp), rtac ctxt (set_alt RS fun_cong RS trans), rtac ctxt trans_o_apply, rtac ctxt (@{thm collect_def} RS arg_cong_Union), - rtac ctxt @{thm UnionI}, rtac ctxt @{thm UN_I}, REPEAT_DETERM_N i o rtac ctxt @{thm insertI2}, - rtac ctxt @{thm insertI1}, rtac ctxt (o_apply RS equalityD2 RS set_mp), - etac ctxt @{thm imageI}, assume_tac ctxt]) + rtac ctxt @{thm UnionI}, rtac ctxt @{thm UN_I}, + REPEAT_DETERM_N i o rtac ctxt @{thm insertI2}, rtac ctxt @{thm insertI1}, + rtac ctxt (o_apply RS equalityD2 RS set_mp), etac ctxt @{thm imageI}, assume_tac ctxt]) comp_set_alts)) map_cong0s) 1) end; @@ -220,14 +222,15 @@ fun mk_permute_in_alt_tac ctxt src dest = (rtac ctxt @{thm Collect_cong} THEN' - mk_rotate_eq_tac ctxt (rtac ctxt refl) trans @{thm conj_assoc} @{thm conj_commute} @{thm conj_cong} - dest src) 1; + mk_rotate_eq_tac ctxt (rtac ctxt refl) trans @{thm conj_assoc} @{thm conj_commute} + @{thm conj_cong} dest src) 1; (* Miscellaneous *) fun mk_le_rel_OO_tac ctxt outer_le_rel_OO outer_rel_mono inner_le_rel_OOs = - EVERY' (map (rtac ctxt) (@{thm order_trans} :: outer_le_rel_OO :: outer_rel_mono :: inner_le_rel_OOs)) 1; + EVERY' (map (rtac ctxt) (@{thm order_trans} :: outer_le_rel_OO :: outer_rel_mono :: + inner_le_rel_OOs)) 1; fun mk_simple_rel_OO_Grp_tac ctxt rel_OO_Grp in_alt_thm = rtac ctxt (trans OF [rel_OO_Grp, in_alt_thm RS @{thm OO_Grp_cong} RS sym]) 1; diff -r 49353865e539 -r 1647bb489522 src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Mon Nov 30 19:12:08 2015 +0100 +++ b/src/HOL/Tools/BNF/bnf_def.ML Tue Dec 01 13:07:40 2015 +0100 @@ -1300,10 +1300,12 @@ val funTs = map (fn T => bdT --> T) ranTs; val ran_bnfT = mk_bnf_T ranTs Calpha; val (revTs, Ts) = `rev (bd_bnfT :: funTs); - val cTs = map (SOME o Thm.ctyp_of lthy) [ran_bnfT, Library.foldr1 HOLogic.mk_prodT Ts]; - val tinst = fold (fn T => fn t => HOLogic.mk_case_prod (Term.absdummy T t)) (tl revTs) - (Term.absdummy (hd revTs) (Term.list_comb (mk_bnf_map bdTs ranTs, - map Bound (live - 1 downto 0)) $ Bound live)); + val cTs = map (SOME o Thm.ctyp_of lthy) [ran_bnfT, + Library.foldr1 HOLogic.mk_prodT Ts]; + val tinst = fold (fn T => fn t => + HOLogic.mk_case_prod (Term.absdummy T t)) (tl revTs) + (Term.absdummy (hd revTs) (Term.list_comb (mk_bnf_map bdTs ranTs, + map Bound (live - 1 downto 0)) $ Bound live)); val cts = [NONE, SOME (Thm.cterm_of lthy tinst)]; in Thm.instantiate' cTs cts @{thm surj_imp_ordLeq} @@ -1420,7 +1422,8 @@ val in_rel = Lazy.lazy mk_in_rel; fun mk_rel_flip () = - unfold_thms lthy @{thms conversep_iff} (Lazy.force rel_conversep RS @{thm predicate2_eqD}); + unfold_thms lthy @{thms conversep_iff} + (Lazy.force rel_conversep RS @{thm predicate2_eqD}); val rel_flip = Lazy.lazy mk_rel_flip; diff -r 49353865e539 -r 1647bb489522 src/HOL/Tools/BNF/bnf_def_tactics.ML --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Mon Nov 30 19:12:08 2015 +0100 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Tue Dec 01 13:07:40 2015 +0100 @@ -97,18 +97,20 @@ fun mk_rel_Grp_tac ctxt rel_OO_Grps map_id0 map_cong0 map_id map_comp set_maps = let val n = length set_maps; - val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac else rtac ctxt (hd rel_OO_Grps RS trans); + val rel_OO_Grps_tac = + if null rel_OO_Grps then K all_tac else rtac ctxt (hd rel_OO_Grps RS trans); in if null set_maps then unfold_thms_tac ctxt ((map_id0 RS @{thm Grp_UNIV_id}) :: rel_OO_Grps) THEN rtac ctxt @{thm Grp_UNIV_idI[OF refl]} 1 else EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm antisym}, rtac ctxt @{thm predicate2I}, - REPEAT_DETERM o - eresolve_tac ctxt [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}], - hyp_subst_tac ctxt, rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp, rtac ctxt map_cong0, - REPEAT_DETERM_N n o - EVERY' [rtac ctxt @{thm Collect_case_prod_Grp_eqD}, etac ctxt @{thm set_mp}, assume_tac ctxt], + REPEAT_DETERM o eresolve_tac ctxt + [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}], + hyp_subst_tac ctxt, rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp, + rtac ctxt map_cong0, + REPEAT_DETERM_N n o EVERY' [rtac ctxt @{thm Collect_case_prod_Grp_eqD}, + etac ctxt @{thm set_mp}, assume_tac ctxt], rtac ctxt CollectI, CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans), rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm Collect_case_prod_Grp_in}, @@ -151,8 +153,9 @@ unfold_thms_tac ctxt [rel_compp, rel_conversep, rel_Grp, @{thm vimage2p_Grp}] THEN TRYALL (EVERY' [rtac ctxt iffI, rtac ctxt @{thm relcomppI}, rtac ctxt @{thm GrpI}, resolve_tac ctxt [map_id, refl], rtac ctxt CollectI, - CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks, rtac ctxt @{thm relcomppI}, assume_tac ctxt, - rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI}, resolve_tac ctxt [map_id, refl], rtac ctxt CollectI, + CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks, rtac ctxt @{thm relcomppI}, + assume_tac ctxt, rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI}, + resolve_tac ctxt [map_id, refl], rtac ctxt CollectI, CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks, REPEAT_DETERM o eresolve_tac ctxt @{thms relcomppE conversepE GrpE}, dtac ctxt (trans OF [sym, map_id]), hyp_subst_tac ctxt, assume_tac ctxt]) diff -r 49353865e539 -r 1647bb489522 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Nov 30 19:12:08 2015 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Dec 01 13:07:40 2015 +0100 @@ -75,8 +75,8 @@ val fp_sugar_of_global: theory -> string -> fp_sugar option val fp_sugars_of: Proof.context -> fp_sugar list val fp_sugars_of_global: theory -> fp_sugar list - val fp_sugars_interpretation: string -> - (fp_sugar list -> local_theory -> local_theory)-> theory -> theory + val fp_sugars_interpretation: string -> (fp_sugar list -> local_theory -> local_theory) -> + theory -> theory val interpret_fp_sugars: (string -> bool) -> fp_sugar list -> local_theory -> local_theory val register_fp_sugars_raw: fp_sugar list -> local_theory -> local_theory val register_fp_sugars: (string -> bool) -> fp_sugar list -> local_theory -> local_theory @@ -334,7 +334,7 @@ ); fun fp_sugar_of_generic context = - Option.map (transfer_fp_sugar (Context.theory_of context)) o Symtab.lookup (Data.get context) + Option.map (transfer_fp_sugar (Context.theory_of context)) o Symtab.lookup (Data.get context); fun fp_sugars_of_generic context = Symtab.fold (cons o transfer_fp_sugar (Context.theory_of context) o snd) (Data.get context) []; @@ -1206,7 +1206,8 @@ let val ctr_Tsss' = map repair_nullary_single_ctr ctr_Tsss; val g_absTs = map range_type fun_Ts; - val g_Tsss = map repair_nullary_single_ctr (@{map 5} dest_absumprodT absTs repTs ns mss g_absTs); + val g_Tsss = + map repair_nullary_single_ctr (@{map 5} dest_absumprodT absTs repTs ns mss g_absTs); val g_Tssss = @{map 3} (fn C => map2 (map2 (map (curry (op -->) C) oo unzip_corecT))) Cs ctr_Tsss' g_Tsss; val q_Tssss = map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) g_Tssss; @@ -1312,7 +1313,8 @@ ctor_rec_absTs reps fss xssss))) end; -fun define_corec (_, cs, cpss, (((pgss, _, _, _), cqgsss), f_absTs)) mk_binding fpTs Cs abss dtor_corec = +fun define_corec (_, cs, cpss, (((pgss, _, _, _), cqgsss), f_absTs)) mk_binding fpTs Cs abss + dtor_corec = let val nn = length fpTs; val fpT = range_type (snd (strip_typeN nn (fastype_of dtor_corec))); @@ -1371,8 +1373,8 @@ val rel_induct0_thm = Goal.prove_sorry lthy vars prems goal (fn {context = ctxt, prems} => - mk_rel_induct0_tac ctxt ctor_rel_induct prems (map (Thm.cterm_of ctxt) IRs) exhausts ctor_defss - ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs) + mk_rel_induct0_tac ctxt ctor_rel_induct prems (map (Thm.cterm_of ctxt) IRs) exhausts + ctor_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs) |> Thm.close_derivation; in (postproc_co_induct lthy (length fpA_Ts) @{thm predicate2D} @{thm predicate2D_conj} @@ -1713,8 +1715,8 @@ val thm = Goal.prove_sorry lthy vars prems (HOLogic.mk_Trueprop concl) (fn {context = ctxt, prems} => - mk_set_induct0_tac ctxt (map (Thm.cterm_of ctxt'') Ps) prems dtor_set_inducts exhausts - set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses) + mk_set_induct0_tac ctxt (map (Thm.cterm_of ctxt'') Ps) prems dtor_set_inducts + exhausts set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses) |> Thm.close_derivation; val case_names_attr = @@ -1811,7 +1813,8 @@ [] else [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [udisc, vdisc], - Library.foldr1 HOLogic.mk_conj (@{map 3} (build_rel_app rs') usels vsels ctrXs_Ts))]); + Library.foldr1 HOLogic.mk_conj + (@{map 3} (build_rel_app rs') usels vsels ctrXs_Ts))]); fun mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss = Library.foldr1 HOLogic.mk_conj (flat (@{map 6} (mk_prem_ctr_concls rs' n) @@ -2323,8 +2326,9 @@ in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => - mk_rec_transfer_tac ctxt nn ns (map (Thm.cterm_of ctxt) Ss) (map (Thm.cterm_of ctxt) Rs) xsssss - rec_defs xtor_co_rec_transfers pre_rel_defs live_nesting_rel_eqs) + mk_rec_transfer_tac ctxt nn ns (map (Thm.cterm_of ctxt) Ss) + (map (Thm.cterm_of ctxt) Rs) xsssss rec_defs xtor_co_rec_transfers pre_rel_defs + live_nesting_rel_eqs) |> Thm.close_derivation |> Conjunction.elim_balanced nn end; @@ -2431,7 +2435,8 @@ val rec_o_map_thmss = derive_rec_o_map_thmss lthy recs rec_defs; val simp_thmss = - @{map 6} mk_simp_thms ctr_sugars rec_thmss map_thmss rel_injectss rel_distinctss set_thmss; + @{map 6} mk_simp_thms ctr_sugars rec_thmss map_thmss rel_injectss rel_distinctss + set_thmss; val common_notes = (if nn > 1 then diff -r 49353865e539 -r 1647bb489522 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Mon Nov 30 19:12:08 2015 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Dec 01 13:07:40 2015 +0100 @@ -305,13 +305,15 @@ end; fun solve_prem_prem_tac ctxt = - REPEAT o (eresolve_tac ctxt @{thms bexE rev_bexI} ORELSE' rtac ctxt @{thm rev_bexI[OF UNIV_I]} ORELSE' - hyp_subst_tac ctxt ORELSE' resolve_tac ctxt @{thms disjI1 disjI2}) THEN' + REPEAT o (eresolve_tac ctxt @{thms bexE rev_bexI} ORELSE' + rtac ctxt @{thm rev_bexI[OF UNIV_I]} ORELSE' hyp_subst_tac ctxt ORELSE' + resolve_tac ctxt @{thms disjI1 disjI2}) THEN' (rtac ctxt refl ORELSE' assume_tac ctxt ORELSE' rtac ctxt @{thm singletonI}); fun mk_induct_leverage_prem_prems_tac ctxt nn kks fp_abs_inverses abs_inverses set_maps pre_set_defs = - HEADGOAL (EVERY' (maps (fn kk => [select_prem_tac ctxt nn (dtac ctxt meta_spec) kk, etac ctxt meta_mp, + HEADGOAL (EVERY' (maps (fn kk => [select_prem_tac ctxt nn (dtac ctxt meta_spec) kk, + etac ctxt meta_mp, SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ fp_abs_inverses @ abs_inverses @ set_maps @ sumprod_thms_set)), solve_prem_prem_tac ctxt]) (rev kks))); @@ -366,9 +368,10 @@ fun mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn kk n pre_rel_def fp_abs_inverse abs_inverse dtor_ctor exhaust ctr_defs discss selss = let val ks = 1 upto n in - EVERY' ([rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, select_prem_tac ctxt nn (dtac ctxt meta_spec) kk, - dtac ctxt meta_spec, dtac ctxt meta_mp, assume_tac ctxt, rtac ctxt exhaust, - K (co_induct_inst_as_projs_tac ctxt 0), hyp_subst_tac ctxt] @ + EVERY' ([rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, + select_prem_tac ctxt nn (dtac ctxt meta_spec) kk, dtac ctxt meta_spec, dtac ctxt meta_mp, + assume_tac ctxt, rtac ctxt exhaust, K (co_induct_inst_as_projs_tac ctxt 0), + hyp_subst_tac ctxt] @ @{map 4} (fn k => fn ctr_def => fn discs => fn sels => EVERY' ([rtac ctxt exhaust, K (co_induct_inst_as_projs_tac ctxt 1)] @ map2 (fn k' => fn discs' => @@ -435,8 +438,8 @@ abs_inject :: ctor_defs @ nesting_rel_eqs @ simp_thms' @ @{thms id_bnf_def rel_sum_simps rel_prod_apply vimage2p_def Inl_Inr_False iffD2[OF eq_False Inr_not_Inl] sum.inject prod.inject}) THEN - REPEAT_DETERM (HEADGOAL ((REPEAT_DETERM o etac ctxt conjE) THEN' (REPEAT_DETERM o rtac ctxt conjI) THEN' - (rtac ctxt refl ORELSE' assume_tac ctxt)))) + REPEAT_DETERM (HEADGOAL ((REPEAT_DETERM o etac ctxt conjE) THEN' + (REPEAT_DETERM o rtac ctxt conjI) THEN' (rtac ctxt refl ORELSE' assume_tac ctxt)))) cts assms exhausts discss selss ctor_defss dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses); @@ -445,7 +448,8 @@ rtac ctxt ctor_rel_induct 1 THEN EVERY (@{map 6} (fn cterm => fn exhaust => fn ctor_defs => fn ctor_inject => fn rel_pre_list_def => fn Abs_inverse => HEADGOAL (rtac ctxt exhaust THEN_ALL_NEW (rtac ctxt exhaust THEN_ALL_NEW - (rtac ctxt (infer_instantiate' ctxt (replicate 4 NONE @ [SOME cterm]) @{thm arg_cong2} RS iffD2) + (rtac ctxt (infer_instantiate' ctxt (replicate 4 NONE @ [SOME cterm]) @{thm arg_cong2} + RS iffD2) THEN' assume_tac ctxt THEN' assume_tac ctxt THEN' TRY o resolve_tac ctxt assms))) THEN unfold_thms_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @ @{thms id_bnf_def vimage2p_def}) THEN @@ -485,12 +489,14 @@ (rtac ctxt @{thm singletonI} ORELSE' assume_tac ctxt)); fun mk_set_cases_tac ctxt ct assms exhaust sets = - HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW hyp_subst_tac ctxt) THEN + HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) + THEN_ALL_NEW hyp_subst_tac ctxt) THEN unfold_thms_tac ctxt sets THEN REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt @{thms FalseE emptyE singletonE UnE UN_E insertE} ORELSE' hyp_subst_tac ctxt ORELSE' - SELECT_GOAL (SOLVE (HEADGOAL (eresolve_tac ctxt assms THEN' REPEAT_DETERM o assume_tac ctxt))))); + SELECT_GOAL (SOLVE (HEADGOAL (eresolve_tac ctxt assms THEN' REPEAT_DETERM o + assume_tac ctxt))))); fun mk_set_intros_tac ctxt sets = TRYALL Goal.conjunction_tac THEN unfold_thms_tac ctxt sets THEN @@ -505,7 +511,8 @@ val assms_tac = let val assms' = map (unfold_thms ctxt (@{thm id_bnf_def} :: ctor_defs)) assms in fold (curry (op ORELSE')) (map (fn thm => - funpow (length (Thm.prems_of thm)) (fn tac => tac THEN' assume_tac ctxt) (rtac ctxt thm)) assms') + funpow (length (Thm.prems_of thm)) (fn tac => tac THEN' assume_tac ctxt) + (rtac ctxt thm)) assms') (etac ctxt FalseE) end; val exhausts' = map (fn thm => thm RS @{thm asm_rl[of "P x y" for P x y]}) exhausts @@ -519,8 +526,8 @@ unfold_thms_tac ctxt (Abs_pre_inverses @ dtor_ctors @ set_pre_defs @ ctor_defs @ @{thms id_bnf_def o_apply sum_set_simps prod_set_simps UN_empty UN_insert Un_empty_left Un_empty_right empty_iff singleton_iff}) THEN - REPEAT (HEADGOAL (hyp_subst_tac ctxt ORELSE' eresolve_tac ctxt @{thms UN_E UnE singletonE} ORELSE' - assms_tac)) + REPEAT (HEADGOAL (hyp_subst_tac ctxt ORELSE' + eresolve_tac ctxt @{thms UN_E UnE singletonE} ORELSE' assms_tac)) end; end; diff -r 49353865e539 -r 1647bb489522 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Nov 30 19:12:08 2015 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Dec 01 13:07:40 2015 +0100 @@ -1009,8 +1009,8 @@ |> map2 abs_curried_balanced arg_Tss |> (fn ts => Syntax.check_terms ctxt ts handle ERROR _ => nonprimitive_corec ctxt []) - |> @{map 3} (fn b => fn mx => fn t => ((b, mx), ((Binding.concealed (Thm.def_binding b), []), t))) - bs mxs + |> @{map 3} (fn b => fn mx => fn t => + ((b, mx), ((Binding.concealed (Thm.def_binding b), []), t))) bs mxs |> rpair excludess' end; @@ -1037,7 +1037,8 @@ val prems = maps (s_not_conj o #prems) disc_eqns; val ctr_rhs_opt = Option.map #ctr_rhs_opt sel_eqn_opt |> the_default NONE; val code_rhs_opt = Option.map #code_rhs_opt sel_eqn_opt |> the_default NONE; - val eqn_pos = Option.map (curry (op +) 1 o #eqn_pos) sel_eqn_opt |> the_default 100000; (* FIXME *) + val eqn_pos = Option.map (curry (op +) 1 o #eqn_pos) sel_eqn_opt + |> the_default 100000; (* FIXME *) val extra_disc_eqn = {fun_name = fun_name, fun_T = fun_T, fun_args = fun_args, ctr = ctr, ctr_no = ctr_no, @@ -1307,7 +1308,8 @@ Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => mk_primcorec_sel_tac ctxt def_thms distincts split_sels split_sel_asms - fp_nesting_maps fp_nesting_map_ident0s fp_nesting_map_comps corec_sel k m excludesss) + fp_nesting_maps fp_nesting_map_ident0s fp_nesting_map_comps corec_sel k m + excludesss) |> Thm.close_derivation |> `(is_some code_rhs_opt ? fold_thms lthy sel_defs) (*mildly too aggressive*) |> pair sel @@ -1444,7 +1446,8 @@ Goal.prove_sorry lthy [] [] raw_goal (fn {context = ctxt, prems = _} => mk_primcorec_raw_code_tac ctxt distincts discIs split_sels split_sel_asms - ms ctr_thms (if exhaustive_code then try the_single nchotomys else NONE)) + ms ctr_thms + (if exhaustive_code then try the_single nchotomys else NONE)) |> Thm.close_derivation; in Goal.prove_sorry lthy [] [] goal diff -r 49353865e539 -r 1647bb489522 src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Mon Nov 30 19:12:08 2015 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Tue Dec 01 13:07:40 2015 +0100 @@ -72,7 +72,8 @@ fun mk_primcorec_assumption_tac ctxt discIs = SELECT_GOAL (unfold_thms_tac ctxt @{thms fst_conv snd_conv not_not not_False_eq_True not_True_eq_False de_Morgan_conj de_Morgan_disj} THEN - SOLVE (HEADGOAL (REPEAT o (rtac ctxt refl ORELSE' assume_tac ctxt ORELSE' etac ctxt conjE ORELSE' + SOLVE (HEADGOAL (REPEAT o (rtac ctxt refl ORELSE' assume_tac ctxt ORELSE' + etac ctxt conjE ORELSE' eresolve_tac ctxt falseEs ORELSE' resolve_tac ctxt @{thms TrueI conjI disjI1 disjI2} ORELSE' dresolve_tac ctxt discIs THEN' assume_tac ctxt ORELSE' @@ -137,7 +138,8 @@ resolve_tac ctxt split_connectI ORELSE' Splitter.split_asm_tac ctxt (split_if_asm :: split_asms) ORELSE' Splitter.split_tac ctxt (split_if :: splits) ORELSE' - eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' assume_tac ctxt ORELSE' + eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' + assume_tac ctxt ORELSE' etac ctxt notE THEN' assume_tac ctxt ORELSE' (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def sum.case sum.sel sum.distinct[THEN eq_False[THEN iffD2]]} @ @@ -148,7 +150,8 @@ fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs = HEADGOAL (rtac ctxt ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN' - (the_default (K all_tac) (Option.map (rtac ctxt) disc_fun_opt)) THEN' REPEAT_DETERM_N m o assume_tac ctxt) THEN + (the_default (K all_tac) (Option.map (rtac ctxt) disc_fun_opt)) THEN' + REPEAT_DETERM_N m o assume_tac ctxt) THEN unfold_thms_tac ctxt (@{thm split_def} :: unfold_lets @ sel_funs) THEN HEADGOAL (rtac ctxt refl); fun inst_split_eq ctxt split = diff -r 49353865e539 -r 1647bb489522 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Nov 30 19:12:08 2015 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Tue Dec 01 13:07:40 2015 +0100 @@ -458,7 +458,8 @@ (recs, ctr_poss) |-> map2 (fn recx => fn ctr_pos => list_comb (recx, rec_args) |> permute_args ctr_pos) |> Syntax.check_terms ctxt - |> @{map 3} (fn b => fn mx => fn t => ((b, mx), ((Binding.concealed (Thm.def_binding b), []), t))) + |> @{map 3} (fn b => fn mx => fn t => + ((b, mx), ((Binding.concealed (Thm.def_binding b), []), t))) bs mxs end; diff -r 49353865e539 -r 1647bb489522 src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Mon Nov 30 19:12:08 2015 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Tue Dec 01 13:07:40 2015 +0100 @@ -40,7 +40,8 @@ | basic_lfp_sugars_of bs arg_Ts callers callssss0 lthy0 = let val ((missing_arg_Ts, perm0_kks, - fp_sugars as {fp_nesting_bnfs, fp_co_induct_sugar = {common_co_inducts = [common_induct], ...}, ...} :: _, + fp_sugars as {fp_nesting_bnfs, + fp_co_induct_sugar = {common_co_inducts = [common_induct], ...}, ...} :: _, (lfp_sugar_thms, _)), lthy) = nested_to_mutual_fps (K true) Least_FP bs arg_Ts callers callssss0 lthy0; diff -r 49353865e539 -r 1647bb489522 src/HOL/Tools/BNF/bnf_lfp_size.ML --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Mon Nov 30 19:12:08 2015 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Dec 01 13:07:40 2015 +0100 @@ -42,7 +42,8 @@ Context.proof_map (Data.map (Symtab.update (T_name, (size_name, (size_simps, size_gen_o_maps))))); fun register_size_global T_name size_name size_simps size_gen_o_maps = - Context.theory_map (Data.map (Symtab.update (T_name, (size_name, (size_simps, size_gen_o_maps))))); + Context.theory_map + (Data.map (Symtab.update (T_name, (size_name, (size_simps, size_gen_o_maps))))); val size_of = Symtab.lookup o Data.get o Context.Proof; val size_of_global = Symtab.lookup o Data.get o Context.Theory; @@ -70,8 +71,9 @@ fun mk_size_neq ctxt cts exhaust sizes = HEADGOAL (rtac ctxt (infer_instantiate' ctxt (map SOME cts) exhaust)) THEN ALLGOALS (hyp_subst_tac ctxt) THEN - Ctr_Sugar_Tactics.unfold_thms_tac ctxt (@{thm neq0_conv} :: sizes) THEN - ALLGOALS (REPEAT_DETERM o (rtac ctxt @{thm zero_less_Suc} ORELSE' rtac ctxt @{thm trans_less_add2})); + unfold_thms_tac ctxt (@{thm neq0_conv} :: sizes) THEN + ALLGOALS (REPEAT_DETERM o (rtac ctxt @{thm zero_less_Suc} ORELSE' + rtac ctxt @{thm trans_less_add2})); fun generate_datatype_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs), fp = Least_FP, fp_res = {bnfs = fp_bnfs, ...}, fp_nesting_bnfs, live_nesting_bnfs, ...} : fp_sugar) :: _) @@ -236,7 +238,8 @@ (Spec_Rules.retrieve lthy0 @{const size ('a)} |> map_filter (try (fn (Spec_Rules.Equational, (_, [thm])) => thm))); - val nested_size_maps = map (mk_pointful lthy2) nested_size_gen_o_maps @ nested_size_gen_o_maps; + val nested_size_maps = + map (mk_pointful lthy2) nested_size_gen_o_maps @ nested_size_gen_o_maps; val all_inj_maps = @{thm prod.inj_map} :: map inj_map_of_bnf (fp_bnfs @ fp_nesting_bnfs @ live_nesting_bnfs) |> distinct Thm.eq_thm_prop; diff -r 49353865e539 -r 1647bb489522 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Nov 30 19:12:08 2015 +0100 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Tue Dec 01 13:07:40 2015 +0100 @@ -50,8 +50,8 @@ val ctr_sugars_of_global: theory -> ctr_sugar list val ctr_sugar_of_case: Proof.context -> string -> ctr_sugar option val ctr_sugar_of_case_global: theory -> string -> ctr_sugar option - val ctr_sugar_interpretation: string -> - (ctr_sugar -> local_theory -> local_theory) -> theory -> theory + val ctr_sugar_interpretation: string -> (ctr_sugar -> local_theory -> local_theory) -> theory -> + theory val interpret_ctr_sugar: (string -> bool) -> ctr_sugar -> local_theory -> local_theory val register_ctr_sugar_raw: ctr_sugar -> local_theory -> local_theory val register_ctr_sugar: (string -> bool) -> ctr_sugar -> local_theory -> local_theory diff -r 49353865e539 -r 1647bb489522 src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML Mon Nov 30 19:12:08 2015 +0100 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML Tue Dec 01 13:07:40 2015 +0100 @@ -54,7 +54,8 @@ fun mk_nchotomy_tac ctxt n exhaust = HEADGOAL (rtac ctxt allI THEN' rtac ctxt exhaust THEN' - EVERY' (maps (fn k => [rtac ctxt (mk_disjIN n k), REPEAT_DETERM o rtac ctxt exI, assume_tac ctxt]) + EVERY' (maps (fn k => + [rtac ctxt (mk_disjIN n k), REPEAT_DETERM o rtac ctxt exI, assume_tac ctxt]) (1 upto n))); fun mk_unique_disc_def_tac ctxt m uexhaust = @@ -114,7 +115,8 @@ else let val ks = 1 upto n in HEADGOAL (rtac ctxt uexhaust_disc THEN' - EVERY' (@{map 5} (fn k => fn m => fn distinct_discss => fn distinct_discss' => fn uuncollapse => + EVERY' (@{map 5} (fn k => fn m => fn distinct_discss => fn distinct_discss' => + fn uuncollapse => EVERY' [rtac ctxt (uuncollapse RS trans) THEN' TRY o assume_tac ctxt, rtac ctxt sym, rtac ctxt vexhaust_disc, EVERY' (@{map 4} (fn k' => fn distinct_discs => fn distinct_discs' => fn vuncollapse => @@ -124,13 +126,17 @@ (if m = 0 then [rtac ctxt refl] else - [if n = 1 then K all_tac - else EVERY' [dtac ctxt meta_mp, assume_tac ctxt, dtac ctxt meta_mp, assume_tac ctxt], - REPEAT_DETERM_N (Int.max (0, m - 1)) o etac ctxt conjE, - asm_simp_tac (ss_only [] ctxt)]) + [if n = 1 then + K all_tac + else + EVERY' [dtac ctxt meta_mp, assume_tac ctxt, dtac ctxt meta_mp, + assume_tac ctxt], + REPEAT_DETERM_N (Int.max (0, m - 1)) o etac ctxt conjE, + asm_simp_tac (ss_only [] ctxt)]) else [dtac ctxt (the_single (if k = n then distinct_discs else distinct_discs')), - etac ctxt (if k = n then @{thm iff_contradict(1)} else @{thm iff_contradict(2)}), + etac ctxt (if k = n then @{thm iff_contradict(1)} + else @{thm iff_contradict(2)}), assume_tac ctxt, assume_tac ctxt])) ks distinct_discss distinct_discss' uncollapses)]) ks ms distinct_discsss distinct_discsss' uncollapses)) @@ -152,8 +158,8 @@ val ks = 1 upto n; in HEADGOAL (rtac ctxt (case_def' RS trans) THEN' rtac ctxt @{thm the_equality} THEN' - rtac ctxt (mk_disjIN n k) THEN' REPEAT_DETERM o rtac ctxt exI THEN' rtac ctxt conjI THEN' rtac ctxt refl THEN' - rtac ctxt refl THEN' + rtac ctxt (mk_disjIN n k) THEN' REPEAT_DETERM o rtac ctxt exI THEN' rtac ctxt conjI THEN' + rtac ctxt refl THEN' rtac ctxt refl THEN' EVERY' (map2 (fn k' => fn distincts => (if k' < n then etac ctxt disjE else K all_tac) THEN' (if k' = k then mk_case_same_ctr_tac ctxt injects @@ -182,7 +188,8 @@ 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 (etac ctxt thin_rl THEN' rtac ctxt iffI THEN' - REPEAT_DETERM o rtac ctxt allI THEN' rtac ctxt impI THEN' REPEAT_DETERM o etac ctxt conjE THEN' + REPEAT_DETERM o rtac ctxt allI THEN' rtac ctxt impI THEN' + REPEAT_DETERM o etac ctxt conjE THEN' hyp_subst_tac ctxt THEN' assume_tac ctxt THEN' REPEAT_DETERM o etac ctxt allE THEN' etac ctxt impE THEN' REPEAT_DETERM o (rtac ctxt conjI THEN' rtac ctxt refl) THEN'