# HG changeset patch # User desharna # Date 1411655750 -7200 # Node ID ed95293f14b65435a6e96c755fdcc4c0a0d39d43 # Parent a23780c2224527227a77729a3f277cf8bc751105 generate 'ctor_rec_transfer' for datatypes diff -r a23780c22245 -r ed95293f14b6 src/HOL/BNF_Least_Fixpoint.thy --- a/src/HOL/BNF_Least_Fixpoint.thy Mon Sep 01 14:14:47 2014 +0200 +++ b/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 25 16:35:50 2014 +0200 @@ -178,6 +178,29 @@ lemma id_transfer: "rel_fun A A id id" unfolding rel_fun_def by simp +lemma fst_transfer: "rel_fun (rel_prod A B) A fst fst" + unfolding rel_fun_def rel_prod_def by simp + +lemma snd_transfer: "rel_fun (rel_prod A B) B snd snd" + unfolding rel_fun_def rel_prod_def by simp + +lemma case_sum_transfer: + "rel_fun (rel_fun R T) (rel_fun (rel_fun S T) (rel_fun (rel_sum R S) T)) case_sum case_sum" + unfolding rel_fun_def rel_sum_def by (auto split: sum.splits) + +lemma map_sum_transfer: + "rel_fun (rel_fun R T) (rel_fun (rel_fun S U) (rel_fun (rel_sum R S) (rel_sum T U))) map_sum map_sum" + unfolding rel_fun_def rel_sum_def by (auto split: sum.splits) + +lemma convol_transfer: + "rel_fun (rel_fun R S) (rel_fun (rel_fun R T) (rel_fun R (rel_prod S T))) BNF_Def.convol BNF_Def.convol" + unfolding rel_prod_def rel_fun_def convol_def by auto + +lemma comp_transfer: + "rel_fun (rel_fun B C) (rel_fun (rel_fun A B) (rel_fun A C)) (op \) (op \)" + unfolding rel_fun_def by simp + + lemma ssubst_Pair_rhs: "\(r, s) \ R; s' = s\ \ (r, s') \ R" by (rule ssubst) diff -r a23780c22245 -r ed95293f14b6 src/HOL/Lifting_Product.thy --- a/src/HOL/Lifting_Product.thy Mon Sep 01 14:14:47 2014 +0200 +++ b/src/HOL/Lifting_Product.thy Thu Sep 25 16:35:50 2014 +0200 @@ -22,11 +22,8 @@ lemma Pair_transfer [transfer_rule]: "(A ===> B ===> rel_prod A B) Pair Pair" unfolding rel_fun_def rel_prod_def by simp -lemma fst_transfer [transfer_rule]: "(rel_prod A B ===> A) fst fst" - unfolding rel_fun_def rel_prod_def by simp - -lemma snd_transfer [transfer_rule]: "(rel_prod A B ===> B) snd snd" - unfolding rel_fun_def rel_prod_def by simp +declare fst_transfer [transfer_rule] +declare snd_transfer [transfer_rule] lemma case_prod_transfer [transfer_rule]: "((A ===> B ===> C) ===> rel_prod A B ===> C) case_prod case_prod" diff -r a23780c22245 -r ed95293f14b6 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Sep 01 14:14:47 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Sep 25 16:35:50 2014 +0200 @@ -62,6 +62,7 @@ val ctor_map_uniqueN: string val ctor_recN: string val ctor_rec_o_mapN: string + val ctor_rec_transferN: string val ctor_rec_uniqueN: string val ctor_relN: string val ctor_rel_inductN: string @@ -294,6 +295,7 @@ val corecN = coN ^ recN val ctor_recN = ctorN ^ "_" ^ recN val ctor_rec_o_mapN = ctor_recN ^ "_o_" ^ mapN +val ctor_rec_transferN = ctor_recN ^ transferN val ctor_rec_uniqueN = ctor_recN ^ uniqueN val dtor_corecN = dtorN ^ "_" ^ corecN val dtor_corec_o_mapN = dtor_corecN ^ "_o_" ^ mapN diff -r a23780c22245 -r ed95293f14b6 src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Mon Sep 01 14:14:47 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Thu Sep 25 16:35:50 2014 +0200 @@ -1786,7 +1786,8 @@ val ctor_rec_transfer_thms = mk_co_iter_transfer_thms Least_FP rec_rels rec_activephis activephis Irels Iphis (mk_recs Ts passiveAs activeAs) (mk_recs Ts' passiveBs activeBs) - (fn {context = ctxt, prems = _} => print_tac ctxt "xxx" THEN Skip_Proof.cheat_tac 1) + (fn {context = ctxt, prems = _} => mk_ctor_rec_transfer_tac ctxt n m rec_defs + ctor_fold_transfer_thms (map map_transfer_of_bnf bnfs) ctor_Irel_thms) lthy; val timer = time (timer "relator induction"); @@ -1795,6 +1796,7 @@ [(ctor_inductN, [ctor_induct_thm]), (ctor_induct2N, [ctor_induct2_thm]), (ctor_fold_transferN, ctor_fold_transfer_thms), + (ctor_rec_transferN, ctor_rec_transfer_thms), (ctor_rel_inductN, [Irel_induct_thm])] |> map (fn (thmN, thms) => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); diff -r a23780c22245 -r ed95293f14b6 src/HOL/Tools/BNF/bnf_lfp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Mon Sep 01 14:14:47 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Thu Sep 25 16:35:50 2014 +0200 @@ -22,6 +22,8 @@ val mk_ctor_induct2_tac: Proof.context -> ctyp option list -> cterm option list -> thm -> thm list -> tactic val mk_ctor_set_tac: thm -> thm -> thm list -> tactic + val mk_ctor_rec_transfer_tac: Proof.context -> int -> int -> thm list -> thm list -> thm list -> + thm list -> tactic val mk_ctor_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 -> tactic @@ -701,6 +703,29 @@ EVERY' [rtac iffI, if_tac, only_if_tac] 1 end; +fun mk_ctor_rec_transfer_tac ctxt n m ctor_rec_defs ctor_fold_transfers pre_T_map_transfers + ctor_rels = + let + val rel_funD = @{thm rel_funD}; + fun rel_funD_n n = funpow n (fn thm => thm RS rel_funD); + val rel_funD_n_rotated = rotate_prems ~1 oo rel_funD_n; + in + CONJ_WRAP (fn (ctor_rec_def, ctor_fold_transfer) => + REPEAT_DETERM (HEADGOAL (rtac @{thm rel_funI})) THEN + unfold_thms_tac ctxt [ctor_rec_def, o_apply] THEN + HEADGOAL (rtac @{thm rel_funD[OF snd_transfer]} THEN' + etac (rel_funD_n_rotated (n + 1) ctor_fold_transfer) THEN' + EVERY' (map2 (fn pre_T_map_transfer => fn ctor_rel => + etac (rel_funD_n_rotated 2 @{thm convol_transfer}) THEN' + rtac (rel_funD_n_rotated 2 @{thm comp_transfer}) THEN' + rtac (rel_funD_n (m + n) pre_T_map_transfer) THEN' + REPEAT_DETERM_N m o rtac @{thm id_transfer} THEN' + REPEAT_DETERM o rtac @{thm fst_transfer} THEN' + rtac @{thm rel_funI} THEN' + etac (ctor_rel RS iffD2)) pre_T_map_transfers ctor_rels))) + (ctor_rec_defs ~~ ctor_fold_transfers) + end; + fun mk_rel_induct_tac ctxt IHs m ctor_induct2 ks ctor_rels rel_mono_strong0s = let val n = length ks; in diff -r a23780c22245 -r ed95293f14b6 src/HOL/Transfer.thy --- a/src/HOL/Transfer.thy Mon Sep 01 14:14:47 2014 +0200 +++ b/src/HOL/Transfer.thy Thu Sep 25 16:35:50 2014 +0200 @@ -458,9 +458,7 @@ lemma id_transfer [transfer_rule]: "(A ===> A) id id" unfolding rel_fun_def by simp -lemma comp_transfer [transfer_rule]: - "((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \) (op \)" - unfolding rel_fun_def by simp +declare comp_transfer [transfer_rule] lemma fun_upd_transfer [transfer_rule]: assumes [transfer_rule]: "bi_unique A"