--- a/src/HOL/BNF_FP_Base.thy Tue Jun 24 13:48:14 2014 +0200
+++ b/src/HOL/BNF_FP_Base.thy Tue Jun 24 13:48:14 2014 +0200
@@ -16,7 +16,7 @@
lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
by auto
-lemma predicate2D_conj: "(P \<le> Q) \<and> R \<Longrightarrow> P x y \<Longrightarrow> R \<and> Q x y"
+lemma predicate2D_conj: "P \<le> Q \<and> R \<Longrightarrow> P x y \<Longrightarrow> R \<and> Q x y"
by auto
lemma eq_sym_Unity_conv: "(x = (() = ())) = x"
--- a/src/HOL/Tools/BNF/bnf_def.ML Tue Jun 24 13:48:14 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Tue Jun 24 13:48:14 2014 +0200
@@ -83,9 +83,8 @@
val mk_map: int -> typ list -> typ list -> term -> term
val mk_rel: int -> typ list -> typ list -> term -> term
- val build_map: Proof.context -> (typ * typ -> term) -> typ * typ -> term
- val build_rel: Proof.context -> (typ * typ -> term) -> typ * typ -> term
- val build_rel': Proof.context -> typ list -> (typ * typ -> term) -> typ * typ -> term
+ val build_map: Proof.context -> typ list -> (typ * typ -> term) -> typ * typ -> term
+ val build_rel: Proof.context -> typ list -> (typ * typ -> term) -> typ * typ -> term
val flatten_type_args_of_bnf: bnf -> 'a -> 'a list -> 'a list
val map_flattened_map_args: Proof.context -> string -> (term list -> 'a list) -> term list ->
'a list
@@ -534,12 +533,12 @@
Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
end;
-fun build_map_or_rel mk const of_bnf dest blacklist ctxt build_simple =
+fun build_map_or_rel mk const of_bnf dest ctxt simpleTs build_simple =
let
fun build (TU as (T, U)) =
- if exists (curry (op =) T) blacklist then
+ if exists (curry (op =) T) simpleTs then
build_simple TU
- else if T = U andalso not (exists_subtype_in blacklist T) then
+ else if T = U andalso not (exists_subtype_in simpleTs T) then
const T
else
(case TU of
@@ -556,9 +555,8 @@
| _ => build_simple TU);
in build end;
-val build_map = build_map_or_rel mk_map HOLogic.id_const map_of_bnf dest_funT [];
-val build_rel = build_map_or_rel mk_rel HOLogic.eq_const rel_of_bnf dest_pred2T [];
-fun build_rel' ctxt blacklist = build_map_or_rel mk_rel HOLogic.eq_const rel_of_bnf dest_pred2T blacklist ctxt;
+val build_map = build_map_or_rel mk_map HOLogic.id_const map_of_bnf dest_funT;
+val build_rel = build_map_or_rel mk_rel HOLogic.eq_const rel_of_bnf dest_pred2T;
fun map_flattened_map_args ctxt s map_args fs =
let
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Jun 24 13:48:14 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Jun 24 13:48:14 2014 +0200
@@ -359,7 +359,7 @@
val cpss = map2 (map o rapp) cs pss;
- fun build_sum_inj mk_inj = build_map lthy (uncurry mk_inj o dest_sumT o snd);
+ fun build_sum_inj mk_inj = build_map lthy [] (uncurry mk_inj o dest_sumT o snd);
fun build_dtor_corec_arg _ [] [cg] = cg
| build_dtor_corec_arg T [cq] [cg, cg'] =
@@ -574,7 +574,7 @@
if T = U then
x
else
- build_map lthy (indexify (perhaps (try (snd o HOLogic.dest_prodT)) o snd) Cs
+ build_map lthy [] (indexify (perhaps (try (snd o HOLogic.dest_prodT)) o snd) Cs
(fn kk => fn TU => maybe_tick TU (nth us kk) (nth frecs kk))) (T, U) $ x;
val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_rec))) xsss x_Tssss;
@@ -634,6 +634,14 @@
(coinduct_attrs, common_coinduct_attrs)
end;
+fun postproc_coinduct nn prop prop_conj =
+ Drule.zero_var_indexes
+ #> `(conj_dests nn)
+ #>> map (fn thm => Thm.permute_prems 0 nn (thm RS prop))
+ ##> (fn thm => Thm.permute_prems 0 nn
+ (if nn = 1 then thm RS prop
+ else funpow nn (fn thm => reassoc_conjs (thm RS prop_conj)) thm));
+
fun derive_rel_coinduct0_thm_for_types lthy fpA_Ts ns As Bs mss ctr_sugars abs_inverses abs_injects
ctor_injects dtor_ctors rel_pre_defs ctor_defss dtor_rel_coinduct =
let
@@ -666,18 +674,12 @@
(mk_discss fpBs Bs, mk_selsss fpBs Bs))
end;
- fun choose_relator (A, B) = the (find_first (fn t =>
- let
- val T = fastype_of t
- val arg1T = domain_type T;
- val arg2T = domain_type (range_type T);
- in
- A = arg1T andalso B = arg2T
- end) (Rs @ IRs));
+ fun choose_relator AB = the (find_first
+ (fastype_of #> binder_types #> (fn [T1, T2] => AB = (T1, T2))) (Rs @ IRs));
val premises =
let
- fun build_the_rel A B = build_rel' lthy fpA_Ts choose_relator (A, B);
+ fun build_the_rel A B = build_rel lthy fpA_Ts choose_relator (A, B);
fun build_rel_app selA_t selB_t =
(build_the_rel (fastype_of selA_t) (fastype_of selB_t )) $ selA_t $ selB_t
@@ -685,7 +687,7 @@
fun mk_prem_ctr_concls n k discA_t selA_ts discB_t selB_ts =
(if k = n then [] else [HOLogic.mk_eq (discA_t, discB_t)]) @
(case (selA_ts, selB_ts) of
- ([],[]) => []
+ ([], []) => []
| (_ :: _, _ :: _) =>
[Library.foldr HOLogic.mk_imp (if n = 1 then [] else [discA_t, discB_t],
Library.foldr1 HOLogic.mk_conj (map2 build_rel_app selA_ts selB_ts))]);
@@ -703,36 +705,19 @@
end;
val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
- (map2 mk_leq IRs (map (build_rel lthy choose_relator) (fpA_Ts ~~ fpB_Ts))));
-
- (*
- fun string_of_list f Ts = "[" ^ (fold_rev (curry op ^) (separate ", " (map f Ts)) "") ^ "]"
- val _ = writeln ("Premises: " ^ string_of_list (Syntax.string_of_term names_lthy) premises)
- val _ = writeln ("Goal: " ^ Syntax.string_of_term names_lthy goal)
- val _ = writeln ("derive_rel_coinduct0_thm_for_types " ^ string_of_list (Syntax.string_of_typ names_lthy) fpA_Ts)
- *)
+ (map2 mk_leq IRs (map (build_rel lthy [] choose_relator) (fpA_Ts ~~ fpB_Ts))));
val rel_coinduct0_thm = Goal.prove_sorry lthy [] premises goal
(fn {context = ctxt, prems = prems} =>
mk_rel_coinduct0_tac ctxt dtor_rel_coinduct (map (certify ctxt) IRs) prems
- (map #exhaust ctr_sugars) (map (flat o #disc_thmss) ctr_sugars) (map (flat o #sel_thmss)
- ctr_sugars) ctor_defss dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses)
+ (map #exhaust ctr_sugars) (map (flat o #disc_thmss) ctr_sugars)
+ (map (flat o #sel_thmss) ctr_sugars) ctor_defss dtor_ctors ctor_injects abs_injects
+ rel_pre_defs abs_inverses)
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation;
-
- val nn = length fpA_Ts;
- val predicate2D = @{thm predicate2D};
- val predicate2D_conj = @{thm predicate2D_conj};
-
- val postproc =
- Drule.zero_var_indexes
- #> `(conj_dests nn)
- #>> map (fn thm => Thm.permute_prems 0 nn (thm RS predicate2D))
- ##> (fn thm => Thm.permute_prems 0 nn
- (if nn = 1 then thm RS predicate2D
- else funpow nn (fn thm => reassoc_conjs (thm RS predicate2D_conj)) thm));
in
- (postproc rel_coinduct0_thm, coinduct_attrs fpA_Ts ctr_sugars mss)
+ (postproc_coinduct (length fpA_Ts) @{thm predicate2D} @{thm predicate2D_conj} rel_coinduct0_thm,
+ coinduct_attrs fpA_Ts ctr_sugars mss)
end;
fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, ((pgss, cqgsss), _))
@@ -785,7 +770,7 @@
fold_rev Term.lambda [u, v] (HOLogic.mk_disj (uvr, uv_eq))) us vs uvrs uv_eqs;
fun build_the_rel rs' T Xs_T =
- build_rel lthy (fn (_, X) => nth rs' (find_index (curry (op =) X) Xs)) (T, Xs_T)
+ build_rel lthy [] (fn (_, X) => nth rs' (find_index (curry (op =) X) Xs)) (T, Xs_T)
|> Term.subst_atomic_types (Xs ~~ fpTs);
fun build_rel_app rs' usel vsel Xs_T =
@@ -826,20 +811,12 @@
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation;
- val postproc =
- Drule.zero_var_indexes
- #> `(conj_dests nn)
- #>> map (fn thm => Thm.permute_prems 0 nn (thm RS mp))
- ##> (fn thm => Thm.permute_prems 0 nn
- (if nn = 1 then thm RS mp
- else funpow nn (fn thm => reassoc_conjs (thm RS mp_conj)) thm));
-
val rel_eqs = map rel_eq_of_bnf pre_bnfs;
val rel_monos = map rel_mono_of_bnf pre_bnfs;
val dtor_coinducts =
[dtor_coinduct, mk_strong_coinduct_thm dtor_coinduct rel_eqs rel_monos mk_vimage2p lthy]
in
- map2 (postproc oo prove) dtor_coinducts goals
+ map2 (postproc_coinduct nn mp mp_conj oo prove) dtor_coinducts goals
end;
fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
@@ -864,7 +841,7 @@
let val T = fastype_of cqg in
if exists_subtype_in Cs T then
let val U = mk_U T in
- build_map lthy (indexify fst (map2 (curry mk_sumT) fpTs Cs) (fn kk => fn _ =>
+ build_map lthy [] (indexify fst (map2 (curry mk_sumT) fpTs Cs) (fn kk => fn _ =>
tack (nth cs kk, nth us kk) (nth gcorecs kk))) (T, U) $ cqg
end
else
@@ -1336,7 +1313,7 @@
val lhs = selB $ (Term.list_comb (map_term, fs) $ ta);
val lhsT = fastype_of lhs;
val map_rhsT = map_atyps (perhaps (AList.lookup (op =) (Bs ~~ As))) lhsT;
- val map_rhs = build_map lthy
+ val map_rhs = build_map lthy []
(the o (AList.lookup (op =) ((As ~~ Bs) ~~ fs))) (map_rhsT, lhsT);
val rhs = (case map_rhs of
Const (@{const_name id}, _) => selA $ ta
@@ -1592,8 +1569,8 @@
val ((rel_coinduct_thms, rel_coinduct_thm),
(rel_coinduct_attrs, common_rel_coinduct_attrs)) =
- derive_rel_coinduct0_thm_for_types lthy fpTs ns As Bs mss ctr_sugars abs_inverses abs_injects
- ctor_injects dtor_ctors pre_rel_defs ctr_defss rel_xtor_co_induct_thm;
+ derive_rel_coinduct0_thm_for_types lthy fpTs ns As Bs mss ctr_sugars abs_inverses
+ abs_injects ctor_injects dtor_ctors pre_rel_defs ctr_defss rel_xtor_co_induct_thm;
val sel_corec_thmss = map flat sel_corec_thmsss;
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Jun 24 13:48:14 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Jun 24 13:48:14 2014 +0200
@@ -44,6 +44,7 @@
val basic_simp_thms = @{thms simp_thms(7,8,12,14,22,24)};
val more_simp_thms = basic_simp_thms @ @{thms simp_thms(11,15,16,21)};
+val simp_thms' = @{thms simp_thms(6,7,8,11,12,15,16,22,24)};
val sumprod_thms_map = @{thms id_apply map_prod_simp prod.case sum.case map_sum.simps};
val sumprod_thms_set =
@@ -218,12 +219,12 @@
arg_cong2}) RS iffD1)) THEN'
atac THEN' atac THEN' hyp_subst_tac ctxt THEN' dtac assm THEN'
REPEAT_DETERM o etac conjE))) 1 THEN
- Local_Defs.unfold_tac ctxt ((discs RL @{thms iffD2[OF eq_True] iffD2[OF eq_False]}) @
- sels @ @{thms simp_thms(6,7,8,11,12,15,16,22,24)}) THEN
+ Local_Defs.unfold_tac ctxt ((discs RL @{thms iffD2[OF eq_True] iffD2[OF eq_False]}) @ sels
+ @ simp_thms') THEN
Local_Defs.unfold_tac ctxt (dtor_ctor :: rel_pre_def :: abs_inverse :: ctor_inject ::
- abs_inject :: ctor_defs @ @{thms BNF_Comp.id_bnf_comp_def rel_sum_simps rel_prod_apply
- vimage2p_def Inl_Inr_False iffD2[OF eq_False Inr_not_Inl] sum.inject prod.inject
- simp_thms(6,7,8,11,12,15,16,22,24)}) THEN
+ abs_inject :: ctor_defs @ simp_thms' @ @{thms BNF_Comp.id_bnf_comp_def rel_sum_simps
+ rel_prod_apply vimage2p_def Inl_Inr_False iffD2[OF eq_False Inr_not_Inl] sum.inject
+ prod.inject}) THEN
REPEAT_DETERM (HEADGOAL ((REPEAT_DETERM o etac conjE) THEN' (REPEAT_DETERM o rtac conjI) THEN'
(rtac refl ORELSE' atac))))
cts assms exhausts discss selss ctor_defss dtor_ctors ctor_injects abs_injects rel_pre_defs
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Tue Jun 24 13:48:14 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Tue Jun 24 13:48:14 2014 +0200
@@ -340,11 +340,11 @@
val (TY, (U, X)) = TU |> dest_co_algT ||> dest_co_productT;
val T = mk_co_algT TY U;
in
- (case try (force_typ names_lthy T o build_map lthy co_proj1_const o dest_funT) T of
+ (case try (force_typ names_lthy T o build_map lthy [] co_proj1_const o dest_funT) T of
SOME f => mk_co_product f
(fst (fst (mk_rec NONE recs lthy (mk_co_algT TY X))))
| NONE => mk_map_co_product
- (build_map lthy co_proj1_const
+ (build_map lthy [] co_proj1_const
(dest_funT (mk_co_algT (dest_co_productT TY |> fst) U)))
(HOLogic.id_const X))
end)
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Jun 24 13:48:14 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Jun 24 13:48:14 2014 +0200
@@ -239,7 +239,7 @@
let
fun check_no_call t = if has_call t then unexpected_corec_call ctxt t else ();
- val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o snd);
+ val build_map_Inl = build_map ctxt [] (uncurry Inl_const o dest_sumT o snd);
fun massage_mutual_call bound_Ts U T t =
if has_call t then
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Tue Jun 24 13:48:14 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Tue Jun 24 13:48:14 2014 +0200
@@ -68,7 +68,7 @@
fun check_no_call t = if has_call t then unexpected_rec_call ctxt t else ();
val typof = curry fastype_of1 bound_Ts;
- val build_map_fst = build_map ctxt (fst_const o fst);
+ val build_map_fst = build_map ctxt [] (fst_const o fst);
val yT = typof y;
val yU = typof y';
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Jun 24 13:48:14 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Jun 24 13:48:14 2014 +0200
@@ -275,7 +275,7 @@
fun mk_rec_arg_arg (x as Free (_, T)) =
let val U = B_ify T in
- if T = U then x else build_map lthy2 (the o AList.lookup (op =) ABgs) (T, U) $ x
+ if T = U then x else build_map lthy2 [] (the o AList.lookup (op =) ABgs) (T, U) $ x
end;
fun mk_rec_o_map_arg rec_arg_T h =