--- 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"
--- 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
--- 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;
--- 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;
--- 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},
--- 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;
--- 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,