--- a/src/HOL/BNF_FP_Base.thy Thu Mar 06 22:15:01 2014 +0100
+++ b/src/HOL/BNF_FP_Base.thy Fri Mar 07 01:02:21 2014 +0100
@@ -28,12 +28,6 @@
lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
by simp
-lemma prod_all_impI: "(\<And>x y. P (x, y) \<Longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
-by clarify
-
-lemma prod_all_impI_step: "(\<And>x. \<forall>y. P (x, y) \<longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
-by auto
-
lemma pointfree_idE: "f \<circ> g = id \<Longrightarrow> f (g x) = x"
unfolding comp_def fun_eq_iff by simp
@@ -58,9 +52,6 @@
"case_sum f (case_sum f' g') (Inr p) = case_sum f' g' p"
by auto
-lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
-by simp
-
lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P"
by blast
@@ -76,9 +67,6 @@
fix x from assms show "s = f x \<longrightarrow> P" by (cases x) auto
qed
-lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
-by (cases s) auto
-
lemma case_sum_if:
"case_sum f g (if p then Inl x else Inr y) = (if p then f x else g y)"
by simp
--- a/src/HOL/BNF_GFP.thy Thu Mar 06 22:15:01 2014 +0100
+++ b/src/HOL/BNF_GFP.thy Fri Mar 07 01:02:21 2014 +0100
@@ -21,6 +21,12 @@
Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj}
*}
+lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+by simp
+
+lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+by (cases s) auto
+
lemma not_TrueE: "\<not> True \<Longrightarrow> P"
by (erule notE, rule TrueI)
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Mar 06 22:15:01 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Mar 07 01:02:21 2014 +0100
@@ -365,7 +365,7 @@
end;
(*avoid "'a itself" arguments in corecursors*)
-fun repair_nullary_single_ctr [[]] = [[@{typ unit}]]
+fun repair_nullary_single_ctr [[]] = [[HOLogic.unitT]]
| repair_nullary_single_ctr Tss = Tss;
fun mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss fun_Ts =
@@ -479,7 +479,7 @@
(fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_rec,
map4 (fn ctor_rec_absT => fn rep => fn fs => fn xsss =>
mk_case_absumprod ctor_rec_absT rep fs
- (map (HOLogic.mk_tuple o map HOLogic.mk_tuple) xsss) (map flat_rec_arg_args xsss))
+ (map (mk_tuple_balanced o map HOLogic.mk_tuple) xsss) (map flat_rec_arg_args xsss))
ctor_rec_absTs reps fss xssss)))
end;
@@ -978,7 +978,7 @@
val unfreeze_fp = Term.typ_subst_atomic (Xs ~~ fake_Ts);
val ctrXs_Tsss = map (map (map freeze_fp)) fake_ctr_Tsss;
- val ctrXs_repTs = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss;
+ val ctrXs_repTs = map mk_sumprodT_balanced ctrXs_Tsss;
val fp_eqs =
map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctrXs_repTs;
@@ -1196,7 +1196,7 @@
fun mk_map_thm ctr_def' cxIn =
fold_thms lthy [ctr_def']
(unfold_thms lthy (o_apply :: pre_map_def ::
- (if fp = Least_FP then [] else [ctor_dtor, dtor_ctor]) @ sum_prod_thms_map @
+ (if fp = Least_FP then [] else [ctor_dtor, dtor_ctor]) @ sumprod_thms_map @
abs_inverses)
(cterm_instantiate_pos (nones @ [SOME cxIn])
(if fp = Least_FP then fp_map_thm else fp_map_thm RS ctor_cong)))
@@ -1205,7 +1205,7 @@
fun mk_set_thm fp_set_thm ctr_def' cxIn =
fold_thms lthy [ctr_def']
(unfold_thms lthy (pre_set_defs @ nested_set_maps @ nesting_set_maps @
- (if fp = Least_FP then [] else [dtor_ctor]) @ sum_prod_thms_set @
+ (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_set @
abs_inverses)
(cterm_instantiate_pos [SOME cxIn] fp_set_thm))
|> singleton (Proof_Context.export names_lthy no_defs_lthy);
@@ -1221,7 +1221,7 @@
fun mk_rel_thm postproc ctr_defs' cxIn cyIn =
fold_thms lthy ctr_defs'
(unfold_thms lthy (pre_rel_def :: abs_inverse ::
- (if fp = Least_FP then [] else [dtor_ctor]) @ sum_prod_thms_rel @
+ (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_rel @
@{thms vimage2p_def Inl_Inr_False})
(cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
|> postproc
@@ -1396,7 +1396,7 @@
abss ~~ abs_injects ~~ abs_inverses ~~ type_definitions ~~ ctr_bindingss ~~ ctr_mixfixess ~~
ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_defaultsss)
|> wrap_types_etc
- |> fp_case fp derive_note_induct_recs_thms_for_types
+ |> case_fp fp derive_note_induct_recs_thms_for_types
derive_note_coinduct_corecs_thms_for_types;
val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Mar 06 22:15:01 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Fri Mar 07 01:02:21 2014 +0100
@@ -7,9 +7,9 @@
signature BNF_FP_DEF_SUGAR_TACTICS =
sig
- val sum_prod_thms_map: thm list
- val sum_prod_thms_set: thm list
- val sum_prod_thms_rel: thm list
+ val sumprod_thms_map: thm list
+ val sumprod_thms_set: thm list
+ val sumprod_thms_rel: thm list
val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list ->
thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list ->
@@ -37,12 +37,12 @@
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 sum_prod_thms_map = @{thms id_apply map_prod_simp prod.case sum.case map_sum.simps};
-val sum_prod_thms_set =
+val sumprod_thms_map = @{thms id_apply map_prod_simp prod.case sum.case map_sum.simps};
+val sumprod_thms_set =
@{thms UN_empty UN_insert Un_empty_left Un_empty_right Un_iff UN_simps(10) UN_iff
Union_Un_distrib image_iff o_apply map_prod_simp
mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps};
-val sum_prod_thms_rel = @{thms rel_prod_apply rel_sum_simps id_apply};
+val sumprod_thms_rel = @{thms rel_prod_apply rel_sum_simps id_apply};
fun hhf_concl_conv cv ctxt ct =
(case Thm.term_of ct of
@@ -87,13 +87,13 @@
val rec_unfold_thms =
@{thms comp_def convol_def fst_conv id_def case_prod_Pair_iden snd_conv split_conv
- case_unit_Unity} @ sum_prod_thms_map;
+ case_unit_Unity} @ sumprod_thms_map;
fun mk_rec_tac pre_map_defs map_idents rec_defs ctor_rec fp_abs_inverse abs_inverse ctr_def ctxt =
unfold_thms_tac ctxt (ctr_def :: ctor_rec :: fp_abs_inverse :: abs_inverse :: rec_defs @
pre_map_defs @ map_idents @ rec_unfold_thms) THEN HEADGOAL (rtac refl);
-val corec_unfold_thms = @{thms id_def} @ sum_prod_thms_map;
+val corec_unfold_thms = @{thms id_def} @ sumprod_thms_map;
fun mk_corec_tac corec_defs map_idents ctor_dtor_corec pre_map_def abs_inverse ctr_def ctxt =
let
@@ -121,7 +121,7 @@
pre_set_defs =
HEADGOAL (EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ fp_abs_inverses @ abs_inverses @ set_maps @
- sum_prod_thms_set)),
+ sumprod_thms_set)),
solve_prem_prem_tac ctxt]) (rev kks)));
fun mk_induct_discharge_prem_tac ctxt nn n fp_abs_inverses abs_inverses set_maps pre_set_defs m k
@@ -153,7 +153,7 @@
(Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv ctr_def))) ctxt) ctxt) THEN'
SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: sels)) THEN'
SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: fp_abs_inverse :: abs_inverse :: dtor_ctor ::
- sels @ sum_prod_thms_rel @ @{thms o_apply vimage2p_def})) THEN'
+ sels @ sumprod_thms_rel @ @{thms o_apply vimage2p_def})) THEN'
(atac ORELSE' REPEAT o etac conjE THEN'
full_simp_tac
(ss_only (@{thm prod.inject} :: no_refl discs @ rel_eqs @ more_simp_thms) ctxt) THEN'
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Thu Mar 06 22:15:01 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Fri Mar 07 01:02:21 2014 +0100
@@ -52,20 +52,20 @@
fun of_fp_res get =
map (fn {fp_res, fp_res_index, ...} => nth (get fp_res) fp_res_index) fp_sugars;
- fun mk_co_algT T U = fp_case fp (T --> U) (U --> T);
- fun co_swap pair = fp_case fp I swap pair;
+ fun mk_co_algT T U = case_fp fp (T --> U) (U --> T);
+ fun co_swap pair = case_fp fp I swap pair;
val mk_co_comp = HOLogic.mk_comp o co_swap;
- val co_productC = BNF_FP_Rec_Sugar_Util.fp_case fp @{type_name prod} @{type_name sum};
+ val co_productC = BNF_FP_Rec_Sugar_Util.case_fp fp @{type_name prod} @{type_name sum};
val dest_co_algT = co_swap o dest_funT;
- val co_alg_argT = fp_case fp range_type domain_type;
- val co_alg_funT = fp_case fp domain_type range_type;
- val mk_co_product = curry (fp_case fp mk_convol mk_case_sum);
- val mk_map_co_product = fp_case fp mk_prod_map mk_map_sum;
- val co_proj1_const = fp_case fp (fst_const o fst) (uncurry Inl_const o dest_sumT o snd);
- val mk_co_productT = curry (fp_case fp HOLogic.mk_prodT mk_sumT);
- val dest_co_productT = fp_case fp HOLogic.dest_prodT dest_sumT;
- val rewrite_comp_comp = fp_case fp @{thm rewriteL_comp_comp} @{thm rewriteR_comp_comp};
+ val co_alg_argT = case_fp fp range_type domain_type;
+ val co_alg_funT = case_fp fp domain_type range_type;
+ val mk_co_product = curry (case_fp fp mk_convol mk_case_sum);
+ val mk_map_co_product = case_fp fp mk_prod_map mk_map_sum;
+ val co_proj1_const = case_fp fp (fst_const o fst) (uncurry Inl_const o dest_sumT o snd);
+ val mk_co_productT = curry (case_fp fp HOLogic.mk_prodT mk_sumT);
+ val dest_co_productT = case_fp fp HOLogic.dest_prodT dest_sumT;
+ val rewrite_comp_comp = case_fp fp @{thm rewriteL_comp_comp} @{thm rewriteR_comp_comp};
val fp_absT_infos = map #absT_info fp_sugars;
val fp_bnfs = of_fp_res #bnfs;
@@ -115,7 +115,7 @@
val ctors = map2 (force_typ names_lthy o (fn T => dummyT --> T)) fpTs (of_fp_res #ctors);
val dtors = map2 (force_typ names_lthy o (fn T => T --> dummyT)) fpTs (of_fp_res #dtors);
in
- ((ctors, dtors), `(map (Term.subst_atomic_types thetaBs)) (fp_case fp ctors dtors))
+ ((ctors, dtors), `(map (Term.subst_atomic_types thetaBs)) (case_fp fp ctors dtors))
end;
val absATs = map (domain_type o fastype_of) ctors;
@@ -283,7 +283,7 @@
end;
fun mk_co_comp_abs_rep fp_absT absT fp_abs fp_rep abs rep t =
- fp_case fp (HOLogic.mk_comp (HOLogic.mk_comp (t, mk_abs absT abs), mk_rep fp_absT fp_rep))
+ case_fp fp (HOLogic.mk_comp (HOLogic.mk_comp (t, mk_abs absT abs), mk_rep fp_absT fp_rep))
(HOLogic.mk_comp (mk_abs fp_absT fp_abs, HOLogic.mk_comp (mk_rep absT rep, t)));
fun mk_rec b_opt recs lthy TU =
@@ -358,7 +358,7 @@
fold_rev Term.absfree rec_strs' t)) lthy |>> apsnd snd)
end;
- val recN = fp_case fp ctor_recN dtor_corecN;
+ val recN = case_fp fp ctor_recN dtor_corecN;
fun mk_recs lthy =
fold2 (fn TU => fn b => fn ((recs, defs), lthy) =>
mk_rec (SOME b) recs lthy TU |>> (fn (f, d) => (f :: recs, d :: defs)))
@@ -403,10 +403,10 @@
val fp_xtor_co_recs = map (mk_pointfree lthy) (of_fp_res #xtor_co_rec_thms);
- val fold_thms = fp_case fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} ::
+ val fold_thms = case_fp fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} ::
map (fn thm => thm RS rewrite_comp_comp) @{thms map_prod.comp map_sum.comp} @
@{thms id_apply comp_id id_comp map_prod.comp map_prod.id map_sum.comp map_sum.id};
- val rec_thms = fold_thms @ fp_case fp
+ val rec_thms = fold_thms @ case_fp fp
@{thms fst_convol map_prod_o_convol convol_o}
@{thms case_sum_o_inj(1) case_sum_o_map_sum o_case_sum};
@@ -415,7 +415,7 @@
val map_thms = no_refl (maps (fn bnf =>
let val map_comp0 = map_comp0_of_bnf bnf RS sym
in [map_comp0, map_comp0 RS rewrite_comp_comp, map_id0_of_bnf bnf] end) fp_nesty_bnfs) @
- remove eq_thm_prop_untyped (fp_case fp @{thm comp_assoc[symmetric]} @{thm comp_assoc})
+ remove eq_thm_prop_untyped (case_fp fp @{thm comp_assoc[symmetric]} @{thm comp_assoc})
(map2 (fn thm => fn bnf =>
@{thm type_copy_map_comp0_undo} OF
(replicate 3 thm @ unfold_map [map_comp0_of_bnf bnf]) RS
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Thu Mar 06 22:15:01 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Fri Mar 07 01:02:21 2014 +0100
@@ -101,7 +101,7 @@
xs ([], ([], []));
fun key_of_fp_eqs fp fpTs fp_eqs =
- Type (fp_case fp "l" "g", fpTs @ maps (fn (x, T) => [TFree x, T]) fp_eqs);
+ Type (case_fp fp "l" "g", fpTs @ maps (fn (x, T) => [TFree x, T]) fp_eqs);
fun get_indices callers t =
callers
@@ -191,7 +191,7 @@
val ctr_Tsss = map (map binder_types) ctr_Tss;
val ctrXs_Tsss = map4 (map2 o map2 oo freeze_fpTs_call) kks fpTs callssss ctr_Tsss;
- val ctrXs_repTs = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss;
+ val ctrXs_repTs = map mk_sumprodT_balanced ctrXs_Tsss;
val ns = map length ctr_Tsss;
val kss = map (fn n => 1 upto n) ns;
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Thu Mar 06 22:15:01 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Fri Mar 07 01:02:21 2014 +0100
@@ -10,7 +10,7 @@
sig
datatype fp_kind = Least_FP | Greatest_FP
- val fp_case: fp_kind -> 'a -> 'a -> 'a
+ val case_fp: fp_kind -> 'a -> 'a -> 'a
val flat_rec_arg_args: 'a list list -> 'a list
@@ -48,8 +48,8 @@
datatype fp_kind = Least_FP | Greatest_FP;
-fun fp_case Least_FP l _ = l
- | fp_case Greatest_FP _ g = g;
+fun case_fp Least_FP l _ = l
+ | case_fp Greatest_FP _ g = g;
fun flat_rec_arg_args xss =
(* FIXME (once the old datatype package is phased out): The first line below gives the preferred
@@ -107,8 +107,8 @@
fun mk_co_rec thy fp fpT Cs t =
let
val ((f_Cs, prebody), body) = strip_type (fastype_of t) |>> split_last;
- val fpT0 = fp_case fp prebody body;
- val Cs0 = distinct (op =) (map (fp_case fp body_type domain_type) f_Cs);
+ val fpT0 = case_fp fp prebody body;
+ val Cs0 = distinct (op =) (map (case_fp fp body_type domain_type) f_Cs);
val rho = tvar_subst thy (fpT0 :: Cs0) (fpT :: Cs);
in
Term.subst_TVars rho t
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Mar 06 22:15:01 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Mar 07 01:02:21 2014 +0100
@@ -128,7 +128,7 @@
val split_conj_prems: int -> thm -> thm
val mk_sumTN: typ list -> typ
- val mk_sumTN_balanced: typ list -> typ
+ val mk_sumprodT_balanced: typ list list -> typ
val mk_proj: typ -> int -> int -> term
@@ -143,7 +143,7 @@
val mk_Inl: typ -> term -> term
val mk_Inr: typ -> term -> term
- val mk_InN: typ list -> term -> int -> term
+ val mk_tuple_balanced: term list -> term
val mk_absumprod: typ -> term -> int -> int -> term list -> term
val dest_sumT: typ -> typ * typ
@@ -155,7 +155,6 @@
val mk_If: term -> term -> term -> term
val mk_union: term * term -> term
- val mk_sumEN: int -> thm
val mk_absumprodE: thm -> int list -> thm
val mk_sum_caseN: int -> int -> thm
@@ -331,7 +330,7 @@
val selN = "sel"
val sel_corecN = selN ^ "_" ^ corecN
-fun co_prefix fp = (if fp = Greatest_FP then "co" else "");
+fun co_prefix fp = case_fp fp "" "co";
fun add_components_of_typ (Type (s, Ts)) =
cons (Long_Name.base_name s) #> fold_rev add_components_of_typ Ts
@@ -343,16 +342,20 @@
val dest_sumTN_balanced = Balanced_Tree.dest dest_sumT;
-(* TODO: move something like this to "HOLogic"? *)
-fun dest_tupleT 0 @{typ unit} = []
- | dest_tupleT 1 T = [T]
- | dest_tupleT n (Type (@{type_name prod}, [T, T'])) = T :: dest_tupleT (n - 1) T';
+fun dest_tupleT_balanced 0 @{typ unit} = []
+ | dest_tupleT_balanced n T = Balanced_Tree.dest HOLogic.dest_prodT n T;
-fun dest_absumprodT absT repT n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o mk_repT absT repT;
+fun dest_absumprodT absT repT n ms =
+ map2 dest_tupleT_balanced ms o dest_sumTN_balanced n o mk_repT absT repT;
val mk_sumTN = Library.foldr1 mk_sumT;
val mk_sumTN_balanced = Balanced_Tree.make mk_sumT;
+fun mk_tupleT_balanced [] = HOLogic.unitT
+ | mk_tupleT_balanced Ts = Balanced_Tree.make HOLogic.mk_prodT Ts;
+
+val mk_sumprodT_balanced = mk_sumTN_balanced o map mk_tupleT_balanced;
+
fun mk_proj T n k =
let val (binders, _) = strip_typeN n T in
fold_rev (fn T => fn t => Abs (Name.uu, T, t)) binders (Bound (n - k - 1))
@@ -371,11 +374,7 @@
fun Inr_const LT RT = Const (@{const_name Inr}, RT --> mk_sumT (LT, RT));
fun mk_Inr LT t = Inr_const LT (fastype_of t) $ t;
-fun mk_InN [_] t 1 = t
- | mk_InN (_ :: Ts) t 1 = mk_Inl (mk_sumTN Ts) t
- | mk_InN (LT :: Ts) t m = mk_Inr LT (mk_InN Ts t (m - 1))
- | mk_InN Ts t _ = raise (TYPE ("mk_InN", Ts, [t]));
-
+(* FIXME: reuse "mk_inj" in function package *)
fun mk_InN_balanced sum_T n t k =
let
fun repair_types T (Const (s as @{const_name Inl}, _) $ t) = repair_inj_types T s fst t
@@ -390,9 +389,12 @@
|> repair_types sum_T
end;
+fun mk_tuple_balanced [] = HOLogic.unit
+ | mk_tuple_balanced ts = Balanced_Tree.make HOLogic.mk_prod ts;
+
fun mk_absumprod absT abs0 n k ts =
let val abs = mk_abs absT abs0;
- in abs $ mk_InN_balanced (domain_type (fastype_of abs)) n (HOLogic.mk_tuple ts) k end;
+ in abs $ mk_InN_balanced (domain_type (fastype_of abs)) n (mk_tuple_balanced ts) k end;
fun mk_case_sum (f, g) =
let
@@ -434,24 +436,26 @@
if i = n then th else split n (i + 1) (conjI RSN (i, th)) handle THM _ => th;
in split limit 1 th end;
-fun mk_sumEN 1 = @{thm one_pointE}
- | mk_sumEN 2 = @{thm sumE}
- | mk_sumEN n =
- (fold (fn i => fn thm => @{thm obj_sumE_f} RSN (i, thm)) (2 upto n - 1) @{thm obj_sumE}) OF
- replicate n (impI RS allI);
-
fun mk_obj_sumEN_balanced n =
Balanced_Tree.make (fn (thm1, thm2) => thm1 RSN (1, thm2 RSN (2, @{thm obj_sumE_f})))
(replicate n asm_rl);
-fun mk_tupled_allIN 0 = @{thm unit_all_impI}
- | mk_tupled_allIN 1 = @{thm impI[THEN allI]}
- | mk_tupled_allIN 2 = @{thm prod_all_impI} (*optimization*)
- | mk_tupled_allIN n = mk_tupled_allIN (n - 1) RS @{thm prod_all_impI_step};
+fun mk_tupled_allIN_balanced 0 = @{thm unit_all_impI}
+ | mk_tupled_allIN_balanced n =
+ let
+ val (tfrees, _) = BNF_Util.mk_TFrees n @{context};
+ val T = mk_tupleT_balanced tfrees;
+ in
+ @{thm asm_rl[of "ALL x. P x --> Q x" for P Q]}
+ |> Drule.instantiate' [SOME (ctyp_of @{theory} T)] []
+ |> Raw_Simplifier.rewrite_goals_rule @{context} @{thms split_paired_All[THEN eq_reflection]}
+ |> (fn thm => impI RS funpow n (fn th => allI RS th) thm)
+ |> Thm.varifyT_global
+ end;
fun mk_absumprodE type_definition ms =
let val n = length ms in
- mk_obj_sumEN_balanced n OF map mk_tupled_allIN ms RS
+ mk_obj_sumEN_balanced n OF map mk_tupled_allIN_balanced ms RS
(type_definition RS @{thm type_copy_obj_one_point_absE})
end;
@@ -519,16 +523,16 @@
map_cong0s =
let
val n = length sym_map_comps;
- val rewrite_comp_comp2 = fp_case fp @{thm rewriteR_comp_comp2} @{thm rewriteL_comp_comp2};
- val rewrite_comp_comp = fp_case fp @{thm rewriteR_comp_comp} @{thm rewriteL_comp_comp};
- val map_cong_passive_args1 = replicate m (fp_case fp @{thm id_comp} @{thm comp_id} RS fun_cong);
+ val rewrite_comp_comp2 = case_fp fp @{thm rewriteR_comp_comp2} @{thm rewriteL_comp_comp2};
+ val rewrite_comp_comp = case_fp fp @{thm rewriteR_comp_comp} @{thm rewriteL_comp_comp};
+ val map_cong_passive_args1 = replicate m (case_fp fp @{thm id_comp} @{thm comp_id} RS fun_cong);
val map_cong_active_args1 = replicate n (if is_rec
- then fp_case fp @{thm convol_o} @{thm o_case_sum} RS fun_cong
+ then case_fp fp @{thm convol_o} @{thm o_case_sum} RS fun_cong
else refl);
- val map_cong_passive_args2 = replicate m (fp_case fp @{thm comp_id} @{thm id_comp} RS fun_cong);
+ val map_cong_passive_args2 = replicate m (case_fp fp @{thm comp_id} @{thm id_comp} RS fun_cong);
val map_cong_active_args2 = replicate n (if is_rec
- then fp_case fp @{thm map_prod_o_convol_id} @{thm case_sum_o_map_sum_id}
- else fp_case fp @{thm id_comp} @{thm comp_id} RS fun_cong);
+ then case_fp fp @{thm map_prod_o_convol_id} @{thm case_sum_o_map_sum_id}
+ else case_fp fp @{thm id_comp} @{thm comp_id} RS fun_cong);
fun mk_map_congs passive active = map (fn thm => thm OF (passive @ active) RS ext) map_cong0s;
val map_cong1s = mk_map_congs map_cong_passive_args1 map_cong_active_args1;
val map_cong2s = mk_map_congs map_cong_passive_args2 map_cong_active_args2;
@@ -543,7 +547,7 @@
(mk_trans rewrite1 (mk_sym rewrite2)))
xtor_maps xtor_un_folds rewrite1s rewrite2s;
in
- split_conj_thm (un_fold_unique OF map (fp_case fp I mk_sym) unique_prems)
+ split_conj_thm (un_fold_unique OF map (case_fp fp I mk_sym) unique_prems)
end;
fun mk_strong_coinduct_thm coind rel_eqs rel_monos mk_vimage2p ctxt =
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Thu Mar 06 22:15:01 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Mar 07 01:02:21 2014 +0100
@@ -821,7 +821,7 @@
val ctr_specss = map #ctr_specs corec_specs;
val corec_args = hd corecs
|> fst o split_last o binder_types o fastype_of
- |> map (fn T => if range_type T = @{typ bool}
+ |> map (fn T => if range_type T = HOLogic.boolT
then Abs (Name.uu_, domain_type T, @{term False})
else Const (@{const_name undefined}, T))
|> fold2 (fold o build_corec_arg_disc) ctr_specss disc_eqnss
@@ -1227,9 +1227,9 @@
split_last (map_filter I ctr_conds_argss_opt) ||> snd
else
Const (@{const_name Code.abort}, @{typ String.literal} -->
- (@{typ unit} --> body_type fun_T) --> body_type fun_T) $
+ (HOLogic.unitT --> body_type fun_T) --> body_type fun_T) $
HOLogic.mk_literal fun_name $
- absdummy @{typ unit} (incr_boundvars 1 lhs)
+ absdummy HOLogic.unitT (incr_boundvars 1 lhs)
|> pair (map_filter I ctr_conds_argss_opt))
|-> fold_rev (fn (prems, u) => mk_If (s_conjs prems) u)
in
--- a/src/HOL/Tools/BNF/bnf_gfp_util.ML Thu Mar 06 22:15:01 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_util.ML Fri Mar 07 01:02:21 2014 +0100
@@ -12,6 +12,7 @@
val dest_listT: typ -> typ
val mk_Cons: term -> term -> term
+ val mk_InN: typ list -> term -> int -> term
val mk_Shift: term -> term -> term
val mk_Succ: term -> term -> term
val mk_Times: term * term -> term
@@ -36,18 +37,25 @@
val mk_InN_Field: int -> int -> thm
val mk_InN_inject: int -> int -> thm
val mk_InN_not_InM: int -> int -> thm
+ val mk_sumEN: int -> thm
end;
structure BNF_GFP_Util : BNF_GFP_UTIL =
struct
open BNF_Util
+open BNF_FP_Util
val mk_append = HOLogic.mk_binop @{const_name append};
fun mk_equiv B R =
Const (@{const_name equiv}, fastype_of B --> fastype_of R --> HOLogic.boolT) $ B $ R;
+fun mk_InN [_] t 1 = t
+ | mk_InN (_ :: Ts) t 1 = mk_Inl (mk_sumTN Ts) t
+ | mk_InN (LT :: Ts) t m = mk_Inr LT (mk_InN Ts t (m - 1))
+ | mk_InN Ts t _ = raise TYPE ("mk_InN", Ts, [t]);
+
fun mk_Sigma (A, B) =
let
val AT = fastype_of A;
@@ -160,6 +168,12 @@
| mk_InN_inject 2 2 = @{thm Inr_inject}
| mk_InN_inject n m = @{thm Inr_inject} RS mk_InN_inject (n - 1) (m - 1);
+fun mk_sumEN 1 = @{thm one_pointE}
+ | mk_sumEN 2 = @{thm sumE}
+ | mk_sumEN n =
+ (fold (fn i => fn thm => @{thm obj_sumE_f} RSN (i, thm)) (2 upto n - 1) @{thm obj_sumE}) OF
+ replicate n (impI RS allI);
+
fun mk_specN 0 thm = thm
| mk_specN n thm = mk_specN (n - 1) (thm RS spec);
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Thu Mar 06 22:15:01 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Fri Mar 07 01:02:21 2014 +0100
@@ -120,7 +120,7 @@
val callers = map (fn kk => Var ((Name.uu, kk), @{typ "unit => unit"})) (0 upto nn - 1);
fun apply_comps n kk =
- mk_partial_compN n (replicate n @{typ unit} ---> @{typ unit}) (nth callers kk);
+ mk_partial_compN n (replicate n HOLogic.unitT ---> HOLogic.unitT) (nth callers kk);
val callssss =
map2 (map2 (map2 (fn kks => fn ctr_T => map (apply_comps (num_binder_types ctr_T)) kks)))