# HG changeset patch # User traytel # Date 1377013147 -7200 # Node ID ec38e9f4352f19240dc7dad9367bc6ddb33e10bc # Parent c042b3ad18a021e9498de6895e6a9d9ceee3ba2b simpler (forward) derivation of strong (up-to equality) coinduction properties diff -r c042b3ad18a0 -r ec38e9f4352f src/HOL/BNF/BNF_FP_Basic.thy --- a/src/HOL/BNF/BNF_FP_Basic.thy Tue Aug 20 16:10:58 2013 +0200 +++ b/src/HOL/BNF/BNF_FP_Basic.thy Tue Aug 20 17:39:07 2013 +0200 @@ -147,6 +147,12 @@ "(fun_rel R (fun_rel S T)) f g = (\x y. R x y \ (fun_rel S T) (f x) (g y))" unfolding fun_rel_def .. +lemma subst_eq_imp: "(\a b. a = b \ P a b) \ (\a. P a a)" + by auto + +lemma eq_subset: "op = \ (\a b. P a b \ a = b)" + by auto + ML_file "Tools/bnf_fp_util.ML" ML_file "Tools/bnf_fp_def_sugar_tactics.ML" ML_file "Tools/bnf_fp_def_sugar.ML" diff -r c042b3ad18a0 -r ec38e9f4352f src/HOL/BNF/BNF_GFP.thy --- a/src/HOL/BNF/BNF_GFP.thy Tue Aug 20 16:10:58 2013 +0200 +++ b/src/HOL/BNF/BNF_GFP.thy Tue Aug 20 17:39:07 2013 +0200 @@ -70,9 +70,6 @@ lemma image2_eqI: "\b = f x; c = g x; x \ A\ \ (b, c) \ image2 A f g" unfolding image2_def by auto -lemma eq_subset: "op = \ (\a b. P a b \ a = b)" -by auto - lemma IdD: "(a, b) \ Id \ a = b" by auto diff -r c042b3ad18a0 -r ec38e9f4352f src/HOL/BNF/Tools/bnf_fp_util.ML --- a/src/HOL/BNF/Tools/bnf_fp_util.ML Tue Aug 20 16:10:58 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Tue Aug 20 17:39:07 2013 +0200 @@ -179,6 +179,8 @@ val mk_xtor_un_fold_o_map_thms: fp_kind -> bool -> int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list + val mk_strong_coinduct_thm: int -> thm -> thm list -> thm list -> Proof.context -> thm + val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> local_theory -> 'a) -> binding list -> (string * sort) list -> ((string * sort) * typ) list -> local_theory -> @@ -552,6 +554,24 @@ split_conj_thm (un_fold_unique OF map (fp_case fp I mk_sym) unique_prems) end; +fun mk_strong_coinduct_thm m coind rel_eqs rel_monos ctxt = + let + val n = Thm.nprems_of coind; + fun mk_inst phi = (phi, mk_union (phi, HOLogic.eq_const (fst (dest_pred2T (fastype_of phi))))) + |> pairself (certify ctxt); + val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map (mk_inst o Var); + fun mk_unfold rel_eq rel_mono = + let + val eq = iffD2 OF [rel_eq RS @{thm predicate2_eqD}, refl]; + val mono = rel_mono OF (replicate m @{thm order_refl} @ replicate n @{thm eq_subset}); + in eq RS (mono RS @{thm predicate2D}) RS @{thm eqTrueI} end; + val unfolds = map2 mk_unfold rel_eqs rel_monos @ @{thms sup_fun_def sup_bool_def + imp_disjL all_conj_distrib subst_eq_imp simp_thms(18,21,35)}; + in + Thm.instantiate ([], insts) coind + |> unfold_thms ctxt unfolds + end; + fun fp_bnf construct_fp bs resBs eqs lthy = let val timer = time (Timer.startRealTimer ()); diff -r c042b3ad18a0 -r ec38e9f4352f src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Tue Aug 20 16:10:58 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Tue Aug 20 17:39:07 2013 +0200 @@ -2019,48 +2019,36 @@ val timer = time (timer "corec definitions & thms"); - (* TODO: Get rid of strong versions (since these can easily be derived from the weak ones). *) - val (dtor_map_coinduct_thm, coinduct_params, dtor_coinduct_thm, dtor_strong_coinduct_thm) = + val (dtor_map_coinduct_thm, coinduct_params, dtor_coinduct_thm) = let val zs = Jzs1 @ Jzs2; val frees = phis @ zs; - fun mk_phi strong_eq phi z1 z2 = if strong_eq - then Term.absfree (dest_Free z1) (Term.absfree (dest_Free z2) - (HOLogic.mk_disj (phi $ z1 $ z2, HOLogic.mk_eq (z1, z2)))) - else phi; - - fun phi_rels strong_eq = - map3 (fn phi => fn z1 => fn z2 => mk_phi strong_eq phi z1 z2) phis Jzs1 Jzs2; - val rels = map (Term.subst_atomic_types ((activeAs ~~ Ts) @ (activeBs ~~ Ts))) relsAsBs; fun mk_concl phi z1 z2 = HOLogic.mk_imp (phi $ z1 $ z2, HOLogic.mk_eq (z1, z2)); val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map3 mk_concl phis Jzs1 Jzs2)); - fun mk_rel_prem strong_eq phi dtor rel Jz Jz_copy = + fun mk_rel_prem phi dtor rel Jz Jz_copy = let - val concl = Term.list_comb (rel, map HOLogic.eq_const passiveAs @ phi_rels strong_eq) $ + val concl = Term.list_comb (rel, map HOLogic.eq_const passiveAs @ phis) $ (dtor $ Jz) $ (dtor $ Jz_copy); in HOLogic.mk_Trueprop (list_all_free [Jz, Jz_copy] (HOLogic.mk_imp (phi $ Jz $ Jz_copy, concl))) end; - val rel_prems = map5 (mk_rel_prem false) phis dtors rels Jzs Jzs_copy; - val rel_strong_prems = map5 (mk_rel_prem true) phis dtors rels Jzs Jzs_copy; - + val rel_prems = map5 mk_rel_prem phis dtors rels Jzs Jzs_copy; val dtor_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (rel_prems, concl)); - val coinduct_params = rev (Term.add_tfrees dtor_coinduct_goal []); val dtor_coinduct = Goal.prove_sorry lthy [] [] dtor_coinduct_goal (K (mk_dtor_coinduct_tac m raw_coind_thm bis_rel_thm rel_congs)) |> Thm.close_derivation; - fun mk_prem strong_eq phi dtor map_nth sets Jz Jz_copy FJz = + fun mk_prem phi dtor map_nth sets Jz Jz_copy FJz = let val xs = [Jz, Jz_copy]; @@ -2070,7 +2058,7 @@ fun mk_set_conjunct set phi z1 z2 = list_all_free [z1, z2] (HOLogic.mk_imp (HOLogic.mk_mem (HOLogic.mk_prod (z1, z2), set $ FJz), - mk_phi strong_eq phi z1 z2 $ z1 $ z2)); + phi $ z1 $ z2)); val concl = list_exists_free [FJz] (HOLogic.mk_conj (Library.foldr1 HOLogic.mk_conj (map2 mk_map_conjunct [fstsTs, sndsTs] xs), @@ -2081,31 +2069,21 @@ (HOLogic.mk_Trueprop (Term.list_comb (phi, xs)), HOLogic.mk_Trueprop concl)) end; - fun mk_prems strong_eq = - map7 (mk_prem strong_eq) phis dtors map_FT_nths prodFT_setss Jzs Jzs_copy FJzs; - - val prems = mk_prems false; - val strong_prems = mk_prems true; + val prems = map7 mk_prem phis dtors map_FT_nths prodFT_setss Jzs Jzs_copy FJzs; val dtor_map_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (prems, concl)); val dtor_map_coinduct = Goal.prove_sorry lthy [] [] dtor_map_coinduct_goal (K (mk_dtor_map_coinduct_tac m ks raw_coind_thm bis_def)) |> Thm.close_derivation; - - val cTs = map (SOME o certifyT lthy o TFree) coinduct_params; - val cts = map3 (SOME o certify lthy ooo mk_phi true) phis Jzs1 Jzs2; - - val dtor_strong_coinduct = singleton (Proof_Context.export names_lthy lthy) - (Goal.prove_sorry lthy [] [] - (fold_rev Logic.all zs (Logic.list_implies (rel_strong_prems, concl))) - (K (mk_dtor_strong_coinduct_tac lthy m cTs cts dtor_coinduct rel_monos rel_eqs))) - |> Thm.close_derivation; in - (dtor_map_coinduct, rev (Term.add_tfrees dtor_map_coinduct_goal []), - dtor_coinduct, dtor_strong_coinduct) + (dtor_map_coinduct, rev (Term.add_tfrees dtor_map_coinduct_goal []), dtor_coinduct) end; + (* TODO: Get rid of strong versions (since these can easily be derived from the weak ones). *) + val dtor_strong_coinduct_thm = + mk_strong_coinduct_thm m dtor_coinduct_thm rel_eqs rel_monos lthy; + val timer = time (timer "coinduction"); fun mk_dtor_map_DEADID_thm dtor_inject map_id = diff -r c042b3ad18a0 -r ec38e9f4352f src/HOL/BNF/Tools/bnf_gfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Tue Aug 20 16:10:58 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Tue Aug 20 17:39:07 2013 +0200 @@ -41,8 +41,6 @@ val mk_dtor_map_coinduct_tac: int -> int list -> thm -> thm -> tactic val mk_dtor_set_tac: int -> thm -> thm -> thm list -> tactic val mk_dtor_coinduct_tac: int -> thm -> thm -> thm list -> tactic - val mk_dtor_strong_coinduct_tac: Proof.context -> int -> ctyp option list -> - cterm option list -> thm -> thm list -> thm list -> tactic val mk_dtor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm -> thm list -> thm list -> thm list list -> tactic val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> @@ -989,18 +987,6 @@ CONJ_WRAP' (K (EVERY' [rtac impI, rtac @{thm IdD}, etac set_mp, rtac CollectI, etac @{thm prod_caseI}])) rel_congs] 1; -fun mk_dtor_strong_coinduct_tac ctxt m cTs cts dtor_coinduct rel_monos rel_eqs = - EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_coinduct), - EVERY' (map2 (fn rel_mono => fn rel_eq => - EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], REPEAT_DETERM o etac allE, - etac disjE, etac mp, atac, hyp_subst_tac ctxt, rtac (rel_mono RS @{thm predicate2D}), - REPEAT_DETERM_N m o rtac @{thm order_refl}, - REPEAT_DETERM_N (length rel_monos) o rtac @{thm eq_subset}, - rtac (rel_eq RS sym RS @{thm eq_refl} RS @{thm predicate2D}), rtac refl]) - rel_monos rel_eqs), - rtac impI, REPEAT_DETERM o etac conjE, - CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) rel_eqs] 1; - fun mk_dtor_map_coinduct_tac m ks raw_coind bis_def = let val n = length ks;