# HG changeset patch # User blanchet # Date 1346418243 -7200 # Node ID c4a34ae5504d8d16acc71cd3fd97f2c72682066b # Parent bd3e33ee762d6eaf1daba93c5a54373a68b76a92 generate "split_asm" property diff -r bd3e33ee762d -r c4a34ae5504d src/HOL/Codatatype/Tools/bnf_sugar.ML --- 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.) *) diff -r bd3e33ee762d -r c4a34ae5504d src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML --- 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;