avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time) -- relevant for any application using it, e.g. small paper sessions;
authorwenzelm
Fri Dec 07 16:25:33 2012 +0100 (2012-12-07)
changeset 50422ee729dbd1b7f
parent 50416 2e1b47e22fc6
child 50423 027d405951c8
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time) -- relevant for any application using it, e.g. small paper sessions;
src/HOL/Divides.thy
src/HOL/List.thy
src/HOL/Nat_Transfer.thy
src/HOL/Tools/list_code.ML
src/HOL/Tools/list_to_set_comprehension.ML
     1.1 --- a/src/HOL/Divides.thy	Fri Dec 07 14:30:00 2012 +0100
     1.2 +++ b/src/HOL/Divides.thy	Fri Dec 07 16:25:33 2012 +0100
     1.3 @@ -9,8 +9,6 @@
     1.4  imports Nat_Transfer
     1.5  begin
     1.6  
     1.7 -ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
     1.8 -
     1.9  subsection {* Syntactic division operations *}
    1.10  
    1.11  class div = dvd +
     2.1 --- a/src/HOL/List.thy	Fri Dec 07 14:30:00 2012 +0100
     2.2 +++ b/src/HOL/List.thy	Fri Dec 07 16:25:33 2012 +0100
     2.3 @@ -504,7 +504,228 @@
     2.4  *)
     2.5  
     2.6  
     2.7 -ML_file "Tools/list_to_set_comprehension.ML"
     2.8 +ML {*
     2.9 +(* Simproc for rewriting list comprehensions applied to List.set to set
    2.10 +   comprehension. *)
    2.11 +
    2.12 +signature LIST_TO_SET_COMPREHENSION =
    2.13 +sig
    2.14 +  val simproc : simpset -> cterm -> thm option
    2.15 +end
    2.16 +
    2.17 +structure List_to_Set_Comprehension : LIST_TO_SET_COMPREHENSION =
    2.18 +struct
    2.19 +
    2.20 +(* conversion *)
    2.21 +
    2.22 +fun all_exists_conv cv ctxt ct =
    2.23 +  (case Thm.term_of ct of
    2.24 +    Const (@{const_name HOL.Ex}, _) $ Abs _ =>
    2.25 +      Conv.arg_conv (Conv.abs_conv (all_exists_conv cv o #2) ctxt) ct
    2.26 +  | _ => cv ctxt ct)
    2.27 +
    2.28 +fun all_but_last_exists_conv cv ctxt ct =
    2.29 +  (case Thm.term_of ct of
    2.30 +    Const (@{const_name HOL.Ex}, _) $ Abs (_, _, Const (@{const_name HOL.Ex}, _) $ _) =>
    2.31 +      Conv.arg_conv (Conv.abs_conv (all_but_last_exists_conv cv o #2) ctxt) ct
    2.32 +  | _ => cv ctxt ct)
    2.33 +
    2.34 +fun Collect_conv cv ctxt ct =
    2.35 +  (case Thm.term_of ct of
    2.36 +    Const (@{const_name Set.Collect}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv cv ctxt) ct
    2.37 +  | _ => raise CTERM ("Collect_conv", [ct]))
    2.38 +
    2.39 +fun Trueprop_conv cv ct =
    2.40 +  (case Thm.term_of ct of
    2.41 +    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
    2.42 +  | _ => raise CTERM ("Trueprop_conv", [ct]))
    2.43 +
    2.44 +fun eq_conv cv1 cv2 ct =
    2.45 +  (case Thm.term_of ct of
    2.46 +    Const (@{const_name HOL.eq}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
    2.47 +  | _ => raise CTERM ("eq_conv", [ct]))
    2.48 +
    2.49 +fun conj_conv cv1 cv2 ct =
    2.50 +  (case Thm.term_of ct of
    2.51 +    Const (@{const_name HOL.conj}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
    2.52 +  | _ => raise CTERM ("conj_conv", [ct]))
    2.53 +
    2.54 +fun rewr_conv' th = Conv.rewr_conv (mk_meta_eq th)
    2.55 +
    2.56 +fun conjunct_assoc_conv ct =
    2.57 +  Conv.try_conv
    2.58 +    (rewr_conv' @{thm conj_assoc} then_conv conj_conv Conv.all_conv conjunct_assoc_conv) ct
    2.59 +
    2.60 +fun right_hand_set_comprehension_conv conv ctxt =
    2.61 +  Trueprop_conv (eq_conv Conv.all_conv
    2.62 +    (Collect_conv (all_exists_conv conv o #2) ctxt))
    2.63 +
    2.64 +
    2.65 +(* term abstraction of list comprehension patterns *)
    2.66 +
    2.67 +datatype termlets = If | Case of (typ * int)
    2.68 +
    2.69 +fun simproc ss redex =
    2.70 +  let
    2.71 +    val ctxt = Simplifier.the_context ss
    2.72 +    val thy = Proof_Context.theory_of ctxt
    2.73 +    val set_Nil_I = @{thm trans} OF [@{thm set.simps(1)}, @{thm empty_def}]
    2.74 +    val set_singleton = @{lemma "set [a] = {x. x = a}" by simp}
    2.75 +    val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp}
    2.76 +    val del_refl_eq = @{lemma "(t = t & P) == P" by simp}
    2.77 +    fun mk_set T = Const (@{const_name List.set}, HOLogic.listT T --> HOLogic.mk_setT T)
    2.78 +    fun dest_set (Const (@{const_name List.set}, _) $ xs) = xs
    2.79 +    fun dest_singleton_list (Const (@{const_name List.Cons}, _)
    2.80 +          $ t $ (Const (@{const_name List.Nil}, _))) = t
    2.81 +      | dest_singleton_list t = raise TERM ("dest_singleton_list", [t])
    2.82 +    (* We check that one case returns a singleton list and all other cases
    2.83 +       return [], and return the index of the one singleton list case *)
    2.84 +    fun possible_index_of_singleton_case cases =
    2.85 +      let
    2.86 +        fun check (i, case_t) s =
    2.87 +          (case strip_abs_body case_t of
    2.88 +            (Const (@{const_name List.Nil}, _)) => s
    2.89 +          | _ => (case s of NONE => SOME i | SOME _ => NONE))
    2.90 +      in
    2.91 +        fold_index check cases NONE
    2.92 +      end
    2.93 +    (* returns (case_expr type index chosen_case) option  *)
    2.94 +    fun dest_case case_term =
    2.95 +      let
    2.96 +        val (case_const, args) = strip_comb case_term
    2.97 +      in
    2.98 +        (case try dest_Const case_const of
    2.99 +          SOME (c, T) =>
   2.100 +            (case Datatype.info_of_case thy c of
   2.101 +              SOME _ =>
   2.102 +                (case possible_index_of_singleton_case (fst (split_last args)) of
   2.103 +                  SOME i =>
   2.104 +                    let
   2.105 +                      val (Ts, _) = strip_type T
   2.106 +                      val T' = List.last Ts
   2.107 +                    in SOME (List.last args, T', i, nth args i) end
   2.108 +                | NONE => NONE)
   2.109 +            | NONE => NONE)
   2.110 +        | NONE => NONE)
   2.111 +      end
   2.112 +    (* returns condition continuing term option *)
   2.113 +    fun dest_if (Const (@{const_name If}, _) $ cond $ then_t $ Const (@{const_name Nil}, _)) =
   2.114 +          SOME (cond, then_t)
   2.115 +      | dest_if _ = NONE
   2.116 +    fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1
   2.117 +      | tac ctxt (If :: cont) =
   2.118 +          Splitter.split_tac [@{thm split_if}] 1
   2.119 +          THEN rtac @{thm conjI} 1
   2.120 +          THEN rtac @{thm impI} 1
   2.121 +          THEN Subgoal.FOCUS (fn {prems, context, ...} =>
   2.122 +            CONVERSION (right_hand_set_comprehension_conv (K
   2.123 +              (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv
   2.124 +               then_conv
   2.125 +               rewr_conv' @{lemma "(True & P) = P" by simp})) context) 1) ctxt 1
   2.126 +          THEN tac ctxt cont
   2.127 +          THEN rtac @{thm impI} 1
   2.128 +          THEN Subgoal.FOCUS (fn {prems, context, ...} =>
   2.129 +              CONVERSION (right_hand_set_comprehension_conv (K
   2.130 +                (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv
   2.131 +                 then_conv rewr_conv' @{lemma "(False & P) = False" by simp})) context) 1) ctxt 1
   2.132 +          THEN rtac set_Nil_I 1
   2.133 +      | tac ctxt (Case (T, i) :: cont) =
   2.134 +          let
   2.135 +            val info = Datatype.the_info thy (fst (dest_Type T))
   2.136 +          in
   2.137 +            (* do case distinction *)
   2.138 +            Splitter.split_tac [#split info] 1
   2.139 +            THEN EVERY (map_index (fn (i', _) =>
   2.140 +              (if i' < length (#case_rewrites info) - 1 then rtac @{thm conjI} 1 else all_tac)
   2.141 +              THEN REPEAT_DETERM (rtac @{thm allI} 1)
   2.142 +              THEN rtac @{thm impI} 1
   2.143 +              THEN (if i' = i then
   2.144 +                (* continue recursively *)
   2.145 +                Subgoal.FOCUS (fn {prems, context, ...} =>
   2.146 +                  CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K
   2.147 +                      ((conj_conv
   2.148 +                        (eq_conv Conv.all_conv (rewr_conv' (List.last prems)) then_conv
   2.149 +                          (Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq (#inject info)))))
   2.150 +                        Conv.all_conv)
   2.151 +                        then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq))
   2.152 +                        then_conv conjunct_assoc_conv)) context
   2.153 +                    then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>
   2.154 +                      Conv.repeat_conv
   2.155 +                        (all_but_last_exists_conv
   2.156 +                          (K (rewr_conv'
   2.157 +                            @{lemma "(EX x. x = t & P x) = P t" by simp})) ctxt)) context)))) 1) ctxt 1
   2.158 +                THEN tac ctxt cont
   2.159 +              else
   2.160 +                Subgoal.FOCUS (fn {prems, context, ...} =>
   2.161 +                  CONVERSION
   2.162 +                    (right_hand_set_comprehension_conv (K
   2.163 +                      (conj_conv
   2.164 +                        ((eq_conv Conv.all_conv
   2.165 +                          (rewr_conv' (List.last prems))) then_conv
   2.166 +                          (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) (#distinct info))))
   2.167 +                        Conv.all_conv then_conv
   2.168 +                        (rewr_conv' @{lemma "(False & P) = False" by simp}))) context then_conv
   2.169 +                      Trueprop_conv
   2.170 +                        (eq_conv Conv.all_conv
   2.171 +                          (Collect_conv (fn (_, ctxt) =>
   2.172 +                            Conv.repeat_conv
   2.173 +                              (Conv.bottom_conv
   2.174 +                                (K (rewr_conv'
   2.175 +                                  @{lemma "(EX x. P) = P" by simp})) ctxt)) context))) 1) ctxt 1
   2.176 +                THEN rtac set_Nil_I 1)) (#case_rewrites info))
   2.177 +          end
   2.178 +    fun make_inner_eqs bound_vs Tis eqs t =
   2.179 +      (case dest_case t of
   2.180 +        SOME (x, T, i, cont) =>
   2.181 +          let
   2.182 +            val (vs, body) = strip_abs (Pattern.eta_long (map snd bound_vs) cont)
   2.183 +            val x' = incr_boundvars (length vs) x
   2.184 +            val eqs' = map (incr_boundvars (length vs)) eqs
   2.185 +            val (constr_name, _) = nth (the (Datatype.get_constrs thy (fst (dest_Type T)))) i
   2.186 +            val constr_t =
   2.187 +              list_comb
   2.188 +                (Const (constr_name, map snd vs ---> T), map Bound (((length vs) - 1) downto 0))
   2.189 +            val constr_eq = Const (@{const_name HOL.eq}, T --> T --> @{typ bool}) $ constr_t $ x'
   2.190 +          in
   2.191 +            make_inner_eqs (rev vs @ bound_vs) (Case (T, i) :: Tis) (constr_eq :: eqs') body
   2.192 +          end
   2.193 +      | NONE =>
   2.194 +          (case dest_if t of
   2.195 +            SOME (condition, cont) => make_inner_eqs bound_vs (If :: Tis) (condition :: eqs) cont
   2.196 +          | NONE =>
   2.197 +            if eqs = [] then NONE (* no rewriting, nothing to be done *)
   2.198 +            else
   2.199 +              let
   2.200 +                val Type (@{type_name List.list}, [rT]) = fastype_of1 (map snd bound_vs, t)
   2.201 +                val pat_eq =
   2.202 +                  (case try dest_singleton_list t of
   2.203 +                    SOME t' =>
   2.204 +                      Const (@{const_name HOL.eq}, rT --> rT --> @{typ bool}) $
   2.205 +                        Bound (length bound_vs) $ t'
   2.206 +                  | NONE =>
   2.207 +                      Const (@{const_name Set.member}, rT --> HOLogic.mk_setT rT --> @{typ bool}) $
   2.208 +                        Bound (length bound_vs) $ (mk_set rT $ t))
   2.209 +                val reverse_bounds = curry subst_bounds
   2.210 +                  ((map Bound ((length bound_vs - 1) downto 0)) @ [Bound (length bound_vs)])
   2.211 +                val eqs' = map reverse_bounds eqs
   2.212 +                val pat_eq' = reverse_bounds pat_eq
   2.213 +                val inner_t =
   2.214 +                  fold (fn (_, T) => fn t => HOLogic.exists_const T $ absdummy T t)
   2.215 +                    (rev bound_vs) (fold (curry HOLogic.mk_conj) eqs' pat_eq')
   2.216 +                val lhs = term_of redex
   2.217 +                val rhs = HOLogic.mk_Collect ("x", rT, inner_t)
   2.218 +                val rewrite_rule_t = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   2.219 +              in
   2.220 +                SOME
   2.221 +                  ((Goal.prove ctxt [] [] rewrite_rule_t
   2.222 +                    (fn {context, ...} => tac context (rev Tis))) RS @{thm eq_reflection})
   2.223 +              end))
   2.224 +  in
   2.225 +    make_inner_eqs [] [] [] (dest_set (term_of redex))
   2.226 +  end
   2.227 +
   2.228 +end
   2.229 +*}
   2.230  
   2.231  simproc_setup list_to_set_comprehension ("set xs") = {* K List_to_Set_Comprehension.simproc *}
   2.232  
   2.233 @@ -5664,7 +5885,57 @@
   2.234  
   2.235  subsubsection {* Pretty lists *}
   2.236  
   2.237 -ML_file "Tools/list_code.ML"
   2.238 +ML {*
   2.239 +(* Code generation for list literals. *)
   2.240 +
   2.241 +signature LIST_CODE =
   2.242 +sig
   2.243 +  val implode_list: string -> string -> Code_Thingol.iterm -> Code_Thingol.iterm list option
   2.244 +  val default_list: int * string
   2.245 +    -> (Code_Printer.fixity -> Code_Thingol.iterm -> Pretty.T)
   2.246 +    -> Code_Printer.fixity -> Code_Thingol.iterm -> Code_Thingol.iterm -> Pretty.T
   2.247 +  val add_literal_list: string -> theory -> theory
   2.248 +end;
   2.249 +
   2.250 +structure List_Code : LIST_CODE =
   2.251 +struct
   2.252 +
   2.253 +open Basic_Code_Thingol;
   2.254 +
   2.255 +fun implode_list nil' cons' t =
   2.256 +  let
   2.257 +    fun dest_cons (IConst { name = c, ... } `$ t1 `$ t2) =
   2.258 +          if c = cons'
   2.259 +          then SOME (t1, t2)
   2.260 +          else NONE
   2.261 +      | dest_cons _ = NONE;
   2.262 +    val (ts, t') = Code_Thingol.unfoldr dest_cons t;
   2.263 +  in case t'
   2.264 +   of IConst { name = c, ... } => if c = nil' then SOME ts else NONE
   2.265 +    | _ => NONE
   2.266 +  end;
   2.267 +
   2.268 +fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
   2.269 +  Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy (
   2.270 +    pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
   2.271 +    Code_Printer.str target_cons,
   2.272 +    pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
   2.273 +  );
   2.274 +
   2.275 +fun add_literal_list target =
   2.276 +  let
   2.277 +    fun pretty literals [nil', cons'] pr thm vars fxy [(t1, _), (t2, _)] =
   2.278 +      case Option.map (cons t1) (implode_list nil' cons' t2)
   2.279 +       of SOME ts =>
   2.280 +            Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
   2.281 +        | NONE =>
   2.282 +            default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
   2.283 +  in Code_Target.add_const_syntax target @{const_name Cons}
   2.284 +    (SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))
   2.285 +  end
   2.286 +
   2.287 +end;
   2.288 +*}
   2.289  
   2.290  code_type list
   2.291    (SML "_ list")
     3.1 --- a/src/HOL/Nat_Transfer.thy	Fri Dec 07 14:30:00 2012 +0100
     3.2 +++ b/src/HOL/Nat_Transfer.thy	Fri Dec 07 16:25:33 2012 +0100
     3.3 @@ -420,4 +420,8 @@
     3.4    return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
     3.5    cong: setsum_cong setprod_cong]
     3.6  
     3.7 +
     3.8 +(*belongs to Divides.thy, but slows down dependency discovery*)
     3.9 +ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
    3.10 +
    3.11  end
     4.1 --- a/src/HOL/Tools/list_code.ML	Fri Dec 07 14:30:00 2012 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,53 +0,0 @@
     4.4 -(*  Title:  HOL/Tools/list_code.ML
     4.5 -    Author: Florian Haftmann, TU Muenchen
     4.6 -
     4.7 -Code generation for list literals.
     4.8 -*)
     4.9 -
    4.10 -signature LIST_CODE =
    4.11 -sig
    4.12 -  val implode_list: string -> string -> Code_Thingol.iterm -> Code_Thingol.iterm list option
    4.13 -  val default_list: int * string
    4.14 -    -> (Code_Printer.fixity -> Code_Thingol.iterm -> Pretty.T)
    4.15 -    -> Code_Printer.fixity -> Code_Thingol.iterm -> Code_Thingol.iterm -> Pretty.T
    4.16 -  val add_literal_list: string -> theory -> theory
    4.17 -end;
    4.18 -
    4.19 -structure List_Code : LIST_CODE =
    4.20 -struct
    4.21 -
    4.22 -open Basic_Code_Thingol;
    4.23 -
    4.24 -fun implode_list nil' cons' t =
    4.25 -  let
    4.26 -    fun dest_cons (IConst { name = c, ... } `$ t1 `$ t2) =
    4.27 -          if c = cons'
    4.28 -          then SOME (t1, t2)
    4.29 -          else NONE
    4.30 -      | dest_cons _ = NONE;
    4.31 -    val (ts, t') = Code_Thingol.unfoldr dest_cons t;
    4.32 -  in case t'
    4.33 -   of IConst { name = c, ... } => if c = nil' then SOME ts else NONE
    4.34 -    | _ => NONE
    4.35 -  end;
    4.36 -
    4.37 -fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
    4.38 -  Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy (
    4.39 -    pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
    4.40 -    Code_Printer.str target_cons,
    4.41 -    pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
    4.42 -  );
    4.43 -
    4.44 -fun add_literal_list target =
    4.45 -  let
    4.46 -    fun pretty literals [nil', cons'] pr thm vars fxy [(t1, _), (t2, _)] =
    4.47 -      case Option.map (cons t1) (implode_list nil' cons' t2)
    4.48 -       of SOME ts =>
    4.49 -            Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
    4.50 -        | NONE =>
    4.51 -            default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
    4.52 -  in Code_Target.add_const_syntax target @{const_name Cons}
    4.53 -    (SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))
    4.54 -  end
    4.55 -
    4.56 -end;
     5.1 --- a/src/HOL/Tools/list_to_set_comprehension.ML	Fri Dec 07 14:30:00 2012 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,224 +0,0 @@
     5.4 -(*  Title:      HOL/Tools/list_to_set_comprehension.ML
     5.5 -    Author:     Lukas Bulwahn, TU Muenchen
     5.6 -
     5.7 -Simproc for rewriting list comprehensions applied to List.set to set
     5.8 -comprehension.
     5.9 -*)
    5.10 -
    5.11 -signature LIST_TO_SET_COMPREHENSION =
    5.12 -sig
    5.13 -  val simproc : simpset -> cterm -> thm option
    5.14 -end
    5.15 -
    5.16 -structure List_to_Set_Comprehension : LIST_TO_SET_COMPREHENSION =
    5.17 -struct
    5.18 -
    5.19 -(* conversion *)
    5.20 -
    5.21 -fun all_exists_conv cv ctxt ct =
    5.22 -  (case Thm.term_of ct of
    5.23 -    Const (@{const_name HOL.Ex}, _) $ Abs _ =>
    5.24 -      Conv.arg_conv (Conv.abs_conv (all_exists_conv cv o #2) ctxt) ct
    5.25 -  | _ => cv ctxt ct)
    5.26 -
    5.27 -fun all_but_last_exists_conv cv ctxt ct =
    5.28 -  (case Thm.term_of ct of
    5.29 -    Const (@{const_name HOL.Ex}, _) $ Abs (_, _, Const (@{const_name HOL.Ex}, _) $ _) =>
    5.30 -      Conv.arg_conv (Conv.abs_conv (all_but_last_exists_conv cv o #2) ctxt) ct
    5.31 -  | _ => cv ctxt ct)
    5.32 -
    5.33 -fun Collect_conv cv ctxt ct =
    5.34 -  (case Thm.term_of ct of
    5.35 -    Const (@{const_name Set.Collect}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv cv ctxt) ct
    5.36 -  | _ => raise CTERM ("Collect_conv", [ct]))
    5.37 -
    5.38 -fun Trueprop_conv cv ct =
    5.39 -  (case Thm.term_of ct of
    5.40 -    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
    5.41 -  | _ => raise CTERM ("Trueprop_conv", [ct]))
    5.42 -
    5.43 -fun eq_conv cv1 cv2 ct =
    5.44 -  (case Thm.term_of ct of
    5.45 -    Const (@{const_name HOL.eq}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
    5.46 -  | _ => raise CTERM ("eq_conv", [ct]))
    5.47 -
    5.48 -fun conj_conv cv1 cv2 ct =
    5.49 -  (case Thm.term_of ct of
    5.50 -    Const (@{const_name HOL.conj}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
    5.51 -  | _ => raise CTERM ("conj_conv", [ct]))
    5.52 -
    5.53 -fun rewr_conv' th = Conv.rewr_conv (mk_meta_eq th)
    5.54 -
    5.55 -fun conjunct_assoc_conv ct =
    5.56 -  Conv.try_conv
    5.57 -    (rewr_conv' @{thm conj_assoc} then_conv conj_conv Conv.all_conv conjunct_assoc_conv) ct
    5.58 -
    5.59 -fun right_hand_set_comprehension_conv conv ctxt =
    5.60 -  Trueprop_conv (eq_conv Conv.all_conv
    5.61 -    (Collect_conv (all_exists_conv conv o #2) ctxt))
    5.62 -
    5.63 -
    5.64 -(* term abstraction of list comprehension patterns *)
    5.65 -
    5.66 -datatype termlets = If | Case of (typ * int)
    5.67 -
    5.68 -fun simproc ss redex =
    5.69 -  let
    5.70 -    val ctxt = Simplifier.the_context ss
    5.71 -    val thy = Proof_Context.theory_of ctxt
    5.72 -    val set_Nil_I = @{thm trans} OF [@{thm set.simps(1)}, @{thm empty_def}]
    5.73 -    val set_singleton = @{lemma "set [a] = {x. x = a}" by simp}
    5.74 -    val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp}
    5.75 -    val del_refl_eq = @{lemma "(t = t & P) == P" by simp}
    5.76 -    fun mk_set T = Const (@{const_name List.set}, HOLogic.listT T --> HOLogic.mk_setT T)
    5.77 -    fun dest_set (Const (@{const_name List.set}, _) $ xs) = xs
    5.78 -    fun dest_singleton_list (Const (@{const_name List.Cons}, _)
    5.79 -          $ t $ (Const (@{const_name List.Nil}, _))) = t
    5.80 -      | dest_singleton_list t = raise TERM ("dest_singleton_list", [t])
    5.81 -    (* We check that one case returns a singleton list and all other cases
    5.82 -       return [], and return the index of the one singleton list case *)
    5.83 -    fun possible_index_of_singleton_case cases =
    5.84 -      let
    5.85 -        fun check (i, case_t) s =
    5.86 -          (case strip_abs_body case_t of
    5.87 -            (Const (@{const_name List.Nil}, _)) => s
    5.88 -          | _ => (case s of NONE => SOME i | SOME _ => NONE))
    5.89 -      in
    5.90 -        fold_index check cases NONE
    5.91 -      end
    5.92 -    (* returns (case_expr type index chosen_case) option  *)
    5.93 -    fun dest_case case_term =
    5.94 -      let
    5.95 -        val (case_const, args) = strip_comb case_term
    5.96 -      in
    5.97 -        (case try dest_Const case_const of
    5.98 -          SOME (c, T) =>
    5.99 -            (case Datatype.info_of_case thy c of
   5.100 -              SOME _ =>
   5.101 -                (case possible_index_of_singleton_case (fst (split_last args)) of
   5.102 -                  SOME i =>
   5.103 -                    let
   5.104 -                      val (Ts, _) = strip_type T
   5.105 -                      val T' = List.last Ts
   5.106 -                    in SOME (List.last args, T', i, nth args i) end
   5.107 -                | NONE => NONE)
   5.108 -            | NONE => NONE)
   5.109 -        | NONE => NONE)
   5.110 -      end
   5.111 -    (* returns condition continuing term option *)
   5.112 -    fun dest_if (Const (@{const_name If}, _) $ cond $ then_t $ Const (@{const_name Nil}, _)) =
   5.113 -          SOME (cond, then_t)
   5.114 -      | dest_if _ = NONE
   5.115 -    fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1
   5.116 -      | tac ctxt (If :: cont) =
   5.117 -          Splitter.split_tac [@{thm split_if}] 1
   5.118 -          THEN rtac @{thm conjI} 1
   5.119 -          THEN rtac @{thm impI} 1
   5.120 -          THEN Subgoal.FOCUS (fn {prems, context, ...} =>
   5.121 -            CONVERSION (right_hand_set_comprehension_conv (K
   5.122 -              (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv
   5.123 -               then_conv
   5.124 -               rewr_conv' @{lemma "(True & P) = P" by simp})) context) 1) ctxt 1
   5.125 -          THEN tac ctxt cont
   5.126 -          THEN rtac @{thm impI} 1
   5.127 -          THEN Subgoal.FOCUS (fn {prems, context, ...} =>
   5.128 -              CONVERSION (right_hand_set_comprehension_conv (K
   5.129 -                (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv
   5.130 -                 then_conv rewr_conv' @{lemma "(False & P) = False" by simp})) context) 1) ctxt 1
   5.131 -          THEN rtac set_Nil_I 1
   5.132 -      | tac ctxt (Case (T, i) :: cont) =
   5.133 -          let
   5.134 -            val info = Datatype.the_info thy (fst (dest_Type T))
   5.135 -          in
   5.136 -            (* do case distinction *)
   5.137 -            Splitter.split_tac [#split info] 1
   5.138 -            THEN EVERY (map_index (fn (i', _) =>
   5.139 -              (if i' < length (#case_rewrites info) - 1 then rtac @{thm conjI} 1 else all_tac)
   5.140 -              THEN REPEAT_DETERM (rtac @{thm allI} 1)
   5.141 -              THEN rtac @{thm impI} 1
   5.142 -              THEN (if i' = i then
   5.143 -                (* continue recursively *)
   5.144 -                Subgoal.FOCUS (fn {prems, context, ...} =>
   5.145 -                  CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K
   5.146 -                      ((conj_conv
   5.147 -                        (eq_conv Conv.all_conv (rewr_conv' (List.last prems)) then_conv
   5.148 -                          (Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq (#inject info)))))
   5.149 -                        Conv.all_conv)
   5.150 -                        then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq))
   5.151 -                        then_conv conjunct_assoc_conv)) context
   5.152 -                    then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>
   5.153 -                      Conv.repeat_conv
   5.154 -                        (all_but_last_exists_conv
   5.155 -                          (K (rewr_conv'
   5.156 -                            @{lemma "(EX x. x = t & P x) = P t" by simp})) ctxt)) context)))) 1) ctxt 1
   5.157 -                THEN tac ctxt cont
   5.158 -              else
   5.159 -                Subgoal.FOCUS (fn {prems, context, ...} =>
   5.160 -                  CONVERSION
   5.161 -                    (right_hand_set_comprehension_conv (K
   5.162 -                      (conj_conv
   5.163 -                        ((eq_conv Conv.all_conv
   5.164 -                          (rewr_conv' (List.last prems))) then_conv
   5.165 -                          (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) (#distinct info))))
   5.166 -                        Conv.all_conv then_conv
   5.167 -                        (rewr_conv' @{lemma "(False & P) = False" by simp}))) context then_conv
   5.168 -                      Trueprop_conv
   5.169 -                        (eq_conv Conv.all_conv
   5.170 -                          (Collect_conv (fn (_, ctxt) =>
   5.171 -                            Conv.repeat_conv
   5.172 -                              (Conv.bottom_conv
   5.173 -                                (K (rewr_conv'
   5.174 -                                  @{lemma "(EX x. P) = P" by simp})) ctxt)) context))) 1) ctxt 1
   5.175 -                THEN rtac set_Nil_I 1)) (#case_rewrites info))
   5.176 -          end
   5.177 -    fun make_inner_eqs bound_vs Tis eqs t =
   5.178 -      (case dest_case t of
   5.179 -        SOME (x, T, i, cont) =>
   5.180 -          let
   5.181 -            val (vs, body) = strip_abs (Pattern.eta_long (map snd bound_vs) cont)
   5.182 -            val x' = incr_boundvars (length vs) x
   5.183 -            val eqs' = map (incr_boundvars (length vs)) eqs
   5.184 -            val (constr_name, _) = nth (the (Datatype.get_constrs thy (fst (dest_Type T)))) i
   5.185 -            val constr_t =
   5.186 -              list_comb
   5.187 -                (Const (constr_name, map snd vs ---> T), map Bound (((length vs) - 1) downto 0))
   5.188 -            val constr_eq = Const (@{const_name HOL.eq}, T --> T --> @{typ bool}) $ constr_t $ x'
   5.189 -          in
   5.190 -            make_inner_eqs (rev vs @ bound_vs) (Case (T, i) :: Tis) (constr_eq :: eqs') body
   5.191 -          end
   5.192 -      | NONE =>
   5.193 -          (case dest_if t of
   5.194 -            SOME (condition, cont) => make_inner_eqs bound_vs (If :: Tis) (condition :: eqs) cont
   5.195 -          | NONE =>
   5.196 -            if eqs = [] then NONE (* no rewriting, nothing to be done *)
   5.197 -            else
   5.198 -              let
   5.199 -                val Type (@{type_name List.list}, [rT]) = fastype_of1 (map snd bound_vs, t)
   5.200 -                val pat_eq =
   5.201 -                  (case try dest_singleton_list t of
   5.202 -                    SOME t' =>
   5.203 -                      Const (@{const_name HOL.eq}, rT --> rT --> @{typ bool}) $
   5.204 -                        Bound (length bound_vs) $ t'
   5.205 -                  | NONE =>
   5.206 -                      Const (@{const_name Set.member}, rT --> HOLogic.mk_setT rT --> @{typ bool}) $
   5.207 -                        Bound (length bound_vs) $ (mk_set rT $ t))
   5.208 -                val reverse_bounds = curry subst_bounds
   5.209 -                  ((map Bound ((length bound_vs - 1) downto 0)) @ [Bound (length bound_vs)])
   5.210 -                val eqs' = map reverse_bounds eqs
   5.211 -                val pat_eq' = reverse_bounds pat_eq
   5.212 -                val inner_t =
   5.213 -                  fold (fn (_, T) => fn t => HOLogic.exists_const T $ absdummy T t)
   5.214 -                    (rev bound_vs) (fold (curry HOLogic.mk_conj) eqs' pat_eq')
   5.215 -                val lhs = term_of redex
   5.216 -                val rhs = HOLogic.mk_Collect ("x", rT, inner_t)
   5.217 -                val rewrite_rule_t = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   5.218 -              in
   5.219 -                SOME
   5.220 -                  ((Goal.prove ctxt [] [] rewrite_rule_t
   5.221 -                    (fn {context, ...} => tac context (rev Tis))) RS @{thm eq_reflection})
   5.222 -              end))
   5.223 -  in
   5.224 -    make_inner_eqs [] [] [] (dest_set (term_of redex))
   5.225 -  end
   5.226 -
   5.227 -end