# HG changeset patch
# User haftmann
# Date 1277731926 -7200
# Node ID 9591362629e34d97f24982840cacb97e6165fb5a
# Parent  a92a7f45ca28a3e7567affda0e64f4d66dea0761
dropped ancient infix mem; refined code generation operations in List.thy

diff -r a92a7f45ca28 -r 9591362629e3 NEWS
--- a/NEWS	Fri Jun 25 07:19:21 2010 +0200
+++ b/NEWS	Mon Jun 28 15:32:06 2010 +0200
@@ -6,6 +6,22 @@
 
 *** HOL ***
 
+* Dropped old infix syntax "mem" for List.member;  use "in set"
+instead.  INCOMPATIBILITY.
+
+* Refactoring of code-generation specific operations in List.thy
+
+  constants
+    null ~> List.null
+
+  facts
+    mem_iff ~> member_def
+    null_empty ~> null_def
+
+INCOMPATIBILITY.  Note that these were not suppossed to be used
+regularly unless for striking reasons;  their main purpose was code
+generation.
+
 * Some previously unqualified names have been qualified:
 
   types
diff -r a92a7f45ca28 -r 9591362629e3 src/HOL/Library/AssocList.thy
--- a/src/HOL/Library/AssocList.thy	Fri Jun 25 07:19:21 2010 +0200
+++ b/src/HOL/Library/AssocList.thy	Mon Jun 28 15:32:06 2010 +0200
@@ -675,8 +675,8 @@
   by (rule mapping_eqI) simp
 
 lemma is_empty_Mapping [code]:
-  "Mapping.is_empty (Mapping xs) \<longleftrightarrow> null xs"
-  by (cases xs) (simp_all add: is_empty_def)
+  "Mapping.is_empty (Mapping xs) \<longleftrightarrow> List.null xs"
+  by (cases xs) (simp_all add: is_empty_def null_def)
 
 lemma update_Mapping [code]:
   "Mapping.update k v (Mapping xs) = Mapping (update k v xs)"
diff -r a92a7f45ca28 -r 9591362629e3 src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Fri Jun 25 07:19:21 2010 +0200
+++ b/src/HOL/Library/Dlist.thy	Mon Jun 28 15:32:06 2010 +0200
@@ -122,7 +122,7 @@
   next
     case (insert x xs)
     then have "\<not> member (Dlist xs) x" and "P (Dlist xs)"
-      by (simp_all add: member_def mem_iff)
+      by (simp_all add: member_def List.member_def)
     with insrt have "P (insert x (Dlist xs))" .
     with insert show ?case by (simp add: insert_def distinct_remdups_id)
   qed
@@ -144,7 +144,7 @@
     case (Cons x xs)
     with dxs distinct have "\<not> member (Dlist xs) x"
       and "dxs = insert x (Dlist xs)"
-      by (simp_all add: member_def mem_iff insert_def distinct_remdups_id)
+      by (simp_all add: member_def List.member_def insert_def distinct_remdups_id)
     with insert show P .
   qed
 qed
@@ -205,7 +205,7 @@
 
 lemma is_empty_Set [code]:
   "Fset.is_empty (Set dxs) \<longleftrightarrow> null dxs"
-  by (simp add: null_def null_empty member_set)
+  by (simp add: null_def List.null_def member_set)
 
 lemma bot_code [code]:
   "bot = Set empty"
diff -r a92a7f45ca28 -r 9591362629e3 src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Fri Jun 25 07:19:21 2010 +0200
+++ b/src/HOL/Library/Executable_Set.thy	Mon Jun 28 15:32:06 2010 +0200
@@ -50,9 +50,9 @@
   by simp
 
 lemma [code]:
-  "x \<in> Set xs \<longleftrightarrow> member xs x"
-  "x \<in> Coset xs \<longleftrightarrow> \<not> member xs x"
-  by (simp_all add: mem_iff)
+  "x \<in> Set xs \<longleftrightarrow> List.member xs x"
+  "x \<in> Coset xs \<longleftrightarrow> \<not> List.member xs x"
+  by (simp_all add: member_def)
 
 definition is_empty :: "'a set \<Rightarrow> bool" where
   [simp]: "is_empty A \<longleftrightarrow> A = {}"
@@ -85,8 +85,8 @@
 *}
 
 lemma is_empty_Set [code]:
-  "is_empty (Set xs) \<longleftrightarrow> null xs"
-  by (simp add: empty_null)
+  "is_empty (Set xs) \<longleftrightarrow> List.null xs"
+  by (simp add: null_def)
 
 lemma empty_Set [code]:
   "empty = Set []"
@@ -112,11 +112,11 @@
 
 lemma Ball_Set [code]:
   "Ball (Set xs) P \<longleftrightarrow> list_all P xs"
-  by (simp add: ball_set)
+  by (simp add: list_all_iff)
 
 lemma Bex_Set [code]:
   "Bex (Set xs) P \<longleftrightarrow> list_ex P xs"
-  by (simp add: bex_set)
+  by (simp add: list_ex_iff)
 
 lemma card_Set [code]:
   "card (Set xs) = length (remdups xs)"
diff -r a92a7f45ca28 -r 9591362629e3 src/HOL/Library/Fset.thy
--- a/src/HOL/Library/Fset.thy	Fri Jun 25 07:19:21 2010 +0200
+++ b/src/HOL/Library/Fset.thy	Mon Jun 28 15:32:06 2010 +0200
@@ -51,7 +51,7 @@
 lemma member_code [code]:
   "member (Set xs) = List.member xs"
   "member (Coset xs) = Not \<circ> List.member xs"
-  by (simp_all add: expand_fun_eq mem_iff fun_Compl_def bool_Compl_def)
+  by (simp_all add: expand_fun_eq member_def fun_Compl_def bool_Compl_def)
 
 lemma member_image_UNIV [simp]:
   "member ` UNIV = UNIV"
@@ -141,7 +141,7 @@
   [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)"
 
 lemma is_empty_Set [code]:
-  "is_empty (Set xs) \<longleftrightarrow> null xs"
+  "is_empty (Set xs) \<longleftrightarrow> List.null xs"
   by (simp add: is_empty_set)
 
 lemma empty_Set [code]:
@@ -188,14 +188,14 @@
 
 lemma forall_Set [code]:
   "forall P (Set xs) \<longleftrightarrow> list_all P xs"
-  by (simp add: Set_def ball_set)
+  by (simp add: Set_def list_all_iff)
 
 definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
   [simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
 
 lemma exists_Set [code]:
   "exists P (Set xs) \<longleftrightarrow> list_ex P xs"
-  by (simp add: Set_def bex_set)
+  by (simp add: Set_def list_ex_iff)
 
 definition card :: "'a fset \<Rightarrow> nat" where
   [simp]: "card A = Finite_Set.card (member A)"
diff -r a92a7f45ca28 -r 9591362629e3 src/HOL/Library/More_Set.thy
--- a/src/HOL/Library/More_Set.thy	Fri Jun 25 07:19:21 2010 +0200
+++ b/src/HOL/Library/More_Set.thy	Mon Jun 28 15:32:06 2010 +0200
@@ -37,16 +37,8 @@
 subsection {* Basic set operations *}
 
 lemma is_empty_set:
-  "is_empty (set xs) \<longleftrightarrow> null xs"
-  by (simp add: is_empty_def null_empty)
-
-lemma ball_set:
-  "(\<forall>x\<in>set xs. P x) \<longleftrightarrow> list_all P xs"
-  by (rule list_ball_code)
-
-lemma bex_set:
-  "(\<exists>x\<in>set xs. P x) \<longleftrightarrow> list_ex P xs"
-  by (rule list_bex_code)
+  "is_empty (set xs) \<longleftrightarrow> List.null xs"
+  by (simp add: is_empty_def null_def)
 
 lemma empty_set:
   "{} = set []"
diff -r a92a7f45ca28 -r 9591362629e3 src/HOL/MicroJava/DFA/LBVComplete.thy
--- a/src/HOL/MicroJava/DFA/LBVComplete.thy	Fri Jun 25 07:19:21 2010 +0200
+++ b/src/HOL/MicroJava/DFA/LBVComplete.thy	Mon Jun 28 15:32:06 2010 +0200
@@ -10,17 +10,17 @@
 begin
 
 definition is_target :: "['s step_type, 's list, nat] \<Rightarrow> bool" where 
-  "is_target step phi pc' \<equiv>
-     \<exists>pc s'. pc' \<noteq> pc+1 \<and> pc < length phi \<and> (pc',s') \<in> set (step pc (phi!pc))"
+  "is_target step phi pc' \<longleftrightarrow>
+     (\<exists>pc s'. pc' \<noteq> pc+1 \<and> pc < length phi \<and> (pc',s') \<in> set (step pc (phi!pc)))"
 
 definition make_cert :: "['s step_type, 's list, 's] \<Rightarrow> 's certificate" where
-  "make_cert step phi B \<equiv> 
+  "make_cert step phi B =
      map (\<lambda>pc. if is_target step phi pc then phi!pc else B) [0..<length phi] @ [B]"
 
 lemma [code]:
   "is_target step phi pc' =
-  list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> pc' mem (map fst (step pc (phi!pc)))) [0..<length phi]"
-by (force simp: list_ex_iff is_target_def mem_iff)
+    list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> List.member (map fst (step pc (phi!pc))) pc') [0..<length phi]"
+by (force simp: list_ex_iff member_def is_target_def)
 
 
 locale lbvc = lbv + 
diff -r a92a7f45ca28 -r 9591362629e3 src/HOL/ex/Execute_Choice.thy
--- a/src/HOL/ex/Execute_Choice.thy	Fri Jun 25 07:19:21 2010 +0200
+++ b/src/HOL/ex/Execute_Choice.thy	Mon Jun 28 15:32:06 2010 +0200
@@ -66,7 +66,7 @@
   shows [code]: "valuesum (Mapping []) = 0"
   and "valuesum (Mapping (x # xs)) = (let l = (SOME l. l \<in> Mapping.keys (Mapping (x # xs))) in
     the (Mapping.lookup (Mapping (x # xs)) l) + valuesum (Mapping.delete l (Mapping (x # xs))))"
-  by (simp_all add: valuesum_rec finite_dom_map_of is_empty_Mapping)
+  by (simp_all add: valuesum_rec finite_dom_map_of is_empty_Mapping null_def)
 
 text {*
   As a side effect the precondition disappears (but note this has nothing to do with choice!).
diff -r a92a7f45ca28 -r 9591362629e3 src/HOL/ex/Meson_Test.thy
--- a/src/HOL/ex/Meson_Test.thy	Fri Jun 25 07:19:21 2010 +0200
+++ b/src/HOL/ex/Meson_Test.thy	Mon Jun 28 15:32:06 2010 +0200
@@ -16,7 +16,7 @@
   below and constants declared in HOL!
 *}
 
-hide_const (open) subset member quotient union inter sum
+hide_const (open) subset quotient union inter sum
 
 text {*
   Test data for the MESON proof procedure
diff -r a92a7f45ca28 -r 9591362629e3 src/HOL/ex/Recdefs.thy
--- a/src/HOL/ex/Recdefs.thy	Fri Jun 25 07:19:21 2010 +0200
+++ b/src/HOL/ex/Recdefs.thy	Mon Jun 28 15:32:06 2010 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/ex/Recdefs.thy
-    ID:         $Id$
     Author:     Konrad Slind and Lawrence C Paulson
     Copyright   1996  University of Cambridge
 
@@ -44,7 +43,7 @@
 text {* Not handled automatically: too complicated. *}
 consts variant :: "nat * nat list => nat"
 recdef (permissive) variant "measure (\<lambda>(n,ns). size (filter (\<lambda>y. n \<le> y) ns))"
-  "variant (x, L) = (if x mem L then variant (Suc x, L) else x)"
+  "variant (x, L) = (if x \<in> set L then variant (Suc x, L) else x)"
 
 consts gcd :: "nat * nat => nat"
 recdef gcd  "measure (\<lambda>(x, y). x + y)"