src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
changeset 61140 78ece168f5b5
parent 61125 4c68426800de
child 61180 e4716b792713
     1.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Sun Sep 06 22:14:52 2015 +0200
     1.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Wed Sep 09 17:07:44 2015 +0200
     1.3 @@ -212,6 +212,18 @@
     1.4      done
     1.5  qed
     1.6  
     1.7 +subsection \<open>Alternative rules for membership in lists\<close>
     1.8 +
     1.9 +declare in_set_member[code_pred_inline]
    1.10 +
    1.11 +lemma member_intros [code_pred_intro]:
    1.12 +  "List.member (x#xs) x"
    1.13 +  "List.member xs x \<Longrightarrow> List.member (y#xs) x"
    1.14 +by(simp_all add: List.member_def)
    1.15 +
    1.16 +code_pred List.member
    1.17 +  by(auto simp add: List.member_def elim: list.set_cases)
    1.18 +
    1.19  section \<open>Setup for String.literal\<close>
    1.20  
    1.21  setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name "STR"}]\<close>