generalized generation of coinduction goal (towards nonuniform codatatypes)
authorblanchet
Fri Dec 23 00:13:30 2016 +0100 (2016-12-23)
changeset 64638235df39ade87
parent 64637 a15785625f7c
child 64669 ce441970956f
generalized generation of coinduction goal (towards nonuniform codatatypes)
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Dec 22 19:14:58 2016 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Dec 23 00:13:30 2016 +0100
     1.3 @@ -168,9 +168,9 @@
     1.4      term list * ((term * (term * term)) list * (int * term)) list * term
     1.5    val finish_induct_prem: Proof.context -> int -> term list ->
     1.6      term list * ((term * (term * term)) list * (int * term)) list * term -> term
     1.7 -  val mk_coinduct_prem: Proof.context -> typ list -> typ list -> term list -> term -> term ->
     1.8 -    term -> int -> term list -> term list list -> term list -> term list list -> typ list list ->
     1.9 -    term
    1.10 +  val mk_coinduct_prem: Proof.context -> typ list list -> typ list list -> term list -> term ->
    1.11 +    term -> term -> int -> term list -> term list list -> term list -> term list list ->
    1.12 +    typ list list -> term
    1.13    val mk_induct_attrs: term list list -> Token.src list
    1.14    val mk_coinduct_attrs: typ list -> term list list -> term list list -> int list list ->
    1.15      Token.src list * Token.src list
    1.16 @@ -1646,12 +1646,12 @@
    1.17      [([], (find_index (fn Xs => member (op =) Xs X) Xss + 1, x))]
    1.18    | mk_induct_raw_prem_prems _ _ _ _ _ = [];
    1.19  
    1.20 -fun mk_induct_raw_prem modify_x names_ctxt Xss setss_fp_nesting p ctr ctr_Ts ctrXs_Ts =
    1.21 +fun mk_induct_raw_prem alter_x names_ctxt Xss setss_fp_nesting p ctr ctr_Ts ctrXs_Ts =
    1.22    let
    1.23      val (xs, names_ctxt') = names_ctxt |> mk_Frees "x" ctr_Ts;
    1.24      val pprems =
    1.25        flat (map2 (mk_induct_raw_prem_prems names_ctxt' Xss setss_fp_nesting) xs ctrXs_Ts);
    1.26 -    val y = Term.list_comb (ctr, map modify_x xs);
    1.27 +    val y = Term.list_comb (ctr, map alter_x xs);
    1.28      val p' = enforce_type names_ctxt domain_type (fastype_of y) p;
    1.29    in (xs, pprems, HOLogic.mk_Trueprop (p' $ y)) end;
    1.30  
    1.31 @@ -1670,31 +1670,34 @@
    1.32    fold_rev Logic.all xs (Logic.list_implies
    1.33      (map (finish_induct_prem_prem ctxt nn ps xs) raw_pprems, concl));
    1.34  
    1.35 -fun mk_coinduct_prem_ctr_concls ctxt Xs fpTs rs' n k udisc usels vdisc vsels ctrXs_Ts =
    1.36 +fun mk_coinduct_prem_ctr_concls ctxt Xss fpTss rs' n k udisc usels vdisc vsels ctrXs_Ts =
    1.37    let
    1.38 -    fun build_the_rel rs' T Xs_T =
    1.39 -      build_rel [] ctxt [] [] (fn (_, X) => nth rs' (find_index (curry (op =) X) Xs)) (T, Xs_T)
    1.40 -      |> Term.subst_atomic_types (Xs ~~ fpTs);
    1.41 -    fun build_rel_app rs' usel vsel Xs_T =
    1.42 -      fold rapp [usel, vsel] (build_the_rel rs' (fastype_of usel) Xs_T);
    1.43 +    fun build_the_rel T Xs_T =
    1.44 +      build_rel [] ctxt [] [] (fn (T, X) =>
    1.45 +          nth rs' (find_index (fn Xs => member (op =) Xs X) Xss)
    1.46 +          |> enforce_type ctxt domain_type T)
    1.47 +        (T, Xs_T)
    1.48 +      |> Term.subst_atomic_types (flat Xss ~~ flat fpTss);
    1.49 +    fun build_rel_app usel vsel Xs_T =
    1.50 +      fold rapp [usel, vsel] (build_the_rel (fastype_of usel) Xs_T);
    1.51    in
    1.52      (if k = n then [] else [HOLogic.mk_eq (udisc, vdisc)]) @
    1.53      (if null usels then
    1.54         []
    1.55       else
    1.56         [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [udisc, vdisc],
    1.57 -          Library.foldr1 HOLogic.mk_conj (@{map 3} (build_rel_app rs') usels vsels ctrXs_Ts))])
    1.58 +          Library.foldr1 HOLogic.mk_conj (@{map 3} build_rel_app usels vsels ctrXs_Ts))])
    1.59    end;
    1.60  
    1.61 -fun mk_coinduct_prem_concl ctxt Xs fpTs rs' n udiscs uselss vdiscs vselss ctrXs_Tss =
    1.62 -  @{map 6} (mk_coinduct_prem_ctr_concls ctxt Xs fpTs rs' n)
    1.63 +fun mk_coinduct_prem_concl ctxt Xss fpTss rs' n udiscs uselss vdiscs vselss ctrXs_Tss =
    1.64 +  @{map 6} (mk_coinduct_prem_ctr_concls ctxt Xss fpTss rs' n)
    1.65      (1 upto n) udiscs uselss vdiscs vselss ctrXs_Tss
    1.66    |> flat |> Library.foldr1 HOLogic.mk_conj
    1.67    handle List.Empty => @{term True};
    1.68  
    1.69 -fun mk_coinduct_prem ctxt Xs fpTs rs' uvr u v n udiscs uselss vdiscs vselss ctrXs_Tss =
    1.70 +fun mk_coinduct_prem ctxt Xss fpTss rs' uvr u v n udiscs uselss vdiscs vselss ctrXs_Tss =
    1.71    fold_rev Logic.all [u, v] (Logic.mk_implies (HOLogic.mk_Trueprop uvr,
    1.72 -    HOLogic.mk_Trueprop (mk_coinduct_prem_concl ctxt Xs fpTs rs' n udiscs uselss vdiscs vselss
    1.73 +    HOLogic.mk_Trueprop (mk_coinduct_prem_concl ctxt Xss fpTss rs' n udiscs uselss vdiscs vselss
    1.74        ctrXs_Tss)));
    1.75  
    1.76  fun postproc_co_induct ctxt nn prop prop_conj =
    1.77 @@ -2105,7 +2108,8 @@
    1.78             uvrs us vs))
    1.79  
    1.80      fun mk_goal rs0' =
    1.81 -      Logic.list_implies (@{map 9} (mk_coinduct_prem ctxt Xs fpTs (map alter_r rs0'))
    1.82 +      Logic.list_implies (@{map 9} (mk_coinduct_prem ctxt (map single Xs) (map single fpTs)
    1.83 +            (map alter_r rs0'))
    1.84            uvrs us vs ns udiscss uselsss vdiscss vselsss ctrXs_Tsss,
    1.85          concl);
    1.86