# HG changeset patch # User nipkow # Date 1143140633 -3600 # Node ID ec5cd5b1804c9d5ea041eb3ad38063560c69fe75 # Parent bf84bdf05f140058c0c5a5d95cfd12b40cb266be Converted translations to abbbreviations. Removed a few odd functions from Map and AssocList. Moved chg_map from Map to Bali/Basis. diff -r bf84bdf05f14 -r ec5cd5b1804c src/HOL/Bali/Basis.thy --- 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 \ b \ chg_map f a m b = m b" +by (auto simp: chg_map_def split add: option.split) + section "unique association lists" diff -r bf84bdf05f14 -r ec5cd5b1804c src/HOL/Equiv_Relations.thy --- 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) \ 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 \ A ==> \y \ A. f y = c ==> (\y \ 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 \ 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 diff -r bf84bdf05f14 -r ec5cd5b1804c src/HOL/Fun.thy --- 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*) diff -r bf84bdf05f14 -r ec5cd5b1804c src/HOL/Library/AssocList.thy --- 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 \ ('key * 'val)list \ ('key * 'val)list" update :: "'key \ 'val \ ('key * 'val)list \ ('key * 'val)list" updates :: "'key list \ 'val list \ ('key * 'val)list \ ('key * 'val)list" - substitute :: "'val \ 'val \ ('key * 'val)list \ ('key * 'val)list" - map_at :: "('val \ 'val) \ 'key \ ('key * 'val)list \ ('key * 'val) list" merge :: "('key * 'val)list \ ('key * 'val)list \ ('key * 'val)list" compose :: "('key * 'a)list \ ('a * 'b)list \ ('key * 'b)list" restrict :: "('key set) \ ('key * 'val)list \ ('key * 'val)list" clearjunk :: "('key * 'val)list \ ('key * 'val)list" +(* a bit special + substitute :: "'val \ 'val \ ('key * 'val)list \ ('key * 'val)list" + map_at :: "('val \ 'val) \ 'key \ ('key * 'val)list \ ('key * 'val) list" +*) + defs delete_def: "delete k \ filter (\p. fst p \ k)" @@ -35,15 +38,18 @@ "updates (k#ks) vs al = (case vs of [] \ al | (v#vs') \ 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) \ length al" proof (induct al) @@ -431,7 +437,7 @@ "size xs = size ys \ 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 \ b \ map_of (map_at f a al) b = map_of al b" by (simp add: map_at_conv') - +*) (* ******************************************************************************** *) subsection {* @{const merge} *} (* ******************************************************************************** *) diff -r bf84bdf05f14 -r ec5cd5b1804c src/HOL/Map.thy --- 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 "\\<^sub>m" 50) constdefs map_comp :: "('b ~=> 'c) => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "o'_m" 55) "f o_m g == (\k. case g k of None \ None | Some v \ 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" ("_ /\/ _") "_maplets" :: "['a, 'a] => maplet" ("_ /[\]/ _") - 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) - "@chg_map" :: "('a ~=> 'b) => 'a => ('b => 'b) => ('a ~=> 'b)" - ("_/'(_/\\_. _')" [900,0,0,0] 900) - syntax (latex output) restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" ("_\\<^bsub>_\<^esub>" [111,110] 110) --"requires amssymb!" translations - "empty" => "%_. None" - "empty" <= "%x. None" - - "m(x\\y. f)" == "chg_map (\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)" + ("_/'(_/\\_. _')" [900,0,0,0] 900) + "m(x\\y. f)" == "chg_map (\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)" + ("_/'(_/{\}/_')" [900,0,0]900) + map_subst :: "('a ~=> 'b) => 'b => 'b => + ('a ~=> 'b)" ("_/'(_\_/')" [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 \ b \ 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" diff -r bf84bdf05f14 -r ec5cd5b1804c src/HOL/Relation.thy --- 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 *} diff -r bf84bdf05f14 -r ec5cd5b1804c src/HOL/Set.thy --- 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 {}"