diff -r d71774989c4a -r 4ceda7d0c955 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Feb 23 18:04:38 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Feb 23 19:05:18 2016 +0100 @@ -138,6 +138,10 @@ BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> typ list -> typ list list list -> thm list -> thm list -> thm list -> term list list -> thm list list -> term list -> thm list -> Proof.context -> lfp_sugar_thms + val derive_coinduct_thms_for_types: bool -> (term -> term) -> BNF_Def.bnf list -> thm -> + thm list -> BNF_Def.bnf list -> typ list -> typ list -> typ list list list -> int list -> + thm list -> thm list -> (thm -> thm) -> thm list list -> Ctr_Sugar.ctr_sugar list -> + Proof.context -> (thm list * thm) list val derive_coinduct_corecs_thms_for_types: BNF_Def.bnf list -> string * term list * term list list * (((term list list * term list list * term list list list list * term list list list list) @@ -1590,7 +1594,6 @@ fun mk_coinduct_attrs fpTs ctrss discss mss = let - val nn = length fpTs; val fp_b_names = map base_name_of_typ fpTs; fun mk_coinduct_concls ms discs ctrs = @@ -1805,35 +1808,24 @@ |> unfold_thms ctxt unfolds end; -fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, (((pgss, _, _, _), cqgsss), _)) - dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss - kss mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list) - corecs corec_defs lthy = +fun derive_coinduct_thms_for_types strong alter_r pre_bnfs dtor_coinduct dtor_ctors + live_nesting_bnfs fpTs Xs ctrXs_Tsss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss + (ctr_sugars : ctr_sugar list) ctxt = let - fun mk_ctor_dtor_corec_thm dtor_inject dtor_ctor corec = - iffD1 OF [dtor_inject, trans OF [corec, dtor_ctor RS sym]]; - - val ctor_dtor_corec_thms = - @{map 3} mk_ctor_dtor_corec_thm dtor_injects dtor_ctors dtor_corec_thms; - val nn = length pre_bnfs; - val pre_map_defs = map map_def_of_bnf pre_bnfs; val pre_rel_defs = map rel_def_of_bnf pre_bnfs; - val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs; val live_nesting_rel_eqs = map rel_eq_of_bnf live_nesting_bnfs; val fp_b_names = map base_name_of_typ fpTs; - val ctrss = map #ctrs ctr_sugars; val discss = map #discs ctr_sugars; val selsss = map #selss ctr_sugars; val exhausts = map #exhaust ctr_sugars; val disc_thmsss = map #disc_thmss ctr_sugars; - val discIss = map #discIs ctr_sugars; val sel_thmsss = map #sel_thmss ctr_sugars; - val (((rs, us'), vs'), _) = lthy + val (((rs, us'), vs'), _) = ctxt |> mk_Frees "R" (map (fn T => mk_pred2T T T) fpTs) ||>> Variable.variant_fixes fp_b_names ||>> Variable.variant_fixes (map (suffix "'") fp_b_names); @@ -1846,65 +1838,91 @@ val vdiscss = map2 (map o rapp) vs discss; val vselsss = map2 (map o map o rapp) vs selsss; - val coinduct_thms_pairs = - let - val uvrs = @{map 3} (fn r => fn u => fn v => r $ u $ v) rs us vs; - val uv_eqs = map2 (curry HOLogic.mk_eq) us vs; - val strong_rs = - @{map 4} (fn u => fn v => fn uvr => fn uv_eq => - fold_rev Term.lambda [u, v] (HOLogic.mk_disj (uvr, uv_eq))) us vs uvrs uv_eqs; - - fun build_the_rel rs' T Xs_T = - build_rel [] lthy [] (fn (_, X) => nth rs' (find_index (curry (op =) X) Xs)) (T, Xs_T) - |> Term.subst_atomic_types (Xs ~~ fpTs); - - fun build_rel_app rs' usel vsel Xs_T = - fold rapp [usel, vsel] (build_the_rel rs' (fastype_of usel) Xs_T); - - fun mk_prem_ctr_concls rs' n k udisc usels vdisc vsels ctrXs_Ts = - (if k = n then [] else [HOLogic.mk_eq (udisc, vdisc)]) @ - (if null usels then - [] - else - [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [udisc, vdisc], - Library.foldr1 HOLogic.mk_conj - (@{map 3} (build_rel_app rs') usels vsels ctrXs_Ts))]); - - fun mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss = - Library.foldr1 HOLogic.mk_conj (flat (@{map 6} (mk_prem_ctr_concls rs' n) - (1 upto n) udiscs uselss vdiscs vselss ctrXs_Tss)) - handle List.Empty => @{term True}; - - fun mk_prem rs' uvr u v n udiscs uselss vdiscs vselss ctrXs_Tss = - fold_rev Logic.all [u, v] (Logic.mk_implies (HOLogic.mk_Trueprop uvr, - HOLogic.mk_Trueprop (mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss))); - - val concl = - HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (@{map 3} (fn uvr => fn u => fn v => HOLogic.mk_imp (uvr, HOLogic.mk_eq (u, v))) - uvrs us vs)); - - fun mk_goal rs' = - Logic.list_implies (@{map 9} (mk_prem rs') uvrs us vs ns udiscss uselsss vdiscss vselsss - ctrXs_Tsss, concl); - - val goals = map mk_goal [rs, strong_rs]; - val varss = map (fn goal => Variable.add_free_names lthy goal []) goals; - - fun prove dtor_coinduct' goal vars = - Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} => - mk_coinduct_tac ctxt live_nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs - fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss disc_thmsss sel_thmsss) - |> Thm.close_derivation; - - val rel_eqs = map rel_eq_of_bnf pre_bnfs; - val rel_monos = map rel_mono_of_bnf pre_bnfs; - val dtor_coinducts = - [dtor_coinduct, mk_coinduct_strong_thm dtor_coinduct rel_eqs rel_monos mk_vimage2p lthy] - in - @{map 3} (postproc_co_induct lthy nn mp @{thm conj_commute[THEN iffD1]} ooo prove) - dtor_coinducts goals varss - end; + val uvrs = @{map 3} (fn r => fn u => fn v => r $ u $ v) rs us vs; + val uv_eqs = map2 (curry HOLogic.mk_eq) us vs; + val strong_rs = + @{map 4} (fn u => fn v => fn uvr => fn uv_eq => + fold_rev Term.lambda [u, v] (HOLogic.mk_disj (uvr, uv_eq))) us vs uvrs uv_eqs; + + fun build_the_rel rs' T Xs_T = + build_rel [] ctxt [] (fn (_, X) => nth rs' (find_index (curry (op =) X) Xs)) (T, Xs_T) + |> Term.subst_atomic_types (Xs ~~ fpTs); + + fun build_rel_app rs' usel vsel Xs_T = + fold rapp [usel, vsel] (build_the_rel rs' (fastype_of usel) Xs_T); + + fun mk_prem_ctr_concls rs' n k udisc usels vdisc vsels ctrXs_Ts = + (if k = n then [] else [HOLogic.mk_eq (udisc, vdisc)]) @ + (if null usels then + [] + else + [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [udisc, vdisc], + Library.foldr1 HOLogic.mk_conj (@{map 3} (build_rel_app rs') usels vsels ctrXs_Ts))]); + + fun mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss = + flat (@{map 6} (mk_prem_ctr_concls rs' n) (1 upto n) udiscs uselss vdiscs vselss ctrXs_Tss) + |> Library.foldr1 HOLogic.mk_conj + handle List.Empty => @{term True}; + + fun mk_prem rs' uvr u v n udiscs uselss vdiscs vselss ctrXs_Tss = + fold_rev Logic.all [u, v] (Logic.mk_implies (HOLogic.mk_Trueprop uvr, + HOLogic.mk_Trueprop (mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss))); + + val concl = + HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj + (@{map 3} (fn uvr => fn u => fn v => HOLogic.mk_imp (uvr, HOLogic.mk_eq (u, v))) + uvrs us vs)); + + fun mk_goal rs0' = + Logic.list_implies (@{map 9} (mk_prem (map alter_r rs0')) uvrs us vs ns udiscss uselsss + vdiscss vselsss ctrXs_Tsss, concl); + + val goals = map mk_goal ([rs] @ (if strong then [strong_rs] else [])); + + fun prove dtor_coinduct' goal = + Variable.add_free_names ctxt goal [] + |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, ...} => + mk_coinduct_tac ctxt live_nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs fp_abs_inverses + abs_inverses dtor_ctors exhausts ctr_defss disc_thmsss sel_thmsss)) + |> Thm.close_derivation; + + val rel_eqs = map rel_eq_of_bnf pre_bnfs; + val rel_monos = map rel_mono_of_bnf pre_bnfs; + val dtor_coinducts = + [dtor_coinduct] @ + (if strong then [mk_coinduct_strong_thm dtor_coinduct rel_eqs rel_monos mk_vimage2p ctxt] + else []); + in + map2 (postproc_co_induct ctxt nn mp @{thm conj_commute[THEN iffD1]} oo prove) + dtor_coinducts goals + end; + +fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, (((pgss, _, _, _), cqgsss), _)) + dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss + kss mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list) + corecs corec_defs ctxt = + let + fun mk_ctor_dtor_corec_thm dtor_inject dtor_ctor corec = + iffD1 OF [dtor_inject, trans OF [corec, dtor_ctor RS sym]]; + + val ctor_dtor_corec_thms = + @{map 3} mk_ctor_dtor_corec_thm dtor_injects dtor_ctors dtor_corec_thms; + + val pre_map_defs = map map_def_of_bnf pre_bnfs; + val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs; + + val fp_b_names = map base_name_of_typ fpTs; + + val ctrss = map #ctrs ctr_sugars; + val discss = map #discs ctr_sugars; + val selsss = map #selss ctr_sugars; + val disc_thmsss = map #disc_thmss ctr_sugars; + val discIss = map #discIs ctr_sugars; + val sel_thmsss = map #sel_thmss ctr_sugars; + + val coinduct_thms_pairs = derive_coinduct_thms_for_types true I pre_bnfs dtor_coinduct + dtor_ctors live_nesting_bnfs fpTs Xs ctrXs_Tsss ns fp_abs_inverses abs_inverses mk_vimage2p + ctr_defss ctr_sugars ctxt; fun mk_maybe_not pos = not pos ? HOLogic.mk_not; @@ -1912,6 +1930,11 @@ val corec_thmss = let + val (us', _) = ctxt + |> Variable.variant_fixes fp_b_names; + + val us = map2 (curry Free) us' fpTs; + fun mk_goal c cps gcorec n k ctr m cfs' = fold_rev (fold_rev Logic.all) ([c] :: pgss) (Logic.list_implies (seq_conds (HOLogic.mk_Trueprop oo mk_maybe_not) n k cps, @@ -1933,7 +1956,7 @@ indexify fst (map2 (curry mk_sumT) fpTs Cs) (fn kk => fn _ => tack (nth cs kk, nth us kk) (nth gcorecs kk)); in - build_map lthy [] build_simple (T, U) $ cqg + build_map ctxt [] build_simple (T, U) $ cqg end else cqg @@ -1947,11 +1970,11 @@ ctor_dtor_corec_thms pre_map_defs abs_inverses ctr_defss; fun prove goal tac = - Goal.prove_sorry lthy [] [] goal (tac o #context) + Goal.prove_sorry ctxt [] [] goal (tac o #context) |> Thm.close_derivation; in map2 (map2 prove) goalss tacss - |> map (map (unfold_thms lthy @{thms case_sum_if})) + |> map (map (unfold_thms ctxt @{thms case_sum_if})) end; val corec_disc_iff_thmss = @@ -1963,15 +1986,15 @@ val goalss = @{map 6} (map2 oooo mk_goal) cs cpss gcorecs ns kss discss; - fun mk_case_split' cp = Thm.instantiate' [] [SOME (Thm.cterm_of lthy cp)] @{thm case_split}; + fun mk_case_split' cp = Thm.instantiate' [] [SOME (Thm.cterm_of ctxt cp)] @{thm case_split}; val case_splitss' = map (map mk_case_split') cpss; val tacss = @{map 3} (map oo mk_corec_disc_iff_tac) case_splitss' corec_thmss disc_thmsss; fun prove goal tac = - Variable.add_free_names lthy goal [] - |> (fn vars => Goal.prove_sorry lthy vars [] goal (tac o #context)) + Variable.add_free_names ctxt goal [] + |> (fn vars => Goal.prove_sorry ctxt vars [] goal (tac o #context)) |> Thm.close_derivation; fun proves [_] [_] = [] @@ -1988,8 +2011,8 @@ let val (domT, ranT) = dest_funT (fastype_of sel); val arg_cong' = - Thm.instantiate' (map (SOME o Thm.ctyp_of lthy) [domT, ranT]) - [NONE, NONE, SOME (Thm.cterm_of lthy sel)] arg_cong + Thm.instantiate' (map (SOME o Thm.ctyp_of ctxt) [domT, ranT]) + [NONE, NONE, SOME (Thm.cterm_of ctxt sel)] arg_cong |> Thm.varifyT_global; val sel_thm' = sel_thm RSN (2, trans); in