adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
authorbulwahn
Fri Jan 07 18:10:35 2011 +0100 (2011-01-07)
changeset 41463edbf0a86fb1c
parent 41462 5f4939d46b63
child 41464 cb2e3e651893
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
src/HOL/IsaMakefile
src/HOL/List.thy
src/HOL/Tools/list_to_set_comprehension.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Jan 07 17:58:51 2011 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Jan 07 18:10:35 2011 +0100
     1.3 @@ -300,6 +300,7 @@
     1.4    Tools/int_arith.ML \
     1.5    Tools/groebner.ML \
     1.6    Tools/list_code.ML \
     1.7 +  Tools/list_to_set_comprehension.ML \
     1.8    Tools/nat_numeral_simprocs.ML \
     1.9    Tools/Nitpick/kodkod.ML \
    1.10    Tools/Nitpick/kodkod_sat.ML \
     2.1 --- a/src/HOL/List.thy	Fri Jan 07 17:58:51 2011 +0100
     2.2 +++ b/src/HOL/List.thy	Fri Jan 07 18:10:35 2011 +0100
     2.3 @@ -6,7 +6,9 @@
     2.4  
     2.5  theory List
     2.6  imports Plain Presburger Recdef Code_Numeral Quotient ATP
     2.7 -uses ("Tools/list_code.ML")
     2.8 +uses
     2.9 +  ("Tools/list_code.ML")
    2.10 +  ("Tools/list_to_set_comprehension.ML")
    2.11  begin
    2.12  
    2.13  datatype 'a list =
    2.14 @@ -339,13 +341,6 @@
    2.15  mangled). In such cases it can be advisable to introduce separate
    2.16  definitions for the list comprehensions in question.  *}
    2.17  
    2.18 -(*
    2.19 -Proper theorem proving support would be nice. For example, if
    2.20 -@{text"set[f x y. x \<leftarrow> xs, y \<leftarrow> ys, P x y]"}
    2.21 -produced something like
    2.22 -@{term"{z. EX x: set xs. EX y:set ys. P x y \<and> z = f x y}"}.
    2.23 -*)
    2.24 -
    2.25  nonterminal lc_qual and lc_quals
    2.26  
    2.27  syntax
    2.28 @@ -450,6 +445,10 @@
    2.29  term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]"
    2.30  *)
    2.31  
    2.32 +use "Tools/list_to_set_comprehension.ML"
    2.33 +
    2.34 +simproc_setup list_to_set_comprehension ("set xs") = {* K List_to_Set_Comprehension.simproc *}
    2.35 +
    2.36  
    2.37  subsubsection {* @{const Nil} and @{const Cons} *}
    2.38  
    2.39 @@ -965,7 +964,7 @@
    2.40  by (induct xs) auto
    2.41  
    2.42  lemma set_upt [simp]: "set[i..<j] = {i..<j}"
    2.43 -by (induct j) (simp_all add: atLeastLessThanSuc)
    2.44 +by (induct j) auto
    2.45  
    2.46  
    2.47  lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs"
    2.48 @@ -1758,7 +1757,11 @@
    2.49  
    2.50  lemma set_take_subset_set_take:
    2.51    "m <= n \<Longrightarrow> set(take m xs) <= set(take n xs)"
    2.52 -by(induct xs arbitrary: m n)(auto simp:take_Cons split:nat.split)
    2.53 +apply (induct xs arbitrary: m n)
    2.54 +apply simp
    2.55 +apply (case_tac n)
    2.56 +apply (auto simp: take_Cons)
    2.57 +done
    2.58  
    2.59  lemma set_take_subset: "set(take n xs) \<subseteq> set xs"
    2.60  by(induct xs arbitrary: n)(auto simp:take_Cons split:nat.split)
    2.61 @@ -2690,9 +2693,11 @@
    2.62  by(simp add: upto.simps)
    2.63  
    2.64  lemma set_upto[simp]: "set[i..j] = {i..j}"
    2.65 -apply(induct i j rule:upto.induct)
    2.66 -apply(simp add: upto.simps simp_from_to)
    2.67 -done
    2.68 +proof(induct i j rule:upto.induct)
    2.69 +  case (1 i j)
    2.70 +  from this show ?case
    2.71 +    unfolding upto.simps[of i j] simp_from_to[of i j] by auto
    2.72 +qed
    2.73  
    2.74  
    2.75  subsubsection {* @{text "distinct"} and @{text remdups} *}
    2.76 @@ -3366,7 +3371,7 @@
    2.77  by(simp add:rotate_drop_take take_map drop_map)
    2.78  
    2.79  lemma set_rotate1[simp]: "set(rotate1 xs) = set xs"
    2.80 -by(simp add:rotate1_def split:list.split)
    2.81 +by (cases xs) (auto simp add:rotate1_def)
    2.82  
    2.83  lemma set_rotate[simp]: "set(rotate n xs) = set xs"
    2.84  by (induct n) (simp_all add:rotate_def)
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/list_to_set_comprehension.ML	Fri Jan 07 18:10:35 2011 +0100
     3.3 @@ -0,0 +1,206 @@
     3.4 +(*  Title:  HOL/Tools/list_to_set_comprehension.ML
     3.5 +    Author: Lukas Bulwahn, TU Muenchen
     3.6 +
     3.7 +  Simproc for rewriting list comprehensions applied to List.set to set comprehension
     3.8 +*)
     3.9 +
    3.10 +signature LIST_TO_SET_COMPREHENSION =
    3.11 +sig
    3.12 +  val simproc : simpset -> cterm -> thm option
    3.13 +end;
    3.14 +
    3.15 +structure List_to_Set_Comprehension : LIST_TO_SET_COMPREHENSION =
    3.16 +struct
    3.17 +
    3.18 +fun CONVERSION' cv i st = Seq.single (Conv.gconv_rule cv i st)
    3.19 +
    3.20 +(* conversion *)
    3.21 +
    3.22 +fun trace_conv cv ct =
    3.23 +  (tracing (Syntax.string_of_term_global @{theory} (Thm.term_of ct)); cv ct)
    3.24 +
    3.25 +fun all_exists_conv cv ctxt ct =
    3.26 +  case Thm.term_of ct of
    3.27 +    Const(@{const_name HOL.Ex}, _) $ Abs(_, _, _) =>
    3.28 +      Conv.arg_conv (Conv.abs_conv (all_exists_conv cv o #2) ctxt) ct
    3.29 +  | _ => cv ctxt ct
    3.30 +
    3.31 +fun all_but_last_exists_conv cv ctxt ct =
    3.32 +  case Thm.term_of ct of
    3.33 +    Const (@{const_name HOL.Ex}, _) $ Abs (_, _, Const (@{const_name HOL.Ex}, _) $ _) =>
    3.34 +      Conv.arg_conv (Conv.abs_conv (all_but_last_exists_conv cv o #2) ctxt) ct
    3.35 +  | _ => cv ctxt ct
    3.36 +
    3.37 +fun Collect_conv cv ctxt ct =
    3.38 +  (case Thm.term_of ct of
    3.39 +    Const (@{const_name Set.Collect}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv cv ctxt) ct
    3.40 +  | _ => raise CTERM ("Collect_conv", [ct]));
    3.41 +
    3.42 +fun Trueprop_conv cv ct =
    3.43 +  (case Thm.term_of ct of
    3.44 +    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
    3.45 +  | _ => raise CTERM ("Trueprop_conv", [ct]));
    3.46 +
    3.47 +fun eq_conv cv1 cv2 ct =
    3.48 +  (case Thm.term_of ct of
    3.49 +    Const (@{const_name HOL.eq}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
    3.50 +  | _ => raise CTERM ("eq_conv", [ct]));
    3.51 +
    3.52 +fun conj_conv cv1 cv2 ct =
    3.53 +  (case Thm.term_of ct of
    3.54 +    Const (@{const_name HOL.conj}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
    3.55 +  | _ => raise CTERM ("conj_conv", [ct]));
    3.56 +
    3.57 +fun right_hand_set_comprehension_conv conv ctxt = Trueprop_conv (eq_conv Conv.all_conv
    3.58 +  (Collect_conv (all_exists_conv conv o #2) ctxt))
    3.59 +
    3.60 +(* term abstraction of list comprehension patterns *)
    3.61 + 
    3.62 +datatype termlets = If | Case of (typ * int)
    3.63 +
    3.64 +val last = snd o split_last
    3.65 +
    3.66 +fun meta_eq th = th RS @{thm eq_reflection}
    3.67 +
    3.68 +fun rewr_conv' th = Conv.rewr_conv (meta_eq th)
    3.69 +
    3.70 +fun simproc ss redex =
    3.71 +  let
    3.72 +    val ctxt = Simplifier.the_context ss
    3.73 +    val thy = ProofContext.theory_of ctxt 
    3.74 +    val set_Nil_I = @{thm trans} OF [@{thm set.simps(1)}, @{thm empty_def}]
    3.75 +    val set_singleton = @{lemma "set [a] = {x. x = a}" by simp}
    3.76 +    val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp}
    3.77 +    val del_refl_eq = @{lemma "(t = t & P) == P" by simp} 
    3.78 +    fun mk_set T = Const (@{const_name List.set}, HOLogic.listT T --> HOLogic.mk_setT T)
    3.79 +    fun dest_set (Const (@{const_name List.set}, _) $ xs) = xs
    3.80 +    fun dest_singleton_list (Const (@{const_name List.Cons}, _)
    3.81 +      $ t $ (Const (@{const_name List.Nil}, _))) = t
    3.82 +      | dest_singleton_list t = raise TERM ("dest_singleton_list", [t])
    3.83 +    (* We check that one case returns a singleton list and all other cases
    3.84 +       return [], and return the index of the one singleton list case *) 
    3.85 +    fun possible_index_of_singleton_case cases =
    3.86 +      let  
    3.87 +        fun check (i, case_t) s =
    3.88 +          (case strip_abs_body case_t of
    3.89 +            (Const (@{const_name List.Nil}, _)) => s
    3.90 +          | t => (case s of NONE => SOME i | SOME s => NONE))
    3.91 +      in
    3.92 +        fold_index check cases NONE
    3.93 +      end
    3.94 +    (* returns (case_expr type index chosen_case) option  *)
    3.95 +    fun dest_case case_term =
    3.96 +      let
    3.97 +        val (case_const, args) = strip_comb case_term
    3.98 +      in
    3.99 +        case try dest_Const case_const of
   3.100 +          SOME (c, T) => (case Datatype_Data.info_of_case thy c of
   3.101 +            SOME _ => (case possible_index_of_singleton_case (fst (split_last args)) of
   3.102 +              SOME i => 
   3.103 +                let
   3.104 +                  val (Ts, _) = strip_type T
   3.105 +                  val T' = last Ts
   3.106 +                in SOME (snd (split_last args), T', i, nth args i) end
   3.107 +            | NONE => NONE)
   3.108 +          | NONE => NONE)
   3.109 +        | NONE => NONE
   3.110 +      end
   3.111 +    (* returns condition continuing term option *)
   3.112 +    fun dest_if (Const (@{const_name If}, _) $ cond $ then_t $ Const (@{const_name Nil}, _)) =
   3.113 +        SOME (cond, then_t)
   3.114 +      | dest_if _ = NONE
   3.115 +    fun tac _ [] =
   3.116 +      rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1
   3.117 +    | tac ctxt (If :: cont) =
   3.118 +      Splitter.split_tac [@{thm split_if}] 1
   3.119 +      THEN rtac @{thm conjI} 1
   3.120 +      THEN rtac @{thm impI} 1
   3.121 +      THEN Subgoal.FOCUS (fn {prems, context, ...} =>
   3.122 +        CONVERSION (right_hand_set_comprehension_conv (K
   3.123 +          (conj_conv (Conv.rewr_conv (snd (split_last prems) RS @{thm Eq_TrueI})) Conv.all_conv
   3.124 +           then_conv rewr_conv' @{thm simp_thms(22)})) context) 1) ctxt 1
   3.125 +      THEN tac ctxt cont
   3.126 +      THEN rtac @{thm impI} 1
   3.127 +      THEN Subgoal.FOCUS (fn {prems, context, ...} =>
   3.128 +          CONVERSION (right_hand_set_comprehension_conv (K
   3.129 +            (conj_conv (Conv.rewr_conv (snd (split_last prems) RS @{thm Eq_FalseI})) Conv.all_conv
   3.130 +             then_conv rewr_conv' @{thm simp_thms(24)})) context) 1) ctxt 1
   3.131 +      THEN rtac set_Nil_I 1
   3.132 +    | tac ctxt (Case (T, i) :: cont) =
   3.133 +      let
   3.134 +        val info = Datatype.the_info thy (fst (dest_Type T))
   3.135 +      in
   3.136 +        (* do case distinction *)
   3.137 +        Splitter.split_tac [#split info] 1
   3.138 +        THEN EVERY (map_index (fn (i', case_rewrite) =>
   3.139 +          (if i' < length (#case_rewrites info) - 1 then rtac @{thm conjI} 1 else all_tac)
   3.140 +          THEN REPEAT_DETERM (rtac @{thm allI} 1)
   3.141 +          THEN rtac @{thm impI} 1
   3.142 +          THEN (if i' = i then
   3.143 +            (* continue recursively *)
   3.144 +            Subgoal.FOCUS (fn {prems, context, ...} =>
   3.145 +              CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K
   3.146 +                  ((conj_conv 
   3.147 +                    (eq_conv Conv.all_conv (rewr_conv' (snd (split_last prems)))
   3.148 +                    then_conv (Conv.try_conv (Conv.rewrs_conv (map meta_eq (#inject info))))) Conv.all_conv)
   3.149 +                    then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq))
   3.150 +                    then_conv (Conv.try_conv (rewr_conv' @{thm conj_assoc})))) context
   3.151 +                then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>
   3.152 +                  Conv.repeat_conv (all_but_last_exists_conv (K (rewr_conv' @{thm simp_thms(39)})) ctxt)) context)))) 1) ctxt 1
   3.153 +            THEN tac ctxt cont
   3.154 +          else
   3.155 +            Subgoal.FOCUS (fn {prems, context, ...} =>
   3.156 +              CONVERSION ((right_hand_set_comprehension_conv (K
   3.157 +                (conj_conv
   3.158 +                  ((eq_conv Conv.all_conv
   3.159 +                    (rewr_conv' (snd (split_last prems))))
   3.160 +                     then_conv (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) (#distinct info)))) Conv.all_conv
   3.161 +                  then_conv (rewr_conv' @{thm simp_thms(24)}))) context)
   3.162 +               then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>
   3.163 +                   Conv.repeat_conv (Conv.bottom_conv (K (rewr_conv' @{thm simp_thms(36)})) ctxt)) context)))) 1) ctxt 1
   3.164 +            THEN rtac set_Nil_I 1)) (#case_rewrites info))
   3.165 +      end
   3.166 +    fun make_inner_eqs bound_vs Tis eqs t =
   3.167 +      case dest_case t of
   3.168 +        SOME (x, T, i, cont) =>
   3.169 +          let
   3.170 +            val (vs, body) = strip_abs (Pattern.eta_long (map snd bound_vs) cont)
   3.171 +            val x' = incr_boundvars (length vs) x
   3.172 +            val eqs' = map (incr_boundvars (length vs)) eqs
   3.173 +            val (constr_name, _) = nth (the (Datatype_Data.get_constrs thy (fst (dest_Type T)))) i
   3.174 +            val constr_t = list_comb (Const (constr_name, map snd vs ---> T), map Bound (((length vs) - 1) downto 0))
   3.175 +            val constr_eq = Const (@{const_name HOL.eq}, T --> T --> @{typ bool}) $ constr_t $ x'
   3.176 +          in
   3.177 +            make_inner_eqs (rev vs @ bound_vs) (Case (T, i) :: Tis) (constr_eq :: eqs') body
   3.178 +          end
   3.179 +      | NONE =>
   3.180 +        case dest_if t of
   3.181 +          SOME (condition, cont) => make_inner_eqs bound_vs (If :: Tis) (condition :: eqs) cont
   3.182 +        | NONE =>
   3.183 +          if eqs = [] then NONE (* no rewriting, nothing to be done *)
   3.184 +          else
   3.185 +            let
   3.186 +              val Type ("List.list", [rT]) = fastype_of t
   3.187 +              val pat_eq =
   3.188 +                case try dest_singleton_list t of
   3.189 +                  SOME t' => Const (@{const_name HOL.eq}, rT --> rT --> @{typ bool})
   3.190 +                    $ Bound (length bound_vs) $ t'
   3.191 +                | NONE => Const ("Set.member", rT --> HOLogic.mk_setT rT --> @{typ bool})
   3.192 +                  $ Bound (length bound_vs) $ (mk_set rT $ t)
   3.193 +              val reverse_bounds = curry subst_bounds
   3.194 +                ((map Bound ((length bound_vs - 1) downto 0)) @ [Bound (length bound_vs)])
   3.195 +              val eqs' = map reverse_bounds eqs
   3.196 +              val pat_eq' = reverse_bounds pat_eq
   3.197 +              val inner_t = fold (fn (v, T) => fn t => HOLogic.exists_const T $ absdummy (T, t))
   3.198 +                (rev bound_vs) (fold (curry HOLogic.mk_conj) eqs' pat_eq')
   3.199 +              val lhs = term_of redex
   3.200 +              val rhs = HOLogic.mk_Collect ("x", rT, inner_t)
   3.201 +              val rewrite_rule_t = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   3.202 +            in
   3.203 +              SOME ((Goal.prove ctxt [] [] rewrite_rule_t (fn {context, ...} => tac context (rev Tis))) RS @{thm eq_reflection})
   3.204 +            end
   3.205 +  in
   3.206 +    make_inner_eqs [] [] [] (dest_set (term_of redex))
   3.207 +  end
   3.208 +
   3.209 +end