# HG changeset patch # User desharna # Date 1403610494 -7200 # Node ID 498a62e65f5fd04e7a5e1c302dd452d71b44830b # Parent 58f02fbaa76459fe62420725755f035281d0084e tune the implementation of 'rel_coinduct' diff -r 58f02fbaa764 -r 498a62e65f5f src/HOL/BNF_FP_Base.thy --- a/src/HOL/BNF_FP_Base.thy Tue Jun 24 13:48:14 2014 +0200 +++ b/src/HOL/BNF_FP_Base.thy Tue Jun 24 13:48:14 2014 +0200 @@ -16,7 +16,7 @@ lemma mp_conj: "(P \ Q) \ R \ P \ R \ Q" by auto -lemma predicate2D_conj: "(P \ Q) \ R \ P x y \ R \ Q x y" +lemma predicate2D_conj: "P \ Q \ R \ P x y \ R \ Q x y" by auto lemma eq_sym_Unity_conv: "(x = (() = ())) = x" diff -r 58f02fbaa764 -r 498a62e65f5f src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Tue Jun 24 13:48:14 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_def.ML Tue Jun 24 13:48:14 2014 +0200 @@ -83,9 +83,8 @@ val mk_map: int -> typ list -> typ list -> term -> term val mk_rel: int -> typ list -> typ list -> term -> term - val build_map: Proof.context -> (typ * typ -> term) -> typ * typ -> term - val build_rel: Proof.context -> (typ * typ -> term) -> typ * typ -> term - val build_rel': Proof.context -> typ list -> (typ * typ -> term) -> typ * typ -> term + val build_map: Proof.context -> typ list -> (typ * typ -> term) -> typ * typ -> term + val build_rel: Proof.context -> typ list -> (typ * typ -> term) -> typ * typ -> term val flatten_type_args_of_bnf: bnf -> 'a -> 'a list -> 'a list val map_flattened_map_args: Proof.context -> string -> (term list -> 'a list) -> term list -> 'a list @@ -534,12 +533,12 @@ Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t end; -fun build_map_or_rel mk const of_bnf dest blacklist ctxt build_simple = +fun build_map_or_rel mk const of_bnf dest ctxt simpleTs build_simple = let fun build (TU as (T, U)) = - if exists (curry (op =) T) blacklist then + if exists (curry (op =) T) simpleTs then build_simple TU - else if T = U andalso not (exists_subtype_in blacklist T) then + else if T = U andalso not (exists_subtype_in simpleTs T) then const T else (case TU of @@ -556,9 +555,8 @@ | _ => build_simple TU); in build end; -val build_map = build_map_or_rel mk_map HOLogic.id_const map_of_bnf dest_funT []; -val build_rel = build_map_or_rel mk_rel HOLogic.eq_const rel_of_bnf dest_pred2T []; -fun build_rel' ctxt blacklist = build_map_or_rel mk_rel HOLogic.eq_const rel_of_bnf dest_pred2T blacklist ctxt; +val build_map = build_map_or_rel mk_map HOLogic.id_const map_of_bnf dest_funT; +val build_rel = build_map_or_rel mk_rel HOLogic.eq_const rel_of_bnf dest_pred2T; fun map_flattened_map_args ctxt s map_args fs = let diff -r 58f02fbaa764 -r 498a62e65f5f src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Jun 24 13:48:14 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Jun 24 13:48:14 2014 +0200 @@ -359,7 +359,7 @@ val cpss = map2 (map o rapp) cs pss; - fun build_sum_inj mk_inj = build_map lthy (uncurry mk_inj o dest_sumT o snd); + fun build_sum_inj mk_inj = build_map lthy [] (uncurry mk_inj o dest_sumT o snd); fun build_dtor_corec_arg _ [] [cg] = cg | build_dtor_corec_arg T [cq] [cg, cg'] = @@ -574,7 +574,7 @@ if T = U then x else - build_map lthy (indexify (perhaps (try (snd o HOLogic.dest_prodT)) o snd) Cs + 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 frecs kk))) (T, U) $ x; val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_rec))) xsss x_Tssss; @@ -634,6 +634,14 @@ (coinduct_attrs, common_coinduct_attrs) end; +fun postproc_coinduct nn prop prop_conj = + Drule.zero_var_indexes + #> `(conj_dests nn) + #>> map (fn thm => Thm.permute_prems 0 nn (thm RS prop)) + ##> (fn thm => Thm.permute_prems 0 nn + (if nn = 1 then thm RS prop + else funpow nn (fn thm => reassoc_conjs (thm RS prop_conj)) thm)); + fun derive_rel_coinduct0_thm_for_types lthy fpA_Ts ns As Bs mss ctr_sugars abs_inverses abs_injects ctor_injects dtor_ctors rel_pre_defs ctor_defss dtor_rel_coinduct = let @@ -666,18 +674,12 @@ (mk_discss fpBs Bs, mk_selsss fpBs Bs)) end; - fun choose_relator (A, B) = the (find_first (fn t => - let - val T = fastype_of t - val arg1T = domain_type T; - val arg2T = domain_type (range_type T); - in - A = arg1T andalso B = arg2T - end) (Rs @ IRs)); + fun choose_relator AB = the (find_first + (fastype_of #> binder_types #> (fn [T1, T2] => AB = (T1, T2))) (Rs @ IRs)); val premises = let - fun build_the_rel A B = build_rel' lthy fpA_Ts choose_relator (A, B); + fun build_the_rel A B = build_rel lthy fpA_Ts choose_relator (A, B); fun build_rel_app selA_t selB_t = (build_the_rel (fastype_of selA_t) (fastype_of selB_t )) $ selA_t $ selB_t @@ -685,7 +687,7 @@ fun mk_prem_ctr_concls n k discA_t selA_ts discB_t selB_ts = (if k = n then [] else [HOLogic.mk_eq (discA_t, discB_t)]) @ (case (selA_ts, selB_ts) of - ([],[]) => [] + ([], []) => [] | (_ :: _, _ :: _) => [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [discA_t, discB_t], Library.foldr1 HOLogic.mk_conj (map2 build_rel_app selA_ts selB_ts))]); @@ -703,36 +705,19 @@ end; val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map2 mk_leq IRs (map (build_rel lthy choose_relator) (fpA_Ts ~~ fpB_Ts)))); - - (* - fun string_of_list f Ts = "[" ^ (fold_rev (curry op ^) (separate ", " (map f Ts)) "") ^ "]" - val _ = writeln ("Premises: " ^ string_of_list (Syntax.string_of_term names_lthy) premises) - val _ = writeln ("Goal: " ^ Syntax.string_of_term names_lthy goal) - val _ = writeln ("derive_rel_coinduct0_thm_for_types " ^ string_of_list (Syntax.string_of_typ names_lthy) fpA_Ts) - *) + (map2 mk_leq IRs (map (build_rel lthy [] choose_relator) (fpA_Ts ~~ fpB_Ts)))); val rel_coinduct0_thm = Goal.prove_sorry lthy [] premises goal (fn {context = ctxt, prems = prems} => mk_rel_coinduct0_tac ctxt dtor_rel_coinduct (map (certify ctxt) IRs) prems - (map #exhaust ctr_sugars) (map (flat o #disc_thmss) ctr_sugars) (map (flat o #sel_thmss) - ctr_sugars) ctor_defss dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses) + (map #exhaust ctr_sugars) (map (flat o #disc_thmss) ctr_sugars) + (map (flat o #sel_thmss) ctr_sugars) ctor_defss dtor_ctors ctor_injects abs_injects + rel_pre_defs abs_inverses) |> singleton (Proof_Context.export names_lthy lthy) |> Thm.close_derivation; - - val nn = length fpA_Ts; - val predicate2D = @{thm predicate2D}; - val predicate2D_conj = @{thm predicate2D_conj}; - - val postproc = - Drule.zero_var_indexes - #> `(conj_dests nn) - #>> map (fn thm => Thm.permute_prems 0 nn (thm RS predicate2D)) - ##> (fn thm => Thm.permute_prems 0 nn - (if nn = 1 then thm RS predicate2D - else funpow nn (fn thm => reassoc_conjs (thm RS predicate2D_conj)) thm)); in - (postproc rel_coinduct0_thm, coinduct_attrs fpA_Ts ctr_sugars mss) + (postproc_coinduct (length fpA_Ts) @{thm predicate2D} @{thm predicate2D_conj} rel_coinduct0_thm, + coinduct_attrs fpA_Ts ctr_sugars mss) end; fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, ((pgss, cqgsss), _)) @@ -785,7 +770,7 @@ fold_rev Term.lambda [u, v] (HOLogic.mk_disj (uvr, uv_eq))) us vs uvrs uv_eqs; fun build_the_rel rs' T Xs_T = - build_rel lthy (fn (_, X) => nth rs' (find_index (curry (op =) X) Xs)) (T, Xs_T) + build_rel lthy [] (fn (_, X) => nth rs' (find_index (curry (op =) X) Xs)) (T, Xs_T) |> Term.subst_atomic_types (Xs ~~ fpTs); fun build_rel_app rs' usel vsel Xs_T = @@ -826,20 +811,12 @@ |> singleton (Proof_Context.export names_lthy lthy) |> Thm.close_derivation; - val postproc = - Drule.zero_var_indexes - #> `(conj_dests nn) - #>> map (fn thm => Thm.permute_prems 0 nn (thm RS mp)) - ##> (fn thm => Thm.permute_prems 0 nn - (if nn = 1 then thm RS mp - else funpow nn (fn thm => reassoc_conjs (thm RS mp_conj)) thm)); - val rel_eqs = map rel_eq_of_bnf pre_bnfs; val rel_monos = map rel_mono_of_bnf pre_bnfs; val dtor_coinducts = [dtor_coinduct, mk_strong_coinduct_thm dtor_coinduct rel_eqs rel_monos mk_vimage2p lthy] in - map2 (postproc oo prove) dtor_coinducts goals + map2 (postproc_coinduct nn mp mp_conj oo prove) dtor_coinducts goals end; fun mk_maybe_not pos = not pos ? HOLogic.mk_not; @@ -864,7 +841,7 @@ let val T = fastype_of cqg in if exists_subtype_in Cs T then let val U = mk_U T in - build_map lthy (indexify fst (map2 (curry mk_sumT) fpTs Cs) (fn kk => fn _ => + build_map lthy [] (indexify fst (map2 (curry mk_sumT) fpTs Cs) (fn kk => fn _ => tack (nth cs kk, nth us kk) (nth gcorecs kk))) (T, U) $ cqg end else @@ -1336,7 +1313,7 @@ val lhs = selB $ (Term.list_comb (map_term, fs) $ ta); val lhsT = fastype_of lhs; val map_rhsT = map_atyps (perhaps (AList.lookup (op =) (Bs ~~ As))) lhsT; - val map_rhs = build_map lthy + val map_rhs = build_map lthy [] (the o (AList.lookup (op =) ((As ~~ Bs) ~~ fs))) (map_rhsT, lhsT); val rhs = (case map_rhs of Const (@{const_name id}, _) => selA $ ta @@ -1592,8 +1569,8 @@ val ((rel_coinduct_thms, rel_coinduct_thm), (rel_coinduct_attrs, common_rel_coinduct_attrs)) = - derive_rel_coinduct0_thm_for_types lthy fpTs ns As Bs mss ctr_sugars abs_inverses abs_injects - ctor_injects dtor_ctors pre_rel_defs ctr_defss rel_xtor_co_induct_thm; + derive_rel_coinduct0_thm_for_types lthy fpTs ns As Bs mss ctr_sugars abs_inverses + abs_injects ctor_injects dtor_ctors pre_rel_defs ctr_defss rel_xtor_co_induct_thm; val sel_corec_thmss = map flat sel_corec_thmsss; diff -r 58f02fbaa764 -r 498a62e65f5f src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Jun 24 13:48:14 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Jun 24 13:48:14 2014 +0200 @@ -44,6 +44,7 @@ val basic_simp_thms = @{thms simp_thms(7,8,12,14,22,24)}; val more_simp_thms = basic_simp_thms @ @{thms simp_thms(11,15,16,21)}; +val simp_thms' = @{thms simp_thms(6,7,8,11,12,15,16,22,24)}; val sumprod_thms_map = @{thms id_apply map_prod_simp prod.case sum.case map_sum.simps}; val sumprod_thms_set = @@ -218,12 +219,12 @@ arg_cong2}) RS iffD1)) THEN' atac THEN' atac THEN' hyp_subst_tac ctxt THEN' dtac assm THEN' REPEAT_DETERM o etac conjE))) 1 THEN - Local_Defs.unfold_tac ctxt ((discs RL @{thms iffD2[OF eq_True] iffD2[OF eq_False]}) @ - sels @ @{thms simp_thms(6,7,8,11,12,15,16,22,24)}) THEN + Local_Defs.unfold_tac ctxt ((discs RL @{thms iffD2[OF eq_True] iffD2[OF eq_False]}) @ sels + @ simp_thms') THEN Local_Defs.unfold_tac ctxt (dtor_ctor :: rel_pre_def :: abs_inverse :: ctor_inject :: - abs_inject :: ctor_defs @ @{thms BNF_Comp.id_bnf_comp_def rel_sum_simps rel_prod_apply - vimage2p_def Inl_Inr_False iffD2[OF eq_False Inr_not_Inl] sum.inject prod.inject - simp_thms(6,7,8,11,12,15,16,22,24)}) THEN + abs_inject :: ctor_defs @ simp_thms' @ @{thms BNF_Comp.id_bnf_comp_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 conjE) THEN' (REPEAT_DETERM o rtac conjI) THEN' (rtac refl ORELSE' atac)))) cts assms exhausts discss selss ctor_defss dtor_ctors ctor_injects abs_injects rel_pre_defs diff -r 58f02fbaa764 -r 498a62e65f5f src/HOL/Tools/BNF/bnf_fp_n2m.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Tue Jun 24 13:48:14 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Tue Jun 24 13:48:14 2014 +0200 @@ -340,11 +340,11 @@ val (TY, (U, X)) = TU |> dest_co_algT ||> dest_co_productT; val T = mk_co_algT TY U; in - (case try (force_typ names_lthy T o build_map lthy co_proj1_const o dest_funT) T of + (case try (force_typ names_lthy T o build_map lthy [] co_proj1_const o dest_funT) T of SOME f => mk_co_product f (fst (fst (mk_rec NONE recs lthy (mk_co_algT TY X)))) | NONE => mk_map_co_product - (build_map lthy co_proj1_const + (build_map lthy [] co_proj1_const (dest_funT (mk_co_algT (dest_co_productT TY |> fst) U))) (HOLogic.id_const X)) end) diff -r 58f02fbaa764 -r 498a62e65f5f src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Jun 24 13:48:14 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Jun 24 13:48:14 2014 +0200 @@ -239,7 +239,7 @@ let fun check_no_call t = if has_call t then unexpected_corec_call ctxt t else (); - val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o snd); + val build_map_Inl = build_map ctxt [] (uncurry Inl_const o dest_sumT o snd); fun massage_mutual_call bound_Ts U T t = if has_call t then diff -r 58f02fbaa764 -r 498a62e65f5f src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Tue Jun 24 13:48:14 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Tue Jun 24 13:48:14 2014 +0200 @@ -68,7 +68,7 @@ fun check_no_call t = if has_call t then unexpected_rec_call ctxt t else (); val typof = curry fastype_of1 bound_Ts; - val build_map_fst = build_map ctxt (fst_const o fst); + val build_map_fst = build_map ctxt [] (fst_const o fst); val yT = typof y; val yU = typof y'; diff -r 58f02fbaa764 -r 498a62e65f5f src/HOL/Tools/BNF/bnf_lfp_size.ML --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Jun 24 13:48:14 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Jun 24 13:48:14 2014 +0200 @@ -275,7 +275,7 @@ fun mk_rec_arg_arg (x as Free (_, T)) = let val U = B_ify T in - if T = U then x else build_map lthy2 (the o AList.lookup (op =) ABgs) (T, U) $ x + if T = U then x else build_map lthy2 [] (the o AList.lookup (op =) ABgs) (T, U) $ x end; fun mk_rec_o_map_arg rec_arg_T h =