--- a/src/Doc/Datatypes/Datatypes.thy Thu Aug 29 19:20:35 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Thu Aug 29 19:22:48 2013 +0200
@@ -1128,6 +1128,9 @@
(for datatype\_compat and prim(co)rec)
* no way to register same type as both data- and codatatype?
+
+* no recursion through unused arguments (unlike with the old package)
+
*}
--- a/src/HOL/BNF/More_BNFs.thy Thu Aug 29 19:20:35 2013 +0200
+++ b/src/HOL/BNF/More_BNFs.thy Thu Aug 29 19:22:48 2013 +0200
@@ -376,7 +376,7 @@
qed
qed
-lemma mmap_id: "mmap id = id"
+lemma mmap_id0: "mmap id = id"
proof (intro ext multiset_eqI)
fix f a show "count (mmap id f) a = count (id f) a"
proof (cases "count f a = 0")
@@ -872,7 +872,7 @@
(auto intro!: ordLess_imp_ordLeq simp: finite_iff_ordLess_natLeq[symmetric] multiset_def)
bnf mmap [set_of] "\<lambda>_::'a multiset. natLeq" ["{#}"]
-by (auto simp add: mmap_id mmap_comp set_of_mmap natLeq_card_order natLeq_cinfinite set_of_bd
+by (auto simp add: mmap_id0 mmap_comp set_of_mmap natLeq_card_order natLeq_cinfinite set_of_bd
intro: mmap_cong wpull_mmap)
inductive multiset_rel' where
--- a/src/HOL/BNF/Tools/bnf_comp.ML Thu Aug 29 19:20:35 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML Thu Aug 29 19:22:48 2013 +0200
@@ -24,8 +24,8 @@
val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list ->
(''a list list -> ''a list) -> BNF_Def.bnf list -> unfold_set -> Proof.context ->
(int list list * ''a list) * (BNF_Def.bnf list * (unfold_set * Proof.context))
- val seal_bnf: unfold_set -> binding -> typ list -> BNF_Def.bnf -> Proof.context ->
- (BNF_Def.bnf * typ list) * local_theory
+ val seal_bnf: (binding -> binding) -> unfold_set -> binding -> typ list -> BNF_Def.bnf ->
+ Proof.context -> (BNF_Def.bnf * typ list) * local_theory
end;
structure BNF_Comp : BNF_COMP =
@@ -149,9 +149,9 @@
(*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*)
val bd = Term.absdummy CCA (mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd);
- fun map_id_tac _ =
- mk_comp_map_id_tac (map_id_of_bnf outer) (map_cong0_of_bnf outer)
- (map map_id_of_bnf inners);
+ fun map_id0_tac _ =
+ mk_comp_map_id0_tac (map_id0_of_bnf outer) (map_cong0_of_bnf outer)
+ (map map_id0_of_bnf inners);
fun map_comp_tac _ =
mk_comp_map_comp_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer)
@@ -233,7 +233,7 @@
rtac thm 1
end;
- val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
+ val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac;
val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
@@ -300,7 +300,7 @@
val bd = mk_cprod
(Library.foldr1 (uncurry mk_csum) (map (mk_card_of o HOLogic.mk_UNIV) killedAs)) bnf_bd;
- fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
+ fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
fun map_comp_tac {context = ctxt, prems = _} =
unfold_thms_tac ctxt ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
rtac refl 1;
@@ -339,7 +339,7 @@
rtac thm 1
end;
- val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
+ val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac;
val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
@@ -390,7 +390,7 @@
val bd = mk_bd_of_bnf Ds As bnf;
- fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
+ fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
fun map_comp_tac {context = ctxt, prems = _} =
unfold_thms_tac ctxt ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
rtac refl 1;
@@ -424,7 +424,7 @@
fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm;
- val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
+ val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac;
val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -434,7 +434,6 @@
val (bnf', lthy') =
bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty
[] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
-
in
(bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
end;
@@ -475,7 +474,7 @@
val bd = mk_bd_of_bnf Ds As bnf;
- fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
+ fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
fun map_comp_tac _ = rtac (map_comp_of_bnf bnf) 1;
fun map_cong0_tac {context = ctxt, prems = _} =
rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
@@ -498,7 +497,7 @@
fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm;
- val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
+ val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac;
val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -571,7 +570,7 @@
(* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *)
-fun seal_bnf (unfold_set : unfold_set) b Ds bnf lthy =
+fun seal_bnf qualify (unfold_set : unfold_set) b Ds bnf lthy =
let
val live = live_of_bnf bnf;
val nwits = nwits_of_bnf bnf;
@@ -604,7 +603,7 @@
(*bd should only depend on dead type variables!*)
val bd_repT = fst (dest_relT (fastype_of bnf_bd));
- val bdT_bind = Binding.suffix_name ("_" ^ bdTN) b;
+ val bdT_bind = qualify (Binding.suffix_name ("_" ^ bdTN) b);
val params = fold Term.add_tfreesT Ds [];
val deads = map TFree params;
@@ -631,7 +630,7 @@
(rtac (unfold_all thm) THEN'
SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1;
- val tacs = zip_axioms (mk_tac (map_id_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf))
+ val tacs = zip_axioms (mk_tac (map_id0_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf))
(mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_map_of_bnf bnf))
(K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds)
(mk_tac (map_wpull_of_bnf bnf))
@@ -641,9 +640,10 @@
fun wit_tac _ = mk_simple_wit_tac (map unfold_all (wit_thms_of_bnf bnf));
- val (bnf', lthy') = bnf_def Hardly_Inline (user_policy Dont_Note) I tacs wit_tac (SOME deads)
- Binding.empty Binding.empty []
- (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
+ val (bnf', lthy') =
+ bnf_def Hardly_Inline (user_policy Dont_Note) qualify tacs wit_tac (SOME deads)
+ Binding.empty Binding.empty []
+ (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
in
((bnf', deads), lthy')
end;
--- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML Thu Aug 29 19:20:35 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML Thu Aug 29 19:22:48 2013 +0200
@@ -13,7 +13,7 @@
val mk_comp_in_alt_tac: Proof.context -> thm list -> tactic
val mk_comp_map_comp_tac: thm -> thm -> thm list -> tactic
val mk_comp_map_cong0_tac: thm list -> thm -> thm list -> tactic
- val mk_comp_map_id_tac: thm -> thm -> thm list -> tactic
+ val mk_comp_map_id0_tac: thm -> thm -> thm list -> tactic
val mk_comp_set_alt_tac: Proof.context -> thm -> tactic
val mk_comp_set_bd_tac: Proof.context -> thm -> thm list -> tactic
val mk_comp_set_map_tac: thm -> thm -> thm -> thm list -> tactic
@@ -58,9 +58,9 @@
unfold_thms_tac ctxt [collect_set_map RS sym] THEN
rtac refl 1;
-fun mk_comp_map_id_tac Gmap_id Gmap_cong0 map_ids =
+fun mk_comp_map_id0_tac Gmap_id0 Gmap_cong0 map_id0s =
EVERY' ([rtac ext, rtac (Gmap_cong0 RS trans)] @
- map (fn thm => rtac (thm RS fun_cong)) map_ids @ [rtac (Gmap_id RS fun_cong)]) 1;
+ map (fn thm => rtac (thm RS fun_cong)) map_id0s @ [rtac (Gmap_id0 RS fun_cong)]) 1;
fun mk_comp_map_comp_tac Gmap_comp Gmap_cong0 map_comps =
EVERY' ([rtac ext, rtac sym, rtac trans_o_apply,
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Thu Aug 29 19:20:35 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Thu Aug 29 19:22:48 2013 +0200
@@ -199,15 +199,17 @@
Binding.qualify mandatory data_b_name o
(rep_compat ? Binding.qualify false rep_compat_prefix);
- fun tfree_name_of (TFree (s, _)) = s
- | tfree_name_of (TVar ((s, _), _)) = s
- | tfree_name_of (Type (s, _)) = Long_Name.base_name s;
+ fun dest_TFree_or_TVar (TFree p) = p
+ | dest_TFree_or_TVar (TVar ((s, _), S)) = (s, S)
+ | dest_TFree_or_TVar _ = error "Invalid type argument";
- val (As, B) =
+ val (unsorted_As, B) =
no_defs_lthy
- |> variant_tfrees (map tfree_name_of As0)
+ |> variant_tfrees (map (fst o dest_TFree_or_TVar) As0)
||> the_single o fst o mk_TFrees 1;
+ val As = map2 (resort_tfree o snd o dest_TFree_or_TVar) As0 unsorted_As;
+
val dataT = Type (dataT_name, As);
val ctrs = map (mk_ctr As) ctrs0;
val ctr_Tss = map (binder_types o fastype_of) ctrs;
--- a/src/HOL/BNF/Tools/bnf_def.ML Thu Aug 29 19:20:35 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML Thu Aug 29 19:22:48 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,
@@ -292,10 +292,10 @@
name: binding,
T: typ,
live: int,
- lives: typ list, (*source type variables of map, only for composition*)
- lives': typ list, (*target type variables of map, only for composition*)
+ lives: typ list, (*source type variables of map*)
+ lives': typ list, (*target type variables of map*)
dead: int,
- deads: typ list, (*only for composition*)
+ deads: typ list,
map: term,
sets: term list,
bd: term,
@@ -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'";
@@ -539,7 +539,7 @@
val smart_max_inline_size = 25; (*FUDGE*)
-fun note_bnf_thms fact_policy qualify b bnf =
+fun note_bnf_thms fact_policy qualify bnf_b bnf =
let
val axioms = axioms_of_bnf bnf;
val facts = facts_of_bnf bnf;
@@ -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)]),
@@ -567,7 +567,7 @@
(set_bdN, #set_bd axioms)] @
(witNs ~~ wit_thmss_of_bnf bnf)
|> map (fn (thmN, thms) =>
- ((qualify (Binding.qualify true (Binding.name_of b) (Binding.name thmN)), []),
+ ((qualify (Binding.qualify true (Binding.name_of bnf_b) (Binding.name thmN)), []),
[(thms, [])]));
in
Local_Theory.notes notes #> snd
@@ -591,7 +591,7 @@
(rel_OON, [Lazy.force (#rel_OO facts)], [])]
|> filter_out (null o #2)
|> map (fn (thmN, thms, attrs) =>
- ((qualify (Binding.qualify true (Binding.name_of b) (Binding.name thmN)),
+ ((qualify (Binding.qualify true (Binding.name_of bnf_b) (Binding.name thmN)),
attrs), [(thms, [])]));
in
Local_Theory.notes notes #> snd
@@ -604,10 +604,10 @@
(* Define new BNFs *)
fun prepare_def const_policy mk_fact_policy qualify prep_term Ds_opt map_b rel_b set_bs
- (((((raw_b, raw_map), raw_sets), raw_bd_Abs), raw_wits), raw_rel_opt) no_defs_lthy =
+ (((((raw_bnf_b, raw_map), raw_sets), raw_bd_Abs), raw_wits), raw_rel_opt) no_defs_lthy =
let
val fact_policy = mk_fact_policy no_defs_lthy;
- val b = qualify raw_b;
+ val bnf_b = qualify raw_bnf_b;
val live = length raw_sets;
val nwits = length raw_wits;
@@ -622,13 +622,17 @@
error ("Trying to register the type " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^
" as unnamed BNF");
- val (b, key) =
- if Binding.eq_name (b, Binding.empty) then
+ val (bnf_b, key) =
+ if Binding.eq_name (bnf_b, Binding.empty) then
(case bd_rhsT of
- Type (C, Ts) => if forall (is_some o try dest_TFree) Ts
+ Type (C, Ts) => if forall (can dest_TFree) Ts
then (Binding.qualified_name C, C) else err bd_rhsT
| T => err T)
- else (b, Local_Theory.full_name no_defs_lthy b);
+ else (bnf_b, Local_Theory.full_name no_defs_lthy bnf_b);
+
+ val def_qualify = Binding.qualify false (Binding.name_of bnf_b);
+
+ fun mk_suffix_binding suf = Binding.suffix_name ("_" ^ suf) bnf_b;
fun maybe_define user_specified (b, rhs) lthy =
let
@@ -653,26 +657,22 @@
lthy |> not (pointer_eq (lthy_old, lthy)) ? Local_Theory.restore;
val map_bind_def =
- (fn () => if Binding.is_empty map_b then Binding.suffix_name ("_" ^ mapN) b else map_b,
- map_rhs);
+ (fn () => def_qualify (if Binding.is_empty map_b then mk_suffix_binding mapN else map_b),
+ map_rhs);
val set_binds_defs =
let
fun set_name i get_b =
(case try (nth set_bs) (i - 1) of
SOME b => if Binding.is_empty b then get_b else K b
- | NONE => get_b);
- val bs =
- if live = 1 then
- [set_name 1 (fn () => Binding.suffix_name ("_" ^ setN) b)]
- else
- map (fn i => set_name i (fn () => Binding.suffix_name ("_" ^ mk_setN i) b))
- (1 upto live);
+ | NONE => get_b) #> def_qualify;
+ val bs = if live = 1 then [set_name 1 (fn () => mk_suffix_binding setN)]
+ else map (fn i => set_name i (fn () => mk_suffix_binding (mk_setN i))) (1 upto live);
in bs ~~ set_rhss end;
- val bd_bind_def = (fn () => Binding.suffix_name ("_" ^ bdN) b, bd_rhs);
+ val bd_bind_def = (fn () => def_qualify (mk_suffix_binding bdN), bd_rhs);
val wit_binds_defs =
let
- 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);
+ val bs = if nwits = 1 then [fn () => def_qualify (mk_suffix_binding witN)]
+ else map (fn i => fn () => def_qualify (mk_suffix_binding (mk_witN i))) (1 upto nwits);
in bs ~~ wit_rhss end;
val (((((bnf_map_term, raw_map_def),
@@ -822,8 +822,8 @@
| SOME raw_rel => prep_term no_defs_lthy raw_rel);
val rel_bind_def =
- (fn () => if Binding.is_empty rel_b then Binding.suffix_name ("_" ^ relN) b else rel_b,
- rel_rhs);
+ (fn () => def_qualify (if Binding.is_empty rel_b then mk_suffix_binding relN else rel_b),
+ rel_rhs);
val ((bnf_rel_term, raw_rel_def), (lthy, lthy_old)) =
lthy
@@ -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;
@@ -1262,10 +1262,10 @@
val bnf_rel =
Term.subst_atomic_types ((Ds ~~ deads) @ (As' ~~ alphas) @ (Bs' ~~ betas)) rel;
- val bnf = mk_bnf b CA live alphas betas dead deads bnf_map bnf_sets bnf_bd axioms defs facts
- wits bnf_rel;
+ val bnf = mk_bnf bnf_b CA live alphas betas dead deads bnf_map bnf_sets bnf_bd axioms defs
+ facts wits bnf_rel;
in
- (bnf, lthy |> note_bnf_thms fact_policy qualify b bnf)
+ (bnf, lthy |> note_bnf_thms fact_policy qualify bnf_b bnf)
end;
val one_step_defs =
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Aug 29 19:20:35 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Aug 29 19:22:48 2013 +0200
@@ -66,9 +66,9 @@
rtac set_map) set_maps) THEN'
rtac @{thm image_empty}) 1;
-fun mk_map_wppull_tac map_id map_cong0 map_wpull map_comp set_maps =
+fun mk_map_wppull_tac map_id0 map_cong0 map_wpull map_comp set_maps =
if null set_maps then
- EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id, rtac map_id] 1
+ EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id0, rtac map_id0] 1
else EVERY' [REPEAT_DETERM o etac conjE, REPEAT_DETERM o dtac @{thm wppull_thePull},
REPEAT_DETERM o etac exE, rtac @{thm wpull_wppull}, rtac map_wpull,
REPEAT_DETERM o rtac @{thm wpull_thePull}, rtac ballI,
@@ -82,14 +82,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_Grp_tac rel_OO_Grps map_id map_cong0 map_id' map_comp set_maps
+fun mk_rel_Grp_tac rel_OO_Grps map_id0 map_cong0 map_id' map_comp set_maps
{context = ctxt, prems = _} =
let
val n = length set_maps;
val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac else rtac (hd rel_OO_Grps RS trans);
in
if null set_maps then
- unfold_thms_tac ctxt ((map_id RS @{thm Grp_UNIV_id}) :: rel_OO_Grps) THEN
+ unfold_thms_tac ctxt ((map_id0 RS @{thm Grp_UNIV_id}) :: rel_OO_Grps) THEN
rtac @{thm Grp_UNIV_idI[OF refl]} 1
else
EVERY' [rel_OO_Grps_tac, rtac @{thm antisym}, rtac @{thm predicate2I},
@@ -104,8 +104,8 @@
rtac @{thm predicate2I}, REPEAT_DETERM o eresolve_tac [@{thm GrpE}, exE, conjE],
hyp_subst_tac ctxt,
rtac @{thm relcomppI}, rtac @{thm conversepI},
- EVERY' (map2 (fn convol => fn map_id =>
- EVERY' [rtac @{thm GrpI}, rtac (box_equals OF [map_cong0, map_comp RS sym, map_id]),
+ EVERY' (map2 (fn convol => fn map_id0 =>
+ EVERY' [rtac @{thm GrpI}, rtac (box_equals OF [map_cong0, map_comp RS sym, map_id0]),
REPEAT_DETERM_N n o rtac (convol RS fun_cong),
REPEAT_DETERM o eresolve_tac [CollectE, conjE],
rtac CollectI,
@@ -116,13 +116,13 @@
@{thms fst_convol snd_convol} [map_id', refl])] 1
end;
-fun mk_rel_eq_tac n rel_Grp rel_cong map_id =
+fun mk_rel_eq_tac n rel_Grp rel_cong map_id0 =
(EVERY' (rtac (rel_cong RS trans) :: replicate n (rtac @{thm eq_alt})) THEN'
rtac (rel_Grp RSN (2, @{thm box_equals[OF _ sym sym[OF eq_alt]]})) THEN'
(if n = 0 then rtac refl
else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ "Grp"]},
rtac @{thm equalityI}, rtac subset_UNIV, rtac subsetI, rtac CollectI,
- CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac map_id])) 1;
+ CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac map_id0])) 1;
fun mk_rel_mono_tac rel_OO_Grps in_mono =
let
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Aug 29 19:20:35 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Aug 29 19:22:48 2013 +0200
@@ -13,6 +13,7 @@
index: int,
pre_bnfs: BNF_Def.bnf list,
nested_bnfs: BNF_Def.bnf list,
+ nesting_bnfs: BNF_Def.bnf list,
fp_res: BNF_FP_Util.fp_result,
ctr_defss: thm list list,
ctr_sugars: BNF_Ctr_Sugar.ctr_sugar list,
@@ -35,7 +36,9 @@
val mk_co_iter: theory -> BNF_FP_Util.fp_kind -> typ -> typ list -> term -> term
val nesty_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
val mk_map: int -> typ list -> typ list -> term -> term
+ val mk_rel: int -> typ list -> typ list -> term -> term
val build_map: local_theory -> (typ * typ -> term) -> typ * typ -> term
+ val build_rel: local_theory -> (typ * typ -> term) -> typ * typ -> term
val dest_map: Proof.context -> string -> term -> term * term list
val dest_ctr: Proof.context -> string -> term -> term * term list
val mk_co_iters_prelims: BNF_FP_Util.fp_kind -> typ list -> typ list -> int list ->
@@ -110,6 +113,7 @@
index: int,
pre_bnfs: bnf list,
nested_bnfs: bnf list,
+ nesting_bnfs: bnf list,
fp_res: fp_result,
ctr_defss: thm list list,
ctr_sugars: ctr_sugar list,
@@ -123,10 +127,11 @@
{T = T2, fp = fp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) =
T1 = T2 andalso fp1 = fp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2);
-fun morph_fp_sugar phi {T, fp, index, pre_bnfs, nested_bnfs, fp_res, ctr_defss, ctr_sugars,
- co_iterss, co_inducts, co_iter_thmsss} =
+fun morph_fp_sugar phi {T, fp, index, pre_bnfs, nested_bnfs, nesting_bnfs, fp_res, ctr_defss,
+ ctr_sugars, co_iterss, co_inducts, co_iter_thmsss} =
{T = Morphism.typ phi T, fp = fp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs,
- nested_bnfs = map (morph_bnf phi) nested_bnfs, fp_res = morph_fp_result phi fp_res,
+ nested_bnfs = map (morph_bnf phi) nested_bnfs, nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
+ fp_res = morph_fp_result phi fp_res,
ctr_defss = map (map (Morphism.thm phi)) ctr_defss,
ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars,
co_iterss = map (map (Morphism.term phi)) co_iterss,
@@ -155,13 +160,14 @@
Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi => Data.map (Symtab.default (key, morph_fp_sugar phi fp_sugar)));
-fun register_fp_sugars fp pre_bnfs nested_bnfs (fp_res as {Ts, ...}) ctr_defss ctr_sugars co_iterss
- co_inducts co_iter_thmsss lthy =
+fun register_fp_sugars fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctr_defss
+ ctr_sugars co_iterss co_inducts co_iter_thmsss lthy =
(0, lthy)
|> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1,
register_fp_sugar s {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs,
- nested_bnfs = nested_bnfs, fp_res = fp_res, ctr_defss = ctr_defss, ctr_sugars = ctr_sugars,
- co_iterss = co_iterss, co_inducts = co_inducts, co_iter_thmsss = co_iter_thmsss}
+ nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, fp_res = fp_res,
+ ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, co_iterss = co_iterss,
+ co_inducts = co_inducts, co_iter_thmsss = co_iter_thmsss}
lthy)) Ts
|> snd;
@@ -270,11 +276,13 @@
Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
end;
-fun build_map lthy build_simple =
+local
+
+fun build_map_or_rel mk const of_bnf dest lthy build_simple =
let
fun build (TU as (T, U)) =
if T = U then
- HOLogic.id_const T
+ const T
else
(case TU of
(Type (s, Ts), Type (s', Us)) =>
@@ -282,14 +290,21 @@
let
val bnf = the (bnf_of lthy s);
val live = live_of_bnf bnf;
- val mapx = mk_map live Ts Us (map_of_bnf bnf);
- val TUs' = map dest_funT (fst (strip_typeN live (fastype_of mapx)));
+ val mapx = mk live Ts Us (of_bnf bnf);
+ val TUs' = map dest (fst (strip_typeN live (fastype_of mapx)));
in Term.list_comb (mapx, map build TUs') end
else
build_simple TU
| _ => build_simple TU);
in build end;
+in
+
+val build_map = build_map_or_rel mk_map HOLogic.id_const map_of_bnf dest_funT;
+val build_rel = build_map_or_rel mk_rel HOLogic.eq_const rel_of_bnf dest_pred2T;
+
+end;
+
fun fo_match ctxt t pat =
let val thy = Proof_Context.theory_of ctxt in
Pattern.first_order_match thy (pat, t) (Vartab.empty, Vartab.empty)
@@ -587,8 +602,8 @@
val pre_map_defs = map map_def_of_bnf pre_bnfs;
val pre_set_defss = map set_defs_of_bnf pre_bnfs;
- val nesting_map_ids'' = map (unfold_thms lthy [id_def] o map_id_of_bnf) nesting_bnfs;
- val nested_map_ids'' = map (unfold_thms lthy [id_def] o map_id_of_bnf) nested_bnfs;
+ val nesting_map_ids'' = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
+ val nested_map_ids'' = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs;
val nested_set_map's = maps set_map'_of_bnf nested_bnfs;
val fp_b_names = map base_name_of_typ fpTs;
@@ -748,7 +763,7 @@
val pre_map_defs = map map_def_of_bnf pre_bnfs;
val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
- val nesting_map_ids'' = map (unfold_thms lthy [id_def] o map_id_of_bnf) nesting_bnfs;
+ val nesting_map_ids'' = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
val nesting_rel_eqs = map rel_eq_of_bnf nesting_bnfs;
val fp_b_names = map base_name_of_typ fpTs;
@@ -1023,8 +1038,8 @@
val fp_bs = map type_binding_of specs;
val fp_b_names = map Binding.name_of fp_bs;
val fp_common_name = mk_common_name fp_b_names;
- val map_bs = map2 (fn fp_b_name => qualify false fp_b_name o map_binding_of) fp_b_names specs;
- val rel_bs = map2 (fn fp_b_name => qualify false fp_b_name o rel_binding_of) fp_b_names specs;
+ val map_bs = map map_binding_of specs;
+ val rel_bs = map rel_binding_of specs;
fun prepare_type_arg (_, (ty, c)) =
let val TFree (s, _) = prepare_typ no_defs_lthy0 ty in
@@ -1034,43 +1049,33 @@
val Ass0 = map (map prepare_type_arg o type_args_named_constrained_of) specs;
val unsorted_Ass0 = map (map (resort_tfree HOLogic.typeS)) Ass0;
val unsorted_As = Library.foldr1 merge_type_args unsorted_Ass0;
+ val num_As = length unsorted_As;
val set_bss = map (map fst o type_args_named_constrained_of) specs;
- val _ = has_duplicates (op =) unsorted_As andalso
- error ("Duplicate parameters in " ^ co_prefix fp ^ "datatype specification");
+ val (((Bs0, Cs), Xs), no_defs_lthy) =
+ no_defs_lthy0
+ |> fold (Variable.declare_typ o resort_tfree dummyS) unsorted_As
+ |> mk_TFrees num_As
+ ||>> mk_TFrees nn
+ ||>> variant_tfrees fp_b_names;
+
+ fun add_fake_type spec = Typedecl.basic_typedecl (type_binding_of spec, num_As, mixfix_of spec);
+
+ val (fake_T_names, fake_lthy) = fold_map add_fake_type specs no_defs_lthy0;
+
+ val qsoty = quote o Syntax.string_of_typ fake_lthy;
+
+ val _ = (case duplicates (op =) unsorted_As of [] => ()
+ | A :: _ => error ("Duplicate type parameter " ^ qsoty A ^ " in " ^ co_prefix fp ^
+ "datatype specification"));
val bad_args =
map (Logic.type_map (singleton (Variable.polymorphic no_defs_lthy0))) unsorted_As
|> filter_out Term.is_TVar;
val _ = null bad_args orelse
- error ("Locally fixed type argument " ^
- quote (Syntax.string_of_typ no_defs_lthy0 (hd bad_args)) ^ " in " ^ co_prefix fp ^
+ error ("Locally fixed type argument " ^ qsoty (hd bad_args) ^ " in " ^ co_prefix fp ^
"datatype specification");
- val (((Bs0, Cs), Xs), no_defs_lthy) =
- no_defs_lthy0
- |> fold (Variable.declare_typ o resort_tfree dummyS) unsorted_As
- |> mk_TFrees (length unsorted_As)
- ||>> mk_TFrees nn
- ||>> variant_tfrees fp_b_names;
-
- (* TODO: Cleaner handling of fake contexts, without "background_theory". *)
-
- fun add_fake_type spec =
- (*The "qualify" hack below is for the case where the new type shadows an existing global type
- defined in the same theory.*)
- Sign.add_type no_defs_lthy (qualify false "" (type_binding_of spec),
- length (type_args_named_constrained_of spec), mixfix_of spec);
-
- val fake_thy = fold add_fake_type specs;
- val fake_lthy = Proof_Context.background_theory fake_thy no_defs_lthy;
-
- fun mk_fake_T b =
- Type (fst (Term.dest_Type (Proof_Context.read_type_name fake_lthy true (Binding.name_of b))),
- unsorted_As);
-
- val fake_Ts = map mk_fake_T fp_bs;
-
val mixfixes = map mixfix_of specs;
val _ = (case duplicates Binding.eq_name fp_bs of [] => ()
@@ -1090,20 +1095,19 @@
val (As :: _) :: fake_ctr_Tsss =
burrow (burrow (Syntax.check_typs fake_lthy)) (Ass0 :: fake_ctr_Tsss0);
-
- val _ = (case duplicates (op =) unsorted_As of [] => ()
- | A :: _ => error ("Duplicate type parameter " ^
- quote (Syntax.string_of_typ no_defs_lthy A)));
+ val As' = map dest_TFree As;
val rhs_As' = fold (fold (fold Term.add_tfreesT)) fake_ctr_Tsss [];
- val _ = (case subtract (op =) (map dest_TFree As) rhs_As' of
- [] => ()
- | A' :: _ => error ("Extra type variable on right-hand side: " ^
- quote (Syntax.string_of_typ no_defs_lthy (TFree A'))));
+ val _ = (case subtract (op =) As' rhs_As' of [] => ()
+ | extras => error ("Extra type variables on right-hand side: " ^
+ commas (map (qsoty o TFree) extras)));
- fun eq_fpT_check (T as Type (s, Us)) (Type (s', Us')) =
- s = s' andalso (Us = Us' orelse error ("Illegal occurrence of recursive type " ^
- quote (Syntax.string_of_typ fake_lthy T)))
+ val fake_Ts = map (fn s => Type (s, As)) fake_T_names;
+
+ fun eq_fpT_check (T as Type (s, Ts)) (T' as Type (s', Ts')) =
+ s = s' andalso (Ts = Ts' orelse
+ error ("Wrong type arguments in " ^ co_prefix fp ^ "recursive type " ^ qsoty T ^
+ " (expected " ^ qsoty T' ^ ")"))
| eq_fpT_check _ _ = false;
fun freeze_fp (T as Type (s, Ts)) =
@@ -1120,6 +1124,11 @@
val fp_eqs =
map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctrXs_sum_prod_Ts;
+ val rhsXs_As' = fold (fold (fold Term.add_tfreesT)) ctrXs_Tsss [];
+ val _ = (case subtract (op =) rhsXs_As' As' of [] => ()
+ | extras => List.app (fn extra => warning ("Unused type variable on right-hand side of " ^
+ co_prefix fp ^ "datatype definition: " ^ qsoty (TFree extra))) extras);
+
val (pre_bnfs, (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0, dtors = dtors0,
xtor_co_iterss = xtor_co_iterss0, xtor_co_induct, dtor_ctors, ctor_dtors, ctor_injects,
dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms, xtor_co_iter_thmss, ...},
@@ -1130,7 +1139,6 @@
(case X_backdrop of
Type (bad_tc, _) =>
let
- val qsoty = quote o Syntax.string_of_typ fake_lthy;
val fake_T = qsoty (unfreeze_fp X);
val fake_T_backdrop = qsoty (unfreeze_fp X_backdrop);
fun register_hint () =
@@ -1168,13 +1176,13 @@
val live = live_of_bnf any_fp_bnf;
val _ =
if live = 0 andalso exists (not o Binding.is_empty) (map_bs @ rel_bs) then
- warning ("Map function and relator names ignored")
+ warning "Map function and relator names ignored"
else
();
val Bs =
map3 (fn alive => fn A as TFree (_, S) => fn B => if alive then resort_tfree S B else A)
- (liveness_of_fp_bnf (length As) any_fp_bnf) As Bs0;
+ (liveness_of_fp_bnf num_As any_fp_bnf) As Bs0;
val B_ify = Term.typ_subst_atomic (As ~~ Bs);
@@ -1275,7 +1283,7 @@
val inject_tacss =
map2 (fn 0 => K [] | _ => fn ctr_def => [fn {context = ctxt, ...} =>
- mk_inject_tac ctxt ctr_def ctor_inject]) ms ctr_defs;
+ mk_inject_tac ctxt ctr_def ctor_inject]) ms ctr_defs;
val half_distinct_tacss =
map (map (fn (def, def') => fn {context = ctxt, ...} =>
@@ -1336,9 +1344,9 @@
fun mk_rel_thm postproc ctr_defs' cxIn cyIn =
fold_thms lthy ctr_defs'
- (unfold_thms lthy (@{thm Inl_Inr_False} :: pre_rel_def ::
- (if fp = Least_FP then [] else [dtor_ctor]) @ sum_prod_thms_rel)
- (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
+ (unfold_thms lthy (@{thm Inl_Inr_False} :: pre_rel_def ::
+ (if fp = Least_FP then [] else [dtor_ctor]) @ sum_prod_thms_rel)
+ (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
|> postproc
|> singleton (Proof_Context.export names_lthy no_defs_lthy);
@@ -1426,8 +1434,8 @@
in
lthy
|> Local_Theory.notes (common_notes @ notes) |> snd
- |> register_fp_sugars Least_FP pre_bnfs nested_bnfs fp_res ctr_defss ctr_sugars iterss
- [induct_thm] (transpose [fold_thmss, rec_thmss])
+ |> register_fp_sugars Least_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss ctr_sugars
+ iterss [induct_thm] (transpose [fold_thmss, rec_thmss])
end;
fun derive_and_note_coinduct_coiters_thms_for_types
@@ -1485,8 +1493,9 @@
in
lthy
|> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
- |> register_fp_sugars Greatest_FP pre_bnfs nested_bnfs fp_res ctr_defss ctr_sugars coiterss
- [coinduct_thm, strong_coinduct_thm] (transpose [unfold_thmss, corec_thmss])
+ |> register_fp_sugars Greatest_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss
+ ctr_sugars coiterss [coinduct_thm, strong_coinduct_thm]
+ (transpose [unfold_thmss, corec_thmss])
end;
val lthy'' = lthy'
@@ -1535,7 +1544,7 @@
that we don't want them to be highlighted everywhere. *)
fun extract_map_rel ("map", b) = apfst (K b)
| extract_map_rel ("rel", b) = apsnd (K b)
- | extract_map_rel (s, _) = error ("Expected \"map\" or \"rel\" instead of " ^ quote s);
+ | extract_map_rel (s, _) = error ("Unknown label " ^ quote s ^ " (expected \"map\" or \"rel\")");
val parse_map_rel_bindings =
@{keyword "("} |-- Scan.repeat parse_map_rel_binding --| @{keyword ")"}
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML Thu Aug 29 19:20:35 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Thu Aug 29 19:22:48 2013 +0200
@@ -582,20 +582,18 @@
fun fp_sort Ass =
subtract (op =) Xs (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs) @ Xs;
- val common_name = mk_common_name (map Binding.name_of bs);
-
- fun raw_qualify b =
- let val s = Binding.name_of b in
- Binding.qualify false s o Binding.qualify true (rawN ^ s)
+ fun raw_qualify base_b =
+ let val (_, qs, n) = Binding.dest base_b;
+ in
+ Binding.prefix_name rawN
+ #> fold_rev (fn (s, mand) => Binding.qualify mand s) (qs @ [(n, true)])
end;
val ((bnfs, (deadss, livess)), (unfold_set, lthy)) = apfst (apsnd split_list o split_list)
(fold_map2 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) fp_sort Xs) bs rhsXs
(empty_unfolds, lthy));
- fun qualify i =
- let val namei = common_name ^ nonzero_string_of_int i;
- in Binding.qualify true namei end;
+ fun norm_qualify i = Binding.qualify true (Binding.name_of (nth bs (Int.max (0, i - 1))));
val Ass = map (map dest_TFree) livess;
val resDs = fold (subtract (op =)) Ass resBs;
@@ -604,14 +602,15 @@
val timer = time (timer "Construction of BNFs");
val ((kill_poss, _), (bnfs', (unfold_set', lthy'))) =
- normalize_bnfs qualify Ass Ds fp_sort bnfs unfold_set lthy;
+ normalize_bnfs norm_qualify Ass Ds fp_sort bnfs unfold_set lthy;
val Dss = map3 (append oo map o nth) livess kill_poss deadss;
- fun pre_binding b = Binding.qualify false (Binding.name_of b) (Binding.prefix_name preN b);
+ val pre_qualify = Binding.qualify false o Binding.name_of;
val ((pre_bnfs, deadss), lthy'') =
- fold_map3 (seal_bnf unfold_set') (map pre_binding bs) Dss bnfs' lthy'
+ fold_map3 (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b))
+ bs Dss bnfs' lthy'
|>> split_list;
val timer = time (timer "Normalization & sealing of BNFs");
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 29 19:20:35 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 29 19:22:48 2013 +0200
@@ -218,7 +218,7 @@
val sym_map_comps = map mk_sym map_comps;
val map_comp's = map map_comp'_of_bnf bnfs;
val map_cong0s = map map_cong0_of_bnf bnfs;
- val map_ids = map map_id_of_bnf bnfs;
+ val map_id0s = map map_id0_of_bnf bnfs;
val map_id's = map map_id'_of_bnf bnfs;
val map_wpulls = map map_wpull_of_bnf bnfs;
val set_bdss = map set_bd_of_bnf bnfs;
@@ -2007,7 +2007,7 @@
`split_conj_thm (split_conj_prems n
(mor_UNIV_thm RS iffD2 RS corec_unique_mor_thm)
|> Local_Defs.unfold lthy (@{thms o_sum_case o_id id_o o_assoc sum_case_o_inj(1)} @
- map_ids @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]});
+ map_id0s @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]});
val timer = time (timer "corec definitions & thms");
@@ -2074,8 +2074,8 @@
val timer = time (timer "coinduction");
- fun mk_dtor_map_DEADID_thm dtor_inject map_id =
- trans OF [iffD2 OF [dtor_inject, id_apply], map_id RS sym];
+ fun mk_dtor_map_DEADID_thm dtor_inject map_id0 =
+ trans OF [iffD2 OF [dtor_inject, id_apply], map_id0 RS sym];
fun mk_dtor_Jrel_DEADID_thm dtor_inject bnf =
trans OF [rel_eq_of_bnf bnf RS @{thm predicate2_eqD}, dtor_inject] RS sym;
@@ -2457,8 +2457,8 @@
val timer = time (timer "helpers for BNF properties");
- val map_id_tacs =
- map2 (K oo mk_map_id_tac map_thms) dtor_unfold_unique_thms unfold_dtor_thms;
+ val map_id0_tacs =
+ map2 (K oo mk_map_id0_tac map_thms) dtor_unfold_unique_thms unfold_dtor_thms;
val map_comp_tacs = map (fn thm => K (rtac (thm RS sym) 1)) map_comp_thms;
val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms;
val set_nat_tacss =
@@ -2476,7 +2476,7 @@
val rel_OO_Grp_tacs = replicate n (K (rtac refl 1));
- val tacss = map9 zip_axioms map_id_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
+ val tacss = map9 zip_axioms map_id0_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
bd_co_tacs bd_cinf_tacs set_bd_tacss map_wpull_tacs rel_OO_Grp_tacs;
val (hset_dtor_incl_thmss, hset_hset_dtor_incl_thmsss, dtor_hset_induct_thms) =
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Aug 29 19:20:35 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Aug 29 19:22:48 2013 +0200
@@ -55,7 +55,7 @@
val mk_map_comp_tac: int -> int -> thm list -> thm list -> thm list -> thm -> tactic
val mk_mcong_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list -> thm list ->
thm list list -> thm list list -> thm list list list -> tactic
- val mk_map_id_tac: thm list -> thm -> thm -> tactic
+ val mk_map_id0_tac: thm list -> thm -> thm -> tactic
val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> tactic
val mk_dtor_map_unique_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
val mk_mor_Abs_tac: thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic
@@ -1030,7 +1030,7 @@
REPEAT_DETERM_N (n - 1) o rtac @{thm Un_least},
EVERY' (map (fn thm => rtac @{thm UN_least} THEN' etac thm) set_hset_incl_hsets)] 1;
-fun mk_map_id_tac maps unfold_unique unfold_dtor =
+fun mk_map_id0_tac maps unfold_unique unfold_dtor =
EVERY' [rtac (unfold_unique RS trans), EVERY' (map (rtac o mk_sym) maps),
rtac unfold_dtor] 1;
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 29 19:20:35 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 29 19:22:48 2013 +0200
@@ -162,7 +162,7 @@
val sym_map_comps = map (fn bnf => map_comp_of_bnf bnf RS sym) bnfs;
val map_comp's = map map_comp'_of_bnf bnfs;
val map_cong0s = map map_cong0_of_bnf bnfs;
- val map_ids = map map_id_of_bnf bnfs;
+ val map_id0s = map map_id0_of_bnf bnfs;
val map_id's = map map_id'_of_bnf bnfs;
val map_wpulls = map map_wpull_of_bnf bnfs;
val set_map'ss = map set_map'_of_bnf bnfs;
@@ -1303,7 +1303,7 @@
`split_conj_thm (split_conj_prems n
(mor_UNIV_thm RS iffD2 RS rec_unique_mor_thm)
|> Local_Defs.unfold lthy (@{thms convol_o o_id id_o o_assoc[symmetric] fst_convol} @
- map_ids @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ convol, OF refl]});
+ map_id0s @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ convol, OF refl]});
val timer = time (timer "rec definitions & thms");
@@ -1385,8 +1385,8 @@
val timer = time (timer "induction");
- fun mk_ctor_map_DEADID_thm ctor_inject map_id =
- trans OF [id_apply, iffD2 OF [ctor_inject, map_id RS sym]];
+ fun mk_ctor_map_DEADID_thm ctor_inject map_id0 =
+ trans OF [id_apply, iffD2 OF [ctor_inject, map_id0 RS sym]];
fun mk_ctor_Irel_DEADID_thm ctor_inject bnf =
trans OF [ctor_inject, rel_eq_of_bnf bnf RS @{thm predicate2_eqD} RS sym];
@@ -1691,7 +1691,7 @@
val timer = time (timer "helpers for BNF properties");
- val map_id_tacs = map (K o mk_map_id_tac map_ids) ctor_map_unique_thms;
+ val map_id0_tacs = map (K o mk_map_id0_tac map_id0s) ctor_map_unique_thms;
val map_comp_tacs =
map2 (K oo mk_map_comp_tac map_comp's ctor_map_thms) ctor_map_unique_thms ks;
val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms;
@@ -1703,7 +1703,7 @@
val rel_OO_Grp_tacs = replicate n (K (rtac refl 1));
- val tacss = map9 zip_axioms map_id_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
+ val tacss = map9 zip_axioms map_id0_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
bd_co_tacs bd_cinf_tacs set_bd_tacss map_wpull_tacs rel_OO_Grp_tacs;
val ctor_witss =
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Aug 29 19:20:35 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Aug 29 19:22:48 2013 +0200
@@ -40,7 +40,7 @@
val mk_lfp_map_wpull_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list ->
thm list list -> thm list list list -> thm list -> tactic
val mk_map_comp_tac: thm list -> thm list -> thm -> int -> tactic
- val mk_map_id_tac: thm list -> thm -> tactic
+ val mk_map_id0_tac: thm list -> thm -> tactic
val mk_map_tac: int -> int -> thm -> thm -> thm -> tactic
val mk_ctor_map_unique_tac: thm -> thm list -> {prems: thm list, context: Proof.context} -> tactic
val mk_mcong_tac: (int -> tactic) -> thm list list list -> thm list -> thm list ->
@@ -704,11 +704,11 @@
(* BNF tactics *)
-fun mk_map_id_tac map_ids unique =
+fun mk_map_id0_tac map_id0s unique =
(rtac sym THEN' rtac unique THEN'
EVERY' (map (fn thm =>
EVERY' [rtac trans, rtac @{thm id_o}, rtac trans, rtac sym, rtac @{thm o_id},
- rtac (thm RS sym RS arg_cong)]) map_ids)) 1;
+ rtac (thm RS sym RS arg_cong)]) map_id0s)) 1;
fun mk_map_comp_tac map_comps ctor_maps unique iplus1 =
let
--- a/src/HOL/BNF/Tools/bnf_util.ML Thu Aug 29 19:20:35 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML Thu Aug 29 19:22:48 2013 +0200
@@ -323,7 +323,7 @@
fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);
-(* The standard binding stands for a name generated following the canonical convention (e.g.
+(* The standard binding stands for a name generated following the canonical convention (e.g.,
"is_Nil" from "Nil"). The smart binding is either the standard binding or no binding at all,
depending on the context. *)
val standard_binding = @{binding _};
@@ -334,11 +334,13 @@
val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty;
(*TODO: is this really different from Typedef.add_typedef_global?*)
-fun typedef typ set opt_morphs tac lthy =
+fun typedef (b, Ts, mx) set opt_morphs tac lthy =
let
+ (*Work around loss of qualification in "typedef" axioms by replicating it in the name*)
+ val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (#2 (Binding.dest b))) b;
val ((name, info), (lthy, lthy_old)) =
lthy
- |> Typedef.add_typedef typ set opt_morphs tac
+ |> Typedef.add_typedef (b', Ts, mx) set opt_morphs tac
||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy_old lthy;
in