--- a/src/HOL/Codatatype/Tools/bnf_sugar.ML Fri Aug 31 15:04:03 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar.ML Fri Aug 31 15:04:03 2012 +0200
@@ -316,21 +316,34 @@
|> pairself (singleton (Proof_Context.export names_lthy lthy))
end;
- val split_thm =
+ val (split_thm, split_asm_thm) =
let
- fun mk_clause xctr xs f_xs =
+ fun mk_conjunct xctr xs f_xs =
list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (v, xctr), q $ f_xs));
+ fun mk_disjunct xctr xs f_xs =
+ list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (v, xctr),
+ HOLogic.mk_not (q $ f_xs)));
+
+ val lhs = q $ (mk_caseofB_term eta_fs $ v);
+
val goal =
- mk_Trueprop_eq (q $ (mk_caseofB_term eta_fs $ v),
- Library.foldr1 HOLogic.mk_conj (map3 mk_clause xctrs xss xfs));
+ mk_Trueprop_eq (lhs, Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct xctrs xss xfs));
+ val goal_asm =
+ mk_Trueprop_eq (lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj
+ (map3 mk_disjunct xctrs xss xfs)));
+
+ val split_thm =
+ Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
+ mk_split_tac ctxt exhaust_thm' case_thms inject_thms distinct_thms)
+ |> singleton (Proof_Context.export names_lthy lthy)
+ val split_asm_thm =
+ Skip_Proof.prove lthy [] [] goal_asm (fn {context = ctxt, ...} =>
+ mk_split_asm_tac ctxt split_thm)
+ |> singleton (Proof_Context.export names_lthy lthy)
in
- Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
- mk_split_tac ctxt exhaust_thm' case_thms inject_thms distinct_thms)
- |> singleton (Proof_Context.export names_lthy lthy)
+ (split_thm, split_asm_thm)
end;
- val split_asm_thm = TrueI;
-
(* TODO: case syntax *)
(* TODO: attributes (simp, case_names, etc.) *)
--- a/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML Fri Aug 31 15:04:03 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML Fri Aug 31 15:04:03 2012 +0200
@@ -14,7 +14,8 @@
val mk_half_disc_disjoint_tac: int -> thm -> thm -> tactic
val mk_nchotomy_tac: int -> thm -> tactic
val mk_other_half_disc_disjoint_tac: thm -> tactic
- val mk_split_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> tactic
+ val mk_split_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> tactic
+ val mk_split_asm_tac: Proof.context -> thm -> tactic
end;
structure BNF_Sugar_Tactics : BNF_SUGAR_TACTICS =
@@ -77,4 +78,11 @@
simp_tac (ss_only (@{thms simp_thms} @ case_thms @ injects @ distincts) HOL_basic_ss)) THEN
ALLGOALS (blast_tac ctxt);
+val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};
+
+fun mk_split_asm_tac ctxt split =
+ rtac (split RS trans) 1 THEN
+ Local_Defs.unfold_tac ctxt split_asm_thms THEN
+ rtac refl 1;
+
end;