--- a/src/HOL/Tools/BNF/bnf_gfp.ML Fri Jan 31 13:42:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Fri Jan 31 13:45:39 2014 +0100
@@ -163,7 +163,6 @@
val Zeros = map (fn empty =>
HOLogic.mk_tuple (map (fn U => absdummy U empty) activeAs)) emptys;
val hrecTs = map fastype_of Zeros;
- val hsetTs = map (fn hrecT => Library.foldr (op -->) (sTs, HOLogic.natT --> hrecT)) hrecTs;
val (((((((((((((((((((((((((((((((((((zs, zs'), zs_copy), zs_copy2), z's), (ys, ys')),
As), Bs), Bs_copy), B's), B''s), ss), sum_ss), s's), s''s), fs), fs_copy),
@@ -297,32 +296,28 @@
(* coalgebra *)
val coalg_bind = mk_internal_b (coN ^ algN) ;
- val coalg_name = Binding.name_of coalg_bind;
val coalg_def_bind = (Thm.def_binding coalg_bind, []);
(*forall i = 1 ... n: (\<forall>x \<in> Bi. si \<in> Fi_in A1 .. Am B1 ... Bn)*)
val coalg_spec =
let
- val coalgT = Library.foldr (op -->) (ATs @ BTs @ sTs, HOLogic.boolT);
-
val ins = map3 mk_in (replicate n (As @ Bs)) setssAs FTsAs;
fun mk_coalg_conjunct B s X z z' =
mk_Ball B (Term.absfree z' (HOLogic.mk_mem (s $ z, X)));
- val lhs = Term.list_comb (Free (coalg_name, coalgT), As @ Bs @ ss);
val rhs = Library.foldr1 HOLogic.mk_conj (map5 mk_coalg_conjunct Bs ss ins zs zs')
in
- mk_Trueprop_eq (lhs, rhs)
+ fold_rev (Term.absfree o Term.dest_Free) (As @ Bs @ ss) rhs
end;
val ((coalg_free, (_, coalg_def_free)), (lthy, lthy_old)) =
lthy
- |> Specification.definition (SOME (coalg_bind, NONE, NoSyn), (coalg_def_bind, coalg_spec))
+ |> Local_Theory.define ((coalg_bind, NoSyn), (coalg_def_bind, coalg_spec))
||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy_old lthy;
val coalg = fst (Term.dest_Const (Morphism.term phi coalg_free));
- val coalg_def = Morphism.thm phi coalg_def_free;
+ val coalg_def = mk_unabs_def (live + n) (Morphism.thm phi coalg_def_free RS meta_eq_to_obj_eq);
fun mk_coalg As Bs ss =
let
@@ -373,7 +368,6 @@
(* morphism *)
val mor_bind = mk_internal_b morN;
- val mor_name = Binding.name_of mor_bind;
val mor_def_bind = (Thm.def_binding mor_bind, []);
(*fbetw) forall i = 1 ... n: (\<forall>x \<in> Bi. fi x \<in> B'i)*)
@@ -381,29 +375,26 @@
Fi_map id ... id f1 ... fn (si x) = si' (fi x)*)
val mor_spec =
let
- val morT = Library.foldr (op -->) (BTs @ sTs @ B'Ts @ s'Ts @ fTs, HOLogic.boolT);
-
fun mk_fbetw f B1 B2 z z' =
mk_Ball B1 (Term.absfree z' (HOLogic.mk_mem (f $ z, B2)));
fun mk_mor B mapAsBs f s s' z z' =
mk_Ball B (Term.absfree z' (HOLogic.mk_eq
(Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ z]), s' $ (f $ z))));
- val lhs = Term.list_comb (Free (mor_name, morT), Bs @ ss @ B's @ s's @ fs);
val rhs = HOLogic.mk_conj
(Library.foldr1 HOLogic.mk_conj (map5 mk_fbetw fs Bs B's zs zs'),
Library.foldr1 HOLogic.mk_conj (map7 mk_mor Bs mapsAsBs fs ss s's zs zs'))
in
- mk_Trueprop_eq (lhs, rhs)
+ fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss @ B's @ s's @ fs) rhs
end;
val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) =
lthy
- |> Specification.definition (SOME (mor_bind, NONE, NoSyn), (mor_def_bind, mor_spec))
+ |> Local_Theory.define ((mor_bind, NoSyn), (mor_def_bind, mor_spec))
||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy_old lthy;
val mor = fst (Term.dest_Const (Morphism.term phi mor_free));
- val mor_def = Morphism.thm phi mor_def_free;
+ val mor_def = mk_unabs_def (5 * n) (Morphism.thm phi mor_def_free RS meta_eq_to_obj_eq);
fun mk_mor Bs1 ss1 Bs2 ss2 fs =
let
@@ -518,10 +509,9 @@
val timer = time (timer "Morphism definition & thms");
fun hset_rec_bind j = mk_internal_b (hset_recN ^ (if m = 1 then "" else string_of_int j));
- val hset_rec_name = Binding.name_of o hset_rec_bind;
val hset_rec_def_bind = rpair [] o Thm.def_binding o hset_rec_bind;
- fun hset_rec_spec j Zero hsetT hrec hrec' =
+ fun hset_rec_spec j Zero hrec hrec' =
let
fun mk_Suc s setsAs z z' =
let
@@ -535,24 +525,23 @@
val Suc = Term.absdummy HOLogic.natT (Term.absfree hrec'
(HOLogic.mk_tuple (map4 mk_Suc ss setssAs zs zs')));
- val lhs = Term.list_comb (Free (hset_rec_name j, hsetT), ss);
val rhs = mk_nat_rec Zero Suc;
in
- mk_Trueprop_eq (lhs, rhs)
+ fold_rev (Term.absfree o Term.dest_Free) ss rhs
end;
val ((hset_rec_frees, (_, hset_rec_def_frees)), (lthy, lthy_old)) =
lthy
- |> fold_map5 (fn j => fn Zero => fn hsetT => fn hrec => fn hrec' => Specification.definition
- (SOME (hset_rec_bind j, NONE, NoSyn),
- (hset_rec_def_bind j, hset_rec_spec j Zero hsetT hrec hrec')))
- ls Zeros hsetTs hrecs hrecs'
+ |> fold_map4 (fn j => fn Zero => fn hrec => fn hrec' => Local_Theory.define
+ ((hset_rec_bind j, NoSyn), (hset_rec_def_bind j, hset_rec_spec j Zero hrec hrec')))
+ ls Zeros hrecs hrecs'
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy_old lthy;
- val hset_rec_defs = map (Morphism.thm phi) hset_rec_def_frees;
+ val hset_rec_defs = map (fn def =>
+ mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) hset_rec_def_frees;
val hset_recs = map (fst o Term.dest_Const o Morphism.term phi) hset_rec_frees;
fun mk_hset_rec ss nat i j T =
@@ -573,35 +562,31 @@
fun hset_binds j = mk_internal_bs (hsetN ^ (if m = 1 then "" else string_of_int j))
fun hset_bind i j = nth (hset_binds j) (i - 1);
- val hset_name = Binding.name_of oo hset_bind;
val hset_def_bind = rpair [] o Thm.def_binding oo hset_bind;
fun hset_spec i j =
let
- val U = nth activeAs (i - 1);
val z = nth zs (i - 1);
val T = nth passiveAs (j - 1);
- val setT = HOLogic.mk_setT T;
- val hsetT = Library.foldr (op -->) (sTs, U --> setT);
-
- val lhs = Term.list_comb (Free (hset_name i j, hsetT), ss @ [z]);
+
val rhs = mk_UNION (HOLogic.mk_UNIV HOLogic.natT)
(Term.absfree nat' (mk_hset_rec ss nat i j T $ z));
in
- mk_Trueprop_eq (lhs, rhs)
+ fold_rev (Term.absfree o Term.dest_Free) (ss @ [z]) rhs
end;
val ((hset_frees, (_, hset_def_frees)), (lthy, lthy_old)) =
lthy
- |> fold_map (fn i => fold_map (fn j => Specification.definition
- (SOME (hset_bind i j, NONE, NoSyn), (hset_def_bind i j, hset_spec i j))) ls) ks
+ |> fold_map (fn i => fold_map (fn j => Local_Theory.define
+ ((hset_bind i j, NoSyn), (hset_def_bind i j, hset_spec i j))) ls) ks
|>> map (apsnd split_list o split_list)
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy_old lthy;
- val hset_defss = map (map (Morphism.thm phi)) hset_def_frees;
+ val hset_defss = map (map (fn def =>
+ mk_unabs_def (n + 1) (Morphism.thm phi def RS meta_eq_to_obj_eq))) hset_def_frees;
val hset_defss' = transpose hset_defss;
val hset_namess = map (map (fst o Term.dest_Const o Morphism.term phi)) hset_frees;
@@ -723,7 +708,6 @@
(* bisimulation *)
val bis_bind = mk_internal_b bisN;
- val bis_name = Binding.name_of bis_bind;
val bis_def_bind = (Thm.def_binding bis_bind, []);
fun mk_bis_le_conjunct R B1 B2 = mk_leq R (mk_Times (B1, B2));
@@ -731,8 +715,6 @@
val bis_spec =
let
- val bisT = Library.foldr (op -->) (ATs @ BTs @ sTs @ B'Ts @ s'Ts @ setRTs, HOLogic.boolT);
-
val fst_args = passive_ids @ fsts;
val snd_args = passive_ids @ snds;
fun mk_bis R s s' b1 b2 RF map1 map2 sets =
@@ -743,22 +725,21 @@
(HOLogic.mk_eq (Term.list_comb (map1, fst_args) $ RF, s $ b1),
HOLogic.mk_eq (Term.list_comb (map2, snd_args) $ RF, s' $ b2))))));
- val lhs = Term.list_comb (Free (bis_name, bisT), As @ Bs @ ss @ B's @ s's @ Rs);
val rhs = HOLogic.mk_conj
(bis_le, Library.foldr1 HOLogic.mk_conj
(map9 mk_bis Rs ss s's zs z's RFs map_fsts map_snds bis_setss))
in
- mk_Trueprop_eq (lhs, rhs)
+ fold_rev (Term.absfree o Term.dest_Free) (As @ Bs @ ss @ B's @ s's @ Rs) rhs
end;
val ((bis_free, (_, bis_def_free)), (lthy, lthy_old)) =
lthy
- |> Specification.definition (SOME (bis_bind, NONE, NoSyn), (bis_def_bind, bis_spec))
+ |> Local_Theory.define ((bis_bind, NoSyn), (bis_def_bind, bis_spec))
||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy_old lthy;
val bis = fst (Term.dest_Const (Morphism.term phi bis_free));
- val bis_def = Morphism.thm phi bis_def_free;
+ val bis_def = mk_unabs_def (m + 5 * n) (Morphism.thm phi bis_def_free RS meta_eq_to_obj_eq);
fun mk_bis As Bs1 ss1 Bs2 ss2 Rs =
let
@@ -869,32 +850,26 @@
val lsbis_binds = mk_internal_bs lsbisN;
fun lsbis_bind i = nth lsbis_binds (i - 1);
- val lsbis_name = Binding.name_of o lsbis_bind;
val lsbis_def_bind = rpair [] o Thm.def_binding o lsbis_bind;
val all_sbis = HOLogic.mk_Collect (fst Rtuple', snd Rtuple', list_exists_free sRs
(HOLogic.mk_conj (HOLogic.mk_eq (Rtuple, HOLogic.mk_tuple sRs), mk_sbis As Bs ss sRs)));
- fun lsbis_spec i RT =
- let
- fun mk_lsbisT RT =
- Library.foldr (op -->) (map fastype_of (As @ Bs @ ss), RT);
- val lhs = Term.list_comb (Free (lsbis_name i, mk_lsbisT RT), As @ Bs @ ss);
- val rhs = mk_UNION all_sbis (Term.absfree Rtuple' (mk_nthN n Rtuple i));
- in
- mk_Trueprop_eq (lhs, rhs)
- end;
+ fun lsbis_spec i =
+ fold_rev (Term.absfree o Term.dest_Free) (As @ Bs @ ss)
+ (mk_UNION all_sbis (Term.absfree Rtuple' (mk_nthN n Rtuple i)));
val ((lsbis_frees, (_, lsbis_def_frees)), (lthy, lthy_old)) =
lthy
- |> fold_map2 (fn i => fn RT => Specification.definition
- (SOME (lsbis_bind i, NONE, NoSyn), (lsbis_def_bind i, lsbis_spec i RT))) ks setsRTs
+ |> fold_map (fn i => Local_Theory.define
+ ((lsbis_bind i, NoSyn), (lsbis_def_bind i, lsbis_spec i))) ks
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy_old lthy;
- val lsbis_defs = map (Morphism.thm phi) lsbis_def_frees;
+ val lsbis_defs = map (fn def =>
+ mk_unabs_def (live + n) (Morphism.thm phi def RS meta_eq_to_obj_eq)) lsbis_def_frees;
val lsbiss = map (fst o Term.dest_Const o Morphism.term phi) lsbis_frees;
fun mk_lsbis As Bs ss i =
@@ -963,20 +938,18 @@
val Abs_sbdT = Const (#Abs_name sbdT_glob_info, sum_bdT --> sbdT);
val sbd_bind = mk_internal_b sum_bdN;
- val sbd_name = Binding.name_of sbd_bind;
val sbd_def_bind = (Thm.def_binding sbd_bind, []);
- val sbd_spec = HOLogic.mk_Trueprop
- (HOLogic.mk_eq (Free (sbd_name, mk_relT (`I sbdT)), mk_dir_image sum_bd Abs_sbdT));
+ val sbd_spec = mk_dir_image sum_bd Abs_sbdT;
val ((sbd_free, (_, sbd_def_free)), (lthy, lthy_old)) =
lthy
- |> Specification.definition (SOME (sbd_bind, NONE, NoSyn), (sbd_def_bind, sbd_spec))
+ |> Local_Theory.define ((sbd_bind, NoSyn), (sbd_def_bind, sbd_spec))
||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy_old lthy;
- val sbd_def = Morphism.thm phi sbd_def_free;
+ val sbd_def = Morphism.thm phi sbd_def_free RS meta_eq_to_obj_eq;
val sbd = Const (fst (Term.dest_Const (Morphism.term phi sbd_free)), mk_relT (`I sbdT));
val Abs_sbdT_inj = mk_Abs_inj_thm (#Abs_inject sbdT_loc_info);
@@ -1031,12 +1004,10 @@
val root = HOLogic.mk_set sum_sbd_listT [HOLogic.mk_list sum_sbdT []];
val Zero = HOLogic.mk_tuple (map (fn U => absdummy U root) activeAs);
val Lev_recT = fastype_of Zero;
- val LevT = Library.foldr (op -->) (sTs, HOLogic.natT --> Lev_recT);
val Nil = HOLogic.mk_tuple (map3 (fn i => fn z => fn z'=>
Term.absfree z' (mk_InN activeAs z i)) ks zs zs');
val rv_recT = fastype_of Nil;
- val rvT = Library.foldr (op -->) (sTs, sum_sbd_listT --> rv_recT);
val (((((((((((sumx, sumx'), (kks, kks')), (kl, kl')), (kl_copy, kl'_copy)), (Kl, Kl')),
(lab, lab')), (Kl_lab, Kl_lab')), xs), (Lev_rec, Lev_rec')), (rv_rec, rv_rec')),
@@ -1060,7 +1031,6 @@
val isNode_binds = mk_internal_bs isNodeN;
fun isNode_bind i = nth isNode_binds (i - 1);
- val isNode_name = Binding.name_of o isNode_bind;
val isNode_def_bind = rpair [] o Thm.def_binding o isNode_bind;
val isNodeT =
@@ -1073,25 +1043,25 @@
fun isNode_spec sets x i =
let
val (passive_sets, active_sets) = chop m (map (fn set => set $ x) sets);
- val lhs = Term.list_comb (Free (isNode_name i, isNodeT), As @ [Kl, lab, kl]);
val rhs = list_exists_free [x]
(Library.foldr1 HOLogic.mk_conj (HOLogic.mk_eq (lab $ kl, mk_InN bdFTs x i) ::
map2 mk_leq passive_sets As @ map2 (curry HOLogic.mk_eq) active_sets Succs));
in
- mk_Trueprop_eq (lhs, rhs)
+ fold_rev (Term.absfree o Term.dest_Free) (As @ [Kl, lab, kl]) rhs
end;
val ((isNode_frees, (_, isNode_def_frees)), (lthy, lthy_old)) =
lthy
- |> fold_map3 (fn i => fn x => fn sets => Specification.definition
- (SOME (isNode_bind i, NONE, NoSyn), (isNode_def_bind i, isNode_spec sets x i)))
+ |> fold_map3 (fn i => fn x => fn sets => Local_Theory.define
+ ((isNode_bind i, NoSyn), (isNode_def_bind i, isNode_spec sets x i)))
ks xs isNode_setss
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy_old lthy;
- val isNode_defs = map (Morphism.thm phi) isNode_def_frees;
+ val isNode_defs = map (fn def =>
+ mk_unabs_def (m + 3) (Morphism.thm phi def RS meta_eq_to_obj_eq)) isNode_def_frees;
val isNodes = map (fst o Term.dest_Const o Morphism.term phi) isNode_frees;
fun mk_isNode As kl i =
@@ -1120,31 +1090,28 @@
val carT_binds = mk_internal_bs carTN;
fun carT_bind i = nth carT_binds (i - 1);
- val carT_name = Binding.name_of o carT_bind;
val carT_def_bind = rpair [] o Thm.def_binding o carT_bind;
fun carT_spec i =
let
- val carTT = Library.foldr (op -->) (ATs, HOLogic.mk_setT treeT);
-
- val lhs = Term.list_comb (Free (carT_name i, carTT), As);
val rhs = HOLogic.mk_Collect (fst Kl_lab', snd Kl_lab', list_exists_free [Kl, lab]
(HOLogic.mk_conj (HOLogic.mk_eq (Kl_lab, HOLogic.mk_prod (Kl, lab)),
HOLogic.mk_conj (isTree, mk_isNode As (HOLogic.mk_list sum_sbdT []) i))));
in
- mk_Trueprop_eq (lhs, rhs)
+ fold_rev (Term.absfree o Term.dest_Free) As rhs
end;
val ((carT_frees, (_, carT_def_frees)), (lthy, lthy_old)) =
lthy
- |> fold_map (fn i => Specification.definition
- (SOME (carT_bind i, NONE, NoSyn), (carT_def_bind i, carT_spec i))) ks
+ |> fold_map (fn i =>
+ Local_Theory.define ((carT_bind i, NoSyn), (carT_def_bind i, carT_spec i))) ks
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy_old lthy;
- val carT_defs = map (Morphism.thm phi) carT_def_frees;
+ val carT_defs = map (fn def =>
+ mk_unabs_def m (Morphism.thm phi def RS meta_eq_to_obj_eq)) carT_def_frees;
val carTs = map (fst o Term.dest_Const o Morphism.term phi) carT_frees;
fun mk_carT As i = Term.list_comb
@@ -1153,13 +1120,10 @@
val strT_binds = mk_internal_bs strTN;
fun strT_bind i = nth strT_binds (i - 1);
- val strT_name = Binding.name_of o strT_bind;
val strT_def_bind = rpair [] o Thm.def_binding o strT_bind;
fun strT_spec mapFT FT i =
let
- val strTT = treeT --> FT;
-
fun mk_f i k k' =
let val in_k = mk_InN sbdTs k i;
in Term.absfree k' (HOLogic.mk_prod (mk_Shift Kl in_k, mk_shift lab in_k)) end;
@@ -1167,25 +1131,24 @@
val f = Term.list_comb (mapFT, passive_ids @ map3 mk_f ks kks kks');
val (fTs1, fTs2) = apsnd tl (chop (i - 1) (map (fn T => T --> FT) bdFTs));
val fs = map mk_undefined fTs1 @ (f :: map mk_undefined fTs2);
- val lhs = Free (strT_name i, strTT);
- val rhs = HOLogic.mk_split (Term.absfree Kl' (Term.absfree lab'
- (mk_sum_caseN fs $ (lab $ HOLogic.mk_list sum_sbdT []))));
in
- mk_Trueprop_eq (lhs, rhs)
+ HOLogic.mk_split (Term.absfree Kl' (Term.absfree lab'
+ (mk_sum_caseN fs $ (lab $ HOLogic.mk_list sum_sbdT []))))
end;
val ((strT_frees, (_, strT_def_frees)), (lthy, lthy_old)) =
lthy
- |> fold_map3 (fn i => fn mapFT => fn FT => Specification.definition
- (SOME (strT_bind i, NONE, NoSyn), (strT_def_bind i, strT_spec mapFT FT i)))
+ |> fold_map3 (fn i => fn mapFT => fn FT => Local_Theory.define
+ ((strT_bind i, NoSyn), (strT_def_bind i, strT_spec mapFT FT i)))
ks tree_maps treeFTs
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy_old lthy;
- val strT_defs = map ((fn def => trans OF [def RS fun_cong, @{thm prod.cases}]) o
- Morphism.thm phi) strT_def_frees;
+ val strT_defs = map (fn def =>
+ trans OF [Morphism.thm phi def RS meta_eq_to_obj_eq RS fun_cong, @{thm prod.cases}])
+ strT_def_frees;
val strTs = map (fst o Term.dest_Const o Morphism.term phi) strT_frees;
fun mk_strT FT i = Const (nth strTs (i - 1), treeT --> FT);
@@ -1215,7 +1178,6 @@
val from_to_sbd_thmss = mk_to_sbd_thmss @{thm fromCard_toCard};
val Lev_bind = mk_internal_b LevN;
- val Lev_name = Binding.name_of Lev_bind;
val Lev_def_bind = rpair [] (Thm.def_binding Lev_bind);
val Lev_spec =
@@ -1240,20 +1202,19 @@
val Suc = Term.absdummy HOLogic.natT (Term.absfree Lev_rec'
(HOLogic.mk_tuple (map5 mk_Suc ks ss setssAs zs zs')));
- val lhs = Term.list_comb (Free (Lev_name, LevT), ss);
val rhs = mk_nat_rec Zero Suc;
in
- mk_Trueprop_eq (lhs, rhs)
+ fold_rev (Term.absfree o Term.dest_Free) ss rhs
end;
val ((Lev_free, (_, Lev_def_free)), (lthy, lthy_old)) =
lthy
- |> Specification.definition (SOME (Lev_bind, NONE, NoSyn), (Lev_def_bind, Lev_spec))
+ |> Local_Theory.define ((Lev_bind, NoSyn), (Lev_def_bind, Lev_spec))
||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy_old lthy;
- val Lev_def = Morphism.thm phi Lev_def_free;
+ val Lev_def = mk_unabs_def n (Morphism.thm phi Lev_def_free RS meta_eq_to_obj_eq);
val Lev = fst (Term.dest_Const (Morphism.term phi Lev_free));
fun mk_Lev ss nat i =
@@ -1269,7 +1230,6 @@
val Lev_Sucs = flat (mk_rec_simps n @{thm nat_rec_Suc_imp} [Lev_def]);
val rv_bind = mk_internal_b rvN;
- val rv_name = Binding.name_of rv_bind;
val rv_def_bind = rpair [] (Thm.def_binding rv_bind);
val rv_spec =
@@ -1285,20 +1245,19 @@
val Cons = Term.absfree sumx' (Term.absdummy sum_sbd_listT (Term.absfree rv_rec'
(HOLogic.mk_tuple (map4 mk_Cons ks ss zs zs'))));
- val lhs = Term.list_comb (Free (rv_name, rvT), ss);
val rhs = mk_list_rec Nil Cons;
in
- mk_Trueprop_eq (lhs, rhs)
+ fold_rev (Term.absfree o Term.dest_Free) ss rhs
end;
val ((rv_free, (_, rv_def_free)), (lthy, lthy_old)) =
lthy
- |> Specification.definition (SOME (rv_bind, NONE, NoSyn), (rv_def_bind, rv_spec))
+ |> Local_Theory.define ((rv_bind, NoSyn), (rv_def_bind, rv_spec))
||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy_old lthy;
- val rv_def = Morphism.thm phi rv_def_free;
+ val rv_def = mk_unabs_def n (Morphism.thm phi rv_def_free RS meta_eq_to_obj_eq);
val rv = fst (Term.dest_Const (Morphism.term phi rv_free));
fun mk_rv ss kl i =
@@ -1316,13 +1275,10 @@
val beh_binds = mk_internal_bs behN;
fun beh_bind i = nth beh_binds (i - 1);
- val beh_name = Binding.name_of o beh_bind;
val beh_def_bind = rpair [] o Thm.def_binding o beh_bind;
fun beh_spec i z =
let
- val mk_behT = Library.foldr (op -->) (map fastype_of (ss @ [z]), treeT);
-
fun mk_case i to_sbd_map s k k' =
Term.absfree k' (mk_InN bdFTs
(Term.list_comb (to_sbd_map, passive_ids @ map (mk_to_sbd s k i) ks) $ (s $ k)) i);
@@ -1332,23 +1288,23 @@
(mk_sum_caseN (map5 mk_case ks to_sbd_maps ss zs zs') $ (mk_rv ss kl i $ z))
(mk_undefined sbdFT));
- val lhs = Term.list_comb (Free (beh_name i, mk_behT), ss) $ z;
val rhs = HOLogic.mk_prod (mk_UNION (HOLogic.mk_UNIV HOLogic.natT)
(Term.absfree nat' (mk_Lev ss nat i $ z)), Lab);
in
- mk_Trueprop_eq (lhs, rhs)
+ fold_rev (Term.absfree o Term.dest_Free) (ss @ [z]) rhs
end;
val ((beh_frees, (_, beh_def_frees)), (lthy, lthy_old)) =
lthy
- |> fold_map2 (fn i => fn z => Specification.definition
- (SOME (beh_bind i, NONE, NoSyn), (beh_def_bind i, beh_spec i z))) ks zs
+ |> fold_map2 (fn i => fn z =>
+ Local_Theory.define ((beh_bind i, NoSyn), (beh_def_bind i, beh_spec i z))) ks zs
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy_old lthy;
- val beh_defs = map (Morphism.thm phi) beh_def_frees;
+ val beh_defs = map (fn def =>
+ mk_unabs_def (n + 1) (Morphism.thm phi def RS meta_eq_to_obj_eq)) beh_def_frees;
val behs = map (fst o Term.dest_Const o Morphism.term phi) beh_frees;
fun mk_beh ss i =
@@ -1651,8 +1607,6 @@
mk_map_of_bnf Ds (passiveAs @ prodTs) (passiveAs @ Ts)) Dss bnfs;
val fstsTs = map fst_const prodTs;
val sndsTs = map snd_const prodTs;
- val dtorTs = map2 (curry op -->) Ts FTs;
- val ctorTs = map2 (curry op -->) FTs Ts;
val unfold_fTs = map2 (curry op -->) activeAs Ts;
val corec_sTs = map (Term.typ_subst_atomic (activeBs ~~ Ts)) sum_sTs;
val corec_maps = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_Inls;
@@ -1677,25 +1631,18 @@
||>> mk_Freess "P" (map (fn A => map (mk_pred2T A) Ts) passiveAs);
fun dtor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtorN ^ "_");
- val dtor_name = Binding.name_of o dtor_bind;
val dtor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o dtor_bind;
- fun dtor_spec i rep str map_FT dtorT Jz Jz' =
- let
- val lhs = Free (dtor_name i, dtorT);
- val rhs = Term.absfree Jz'
- (Term.list_comb (map_FT, map HOLogic.id_const passiveAs @ Abs_Ts) $
- (str $ (rep $ Jz)));
- in
- mk_Trueprop_eq (lhs, rhs)
- end;
+ fun dtor_spec rep str map_FT Jz Jz' =
+ Term.absfree Jz'
+ (Term.list_comb (map_FT, map HOLogic.id_const passiveAs @ Abs_Ts) $ (str $ (rep $ Jz)));
val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) =
lthy
- |> fold_map7 (fn i => fn rep => fn str => fn mapx => fn dtorT => fn Jz => fn Jz' =>
- Specification.definition (SOME (dtor_bind i, NONE, NoSyn),
- (dtor_def_bind i, dtor_spec i rep str mapx dtorT Jz Jz')))
- ks Rep_Ts str_finals map_FTs dtorTs Jzs Jzs'
+ |> fold_map6 (fn i => fn rep => fn str => fn mapx => fn Jz => fn Jz' =>
+ Local_Theory.define ((dtor_bind i, NoSyn),
+ (dtor_def_bind i, dtor_spec rep str mapx Jz Jz')))
+ ks Rep_Ts str_finals map_FTs Jzs Jzs'
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
@@ -1705,7 +1652,8 @@
Morphism.term phi) dtor_frees;
val dtors = mk_dtors passiveAs;
val dtor's = mk_dtors passiveBs;
- val dtor_defs = map ((fn thm => thm RS fun_cong) o Morphism.thm phi) dtor_def_frees;
+ val dtor_defs = map (fn def =>
+ Morphism.thm phi def RS meta_eq_to_obj_eq RS fun_cong) dtor_def_frees;
val coalg_final_set_thmss = map (map (fn thm => coalg_final_thm RS thm)) coalg_set_thmss;
val (mor_Rep_thm, mor_Abs_thm) =
@@ -1730,26 +1678,16 @@
val timer = time (timer "dtor definitions & thms");
fun unfold_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtor_unfoldN ^ "_");
- val unfold_name = Binding.name_of o unfold_bind;
val unfold_def_bind = rpair [] o Binding.conceal o Thm.def_binding o unfold_bind;
- fun unfold_spec i T AT abs f z z' =
- let
- val unfoldT = Library.foldr (op -->) (sTs, AT --> T);
-
- val lhs = Term.list_comb (Free (unfold_name i, unfoldT), ss);
- val rhs = Term.absfree z' (abs $ (f $ z));
- in
- mk_Trueprop_eq (lhs, rhs)
- end;
+ fun unfold_spec abs f z = fold_rev (Term.absfree o Term.dest_Free) (ss @ [z]) (abs $ (f $ z));
val ((unfold_frees, (_, unfold_def_frees)), (lthy, lthy_old)) =
lthy
- |> fold_map7 (fn i => fn T => fn AT => fn abs => fn f => fn z => fn z' =>
- Specification.definition
- (SOME (unfold_bind i, NONE, NoSyn), (unfold_def_bind i, unfold_spec i T AT abs f z z')))
- ks Ts activeAs Abs_Ts (map (fn i => HOLogic.mk_comp
- (mk_proj (mk_LSBIS passive_UNIVs i), mk_beh ss i)) ks) zs zs'
+ |> fold_map4 (fn i => fn abs => fn f => fn z =>
+ Local_Theory.define ((unfold_bind i, NoSyn), (unfold_def_bind i, unfold_spec abs f z)))
+ ks Abs_Ts (map (fn i => HOLogic.mk_comp
+ (mk_proj (mk_LSBIS passive_UNIVs i), mk_beh ss i)) ks) zs
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
@@ -1763,7 +1701,8 @@
unfold_names (mk_Ts passives) actives;
fun mk_unfold Ts ss i = Term.list_comb (Const (nth unfold_names (i - 1), Library.foldr (op -->)
(map fastype_of ss, domain_type (fastype_of (nth ss (i - 1))) --> nth Ts (i - 1))), ss);
- val unfold_defs = map ((fn thm => thm RS fun_cong) o Morphism.thm phi) unfold_def_frees;
+ val unfold_defs = map (fn def =>
+ mk_unabs_def (n + 1) (Morphism.thm phi def RS meta_eq_to_obj_eq)) unfold_def_frees;
val mor_unfold_thm =
let
@@ -1832,22 +1771,14 @@
map HOLogic.id_const passiveAs @ dtors)) Dss bnfs;
fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_");
- val ctor_name = Binding.name_of o ctor_bind;
val ctor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o ctor_bind;
- fun ctor_spec i ctorT =
- let
- val lhs = Free (ctor_name i, ctorT);
- val rhs = mk_unfold Ts map_dtors i;
- in
- mk_Trueprop_eq (lhs, rhs)
- end;
+ fun ctor_spec i = mk_unfold Ts map_dtors i;
val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) =
lthy
- |> fold_map2 (fn i => fn ctorT =>
- Specification.definition
- (SOME (ctor_bind i, NONE, NoSyn), (ctor_def_bind i, ctor_spec i ctorT))) ks ctorTs
+ |> fold_map (fn i =>
+ Local_Theory.define ((ctor_bind i, NoSyn), (ctor_def_bind i, ctor_spec i))) ks
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
@@ -1856,7 +1787,7 @@
map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ params) o Morphism.term phi)
ctor_frees;
val ctors = mk_ctors params';
- val ctor_defs = map (Morphism.thm phi) ctor_def_frees;
+ val ctor_defs = map (fn def => Morphism.thm phi def RS meta_eq_to_obj_eq) ctor_def_frees;
val ctor_o_dtor_thms = map2 (fold_thms lthy o single) ctor_defs unfold_o_dtor_thms;
@@ -1904,7 +1835,6 @@
end;
fun corec_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtor_corecN ^ "_");
- val corec_name = Binding.name_of o corec_bind;
val corec_def_bind = rpair [] o Binding.conceal o Thm.def_binding o corec_bind;
val corec_strs =
@@ -1914,20 +1844,13 @@
dtors corec_ss corec_maps;
fun corec_spec i T AT =
- let
- val corecT = Library.foldr (op -->) (corec_sTs, AT --> T);
-
- val lhs = Term.list_comb (Free (corec_name i, corecT), corec_ss);
- val rhs = HOLogic.mk_comp (mk_unfold Ts corec_strs i, Inr_const T AT);
- in
- mk_Trueprop_eq (lhs, rhs)
- end;
+ fold_rev (Term.absfree o Term.dest_Free) corec_ss
+ (HOLogic.mk_comp (mk_unfold Ts corec_strs i, Inr_const T AT));
val ((corec_frees, (_, corec_def_frees)), (lthy, lthy_old)) =
lthy
|> fold_map3 (fn i => fn T => fn AT =>
- Specification.definition
- (SOME (corec_bind i, NONE, NoSyn), (corec_def_bind i, corec_spec i T AT)))
+ Local_Theory.define ((corec_bind i, NoSyn), (corec_def_bind i, corec_spec i T AT)))
ks Ts activeAs
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
@@ -1937,7 +1860,8 @@
val corec_names = map (fst o dest_Const) corecs;
fun mk_corec ss i = Term.list_comb (Const (nth corec_names (i - 1), Library.foldr (op -->)
(map fastype_of ss, domain_type (fastype_of (nth ss (i - 1))) --> nth Ts (i - 1))), ss);
- val corec_defs = map (Morphism.thm phi) corec_def_frees;
+ val corec_defs = map (fn def =>
+ mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) corec_def_frees;
val sum_cases =
map2 (fn T => fn i => mk_sum_case (HOLogic.id_const T, mk_corec corec_ss i)) Ts ks;
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Fri Jan 31 13:42:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Fri Jan 31 13:45:39 2014 +0100
@@ -244,32 +244,28 @@
(* algebra *)
val alg_bind = mk_internal_b algN;
- val alg_name = Binding.name_of alg_bind;
val alg_def_bind = (Thm.def_binding alg_bind, []);
(*forall i = 1 ... n: (\<forall>x \<in> Fi_in A1 .. Am B1 ... Bn. si x \<in> Bi)*)
val alg_spec =
let
- val algT = Library.foldr (op -->) (ATs @ BTs @ sTs, HOLogic.boolT);
-
val ins = map3 mk_in (replicate n (As @ Bs)) setssAs FTsAs;
fun mk_alg_conjunct B s X x x' =
mk_Ball X (Term.absfree x' (HOLogic.mk_mem (s $ x, B)));
- val lhs = Term.list_comb (Free (alg_name, algT), As @ Bs @ ss);
val rhs = Library.foldr1 HOLogic.mk_conj (map5 mk_alg_conjunct Bs ss ins xFs xFs')
in
- mk_Trueprop_eq (lhs, rhs)
+ fold_rev (Term.absfree o Term.dest_Free) (As @ Bs @ ss) rhs
end;
val ((alg_free, (_, alg_def_free)), (lthy, lthy_old)) =
lthy
- |> Specification.definition (SOME (alg_bind, NONE, NoSyn), (alg_def_bind, alg_spec))
+ |> Local_Theory.define ((alg_bind, NoSyn), (alg_def_bind, alg_spec))
||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy_old lthy;
val alg = fst (Term.dest_Const (Morphism.term phi alg_free));
- val alg_def = Morphism.thm phi alg_def_free;
+ val alg_def = mk_unabs_def (live + n) (Morphism.thm phi alg_def_free RS meta_eq_to_obj_eq);
fun mk_alg As Bs ss =
let
@@ -331,7 +327,6 @@
(* morphism *)
val mor_bind = mk_internal_b morN;
- val mor_name = Binding.name_of mor_bind;
val mor_def_bind = (Thm.def_binding mor_bind, []);
(*fbetw) forall i = 1 ... n: (\<forall>x \<in> Bi. f x \<in> B'i)*)
@@ -339,31 +334,28 @@
f (s1 x) = s1' (Fi_map id ... id f1 ... fn x))*)
val mor_spec =
let
- val morT = Library.foldr (op -->) (BTs @ sTs @ B'Ts @ s'Ts @ fTs, HOLogic.boolT);
-
fun mk_fbetw f B1 B2 z z' =
mk_Ball B1 (Term.absfree z' (HOLogic.mk_mem (f $ z, B2)));
fun mk_mor sets mapAsBs f s s' T x x' =
mk_Ball (mk_in (passive_UNIVs @ Bs) sets T)
(Term.absfree x' (HOLogic.mk_eq (f $ (s $ x), s' $
(Term.list_comb (mapAsBs, passive_ids @ fs) $ x))));
- val lhs = Term.list_comb (Free (mor_name, morT), Bs @ ss @ B's @ s's @ fs);
val rhs = HOLogic.mk_conj
(Library.foldr1 HOLogic.mk_conj (map5 mk_fbetw fs Bs B's zs zs'),
Library.foldr1 HOLogic.mk_conj
(map8 mk_mor setssAs mapsAsBs fs ss s's FTsAs xFs xFs'))
in
- mk_Trueprop_eq (lhs, rhs)
+ fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss @ B's @ s's @ fs) rhs
end;
val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) =
lthy
- |> Specification.definition (SOME (mor_bind, NONE, NoSyn), (mor_def_bind, mor_spec))
+ |> Local_Theory.define ((mor_bind, NoSyn), (mor_def_bind, mor_spec))
||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy_old lthy;
val mor = fst (Term.dest_Const (Morphism.term phi mor_free));
- val mor_def = Morphism.thm phi mor_def_free;
+ val mor_def = mk_unabs_def (5 * n) (Morphism.thm phi mor_def_free RS meta_eq_to_obj_eq);
fun mk_mor Bs1 ss1 Bs2 ss2 fs =
let
@@ -719,31 +711,27 @@
val min_alg_binds = mk_internal_bs min_algN;
fun min_alg_bind i = nth min_alg_binds (i - 1);
- fun min_alg_name i = Binding.name_of (min_alg_bind i);
val min_alg_def_bind = rpair [] o Thm.def_binding o min_alg_bind;
fun min_alg_spec i =
let
- val min_algT =
- Library.foldr (op -->) (ATs @ sTs, HOLogic.mk_setT (nth activeAs (i - 1)));
-
- val lhs = Term.list_comb (Free (min_alg_name i, min_algT), As @ ss);
val rhs = mk_UNION (field_suc_bd)
(Term.absfree idx' (mk_nthN n (mk_min_algs As ss $ idx) i));
in
- mk_Trueprop_eq (lhs, rhs)
+ fold_rev (Term.absfree o Term.dest_Free) (As @ ss) rhs
end;
val ((min_alg_frees, (_, min_alg_def_frees)), (lthy, lthy_old)) =
lthy
- |> fold_map (fn i => Specification.definition
- (SOME (min_alg_bind i, NONE, NoSyn), (min_alg_def_bind i, min_alg_spec i))) ks
+ |> fold_map (fn i => Local_Theory.define
+ ((min_alg_bind i, NoSyn), (min_alg_def_bind i, min_alg_spec i))) ks
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy_old lthy;
val min_algs = map (fst o Term.dest_Const o Morphism.term phi) min_alg_frees;
- val min_alg_defs = map (Morphism.thm phi) min_alg_def_frees;
+ val min_alg_defs = map (fn def =>
+ mk_unabs_def live (Morphism.thm phi def RS meta_eq_to_obj_eq)) min_alg_def_frees;
fun mk_min_alg As ss i =
let
@@ -832,30 +820,25 @@
val str_init_binds = mk_internal_bs str_initN;
fun str_init_bind i = nth str_init_binds (i - 1);
- val str_init_name = Binding.name_of o str_init_bind;
val str_init_def_bind = rpair [] o Thm.def_binding o str_init_bind;
fun str_init_spec i =
let
- val T = nth init_FTs (i - 1);
val init_xF = nth init_xFs (i - 1)
val select_s = nth select_ss (i - 1);
val map = mk_map_of_bnf (nth Dss (i - 1))
(passiveAs @ active_initTs) (passiveAs @ replicate n Asuc_bdT)
(nth bnfs (i - 1));
val map_args = passive_ids @ replicate n (mk_rapp iidx Asuc_bdT);
- val str_initT = T --> IIT --> Asuc_bdT;
-
- val lhs = Term.list_comb (Free (str_init_name i, str_initT), [init_xF, iidx]);
val rhs = select_s $ (Term.list_comb (map, map_args) $ init_xF);
in
- mk_Trueprop_eq (lhs, rhs)
+ fold_rev (Term.absfree o Term.dest_Free) [init_xF, iidx] rhs
end;
val ((str_init_frees, (_, str_init_def_frees)), (lthy, lthy_old)) =
lthy
- |> fold_map (fn i => Specification.definition
- (SOME (str_init_bind i, NONE, NoSyn), (str_init_def_bind i, str_init_spec i))) ks
+ |> fold_map (fn i => Local_Theory.define
+ ((str_init_bind i, NoSyn), (str_init_def_bind i, str_init_spec i))) ks
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
@@ -864,7 +847,8 @@
map (Term.subst_atomic_types (map (`(Morphism.typ phi)) params') o Morphism.term phi)
str_init_frees;
- val str_init_defs = map (Morphism.thm phi) str_init_def_frees;
+ val str_init_defs = map (fn def =>
+ mk_unabs_def 2 (Morphism.thm phi def RS meta_eq_to_obj_eq)) str_init_def_frees;
val car_inits = map (mk_min_alg passive_UNIVs str_inits) ks;
@@ -1024,25 +1008,17 @@
val phi2s = map2 retype_free (map2 mk_pred2T Ts Ts') init_phis;
fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_");
- val ctor_name = Binding.name_of o ctor_bind;
val ctor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o ctor_bind;
- fun ctor_spec i abs str map_FT_init x x' =
- let
- val ctorT = nth FTs (i - 1) --> nth Ts (i - 1);
-
- val lhs = Free (ctor_name i, ctorT);
- val rhs = Term.absfree x' (abs $ (str $
+ fun ctor_spec abs str map_FT_init x x' =
+ Term.absfree x' (abs $ (str $
(Term.list_comb (map_FT_init, map HOLogic.id_const passiveAs @ Rep_Ts) $ x)));
- in
- mk_Trueprop_eq (lhs, rhs)
- end;
val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) =
lthy
|> fold_map6 (fn i => fn abs => fn str => fn mapx => fn x => fn x' =>
- Specification.definition
- (SOME (ctor_bind i, NONE, NoSyn), (ctor_def_bind i, ctor_spec i abs str mapx x x')))
+ Local_Theory.define
+ ((ctor_bind i, NoSyn), (ctor_def_bind i, ctor_spec abs str mapx x x')))
ks Abs_Ts str_inits map_FT_inits xFs xFs'
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
@@ -1053,7 +1029,7 @@
Morphism.term phi) ctor_frees;
val ctors = mk_ctors passiveAs;
val ctor's = mk_ctors passiveBs;
- val ctor_defs = map (Morphism.thm phi) ctor_def_frees;
+ val ctor_defs = map (fn def => Morphism.thm phi def RS meta_eq_to_obj_eq) ctor_def_frees;
val (mor_Rep_thm, mor_Abs_thm) =
let
@@ -1084,25 +1060,14 @@
val foldx = HOLogic.choice_const foldT $ fold_fun;
fun fold_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctor_foldN ^ "_");
- val fold_name = Binding.name_of o fold_bind;
val fold_def_bind = rpair [] o Binding.conceal o Thm.def_binding o fold_bind;
- fun fold_spec i T AT =
- let
- val foldT = Library.foldr (op -->) (sTs, T --> AT);
-
- val lhs = Term.list_comb (Free (fold_name i, foldT), ss);
- val rhs = mk_nthN n foldx i;
- in
- mk_Trueprop_eq (lhs, rhs)
- end;
+ fun fold_spec i = fold_rev (Term.absfree o Term.dest_Free) ss (mk_nthN n foldx i);
val ((fold_frees, (_, fold_def_frees)), (lthy, lthy_old)) =
lthy
- |> fold_map3 (fn i => fn T => fn AT =>
- Specification.definition
- (SOME (fold_bind i, NONE, NoSyn), (fold_def_bind i, fold_spec i T AT)))
- ks Ts activeAs
+ |> fold_map (fn i =>
+ Local_Theory.define ((fold_bind i, NoSyn), (fold_def_bind i, fold_spec i))) ks
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
@@ -1116,7 +1081,8 @@
fold_names (mk_Ts passives) actives;
fun mk_fold Ts ss i = Term.list_comb (Const (nth fold_names (i - 1), Library.foldr (op -->)
(map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss);
- val fold_defs = map (Morphism.thm phi) fold_def_frees;
+ val fold_defs = map (fn def =>
+ mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) fold_def_frees;
val mor_fold_thm =
let
@@ -1174,24 +1140,14 @@
map HOLogic.id_const passiveAs @ ctors)) Dss bnfs;
fun dtor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtorN ^ "_");
- val dtor_name = Binding.name_of o dtor_bind;
val dtor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o dtor_bind;
- fun dtor_spec i FT T =
- let
- val dtorT = T --> FT;
-
- val lhs = Free (dtor_name i, dtorT);
- val rhs = mk_fold Ts map_ctors i;
- in
- mk_Trueprop_eq (lhs, rhs)
- end;
+ fun dtor_spec i = mk_fold Ts map_ctors i;
val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) =
lthy
- |> fold_map3 (fn i => fn FT => fn T =>
- Specification.definition
- (SOME (dtor_bind i, NONE, NoSyn), (dtor_def_bind i, dtor_spec i FT T))) ks FTs Ts
+ |> fold_map (fn i =>
+ Local_Theory.define ((dtor_bind i, NoSyn), (dtor_def_bind i, dtor_spec i))) ks
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
@@ -1200,7 +1156,7 @@
map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ params) o Morphism.term phi)
dtor_frees;
val dtors = mk_dtors params';
- val dtor_defs = map (Morphism.thm phi) dtor_def_frees;
+ val dtor_defs = map (fn def => Morphism.thm phi def RS meta_eq_to_obj_eq) dtor_def_frees;
val ctor_o_dtor_thms = map2 (fold_thms lthy o single) dtor_defs ctor_o_fold_thms;
@@ -1247,7 +1203,6 @@
end;
fun rec_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctor_recN ^ "_");
- val rec_name = Binding.name_of o rec_bind;
val rec_def_bind = rpair [] o Binding.conceal o Thm.def_binding o rec_bind;
val rec_strs =
@@ -1256,21 +1211,13 @@
ctors rec_ss rec_maps;
fun rec_spec i T AT =
- let
- val recT = Library.foldr (op -->) (rec_sTs, T --> AT);
-
- val lhs = Term.list_comb (Free (rec_name i, recT), rec_ss);
- val rhs = HOLogic.mk_comp (snd_const (HOLogic.mk_prodT (T, AT)), mk_fold Ts rec_strs i);
- in
- mk_Trueprop_eq (lhs, rhs)
- end;
+ fold_rev (Term.absfree o Term.dest_Free) rec_ss
+ (HOLogic.mk_comp (snd_const (HOLogic.mk_prodT (T, AT)), mk_fold Ts rec_strs i));
val ((rec_frees, (_, rec_def_frees)), (lthy, lthy_old)) =
lthy
|> fold_map3 (fn i => fn T => fn AT =>
- Specification.definition
- (SOME (rec_bind i, NONE, NoSyn), (rec_def_bind i, rec_spec i T AT)))
- ks Ts activeAs
+ Local_Theory.define ((rec_bind i, NoSyn), (rec_def_bind i, rec_spec i T AT))) ks Ts activeAs
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
@@ -1279,7 +1226,8 @@
val rec_names = map (fst o dest_Const) recs;
fun mk_rec ss i = Term.list_comb (Const (nth rec_names (i - 1), Library.foldr (op -->)
(map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss);
- val rec_defs = map (Morphism.thm phi) rec_def_frees;
+ val rec_defs = map (fn def =>
+ mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) rec_def_frees;
val convols = map2 (fn T => fn i => mk_convol (HOLogic.id_const T, mk_rec rec_ss i)) Ts ks;
val ctor_rec_thms =