# HG changeset patch
# User blanchet
# Date 1392190556 -3600
# Node ID 4e79187f847e352d7098158a2900a5004d5ec8e3
# Parent  d5ebe055b599553b76cd0abefc44e47bf3b5ca69
removed trivial 'rec' examples for nonrecursive types (I could also have added the 'old.' prefix in front of the constant names)

diff -r d5ebe055b599 -r 4e79187f847e src/HOL/Nitpick_Examples/Core_Nits.thy
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Wed Feb 12 08:35:56 2014 +0100
@@ -925,18 +925,6 @@
 nitpick [card = 2, expect = none]
 by auto
 
-lemma "bool_rec x y True = x"
-nitpick [card = 2, expect = none]
-by auto
-
-lemma "bool_rec x y False = y"
-nitpick [card = 2, expect = none]
-by auto
-
-lemma "(x\<Colon>bool) = bool_rec x x True"
-nitpick [card = 2, expect = none]
-by auto
-
 lemma "x = (case (x, y) of (x', y') \<Rightarrow> x')"
 nitpick [expect = none]
 sorry
diff -r d5ebe055b599 -r 4e79187f847e src/HOL/Nitpick_Examples/Refute_Nits.thy
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Wed Feb 12 08:35:56 2014 +0100
@@ -519,18 +519,6 @@
 nitpick [expect = genuine]
 oops
 
-lemma "prod_rec f p = f (fst p) (snd p)"
-nitpick [expect = none]
-by (case_tac p) auto
-
-lemma "prod_rec f (a, b) = f a b"
-nitpick [expect = none]
-by auto
-
-lemma "P (prod_rec f x)"
-nitpick [expect = genuine]
-oops
-
 lemma "P (case x of Pair a b \<Rightarrow> f a b)"
 nitpick [expect = genuine]
 oops
@@ -575,15 +563,6 @@
 nitpick [expect = genuine]
 oops
 
-lemma "unit_rec u x = u"
-nitpick [expect = none]
-apply simp
-done
-
-lemma "P (unit_rec u x)"
-nitpick [expect = genuine]
-oops
-
 lemma "P (case x of () \<Rightarrow> u)"
 nitpick [expect = genuine]
 oops
@@ -646,20 +625,6 @@
 nitpick [expect = genuine]
 oops
 
-lemma "sum_rec l r (Inl x) = l x"
-nitpick [expect = none]
-apply simp
-done
-
-lemma "sum_rec l r (Inr x) = r x"
-nitpick [expect = none]
-apply simp
-done
-
-lemma "P (sum_rec l r x)"
-nitpick [expect = genuine]
-oops
-
 lemma "P (case x of Inl a \<Rightarrow> l a | Inr b \<Rightarrow> r b)"
 nitpick [expect = genuine]
 oops
diff -r d5ebe055b599 -r 4e79187f847e src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/ex/Refute_Examples.thy	Wed Feb 12 08:35:56 2014 +0100
@@ -525,14 +525,6 @@
 refute [expect = genuine]
 oops
 
-lemma "unit_rec u x = u"
-refute [expect = none]
-by simp
-
-lemma "P (unit_rec u x)"
-refute [expect = genuine]
-oops
-
 lemma "P (case x of () \<Rightarrow> u)"
 refute [expect = genuine]
 oops
@@ -597,14 +589,6 @@
 refute [expect = genuine]
 oops
 
-lemma "prod_rec p (a, b) = p a b"
-refute [maxsize = 2, expect = none]
-by simp
-
-lemma "P (prod_rec p x)"
-refute [expect = genuine]
-oops
-
 lemma "P (case x of Pair a b \<Rightarrow> p a b)"
 refute [expect = genuine]
 oops
@@ -631,18 +615,6 @@
 refute [expect = genuine]
 oops
 
-lemma "sum_rec l r (Inl x) = l x"
-refute [maxsize = 3, expect = none]
-by simp
-
-lemma "sum_rec l r (Inr x) = r x"
-refute [maxsize = 3, expect = none]
-by simp
-
-lemma "P (sum_rec l r x)"
-refute [expect = genuine]
-oops
-
 lemma "P (case x of Inl a \<Rightarrow> l a | Inr b \<Rightarrow> r b)"
 refute [expect = genuine]
 oops