--- a/src/HOL/Codatatype/Codatatype.thy Tue Sep 04 13:05:07 2012 +0200
+++ b/src/HOL/Codatatype/Codatatype.thy Tue Sep 04 13:06:41 2012 +0200
@@ -16,6 +16,7 @@
and
"codata" :: thy_decl
uses
+ "Tools/bnf_fp_sugar_tactics.ML"
"Tools/bnf_fp_sugar.ML"
begin
--- a/src/HOL/Codatatype/Tools/bnf_comp.ML Tue Sep 04 13:05:07 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML Tue Sep 04 13:06:41 2012 +0200
@@ -223,9 +223,7 @@
let
val comp_in = mk_in Asets comp_sets CCA;
val comp_in_alt = mk_in (map2 (mk_in Asets) inner_setss CAs) outer_sets CCA;
- val goal =
- fold_rev Logic.all Asets
- (HOLogic.mk_Trueprop (HOLogic.mk_eq (comp_in, comp_in_alt)));
+ val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (comp_in, comp_in_alt));
in
Skip_Proof.prove lthy [] [] goal
(fn {context, ...} => mk_comp_in_alt_tac context comp_set_alt_thms)
@@ -346,8 +344,7 @@
let
val killN_in = mk_in Asets killN_sets T;
val killN_in_alt = mk_in (map HOLogic.mk_UNIV killedAs @ Asets) bnf_sets T;
- val goal =
- fold_rev Logic.all Asets (HOLogic.mk_Trueprop (HOLogic.mk_eq (killN_in, killN_in_alt)));
+ val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (killN_in, killN_in_alt));
in
Skip_Proof.prove lthy [] [] goal (K killN_in_alt_tac) |> Thm.close_derivation
end;
@@ -455,8 +452,7 @@
let
val liftN_in = mk_in Asets liftN_sets T;
val liftN_in_alt = mk_in (drop n Asets) bnf_sets T;
- val goal =
- fold_rev Logic.all Asets (HOLogic.mk_Trueprop (HOLogic.mk_eq (liftN_in, liftN_in_alt)))
+ val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (liftN_in, liftN_in_alt));
in
Skip_Proof.prove lthy [] [] goal (K liftN_in_alt_tac) |> Thm.close_derivation
end;
@@ -541,9 +537,7 @@
let
val permute_in = mk_in Asets permute_sets T;
val permute_in_alt = mk_in (permute_rev Asets) bnf_sets T;
- val goal =
- fold_rev Logic.all Asets
- (HOLogic.mk_Trueprop (HOLogic.mk_eq (permute_in, permute_in_alt)));
+ val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (permute_in, permute_in_alt));
in
Skip_Proof.prove lthy [] [] goal (K (mk_permute_in_alt_tac src dest))
|> Thm.close_derivation
--- a/src/HOL/Codatatype/Tools/bnf_def.ML Tue Sep 04 13:05:07 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML Tue Sep 04 13:06:41 2012 +0200
@@ -721,8 +721,7 @@
(Term.list_comb (bnf_map_BsCs, gs),
Term.list_comb (bnf_map_AsBs, fs));
in
- fold_rev Logic.all (fs @ gs)
- (HOLogic.mk_Trueprop (HOLogic.mk_eq (bnf_map_app_comp, comp_bnf_map_app)))
+ fold_rev Logic.all (fs @ gs) (mk_Trueprop_eq (bnf_map_app_comp, comp_bnf_map_app))
end;
val goal_map_cong =
@@ -730,7 +729,7 @@
fun mk_prem z set f f_copy =
Logic.all z (Logic.mk_implies
(HOLogic.mk_Trueprop (HOLogic.mk_mem (z, set $ x)),
- HOLogic.mk_Trueprop (HOLogic.mk_eq (f $ z, f_copy $ z))));
+ mk_Trueprop_eq (f $ z, f_copy $ z)));
val prems = map4 mk_prem zs bnf_sets_As fs fs_copy;
val eq = HOLogic.mk_eq (Term.list_comb (bnf_map_AsBs, fs) $ x,
Term.list_comb (bnf_map_AsBs, fs_copy) $ x);
@@ -747,8 +746,7 @@
HOLogic.mk_comp (setB, Term.list_comb (bnf_map_AsBs, fs));
val image_comp_set = HOLogic.mk_comp (mk_image f, setA);
in
- fold_rev Logic.all fs
- (HOLogic.mk_Trueprop (HOLogic.mk_eq (set_comp_map, image_comp_set)))
+ fold_rev Logic.all fs (mk_Trueprop_eq (set_comp_map, image_comp_set))
end;
in
map3 mk_goal bnf_sets_As bnf_sets_Bs fs
@@ -845,9 +843,7 @@
(map2 (fn h => fn set => HOLogic.mk_comp (mk_image h, set)) hs bnf_sets_As)
defT;
(*collect {set1 ... setm} o map f1 ... fm = collect {f1` o set1 ... fm` o setm}*)
- val goal =
- fold_rev Logic.all hs
- (HOLogic.mk_Trueprop (HOLogic.mk_eq (collect_map, image_collect)));
+ val goal = fold_rev Logic.all hs (mk_Trueprop_eq (collect_map, image_collect));
in
Skip_Proof.prove lthy [] [] goal
(fn {context = ctxt, ...} => mk_collect_set_natural_tac ctxt (#set_natural axioms))
@@ -990,8 +986,7 @@
let
val lhs = Term.list_comb (relAsBs, map2 mk_Gr As fs);
val rhs = mk_Gr (mk_in As bnf_sets_As CA') (Term.list_comb (bnf_map_AsBs, fs));
- val goal = fold_rev Logic.all (As @ fs)
- (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)));
+ val goal = fold_rev Logic.all (As @ fs) (mk_Trueprop_eq (lhs, rhs));
in
Skip_Proof.prove lthy [] [] goal
(mk_rel_Gr_tac bnf_rel_def (#map_id axioms) (#map_cong axioms)
@@ -1052,7 +1047,7 @@
(mk_rel_converse_le_tac bnf_rel_def (Lazy.force rel_Id) (#map_cong axioms)
(Lazy.force map_comp') (map Lazy.force set_natural'))
|> Thm.close_derivation
- val goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)));
+ val goal = fold_rev Logic.all Rs (mk_Trueprop_eq (lhs, rhs));
in
Skip_Proof.prove lthy [] [] goal (fn _ => mk_rel_converse_tac le_thm)
|> Thm.close_derivation
@@ -1066,8 +1061,7 @@
val relBsCs = mk_bnf_rel setRTsBsCs CB' CC';
val lhs = Term.list_comb (relAsCs, map2 (curry mk_rel_comp) Rs Ss);
val rhs = mk_rel_comp (Term.list_comb (relAsBs, Rs), Term.list_comb (relBsCs, Ss));
- val goal =
- fold_rev Logic.all (Rs @ Ss) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)));
+ val goal = fold_rev Logic.all (Rs @ Ss) (mk_Trueprop_eq (lhs, rhs));
in
Skip_Proof.prove lthy [] [] goal
(mk_rel_O_tac bnf_rel_def (Lazy.force rel_Id) (#map_cong axioms)
@@ -1089,7 +1083,7 @@
HOLogic.mk_exists (fst z', snd z', HOLogic.mk_conj (HOLogic.mk_mem (z, bnf_in),
HOLogic.mk_conj (map_fst_eq, map_snd_eq)));
val goal =
- fold_rev Logic.all (x :: y :: Rs) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)));
+ fold_rev Logic.all (x :: y :: Rs) (mk_Trueprop_eq (lhs, rhs));
in
Skip_Proof.prove lthy [] [] goal (mk_in_rel_tac bnf_rel_def (length bnf_sets))
|> Thm.close_derivation
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Tue Sep 04 13:05:07 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Tue Sep 04 13:06:41 2012 +0200
@@ -17,6 +17,7 @@
open BNF_FP_Util
open BNF_LFP
open BNF_GFP
+open BNF_FP_Sugar_Tactics
fun cannot_merge_types () = error "Mutually recursive (co)datatypes must have same type parameters";
@@ -142,10 +143,22 @@
val phi = Proof_Context.export_morphism lthy lthy';
val ctr_defs = map (Morphism.thm phi) raw_ctr_defs;
+ val ctrs = map (Morphism.term phi) raw_ctrs;
+ val caseof = Morphism.term phi raw_caseof;
- val ctrs = map (Morphism.term phi) raw_ctrs;
-
- val caseof = Morphism.term phi raw_caseof;
+ val fld_iff_unf_thm =
+ let
+ val fld = @{term "undefined::'a=>'b"};
+ val unf = @{term True};
+ val (T, T') = dest_funT (fastype_of fld);
+ val fld_unf = TrueI;
+ val unf_fld = TrueI;
+ val goal = @{term True};
+ in
+ Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
+ mk_fld_iff_unf_tac ctxt (map (SOME o certifyT lthy) [T, T']) (certify lthy fld)
+ (certify lthy unf) fld_unf unf_fld)
+ end;
(* ### *)
fun cheat_tac {context = ctxt, ...} = Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Tue Sep 04 13:06:41 2012 +0200
@@ -0,0 +1,26 @@
+(* Title: HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2012
+
+Tactics for the LFP/GFP sugar.
+*)
+
+signature BNF_FP_SUGAR_TACTICS =
+sig
+ val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm
+ -> tactic
+end;
+
+structure BNF_FP_Sugar_Tactics : BNF_FP_SUGAR_TACTICS =
+struct
+
+open BNF_Util
+
+fun mk_fld_iff_unf_tac ctxt cTs cfld cunf fld_unf unf_fld =
+ (rtac iffI THEN'
+ EVERY' (map3 (fn cTs => fn cx => fn th =>
+ dtac (Drule.instantiate' cTs [NONE, NONE, SOME cx] arg_cong) THEN'
+ SELECT_GOAL (Local_Defs.unfold_tac ctxt [th]) THEN'
+ atac) [rev cTs, cTs] [cunf, cfld] [unf_fld, fld_unf])) 1;
+
+end;
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Tue Sep 04 13:05:07 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Tue Sep 04 13:06:41 2012 +0200
@@ -237,7 +237,7 @@
Term.list_comb (mapAsCs, take m all_gs @ map HOLogic.mk_comp (drop m all_gs ~~ fs)) $ x;
in
Skip_Proof.prove lthy [] []
- (fold_rev Logic.all (x :: fs @ all_gs) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))))
+ (fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs)))
(K (mk_map_comp_id_tac map_comp))
|> Thm.close_derivation
end;
@@ -252,8 +252,7 @@
HOLogic.mk_Trueprop
(mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z))));
val prems = map4 mk_prem (drop m sets) self_fs zs zs';
- val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq
- (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x))
+ val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x);
in
Skip_Proof.prove lthy [] []
(fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
@@ -268,11 +267,10 @@
val map_arg_cong_thms =
let
- val prems = map2 (fn x => fn y =>
- HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y))) xFs xFs_copy;
+ val prems = map2 (curry mk_Trueprop_eq) xFs xFs_copy;
val maps = map (fn map => Term.list_comb (map, all_fs)) mapsAsBs;
- val concls = map3 (fn x => fn y => fn map =>
- HOLogic.mk_Trueprop (HOLogic.mk_eq (map $ x, map $ y))) xFs xFs_copy maps;
+ val concls =
+ map3 (fn x => fn y => fn map => mk_Trueprop_eq (map $ x, map $ y)) xFs xFs_copy maps;
val goals =
map4 (fn prem => fn concl => fn x => fn y =>
fold_rev Logic.all (x :: y :: all_fs) (Logic.mk_implies (prem, concl)))
@@ -302,7 +300,7 @@
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
- HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ mk_Trueprop_eq (lhs, rhs)
end;
val ((coalg_free, (_, coalg_def_free)), (lthy, lthy_old)) =
@@ -386,7 +384,7 @@
(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
- HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ mk_Trueprop_eq (lhs, rhs)
end;
val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) =
@@ -419,8 +417,7 @@
fun mk_elim_goal B mapAsBs f s s' x =
fold_rev Logic.all (x :: Bs @ ss @ B's @ s's @ fs)
(Logic.list_implies ([prem, HOLogic.mk_Trueprop (HOLogic.mk_mem (x, B))],
- HOLogic.mk_Trueprop (HOLogic.mk_eq
- (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ x]), s' $ (f $ x)))));
+ 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 =
Skip_Proof.prove lthy [] [] goal (K (mk_mor_elim_tac mor_def))
@@ -480,8 +477,7 @@
val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs;
val rhs = Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct mapsAsBs fs ss s's);
in
- Skip_Proof.prove lthy [] []
- (fold_rev Logic.all (ss @ s's @ fs) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))))
+ Skip_Proof.prove lthy [] [] (fold_rev Logic.all (ss @ s's @ fs) (mk_Trueprop_eq (lhs, rhs)))
(K (mk_mor_UNIV_tac morE_thms mor_def))
|> Thm.close_derivation
end;
@@ -535,7 +531,7 @@
val lhs = Term.list_comb (Free (hset_rec_name j, hsetT), ss);
val rhs = mk_nat_rec Zero Suc;
in
- HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ mk_Trueprop_eq (lhs, rhs)
end;
val ((hset_rec_frees, (_, hset_rec_def_frees)), (lthy, lthy_old)) =
@@ -586,7 +582,7 @@
val rhs = mk_UNION (HOLogic.mk_UNIV HOLogic.natT)
(Term.absfree nat' (mk_hset_rec ss nat i j T $ z));
in
- HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ mk_Trueprop_eq (lhs, rhs)
end;
val ((hset_frees, (_, hset_def_frees)), (lthy, lthy_old)) =
@@ -767,8 +763,8 @@
fun mk_prem x B = HOLogic.mk_Trueprop (HOLogic.mk_mem (x, B));
- fun mk_concl j T i f x = HOLogic.mk_Trueprop (HOLogic.mk_eq
- (mk_hset s's i j T $ (f $ x), mk_hset ss i j T $ x));
+ fun mk_concl j T i f x =
+ mk_Trueprop_eq (mk_hset s's i j T $ (f $ x), mk_hset ss i j T $ x);
val goalss = map2 (fn j => fn T => map4 (fn i => fn f => fn x => fn B =>
fold_rev Logic.all (x :: As @ Bs @ ss @ B's @ s's @ fs)
@@ -812,7 +808,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
- HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ mk_Trueprop_eq (lhs, rhs)
end;
val ((bis_free, (_, bis_def_free)), (lthy, lthy_old)) =
@@ -861,7 +857,7 @@
in
Skip_Proof.prove lthy [] []
(fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs)
- (HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_bis As Bs ss B's s's Rs, rhs))))
+ (mk_Trueprop_eq (mk_bis As Bs ss B's s's Rs, rhs)))
(K (mk_bis_rel_tac m bis_def rel_defs map_comp's map_congs set_natural'ss))
|> Thm.close_derivation
end;
@@ -947,7 +943,7 @@
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
- HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ mk_Trueprop_eq (lhs, rhs)
end;
val ((lsbis_frees, (_, lsbis_def_frees)), (lthy, lthy_old)) =
@@ -1166,7 +1162,7 @@
(Library.foldr1 HOLogic.mk_conj (HOLogic.mk_eq (lab $ kl, mk_InN bdFTs x i) ::
map2 mk_subset passive_sets As @ map2 (curry HOLogic.mk_eq) active_sets Succs));
in
- HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ mk_Trueprop_eq (lhs, rhs)
end;
val ((isNode_frees, (_, isNode_def_frees)), (lthy, lthy_old)) =
@@ -1221,7 +1217,7 @@
(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
- HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ mk_Trueprop_eq (lhs, rhs)
end;
val ((carT_frees, (_, carT_def_frees)), (lthy, lthy_old)) =
@@ -1261,7 +1257,7 @@
val rhs = HOLogic.mk_split (Term.absfree Kl' (Term.absfree lab'
(mk_sum_caseN fs $ (lab $ HOLogic.mk_list sum_sbdT []))));
in
- HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ mk_Trueprop_eq (lhs, rhs)
end;
val ((strT_frees, (_, strT_def_frees)), (lthy, lthy_old)) =
@@ -1452,7 +1448,7 @@
val lhs = Term.list_comb (Free (Lev_name, LevT), ss);
val rhs = mk_nat_rec Zero Suc;
in
- HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ mk_Trueprop_eq (lhs, rhs)
end;
val ((Lev_free, (_, Lev_def_free)), (lthy, lthy_old)) =
@@ -1498,7 +1494,7 @@
val lhs = Term.list_comb (Free (rv_name, rvT), ss);
val rhs = mk_list_rec Nil Cons;
in
- HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ mk_Trueprop_eq (lhs, rhs)
end;
val ((rv_free, (_, rv_def_free)), (lthy, lthy_old)) =
@@ -1547,7 +1543,7 @@
val rhs = HOLogic.mk_prod (mk_UNION (HOLogic.mk_UNIV HOLogic.natT)
(Term.absfree nat' (mk_Lev ss nat i $ z)), Lab);
in
- HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ mk_Trueprop_eq (lhs, rhs)
end;
val ((beh_frees, (_, beh_def_frees)), (lthy, lthy_old)) =
@@ -1900,7 +1896,7 @@
(Term.list_comb (map_FT, map HOLogic.id_const passiveAs @ Abs_Ts) $
(str $ (rep $ Jz)));
in
- HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ mk_Trueprop_eq (lhs, rhs)
end;
val ((unf_frees, (_, unf_def_frees)), (lthy, lthy_old)) =
@@ -1953,7 +1949,7 @@
val lhs = Term.list_comb (Free (coiter_name i, coiterT), ss);
val rhs = Term.absfree z' (abs $ (f $ z));
in
- HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ mk_Trueprop_eq (lhs, rhs)
end;
val ((coiter_frees, (_, coiter_def_frees)), (lthy, lthy_old)) =
@@ -2067,7 +2063,7 @@
val lhs = Free (fld_name i, fldT);
val rhs = mk_coiter Ts map_unfs i;
in
- HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ mk_Trueprop_eq (lhs, rhs)
end;
val ((fld_frees, (_, fld_def_frees)), (lthy, lthy_old)) =
@@ -2090,8 +2086,7 @@
val unf_o_fld_thms =
let
- fun mk_goal unf fld FT =
- HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (unf, fld), HOLogic.id_const FT));
+ fun mk_goal unf fld FT = mk_Trueprop_eq (HOLogic.mk_comp (unf, fld), HOLogic.id_const FT);
val goals = map3 mk_goal unfs flds FTs;
in
map5 (fn goal => fn fld_def => fn coiter => fn map_comp_id => fn map_congL =>
@@ -2148,7 +2143,7 @@
val lhs = Term.list_comb (Free (corec_name i, corecT), corec_ss);
val rhs = HOLogic.mk_comp (mk_coiter Ts maps i, Inr_const T AT);
in
- HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ mk_Trueprop_eq (lhs, rhs)
end;
val ((corec_frees, (_, corec_def_frees)), (lthy, lthy_old)) =
@@ -2176,7 +2171,7 @@
val lhs = unf $ (mk_corec corec_ss i $ z);
val rhs = Term.list_comb (corec_map, passive_ids @ sum_cases) $ (corec_s $ z);
in
- fold_rev Logic.all (z :: corec_ss) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
+ fold_rev Logic.all (z :: corec_ss) (mk_Trueprop_eq (lhs, rhs))
end;
val goals = map5 mk_goal ks corec_ss corec_maps_rev unfs zs;
in
@@ -2382,8 +2377,8 @@
val (map_simp_thms, map_thms) =
let
fun mk_goal fs_map map unf unf' = fold_rev Logic.all fs
- (HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (unf', fs_map),
- HOLogic.mk_comp (Term.list_comb (map, fs @ fs_maps), unf))));
+ (mk_Trueprop_eq (HOLogic.mk_comp (unf', fs_map),
+ HOLogic.mk_comp (Term.list_comb (map, fs @ fs_maps), unf)));
val goals = map4 mk_goal fs_maps map_FTFT's unfs unf's;
val cTs = map (SOME o certifyT lthy) FTs';
val maps =
@@ -2412,8 +2407,8 @@
val (map_unique_thms, map_unique_thm) =
let
fun mk_prem u map unf unf' =
- HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (unf', u),
- HOLogic.mk_comp (Term.list_comb (map, fs @ us), unf)));
+ mk_Trueprop_eq (HOLogic.mk_comp (unf', u),
+ HOLogic.mk_comp (Term.list_comb (map, fs @ us), unf));
val prems = map4 mk_prem us map_FTFT's unfs unf's;
val goal =
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
@@ -2915,9 +2910,8 @@
val Jrel_unfold_thms =
let
fun mk_goal Jz Jz' unf unf' JrelR relR = fold_rev Logic.all (Jz :: Jz' :: JRs)
- (HOLogic.mk_Trueprop (HOLogic.mk_eq
- (HOLogic.mk_mem (HOLogic.mk_prod (Jz, Jz'), JrelR),
- HOLogic.mk_mem (HOLogic.mk_prod (unf $ Jz, unf' $ Jz'), relR))));
+ (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (Jz, Jz'), JrelR),
+ HOLogic.mk_mem (HOLogic.mk_prod (unf $ Jz, unf' $ Jz'), relR)));
val goals = map6 mk_goal Jzs Jz's unfs unf's JrelRs relRs;
in
map12 (fn i => fn goal => fn in_rel => fn map_comp => fn map_cong =>
@@ -2934,8 +2928,7 @@
val Jpred_unfold_thms =
let
fun mk_goal Jz Jz' unf unf' Jpredphi predphi = fold_rev Logic.all (Jz :: Jz' :: Jphis)
- (HOLogic.mk_Trueprop (HOLogic.mk_eq
- (Jpredphi $ Jz $ Jz', predphi $ (unf $ Jz) $ (unf' $ Jz'))));
+ (mk_Trueprop_eq (Jpredphi $ Jz $ Jz', predphi $ (unf $ Jz) $ (unf' $ Jz')));
val goals = map6 mk_goal Jzs Jz's unfs unf's Jpredphis predphis;
in
map3 (fn goal => fn pred_def => fn Jrel_unfold =>
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Tue Sep 04 13:05:07 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Tue Sep 04 13:06:41 2012 +0200
@@ -170,7 +170,7 @@
take m all_gs @ map HOLogic.mk_comp (drop m all_gs ~~ fs)) $ x;
in
Skip_Proof.prove lthy [] []
- (fold_rev Logic.all (x :: fs @ all_gs) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))))
+ (fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs)))
(K (mk_map_comp_id_tac map_comp))
|> Thm.close_derivation
end;
@@ -184,8 +184,7 @@
fun mk_prem set f z z' = HOLogic.mk_Trueprop
(mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z))));
val prems = map4 mk_prem (drop m sets) self_fs zs zs';
- val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq
- (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x))
+ val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x);
in
Skip_Proof.prove lthy [] []
(fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
@@ -217,7 +216,7 @@
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
- HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ mk_Trueprop_eq (lhs, rhs)
end;
val ((alg_free, (_, alg_def_free)), (lthy, lthy_old)) =
@@ -312,7 +311,7 @@
Library.foldr1 HOLogic.mk_conj
(map8 mk_mor setssAs mapsAsBs fs ss s's FTsAs xFs xFs'))
in
- HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ mk_Trueprop_eq (lhs, rhs)
end;
val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) =
@@ -345,8 +344,7 @@
fun mk_elim_goal sets mapAsBs f s s' x T =
fold_rev Logic.all (x :: Bs @ ss @ B's @ s's @ fs)
(Logic.list_implies ([prem, mk_elim_prem sets x T],
- HOLogic.mk_Trueprop (HOLogic.mk_eq (f $ (s $ x),
- s' $ Term.list_comb (mapAsBs, passive_ids @ fs @ [x])))));
+ mk_Trueprop_eq (f $ (s $ x), s' $ Term.list_comb (mapAsBs, passive_ids @ fs @ [x]))));
val elim_goals = map7 mk_elim_goal setssAs mapsAsBs fs ss s's xFs FTsAs;
fun prove goal =
Skip_Proof.prove lthy [] [] goal (K (mk_mor_elim_tac mor_def)) |> Thm.close_derivation;
@@ -445,8 +443,7 @@
val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs;
val rhs = Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct mapsAsBs fs ss s's);
in
- Skip_Proof.prove lthy [] []
- (fold_rev Logic.all (ss @ s's @ fs) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))))
+ Skip_Proof.prove lthy [] [] (fold_rev Logic.all (ss @ s's @ fs) (mk_Trueprop_eq (lhs, rhs)))
(K (mk_mor_UNIV_tac m morE_thms mor_def))
|> Thm.close_derivation
end;
@@ -472,9 +469,9 @@
val prems = map HOLogic.mk_Trueprop
[mk_alg passive_UNIVs Bs ss,
mk_alg passive_UNIVs B's s's]
- val concl = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_iso Bs ss B's s's fs inv_fs,
+ 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))));
+ Library.foldr1 HOLogic.mk_conj (map3 mk_bij_betw fs Bs B's)));
in
Skip_Proof.prove lthy [] []
(fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs) (Logic.list_implies (prems, concl)))
@@ -698,7 +695,7 @@
val rhs = mk_UNION (field_suc_bd)
(Term.absfree idx' (mk_nthN n (mk_min_algs As ss $ idx) i));
in
- HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ mk_Trueprop_eq (lhs, rhs)
end;
val ((min_alg_frees, (_, min_alg_def_frees)), (lthy, lthy_old)) =
@@ -818,7 +815,7 @@
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
- HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ mk_Trueprop_eq (lhs, rhs)
end;
val ((str_init_frees, (_, str_init_def_frees)), (lthy, lthy_old)) =
@@ -1006,7 +1003,7 @@
val rhs = Term.absfree x' (abs $ (str $
(Term.list_comb (map_FT_init, map HOLogic.id_const passiveAs @ Rep_Ts) $ x)));
in
- HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ mk_Trueprop_eq (lhs, rhs)
end;
val ((fld_frees, (_, fld_def_frees)), (lthy, lthy_old)) =
@@ -1066,7 +1063,7 @@
val lhs = Term.list_comb (Free (iter_name i, iterT), ss);
val rhs = mk_nthN n iter i;
in
- HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ mk_Trueprop_eq (lhs, rhs)
end;
val ((iter_frees, (_, iter_def_frees)), (lthy, lthy_old)) =
@@ -1151,7 +1148,7 @@
val lhs = Free (unf_name i, unfT);
val rhs = mk_iter Ts map_flds i;
in
- HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ mk_Trueprop_eq (lhs, rhs)
end;
val ((unf_frees, (_, unf_def_frees)), (lthy, lthy_old)) =
@@ -1174,8 +1171,7 @@
val unf_o_fld_thms =
let
- fun mk_goal unf fld FT =
- HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (unf, fld), HOLogic.id_const FT));
+ fun mk_goal unf fld FT = mk_Trueprop_eq (HOLogic.mk_comp (unf, fld), HOLogic.id_const FT);
val goals = map3 mk_goal unfs flds FTs;
in
map5 (fn goal => fn unf_def => fn iter => fn map_comp_id => fn map_congL =>
@@ -1228,7 +1224,7 @@
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_iter Ts maps i);
in
- HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ mk_Trueprop_eq (lhs, rhs)
end;
val ((rec_frees, (_, rec_def_frees)), (lthy, lthy_old)) =
@@ -1255,7 +1251,7 @@
val lhs = mk_rec rec_ss i $ (fld $ x);
val rhs = rec_s $ (Term.list_comb (rec_map, passive_ids @ convols) $ x);
in
- fold_rev Logic.all (x :: rec_ss) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
+ fold_rev Logic.all (x :: rec_ss) (mk_Trueprop_eq (lhs, rhs))
end;
val goals = map5 mk_goal ks rec_ss rec_maps_rev flds xFs;
in
@@ -1400,8 +1396,8 @@
val (map_simp_thms, map_thms) =
let
fun mk_goal fs_map map fld fld' = fold_rev Logic.all fs
- (HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (fs_map, fld),
- HOLogic.mk_comp (fld', Term.list_comb (map, fs @ fs_maps)))));
+ (mk_Trueprop_eq (HOLogic.mk_comp (fs_map, fld),
+ HOLogic.mk_comp (fld', Term.list_comb (map, fs @ fs_maps))));
val goals = map4 mk_goal fs_maps map_FTFT's flds fld's;
val maps =
map4 (fn goal => fn iter => fn map_comp_id => fn map_cong =>
@@ -1415,8 +1411,8 @@
val (map_unique_thms, map_unique_thm) =
let
fun mk_prem u map fld fld' =
- HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (u, fld),
- HOLogic.mk_comp (fld', Term.list_comb (map, fs @ us))));
+ mk_Trueprop_eq (HOLogic.mk_comp (u, fld),
+ HOLogic.mk_comp (fld', Term.list_comb (map, fs @ us)));
val prems = map4 mk_prem us map_FTFT's flds fld's;
val goal =
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
@@ -1460,8 +1456,8 @@
val (set_simp_thmss, set_thmss) =
let
fun mk_goal sets fld set col map =
- HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (set, fld),
- HOLogic.mk_comp (col, Term.list_comb (map, passive_ids @ sets))));
+ mk_Trueprop_eq (HOLogic.mk_comp (set, fld),
+ HOLogic.mk_comp (col, Term.list_comb (map, passive_ids @ sets)));
val goalss =
map3 (fn sets => map4 (mk_goal sets) flds sets) setss_by_range colss map_setss;
val setss = map (map2 (fn iter => fn goal =>
@@ -1469,9 +1465,9 @@
iter_thms) goalss;
fun mk_simp_goal pas_set act_sets sets fld z set =
- Logic.all z (HOLogic.mk_Trueprop (HOLogic.mk_eq (set $ (fld $ z),
+ Logic.all z (mk_Trueprop_eq (set $ (fld $ z),
mk_union (pas_set $ z,
- Library.foldl1 mk_union (map2 (fn X => mk_UNION (X $ z)) act_sets sets)))));
+ Library.foldl1 mk_union (map2 (fn X => mk_UNION (X $ z)) act_sets sets))));
val simp_goalss =
map2 (fn i => fn sets =>
map4 (fn Fsets => mk_simp_goal (nth Fsets (i - 1)) (drop m Fsets) sets)
@@ -1743,9 +1739,8 @@
val Irel_unfold_thms =
let
fun mk_goal xF yF fld fld' IrelR relR = fold_rev Logic.all (xF :: yF :: IRs)
- (HOLogic.mk_Trueprop (HOLogic.mk_eq
- (HOLogic.mk_mem (HOLogic.mk_prod (fld $ xF, fld' $ yF), IrelR),
- HOLogic.mk_mem (HOLogic.mk_prod (xF, yF), relR))));
+ (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (fld $ xF, fld' $ yF), IrelR),
+ HOLogic.mk_mem (HOLogic.mk_prod (xF, yF), relR)));
val goals = map6 mk_goal xFs yFs flds fld's IrelRs relRs;
in
map12 (fn i => fn goal => fn in_rel => fn map_comp => fn map_cong =>
@@ -1762,8 +1757,7 @@
val Ipred_unfold_thms =
let
fun mk_goal xF yF fld fld' Ipredphi predphi = fold_rev Logic.all (xF :: yF :: Iphis)
- (HOLogic.mk_Trueprop (HOLogic.mk_eq
- (Ipredphi $ (fld $ xF) $ (fld' $ yF), predphi $ xF $ yF)));
+ (mk_Trueprop_eq (Ipredphi $ (fld $ xF) $ (fld' $ yF), predphi $ xF $ yF));
val goals = map6 mk_goal xFs yFs flds fld's Ipredphis predphis;
in
map3 (fn goal => fn pred_def => fn Irel_unfold =>
--- a/src/HOL/Codatatype/Tools/bnf_util.ML Tue Sep 04 13:05:07 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_util.ML Tue Sep 04 13:06:41 2012 +0200
@@ -69,6 +69,7 @@
val mk_Card_order: term -> term
val mk_Field: term -> term
val mk_Gr: term -> term -> term
+ val mk_Trueprop_eq: term * term -> term
val mk_UNION: term -> term -> term
val mk_Union: typ -> term
val mk_card_binop: string -> (typ * typ -> typ) -> term -> term -> term
@@ -302,6 +303,8 @@
(** Operators **)
+val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
+
fun mk_converse R =
let
val RT = dest_relT (fastype_of R);
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Tue Sep 04 13:05:07 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Tue Sep 04 13:06:41 2012 +0200
@@ -51,8 +51,6 @@
fun mk_half_pairss ys = mk_half_pairss' [[]] ys;
-val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
-
fun mk_undef T Ts = Const (@{const_name undefined}, Ts ---> T);
fun eta_expand_caseof_arg xs f_xs = fold_rev Term.lambda xs f_xs;