# HG changeset patch # User blanchet # Date 1347617367 -7200 # Node ID be6e749fd003eb5ee395309c091f6a14a30104a0 # Parent d9800bc28427cbbcd4be60c9f3632d5ea514089f fixed variable exporting problem diff -r d9800bc28427 -r be6e749fd003 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 14 12:09:27 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 14 12:09:27 2012 +0200 @@ -34,9 +34,9 @@ val simp_attrs = @{attributes [simp]}; -fun split_list11 xs = +fun split_list10 xs = (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs, map #8 xs, - map #9 xs, map #10 xs, map #11 xs); + map #9 xs, map #10 xs); fun strip_map_type (Type (@{type_name fun}, [T as Type _, T'])) = strip_map_type T' |>> cons T | strip_map_type T = ([], T); @@ -102,12 +102,11 @@ val unsorted_Ass0 = map (map (resort_tfree HOLogic.typeS)) Ass0; val unsorted_As = Library.foldr1 merge_type_args unsorted_Ass0; - val (((Bs, Cs), vs'), no_defs_lthy) = + val ((Bs, Cs), no_defs_lthy) = no_defs_lthy0 |> fold (Variable.declare_typ o resort_tfree dummyS) unsorted_As |> mk_TFrees nn - ||>> mk_TFrees nn - ||>> Variable.variant_fixes (map Binding.name_of fp_bs); + ||>> mk_TFrees nn; (* 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 @@ -205,8 +204,6 @@ val exists_fp_subtype = exists_subtype (member (op =) fpTs); - 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; val kss = map (fn n => 1 upto n) ns; @@ -330,20 +327,23 @@ (mk_terms sssss hssss, (h_sum_prod_Ts, ph_Tss)))) end; - 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 = + 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 = 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, fs), xss), _) = + val ((((u, fs), xss), v'), _) = no_defs_lthy |> yield_singleton (mk_Frees "u") unfT ||>> mk_Frees "f" case_Ts - ||>> mk_Freess "x" ctr_Tss; + ||>> mk_Freess "x" ctr_Tss + ||>> yield_singleton (Variable.variant_fixes) (Binding.name_of fp_b); + + val v = Free (v', fpT); val ctr_rhss = map2 (fn k => fn xs => fold_rev Term.lambda xs (fld $ @@ -441,8 +441,7 @@ val [iter, recx] = map (mk_iter_like As Cs o Morphism.term phi) csts; in - ((ctrs, selss0, iter, recx, v, xss, ctr_defs, discIs, sel_thmss, iter_def, rec_def), - lthy) + ((ctrs, selss0, iter, recx, xss, ctr_defs, discIs, sel_thmss, iter_def, rec_def), lthy) end; fun define_coiter_corec ((selss0, discIs, sel_thmss), no_defs_lthy) = @@ -482,8 +481,8 @@ val [coiter, corec] = map (mk_iter_like As Cs o Morphism.term phi) csts; in - ((ctrs, selss0, coiter, corec, v, xss, ctr_defs, discIs, sel_thmss, coiter_def, - corec_def), lthy) + ((ctrs, selss0, coiter, corec, xss, ctr_defs, discIs, sel_thmss, coiter_def, corec_def), + lthy) end; fun wrap lthy = @@ -516,9 +515,16 @@ val args = map build_arg TUs; in Term.list_comb (mapx, args) end; - fun derive_induct_iter_rec_thms_for_types ((ctrss, _, iters, recs, vs, xsss, ctr_defss, _, _, + fun derive_induct_iter_rec_thms_for_types ((ctrss, _, iters, recs, xsss, ctr_defss, _, _, iter_defs, rec_defs), lthy) = let + val (((phis, phis'), vs'), names_lthy) = + lthy + |> mk_Frees' "P" (map mk_predT fpTs) + ||>> Variable.variant_fixes (map Binding.name_of fp_bs); + + val vs = map2 (curry Free) vs' fpTs; + fun mk_sets_nested bnf = let val Type (T_name, Us) = T_of_bnf bnf; @@ -536,10 +542,6 @@ val (induct_thms, induct_thm) = let - val ((phis, phis'), names_lthy) = - lthy - |> mk_Frees' "P" (map mk_predT fpTs); - fun mk_set Ts t = let val Type (_, Ts0) = domain_type (fastype_of t) in Term.subst_atomic_types (Ts0 ~~ Ts) t @@ -597,9 +599,7 @@ Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => mk_induct_tac ctxt ns mss rss (flat ctr_defss) fld_induct' pre_set_defss nested_set_natural's) - (* TODO: thread name context properly ### *) |> singleton (Proof_Context.export names_lthy lthy) - |> singleton (Proof_Context.export no_defs_lthy no_defs_lthy0) in `(conj_dests nn) induct_thm end; @@ -669,9 +669,15 @@ lthy |> Local_Theory.notes (common_notes @ notes) |> snd end; - fun derive_coinduct_coiter_corec_thms_for_types ((ctrss, selsss, coiters, corecs, vs, _, - ctr_defss, discIss, sel_thmsss, coiter_defs, corec_defs), lthy) = + fun derive_coinduct_coiter_corec_thms_for_types ((ctrss, selsss, coiters, corecs, _, ctr_defss, + discIss, sel_thmsss, coiter_defs, corec_defs), lthy) = let + val (vs', names_lthy) = + lthy + |> Variable.variant_fixes (map Binding.name_of fp_bs); + + val vs = map2 (curry Free) vs' fpTs; + val (coinduct_thms, coinduct_thm) = let val coinduct_thm = fp_induct; @@ -780,13 +786,12 @@ 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 + fold_map2 (curry (op o)) define_iter_likess wraps lthy |>> split_list10 val lthy' = lthy - |> 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) + |> 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) |>> 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); diff -r d9800bc28427 -r be6e749fd003 src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Fri Sep 14 12:09:27 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Fri Sep 14 12:09:27 2012 +0200 @@ -29,7 +29,7 @@ val meta_mp = @{thm meta_mp}; val meta_spec = @{thm meta_spec}; -fun squash_spurious_fs lthy thm = +fun smash_spurious_fs lthy thm = let val spurious_fs = Term.add_vars (prop_of thm) [] @@ -41,7 +41,7 @@ Drule.cterm_instantiate cxs thm end; -val squash_spurious_fs_tac = PRIMITIVE o squash_spurious_fs; +val smash_spurious_fs_tac = PRIMITIVE o smash_spurious_fs; fun mk_case_tac ctxt n k m case_def ctr_def unf_fld = Local_Defs.unfold_tac ctxt [case_def, ctr_def, unf_fld] THEN @@ -89,7 +89,7 @@ TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1); fun mk_induct_prelude_tac ctxt ctr_defs fld_induct' = - Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN squash_spurious_fs_tac ctxt; + Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN smash_spurious_fs_tac ctxt; fun mk_induct_prepare_prem_tac n m k = EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac,