merged
authorAndreas Lochbihler
Tue Jan 01 18:33:19 2019 +0100 (6 months ago)
changeset 695692d88bf80c84f
parent 69564 a59f7d07bf17
parent 69568 de09a7261120
child 69570 2f78e0d73a34
merged
NEWS
     1.1 --- a/CONTRIBUTORS	Tue Jan 01 13:26:37 2019 +0100
     1.2 +++ b/CONTRIBUTORS	Tue Jan 01 18:33:19 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	Tue Jan 01 13:26:37 2019 +0100
     2.2 +++ b/NEWS	Tue Jan 01 18:33:19 2019 +0100
     2.3 @@ -92,6 +92,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 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Case_Converter.thy	Tue Jan 01 18:33:19 2019 +0100
     3.3 @@ -0,0 +1,23 @@
     3.4 +(* Author: Pascal Stoop, ETH Zurich
     3.5 +   Author: Andreas Lochbihler, Digital Asset *)
     3.6 +
     3.7 +theory Case_Converter
     3.8 +  imports Main
     3.9 +begin
    3.10 +
    3.11 +subsection \<open>Eliminating pattern matches\<close>
    3.12 +
    3.13 +definition missing_pattern_match :: "String.literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a" where
    3.14 +  [code del]: "missing_pattern_match m f = f ()"
    3.15 +
    3.16 +lemma missing_pattern_match_cong [cong]:
    3.17 +  "m = m' \<Longrightarrow> missing_pattern_match m f = missing_pattern_match m' f"
    3.18 +  by(rule arg_cong)
    3.19 +
    3.20 +lemma missing_pattern_match_code [code_unfold]:
    3.21 +  "missing_pattern_match = Code.abort"
    3.22 +  unfolding missing_pattern_match_def Code.abort_def ..
    3.23 +
    3.24 +ML_file "case_converter.ML"
    3.25 +
    3.26 +end
     4.1 --- a/src/HOL/Library/Code_Lazy.thy	Tue Jan 01 13:26:37 2019 +0100
     4.2 +++ b/src/HOL/Library/Code_Lazy.thy	Tue Jan 01 18:33:19 2019 +0100
     4.3 @@ -4,7 +4,7 @@
     4.4  section \<open>Lazy types in generated code\<close>
     4.5  
     4.6  theory Code_Lazy
     4.7 -imports Main
     4.8 +imports Case_Converter
     4.9  keywords
    4.10    "code_lazy_type"
    4.11    "activate_lazy_type"
    4.12 @@ -24,22 +24,6 @@
    4.13    and thus eligible for lazification.
    4.14  \<close>
    4.15  
    4.16 -subsection \<open>Eliminating pattern matches\<close>
    4.17 -
    4.18 -definition missing_pattern_match :: "String.literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a" where
    4.19 -  [code del]: "missing_pattern_match m f = f ()"
    4.20 -
    4.21 -lemma missing_pattern_match_cong [cong]:
    4.22 -  "m = m' \<Longrightarrow> missing_pattern_match m f = missing_pattern_match m' f"
    4.23 -  by(rule arg_cong)
    4.24 -
    4.25 -lemma missing_pattern_match_code [code_unfold]:
    4.26 -  "missing_pattern_match = Code.abort"
    4.27 -  unfolding missing_pattern_match_def Code.abort_def ..
    4.28 -
    4.29 -ML_file "case_converter.ML"
    4.30 -
    4.31 -
    4.32  subsection \<open>The type \<open>lazy\<close>\<close>
    4.33  
    4.34  typedef 'a lazy = "UNIV :: 'a set" ..
     5.1 --- a/src/HOL/Library/Simps_Case_Conv.thy	Tue Jan 01 13:26:37 2019 +0100
     5.2 +++ b/src/HOL/Library/Simps_Case_Conv.thy	Tue Jan 01 18:33:19 2019 +0100
     5.3 @@ -3,7 +3,7 @@
     5.4  *)
     5.5  
     5.6  theory Simps_Case_Conv
     5.7 -imports Main
     5.8 +imports Case_Converter
     5.9    keywords "simps_of_case" "case_of_simps" :: thy_decl
    5.10    abbrevs "simps_of_case" "case_of_simps" = ""
    5.11  begin
     6.1 --- a/src/HOL/Library/case_converter.ML	Tue Jan 01 13:26:37 2019 +0100
     6.2 +++ b/src/HOL/Library/case_converter.ML	Tue Jan 01 18:33:19 2019 +0100
     6.3 @@ -3,8 +3,11 @@
     6.4  
     6.5  signature CASE_CONVERTER =
     6.6  sig
     6.7 -  val to_case: Proof.context -> (string * string -> bool) -> (string * typ -> int) ->
     6.8 +  type elimination_strategy
     6.9 +  val to_case: Proof.context -> elimination_strategy -> (string * typ -> int) ->
    6.10      thm list -> thm list option
    6.11 +  val replace_by_type: (Proof.context -> string * string -> bool) -> elimination_strategy
    6.12 +  val keep_constructor_context: elimination_strategy
    6.13  end;
    6.14  
    6.15  structure Case_Converter : CASE_CONVERTER =
    6.16 @@ -60,30 +63,72 @@
    6.17      Coordinate (merge_consts xs ys)
    6.18    end;
    6.19  
    6.20 -fun term_to_coordinates P term = 
    6.21 -  let
    6.22 -    val (ctr, args) = strip_comb term
    6.23 -  in
    6.24 -    case ctr of Const (s, T) =>
    6.25 -      if P (body_type T |> dest_Type |> fst, s)
    6.26 -      then SOME (End (body_type T))
    6.27 -      else
    6.28 -        let
    6.29 -          fun f (i, t) = term_to_coordinates P t |> Option.map (pair i)
    6.30 -          val tcos = map_filter I (map_index f args)
    6.31 -        in
    6.32 -          if null tcos then NONE
    6.33 -          else SOME (Coordinate (map (pair s) tcos))
    6.34 -        end
    6.35 -    | _ => NONE
    6.36 -  end;
    6.37 -
    6.38  fun coordinates_to_list (End x) = [(x, [])]
    6.39    | coordinates_to_list (Coordinate xs) = 
    6.40    let
    6.41      fun f (s, (n, xss)) = map (fn (T, xs) => (T, (s, n) :: xs)) (coordinates_to_list xss)
    6.42    in flat (map f xs) end;
    6.43  
    6.44 +type elimination_strategy = Proof.context -> term list -> term_coordinate list
    6.45 +
    6.46 +fun replace_by_type replace_ctr ctxt pats =
    6.47 +  let
    6.48 +    fun term_to_coordinates P term = 
    6.49 +      let
    6.50 +        val (ctr, args) = strip_comb term
    6.51 +      in
    6.52 +        case ctr of Const (s, T) =>
    6.53 +          if P (body_type T |> dest_Type |> fst, s)
    6.54 +          then SOME (End (body_type T))
    6.55 +          else
    6.56 +            let
    6.57 +              fun f (i, t) = term_to_coordinates P t |> Option.map (pair i)
    6.58 +              val tcos = map_filter I (map_index f args)
    6.59 +            in
    6.60 +              if null tcos then NONE
    6.61 +              else SOME (Coordinate (map (pair s) tcos))
    6.62 +            end
    6.63 +        | _ => NONE
    6.64 +      end
    6.65 +    in
    6.66 +      map_filter (term_to_coordinates (replace_ctr ctxt)) pats
    6.67 +    end
    6.68 +
    6.69 +fun keep_constructor_context ctxt pats =
    6.70 +  let
    6.71 +    fun to_coordinates [] = NONE
    6.72 +      | to_coordinates pats =
    6.73 +        let
    6.74 +          val (fs, argss) = map strip_comb pats |> split_list
    6.75 +          val f = hd fs
    6.76 +          fun is_single_ctr (Const (name, T)) = 
    6.77 +              let
    6.78 +                val tyco = body_type T |> dest_Type |> fst
    6.79 +                val _ = Ctr_Sugar.ctr_sugar_of ctxt tyco |> the |> #ctrs
    6.80 +              in
    6.81 +                case Ctr_Sugar.ctr_sugar_of ctxt tyco of
    6.82 +                  NONE => error ("Not a free constructor " ^ name ^ " in pattern")
    6.83 +                | SOME info =>
    6.84 +                  case #ctrs info of [Const (name', _)] => name = name'
    6.85 +                    | _ => false
    6.86 +              end
    6.87 +            | is_single_ctr _ = false
    6.88 +        in 
    6.89 +          if not (is_single_ctr f) andalso forall (fn x => f = x) fs then
    6.90 +            let
    6.91 +              val patss = Ctr_Sugar_Util.transpose argss
    6.92 +              fun recurse (i, pats) = to_coordinates pats |> Option.map (pair i)
    6.93 +              val coords = map_filter I (map_index recurse patss)
    6.94 +            in
    6.95 +              if null coords then NONE
    6.96 +              else SOME (Coordinate (map (pair (dest_Const f |> fst)) coords))
    6.97 +            end
    6.98 +          else SOME (End (body_type (fastype_of f)))
    6.99 +          end
   6.100 +    in
   6.101 +      the_list (to_coordinates pats)
   6.102 +    end
   6.103 +
   6.104  
   6.105  (* AL: TODO: change from term to const_name *)
   6.106  fun find_ctr ctr1 xs =
   6.107 @@ -453,7 +498,8 @@
   6.108        ctxt1)
   6.109    end;
   6.110  
   6.111 -fun build_case_t replace_ctr ctr_count head lhss rhss ctxt =
   6.112 +
   6.113 +fun build_case_t elimination_strategy ctr_count head lhss rhss ctxt =
   6.114    let
   6.115      val num_eqs = length lhss
   6.116      val _ = if length rhss = num_eqs andalso num_eqs > 0 then ()
   6.117 @@ -464,16 +510,17 @@
   6.118      val _ = if forall (fn m => length m = n) lhss then ()
   6.119        else raise Fail "expected equal number of arguments"
   6.120  
   6.121 -    fun to_coordinates (n, ts) = case map_filter (term_to_coordinates replace_ctr) ts of
   6.122 -        [] => NONE
   6.123 -      | (tco :: tcos) => SOME (n, fold term_coordinate_merge tcos tco |> coordinates_to_list)
   6.124 +    fun to_coordinates (n, ts) = 
   6.125 +      case elimination_strategy ctxt ts of
   6.126 +          [] => NONE
   6.127 +        | (tco :: tcos) => SOME (n, fold term_coordinate_merge tcos tco |> coordinates_to_list)
   6.128      fun add_T (n, xss) = map (fn (T, xs) => (T, (n, xs))) xss
   6.129      val (typ_list, poss) = lhss
   6.130        |> Ctr_Sugar_Util.transpose
   6.131        |> map_index to_coordinates
   6.132        |> map_filter (Option.map add_T)
   6.133        |> flat
   6.134 -      |> split_list 
   6.135 +      |> split_list
   6.136    in
   6.137      if null poss then ([], [], ctxt)
   6.138      else terms_to_case ctxt (dest_Const #> ctr_count) head lhss rhss typ_list poss
     7.1 --- a/src/HOL/Library/code_lazy.ML	Tue Jan 01 13:26:37 2019 +0100
     7.2 +++ b/src/HOL/Library/code_lazy.ML	Tue Jan 01 18:33:19 2019 +0100
     7.3 @@ -530,18 +530,23 @@
     7.4  fun transform_code_eqs _ [] = NONE
     7.5    | transform_code_eqs ctxt eqs =
     7.6      let
     7.7 +      fun replace_ctr ctxt =
     7.8 +        let 
     7.9 +          val thy = Proof_Context.theory_of ctxt
    7.10 +          val table = Laziness_Data.get thy
    7.11 +        in fn (s1, s2) => case Symtab.lookup table s1 of
    7.12 +            NONE => false
    7.13 +          | SOME x => #active x andalso s2 <> (#ctr x |> dest_Const |> fst)
    7.14 +        end
    7.15        val thy = Proof_Context.theory_of ctxt
    7.16        val table = Laziness_Data.get thy
    7.17 -      fun eliminate (s1, s2) = case Symtab.lookup table s1 of
    7.18 -          NONE => false
    7.19 -        | SOME x => #active x andalso s2 <> (#ctr x |> dest_Const |> fst)
    7.20        fun num_consts_fun (_, T) =
    7.21          let
    7.22            val s = body_type T |> dest_Type |> fst
    7.23          in
    7.24            if Symtab.defined table s
    7.25 -            then Ctr_Sugar.ctr_sugar_of ctxt s |> the |> #ctrs |> length
    7.26 -            else Code.get_type thy s |> fst |> snd |> length
    7.27 +          then Ctr_Sugar.ctr_sugar_of ctxt s |> the |> #ctrs |> length
    7.28 +          else Code.get_type thy s |> fst |> snd |> length
    7.29          end
    7.30        val eqs = map (apfst (Thm.transfer thy)) eqs;
    7.31  
    7.32 @@ -554,10 +559,10 @@
    7.33          handle THM _ => (([], eqs), false)
    7.34        val to_original_eq = if pure then map (apfst (fn x => x RS @{thm eq_reflection})) else I
    7.35      in
    7.36 -      case Case_Converter.to_case ctxt eliminate num_consts_fun (map fst code_eqs) of
    7.37 +      case Case_Converter.to_case ctxt (Case_Converter.replace_by_type replace_ctr) num_consts_fun (map fst code_eqs) of
    7.38            NONE => NONE
    7.39          | SOME thms => SOME (nbe_eqs @ map (rpair true) thms |> to_original_eq)
    7.40 -    end handle THM ex => (Output.writeln (@{make_string} eqs); raise THM ex);
    7.41 +    end
    7.42  
    7.43  val activate_lazy_type = set_active_lazy_type true;
    7.44  val deactivate_lazy_type = set_active_lazy_type false;
     8.1 --- a/src/HOL/Library/simps_case_conv.ML	Tue Jan 01 13:26:37 2019 +0100
     8.2 +++ b/src/HOL/Library/simps_case_conv.ML	Tue Jan 01 18:33:19 2019 +0100
     8.3 @@ -31,88 +31,6 @@
     8.4  
     8.5  val strip_eq = Thm.prop_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq
     8.6  
     8.7 -
     8.8 -local
     8.9 -
    8.10 -  fun transpose [] = []
    8.11 -    | transpose ([] :: xss) = transpose xss
    8.12 -    | transpose xss = map hd xss :: transpose (map tl xss);
    8.13 -
    8.14 -  fun same_fun single_ctrs (ts as _ $ _ :: _) =
    8.15 -      let
    8.16 -        val (fs, argss) = map strip_comb ts |> split_list
    8.17 -        val f = hd fs
    8.18 -        fun is_single_ctr (Const (name, _)) = member (op =) single_ctrs name
    8.19 -          | is_single_ctr _ = false
    8.20 -      in if not (is_single_ctr f) andalso forall (fn x => f = x) fs then SOME (f, argss) else NONE end
    8.21 -    | same_fun _ _ = NONE
    8.22 -
    8.23 -  (* pats must be non-empty *)
    8.24 -  fun split_pat single_ctrs pats ctxt =
    8.25 -      case same_fun single_ctrs pats of
    8.26 -        NONE =>
    8.27 -          let
    8.28 -            val (name, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt
    8.29 -            val var = Free (name, fastype_of (hd pats))
    8.30 -          in (((var, [var]), map single pats), ctxt') end
    8.31 -      | SOME (f, argss) =>
    8.32 -          let
    8.33 -            val (((def_pats, def_frees), case_patss), ctxt') =
    8.34 -              split_pats single_ctrs argss ctxt
    8.35 -            val def_pat = list_comb (f, def_pats)
    8.36 -          in (((def_pat, flat def_frees), case_patss), ctxt') end
    8.37 -  and
    8.38 -      split_pats single_ctrs patss ctxt =
    8.39 -        let
    8.40 -          val (splitted, ctxt') = fold_map (split_pat single_ctrs) (transpose patss) ctxt
    8.41 -          val r = splitted |> split_list |> apfst split_list |> apsnd (transpose #> map flat)
    8.42 -        in (r, ctxt') end
    8.43 -
    8.44 -(*
    8.45 -  Takes a list lhss of left hand sides (which are lists of patterns)
    8.46 -  and a list rhss of right hand sides. Returns
    8.47 -    - a single equation with a (nested) case-expression on the rhs
    8.48 -    - a list of all split-thms needed to split the rhs
    8.49 -  Patterns which have the same outer context in all lhss remain
    8.50 -  on the lhs of the computed equation.
    8.51 -*)
    8.52 -fun build_case_t fun_t lhss rhss ctxt =
    8.53 -  let
    8.54 -    val single_ctrs =
    8.55 -      get_type_infos ctxt (map fastype_of (flat lhss))
    8.56 -      |> map_filter (fn ti => case #ctrs ti of [Const (name, _)] => SOME name | _ => NONE)
    8.57 -    val (((def_pats, def_frees), case_patss), ctxt') =
    8.58 -      split_pats single_ctrs lhss ctxt
    8.59 -    val pattern = map HOLogic.mk_tuple case_patss
    8.60 -    val case_arg = HOLogic.mk_tuple (flat def_frees)
    8.61 -    val cases = Case_Translation.make_case ctxt' Case_Translation.Warning Name.context
    8.62 -      case_arg (pattern ~~ rhss)
    8.63 -    val split_thms = get_split_ths ctxt' [fastype_of case_arg]
    8.64 -    val t = (list_comb (fun_t, def_pats), cases)
    8.65 -      |> HOLogic.mk_eq
    8.66 -      |> HOLogic.mk_Trueprop
    8.67 -  in ((t, split_thms), ctxt') end
    8.68 -
    8.69 -fun tac ctxt {splits, intros, defs} =
    8.70 -  let val ctxt' = Classical.addSIs (ctxt, intros) in
    8.71 -    REPEAT_DETERM1 (FIRSTGOAL (split_tac ctxt splits))
    8.72 -    THEN Local_Defs.unfold_tac ctxt defs
    8.73 -    THEN safe_tac ctxt'
    8.74 -  end
    8.75 -
    8.76 -fun import [] ctxt = ([], ctxt)
    8.77 -  | import (thm :: thms) ctxt =
    8.78 -    let
    8.79 -      val fun_ct = strip_eq #> fst #> strip_comb #> fst #> Logic.mk_term
    8.80 -        #> Thm.cterm_of ctxt
    8.81 -      val ct = fun_ct thm
    8.82 -      val cts = map fun_ct thms
    8.83 -      val pairs = map (fn s => (s,ct)) cts
    8.84 -      val thms' = map (fn (th,p) => Thm.instantiate (Thm.match p) th) (thms ~~ pairs)
    8.85 -    in Variable.import true (thm :: thms') ctxt |> apfst snd end
    8.86 -
    8.87 -in
    8.88 -
    8.89  (*
    8.90    For a list
    8.91      f p_11 ... p_1n = t1
    8.92 @@ -122,39 +40,24 @@
    8.93    of theorems, prove a single theorem
    8.94      f x1 ... xn = t
    8.95    where t is a (nested) case expression. f must not be a function
    8.96 -  application. Moreover, the terms p_11, ..., p_mn must be non-overlapping
    8.97 -  datatype patterns. The patterns must be exhausting up to common constructor
    8.98 -  contexts.
    8.99 +  application.
   8.100  *)
   8.101  fun to_case ctxt ths =
   8.102    let
   8.103 -    val (iths, ctxt') = import ths ctxt
   8.104 -    val fun_t = hd iths |> strip_eq |> fst |> head_of
   8.105 -    val eqs = map (strip_eq #> apfst (snd o strip_comb)) iths
   8.106 -
   8.107 -    fun hide_rhs ((pat, rhs), name) lthy =
   8.108 +    fun ctr_count (ctr, T) = 
   8.109        let
   8.110 -        val frees = fold Term.add_frees pat []
   8.111 -        val abs_rhs = fold absfree frees rhs
   8.112 -        val ([(f, (_, def))], lthy') = lthy
   8.113 -          |> Local_Defs.define [((Binding.name name, NoSyn), (Binding.empty_atts, abs_rhs))]
   8.114 -      in ((list_comb (f, map Free (rev frees)), def), lthy') end
   8.115 -
   8.116 -    val ((def_ts, def_thms), ctxt2) =
   8.117 -      let val names = Name.invent (Variable.names_of ctxt') "rhs" (length eqs)
   8.118 -      in fold_map hide_rhs (eqs ~~ names) ctxt' |> apfst split_list end
   8.119 -
   8.120 -    val ((t, split_thms), ctxt3) = build_case_t fun_t (map fst eqs) def_ts ctxt2
   8.121 -
   8.122 -    val th = Goal.prove ctxt3 [] [] t (fn {context=ctxt, ...} =>
   8.123 -          tac ctxt {splits=split_thms, intros=ths, defs=def_thms})
   8.124 -  in th
   8.125 -    |> singleton (Proof_Context.export ctxt3 ctxt)
   8.126 -    |> Goal.norm_result ctxt
   8.127 +        val tyco = body_type T |> dest_Type |> fst
   8.128 +        val info = Ctr_Sugar.ctr_sugar_of ctxt tyco
   8.129 +        val _ = if is_none info then error ("Pattern match on non-constructor constant " ^ ctr) else ()
   8.130 +      in
   8.131 +        info |> the |> #ctrs |> length
   8.132 +      end
   8.133 +    val thms = Case_Converter.to_case ctxt Case_Converter.keep_constructor_context ctr_count ths
   8.134 +  in
   8.135 +    case thms of SOME thms => hd thms
   8.136 +      | _ => error ("Conversion to case expression failed.")
   8.137    end
   8.138  
   8.139 -end
   8.140 -
   8.141  local
   8.142  
   8.143  fun was_split t =
     9.1 --- a/src/HOL/ex/Simps_Case_Conv_Examples.thy	Tue Jan 01 13:26:37 2019 +0100
     9.2 +++ b/src/HOL/ex/Simps_Case_Conv_Examples.thy	Tue Jan 01 18:33:19 2019 +0100
     9.3 @@ -30,27 +30,23 @@
     9.4  case_of_simps foo_cases1: foo.simps
     9.5  lemma
     9.6    fixes xs :: "'a list" and ys :: "'b list"
     9.7 -  shows "foo xs ys = (case (xs, ys) of
     9.8 -    ( [], []) \<Rightarrow> 3
     9.9 -    | ([], y # ys) \<Rightarrow> 1
    9.10 -    | (x # xs, []) \<Rightarrow> 0
    9.11 -    | (x # xs, y # ys) \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list))"
    9.12 +  shows "foo xs ys = 
    9.13 +   (case xs of [] \<Rightarrow> (case ys of [] \<Rightarrow> 3 | _ # _ \<Rightarrow> 1)
    9.14 +    | _ # _ \<Rightarrow> (case ys of [] \<Rightarrow> 0 | _ # _ \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list)))"
    9.15    by (fact foo_cases1)
    9.16  
    9.17  text \<open>Redundant equations are ignored\<close>
    9.18  case_of_simps foo_cases2: foo.simps foo.simps
    9.19  lemma
    9.20    fixes xs :: "'a list" and ys :: "'b list"
    9.21 -  shows "foo xs ys = (case (xs, ys) of
    9.22 -    ( [], []) \<Rightarrow> 3
    9.23 -    | ([], y # ys) \<Rightarrow> 1
    9.24 -    | (x # xs, []) \<Rightarrow> 0
    9.25 -    | (x # xs, y # ys) \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list))"
    9.26 +  shows "foo xs ys = 
    9.27 +   (case xs of [] \<Rightarrow> (case ys of [] \<Rightarrow> 3 | _ # _ \<Rightarrow> 1)
    9.28 +    | _ # _ \<Rightarrow> (case ys of [] \<Rightarrow> 0 | _ # _ \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list)))"
    9.29    by (fact foo_cases2)
    9.30  
    9.31  text \<open>Variable patterns\<close>
    9.32  case_of_simps bar_cases: bar.simps
    9.33 -print_theorems
    9.34 +lemma "bar x n y = (case n of 0 \<Rightarrow> 0 + x | Suc n' \<Rightarrow> n' + x)" by(fact bar_cases)
    9.35  
    9.36  text \<open>Case expression not at top level\<close>
    9.37  simps_of_case split_rule_test_simps: split_rule_test_def
    9.38 @@ -96,24 +92,23 @@
    9.39  text \<open>Reversal\<close>
    9.40  case_of_simps test_def1: test_simps1
    9.41  lemma
    9.42 -  "test x y = (case (x,y) of
    9.43 -    (None, []) \<Rightarrow> 1
    9.44 -  | (None, _#_) \<Rightarrow> 2
    9.45 -  | (Some x, _) \<Rightarrow> x)"
    9.46 +  "test x y = 
    9.47 +   (case x of None \<Rightarrow> (case y of [] \<Rightarrow> 1 | _ # _ \<Rightarrow> 2)
    9.48 +    | Some x' \<Rightarrow> x')"
    9.49    by (fact test_def1)
    9.50  
    9.51  text \<open>Case expressions on RHS\<close>
    9.52  case_of_simps test_def2: test_simps2
    9.53 -lemma "test xs y = (case (xs, y) of (None, []) \<Rightarrow> 1 | (None, x # xa) \<Rightarrow> 2 | (Some x, y) \<Rightarrow> x)"
    9.54 +lemma "test x y = 
    9.55 +  (case x of None \<Rightarrow> (case y of [] \<Rightarrow> 1 | _ # _ \<Rightarrow> 2)
    9.56 +   | Some x' \<Rightarrow> x')"
    9.57    by (fact test_def2)
    9.58  
    9.59  text \<open>Partial split of simps\<close>
    9.60  case_of_simps foo_cons_def: foo.simps(1,2)
    9.61  lemma
    9.62    fixes xs :: "'a list" and ys :: "'b list"
    9.63 -  shows "foo (x # xs) ys = (case (x,xs,ys) of
    9.64 -      (_,_,[]) \<Rightarrow> 0
    9.65 -    | (_,_,_ # _) \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list))"
    9.66 +  shows "foo (x # xs) ys = (case ys of [] \<Rightarrow> 0 | _ # _ \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list))"
    9.67    by (fact foo_cons_def)
    9.68  
    9.69  end