# HG changeset patch # User blanchet # Date 1348101768 -7200 # Node ID ff0e540d875867de5f36df782c0611807a02102e # Parent e053519494d61c985bdfc37b2ffa6e7812114895 add rel as first-class citizen of BNF diff -r e053519494d6 -r ff0e540d8758 src/HOL/Codatatype/Basic_BNFs.thy --- a/src/HOL/Codatatype/Basic_BNFs.thy Thu Sep 20 02:42:48 2012 +0200 +++ b/src/HOL/Codatatype/Basic_BNFs.thy Thu Sep 20 02:42:48 2012 +0200 @@ -25,11 +25,12 @@ unfolding cinfinite_def Field_natLeq by (rule nat_infinite) bnf_def ID: "id :: ('a \ 'b) \ 'a \ 'b" ["\x. {x}"] "\_:: 'a. natLeq" ["id :: 'a \ 'a"] + "\x :: ('a \ 'b) set. x" apply auto apply (rule natLeq_card_order) apply (rule natLeq_cinfinite) apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]]) -apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on) +apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3] apply (rule ordLeq_transitive) apply (rule ordLeq_cexp1[of natLeq]) apply (rule Cinfinite_Cnotzero) @@ -47,12 +48,10 @@ apply (rule ordLeq_csum2) apply (rule Card_order_ctwo) apply (rule natLeq_Card_order) +apply (auto simp: Gr_def fun_eq_iff) done -lemma ID_pred[simp]: "ID_pred \ = \" -unfolding ID_pred_def ID_rel_def Gr_def fun_eq_iff by auto - -bnf_def DEADID: "id :: 'a \ 'a" [] "\_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"] +bnf_def DEADID: "id :: 'a \ 'a" [] "\_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"] Id apply (auto simp add: wpull_id) apply (rule card_order_csum) apply (rule natLeq_card_order) @@ -68,10 +67,9 @@ apply (rule ordLeq_csum2) apply (rule card_of_Card_order) apply (rule ctwo_Cnotzero) -by (rule card_of_Card_order) - -lemma DEADID_pred[simp]: "DEADID_pred = (op =)" -unfolding DEADID_pred_def DEADID.rel_Id by simp +apply (rule card_of_Card_order) +apply (auto simp: Id_def Gr_def fun_eq_iff) +done definition setl :: "'a + 'b \ 'a set" where "setl x = (case x of Inl z => {z} | _ => {})" @@ -81,7 +79,14 @@ lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def] -bnf_def sum_map [setl, setr] "\_::'a + 'b. natLeq" [Inl, Inr] +(*### RENAME TODO *) +definition sum_rel0 :: "('a \ 'b) set \ ('c \ 'd) set \ (('a + 'c) \ ('b + 'd)) set" where +"sum_rel0 R S = + {x. case x of (Inl a, Inl c) \ (a, c) \ R + | (Inr b, Inr d) \ (b, d) \ S + | _ \ False}" + +bnf_def sum_map [setl, setr] "\_::'a + 'b. natLeq" [Inl, Inr] sum_rel0 proof - show "sum_map id id = id" by (rule sum_map.id) next @@ -190,15 +195,15 @@ thus "\B1 B2. B1 \ ?in1 \ B2 \ ?in2 \ ?mapf1 B1 = ?mapf2 B2 \ (\A \ ?in. ?mapp1 A = B1 \ ?mapp2 A = B2)" by fastforce qed +next + fix R S + show "sum_rel0 R S = + (Gr {x. setl x \ R \ setr x \ S} (sum_map fst fst))\ O + Gr {x. setl x \ R \ setr x \ S} (sum_map snd snd)" + unfolding setl_def setr_def sum_rel0_def Gr_def relcomp_unfold converse_unfold + by (fastforce split: sum.splits) qed (auto simp: sum_set_defs) -lemma sum_pred[simp]: - "sum_pred \ \ x y = - (case x of Inl a1 \ (case y of Inl a2 \ \ a1 a2 | Inr _ \ False) - | Inr b1 \ (case y of Inl _ \ False | Inr b2 \ \ b1 b2))" -unfolding setl_def setr_def sum_pred_def sum_rel_def Gr_def relcomp_unfold converse_unfold -by (fastforce split: sum.splits)+ - lemma singleton_ordLeq_ctwo_natLeq: "|{x}| \o ctwo *c natLeq" apply (rule ordLeq_transitive) apply (rule ordLeq_cprod2) @@ -217,7 +222,10 @@ lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def] -bnf_def map_pair [fsts, snds] "\_::'a \ 'b. ctwo *c natLeq" [Pair] +definition prod_rel0 :: "('a \ 'b) set \ ('c \ 'd) set \ (('a \ 'c) \ 'b \ 'd) set" where +"prod_rel0 R S = {((a, c), b, d) | a b c d. (a, b) \ R \ (c, d) \ S}" + +bnf_def map_pair [fsts, snds] "\_::'a \ 'b. ctwo *c natLeq" [Pair] prod_rel0 proof (unfold prod_set_defs) show "map_pair id id = id" by (rule map_pair.id) next @@ -292,12 +300,15 @@ {x. {fst x} \ B11 \ {snd x} \ B12} {x. {fst x} \ B21 \ {snd x} \ B22} (map_pair f11 f12) (map_pair f21 f22) (map_pair p11 p12) (map_pair p21 p22)" unfolding wpull_def by simp fast +next + fix R S + show "prod_rel0 R S = + (Gr {x. {fst x} \ R \ {snd x} \ S} (map_pair fst fst))\ O + Gr {x. {fst x} \ R \ {snd x} \ S} (map_pair snd snd)" + unfolding prod_set_defs prod_rel0_def Gr_def relcomp_unfold converse_unfold + by auto qed simp+ -lemma prod_pred[simp]: -"prod_pred \ \ p1 p2 = (case p1 of (a1, b1) \ case p2 of (a2, b2) \ (\ a1 a2 \ \ b1 b2))" -unfolding prod_set_defs prod_pred_def prod_rel_def Gr_def relcomp_unfold converse_unfold by auto - (* Categorical version of pullback: *) lemma wpull_cat: assumes p: "wpull A B1 B2 f1 f2 p1 p2" @@ -334,8 +345,11 @@ ultimately show ?thesis using card_of_ordLeq by fast qed -bnf_def "op \" [range] "\_:: 'a \ 'b. natLeq +c |UNIV :: 'a set|" - ["%c x::'b::type. c::'a::type"] +definition fun_rel0 :: "('a \ 'b) set \ (('c \ 'a) \ ('c \ 'b)) set" where +"fun_rel0 R = {(f, g) | f g. \x. (f x, g x) \ R}" + +bnf_def "op \" [range] "\_:: 'a \ 'b. natLeq +c |UNIV :: 'a set|" ["%c x::'b::type. c::'a::type"] + fun_rel0 proof fix f show "id \ f = id f" by simp next @@ -393,10 +407,11 @@ show "\h \ {h. range h \ A}. p1 \ h = g1 \ p2 \ h = g2" using wpull_cat[OF p c r] by simp metis qed +next + fix R + show "fun_rel0 R = (Gr {x. range x \ R} (op \ fst))\ O Gr {x. range x \ R} (op \ snd)" + unfolding fun_rel0_def Gr_def relcomp_unfold converse_unfold + by (auto intro!: exI dest!: in_mono) qed auto -lemma fun_pred[simp]: "fun_pred \ f g = (\x. \ (f x) (g x))" -unfolding fun_rel_def fun_pred_def Gr_def relcomp_unfold converse_unfold -by (auto intro!: exI dest!: in_mono) - end diff -r e053519494d6 -r ff0e540d8758 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 @@ -89,12 +89,12 @@ val bnf_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) -> ({prems: thm list, context: Proof.context} -> tactic) list -> ({prems: thm list, context: Proof.context} -> tactic) -> typ list option -> - (((binding * term) * term list) * term) * term list -> local_theory -> + ((((binding * term) * term list) * term) * term list) * term -> local_theory -> BNF * local_theory val filter_refl: thm list -> thm list - val bnf_def_cmd: (((binding * string) * string list) * string) * string list -> local_theory -> - Proof.state + val bnf_def_cmd: ((((binding * string) * string list) * string) * string list) * string -> + local_theory -> Proof.state end; structure BNF_Def : BNF_DEF = @@ -112,12 +112,13 @@ bd_cinfinite: thm, set_bd: thm list, in_bd: thm, - map_wpull: thm + map_wpull: thm, + rel_O_Gr: thm }; -fun mk_axioms' ((((((((id, comp), cong), nat), c_o), cinf), set_bd), in_bd), wpull) = +fun mk_axioms' (((((((((id, comp), cong), nat), c_o), cinf), set_bd), in_bd), wpull), rel) = {map_id = id, map_comp = comp, map_cong = cong, set_natural = nat, bd_card_order = c_o, - bd_cinfinite = cinf, set_bd = set_bd, in_bd = in_bd, map_wpull = wpull}; + bd_cinfinite = cinf, set_bd = set_bd, in_bd = in_bd, map_wpull = wpull, rel_O_Gr = rel}; fun dest_cons [] = raise Empty | dest_cons (x :: xs) = (x, xs); @@ -132,18 +133,19 @@ ||>> dest_cons ||>> chop n ||>> dest_cons + ||>> dest_cons ||> the_single |> mk_axioms'; -fun dest_axioms {map_id, map_comp, map_cong, set_natural, - bd_card_order, bd_cinfinite, set_bd, in_bd, map_wpull} = +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]; + 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, - bd_card_order = bd_card_order, bd_cinfinite = bd_cinfinite, - set_bd = set_bd, in_bd = in_bd, map_wpull = map_wpull} = + bd_card_order = bd_card_order, bd_cinfinite = bd_cinfinite, set_bd = set_bd, in_bd = in_bd, + map_wpull = map_wpull, rel_O_Gr} = {map_id = f map_id, map_comp = f map_comp, map_cong = f map_cong, @@ -152,7 +154,8 @@ bd_cinfinite = f bd_cinfinite, set_bd = map f set_bd, in_bd = f in_bd, - map_wpull = f map_wpull}; + map_wpull = f map_wpull, + rel_O_Gr = f rel_O_Gr}; val morph_axioms = map_axioms o Morphism.thm; @@ -187,13 +190,12 @@ rel_Gr: thm lazy, rel_converse: thm lazy, rel_O: thm lazy, - rel_O_Gr: thm, set_natural': thm lazy list }; fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_natural in_cong in_mono in_rel map_comp' map_id' map_wppull - rel_cong rel_mono rel_Id rel_Gr rel_converse rel_O rel_O_Gr set_natural' = { + rel_cong rel_mono rel_Id rel_Gr rel_converse rel_O set_natural' = { bd_Card_order = bd_Card_order, bd_Cinfinite = bd_Cinfinite, bd_Cnotzero = bd_Cnotzero, @@ -210,7 +212,6 @@ rel_Gr = rel_Gr, rel_converse = rel_converse, rel_O = rel_O, - rel_O_Gr = rel_O_Gr, set_natural' = set_natural'}; fun map_facts f { @@ -230,7 +231,6 @@ rel_Gr, rel_converse, rel_O, - rel_O_Gr, set_natural'} = {bd_Card_order = f bd_Card_order, bd_Cinfinite = f bd_Cinfinite, @@ -248,7 +248,6 @@ rel_Gr = Lazy.map f rel_Gr, rel_converse = Lazy.map f rel_converse, rel_O = Lazy.map f rel_O, - rel_O_Gr = f rel_O_Gr, set_natural' = map (Lazy.map f) set_natural'}; val morph_facts = map_facts o Morphism.thm; @@ -369,7 +368,7 @@ val rel_Gr_of_bnf = Lazy.force o #rel_Gr o #facts o rep_bnf; val rel_converse_of_bnf = Lazy.force o #rel_converse o #facts o rep_bnf; val rel_O_of_bnf = Lazy.force o #rel_O o #facts o rep_bnf; -val rel_O_Gr_of_bnf = #rel_O_Gr o #facts o rep_bnf; +val rel_O_Gr_of_bnf = #rel_O_Gr o #axioms o rep_bnf; val set_bd_of_bnf = #set_bd o #axioms o rep_bnf; val set_defs_of_bnf = #set_defs o #defs o rep_bnf; val set_natural_of_bnf = #set_natural o #axioms o rep_bnf; @@ -432,7 +431,8 @@ val tyenv = Sign.typ_match thy (fastype_of rel, Library.foldr (op -->) (instTs, mk_relT (instA, instB))) Vartab.empty; - in Envir.subst_term (tyenv, Vartab.empty) rel end; + in Envir.subst_term (tyenv, Vartab.empty) rel end + handle Type.TYPE_MATCH => error "Bad relator"; fun normalize_pred ctxt instTs instA instB pred = let @@ -440,7 +440,8 @@ val tyenv = Sign.typ_match thy (fastype_of pred, Library.foldr (op -->) (instTs, instA --> instB --> HOLogic.boolT)) Vartab.empty; - in Envir.subst_term (tyenv, Vartab.empty) pred end; + in Envir.subst_term (tyenv, Vartab.empty) pred end + handle Type.TYPE_MATCH => error "Bad predicator"; fun normalize_wit insts CA As wit = let @@ -535,7 +536,7 @@ (* Define new BNFs *) fun prepare_def const_policy mk_fact_policy qualify prep_term Ds_opt - ((((raw_b, raw_map), raw_sets), raw_bd_Abs), raw_wits) no_defs_lthy = + (((((raw_b, raw_map), raw_sets), raw_bd_Abs), raw_wits), raw_rel) no_defs_lthy = let val fact_policy = mk_fact_policy no_defs_lthy; val b = qualify raw_b; @@ -548,6 +549,7 @@ Abs (_, T, t) => (T, t) | _ => error "Bad bound constant"); val wit_rhss = map (prep_term no_defs_lthy) raw_wits; + val rel_rhs = prep_term no_defs_lthy raw_rel; fun err T = error ("Trying to register the type " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^ @@ -573,7 +575,9 @@ val bs = if nwits = 1 then [fn () => Binding.suffix_name ("_" ^ witN) b] else map (fn i => fn () => Binding.suffix_name ("_" ^ mk_witN i) b) (1 upto nwits); in map2 pair bs wit_rhss end; + val rel_bind_def = (fn () => Binding.suffix_name ("_" ^ relN) b, rel_rhs); + (* TODO: ### Kill "needed_for_extra_facts" *) fun maybe_define needed_for_extra_facts (b, rhs) lthy = let val inline = @@ -594,15 +598,17 @@ end; fun maybe_restore lthy0 lthy = lthy |> not (pointer_eq (lthy0, lthy)) ? Local_Theory.restore; - val (((((bnf_map_term, raw_map_def), + val ((((((bnf_map_term, raw_map_def), (bnf_set_terms, raw_set_defs)), (bnf_bd_term, raw_bd_def)), - (bnf_wit_terms, raw_wit_defs)), (lthy', lthy)) = + (bnf_wit_terms, raw_wit_defs)), + (bnf_rel_term, raw_rel_def)), (lthy', lthy)) = no_defs_lthy |> maybe_define false map_bind_def ||>> apfst split_list o fold_map (maybe_define false) set_binds_defs ||>> maybe_define false bd_bind_def ||>> apfst split_list o fold_map (maybe_define false) wit_binds_defs + ||>> maybe_define true(*###*) rel_bind_def ||> `(maybe_restore no_defs_lthy); (*transforms defined frees into consts (and more)*) @@ -612,8 +618,10 @@ val bnf_set_defs = map (Morphism.thm phi) raw_set_defs; val bnf_bd_def = Morphism.thm phi raw_bd_def; val bnf_wit_defs = map (Morphism.thm phi) raw_wit_defs; + val bnf_rel_def = Morphism.thm phi raw_rel_def; - val one_step_defs = filter_refl (bnf_map_def :: bnf_bd_def :: bnf_set_defs @ bnf_wit_defs); + val one_step_defs = + filter_refl (bnf_map_def :: bnf_bd_def :: bnf_set_defs @ bnf_wit_defs @ [bnf_rel_def]); val _ = case map_filter (try dest_Free) (bnf_map_term :: bnf_set_terms @ [bnf_bd_term] @ bnf_wit_terms) of @@ -638,6 +646,7 @@ val bnf_bd = Term.subst_TVars (Term.add_tvar_namesT bdT [] ~~ CA_params) (Morphism.term phi bnf_bd_term); val bnf_wits = map (normalize_wit CA_params CA alphas o Morphism.term phi) bnf_wit_terms; + val bnf_rel = Morphism.term phi bnf_rel_term; (*TODO: assert Ds = (TVars of bnf_map) \ (alphas @ betas) as sets*) val deads = (case Ds_opt of @@ -667,10 +676,10 @@ fun mk_bnf_map As' Bs' = Term.subst_atomic_types ((deads ~~ Ds) @ (alphas ~~ As') @ (betas ~~ Bs')) bnf_map; - fun mk_bnf_t As' t = - Term.subst_atomic_types ((deads ~~ Ds) @ (alphas ~~ As')) t; - fun mk_bnf_T As' T = - Term.typ_subst_atomic ((deads ~~ Ds) @ (alphas ~~ As')) T; + fun mk_bnf_t As' = Term.subst_atomic_types ((deads ~~ Ds) @ (alphas ~~ As')); + fun mk_bnf_T As' = Term.typ_subst_atomic ((deads ~~ Ds) @ (alphas ~~ As')); + + fun mk_bnf_rel setRTs CA' CB' = normalize_rel lthy setRTs CA' CB' bnf_rel; val (setRTs, RTs) = map_split (`HOLogic.mk_setT o HOLogic.mk_prodT) (As' ~~ Bs'); val setRTsAsCs = map (HOLogic.mk_setT o HOLogic.mk_prodT) (As' ~~ Cs); @@ -679,6 +688,11 @@ val self_setRTs = map (HOLogic.mk_setT o HOLogic.mk_prodT) (As' ~~ As'); val QTs = map2 (fn T => fn U => T --> U --> HOLogic.boolT) As' Bs'; + val CA' = mk_bnf_T As' CA; + val CB' = mk_bnf_T Bs' CA; + val CC' = mk_bnf_T Cs CA; + val CRs' = mk_bnf_T RTs CA; + val bnf_map_AsAs = mk_bnf_map As' As'; val bnf_map_AsBs = mk_bnf_map As' Bs'; val bnf_map_AsCs = mk_bnf_map As' Cs; @@ -687,14 +701,11 @@ val bnf_sets_Bs = map (mk_bnf_t Bs') bnf_sets; val bnf_bd_As = mk_bnf_t As' bnf_bd; val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits; - val CA' = mk_bnf_T As' CA; - val CB' = mk_bnf_T Bs' CA; - val CC' = mk_bnf_T Cs CA; - val CRs' = mk_bnf_T RTs CA; + val relAsBs = mk_bnf_rel setRTs CA' CB'; val ((((((((((((((((((((((((fs, fs_copy), gs), hs), (x, x')), (y, y')), (z, z')), zs), As), - As_copy), Xs), B1s), B2s), f1s), f2s), e1s), e2s), p1s), p2s), bs), - (Rs, Rs')), Rs_copy), Ss), (Qs, Qs')), _) = lthy' + As_copy), Xs), B1s), B2s), f1s), f2s), e1s), e2s), p1s), p2s), bs), Rs), Rs_copy), Ss), + (Qs, Qs')), _) = lthy' |> mk_Frees "f" (map2 (curry (op -->)) As' Bs') ||>> mk_Frees "f" (map2 (curry (op -->)) As' Bs') ||>> mk_Frees "g" (map2 (curry (op -->)) Bs' Cs) @@ -715,7 +726,7 @@ ||>> mk_Frees "p1" (map2 (curry (op -->)) domTs B1Ts) ||>> mk_Frees "p2" (map2 (curry (op -->)) domTs B2Ts) ||>> mk_Frees "b" As' - ||>> mk_Frees' "R" setRTs + ||>> mk_Frees "R" setRTs ||>> mk_Frees "R" setRTs ||>> mk_Frees "S" setRTsBsCs ||>> mk_Frees' "Q" QTs; @@ -812,10 +823,21 @@ (Logic.list_implies (prems, HOLogic.mk_Trueprop map_wpull)) end; + val goal_rel_O_Gr = + let + val map1 = Term.list_comb (mk_bnf_map RTs As', map fst_const RTs); + val map2 = Term.list_comb (mk_bnf_map RTs Bs', map snd_const RTs); + val bnf_in = mk_in Rs (map (mk_bnf_t RTs) bnf_sets) CRs'; + (*Gr (in R1 .. Rn) (map fst .. fst)^-1 O Gr (in R1 .. Rn) (map snd .. snd)*) + val rhs = mk_rel_comp (mk_converse (mk_Gr bnf_in map1), mk_Gr bnf_in map2); + in + fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (relAsBs, Rs), rhs)) + end; + val goals = [goal_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_in_bd, goal_map_wpull, goal_rel_O_Gr]; fun mk_wit_goals (I, wit) = let @@ -900,40 +922,7 @@ val set_natural' = map (fn thm => mk_lazy (fn () => mk_set_natural' thm)) (#set_natural axioms); - (* relator *) - - (*%R1 .. Rn. Gr (in R1 .. Rn) (map fst .. fst)^-1 O Gr (in R1 .. Rn) (map snd .. snd)*) - val rel_rhs = - let - val map1 = Term.list_comb (mk_bnf_map RTs As', map fst_const RTs); - val map2 = Term.list_comb (mk_bnf_map RTs Bs', map snd_const RTs); - val bnf_in = mk_in Rs (map (mk_bnf_t RTs) bnf_sets) CRs'; - in - fold_rev Term.absfree Rs' - (mk_rel_comp (mk_converse (mk_Gr bnf_in map1), mk_Gr bnf_in map2)) - end; - val rel_bind_def = (fn () => Binding.suffix_name ("_" ^ relN) b, rel_rhs); - - val ((bnf_rel_term, raw_rel_def), (lthy, lthy_old)) = - lthy - |> maybe_define true rel_bind_def - ||> `(maybe_restore lthy); - - (*transforms defined frees into consts*) - val phi = Proof_Context.export_morphism lthy_old lthy; - val bnf_rel = Morphism.term phi bnf_rel_term; - - fun mk_bnf_rel setRTs CA' CB' = normalize_rel lthy setRTs CA' CB' bnf_rel; - - val relAsBs = mk_bnf_rel setRTs CA' CB'; - val bnf_rel_def = Morphism.thm phi raw_rel_def; - - val rel_O_Gr = Morphism.thm phi raw_rel_def; (*###*) - val rel_O_Gr_unabs = - if fact_policy <> Derive_Some_Facts then - mk_unabs_def live (rel_O_Gr RS meta_eq_to_obj_eq) - else - no_fact; + (* predicator *) val pred_rhs = fold absfree (y' :: x' :: rev Qs') (HOLogic.mk_mem (HOLogic.mk_prod (x, y), Term.list_comb (relAsBs, map3 (fn Q => fn T => fn U => @@ -996,6 +985,8 @@ |> Thm.close_derivation end; + val rel_O_Gr = #rel_O_Gr axioms; + val map_wppull = mk_lazy mk_map_wppull; fun mk_rel_Gr () = @@ -1111,7 +1102,7 @@ val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_natural in_cong in_mono in_rel map_comp' map_id' map_wppull - rel_cong rel_mono rel_Id rel_Gr rel_converse rel_O rel_O_Gr_unabs set_natural'; + rel_cong rel_mono rel_Id rel_Gr rel_converse rel_O set_natural'; val wits = map2 mk_witness bnf_wits wit_thms; @@ -1156,12 +1147,12 @@ let val notes = [(map_congN, [#map_cong axioms]), + (rel_O_GrN, [rel_O_Gr]), (rel_IdN, [Lazy.force (#rel_Id facts)]), (rel_GrN, [Lazy.force (#rel_Gr facts)]), (rel_converseN, [Lazy.force (#rel_converse facts)]), (rel_monoN, [Lazy.force (#rel_mono facts)]), (rel_ON, [Lazy.force (#rel_O facts)]), - (rel_O_GrN, [#rel_O_Gr facts]), (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))] @@ -1238,6 +1229,6 @@ Outer_Syntax.local_theory_to_proof @{command_spec "bnf_def"} "define a BNF for an existing type" ((parse_opt_binding_colon -- Parse.term -- (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Parse.term -- - (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"})) >> bnf_def_cmd); + (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Parse.term) >> bnf_def_cmd); end;