--- a/src/HOL/Codatatype/BNF_FP.thy Fri Sep 14 12:09:27 2012 +0200
+++ b/src/HOL/Codatatype/BNF_FP.thy Fri Sep 14 12:09:27 2012 +0200
@@ -26,17 +26,11 @@
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 all_unit_eq: "(\<And>x. PROP P x) \<equiv> PROP P ()" by simp
-
-lemma all_prod_eq: "(\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (a, b))" by clarsimp
+lemma all_unit_eq: "(\<And>x. PROP P x) \<equiv> PROP P ()"
+by simp
-(* FIXME: needed? *)
-lemma False_imp_eq: "(False \<Longrightarrow> P) \<equiv> Trueprop True"
-by presburger
-
-(* FIXME: needed? *)
-lemma all_point_1: "(\<And>z. z = b \<Longrightarrow> phi z) \<equiv> Trueprop (phi b)"
-by presburger
+lemma all_prod_eq: "(\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (a, b))"
+by clarsimp
lemma rev_bspec: "a \<in> A \<Longrightarrow> \<forall>z \<in> A. P z \<Longrightarrow> P a"
by simp
@@ -110,6 +104,20 @@
"sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
by simp
+lemma UN_compreh_bex:
+"\<Union>{y. \<exists>x \<in> A. y = {}} = {}"
+"\<Union>{y. \<exists>x \<in> A. y = {x}} = A"
+by blast+
+
+lemma induct_set_step: "\<lbrakk>B \<in> A; c \<in> f B\<rbrakk> \<Longrightarrow> \<exists>C. (\<exists>a \<in> A. C = f a) \<and> c \<in> C"
+apply (rule exI)
+apply (rule conjI)
+ apply (rule bexI)
+ apply (rule refl)
+ apply assumption
+apply assumption
+done
+
ML_file "Tools/bnf_fp_util.ML"
ML_file "Tools/bnf_fp_sugar_tactics.ML"
ML_file "Tools/bnf_fp_sugar.ML"
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 14 12:09:27 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 14 12:09:27 2012 +0200
@@ -51,8 +51,6 @@
val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs));
-fun mk_id T = Const (@{const_name id}, T --> T);
-
fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs));
fun mk_uncurried_fun f xs = mk_tupled_fun (HOLogic.mk_tuple xs) f xs;
fun mk_uncurried2_fun f xss =
@@ -499,9 +497,10 @@
((wrap, define_iter_likes), lthy')
end;
- (* TODO: remove all "nested" and "nesting" BNFs from pre_bnfs, if they're there *)
+ (* TODO: remove all "nested" and "nesting" BNFs from pre_bnfs, if they're there ### *)
val pre_map_defs = map map_def_of_bnf pre_bnfs;
val pre_set_defss = map set_defs_of_bnf pre_bnfs;
+ val nested_set_natural's = maps set_natural'_of_bnf nested_bnfs;
val nesting_map_ids = map map_id_of_bnf nesting_bnfs;
fun mk_map Ts Us t =
@@ -571,26 +570,36 @@
fold_rev Logic.all
(map Free (drop (nn + 1) (rev (Term.add_frees t (x' :: phis'))))) t;
- fun mk_prem phi ctr ctr_Ts =
+ fun mk_prem_triple phi ctr ctr_Ts =
let
val (xs, names_lthy') = names_lthy |> mk_Frees "x" ctr_Ts;
val prem_prems =
maps (fn x => map (close_prem_prem x) (mk_prem_prems names_lthy' x)) xs;
in
- fold_rev Logic.all xs
- (Logic.list_implies (prem_prems,
- HOLogic.mk_Trueprop (phi $ Term.list_comb (ctr, xs))))
+ (xs, prem_prems, HOLogic.mk_Trueprop (phi $ Term.list_comb (ctr, xs)))
end;
+ val prem_tripless = map3 (map2 o mk_prem_triple) phis ctrss ctr_Tsss;
+
+ fun mk_prem (xs, prem_prems, concl) =
+ fold_rev Logic.all xs (Logic.list_implies (prem_prems, concl));
+
val goal =
- fold_rev (fold_rev Logic.all) [phis, vs]
- (Library.foldr Logic.list_implies (map3 (map2 o mk_prem) phis ctrss ctr_Tsss,
- HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
- (map2 (curry (op $)) phis vs))));
+ Library.foldr (Logic.list_implies o apfst (map mk_prem)) (prem_tripless,
+ HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
+ (map2 (curry (op $)) phis vs)));
+
+ val rss = map (map (length o #2)) prem_tripless;
+
+ val fld_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss);
val induct_thm =
Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
- mk_induct_tac ctxt);
+ mk_induct_tac ctxt ns mss rss (flat ctr_defss) fld_induct' pre_set_defss
+ nested_set_natural's)
+ (* TODO: thread name context properly ### *)
+ |> singleton (Proof_Context.export names_lthy lthy)
+ |> singleton (Proof_Context.export no_defs_lthy no_defs_lthy0)
in
`(conj_dests nn) induct_thm
end;
@@ -607,7 +616,7 @@
fun build_call fiter_likes maybe_tick (T, U) =
if T = U then
- mk_id T
+ id_const T
else
(case find_index (curry (op =) T) fpTs of
~1 => build_map (build_call fiter_likes maybe_tick) T U
@@ -685,7 +694,7 @@
fun build_call fiter_likes maybe_tack (T, U) =
if T = U then
- mk_id T
+ id_const T
else
(case find_index (curry (op =) U) fpTs of
~1 => build_map (build_call fiter_likes maybe_tack) T U
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Fri Sep 14 12:09:27 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Fri Sep 14 12:09:27 2012 +0200
@@ -13,7 +13,8 @@
val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm
-> tactic
val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic
- val mk_induct_tac: Proof.context -> tactic
+ val mk_induct_tac: Proof.context -> int list -> int list list -> int list list -> thm list ->
+ thm -> thm list list -> thm list -> tactic
val mk_inject_tac: Proof.context -> thm -> thm -> tactic
val mk_iter_like_tac: thm list -> thm list -> thm list -> thm -> thm -> Proof.context -> tactic
end;
@@ -25,6 +26,23 @@
open BNF_Util
open BNF_FP_Util
+val meta_mp = @{thm meta_mp};
+val meta_spec = @{thm meta_spec};
+
+fun squash_spurious_fs lthy thm =
+ let
+ val spurious_fs =
+ Term.add_vars (prop_of thm) []
+ |> filter (fn (_, Type (@{type_name fun}, [_, T'])) => T' <> HOLogic.boolT | _ => false);
+ val cxs =
+ map (fn s as (_, T) =>
+ (certify lthy (Var s), certify lthy (id_abs (domain_type T)))) spurious_fs;
+ in
+ Drule.cterm_instantiate cxs thm
+ end;
+
+val squash_spurious_fs_tac = PRIMITIVE o squash_spurious_fs;
+
fun mk_case_tac ctxt n k m case_def ctr_def unf_fld =
Local_Defs.unfold_tac ctxt [case_def, ctr_def, unf_fld] THEN
(rtac (mk_sum_casesN_balanced n k RS ssubst) THEN'
@@ -34,8 +52,8 @@
fun mk_exhaust_tac ctxt n ctr_defs fld_iff_unf sumEN' =
Local_Defs.unfold_tac ctxt (fld_iff_unf :: ctr_defs) THEN rtac sumEN' 1 THEN
Local_Defs.unfold_tac ctxt @{thms all_prod_eq} THEN
- EVERY' (maps (fn k => [select_prem_tac n (rotate_tac 1) k, REPEAT_DETERM o dtac @{thm meta_spec},
- etac @{thm meta_mp}, atac]) (1 upto n)) 1;
+ EVERY' (maps (fn k => [select_prem_tac n (rotate_tac 1) k, REPEAT_DETERM o dtac meta_spec,
+ etac meta_mp, atac]) (1 upto n)) 1;
fun mk_fld_iff_unf_tac ctxt cTs cfld cunf fld_unf unf_fld =
(rtac iffI THEN'
@@ -52,9 +70,6 @@
Local_Defs.unfold_tac ctxt [ctr_def] THEN rtac (fld_inject RS ssubst) 1 THEN
Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
-fun mk_induct_tac ctxt =
- Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt) (* FIXME: TODO *);
-
val iter_like_thms =
@{thms case_unit comp_def convol_def id_apply map_pair_def sum.simps(5,6) sum_map.simps
split_conv};
@@ -73,4 +88,52 @@
Local_Defs.unfold_tac ctxt @{thms id_def} THEN
TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1);
+fun mk_induct_prelude_tac ctxt ctr_defs fld_induct' =
+ Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN squash_spurious_fs_tac ctxt;
+
+fun mk_induct_prepare_prem_tac n m k =
+ EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac,
+ REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1;
+
+fun mk_induct_prepare_prem_prems_tac _ _ 0 = all_tac
+ | mk_induct_prepare_prem_prems_tac nn kk r =
+ REPEAT_DETERM_N r (rotate_tac (~1 + kk - nn) 1 THEN dtac meta_mp 1 THEN
+ defer_tac 2 THEN PRIMITIVE (Thm.permute_prems 0 ~1) THEN rotate_tac 1 1) THEN
+ PRIMITIVE Raw_Simplifier.norm_hhf;
+
+val induct_prem_prem_thms =
+ @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex UN_insert Un_assoc[symmetric] Un_empty_left
+ Un_empty_right Union_Un_distrib collect_def[abs_def] fst_conv fsts_def[abs_def] image_def
+ map_pair_simp o_apply snd_conv snds_def[abs_def] sum.cases sum_map.simps sum_setl_def[abs_def]
+ sum_setr_def[abs_def] sup_bot_right};
+
+fun mk_induct_discharge_prem_prems_tac ctxt r pre_set_defs set_natural's =
+ EVERY' (maps (fn i =>
+ [dtac meta_spec, rotate_tac ~1, etac meta_mp,
+ SELECT_GOAL (Local_Defs.unfold_tac ctxt
+ (set_natural's @ pre_set_defs @ induct_prem_prem_thms)),
+ rtac (mk_UnIN r i),
+ atac ORELSE'
+ rtac @{thm singletonI} ORELSE'
+ (REPEAT_DETERM o (atac ORELSE'
+ SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
+ etac @{thm induct_set_step}))]) (r downto 1)) 1;
+
+fun mk_induct_discharge_prem_tac ctxt nn kk n m k r pre_set_defs set_natural's =
+ EVERY [mk_induct_prepare_prem_tac n m k,
+ mk_induct_prepare_prem_prems_tac nn kk r, atac 1,
+ mk_induct_discharge_prem_prems_tac ctxt r pre_set_defs set_natural's];
+
+fun mk_induct_tac ctxt ns mss rss ctr_defs fld_induct' pre_set_defss set_natural's =
+ let
+ val nn = length ns;
+ val n = Integer.sum ns;
+ in
+ mk_induct_prelude_tac ctxt ctr_defs fld_induct' THEN
+ EVERY (map5 (fn kk => fn pre_set_defs =>
+ EVERY ooo map3 (fn m => fn k => fn r =>
+ mk_induct_discharge_prem_tac ctxt nn kk n m k r pre_set_defs set_natural's))
+ (1 upto nn) pre_set_defss mss (unflat mss (1 upto Integer.sum ns)) rss)
+ end;
+
end;
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Fri Sep 14 12:09:27 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Fri Sep 14 12:09:27 2012 +0200
@@ -99,6 +99,9 @@
val mk_sumTN: typ list -> typ
val mk_sumTN_balanced: typ list -> typ
+ val id_const: typ -> term
+ val id_abs: typ -> term
+
val Inl_const: typ -> typ -> term
val Inr_const: typ -> typ -> term
@@ -256,6 +259,9 @@
val mk_sumTN = Library.foldr1 mk_sumT;
val mk_sumTN_balanced = Balanced_Tree.make mk_sumT;
+fun id_const T = Const (@{const_name id}, T --> T);
+fun id_abs T = Abs (Name.uu, T, Bound 0);
+
fun Inl_const LT RT = Const (@{const_name Inl}, LT --> mk_sumT (LT, RT));
fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t;