generalized code (towards nonuniform datatypes)
authorblanchet
Tue Dec 20 16:17:13 2016 +0100 (2016-12-20)
changeset 6460720f3dbfe4b24
parent 64576 ce8802dc3145
child 64608 20ccca53dd73
generalized code (towards nonuniform datatypes)
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Dec 16 22:54:14 2016 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Dec 20 16:17:13 2016 +0100
     1.3 @@ -1648,16 +1648,20 @@
     1.4      val (xs, names_lthy') = names_lthy |> mk_Frees "x" ctr_Ts;
     1.5      val pprems =
     1.6        flat (map2 (mk_induct_raw_prem_prems names_lthy' Xss setss_fp_nesting) xs ctrXs_Ts);
     1.7 -  in (xs, pprems, HOLogic.mk_Trueprop (p $ Term.list_comb (ctr, xs))) end;
     1.8 +    val y = Term.list_comb (ctr, xs);
     1.9 +    val p' = enforce_type names_lthy domain_type (fastype_of y) p;
    1.10 +  in (xs, pprems, HOLogic.mk_Trueprop (p' $ y)) end;
    1.11  
    1.12  fun close_induct_prem_prem nn ps xs t =
    1.13    fold_rev Logic.all (map Free (drop (nn + length xs)
    1.14      (rev (Term.add_frees t (map dest_Free xs @ map_filter (try dest_Free) ps))))) t;
    1.15  
    1.16  fun finish_induct_prem_prem lthy nn ps xs (xysets, (j, x)) =
    1.17 -  close_induct_prem_prem nn ps xs (Logic.list_implies (map (fn (x', (y, set)) =>
    1.18 -      mk_Trueprop_mem (y, set $ x')) xysets,
    1.19 -    HOLogic.mk_Trueprop (enforce_type lthy domain_type (fastype_of x) (nth ps (j - 1)) $ x)));
    1.20 +  let val p' = enforce_type lthy domain_type (fastype_of x) (nth ps (j - 1)) in
    1.21 +    close_induct_prem_prem nn ps xs (Logic.list_implies (map (fn (x', (y, set)) =>
    1.22 +        mk_Trueprop_mem (y, set $ x')) xysets,
    1.23 +      HOLogic.mk_Trueprop (p' $ x)))
    1.24 +  end;
    1.25  
    1.26  fun finish_induct_prem lthy nn ps (xs, raw_pprems, concl) =
    1.27    fold_rev Logic.all xs (Logic.list_implies
    1.28 @@ -1717,7 +1721,7 @@
    1.29    end;
    1.30  
    1.31  fun derive_induct_recs_thms_for_types plugins pre_bnfs rec_args_typess ctor_induct ctor_rec_thms
    1.32 -    live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses fp_type_definitions
    1.33 +    live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses pre_type_definitions
    1.34      abs_inverses ctrss ctr_defss recs rec_defs lthy =
    1.35    let
    1.36      val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss;
    1.37 @@ -1757,7 +1761,7 @@
    1.38  
    1.39          val kksss = map (map (map (fst o snd) o #2)) raw_premss;
    1.40  
    1.41 -        val ctor_induct' = ctor_induct OF (map2 mk_absumprodE fp_type_definitions mss);
    1.42 +        val ctor_induct' = ctor_induct OF (map2 mk_absumprodE pre_type_definitions mss);
    1.43  
    1.44          val thm =
    1.45            Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} =>
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Fri Dec 16 22:54:14 2016 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Dec 20 16:17:13 2016 +0100
     2.3 @@ -10,6 +10,7 @@
     2.4  sig
     2.5    val sumprod_thms_rel: thm list
     2.6  
     2.7 +  val co_induct_inst_as_projs_tac: Proof.context -> int -> tactic
     2.8    val mk_case_transfer_tac: Proof.context -> thm -> thm list -> tactic
     2.9    val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list ->
    2.10      thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list ->