dropped ancient infix mem
authorhaftmann
Mon Jun 28 15:32:08 2010 +0200 (2010-06-28)
changeset 37596248db70c9bcf
parent 37595 9591362629e3
child 37597 a02ea93e88c6
dropped ancient infix mem
src/HOL/Auth/Guard/Guard.thy
src/HOL/Auth/Guard/GuardK.thy
src/HOL/Import/HOL4Compat.thy
     1.1 --- a/src/HOL/Auth/Guard/Guard.thy	Mon Jun 28 15:32:06 2010 +0200
     1.2 +++ b/src/HOL/Auth/Guard/Guard.thy	Mon Jun 28 15:32:08 2010 +0200
     1.3 @@ -201,14 +201,16 @@
     1.4  lemma cnb_app [simp]: "cnb (l @ l') = cnb l + cnb l'"
     1.5  by (induct l, auto)
     1.6  
     1.7 -lemma mem_cnb_minus: "x mem l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)"
     1.8 -by (induct l, auto)
     1.9 +lemma mem_cnb_minus: "x \<in> set l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)"
    1.10 +  by (induct l) auto
    1.11  
    1.12  lemmas mem_cnb_minus_substI = mem_cnb_minus [THEN ssubst]
    1.13  
    1.14 -lemma cnb_minus [simp]: "x mem l ==> cnb (remove l x) = cnb l - crypt_nb x"
    1.15 +lemma cnb_minus [simp]: "x \<in> set l ==> cnb (remove l x) = cnb l - crypt_nb x"
    1.16  apply (induct l, auto)
    1.17 -by (erule_tac l1=l and x1=x in mem_cnb_minus_substI, simp)
    1.18 +apply (erule_tac l1=l and x1=x in mem_cnb_minus_substI)
    1.19 +apply simp
    1.20 +done
    1.21  
    1.22  lemma parts_cnb: "Z:parts (set l) ==>
    1.23  cnb l = (cnb l - crypt_nb Z) + crypt_nb Z"
    1.24 @@ -272,7 +274,7 @@
    1.25  apply (clarsimp, blast)
    1.26  (* K ~:invKey`Ks *)
    1.27  apply (subgoal_tac "Guard n Ks (set (decrypt' l' K Y))")
    1.28 -apply (drule_tac x="decrypt' l' K Y" in spec, simp add: mem_iff)
    1.29 +apply (drule_tac x="decrypt' l' K Y" in spec, simp)
    1.30  apply (subgoal_tac "Crypt K Y:parts (set l)")
    1.31  apply (drule parts_cnb, rotate_tac -1, simp)
    1.32  apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub)
     2.1 --- a/src/HOL/Auth/Guard/GuardK.thy	Mon Jun 28 15:32:06 2010 +0200
     2.2 +++ b/src/HOL/Auth/Guard/GuardK.thy	Mon Jun 28 15:32:08 2010 +0200
     2.3 @@ -197,12 +197,12 @@
     2.4  lemma cnb_app [simp]: "cnb (l @ l') = cnb l + cnb l'"
     2.5  by (induct l, auto)
     2.6  
     2.7 -lemma mem_cnb_minus: "x mem l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)"
     2.8 +lemma mem_cnb_minus: "x \<in> set l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)"
     2.9  by (induct l, auto)
    2.10  
    2.11  lemmas mem_cnb_minus_substI = mem_cnb_minus [THEN ssubst]
    2.12  
    2.13 -lemma cnb_minus [simp]: "x mem l ==> cnb (remove l x) = cnb l - crypt_nb x"
    2.14 +lemma cnb_minus [simp]: "x \<in> set l ==> cnb (remove l x) = cnb l - crypt_nb x"
    2.15  apply (induct l, auto)
    2.16  by (erule_tac l1=l and x1=x in mem_cnb_minus_substI, simp)
    2.17  
    2.18 @@ -268,7 +268,7 @@
    2.19  apply (clarsimp, blast)
    2.20  (* K ~:invKey`Ks *)
    2.21  apply (subgoal_tac "GuardK n Ks (set (decrypt' l' K Y))")
    2.22 -apply (drule_tac x="decrypt' l' K Y" in spec, simp add: mem_iff)
    2.23 +apply (drule_tac x="decrypt' l' K Y" in spec, simp)
    2.24  apply (subgoal_tac "Crypt K Y:parts (set l)")
    2.25  apply (drule parts_cnb, rotate_tac -1, simp)
    2.26  apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub)
     3.1 --- a/src/HOL/Import/HOL4Compat.thy	Mon Jun 28 15:32:06 2010 +0200
     3.2 +++ b/src/HOL/Import/HOL4Compat.thy	Mon Jun 28 15:32:08 2010 +0200
     3.3 @@ -6,6 +6,7 @@
     3.4  imports HOL4Setup Complex_Main "~~/src/HOL/Old_Number_Theory/Primes" ContNotDenum
     3.5  begin
     3.6  
     3.7 +abbreviation (input) mem (infixl "mem" 55) where "x mem xs \<equiv> List.member xs x"
     3.8  no_notation differentiable (infixl "differentiable" 60)
     3.9  no_notation sums (infixr "sums" 80)
    3.10  
    3.11 @@ -326,8 +327,8 @@
    3.12    qed
    3.13  qed
    3.14  
    3.15 -lemma NULL_DEF: "(null [] = True) & (!h t. null (h # t) = False)"
    3.16 -  by simp
    3.17 +lemma NULL_DEF: "(List.null [] = True) & (!h t. List.null (h # t) = False)"
    3.18 +  by (simp add: null_def)
    3.19  
    3.20  definition sum :: "nat list \<Rightarrow> nat" where
    3.21    "sum l == foldr (op +) l 0"
    3.22 @@ -347,8 +348,8 @@
    3.23  lemma MAP: "(!f. map f [] = []) & (!f h t. map f (h#t) = f h#map f t)"
    3.24    by simp
    3.25  
    3.26 -lemma MEM: "(!x. x mem [] = False) & (!x h t. x mem (h#t) = ((x = h) | x mem t))"
    3.27 -  by auto
    3.28 +lemma MEM: "(!x. List.member [] x = False) & (!x h t. List.member (h#t) x = ((x = h) | List.member t x))"
    3.29 +  by (simp add: member_def)
    3.30  
    3.31  lemma FILTER: "(!P. filter P [] = []) & (!P h t.
    3.32             filter P (h#t) = (if P h then h#filter P t else filter P t))"
    3.33 @@ -373,15 +374,7 @@
    3.34  lemma EVERY_DEF: "(!P. list_all P [] = True) & (!P h t. list_all P (h#t) = (P h & list_all P t))"
    3.35    by simp
    3.36  
    3.37 -consts
    3.38 -  list_exists :: "['a \<Rightarrow> bool,'a list] \<Rightarrow> bool"
    3.39 -
    3.40 -primrec
    3.41 -  list_exists_Nil: "list_exists P Nil = False"
    3.42 -  list_exists_Cons: "list_exists P (x#xs) = (if P x then True else list_exists P xs)"
    3.43 -
    3.44 -lemma list_exists_DEF: "(!P. list_exists P [] = False) &
    3.45 -         (!P h t. list_exists P (h#t) = (P h | list_exists P t))"
    3.46 +lemma list_exists_DEF: "(!P. list_ex P [] = False) & (!P h t. list_ex P (h#t) = (P h | list_ex P t))"
    3.47    by simp
    3.48  
    3.49  consts