src/HOL/Tools/Datatype/datatype_case.ML
changeset 31775 2b04504fcb69
parent 31737 b3f63611784e
child 32035 8e77b6a250d5
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_case.ML	Tue Jun 23 12:09:30 2009 +0200
     1.3 @@ -0,0 +1,469 @@
     1.4 +(*  Title:      HOL/Tools/datatype_case.ML
     1.5 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
     1.6 +    Author:     Stefan Berghofer, TU Muenchen
     1.7 +
     1.8 +Nested case expressions on datatypes.
     1.9 +*)
    1.10 +
    1.11 +signature DATATYPE_CASE =
    1.12 +sig
    1.13 +  val make_case: (string -> DatatypeAux.info option) ->
    1.14 +    Proof.context -> bool -> string list -> term -> (term * term) list ->
    1.15 +    term * (term * (int * bool)) list
    1.16 +  val dest_case: (string -> DatatypeAux.info option) -> bool ->
    1.17 +    string list -> term -> (term * (term * term) list) option
    1.18 +  val strip_case: (string -> DatatypeAux.info option) -> bool ->
    1.19 +    term -> (term * (term * term) list) option
    1.20 +  val case_tr: bool -> (theory -> string -> DatatypeAux.info option)
    1.21 +    -> Proof.context -> term list -> term
    1.22 +  val case_tr': (theory -> string -> DatatypeAux.info option) ->
    1.23 +    string -> Proof.context -> term list -> term
    1.24 +end;
    1.25 +
    1.26 +structure DatatypeCase : DATATYPE_CASE =
    1.27 +struct
    1.28 +
    1.29 +exception CASE_ERROR of string * int;
    1.30 +
    1.31 +fun match_type thy pat ob = Sign.typ_match thy (pat, ob) Vartab.empty;
    1.32 +
    1.33 +(*---------------------------------------------------------------------------
    1.34 + * Get information about datatypes
    1.35 + *---------------------------------------------------------------------------*)
    1.36 +
    1.37 +fun ty_info (tab : string -> DatatypeAux.info option) s =
    1.38 +  case tab s of
    1.39 +    SOME {descr, case_name, index, sorts, ...} =>
    1.40 +      let
    1.41 +        val (_, (tname, dts, constrs)) = nth descr index;
    1.42 +        val mk_ty = DatatypeAux.typ_of_dtyp descr sorts;
    1.43 +        val T = Type (tname, map mk_ty dts)
    1.44 +      in
    1.45 +        SOME {case_name = case_name,
    1.46 +          constructors = map (fn (cname, dts') =>
    1.47 +            Const (cname, Logic.varifyT (map mk_ty dts' ---> T))) constrs}
    1.48 +      end
    1.49 +  | NONE => NONE;
    1.50 +
    1.51 +
    1.52 +(*---------------------------------------------------------------------------
    1.53 + * Each pattern carries with it a tag (i,b) where
    1.54 + * i is the clause it came from and
    1.55 + * b=true indicates that clause was given by the user
    1.56 + * (or is an instantiation of a user supplied pattern)
    1.57 + * b=false --> i = ~1
    1.58 + *---------------------------------------------------------------------------*)
    1.59 +
    1.60 +fun pattern_subst theta (tm, x) = (subst_free theta tm, x);
    1.61 +
    1.62 +fun row_of_pat x = fst (snd x);
    1.63 +
    1.64 +fun add_row_used ((prfx, pats), (tm, tag)) =
    1.65 +  fold Term.add_free_names (tm :: pats @ prfx);
    1.66 +
    1.67 +(* try to preserve names given by user *)
    1.68 +fun default_names names ts =
    1.69 +  map (fn ("", Free (name', _)) => name' | (name, _) => name) (names ~~ ts);
    1.70 +
    1.71 +fun strip_constraints (Const ("_constrain", _) $ t $ tT) =
    1.72 +      strip_constraints t ||> cons tT
    1.73 +  | strip_constraints t = (t, []);
    1.74 +
    1.75 +fun mk_fun_constrain tT t = Syntax.const "_constrain" $ t $
    1.76 +  (Syntax.free "fun" $ tT $ Syntax.free "dummy");
    1.77 +
    1.78 +
    1.79 +(*---------------------------------------------------------------------------
    1.80 + * Produce an instance of a constructor, plus genvars for its arguments.
    1.81 + *---------------------------------------------------------------------------*)
    1.82 +fun fresh_constr ty_match ty_inst colty used c =
    1.83 +  let
    1.84 +    val (_, Ty) = dest_Const c
    1.85 +    val Ts = binder_types Ty;
    1.86 +    val names = Name.variant_list used
    1.87 +      (DatatypeProp.make_tnames (map Logic.unvarifyT Ts));
    1.88 +    val ty = body_type Ty;
    1.89 +    val ty_theta = ty_match ty colty handle Type.TYPE_MATCH =>
    1.90 +      raise CASE_ERROR ("type mismatch", ~1)
    1.91 +    val c' = ty_inst ty_theta c
    1.92 +    val gvars = map (ty_inst ty_theta o Free) (names ~~ Ts)
    1.93 +  in (c', gvars)
    1.94 +  end;
    1.95 +
    1.96 +
    1.97 +(*---------------------------------------------------------------------------
    1.98 + * Goes through a list of rows and picks out the ones beginning with a
    1.99 + * pattern with constructor = name.
   1.100 + *---------------------------------------------------------------------------*)
   1.101 +fun mk_group (name, T) rows =
   1.102 +  let val k = length (binder_types T)
   1.103 +  in fold (fn (row as ((prfx, p :: rst), rhs as (_, (i, _)))) =>
   1.104 +    fn ((in_group, not_in_group), (names, cnstrts)) => (case strip_comb p of
   1.105 +        (Const (name', _), args) =>
   1.106 +          if name = name' then
   1.107 +            if length args = k then
   1.108 +              let val (args', cnstrts') = split_list (map strip_constraints args)
   1.109 +              in
   1.110 +                ((((prfx, args' @ rst), rhs) :: in_group, not_in_group),
   1.111 +                 (default_names names args', map2 append cnstrts cnstrts'))
   1.112 +              end
   1.113 +            else raise CASE_ERROR
   1.114 +              ("Wrong number of arguments for constructor " ^ name, i)
   1.115 +          else ((in_group, row :: not_in_group), (names, cnstrts))
   1.116 +      | _ => raise CASE_ERROR ("Not a constructor pattern", i)))
   1.117 +    rows (([], []), (replicate k "", replicate k [])) |>> pairself rev
   1.118 +  end;
   1.119 +
   1.120 +(*---------------------------------------------------------------------------
   1.121 + * Partition the rows. Not efficient: we should use hashing.
   1.122 + *---------------------------------------------------------------------------*)
   1.123 +fun partition _ _ _ _ _ _ _ [] = raise CASE_ERROR ("partition: no rows", ~1)
   1.124 +  | partition ty_match ty_inst type_of used constructors colty res_ty
   1.125 +        (rows as (((prfx, _ :: rstp), _) :: _)) =
   1.126 +      let
   1.127 +        fun part {constrs = [], rows = [], A} = rev A
   1.128 +          | part {constrs = [], rows = (_, (_, (i, _))) :: _, A} =
   1.129 +              raise CASE_ERROR ("Not a constructor pattern", i)
   1.130 +          | part {constrs = c :: crst, rows, A} =
   1.131 +              let
   1.132 +                val ((in_group, not_in_group), (names, cnstrts)) =
   1.133 +                  mk_group (dest_Const c) rows;
   1.134 +                val used' = fold add_row_used in_group used;
   1.135 +                val (c', gvars) = fresh_constr ty_match ty_inst colty used' c;
   1.136 +                val in_group' =
   1.137 +                  if null in_group  (* Constructor not given *)
   1.138 +                  then
   1.139 +                    let
   1.140 +                      val Ts = map type_of rstp;
   1.141 +                      val xs = Name.variant_list
   1.142 +                        (fold Term.add_free_names gvars used')
   1.143 +                        (replicate (length rstp) "x")
   1.144 +                    in
   1.145 +                      [((prfx, gvars @ map Free (xs ~~ Ts)),
   1.146 +                        (Const ("HOL.undefined", res_ty), (~1, false)))]
   1.147 +                    end
   1.148 +                  else in_group
   1.149 +              in
   1.150 +                part{constrs = crst,
   1.151 +                  rows = not_in_group,
   1.152 +                  A = {constructor = c',
   1.153 +                    new_formals = gvars,
   1.154 +                    names = names,
   1.155 +                    constraints = cnstrts,
   1.156 +                    group = in_group'} :: A}
   1.157 +              end
   1.158 +      in part {constrs = constructors, rows = rows, A = []}
   1.159 +      end;
   1.160 +
   1.161 +(*---------------------------------------------------------------------------
   1.162 + * Misc. routines used in mk_case
   1.163 + *---------------------------------------------------------------------------*)
   1.164 +
   1.165 +fun mk_pat ((c, c'), l) =
   1.166 +  let
   1.167 +    val L = length (binder_types (fastype_of c))
   1.168 +    fun build (prfx, tag, plist) =
   1.169 +      let val (args, plist') = chop L plist
   1.170 +      in (prfx, tag, list_comb (c', args) :: plist') end
   1.171 +  in map build l end;
   1.172 +
   1.173 +fun v_to_prfx (prfx, v::pats) = (v::prfx,pats)
   1.174 +  | v_to_prfx _ = raise CASE_ERROR ("mk_case: v_to_prfx", ~1);
   1.175 +
   1.176 +fun v_to_pats (v::prfx,tag, pats) = (prfx, tag, v::pats)
   1.177 +  | v_to_pats _ = raise CASE_ERROR ("mk_case: v_to_pats", ~1);
   1.178 +
   1.179 +
   1.180 +(*----------------------------------------------------------------------------
   1.181 + * Translation of pattern terms into nested case expressions.
   1.182 + *
   1.183 + * This performs the translation and also builds the full set of patterns.
   1.184 + * Thus it supports the construction of induction theorems even when an
   1.185 + * incomplete set of patterns is given.
   1.186 + *---------------------------------------------------------------------------*)
   1.187 +
   1.188 +fun mk_case tab ctxt ty_match ty_inst type_of used range_ty =
   1.189 +  let
   1.190 +    val name = Name.variant used "a";
   1.191 +    fun expand constructors used ty ((_, []), _) =
   1.192 +          raise CASE_ERROR ("mk_case: expand_var_row", ~1)
   1.193 +      | expand constructors used ty (row as ((prfx, p :: rst), rhs)) =
   1.194 +          if is_Free p then
   1.195 +            let
   1.196 +              val used' = add_row_used row used;
   1.197 +              fun expnd c =
   1.198 +                let val capp =
   1.199 +                  list_comb (fresh_constr ty_match ty_inst ty used' c)
   1.200 +                in ((prfx, capp :: rst), pattern_subst [(p, capp)] rhs)
   1.201 +                end
   1.202 +            in map expnd constructors end
   1.203 +          else [row]
   1.204 +    fun mk {rows = [], ...} = raise CASE_ERROR ("no rows", ~1)
   1.205 +      | mk {path = [], rows = ((prfx, []), (tm, tag)) :: _} =  (* Done *)
   1.206 +          ([(prfx, tag, [])], tm)
   1.207 +      | mk {path, rows as ((row as ((_, [Free _]), _)) :: _ :: _)} =
   1.208 +          mk {path = path, rows = [row]}
   1.209 +      | mk {path = u :: rstp, rows as ((_, _ :: _), _) :: _} =
   1.210 +          let val col0 = map (fn ((_, p :: _), (_, (i, _))) => (p, i)) rows
   1.211 +          in case Option.map (apfst head_of)
   1.212 +            (find_first (not o is_Free o fst) col0) of
   1.213 +              NONE =>
   1.214 +                let
   1.215 +                  val rows' = map (fn ((v, _), row) => row ||>
   1.216 +                    pattern_subst [(v, u)] |>> v_to_prfx) (col0 ~~ rows);
   1.217 +                  val (pref_patl, tm) = mk {path = rstp, rows = rows'}
   1.218 +                in (map v_to_pats pref_patl, tm) end
   1.219 +            | SOME (Const (cname, cT), i) => (case ty_info tab cname of
   1.220 +                NONE => raise CASE_ERROR ("Not a datatype constructor: " ^ cname, i)
   1.221 +              | SOME {case_name, constructors} =>
   1.222 +                let
   1.223 +                  val pty = body_type cT;
   1.224 +                  val used' = fold Term.add_free_names rstp used;
   1.225 +                  val nrows = maps (expand constructors used' pty) rows;
   1.226 +                  val subproblems = partition ty_match ty_inst type_of used'
   1.227 +                    constructors pty range_ty nrows;
   1.228 +                  val new_formals = map #new_formals subproblems
   1.229 +                  val constructors' = map #constructor subproblems
   1.230 +                  val news = map (fn {new_formals, group, ...} =>
   1.231 +                    {path = new_formals @ rstp, rows = group}) subproblems;
   1.232 +                  val (pat_rect, dtrees) = split_list (map mk news);
   1.233 +                  val case_functions = map2
   1.234 +                    (fn {new_formals, names, constraints, ...} =>
   1.235 +                       fold_rev (fn ((x as Free (_, T), s), cnstrts) => fn t =>
   1.236 +                         Abs (if s = "" then name else s, T,
   1.237 +                           abstract_over (x, t)) |>
   1.238 +                         fold mk_fun_constrain cnstrts)
   1.239 +                           (new_formals ~~ names ~~ constraints))
   1.240 +                    subproblems dtrees;
   1.241 +                  val types = map type_of (case_functions @ [u]);
   1.242 +                  val case_const = Const (case_name, types ---> range_ty)
   1.243 +                  val tree = list_comb (case_const, case_functions @ [u])
   1.244 +                  val pat_rect1 = flat (map mk_pat
   1.245 +                    (constructors ~~ constructors' ~~ pat_rect))
   1.246 +                in (pat_rect1, tree)
   1.247 +                end)
   1.248 +            | SOME (t, i) => raise CASE_ERROR ("Not a datatype constructor: " ^
   1.249 +                Syntax.string_of_term ctxt t, i)
   1.250 +          end
   1.251 +      | mk _ = raise CASE_ERROR ("Malformed row matrix", ~1)
   1.252 +  in mk
   1.253 +  end;
   1.254 +
   1.255 +fun case_error s = error ("Error in case expression:\n" ^ s);
   1.256 +
   1.257 +(* Repeated variable occurrences in a pattern are not allowed. *)
   1.258 +fun no_repeat_vars ctxt pat = fold_aterms
   1.259 +  (fn x as Free (s, _) => (fn xs =>
   1.260 +        if member op aconv xs x then
   1.261 +          case_error (quote s ^ " occurs repeatedly in the pattern " ^
   1.262 +            quote (Syntax.string_of_term ctxt pat))
   1.263 +        else x :: xs)
   1.264 +    | _ => I) pat [];
   1.265 +
   1.266 +fun gen_make_case ty_match ty_inst type_of tab ctxt err used x clauses =
   1.267 +  let
   1.268 +    fun string_of_clause (pat, rhs) = Syntax.string_of_term ctxt
   1.269 +      (Syntax.const "_case1" $ pat $ rhs);
   1.270 +    val _ = map (no_repeat_vars ctxt o fst) clauses;
   1.271 +    val rows = map_index (fn (i, (pat, rhs)) =>
   1.272 +      (([], [pat]), (rhs, (i, true)))) clauses;
   1.273 +    val rangeT = (case distinct op = (map (type_of o snd) clauses) of
   1.274 +        [] => case_error "no clauses given"
   1.275 +      | [T] => T
   1.276 +      | _ => case_error "all cases must have the same result type");
   1.277 +    val used' = fold add_row_used rows used;
   1.278 +    val (patts, case_tm) = mk_case tab ctxt ty_match ty_inst type_of
   1.279 +        used' rangeT {path = [x], rows = rows}
   1.280 +      handle CASE_ERROR (msg, i) => case_error (msg ^
   1.281 +        (if i < 0 then ""
   1.282 +         else "\nIn clause\n" ^ string_of_clause (nth clauses i)));
   1.283 +    val patts1 = map
   1.284 +      (fn (_, tag, [pat]) => (pat, tag)
   1.285 +        | _ => case_error "error in pattern-match translation") patts;
   1.286 +    val patts2 = Library.sort (Library.int_ord o Library.pairself row_of_pat) patts1
   1.287 +    val finals = map row_of_pat patts2
   1.288 +    val originals = map (row_of_pat o #2) rows
   1.289 +    val _ = case originals \\ finals of
   1.290 +        [] => ()
   1.291 +      | is => (if err then case_error else warning)
   1.292 +          ("The following clauses are redundant (covered by preceding clauses):\n" ^
   1.293 +           cat_lines (map (string_of_clause o nth clauses) is));
   1.294 +  in
   1.295 +    (case_tm, patts2)
   1.296 +  end;
   1.297 +
   1.298 +fun make_case tab ctxt = gen_make_case
   1.299 +  (match_type (ProofContext.theory_of ctxt)) Envir.subst_TVars fastype_of tab ctxt;
   1.300 +val make_case_untyped = gen_make_case (K (K Vartab.empty))
   1.301 +  (K (Term.map_types (K dummyT))) (K dummyT);
   1.302 +
   1.303 +
   1.304 +(* parse translation *)
   1.305 +
   1.306 +fun case_tr err tab_of ctxt [t, u] =
   1.307 +    let
   1.308 +      val thy = ProofContext.theory_of ctxt;
   1.309 +      (* replace occurrences of dummy_pattern by distinct variables *)
   1.310 +      (* internalize constant names                                 *)
   1.311 +      fun prep_pat ((c as Const ("_constrain", _)) $ t $ tT) used =
   1.312 +            let val (t', used') = prep_pat t used
   1.313 +            in (c $ t' $ tT, used') end
   1.314 +        | prep_pat (Const ("dummy_pattern", T)) used =
   1.315 +            let val x = Name.variant used "x"
   1.316 +            in (Free (x, T), x :: used) end
   1.317 +        | prep_pat (Const (s, T)) used =
   1.318 +            (case try (unprefix Syntax.constN) s of
   1.319 +               SOME c => (Const (c, T), used)
   1.320 +             | NONE => (Const (Sign.intern_const thy s, T), used))
   1.321 +        | prep_pat (v as Free (s, T)) used =
   1.322 +            let val s' = Sign.intern_const thy s
   1.323 +            in
   1.324 +              if Sign.declared_const thy s' then
   1.325 +                (Const (s', T), used)
   1.326 +              else (v, used)
   1.327 +            end
   1.328 +        | prep_pat (t $ u) used =
   1.329 +            let
   1.330 +              val (t', used') = prep_pat t used;
   1.331 +              val (u', used'') = prep_pat u used'
   1.332 +            in
   1.333 +              (t' $ u', used'')
   1.334 +            end
   1.335 +        | prep_pat t used = case_error ("Bad pattern: " ^ Syntax.string_of_term ctxt t);
   1.336 +      fun dest_case1 (t as Const ("_case1", _) $ l $ r) =
   1.337 +            let val (l', cnstrts) = strip_constraints l
   1.338 +            in ((fst (prep_pat l' (Term.add_free_names t [])), r), cnstrts)
   1.339 +            end
   1.340 +        | dest_case1 t = case_error "dest_case1";
   1.341 +      fun dest_case2 (Const ("_case2", _) $ t $ u) = t :: dest_case2 u
   1.342 +        | dest_case2 t = [t];
   1.343 +      val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 u));
   1.344 +      val (case_tm, _) = make_case_untyped (tab_of thy) ctxt err []
   1.345 +        (fold (fn tT => fn t => Syntax.const "_constrain" $ t $ tT)
   1.346 +           (flat cnstrts) t) cases;
   1.347 +    in case_tm end
   1.348 +  | case_tr _ _ _ ts = case_error "case_tr";
   1.349 +
   1.350 +
   1.351 +(*---------------------------------------------------------------------------
   1.352 + * Pretty printing of nested case expressions
   1.353 + *---------------------------------------------------------------------------*)
   1.354 +
   1.355 +(* destruct one level of pattern matching *)
   1.356 +
   1.357 +fun gen_dest_case name_of type_of tab d used t =
   1.358 +  case apfst name_of (strip_comb t) of
   1.359 +    (SOME cname, ts as _ :: _) =>
   1.360 +      let
   1.361 +        val (fs, x) = split_last ts;
   1.362 +        fun strip_abs i t =
   1.363 +          let
   1.364 +            val zs = strip_abs_vars t;
   1.365 +            val _ = if length zs < i then raise CASE_ERROR ("", 0) else ();
   1.366 +            val (xs, ys) = chop i zs;
   1.367 +            val u = list_abs (ys, strip_abs_body t);
   1.368 +            val xs' = map Free (Name.variant_list (OldTerm.add_term_names (u, used))
   1.369 +              (map fst xs) ~~ map snd xs)
   1.370 +          in (xs', subst_bounds (rev xs', u)) end;
   1.371 +        fun is_dependent i t =
   1.372 +          let val k = length (strip_abs_vars t) - i
   1.373 +          in k < 0 orelse exists (fn j => j >= k)
   1.374 +            (loose_bnos (strip_abs_body t))
   1.375 +          end;
   1.376 +        fun count_cases (_, _, true) = I
   1.377 +          | count_cases (c, (_, body), false) =
   1.378 +              AList.map_default op aconv (body, []) (cons c);
   1.379 +        val is_undefined = name_of #> equal (SOME "HOL.undefined");
   1.380 +        fun mk_case (c, (xs, body), _) = (list_comb (c, xs), body)
   1.381 +      in case ty_info tab cname of
   1.382 +          SOME {constructors, case_name} =>
   1.383 +            if length fs = length constructors then
   1.384 +              let
   1.385 +                val cases = map (fn (Const (s, U), t) =>
   1.386 +                  let
   1.387 +                    val k = length (binder_types U);
   1.388 +                    val p as (xs, _) = strip_abs k t
   1.389 +                  in
   1.390 +                    (Const (s, map type_of xs ---> type_of x),
   1.391 +                     p, is_dependent k t)
   1.392 +                  end) (constructors ~~ fs);
   1.393 +                val cases' = sort (int_ord o swap o pairself (length o snd))
   1.394 +                  (fold_rev count_cases cases []);
   1.395 +                val R = type_of t;
   1.396 +                val dummy = if d then Const ("dummy_pattern", R)
   1.397 +                  else Free (Name.variant used "x", R)
   1.398 +              in
   1.399 +                SOME (x, map mk_case (case find_first (is_undefined o fst) cases' of
   1.400 +                  SOME (_, cs) =>
   1.401 +                  if length cs = length constructors then [hd cases]
   1.402 +                  else filter_out (fn (_, (_, body), _) => is_undefined body) cases
   1.403 +                | NONE => case cases' of
   1.404 +                  [] => cases
   1.405 +                | (default, cs) :: _ =>
   1.406 +                  if length cs = 1 then cases
   1.407 +                  else if length cs = length constructors then
   1.408 +                    [hd cases, (dummy, ([], default), false)]
   1.409 +                  else
   1.410 +                    filter_out (fn (c, _, _) => member op aconv cs c) cases @
   1.411 +                    [(dummy, ([], default), false)]))
   1.412 +              end handle CASE_ERROR _ => NONE
   1.413 +            else NONE
   1.414 +        | _ => NONE
   1.415 +      end
   1.416 +  | _ => NONE;
   1.417 +
   1.418 +val dest_case = gen_dest_case (try (dest_Const #> fst)) fastype_of;
   1.419 +val dest_case' = gen_dest_case
   1.420 +  (try (dest_Const #> fst #> unprefix Syntax.constN)) (K dummyT);
   1.421 +
   1.422 +
   1.423 +(* destruct nested patterns *)
   1.424 +
   1.425 +fun strip_case'' dest (pat, rhs) =
   1.426 +  case dest (Term.add_free_names pat []) rhs of
   1.427 +    SOME (exp as Free _, clauses) =>
   1.428 +      if member op aconv (OldTerm.term_frees pat) exp andalso
   1.429 +        not (exists (fn (_, rhs') =>
   1.430 +          member op aconv (OldTerm.term_frees rhs') exp) clauses)
   1.431 +      then
   1.432 +        maps (strip_case'' dest) (map (fn (pat', rhs') =>
   1.433 +          (subst_free [(exp, pat')] pat, rhs')) clauses)
   1.434 +      else [(pat, rhs)]
   1.435 +  | _ => [(pat, rhs)];
   1.436 +
   1.437 +fun gen_strip_case dest t = case dest [] t of
   1.438 +    SOME (x, clauses) =>
   1.439 +      SOME (x, maps (strip_case'' dest) clauses)
   1.440 +  | NONE => NONE;
   1.441 +
   1.442 +val strip_case = gen_strip_case oo dest_case;
   1.443 +val strip_case' = gen_strip_case oo dest_case';
   1.444 +
   1.445 +
   1.446 +(* print translation *)
   1.447 +
   1.448 +fun case_tr' tab_of cname ctxt ts =
   1.449 +  let
   1.450 +    val thy = ProofContext.theory_of ctxt;
   1.451 +    val consts = ProofContext.consts_of ctxt;
   1.452 +    fun mk_clause (pat, rhs) =
   1.453 +      let val xs = Term.add_frees pat []
   1.454 +      in
   1.455 +        Syntax.const "_case1" $
   1.456 +          map_aterms
   1.457 +            (fn Free p => Syntax.mark_boundT p
   1.458 +              | Const (s, _) => Const (Consts.extern_early consts s, dummyT)
   1.459 +              | t => t) pat $
   1.460 +          map_aterms
   1.461 +            (fn x as Free (s, T) =>
   1.462 +                  if member (op =) xs (s, T) then Syntax.mark_bound s else x
   1.463 +              | t => t) rhs
   1.464 +      end
   1.465 +  in case strip_case' (tab_of thy) true (list_comb (Syntax.const cname, ts)) of
   1.466 +      SOME (x, clauses) => Syntax.const "_case_syntax" $ x $
   1.467 +        foldr1 (fn (t, u) => Syntax.const "_case2" $ t $ u)
   1.468 +          (map mk_clause clauses)
   1.469 +    | NONE => raise Match
   1.470 +  end;
   1.471 +
   1.472 +end;