cleanup for Fun.thy:
authoroheimb
Wed Aug 12 16:23:25 1998 +0200 (1998-08-12)
changeset 5305513925de8962
parent 5304 c133f16febc7
child 5306 3d1368a3a2a2
cleanup for Fun.thy:
merged Update.{thy|ML} into Fun.{thy|ML}
moved o_def from HOL.thy to Fun.thy
added Id_def to Fun.thy
moved image_compose from Set.ML to Fun.ML
moved o_apply and o_assoc from simpdata.ML to Fun.ML
moved fun_upd_same and fun_upd_other (from Map.ML) to Fun.ML
added fun_upd_twist to Fun.ML
src/HOL/Fun.ML
src/HOL/Fun.thy
src/HOL/HOL.thy
src/HOL/IsaMakefile
src/HOL/Main.thy
src/HOL/Set.ML
src/HOL/Update.ML
src/HOL/Update.thy
     1.1 --- a/src/HOL/Fun.ML	Wed Aug 12 16:21:18 1998 +0200
     1.2 +++ b/src/HOL/Fun.ML	Wed Aug 12 16:23:25 1998 +0200
     1.3 @@ -7,6 +7,17 @@
     1.4  *)
     1.5  
     1.6  
     1.7 +qed_goalw "o_apply" thy [o_def] "(f o g) x = f (g x)"
     1.8 + (K [rtac refl 1]);
     1.9 +Addsimps [o_apply];
    1.10 +
    1.11 +qed_goalw "o_assoc" thy [o_def] "f o (g o h) = f o g o h"
    1.12 +  (K [rtac ext 1, rtac refl 1]);
    1.13 +
    1.14 +Goalw [o_def] "(f o g)``r = f``(g``r)";
    1.15 +by (Blast_tac 1);
    1.16 +qed "image_compose";
    1.17 +
    1.18  Goal "(f = g) = (!x. f(x)=g(x))";
    1.19  by (rtac iffI 1);
    1.20  by (Asm_simp_tac 1);
    1.21 @@ -160,3 +171,35 @@
    1.22  
    1.23  
    1.24  val set_cs = claset() delrules [equalityI];
    1.25 +
    1.26 +
    1.27 +section "fun_upd";
    1.28 +
    1.29 +Goalw [fun_upd_def] "(f(x:=y) = f) = (f x = y)";
    1.30 +by Safe_tac;
    1.31 +by (etac subst 1);
    1.32 +by (rtac ext 2);
    1.33 +by Auto_tac;
    1.34 +qed "fun_upd_idem_iff";
    1.35 +
    1.36 +(* f x = y ==> f(x:=y) = f *)
    1.37 +bind_thm("fun_upd_idem", fun_upd_idem_iff RS iffD2);
    1.38 +
    1.39 +(* f(x := f x) = f *)
    1.40 +AddIffs [refl RS fun_upd_idem];
    1.41 +
    1.42 +Goal "(f(x:=y))z = (if z=x then y else f z)";
    1.43 +by (simp_tac (simpset() addsimps [fun_upd_def]) 1);
    1.44 +qed "fun_upd_apply";
    1.45 +Addsimps [fun_upd_apply];
    1.46 +
    1.47 +qed_goal "fun_upd_same" thy "(f(x:=y)) x = y" 
    1.48 +	(K [Simp_tac 1]);
    1.49 +qed_goal "fund_upd_other" thy "!!X. z~=x ==> (f(x:=y)) z = f z"
    1.50 +	(K [Asm_simp_tac 1]);
    1.51 +(*Addsimps [fun_upd_same, fun_upd_other];*)
    1.52 +
    1.53 +Goal "a ~= c ==> m(a:=b)(c:=d) = m(c:=d)(a:=b)";
    1.54 +by (rtac ext 1);
    1.55 +by (Auto_tac);
    1.56 +qed "fun_upd_twist";
     2.1 --- a/src/HOL/Fun.thy	Wed Aug 12 16:21:18 1998 +0200
     2.2 +++ b/src/HOL/Fun.thy	Wed Aug 12 16:23:25 1998 +0200
     2.3 @@ -12,15 +12,37 @@
     2.4                         (subset_refl,subset_trans,subset_antisym,psubset_eq)
     2.5  consts
     2.6  
     2.7 +  Id          ::  'a => 'a
     2.8 +  o           :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl 55)
     2.9    inj, surj   :: ('a => 'b) => bool                   (*inj/surjective*)
    2.10    inj_on      :: ['a => 'b, 'a set] => bool
    2.11    inv         :: ('a => 'b) => ('b => 'a)
    2.12 +  fun_upd  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
    2.13 +
    2.14 +nonterminals
    2.15 +  updbinds  updbind
    2.16 +
    2.17 +syntax
    2.18 +
    2.19 +  (* Let expressions *)
    2.20 +
    2.21 +  "_updbind"       :: ['a, 'a] => updbind             ("(2_ :=/ _)")
    2.22 +  ""               :: updbind => updbinds             ("_")
    2.23 +  "_updbinds"      :: [updbind, updbinds] => updbinds ("_,/ _")
    2.24 +  "_Update"        :: ['a, updbinds] => 'a            ("_/'((_)')" [900,0] 900)
    2.25 +
    2.26 +translations
    2.27 +  "_Update f (_updbinds b bs)"  == "_Update (_Update f b) bs"
    2.28 +  "f(x:=y)"                     == "fun_upd f x y"
    2.29  
    2.30  defs
    2.31  
    2.32 -  inj_def     "inj f          == ! x y. f(x)=f(y) --> x=y"
    2.33 -  inj_on_def  "inj_on f A     == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    2.34 -  surj_def    "surj f         == ! y. ? x. y=f(x)"
    2.35 -  inv_def     "inv(f::'a=>'b) == (% y. @x. f(x)=y)"
    2.36 +  Id_def	"Id             == %x. x"
    2.37 +  o_def   	"f o g          == %x. f(g(x))"
    2.38 +  inj_def	"inj f          == ! x y. f(x)=f(y) --> x=y"
    2.39 +  inj_on_def	"inj_on f A     == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    2.40 +  surj_def	"surj f         == ! y. ? x. y=f(x)"
    2.41 +  inv_def	"inv(f::'a=>'b) == % y. @x. f(x)=y"
    2.42 +  fun_upd_def	"f(a:=b)        == % x. if x=a then b else f x"
    2.43  
    2.44  end
     3.1 --- a/src/HOL/HOL.thy	Wed Aug 12 16:21:18 1998 +0200
     3.2 +++ b/src/HOL/HOL.thy	Wed Aug 12 16:23:25 1998 +0200
     3.3 @@ -47,7 +47,6 @@
     3.4  
     3.5    (* Infixes *)
     3.6  
     3.7 -  o             :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl 55)
     3.8    "="           :: ['a, 'a] => bool                 (infixl 50)
     3.9    "&"           :: [bool, bool] => bool             (infixr 35)
    3.10    "|"           :: [bool, bool] => bool             (infixr 30)
    3.11 @@ -180,7 +179,6 @@
    3.12  defs
    3.13    (*misc definitions*)
    3.14    Let_def       "Let s f == f(s)"
    3.15 -  o_def         "(f::'b=>'c) o g == (%(x::'a). f(g(x)))"
    3.16    if_def        "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
    3.17  
    3.18    (*arbitrary is completely unspecified, but is made to appear as a
     4.1 --- a/src/HOL/IsaMakefile	Wed Aug 12 16:21:18 1998 +0200
     4.2 +++ b/src/HOL/IsaMakefile	Wed Aug 12 16:23:25 1998 +0200
     4.3 @@ -52,7 +52,7 @@
     4.4    Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
     4.5    Tools/inductive_package.ML Tools/primrec_package.ML Tools/record_package.ML \
     4.6    Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
     4.7 -  Update.ML Update.thy Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML \
     4.8 +  Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML \
     4.9    WF_Rel.thy arith_data.ML cladata.ML equalities.ML \
    4.10    equalities.thy hologic.ML mono.ML mono.thy simpdata.ML subset.ML \
    4.11    subset.thy thy_syntax.ML
     5.1 --- a/src/HOL/Main.thy	Wed Aug 12 16:21:18 1998 +0200
     5.2 +++ b/src/HOL/Main.thy	Wed Aug 12 16:23:25 1998 +0200
     5.3 @@ -1,4 +1,4 @@
     5.4  
     5.5  (*theory Main includes everything*)
     5.6  
     5.7 -Main = Update + Map + Record + Bin + RelPow + Sexp + String + Recdef
     5.8 +Main = Map + Record + Bin + RelPow + Sexp + String + Recdef
     6.1 --- a/src/HOL/Set.ML	Wed Aug 12 16:21:18 1998 +0200
     6.2 +++ b/src/HOL/Set.ML	Wed Aug 12 16:23:25 1998 +0200
     6.3 @@ -606,10 +606,6 @@
     6.4  AddIs  [image_eqI];
     6.5  AddSEs [imageE]; 
     6.6  
     6.7 -Goalw [o_def] "(f o g)``r = f``(g``r)";
     6.8 -by (Blast_tac 1);
     6.9 -qed "image_compose";
    6.10 -
    6.11  Goal "f``(A Un B) = f``A Un f``B";
    6.12  by (Blast_tac 1);
    6.13  qed "image_Un";
     7.1 --- a/src/HOL/Update.ML	Wed Aug 12 16:21:18 1998 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,27 +0,0 @@
     7.4 -(*  Title:      HOL/Update.thy
     7.5 -    ID:         $Id$
     7.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.7 -    Copyright   1998  University of Cambridge
     7.8 -
     7.9 -Function updates: like theory Map, but for ordinary functions
    7.10 -*)
    7.11 -
    7.12 -open Update;
    7.13 -
    7.14 -Goalw [fun_upd_def] "(f(x:=y) = f) = (f x = y)";
    7.15 -by Safe_tac;
    7.16 -by (etac subst 1);
    7.17 -by (rtac ext 2);
    7.18 -by Auto_tac;
    7.19 -qed "fun_upd_idem_iff";
    7.20 -
    7.21 -(* f x = y ==> f(x:=y) = f *)
    7.22 -bind_thm("fun_upd_idem", fun_upd_idem_iff RS iffD2);
    7.23 -
    7.24 -(* f(x := f x) = f *)
    7.25 -AddIffs [refl RS fun_upd_idem];
    7.26 -
    7.27 -Goal "(f(x:=y))z = (if z=x then y else f z)";
    7.28 -by (simp_tac (simpset() addsimps [fun_upd_def]) 1);
    7.29 -qed "fun_upd_apply";
    7.30 -Addsimps [fun_upd_apply];
     8.1 --- a/src/HOL/Update.thy	Wed Aug 12 16:21:18 1998 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,33 +0,0 @@
     8.4 -(*  Title:      HOL/Update.thy
     8.5 -    ID:         $Id$
     8.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.7 -    Copyright   1998  University of Cambridge
     8.8 -
     8.9 -Function updates: like theory Map, but for ordinary functions
    8.10 -*)
    8.11 -
    8.12 -Update = Fun +
    8.13 -
    8.14 -consts
    8.15 -  fun_upd  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
    8.16 -
    8.17 -nonterminals
    8.18 -  updbinds  updbind
    8.19 -
    8.20 -syntax
    8.21 -
    8.22 -  (* Let expressions *)
    8.23 -
    8.24 -  "_updbind"       :: ['a, 'a] => updbind             ("(2_ :=/ _)")
    8.25 -  ""               :: updbind => updbinds             ("_")
    8.26 -  "_updbinds"      :: [updbind, updbinds] => updbinds ("_,/ _")
    8.27 -  "_Update"        :: ['a, updbinds] => 'a            ("_/'((_)')" [900,0] 900)
    8.28 -
    8.29 -translations
    8.30 -  "_Update f (_updbinds b bs)"  == "_Update (_Update f b) bs"
    8.31 -  "f(x:=y)"                     == "fun_upd f x y"
    8.32 -
    8.33 -defs
    8.34 -  fun_upd_def "f(a:=b) == %x. if x=a then b else f x"
    8.35 -
    8.36 -end