--- 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 ());