--- 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;