equal
deleted
inserted
replaced
18 |
18 |
19 Goalw [update_def] "[| f`x = y; f: Pi(A,B); x: A |] ==> f(x:=y) = f"; |
19 Goalw [update_def] "[| f`x = y; f: Pi(A,B); x: A |] ==> f(x:=y) = f"; |
20 by (asm_simp_tac (simpset() addsimps [domain_of_fun, cons_absorb]) 1); |
20 by (asm_simp_tac (simpset() addsimps [domain_of_fun, cons_absorb]) 1); |
21 by (rtac fun_extension 1); |
21 by (rtac fun_extension 1); |
22 by (best_tac (claset() addIs [apply_type, if_type, lam_type]) 1); |
22 by (best_tac (claset() addIs [apply_type, if_type, lam_type]) 1); |
23 ba 1; |
23 by (assume_tac 1); |
24 by (Asm_simp_tac 1); |
24 by (Asm_simp_tac 1); |
25 qed "update_idem"; |
25 qed "update_idem"; |
26 |
26 |
27 |
27 |
28 (* [| f: Pi(A, B); x:A |] ==> f(x := f`x) = f *) |
28 (* [| f: Pi(A, B); x:A |] ==> f(x := f`x) = f *) |