merged

--- a/src/HOL/Auth/Event.thy	Thu Sep 05 23:14:28 2013 +0200
+++ b/src/HOL/Auth/Event.thy	Fri Sep 06 10:57:27 2013 +0200
@@ -48,7 +48,6 @@
              if A'=A then insert X (knows A evs) else knows A evs
          | Notes A' X    => 
              if A'=A then insert X (knows A evs) else knows A evs))"
-
 (*
   Case A=Spy on the Gets event
   enforces the fact that if a message is received then it must have been sent,
@@ -153,17 +152,6 @@
 
 subsection{*Knowledge of Agents*}
 
-lemma knows_Says: "knows A (Says A B X # evs) = insert X (knows A evs)"
-by simp
-
-lemma knows_Notes: "knows A (Notes A X # evs) = insert X (knows A evs)"
-by simp
-
-lemma knows_Gets:
-     "A \<noteq> Spy --> knows A (Gets A X # evs) = insert X (knows A evs)"
-by simp
-
-
 lemma knows_subset_knows_Says: "knows A evs \<subseteq> knows A (Says A' B X # evs)"
 by (simp add: subset_insertI)
 
@@ -260,7 +248,7 @@
 
 
 lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
-by (induct e, auto simp: knows_Cons)
+by (cases e, auto simp: knows_Cons)
 
 lemma initState_subset_knows: "initState A \<subseteq> knows A evs"
 apply (induct_tac evs, simp) 

--- a/src/HOL/Auth/Shared.thy	Thu Sep 05 23:14:28 2013 +0200
+++ b/src/HOL/Auth/Shared.thy	Fri Sep 06 10:57:27 2013 +0200
@@ -251,6 +251,6 @@
     "for proving possibility theorems"
 
 lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)"
-by (induct e) (auto simp: knows_Cons)
+by (cases e) (auto simp: knows_Cons)
 
 end

--- a/src/HOL/Auth/Smartcard/EventSC.thy	Thu Sep 05 23:14:28 2013 +0200
+++ b/src/HOL/Auth/Smartcard/EventSC.thy	Fri Sep 06 10:57:27 2013 +0200
@@ -1,6 +1,10 @@
 header{*Theory of Events for Security Protocols that use smartcards*}
 
-theory EventSC imports "../Message" begin
+theory EventSC
+imports
+  "../Message"
+  "~~/src/HOL/Library/Simps_Case_Conv"
+begin
 
 consts  (*Initial states of agents -- parameter of the construction*)
   initState :: "agent => msg set"
@@ -46,7 +50,6 @@
   Card_Spy_not_cloned    [iff]: "Card Spy \<notin> cloned"
   apply blast done
 
-
 primrec (*This definition is extended over the new events, subject to the 
           assumption of secure means*)
   knows   :: "agent => event list => msg set" (*agents' knowledge*) where
@@ -244,16 +247,6 @@
 
 subsection{*Knowledge of Agents*}
 
-lemma knows_Says: "knows A (Says A B X # evs) = insert X (knows A evs)"
-by simp
-
-lemma knows_Notes: "knows A (Notes A X # evs) = insert X (knows A evs)"
-by simp
-
-lemma knows_Gets:
-      "A \<noteq> Spy \<longrightarrow> knows A (Gets A X # evs) = insert X (knows A evs)"
-by simp
-
 lemma knows_Inputs: "knows A (Inputs A C X # evs) = insert X (knows A evs)"
 by simp
 
@@ -346,7 +339,7 @@
 
 lemma parts_knows_Spy_subset_used: "parts (knows Spy evs) \<subseteq> used evs"
 apply (induct_tac "evs", force)  
-apply (simp add: parts_insert_knows_A knows_Cons add: event.split, blast) 
+apply (simp add: parts_insert_knows_A add: event.split, blast)
 done
 
 lemmas usedI = parts_knows_Spy_subset_used [THEN subsetD, intro]
@@ -356,26 +349,7 @@
 apply (simp_all add: parts_insert_knows_A split add: event.split, blast)
 done
 
-lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} \<union> used evs"
-by simp
-
-lemma used_Notes [simp]: "used (Notes A X # evs) = parts{X} \<union> used evs"
-by simp
-
-lemma used_Gets [simp]: "used (Gets A X # evs) = used evs"
-by simp
-
-lemma used_Inputs [simp]: "used (Inputs A C X # evs) = parts{X} \<union> used evs"
-by simp
-
-lemma used_C_Gets [simp]: "used (C_Gets C X # evs) = used evs"
-by simp
-
-lemma used_Outpts [simp]: "used (Outpts C A X # evs) = parts{X} \<union> used evs"
-by simp
-
-lemma used_A_Gets [simp]: "used (A_Gets A X # evs) = used evs"
-by simp
+simps_of_case used_Cons_simps[simp]: used_Cons
 
 lemma used_nil_subset: "used [] \<subseteq> used evs"
 apply simp
@@ -422,7 +396,7 @@
 
 
 lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
-by (induct e, auto simp: knows_Cons)
+by (cases e, auto simp: knows_Cons)
 
 lemma initState_subset_knows: "initState A \<subseteq> knows A evs"
 apply (induct_tac evs, simp) 

--- a/src/HOL/Auth/Smartcard/Smartcard.thy	Thu Sep 05 23:14:28 2013 +0200
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Fri Sep 06 10:57:27 2013 +0200
@@ -370,8 +370,7 @@
 fun possibility_tac ctxt =
    (REPEAT 
     (ALLGOALS (simp_tac (ctxt
-      delsimps [@{thm used_Says}, @{thm used_Notes}, @{thm used_Gets},
-        @{thm used_Inputs}, @{thm used_C_Gets}, @{thm used_Outpts}, @{thm used_A_Gets}]
+      delsimps @{thms used_Cons_simps}
       setSolver safe_solver))
      THEN
      REPEAT_FIRST (eq_assume_tac ORELSE' 

--- a/src/HOL/IMP/Abs_Int2_ivl.thy	Thu Sep 05 23:14:28 2013 +0200
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Fri Sep 06 10:57:27 2013 +0200
@@ -55,7 +55,7 @@
 
 lift_definition  is_empty_ivl :: "ivl \<Rightarrow> bool" is is_empty_rep
 apply(auto simp: eq_ivl_def \<gamma>_rep_cases is_empty_rep_def)
-apply(auto simp: not_less less_eq_extended_cases split: extended.splits)
+apply(auto simp: not_less less_eq_extended_case split: extended.splits)
 done
 
 lemma eq_ivl_iff: "eq_ivl p1 p2 = (is_empty_rep p1 & is_empty_rep p2 | p1 = p2)"

--- a/src/HOL/Library/Extended.thy	Thu Sep 05 23:14:28 2013 +0200
+++ b/src/HOL/Library/Extended.thy	Fri Sep 06 10:57:27 2013 +0200
@@ -5,14 +5,13 @@
 *)
 
 theory Extended
-imports Main
+imports
+  Main
+  "~~/src/HOL/Library/Simps_Case_Conv"
 begin
 
 datatype 'a extended = Fin 'a | Pinf ("\<infinity>") | Minf ("-\<infinity>")
 
-lemmas extended_cases2 = extended.exhaust[case_product extended.exhaust]
-lemmas extended_cases3 = extended.exhaust[case_product extended_cases2]
-
 
 instantiation extended :: (order)order
 begin
@@ -23,31 +22,18 @@
 "Minf  \<le> _     = True" |
 "(_::'a extended) \<le> _     = False"
 
-lemma less_eq_extended_cases:
-  "x \<le> y = (case x of Fin x \<Rightarrow> (case y of Fin y \<Rightarrow> x \<le> y | Pinf \<Rightarrow> True | Minf \<Rightarrow> False)
-            | Pinf \<Rightarrow> y=Pinf | Minf \<Rightarrow> True)"
-by(induct x y rule: less_eq_extended.induct)(auto split: extended.split)
+case_of_simps less_eq_extended_case: less_eq_extended.simps
 
 definition less_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> bool" where
 "((x::'a extended) < y) = (x \<le> y & \<not> x \<ge> y)"
 
 instance
-proof
-  case goal1 show ?case by(rule less_extended_def)
-next
-  case goal2 show ?case by(cases x) auto
-next
-  case goal3 thus ?case by(auto simp: less_eq_extended_cases split:extended.splits)
-next
-  case goal4 thus ?case by(auto simp: less_eq_extended_cases split:extended.splits)
-qed
+  by intro_classes (auto simp: less_extended_def less_eq_extended_case split: extended.splits)
 
 end
 
 instance extended :: (linorder)linorder
-proof
-  case goal1 thus ?case by(auto simp: less_eq_extended_cases split:extended.splits)
-qed
+  by intro_classes (auto simp: less_eq_extended_case split:extended.splits)
 
 lemma Minf_le[simp]: "Minf \<le> y"
 by(cases y) auto
@@ -114,26 +100,19 @@
 "Minf  + Pinf  = Pinf" |
 "Pinf  + Minf  = Pinf"
 
+case_of_simps plus_case: plus_extended.simps
+
 instance ..
 
 end
 
 
+
 instance extended :: (ab_semigroup_add)ab_semigroup_add
-proof
-  fix a b c :: "'a extended"
-  show "a + b = b + a"
-    by (induct a b rule: plus_extended.induct) (simp_all add: ac_simps)
-  show "a + b + c = a + (b + c)"
-    by (cases rule: extended_cases3[of a b c]) (simp_all add: ac_simps)
-qed
+  by intro_classes (simp_all add: ac_simps plus_case split: extended.splits)
 
 instance extended :: (ordered_ab_semigroup_add)ordered_ab_semigroup_add
-proof
-  fix a b c :: "'a extended"
-  assume "a \<le> b" then show "c + a \<le> c + b"
-    by (cases rule: extended_cases3[of a b c]) (auto simp: add_left_mono)
-qed
+  by intro_classes (auto simp: add_left_mono plus_case split: extended.splits)
 
 instance extended :: (comm_monoid_add)comm_monoid_add
 proof
@@ -206,16 +185,12 @@
 "sup_extended Minf a = a" |
 "sup_extended a Minf = a"
 
+case_of_simps inf_extended_case: inf_extended.simps
+case_of_simps sup_extended_case: sup_extended.simps
+
 instance
-proof
-  fix x y z ::"'a extended"
-  show "inf x y \<le> x" "inf x y \<le> y" "\<lbrakk>x \<le> y; x \<le> z\<rbrakk> \<Longrightarrow> x \<le> inf y z"
-    "x \<le> sup x y" "y \<le> sup x y" "\<lbrakk>y \<le> x; z \<le> x\<rbrakk> \<Longrightarrow> sup y z \<le> x" "bot \<le> x" "x \<le> top"
-    apply (atomize (full))
-    apply (cases rule: extended_cases3[of x y z])
-    apply (auto simp: bot_extended_def top_extended_def)
-    done
-qed
+  by (intro_classes) (auto simp: inf_extended_case sup_extended_case less_eq_extended_case
+    bot_extended_def top_extended_def split: extended.splits)
 end
 
 end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Simps_Case_Conv.thy	Fri Sep 06 10:57:27 2013 +0200
@@ -0,0 +1,12 @@
+(*  Title:    HOL/Library/Simps_Case_Conv.thy
+    Author:   Lars Noschinski
+*)
+
+theory Simps_Case_Conv
+  imports Main
+  keywords "simps_of_case" "case_of_simps" :: thy_decl
+begin
+
+ML_file "simps_case_conv.ML"
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/simps_case_conv.ML	Fri Sep 06 10:57:27 2013 +0200
@@ -0,0 +1,239 @@
+(*  Title:      HOL/Library/simps_case_conv.ML
+    Author:     Lars Noschinski, TU Muenchen
+                Gerwin Klein, NICTA
+
+  Converts function specifications between the representation as
+  a list of equations (with patterns on the lhs) and a single
+  equation (with a nested case expression on the rhs).
+*)
+
+signature SIMPS_CASE_CONV =
+sig
+  val to_case: Proof.context -> thm list -> thm
+  val gen_to_simps: Proof.context -> thm list -> thm -> thm list
+  val to_simps: Proof.context -> thm -> thm list
+end
+
+structure Simps_Case_Conv: SIMPS_CASE_CONV =
+struct
+
+(* Collects all type constructors in a type *)
+fun collect_Tcons (Type (name,Ts)) = name :: maps collect_Tcons Ts
+  | collect_Tcons (TFree _) = []
+  | collect_Tcons (TVar _) = []
+
+fun get_split_ths thy = collect_Tcons
+    #> distinct (op =)
+    #> map_filter (Datatype_Data.get_info thy)
+    #> map #split
+
+val strip_eq = prop_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq
+
+
+local
+
+  fun transpose [] = []
+    | transpose ([] :: xss) = transpose xss
+    | transpose xss = map hd xss :: transpose (map tl xss);
+
+  fun same_fun (ts as _ $ _ :: _) =
+      let
+        val (fs, argss) = map strip_comb ts |> split_list
+        val f = hd fs
+      in if forall (fn x => f = x) fs then SOME (f, argss) else NONE end
+    | same_fun _ = NONE
+
+  (* pats must be non-empty *)
+  fun split_pat pats ctxt =
+      case same_fun pats of
+        NONE =>
+          let
+            val (name, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt
+            val var = Free (name, fastype_of (hd pats))
+          in (((var, [var]), map single pats), ctxt') end
+      | SOME (f, argss) =>
+          let
+            val (((def_pats, def_frees), case_patss), ctxt') =
+              split_pats argss ctxt
+            val def_pat = list_comb (f, def_pats)
+          in (((def_pat, flat def_frees), case_patss), ctxt') end
+  and
+      split_pats patss ctxt =
+        let
+          val (splitted, ctxt') = fold_map split_pat (transpose patss) ctxt
+          val r = splitted |> split_list |> apfst split_list |> apsnd (transpose #> map flat)
+        in (r, ctxt') end
+
+(*
+  Takes a list lhss of left hand sides (which are lists of patterns)
+  and a list rhss of right hand sides. Returns
+    - a single equation with a (nested) case-expression on the rhs
+    - a list of all split-thms needed to split the rhs
+  Patterns which have the same outer context in all lhss remain
+  on the lhs of the computed equation.
+*)
+fun build_case_t fun_t lhss rhss ctxt =
+  let
+    val (((def_pats, def_frees), case_patss), ctxt') =
+      split_pats lhss ctxt
+    val pattern = map HOLogic.mk_tuple case_patss
+    val case_arg = HOLogic.mk_tuple (flat def_frees)
+    val cases = Case_Translation.make_case ctxt' Case_Translation.Warning Name.context
+      case_arg (pattern ~~ rhss)
+    val split_thms = get_split_ths (Proof_Context.theory_of ctxt') (fastype_of case_arg)
+    val t = (list_comb (fun_t, def_pats), cases)
+      |> HOLogic.mk_eq
+      |> HOLogic.mk_Trueprop
+  in ((t, split_thms), ctxt') end
+
+fun tac ctxt {splits, intros, defs} =
+  let val ctxt' = Classical.addSIs (ctxt, intros) in
+    REPEAT_DETERM1 (FIRSTGOAL (split_tac splits))
+    THEN Local_Defs.unfold_tac ctxt defs
+    THEN safe_tac ctxt'
+  end
+
+fun import [] ctxt = ([], ctxt)
+  | import (thm :: thms) ctxt =
+    let
+      val fun_ct = strip_eq #> fst #> strip_comb #> fst #> Logic.mk_term
+        #> Thm.cterm_of (Proof_Context.theory_of ctxt)
+      val ct = fun_ct thm
+      val cts = map fun_ct thms
+      val pairs = map (fn s => (s,ct)) cts
+      val thms' = map (fn (th,p) => Thm.instantiate (Thm.match p) th) (thms ~~ pairs)
+    in Variable.import true (thm :: thms') ctxt |> apfst snd end
+
+in
+
+(*
+  For a list
+    f p_11 ... p_1n = t1
+    f p_21 ... p_2n = t2
+    ...
+    f p_mn ... p_mn = tm
+  of theorems, prove a single theorem
+    f x1 ... xn = t
+  where t is a (nested) case expression. f must not be a function
+  application. Moreover, the terms p_11, ..., p_mn must be non-overlapping
+  datatype patterns. The patterns must be exhausting up to common constructor
+  contexts.
+*)
+fun to_case ctxt ths =
+  let
+    val (iths, ctxt') = import ths ctxt
+    val fun_t = hd iths |> strip_eq |> fst |> head_of
+    val eqs = map (strip_eq #> apfst (snd o strip_comb)) iths
+
+    fun hide_rhs ((pat, rhs), name) lthy = let
+        val frees = fold Term.add_frees pat []
+        val abs_rhs = fold absfree frees rhs
+        val ((f,def), lthy') = Local_Defs.add_def
+          ((Binding.name name, Mixfix.NoSyn), abs_rhs) lthy
+      in ((list_comb (f, map Free (rev frees)), def), lthy') end
+
+    val ((def_ts, def_thms), ctxt2) = let
+        val nctxt = Variable.names_of ctxt'
+        val names = Name.invent nctxt "rhs" (length eqs)
+      in fold_map hide_rhs (eqs ~~ names) ctxt' |> apfst split_list end
+
+    val ((t, split_thms), ctxt3) = build_case_t fun_t (map fst eqs) def_ts ctxt2
+
+    val th = Goal.prove ctxt3 [] [] t (fn {context=ctxt, ...} =>
+          tac ctxt {splits=split_thms, intros=ths, defs=def_thms})
+  in th
+    |> singleton (Proof_Context.export ctxt3 ctxt)
+    |> Goal.norm_result
+  end
+
+end
+
+local
+
+fun was_split t =
+  let
+    val is_free_eq_imp = is_Free o fst o HOLogic.dest_eq
+              o fst o HOLogic.dest_imp
+    val get_conjs = HOLogic.dest_conj o HOLogic.dest_Trueprop
+    fun dest_alls (Const ("HOL.All", _) $ Abs (_, _, t)) = dest_alls t
+      | dest_alls t = t
+  in forall (is_free_eq_imp o dest_alls) (get_conjs t) end
+        handle TERM _ => false
+
+fun apply_split ctxt split thm = Seq.of_list
+  let val ((_,thm'), ctxt') = Variable.import false [thm] ctxt in
+    (Variable.export ctxt' ctxt) (filter (was_split o prop_of) (thm' RL [split]))
+  end
+
+fun forward_tac rules t = Seq.of_list ([t] RL rules)
+
+val refl_imp = refl RSN (2, mp)
+
+val get_rules_once_split =
+  REPEAT (forward_tac [conjunct1, conjunct2])
+    THEN REPEAT (forward_tac [spec])
+    THEN (forward_tac [refl_imp])
+
+fun do_split ctxt split =
+  let
+    val split' = split RS iffD1;
+    val split_rhs = concl_of (hd (snd (fst (Variable.import false [split'] ctxt))))
+  in if was_split split_rhs
+     then DETERM (apply_split ctxt split') THEN get_rules_once_split
+     else raise TERM ("malformed split rule", [split_rhs])
+  end
+
+val atomize_meta_eq = forward_tac [meta_eq_to_obj_eq]
+
+in
+
+fun gen_to_simps ctxt splitthms thm =
+  Seq.list_of ((TRY atomize_meta_eq
+                 THEN (REPEAT (FIRST (map (do_split ctxt) splitthms)))) thm)
+
+fun to_simps ctxt thm =
+  let
+    val T = thm |> strip_eq |> fst |> strip_comb |> fst |> fastype_of
+    val splitthms = get_split_ths (Proof_Context.theory_of ctxt) T
+  in gen_to_simps ctxt splitthms thm end
+
+
+end
+
+fun case_of_simps_cmd (bind, thms_ref) lthy =
+  let
+    val thy = Proof_Context.theory_of lthy
+    val bind' = apsnd (map (Attrib.intern_src thy)) bind
+    val thm = (Attrib.eval_thms lthy) thms_ref |> to_case lthy
+  in
+    Local_Theory.note (bind', [thm]) lthy |> snd
+  end
+
+fun simps_of_case_cmd ((bind, thm_ref), splits_ref) lthy =
+  let
+    val thy = Proof_Context.theory_of lthy
+    val bind' = apsnd (map (Attrib.intern_src thy)) bind
+    val thm = singleton (Attrib.eval_thms lthy) thm_ref
+    val simps = if null splits_ref
+      then to_simps lthy thm
+      else gen_to_simps lthy (Attrib.eval_thms lthy splits_ref) thm
+  in
+    Local_Theory.note (bind', simps) lthy |> snd
+  end
+
+val _ =
+  Outer_Syntax.local_theory @{command_spec "case_of_simps"}
+    "turns a list of equations into a case expression"
+    (Parse_Spec.opt_thm_name ":"  -- Parse_Spec.xthms1 >> case_of_simps_cmd)
+
+val parse_splits = @{keyword "("} |-- Parse.reserved "splits" |-- @{keyword ":"} |--
+  Parse_Spec.xthms1 --| @{keyword ")"}
+
+val _ =
+  Outer_Syntax.local_theory @{command_spec "simps_of_case"}
+    "perform case split on rule"
+    (Parse_Spec.opt_thm_name ":"  -- Parse_Spec.xthm --
+      Scan.optional parse_splits [] >> simps_of_case_cmd)
+
+end
+

--- a/src/HOL/ROOT	Thu Sep 05 23:14:28 2013 +0200
+++ b/src/HOL/ROOT	Fri Sep 06 10:57:27 2013 +0200
@@ -559,6 +559,7 @@
     Parallel_Example
     IArray_Examples
     SVC_Oracle
+    Simps_Case_Conv_Examples
   theories [skip_proofs = false]
     Meson_Test
   theories [condition = SVC_HOME]

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Simps_Case_Conv_Examples.thy	Fri Sep 06 10:57:27 2013 +0200
@@ -0,0 +1,71 @@
+theory Simps_Case_Conv_Examples imports
+  "~~/src/HOL/Library/Simps_Case_Conv"
+begin
+
+section {* Tests for the Simps<->Case conversion tools *}
+
+fun foo where
+  "foo (x # xs) Nil = 0" |
+  "foo (x # xs) (y # ys) = foo [] []" |
+  "foo Nil (y # ys) = 1" |
+  "foo Nil Nil = 3"
+
+fun bar where
+  "bar x 0 y = 0 + x" |
+  "bar x (Suc n) y = n + x"
+
+definition
+  split_rule_test :: "((nat => 'a) + ('b * (('b => 'a) option))) => ('a => nat) => nat"
+where
+ "split_rule_test x f = f (case x of Inl af \<Rightarrow> af 1
+    | Inr (b, None) => inv f 0
+    | Inr (b, Some g) => g b)"
+
+definition test where "test x y = (case x of None => (case y of [] => 1 | _ # _ => 2) | Some x => x)"
+
+definition nosplit where "nosplit x = x @ (case x of [] \<Rightarrow> [1] | xs \<Rightarrow> xs)"
+
+
+text {* Function with complete, non-overlapping patterns *}
+case_of_simps foo_cases1: foo.simps
+
+text {* Redundant equations are ignored *}
+case_of_simps foo_cases2: foo.simps foo.simps
+print_theorems
+
+text {* Variable patterns *}
+case_of_simps bar_cases: bar.simps
+print_theorems
+
+text {* Case expression not at top level *}
+simps_of_case split_rule_test_simps: split_rule_test_def
+print_theorems
+
+text {* Argument occurs both as case parameter and seperately*}
+simps_of_case nosplit_simps1: nosplit_def
+print_theorems
+
+text {* Nested case expressions *}
+simps_of_case test_simps1: test_def
+print_theorems
+
+text {* Partial split of case *}
+simps_of_case nosplit_simps2: nosplit_def (splits: list.split)
+print_theorems
+simps_of_case test_simps2: test_def (splits: option.split)
+print_theorems
+
+text {* Reversal *}
+case_of_simps test_def1: test_simps1
+print_theorems
+
+text {* Case expressions on RHS *}
+case_of_simps test_def2: test_simps2
+print_theorems
+
+text {* Partial split of simps *}
+case_of_simps foo_cons_def: foo.simps(1,2)
+print_theorems
+
+
+end