1.1 --- a/src/HOL/BNF_FP_Base.thy Tue Jul 01 16:26:14 2014 +0200
1.2 +++ b/src/HOL/BNF_FP_Base.thy Tue Jul 01 17:01:28 2014 +0200
1.3 @@ -89,6 +89,9 @@
1.4 lemma Inl_Inr_False: "(Inl x = Inr y) = False"
1.5 by simp
1.6
1.7 +lemma Inr_Inl_False: "(Inr x = Inl y) = False"
1.8 + by simp
1.9 +
1.10 lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
1.11 by blast
1.12
2.1 --- a/src/HOL/BNF_LFP.thy Tue Jul 01 16:26:14 2014 +0200
2.2 +++ b/src/HOL/BNF_LFP.thy Tue Jul 01 17:01:28 2014 +0200
2.3 @@ -1,3 +1,4 @@
2.4 +
2.5 (* Title: HOL/BNF_LFP.thy
2.6 Author: Dmitriy Traytel, TU Muenchen
2.7 Author: Lorenz Panny, TU Muenchen
2.8 @@ -194,4 +195,5 @@
2.9
2.10 hide_fact (open) id_transfer
2.11
2.12 +
2.13 end
3.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Jul 01 16:26:14 2014 +0200
3.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Jul 01 17:01:28 2014 +0200
3.3 @@ -243,10 +243,6 @@
3.4 fun merge_type_args fp (As, As') =
3.5 if length As = length As' then map2 (merge_type_arg fp) As As' else cannot_merge_types fp;
3.6
3.7 -fun reassoc_conjs thm =
3.8 - reassoc_conjs (thm RS @{thm conj_assoc[THEN iffD1]})
3.9 - handle THM _ => thm;
3.10 -
3.11 fun type_args_named_constrained_of_spec (((((ncAs, _), _), _), _), _) = ncAs;
3.12 fun type_binding_of_spec (((((_, b), _), _), _), _) = b;
3.13 fun mixfix_of_spec ((((_, mx), _), _), _) = mx;
3.14 @@ -444,6 +440,69 @@
3.15 map5 mk_preds_getterss_join cs cpss f_absTs abss cqgsss)))
3.16 end;
3.17
3.18 +fun postproc_co_induct lthy nn prop prop_conj =
3.19 + Drule.zero_var_indexes
3.20 + #> `(conj_dests nn)
3.21 + #>> map (fn thm => Thm.permute_prems 0 (~1) (thm RS prop))
3.22 + ##> (fn thm => Thm.permute_prems 0 (~nn)
3.23 + (if nn = 1 then thm RS prop
3.24 + else funpow nn (fn thm => Local_Defs.unfold lthy @{thms conj_assoc} (thm RS prop_conj)) thm));
3.25 +
3.26 +fun mk_induct_attrs ctrss =
3.27 + let
3.28 + val induct_cases = quasi_unambiguous_case_names (maps (map name_of_ctr) ctrss);
3.29 + val induct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names induct_cases));
3.30 + in
3.31 + [induct_case_names_attr]
3.32 + end;
3.33 +
3.34 +fun derive_rel_induct_thm_for_types lthy fpA_Ts ns As Bs mss ctrAss ctrAs_Tsss ctr_sugars
3.35 + ctor_rel_induct ctor_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs =
3.36 + let
3.37 + val B_ify = typ_subst_nonatomic (As ~~ Bs)
3.38 + val fpB_Ts = map B_ify fpA_Ts;
3.39 + val ctrBs_Tsss = map (map (map B_ify)) ctrAs_Tsss;
3.40 + val ctrBss = map (map (subst_nonatomic_types (As ~~ Bs))) ctrAss;
3.41 +
3.42 + val ((((Rs, IRs), ctrAsss), ctrBsss), names_lthy) = lthy
3.43 + |> mk_Frees "R" (map2 mk_pred2T As Bs)
3.44 + ||>> mk_Frees "IR" (map2 mk_pred2T fpA_Ts fpB_Ts)
3.45 + ||>> mk_Freesss "a" ctrAs_Tsss
3.46 + ||>> mk_Freesss "b" ctrBs_Tsss;
3.47 +
3.48 + fun choose_relator AB = the (find_first
3.49 + (fastype_of #> binder_types #> (fn [T1, T2] => AB = (T1, T2))) (Rs @ IRs));
3.50 +
3.51 + val premises =
3.52 + let
3.53 + fun build_the_rel A B = build_rel lthy fpA_Ts choose_relator (A, B);
3.54 + fun build_rel_app a b = build_the_rel (fastype_of a) (fastype_of b) $ a $ b;
3.55 +
3.56 + fun mk_prem ctrA ctrB argAs argBs =
3.57 + fold_rev Logic.all (argAs @ argBs) (fold_rev (curry Logic.mk_implies)
3.58 + (map2 (HOLogic.mk_Trueprop oo build_rel_app) argAs argBs)
3.59 + (HOLogic.mk_Trueprop
3.60 + (build_rel_app (Term.list_comb (ctrA, argAs)) (Term.list_comb (ctrB, argBs)))));
3.61 + in
3.62 + flat (map4 (map4 mk_prem) ctrAss ctrBss ctrAsss ctrBsss)
3.63 + end;
3.64 +
3.65 + val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
3.66 + (map2 mk_leq (map (build_rel lthy [] choose_relator) (fpA_Ts ~~ fpB_Ts)) IRs));
3.67 +
3.68 + val rel_induct0_thm = Goal.prove_sorry lthy [] premises goal
3.69 + (fn {context = ctxt, prems = prems} =>
3.70 + mk_rel_induct0_tac ctxt ctor_rel_induct prems (map (certify ctxt) IRs)
3.71 + (map #exhaust ctr_sugars) ctor_defss ctor_injects pre_rel_defs abs_inverses
3.72 + live_nesting_rel_eqs)
3.73 + |> singleton (Proof_Context.export names_lthy lthy)
3.74 + |> Thm.close_derivation;
3.75 + in
3.76 + (postproc_co_induct lthy (length fpA_Ts) @{thm predicate2D} @{thm predicate2D_conj}
3.77 + rel_induct0_thm,
3.78 + mk_induct_attrs ctrAss)
3.79 + end;
3.80 +
3.81 fun derive_induct_recs_thms_for_types pre_bnfs rec_args_typess ctor_induct ctor_rec_thms
3.82 live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses fp_type_definitions
3.83 abs_inverses ctrss ctr_defss recs rec_defs lthy =
3.84 @@ -552,9 +611,6 @@
3.85 `(conj_dests nn) thm
3.86 end;
3.87
3.88 - val induct_cases = quasi_unambiguous_case_names (maps (map name_of_ctr) ctrss);
3.89 - val induct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names induct_cases));
3.90 -
3.91 val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss;
3.92
3.93 fun mk_rec_thmss (_, x_Tssss, fss, _) recs rec_defs ctor_rec_thms =
3.94 @@ -594,11 +650,11 @@
3.95
3.96 val rec_thmss = mk_rec_thmss (the rec_args_typess) recs rec_defs ctor_rec_thms;
3.97 in
3.98 - ((induct_thms, induct_thm, [induct_case_names_attr]),
3.99 + ((induct_thms, induct_thm, mk_induct_attrs ctrss),
3.100 (rec_thmss, code_nitpicksimp_attrs @ simp_attrs))
3.101 end;
3.102
3.103 -fun coinduct_attrs fpTs ctr_sugars mss =
3.104 +fun mk_coinduct_attrs fpTs ctr_sugars mss =
3.105 let
3.106 val nn = length fpTs;
3.107 val fp_b_names = map base_name_of_typ fpTs;
3.108 @@ -635,16 +691,8 @@
3.109 (coinduct_attrs, common_coinduct_attrs)
3.110 end;
3.111
3.112 -fun postproc_coinduct nn prop prop_conj =
3.113 - Drule.zero_var_indexes
3.114 - #> `(conj_dests nn)
3.115 - #>> map (fn thm => Thm.permute_prems 0 nn (thm RS prop))
3.116 - ##> (fn thm => Thm.permute_prems 0 nn
3.117 - (if nn = 1 then thm RS prop
3.118 - else funpow nn (fn thm => reassoc_conjs (thm RS prop_conj)) thm));
3.119 -
3.120 -fun derive_rel_coinduct0_thm_for_types lthy fpA_Ts ns As Bs mss ctr_sugars abs_inverses abs_injects
3.121 - ctor_injects dtor_ctors rel_pre_defs ctor_defss dtor_rel_coinduct =
3.122 +fun derive_rel_coinduct_thm_for_types lthy fpA_Ts ns As Bs mss ctr_sugars abs_inverses abs_injects
3.123 + ctor_injects dtor_ctors rel_pre_defs ctor_defss dtor_rel_coinduct live_nesting_rel_eqs =
3.124 let
3.125 val fpB_Ts = map (typ_subst_nonatomic (As ~~ Bs)) fpA_Ts;
3.126
3.127 @@ -713,12 +761,13 @@
3.128 mk_rel_coinduct0_tac ctxt dtor_rel_coinduct (map (certify ctxt) IRs) prems
3.129 (map #exhaust ctr_sugars) (map (flat o #disc_thmss) ctr_sugars)
3.130 (map (flat o #sel_thmss) ctr_sugars) ctor_defss dtor_ctors ctor_injects abs_injects
3.131 - rel_pre_defs abs_inverses)
3.132 + rel_pre_defs abs_inverses live_nesting_rel_eqs)
3.133 |> singleton (Proof_Context.export names_lthy lthy)
3.134 |> Thm.close_derivation;
3.135 in
3.136 - (postproc_coinduct (length fpA_Ts) @{thm predicate2D} @{thm predicate2D_conj} rel_coinduct0_thm,
3.137 - coinduct_attrs fpA_Ts ctr_sugars mss)
3.138 + (postproc_co_induct lthy (length fpA_Ts) @{thm predicate2D} @{thm predicate2D_conj}
3.139 + rel_coinduct0_thm,
3.140 + mk_coinduct_attrs fpA_Ts ctr_sugars mss)
3.141 end;
3.142
3.143 fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, ((pgss, cqgsss), _))
3.144 @@ -817,7 +866,7 @@
3.145 val dtor_coinducts =
3.146 [dtor_coinduct, mk_strong_coinduct_thm dtor_coinduct rel_eqs rel_monos mk_vimage2p lthy]
3.147 in
3.148 - map2 (postproc_coinduct nn mp mp_conj oo prove) dtor_coinducts goals
3.149 + map2 (postproc_co_induct lthy nn mp mp_conj oo prove) dtor_coinducts goals
3.150 end;
3.151
3.152 fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
3.153 @@ -912,7 +961,7 @@
3.154
3.155 val sel_corec_thmsss = mk_sel_corec_thms corec_thmss;
3.156 in
3.157 - ((coinduct_thms_pairs, coinduct_attrs fpTs ctr_sugars mss),
3.158 + ((coinduct_thms_pairs, mk_coinduct_attrs fpTs ctr_sugars mss),
3.159 (corec_thmss, code_nitpicksimp_attrs),
3.160 (disc_corec_thmss, []),
3.161 (disc_corec_iff_thmss, simp_attrs),
3.162 @@ -1531,17 +1580,37 @@
3.163 abs_inverses ctrss ctr_defss recs rec_defs lthy;
3.164
3.165 val induct_type_attr = Attrib.internal o K o Induct.induct_type;
3.166 + val induct_pred_attr = Attrib.internal o K o Induct.induct_pred;
3.167 +
3.168 + val ((rel_induct_thmss, common_rel_induct_thms),
3.169 + (rel_induct_attrs, common_rel_induct_attrs)) =
3.170 + if live = 0 then
3.171 + ((replicate nn [], []), ([], []))
3.172 + else
3.173 + let
3.174 + val ((rel_induct_thms, common_rel_induct_thm), rel_induct_attrs) =
3.175 + derive_rel_induct_thm_for_types lthy fpTs ns As Bs mss ctrss ctr_Tsss ctr_sugars
3.176 + rel_xtor_co_induct_thm ctr_defss ctor_injects pre_rel_defs abs_inverses
3.177 + (map rel_eq_of_bnf live_nesting_bnfs);
3.178 + in
3.179 + ((map single rel_induct_thms, single common_rel_induct_thm),
3.180 + (rel_induct_attrs, rel_induct_attrs))
3.181 + end;
3.182
3.183 val simp_thmss =
3.184 map6 mk_simp_thms ctr_sugars rec_thmss mapss rel_injectss rel_distinctss setss;
3.185
3.186 val common_notes =
3.187 - (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])
3.188 + (if nn > 1 then
3.189 + [(inductN, [induct_thm], induct_attrs),
3.190 + (rel_inductN, common_rel_induct_thms, common_rel_induct_attrs)]
3.191 + else [])
3.192 |> massage_simple_notes fp_common_name;
3.193
3.194 val notes =
3.195 [(inductN, map single induct_thms, fn T_name => induct_attrs @ [induct_type_attr T_name]),
3.196 (recN, rec_thmss, K rec_attrs),
3.197 + (rel_inductN, rel_induct_thmss, K (rel_induct_attrs @ [induct_pred_attr ""])),
3.198 (simpsN, simp_thmss, K [])]
3.199 |> massage_multi_notes;
3.200 in
3.201 @@ -1567,11 +1636,6 @@
3.202 ns abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs
3.203 (Proof_Context.export lthy' no_defs_lthy) lthy;
3.204
3.205 - val ((rel_coinduct_thms, rel_coinduct_thm),
3.206 - (rel_coinduct_attrs, common_rel_coinduct_attrs)) =
3.207 - derive_rel_coinduct0_thm_for_types lthy fpTs ns As Bs mss ctr_sugars abs_inverses
3.208 - abs_injects ctor_injects dtor_ctors pre_rel_defs ctr_defss rel_xtor_co_induct_thm;
3.209 -
3.210 val sel_corec_thmss = map flat sel_corec_thmsss;
3.211
3.212 val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
3.213 @@ -1579,6 +1643,22 @@
3.214
3.215 val flat_corec_thms = append oo append;
3.216
3.217 + val ((rel_coinduct_thmss, common_rel_coinduct_thms),
3.218 + (rel_coinduct_attrs, common_rel_coinduct_attrs)) =
3.219 + if live = 0 then
3.220 + ((replicate nn [], []), ([], []))
3.221 + else
3.222 + let
3.223 + val ((rel_coinduct_thms, common_rel_coinduct_thm),
3.224 + (rel_coinduct_attrs, common_rel_coinduct_attrs)) =
3.225 + derive_rel_coinduct_thm_for_types lthy fpTs ns As Bs mss ctr_sugars abs_inverses
3.226 + abs_injects ctor_injects dtor_ctors pre_rel_defs ctr_defss rel_xtor_co_induct_thm
3.227 + (map rel_eq_of_bnf live_nesting_bnfs)
3.228 + in
3.229 + ((map single rel_coinduct_thms, single common_rel_coinduct_thm),
3.230 + (rel_coinduct_attrs, common_rel_coinduct_attrs))
3.231 + end;
3.232 +
3.233 val simp_thmss =
3.234 map6 mk_simp_thms ctr_sugars
3.235 (map3 flat_corec_thms disc_corec_thmss disc_corec_iff_thmss sel_corec_thmss)
3.236 @@ -1586,21 +1666,19 @@
3.237
3.238 val common_notes =
3.239 (if nn > 1 then
3.240 - [(rel_coinductN, [rel_coinduct_thm], common_rel_coinduct_attrs),
3.241 - (coinductN, [coinduct_thm], common_coinduct_attrs),
3.242 + [(coinductN, [coinduct_thm], common_coinduct_attrs),
3.243 + (rel_coinductN, common_rel_coinduct_thms, common_rel_coinduct_attrs),
3.244 (strong_coinductN, [strong_coinduct_thm], common_coinduct_attrs)]
3.245 - else
3.246 - [])
3.247 + else [])
3.248 |> massage_simple_notes fp_common_name;
3.249
3.250 val notes =
3.251 [(coinductN, map single coinduct_thms,
3.252 fn T_name => coinduct_attrs @ [coinduct_type_attr T_name]),
3.253 - (rel_coinductN, map single rel_coinduct_thms,
3.254 - K (rel_coinduct_attrs @ [coinduct_pred_attr ""])),
3.255 (corecN, corec_thmss, K corec_attrs),
3.256 (disc_corecN, disc_corec_thmss, K disc_corec_attrs),
3.257 (disc_corec_iffN, disc_corec_iff_thmss, K disc_corec_iff_attrs),
3.258 + (rel_coinductN, rel_coinduct_thmss, K (rel_coinduct_attrs @ [coinduct_pred_attr ""])),
3.259 (sel_corecN, sel_corec_thmss, K sel_corec_attrs),
3.260 (simpsN, simp_thmss, K []),
3.261 (strong_coinductN, map single strong_coinduct_thms, K coinduct_attrs)]
4.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Jul 01 16:26:14 2014 +0200
4.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Jul 01 17:01:28 2014 +0200
4.3 @@ -28,7 +28,9 @@
4.4 tactic
4.5 val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list ->
4.6 thm list list -> thm list list -> thm list list -> thm list -> thm list -> thm list ->
4.7 - thm list -> thm list -> tactic
4.8 + thm list -> thm list -> thm list -> tactic
4.9 + val mk_rel_induct0_tac: Proof.context -> thm -> thm list -> cterm list -> thm list ->
4.10 + thm list list -> thm list -> thm list -> thm list -> thm list -> tactic
4.11 val mk_sel_map_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
4.12 val mk_sel_set_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
4.13 val mk_set_empty_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
4.14 @@ -210,7 +212,7 @@
4.15 selsss));
4.16
4.17 fun mk_rel_coinduct0_tac ctxt dtor_rel_coinduct cts assms exhausts discss selss ctor_defss
4.18 - dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses =
4.19 + dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses nesting_rel_eqs =
4.20 rtac dtor_rel_coinduct 1 THEN
4.21 EVERY (map11 (fn ct => fn assm => fn exhaust => fn discs => fn sels => fn ctor_defs =>
4.22 fn dtor_ctor => fn ctor_inject => fn abs_inject => fn rel_pre_def => fn abs_inverse =>
4.23 @@ -222,14 +224,29 @@
4.24 Local_Defs.unfold_tac ctxt ((discs RL @{thms iffD2[OF eq_True] iffD2[OF eq_False]}) @ sels
4.25 @ simp_thms') THEN
4.26 Local_Defs.unfold_tac ctxt (dtor_ctor :: rel_pre_def :: abs_inverse :: ctor_inject ::
4.27 - abs_inject :: ctor_defs @ simp_thms' @ @{thms BNF_Comp.id_bnf_comp_def rel_sum_simps
4.28 - rel_prod_apply vimage2p_def Inl_Inr_False iffD2[OF eq_False Inr_not_Inl] sum.inject
4.29 - prod.inject}) THEN
4.30 + abs_inject :: ctor_defs @ nesting_rel_eqs @ simp_thms' @ @{thms BNF_Comp.id_bnf_comp_def
4.31 + rel_sum_simps rel_prod_apply vimage2p_def Inl_Inr_False iffD2[OF eq_False Inr_not_Inl]
4.32 + sum.inject prod.inject}) THEN
4.33 REPEAT_DETERM (HEADGOAL ((REPEAT_DETERM o etac conjE) THEN' (REPEAT_DETERM o rtac conjI) THEN'
4.34 (rtac refl ORELSE' atac))))
4.35 cts assms exhausts discss selss ctor_defss dtor_ctors ctor_injects abs_injects rel_pre_defs
4.36 abs_inverses);
4.37
4.38 +fun mk_rel_induct0_tac ctxt ctor_rel_induct assms cterms exhausts ctor_defss ctor_injects
4.39 + rel_pre_list_defs Abs_inverses nesting_rel_eqs =
4.40 + rtac ctor_rel_induct 1 THEN EVERY (map6 (fn cterm => fn exhaust => fn ctor_defs =>
4.41 + fn ctor_inject => fn rel_pre_list_def => fn Abs_inverse =>
4.42 + HEADGOAL (rtac exhaust THEN_ALL_NEW (rtac exhaust THEN_ALL_NEW
4.43 + (rtac (cterm_instantiate_pos (replicate 4 NONE @ [SOME cterm]) @{thm arg_cong2} RS iffD2)
4.44 + THEN' atac THEN' atac THEN' TRY o resolve_tac assms))) THEN
4.45 + unfold_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @
4.46 + @{thms BNF_Comp.id_bnf_comp_def vimage2p_def}) THEN
4.47 + TRYALL (hyp_subst_tac ctxt) THEN
4.48 + unfold_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_apply Inl_Inr_False
4.49 + Inr_Inl_False sum.inject prod.inject}) THEN
4.50 + TRYALL (etac FalseE ORELSE' (REPEAT_DETERM o etac conjE) THEN' atac))
4.51 + cterms exhausts ctor_defss ctor_injects rel_pre_list_defs Abs_inverses);
4.52 +
4.53 fun mk_sel_map_tac ctxt ct exhaust discs maps sels =
4.54 TRYALL Goal.conjunction_tac THEN
4.55 ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW