--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Mon Aug 18 17:19:58 2014 +0200
@@ -17,15 +17,16 @@
thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list ->
thm list list list -> tactic
val mk_corec_tac: thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic
+ val mk_corec_disc_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
tactic
- val mk_disc_corec_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
- val mk_disc_map_iff_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
val mk_half_distinct_tac: Proof.context -> thm -> thm -> thm list -> tactic
val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list ->
thm list -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic
val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic
+ val mk_map_disc_iff_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
+ val mk_map_sel_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context ->
tactic
val mk_rel_cases_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list ->
@@ -37,13 +38,12 @@
thm list list -> thm list -> thm list -> thm list -> thm list -> tactic
val mk_rel_sel_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list -> thm list ->
thm list -> thm list -> tactic
- val mk_sel_map_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
- val mk_sel_set_tac: Proof.context -> cterm -> thm -> 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
+ val mk_set_sel_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
end;
structure BNF_FP_Def_Sugar_Tactics : BNF_FP_DEF_SUGAR_TACTICS =
@@ -126,22 +126,13 @@
HEADGOAL (rtac refl ORELSE' rtac (@{thm unit_eq} RS arg_cong))
end;
-fun mk_disc_corec_iff_tac case_splits' corecs discs ctxt =
+fun mk_corec_disc_iff_tac case_splits' corecs discs ctxt =
EVERY (map3 (fn case_split_tac => fn corec_thm => fn disc =>
HEADGOAL case_split_tac THEN unfold_thms_tac ctxt [corec_thm] THEN
HEADGOAL (asm_simp_tac (ss_only basic_simp_thms ctxt)) THEN
(if is_refl disc then all_tac else HEADGOAL (rtac disc)))
(map rtac case_splits' @ [K all_tac]) corecs discs);
-fun mk_disc_map_iff_tac ctxt ct exhaust discs maps =
- 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 maps THEN
- unfold_thms_tac ctxt (map (fn thm => thm RS eqFalseI
- handle THM _ => thm RS eqTrueI) discs) THEN
- ALLGOALS (rtac refl ORELSE' rtac TrueI);
-
fun solve_prem_prem_tac ctxt =
REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
hyp_subst_tac ctxt ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
@@ -221,6 +212,25 @@
(1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss
selsss));
+fun mk_map_disc_iff_tac ctxt ct exhaust discs maps =
+ 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 maps THEN
+ unfold_thms_tac ctxt (map (fn thm => thm RS eqFalseI
+ handle THM _ => thm RS eqTrueI) discs) THEN
+ ALLGOALS (rtac refl ORELSE' rtac TrueI);
+
+fun mk_map_sel_tac ctxt ct exhaust discs maps sels =
+ 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 ((discs RL [eqTrueI, eqFalseI]) @
+ @{thms not_True_eq_False not_False_eq_True}) THEN
+ TRYALL (etac FalseE ORELSE' etac @{thm TrueE}) THEN
+ unfold_thms_tac ctxt (maps @ sels) THEN
+ ALLGOALS (rtac refl);
+
fun mk_rel_cases_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs=
HEADGOAL (rtac (cterm_instantiate_pos [SOME ct1] exhaust) THEN_ALL_NEW
rtac (cterm_instantiate_pos [SOME ct2] exhaust) THEN_ALL_NEW
@@ -280,17 +290,7 @@
(rel_distincts RL @{thms iffD2[OF eq_False]})) THEN
TRYALL (resolve_tac [TrueI, refl]);
-fun mk_sel_map_tac ctxt ct exhaust discs maps sels =
- 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 ((discs RL [eqTrueI, eqFalseI]) @
- @{thms not_True_eq_False not_False_eq_True}) THEN
- TRYALL (etac FalseE ORELSE' etac @{thm TrueE}) THEN
- unfold_thms_tac ctxt (maps @ sels) THEN
- ALLGOALS (rtac refl);
-
-fun mk_sel_set_tac ctxt ct exhaust discs sels sets =
+fun mk_set_sel_tac ctxt ct exhaust discs sels sets =
TRYALL Goal.conjunction_tac THEN
ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
REPEAT_DETERM o hyp_subst_tac ctxt) THEN