# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1430409643 -3600
# Node ID 670cddd9756327c8418566e24ada0c6100ce16dc
# Parent  1d218c3e84e2d894972cc57fa47d8221d36c8e2c# Parent  52aa014308cb1d3176d3b4961677976d65657282
Merge

diff -r 1d218c3e84e2 -r 670cddd97563 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Apr 30 15:33:59 2015 +0100
+++ b/src/HOL/List.thy	Thu Apr 30 17:00:43 2015 +0100
@@ -486,35 +486,38 @@
 
 ML_val {*
   let
-    val read = Syntax.read_term @{context};
-    fun check s1 s2 = read s1 aconv read s2 orelse error ("Check failed: " ^ quote s1);
+    val read = Syntax.read_term @{context} o Syntax.implode_input;
+    fun check s1 s2 =
+      read s1 aconv read s2 orelse
+        error ("Check failed: " ^
+          quote (Input.source_content s1) ^ Position.here_list [Input.pos_of s1, Input.pos_of s2]);
   in
-    check "[(x,y,z). b]" "if b then [(x, y, z)] else []";
-    check "[(x,y,z). x\<leftarrow>xs]" "map (\<lambda>x. (x, y, z)) xs";
-    check "[e x y. x\<leftarrow>xs, y\<leftarrow>ys]" "concat (map (\<lambda>x. map (\<lambda>y. e x y) ys) xs)";
-    check "[(x,y,z). x<a, x>b]" "if x < a then if b < x then [(x, y, z)] else [] else []";
-    check "[(x,y,z). x\<leftarrow>xs, x>b]" "concat (map (\<lambda>x. if b < x then [(x, y, z)] else []) xs)";
-    check "[(x,y,z). x<a, x\<leftarrow>xs]" "if x < a then map (\<lambda>x. (x, y, z)) xs else []";
-    check "[(x,y). Cons True x \<leftarrow> xs]"
-      "concat (map (\<lambda>xa. case xa of [] \<Rightarrow> [] | True # x \<Rightarrow> [(x, y)] | False # x \<Rightarrow> []) xs)";
-    check "[(x,y,z). Cons x [] \<leftarrow> xs]"
-      "concat (map (\<lambda>xa. case xa of [] \<Rightarrow> [] | [x] \<Rightarrow> [(x, y, z)] | x # aa # lista \<Rightarrow> []) xs)";
-    check "[(x,y,z). x<a, x>b, x=d]"
-      "if x < a then if b < x then if x = d then [(x, y, z)] else [] else [] else []";
-    check "[(x,y,z). x<a, x>b, y\<leftarrow>ys]"
-      "if x < a then if b < x then map (\<lambda>y. (x, y, z)) ys else [] else []";
-    check "[(x,y,z). x<a, x\<leftarrow>xs,y>b]"
-      "if x < a then concat (map (\<lambda>x. if b < y then [(x, y, z)] else []) xs) else []";
-    check "[(x,y,z). x<a, x\<leftarrow>xs, y\<leftarrow>ys]"
-      "if x < a then concat (map (\<lambda>x. map (\<lambda>y. (x, y, z)) ys) xs) else []";
-    check "[(x,y,z). x\<leftarrow>xs, x>b, y<a]"
-      "concat (map (\<lambda>x. if b < x then if y < a then [(x, y, z)] else [] else []) xs)";
-    check "[(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys]"
-      "concat (map (\<lambda>x. if b < x then map (\<lambda>y. (x, y, z)) ys else []) xs)";
-    check "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x]"
-      "concat (map (\<lambda>x. concat (map (\<lambda>y. if x < y then [(x, y, z)] else []) ys)) xs)";
-    check "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs]"
-      "concat (map (\<lambda>x. concat (map (\<lambda>y. map (\<lambda>z. (x, y, z)) zs) ys)) xs)"
+    check \<open>[(x,y,z). b]\<close> \<open>if b then [(x, y, z)] else []\<close>;
+    check \<open>[(x,y,z). x\<leftarrow>xs]\<close> \<open>map (\<lambda>x. (x, y, z)) xs\<close>;
+    check \<open>[e x y. x\<leftarrow>xs, y\<leftarrow>ys]\<close> \<open>concat (map (\<lambda>x. map (\<lambda>y. e x y) ys) xs)\<close>;
+    check \<open>[(x,y,z). x<a, x>b]\<close> \<open>if x < a then if b < x then [(x, y, z)] else [] else []\<close>;
+    check \<open>[(x,y,z). x\<leftarrow>xs, x>b]\<close> \<open>concat (map (\<lambda>x. if b < x then [(x, y, z)] else []) xs)\<close>;
+    check \<open>[(x,y,z). x<a, x\<leftarrow>xs]\<close> \<open>if x < a then map (\<lambda>x. (x, y, z)) xs else []\<close>;
+    check \<open>[(x,y). Cons True x \<leftarrow> xs]\<close>
+      \<open>concat (map (\<lambda>xa. case xa of [] \<Rightarrow> [] | True # x \<Rightarrow> [(x, y)] | False # x \<Rightarrow> []) xs)\<close>;
+    check \<open>[(x,y,z). Cons x [] \<leftarrow> xs]\<close>
+      \<open>concat (map (\<lambda>xa. case xa of [] \<Rightarrow> [] | [x] \<Rightarrow> [(x, y, z)] | x # aa # lista \<Rightarrow> []) xs)\<close>;
+    check \<open>[(x,y,z). x<a, x>b, x=d]\<close>
+      \<open>if x < a then if b < x then if x = d then [(x, y, z)] else [] else [] else []\<close>;
+    check \<open>[(x,y,z). x<a, x>b, y\<leftarrow>ys]\<close>
+      \<open>if x < a then if b < x then map (\<lambda>y. (x, y, z)) ys else [] else []\<close>;
+    check \<open>[(x,y,z). x<a, x\<leftarrow>xs,y>b]\<close>
+      \<open>if x < a then concat (map (\<lambda>x. if b < y then [(x, y, z)] else []) xs) else []\<close>;
+    check \<open>[(x,y,z). x<a, x\<leftarrow>xs, y\<leftarrow>ys]\<close>
+      \<open>if x < a then concat (map (\<lambda>x. map (\<lambda>y. (x, y, z)) ys) xs) else []\<close>;
+    check \<open>[(x,y,z). x\<leftarrow>xs, x>b, y<a]\<close>
+      \<open>concat (map (\<lambda>x. if b < x then if y < a then [(x, y, z)] else [] else []) xs)\<close>;
+    check \<open>[(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys]\<close>
+      \<open>concat (map (\<lambda>x. if b < x then map (\<lambda>y. (x, y, z)) ys else []) xs)\<close>;
+    check \<open>[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x]\<close>
+      \<open>concat (map (\<lambda>x. concat (map (\<lambda>y. if x < y then [(x, y, z)] else []) ys)) xs)\<close>;
+    check \<open>[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs]\<close>
+      \<open>concat (map (\<lambda>x. concat (map (\<lambda>y. map (\<lambda>z. (x, y, z)) zs) ys)) xs)\<close>
   end;
 *}
 
@@ -569,116 +572,128 @@
 
 datatype termlets = If | Case of typ * int
 
-fun simproc ctxt redex =
+local
+
+val set_Nil_I = @{lemma "set [] = {x. False}" by (simp add: empty_def [symmetric])}
+val set_singleton = @{lemma "set [a] = {x. x = a}" by simp}
+val inst_Collect_mem_eq = @{lemma "set A = {x. x \<in> set A}" by simp}
+val del_refl_eq = @{lemma "(t = t \<and> P) \<equiv> P" by simp}
+
+fun mk_set T = Const (@{const_name set}, HOLogic.listT T --> HOLogic.mk_setT T)
+fun dest_set (Const (@{const_name set}, _) $ xs) = xs
+
+fun dest_singleton_list (Const (@{const_name Cons}, _) $ t $ (Const (@{const_name Nil}, _))) = t
+  | dest_singleton_list t = raise TERM ("dest_singleton_list", [t])
+
+(*We check that one case returns a singleton list and all other cases
+  return [], and return the index of the one singleton list case.*)
+fun possible_index_of_singleton_case cases =
   let
-    val set_Nil_I = @{lemma "set [] = {x. False}" by (simp add: empty_def [symmetric])}
-    val set_singleton = @{lemma "set [a] = {x. x = a}" by simp}
-    val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp}
-    val del_refl_eq = @{lemma "(t = t \<and> P) \<equiv> P" by simp}
-    fun mk_set T = Const (@{const_name set}, HOLogic.listT T --> HOLogic.mk_setT T)
-    fun dest_set (Const (@{const_name set}, _) $ xs) = xs
-    fun dest_singleton_list (Const (@{const_name Cons}, _) $ t $ (Const (@{const_name Nil}, _))) = t
-      | dest_singleton_list t = raise TERM ("dest_singleton_list", [t])
-    (* We check that one case returns a singleton list and all other cases
-       return [], and return the index of the one singleton list case *)
-    fun possible_index_of_singleton_case cases =
-      let
-        fun check (i, case_t) s =
-          (case strip_abs_body case_t of
-            (Const (@{const_name Nil}, _)) => s
-          | _ => (case s of SOME NONE => SOME (SOME i) | _ => NONE))
-      in
-        fold_index check cases (SOME NONE) |> the_default NONE
-      end
-    (* returns (case_expr type index chosen_case constr_name) option  *)
-    fun dest_case case_term =
-      let
-        val (case_const, args) = strip_comb case_term
-      in
-        (case try dest_Const case_const of
-          SOME (c, T) =>
-            (case Ctr_Sugar.ctr_sugar_of_case ctxt c of
-              SOME {ctrs, ...} =>
-                (case possible_index_of_singleton_case (fst (split_last args)) of
-                  SOME i =>
-                    let
-                      val constr_names = map (fst o dest_Const) ctrs
-                      val (Ts, _) = strip_type T
-                      val T' = List.last Ts
-                    in SOME (List.last args, T', i, nth args i, nth constr_names i) end
-                | NONE => NONE)
+    fun check (i, case_t) s =
+      (case strip_abs_body case_t of
+        (Const (@{const_name Nil}, _)) => s
+      | _ => (case s of SOME NONE => SOME (SOME i) | _ => NONE))
+  in
+    fold_index check cases (SOME NONE) |> the_default NONE
+  end
+
+(*returns condition continuing term option*)
+fun dest_if (Const (@{const_name If}, _) $ cond $ then_t $ Const (@{const_name Nil}, _)) =
+      SOME (cond, then_t)
+  | dest_if _ = NONE
+
+(*returns (case_expr type index chosen_case constr_name) option*)
+fun dest_case ctxt case_term =
+  let
+    val (case_const, args) = strip_comb case_term
+  in
+    (case try dest_Const case_const of
+      SOME (c, T) =>
+        (case Ctr_Sugar.ctr_sugar_of_case ctxt c of
+          SOME {ctrs, ...} =>
+            (case possible_index_of_singleton_case (fst (split_last args)) of
+              SOME i =>
+                let
+                  val constr_names = map (fst o dest_Const) ctrs
+                  val (Ts, _) = strip_type T
+                  val T' = List.last Ts
+                in SOME (List.last args, T', i, nth args i, nth constr_names i) end
             | NONE => NONE)
         | NONE => NONE)
-      end
-    (* returns condition continuing term option *)
-    fun dest_if (Const (@{const_name If}, _) $ cond $ then_t $ Const (@{const_name Nil}, _)) =
-          SOME (cond, then_t)
-      | dest_if _ = NONE
-    fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1
-      | tac ctxt (If :: cont) =
-          Splitter.split_tac ctxt [@{thm split_if}] 1
-          THEN rtac @{thm conjI} 1
-          THEN rtac @{thm impI} 1
-          THEN Subgoal.FOCUS (fn {prems, context, ...} =>
-            CONVERSION (right_hand_set_comprehension_conv (K
-              (HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv
-               then_conv
-               rewr_conv' @{lemma "(True \<and> P) = P" by simp})) context) 1) ctxt 1
-          THEN tac ctxt cont
+    | NONE => NONE)
+  end
+
+fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1
+  | tac ctxt (If :: cont) =
+      Splitter.split_tac ctxt @{thms split_if} 1
+      THEN rtac @{thm conjI} 1
+      THEN rtac @{thm impI} 1
+      THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} =>
+        CONVERSION (right_hand_set_comprehension_conv (K
+          (HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv
+           then_conv
+           rewr_conv' @{lemma "(True \<and> P) = P" by simp})) ctxt') 1) ctxt 1
+      THEN tac ctxt cont
+      THEN rtac @{thm impI} 1
+      THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} =>
+          CONVERSION (right_hand_set_comprehension_conv (K
+            (HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv
+             then_conv rewr_conv' @{lemma "(False \<and> P) = False" by simp})) ctxt') 1) ctxt 1
+      THEN rtac set_Nil_I 1
+  | tac ctxt (Case (T, i) :: cont) =
+      let
+        val SOME {injects, distincts, case_thms, split, ...} =
+          Ctr_Sugar.ctr_sugar_of ctxt (fst (dest_Type T))
+      in
+        (* do case distinction *)
+        Splitter.split_tac ctxt [split] 1
+        THEN EVERY (map_index (fn (i', _) =>
+          (if i' < length case_thms - 1 then rtac @{thm conjI} 1 else all_tac)
+          THEN REPEAT_DETERM (rtac @{thm allI} 1)
           THEN rtac @{thm impI} 1
-          THEN Subgoal.FOCUS (fn {prems, context, ...} =>
-              CONVERSION (right_hand_set_comprehension_conv (K
-                (HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv
-                 then_conv rewr_conv' @{lemma "(False \<and> P) = False" by simp})) context) 1) ctxt 1
-          THEN rtac set_Nil_I 1
-      | tac ctxt (Case (T, i) :: cont) =
-          let
-            val SOME {injects, distincts, case_thms, split, ...} =
-              Ctr_Sugar.ctr_sugar_of ctxt (fst (dest_Type T))
-          in
-            (* do case distinction *)
-            Splitter.split_tac ctxt [split] 1
-            THEN EVERY (map_index (fn (i', _) =>
-              (if i' < length case_thms - 1 then rtac @{thm conjI} 1 else all_tac)
-              THEN REPEAT_DETERM (rtac @{thm allI} 1)
-              THEN rtac @{thm impI} 1
-              THEN (if i' = i then
-                (* continue recursively *)
-                Subgoal.FOCUS (fn {prems, context, ...} =>
-                  CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K
-                      ((HOLogic.conj_conv
-                        (HOLogic.eq_conv Conv.all_conv (rewr_conv' (List.last prems)) then_conv
-                          (Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq injects))))
-                        Conv.all_conv)
-                        then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq))
-                        then_conv conjunct_assoc_conv)) context
-                    then_conv (HOLogic.Trueprop_conv (HOLogic.eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>
+          THEN (if i' = i then
+            (* continue recursively *)
+            Subgoal.FOCUS (fn {prems, context = ctxt', ...} =>
+              CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K
+                  ((HOLogic.conj_conv
+                    (HOLogic.eq_conv Conv.all_conv (rewr_conv' (List.last prems)) then_conv
+                      (Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq injects))))
+                    Conv.all_conv)
+                    then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq))
+                    then_conv conjunct_assoc_conv)) ctxt'
+                then_conv
+                  (HOLogic.Trueprop_conv
+                    (HOLogic.eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt'') =>
                       Conv.repeat_conv
                         (all_but_last_exists_conv
                           (K (rewr_conv'
-                            @{lemma "(\<exists>x. x = t \<and> P x) = P t" by simp})) ctxt)) context)))) 1) ctxt 1
-                THEN tac ctxt cont
-              else
-                Subgoal.FOCUS (fn {prems, context, ...} =>
-                  CONVERSION
-                    (right_hand_set_comprehension_conv (K
-                      (HOLogic.conj_conv
-                        ((HOLogic.eq_conv Conv.all_conv
-                          (rewr_conv' (List.last prems))) then_conv
-                          (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) distincts)))
-                        Conv.all_conv then_conv
-                        (rewr_conv' @{lemma "(False \<and> P) = False" by simp}))) context then_conv
-                      HOLogic.Trueprop_conv
-                        (HOLogic.eq_conv Conv.all_conv
-                          (Collect_conv (fn (_, ctxt) =>
-                            Conv.repeat_conv
-                              (Conv.bottom_conv
-                                (K (rewr_conv'
-                                  @{lemma "(\<exists>x. P) = P" by simp})) ctxt)) context))) 1) ctxt 1
-                THEN rtac set_Nil_I 1)) case_thms)
-          end
+                            @{lemma "(\<exists>x. x = t \<and> P x) = P t" by simp})) ctxt'')) ctxt')))) 1) ctxt 1
+            THEN tac ctxt cont
+          else
+            Subgoal.FOCUS (fn {prems, context = ctxt', ...} =>
+              CONVERSION
+                (right_hand_set_comprehension_conv (K
+                  (HOLogic.conj_conv
+                    ((HOLogic.eq_conv Conv.all_conv
+                      (rewr_conv' (List.last prems))) then_conv
+                      (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) distincts)))
+                    Conv.all_conv then_conv
+                    (rewr_conv' @{lemma "(False \<and> P) = False" by simp}))) ctxt' then_conv
+                  HOLogic.Trueprop_conv
+                    (HOLogic.eq_conv Conv.all_conv
+                      (Collect_conv (fn (_, ctxt'') =>
+                        Conv.repeat_conv
+                          (Conv.bottom_conv
+                            (K (rewr_conv' @{lemma "(\<exists>x. P) = P" by simp})) ctxt'')) ctxt'))) 1) ctxt 1
+            THEN rtac set_Nil_I 1)) case_thms)
+      end
+
+in
+
+fun simproc ctxt redex =
+  let
     fun make_inner_eqs bound_vs Tis eqs t =
-      (case dest_case t of
+      (case dest_case ctxt t of
         SOME (x, T, i, cont, constr_name) =>
           let
             val (vs, body) = strip_abs (Envir.eta_long (map snd bound_vs) cont)
@@ -695,7 +710,7 @@
           (case dest_if t of
             SOME (condition, cont) => make_inner_eqs bound_vs (If :: Tis) (condition :: eqs) cont
           | NONE =>
-            if eqs = [] then NONE (* no rewriting, nothing to be done *)
+            if null eqs then NONE (*no rewriting, nothing to be done*)
             else
               let
                 val Type (@{type_name list}, [rT]) = fastype_of1 (map snd bound_vs, t)
@@ -720,19 +735,21 @@
               in
                 SOME
                   ((Goal.prove ctxt [] [] rewrite_rule_t
-                    (fn {context, ...} => tac context (rev Tis))) RS @{thm eq_reflection})
+                    (fn {context = ctxt', ...} => tac ctxt' (rev Tis))) RS @{thm eq_reflection})
               end))
   in
     make_inner_eqs [] [] [] (dest_set (Thm.term_of redex))
   end
 
 end
+
+end
 *}
 
-simproc_setup list_to_set_comprehension ("set xs") = {* K List_to_Set_Comprehension.simproc *}
+simproc_setup list_to_set_comprehension ("set xs") =
+  {* K List_to_Set_Comprehension.simproc *}
 
 code_datatype set coset
-
 hide_const (open) coset