# HG changeset patch # User blanchet # Date 1346756550 -7200 # Node ID 3d520eec27467e2bc4f5f9ea27f844b6e2110412 # Parent c9c09dbdbd1c4e7e6968c02216194ce283a336c2 allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes) diff -r c9c09dbdbd1c -r 3d520eec2746 src/HOL/Codatatype/BNF_Library.thy --- a/src/HOL/Codatatype/BNF_Library.thy Tue Sep 04 13:02:29 2012 +0200 +++ b/src/HOL/Codatatype/BNF_Library.thy Tue Sep 04 13:02:30 2012 +0200 @@ -14,6 +14,9 @@ Equiv_Relations_More begin +lemma iffI_np: "\x \ \ y; \ x \ y\ \ \ x \ y" +by (erule iffI) (erule contrapos_pn) + lemma subset_Collect_iff: "B \ A \ (B \ {x \ A. P x}) = (\x \ B. P x)" by blast diff -r c9c09dbdbd1c -r 3d520eec2746 src/HOL/Codatatype/Tools/bnf_wrap.ML --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Tue Sep 04 13:02:29 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Tue Sep 04 13:02:30 2012 +0200 @@ -23,7 +23,7 @@ | mk_un_N _ l suf = un_N ^ suf ^ string_of_int l; val case_congN = "case_cong"; -val case_discsN = "case_discs"; +val case_eqN = "case_eq"; val casesN = "cases"; val ctr_selsN = "ctr_sels"; val disc_exclusN = "disc_exclus"; @@ -105,6 +105,8 @@ else SOME disc) ctrs0; + val no_discs = map is_none disc_names; + val sel_namess = pad_list [] n raw_sel_namess |> map3 (fn ctr => fn m => map2 (fn l => fn sel => @@ -151,8 +153,16 @@ fun mk_sel_caseof_args k xs x T = map2 (fn Ts => fn i => if i = k then fold_rev Term.lambda xs x else mk_undef T Ts) ctr_Tss ks; - fun disc_spec b exist_xs_v_eq_ctr = - mk_Trueprop_eq (Free (Binding.name_of b, T --> HOLogic.boolT) $ v, exist_xs_v_eq_ctr); + fun disc_free b = Free (Binding.name_of b, T --> HOLogic.boolT); + + fun disc_spec b exist_xs_v_eq_ctr = mk_Trueprop_eq (disc_free b $ v, exist_xs_v_eq_ctr); + + fun not_other_disc_lhs i = + HOLogic.mk_not + (case nth disc_names i of NONE => nth exist_xs_v_eq_ctrs i | SOME b => disc_free b $ v); + + fun not_other_disc k = + if n = 2 then Term.lambda v (not_other_disc_lhs (2 - k)) else error "Cannot use \"*\" here" fun sel_spec b x xs k = let val T' = fastype_of x in @@ -160,13 +170,17 @@ Term.list_comb (mk_caseof As T', mk_sel_caseof_args k xs x T') $ v) end; + val missing_disc_def = TrueI; (* marker *) + val (((raw_discs, raw_disc_defs), (raw_selss, raw_sel_defss)), (lthy', lthy)) = no_defs_lthy - |> apfst split_list o fold_map2 (fn exist_xs_v_eq_ctr => - fn NONE => pair (Term.lambda v exist_xs_v_eq_ctr, refl) + |> apfst split_list o fold_map4 (fn k => fn m => fn exist_xs_v_eq_ctr => + fn NONE => + if m = 0 then pair (Term.lambda v exist_xs_v_eq_ctr, refl) + else pair (not_other_disc k, missing_disc_def) | SOME b => Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), disc_spec b exist_xs_v_eq_ctr)) #>> apsnd snd) - exist_xs_v_eq_ctrs disc_names + ks ms exist_xs_v_eq_ctrs disc_names ||>> apfst split_list o fold_map3 (fn bs => fn xs => fn k => apfst split_list o fold_map2 (fn b => fn x => Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), sel_spec b x xs k)) #>> apsnd snd) bs xs) sel_namess xss ks @@ -258,13 +272,33 @@ map5 mk_thms ks xss goal_cases case_thms sel_defss end; - val discD_thms = map (fn def => def RS iffD1) disc_defs; + fun not_other_disc_def k = + let + val goal = + mk_Trueprop_eq (Morphism.term phi (not_other_disc_lhs (2 - k)), + nth exist_xs_v_eq_ctrs (k - 1)); + in + Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => + mk_not_other_disc_def_tac ctxt (nth disc_defs (2 - k)) (nth distinct_thms (2 - k)) + exhaust_thm') + |> singleton (Proof_Context.export names_lthy lthy) + end; + + val has_not_other_disc_def = + exists (fn def => Thm.eq_thm_prop (def, missing_disc_def)) disc_defs; + + val disc_defs' = + map2 (fn k => fn def => + if Thm.eq_thm_prop (def, missing_disc_def) then not_other_disc_def k else def) + ks disc_defs; + + val discD_thms = map (fn def => def RS iffD1) disc_defs'; val discI_thms = - map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms disc_defs; + map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms disc_defs'; val not_disc_thms = map2 (fn m => fn def => funpow m (fn thm => allI RS thm) - (Local_Defs.unfold lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]}))) - ms disc_defs; + (Local_Defs.unfold lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]}))) + ms disc_defs'; val (disc_thmss', disc_thmss) = let @@ -275,37 +309,47 @@ map3 mk_thms discI_thms not_disc_thms distinct_thmsss' |> `transpose end; + val disc_thms = flat (map2 (fn true => K [] | false => I) no_discs disc_thmss); + val disc_exclus_thms = - let - fun mk_goal ((_, disc), (_, disc')) = - Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (betapply (disc, v)), - HOLogic.mk_Trueprop (HOLogic.mk_not (betapply (disc', v))))); - fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac); + if has_not_other_disc_def then + [] + else + let + fun mk_goal [] = [] + | mk_goal [((_, true), (_, true))] = [] + | mk_goal [(((_, disc), _), ((_, disc'), _))] = + [Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (betapply (disc, v)), + HOLogic.mk_Trueprop (HOLogic.mk_not (betapply (disc', v)))))]; + fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac); - val bundles = ms ~~ discD_thms ~~ discs; - val half_pairss = mk_half_pairss bundles; + val bundles = ms ~~ discD_thms ~~ discs ~~ no_discs; + val half_pairss = mk_half_pairss bundles; - val goal_halvess = map (map mk_goal) half_pairss; - val half_thmss = - map3 (fn [] => K (K []) - | [(((m, discD), _), _)] => fn disc_thm => fn [goal] => - [prove (mk_half_disc_exclus_tac m discD disc_thm) goal]) - half_pairss (flat disc_thmss') goal_halvess; + val goal_halvess = map mk_goal half_pairss; + val half_thmss = + map3 (fn [] => K (K []) | [goal] => fn [((((m, discD), _), _), _)] => fn disc_thm => + [prove (mk_half_disc_exclus_tac m discD disc_thm) goal]) + goal_halvess half_pairss (flat disc_thmss'); - val goal_other_halvess = map (map (mk_goal o swap)) half_pairss; - val other_half_thmss = - map2 (map2 (prove o mk_other_half_disc_exclus_tac)) half_thmss goal_other_halvess; - in - interleave (flat half_thmss) (flat other_half_thmss) - end; + val goal_other_halvess = map (mk_goal o map swap) half_pairss; + val other_half_thmss = + map2 (map2 (prove o mk_other_half_disc_exclus_tac)) half_thmss goal_other_halvess; + in + interleave (flat half_thmss) (flat other_half_thmss) + end; - val disc_exhaust_thm = - let - fun mk_prem disc = mk_imp_p [HOLogic.mk_Trueprop (betapply (disc, v))]; - val goal = fold Logic.all [p, v] (mk_imp_p (map mk_prem discs)); - in - Skip_Proof.prove lthy [] [] goal (fn _ => mk_disc_exhaust_tac n exhaust_thm discI_thms) - end; + val disc_exhaust_thms = + if has_not_other_disc_def orelse forall I no_discs then + [] + else + let + fun mk_prem disc = mk_imp_p [HOLogic.mk_Trueprop (betapply (disc, v))]; + val goal = fold Logic.all [p, v] (mk_imp_p (map mk_prem discs)); + in + [Skip_Proof.prove lthy [] [] goal (fn _ => + mk_disc_exhaust_tac n exhaust_thm discI_thms)] + end; val ctr_sel_thms = let @@ -327,7 +371,7 @@ |> map_filter I end; - val case_disc_thm = + val case_eq_thm = let fun mk_core f sels = Term.list_comb (f, map (fn sel => sel $ v) sels); fun mk_rhs _ [f] [sels] = mk_core f sels @@ -337,7 +381,7 @@ val goal = mk_Trueprop_eq (caseofB_fs $ v, mk_rhs discs fs selss); in Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => - mk_case_disc_tac ctxt exhaust_thm' case_thms disc_thmss' sel_thmss) + mk_case_eq_tac ctxt exhaust_thm' case_thms disc_thmss' sel_thmss) |> singleton (Proof_Context.export names_lthy lthy) end; @@ -392,12 +436,12 @@ val notes = [(case_congN, [case_cong_thm]), - (case_discsN, [case_disc_thm]), + (case_eqN, [case_eq_thm]), (casesN, case_thms), (ctr_selsN, ctr_sel_thms), - (discsN, (flat disc_thmss)), + (discsN, disc_thms), (disc_exclusN, disc_exclus_thms), - (disc_exhaustN, [disc_exhaust_thm]), + (disc_exhaustN, disc_exhaust_thms), (distinctN, distinct_thms), (exhaustN, [exhaust_thm]), (injectN, (flat inject_thmss)), @@ -406,6 +450,7 @@ (splitN, [split_thm]), (split_asmN, [split_asm_thm]), (weak_case_cong_thmsN, [weak_case_cong_thm])] + |> filter_out (null o snd) |> map (fn (thmN, thms) => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); in diff -r c9c09dbdbd1c -r 3d520eec2746 src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML Tue Sep 04 13:02:29 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML Tue Sep 04 13:02:30 2012 +0200 @@ -8,11 +8,12 @@ signature BNF_WRAP_TACTICS = sig val mk_case_cong_tac: thm -> thm list -> tactic - val mk_case_disc_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> tactic + val mk_case_eq_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> tactic val mk_ctr_sel_tac: Proof.context -> int -> thm -> thm list -> tactic val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic val mk_half_disc_exclus_tac: int -> thm -> thm -> tactic val mk_nchotomy_tac: int -> thm -> tactic + val mk_not_other_disc_def_tac: Proof.context -> thm -> thm -> thm -> tactic val mk_other_half_disc_exclus_tac: thm -> tactic val mk_split_tac: thm -> thm list -> thm list list -> thm list list list -> tactic val mk_split_asm_tac: Proof.context -> thm -> tactic @@ -36,6 +37,11 @@ (rtac allI THEN' rtac exhaust THEN' EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1; +fun mk_not_other_disc_def_tac ctxt other_disc_def distinct exhaust' = + EVERY' [subst_tac ctxt [other_disc_def], rtac @{thm iffI_np}, hyp_subst_tac, + SELECT_GOAL (Local_Defs.unfold_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI, rtac distinct, + rtac exhaust', etac notE, atac, REPEAT_DETERM o rtac exI, atac] 1; + fun mk_half_disc_exclus_tac m discD disc'_thm = (dtac discD THEN' REPEAT_DETERM_N m o etac exE THEN' @@ -60,7 +66,7 @@ SELECT_GOAL (Local_Defs.unfold_tac ctxt sel_thms) THEN' rtac refl)) 1; -fun mk_case_disc_tac ctxt exhaust' case_thms disc_thmss' sel_thmss = +fun mk_case_eq_tac ctxt exhaust' case_thms disc_thmss' sel_thmss = (rtac exhaust' THEN' EVERY' (map3 (fn case_thm => fn if_disc_thms => fn sel_thms => EVERY' [ hyp_subst_tac THEN'