# HG changeset patch # User blanchet # Date 1409137559 -7200 # Node ID b5cdfb352814072081b9097c457d73dacc149502 # Parent a90847f03ec8aaae328f52877d6e761d5fcf8fce removed not so interesting 'set_empty' diff -r a90847f03ec8 -r b5cdfb352814 NEWS --- 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" diff -r a90847f03ec8 -r b5cdfb352814 src/Doc/Datatypes/Datatypes.thy --- 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]} diff -r a90847f03ec8 -r b5cdfb352814 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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; diff -r a90847f03ec8 -r b5cdfb352814 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- 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