the function space operator
authorpaulson
Fri Nov 13 13:26:16 1998 +0100 (1998-11-13)
changeset 58524d7320490be4
parent 5851 15ce4c1c8313
child 5853 36b5559d8224
the function space operator
src/HOL/Fun.ML
src/HOL/Fun.thy
     1.1 --- a/src/HOL/Fun.ML	Thu Nov 12 16:45:40 1998 +0100
     1.2 +++ b/src/HOL/Fun.ML	Fri Nov 13 13:26:16 1998 +0100
     1.3 @@ -58,6 +58,10 @@
     1.4  by (Blast_tac 1);
     1.5  qed "image_compose";
     1.6  
     1.7 +Goalw [o_def] "UNION A (g o f) = UNION (f``A) g";
     1.8 +by (Blast_tac 1);
     1.9 +qed "UNION_o";
    1.10 +
    1.11  
    1.12  section "inj";
    1.13  
    1.14 @@ -219,3 +223,156 @@
    1.15  by (rtac ext 1);
    1.16  by (Auto_tac);
    1.17  qed "fun_upd_twist";
    1.18 +
    1.19 +
    1.20 +(*** -> and Pi, by Florian Kammueller and LCP ***)
    1.21 +
    1.22 +val prems = Goalw [Pi_def]
    1.23 +"[| !!x. x: A ==> f x: B x; !!x. x ~: A  ==> f(x) = (@ y. True)|] \
    1.24 +\    ==> f: Pi A B";
    1.25 +by (auto_tac (claset(), simpset() addsimps prems));
    1.26 +qed "Pi_I";
    1.27 +
    1.28 +val prems = Goal 
    1.29 +"[| !!x. x: A ==> f x: B; !!x. x ~: A  ==> f(x) = (@ y. True)|] ==> f: A funcset B";
    1.30 +by (blast_tac (claset() addIs Pi_I::prems) 1);
    1.31 +qed "funcsetI";
    1.32 +
    1.33 +Goalw [Pi_def] "[|f: Pi A B; x: A|] ==> f x: B x";
    1.34 +by Auto_tac;
    1.35 +qed "Pi_mem";
    1.36 +
    1.37 +Goalw [Pi_def] "[|f: A funcset B; x: A|] ==> f x: B";
    1.38 +by Auto_tac;
    1.39 +qed "funcset_mem";
    1.40 +
    1.41 +Goalw [Pi_def] "[|f: Pi A B; x~: A|] ==> f x = (@ y. True)";
    1.42 +by Auto_tac;
    1.43 +qed "apply_arb";
    1.44 +
    1.45 +Goalw [Pi_def] "[| f: Pi A B; g: Pi A B; ! x: A. f x = g x |] ==> f = g";
    1.46 +by (rtac ext 1);
    1.47 +by Auto_tac;
    1.48 +val Pi_extensionality = ballI RSN (3, result());
    1.49 +
    1.50 +(*** compose ***)
    1.51 +
    1.52 +Goalw [Pi_def, compose_def, restrict_def]
    1.53 +     "[| f: A funcset B; g: B funcset C |]==> compose A g f: A funcset C";
    1.54 +by Auto_tac;
    1.55 +qed "funcset_compose";
    1.56 +
    1.57 +Goal "[| f: A funcset B; g: B funcset C; h: C funcset D |]\
    1.58 +\     ==> compose A h (compose A g f) = compose A (compose B h g) f";
    1.59 +by (res_inst_tac [("A","A")] Pi_extensionality 1);
    1.60 +by (blast_tac (claset() addIs [funcset_compose]) 1);
    1.61 +by (blast_tac (claset() addIs [funcset_compose]) 1);
    1.62 +by (rewrite_goals_tac [Pi_def, compose_def, restrict_def]);  
    1.63 +by Auto_tac;
    1.64 +qed "compose_assoc";
    1.65 +
    1.66 +Goal "[| f: A funcset B; g: B funcset C; x: A |]==> compose A g f x = g(f(x))";
    1.67 +by (asm_full_simp_tac (simpset() addsimps [compose_def, restrict_def]) 1);
    1.68 +qed "compose_eq";
    1.69 +
    1.70 +Goal "[| f : A funcset B; f `` A = B; g: B funcset C; g `` B = C |]\
    1.71 +\     ==> compose A g f `` A = C";
    1.72 +by (auto_tac (claset(),
    1.73 +	      simpset() addsimps [image_def, compose_eq]));
    1.74 +qed "surj_compose";
    1.75 +
    1.76 +
    1.77 +Goal "[| f : A funcset B; g: B funcset C; f `` A = B; inj_on f A; inj_on g B |]\
    1.78 +\     ==> inj_on (compose A g f) A";
    1.79 +by (auto_tac (claset(),
    1.80 +	      simpset() addsimps [inj_on_def, compose_eq]));
    1.81 +qed "inj_on_compose";
    1.82 +
    1.83 +
    1.84 +(*** restrict / lam ***)
    1.85 +Goal "[| f `` A <= B |] ==> (lam x: A. f x) : A funcset B";
    1.86 +by (auto_tac (claset(),
    1.87 +	      simpset() addsimps [restrict_def, Pi_def]));
    1.88 +qed "restrict_in_funcset";
    1.89 +
    1.90 +val prems = Goalw [restrict_def, Pi_def]
    1.91 +     "(!!x. x: A ==> f x: B x) ==> (lam x: A. f x) : Pi A B";
    1.92 +by (asm_simp_tac (simpset() addsimps prems) 1);
    1.93 +qed "restrictI";
    1.94 +
    1.95 +
    1.96 +Goal "x: A ==> (lam y: A. f y) x = f x";
    1.97 +by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
    1.98 +qed "restrict_apply1";
    1.99 +
   1.100 +Goal "[| x: A; f : A funcset B |] ==> (lam y: A. f y) x : B";
   1.101 +by (asm_full_simp_tac (simpset() addsimps [restrict_apply1,Pi_def]) 1);
   1.102 +qed "restrict_apply1_mem";
   1.103 +
   1.104 +Goal "x ~: A ==> (lam y: A. f y) x =  (@ y. True)";
   1.105 +by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
   1.106 +qed "restrict_apply2";
   1.107 +
   1.108 +
   1.109 +val prems = Goal
   1.110 +    "(!!x. x: A ==> f x = g x) ==> (lam x: A. f x) = (lam x: A. g x)";
   1.111 +by (rtac ext 1);
   1.112 +by (auto_tac (claset(),
   1.113 +	      simpset() addsimps prems@[restrict_def, Pi_def]));
   1.114 +qed "restrict_ext";
   1.115 +
   1.116 +
   1.117 +(*** Inverse ***)
   1.118 +
   1.119 +Goal "[|f `` A = B;  x: B |] ==> ? y: A. f y = x";
   1.120 +by (Blast_tac 1);
   1.121 +qed "surj_image";
   1.122 +
   1.123 +Goalw [Inv_def] "[| f `` A = B; f : A funcset B |] \
   1.124 +\                ==> (lam x: B. (Inv A f) x) : B funcset A";
   1.125 +by (fast_tac (claset() addIs [restrict_in_funcset, selectI2]) 1);
   1.126 +qed "Inv_funcset";
   1.127 +
   1.128 +
   1.129 +Goal "[| f: A funcset B;  inj_on f A;  f `` A = B;  x: A |] \
   1.130 +\     ==> (lam y: B. (Inv A f) y) (f x) = x";
   1.131 +by (asm_simp_tac (simpset() addsimps [restrict_apply1, funcset_mem]) 1);
   1.132 +by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1);
   1.133 +by (rtac selectI2 1);
   1.134 +by Auto_tac;
   1.135 +qed "Inv_f_f";
   1.136 +
   1.137 +Goal "[| f: A funcset B;  f `` A = B;  x: B |] \
   1.138 +\     ==> f ((lam y: B. (Inv A f y)) x) = x";
   1.139 +by (asm_simp_tac (simpset() addsimps [Inv_def, restrict_apply1]) 1);
   1.140 +by (fast_tac (claset() addIs [selectI2]) 1);
   1.141 +qed "f_Inv_f";
   1.142 +
   1.143 +Goal "[| f: A funcset B;  inj_on f A;  f `` A = B |]\
   1.144 +\     ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)";
   1.145 +by (rtac Pi_extensionality 1);
   1.146 +by (blast_tac (claset() addIs [funcset_compose, Inv_funcset]) 1);
   1.147 +by (blast_tac (claset() addIs [restrict_in_funcset]) 1);
   1.148 +by (asm_simp_tac
   1.149 +    (simpset() addsimps [restrict_apply1, compose_def, Inv_f_f]) 1);
   1.150 +qed "compose_Inv_id";
   1.151 +
   1.152 +
   1.153 +(*** Pi and Applyall ***)
   1.154 +
   1.155 +Goalw [Pi_def] "[| B(x) = {};  x: A |] ==> (PI x: A. B x) = {}";
   1.156 +by Auto_tac;
   1.157 +qed "Pi_eq_empty";
   1.158 +
   1.159 +Goal "[| (PI x: A. B x) ~= {};  x: A |] ==> B(x) ~= {}";
   1.160 +by (blast_tac (HOL_cs addIs [Pi_eq_empty]) 1);
   1.161 +qed "Pi_total1";
   1.162 +
   1.163 +Goal "[| a : A; Pi A B ~= {} |] ==> Applyall (Pi A B) a = B a";
   1.164 +by (auto_tac (claset(), simpset() addsimps [Applyall_def, Pi_def]));
   1.165 +by (rename_tac "g z" 1);
   1.166 +by (res_inst_tac [("x","%y. if  (y = a) then z else g y")] exI 1);
   1.167 +by (auto_tac (claset(), simpset() addsimps [split_if_mem1, split_if_eq1]));
   1.168 +qed "Applyall_beta";
   1.169 +
   1.170 +
     2.1 --- a/src/HOL/Fun.thy	Thu Nov 12 16:45:40 1998 +0100
     2.2 +++ b/src/HOL/Fun.thy	Fri Nov 13 13:26:16 1998 +0100
     2.3 @@ -6,7 +6,7 @@
     2.4  Notions about functions.
     2.5  *)
     2.6  
     2.7 -Fun = Vimage +
     2.8 +Fun = Vimage + equalities + 
     2.9  
    2.10  instance set :: (term) order
    2.11                         (subset_refl,subset_trans,subset_antisym,psubset_eq)
    2.12 @@ -45,4 +45,40 @@
    2.13    inv_def	"inv(f::'a=>'b) == % y. @x. f(x)=y"
    2.14    fun_upd_def	"f(a:=b)        == % x. if x=a then b else f x"
    2.15  
    2.16 +
    2.17 +(*The Pi-operator, by Florian Kammueller*)
    2.18 +  
    2.19 +constdefs
    2.20 +  Pi      :: "['a set, 'a => 'b set] => ('a => 'b) set"
    2.21 +    "Pi A B == {f. ! x. if x:A then f(x) : B(x) else f(x) = (@ y. True)}"
    2.22 +
    2.23 +  restrict :: "['a => 'b, 'a set] => ('a => 'b)"
    2.24 +    "restrict f A == (%x. if x : A then f x else (@ y. True))"
    2.25 +
    2.26 +syntax
    2.27 +  "@Pi"  :: "[idt, 'a set, 'b set] => ('a => 'b) set"  ("(3PI _:_./ _)" 10)
    2.28 +  funcset :: "['a set, 'b set] => ('a => 'b) set"      (infixr 60) 
    2.29 +  "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)"  ("(3lam _:_./ _)" 10)
    2.30 +
    2.31 +  (*Giving funcset the nice arrow syntax -> clashes with existing theories*)
    2.32 +
    2.33 +translations
    2.34 +  "PI x:A. B" => "Pi A (%x. B)"
    2.35 +  "A funcset B"    => "Pi A (_K B)"
    2.36 +  "lam x:A. f"  == "restrict (%x. f) A"
    2.37 +
    2.38 +constdefs
    2.39 +  Applyall :: "[('a => 'b) set, 'a]=> 'b set"
    2.40 +    "Applyall F a == (%f. f a) `` F"
    2.41 +
    2.42 +  compose :: "['a set, 'a => 'b, 'b => 'c] => ('a => 'c)"
    2.43 +    "compose A g f == lam x : A. g(f x)"
    2.44 +
    2.45 +  Inv    :: "['a set, 'a => 'b] => ('b => 'a)"
    2.46 +    "Inv A f == (% x. (@ y. y : A & f y = x))"
    2.47 +
    2.48 +  
    2.49  end
    2.50 +
    2.51 +ML
    2.52 +val print_translation = [("Pi", dependent_tr' ("@Pi", "op funcset"))];