--- a/src/HOL/BNF_Comp.thy Tue Mar 04 18:57:17 2014 +0100
+++ b/src/HOL/BNF_Comp.thy Tue Mar 04 18:57:17 2014 +0100
@@ -57,6 +57,14 @@
lemma UN_image_subset: "\<Union>(f ` g x) \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})"
by blast
+lemma mem_UN_compreh_ex_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)"
+by blast
+
+lemma UN_compreh_ex_eq_eq:
+"\<Union>{y. \<exists>x\<in>A. y = {}} = {}"
+"\<Union>{y. \<exists>x\<in>A. y = {x}} = A"
+by blast+
+
lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>((\<lambda>f. f x) ` X)| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd"
by (unfold comp_apply collect_def SUP_def)
--- a/src/HOL/BNF_FP_Base.thy Tue Mar 04 18:57:17 2014 +0100
+++ b/src/HOL/BNF_FP_Base.thy Tue Mar 04 18:57:17 2014 +0100
@@ -83,14 +83,6 @@
"case_sum f g (if p then Inl x else Inr y) = (if p then f x else g y)"
by simp
-lemma mem_UN_compreh_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)"
-by blast
-
-lemma UN_compreh_eq_eq:
-"\<Union>{y. \<exists>x\<in>A. y = {}} = {}"
-"\<Union>{y. \<exists>x\<in>A. y = {x}} = A"
-by blast+
-
lemma Inl_Inr_False: "(Inl x = Inr y) = False"
by simp
@@ -106,6 +98,13 @@
"setr (Inr x) = {x}"
unfolding sum_set_defs by simp+
+lemma UN_compreh_eq_eq:
+"\<Union>{y. y = A} = A"
+by blast+
+
+lemma ex_in_single: "(\<exists>x \<in> {y}. P x) = P y"
+by blast
+
lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
by blast
--- a/src/HOL/Tools/BNF/bnf_comp.ML Tue Mar 04 18:57:17 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Tue Mar 04 18:57:17 2014 +0100
@@ -142,11 +142,11 @@
(Variable.invent_types (replicate ilive HOLogic.typeS) lthy2);
val As = if ilive > 0 then hd Ass else [];
val Ass_repl = replicate olive As;
- val (Bs, _(*lthy4*)) = apfst (map TFree)
+ val (Bs, names_lthy) = apfst (map TFree)
(Variable.invent_types (replicate ilive HOLogic.typeS) lthy3);
val Bss_repl = replicate olive Bs;
- val ((((fs', Qs'), Asets), xs), _(*names_lthy*)) = lthy
+ val ((((fs', Qs'), Asets), xs), _) = names_lthy
|> apfst snd o mk_Frees' "f" (map2 (curry op -->) As Bs)
||>> apfst snd o mk_Frees' "Q" (map2 mk_pred2T As Bs)
||>> mk_Frees "A" (map HOLogic.mk_setT As)
@@ -192,6 +192,24 @@
val (sets, sets_alt) = map_split mk_set (0 upto ilive - 1);
+ fun mk_simplified_set set =
+ let
+ val setT = fastype_of set;
+ val schem_set' = Const (@{const_name id_bnf_comp}, setT --> setT) $ Var (("?x", 0), setT);
+ val goal = mk_Trueprop_eq (schem_set', set);
+ fun tac {context = ctxt, prems = _} = mk_simplified_set_tac ctxt;
+ val set'_eq_set =
+ Goal.prove_sorry names_lthy [] [] goal tac
+ |> Thm.close_derivation;
+ val set' = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of set'_eq_set)));
+ in
+ (set', set'_eq_set)
+ end;
+
+ val (sets', set'_eq_sets) =
+ map_split mk_simplified_set sets
+ ||> Proof_Context.export names_lthy lthy;
+
(*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*)
val bd = mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd;
@@ -217,9 +235,9 @@
mk_comp_map_comp0_tac (map_comp0_of_bnf outer) (map_cong0_of_bnf outer)
(map map_comp0_of_bnf inners);
- fun mk_single_set_map0_tac i _ =
- mk_comp_set_map0_tac (map_comp0_of_bnf outer) (map_cong0_of_bnf outer)
- (collect_set_map_of_bnf outer)
+ fun mk_single_set_map0_tac i ctxt =
+ mk_comp_set_map0_tac ctxt (nth set'_eq_sets i) (map_comp0_of_bnf outer)
+ (map_cong0_of_bnf outer) (collect_set_map_of_bnf outer)
(map ((fn thms => nth thms i) o set_map0_of_bnf) inners);
val set_map0_tacs = map mk_single_set_map0_tac (0 upto ilive - 1);
@@ -241,8 +259,9 @@
|> Thm.close_derivation)
(map2 (curry (HOLogic.mk_Trueprop o HOLogic.mk_eq)) sets sets_alt);
- fun map_cong0_tac _ =
- mk_comp_map_cong0_tac set_alt_thms (map_cong0_of_bnf outer) (map map_cong0_of_bnf inners);
+ fun map_cong0_tac ctxt =
+ mk_comp_map_cong0_tac ctxt set'_eq_sets set_alt_thms (map_cong0_of_bnf outer)
+ (map map_cong0_of_bnf inners);
val set_bd_tacs =
if Config.get lthy quick_and_dirty then
@@ -258,9 +277,9 @@
val single_set_bd_thmss =
map ((fn f => map f (0 upto olive - 1)) o single_set_bd_thm) (0 upto ilive - 1);
in
- map2 (fn set_alt => fn single_set_bds => fn ctxt =>
- mk_comp_set_bd_tac ctxt bd_ordIso_natLeq_thm_opt set_alt single_set_bds)
- set_alt_thms single_set_bd_thmss
+ map3 (fn set'_eq_set => fn set_alt => fn single_set_bds => fn ctxt =>
+ mk_comp_set_bd_tac ctxt set'_eq_set bd_ordIso_natLeq_thm_opt set_alt single_set_bds)
+ set'_eq_sets set_alt_thms single_set_bd_thmss
end;
val in_alt_thm =
@@ -277,7 +296,7 @@
fun le_rel_OO_tac _ = mk_le_rel_OO_tac (le_rel_OO_of_bnf outer) (rel_mono_of_bnf outer)
(map le_rel_OO_of_bnf inners);
- fun rel_OO_Grp_tac _ =
+ fun rel_OO_Grp_tac ctxt =
let
val outer_rel_Grp = rel_Grp_of_bnf outer RS sym;
val outer_rel_cong = rel_cong_of_bnf outer;
@@ -287,10 +306,9 @@
[trans OF [outer_rel_Grp RS @{thm arg_cong[of _ _ conversep]},
rel_conversep_of_bnf outer RS sym], outer_rel_Grp],
trans OF [rel_OO_of_bnf outer RS sym, outer_rel_cong OF
- (map (fn bnf => rel_OO_Grp_of_bnf bnf RS sym) inners)]]] RS sym)
- (*|> unfold_thms lthy (rel_def_of_bnf outer :: map rel_def_of_bnf inners)*);
+ (map (fn bnf => rel_OO_Grp_of_bnf bnf RS sym) inners)]]] RS sym);
in
- rtac thm 1
+ unfold_thms_tac ctxt set'_eq_sets THEN rtac thm 1
end;
val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac
@@ -312,14 +330,21 @@
|> map (fn (frees, t) => fold absfree frees t);
fun wit_tac ctxt =
- mk_comp_wit_tac ctxt (wit_thms_of_bnf outer) (collect_set_map_of_bnf outer)
+ mk_comp_wit_tac ctxt set'_eq_sets (wit_thms_of_bnf outer) (collect_set_map_of_bnf outer)
(maps wit_thms_of_bnf inners);
val (bnf', lthy') =
bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) Binding.empty
- Binding.empty [] ((((((b, CCA), mapx), sets), bd'), wits), SOME rel) lthy;
+ Binding.empty [] ((((((b, CCA), mapx), sets'), bd'), wits), SOME rel) lthy;
+
+ val phi =
+ Morphism.thm_morphism "BNF" (unfold_thms lthy' @{thms id_bnf_comp_def})
+ $> Morphism.term_morphism "BNF" (Raw_Simplifier.rewrite_term (Proof_Context.theory_of lthy')
+ @{thms id_bnf_comp_def[abs_def]} []);
+
+ val bnf'' = morph_bnf phi bnf';
in
- (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
+ (bnf'', (add_bnf_to_unfolds bnf'' unfold_set, lthy'))
end;
(* Killing live variables *)
--- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML Tue Mar 04 18:57:17 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML Tue Mar 04 18:57:17 2014 +0100
@@ -12,12 +12,12 @@
val mk_comp_bd_cinfinite_tac: thm -> thm -> tactic
val mk_comp_in_alt_tac: Proof.context -> thm list -> tactic
val mk_comp_map_comp0_tac: thm -> thm -> thm list -> tactic
- val mk_comp_map_cong0_tac: thm list -> thm -> thm list -> tactic
+ val mk_comp_map_cong0_tac: Proof.context -> thm list -> thm list -> thm -> thm list -> tactic
val mk_comp_map_id0_tac: thm -> thm -> thm list -> tactic
val mk_comp_set_alt_tac: Proof.context -> thm -> tactic
- val mk_comp_set_bd_tac: Proof.context -> thm option -> thm -> thm list -> tactic
- val mk_comp_set_map0_tac: thm -> thm -> thm -> thm list -> tactic
- val mk_comp_wit_tac: Proof.context -> thm list -> thm -> thm list -> tactic
+ val mk_comp_set_bd_tac: Proof.context -> thm -> thm option -> thm -> thm list -> tactic
+ val mk_comp_set_map0_tac: Proof.context -> thm -> thm -> thm -> thm -> thm list -> tactic
+ val mk_comp_wit_tac: Proof.context -> thm list -> thm list -> thm -> thm list -> tactic
val kill_in_alt_tac: tactic
val mk_kill_map_cong0_tac: Proof.context -> int -> int -> thm -> tactic
@@ -31,6 +31,7 @@
val mk_le_rel_OO_tac: thm -> thm -> thm list -> tactic
val mk_simple_rel_OO_Grp_tac: thm -> thm -> tactic
val mk_simple_wit_tac: thm list -> tactic
+ val mk_simplified_set_tac: Proof.context -> tactic
val bd_ordIso_natLeq_tac: tactic
end;
@@ -62,7 +63,8 @@
rtac (Gmap_comp0 RS sym RS comp_eq_dest_lhs RS trans), rtac Gmap_cong0] @
map (fn thm => rtac (thm RS sym RS fun_cong)) map_comp0s) 1;
-fun mk_comp_set_map0_tac Gmap_comp0 Gmap_cong0 Gset_map0 set_map0s =
+fun mk_comp_set_map0_tac ctxt set'_eq_set Gmap_comp0 Gmap_cong0 Gset_map0 set_map0s =
+ unfold_thms_tac ctxt [set'_eq_set] THEN
EVERY' ([rtac ext] @
replicate 3 (rtac trans_o_apply) @
[rtac (arg_cong_Union RS trans),
@@ -82,10 +84,11 @@
rtac @{thm sym[OF trans[OF o_apply]]}, rtac @{thm image_cong[OF refl o_apply]}],
rtac @{thm image_empty}]) 1;
-fun mk_comp_map_cong0_tac comp_set_alts map_cong0 map_cong0s =
+fun mk_comp_map_cong0_tac ctxt set'_eq_sets comp_set_alts map_cong0 map_cong0s =
let
val n = length comp_set_alts;
in
+ unfold_thms_tac ctxt set'_eq_sets THEN
(if n = 0 then rtac refl 1
else rtac map_cong0 1 THEN
EVERY' (map_index (fn (i, map_cong0) =>
@@ -120,7 +123,7 @@
rtac Fbd_cinfinite) THEN'
rtac Gbd_cinfinite) 1;
-fun mk_comp_set_bd_tac ctxt bd_ordIso_natLeq_opt comp_set_alt Gset_Fset_bds =
+fun mk_comp_set_bd_tac ctxt set'_eq_set bd_ordIso_natLeq_opt comp_set_alt Gset_Fset_bds =
let
val (bds, last_bd) = split_last Gset_Fset_bds;
fun gen_before bd =
@@ -132,7 +135,7 @@
(case bd_ordIso_natLeq_opt of
SOME thm => rtac (thm RSN (2, @{thm ordLeq_ordIso_trans})) 1
| NONE => all_tac) THEN
- unfold_thms_tac ctxt [comp_set_alt] THEN
+ unfold_thms_tac ctxt [set'_eq_set, comp_set_alt] THEN
rtac @{thm comp_set_bd_Union_o_collect} 1 THEN
unfold_thms_tac ctxt @{thms Union_image_insert Union_image_empty Union_Un_distrib o_apply} THEN
(rtac ctrans THEN'
@@ -161,7 +164,8 @@
val comp_wit_thms = @{thms Union_empty_conv o_apply collect_def SUP_def
Union_image_insert Union_image_empty};
-fun mk_comp_wit_tac ctxt Gwit_thms collect_set_map Fwit_thms =
+fun mk_comp_wit_tac ctxt set'_eq_sets Gwit_thms collect_set_map Fwit_thms =
+ unfold_thms_tac ctxt set'_eq_sets THEN
ALLGOALS (dtac @{thm in_Union_o_assoc}) THEN
unfold_thms_tac ctxt (collect_set_map :: comp_wit_thms) THEN
REPEAT_DETERM ((atac ORELSE'
@@ -232,6 +236,15 @@
val cprod_thms =
@{thms cprod_cong1 cprod_cong2 cprod_cong cprod_dup[OF natLeq_cinfinite natLeq_Card_order]};
+(*inspired by "bnf_fp_def_sugar_tactics.ML"*)
+val simplified_set_simps =
+ @{thms SUP_empty Sup_empty Sup_insert UN_insert Un_empty_left Un_empty_right Un_iff
+ Union_Un_distrib collect_def[abs_def] image_def o_def map_pair_simp mem_Collect_eq
+ mem_UN_compreh_ex_eq UN_compreh_ex_eq_eq sum.set_map prod.set_map id_bnf_comp_def};
+
+fun mk_simplified_set_tac ctxt =
+ unfold_thms_tac ctxt simplified_set_simps THEN rtac refl 1;
+
val bd_ordIso_natLeq_tac =
HEADGOAL (REPEAT_DETERM o resolve_tac
(@{thm ordIso_refl[OF natLeq_Card_order]} :: csum_thms @ cprod_thms));
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Mar 04 18:57:17 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Mar 04 18:57:17 2014 +0100
@@ -38,11 +38,11 @@
val more_simp_thms = basic_simp_thms @ @{thms simp_thms(11,15,16,21)};
val sum_prod_thms_map = @{thms id_apply map_pair_simp prod.case sum.case sum_map.simps};
-val sum_prod_thms_set0 =
+val sum_prod_thms_set =
@{thms SUP_empty Sup_empty Sup_insert UN_insert Un_empty_left Un_empty_right Un_iff
Union_Un_distrib collect_def[abs_def] image_def o_apply map_pair_simp
- mem_Collect_eq mem_UN_compreh_eq prod_set_simps sum_map.simps sum_set_simps};
-val sum_prod_thms_set = @{thms UN_compreh_eq_eq} @ sum_prod_thms_set0;
+ mem_Collect_eq mem_UN_compreh_ex_eq prod_set_simps sum_map.simps sum_set_simps
+ UN_compreh_ex_eq_eq UN_compreh_eq_eq ex_in_single};
val sum_prod_thms_rel = @{thms prod_rel_apply sum_rel_simps id_apply};
fun hhf_concl_conv cv ctxt ct =
@@ -122,7 +122,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_set0)),
+ sum_prod_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