port list comprehension simproc to 'Ctr_Sugar' abstraction
authorblanchet
Tue Nov 12 13:47:24 2013 +0100 (2013-11-12)
changeset 544049f0f1152c875
parent 54403 40382f65bc80
child 54405 88f6d5b1422f
port list comprehension simproc to 'Ctr_Sugar' abstraction
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Tue Nov 12 13:47:24 2013 +0100
     1.2 +++ b/src/HOL/List.thy	Tue Nov 12 13:47:24 2013 +0100
     1.3 @@ -542,7 +542,6 @@
     1.4  
     1.5  fun simproc ctxt redex =
     1.6    let
     1.7 -    val thy = Proof_Context.theory_of ctxt
     1.8      val set_Nil_I = @{thm trans} OF [@{thm set.simps(1)}, @{thm empty_def}]
     1.9      val set_singleton = @{lemma "set [a] = {x. x = a}" by simp}
    1.10      val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp}
    1.11 @@ -563,21 +562,22 @@
    1.12        in
    1.13          fold_index check cases (SOME NONE) |> the_default NONE
    1.14        end
    1.15 -    (* returns (case_expr type index chosen_case) option  *)
    1.16 +    (* returns (case_expr type index chosen_case constr_name) option  *)
    1.17      fun dest_case case_term =
    1.18        let
    1.19          val (case_const, args) = strip_comb case_term
    1.20        in
    1.21          (case try dest_Const case_const of
    1.22            SOME (c, T) =>
    1.23 -            (case Datatype.info_of_case thy c of
    1.24 -              SOME _ =>
    1.25 +            (case Ctr_Sugar.ctr_sugar_of_case ctxt c of
    1.26 +              SOME {ctrs, ...} =>
    1.27                  (case possible_index_of_singleton_case (fst (split_last args)) of
    1.28                    SOME i =>
    1.29                      let
    1.30 +                      val constr_names = map (fst o dest_Const) ctrs
    1.31                        val (Ts, _) = strip_type T
    1.32                        val T' = List.last Ts
    1.33 -                    in SOME (List.last args, T', i, nth args i) end
    1.34 +                    in SOME (List.last args, T', i, nth args i, nth constr_names i) end
    1.35                  | NONE => NONE)
    1.36              | NONE => NONE)
    1.37          | NONE => NONE)
    1.38 @@ -605,12 +605,13 @@
    1.39            THEN rtac set_Nil_I 1
    1.40        | tac ctxt (Case (T, i) :: cont) =
    1.41            let
    1.42 -            val info = Datatype.the_info thy (fst (dest_Type T))
    1.43 +            val SOME {injects, distincts, case_thms, split, ...} =
    1.44 +              Ctr_Sugar.ctr_sugar_of ctxt (fst (dest_Type T))
    1.45            in
    1.46              (* do case distinction *)
    1.47 -            Splitter.split_tac [#split info] 1
    1.48 +            Splitter.split_tac [split] 1
    1.49              THEN EVERY (map_index (fn (i', _) =>
    1.50 -              (if i' < length (#case_rewrites info) - 1 then rtac @{thm conjI} 1 else all_tac)
    1.51 +              (if i' < length case_thms - 1 then rtac @{thm conjI} 1 else all_tac)
    1.52                THEN REPEAT_DETERM (rtac @{thm allI} 1)
    1.53                THEN rtac @{thm impI} 1
    1.54                THEN (if i' = i then
    1.55 @@ -619,7 +620,7 @@
    1.56                    CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K
    1.57                        ((HOLogic.conj_conv
    1.58                          (HOLogic.eq_conv Conv.all_conv (rewr_conv' (List.last prems)) then_conv
    1.59 -                          (Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq (#inject info)))))
    1.60 +                          (Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq injects))))
    1.61                          Conv.all_conv)
    1.62                          then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq))
    1.63                          then_conv conjunct_assoc_conv)) context
    1.64 @@ -636,7 +637,7 @@
    1.65                        (HOLogic.conj_conv
    1.66                          ((HOLogic.eq_conv Conv.all_conv
    1.67                            (rewr_conv' (List.last prems))) then_conv
    1.68 -                          (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) (#distinct info))))
    1.69 +                          (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) distincts)))
    1.70                          Conv.all_conv then_conv
    1.71                          (rewr_conv' @{lemma "(False & P) = False" by simp}))) context then_conv
    1.72                        HOLogic.Trueprop_conv
    1.73 @@ -646,16 +647,15 @@
    1.74                                (Conv.bottom_conv
    1.75                                  (K (rewr_conv'
    1.76                                    @{lemma "(EX x. P) = P" by simp})) ctxt)) context))) 1) ctxt 1
    1.77 -                THEN rtac set_Nil_I 1)) (#case_rewrites info))
    1.78 +                THEN rtac set_Nil_I 1)) case_thms)
    1.79            end
    1.80      fun make_inner_eqs bound_vs Tis eqs t =
    1.81        (case dest_case t of
    1.82 -        SOME (x, T, i, cont) =>
    1.83 +        SOME (x, T, i, cont, constr_name) =>
    1.84            let
    1.85              val (vs, body) = strip_abs (Envir.eta_long (map snd bound_vs) cont)
    1.86              val x' = incr_boundvars (length vs) x
    1.87              val eqs' = map (incr_boundvars (length vs)) eqs
    1.88 -            val (constr_name, _) = nth (the (Datatype.get_constrs thy (fst (dest_Type T)))) i
    1.89              val constr_t =
    1.90                list_comb
    1.91                  (Const (constr_name, map snd vs ---> T), map Bound (((length vs) - 1) downto 0))