# HG changeset patch
# User krauss
# Date 1378836593 -7200
# Node ID 437c0a63bb16cbe390b2e913b66dde64859a96e4
# Parent  dde3cc2804cc5b6ef2f9c0039e80d5a6b751e88b
added some examples and tests for fun_cases

diff -r dde3cc2804cc -r 437c0a63bb16 src/HOL/ex/Fundefs.thy
--- a/src/HOL/ex/Fundefs.thy	Mon Sep 09 00:59:45 2013 +0200
+++ b/src/HOL/ex/Fundefs.thy	Tue Sep 10 20:09:53 2013 +0200
@@ -28,6 +28,9 @@
 thm fib.simps
 thm fib.induct
 
+text {* elimination rules *}
+thm fib.elims
+
 subsection {* Currying *}
 
 fun add
@@ -174,6 +177,8 @@
 thm evn_od.induct
 thm evn_od.termination
 
+thm evn.elims
+thm od.elims
 
 subsection {* Definitions in local contexts *}
 
@@ -208,6 +213,74 @@
 thm my_monoid.foldL.simps
 thm my_monoid.foldR_foldL
 
+subsection {* @{text fun_cases} *}
+
+subsubsection {* Predecessor *}
+
+fun pred :: "nat \<Rightarrow> nat" where
+"pred 0 = 0" |
+"pred (Suc n) = n"
+
+thm pred.elims
+
+lemma assumes "pred x = y"
+obtains "x = 0" "y = 0" | "n" where "x = Suc n" "y = n"
+by (fact pred.elims[OF assms])
+
+text {* If the predecessor of a number is 0, that number must be 0 or 1. *}
+
+fun_cases pred0E[elim]: "pred n = 0"
+
+lemma "pred n = 0 \<Longrightarrow> n = 0 \<or> n = Suc 0"
+by (erule pred0E) metis+
+
+
+text {* Other expressions on the right-hand side also work, but whether the
+        generated rule is useful depends on how well the simplifier can
+        simplify it. This example works well: *}
+
+fun_cases pred42E[elim]: "pred n = 42"
+
+lemma "pred n = 42 \<Longrightarrow> n = 43"
+by (erule pred42E)
+
+subsubsection {* List to option *}
+
+fun list_to_option :: "'a list \<Rightarrow> 'a option" where
+"list_to_option [x] = Some x" |
+"list_to_option _ = None"
+
+fun_cases list_to_option_NoneE: "list_to_option xs = None"
+      and list_to_option_SomeE: "list_to_option xs = Some _"
+
+lemma "list_to_option xs = Some y \<Longrightarrow> xs = [y]"
+by (erule list_to_option_SomeE)
+
+subsubsection {* Boolean Functions *}
+
+fun xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
+"xor False False = False" |
+"xor True True = False" |
+"xor _ _ = True"
+
+thm xor.elims
+
+text {* @{text fun_cases} does not only recognise function equations, but also works with
+   functions that return a boolean, e.g.: *}
+
+fun_cases xor_TrueE: "xor a b" and xor_FalseE: "\<not>xor a b"
+print_theorems
+
+subsubsection {* Many parameters *}
+
+fun sum4 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
+"sum4 a b c d = a + b + c + d"
+
+fun_cases sum40E: "sum4 a b c d = 0"
+
+lemma "sum4 a b c d = 0 \<Longrightarrow> a = 0"
+by (erule sum40E)
+
 
 subsection {* Partial Function Definitions *}