Converted translations to abbbreviations.
authornipkow
Thu Mar 23 20:03:53 2006 +0100 (2006-03-23)
changeset 19323ec5cd5b1804c
parent 19322 bf84bdf05f14
child 19324 659b8165c724
Converted translations to abbbreviations.
Removed a few odd functions from Map and AssocList.
Moved chg_map from Map to Bali/Basis.
src/HOL/Bali/Basis.thy
src/HOL/Equiv_Relations.thy
src/HOL/Fun.thy
src/HOL/Library/AssocList.thy
src/HOL/Map.thy
src/HOL/Relation.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/Bali/Basis.thy	Thu Mar 23 18:14:06 2006 +0100
     1.2 +++ b/src/HOL/Bali/Basis.thy	Thu Mar 23 20:03:53 2006 +0100
     1.3 @@ -277,6 +277,23 @@
     1.4    "! x:A: P"    == "! x:o2s A. P"
     1.5    "? x:A: P"    == "? x:o2s A. P"
     1.6  
     1.7 +section "Special map update"
     1.8 +
     1.9 +text{* Deemed too special for theory Map. *}
    1.10 +
    1.11 +constdefs
    1.12 +  chg_map :: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
    1.13 + "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
    1.14 +
    1.15 +lemma chg_map_new[simp]: "m a = None   ==> chg_map f a m = m"
    1.16 +by (unfold chg_map_def, auto)
    1.17 +
    1.18 +lemma chg_map_upd[simp]: "m a = Some b ==> chg_map f a m = m(a|->f b)"
    1.19 +by (unfold chg_map_def, auto)
    1.20 +
    1.21 +lemma chg_map_other [simp]: "a \<noteq> b \<Longrightarrow> chg_map f a m b = m b"
    1.22 +by (auto simp: chg_map_def split add: option.split)
    1.23 +
    1.24  
    1.25  section "unique association lists"
    1.26  
     2.1 --- a/src/HOL/Equiv_Relations.thy	Thu Mar 23 18:14:06 2006 +0100
     2.2 +++ b/src/HOL/Equiv_Relations.thy	Thu Mar 23 20:03:53 2006 +0100
     2.3 @@ -163,11 +163,9 @@
     2.4    fixes r and f
     2.5    assumes congruent: "(y,z) \<in> r ==> f y = f z"
     2.6  
     2.7 -syntax
     2.8 -  RESPECTS ::"['a => 'b, ('a * 'a) set] => bool"  (infixr "respects" 80)
     2.9 -
    2.10 -translations
    2.11 -  "f respects r" == "congruent r f"
    2.12 +abbreviation (output)
    2.13 +  RESPECTS :: "('a => 'b) => ('a * 'a) set => bool"  (infixr "respects" 80)
    2.14 +  "f respects r = congruent r f"
    2.15  
    2.16  
    2.17  lemma UN_constant_eq: "a \<in> A ==> \<forall>y \<in> A. f y = c ==> (\<Union>y \<in> A. f(y))=c"
    2.18 @@ -225,9 +223,12 @@
    2.19  text{*Abbreviation for the common case where the relations are identical*}
    2.20  syntax
    2.21    RESPECTS2 ::"['a => 'b, ('a * 'a) set] => bool"  (infixr "respects2 " 80)
    2.22 -
    2.23  translations
    2.24    "f respects2 r" => "congruent2 r r f"
    2.25 +(*
    2.26 +Warning: cannot use "abbreviation" here because the two occurrences of
    2.27 +r may need to be of different type (see Hyperreal/StarDef).
    2.28 +*)
    2.29  
    2.30  lemma congruent2_implies_congruent:
    2.31      "equiv A r1 ==> congruent2 r1 r2 f ==> a \<in> A ==> congruent r2 (f a)"
    2.32 @@ -333,7 +334,7 @@
    2.33   apply(fastsimp simp add:inj_on_def)
    2.34  apply (simp add:setsum_constant)
    2.35  done
    2.36 -
    2.37 +(*
    2.38  ML
    2.39  {*
    2.40  val UN_UN_split_split_eq = thm "UN_UN_split_split_eq";
    2.41 @@ -371,5 +372,5 @@
    2.42  val subset_equiv_class = thm "subset_equiv_class";
    2.43  val sym_trans_comp_subset = thm "sym_trans_comp_subset";
    2.44  *}
    2.45 -
    2.46 +*)
    2.47  end
     3.1 --- a/src/HOL/Fun.thy	Thu Mar 23 18:14:06 2006 +0100
     3.2 +++ b/src/HOL/Fun.thy	Thu Mar 23 20:03:53 2006 +0100
     3.3 @@ -62,9 +62,9 @@
     3.4      "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
     3.5  
     3.6  text{*A common special case: functions injective over the entire domain type.*}
     3.7 -syntax inj   :: "('a => 'b) => bool"
     3.8 -translations
     3.9 -  "inj f" == "inj_on f UNIV"
    3.10 +
    3.11 +abbreviation (output)
    3.12 +  "inj f = inj_on f UNIV"
    3.13  
    3.14  constdefs
    3.15    surj :: "('a => 'b) => bool"                   (*surjective*)
     4.1 --- a/src/HOL/Library/AssocList.thy	Thu Mar 23 18:14:06 2006 +0100
     4.2 +++ b/src/HOL/Library/AssocList.thy	Thu Mar 23 20:03:53 2006 +0100
     4.3 @@ -16,14 +16,17 @@
     4.4    delete     :: "'key \<Rightarrow> ('key * 'val)list \<Rightarrow>  ('key * 'val)list"
     4.5    update     :: "'key \<Rightarrow> 'val \<Rightarrow> ('key * 'val)list \<Rightarrow>  ('key * 'val)list"
     4.6    updates    :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key * 'val)list \<Rightarrow>  ('key * 'val)list"
     4.7 -  substitute :: "'val \<Rightarrow> 'val \<Rightarrow> ('key * 'val)list \<Rightarrow>  ('key * 'val)list"
     4.8 -  map_at     :: "('val \<Rightarrow> 'val) \<Rightarrow> 'key \<Rightarrow> ('key * 'val)list \<Rightarrow>  ('key * 'val) list"
     4.9    merge      :: "('key * 'val)list \<Rightarrow> ('key * 'val)list \<Rightarrow> ('key * 'val)list"
    4.10    compose    :: "('key * 'a)list \<Rightarrow> ('a * 'b)list \<Rightarrow> ('key * 'b)list"
    4.11    restrict   :: "('key set) \<Rightarrow> ('key * 'val)list \<Rightarrow> ('key * 'val)list"
    4.12  
    4.13    clearjunk  :: "('key * 'val)list \<Rightarrow> ('key * 'val)list"
    4.14  
    4.15 +(* a bit special
    4.16 +  substitute :: "'val \<Rightarrow> 'val \<Rightarrow> ('key * 'val)list \<Rightarrow>  ('key * 'val)list"
    4.17 +  map_at     :: "('val \<Rightarrow> 'val) \<Rightarrow> 'key \<Rightarrow> ('key * 'val)list \<Rightarrow>  ('key * 'val) list"
    4.18 +*)
    4.19 +
    4.20  defs
    4.21  delete_def: "delete k \<equiv> filter (\<lambda>p. fst p \<noteq> k)"
    4.22  
    4.23 @@ -35,15 +38,18 @@
    4.24  "updates (k#ks) vs al = (case vs of [] \<Rightarrow> al 
    4.25                           | (v#vs') \<Rightarrow> updates ks vs' (update k v al))"
    4.26  primrec
    4.27 +"merge xs [] = xs"
    4.28 +"merge xs (p#ps) = update (fst p) (snd p) (merge xs ps)"
    4.29 +
    4.30 +(*
    4.31 +primrec
    4.32  "substitute v v' [] = []"
    4.33  "substitute v v' (p#ps) = (if snd p = v then (fst p,v')#substitute v v' ps
    4.34                            else p#substitute v v' ps)"
    4.35  primrec
    4.36  "map_at f k [] = []"
    4.37  "map_at f k (p#ps) = (if fst p = k then (k,f (snd p))#ps else p # map_at f k ps)"
    4.38 -primrec
    4.39 -"merge xs [] = xs"
    4.40 -"merge xs (p#ps) = update (fst p) (snd p) (merge xs ps)"
    4.41 +*)
    4.42  
    4.43  lemma length_delete_le: "length (delete k al) \<le> length al"
    4.44  proof (induct al)
    4.45 @@ -431,7 +437,7 @@
    4.46    "size xs = size ys \<Longrightarrow> updates xs (ys@zs) al = updates xs ys al"
    4.47    by (induct xs fixing: ys al) (auto split: list.splits)
    4.48  
    4.49 -
    4.50 +(*
    4.51  (* ******************************************************************************** *)
    4.52  subsection {* @{const substitute} *}
    4.53  (* ******************************************************************************** *)
    4.54 @@ -456,7 +462,8 @@
    4.55  lemma clearjunk_substitute:
    4.56   "clearjunk (substitute v v' al) = substitute v v' (clearjunk al)"
    4.57    by (induct al rule: clearjunk.induct) (auto simp add: substitute_filter delete_def)
    4.58 -
    4.59 +*)
    4.60 +(*
    4.61  (* ******************************************************************************** *)
    4.62  subsection {* @{const map_at} *}
    4.63  (* ******************************************************************************** *)
    4.64 @@ -491,7 +498,7 @@
    4.65  
    4.66  lemma map_at_other [simp]: "a \<noteq> b \<Longrightarrow> map_of (map_at f a al) b = map_of al b"
    4.67    by (simp add: map_at_conv')
    4.68 -
    4.69 +*)
    4.70  (* ******************************************************************************** *)
    4.71  subsection {* @{const merge} *}
    4.72  (* ******************************************************************************** *)
     5.1 --- a/src/HOL/Map.thy	Thu Mar 23 18:14:06 2006 +0100
     5.2 +++ b/src/HOL/Map.thy	Thu Mar 23 20:03:53 2006 +0100
     5.3 @@ -16,29 +16,28 @@
     5.4  translations (type) "a ~=> b " <= (type) "a => b option"
     5.5  
     5.6  consts
     5.7 -chg_map	:: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
     5.8  map_add :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
     5.9  restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" (infixl "|`"  110)
    5.10  dom	:: "('a ~=> 'b) => 'a set"
    5.11  ran	:: "('a ~=> 'b) => 'b set"
    5.12  map_of	:: "('a * 'b)list => 'a ~=> 'b"
    5.13 -map_upds:: "('a ~=> 'b) => 'a list => 'b list => 
    5.14 -	    ('a ~=> 'b)"
    5.15 -map_upd_s::"('a ~=> 'b) => 'a set => 'b => 
    5.16 -	    ('a ~=> 'b)"			 ("_/'(_{|->}_/')" [900,0,0]900)
    5.17 -map_subst::"('a ~=> 'b) => 'b => 'b => 
    5.18 -	    ('a ~=> 'b)"			 ("_/'(_~>_/')"    [900,0,0]900)
    5.19 +map_upds:: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"
    5.20  map_le  :: "('a ~=> 'b) => ('a ~=> 'b) => bool" (infix "\<subseteq>\<^sub>m" 50)
    5.21  
    5.22  constdefs
    5.23    map_comp :: "('b ~=> 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "o'_m" 55)
    5.24    "f o_m g  == (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)"
    5.25  
    5.26 +syntax
    5.27 +  empty     ::  "'a ~=> 'b"
    5.28 +translations
    5.29 +  "empty"    => "%_. None"
    5.30 +  "empty"    <= "%x. None"
    5.31 +
    5.32  nonterminals
    5.33    maplets maplet
    5.34  
    5.35  syntax
    5.36 -  empty	    ::  "'a ~=> 'b"
    5.37    "_maplet"  :: "['a, 'a] => maplet"             ("_ /|->/ _")
    5.38    "_maplets" :: "['a, 'a] => maplet"             ("_ /[|->]/ _")
    5.39    ""         :: "maplet => maplets"             ("_")
    5.40 @@ -54,23 +53,11 @@
    5.41    "_maplet"  :: "['a, 'a] => maplet"             ("_ /\<mapsto>/ _")
    5.42    "_maplets" :: "['a, 'a] => maplet"             ("_ /[\<mapsto>]/ _")
    5.43  
    5.44 -  map_upd_s  :: "('a ~=> 'b) => 'a set => 'b => ('a ~=> 'b)"
    5.45 -				    		 ("_/'(_/{\<mapsto>}/_')" [900,0,0]900)
    5.46 -  map_subst :: "('a ~=> 'b) => 'b => 'b => 
    5.47 -	        ('a ~=> 'b)"			 ("_/'(_\<leadsto>_/')"    [900,0,0]900)
    5.48 - "@chg_map" :: "('a ~=> 'b) => 'a => ('b => 'b) => ('a ~=> 'b)"
    5.49 -					  ("_/'(_/\<mapsto>\<lambda>_. _')"  [900,0,0,0] 900)
    5.50 -
    5.51  syntax (latex output)
    5.52    restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" ("_\<restriction>\<^bsub>_\<^esub>" [111,110] 110)
    5.53    --"requires amssymb!"
    5.54  
    5.55  translations
    5.56 -  "empty"    => "%_. None"
    5.57 -  "empty"    <= "%x. None"
    5.58 -
    5.59 -  "m(x\<mapsto>\<lambda>y. f)" == "chg_map (\<lambda>y. f) x m"
    5.60 -
    5.61    "_MapUpd m (_Maplets xy ms)"  == "_MapUpd (_MapUpd m xy) ms"
    5.62    "_MapUpd m (_maplet  x y)"    == "m(x:=Some y)"
    5.63    "_MapUpd m (_maplets x y)"    == "map_upds m x y"
    5.64 @@ -79,14 +66,10 @@
    5.65    "_Maplets ms1 (_Maplets ms2 ms3)" <= "_Maplets (_Maplets ms1 ms2) ms3"
    5.66  
    5.67  defs
    5.68 -chg_map_def:  "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
    5.69 -
    5.70  map_add_def:   "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
    5.71  restrict_map_def: "m|`A == %x. if x : A then m x else None"
    5.72  
    5.73  map_upds_def: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
    5.74 -map_upd_s_def: "m(as{|->}b) == %x. if x : as then Some b else m x"
    5.75 -map_subst_def: "m(a~>b)     == %x. if m x = Some a then Some b else m x"
    5.76  
    5.77  dom_def: "dom(m) == {a. m a ~= None}"
    5.78  ran_def: "ran(m) == {b. EX a. m a = Some b}"
    5.79 @@ -97,6 +80,38 @@
    5.80    "map_of [] = empty"
    5.81    "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
    5.82  
    5.83 +(* special purpose constants that should be defined somewhere else and
    5.84 +whose syntax is a bit odd as well:
    5.85 +
    5.86 + "@chg_map" :: "('a ~=> 'b) => 'a => ('b => 'b) => ('a ~=> 'b)"
    5.87 +					  ("_/'(_/\<mapsto>\<lambda>_. _')"  [900,0,0,0] 900)
    5.88 +  "m(x\<mapsto>\<lambda>y. f)" == "chg_map (\<lambda>y. f) x m"
    5.89 +
    5.90 +map_upd_s::"('a ~=> 'b) => 'a set => 'b => 
    5.91 +	    ('a ~=> 'b)"			 ("_/'(_{|->}_/')" [900,0,0]900)
    5.92 +map_subst::"('a ~=> 'b) => 'b => 'b => 
    5.93 +	    ('a ~=> 'b)"			 ("_/'(_~>_/')"    [900,0,0]900)
    5.94 +
    5.95 +map_upd_s_def: "m(as{|->}b) == %x. if x : as then Some b else m x"
    5.96 +map_subst_def: "m(a~>b)     == %x. if m x = Some a then Some b else m x"
    5.97 +
    5.98 +  map_upd_s  :: "('a ~=> 'b) => 'a set => 'b => ('a ~=> 'b)"
    5.99 +				    		 ("_/'(_/{\<mapsto>}/_')" [900,0,0]900)
   5.100 +  map_subst :: "('a ~=> 'b) => 'b => 'b => 
   5.101 +	        ('a ~=> 'b)"			 ("_/'(_\<leadsto>_/')"    [900,0,0]900)
   5.102 +
   5.103 +
   5.104 +subsection {* @{term [source] map_upd_s} *}
   5.105 +
   5.106 +lemma map_upd_s_apply [simp]: 
   5.107 +  "(m(as{|->}b)) x = (if x : as then Some b else m x)"
   5.108 +by (simp add: map_upd_s_def)
   5.109 +
   5.110 +lemma map_subst_apply [simp]: 
   5.111 +  "(m(a~>b)) x = (if m x = Some a then Some b else m x)" 
   5.112 +by (simp add: map_subst_def)
   5.113 +
   5.114 +*)
   5.115  
   5.116  subsection {* @{term [source] empty} *}
   5.117  
   5.118 @@ -166,18 +181,6 @@
   5.119  done
   5.120  
   5.121  
   5.122 -subsection {* @{term [source] chg_map} *}
   5.123 -
   5.124 -lemma chg_map_new[simp]: "m a = None   ==> chg_map f a m = m"
   5.125 -by (unfold chg_map_def, auto)
   5.126 -
   5.127 -lemma chg_map_upd[simp]: "m a = Some b ==> chg_map f a m = m(a|->f b)"
   5.128 -by (unfold chg_map_def, auto)
   5.129 -
   5.130 -lemma chg_map_other [simp]: "a \<noteq> b \<Longrightarrow> chg_map f a m b = m b"
   5.131 -by (auto simp: chg_map_def split add: option.split)
   5.132 -
   5.133 -
   5.134  subsection {* @{term [source] map_of} *}
   5.135  
   5.136  lemma map_of_eq_None_iff:
   5.137 @@ -461,16 +464,6 @@
   5.138  done
   5.139  
   5.140  
   5.141 -subsection {* @{term [source] map_upd_s} *}
   5.142 -
   5.143 -lemma map_upd_s_apply [simp]: 
   5.144 -  "(m(as{|->}b)) x = (if x : as then Some b else m x)"
   5.145 -by (simp add: map_upd_s_def)
   5.146 -
   5.147 -lemma map_subst_apply [simp]: 
   5.148 -  "(m(a~>b)) x = (if m x = Some a then Some b else m x)" 
   5.149 -by (simp add: map_subst_def)
   5.150 -
   5.151  subsection {* @{term [source] dom} *}
   5.152  
   5.153  lemma domI: "m a = Some b ==> a : dom m"
     6.1 --- a/src/HOL/Relation.thy	Thu Mar 23 18:14:06 2006 +0100
     6.2 +++ b/src/HOL/Relation.thy	Thu Mar 23 20:03:53 2006 +0100
     6.3 @@ -58,10 +58,9 @@
     6.4    inv_image :: "('b * 'b) set => ('a => 'b) => ('a * 'a) set"
     6.5    "inv_image r f == {(x, y). (f x, f y) : r}"
     6.6  
     6.7 -syntax
     6.8 +abbreviation (output)
     6.9    reflexive :: "('a * 'a) set => bool"  -- {* reflexivity over a type *}
    6.10 -translations
    6.11 -  "reflexive" == "refl UNIV"
    6.12 +  "reflexive = refl UNIV"
    6.13  
    6.14  
    6.15  subsection {* The identity relation *}
     7.1 --- a/src/HOL/Set.thy	Thu Mar 23 18:14:06 2006 +0100
     7.2 +++ b/src/HOL/Set.thy	Thu Mar 23 20:03:53 2006 +0100
     7.3 @@ -47,9 +47,11 @@
     7.4  
     7.5  subsection {* Additional concrete syntax *}
     7.6  
     7.7 +abbreviation (output)
     7.8 +  range :: "('a => 'b) => 'b set"             -- "of function"
     7.9 +  "range f  =  f ` UNIV"
    7.10 +
    7.11  syntax
    7.12 -  range         :: "('a => 'b) => 'b set"             -- "of function"
    7.13 -
    7.14    "op ~:"       :: "'a => 'a set => bool"                 ("op ~:")  -- "non-membership"
    7.15    "op ~:"       :: "'a => 'a set => bool"                 ("(_/ ~: _)" [50, 51] 50)
    7.16  
    7.17 @@ -72,7 +74,6 @@
    7.18    "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3? _:_./ _)" [0, 0, 10] 10)
    7.19  
    7.20  translations
    7.21 -  "range f"     == "f`UNIV"
    7.22    "x ~: y"      == "~ (x : y)"
    7.23    "{x, xs}"     == "insert x {xs}"
    7.24    "{x}"         == "insert x {}"