--- a/src/HOL/Codatatype/Tools/bnf_comp.ML Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML Thu Sep 20 02:42:48 2012 +0200
@@ -40,19 +40,16 @@
};
fun add_to_thms thms NONE = thms
- | add_to_thms thms (SOME new) = if Thm.is_reflexive new then thms else insert Thm.eq_thm new thms;
+ | add_to_thms thms (SOME new) = thms |> not (Thm.is_reflexive new) ? insert Thm.eq_thm new;
fun adds_to_thms thms NONE = thms
- | adds_to_thms thms (SOME news) = insert (eq_set Thm.eq_thm) (filter_out_refl news) thms;
-
-fun mk_unfold_thms maps setss rels = {map_unfolds = maps, set_unfoldss = setss, rel_unfolds = rels};
+ | adds_to_thms thms (SOME news) = insert (eq_set Thm.eq_thm) (no_reflexive news) thms;
-val empty_unfold = mk_unfold_thms [] [] [];
+val empty_unfold = {map_unfolds = [], set_unfoldss = [], rel_unfolds = []};
-fun add_to_unfold_opt map_opt sets_opt rel_opt
- {map_unfolds = maps, set_unfoldss = setss, rel_unfolds = rels} = {
- map_unfolds = add_to_thms maps map_opt,
- set_unfoldss = adds_to_thms setss sets_opt,
- rel_unfolds = add_to_thms rels rel_opt};
+fun add_to_unfold_opt map_opt sets_opt rel_opt {map_unfolds, set_unfoldss, rel_unfolds} = {
+ map_unfolds = add_to_thms map_unfolds map_opt,
+ set_unfoldss = adds_to_thms set_unfoldss sets_opt,
+ rel_unfolds = add_to_thms rel_unfolds rel_opt};
fun add_to_unfold map sets rel = add_to_unfold_opt (SOME map) (SOME sets) (SOME rel);
@@ -243,7 +240,7 @@
(map (fn bnf => rel_O_Gr_of_bnf bnf RS sym) inners)]]] RS sym) 1
end
- val tacs = zip_goals map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
+ val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac;
val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
@@ -353,7 +350,7 @@
replicate (live - n) @{thm Gr_fst_snd})]]] RS sym) 1
end;
- val tacs = zip_goals map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
+ val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac;
val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
@@ -444,7 +441,7 @@
fun rel_O_Gr_tac _ =
rtac (trans OF [rel_O_Gr_of_bnf bnf, in_alt_thm RS subst_rel_def RS sym]) 1;
- val tacs = zip_goals map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
+ val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac;
val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -522,7 +519,7 @@
fun rel_O_Gr_tac _ =
rtac (trans OF [rel_O_Gr_of_bnf bnf, in_alt_thm RS subst_rel_def RS sym]) 1;
- val tacs = zip_goals map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
+ val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac;
val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -608,9 +605,9 @@
val (Bs, _) = apfst (map TFree)
(Variable.invent_types (replicate live HOLogic.typeS) lthy1);
- val map_unfolds = filter_out_refl (map_unfolds_of unfold);
- val set_unfoldss = map filter_out_refl (set_unfoldss_of unfold);
- val rel_unfolds = filter_out_refl (rel_unfolds_of unfold);
+ val map_unfolds = map_unfolds_of unfold;
+ val set_unfoldss = set_unfoldss_of unfold;
+ val rel_unfolds = rel_unfolds_of unfold;
val expand_maps = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of)
map_unfolds);
@@ -661,7 +658,7 @@
fun mk_tac thm {context = ctxt, prems = _} = (rtac (unfold_defs thm) THEN'
SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1;
- val tacs = zip_goals (mk_tac (map_id_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf))
+ val tacs = zip_axioms (mk_tac (map_id_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf))
(mk_tac (map_cong_of_bnf bnf)) (map mk_tac (set_natural_of_bnf bnf))
(K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) (mk_tac in_bd)
(mk_tac (map_wpull_of_bnf bnf)) (mk_tac (rel_O_Gr_of_bnf bnf));
--- a/src/HOL/Codatatype/Tools/bnf_def.ML Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML Thu Sep 20 02:42:48 2012 +0200
@@ -77,8 +77,8 @@
val minimize_wits: (''a list * 'b) list -> (''a list * 'b) list
val wits_of_bnf: BNF -> nonemptiness_witness list
- val filter_out_refl: thm list -> thm list
- val zip_goals: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a -> 'a list
+ val no_reflexive: thm list -> thm list
+ val zip_axioms: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a -> 'a list
datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline
datatype fact_policy =
@@ -134,10 +134,13 @@
||> the_single
|> mk_axioms';
+fun zip_axioms mid mcomp mcong snat bdco bdinf sbd inbd wpull rel =
+ [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull, rel];
+
fun dest_axioms {map_id, map_comp, map_cong, set_natural, bd_card_order, bd_cinfinite, set_bd,
in_bd, map_wpull, rel_O_Gr} =
- [map_id, map_comp, map_cong] @ set_natural @ [bd_card_order, bd_cinfinite] @
- set_bd @ [in_bd, map_wpull, rel_O_Gr];
+ zip_axioms map_id map_comp map_cong set_natural bd_card_order bd_cinfinite set_bd in_bd map_wpull
+ rel_O_Gr;
fun map_axioms f
{map_id = map_id, map_comp = map_comp, map_cong = map_cong, set_natural = set_natural,
@@ -513,21 +516,12 @@
val smart_max_inline_size = 25; (*FUDGE*)
-val no_def = Drule.reflexive_thm;
-val no_fact = refl;
+fun is_refl thm =
+ op aconv (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of thm)))
+ handle TERM _ => false;
-fun is_reflexive th =
- let val t = Thm.prop_of th;
- in
- op aconv (Logic.dest_equals t)
- handle TERM _ => op aconv (HOLogic.dest_eq (HOLogic.dest_Trueprop t))
- handle TERM _ => false
- end;
-
-val filter_out_refl = filter_out is_reflexive;
-
-fun zip_goals mid mcomp mcong snat bdco bdinf sbd inbd wpull rel =
- [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull, rel];
+val no_refl = filter_out is_refl;
+val no_reflexive = filter_out Thm.is_reflexive;
(* Define new BNFs *)
@@ -569,7 +563,7 @@
| Do_Inline => true)
in
if inline then
- ((rhs, no_def), lthy)
+ ((rhs, Drule.reflexive_thm), lthy)
else
let val b = b () in
apfst (apsnd snd) (Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []), rhs))
@@ -733,9 +727,7 @@
||> `(maybe_restore lthy);
val phi = Proof_Context.export_morphism lthy_old lthy;
-
val bnf_rel_def = Morphism.thm phi raw_rel_def;
-
val bnf_rel = Morphism.term phi bnf_rel_term;
fun mk_bnf_rel setRTs CA' CB' = normalize_rel lthy setRTs CA' CB' bnf_rel;
@@ -754,20 +746,14 @@
||> `(maybe_restore lthy);
val phi = Proof_Context.export_morphism lthy_old lthy;
-
- val bnf_pred_def =
- if fact_policy <> Derive_Some_Facts then
- mk_unabs_def (live + 2) (Morphism.thm phi raw_pred_def RS meta_eq_to_obj_eq)
- else
- no_fact;
-
+ val bnf_pred_def = Morphism.thm phi raw_pred_def;
val bnf_pred = Morphism.term phi bnf_pred_term;
fun mk_bnf_pred QTs CA' CB' = normalize_pred lthy QTs CA' CB' bnf_pred;
val pred = mk_bnf_pred QTs CA' CB';
- val _ = case filter_out_refl (raw_map_def :: raw_set_defs @ [raw_bd_def] @
+ val _ = case no_reflexive (raw_map_def :: raw_set_defs @ [raw_bd_def] @
raw_wit_defs @ [raw_rel_def, raw_pred_def]) of
[] => ()
| defs => Proof_Display.print_consts true lthy_old (K false)
@@ -868,7 +854,7 @@
val rel_O_Gr_goal =
fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (relAsBs, Rs), rel_O_Gr_rhs));
- val goals = zip_goals map_id_goal map_comp_goal map_cong_goal set_naturals_goal
+ val goals = zip_axioms map_id_goal map_comp_goal map_cong_goal set_naturals_goal
card_order_bd_goal cinfinite_bd_goal set_bds_goal in_bd_goal map_wpull_goal rel_O_Gr_goal;
fun mk_wit_goals (I, wit) =
@@ -990,7 +976,7 @@
|> Thm.close_derivation
end;
- val rel_O_Gr = #rel_O_Gr axioms;
+ val rel_O_Grs = no_refl [#rel_O_Gr axioms];
val map_wppull = mk_lazy mk_map_wppull;
@@ -1001,7 +987,7 @@
val goal = fold_rev Logic.all (As @ fs) (mk_Trueprop_eq (lhs, rhs));
in
Skip_Proof.prove lthy [] [] goal
- (mk_rel_Gr_tac rel_O_Gr (#map_id axioms) (#map_cong axioms)
+ (mk_rel_Gr_tac rel_O_Grs (#map_id axioms) (#map_cong axioms)
(#map_wpull axioms) (Lazy.force in_cong) (Lazy.force map_id')
(Lazy.force map_comp') (map Lazy.force set_natural'))
|> Thm.close_derivation
@@ -1020,7 +1006,7 @@
in
Skip_Proof.prove lthy [] []
(fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (mono_prems, mono_concl)))
- (mk_rel_mono_tac rel_O_Gr (Lazy.force in_mono))
+ (mk_rel_mono_tac rel_O_Grs (Lazy.force in_mono))
|> Thm.close_derivation
end;
@@ -1056,7 +1042,7 @@
val rhs = mk_converse (Term.list_comb (relAsBs, Rs));
val le_goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (mk_subset lhs rhs));
val le_thm = Skip_Proof.prove lthy [] [] le_goal
- (mk_rel_converse_le_tac rel_O_Gr (Lazy.force rel_Id) (#map_cong axioms)
+ (mk_rel_converse_le_tac rel_O_Grs (Lazy.force rel_Id) (#map_cong axioms)
(Lazy.force map_comp') (map Lazy.force set_natural'))
|> Thm.close_derivation
val goal = fold_rev Logic.all Rs (mk_Trueprop_eq (lhs, rhs));
@@ -1076,7 +1062,7 @@
val goal = fold_rev Logic.all (Rs @ Ss) (mk_Trueprop_eq (lhs, rhs));
in
Skip_Proof.prove lthy [] [] goal
- (mk_rel_O_tac rel_O_Gr (Lazy.force rel_Id) (#map_cong axioms)
+ (mk_rel_O_tac rel_O_Grs (Lazy.force rel_Id) (#map_cong axioms)
(Lazy.force map_wppull) (Lazy.force map_comp') (map Lazy.force set_natural'))
|> Thm.close_derivation
end;
@@ -1097,7 +1083,7 @@
val goal =
fold_rev Logic.all (x :: y :: Rs) (mk_Trueprop_eq (lhs, rhs));
in
- Skip_Proof.prove lthy [] [] goal (mk_in_rel_tac rel_O_Gr (length bnf_sets))
+ Skip_Proof.prove lthy [] [] goal (mk_in_rel_tac rel_O_Grs (length bnf_sets))
|> Thm.close_derivation
end;
@@ -1152,7 +1138,7 @@
let
val notes =
[(map_congN, [#map_cong axioms]),
- (rel_O_GrN, [rel_O_Gr]),
+ (rel_O_GrN, rel_O_Grs),
(rel_IdN, [Lazy.force (#rel_Id facts)]),
(rel_GrN, [Lazy.force (#rel_Gr facts)]),
(rel_converseN, [Lazy.force (#rel_converse facts)]),
@@ -1161,6 +1147,7 @@
(map_id'N, [Lazy.force (#map_id' facts)]),
(map_comp'N, [Lazy.force (#map_comp' facts)]),
(set_natural'N, map Lazy.force (#set_natural' facts))]
+ |> filter_out (null o #2)
|> map (fn (thmN, thms) =>
((qualify (Binding.qualify true (Binding.name_of b) (Binding.name thmN)), []),
[(thms, [])]));
@@ -1172,7 +1159,7 @@
end;
val one_step_defs =
- filter_out_refl (bnf_map_def :: bnf_bd_def :: bnf_set_defs @ bnf_wit_defs @ [bnf_rel_def]);
+ no_reflexive (bnf_map_def :: bnf_bd_def :: bnf_set_defs @ bnf_wit_defs @ [bnf_rel_def]);
in
(key, goals, wit_goalss, after_qed, lthy, one_step_defs)
end;
--- a/src/HOL/Codatatype/Tools/bnf_def_tactics.ML Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def_tactics.ML Thu Sep 20 02:42:48 2012 +0200
@@ -15,16 +15,16 @@
val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic
val mk_set_natural': thm -> thm
- val mk_rel_Gr_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
+ val mk_rel_Gr_tac: thm list -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
{prems: thm list, context: Proof.context} -> tactic
val mk_rel_Id_tac: int -> thm -> thm -> {prems: 'a, context: Proof.context} -> tactic
- val mk_rel_O_tac: thm -> thm -> thm -> thm -> thm -> thm list ->
+ val mk_rel_O_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
{prems: thm list, context: Proof.context} -> tactic
- val mk_in_rel_tac: thm -> int -> {prems: 'b, context: Proof.context} -> tactic
+ val mk_in_rel_tac: thm list -> int -> {prems: 'b, context: Proof.context} -> tactic
val mk_rel_converse_tac: thm -> tactic
- val mk_rel_converse_le_tac: thm -> thm -> thm -> thm -> thm list ->
+ val mk_rel_converse_le_tac: thm list -> thm -> thm -> thm -> thm list ->
{prems: thm list, context: Proof.context} -> tactic
- val mk_rel_mono_tac: thm -> thm -> {prems: 'a, context: Proof.context} -> tactic
+ val mk_rel_mono_tac: thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
end;
structure BNF_Def_Tactics : BNF_DEF_TACTICS =
@@ -65,14 +65,14 @@
rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm,
rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1;
-fun mk_rel_Gr_tac rel_O_Gr map_id map_cong map_wpull in_cong map_id' map_comp set_naturals
+fun mk_rel_Gr_tac rel_O_Grs map_id map_cong map_wpull in_cong map_id' map_comp set_naturals
{context = ctxt, prems = _} =
let
val n = length set_naturals;
in
if null set_naturals then
- Local_Defs.unfold_tac ctxt [rel_O_Gr] THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1
- else Local_Defs.unfold_tac ctxt [rel_O_Gr, @{thm Gr_def}] THEN
+ Local_Defs.unfold_tac ctxt rel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1
+ else Local_Defs.unfold_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
EVERY' [rtac equalityI, rtac subsetI,
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
@@ -112,20 +112,20 @@
rtac equalityI, rtac @{thm subset_UNIV}, rtac subsetI, rtac CollectI,
CONJ_WRAP' (K (rtac @{thm subset_UNIV})) (1 upto n), rtac refl] 1);
-fun mk_rel_mono_tac rel_O_Gr in_mono {context = ctxt, prems = _} =
- Local_Defs.unfold_tac ctxt [rel_O_Gr] THEN
+fun mk_rel_mono_tac rel_O_Grs in_mono {context = ctxt, prems = _} =
+ Local_Defs.unfold_tac ctxt rel_O_Grs THEN
EVERY' [rtac @{thm relcomp_mono}, rtac @{thm iffD2[OF converse_mono]},
rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac,
rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1;
-fun mk_rel_converse_le_tac rel_O_Gr rel_Id map_cong map_comp set_naturals
+fun mk_rel_converse_le_tac rel_O_Grs rel_Id map_cong map_comp set_naturals
{context = ctxt, prems = _} =
let
val n = length set_naturals;
in
if null set_naturals then
Local_Defs.unfold_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1
- else Local_Defs.unfold_tac ctxt [rel_O_Gr, @{thm Gr_def}] THEN
+ else Local_Defs.unfold_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
EVERY' [rtac @{thm subrelI},
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
@@ -143,7 +143,7 @@
EVERY' [rtac equalityI, rtac le_converse, rtac @{thm xt1(6)}, rtac @{thm converse_shift},
rtac le_converse, REPEAT_DETERM o stac @{thm converse_converse}, rtac subset_refl] 1;
-fun mk_rel_O_tac rel_O_Gr rel_Id map_cong map_wppull map_comp set_naturals
+fun mk_rel_O_tac rel_O_Grs rel_Id map_cong map_wppull map_comp set_naturals
{context = ctxt, prems = _} =
let
val n = length set_naturals;
@@ -152,7 +152,7 @@
rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_naturals;
in
if null set_naturals then Local_Defs.unfold_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1
- else Local_Defs.unfold_tac ctxt [rel_O_Gr, @{thm Gr_def}] THEN
+ else Local_Defs.unfold_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
EVERY' [rtac equalityI, rtac @{thm subrelI},
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
@@ -193,11 +193,11 @@
rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstO}, @{thm snd_sndO}])] 1
end;
-fun mk_in_rel_tac rel_O_Gr m {context = ctxt, prems = _} =
+fun mk_in_rel_tac rel_O_Grs m {context = ctxt, prems = _} =
let
val ls' = replicate (Int.max (1, m)) ();
in
- Local_Defs.unfold_tac ctxt (rel_O_Gr ::
+ Local_Defs.unfold_tac ctxt (rel_O_Grs @
@{thms Gr_def converse_unfold relcomp_unfold mem_Collect_eq prod.cases Pair_eq}) THEN
EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI,
rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl,
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Thu Sep 20 02:42:48 2012 +0200
@@ -26,35 +26,35 @@
open BNF_GFP_Util
open BNF_GFP_Tactics
-datatype wit_tree = Leaf of int | Node of (int * int * int list) * wit_tree list;
+datatype wit_tree = Wit_Leaf of int | Wit_Node of (int * int * int list) * wit_tree list;
fun mk_tree_args (I, T) (I', Ts) = (sort_distinct int_ord (I @ I'), T :: Ts);
fun finish Iss m seen i (nwit, I) =
let
val treess = map (fn j =>
- if j < m orelse member (op =) seen j then [([j], Leaf j)]
+ if j < m orelse member (op =) seen j then [([j], Wit_Leaf j)]
else
map_index (finish Iss m (insert (op =) j seen) j) (nth Iss (j - m))
|> flat
|> minimize_wits)
I;
in
- map (fn (I, t) => (I, Node ((i - m, nwit, filter (fn i => i < m) I), t)))
+ map (fn (I, t) => (I, Wit_Node ((i - m, nwit, filter (fn i => i < m) I), t)))
(fold_rev (map_product mk_tree_args) treess [([], [])])
|> minimize_wits
end;
-fun tree_to_fld_wit vars _ _ (Leaf j) = ([j], nth vars j)
- | tree_to_fld_wit vars flds witss (Node ((i, nwit, I), subtrees)) =
+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_coind_wits _ (Leaf _) = []
- | tree_to_coind_wits lwitss (Node ((i, nwit, I), subtrees)) =
+fun tree_to_coind_wits _ (Wit_Leaf _) = []
+ | tree_to_coind_wits lwitss (Wit_Node ((i, nwit, I), subtrees)) =
((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees;
-(*all bnfs have the same lives*)
+(*all BNFs have the same lives*)
fun bnf_gfp mixfixes resBs bs (resDs, Dss) bnfs lthy =
let
val timer = time (Timer.startRealTimer ());
@@ -62,11 +62,11 @@
val live = live_of_bnf (hd bnfs);
val n = length bnfs; (*active*)
val ks = 1 upto n;
- val m = live - n (*passive, if 0 don't generate a new bnf*);
+ val m = live - n (*passive, if 0 don't generate a new BNF*);
val ls = 1 upto m;
val b = Binding.name (mk_common_name bs);
- (* TODO: check if m, n etc are sane *)
+ (* TODO: check if m, n, etc., are sane *)
val deads = fold (union (op =)) Dss resDs;
val names_lthy = fold Variable.declare_typ deads lthy;
@@ -2671,7 +2671,7 @@
val rel_O_gr_tacs = replicate n (K (rtac refl 1));
- val tacss = map10 zip_goals map_id_tacs map_comp_tacs map_cong_tacs set_nat_tacss
+ 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) =
@@ -2889,8 +2889,7 @@
val in_rels = map in_rel_of_bnf bnfs;
val in_Jrels = map in_rel_of_bnf Jbnfs;
- val Jpred_defs =
- map (Drule.abs_def o (fn thm => thm RS @{thm eq_reflection}) o pred_def_of_bnf) Jbnfs;
+ val Jpred_defs = map pred_def_of_bnf Jbnfs;
val folded_map_simp_thms = map fold_maps map_simp_thms;
val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss;
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Thu Sep 20 02:42:48 2012 +0200
@@ -25,17 +25,17 @@
open BNF_LFP_Util
open BNF_LFP_Tactics
-(*all bnfs have the same lives*)
+(*all BNFs have the same lives*)
fun bnf_lfp mixfixes resBs bs (resDs, Dss) bnfs lthy =
let
val timer = time (Timer.startRealTimer ());
val live = live_of_bnf (hd bnfs);
val n = length bnfs; (*active*)
val ks = 1 upto n;
- val m = live - n; (*passive, if 0 don't generate a new bnf*)
+ val m = live - n; (*passive, if 0 don't generate a new BNF*)
val b = Binding.name (mk_common_name bs);
- (* TODO: check if m, n etc are sane *)
+ (* TODO: check if m, n, etc., are sane *)
val deads = fold (union (op =)) Dss resDs;
val names_lthy = fold Variable.declare_typ deads lthy;
@@ -1672,7 +1672,7 @@
val rel_O_gr_tacs = replicate n (K (rtac refl 1));
- val tacss = map10 zip_goals map_id_tacs map_comp_tacs map_cong_tacs set_nat_tacss
+ 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 =
@@ -1732,8 +1732,7 @@
val in_rels = map in_rel_of_bnf bnfs;
val in_Irels = map in_rel_of_bnf Ibnfs;
val pred_defs = map pred_def_of_bnf bnfs;
- val Ipred_defs =
- map (Drule.abs_def o (fn thm => thm RS @{thm eq_reflection}) o pred_def_of_bnf) Ibnfs;
+ val Ipred_defs = map pred_def_of_bnf Ibnfs;
val set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss;
val set_set_incl_thmsss = map (transpose o map (map fold_sets o tl)) Fset_set_thmsss;