Converted translations to abbbreviations.
Removed a few odd functions from Map and AssocList.
Moved chg_map from Map to Bali/Basis.
--- a/src/HOL/Bali/Basis.thy Thu Mar 23 18:14:06 2006 +0100
+++ b/src/HOL/Bali/Basis.thy Thu Mar 23 20:03:53 2006 +0100
@@ -277,6 +277,23 @@
"! x:A: P" == "! x:o2s A. P"
"? x:A: P" == "? x:o2s A. P"
+section "Special map update"
+
+text{* Deemed too special for theory Map. *}
+
+constdefs
+ chg_map :: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
+ "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
+
+lemma chg_map_new[simp]: "m a = None ==> chg_map f a m = m"
+by (unfold chg_map_def, auto)
+
+lemma chg_map_upd[simp]: "m a = Some b ==> chg_map f a m = m(a|->f b)"
+by (unfold chg_map_def, auto)
+
+lemma chg_map_other [simp]: "a \<noteq> b \<Longrightarrow> chg_map f a m b = m b"
+by (auto simp: chg_map_def split add: option.split)
+
section "unique association lists"
--- a/src/HOL/Equiv_Relations.thy Thu Mar 23 18:14:06 2006 +0100
+++ b/src/HOL/Equiv_Relations.thy Thu Mar 23 20:03:53 2006 +0100
@@ -163,11 +163,9 @@
fixes r and f
assumes congruent: "(y,z) \<in> r ==> f y = f z"
-syntax
- RESPECTS ::"['a => 'b, ('a * 'a) set] => bool" (infixr "respects" 80)
-
-translations
- "f respects r" == "congruent r f"
+abbreviation (output)
+ RESPECTS :: "('a => 'b) => ('a * 'a) set => bool" (infixr "respects" 80)
+ "f respects r = congruent r f"
lemma UN_constant_eq: "a \<in> A ==> \<forall>y \<in> A. f y = c ==> (\<Union>y \<in> A. f(y))=c"
@@ -225,9 +223,12 @@
text{*Abbreviation for the common case where the relations are identical*}
syntax
RESPECTS2 ::"['a => 'b, ('a * 'a) set] => bool" (infixr "respects2 " 80)
-
translations
"f respects2 r" => "congruent2 r r f"
+(*
+Warning: cannot use "abbreviation" here because the two occurrences of
+r may need to be of different type (see Hyperreal/StarDef).
+*)
lemma congruent2_implies_congruent:
"equiv A r1 ==> congruent2 r1 r2 f ==> a \<in> A ==> congruent r2 (f a)"
@@ -333,7 +334,7 @@
apply(fastsimp simp add:inj_on_def)
apply (simp add:setsum_constant)
done
-
+(*
ML
{*
val UN_UN_split_split_eq = thm "UN_UN_split_split_eq";
@@ -371,5 +372,5 @@
val subset_equiv_class = thm "subset_equiv_class";
val sym_trans_comp_subset = thm "sym_trans_comp_subset";
*}
-
+*)
end
--- a/src/HOL/Fun.thy Thu Mar 23 18:14:06 2006 +0100
+++ b/src/HOL/Fun.thy Thu Mar 23 20:03:53 2006 +0100
@@ -62,9 +62,9 @@
"inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
text{*A common special case: functions injective over the entire domain type.*}
-syntax inj :: "('a => 'b) => bool"
-translations
- "inj f" == "inj_on f UNIV"
+
+abbreviation (output)
+ "inj f = inj_on f UNIV"
constdefs
surj :: "('a => 'b) => bool" (*surjective*)
--- a/src/HOL/Library/AssocList.thy Thu Mar 23 18:14:06 2006 +0100
+++ b/src/HOL/Library/AssocList.thy Thu Mar 23 20:03:53 2006 +0100
@@ -16,14 +16,17 @@
delete :: "'key \<Rightarrow> ('key * 'val)list \<Rightarrow> ('key * 'val)list"
update :: "'key \<Rightarrow> 'val \<Rightarrow> ('key * 'val)list \<Rightarrow> ('key * 'val)list"
updates :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key * 'val)list \<Rightarrow> ('key * 'val)list"
- substitute :: "'val \<Rightarrow> 'val \<Rightarrow> ('key * 'val)list \<Rightarrow> ('key * 'val)list"
- map_at :: "('val \<Rightarrow> 'val) \<Rightarrow> 'key \<Rightarrow> ('key * 'val)list \<Rightarrow> ('key * 'val) list"
merge :: "('key * 'val)list \<Rightarrow> ('key * 'val)list \<Rightarrow> ('key * 'val)list"
compose :: "('key * 'a)list \<Rightarrow> ('a * 'b)list \<Rightarrow> ('key * 'b)list"
restrict :: "('key set) \<Rightarrow> ('key * 'val)list \<Rightarrow> ('key * 'val)list"
clearjunk :: "('key * 'val)list \<Rightarrow> ('key * 'val)list"
+(* a bit special
+ substitute :: "'val \<Rightarrow> 'val \<Rightarrow> ('key * 'val)list \<Rightarrow> ('key * 'val)list"
+ map_at :: "('val \<Rightarrow> 'val) \<Rightarrow> 'key \<Rightarrow> ('key * 'val)list \<Rightarrow> ('key * 'val) list"
+*)
+
defs
delete_def: "delete k \<equiv> filter (\<lambda>p. fst p \<noteq> k)"
@@ -35,15 +38,18 @@
"updates (k#ks) vs al = (case vs of [] \<Rightarrow> al
| (v#vs') \<Rightarrow> updates ks vs' (update k v al))"
primrec
+"merge xs [] = xs"
+"merge xs (p#ps) = update (fst p) (snd p) (merge xs ps)"
+
+(*
+primrec
"substitute v v' [] = []"
"substitute v v' (p#ps) = (if snd p = v then (fst p,v')#substitute v v' ps
else p#substitute v v' ps)"
primrec
"map_at f k [] = []"
"map_at f k (p#ps) = (if fst p = k then (k,f (snd p))#ps else p # map_at f k ps)"
-primrec
-"merge xs [] = xs"
-"merge xs (p#ps) = update (fst p) (snd p) (merge xs ps)"
+*)
lemma length_delete_le: "length (delete k al) \<le> length al"
proof (induct al)
@@ -431,7 +437,7 @@
"size xs = size ys \<Longrightarrow> updates xs (ys@zs) al = updates xs ys al"
by (induct xs fixing: ys al) (auto split: list.splits)
-
+(*
(* ******************************************************************************** *)
subsection {* @{const substitute} *}
(* ******************************************************************************** *)
@@ -456,7 +462,8 @@
lemma clearjunk_substitute:
"clearjunk (substitute v v' al) = substitute v v' (clearjunk al)"
by (induct al rule: clearjunk.induct) (auto simp add: substitute_filter delete_def)
-
+*)
+(*
(* ******************************************************************************** *)
subsection {* @{const map_at} *}
(* ******************************************************************************** *)
@@ -491,7 +498,7 @@
lemma map_at_other [simp]: "a \<noteq> b \<Longrightarrow> map_of (map_at f a al) b = map_of al b"
by (simp add: map_at_conv')
-
+*)
(* ******************************************************************************** *)
subsection {* @{const merge} *}
(* ******************************************************************************** *)
--- a/src/HOL/Map.thy Thu Mar 23 18:14:06 2006 +0100
+++ b/src/HOL/Map.thy Thu Mar 23 20:03:53 2006 +0100
@@ -16,29 +16,28 @@
translations (type) "a ~=> b " <= (type) "a => b option"
consts
-chg_map :: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
map_add :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" (infixl "|`" 110)
dom :: "('a ~=> 'b) => 'a set"
ran :: "('a ~=> 'b) => 'b set"
map_of :: "('a * 'b)list => 'a ~=> 'b"
-map_upds:: "('a ~=> 'b) => 'a list => 'b list =>
- ('a ~=> 'b)"
-map_upd_s::"('a ~=> 'b) => 'a set => 'b =>
- ('a ~=> 'b)" ("_/'(_{|->}_/')" [900,0,0]900)
-map_subst::"('a ~=> 'b) => 'b => 'b =>
- ('a ~=> 'b)" ("_/'(_~>_/')" [900,0,0]900)
+map_upds:: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"
map_le :: "('a ~=> 'b) => ('a ~=> 'b) => bool" (infix "\<subseteq>\<^sub>m" 50)
constdefs
map_comp :: "('b ~=> 'c) => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "o'_m" 55)
"f o_m g == (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)"
+syntax
+ empty :: "'a ~=> 'b"
+translations
+ "empty" => "%_. None"
+ "empty" <= "%x. None"
+
nonterminals
maplets maplet
syntax
- empty :: "'a ~=> 'b"
"_maplet" :: "['a, 'a] => maplet" ("_ /|->/ _")
"_maplets" :: "['a, 'a] => maplet" ("_ /[|->]/ _")
"" :: "maplet => maplets" ("_")
@@ -54,23 +53,11 @@
"_maplet" :: "['a, 'a] => maplet" ("_ /\<mapsto>/ _")
"_maplets" :: "['a, 'a] => maplet" ("_ /[\<mapsto>]/ _")
- map_upd_s :: "('a ~=> 'b) => 'a set => 'b => ('a ~=> 'b)"
- ("_/'(_/{\<mapsto>}/_')" [900,0,0]900)
- map_subst :: "('a ~=> 'b) => 'b => 'b =>
- ('a ~=> 'b)" ("_/'(_\<leadsto>_/')" [900,0,0]900)
- "@chg_map" :: "('a ~=> 'b) => 'a => ('b => 'b) => ('a ~=> 'b)"
- ("_/'(_/\<mapsto>\<lambda>_. _')" [900,0,0,0] 900)
-
syntax (latex output)
restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" ("_\<restriction>\<^bsub>_\<^esub>" [111,110] 110)
--"requires amssymb!"
translations
- "empty" => "%_. None"
- "empty" <= "%x. None"
-
- "m(x\<mapsto>\<lambda>y. f)" == "chg_map (\<lambda>y. f) x m"
-
"_MapUpd m (_Maplets xy ms)" == "_MapUpd (_MapUpd m xy) ms"
"_MapUpd m (_maplet x y)" == "m(x:=Some y)"
"_MapUpd m (_maplets x y)" == "map_upds m x y"
@@ -79,14 +66,10 @@
"_Maplets ms1 (_Maplets ms2 ms3)" <= "_Maplets (_Maplets ms1 ms2) ms3"
defs
-chg_map_def: "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
-
map_add_def: "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
restrict_map_def: "m|`A == %x. if x : A then m x else None"
map_upds_def: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
-map_upd_s_def: "m(as{|->}b) == %x. if x : as then Some b else m x"
-map_subst_def: "m(a~>b) == %x. if m x = Some a then Some b else m x"
dom_def: "dom(m) == {a. m a ~= None}"
ran_def: "ran(m) == {b. EX a. m a = Some b}"
@@ -97,6 +80,38 @@
"map_of [] = empty"
"map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
+(* special purpose constants that should be defined somewhere else and
+whose syntax is a bit odd as well:
+
+ "@chg_map" :: "('a ~=> 'b) => 'a => ('b => 'b) => ('a ~=> 'b)"
+ ("_/'(_/\<mapsto>\<lambda>_. _')" [900,0,0,0] 900)
+ "m(x\<mapsto>\<lambda>y. f)" == "chg_map (\<lambda>y. f) x m"
+
+map_upd_s::"('a ~=> 'b) => 'a set => 'b =>
+ ('a ~=> 'b)" ("_/'(_{|->}_/')" [900,0,0]900)
+map_subst::"('a ~=> 'b) => 'b => 'b =>
+ ('a ~=> 'b)" ("_/'(_~>_/')" [900,0,0]900)
+
+map_upd_s_def: "m(as{|->}b) == %x. if x : as then Some b else m x"
+map_subst_def: "m(a~>b) == %x. if m x = Some a then Some b else m x"
+
+ map_upd_s :: "('a ~=> 'b) => 'a set => 'b => ('a ~=> 'b)"
+ ("_/'(_/{\<mapsto>}/_')" [900,0,0]900)
+ map_subst :: "('a ~=> 'b) => 'b => 'b =>
+ ('a ~=> 'b)" ("_/'(_\<leadsto>_/')" [900,0,0]900)
+
+
+subsection {* @{term [source] map_upd_s} *}
+
+lemma map_upd_s_apply [simp]:
+ "(m(as{|->}b)) x = (if x : as then Some b else m x)"
+by (simp add: map_upd_s_def)
+
+lemma map_subst_apply [simp]:
+ "(m(a~>b)) x = (if m x = Some a then Some b else m x)"
+by (simp add: map_subst_def)
+
+*)
subsection {* @{term [source] empty} *}
@@ -166,18 +181,6 @@
done
-subsection {* @{term [source] chg_map} *}
-
-lemma chg_map_new[simp]: "m a = None ==> chg_map f a m = m"
-by (unfold chg_map_def, auto)
-
-lemma chg_map_upd[simp]: "m a = Some b ==> chg_map f a m = m(a|->f b)"
-by (unfold chg_map_def, auto)
-
-lemma chg_map_other [simp]: "a \<noteq> b \<Longrightarrow> chg_map f a m b = m b"
-by (auto simp: chg_map_def split add: option.split)
-
-
subsection {* @{term [source] map_of} *}
lemma map_of_eq_None_iff:
@@ -461,16 +464,6 @@
done
-subsection {* @{term [source] map_upd_s} *}
-
-lemma map_upd_s_apply [simp]:
- "(m(as{|->}b)) x = (if x : as then Some b else m x)"
-by (simp add: map_upd_s_def)
-
-lemma map_subst_apply [simp]:
- "(m(a~>b)) x = (if m x = Some a then Some b else m x)"
-by (simp add: map_subst_def)
-
subsection {* @{term [source] dom} *}
lemma domI: "m a = Some b ==> a : dom m"
--- a/src/HOL/Relation.thy Thu Mar 23 18:14:06 2006 +0100
+++ b/src/HOL/Relation.thy Thu Mar 23 20:03:53 2006 +0100
@@ -58,10 +58,9 @@
inv_image :: "('b * 'b) set => ('a => 'b) => ('a * 'a) set"
"inv_image r f == {(x, y). (f x, f y) : r}"
-syntax
+abbreviation (output)
reflexive :: "('a * 'a) set => bool" -- {* reflexivity over a type *}
-translations
- "reflexive" == "refl UNIV"
+ "reflexive = refl UNIV"
subsection {* The identity relation *}
--- a/src/HOL/Set.thy Thu Mar 23 18:14:06 2006 +0100
+++ b/src/HOL/Set.thy Thu Mar 23 20:03:53 2006 +0100
@@ -47,9 +47,11 @@
subsection {* Additional concrete syntax *}
+abbreviation (output)
+ range :: "('a => 'b) => 'b set" -- "of function"
+ "range f = f ` UNIV"
+
syntax
- range :: "('a => 'b) => 'b set" -- "of function"
-
"op ~:" :: "'a => 'a set => bool" ("op ~:") -- "non-membership"
"op ~:" :: "'a => 'a set => bool" ("(_/ ~: _)" [50, 51] 50)
@@ -72,7 +74,6 @@
"_Bex" :: "pttrn => 'a set => bool => bool" ("(3? _:_./ _)" [0, 0, 10] 10)
translations
- "range f" == "f`UNIV"
"x ~: y" == "~ (x : y)"
"{x, xs}" == "insert x {xs}"
"{x}" == "insert x {}"