--- a/src/HOL/BNF/Tools/bnf_def.ML Thu Aug 29 18:31:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML Thu Aug 29 18:44:03 2013 +0200
@@ -55,8 +55,8 @@
val map_cong0_of_bnf: bnf -> thm
val map_cong_of_bnf: bnf -> thm
val map_def_of_bnf: bnf -> thm
+ val map_id0_of_bnf: bnf -> thm
val map_id'_of_bnf: bnf -> thm
- val map_id_of_bnf: bnf -> thm
val map_transfer_of_bnf: bnf -> thm
val map_wppull_of_bnf: bnf -> thm
val map_wpull_of_bnf: bnf -> thm
@@ -113,7 +113,7 @@
val fundef_cong_attrs = @{attributes [fundef_cong]};
type axioms = {
- map_id: thm,
+ map_id0: thm,
map_comp: thm,
map_cong0: thm,
set_map: thm list,
@@ -125,7 +125,7 @@
};
fun mk_axioms' ((((((((id, comp), cong), nat), c_o), cinf), set_bd), wpull), rel) =
- {map_id = id, map_comp = comp, map_cong0 = cong, set_map = nat, bd_card_order = c_o,
+ {map_id0 = id, map_comp = comp, map_cong0 = cong, set_map = nat, bd_card_order = c_o,
bd_cinfinite = cinf, set_bd = set_bd, map_wpull = wpull, rel_OO_Grp = rel};
fun dest_cons [] = raise List.Empty
@@ -147,14 +147,14 @@
fun zip_axioms mid mcomp mcong snat bdco bdinf sbd wpull rel =
[mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [wpull, rel];
-fun dest_axioms {map_id, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
+fun dest_axioms {map_id0, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
map_wpull, rel_OO_Grp} =
- zip_axioms map_id map_comp map_cong0 set_map bd_card_order bd_cinfinite set_bd map_wpull
+ zip_axioms map_id0 map_comp map_cong0 set_map bd_card_order bd_cinfinite set_bd map_wpull
rel_OO_Grp;
-fun map_axioms f {map_id, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
+fun map_axioms f {map_id0, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
map_wpull, rel_OO_Grp} =
- {map_id = f map_id,
+ {map_id0 = f map_id0,
map_comp = f map_comp,
map_cong0 = f map_cong0,
set_map = map f set_map,
@@ -380,7 +380,7 @@
val in_mono_of_bnf = Lazy.force o #in_mono o #facts o rep_bnf;
val in_rel_of_bnf = Lazy.force o #in_rel o #facts o rep_bnf;
val map_def_of_bnf = #map_def o #defs o rep_bnf;
-val map_id_of_bnf = #map_id o #axioms o rep_bnf;
+val map_id0_of_bnf = #map_id0 o #axioms o rep_bnf;
val map_id'_of_bnf = Lazy.force o #map_id' o #facts o rep_bnf;
val map_comp_of_bnf = #map_comp o #axioms o rep_bnf;
val map_comp'_of_bnf = Lazy.force o #map_comp' o #facts o rep_bnf;
@@ -508,7 +508,7 @@
val in_bdN = "in_bd";
val in_monoN = "in_mono";
val in_relN = "in_rel";
-val map_idN = "map_id";
+val map_id0N = "map_id0";
val map_id'N = "map_id'";
val map_compN = "map_comp";
val map_comp'N = "map_comp'";
@@ -559,7 +559,7 @@
(in_monoN, [Lazy.force (#in_mono facts)]),
(in_relN, [Lazy.force (#in_rel facts)]),
(map_compN, [#map_comp axioms]),
- (map_idN, [#map_id axioms]),
+ (map_id0N, [#map_id0 axioms]),
(map_transferN, [Lazy.force (#map_transfer facts)]),
(map_wpullN, [#map_wpull axioms]),
(rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]),
@@ -845,7 +845,7 @@
| defs => Proof_Display.print_consts true lthy_old (K false)
(map (dest_Free o fst o Logic.dest_equals o prop_of) defs);
- val map_id_goal =
+ val map_id0_goal =
let val bnf_map_app_id = Term.list_comb (bnf_map_AsAs, map HOLogic.id_const As') in
mk_Trueprop_eq (bnf_map_app_id, HOLogic.id_const CA')
end;
@@ -922,8 +922,8 @@
val rel_OO_Grp_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (rel, Rs), OO_Grp));
- val goals = zip_axioms map_id_goal map_comp_goal map_cong0_goal set_maps_goal card_order_bd_goal
- cinfinite_bd_goal set_bds_goal map_wpull_goal rel_OO_Grp_goal;
+ val goals = zip_axioms map_id0_goal map_comp_goal map_cong0_goal set_maps_goal
+ card_order_bd_goal cinfinite_bd_goal set_bds_goal map_wpull_goal rel_OO_Grp_goal;
fun mk_wit_goals (I, wit) =
let
@@ -1000,7 +1000,7 @@
val in_cong = Lazy.lazy mk_in_cong;
- val map_id' = Lazy.lazy (fn () => mk_map_id' (#map_id axioms));
+ val map_id' = Lazy.lazy (fn () => mk_map_id' (#map_id0 axioms));
val map_comp' = Lazy.lazy (fn () => mk_map_comp' (#map_comp axioms));
fun mk_map_cong () =
@@ -1086,7 +1086,7 @@
(Logic.list_implies (prems, HOLogic.mk_Trueprop concl))
in
Goal.prove_sorry lthy [] [] goal
- (fn _ => mk_map_wppull_tac (#map_id axioms) (#map_cong0 axioms)
+ (fn _ => mk_map_wppull_tac (#map_id0 axioms) (#map_cong0 axioms)
(#map_wpull axioms) (Lazy.force map_comp') (map Lazy.force set_map'))
|> Thm.close_derivation
end;
@@ -1102,7 +1102,7 @@
val goal = fold_rev Logic.all (As @ fs) (mk_Trueprop_eq (lhs, rhs));
in
Goal.prove_sorry lthy [] [] goal
- (mk_rel_Grp_tac rel_OO_Grps (#map_id axioms) (#map_cong0 axioms) (Lazy.force map_id')
+ (mk_rel_Grp_tac rel_OO_Grps (#map_id0 axioms) (#map_cong0 axioms) (Lazy.force map_id')
(Lazy.force map_comp') (map Lazy.force set_map'))
|> Thm.close_derivation
end;
@@ -1142,7 +1142,7 @@
Goal.prove_sorry lthy [] []
(mk_Trueprop_eq (Term.list_comb (relAsAs, map HOLogic.eq_const As'),
HOLogic.eq_const CA'))
- (K (mk_rel_eq_tac live (Lazy.force rel_Grp) (Lazy.force rel_cong) (#map_id axioms)))
+ (K (mk_rel_eq_tac live (Lazy.force rel_Grp) (Lazy.force rel_cong) (#map_id0 axioms)))
|> Thm.close_derivation;
val rel_eq = Lazy.lazy mk_rel_eq;