dropped ancient infix mem; refined code generation operations in List.thy
authorhaftmann
Mon Jun 28 15:32:06 2010 +0200 (2010-06-28)
changeset 375959591362629e3
parent 37547 a92a7f45ca28
child 37596 248db70c9bcf
dropped ancient infix mem; refined code generation operations in List.thy
NEWS
src/HOL/Library/AssocList.thy
src/HOL/Library/Dlist.thy
src/HOL/Library/Executable_Set.thy
src/HOL/Library/Fset.thy
src/HOL/Library/More_Set.thy
src/HOL/MicroJava/DFA/LBVComplete.thy
src/HOL/ex/Execute_Choice.thy
src/HOL/ex/Meson_Test.thy
src/HOL/ex/Recdefs.thy
     1.1 --- a/NEWS	Fri Jun 25 07:19:21 2010 +0200
     1.2 +++ b/NEWS	Mon Jun 28 15:32:06 2010 +0200
     1.3 @@ -6,6 +6,22 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Dropped old infix syntax "mem" for List.member;  use "in set"
     1.8 +instead.  INCOMPATIBILITY.
     1.9 +
    1.10 +* Refactoring of code-generation specific operations in List.thy
    1.11 +
    1.12 +  constants
    1.13 +    null ~> List.null
    1.14 +
    1.15 +  facts
    1.16 +    mem_iff ~> member_def
    1.17 +    null_empty ~> null_def
    1.18 +
    1.19 +INCOMPATIBILITY.  Note that these were not suppossed to be used
    1.20 +regularly unless for striking reasons;  their main purpose was code
    1.21 +generation.
    1.22 +
    1.23  * Some previously unqualified names have been qualified:
    1.24  
    1.25    types
     2.1 --- a/src/HOL/Library/AssocList.thy	Fri Jun 25 07:19:21 2010 +0200
     2.2 +++ b/src/HOL/Library/AssocList.thy	Mon Jun 28 15:32:06 2010 +0200
     2.3 @@ -675,8 +675,8 @@
     2.4    by (rule mapping_eqI) simp
     2.5  
     2.6  lemma is_empty_Mapping [code]:
     2.7 -  "Mapping.is_empty (Mapping xs) \<longleftrightarrow> null xs"
     2.8 -  by (cases xs) (simp_all add: is_empty_def)
     2.9 +  "Mapping.is_empty (Mapping xs) \<longleftrightarrow> List.null xs"
    2.10 +  by (cases xs) (simp_all add: is_empty_def null_def)
    2.11  
    2.12  lemma update_Mapping [code]:
    2.13    "Mapping.update k v (Mapping xs) = Mapping (update k v xs)"
     3.1 --- a/src/HOL/Library/Dlist.thy	Fri Jun 25 07:19:21 2010 +0200
     3.2 +++ b/src/HOL/Library/Dlist.thy	Mon Jun 28 15:32:06 2010 +0200
     3.3 @@ -122,7 +122,7 @@
     3.4    next
     3.5      case (insert x xs)
     3.6      then have "\<not> member (Dlist xs) x" and "P (Dlist xs)"
     3.7 -      by (simp_all add: member_def mem_iff)
     3.8 +      by (simp_all add: member_def List.member_def)
     3.9      with insrt have "P (insert x (Dlist xs))" .
    3.10      with insert show ?case by (simp add: insert_def distinct_remdups_id)
    3.11    qed
    3.12 @@ -144,7 +144,7 @@
    3.13      case (Cons x xs)
    3.14      with dxs distinct have "\<not> member (Dlist xs) x"
    3.15        and "dxs = insert x (Dlist xs)"
    3.16 -      by (simp_all add: member_def mem_iff insert_def distinct_remdups_id)
    3.17 +      by (simp_all add: member_def List.member_def insert_def distinct_remdups_id)
    3.18      with insert show P .
    3.19    qed
    3.20  qed
    3.21 @@ -205,7 +205,7 @@
    3.22  
    3.23  lemma is_empty_Set [code]:
    3.24    "Fset.is_empty (Set dxs) \<longleftrightarrow> null dxs"
    3.25 -  by (simp add: null_def null_empty member_set)
    3.26 +  by (simp add: null_def List.null_def member_set)
    3.27  
    3.28  lemma bot_code [code]:
    3.29    "bot = Set empty"
     4.1 --- a/src/HOL/Library/Executable_Set.thy	Fri Jun 25 07:19:21 2010 +0200
     4.2 +++ b/src/HOL/Library/Executable_Set.thy	Mon Jun 28 15:32:06 2010 +0200
     4.3 @@ -50,9 +50,9 @@
     4.4    by simp
     4.5  
     4.6  lemma [code]:
     4.7 -  "x \<in> Set xs \<longleftrightarrow> member xs x"
     4.8 -  "x \<in> Coset xs \<longleftrightarrow> \<not> member xs x"
     4.9 -  by (simp_all add: mem_iff)
    4.10 +  "x \<in> Set xs \<longleftrightarrow> List.member xs x"
    4.11 +  "x \<in> Coset xs \<longleftrightarrow> \<not> List.member xs x"
    4.12 +  by (simp_all add: member_def)
    4.13  
    4.14  definition is_empty :: "'a set \<Rightarrow> bool" where
    4.15    [simp]: "is_empty A \<longleftrightarrow> A = {}"
    4.16 @@ -85,8 +85,8 @@
    4.17  *}
    4.18  
    4.19  lemma is_empty_Set [code]:
    4.20 -  "is_empty (Set xs) \<longleftrightarrow> null xs"
    4.21 -  by (simp add: empty_null)
    4.22 +  "is_empty (Set xs) \<longleftrightarrow> List.null xs"
    4.23 +  by (simp add: null_def)
    4.24  
    4.25  lemma empty_Set [code]:
    4.26    "empty = Set []"
    4.27 @@ -112,11 +112,11 @@
    4.28  
    4.29  lemma Ball_Set [code]:
    4.30    "Ball (Set xs) P \<longleftrightarrow> list_all P xs"
    4.31 -  by (simp add: ball_set)
    4.32 +  by (simp add: list_all_iff)
    4.33  
    4.34  lemma Bex_Set [code]:
    4.35    "Bex (Set xs) P \<longleftrightarrow> list_ex P xs"
    4.36 -  by (simp add: bex_set)
    4.37 +  by (simp add: list_ex_iff)
    4.38  
    4.39  lemma card_Set [code]:
    4.40    "card (Set xs) = length (remdups xs)"
     5.1 --- a/src/HOL/Library/Fset.thy	Fri Jun 25 07:19:21 2010 +0200
     5.2 +++ b/src/HOL/Library/Fset.thy	Mon Jun 28 15:32:06 2010 +0200
     5.3 @@ -51,7 +51,7 @@
     5.4  lemma member_code [code]:
     5.5    "member (Set xs) = List.member xs"
     5.6    "member (Coset xs) = Not \<circ> List.member xs"
     5.7 -  by (simp_all add: expand_fun_eq mem_iff fun_Compl_def bool_Compl_def)
     5.8 +  by (simp_all add: expand_fun_eq member_def fun_Compl_def bool_Compl_def)
     5.9  
    5.10  lemma member_image_UNIV [simp]:
    5.11    "member ` UNIV = UNIV"
    5.12 @@ -141,7 +141,7 @@
    5.13    [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)"
    5.14  
    5.15  lemma is_empty_Set [code]:
    5.16 -  "is_empty (Set xs) \<longleftrightarrow> null xs"
    5.17 +  "is_empty (Set xs) \<longleftrightarrow> List.null xs"
    5.18    by (simp add: is_empty_set)
    5.19  
    5.20  lemma empty_Set [code]:
    5.21 @@ -188,14 +188,14 @@
    5.22  
    5.23  lemma forall_Set [code]:
    5.24    "forall P (Set xs) \<longleftrightarrow> list_all P xs"
    5.25 -  by (simp add: Set_def ball_set)
    5.26 +  by (simp add: Set_def list_all_iff)
    5.27  
    5.28  definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
    5.29    [simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
    5.30  
    5.31  lemma exists_Set [code]:
    5.32    "exists P (Set xs) \<longleftrightarrow> list_ex P xs"
    5.33 -  by (simp add: Set_def bex_set)
    5.34 +  by (simp add: Set_def list_ex_iff)
    5.35  
    5.36  definition card :: "'a fset \<Rightarrow> nat" where
    5.37    [simp]: "card A = Finite_Set.card (member A)"
     6.1 --- a/src/HOL/Library/More_Set.thy	Fri Jun 25 07:19:21 2010 +0200
     6.2 +++ b/src/HOL/Library/More_Set.thy	Mon Jun 28 15:32:06 2010 +0200
     6.3 @@ -37,16 +37,8 @@
     6.4  subsection {* Basic set operations *}
     6.5  
     6.6  lemma is_empty_set:
     6.7 -  "is_empty (set xs) \<longleftrightarrow> null xs"
     6.8 -  by (simp add: is_empty_def null_empty)
     6.9 -
    6.10 -lemma ball_set:
    6.11 -  "(\<forall>x\<in>set xs. P x) \<longleftrightarrow> list_all P xs"
    6.12 -  by (rule list_ball_code)
    6.13 -
    6.14 -lemma bex_set:
    6.15 -  "(\<exists>x\<in>set xs. P x) \<longleftrightarrow> list_ex P xs"
    6.16 -  by (rule list_bex_code)
    6.17 +  "is_empty (set xs) \<longleftrightarrow> List.null xs"
    6.18 +  by (simp add: is_empty_def null_def)
    6.19  
    6.20  lemma empty_set:
    6.21    "{} = set []"
     7.1 --- a/src/HOL/MicroJava/DFA/LBVComplete.thy	Fri Jun 25 07:19:21 2010 +0200
     7.2 +++ b/src/HOL/MicroJava/DFA/LBVComplete.thy	Mon Jun 28 15:32:06 2010 +0200
     7.3 @@ -10,17 +10,17 @@
     7.4  begin
     7.5  
     7.6  definition is_target :: "['s step_type, 's list, nat] \<Rightarrow> bool" where 
     7.7 -  "is_target step phi pc' \<equiv>
     7.8 -     \<exists>pc s'. pc' \<noteq> pc+1 \<and> pc < length phi \<and> (pc',s') \<in> set (step pc (phi!pc))"
     7.9 +  "is_target step phi pc' \<longleftrightarrow>
    7.10 +     (\<exists>pc s'. pc' \<noteq> pc+1 \<and> pc < length phi \<and> (pc',s') \<in> set (step pc (phi!pc)))"
    7.11  
    7.12  definition make_cert :: "['s step_type, 's list, 's] \<Rightarrow> 's certificate" where
    7.13 -  "make_cert step phi B \<equiv> 
    7.14 +  "make_cert step phi B =
    7.15       map (\<lambda>pc. if is_target step phi pc then phi!pc else B) [0..<length phi] @ [B]"
    7.16  
    7.17  lemma [code]:
    7.18    "is_target step phi pc' =
    7.19 -  list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> pc' mem (map fst (step pc (phi!pc)))) [0..<length phi]"
    7.20 -by (force simp: list_ex_iff is_target_def mem_iff)
    7.21 +    list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> List.member (map fst (step pc (phi!pc))) pc') [0..<length phi]"
    7.22 +by (force simp: list_ex_iff member_def is_target_def)
    7.23  
    7.24  
    7.25  locale lbvc = lbv + 
     8.1 --- a/src/HOL/ex/Execute_Choice.thy	Fri Jun 25 07:19:21 2010 +0200
     8.2 +++ b/src/HOL/ex/Execute_Choice.thy	Mon Jun 28 15:32:06 2010 +0200
     8.3 @@ -66,7 +66,7 @@
     8.4    shows [code]: "valuesum (Mapping []) = 0"
     8.5    and "valuesum (Mapping (x # xs)) = (let l = (SOME l. l \<in> Mapping.keys (Mapping (x # xs))) in
     8.6      the (Mapping.lookup (Mapping (x # xs)) l) + valuesum (Mapping.delete l (Mapping (x # xs))))"
     8.7 -  by (simp_all add: valuesum_rec finite_dom_map_of is_empty_Mapping)
     8.8 +  by (simp_all add: valuesum_rec finite_dom_map_of is_empty_Mapping null_def)
     8.9  
    8.10  text {*
    8.11    As a side effect the precondition disappears (but note this has nothing to do with choice!).
     9.1 --- a/src/HOL/ex/Meson_Test.thy	Fri Jun 25 07:19:21 2010 +0200
     9.2 +++ b/src/HOL/ex/Meson_Test.thy	Mon Jun 28 15:32:06 2010 +0200
     9.3 @@ -16,7 +16,7 @@
     9.4    below and constants declared in HOL!
     9.5  *}
     9.6  
     9.7 -hide_const (open) subset member quotient union inter sum
     9.8 +hide_const (open) subset quotient union inter sum
     9.9  
    9.10  text {*
    9.11    Test data for the MESON proof procedure
    10.1 --- a/src/HOL/ex/Recdefs.thy	Fri Jun 25 07:19:21 2010 +0200
    10.2 +++ b/src/HOL/ex/Recdefs.thy	Mon Jun 28 15:32:06 2010 +0200
    10.3 @@ -1,5 +1,4 @@
    10.4  (*  Title:      HOL/ex/Recdefs.thy
    10.5 -    ID:         $Id$
    10.6      Author:     Konrad Slind and Lawrence C Paulson
    10.7      Copyright   1996  University of Cambridge
    10.8  
    10.9 @@ -44,7 +43,7 @@
   10.10  text {* Not handled automatically: too complicated. *}
   10.11  consts variant :: "nat * nat list => nat"
   10.12  recdef (permissive) variant "measure (\<lambda>(n,ns). size (filter (\<lambda>y. n \<le> y) ns))"
   10.13 -  "variant (x, L) = (if x mem L then variant (Suc x, L) else x)"
   10.14 +  "variant (x, L) = (if x \<in> set L then variant (Suc x, L) else x)"
   10.15  
   10.16  consts gcd :: "nat * nat => nat"
   10.17  recdef gcd  "measure (\<lambda>(x, y). x + y)"