# HG changeset patch # User traytel # Date 1366710189 -7200 # Node ID 3514b90d0a8b038ffdf41ef16e16be2f29eae8c8 # Parent 9e4220605179045ef1e2a6400694ed71dc348fea (co)rec is (just as the (un)fold) the unique morphism; diff -r 9e4220605179 -r 3514b90d0a8b src/HOL/BNF/BNF_GFP.thy --- a/src/HOL/BNF/BNF_GFP.thy Tue Apr 23 11:14:51 2013 +0200 +++ b/src/HOL/BNF/BNF_GFP.thy Tue Apr 23 11:43:09 2013 +0200 @@ -13,13 +13,18 @@ "codata" :: thy_decl begin -lemma sum_case_comp_Inl: -"sum_case f g \ Inl = f" +lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)" +unfolding o_def by (auto split: sum.splits) + +lemma sum_case_comp_Inl: "sum_case f g \ Inl = f" unfolding comp_def by simp lemma sum_case_expand_Inr: "f o Inl = g \ f x = sum_case g (f o Inr) x" by (auto split: sum.splits) +lemma sum_case_expand_Inr': "f o Inl = g \ h = f o Inr \ sum_case g h = f" +by (metis sum_case_comp_Inl sum_case_o_inj(2) surjective_sum) + lemma converse_Times: "(A \ B) ^-1 = B \ A" by auto diff -r 9e4220605179 -r 3514b90d0a8b src/HOL/BNF/BNF_LFP.thy --- a/src/HOL/BNF/BNF_LFP.thy Tue Apr 23 11:14:51 2013 +0200 +++ b/src/HOL/BNF/BNF_LFP.thy Tue Apr 23 11:43:09 2013 +0200 @@ -44,9 +44,15 @@ lemma snd_convol': "snd ( x) = g x" using snd_convol unfolding convol_def by simp +lemma convol_o: " o h = " + unfolding convol_def by auto + lemma convol_expand_snd: "fst o f = g \ = f" unfolding convol_def by auto +lemma convol_expand_snd': "(fst o f = g) \ (h = snd o f) \ ( = f)" + by (metis convol_expand_snd snd_convol) + definition inver where "inver g f A = (ALL a : A. g (f a) = a)" diff -r 9e4220605179 -r 3514b90d0a8b src/HOL/BNF/Tools/bnf_fp.ML --- a/src/HOL/BNF/Tools/bnf_fp.ML Tue Apr 23 11:14:51 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp.ML Tue Apr 23 11:43:09 2013 +0200 @@ -36,6 +36,7 @@ val ctor_mapN: string val ctor_map_uniqueN: string val ctor_recN: string + val ctor_rec_uniqueN: string val ctor_relN: string val ctor_set_inclN: string val ctor_set_set_inclN: string @@ -47,6 +48,7 @@ val dtorN: string val dtor_coinductN: string val dtor_corecN: string + val dtor_corec_uniqueN: string val dtor_ctorN: string val dtor_exhaustN: string val dtor_injectN: string @@ -207,7 +209,9 @@ val recN = "rec" val corecN = coN ^ recN val ctor_recN = ctorN ^ "_" ^ recN +val ctor_rec_uniqueN = ctor_recN ^ uniqueN val dtor_corecN = dtorN ^ "_" ^ corecN +val dtor_corec_uniqueN = dtor_corecN ^ uniqueN val ctor_dtor_corecN = ctorN ^ "_" ^ dtor_corecN val ctor_dtorN = ctorN ^ "_" ^ dtorN diff -r 9e4220605179 -r 3514b90d0a8b src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Tue Apr 23 11:14:51 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Tue Apr 23 11:43:09 2013 +0200 @@ -219,8 +219,10 @@ val in_bds = map in_bd_of_bnf bnfs; val in_monos = map in_mono_of_bnf bnfs; val map_comps = map map_comp_of_bnf bnfs; + val sym_map_comps = map (fn thm => thm RS sym) map_comps; val map_comp's = map map_comp'_of_bnf bnfs; val map_congs = map map_cong_of_bnf bnfs; + val map_ids = map map_id_of_bnf bnfs; val map_id's = map map_id'_of_bnf bnfs; val map_wpulls = map map_wpull_of_bnf bnfs; val set_bdss = map set_bd_of_bnf bnfs; @@ -1861,6 +1863,7 @@ val corec_maps = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_Inls; val corec_maps_rev = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_Inls_rev; val corec_Inls = map (Term.subst_atomic_types (activeBs ~~ Ts)) Inls; + val corec_UNIVs = map2 (HOLogic.mk_UNIV oo curry mk_sumT) Ts activeAs; val (((((((((((((Jzs, Jzs'), (Jz's, Jz's')), Jzs_copy), Jzs1), Jzs2), Jpairs), FJzs), TRs), unfold_fs), unfold_fs_copy), corec_ss), phis), names_lthy) = names_lthy @@ -2126,15 +2129,18 @@ val corec_name = Binding.name_of o corec_bind; val corec_def_bind = rpair [] o Thm.def_binding o corec_bind; + val corec_strs = + map3 (fn dtor => fn sum_s => fn mapx => + mk_sum_case + (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ corec_Inls), dtor), sum_s)) + dtors corec_ss corec_maps; + fun corec_spec i T AT = let val corecT = Library.foldr (op -->) (corec_sTs, AT --> T); - val maps = map3 (fn dtor => fn sum_s => fn mapx => mk_sum_case - (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ corec_Inls), dtor), sum_s)) - dtors corec_ss corec_maps; val lhs = Term.list_comb (Free (corec_name i, corecT), corec_ss); - val rhs = HOLogic.mk_comp (mk_unfold Ts maps i, Inr_const T AT); + val rhs = HOLogic.mk_comp (mk_unfold Ts corec_strs i, Inr_const T AT); in mk_Trueprop_eq (lhs, rhs) end; @@ -2175,6 +2181,26 @@ goals dtor_unfold_thms map_congs end; + val corec_unique_mor_thm = + let + val id_fs = map2 (fn T => fn f => mk_sum_case (HOLogic.id_const T, f)) Ts unfold_fs; + val prem = HOLogic.mk_Trueprop (mk_mor corec_UNIVs corec_strs UNIVs dtors id_fs); + fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_corec corec_ss i); + val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj + (map2 mk_fun_eq unfold_fs ks)); + in + Goal.prove_sorry lthy [] [] + (fold_rev Logic.all (corec_ss @ unfold_fs) (Logic.mk_implies (prem, unique))) + (mk_corec_unique_mor_tac corec_defs corec_Inl_sum_thms unfold_unique_mor_thm) + |> Thm.close_derivation + end; + + val dtor_corec_unique_thms = + split_conj_thm (split_conj_prems n + (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS corec_unique_mor_thm) + |> Local_Defs.unfold lthy (@{thms o_sum_case o_id id_o o_assoc sum_case_comp_Inl} @ + map_ids @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]}); + val ctor_dtor_corec_thms = map3 mk_ctor_dtor_unfold_like_thm dtor_inject_thms dtor_ctor_thms dtor_corec_thms; @@ -2990,7 +3016,8 @@ (dtor_exhaustN, dtor_exhaust_thms), (dtor_injectN, dtor_inject_thms), (dtor_unfoldN, dtor_unfold_thms), - (dtor_unfold_uniqueN, dtor_unfold_unique_thms)] + (dtor_unfold_uniqueN, dtor_unfold_unique_thms), + (dtor_corec_uniqueN, dtor_corec_unique_thms)] |> map (apsnd (map single)) |> maps (fn (thmN, thmss) => map2 (fn b => fn thms => diff -r 9e4220605179 -r 3514b90d0a8b src/HOL/BNF/Tools/bnf_gfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Tue Apr 23 11:14:51 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Tue Apr 23 11:43:09 2013 +0200 @@ -37,6 +37,8 @@ val mk_congruent_str_final_tac: int -> thm -> thm -> thm -> thm list -> tactic val mk_corec_tac: int -> thm list -> thm -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic + val mk_corec_unique_mor_tac: thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} -> + tactic val mk_dtor_map_coinduct_tac: int -> int list -> thm -> thm -> tactic val mk_dtor_map_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm -> thm -> thm -> tactic @@ -1121,6 +1123,11 @@ REPEAT_DETERM_N m o rtac refl, EVERY' (map (fn thm => rtac @{thm sum_case_expand_Inr} THEN' rtac thm) corec_Inls)] 1; +fun mk_corec_unique_mor_tac corec_defs corec_Inls unfold_unique_mor {context = ctxt, prems = _} = + unfold_thms_tac ctxt + (corec_defs @ map (fn thm => thm RS @{thm sum_case_expand_Inr'}) corec_Inls) THEN + etac unfold_unique_mor 1; + fun mk_dtor_srel_coinduct_tac ks raw_coind bis_srel = EVERY' [rtac rev_mp, rtac raw_coind, rtac ssubst, rtac bis_srel, rtac conjI, CONJ_WRAP' (K (rtac @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]})) ks, diff -r 9e4220605179 -r 3514b90d0a8b src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Tue Apr 23 11:14:51 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Tue Apr 23 11:43:09 2013 +0200 @@ -141,6 +141,7 @@ val bd_Cnotzeros = map bd_Cnotzero_of_bnf bnfs; val bd_Cnotzero = hd bd_Cnotzeros; val in_bds = map in_bd_of_bnf bnfs; + val sym_map_comps = map (fn bnf => map_comp_of_bnf bnf RS sym) bnfs; val map_comp's = map map_comp'_of_bnf bnfs; val map_congs = map map_cong_of_bnf bnfs; val map_ids = map map_id_of_bnf bnfs; @@ -980,6 +981,7 @@ val rec_maps = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_fsts; val rec_maps_rev = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_fsts_rev; val rec_fsts = map (Term.subst_atomic_types (activeBs ~~ Ts)) fsts; + val rec_UNIVs = map2 (HOLogic.mk_UNIV oo curry HOLogic.mk_prodT) Ts activeAs; val (((((((((Izs1, Izs1'), (Izs2, Izs2')), (xFs, xFs')), yFs), (AFss, AFss')), (fold_f, fold_f')), fs), rec_ss), names_lthy) = names_lthy @@ -1217,15 +1219,17 @@ val rec_name = Binding.name_of o rec_bind; val rec_def_bind = rpair [] o Thm.def_binding o rec_bind; + val rec_strs = + map3 (fn ctor => fn prod_s => fn mapx => + mk_convol (HOLogic.mk_comp (ctor, Term.list_comb (mapx, passive_ids @ rec_fsts)), prod_s)) + ctors rec_ss rec_maps; + fun rec_spec i T AT = let val recT = Library.foldr (op -->) (rec_sTs, T --> AT); - val maps = map3 (fn ctor => fn prod_s => fn mapx => - mk_convol (HOLogic.mk_comp (ctor, Term.list_comb (mapx, passive_ids @ rec_fsts)), prod_s)) - ctors rec_ss rec_maps; val lhs = Term.list_comb (Free (rec_name i, recT), rec_ss); - val rhs = HOLogic.mk_comp (snd_const (HOLogic.mk_prodT (T, AT)), mk_fold Ts maps i); + val rhs = HOLogic.mk_comp (snd_const (HOLogic.mk_prodT (T, AT)), mk_fold Ts rec_strs i); in mk_Trueprop_eq (lhs, rhs) end; @@ -1264,6 +1268,25 @@ goals ctor_fold_thms end; + val rec_unique_mor_thm = + let + val id_fs = map2 (fn T => fn f => mk_convol (HOLogic.id_const T, f)) Ts fs; + val prem = HOLogic.mk_Trueprop (mk_mor UNIVs ctors rec_UNIVs rec_strs id_fs); + fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_rec rec_ss i); + val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_fun_eq fs ks)); + in + Goal.prove_sorry lthy [] [] + (fold_rev Logic.all (rec_ss @ fs) (Logic.mk_implies (prem, unique))) + (mk_rec_unique_mor_tac rec_defs fst_rec_pair_thms fold_unique_mor_thm) + |> Thm.close_derivation + end; + + val ctor_rec_unique_thms = + split_conj_thm (split_conj_prems n + (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS rec_unique_mor_thm) + |> Local_Defs.unfold lthy (@{thms convol_o o_id id_o o_assoc[symmetric] fst_convol} @ + map_ids @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ convol, OF refl]}); + val timer = time (timer "rec definitions & thms"); val (ctor_induct_thm, induct_params) = @@ -1817,6 +1840,7 @@ (ctor_exhaustN, ctor_exhaust_thms), (ctor_foldN, ctor_fold_thms), (ctor_fold_uniqueN, ctor_fold_unique_thms), + (ctor_rec_uniqueN, ctor_rec_unique_thms), (ctor_injectN, ctor_inject_thms), (ctor_recN, ctor_rec_thms), (dtor_ctorN, dtor_ctor_thms), diff -r 9e4220605179 -r 3514b90d0a8b src/HOL/BNF/Tools/bnf_lfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Tue Apr 23 11:14:51 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Tue Apr 23 11:43:09 2013 +0200 @@ -65,6 +65,8 @@ thm list -> tactic val mk_mor_str_tac: 'a list -> thm -> tactic val mk_rec_tac: thm list -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic + val mk_rec_unique_mor_tac: thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} -> + tactic val mk_set_bd_tac: int -> (int -> tactic) -> thm -> thm list list -> thm list -> int -> {prems: 'a, context: Proof.context} -> tactic val mk_set_nat_tac: int -> (int -> tactic) -> thm list list -> thm list -> cterm list -> @@ -525,6 +527,11 @@ EVERY' [rtac trans, rtac o_apply, rtac trans, rtac (foldx RS @{thm arg_cong[of _ _ snd]}), rtac @{thm snd_convol'}] 1; +fun mk_rec_unique_mor_tac rec_defs fst_recs fold_unique_mor {context = ctxt, prems = _} = + unfold_thms_tac ctxt + (rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd'}) fst_recs) THEN + etac fold_unique_mor 1; + fun mk_ctor_induct_tac m set_natural'ss init_induct morEs mor_Abs Rep_invs Abs_invs Reps = let val n = length set_natural'ss;