generate "disc_exhaust" property
authorblanchet
Thu Aug 30 14:27:26 2012 +0200 (2012-08-30)
changeset 49029f0ecfa9575a9
parent 49028 487427a02bee
child 49030 d0f4f113e43d
generate "disc_exhaust" property
src/HOL/Codatatype/Tools/bnf_gfp.ML
src/HOL/Codatatype/Tools/bnf_lfp.ML
src/HOL/Codatatype/Tools/bnf_sugar.ML
src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Thu Aug 30 13:42:05 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Thu Aug 30 14:27:26 2012 +0200
     1.3 @@ -2039,7 +2039,7 @@
     1.4      val surj_unf_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_unf_thms;
     1.5      val unf_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_unf_thms;
     1.6      val unf_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_unf_thms;
     1.7 -    val unf_exhaust_thms = map (fn thm => thm RS @{thm exE}) unf_nchotomy_thms;
     1.8 +    val unf_exhaust_thms = map (fn thm => thm RS exE) unf_nchotomy_thms;
     1.9  
    1.10      val bij_fld_thms =
    1.11        map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) unf_o_fld_thms fld_o_unf_thms;
    1.12 @@ -2047,7 +2047,7 @@
    1.13      val surj_fld_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_fld_thms;
    1.14      val fld_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_fld_thms;
    1.15      val fld_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_fld_thms;
    1.16 -    val fld_exhaust_thms = map (fn thm => thm RS @{thm exE}) fld_nchotomy_thms;
    1.17 +    val fld_exhaust_thms = map (fn thm => thm RS exE) fld_nchotomy_thms;
    1.18  
    1.19      val fld_coiter_thms = map3 (fn unf_inject => fn coiter => fn unf_fld =>
    1.20        iffD1 OF [unf_inject, trans  OF [coiter, unf_fld RS sym]])
     2.1 --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Thu Aug 30 13:42:05 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Thu Aug 30 14:27:26 2012 +0200
     2.3 @@ -1162,7 +1162,7 @@
     2.4      val surj_unf_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_unf_thms;
     2.5      val unf_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_unf_thms;
     2.6      val unf_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_unf_thms;
     2.7 -    val unf_exhaust_thms = map (fn thm => thm RS @{thm exE}) unf_nchotomy_thms;
     2.8 +    val unf_exhaust_thms = map (fn thm => thm RS exE) unf_nchotomy_thms;
     2.9  
    2.10      val bij_fld_thms =
    2.11        map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) unf_o_fld_thms fld_o_unf_thms;
    2.12 @@ -1170,7 +1170,7 @@
    2.13      val surj_fld_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_fld_thms;
    2.14      val fld_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_fld_thms;
    2.15      val fld_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_fld_thms;
    2.16 -    val fld_exhaust_thms = map (fn thm => thm RS @{thm exE}) fld_nchotomy_thms;
    2.17 +    val fld_exhaust_thms = map (fn thm => thm RS exE) fld_nchotomy_thms;
    2.18  
    2.19      val timer = time (timer "unf definitions & thms");
    2.20  
     3.1 --- a/src/HOL/Codatatype/Tools/bnf_sugar.ML	Thu Aug 30 13:42:05 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Tools/bnf_sugar.ML	Thu Aug 30 14:27:26 2012 +0200
     3.3 @@ -131,9 +131,10 @@
     3.4      val discs = map (mk_disc_or_sel As) discs0;
     3.5      val selss = map (map (mk_disc_or_sel As)) selss0;
     3.6  
     3.7 +    fun mk_imp_p Q = Logic.list_implies (Q, HOLogic.mk_Trueprop p);
     3.8 +
     3.9      val goal_exhaust =
    3.10        let
    3.11 -        fun mk_imp_p Q = Logic.list_implies (Q, HOLogic.mk_Trueprop p);
    3.12          fun mk_prem xctr xs =
    3.13            fold_rev Logic.all xs (mk_imp_p [HOLogic.mk_Trueprop (HOLogic.mk_eq (v, xctr))]);
    3.14        in
    3.15 @@ -175,7 +176,7 @@
    3.16            let
    3.17              val goal =
    3.18                HOLogic.mk_Trueprop (HOLogic.mk_all (fst v', snd v',
    3.19 -                   Library.foldr1 HOLogic.mk_disj exist_xs_v_eq_ctrs));
    3.20 +                Library.foldr1 HOLogic.mk_disj exist_xs_v_eq_ctrs));
    3.21            in
    3.22              Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm)
    3.23            end;
    3.24 @@ -222,8 +223,8 @@
    3.25            let
    3.26              fun get_disc_thm k k' = nth disc_thms ((k' - 1) * n + (k - 1));
    3.27              fun mk_goal ((_, disc), (_, disc')) =
    3.28 -              Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v),
    3.29 -                HOLogic.mk_Trueprop (HOLogic.mk_not (disc' $ v)));
    3.30 +              Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v),
    3.31 +                HOLogic.mk_Trueprop (HOLogic.mk_not (disc' $ v))));
    3.32              fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac);
    3.33  
    3.34              val bundles = ks ~~ ms ~~ disc_defs ~~ discs;
    3.35 @@ -242,7 +243,13 @@
    3.36              half_thms @ other_half_thms
    3.37            end;
    3.38  
    3.39 -        val disc_exhaust_thms = [];
    3.40 +        val disc_exhaust_thm =
    3.41 +          let
    3.42 +            fun mk_prem disc = mk_imp_p [HOLogic.mk_Trueprop (disc $ v)];
    3.43 +            val goal = fold Logic.all [p, v] (mk_imp_p (map mk_prem discs));
    3.44 +          in
    3.45 +            Skip_Proof.prove lthy [] [] goal (fn _ => mk_disc_exhaust_tac n exhaust_thm discI_thms)
    3.46 +          end;
    3.47  
    3.48          val ctr_sel_thms = [];
    3.49  
    3.50 @@ -269,7 +276,7 @@
    3.51          |> note ctr_selsN ctr_sel_thms
    3.52          |> note discsN disc_thms
    3.53          |> note disc_disjointN disc_disjoint_thms
    3.54 -        |> note disc_exhaustN disc_exhaust_thms
    3.55 +        |> note disc_exhaustN [disc_exhaust_thm]
    3.56          |> note distinctN (half_distinct_thms @ other_half_distinct_thms)
    3.57          |> note exhaustN [exhaust_thm]
    3.58          |> note injectN inject_thms
     4.1 --- a/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML	Thu Aug 30 13:42:05 2012 +0200
     4.2 +++ b/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML	Thu Aug 30 14:27:26 2012 +0200
     4.3 @@ -7,14 +7,16 @@
     4.4  
     4.5  signature BNF_SUGAR_TACTICS =
     4.6  sig
     4.7 +  val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
     4.8 +  val mk_half_disc_disjoint_tac: int -> thm -> thm -> tactic
     4.9    val mk_nchotomy_tac: int -> thm -> tactic
    4.10 -  val mk_half_disc_disjoint_tac: int -> thm -> thm -> tactic
    4.11    val mk_other_half_disc_disjoint_tac: thm -> tactic
    4.12  end;
    4.13  
    4.14  structure BNF_Sugar_Tactics : BNF_SUGAR_TACTICS =
    4.15  struct
    4.16  
    4.17 +open BNF_Tactics
    4.18  open BNF_FP_Util
    4.19  
    4.20  fun mk_nchotomy_tac n exhaust =
    4.21 @@ -30,4 +32,9 @@
    4.22  fun mk_other_half_disc_disjoint_tac half_thm =
    4.23    (etac @{thm contrapos_pn} THEN' etac half_thm) 1;
    4.24  
    4.25 +fun mk_disc_exhaust_tac n exhaust discIs =
    4.26 +  (rtac exhaust THEN'
    4.27 +   EVERY' (map2 (fn k => fn discI =>
    4.28 +     dtac discI THEN' select_prem_tac n (etac @{thm meta_mp}) k THEN' atac) (1 upto n) discIs)) 1;
    4.29 +
    4.30  end;