--- a/NEWS Wed Aug 27 08:41:12 2014 +0200
+++ b/NEWS Wed Aug 27 13:05:59 2014 +0200
@@ -33,7 +33,10 @@
strong_coinduct ~> coinduct_strong
weak_case_cong ~> case_cong_weak
INCOMPATIBILITY.
- - The rule "set_cases" is registered with the "[cases set]"
+ - The rules "set_empty" have been removed. They are easy
+ consequences of other set rules "by auto".
+ INCOMPATIBILITY.
+ - The rule "set_cases" is now registered with the "[cases set]"
attribute. This can influence the behavior of the "cases" proof
method when more than one case rule is applicable (e.g., an
assumption is of the form "w : set ws" and the method "cases w"
--- a/src/Doc/Datatypes/Datatypes.thy Wed Aug 27 08:41:12 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Wed Aug 27 13:05:59 2014 +0200
@@ -867,9 +867,6 @@
\item[@{text "t."}\hthm{set_cases} @{text "[consumes 1, cases set: set\<^sub>i_t]"}\rm:] ~ \\
@{thm list.set_cases[no_vars]}
-\item[@{text "t."}\hthm{set_empty}\rm:] ~ \\
-@{thm list.set_empty[no_vars]}
-
\item[@{text "t."}\hthm{set_intros}\rm:] ~ \\
@{thm list.set_intros(1)[no_vars]} \\
@{thm list.set_intros(2)[no_vars]}
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Aug 27 08:41:12 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Aug 27 13:05:59 2014 +0200
@@ -103,7 +103,6 @@
val map_disc_iffN = "map_disc_iff";
val map_selN = "map_sel";
val set_casesN = "set_cases";
-val set_emptyN = "set_empty";
val set_introsN = "set_intros";
val set_inductN = "set_induct";
val set_selN = "set_sel";
@@ -1429,42 +1428,6 @@
|> map (unfold_thms lthy @{thms insert_is_Un[THEN sym] Un_empty_left
Un_insert_left});
- val sets = map (mk_set (snd (Term.dest_Type fpT))) (sets_of_bnf fp_bnf);
-
- val set_empty_thms =
- let
- val ctr_argT_namess = map ((fn Ts => fold Term.add_tfree_namesT Ts []) o
- binder_types o fastype_of) ctrs;
- val setTs = map (HOLogic.dest_setT o range_type o fastype_of) sets;
- val setT_names = map (fn T => the_single (Term.add_tfree_namesT T [])) setTs;
-
- fun mk_set_empty_goal disc set T =
- Logic.mk_implies (HOLogic.mk_Trueprop (disc $ u),
- mk_Trueprop_eq (set $ u, HOLogic.mk_set T []));
-
- val goals =
- if null discs then
- []
- else
- map_filter I (flat
- (map2 (fn names => fn disc =>
- map3 (fn name => fn setT => fn set =>
- if member (op =) names name then NONE
- else SOME (mk_set_empty_goal disc set setT))
- setT_names setTs sets)
- ctr_argT_namess discs));
- in
- if null goals then
- []
- else
- Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
- (fn {context = ctxt, prems = _} =>
- mk_set_empty_tac ctxt (certify ctxt u) exhaust set0_thms (flat disc_thmss))
- |> Conjunction.elim_balanced (length goals)
- |> Proof_Context.export names_lthy lthy
- |> map Thm.close_derivation
- end;
-
val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns);
fun mk_rel_thm postproc ctr_defs' cxIn cyIn =
@@ -1538,7 +1501,7 @@
val goals = mk_parametricity_goals names_lthy Rs ctrAs ctrBs;
in
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
- (fn {context = ctxt, prems = _} => mk_ctr_transfer_tac rel_intro_thms)
+ (K (mk_ctr_transfer_tac rel_intro_thms))
|> Conjunction.elim_balanced (length goals)
|> Proof_Context.export names_lthy lthy
|> map Thm.close_derivation
@@ -1596,7 +1559,7 @@
val thm =
Goal.prove_sorry lthy [] (flat premss) goal
(fn {context = ctxt, prems} =>
- mk_set_cases_tac ctxt (certify ctxt ta) prems exhaust set_thms)
+ mk_set_cases_tac ctxt (certify ctxt ta) prems exhaust set_thms)
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation
|> rotate_prems ~1;
@@ -1680,9 +1643,9 @@
else
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
(fn {context = ctxt, prems = _} =>
- mk_rel_sel_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust
- (flat disc_thmss) (flat sel_thmss) rel_inject_thms distincts
- rel_distinct_thms)
+ mk_rel_sel_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust
+ (flat disc_thmss) (flat sel_thmss) rel_inject_thms distincts
+ rel_distinct_thms)
|> Conjunction.elim_balanced (length goals)
|> Proof_Context.export names_lthy lthy
|> map Thm.close_derivation
@@ -1718,9 +1681,9 @@
val thm =
Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} =>
- mk_rel_cases_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust
- injects rel_inject_thms distincts rel_distinct_thms
- (map rel_eq_of_bnf live_nesting_bnfs))
+ mk_rel_cases_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust
+ injects rel_inject_thms distincts rel_distinct_thms
+ (map rel_eq_of_bnf live_nesting_bnfs))
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation;
@@ -1751,8 +1714,8 @@
else
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
(fn {context = ctxt, prems = _} =>
- mk_map_disc_iff_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
- map_thms)
+ mk_map_disc_iff_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
+ map_thms)
|> Conjunction.elim_balanced (length goals)
|> Proof_Context.export names_lthy lthy
|> map Thm.close_derivation
@@ -1778,6 +1741,7 @@
if is_refl_bool prem then concl
else Logic.mk_implies (HOLogic.mk_Trueprop prem, concl)
end;
+
val goals = map mk_goal discAs_selAss;
in
if null goals then
@@ -1785,8 +1749,8 @@
else
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
(fn {context = ctxt, prems = _} =>
- mk_map_sel_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
- map_thms (flat sel_thmss))
+ mk_map_sel_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
+ map_thms (flat sel_thmss))
|> Conjunction.elim_balanced (length goals)
|> Proof_Context.export names_lthy lthy
|> map Thm.close_derivation
@@ -1878,7 +1842,6 @@
(rel_selN, rel_sel_thms, K []),
(setN, set_thms, K (code_nitpicksimp_attrs @ simp_attrs)),
(set_casesN, set_cases_thms, nth set_cases_attrss),
- (set_emptyN, set_empty_thms, K []),
(set_introsN, set_intros_thms, K []),
(set_selN, set_sel_thms, K [])]
|> massage_simple_notes fp_b_name;
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Wed Aug 27 08:41:12 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Wed Aug 27 13:05:59 2014 +0200
@@ -40,7 +40,6 @@
val mk_rel_sel_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list -> thm list ->
thm list -> thm list -> tactic
val mk_set_cases_tac: Proof.context -> cterm -> thm list -> thm -> thm list -> tactic
- val mk_set_empty_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
val mk_set_induct0_tac: Proof.context -> cterm list -> thm list -> thm list -> thm list ->
thm list -> thm list -> thm list -> thm list -> tactic
val mk_set_intros_tac: Proof.context -> thm list -> tactic
@@ -317,14 +316,6 @@
hyp_subst_tac ctxt ORELSE'
SELECT_GOAL (SOLVE (HEADGOAL (eresolve_tac assms THEN' REPEAT_DETERM o atac)))));
-fun mk_set_empty_tac ctxt ct exhaust sets discs =
- TRYALL Goal.conjunction_tac THEN
- ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
- REPEAT_DETERM o hyp_subst_tac ctxt) THEN
- unfold_thms_tac ctxt (sets @ map_filter (fn thm =>
- SOME (thm RS eqFalseI) handle THM _ => NONE) discs) THEN
- ALLGOALS (rtac refl ORELSE' etac FalseE);
-
fun mk_set_intros_tac ctxt sets =
TRYALL Goal.conjunction_tac THEN
unfold_thms_tac ctxt sets THEN