--- a/src/HOL/Tools/BNF/bnf_gfp.ML Tue Feb 18 01:11:25 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Tue Feb 18 14:51:26 2014 +0100
@@ -163,8 +163,8 @@
HOLogic.mk_tuple (map (fn U => absdummy U empty) activeAs)) emptys;
val hrecTs = map fastype_of Zeros;
- 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),
+ val ((((((((((((((((((((((((((((((((((zs, zs'), zs_copy), zs_copy2), z's), (ys, ys')),
+ Bs), Bs_copy), B's), B''s), ss), sum_ss), s's), s''s), fs), fs_copy),
self_fs), gs), all_gs), xFs), yFs), yFs_copy), RFs), (Rtuple, Rtuple')), (hrecs, hrecs')),
(nat, nat')), Rs), Rs_copy), R's), sRs), (idx, idx')), Idx), Ris), Kss), names_lthy) = lthy
|> mk_Frees' "b" activeAs
@@ -172,7 +172,6 @@
||>> mk_Frees "b" activeAs
||>> mk_Frees "b" activeBs
||>> mk_Frees' "y" passiveAs
- ||>> mk_Frees "A" ATs
||>> mk_Frees "B" BTs
||>> mk_Frees "B" BTs
||>> mk_Frees "B'" B'Ts
@@ -203,7 +202,7 @@
||>> mk_Freess "K" (map (fn AT => map (fn T => T --> AT) activeAs) ATs);
val passive_UNIVs = map HOLogic.mk_UNIV passiveAs;
- val passive_Id_ons = map mk_Id_on As;
+ val passive_eqs = map HOLogic.eq_const passiveAs;
val active_UNIVs = map HOLogic.mk_UNIV activeAs;
val sum_UNIVs = map HOLogic.mk_UNIV sumBsAs;
val passive_ids = map HOLogic.id_const passiveAs;
@@ -297,16 +296,16 @@
val coalg_bind = mk_internal_b (coN ^ algN) ;
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)*)
+ (*forall i = 1 ... n: (\<forall>x \<in> Bi. si \<in> Fi_in UNIV .. UNIV B1 ... Bn)*)
val coalg_spec =
let
- val ins = map3 mk_in (replicate n (As @ Bs)) setssAs FTsAs;
+ val ins = map3 mk_in (replicate n (passive_UNIVs @ 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 rhs = Library.foldr1 HOLogic.mk_conj (map5 mk_coalg_conjunct Bs ss ins zs zs')
in
- fold_rev (Term.absfree o Term.dest_Free) (As @ Bs @ ss) rhs
+ fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss) rhs
end;
val ((coalg_free, (_, coalg_def_free)), (lthy, lthy_old)) =
@@ -316,44 +315,44 @@
val phi = Proof_Context.export_morphism lthy_old lthy;
val coalg = fst (Term.dest_Const (Morphism.term phi coalg_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 =
+ val coalg_def = mk_unabs_def (2 * n) (Morphism.thm phi coalg_def_free RS meta_eq_to_obj_eq);
+
+ fun mk_coalg Bs ss =
let
- val args = As @ Bs @ ss;
+ val args = Bs @ ss;
val Ts = map fastype_of args;
val coalgT = Library.foldr (op -->) (Ts, HOLogic.boolT);
in
Term.list_comb (Const (coalg, coalgT), args)
end;
- val coalg_prem = HOLogic.mk_Trueprop (mk_coalg As Bs ss);
+ val coalg_prem = HOLogic.mk_Trueprop (mk_coalg Bs ss);
val coalg_in_thms = map (fn i =>
coalg_def RS iffD1 RS mk_conjunctN n i RS bspec) ks
val coalg_set_thmss =
let
- val coalg_prem = HOLogic.mk_Trueprop (mk_coalg As Bs ss);
+ val coalg_prem = HOLogic.mk_Trueprop (mk_coalg Bs ss);
fun mk_prem x B = HOLogic.mk_Trueprop (HOLogic.mk_mem (x, B));
fun mk_concl s x B set = HOLogic.mk_Trueprop (mk_leq (set $ (s $ x)) B);
val prems = map2 mk_prem zs Bs;
- val conclss = map3 (fn s => fn x => fn sets => map2 (mk_concl s x) (As @ Bs) sets)
+ val conclss = map3 (fn s => fn x => fn sets => map2 (mk_concl s x) Bs (drop m sets))
ss zs setssAs;
val goalss = map3 (fn x => fn prem => fn concls => map (fn concl =>
- fold_rev Logic.all (x :: As @ Bs @ ss)
+ fold_rev Logic.all (x :: Bs @ ss)
(Logic.list_implies (coalg_prem :: [prem], concl))) concls) zs prems conclss;
in
map (fn goals => map (fn goal => Goal.prove_sorry lthy [] [] goal
(K (mk_coalg_set_tac coalg_def)) |> Thm.close_derivation) goals) goalss
end;
- fun mk_tcoalg ATs BTs = mk_coalg (map HOLogic.mk_UNIV ATs) (map HOLogic.mk_UNIV BTs);
+ fun mk_tcoalg BTs = mk_coalg (map HOLogic.mk_UNIV BTs);
val tcoalg_thm =
let
val goal = fold_rev Logic.all ss
- (HOLogic.mk_Trueprop (mk_tcoalg passiveAs activeAs ss))
+ (HOLogic.mk_Trueprop (mk_tcoalg activeAs ss))
in
Goal.prove_sorry lthy [] [] goal
(K (stac coalg_def 1 THEN CONJ_WRAP
@@ -719,8 +718,8 @@
fun mk_bis R s s' b1 b2 RF map1 map2 sets =
list_all_free [b1, b2] (HOLogic.mk_imp
(HOLogic.mk_mem (HOLogic.mk_prod (b1, b2), R),
- mk_Bex (mk_in (As @ Rs) sets (snd (dest_Free RF))) (Term.absfree (dest_Free RF)
- (HOLogic.mk_conj
+ mk_Bex (mk_in (passive_UNIVs @ Rs) sets (snd (dest_Free RF)))
+ (Term.absfree (dest_Free RF) (HOLogic.mk_conj
(HOLogic.mk_eq (Term.list_comb (map1, fst_args) $ RF, s $ b1),
HOLogic.mk_eq (Term.list_comb (map2, snd_args) $ RF, s' $ b2))))));
@@ -728,7 +727,7 @@
(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
- fold_rev (Term.absfree o Term.dest_Free) (As @ Bs @ ss @ B's @ s's @ Rs) rhs
+ fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss @ B's @ s's @ Rs) rhs
end;
val ((bis_free, (_, bis_def_free)), (lthy, lthy_old)) =
@@ -738,11 +737,11 @@
val phi = Proof_Context.export_morphism lthy_old lthy;
val bis = fst (Term.dest_Const (Morphism.term phi bis_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 =
+ val bis_def = mk_unabs_def (5 * n) (Morphism.thm phi bis_def_free RS meta_eq_to_obj_eq);
+
+ fun mk_bis Bs1 ss1 Bs2 ss2 Rs =
let
- val args = As @ Bs1 @ ss1 @ Bs2 @ ss2 @ Rs;
+ val args = Bs1 @ ss1 @ Bs2 @ ss2 @ Rs;
val Ts = map fastype_of args;
val bisT = Library.foldr (op -->) (Ts, HOLogic.boolT);
in
@@ -752,11 +751,11 @@
val bis_cong_thm =
let
val prems = map HOLogic.mk_Trueprop
- (mk_bis As Bs ss B's s's Rs :: map2 (curry HOLogic.mk_eq) Rs_copy Rs)
- val concl = HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's Rs_copy);
+ (mk_bis Bs ss B's s's Rs :: map2 (curry HOLogic.mk_eq) Rs_copy Rs)
+ val concl = HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs_copy);
in
Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs @ Rs_copy)
+ (fold_rev Logic.all (Bs @ ss @ B's @ s's @ Rs @ Rs_copy)
(Logic.list_implies (prems, concl)))
(K ((hyp_subst_tac lthy THEN' atac) 1))
|> Thm.close_derivation
@@ -767,38 +766,38 @@
fun mk_conjunct R s s' b1 b2 rel =
list_all_free [b1, b2] (HOLogic.mk_imp
(HOLogic.mk_mem (HOLogic.mk_prod (b1, b2), R),
- Term.list_comb (rel, map mk_in_rel (passive_Id_ons @ Rs)) $ (s $ b1) $ (s' $ b2)));
+ Term.list_comb (rel, passive_eqs @ map mk_in_rel Rs) $ (s $ b1) $ (s' $ b2)));
val rhs = HOLogic.mk_conj
(bis_le, Library.foldr1 HOLogic.mk_conj
(map6 mk_conjunct Rs ss s's zs z's relsAsBs))
in
Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs)
- (mk_Trueprop_eq (mk_bis As Bs ss B's s's Rs, rhs)))
+ (fold_rev Logic.all (Bs @ ss @ B's @ s's @ Rs)
+ (mk_Trueprop_eq (mk_bis Bs ss B's s's Rs, rhs)))
(K (mk_bis_rel_tac lthy m bis_def rel_OO_Grps map_comps map_cong0s set_mapss))
|> Thm.close_derivation
end;
val bis_converse_thm =
Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs)
+ (fold_rev Logic.all (Bs @ ss @ B's @ s's @ Rs)
(Logic.mk_implies
- (HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's Rs),
- HOLogic.mk_Trueprop (mk_bis As B's s's Bs ss (map mk_converse Rs)))))
+ (HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs),
+ HOLogic.mk_Trueprop (mk_bis B's s's Bs ss (map mk_converse Rs)))))
(K (mk_bis_converse_tac m bis_rel_thm rel_congs rel_converseps))
|> Thm.close_derivation;
val bis_O_thm =
let
val prems =
- [HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's Rs),
- HOLogic.mk_Trueprop (mk_bis As B's s's B''s s''s R's)];
+ [HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs),
+ HOLogic.mk_Trueprop (mk_bis B's s's B''s s''s R's)];
val concl =
- HOLogic.mk_Trueprop (mk_bis As Bs ss B''s s''s (map2 (curry mk_rel_comp) Rs R's));
+ HOLogic.mk_Trueprop (mk_bis Bs ss B''s s''s (map2 (curry mk_rel_comp) Rs R's));
in
Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ B''s @ s''s @ Rs @ R's)
+ (fold_rev Logic.all (Bs @ ss @ B's @ s's @ B''s @ s''s @ Rs @ R's)
(Logic.list_implies (prems, concl)))
(K (mk_bis_O_tac lthy m bis_rel_thm rel_congs rel_OOs))
|> Thm.close_derivation
@@ -807,10 +806,10 @@
val bis_Gr_thm =
let
val concl =
- HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's (map2 mk_Gr Bs fs));
+ HOLogic.mk_Trueprop (mk_bis Bs ss B's s's (map2 mk_Gr Bs fs));
in
Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ fs)
+ (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs)
(Logic.list_implies ([coalg_prem, mor_prem], concl)))
(fn {context = ctxt, prems = _} => mk_bis_Gr_tac ctxt bis_rel_thm rel_Grps mor_image_thms
morE_thms coalg_in_thms)
@@ -828,12 +827,12 @@
let
val prem =
HOLogic.mk_Trueprop (mk_Ball Idx
- (Term.absfree idx' (mk_bis As Bs ss B's s's (map (fn R => R $ idx) Ris))));
+ (Term.absfree idx' (mk_bis Bs ss B's s's (map (fn R => R $ idx) Ris))));
val concl =
- HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's (map (mk_UNION Idx) Ris));
+ HOLogic.mk_Trueprop (mk_bis Bs ss B's s's (map (mk_UNION Idx) Ris));
in
Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (Idx :: As @ Bs @ ss @ B's @ s's @ Ris)
+ (fold_rev Logic.all (Idx :: Bs @ ss @ B's @ s's @ Ris)
(Logic.mk_implies (prem, concl)))
(fn {context = ctxt, prems = _} => mk_bis_Union_tac ctxt bis_def in_mono'_thms)
|> Thm.close_derivation
@@ -841,9 +840,9 @@
(* self-bisimulation *)
- fun mk_sbis As Bs ss Rs = mk_bis As Bs ss Bs ss Rs;
-
- val sbis_prem = HOLogic.mk_Trueprop (mk_sbis As Bs ss sRs);
+ fun mk_sbis Bs ss Rs = mk_bis Bs ss Bs ss Rs;
+
+ val sbis_prem = HOLogic.mk_Trueprop (mk_sbis Bs ss sRs);
(* largest self-bisimulation *)
@@ -852,10 +851,10 @@
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)));
+ (HOLogic.mk_conj (HOLogic.mk_eq (Rtuple, HOLogic.mk_tuple sRs), mk_sbis Bs ss sRs)));
fun lsbis_spec i =
- fold_rev (Term.absfree o Term.dest_Free) (As @ Bs @ ss)
+ fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss)
(mk_UNION all_sbis (Term.absfree Rtuple' (mk_nthN n Rtuple i)));
val ((lsbis_frees, (_, lsbis_def_frees)), (lthy, lthy_old)) =
@@ -868,12 +867,12 @@
val phi = Proof_Context.export_morphism lthy_old lthy;
val lsbis_defs = map (fn def =>
- mk_unabs_def (live + n) (Morphism.thm phi def RS meta_eq_to_obj_eq)) lsbis_def_frees;
+ mk_unabs_def (2 * 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 =
+ fun mk_lsbis Bs ss i =
let
- val args = As @ Bs @ ss;
+ val args = Bs @ ss;
val Ts = map fastype_of args;
val RT = mk_relT (`I (HOLogic.dest_setT (fastype_of (nth Bs (i - 1)))));
val lsbisT = Library.foldr (op -->) (Ts, RT);
@@ -883,8 +882,8 @@
val sbis_lsbis_thm =
Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (As @ Bs @ ss)
- (HOLogic.mk_Trueprop (mk_sbis As Bs ss (map (mk_lsbis As Bs ss) ks))))
+ (fold_rev Logic.all (Bs @ ss)
+ (HOLogic.mk_Trueprop (mk_sbis Bs ss (map (mk_lsbis Bs ss) ks))))
(K (mk_sbis_lsbis_tac lthy lsbis_defs bis_Union_thm bis_cong_thm))
|> Thm.close_derivation;
@@ -895,8 +894,8 @@
val incl_lsbis_thms =
let
- fun mk_concl i R = HOLogic.mk_Trueprop (mk_leq R (mk_lsbis As Bs ss i));
- val goals = map2 (fn i => fn R => fold_rev Logic.all (As @ Bs @ ss @ sRs)
+ fun mk_concl i R = HOLogic.mk_Trueprop (mk_leq R (mk_lsbis Bs ss i));
+ val goals = map2 (fn i => fn R => fold_rev Logic.all (Bs @ ss @ sRs)
(Logic.mk_implies (sbis_prem, mk_concl i R))) ks sRs;
in
map3 (fn goal => fn i => fn def => Goal.prove_sorry lthy [] [] goal
@@ -905,8 +904,8 @@
val equiv_lsbis_thms =
let
- fun mk_concl i B = HOLogic.mk_Trueprop (mk_equiv B (mk_lsbis As Bs ss i));
- val goals = map2 (fn i => fn B => fold_rev Logic.all (As @ Bs @ ss)
+ fun mk_concl i B = HOLogic.mk_Trueprop (mk_equiv B (mk_lsbis Bs ss i));
+ val goals = map2 (fn i => fn B => fold_rev Logic.all (Bs @ ss)
(Logic.mk_implies (coalg_prem, mk_concl i B))) ks Bs;
in
map3 (fn goal => fn l_incl => fn incl_l =>
@@ -1033,7 +1032,7 @@
val isNode_def_bind = rpair [] o Thm.def_binding o isNode_bind;
val isNodeT =
- Library.foldr (op -->) (map fastype_of (As @ [Kl, lab, kl]), HOLogic.boolT);
+ Library.foldr (op -->) (map fastype_of [Kl, lab, kl], HOLogic.boolT);
val Succs = map3 (fn i => fn k => fn k' =>
HOLogic.mk_Collect (fst k', snd k', HOLogic.mk_mem (mk_InN sbdTs k i, mk_Succ Kl kl)))
@@ -1041,12 +1040,12 @@
fun isNode_spec sets x i =
let
- val (passive_sets, active_sets) = chop m (map (fn set => set $ x) sets);
+ val active_sets = drop m (map (fn set => set $ x) sets);
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));
+ map2 (curry HOLogic.mk_eq) active_sets Succs));
in
- fold_rev (Term.absfree o Term.dest_Free) (As @ [Kl, lab, kl]) rhs
+ fold_rev (Term.absfree o Term.dest_Free) [Kl, lab, kl] rhs
end;
val ((isNode_frees, (_, isNode_def_frees)), (lthy, lthy_old)) =
@@ -1060,11 +1059,11 @@
val phi = Proof_Context.export_morphism lthy_old lthy;
val isNode_defs = map (fn def =>
- mk_unabs_def (m + 3) (Morphism.thm phi def RS meta_eq_to_obj_eq)) isNode_def_frees;
+ mk_unabs_def 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 =
- Term.list_comb (Const (nth isNodes (i - 1), isNodeT), As @ [Kl, lab, kl]);
+ fun mk_isNode kl i =
+ Term.list_comb (Const (nth isNodes (i - 1), isNodeT), [Kl, lab, kl]);
val isTree =
let
@@ -1074,9 +1073,9 @@
val tree = mk_Ball Kl (Term.absfree kl'
(HOLogic.mk_conj
- (Library.foldr1 HOLogic.mk_disj (map (mk_isNode As kl) ks),
+ (Library.foldr1 HOLogic.mk_disj (map (mk_isNode kl) ks),
Library.foldr1 HOLogic.mk_conj (map4 (fn Succ => fn i => fn k => fn k' =>
- mk_Ball Succ (Term.absfree k' (mk_isNode As
+ mk_Ball Succ (Term.absfree k' (mk_isNode
(mk_append (kl, HOLogic.mk_list sum_sbdT [mk_InN sbdTs k i])) i)))
Succs ks kks kks'))));
@@ -1092,13 +1091,9 @@
val carT_def_bind = rpair [] o Thm.def_binding o carT_bind;
fun carT_spec i =
- let
- 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
- fold_rev (Term.absfree o Term.dest_Free) As rhs
- end;
+ 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 (HOLogic.mk_list sum_sbdT []) i))));
val ((carT_frees, (_, carT_def_frees)), (lthy, lthy_old)) =
lthy
@@ -1109,13 +1104,10 @@
val phi = Proof_Context.export_morphism lthy_old lthy;
- val carT_defs = map (fn def =>
- mk_unabs_def m (Morphism.thm phi def RS meta_eq_to_obj_eq)) carT_def_frees;
+ val carT_defs = map (fn def => 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
- (Const (nth carTs (i - 1),
- Library.foldr (op -->) (map fastype_of As, HOLogic.mk_setT treeT)), As);
+ fun mk_carT i = Const (nth carTs (i - 1), HOLogic.mk_setT treeT);
val strT_binds = mk_internal_bs strTN;
fun strT_bind i = nth strT_binds (i - 1);
@@ -1152,12 +1144,11 @@
fun mk_strT FT i = Const (nth strTs (i - 1), treeT --> FT);
- val carTAs = map (mk_carT As) ks;
+ val carTAs = map mk_carT ks;
val strTAs = map2 mk_strT treeFTs ks;
val coalgT_thm =
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all As (HOLogic.mk_Trueprop (mk_coalg As carTAs strTAs)))
+ Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (mk_coalg carTAs strTAs))
(fn {context = ctxt, prems = _} => mk_coalgT_tac ctxt m
(coalg_def :: isNode_defs @ carT_defs) strT_defs set_mapss)
|> Thm.close_derivation;
@@ -1405,36 +1396,6 @@
map (fn i => map (fn i' => rv_last' RS mk_conjunctN n i RS mk_conjunctN n i') ks) ks
end;
- val set_rv_Lev_thmsss = if m = 0 then replicate n (replicate n []) else
- let
- fun mk_case s sets z z_free = Term.absfree z_free (Library.foldr1 HOLogic.mk_conj
- (map2 (fn set => fn A => mk_leq (set $ (s $ z)) A) (take m sets) As));
-
- fun mk_conjunct i z B = HOLogic.mk_imp
- (HOLogic.mk_conj (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z), HOLogic.mk_mem (z, B)),
- mk_case_sumN (map4 mk_case ss setssAs zs zs') $ (mk_rv ss kl i $ z));
-
- val goal = list_all_free (kl :: zs)
- (Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct ks zs Bs));
-
- val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
-
- val set_rv_Lev = singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] []
- (Logic.mk_implies (coalg_prem, HOLogic.mk_Trueprop goal))
- (K (mk_set_rv_Lev_tac lthy m cts Lev_0s Lev_Sucs rv_Nils rv_Conss
- coalg_set_thmss from_to_sbd_thmss)))
- |> Thm.close_derivation;
-
- val set_rv_Lev' = mk_specN (n + 1) set_rv_Lev;
- in
- map (fn i => map (fn i' =>
- split_conj_thm (if n = 1 then set_rv_Lev' RS mk_conjunctN n i RS mp
- else set_rv_Lev' RS mk_conjunctN n i RS mp RSN
- (2, @{thm sum.weak_case_cong} RS iffD1) RS
- (mk_sum_caseN n i' RS iffD1))) ks) ks
- end;
-
val set_Lev_thmsss =
let
fun mk_conjunct i z =
@@ -1514,29 +1475,25 @@
val mor_beh_thm =
Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (As @ Bs @ ss) (Logic.mk_implies (coalg_prem,
- HOLogic.mk_Trueprop (mk_mor Bs ss carTAs strTAs (map (mk_beh ss) ks)))))
+ (fold_rev Logic.all ss (HOLogic.mk_Trueprop
+ (mk_mor active_UNIVs ss carTAs strTAs (map (mk_beh ss) ks))))
(fn {context = ctxt, prems = _} => mk_mor_beh_tac ctxt m mor_def mor_cong_thm
beh_defs carT_defs strT_defs isNode_defs
to_sbd_inj_thmss from_to_sbd_thmss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbd_thms
- length_Lev_thms length_Lev'_thms prefCl_Lev_thms rv_last_thmss
- set_rv_Lev_thmsss set_Lev_thmsss set_image_Lev_thmsss
- set_mapss coalg_set_thmss map_comp_id_thms map_cong0s map_arg_cong_thms)
+ length_Lev_thms length_Lev'_thms prefCl_Lev_thms rv_last_thmss set_Lev_thmsss
+ set_image_Lev_thmsss set_mapss map_comp_id_thms map_cong0s map_arg_cong_thms)
|> Thm.close_derivation;
val timer = time (timer "Behavioral morphism");
- fun mk_LSBIS As i = mk_lsbis As (map (mk_carT As) ks) strTAs i;
- fun mk_car_final As i =
- mk_quotient (mk_carT As i) (mk_LSBIS As i);
- fun mk_str_final As i =
+ val lsbisAs = map (mk_lsbis carTAs strTAs) ks;
+
+ fun mk_str_final i =
mk_univ (HOLogic.mk_comp (Term.list_comb (nth final_maps (i - 1),
- passive_ids @ map (mk_proj o mk_LSBIS As) ks), nth strTAs (i - 1)));
-
- val car_finalAs = map (mk_car_final As) ks;
- val str_finalAs = map (mk_str_final As) ks;
- val car_finals = map (mk_car_final passive_UNIVs) ks;
- val str_finals = map (mk_str_final passive_UNIVs) ks;
+ passive_ids @ map mk_proj lsbisAs), nth strTAs (i - 1)));
+
+ val car_finals = map2 mk_quotient carTAs lsbisAs;
+ val str_finals = map mk_str_final ks;
val coalgT_set_thmss = map (map (fn thm => coalgT_thm RS thm)) coalg_set_thmss;
val equiv_LSBIS_thms = map (fn thm => coalgT_thm RS thm) equiv_lsbis_thms;
@@ -1544,11 +1501,10 @@
val congruent_str_final_thms =
let
fun mk_goal R final_map strT =
- fold_rev Logic.all As (HOLogic.mk_Trueprop
- (mk_congruent R (HOLogic.mk_comp
- (Term.list_comb (final_map, passive_ids @ map (mk_proj o mk_LSBIS As) ks), strT))));
-
- val goals = map3 mk_goal (map (mk_LSBIS As) ks) final_maps strTAs;
+ HOLogic.mk_Trueprop (mk_congruent R (HOLogic.mk_comp
+ (Term.list_comb (final_map, passive_ids @ map mk_proj lsbisAs), strT)));
+
+ val goals = map3 mk_goal lsbisAs final_maps strTAs;
in
map4 (fn goal => fn lsbisE => fn map_comp_id => fn map_cong0 =>
Goal.prove_sorry lthy [] [] goal
@@ -1557,21 +1513,19 @@
goals lsbisE_thms map_comp_id_thms map_cong0s
end;
- val coalg_final_thm = Goal.prove_sorry lthy [] [] (fold_rev Logic.all As
- (HOLogic.mk_Trueprop (mk_coalg As car_finalAs str_finalAs)))
+ val coalg_final_thm = Goal.prove_sorry lthy [] []
+ (HOLogic.mk_Trueprop (mk_coalg car_finals str_finals))
(K (mk_coalg_final_tac m coalg_def congruent_str_final_thms equiv_LSBIS_thms
set_mapss coalgT_set_thmss))
|> Thm.close_derivation;
- val mor_T_final_thm = Goal.prove_sorry lthy [] [] (fold_rev Logic.all As
- (HOLogic.mk_Trueprop (mk_mor carTAs strTAs car_finalAs str_finalAs
- (map (mk_proj o mk_LSBIS As) ks))))
+ val mor_T_final_thm = Goal.prove_sorry lthy [] []
+ (HOLogic.mk_Trueprop (mk_mor carTAs strTAs car_finals str_finals (map mk_proj lsbisAs)))
(K (mk_mor_T_final_tac mor_def congruent_str_final_thms equiv_LSBIS_thms))
|> Thm.close_derivation;
val mor_final_thm = mor_comp_thm OF [mor_beh_thm, mor_T_final_thm];
- val in_car_final_thms = map (fn mor_image' => mor_image' OF
- [tcoalg_thm RS mor_final_thm, UNIV_I]) mor_image'_thms;
+ val in_car_final_thms = map (fn thm => thm OF [mor_final_thm, UNIV_I]) mor_image'_thms;
val timer = time (timer "Final coalgebra");
@@ -1660,7 +1614,7 @@
val mor_Rep =
Goal.prove_sorry lthy [] []
(HOLogic.mk_Trueprop (mk_mor UNIVs dtors car_finals str_finals Rep_Ts))
- (fn {context = ctxt, prems = _} => mk_mor_Rep_tac ctxt m (mor_def :: dtor_defs) Reps
+ (fn {context = ctxt, prems = _} => mk_mor_Rep_tac ctxt (mor_def :: dtor_defs) Reps
Abs_inverses coalg_final_set_thmss map_comp_id_thms map_cong0L_thms)
|> Thm.close_derivation;
@@ -1686,7 +1640,7 @@
|> 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
+ (mk_proj (nth lsbisAs (i - 1)), mk_beh ss i)) ks) zs
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
@@ -1706,8 +1660,7 @@
val mor_unfold_thm =
let
val Abs_inverses' = map2 (curry op RS) in_car_final_thms Abs_inverses;
- val morEs' = map (fn thm =>
- (thm OF [tcoalg_thm RS mor_final_thm, UNIV_I]) RS sym) morE_thms;
+ val morEs' = map (fn thm => (thm OF [mor_final_thm, UNIV_I]) RS sym) morE_thms;
in
Goal.prove_sorry lthy [] []
(fold_rev Logic.all ss
@@ -1720,7 +1673,7 @@
val (raw_coind_thms, raw_coind_thm) =
let
- val prem = HOLogic.mk_Trueprop (mk_sbis passive_UNIVs UNIVs dtors TRs);
+ val prem = HOLogic.mk_Trueprop (mk_sbis UNIVs dtors TRs);
val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map2 (fn R => fn T => mk_leq R (Id_const T)) TRs Ts));
val goal = fold_rev Logic.all TRs (Logic.mk_implies (prem, concl));
@@ -1740,7 +1693,7 @@
(map2 mk_fun_eq unfold_fs ks));
val bis_thm = tcoalg_thm RSN (2, tcoalg_thm RS bis_image2_thm);
- val mor_thm = mor_comp_thm OF [tcoalg_thm RS mor_final_thm, mor_Abs_thm];
+ val mor_thm = mor_comp_thm OF [mor_final_thm, mor_Abs_thm];
val unique_mor = Goal.prove_sorry lthy [] []
(fold_rev Logic.all (ss @ unfold_fs) (Logic.mk_implies (prem, unique)))
@@ -1925,7 +1878,7 @@
fun mk_rel_prem phi dtor rel Jz Jz_copy =
let
- val concl = Term.list_comb (rel, map HOLogic.eq_const passiveAs @ phis) $
+ val concl = Term.list_comb (rel, passive_eqs @ phis) $
(dtor $ Jz) $ (dtor $ Jz_copy);
in
HOLogic.mk_Trueprop
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Tue Feb 18 01:11:25 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Tue Feb 18 14:51:26 2014 +0100
@@ -48,15 +48,14 @@
val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> tactic
val mk_dtor_map_unique_tac: Proof.context -> thm -> thm list -> tactic
val mk_mor_Abs_tac: Proof.context -> thm list -> thm list -> tactic
- val mk_mor_Rep_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm list list ->
+ val mk_mor_Rep_tac: Proof.context -> thm list -> thm list -> thm list -> thm list list ->
thm list -> thm list -> tactic
val mk_mor_T_final_tac: thm -> thm list -> thm list -> tactic
val mk_mor_UNIV_tac: thm list -> thm -> tactic
val mk_mor_beh_tac: Proof.context -> int -> thm -> thm -> thm list -> thm list -> thm list ->
thm list -> thm list list -> thm list list -> thm list -> thm list -> thm list -> thm list ->
thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list ->
- thm list list list -> thm list list list -> thm list list -> thm list list -> thm list ->
- thm list -> thm list -> tactic
+ thm list list list -> thm list list -> thm list -> thm list -> thm list -> tactic
val mk_mor_case_sum_tac: 'a list -> thm -> tactic
val mk_mor_comp_tac: thm -> thm list -> thm list -> thm list -> tactic
val mk_mor_elim_tac: thm -> tactic
@@ -87,8 +86,6 @@
val mk_set_ge_tac: int -> thm -> thm list -> tactic
val mk_set_le_tac: int -> thm -> thm list -> thm list list -> tactic
val mk_set_map0_tac: thm -> thm -> tactic
- val mk_set_rv_Lev_tac: Proof.context -> int -> cterm option list -> thm list -> thm list ->
- thm list -> thm list -> thm list list -> thm list list -> tactic
val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
val mk_unfold_transfer_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm list -> tactic
@@ -108,8 +105,6 @@
val nat_induct = @{thm nat_induct};
val o_apply_trans_sym = o_apply RS trans RS sym;
val ord_eq_le_trans = @{thm ord_eq_le_trans};
-val ord_eq_le_trans_trans_fun_cong_image_id_id_apply =
- @{thm ord_eq_le_trans[OF trans[OF fun_cong[OF image_id] id_apply]]};
val ordIso_ordLeq_trans = @{thm ordIso_ordLeq_trans};
val snd_convol_fun_cong_sym = @{thm snd_convol} RS fun_cong RS sym;
val sum_weak_case_cong = @{thm sum.weak_case_cong};
@@ -117,10 +112,6 @@
val Collect_splitD_set_mp = @{thm Collect_splitD[OF set_mp]};
val rev_bspec = Drule.rotate_prems 1 bspec;
val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \<union>"]};
-val conversep_in_rel_Id_on =
- @{thm trans[OF conversep_in_rel arg_cong[of _ _ in_rel, OF converse_Id_on]]};
-val relcompp_in_rel_Id_on =
- @{thm trans[OF relcompp_in_rel arg_cong[of _ _ in_rel, OF Id_on_Comp[symmetric]]]};
val converse_shift = @{thm converse_subset_swap} RS iffD1;
fun mk_coalg_set_tac coalg_def =
@@ -245,8 +236,8 @@
CONJ_WRAP' (fn (i, thm) =>
if i <= m
then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans,
- etac @{thm image_mono}, rtac @{thm image_subsetI},
- etac @{thm Collect_split_in_relI[OF Id_onI]}]
+ etac @{thm image_mono}, rtac @{thm image_subsetI}, rtac CollectI,
+ rtac @{thm case_prodI}, rtac refl]
else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
rtac trans_fun_cong_image_id_id_apply, etac @{thm Collect_split_in_rel_leI}])
(1 upto (m + n) ~~ set_map0s)])
@@ -266,13 +257,11 @@
REPEAT_DETERM_N m o rtac (@{thm id_comp} RS fun_cong),
REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong),
rtac trans, rtac map_cong0,
- REPEAT_DETERM_N m o EVERY' [rtac @{thm Id_onD'}, etac set_mp, atac],
+ REPEAT_DETERM_N m o EVERY' [rtac @{thm Collect_splitD}, etac set_mp, atac],
REPEAT_DETERM_N n o rtac refl,
atac, rtac CollectI,
CONJ_WRAP' (fn (i, thm) =>
- if i <= m
- then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI},
- rtac @{thm Id_on_fst}, etac set_mp, atac]
+ if i <= m then rtac subset_UNIV
else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
rtac trans_fun_cong_image_id_id_apply, atac])
(1 upto (m + n) ~~ set_map0s)];
@@ -290,7 +279,7 @@
CONJ_WRAP' (fn (rel_cong, rel_conversep) =>
EVERY' [rtac allI, rtac allI, rtac impI,
rtac (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
- REPEAT_DETERM_N m o rtac conversep_in_rel_Id_on,
+ REPEAT_DETERM_N m o rtac @{thm conversep_eq},
REPEAT_DETERM_N (length rel_congs) o rtac @{thm conversep_in_rel},
rtac (rel_conversep RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
REPEAT_DETERM o etac allE,
@@ -303,7 +292,7 @@
CONJ_WRAP' (fn (rel_cong, rel_OO) =>
EVERY' [rtac allI, rtac allI, rtac impI,
rtac (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
- REPEAT_DETERM_N m o rtac relcompp_in_rel_Id_on,
+ REPEAT_DETERM_N m o rtac @{thm eq_OO},
REPEAT_DETERM_N (length rel_congs) o rtac @{thm relcompp_in_rel},
rtac (rel_OO RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
etac @{thm relcompE},
@@ -313,7 +302,7 @@
etac mp, atac, etac mp, atac]) (rel_congs ~~ rel_OOs)] 1;
fun mk_bis_Gr_tac ctxt bis_rel rel_Grps mor_images morEs coalg_ins =
- unfold_thms_tac ctxt (bis_rel :: @{thm Id_on_Gr} :: @{thm in_rel_Gr} :: rel_Grps) THEN
+ unfold_thms_tac ctxt (bis_rel :: @{thm eq_alt} :: @{thm in_rel_Gr} :: rel_Grps) THEN
EVERY' [rtac conjI,
CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS ssubst) THEN' etac thm) mor_images,
CONJ_WRAP' (fn (coalg_in, morE) =>
@@ -373,13 +362,11 @@
let
val n = length strT_defs;
val ks = 1 upto n;
- fun coalg_tac (i, ((passive_sets, active_sets), def)) =
+ fun coalg_tac (i, (active_sets, def)) =
EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
hyp_subst_tac ctxt, rtac (def RS trans RS @{thm ssubst_mem}), etac (arg_cong RS trans),
rtac (mk_sum_caseN n i), rtac CollectI,
- EVERY' (map (fn thm => EVERY' [rtac conjI, rtac (thm RS ord_eq_le_trans),
- etac ((trans OF [@{thm image_id} RS fun_cong, id_apply]) RS ord_eq_le_trans)])
- passive_sets),
+ REPEAT_DETERM_N m o EVERY' [rtac conjI, rtac subset_UNIV],
CONJ_WRAP' (fn (i, thm) => EVERY' [rtac (thm RS ord_eq_le_trans),
rtac @{thm image_subsetI}, rtac CollectI, rtac exI, rtac exI, rtac conjI, rtac refl,
rtac conjI,
@@ -397,7 +384,6 @@
REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI,
rtac conjI, rtac (@{thm shift_def} RS fun_cong RS trans),
rtac (@{thm append_Cons} RS sym RS arg_cong RS trans), atac,
- REPEAT_DETERM_N m o (rtac conjI THEN' atac),
CONJ_WRAP' (K (EVERY' [etac trans, rtac @{thm Collect_cong},
rtac @{thm eqset_imp_iff}, rtac sym, rtac trans, rtac @{thm Succ_Shift},
rtac (@{thm append_Cons} RS sym RS arg_cong)])) ks]) ks,
@@ -414,7 +400,7 @@
rtac (@{thm append_Nil} RS sym RS arg_cong)])) ks]) (ks ~~ active_sets)];
in
unfold_thms_tac ctxt defs THEN
- CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_map0ss ~~ strT_defs)) 1
+ CONJ_WRAP' coalg_tac (ks ~~ (map (drop m) set_map0ss ~~ strT_defs)) 1
end;
fun mk_Lev_sbd_tac ctxt cts Lev_0s Lev_Sucs to_sbdss =
@@ -519,35 +505,6 @@
ks)] 1
end;
-fun mk_set_rv_Lev_tac ctxt m cts Lev_0s Lev_Sucs rv_Nils rv_Conss coalg_setss from_to_sbdss =
- let
- val n = length Lev_0s;
- val ks = 1 upto n;
- in
- EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
- REPEAT_DETERM o rtac allI,
- CONJ_WRAP' (fn (i, ((Lev_0, rv_Nil), coalg_sets)) =>
- EVERY' [rtac impI, REPEAT_DETERM o etac conjE,
- dtac (Lev_0 RS equalityD1 RS set_mp), etac @{thm singletonE}, etac ssubst,
- rtac (rv_Nil RS arg_cong RS iffD2),
- rtac (mk_sum_caseN n i RS iffD2),
- CONJ_WRAP' (fn thm => etac thm THEN' atac) (take m coalg_sets)])
- (ks ~~ ((Lev_0s ~~ rv_Nils) ~~ coalg_setss)),
- REPEAT_DETERM o rtac allI,
- CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), (from_to_sbds, coalg_sets)) =>
- EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp),
- CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
- (fn (i, (from_to_sbd, coalg_set)) =>
- EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
- rtac (rv_Cons RS arg_cong RS iffD2),
- rtac (mk_sum_caseN n i RS arg_cong RS trans RS iffD2),
- etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE,
- dtac (mk_conjunctN n i), etac mp, etac conjI, etac set_rev_mp,
- etac coalg_set, atac])
- (rev (ks ~~ (from_to_sbds ~~ drop m coalg_sets)))])
- ((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ coalg_setss))] 1
- end;
-
fun mk_set_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss =
let
val n = length Lev_0s;
@@ -655,7 +612,7 @@
fun mk_mor_beh_tac ctxt m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs
to_sbd_injss from_to_sbdss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbds length_Levs length_Lev's
- prefCl_Levs rv_lastss set_rv_Levsss set_Levsss set_image_Levsss set_map0ss coalg_setss
+ prefCl_Levs rv_lastss set_Levsss set_image_Levsss set_map0ss
map_comp_ids map_cong0s map_arg_congs =
let
val n = length beh_defs;
@@ -663,7 +620,7 @@
fun fbetw_tac (i, (carT_def, (isNode_def, (Lev_0, (rv_Nil, (Lev_sbd,
((length_Lev, length_Lev'), (prefCl_Lev, (rv_lasts, (set_map0s,
- (coalg_sets, (set_rv_Levss, (set_Levss, set_image_Levss))))))))))))) =
+ (set_Levss, set_image_Levss))))))))))) =
EVERY' [rtac ballI, rtac (carT_def RS equalityD2 RS set_mp),
rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, rtac conjI,
rtac conjI,
@@ -678,18 +635,12 @@
rtac conjI,
rtac ballI, etac @{thm UN_E}, rtac conjI,
if n = 1 then K all_tac else rtac (mk_sumEN n),
- EVERY' (map6 (fn i => fn isNode_def => fn set_map0s =>
- fn set_rv_Levs => fn set_Levs => fn set_image_Levs =>
+ EVERY' (map5 (fn i => fn isNode_def => fn set_map0s => fn set_Levs => fn set_image_Levs =>
EVERY' [rtac (mk_disjIN n i), rtac (isNode_def RS ssubst),
rtac exI, rtac conjI,
(if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
else rtac (@{thm if_P} RS arg_cong RS trans) THEN' etac length_Lev' THEN'
etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_caseN n i)),
- EVERY' (map2 (fn set_map0 => fn set_rv_Lev =>
- EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans),
- rtac trans_fun_cong_image_id_id_apply,
- etac set_rv_Lev, TRY o atac, etac conjI, atac])
- (take m set_map0s) set_rv_Levs),
CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
EVERY' [rtac (set_map0 RS trans), rtac equalityI, rtac @{thm image_subsetI},
rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
@@ -699,9 +650,9 @@
etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
if n = 1 then rtac refl else atac])
(drop m set_map0s ~~ (set_Levs ~~ set_image_Levs))])
- ks isNode_defs set_map0ss set_rv_Levss set_Levss set_image_Levss),
+ ks isNode_defs set_map0ss set_Levss set_image_Levss),
CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_map0s,
- (set_rv_Levs, (set_Levs, set_image_Levs)))))) =>
+ (set_Levs, set_image_Levs))))) =>
EVERY' [rtac ballI,
REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
rtac (rev_mp OF [rv_last, impI]), etac exE, rtac (isNode_def RS ssubst),
@@ -709,11 +660,6 @@
(if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
else rtac (@{thm if_P} RS trans) THEN' etac length_Lev' THEN'
etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_caseN n i)),
- EVERY' (map2 (fn set_map0 => fn set_rv_Lev =>
- EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans),
- rtac trans_fun_cong_image_id_id_apply,
- etac set_rv_Lev, TRY o atac, etac conjI, atac])
- (take m set_map0s) set_rv_Levs),
CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
EVERY' [rtac (set_map0 RS trans), rtac equalityI, rtac @{thm image_subsetI},
rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
@@ -726,7 +672,7 @@
if n = 1 then rtac refl else atac])
(drop m set_map0s ~~ (set_Levs ~~ set_image_Levs))])
(ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_map0ss ~~
- (set_rv_Levss ~~ (set_Levss ~~ set_image_Levss)))))),
+ (set_Levss ~~ set_image_Levss))))),
(**)
rtac allI, rtac impI, rtac @{thm if_not_P}, rtac notI,
etac notE, etac @{thm UN_I[OF UNIV_I]},
@@ -736,10 +682,6 @@
CONVERSION (Conv.top_conv
(K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
if n = 1 then rtac refl else rtac (mk_sum_caseN n i),
- EVERY' (map2 (fn set_map0 => fn coalg_set =>
- EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans),
- rtac trans_fun_cong_image_id_id_apply, etac coalg_set, atac])
- (take m set_map0s) (take m coalg_sets)),
CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
EVERY' [rtac (set_map0 RS trans), rtac equalityI, rtac @{thm image_subsetI},
rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, rtac set_Lev,
@@ -768,7 +710,7 @@
EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
DETERM o EVERY' [rtac trans, rtac o_apply, rtac Pair_eqI, rtac conjI,
rtac trans, rtac @{thm Shift_def},
- rtac equalityI, rtac subsetI, etac thin_rl, etac thin_rl,
+ rtac equalityI, rtac subsetI, etac thin_rl,
REPEAT_DETERM o eresolve_tac [CollectE, @{thm UN_E}], dtac length_Lev', dtac asm_rl,
etac thin_rl, dtac @{thm set_rev_mp[OF _ equalityD1]},
rtac (@{thm length_Cons} RS arg_cong RS trans), rtac Lev_Suc,
@@ -811,8 +753,7 @@
CONJ_WRAP' fbetw_tac
(ks ~~ (carT_defs ~~ (isNode_defs ~~ (Lev_0s ~~ (rv_Nils ~~ (Lev_sbds ~~
((length_Levs ~~ length_Lev's) ~~ (prefCl_Levs ~~ (rv_lastss ~~
- (set_map0ss ~~ (coalg_setss ~~
- (set_rv_Levsss ~~ (set_Levsss ~~ set_image_Levsss))))))))))))) THEN'
+ (set_map0ss ~~ (set_Levsss ~~ set_image_Levsss))))))))))) THEN'
CONJ_WRAP' mor_tac
(ks ~~ (strT_defs ~~ (((Lev_0s ~~ Lev_Sucs) ~~ (rv_Nils ~~ rv_Conss)) ~~
((map_comp_ids ~~ (map_cong0s ~~ map_arg_congs)) ~~
@@ -834,16 +775,12 @@
CONJ_WRAP' (fn ((set_map0s, coalgT_sets), (equiv_LSBIS, congruent_str_final)) =>
EVERY' [rtac @{thm univ_preserves}, rtac equiv_LSBIS, rtac congruent_str_final,
rtac ballI, rtac @{thm ssubst_mem}, rtac o_apply, rtac CollectI,
- EVERY' (map2 (fn set_map0 => fn coalgT_set =>
- EVERY' [rtac conjI, rtac (set_map0 RS ord_eq_le_trans),
- rtac ord_eq_le_trans_trans_fun_cong_image_id_id_apply,
- etac coalgT_set])
- (take m set_map0s) (take m coalgT_sets)),
+ REPEAT_DETERM_N m o EVERY' [rtac conjI, rtac subset_UNIV],
CONJ_WRAP' (fn (equiv_LSBIS, (set_map0, coalgT_set)) =>
EVERY' [rtac (set_map0 RS ord_eq_le_trans),
rtac @{thm image_subsetI}, rtac ssubst, rtac @{thm proj_in_iff},
rtac equiv_LSBIS, etac set_rev_mp, etac coalgT_set])
- (equiv_LSBISs ~~ drop m (set_map0s ~~ coalgT_sets))])
+ (equiv_LSBISs ~~ (drop m set_map0s ~~ coalgT_sets))])
((set_map0ss ~~ coalgT_setss) ~~ (equiv_LSBISs ~~ congruent_str_finals))] 1;
fun mk_mor_T_final_tac mor_def congruent_str_finals equiv_LSBISs =
@@ -856,7 +793,7 @@
rtac congruent_str_final, atac, rtac o_apply])
(equiv_LSBISs ~~ congruent_str_finals)] 1;
-fun mk_mor_Rep_tac ctxt m defs Reps Abs_inverses coalg_final_setss map_comp_ids map_cong0Ls =
+fun mk_mor_Rep_tac ctxt defs Reps Abs_inverses coalg_final_setss map_comp_ids map_cong0Ls =
unfold_thms_tac ctxt defs THEN
EVERY' [rtac conjI,
CONJ_WRAP' (fn thm => rtac ballI THEN' rtac thm) Reps,
@@ -865,7 +802,7 @@
EVERY' (map2 (fn Abs_inverse => fn coalg_final_set =>
EVERY' [rtac ballI, rtac (o_apply RS trans), rtac Abs_inverse,
etac set_rev_mp, rtac coalg_final_set, rtac Rep])
- Abs_inverses (drop m coalg_final_sets))])
+ Abs_inverses coalg_final_sets)])
(Reps ~~ ((map_comp_ids ~~ map_cong0Ls) ~~ coalg_final_setss))] 1;
fun mk_mor_Abs_tac ctxt defs Abs_inverses =
@@ -940,7 +877,7 @@
rel_congs,
CONJ_WRAP' (fn rel_cong => EVERY' [rtac allI, rtac allI, rtac impI,
REPEAT_DETERM o etac allE, rtac (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
- REPEAT_DETERM_N m o rtac @{thm in_rel_Id_on_UNIV[symmetric]},
+ REPEAT_DETERM_N m o rtac refl,
REPEAT_DETERM_N (length rel_congs) o rtac @{thm in_rel_Collect_split_eq[symmetric]},
etac mp, etac CollectE, etac @{thm splitD}])
rel_congs,
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Tue Feb 18 01:11:25 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Tue Feb 18 14:51:26 2014 +0100
@@ -85,7 +85,6 @@
val FTsAs = mk_FTs allAs;
val FTsBs = mk_FTs allBs;
val FTsCs = mk_FTs allCs;
- val ATs = map HOLogic.mk_setT passiveAs;
val BTs = map HOLogic.mk_setT activeAs;
val B'Ts = map HOLogic.mk_setT activeBs;
val B''Ts = map HOLogic.mk_setT activeCs;
@@ -120,11 +119,10 @@
bd0s Dss bnfs;
val witss = map wits_of_bnf bnfs;
- val (((((((((((((((((((zs, zs'), As), Bs), Bs_copy), B's), B''s), ss), prod_ss), s's), s''s),
+ val ((((((((((((((((((zs, zs'), Bs), Bs_copy), B's), B''s), ss), prod_ss), s's), s''s),
fs), fs_copy), inv_fs), self_fs), gs), all_gs), (xFs, xFs')), (yFs, yFs')),
names_lthy) = lthy
|> mk_Frees' "z" activeAs
- ||>> mk_Frees "A" ATs
||>> mk_Frees "B" BTs
||>> mk_Frees "B" BTs
||>> mk_Frees "B'" B'Ts
@@ -245,16 +243,16 @@
val alg_bind = mk_internal_b algN;
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)*)
+ (*forall i = 1 ... n: (\<forall>x \<in> Fi_in UNIV .. UNIV B1 ... Bn. si x \<in> Bi)*)
val alg_spec =
let
- val ins = map3 mk_in (replicate n (As @ Bs)) setssAs FTsAs;
+ val ins = map3 mk_in (replicate n (passive_UNIVs @ 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 rhs = Library.foldr1 HOLogic.mk_conj (map5 mk_alg_conjunct Bs ss ins xFs xFs')
in
- fold_rev (Term.absfree o Term.dest_Free) (As @ Bs @ ss) rhs
+ fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss) rhs
end;
val ((alg_free, (_, alg_def_free)), (lthy, lthy_old)) =
@@ -264,11 +262,11 @@
val phi = Proof_Context.export_morphism lthy_old lthy;
val alg = fst (Term.dest_Const (Morphism.term phi alg_free));
- val alg_def = mk_unabs_def (live + n) (Morphism.thm phi alg_def_free RS meta_eq_to_obj_eq);
+ val alg_def = mk_unabs_def (2 * n) (Morphism.thm phi alg_def_free RS meta_eq_to_obj_eq);
- fun mk_alg As Bs ss =
+ fun mk_alg Bs ss =
let
- val args = As @ Bs @ ss;
+ val args = Bs @ ss;
val Ts = map fastype_of args;
val algT = Library.foldr (op -->) (Ts, HOLogic.boolT);
in
@@ -277,13 +275,13 @@
val alg_set_thms =
let
- val alg_prem = HOLogic.mk_Trueprop (mk_alg As Bs ss);
+ val alg_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
fun mk_prem x set B = HOLogic.mk_Trueprop (mk_leq (set $ x) B);
fun mk_concl s x B = HOLogic.mk_Trueprop (HOLogic.mk_mem (s $ x, B));
- val premss = map2 ((fn x => fn sets => map2 (mk_prem x) sets (As @ Bs))) xFs setssAs;
+ val premss = map2 ((fn x => fn sets => map2 (mk_prem x) (drop m sets) Bs)) xFs setssAs;
val concls = map3 mk_concl ss xFs Bs;
val goals = map3 (fn x => fn prems => fn concl =>
- fold_rev Logic.all (x :: As @ Bs @ ss)
+ fold_rev Logic.all (x :: Bs @ ss)
(Logic.list_implies (alg_prem :: prems, concl))) xFs premss concls;
in
map (fn goal =>
@@ -291,12 +289,12 @@
goals
end;
- fun mk_talg ATs BTs = mk_alg (map HOLogic.mk_UNIV ATs) (map HOLogic.mk_UNIV BTs);
+ fun mk_talg BTs = mk_alg (map HOLogic.mk_UNIV BTs);
val talg_thm =
let
val goal = fold_rev Logic.all ss
- (HOLogic.mk_Trueprop (mk_talg passiveAs activeAs ss))
+ (HOLogic.mk_Trueprop (mk_talg activeAs ss))
in
Goal.prove_sorry lthy [] [] goal
(K (stac alg_def 1 THEN CONJ_WRAP (K (EVERY' [rtac ballI, rtac UNIV_I] 1)) ss))
@@ -308,7 +306,7 @@
val alg_not_empty_thms =
let
val alg_prem =
- HOLogic.mk_Trueprop (mk_alg passive_UNIVs Bs ss);
+ HOLogic.mk_Trueprop (mk_alg Bs ss);
val concls = map (HOLogic.mk_Trueprop o mk_not_empty) Bs;
val goals =
map (fn concl =>
@@ -415,9 +413,7 @@
fun mk_inv_prem f inv_f B B' = HOLogic.mk_conj (mk_leq (mk_image inv_f $ B') B,
HOLogic.mk_conj (mk_inver inv_f f B, mk_inver f inv_f B'));
val prems = map HOLogic.mk_Trueprop
- ([mk_mor Bs ss B's s's fs,
- mk_alg passive_UNIVs Bs ss,
- mk_alg passive_UNIVs B's s's] @
+ ([mk_mor Bs ss B's s's fs, mk_alg Bs ss, mk_alg B's s's] @
map4 mk_inv_prem fs inv_fs Bs B's);
val concl = HOLogic.mk_Trueprop (mk_mor B's s's Bs ss inv_fs);
in
@@ -497,9 +493,7 @@
val iso_alt_thm =
let
- val prems = map HOLogic.mk_Trueprop
- [mk_alg passive_UNIVs Bs ss,
- mk_alg passive_UNIVs B's s's]
+ val prems = map HOLogic.mk_Trueprop [mk_alg Bs ss, mk_alg B's s's]
val concl = mk_Trueprop_eq (mk_iso Bs ss B's s's fs inv_fs,
HOLogic.mk_conj (mk_mor Bs ss B's s's fs,
Library.foldr1 HOLogic.mk_conj (map3 mk_bij_betw fs Bs B's)));
@@ -517,7 +511,7 @@
val (copy_alg_thm, ex_copy_alg_thm) =
let
val prems = map HOLogic.mk_Trueprop
- (mk_alg passive_UNIVs Bs ss :: map3 mk_bij_betw inv_fs B's Bs);
+ (mk_alg Bs ss :: map3 mk_bij_betw inv_fs B's Bs);
val inver_prems = map HOLogic.mk_Trueprop
(map3 mk_inver inv_fs fs Bs @ map3 mk_inver fs inv_fs B's);
val all_prems = prems @ inver_prems;
@@ -525,7 +519,7 @@
(Term.list_comb (mapT, passive_ids @ inv_fs) $ y)));
val alg = HOLogic.mk_Trueprop
- (mk_alg passive_UNIVs B's (map5 mk_s fs ss mapsBsAs yFs yFs'));
+ (mk_alg B's (map5 mk_s fs ss mapsBsAs yFs yFs'));
val copy_str_thm = Goal.prove_sorry lthy [] []
(fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs)
(Logic.list_implies (all_prems, alg)))
@@ -542,7 +536,7 @@
val ex = HOLogic.mk_Trueprop
(list_exists_free s's
- (HOLogic.mk_conj (mk_alg passive_UNIVs B's s's,
+ (HOLogic.mk_conj (mk_alg B's s's,
mk_iso B's s's Bs ss inv_fs fs_copy)));
val ex_copy_alg_thm = Goal.prove_sorry lthy [] []
(fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs)
@@ -593,7 +587,9 @@
val suc_bd_Asuc_bd = @{thm ordLess_ordLeq_trans[OF ordLess_ctwo_cexp cexp_mono1]} OF
[suc_bd_Card_order, basis_Asuc, suc_bd_Card_order];
- val Asuc_bdT = fst (dest_relT (fastype_of (mk_Asuc_bd As)));
+
+ val Asuc_bd = mk_Asuc_bd passive_UNIVs;
+ val Asuc_bdT = fst (dest_relT (fastype_of Asuc_bd));
val II_BTs = replicate n (HOLogic.mk_setT Asuc_bdT);
val II_sTs = map2 (fn Ds => fn bnf =>
mk_T_of_bnf Ds (passiveAs @ replicate n Asuc_bdT) bnf --> Asuc_bdT) Dss bnfs;
@@ -631,31 +627,31 @@
fun mk_minG Asi i k = mk_UNION (mk_underS suc_bd $ i)
(Term.absfree jdx' (mk_nthN n (Asi $ jdx) k));
- fun mk_minH_component As Asi i sets Ts s k =
+ fun mk_minH_component Asi i sets Ts s k =
HOLogic.mk_binop @{const_name "sup"}
- (mk_minG Asi i k, mk_image s $ mk_in (As @ map (mk_minG Asi i) ks) sets Ts);
+ (mk_minG Asi i k, mk_image s $ mk_in (passive_UNIVs @ map (mk_minG Asi i) ks) sets Ts);
- fun mk_min_algs As ss =
+ fun mk_min_algs ss =
let
val BTs = map (range_type o fastype_of) ss;
- val Ts = map (HOLogic.dest_setT o fastype_of) As @ BTs;
+ val Ts = passiveAs @ BTs;
val (Asi, Asi') = `Free (Asi_name, suc_bdT -->
Library.foldr1 HOLogic.mk_prodT (map HOLogic.mk_setT BTs));
in
mk_worec suc_bd (Term.absfree Asi' (Term.absfree idx' (HOLogic.mk_tuple
- (map4 (mk_minH_component As Asi idx) (mk_setss Ts) (mk_FTs Ts) ss ks))))
+ (map4 (mk_minH_component Asi idx) (mk_setss Ts) (mk_FTs Ts) ss ks))))
end;
val (min_algs_thms, min_algs_mono_thms, card_of_min_algs_thm, least_min_algs_thm) =
let
val i_field = HOLogic.mk_mem (idx, field_suc_bd);
- val min_algs = mk_min_algs As ss;
+ val min_algs = mk_min_algs ss;
val min_algss = map (fn k => mk_nthN n (min_algs $ idx) k) ks;
val concl = HOLogic.mk_Trueprop
(HOLogic.mk_eq (min_algs $ idx, HOLogic.mk_tuple
- (map4 (mk_minH_component As min_algs idx) setssAs FTsAs ss ks)));
- val goal = fold_rev Logic.all (idx :: As @ ss)
+ (map4 (mk_minH_component min_algs idx) setssAs FTsAs ss ks)));
+ val goal = fold_rev Logic.all (idx :: ss)
(Logic.mk_implies (HOLogic.mk_Trueprop i_field, concl));
val min_algs_thm = Goal.prove_sorry lthy [] [] goal
@@ -665,7 +661,7 @@
val min_algs_thms = map (fn k => min_algs_thm RS mk_nthI n k) ks;
fun mk_mono_goal min_alg =
- fold_rev Logic.all (As @ ss) (HOLogic.mk_Trueprop (mk_relChain suc_bd
+ fold_rev Logic.all ss (HOLogic.mk_Trueprop (mk_relChain suc_bd
(Term.absfree idx' min_alg)));
val monos =
@@ -674,8 +670,6 @@
|> Thm.close_derivation)
(map mk_mono_goal min_algss) min_algs_thms;
- val Asuc_bd = mk_Asuc_bd As;
-
fun mk_card_conjunct min_alg = mk_ordLeq (mk_card_of min_alg) Asuc_bd;
val card_conjunction = Library.foldr1 HOLogic.mk_conj (map mk_card_conjunct min_algss);
val card_cT = certifyT lthy suc_bdT;
@@ -690,7 +684,7 @@
suc_bd_Asuc_bd Asuc_bd_Cinfinite)))
|> Thm.close_derivation;
- val least_prem = HOLogic.mk_Trueprop (mk_alg As Bs ss);
+ val least_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
val least_conjunction = Library.foldr1 HOLogic.mk_conj (map2 mk_leq min_algss Bs);
val least_cT = certifyT lthy suc_bdT;
val least_ct = certify lthy (Term.absfree idx' least_conjunction);
@@ -715,9 +709,9 @@
fun min_alg_spec i =
let
val rhs = mk_UNION (field_suc_bd)
- (Term.absfree idx' (mk_nthN n (mk_min_algs As ss $ idx) i));
+ (Term.absfree idx' (mk_nthN n (mk_min_algs ss $ idx) i));
in
- fold_rev (Term.absfree o Term.dest_Free) (As @ ss) rhs
+ fold_rev (Term.absfree o Term.dest_Free) ss rhs
end;
val ((min_alg_frees, (_, min_alg_def_frees)), (lthy, lthy_old)) =
@@ -730,47 +724,45 @@
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 (fn def =>
- mk_unabs_def live (Morphism.thm phi def RS meta_eq_to_obj_eq)) min_alg_def_frees;
+ mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) min_alg_def_frees;
- fun mk_min_alg As ss i =
+ fun mk_min_alg ss i =
let
val T = HOLogic.mk_setT (range_type (fastype_of (nth ss (i - 1))))
- val args = As @ ss;
- val Ts = map fastype_of args;
+ val Ts = map fastype_of ss;
val min_algT = Library.foldr (op -->) (Ts, T);
in
- Term.list_comb (Const (nth min_algs (i - 1), min_algT), args)
+ Term.list_comb (Const (nth min_algs (i - 1), min_algT), ss)
end;
val (alg_min_alg_thm, card_of_min_alg_thms, least_min_alg_thms, mor_incl_min_alg_thm) =
let
- val min_algs = map (mk_min_alg As ss) ks;
+ val min_algs = map (mk_min_alg ss) ks;
- val goal = fold_rev Logic.all (As @ ss) (HOLogic.mk_Trueprop (mk_alg As min_algs ss));
+ val goal = fold_rev Logic.all ss (HOLogic.mk_Trueprop (mk_alg min_algs ss));
val alg_min_alg = Goal.prove_sorry lthy [] [] goal
(K (mk_alg_min_alg_tac m alg_def min_alg_defs suc_bd_limit_thm sum_Cinfinite
set_bd_sumss min_algs_thms min_algs_mono_thms))
|> Thm.close_derivation;
- val Asuc_bd = mk_Asuc_bd As;
fun mk_card_of_thm min_alg def = Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (As @ ss)
+ (fold_rev Logic.all ss
(HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of min_alg) Asuc_bd)))
(K (mk_card_of_min_alg_tac def card_of_min_algs_thm
suc_bd_Card_order suc_bd_Asuc_bd Asuc_bd_Cinfinite))
|> Thm.close_derivation;
- val least_prem = HOLogic.mk_Trueprop (mk_alg As Bs ss);
+ val least_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
fun mk_least_thm min_alg B def = Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (As @ Bs @ ss)
+ (fold_rev Logic.all (Bs @ ss)
(Logic.mk_implies (least_prem, HOLogic.mk_Trueprop (mk_leq min_alg B))))
(K (mk_least_min_alg_tac def least_min_algs_thm))
|> Thm.close_derivation;
val leasts = map3 mk_least_thm min_algs Bs min_alg_defs;
- val incl_prem = HOLogic.mk_Trueprop (mk_alg passive_UNIVs Bs ss);
- val incl_min_algs = map (mk_min_alg passive_UNIVs ss) ks;
+ val incl_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
+ val incl_min_algs = map (mk_min_alg ss) ks;
val incl = Goal.prove_sorry lthy [] []
(fold_rev Logic.all (Bs @ ss)
(Logic.mk_implies (incl_prem,
@@ -812,7 +804,7 @@
val II = HOLogic.mk_Collect (fst iidx', IIT, list_exists_free (II_Bs @ II_ss)
(HOLogic.mk_conj (HOLogic.mk_eq (iidx,
Abs_IIT $ (HOLogic.mk_prod (HOLogic.mk_tuple II_Bs, HOLogic.mk_tuple II_ss))),
- mk_alg passive_UNIVs II_Bs II_ss)));
+ mk_alg II_Bs II_ss)));
val select_Bs = map (mk_nthN n (HOLogic.mk_fst (Rep_IIT $ iidx))) ks;
val select_ss = map (mk_nthN n (HOLogic.mk_snd (Rep_IIT $ iidx))) ks;
@@ -849,23 +841,23 @@
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;
+ val car_inits = map (mk_min_alg str_inits) ks;
(*TODO: replace with instantiate? (problem: figure out right type instantiation)*)
val alg_init_thm = Goal.prove_sorry lthy [] []
- (HOLogic.mk_Trueprop (mk_alg passive_UNIVs car_inits str_inits))
+ (HOLogic.mk_Trueprop (mk_alg car_inits str_inits))
(K (rtac alg_min_alg_thm 1))
|> Thm.close_derivation;
val alg_select_thm = Goal.prove_sorry lthy [] []
(HOLogic.mk_Trueprop (mk_Ball II
- (Term.absfree iidx' (mk_alg passive_UNIVs select_Bs select_ss))))
+ (Term.absfree iidx' (mk_alg select_Bs select_ss))))
(fn {context = ctxt, prems = _} => mk_alg_select_tac ctxt Abs_IIT_inverse_thm)
|> Thm.close_derivation;
val mor_select_thm =
let
- val alg_prem = HOLogic.mk_Trueprop (mk_alg passive_UNIVs Bs ss);
+ val alg_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
val i_prem = HOLogic.mk_Trueprop (HOLogic.mk_mem (iidx, II));
val mor_prem = HOLogic.mk_Trueprop (mk_mor select_Bs select_ss Bs ss Asuc_fs);
val prems = [alg_prem, i_prem, mor_prem];
@@ -882,7 +874,7 @@
val (init_ex_mor_thm, init_unique_mor_thms) =
let
- val prem = HOLogic.mk_Trueprop (mk_alg passive_UNIVs Bs ss);
+ val prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
val concl = HOLogic.mk_Trueprop
(list_exists_free init_fs (mk_mor car_inits str_inits Bs ss init_fs));
val ex_mor = Goal.prove_sorry lthy [] []
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Tue Feb 18 01:11:25 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Tue Feb 18 14:51:26 2014 +0100
@@ -89,16 +89,13 @@
val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \<union>"]}
fun mk_alg_set_tac alg_def =
- dtac (alg_def RS iffD1) 1 THEN
- REPEAT_DETERM (etac conjE 1) THEN
- EVERY' [etac bspec, rtac CollectI] 1 THEN
- REPEAT_DETERM (etac conjI 1) THEN atac 1;
+ EVERY' [dtac (alg_def RS iffD1), REPEAT_DETERM o etac conjE, etac bspec, rtac CollectI,
+ REPEAT_DETERM o (rtac (subset_UNIV RS conjI) ORELSE' etac conjI), atac] 1;
fun mk_alg_not_empty_tac ctxt alg_set alg_sets wits =
(EVERY' [rtac notI, hyp_subst_tac ctxt, ftac alg_set] THEN'
REPEAT_DETERM o FIRST'
- [rtac subset_UNIV,
- EVERY' [rtac @{thm subset_emptyI}, eresolve_tac wits],
+ [EVERY' [rtac @{thm subset_emptyI}, eresolve_tac wits],
EVERY' [rtac subsetI, rtac FalseE, eresolve_tac wits],
EVERY' [rtac subsetI, dresolve_tac wits, hyp_subst_tac ctxt,
FIRST' (map (fn thm => rtac thm THEN' atac) alg_sets)]] THEN'
@@ -220,7 +217,7 @@
CONJ_WRAP' (fn (thms, thm) =>
EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac set_mp,
rtac equalityD1, etac @{thm bij_betw_imageE}, rtac imageI, etac thm,
- REPEAT_DETERM o rtac subset_UNIV, REPEAT_DETERM_N n o (set_tac thms)])
+ REPEAT_DETERM_N n o set_tac thms])
(set_maps ~~ alg_sets);
in
(rtac rev_mp THEN' DETERM o bij_betw_inv_tac THEN' rtac impI THEN'
@@ -238,7 +235,7 @@
val mor_tac =
CONJ_WRAP' (fn (thms, thm) =>
EVERY' [rtac ballI, etac CollectE, etac @{thm inverE}, etac thm,
- REPEAT_DETERM o rtac subset_UNIV, REPEAT_DETERM_N n o (set_tac thms)])
+ REPEAT_DETERM_N n o set_tac thms])
(set_maps ~~ alg_sets);
in
(rtac (iso_alt RS iffD2) THEN'
@@ -340,7 +337,7 @@
fun mk_minH_tac (min_alg, alg_set) = EVERY' [rtac ord_eq_le_trans, etac min_alg,
rtac @{thm Un_least}, minG_tac, rtac @{thm image_subsetI},
REPEAT_DETERM o eresolve_tac [CollectE, conjE], etac alg_set,
- REPEAT_DETERM o FIRST' [atac, etac subset_trans THEN' minG_tac]];
+ REPEAT_DETERM o (etac subset_trans THEN' minG_tac)];
in
(rtac induct THEN'
rtac impI THEN'
@@ -397,9 +394,8 @@
fun alg_epi_tac ((alg_set, str_init_def), set_map) =
EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
rtac ballI, ftac (alg_select RS bspec), stac str_init_def, etac alg_set,
- REPEAT_DETERM o FIRST' [rtac subset_UNIV,
- EVERY' [rtac ord_eq_le_trans, resolve_tac set_map, rtac subset_trans,
- etac @{thm image_mono}, rtac @{thm image_Collect_subsetI}, etac bspec, atac]]];
+ REPEAT_DETERM o EVERY' [rtac ord_eq_le_trans, resolve_tac set_map, rtac subset_trans,
+ etac @{thm image_mono}, rtac @{thm image_Collect_subsetI}, etac bspec, atac]];
in
(rtac mor_cong THEN' REPEAT_DETERM_N n o (rtac sym THEN' rtac @{thm comp_id}) THEN'
rtac (Thm.permute_prems 0 1 mor_comp) THEN' etac (Thm.permute_prems 0 1 mor_comp) THEN'
@@ -448,7 +444,6 @@
fun mk_alg_tac (alg_set, (in_mono, (morE, map_cong0))) = EVERY' [rtac ballI, rtac CollectI,
REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac (alg_min_alg RS alg_set),
- REPEAT_DETERM_N m o rtac subset_UNIV,
REPEAT_DETERM_N n o (etac subset_trans THEN' rtac @{thm Collect_restrict}),
rtac trans, mor_tac morE in_mono,
rtac trans, cong_tac map_cong0,
@@ -468,7 +463,6 @@
fun mk_alg_tac alg_set = EVERY' [rtac ballI, rtac CollectI,
REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac (alg_min_alg RS alg_set),
- REPEAT_DETERM_N m o rtac subset_UNIV,
REPEAT_DETERM_N n o (etac subset_trans THEN' rtac @{thm Collect_restrict}),
rtac mp, etac bspec, rtac CollectI,
REPEAT_DETERM_N m o (rtac conjI THEN' atac),