1.1 --- a/src/HOL/Library/simps_case_conv.ML	Fri Sep 06 10:56:40 2013 +0200
     1.2 +++ b/src/HOL/Library/simps_case_conv.ML	Fri Sep 06 10:56:40 2013 +0200
     1.3 @@ -32,12 +32,59 @@
     1.4  
     1.5  local
     1.6  
     1.7 -(*Creates free variables for a list of types*)
     1.8 -fun mk_Frees Ts ctxt =
     1.9 +  fun transpose [] = []
    1.10 +    | transpose ([] :: xss) = transpose xss
    1.11 +    | transpose xss = map hd xss :: transpose (map tl xss);
    1.12 +
    1.13 +  fun same_fun (ts as _ $ _ :: _) =
    1.14 +      let
    1.15 +        val (fs, argss) = map strip_comb ts |> split_list
    1.16 +        val f = hd fs
    1.17 +      in if forall (fn x => f = x) fs then SOME (f, argss) else NONE end
    1.18 +    | same_fun _ = NONE
    1.19 +
    1.20 +  (* pats must be non-empty *)
    1.21 +  fun split_pat pats ctxt =
    1.22 +      case same_fun pats of
    1.23 +        NONE =>
    1.24 +          let
    1.25 +            val (name, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt
    1.26 +            val var = Free (name, fastype_of (hd pats))
    1.27 +          in (((var, [var]), map single pats), ctxt') end
    1.28 +      | SOME (f, argss) =>
    1.29 +          let
    1.30 +            val (((def_pats, def_frees), case_patss), ctxt') =
    1.31 +              split_pats argss ctxt
    1.32 +            val def_pat = list_comb (f, def_pats)
    1.33 +          in (((def_pat, flat def_frees), case_patss), ctxt') end
    1.34 +  and
    1.35 +      split_pats patss ctxt =
    1.36 +        let
    1.37 +          val (splitted, ctxt') = fold_map split_pat (transpose patss) ctxt
    1.38 +          val r = splitted |> split_list |> apfst split_list |> apsnd (transpose #> map flat)
    1.39 +        in (r, ctxt') end
    1.40 +
    1.41 +(*
    1.42 +  Takes a list lhss of left hand sides (which are lists of patterns)
    1.43 +  and a list rhss of right hand sides. Returns
    1.44 +    - a single equation with a (nested) case-expression on the rhs
    1.45 +    - a list of all split-thms needed to split the rhs
    1.46 +  Patterns which have the same outer context in all lhss remain
    1.47 +  on the lhs of the computed equation.
    1.48 +*)
    1.49 +fun build_case_t fun_t lhss rhss ctxt =
    1.50    let
    1.51 -    val (names,ctxt') = Variable.variant_fixes (replicate (length Ts) "x") ctxt
    1.52 -    val ts = map Free (names ~~ Ts)
    1.53 -  in (ts, ctxt') end
    1.54 +    val (((def_pats, def_frees), case_patss), ctxt') =
    1.55 +      split_pats lhss ctxt
    1.56 +    val pattern = map HOLogic.mk_tuple case_patss
    1.57 +    val case_arg = HOLogic.mk_tuple (flat def_frees)
    1.58 +    val cases = Case_Translation.make_case ctxt' Case_Translation.Warning Name.context
    1.59 +      case_arg (pattern ~~ rhss)
    1.60 +    val split_thms = get_split_ths (Proof_Context.theory_of ctxt') (fastype_of case_arg)
    1.61 +    val t = (list_comb (fun_t, def_pats), cases)
    1.62 +      |> HOLogic.mk_eq
    1.63 +      |> HOLogic.mk_Trueprop
    1.64 +  in ((t, split_thms), ctxt') end
    1.65  
    1.66  fun tac ctxt {splits, intros, defs} =
    1.67    let val ctxt' = Classical.addSIs (ctxt, intros) in
    1.68 @@ -67,16 +114,16 @@
    1.69      f p_mn ... p_mn = tm
    1.70    of theorems, prove a single theorem
    1.71      f x1 ... xn = t
    1.72 -  where t is a (nested) case expression. The terms p_11, ..., p_mn must
    1.73 -  be exhaustive, non-overlapping datatype patterns. f must not be a function
    1.74 -  application.
    1.75 +  where t is a (nested) case expression. f must not be a function
    1.76 +  application. Moreover, the terms p_11, ..., p_mn must be non-overlapping
    1.77 +  datatype patterns. The patterns must be exhausting up to common constructor
    1.78 +  contexts.
    1.79  *)
    1.80  fun to_case ctxt ths =
    1.81    let
    1.82      val (iths, ctxt') = import ths ctxt
    1.83 -    val (fun_t, arg_ts) = hd iths |> strip_eq |> fst |> strip_comb
    1.84 +    val fun_t = hd iths |> strip_eq |> fst |> head_of
    1.85      val eqs = map (strip_eq #> apfst (snd o strip_comb)) iths
    1.86 -    val (arg_Frees, ctxt'') = mk_Frees (map fastype_of arg_ts) ctxt'
    1.87  
    1.88      fun hide_rhs ((pat, rhs), name) lthy = let
    1.89          val frees = fold Term.add_frees pat []
    1.90 @@ -85,23 +132,13 @@
    1.91            ((Binding.name name, Mixfix.NoSyn), abs_rhs) lthy
    1.92        in ((list_comb (f, map Free (rev frees)), def), lthy') end
    1.93  
    1.94 -    val ((def_ts, def_thms), ctxt3) = let
    1.95 -        val nctxt = Variable.names_of ctxt''
    1.96 +    val ((def_ts, def_thms), ctxt2) = let
    1.97 +        val nctxt = Variable.names_of ctxt'
    1.98          val names = Name.invent nctxt "rhs" (length eqs)
    1.99 -      in fold_map hide_rhs (eqs ~~ names) ctxt'' |> apfst split_list end
   1.100 +      in fold_map hide_rhs (eqs ~~ names) ctxt' |> apfst split_list end
   1.101  
   1.102 -    val (cases, split_thms) =
   1.103 -      let
   1.104 -        val pattern = map (fst #> HOLogic.mk_tuple) eqs
   1.105 -        val case_arg = HOLogic.mk_tuple arg_Frees
   1.106 -        val cases = Case_Translation.make_case ctxt Case_Translation.Warning Name.context
   1.107 -          case_arg (pattern ~~ def_ts)
   1.108 -        val split_thms = get_split_ths (Proof_Context.theory_of ctxt3) (fastype_of case_arg)
   1.109 -      in (cases, split_thms) end
   1.110 +    val ((t, split_thms), ctxt3) = build_case_t fun_t (map fst eqs) def_ts ctxt2
   1.111  
   1.112 -    val t = (list_comb (fun_t, arg_Frees), cases)
   1.113 -      |> HOLogic.mk_eq
   1.114 -      |> HOLogic.mk_Trueprop
   1.115      val th = Goal.prove ctxt3 [] [] t (fn {context=ctxt, ...} =>
   1.116            tac ctxt {splits=split_thms, intros=ths, defs=def_thms})
   1.117    in th