src/HOL/Fun.ML
author clasohm
Wed Mar 13 11:55:25 1996 +0100 (1996-03-13 ago)
changeset 1574 5a63ab90ee8a
parent 1561 9ba6d69f7763
child 1666 5183de4c496d
permissions -rw-r--r--
modified primrec so it can be used in MiniML/Type.thy
     1 (*  Title:      HOL/Fun
     2     ID:         $Id$
     3     Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Lemmas about functions.
     7 *)
     8 
     9 simpset := HOL_ss;
    10 
    11 goal Fun.thy "(f = g) = (!x. f(x)=g(x))";
    12 by (rtac iffI 1);
    13 by (Asm_simp_tac 1);
    14 by (rtac ext 1 THEN Asm_simp_tac 1);
    15 qed "expand_fun_eq";
    16 
    17 val prems = goal Fun.thy
    18     "[| f(x)=u;  !!x. P(x) ==> g(f(x)) = x;  P(x) |] ==> x=g(u)";
    19 by (rtac (arg_cong RS box_equals) 1);
    20 by (REPEAT (resolve_tac (prems@[refl]) 1));
    21 qed "apply_inverse";
    22 
    23 
    24 (*** Range of a function ***)
    25 
    26 (*Frequently b does not have the syntactic form of f(x).*)
    27 val [prem] = goalw Fun.thy [range_def] "b=f(x) ==> b : range(f)";
    28 by (EVERY1 [rtac CollectI, rtac exI, rtac prem]);
    29 qed "range_eqI";
    30 
    31 val rangeI = refl RS range_eqI;
    32 
    33 val [major,minor] = goalw Fun.thy [range_def]
    34     "[| b : range(%x.f(x));  !!x. b=f(x) ==> P |] ==> P"; 
    35 by (rtac (major RS CollectD RS exE) 1);
    36 by (etac minor 1);
    37 qed "rangeE";
    38 
    39 (*** Image of a set under a function ***)
    40 
    41 val prems = goalw Fun.thy [image_def] "[| b=f(x);  x:A |] ==> b : f``A";
    42 by (REPEAT (resolve_tac (prems @ [CollectI,bexI,prem]) 1));
    43 qed "image_eqI";
    44 
    45 val imageI = refl RS image_eqI;
    46 
    47 (*The eta-expansion gives variable-name preservation.*)
    48 val major::prems = goalw Fun.thy [image_def]
    49     "[| b : (%x.f(x))``A;  !!x.[| b=f(x);  x:A |] ==> P |] ==> P"; 
    50 by (rtac (major RS CollectD RS bexE) 1);
    51 by (REPEAT (ares_tac prems 1));
    52 qed "imageE";
    53 
    54 goalw Fun.thy [o_def] "(f o g)``r = f``(g``r)";
    55 by (rtac set_ext 1);
    56 by (fast_tac (HOL_cs addIs [imageI] addSEs [imageE]) 1);
    57 qed "image_compose";
    58 
    59 goal Fun.thy "f``(A Un B) = f``A Un f``B";
    60 by (rtac set_ext 1);
    61 by (fast_tac (HOL_cs addIs [imageI,UnCI] addSEs [imageE,UnE]) 1);
    62 qed "image_Un";
    63 
    64 (*** inj(f): f is a one-to-one function ***)
    65 
    66 val prems = goalw Fun.thy [inj_def]
    67     "[| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)";
    68 by (fast_tac (HOL_cs addIs prems) 1);
    69 qed "injI";
    70 
    71 val [major] = goal Fun.thy "(!!x. g(f(x)) = x) ==> inj(f)";
    72 by (rtac injI 1);
    73 by (etac (arg_cong RS box_equals) 1);
    74 by (rtac major 1);
    75 by (rtac major 1);
    76 qed "inj_inverseI";
    77 
    78 val [major,minor] = goalw Fun.thy [inj_def]
    79     "[| inj(f); f(x) = f(y) |] ==> x=y";
    80 by (rtac (major RS spec RS spec RS mp) 1);
    81 by (rtac minor 1);
    82 qed "injD";
    83 
    84 (*Useful with the simplifier*)
    85 val [major] = goal Fun.thy "inj(f) ==> (f(x) = f(y)) = (x=y)";
    86 by (rtac iffI 1);
    87 by (etac (major RS injD) 1);
    88 by (etac arg_cong 1);
    89 qed "inj_eq";
    90 
    91 val [major] = goal Fun.thy "inj(f) ==> (@x.f(x)=f(y)) = y";
    92 by (rtac (major RS injD) 1);
    93 by (rtac selectI 1);
    94 by (rtac refl 1);
    95 qed "inj_select";
    96 
    97 (*A one-to-one function has an inverse (given using select).*)
    98 val [major] = goalw Fun.thy [Inv_def] "inj(f) ==> Inv f (f x) = x";
    99 by (EVERY1 [rtac (major RS inj_select)]);
   100 qed "Inv_f_f";
   101 
   102 (* Useful??? *)
   103 val [oneone,minor] = goal Fun.thy
   104     "[| inj(f); !!y. y: range(f) ==> P(Inv f y) |] ==> P(x)";
   105 by (res_inst_tac [("t", "x")] (oneone RS (Inv_f_f RS subst)) 1);
   106 by (rtac (rangeI RS minor) 1);
   107 qed "inj_transfer";
   108 
   109 
   110 (*** inj_onto f A: f is one-to-one over A ***)
   111 
   112 val prems = goalw Fun.thy [inj_onto_def]
   113     "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_onto f A";
   114 by (fast_tac (HOL_cs addIs prems addSIs [ballI]) 1);
   115 qed "inj_ontoI";
   116 
   117 val [major] = goal Fun.thy 
   118     "(!!x. x:A ==> g(f(x)) = x) ==> inj_onto f A";
   119 by (rtac inj_ontoI 1);
   120 by (etac (apply_inverse RS trans) 1);
   121 by (REPEAT (eresolve_tac [asm_rl,major] 1));
   122 qed "inj_onto_inverseI";
   123 
   124 val major::prems = goalw Fun.thy [inj_onto_def]
   125     "[| inj_onto f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
   126 by (rtac (major RS bspec RS bspec RS mp) 1);
   127 by (REPEAT (resolve_tac prems 1));
   128 qed "inj_ontoD";
   129 
   130 goal Fun.thy "!!x y.[| inj_onto f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
   131 by (fast_tac (HOL_cs addSEs [inj_ontoD]) 1);
   132 qed "inj_onto_iff";
   133 
   134 val major::prems = goal Fun.thy
   135     "[| inj_onto f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
   136 by (rtac contrapos 1);
   137 by (etac (major RS inj_ontoD) 2);
   138 by (REPEAT (resolve_tac prems 1));
   139 qed "inj_onto_contraD";
   140 
   141 
   142 (*** Lemmas about inj ***)
   143 
   144 val prems = goalw Fun.thy [o_def]
   145     "[| inj(f);  inj_onto g (range f) |] ==> inj(g o f)";
   146 by (cut_facts_tac prems 1);
   147 by (fast_tac (HOL_cs addIs [injI,rangeI]
   148                      addEs [injD,inj_ontoD]) 1);
   149 qed "comp_inj";
   150 
   151 val [prem] = goal Fun.thy "inj(f) ==> inj_onto f A";
   152 by (fast_tac (HOL_cs addIs [prem RS injD, inj_ontoI]) 1);
   153 qed "inj_imp";
   154 
   155 val [prem] = goalw Fun.thy [Inv_def] "y : range(f) ==> f(Inv f y) = y";
   156 by (EVERY1 [rtac (prem RS rangeE), rtac selectI, etac sym]);
   157 qed "f_Inv_f";
   158 
   159 val prems = goal Fun.thy
   160     "[| Inv f x=Inv f y; x: range(f);  y: range(f) |] ==> x=y";
   161 by (rtac (arg_cong RS box_equals) 1);
   162 by (REPEAT (resolve_tac (prems @ [f_Inv_f]) 1));
   163 qed "Inv_injective";
   164 
   165 val prems = goal Fun.thy
   166     "[| inj(f);  A<=range(f) |] ==> inj_onto (Inv f) A";
   167 by (cut_facts_tac prems 1);
   168 by (fast_tac (HOL_cs addIs [inj_ontoI] 
   169                      addEs [Inv_injective,injD,subsetD]) 1);
   170 qed "inj_onto_Inv";
   171 
   172 
   173 (*** Set reasoning tools ***)
   174 
   175 val set_cs = HOL_cs 
   176     addSIs [ballI, PowI, subsetI, InterI, INT_I, INT1_I, CollectI, 
   177             ComplI, IntI, DiffI, UnCI, insertCI] 
   178     addIs  [bexI, UnionI, UN_I, UN1_I, imageI, rangeI] 
   179     addSEs [bexE, make_elim PowD, UnionE, UN_E, UN1_E, DiffE,
   180 	    make_elim singleton_inject,
   181             CollectE, ComplE, IntE, UnE, insertE, imageE, rangeE, emptyE] 
   182     addEs  [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D,
   183             subsetD, subsetCE];
   184 
   185 fun cfast_tac prems = cut_facts_tac prems THEN' fast_tac set_cs;
   186 
   187 
   188 fun prover s = prove_goal Fun.thy s (fn _=>[fast_tac set_cs 1]);
   189 
   190 val mem_simps = map prover
   191  [ "(a : A Un B)   =  (a:A | a:B)",
   192    "(a : A Int B)  =  (a:A & a:B)",
   193    "(a : Compl(B)) =  (~a:B)",
   194    "(a : A-B)      =  (a:A & ~a:B)",
   195    "(a : {b})      =  (a=b)",
   196    "(a : {x.P(x)}) =  P(a)" ];
   197 
   198 val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;
   199 
   200 simpset := !simpset addsimps mem_simps
   201                     addcongs [ball_cong,bex_cong]
   202                     setmksimps (mksimps mksimps_pairs);