# HG changeset patch # User blanchet # Date 1348101768 -7200 # Node ID 4dd451a075ce41aca0d8af4b429952f7478f39f3 # Parent 3f8e2b5249ec3740b1c21631f841f6824d92e6f9 fixed infinite loop with trivial rel_O_Gr + tuning diff -r 3f8e2b5249ec -r 4dd451a075ce src/HOL/Codatatype/Tools/bnf_comp.ML --- 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)); diff -r 3f8e2b5249ec -r 4dd451a075ce src/HOL/Codatatype/Tools/bnf_def.ML --- 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; diff -r 3f8e2b5249ec -r 4dd451a075ce src/HOL/Codatatype/Tools/bnf_def_tactics.ML --- 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, diff -r 3f8e2b5249ec -r 4dd451a075ce src/HOL/Codatatype/Tools/bnf_gfp.ML --- 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; diff -r 3f8e2b5249ec -r 4dd451a075ce src/HOL/Codatatype/Tools/bnf_lfp.ML --- 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;