# HG changeset patch
# User haftmann
# Date 1277731928 -7200
# Node ID 248db70c9bcff1ffb777e24ba018d35a4b7e6424
# Parent  9591362629e34d97f24982840cacb97e6165fb5a
dropped ancient infix mem

diff -r 9591362629e3 -r 248db70c9bcf src/HOL/Auth/Guard/Guard.thy
--- a/src/HOL/Auth/Guard/Guard.thy	Mon Jun 28 15:32:06 2010 +0200
+++ b/src/HOL/Auth/Guard/Guard.thy	Mon Jun 28 15:32:08 2010 +0200
@@ -201,14 +201,16 @@
 lemma cnb_app [simp]: "cnb (l @ l') = cnb l + cnb l'"
 by (induct l, auto)
 
-lemma mem_cnb_minus: "x mem l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)"
-by (induct l, auto)
+lemma mem_cnb_minus: "x \<in> set l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)"
+  by (induct l) auto
 
 lemmas mem_cnb_minus_substI = mem_cnb_minus [THEN ssubst]
 
-lemma cnb_minus [simp]: "x mem l ==> cnb (remove l x) = cnb l - crypt_nb x"
+lemma cnb_minus [simp]: "x \<in> set l ==> cnb (remove l x) = cnb l - crypt_nb x"
 apply (induct l, auto)
-by (erule_tac l1=l and x1=x in mem_cnb_minus_substI, simp)
+apply (erule_tac l1=l and x1=x in mem_cnb_minus_substI)
+apply simp
+done
 
 lemma parts_cnb: "Z:parts (set l) ==>
 cnb l = (cnb l - crypt_nb Z) + crypt_nb Z"
@@ -272,7 +274,7 @@
 apply (clarsimp, blast)
 (* K ~:invKey`Ks *)
 apply (subgoal_tac "Guard n Ks (set (decrypt' l' K Y))")
-apply (drule_tac x="decrypt' l' K Y" in spec, simp add: mem_iff)
+apply (drule_tac x="decrypt' l' K Y" in spec, simp)
 apply (subgoal_tac "Crypt K Y:parts (set l)")
 apply (drule parts_cnb, rotate_tac -1, simp)
 apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub)
diff -r 9591362629e3 -r 248db70c9bcf src/HOL/Auth/Guard/GuardK.thy
--- a/src/HOL/Auth/Guard/GuardK.thy	Mon Jun 28 15:32:06 2010 +0200
+++ b/src/HOL/Auth/Guard/GuardK.thy	Mon Jun 28 15:32:08 2010 +0200
@@ -197,12 +197,12 @@
 lemma cnb_app [simp]: "cnb (l @ l') = cnb l + cnb l'"
 by (induct l, auto)
 
-lemma mem_cnb_minus: "x mem l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)"
+lemma mem_cnb_minus: "x \<in> set l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)"
 by (induct l, auto)
 
 lemmas mem_cnb_minus_substI = mem_cnb_minus [THEN ssubst]
 
-lemma cnb_minus [simp]: "x mem l ==> cnb (remove l x) = cnb l - crypt_nb x"
+lemma cnb_minus [simp]: "x \<in> set l ==> cnb (remove l x) = cnb l - crypt_nb x"
 apply (induct l, auto)
 by (erule_tac l1=l and x1=x in mem_cnb_minus_substI, simp)
 
@@ -268,7 +268,7 @@
 apply (clarsimp, blast)
 (* K ~:invKey`Ks *)
 apply (subgoal_tac "GuardK n Ks (set (decrypt' l' K Y))")
-apply (drule_tac x="decrypt' l' K Y" in spec, simp add: mem_iff)
+apply (drule_tac x="decrypt' l' K Y" in spec, simp)
 apply (subgoal_tac "Crypt K Y:parts (set l)")
 apply (drule parts_cnb, rotate_tac -1, simp)
 apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub)
diff -r 9591362629e3 -r 248db70c9bcf src/HOL/Import/HOL4Compat.thy
--- a/src/HOL/Import/HOL4Compat.thy	Mon Jun 28 15:32:06 2010 +0200
+++ b/src/HOL/Import/HOL4Compat.thy	Mon Jun 28 15:32:08 2010 +0200
@@ -6,6 +6,7 @@
 imports HOL4Setup Complex_Main "~~/src/HOL/Old_Number_Theory/Primes" ContNotDenum
 begin
 
+abbreviation (input) mem (infixl "mem" 55) where "x mem xs \<equiv> List.member xs x"
 no_notation differentiable (infixl "differentiable" 60)
 no_notation sums (infixr "sums" 80)
 
@@ -326,8 +327,8 @@
   qed
 qed
 
-lemma NULL_DEF: "(null [] = True) & (!h t. null (h # t) = False)"
-  by simp
+lemma NULL_DEF: "(List.null [] = True) & (!h t. List.null (h # t) = False)"
+  by (simp add: null_def)
 
 definition sum :: "nat list \<Rightarrow> nat" where
   "sum l == foldr (op +) l 0"
@@ -347,8 +348,8 @@
 lemma MAP: "(!f. map f [] = []) & (!f h t. map f (h#t) = f h#map f t)"
   by simp
 
-lemma MEM: "(!x. x mem [] = False) & (!x h t. x mem (h#t) = ((x = h) | x mem t))"
-  by auto
+lemma MEM: "(!x. List.member [] x = False) & (!x h t. List.member (h#t) x = ((x = h) | List.member t x))"
+  by (simp add: member_def)
 
 lemma FILTER: "(!P. filter P [] = []) & (!P h t.
            filter P (h#t) = (if P h then h#filter P t else filter P t))"
@@ -373,15 +374,7 @@
 lemma EVERY_DEF: "(!P. list_all P [] = True) & (!P h t. list_all P (h#t) = (P h & list_all P t))"
   by simp
 
-consts
-  list_exists :: "['a \<Rightarrow> bool,'a list] \<Rightarrow> bool"
-
-primrec
-  list_exists_Nil: "list_exists P Nil = False"
-  list_exists_Cons: "list_exists P (x#xs) = (if P x then True else list_exists P xs)"
-
-lemma list_exists_DEF: "(!P. list_exists P [] = False) &
-         (!P h t. list_exists P (h#t) = (P h | list_exists P t))"
+lemma list_exists_DEF: "(!P. list_ex P [] = False) & (!P h t. list_ex P (h#t) = (P h | list_ex P t))"
   by simp
 
 consts