# HG changeset patch # User desharna # Date 1403610494 -7200 # Node ID 7b997028aaac2e7478aa2b13c0a30c416a9db452 # Parent 7e22d7b75e2af2d8db6d3a36837fa6ff6ef2623c generate 'rel_coinduct0' theorem for codatatypes diff -r 7e22d7b75e2a -r 7b997028aaac src/HOL/BNF_FP_Base.thy --- a/src/HOL/BNF_FP_Base.thy Tue Jun 24 12:36:45 2014 +0200 +++ b/src/HOL/BNF_FP_Base.thy Tue Jun 24 13:48:14 2014 +0200 @@ -83,6 +83,9 @@ "setr (Inr x) = {x}" unfolding sum_set_defs by simp+ +lemma Inl_Inr_False: "(Inl x = Inr y) = False" + by simp + lemma spec2: "\x y. P x y \ P x y" by blast diff -r 7e22d7b75e2a -r 7b997028aaac src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Tue Jun 24 12:36:45 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_def.ML Tue Jun 24 13:48:14 2014 +0200 @@ -85,6 +85,7 @@ 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 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 @@ -533,10 +534,12 @@ Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t end; -fun build_map_or_rel mk const of_bnf dest ctxt build_simple = +fun build_map_or_rel mk const of_bnf dest blacklist ctxt build_simple = let fun build (TU as (T, U)) = - if T = U then + if exists (curry (op =) T) blacklist then + build_simple TU + else if T = U andalso not (exists_subtype_in blacklist T) then const T else (case TU of @@ -553,8 +556,9 @@ | _ => 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; +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; fun map_flattened_map_args ctxt s map_args fs = let @@ -1284,7 +1288,7 @@ (mk_Ball (setA $ x) (Term.absfree (dest_Free a) (mk_Ball (setB $ y) (Term.absfree (dest_Free b) (HOLogic.mk_imp (R $ a $ b, S $ a $ b)))))); - val prems = HOLogic.mk_Trueprop (Term.list_comb (rel, Rs) $ x $ y) :: + val prems = HOLogic.mk_Trueprop (Term.list_comb (rel, Rs) $ x $ y) :: map6 mk_prem bnf_sets_As bnf_sets_Bs Rs Rs_copy zs ys; val concl = HOLogic.mk_Trueprop (Term.list_comb (rel, Rs_copy) $ x $ y); in @@ -1399,7 +1403,7 @@ |> Conjunction.elim_balanced (length wit_goals) |> map2 (Conjunction.elim_balanced o length) wit_goalss |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0)); - val (mk_wit_thms, nontriv_wit_goals) = + val (mk_wit_thms, nontriv_wit_goals) = (case triv_tac_opt of NONE => (fn _ => [], map (map (rpair [])) wit_goalss) | SOME tac => (mk_triv_wit_thms tac, [])); diff -r 7e22d7b75e2a -r 7b997028aaac src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Jun 24 12:36:45 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Jun 24 13:48:14 2014 +0200 @@ -597,6 +597,92 @@ (rec_thmss, code_nitpicksimp_attrs @ simp_attrs)) end; +fun derive_rel_coinduct0_thm_for_types lthy fpA_Ts ns As Bs ctr_sugars abs_inverses abs_injects + ctor_injects dtor_ctors rel_pre_defs ctor_defss dtor_rel_coinduct = + let + val fpB_Ts = map (typ_subst_nonatomic (As ~~ Bs)) fpA_Ts + + val (Rs, IRs, fpAs, fpBs, names_lthy) = + let + val fp_names = map base_name_of_typ fpA_Ts; + val ((((Rs, IRs), fpAs_names), fpBs_names), names_lthy) = lthy + |> mk_Frees "R" (map2 mk_pred2T As Bs) + ||>> mk_Frees "IR" (map2 mk_pred2T fpA_Ts fpB_Ts) + ||>> Variable.variant_fixes fp_names + ||>> Variable.variant_fixes (map (suffix "'") fp_names); + in + (Rs, IRs, + map2 (curry Free) fpAs_names fpA_Ts, + map2 (curry Free) fpBs_names fpB_Ts, names_lthy) + end; + + val ((discA_tss, selA_tsss), (discB_tss, selB_tsss)) = + let + val discss = map #discs ctr_sugars; + val selsss = map #selss ctr_sugars; + fun mk_discss ts Ts = map2 (map o rapp) ts (map (map (mk_disc_or_sel Ts)) discss); + fun mk_selsss ts Ts = map2 (map o map o rapp) ts (map (map (map (mk_disc_or_sel Ts))) + selsss); + in + ((mk_discss fpAs As, mk_selsss fpAs As) + ,(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)); + + val premises = + let + 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 + + 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))]); + + fun mk_prem_concl n discA_ts selA_tss discB_ts selB_tss = + Library.foldr1 HOLogic.mk_conj (flat (map5 (mk_prem_ctr_concls n) + (1 upto n) discA_ts selA_tss discB_ts selB_tss)) + handle List.Empty => @{term True}; + + fun mk_prem IR tA tB n discA_ts selA_tss discB_ts selB_tss = + fold_rev Logic.all [tA, tB] (Logic.mk_implies (HOLogic.mk_Trueprop (IR $ tA $ tB), + HOLogic.mk_Trueprop (mk_prem_concl n discA_ts selA_tss discB_ts selB_tss))); + in + map8 mk_prem IRs fpAs fpBs ns discA_tss selA_tsss discB_tss selB_tsss + 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) + *) + in + 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) + |> singleton (Proof_Context.export names_lthy lthy) + end; + fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, ((pgss, cqgsss), _)) 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) @@ -666,10 +752,12 @@ (1 upto n) udiscs uselss vdiscs vselss ctrXs_Tss)) handle List.Empty => @{term True}; + (* Probably the good premise *) fun mk_prem rs' uvr u v n udiscs uselss vdiscs vselss ctrXs_Tss = fold_rev Logic.all [u, v] (Logic.mk_implies (HOLogic.mk_Trueprop uvr, HOLogic.mk_Trueprop (mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss))); + (* Make a new conclusion (e.g. rel_concl) *) val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map3 (fn uvr => fn u => fn v => HOLogic.mk_imp (uvr, HOLogic.mk_eq (u, v))) @@ -946,7 +1034,7 @@ val ((pre_bnfs, absT_infos), (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0, dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms, - xtor_co_rec_thms, ...}, + xtor_co_rec_thms, rel_xtor_co_induct_thm, ...}, lthy)) = fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) (map dest_TFree killed_As) fp_eqs no_defs_lthy0 @@ -1481,6 +1569,10 @@ abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs (Proof_Context.export lthy' no_defs_lthy) lthy; + val rel_coinduct0_thm = derive_rel_coinduct0_thm_for_types lthy fpTs ns As Bs 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; val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type; @@ -1493,7 +1585,7 @@ mapss rel_injectss rel_distinctss setss; val common_notes = - (if nn > 1 then + (rel_coinductN ^ "0", [rel_coinduct0_thm], []) :: (if nn > 1 then [(coinductN, [coinduct_thm], common_coinduct_attrs), (strong_coinductN, [strong_coinduct_thm], common_coinduct_attrs)] else diff -r 7e22d7b75e2a -r 7b997028aaac src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Jun 24 12:36:45 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Jun 24 13:48:14 2014 +0200 @@ -26,6 +26,9 @@ val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic + val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list -> + thm list list -> thm list list -> thm list list -> thm list -> thm list -> thm list -> + thm list -> thm list -> tactic val mk_sel_map_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic val mk_sel_set_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic val mk_set_empty_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic @@ -205,6 +208,27 @@ (1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss selsss)); +fun mk_rel_coinduct0_tac ctxt dtor_rel_coinduct cts assms exhausts discss selss ctor_defss + dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses = + rtac dtor_rel_coinduct 1 THEN + EVERY (map11 (fn ct => fn assm => fn exhaust => fn discs => fn sels => fn ctor_defs => + fn dtor_ctor => fn ctor_inject => fn abs_inject => fn rel_pre_def => fn abs_inverse => + (rtac exhaust THEN_ALL_NEW (rtac exhaust THEN_ALL_NEW + (dtac (rotate_prems (~1) ((cterm_instantiate_pos [NONE, NONE, NONE, NONE, SOME ct] @{thm + 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 (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 + 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 + abs_inverses); + fun mk_sel_map_tac ctxt ct exhaust discs maps sels = TRYALL Goal.conjunction_tac THEN ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW