# HG changeset patch
# User haftmann
# Date 1166705711 -3600
# Node ID b4e4ea3db161f2732f8f83e9547a20222955c234
# Parent  3fb9762ba7017bd53e63258d57bca847a93af24d
added code lemmas for quantification over bounded nats

diff -r 3fb9762ba701 -r b4e4ea3db161 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Dec 21 08:42:53 2006 +0100
+++ b/src/HOL/List.thy	Thu Dec 21 13:55:11 2006 +0100
@@ -2730,4 +2730,56 @@
   "rev xs == itrev xs []"
   by simp
 
+text {* code for bounded quantification over nats *}
+
+lemma atMost_upto [code inline]:
+  "{..n} = set [0..n]"
+  by auto
+lemmas atMost_upto' [code unfold] = atMost_upto [THEN eq_reflection]
+
+lemma atLeast_upt [code inline]:
+  "{..<n} = set [0..<n]"
+  by auto
+lemmas atLeast_upt' [code unfold] = atLeast_upt [THEN eq_reflection]
+
+lemma greaterThanLessThan_upd [code inline]:
+  "{n<..<m} = set [Suc n..<m]"
+  by auto
+lemmas greaterThanLessThan_upd' [code unfold] = greaterThanLessThan_upd [THEN eq_reflection]
+
+lemma atLeastLessThan_upd [code inline]:
+  "{n..<m} = set [n..<m]"
+  by auto
+lemmas atLeastLessThan_upd' [code unfold] = atLeastLessThan_upd [THEN eq_reflection]
+
+lemma greaterThanAtMost_upto [code inline]:
+  "{n<..m} = set [Suc n..m]"
+  by auto
+lemmas greaterThanAtMost_upto' [code unfold] = greaterThanAtMost_upto [THEN eq_reflection]
+
+lemma atLeastAtMost_upto [code inline]:
+  "{n..m} = set [n..m]"
+  by auto
+lemmas atLeastAtMost_upto' [code unfold] = atLeastAtMost_upto [THEN eq_reflection]
+
+lemma all_nat_less_eq [code inline]:
+  "(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
+  by auto
+lemmas all_nat_less_eq' [code unfold] = all_nat_less_eq [THEN eq_reflection]
+
+lemma ex_nat_less_eq [code inline]:
+  "(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
+  by auto
+lemmas ex_nat_less_eq' [code unfold] = ex_nat_less_eq [THEN eq_reflection]
+
+lemma all_nat_less [code inline]:
+  "(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
+  by auto
+lemmas all_nat_less' [code unfold] =  all_nat_less [THEN eq_reflection]
+
+lemma ex_nat_less [code inline]:
+  "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
+  by auto
+lemmas ex_nat_less' [code unfold] = ex_nat_less [THEN eq_reflection]
+
 end