--- 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
--- 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)"
--- 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"
--- 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)"
--- 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)"
--- 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 []"
--- 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 +
--- 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!).
--- 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
--- 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)"