# HG changeset patch # User traytel # Date 1392982429 -3600 # Node ID b657146dc030a059f681832f0372c86fef587c4a # Parent 18fe288f6801ff779fca6ad4b95f1be02a41d1bf only one internal coinduction rule diff -r 18fe288f6801 -r b657146dc030 src/HOL/BNF_GFP.thy --- a/src/HOL/BNF_GFP.thy Fri Feb 21 00:18:40 2014 +0100 +++ b/src/HOL/BNF_GFP.thy Fri Feb 21 12:33:49 2014 +0100 @@ -140,14 +140,13 @@ lemma subst_Pair: "P x y \ a = (x, y) \ P (fst a) (snd a)" by simp -lemma fst_diag_id: "(fst \ (%x. (x, x))) z = id z" -by simp +lemma fst_diag_id: "(fst \ (%x. (x, x))) z = id z" by simp +lemma snd_diag_id: "(snd \ (%x. (x, x))) z = id z" by simp -lemma snd_diag_id: "(snd \ (%x. (x, x))) z = id z" -by simp - -lemma image_convolD: "\(a, b) \ ` X\ \ \x. x \ X \ a = f x \ b = g x" -unfolding convol_def by auto +lemma fst_diag_fst: "fst o ((\x. (x, x)) o fst) = fst" by auto +lemma snd_diag_fst: "snd o ((\x. (x, x)) o fst) = fst" by auto +lemma fst_diag_snd: "fst o ((\x. (x, x)) o snd) = snd" by auto +lemma snd_diag_snd: "snd o ((\x. (x, x)) o snd) = snd" by auto definition Succ where "Succ Kl kl = {k . kl @ [k] \ Kl}" definition Shift where "Shift Kl k = {kl. k # kl \ Kl}" diff -r 18fe288f6801 -r b657146dc030 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Fri Feb 21 00:18:40 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Fri Feb 21 12:33:49 2014 +0100 @@ -1500,15 +1500,8 @@ val UNIVs = map HOLogic.mk_UNIV Ts; val FTs = mk_FTs (passiveAs @ Ts); - val prodTs = map (HOLogic.mk_prodT o `I) Ts; - val prodFTs = mk_FTs (passiveAs @ prodTs); val FTs_setss = mk_setss (passiveAs @ Ts); - val prodFT_setss = mk_setss (passiveAs @ prodTs); val map_FTs = map2 (fn Ds => mk_map_of_bnf Ds treeQTs (passiveAs @ Ts)) Dss bnfs; - val map_FT_nths = map2 (fn Ds => - mk_map_of_bnf Ds (passiveAs @ prodTs) (passiveAs @ Ts)) Dss bnfs; - val fstsTs = map fst_const prodTs; - val sndsTs = map snd_const prodTs; val unfold_fTs = map2 (curry op -->) activeAs Ts; val corec_sTs = map (Term.typ_subst_atomic (activeBs ~~ Ts)) sum_sTs; val corec_maps = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_Inls; @@ -1516,8 +1509,8 @@ 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), Jzs_copy), Jz's_copy), Jzs1), Jzs2), - FJzs), TRs), unfold_fs), corec_ss), phis), dtor_set_induct_phiss), + val ((((((((((((Jzs, Jzs'), Jz's), Jzs_copy), Jz's_copy), Jzs1), Jzs2), + TRs), unfold_fs), corec_ss), phis), dtor_set_induct_phiss), names_lthy) = names_lthy |> mk_Frees' "z" Ts ||>> mk_Frees "y" Ts' @@ -1525,7 +1518,6 @@ ||>> mk_Frees "y'" Ts' ||>> mk_Frees "z1" Ts ||>> mk_Frees "z2" Ts - ||>> mk_Frees "x" prodFTs ||>> mk_Frees "r" (map (mk_relT o `I) Ts) ||>> mk_Frees "f" unfold_fTs ||>> mk_Frees "s" corec_sTs @@ -1814,7 +1806,7 @@ val timer = time (timer "corec definitions & thms"); - val (dtor_map_coinduct_thm, coinduct_params, dtor_coinduct_thm) = + val (coinduct_params, dtor_coinduct_thm) = let val zs = Jzs1 @ Jzs2; val frees = phis @ zs; @@ -1842,37 +1834,8 @@ 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 phi dtor map_nth sets Jz Jz_copy FJz = - let - val xs = [Jz, Jz_copy]; - - fun mk_map_conjunct nths x = - HOLogic.mk_eq (Term.list_comb (map_nth, passive_ids @ nths) $ FJz, dtor $ x); - - 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), - phi $ z1 $ z2)); - - val concl = list_exists_free [FJz] (HOLogic.mk_conj - (Library.foldr1 HOLogic.mk_conj (map2 mk_map_conjunct [fstsTs, sndsTs] xs), - Library.foldr1 HOLogic.mk_conj - (map4 mk_set_conjunct (drop m sets) phis Jzs1 Jzs2))); - in - fold_rev Logic.all xs (Logic.mk_implies - (HOLogic.mk_Trueprop (Term.list_comb (phi, xs)), HOLogic.mk_Trueprop concl)) - end; - - 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; in - (dtor_map_coinduct, rev (Term.add_tfrees dtor_map_coinduct_goal []), dtor_coinduct) + (rev (Term.add_tfrees dtor_coinduct_goal []), dtor_coinduct) end; val timer = time (timer "coinduction"); @@ -2339,7 +2302,7 @@ Jsetss_by_bnf Jzs' Jzs fs_Jmaps fs_copy_Jmaps Jys' Jys Jys'_copy Jys_copy; val coinduct = unfold_thms lthy Jset_defs - (Drule.instantiate' cTs (map SOME cphis) dtor_map_coinduct_thm); + (Drule.instantiate' cTs (map SOME cphis) dtor_coinduct_thm); val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj @@ -2349,7 +2312,7 @@ (Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN mk_mcong_tac lthy m (rtac coinduct) map_comps dtor_Jmap_thms map_cong0s - set_mapss set_hset_thmss set_hset_hset_thmsss)) + set_mapss set_hset_thmss set_hset_hset_thmsss in_rels)) |> Thm.close_derivation in split_conj_thm thm @@ -2458,17 +2421,17 @@ HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map3 mk_helper_coind_concl Jz's Jz's_copy coind2_phis)); - fun mk_helper_coind_thms concl cts = + fun mk_helper_coind_thms fst concl cts = Goal.prove_sorry lthy [] [] (Logic.list_implies (helper_prems, concl)) - (fn {context = ctxt, prems = _} => mk_rel_coinduct_coind_tac ctxt m - (cterm_instantiate_pos cts dtor_map_coinduct_thm) ks map_comps map_cong0s - map_arg_cong_thms set_mapss dtor_unfold_thms dtor_Jmap_thms) + (fn {context = ctxt, prems = _} => mk_rel_coinduct_coind_tac ctxt fst m + (cterm_instantiate_pos cts dtor_coinduct_thm) ks map_comps map_cong0s + map_arg_cong_thms set_mapss dtor_unfold_thms dtor_Jmap_thms in_rels) |> Thm.close_derivation |> split_conj_thm |> Proof_Context.export names_lthy lthy; - val helper_coind1_thms = mk_helper_coind_thms helper_coind1_concl cts1; - val helper_coind2_thms = mk_helper_coind_thms helper_coind2_concl cts2; + val helper_coind1_thms = mk_helper_coind_thms true helper_coind1_concl cts1; + val helper_coind2_thms = mk_helper_coind_thms false helper_coind2_concl cts2; fun mk_helper_ind_phi phi ab fst snd z active_phi x y zip_unfold = list_all_free [x, y] (HOLogic.mk_imp @@ -2617,7 +2580,6 @@ val common_notes = [(dtor_coinductN, [dtor_coinduct_thm]), - (dtor_map_coinductN, [dtor_map_coinduct_thm]), (rel_coinductN, [Jrel_coinduct_thm]), (dtor_unfold_transferN, dtor_unfold_transfer_thms)] |> map (fn (thmN, thms) => diff -r 18fe288f6801 -r b657146dc030 src/HOL/Tools/BNF/bnf_gfp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Fri Feb 21 00:18:40 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Fri Feb 21 12:33:49 2014 +0100 @@ -27,7 +27,6 @@ val mk_congruent_str_final_tac: int -> thm -> thm -> thm -> thm list -> tactic val mk_corec_tac: Proof.context -> int -> thm list -> thm -> thm -> thm list -> tactic val mk_corec_unique_mor_tac: Proof.context -> thm list -> thm list -> thm -> tactic - val mk_dtor_map_coinduct_tac: int -> int list -> thm -> thm -> tactic val mk_dtor_coinduct_tac: int -> thm -> thm -> 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 @@ -41,7 +40,7 @@ val mk_length_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic val mk_map_comp0_tac: thm list -> thm list -> thm -> tactic val mk_mcong_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list -> thm list -> - thm list list -> thm list list -> thm list list list -> tactic + thm list list -> thm list list -> thm list list list -> thm list -> tactic val mk_map_id0_tac: thm list -> thm -> thm -> tactic val mk_map_tac: int -> int -> thm -> thm -> thm -> thm -> tactic val mk_dtor_map_unique_tac: Proof.context -> thm -> thm list -> tactic @@ -67,8 +66,8 @@ thm list -> thm list -> thm -> thm list -> tactic val mk_rel_coinduct_tac: Proof.context -> thm list -> thm list -> thm list -> thm list list -> thm list -> thm list -> tactic - val mk_rel_coinduct_coind_tac: Proof.context -> int -> thm -> int list -> thm list -> thm list -> - thm list -> thm list list -> thm list -> thm list -> tactic + val mk_rel_coinduct_coind_tac: Proof.context -> bool -> int -> thm -> int list -> thm list -> + thm list -> thm list -> thm list list -> thm list -> thm list -> thm list -> tactic val mk_rel_coinduct_ind_tac: Proof.context -> int -> int list -> thm list -> thm list list -> int -> thm -> tactic val mk_rv_last_tac: ctyp option list -> cterm option list -> thm list -> thm list -> tactic @@ -97,13 +96,13 @@ open BNF_FP_Util open BNF_GFP_Util -val fst_convol_fun_cong_sym = @{thm fst_convol} RS fun_cong RS sym; +val fst_convol_fun_cong_sym = @{thm fst_convol[unfolded convol_def]} RS fun_cong RS sym; val list_inject_iffD1 = @{thm list.inject[THEN iffD1]}; val nat_induct = @{thm nat_induct}; val o_apply_trans_sym = o_apply RS trans RS sym; val ord_eq_le_trans = @{thm ord_eq_le_trans}; val ordIso_ordLeq_trans = @{thm ordIso_ordLeq_trans}; -val snd_convol_fun_cong_sym = @{thm snd_convol} RS fun_cong RS sym; +val snd_convol_fun_cong_sym = @{thm snd_convol[unfolded convol_def]} RS fun_cong RS sym; val sum_weak_case_cong = @{thm sum.weak_case_cong}; val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]}; val Collect_splitD_set_mp = @{thm Collect_splitD[OF set_mp]}; @@ -774,27 +773,6 @@ CONJ_WRAP' (K (EVERY' [rtac impI, rtac @{thm IdD}, etac set_mp, rtac CollectI, etac @{thm case_prodI}])) rel_congs] 1; -fun mk_dtor_map_coinduct_tac m ks raw_coind bis_def = - let - val n = length ks; - in - EVERY' [rtac rev_mp, rtac raw_coind, rtac ssubst, rtac bis_def, rtac conjI, - CONJ_WRAP' (K (rtac @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]})) ks, - CONJ_WRAP' (fn i => EVERY' [select_prem_tac n (dtac asm_rl) i, REPEAT_DETERM o rtac allI, - rtac impI, REPEAT_DETERM o dtac @{thm meta_spec}, etac CollectE, etac @{thm meta_impE}, - atac, etac exE, etac conjE, etac conjE, rtac bexI, rtac conjI, - etac @{thm fst_conv[THEN subst]}, etac @{thm snd_conv[THEN subst]}, - rtac CollectI, REPEAT_DETERM_N m o (rtac conjI THEN' rtac subset_UNIV), - CONJ_WRAP' (fn i' => EVERY' [rtac subsetI, rtac CollectI, dtac (mk_conjunctN n i'), - REPEAT_DETERM o etac allE, etac mp, rtac @{thm ssubst_mem[OF pair_collapse]}, atac]) - ks]) - ks, - rtac impI, - CONJ_WRAP' (fn i => EVERY' [rtac impI, dtac (mk_conjunctN n i), - rtac @{thm subst[OF pair_in_Id_conv]}, etac set_mp, - rtac CollectI, etac (refl RSN (2, @{thm subst_Pair}))]) ks] 1 - end; - fun mk_map_tac m n map_arg_cong unfold map_comp map_cong0 = EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym), rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp RS box_equals)), rtac map_cong0, @@ -833,34 +811,40 @@ maps map_comp0s)] 1; fun mk_mcong_tac ctxt m coinduct_tac map_comps dtor_maps map_cong0s set_map0ss set_hsetss - set_hset_hsetsss = + set_hset_hsetsss in_rels = let val n = length map_comps; val ks = 1 upto n; in - EVERY' ([rtac rev_mp, - coinduct_tac] @ - maps (fn (((((map_comp_trans, dtor_maps_trans), map_cong0), set_map0s), set_hsets), - set_hset_hsetss) => - [REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt, rtac exI, rtac conjI, + EVERY' ([rtac rev_mp, coinduct_tac] @ + maps (fn ((((((map_comp_trans, dtor_maps_trans), map_cong0), set_map0s), set_hsets), + set_hset_hsetss), in_rel) => + [REPEAT_DETERM o resolve_tac [allI, impI, in_rel RS iffD2], + REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt, rtac exI, + rtac (Drule.rotate_prems 1 conjI), rtac conjI, rtac map_comp_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0, - REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac id_apply), + REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac @{thm fst_conv}), REPEAT_DETERM_N n o rtac fst_convol_fun_cong_sym, rtac map_comp_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0, EVERY' (maps (fn set_hset => - [rtac o_apply_trans_sym, rtac (id_apply RS trans), etac CollectE, + [rtac o_apply_trans_sym, rtac (@{thm snd_conv} RS trans), etac CollectE, REPEAT_DETERM o etac conjE, etac bspec, etac set_hset]) set_hsets), REPEAT_DETERM_N n o rtac snd_convol_fun_cong_sym, + rtac CollectI, + EVERY' (map (fn set_map0 => EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map0, + rtac @{thm image_subsetI}, rtac CollectI, rtac @{thm case_prodI}, rtac refl]) + (take m set_map0s)), CONJ_WRAP' (fn (set_map0, set_hset_hsets) => - EVERY' [REPEAT_DETERM o rtac allI, rtac impI, rtac @{thm image_convolD}, - etac set_rev_mp, rtac ord_eq_le_trans, rtac set_map0, - rtac @{thm image_mono}, rtac subsetI, rtac CollectI, etac CollectE, + EVERY' [rtac ord_eq_le_trans, rtac set_map0, + rtac @{thm image_subsetI}, rtac CollectI, rtac @{thm case_prodI}, rtac exI, rtac conjI, + rtac CollectI, etac CollectE, REPEAT_DETERM o etac conjE, CONJ_WRAP' (fn set_hset_hset => - EVERY' [rtac ballI, etac bspec, etac set_hset_hset, atac]) set_hset_hsets]) + EVERY' [rtac ballI, etac bspec, etac set_hset_hset, atac]) set_hset_hsets, + rtac (conjI OF [refl, refl])]) (drop m set_map0s ~~ set_hset_hsetss)]) (map (fn th => th RS trans) map_comps ~~ map (fn th => th RS trans) dtor_maps ~~ - map_cong0s ~~ set_map0ss ~~ set_hsetss ~~ set_hset_hsetsss) @ + map_cong0s ~~ set_map0ss ~~ set_hsetss ~~ set_hset_hsetsss ~~ in_rels) @ [rtac impI, CONJ_WRAP' (fn k => EVERY' [rtac impI, dtac (mk_conjunctN n k), etac mp, rtac exI, rtac conjI, etac CollectI, @@ -1014,36 +998,38 @@ EVERY' [rtac iffI, if_tac, only_if_tac] 1 end; -fun mk_rel_coinduct_coind_tac ctxt m coinduct ks map_comp0s map_congs map_arg_congs set_map0ss - dtor_unfolds dtor_maps = - let val n = length ks; +fun mk_rel_coinduct_coind_tac ctxt fst m coinduct ks map_comp0s map_congs map_arg_congs set_map0ss + dtor_unfolds dtor_maps in_rels = + let + val n = length ks; + val fst_diag_nth = if fst then @{thm fst_diag_fst} else @{thm fst_diag_snd}; + val snd_diag_nth = if fst then @{thm snd_diag_fst} else @{thm snd_diag_snd}; in EVERY' [rtac coinduct, - EVERY' (map7 (fn i => fn map_comp0 => fn map_cong => fn map_arg_cong => fn set_map0s => - fn dtor_unfold => fn dtor_map => - EVERY' [REPEAT_DETERM o eresolve_tac [exE, conjE], + EVERY' (map8 (fn i => fn map_comp0 => fn map_cong => fn map_arg_cong => fn set_map0s => + fn dtor_unfold => fn dtor_map => fn in_rel => + EVERY' [REPEAT_DETERM o resolve_tac [allI, impI, in_rel RS iffD2], + REPEAT_DETERM o eresolve_tac [exE, conjE], select_prem_tac (length ks) (dtac @{thm spec2}) i, dtac mp, atac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], hyp_subst_tac ctxt, - rtac exI, rtac conjI, rtac conjI, + rtac exI, rtac (Drule.rotate_prems 1 conjI), rtac conjI, rtac (map_comp0 RS trans), rtac (dtor_map RS trans RS sym), rtac (dtor_unfold RS map_arg_cong RS trans), rtac (trans OF [map_comp0, map_cong]), - REPEAT_DETERM_N m o - rtac @{thm trans[OF fun_cong[OF comp_id] sym[OF fun_cong[OF id_comp]]]}, + REPEAT_DETERM_N m o rtac (fst_diag_nth RS @{thm fun_cong[OF trans[OF o_id sym]]}), REPEAT_DETERM_N n o (rtac @{thm sym[OF trans[OF o_apply]]} THEN' rtac @{thm fst_conv}), rtac (map_comp0 RS trans), rtac (map_cong RS trans), - REPEAT_DETERM_N m o rtac @{thm fun_cong[OF id_comp]}, + REPEAT_DETERM_N m o rtac (snd_diag_nth RS fun_cong), REPEAT_DETERM_N n o (rtac @{thm trans[OF o_apply]} THEN' rtac @{thm snd_conv}), etac (@{thm prod.case} RS map_arg_cong RS trans), - SELECT_GOAL (unfold_thms_tac ctxt @{thms prod.case}), + SELECT_GOAL (unfold_thms_tac ctxt @{thms prod.case o_def fst_conv snd_conv}), + rtac CollectI, CONJ_WRAP' (fn set_map0 => - EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], - dtac (set_map0 RS equalityD1 RS set_mp), - REPEAT_DETERM o - eresolve_tac (imageE :: conjE :: @{thms iffD1[OF Pair_eq, elim_format]}), - hyp_subst_tac ctxt, rtac exI, rtac conjI, etac Collect_splitD_set_mp, atac, - rtac (o_apply RS trans), rtac (@{thm surjective_pairing} RS arg_cong)]) - (drop m set_map0s)]) - ks map_comp0s map_congs map_arg_congs set_map0ss dtor_unfolds dtor_maps)] 1 + EVERY' [rtac (set_map0 RS ord_eq_le_trans), + rtac @{thm image_subsetI}, rtac CollectI, rtac @{thm case_prodI}, + FIRST' [rtac refl, EVERY'[rtac exI, rtac conjI, etac Collect_splitD_set_mp, atac, + rtac (@{thm surjective_pairing} RS arg_cong)]]]) + set_map0s]) + ks map_comp0s map_congs map_arg_congs set_map0ss dtor_unfolds dtor_maps in_rels)] 1 end; val split_id_unfolds = @{thms prod.case image_id id_apply};