# HG changeset patch # User blanchet # Date 1393847300 -3600 # Node ID 79b915f265339df251463eb7eb32f17263f72dda # Parent a6fa341a6d667c373905bb7fee9fd8587909c9a2 rationalized internals diff -r a6fa341a6d66 -r 79b915f26533 NEWS --- a/NEWS Mon Mar 03 12:48:20 2014 +0100 +++ b/NEWS Mon Mar 03 12:48:20 2014 +0100 @@ -169,10 +169,12 @@ Option.set ~> set_option Option.map ~> map_option option_rel ~> rel_option + option_rec ~> case_option Renamed theorems: set_def ~> set_rec[abs_def] map_def ~> map_rec[abs_def] Option.map_def ~> map_option_case[abs_def] (with "case_option" instead of "rec_option") + option.recs ~> option.case list_all2_def ~> list_all2_iff set.simps ~> set_simps (or the slightly different "list.set") map.simps ~> list.map diff -r a6fa341a6d66 -r 79b915f26533 src/HOL/BNF_LFP.thy --- a/src/HOL/BNF_LFP.thy Mon Mar 03 12:48:20 2014 +0100 +++ b/src/HOL/BNF_LFP.thy Mon Mar 03 12:48:20 2014 +0100 @@ -264,10 +264,10 @@ hide_fact (open) id_transfer -datatype_new 'a F = F 'a +datatype_new 'a F = F0 | F 'a "'a F" datatype_compat F primrec f where - "f (F x) = x" + "f (F x y) = F x (f y)" end diff -r a6fa341a6d66 -r 79b915f26533 src/HOL/Nitpick_Examples/Refute_Nits.thy --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Mon Mar 03 12:48:20 2014 +0100 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Mon Mar 03 12:48:20 2014 +0100 @@ -585,20 +585,6 @@ nitpick [expect = genuine] oops -lemma "rec_option n s None = n" -nitpick [expect = none] -apply simp -done - -lemma "rec_option n s (Some x) = s x" -nitpick [expect = none] -apply simp -done - -lemma "P (rec_option n s x)" -nitpick [expect = genuine] -oops - lemma "P (case x of None \ n | Some u \ s u)" nitpick [expect = genuine] oops diff -r a6fa341a6d66 -r 79b915f26533 src/HOL/Option.thy --- a/src/HOL/Option.thy Mon Mar 03 12:48:20 2014 +0100 +++ b/src/HOL/Option.thy Mon Mar 03 12:48:20 2014 +0100 @@ -28,7 +28,6 @@ setup {* Sign.mandatory_path "option" *} lemmas inducts = option.induct -lemmas recs = option.rec lemmas cases = option.case setup {* Sign.parent_path *} diff -r a6fa341a6d66 -r 79b915f26533 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Mar 03 12:48:20 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Mar 03 12:48:20 2014 +0100 @@ -56,34 +56,34 @@ val morph_gfp_sugar_thms: morphism -> gfp_sugar_thms -> gfp_sugar_thms val transfer_gfp_sugar_thms: Proof.context -> gfp_sugar_thms -> gfp_sugar_thms - val mk_co_iters_prelims: BNF_Util.fp_kind -> typ list list list -> typ list -> typ list -> - typ list -> typ list -> int list -> int list list -> term list list -> Proof.context -> - (term list list * (typ list list * typ list list list list * term list list - * term list list list list) option + val mk_co_recs_prelims: BNF_Util.fp_kind -> typ list list list -> typ list -> typ list -> + typ list -> typ list -> int list -> int list list -> term list -> Proof.context -> + (term list + * (typ list list * typ list list list list * term list list * term list list list list) option * (string * term list * term list list - * ((term list list * term list list list) * typ list)) option) + * ((term list list * term list list list) * typ list)) option) * Proof.context val repair_nullary_single_ctr: typ list list -> typ list list - val mk_coiter_p_pred_types: typ list -> int list -> typ list list - val mk_coiter_fun_arg_types: typ list list list -> typ list -> typ list -> typ list -> int list -> + val mk_corec_p_pred_types: typ list -> int list -> typ list list + val mk_corec_fun_arg_types: typ list list list -> typ list -> typ list -> typ list -> int list -> int list list -> term -> typ list list * (typ list list list list * typ list list list * typ list list list list * typ list) - val define_iter: + val define_rec: (typ list list * typ list list list list * term list list * term list list list list) option -> (string -> binding) -> typ list -> typ list -> term list -> term -> Proof.context -> (term * thm) * Proof.context - val define_coiter: 'a * term list * term list list + val define_corec: 'a * term list * term list list * ((term list list * term list list list) * typ list) -> (string -> binding) -> 'b list -> typ list -> term list -> term -> Proof.context -> (term * thm) * local_theory - val derive_induct_iters_thms_for_types: BNF_Def.bnf list -> - ('a * typ list list list list * term list list * 'b) option -> thm -> thm list list -> + val derive_induct_recs_thms_for_types: BNF_Def.bnf list -> + ('a * typ list list list list * term list list * 'b) option -> thm -> thm list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> typ list -> typ list list list -> thm list -> thm list -> thm list -> term list list -> thm list list -> term list -> thm list -> Proof.context -> lfp_sugar_thms - val derive_coinduct_coiters_thms_for_types: BNF_Def.bnf list -> + val derive_coinduct_corecs_thms_for_types: BNF_Def.bnf list -> string * term list * term list list * ((term list list * term list list list) * typ list) -> - thm -> thm list -> thm list -> thm list list -> BNF_Def.bnf list -> typ list -> typ list -> + thm -> thm list -> thm list -> thm list -> BNF_Def.bnf list -> typ list -> typ list -> typ list -> typ list list list -> int list list -> int list list -> int list -> thm list -> thm list -> (thm -> thm) -> thm list list -> Ctr_Sugar.ctr_sugar list -> term list -> thm list -> (thm list -> thm list) -> local_theory -> gfp_sugar_thms @@ -254,7 +254,7 @@ val mk_ctor = mk_ctor_or_dtor range_type; val mk_dtor = mk_ctor_or_dtor domain_type; -fun mk_co_iters thy fp fpTs Cs ts0 = +fun mk_xtor_co_recs thy fp fpTs Cs ts0 = let val nn = length fpTs; val (fpTs0, Cs0) = @@ -318,9 +318,9 @@ type lfp_sugar_thms = (thm list * thm * Args.src list) * (thm list list * Args.src list); -fun morph_lfp_sugar_thms phi ((inducts, induct, induct_attrs), (recss, iter_attrs)) = +fun morph_lfp_sugar_thms phi ((inducts, induct, induct_attrs), (recss, rec_attrs)) = ((map (Morphism.thm phi) inducts, Morphism.thm phi induct, induct_attrs), - (map (map (Morphism.thm phi)) recss, iter_attrs)) + (map (map (Morphism.thm phi)) recss, rec_attrs)) : lfp_sugar_thms; val transfer_lfp_sugar_thms = @@ -334,48 +334,43 @@ * (thm list list list * Args.src list); fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs), - (corecss, coiter_attrs), (disc_corecss, disc_iter_attrs), - (disc_corec_iffss, disc_iter_iff_attrs), (sel_corecsss, sel_iter_attrs)) = + (corecss, corec_attrs), (disc_corecss, disc_rec_attrs), + (disc_corec_iffss, disc_rec_iff_attrs), (sel_corecsss, sel_rec_attrs)) = ((map (apfst (map (Morphism.thm phi)) o apsnd (Morphism.thm phi)) coinducts_pairs, coinduct_attrs), - (map (map (Morphism.thm phi)) corecss, coiter_attrs), - (map (map (Morphism.thm phi)) disc_corecss, disc_iter_attrs), - (map (map (Morphism.thm phi)) disc_corec_iffss, disc_iter_iff_attrs), - (map (map (map (Morphism.thm phi))) sel_corecsss, sel_iter_attrs)) : gfp_sugar_thms; + (map (map (Morphism.thm phi)) corecss, corec_attrs), + (map (map (Morphism.thm phi)) disc_corecss, disc_rec_attrs), + (map (map (Morphism.thm phi)) disc_corec_iffss, disc_rec_iff_attrs), + (map (map (map (Morphism.thm phi))) sel_corecsss, sel_rec_attrs)) : gfp_sugar_thms; val transfer_gfp_sugar_thms = morph_gfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of; -fun mk_iters_args_types ctr_Tsss Cs absTs repTs ns mss ctor_iter_fun_Tss lthy = +fun mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss ctor_rec_fun_Ts lthy = let val Css = map2 replicate ns Cs; - val y_Tsss = map5 (fn absT => fn repT => fn n => fn ms => - dest_absumprodT absT repT n ms o domain_type) - absTs repTs ns mss (map un_fold_of ctor_iter_fun_Tss); - val z_Tssss = - map6 (fn absT => fn repT => fn n => fn ms => fn ctr_Tss => fn ctor_iter_fun_Ts => + map6 (fn absT => fn repT => fn n => fn ms => fn ctr_Tss => fn ctor_rec_fun_T => map2 (map2 unzip_recT) - ctr_Tss (dest_absumprodT absT repT n ms (domain_type (co_rec_of ctor_iter_fun_Ts)))) - absTs repTs ns mss ctr_Tsss ctor_iter_fun_Tss; + ctr_Tss (dest_absumprodT absT repT n ms (domain_type ctor_rec_fun_T))) + absTs repTs ns mss ctr_Tsss ctor_rec_fun_Ts; val z_Tsss' = map (map flat_rec_arg_args) z_Tssss; val h_Tss = map2 (map2 (curry (op --->))) z_Tsss' Css; - val (((hss, ysss), zssss), lthy) = + val ((hss, zssss), lthy) = lthy |> mk_Freess "f" h_Tss - ||>> mk_Freesss "x" (*###*)y_Tsss - ||>> mk_Freessss "y" z_Tssss; + ||>> mk_Freessss "x" z_Tssss; in ((h_Tss, z_Tssss, hss, zssss), lthy) end; -(*avoid "'a itself" arguments in coiterators*) +(*avoid "'a itself" arguments in corecursors*) fun repair_nullary_single_ctr [[]] = [[@{typ unit}]] | repair_nullary_single_ctr Tss = Tss; -fun mk_coiter_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss fun_Ts = +fun mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss fun_Ts = let val ctr_Tsss' = map repair_nullary_single_ctr ctr_Tsss; val f_absTs = map range_type fun_Ts; @@ -387,27 +382,19 @@ (q_Tssss, f_Tsss, f_Tssss, f_absTs) end; -fun mk_coiter_p_pred_types Cs ns = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_pred1T) ns Cs; +fun mk_corec_p_pred_types Cs ns = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_pred1T) ns Cs; -fun mk_coiter_fun_arg_types ctr_Tsss Cs absTs repTs ns mss dtor_coiter = - (mk_coiter_p_pred_types Cs ns, - mk_coiter_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss - (binder_fun_types (fastype_of dtor_coiter))); - -fun mk_coiters_args_types ctr_Tsss Cs absTs repTs ns mss dtor_coiter_fun_Tss lthy = - let - val p_Tss = mk_coiter_p_pred_types Cs ns; +fun mk_corec_fun_arg_types ctr_Tsss Cs absTs repTs ns mss dtor_corec = + (mk_corec_p_pred_types Cs ns, + mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss + (binder_fun_types (fastype_of dtor_corec))); - fun mk_types get_Ts = - let - val fun_Ts = map get_Ts dtor_coiter_fun_Tss; - val (q_Tssss, f_Tsss, f_Tssss, f_repTs) = - mk_coiter_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss fun_Ts; - in - (q_Tssss, f_Tsss, f_Tssss, f_repTs) - end; +fun mk_corecs_args_types ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts lthy = + let + val p_Tss = mk_corec_p_pred_types Cs ns; - val (s_Tssss, h_Tsss, h_Tssss, corec_types) = mk_types co_rec_of; + val (s_Tssss, h_Tsss, h_Tssss, corec_types) = + mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts; val (((((Free (z, _), cs), pss), sssss), hssss), lthy) = lthy @@ -421,8 +408,8 @@ fun build_sum_inj mk_inj = build_map lthy (uncurry mk_inj o dest_sumT o snd); - fun build_dtor_coiter_arg _ [] [cf] = cf - | build_dtor_coiter_arg T [cq] [cf, cf'] = + fun build_dtor_corec_arg _ [] [cf] = cf + | build_dtor_corec_arg T [cq] [cf, cf'] = mk_If cq (build_sum_inj Inl_const (fastype_of cf, T) $ cf) (build_sum_inj Inr_const (fastype_of cf', T) $ cf'); @@ -431,7 +418,7 @@ val pfss = map3 flat_corec_preds_predsss_gettersss pss qssss fssss; val cqssss = map2 (map o map o map o rapp) cs qssss; val cfssss = map2 (map o map o map o rapp) cs fssss; - val cqfsss = map3 (map3 (map3 build_dtor_coiter_arg)) f_Tsss cqssss cfssss; + val cqfsss = map3 (map3 (map3 build_dtor_corec_arg)) f_Tsss cqssss cfssss; in (pfss, cqfsss) end; val corec_args = mk_args sssss hssss h_Tsss; @@ -439,28 +426,26 @@ ((z, cs, cpss, (corec_args, corec_types)), lthy) end; -fun mk_co_iters_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_iterss0 lthy = +fun mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy = let val thy = Proof_Context.theory_of lthy; val nn = length fpTs; - val (xtor_co_iter_fun_Tss, xtor_co_iterss) = - map (mk_co_iters thy fp fpTs Cs #> `(binder_fun_types o fastype_of o hd)) - (transpose xtor_co_iterss0) - |> apsnd transpose o apfst transpose o split_list; + val (xtor_co_rec_fun_Ts, xtor_co_recs) = + mk_xtor_co_recs thy fp fpTs Cs xtor_co_recs0 |> `(binder_fun_types o fastype_of o hd); - val ((iters_args_types, coiters_args_types), lthy') = + val ((recs_args_types, corecs_args_types), lthy') = if fp = Least_FP then if nn = 1 andalso forall (forall (forall (not o exists_subtype_in fpTs))) ctr_Tsss then ((NONE, NONE), lthy) else - mk_iters_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_iter_fun_Tss lthy + mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts lthy |>> (rpair NONE o SOME) else - mk_coiters_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_iter_fun_Tss lthy + mk_corecs_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts lthy |>> (pair NONE o SOME); in - ((xtor_co_iterss, iters_args_types, coiters_args_types), lthy') + ((xtor_co_recs, recs_args_types, corecs_args_types), lthy') end; fun mk_preds_getterss_join c cps absT abs cqfss = @@ -471,7 +456,7 @@ Term.lambda c (mk_IfN absT cps ts) end; -fun define_co_iter fp fpT Cs b rhs lthy0 = +fun define_co_rec fp fpT Cs b rhs lthy0 = let val thy = Proof_Context.theory_of lthy0; @@ -490,32 +475,32 @@ ((cst', def'), lthy') end; -fun define_iter NONE _ _ _ _ _ = pair (Term.dummy, refl) - | define_iter (SOME (_, _, fss, xssss)) mk_binding fpTs Cs reps ctor_iter = +fun define_rec NONE _ _ _ _ _ = pair (Term.dummy, refl) + | define_rec (SOME (_, _, fss, xssss)) mk_binding fpTs Cs reps ctor_rec = let val nn = length fpTs; - val (ctor_iter_absTs, fpT) = strip_typeN nn (fastype_of ctor_iter) + val (ctor_rec_absTs, fpT) = strip_typeN nn (fastype_of ctor_rec) |>> map domain_type ||> domain_type; in - define_co_iter Least_FP fpT Cs (mk_binding recN) - (fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_iter, - map4 (fn ctor_iter_absT => fn rep => fn fs => fn xsss => - mk_case_absumprod ctor_iter_absT rep fs + define_co_rec Least_FP fpT Cs (mk_binding recN) + (fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_rec, + map4 (fn ctor_rec_absT => fn rep => fn fs => fn xsss => + mk_case_absumprod ctor_rec_absT rep fs (map (HOLogic.mk_tuple o map HOLogic.mk_tuple) xsss) (map flat_rec_arg_args xsss)) - ctor_iter_absTs reps fss xssss))) + ctor_rec_absTs reps fss xssss))) end; -fun define_coiter (_, cs, cpss, ((pfss, cqfsss), f_absTs)) mk_binding fpTs Cs abss dtor_coiter = +fun define_corec (_, cs, cpss, ((pfss, cqfsss), 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_coiter))); + val fpT = range_type (snd (strip_typeN nn (fastype_of dtor_corec))); in - define_co_iter Greatest_FP fpT Cs (mk_binding corecN) - (fold_rev (fold_rev Term.lambda) pfss (Term.list_comb (dtor_coiter, + define_co_rec Greatest_FP fpT Cs (mk_binding corecN) + (fold_rev (fold_rev Term.lambda) pfss (Term.list_comb (dtor_corec, map5 mk_preds_getterss_join cs cpss f_absTs abss cqfsss))) end; -fun derive_induct_iters_thms_for_types pre_bnfs rec_args_typess ctor_induct ctor_iter_thmss +fun derive_induct_recs_thms_for_types pre_bnfs rec_args_typess ctor_induct ctor_rec_thms nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses fp_type_definitions abs_inverses ctrss ctr_defss recs rec_defs lthy = let @@ -628,13 +613,13 @@ val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss; - fun mk_iter_thmss (_, x_Tssss, fss, _) iters iter_defs ctor_iter_thms = + fun mk_rec_thmss (_, x_Tssss, fss, _) recs rec_defs ctor_rec_thms = let - val fiters = map (lists_bmoc fss) iters; + val frecs = map (lists_bmoc fss) recs; - fun mk_goal fss fiter xctr f xs fxs = + fun mk_goal fss frec xctr f xs fxs = fold_rev (fold_rev Logic.all) (xs :: fss) - (mk_Trueprop_eq (fiter $ xctr, Term.list_comb (f, fxs))); + (mk_Trueprop_eq (frec $ xctr, Term.list_comb (f, fxs))); fun maybe_tick (T, U) u f = if try (fst o HOLogic.dest_prodT) U = SOME T then @@ -642,20 +627,20 @@ else f; - fun build_iter (x as Free (_, T)) U = + fun build_rec (x as Free (_, T)) U = if T = U then x else build_map lthy (indexify (perhaps (try (snd o HOLogic.dest_prodT)) o snd) Cs - (fn kk => fn TU => maybe_tick TU (nth us kk) (nth fiters kk))) (T, U) $ x; + (fn kk => fn TU => maybe_tick TU (nth us kk) (nth frecs kk))) (T, U) $ x; - val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_iter))) xsss x_Tssss; + val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_rec))) xsss x_Tssss; - val goalss = map5 (map4 o mk_goal fss) fiters xctrss fss xsss fxsss; + val goalss = map5 (map4 o mk_goal fss) frecs xctrss fss xsss fxsss; val tacss = - map4 (map ooo mk_iter_tac pre_map_defs (nested_map_idents @ nesting_map_idents) iter_defs) - ctor_iter_thms fp_abs_inverses abs_inverses ctr_defss; + map4 (map ooo mk_rec_tac pre_map_defs (nested_map_idents @ nesting_map_idents) rec_defs) + ctor_rec_thms fp_abs_inverses abs_inverses ctr_defss; fun prove goal tac = Goal.prove_sorry lthy [] [] goal (tac o #context) @@ -666,25 +651,23 @@ val rec_thmss = (case rec_args_typess of - SOME types => - mk_iter_thmss types recs rec_defs (map co_rec_of ctor_iter_thmss) + SOME types => mk_rec_thmss types recs rec_defs ctor_rec_thms | NONE => replicate nn []); in ((induct_thms, induct_thm, [induct_case_names_attr]), (rec_thmss, code_nitpicksimp_attrs @ simp_attrs)) end; -fun derive_coinduct_coiters_thms_for_types pre_bnfs (z, cs, cpss, - coiters_args_types as ((phss, cshsss), _)) - dtor_coinduct dtor_injects dtor_ctors dtor_coiter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss +fun derive_coinduct_corecs_thms_for_types pre_bnfs (z, cs, cpss, + corecs_args_types as ((phss, cshsss), _)) + dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list) corecs corec_defs export_args lthy = let - fun mk_ctor_dtor_coiter_thm dtor_inject dtor_ctor coiter = - iffD1 OF [dtor_inject, trans OF [coiter, dtor_ctor RS sym]]; + fun mk_ctor_dtor_corec_thm dtor_inject dtor_ctor corec = + iffD1 OF [dtor_inject, trans OF [corec, dtor_ctor RS sym]]; - val ctor_dtor_coiter_thmss = - map3 (map oo mk_ctor_dtor_coiter_thm) dtor_injects dtor_ctors dtor_coiter_thmss; + val ctor_dtor_corec_thms = map3 mk_ctor_dtor_corec_thm dtor_injects dtor_ctors dtor_corec_thms; val nn = length pre_bnfs; @@ -798,15 +781,15 @@ fun mk_maybe_not pos = not pos ? HOLogic.mk_not; - val fcoiterss' as [hcorecs] = - map2 (fn (pfss, _) => map (lists_bmoc pfss)) [fst coiters_args_types] [corecs]; + val fcorecss' as [hcorecs] = + map2 (fn (pfss, _) => map (lists_bmoc pfss)) [fst corecs_args_types] [corecs]; val corec_thmss = let - fun mk_goal pfss c cps fcoiter n k ctr m cfs' = + fun mk_goal pfss c cps fcorec n k ctr m cfs' = fold_rev (fold_rev Logic.all) ([c] :: pfss) (Logic.list_implies (seq_conds (HOLogic.mk_Trueprop oo mk_maybe_not) n k cps, - mk_Trueprop_eq (fcoiter $ c, Term.list_comb (ctr, take m cfs')))); + mk_Trueprop_eq (fcorec $ c, Term.list_comb (ctr, take m cfs')))); fun mk_U maybe_mk_sumT = typ_subst_nonatomic (map2 (fn C => fn fpT => (maybe_mk_sumT fpT C, fpT)) Cs fpTs); @@ -816,25 +799,25 @@ Term.lambda z (mk_case_sum (Term.lambda u u, Term.lambda c (f $ c)) $ z) end; - fun build_coiter fcoiters maybe_mk_sumT maybe_tack cqf = + fun build_corec fcorecs maybe_mk_sumT maybe_tack cqf = let val T = fastype_of cqf in if exists_subtype_in Cs T then let val U = mk_U maybe_mk_sumT T in build_map lthy (indexify fst (map2 maybe_mk_sumT fpTs Cs) (fn kk => fn _ => - maybe_tack (nth cs kk, nth us kk) (nth fcoiters kk))) (T, U) $ cqf + maybe_tack (nth cs kk, nth us kk) (nth fcorecs kk))) (T, U) $ cqf end else cqf end; - val cshsss' = map (map (map (build_coiter (co_rec_of fcoiterss') (curry mk_sumT) (tack z)))) + val cshsss' = map (map (map (build_corec (co_rec_of fcorecss') (curry mk_sumT) (tack z)))) cshsss; val goalss = map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss'; val tacss = - map4 (map ooo mk_coiter_tac corec_defs nesting_map_idents) - (map co_rec_of ctor_dtor_coiter_thmss) pre_map_defs abs_inverses ctr_defss; + map4 (map ooo mk_corec_tac corec_defs nesting_map_idents) + ctor_dtor_corec_thms pre_map_defs abs_inverses ctr_defss; fun prove goal tac = Goal.prove_sorry lthy [] [] goal (tac o #context) @@ -846,8 +829,8 @@ val disc_corec_iff_thmss = let - fun mk_goal c cps fcoiter n k disc = - mk_Trueprop_eq (disc $ (fcoiter $ c), + fun mk_goal c cps fcorec n k disc = + mk_Trueprop_eq (disc $ (fcorec $ c), if n = 1 then @{const True} else Library.foldr1 HOLogic.mk_conj (seq_conds mk_maybe_not n k cps)); @@ -857,7 +840,7 @@ val case_splitss' = map (map mk_case_split') cpss; - val tacss = map3 (map oo mk_disc_coiter_iff_tac) case_splitss' corec_thmss disc_thmsss; + val tacss = map3 (map oo mk_disc_corec_iff_tac) case_splitss' corec_thmss disc_thmsss; fun prove goal tac = Goal.prove_sorry lthy [] [] goal (tac o #context) @@ -871,11 +854,11 @@ map2 proves goalss tacss end; - fun mk_disc_coiter_thms coiters discIs = map (op RS) (coiters ~~ discIs); + fun mk_disc_corec_thms corecs discIs = map (op RS) (corecs ~~ discIs); - val disc_corec_thmss = map2 mk_disc_coiter_thms corec_thmss discIss; + val disc_corec_thmss = map2 mk_disc_corec_thms corec_thmss discIss; - fun mk_sel_coiter_thm coiter_thm sel sel_thm = + fun mk_sel_corec_thm corec_thm sel sel_thm = let val (domT, ranT) = dest_funT (fastype_of sel); val arg_cong' = @@ -884,13 +867,13 @@ |> Thm.varifyT_global; val sel_thm' = sel_thm RSN (2, trans); in - coiter_thm RS arg_cong' RS sel_thm' + corec_thm RS arg_cong' RS sel_thm' end; - fun mk_sel_coiter_thms coiter_thmss = - map3 (map3 (map2 o mk_sel_coiter_thm)) coiter_thmss selsss sel_thmsss; + fun mk_sel_corec_thms corec_thmss = + map3 (map3 (map2 o mk_sel_corec_thm)) corec_thmss selsss sel_thmsss; - val sel_corec_thmsss = mk_sel_coiter_thms corec_thmss; + val sel_corec_thmsss = mk_sel_corec_thms corec_thmss; val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn)); val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases)); @@ -1110,11 +1093,12 @@ val kss = map (fn n => 1 upto n) ns; val mss = map (map length) ctr_Tsss; - val ((xtor_co_iterss, iters_args_types, coiters_args_types), lthy') = - mk_co_iters_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_iterss0 lthy; + val ((xtor_co_recs, recs_args_types, corecs_args_types), lthy') = + mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss (map co_rec_of xtor_co_iterss0) + lthy; fun define_ctrs_dtrs_for_type (((((((((((((((((((((((((((fp_bnf, fp_b), fpT), ctor), dtor), - xtor_co_iters), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs), + xtor_co_rec), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs), pre_rel_def), fp_map_thm), fp_set_thms), fp_rel_thm), n), ks), ms), abs), abs_inject), abs_inverse), type_definition), ctr_bindings), ctr_mixfixes), ctr_Tss), disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy = @@ -1305,15 +1289,14 @@ fun mk_binding pre = Binding.qualify false fp_b_name (Binding.prefix_name (pre ^ "_") fp_b); - fun massage_res (((maps_sets_rels, ctr_sugar), co_iter_res), lthy) = - (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_sugar)), co_iter_res), lthy); + fun massage_res (((maps_sets_rels, ctr_sugar), co_rec_res), lthy) = + (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_sugar)), co_rec_res), lthy); in (wrap_ctrs #> derive_maps_sets_rels ##>> - (if fp = Least_FP then define_iter iters_args_types mk_binding fpTs Cs reps - else define_coiter (the coiters_args_types) mk_binding fpTs Cs abss) - (co_rec_of xtor_co_iters) + (if fp = Least_FP then define_rec recs_args_types mk_binding fpTs Cs reps + else define_corec (the corecs_args_types) mk_binding fpTs Cs abss) xtor_co_rec #> massage_res, lthy') end; @@ -1326,19 +1309,19 @@ rel_distincts setss = injects @ distincts @ case_thms @ co_recs @ mapsx @ rel_injects @ rel_distincts @ flat setss; - fun derive_note_induct_iters_thms_for_types + fun derive_note_induct_recs_thms_for_types ((((mapss, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)), (recs, rec_defs)), lthy) = let val ((induct_thms, induct_thm, induct_attrs), (rec_thmss, iter_attrs)) = - derive_induct_iters_thms_for_types pre_bnfs iters_args_types xtor_co_induct - xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss abs_inverses - type_definitions abs_inverses ctrss ctr_defss recs rec_defs lthy; + derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct + (map co_rec_of xtor_co_iter_thmss) nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss + abs_inverses type_definitions abs_inverses ctrss ctr_defss recs rec_defs lthy; val induct_type_attr = Attrib.internal o K o Induct.induct_type; val (recs', rec_thmss') = - if is_some iters_args_types then (recs, rec_thmss) + if is_some recs_args_types then (recs, rec_thmss) else (map #casex ctr_sugars, map #case_thms ctr_sugars); val simp_thmss = @@ -1355,7 +1338,7 @@ |> massage_multi_notes; in lthy - |> (if is_some iters_args_types then + |> (if is_some recs_args_types then Spec_Rules.add Spec_Rules.Equational (recs, flat rec_thmss) else I) @@ -1365,30 +1348,30 @@ rec_thmss' (replicate nn []) (replicate nn []) end; - fun derive_note_coinduct_coiters_thms_for_types + fun derive_note_coinduct_corecs_thms_for_types ((((mapss, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)), - (coiters, corec_defs)), lthy) = + (corecs, corec_defs)), lthy) = let val (([(coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)], coinduct_attrs), - (corec_thmss, coiter_attrs), - (disc_corec_thmss, disc_coiter_attrs), - (disc_corec_iff_thmss, disc_coiter_iff_attrs), - (sel_corec_thmsss, sel_coiter_attrs)) = - derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct - dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns - abs_inverses abs_inverses I ctr_defss ctr_sugars coiters corec_defs + (corec_thmss, corec_attrs), + (disc_corec_thmss, disc_corec_attrs), + (disc_corec_iff_thmss, disc_corec_iff_attrs), + (sel_corec_thmsss, sel_corec_attrs)) = + derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct + dtor_injects dtor_ctors (map co_rec_of xtor_co_iter_thmss) nesting_bnfs fpTs Cs Xs + ctrXs_Tsss kss mss ns abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs (Proof_Context.export lthy' no_defs_lthy) lthy; val sel_corec_thmss = map flat sel_corec_thmsss; val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type; - val flat_coiter_thms = append oo append; + val flat_corec_thms = append oo append; val simp_thmss = map6 mk_simp_thms ctr_sugars - (map3 flat_coiter_thms disc_corec_thmss disc_corec_iff_thmss sel_corec_thmss) + (map3 flat_corec_thms disc_corec_thmss disc_corec_iff_thmss sel_corec_thmss) mapss rel_injects rel_distincts setss; val common_notes = @@ -1402,35 +1385,34 @@ val notes = [(coinductN, map single coinduct_thms, fn T_name => coinduct_attrs @ [coinduct_type_attr T_name]), - (corecN, corec_thmss, K coiter_attrs), - (disc_corecN, disc_corec_thmss, K disc_coiter_attrs), - (disc_corec_iffN, disc_corec_iff_thmss, K disc_coiter_iff_attrs), - (sel_corecN, sel_corec_thmss, K sel_coiter_attrs), + (corecN, corec_thmss, K corec_attrs), + (disc_corecN, disc_corec_thmss, K disc_corec_attrs), + (disc_corec_iffN, disc_corec_iff_thmss, K disc_corec_iff_attrs), + (sel_corecN, sel_corec_thmss, K sel_corec_attrs), (simpsN, simp_thmss, K []), (strong_coinductN, map single strong_coinduct_thms, K coinduct_attrs)] |> massage_multi_notes; in lthy (* TODO: code theorems *) - |> fold (curry (Spec_Rules.add Spec_Rules.Equational) coiters) + |> fold (curry (Spec_Rules.add Spec_Rules.Equational) corecs) [flat sel_corec_thmss, flat corec_thmss] |> Local_Theory.notes (common_notes @ notes) |> snd |> register_fp_sugars Xs Greatest_FP pre_bnfs absT_infos nested_bnfs nesting_bnfs fp_res - ctrXs_Tsss ctr_defss ctr_sugars coiters mapss [coinduct_thm, strong_coinduct_thm] + ctrXs_Tsss ctr_defss ctr_sugars corecs mapss [coinduct_thm, strong_coinduct_thm] (transpose [coinduct_thms, strong_coinduct_thms]) corec_thmss disc_corec_thmss sel_corec_thmsss end; val lthy'' = lthy' |> fold_map define_ctrs_dtrs_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ ctors ~~ dtors ~~ - xtor_co_iterss ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~ - pre_set_defss ~~ pre_rel_defs ~~ xtor_map_thms ~~ xtor_set_thmss ~~ xtor_rel_thms ~~ ns ~~ - kss ~~ mss ~~ abss ~~ abs_injects ~~ abs_inverses ~~ type_definitions ~~ - ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ - raw_sel_defaultsss) + xtor_co_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~ pre_set_defss ~~ + pre_rel_defs ~~ xtor_map_thms ~~ xtor_set_thmss ~~ xtor_rel_thms ~~ ns ~~ kss ~~ mss ~~ + abss ~~ abs_injects ~~ abs_inverses ~~ type_definitions ~~ ctr_bindingss ~~ ctr_mixfixess ~~ + ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_defaultsss) |> wrap_types_etc - |> fp_case fp derive_note_induct_iters_thms_for_types - derive_note_coinduct_coiters_thms_for_types; + |> fp_case fp derive_note_induct_recs_thms_for_types + derive_note_coinduct_corecs_thms_for_types; val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^ co_prefix fp ^ "datatype")); diff -r a6fa341a6d66 -r 79b915f26533 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Mon Mar 03 12:48:20 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Mon Mar 03 12:48:20 2014 +0100 @@ -14,16 +14,16 @@ val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list -> thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list -> thm list list list -> tactic - val mk_coiter_tac: thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic + val mk_corec_tac: thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm -> tactic - val mk_disc_coiter_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic + val mk_disc_corec_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic val mk_half_distinct_tac: Proof.context -> thm -> thm -> thm list -> tactic val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list -> thm list -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic - val mk_iter_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> + val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic end; @@ -87,32 +87,32 @@ unfold_thms_tac ctxt (abs_inject :: @{thms sum.inject Pair_eq conj_assoc}) THEN HEADGOAL (rtac refl); -val iter_unfold_thms = +val rec_unfold_thms = @{thms comp_def convol_def fst_conv id_def case_prod_Pair_iden snd_conv split_conv case_unit_Unity} @ sum_prod_thms_map; -fun mk_iter_tac pre_map_defs map_idents iter_defs ctor_iter fp_abs_inverse abs_inverse ctr_def ctxt = - unfold_thms_tac ctxt (ctr_def :: ctor_iter :: fp_abs_inverse :: abs_inverse :: iter_defs @ - pre_map_defs @ map_idents @ iter_unfold_thms) THEN HEADGOAL (rtac refl); +fun mk_rec_tac pre_map_defs map_idents rec_defs ctor_rec fp_abs_inverse abs_inverse ctr_def ctxt = + unfold_thms_tac ctxt (ctr_def :: ctor_rec :: fp_abs_inverse :: abs_inverse :: rec_defs @ + pre_map_defs @ map_idents @ rec_unfold_thms) THEN HEADGOAL (rtac refl); -val coiter_unfold_thms = @{thms id_def} @ sum_prod_thms_map; +val corec_unfold_thms = @{thms id_def} @ sum_prod_thms_map; -fun mk_coiter_tac coiter_defs map_idents ctor_dtor_coiter pre_map_def abs_inverse ctr_def ctxt = +fun mk_corec_tac corec_defs map_idents ctor_dtor_corec pre_map_def abs_inverse ctr_def ctxt = let - val ss = ss_only (pre_map_def :: abs_inverse :: map_idents @ coiter_unfold_thms @ + val ss = ss_only (pre_map_def :: abs_inverse :: map_idents @ corec_unfold_thms @ @{thms o_apply vimage2p_def if_True if_False}) ctxt; in - unfold_thms_tac ctxt (ctr_def :: coiter_defs) THEN - HEADGOAL (rtac (ctor_dtor_coiter RS trans) THEN' asm_simp_tac ss) THEN_MAYBE + unfold_thms_tac ctxt (ctr_def :: corec_defs) THEN + HEADGOAL (rtac (ctor_dtor_corec RS trans) THEN' asm_simp_tac ss) THEN_MAYBE HEADGOAL (rtac refl ORELSE' rtac (@{thm unit_eq} RS arg_cong)) end; -fun mk_disc_coiter_iff_tac case_splits' coiters discs ctxt = - EVERY (map3 (fn case_split_tac => fn coiter_thm => fn disc => - HEADGOAL case_split_tac THEN unfold_thms_tac ctxt [coiter_thm] THEN +fun mk_disc_corec_iff_tac case_splits' corecs discs ctxt = + EVERY (map3 (fn case_split_tac => fn corec_thm => fn disc => + HEADGOAL case_split_tac THEN unfold_thms_tac ctxt [corec_thm] THEN HEADGOAL (asm_simp_tac (ss_only basic_simp_thms ctxt)) THEN (if is_refl disc then all_tac else HEADGOAL (rtac disc))) - (map rtac case_splits' @ [K all_tac]) coiters discs); + (map rtac case_splits' @ [K all_tac]) corecs discs); fun solve_prem_prem_tac ctxt = REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE' diff -r a6fa341a6d66 -r 79b915f26533 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Mar 03 12:48:20 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Mar 03 12:48:20 2014 +0100 @@ -240,31 +240,33 @@ val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As; val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs; - val ((xtor_co_iterss, iters_args_types, coiters_args_types), _) = - mk_co_iters_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_iterss0 lthy; + val xtor_co_rec_thms = map co_rec_of xtor_co_iter_thmss; + val ((xtor_co_recs, recs_args_types, corecs_args_types), _) = + mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss (map co_rec_of xtor_co_iterss0) + lthy; fun mk_binding b suf = Binding.suffix_name ("_" ^ suf) b; val ((co_recs, co_rec_defs), lthy) = fold_map2 (fn b => - if fp = Least_FP then define_iter iters_args_types (mk_binding b) fpTs Cs reps - else define_coiter (the coiters_args_types) (mk_binding b) fpTs Cs abss) - fp_bs (map co_rec_of xtor_co_iterss) lthy + if fp = Least_FP then define_rec recs_args_types (mk_binding b) fpTs Cs reps + else define_corec (the corecs_args_types) (mk_binding b) fpTs Cs abss) + fp_bs xtor_co_recs lthy |>> split_list; val ((common_co_inducts, co_inductss, co_rec_thmss, disc_corec_thmss, sel_corec_thmsss), fp_sugar_thms) = if fp = Least_FP then - derive_induct_iters_thms_for_types pre_bnfs iters_args_types xtor_co_induct - xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses + derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct + xtor_co_rec_thms nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses fp_type_definitions abs_inverses ctrss ctr_defss co_recs co_rec_defs lthy |> `(fn ((inducts, induct, _), (rec_thmss, _)) => ([induct], [inducts], rec_thmss, replicate nn [], replicate nn [])) ||> (fn info => (SOME info, NONE)) else - derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct - dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss - ns fp_abs_inverses abs_inverses (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss + derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct + dtor_injects dtor_ctors xtor_co_rec_thms nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns + fp_abs_inverses abs_inverses (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss ctr_sugars co_recs co_rec_defs (Proof_Context.export lthy no_defs_lthy) lthy |> `(fn ((coinduct_thms_pairs, _), (corec_thmss, _), (disc_corec_thmss, _), _, (sel_corec_thmsss, _)) => diff -r a6fa341a6d66 -r 79b915f26533 src/HOL/ex/Refute_Examples.thy --- a/src/HOL/ex/Refute_Examples.thy Mon Mar 03 12:48:20 2014 +0100 +++ b/src/HOL/ex/Refute_Examples.thy Mon Mar 03 12:48:20 2014 +0100 @@ -547,18 +547,6 @@ refute [expect = genuine] oops -lemma "rec_option n s None = n" -refute [expect = none] -by simp - -lemma "rec_option n s (Some x) = s x" -refute [maxsize = 4, expect = none] -by simp - -lemma "P (rec_option n s x)" -refute [expect = genuine] -oops - lemma "P (case x of None \ n | Some u \ s u)" refute [expect = genuine] oops