src/HOL/Codatatype/Tools/bnf_sugar.ML
changeset 49029 f0ecfa9575a9
parent 49028 487427a02bee
child 49030 d0f4f113e43d
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_sugar.ML	Thu Aug 30 13:42:05 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_sugar.ML	Thu Aug 30 14:27:26 2012 +0200
     1.3 @@ -131,9 +131,10 @@
     1.4      val discs = map (mk_disc_or_sel As) discs0;
     1.5      val selss = map (map (mk_disc_or_sel As)) selss0;
     1.6  
     1.7 +    fun mk_imp_p Q = Logic.list_implies (Q, HOLogic.mk_Trueprop p);
     1.8 +
     1.9      val goal_exhaust =
    1.10        let
    1.11 -        fun mk_imp_p Q = Logic.list_implies (Q, HOLogic.mk_Trueprop p);
    1.12          fun mk_prem xctr xs =
    1.13            fold_rev Logic.all xs (mk_imp_p [HOLogic.mk_Trueprop (HOLogic.mk_eq (v, xctr))]);
    1.14        in
    1.15 @@ -175,7 +176,7 @@
    1.16            let
    1.17              val goal =
    1.18                HOLogic.mk_Trueprop (HOLogic.mk_all (fst v', snd v',
    1.19 -                   Library.foldr1 HOLogic.mk_disj exist_xs_v_eq_ctrs));
    1.20 +                Library.foldr1 HOLogic.mk_disj exist_xs_v_eq_ctrs));
    1.21            in
    1.22              Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm)
    1.23            end;
    1.24 @@ -222,8 +223,8 @@
    1.25            let
    1.26              fun get_disc_thm k k' = nth disc_thms ((k' - 1) * n + (k - 1));
    1.27              fun mk_goal ((_, disc), (_, disc')) =
    1.28 -              Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v),
    1.29 -                HOLogic.mk_Trueprop (HOLogic.mk_not (disc' $ v)));
    1.30 +              Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v),
    1.31 +                HOLogic.mk_Trueprop (HOLogic.mk_not (disc' $ v))));
    1.32              fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac);
    1.33  
    1.34              val bundles = ks ~~ ms ~~ disc_defs ~~ discs;
    1.35 @@ -242,7 +243,13 @@
    1.36              half_thms @ other_half_thms
    1.37            end;
    1.38  
    1.39 -        val disc_exhaust_thms = [];
    1.40 +        val disc_exhaust_thm =
    1.41 +          let
    1.42 +            fun mk_prem disc = mk_imp_p [HOLogic.mk_Trueprop (disc $ v)];
    1.43 +            val goal = fold Logic.all [p, v] (mk_imp_p (map mk_prem discs));
    1.44 +          in
    1.45 +            Skip_Proof.prove lthy [] [] goal (fn _ => mk_disc_exhaust_tac n exhaust_thm discI_thms)
    1.46 +          end;
    1.47  
    1.48          val ctr_sel_thms = [];
    1.49  
    1.50 @@ -269,7 +276,7 @@
    1.51          |> note ctr_selsN ctr_sel_thms
    1.52          |> note discsN disc_thms
    1.53          |> note disc_disjointN disc_disjoint_thms
    1.54 -        |> note disc_exhaustN disc_exhaust_thms
    1.55 +        |> note disc_exhaustN [disc_exhaust_thm]
    1.56          |> note distinctN (half_distinct_thms @ other_half_distinct_thms)
    1.57          |> note exhaustN [exhaust_thm]
    1.58          |> note injectN inject_thms