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