equal
deleted
inserted
replaced
48 |
48 |
49 (* ------------------------------------------------------------------------ *) |
49 (* ------------------------------------------------------------------------ *) |
50 (* lemmas about application of continuous functions *) |
50 (* lemmas about application of continuous functions *) |
51 (* ------------------------------------------------------------------------ *) |
51 (* ------------------------------------------------------------------------ *) |
52 |
52 |
53 Goal "[| f=g; x=y |] ==> f`x = g`y"; |
53 Goal "[| f=g; x=y |] ==> f$x = g$y"; |
54 by (Asm_simp_tac 1); |
54 by (Asm_simp_tac 1); |
55 qed "cfun_cong"; |
55 qed "cfun_cong"; |
56 |
56 |
57 Goal "f=g ==> f`x = g`x"; |
57 Goal "f=g ==> f$x = g$x"; |
58 by (Asm_simp_tac 1); |
58 by (Asm_simp_tac 1); |
59 qed "cfun_fun_cong"; |
59 qed "cfun_fun_cong"; |
60 |
60 |
61 Goal "x=y ==> f`x = f`y"; |
61 Goal "x=y ==> f$x = f$y"; |
62 by (Asm_simp_tac 1); |
62 by (Asm_simp_tac 1); |
63 qed "cfun_arg_cong"; |
63 qed "cfun_arg_cong"; |
64 |
64 |
65 |
65 |
66 (* ------------------------------------------------------------------------ *) |
66 (* ------------------------------------------------------------------------ *) |
75 |
75 |
76 (* ------------------------------------------------------------------------ *) |
76 (* ------------------------------------------------------------------------ *) |
77 (* simplification of application *) |
77 (* simplification of application *) |
78 (* ------------------------------------------------------------------------ *) |
78 (* ------------------------------------------------------------------------ *) |
79 |
79 |
80 Goal "cont f ==> (Abs_CFun f)`x = f x"; |
80 Goal "cont f ==> (Abs_CFun f)$x = f x"; |
81 by (etac (Abs_Cfun_inverse2 RS fun_cong) 1); |
81 by (etac (Abs_Cfun_inverse2 RS fun_cong) 1); |
82 qed "Cfunapp2"; |
82 qed "Cfunapp2"; |
83 |
83 |
84 (* ------------------------------------------------------------------------ *) |
84 (* ------------------------------------------------------------------------ *) |
85 (* beta - equality for continuous functions *) |
85 (* beta - equality for continuous functions *) |
86 (* ------------------------------------------------------------------------ *) |
86 (* ------------------------------------------------------------------------ *) |
87 |
87 |
88 Goal "cont(c1) ==> (LAM x .c1 x)`u = c1 u"; |
88 Goal "cont(c1) ==> (LAM x .c1 x)$u = c1 u"; |
89 by (rtac Cfunapp2 1); |
89 by (rtac Cfunapp2 1); |
90 by (atac 1); |
90 by (atac 1); |
91 qed "beta_cfun"; |
91 qed "beta_cfun"; |