# HG changeset patch # User blanchet # Date 1346329646 -7200 # Node ID f0ecfa9575a94f37bbe31fb545de53d0424b432c # Parent 487427a02beeeb41bb1cf595f7aa380921f966ec generate "disc_exhaust" property diff -r 487427a02bee -r f0ecfa9575a9 src/HOL/Codatatype/Tools/bnf_gfp.ML --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Thu Aug 30 13:42:05 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Thu Aug 30 14:27:26 2012 +0200 @@ -2039,7 +2039,7 @@ val surj_unf_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_unf_thms; val unf_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_unf_thms; val unf_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_unf_thms; - val unf_exhaust_thms = map (fn thm => thm RS @{thm exE}) unf_nchotomy_thms; + val unf_exhaust_thms = map (fn thm => thm RS exE) unf_nchotomy_thms; val bij_fld_thms = map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) unf_o_fld_thms fld_o_unf_thms; @@ -2047,7 +2047,7 @@ val surj_fld_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_fld_thms; val fld_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_fld_thms; val fld_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_fld_thms; - val fld_exhaust_thms = map (fn thm => thm RS @{thm exE}) fld_nchotomy_thms; + val fld_exhaust_thms = map (fn thm => thm RS exE) fld_nchotomy_thms; val fld_coiter_thms = map3 (fn unf_inject => fn coiter => fn unf_fld => iffD1 OF [unf_inject, trans OF [coiter, unf_fld RS sym]]) diff -r 487427a02bee -r f0ecfa9575a9 src/HOL/Codatatype/Tools/bnf_lfp.ML --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Thu Aug 30 13:42:05 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Thu Aug 30 14:27:26 2012 +0200 @@ -1162,7 +1162,7 @@ val surj_unf_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_unf_thms; val unf_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_unf_thms; val unf_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_unf_thms; - val unf_exhaust_thms = map (fn thm => thm RS @{thm exE}) unf_nchotomy_thms; + val unf_exhaust_thms = map (fn thm => thm RS exE) unf_nchotomy_thms; val bij_fld_thms = map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) unf_o_fld_thms fld_o_unf_thms; @@ -1170,7 +1170,7 @@ val surj_fld_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_fld_thms; val fld_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_fld_thms; val fld_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_fld_thms; - val fld_exhaust_thms = map (fn thm => thm RS @{thm exE}) fld_nchotomy_thms; + val fld_exhaust_thms = map (fn thm => thm RS exE) fld_nchotomy_thms; val timer = time (timer "unf definitions & thms"); diff -r 487427a02bee -r f0ecfa9575a9 src/HOL/Codatatype/Tools/bnf_sugar.ML --- a/src/HOL/Codatatype/Tools/bnf_sugar.ML Thu Aug 30 13:42:05 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_sugar.ML Thu Aug 30 14:27:26 2012 +0200 @@ -131,9 +131,10 @@ val discs = map (mk_disc_or_sel As) discs0; val selss = map (map (mk_disc_or_sel As)) selss0; + fun mk_imp_p Q = Logic.list_implies (Q, HOLogic.mk_Trueprop p); + val goal_exhaust = let - fun mk_imp_p Q = Logic.list_implies (Q, HOLogic.mk_Trueprop p); fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [HOLogic.mk_Trueprop (HOLogic.mk_eq (v, xctr))]); in @@ -175,7 +176,7 @@ let val goal = HOLogic.mk_Trueprop (HOLogic.mk_all (fst v', snd v', - Library.foldr1 HOLogic.mk_disj exist_xs_v_eq_ctrs)); + Library.foldr1 HOLogic.mk_disj exist_xs_v_eq_ctrs)); in Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm) end; @@ -222,8 +223,8 @@ let fun get_disc_thm k k' = nth disc_thms ((k' - 1) * n + (k - 1)); fun mk_goal ((_, disc), (_, disc')) = - Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v), - HOLogic.mk_Trueprop (HOLogic.mk_not (disc' $ v))); + Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v), + HOLogic.mk_Trueprop (HOLogic.mk_not (disc' $ v)))); fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac); val bundles = ks ~~ ms ~~ disc_defs ~~ discs; @@ -242,7 +243,13 @@ half_thms @ other_half_thms end; - val disc_exhaust_thms = []; + val disc_exhaust_thm = + let + fun mk_prem disc = mk_imp_p [HOLogic.mk_Trueprop (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 = []; @@ -269,7 +276,7 @@ |> note ctr_selsN ctr_sel_thms |> note discsN disc_thms |> note disc_disjointN disc_disjoint_thms - |> note disc_exhaustN disc_exhaust_thms + |> note disc_exhaustN [disc_exhaust_thm] |> note distinctN (half_distinct_thms @ other_half_distinct_thms) |> note exhaustN [exhaust_thm] |> note injectN inject_thms diff -r 487427a02bee -r f0ecfa9575a9 src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML Thu Aug 30 13:42:05 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML Thu Aug 30 14:27:26 2012 +0200 @@ -7,14 +7,16 @@ signature BNF_SUGAR_TACTICS = sig + val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic + val mk_half_disc_disjoint_tac: int -> thm -> thm -> tactic val mk_nchotomy_tac: int -> thm -> tactic - val mk_half_disc_disjoint_tac: int -> thm -> thm -> tactic val mk_other_half_disc_disjoint_tac: thm -> tactic end; structure BNF_Sugar_Tactics : BNF_SUGAR_TACTICS = struct +open BNF_Tactics open BNF_FP_Util fun mk_nchotomy_tac n exhaust = @@ -30,4 +32,9 @@ fun mk_other_half_disc_disjoint_tac half_thm = (etac @{thm contrapos_pn} THEN' etac half_thm) 1; +fun mk_disc_exhaust_tac n exhaust discIs = + (rtac exhaust THEN' + EVERY' (map2 (fn k => fn discI => + dtac discI THEN' select_prem_tac n (etac @{thm meta_mp}) k THEN' atac) (1 upto n) discIs)) 1; + end;