--- a/src/HOL/BNF_FP_Base.thy Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/BNF_FP_Base.thy Tue Feb 18 21:00:13 2014 +0100
@@ -154,6 +154,5 @@
ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML"
ML_file "Tools/BNF/bnf_fp_n2m.ML"
ML_file "Tools/BNF/bnf_fp_n2m_sugar.ML"
-ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML"
end
--- a/src/HOL/BNF_GFP.thy Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/BNF_GFP.thy Tue Feb 18 21:00:13 2014 +0100
@@ -51,21 +51,6 @@
(* Operators: *)
definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
-lemma Id_onD: "(a, b) \<in> Id_on A \<Longrightarrow> a = b"
-unfolding Id_on_def by simp
-
-lemma Id_onD': "x \<in> Id_on A \<Longrightarrow> fst x = snd x"
-unfolding Id_on_def by auto
-
-lemma Id_on_fst: "x \<in> Id_on A \<Longrightarrow> fst x \<in> A"
-unfolding Id_on_def by auto
-
-lemma Id_on_UNIV: "Id_on UNIV = Id"
-unfolding Id_on_def by auto
-
-lemma Id_on_Comp: "Id_on A = Id_on A O Id_on A"
-unfolding Id_on_def by auto
-
lemma Id_on_Gr: "Id_on A = Gr A id"
unfolding Id_on_def Gr_def by auto
@@ -102,9 +87,6 @@
lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (split (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
by force
-lemma Collect_split_in_relI: "x \<in> X \<Longrightarrow> x \<in> Collect (split (in_rel X))"
-by auto
-
lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
unfolding fun_eq_iff by auto
@@ -114,9 +96,6 @@
lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f"
unfolding Gr_def Grp_def fun_eq_iff by auto
-lemma in_rel_Id_on_UNIV: "in_rel (Id_on UNIV) = op ="
-unfolding fun_eq_iff by auto
-
definition relImage where
"relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"
@@ -349,10 +328,10 @@
thus "univ f X \<in> B" using x PRES by simp
qed
-ML_file "Tools/BNF/bnf_gfp_rec_sugar_tactics.ML"
-ML_file "Tools/BNF/bnf_gfp_rec_sugar.ML"
ML_file "Tools/BNF/bnf_gfp_util.ML"
ML_file "Tools/BNF/bnf_gfp_tactics.ML"
ML_file "Tools/BNF/bnf_gfp.ML"
+ML_file "Tools/BNF/bnf_gfp_rec_sugar_tactics.ML"
+ML_file "Tools/BNF/bnf_gfp_rec_sugar.ML"
end
--- a/src/HOL/BNF_LFP.thy Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/BNF_LFP.thy Tue Feb 18 21:00:13 2014 +0100
@@ -237,11 +237,12 @@
lemma id_transfer: "fun_rel A A id id"
unfolding fun_rel_def by simp
-ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML"
ML_file "Tools/BNF/bnf_lfp_util.ML"
ML_file "Tools/BNF/bnf_lfp_tactics.ML"
ML_file "Tools/BNF/bnf_lfp.ML"
ML_file "Tools/BNF/bnf_lfp_compat.ML"
+ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML"
+ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML"
hide_fact (open) id_transfer
--- a/src/HOL/Nitpick.thy Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/Nitpick.thy Tue Feb 18 21:00:13 2014 +0100
@@ -9,7 +9,9 @@
theory Nitpick
imports BNF_FP_Base Map Record Sledgehammer
-keywords "nitpick" :: diag and "nitpick_params" :: thy_decl
+keywords
+ "nitpick" :: diag and
+ "nitpick_params" :: thy_decl
begin
typedecl bisim_iterator
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Feb 18 21:00:13 2014 +0100
@@ -10,22 +10,21 @@
type fp_sugar =
{T: typ,
fp: BNF_FP_Util.fp_kind,
- index: int,
- pre_bnfs: BNF_Def.bnf list,
+ fp_res_index: int,
+ fp_res: BNF_FP_Util.fp_result,
+ pre_bnf: BNF_Def.bnf,
nested_bnfs: BNF_Def.bnf list,
nesting_bnfs: BNF_Def.bnf list,
- fp_res: BNF_FP_Util.fp_result,
- ctr_defss: thm list list,
- ctr_sugars: Ctr_Sugar.ctr_sugar list,
- co_iterss: term list list,
- mapss: thm list list,
+ ctr_defs: thm list,
+ ctr_sugar: Ctr_Sugar.ctr_sugar,
+ co_iters: term list,
+ maps: thm list,
+ common_co_inducts: thm list,
co_inducts: thm list,
- co_inductss: thm list list,
- co_iter_thmsss: thm list list list,
- disc_co_itersss: thm list list list,
- sel_co_iterssss: thm list list list list};
+ co_iter_thmss: thm list list,
+ disc_co_iterss: thm list list,
+ sel_co_itersss: thm list list list};
- val of_fp_sugar: (fp_sugar -> 'a list) -> fp_sugar -> 'a
val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
val transfer_fp_sugar: Proof.context -> fp_sugar -> fp_sugar
val fp_sugar_of: Proof.context -> string -> fp_sugar option
@@ -122,38 +121,40 @@
type fp_sugar =
{T: typ,
fp: fp_kind,
- index: int,
- pre_bnfs: bnf list,
+ fp_res_index: int,
+ fp_res: fp_result,
+ pre_bnf: bnf,
nested_bnfs: bnf list,
nesting_bnfs: bnf list,
- fp_res: fp_result,
- ctr_defss: thm list list,
- ctr_sugars: ctr_sugar list,
- co_iterss: term list list,
- mapss: thm list list,
+ ctr_defs: thm list,
+ ctr_sugar: Ctr_Sugar.ctr_sugar,
+ co_iters: term list,
+ maps: thm list,
+ common_co_inducts: thm list,
co_inducts: thm list,
- co_inductss: thm list list,
- co_iter_thmsss: thm list list list,
- disc_co_itersss: thm list list list,
- sel_co_iterssss: thm list list list list};
-
-fun of_fp_sugar f (fp_sugar as ({index, ...}: fp_sugar)) = nth (f fp_sugar) index;
+ co_iter_thmss: thm list list,
+ disc_co_iterss: thm list list,
+ sel_co_itersss: thm list list list};
-fun morph_fp_sugar phi ({T, fp, index, pre_bnfs, nested_bnfs, nesting_bnfs, fp_res, ctr_defss,
- ctr_sugars, co_iterss, mapss, co_inducts, co_inductss, co_iter_thmsss, disc_co_itersss,
- sel_co_iterssss} : fp_sugar) =
- {T = Morphism.typ phi T, fp = fp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs,
- nested_bnfs = map (morph_bnf phi) nested_bnfs, nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
+fun morph_fp_sugar phi ({T, fp, fp_res, fp_res_index, pre_bnf, nested_bnfs, nesting_bnfs, ctr_defs,
+ ctr_sugar, co_iters, maps, common_co_inducts, co_inducts, co_iter_thmss, disc_co_iterss,
+ sel_co_itersss} : fp_sugar) =
+ {T = Morphism.typ phi T,
+ fp = fp,
fp_res = morph_fp_result phi fp_res,
- ctr_defss = map (map (Morphism.thm phi)) ctr_defss,
- ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars,
- co_iterss = map (map (Morphism.term phi)) co_iterss,
- mapss = map (map (Morphism.thm phi)) mapss,
+ fp_res_index = fp_res_index,
+ pre_bnf = morph_bnf phi pre_bnf,
+ nested_bnfs = map (morph_bnf phi) nested_bnfs,
+ nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
+ ctr_defs = map (Morphism.thm phi) ctr_defs,
+ ctr_sugar = morph_ctr_sugar phi ctr_sugar,
+ co_iters = map (Morphism.term phi) co_iters,
+ maps = map (Morphism.thm phi) maps,
+ common_co_inducts = map (Morphism.thm phi) common_co_inducts,
co_inducts = map (Morphism.thm phi) co_inducts,
- co_inductss = map (map (Morphism.thm phi)) co_inductss,
- co_iter_thmsss = map (map (map (Morphism.thm phi))) co_iter_thmsss,
- disc_co_itersss = map (map (map (Morphism.thm phi))) disc_co_itersss,
- sel_co_iterssss = map (map (map (map (Morphism.thm phi)))) sel_co_iterssss};
+ co_iter_thmss = map (map (Morphism.thm phi)) co_iter_thmss,
+ disc_co_iterss = map (map (Morphism.thm phi)) disc_co_iterss,
+ sel_co_itersss = map (map (map (Morphism.thm phi))) sel_co_itersss};
val transfer_fp_sugar =
morph_fp_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
@@ -183,15 +184,16 @@
(fn phi => Data.map (Symtab.update (key, morph_fp_sugar phi fp_sugar)));
fun register_fp_sugars fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctr_defss
- ctr_sugars co_iterss mapss co_inducts co_inductss co_iter_thmsss disc_co_itersss
+ ctr_sugars co_iterss mapss common_co_inducts co_inductss co_iter_thmsss disc_co_itersss
sel_co_iterssss lthy =
(0, lthy)
|> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1,
- register_fp_sugar s {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs,
- nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss,
- ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, co_inducts = co_inducts,
- co_inductss = co_inductss, co_iter_thmsss = co_iter_thmsss,
- disc_co_itersss = disc_co_itersss, sel_co_iterssss = sel_co_iterssss}
+ register_fp_sugar s {T = T, fp = fp, fp_res = fp_res, fp_res_index = kk,
+ pre_bnf = nth pre_bnfs kk, nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs,
+ ctr_defs = nth ctr_defss kk, ctr_sugar = nth ctr_sugars kk, co_iters = nth co_iterss kk,
+ maps = nth mapss kk, common_co_inducts = common_co_inducts, co_inducts = nth co_inductss kk,
+ co_iter_thmss = nth co_iter_thmsss kk, disc_co_iterss = nth disc_co_itersss kk,
+ sel_co_itersss = nth sel_co_iterssss kk}
lthy)) Ts
|> snd;
@@ -1407,8 +1409,8 @@
|> Spec_Rules.add Spec_Rules.Equational (map co_rec_of iterss, flat rec_thmss)
|> Local_Theory.notes (common_notes @ notes) |> snd
|> register_fp_sugars Least_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss ctr_sugars
- iterss mapss [induct_thm] (transpose [induct_thms]) (transpose [fold_thmss, rec_thmss])
- [] []
+ iterss mapss [induct_thm] (map single induct_thms) (transpose [fold_thmss, rec_thmss])
+ (replicate nn []) (replicate nn [])
end;
fun derive_note_coinduct_coiters_thms_for_types
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Tue Feb 18 21:00:13 2014 +0100
@@ -47,7 +47,8 @@
fun construct_mutualized_fp fp fpTs fp_sugars bs resBs (resDs, Dss) bnfs lthy =
let
- fun steal get = map (of_fp_sugar (get o #fp_res)) fp_sugars;
+ fun steal_fp_res get =
+ map (fn {fp_res, fp_res_index, ...} => nth (get fp_res) fp_res_index) fp_sugars;
val n = length bnfs;
val deads = fold (union (op =)) Dss resDs;
@@ -77,8 +78,8 @@
val ((ctors, dtors), (xtor's, xtors)) =
let
- val ctors = map2 (force_typ names_lthy o (fn T => dummyT --> T)) fpTs (steal #ctors);
- val dtors = map2 (force_typ names_lthy o (fn T => T --> dummyT)) fpTs (steal #dtors);
+ val ctors = map2 (force_typ names_lthy o (fn T => dummyT --> T)) fpTs (steal_fp_res #ctors);
+ val dtors = map2 (force_typ names_lthy o (fn T => T --> dummyT)) fpTs (steal_fp_res #dtors);
in
((ctors, dtors), `(map (Term.subst_atomic_types theta)) (fp_case fp ctors dtors))
end;
@@ -92,9 +93,8 @@
||>> mk_Frees "x" xTs
||>> mk_Frees "y" yTs;
- val fp_bnfs = steal #bnfs;
- val pre_bnfs = map (of_fp_sugar #pre_bnfs) fp_sugars;
- val pre_bnfss = map #pre_bnfs fp_sugars;
+ val fp_bnfs = steal_fp_res #bnfs;
+ val pre_bnfs = map #pre_bnf fp_sugars;
val nesty_bnfss = map (fn sugar => #nested_bnfs sugar @ #nesting_bnfs sugar) fp_sugars;
val fp_nesty_bnfss = fp_bnfs :: nesty_bnfss;
val fp_nesty_bnfs = distinct (op = o pairself T_of_bnf) (flat fp_nesty_bnfss);
@@ -126,9 +126,9 @@
val pre_rels = map2 (fn Ds => mk_rel_of_bnf Ds (As @ fpTs) (Bs @ fpTs')) Dss bnfs;
- val rel_unfoldss = map (maps (fn bnf => no_refl [rel_def_of_bnf bnf])) pre_bnfss;
- val rel_xtor_co_inducts = steal (split_conj_thm o #rel_xtor_co_induct_thm)
- |> map2 (fn unfs => unfold_thms lthy (id_apply :: unfs)) rel_unfoldss;
+ val rel_unfolds = maps (no_refl o single o rel_def_of_bnf) pre_bnfs;
+ val rel_xtor_co_inducts = steal_fp_res (split_conj_thm o #rel_xtor_co_induct_thm)
+ |> map (unfold_thms lthy (id_apply :: rel_unfolds));
val rel_defs = map rel_def_of_bnf bnfs;
val rel_monos = map rel_mono_of_bnf bnfs;
@@ -185,11 +185,13 @@
|> mk_Frees' "s" fold_strTs
||>> mk_Frees' "s" rec_strTs;
- val co_iters = steal #xtor_co_iterss;
- val ns = map (length o #pre_bnfs) fp_sugars;
+ val co_iters = steal_fp_res #xtor_co_iterss;
+ val ns = map (length o #Ts o #fp_res) fp_sugars;
+
fun substT rho (Type (@{type_name "fun"}, [T, U])) = substT rho T --> substT rho U
| substT rho (Type (s, Ts)) = Type (s, map (typ_subst_nonatomic rho) Ts)
| substT _ T = T;
+
fun force_iter is_rec i TU TU_rec raw_iters =
let
val approx_fold = un_fold_of raw_iters
@@ -325,14 +327,14 @@
val pre_map_defs = no_refl (map map_def_of_bnf bnfs);
val fp_pre_map_defs = no_refl (map map_def_of_bnf pre_bnfs);
- val map_unfoldss = map (maps (fn bnf => no_refl [map_def_of_bnf bnf])) pre_bnfss;
- val unfold_map = map2 (fn unfs => unfold_thms lthy (id_apply :: unfs)) map_unfoldss;
+ val map_unfolds = maps (fn bnf => no_refl [map_def_of_bnf bnf]) pre_bnfs;
+ val unfold_map = map (unfold_thms lthy (id_apply :: map_unfolds));
- val fp_xtor_co_iterss = steal #xtor_co_iter_thmss;
+ val fp_xtor_co_iterss = steal_fp_res #xtor_co_iter_thmss;
val fp_xtor_un_folds = map (mk_pointfree lthy o un_fold_of) fp_xtor_co_iterss |> unfold_map;
val fp_xtor_co_recs = map (mk_pointfree lthy o co_rec_of) fp_xtor_co_iterss |> unfold_map;
- val fp_co_iter_o_mapss = steal #xtor_co_iter_o_map_thmss;
+ val fp_co_iter_o_mapss = steal_fp_res #xtor_co_iter_o_map_thmss;
val fp_fold_o_maps = map un_fold_of fp_co_iter_o_mapss |> unfold_map;
val fp_rec_o_maps = map co_rec_of fp_co_iter_o_mapss |> unfold_map;
val fold_thms = fp_case fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} :: @{thms id_apply
@@ -358,20 +360,21 @@
used by "primrec", "primcorecursive", and "datatype_compat". *)
val fp_res =
({Ts = fpTs,
- bnfs = steal #bnfs,
+ bnfs = steal_fp_res #bnfs,
dtors = dtors,
ctors = ctors,
xtor_co_iterss = transpose [un_folds, co_recs],
xtor_co_induct = xtor_co_induct_thm,
- dtor_ctors = steal #dtor_ctors (*too general types*),
- ctor_dtors = steal #ctor_dtors (*too general types*),
- ctor_injects = steal #ctor_injects (*too general types*),
- dtor_injects = steal #dtor_injects (*too general types*),
- xtor_map_thms = steal #xtor_map_thms (*too general types and terms*),
- xtor_set_thmss = steal #xtor_set_thmss (*too general types and terms*),
- xtor_rel_thms = steal #xtor_rel_thms (*too general types and terms*),
+ dtor_ctors = steal_fp_res #dtor_ctors (*too general types*),
+ ctor_dtors = steal_fp_res #ctor_dtors (*too general types*),
+ ctor_injects = steal_fp_res #ctor_injects (*too general types*),
+ dtor_injects = steal_fp_res #dtor_injects (*too general types*),
+ xtor_map_thms = steal_fp_res #xtor_map_thms (*too general types and terms*),
+ xtor_set_thmss = steal_fp_res #xtor_set_thmss (*too general types and terms*),
+ xtor_rel_thms = steal_fp_res #xtor_rel_thms (*too general types and terms*),
xtor_co_iter_thmss = transpose [xtor_un_fold_thms, xtor_co_rec_thms],
- xtor_co_iter_o_map_thmss = steal #xtor_co_iter_o_map_thmss (*theorem about old constant*),
+ xtor_co_iter_o_map_thmss = steal_fp_res #xtor_co_iter_o_map_thmss
+ (*theorem about old constant*),
rel_xtor_co_induct_thm = rel_xtor_co_induct_thm}
|> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
in
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Tue Feb 18 21:00:13 2014 +0100
@@ -119,17 +119,18 @@
val fp_b_names = map base_name_of_typ fpTs;
val nn = length fpTs;
+ val kks = 0 upto nn - 1;
- fun target_ctr_sugar_of_fp_sugar fpT ({T, index, ctr_sugars, ...} : fp_sugar) =
+ fun target_ctr_sugar_of_fp_sugar fpT ({T, ctr_sugar, ...} : fp_sugar) =
let
val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T, fpT) Vartab.empty) [];
val phi = Morphism.term_morphism "BNF" (Term.subst_TVars rho);
in
- morph_ctr_sugar phi (nth ctr_sugars index)
+ morph_ctr_sugar phi ctr_sugar
end;
- val ctr_defss = map (of_fp_sugar #ctr_defss) fp_sugars0;
- val mapss = map (of_fp_sugar #mapss) fp_sugars0;
+ val ctr_defss = map #ctr_defs fp_sugars0;
+ val mapss = map #maps fp_sugars0;
val ctr_sugars = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0;
val ctrss = map #ctrs ctr_sugars;
@@ -215,14 +216,15 @@
(mk_binding b) fpTs Cs) fp_bs xtor_co_iterss lthy
|>> split_list;
- val ((co_inducts, co_inductss, un_fold_thmss, co_rec_thmss, disc_unfold_thmss,
+ val ((common_co_inducts, co_inductss, un_fold_thmss, co_rec_thmss, disc_unfold_thmss,
disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss), fp_sugar_thms) =
if fp = Least_FP then
derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss
co_iterss co_iter_defss lthy
|> `(fn ((inducts, induct, _), (fold_thmss, rec_thmss, _)) =>
- ([induct], [inducts], fold_thmss, rec_thmss, [], [], [], []))
+ ([induct], [inducts], fold_thmss, rec_thmss, replicate nn [],
+ replicate nn [], replicate nn [], replicate nn []))
||> (fn info => (SOME info, NONE))
else
derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
@@ -232,32 +234,38 @@
|> `(fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _),
(disc_unfold_thmss, disc_corec_thmss, _), _,
(sel_unfold_thmsss, sel_corec_thmsss, _)) =>
- (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, unfold_thmss, corec_thmss,
- disc_unfold_thmss, disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss))
+ (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, unfold_thmss,
+ corec_thmss, disc_unfold_thmss, disc_corec_thmss, sel_unfold_thmsss,
+ sel_corec_thmsss))
||> (fn info => (NONE, SOME info));
val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
- fun mk_target_fp_sugar (kk, T) =
- {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs,
- nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss,
- ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, co_inducts = co_inducts,
- co_inductss = transpose co_inductss,
- co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss],
- disc_co_itersss = transpose [disc_unfold_thmss, disc_corec_thmss],
- sel_co_iterssss = transpose [sel_unfold_thmsss, sel_corec_thmsss]}
+ fun mk_target_fp_sugar T kk pre_bnf ctr_defs ctr_sugar co_iters maps co_inducts un_fold_thms
+ co_rec_thms disc_unfold_thms disc_corec_thms sel_unfold_thmss sel_corec_thmss =
+ {T = T, fp = fp, fp_res = fp_res, fp_res_index = kk, pre_bnf = pre_bnf,
+ nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, ctr_defs = ctr_defs,
+ ctr_sugar = ctr_sugar, co_iters = co_iters, maps = maps,
+ common_co_inducts = common_co_inducts, co_inducts = co_inducts,
+ co_iter_thmss = [un_fold_thms, co_rec_thms],
+ disc_co_iterss = [disc_unfold_thms, disc_corec_thms],
+ sel_co_itersss = [sel_unfold_thmss, sel_corec_thmss]}
|> morph_fp_sugar phi;
- val n2m_sugar = (map_index mk_target_fp_sugar fpTs, fp_sugar_thms);
+ val target_fp_sugars =
+ map14 mk_target_fp_sugar fpTs kks pre_bnfs ctr_defss ctr_sugars co_iterss mapss
+ (transpose co_inductss) un_fold_thmss co_rec_thmss disc_unfold_thmss disc_corec_thmss
+ sel_unfold_thmsss sel_corec_thmsss;
+
+ val n2m_sugar = (target_fp_sugars, fp_sugar_thms);
in
(n2m_sugar, lthy |> register_n2m_sugar key n2m_sugar)
end)
end;
(* TODO: needed? *)
-fun indexify_callsss fp_sugar callsss =
+fun indexify_callsss (fp_sugar as {ctr_sugar = {ctrs, ...}, ...} : fp_sugar) callsss =
let
- val {ctrs, ...} = of_fp_sugar #ctr_sugars fp_sugar;
fun indexify_ctr ctr =
(case AList.lookup Term.aconv_untyped callsss ctr of
NONE => replicate (num_binder_types (fastype_of ctr)) []
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Tue Feb 18 21:00:13 2014 +0100
@@ -23,7 +23,6 @@
open BNF_Comp
open BNF_FP_Util
open BNF_FP_Def_Sugar
-open BNF_GFP_Rec_Sugar
open BNF_GFP_Util
open BNF_GFP_Tactics
@@ -164,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
@@ -173,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
@@ -204,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;
@@ -298,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)) =
@@ -317,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
@@ -720,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))))));
@@ -729,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)) =
@@ -739,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
@@ -753,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
@@ -768,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
@@ -808,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)
@@ -829,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
@@ -842,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 *)
@@ -853,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)) =
@@ -869,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);
@@ -884,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;
@@ -896,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
@@ -906,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 =>
@@ -1034,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)))
@@ -1042,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)) =
@@ -1061,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
@@ -1075,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'))));
@@ -1093,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
@@ -1110,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);
@@ -1153,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;
@@ -1406,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 =
@@ -1515,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;
@@ -1545,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
@@ -1558,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");
@@ -1661,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;
@@ -1687,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;
@@ -1707,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
@@ -1721,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));
@@ -1741,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)))
@@ -1926,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_rec_sugar.ML Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Feb 18 21:00:13 2014 +0100
@@ -3,7 +3,7 @@
Author: Jasmin Blanchette, TU Muenchen
Copyright 2013
-Corecursor sugar.
+Corecursor sugar ("primcorec" and "primcorecursive").
*)
signature BNF_GFP_REC_SUGAR =
@@ -367,9 +367,7 @@
| _ => not_codatatype ctxt res_T);
fun map_thms_of_typ ctxt (Type (s, _)) =
- (case fp_sugar_of ctxt s of
- SOME {index, mapss, ...} => nth mapss index
- | NONE => [])
+ (case fp_sugar_of ctxt s of SOME {maps, ...} => maps | NONE => [])
| map_thms_of_typ _ _ = [];
fun corec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy0 =
@@ -378,15 +376,15 @@
val ((missing_res_Ts, perm0_kks,
fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...},
- co_inducts = coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) =
+ common_co_inducts = common_coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) =
nested_to_mutual_fps Greatest_FP bs res_Ts get_indices callssss0 lthy0;
- val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars;
+ val perm_fp_sugars = sort (int_ord o pairself #fp_res_index) fp_sugars;
- val indices = map #index fp_sugars;
- val perm_indices = map #index perm_fp_sugars;
+ val indices = map #fp_res_index fp_sugars;
+ val perm_indices = map #fp_res_index perm_fp_sugars;
- val perm_ctrss = map (#ctrs o of_fp_sugar #ctr_sugars) perm_fp_sugars;
+ val perm_ctrss = map (#ctrs o #ctr_sugar) perm_fp_sugars;
val perm_ctr_Tsss = map (map (binder_types o fastype_of)) perm_ctrss;
val perm_gfpTs = map (body_type o fastype_of o hd) perm_ctrss;
@@ -395,8 +393,8 @@
val kks = 0 upto nn - 1;
val perm_ns = map length perm_ctr_Tsss;
- val perm_Cs = map (domain_type o body_fun_type o fastype_of o co_rec_of o
- of_fp_sugar (#xtor_co_iterss o #fp_res)) perm_fp_sugars;
+ val perm_Cs = map (fn {fp_res, fp_res_index, ...} => domain_type (body_fun_type (fastype_of
+ (co_rec_of (nth (#xtor_co_iterss fp_res) fp_res_index))))) perm_fp_sugars;
val (perm_p_Tss, (perm_q_Tssss, _, perm_f_Tssss, _)) =
mk_coiter_fun_arg_types perm_ctr_Tsss perm_Cs perm_ns (co_rec_of dtor_coiters1);
@@ -410,7 +408,7 @@
fun unpermute0 perm0_xs = permute_like_unique (op =) perm0_kks kks perm0_xs;
fun unpermute perm_xs = permute_like_unique (op =) perm_indices indices perm_xs;
- val coinduct_thmss = map (unpermute0 o conj_dests nn) coinduct_thms;
+ val coinduct_thmss = map (unpermute0 o conj_dests nn) common_coinduct_thms;
val p_iss = map (map (find_index_eq fun_arg_hs)) (unpermute perm_p_hss);
val q_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_q_hssss);
@@ -444,35 +442,32 @@
disc_corec = disc_corec, sel_corecs = sel_corecs}
end;
- fun mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss disc_coitersss
- sel_coiterssss =
+ fun mk_ctr_specs ({ctrs, discs, selss, discIs, sel_thmss, disc_excludesss, collapses, ...}
+ : ctr_sugar) p_is q_isss f_isss f_Tsss coiter_thmss disc_coiterss sel_coitersss =
let
- val {ctrs, discs, selss, discIs, sel_thmss, disc_excludesss, collapses, ...} : ctr_sugar =
- nth ctr_sugars index;
val p_ios = map SOME p_is @ [NONE];
- val discIs = #discIs (nth ctr_sugars index);
- val corec_thms = co_rec_of (nth coiter_thmsss index);
- val disc_corecs = co_rec_of (nth disc_coitersss index);
- val sel_corecss = co_rec_of (nth sel_coiterssss index);
+ val corec_thms = co_rec_of coiter_thmss;
+ val disc_corecs = co_rec_of disc_coiterss;
+ val sel_corecss = co_rec_of sel_coitersss;
in
map14 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss
disc_excludesss collapses corec_thms disc_corecs sel_corecss
end;
- fun mk_spec ({T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss,
- disc_co_itersss = disc_coitersss, sel_co_iterssss = sel_coiterssss, ...} : fp_sugar)
- p_is q_isss f_isss f_Tsss =
- {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of (nth coiterss index)),
- disc_exhausts = #disc_exhausts (nth ctr_sugars index),
+ fun mk_spec ({T, ctr_sugar as {disc_exhausts, ...}, co_iters = coiters,
+ co_iter_thmss = coiter_thmss, disc_co_iterss = disc_coiterss,
+ sel_co_itersss = sel_coitersss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
+ {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of coiters),
+ disc_exhausts = disc_exhausts,
nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs,
nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs,
nested_map_comps = map map_comp_of_bnf nested_bnfs,
- ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss
- disc_coitersss sel_coiterssss};
+ ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss coiter_thmss disc_coiterss
+ sel_coitersss};
in
((is_some gfp_sugar_thms, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
- co_induct_of coinduct_thms, strong_co_induct_of coinduct_thms, co_induct_of coinduct_thmss,
- strong_co_induct_of coinduct_thmss), lthy)
+ co_induct_of common_coinduct_thms, strong_co_induct_of common_coinduct_thms,
+ co_induct_of coinduct_thmss, strong_co_induct_of coinduct_thmss), lthy)
end;
val undef_const = Const (@{const_name undefined}, dummyT);
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Tue Feb 18 21:00:13 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 20:50:07 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Tue Feb 18 21:00:13 2014 +0100
@@ -22,7 +22,6 @@
open BNF_Comp
open BNF_FP_Util
open BNF_FP_Def_Sugar
-open BNF_LFP_Rec_Sugar
open BNF_LFP_Util
open BNF_LFP_Tactics
@@ -86,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;
@@ -121,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
@@ -246,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)) =
@@ -265,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
@@ -278,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 =>
@@ -292,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))
@@ -309,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 =>
@@ -416,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
@@ -498,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)));
@@ -518,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;
@@ -526,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)))
@@ -543,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)
@@ -594,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;
@@ -632,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
@@ -666,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 =
@@ -675,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;
@@ -691,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);
@@ -716,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)) =
@@ -731,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,
@@ -813,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;
@@ -850,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];
@@ -883,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_compat.ML Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Tue Feb 18 21:00:13 2014 +0100
@@ -2,7 +2,7 @@
Author: Jasmin Blanchette, TU Muenchen
Copyright 2013
-Compatibility layer with the old datatype package.
+Compatibility layer with the old datatype package ("datatype_compat").
*)
signature BNF_LFP_COMPAT =
@@ -32,7 +32,7 @@
fun not_mutually_recursive ss =
error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive new-style datatypes");
- val (fpT_names as fpT_name1 :: _) =
+ val fpT_names =
map (fst o dest_Type o Proof_Context.read_type_name_proper lthy false) raw_fpT_names;
fun lfp_sugar_of s =
@@ -40,7 +40,7 @@
SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar
| _ => not_datatype s);
- val {ctr_sugars = fp_ctr_sugars, ...} = lfp_sugar_of fpT_name1;
+ val fp_ctr_sugars = map (#ctr_sugar o lfp_sugar_of) fpT_names;
val fpTs0 as Type (_, var_As) :: _ = map (body_type o fastype_of o hd o #ctrs) fp_ctr_sugars;
val fpT_names' = map (fst o dest_Type) fpTs0;
@@ -52,7 +52,7 @@
fun nested_Tparentss_indicessss_of parent_Tkks (T as Type (s, _)) kk =
(case try lfp_sugar_of s of
- SOME ({T = T0, fp_res = {Ts = mutual_Ts0, ...}, ctr_sugars, ...}) =>
+ SOME ({T = T0, fp_res = {Ts = mutual_Ts0, ...}, ...}) =>
let
val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T0, T) Vartab.empty) [];
val substT = Term.typ_subst_TVars rho;
@@ -88,7 +88,7 @@
#>> pair parent_Tkks'
end;
- val ctrss = map #ctrs ctr_sugars;
+ val ctrss = map (#ctrs o #ctr_sugar o lfp_sugar_of o fst o dest_Type) mutual_Ts;
val ctr_Tsss = map (map (binder_types o substT o fastype_of)) ctrss;
in
([], kk + mutual_nn)
@@ -107,7 +107,7 @@
val kkssss = map snd Tparentss_kkssss;
val fp_sugars0 = map (lfp_sugar_of o fst o dest_Type) Ts;
- val ctrss0 = map (#ctrs o of_fp_sugar #ctr_sugars) fp_sugars0;
+ val ctrss0 = map (#ctrs o #ctr_sugar) fp_sugars0;
val ctr_Tsss0 = map (map (binder_types o fastype_of)) ctrss0;
fun apply_comps n kk =
@@ -132,9 +132,8 @@
else
((fp_sugars0, (NONE, NONE)), lthy);
- val {ctr_sugars, co_inducts = [induct], co_inductss = inductss, co_iterss,
- co_iter_thmsss = iter_thmsss, ...} :: _ = fp_sugars;
- val inducts = map the_single inductss;
+ val {common_co_inducts = [induct], ...} :: _ = fp_sugars;
+ val inducts = map (the_single o #co_inducts) fp_sugars;
fun mk_dtyp [] (TFree a) = Datatype_Aux.DtTFree a
| mk_dtyp [] (Type (s, Ts)) = Datatype_Aux.DtType (s, map (mk_dtyp []) Ts)
@@ -148,23 +147,19 @@
(kk, (T_name, map (mk_dtyp (map snd (take 1 parents))) Ts, map2 (mk_ctr_descr Ts) kksss ctrs0));
val descr = map3 mk_typ_descr kkssss Tparentss ctrss0;
- val recs = map (fst o dest_Const o co_rec_of) co_iterss;
- val rec_thms = flat (map co_rec_of iter_thmsss);
+ val recs = map (fst o dest_Const o co_rec_of o #co_iters) fp_sugars;
+ val rec_thms = maps (co_rec_of o #co_iter_thmss) fp_sugars;
- fun mk_info ({T = Type (T_name0, _), index, ...} : fp_sugar) =
- let
- val {casex, exhaust, nchotomy, injects, distincts, case_thms, case_cong, weak_case_cong,
- split, split_asm, ...} = nth ctr_sugars index;
- in
- (T_name0,
- {index = index, descr = descr, inject = injects, distinct = distincts, induct = induct,
- inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs,
- rec_rewrites = rec_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms,
- case_cong = case_cong, weak_case_cong = weak_case_cong, split = split,
- split_asm = split_asm})
- end;
+ fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar as {casex, exhaust, nchotomy, injects,
+ distincts, case_thms, case_cong, weak_case_cong, split, split_asm, ...}, ...} : fp_sugar) =
+ (T_name0,
+ {index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct,
+ inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs,
+ rec_rewrites = rec_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms,
+ case_cong = case_cong, weak_case_cong = weak_case_cong, split = split,
+ split_asm = split_asm});
- val infos = map mk_info (take nn_fp fp_sugars);
+ val infos = map_index mk_info (take nn_fp fp_sugars);
val all_notes =
(case lfp_sugar_thms of
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Tue Feb 18 21:00:13 2014 +0100
@@ -3,7 +3,7 @@
Author: Jasmin Blanchette, TU Muenchen
Copyright 2013
-Recursor sugar.
+Recursor sugar ("primrec").
*)
signature BNF_LFP_REC_SUGAR =
@@ -134,32 +134,59 @@
massage_call
end;
-fun rec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy0 =
+type basic_lfp_sugar =
+ {T: typ,
+ fp_res_index: int,
+ ctor_iters: term list,
+ ctr_defs: thm list,
+ ctr_sugar: ctr_sugar,
+ iters: term list,
+ iter_thmss: thm list list};
+
+fun basic_lfp_sugar_of ({T, fp_res = {xtor_co_iterss = ctor_iterss, ...}, fp_res_index, ctr_defs,
+ ctr_sugar, co_iters = iters, co_iter_thmss = iter_thmss, ...} : fp_sugar) =
+ {T = T, fp_res_index = fp_res_index, ctor_iters = nth ctor_iterss fp_res_index,
+ ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, iters = iters, iter_thmss = iter_thmss};
+
+fun get_basic_lfp_sugars bs arg_Ts get_indices callssss0 lthy0 =
let
- val thy = Proof_Context.theory_of lthy0;
-
val ((missing_arg_Ts, perm0_kks,
fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = ctor_iters1 :: _, ...},
co_inducts = [induct_thm], ...} :: _, (lfp_sugar_thms, _)), lthy) =
nested_to_mutual_fps Least_FP bs arg_Ts get_indices callssss0 lthy0;
+ val nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs;
+ val nested_map_comps = map map_comp_of_bnf nested_bnfs;
+ in
+ (missing_arg_Ts, perm0_kks, map basic_lfp_sugar_of fp_sugars, nested_map_idents,
+ nested_map_comps, ctor_iters1, induct_thm, lfp_sugar_thms, lthy)
+ end;
- val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars;
+fun rec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy0 =
+ let
+ val thy = Proof_Context.theory_of lthy0;
- val indices = map #index fp_sugars;
- val perm_indices = map #index perm_fp_sugars;
+ val (missing_arg_Ts, perm0_kks, basic_lfp_sugars, nested_map_idents, nested_map_comps,
+ ctor_iters1, induct_thm, lfp_sugar_thms, lthy) =
+ get_basic_lfp_sugars bs arg_Ts get_indices callssss0 lthy0;
+
+ val perm_basic_lfp_sugars = sort (int_ord o pairself #fp_res_index) basic_lfp_sugars;
- val perm_ctrss = map (#ctrs o of_fp_sugar #ctr_sugars) perm_fp_sugars;
+ val indices = map #fp_res_index basic_lfp_sugars;
+ val perm_indices = map #fp_res_index perm_basic_lfp_sugars;
+
+ val perm_ctrss = map (#ctrs o #ctr_sugar) perm_basic_lfp_sugars;
val perm_ctr_Tsss = map (map (binder_types o fastype_of)) perm_ctrss;
- val perm_lfpTs = map (body_type o fastype_of o hd) perm_ctrss;
val nn0 = length arg_Ts;
- val nn = length perm_lfpTs;
+ val nn = length perm_ctrss;
val kks = 0 upto nn - 1;
+
val perm_ns = map length perm_ctr_Tsss;
val perm_mss = map (map length) perm_ctr_Tsss;
+ val perm_ctr_offsets = map (fn kk => Integer.sum (map length (take kk perm_ctrss))) kks;
- val perm_Cs = map (body_type o fastype_of o co_rec_of o of_fp_sugar (#xtor_co_iterss o #fp_res))
- perm_fp_sugars;
+ val perm_lfpTs = map (body_type o fastype_of o hd) perm_ctrss;
+ val perm_Cs = map (body_type o fastype_of o co_rec_of o #ctor_iters) perm_basic_lfp_sugars;
val perm_fun_arg_Tssss =
mk_iter_fun_arg_types perm_ctr_Tsss perm_ns perm_mss (co_rec_of ctor_iters1);
@@ -170,6 +197,7 @@
val lfpTs = unpermute perm_lfpTs;
val Cs = unpermute perm_Cs;
+ val ctr_offsets = unpermute perm_ctr_offsets;
val As_rho = tvar_subst thy (take nn0 lfpTs) arg_Ts;
val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn res_Ts;
@@ -181,10 +209,6 @@
val perm_Cs' = map substCT perm_Cs;
- fun offset_of_ctr 0 _ = 0
- | offset_of_ctr n (({ctrs, ...} : ctr_sugar) :: ctr_sugars) =
- length ctrs + offset_of_ctr (n - 1) ctr_sugars;
-
fun call_of [i] [T] = (if exists_subtype_in Cs T then Nested_Rec else No_Rec) (i, substACT T)
| call_of [i, i'] [T, T'] = Mutual_Rec ((i, substACT T), (i', substACT T'));
@@ -198,24 +222,18 @@
rec_thm = rec_thm}
end;
- fun mk_ctr_specs index (ctr_sugars : ctr_sugar list) iter_thmsss =
- let
- val ctrs = #ctrs (nth ctr_sugars index);
- val rec_thms = co_rec_of (nth iter_thmsss index);
- val k = offset_of_ctr index ctr_sugars;
- val n = length ctrs;
- in
- map4 mk_ctr_spec ctrs (k upto k + n - 1) (nth perm_fun_arg_Tssss index) rec_thms
- end;
+ fun mk_ctr_specs fp_res_index k ctrs rec_thms =
+ map4 mk_ctr_spec ctrs (k upto k + length ctrs - 1) (nth perm_fun_arg_Tssss fp_res_index)
+ rec_thms;
- fun mk_spec ({T, index, ctr_sugars, co_iterss = iterss, co_iter_thmsss = iter_thmsss, ...}
- : fp_sugar) =
- {recx = mk_co_iter thy Least_FP (substAT T) perm_Cs' (co_rec_of (nth iterss index)),
- nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs,
- nested_map_comps = map map_comp_of_bnf nested_bnfs,
- ctr_specs = mk_ctr_specs index ctr_sugars iter_thmsss};
+ fun mk_spec ctr_offset
+ ({T, fp_res_index, ctr_sugar = {ctrs, ...}, iters, iter_thmss, ...} : basic_lfp_sugar) =
+ {recx = mk_co_iter thy Least_FP (substAT T) perm_Cs' (co_rec_of iters),
+ nested_map_idents = nested_map_idents, nested_map_comps = nested_map_comps,
+ ctr_specs = mk_ctr_specs fp_res_index ctr_offset ctrs (co_rec_of iter_thmss)};
in
- ((is_some lfp_sugar_thms, map mk_spec fp_sugars, missing_arg_Ts, induct_thm, induct_thms), lthy)
+ ((is_some lfp_sugar_thms, map2 mk_spec ctr_offsets basic_lfp_sugars, missing_arg_Ts, induct_thm,
+ induct_thms), lthy)
end;
val undef_const = Const (@{const_name undefined}, dummyT);
@@ -501,10 +519,11 @@
val actual_nn = length funs_data;
- val _ = let val ctrs = (maps (map #ctr o #ctr_specs) rec_specs) in
+ val ctrs = maps (map #ctr o #ctr_specs) rec_specs;
+ val _ =
map (fn {ctr, user_eqn, ...} => member (op =) ctrs ctr orelse
primrec_error_eqn ("argument " ^ quote (Syntax.string_of_term lthy ctr) ^
- " is not a constructor in left-hand side") user_eqn) eqns_data end;
+ " is not a constructor in left-hand side") user_eqn) eqns_data;
val defs = build_defs lthy bs mxs funs_data rec_specs has_call;
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Tue Feb 18 21:00:13 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),
--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Feb 18 21:00:13 2014 +0100
@@ -1059,8 +1059,8 @@
(* Give the inner timeout a chance. *)
val timeout_bonus = seconds 1.0
-fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) mode i n
- step subst def_assm_ts nondef_assm_ts orig_t =
+fun pick_nits_in_term state (params as {timeout, expect, ...}) mode i n step
+ subst def_assm_ts nondef_assm_ts orig_t =
let
val print_nt = if is_mode_nt mode then Output.urgent_message else K ()
val print_t = if mode = TPTP then Output.urgent_message else K ()
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Feb 18 21:00:13 2014 +0100
@@ -791,8 +791,7 @@
val ctrs2 =
(case BNF_FP_Def_Sugar.fp_sugar_of ctxt co_s of
SOME (fp_sugar as {fp = BNF_FP_Util.Greatest_FP, ...}) =>
- map dest_Const
- (#ctrs (BNF_FP_Def_Sugar.of_fp_sugar #ctr_sugars fp_sugar))
+ map dest_Const (#ctrs (#ctr_sugar fp_sugar))
| _ => [])
in
exists (fn (s', T') => s = s' andalso repair_constr_type coT T' = T)
@@ -937,7 +936,7 @@
(case BNF_FP_Def_Sugar.fp_sugar_of ctxt s of
SOME (fp_sugar as {fp = BNF_FP_Util.Greatest_FP, ...}) =>
map (apsnd (repair_constr_type T) o dest_Const)
- (#ctrs (BNF_FP_Def_Sugar.of_fp_sugar #ctr_sugars fp_sugar))
+ (#ctrs (#ctr_sugar fp_sugar))
| _ =>
if is_frac_type ctxt T then
case typedef_info ctxt s of
@@ -1465,12 +1464,12 @@
|> the |> #3 |> length))
(Datatype.get_all thy) [] @
map (apsnd length o snd) (#codatatypes (Data.get (Context.Proof ctxt))) @
- maps (fn {fp, ctr_sugars, ...} =>
- if fp = BNF_FP_Util.Greatest_FP then
- map (apsnd num_binder_types o dest_Const o #casex) ctr_sugars
- else
- [])
- (BNF_FP_Def_Sugar.fp_sugars_of ctxt)
+ map_filter (fn {fp, ctr_sugar = {casex, ...}, ...} =>
+ if fp = BNF_FP_Util.Greatest_FP then
+ SOME (apsnd num_binder_types (dest_Const casex))
+ else
+ NONE)
+ (BNF_FP_Def_Sugar.fp_sugars_of ctxt)
end
fun fixpoint_kind_of_const thy table x =
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Tue Feb 18 21:00:13 2014 +0100
@@ -31,7 +31,6 @@
val atom16_v1 = FreeName ("atom16_v1", dummy_T, Atom (16, 0))
val atom24_v1 = FreeName ("atom24_v1", dummy_T, Atom (24, 0))
val atom36_v1 = FreeName ("atom36_v1", dummy_T, Atom (36, 0))
-val atom81_v1 = FreeName ("atom81_v1", dummy_T, Atom (81, 0))
val struct_atom1_atom1_v1 =
FreeName ("struct_atom1_atom1_v1", dummy_T, Struct [Atom (1, 0), Atom (1, 0)])