src/HOL/List.thy
changeset 50422 ee729dbd1b7f
parent 50134 13211e07d931
child 50548 0aec55e63795
     1.1 --- a/src/HOL/List.thy	Fri Dec 07 14:30:00 2012 +0100
     1.2 +++ b/src/HOL/List.thy	Fri Dec 07 16:25:33 2012 +0100
     1.3 @@ -504,7 +504,228 @@
     1.4  *)
     1.5  
     1.6  
     1.7 -ML_file "Tools/list_to_set_comprehension.ML"
     1.8 +ML {*
     1.9 +(* Simproc for rewriting list comprehensions applied to List.set to set
    1.10 +   comprehension. *)
    1.11 +
    1.12 +signature LIST_TO_SET_COMPREHENSION =
    1.13 +sig
    1.14 +  val simproc : simpset -> cterm -> thm option
    1.15 +end
    1.16 +
    1.17 +structure List_to_Set_Comprehension : LIST_TO_SET_COMPREHENSION =
    1.18 +struct
    1.19 +
    1.20 +(* conversion *)
    1.21 +
    1.22 +fun all_exists_conv cv ctxt ct =
    1.23 +  (case Thm.term_of ct of
    1.24 +    Const (@{const_name HOL.Ex}, _) $ Abs _ =>
    1.25 +      Conv.arg_conv (Conv.abs_conv (all_exists_conv cv o #2) ctxt) ct
    1.26 +  | _ => cv ctxt ct)
    1.27 +
    1.28 +fun all_but_last_exists_conv cv ctxt ct =
    1.29 +  (case Thm.term_of ct of
    1.30 +    Const (@{const_name HOL.Ex}, _) $ Abs (_, _, Const (@{const_name HOL.Ex}, _) $ _) =>
    1.31 +      Conv.arg_conv (Conv.abs_conv (all_but_last_exists_conv cv o #2) ctxt) ct
    1.32 +  | _ => cv ctxt ct)
    1.33 +
    1.34 +fun Collect_conv cv ctxt ct =
    1.35 +  (case Thm.term_of ct of
    1.36 +    Const (@{const_name Set.Collect}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv cv ctxt) ct
    1.37 +  | _ => raise CTERM ("Collect_conv", [ct]))
    1.38 +
    1.39 +fun Trueprop_conv cv ct =
    1.40 +  (case Thm.term_of ct of
    1.41 +    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
    1.42 +  | _ => raise CTERM ("Trueprop_conv", [ct]))
    1.43 +
    1.44 +fun eq_conv cv1 cv2 ct =
    1.45 +  (case Thm.term_of ct of
    1.46 +    Const (@{const_name HOL.eq}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
    1.47 +  | _ => raise CTERM ("eq_conv", [ct]))
    1.48 +
    1.49 +fun conj_conv cv1 cv2 ct =
    1.50 +  (case Thm.term_of ct of
    1.51 +    Const (@{const_name HOL.conj}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
    1.52 +  | _ => raise CTERM ("conj_conv", [ct]))
    1.53 +
    1.54 +fun rewr_conv' th = Conv.rewr_conv (mk_meta_eq th)
    1.55 +
    1.56 +fun conjunct_assoc_conv ct =
    1.57 +  Conv.try_conv
    1.58 +    (rewr_conv' @{thm conj_assoc} then_conv conj_conv Conv.all_conv conjunct_assoc_conv) ct
    1.59 +
    1.60 +fun right_hand_set_comprehension_conv conv ctxt =
    1.61 +  Trueprop_conv (eq_conv Conv.all_conv
    1.62 +    (Collect_conv (all_exists_conv conv o #2) ctxt))
    1.63 +
    1.64 +
    1.65 +(* term abstraction of list comprehension patterns *)
    1.66 +
    1.67 +datatype termlets = If | Case of (typ * int)
    1.68 +
    1.69 +fun simproc ss redex =
    1.70 +  let
    1.71 +    val ctxt = Simplifier.the_context ss
    1.72 +    val thy = Proof_Context.theory_of ctxt
    1.73 +    val set_Nil_I = @{thm trans} OF [@{thm set.simps(1)}, @{thm empty_def}]
    1.74 +    val set_singleton = @{lemma "set [a] = {x. x = a}" by simp}
    1.75 +    val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp}
    1.76 +    val del_refl_eq = @{lemma "(t = t & P) == P" by simp}
    1.77 +    fun mk_set T = Const (@{const_name List.set}, HOLogic.listT T --> HOLogic.mk_setT T)
    1.78 +    fun dest_set (Const (@{const_name List.set}, _) $ xs) = xs
    1.79 +    fun dest_singleton_list (Const (@{const_name List.Cons}, _)
    1.80 +          $ t $ (Const (@{const_name List.Nil}, _))) = t
    1.81 +      | dest_singleton_list t = raise TERM ("dest_singleton_list", [t])
    1.82 +    (* We check that one case returns a singleton list and all other cases
    1.83 +       return [], and return the index of the one singleton list case *)
    1.84 +    fun possible_index_of_singleton_case cases =
    1.85 +      let
    1.86 +        fun check (i, case_t) s =
    1.87 +          (case strip_abs_body case_t of
    1.88 +            (Const (@{const_name List.Nil}, _)) => s
    1.89 +          | _ => (case s of NONE => SOME i | SOME _ => NONE))
    1.90 +      in
    1.91 +        fold_index check cases NONE
    1.92 +      end
    1.93 +    (* returns (case_expr type index chosen_case) option  *)
    1.94 +    fun dest_case case_term =
    1.95 +      let
    1.96 +        val (case_const, args) = strip_comb case_term
    1.97 +      in
    1.98 +        (case try dest_Const case_const of
    1.99 +          SOME (c, T) =>
   1.100 +            (case Datatype.info_of_case thy c of
   1.101 +              SOME _ =>
   1.102 +                (case possible_index_of_singleton_case (fst (split_last args)) of
   1.103 +                  SOME i =>
   1.104 +                    let
   1.105 +                      val (Ts, _) = strip_type T
   1.106 +                      val T' = List.last Ts
   1.107 +                    in SOME (List.last args, T', i, nth args i) end
   1.108 +                | NONE => NONE)
   1.109 +            | NONE => NONE)
   1.110 +        | NONE => NONE)
   1.111 +      end
   1.112 +    (* returns condition continuing term option *)
   1.113 +    fun dest_if (Const (@{const_name If}, _) $ cond $ then_t $ Const (@{const_name Nil}, _)) =
   1.114 +          SOME (cond, then_t)
   1.115 +      | dest_if _ = NONE
   1.116 +    fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1
   1.117 +      | tac ctxt (If :: cont) =
   1.118 +          Splitter.split_tac [@{thm split_if}] 1
   1.119 +          THEN rtac @{thm conjI} 1
   1.120 +          THEN rtac @{thm impI} 1
   1.121 +          THEN Subgoal.FOCUS (fn {prems, context, ...} =>
   1.122 +            CONVERSION (right_hand_set_comprehension_conv (K
   1.123 +              (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv
   1.124 +               then_conv
   1.125 +               rewr_conv' @{lemma "(True & P) = P" by simp})) context) 1) ctxt 1
   1.126 +          THEN tac ctxt cont
   1.127 +          THEN rtac @{thm impI} 1
   1.128 +          THEN Subgoal.FOCUS (fn {prems, context, ...} =>
   1.129 +              CONVERSION (right_hand_set_comprehension_conv (K
   1.130 +                (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv
   1.131 +                 then_conv rewr_conv' @{lemma "(False & P) = False" by simp})) context) 1) ctxt 1
   1.132 +          THEN rtac set_Nil_I 1
   1.133 +      | tac ctxt (Case (T, i) :: cont) =
   1.134 +          let
   1.135 +            val info = Datatype.the_info thy (fst (dest_Type T))
   1.136 +          in
   1.137 +            (* do case distinction *)
   1.138 +            Splitter.split_tac [#split info] 1
   1.139 +            THEN EVERY (map_index (fn (i', _) =>
   1.140 +              (if i' < length (#case_rewrites info) - 1 then rtac @{thm conjI} 1 else all_tac)
   1.141 +              THEN REPEAT_DETERM (rtac @{thm allI} 1)
   1.142 +              THEN rtac @{thm impI} 1
   1.143 +              THEN (if i' = i then
   1.144 +                (* continue recursively *)
   1.145 +                Subgoal.FOCUS (fn {prems, context, ...} =>
   1.146 +                  CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K
   1.147 +                      ((conj_conv
   1.148 +                        (eq_conv Conv.all_conv (rewr_conv' (List.last prems)) then_conv
   1.149 +                          (Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq (#inject info)))))
   1.150 +                        Conv.all_conv)
   1.151 +                        then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq))
   1.152 +                        then_conv conjunct_assoc_conv)) context
   1.153 +                    then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>
   1.154 +                      Conv.repeat_conv
   1.155 +                        (all_but_last_exists_conv
   1.156 +                          (K (rewr_conv'
   1.157 +                            @{lemma "(EX x. x = t & P x) = P t" by simp})) ctxt)) context)))) 1) ctxt 1
   1.158 +                THEN tac ctxt cont
   1.159 +              else
   1.160 +                Subgoal.FOCUS (fn {prems, context, ...} =>
   1.161 +                  CONVERSION
   1.162 +                    (right_hand_set_comprehension_conv (K
   1.163 +                      (conj_conv
   1.164 +                        ((eq_conv Conv.all_conv
   1.165 +                          (rewr_conv' (List.last prems))) then_conv
   1.166 +                          (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) (#distinct info))))
   1.167 +                        Conv.all_conv then_conv
   1.168 +                        (rewr_conv' @{lemma "(False & P) = False" by simp}))) context then_conv
   1.169 +                      Trueprop_conv
   1.170 +                        (eq_conv Conv.all_conv
   1.171 +                          (Collect_conv (fn (_, ctxt) =>
   1.172 +                            Conv.repeat_conv
   1.173 +                              (Conv.bottom_conv
   1.174 +                                (K (rewr_conv'
   1.175 +                                  @{lemma "(EX x. P) = P" by simp})) ctxt)) context))) 1) ctxt 1
   1.176 +                THEN rtac set_Nil_I 1)) (#case_rewrites info))
   1.177 +          end
   1.178 +    fun make_inner_eqs bound_vs Tis eqs t =
   1.179 +      (case dest_case t of
   1.180 +        SOME (x, T, i, cont) =>
   1.181 +          let
   1.182 +            val (vs, body) = strip_abs (Pattern.eta_long (map snd bound_vs) cont)
   1.183 +            val x' = incr_boundvars (length vs) x
   1.184 +            val eqs' = map (incr_boundvars (length vs)) eqs
   1.185 +            val (constr_name, _) = nth (the (Datatype.get_constrs thy (fst (dest_Type T)))) i
   1.186 +            val constr_t =
   1.187 +              list_comb
   1.188 +                (Const (constr_name, map snd vs ---> T), map Bound (((length vs) - 1) downto 0))
   1.189 +            val constr_eq = Const (@{const_name HOL.eq}, T --> T --> @{typ bool}) $ constr_t $ x'
   1.190 +          in
   1.191 +            make_inner_eqs (rev vs @ bound_vs) (Case (T, i) :: Tis) (constr_eq :: eqs') body
   1.192 +          end
   1.193 +      | NONE =>
   1.194 +          (case dest_if t of
   1.195 +            SOME (condition, cont) => make_inner_eqs bound_vs (If :: Tis) (condition :: eqs) cont
   1.196 +          | NONE =>
   1.197 +            if eqs = [] then NONE (* no rewriting, nothing to be done *)
   1.198 +            else
   1.199 +              let
   1.200 +                val Type (@{type_name List.list}, [rT]) = fastype_of1 (map snd bound_vs, t)
   1.201 +                val pat_eq =
   1.202 +                  (case try dest_singleton_list t of
   1.203 +                    SOME t' =>
   1.204 +                      Const (@{const_name HOL.eq}, rT --> rT --> @{typ bool}) $
   1.205 +                        Bound (length bound_vs) $ t'
   1.206 +                  | NONE =>
   1.207 +                      Const (@{const_name Set.member}, rT --> HOLogic.mk_setT rT --> @{typ bool}) $
   1.208 +                        Bound (length bound_vs) $ (mk_set rT $ t))
   1.209 +                val reverse_bounds = curry subst_bounds
   1.210 +                  ((map Bound ((length bound_vs - 1) downto 0)) @ [Bound (length bound_vs)])
   1.211 +                val eqs' = map reverse_bounds eqs
   1.212 +                val pat_eq' = reverse_bounds pat_eq
   1.213 +                val inner_t =
   1.214 +                  fold (fn (_, T) => fn t => HOLogic.exists_const T $ absdummy T t)
   1.215 +                    (rev bound_vs) (fold (curry HOLogic.mk_conj) eqs' pat_eq')
   1.216 +                val lhs = term_of redex
   1.217 +                val rhs = HOLogic.mk_Collect ("x", rT, inner_t)
   1.218 +                val rewrite_rule_t = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   1.219 +              in
   1.220 +                SOME
   1.221 +                  ((Goal.prove ctxt [] [] rewrite_rule_t
   1.222 +                    (fn {context, ...} => tac context (rev Tis))) RS @{thm eq_reflection})
   1.223 +              end))
   1.224 +  in
   1.225 +    make_inner_eqs [] [] [] (dest_set (term_of redex))
   1.226 +  end
   1.227 +
   1.228 +end
   1.229 +*}
   1.230  
   1.231  simproc_setup list_to_set_comprehension ("set xs") = {* K List_to_Set_Comprehension.simproc *}
   1.232  
   1.233 @@ -5664,7 +5885,57 @@
   1.234  
   1.235  subsubsection {* Pretty lists *}
   1.236  
   1.237 -ML_file "Tools/list_code.ML"
   1.238 +ML {*
   1.239 +(* Code generation for list literals. *)
   1.240 +
   1.241 +signature LIST_CODE =
   1.242 +sig
   1.243 +  val implode_list: string -> string -> Code_Thingol.iterm -> Code_Thingol.iterm list option
   1.244 +  val default_list: int * string
   1.245 +    -> (Code_Printer.fixity -> Code_Thingol.iterm -> Pretty.T)
   1.246 +    -> Code_Printer.fixity -> Code_Thingol.iterm -> Code_Thingol.iterm -> Pretty.T
   1.247 +  val add_literal_list: string -> theory -> theory
   1.248 +end;
   1.249 +
   1.250 +structure List_Code : LIST_CODE =
   1.251 +struct
   1.252 +
   1.253 +open Basic_Code_Thingol;
   1.254 +
   1.255 +fun implode_list nil' cons' t =
   1.256 +  let
   1.257 +    fun dest_cons (IConst { name = c, ... } `$ t1 `$ t2) =
   1.258 +          if c = cons'
   1.259 +          then SOME (t1, t2)
   1.260 +          else NONE
   1.261 +      | dest_cons _ = NONE;
   1.262 +    val (ts, t') = Code_Thingol.unfoldr dest_cons t;
   1.263 +  in case t'
   1.264 +   of IConst { name = c, ... } => if c = nil' then SOME ts else NONE
   1.265 +    | _ => NONE
   1.266 +  end;
   1.267 +
   1.268 +fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
   1.269 +  Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy (
   1.270 +    pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
   1.271 +    Code_Printer.str target_cons,
   1.272 +    pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
   1.273 +  );
   1.274 +
   1.275 +fun add_literal_list target =
   1.276 +  let
   1.277 +    fun pretty literals [nil', cons'] pr thm vars fxy [(t1, _), (t2, _)] =
   1.278 +      case Option.map (cons t1) (implode_list nil' cons' t2)
   1.279 +       of SOME ts =>
   1.280 +            Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
   1.281 +        | NONE =>
   1.282 +            default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
   1.283 +  in Code_Target.add_const_syntax target @{const_name Cons}
   1.284 +    (SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))
   1.285 +  end
   1.286 +
   1.287 +end;
   1.288 +*}
   1.289  
   1.290  code_type list
   1.291    (SML "_ list")