equal
deleted
inserted
replaced
87 by (rtac the_0 1); |
87 by (rtac the_0 1); |
88 by (Blast_tac 1); |
88 by (Blast_tac 1); |
89 qed "apply_0"; |
89 qed "apply_0"; |
90 |
90 |
91 Goal "[| f: Pi(A,B); c: f |] ==> EX x:A. c = <x,f`x>"; |
91 Goal "[| f: Pi(A,B); c: f |] ==> EX x:A. c = <x,f`x>"; |
92 by (forward_tac [fun_is_rel] 1); |
92 by (ftac fun_is_rel 1); |
93 by (blast_tac (claset() addDs [apply_equality]) 1); |
93 by (blast_tac (claset() addDs [apply_equality]) 1); |
94 qed "Pi_memberD"; |
94 qed "Pi_memberD"; |
95 |
95 |
96 Goal "[| f: Pi(A,B); a:A |] ==> <a,f`a>: f"; |
96 Goal "[| f: Pi(A,B); a:A |] ==> <a,f`a>: f"; |
97 by (rtac (fun_unique_Pair RS ex1E) 1); |
97 by (rtac (fun_unique_Pair RS ex1E) 1); |
110 Goal "[| f: A->B; a:A |] ==> f`a : B"; |
110 Goal "[| f: A->B; a:A |] ==> f`a : B"; |
111 by (REPEAT (ares_tac [apply_type] 1)); |
111 by (REPEAT (ares_tac [apply_type] 1)); |
112 qed "apply_funtype"; |
112 qed "apply_funtype"; |
113 |
113 |
114 Goal "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b"; |
114 Goal "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b"; |
115 by (forward_tac [fun_is_rel] 1); |
115 by (ftac fun_is_rel 1); |
116 by (blast_tac (claset() addSIs [apply_Pair, apply_equality]) 1); |
116 by (blast_tac (claset() addSIs [apply_Pair, apply_equality]) 1); |
117 qed "apply_iff"; |
117 qed "apply_iff"; |
118 |
118 |
119 (*Refining one Pi type to another*) |
119 (*Refining one Pi type to another*) |
120 val pi_prem::prems = Goal |
120 val pi_prem::prems = Goal |