# HG changeset patch # User blanchet # Date 1347617367 -7200 # Node ID cc1d39529dd1c9852cc30860b14d035ab8802b57 # Parent 023be49d7fb80f17ae46ea98024818f0541d0927 derive induction via backward proof, to ensure that the premises are in the right order for constructors like "X x y x" where x and y are mutually recursive diff -r 023be49d7fb8 -r cc1d39529dd1 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 14 10:01:42 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 14 12:09:27 2012 +0200 @@ -95,6 +95,8 @@ else (); val N = length specs; + val fp_bs = map type_binding_of specs; + val fp_common_name = mk_common_name fp_bs; fun prepare_type_arg (ty, c) = let val TFree (s, _) = prepare_typ no_defs_lthy0 ty in @@ -105,11 +107,12 @@ val unsorted_Ass0 = map (map (resort_tfree HOLogic.typeS)) Ass0; val unsorted_As = Library.foldr1 merge_type_args unsorted_Ass0; - val ((Bs, Cs), no_defs_lthy) = + val (((Bs, Cs), vs'), no_defs_lthy) = no_defs_lthy0 |> fold (Variable.declare_typ o resort_tfree dummyS) unsorted_As |> mk_TFrees N - ||>> mk_TFrees N; + ||>> mk_TFrees N + ||>> Variable.variant_fixes (map Binding.name_of fp_bs); (* TODO: cleaner handling of fake contexts, without "background_theory" *) (*the "perhaps o try" below helps gracefully handles the case where the new type is defined in a @@ -123,9 +126,6 @@ Type (fst (Term.dest_Type (Proof_Context.read_type_name fake_lthy true (Binding.name_of b))), unsorted_As); - val fp_bs = map type_binding_of specs; - val fp_common_name = mk_common_name fp_bs; - val fake_Ts = map mk_fake_T fp_bs; val mixfixes = map mixfix_of specs; @@ -204,6 +204,7 @@ val flds = map (mk_fld As) flds0; val fpTs = map (domain_type o fastype_of) unfs; + val vs = map2 (curry Free) vs' fpTs; val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Bs ~~ fpTs)))) ctr_TsssBs; val ns = map length ctr_Tsss; @@ -328,19 +329,18 @@ (mk_terms sssss hssss, (h_sum_prod_Ts, ph_Tss)))) end; - fun define_ctrs_case_for_type ((((((((((((((((((fp_b, fpT), C), fld), unf), fp_iter), fp_rec), - fld_unf), unf_fld), fld_inject), n), ks), ms), ctr_bindings), ctr_mixfixes), ctr_Tss), - disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy = + fun define_ctrs_case_for_type (((((((((((((((((((fp_b, fpT), C), v), fld), unf), fp_iter), + fp_rec), fld_unf), unf_fld), fld_inject), n), ks), ms), ctr_bindings), ctr_mixfixes), + ctr_Tss), disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy = let val unfT = domain_type (fastype_of fld); val ctr_prod_Ts = map HOLogic.mk_tupleT ctr_Tss; val ctr_sum_prod_T = mk_sumTN_balanced ctr_prod_Ts; val case_Ts = map (fn Ts => Ts ---> C) ctr_Tss; - val ((((u, v), fs), xss), _) = + val (((u, fs), xss), _) = no_defs_lthy |> yield_singleton (mk_Frees "u") unfT - ||>> yield_singleton (mk_Frees "v") fpT ||>> mk_Frees "f" case_Ts ||>> mk_Freess "x" ctr_Tss; @@ -518,29 +518,32 @@ let val (induct_thms, induct_thm) = let - val sym_ctr_defss = map2 (map2 fold_def_rule) mss ctr_defss; + val (ps, names_lthy) = + lthy + |> mk_Frees "P" (map mk_predT fpTs); - val ss = @{simpset} |> fold Simplifier.add_simp - @{thms collect_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def] - fsts_def[abs_def] snds_def[abs_def] False_imp_eq all_point_1}; - - val induct_thm0 = fp_induct OF (map mk_sumEN_tupled_balanced mss); + fun mk_prem_prem (x as Free (_, T)) = + map HOLogic.mk_Trueprop + (case find_index (curry (op =) T) fpTs of + ~1 => [] + | i => [nth ps i $ x]); - val spurious_fs = - Term.add_vars (prop_of induct_thm0) [] - |> filter (fn (_, Type (@{type_name fun}, [_, T'])) => T' <> HOLogic.boolT - | _ => false); + fun mk_prem p ctr ctr_Ts = + let val (xs, _) = names_lthy |> mk_Frees "x" ctr_Ts in + fold_rev Logic.all xs + (Logic.list_implies (maps mk_prem_prem xs, + HOLogic.mk_Trueprop (p $ Term.list_comb (ctr, xs)))) + end; - val cxs = - map (fn s as (_, T) => - (certify lthy (Var s), certify lthy (mk_id_fun (domain_type T)))) spurious_fs; + val goal = + fold_rev (fold_rev Logic.all) [ps, vs] + (Library.foldr Logic.list_implies (map3 (map2 o mk_prem) ps ctrss ctr_Tsss, + HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj + (map2 (curry (op $)) ps vs)))); val induct_thm = - Drule.cterm_instantiate cxs induct_thm0 - |> Tactic.rule_by_tactic lthy (ALLGOALS (REPEAT_DETERM o bound_hyp_subst_tac)) - |> Local_Defs.unfold lthy - (@{thm triv_forall_equality} :: flat sym_ctr_defss @ flat pre_set_defss) - |> Simplifier.full_simplify ss; + Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => + Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt)); in `(conj_dests N) induct_thm end; @@ -715,16 +718,17 @@ SOME ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs), [(thms, [])])) (fp_bs ~~ thmss)); in - lthy |> Local_Theory.notes notes |> snd + lthy |> Local_Theory.notes (common_notes @ notes) |> snd end; fun wrap_types_and_define_iter_likes ((wraps, define_iter_likess), lthy) = fold_map2 (curry (op o)) define_iter_likess wraps lthy |>> split_list11 val lthy' = lthy - |> fold_map define_ctrs_case_for_type (fp_bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~ - fp_recs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ns ~~ kss ~~ mss ~~ ctr_bindingss ~~ - ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_defaultsss) + |> fold_map define_ctrs_case_for_type (fp_bs ~~ fpTs ~~ Cs ~~ vs ~~ flds ~~ unfs ~~ + fp_iters ~~ fp_recs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ns ~~ kss ~~ mss ~~ + ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ + raw_sel_defaultsss) |>> split_list |> wrap_types_and_define_iter_likes |> (if lfp then derive_induct_iter_rec_thms_for_types else derive_coinduct_coiter_corec_thms_for_types);