new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
authorAndreas Lochbihler
Tue Jan 01 17:04:53 2019 +0100 (5 months ago)
changeset 69568de09a7261120
parent 69567 6b4c41037649
child 69569 2d88bf80c84f
new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
CONTRIBUTORS
NEWS
src/HOL/Library/Simps_Case_Conv.thy
src/HOL/Library/case_converter.ML
src/HOL/Library/code_lazy.ML
src/HOL/Library/simps_case_conv.ML
src/HOL/ex/Simps_Case_Conv_Examples.thy
     1.1 --- a/CONTRIBUTORS	Sun Dec 30 10:30:41 2018 +0100
     1.2 +++ b/CONTRIBUTORS	Tue Jan 01 17:04:53 2019 +0100
     1.3 @@ -6,6 +6,10 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* January 2019: Andreas Lochbihler
     1.8 +  New implementation for case_of_simps based on Code_Lazy's
     1.9 +  pattern matching elimination algorithm.
    1.10 +
    1.11  * October 2018: Mathias Fleury
    1.12    Proof reconstruction for the SMT solver veriT in the smt method
    1.13  
     2.1 --- a/NEWS	Sun Dec 30 10:30:41 2018 +0100
     2.2 +++ b/NEWS	Tue Jan 01 17:04:53 2019 +0100
     2.3 @@ -91,6 +91,13 @@
     2.4  
     2.5  * SMT: reconstruction is now possible using the SMT solver veriT.
     2.6  
     2.7 +* HOL-Library.Simps_Case_Conv: case_of_simps now supports overlapping 
     2.8 +and non-exhaustive patterns and handles arbitrarily nested patterns.
     2.9 +It uses on the same algorithm as HOL-Library.Code_Lazy, which assumes
    2.10 +sequential left-to-right pattern matching. The generated
    2.11 +equation no longer tuples the arguments on the right-hand side.
    2.12 +INCOMPATIBILITY.
    2.13 +
    2.14  * Session HOL-SPARK: .prv files are no longer written to the
    2.15  file-system, but exported to the session database. Results may be
    2.16  retrieved with the "isabelle export" command-line tool like this:
     3.1 --- a/src/HOL/Library/Simps_Case_Conv.thy	Sun Dec 30 10:30:41 2018 +0100
     3.2 +++ b/src/HOL/Library/Simps_Case_Conv.thy	Tue Jan 01 17:04:53 2019 +0100
     3.3 @@ -3,7 +3,7 @@
     3.4  *)
     3.5  
     3.6  theory Simps_Case_Conv
     3.7 -imports Main
     3.8 +imports Case_Converter
     3.9    keywords "simps_of_case" "case_of_simps" :: thy_decl
    3.10    abbrevs "simps_of_case" "case_of_simps" = ""
    3.11  begin
     4.1 --- a/src/HOL/Library/case_converter.ML	Sun Dec 30 10:30:41 2018 +0100
     4.2 +++ b/src/HOL/Library/case_converter.ML	Tue Jan 01 17:04:53 2019 +0100
     4.3 @@ -3,8 +3,11 @@
     4.4  
     4.5  signature CASE_CONVERTER =
     4.6  sig
     4.7 -  val to_case: Proof.context -> (string * string -> bool) -> (string * typ -> int) ->
     4.8 +  type elimination_strategy
     4.9 +  val to_case: Proof.context -> elimination_strategy -> (string * typ -> int) ->
    4.10      thm list -> thm list option
    4.11 +  val replace_by_type: (Proof.context -> string * string -> bool) -> elimination_strategy
    4.12 +  val keep_constructor_context: elimination_strategy
    4.13  end;
    4.14  
    4.15  structure Case_Converter : CASE_CONVERTER =
    4.16 @@ -60,30 +63,72 @@
    4.17      Coordinate (merge_consts xs ys)
    4.18    end;
    4.19  
    4.20 -fun term_to_coordinates P term = 
    4.21 -  let
    4.22 -    val (ctr, args) = strip_comb term
    4.23 -  in
    4.24 -    case ctr of Const (s, T) =>
    4.25 -      if P (body_type T |> dest_Type |> fst, s)
    4.26 -      then SOME (End (body_type T))
    4.27 -      else
    4.28 -        let
    4.29 -          fun f (i, t) = term_to_coordinates P t |> Option.map (pair i)
    4.30 -          val tcos = map_filter I (map_index f args)
    4.31 -        in
    4.32 -          if null tcos then NONE
    4.33 -          else SOME (Coordinate (map (pair s) tcos))
    4.34 -        end
    4.35 -    | _ => NONE
    4.36 -  end;
    4.37 -
    4.38  fun coordinates_to_list (End x) = [(x, [])]
    4.39    | coordinates_to_list (Coordinate xs) = 
    4.40    let
    4.41      fun f (s, (n, xss)) = map (fn (T, xs) => (T, (s, n) :: xs)) (coordinates_to_list xss)
    4.42    in flat (map f xs) end;
    4.43  
    4.44 +type elimination_strategy = Proof.context -> term list -> term_coordinate list
    4.45 +
    4.46 +fun replace_by_type replace_ctr ctxt pats =
    4.47 +  let
    4.48 +    fun term_to_coordinates P term = 
    4.49 +      let
    4.50 +        val (ctr, args) = strip_comb term
    4.51 +      in
    4.52 +        case ctr of Const (s, T) =>
    4.53 +          if P (body_type T |> dest_Type |> fst, s)
    4.54 +          then SOME (End (body_type T))
    4.55 +          else
    4.56 +            let
    4.57 +              fun f (i, t) = term_to_coordinates P t |> Option.map (pair i)
    4.58 +              val tcos = map_filter I (map_index f args)
    4.59 +            in
    4.60 +              if null tcos then NONE
    4.61 +              else SOME (Coordinate (map (pair s) tcos))
    4.62 +            end
    4.63 +        | _ => NONE
    4.64 +      end
    4.65 +    in
    4.66 +      map_filter (term_to_coordinates (replace_ctr ctxt)) pats
    4.67 +    end
    4.68 +
    4.69 +fun keep_constructor_context ctxt pats =
    4.70 +  let
    4.71 +    fun to_coordinates [] = NONE
    4.72 +      | to_coordinates pats =
    4.73 +        let
    4.74 +          val (fs, argss) = map strip_comb pats |> split_list
    4.75 +          val f = hd fs
    4.76 +          fun is_single_ctr (Const (name, T)) = 
    4.77 +              let
    4.78 +                val tyco = body_type T |> dest_Type |> fst
    4.79 +                val _ = Ctr_Sugar.ctr_sugar_of ctxt tyco |> the |> #ctrs
    4.80 +              in
    4.81 +                case Ctr_Sugar.ctr_sugar_of ctxt tyco of
    4.82 +                  NONE => error ("Not a free constructor " ^ name ^ " in pattern")
    4.83 +                | SOME info =>
    4.84 +                  case #ctrs info of [Const (name', _)] => name = name'
    4.85 +                    | _ => false
    4.86 +              end
    4.87 +            | is_single_ctr _ = false
    4.88 +        in 
    4.89 +          if not (is_single_ctr f) andalso forall (fn x => f = x) fs then
    4.90 +            let
    4.91 +              val patss = Ctr_Sugar_Util.transpose argss
    4.92 +              fun recurse (i, pats) = to_coordinates pats |> Option.map (pair i)
    4.93 +              val coords = map_filter I (map_index recurse patss)
    4.94 +            in
    4.95 +              if null coords then NONE
    4.96 +              else SOME (Coordinate (map (pair (dest_Const f |> fst)) coords))
    4.97 +            end
    4.98 +          else SOME (End (body_type (fastype_of f)))
    4.99 +          end
   4.100 +    in
   4.101 +      the_list (to_coordinates pats)
   4.102 +    end
   4.103 +
   4.104  
   4.105  (* AL: TODO: change from term to const_name *)
   4.106  fun find_ctr ctr1 xs =
   4.107 @@ -453,7 +498,8 @@
   4.108        ctxt1)
   4.109    end;
   4.110  
   4.111 -fun build_case_t replace_ctr ctr_count head lhss rhss ctxt =
   4.112 +
   4.113 +fun build_case_t elimination_strategy ctr_count head lhss rhss ctxt =
   4.114    let
   4.115      val num_eqs = length lhss
   4.116      val _ = if length rhss = num_eqs andalso num_eqs > 0 then ()
   4.117 @@ -464,16 +510,17 @@
   4.118      val _ = if forall (fn m => length m = n) lhss then ()
   4.119        else raise Fail "expected equal number of arguments"
   4.120  
   4.121 -    fun to_coordinates (n, ts) = case map_filter (term_to_coordinates replace_ctr) ts of
   4.122 -        [] => NONE
   4.123 -      | (tco :: tcos) => SOME (n, fold term_coordinate_merge tcos tco |> coordinates_to_list)
   4.124 +    fun to_coordinates (n, ts) = 
   4.125 +      case elimination_strategy ctxt ts of
   4.126 +          [] => NONE
   4.127 +        | (tco :: tcos) => SOME (n, fold term_coordinate_merge tcos tco |> coordinates_to_list)
   4.128      fun add_T (n, xss) = map (fn (T, xs) => (T, (n, xs))) xss
   4.129      val (typ_list, poss) = lhss
   4.130        |> Ctr_Sugar_Util.transpose
   4.131        |> map_index to_coordinates
   4.132        |> map_filter (Option.map add_T)
   4.133        |> flat
   4.134 -      |> split_list 
   4.135 +      |> split_list
   4.136    in
   4.137      if null poss then ([], [], ctxt)
   4.138      else terms_to_case ctxt (dest_Const #> ctr_count) head lhss rhss typ_list poss
     5.1 --- a/src/HOL/Library/code_lazy.ML	Sun Dec 30 10:30:41 2018 +0100
     5.2 +++ b/src/HOL/Library/code_lazy.ML	Tue Jan 01 17:04:53 2019 +0100
     5.3 @@ -530,18 +530,23 @@
     5.4  fun transform_code_eqs _ [] = NONE
     5.5    | transform_code_eqs ctxt eqs =
     5.6      let
     5.7 +      fun replace_ctr ctxt =
     5.8 +        let 
     5.9 +          val thy = Proof_Context.theory_of ctxt
    5.10 +          val table = Laziness_Data.get thy
    5.11 +        in fn (s1, s2) => case Symtab.lookup table s1 of
    5.12 +            NONE => false
    5.13 +          | SOME x => #active x andalso s2 <> (#ctr x |> dest_Const |> fst)
    5.14 +        end
    5.15        val thy = Proof_Context.theory_of ctxt
    5.16        val table = Laziness_Data.get thy
    5.17 -      fun eliminate (s1, s2) = case Symtab.lookup table s1 of
    5.18 -          NONE => false
    5.19 -        | SOME x => #active x andalso s2 <> (#ctr x |> dest_Const |> fst)
    5.20        fun num_consts_fun (_, T) =
    5.21          let
    5.22            val s = body_type T |> dest_Type |> fst
    5.23          in
    5.24            if Symtab.defined table s
    5.25 -            then Ctr_Sugar.ctr_sugar_of ctxt s |> the |> #ctrs |> length
    5.26 -            else Code.get_type thy s |> fst |> snd |> length
    5.27 +          then Ctr_Sugar.ctr_sugar_of ctxt s |> the |> #ctrs |> length
    5.28 +          else Code.get_type thy s |> fst |> snd |> length
    5.29          end
    5.30        val eqs = map (apfst (Thm.transfer thy)) eqs;
    5.31  
    5.32 @@ -554,10 +559,10 @@
    5.33          handle THM _ => (([], eqs), false)
    5.34        val to_original_eq = if pure then map (apfst (fn x => x RS @{thm eq_reflection})) else I
    5.35      in
    5.36 -      case Case_Converter.to_case ctxt eliminate num_consts_fun (map fst code_eqs) of
    5.37 +      case Case_Converter.to_case ctxt (Case_Converter.replace_by_type replace_ctr) num_consts_fun (map fst code_eqs) of
    5.38            NONE => NONE
    5.39          | SOME thms => SOME (nbe_eqs @ map (rpair true) thms |> to_original_eq)
    5.40 -    end handle THM ex => (Output.writeln (@{make_string} eqs); raise THM ex);
    5.41 +    end
    5.42  
    5.43  val activate_lazy_type = set_active_lazy_type true;
    5.44  val deactivate_lazy_type = set_active_lazy_type false;
     6.1 --- a/src/HOL/Library/simps_case_conv.ML	Sun Dec 30 10:30:41 2018 +0100
     6.2 +++ b/src/HOL/Library/simps_case_conv.ML	Tue Jan 01 17:04:53 2019 +0100
     6.3 @@ -31,88 +31,6 @@
     6.4  
     6.5  val strip_eq = Thm.prop_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq
     6.6  
     6.7 -
     6.8 -local
     6.9 -
    6.10 -  fun transpose [] = []
    6.11 -    | transpose ([] :: xss) = transpose xss
    6.12 -    | transpose xss = map hd xss :: transpose (map tl xss);
    6.13 -
    6.14 -  fun same_fun single_ctrs (ts as _ $ _ :: _) =
    6.15 -      let
    6.16 -        val (fs, argss) = map strip_comb ts |> split_list
    6.17 -        val f = hd fs
    6.18 -        fun is_single_ctr (Const (name, _)) = member (op =) single_ctrs name
    6.19 -          | is_single_ctr _ = false
    6.20 -      in if not (is_single_ctr f) andalso forall (fn x => f = x) fs then SOME (f, argss) else NONE end
    6.21 -    | same_fun _ _ = NONE
    6.22 -
    6.23 -  (* pats must be non-empty *)
    6.24 -  fun split_pat single_ctrs pats ctxt =
    6.25 -      case same_fun single_ctrs pats of
    6.26 -        NONE =>
    6.27 -          let
    6.28 -            val (name, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt
    6.29 -            val var = Free (name, fastype_of (hd pats))
    6.30 -          in (((var, [var]), map single pats), ctxt') end
    6.31 -      | SOME (f, argss) =>
    6.32 -          let
    6.33 -            val (((def_pats, def_frees), case_patss), ctxt') =
    6.34 -              split_pats single_ctrs argss ctxt
    6.35 -            val def_pat = list_comb (f, def_pats)
    6.36 -          in (((def_pat, flat def_frees), case_patss), ctxt') end
    6.37 -  and
    6.38 -      split_pats single_ctrs patss ctxt =
    6.39 -        let
    6.40 -          val (splitted, ctxt') = fold_map (split_pat single_ctrs) (transpose patss) ctxt
    6.41 -          val r = splitted |> split_list |> apfst split_list |> apsnd (transpose #> map flat)
    6.42 -        in (r, ctxt') end
    6.43 -
    6.44 -(*
    6.45 -  Takes a list lhss of left hand sides (which are lists of patterns)
    6.46 -  and a list rhss of right hand sides. Returns
    6.47 -    - a single equation with a (nested) case-expression on the rhs
    6.48 -    - a list of all split-thms needed to split the rhs
    6.49 -  Patterns which have the same outer context in all lhss remain
    6.50 -  on the lhs of the computed equation.
    6.51 -*)
    6.52 -fun build_case_t fun_t lhss rhss ctxt =
    6.53 -  let
    6.54 -    val single_ctrs =
    6.55 -      get_type_infos ctxt (map fastype_of (flat lhss))
    6.56 -      |> map_filter (fn ti => case #ctrs ti of [Const (name, _)] => SOME name | _ => NONE)
    6.57 -    val (((def_pats, def_frees), case_patss), ctxt') =
    6.58 -      split_pats single_ctrs lhss ctxt
    6.59 -    val pattern = map HOLogic.mk_tuple case_patss
    6.60 -    val case_arg = HOLogic.mk_tuple (flat def_frees)
    6.61 -    val cases = Case_Translation.make_case ctxt' Case_Translation.Warning Name.context
    6.62 -      case_arg (pattern ~~ rhss)
    6.63 -    val split_thms = get_split_ths ctxt' [fastype_of case_arg]
    6.64 -    val t = (list_comb (fun_t, def_pats), cases)
    6.65 -      |> HOLogic.mk_eq
    6.66 -      |> HOLogic.mk_Trueprop
    6.67 -  in ((t, split_thms), ctxt') end
    6.68 -
    6.69 -fun tac ctxt {splits, intros, defs} =
    6.70 -  let val ctxt' = Classical.addSIs (ctxt, intros) in
    6.71 -    REPEAT_DETERM1 (FIRSTGOAL (split_tac ctxt splits))
    6.72 -    THEN Local_Defs.unfold_tac ctxt defs
    6.73 -    THEN safe_tac ctxt'
    6.74 -  end
    6.75 -
    6.76 -fun import [] ctxt = ([], ctxt)
    6.77 -  | import (thm :: thms) ctxt =
    6.78 -    let
    6.79 -      val fun_ct = strip_eq #> fst #> strip_comb #> fst #> Logic.mk_term
    6.80 -        #> Thm.cterm_of ctxt
    6.81 -      val ct = fun_ct thm
    6.82 -      val cts = map fun_ct thms
    6.83 -      val pairs = map (fn s => (s,ct)) cts
    6.84 -      val thms' = map (fn (th,p) => Thm.instantiate (Thm.match p) th) (thms ~~ pairs)
    6.85 -    in Variable.import true (thm :: thms') ctxt |> apfst snd end
    6.86 -
    6.87 -in
    6.88 -
    6.89  (*
    6.90    For a list
    6.91      f p_11 ... p_1n = t1
    6.92 @@ -122,39 +40,24 @@
    6.93    of theorems, prove a single theorem
    6.94      f x1 ... xn = t
    6.95    where t is a (nested) case expression. f must not be a function
    6.96 -  application. Moreover, the terms p_11, ..., p_mn must be non-overlapping
    6.97 -  datatype patterns. The patterns must be exhausting up to common constructor
    6.98 -  contexts.
    6.99 +  application.
   6.100  *)
   6.101  fun to_case ctxt ths =
   6.102    let
   6.103 -    val (iths, ctxt') = import ths ctxt
   6.104 -    val fun_t = hd iths |> strip_eq |> fst |> head_of
   6.105 -    val eqs = map (strip_eq #> apfst (snd o strip_comb)) iths
   6.106 -
   6.107 -    fun hide_rhs ((pat, rhs), name) lthy =
   6.108 +    fun ctr_count (ctr, T) = 
   6.109        let
   6.110 -        val frees = fold Term.add_frees pat []
   6.111 -        val abs_rhs = fold absfree frees rhs
   6.112 -        val ([(f, (_, def))], lthy') = lthy
   6.113 -          |> Local_Defs.define [((Binding.name name, NoSyn), (Binding.empty_atts, abs_rhs))]
   6.114 -      in ((list_comb (f, map Free (rev frees)), def), lthy') end
   6.115 -
   6.116 -    val ((def_ts, def_thms), ctxt2) =
   6.117 -      let val names = Name.invent (Variable.names_of ctxt') "rhs" (length eqs)
   6.118 -      in fold_map hide_rhs (eqs ~~ names) ctxt' |> apfst split_list end
   6.119 -
   6.120 -    val ((t, split_thms), ctxt3) = build_case_t fun_t (map fst eqs) def_ts ctxt2
   6.121 -
   6.122 -    val th = Goal.prove ctxt3 [] [] t (fn {context=ctxt, ...} =>
   6.123 -          tac ctxt {splits=split_thms, intros=ths, defs=def_thms})
   6.124 -  in th
   6.125 -    |> singleton (Proof_Context.export ctxt3 ctxt)
   6.126 -    |> Goal.norm_result ctxt
   6.127 +        val tyco = body_type T |> dest_Type |> fst
   6.128 +        val info = Ctr_Sugar.ctr_sugar_of ctxt tyco
   6.129 +        val _ = if is_none info then error ("Pattern match on non-constructor constant " ^ ctr) else ()
   6.130 +      in
   6.131 +        info |> the |> #ctrs |> length
   6.132 +      end
   6.133 +    val thms = Case_Converter.to_case ctxt Case_Converter.keep_constructor_context ctr_count ths
   6.134 +  in
   6.135 +    case thms of SOME thms => hd thms
   6.136 +      | _ => error ("Conversion to case expression failed.")
   6.137    end
   6.138  
   6.139 -end
   6.140 -
   6.141  local
   6.142  
   6.143  fun was_split t =
     7.1 --- a/src/HOL/ex/Simps_Case_Conv_Examples.thy	Sun Dec 30 10:30:41 2018 +0100
     7.2 +++ b/src/HOL/ex/Simps_Case_Conv_Examples.thy	Tue Jan 01 17:04:53 2019 +0100
     7.3 @@ -30,27 +30,23 @@
     7.4  case_of_simps foo_cases1: foo.simps
     7.5  lemma
     7.6    fixes xs :: "'a list" and ys :: "'b list"
     7.7 -  shows "foo xs ys = (case (xs, ys) of
     7.8 -    ( [], []) \<Rightarrow> 3
     7.9 -    | ([], y # ys) \<Rightarrow> 1
    7.10 -    | (x # xs, []) \<Rightarrow> 0
    7.11 -    | (x # xs, y # ys) \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list))"
    7.12 +  shows "foo xs ys = 
    7.13 +   (case xs of [] \<Rightarrow> (case ys of [] \<Rightarrow> 3 | _ # _ \<Rightarrow> 1)
    7.14 +    | _ # _ \<Rightarrow> (case ys of [] \<Rightarrow> 0 | _ # _ \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list)))"
    7.15    by (fact foo_cases1)
    7.16  
    7.17  text \<open>Redundant equations are ignored\<close>
    7.18  case_of_simps foo_cases2: foo.simps foo.simps
    7.19  lemma
    7.20    fixes xs :: "'a list" and ys :: "'b list"
    7.21 -  shows "foo xs ys = (case (xs, ys) of
    7.22 -    ( [], []) \<Rightarrow> 3
    7.23 -    | ([], y # ys) \<Rightarrow> 1
    7.24 -    | (x # xs, []) \<Rightarrow> 0
    7.25 -    | (x # xs, y # ys) \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list))"
    7.26 +  shows "foo xs ys = 
    7.27 +   (case xs of [] \<Rightarrow> (case ys of [] \<Rightarrow> 3 | _ # _ \<Rightarrow> 1)
    7.28 +    | _ # _ \<Rightarrow> (case ys of [] \<Rightarrow> 0 | _ # _ \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list)))"
    7.29    by (fact foo_cases2)
    7.30  
    7.31  text \<open>Variable patterns\<close>
    7.32  case_of_simps bar_cases: bar.simps
    7.33 -print_theorems
    7.34 +lemma "bar x n y = (case n of 0 \<Rightarrow> 0 + x | Suc n' \<Rightarrow> n' + x)" by(fact bar_cases)
    7.35  
    7.36  text \<open>Case expression not at top level\<close>
    7.37  simps_of_case split_rule_test_simps: split_rule_test_def
    7.38 @@ -96,24 +92,23 @@
    7.39  text \<open>Reversal\<close>
    7.40  case_of_simps test_def1: test_simps1
    7.41  lemma
    7.42 -  "test x y = (case (x,y) of
    7.43 -    (None, []) \<Rightarrow> 1
    7.44 -  | (None, _#_) \<Rightarrow> 2
    7.45 -  | (Some x, _) \<Rightarrow> x)"
    7.46 +  "test x y = 
    7.47 +   (case x of None \<Rightarrow> (case y of [] \<Rightarrow> 1 | _ # _ \<Rightarrow> 2)
    7.48 +    | Some x' \<Rightarrow> x')"
    7.49    by (fact test_def1)
    7.50  
    7.51  text \<open>Case expressions on RHS\<close>
    7.52  case_of_simps test_def2: test_simps2
    7.53 -lemma "test xs y = (case (xs, y) of (None, []) \<Rightarrow> 1 | (None, x # xa) \<Rightarrow> 2 | (Some x, y) \<Rightarrow> x)"
    7.54 +lemma "test x y = 
    7.55 +  (case x of None \<Rightarrow> (case y of [] \<Rightarrow> 1 | _ # _ \<Rightarrow> 2)
    7.56 +   | Some x' \<Rightarrow> x')"
    7.57    by (fact test_def2)
    7.58  
    7.59  text \<open>Partial split of simps\<close>
    7.60  case_of_simps foo_cons_def: foo.simps(1,2)
    7.61  lemma
    7.62    fixes xs :: "'a list" and ys :: "'b list"
    7.63 -  shows "foo (x # xs) ys = (case (x,xs,ys) of
    7.64 -      (_,_,[]) \<Rightarrow> 0
    7.65 -    | (_,_,_ # _) \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list))"
    7.66 +  shows "foo (x # xs) ys = (case ys of [] \<Rightarrow> 0 | _ # _ \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list))"
    7.67    by (fact foo_cons_def)
    7.68  
    7.69  end