--- a/src/HOL/Tools/BNF/bnf_comp.ML Wed Jul 16 17:57:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Thu Jul 17 10:28:32 2014 +0200
@@ -223,7 +223,7 @@
val bd' = @{term natLeq};
val bd_bd' = HOLogic.mk_prod (bd, bd');
val ordIso = Const (@{const_name ordIso}, HOLogic.mk_setT (fastype_of bd_bd'));
- val goal = HOLogic.mk_Trueprop (HOLogic.mk_mem (bd_bd', ordIso));
+ val goal = mk_Trueprop_mem (bd_bd', ordIso);
in
(bd', SOME (Goal.prove_sorry lthy [] [] goal (K bd_ordIso_natLeq_tac)
|> Thm.close_derivation))
@@ -811,7 +811,7 @@
val Abs_bdT_inj = mk_Abs_inj_thm Abs_bdT_inject;
val Abs_bdT_bij = mk_Abs_bij_thm lthy Abs_bdT_inj Abs_bdT_cases;
-
+
val bd_ordIso = @{thm dir_image} OF [Abs_bdT_inj, bd_Card_order_of_bnf bnf];
val bd_card_order =
@{thm card_order_dir_image} OF [Abs_bdT_bij, bd_card_order_of_bnf bnf];
@@ -862,7 +862,7 @@
(#map_unfolds unfold_set @ flat (#set_unfoldss unfold_set) @ #rel_unfolds unfold_set);
val bnf'' = bnf' |> morph_bnf_defs (Morphism.thm_morphism "BNF" (unfold_thms lthy' unfolds));
-
+
val map_def = map_def_of_bnf bnf'';
val set_defs = set_defs_of_bnf bnf'';
val rel_def = rel_def_of_bnf bnf'';
--- a/src/HOL/Tools/BNF/bnf_def.ML Wed Jul 16 17:57:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Thu Jul 17 10:28:32 2014 +0200
@@ -981,8 +981,7 @@
fun mk_map_cong_prem x z set f f_copy =
Logic.all z (Logic.mk_implies
- (HOLogic.mk_Trueprop (HOLogic.mk_mem (z, set $ x)),
- mk_Trueprop_eq (f $ z, f_copy $ z)));
+ (mk_Trueprop_mem (z, set $ x), mk_Trueprop_eq (f $ z, f_copy $ z)));
val map_cong0_goal =
let
@@ -1044,7 +1043,7 @@
else @{term False});
in
fold_rev Logic.all (z :: xs)
- (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (z, set_wit)), concl))
+ (Logic.mk_implies (mk_Trueprop_mem (z, set_wit), concl))
end;
in
map wit_goal (0 upto live - 1)
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Jul 16 17:57:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Jul 17 10:28:32 2014 +0200
@@ -574,7 +574,7 @@
fun mk_prem_prem xs (xysets, (j, x)) =
close_prem_prem xs (Logic.list_implies (map (fn (x', (y, set)) =>
- HOLogic.mk_Trueprop (HOLogic.mk_mem (y, set $ x'))) xysets,
+ mk_Trueprop_mem (y, set $ x')) xysets,
HOLogic.mk_Trueprop (nth ps (j - 1) $ x)));
fun mk_raw_prem phi ctr ctr_Ts ctrXs_Ts =
@@ -1564,7 +1564,7 @@
let
val X = HOLogic.dest_setT (range_type (fastype_of set));
val (x, ctxt') = yield_singleton (mk_Frees "x") X ctxt;
- val assm = HOLogic.mk_Trueprop (HOLogic.mk_mem (x, set $ a));
+ val assm = mk_Trueprop_mem (x, set $ a);
in
travese_nested_types x ctxt'
|>> map (Logic.mk_implies o pair assm)
@@ -1575,13 +1575,13 @@
end)
| T =>
if T = A then
- ([HOLogic.mk_Trueprop (HOLogic.mk_mem (t, setA $ ta))], ctxt)
+ ([mk_Trueprop_mem (t, setA $ ta)], ctxt)
else
([], ctxt));
val (concls, ctxt') =
if sel_rangeT = A then
- ([HOLogic.mk_Trueprop (HOLogic.mk_mem (selA $ ta, setA $ ta))], ctxt)
+ ([mk_Trueprop_mem (selA $ ta, setA $ ta)], ctxt)
else
travese_nested_types (selA $ ta) names_lthy;
in
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Wed Jul 16 17:57:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Thu Jul 17 10:28:32 2014 +0200
@@ -326,7 +326,7 @@
val coalg_set_thmss =
let
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_prem x B = mk_Trueprop_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) Bs (drop m sets))
@@ -405,7 +405,7 @@
Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_leq (mk_image f $ B1) B2));
val image_goals = map3 mk_image_goal fs Bs B's;
fun mk_elim_goal B mapAsBs f s s' x =
- Logic.list_implies ([prem, HOLogic.mk_Trueprop (HOLogic.mk_mem (x, B))],
+ Logic.list_implies ([prem, mk_Trueprop_mem (x, B)],
mk_Trueprop_eq (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ x]), s' $ (f $ x)));
val elim_goals = map6 mk_elim_goal Bs mapsAsBs fs ss s's zs;
fun prove goal =
@@ -1092,8 +1092,8 @@
val length_Levs = map (fn i => length_Lev' RS mk_conjunctN n i RS mp) ks;
fun mk_goal i z = Logic.mk_implies
- (HOLogic.mk_Trueprop (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z)),
- HOLogic.mk_Trueprop (HOLogic.mk_mem (kl, mk_Lev ss (mk_size kl) i $ z)));
+ (mk_Trueprop_mem (kl, mk_Lev ss nat i $ z),
+ mk_Trueprop_mem (kl, mk_Lev ss (mk_size kl) i $ z));
val goals = map2 mk_goal ks zs;
val length_Levs' = map2 (fn goal => fn length_Lev =>
@@ -1651,7 +1651,7 @@
||>> mk_Frees "JR" activeJphiTs;
val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
- fun mk_Jrel_DEADID_coinduct_thm () =
+ fun mk_Jrel_DEADID_coinduct_thm () =
mk_rel_xtor_co_induct_thm Greatest_FP rels activeJphis (map HOLogic.eq_const Ts) Jphis
Jzs Jz's dtors dtor's (fn {context = ctxt, prems} =>
(unfold_thms_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN
@@ -1697,10 +1697,10 @@
val set_bss =
map (flat o map2 (fn B => fn b =>
if member (op =) resDs (TFree B) then [] else [b]) resBs) set_bss0;
-
+
fun col_bind j = mk_internal_b (colN ^ (if m = 1 then "" else string_of_int j));
val col_def_bind = rpair [] o Thm.def_binding o col_bind;
-
+
fun col_spec j Zero hrec hrec' =
let
fun mk_Suc dtor sets z z' =
@@ -1711,13 +1711,13 @@
Term.absfree z'
(mk_union (set $ (dtor $ z), Library.foldl1 mk_union (map2 mk_UN sets ks)))
end;
-
+
val Suc = Term.absdummy HOLogic.natT (Term.absfree hrec'
(HOLogic.mk_tuple (map4 mk_Suc dtors FTs_setss Jzs Jzs')));
in
mk_rec_nat Zero Suc
end;
-
+
val ((col_frees, (_, col_def_frees)), (lthy, lthy_old)) =
lthy
|> fold_map4 (fn j => fn Zero => fn hrec => fn hrec' => Local_Theory.define
@@ -1725,12 +1725,12 @@
ls Zeros hrecs hrecs'
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
-
+
val phi = Proof_Context.export_morphism lthy_old lthy;
-
+
val col_defs = map (fn def => Morphism.thm phi def RS meta_eq_to_obj_eq) col_def_frees;
val cols = map (fst o Term.dest_Const o Morphism.term phi) col_frees;
-
+
fun mk_col Ts nat i j T =
let
val hrecT = HOLogic.mk_tupleT (map (fn U => U --> HOLogic.mk_setT T) Ts)
@@ -1738,12 +1738,12 @@
in
mk_nthN n (Term.list_comb (Const (nth cols (j - 1), colT), [nat])) i
end;
-
+
val col_0ss = mk_rec_simps n @{thm rec_nat_0_imp} col_defs;
val col_Sucss = mk_rec_simps n @{thm rec_nat_Suc_imp} col_defs;
val col_0ss' = transpose col_0ss;
val col_Sucss' = transpose col_Sucss;
-
+
fun mk_set Ts i j T =
Abs (Name.uu, nth Ts (i - 1), mk_UNION (HOLogic.mk_UNIV HOLogic.natT)
(Term.absfree nat' (mk_col Ts nat i j T $ Bound 1)));
@@ -1835,28 +1835,28 @@
let
fun mk_passive_prem set dtor x K =
Logic.all x (HOLogic.mk_Trueprop (mk_leq (set $ (dtor $ x)) (K $ x)));
-
+
fun mk_active_prem dtor x1 K1 set x2 K2 =
fold_rev Logic.all [x1, x2]
- (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (x2, set $ (dtor $ x1))),
+ (Logic.mk_implies (mk_Trueprop_mem (x2, set $ (dtor $ x1)),
HOLogic.mk_Trueprop (mk_leq (K2 $ x2) (K1 $ x1))));
-
+
val premss = map2 (fn j => fn Ks =>
map4 mk_passive_prem (map (fn xs => nth xs (j - 1)) FTs_setss) dtors Jzs Ks @
flat (map4 (fn sets => fn s => fn x1 => fn K1 =>
map3 (mk_active_prem s x1 K1) (drop m sets) Jzs_copy Ks) FTs_setss dtors Jzs Ks))
ls Kss;
-
+
val col_minimal_thms =
let
fun mk_conjunct j T i K x = mk_leq (mk_col Ts nat i j T $ x) (K $ x);
fun mk_concl j T Ks = list_all_free Jzs
(Library.foldr1 HOLogic.mk_conj (map3 (mk_conjunct j T) ks Ks Jzs));
val concls = map3 mk_concl ls passiveAs Kss;
-
+
val goals = map2 (fn prems => fn concl =>
Logic.list_implies (prems, HOLogic.mk_Trueprop concl)) premss concls
-
+
val ctss =
map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) concls;
in
@@ -1868,11 +1868,11 @@
|> singleton (Proof_Context.export names_lthy lthy))
goals ctss col_0ss' col_Sucss'
end;
-
+
fun mk_conjunct set K x = mk_leq (set $ x) (K $ x);
fun mk_concl sets Ks = Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct sets Ks Jzs);
val concls = map2 mk_concl Jsetss_by_range Kss;
-
+
val goals = map2 (fn prems => fn concl =>
Logic.list_implies (prems, HOLogic.mk_Trueprop concl)) premss concls;
in
@@ -1889,16 +1889,16 @@
let
fun mk_set_incl_Jset dtor x set Jset =
HOLogic.mk_Trueprop (mk_leq (set $ (dtor $ x)) (Jset $ x));
-
+
fun mk_set_Jset_incl_Jset dtor x y set Jset1 Jset2 =
- Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (x, set $ (dtor $ y))),
+ Logic.mk_implies (mk_Trueprop_mem (x, set $ (dtor $ y)),
HOLogic.mk_Trueprop (mk_leq (Jset1 $ x) (Jset2 $ y)));
-
+
val set_incl_Jset_goalss =
map4 (fn dtor => fn x => fn sets => fn Jsets =>
map2 (mk_set_incl_Jset dtor x) (take m sets) Jsets)
dtors Jzs FTs_setss Jsetss_by_bnf;
-
+
(*x(k) : F(i)set(m+k) (dtor(i) y(i)) ==> J(k)set(j) x(k) <= J(i)set(j) y(i)*)
val set_Jset_incl_Jset_goalsss =
map4 (fn dtori => fn yi => fn sets => fn Jsetsi =>
@@ -1928,7 +1928,7 @@
ks goalss)
set_Jset_incl_Jset_goalsss col_Sucss)
end;
-
+
val set_incl_Jset_thmss' = transpose dtor_Jset_incl_thmss;
val set_Jset_incl_Jset_thmsss' = transpose (map transpose dtor_set_Jset_incl_thmsss);
val set_Jset_thmss = map (map (fn thm => thm RS @{thm set_mp})) dtor_Jset_incl_thmss;
@@ -1936,14 +1936,14 @@
dtor_set_Jset_incl_thmsss;
val set_Jset_thmss' = transpose set_Jset_thmss;
val set_Jset_Jset_thmsss' = transpose (map transpose set_Jset_Jset_thmsss);
-
+
val dtor_Jset_induct_thms =
let
val incls =
maps (map (fn thm => thm RS @{thm subset_Collect_iff})) dtor_Jset_incl_thmss @
@{thms subset_Collect_iff[OF subset_refl]};
- val cTs = map (SOME o certifyT lthy) params';
+ val cTs = map (SOME o certifyT lthy) params';
fun mk_induct_tinst phis jsets y y' =
map4 (fn phi => fn jset => fn Jz => fn Jz' =>
SOME (certify lthy (Term.absfree Jz' (HOLogic.mk_Collect (fst y', snd y',
@@ -1985,7 +1985,7 @@
le_goals Jset_minimal_thms set_Jset_thmss' set_Jset_Jset_thmsss');
val ge_goalss = map (map HOLogic.mk_Trueprop) (mk_goals (uncurry mk_leq o swap));
- val set_ge_thmss =
+ val set_ge_thmss =
map3 (map3 (fn goal => fn set_incl_Jset => fn set_Jset_incl_Jsets =>
Goal.prove_sorry lthy [] [] goal
(K (mk_set_ge_tac n set_incl_Jset set_Jset_incl_Jsets))
@@ -2225,7 +2225,7 @@
abs' helper_ind_phiss;
fun mk_helper_ind_concl ab' z ind_phi set =
mk_Ball (set $ z) (Term.absfree ab' ind_phi);
-
+
val mk_helper_ind_concls =
map3 (fn ab' => fn ind_phis => fn zip_sets =>
map3 (mk_helper_ind_concl ab') zip_zs ind_phis zip_sets)
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Wed Jul 16 17:57:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Thu Jul 17 10:28:32 2014 +0200
@@ -272,7 +272,7 @@
let
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));
+ fun mk_concl s x B = mk_Trueprop_mem (s $ x, B);
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 = map2 (fn prems => fn concl =>
@@ -790,7 +790,7 @@
val mor_select_thm =
let
- val i_prem = HOLogic.mk_Trueprop (HOLogic.mk_mem (iidx, II));
+ val i_prem = mk_Trueprop_mem (iidx, II);
val mor_prem = HOLogic.mk_Trueprop (mk_mor select_Bs select_ss active_UNIVs ss Asuc_fs);
val prems = [i_prem, mor_prem];
val concl = HOLogic.mk_Trueprop
@@ -1208,7 +1208,7 @@
let
fun mk_IH phi set z =
let
- val prem = HOLogic.mk_Trueprop (HOLogic.mk_mem (z, set $ x));
+ val prem = mk_Trueprop_mem (z, set $ x);
val concl = HOLogic.mk_Trueprop (phi $ z);
in
Logic.all z (Logic.mk_implies (prem, concl))
@@ -1247,8 +1247,8 @@
let
fun mk_IH phi set set' z1 z2 =
let
- val prem1 = HOLogic.mk_Trueprop (HOLogic.mk_mem (z1, (set $ x)));
- val prem2 = HOLogic.mk_Trueprop (HOLogic.mk_mem (z2, (set' $ y)));
+ val prem1 = mk_Trueprop_mem (z1, (set $ x));
+ val prem2 = mk_Trueprop_mem (z2, (set' $ y));
val concl = HOLogic.mk_Trueprop (phi $ z1 $ z2);
in
fold_rev Logic.all [z1, z2] (Logic.list_implies ([prem1, prem2], concl))
@@ -1383,44 +1383,44 @@
val (sum_bd0T_params, sum_bd0T_params') = `(map TFree) (Term.add_tfreesT sum_bd0T []);
val sbd0T_bind = mk_internal_b (sum_bdTN ^ "0");
-
+
val ((sbd0T_name, (sbd0T_glob_info, sbd0T_loc_info)), lthy) =
typedef (sbd0T_bind, sum_bd0T_params', NoSyn)
(HOLogic.mk_UNIV sum_bd0T) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
-
+
val sbd0T = Type (sbd0T_name, sum_bd0T_params);
val Abs_sbd0T = Const (#Abs_name sbd0T_glob_info, sum_bd0T --> sbd0T);
-
+
val sbd0_bind = mk_internal_b (sum_bdN ^ "0");
val sbd0_def_bind = (Thm.def_binding sbd0_bind, []);
-
+
val sbd0_spec = mk_dir_image sum_bd0 Abs_sbd0T;
-
+
val ((sbd0_free, (_, sbd0_def_free)), (lthy, lthy_old)) =
lthy
|> Local_Theory.define ((sbd0_bind, NoSyn), (sbd0_def_bind, sbd0_spec))
||> `Local_Theory.restore;
-
+
val phi = Proof_Context.export_morphism lthy_old lthy;
-
+
val sbd0_def = Morphism.thm phi sbd0_def_free RS meta_eq_to_obj_eq;
val sbd0 = Const (fst (Term.dest_Const (Morphism.term phi sbd0_free)),
mk_relT (`I sbd0T));
-
+
val Abs_sbd0T_inj = mk_Abs_inj_thm (#Abs_inject sbd0T_loc_info);
val Abs_sbd0T_bij = mk_Abs_bij_thm lthy Abs_sbd0T_inj (#Abs_cases sbd0T_loc_info);
-
+
val sum_Cinfinite = mk_sum_Cinfinite bd0_Cinfinites;
val sum_Card_order = sum_Cinfinite RS conjunct2;
val sum_card_order = mk_sum_card_order bd0_card_orders;
-
+
val sbd0_ordIso = @{thm ssubst_Pair_rhs} OF
[@{thm dir_image} OF [Abs_sbd0T_inj, sum_Card_order], sbd0_def];
val sbd0_Cinfinite = @{thm Cinfinite_cong} OF [sbd0_ordIso, sum_Cinfinite];
-
+
val sbd0_card_order = @{thm iffD2[OF arg_cong[of _ _ card_order]]} OF
[sbd0_def, @{thm card_order_dir_image} OF [Abs_sbd0T_bij, sum_card_order]];
-
+
fun mk_set_sbd0 i bd0_Card_order bd0s =
map (fn thm => @{thm ordLeq_ordIso_trans} OF
[bd0_Card_order RS mk_ordLeq_csum n i thm, sbd0_ordIso]) bd0s;
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Wed Jul 16 17:57:27 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Thu Jul 17 10:28:32 2014 +0200
@@ -53,6 +53,7 @@
val mk_IfN: typ -> term list -> term list -> term
val mk_Trueprop_eq: term * term -> term
+ val mk_Trueprop_mem: term * term -> term
val rapp: term -> term -> term
@@ -201,6 +202,7 @@
Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ c $ t $ mk_IfN T cs ts;
val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
+val mk_Trueprop_mem = HOLogic.mk_Trueprop o HOLogic.mk_mem;
fun rapp u t = betapply (t, u);