# HG changeset patch # User blanchet # Date 1348235609 -7200 # Node ID acc9635a644a96d0bac27cd73437055932cc5303 # Parent 3cb59fdd69a8ae84e20759ecb08261757b134405 renamed "fld"/"unf" to "ctor"/"dtor" diff -r 3cb59fdd69a8 -r acc9635a644a src/HOL/Codatatype/Tools/bnf_fp.ML --- a/src/HOL/Codatatype/Tools/bnf_fp.ML Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp.ML Fri Sep 21 15:53:29 2012 +0200 @@ -22,24 +22,35 @@ val coitersN: string val corecN: string val corecsN: string + val ctorN: string + val ctor_dtorN: string + val ctor_dtor_coitersN: string + val ctor_dtor_corecsN: string + val ctor_exhaustN: string + val ctor_induct2N: string + val ctor_inductN: string + val ctor_injectN: string + val ctor_iterN: string + val ctor_iter_uniqueN: string + val ctor_itersN: string + val ctor_recN: string + val ctor_recsN: string val disc_coiter_iffN: string val disc_coitersN: string val disc_corec_iffN: string val disc_corecsN: string + val dtorN: string + val dtor_coinductN: string + val dtor_coiterN: string + val dtor_coiter_uniqueN: string + val dtor_coitersN: string + val dtor_corecN: string + val dtor_corecsN: string + val dtor_exhaustN: string + val dtor_ctorN: string + val dtor_injectN: string + val dtor_strong_coinductN: string val exhaustN: string - val fldN: string - val fld_exhaustN: string - val fld_induct2N: string - val fld_inductN: string - val fld_injectN: string - val fld_iterN: string - val fld_iter_uniqueN: string - val fld_itersN: string - val fld_recN: string - val fld_recsN: string - val fld_unfN: string - val fld_unf_coitersN: string - val fld_unf_corecsN: string val hsetN: string val hset_recN: string val inductN: string @@ -72,17 +83,6 @@ val strongN: string val sum_bdN: string val sum_bdTN: string - val unfN: string - val unf_coinductN: string - val unf_coiterN: string - val unf_coiter_uniqueN: string - val unf_coitersN: string - val unf_corecN: string - val unf_corecsN: string - val unf_exhaustN: string - val unf_fldN: string - val unf_injectN: string - val unf_strong_coinductN: string val uniqueN: string val mk_exhaustN: string -> string @@ -166,15 +166,15 @@ val coitersN = coiterN ^ "s" val uniqueN = "_unique" val simpsN = "simps" -val fldN = "fld" -val unfN = "unf" -val fld_iterN = fldN ^ "_" ^ iterN -val fld_itersN = fld_iterN ^ "s" -val unf_coiterN = unfN ^ "_" ^ coiterN -val unf_coitersN = unf_coiterN ^ "s" -val fld_iter_uniqueN = fld_iterN ^ uniqueN -val unf_coiter_uniqueN = unf_coiterN ^ uniqueN -val fld_unf_coitersN = fldN ^ "_" ^ unf_coiterN ^ "s" +val ctorN = "ctor" +val dtorN = "dtor" +val ctor_iterN = ctorN ^ "_" ^ iterN +val ctor_itersN = ctor_iterN ^ "s" +val dtor_coiterN = dtorN ^ "_" ^ coiterN +val dtor_coitersN = dtor_coiterN ^ "s" +val ctor_iter_uniqueN = ctor_iterN ^ uniqueN +val dtor_coiter_uniqueN = dtor_coiterN ^ uniqueN +val ctor_dtor_coitersN = ctorN ^ "_" ^ dtor_coiterN ^ "s" val map_simpsN = mapN ^ "_" ^ simpsN val map_uniqueN = mapN ^ uniqueN val min_algN = "min_alg" @@ -198,36 +198,36 @@ val recsN = recN ^ "s" val corecN = coN ^ recN val corecsN = corecN ^ "s" -val fld_recN = fldN ^ "_" ^ recN -val fld_recsN = fld_recN ^ "s" -val unf_corecN = unfN ^ "_" ^ corecN -val unf_corecsN = unf_corecN ^ "s" -val fld_unf_corecsN = fldN ^ "_" ^ unf_corecN ^ "s" +val ctor_recN = ctorN ^ "_" ^ recN +val ctor_recsN = ctor_recN ^ "s" +val dtor_corecN = dtorN ^ "_" ^ corecN +val dtor_corecsN = dtor_corecN ^ "s" +val ctor_dtor_corecsN = ctorN ^ "_" ^ dtor_corecN ^ "s" -val fld_unfN = fldN ^ "_" ^ unfN -val unf_fldN = unfN ^ "_" ^ fldN +val ctor_dtorN = ctorN ^ "_" ^ dtorN +val dtor_ctorN = dtorN ^ "_" ^ ctorN val nchotomyN = "nchotomy" fun mk_nchotomyN s = s ^ "_" ^ nchotomyN val injectN = "inject" fun mk_injectN s = s ^ "_" ^ injectN val exhaustN = "exhaust" fun mk_exhaustN s = s ^ "_" ^ exhaustN -val fld_injectN = mk_injectN fldN -val fld_exhaustN = mk_exhaustN fldN -val unf_injectN = mk_injectN unfN -val unf_exhaustN = mk_exhaustN unfN +val ctor_injectN = mk_injectN ctorN +val ctor_exhaustN = mk_exhaustN ctorN +val dtor_injectN = mk_injectN dtorN +val dtor_exhaustN = mk_exhaustN dtorN val inductN = "induct" val coinductN = coN ^ inductN -val fld_inductN = fldN ^ "_" ^ inductN -val fld_induct2N = fld_inductN ^ "2" -val unf_coinductN = unfN ^ "_" ^ coinductN +val ctor_inductN = ctorN ^ "_" ^ inductN +val ctor_induct2N = ctor_inductN ^ "2" +val dtor_coinductN = dtorN ^ "_" ^ coinductN val rel_coinductN = relN ^ "_" ^ coinductN val pred_coinductN = predN ^ "_" ^ coinductN val simpN = "_simp"; val rel_simpN = relN ^ simpN; val pred_simpN = predN ^ simpN; val strongN = "strong_" -val unf_strong_coinductN = unfN ^ "_" ^ strongN ^ coinductN +val dtor_strong_coinductN = dtorN ^ "_" ^ strongN ^ coinductN val rel_strong_coinductN = relN ^ "_" ^ strongN ^ coinductN val pred_strong_coinductN = predN ^ "_" ^ strongN ^ coinductN val hsetN = "Hset" diff -r 3cb59fdd69a8 -r acc9635a644a src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 21 15:53:29 2012 +0200 @@ -169,8 +169,8 @@ val fp_eqs = map dest_TFree Bs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctr_sum_prod_TsBs; - val (pre_bnfs, ((unfs0, flds0, fp_iters0, fp_recs0, fp_induct, unf_flds, fld_unfs, fld_injects, - fp_iter_thms, fp_rec_thms), lthy)) = + val (pre_bnfs, ((dtors0, ctors0, fp_iters0, fp_recs0, fp_induct, dtor_ctors, ctor_dtors, + ctor_injects, fp_iter_thms, fp_rec_thms), lthy)) = fp_bnf construct fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0; fun add_nesty_bnf_names Us = @@ -190,18 +190,18 @@ val timer = time (Timer.startRealTimer ()); - fun mk_unf_or_fld get_T Ts t = + fun mk_ctor_or_dtor get_T Ts t = let val Type (_, Ts0) = get_T (fastype_of t) in Term.subst_atomic_types (Ts0 ~~ Ts) t end; - val mk_unf = mk_unf_or_fld domain_type; - val mk_fld = mk_unf_or_fld range_type; + val mk_ctor = mk_ctor_or_dtor range_type; + val mk_dtor = mk_ctor_or_dtor domain_type; - val unfs = map (mk_unf As) unfs0; - val flds = map (mk_fld As) flds0; + val ctors = map (mk_ctor As) ctors0; + val dtors = map (mk_dtor As) dtors0; - val fpTs = map (domain_type o fastype_of) unfs; + val fpTs = map (domain_type o fastype_of) dtors; val exists_fp_subtype = exists_subtype (member (op =) fpTs); @@ -329,20 +329,20 @@ (mk_terms sssss hssss, (h_sum_prod_Ts, ph_Tss)))), lthy) 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), + fun define_ctrs_case_for_type ((((((((((((((((((fp_b, fpT), C), ctor), dtor), fp_iter), fp_rec), + ctor_dtor), dtor_ctor), ctor_inject), n), ks), ms), ctr_bindings), ctr_mixfixes), ctr_Tss), disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy = let val fp_b_name = Binding.name_of fp_b; - val unfT = domain_type (fastype_of fld); + val dtorT = domain_type (fastype_of ctor); 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 ((((w, fs), xss), u'), _) = no_defs_lthy - |> yield_singleton (mk_Frees "w") unfT + |> yield_singleton (mk_Frees "w") dtorT ||>> mk_Frees "f" case_Ts ||>> mk_Freess "x" ctr_Tss ||>> yield_singleton Variable.variant_fixes fp_b_name; @@ -350,14 +350,14 @@ val u = Free (u', fpT); val ctr_rhss = - map2 (fn k => fn xs => fold_rev Term.lambda xs (fld $ + map2 (fn k => fn xs => fold_rev Term.lambda xs (ctor $ mk_InN_balanced ctr_sum_prod_T n (HOLogic.mk_tuple xs) k)) ks xss; val case_binding = Binding.suffix_name ("_" ^ caseN) fp_b; val case_rhs = fold_rev Term.lambda (fs @ [u]) - (mk_sum_caseN_balanced (map2 mk_uncurried_fun fs xss) $ (unf $ u)); + (mk_sum_caseN_balanced (map2 mk_uncurried_fun fs xss) $ (dtor $ u)); val ((raw_case :: raw_ctrs, raw_case_def :: raw_ctr_defs), (lthy', lthy)) = no_defs_lthy |> apfst split_list o fold_map3 (fn b => fn mx => fn rhs => @@ -377,15 +377,15 @@ fun exhaust_tac {context = ctxt, ...} = let - val fld_iff_unf_thm = + val ctor_iff_dtor_thm = let val goal = fold_rev Logic.all [w, u] - (mk_Trueprop_eq (HOLogic.mk_eq (u, fld $ w), HOLogic.mk_eq (unf $ u, w))); + (mk_Trueprop_eq (HOLogic.mk_eq (u, ctor $ w), HOLogic.mk_eq (dtor $ u, w))); in Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => - mk_fld_iff_unf_tac ctxt (map (SOME o certifyT lthy) [unfT, fpT]) - (certify lthy fld) (certify lthy unf) fld_unf unf_fld) + mk_ctor_iff_dtor_tac ctxt (map (SOME o certifyT lthy) [dtorT, fpT]) + (certify lthy ctor) (certify lthy dtor) ctor_dtor dtor_ctor) |> Thm.close_derivation |> Morphism.thm phi end; @@ -396,20 +396,20 @@ (mk_sumEN_balanced n)) |> Morphism.thm phi; in - mk_exhaust_tac ctxt n ctr_defs fld_iff_unf_thm sumEN_thm' + mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor_thm sumEN_thm' end; val inject_tacss = map2 (fn 0 => K [] | _ => fn ctr_def => [fn {context = ctxt, ...} => - mk_inject_tac ctxt ctr_def fld_inject]) ms ctr_defs; + mk_inject_tac ctxt ctr_def ctor_inject]) ms ctr_defs; val half_distinct_tacss = map (map (fn (def, def') => fn {context = ctxt, ...} => - mk_half_distinct_tac ctxt fld_inject [def, def'])) (mk_half_pairss ctr_defs); + mk_half_distinct_tac ctxt ctor_inject [def, def'])) (mk_half_pairss ctr_defs); val case_tacs = map3 (fn k => fn m => fn ctr_def => fn {context = ctxt, ...} => - mk_case_tac ctxt n k m case_def ctr_def unf_fld) ks ms ctr_defs; + mk_case_tac ctxt n k m case_def ctr_def dtor_ctor) ks ms ctr_defs; val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss @ [case_tacs]; @@ -601,11 +601,11 @@ val kksss = map (map (map (fst o snd) o #2)) raw_premss; - val fld_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss); + val ctor_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss); val induct_thm = Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => - mk_induct_tac ctxt ns mss kksss (flat ctr_defss) fld_induct' + mk_induct_tac ctxt ns mss kksss (flat ctr_defss) ctor_induct' nested_set_natural's pre_set_defss) |> singleton (Proof_Context.export names_lthy lthy) in @@ -875,8 +875,8 @@ fold_map2 (curry (op o)) define_iter_likess wraps lthy |>> split_list8 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 ~~ + |> fold_map define_ctrs_case_for_type (fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~ fp_iters ~~ + fp_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_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 diff -r 3cb59fdd69a8 -r acc9635a644a src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Fri Sep 21 15:53:29 2012 +0200 @@ -9,10 +9,10 @@ sig val mk_case_tac: Proof.context -> int -> int -> int -> thm -> thm -> thm -> tactic val mk_coiter_like_tac: thm list -> thm list -> thm -> thm -> thm -> Proof.context -> tactic + val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm -> + tactic val mk_disc_coiter_like_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic - val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm -> - tactic val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic val mk_induct_tac: Proof.context -> int list -> int list list -> int list list list -> thm list -> thm -> thm list -> thm list list -> tactic @@ -43,47 +43,47 @@ val inst_spurious_fs_tac = PRIMITIVE o inst_spurious_fs; -fun mk_case_tac ctxt n k m case_def ctr_def unf_fld = - unfold_defs_tac ctxt [case_def, ctr_def, unf_fld] THEN +fun mk_case_tac ctxt n k m case_def ctr_def dtor_ctor = + unfold_defs_tac ctxt [case_def, ctr_def, dtor_ctor] THEN (rtac (mk_sum_casesN_balanced n k RS ssubst) THEN' REPEAT_DETERM_N (Int.max (0, m - 1)) o rtac (@{thm split} RS ssubst) THEN' rtac refl) 1; -fun mk_exhaust_tac ctxt n ctr_defs fld_iff_unf sumEN' = - unfold_defs_tac ctxt (fld_iff_unf :: ctr_defs) THEN rtac sumEN' 1 THEN +fun mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor sumEN' = + unfold_defs_tac ctxt (ctor_iff_dtor :: ctr_defs) THEN rtac sumEN' 1 THEN unfold_defs_tac ctxt @{thms all_prod_eq} THEN EVERY' (maps (fn k => [select_prem_tac n (rotate_tac 1) k, REPEAT_DETERM o dtac meta_spec, etac meta_mp, atac]) (1 upto n)) 1; -fun mk_fld_iff_unf_tac ctxt cTs cfld cunf fld_unf unf_fld = +fun mk_ctor_iff_dtor_tac ctxt cTs cctor cdtor ctor_dtor dtor_ctor = (rtac iffI THEN' EVERY' (map3 (fn cTs => fn cx => fn th => dtac (Drule.instantiate' cTs [NONE, NONE, SOME cx] arg_cong) THEN' SELECT_GOAL (unfold_defs_tac ctxt [th]) THEN' - atac) [rev cTs, cTs] [cunf, cfld] [unf_fld, fld_unf])) 1; + atac) [rev cTs, cTs] [cdtor, cctor] [dtor_ctor, ctor_dtor])) 1; -fun mk_half_distinct_tac ctxt fld_inject ctr_defs = - unfold_defs_tac ctxt (fld_inject :: @{thms sum.inject} @ ctr_defs) THEN +fun mk_half_distinct_tac ctxt ctor_inject ctr_defs = + unfold_defs_tac ctxt (ctor_inject :: @{thms sum.inject} @ ctr_defs) THEN rtac @{thm sum.distinct(1)} 1; -fun mk_inject_tac ctxt ctr_def fld_inject = - unfold_defs_tac ctxt [ctr_def] THEN rtac (fld_inject RS ssubst) 1 THEN +fun mk_inject_tac ctxt ctr_def ctor_inject = + unfold_defs_tac ctxt [ctr_def] THEN rtac (ctor_inject RS ssubst) 1 THEN unfold_defs_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1; val iter_like_unfold_thms = @{thms case_unit comp_def convol_def id_apply map_pair_def sum.simps(5,6) sum_map.simps split_conv}; -fun mk_iter_like_tac pre_map_defs map_ids iter_like_defs fld_iter_like ctr_def ctxt = - unfold_defs_tac ctxt (ctr_def :: fld_iter_like :: iter_like_defs @ pre_map_defs @ map_ids @ +fun mk_iter_like_tac pre_map_defs map_ids iter_like_defs ctor_iter_like ctr_def ctxt = + unfold_defs_tac ctxt (ctr_def :: ctor_iter_like :: iter_like_defs @ pre_map_defs @ map_ids @ iter_like_unfold_thms) THEN unfold_defs_tac ctxt @{thms id_def} THEN rtac refl 1; val coiter_like_ss = ss_only @{thms if_True if_False}; val coiter_like_unfold_thms = @{thms id_apply map_pair_def sum_map.simps prod.cases}; -fun mk_coiter_like_tac coiter_like_defs map_ids fld_unf_coiter_like pre_map_def ctr_def ctxt = +fun mk_coiter_like_tac coiter_like_defs map_ids ctor_dtor_coiter_like pre_map_def ctr_def ctxt = unfold_defs_tac ctxt (ctr_def :: coiter_like_defs) THEN - subst_tac ctxt [fld_unf_coiter_like] 1 THEN asm_simp_tac coiter_like_ss 1 THEN + subst_tac ctxt [ctor_dtor_coiter_like] 1 THEN asm_simp_tac coiter_like_ss 1 THEN unfold_defs_tac ctxt (pre_map_def :: coiter_like_unfold_thms @ map_ids) THEN unfold_defs_tac ctxt @{thms id_def} THEN TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1); @@ -120,12 +120,12 @@ mk_induct_leverage_prem_prems_tac ctxt nn kks set_natural's pre_set_defs] end; -fun mk_induct_tac ctxt ns mss kkss ctr_defs fld_induct' set_natural's pre_set_defss = +fun mk_induct_tac ctxt ns mss kkss ctr_defs ctor_induct' set_natural's pre_set_defss = let val nn = length ns; val n = Integer.sum ns; in - unfold_defs_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN inst_spurious_fs_tac ctxt THEN + unfold_defs_tac ctxt ctr_defs THEN rtac ctor_induct' 1 THEN inst_spurious_fs_tac ctxt THEN EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's) pre_set_defss mss (unflat mss (1 upto n)) kkss) end; diff -r 3cb59fdd69a8 -r acc9635a644a src/HOL/Codatatype/Tools/bnf_gfp.ML --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Fri Sep 21 15:53:29 2012 +0200 @@ -45,10 +45,10 @@ |> minimize_wits end; -fun tree_to_fld_wit vars _ _ (Wit_Leaf j) = ([j], nth vars j) - | tree_to_fld_wit vars flds witss (Wit_Node ((i, nwit, I), subtrees)) = - (I, nth flds i $ (Term.list_comb (snd (nth (nth witss i) nwit), - map (snd o tree_to_fld_wit vars flds witss) subtrees))); +fun tree_to_ctor_wit vars _ _ (Wit_Leaf j) = ([j], nth vars j) + | tree_to_ctor_wit vars ctors witss (Wit_Node ((i, nwit, I), subtrees)) = + (I, nth ctors i $ (Term.list_comb (snd (nth (nth witss i) nwit), + map (snd o tree_to_ctor_wit vars ctors witss) subtrees))); fun tree_to_coind_wits _ (Wit_Leaf _) = [] | tree_to_coind_wits lwitss (Wit_Node ((i, nwit, I), subtrees)) = @@ -1852,8 +1852,8 @@ mk_map_of_bnf Ds (passiveAs @ prodTs) (passiveAs @ Ts)) Dss bnfs; val fstsTs = map fst_const prodTs; val sndsTs = map snd_const prodTs; - val unfTs = map2 (curry (op -->)) Ts FTs; - val fldTs = map2 (curry (op -->)) FTs Ts; + val dtorTs = map2 (curry (op -->)) Ts FTs; + val ctorTs = map2 (curry (op -->)) FTs Ts; val coiter_fTs = map2 (curry op -->) activeAs Ts; val corec_sTs = map (Term.typ_subst_atomic (activeBs ~~ Ts)) sum_sTs; val corec_maps = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_Inls; @@ -1875,13 +1875,13 @@ ||>> mk_Frees "s" corec_sTs ||>> mk_Frees "P" (map2 mk_pred2T Ts Ts); - fun unf_bind i = Binding.suffix_name ("_" ^ unfN) (nth bs (i - 1)); - val unf_name = Binding.name_of o unf_bind; - val unf_def_bind = rpair [] o Thm.def_binding o unf_bind; - - fun unf_spec i rep str map_FT unfT Jz Jz' = + fun dtor_bind i = Binding.suffix_name ("_" ^ dtorN) (nth bs (i - 1)); + val dtor_name = Binding.name_of o dtor_bind; + val dtor_def_bind = rpair [] o Thm.def_binding o dtor_bind; + + fun dtor_spec i rep str map_FT dtorT Jz Jz' = let - val lhs = Free (unf_name i, unfT); + val lhs = Free (dtor_name i, dtorT); val rhs = Term.absfree Jz' (Term.list_comb (map_FT, map HOLogic.id_const passiveAs @ Abs_Ts) $ (str $ (rep $ Jz))); @@ -1889,45 +1889,45 @@ mk_Trueprop_eq (lhs, rhs) end; - val ((unf_frees, (_, unf_def_frees)), (lthy, lthy_old)) = + val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) = lthy - |> fold_map7 (fn i => fn rep => fn str => fn mapx => fn unfT => fn Jz => fn Jz' => - Specification.definition - (SOME (unf_bind i, NONE, NoSyn), (unf_def_bind i, unf_spec i rep str mapx unfT Jz Jz'))) - ks Rep_Ts str_finals map_FTs unfTs Jzs Jzs' + |> fold_map7 (fn i => fn rep => fn str => fn mapx => fn dtorT => fn Jz => fn Jz' => + Specification.definition (SOME (dtor_bind i, NONE, NoSyn), + (dtor_def_bind i, dtor_spec i rep str mapx dtorT Jz Jz'))) + ks Rep_Ts str_finals map_FTs dtorTs Jzs Jzs' |>> apsnd split_list o split_list ||> `Local_Theory.restore; val phi = Proof_Context.export_morphism lthy_old lthy; - fun mk_unfs passive = + fun mk_dtors passive = map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (mk_params passive)) o - Morphism.term phi) unf_frees; - val unfs = mk_unfs passiveAs; - val unf's = mk_unfs passiveBs; - val unf_defs = map ((fn thm => thm RS fun_cong) o Morphism.thm phi) unf_def_frees; + Morphism.term phi) dtor_frees; + val dtors = mk_dtors passiveAs; + val dtor's = mk_dtors passiveBs; + val dtor_defs = map ((fn thm => thm RS fun_cong) o Morphism.thm phi) dtor_def_frees; val coalg_final_set_thmss = map (map (fn thm => coalg_final_thm RS thm)) coalg_set_thmss; val (mor_Rep_thm, mor_Abs_thm) = let val mor_Rep = Skip_Proof.prove lthy [] [] - (HOLogic.mk_Trueprop (mk_mor UNIVs unfs car_finals str_finals Rep_Ts)) - (mk_mor_Rep_tac m (mor_def :: unf_defs) Reps Abs_inverses coalg_final_set_thmss + (HOLogic.mk_Trueprop (mk_mor UNIVs dtors car_finals str_finals Rep_Ts)) + (mk_mor_Rep_tac m (mor_def :: dtor_defs) Reps Abs_inverses coalg_final_set_thmss map_comp_id_thms map_congL_thms) |> Thm.close_derivation; val mor_Abs = Skip_Proof.prove lthy [] [] - (HOLogic.mk_Trueprop (mk_mor car_finals str_finals UNIVs unfs Abs_Ts)) - (mk_mor_Abs_tac (mor_def :: unf_defs) Abs_inverses) + (HOLogic.mk_Trueprop (mk_mor car_finals str_finals UNIVs dtors Abs_Ts)) + (mk_mor_Abs_tac (mor_def :: dtor_defs) Abs_inverses) |> Thm.close_derivation; in (mor_Rep, mor_Abs) end; - val timer = time (timer "unf definitions & thms"); - - fun coiter_bind i = Binding.suffix_name ("_" ^ unf_coiterN) (nth bs (i - 1)); + val timer = time (timer "dtor definitions & thms"); + + fun coiter_bind i = Binding.suffix_name ("_" ^ dtor_coiterN) (nth bs (i - 1)); val coiter_name = Binding.name_of o coiter_bind; val coiter_def_bind = rpair [] o Thm.def_binding o coiter_bind; @@ -1966,8 +1966,8 @@ in Skip_Proof.prove lthy [] [] (fold_rev Logic.all ss - (HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs unfs (map (mk_coiter Ts ss) ks)))) - (K (mk_mor_coiter_tac m mor_UNIV_thm unf_defs coiter_defs Abs_inverses' morEs' + (HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors (map (mk_coiter Ts ss) ks)))) + (K (mk_mor_coiter_tac m mor_UNIV_thm dtor_defs coiter_defs Abs_inverses' morEs' map_comp_id_thms map_congs)) |> Thm.close_derivation end; @@ -1975,7 +1975,7 @@ val (raw_coind_thms, raw_coind_thm) = let - val prem = HOLogic.mk_Trueprop (mk_sbis passive_UNIVs UNIVs unfs TRs); + val prem = HOLogic.mk_Trueprop (mk_sbis passive_UNIVs UNIVs dtors TRs); val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (fn R => fn T => mk_subset R (Id_const T)) TRs Ts)); val goal = fold_rev Logic.all TRs (Logic.mk_implies (prem, concl)); @@ -1990,8 +1990,8 @@ val unique_mor_thms = let val prems = [HOLogic.mk_Trueprop (mk_coalg passive_UNIVs Bs ss), HOLogic.mk_Trueprop - (HOLogic.mk_conj (mk_mor Bs ss UNIVs unfs coiter_fs, - mk_mor Bs ss UNIVs unfs coiter_fs_copy))]; + (HOLogic.mk_conj (mk_mor Bs ss UNIVs dtors coiter_fs, + mk_mor Bs ss UNIVs dtors coiter_fs_copy))]; fun mk_fun_eq B f g z = HOLogic.mk_imp (HOLogic.mk_mem (z, B), HOLogic.mk_eq (f $ z, g $ z)); val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj @@ -2008,7 +2008,7 @@ val (coiter_unique_mor_thms, coiter_unique_mor_thm) = let - val prem = HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs unfs coiter_fs); + val prem = HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors coiter_fs); fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_coiter Ts ss i); val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_fun_eq coiter_fs ks)); @@ -2027,107 +2027,109 @@ val (coiter_unique_thms, coiter_unique_thm) = `split_conj_thm (split_conj_prems n (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS coiter_unique_mor_thm)); - val coiter_unf_thms = map (fn thm => mor_id_thm RS thm RS sym) coiter_unique_mor_thms; - - val coiter_o_unf_thms = + val coiter_dtor_thms = map (fn thm => mor_id_thm RS thm RS sym) coiter_unique_mor_thms; + + val coiter_o_dtor_thms = let val mor = mor_comp_thm OF [mor_str_thm, mor_coiter_thm]; in - map2 (fn unique => fn coiter_fld => - trans OF [mor RS unique, coiter_fld]) coiter_unique_mor_thms coiter_unf_thms + map2 (fn unique => fn coiter_ctor => + trans OF [mor RS unique, coiter_ctor]) coiter_unique_mor_thms coiter_dtor_thms end; val timer = time (timer "coiter definitions & thms"); - val map_unfs = map2 (fn Ds => fn bnf => + val map_dtors = map2 (fn Ds => fn bnf => Term.list_comb (mk_map_of_bnf Ds (passiveAs @ Ts) (passiveAs @ FTs) bnf, - map HOLogic.id_const passiveAs @ unfs)) Dss bnfs; - - fun fld_bind i = Binding.suffix_name ("_" ^ fldN) (nth bs (i - 1)); - val fld_name = Binding.name_of o fld_bind; - val fld_def_bind = rpair [] o Thm.def_binding o fld_bind; - - fun fld_spec i fldT = + map HOLogic.id_const passiveAs @ dtors)) Dss bnfs; + + fun ctor_bind i = Binding.suffix_name ("_" ^ ctorN) (nth bs (i - 1)); + val ctor_name = Binding.name_of o ctor_bind; + val ctor_def_bind = rpair [] o Thm.def_binding o ctor_bind; + + fun ctor_spec i ctorT = let - val lhs = Free (fld_name i, fldT); - val rhs = mk_coiter Ts map_unfs i; + val lhs = Free (ctor_name i, ctorT); + val rhs = mk_coiter Ts map_dtors i; in mk_Trueprop_eq (lhs, rhs) end; - val ((fld_frees, (_, fld_def_frees)), (lthy, lthy_old)) = + val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) = lthy - |> fold_map2 (fn i => fn fldT => + |> fold_map2 (fn i => fn ctorT => Specification.definition - (SOME (fld_bind i, NONE, NoSyn), (fld_def_bind i, fld_spec i fldT))) ks fldTs + (SOME (ctor_bind i, NONE, NoSyn), (ctor_def_bind i, ctor_spec i ctorT))) ks ctorTs |>> apsnd split_list o split_list ||> `Local_Theory.restore; val phi = Proof_Context.export_morphism lthy_old lthy; - fun mk_flds params = + fun mk_ctors params = map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ params) o Morphism.term phi) - fld_frees; - val flds = mk_flds params'; - val fld_defs = map (Morphism.thm phi) fld_def_frees; - - val fld_o_unf_thms = map2 (fold_defs lthy o single) fld_defs coiter_o_unf_thms; - - val unf_o_fld_thms = + ctor_frees; + val ctors = mk_ctors params'; + val ctor_defs = map (Morphism.thm phi) ctor_def_frees; + + val ctor_o_dtor_thms = map2 (fold_defs lthy o single) ctor_defs coiter_o_dtor_thms; + + val dtor_o_ctor_thms = let - fun mk_goal unf fld FT = mk_Trueprop_eq (HOLogic.mk_comp (unf, fld), HOLogic.id_const FT); - val goals = map3 mk_goal unfs flds FTs; + fun mk_goal dtor ctor FT = + mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT); + val goals = map3 mk_goal dtors ctors FTs; in - map5 (fn goal => fn fld_def => fn coiter => fn map_comp_id => fn map_congL => + map5 (fn goal => fn ctor_def => fn coiter => fn map_comp_id => fn map_congL => Skip_Proof.prove lthy [] [] goal - (mk_unf_o_fld_tac fld_def coiter map_comp_id map_congL coiter_o_unf_thms) + (mk_dtor_o_ctor_tac ctor_def coiter map_comp_id map_congL coiter_o_dtor_thms) |> Thm.close_derivation) - goals fld_defs coiter_thms map_comp_id_thms map_congL_thms + goals ctor_defs coiter_thms map_comp_id_thms map_congL_thms end; - val unf_fld_thms = map (fn thm => thm RS @{thm pointfree_idE}) unf_o_fld_thms; - val fld_unf_thms = map (fn thm => thm RS @{thm pointfree_idE}) fld_o_unf_thms; - - val bij_unf_thms = - map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) fld_o_unf_thms unf_o_fld_thms; - val inj_unf_thms = map (fn thm => thm RS @{thm bij_is_inj}) bij_unf_thms; - val surj_unf_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_unf_thms; - val unf_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_unf_thms; - val unf_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_unf_thms; - val unf_exhaust_thms = map (fn thm => thm RS exE) unf_nchotomy_thms; - - val bij_fld_thms = - map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) unf_o_fld_thms fld_o_unf_thms; - val inj_fld_thms = map (fn thm => thm RS @{thm bij_is_inj}) bij_fld_thms; - val surj_fld_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_fld_thms; - val fld_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_fld_thms; - val fld_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_fld_thms; - val fld_exhaust_thms = map (fn thm => thm RS exE) fld_nchotomy_thms; - - fun mk_fld_unf_coiter_like_thm unf_inject unf_fld coiter = - iffD1 OF [unf_inject, trans OF [coiter, unf_fld RS sym]]; - - val fld_coiter_thms = map3 mk_fld_unf_coiter_like_thm unf_inject_thms unf_fld_thms coiter_thms; - - val timer = time (timer "fld definitions & thms"); + val dtor_ctor_thms = map (fn thm => thm RS @{thm pointfree_idE}) dtor_o_ctor_thms; + val ctor_dtor_thms = map (fn thm => thm RS @{thm pointfree_idE}) ctor_o_dtor_thms; + + val bij_dtor_thms = + map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) ctor_o_dtor_thms dtor_o_ctor_thms; + val inj_dtor_thms = map (fn thm => thm RS @{thm bij_is_inj}) bij_dtor_thms; + val surj_dtor_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_dtor_thms; + val dtor_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_dtor_thms; + val dtor_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_dtor_thms; + val dtor_exhaust_thms = map (fn thm => thm RS exE) dtor_nchotomy_thms; + + val bij_ctor_thms = + map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) dtor_o_ctor_thms ctor_o_dtor_thms; + val inj_ctor_thms = map (fn thm => thm RS @{thm bij_is_inj}) bij_ctor_thms; + val surj_ctor_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_ctor_thms; + val ctor_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_ctor_thms; + val ctor_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_ctor_thms; + val ctor_exhaust_thms = map (fn thm => thm RS exE) ctor_nchotomy_thms; + + fun mk_ctor_dtor_coiter_like_thm dtor_inject dtor_ctor coiter = + iffD1 OF [dtor_inject, trans OF [coiter, dtor_ctor RS sym]]; + + val ctor_coiter_thms = + map3 mk_ctor_dtor_coiter_like_thm dtor_inject_thms dtor_ctor_thms coiter_thms; + + val timer = time (timer "ctor definitions & thms"); val corec_Inl_sum_thms = let val mor = mor_comp_thm OF [mor_sum_case_thm, mor_coiter_thm]; in - map2 (fn unique => fn coiter_unf => - trans OF [mor RS unique, coiter_unf]) coiter_unique_mor_thms coiter_unf_thms + map2 (fn unique => fn coiter_dtor => + trans OF [mor RS unique, coiter_dtor]) coiter_unique_mor_thms coiter_dtor_thms end; - fun corec_bind i = Binding.suffix_name ("_" ^ unf_corecN) (nth bs (i - 1)); + fun corec_bind i = Binding.suffix_name ("_" ^ dtor_corecN) (nth bs (i - 1)); val corec_name = Binding.name_of o corec_bind; val corec_def_bind = rpair [] o Thm.def_binding o corec_bind; fun corec_spec i T AT = let val corecT = Library.foldr (op -->) (corec_sTs, AT --> T); - val maps = map3 (fn unf => fn sum_s => fn mapx => mk_sum_case - (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ corec_Inls), unf), sum_s)) - unfs corec_ss corec_maps; + val maps = map3 (fn dtor => fn sum_s => fn mapx => mk_sum_case + (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ corec_Inls), dtor), sum_s)) + dtors corec_ss corec_maps; val lhs = Term.list_comb (Free (corec_name i, corecT), corec_ss); val rhs = HOLogic.mk_comp (mk_coiter Ts maps i, Inr_const T AT); @@ -2155,14 +2157,14 @@ map2 (fn T => fn i => mk_sum_case (HOLogic.id_const T, mk_corec corec_ss i)) Ts ks; val corec_thms = let - fun mk_goal i corec_s corec_map unf z = + fun mk_goal i corec_s corec_map dtor z = let - val lhs = unf $ (mk_corec corec_ss i $ z); + val lhs = dtor $ (mk_corec corec_ss i $ z); val rhs = Term.list_comb (corec_map, passive_ids @ sum_cases) $ (corec_s $ z); in fold_rev Logic.all (z :: corec_ss) (mk_Trueprop_eq (lhs, rhs)) end; - val goals = map5 mk_goal ks corec_ss corec_maps_rev unfs zs; + val goals = map5 mk_goal ks corec_ss corec_maps_rev dtors zs; in map3 (fn goal => fn coiter => fn map_cong => Skip_Proof.prove lthy [] [] goal @@ -2171,12 +2173,13 @@ goals coiter_thms map_congs end; - val fld_corec_thms = map3 mk_fld_unf_coiter_like_thm unf_inject_thms unf_fld_thms corec_thms; + val ctor_corec_thms = + map3 mk_ctor_dtor_coiter_like_thm dtor_inject_thms dtor_ctor_thms corec_thms; val timer = time (timer "corec definitions & thms"); - val (unf_coinduct_thm, coinduct_params, rel_coinduct_thm, pred_coinduct_thm, - unf_strong_coinduct_thm, rel_strong_coinduct_thm, pred_strong_coinduct_thm) = + val (dtor_coinduct_thm, coinduct_params, rel_coinduct_thm, pred_coinduct_thm, + dtor_strong_coinduct_thm, rel_strong_coinduct_thm, pred_strong_coinduct_thm) = let val zs = Jzs1 @ Jzs2; val frees = phis @ zs; @@ -2198,17 +2201,17 @@ val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map3 mk_concl phis Jzs1 Jzs2)); - fun mk_rel_prem upto_eq phi unf rel Jz Jz_copy = + fun mk_rel_prem upto_eq phi dtor rel Jz Jz_copy = let - val concl = HOLogic.mk_mem (HOLogic.mk_tuple [unf $ Jz, unf $ Jz_copy], + val concl = HOLogic.mk_mem (HOLogic.mk_tuple [dtor $ Jz, dtor $ Jz_copy], Term.list_comb (rel, mk_Ids upto_eq @ phi_rels upto_eq)); in HOLogic.mk_Trueprop (list_all_free [Jz, Jz_copy] (HOLogic.mk_imp (phi $ Jz $ Jz_copy, concl))) end; - val rel_prems = map5 (mk_rel_prem false) phis unfs rels Jzs Jzs_copy; - val rel_upto_prems = map5 (mk_rel_prem true) phis unfs rels Jzs Jzs_copy; + val rel_prems = map5 (mk_rel_prem false) phis dtors rels Jzs Jzs_copy; + val rel_upto_prems = map5 (mk_rel_prem true) phis dtors rels Jzs Jzs_copy; val rel_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (rel_prems, concl)); val coinduct_params = rev (Term.add_tfrees rel_coinduct_goal []); @@ -2218,12 +2221,12 @@ (K (mk_rel_coinduct_tac ks raw_coind_thm bis_rel_thm)) |> Thm.close_derivation); - fun mk_unf_prem upto_eq phi unf map_nth sets Jz Jz_copy FJz = + fun mk_dtor_prem upto_eq phi dtor map_nth sets Jz Jz_copy FJz = let val xs = [Jz, Jz_copy]; fun mk_map_conjunct nths x = - HOLogic.mk_eq (Term.list_comb (map_nth, passive_ids @ nths) $ FJz, unf $ x); + HOLogic.mk_eq (Term.list_comb (map_nth, passive_ids @ nths) $ FJz, dtor $ x); fun mk_set_conjunct set phi z1 z2 = list_all_free [z1, z2] @@ -2239,15 +2242,15 @@ (HOLogic.mk_Trueprop (Term.list_comb (phi, xs)), HOLogic.mk_Trueprop concl)) end; - fun mk_unf_prems upto_eq = - map7 (mk_unf_prem upto_eq) phis unfs map_FT_nths prodFT_setss Jzs Jzs_copy FJzs - - val unf_prems = mk_unf_prems false; - val unf_upto_prems = mk_unf_prems true; - - val unf_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (unf_prems, concl)); - val unf_coinduct = Skip_Proof.prove lthy [] [] unf_coinduct_goal - (K (mk_unf_coinduct_tac m ks raw_coind_thm bis_def)) + fun mk_dtor_prems upto_eq = + map7 (mk_dtor_prem upto_eq) phis dtors map_FT_nths prodFT_setss Jzs Jzs_copy FJzs; + + val dtor_prems = mk_dtor_prems false; + val dtor_upto_prems = mk_dtor_prems true; + + val dtor_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (dtor_prems, concl)); + val dtor_coinduct = Skip_Proof.prove lthy [] [] dtor_coinduct_goal + (K (mk_dtor_coinduct_tac m ks raw_coind_thm bis_def)) |> Thm.close_derivation; val cTs = map (SOME o certifyT lthy o TFree) coinduct_params; @@ -2259,10 +2262,10 @@ (K (mk_rel_strong_coinduct_tac m cTs cts rel_coinduct rel_monos rel_Ids))) |> Thm.close_derivation; - val unf_strong_coinduct = singleton (Proof_Context.export names_lthy lthy) + val dtor_strong_coinduct = singleton (Proof_Context.export names_lthy lthy) (Skip_Proof.prove lthy [] [] - (fold_rev Logic.all zs (Logic.list_implies (unf_upto_prems, concl))) - (K (mk_unf_strong_coinduct_tac ks cTs cts unf_coinduct bis_def + (fold_rev Logic.all zs (Logic.list_implies (dtor_upto_prems, concl))) + (K (mk_dtor_strong_coinduct_tac ks cTs cts dtor_coinduct bis_def (tcoalg_thm RS bis_diag_thm)))) |> Thm.close_derivation; @@ -2272,8 +2275,8 @@ val pred_coinduct = unfold_defs lthy pred_of_rel_thms rel_coinduct; val pred_strong_coinduct = unfold_defs lthy pred_of_rel_thms rel_strong_coinduct; in - (unf_coinduct, rev (Term.add_tfrees unf_coinduct_goal []), rel_coinduct, pred_coinduct, - unf_strong_coinduct, rel_strong_coinduct, pred_strong_coinduct) + (dtor_coinduct, rev (Term.add_tfrees dtor_coinduct_goal []), rel_coinduct, pred_coinduct, + dtor_strong_coinduct, rel_strong_coinduct, pred_strong_coinduct) end; val timer = time (timer "coinduction"); @@ -2328,9 +2331,9 @@ fun mk_maps ATs BTs Ts mk_T = map2 (fn Ds => mk_map_of_bnf Ds (ATs @ Ts) (BTs @ map mk_T Ts)) Dss bnfs; fun mk_Fmap mk_const fs Ts Fmap = Term.list_comb (Fmap, fs @ map mk_const Ts); - fun mk_map mk_const mk_T Ts fs Ts' unfs mk_maps = - mk_coiter Ts' (map2 (fn unf => fn Fmap => - HOLogic.mk_comp (mk_Fmap mk_const fs Ts Fmap, unf)) unfs (mk_maps Ts mk_T)); + fun mk_map mk_const mk_T Ts fs Ts' dtors mk_maps = + mk_coiter Ts' (map2 (fn dtor => fn Fmap => + HOLogic.mk_comp (mk_Fmap mk_const fs Ts Fmap, dtor)) dtors (mk_maps Ts mk_T)); val mk_map_id = mk_map HOLogic.id_const I; val mk_mapsAB = mk_maps passiveAs passiveBs; val mk_mapsBC = mk_maps passiveBs passiveCs; @@ -2340,21 +2343,21 @@ val mk_mapsXA = mk_maps passiveXs passiveAs; val mk_mapsXB = mk_maps passiveXs passiveBs; val mk_mapsXC = mk_maps passiveXs passiveCs; - val fs_maps = map (mk_map_id Ts fs Ts' unfs mk_mapsAB) ks; - val fs_copy_maps = map (mk_map_id Ts fs_copy Ts' unfs mk_mapsAB) ks; - val gs_maps = map (mk_map_id Ts' gs Ts'' unf's mk_mapsBC) ks; + val fs_maps = map (mk_map_id Ts fs Ts' dtors mk_mapsAB) ks; + val fs_copy_maps = map (mk_map_id Ts fs_copy Ts' dtors mk_mapsAB) ks; + val gs_maps = map (mk_map_id Ts' gs Ts'' dtor's mk_mapsBC) ks; val fgs_maps = - map (mk_map_id Ts (map2 (curry HOLogic.mk_comp) gs fs) Ts'' unfs mk_mapsAC) ks; - val Xunfs = mk_unfs passiveXs; + map (mk_map_id Ts (map2 (curry HOLogic.mk_comp) gs fs) Ts'' dtors mk_mapsAC) ks; + val Xdtors = mk_dtors passiveXs; val UNIV's = map HOLogic.mk_UNIV Ts'; val CUNIVs = map HOLogic.mk_UNIV passiveCs; val UNIV''s = map HOLogic.mk_UNIV Ts''; val fstsTsTs' = map fst_const prodTs; val sndsTsTs' = map snd_const prodTs; - val unf''s = mk_unfs passiveCs; - val f1s_maps = map (mk_map_id Ts f1s YTs unfs mk_mapsAY) ks; - val f2s_maps = map (mk_map_id Ts' f2s YTs unf's mk_mapsBY) ks; - val pid_maps = map (mk_map_id XTs ps Ts'' Xunfs mk_mapsXC) ks; + val dtor''s = mk_dtors passiveCs; + val f1s_maps = map (mk_map_id Ts f1s YTs dtors mk_mapsAY) ks; + val f2s_maps = map (mk_map_id Ts' f2s YTs dtor's mk_mapsBY) ks; + val pid_maps = map (mk_map_id XTs ps Ts'' Xdtors mk_mapsXC) ks; val pfst_Fmaps = map (mk_Fmap fst_const p1s prodTs) (mk_mapsXA prodTs (fst o HOLogic.dest_prodT)); val psnd_Fmaps = @@ -2365,10 +2368,10 @@ val (map_simp_thms, map_thms) = let - fun mk_goal fs_map map unf unf' = fold_rev Logic.all fs - (mk_Trueprop_eq (HOLogic.mk_comp (unf', fs_map), - HOLogic.mk_comp (Term.list_comb (map, fs @ fs_maps), unf))); - val goals = map4 mk_goal fs_maps map_FTFT's unfs unf's; + fun mk_goal fs_map map dtor dtor' = fold_rev Logic.all fs + (mk_Trueprop_eq (HOLogic.mk_comp (dtor', fs_map), + HOLogic.mk_comp (Term.list_comb (map, fs @ fs_maps), dtor))); + val goals = map4 mk_goal fs_maps map_FTFT's dtors dtor's; val cTs = map (SOME o certifyT lthy) FTs'; val maps = map5 (fn goal => fn cT => fn coiter => fn map_comp' => fn map_cong => @@ -2395,10 +2398,10 @@ val map_unique_thm = let - fun mk_prem u map unf unf' = - mk_Trueprop_eq (HOLogic.mk_comp (unf', u), - HOLogic.mk_comp (Term.list_comb (map, fs @ us), unf)); - val prems = map4 mk_prem us map_FTFT's unfs unf's; + fun mk_prem u map dtor dtor' = + mk_Trueprop_eq (HOLogic.mk_comp (dtor', u), + HOLogic.mk_comp (Term.list_comb (map, fs @ us), dtor)); + val prems = map4 mk_prem us map_FTFT's dtors dtor's; val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) us fs_maps)); @@ -2415,21 +2418,21 @@ val timer = time (timer "bounds for the new codatatypes"); - val setss_by_bnf = map (fn i => map2 (mk_hset unfs i) ls passiveAs) ks; - val setss_by_bnf' = map (fn i => map2 (mk_hset unf's i) ls passiveBs) ks; + val setss_by_bnf = map (fn i => map2 (mk_hset dtors i) ls passiveAs) ks; + val setss_by_bnf' = map (fn i => map2 (mk_hset dtor's i) ls passiveBs) ks; val setss_by_range = transpose setss_by_bnf; val set_simp_thmss = let - fun mk_simp_goal relate pas_set act_sets sets unf z set = - relate (set $ z, mk_union (pas_set $ (unf $ z), + fun mk_simp_goal relate pas_set act_sets sets dtor z set = + relate (set $ z, mk_union (pas_set $ (dtor $ z), Library.foldl1 mk_union - (map2 (fn X => mk_UNION (X $ (unf $ z))) act_sets sets))); + (map2 (fn X => mk_UNION (X $ (dtor $ z))) act_sets sets))); fun mk_goals eq = map2 (fn i => fn sets => map4 (fn Fsets => mk_simp_goal eq (nth Fsets (i - 1)) (drop m Fsets) sets) - FTs_setss unfs Jzs sets) + FTs_setss dtors Jzs sets) ls setss_by_range; val le_goals = map @@ -2456,11 +2459,11 @@ val timer = time (timer "set functions for the new codatatypes"); val colss = map2 (fn j => fn T => - map (fn i => mk_hset_rec unfs nat i j T) ks) ls passiveAs; + map (fn i => mk_hset_rec dtors nat i j T) ks) ls passiveAs; val colss' = map2 (fn j => fn T => - map (fn i => mk_hset_rec unf's nat i j T) ks) ls passiveBs; + map (fn i => mk_hset_rec dtor's nat i j T) ks) ls passiveBs; val Xcolss = map2 (fn j => fn T => - map (fn i => mk_hset_rec Xunfs nat i j T) ks) ls passiveXs; + map (fn i => mk_hset_rec Xdtors nat i j T) ks) ls passiveXs; val col_natural_thmss = let @@ -2539,7 +2542,7 @@ val cphis = map9 mk_cphi setss_by_bnf Jzs' Jzs fs_maps fs_copy_maps Jys' Jys Jys'_copy Jys_copy; - val coinduct = Drule.instantiate' cTs (map SOME cphis) unf_coinduct_thm; + val coinduct = Drule.instantiate' cTs (map SOME cphis) dtor_coinduct_thm; val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj @@ -2560,7 +2563,7 @@ val thePullTs = passiveXs @ map2 (curry HOLogic.mk_prodT) Ts Ts'; val thePull_ins = map2 (mk_in (AXs @ thePulls)) (mk_setss thePullTs) (mk_FTs thePullTs); val pickFs = map5 mk_pickWP thePull_ins pfst_Fmaps psnd_Fmaps - (map2 (curry (op $)) unfs Jzs) (map2 (curry (op $)) unf's Jz's); + (map2 (curry (op $)) dtors Jzs) (map2 (curry (op $)) dtor's Jz's); val pickF_ss = map3 (fn pickF => fn z => fn z' => HOLogic.mk_split (Term.absfree z (Term.absfree z' pickF))) pickFs Jzs' Jz's'; val picks = map (mk_coiter XTs pickF_ss) ks; @@ -2569,7 +2572,7 @@ (map8 mk_wpull AXs B1s B2s f1s f2s (replicate m NONE) p1s p2s)); val map_eq_thms = map2 (fn simp => fn diff => box_equals OF [diff RS iffD2, simp, simp]) - map_simp_thms unf_inject_thms; + map_simp_thms dtor_inject_thms; val map_wpull_thms = map (fn thm => thm OF (replicate m asm_rl @ replicate n @{thm wpull_thePull})) map_wpulls; val pickWP_assms_tacs = @@ -2591,13 +2594,13 @@ let val mor_fst = HOLogic.mk_Trueprop (mk_mor thePulls (map2 (curry HOLogic.mk_comp) p1id_Fmaps pickF_ss) - UNIVs unfs fstsTsTs'); + UNIVs dtors fstsTsTs'); val mor_snd = HOLogic.mk_Trueprop (mk_mor thePulls (map2 (curry HOLogic.mk_comp) p2id_Fmaps pickF_ss) - UNIV's unf's sndsTsTs'); + UNIV's dtor's sndsTsTs'); val mor_pick = HOLogic.mk_Trueprop (mk_mor thePulls (map2 (curry HOLogic.mk_comp) pid_Fmaps pickF_ss) - UNIV''s unf''s (map2 (curry HOLogic.mk_comp) pid_maps picks)); + UNIV''s dtor''s (map2 (curry HOLogic.mk_comp) pid_maps picks)); val fst_goal = fold_rev Logic.all (AXs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s) (Logic.mk_implies (wpull_prem, mor_fst)); @@ -2644,7 +2647,7 @@ val timer = time (timer "helpers for BNF properties"); - val map_id_tacs = map2 (K oo mk_map_id_tac map_thms) coiter_unique_thms coiter_unf_thms; + val map_id_tacs = map2 (K oo mk_map_id_tac map_thms) coiter_unique_thms coiter_dtor_thms; val map_comp_tacs = map (fn thm => K (rtac (thm RS sym) 1)) map_comp_thms; val map_cong_tacs = map (mk_map_cong_tac m) map_cong_thms; val set_nat_tacss = @@ -2673,30 +2676,30 @@ val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong_tacs set_nat_tacss bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs rel_O_Gr_tacs; - val (hset_unf_incl_thmss, hset_hset_unf_incl_thmsss, hset_induct_thms) = + val (hset_dtor_incl_thmss, hset_hset_dtor_incl_thmsss, hset_induct_thms) = let - fun tinst_of unf = - map (SOME o certify lthy) (unf :: remove (op =) unf unfs); - fun tinst_of' unf = case tinst_of unf of t :: ts => t :: NONE :: ts; + fun tinst_of dtor = + map (SOME o certify lthy) (dtor :: remove (op =) dtor dtors); + fun tinst_of' dtor = case tinst_of dtor of t :: ts => t :: NONE :: ts; val Tinst = map (pairself (certifyT lthy)) (map Logic.varifyT_global (deads @ allAs) ~~ (deads @ passiveAs @ Ts)); val set_incl_thmss = - map2 (fn unf => map (singleton (Proof_Context.export names_lthy lthy) o - Drule.instantiate' [] (tinst_of' unf) o + map2 (fn dtor => map (singleton (Proof_Context.export names_lthy lthy) o + Drule.instantiate' [] (tinst_of' dtor) o Thm.instantiate (Tinst, []) o Drule.zero_var_indexes)) - unfs set_incl_hset_thmss; - - val tinst = interleave (map (SOME o certify lthy) unfs) (replicate n NONE) + dtors set_incl_hset_thmss; + + val tinst = interleave (map (SOME o certify lthy) dtors) (replicate n NONE) val set_minimal_thms = map (Drule.instantiate' [] tinst o Thm.instantiate (Tinst, []) o Drule.zero_var_indexes) hset_minimal_thms; val set_set_incl_thmsss = - map2 (fn unf => map (map (singleton (Proof_Context.export names_lthy lthy) o - Drule.instantiate' [] (NONE :: tinst_of' unf) o + map2 (fn dtor => map (map (singleton (Proof_Context.export names_lthy lthy) o + Drule.instantiate' [] (NONE :: tinst_of' dtor) o Thm.instantiate (Tinst, []) o Drule.zero_var_indexes))) - unfs set_hset_incl_hset_thmsss; + dtors set_hset_incl_hset_thmsss; val set_set_incl_thmsss' = transpose (map transpose set_set_incl_thmsss); @@ -2843,17 +2846,17 @@ (replicate (nwits_of_bnf bnf) Ds) (replicate (nwits_of_bnf bnf) (passiveAs @ Ts)) bnf) Dss bnfs; - val fld_witss = - map (map (uncurry close_wit o tree_to_fld_wit ys flds witss o snd o snd) o + val ctor_witss = + map (map (uncurry close_wit o tree_to_ctor_wit ys ctors witss o snd o snd) o filter_out (fst o snd)) wit_treess; val all_witss = fold (fn ((i, wit), thms) => fn witss => nth_map i (fn (thms', wits) => (thms @ thms', wit :: wits)) witss) - coind_wit_thms (map (pair []) fld_witss) + coind_wit_thms (map (pair []) ctor_witss) |> map (apsnd (map snd o minimize_wits)); - val wit_tac = mk_wit_tac n unf_fld_thms (flat set_simp_thmss) (maps wit_thms_of_bnf bnfs); + val wit_tac = mk_wit_tac n dtor_ctor_thms (flat set_simp_thmss) (maps wit_thms_of_bnf bnfs); val policy = user_policy Derive_All_Facts_Note_Most; @@ -2872,8 +2875,8 @@ val timer = time (timer "registered new codatatypes as BNFs"); - val set_incl_thmss = map (map fold_sets) hset_unf_incl_thmss; - val set_set_incl_thmsss = map (map (map fold_sets)) hset_hset_unf_incl_thmsss; + val set_incl_thmss = map (map fold_sets) hset_dtor_incl_thmss; + val set_set_incl_thmsss = map (map (map fold_sets)) hset_hset_dtor_incl_thmsss; val set_induct_thms = map fold_sets hset_induct_thms; val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; @@ -2897,27 +2900,27 @@ val Jrel_simp_thms = let - fun mk_goal Jz Jz' unf unf' JrelR relR = fold_rev Logic.all (Jz :: Jz' :: JRs) + fun mk_goal Jz Jz' dtor dtor' JrelR relR = fold_rev Logic.all (Jz :: Jz' :: JRs) (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (Jz, Jz'), JrelR), - HOLogic.mk_mem (HOLogic.mk_prod (unf $ Jz, unf' $ Jz'), relR))); - val goals = map6 mk_goal Jzs Jz's unfs unf's JrelRs relRs; + HOLogic.mk_mem (HOLogic.mk_prod (dtor $ Jz, dtor' $ Jz'), relR))); + val goals = map6 mk_goal Jzs Jz's dtors dtor's JrelRs relRs; in map12 (fn i => fn goal => fn in_rel => fn map_comp => fn map_cong => - fn map_simp => fn set_simps => fn unf_inject => fn unf_fld => + fn map_simp => fn set_simps => fn dtor_inject => fn dtor_ctor => fn set_naturals => fn set_incls => fn set_set_inclss => Skip_Proof.prove lthy [] [] goal (K (mk_rel_simp_tac in_Jrels i in_rel map_comp map_cong map_simp set_simps - unf_inject unf_fld set_naturals set_incls set_set_inclss)) + dtor_inject dtor_ctor set_naturals set_incls set_set_inclss)) |> Thm.close_derivation) ks goals in_rels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss' - unf_inject_thms unf_fld_thms set_natural'ss set_incl_thmss set_set_incl_thmsss + dtor_inject_thms dtor_ctor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss end; val Jpred_simp_thms = let - fun mk_goal Jz Jz' unf unf' Jpredphi predphi = fold_rev Logic.all (Jz :: Jz' :: Jphis) - (mk_Trueprop_eq (Jpredphi $ Jz $ Jz', predphi $ (unf $ Jz) $ (unf' $ Jz'))); - val goals = map6 mk_goal Jzs Jz's unfs unf's Jpredphis predphis; + fun mk_goal Jz Jz' dtor dtor' Jpredphi predphi = fold_rev Logic.all (Jz :: Jz' :: Jphis) + (mk_Trueprop_eq (Jpredphi $ Jz $ Jz', predphi $ (dtor $ Jz) $ (dtor' $ Jz'))); + val goals = map6 mk_goal Jzs Jz's dtors dtor's Jpredphis predphis; in map3 (fn goal => fn rel_def => fn Jrel_simp => Skip_Proof.prove lthy [] [] goal @@ -2952,35 +2955,35 @@ end; val common_notes = - [(unf_coinductN, [unf_coinduct_thm]), + [(dtor_coinductN, [dtor_coinduct_thm]), (rel_coinductN, [rel_coinduct_thm]), (pred_coinductN, [pred_coinduct_thm]), - (unf_strong_coinductN, [unf_strong_coinduct_thm]), + (dtor_strong_coinductN, [dtor_strong_coinduct_thm]), (rel_strong_coinductN, [rel_strong_coinduct_thm]), (pred_strong_coinductN, [pred_strong_coinduct_thm])] |> map (fn (thmN, thms) => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); val notes = - [(unf_coitersN, coiter_thms), - (unf_coiter_uniqueN, coiter_unique_thms), - (unf_corecsN, corec_thms), - (unf_fldN, unf_fld_thms), - (fld_unfN, fld_unf_thms), - (unf_injectN, unf_inject_thms), - (unf_exhaustN, unf_exhaust_thms), - (fld_injectN, fld_inject_thms), - (fld_exhaustN, fld_exhaust_thms), - (fld_unf_coitersN, fld_coiter_thms), - (fld_unf_corecsN, fld_corec_thms)] + [(dtor_coitersN, coiter_thms), + (dtor_coiter_uniqueN, coiter_unique_thms), + (dtor_corecsN, corec_thms), + (dtor_ctorN, dtor_ctor_thms), + (ctor_dtorN, ctor_dtor_thms), + (dtor_injectN, dtor_inject_thms), + (dtor_exhaustN, dtor_exhaust_thms), + (ctor_injectN, ctor_inject_thms), + (ctor_exhaustN, ctor_exhaust_thms), + (ctor_dtor_coitersN, ctor_coiter_thms), + (ctor_dtor_corecsN, ctor_corec_thms)] |> map (apsnd (map single)) |> maps (fn (thmN, thmss) => map2 (fn b => fn thms => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) bs thmss) in - ((unfs, flds, coiters, corecs, unf_coinduct_thm, unf_fld_thms, fld_unf_thms, fld_inject_thms, - fld_coiter_thms, fld_corec_thms), + ((dtors, ctors, coiters, corecs, dtor_coinduct_thm, dtor_ctor_thms, ctor_dtor_thms, + ctor_inject_thms, ctor_coiter_thms, ctor_corec_thms), lthy |> Local_Theory.notes (common_notes @ notes) |> snd) end; diff -r 3cb59fdd69a8 -r acc9635a644a src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Fri Sep 21 15:53:29 2012 +0200 @@ -38,6 +38,11 @@ val mk_congruent_str_final_tac: int -> thm -> thm -> thm -> thm list -> tactic val mk_corec_tac: int -> thm list -> thm -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic + val mk_dtor_coinduct_tac: int -> int list -> thm -> thm -> tactic + val mk_dtor_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm -> thm -> + thm -> tactic + val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> + {prems: 'a, context: Proof.context} -> tactic val mk_equiv_lsbis_tac: thm -> thm -> thm -> thm -> thm -> thm -> tactic val mk_hset_minimal_tac: int -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic val mk_hset_rec_minimal_tac: int -> cterm option list -> thm list -> thm list -> @@ -110,11 +115,6 @@ val mk_strT_hset_tac: int -> int -> int -> ctyp option list -> ctyp option list -> cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list -> thm list list -> thm -> thm list list -> tactic - val mk_unf_coinduct_tac: int -> int list -> thm -> thm -> tactic - val mk_unf_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm -> thm -> - thm -> tactic - val mk_unf_o_fld_tac: thm -> thm -> thm -> thm -> thm list -> - {prems: 'a, context: Proof.context} -> tactic val mk_unique_mor_tac: thm list -> thm -> tactic val mk_wit_tac: int -> thm list -> thm list -> thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic @@ -1061,16 +1061,16 @@ CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) Abs_inverses, CONJ_WRAP' (fn thm => rtac ballI THEN' etac (thm RS arg_cong RS sym)) Abs_inverses] 1; -fun mk_mor_coiter_tac m mor_UNIV unf_defs coiter_defs Abs_inverses morEs map_comp_ids map_congs = +fun mk_mor_coiter_tac m mor_UNIV dtor_defs coiter_defs Abs_inverses morEs map_comp_ids map_congs = EVERY' [rtac iffD2, rtac mor_UNIV, - CONJ_WRAP' (fn ((Abs_inverse, morE), ((unf_def, coiter_def), (map_comp_id, map_cong))) => - EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (unf_def RS trans), + CONJ_WRAP' (fn ((Abs_inverse, morE), ((dtor_def, coiter_def), (map_comp_id, map_cong))) => + EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (dtor_def RS trans), rtac (coiter_def RS arg_cong RS trans), rtac (Abs_inverse RS arg_cong RS trans), rtac (morE RS arg_cong RS trans), rtac (map_comp_id RS trans), rtac (o_apply RS trans RS sym), rtac map_cong, REPEAT_DETERM_N m o rtac refl, EVERY' (map (fn thm => rtac (thm RS trans) THEN' rtac (o_apply RS sym)) coiter_defs)]) - ((Abs_inverses ~~ morEs) ~~ ((unf_defs ~~ coiter_defs) ~~ (map_comp_ids ~~ map_congs)))] 1; + ((Abs_inverses ~~ morEs) ~~ ((dtor_defs ~~ coiter_defs) ~~ (map_comp_ids ~~ map_congs)))] 1; fun mk_raw_coind_tac bis_def bis_cong bis_O bis_converse bis_Gr tcoalg coalgT mor_T_final sbis_lsbis lsbis_incls incl_lsbiss equiv_LSBISs mor_Rep Rep_injects = @@ -1109,12 +1109,12 @@ rtac @{thm image2_eqI}, rtac refl, rtac (coiter_def RS arg_cong RS trans), rtac (o_apply RS sym), rtac UNIV_I]) (raw_coinds ~~ coiter_defs) 1; -fun mk_unf_o_fld_tac fld_def coiter map_comp_id map_congL coiter_o_unfs +fun mk_dtor_o_ctor_tac ctor_def coiter map_comp_id map_congL coiter_o_dtors {context = ctxt, prems = _} = - unfold_defs_tac ctxt [fld_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply, + unfold_defs_tac ctxt [ctor_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac coiter, rtac trans, rtac map_comp_id, rtac trans, rtac map_congL, EVERY' (map (fn thm => - rtac ballI THEN' rtac (trans OF [thm RS fun_cong, @{thm id_apply}])) coiter_o_unfs), + rtac ballI THEN' rtac (trans OF [thm RS fun_cong, @{thm id_apply}])) coiter_o_dtors), rtac sym, rtac @{thm id_apply}] 1; fun mk_corec_tac m corec_defs coiter map_cong corec_Inls {context = ctxt, prems = _} = @@ -1144,7 +1144,7 @@ rtac impI, REPEAT_DETERM o etac conjE, CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) rel_Ids] 1; -fun mk_unf_coinduct_tac m ks raw_coind bis_def = +fun mk_dtor_coinduct_tac m ks raw_coind bis_def = let val n = length ks; in @@ -1165,8 +1165,8 @@ rtac CollectI, etac (refl RSN (2, @{thm subst_Pair}))]) ks] 1 end; -fun mk_unf_strong_coinduct_tac ks cTs cts unf_coinduct bis_def bis_diag = - EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts unf_coinduct), +fun mk_dtor_strong_coinduct_tac ks cTs cts dtor_coinduct bis_def bis_diag = + EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_coinduct), EVERY' (map (fn i => EVERY' [etac disjE, REPEAT_DETERM o dtac @{thm meta_spec}, etac @{thm meta_mp}, atac, rtac rev_mp, rtac subst, rtac bis_def, rtac bis_diag, @@ -1201,9 +1201,9 @@ REPEAT_DETERM_N (n - 1) o rtac @{thm Un_least}, EVERY' (map (fn thm => rtac @{thm UN_least} THEN' etac thm) set_hset_incl_hsets)] 1; -fun mk_map_id_tac maps coiter_unique coiter_unf = +fun mk_map_id_tac maps coiter_unique coiter_dtor = EVERY' [rtac (coiter_unique RS trans), EVERY' (map (fn thm => rtac (thm RS sym)) maps), - rtac coiter_unf] 1; + rtac coiter_dtor] 1; fun mk_map_comp_tac m n maps map_comps map_congs coiter_unique = EVERY' [rtac coiter_unique, @@ -1473,11 +1473,11 @@ rtac @{thm prod_caseI}, etac conjI, etac conjI, atac]) (pick_cols ~~ hset_defs)] 1; -fun mk_wit_tac n unf_flds set_simp wit coind_wits {context = ctxt, prems = _} = +fun mk_wit_tac n dtor_ctors set_simp wit coind_wits {context = ctxt, prems = _} = ALLGOALS (TRY o (eresolve_tac coind_wits THEN' rtac refl)) THEN REPEAT_DETERM (atac 1 ORELSE EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp, - K (unfold_defs_tac ctxt unf_flds), + K (unfold_defs_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac UnE, REPEAT_DETERM o (TRY o REPEAT_DETERM o etac UnE THEN' TRY o etac @{thm UN_E} THEN' @@ -1485,7 +1485,7 @@ (dresolve_tac wit THEN' (etac FalseE ORELSE' EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp, - K (unfold_defs_tac ctxt unf_flds), REPEAT_DETERM_N n o etac UnE]))))] 1); + K (unfold_defs_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac UnE]))))] 1); fun mk_coind_wit_tac induct coiters set_nats wits {context = ctxt, prems = _} = rtac induct 1 THEN ALLGOALS (TRY o rtac impI THEN' TRY o hyp_subst_tac) THEN @@ -1494,7 +1494,7 @@ ALLGOALS (TRY o FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE]) -fun mk_rel_simp_tac in_Jrels i in_rel map_comp map_cong map_simp set_simps unf_inject unf_fld +fun mk_rel_simp_tac in_Jrels i in_rel map_comp map_cong map_simp set_simps dtor_inject dtor_ctor set_naturals set_incls set_set_inclss = let val m = length set_incls; @@ -1519,7 +1519,7 @@ EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]}, REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]), - rtac trans, rtac sym, rtac map_simp, rtac (unf_inject RS iffD2), atac]) + rtac trans, rtac sym, rtac map_simp, rtac (dtor_inject RS iffD2), atac]) @{thms fst_conv snd_conv}]; val only_if_tac = EVERY' [dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], @@ -1527,11 +1527,11 @@ CONJ_WRAP' (fn (set_simp, passive_set_natural) => EVERY' [rtac ord_eq_le_trans, rtac set_simp, rtac @{thm Un_least}, rtac ord_eq_le_trans, rtac box_equals, rtac passive_set_natural, - rtac (unf_fld RS sym RS arg_cong), rtac trans_fun_cong_image_id_id_apply, atac, + rtac (dtor_ctor RS sym RS arg_cong), rtac trans_fun_cong_image_id_id_apply, atac, CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (active_set_natural, in_Jrel) => EVERY' [rtac ord_eq_le_trans, rtac @{thm UN_cong[OF _ refl]}, rtac @{thm box_equals[OF _ _ refl]}, - rtac active_set_natural, rtac (unf_fld RS sym RS arg_cong), rtac @{thm UN_least}, + rtac active_set_natural, rtac (dtor_ctor RS sym RS arg_cong), rtac @{thm UN_least}, dtac set_rev_mp, etac @{thm image_mono}, etac imageE, dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jrel RS iffD1), dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, @@ -1540,8 +1540,8 @@ (rev (active_set_naturals ~~ in_Jrels))]) (set_simps ~~ passive_set_naturals), rtac conjI, - REPEAT_DETERM_N 2 o EVERY'[rtac (unf_inject RS iffD1), rtac trans, rtac map_simp, - rtac box_equals, rtac map_comp, rtac (unf_fld RS sym RS arg_cong), rtac trans, + REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac map_simp, + rtac box_equals, rtac map_comp, rtac (dtor_ctor RS sym RS arg_cong), rtac trans, rtac map_cong, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]}, EVERY' (map (fn in_Jrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac, dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jrel RS iffD1), dtac @{thm someI_ex}, diff -r 3cb59fdd69a8 -r acc9635a644a src/HOL/Codatatype/Tools/bnf_lfp.ML --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Fri Sep 21 15:53:29 2012 +0200 @@ -994,37 +994,37 @@ val phis = map2 retype_free (map mk_pred1T Ts) init_phis; val phi2s = map2 retype_free (map2 mk_pred2T Ts Ts') init_phis; - fun fld_bind i = Binding.suffix_name ("_" ^ fldN) (nth bs (i - 1)); - val fld_name = Binding.name_of o fld_bind; - val fld_def_bind = rpair [] o Thm.def_binding o fld_bind; + fun ctor_bind i = Binding.suffix_name ("_" ^ ctorN) (nth bs (i - 1)); + val ctor_name = Binding.name_of o ctor_bind; + val ctor_def_bind = rpair [] o Thm.def_binding o ctor_bind; - fun fld_spec i abs str map_FT_init x x' = + fun ctor_spec i abs str map_FT_init x x' = let - val fldT = nth FTs (i - 1) --> nth Ts (i - 1); + val ctorT = nth FTs (i - 1) --> nth Ts (i - 1); - val lhs = Free (fld_name i, fldT); + val lhs = Free (ctor_name i, ctorT); val rhs = Term.absfree x' (abs $ (str $ (Term.list_comb (map_FT_init, map HOLogic.id_const passiveAs @ Rep_Ts) $ x))); in mk_Trueprop_eq (lhs, rhs) end; - val ((fld_frees, (_, fld_def_frees)), (lthy, lthy_old)) = + val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) = lthy |> fold_map6 (fn i => fn abs => fn str => fn mapx => fn x => fn x' => Specification.definition - (SOME (fld_bind i, NONE, NoSyn), (fld_def_bind i, fld_spec i abs str mapx x x'))) + (SOME (ctor_bind i, NONE, NoSyn), (ctor_def_bind i, ctor_spec i abs str mapx x x'))) ks Abs_Ts str_inits map_FT_inits xFs xFs' |>> apsnd split_list o split_list ||> `Local_Theory.restore; val phi = Proof_Context.export_morphism lthy_old lthy; - fun mk_flds passive = + fun mk_ctors passive = map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (mk_params passive)) o - Morphism.term phi) fld_frees; - val flds = mk_flds passiveAs; - val fld's = mk_flds passiveBs; - val fld_defs = map (Morphism.thm phi) fld_def_frees; + Morphism.term phi) ctor_frees; + val ctors = mk_ctors passiveAs; + val ctor's = mk_ctors passiveBs; + val ctor_defs = map (Morphism.thm phi) ctor_def_frees; val (mor_Rep_thm, mor_Abs_thm) = let @@ -1033,27 +1033,27 @@ val bijs = map3 mk_bij Rep_injects Reps Rep_casess; val mor_Rep = Skip_Proof.prove lthy [] [] - (HOLogic.mk_Trueprop (mk_mor UNIVs flds car_inits str_inits Rep_Ts)) - (mk_mor_Rep_tac fld_defs copy bijs inver_Abss inver_Reps) + (HOLogic.mk_Trueprop (mk_mor UNIVs ctors car_inits str_inits Rep_Ts)) + (mk_mor_Rep_tac ctor_defs copy bijs inver_Abss inver_Reps) |> Thm.close_derivation; val inv = mor_inv_thm OF [mor_Rep, talg_thm, alg_init_thm]; val mor_Abs = Skip_Proof.prove lthy [] [] - (HOLogic.mk_Trueprop (mk_mor car_inits str_inits UNIVs flds Abs_Ts)) + (HOLogic.mk_Trueprop (mk_mor car_inits str_inits UNIVs ctors Abs_Ts)) (K (mk_mor_Abs_tac inv inver_Abss inver_Reps)) |> Thm.close_derivation; in (mor_Rep, mor_Abs) end; - val timer = time (timer "fld definitions & thms"); + val timer = time (timer "ctor definitions & thms"); val iter_fun = Term.absfree iter_f' - (mk_mor UNIVs flds active_UNIVs ss (map (mk_nthN n iter_f) ks)); + (mk_mor UNIVs ctors active_UNIVs ss (map (mk_nthN n iter_f) ks)); val iter = HOLogic.choice_const iterT $ iter_fun; - fun iter_bind i = Binding.suffix_name ("_" ^ fld_iterN) (nth bs (i - 1)); + fun iter_bind i = Binding.suffix_name ("_" ^ ctor_iterN) (nth bs (i - 1)); val iter_name = Binding.name_of o iter_bind; val iter_def_bind = rpair [] o Thm.def_binding o iter_bind; @@ -1093,7 +1093,7 @@ in singleton (Proof_Context.export names_lthy lthy) (Skip_Proof.prove lthy [] [] - (HOLogic.mk_Trueprop (mk_mor UNIVs flds active_UNIVs ss (map (mk_iter Ts ss) ks))) + (HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss (map (mk_iter Ts ss) ks))) (K (mk_mor_iter_tac cT ct iter_defs ex_mor (mor_comp RS mor_cong)))) |> Thm.close_derivation end; @@ -1104,7 +1104,7 @@ val (iter_unique_mor_thms, iter_unique_mor_thm) = let - val prem = HOLogic.mk_Trueprop (mk_mor UNIVs flds active_UNIVs ss fs); + val prem = HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss fs); fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_iter Ts ss i); val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_fun_eq fs ks)); val unique_mor = Skip_Proof.prove lthy [] [] @@ -1120,106 +1120,107 @@ split_conj_thm (mk_conjIN n RS (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS iter_unique_mor_thm)) - val iter_fld_thms = + val iter_ctor_thms = map (fn thm => (mor_incl_thm OF replicate n @{thm subset_UNIV}) RS thm RS sym) iter_unique_mor_thms; - val fld_o_iter_thms = + val ctor_o_iter_thms = let val mor = mor_comp_thm OF [mor_iter_thm, mor_str_thm]; in - map2 (fn unique => fn iter_fld => - trans OF [mor RS unique, iter_fld]) iter_unique_mor_thms iter_fld_thms + map2 (fn unique => fn iter_ctor => + trans OF [mor RS unique, iter_ctor]) iter_unique_mor_thms iter_ctor_thms end; val timer = time (timer "iter definitions & thms"); - val map_flds = map2 (fn Ds => fn bnf => + val map_ctors = map2 (fn Ds => fn bnf => Term.list_comb (mk_map_of_bnf Ds (passiveAs @ FTs) (passiveAs @ Ts) bnf, - map HOLogic.id_const passiveAs @ flds)) Dss bnfs; + map HOLogic.id_const passiveAs @ ctors)) Dss bnfs; - fun unf_bind i = Binding.suffix_name ("_" ^ unfN) (nth bs (i - 1)); - val unf_name = Binding.name_of o unf_bind; - val unf_def_bind = rpair [] o Thm.def_binding o unf_bind; + fun dtor_bind i = Binding.suffix_name ("_" ^ dtorN) (nth bs (i - 1)); + val dtor_name = Binding.name_of o dtor_bind; + val dtor_def_bind = rpair [] o Thm.def_binding o dtor_bind; - fun unf_spec i FT T = + fun dtor_spec i FT T = let - val unfT = T --> FT; + val dtorT = T --> FT; - val lhs = Free (unf_name i, unfT); - val rhs = mk_iter Ts map_flds i; + val lhs = Free (dtor_name i, dtorT); + val rhs = mk_iter Ts map_ctors i; in mk_Trueprop_eq (lhs, rhs) end; - val ((unf_frees, (_, unf_def_frees)), (lthy, lthy_old)) = + val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) = lthy |> fold_map3 (fn i => fn FT => fn T => Specification.definition - (SOME (unf_bind i, NONE, NoSyn), (unf_def_bind i, unf_spec i FT T))) ks FTs Ts + (SOME (dtor_bind i, NONE, NoSyn), (dtor_def_bind i, dtor_spec i FT T))) ks FTs Ts |>> apsnd split_list o split_list ||> `Local_Theory.restore; val phi = Proof_Context.export_morphism lthy_old lthy; - fun mk_unfs params = + fun mk_dtors params = map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ params) o Morphism.term phi) - unf_frees; - val unfs = mk_unfs params'; - val unf_defs = map (Morphism.thm phi) unf_def_frees; + dtor_frees; + val dtors = mk_dtors params'; + val dtor_defs = map (Morphism.thm phi) dtor_def_frees; - val fld_o_unf_thms = map2 (fold_defs lthy o single) unf_defs fld_o_iter_thms; + val ctor_o_dtor_thms = map2 (fold_defs lthy o single) dtor_defs ctor_o_iter_thms; - val unf_o_fld_thms = + val dtor_o_ctor_thms = let - fun mk_goal unf fld FT = mk_Trueprop_eq (HOLogic.mk_comp (unf, fld), HOLogic.id_const FT); - val goals = map3 mk_goal unfs flds FTs; + fun mk_goal dtor ctor FT = + mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT); + val goals = map3 mk_goal dtors ctors FTs; in - map5 (fn goal => fn unf_def => fn iter => fn map_comp_id => fn map_congL => + map5 (fn goal => fn dtor_def => fn iter => fn map_comp_id => fn map_congL => Skip_Proof.prove lthy [] [] goal - (K (mk_unf_o_fld_tac unf_def iter map_comp_id map_congL fld_o_iter_thms)) + (K (mk_dtor_o_ctor_tac dtor_def iter map_comp_id map_congL ctor_o_iter_thms)) |> Thm.close_derivation) - goals unf_defs iter_thms map_comp_id_thms map_congL_thms + goals dtor_defs iter_thms map_comp_id_thms map_congL_thms end; - val unf_fld_thms = map (fn thm => thm RS @{thm pointfree_idE}) unf_o_fld_thms; - val fld_unf_thms = map (fn thm => thm RS @{thm pointfree_idE}) fld_o_unf_thms; + val dtor_ctor_thms = map (fn thm => thm RS @{thm pointfree_idE}) dtor_o_ctor_thms; + val ctor_dtor_thms = map (fn thm => thm RS @{thm pointfree_idE}) ctor_o_dtor_thms; - val bij_unf_thms = - map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) fld_o_unf_thms unf_o_fld_thms; - val inj_unf_thms = map (fn thm => thm RS @{thm bij_is_inj}) bij_unf_thms; - val surj_unf_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_unf_thms; - val unf_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_unf_thms; - val unf_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_unf_thms; - val unf_exhaust_thms = map (fn thm => thm RS exE) unf_nchotomy_thms; + val bij_dtor_thms = + map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) ctor_o_dtor_thms dtor_o_ctor_thms; + val inj_dtor_thms = map (fn thm => thm RS @{thm bij_is_inj}) bij_dtor_thms; + val surj_dtor_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_dtor_thms; + val dtor_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_dtor_thms; + val dtor_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_dtor_thms; + val dtor_exhaust_thms = map (fn thm => thm RS exE) dtor_nchotomy_thms; - val bij_fld_thms = - map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) unf_o_fld_thms fld_o_unf_thms; - val inj_fld_thms = map (fn thm => thm RS @{thm bij_is_inj}) bij_fld_thms; - val surj_fld_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_fld_thms; - val fld_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_fld_thms; - val fld_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_fld_thms; - val fld_exhaust_thms = map (fn thm => thm RS exE) fld_nchotomy_thms; + val bij_ctor_thms = + map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) dtor_o_ctor_thms ctor_o_dtor_thms; + val inj_ctor_thms = map (fn thm => thm RS @{thm bij_is_inj}) bij_ctor_thms; + val surj_ctor_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_ctor_thms; + val ctor_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_ctor_thms; + val ctor_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_ctor_thms; + val ctor_exhaust_thms = map (fn thm => thm RS exE) ctor_nchotomy_thms; - val timer = time (timer "unf definitions & thms"); + val timer = time (timer "dtor definitions & thms"); val fst_rec_pair_thms = let val mor = mor_comp_thm OF [mor_iter_thm, mor_convol_thm]; in - map2 (fn unique => fn iter_fld => - trans OF [mor RS unique, iter_fld]) iter_unique_mor_thms iter_fld_thms + map2 (fn unique => fn iter_ctor => + trans OF [mor RS unique, iter_ctor]) iter_unique_mor_thms iter_ctor_thms end; - fun rec_bind i = Binding.suffix_name ("_" ^ fld_recN) (nth bs (i - 1)); + fun rec_bind i = Binding.suffix_name ("_" ^ ctor_recN) (nth bs (i - 1)); val rec_name = Binding.name_of o rec_bind; val rec_def_bind = rpair [] o Thm.def_binding o rec_bind; fun rec_spec i T AT = let val recT = Library.foldr (op -->) (rec_sTs, T --> AT); - val maps = map3 (fn fld => fn prod_s => fn mapx => - mk_convol (HOLogic.mk_comp (fld, Term.list_comb (mapx, passive_ids @ rec_fsts)), prod_s)) - flds rec_ss rec_maps; + val maps = map3 (fn ctor => fn prod_s => fn mapx => + mk_convol (HOLogic.mk_comp (ctor, Term.list_comb (mapx, passive_ids @ rec_fsts)), prod_s)) + ctors rec_ss rec_maps; val lhs = Term.list_comb (Free (rec_name i, recT), rec_ss); val rhs = HOLogic.mk_comp (snd_const (HOLogic.mk_prodT (T, AT)), mk_iter Ts maps i); @@ -1246,14 +1247,14 @@ val convols = map2 (fn T => fn i => mk_convol (HOLogic.id_const T, mk_rec rec_ss i)) Ts ks; val rec_thms = let - fun mk_goal i rec_s rec_map fld x = + fun mk_goal i rec_s rec_map ctor x = let - val lhs = mk_rec rec_ss i $ (fld $ x); + val lhs = mk_rec rec_ss i $ (ctor $ x); val rhs = rec_s $ (Term.list_comb (rec_map, passive_ids @ convols) $ x); in fold_rev Logic.all (x :: rec_ss) (mk_Trueprop_eq (lhs, rhs)) end; - val goals = map5 mk_goal ks rec_ss rec_maps_rev flds xFs; + val goals = map5 mk_goal ks rec_ss rec_maps_rev ctors xFs; in map2 (fn goal => fn iter => Skip_Proof.prove lthy [] [] goal (mk_rec_tac rec_defs iter fst_rec_pair_thms) @@ -1263,9 +1264,9 @@ val timer = time (timer "rec definitions & thms"); - val (fld_induct_thm, induct_params) = + val (ctor_induct_thm, induct_params) = let - fun mk_prem phi fld sets x = + fun mk_prem phi ctor sets x = let fun mk_IH phi set z = let @@ -1276,12 +1277,12 @@ end; val IHs = map3 mk_IH phis (drop m sets) Izs; - val concl = HOLogic.mk_Trueprop (phi $ (fld $ x)); + val concl = HOLogic.mk_Trueprop (phi $ (ctor $ x)); in Logic.all x (Logic.list_implies (IHs, concl)) end; - val prems = map4 mk_prem phis flds FTs_setss xFs; + val prems = map4 mk_prem phis ctors FTs_setss xFs; fun mk_concl phi z = phi $ z; val concl = @@ -1291,7 +1292,7 @@ in (Skip_Proof.prove lthy [] [] (fold_rev Logic.all (phis @ Izs) goal) - (K (mk_fld_induct_tac m set_natural'ss init_induct_thm morE_thms mor_Abs_thm + (K (mk_ctor_induct_tac m set_natural'ss init_induct_thm morE_thms mor_Abs_thm Rep_inverses Abs_inverses Reps)) |> Thm.close_derivation, rev (Term.add_tfrees goal [])) @@ -1299,13 +1300,13 @@ val cTs = map (SOME o certifyT lthy o TFree) induct_params; - val weak_fld_induct_thms = + val weak_ctor_induct_thms = let fun insts i = (replicate (i - 1) TrueI) @ (@{thm asm_rl} :: replicate (n - i) TrueI); - in map (fn i => (fld_induct_thm OF insts i) RS mk_conjunctN n i) ks end; + in map (fn i => (ctor_induct_thm OF insts i) RS mk_conjunctN n i) ks end; - val (fld_induct2_thm, induct2_params) = + val (ctor_induct2_thm, induct2_params) = let - fun mk_prem phi fld fld' sets sets' x y = + fun mk_prem phi ctor ctor' sets sets' x y = let fun mk_IH phi set set' z1 z2 = let @@ -1317,12 +1318,12 @@ end; val IHs = map5 mk_IH phi2s (drop m sets) (drop m sets') Izs1 Izs2; - val concl = HOLogic.mk_Trueprop (phi $ (fld $ x) $ (fld' $ y)); + val concl = HOLogic.mk_Trueprop (phi $ (ctor $ x) $ (ctor' $ y)); in fold_rev Logic.all [x, y] (Logic.list_implies (IHs, concl)) end; - val prems = map7 mk_prem phi2s flds fld's FTs_setss FTs'_setss xFs yFs; + val prems = map7 mk_prem phi2s ctors ctor's FTs_setss FTs'_setss xFs yFs; fun mk_concl phi z1 z2 = phi $ z1 $ z2; val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj @@ -1334,7 +1335,7 @@ in (singleton (Proof_Context.export names_lthy lthy) (Skip_Proof.prove lthy [] [] goal - (mk_fld_induct2_tac cTs cts fld_induct_thm weak_fld_induct_thms)) + (mk_ctor_induct2_tac cTs cts ctor_induct_thm weak_ctor_induct_thms)) |> Thm.close_derivation, rev (Term.add_tfrees goal [])) end; @@ -1380,25 +1381,25 @@ mk_map_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; fun mk_passive_maps ATs BTs Ts = map2 (fn Ds => mk_map_of_bnf Ds (ATs @ Ts) (BTs @ Ts)) Dss bnfs; - fun mk_map_iter_arg fs Ts fld fmap = - HOLogic.mk_comp (fld, Term.list_comb (fmap, fs @ map HOLogic.id_const Ts)); - fun mk_map Ts fs Ts' flds mk_maps = - mk_iter Ts (map2 (mk_map_iter_arg fs Ts') flds (mk_maps Ts')); + fun mk_map_iter_arg fs Ts ctor fmap = + HOLogic.mk_comp (ctor, Term.list_comb (fmap, fs @ map HOLogic.id_const Ts)); + fun mk_map Ts fs Ts' ctors mk_maps = + mk_iter Ts (map2 (mk_map_iter_arg fs Ts') ctors (mk_maps Ts')); val pmapsABT' = mk_passive_maps passiveAs passiveBs; - val fs_maps = map (mk_map Ts fs Ts' fld's pmapsABT') ks; - val fs_copy_maps = map (mk_map Ts fs_copy Ts' fld's pmapsABT') ks; - val Yflds = mk_flds passiveYs; - val f1s_maps = map (mk_map Ts f1s YTs Yflds (mk_passive_maps passiveAs passiveYs)) ks; - val f2s_maps = map (mk_map Ts' f2s YTs Yflds (mk_passive_maps passiveBs passiveYs)) ks; - val p1s_maps = map (mk_map XTs p1s Ts flds (mk_passive_maps passiveXs passiveAs)) ks; - val p2s_maps = map (mk_map XTs p2s Ts' fld's (mk_passive_maps passiveXs passiveBs)) ks; + val fs_maps = map (mk_map Ts fs Ts' ctor's pmapsABT') ks; + val fs_copy_maps = map (mk_map Ts fs_copy Ts' ctor's pmapsABT') ks; + val Yctors = mk_ctors passiveYs; + val f1s_maps = map (mk_map Ts f1s YTs Yctors (mk_passive_maps passiveAs passiveYs)) ks; + val f2s_maps = map (mk_map Ts' f2s YTs Yctors (mk_passive_maps passiveBs passiveYs)) ks; + val p1s_maps = map (mk_map XTs p1s Ts ctors (mk_passive_maps passiveXs passiveAs)) ks; + val p2s_maps = map (mk_map XTs p2s Ts' ctor's (mk_passive_maps passiveXs passiveBs)) ks; val map_simp_thms = let - fun mk_goal fs_map map fld fld' = fold_rev Logic.all fs - (mk_Trueprop_eq (HOLogic.mk_comp (fs_map, fld), - HOLogic.mk_comp (fld', Term.list_comb (map, fs @ fs_maps)))); - val goals = map4 mk_goal fs_maps map_FTFT's flds fld's; + fun mk_goal fs_map map ctor ctor' = fold_rev Logic.all fs + (mk_Trueprop_eq (HOLogic.mk_comp (fs_map, ctor), + HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ fs_maps)))); + val goals = map4 mk_goal fs_maps map_FTFT's ctors ctor's; val maps = map4 (fn goal => fn iter => fn map_comp_id => fn map_cong => Skip_Proof.prove lthy [] [] goal (K (mk_map_tac m n iter map_comp_id map_cong)) @@ -1410,10 +1411,10 @@ val (map_unique_thms, map_unique_thm) = let - fun mk_prem u map fld fld' = - mk_Trueprop_eq (HOLogic.mk_comp (u, fld), - HOLogic.mk_comp (fld', Term.list_comb (map, fs @ us))); - val prems = map4 mk_prem us map_FTFT's flds fld's; + fun mk_prem u map ctor ctor' = + mk_Trueprop_eq (HOLogic.mk_comp (u, ctor), + HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ us))); + val prems = map4 mk_prem us map_FTFT's ctors ctor's; val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) us fs_maps)); @@ -1455,23 +1456,23 @@ val set_simp_thmss = let - fun mk_goal sets fld set col map = - mk_Trueprop_eq (HOLogic.mk_comp (set, fld), + fun mk_goal sets ctor set col map = + mk_Trueprop_eq (HOLogic.mk_comp (set, ctor), HOLogic.mk_comp (col, Term.list_comb (map, passive_ids @ sets))); val goalss = - map3 (fn sets => map4 (mk_goal sets) flds sets) setss_by_range colss map_setss; + map3 (fn sets => map4 (mk_goal sets) ctors sets) setss_by_range colss map_setss; val setss = map (map2 (fn iter => fn goal => Skip_Proof.prove lthy [] [] goal (K (mk_set_tac iter)) |> Thm.close_derivation) iter_thms) goalss; - fun mk_simp_goal pas_set act_sets sets fld z set = - Logic.all z (mk_Trueprop_eq (set $ (fld $ z), + fun mk_simp_goal pas_set act_sets sets ctor z set = + Logic.all z (mk_Trueprop_eq (set $ (ctor $ z), mk_union (pas_set $ z, Library.foldl1 mk_union (map2 (fn X => mk_UNION (X $ z)) act_sets sets)))); val simp_goalss = map2 (fn i => fn sets => map4 (fn Fsets => mk_simp_goal (nth Fsets (i - 1)) (drop m Fsets) sets) - FTs_setss flds xFs sets) + FTs_setss ctors xFs sets) ls setss_by_range; val set_simpss = map3 (fn i => map3 (fn set_nats => fn goal => fn set => @@ -1511,7 +1512,7 @@ (map4 (mk_cphi f) fs_maps Izs sets sets')) fs setss_by_range setss_by_range'; val inducts = map (fn cphis => - Drule.instantiate' cTs (map SOME cphis @ cxs) fld_induct_thm) cphiss; + Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss; val goals = map3 (fn f => fn sets => fn sets' => @@ -1539,7 +1540,7 @@ val cphiss = map (map2 mk_cphi Izs) setss_by_range; val inducts = map (fn cphis => - Drule.instantiate' cTs (map SOME cphis @ cxs) fld_induct_thm) cphiss; + Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss; val goals = map (fn sets => @@ -1572,7 +1573,7 @@ val cphis = map4 mk_cphi setss_by_bnf Izs fs_maps fs_copy_maps; - val induct = Drule.instantiate' cTs (map SOME cphis @ cxs) fld_induct_thm; + val induct = Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm; val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj @@ -1592,14 +1593,14 @@ HOLogic.mk_mem (z, mk_in As sets (fastype_of z)); fun mk_incl z sets i = - HOLogic.mk_imp (mk_prem z sets, HOLogic.mk_mem (z, mk_min_alg As flds i)); + HOLogic.mk_imp (mk_prem z sets, HOLogic.mk_mem (z, mk_min_alg As ctors i)); fun mk_cphi z sets i = certify lthy (Term.absfree (dest_Free z) (mk_incl z sets i)); val cphis = map3 mk_cphi Izs setss_by_bnf ks; - val induct = Drule.instantiate' cTs (map SOME cphis @ cxs) fld_induct_thm; + val induct = Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm; val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj @@ -1641,7 +1642,7 @@ val cphis = map3 mk_cphi Izs1' Izs2' goals; - val induct = Drule.instantiate' cTs (map SOME cphis @ cxs) fld_induct2_thm; + val induct = Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct2_thm; val goal = Logic.list_implies (map HOLogic.mk_Trueprop (map8 mk_wpull AXs B1s B2s f1s f2s (replicate m NONE) p1s p2s), @@ -1650,7 +1651,7 @@ val thm = singleton (Proof_Context.export names_lthy lthy) (Skip_Proof.prove lthy [] [] goal (K (mk_lfp_map_wpull_tac m (rtac induct) map_wpulls map_simp_thms - (transpose set_simp_thmss) Fset_set_thmsss fld_inject_thms))) + (transpose set_simp_thmss) Fset_set_thmsss ctor_inject_thms))) |> Thm.close_derivation; in split_conj_thm thm @@ -1675,7 +1676,7 @@ val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong_tacs set_nat_tacss bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs rel_O_Gr_tacs; - val fld_witss = + val ctor_witss = let val witss = map2 (fn Ds => fn bnf => mk_wits_of_bnf (replicate (nwits_of_bnf bnf) Ds) @@ -1686,18 +1687,18 @@ fun gen_arg support i = if i < m then [([i], nth ys i)] - else maps (mk_wit support (nth flds (i - m)) (i - m)) (nth support (i - m)) - and mk_wit support fld i (I, wit) = + else maps (mk_wit support (nth ctors (i - m)) (i - m)) (nth support (i - m)) + and mk_wit support ctor i (I, wit) = let val args = map (gen_arg (nth_map i (remove (op =) (I, wit)) support)) I; in (args, [([], wit)]) |-> fold (map_product wit_apply) - |> map (apsnd (fn t => fld $ t)) + |> map (apsnd (fn t => ctor $ t)) |> minimize_wits end; in - map3 (fn fld => fn i => map close_wit o minimize_wits o maps (mk_wit witss fld i)) - flds (0 upto n - 1) witss + map3 (fn ctor => fn i => map close_wit o minimize_wits o maps (mk_wit witss ctor i)) + ctors (0 upto n - 1) witss end; fun wit_tac _ = mk_wit_tac n (flat set_simp_thmss) (maps wit_thms_of_bnf bnfs); @@ -1709,7 +1710,7 @@ bnf_def Dont_Inline policy I tacs wit_tac (SOME deads) (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE) lthy |> register_bnf (Local_Theory.full_name lthy b)) - tacss bs fs_maps setss_by_bnf Ts fld_witss lthy; + tacss bs fs_maps setss_by_bnf Ts ctor_witss lthy; val fold_maps = fold_defs lthy (map (fn bnf => mk_unabs_def m (map_def_of_bnf bnf RS @{thm meta_eq_to_obj_eq})) Ibnfs); @@ -1743,27 +1744,27 @@ val Irel_simp_thms = let - fun mk_goal xF yF fld fld' IrelR relR = fold_rev Logic.all (xF :: yF :: IRs) - (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (fld $ xF, fld' $ yF), IrelR), + fun mk_goal xF yF ctor ctor' IrelR relR = fold_rev Logic.all (xF :: yF :: IRs) + (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (ctor $ xF, ctor' $ yF), IrelR), HOLogic.mk_mem (HOLogic.mk_prod (xF, yF), relR))); - val goals = map6 mk_goal xFs yFs flds fld's IrelRs relRs; + val goals = map6 mk_goal xFs yFs ctors ctor's IrelRs relRs; in map12 (fn i => fn goal => fn in_rel => fn map_comp => fn map_cong => - fn map_simp => fn set_simps => fn fld_inject => fn fld_unf => + fn map_simp => fn set_simps => fn ctor_inject => fn ctor_dtor => fn set_naturals => fn set_incls => fn set_set_inclss => Skip_Proof.prove lthy [] [] goal (K (mk_rel_simp_tac in_Irels i in_rel map_comp map_cong map_simp set_simps - fld_inject fld_unf set_naturals set_incls set_set_inclss)) + ctor_inject ctor_dtor set_naturals set_incls set_set_inclss)) |> Thm.close_derivation) ks goals in_rels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss' - fld_inject_thms fld_unf_thms set_natural'ss set_incl_thmss set_set_incl_thmsss + ctor_inject_thms ctor_dtor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss end; val Ipred_simp_thms = let - fun mk_goal xF yF fld fld' Ipredphi predphi = fold_rev Logic.all (xF :: yF :: Iphis) - (mk_Trueprop_eq (Ipredphi $ (fld $ xF) $ (fld' $ yF), predphi $ xF $ yF)); - val goals = map6 mk_goal xFs yFs flds fld's Ipredphis predphis; + fun mk_goal xF yF ctor ctor' Ipredphi predphi = fold_rev Logic.all (xF :: yF :: Iphis) + (mk_Trueprop_eq (Ipredphi $ (ctor $ xF) $ (ctor' $ yF), predphi $ xF $ yF)); + val goals = map6 mk_goal xFs yFs ctors ctor's Ipredphis predphis; in map3 (fn goal => fn rel_def => fn Irel_simp => Skip_Proof.prove lthy [] [] goal @@ -1797,28 +1798,28 @@ end; val common_notes = - [(fld_inductN, [fld_induct_thm]), - (fld_induct2N, [fld_induct2_thm])] + [(ctor_inductN, [ctor_induct_thm]), + (ctor_induct2N, [ctor_induct2_thm])] |> map (fn (thmN, thms) => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); val notes = - [(fld_itersN, iter_thms), - (fld_iter_uniqueN, iter_unique_thms), - (fld_recsN, rec_thms), - (unf_fldN, unf_fld_thms), - (fld_unfN, fld_unf_thms), - (unf_injectN, unf_inject_thms), - (unf_exhaustN, unf_exhaust_thms), - (fld_injectN, fld_inject_thms), - (fld_exhaustN, fld_exhaust_thms)] + [(ctor_dtorN, ctor_dtor_thms), + (ctor_exhaustN, ctor_exhaust_thms), + (ctor_injectN, ctor_inject_thms), + (ctor_iter_uniqueN, iter_unique_thms), + (ctor_itersN, iter_thms), + (ctor_recsN, rec_thms), + (dtor_ctorN, dtor_ctor_thms), + (dtor_exhaustN, dtor_exhaust_thms), + (dtor_injectN, dtor_inject_thms)] |> map (apsnd (map single)) |> maps (fn (thmN, thmss) => map2 (fn b => fn thms => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) bs thmss) in - ((unfs, flds, iters, recs, fld_induct_thm, unf_fld_thms, fld_unf_thms, fld_inject_thms, + ((dtors, ctors, iters, recs, ctor_induct_thm, dtor_ctor_thms, ctor_dtor_thms, ctor_inject_thms, iter_thms, rec_thms), lthy |> Local_Theory.notes (common_notes @ notes) |> snd) end; diff -r 3cb59fdd69a8 -r acc9635a644a src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML Fri Sep 21 15:53:29 2012 +0200 @@ -18,11 +18,11 @@ val mk_card_of_min_alg_tac: thm -> thm -> thm -> thm -> thm -> tactic val mk_copy_alg_tac: thm list list -> thm list -> thm -> thm -> thm -> tactic val mk_copy_str_tac: thm list list -> thm -> thm list -> tactic - val mk_ex_copy_alg_tac: int -> thm -> thm -> tactic - val mk_fld_induct2_tac: ctyp option list -> cterm option list -> thm -> thm list -> + val mk_ctor_induct_tac: int -> thm list list -> thm -> thm list -> thm -> thm list -> thm list -> + thm list -> tactic + val mk_ctor_induct2_tac: ctyp option list -> cterm option list -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic - val mk_fld_induct_tac: int -> thm list list -> thm -> thm list -> thm -> thm list -> thm list -> - thm list -> tactic + val mk_ex_copy_alg_tac: int -> thm -> thm -> tactic val mk_in_bd_tac: thm -> thm -> thm -> thm -> tactic val mk_incl_min_alg_tac: (int -> tactic) -> thm list list list -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic @@ -70,7 +70,7 @@ val mk_set_natural_tac: thm -> tactic val mk_set_simp_tac: thm -> thm -> thm list -> tactic val mk_set_tac: thm -> tactic - val mk_unf_o_fld_tac: thm -> thm -> thm -> thm -> thm list -> tactic + val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> tactic val mk_wit_tac: int -> thm list -> thm list -> tactic val mk_wpull_tac: thm -> tactic end; @@ -485,8 +485,8 @@ CONJ_WRAP' mk_induct_tac least_min_algs 1 end; -fun mk_mor_Rep_tac fld_defs copy bijs inver_Abss inver_Reps {context = ctxt, prems = _} = - (K (unfold_defs_tac ctxt fld_defs) THEN' rtac conjunct1 THEN' rtac copy THEN' +fun mk_mor_Rep_tac ctor_defs copy bijs inver_Abss inver_Reps {context = ctxt, prems = _} = + (K (unfold_defs_tac ctxt ctor_defs) THEN' rtac conjunct1 THEN' rtac copy THEN' EVERY' (map (fn bij => EVERY' [rtac bij, atac, etac bexI, rtac UNIV_I]) bijs) THEN' EVERY' (map rtac inver_Abss) THEN' EVERY' (map rtac inver_Reps)) 1; @@ -514,11 +514,11 @@ CONJ_WRAP' mk_unique type_defs 1 end; -fun mk_unf_o_fld_tac unf_def iter map_comp_id map_congL fld_o_iters = - EVERY' [stac unf_def, rtac ext, rtac trans, rtac o_apply, rtac trans, rtac iter, +fun mk_dtor_o_ctor_tac dtor_def iter map_comp_id map_congL ctor_o_iters = + EVERY' [stac dtor_def, rtac ext, rtac trans, rtac o_apply, rtac trans, rtac iter, rtac trans, rtac map_comp_id, rtac trans, rtac map_congL, EVERY' (map (fn thm => rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply])) - fld_o_iters), + ctor_o_iters), rtac sym, rtac id_apply] 1; fun mk_rec_tac rec_defs iter fst_recs {context = ctxt, prems = _}= @@ -527,7 +527,7 @@ EVERY' [rtac trans, rtac o_apply, rtac trans, rtac (iter RS @{thm arg_cong[of _ _ snd]}), rtac @{thm snd_convol'}] 1; -fun mk_fld_induct_tac m set_natural'ss init_induct morEs mor_Abs Rep_invs Abs_invs Reps = +fun mk_ctor_induct_tac m set_natural'ss init_induct morEs mor_Abs Rep_invs Abs_invs Reps = let val n = length set_natural'ss; val ks = 1 upto n; @@ -552,9 +552,9 @@ DETERM o CONJ_WRAP' mk_closed_tac (ks ~~ (morEs ~~ set_natural'ss))) 1 end; -fun mk_fld_induct2_tac cTs cts fld_induct weak_fld_inducts {context = ctxt, prems = _} = +fun mk_ctor_induct2_tac cTs cts ctor_induct weak_ctor_inducts {context = ctxt, prems = _} = let - val n = length weak_fld_inducts; + val n = length weak_ctor_inducts; val ks = 1 upto n; fun mk_inner_induct_tac induct i = EVERY' [rtac allI, fo_rtac induct ctxt, @@ -564,8 +564,8 @@ REPEAT_DETERM o dtac @{thm meta_spec}, etac (spec RS meta_mp), atac], atac]; in - EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts fld_induct), - EVERY' (map2 mk_inner_induct_tac weak_fld_inducts ks), rtac impI, + EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts ctor_induct), + EVERY' (map2 mk_inner_induct_tac weak_ctor_inducts ks), rtac impI, REPEAT_DETERM o eresolve_tac [conjE, allE], CONJ_WRAP' (K atac) ks] 1 end; @@ -676,7 +676,7 @@ (induct_tac THEN' EVERY' (map2 mk_incl alg_sets set_setsss)) 1 end; -fun mk_lfp_map_wpull_tac m induct_tac wpulls map_simps set_simpss set_setsss fld_injects = +fun mk_lfp_map_wpull_tac m induct_tac wpulls map_simps set_simpss set_setsss ctor_injects = let val n = length wpulls; val ks = 1 upto n; @@ -701,7 +701,7 @@ EVERY' [rtac @{thm UN_least}, rtac CollectE, etac set_rev_mp, atac, REPEAT_DETERM o etac conjE, atac]]; - fun mk_wpull wpull map_simp set_simps set_setss fld_inject = + fun mk_wpull wpull map_simp set_simps set_setss ctor_inject = EVERY' [rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac rev_mp, rtac wpull, EVERY' (map (fn i => REPEAT_DETERM_N (i - 1) o etac thin_rl THEN' atac) ls), @@ -712,12 +712,12 @@ CONJ_WRAP' (K (rtac subset_refl)) ks, rtac conjI, rtac CollectI, EVERY' (map (use_pass_asm o hd) set_setss), CONJ_WRAP' (K (rtac subset_refl)) ks, - rtac subst, rtac fld_inject, rtac trans, rtac sym, rtac map_simp, + rtac subst, rtac ctor_inject, rtac trans, rtac sym, rtac map_simp, rtac trans, atac, rtac map_simp, REPEAT_DETERM o eresolve_tac [CollectE, conjE, bexE], hyp_subst_tac, rtac bexI, rtac conjI, rtac map_simp, rtac map_simp, rtac CollectI, CONJ_WRAP' mk_subset set_simps]; in - (induct_tac THEN' EVERY' (map5 mk_wpull wpulls map_simps set_simpss set_setsss fld_injects)) 1 + (induct_tac THEN' EVERY' (map5 mk_wpull wpulls map_simps set_simpss set_setsss ctor_injects)) 1 end; (* BNF tactics *) @@ -770,29 +770,29 @@ EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp, REPEAT_DETERM_N n o etac UnE]))))] 1); -fun mk_rel_simp_tac in_Irels i in_rel map_comp map_cong map_simp set_simps fld_inject - fld_unf set_naturals set_incls set_set_inclss = +fun mk_rel_simp_tac in_Irels i in_rel map_comp map_cong map_simp set_simps ctor_inject + ctor_dtor set_naturals set_incls set_set_inclss = let val m = length set_incls; val n = length set_set_inclss; val (passive_set_naturals, active_set_naturals) = chop m set_naturals; val in_Irel = nth in_Irels (i - 1); - val le_arg_cong_fld_unf = fld_unf RS arg_cong RS ord_eq_le_trans; - val eq_arg_cong_fld_unf = fld_unf RS arg_cong RS trans; + val le_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS ord_eq_le_trans; + val eq_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS trans; val if_tac = EVERY' [dtac (in_Irel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI, EVERY' (map2 (fn set_natural => fn set_incl => EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_natural, rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply, - rtac (set_incl RS subset_trans), etac le_arg_cong_fld_unf]) + rtac (set_incl RS subset_trans), etac le_arg_cong_ctor_dtor]) passive_set_naturals set_incls), CONJ_WRAP' (fn (in_Irel, (set_natural, set_set_incls)) => EVERY' [rtac ord_eq_le_trans, rtac set_natural, rtac @{thm image_subsetI}, rtac (in_Irel RS iffD2), rtac exI, rtac conjI, rtac CollectI, CONJ_WRAP' (fn thm => - EVERY' (map etac [thm RS subset_trans, le_arg_cong_fld_unf])) + EVERY' (map etac [thm RS subset_trans, le_arg_cong_ctor_dtor])) set_set_incls, rtac conjI, rtac refl, rtac refl]) (in_Irels ~~ (active_set_naturals ~~ set_set_inclss)), @@ -800,8 +800,8 @@ EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]}, REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]), - rtac (fld_inject RS iffD1), rtac trans, rtac sym, rtac map_simp, - etac eq_arg_cong_fld_unf]) + rtac (ctor_inject RS iffD1), rtac trans, rtac sym, rtac map_simp, + etac eq_arg_cong_ctor_dtor]) fst_snd_convs]; val only_if_tac = EVERY' [dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], @@ -821,7 +821,7 @@ (rev (active_set_naturals ~~ in_Irels))]) (set_simps ~~ passive_set_naturals), rtac conjI, - REPEAT_DETERM_N 2 o EVERY' [rtac trans, rtac map_simp, rtac (fld_inject RS iffD2), + REPEAT_DETERM_N 2 o EVERY' [rtac trans, rtac map_simp, rtac (ctor_inject RS iffD2), rtac trans, rtac map_comp, rtac trans, rtac map_cong, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]}, EVERY' (map (fn in_Irel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,