src/HOL/Import/HOL4Compat.thy
 changeset 37596 248db70c9bcf parent 35416 d8d7d1b785af child 39246 9e58f0499f57
```     1.1 --- a/src/HOL/Import/HOL4Compat.thy	Mon Jun 28 15:32:06 2010 +0200
1.2 +++ b/src/HOL/Import/HOL4Compat.thy	Mon Jun 28 15:32:08 2010 +0200
1.3 @@ -6,6 +6,7 @@
1.4  imports HOL4Setup Complex_Main "~~/src/HOL/Old_Number_Theory/Primes" ContNotDenum
1.5  begin
1.6
1.7 +abbreviation (input) mem (infixl "mem" 55) where "x mem xs \<equiv> List.member xs x"
1.8  no_notation differentiable (infixl "differentiable" 60)
1.9  no_notation sums (infixr "sums" 80)
1.10
1.11 @@ -326,8 +327,8 @@
1.12    qed
1.13  qed
1.14
1.15 -lemma NULL_DEF: "(null [] = True) & (!h t. null (h # t) = False)"
1.16 -  by simp
1.17 +lemma NULL_DEF: "(List.null [] = True) & (!h t. List.null (h # t) = False)"
1.18 +  by (simp add: null_def)
1.19
1.20  definition sum :: "nat list \<Rightarrow> nat" where
1.21    "sum l == foldr (op +) l 0"
1.22 @@ -347,8 +348,8 @@
1.23  lemma MAP: "(!f. map f [] = []) & (!f h t. map f (h#t) = f h#map f t)"
1.24    by simp
1.25
1.26 -lemma MEM: "(!x. x mem [] = False) & (!x h t. x mem (h#t) = ((x = h) | x mem t))"
1.27 -  by auto
1.28 +lemma MEM: "(!x. List.member [] x = False) & (!x h t. List.member (h#t) x = ((x = h) | List.member t x))"
1.29 +  by (simp add: member_def)
1.30
1.31  lemma FILTER: "(!P. filter P [] = []) & (!P h t.
1.32             filter P (h#t) = (if P h then h#filter P t else filter P t))"
1.33 @@ -373,15 +374,7 @@
1.34  lemma EVERY_DEF: "(!P. list_all P [] = True) & (!P h t. list_all P (h#t) = (P h & list_all P t))"
1.35    by simp
1.36
1.37 -consts
1.38 -  list_exists :: "['a \<Rightarrow> bool,'a list] \<Rightarrow> bool"
1.39 -
1.40 -primrec
1.41 -  list_exists_Nil: "list_exists P Nil = False"
1.42 -  list_exists_Cons: "list_exists P (x#xs) = (if P x then True else list_exists P xs)"
1.43 -
1.44 -lemma list_exists_DEF: "(!P. list_exists P [] = False) &
1.45 -         (!P h t. list_exists P (h#t) = (P h | list_exists P t))"
1.46 +lemma list_exists_DEF: "(!P. list_ex P [] = False) & (!P h t. list_ex P (h#t) = (P h | list_ex P t))"
1.47    by simp
1.48
1.49  consts
```